41589

1 
(* Title: HOL/TLA/Buffer/DBuffer.thy


2 
Author: Stephan Merz, University of Munich

3807

3 
*)


4 

17309

5 
header {* Two FIFO buffers in a row, with interleaving assumption *}


6 


7 
theory DBuffer


8 
imports Buffer


9 
begin

3807

10 


11 
consts


12 
(* implementation variables *)

17309

13 
inp :: "nat stfun"


14 
mid :: "nat stfun"


15 
out :: "nat stfun"


16 
q1 :: "nat list stfun"


17 
q2 :: "nat list stfun"


18 
qc :: "nat list stfun"

3807

19 

17309

20 
DBInit :: stpred


21 
DBEnq :: action


22 
DBDeq :: action


23 
DBPass :: action


24 
DBNext :: action


25 
DBuffer :: temporal

3807

26 

17309

27 
axioms


28 
DB_base: "basevars (inp,mid,out,q1,q2)"

3807

29 


30 
(* the concatenation of the two buffers *)

17309

31 
qc_def: "PRED qc == PRED (q2 @ q1)"

3807

32 

17309

33 
DBInit_def: "DBInit == PRED (BInit inp q1 mid & BInit mid q2 out)"


34 
DBEnq_def: "DBEnq == ACT Enq inp q1 mid & unchanged (q2,out)"


35 
DBDeq_def: "DBDeq == ACT Deq mid q2 out & unchanged (inp,q1)"


36 
DBPass_def: "DBPass == ACT Deq inp q1 mid

6255

37 
& (q2$ = $q2 @ [ mid$ ])


38 
& (out$ = $out)"

17309

39 
DBNext_def: "DBNext == ACT (DBEnq  DBDeq  DBPass)"


40 
DBuffer_def: "DBuffer == TEMP Init DBInit

6255

41 
& [][DBNext]_(inp,mid,out,q1,q2)


42 
& WF(DBDeq)_(inp,mid,out,q1,q2)


43 
& WF(DBPass)_(inp,mid,out,q1,q2)"

3807

44 

21624

45 


46 
declare qc_def [simp]


47 


48 
lemmas db_defs =


49 
BInit_def Enq_def Deq_def Next_def IBuffer_def Buffer_def


50 
DBInit_def DBEnq_def DBDeq_def DBPass_def DBNext_def DBuffer_def


51 


52 


53 
(*** Proper initialization ***)


54 
lemma DBInit: " Init DBInit > Init (BInit inp qc out)"


55 
by (auto simp: Init_def DBInit_def BInit_def)


56 


57 


58 
(*** Step simulation ***)


59 
lemma DB_step_simulation: " [DBNext]_(inp,mid,out,q1,q2) > [Next inp qc out]_(inp,qc,out)"


60 
apply (rule square_simulation)


61 
apply clarsimp


62 
apply (tactic

26342

63 
{* action_simp_tac (@{simpset} addsimps (@{thm hd_append} :: @{thms db_defs})) [] [] 1 *})

21624

64 
done


65 


66 


67 
(*** Simulation of fairness ***)


68 


69 
(* Compute enabledness predicates for DBDeq and DBPass actions *)


70 
lemma DBDeq_visible: " <DBDeq>_(inp,mid,out,q1,q2) = DBDeq"


71 
apply (unfold angle_def DBDeq_def Deq_def)


72 
apply (safe, simp (asm_lr))+


73 
done


74 


75 
lemma DBDeq_enabled:


76 
" Enabled (<DBDeq>_(inp,mid,out,q1,q2)) = (q2 ~= #[])"


77 
apply (unfold DBDeq_visible [action_rewrite])


78 
apply (force intro!: DB_base [THEN base_enabled, temp_use]


79 
elim!: enabledE simp: angle_def DBDeq_def Deq_def)


80 
done


81 


82 
lemma DBPass_visible: " <DBPass>_(inp,mid,out,q1,q2) = DBPass"


83 
by (auto simp: angle_def DBPass_def Deq_def)


84 


85 
lemma DBPass_enabled:


86 
" Enabled (<DBPass>_(inp,mid,out,q1,q2)) = (q1 ~= #[])"


