author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45605  a89b4bc311a5 
child 47968  3119ad2b5ad3 
permissions  rwrr 
35108  1 
(* Title: HOL/TLA/TLA.thy 
2 
Author: Stephan Merz 

3 
Copyright: 1998 University of Munich 

21624  4 
*) 
3807  5 

21624  6 
header {* The temporal level of TLA *} 
3807  7 

17309  8 
theory TLA 
9 
imports Init 

10 
begin 

3807  11 

12 
consts 

6255  13 
(** abstract syntax **) 
17309  14 
Box :: "('w::world) form => temporal" 
15 
Dmd :: "('w::world) form => temporal" 

16 
leadsto :: "['w::world form, 'v::world form] => temporal" 

17 
Stable :: "stpred => temporal" 

18 
WF :: "[action, 'a stfun] => temporal" 

19 
SF :: "[action, 'a stfun] => temporal" 

3807  20 

21 
(* Quantification over (flexible) state variables *) 

17309  22 
EEx :: "('a stfun => temporal) => temporal" (binder "Eex " 10) 
23 
AAll :: "('a stfun => temporal) => temporal" (binder "Aall " 10) 

6255  24 

25 
(** concrete syntax **) 

26 
syntax 

17309  27 
"_Box" :: "lift => lift" ("([]_)" [40] 40) 
28 
"_Dmd" :: "lift => lift" ("(<>_)" [40] 40) 

29 
"_leadsto" :: "[lift,lift] => lift" ("(_ ~> _)" [23,22] 22) 

30 
"_stable" :: "lift => lift" ("(stable/ _)") 

31 
"_WF" :: "[lift,lift] => lift" ("(WF'(_')'_(_))" [0,60] 55) 

32 
"_SF" :: "[lift,lift] => lift" ("(SF'(_')'_(_))" [0,60] 55) 

6255  33 

17309  34 
"_EEx" :: "[idts, lift] => lift" ("(3EEX _./ _)" [0,10] 10) 
35 
"_AAll" :: "[idts, lift] => lift" ("(3AALL _./ _)" [0,10] 10) 

3807  36 

37 
translations 

35068  38 
"_Box" == "CONST Box" 
39 
"_Dmd" == "CONST Dmd" 

40 
"_leadsto" == "CONST leadsto" 

41 
"_stable" == "CONST Stable" 

42 
"_WF" == "CONST WF" 

43 
"_SF" == "CONST SF" 

6255  44 
"_EEx v A" == "Eex v. A" 
45 
"_AAll v A" == "Aall v. A" 

46 

47 
"sigma = []F" <= "_Box F sigma" 

48 
"sigma = <>F" <= "_Dmd F sigma" 

49 
"sigma = F ~> G" <= "_leadsto F G sigma" 

50 
"sigma = stable P" <= "_stable P sigma" 

51 
"sigma = WF(A)_v" <= "_WF A v sigma" 

52 
"sigma = SF(A)_v" <= "_SF A v sigma" 

53 
"sigma = EEX x. F" <= "_EEx x F sigma" 

54 
"sigma = AALL x. F" <= "_AAll x F sigma" 

3807  55 

12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
9517
diff
changeset

56 
syntax (xsymbols) 
17309  57 
"_Box" :: "lift => lift" ("(\<box>_)" [40] 40) 
58 
"_Dmd" :: "lift => lift" ("(\<diamond>_)" [40] 40) 

59 
"_leadsto" :: "[lift,lift] => lift" ("(_ \<leadsto> _)" [23,22] 22) 

60 
"_EEx" :: "[idts, lift] => lift" ("(3\<exists>\<exists> _./ _)" [0,10] 10) 

61 
"_AAll" :: "[idts, lift] => lift" ("(3\<forall>\<forall> _./ _)" [0,10] 10) 

3808  62 

14565  63 
syntax (HTML output) 
17309  64 
"_EEx" :: "[idts, lift] => lift" ("(3\<exists>\<exists> _./ _)" [0,10] 10) 
65 
"_AAll" :: "[idts, lift] => lift" ("(3\<forall>\<forall> _./ _)" [0,10] 10) 

14565  66 

17309  67 
axioms 
6255  68 
(* Definitions of derived operators *) 
17309  69 
dmd_def: "TEMP <>F == TEMP ~[]~F" 
70 
boxInit: "TEMP []F == TEMP []Init F" 

71 
leadsto_def: "TEMP F ~> G == TEMP [](Init F > <>G)" 

72 
stable_def: "TEMP stable P == TEMP []($P > P$)" 

73 
WF_def: "TEMP WF(A)_v == TEMP <>[] Enabled(<A>_v) > []<><A>_v" 

74 
SF_def: "TEMP SF(A)_v == TEMP []<> Enabled(<A>_v) > []<><A>_v" 

75 
aall_def: "TEMP (AALL x. F x) == TEMP ~ (EEX x. ~ F x)" 

3807  76 

6255  77 
(* Base axioms for raw TLA. *) 
17309  78 
normalT: " [](F > G) > ([]F > []G)" (* polymorphic *) 
79 
reflT: " []F > F" (* F::temporal *) 

80 
transT: " []F > [][]F" (* polymorphic *) 

81 
linT: " <>F & <>G > (<>(F & <>G))  (<>(G & <>F))" 

82 
discT: " [](F > <>(~F & <>F)) > (F > []<>F)" 

83 
primeI: " []P > Init P`" 

84 
primeE: " [](Init P > []F) > Init P` > (F > []F)" 

85 
indT: " [](Init P & ~[]F > Init P` & F) > Init P > []F" 

86 
allT: " (ALL x. [](F x)) = ([](ALL x. F x))" 

3807  87 

17309  88 
necT: " F ==>  []F" (* polymorphic *) 
3807  89 

90 
(* Flexible quantification: refinement mappings, history variables *) 

17309  91 
eexI: " F x > (EEX x. F x)" 
92 
eexE: "[ sigma = (EEX x. F x); basevars vs; 

93 
(!!x. [ basevars (x, vs); sigma = F x ] ==> (G sigma)::bool) 

94 
] ==> G sigma" 

95 
history: " EEX h. Init(h = ha) & [](!x. $h = #x > h` = hb x)" 

96 

21624  97 

98 
(* Specialize intensional introduction/elimination rules for temporal formulas *) 

99 

100 
lemma tempI: "(!!sigma. sigma = (F::temporal)) ==>  F" 

101 
apply (rule intI) 

102 
apply (erule meta_spec) 

103 
done 

104 

105 
lemma tempD: " (F::temporal) ==> sigma = F" 

106 
by (erule intD) 

107 

108 

109 
(* ======== Functions to "unlift" temporal theorems ====== *) 

110 

111 
ML {* 

112 
(* The following functions are specialized versions of the corresponding 

113 
functions defined in theory Intensional in that they introduce a 

114 
"world" parameter of type "behavior". 

115 
*) 

116 
fun temp_unlift th = 

26305  117 
(rewrite_rule @{thms action_rews} (th RS @{thm tempD})) handle THM _ => action_unlift th; 
21624  118 

119 
(* Turn  F = G into metalevel rewrite rule F == G *) 

120 
val temp_rewrite = int_rewrite 

121 

122 
fun temp_use th = 

123 
case (concl_of th) of 

26305  124 
Const _ $ (Const (@{const_name Intensional.Valid}, _) $ _) => 
21624  125 
((flatten (temp_unlift th)) handle THM _ => th) 
126 
 _ => th; 

127 

128 
fun try_rewrite th = temp_rewrite th handle THM _ => temp_use th; 

129 
*} 

130 

