src/HOL/TLA/TLA.ML
author paulson
Wed Dec 24 10:02:30 1997 +0100 (1997-12-24 ago)
changeset 4477 b3e5857d8d99
parent 4423 a129b817b58a
child 4651 70dd492a1698
permissions -rw-r--r--
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
     1 (* 
     2     File:	 TLA/TLA.ML
     3     Author:      Stephan Merz
     4     Copyright:   1997 University of Munich
     5 
     6 Lemmas and tactics for temporal reasoning.
     7 *)
     8 
     9 (* Specialize intensional introduction/elimination rules to temporal formulas *)
    10 
    11 qed_goal "tempI" TLA.thy "(!!sigma. (sigma |= (F::temporal))) ==> F"
    12   (fn [prem] => [ REPEAT (resolve_tac [prem,intI] 1) ]);
    13 
    14 qed_goal "tempD" TLA.thy "F::temporal ==> (sigma |= F)"
    15   (fn [prem] => [ REPEAT (resolve_tac [prem,intD] 1) ]);
    16 
    17 
    18 (* ======== Functions to "unlift" temporal implications into HOL rules ====== *)
    19 
    20 (* Basic unlifting introduces a parameter "sigma" and applies basic rewrites, e.g.
    21    F .= G    gets   (sigma |= F) = (sigma |= G)
    22    F .-> G   gets   (sigma |= F) --> (sigma |= G)
    23 *)
    24 fun temp_unlift th = rewrite_rule intensional_rews (th RS tempD);
    25 
    26 (* F .-> G   becomes   sigma |= F  ==>  sigma |= G *)
    27 fun temp_mp th = zero_var_indexes ((temp_unlift th) RS mp);
    28 
    29 (* F .-> G   becomes   [| sigma |= F; sigma |= G ==> R |] ==> R 
    30    so that it can be used as an elimination rule
    31 *)
    32 fun temp_impE th = zero_var_indexes ((temp_unlift th) RS impE);
    33 
    34 (* F .& G .-> H  becomes  [| sigma |= F; sigma |= G |] ==> sigma |= H *)
    35 fun temp_conjmp th = zero_var_indexes (conjI RS (temp_mp th));
    36 
    37 (* F .& G .-> H  becomes  [| sigma |= F; sigma |= G; (sigma |= H ==> R) |] ==> R *)
    38 fun temp_conjimpE th = zero_var_indexes (conjI RS (temp_impE th));
    39 
    40 (* Turn  F .= G  into meta-level rewrite rule  F == G *)
    41 fun temp_rewrite th = (rewrite_rule intensional_rews (th RS inteq_reflection));
    42 
    43 
    44 (* Update classical reasoner---will be updated once more below! *)
    45 
    46 AddSIs [tempI];
    47 AddDs [tempD];
    48 
    49 val temp_cs = action_cs addSIs [tempI] addDs [tempD];
    50 val temp_css = (temp_cs,simpset());
    51 
    52 (* ========================================================================= *)
    53 section "Init";
    54 
    55 (* Push logical connectives through Init. *)
    56 qed_goal "Init_true" TLA.thy "Init(#True) .= #True"
    57   (fn _ => [ auto_tac (temp_css addsimps2 [Init_def]) ]);
    58 
    59 qed_goal "Init_false" TLA.thy "Init(#False) .= #False"
    60   (fn _ => [ auto_tac (temp_css addsimps2 [Init_def]) ]);
    61 
    62 qed_goal "Init_not" TLA.thy "Init(.~P) .= (.~Init(P))"
    63   (fn _ => [ auto_tac (temp_css addsimps2 [Init_def]) ]);
    64 
    65 qed_goal "Init_and" TLA.thy "Init(P .& Q) .= (Init(P) .& Init(Q))"
    66   (fn _ => [ auto_tac (temp_css addsimps2 [Init_def]) ]);
    67 
    68 qed_goal "Init_or" TLA.thy "Init(P .| Q) .= (Init(P) .| Init(Q))"
    69   (fn _ => [ auto_tac (temp_css addsimps2 [Init_def]) ]);
    70 
    71 qed_goal "Init_imp" TLA.thy "Init(P .-> Q) .= (Init(P) .-> Init(Q))"
    72   (fn _ => [ auto_tac (temp_css addsimps2 [Init_def]) ]);
    73 
    74 qed_goal "Init_iff" TLA.thy "Init(P .= Q) .= (Init(P) .= Init(Q))"
    75   (fn _ => [ auto_tac (temp_css addsimps2 [Init_def]) ]);
    76 
    77 qed_goal "Init_all" TLA.thy "Init(RALL x. P(x)) .= (RALL x. Init(P(x)))"
    78   (fn _ => [ auto_tac (temp_css addsimps2 [Init_def]) ]);
    79 
    80 qed_goal "Init_ex" TLA.thy "Init(REX x. P(x)) .= (REX x. Init(P(x)))"
    81   (fn _ => [ auto_tac (temp_css addsimps2 [Init_def]) ]);
    82 
    83 val Init_simps = map temp_rewrite
    84                      [Init_true,Init_false,Init_not,Init_and,Init_or,
    85 		      Init_imp,Init_iff,Init_all,Init_ex];
    86 
    87 
    88 (* Temporal lemmas *)
    89 
    90 qed_goalw "DmdAct" TLA.thy [dmd_def,boxact_def] "(<>(F::action)) .= (<> Init F)"
    91   (fn _ => [auto_tac (temp_css addsimps2 Init_simps)]);
    92 
    93 
    94 (* ------------------------------------------------------------------------- *)
    95 (***           "Simple temporal logic": only [] and <>                     ***)
    96 (* ------------------------------------------------------------------------- *)
    97 section "Simple temporal logic";
    98 
    99 (* ------------------------ STL2 ------------------------------------------- *)
   100 bind_thm("STL2", reflT);
   101 bind_thm("STL2D", temp_mp STL2);
   102 
   103 (* The action variants. *)
   104 qed_goalw "STL2b" TLA.thy [boxact_def] "[]P .-> Init P"
   105    (fn _ => [rtac STL2 1]);
   106 bind_thm("STL2bD", temp_mp STL2b);
   107 (* see also STL2b_pr below: "[]P .-> Init(P .& P`)" *)
   108 
   109 (* Dual versions for <> *)
   110 qed_goalw "ImplDmd" TLA.thy [dmd_def] "F .-> <>F"
   111    (fn _ => [ auto_tac (temp_css addSDs2 [STL2D]) ]);
   112 bind_thm ("ImplDmdD", temp_mp ImplDmd);
   113 
   114 qed_goalw "InitDmd" TLA.thy [dmd_def] "Init(P) .-> <>P"
   115    (fn _ => [ auto_tac (temp_css addsimps2 Init_simps addSDs2 [STL2bD]) ]);
   116 bind_thm("InitDmdD", temp_mp InitDmd);
   117 
   118 
   119 (* ------------------------ STL3 ------------------------------------------- *)
   120 qed_goal "STL3" TLA.thy "([][]F) .= ([]F)"
   121    (fn _ => [auto_tac (temp_css addIs2 [temp_mp transT,temp_mp STL2])]);
   122 
   123 (* corresponding elimination rule introduces double boxes: 
   124    [| (sigma |= []F); (sigma |= [][]F) ==> PROP W |] ==> PROP W
   125 *)
   126 bind_thm("dup_boxE", make_elim((temp_unlift STL3) RS iffD2));
   127 bind_thm("dup_boxD", (temp_unlift STL3) RS iffD1);
   128 
   129 (* dual versions for <> *)
   130 qed_goalw "DmdDmd" TLA.thy [dmd_def] "(<><>F) .= (<>F)"
   131    (fn _ => [ auto_tac (temp_css addsimps2 [STL3]) ]);
   132 bind_thm("dup_dmdE", make_elim((temp_unlift DmdDmd) RS iffD2));
   133 bind_thm("dup_dmdD", (temp_unlift DmdDmd) RS iffD1);
   134 
   135 
   136 (* ------------------------ STL4 ------------------------------------------- *)
   137 qed_goal "STL4" TLA.thy "(F .-> G)  ==> ([]F .-> []G)"
   138    (fn [prem] => [Auto_tac,
   139 		  rtac ((temp_mp normalT) RS mp) 1,
   140 		  REPEAT (ares_tac [prem, necT RS tempD] 1)
   141 		 ]);
   142 
   143 (* A more practical variant as an (unlifted) elimination rule *)
   144 qed_goal "STL4E" TLA.thy 
   145          "[| (sigma |= []F); F .-> G |] ==> (sigma |= []G)"
   146    (fn prems => [ REPEAT (resolve_tac (prems @ [temp_mp STL4]) 1) ]);
   147 
   148 (* see also STL4Edup below, which allows an auxiliary boxed formula:
   149        []A /\ F => G
   150      -----------------
   151      []A /\ []F => []G
   152 *)
   153 
   154 (* The dual versions for <> *)
   155 qed_goalw "DmdImpl" TLA.thy [dmd_def]
   156    "(F .-> G) ==> (<>F .-> <>G)"
   157    (fn [prem] => [fast_tac (temp_cs addSIs [int_mp prem] addSEs [STL4E]) 1]);
   158 
   159 qed_goal "DmdImplE" TLA.thy
   160    "[| (sigma |= <>F); F .-> G |] ==> (sigma |= <>G)"
   161    (fn prems => [ REPEAT (resolve_tac (prems @ [temp_mp DmdImpl]) 1) ]);
   162 
   163 
   164 (* ------------------------ STL5 ------------------------------------------- *)
   165 qed_goal "STL5" TLA.thy "([]F .& []G) .= ([](F .& G))"
   166    (fn _ => [Auto_tac,
   167 	     subgoal_tac "sigma |= [](G .-> (F .& G))" 1,
   168 	     etac ((temp_mp normalT) RS mp) 1, atac 1,
   169 	     ALLGOALS (fast_tac (temp_cs addSEs [STL4E]))
   170 	    ]);
   171 (* rewrite rule to split conjunctions under boxes *)
   172 bind_thm("split_box_conj", (temp_unlift STL5) RS sym);
   173 
   174 (* the corresponding elimination rule allows to combine boxes in the hypotheses
   175    (NB: F and G must have the same type, i.e., both actions or temporals.)
   176 *)
   177 qed_goal "box_conjE" TLA.thy
   178    "[| (sigma |= []F); (sigma |= []G); (sigma |= [](F.&G)) ==> PROP R |] ==> PROP R"
   179    (fn prems => [ REPEAT (resolve_tac
   180 			   (prems @ [(temp_unlift STL5) RS iffD1, conjI]) 1) ]);
   181 
   182 (* Define a tactic that tries to merge all boxes in an antecedent. The definition is
   183    a bit kludgy: how do you simulate "double elim-resolution"?
   184    Note: If there are boxed hypotheses of different types, the tactic may delete the 
   185          wrong formulas. We therefore also define less polymorphic tactics for
   186          temporals and actions.
   187 *)
   188 qed_goal "box_thin" TLA.thy "[| (sigma |= []F); PROP W |] ==> PROP W"
   189   (fn prems => [resolve_tac prems 1]);
   190 
   191 fun merge_box_tac i =
   192    REPEAT_DETERM (EVERY [etac box_conjE i, atac i, etac box_thin i]);
   193 
   194 qed_goal "temp_box_conjE" TLA.thy
   195    "[| (sigma |= [](F::temporal)); (sigma |= []G); (sigma |= [](F.&G)) ==> PROP R |] ==> PROP R"
   196    (fn prems => [ REPEAT (resolve_tac
   197 			   (prems @ [(temp_unlift STL5) RS iffD1, conjI]) 1) ]);
   198 qed_goal "temp_box_thin" TLA.thy "[| (sigma |= [](F::temporal)); PROP W |] ==> PROP W"
   199   (fn prems => [resolve_tac prems 1]);
   200 fun merge_temp_box_tac i =
   201    REPEAT_DETERM (EVERY [etac temp_box_conjE i, atac i, etac temp_box_thin i]);
   202 
   203 qed_goal "act_box_conjE" TLA.thy
   204    "[| (sigma |= [](A::action)); (sigma |= []B); (sigma |= [](A.&B)) ==> PROP R |] ==> PROP R"
   205    (fn prems => [ REPEAT (resolve_tac
   206 			   (prems @ [(temp_unlift STL5) RS iffD1, conjI]) 1) ]);
   207 qed_goal "act_box_thin" TLA.thy "[| (sigma |= [](A::action)); PROP W |] ==> PROP W"
   208   (fn prems => [resolve_tac prems 1]);
   209 fun merge_act_box_tac i =
   210    REPEAT_DETERM (EVERY [etac act_box_conjE i, atac i, etac act_box_thin i]);
   211 
   212 (* rewrite rule to push universal quantification through box:
   213       (sigma |= [](RALL x. F x)) = (! x. (sigma |= []F x))
   214 *)
   215 bind_thm("all_box", standard((temp_unlift allT) RS sym));
   216 
   217 
   218 qed_goal "DmdOr" TLA.thy "(<>(F .| G)) .= (<>F .| <>G)"
   219    (fn _ => [auto_tac (temp_css addsimps2 [dmd_def,split_box_conj]),
   220              TRYALL (EVERY' [etac swap, 
   221                              merge_box_tac, 
   222                              fast_tac (temp_cs addSEs [STL4E])])
   223             ]);
   224 
   225 qed_goal "exT" TLA.thy "(REX x. <>(F x)) .= (<>(REX x. F x))"
   226    (fn _ => [ auto_tac (temp_css addsimps2 [dmd_def,temp_rewrite Not_rex,all_box]) ]);
   227 
   228 bind_thm("ex_dmd", standard((temp_unlift exT) RS sym));
   229 	     
   230 
   231 qed_goal "STL4Edup" TLA.thy
   232    "!!sigma. [| (sigma |= []A); (sigma |= []F); F .& []A .-> G |] ==> (sigma |= []G)"
   233    (fn _ => [etac dup_boxE 1,
   234 	     merge_box_tac 1,
   235 	     etac STL4E 1,
   236 	     atac 1
   237 	    ]);
   238 
   239 qed_goalw "DmdImpl2" TLA.thy [dmd_def]
   240    "!!sigma. [| (sigma |= <>F); (sigma |= [](F .-> G)) |] ==> (sigma |= <>G)"
   241    (fn _ => [Auto_tac,
   242 	     etac notE 1,
   243 	     merge_box_tac 1,
   244 	     fast_tac (temp_cs addSEs [STL4E]) 1
   245 	    ]);
   246 
   247 qed_goal "InfImpl" TLA.thy
   248    "[| (sigma |= []<>F); (sigma |= []G); F .& G .-> H |] ==> (sigma |= []<>H)"
   249    (fn [prem1,prem2,prem3] 
   250        => [cut_facts_tac [prem1,prem2] 1,
   251 	   eres_inst_tac [("F","G")] dup_boxE 1,
   252 	   merge_box_tac 1,
   253 	   fast_tac (temp_cs addSEs [STL4E,DmdImpl2] addSIs [int_mp prem3]) 1
   254 	  ]);
   255 
   256 (* ------------------------ STL6 ------------------------------------------- *)
   257 (* Used in the proof of STL6, but useful in itself. *)
   258 qed_goalw "BoxDmdT" TLA.thy [dmd_def] "[]F .& <>G .-> <>([]F .& G)"
   259   (fn _ => [ Auto_tac,
   260              etac dup_boxE 1,
   261 	     merge_box_tac 1,
   262              etac swap 1,
   263              fast_tac (temp_cs addSEs [STL4E]) 1 ]);
   264 bind_thm("BoxDmd", temp_conjmp BoxDmdT);
   265 
   266 (* weaker than BoxDmd, but more polymorphic (and often just right) *)
   267 qed_goalw "BoxDmdT2" TLA.thy [dmd_def] "<>F .& []G .-> <>(F .& G)"
   268   (fn _ => [ Auto_tac,
   269 	     merge_box_tac 1,
   270              fast_tac (temp_cs addSEs [notE,STL4E]) 1
   271 	   ]);
   272 
   273 qed_goal "STL6" TLA.thy "<>[]F .& <>[]G .-> <>[](F .& G)"
   274   (fn _ => [auto_tac (temp_css addsimps2 [symmetric (temp_rewrite STL5)]),
   275 	    etac (temp_conjimpE linT) 1, atac 1, etac thin_rl 1,
   276 	    rtac ((temp_unlift DmdDmd) RS iffD1) 1,
   277 	    etac disjE 1,
   278 	    etac DmdImplE 1, rtac BoxDmdT 1,
   279 	    (* the second subgoal needs commutativity of .&, which complicates the proof *)
   280 	    etac DmdImplE 1,
   281 	    Auto_tac,
   282 	    etac (temp_conjimpE BoxDmdT) 1, atac 1, etac thin_rl 1,
   283 	    fast_tac (temp_cs addSEs [DmdImplE]) 1
   284 	   ]);
   285 
   286 
   287 (* ------------------------ True / False ----------------------------------------- *)
   288 section "Simplification of constants";
   289 
   290 qed_goal "BoxTrue" TLA.thy "[](#True)"
   291    (fn _ => [ fast_tac (temp_cs addSIs [necT]) 1 ]);
   292 
   293 qed_goal "BoxTrue_simp" TLA.thy "([](#True)) .= #True"
   294    (fn _ => [ fast_tac (temp_cs addSIs [BoxTrue RS tempD]) 1 ]);
   295 
   296 qed_goal "DmdFalse_simp" TLA.thy "(<>(#False)) .= #False"
   297    (fn _ => [ auto_tac (temp_css addsimps2 [dmd_def, BoxTrue_simp]) ]);
   298 
   299 qed_goal "DmdTrue_simp" TLA.thy "(<>((#True)::temporal)) .= #True"
   300    (fn _ => [ fast_tac (temp_cs addSIs [ImplDmdD]) 1 ]);
   301 
   302 qed_goal "DmdActTrue_simp" TLA.thy "(<>((#True)::action)) .= #True"
   303    (fn _ => [ auto_tac (temp_css addsimps2 Init_simps addSIs2 [InitDmdD]) ]);
   304 
   305 qed_goal "BoxFalse_simp" TLA.thy "([]((#False)::temporal)) .= #False"
   306    (fn _ => [ fast_tac (temp_cs addSDs [STL2D]) 1 ]);
   307 
   308 qed_goal "BoxActFalse_simp" TLA.thy "([]((#False)::action)) .= #False"
   309    (fn _ => [ auto_tac (temp_css addsimps2 Init_simps addSDs2 [STL2bD]) ]);
   310 
   311 qed_goal "BoxConst_simp" TLA.thy "([]((#P)::temporal)) .= #P"
   312    (fn _ => [rtac tempI 1,
   313              case_tac "P" 1,
   314              auto_tac (temp_css addsimps2 [BoxTrue_simp,BoxFalse_simp])
   315             ]);
   316 
   317 qed_goal "BoxActConst_simp" TLA.thy "([]((#P)::action)) .= #P"
   318    (fn _ => [rtac tempI 1,
   319              case_tac "P" 1,
   320              auto_tac (temp_css addsimps2 [BoxTrue_simp,BoxActFalse_simp])
   321             ]);
   322 
   323 qed_goal "DmdConst_simp" TLA.thy "(<>((#P)::temporal)) .= #P"
   324    (fn _ => [rtac tempI 1,
   325              case_tac "P" 1,
   326              auto_tac (temp_css addsimps2 [DmdTrue_simp,DmdFalse_simp])
   327             ]);
   328 
   329 qed_goal "DmdActConst_simp" TLA.thy "(<>((#P)::action)) .= #P"
   330    (fn _ => [rtac tempI 1,
   331              case_tac "P" 1,
   332              auto_tac (temp_css addsimps2 [DmdActTrue_simp,DmdFalse_simp])
   333             ]);
   334 
   335 val temp_simps = map temp_rewrite
   336                   [BoxTrue_simp,DmdFalse_simp,DmdTrue_simp,
   337 		   DmdActTrue_simp, BoxFalse_simp, BoxActFalse_simp,
   338 		   BoxConst_simp,BoxActConst_simp,DmdConst_simp,DmdActConst_simp];
   339 
   340 (* Make these rewrites active by default *)
   341 Addsimps temp_simps;
   342 val temp_css = temp_css addsimps2 temp_simps;
   343 val temp_cs = temp_cs addss (empty_ss addsimps temp_simps);
   344 
   345 
   346 (* ------------------------ Further rewrites ----------------------------------------- *)
   347 section "Further rewrites";
   348 
   349 qed_goalw "NotBox" TLA.thy [dmd_def] "(.~[]F) .= (<>.~F)"
   350    (fn _ => [ Auto_tac ]);
   351 
   352 qed_goalw "NotDmd" TLA.thy [dmd_def] "(.~<>F) .= ([].~F)"
   353    (fn _ => [ Auto_tac ]);
   354 
   355 (* These are not by default included in temp_css, because they could be harmful,
   356    e.g. []F .& .~[]F becomes []F .& <>.~F !! *)
   357 val more_temp_simps =  (map temp_rewrite [STL3, DmdDmd, NotBox, NotDmd])
   358                        @ (map (fn th => (temp_unlift th) RS eq_reflection)
   359 		         [NotBox, NotDmd]);
   360 
   361 qed_goal "BoxDmdBox" TLA.thy "([]<>[]F) .= (<>[]F)"
   362    (fn _ => [ auto_tac (temp_css addSDs2 [STL2D]),
   363               rtac ccontr 1,
   364               subgoal_tac "sigma |= <>[][]F .& <>[].~[]F" 1,
   365               etac thin_rl 1,
   366               Auto_tac,
   367 	      etac (temp_conjimpE STL6) 1, atac 1,
   368 	      Asm_full_simp_tac 1,
   369 	      ALLGOALS (asm_full_simp_tac (simpset() addsimps more_temp_simps))
   370 	    ]);
   371 
   372 qed_goalw "DmdBoxDmd" TLA.thy [dmd_def] "(<>[]<>F) .= ([]<>F)"
   373   (fn _ => [auto_tac (temp_css addsimps2 [temp_rewrite (rewrite_rule [dmd_def] BoxDmdBox)])]);
   374 
   375 val more_temp_simps = more_temp_simps @ (map temp_rewrite [BoxDmdBox, DmdBoxDmd]);
   376 
   377 
   378 (* ------------------------ Miscellaneous ----------------------------------- *)
   379 
   380 qed_goal "BoxOr" TLA.thy 
   381    "!!sigma. [| (sigma |= []F .| []G) |] ==> (sigma |= [](F .| G))"
   382    (fn _ => [ fast_tac (temp_cs addSEs [STL4E]) 1 ]);
   383 
   384 qed_goal "DBImplBD" TLA.thy "<>[](F::temporal) .-> []<>F"
   385   (fn _ => [Auto_tac,
   386 	    rtac ccontr 1,
   387 	    old_auto_tac (temp_css addsimps2 more_temp_simps 
   388 			           addEs2 [temp_conjimpE STL6])
   389 	   ]);
   390 
   391 (* Although the script is the same, the derivation isn't polymorphic and doesn't
   392    work for other types of formulas (uses STL2).
   393 *)
   394 qed_goal "DBImplBDAct" TLA.thy "<>[](A::action) .-> []<>A"
   395   (fn _ => [Auto_tac,
   396 	    rtac ccontr 1,
   397 	    old_auto_tac (temp_css addsimps2 more_temp_simps addEs2 [temp_conjimpE STL6])
   398 	   ]);
   399 
   400 qed_goal "BoxDmdDmdBox" TLA.thy
   401    "!!sigma. [| (sigma |= []<>F); (sigma |= <>[]G) |] ==> (sigma |= []<>(F .& G))"
   402    (fn _ => [rtac ccontr 1,
   403 	     rewrite_goals_tac more_temp_simps,
   404 	     etac (temp_conjimpE STL6) 1, atac 1,
   405 	     subgoal_tac "sigma |= <>[].~F" 1,
   406 	     SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1,
   407 	     fast_tac (temp_cs addEs [DmdImplE,STL4E]) 1
   408 	    ]);
   409 
   410 
   411 (* ------------------------------------------------------------------------- *)
   412 (***          TLA-specific theorems: primed formulas                       ***)
   413 (* ------------------------------------------------------------------------- *)
   414 section "priming";
   415 
   416 (* ------------------------ TLA2 ------------------------------------------- *)
   417 qed_goal "STL2bD_pr" TLA.thy
   418   "!!sigma. (sigma |= []P) ==> (sigma |= Init(P .& P`))"
   419   (fn _ => [rewrite_goals_tac Init_simps,
   420 	    fast_tac (temp_cs addSIs [temp_mp primeI, STL2bD]) 1]);
   421 
   422 (* Auxiliary lemma allows priming of boxed actions *)
   423 qed_goal "BoxPrime" TLA.thy "[]P .-> [](P .& P`)"
   424   (fn _ => [Auto_tac,
   425 	    etac dup_boxE 1,
   426 	    auto_tac (temp_css addsimps2 [boxact_def]
   427 		               addSIs2 [STL2bD_pr] addSEs2 [STL4E])
   428 	   ]);
   429 
   430 qed_goal "TLA2" TLA.thy "P .& P` .-> Q  ==>  []P .-> []Q"
   431   (fn prems => [fast_tac (temp_cs addSIs prems addDs [temp_mp BoxPrime] addEs [STL4E]) 1]);
   432 
   433 qed_goal "TLA2E" TLA.thy 
   434    "[| (sigma |= []P); P .& P` .-> Q |] ==> (sigma |= []Q)"
   435    (fn prems => [REPEAT (resolve_tac (prems @ (prems RL [temp_mp TLA2])) 1)]);
   436 
   437 qed_goalw "DmdPrime" TLA.thy [dmd_def] "(<>P`) .-> (<>P)"
   438    (fn _ => [ fast_tac (temp_cs addSEs [TLA2E]) 1 ]);
   439 
   440 
   441 (* ------------------------ INV1, stable --------------------------------------- *)
   442 section "stable, invariant";
   443 
   444 qed_goal "ind_rule" TLA.thy
   445    "[| (sigma |= []H); (sigma |= Init(P)); H .-> (Init(P) .& .~[]F .-> Init(P`) .& F) |] \
   446 \   ==> (sigma |= []F)"
   447    (fn prems => [rtac ((temp_mp indT) RS mp) 1,
   448 		 REPEAT (resolve_tac (prems @ (prems RL [STL4E])) 1)]);
   449 		 
   450 
   451 qed_goalw "INV1" TLA.thy [stable_def,boxact_def] 
   452   "Init(P) .& stable(P) .-> []P"
   453   (fn _ => [auto_tac (temp_css addsimps2 Init_simps addEs2 [ind_rule])]);
   454 bind_thm("INV1I", temp_conjmp INV1);
   455 
   456 qed_goalw "StableL" TLA.thy [stable_def]
   457    "(P .& A .-> P`) ==> ([]A .-> stable(P))"
   458    (fn [prem] => [fast_tac (temp_cs addSIs [action_mp prem] addSEs [STL4E]) 1]);
   459 
   460 qed_goal "Stable" TLA.thy
   461    "[| (sigma |= []A); P .& A .-> P` |] ==> (sigma |= stable P)"
   462    (fn prems => [ REPEAT (resolve_tac (prems @ [temp_mp StableL]) 1) ]);
   463 
   464 (* Generalization of INV1 *)
   465 qed_goalw "StableBox" TLA.thy [stable_def]
   466    "!!sigma. (sigma |= stable P) ==> (sigma |= [](Init P .-> []P))"
   467    (fn _ => [etac dup_boxE 1,
   468 	     auto_tac (temp_css addsimps2 [stable_def] addEs2 [STL4E, INV1I])
   469 	    ]);
   470      
   471 (* useful for WF2 / SF2 *)
   472 qed_goal "DmdStable" TLA.thy 
   473    "!!sigma. [| (sigma |= stable P); (sigma |= <>P) |] ==> (sigma |= <>[]P)"
   474    (fn _ => [rtac DmdImpl2 1,
   475 	     etac StableBox 2,
   476 	     auto_tac (temp_css addsimps2 [DmdAct])
   477 	    ]);
   478 
   479 (* ---------------- (Semi-)automatic invariant tactics ---------------------- *)
   480 
   481 (* inv_tac reduces goals of the form ... ==> sigma |= []P *)
   482 fun inv_tac css =
   483    SELECT_GOAL
   484      (EVERY [auto_tac css,
   485              TRY (merge_box_tac 1),
   486              rtac INV1I 1, (* fail if the goal is not a box *)
   487              TRYALL (etac Stable)]);
   488 
   489 (* auto_inv_tac applies inv_tac and then tries to attack the subgoals;
   490    in simple cases it may be able to handle goals like MyProg .-> []Inv.
   491    In these simple cases the simplifier seems to be more useful than the
   492    auto-tactic, which applies too much propositional logic and simplifies
   493    too late.
   494 *)
   495 
   496 fun auto_inv_tac ss =
   497   SELECT_GOAL
   498     ((inv_tac (claset(),ss) 1) THEN
   499      (TRYALL (action_simp_tac (ss addsimps [Init_def,square_def]) [] [])));
   500 
   501 
   502 qed_goalw "unless" TLA.thy [dmd_def]
   503    "!!sigma. (sigma |= [](P .-> P` .| Q`)) ==> (sigma |= stable P .| <>Q`)"
   504    (fn _ => [action_simp_tac (simpset()) [disjCI] [] 1,
   505 	     merge_box_tac 1,
   506 	     fast_tac (temp_cs addSEs [Stable]) 1
   507 	    ]);
   508 
   509 
   510 (* --------------------- Recursive expansions --------------------------------------- *)
   511 section "recursive expansions";
   512 
   513 (* Recursive expansions of [] and <>, restricted to state predicates to avoid looping *)
   514 qed_goal "BoxRec" TLA.thy "([]$P) .= (Init($P) .& ([]P$))"
   515    (fn _ => [auto_tac (temp_css addSIs2 [STL2bD]),
   516 	     fast_tac (temp_cs addSEs [TLA2E]) 1,
   517 	     auto_tac (temp_css addsimps2 [stable_def] addSEs2 [INV1I,STL4E])
   518 	    ]);
   519 
   520 qed_goalw "DmdRec" TLA.thy [dmd_def] "(<>$P) .= (Init($P) .| (<>P$))"
   521    (fn _ => [Auto_tac,
   522 	     etac notE 1,
   523 	     SELECT_GOAL (auto_tac (temp_css addsimps2 (stable_def::Init_simps)
   524 				             addIs2 [INV1I] addEs2 [STL4E])) 1,
   525 	     SELECT_GOAL (auto_tac (temp_css addsimps2 Init_simps addSDs2 [STL2bD])) 1,
   526 	     fast_tac (temp_cs addSEs [notE,TLA2E]) 1
   527 	    ]);
   528 
   529 qed_goal "DmdRec2" TLA.thy
   530    "!!sigma. [| (sigma |= <>($P)); (sigma |= [](.~P$)) |] ==> (sigma |= Init($P))"
   531    (fn _ => [dtac ((temp_unlift DmdRec) RS iffD1) 1,
   532 	     SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1
   533 	    ]);
   534 
   535 (* The "=>" part of the following is a little intricate. *)
   536 qed_goal "InfinitePrime" TLA.thy "([]<>$P) .= ([]<>P$)"
   537    (fn _ => [Auto_tac,
   538 	     rtac classical 1,
   539 	     rtac (temp_mp DBImplBDAct) 1,
   540 	     subgoal_tac "sigma |= <>[]$P" 1,
   541 	     fast_tac (temp_cs addSEs [DmdImplE,TLA2E]) 1,
   542 	     subgoal_tac "sigma |= <>[](<>$P .& [].~P$)" 1,
   543 	     SELECT_GOAL (auto_tac (temp_css addsimps2 [boxact_def]
   544 				             addSEs2 [DmdImplE,STL4E,DmdRec2])) 1,
   545 	     SELECT_GOAL (auto_tac (temp_css addSIs2 [temp_mp STL6] addsimps2 more_temp_simps)) 1,
   546 	     fast_tac (temp_cs addIs [temp_mp DmdPrime] addSEs [STL4E]) 1
   547 	    ]);
   548 
   549 (* ------------------------ fairness ------------------------------------------- *)
   550 section "fairness";
   551 
   552 (* alternative definitions of fairness *)
   553 qed_goalw "WF_alt" TLA.thy [WF_def,dmd_def] 
   554    "WF(A)_v .= (([]<>.~$(Enabled(<A>_v))) .| []<><A>_v)"
   555    (fn _ => [ fast_tac temp_cs 1 ]);
   556 
   557 qed_goalw "SF_alt" TLA.thy [SF_def,dmd_def]
   558    "SF(A)_v .= ((<>[].~$(Enabled(<A>_v))) .| []<><A>_v)"
   559    (fn _ => [ fast_tac temp_cs 1 ]);
   560 
   561 (* theorems to "box" fairness conditions *)
   562 qed_goal "BoxWFI" TLA.thy
   563    "!!sigma. (sigma |= WF(A)_v) ==> (sigma |= []WF(A)_v)"
   564    (fn _ => [ auto_tac (temp_css addsimps2 (temp_rewrite WF_alt::more_temp_simps) addSIs2 [BoxOr]) ]);
   565 
   566 qed_goal "WF_Box" TLA.thy "([]WF(A)_v) .= WF(A)_v"
   567   (fn prems => [ fast_tac (temp_cs addSIs [BoxWFI] addSDs [STL2D]) 1 ]);
   568 
   569 qed_goal "BoxSFI" TLA.thy
   570    "!!sigma. (sigma |= SF(A)_v) ==> (sigma |= []SF(A)_v)"
   571    (fn _ => [ auto_tac (temp_css addsimps2 (temp_rewrite SF_alt::more_temp_simps) addSIs2 [BoxOr]) ]);
   572 
   573 qed_goal "SF_Box" TLA.thy "([]SF(A)_v) .= SF(A)_v"
   574   (fn prems => [ fast_tac (temp_cs addSIs [BoxSFI] addSDs [STL2D]) 1 ]);
   575 
   576 val more_temp_simps = more_temp_simps @ (map temp_rewrite [WF_Box, SF_Box]);
   577 
   578 qed_goalw "SFImplWF" TLA.thy [SF_def,WF_def]
   579   "!!sigma. (sigma |= SF(A)_v) ==> (sigma |= WF(A)_v)"
   580   (fn _ => [ fast_tac (temp_cs addSDs [temp_mp DBImplBDAct]) 1 ]);
   581 
   582 (* A tactic that "boxes" all fairness conditions. Apply more_temp_simps to "unbox". *)
   583 val box_fair_tac = SELECT_GOAL (REPEAT (dresolve_tac [BoxWFI,BoxSFI] 1));
   584 
   585 
   586 (* ------------------------------ leads-to ------------------------------ *)
   587 
   588 section "~>";
   589 
   590 qed_goalw "leadsto_init" TLA.thy [leadsto]
   591    "!!sigma. [| (sigma |= Init P); (sigma |= P ~> Q) |] ==> (sigma |= <>Q)"
   592    (fn _ => [ fast_tac (temp_cs addSDs [temp_mp STL2]) 1 ]);
   593 
   594 qed_goalw "streett_leadsto" TLA.thy [leadsto]
   595    "([]<>P .-> []<>Q) .= (<>(P ~> Q))"
   596    (fn _ => [Auto_tac,
   597              asm_full_simp_tac (simpset() addsimps boxact_def::more_temp_simps) 1,
   598              SELECT_GOAL (auto_tac (temp_css addSEs2 [DmdImplE,STL4E] 
   599                                              addsimps2 Init_simps)) 1,
   600              SELECT_GOAL (auto_tac (temp_css addSIs2 [ImplDmdD] addSEs2 [STL4E])) 1,
   601              subgoal_tac "sigma |= []<><>Q" 1,
   602              asm_full_simp_tac (simpset() addsimps more_temp_simps) 1,
   603              rewtac (temp_rewrite DmdAct),
   604              dtac BoxDmdDmdBox 1, atac 1,
   605              auto_tac (temp_css addSEs2 [DmdImplE,STL4E])
   606             ]);
   607 
   608 qed_goal "leadsto_infinite" TLA.thy
   609    "!!sigma. [| (sigma |= []<>P); (sigma |= P ~> Q) |] ==> (sigma |= []<>Q)"
   610    (fn _ => [rtac ((temp_unlift streett_leadsto) RS iffD2 RS mp) 1,
   611              auto_tac (temp_css addSIs2 [ImplDmdD])
   612             ]);
   613 
   614 (* In particular, strong fairness is a Streett condition. The following
   615    rules are sometimes easier to use than WF2 or SF2 below.
   616 *)
   617 qed_goalw "leadsto_SF" TLA.thy [SF_def]
   618   "!!sigma. (sigma |= $(Enabled(<A>_v)) ~> <A>_v) ==> sigma |= SF(A)_v"
   619   (fn _ => [step_tac temp_cs 1,
   620             rtac leadsto_infinite 1,
   621             ALLGOALS atac
   622            ]);
   623 
   624 bind_thm("leadsto_WF", leadsto_SF RS SFImplWF);
   625 
   626 (* introduce an invariant into the proof of a leadsto assertion.
   627    []I => ((P ~> Q)  =  (P /\ I ~> Q))
   628 *)
   629 qed_goalw "INV_leadsto" TLA.thy [leadsto]
   630    "!!sigma. [| (sigma |= []I); (sigma |= (P .& I) ~> Q) |] ==> (sigma |= P ~> Q)"
   631    (fn _ => [etac STL4Edup 1, atac 1,
   632 	     auto_tac (temp_css addsimps2 [Init_def] addSDs2 [STL2bD])
   633 	    ]);
   634 
   635 qed_goalw "leadsto_classical" TLA.thy [leadsto,dmd_def]
   636    "!!sigma. (sigma |= [](Init P .& [].~Q .-> <>Q)) ==> (sigma |= P ~> Q)"
   637    (fn _ => [fast_tac (temp_cs addSEs [STL4E]) 1]);
   638 
   639 qed_goalw "leadsto_false" TLA.thy [leadsto]
   640   "(P ~> #False) .= ([] .~P)"
   641   (fn _ => [ auto_tac (temp_css addsimps2 boxact_def::Init_simps) ]);
   642 
   643 (* basic leadsto properties, cf. Unity *)
   644 
   645 qed_goal "ImplLeadsto" TLA.thy
   646    "!!sigma. (sigma |= [](P .-> Q)) ==> (sigma |= (P ~> Q))"
   647    (fn _ => [etac INV_leadsto 1, rewtac leadsto,
   648 	     rtac (temp_unlift necT) 1,
   649 	     auto_tac (temp_css addSIs2 [InitDmdD] addsimps2 [Init_def])
   650 	    ]);
   651 
   652 qed_goal "EnsuresLeadsto" TLA.thy
   653    "A .& P .-> Q` ==> []A .-> (P ~> Q)"
   654    (fn [prem] => [auto_tac (temp_css addSEs2 [INV_leadsto]),
   655 		  rewtac leadsto,
   656  		  auto_tac (temp_css addSIs2 [temp_unlift necT]),
   657 		  rtac (temp_mp DmdPrime) 1, rtac InitDmdD 1,
   658 		  auto_tac (action_css addsimps2 [Init_def] addSIs2 [action_mp prem])
   659 		 ]);
   660 
   661 qed_goalw "EnsuresLeadsto2" TLA.thy [leadsto]
   662    "!!sigma. sigma |= [](P .-> Q`) ==> sigma |= P ~> Q"
   663    (fn _ => [subgoal_tac "sigma |= []Init(P .-> Q`)" 1,
   664              etac STL4E 1,
   665              auto_tac (temp_css addsimps2 boxact_def::Init_simps 
   666                                 addIs2 [(temp_mp InitDmd) RS (temp_mp DmdPrime)])
   667             ]);
   668              
   669 qed_goal "EnsuresInfinite" TLA.thy
   670    "[| (sigma |= []<>P); (sigma |= []A); A .& P .-> Q` |] ==> (sigma |= []<>Q)"
   671    (fn prems => [REPEAT (resolve_tac (prems @ [leadsto_infinite,
   672 					       temp_mp EnsuresLeadsto]) 1)]);
   673 
   674 (*** Gronning's lattice rules (taken from TLP) ***)
   675 section "Lattice rules";
   676 
   677 qed_goalw "LatticeReflexivity" TLA.thy [leadsto] "F ~> F"
   678    (fn _ => [REPEAT (resolve_tac [necT,InitDmd] 1)]);
   679 
   680 qed_goalw "LatticeTransitivity" TLA.thy [leadsto]
   681    "!!sigma. [| (sigma |= G ~> H); (sigma |= F ~> G) |] ==> (sigma |= F ~> H)"
   682    (fn _ => [etac dup_boxE 1,  (* [][](Init G .-> H) *)
   683 	     merge_box_tac 1,
   684 	     auto_tac (temp_css addSEs2 [STL4E]),
   685 	     rewtac (temp_rewrite DmdAct),
   686 	     subgoal_tac "sigmaa |= <><> Init H" 1,
   687 	     asm_full_simp_tac (simpset() addsimps more_temp_simps) 1,
   688 	     fast_tac (temp_cs addSEs [DmdImpl2]) 1
   689 	    ]);
   690 
   691 qed_goalw "LatticeDisjunctionElim1" TLA.thy [leadsto]
   692    "!!sigma. (sigma |= (F .| G) ~> H) ==> (sigma |= F ~> H)"
   693    (fn _ => [ auto_tac (temp_css addsimps2 [Init_def] addSEs2 [STL4E]) ]);
   694 
   695 qed_goalw "LatticeDisjunctionElim2" TLA.thy [leadsto]
   696    "!!sigma. (sigma |= (F .| G) ~> H) ==> (sigma |= G ~> H)"
   697    (fn _ => [ auto_tac (temp_css addsimps2 [Init_def] addSEs2 [STL4E]) ]);
   698 
   699 qed_goalw "LatticeDisjunctionIntro" TLA.thy [leadsto]
   700    "!!sigma. [| (sigma |= F ~> H); (sigma |= G ~> H) |] ==> (sigma |= (F .| G) ~> H)"
   701    (fn _ => [merge_box_tac 1,
   702 	     auto_tac (temp_css addsimps2 [Init_def] addSEs2 [STL4E])
   703 	    ]);
   704 
   705 qed_goal "LatticeDiamond" TLA.thy
   706    "!!sigma. [| (sigma |= B ~> D); (sigma |= A ~> (B .| C)); (sigma |= C ~> D) |]  \
   707 \            ==> (sigma |= A ~> D)"
   708    (fn _ => [subgoal_tac "sigma |= (B .| C) ~> D" 1,
   709 	     eres_inst_tac [("G", "B .| C")] LatticeTransitivity 1,
   710 	     ALLGOALS (fast_tac (temp_cs addSIs [LatticeDisjunctionIntro]))
   711 	    ]);
   712 
   713 qed_goal "LatticeTriangle" TLA.thy
   714    "!!sigma. [| (sigma |= B ~> D); (sigma |= A ~> (B .| D)) |] ==> (sigma |= A ~> D)"
   715    (fn _ => [subgoal_tac "sigma |= (B .| D) ~> D" 1,
   716 	     eres_inst_tac [("G", "B .| D")] LatticeTransitivity 1, atac 1,
   717 	     auto_tac (temp_css addSIs2 [LatticeDisjunctionIntro] addIs2 [ImplLeadsto])
   718 	    ]);
   719 
   720 (*** Lamport's fairness rules ***)
   721 section "Fairness rules";
   722 
   723 qed_goalw "WF1" TLA.thy [leadsto]
   724    "[| P .& N  .-> P` .| Q`;   \
   725 \      P .& N .& <A>_v .-> Q`;   \
   726 \      P .& N .-> $(Enabled(<A>_v)) |]   \
   727 \  ==> []N .& WF(A)_v .-> (P ~> Q)"
   728    (fn [prem1,prem2,prem3]
   729 	 => [auto_tac (temp_css addSDs2 [BoxWFI]),
   730 	     etac STL4Edup 1, atac 1,
   731 	     Auto_tac,
   732 	     subgoal_tac "sigmaa |= [](P .-> P` .| Q`)" 1,
   733 	     auto_tac (temp_css addSDs2 [unless]),
   734 	     etac (temp_conjimpE INV1) 1, atac 1,
   735 	     merge_box_tac 1,
   736 	     rtac STL2D 1,
   737 	     rtac EnsuresInfinite 1, atac 2,
   738 	     SELECT_GOAL (old_auto_tac (temp_css addsimps2 [WF_alt])) 1,
   739 	     atac 2,
   740 	     subgoal_tac "sigmaa |= [][]$(Enabled(<A>_v))" 1,
   741 	     merge_box_tac 1,
   742 	     SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1,
   743 	     SELECT_GOAL ((rewtac (temp_rewrite STL3)) THEN
   744 			  (auto_tac (temp_css addSEs2 [STL4E] addSIs2 [action_mp prem3]))) 1,
   745 	     fast_tac (action_cs addSIs [action_mp prem2]) 1,
   746 	     fast_tac (temp_cs addIs [temp_mp DmdPrime]) 1,
   747 	     fast_tac (temp_cs addSEs [STL4E] addSIs [action_mp prem1]) 1
   748 	    ]);
   749 
   750 (* Sometimes easier to use; designed for action B rather than state predicate Q *)
   751 qed_goalw "WF_leadsto" TLA.thy [leadsto]
   752    "[| N .& P .-> $Enabled (<A>_v);            \
   753 \      N .& <A>_v .-> B;                  \ 
   754 \      [](N .& [.~A]_v) .-> stable P  |]  \
   755 \   ==> []N .& WF(A)_v .-> (P ~> B)"
   756    (fn [prem1,prem2,prem3]
   757        => [auto_tac (temp_css addSDs2 [BoxWFI]),
   758            etac STL4Edup 1, atac 1,
   759            Auto_tac,
   760            subgoal_tac "sigmaa |= <><A>_v" 1,
   761            SELECT_GOAL (auto_tac (temp_css addSEs2 [DmdImpl2,STL4E] addSIs2 [action_mp prem2])) 1,
   762            rtac classical 1,
   763            rtac STL2D 1,
   764            auto_tac (temp_css addsimps2 WF_def::more_temp_simps addSEs2 [mp]),
   765            rtac ImplDmdD 1,
   766            rtac (temp_mp (prem1 RS STL4)) 1,
   767            auto_tac (temp_css addsimps2 [split_box_conj]),
   768            etac INV1I 1,
   769            merge_act_box_tac 1,
   770            auto_tac (temp_css addsimps2 [temp_rewrite not_angle] addSEs2 [temp_mp prem3])
   771           ]);
   772 
   773 qed_goalw "SF1" TLA.thy [leadsto]
   774    "[| P .& N  .-> P` .| Q`;   \
   775 \      P .& N .& <A>_v .-> Q`;   \
   776 \      []P .& []N .& []F .-> <>$(Enabled(<A>_v)) |]   \
   777 \  ==> []N .& SF(A)_v .& []F .-> (P ~> Q)"
   778    (fn [prem1,prem2,prem3] =>
   779                 [auto_tac (temp_css addSDs2 [BoxSFI]),
   780 		 eres_inst_tac [("F","F")] dup_boxE 1,
   781 		 merge_temp_box_tac 1,
   782 		 etac STL4Edup 1, atac 1,
   783 		 Auto_tac,
   784 		 subgoal_tac "sigmaa |= [](P .-> P` .| Q`)" 1,
   785 		 auto_tac (temp_css addSDs2 [unless]),
   786 		 etac (temp_conjimpE INV1) 1, atac 1,
   787 		 merge_act_box_tac 1,
   788 		 rtac STL2D 1,
   789 		 rtac EnsuresInfinite 1, atac 2,
   790 		 SELECT_GOAL (old_auto_tac (temp_css addsimps2 [SF_alt])) 1,
   791 		 atac 2,
   792 		 subgoal_tac "sigmaa |= []<>$(Enabled(<A>_v))" 1,
   793 		 SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1,
   794 		 eres_inst_tac [("F","F")] dup_boxE 1,
   795 		 etac STL4Edup 1, atac 1,
   796 		 fast_tac (temp_cs addSEs [STL4E] addSIs [temp_mp prem3]) 1,
   797 		 fast_tac (action_cs addSIs [action_mp prem2]) 1,
   798 		 fast_tac (temp_cs addIs [temp_mp DmdPrime]) 1,
   799 		 fast_tac (temp_cs addSEs [STL4E] addSIs [action_mp prem1]) 1
   800 		]);
   801 
   802 qed_goal "WF2" TLA.thy
   803    "[| N .& <B>_f .-> <M>_g;   \
   804 \      P .& P` .& <N .& A>_f .-> B;   \
   805 \      P .& $(Enabled(<M>_g)) .-> $(Enabled(<A>_f));   \
   806 \      [](N .& [.~B]_f) .& WF(A)_f .& []F .& <>[]($(Enabled(<M>_g))) .-> <>[]P |]   \
   807 \  ==> []N .& WF(A)_f .& []F .-> WF(M)_g"
   808    (fn [prem1,prem2,prem3,prem4]
   809        => [Auto_tac,
   810 	   case_tac "sigma |= <>[]$Enabled(<M>_g)" 1,
   811 	   SELECT_GOAL (auto_tac (temp_css addsimps2 [WF_def,dmd_def])) 2,
   812 	   case_tac "sigma |= <>[][.~B]_f" 1,
   813 	   subgoal_tac "sigma |= <>[]P" 1,
   814 	   asm_full_simp_tac (simpset() addsimps [WF_def]) 1,
   815 	   rtac (temp_mp (prem1 RS DmdImpl RS STL4)) 1,
   816 	   eres_inst_tac [("V","sigma |= <>[][.~B]_f")] thin_rl 1,
   817 	   etac (temp_conjimpE STL6) 1, atac 1,
   818 	   subgoal_tac "sigma |= <>[]$Enabled(<A>_f)" 1,
   819 	   dtac mp 1, atac 1,
   820 	   subgoal_tac "sigma |= <>([]N .& []P .& []<><A>_f)" 1,
   821 	   rtac ((temp_unlift DmdBoxDmd) RS iffD1) 1,
   822 	   eres_inst_tac [("F","[]N .& []P .& []<><A>_f")] DmdImplE 1,
   823 	   SELECT_GOAL Auto_tac 1,
   824 	   dres_inst_tac [("P","P")] (temp_mp BoxPrime) 1,
   825 	   merge_act_box_tac 1,
   826 	   etac InfImpl 1, atac 1,
   827 	   SELECT_GOAL (auto_tac (temp_css addsimps2 [angle_def] addSIs2 [action_mp prem2])) 1,
   828 	   etac BoxDmd 1,
   829 	   dres_inst_tac [("F","<><A>_f"),("G","[]P")] BoxDmd 1, atac 1,
   830 	   eres_inst_tac [("F","[]<><A>_f .& []P")] DmdImplE 1,
   831 	   SELECT_GOAL Auto_tac 1,
   832 	   rtac (temp_mp (prem3 RS STL4 RS DmdImpl)) 1,
   833 	   fast_tac (temp_cs addIs [STL4E,DmdImplE]) 1,
   834 	   etac (temp_conjimpE STL6) 1, atac 1,
   835 	   eres_inst_tac [("V","sigma |= <>[][.~ B]_f")] thin_rl 1,
   836 	   dtac BoxWFI 1,
   837 	   eres_inst_tac [("F","N")] dup_boxE 1,
   838 	   eres_inst_tac [("F","F")] dup_boxE 1,
   839 	   merge_temp_box_tac 1,
   840 	   dtac BoxDmd 1, atac 1,
   841 	   eres_inst_tac [("V","sigma |= <>[]($Enabled (<M>_g) .& [.~ B]_f)")] thin_rl 1,
   842 	   rtac dup_dmdD 1,
   843 	   rtac (temp_mp (prem4 RS DmdImpl)) 1,
   844 	   etac DmdImplE 1,
   845 	   SELECT_GOAL
   846 	     (auto_tac (temp_css addsimps2 [symmetric(temp_rewrite STL5), temp_rewrite STL3]
   847 		                 addIs2 [(temp_unlift WF_Box) RS iffD1, temp_mp ImplDmd])) 1,
   848 	   asm_full_simp_tac (simpset() addsimps (WF_def::more_temp_simps)) 1,
   849 	   etac InfImpl 1, atac 1,
   850 	   SELECT_GOAL (auto_tac (temp_css addSIs2 [action_mp prem1])) 1,
   851 	   ALLGOALS (asm_full_simp_tac (simpset() addsimps [square_def,angle_def]))
   852 	  ]);
   853 
   854 qed_goal "SF2" TLA.thy
   855    "[| N .& <B>_f .-> <M>_g;   \
   856 \      P .& P` .& <N .& A>_f .-> B;   \
   857 \      P .& $(Enabled(<M>_g)) .-> $(Enabled(<A>_f));   \
   858 \      [](N .& [.~B]_f) .& SF(A)_f .& []F .& []<>($(Enabled(<M>_g))) .-> <>[]P |]   \
   859 \  ==> []N .& SF(A)_f .& []F .-> SF(M)_g"
   860    (fn [prem1,prem2,prem3,prem4]
   861        => [Auto_tac,
   862 	   case_tac "sigma |= []<>$Enabled(<M>_g)" 1,
   863 	   SELECT_GOAL (auto_tac (temp_css addsimps2 [SF_def,dmd_def])) 2,
   864 	   case_tac "sigma |= <>[][.~B]_f" 1,
   865 	   subgoal_tac "sigma |= <>[]P" 1,
   866 	   asm_full_simp_tac (simpset() addsimps [SF_def]) 1,
   867 	   rtac (temp_mp (prem1 RS DmdImpl RS STL4)) 1,
   868 	   eres_inst_tac [("V","sigma |= <>[][.~B]_f")] thin_rl 1,
   869 	   dtac BoxDmdDmdBox 1, atac 1,
   870 	   subgoal_tac "sigma |= []<>$Enabled(<A>_f)" 1,
   871 	   dtac mp 1, atac 1,
   872 	   subgoal_tac "sigma |= <>([]N .& []P .& []<><A>_f)" 1,
   873 	   rtac ((temp_unlift DmdBoxDmd) RS iffD1) 1,
   874 	   eres_inst_tac [("F","[]N .& []P .& []<><A>_f")] DmdImplE 1,
   875 	   SELECT_GOAL Auto_tac 1,
   876 	   dres_inst_tac [("P","P")] (temp_mp BoxPrime) 1,
   877 	   merge_act_box_tac 1,
   878 	   etac InfImpl 1, atac 1,
   879 	   SELECT_GOAL (auto_tac (temp_css addsimps2 [angle_def] addSIs2 [action_mp prem2])) 1,
   880 	   etac BoxDmd 1,
   881 	   dres_inst_tac [("F","<><A>_f"),("G","[]P")] BoxDmd 1, atac 1,
   882 	   eres_inst_tac [("F","[]<><A>_f .& []P")] DmdImplE 1,
   883 	   SELECT_GOAL Auto_tac 1,
   884 	   rtac (temp_mp (prem3 RS DmdImpl RS STL4)) 1,
   885 	   fast_tac (temp_cs addEs [STL4E,DmdImplE]) 1,
   886 	   dtac BoxSFI 1,
   887 	   eres_inst_tac [("F","N")] dup_boxE 1,
   888 	   eres_inst_tac [("F","F")] dup_boxE 1,
   889 	   eres_inst_tac [("F","<>$Enabled (<M>_g)")] dup_boxE 1,
   890 	   merge_temp_box_tac 1,
   891 	   dtac (temp_conjmp BoxDmdT2) 1, atac 1,
   892 	   rtac dup_dmdD 1,
   893 	   rtac (temp_mp (prem4 RS DmdImpl)) 1,
   894 	   SELECT_GOAL
   895 	     (auto_tac (temp_css addsimps2 [symmetric(temp_rewrite STL5), temp_rewrite STL3]
   896 		                 addIs2 [(temp_unlift WF_Box) RS iffD1, temp_mp ImplDmd]
   897 			         addSEs2 [DmdImplE])) 1,
   898 	   asm_full_simp_tac (simpset() addsimps (SF_def::more_temp_simps)) 1,
   899 	   eres_inst_tac [("F",".~ [.~ B]_f")] InfImpl 1, atac 1,
   900 	   SELECT_GOAL (auto_tac (temp_css addSIs2 [action_mp prem1])) 1,
   901 	   ALLGOALS (asm_full_simp_tac (simpset() addsimps [square_def,angle_def]))
   902 	  ]);
   903 
   904 (* ------------------------------------------------------------------------- *)
   905 (***           Liveness proofs by well-founded orderings                   ***)
   906 (* ------------------------------------------------------------------------- *)
   907 section "Well-founded orderings";
   908 
   909 qed_goal "wf_dmd" TLA.thy
   910   "[| (wf r);  \
   911 \     !!x. sigma |= [](F x .-> <>G .| <>(REX y. #((y,x):r) .& F y))   \
   912 \  |] ==> sigma |= [](F x .-> <>G)"
   913   (fn prem1::prems => 
   914          [cut_facts_tac [prem1] 1,
   915           etac wf_induct 1,
   916           subgoal_tac "sigma |= []((REX y. #((y,x):r) .& F y) .-> <>G)" 1,
   917 	  cut_facts_tac prems 1,
   918 	  etac STL4Edup 1, atac 1,
   919 	  Auto_tac, etac swap 1, atac 1,
   920 	  rtac dup_dmdD 1,
   921 	  etac DmdImpl2 1, atac 1,
   922 	  subgoal_tac "sigma |= [](RALL y. #((y,x):r) .& F y .-> <>G)" 1,
   923 	  fast_tac (temp_cs addSEs [STL4E]) 1,
   924 	  auto_tac (temp_css addsimps2 [all_box]),
   925 	  etac allE 1, etac impCE 1,
   926 	  rtac (temp_unlift necT) 1,
   927 	  auto_tac (temp_css addSEs2 [STL4E])
   928          ]);
   929 
   930 (* Special case: leadsto via well-foundedness *)
   931 qed_goalw "wf_leadsto" TLA.thy [leadsto]
   932   "[| (wf r);  \
   933 \     !!x. sigma |= P x ~> (Q .| (REX y. #((y,x):r) .& P y))   \
   934 \  |] ==> sigma |= P x ~> Q"
   935   (fn prems => [REPEAT (resolve_tac (wf_dmd::prems) 1),
   936 		resolve_tac (prems RL [STL4E]) 1,
   937 		auto_tac (temp_css addsimps2 [temp_rewrite DmdOr]),
   938                 fast_tac temp_cs 1,
   939 		etac swap 1,
   940 		rewtac (temp_rewrite DmdAct),
   941 		auto_tac (temp_css addsimps2 [Init_def] addSEs2 [DmdImplE])
   942 	       ]);
   943 
   944 (* If r is well-founded, state function v cannot decrease forever *)
   945 qed_goal "wf_not_box_decrease" TLA.thy
   946   "!!r. wf r ==> [][ {[v$, $v]} .: #r ]_v .-> <>[][#False]_v"
   947   (fn _ => [Auto_tac,
   948             subgoal_tac "ALL x. (sigma |= [](Init($v .= #x) .-> <>[][#False]_v))" 1,
   949             etac allE 1,
   950             dtac STL2D 1,
   951             auto_tac (temp_css addsimps2 [Init_def]),
   952             etac wf_dmd 1,
   953             etac dup_boxE 1,
   954             etac STL4E 1,
   955             action_simp_tac (simpset() addsimps [con_abs]) [tempI] [] 1,
   956             case_tac "sigma |= <>[][#False]_v" 1,
   957             ALLGOALS Asm_full_simp_tac,
   958             rewrite_goals_tac more_temp_simps,
   959             dtac STL2D 1,
   960             subgoal_tac "sigma |= <>(REX y. #((y, xa) : r) .& ($v .= #y))" 1,
   961             SELECT_GOAL (auto_tac (temp_css addsimps2 [DmdAct,Init_def] 
   962                                             addEs2 [DmdImplE])) 1,
   963             subgoal_tac "sigma |= (stable ($v .= #xa) .| <>(REX y. #((y, xa) : r) .& $v .= #y)`)" 1,
   964             case_tac "sigma |= stable ($v .= #xa)" 1,
   965             SELECT_GOAL (auto_tac (temp_css addIs2 [temp_mp DmdPrime])) 2,
   966             SELECT_GOAL (rewrite_goals_tac ((symmetric (temp_rewrite NotBox))::action_rews)) 1,
   967             etac swap 1,
   968             subgoal_tac "sigma |= []($v .= #xa)" 1,
   969             dres_inst_tac [("P", "$v .= #xa")] (temp_mp BoxPrime) 1,
   970             SELECT_GOAL (auto_tac (temp_css addEs2 [STL4E] addsimps2 [square_def])) 1,
   971             SELECT_GOAL (auto_tac (temp_css addSIs2 [INV1I] addsimps2 [Init_def])) 1,
   972             old_auto_tac (temp_css addsimps2 [square_def] addSIs2 [unless] addSEs2 [STL4E])
   973            ]);
   974 
   975 (* "wf ?r  ==>  <>[][{[?v$, $?v]} .: #?r]_?v .-> <>[][#False]_?v" *)
   976 bind_thm("wf_not_dmd_box_decrease",
   977          standard(rewrite_rule more_temp_simps (wf_not_box_decrease RS DmdImpl)));
   978 
   979 (* If there are infinitely many steps where v decreases w.r.t. r, then there
   980    have to be infinitely many non-stuttering steps where v doesn't decrease.
   981 *)
   982 qed_goal "wf_box_dmd_decrease" TLA.thy
   983   "wf r ==> []<>({[v$, $v]} .: #r) .-> []<><.~({[v$, $v]} .: #r)>_v"
   984   (fn [prem] => [Auto_tac,
   985                  rtac ccontr 1,
   986                  asm_full_simp_tac 
   987                    (simpset() addsimps ([action_rewrite not_angle] @ more_temp_simps)) 1,
   988                  dtac (prem RS (temp_mp wf_not_dmd_box_decrease)) 1,
   989                  dtac BoxDmdDmdBox 1, atac 1,
   990                  subgoal_tac "sigma |= []<>((#False)::action)" 1,
   991                  SELECT_GOAL Auto_tac 1,
   992                  etac STL4E 1,
   993                  rtac DmdImpl 1,
   994                  auto_tac (action_css addsimps2 [square_def] addSEs2 [prem RS wf_irrefl])
   995                 ]);
   996 
   997 (* In particular, for natural numbers, if n decreases infinitely often
   998    then it has to increase infinitely often.
   999 *)
  1000 qed_goal "nat_box_dmd_decrease" TLA.thy
  1001   "!!n::nat stfun. []<>(n$ .< $n) .-> []<>($n .< n$)"
  1002   (fn _ => [Auto_tac,
  1003             subgoal_tac "sigma |= []<><.~( {[n$,$n]} .: #less_than)>_n" 1,
  1004             etac thin_rl 1, etac STL4E 1, rtac DmdImpl 1,
  1005             SELECT_GOAL (auto_tac (claset(), simpset() addsimps [angle_def])) 1,
  1006             rtac nat_less_cases 1,
  1007             Auto_tac,
  1008             rtac (temp_mp wf_box_dmd_decrease) 1,
  1009             auto_tac (claset() addSEs [STL4E] addSIs [DmdImpl], simpset())
  1010            ]);
  1011 
  1012 (* ------------------------------------------------------------------------- *)
  1013 (***           Flexible quantification over state variables                ***)
  1014 (* ------------------------------------------------------------------------- *)
  1015 section "Flexible quantification";
  1016 
  1017 qed_goal "aallI" TLA.thy 
  1018   "(!!x. base_var x ==> sigma |= F x) ==> sigma |= (AALL x. F(x))"
  1019   (fn prems => [auto_tac (temp_css addsimps2 [aall_def] addSEs2 [eexE] addSDs2 prems)]);
  1020 
  1021 qed_goal "aallE" TLA.thy
  1022    "[| sigma |= (AALL x. F(x));  (!!sigma. sigma |= F(x) ==> P sigma) |] \
  1023 \   ==> (P sigma)::bool"
  1024    (fn prems => [cut_facts_tac prems 1,
  1025 		 resolve_tac prems 1,
  1026 		 rewrite_goals_tac (aall_def::intensional_rews),
  1027 		 etac swap 1,
  1028 		 auto_tac (temp_css addSIs2 [temp_mp eexI])
  1029 		]);
  1030 
  1031 (* monotonicity of quantification *)
  1032 qed_goal "eex_mono" TLA.thy
  1033   "[| sigma |= EEX x. F(x); !!x. F(x) .-> G(x) |] ==> sigma |= EEX x. G(x)"
  1034   (fn [min,maj] => [cut_facts_tac [min] 1,
  1035                     etac eexE 1,
  1036                     REPEAT (ares_tac (map temp_mp [eexI,maj]) 1)
  1037                    ]);
  1038 
  1039 qed_goal "aall_mono" TLA.thy
  1040   "[| sigma |= AALL x. F(x); !!x. F(x) .-> G(x) |] ==> sigma |= AALL x. G(x)"
  1041   (fn [min,maj] => [cut_facts_tac [min] 1,
  1042                     fast_tac (temp_cs addSIs [aallI, temp_mp maj]
  1043                                       addEs [aallE]) 1
  1044                    ]);
  1045 
  1046 (* ----------------------------------------------------------------------
  1047    example of a history variable: existence of a clock
  1048 
  1049 goal TLA.thy "(EEX h. Init($h .= #True) .& [](h$ .~= $h))";
  1050 by (rtac tempI 1);
  1051 by (rtac historyI 1);
  1052 by (rewrite_goals_tac action_rews);
  1053 by (TRYALL (rtac impI));
  1054 by (TRYALL (etac conjE));
  1055 by (assume_tac 3);
  1056 by (Asm_full_simp_tac 3);
  1057 by (auto_tac (temp_css addSIs2 [(temp_unlift Init_true) RS iffD2, temp_unlift BoxTrue]));
  1058 (** solved **)
  1059 
  1060 ---------------------------------------------------------------------- *)