src/HOL/TLA/TLA.ML
changeset 3807 82a99b090d9d
child 4089 96fba19bcbe2
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/TLA/TLA.ML	Wed Oct 08 11:50:33 1997 +0200
     1.3 @@ -0,0 +1,1059 @@
     1.4 +(* 
     1.5 +    File:	 TLA/TLA.ML
     1.6 +    Author:      Stephan Merz
     1.7 +    Copyright:   1997 University of Munich
     1.8 +
     1.9 +Lemmas and tactics for temporal reasoning.
    1.10 +*)
    1.11 +
    1.12 +(* Specialize intensional introduction/elimination rules to temporal formulas *)
    1.13 +
    1.14 +qed_goal "tempI" TLA.thy "(!!sigma. (sigma |= (F::temporal))) ==> F"
    1.15 +  (fn [prem] => [ REPEAT (resolve_tac [prem,intI] 1) ]);
    1.16 +
    1.17 +qed_goal "tempD" TLA.thy "F::temporal ==> (sigma |= F)"
    1.18 +  (fn [prem] => [ REPEAT (resolve_tac [prem,intD] 1) ]);
    1.19 +
    1.20 +
    1.21 +(* ======== Functions to "unlift" temporal implications into HOL rules ====== *)
    1.22 +
    1.23 +(* Basic unlifting introduces a parameter "sigma" and applies basic rewrites, e.g.
    1.24 +   F .= G    gets   (sigma |= F) = (sigma |= G)
    1.25 +   F .-> G   gets   (sigma |= F) --> (sigma |= G)
    1.26 +*)
    1.27 +fun temp_unlift th = rewrite_rule intensional_rews (th RS tempD);
    1.28 +
    1.29 +(* F .-> G   becomes   sigma |= F  ==>  sigma |= G *)
    1.30 +fun temp_mp th = zero_var_indexes ((temp_unlift th) RS mp);
    1.31 +
    1.32 +(* F .-> G   becomes   [| sigma |= F; sigma |= G ==> R |] ==> R 
    1.33 +   so that it can be used as an elimination rule
    1.34 +*)
    1.35 +fun temp_impE th = zero_var_indexes ((temp_unlift th) RS impE);
    1.36 +
    1.37 +(* F .& G .-> H  becomes  [| sigma |= F; sigma |= G |] ==> sigma |= H *)
    1.38 +fun temp_conjmp th = zero_var_indexes (conjI RS (temp_mp th));
    1.39 +
    1.40 +(* F .& G .-> H  becomes  [| sigma |= F; sigma |= G; (sigma |= H ==> R) |] ==> R *)
    1.41 +fun temp_conjimpE th = zero_var_indexes (conjI RS (temp_impE th));
    1.42 +
    1.43 +(* Turn  F .= G  into meta-level rewrite rule  F == G *)
    1.44 +fun temp_rewrite th = (rewrite_rule intensional_rews (th RS inteq_reflection));
    1.45 +
    1.46 +
    1.47 +(* Update classical reasoner---will be updated once more below! *)
    1.48 +
    1.49 +AddSIs [tempI];
    1.50 +AddDs [tempD];
    1.51 +
    1.52 +val temp_cs = action_cs addSIs [tempI] addDs [tempD];
    1.53 +val temp_css = (temp_cs,!simpset);
    1.54 +
    1.55 +(* ========================================================================= *)
    1.56 +section "Init";
    1.57 +
    1.58 +(* Push logical connectives through Init. *)
    1.59 +qed_goal "Init_true" TLA.thy "Init(#True) .= #True"
    1.60 +  (fn _ => [ auto_tac (temp_css addsimps2 [Init_def]) ]);
    1.61 +
    1.62 +qed_goal "Init_false" TLA.thy "Init(#False) .= #False"
    1.63 +  (fn _ => [ auto_tac (temp_css addsimps2 [Init_def]) ]);
    1.64 +
    1.65 +qed_goal "Init_not" TLA.thy "Init(.~P) .= (.~Init(P))"
    1.66 +  (fn _ => [ auto_tac (temp_css addsimps2 [Init_def]) ]);
    1.67 +
    1.68 +qed_goal "Init_and" TLA.thy "Init(P .& Q) .= (Init(P) .& Init(Q))"
    1.69 +  (fn _ => [ auto_tac (temp_css addsimps2 [Init_def]) ]);
    1.70 +
    1.71 +qed_goal "Init_or" TLA.thy "Init(P .| Q) .= (Init(P) .| Init(Q))"
    1.72 +  (fn _ => [ auto_tac (temp_css addsimps2 [Init_def]) ]);
    1.73 +
    1.74 +qed_goal "Init_imp" TLA.thy "Init(P .-> Q) .= (Init(P) .-> Init(Q))"
    1.75 +  (fn _ => [ auto_tac (temp_css addsimps2 [Init_def]) ]);
    1.76 +
    1.77 +qed_goal "Init_iff" TLA.thy "Init(P .= Q) .= (Init(P) .= Init(Q))"
    1.78 +  (fn _ => [ auto_tac (temp_css addsimps2 [Init_def]) ]);
    1.79 +
    1.80 +qed_goal "Init_all" TLA.thy "Init(RALL x. P(x)) .= (RALL x. Init(P(x)))"
    1.81 +  (fn _ => [ auto_tac (temp_css addsimps2 [Init_def]) ]);
    1.82 +
    1.83 +qed_goal "Init_ex" TLA.thy "Init(REX x. P(x)) .= (REX x. Init(P(x)))"
    1.84 +  (fn _ => [ auto_tac (temp_css addsimps2 [Init_def]) ]);
    1.85 +
    1.86 +val Init_simps = map temp_rewrite
    1.87 +                     [Init_true,Init_false,Init_not,Init_and,Init_or,
    1.88 +		      Init_imp,Init_iff,Init_all,Init_ex];
    1.89 +
    1.90 +
    1.91 +(* Temporal lemmas *)
    1.92 +
    1.93 +qed_goalw "DmdAct" TLA.thy [dmd_def,boxact_def] "(<>(F::action)) .= (<> Init F)"
    1.94 +  (fn _ => [auto_tac (temp_css addsimps2 Init_simps)]);
    1.95 +
    1.96 +
    1.97 +(* ------------------------------------------------------------------------- *)
    1.98 +(***           "Simple temporal logic": only [] and <>                     ***)
    1.99 +(* ------------------------------------------------------------------------- *)
   1.100 +section "Simple temporal logic";
   1.101 +
   1.102 +(* ------------------------ STL2 ------------------------------------------- *)
   1.103 +bind_thm("STL2", reflT);
   1.104 +bind_thm("STL2D", temp_mp STL2);
   1.105 +
   1.106 +(* The action variants. *)
   1.107 +qed_goalw "STL2b" TLA.thy [boxact_def] "[]P .-> Init P"
   1.108 +   (fn _ => [rtac STL2 1]);
   1.109 +bind_thm("STL2bD", temp_mp STL2b);
   1.110 +(* see also STL2b_pr below: "[]P .-> Init(P .& P`)" *)
   1.111 +
   1.112 +(* Dual versions for <> *)
   1.113 +qed_goalw "ImplDmd" TLA.thy [dmd_def] "F .-> <>F"
   1.114 +   (fn _ => [ auto_tac (temp_css addSDs2 [STL2D]) ]);
   1.115 +bind_thm ("ImplDmdD", temp_mp ImplDmd);
   1.116 +
   1.117 +qed_goalw "InitDmd" TLA.thy [dmd_def] "Init(P) .-> <>P"
   1.118 +   (fn _ => [ auto_tac (temp_css addsimps2 Init_simps addSDs2 [STL2bD]) ]);
   1.119 +bind_thm("InitDmdD", temp_mp InitDmd);
   1.120 +
   1.121 +
   1.122 +(* ------------------------ STL3 ------------------------------------------- *)
   1.123 +qed_goal "STL3" TLA.thy "([][]F) .= ([]F)"
   1.124 +   (fn _ => [auto_tac (temp_css addIs2 [temp_mp transT,temp_mp STL2])]);
   1.125 +
   1.126 +(* corresponding elimination rule introduces double boxes: 
   1.127 +   [| (sigma |= []F); (sigma |= [][]F) ==> PROP W |] ==> PROP W
   1.128 +*)
   1.129 +bind_thm("dup_boxE", make_elim((temp_unlift STL3) RS iffD2));
   1.130 +bind_thm("dup_boxD", (temp_unlift STL3) RS iffD1);
   1.131 +
   1.132 +(* dual versions for <> *)
   1.133 +qed_goalw "DmdDmd" TLA.thy [dmd_def] "(<><>F) .= (<>F)"
   1.134 +   (fn _ => [ auto_tac (temp_css addsimps2 [STL3]) ]);
   1.135 +bind_thm("dup_dmdE", make_elim((temp_unlift DmdDmd) RS iffD2));
   1.136 +bind_thm("dup_dmdD", (temp_unlift DmdDmd) RS iffD1);
   1.137 +
   1.138 +
   1.139 +(* ------------------------ STL4 ------------------------------------------- *)
   1.140 +qed_goal "STL4" TLA.thy "(F .-> G)  ==> ([]F .-> []G)"
   1.141 +   (fn [prem] => [Auto_tac(),
   1.142 +		  rtac ((temp_mp normalT) RS mp) 1,
   1.143 +		  REPEAT (ares_tac [prem, necT RS tempD] 1)
   1.144 +		 ]);
   1.145 +
   1.146 +(* A more practical variant as an (unlifted) elimination rule *)
   1.147 +qed_goal "STL4E" TLA.thy 
   1.148 +         "[| (sigma |= []F); F .-> G |] ==> (sigma |= []G)"
   1.149 +   (fn prems => [ REPEAT (resolve_tac (prems @ [temp_mp STL4]) 1) ]);
   1.150 +
   1.151 +(* see also STL4Edup below, which allows an auxiliary boxed formula:
   1.152 +       []A /\ F => G
   1.153 +     -----------------
   1.154 +     []A /\ []F => []G
   1.155 +*)
   1.156 +
   1.157 +(* The dual versions for <> *)
   1.158 +qed_goalw "DmdImpl" TLA.thy [dmd_def]
   1.159 +   "(F .-> G) ==> (<>F .-> <>G)"
   1.160 +   (fn [prem] => [fast_tac (temp_cs addSIs [int_mp prem] addSEs [STL4E]) 1]);
   1.161 +
   1.162 +qed_goal "DmdImplE" TLA.thy
   1.163 +   "[| (sigma |= <>F); F .-> G |] ==> (sigma |= <>G)"
   1.164 +   (fn prems => [ REPEAT (resolve_tac (prems @ [temp_mp DmdImpl]) 1) ]);
   1.165 +
   1.166 +
   1.167 +(* ------------------------ STL5 ------------------------------------------- *)
   1.168 +qed_goal "STL5" TLA.thy "([]F .& []G) .= ([](F .& G))"
   1.169 +   (fn _ => [Auto_tac(),
   1.170 +	     subgoal_tac "sigma |= [](G .-> (F .& G))" 1,
   1.171 +	     etac ((temp_mp normalT) RS mp) 1, atac 1,
   1.172 +	     ALLGOALS (fast_tac (temp_cs addSEs [STL4E]))
   1.173 +	    ]);
   1.174 +(* rewrite rule to split conjunctions under boxes *)
   1.175 +bind_thm("split_box_conj", (temp_unlift STL5) RS sym);
   1.176 +
   1.177 +(* the corresponding elimination rule allows to combine boxes in the hypotheses
   1.178 +   (NB: F and G must have the same type, i.e., both actions or temporals.)
   1.179 +*)
   1.180 +qed_goal "box_conjE" TLA.thy
   1.181 +   "[| (sigma |= []F); (sigma |= []G); (sigma |= [](F.&G)) ==> PROP R |] ==> PROP R"
   1.182 +   (fn prems => [ REPEAT (resolve_tac
   1.183 +			   (prems @ [(temp_unlift STL5) RS iffD1, conjI]) 1) ]);
   1.184 +
   1.185 +(* Define a tactic that tries to merge all boxes in an antecedent. The definition is
   1.186 +   a bit kludgy: how do you simulate "double elim-resolution"?
   1.187 +   Note: If there are boxed hypotheses of different types, the tactic may delete the 
   1.188 +         wrong formulas. We therefore also define less polymorphic tactics for
   1.189 +         temporals and actions.
   1.190 +*)
   1.191 +qed_goal "box_thin" TLA.thy "[| (sigma |= []F); PROP W |] ==> PROP W"
   1.192 +  (fn prems => [resolve_tac prems 1]);
   1.193 +
   1.194 +fun merge_box_tac i =
   1.195 +   REPEAT_DETERM (EVERY [etac box_conjE i, atac i, etac box_thin i]);
   1.196 +
   1.197 +qed_goal "temp_box_conjE" TLA.thy
   1.198 +   "[| (sigma |= [](F::temporal)); (sigma |= []G); (sigma |= [](F.&G)) ==> PROP R |] ==> PROP R"
   1.199 +   (fn prems => [ REPEAT (resolve_tac
   1.200 +			   (prems @ [(temp_unlift STL5) RS iffD1, conjI]) 1) ]);
   1.201 +qed_goal "temp_box_thin" TLA.thy "[| (sigma |= [](F::temporal)); PROP W |] ==> PROP W"
   1.202 +  (fn prems => [resolve_tac prems 1]);
   1.203 +fun merge_temp_box_tac i =
   1.204 +   REPEAT_DETERM (EVERY [etac temp_box_conjE i, atac i, etac temp_box_thin i]);
   1.205 +
   1.206 +qed_goal "act_box_conjE" TLA.thy
   1.207 +   "[| (sigma |= [](A::action)); (sigma |= []B); (sigma |= [](A.&B)) ==> PROP R |] ==> PROP R"
   1.208 +   (fn prems => [ REPEAT (resolve_tac
   1.209 +			   (prems @ [(temp_unlift STL5) RS iffD1, conjI]) 1) ]);
   1.210 +qed_goal "act_box_thin" TLA.thy "[| (sigma |= [](A::action)); PROP W |] ==> PROP W"
   1.211 +  (fn prems => [resolve_tac prems 1]);
   1.212 +fun merge_act_box_tac i =
   1.213 +   REPEAT_DETERM (EVERY [etac act_box_conjE i, atac i, etac act_box_thin i]);
   1.214 +
   1.215 +(* rewrite rule to push universal quantification through box:
   1.216 +      (sigma |= [](RALL x. F x)) = (! x. (sigma |= []F x))
   1.217 +*)
   1.218 +bind_thm("all_box", standard((temp_unlift allT) RS sym));
   1.219 +
   1.220 +
   1.221 +qed_goal "DmdOr" TLA.thy "(<>(F .| G)) .= (<>F .| <>G)"
   1.222 +   (fn _ => [auto_tac (temp_css addsimps2 [dmd_def,split_box_conj]),
   1.223 +             TRYALL (EVERY' [etac swap, 
   1.224 +                             merge_box_tac, 
   1.225 +                             fast_tac (temp_cs addSEs [STL4E])])
   1.226 +            ]);
   1.227 +
   1.228 +qed_goal "exT" TLA.thy "(REX x. <>(F x)) .= (<>(REX x. F x))"
   1.229 +   (fn _ => [ auto_tac (temp_css addsimps2 [dmd_def,temp_rewrite Not_rex,all_box]) ]);
   1.230 +
   1.231 +bind_thm("ex_dmd", standard((temp_unlift exT) RS sym));
   1.232 +	     
   1.233 +
   1.234 +qed_goal "STL4Edup" TLA.thy
   1.235 +   "!!sigma. [| (sigma |= []A); (sigma |= []F); F .& []A .-> G |] ==> (sigma |= []G)"
   1.236 +   (fn _ => [etac dup_boxE 1,
   1.237 +	     merge_box_tac 1,
   1.238 +	     etac STL4E 1,
   1.239 +	     atac 1
   1.240 +	    ]);
   1.241 +
   1.242 +qed_goalw "DmdImpl2" TLA.thy [dmd_def]
   1.243 +   "!!sigma. [| (sigma |= <>F); (sigma |= [](F .-> G)) |] ==> (sigma |= <>G)"
   1.244 +   (fn _ => [Auto_tac(),
   1.245 +	     etac notE 1,
   1.246 +	     merge_box_tac 1,
   1.247 +	     fast_tac (temp_cs addSEs [STL4E]) 1
   1.248 +	    ]);
   1.249 +
   1.250 +qed_goal "InfImpl" TLA.thy
   1.251 +   "[| (sigma |= []<>F); (sigma |= []G); F .& G .-> H |] ==> (sigma |= []<>H)"
   1.252 +   (fn [prem1,prem2,prem3] 
   1.253 +       => [cut_facts_tac [prem1,prem2] 1,
   1.254 +	   eres_inst_tac [("F","G")] dup_boxE 1,
   1.255 +	   merge_box_tac 1,
   1.256 +	   fast_tac (temp_cs addSEs [STL4E,DmdImpl2] addSIs [int_mp prem3]) 1
   1.257 +	  ]);
   1.258 +
   1.259 +(* ------------------------ STL6 ------------------------------------------- *)
   1.260 +(* Used in the proof of STL6, but useful in itself. *)
   1.261 +qed_goalw "BoxDmdT" TLA.thy [dmd_def] "[]F .& <>G .-> <>([]F .& G)"
   1.262 +  (fn _ => [ Auto_tac(),
   1.263 +             etac dup_boxE 1,
   1.264 +	     merge_box_tac 1,
   1.265 +             etac swap 1,
   1.266 +             fast_tac (temp_cs addSEs [STL4E]) 1 ]);
   1.267 +bind_thm("BoxDmd", temp_conjmp BoxDmdT);
   1.268 +
   1.269 +(* weaker than BoxDmd, but more polymorphic (and often just right) *)
   1.270 +qed_goalw "BoxDmdT2" TLA.thy [dmd_def] "<>F .& []G .-> <>(F .& G)"
   1.271 +  (fn _ => [ Auto_tac(),
   1.272 +	     merge_box_tac 1,
   1.273 +             fast_tac (temp_cs addSEs [notE,STL4E]) 1
   1.274 +	   ]);
   1.275 +
   1.276 +qed_goal "STL6" TLA.thy "<>[]F .& <>[]G .-> <>[](F .& G)"
   1.277 +  (fn _ => [auto_tac (temp_css addsimps2 [symmetric (temp_rewrite STL5)]),
   1.278 +	    etac (temp_conjimpE linT) 1, atac 1, etac thin_rl 1,
   1.279 +	    rtac ((temp_unlift DmdDmd) RS iffD1) 1,
   1.280 +	    etac disjE 1,
   1.281 +	    etac DmdImplE 1, rtac BoxDmdT 1,
   1.282 +	    (* the second subgoal needs commutativity of .&, which complicates the proof *)
   1.283 +	    etac DmdImplE 1,
   1.284 +	    Auto_tac(),
   1.285 +	    etac (temp_conjimpE BoxDmdT) 1, atac 1, etac thin_rl 1,
   1.286 +	    fast_tac (temp_cs addSEs [DmdImplE]) 1
   1.287 +	   ]);
   1.288 +
   1.289 +
   1.290 +(* ------------------------ True / False ----------------------------------------- *)
   1.291 +section "Simplification of constants";
   1.292 +
   1.293 +qed_goal "BoxTrue" TLA.thy "[](#True)"
   1.294 +   (fn _ => [ fast_tac (temp_cs addSIs [necT]) 1 ]);
   1.295 +
   1.296 +qed_goal "BoxTrue_simp" TLA.thy "([](#True)) .= #True"
   1.297 +   (fn _ => [ fast_tac (temp_cs addSIs [BoxTrue RS tempD]) 1 ]);
   1.298 +
   1.299 +qed_goal "DmdFalse_simp" TLA.thy "(<>(#False)) .= #False"
   1.300 +   (fn _ => [ auto_tac (temp_css addsimps2 [dmd_def, BoxTrue_simp]) ]);
   1.301 +
   1.302 +qed_goal "DmdTrue_simp" TLA.thy "(<>((#True)::temporal)) .= #True"
   1.303 +   (fn _ => [ fast_tac (temp_cs addSIs [ImplDmdD]) 1 ]);
   1.304 +
   1.305 +qed_goal "DmdActTrue_simp" TLA.thy "(<>((#True)::action)) .= #True"
   1.306 +   (fn _ => [ auto_tac (temp_css addsimps2 Init_simps addSIs2 [InitDmdD]) ]);
   1.307 +
   1.308 +qed_goal "BoxFalse_simp" TLA.thy "([]((#False)::temporal)) .= #False"
   1.309 +   (fn _ => [ fast_tac (temp_cs addSDs [STL2D]) 1 ]);
   1.310 +
   1.311 +qed_goal "BoxActFalse_simp" TLA.thy "([]((#False)::action)) .= #False"
   1.312 +   (fn _ => [ auto_tac (temp_css addsimps2 Init_simps addSDs2 [STL2bD]) ]);
   1.313 +
   1.314 +qed_goal "BoxConst_simp" TLA.thy "([]((#P)::temporal)) .= #P"
   1.315 +   (fn _ => [rtac tempI 1,
   1.316 +             case_tac "P" 1,
   1.317 +             auto_tac (temp_css addsimps2 [BoxTrue_simp,BoxFalse_simp])
   1.318 +            ]);
   1.319 +
   1.320 +qed_goal "BoxActConst_simp" TLA.thy "([]((#P)::action)) .= #P"
   1.321 +   (fn _ => [rtac tempI 1,
   1.322 +             case_tac "P" 1,
   1.323 +             auto_tac (temp_css addsimps2 [BoxTrue_simp,BoxActFalse_simp])
   1.324 +            ]);
   1.325 +
   1.326 +qed_goal "DmdConst_simp" TLA.thy "(<>((#P)::temporal)) .= #P"
   1.327 +   (fn _ => [rtac tempI 1,
   1.328 +             case_tac "P" 1,
   1.329 +             auto_tac (temp_css addsimps2 [DmdTrue_simp,DmdFalse_simp])
   1.330 +            ]);
   1.331 +
   1.332 +qed_goal "DmdActConst_simp" TLA.thy "(<>((#P)::action)) .= #P"
   1.333 +   (fn _ => [rtac tempI 1,
   1.334 +             case_tac "P" 1,
   1.335 +             auto_tac (temp_css addsimps2 [DmdActTrue_simp,DmdFalse_simp])
   1.336 +            ]);
   1.337 +
   1.338 +val temp_simps = map temp_rewrite
   1.339 +                  [BoxTrue_simp,DmdFalse_simp,DmdTrue_simp,
   1.340 +		   DmdActTrue_simp, BoxFalse_simp, BoxActFalse_simp,
   1.341 +		   BoxConst_simp,BoxActConst_simp,DmdConst_simp,DmdActConst_simp];
   1.342 +
   1.343 +(* Make these rewrites active by default *)
   1.344 +Addsimps temp_simps;
   1.345 +val temp_css = temp_css addsimps2 temp_simps;
   1.346 +val temp_cs = temp_cs addss (empty_ss addsimps temp_simps);
   1.347 +
   1.348 +
   1.349 +(* ------------------------ Further rewrites ----------------------------------------- *)
   1.350 +section "Further rewrites";
   1.351 +
   1.352 +qed_goalw "NotBox" TLA.thy [dmd_def] "(.~[]F) .= (<>.~F)"
   1.353 +   (fn _ => [ Auto_tac() ]);
   1.354 +
   1.355 +qed_goalw "NotDmd" TLA.thy [dmd_def] "(.~<>F) .= ([].~F)"
   1.356 +   (fn _ => [ Auto_tac () ]);
   1.357 +
   1.358 +(* These are not by default included in temp_css, because they could be harmful,
   1.359 +   e.g. []F .& .~[]F becomes []F .& <>.~F !! *)
   1.360 +val more_temp_simps =  (map temp_rewrite [STL3, DmdDmd, NotBox, NotDmd])
   1.361 +                       @ (map (fn th => (temp_unlift th) RS eq_reflection)
   1.362 +		         [NotBox, NotDmd]);
   1.363 +
   1.364 +qed_goal "BoxDmdBox" TLA.thy "([]<>[]F) .= (<>[]F)"
   1.365 +   (fn _ => [ auto_tac (temp_css addSDs2 [STL2D]),
   1.366 +              rtac ccontr 1,
   1.367 +              subgoal_tac "sigma |= <>[][]F .& <>[].~[]F" 1,
   1.368 +              etac thin_rl 1,
   1.369 +              Auto_tac(),
   1.370 +	      etac (temp_conjimpE STL6) 1, atac 1,
   1.371 +	      Asm_full_simp_tac 1,
   1.372 +	      ALLGOALS (asm_full_simp_tac (!simpset addsimps more_temp_simps))
   1.373 +	    ]);
   1.374 +
   1.375 +qed_goalw "DmdBoxDmd" TLA.thy [dmd_def] "(<>[]<>F) .= ([]<>F)"
   1.376 +  (fn _ => [auto_tac (temp_css addsimps2 [temp_rewrite (rewrite_rule [dmd_def] BoxDmdBox)])]);
   1.377 +
   1.378 +val more_temp_simps = more_temp_simps @ (map temp_rewrite [BoxDmdBox, DmdBoxDmd]);
   1.379 +
   1.380 +
   1.381 +(* ------------------------ Miscellaneous ----------------------------------- *)
   1.382 +
   1.383 +qed_goal "BoxOr" TLA.thy 
   1.384 +   "!!sigma. [| (sigma |= []F .| []G) |] ==> (sigma |= [](F .| G))"
   1.385 +   (fn _ => [ fast_tac (temp_cs addSEs [STL4E]) 1 ]);
   1.386 +
   1.387 +qed_goal "DBImplBD" TLA.thy "<>[](F::temporal) .-> []<>F"
   1.388 +  (fn _ => [Auto_tac(),
   1.389 +	    rtac ccontr 1,
   1.390 +	    auto_tac (temp_css addsimps2 more_temp_simps addEs2 [temp_conjimpE STL6])
   1.391 +	   ]);
   1.392 +
   1.393 +(* Although the script is the same, the derivation isn't polymorphic and doesn't
   1.394 +   work for other types of formulas (uses STL2).
   1.395 +*)
   1.396 +qed_goal "DBImplBDAct" TLA.thy "<>[](A::action) .-> []<>A"
   1.397 +  (fn _ => [Auto_tac(),
   1.398 +	    rtac ccontr 1,
   1.399 +	    auto_tac (temp_css addsimps2 more_temp_simps addEs2 [temp_conjimpE STL6])
   1.400 +	   ]);
   1.401 +
   1.402 +qed_goal "BoxDmdDmdBox" TLA.thy
   1.403 +   "!!sigma. [| (sigma |= []<>F); (sigma |= <>[]G) |] ==> (sigma |= []<>(F .& G))"
   1.404 +   (fn _ => [rtac ccontr 1,
   1.405 +	     rewrite_goals_tac more_temp_simps,
   1.406 +	     etac (temp_conjimpE STL6) 1, atac 1,
   1.407 +	     subgoal_tac "sigma |= <>[].~F" 1,
   1.408 +	     SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1,
   1.409 +	     fast_tac (temp_cs addEs [DmdImplE,STL4E]) 1
   1.410 +	    ]);
   1.411 +
   1.412 +
   1.413 +(* ------------------------------------------------------------------------- *)
   1.414 +(***          TLA-specific theorems: primed formulas                       ***)
   1.415 +(* ------------------------------------------------------------------------- *)
   1.416 +section "priming";
   1.417 +
   1.418 +(* ------------------------ TLA2 ------------------------------------------- *)
   1.419 +qed_goal "STL2bD_pr" TLA.thy
   1.420 +  "!!sigma. (sigma |= []P) ==> (sigma |= Init(P .& P`))"
   1.421 +  (fn _ => [rewrite_goals_tac Init_simps,
   1.422 +	    fast_tac (temp_cs addSIs [temp_mp primeI, STL2bD]) 1]);
   1.423 +
   1.424 +(* Auxiliary lemma allows priming of boxed actions *)
   1.425 +qed_goal "BoxPrime" TLA.thy "[]P .-> [](P .& P`)"
   1.426 +  (fn _ => [Auto_tac(),
   1.427 +	    etac dup_boxE 1,
   1.428 +	    auto_tac (temp_css addsimps2 [boxact_def]
   1.429 +		               addSIs2 [STL2bD_pr] addSEs2 [STL4E])
   1.430 +	   ]);
   1.431 +
   1.432 +qed_goal "TLA2" TLA.thy "P .& P` .-> Q  ==>  []P .-> []Q"
   1.433 +  (fn prems => [fast_tac (temp_cs addSIs prems addDs [temp_mp BoxPrime] addEs [STL4E]) 1]);
   1.434 +
   1.435 +qed_goal "TLA2E" TLA.thy 
   1.436 +   "[| (sigma |= []P); P .& P` .-> Q |] ==> (sigma |= []Q)"
   1.437 +   (fn prems => [REPEAT (resolve_tac (prems @ (prems RL [temp_mp TLA2])) 1)]);
   1.438 +
   1.439 +qed_goalw "DmdPrime" TLA.thy [dmd_def] "(<>P`) .-> (<>P)"
   1.440 +   (fn _ => [ fast_tac (temp_cs addSEs [TLA2E]) 1 ]);
   1.441 +
   1.442 +
   1.443 +(* ------------------------ INV1, stable --------------------------------------- *)
   1.444 +section "stable, invariant";
   1.445 +
   1.446 +qed_goal "ind_rule" TLA.thy
   1.447 +   "[| (sigma |= []H); (sigma |= Init(P)); H .-> (Init(P) .& .~[]F .-> Init(P`) .& F) |] \
   1.448 +\   ==> (sigma |= []F)"
   1.449 +   (fn prems => [rtac ((temp_mp indT) RS mp) 1,
   1.450 +		 REPEAT (resolve_tac (prems @ (prems RL [STL4E])) 1)]);
   1.451 +		 
   1.452 +
   1.453 +qed_goalw "INV1" TLA.thy [stable_def,boxact_def] 
   1.454 +  "Init(P) .& stable(P) .-> []P"
   1.455 +  (fn _ => [auto_tac (temp_css addsimps2 Init_simps addEs2 [ind_rule])]);
   1.456 +bind_thm("INV1I", temp_conjmp INV1);
   1.457 +
   1.458 +qed_goalw "StableL" TLA.thy [stable_def]
   1.459 +   "(P .& A .-> P`) ==> ([]A .-> stable(P))"
   1.460 +   (fn [prem] => [fast_tac (temp_cs addSIs [action_mp prem] addSEs [STL4E]) 1]);
   1.461 +
   1.462 +qed_goal "Stable" TLA.thy
   1.463 +   "[| (sigma |= []A); P .& A .-> P` |] ==> (sigma |= stable P)"
   1.464 +   (fn prems => [ REPEAT (resolve_tac (prems @ [temp_mp StableL]) 1) ]);
   1.465 +
   1.466 +(* Generalization of INV1 *)
   1.467 +qed_goalw "StableBox" TLA.thy [stable_def]
   1.468 +   "!!sigma. (sigma |= stable P) ==> (sigma |= [](Init P .-> []P))"
   1.469 +   (fn _ => [etac dup_boxE 1,
   1.470 +	     auto_tac (temp_css addsimps2 [stable_def] addEs2 [STL4E, INV1I])
   1.471 +	    ]);
   1.472 +     
   1.473 +(* useful for WF2 / SF2 *)
   1.474 +qed_goal "DmdStable" TLA.thy 
   1.475 +   "!!sigma. [| (sigma |= stable P); (sigma |= <>P) |] ==> (sigma |= <>[]P)"
   1.476 +   (fn _ => [rtac DmdImpl2 1,
   1.477 +	     etac StableBox 2,
   1.478 +	     auto_tac (temp_css addsimps2 [DmdAct])
   1.479 +	    ]);
   1.480 +
   1.481 +(* ---------------- (Semi-)automatic invariant tactics ---------------------- *)
   1.482 +
   1.483 +(* inv_tac reduces goals of the form ... ==> sigma |= []P *)
   1.484 +fun inv_tac css =
   1.485 +   SELECT_GOAL
   1.486 +     (EVERY [auto_tac css,
   1.487 +             TRY (merge_box_tac 1),
   1.488 +             rtac INV1I 1, (* fail if the goal is not a box *)
   1.489 +             TRYALL (etac Stable)]);
   1.490 +
   1.491 +(* auto_inv_tac applies inv_tac and then tries to attack the subgoals;
   1.492 +   in simple cases it may be able to handle goals like MyProg .-> []Inv.
   1.493 +   In these simple cases the simplifier seems to be more useful than the
   1.494 +   auto-tactic, which applies too much propositional logic and simplifies
   1.495 +   too late.
   1.496 +*)
   1.497 +
   1.498 +fun auto_inv_tac ss =
   1.499 +  SELECT_GOAL
   1.500 +    ((inv_tac (!claset,ss) 1) THEN
   1.501 +     (TRYALL (action_simp_tac (ss addsimps [Init_def,square_def]) [] [])));
   1.502 +
   1.503 +
   1.504 +qed_goalw "unless" TLA.thy [dmd_def]
   1.505 +   "!!sigma. (sigma |= [](P .-> P` .| Q`)) ==> (sigma |= stable P .| <>Q`)"
   1.506 +   (fn _ => [action_simp_tac (!simpset) [disjCI] [] 1,
   1.507 +	     merge_box_tac 1,
   1.508 +	     fast_tac (temp_cs addSEs [Stable]) 1
   1.509 +	    ]);
   1.510 +
   1.511 +
   1.512 +(* --------------------- Recursive expansions --------------------------------------- *)
   1.513 +section "recursive expansions";
   1.514 +
   1.515 +(* Recursive expansions of [] and <>, restricted to state predicates to avoid looping *)
   1.516 +qed_goal "BoxRec" TLA.thy "([]$P) .= (Init($P) .& ([]P$))"
   1.517 +   (fn _ => [auto_tac (temp_css addSIs2 [STL2bD]),
   1.518 +	     fast_tac (temp_cs addSEs [TLA2E]) 1,
   1.519 +	     auto_tac (temp_css addsimps2 [stable_def] addSEs2 [INV1I,STL4E])
   1.520 +	    ]);
   1.521 +
   1.522 +qed_goalw "DmdRec" TLA.thy [dmd_def] "(<>$P) .= (Init($P) .| (<>P$))"
   1.523 +   (fn _ => [Auto_tac(),
   1.524 +	     etac notE 1,
   1.525 +	     SELECT_GOAL (auto_tac (temp_css addsimps2 (stable_def::Init_simps)
   1.526 +				             addIs2 [INV1I] addEs2 [STL4E])) 1,
   1.527 +	     SELECT_GOAL (auto_tac (temp_css addsimps2 Init_simps addSDs2 [STL2bD])) 1,
   1.528 +	     fast_tac (temp_cs addSEs [notE,TLA2E]) 1
   1.529 +	    ]);
   1.530 +
   1.531 +qed_goal "DmdRec2" TLA.thy
   1.532 +   "!!sigma. [| (sigma |= <>($P)); (sigma |= [](.~P$)) |] ==> (sigma |= Init($P))"
   1.533 +   (fn _ => [dtac ((temp_unlift DmdRec) RS iffD1) 1,
   1.534 +	     SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1
   1.535 +	    ]);
   1.536 +
   1.537 +(* The "=>" part of the following is a little intricate. *)
   1.538 +qed_goal "InfinitePrime" TLA.thy "([]<>$P) .= ([]<>P$)"
   1.539 +   (fn _ => [Auto_tac(),
   1.540 +	     rtac classical 1,
   1.541 +	     rtac (temp_mp DBImplBDAct) 1,
   1.542 +	     subgoal_tac "sigma |= <>[]$P" 1,
   1.543 +	     fast_tac (temp_cs addSEs [DmdImplE,TLA2E]) 1,
   1.544 +	     subgoal_tac "sigma |= <>[](<>$P .& [].~P$)" 1,
   1.545 +	     SELECT_GOAL (auto_tac (temp_css addsimps2 [boxact_def]
   1.546 +				             addSEs2 [DmdImplE,STL4E,DmdRec2])) 1,
   1.547 +	     SELECT_GOAL (auto_tac (temp_css addSIs2 [temp_mp STL6] addsimps2 more_temp_simps)) 1,
   1.548 +	     fast_tac (temp_cs addIs [temp_mp DmdPrime] addSEs [STL4E]) 1
   1.549 +	    ]);
   1.550 +
   1.551 +(* ------------------------ fairness ------------------------------------------- *)
   1.552 +section "fairness";
   1.553 +
   1.554 +(* alternative definitions of fairness *)
   1.555 +qed_goalw "WF_alt" TLA.thy [WF_def,dmd_def] 
   1.556 +   "WF(A)_v .= (([]<>.~$(Enabled(<A>_v))) .| []<><A>_v)"
   1.557 +   (fn _ => [ fast_tac temp_cs 1 ]);
   1.558 +
   1.559 +qed_goalw "SF_alt" TLA.thy [SF_def,dmd_def]
   1.560 +   "SF(A)_v .= ((<>[].~$(Enabled(<A>_v))) .| []<><A>_v)"
   1.561 +   (fn _ => [ fast_tac temp_cs 1 ]);
   1.562 +
   1.563 +(* theorems to "box" fairness conditions *)
   1.564 +qed_goal "BoxWFI" TLA.thy
   1.565 +   "!!sigma. (sigma |= WF(A)_v) ==> (sigma |= []WF(A)_v)"
   1.566 +   (fn _ => [ auto_tac (temp_css addsimps2 (temp_rewrite WF_alt::more_temp_simps) addSIs2 [BoxOr]) ]);
   1.567 +
   1.568 +qed_goal "WF_Box" TLA.thy "([]WF(A)_v) .= WF(A)_v"
   1.569 +  (fn prems => [ fast_tac (temp_cs addSIs [BoxWFI] addSDs [STL2D]) 1 ]);
   1.570 +
   1.571 +qed_goal "BoxSFI" TLA.thy
   1.572 +   "!!sigma. (sigma |= SF(A)_v) ==> (sigma |= []SF(A)_v)"
   1.573 +   (fn _ => [ auto_tac (temp_css addsimps2 (temp_rewrite SF_alt::more_temp_simps) addSIs2 [BoxOr]) ]);
   1.574 +
   1.575 +qed_goal "SF_Box" TLA.thy "([]SF(A)_v) .= SF(A)_v"
   1.576 +  (fn prems => [ fast_tac (temp_cs addSIs [BoxSFI] addSDs [STL2D]) 1 ]);
   1.577 +
   1.578 +val more_temp_simps = more_temp_simps @ (map temp_rewrite [WF_Box, SF_Box]);
   1.579 +
   1.580 +qed_goalw "SFImplWF" TLA.thy [SF_def,WF_def]
   1.581 +  "!!sigma. (sigma |= SF(A)_v) ==> (sigma |= WF(A)_v)"
   1.582 +  (fn _ => [ fast_tac (temp_cs addSDs [temp_mp DBImplBDAct]) 1 ]);
   1.583 +
   1.584 +(* A tactic that "boxes" all fairness conditions. Apply more_temp_simps to "unbox". *)
   1.585 +val box_fair_tac = SELECT_GOAL (REPEAT (dresolve_tac [BoxWFI,BoxSFI] 1));
   1.586 +
   1.587 +
   1.588 +(* ------------------------------ leads-to ------------------------------ *)
   1.589 +
   1.590 +section "~>";
   1.591 +
   1.592 +qed_goalw "leadsto_init" TLA.thy [leadsto]
   1.593 +   "!!sigma. [| (sigma |= Init P); (sigma |= P ~> Q) |] ==> (sigma |= <>Q)"
   1.594 +   (fn _ => [ fast_tac (temp_cs addSDs [temp_mp STL2]) 1 ]);
   1.595 +
   1.596 +qed_goalw "streett_leadsto" TLA.thy [leadsto]
   1.597 +   "([]<>P .-> []<>Q) .= (<>(P ~> Q))"
   1.598 +   (fn _ => [Auto_tac(),
   1.599 +             asm_full_simp_tac (!simpset addsimps boxact_def::more_temp_simps) 1,
   1.600 +             SELECT_GOAL (auto_tac (temp_css addSEs2 [DmdImplE,STL4E] 
   1.601 +                                             addsimps2 Init_simps)) 1,
   1.602 +             SELECT_GOAL (auto_tac (temp_css addSIs2 [ImplDmdD] addSEs2 [STL4E])) 1,
   1.603 +             subgoal_tac "sigma |= []<><>Q" 1,
   1.604 +             asm_full_simp_tac (!simpset addsimps more_temp_simps) 1,
   1.605 +             rewtac (temp_rewrite DmdAct),
   1.606 +             dtac BoxDmdDmdBox 1, atac 1,
   1.607 +             auto_tac (temp_css addSEs2 [DmdImplE,STL4E])
   1.608 +            ]);
   1.609 +
   1.610 +qed_goal "leadsto_infinite" TLA.thy
   1.611 +   "!!sigma. [| (sigma |= []<>P); (sigma |= P ~> Q) |] ==> (sigma |= []<>Q)"
   1.612 +   (fn _ => [rtac ((temp_unlift streett_leadsto) RS iffD2 RS mp) 1,
   1.613 +             auto_tac (temp_css addSIs2 [ImplDmdD])
   1.614 +            ]);
   1.615 +
   1.616 +(* In particular, strong fairness is a Streett condition. The following
   1.617 +   rules are sometimes easier to use than WF2 or SF2 below.
   1.618 +*)
   1.619 +qed_goalw "leadsto_SF" TLA.thy [SF_def]
   1.620 +  "!!sigma. (sigma |= $(Enabled(<A>_v)) ~> <A>_v) ==> sigma |= SF(A)_v"
   1.621 +  (fn _ => [step_tac temp_cs 1,
   1.622 +            rtac leadsto_infinite 1,
   1.623 +            ALLGOALS atac
   1.624 +           ]);
   1.625 +
   1.626 +bind_thm("leadsto_WF", leadsto_SF RS SFImplWF);
   1.627 +
   1.628 +(* introduce an invariant into the proof of a leadsto assertion.
   1.629 +   []I => ((P ~> Q)  =  (P /\ I ~> Q))
   1.630 +*)
   1.631 +qed_goalw "INV_leadsto" TLA.thy [leadsto]
   1.632 +   "!!sigma. [| (sigma |= []I); (sigma |= (P .& I) ~> Q) |] ==> (sigma |= P ~> Q)"
   1.633 +   (fn _ => [etac STL4Edup 1, atac 1,
   1.634 +	     auto_tac (temp_css addsimps2 [Init_def] addSDs2 [STL2bD])
   1.635 +	    ]);
   1.636 +
   1.637 +qed_goalw "leadsto_classical" TLA.thy [leadsto,dmd_def]
   1.638 +   "!!sigma. (sigma |= [](Init P .& [].~Q .-> <>Q)) ==> (sigma |= P ~> Q)"
   1.639 +   (fn _ => [fast_tac (temp_cs addSEs [STL4E]) 1]);
   1.640 +
   1.641 +qed_goalw "leadsto_false" TLA.thy [leadsto]
   1.642 +  "(P ~> #False) .= ([] .~P)"
   1.643 +  (fn _ => [ auto_tac (temp_css addsimps2 boxact_def::Init_simps) ]);
   1.644 +
   1.645 +(* basic leadsto properties, cf. Unity *)
   1.646 +
   1.647 +qed_goal "ImplLeadsto" TLA.thy
   1.648 +   "!!sigma. (sigma |= [](P .-> Q)) ==> (sigma |= (P ~> Q))"
   1.649 +   (fn _ => [etac INV_leadsto 1, rewtac leadsto,
   1.650 +	     rtac (temp_unlift necT) 1,
   1.651 +	     auto_tac (temp_css addSIs2 [InitDmdD] addsimps2 [Init_def])
   1.652 +	    ]);
   1.653 +
   1.654 +qed_goal "EnsuresLeadsto" TLA.thy
   1.655 +   "A .& P .-> Q` ==> []A .-> (P ~> Q)"
   1.656 +   (fn [prem] => [auto_tac (temp_css addSEs2 [INV_leadsto]),
   1.657 +		  rewtac leadsto,
   1.658 + 		  auto_tac (temp_css addSIs2 [temp_unlift necT]),
   1.659 +		  rtac (temp_mp DmdPrime) 1, rtac InitDmdD 1,
   1.660 +		  auto_tac (action_css addsimps2 [Init_def] addSIs2 [action_mp prem])
   1.661 +		 ]);
   1.662 +
   1.663 +qed_goalw "EnsuresLeadsto2" TLA.thy [leadsto]
   1.664 +   "!!sigma. sigma |= [](P .-> Q`) ==> sigma |= P ~> Q"
   1.665 +   (fn _ => [subgoal_tac "sigma |= []Init(P .-> Q`)" 1,
   1.666 +             etac STL4E 1,
   1.667 +             auto_tac (temp_css addsimps2 boxact_def::Init_simps 
   1.668 +                                addIs2 [(temp_mp InitDmd) RS (temp_mp DmdPrime)])
   1.669 +            ]);
   1.670 +             
   1.671 +qed_goal "EnsuresInfinite" TLA.thy
   1.672 +   "[| (sigma |= []<>P); (sigma |= []A); A .& P .-> Q` |] ==> (sigma |= []<>Q)"
   1.673 +   (fn prems => [REPEAT (resolve_tac (prems @ [leadsto_infinite,
   1.674 +					       temp_mp EnsuresLeadsto]) 1)]);
   1.675 +
   1.676 +(*** Gronning's lattice rules (taken from TLP) ***)
   1.677 +section "Lattice rules";
   1.678 +
   1.679 +qed_goalw "LatticeReflexivity" TLA.thy [leadsto] "F ~> F"
   1.680 +   (fn _ => [REPEAT (resolve_tac [necT,InitDmd] 1)]);
   1.681 +
   1.682 +qed_goalw "LatticeTransitivity" TLA.thy [leadsto]
   1.683 +   "!!sigma. [| (sigma |= G ~> H); (sigma |= F ~> G) |] ==> (sigma |= F ~> H)"
   1.684 +   (fn _ => [etac dup_boxE 1,  (* [][](Init G .-> H) *)
   1.685 +	     merge_box_tac 1,
   1.686 +	     auto_tac (temp_css addSEs2 [STL4E]),
   1.687 +	     rewtac (temp_rewrite DmdAct),
   1.688 +	     subgoal_tac "sigmaa |= <><> Init H" 1,
   1.689 +	     asm_full_simp_tac (!simpset addsimps more_temp_simps) 1,
   1.690 +	     fast_tac (temp_cs addSEs [DmdImpl2]) 1
   1.691 +	    ]);
   1.692 +
   1.693 +qed_goalw "LatticeDisjunctionElim1" TLA.thy [leadsto]
   1.694 +   "!!sigma. (sigma |= (F .| G) ~> H) ==> (sigma |= F ~> H)"
   1.695 +   (fn _ => [ auto_tac (temp_css addsimps2 [Init_def] addSEs2 [STL4E]) ]);
   1.696 +
   1.697 +qed_goalw "LatticeDisjunctionElim2" TLA.thy [leadsto]
   1.698 +   "!!sigma. (sigma |= (F .| G) ~> H) ==> (sigma |= G ~> H)"
   1.699 +   (fn _ => [ auto_tac (temp_css addsimps2 [Init_def] addSEs2 [STL4E]) ]);
   1.700 +
   1.701 +qed_goalw "LatticeDisjunctionIntro" TLA.thy [leadsto]
   1.702 +   "!!sigma. [| (sigma |= F ~> H); (sigma |= G ~> H) |] ==> (sigma |= (F .| G) ~> H)"
   1.703 +   (fn _ => [merge_box_tac 1,
   1.704 +	     auto_tac (temp_css addsimps2 [Init_def] addSEs2 [STL4E])
   1.705 +	    ]);
   1.706 +
   1.707 +qed_goal "LatticeDiamond" TLA.thy
   1.708 +   "!!sigma. [| (sigma |= B ~> D); (sigma |= A ~> (B .| C)); (sigma |= C ~> D) |]  \
   1.709 +\            ==> (sigma |= A ~> D)"
   1.710 +   (fn _ => [subgoal_tac "sigma |= (B .| C) ~> D" 1,
   1.711 +	     eres_inst_tac [("G", "B .| C")] LatticeTransitivity 1,
   1.712 +	     ALLGOALS (fast_tac (temp_cs addSIs [LatticeDisjunctionIntro]))
   1.713 +	    ]);
   1.714 +
   1.715 +qed_goal "LatticeTriangle" TLA.thy
   1.716 +   "!!sigma. [| (sigma |= B ~> D); (sigma |= A ~> (B .| D)) |] ==> (sigma |= A ~> D)"
   1.717 +   (fn _ => [subgoal_tac "sigma |= (B .| D) ~> D" 1,
   1.718 +	     eres_inst_tac [("G", "B .| D")] LatticeTransitivity 1, atac 1,
   1.719 +	     auto_tac (temp_css addSIs2 [LatticeDisjunctionIntro] addIs2 [ImplLeadsto])
   1.720 +	    ]);
   1.721 +
   1.722 +(*** Lamport's fairness rules ***)
   1.723 +section "Fairness rules";
   1.724 +
   1.725 +qed_goalw "WF1" TLA.thy [leadsto]
   1.726 +   "[| P .& N  .-> P` .| Q`;   \
   1.727 +\      P .& N .& <A>_v .-> Q`;   \
   1.728 +\      P .& N .-> $(Enabled(<A>_v)) |]   \
   1.729 +\  ==> []N .& WF(A)_v .-> (P ~> Q)"
   1.730 +   (fn [prem1,prem2,prem3]
   1.731 +             => [auto_tac (temp_css addSDs2 [BoxWFI]),
   1.732 +		 etac STL4Edup 1, atac 1,
   1.733 +		 Auto_tac(),
   1.734 +		 subgoal_tac "sigmaa |= [](P .-> P` .| Q`)" 1,
   1.735 +		 auto_tac (temp_css addSDs2 [unless]),
   1.736 +		 etac (temp_conjimpE INV1) 1, atac 1,
   1.737 +		 merge_box_tac 1,
   1.738 +		 rtac STL2D 1,
   1.739 +		 rtac EnsuresInfinite 1, atac 2,
   1.740 +		 SELECT_GOAL (auto_tac (temp_css addsimps2 [WF_alt])) 1,
   1.741 +		 atac 2,
   1.742 +		 subgoal_tac "sigmaa |= [][]$(Enabled(<A>_v))" 1,
   1.743 +		 merge_box_tac 1,
   1.744 +		 SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1,
   1.745 +		 SELECT_GOAL ((rewtac (temp_rewrite STL3)) THEN
   1.746 +			      (auto_tac (temp_css addSEs2 [STL4E] addSIs2 [action_mp prem3]))) 1,
   1.747 +		 fast_tac (action_cs addSIs [action_mp prem2]) 1,
   1.748 +		 fast_tac (temp_cs addIs [temp_mp DmdPrime]) 1,
   1.749 +		 fast_tac (temp_cs addSEs [STL4E] addSIs [action_mp prem1]) 1
   1.750 +		]);
   1.751 +
   1.752 +(* Sometimes easier to use; designed for action B rather than state predicate Q *)
   1.753 +qed_goalw "WF_leadsto" TLA.thy [leadsto]
   1.754 +   "[| N .& P .-> $Enabled (<A>_v);            \
   1.755 +\      N .& <A>_v .-> B;                  \ 
   1.756 +\      [](N .& [.~A]_v) .-> stable P  |]  \
   1.757 +\   ==> []N .& WF(A)_v .-> (P ~> B)"
   1.758 +   (fn [prem1,prem2,prem3]
   1.759 +       => [auto_tac (temp_css addSDs2 [BoxWFI]),
   1.760 +           etac STL4Edup 1, atac 1,
   1.761 +           Auto_tac(),
   1.762 +           subgoal_tac "sigmaa |= <><A>_v" 1,
   1.763 +           SELECT_GOAL (auto_tac (temp_css addSEs2 [DmdImpl2,STL4E] addSIs2 [action_mp prem2])) 1,
   1.764 +           rtac classical 1,
   1.765 +           rtac STL2D 1,
   1.766 +           auto_tac (temp_css addsimps2 WF_def::more_temp_simps addSEs2 [mp]),
   1.767 +           rtac ImplDmdD 1,
   1.768 +           rtac (temp_mp (prem1 RS STL4)) 1,
   1.769 +           auto_tac (temp_css addsimps2 [split_box_conj]),
   1.770 +           etac INV1I 1,
   1.771 +           merge_act_box_tac 1,
   1.772 +           auto_tac (temp_css addsimps2 [temp_rewrite not_angle] addSEs2 [temp_mp prem3])
   1.773 +          ]);
   1.774 +
   1.775 +qed_goalw "SF1" TLA.thy [leadsto]
   1.776 +   "[| P .& N  .-> P` .| Q`;   \
   1.777 +\      P .& N .& <A>_v .-> Q`;   \
   1.778 +\      []P .& []N .& []F .-> <>$(Enabled(<A>_v)) |]   \
   1.779 +\  ==> []N .& SF(A)_v .& []F .-> (P ~> Q)"
   1.780 +   (fn [prem1,prem2,prem3] =>
   1.781 +                [auto_tac (temp_css addSDs2 [BoxSFI]),
   1.782 +		 eres_inst_tac [("F","F")] dup_boxE 1,
   1.783 +		 merge_temp_box_tac 1,
   1.784 +		 etac STL4Edup 1, atac 1,
   1.785 +		 Auto_tac(),
   1.786 +		 subgoal_tac "sigmaa |= [](P .-> P` .| Q`)" 1,
   1.787 +		 auto_tac (temp_css addSDs2 [unless]),
   1.788 +		 etac (temp_conjimpE INV1) 1, atac 1,
   1.789 +		 merge_act_box_tac 1,
   1.790 +		 rtac STL2D 1,
   1.791 +		 rtac EnsuresInfinite 1, atac 2,
   1.792 +		 SELECT_GOAL (auto_tac (temp_css addsimps2 [SF_alt])) 1,
   1.793 +		 atac 2,
   1.794 +		 subgoal_tac "sigmaa |= []<>$(Enabled(<A>_v))" 1,
   1.795 +		 SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1,
   1.796 +		 eres_inst_tac [("F","F")] dup_boxE 1,
   1.797 +		 etac STL4Edup 1, atac 1,
   1.798 +		 fast_tac (temp_cs addSEs [STL4E] addSIs [temp_mp prem3]) 1,
   1.799 +		 fast_tac (action_cs addSIs [action_mp prem2]) 1,
   1.800 +		 fast_tac (temp_cs addIs [temp_mp DmdPrime]) 1,
   1.801 +		 fast_tac (temp_cs addSEs [STL4E] addSIs [action_mp prem1]) 1
   1.802 +		]);
   1.803 +
   1.804 +qed_goal "WF2" TLA.thy
   1.805 +   "[| N .& <B>_f .-> <M>_g;   \
   1.806 +\      P .& P` .& <N .& A>_f .-> B;   \
   1.807 +\      P .& $(Enabled(<M>_g)) .-> $(Enabled(<A>_f));   \
   1.808 +\      [](N .& [.~B]_f) .& WF(A)_f .& []F .& <>[]($(Enabled(<M>_g))) .-> <>[]P |]   \
   1.809 +\  ==> []N .& WF(A)_f .& []F .-> WF(M)_g"
   1.810 +   (fn [prem1,prem2,prem3,prem4]
   1.811 +       => [Auto_tac(),
   1.812 +	   case_tac "sigma |= <>[]$Enabled(<M>_g)" 1,
   1.813 +	   SELECT_GOAL (auto_tac (temp_css addsimps2 [WF_def,dmd_def])) 2,
   1.814 +	   case_tac "sigma |= <>[][.~B]_f" 1,
   1.815 +	   subgoal_tac "sigma |= <>[]P" 1,
   1.816 +	   asm_full_simp_tac (!simpset addsimps [WF_def]) 1,
   1.817 +	   rtac (temp_mp (prem1 RS DmdImpl RS STL4)) 1,
   1.818 +	   eres_inst_tac [("V","sigma |= <>[][.~B]_f")] thin_rl 1,
   1.819 +	   etac (temp_conjimpE STL6) 1, atac 1,
   1.820 +	   subgoal_tac "sigma |= <>[]$Enabled(<A>_f)" 1,
   1.821 +	   dtac mp 1, atac 1,
   1.822 +	   subgoal_tac "sigma |= <>([]N .& []P .& []<><A>_f)" 1,
   1.823 +	   rtac ((temp_unlift DmdBoxDmd) RS iffD1) 1,
   1.824 +	   eres_inst_tac [("F","[]N .& []P .& []<><A>_f")] DmdImplE 1,
   1.825 +	   SELECT_GOAL (Auto_tac()) 1,
   1.826 +	   dres_inst_tac [("P","P")] (temp_mp BoxPrime) 1,
   1.827 +	   merge_act_box_tac 1,
   1.828 +	   etac InfImpl 1, atac 1,
   1.829 +	   SELECT_GOAL (auto_tac (temp_css addsimps2 [angle_def] addSIs2 [action_mp prem2])) 1,
   1.830 +	   etac BoxDmd 1,
   1.831 +	   dres_inst_tac [("F","<><A>_f"),("G","[]P")] BoxDmd 1, atac 1,
   1.832 +	   eres_inst_tac [("F","[]<><A>_f .& []P")] DmdImplE 1,
   1.833 +	   SELECT_GOAL (Auto_tac ()) 1,
   1.834 +	   rtac (temp_mp (prem3 RS STL4 RS DmdImpl)) 1,
   1.835 +	   fast_tac (temp_cs addIs [STL4E,DmdImplE]) 1,
   1.836 +	   etac (temp_conjimpE STL6) 1, atac 1,
   1.837 +	   eres_inst_tac [("V","sigma |= <>[][.~ B]_f")] thin_rl 1,
   1.838 +	   dtac BoxWFI 1,
   1.839 +	   eres_inst_tac [("F","N")] dup_boxE 1,
   1.840 +	   eres_inst_tac [("F","F")] dup_boxE 1,
   1.841 +	   merge_temp_box_tac 1,
   1.842 +	   dtac BoxDmd 1, atac 1,
   1.843 +	   eres_inst_tac [("V","sigma |= <>[]($Enabled (<M>_g) .& [.~ B]_f)")] thin_rl 1,
   1.844 +	   rtac dup_dmdD 1,
   1.845 +	   rtac (temp_mp (prem4 RS DmdImpl)) 1,
   1.846 +	   etac DmdImplE 1,
   1.847 +	   SELECT_GOAL
   1.848 +	     (auto_tac (temp_css addsimps2 [symmetric(temp_rewrite STL5), temp_rewrite STL3]
   1.849 +		                 addIs2 [(temp_unlift WF_Box) RS iffD1, temp_mp ImplDmd])) 1,
   1.850 +	   asm_full_simp_tac (!simpset addsimps (WF_def::more_temp_simps)) 1,
   1.851 +	   etac InfImpl 1, atac 1,
   1.852 +	   SELECT_GOAL (auto_tac (temp_css addSIs2 [action_mp prem1])) 1,
   1.853 +	   ALLGOALS (asm_full_simp_tac (!simpset addsimps [square_def,angle_def]))
   1.854 +	  ]);
   1.855 +
   1.856 +qed_goal "SF2" TLA.thy
   1.857 +   "[| N .& <B>_f .-> <M>_g;   \
   1.858 +\      P .& P` .& <N .& A>_f .-> B;   \
   1.859 +\      P .& $(Enabled(<M>_g)) .-> $(Enabled(<A>_f));   \
   1.860 +\      [](N .& [.~B]_f) .& SF(A)_f .& []F .& []<>($(Enabled(<M>_g))) .-> <>[]P |]   \
   1.861 +\  ==> []N .& SF(A)_f .& []F .-> SF(M)_g"
   1.862 +   (fn [prem1,prem2,prem3,prem4]
   1.863 +       => [Auto_tac(),
   1.864 +	   case_tac "sigma |= []<>$Enabled(<M>_g)" 1,
   1.865 +	   SELECT_GOAL (auto_tac (temp_css addsimps2 [SF_def,dmd_def])) 2,
   1.866 +	   case_tac "sigma |= <>[][.~B]_f" 1,
   1.867 +	   subgoal_tac "sigma |= <>[]P" 1,
   1.868 +	   asm_full_simp_tac (!simpset addsimps [SF_def]) 1,
   1.869 +	   rtac (temp_mp (prem1 RS DmdImpl RS STL4)) 1,
   1.870 +	   eres_inst_tac [("V","sigma |= <>[][.~B]_f")] thin_rl 1,
   1.871 +	   dtac BoxDmdDmdBox 1, atac 1,
   1.872 +	   subgoal_tac "sigma |= []<>$Enabled(<A>_f)" 1,
   1.873 +	   dtac mp 1, atac 1,
   1.874 +	   subgoal_tac "sigma |= <>([]N .& []P .& []<><A>_f)" 1,
   1.875 +	   rtac ((temp_unlift DmdBoxDmd) RS iffD1) 1,
   1.876 +	   eres_inst_tac [("F","[]N .& []P .& []<><A>_f")] DmdImplE 1,
   1.877 +	   SELECT_GOAL (Auto_tac()) 1,
   1.878 +	   dres_inst_tac [("P","P")] (temp_mp BoxPrime) 1,
   1.879 +	   merge_act_box_tac 1,
   1.880 +	   etac InfImpl 1, atac 1,
   1.881 +	   SELECT_GOAL (auto_tac (temp_css addsimps2 [angle_def] addSIs2 [action_mp prem2])) 1,
   1.882 +	   etac BoxDmd 1,
   1.883 +	   dres_inst_tac [("F","<><A>_f"),("G","[]P")] BoxDmd 1, atac 1,
   1.884 +	   eres_inst_tac [("F","[]<><A>_f .& []P")] DmdImplE 1,
   1.885 +	   SELECT_GOAL (Auto_tac ()) 1,
   1.886 +	   rtac (temp_mp (prem3 RS DmdImpl RS STL4)) 1,
   1.887 +	   fast_tac (temp_cs addEs [STL4E,DmdImplE]) 1,
   1.888 +	   dtac BoxSFI 1,
   1.889 +	   eres_inst_tac [("F","N")] dup_boxE 1,
   1.890 +	   eres_inst_tac [("F","F")] dup_boxE 1,
   1.891 +	   eres_inst_tac [("F","<>$Enabled (<M>_g)")] dup_boxE 1,
   1.892 +	   merge_temp_box_tac 1,
   1.893 +	   dtac (temp_conjmp BoxDmdT2) 1, atac 1,
   1.894 +	   rtac dup_dmdD 1,
   1.895 +	   rtac (temp_mp (prem4 RS DmdImpl)) 1,
   1.896 +	   SELECT_GOAL
   1.897 +	     (auto_tac (temp_css addsimps2 [symmetric(temp_rewrite STL5), temp_rewrite STL3]
   1.898 +		                 addIs2 [(temp_unlift WF_Box) RS iffD1, temp_mp ImplDmd]
   1.899 +			         addSEs2 [DmdImplE])) 1,
   1.900 +	   asm_full_simp_tac (!simpset addsimps (SF_def::more_temp_simps)) 1,
   1.901 +	   eres_inst_tac [("F",".~ [.~ B]_f")] InfImpl 1, atac 1,
   1.902 +	   SELECT_GOAL (auto_tac (temp_css addSIs2 [action_mp prem1])) 1,
   1.903 +	   ALLGOALS (asm_full_simp_tac (!simpset addsimps [square_def,angle_def]))
   1.904 +	  ]);
   1.905 +
   1.906 +(* ------------------------------------------------------------------------- *)
   1.907 +(***           Liveness proofs by well-founded orderings                   ***)
   1.908 +(* ------------------------------------------------------------------------- *)
   1.909 +section "Well-founded orderings";
   1.910 +
   1.911 +qed_goal "wf_dmd" TLA.thy
   1.912 +  "[| (wf r);  \
   1.913 +\     !!x. sigma |= [](F x .-> <>G .| <>(REX y. #((y,x):r) .& F y))   \
   1.914 +\  |] ==> sigma |= [](F x .-> <>G)"
   1.915 +  (fn prem1::prems => 
   1.916 +         [cut_facts_tac [prem1] 1,
   1.917 +          etac wf_induct 1,
   1.918 +          subgoal_tac "sigma |= []((REX y. #((y,x):r) .& F y) .-> <>G)" 1,
   1.919 +	  cut_facts_tac prems 1,
   1.920 +	  etac STL4Edup 1, atac 1,
   1.921 +	  Auto_tac(), etac swap 1, atac 1,
   1.922 +	  rtac dup_dmdD 1,
   1.923 +	  etac DmdImpl2 1, atac 1,
   1.924 +	  subgoal_tac "sigma |= [](RALL y. #((y,x):r) .& F y .-> <>G)" 1,
   1.925 +	  fast_tac (temp_cs addSEs [STL4E]) 1,
   1.926 +	  auto_tac (temp_css addsimps2 [all_box]),
   1.927 +	  etac allE 1, etac impCE 1,
   1.928 +	  rtac (temp_unlift necT) 1,
   1.929 +	  auto_tac (temp_css addSEs2 [STL4E])
   1.930 +         ]);
   1.931 +
   1.932 +(* Special case: leadsto via well-foundedness *)
   1.933 +qed_goalw "wf_leadsto" TLA.thy [leadsto]
   1.934 +  "[| (wf r);  \
   1.935 +\     !!x. sigma |= P x ~> (Q .| (REX y. #((y,x):r) .& P y))   \
   1.936 +\  |] ==> sigma |= P x ~> Q"
   1.937 +  (fn prems => [REPEAT (resolve_tac (wf_dmd::prems) 1),
   1.938 +		resolve_tac (prems RL [STL4E]) 1,
   1.939 +		auto_tac (temp_css addsimps2 [temp_rewrite DmdOr]),
   1.940 +                fast_tac temp_cs 1,
   1.941 +		etac swap 1,
   1.942 +		rewtac (temp_rewrite DmdAct),
   1.943 +		auto_tac (temp_css addsimps2 [Init_def] addSEs2 [DmdImplE])
   1.944 +	       ]);
   1.945 +
   1.946 +(* If r is well-founded, state function v cannot decrease forever *)
   1.947 +qed_goal "wf_not_box_decrease" TLA.thy
   1.948 +  "!!r. wf r ==> [][ {[v$, $v]} .: #r ]_v .-> <>[][#False]_v"
   1.949 +  (fn _ => [Auto_tac(),
   1.950 +            subgoal_tac "ALL x. (sigma |= [](Init($v .= #x) .-> <>[][#False]_v))" 1,
   1.951 +            etac allE 1,
   1.952 +            dtac STL2D 1,
   1.953 +            auto_tac (temp_css addsimps2 [Init_def]),
   1.954 +            etac wf_dmd 1,
   1.955 +            etac dup_boxE 1,
   1.956 +            etac STL4E 1,
   1.957 +            action_simp_tac (!simpset addsimps [con_abs]) [tempI] [] 1,
   1.958 +            case_tac "sigma |= <>[][#False]_v" 1,
   1.959 +            ALLGOALS Asm_full_simp_tac,
   1.960 +            rewrite_goals_tac more_temp_simps,
   1.961 +            dtac STL2D 1,
   1.962 +            subgoal_tac "sigma |= <>(REX y. #((y, xa) : r) .& ($v .= #y))" 1,
   1.963 +            SELECT_GOAL (auto_tac (temp_css addsimps2 [DmdAct,Init_def] 
   1.964 +                                            addEs2 [DmdImplE])) 1,
   1.965 +            subgoal_tac "sigma |= (stable ($v .= #xa) .| <>(REX y. #((y, xa) : r) .& $v .= #y)`)" 1,
   1.966 +            case_tac "sigma |= stable ($v .= #xa)" 1,
   1.967 +            SELECT_GOAL (auto_tac (temp_css addIs2 [temp_mp DmdPrime])) 2,
   1.968 +            SELECT_GOAL (rewrite_goals_tac ((symmetric (temp_rewrite NotBox))::action_rews)) 1,
   1.969 +            etac swap 1,
   1.970 +            subgoal_tac "sigma |= []($v .= #xa)" 1,
   1.971 +            dres_inst_tac [("P", "$v .= #xa")] (temp_mp BoxPrime) 1,
   1.972 +            SELECT_GOAL (auto_tac (temp_css addEs2 [STL4E] addsimps2 [square_def])) 1,
   1.973 +            SELECT_GOAL (auto_tac (temp_css addSIs2 [INV1I] addsimps2 [Init_def])) 1,
   1.974 +            auto_tac (temp_css addsimps2 [square_def] addSIs2 [unless] addSEs2 [STL4E])
   1.975 +           ]);
   1.976 +
   1.977 +(* "wf ?r  ==>  <>[][{[?v$, $?v]} .: #?r]_?v .-> <>[][#False]_?v" *)
   1.978 +bind_thm("wf_not_dmd_box_decrease",
   1.979 +         standard(rewrite_rule more_temp_simps (wf_not_box_decrease RS DmdImpl)));
   1.980 +
   1.981 +(* If there are infinitely many steps where v decreases w.r.t. r, then there
   1.982 +   have to be infinitely many non-stuttering steps where v doesn't decrease.
   1.983 +*)
   1.984 +qed_goal "wf_box_dmd_decrease" TLA.thy
   1.985 +  "wf r ==> []<>({[v$, $v]} .: #r) .-> []<><.~({[v$, $v]} .: #r)>_v"
   1.986 +  (fn [prem] => [Auto_tac(),
   1.987 +                 rtac ccontr 1,
   1.988 +                 asm_full_simp_tac 
   1.989 +                   (!simpset addsimps ([action_rewrite not_angle] @ more_temp_simps)) 1,
   1.990 +                 dtac (prem RS (temp_mp wf_not_dmd_box_decrease)) 1,
   1.991 +                 dtac BoxDmdDmdBox 1, atac 1,
   1.992 +                 subgoal_tac "sigma |= []<>((#False)::action)" 1,
   1.993 +                 SELECT_GOAL (Auto_tac()) 1,
   1.994 +                 etac STL4E 1,
   1.995 +                 rtac DmdImpl 1,
   1.996 +                 auto_tac (action_css addsimps2 [square_def] addSEs2 [prem RS wf_irrefl])
   1.997 +                ]);
   1.998 +
   1.999 +(* In particular, for natural numbers, if n decreases infinitely often
  1.1000 +   then it has to increase infinitely often.
  1.1001 +*)
  1.1002 +qed_goal "nat_box_dmd_decrease" TLA.thy
  1.1003 +  "!!n::nat stfun. []<>(n$ .< $n) .-> []<>($n .< n$)"
  1.1004 +  (fn _ => [Auto_tac(),
  1.1005 +            subgoal_tac "sigma |= []<><.~( {[n$,$n]} .: #less_than)>_n" 1,
  1.1006 +            etac thin_rl 1, etac STL4E 1, rtac DmdImpl 1,
  1.1007 +            SELECT_GOAL (auto_tac (!claset, !simpset addsimps [angle_def])) 1,
  1.1008 +            rtac nat_less_cases 1,
  1.1009 +            Auto_tac(),
  1.1010 +            rtac (temp_mp wf_box_dmd_decrease) 1,
  1.1011 +            auto_tac (!claset addSEs [STL4E] addSIs [DmdImpl], !simpset)
  1.1012 +           ]);
  1.1013 +
  1.1014 +(* ------------------------------------------------------------------------- *)
  1.1015 +(***           Flexible quantification over state variables                ***)
  1.1016 +(* ------------------------------------------------------------------------- *)
  1.1017 +section "Flexible quantification";
  1.1018 +
  1.1019 +qed_goal "aallI" TLA.thy 
  1.1020 +  "(!!x. base_var x ==> sigma |= F x) ==> sigma |= (AALL x. F(x))"
  1.1021 +  (fn prems => [auto_tac (temp_css addsimps2 [aall_def] addSEs2 [eexE] addSDs2 prems)]);
  1.1022 +
  1.1023 +qed_goal "aallE" TLA.thy
  1.1024 +   "[| sigma |= (AALL x. F(x));  (!!sigma. sigma |= F(x) ==> P sigma) |] \
  1.1025 +\   ==> (P sigma)::bool"
  1.1026 +   (fn prems => [cut_facts_tac prems 1,
  1.1027 +		 resolve_tac prems 1,
  1.1028 +		 rewrite_goals_tac (aall_def::intensional_rews),
  1.1029 +		 etac swap 1,
  1.1030 +		 auto_tac (temp_css addSIs2 [temp_mp eexI])
  1.1031 +		]);
  1.1032 +
  1.1033 +(* monotonicity of quantification *)
  1.1034 +qed_goal "eex_mono" TLA.thy
  1.1035 +  "[| sigma |= EEX x. F(x); !!x. F(x) .-> G(x) |] ==> sigma |= EEX x. G(x)"
  1.1036 +  (fn [min,maj] => [cut_facts_tac [min] 1,
  1.1037 +                    etac eexE 1,
  1.1038 +                    REPEAT (ares_tac (map temp_mp [eexI,maj]) 1)
  1.1039 +                   ]);
  1.1040 +
  1.1041 +qed_goal "aall_mono" TLA.thy
  1.1042 +  "[| sigma |= AALL x. F(x); !!x. F(x) .-> G(x) |] ==> sigma |= AALL x. G(x)"
  1.1043 +  (fn [min,maj] => [cut_facts_tac [min] 1,
  1.1044 +                    fast_tac (temp_cs addSIs [aallI, temp_mp maj]
  1.1045 +                                      addEs [aallE]) 1
  1.1046 +                   ]);
  1.1047 +
  1.1048 +(* ----------------------------------------------------------------------
  1.1049 +   example of a history variable: existence of a clock
  1.1050 +
  1.1051 +goal TLA.thy "(EEX h. Init($h .= #True) .& [](h$ .~= $h))";
  1.1052 +br tempI 1;
  1.1053 +br historyI 1;
  1.1054 +bws action_rews;
  1.1055 +by (TRYALL (rtac impI));
  1.1056 +by (TRYALL (etac conjE));
  1.1057 +ba 3;
  1.1058 +by (Asm_full_simp_tac 3);
  1.1059 +by (auto_tac (temp_css addSIs2 [(temp_unlift Init_true) RS iffD2, temp_unlift BoxTrue]));
  1.1060 +(** solved **)
  1.1061 +
  1.1062 +---------------------------------------------------------------------- *)