42814  131 
attribute_setup temp_unlift = {* Scan.succeed (Thm.rule_attribute (K temp_unlift)) *} 
132 
attribute_setup temp_rewrite = {* Scan.succeed (Thm.rule_attribute (K temp_rewrite)) *} 

133 
attribute_setup temp_use = {* Scan.succeed (Thm.rule_attribute (K temp_use)) *} 

134 
attribute_setup try_rewrite = {* Scan.succeed (Thm.rule_attribute (K try_rewrite)) *} 

30528  135 

21624  136 

137 
(* Update classical reasonerwill be updated once more below! *) 

138 

139 
declare tempI [intro!] 

140 
declare tempD [dest] 

141 

142 
(* Modify the functions that add rules to simpsets, classical sets, 

143 
and clasimpsets in order to accept "lifted" theorems 

144 
*) 

145 

146 
(*  *) 

147 
(*** "Simple temporal logic": only [] and <> ***) 

148 
(*  *) 

149 
section "Simple temporal logic" 

150 

151 
(* []~F == []~Init F *) 

45605  152 
lemmas boxNotInit = boxInit [of "LIFT ~F", unfolded Init_simps] for F 
21624  153 

154 
lemma dmdInit: "TEMP <>F == TEMP <> Init F" 

155 
apply (unfold dmd_def) 

156 
apply (unfold boxInit [of "LIFT ~F"]) 

157 
apply (simp (no_asm) add: Init_simps) 

158 
done 

159 

45605  160 
lemmas dmdNotInit = dmdInit [of "LIFT ~F", unfolded Init_simps] for F 
21624  161 

162 
(* boxInit and dmdInit cannot be used as rewrites, because they loop. 

163 
Nonlooping instances for state predicates and actions are occasionally useful. 

164 
*) 

