author | wenzelm |
Fri, 26 Jun 2015 14:53:15 +0200 | |
changeset 60588 | 750c533459b1 |
parent 60587 | 0318b43ee95c |
child 60591 | e0b77517f9a9 |
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 |
|
60587 | 51 |
Phi_def: "Phi == TEMP Init InitPhi & \<box>[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 |
60587 | 72 |
& \<box>[N1 | N2]_(x,y,sem,pc1,pc2) |
6255 | 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 |
||
60588 | 89 |
lemma PsiInv_Init: "\<turnstile> InitPsi \<longrightarrow> PsiInv" |
21624 | 90 |
by (auto simp: InitPsi_def PsiInv_defs) |
91 |
||
60588 | 92 |
lemma PsiInv_alpha1: "\<turnstile> alpha1 & $PsiInv \<longrightarrow> PsiInv$" |
21624 | 93 |
by (auto simp: alpha1_def PsiInv_defs) |
94 |
||
60588 | 95 |
lemma PsiInv_alpha2: "\<turnstile> alpha2 & $PsiInv \<longrightarrow> PsiInv$" |
21624 | 96 |
by (auto simp: alpha2_def PsiInv_defs) |
97 |
||
60588 | 98 |
lemma PsiInv_beta1: "\<turnstile> beta1 & $PsiInv \<longrightarrow> PsiInv$" |
21624 | 99 |
by (auto simp: beta1_def PsiInv_defs) |
100 |
||
60588 | 101 |
lemma PsiInv_beta2: "\<turnstile> beta2 & $PsiInv \<longrightarrow> PsiInv$" |
21624 | 102 |
by (auto simp: beta2_def PsiInv_defs) |
103 |
||
60588 | 104 |
lemma PsiInv_gamma1: "\<turnstile> gamma1 & $PsiInv \<longrightarrow> PsiInv$" |
21624 | 105 |
by (auto simp: gamma1_def PsiInv_defs) |
106 |
||
60588 | 107 |
lemma PsiInv_gamma2: "\<turnstile> gamma2 & $PsiInv \<longrightarrow> PsiInv$" |
21624 | 108 |
by (auto simp: gamma2_def PsiInv_defs) |
109 |
||
60588 | 110 |
lemma PsiInv_stutter: "\<turnstile> unchanged (x,y,sem,pc1,pc2) & $PsiInv \<longrightarrow> PsiInv$" |
21624 | 111 |
by (auto simp: PsiInv_defs) |
112 |
||
60588 | 113 |
lemma PsiInv: "\<turnstile> Psi \<longrightarrow> \<box>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 |
||
60588 | 126 |
lemma "\<turnstile> Psi \<longrightarrow> \<box>PsiInv" |
42769 | 127 |
by (auto_invariant simp: PsiInv_defs Psi_defs) |
21624 | 128 |
|
129 |
||
130 |
(**** Step simulation ****) |
|
131 |
||
60588 | 132 |
lemma Init_sim: "\<turnstile> Psi \<longrightarrow> Init InitPhi" |
21624 | 133 |
by (auto simp: InitPhi_def Psi_def InitPsi_def Init_def) |
134 |
||
60588 | 135 |
lemma Step_sim: "\<turnstile> Psi \<longrightarrow> \<box>[M1 | M2]_(x,y)" |
21624 | 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 |
|
60588 | 143 |
\<turnstile> Psi \<longrightarrow> WF(M1)_(x,y) |
21624 | 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 |
||
60588 | 157 |
lemma Stuck_at_b: "\<turnstile> \<box>[(N1 | N2) & \<not> beta1]_(x,y,sem,pc1,pc2) \<longrightarrow> stable(pc1 = #b)" |
21624 | 158 |
by (auto elim!: Stable squareE simp: Psi_defs) |
159 |
||
60588 | 160 |
lemma N1_enabled_at_g: "\<turnstile> pc1 = #g \<longrightarrow> Enabled (<N1>_(x,y,sem,pc1,pc2))" |
21624 | 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: |
|
60588 | 169 |
"\<turnstile> \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N1)_(x,y,sem,pc1,pc2) & \<box>#True |
170 |
\<longrightarrow> (pc1 = #g \<leadsto> pc1 = #a)" |
|
21624 | 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 *}) |
60588 | 176 |
(* reduce \<turnstile> \<box>A \<longrightarrow> \<diamond>Enabled B to \<turnstile> A \<longrightarrow> Enabled B *) |
21624 | 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 *) |
|
60588 | 182 |
lemma N2_enabled_at_g: "\<turnstile> pc2 = #g \<longrightarrow> Enabled (<N2>_(x,y,sem,pc1,pc2))" |
21624 | 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: |
|
60588 | 191 |
"\<turnstile> \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & \<box>#True |
192 |
\<longrightarrow> (pc2 = #g \<leadsto> pc2 = #a)" |
|
21624 | 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 |
||
60588 | 201 |
lemma N2_enabled_at_b: "\<turnstile> pc2 = #b \<longrightarrow> Enabled (<N2>_(x,y,sem,pc1,pc2))" |
21624 | 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: |
|
60588 | 210 |
"\<turnstile> \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & \<box>#True |
211 |
\<longrightarrow> (pc2 = #b \<leadsto> pc2 = #g)" |
|
21624 | 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: |
|
60588 | 223 |
"\<turnstile> \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & \<box>#True |
224 |
\<longrightarrow> (pc2 = #a | pc2 = #b | pc2 = #g \<leadsto> pc2 = #a)" |
|
21624 | 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 |
||
60587 | 231 |
(* Get rid of disjunction on the left-hand side of \<leadsto> above. *) |
21624 | 232 |
lemma N2_live: |
60588 | 233 |
"\<turnstile> \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) |
234 |
\<longrightarrow> \<diamond>(pc2 = #a)" |
|
21624 | 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: |
|
60588 | 243 |
"\<turnstile> pc2 = #a & (PsiInv & pc1 = #a) \<longrightarrow> Enabled (<N1>_(x,y,sem,pc1,pc2))" |
21624 | 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: |
|
60588 | 252 |
"\<turnstile> \<box>($PsiInv & [(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2)) |
60587 | 253 |
& SF(N1)_(x,y,sem,pc1,pc2) & \<box> SF(N2)_(x,y,sem,pc1,pc2) |
60588 | 254 |
\<longrightarrow> (pc1 = #a \<leadsto> pc1 = #b)" |
21624 | 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 |
||
60588 | 266 |
lemma N1_leadsto_b: "\<turnstile> \<box>($PsiInv & [(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2)) |
60587 | 267 |
& SF(N1)_(x,y,sem,pc1,pc2) & \<box> SF(N2)_(x,y,sem,pc1,pc2) |
60588 | 268 |
\<longrightarrow> (pc1 = #b | pc1 = #g | pc1 = #a \<leadsto> pc1 = #b)" |
21624 | 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 |
||
60588 | 276 |
lemma N1_live: "\<turnstile> \<box>($PsiInv & [(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2)) |
60587 | 277 |
& SF(N1)_(x,y,sem,pc1,pc2) & \<box> SF(N2)_(x,y,sem,pc1,pc2) |
60588 | 278 |
\<longrightarrow> \<diamond>(pc1 = #b)" |
21624 | 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 |
||
60588 | 284 |
lemma N1_enabled_at_b: "\<turnstile> pc1 = #b \<longrightarrow> Enabled (<N1>_(x,y,sem,pc1,pc2))" |
21624 | 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 |
||
60588 | 294 |
lemma Fair_M1_lemma: "\<turnstile> \<box>($PsiInv & [(N1 | N2)]_(x,y,sem,pc1,pc2)) |
60587 | 295 |
& SF(N1)_(x,y,sem,pc1,pc2) & \<box>SF(N2)_(x,y,sem,pc1,pc2) |
60588 | 296 |
\<longrightarrow> SF(M1)_(x,y)" |
21624 | 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 |
||
60588 | 307 |
lemma Fair_M1: "\<turnstile> Psi \<longrightarrow> WF(M1)_(x,y)" |
21624 | 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 |