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.65 +  Attrib.add_attributes [
    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.661 +  apply (unfold leadsto_def)
   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.669 +  apply (unfold leadsto_def)
   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.702 +  apply (unfold leadsto_def)
   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.715 +  apply (unfold leadsto_def)
   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.720 +  apply (unfold leadsto_def)
   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.727 +  apply (unfold leadsto_def)
   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.738 +lemma EnsuresLeadsto:
   1.739 +  assumes "|- A & $P --> Q`"
   1.740 +  shows "|- []A --> (P ~> Q)"
   1.741 +  apply (unfold leadsto_def)
   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.748 +  apply (unfold leadsto_def)
   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.758 +  apply (unfold leadsto_def)
   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.793 +  apply (unfold leadsto_def)
   1.794 +  apply (rule necT InitDmd_gen)+
   1.795 +  done
   1.796 +
   1.797 +lemma LatticeTransitivity: "|- (G ~> H) & (F ~> G) --> (F ~> H)"
   1.798 +  apply (unfold leadsto_def)
   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.811 +  apply (unfold leadsto_def)
   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.816 +  apply (unfold leadsto_def)
   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.821 +  apply (unfold leadsto_def)
   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.874 +lemma WF_leadsto:
   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.879 +  apply (unfold leadsto_def)
   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.993 +lemma wf_leadsto:
   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.1014 +  apply (erule wf_leadsto)
  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 +