45605  165 
lemmas boxInit_stp = boxInit [where 'a = state] 
166 
lemmas boxInit_act = boxInit [where 'a = "state * state"] 

167 
lemmas dmdInit_stp = dmdInit [where 'a = state] 

168 
lemmas dmdInit_act = dmdInit [where 'a = "state * state"] 

21624  169 

170 
(* The symmetric equations can be used to get rid of Init *) 

171 
lemmas boxInitD = boxInit [symmetric] 

172 
lemmas dmdInitD = dmdInit [symmetric] 

173 
lemmas boxNotInitD = boxNotInit [symmetric] 

174 
lemmas dmdNotInitD = dmdNotInit [symmetric] 

175 

176 
lemmas Init_simps = Init_simps boxInitD dmdInitD boxNotInitD dmdNotInitD 

177 

178 
(*  STL2  *) 

179 
lemmas STL2 = reflT 

180 

181 
(* The "polymorphic" (generic) variant *) 

182 
lemma STL2_gen: " []F > Init F" 

183 
apply (unfold boxInit [of F]) 

184 
apply (rule STL2) 

185 
done 

186 

187 
(* see also STL2_pr below: " []P > Init P & Init (P`)" *) 

188 

189 

190 
(* Dual versions for <> *) 

191 
lemma InitDmd: " F > <> F" 

192 
apply (unfold dmd_def) 

193 
apply (auto dest!: STL2 [temp_use]) 

194 
done 

195 

196 
lemma InitDmd_gen: " Init F > <>F" 

197 
apply clarsimp 

198 
apply (drule InitDmd [temp_use]) 

199 
apply (simp add: dmdInitD) 

200 
done 

201 

202 

203 
(*  STL3  *) 

204 
lemma STL3: " ([][]F) = ([]F)" 

205 
by (auto elim: transT [temp_use] STL2 [temp_use]) 

206 

207 
(* corresponding elimination rule introduces double boxes: 

208 
[ (sigma = []F); (sigma = [][]F) ==> PROP W ] ==> PROP W 

209 
*) 

210 
lemmas dup_boxE = STL3 [temp_unlift, THEN iffD2, elim_format] 

45605  211 
lemmas dup_boxD = STL3 [temp_unlift, THEN iffD1] 
21624  212 

213 
(* dual versions for <> *) 

214 
lemma DmdDmd: " (<><>F) = (<>F)" 

215 
by (auto simp add: dmd_def [try_rewrite] STL3 [try_rewrite]) 

216 

217 
lemmas dup_dmdE = DmdDmd [temp_unlift, THEN iffD2, elim_format] 

45605  218 
lemmas dup_dmdD = DmdDmd [temp_unlift, THEN iffD1] 
21624  219 

220 

221 
(*  STL4  *) 

222 
lemma STL4: 

223 
assumes " F > G" 

224 
shows " []F > []G" 

225 
apply clarsimp 

226 
apply (rule normalT [temp_use]) 

227 
apply (rule assms [THEN necT, temp_use]) 

228 
apply assumption 

229 
done 

230 

231 
(* Unlifted version as an elimination rule *) 

232 
lemma STL4E: "[ sigma = []F;  F > G ] ==> sigma = []G" 

233 
by (erule (1) STL4 [temp_use]) 

234 

235 
lemma STL4_gen: " Init F > Init G ==>  []F > []G" 

236 
apply (drule STL4) 

237 
apply (simp add: boxInitD) 

238 
done 

239 

240 
lemma STL4E_gen: "[ sigma = []F;  Init F > Init G ] ==> sigma = []G" 

241 
by (erule (1) STL4_gen [temp_use]) 

242 

243 
(* see also STL4Edup below, which allows an auxiliary boxed formula: 

244 
[]A /\ F => G 

245 
 

246 
[]A /\ []F => []G 

247 
*) 

248 

249 
(* The dual versions for <> *) 

250 
lemma DmdImpl: 

251 
assumes prem: " F > G" 

252 
shows " <>F > <>G" 

253 
apply (unfold dmd_def) 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
42814
diff
changeset

254 
apply (fastforce intro!: prem [temp_use] elim!: STL4E [temp_use]) 
21624  255 
done 
256 

257 
lemma DmdImplE: "[ sigma = <>F;  F > G ] ==> sigma = <>G" 

258 
by (erule (1) DmdImpl [temp_use]) 

259 

260 
(*  STL5  *) 

261 
lemma STL5: " ([]F & []G) = ([](F & G))" 

262 
apply auto 

263 
apply (subgoal_tac "sigma = [] (G > (F & G))") 

264 
apply (erule normalT [temp_use]) 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
42814
diff
changeset

265 
apply (fastforce elim!: STL4E [temp_use])+ 
21624  266 
done 
267 

268 
(* rewrite rule to split conjunctions under boxes *) 

45605  269 
lemmas split_box_conj = STL5 [temp_unlift, symmetric] 
21624  270 

271 

272 
(* the corresponding elimination rule allows to combine boxes in the hypotheses 

273 
(NB: F and G must have the same type, i.e., both actions or temporals.) 

274 
Use "addSE2" etc. if you want to add this to a claset, otherwise it will loop! 

275 
*) 

276 
lemma box_conjE: 

277 
assumes "sigma = []F" 

278 
and "sigma = []G" 

279 
and "sigma = [](F&G) ==> PROP R" 

280 
shows "PROP R" 

281 
by (rule assms STL5 [temp_unlift, THEN iffD1] conjI)+ 

282 

283 
(* Instances of box_conjE for state predicates, actions, and temporals 

284 
in case the general rule is "too polymorphic". 

285 
*) 

45605  286 
lemmas box_conjE_temp = box_conjE [where 'a = behavior] 
287 
lemmas box_conjE_stp = box_conjE [where 'a = state] 

288 
lemmas box_conjE_act = box_conjE [where 'a = "state * state"] 

21624  289 

290 
(* Define a tactic that tries to merge all boxes in an antecedent. The definition is 

291 
a bit kludgy in order to simulate "double elimresolution". 

292 
*) 

293 

294 
lemma box_thin: "[ sigma = []F; PROP W ] ==> PROP W" . 

295 

296 
ML {* 

297 
fun merge_box_tac i = 

26305  298 
REPEAT_DETERM (EVERY [etac @{thm box_conjE} i, atac i, etac @{thm box_thin} i]) 
21624  299 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26305
diff
changeset

300 
fun merge_temp_box_tac ctxt i = 
26305  301 
REPEAT_DETERM (EVERY [etac @{thm box_conjE_temp} i, atac i, 
27239  302 
eres_inst_tac ctxt [(("'a", 0), "behavior")] @{thm box_thin} i]) 
21624  303 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26305
diff
changeset

304 
fun merge_stp_box_tac ctxt i = 
26305  305 
REPEAT_DETERM (EVERY [etac @{thm box_conjE_stp} i, atac i, 
27239  306 
eres_inst_tac ctxt [(("'a", 0), "state")] @{thm box_thin} i]) 
21624  307 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26305
diff
changeset

308 
fun merge_act_box_tac ctxt i = 
26305  309 
REPEAT_DETERM (EVERY [etac @{thm box_conjE_act} i, atac i, 
27239  310 
eres_inst_tac ctxt [(("'a", 0), "state * state")] @{thm box_thin} i]) 
21624  311 
*} 
312 

42814  313 
method_setup merge_box = {* Scan.succeed (K (SIMPLE_METHOD' merge_box_tac)) *} 
314 
method_setup merge_temp_box = {* Scan.succeed (SIMPLE_METHOD' o merge_temp_box_tac) *} 

315 
method_setup merge_stp_box = {* Scan.succeed (SIMPLE_METHOD' o merge_stp_box_tac) *} 

316 
method_setup merge_act_box = {* Scan.succeed (SIMPLE_METHOD' o merge_act_box_tac) *} 

42787  317 

21624  318 
(* rewrite rule to push universal quantification through box: 
319 
(sigma = [](! x. F x)) = (! x. (sigma = []F x)) 

320 
*) 

45605  321 
lemmas all_box = allT [temp_unlift, symmetric] 
21624  322 

323 
lemma DmdOr: " (<>(F  G)) = (<>F  <>G)" 

324 
apply (auto simp add: dmd_def split_box_conj [try_rewrite]) 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
42814
diff
changeset

325 
apply (erule contrapos_np, merge_box, fastforce elim!: STL4E [temp_use])+ 
21624  326 
done 
327 

328 
lemma exT: " (EX x. <>(F x)) = (<>(EX x. F x))" 

329 
by (auto simp: dmd_def Not_Rex [try_rewrite] all_box [try_rewrite]) 

330 

45605  331 
lemmas ex_dmd = exT [temp_unlift, symmetric] 
21624  332 

333 
lemma STL4Edup: "!!sigma. [ sigma = []A; sigma = []F;  F & []A > G ] ==> sigma = []G" 

334 
apply (erule dup_boxE) 

42787  335 
apply merge_box 
21624  336 
apply (erule STL4E) 
337 
apply assumption 

338 
done 

339 

340 
lemma DmdImpl2: 

341 
"!!sigma. [ sigma = <>F; sigma = [](F > G) ] ==> sigma = <>G" 

342 
apply (unfold dmd_def) 

343 
apply auto 

344 
apply (erule notE) 

42787  345 
apply merge_box 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
42814
diff
changeset

346 
apply (fastforce elim!: STL4E [temp_use]) 
21624  347 
done 
348 

349 
lemma InfImpl: 

350 
assumes 1: "sigma = []<>F" 

351 
and 2: "sigma = []G" 

352 
and 3: " F & G > H" 

353 
shows "sigma = []<>H" 

354 
apply (insert 1 2) 

355 
apply (erule_tac F = G in dup_boxE) 

42787  356 
apply merge_box 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
42814
diff
changeset

357 
apply (fastforce elim!: STL4E [temp_use] DmdImpl2 [temp_use] intro!: 3 [temp_use]) 
21624  358 
done 
359 

360 
(*  STL6  *) 

361 
(* Used in the proof of STL6, but useful in itself. *) 

362 
lemma BoxDmd: " []F & <>G > <>([]F & G)" 

363 
apply (unfold dmd_def) 

364 
apply clarsimp 

365 
apply (erule dup_boxE) 

42787  366 
apply merge_box 
21624  367 
apply (erule contrapos_np) 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
42814
diff
changeset

368 
apply (fastforce elim!: STL4E [temp_use]) 
21624  369 
done 
370 

371 
(* weaker than BoxDmd, but more polymorphic (and often just right) *) 

372 
lemma BoxDmd_simple: " []F & <>G > <>(F & G)" 

373 
apply (unfold dmd_def) 

374 
apply clarsimp 

42787  375 
apply merge_box 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
42814
diff
changeset

376 
apply (fastforce elim!: notE STL4E [temp_use]) 
21624  377 
done 
378 

379 
lemma BoxDmd2_simple: " []F & <>G > <>(G & F)" 

380 
apply (unfold dmd_def) 

381 
apply clarsimp 

42787  382 
apply merge_box 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
42814
diff
changeset

383 
apply (fastforce elim!: notE STL4E [temp_use]) 
21624  384 
done 
385 

386 
lemma DmdImpldup: 

387 
assumes 1: "sigma = []A" 

388 
and 2: "sigma = <>F" 

389 
and 3: " []A & F > G" 

390 
shows "sigma = <>G" 

391 
apply (rule 2 [THEN 1 [THEN BoxDmd [temp_use]], THEN DmdImplE]) 

392 
apply (rule 3) 

393 
done 

394 

395 
lemma STL6: " <>[]F & <>[]G > <>[](F & G)" 

396 
apply (auto simp: STL5 [temp_rewrite, symmetric]) 

397 
apply (drule linT [temp_use]) 

398 
apply assumption 

399 
apply (erule thin_rl) 

400 
apply (rule DmdDmd [temp_unlift, THEN iffD1]) 

401 
apply (erule disjE) 

402 
apply (erule DmdImplE) 

403 
apply (rule BoxDmd) 

404 
apply (erule DmdImplE) 

405 
apply auto 

406 
apply (drule BoxDmd [temp_use]) 

407 
apply assumption 

408 
apply (erule thin_rl) 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
42814
diff
changeset

409 
apply (fastforce elim!: DmdImplE [temp_use]) 
21624  410 
done 
411 

412 

413 
(*  True / False  *) 

414 
section "Simplification of constants" 

415 

416 
lemma BoxConst: " ([]#P) = #P" 

417 
apply (rule tempI) 

418 
apply (cases P) 

419 
apply (auto intro!: necT [temp_use] dest: STL2_gen [temp_use] simp: Init_simps) 

420 
done 

421 

422 
lemma DmdConst: " (<>#P) = #P" 

423 
apply (unfold dmd_def) 

424 
apply (cases P) 

425 
apply (simp_all add: BoxConst [try_rewrite]) 

426 
done 

427 

428 
lemmas temp_simps [temp_rewrite, simp] = BoxConst DmdConst 

429 

430 

431 
(*  Further rewrites  *) 

432 
section "Further rewrites" 

433 

434 
lemma NotBox: " (~[]F) = (<>~F)" 

435 
by (simp add: dmd_def) 

436 

437 
lemma NotDmd: " (~<>F) = ([]~F)" 

438 
by (simp add: dmd_def) 

439 

440 
(* These are not declared by default, because they could be harmful, 

441 
e.g. []F & ~[]F becomes []F & <>~F !! *) 

26305  442 
lemmas more_temp_simps1 = 
21624  443 
STL3 [temp_rewrite] DmdDmd [temp_rewrite] NotBox [temp_rewrite] NotDmd [temp_rewrite] 
444 
NotBox [temp_unlift, THEN eq_reflection] 

445 
NotDmd [temp_unlift, THEN eq_reflection] 

446 

447 
lemma BoxDmdBox: " ([]<>[]F) = (<>[]F)" 

448 
apply (auto dest!: STL2 [temp_use]) 

449 
apply (rule ccontr) 

450 
apply (subgoal_tac "sigma = <>[][]F & <>[]~[]F") 

451 
apply (erule thin_rl) 

452 
apply auto 

453 
apply (drule STL6 [temp_use]) 

454 
apply assumption 

455 
apply simp 

26305  456 
apply (simp_all add: more_temp_simps1) 
21624  457 
done 
458 

459 
lemma DmdBoxDmd: " (<>[]<>F) = ([]<>F)" 

460 
apply (unfold dmd_def) 

461 
apply (auto simp: BoxDmdBox [unfolded dmd_def, try_rewrite]) 

462 
done 

463 

26305  464 
lemmas more_temp_simps2 = more_temp_simps1 BoxDmdBox [temp_rewrite] DmdBoxDmd [temp_rewrite] 
21624  465 

466 

467 
(*  Miscellaneous  *) 

468 

469 
lemma BoxOr: "!!sigma. [ sigma = []F  []G ] ==> sigma = [](F  G)" 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
42814
diff
changeset

470 
by (fastforce elim!: STL4E [temp_use]) 
21624  471 

472 
(* "persistently implies infinitely often" *) 

473 
lemma DBImplBD: " <>[]F > []<>F" 

474 
apply clarsimp 

475 
apply (rule ccontr) 

26305  476 
apply (simp add: more_temp_simps2) 
21624  477 
apply (drule STL6 [temp_use]) 
478 
apply assumption 

479 
apply simp 

480 
done 

481 

482 
lemma BoxDmdDmdBox: " []<>F & <>[]G > []<>(F & G)" 

483 
apply clarsimp 

484 
apply (rule ccontr) 

26305  485 
apply (unfold more_temp_simps2) 
21624  486 
apply (drule STL6 [temp_use]) 
487 
apply assumption 

488 
apply (subgoal_tac "sigma = <>[]~F") 

489 
apply (force simp: dmd_def) 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
42814
diff
changeset

490 
apply (fastforce elim: DmdImplE [temp_use] STL4E [temp_use]) 
21624  491 
done 
492 

493 

494 
(*  *) 

495 
(*** TLAspecific theorems: primed formulas ***) 

496 
(*  *) 

497 
section "priming" 

498 

499 
(*  TLA2  *) 

500 
lemma STL2_pr: " []P > Init P & Init P`" 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
42814
diff
changeset

501 
by (fastforce intro!: STL2_gen [temp_use] primeI [temp_use]) 
21624  502 

503 
(* Auxiliary lemma allows priming of boxed actions *) 

504 
lemma BoxPrime: " []P > []($P & P$)" 

505 
apply clarsimp 

506 
apply (erule dup_boxE) 

507 
apply (unfold boxInit_act) 

508 
apply (erule STL4E) 

509 
apply (auto simp: Init_simps dest!: STL2_pr [temp_use]) 

510 
done 

511 

512 
lemma TLA2: 

513 
assumes " $P & P$ > A" 

514 
shows " []P > []A" 

515 
apply clarsimp 

516 
apply (drule BoxPrime [temp_use]) 

41529  517 
apply (auto simp: Init_stp_act_rev [try_rewrite] intro!: assms [temp_use] 
21624  518 
elim!: STL4E [temp_use]) 
519 
done 

520 

521 
lemma TLA2E: "[ sigma = []P;  $P & P$ > A ] ==> sigma = []A" 

522 
by (erule (1) TLA2 [temp_use]) 

523 

524 
lemma DmdPrime: " (<>P`) > (<>P)" 

525 
apply (unfold dmd_def) 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
42814
diff
changeset

526 
apply (fastforce elim!: TLA2E [temp_use]) 
21624  527 
done 
528 

45605  529 
lemmas PrimeDmd = InitDmd_gen [temp_use, THEN DmdPrime [temp_use]] 
21624  530 

531 
(*  INV1, stable  *) 

532 
section "stable, invariant" 

533 

534 
lemma ind_rule: 

535 
"[ sigma = []H; sigma = Init P;  H > (Init P & ~[]F > Init(P`) & F) ] 

536 
==> sigma = []F" 

537 
apply (rule indT [temp_use]) 

538 
apply (erule (2) STL4E) 

539 
done 

540 

541 
lemma box_stp_act: " ([]$P) = ([]P)" 

542 
by (simp add: boxInit_act Init_simps) 

543 

45605  544 
lemmas box_stp_actI = box_stp_act [temp_use, THEN iffD2] 
545 
lemmas box_stp_actD = box_stp_act [temp_use, THEN iffD1] 

21624  546 

26305  547 
lemmas more_temp_simps3 = box_stp_act [temp_rewrite] more_temp_simps2 
21624  548 

549 
lemma INV1: 

550 
" (Init P) > (stable P) > []P" 

551 
apply (unfold stable_def boxInit_stp boxInit_act) 

552 
apply clarsimp 

553 
apply (erule ind_rule) 

554 
apply (auto simp: Init_simps elim: ind_rule) 

555 
done 

556 

557 
lemma StableT: 

558 
"!!P.  $P & A > P` ==>  []A > stable P" 

559 
apply (unfold stable_def) 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
42814
diff
changeset

560 
apply (fastforce elim!: STL4E [temp_use]) 
21624  561 
done 
562 

563 
lemma Stable: "[ sigma = []A;  $P & A > P` ] ==> sigma = stable P" 

564 
by (erule (1) StableT [temp_use]) 

565 

566 
(* Generalization of INV1 *) 

567 
lemma StableBox: " (stable P) > [](Init P > []P)" 

568 
apply (unfold stable_def) 

569 
apply clarsimp 

570 
apply (erule dup_boxE) 

571 
apply (force simp: stable_def elim: STL4E [temp_use] INV1 [temp_use]) 

572 
done 

573 

574 
lemma DmdStable: " (stable P) & <>P > <>[]P" 

575 
apply clarsimp 

576 
apply (rule DmdImpl2) 

577 
prefer 2 

578 
apply (erule StableBox [temp_use]) 

579 
apply (simp add: dmdInitD) 

580 
done 

581 

582 
(*  (Semi)automatic invariant tactics  *) 

583 

584 
ML {* 

585 
(* inv_tac reduces goals of the form ... ==> sigma = []P *) 

42793  586 
fun inv_tac ctxt = 
587 
SELECT_GOAL 

588 
(EVERY 

589 
[auto_tac ctxt, 

590 
TRY (merge_box_tac 1), 

591 
rtac (temp_use @{thm INV1}) 1, (* fail if the goal is not a box *) 

592 
TRYALL (etac @{thm Stable})]); 

21624  593 

594 
(* auto_inv_tac applies inv_tac and then tries to attack the subgoals 

595 
in simple cases it may be able to handle goals like  MyProg > []Inv. 

596 
In these simple cases the simplifier seems to be more useful than the 

597 
autotactic, which applies too much propositional logic and simplifies 

598 
too late. 

599 
*) 

42803  600 
fun auto_inv_tac ctxt = 
42793  601 
SELECT_GOAL 
42803  602 
(inv_tac ctxt 1 THEN 
42793  603 
(TRYALL (action_simp_tac 
42803  604 
(simpset_of ctxt addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}]))); 
21624  605 
*} 
606 

42769  607 
method_setup invariant = {* 
42793  608 
Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o inv_tac)) 
42814  609 
*} 
42769  610 

611 
method_setup auto_invariant = {* 

42803  612 
Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o auto_inv_tac)) 
42814  613 
*} 
42769  614 

21624  615 
lemma unless: " []($P > P`  Q`) > (stable P)  <>Q" 
616 
apply (unfold dmd_def) 

617 
apply (clarsimp dest!: BoxPrime [temp_use]) 

42787  618 
apply merge_box 
21624  619 
apply (erule contrapos_np) 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
42814
diff
changeset

620 
apply (fastforce elim!: Stable [temp_use]) 
21624  621 
done 
622 

623 

624 
(*  Recursive expansions  *) 

625 
section "recursive expansions" 

626 

627 
(* Recursive expansions of [] and <> for state predicates *) 

628 
lemma BoxRec: " ([]P) = (Init P & []P`)" 

629 
apply (auto intro!: STL2_gen [temp_use]) 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
42814
diff
changeset

630 
apply (fastforce elim!: TLA2E [temp_use]) 
21624  631 
apply (auto simp: stable_def elim!: INV1 [temp_use] STL4E [temp_use]) 
632 
done 

633 

634 
lemma DmdRec: " (<>P) = (Init P  <>P`)" 

635 
apply (unfold dmd_def BoxRec [temp_rewrite]) 

636 
apply (auto simp: Init_simps) 

637 
done 

638 

639 
lemma DmdRec2: "!!sigma. [ sigma = <>P; sigma = []~P` ] ==> sigma = Init P" 

640 
apply (force simp: DmdRec [temp_rewrite] dmd_def) 

641 
done 

642 

643 
lemma InfinitePrime: " ([]<>P) = ([]<>P`)" 

644 
apply auto 

645 
apply (rule classical) 

646 
apply (rule DBImplBD [temp_use]) 

647 
apply (subgoal_tac "sigma = <>[]P") 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
42814
diff
changeset

648 
apply (fastforce elim!: DmdImplE [temp_use] TLA2E [temp_use]) 
21624  649 
apply (subgoal_tac "sigma = <>[] (<>P & []~P`)") 
650 
apply (force simp: boxInit_stp [temp_use] 

651 
elim!: DmdImplE [temp_use] STL4E [temp_use] DmdRec2 [temp_use]) 

26305  652 
apply (force intro!: STL6 [temp_use] simp: more_temp_simps3) 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
42814
diff
changeset

653 
apply (fastforce intro: DmdPrime [temp_use] elim!: STL4E [temp_use]) 
21624  654 
done 
655 

656 
lemma InfiniteEnsures: 

657 
"[ sigma = []N; sigma = []<>A;  A & N > P` ] ==> sigma = []<>P" 

658 
apply (unfold InfinitePrime [temp_rewrite]) 

659 
apply (rule InfImpl) 

660 
apply assumption+ 

661 
done 

662 

663 
(*  fairness  *) 

664 
section "fairness" 

665 

666 
(* alternative definitions of fairness *) 

667 
lemma WF_alt: " WF(A)_v = ([]<>~Enabled(<A>_v)  []<><A>_v)" 

668 
apply (unfold WF_def dmd_def) 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
42814
diff
changeset

669 
apply fastforce 
21624  670 
done 
671 

672 
lemma SF_alt: " SF(A)_v = (<>[]~Enabled(<A>_v)  []<><A>_v)" 

673 
apply (unfold SF_def dmd_def) 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
42814
diff
changeset

674 
apply fastforce 
21624  675 
done 
676 

677 
(* theorems to "box" fairness conditions *) 

678 
lemma BoxWFI: " WF(A)_v > []WF(A)_v" 

26305  679 
by (auto simp: WF_alt [try_rewrite] more_temp_simps3 intro!: BoxOr [temp_use]) 
21624  680 

681 
lemma WF_Box: " ([]WF(A)_v) = WF(A)_v" 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
42814
diff
changeset

682 
by (fastforce intro!: BoxWFI [temp_use] dest!: STL2 [temp_use]) 
21624  683 

684 
lemma BoxSFI: " SF(A)_v > []SF(A)_v" 

26305  685 
by (auto simp: SF_alt [try_rewrite] more_temp_simps3 intro!: BoxOr [temp_use]) 
21624  686 

687 
lemma SF_Box: " ([]SF(A)_v) = SF(A)_v" 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
42814
diff
changeset

688 
by (fastforce intro!: BoxSFI [temp_use] dest!: STL2 [temp_use]) 
21624  689 

26305  690 
lemmas more_temp_simps = more_temp_simps3 WF_Box [temp_rewrite] SF_Box [temp_rewrite] 
21624  691 

692 
lemma SFImplWF: " SF(A)_v > WF(A)_v" 

693 
apply (unfold SF_def WF_def) 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
42814
diff
changeset

694 
apply (fastforce dest!: DBImplBD [temp_use]) 
21624  695 
done 
696 

697 
(* A tactic that "boxes" all fairness conditions. Apply more_temp_simps to "unbox". *) 

698 
ML {* 

26305  699 
val box_fair_tac = SELECT_GOAL (REPEAT (dresolve_tac [@{thm BoxWFI}, @{thm BoxSFI}] 1)) 
21624  700 
*} 
701 

702 

703 
(*  leadsto  *) 

704 

705 
section "~>" 

706 

707 
lemma leadsto_init: " (Init F) & (F ~> G) > <>G" 

708 
apply (unfold leadsto_def) 

709 
apply (auto dest!: STL2 [temp_use]) 

710 
done 

711 

712 
(*  F & (F ~> G) > <>G *) 

45605  713 
lemmas leadsto_init_temp = leadsto_init [where 'a = behavior, unfolded Init_simps] 
21624  714 

715 
lemma streett_leadsto: " ([]<>Init F > []<>G) = (<>(F ~> G))" 

716 
apply (unfold leadsto_def) 

717 
apply auto 

718 
apply (simp add: more_temp_simps) 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
42814
diff
changeset

719 
apply (fastforce elim!: DmdImplE [temp_use] STL4E [temp_use]) 
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
42814
diff
changeset

720 
apply (fastforce intro!: InitDmd [temp_use] elim!: STL4E [temp_use]) 
21624  721 
apply (subgoal_tac "sigma = []<><>G") 
722 
apply (simp add: more_temp_simps) 

723 
apply (drule BoxDmdDmdBox [temp_use]) 

724 
apply assumption 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
42814
diff
changeset

725 
apply (fastforce elim!: DmdImplE [temp_use] STL4E [temp_use]) 
21624  726 
done 
727 

728 
lemma leadsto_infinite: " []<>F & (F ~> G) > []<>G" 

729 
apply clarsimp 

730 
apply (erule InitDmd [temp_use, THEN streett_leadsto [temp_unlift, THEN iffD2, THEN mp]]) 

731 
apply (simp add: dmdInitD) 

732 
done 

733 

734 
(* In particular, strong fairness is a Streett condition. The following 

735 
rules are sometimes easier to use than WF2 or SF2 below. 

736 
*) 

737 
lemma leadsto_SF: " (Enabled(<A>_v) ~> <A>_v) > SF(A)_v" 

738 
apply (unfold SF_def) 

739 
apply (clarsimp elim!: leadsto_infinite [temp_use]) 

740 
done 

741 

742 
lemma leadsto_WF: " (Enabled(<A>_v) ~> <A>_v) > WF(A)_v" 

743 
by (clarsimp intro!: SFImplWF [temp_use] leadsto_SF [temp_use]) 

744 

745 
(* introduce an invariant into the proof of a leadsto assertion. 

746 
[]I > ((P ~> Q) = (P /\ I ~> Q)) 

747 
*) 

748 
lemma INV_leadsto: " []I & (P & I ~> Q) > (P ~> Q)" 

749 
apply (unfold leadsto_def) 

750 
apply clarsimp 

751 
apply (erule STL4Edup) 

752 
apply assumption 

753 
apply (auto simp: Init_simps dest!: STL2_gen [temp_use]) 

754 
done 

755 

756 
lemma leadsto_classical: " (Init F & []~G ~> G) > (F ~> G)" 

757 
apply (unfold leadsto_def dmd_def) 

758 
apply (force simp: Init_simps elim!: STL4E [temp_use]) 

759 
done 

760 

761 
lemma leadsto_false: " (F ~> #False) = ([]~F)" 

762 
apply (unfold leadsto_def) 

763 
apply (simp add: boxNotInitD) 

764 
done 

765 

766 
lemma leadsto_exists: " ((EX x. F x) ~> G) = (ALL x. (F x ~> G))" 

767 
apply (unfold leadsto_def) 

768 
apply (auto simp: allT [try_rewrite] Init_simps elim!: STL4E [temp_use]) 

769 
done 

770 

771 
(* basic leadsto properties, cf. Unity *) 

772 

773 
lemma ImplLeadsto_gen: " [](Init F > Init G) > (F ~> G)" 

774 
apply (unfold leadsto_def) 

775 
apply (auto intro!: InitDmd_gen [temp_use] 

776 
elim!: STL4E_gen [temp_use] simp: Init_simps) 

777 
done 

778 

45605  779 
lemmas ImplLeadsto = 
780 
ImplLeadsto_gen [where 'a = behavior and 'b = behavior, unfolded Init_simps] 

21624  781 

782 
lemma ImplLeadsto_simple: "!!F G.  F > G ==>  F ~> G" 

783 
by (auto simp: Init_def intro!: ImplLeadsto_gen [temp_use] necT [temp_use]) 

784 

785 
lemma EnsuresLeadsto: 

786 
assumes " A & $P > Q`" 

787 
shows " []A > (P ~> Q)" 

788 
apply (unfold leadsto_def) 

789 
apply (clarsimp elim!: INV_leadsto [temp_use]) 

790 
apply (erule STL4E_gen) 

791 
apply (auto simp: Init_defs intro!: PrimeDmd [temp_use] assms [temp_use]) 

792 
done 

793 

794 
lemma EnsuresLeadsto2: " []($P > Q`) > (P ~> Q)" 

795 
apply (unfold leadsto_def) 

796 
apply clarsimp 

797 
apply (erule STL4E_gen) 

798 
apply (auto simp: Init_simps intro!: PrimeDmd [temp_use]) 

799 
done 

800 

801 
lemma ensures: 

802 
assumes 1: " $P & N > P`  Q`" 

803 
and 2: " ($P & N) & A > Q`" 

804 
shows " []N & []([]P > <>A) > (P ~> Q)" 

805 
apply (unfold leadsto_def) 

806 
apply clarsimp 

807 
apply (erule STL4Edup) 

808 
apply assumption 

809 
apply clarsimp 

810 
apply (subgoal_tac "sigmaa = [] ($P > P`  Q`) ") 

811 
apply (drule unless [temp_use]) 

812 
apply (clarsimp dest!: INV1 [temp_use]) 

813 
apply (rule 2 [THEN DmdImpl, temp_use, THEN DmdPrime [temp_use]]) 

814 
apply (force intro!: BoxDmd_simple [temp_use] 

815 
simp: split_box_conj [try_rewrite] box_stp_act [try_rewrite]) 

816 
apply (force elim: STL4E [temp_use] dest: 1 [temp_use]) 

817 
done 

818 

819 
lemma ensures_simple: 

820 
"[  $P & N > P`  Q`; 

821 
 ($P & N) & A > Q` 

822 
] ==>  []N & []<>A > (P ~> Q)" 

823 
apply clarsimp 

824 
apply (erule (2) ensures [temp_use]) 

825 
apply (force elim!: STL4E [temp_use]) 

826 
done 

827 

828 
lemma EnsuresInfinite: 

829 
"[ sigma = []<>P; sigma = []A;  A & $P > Q` ] ==> sigma = []<>Q" 

830 
apply (erule leadsto_infinite [temp_use]) 

831 
apply (erule EnsuresLeadsto [temp_use]) 

832 
apply assumption 

833 
done 

834 

835 

836 
(*** Gronning's lattice rules (taken from TLP) ***) 

837 
section "Lattice rules" 

838 

839 
lemma LatticeReflexivity: " F ~> F" 

840 
apply (unfold leadsto_def) 

841 
apply (rule necT InitDmd_gen)+ 

842 
done 

843 

844 
lemma LatticeTransitivity: " (G ~> H) & (F ~> G) > (F ~> H)" 

845 
apply (unfold leadsto_def) 

846 
apply clarsimp 

847 
apply (erule dup_boxE) (* [][] (Init G > H) *) 

42787  848 
apply merge_box 
21624  849 
apply (clarsimp elim!: STL4E [temp_use]) 
850 
apply (rule dup_dmdD) 

851 
apply (subgoal_tac "sigmaa = <>Init G") 

852 
apply (erule DmdImpl2) 

853 
apply assumption 

854 
apply (simp add: dmdInitD) 

855 
done 

856 

857 
lemma LatticeDisjunctionElim1: " (F  G ~> H) > (F ~> H)" 

858 
apply (unfold leadsto_def) 

859 
apply (auto simp: Init_simps elim!: STL4E [temp_use]) 

860 
done 

861 

862 
lemma LatticeDisjunctionElim2: " (F  G ~> H) > (G ~> H)" 

863 
apply (unfold leadsto_def) 

864 
apply (auto simp: Init_simps elim!: STL4E [temp_use]) 

865 
done 

866 

867 
lemma LatticeDisjunctionIntro: " (F ~> H) & (G ~> H) > (F  G ~> H)" 

868 
apply (unfold leadsto_def) 

869 
apply clarsimp 

42787  870 
apply merge_box 
21624  871 
apply (auto simp: Init_simps elim!: STL4E [temp_use]) 
872 
done 

873 

874 
lemma LatticeDisjunction: " (F  G ~> H) = ((F ~> H) & (G ~> H))" 

875 
by (auto intro: LatticeDisjunctionIntro [temp_use] 

876 
LatticeDisjunctionElim1 [temp_use] 

877 
LatticeDisjunctionElim2 [temp_use]) 

878 

879 
lemma LatticeDiamond: " (A ~> B  C) & (B ~> D) & (C ~> D) > (A ~> D)" 

880 
apply clarsimp 

881 
apply (subgoal_tac "sigma = (B  C) ~> D") 

882 
apply (erule_tac G = "LIFT (B  C)" in LatticeTransitivity [temp_use]) 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
42814
diff
changeset

883 
apply (fastforce intro!: LatticeDisjunctionIntro [temp_use])+ 
21624  884 
done 
885 

886 
lemma LatticeTriangle: " (A ~> D  B) & (B ~> D) > (A ~> D)" 

887 
apply clarsimp 

888 
apply (subgoal_tac "sigma = (D  B) ~> D") 

889 
apply (erule_tac G = "LIFT (D  B)" in LatticeTransitivity [temp_use]) 

890 
apply assumption 

891 
apply (auto intro: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use]) 

892 
done 

893 

894 
lemma LatticeTriangle2: " (A ~> B  D) & (B ~> D) > (A ~> D)" 

895 
apply clarsimp 

896 
apply (subgoal_tac "sigma = B  D ~> D") 

897 
apply (erule_tac G = "LIFT (B  D)" in LatticeTransitivity [temp_use]) 

898 
apply assumption 

899 
apply (auto intro: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use]) 

900 
done 

901 

902 
(*** Lamport's fairness rules ***) 

903 
section "Fairness rules" 

904 

905 
lemma WF1: 

906 
"[  $P & N > P`  Q`; 

907 
 ($P & N) & <A>_v > Q`; 

908 
 $P & N > $(Enabled(<A>_v)) ] 

909 
==>  []N & WF(A)_v > (P ~> Q)" 

910 
apply (clarsimp dest!: BoxWFI [temp_use]) 

911 
apply (erule (2) ensures [temp_use]) 

912 
apply (erule (1) STL4Edup) 

913 
apply (clarsimp simp: WF_def) 

914 
apply (rule STL2 [temp_use]) 

915 
apply (clarsimp elim!: mp intro!: InitDmd [temp_use]) 

916 
apply (erule STL4 [temp_use, THEN box_stp_actD [temp_use]]) 

917 
apply (simp add: split_box_conj box_stp_actI) 

918 
done 

919 

920 
(* Sometimes easier to use; designed for action B rather than state predicate Q *) 

921 
lemma WF_leadsto: 

922 
assumes 1: " N & $P > $Enabled (<A>_v)" 

923 
and 2: " N & <A>_v > B" 

924 
and 3: " [](N & [~A]_v) > stable P" 

925 
shows " []N & WF(A)_v > (P ~> B)" 

926 
apply (unfold leadsto_def) 

927 
apply (clarsimp dest!: BoxWFI [temp_use]) 

928 
apply (erule (1) STL4Edup) 

929 
apply clarsimp 

930 
apply (rule 2 [THEN DmdImpl, temp_use]) 

931 
apply (rule BoxDmd_simple [temp_use]) 

932 
apply assumption 

933 
apply (rule classical) 

934 
apply (rule STL2 [temp_use]) 

935 
apply (clarsimp simp: WF_def elim!: mp intro!: InitDmd [temp_use]) 

936 
apply (rule 1 [THEN STL4, temp_use, THEN box_stp_actD]) 

937 
apply (simp (no_asm_simp) add: split_box_conj [try_rewrite] box_stp_act [try_rewrite]) 

938 
apply (erule INV1 [temp_use]) 

939 
apply (rule 3 [temp_use]) 

940 
apply (simp add: split_box_conj [try_rewrite] NotDmd [temp_use] not_angle [try_rewrite]) 

941 
done 

942 

943 
lemma SF1: 

944 
"[  $P & N > P`  Q`; 

945 
 ($P & N) & <A>_v > Q`; 

946 
 []P & []N & []F > <>Enabled(<A>_v) ] 

947 
==>  []N & SF(A)_v & []F > (P ~> Q)" 

948 
apply (clarsimp dest!: BoxSFI [temp_use]) 

949 
apply (erule (2) ensures [temp_use]) 

950 
apply (erule_tac F = F in dup_boxE) 

42787  951 
apply merge_temp_box 
21624  952 
apply (erule STL4Edup) 
953 
apply assumption 

954 
apply (clarsimp simp: SF_def) 

955 
apply (rule STL2 [temp_use]) 

956 
apply (erule mp) 

957 
apply (erule STL4 [temp_use]) 

958 
apply (simp add: split_box_conj [try_rewrite] STL3 [try_rewrite]) 

959 
done 

960 

961 
lemma WF2: 

962 
assumes 1: " N & <B>_f > <M>_g" 

963 
and 2: " $P & P` & <N & A>_f > B" 

964 
and 3: " P & Enabled(<M>_g) > Enabled(<A>_f)" 

965 
and 4: " [](N & [~B]_f) & WF(A)_f & []F & <>[]Enabled(<M>_g) > <>[]P" 

966 
shows " []N & WF(A)_f & []F > WF(M)_g" 

967 
apply (clarsimp dest!: BoxWFI [temp_use] BoxDmdBox [temp_use, THEN iffD2] 

968 
simp: WF_def [where A = M]) 

969 
apply (erule_tac F = F in dup_boxE) 

42787  970 
apply merge_temp_box 
21624  971 
apply (erule STL4Edup) 
972 
apply assumption 

973 
apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]]) 

974 
apply (rule classical) 

975 
apply (subgoal_tac "sigmaa = <> (($P & P` & N) & <A>_f)") 

976 
apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use]) 

977 
apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use]) 

978 
apply (simp add: NotDmd [temp_use] not_angle [try_rewrite]) 

42787  979 
apply merge_act_box 
21624  980 
apply (frule 4 [temp_use]) 
981 
apply assumption+ 

982 
apply (drule STL6 [temp_use]) 

983 
apply assumption 

984 
apply (erule_tac V = "sigmaa = <>[]P" in thin_rl) 

985 
apply (erule_tac V = "sigmaa = []F" in thin_rl) 

986 
apply (drule BoxWFI [temp_use]) 

987 
apply (erule_tac F = "ACT N & [~B]_f" in dup_boxE) 

42787  988 
apply merge_temp_box 
21624  989 
apply (erule DmdImpldup) 
990 
apply assumption 

991 
apply (auto simp: split_box_conj [try_rewrite] STL3 [try_rewrite] 

992 
WF_Box [try_rewrite] box_stp_act [try_rewrite]) 

993 
apply (force elim!: TLA2E [where P = P, temp_use]) 

994 
apply (rule STL2 [temp_use]) 

995 
apply (force simp: WF_def split_box_conj [try_rewrite] 

996 
elim!: mp intro!: InitDmd [temp_use] 3 [THEN STL4, temp_use]) 

997 
done 

998 

999 
lemma SF2: 

1000 
assumes 1: " N & <B>_f > <M>_g" 

1001 
and 2: " $P & P` & <N & A>_f > B" 

1002 
and 3: " P & Enabled(<M>_g) > Enabled(<A>_f)" 

1003 
and 4: " [](N & [~B]_f) & SF(A)_f & []F & []<>Enabled(<M>_g) > <>[]P" 

1004 
shows " []N & SF(A)_f & []F > SF(M)_g" 

1005 
apply (clarsimp dest!: BoxSFI [temp_use] simp: 2 [try_rewrite] SF_def [where A = M]) 

1006 
apply (erule_tac F = F in dup_boxE) 

1007 
apply (erule_tac F = "TEMP <>Enabled (<M>_g) " in dup_boxE) 

42787  1008 
apply merge_temp_box 
21624  1009 
apply (erule STL4Edup) 
1010 
apply assumption 

1011 
apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]]) 

