1(* Title: HOL/TLA/TLA.thy 2 Author: Stephan Merz 3 Copyright: 1998 University of Munich 4*) 5 6section \<open>The temporal level of TLA\<close> 7 8theory TLA 9imports Init 10begin 11 12consts 13 (** abstract syntax **) 14 Box :: "('w::world) form \<Rightarrow> temporal" 15 Dmd :: "('w::world) form \<Rightarrow> temporal" 16 leadsto :: "['w::world form, 'v::world form] \<Rightarrow> temporal" 17 Stable :: "stpred \<Rightarrow> temporal" 18 WF :: "[action, 'a stfun] \<Rightarrow> temporal" 19 SF :: "[action, 'a stfun] \<Rightarrow> temporal" 20 21 (* Quantification over (flexible) state variables *) 22 EEx :: "('a stfun \<Rightarrow> temporal) \<Rightarrow> temporal" (binder "Eex " 10) 23 AAll :: "('a stfun \<Rightarrow> temporal) \<Rightarrow> temporal" (binder "Aall " 10) 24 25 (** concrete syntax **) 26syntax 27 "_Box" :: "lift \<Rightarrow> lift" ("(\<box>_)" [40] 40) 28 "_Dmd" :: "lift \<Rightarrow> lift" ("(\<diamond>_)" [40] 40) 29 "_leadsto" :: "[lift,lift] \<Rightarrow> lift" ("(_ \<leadsto> _)" [23,22] 22) 30 "_stable" :: "lift \<Rightarrow> lift" ("(stable/ _)") 31 "_WF" :: "[lift,lift] \<Rightarrow> lift" ("(WF'(_')'_(_))" [0,60] 55) 32 "_SF" :: "[lift,lift] \<Rightarrow> lift" ("(SF'(_')'_(_))" [0,60] 55) 33 34 "_EEx" :: "[idts, lift] \<Rightarrow> lift" ("(3\<exists>\<exists> _./ _)" [0,10] 10) 35 "_AAll" :: "[idts, lift] \<Rightarrow> lift" ("(3\<forall>\<forall> _./ _)" [0,10] 10) 36 37translations 38 "_Box" == "CONST Box" 39 "_Dmd" == "CONST Dmd" 40 "_leadsto" == "CONST leadsto" 41 "_stable" == "CONST Stable" 42 "_WF" == "CONST WF" 43 "_SF" == "CONST SF" 44 "_EEx v A" == "Eex v. A" 45 "_AAll v A" == "Aall v. A" 46 47 "sigma \<Turnstile> \<box>F" <= "_Box F sigma" 48 "sigma \<Turnstile> \<diamond>F" <= "_Dmd F sigma" 49 "sigma \<Turnstile> F \<leadsto> G" <= "_leadsto F G sigma" 50 "sigma \<Turnstile> stable P" <= "_stable P sigma" 51 "sigma \<Turnstile> WF(A)_v" <= "_WF A v sigma" 52 "sigma \<Turnstile> SF(A)_v" <= "_SF A v sigma" 53 "sigma \<Turnstile> \<exists>\<exists>x. F" <= "_EEx x F sigma" 54 "sigma \<Turnstile> \<forall>\<forall>x. F" <= "_AAll x F sigma" 55 56axiomatization where 57 (* Definitions of derived operators *) 58 dmd_def: "\<And>F. TEMP \<diamond>F == TEMP \<not>\<box>\<not>F" 59 60axiomatization where 61 boxInit: "\<And>F. TEMP \<box>F == TEMP \<box>Init F" and 62 leadsto_def: "\<And>F G. TEMP F \<leadsto> G == TEMP \<box>(Init F \<longrightarrow> \<diamond>G)" and 63 stable_def: "\<And>P. TEMP stable P == TEMP \<box>($P \<longrightarrow> P$)" and 64 WF_def: "TEMP WF(A)_v == TEMP \<diamond>\<box> Enabled(<A>_v) \<longrightarrow> \<box>\<diamond><A>_v" and 65 SF_def: "TEMP SF(A)_v == TEMP \<box>\<diamond> Enabled(<A>_v) \<longrightarrow> \<box>\<diamond><A>_v" and 66 aall_def: "TEMP (\<forall>\<forall>x. F x) == TEMP \<not> (\<exists>\<exists>x. \<not> F x)" 67 68axiomatization where 69(* Base axioms for raw TLA. *) 70 normalT: "\<And>F G. \<turnstile> \<box>(F \<longrightarrow> G) \<longrightarrow> (\<box>F \<longrightarrow> \<box>G)" and (* polymorphic *) 71 reflT: "\<And>F. \<turnstile> \<box>F \<longrightarrow> F" and (* F::temporal *) 72 transT: "\<And>F. \<turnstile> \<box>F \<longrightarrow> \<box>\<box>F" and (* polymorphic *) 73 linT: "\<And>F G. \<turnstile> \<diamond>F \<and> \<diamond>G \<longrightarrow> (\<diamond>(F \<and> \<diamond>G)) \<or> (\<diamond>(G \<and> \<diamond>F))" and 74 discT: "\<And>F. \<turnstile> \<box>(F \<longrightarrow> \<diamond>(\<not>F \<and> \<diamond>F)) \<longrightarrow> (F \<longrightarrow> \<box>\<diamond>F)" and 75 primeI: "\<And>P. \<turnstile> \<box>P \<longrightarrow> Init P`" and 76 primeE: "\<And>P F. \<turnstile> \<box>(Init P \<longrightarrow> \<box>F) \<longrightarrow> Init P` \<longrightarrow> (F \<longrightarrow> \<box>F)" and 77 indT: "\<And>P F. \<turnstile> \<box>(Init P \<and> \<not>\<box>F \<longrightarrow> Init P` \<and> F) \<longrightarrow> Init P \<longrightarrow> \<box>F" and 78 allT: "\<And>F. \<turnstile> (\<forall>x. \<box>(F x)) = (\<box>(\<forall> x. F x))" 79 80axiomatization where 81 necT: "\<And>F. \<turnstile> F \<Longrightarrow> \<turnstile> \<box>F" (* polymorphic *) 82 83axiomatization where 84(* Flexible quantification: refinement mappings, history variables *) 85 eexI: "\<turnstile> F x \<longrightarrow> (\<exists>\<exists>x. F x)" and 86 eexE: "\<lbrakk> sigma \<Turnstile> (\<exists>\<exists>x. F x); basevars vs; 87 (\<And>x. \<lbrakk> basevars (x, vs); sigma \<Turnstile> F x \<rbrakk> \<Longrightarrow> (G sigma)::bool) 88 \<rbrakk> \<Longrightarrow> G sigma" and 89 history: "\<turnstile> \<exists>\<exists>h. Init(h = ha) \<and> \<box>(\<forall>x. $h = #x \<longrightarrow> h` = hb x)" 90 91 92(* Specialize intensional introduction/elimination rules for temporal formulas *) 93 94lemma tempI [intro!]: "(\<And>sigma. sigma \<Turnstile> (F::temporal)) \<Longrightarrow> \<turnstile> F" 95 apply (rule intI) 96 apply (erule meta_spec) 97 done 98 99lemma tempD [dest]: "\<turnstile> (F::temporal) \<Longrightarrow> sigma \<Turnstile> F" 100 by (erule intD) 101 102 103(* ======== Functions to "unlift" temporal theorems ====== *) 104 105ML \<open> 106(* The following functions are specialized versions of the corresponding 107 functions defined in theory Intensional in that they introduce a 108 "world" parameter of type "behavior". 109*) 110fun temp_unlift ctxt th = 111 (rewrite_rule ctxt @{thms action_rews} (th RS @{thm tempD})) 112 handle THM _ => action_unlift ctxt th; 113 114(* Turn \<turnstile> F = G into meta-level rewrite rule F == G *) 115val temp_rewrite = int_rewrite 116 117fun temp_use ctxt th = 118 case Thm.concl_of th of 119 Const _ $ (Const (\<^const_name>\<open>Intensional.Valid\<close>, _) $ _) => 120 ((flatten (temp_unlift ctxt th)) handle THM _ => th) 121 | _ => th; 122 123fun try_rewrite ctxt th = temp_rewrite ctxt th handle THM _ => temp_use ctxt th; 124\<close> 125 126attribute_setup temp_unlift = 127 \<open>Scan.succeed (Thm.rule_attribute [] (temp_unlift o Context.proof_of))\<close> 128attribute_setup temp_rewrite = 129 \<open>Scan.succeed (Thm.rule_attribute [] (temp_rewrite o Context.proof_of))\<close> 130attribute_setup temp_use = 131 \<open>Scan.succeed (Thm.rule_attribute [] (temp_use o Context.proof_of))\<close> 132attribute_setup try_rewrite = 133 \<open>Scan.succeed (Thm.rule_attribute [] (try_rewrite o Context.proof_of))\<close> 134 135 136(* ------------------------------------------------------------------------- *) 137(*** "Simple temporal logic": only \<box> and \<diamond> ***) 138(* ------------------------------------------------------------------------- *) 139section "Simple temporal logic" 140 141(* \<box>\<not>F == \<box>\<not>Init F *) 142lemmas boxNotInit = boxInit [of "LIFT \<not>F", unfolded Init_simps] for F 143 144lemma dmdInit: "TEMP \<diamond>F == TEMP \<diamond> Init F" 145 apply (unfold dmd_def) 146 apply (unfold boxInit [of "LIFT \<not>F"]) 147 apply (simp (no_asm) add: Init_simps) 148 done 149 150lemmas dmdNotInit = dmdInit [of "LIFT \<not>F", unfolded Init_simps] for F 151 152(* boxInit and dmdInit cannot be used as rewrites, because they loop. 153 Non-looping instances for state predicates and actions are occasionally useful. 154*) 155lemmas boxInit_stp = boxInit [where 'a = state] 156lemmas boxInit_act = boxInit [where 'a = "state * state"] 157lemmas dmdInit_stp = dmdInit [where 'a = state] 158lemmas dmdInit_act = dmdInit [where 'a = "state * state"] 159 160(* The symmetric equations can be used to get rid of Init *) 161lemmas boxInitD = boxInit [symmetric] 162lemmas dmdInitD = dmdInit [symmetric] 163lemmas boxNotInitD = boxNotInit [symmetric] 164lemmas dmdNotInitD = dmdNotInit [symmetric] 165 166lemmas Init_simps = Init_simps boxInitD dmdInitD boxNotInitD dmdNotInitD 167 168(* ------------------------ STL2 ------------------------------------------- *) 169lemmas STL2 = reflT 170 171(* The "polymorphic" (generic) variant *) 172lemma STL2_gen: "\<turnstile> \<box>F \<longrightarrow> Init F" 173 apply (unfold boxInit [of F]) 174 apply (rule STL2) 175 done 176 177(* see also STL2_pr below: "\<turnstile> \<box>P \<longrightarrow> Init P & Init (P`)" *) 178 179 180(* Dual versions for \<diamond> *) 181lemma InitDmd: "\<turnstile> F \<longrightarrow> \<diamond> F" 182 apply (unfold dmd_def) 183 apply (auto dest!: STL2 [temp_use]) 184 done 185 186lemma InitDmd_gen: "\<turnstile> Init F \<longrightarrow> \<diamond>F" 187 apply clarsimp 188 apply (drule InitDmd [temp_use]) 189 apply (simp add: dmdInitD) 190 done 191 192 193(* ------------------------ STL3 ------------------------------------------- *) 194lemma STL3: "\<turnstile> (\<box>\<box>F) = (\<box>F)" 195 by (auto elim: transT [temp_use] STL2 [temp_use]) 196 197(* corresponding elimination rule introduces double boxes: 198 \<lbrakk> (sigma \<Turnstile> \<box>F); (sigma \<Turnstile> \<box>\<box>F) \<Longrightarrow> PROP W \<rbrakk> \<Longrightarrow> PROP W 199*) 200lemmas dup_boxE = STL3 [temp_unlift, THEN iffD2, elim_format] 201lemmas dup_boxD = STL3 [temp_unlift, THEN iffD1] 202 203(* dual versions for \<diamond> *) 204lemma DmdDmd: "\<turnstile> (\<diamond>\<diamond>F) = (\<diamond>F)" 205 by (auto simp add: dmd_def [try_rewrite] STL3 [try_rewrite]) 206 207lemmas dup_dmdE = DmdDmd [temp_unlift, THEN iffD2, elim_format] 208lemmas dup_dmdD = DmdDmd [temp_unlift, THEN iffD1] 209 210 211(* ------------------------ STL4 ------------------------------------------- *) 212lemma STL4: 213 assumes "\<turnstile> F \<longrightarrow> G" 214 shows "\<turnstile> \<box>F \<longrightarrow> \<box>G" 215 apply clarsimp 216 apply (rule normalT [temp_use]) 217 apply (rule assms [THEN necT, temp_use]) 218 apply assumption 219 done 220 221(* Unlifted version as an elimination rule *) 222lemma STL4E: "\<lbrakk> sigma \<Turnstile> \<box>F; \<turnstile> F \<longrightarrow> G \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>G" 223 by (erule (1) STL4 [temp_use]) 224 225lemma STL4_gen: "\<turnstile> Init F \<longrightarrow> Init G \<Longrightarrow> \<turnstile> \<box>F \<longrightarrow> \<box>G" 226 apply (drule STL4) 227 apply (simp add: boxInitD) 228 done 229 230lemma STL4E_gen: "\<lbrakk> sigma \<Turnstile> \<box>F; \<turnstile> Init F \<longrightarrow> Init G \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>G" 231 by (erule (1) STL4_gen [temp_use]) 232 233(* see also STL4Edup below, which allows an auxiliary boxed formula: 234 \<box>A /\ F => G 235 ----------------- 236 \<box>A /\ \<box>F => \<box>G 237*) 238 239(* The dual versions for \<diamond> *) 240lemma DmdImpl: 241 assumes prem: "\<turnstile> F \<longrightarrow> G" 242 shows "\<turnstile> \<diamond>F \<longrightarrow> \<diamond>G" 243 apply (unfold dmd_def) 244 apply (fastforce intro!: prem [temp_use] elim!: STL4E [temp_use]) 245 done 246 247lemma DmdImplE: "\<lbrakk> sigma \<Turnstile> \<diamond>F; \<turnstile> F \<longrightarrow> G \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<diamond>G" 248 by (erule (1) DmdImpl [temp_use]) 249 250(* ------------------------ STL5 ------------------------------------------- *) 251lemma STL5: "\<turnstile> (\<box>F \<and> \<box>G) = (\<box>(F \<and> G))" 252 apply auto 253 apply (subgoal_tac "sigma \<Turnstile> \<box> (G \<longrightarrow> (F \<and> G))") 254 apply (erule normalT [temp_use]) 255 apply (fastforce elim!: STL4E [temp_use])+ 256 done 257 258(* rewrite rule to split conjunctions under boxes *) 259lemmas split_box_conj = STL5 [temp_unlift, symmetric] 260 261 262(* the corresponding elimination rule allows to combine boxes in the hypotheses 263 (NB: F and G must have the same type, i.e., both actions or temporals.) 264 Use "addSE2" etc. if you want to add this to a claset, otherwise it will loop! 265*) 266lemma box_conjE: 267 assumes "sigma \<Turnstile> \<box>F" 268 and "sigma \<Turnstile> \<box>G" 269 and "sigma \<Turnstile> \<box>(F\<and>G) \<Longrightarrow> PROP R" 270 shows "PROP R" 271 by (rule assms STL5 [temp_unlift, THEN iffD1] conjI)+ 272 273(* Instances of box_conjE for state predicates, actions, and temporals 274 in case the general rule is "too polymorphic". 275*) 276lemmas box_conjE_temp = box_conjE [where 'a = behavior] 277lemmas box_conjE_stp = box_conjE [where 'a = state] 278lemmas box_conjE_act = box_conjE [where 'a = "state * state"] 279 280(* Define a tactic that tries to merge all boxes in an antecedent. The definition is 281 a bit kludgy in order to simulate "double elim-resolution". 282*) 283 284lemma box_thin: "\<lbrakk> sigma \<Turnstile> \<box>F; PROP W \<rbrakk> \<Longrightarrow> PROP W" . 285 286ML \<open> 287fun merge_box_tac ctxt i = 288 REPEAT_DETERM (EVERY [eresolve_tac ctxt @{thms box_conjE} i, assume_tac ctxt i, 289 eresolve_tac ctxt @{thms box_thin} i]) 290 291fun merge_temp_box_tac ctxt i = 292 REPEAT_DETERM (EVERY [eresolve_tac ctxt @{thms box_conjE_temp} i, assume_tac ctxt i, 293 Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "behavior")] [] @{thm box_thin} i]) 294 295fun merge_stp_box_tac ctxt i = 296 REPEAT_DETERM (EVERY [eresolve_tac ctxt @{thms box_conjE_stp} i, assume_tac ctxt i, 297 Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "state")] [] @{thm box_thin} i]) 298 299fun merge_act_box_tac ctxt i = 300 REPEAT_DETERM (EVERY [eresolve_tac ctxt @{thms box_conjE_act} i, assume_tac ctxt i, 301 Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "state * state")] [] @{thm box_thin} i]) 302\<close> 303 304method_setup merge_box = \<open>Scan.succeed (SIMPLE_METHOD' o merge_box_tac)\<close> 305method_setup merge_temp_box = \<open>Scan.succeed (SIMPLE_METHOD' o merge_temp_box_tac)\<close> 306method_setup merge_stp_box = \<open>Scan.succeed (SIMPLE_METHOD' o merge_stp_box_tac)\<close> 307method_setup merge_act_box = \<open>Scan.succeed (SIMPLE_METHOD' o merge_act_box_tac)\<close> 308 309(* rewrite rule to push universal quantification through box: 310 (sigma \<Turnstile> \<box>(\<forall>x. F x)) = (\<forall>x. (sigma \<Turnstile> \<box>F x)) 311*) 312lemmas all_box = allT [temp_unlift, symmetric] 313 314lemma DmdOr: "\<turnstile> (\<diamond>(F \<or> G)) = (\<diamond>F \<or> \<diamond>G)" 315 apply (auto simp add: dmd_def split_box_conj [try_rewrite]) 316 apply (erule contrapos_np, merge_box, fastforce elim!: STL4E [temp_use])+ 317 done 318 319lemma exT: "\<turnstile> (\<exists>x. \<diamond>(F x)) = (\<diamond>(\<exists>x. F x))" 320 by (auto simp: dmd_def Not_Rex [try_rewrite] all_box [try_rewrite]) 321 322lemmas ex_dmd = exT [temp_unlift, symmetric] 323 324lemma STL4Edup: "\<And>sigma. \<lbrakk> sigma \<Turnstile> \<box>A; sigma \<Turnstile> \<box>F; \<turnstile> F \<and> \<box>A \<longrightarrow> G \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>G" 325 apply (erule dup_boxE) 326 apply merge_box 327 apply (erule STL4E) 328 apply assumption 329 done 330 331lemma DmdImpl2: 332 "\<And>sigma. \<lbrakk> sigma \<Turnstile> \<diamond>F; sigma \<Turnstile> \<box>(F \<longrightarrow> G) \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<diamond>G" 333 apply (unfold dmd_def) 334 apply auto 335 apply (erule notE) 336 apply merge_box 337 apply (fastforce elim!: STL4E [temp_use]) 338 done 339 340lemma InfImpl: 341 assumes 1: "sigma \<Turnstile> \<box>\<diamond>F" 342 and 2: "sigma \<Turnstile> \<box>G" 343 and 3: "\<turnstile> F \<and> G \<longrightarrow> H" 344 shows "sigma \<Turnstile> \<box>\<diamond>H" 345 apply (insert 1 2) 346 apply (erule_tac F = G in dup_boxE) 347 apply merge_box 348 apply (fastforce elim!: STL4E [temp_use] DmdImpl2 [temp_use] intro!: 3 [temp_use]) 349 done 350 351(* ------------------------ STL6 ------------------------------------------- *) 352(* Used in the proof of STL6, but useful in itself. *) 353lemma BoxDmd: "\<turnstile> \<box>F \<and> \<diamond>G \<longrightarrow> \<diamond>(\<box>F \<and> G)" 354 apply (unfold dmd_def) 355 apply clarsimp 356 apply (erule dup_boxE) 357 apply merge_box 358 apply (erule contrapos_np) 359 apply (fastforce elim!: STL4E [temp_use]) 360 done 361 362(* weaker than BoxDmd, but more polymorphic (and often just right) *) 363lemma BoxDmd_simple: "\<turnstile> \<box>F \<and> \<diamond>G \<longrightarrow> \<diamond>(F \<and> G)" 364 apply (unfold dmd_def) 365 apply clarsimp 366 apply merge_box 367 apply (fastforce elim!: notE STL4E [temp_use]) 368 done 369 370lemma BoxDmd2_simple: "\<turnstile> \<box>F \<and> \<diamond>G \<longrightarrow> \<diamond>(G \<and> F)" 371 apply (unfold dmd_def) 372 apply clarsimp 373 apply merge_box 374 apply (fastforce elim!: notE STL4E [temp_use]) 375 done 376 377lemma DmdImpldup: 378 assumes 1: "sigma \<Turnstile> \<box>A" 379 and 2: "sigma \<Turnstile> \<diamond>F" 380 and 3: "\<turnstile> \<box>A \<and> F \<longrightarrow> G" 381 shows "sigma \<Turnstile> \<diamond>G" 382 apply (rule 2 [THEN 1 [THEN BoxDmd [temp_use]], THEN DmdImplE]) 383 apply (rule 3) 384 done 385 386lemma STL6: "\<turnstile> \<diamond>\<box>F \<and> \<diamond>\<box>G \<longrightarrow> \<diamond>\<box>(F \<and> G)" 387 apply (auto simp: STL5 [temp_rewrite, symmetric]) 388 apply (drule linT [temp_use]) 389 apply assumption 390 apply (erule thin_rl) 391 apply (rule DmdDmd [temp_unlift, THEN iffD1]) 392 apply (erule disjE) 393 apply (erule DmdImplE) 394 apply (rule BoxDmd) 395 apply (erule DmdImplE) 396 apply auto 397 apply (drule BoxDmd [temp_use]) 398 apply assumption 399 apply (erule thin_rl) 400 apply (fastforce elim!: DmdImplE [temp_use]) 401 done 402 403 404(* ------------------------ True / False ----------------------------------------- *) 405section "Simplification of constants" 406 407lemma BoxConst: "\<turnstile> (\<box>#P) = #P" 408 apply (rule tempI) 409 apply (cases P) 410 apply (auto intro!: necT [temp_use] dest: STL2_gen [temp_use] simp: Init_simps) 411 done 412 413lemma DmdConst: "\<turnstile> (\<diamond>#P) = #P" 414 apply (unfold dmd_def) 415 apply (cases P) 416 apply (simp_all add: BoxConst [try_rewrite]) 417 done 418 419lemmas temp_simps [temp_rewrite, simp] = BoxConst DmdConst 420 421 422(* ------------------------ Further rewrites ----------------------------------------- *) 423section "Further rewrites" 424 425lemma NotBox: "\<turnstile> (\<not>\<box>F) = (\<diamond>\<not>F)" 426 by (simp add: dmd_def) 427 428lemma NotDmd: "\<turnstile> (\<not>\<diamond>F) = (\<box>\<not>F)" 429 by (simp add: dmd_def) 430 431(* These are not declared by default, because they could be harmful, 432 e.g. \<box>F & \<not>\<box>F becomes \<box>F & \<diamond>\<not>F !! *) 433lemmas more_temp_simps1 = 434 STL3 [temp_rewrite] DmdDmd [temp_rewrite] NotBox [temp_rewrite] NotDmd [temp_rewrite] 435 NotBox [temp_unlift, THEN eq_reflection] 436 NotDmd [temp_unlift, THEN eq_reflection] 437 438lemma BoxDmdBox: "\<turnstile> (\<box>\<diamond>\<box>F) = (\<diamond>\<box>F)" 439 apply (auto dest!: STL2 [temp_use]) 440 apply (rule ccontr) 441 apply (subgoal_tac "sigma \<Turnstile> \<diamond>\<box>\<box>F \<and> \<diamond>\<box>\<not>\<box>F") 442 apply (erule thin_rl) 443 apply auto 444 apply (drule STL6 [temp_use]) 445 apply assumption 446 apply simp 447 apply (simp_all add: more_temp_simps1) 448 done 449 450lemma DmdBoxDmd: "\<turnstile> (\<diamond>\<box>\<diamond>F) = (\<box>\<diamond>F)" 451 apply (unfold dmd_def) 452 apply (auto simp: BoxDmdBox [unfolded dmd_def, try_rewrite]) 453 done 454 455lemmas more_temp_simps2 = more_temp_simps1 BoxDmdBox [temp_rewrite] DmdBoxDmd [temp_rewrite] 456 457 458(* ------------------------ Miscellaneous ----------------------------------- *) 459 460lemma BoxOr: "\<And>sigma. \<lbrakk> sigma \<Turnstile> \<box>F \<or> \<box>G \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>(F \<or> G)" 461 by (fastforce elim!: STL4E [temp_use]) 462 463(* "persistently implies infinitely often" *) 464lemma DBImplBD: "\<turnstile> \<diamond>\<box>F \<longrightarrow> \<box>\<diamond>F" 465 apply clarsimp 466 apply (rule ccontr) 467 apply (simp add: more_temp_simps2) 468 apply (drule STL6 [temp_use]) 469 apply assumption 470 apply simp 471 done 472 473lemma BoxDmdDmdBox: "\<turnstile> \<box>\<diamond>F \<and> \<diamond>\<box>G \<longrightarrow> \<box>\<diamond>(F \<and> G)" 474 apply clarsimp 475 apply (rule ccontr) 476 apply (unfold more_temp_simps2) 477 apply (drule STL6 [temp_use]) 478 apply assumption 479 apply (subgoal_tac "sigma \<Turnstile> \<diamond>\<box>\<not>F") 480 apply (force simp: dmd_def) 481 apply (fastforce elim: DmdImplE [temp_use] STL4E [temp_use]) 482 done 483 484 485(* ------------------------------------------------------------------------- *) 486(*** TLA-specific theorems: primed formulas ***) 487(* ------------------------------------------------------------------------- *) 488section "priming" 489 490(* ------------------------ TLA2 ------------------------------------------- *) 491lemma STL2_pr: "\<turnstile> \<box>P \<longrightarrow> Init P \<and> Init P`" 492 by (fastforce intro!: STL2_gen [temp_use] primeI [temp_use]) 493 494(* Auxiliary lemma allows priming of boxed actions *) 495lemma BoxPrime: "\<turnstile> \<box>P \<longrightarrow> \<box>($P \<and> P$)" 496 apply clarsimp 497 apply (erule dup_boxE) 498 apply (unfold boxInit_act) 499 apply (erule STL4E) 500 apply (auto simp: Init_simps dest!: STL2_pr [temp_use]) 501 done 502 503lemma TLA2: 504 assumes "\<turnstile> $P \<and> P$ \<longrightarrow> A" 505 shows "\<turnstile> \<box>P \<longrightarrow> \<box>A" 506 apply clarsimp 507 apply (drule BoxPrime [temp_use]) 508 apply (auto simp: Init_stp_act_rev [try_rewrite] intro!: assms [temp_use] 509 elim!: STL4E [temp_use]) 510 done 511 512lemma TLA2E: "\<lbrakk> sigma \<Turnstile> \<box>P; \<turnstile> $P \<and> P$ \<longrightarrow> A \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>A" 513 by (erule (1) TLA2 [temp_use]) 514 515lemma DmdPrime: "\<turnstile> (\<diamond>P`) \<longrightarrow> (\<diamond>P)" 516 apply (unfold dmd_def) 517 apply (fastforce elim!: TLA2E [temp_use]) 518 done 519 520lemmas PrimeDmd = InitDmd_gen [temp_use, THEN DmdPrime [temp_use]] 521 522(* ------------------------ INV1, stable --------------------------------------- *) 523section "stable, invariant" 524 525lemma ind_rule: 526 "\<lbrakk> sigma \<Turnstile> \<box>H; sigma \<Turnstile> Init P; \<turnstile> H \<longrightarrow> (Init P \<and> \<not>\<box>F \<longrightarrow> Init(P`) \<and> F) \<rbrakk> 527 \<Longrightarrow> sigma \<Turnstile> \<box>F" 528 apply (rule indT [temp_use]) 529 apply (erule (2) STL4E) 530 done 531 532lemma box_stp_act: "\<turnstile> (\<box>$P) = (\<box>P)" 533 by (simp add: boxInit_act Init_simps) 534 535lemmas box_stp_actI = box_stp_act [temp_use, THEN iffD2] 536lemmas box_stp_actD = box_stp_act [temp_use, THEN iffD1] 537 538lemmas more_temp_simps3 = box_stp_act [temp_rewrite] more_temp_simps2 539 540lemma INV1: 541 "\<turnstile> (Init P) \<longrightarrow> (stable P) \<longrightarrow> \<box>P" 542 apply (unfold stable_def boxInit_stp boxInit_act) 543 apply clarsimp 544 apply (erule ind_rule) 545 apply (auto simp: Init_simps elim: ind_rule) 546 done 547 548lemma StableT: 549 "\<And>P. \<turnstile> $P \<and> A \<longrightarrow> P` \<Longrightarrow> \<turnstile> \<box>A \<longrightarrow> stable P" 550 apply (unfold stable_def) 551 apply (fastforce elim!: STL4E [temp_use]) 552 done 553 554lemma Stable: "\<lbrakk> sigma \<Turnstile> \<box>A; \<turnstile> $P \<and> A \<longrightarrow> P` \<rbrakk> \<Longrightarrow> sigma \<Turnstile> stable P" 555 by (erule (1) StableT [temp_use]) 556 557(* Generalization of INV1 *) 558lemma StableBox: "\<turnstile> (stable P) \<longrightarrow> \<box>(Init P \<longrightarrow> \<box>P)" 559 apply (unfold stable_def) 560 apply clarsimp 561 apply (erule dup_boxE) 562 apply (force simp: stable_def elim: STL4E [temp_use] INV1 [temp_use]) 563 done 564 565lemma DmdStable: "\<turnstile> (stable P) \<and> \<diamond>P \<longrightarrow> \<diamond>\<box>P" 566 apply clarsimp 567 apply (rule DmdImpl2) 568 prefer 2 569 apply (erule StableBox [temp_use]) 570 apply (simp add: dmdInitD) 571 done 572 573(* ---------------- (Semi-)automatic invariant tactics ---------------------- *) 574 575ML \<open> 576(* inv_tac reduces goals of the form ... \<Longrightarrow> sigma \<Turnstile> \<box>P *) 577fun inv_tac ctxt = 578 SELECT_GOAL 579 (EVERY 580 [auto_tac ctxt, 581 TRY (merge_box_tac ctxt 1), 582 resolve_tac ctxt [temp_use ctxt @{thm INV1}] 1, (* fail if the goal is not a box *) 583 TRYALL (eresolve_tac ctxt @{thms Stable})]); 584 585(* auto_inv_tac applies inv_tac and then tries to attack the subgoals 586 in simple cases it may be able to handle goals like \<turnstile> MyProg \<longrightarrow> \<box>Inv. 587 In these simple cases the simplifier seems to be more useful than the 588 auto-tactic, which applies too much propositional logic and simplifies 589 too late. 590*) 591fun auto_inv_tac ctxt = 592 SELECT_GOAL 593 (inv_tac ctxt 1 THEN 594 (TRYALL (action_simp_tac 595 (ctxt addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}]))); 596\<close> 597 598method_setup invariant = \<open> 599 Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o inv_tac)) 600\<close> 601 602method_setup auto_invariant = \<open> 603 Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o auto_inv_tac)) 604\<close> 605 606lemma unless: "\<turnstile> \<box>($P \<longrightarrow> P` \<or> Q`) \<longrightarrow> (stable P) \<or> \<diamond>Q" 607 apply (unfold dmd_def) 608 apply (clarsimp dest!: BoxPrime [temp_use]) 609 apply merge_box 610 apply (erule contrapos_np) 611 apply (fastforce elim!: Stable [temp_use]) 612 done 613 614 615(* --------------------- Recursive expansions --------------------------------------- *) 616section "recursive expansions" 617 618(* Recursive expansions of \<box> and \<diamond> for state predicates *) 619lemma BoxRec: "\<turnstile> (\<box>P) = (Init P \<and> \<box>P`)" 620 apply (auto intro!: STL2_gen [temp_use]) 621 apply (fastforce elim!: TLA2E [temp_use]) 622 apply (auto simp: stable_def elim!: INV1 [temp_use] STL4E [temp_use]) 623 done 624 625lemma DmdRec: "\<turnstile> (\<diamond>P) = (Init P \<or> \<diamond>P`)" 626 apply (unfold dmd_def BoxRec [temp_rewrite]) 627 apply (auto simp: Init_simps) 628 done 629 630lemma DmdRec2: "\<And>sigma. \<lbrakk> sigma \<Turnstile> \<diamond>P; sigma \<Turnstile> \<box>\<not>P` \<rbrakk> \<Longrightarrow> sigma \<Turnstile> Init P" 631 apply (force simp: DmdRec [temp_rewrite] dmd_def) 632 done 633 634lemma InfinitePrime: "\<turnstile> (\<box>\<diamond>P) = (\<box>\<diamond>P`)" 635 apply auto 636 apply (rule classical) 637 apply (rule DBImplBD [temp_use]) 638 apply (subgoal_tac "sigma \<Turnstile> \<diamond>\<box>P") 639 apply (fastforce elim!: DmdImplE [temp_use] TLA2E [temp_use]) 640 apply (subgoal_tac "sigma \<Turnstile> \<diamond>\<box> (\<diamond>P \<and> \<box>\<not>P`)") 641 apply (force simp: boxInit_stp [temp_use] 642 elim!: DmdImplE [temp_use] STL4E [temp_use] DmdRec2 [temp_use]) 643 apply (force intro!: STL6 [temp_use] simp: more_temp_simps3) 644 apply (fastforce intro: DmdPrime [temp_use] elim!: STL4E [temp_use]) 645 done 646 647lemma InfiniteEnsures: 648 "\<lbrakk> sigma \<Turnstile> \<box>N; sigma \<Turnstile> \<box>\<diamond>A; \<turnstile> A \<and> N \<longrightarrow> P` \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>\<diamond>P" 649 apply (unfold InfinitePrime [temp_rewrite]) 650 apply (rule InfImpl) 651 apply assumption+ 652 done 653 654(* ------------------------ fairness ------------------------------------------- *) 655section "fairness" 656 657(* alternative definitions of fairness *) 658lemma WF_alt: "\<turnstile> WF(A)_v = (\<box>\<diamond>\<not>Enabled(<A>_v) \<or> \<box>\<diamond><A>_v)" 659 apply (unfold WF_def dmd_def) 660 apply fastforce 661 done 662 663lemma SF_alt: "\<turnstile> SF(A)_v = (\<diamond>\<box>\<not>Enabled(<A>_v) \<or> \<box>\<diamond><A>_v)" 664 apply (unfold SF_def dmd_def) 665 apply fastforce 666 done 667 668(* theorems to "box" fairness conditions *) 669lemma BoxWFI: "\<turnstile> WF(A)_v \<longrightarrow> \<box>WF(A)_v" 670 by (auto simp: WF_alt [try_rewrite] more_temp_simps3 intro!: BoxOr [temp_use]) 671 672lemma WF_Box: "\<turnstile> (\<box>WF(A)_v) = WF(A)_v" 673 by (fastforce intro!: BoxWFI [temp_use] dest!: STL2 [temp_use]) 674 675lemma BoxSFI: "\<turnstile> SF(A)_v \<longrightarrow> \<box>SF(A)_v" 676 by (auto simp: SF_alt [try_rewrite] more_temp_simps3 intro!: BoxOr [temp_use]) 677 678lemma SF_Box: "\<turnstile> (\<box>SF(A)_v) = SF(A)_v" 679 by (fastforce intro!: BoxSFI [temp_use] dest!: STL2 [temp_use]) 680 681lemmas more_temp_simps = more_temp_simps3 WF_Box [temp_rewrite] SF_Box [temp_rewrite] 682 683lemma SFImplWF: "\<turnstile> SF(A)_v \<longrightarrow> WF(A)_v" 684 apply (unfold SF_def WF_def) 685 apply (fastforce dest!: DBImplBD [temp_use]) 686 done 687 688(* A tactic that "boxes" all fairness conditions. Apply more_temp_simps to "unbox". *) 689ML \<open> 690fun box_fair_tac ctxt = 691 SELECT_GOAL (REPEAT (dresolve_tac ctxt [@{thm BoxWFI}, @{thm BoxSFI}] 1)) 692\<close> 693 694 695(* ------------------------------ leads-to ------------------------------ *) 696 697section "\<leadsto>" 698 699lemma leadsto_init: "\<turnstile> (Init F) \<and> (F \<leadsto> G) \<longrightarrow> \<diamond>G" 700 apply (unfold leadsto_def) 701 apply (auto dest!: STL2 [temp_use]) 702 done 703 704(* \<turnstile> F & (F \<leadsto> G) \<longrightarrow> \<diamond>G *) 705lemmas leadsto_init_temp = leadsto_init [where 'a = behavior, unfolded Init_simps] 706 707lemma streett_leadsto: "\<turnstile> (\<box>\<diamond>Init F \<longrightarrow> \<box>\<diamond>G) = (\<diamond>(F \<leadsto> G))" 708 apply (unfold leadsto_def) 709 apply auto 710 apply (simp add: more_temp_simps) 711 apply (fastforce elim!: DmdImplE [temp_use] STL4E [temp_use]) 712 apply (fastforce intro!: InitDmd [temp_use] elim!: STL4E [temp_use]) 713 apply (subgoal_tac "sigma \<Turnstile> \<box>\<diamond>\<diamond>G") 714 apply (simp add: more_temp_simps) 715 apply (drule BoxDmdDmdBox [temp_use]) 716 apply assumption 717 apply (fastforce elim!: DmdImplE [temp_use] STL4E [temp_use]) 718 done 719 720lemma leadsto_infinite: "\<turnstile> \<box>\<diamond>F \<and> (F \<leadsto> G) \<longrightarrow> \<box>\<diamond>G" 721 apply clarsimp 722 apply (erule InitDmd [temp_use, THEN streett_leadsto [temp_unlift, THEN iffD2, THEN mp]]) 723 apply (simp add: dmdInitD) 724 done 725 726(* In particular, strong fairness is a Streett condition. The following 727 rules are sometimes easier to use than WF2 or SF2 below. 728*) 729lemma leadsto_SF: "\<turnstile> (Enabled(<A>_v) \<leadsto> <A>_v) \<longrightarrow> SF(A)_v" 730 apply (unfold SF_def) 731 apply (clarsimp elim!: leadsto_infinite [temp_use]) 732 done 733 734lemma leadsto_WF: "\<turnstile> (Enabled(<A>_v) \<leadsto> <A>_v) \<longrightarrow> WF(A)_v" 735 by (clarsimp intro!: SFImplWF [temp_use] leadsto_SF [temp_use]) 736 737(* introduce an invariant into the proof of a leadsto assertion. 738 \<box>I \<longrightarrow> ((P \<leadsto> Q) = (P /\ I \<leadsto> Q)) 739*) 740lemma INV_leadsto: "\<turnstile> \<box>I \<and> (P \<and> I \<leadsto> Q) \<longrightarrow> (P \<leadsto> Q)" 741 apply (unfold leadsto_def) 742 apply clarsimp 743 apply (erule STL4Edup) 744 apply assumption 745 apply (auto simp: Init_simps dest!: STL2_gen [temp_use]) 746 done 747 748lemma leadsto_classical: "\<turnstile> (Init F \<and> \<box>\<not>G \<leadsto> G) \<longrightarrow> (F \<leadsto> G)" 749 apply (unfold leadsto_def dmd_def) 750 apply (force simp: Init_simps elim!: STL4E [temp_use]) 751 done 752 753lemma leadsto_false: "\<turnstile> (F \<leadsto> #False) = (\<box>\<not>F)" 754 apply (unfold leadsto_def) 755 apply (simp add: boxNotInitD) 756 done 757 758lemma leadsto_exists: "\<turnstile> ((\<exists>x. F x) \<leadsto> G) = (\<forall>x. (F x \<leadsto> G))" 759 apply (unfold leadsto_def) 760 apply (auto simp: allT [try_rewrite] Init_simps elim!: STL4E [temp_use]) 761 done 762 763(* basic leadsto properties, cf. Unity *) 764 765lemma ImplLeadsto_gen: "\<turnstile> \<box>(Init F \<longrightarrow> Init G) \<longrightarrow> (F \<leadsto> G)" 766 apply (unfold leadsto_def) 767 apply (auto intro!: InitDmd_gen [temp_use] 768 elim!: STL4E_gen [temp_use] simp: Init_simps) 769 done 770 771lemmas ImplLeadsto = 772 ImplLeadsto_gen [where 'a = behavior and 'b = behavior, unfolded Init_simps] 773 774lemma ImplLeadsto_simple: "\<And>F G. \<turnstile> F \<longrightarrow> G \<Longrightarrow> \<turnstile> F \<leadsto> G" 775 by (auto simp: Init_def intro!: ImplLeadsto_gen [temp_use] necT [temp_use]) 776 777lemma EnsuresLeadsto: 778 assumes "\<turnstile> A \<and> $P \<longrightarrow> Q`" 779 shows "\<turnstile> \<box>A \<longrightarrow> (P \<leadsto> Q)" 780 apply (unfold leadsto_def) 781 apply (clarsimp elim!: INV_leadsto [temp_use]) 782 apply (erule STL4E_gen) 783 apply (auto simp: Init_defs intro!: PrimeDmd [temp_use] assms [temp_use]) 784 done 785 786lemma EnsuresLeadsto2: "\<turnstile> \<box>($P \<longrightarrow> Q`) \<longrightarrow> (P \<leadsto> Q)" 787 apply (unfold leadsto_def) 788 apply clarsimp 789 apply (erule STL4E_gen) 790 apply (auto simp: Init_simps intro!: PrimeDmd [temp_use]) 791 done 792 793lemma ensures: 794 assumes 1: "\<turnstile> $P \<and> N \<longrightarrow> P` \<or> Q`" 795 and 2: "\<turnstile> ($P \<and> N) \<and> A \<longrightarrow> Q`" 796 shows "\<turnstile> \<box>N \<and> \<box>(\<box>P \<longrightarrow> \<diamond>A) \<longrightarrow> (P \<leadsto> Q)" 797 apply (unfold leadsto_def) 798 apply clarsimp 799 apply (erule STL4Edup) 800 apply assumption 801 apply clarsimp 802 apply (subgoal_tac "sigmaa \<Turnstile> \<box>($P \<longrightarrow> P` \<or> Q`) ") 803 apply (drule unless [temp_use]) 804 apply (clarsimp dest!: INV1 [temp_use]) 805 apply (rule 2 [THEN DmdImpl, temp_use, THEN DmdPrime [temp_use]]) 806 apply (force intro!: BoxDmd_simple [temp_use] 807 simp: split_box_conj [try_rewrite] box_stp_act [try_rewrite]) 808 apply (force elim: STL4E [temp_use] dest: 1 [temp_use]) 809 done 810 811lemma ensures_simple: 812 "\<lbrakk> \<turnstile> $P \<and> N \<longrightarrow> P` \<or> Q`; 813 \<turnstile> ($P \<and> N) \<and> A \<longrightarrow> Q` 814 \<rbrakk> \<Longrightarrow> \<turnstile> \<box>N \<and> \<box>\<diamond>A \<longrightarrow> (P \<leadsto> Q)" 815 apply clarsimp 816 apply (erule (2) ensures [temp_use]) 817 apply (force elim!: STL4E [temp_use]) 818 done 819 820lemma EnsuresInfinite: 821 "\<lbrakk> sigma \<Turnstile> \<box>\<diamond>P; sigma \<Turnstile> \<box>A; \<turnstile> A \<and> $P \<longrightarrow> Q` \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>\<diamond>Q" 822 apply (erule leadsto_infinite [temp_use]) 823 apply (erule EnsuresLeadsto [temp_use]) 824 apply assumption 825 done 826 827 828(*** Gronning's lattice rules (taken from TLP) ***) 829section "Lattice rules" 830 831lemma LatticeReflexivity: "\<turnstile> F \<leadsto> F" 832 apply (unfold leadsto_def) 833 apply (rule necT InitDmd_gen)+ 834 done 835 836lemma LatticeTransitivity: "\<turnstile> (G \<leadsto> H) \<and> (F \<leadsto> G) \<longrightarrow> (F \<leadsto> H)" 837 apply (unfold leadsto_def) 838 apply clarsimp 839 apply (erule dup_boxE) (* \<box>\<box>(Init G \<longrightarrow> H) *) 840 apply merge_box 841 apply (clarsimp elim!: STL4E [temp_use]) 842 apply (rule dup_dmdD) 843 apply (subgoal_tac "sigmaa \<Turnstile> \<diamond>Init G") 844 apply (erule DmdImpl2) 845 apply assumption 846 apply (simp add: dmdInitD) 847 done 848 849lemma LatticeDisjunctionElim1: "\<turnstile> (F \<or> G \<leadsto> H) \<longrightarrow> (F \<leadsto> H)" 850 apply (unfold leadsto_def) 851 apply (auto simp: Init_simps elim!: STL4E [temp_use]) 852 done 853 854lemma LatticeDisjunctionElim2: "\<turnstile> (F \<or> G \<leadsto> H) \<longrightarrow> (G \<leadsto> H)" 855 apply (unfold leadsto_def) 856 apply (auto simp: Init_simps elim!: STL4E [temp_use]) 857 done 858 859lemma LatticeDisjunctionIntro: "\<turnstile> (F \<leadsto> H) \<and> (G \<leadsto> H) \<longrightarrow> (F \<or> G \<leadsto> H)" 860 apply (unfold leadsto_def) 861 apply clarsimp 862 apply merge_box 863 apply (auto simp: Init_simps elim!: STL4E [temp_use]) 864 done 865 866lemma LatticeDisjunction: "\<turnstile> (F \<or> G \<leadsto> H) = ((F \<leadsto> H) \<and> (G \<leadsto> H))" 867 by (auto intro: LatticeDisjunctionIntro [temp_use] 868 LatticeDisjunctionElim1 [temp_use] 869 LatticeDisjunctionElim2 [temp_use]) 870 871lemma LatticeDiamond: "\<turnstile> (A \<leadsto> B \<or> C) \<and> (B \<leadsto> D) \<and> (C \<leadsto> D) \<longrightarrow> (A \<leadsto> D)" 872 apply clarsimp 873 apply (subgoal_tac "sigma \<Turnstile> (B \<or> C) \<leadsto> D") 874 apply (erule_tac G = "LIFT (B \<or> C)" in LatticeTransitivity [temp_use]) 875 apply (fastforce intro!: LatticeDisjunctionIntro [temp_use])+ 876 done 877 878lemma LatticeTriangle: "\<turnstile> (A \<leadsto> D \<or> B) \<and> (B \<leadsto> D) \<longrightarrow> (A \<leadsto> D)" 879 apply clarsimp 880 apply (subgoal_tac "sigma \<Turnstile> (D \<or> B) \<leadsto> D") 881 apply (erule_tac G = "LIFT (D \<or> B)" in LatticeTransitivity [temp_use]) 882 apply assumption 883 apply (auto intro: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use]) 884 done 885 886lemma LatticeTriangle2: "\<turnstile> (A \<leadsto> B \<or> D) \<and> (B \<leadsto> D) \<longrightarrow> (A \<leadsto> D)" 887 apply clarsimp 888 apply (subgoal_tac "sigma \<Turnstile> B \<or> D \<leadsto> D") 889 apply (erule_tac G = "LIFT (B \<or> D)" in LatticeTransitivity [temp_use]) 890 apply assumption 891 apply (auto intro: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use]) 892 done 893 894(*** Lamport's fairness rules ***) 895section "Fairness rules" 896 897lemma WF1: 898 "\<lbrakk> \<turnstile> $P \<and> N \<longrightarrow> P` \<or> Q`; 899 \<turnstile> ($P \<and> N) \<and> <A>_v \<longrightarrow> Q`; 900 \<turnstile> $P \<and> N \<longrightarrow> $(Enabled(<A>_v)) \<rbrakk> 901 \<Longrightarrow> \<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> (P \<leadsto> Q)" 902 apply (clarsimp dest!: BoxWFI [temp_use]) 903 apply (erule (2) ensures [temp_use]) 904 apply (erule (1) STL4Edup) 905 apply (clarsimp simp: WF_def) 906 apply (rule STL2 [temp_use]) 907 apply (clarsimp elim!: mp intro!: InitDmd [temp_use]) 908 apply (erule STL4 [temp_use, THEN box_stp_actD [temp_use]]) 909 apply (simp add: split_box_conj box_stp_actI) 910 done 911 912(* Sometimes easier to use; designed for action B rather than state predicate Q *) 913lemma WF_leadsto: 914 assumes 1: "\<turnstile> N \<and> $P \<longrightarrow> $Enabled (<A>_v)" 915 and 2: "\<turnstile> N \<and> <A>_v \<longrightarrow> B" 916 and 3: "\<turnstile> \<box>(N \<and> [\<not>A]_v) \<longrightarrow> stable P" 917 shows "\<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> (P \<leadsto> B)" 918 apply (unfold leadsto_def) 919 apply (clarsimp dest!: BoxWFI [temp_use]) 920 apply (erule (1) STL4Edup) 921 apply clarsimp 922 apply (rule 2 [THEN DmdImpl, temp_use]) 923 apply (rule BoxDmd_simple [temp_use]) 924 apply assumption 925 apply (rule classical) 926 apply (rule STL2 [temp_use]) 927 apply (clarsimp simp: WF_def elim!: mp intro!: InitDmd [temp_use]) 928 apply (rule 1 [THEN STL4, temp_use, THEN box_stp_actD]) 929 apply (simp (no_asm_simp) add: split_box_conj [try_rewrite] box_stp_act [try_rewrite]) 930 apply (erule INV1 [temp_use]) 931 apply (rule 3 [temp_use]) 932 apply (simp add: split_box_conj [try_rewrite] NotDmd [temp_use] not_angle [try_rewrite]) 933 done 934 935lemma SF1: 936 "\<lbrakk> \<turnstile> $P \<and> N \<longrightarrow> P` \<or> Q`; 937 \<turnstile> ($P \<and> N) \<and> <A>_v \<longrightarrow> Q`; 938 \<turnstile> \<box>P \<and> \<box>N \<and> \<box>F \<longrightarrow> \<diamond>Enabled(<A>_v) \<rbrakk> 939 \<Longrightarrow> \<turnstile> \<box>N \<and> SF(A)_v \<and> \<box>F \<longrightarrow> (P \<leadsto> Q)" 940 apply (clarsimp dest!: BoxSFI [temp_use]) 941 apply (erule (2) ensures [temp_use]) 942 apply (erule_tac F = F in dup_boxE) 943 apply merge_temp_box 944 apply (erule STL4Edup) 945 apply assumption 946 apply (clarsimp simp: SF_def) 947 apply (rule STL2 [temp_use]) 948 apply (erule mp) 949 apply (erule STL4 [temp_use]) 950 apply (simp add: split_box_conj [try_rewrite] STL3 [try_rewrite]) 951 done 952 953lemma WF2: 954 assumes 1: "\<turnstile> N \<and> <B>_f \<longrightarrow> <M>_g" 955 and 2: "\<turnstile> $P \<and> P` \<and> <N \<and> A>_f \<longrightarrow> B" 956 and 3: "\<turnstile> P \<and> Enabled(<M>_g) \<longrightarrow> Enabled(<A>_f)" 957 and 4: "\<turnstile> \<box>(N \<and> [\<not>B]_f) \<and> WF(A)_f \<and> \<box>F \<and> \<diamond>\<box>Enabled(<M>_g) \<longrightarrow> \<diamond>\<box>P" 958 shows "\<turnstile> \<box>N \<and> WF(A)_f \<and> \<box>F \<longrightarrow> WF(M)_g" 959 apply (clarsimp dest!: BoxWFI [temp_use] BoxDmdBox [temp_use, THEN iffD2] 960 simp: WF_def [where A = M]) 961 apply (erule_tac F = F in dup_boxE) 962 apply merge_temp_box 963 apply (erule STL4Edup) 964 apply assumption 965 apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]]) 966 apply (rule classical) 967 apply (subgoal_tac "sigmaa \<Turnstile> \<diamond> (($P \<and> P` \<and> N) \<and> <A>_f)") 968 apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use]) 969 apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use]) 970 apply (simp add: NotDmd [temp_use] not_angle [try_rewrite]) 971 apply merge_act_box 972 apply (frule 4 [temp_use]) 973 apply assumption+ 974 apply (drule STL6 [temp_use]) 975 apply assumption 976 apply (erule_tac V = "sigmaa \<Turnstile> \<diamond>\<box>P" in thin_rl) 977 apply (erule_tac V = "sigmaa \<Turnstile> \<box>F" in thin_rl) 978 apply (drule BoxWFI [temp_use]) 979 apply (erule_tac F = "ACT N \<and> [\<not>B]_f" in dup_boxE) 980 apply merge_temp_box 981 apply (erule DmdImpldup) 982 apply assumption 983 apply (auto simp: split_box_conj [try_rewrite] STL3 [try_rewrite] 984 WF_Box [try_rewrite] box_stp_act [try_rewrite]) 985 apply (force elim!: TLA2E [where P = P, temp_use]) 986 apply (rule STL2 [temp_use]) 987 apply (force simp: WF_def split_box_conj [try_rewrite] 988 elim!: mp intro!: InitDmd [temp_use] 3 [THEN STL4, temp_use]) 989 done 990 991lemma SF2: 992 assumes 1: "\<turnstile> N \<and> <B>_f \<longrightarrow> <M>_g" 993 and 2: "\<turnstile> $P \<and> P` \<and> <N \<and> A>_f \<longrightarrow> B" 994 and 3: "\<turnstile> P \<and> Enabled(<M>_g) \<longrightarrow> Enabled(<A>_f)" 995 and 4: "\<turnstile> \<box>(N \<and> [\<not>B]_f) \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled(<M>_g) \<longrightarrow> \<diamond>\<box>P" 996 shows "\<turnstile> \<box>N \<and> SF(A)_f \<and> \<box>F \<longrightarrow> SF(M)_g" 997 apply (clarsimp dest!: BoxSFI [temp_use] simp: 2 [try_rewrite] SF_def [where A = M]) 998 apply (erule_tac F = F in dup_boxE) 999 apply (erule_tac F = "TEMP \<diamond>Enabled (<M>_g) " in dup_boxE) 1000 apply merge_temp_box 1001 apply (erule STL4Edup) 1002 apply assumption 1003 apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]]) 1004 apply (rule classical) 1005 apply (subgoal_tac "sigmaa \<Turnstile> \<diamond> (($P \<and> P` \<and> N) \<and> <A>_f)") 1006 apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use]) 1007 apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use]) 1008 apply (simp add: NotDmd [temp_use] not_angle [try_rewrite]) 1009 apply merge_act_box 1010 apply (frule 4 [temp_use]) 1011 apply assumption+ 1012 apply (erule_tac V = "sigmaa \<Turnstile> \<box>F" in thin_rl) 1013 apply (drule BoxSFI [temp_use]) 1014 apply (erule_tac F = "TEMP \<diamond>Enabled (<M>_g)" in dup_boxE) 1015 apply (erule_tac F = "ACT N \<and> [\<not>B]_f" in dup_boxE) 1016 apply merge_temp_box 1017 apply (erule DmdImpldup) 1018 apply assumption 1019 apply (auto simp: split_box_conj [try_rewrite] STL3 [try_rewrite] 1020 SF_Box [try_rewrite] box_stp_act [try_rewrite]) 1021 apply (force elim!: TLA2E [where P = P, temp_use]) 1022 apply (rule STL2 [temp_use]) 1023 apply (force simp: SF_def split_box_conj [try_rewrite] 1024 elim!: mp InfImpl [temp_use] intro!: 3 [temp_use]) 1025 done 1026 1027(* ------------------------------------------------------------------------- *) 1028(*** Liveness proofs by well-founded orderings ***) 1029(* ------------------------------------------------------------------------- *) 1030section "Well-founded orderings" 1031 1032lemma wf_leadsto: 1033 assumes 1: "wf r" 1034 and 2: "\<And>x. sigma \<Turnstile> F x \<leadsto> (G \<or> (\<exists>y. #((y,x)\<in>r) \<and> F y)) " 1035 shows "sigma \<Turnstile> F x \<leadsto> G" 1036 apply (rule 1 [THEN wf_induct]) 1037 apply (rule LatticeTriangle [temp_use]) 1038 apply (rule 2) 1039 apply (auto simp: leadsto_exists [try_rewrite]) 1040 apply (case_tac "(y,x) \<in> r") 1041 apply force 1042 apply (force simp: leadsto_def Init_simps intro!: necT [temp_use]) 1043 done 1044 1045(* If r is well-founded, state function v cannot decrease forever *) 1046lemma wf_not_box_decrease: "\<And>r. wf r \<Longrightarrow> \<turnstile> \<box>[ (v`, $v) \<in> #r ]_v \<longrightarrow> \<diamond>\<box>[#False]_v" 1047 apply clarsimp 1048 apply (rule ccontr) 1049 apply (subgoal_tac "sigma \<Turnstile> (\<exists>x. v=#x) \<leadsto> #False") 1050 apply (drule leadsto_false [temp_use, THEN iffD1, THEN STL2_gen [temp_use]]) 1051 apply (force simp: Init_defs) 1052 apply (clarsimp simp: leadsto_exists [try_rewrite] not_square [try_rewrite] more_temp_simps) 1053 apply (erule wf_leadsto) 1054 apply (rule ensures_simple [temp_use]) 1055 apply (auto simp: square_def angle_def) 1056 done 1057 1058(* "wf r \<Longrightarrow> \<turnstile> \<diamond>\<box>[ (v`, $v) : #r ]_v \<longrightarrow> \<diamond>\<box>[#False]_v" *) 1059lemmas wf_not_dmd_box_decrease = 1060 wf_not_box_decrease [THEN DmdImpl, unfolded more_temp_simps] 1061 1062(* If there are infinitely many steps where v decreases, then there 1063 have to be infinitely many non-stuttering steps where v doesn't decrease. 1064*) 1065lemma wf_box_dmd_decrease: 1066 assumes 1: "wf r" 1067 shows "\<turnstile> \<box>\<diamond>((v`, $v) \<in> #r) \<longrightarrow> \<box>\<diamond><(v`, $v) \<notin> #r>_v" 1068 apply clarsimp 1069 apply (rule ccontr) 1070 apply (simp add: not_angle [try_rewrite] more_temp_simps) 1071 apply (drule 1 [THEN wf_not_dmd_box_decrease [temp_use]]) 1072 apply (drule BoxDmdDmdBox [temp_use]) 1073 apply assumption 1074 apply (subgoal_tac "sigma \<Turnstile> \<box>\<diamond> ((#False) ::action)") 1075 apply force 1076 apply (erule STL4E) 1077 apply (rule DmdImpl) 1078 apply (force intro: 1 [THEN wf_irrefl, temp_use]) 1079 done 1080 1081(* In particular, for natural numbers, if n decreases infinitely often 1082 then it has to increase infinitely often. 1083*) 1084lemma nat_box_dmd_decrease: "\<And>n::nat stfun. \<turnstile> \<box>\<diamond>(n` < $n) \<longrightarrow> \<box>\<diamond>($n < n`)" 1085 apply clarsimp 1086 apply (subgoal_tac "sigma \<Turnstile> \<box>\<diamond><\<not> ((n`,$n) \<in> #less_than)>_n") 1087 apply (erule thin_rl) 1088 apply (erule STL4E) 1089 apply (rule DmdImpl) 1090 apply (clarsimp simp: angle_def [try_rewrite]) 1091 apply (rule wf_box_dmd_decrease [temp_use]) 1092 apply (auto elim!: STL4E [temp_use] DmdImplE [temp_use]) 1093 done 1094 1095 1096(* ------------------------------------------------------------------------- *) 1097(*** Flexible quantification over state variables ***) 1098(* ------------------------------------------------------------------------- *) 1099section "Flexible quantification" 1100 1101lemma aallI: 1102 assumes 1: "basevars vs" 1103 and 2: "(\<And>x. basevars (x,vs) \<Longrightarrow> sigma \<Turnstile> F x)" 1104 shows "sigma \<Turnstile> (\<forall>\<forall>x. F x)" 1105 by (auto simp: aall_def elim!: eexE [temp_use] intro!: 1 dest!: 2 [temp_use]) 1106 1107lemma aallE: "\<turnstile> (\<forall>\<forall>x. F x) \<longrightarrow> F x" 1108 apply (unfold aall_def) 1109 apply clarsimp 1110 apply (erule contrapos_np) 1111 apply (force intro!: eexI [temp_use]) 1112 done 1113 1114(* monotonicity of quantification *) 1115lemma eex_mono: 1116 assumes 1: "sigma \<Turnstile> \<exists>\<exists>x. F x" 1117 and 2: "\<And>x. sigma \<Turnstile> F x \<longrightarrow> G x" 1118 shows "sigma \<Turnstile> \<exists>\<exists>x. G x" 1119 apply (rule unit_base [THEN 1 [THEN eexE]]) 1120 apply (rule eexI [temp_use]) 1121 apply (erule 2 [unfolded intensional_rews, THEN mp]) 1122 done 1123 1124lemma aall_mono: 1125 assumes 1: "sigma \<Turnstile> \<forall>\<forall>x. F(x)" 1126 and 2: "\<And>x. sigma \<Turnstile> F(x) \<longrightarrow> G(x)" 1127 shows "sigma \<Turnstile> \<forall>\<forall>x. G(x)" 1128 apply (rule unit_base [THEN aallI]) 1129 apply (rule 2 [unfolded intensional_rews, THEN mp]) 1130 apply (rule 1 [THEN aallE [temp_use]]) 1131 done 1132 1133(* Derived history introduction rule *) 1134lemma historyI: 1135 assumes 1: "sigma \<Turnstile> Init I" 1136 and 2: "sigma \<Turnstile> \<box>N" 1137 and 3: "basevars vs" 1138 and 4: "\<And>h. basevars(h,vs) \<Longrightarrow> \<turnstile> I \<and> h = ha \<longrightarrow> HI h" 1139 and 5: "\<And>h s t. \<lbrakk> basevars(h,vs); N (s,t); h t = hb (h s) (s,t) \<rbrakk> \<Longrightarrow> HN h (s,t)" 1140 shows "sigma \<Turnstile> \<exists>\<exists>h. Init (HI h) \<and> \<box>(HN h)" 1141 apply (rule history [temp_use, THEN eexE]) 1142 apply (rule 3) 1143 apply (rule eexI [temp_use]) 1144 apply clarsimp 1145 apply (rule conjI) 1146 prefer 2 1147 apply (insert 2) 1148 apply merge_box 1149 apply (force elim!: STL4E [temp_use] 5 [temp_use]) 1150 apply (insert 1) 1151 apply (force simp: Init_defs elim!: 4 [temp_use]) 1152 done 1153 1154(* ---------------------------------------------------------------------- 1155 example of a history variable: existence of a clock 1156*) 1157 1158lemma "\<turnstile> \<exists>\<exists>h. Init(h = #True) \<and> \<box>(h` = (\<not>$h))" 1159 apply (rule tempI) 1160 apply (rule historyI) 1161 apply (force simp: Init_defs intro!: unit_base [temp_use] necT [temp_use])+ 1162 done 1163 1164end 1165