src/HOL/TLA/TLA.thy
 changeset 21624 6f79647cf536 parent 17309 c43ed29bd197 child 26305 651371f29e00
```     1.1 --- a/src/HOL/TLA/TLA.thy	Fri Dec 01 17:22:33 2006 +0100
1.2 +++ b/src/HOL/TLA/TLA.thy	Sat Dec 02 02:52:02 2006 +0100
1.3 @@ -3,12 +3,9 @@
1.4      ID:          \$Id\$
1.5      Author:      Stephan Merz
1.6      Copyright:   1998 University of Munich
1.7 +*)
1.8
1.9 -    Theory Name: TLA
1.10 -    Logic Image: HOL
1.11 -
1.12 -The temporal level of TLA.
1.13 -*)
1.14 +header {* The temporal level of TLA *}
1.15
1.16  theory TLA
1.17  imports Init
1.18 @@ -99,6 +96,1108 @@
1.19                |] ==> G sigma"
1.20    history:    "|- EEX h. Init(h = ha) & [](!x. \$h = #x --> h` = hb x)"
1.21
1.22 -ML {* use_legacy_bindings (the_context ()) *}
1.23 +
1.24 +(* Specialize intensional introduction/elimination rules for temporal formulas *)
1.25 +
1.26 +lemma tempI: "(!!sigma. sigma |= (F::temporal)) ==> |- F"
1.27 +  apply (rule intI)
1.28 +  apply (erule meta_spec)
1.29 +  done
1.30 +
1.31 +lemma tempD: "|- (F::temporal) ==> sigma |= F"
1.32 +  by (erule intD)
1.33 +
1.34 +
1.35 +(* ======== Functions to "unlift" temporal theorems ====== *)
1.36 +
1.37 +ML {*
1.38 +(* The following functions are specialized versions of the corresponding
1.39 +   functions defined in theory Intensional in that they introduce a
1.40 +   "world" parameter of type "behavior".
1.41 +*)
1.42 +local
1.43 +  val action_rews = thms "action_rews";
1.44 +  val tempD = thm "tempD";
1.45 +in
1.46 +
1.47 +fun temp_unlift th =
1.48 +  (rewrite_rule action_rews (th RS tempD)) handle THM _ => action_unlift th;
1.49 +
1.50 +(* Turn  |- F = G  into meta-level rewrite rule  F == G *)
1.51 +val temp_rewrite = int_rewrite
1.52 +
1.53 +fun temp_use th =
1.54 +  case (concl_of th) of
1.55 +    Const _ \$ (Const ("Intensional.Valid", _) \$ _) =>
1.56 +            ((flatten (temp_unlift th)) handle THM _ => th)
1.57 +  | _ => th;
1.58 +
1.59 +fun try_rewrite th = temp_rewrite th handle THM _ => temp_use th;
1.60 +
1.61 +end
1.62 +*}
1.63 +
1.64 +setup {*
1.66 +    ("temp_unlift", Attrib.no_args (Thm.rule_attribute (K temp_unlift)), ""),
1.67 +    ("temp_rewrite", Attrib.no_args (Thm.rule_attribute (K temp_rewrite)), ""),
1.68 +    ("temp_use", Attrib.no_args (Thm.rule_attribute (K temp_use)), ""),
1.69 +    ("try_rewrite", Attrib.no_args (Thm.rule_attribute (K try_rewrite)), "")]
1.70 +*}
1.71 +
1.72 +(* Update classical reasoner---will be updated once more below! *)
1.73 +
1.74 +declare tempI [intro!]
1.75 +declare tempD [dest]
1.76 +ML {*
1.77 +val temp_css = (claset(), simpset())
1.78 +val temp_cs = op addss temp_css
1.79 +*}
1.80 +
1.81 +(* Modify the functions that add rules to simpsets, classical sets,
1.82 +   and clasimpsets in order to accept "lifted" theorems
1.83 +*)
1.84 +
1.85 +(* ------------------------------------------------------------------------- *)
1.86 +(***           "Simple temporal logic": only [] and <>                     ***)
1.87 +(* ------------------------------------------------------------------------- *)
1.88 +section "Simple temporal logic"
1.89 +
1.90 +(* []~F == []~Init F *)
1.91 +lemmas boxNotInit = boxInit [of "LIFT ~F", unfolded Init_simps, standard]
1.92 +
1.93 +lemma dmdInit: "TEMP <>F == TEMP <> Init F"
1.94 +  apply (unfold dmd_def)
1.95 +  apply (unfold boxInit [of "LIFT ~F"])
1.96 +  apply (simp (no_asm) add: Init_simps)
1.97 +  done
1.98 +
1.99 +lemmas dmdNotInit = dmdInit [of "LIFT ~F", unfolded Init_simps, standard]
1.100 +
1.101 +(* boxInit and dmdInit cannot be used as rewrites, because they loop.
1.102 +   Non-looping instances for state predicates and actions are occasionally useful.
1.103 +*)
1.104 +lemmas boxInit_stp = boxInit [where 'a = state, standard]
1.105 +lemmas boxInit_act = boxInit [where 'a = "state * state", standard]
1.106 +lemmas dmdInit_stp = dmdInit [where 'a = state, standard]
1.107 +lemmas dmdInit_act = dmdInit [where 'a = "state * state", standard]
1.108 +
1.109 +(* The symmetric equations can be used to get rid of Init *)
1.110 +lemmas boxInitD = boxInit [symmetric]
1.111 +lemmas dmdInitD = dmdInit [symmetric]
1.112 +lemmas boxNotInitD = boxNotInit [symmetric]
1.113 +lemmas dmdNotInitD = dmdNotInit [symmetric]
1.114 +
1.115 +lemmas Init_simps = Init_simps boxInitD dmdInitD boxNotInitD dmdNotInitD
1.116 +
1.117 +(* ------------------------ STL2 ------------------------------------------- *)
1.118 +lemmas STL2 = reflT
1.119 +
1.120 +(* The "polymorphic" (generic) variant *)
1.121 +lemma STL2_gen: "|- []F --> Init F"
1.122 +  apply (unfold boxInit [of F])
1.123 +  apply (rule STL2)
1.124 +  done
1.125 +
1.126 +(* see also STL2_pr below: "|- []P --> Init P & Init (P`)" *)
1.127 +
1.128 +
1.129 +(* Dual versions for <> *)
1.130 +lemma InitDmd: "|- F --> <> F"
1.131 +  apply (unfold dmd_def)
1.132 +  apply (auto dest!: STL2 [temp_use])
1.133 +  done
1.134 +
1.135 +lemma InitDmd_gen: "|- Init F --> <>F"
1.136 +  apply clarsimp
1.137 +  apply (drule InitDmd [temp_use])
1.138 +  apply (simp add: dmdInitD)
1.139 +  done
1.140 +
1.141 +
1.142 +(* ------------------------ STL3 ------------------------------------------- *)
1.143 +lemma STL3: "|- ([][]F) = ([]F)"
1.144 +  by (auto elim: transT [temp_use] STL2 [temp_use])
1.145 +
1.146 +(* corresponding elimination rule introduces double boxes:
1.147 +   [| (sigma |= []F); (sigma |= [][]F) ==> PROP W |] ==> PROP W
1.148 +*)
1.149 +lemmas dup_boxE = STL3 [temp_unlift, THEN iffD2, elim_format]
1.150 +lemmas dup_boxD = STL3 [temp_unlift, THEN iffD1, standard]
1.151 +
1.152 +(* dual versions for <> *)
1.153 +lemma DmdDmd: "|- (<><>F) = (<>F)"
1.154 +  by (auto simp add: dmd_def [try_rewrite] STL3 [try_rewrite])
1.155 +
1.156 +lemmas dup_dmdE = DmdDmd [temp_unlift, THEN iffD2, elim_format]
1.157 +lemmas dup_dmdD = DmdDmd [temp_unlift, THEN iffD1, standard]
1.158 +
1.159 +
1.160 +(* ------------------------ STL4 ------------------------------------------- *)
1.161 +lemma STL4:
1.162 +  assumes "|- F --> G"
1.163 +  shows "|- []F --> []G"
1.164 +  apply clarsimp
1.165 +  apply (rule normalT [temp_use])
1.166 +   apply (rule assms [THEN necT, temp_use])
1.167 +  apply assumption
1.168 +  done
1.169 +
1.170 +(* Unlifted version as an elimination rule *)
1.171 +lemma STL4E: "[| sigma |= []F; |- F --> G |] ==> sigma |= []G"
1.172 +  by (erule (1) STL4 [temp_use])
1.173 +
1.174 +lemma STL4_gen: "|- Init F --> Init G ==> |- []F --> []G"
1.175 +  apply (drule STL4)
1.176 +  apply (simp add: boxInitD)
1.177 +  done
1.178 +
1.179 +lemma STL4E_gen: "[| sigma |= []F; |- Init F --> Init G |] ==> sigma |= []G"
1.180 +  by (erule (1) STL4_gen [temp_use])
1.181 +
1.182 +(* see also STL4Edup below, which allows an auxiliary boxed formula:
1.183 +       []A /\ F => G
1.184 +     -----------------
1.185 +     []A /\ []F => []G
1.186 +*)
1.187 +
1.188 +(* The dual versions for <> *)
1.189 +lemma DmdImpl:
1.190 +  assumes prem: "|- F --> G"
1.191 +  shows "|- <>F --> <>G"
1.192 +  apply (unfold dmd_def)
1.193 +  apply (fastsimp intro!: prem [temp_use] elim!: STL4E [temp_use])
1.194 +  done
1.195 +
1.196 +lemma DmdImplE: "[| sigma |= <>F; |- F --> G |] ==> sigma |= <>G"
1.197 +  by (erule (1) DmdImpl [temp_use])
1.198 +
1.199 +(* ------------------------ STL5 ------------------------------------------- *)
1.200 +lemma STL5: "|- ([]F & []G) = ([](F & G))"
1.201 +  apply auto
1.202 +  apply (subgoal_tac "sigma |= [] (G --> (F & G))")
1.203 +     apply (erule normalT [temp_use])
1.204 +     apply (fastsimp elim!: STL4E [temp_use])+
1.205 +  done
1.206 +
1.207 +(* rewrite rule to split conjunctions under boxes *)
1.208 +lemmas split_box_conj = STL5 [temp_unlift, symmetric, standard]
1.209 +
1.210 +
1.211 +(* the corresponding elimination rule allows to combine boxes in the hypotheses
1.212 +   (NB: F and G must have the same type, i.e., both actions or temporals.)
1.213 +   Use "addSE2" etc. if you want to add this to a claset, otherwise it will loop!
1.214 +*)
1.215 +lemma box_conjE:
1.216 +  assumes "sigma |= []F"
1.217 +     and "sigma |= []G"
1.218 +  and "sigma |= [](F&G) ==> PROP R"
1.219 +  shows "PROP R"
1.220 +  by (rule assms STL5 [temp_unlift, THEN iffD1] conjI)+
1.221 +
1.222 +(* Instances of box_conjE for state predicates, actions, and temporals
1.223 +   in case the general rule is "too polymorphic".
1.224 +*)
1.225 +lemmas box_conjE_temp = box_conjE [where 'a = behavior, standard]
1.226 +lemmas box_conjE_stp = box_conjE [where 'a = state, standard]
1.227 +lemmas box_conjE_act = box_conjE [where 'a = "state * state", standard]
1.228 +
1.229 +(* Define a tactic that tries to merge all boxes in an antecedent. The definition is
1.230 +   a bit kludgy in order to simulate "double elim-resolution".
1.231 +*)
1.232 +
1.233 +lemma box_thin: "[| sigma |= []F; PROP W |] ==> PROP W" .
1.234 +
1.235 +ML {*
1.236 +local
1.237 +  val box_conjE = thm "box_conjE";
1.238 +  val box_thin = thm "box_thin";
1.239 +  val box_conjE_temp = thm "box_conjE_temp";
1.240 +  val box_conjE_stp = thm "box_conjE_stp";
1.241 +  val box_conjE_act = thm "box_conjE_act";
1.242 +in
1.243 +
1.244 +fun merge_box_tac i =
1.245 +   REPEAT_DETERM (EVERY [etac box_conjE i, atac i, etac box_thin i])
1.246 +
1.247 +fun merge_temp_box_tac i =
1.248 +   REPEAT_DETERM (EVERY [etac box_conjE_temp i, atac i,
1.249 +                         eres_inst_tac [("'a","behavior")] box_thin i])
1.250 +
1.251 +fun merge_stp_box_tac i =
1.252 +   REPEAT_DETERM (EVERY [etac box_conjE_stp i, atac i,
1.253 +                         eres_inst_tac [("'a","state")] box_thin i])
1.254 +
1.255 +fun merge_act_box_tac i =
1.256 +   REPEAT_DETERM (EVERY [etac box_conjE_act i, atac i,
1.257 +                         eres_inst_tac [("'a","state * state")] box_thin i])
1.258
1.259  end
1.260 +*}
1.261 +
1.262 +(* rewrite rule to push universal quantification through box:
1.263 +      (sigma |= [](! x. F x)) = (! x. (sigma |= []F x))
1.264 +*)
1.265 +lemmas all_box = allT [temp_unlift, symmetric, standard]
1.266 +
1.267 +lemma DmdOr: "|- (<>(F | G)) = (<>F | <>G)"
1.268 +  apply (auto simp add: dmd_def split_box_conj [try_rewrite])
1.269 +  apply (erule contrapos_np, tactic "merge_box_tac 1",
1.270 +    fastsimp elim!: STL4E [temp_use])+
1.271 +  done
1.272 +
1.273 +lemma exT: "|- (EX x. <>(F x)) = (<>(EX x. F x))"
1.274 +  by (auto simp: dmd_def Not_Rex [try_rewrite] all_box [try_rewrite])
1.275 +
1.276 +lemmas ex_dmd = exT [temp_unlift, symmetric, standard]
1.277 +
1.278 +lemma STL4Edup: "!!sigma. [| sigma |= []A; sigma |= []F; |- F & []A --> G |] ==> sigma |= []G"
1.279 +  apply (erule dup_boxE)
1.280 +  apply (tactic "merge_box_tac 1")
1.281 +  apply (erule STL4E)
1.282 +  apply assumption
1.283 +  done
1.284 +
1.285 +lemma DmdImpl2:
1.286 +    "!!sigma. [| sigma |= <>F; sigma |= [](F --> G) |] ==> sigma |= <>G"
1.287 +  apply (unfold dmd_def)
1.288 +  apply auto
1.289 +  apply (erule notE)
1.290 +  apply (tactic "merge_box_tac 1")
1.291 +  apply (fastsimp elim!: STL4E [temp_use])
1.292 +  done
1.293 +
1.294 +lemma InfImpl:
1.295 +  assumes 1: "sigma |= []<>F"
1.296 +    and 2: "sigma |= []G"
1.297 +    and 3: "|- F & G --> H"
1.298 +  shows "sigma |= []<>H"
1.299 +  apply (insert 1 2)
1.300 +  apply (erule_tac F = G in dup_boxE)
1.301 +  apply (tactic "merge_box_tac 1")
1.302 +  apply (fastsimp elim!: STL4E [temp_use] DmdImpl2 [temp_use] intro!: 3 [temp_use])
1.303 +  done
1.304 +
1.305 +(* ------------------------ STL6 ------------------------------------------- *)
1.306 +(* Used in the proof of STL6, but useful in itself. *)
1.307 +lemma BoxDmd: "|- []F & <>G --> <>([]F & G)"
1.308 +  apply (unfold dmd_def)
1.309 +  apply clarsimp
1.310 +  apply (erule dup_boxE)
1.311 +  apply (tactic "merge_box_tac 1")
1.312 +  apply (erule contrapos_np)
1.313 +  apply (fastsimp elim!: STL4E [temp_use])
1.314 +  done
1.315 +
1.316 +(* weaker than BoxDmd, but more polymorphic (and often just right) *)
1.317 +lemma BoxDmd_simple: "|- []F & <>G --> <>(F & G)"
1.318 +  apply (unfold dmd_def)
1.319 +  apply clarsimp
1.320 +  apply (tactic "merge_box_tac 1")
1.321 +  apply (fastsimp elim!: notE STL4E [temp_use])
1.322 +  done
1.323 +
1.324 +lemma BoxDmd2_simple: "|- []F & <>G --> <>(G & F)"
1.325 +  apply (unfold dmd_def)
1.326 +  apply clarsimp
1.327 +  apply (tactic "merge_box_tac 1")
1.328 +  apply (fastsimp elim!: notE STL4E [temp_use])
1.329 +  done
1.330 +
1.331 +lemma DmdImpldup:
1.332 +  assumes 1: "sigma |= []A"
1.333 +    and 2: "sigma |= <>F"
1.334 +    and 3: "|- []A & F --> G"
1.335 +  shows "sigma |= <>G"
1.336 +  apply (rule 2 [THEN 1 [THEN BoxDmd [temp_use]], THEN DmdImplE])
1.337 +  apply (rule 3)
1.338 +  done
1.339 +
1.340 +lemma STL6: "|- <>[]F & <>[]G --> <>[](F & G)"
1.341 +  apply (auto simp: STL5 [temp_rewrite, symmetric])
1.342 +  apply (drule linT [temp_use])
1.343 +   apply assumption
1.344 +  apply (erule thin_rl)
1.345 +  apply (rule DmdDmd [temp_unlift, THEN iffD1])
1.346 +  apply (erule disjE)
1.347 +   apply (erule DmdImplE)
1.348 +   apply (rule BoxDmd)
1.349 +  apply (erule DmdImplE)
1.350 +  apply auto
1.351 +  apply (drule BoxDmd [temp_use])
1.352 +   apply assumption
1.353 +  apply (erule thin_rl)
1.354 +  apply (fastsimp elim!: DmdImplE [temp_use])
1.355 +  done
1.356 +
1.357 +
1.358 +(* ------------------------ True / False ----------------------------------------- *)
1.359 +section "Simplification of constants"
1.360 +
1.361 +lemma BoxConst: "|- ([]#P) = #P"
1.362 +  apply (rule tempI)
1.363 +  apply (cases P)
1.364 +   apply (auto intro!: necT [temp_use] dest: STL2_gen [temp_use] simp: Init_simps)
1.365 +  done
1.366 +
1.367 +lemma DmdConst: "|- (<>#P) = #P"
1.368 +  apply (unfold dmd_def)
1.369 +  apply (cases P)
1.370 +  apply (simp_all add: BoxConst [try_rewrite])
1.371 +  done
1.372 +
1.373 +lemmas temp_simps [temp_rewrite, simp] = BoxConst DmdConst
1.374 +
1.375 +(* Make these rewrites active by default *)
1.376 +ML {*
1.377 +val temp_css = temp_css addsimps2 (thms "temp_simps")
1.378 +val temp_cs = op addss temp_css
1.379 +*}
1.380 +
1.381 +
1.382 +(* ------------------------ Further rewrites ----------------------------------------- *)
1.383 +section "Further rewrites"
1.384 +
1.385 +lemma NotBox: "|- (~[]F) = (<>~F)"
1.386 +  by (simp add: dmd_def)
1.387 +
1.388 +lemma NotDmd: "|- (~<>F) = ([]~F)"
1.389 +  by (simp add: dmd_def)
1.390 +
1.391 +(* These are not declared by default, because they could be harmful,
1.392 +   e.g. []F & ~[]F becomes []F & <>~F !! *)
1.393 +lemmas more_temp_simps =
1.394 +  STL3 [temp_rewrite] DmdDmd [temp_rewrite] NotBox [temp_rewrite] NotDmd [temp_rewrite]
1.395 +  NotBox [temp_unlift, THEN eq_reflection]
1.396 +  NotDmd [temp_unlift, THEN eq_reflection]
1.397 +
1.398 +lemma BoxDmdBox: "|- ([]<>[]F) = (<>[]F)"
1.399 +  apply (auto dest!: STL2 [temp_use])
1.400 +  apply (rule ccontr)
1.401 +  apply (subgoal_tac "sigma |= <>[][]F & <>[]~[]F")
1.402 +   apply (erule thin_rl)
1.403 +   apply auto
1.404 +    apply (drule STL6 [temp_use])
1.405 +     apply assumption
1.406 +    apply simp
1.407 +   apply (simp_all add: more_temp_simps)
1.408 +  done
1.409 +
1.410 +lemma DmdBoxDmd: "|- (<>[]<>F) = ([]<>F)"
1.411 +  apply (unfold dmd_def)
1.412 +  apply (auto simp: BoxDmdBox [unfolded dmd_def, try_rewrite])
1.413 +  done
1.414 +
1.415 +lemmas more_temp_simps = more_temp_simps BoxDmdBox [temp_rewrite] DmdBoxDmd [temp_rewrite]
1.416 +
1.417 +
1.418 +(* ------------------------ Miscellaneous ----------------------------------- *)
1.419 +
1.420 +lemma BoxOr: "!!sigma. [| sigma |= []F | []G |] ==> sigma |= [](F | G)"
1.421 +  by (fastsimp elim!: STL4E [temp_use])
1.422 +
1.423 +(* "persistently implies infinitely often" *)
1.424 +lemma DBImplBD: "|- <>[]F --> []<>F"
1.425 +  apply clarsimp
1.426 +  apply (rule ccontr)
1.427 +  apply (simp add: more_temp_simps)
1.428 +  apply (drule STL6 [temp_use])
1.429 +   apply assumption
1.430 +  apply simp
1.431 +  done
1.432 +
1.433 +lemma BoxDmdDmdBox: "|- []<>F & <>[]G --> []<>(F & G)"
1.434 +  apply clarsimp
1.435 +  apply (rule ccontr)
1.436 +  apply (unfold more_temp_simps)
1.437 +  apply (drule STL6 [temp_use])
1.438 +   apply assumption
1.439 +  apply (subgoal_tac "sigma |= <>[]~F")
1.440 +   apply (force simp: dmd_def)
1.441 +  apply (fastsimp elim: DmdImplE [temp_use] STL4E [temp_use])
1.442 +  done
1.443 +
1.444 +
1.445 +(* ------------------------------------------------------------------------- *)
1.446 +(***          TLA-specific theorems: primed formulas                       ***)
1.447 +(* ------------------------------------------------------------------------- *)
1.448 +section "priming"
1.449 +
1.450 +(* ------------------------ TLA2 ------------------------------------------- *)
1.451 +lemma STL2_pr: "|- []P --> Init P & Init P`"
1.452 +  by (fastsimp intro!: STL2_gen [temp_use] primeI [temp_use])
1.453 +
1.454 +(* Auxiliary lemma allows priming of boxed actions *)
1.455 +lemma BoxPrime: "|- []P --> [](\$P & P\$)"
1.456 +  apply clarsimp
1.457 +  apply (erule dup_boxE)
1.458 +  apply (unfold boxInit_act)
1.459 +  apply (erule STL4E)
1.460 +  apply (auto simp: Init_simps dest!: STL2_pr [temp_use])
1.461 +  done
1.462 +
1.463 +lemma TLA2:
1.464 +  assumes "|- \$P & P\$ --> A"
1.465 +  shows "|- []P --> []A"
1.466 +  apply clarsimp
1.467 +  apply (drule BoxPrime [temp_use])
1.468 +  apply (auto simp: Init_stp_act_rev [try_rewrite] intro!: prems [temp_use]
1.469 +    elim!: STL4E [temp_use])
1.470 +  done
1.471 +
1.472 +lemma TLA2E: "[| sigma |= []P; |- \$P & P\$ --> A |] ==> sigma |= []A"
1.473 +  by (erule (1) TLA2 [temp_use])
1.474 +
1.475 +lemma DmdPrime: "|- (<>P`) --> (<>P)"
1.476 +  apply (unfold dmd_def)
1.477 +  apply (fastsimp elim!: TLA2E [temp_use])
1.478 +  done
1.479 +
1.480 +lemmas PrimeDmd = InitDmd_gen [temp_use, THEN DmdPrime [temp_use], standard]
1.481 +
1.482 +(* ------------------------ INV1, stable --------------------------------------- *)
1.483 +section "stable, invariant"
1.484 +
1.485 +lemma ind_rule:
1.486 +   "[| sigma |= []H; sigma |= Init P; |- H --> (Init P & ~[]F --> Init(P`) & F) |]
1.487 +    ==> sigma |= []F"
1.488 +  apply (rule indT [temp_use])
1.489 +   apply (erule (2) STL4E)
1.490 +  done
1.491 +
1.492 +lemma box_stp_act: "|- ([]\$P) = ([]P)"
1.493 +  by (simp add: boxInit_act Init_simps)
1.494 +
1.495 +lemmas box_stp_actI = box_stp_act [temp_use, THEN iffD2, standard]
1.496 +lemmas box_stp_actD = box_stp_act [temp_use, THEN iffD1, standard]
1.497 +
1.498 +lemmas more_temp_simps = box_stp_act [temp_rewrite] more_temp_simps
1.499 +
1.500 +lemma INV1:
1.501 +  "|- (Init P) --> (stable P) --> []P"
1.502 +  apply (unfold stable_def boxInit_stp boxInit_act)
1.503 +  apply clarsimp
1.504 +  apply (erule ind_rule)
1.505 +   apply (auto simp: Init_simps elim: ind_rule)
1.506 +  done
1.507 +
1.508 +lemma StableT:
1.509 +    "!!P. |- \$P & A --> P` ==> |- []A --> stable P"
1.510 +  apply (unfold stable_def)
1.511 +  apply (fastsimp elim!: STL4E [temp_use])
1.512 +  done
1.513 +
1.514 +lemma Stable: "[| sigma |= []A; |- \$P & A --> P` |] ==> sigma |= stable P"
1.515 +  by (erule (1) StableT [temp_use])
1.516 +
1.517 +(* Generalization of INV1 *)
1.518 +lemma StableBox: "|- (stable P) --> [](Init P --> []P)"
1.519 +  apply (unfold stable_def)
1.520 +  apply clarsimp
1.521 +  apply (erule dup_boxE)
1.522 +  apply (force simp: stable_def elim: STL4E [temp_use] INV1 [temp_use])
1.523 +  done
1.524 +
1.525 +lemma DmdStable: "|- (stable P) & <>P --> <>[]P"
1.526 +  apply clarsimp
1.527 +  apply (rule DmdImpl2)
1.528 +   prefer 2
1.529 +   apply (erule StableBox [temp_use])
1.530 +  apply (simp add: dmdInitD)
1.531 +  done
1.532 +
1.533 +(* ---------------- (Semi-)automatic invariant tactics ---------------------- *)
1.534 +
1.535 +ML {*
1.536 +local
1.537 +  val INV1 = thm "INV1";
1.538 +  val Stable = thm "Stable";
1.539 +  val Init_stp = thm "Init_stp";
1.540 +  val Init_act = thm "Init_act";
1.541 +  val squareE = thm "squareE";
1.542 +in
1.543 +
1.544 +(* inv_tac reduces goals of the form ... ==> sigma |= []P *)
1.545 +fun inv_tac css = SELECT_GOAL
1.546 +     (EVERY [auto_tac css,
1.547 +             TRY (merge_box_tac 1),
1.548 +             rtac (temp_use INV1) 1, (* fail if the goal is not a box *)
1.549 +             TRYALL (etac Stable)]);
1.550 +
1.551 +(* auto_inv_tac applies inv_tac and then tries to attack the subgoals
1.552 +   in simple cases it may be able to handle goals like |- MyProg --> []Inv.
1.553 +   In these simple cases the simplifier seems to be more useful than the
1.554 +   auto-tactic, which applies too much propositional logic and simplifies
1.555 +   too late.
1.556 +*)
1.557 +fun auto_inv_tac ss = SELECT_GOAL
1.558 +    ((inv_tac (claset(),ss) 1) THEN
1.559 +     (TRYALL (action_simp_tac (ss addsimps [Init_stp, Init_act]) [] [squareE])));
1.560 +end
1.561 +*}
1.562 +
1.563 +lemma unless: "|- [](\$P --> P` | Q`) --> (stable P) | <>Q"
1.564 +  apply (unfold dmd_def)
1.565 +  apply (clarsimp dest!: BoxPrime [temp_use])
1.566 +  apply (tactic "merge_box_tac 1")
1.567 +  apply (erule contrapos_np)
1.568 +  apply (fastsimp elim!: Stable [temp_use])
1.569 +  done
1.570 +
1.571 +
1.572 +(* --------------------- Recursive expansions --------------------------------------- *)
1.573 +section "recursive expansions"
1.574 +
1.575 +(* Recursive expansions of [] and <> for state predicates *)
1.576 +lemma BoxRec: "|- ([]P) = (Init P & []P`)"
1.577 +  apply (auto intro!: STL2_gen [temp_use])
1.578 +   apply (fastsimp elim!: TLA2E [temp_use])
1.579 +  apply (auto simp: stable_def elim!: INV1 [temp_use] STL4E [temp_use])
1.580 +  done
1.581 +
1.582 +lemma DmdRec: "|- (<>P) = (Init P | <>P`)"
1.583 +  apply (unfold dmd_def BoxRec [temp_rewrite])
1.584 +  apply (auto simp: Init_simps)
1.585 +  done
1.586 +
1.587 +lemma DmdRec2: "!!sigma. [| sigma |= <>P; sigma |= []~P` |] ==> sigma |= Init P"
1.588 +  apply (force simp: DmdRec [temp_rewrite] dmd_def)
1.589 +  done
1.590 +
1.591 +lemma InfinitePrime: "|- ([]<>P) = ([]<>P`)"
1.592 +  apply auto
1.593 +   apply (rule classical)
1.594 +   apply (rule DBImplBD [temp_use])
1.595 +   apply (subgoal_tac "sigma |= <>[]P")
1.596 +    apply (fastsimp elim!: DmdImplE [temp_use] TLA2E [temp_use])
1.597 +   apply (subgoal_tac "sigma |= <>[] (<>P & []~P`)")
1.598 +    apply (force simp: boxInit_stp [temp_use]
1.599 +      elim!: DmdImplE [temp_use] STL4E [temp_use] DmdRec2 [temp_use])
1.600 +   apply (force intro!: STL6 [temp_use] simp: more_temp_simps)
1.601 +  apply (fastsimp intro: DmdPrime [temp_use] elim!: STL4E [temp_use])
1.602 +  done
1.603 +
1.604 +lemma InfiniteEnsures:
1.605 +  "[| sigma |= []N; sigma |= []<>A; |- A & N --> P` |] ==> sigma |= []<>P"
1.606 +  apply (unfold InfinitePrime [temp_rewrite])
1.607 +  apply (rule InfImpl)
1.608 +    apply assumption+
1.609 +  done
1.610 +
1.611 +(* ------------------------ fairness ------------------------------------------- *)
1.612 +section "fairness"
1.613 +
1.614 +(* alternative definitions of fairness *)
1.615 +lemma WF_alt: "|- WF(A)_v = ([]<>~Enabled(<A>_v) | []<><A>_v)"
1.616 +  apply (unfold WF_def dmd_def)
1.617 +  apply fastsimp
1.618 +  done
1.619 +
1.620 +lemma SF_alt: "|- SF(A)_v = (<>[]~Enabled(<A>_v) | []<><A>_v)"
1.621 +  apply (unfold SF_def dmd_def)
1.622 +  apply fastsimp
1.623 +  done
1.624 +
1.625 +(* theorems to "box" fairness conditions *)
1.626 +lemma BoxWFI: "|- WF(A)_v --> []WF(A)_v"
1.627 +  by (auto simp: WF_alt [try_rewrite] more_temp_simps intro!: BoxOr [temp_use])
1.628 +
1.629 +lemma WF_Box: "|- ([]WF(A)_v) = WF(A)_v"
1.630 +  by (fastsimp intro!: BoxWFI [temp_use] dest!: STL2 [temp_use])
1.631 +
1.632 +lemma BoxSFI: "|- SF(A)_v --> []SF(A)_v"
1.633 +  by (auto simp: SF_alt [try_rewrite] more_temp_simps intro!: BoxOr [temp_use])
1.634 +
1.635 +lemma SF_Box: "|- ([]SF(A)_v) = SF(A)_v"
1.636 +  by (fastsimp intro!: BoxSFI [temp_use] dest!: STL2 [temp_use])
1.637 +
1.638 +lemmas more_temp_simps = more_temp_simps WF_Box [temp_rewrite] SF_Box [temp_rewrite]
1.639 +
1.640 +lemma SFImplWF: "|- SF(A)_v --> WF(A)_v"
1.641 +  apply (unfold SF_def WF_def)
1.642 +  apply (fastsimp dest!: DBImplBD [temp_use])
1.643 +  done
1.644 +
1.645 +(* A tactic that "boxes" all fairness conditions. Apply more_temp_simps to "unbox". *)
1.646 +ML {*
1.647 +local
1.648 +  val BoxWFI = thm "BoxWFI";
1.649 +  val BoxSFI = thm "BoxSFI";
1.650 +in
1.651 +val box_fair_tac = SELECT_GOAL (REPEAT (dresolve_tac [BoxWFI,BoxSFI] 1))
1.652 +end
1.653 +*}
1.654 +
1.655 +
1.656 +(* ------------------------------ leads-to ------------------------------ *)
1.657 +
1.658 +section "~>"
1.659 +
1.660 +lemma leadsto_init: "|- (Init F) & (F ~> G) --> <>G"
1.662 +  apply (auto dest!: STL2 [temp_use])
1.663 +  done
1.664 +
1.665 +(* |- F & (F ~> G) --> <>G *)
1.666 +lemmas leadsto_init_temp = leadsto_init [where 'a = behavior, unfolded Init_simps, standard]
1.667 +
1.668 +lemma streett_leadsto: "|- ([]<>Init F --> []<>G) = (<>(F ~> G))"
1.670 +  apply auto
1.671 +    apply (simp add: more_temp_simps)
1.672 +    apply (fastsimp elim!: DmdImplE [temp_use] STL4E [temp_use])
1.673 +   apply (fastsimp intro!: InitDmd [temp_use] elim!: STL4E [temp_use])
1.674 +  apply (subgoal_tac "sigma |= []<><>G")
1.675 +   apply (simp add: more_temp_simps)
1.676 +  apply (drule BoxDmdDmdBox [temp_use])
1.677 +   apply assumption
1.678 +  apply (fastsimp elim!: DmdImplE [temp_use] STL4E [temp_use])
1.679 +  done
1.680 +
1.681 +lemma leadsto_infinite: "|- []<>F & (F ~> G) --> []<>G"
1.682 +  apply clarsimp
1.683 +  apply (erule InitDmd [temp_use, THEN streett_leadsto [temp_unlift, THEN iffD2, THEN mp]])
1.684 +  apply (simp add: dmdInitD)
1.685 +  done
1.686 +
1.687 +(* In particular, strong fairness is a Streett condition. The following
1.688 +   rules are sometimes easier to use than WF2 or SF2 below.
1.689 +*)
1.690 +lemma leadsto_SF: "|- (Enabled(<A>_v) ~> <A>_v) --> SF(A)_v"
1.691 +  apply (unfold SF_def)
1.692 +  apply (clarsimp elim!: leadsto_infinite [temp_use])
1.693 +  done
1.694 +
1.695 +lemma leadsto_WF: "|- (Enabled(<A>_v) ~> <A>_v) --> WF(A)_v"
1.696 +  by (clarsimp intro!: SFImplWF [temp_use] leadsto_SF [temp_use])
1.697 +
1.698 +(* introduce an invariant into the proof of a leadsto assertion.
1.699 +   []I --> ((P ~> Q)  =  (P /\ I ~> Q))
1.700 +*)
1.701 +lemma INV_leadsto: "|- []I & (P & I ~> Q) --> (P ~> Q)"
1.703 +  apply clarsimp
1.704 +  apply (erule STL4Edup)
1.705 +   apply assumption
1.706 +  apply (auto simp: Init_simps dest!: STL2_gen [temp_use])
1.707 +  done
1.708 +
1.709 +lemma leadsto_classical: "|- (Init F & []~G ~> G) --> (F ~> G)"
1.710 +  apply (unfold leadsto_def dmd_def)
1.711 +  apply (force simp: Init_simps elim!: STL4E [temp_use])
1.712 +  done
1.713 +
1.714 +lemma leadsto_false: "|- (F ~> #False) = ([]~F)"
1.716 +  apply (simp add: boxNotInitD)
1.717 +  done
1.718 +
1.719 +lemma leadsto_exists: "|- ((EX x. F x) ~> G) = (ALL x. (F x ~> G))"
1.721 +  apply (auto simp: allT [try_rewrite] Init_simps elim!: STL4E [temp_use])
1.722 +  done
1.723 +
1.724 +(* basic leadsto properties, cf. Unity *)
1.725 +
1.726 +lemma ImplLeadsto_gen: "|- [](Init F --> Init G) --> (F ~> G)"
1.728 +  apply (auto intro!: InitDmd_gen [temp_use]
1.729 +    elim!: STL4E_gen [temp_use] simp: Init_simps)
1.730 +  done
1.731 +
1.732 +lemmas ImplLeadsto = ImplLeadsto_gen [where 'a = behavior and 'b = behavior,
1.733 +  unfolded Init_simps, standard]
1.734 +
1.735 +lemma ImplLeadsto_simple: "!!F G. |- F --> G ==> |- F ~> G"
1.736 +  by (auto simp: Init_def intro!: ImplLeadsto_gen [temp_use] necT [temp_use])
1.737 +
1.739 +  assumes "|- A & \$P --> Q`"
1.740 +  shows "|- []A --> (P ~> Q)"
1.742 +  apply (clarsimp elim!: INV_leadsto [temp_use])
1.743 +  apply (erule STL4E_gen)
1.744 +  apply (auto simp: Init_defs intro!: PrimeDmd [temp_use] assms [temp_use])
1.745 +  done
1.746 +
1.747 +lemma EnsuresLeadsto2: "|- [](\$P --> Q`) --> (P ~> Q)"
1.749 +  apply clarsimp
1.750 +  apply (erule STL4E_gen)
1.751 +  apply (auto simp: Init_simps intro!: PrimeDmd [temp_use])
1.752 +  done
1.753 +
1.754 +lemma ensures:
1.755 +  assumes 1: "|- \$P & N --> P` | Q`"
1.756 +    and 2: "|- (\$P & N) & A --> Q`"
1.757 +  shows "|- []N & []([]P --> <>A) --> (P ~> Q)"
1.759 +  apply clarsimp
1.760 +  apply (erule STL4Edup)
1.761 +   apply assumption
1.762 +  apply clarsimp
1.763 +  apply (subgoal_tac "sigmaa |= [] (\$P --> P` | Q`) ")
1.764 +   apply (drule unless [temp_use])
1.765 +   apply (clarsimp dest!: INV1 [temp_use])
1.766 +  apply (rule 2 [THEN DmdImpl, temp_use, THEN DmdPrime [temp_use]])
1.767 +   apply (force intro!: BoxDmd_simple [temp_use]
1.768 +     simp: split_box_conj [try_rewrite] box_stp_act [try_rewrite])
1.769 +  apply (force elim: STL4E [temp_use] dest: 1 [temp_use])
1.770 +  done
1.771 +
1.772 +lemma ensures_simple:
1.773 +  "[| |- \$P & N --> P` | Q`;
1.774 +      |- (\$P & N) & A --> Q`
1.775 +   |] ==> |- []N & []<>A --> (P ~> Q)"
1.776 +  apply clarsimp
1.777 +  apply (erule (2) ensures [temp_use])
1.778 +  apply (force elim!: STL4E [temp_use])
1.779 +  done
1.780 +
1.781 +lemma EnsuresInfinite:
1.782 +    "[| sigma |= []<>P; sigma |= []A; |- A & \$P --> Q` |] ==> sigma |= []<>Q"
1.783 +  apply (erule leadsto_infinite [temp_use])
1.784 +  apply (erule EnsuresLeadsto [temp_use])
1.785 +  apply assumption
1.786 +  done
1.787 +
1.788 +
1.789 +(*** Gronning's lattice rules (taken from TLP) ***)
1.790 +section "Lattice rules"
1.791 +
1.792 +lemma LatticeReflexivity: "|- F ~> F"
1.794 +  apply (rule necT InitDmd_gen)+
1.795 +  done
1.796 +
1.797 +lemma LatticeTransitivity: "|- (G ~> H) & (F ~> G) --> (F ~> H)"
1.799 +  apply clarsimp
1.800 +  apply (erule dup_boxE) (* [][] (Init G --> H) *)
1.801 +  apply (tactic "merge_box_tac 1")
1.802 +  apply (clarsimp elim!: STL4E [temp_use])
1.803 +  apply (rule dup_dmdD)
1.804 +  apply (subgoal_tac "sigmaa |= <>Init G")
1.805 +   apply (erule DmdImpl2)
1.806 +   apply assumption
1.807 +  apply (simp add: dmdInitD)
1.808 +  done
1.809 +
1.810 +lemma LatticeDisjunctionElim1: "|- (F | G ~> H) --> (F ~> H)"
1.812 +  apply (auto simp: Init_simps elim!: STL4E [temp_use])
1.813 +  done
1.814 +
1.815 +lemma LatticeDisjunctionElim2: "|- (F | G ~> H) --> (G ~> H)"
1.817 +  apply (auto simp: Init_simps elim!: STL4E [temp_use])
1.818 +  done
1.819 +
1.820 +lemma LatticeDisjunctionIntro: "|- (F ~> H) & (G ~> H) --> (F | G ~> H)"
1.822 +  apply clarsimp
1.823 +  apply (tactic "merge_box_tac 1")
1.824 +  apply (auto simp: Init_simps elim!: STL4E [temp_use])
1.825 +  done
1.826 +
1.827 +lemma LatticeDisjunction: "|- (F | G ~> H) = ((F ~> H) & (G ~> H))"
1.828 +  by (auto intro: LatticeDisjunctionIntro [temp_use]
1.829 +    LatticeDisjunctionElim1 [temp_use]
1.830 +    LatticeDisjunctionElim2 [temp_use])
1.831 +
1.832 +lemma LatticeDiamond: "|- (A ~> B | C) & (B ~> D) & (C ~> D) --> (A ~> D)"
1.833 +  apply clarsimp
1.834 +  apply (subgoal_tac "sigma |= (B | C) ~> D")
1.835 +  apply (erule_tac G = "LIFT (B | C)" in LatticeTransitivity [temp_use])
1.836 +   apply (fastsimp intro!: LatticeDisjunctionIntro [temp_use])+
1.837 +  done
1.838 +
1.839 +lemma LatticeTriangle: "|- (A ~> D | B) & (B ~> D) --> (A ~> D)"
1.840 +  apply clarsimp
1.841 +  apply (subgoal_tac "sigma |= (D | B) ~> D")
1.842 +   apply (erule_tac G = "LIFT (D | B)" in LatticeTransitivity [temp_use])
1.843 +  apply assumption
1.844 +  apply (auto intro: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use])
1.845 +  done
1.846 +
1.847 +lemma LatticeTriangle2: "|- (A ~> B | D) & (B ~> D) --> (A ~> D)"
1.848 +  apply clarsimp
1.849 +  apply (subgoal_tac "sigma |= B | D ~> D")
1.850 +   apply (erule_tac G = "LIFT (B | D)" in LatticeTransitivity [temp_use])
1.851 +   apply assumption
1.852 +  apply (auto intro: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use])
1.853 +  done
1.854 +
1.855 +(*** Lamport's fairness rules ***)
1.856 +section "Fairness rules"
1.857 +
1.858 +lemma WF1:
1.859 +  "[| |- \$P & N  --> P` | Q`;
1.860 +      |- (\$P & N) & <A>_v --> Q`;
1.861 +      |- \$P & N --> \$(Enabled(<A>_v)) |]
1.862 +  ==> |- []N & WF(A)_v --> (P ~> Q)"
1.863 +  apply (clarsimp dest!: BoxWFI [temp_use])
1.864 +  apply (erule (2) ensures [temp_use])
1.865 +  apply (erule (1) STL4Edup)
1.866 +  apply (clarsimp simp: WF_def)
1.867 +  apply (rule STL2 [temp_use])
1.868 +  apply (clarsimp elim!: mp intro!: InitDmd [temp_use])
1.869 +  apply (erule STL4 [temp_use, THEN box_stp_actD [temp_use]])
1.870 +  apply (simp add: split_box_conj box_stp_actI)
1.871 +  done
1.872 +
1.873 +(* Sometimes easier to use; designed for action B rather than state predicate Q *)
1.875 +  assumes 1: "|- N & \$P --> \$Enabled (<A>_v)"
1.876 +    and 2: "|- N & <A>_v --> B"
1.877 +    and 3: "|- [](N & [~A]_v) --> stable P"
1.878 +  shows "|- []N & WF(A)_v --> (P ~> B)"
1.880 +  apply (clarsimp dest!: BoxWFI [temp_use])
1.881 +  apply (erule (1) STL4Edup)
1.882 +  apply clarsimp
1.883 +  apply (rule 2 [THEN DmdImpl, temp_use])
1.884 +  apply (rule BoxDmd_simple [temp_use])
1.885 +   apply assumption
1.886 +  apply (rule classical)
1.887 +  apply (rule STL2 [temp_use])
1.888 +  apply (clarsimp simp: WF_def elim!: mp intro!: InitDmd [temp_use])
1.889 +  apply (rule 1 [THEN STL4, temp_use, THEN box_stp_actD])
1.890 +  apply (simp (no_asm_simp) add: split_box_conj [try_rewrite] box_stp_act [try_rewrite])
1.891 +  apply (erule INV1 [temp_use])
1.892 +  apply (rule 3 [temp_use])
1.893 +  apply (simp add: split_box_conj [try_rewrite] NotDmd [temp_use] not_angle [try_rewrite])
1.894 +  done
1.895 +
1.896 +lemma SF1:
1.897 +  "[| |- \$P & N  --> P` | Q`;
1.898 +      |- (\$P & N) & <A>_v --> Q`;
1.899 +      |- []P & []N & []F --> <>Enabled(<A>_v) |]
1.900 +  ==> |- []N & SF(A)_v & []F --> (P ~> Q)"
1.901 +  apply (clarsimp dest!: BoxSFI [temp_use])
1.902 +  apply (erule (2) ensures [temp_use])
1.903 +  apply (erule_tac F = F in dup_boxE)
1.904 +  apply (tactic "merge_temp_box_tac 1")
1.905 +  apply (erule STL4Edup)
1.906 +  apply assumption
1.907 +  apply (clarsimp simp: SF_def)
1.908 +  apply (rule STL2 [temp_use])
1.909 +  apply (erule mp)
1.910 +  apply (erule STL4 [temp_use])
1.911 +  apply (simp add: split_box_conj [try_rewrite] STL3 [try_rewrite])
1.912 +  done
1.913 +
1.914 +lemma WF2:
1.915 +  assumes 1: "|- N & <B>_f --> <M>_g"
1.916 +    and 2: "|- \$P & P` & <N & A>_f --> B"
1.917 +    and 3: "|- P & Enabled(<M>_g) --> Enabled(<A>_f)"
1.918 +    and 4: "|- [](N & [~B]_f) & WF(A)_f & []F & <>[]Enabled(<M>_g) --> <>[]P"
1.919 +  shows "|- []N & WF(A)_f & []F --> WF(M)_g"
1.920 +  apply (clarsimp dest!: BoxWFI [temp_use] BoxDmdBox [temp_use, THEN iffD2]
1.921 +    simp: WF_def [where A = M])
1.922 +  apply (erule_tac F = F in dup_boxE)
1.923 +  apply (tactic "merge_temp_box_tac 1")
1.924 +  apply (erule STL4Edup)
1.925 +   apply assumption
1.926 +  apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]])
1.927 +  apply (rule classical)
1.928 +  apply (subgoal_tac "sigmaa |= <> ((\$P & P` & N) & <A>_f)")
1.929 +   apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use])
1.930 +  apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use])
1.931 +  apply (simp add: NotDmd [temp_use] not_angle [try_rewrite])
1.932 +  apply (tactic "merge_act_box_tac 1")
1.933 +  apply (frule 4 [temp_use])
1.934 +     apply assumption+
1.935 +  apply (drule STL6 [temp_use])
1.936 +   apply assumption
1.937 +  apply (erule_tac V = "sigmaa |= <>[]P" in thin_rl)
1.938 +  apply (erule_tac V = "sigmaa |= []F" in thin_rl)
1.939 +  apply (drule BoxWFI [temp_use])
1.940 +  apply (erule_tac F = "ACT N & [~B]_f" in dup_boxE)
1.941 +  apply (tactic "merge_temp_box_tac 1")
1.942 +  apply (erule DmdImpldup)
1.943 +   apply assumption
1.944 +  apply (auto simp: split_box_conj [try_rewrite] STL3 [try_rewrite]
1.945 +    WF_Box [try_rewrite] box_stp_act [try_rewrite])
1.946 +   apply (force elim!: TLA2E [where P = P, temp_use])
1.947 +  apply (rule STL2 [temp_use])
1.948 +  apply (force simp: WF_def split_box_conj [try_rewrite]
1.949 +    elim!: mp intro!: InitDmd [temp_use] 3 [THEN STL4, temp_use])
1.950 +  done
1.951 +
1.952 +lemma SF2:
1.953 +  assumes 1: "|- N & <B>_f --> <M>_g"
1.954 +    and 2: "|- \$P & P` & <N & A>_f --> B"
1.955 +    and 3: "|- P & Enabled(<M>_g) --> Enabled(<A>_f)"
1.956 +    and 4: "|- [](N & [~B]_f) & SF(A)_f & []F & []<>Enabled(<M>_g) --> <>[]P"
1.957 +  shows "|- []N & SF(A)_f & []F --> SF(M)_g"
1.958 +  apply (clarsimp dest!: BoxSFI [temp_use] simp: 2 [try_rewrite] SF_def [where A = M])
1.959 +  apply (erule_tac F = F in dup_boxE)
1.960 +  apply (erule_tac F = "TEMP <>Enabled (<M>_g) " in dup_boxE)
1.961 +  apply (tactic "merge_temp_box_tac 1")
1.962 +  apply (erule STL4Edup)
1.963 +   apply assumption
1.964 +  apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]])
1.965 +  apply (rule classical)
1.966 +  apply (subgoal_tac "sigmaa |= <> ((\$P & P` & N) & <A>_f)")
1.967 +   apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use])
1.968 +  apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use])
1.969 +  apply (simp add: NotDmd [temp_use] not_angle [try_rewrite])
1.970 +  apply (tactic "merge_act_box_tac 1")
1.971 +  apply (frule 4 [temp_use])
1.972 +     apply assumption+
1.973 +  apply (erule_tac V = "sigmaa |= []F" in thin_rl)
1.974 +  apply (drule BoxSFI [temp_use])
1.975 +  apply (erule_tac F = "TEMP <>Enabled (<M>_g)" in dup_boxE)
1.976 +  apply (erule_tac F = "ACT N & [~B]_f" in dup_boxE)
1.977 +  apply (tactic "merge_temp_box_tac 1")
1.978 +  apply (erule DmdImpldup)
1.979 +   apply assumption
1.980 +  apply (auto simp: split_box_conj [try_rewrite] STL3 [try_rewrite]
1.981 +    SF_Box [try_rewrite] box_stp_act [try_rewrite])
1.982 +   apply (force elim!: TLA2E [where P = P, temp_use])
1.983 +  apply (rule STL2 [temp_use])
1.984 +  apply (force simp: SF_def split_box_conj [try_rewrite]
1.985 +    elim!: mp InfImpl [temp_use] intro!: 3 [temp_use])
1.986 +  done
1.987 +
1.988 +(* ------------------------------------------------------------------------- *)
1.989 +(***           Liveness proofs by well-founded orderings                   ***)
1.990 +(* ------------------------------------------------------------------------- *)
1.991 +section "Well-founded orderings"
1.992 +
1.994 +  assumes 1: "wf r"
1.995 +    and 2: "!!x. sigma |= F x ~> (G | (EX y. #((y,x):r) & F y))    "
1.996 +  shows "sigma |= F x ~> G"
1.997 +  apply (rule 1 [THEN wf_induct])
1.998 +  apply (rule LatticeTriangle [temp_use])
1.999 +   apply (rule 2)
1.1000 +  apply (auto simp: leadsto_exists [try_rewrite])
1.1001 +  apply (case_tac "(y,x) :r")
1.1002 +   apply force
1.1003 +  apply (force simp: leadsto_def Init_simps intro!: necT [temp_use])
1.1004 +  done
1.1005 +
1.1006 +(* If r is well-founded, state function v cannot decrease forever *)
1.1007 +lemma wf_not_box_decrease: "!!r. wf r ==> |- [][ (v`, \$v) : #r ]_v --> <>[][#False]_v"
1.1008 +  apply clarsimp
1.1009 +  apply (rule ccontr)
1.1010 +  apply (subgoal_tac "sigma |= (EX x. v=#x) ~> #False")
1.1011 +   apply (drule leadsto_false [temp_use, THEN iffD1, THEN STL2_gen [temp_use]])
1.1012 +   apply (force simp: Init_defs)
1.1013 +  apply (clarsimp simp: leadsto_exists [try_rewrite] not_square [try_rewrite] more_temp_simps)
1.1015 +  apply (rule ensures_simple [temp_use])
1.1016 +     apply (tactic "TRYALL atac")
1.1017 +   apply (auto simp: square_def angle_def)
1.1018 +  done
1.1019 +
1.1020 +(* "wf r  ==>  |- <>[][ (v`, \$v) : #r ]_v --> <>[][#False]_v" *)
1.1021 +lemmas wf_not_dmd_box_decrease =
1.1022 +  wf_not_box_decrease [THEN DmdImpl, unfolded more_temp_simps, standard]
1.1023 +
1.1024 +(* If there are infinitely many steps where v decreases, then there
1.1025 +   have to be infinitely many non-stuttering steps where v doesn't decrease.
1.1026 +*)
1.1027 +lemma wf_box_dmd_decrease:
1.1028 +  assumes 1: "wf r"
1.1029 +  shows "|- []<>((v`, \$v) : #r) --> []<><(v`, \$v) ~: #r>_v"
1.1030 +  apply clarsimp
1.1031 +  apply (rule ccontr)
1.1032 +  apply (simp add: not_angle [try_rewrite] more_temp_simps)
1.1033 +  apply (drule 1 [THEN wf_not_dmd_box_decrease [temp_use]])
1.1034 +  apply (drule BoxDmdDmdBox [temp_use])
1.1035 +   apply assumption
1.1036 +  apply (subgoal_tac "sigma |= []<> ((#False) ::action)")
1.1037 +   apply force
1.1038 +  apply (erule STL4E)
1.1039 +  apply (rule DmdImpl)
1.1040 +  apply (force intro: 1 [THEN wf_irrefl, temp_use])
1.1041 +  done
1.1042 +
1.1043 +(* In particular, for natural numbers, if n decreases infinitely often
1.1044 +   then it has to increase infinitely often.
1.1045 +*)
1.1046 +lemma nat_box_dmd_decrease: "!!n::nat stfun. |- []<>(n` < \$n) --> []<>(\$n < n`)"
1.1047 +  apply clarsimp
1.1048 +  apply (subgoal_tac "sigma |= []<><~ ((n`,\$n) : #less_than) >_n")
1.1049 +   apply (erule thin_rl)
1.1050 +   apply (erule STL4E)
1.1051 +   apply (rule DmdImpl)
1.1052 +   apply (clarsimp simp: angle_def [try_rewrite])
1.1053 +  apply (rule wf_box_dmd_decrease [temp_use])
1.1054 +   apply (auto elim!: STL4E [temp_use] DmdImplE [temp_use])
1.1055 +  done
1.1056 +
1.1057 +
1.1058 +(* ------------------------------------------------------------------------- *)
1.1059 +(***           Flexible quantification over state variables                ***)
1.1060 +(* ------------------------------------------------------------------------- *)
1.1061 +section "Flexible quantification"
1.1062 +
1.1063 +lemma aallI:
1.1064 +  assumes 1: "basevars vs"
1.1065 +    and 2: "(!!x. basevars (x,vs) ==> sigma |= F x)"
1.1066 +  shows "sigma |= (AALL x. F x)"
1.1067 +  by (auto simp: aall_def elim!: eexE [temp_use] intro!: 1 dest!: 2 [temp_use])
1.1068 +
1.1069 +lemma aallE: "|- (AALL x. F x) --> F x"
1.1070 +  apply (unfold aall_def)
1.1071 +  apply clarsimp
1.1072 +  apply (erule contrapos_np)
1.1073 +  apply (force intro!: eexI [temp_use])
1.1074 +  done
1.1075 +
1.1076 +(* monotonicity of quantification *)
1.1077 +lemma eex_mono:
1.1078 +  assumes 1: "sigma |= EEX x. F x"
1.1079 +    and 2: "!!x. sigma |= F x --> G x"
1.1080 +  shows "sigma |= EEX x. G x"
1.1081 +  apply (rule unit_base [THEN 1 [THEN eexE]])
1.1082 +  apply (rule eexI [temp_use])
1.1083 +  apply (erule 2 [unfolded intensional_rews, THEN mp])
1.1084 +  done
1.1085 +
1.1086 +lemma aall_mono:
1.1087 +  assumes 1: "sigma |= AALL x. F(x)"
1.1088 +    and 2: "!!x. sigma |= F(x) --> G(x)"
1.1089 +  shows "sigma |= AALL x. G(x)"
1.1090 +  apply (rule unit_base [THEN aallI])
1.1091 +  apply (rule 2 [unfolded intensional_rews, THEN mp])
1.1092 +  apply (rule 1 [THEN aallE [temp_use]])
1.1093 +  done
1.1094 +
1.1095 +(* Derived history introduction rule *)
1.1096 +lemma historyI:
1.1097 +  assumes 1: "sigma |= Init I"
1.1098 +    and 2: "sigma |= []N"
1.1099 +    and 3: "basevars vs"
1.1100 +    and 4: "!!h. basevars(h,vs) ==> |- I & h = ha --> HI h"
1.1101 +    and 5: "!!h s t. [| basevars(h,vs); N (s,t); h t = hb (h s) (s,t) |] ==> HN h (s,t)"
1.1102 +  shows "sigma |= EEX h. Init (HI h) & [](HN h)"
1.1103 +  apply (rule history [temp_use, THEN eexE])
1.1104 +  apply (rule 3)
1.1105 +  apply (rule eexI [temp_use])
1.1106 +  apply clarsimp
1.1107 +  apply (rule conjI)
1.1108 +   prefer 2
1.1109 +   apply (insert 2)
1.1110 +   apply (tactic "merge_box_tac 1")
1.1111 +   apply (force elim!: STL4E [temp_use] 5 [temp_use])
1.1112 +  apply (insert 1)
1.1113 +  apply (force simp: Init_defs elim!: 4 [temp_use])
1.1114 +  done
1.1115 +
1.1116 +(* ----------------------------------------------------------------------
1.1117 +   example of a history variable: existence of a clock
1.1118 +*)
1.1119 +
1.1120 +lemma "|- EEX h. Init(h = #True) & [](h` = (~\$h))"
1.1121 +  apply (rule tempI)
1.1122 +  apply (rule historyI)
1.1123 +  apply (force simp: Init_defs intro!: unit_base [temp_use] necT [temp_use])+
1.1124 +  done
1.1125 +
1.1126 +end
1.1127 +
```