1012 
apply (rule classical) 

1013 
apply (subgoal_tac "sigmaa = <> (($P & P` & N) & <A>_f)") 

1014 
apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use]) 

1015 
apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use]) 

1016 
apply (simp add: NotDmd [temp_use] not_angle [try_rewrite]) 

42787  1017 
apply merge_act_box 
21624  1018 
apply (frule 4 [temp_use]) 
1019 
apply assumption+ 

1020 
apply (erule_tac V = "sigmaa = []F" in thin_rl) 

1021 
apply (drule BoxSFI [temp_use]) 

1022 
apply (erule_tac F = "TEMP <>Enabled (<M>_g)" in dup_boxE) 

1023 
apply (erule_tac F = "ACT N & [~B]_f" in dup_boxE) 

42787  1024 
apply merge_temp_box 
21624  1025 
apply (erule DmdImpldup) 
1026 
apply assumption 

1027 
apply (auto simp: split_box_conj [try_rewrite] STL3 [try_rewrite] 

1028 
SF_Box [try_rewrite] box_stp_act [try_rewrite]) 

1029 
apply (force elim!: TLA2E [where P = P, temp_use]) 

1030 
apply (rule STL2 [temp_use]) 

1031 
apply (force simp: SF_def split_box_conj [try_rewrite] 

1032 
elim!: mp InfImpl [temp_use] intro!: 3 [temp_use]) 

