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

section ‹A simple FIFO buffer (synchronous communication, interleaving)›

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)
                         ∧ (q$ = $q @ [ ic$ ])
                         ∧ (oc$ = $oc)"

definition Deq :: "'a stfun → 'a list stfun → 'a stfun → action"
  where "Deq ic q oc == ACT ($q ≠ #[])
                         ∧ (oc$ = hd< $q >)
                         ∧ (q$ = tl< $q >)
                         ∧ (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)
                                  ∧ ◻[Next ic q oc]_(ic,q,oc)
                                  ∧ 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: "⊨ <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: 
    "∧q. basevars (ic,q,oc) ==> ⊨ Enabled (<Deq ic q oc>_(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 (<Deq ic q oc>_(ic,q,oc)) ⟶ (q ≠ #[])"
  apply (unfold Deq_visible [temp_rewrite])
  apply (auto elim!: enabledE simp add: Deq_def)
  done

end