Quelle Buffer.thy Sprache: Isabelle

(*  Title:      HOL/TLA/Buffer/Buffer.thy
    Author:     Stephan Merz, University of Munich
*)

section \<open>A simple FIFO buffer (synchronous communication, interleaving)\<close>

theory Buffer
imports "HOL-TLA.TLA"
begin

(* actions *)

definition BInit :: "'a stfun \ 'a list stfun \ 'a stfun \ stpred"
  where "BInit ic q oc == PRED q = #[]"

definition Enq :: "'a stfun \ 'a list stfun \ 'a stfun \ action"
  where "Enq ic q oc == ACT (ic$ \ $ic)
                         \<and> (q$ = $q @ [ ic$ ])
                         \<and> (oc$ = $oc)"

definition Deq :: "'a stfun \ 'a list stfun \ 'a stfun \ action"
  where "Deq ic q oc == ACT ($q \ #[])
                         \<and> (oc$ = hd< $q >)
                         \<and> (q$ = tl< $q >)
                         \<and> (ic$ = $ic)"

definition Next :: "'a stfun \ 'a list stfun \ 'a stfun \ action"
  where "Next ic q oc == ACT (Enq ic q oc \ Deq ic q oc)"

(* temporal formulas *)

definition IBuffer :: "'a stfun \ 'a list stfun \ 'a stfun \ temporal"
  where "IBuffer ic q oc == TEMP Init (BInit ic q oc)
                                  \<and> \<box>[Next ic q oc]_(ic,q,oc)
                                  \<and> WF(Deq ic q oc)_(ic,q,oc)"

definition Buffer :: "'a stfun \ 'a stfun \ temporal"
  where "Buffer ic oc == TEMP (\\q. IBuffer ic q oc)"

(* ---------------------------- Data lemmas ---------------------------- *)

(*FIXME: move to theory List? Maybe as (tl xs = xs) = (xs = [])"?*)
lemma tl_not_self [simp]: "xs \ [] \ tl xs \ xs"
  by (auto simp: neq_Nil_conv)

(* ---------------------------- Action lemmas ---------------------------- *)

(* Dequeue is visible *)
lemma Deq_visible: "\ _(ic,q,oc) = Deq ic q oc"
  apply (unfold angle_def Deq_def)
  apply (safe, simp (asm_lr))+
  done

(* Enabling condition for dequeue -- NOT NEEDED *)
lemma Deq_enabled:
    "\q. basevars (ic,q,oc) \ \ Enabled (_(ic,q,oc)) = (q \ #[])"
  apply (unfold Deq_visible [temp_rewrite])
  apply (force elim!: base_enabled [temp_use] enabledE [temp_use] simp: Deq_def)
  done

(* For the left-to-right implication, we don't need the base variable stuff *)
lemma Deq_enabledE:
    "\ Enabled (_(ic,q,oc)) \ (q \ #[])"
  apply (unfold Deq_visible [temp_rewrite])
  apply (auto elim!: enabledE simp add: Deq_def)
  done

end

quality100%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.