1033 
done 

1034 

1035 
(*  *) 

1036 
(*** Liveness proofs by wellfounded orderings ***) 

1037 
(*  *) 

1038 
section "Wellfounded orderings" 

1039 

1040 
lemma wf_leadsto: 

1041 
assumes 1: "wf r" 

1042 
and 2: "!!x. sigma = F x ~> (G  (EX y. #((y,x):r) & F y)) " 

1043 
shows "sigma = F x ~> G" 

1044 
apply (rule 1 [THEN wf_induct]) 

1045 
apply (rule LatticeTriangle [temp_use]) 

1046 
apply (rule 2) 

1047 
apply (auto simp: leadsto_exists [try_rewrite]) 

1048 
apply (case_tac "(y,x) :r") 

1049 
apply force 

1050 
apply (force simp: leadsto_def Init_simps intro!: necT [temp_use]) 

1051 
done 

1052 

1053 
(* If r is wellfounded, state function v cannot decrease forever *) 

1054 
lemma wf_not_box_decrease: "!!r. wf r ==>  [][ (v`, $v) : #r ]_v > <>[][#False]_v" 

1055 
apply clarsimp 

1056 
apply (rule ccontr) 

1057 
apply (subgoal_tac "sigma = (EX x. v=#x) ~> #False") 

