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.51 +
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.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.345 +val temp_css = temp_css addsimps2 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.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.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.430 +	   ]);
1.431 +
1.432 +qed_goal "TLA2" TLA.thy "P .& P` .-> Q  ==>  []P .-> []Q"
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.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.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.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.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.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.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.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.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.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.620 +  "!!sigma. (sigma |= \$(Enabled(<A>_v)) ~> <A>_v) ==> sigma |= SF(A)_v"
1.621 +  (fn _ => [step_tac temp_cs 1,
1.623 +            ALLGOALS atac
1.624 +           ]);
1.625 +
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.632 +   "!!sigma. [| (sigma |= []I); (sigma |= (P .& I) ~> Q) |] ==> (sigma |= P ~> Q)"
1.633 +   (fn _ => [etac STL4Edup 1, atac 1,
1.635 +	    ]);
1.636 +
1.638 +   "!!sigma. (sigma |= [](Init P .& [].~Q .-> <>Q)) ==> (sigma |= P ~> Q)"
1.639 +   (fn _ => [fast_tac (temp_cs addSEs [STL4E]) 1]);
1.640 +
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.648 +   "!!sigma. (sigma |= [](P .-> Q)) ==> (sigma |= (P ~> Q))"
1.650 +	     rtac (temp_unlift necT) 1,
1.652 +	    ]);
1.653 +
1.655 +   "A .& P .-> Q` ==> []A .-> (P ~> Q)"
1.658 + 		  auto_tac (temp_css addSIs2 [temp_unlift necT]),
1.659 +		  rtac (temp_mp DmdPrime) 1, rtac InitDmdD 1,
1.661 +		 ]);
1.662 +
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.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.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.694 +   "!!sigma. (sigma |= (F .| G) ~> H) ==> (sigma |= F ~> H)"
1.695 +   (fn _ => [ auto_tac (temp_css addsimps2 [Init_def] addSEs2 [STL4E]) ]);
1.696 +
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.702 +   "!!sigma. [| (sigma |= F ~> H); (sigma |= G ~> H) |] ==> (sigma |= (F .| G) ~> H)"
1.703 +   (fn _ => [merge_box_tac 1,
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.720 +	    ]);
1.721 +
1.722 +(*** Lamport's fairness rules ***)
1.723 +section "Fairness rules";
1.724 +
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.747 +		 fast_tac (action_cs addSIs [action_mp prem2]) 1,
1.748 +		 fast_tac (temp_cs addIs [temp_mp DmdPrime]) 1,
1.750 +		]);
1.751 +
1.752 +(* Sometimes easier to use; designed for action B rather than state predicate Q *)
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.764 +           rtac classical 1,
1.765 +           rtac STL2D 1,
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.773 +          ]);
1.774 +
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.799 +		 fast_tac (action_cs addSIs [action_mp prem2]) 1,
1.800 +		 fast_tac (temp_cs addIs [temp_mp DmdPrime]) 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.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.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.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.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.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.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.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.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.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.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.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 +---------------------------------------------------------------------- *)
```