[f01853]: thys / TLA / Liveness.thy  Maximize  Restore  History

Download this file

412 lines (358 with data), 25.4 kB

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
(* Title: A Definitional Encoding of TLA in Isabelle/HOL
Authors: Gudmund Grov <ggrov at inf.ed.ac.uk>
Stephan Merz <Stephan.Merz at loria.fr>
Year: 2011
Maintainer: Gudmund Grov <ggrov at inf.ed.ac.uk>
*)
header "Liveness"
theory Liveness
imports Rules
begin
text{* This theory derives proof rules for liveness properties.*}
definition enabled :: "'a formula \<Rightarrow> 'a formula"
where "enabled F \<equiv> \<lambda> s. \<exists> t. ((first s) ## t) \<Turnstile> F"
syntax "_Enabled" :: "lift \<Rightarrow> lift" ("(Enabled _)" [90] 90)
translations "_Enabled" \<rightleftharpoons> "CONST enabled"
definition WeakF :: "('a::world) formula \<Rightarrow> ('a,'b) stfun \<Rightarrow> 'a formula"
where "WeakF F v \<equiv> TEMP \<diamond>\<box>Enabled \<langle>F\<rangle>_v \<longrightarrow> \<box>\<diamond>\<langle>F\<rangle>_v"
definition StrongF :: "('a::world) formula \<Rightarrow> ('a,'b) stfun \<Rightarrow> 'a formula"
where "StrongF F v \<equiv> TEMP \<box>\<diamond>Enabled \<langle>F\<rangle>_v \<longrightarrow> \<box>\<diamond>\<langle>F\<rangle>_v"
text{*
Lamport's TLA defines the above notions for actions.
In \tlastar{}, (pre-)formulas generalise TLA's actions and the above
definition is the natural generalisation of enabledness to pre-formulas.
In particular, we have chosen to define @{text enabled} such that it
yields itself a temporal formula, although its value really just depends
on the first state of the sequence it is evaluated over.
Then, the definitions of weak and strong fairness are exactly as in TLA.
*}
syntax
"_WF" :: "[lift,lift] \<Rightarrow> lift" ("(WF'(_')'_(_))" [20,1000] 90)
"_SF" :: "[lift,lift] \<Rightarrow> lift" ("(SF'(_')'_(_))" [20,1000] 90)
"_WFsp" :: "[lift,lift] \<Rightarrow> lift" ("(WF '(_')'_(_))" [20,1000] 90)
"_SFsp" :: "[lift,lift] \<Rightarrow> lift" ("(SF '(_')'_(_))" [20,1000] 90)
translations
"_WF" \<rightleftharpoons> "CONST WeakF"
"_SF" \<rightleftharpoons> "CONST StrongF"
"_WFsp" \<rightharpoonup> "CONST WeakF"
"_SFsp" \<rightharpoonup> "CONST StrongF"
subsection "Properties of @{term enabled}"
theorem enabledI: "\<turnstile> F \<longrightarrow> Enabled F"
proof (clarsimp)
fix w
assume "w \<Turnstile> F"
with seq_app_first_tail[of w] have "((first w) ## tail w) \<Turnstile> F" by simp
thus "w \<Turnstile> Enabled F" by (auto simp: enabled_def)
qed
theorem enabledE:
assumes "s \<Turnstile> Enabled F" and "\<And>u. (first s ## u) \<Turnstile> F \<Longrightarrow> Q"
shows "Q"
using assms unfolding enabled_def by blast
lemma enabled_mono:
assumes "w \<Turnstile> Enabled F" and "\<turnstile> F \<longrightarrow> G"
shows "w \<Turnstile> Enabled G"
using assms[unlifted] unfolding enabled_def by blast
lemma Enabled_disj1: "\<turnstile> Enabled F \<longrightarrow> Enabled (F \<or> G)"
by (auto simp: enabled_def)
lemma Enabled_disj2: "\<turnstile> Enabled F \<longrightarrow> Enabled (G \<or> F)"
by (auto simp: enabled_def)
lemma Enabled_conj1: "\<turnstile> Enabled (F \<and> G) \<longrightarrow> Enabled F"
by (auto simp: enabled_def)
lemma Enabled_conj2: "\<turnstile> Enabled (G \<and> F) \<longrightarrow> Enabled F"
by (auto simp: enabled_def)
lemma Enabled_disjD: "\<turnstile> Enabled (F \<or> G) \<longrightarrow> Enabled F \<or> Enabled G"
by (auto simp: enabled_def)
lemma Enabled_disj: "\<turnstile> Enabled (F \<or> G) = (Enabled F \<or> Enabled G)"
by (auto simp: enabled_def)
lemmas enabled_disj_rew = Enabled_disj[int_rewrite]
lemma Enabled_ex: "\<turnstile> Enabled (\<exists> x. F x) = (\<exists> x. Enabled (F x))"
by (force simp: enabled_def)
subsection "Fairness Properties"
lemma WF_alt: "\<turnstile> WF(A)_v = (\<box>\<diamond>\<not>Enabled \<langle>A\<rangle>_v \<or> \<box>\<diamond>\<langle>A\<rangle>_v)"
proof -
have "\<turnstile> WF(A)_v = (\<not>\<diamond>\<box> Enabled \<langle>A\<rangle>_v \<or> \<box>\<diamond>\<langle>A\<rangle>_v)" by (auto simp: WeakF_def)
thus ?thesis by (simp add: dualization_rew)
qed
lemma SF_alt: "\<turnstile> SF(A)_v = (\<diamond>\<box>\<not>Enabled \<langle>A\<rangle>_v \<or> \<box>\<diamond>\<langle>A\<rangle>_v)"
proof -
have "\<turnstile> SF(A)_v = (\<not>\<box>\<diamond> Enabled \<langle>A\<rangle>_v \<or> \<box>\<diamond>\<langle>A\<rangle>_v)" by (auto simp: StrongF_def)
thus ?thesis by (simp add: dualization_rew)
qed
lemma alwaysWFI: "\<turnstile> WF(A)_v \<longrightarrow> \<box>WF(A)_v"
unfolding WF_alt[int_rewrite] by (rule MM6)
theorem WF_always[simp_unl]: "\<turnstile> \<box>WF(A)_v = WF(A)_v"
by (rule int_iffI[OF ax1 alwaysWFI])
theorem WF_eventually[simp_unl]: "\<turnstile> \<diamond>WF(A)_v = WF(A)_v"
proof -
have 1: "\<turnstile> \<not>WF(A)_v = (\<diamond>\<box>Enabled \<langle>A\<rangle>_v \<and> \<not> \<box>\<diamond>\<langle>A\<rangle>_v)"
by (auto simp: WeakF_def)
have "\<turnstile> \<box>\<not>WF(A)_v = \<not>WF(A)_v"
by (simp add: 1[int_rewrite] STL5[int_rewrite] dualization_rew)
thus ?thesis
by (auto simp: eventually_def)
qed
lemma alwaysSFI: "\<turnstile> SF(A)_v \<longrightarrow> \<box>SF(A)_v"
proof -
have "\<turnstile> \<box>\<diamond>\<box>\<not>Enabled \<langle>A\<rangle>_v \<or> \<box>\<diamond>\<langle>A\<rangle>_v \<longrightarrow> \<box>(\<box>\<diamond>\<box>\<not>Enabled \<langle>A\<rangle>_v \<or> \<box>\<diamond>\<langle>A\<rangle>_v)"
by (rule MM6)
thus ?thesis unfolding SF_alt[int_rewrite] by simp
qed
theorem SF_always[simp_unl]: "\<turnstile> \<box>SF(A)_v = SF(A)_v"
by (rule int_iffI[OF ax1 alwaysSFI])
theorem SF_eventually[simp_unl]: "\<turnstile> \<diamond>SF(A)_v = SF(A)_v"
proof -
have 1: "\<turnstile> \<not>SF(A)_v = (\<box>\<diamond>Enabled \<langle>A\<rangle>_v \<and> \<not> \<box>\<diamond>\<langle>A\<rangle>_v)"
by (auto simp: StrongF_def)
have "\<turnstile> \<box>\<not>SF(A)_v = \<not>SF(A)_v"
by (simp add: 1[int_rewrite] STL5[int_rewrite] dualization_rew)
thus ?thesis
by (auto simp: eventually_def)
qed
theorem SF_imp_WF: "\<turnstile> SF (A)_v \<longrightarrow> WF (A)_v"
unfolding WeakF_def StrongF_def by (auto dest: E20[unlift_rule])
lemma enabled_WFSF: "\<turnstile> \<box>Enabled \<langle>F\<rangle>_v \<longrightarrow> (WF(F)_v = SF(F)_v)"
proof -
have "\<turnstile> \<box>Enabled \<langle>F\<rangle>_v \<longrightarrow> \<diamond>\<box>Enabled \<langle>F\<rangle>_v" by (rule E3)
hence "\<turnstile> \<box>Enabled \<langle>F\<rangle>_v \<longrightarrow> WF(F)_v \<longrightarrow> SF(F)_v" by (auto simp: WeakF_def StrongF_def)
moreover
have "\<turnstile> \<box>Enabled \<langle>F\<rangle>_v \<longrightarrow> \<box>\<diamond>Enabled \<langle>F\<rangle>_v" by (rule STL4[OF E3])
hence "\<turnstile> \<box>Enabled \<langle>F\<rangle>_v \<longrightarrow> SF(F)_v \<longrightarrow> WF(F)_v" by (auto simp: WeakF_def StrongF_def)
ultimately show ?thesis by force
qed
theorem WF1_general:
assumes h1: "|~ P \<and> N \<longrightarrow> \<circ>P \<or> \<circ>Q"
and h2: "|~ P \<and> N \<and> \<langle>A\<rangle>_v \<longrightarrow> \<circ>Q"
and h3: "\<turnstile> P \<and> N \<longrightarrow> Enabled \<langle>A\<rangle>_v"
and h4: "|~ P \<and> Unchanged w \<longrightarrow> \<circ>P"
shows "\<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> (P \<leadsto> Q)"
proof -
have "\<turnstile> \<box>(\<box>N \<and> WF(A)_v) \<longrightarrow> \<box>(\<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v)"
proof (rule STL4)
have "\<turnstile> \<box>(P \<and> N) \<longrightarrow> \<diamond>\<box>Enabled \<langle>A\<rangle>_v" by (rule lift_imp_trans[OF h3[THEN STL4] E3])
hence "\<turnstile> \<box>P \<and> \<box>N \<and> WF(A)_v \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_v" by (auto simp: WeakF_def STL5[int_rewrite])
with ax1[of "TEMP \<diamond>\<langle>A\<rangle>_v"] show "\<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> \<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v" by force
qed
hence "\<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> \<box>(\<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v)"
by (simp add: STL5[int_rewrite])
with AA22[OF h1 h2 h4] show ?thesis by force
qed
text {* Lamport's version of the rule is derived as a special case. *}
theorem WF1:
assumes h1: "|~ P \<and> [N]_v \<longrightarrow> \<circ>P \<or> \<circ>Q"
and h2: "|~ P \<and> \<langle>N \<and> A\<rangle>_v \<longrightarrow> \<circ>Q"
and h3: "\<turnstile> P \<longrightarrow> Enabled \<langle>A\<rangle>_v"
and h4: "|~ P \<and> Unchanged v \<longrightarrow> \<circ>P"
shows "\<turnstile> \<box>[N]_v \<and> WF(A)_v \<longrightarrow> (P \<leadsto> Q)"
proof -
have "\<turnstile> \<box>\<box>[N]_v \<and> WF(A)_v \<longrightarrow> (P \<leadsto> Q)"
proof (rule WF1_general)
from h1 T9[of N v] show "|~ P \<and> \<box>[N]_v \<longrightarrow> \<circ>P \<or> \<circ>Q" by force
next
from T9[of N v] have "|~ P \<and> \<box>[N]_v \<and> \<langle>A\<rangle>_v \<longrightarrow> P \<and> \<langle>N \<and> A\<rangle>_v"
by (auto simp: actrans_def angle_actrans_def)
from this h2 show "|~ P \<and> \<box>[N]_v \<and> \<langle>A\<rangle>_v \<longrightarrow> \<circ>Q" by (rule pref_imp_trans)
next
from h3 T9[of N v] show "\<turnstile> P \<and> \<box>[N]_v \<longrightarrow> Enabled \<langle>A\<rangle>_v" by force
qed (rule h4)
thus ?thesis by simp
qed
text {*
The corresponding rule for strong fairness has an additional hypothesis
@{text "\<box>F"}, which is typically a conjunction of other fairness properties
used to prove that the helpful action eventually becomes enabled.
*}
theorem SF1_general:
assumes h1: "|~ P \<and> N \<longrightarrow> \<circ>P \<or> \<circ>Q"
and h2: "|~ P \<and> N \<and> \<langle>A\<rangle>_v \<longrightarrow> \<circ>Q"
and h3: "\<turnstile> \<box>P \<and> \<box>N \<and> \<box>F \<longrightarrow> \<diamond>Enabled \<langle>A\<rangle>_v"
and h4: "|~ P \<and> Unchanged w \<longrightarrow> \<circ>P"
shows "\<turnstile> \<box>N \<and> SF(A)_v \<and> \<box>F \<longrightarrow> (P \<leadsto> Q)"
proof -
have "\<turnstile> \<box>(\<box>N \<and> SF(A)_v \<and> \<box>F) \<longrightarrow> \<box>(\<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v)"
proof (rule STL4)
have "\<turnstile> \<box>(\<box>P \<and> \<box>N \<and> \<box>F) \<longrightarrow> \<box>\<diamond>Enabled \<langle>A\<rangle>_v" by (rule STL4[OF h3])
hence "\<turnstile> \<box>P \<and> \<box>N \<and> \<box>F \<and> SF(A)_v \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_v" by (auto simp: StrongF_def STL5[int_rewrite])
with ax1[of "TEMP \<diamond>\<langle>A\<rangle>_v"] show "\<turnstile> \<box>N \<and> SF(A)_v \<and> \<box>F \<longrightarrow> \<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v" by force
qed
hence "\<turnstile> \<box>N \<and> SF(A)_v \<and> \<box>F \<longrightarrow> \<box>(\<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v)"
by (simp add: STL5[int_rewrite])
with AA22[OF h1 h2 h4] show ?thesis by force
qed
theorem SF1:
assumes h1: "|~ P \<and> [N]_v \<longrightarrow> \<circ>P \<or> \<circ>Q"
and h2: "|~ P \<and> \<langle>N \<and> A\<rangle>_v \<longrightarrow> \<circ>Q"
and h3: "\<turnstile> \<box>P \<and> \<box>[N]_v \<and> \<box>F \<longrightarrow> \<diamond>Enabled \<langle>A\<rangle>_v"
and h4: "|~ P \<and> Unchanged v \<longrightarrow> \<circ>P"
shows "\<turnstile> \<box>[N]_v \<and> SF(A)_v \<and> \<box>F \<longrightarrow> (P \<leadsto> Q)"
proof -
have "\<turnstile> \<box>\<box>[N]_v \<and> SF(A)_v \<and> \<box>F \<longrightarrow> (P \<leadsto> Q)"
proof (rule SF1_general)
from h1 T9[of N v] show "|~ P \<and> \<box>[N]_v \<longrightarrow> \<circ>P \<or> \<circ>Q" by force
next
from T9[of N v] have "|~ P \<and> \<box>[N]_v \<and> \<langle>A\<rangle>_v \<longrightarrow> P \<and> \<langle>N \<and> A\<rangle>_v"
by (auto simp: actrans_def angle_actrans_def)
from this h2 show "|~ P \<and> \<box>[N]_v \<and> \<langle>A\<rangle>_v \<longrightarrow> \<circ>Q" by (rule pref_imp_trans)
next
from h3 show "\<turnstile> \<box>P \<and> \<box>\<box>[N]_v \<and> \<box>F \<longrightarrow> \<diamond>Enabled \<langle>A\<rangle>_v" by simp
qed (rule h4)
thus ?thesis by simp
qed
text {*
Lamport proposes the following rule as an introduction rule for @{text WF} formulas.
*}
theorem WF2:
assumes h1: "|~ \<langle>N \<and> B\<rangle>_f \<longrightarrow> \<langle>M\<rangle>_g"
and h2: "|~ P \<and> \<circ>P \<and> \<langle>N \<and> A\<rangle>_f \<longrightarrow> B"
and h3: "\<turnstile> P \<and> Enabled \<langle>M\<rangle>_g \<longrightarrow> Enabled \<langle>A\<rangle>_f"
and h4: "\<turnstile> \<box>[N \<and> \<not>B]_f \<and> WF(A)_f \<and> \<box>F \<and> \<diamond>\<box>Enabled \<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P"
shows "\<turnstile> \<box>[N]_f \<and> WF(A)_f \<and> \<box>F \<longrightarrow> WF(M)_g"
proof -
have "\<turnstile> \<box>[N]_f \<and> WF(A)_f \<and> \<box>F \<and> \<diamond>\<box>Enabled \<langle>M\<rangle>_g \<and> \<not>\<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g"
proof -
have 1: "\<turnstile> \<box>[N]_f \<and> WF(A)_f \<and> \<box>F \<and> \<diamond>\<box>Enabled \<langle>M\<rangle>_g \<and> \<not>\<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P"
proof -
have A: "\<turnstile> \<box>[N]_f \<and> WF(A)_f \<and> \<box>F \<and> \<diamond>\<box>Enabled \<langle>M\<rangle>_g \<and> \<not>\<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow>
\<box>(\<box>[N]_f \<and> WF(A)_f \<and> \<box>F) \<and> \<diamond>\<box>(\<diamond>\<box>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not>M]_g)"
unfolding STL6[int_rewrite] (* important to do this before STL5 is applied *)
by (auto simp: STL5[int_rewrite] dualization_rew)
have B: "\<turnstile> \<box>(\<box>[N]_f \<and> WF(A)_f \<and> \<box>F) \<and> \<diamond>\<box>(\<diamond>\<box>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not>M]_g) \<longrightarrow>
\<diamond>((\<box>[N]_f \<and> WF(A)_f \<and> \<box>F) \<and> \<box>(\<diamond>\<box>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not>M]_g))"
by (rule SE2)
from lift_imp_trans[OF A B]
have "\<turnstile> \<box>[N]_f \<and> WF(A)_f \<and> \<box>F \<and> \<diamond>\<box>Enabled \<langle>M\<rangle>_g \<and> \<not>\<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow>
\<diamond>((\<box>[N]_f \<and> WF(A)_f \<and> \<box>F) \<and> (\<diamond>\<box>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not>M]_g))"
by (simp add: STL5[int_rewrite])
moreover
from h1 have "|~ [N]_f \<longrightarrow> [\<not>M]_g \<longrightarrow> [N \<and> \<not>B]_f" by (auto simp: actrans_def angle_actrans_def)
hence "\<turnstile> \<box>[[N]_f]_f \<longrightarrow> \<box>[[\<not>M]_g \<longrightarrow> [N \<and> \<not>B]_f]_f" by (rule M2)
from lift_imp_trans[OF this ax4] have "\<turnstile> \<box>[N]_f \<and> \<box>[\<not>M]_g \<longrightarrow> \<box>[N \<and> \<not>B]_f"
by (force intro: T4[unlift_rule])
with h4 have "\<turnstile> (\<box>[N]_f \<and> WF(A)_f \<and> \<box>F) \<and> (\<diamond>\<box>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not>M]_g) \<longrightarrow> \<diamond>\<box>P"
by force
from STL4_eve[OF this]
have "\<turnstile> \<diamond>((\<box>[N]_f \<and> WF(A)_f \<and> \<box>F) \<and> (\<diamond>\<box>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not>M]_g)) \<longrightarrow> \<diamond>\<box>P" by simp
ultimately
show ?thesis by (rule lift_imp_trans)
qed
have 2: "\<turnstile> \<box>[N]_f \<and> WF(A)_f \<and> \<diamond>\<box>Enabled \<langle>M\<rangle>_g \<and> \<diamond>\<box>P \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g"
proof -
have A: "\<turnstile> \<diamond>\<box>P \<and> \<diamond>\<box>Enabled \<langle>M\<rangle>_g \<and> WF(A)_f \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_f"
using h3[THEN STL4, THEN STL4_eve] by (auto simp: STL6[int_rewrite] WeakF_def)
have B: "\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g"
proof -
from M1[of P f] have "\<turnstile> \<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circ>P) \<and> (N \<and> A)\<rangle>_f"
by (force intro: AA29[unlift_rule])
hence "\<turnstile> \<diamond>\<box>(\<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f) \<longrightarrow> \<diamond>\<box>\<box>\<diamond>\<langle>(P \<and> \<circ>P) \<and> (N \<and> A)\<rangle>_f"
by (rule STL4_eve[OF STL4])
hence "\<turnstile> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circ>P) \<and> (N \<and> A)\<rangle>_f"
by (simp add: STL6[int_rewrite])
with AA29[of N f A]
have B1: "\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circ>P) \<and> (N \<and> A)\<rangle>_f" by force
from h2 have "|~ \<langle>(P \<and> \<circ>P) \<and> (N \<and> A)\<rangle>_f \<longrightarrow> \<langle>N \<and> B\<rangle>_f"
by (auto simp: angle_actrans_sem[unlifted])
from B1 this[THEN AA25, THEN STL4] have "\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>N \<and> B\<rangle>_f"
by (rule lift_imp_trans)
moreover
have "\<turnstile> \<box>\<diamond>\<langle>N \<and> B\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g" by (rule h1[THEN AA25, THEN STL4])
ultimately show ?thesis by (rule lift_imp_trans)
qed
from A B show ?thesis by force
qed
from 1 2 show ?thesis by force
qed
thus ?thesis by (auto simp: WeakF_def)
qed
text {*
Lamport proposes an analogous theorem for introducing strong fairness, and its
proof is very similar, in fact, it was obtained by copy and paste, with minimal
modifications.
*}
theorem SF2:
assumes h1: "|~ \<langle>N \<and> B\<rangle>_f \<longrightarrow> \<langle>M\<rangle>_g"
and h2: "|~ P \<and> \<circ>P \<and> \<langle>N \<and> A\<rangle>_f \<longrightarrow> B"
and h3: "\<turnstile> P \<and> Enabled \<langle>M\<rangle>_g \<longrightarrow> Enabled \<langle>A\<rangle>_f"
and h4: "\<turnstile> \<box>[N \<and> \<not>B]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P"
shows "\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<longrightarrow> SF(M)_g"
proof -
have "\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not>\<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g"
proof -
have 1: "\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not>\<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P"
proof -
have A: "\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not>\<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow>
\<box>(\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<diamond>\<box>(\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not>M]_g)"
unfolding STL6[int_rewrite] (* important to do this before STL5 is applied *)
by (auto simp: STL5[int_rewrite] dualization_rew)
have B: "\<turnstile> \<box>(\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<diamond>\<box>(\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not>M]_g) \<longrightarrow>
\<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>(\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not>M]_g))"
by (rule SE2)
from lift_imp_trans[OF A B]
have "\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not>\<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow>
\<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> (\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not>M]_g))"
by (simp add: STL5[int_rewrite])
moreover
from h1 have "|~ [N]_f \<longrightarrow> [\<not>M]_g \<longrightarrow> [N \<and> \<not>B]_f" by (auto simp: actrans_def angle_actrans_def)
hence "\<turnstile> \<box>[[N]_f]_f \<longrightarrow> \<box>[[\<not>M]_g \<longrightarrow> [N \<and> \<not>B]_f]_f" by (rule M2)
from lift_imp_trans[OF this ax4] have "\<turnstile> \<box>[N]_f \<and> \<box>[\<not>M]_g \<longrightarrow> \<box>[N \<and> \<not>B]_f"
by (force intro: T4[unlift_rule])
with h4 have "\<turnstile> (\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> (\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not>M]_g) \<longrightarrow> \<diamond>\<box>P"
by force
from STL4_eve[OF this]
have "\<turnstile> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> (\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not>M]_g)) \<longrightarrow> \<diamond>\<box>P" by simp
ultimately
show ?thesis by (rule lift_imp_trans)
qed
have 2: "\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<diamond>\<box>P \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g"
proof -
have "\<turnstile> \<box>\<diamond>(P \<and> Enabled \<langle>M\<rangle>_g) \<and> SF(A)_f \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_f"
using h3[THEN STL4_eve, THEN STL4] by (auto simp: StrongF_def)
with E28 have A: "\<turnstile> \<diamond>\<box>P \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> SF(A)_f \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_f"
by force
have B: "\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g"
proof -
from M1[of P f] have "\<turnstile> \<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circ>P) \<and> (N \<and> A)\<rangle>_f"
by (force intro: AA29[unlift_rule])
hence "\<turnstile> \<diamond>\<box>(\<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f) \<longrightarrow> \<diamond>\<box>\<box>\<diamond>\<langle>(P \<and> \<circ>P) \<and> (N \<and> A)\<rangle>_f"
by (rule STL4_eve[OF STL4])
hence "\<turnstile> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circ>P) \<and> (N \<and> A)\<rangle>_f"
by (simp add: STL6[int_rewrite])
with AA29[of N f A]
have B1: "\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circ>P) \<and> (N \<and> A)\<rangle>_f" by force
from h2 have "|~ \<langle>(P \<and> \<circ>P) \<and> (N \<and> A)\<rangle>_f \<longrightarrow> \<langle>N \<and> B\<rangle>_f"
by (auto simp: angle_actrans_sem[unlifted])
from B1 this[THEN AA25, THEN STL4] have "\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>N \<and> B\<rangle>_f"
by (rule lift_imp_trans)
moreover
have "\<turnstile> \<box>\<diamond>\<langle>N \<and> B\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g" by (rule h1[THEN AA25, THEN STL4])
ultimately show ?thesis by (rule lift_imp_trans)
qed
from A B show ?thesis by force
qed
from 1 2 show ?thesis by force
qed
thus ?thesis by (auto simp: StrongF_def)
qed
text {* This is the lattice rule from TLA *}
theorem wf_leadsto:
assumes h1: "wf r"
and h2: "\<And>x. \<turnstile> F x \<leadsto> (G \<or> (\<exists>y. #((y,x) \<in> r) \<and> F y))"
shows "\<turnstile> F x \<leadsto> G"
using h1
proof (rule wf_induct)
fix x
assume ih: "\<forall>y. (y, x) \<in> r \<longrightarrow> (\<turnstile> F y \<leadsto> G)"
show "\<turnstile> F x \<leadsto> G"
proof -
from ih have "\<turnstile> (\<exists>y. #((y,x) \<in> r) \<and> F y) \<leadsto> G"
by (force simp: LT21[int_rewrite] LT33[int_rewrite])
with h2 show ?thesis by (force intro: LT19[unlift_rule])
qed
qed
subsection "Stuttering Invariance"
theorem stut_Enabled: "STUTINV Enabled \<langle>F\<rangle>_v"
by (auto simp: enabled_def stutinv_def dest!: sim_first)
theorem stut_WF: "NSTUTINV F \<Longrightarrow> STUTINV WF(F)_v"
by (auto simp: WeakF_def stut_Enabled bothstutinvs)
theorem stut_SF: "NSTUTINV F \<Longrightarrow> STUTINV SF(F)_v"
by (auto simp: StrongF_def stut_Enabled bothstutinvs)
lemmas livestutinv = stut_WF stut_SF stut_Enabled
end

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:





No, thanks