1058 
apply (drule leadsto_false [temp_use, THEN iffD1, THEN STL2_gen [temp_use]]) 

1059 
apply (force simp: Init_defs) 

1060 
apply (clarsimp simp: leadsto_exists [try_rewrite] not_square [try_rewrite] more_temp_simps) 

1061 
apply (erule wf_leadsto) 

1062 
apply (rule ensures_simple [temp_use]) 

1063 
apply (auto simp: square_def angle_def) 

1064 
done 

1065 

1066 
(* "wf r ==>  <>[][ (v`, $v) : #r ]_v > <>[][#False]_v" *) 

1067 
lemmas wf_not_dmd_box_decrease = 

45605  1068 
wf_not_box_decrease [THEN DmdImpl, unfolded more_temp_simps] 
21624  1069 

1070 
(* If there are infinitely many steps where v decreases, then there 

1071 
have to be infinitely many nonstuttering steps where v doesn't decrease. 

1072 
*) 

1073 
lemma wf_box_dmd_decrease: 

1074 
assumes 1: "wf r" 

1075 
shows " []<>((v`, $v) : #r) > []<><(v`, $v) ~: #r>_v" 

1076 
apply clarsimp 

1077 
apply (rule ccontr) 

1078 
apply (simp add: not_angle [try_rewrite] more_temp_simps) 