87 
apply (unfold DBPass_visible [action_rewrite])


88 
apply (force intro!: DB_base [THEN base_enabled, temp_use]


89 
elim!: enabledE simp: angle_def DBPass_def Deq_def)


90 
done


91 


92 


93 
(* The plan for proving weak fairness at the higher level is to prove


94 
(0) DBuffer => (Enabled (Deq inp qc out) ~> (Deq inp qc out))


95 
which is in turn reduced to the two leadsto conditions


96 
(1) DBuffer => (Enabled (Deq inp qc out) ~> q2 ~= [])


97 
(2) DBuffer => (q2 ~= [] ~> DBDeq)


98 
and the fact that DBDeq implies <Deq inp qc out>_(inp,qc,out)


99 
(and therefore DBDeq ~> <Deq inp qc out>_(inp,qc,out) trivially holds).

17309

100 

21624

101 
Condition (1) is reduced to


102 
(1a) DBuffer => (qc ~= [] /\ q2 = [] ~> q2 ~= [])


103 
by standard leadsto rules (leadsto_classical) and rule Deq_enabledE.


104 


105 
Both (1a) and (2) are proved from DBuffer's WF conditions by standard


106 
WF reasoning (Lamport's WF1 and WF_leadsto).


107 
The condition WF(Deq inp qc out) follows from (0) by rule leadsto_WF.


108 


109 
One could use Lamport's WF2 instead.


110 
*)


111 


112 
(* Condition (1a) *)


113 
lemma DBFair_1a: " [][DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)


114 
> (qc ~= #[] & q2 = #[] ~> q2 ~= #[])"


115 
apply (rule WF1)


116 
apply (force simp: db_defs)


117 
apply (force simp: angle_def DBPass_def)


118 
apply (force simp: DBPass_enabled [temp_use])


119 
done


120 


121 
(* Condition (1) *)


122 
lemma DBFair_1: " [][DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)


123 
> (Enabled (<Deq inp qc out>_(inp,qc,out)) ~> q2 ~= #[])"


124 
apply clarsimp


125 
apply (rule leadsto_classical [temp_use])


126 
apply (rule DBFair_1a [temp_use, THEN LatticeTransitivity [temp_use]])


127 
apply assumption+


128 
apply (rule ImplLeadsto_gen [temp_use])


129 
apply (force intro!: necT [temp_use] dest!: STL2_gen [temp_use] Deq_enabledE [temp_use]


130 
simp add: Init_defs)


131 
done


132 


133 
(* Condition (2) *)


134 
lemma DBFair_2: " [][DBNext]_(inp,mid,out,q1,q2) & WF(DBDeq)_(inp,mid,out,q1,q2)


135 
> (q2 ~= #[] ~> DBDeq)"


136 
apply (rule WF_leadsto)


137 
apply (force simp: DBDeq_enabled [temp_use])


138 
apply (force simp: angle_def)


139 
apply (force simp: db_defs elim!: Stable [temp_use])


140 
done


141 


142 
(* Highlevel fairness *)


143 
lemma DBFair: " [][DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)


144 
& WF(DBDeq)_(inp,mid,out,q1,q2)


145 
> WF(Deq inp qc out)_(inp,qc,out)"


146 
apply (auto simp del: qc_def intro!: leadsto_WF [temp_use]


147 
DBFair_1 [temp_use, THEN [2] LatticeTransitivity [temp_use]]


148 
DBFair_2 [temp_use, THEN [2] LatticeTransitivity [temp_use]])


149 
apply (auto intro!: ImplLeadsto_simple [temp_use]


150 
simp: angle_def DBDeq_def Deq_def hd_append [try_rewrite])


151 
done


152 


153 
(*** Main theorem ***)


154 
lemma DBuffer_impl_Buffer: " DBuffer > Buffer inp out"


155 
apply (unfold DBuffer_def Buffer_def IBuffer_def)


156 
apply (force intro!: eexI [temp_use] DBInit [temp_use]


157 
DB_step_simulation [THEN STL4, temp_use] DBFair [temp_use])


158 
done


159 


160 
end
