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