# Theory DBuffer

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

section ‹Two FIFO buffers in a row, with interleaving assumption›

theory DBuffer
imports Buffer
begin

axiomatization
(* implementation variables *)
inp  :: "nat stfun" and
mid  :: "nat stfun" and
out  :: "nat stfun" and
q1   :: "nat list stfun" and
q2   :: "nat list stfun" and
qc   :: "nat list stfun" and

DBInit :: stpred and
DBEnq :: action and
DBDeq :: action and
DBPass :: action and
DBNext :: action and
DBuffer :: temporal
where
DB_base:        "basevars (inp,mid,out,q1,q2)" and

(* the concatenation of the two buffers *)
qc_def:         "PRED qc == PRED (q2 @ q1)" and

DBInit_def:     "DBInit   == PRED (BInit inp q1 mid  ∧  BInit mid q2 out)" and
DBEnq_def:      "DBEnq    == ACT  Enq inp q1 mid  ∧  unchanged (q2,out)" and
DBDeq_def:      "DBDeq    == ACT  Deq mid q2 out  ∧  unchanged (inp,q1)" and
DBPass_def:     "DBPass   == ACT  Deq inp q1 mid
∧ (q2\$ = \$q2 @ [ mid\$ ])
∧ (out\$ = \$out)" and
DBNext_def:     "DBNext   == ACT  (DBEnq ∨ DBDeq ∨ DBPass)" and
DBuffer_def:    "DBuffer  == TEMP Init DBInit
∧ □[DBNext]_(inp,mid,out,q1,q2)
∧ WF(DBDeq)_(inp,mid,out,q1,q2)
∧ WF(DBPass)_(inp,mid,out,q1,q2)"

declare qc_def [simp]

lemmas db_defs =
BInit_def Enq_def Deq_def Next_def IBuffer_def Buffer_def
DBInit_def DBEnq_def DBDeq_def DBPass_def DBNext_def DBuffer_def

(*** Proper initialization ***)
lemma DBInit: "⊢ Init DBInit ⟶ Init (BInit inp qc out)"
by (auto simp: Init_def DBInit_def BInit_def)

(*** Step simulation ***)
lemma DB_step_simulation: "⊢ [DBNext]_(inp,mid,out,q1,q2) ⟶ [Next inp qc out]_(inp,qc,out)"
apply (rule square_simulation)
apply clarsimp
apply (tactic
‹action_simp_tac (@{context} addsimps (@{thm hd_append} :: @{thms db_defs})) [] [] 1›)
done

(*** Simulation of fairness ***)

(* Compute enabledness predicates for DBDeq and DBPass actions *)
lemma DBDeq_visible: "⊢ <DBDeq>_(inp,mid,out,q1,q2) = DBDeq"
apply (unfold angle_def DBDeq_def Deq_def)
apply (safe, simp (asm_lr))+
done

lemma DBDeq_enabled:
"⊢ Enabled (<DBDeq>_(inp,mid,out,q1,q2)) = (q2 ≠ #[])"
apply (unfold DBDeq_visible [action_rewrite])
apply (force intro!: DB_base [THEN base_enabled, temp_use]
elim!: enabledE simp: angle_def DBDeq_def Deq_def)
done

lemma DBPass_visible: "⊢ <DBPass>_(inp,mid,out,q1,q2) = DBPass"
by (auto simp: angle_def DBPass_def Deq_def)

lemma DBPass_enabled:
"⊢ Enabled (<DBPass>_(inp,mid,out,q1,q2)) = (q1 ≠ #[])"
apply (unfold DBPass_visible [action_rewrite])
apply (force intro!: DB_base [THEN base_enabled, temp_use]
elim!: enabledE simp: angle_def DBPass_def Deq_def)
done

(* The plan for proving weak fairness at the higher level is to prove
(0)  DBuffer => (Enabled (Deq inp qc out) ↝ (Deq inp qc out))
which is in turn reduced to the two leadsto conditions
(1)  DBuffer => (Enabled (Deq inp qc out) ↝ q2 ≠ [])
(2)  DBuffer => (q2 ≠ [] ↝ DBDeq)
and the fact that DBDeq implies <Deq inp qc out>_(inp,qc,out)
(and therefore DBDeq ↝ <Deq inp qc out>_(inp,qc,out) trivially holds).

Condition (1) is reduced to
(1a) DBuffer => (qc ≠ [] /\ q2 = [] ↝ q2 ≠ [])
by standard leadsto rules (leadsto_classical) and rule Deq_enabledE.

Both (1a) and (2) are proved from DBuffer's WF conditions by standard
WF reasoning (Lamport's WF1 and WF_leadsto).
The condition WF(Deq inp qc out) follows from (0) by rule leadsto_WF.

One could use Lamport's WF2 instead.
*)

(* Condition (1a) *)
lemma DBFair_1a: "⊢ □[DBNext]_(inp,mid,out,q1,q2) ∧ WF(DBPass)_(inp,mid,out,q1,q2)
⟶ (qc ≠ #[] ∧ q2 = #[] ↝ q2 ≠ #[])"
apply (rule WF1)
apply (force simp: db_defs)
apply (force simp: angle_def DBPass_def)
apply (force simp: DBPass_enabled [temp_use])
done

(* Condition (1) *)
lemma DBFair_1: "⊢ □[DBNext]_(inp,mid,out,q1,q2) ∧ WF(DBPass)_(inp,mid,out,q1,q2)
⟶ (Enabled (<Deq inp qc out>_(inp,qc,out)) ↝ q2 ≠ #[])"
apply clarsimp
apply (rule leadsto_classical [temp_use])
apply (rule DBFair_1a [temp_use, THEN LatticeTransitivity [temp_use]])
apply assumption+
apply (rule ImplLeadsto_gen [temp_use])
apply (force intro!: necT [temp_use] dest!: STL2_gen [temp_use] Deq_enabledE [temp_use]
done

(* Condition (2) *)
lemma DBFair_2: "⊢ □[DBNext]_(inp,mid,out,q1,q2) ∧ WF(DBDeq)_(inp,mid,out,q1,q2)
⟶ (q2 ≠ #[] ↝ DBDeq)"
apply (force simp: DBDeq_enabled [temp_use])
apply (force simp: angle_def)
apply (force simp: db_defs elim!: Stable [temp_use])
done

(* High-level fairness *)
lemma DBFair: "⊢ □[DBNext]_(inp,mid,out,q1,q2) ∧ WF(DBPass)_(inp,mid,out,q1,q2)
∧ WF(DBDeq)_(inp,mid,out,q1,q2)
⟶ WF(Deq inp qc out)_(inp,qc,out)"
apply (auto simp del: qc_def intro!: leadsto_WF [temp_use]
DBFair_1 [temp_use, THEN [2] LatticeTransitivity [temp_use]]
DBFair_2 [temp_use, THEN [2] LatticeTransitivity [temp_use]])
apply (auto intro!: ImplLeadsto_simple [temp_use]
simp: angle_def DBDeq_def Deq_def hd_append [try_rewrite])
done

(*** Main theorem ***)
lemma DBuffer_impl_Buffer: "⊢ DBuffer ⟶ Buffer inp out"
apply (unfold DBuffer_def Buffer_def IBuffer_def)
apply (force intro!: eexI [temp_use] DBInit [temp_use]
DB_step_simulation [THEN STL4, temp_use] DBFair [temp_use])
done

end
```