41589
|
1 |
(* Title: HOL/TLA/Inc/Inc.thy
|
|
2 |
Author: Stephan Merz, University of Munich
|
3807
|
3 |
*)
|
|
4 |
|
17309
|
5 |
header {* Lamport's "increment" example *}
|
|
6 |
|
|
7 |
theory Inc
|
|
8 |
imports TLA
|
|
9 |
begin
|
6255
|
10 |
|
|
11 |
(* program counter as an enumeration type *)
|
|
12 |
datatype pcount = a | b | g
|
3807
|
13 |
|
|
14 |
consts
|
|
15 |
(* program variables *)
|
17309
|
16 |
x :: "nat stfun"
|
|
17 |
y :: "nat stfun"
|
|
18 |
sem :: "nat stfun"
|
|
19 |
pc1 :: "pcount stfun"
|
|
20 |
pc2 :: "pcount stfun"
|
3807
|
21 |
|
|
22 |
(* names of actions and predicates *)
|
17309
|
23 |
M1 :: action
|
|
24 |
M2 :: action
|
|
25 |
N1 :: action
|
|
26 |
N2 :: action
|
|
27 |
alpha1 :: action
|
|
28 |
alpha2 :: action
|
|
29 |
beta1 :: action
|
|
30 |
beta2 :: action
|
|
31 |
gamma1 :: action
|
|
32 |
gamma2 :: action
|
|
33 |
InitPhi :: stpred
|
|
34 |
InitPsi :: stpred
|
|
35 |
PsiInv :: stpred
|
|
36 |
PsiInv1 :: stpred
|
|
37 |
PsiInv2 :: stpred
|
|
38 |
PsiInv3 :: stpred
|
3807
|
39 |
|
|
40 |
(* temporal formulas *)
|
17309
|
41 |
Phi :: temporal
|
|
42 |
Psi :: temporal
|
|
43 |
|
|
44 |
axioms
|
3807
|
45 |
(* the "base" variables, required to compute enabledness predicates *)
|
17309
|
46 |
Inc_base: "basevars (x, y, sem, pc1, pc2)"
|
3807
|
47 |
|
|
48 |
(* definitions for high-level program *)
|
17309
|
49 |
InitPhi_def: "InitPhi == PRED x = # 0 & y = # 0"
|
|
50 |
M1_def: "M1 == ACT x$ = Suc<$x> & y$ = $y"
|
|
51 |
M2_def: "M2 == ACT y$ = Suc<$y> & x$ = $x"
|
|
52 |
Phi_def: "Phi == TEMP Init InitPhi & [][M1 | M2]_(x,y)
|
6255
|
53 |
& WF(M1)_(x,y) & WF(M2)_(x,y)"
|
3807
|
54 |
|
|
55 |
(* definitions for low-level program *)
|
17309
|
56 |
InitPsi_def: "InitPsi == PRED pc1 = #a & pc2 = #a
|
6255
|
57 |
& x = # 0 & y = # 0 & sem = # 1"
|
17309
|
58 |
alpha1_def: "alpha1 == ACT $pc1 = #a & pc1$ = #b & $sem = Suc<sem$>
|
6255
|
59 |
& unchanged(x,y,pc2)"
|
17309
|
60 |
alpha2_def: "alpha2 == ACT $pc2 = #a & pc2$ = #b & $sem = Suc<sem$>
|
6255
|
61 |
& unchanged(x,y,pc1)"
|
17309
|
62 |
beta1_def: "beta1 == ACT $pc1 = #b & pc1$ = #g & x$ = Suc<$x>
|
6255
|
63 |
& unchanged(y,sem,pc2)"
|
17309
|
64 |
beta2_def: "beta2 == ACT $pc2 = #b & pc2$ = #g & y$ = Suc<$y>
|
6255
|
65 |
& unchanged(x,sem,pc1)"
|
17309
|
66 |
gamma1_def: "gamma1 == ACT $pc1 = #g & pc1$ = #a & sem$ = Suc<$sem>
|
6255
|
67 |
& unchanged(x,y,pc2)"
|
17309
|
68 |
gamma2_def: "gamma2 == ACT $pc2 = #g & pc2$ = #a & sem$ = Suc<$sem>
|
6255
|
69 |
& unchanged(x,y,pc1)"
|
17309
|
70 |
N1_def: "N1 == ACT (alpha1 | beta1 | gamma1)"
|
|
71 |
N2_def: "N2 == ACT (alpha2 | beta2 | gamma2)"
|
|
72 |
Psi_def: "Psi == TEMP Init InitPsi
|
6255
|
73 |
& [][N1 | N2]_(x,y,sem,pc1,pc2)
|
|
74 |
& SF(N1)_(x,y,sem,pc1,pc2)
|
|
75 |
& SF(N2)_(x,y,sem,pc1,pc2)"
|
3807
|
76 |
|
17309
|
77 |
PsiInv1_def: "PsiInv1 == PRED sem = # 1 & pc1 = #a & pc2 = #a"
|
|
78 |
PsiInv2_def: "PsiInv2 == PRED sem = # 0 & pc1 = #a & (pc2 = #b | pc2 = #g)"
|
|
79 |
PsiInv3_def: "PsiInv3 == PRED sem = # 0 & pc2 = #a & (pc1 = #b | pc1 = #g)"
|
|
80 |
PsiInv_def: "PsiInv == PRED (PsiInv1 | PsiInv2 | PsiInv3)"
|
|
81 |
|
21624
|
82 |
|
|
83 |
lemmas PsiInv_defs = PsiInv_def PsiInv1_def PsiInv2_def PsiInv3_def
|
|
84 |
lemmas Psi_defs = Psi_def InitPsi_def N1_def N2_def alpha1_def alpha2_def
|
|
85 |
beta1_def beta2_def gamma1_def gamma2_def
|
|
86 |
|
|
87 |
|
|
88 |
(*** Invariant proof for Psi: "manual" proof proves individual lemmas ***)
|
|
89 |
|
|
90 |
lemma PsiInv_Init: "|- InitPsi --> PsiInv"
|
|
91 |
by (auto simp: InitPsi_def PsiInv_defs)
|
|
92 |
|
|
93 |
lemma PsiInv_alpha1: "|- alpha1 & $PsiInv --> PsiInv$"
|
|
94 |
by (auto simp: alpha1_def PsiInv_defs)
|
|
95 |
|
|
96 |
lemma PsiInv_alpha2: "|- alpha2 & $PsiInv --> PsiInv$"
|
|
97 |
by (auto simp: alpha2_def PsiInv_defs)
|
|
98 |
|
|
99 |
lemma PsiInv_beta1: "|- beta1 & $PsiInv --> PsiInv$"
|
|
100 |
by (auto simp: beta1_def PsiInv_defs)
|
|
101 |
|
|
102 |
lemma PsiInv_beta2: "|- beta2 & $PsiInv --> PsiInv$"
|
|
103 |
by (auto simp: beta2_def PsiInv_defs)
|
|
104 |
|
|
105 |
lemma PsiInv_gamma1: "|- gamma1 & $PsiInv --> PsiInv$"
|
|
106 |
by (auto simp: gamma1_def PsiInv_defs)
|
|
107 |
|
|
108 |
lemma PsiInv_gamma2: "|- gamma2 & $PsiInv --> PsiInv$"
|
|
109 |
by (auto simp: gamma2_def PsiInv_defs)
|
|
110 |
|
|
111 |
lemma PsiInv_stutter: "|- unchanged (x,y,sem,pc1,pc2) & $PsiInv --> PsiInv$"
|
|
112 |
by (auto simp: PsiInv_defs)
|
|
113 |
|
|
114 |
lemma PsiInv: "|- Psi --> []PsiInv"
|
42769
|
115 |
apply (invariant simp: Psi_def)
|
21624
|
116 |
apply (force simp: PsiInv_Init [try_rewrite] Init_def)
|
|
117 |
apply (auto intro: PsiInv_alpha1 [try_rewrite] PsiInv_alpha2 [try_rewrite]
|
|
118 |
PsiInv_beta1 [try_rewrite] PsiInv_beta2 [try_rewrite] PsiInv_gamma1 [try_rewrite]
|
|
119 |
PsiInv_gamma2 [try_rewrite] PsiInv_stutter [try_rewrite]
|
|
120 |
simp add: square_def N1_def N2_def)
|
|
121 |
done
|
|
122 |
|
|
123 |
(* Automatic proof works too, but it make take a while on a slow machine.
|
|
124 |
More realistic examples require user guidance anyway.
|
|
125 |
*)
|
|
126 |
|
|
127 |
lemma "|- Psi --> []PsiInv"
|
42769
|
128 |
by (auto_invariant simp: PsiInv_defs Psi_defs)
|
21624
|
129 |
|
|
130 |
|
|
131 |
(**** Step simulation ****)
|
|
132 |
|
|
133 |
lemma Init_sim: "|- Psi --> Init InitPhi"
|
|
134 |
by (auto simp: InitPhi_def Psi_def InitPsi_def Init_def)
|
|
135 |
|
|
136 |
lemma Step_sim: "|- Psi --> [][M1 | M2]_(x,y)"
|
|
137 |
by (auto simp: square_def M1_def M2_def Psi_defs elim!: STL4E [temp_use])
|
|
138 |
|
|
139 |
|
|
140 |
(**** Proof of fairness ****)
|
|
141 |
|
|
142 |
(*
|
|
143 |
The goal is to prove Fair_M1 far below, which asserts
|
|
144 |
|- Psi --> WF(M1)_(x,y)
|
|
145 |
(the other fairness condition is symmetrical).
|
|
146 |
|
|
147 |
The strategy is to use WF2 (with beta1 as the helpful action). Proving its
|
|
148 |
temporal premise needs two auxiliary lemmas:
|
|
149 |
1. Stuck_at_b: control can only proceed at pc1 = b by executing beta1
|
|
150 |
2. N1_live: the first component will eventually reach b
|
|
151 |
|
|
152 |
Lemma 1 is easy, lemma 2 relies on the invariant, the strong fairness
|
|
153 |
of the semaphore, and needs auxiliary lemmas that ensure that the second
|
|
154 |
component will eventually release the semaphore. Most of the proofs of
|
|
155 |
the auxiliary lemmas are very similar.
|
|
156 |
*)
|
|
157 |
|
|
158 |
lemma Stuck_at_b: "|- [][(N1 | N2) & ~ beta1]_(x,y,sem,pc1,pc2) --> stable(pc1 = #b)"
|
|
159 |
by (auto elim!: Stable squareE simp: Psi_defs)
|
|
160 |
|
|
161 |
lemma N1_enabled_at_g: "|- pc1 = #g --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
|
|
162 |
apply clarsimp
|
|
163 |
apply (rule_tac F = gamma1 in enabled_mono)
|
42785
|
164 |
apply (enabled Inc_base)
|
21624
|
165 |
apply (force simp: gamma1_def)
|
|
166 |
apply (force simp: angle_def gamma1_def N1_def)
|
|
167 |
done
|
|
168 |
|
|
169 |
lemma g1_leadsto_a1:
|
|
170 |
"|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N1)_(x,y,sem,pc1,pc2) & []#True
|
|
171 |
--> (pc1 = #g ~> pc1 = #a)"
|
|
172 |
apply (rule SF1)
|
|
173 |
apply (tactic
|
26342
|
174 |
{* action_simp_tac (@{simpset} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
|
21624
|
175 |
apply (tactic
|
26342
|
176 |
{* action_simp_tac (@{simpset} addsimps @{thm angle_def} :: @{thms Psi_defs}) [] [] 1 *})
|
21624
|
177 |
(* reduce |- []A --> <>Enabled B to |- A --> Enabled B *)
|
|
178 |
apply (auto intro!: InitDmd_gen [temp_use] N1_enabled_at_g [temp_use]
|
|
179 |
dest!: STL2_gen [temp_use] simp: Init_def)
|
|
180 |
done
|
|
181 |
|
|
182 |
(* symmetrical for N2, and similar for beta2 *)
|
|
183 |
lemma N2_enabled_at_g: "|- pc2 = #g --> Enabled (<N2>_(x,y,sem,pc1,pc2))"
|
|
184 |
apply clarsimp
|
|
185 |
apply (rule_tac F = gamma2 in enabled_mono)
|
42785
|
186 |
apply (enabled Inc_base)
|
21624
|
187 |
apply (force simp: gamma2_def)
|
|
188 |
apply (force simp: angle_def gamma2_def N2_def)
|
|
189 |
done
|
|
190 |
|
|
191 |
lemma g2_leadsto_a2:
|
|
192 |
"|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & []#True
|
|
193 |
--> (pc2 = #g ~> pc2 = #a)"
|
|
194 |
apply (rule SF1)
|
26342
|
195 |
apply (tactic {* action_simp_tac (@{simpset} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
|
|
196 |
apply (tactic {* action_simp_tac (@{simpset} addsimps @{thm angle_def} :: @{thms Psi_defs})
|
21624
|
197 |
[] [] 1 *})
|
|
198 |
apply (auto intro!: InitDmd_gen [temp_use] N2_enabled_at_g [temp_use]
|
|
199 |
dest!: STL2_gen [temp_use] simp add: Init_def)
|
|
200 |
done
|
|
201 |
|
|
202 |
lemma N2_enabled_at_b: "|- pc2 = #b --> Enabled (<N2>_(x,y,sem,pc1,pc2))"
|
|
203 |
apply clarsimp
|
|
204 |
apply (rule_tac F = beta2 in enabled_mono)
|
42785
|
205 |
apply (enabled Inc_base)
|
21624
|
206 |
apply (force simp: beta2_def)
|
|
207 |
apply (force simp: angle_def beta2_def N2_def)
|
|
208 |
done
|
|
209 |
|
|
210 |
lemma b2_leadsto_g2:
|
|
211 |
"|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & []#True
|
|
212 |
--> (pc2 = #b ~> pc2 = #g)"
|
|
213 |
apply (rule SF1)
|
|
214 |
apply (tactic
|
26342
|
215 |
{* action_simp_tac (@{simpset} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
|
21624
|
216 |
apply (tactic
|
26342
|
217 |
{* action_simp_tac (@{simpset} addsimps @{thm angle_def} :: @{thms Psi_defs}) [] [] 1 *})
|
21624
|
218 |
apply (auto intro!: InitDmd_gen [temp_use] N2_enabled_at_b [temp_use]
|
|
219 |
dest!: STL2_gen [temp_use] simp: Init_def)
|
|
220 |
done
|
|
221 |
|
|
222 |
(* Combine above lemmas: the second component will eventually reach pc2 = a *)
|
|
223 |
lemma N2_leadsto_a:
|
|
224 |
"|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & []#True
|
|
225 |
--> (pc2 = #a | pc2 = #b | pc2 = #g ~> pc2 = #a)"
|
|
226 |
apply (auto intro!: LatticeDisjunctionIntro [temp_use])
|
|
227 |
apply (rule LatticeReflexivity [temp_use])
|
|
228 |
apply (rule LatticeTransitivity [temp_use])
|
|
229 |
apply (auto intro!: b2_leadsto_g2 [temp_use] g2_leadsto_a2 [temp_use])
|
|
230 |
done
|
|
231 |
|
|
232 |
(* Get rid of disjunction on the left-hand side of ~> above. *)
|
|
233 |
lemma N2_live:
|
|
234 |
"|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2)
|
|
235 |
--> <>(pc2 = #a)"
|
|
236 |
apply (auto simp: Init_defs intro!: N2_leadsto_a [temp_use, THEN [2] leadsto_init [temp_use]])
|
|
237 |
apply (case_tac "pc2 (st1 sigma)")
|
|
238 |
apply auto
|
|
239 |
done
|
|
240 |
|
|
241 |
(* Now prove that the first component will eventually reach pc1 = b from pc1 = a *)
|
|
242 |
|
|
243 |
lemma N1_enabled_at_both_a:
|
|
244 |
"|- pc2 = #a & (PsiInv & pc1 = #a) --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
|
|
245 |
apply clarsimp
|
|
246 |
apply (rule_tac F = alpha1 in enabled_mono)
|
42785
|
247 |
apply (enabled Inc_base)
|
21624
|
248 |
apply (force simp: alpha1_def PsiInv_defs)
|
|
249 |
apply (force simp: angle_def alpha1_def N1_def)
|
|
250 |
done
|
|
251 |
|
|
252 |
lemma a1_leadsto_b1:
|
|
253 |
"|- []($PsiInv & [(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2))
|
|
254 |
& SF(N1)_(x,y,sem,pc1,pc2) & [] SF(N2)_(x,y,sem,pc1,pc2)
|
|
255 |
--> (pc1 = #a ~> pc1 = #b)"
|
|
256 |
apply (rule SF1)
|
26342
|
257 |
apply (tactic {* action_simp_tac (@{simpset} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
|
21624
|
258 |
apply (tactic
|
26342
|
259 |
{* action_simp_tac (@{simpset} addsimps (@{thm angle_def} :: @{thms Psi_defs})) [] [] 1 *})
|
21624
|
260 |
apply (clarsimp intro!: N1_enabled_at_both_a [THEN DmdImpl [temp_use]])
|
|
261 |
apply (auto intro!: BoxDmd2_simple [temp_use] N2_live [temp_use]
|
|
262 |
simp: split_box_conj more_temp_simps)
|
|
263 |
done
|
|
264 |
|
|
265 |
(* Combine the leadsto properties for N1: it will arrive at pc1 = b *)
|
|
266 |
|
|
267 |
lemma N1_leadsto_b: "|- []($PsiInv & [(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2))
|
|
268 |
& SF(N1)_(x,y,sem,pc1,pc2) & [] SF(N2)_(x,y,sem,pc1,pc2)
|
|
269 |
--> (pc1 = #b | pc1 = #g | pc1 = #a ~> pc1 = #b)"
|
|
270 |
apply (auto intro!: LatticeDisjunctionIntro [temp_use])
|
|
271 |
apply (rule LatticeReflexivity [temp_use])
|
|
272 |
apply (rule LatticeTransitivity [temp_use])
|
|
273 |
apply (auto intro!: a1_leadsto_b1 [temp_use] g1_leadsto_a1 [temp_use]
|
|
274 |
simp: split_box_conj)
|
|
275 |
done
|
|
276 |
|
|
277 |
lemma N1_live: "|- []($PsiInv & [(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2))
|
|
278 |
& SF(N1)_(x,y,sem,pc1,pc2) & [] SF(N2)_(x,y,sem,pc1,pc2)
|
|
279 |
--> <>(pc1 = #b)"
|
|
280 |
apply (auto simp: Init_defs intro!: N1_leadsto_b [temp_use, THEN [2] leadsto_init [temp_use]])
|
|
281 |
apply (case_tac "pc1 (st1 sigma)")
|
|
282 |
apply auto
|
|
283 |
done
|
|
284 |
|
|
285 |
lemma N1_enabled_at_b: "|- pc1 = #b --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
|
|
286 |
apply clarsimp
|
|
287 |
apply (rule_tac F = beta1 in enabled_mono)
|
42785
|
288 |
apply (enabled Inc_base)
|
21624
|
289 |
apply (force simp: beta1_def)
|
|
290 |
apply (force simp: angle_def beta1_def N1_def)
|
|
291 |
done
|
|
292 |
|
|
293 |
(* Now assemble the bits and pieces to prove that Psi is fair. *)
|
|
294 |
|
|
295 |
lemma Fair_M1_lemma: "|- []($PsiInv & [(N1 | N2)]_(x,y,sem,pc1,pc2))
|
|
296 |
& SF(N1)_(x,y,sem,pc1,pc2) & []SF(N2)_(x,y,sem,pc1,pc2)
|
|
297 |
--> SF(M1)_(x,y)"
|
|
298 |
apply (rule_tac B = beta1 and P = "PRED pc1 = #b" in SF2)
|
|
299 |
(* action premises *)
|
|
300 |
apply (force simp: angle_def M1_def beta1_def)
|
|
301 |
apply (force simp: angle_def Psi_defs)
|
|
302 |
apply (force elim!: N1_enabled_at_b [temp_use])
|
|
303 |
(* temporal premise: use previous lemmas and simple TL *)
|
|
304 |
apply (force intro!: DmdStable [temp_use] N1_live [temp_use] Stuck_at_b [temp_use]
|
|
305 |
elim: STL4E [temp_use] simp: square_def)
|
|
306 |
done
|
|
307 |
|
|
308 |
lemma Fair_M1: "|- Psi --> WF(M1)_(x,y)"
|
|
309 |
by (auto intro!: SFImplWF [temp_use] Fair_M1_lemma [temp_use] PsiInv [temp_use]
|
|
310 |
simp: Psi_def split_box_conj [temp_use] more_temp_simps)
|
17309
|
311 |
|
3807
|
312 |
end
|