author | wenzelm |
Wed, 11 Oct 2017 20:46:38 +0200 | |
changeset 66842 | 7ded55dd2a55 |
parent 66453 | cc19f7ca2ed6 |
child 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
41589 | 1 |
(* Title: HOL/TLA/Inc/Inc.thy |
2 |
Author: Stephan Merz, University of Munich |
|
3807 | 3 |
*) |
4 |
||
60592 | 5 |
section \<open>Lamport's "increment" example\<close> |
17309 | 6 |
|
7 |
theory Inc |
|
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
60592
diff
changeset
|
8 |
imports "HOL-TLA.TLA" |
17309 | 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 *) |
|
60591 | 48 |
InitPhi_def: "InitPhi == PRED x = # 0 \<and> y = # 0" and |
49 |
M1_def: "M1 == ACT x$ = Suc<$x> \<and> y$ = $y" and |
|
50 |
M2_def: "M2 == ACT y$ = Suc<$y> \<and> x$ = $x" and |
|
51 |
Phi_def: "Phi == TEMP Init InitPhi \<and> \<box>[M1 \<or> M2]_(x,y) |
|
52 |
\<and> WF(M1)_(x,y) \<and> WF(M2)_(x,y)" and |
|
3807 | 53 |
|
54 |
(* definitions for low-level program *) |
|
60591 | 55 |
InitPsi_def: "InitPsi == PRED pc1 = #a \<and> pc2 = #a |
56 |
\<and> x = # 0 \<and> y = # 0 \<and> sem = # 1" and |
|
57 |
alpha1_def: "alpha1 == ACT $pc1 = #a \<and> pc1$ = #b \<and> $sem = Suc<sem$> |
|
58 |
\<and> unchanged(x,y,pc2)" and |
|
59 |
alpha2_def: "alpha2 == ACT $pc2 = #a \<and> pc2$ = #b \<and> $sem = Suc<sem$> |
|
60 |
\<and> unchanged(x,y,pc1)" and |
|
61 |
beta1_def: "beta1 == ACT $pc1 = #b \<and> pc1$ = #g \<and> x$ = Suc<$x> |
|
62 |
\<and> unchanged(y,sem,pc2)" and |
|
63 |
beta2_def: "beta2 == ACT $pc2 = #b \<and> pc2$ = #g \<and> y$ = Suc<$y> |
|
64 |
\<and> unchanged(x,sem,pc1)" and |
|
65 |
gamma1_def: "gamma1 == ACT $pc1 = #g \<and> pc1$ = #a \<and> sem$ = Suc<$sem> |
|
66 |
\<and> unchanged(x,y,pc2)" and |
|
67 |
gamma2_def: "gamma2 == ACT $pc2 = #g \<and> pc2$ = #a \<and> sem$ = Suc<$sem> |
|
68 |
\<and> unchanged(x,y,pc1)" and |
|
69 |
N1_def: "N1 == ACT (alpha1 \<or> beta1 \<or> gamma1)" and |
|
70 |
N2_def: "N2 == ACT (alpha2 \<or> beta2 \<or> gamma2)" and |
|
17309 | 71 |
Psi_def: "Psi == TEMP Init InitPsi |
60591 | 72 |
\<and> \<box>[N1 \<or> N2]_(x,y,sem,pc1,pc2) |
73 |
\<and> SF(N1)_(x,y,sem,pc1,pc2) |
|
74 |
\<and> SF(N2)_(x,y,sem,pc1,pc2)" and |
|
3807 | 75 |
|
60591 | 76 |
PsiInv1_def: "PsiInv1 == PRED sem = # 1 \<and> pc1 = #a \<and> pc2 = #a" and |
77 |
PsiInv2_def: "PsiInv2 == PRED sem = # 0 \<and> pc1 = #a \<and> (pc2 = #b \<or> pc2 = #g)" and |
|
78 |
PsiInv3_def: "PsiInv3 == PRED sem = # 0 \<and> pc2 = #a \<and> (pc1 = #b \<or> pc1 = #g)" and |
|
79 |
PsiInv_def: "PsiInv == PRED (PsiInv1 \<or> PsiInv2 \<or> PsiInv3)" |
|
17309 | 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 |
||
60591 | 92 |
lemma PsiInv_alpha1: "\<turnstile> alpha1 \<and> $PsiInv \<longrightarrow> PsiInv$" |
21624 | 93 |
by (auto simp: alpha1_def PsiInv_defs) |
94 |
||
60591 | 95 |
lemma PsiInv_alpha2: "\<turnstile> alpha2 \<and> $PsiInv \<longrightarrow> PsiInv$" |
21624 | 96 |
by (auto simp: alpha2_def PsiInv_defs) |
97 |
||
60591 | 98 |
lemma PsiInv_beta1: "\<turnstile> beta1 \<and> $PsiInv \<longrightarrow> PsiInv$" |
21624 | 99 |
by (auto simp: beta1_def PsiInv_defs) |
100 |
||
60591 | 101 |
lemma PsiInv_beta2: "\<turnstile> beta2 \<and> $PsiInv \<longrightarrow> PsiInv$" |
21624 | 102 |
by (auto simp: beta2_def PsiInv_defs) |
103 |
||
60591 | 104 |
lemma PsiInv_gamma1: "\<turnstile> gamma1 \<and> $PsiInv \<longrightarrow> PsiInv$" |
21624 | 105 |
by (auto simp: gamma1_def PsiInv_defs) |
106 |
||
60591 | 107 |
lemma PsiInv_gamma2: "\<turnstile> gamma2 \<and> $PsiInv \<longrightarrow> PsiInv$" |
21624 | 108 |
by (auto simp: gamma2_def PsiInv_defs) |
109 |
||
60591 | 110 |
lemma PsiInv_stutter: "\<turnstile> unchanged (x,y,sem,pc1,pc2) \<and> $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 |
||
60591 | 135 |
lemma Step_sim: "\<turnstile> Psi \<longrightarrow> \<box>[M1 \<or> 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 |
||
60591 | 157 |
lemma Stuck_at_b: "\<turnstile> \<box>[(N1 \<or> N2) \<and> \<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: |
|
60591 | 169 |
"\<turnstile> \<box>[(N1 \<or> N2) \<and> \<not>beta1]_(x,y,sem,pc1,pc2) \<and> SF(N1)_(x,y,sem,pc1,pc2) \<and> \<box>#True |
60588 | 170 |
\<longrightarrow> (pc1 = #g \<leadsto> pc1 = #a)" |
21624 | 171 |
apply (rule SF1) |
172 |
apply (tactic |
|
60592 | 173 |
\<open>action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1\<close>) |
21624 | 174 |
apply (tactic |
60592 | 175 |
\<open>action_simp_tac (@{context} addsimps @{thm angle_def} :: @{thms Psi_defs}) [] [] 1\<close>) |
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: |
|
60591 | 191 |
"\<turnstile> \<box>[(N1 \<or> N2) \<and> \<not>beta1]_(x,y,sem,pc1,pc2) \<and> SF(N2)_(x,y,sem,pc1,pc2) \<and> \<box>#True |
60588 | 192 |
\<longrightarrow> (pc2 = #g \<leadsto> pc2 = #a)" |
21624 | 193 |
apply (rule SF1) |
60592 | 194 |
apply (tactic \<open>action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1\<close>) |
195 |
apply (tactic \<open>action_simp_tac (@{context} addsimps @{thm angle_def} :: @{thms Psi_defs}) |
|
196 |
[] [] 1\<close>) |
|
21624 | 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: |
|
60591 | 210 |
"\<turnstile> \<box>[(N1 \<or> N2) \<and> \<not>beta1]_(x,y,sem,pc1,pc2) \<and> SF(N2)_(x,y,sem,pc1,pc2) \<and> \<box>#True |
60588 | 211 |
\<longrightarrow> (pc2 = #b \<leadsto> pc2 = #g)" |
21624 | 212 |
apply (rule SF1) |
213 |
apply (tactic |
|
60592 | 214 |
\<open>action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1\<close>) |
21624 | 215 |
apply (tactic |
60592 | 216 |
\<open>action_simp_tac (@{context} addsimps @{thm angle_def} :: @{thms Psi_defs}) [] [] 1\<close>) |
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: |
|
60591 | 223 |
"\<turnstile> \<box>[(N1 \<or> N2) \<and> \<not>beta1]_(x,y,sem,pc1,pc2) \<and> SF(N2)_(x,y,sem,pc1,pc2) \<and> \<box>#True |
224 |
\<longrightarrow> (pc2 = #a \<or> pc2 = #b \<or> 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: |
60591 | 233 |
"\<turnstile> \<box>[(N1 \<or> N2) \<and> \<not>beta1]_(x,y,sem,pc1,pc2) \<and> SF(N2)_(x,y,sem,pc1,pc2) |
60588 | 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: |
|
60591 | 243 |
"\<turnstile> pc2 = #a \<and> (PsiInv \<and> 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: |
|
60591 | 252 |
"\<turnstile> \<box>($PsiInv \<and> [(N1 \<or> N2) \<and> \<not>beta1]_(x,y,sem,pc1,pc2)) |
253 |
\<and> SF(N1)_(x,y,sem,pc1,pc2) \<and> \<box> SF(N2)_(x,y,sem,pc1,pc2) |
|
60588 | 254 |
\<longrightarrow> (pc1 = #a \<leadsto> pc1 = #b)" |
21624 | 255 |
apply (rule SF1) |
60592 | 256 |
apply (tactic \<open>action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1\<close>) |
21624 | 257 |
apply (tactic |
60592 | 258 |
\<open>action_simp_tac (@{context} addsimps (@{thm angle_def} :: @{thms Psi_defs})) [] [] 1\<close>) |
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 |
||
60591 | 266 |
lemma N1_leadsto_b: "\<turnstile> \<box>($PsiInv \<and> [(N1 \<or> N2) \<and> \<not>beta1]_(x,y,sem,pc1,pc2)) |
267 |
\<and> SF(N1)_(x,y,sem,pc1,pc2) \<and> \<box> SF(N2)_(x,y,sem,pc1,pc2) |
|
268 |
\<longrightarrow> (pc1 = #b \<or> pc1 = #g \<or> 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 |
||
60591 | 276 |
lemma N1_live: "\<turnstile> \<box>($PsiInv \<and> [(N1 \<or> N2) \<and> \<not>beta1]_(x,y,sem,pc1,pc2)) |
277 |
\<and> SF(N1)_(x,y,sem,pc1,pc2) \<and> \<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 |
||
60591 | 294 |
lemma Fair_M1_lemma: "\<turnstile> \<box>($PsiInv \<and> [(N1 \<or> N2)]_(x,y,sem,pc1,pc2)) |
295 |
\<and> SF(N1)_(x,y,sem,pc1,pc2) \<and> \<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 |