src/HOL/TLA/Buffer/Buffer.thy

more symbols;

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

section {* A simple FIFO buffer (synchronous communication, interleaving) *}

theory Buffer
imports TLA
begin

consts
  (* actions *)
  BInit     :: "'a stfun => 'a list stfun => 'a stfun => stpred"
  Enq       :: "'a stfun => 'a list stfun => 'a stfun => action"
  Deq       :: "'a stfun => 'a list stfun => 'a stfun => action"
  Next      :: "'a stfun => 'a list stfun => 'a stfun => action"

  (* temporal formulas *)
  IBuffer   :: "'a stfun => 'a list stfun => 'a stfun => temporal"
  Buffer    :: "'a stfun => 'a stfun => temporal"

defs
  BInit_def:   "BInit ic q oc    == PRED q = #[]"
  Enq_def:     "Enq ic q oc      == ACT (ic$ \<noteq> $ic)
                                     & (q$ = $q @ [ ic$ ])
                                     & (oc$ = $oc)"
  Deq_def:     "Deq ic q oc      == ACT ($q \<noteq> #[])
                                     & (oc$ = hd< $q >)
                                     & (q$ = tl< $q >)
                                     & (ic$ = $ic)"
  Next_def:    "Next ic q oc     == ACT (Enq ic q oc | Deq ic q oc)"
  IBuffer_def: "IBuffer ic q oc  == TEMP Init (BInit ic q oc)
                                      & \<box>[Next ic q oc]_(ic,q,oc)
                                      & WF(Deq ic q oc)_(ic,q,oc)"
  Buffer_def:  "Buffer ic oc     == TEMP (\<exists>\<exists>q. IBuffer ic q oc)"


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

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


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

(* Dequeue is visible *)
lemma Deq_visible: "|- <Deq ic q oc>_(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: 
    "\<And>q. basevars (ic,q,oc) ==> |- Enabled (<Deq ic q oc>_(ic,q,oc)) = (q \<noteq> #[])"
  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 (<Deq ic q oc>_(ic,q,oc)) --> (q \<noteq> #[])"
  apply (unfold Deq_visible [temp_rewrite])
  apply (auto elim!: enabledE simp add: Deq_def)
  done

end