Theory DBuffer

(*  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]
    simp add: Init_defs)
  done

(* Condition (2) *)
lemma DBFair_2: "⊢ □[DBNext]_(inp,mid,out,q1,q2) ∧ WF(DBDeq)_(inp,mid,out,q1,q2)  
         ⟶ (q2 ≠ #[] ↝ DBDeq)"
  apply (rule WF_leadsto)
    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