# Theory Buffer

```(*  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
```