1079 
apply (drule 1 [THEN wf_not_dmd_box_decrease [temp_use]]) 

1080 
apply (drule BoxDmdDmdBox [temp_use]) 

1081 
apply assumption 

1082 
apply (subgoal_tac "sigma = []<> ((#False) ::action)") 

1083 
apply force 

1084 
apply (erule STL4E) 

1085 
apply (rule DmdImpl) 

1086 
apply (force intro: 1 [THEN wf_irrefl, temp_use]) 

1087 
done 

1088 

1089 
(* In particular, for natural numbers, if n decreases infinitely often 

1090 
then it has to increase infinitely often. 

1091 
*) 

1092 
lemma nat_box_dmd_decrease: "!!n::nat stfun.  []<>(n` < $n) > []<>($n < n`)" 

1093 
apply clarsimp 

1094 
apply (subgoal_tac "sigma = []<><~ ((n`,$n) : #less_than) >_n") 

1095 
apply (erule thin_rl) 

1096 
apply (erule STL4E) 

1097 
apply (rule DmdImpl) 

1098 
apply (clarsimp simp: angle_def [try_rewrite]) 

1099 
apply (rule wf_box_dmd_decrease [temp_use]) 

1100 
apply (auto elim!: STL4E [temp_use] DmdImplE [temp_use]) 

