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