src/HOL/TLA/Buffer/DBuffer.thy

 (*
     File:        DBuffer.thy
     ID:          $Id$
     Author:      Stephan Merz
     Copyright:   1997 University of Munich
-
-   Theory Name: DBuffer
-   Logic Image: TLA
 *)
 
 header {* Two FIFO buffers in a row, with interleaving assumption *}
 
 theory DBuffer

   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)"
 
-ML {* use_legacy_bindings (the_context ()) *}
+
+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 (simpset () 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