1101 
done 

1102 

1103 

1104 
(*  *) 

1105 
(*** Flexible quantification over state variables ***) 

1106 
(*  *) 

1107 
section "Flexible quantification" 

1108 

1109 
lemma aallI: 

1110 
assumes 1: "basevars vs" 

1111 
and 2: "(!!x. basevars (x,vs) ==> sigma = F x)" 

1112 
shows "sigma = (AALL x. F x)" 

1113 
by (auto simp: aall_def elim!: eexE [temp_use] intro!: 1 dest!: 2 [temp_use]) 

1114 

1115 
lemma aallE: " (AALL x. F x) > F x" 

1116 
apply (unfold aall_def) 

1117 
apply clarsimp 

1118 
apply (erule contrapos_np) 

1119 
apply (force intro!: eexI [temp_use]) 

1120 
done 

1121 

1122 
(* monotonicity of quantification *) 

1123 
lemma eex_mono: 

1124 
assumes 1: "sigma = EEX x. F x" 

1125 
and 2: "!!x. sigma = F x > G x" 

1126 
shows "sigma = EEX x. G x" 

1127 
apply (rule unit_base [THEN 1 [THEN eexE]]) 

1128 
apply (rule eexI [temp_use]) 

1129 
apply (erule 2 [unfolded intensional_rews, THEN mp]) 

1130 
done 

1131 

1132 
lemma aall_mono: 

1133 
assumes 1: "sigma = AALL x. F(x)" 

1134 
and 2: "!!x. sigma = F(x) > G(x)" 

1135 
shows "sigma = AALL x. G(x)" 

1136 
apply (rule unit_base [THEN aallI]) 

1137 
apply (rule 2 [unfolded intensional_rews, THEN mp]) 

1138 
apply (rule 1 [THEN aallE [temp_use]]) 

1139 
done 

1140 

1141 
(* Derived history introduction rule *) 

1142 
lemma historyI: 

1143 
assumes 1: "sigma = Init I" 

1144 
and 2: "sigma = []N" 

1145 
and 3: "basevars vs" 

1146 
and 4: "!!h. basevars(h,vs) ==>  I & h = ha > HI h" 

1147 
and 5: "!!h s t. [ basevars(h,vs); N (s,t); h t = hb (h s) (s,t) ] ==> HN h (s,t)" 

1148 
shows "sigma = EEX h. Init (HI h) & [](HN h)" 

1149 
apply (rule history [temp_use, THEN eexE]) 

1150 
apply (rule 3) 

1151 
apply (rule eexI [temp_use]) 

1152 
apply clarsimp 

1153 
apply (rule conjI) 

1154 
prefer 2 

1155 
apply (insert 2) 

42787  1156 
apply merge_box 
21624  1157 
apply (force elim!: STL4E [temp_use] 5 [temp_use]) 
1158 
apply (insert 1) 

1159 
apply (force simp: Init_defs elim!: 4 [temp_use]) 

1160 
done 

1161 

1162 
(*  

1163 
example of a history variable: existence of a clock 

1164 
*) 

1165 

1166 
lemma " EEX h. Init(h = #True) & [](h` = (~$h))" 

1167 
apply (rule tempI) 

1168 
apply (rule historyI) 

1169 
apply (force simp: Init_defs intro!: unit_base [temp_use] necT [temp_use])+ 

1170 
done 

1171 

1172 
end 