src/HOL/TLA/TLA.ML
 author wenzelm Mon Nov 03 12:13:18 1997 +0100 (1997-11-03 ago) changeset 4089 96fba19bcbe2 parent 3807 82a99b090d9d child 4423 a129b817b58a permissions -rw-r--r--
isatool fixclasimp;
```     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 	    auto_tac (temp_css addsimps2 more_temp_simps addEs2 [temp_conjimpE STL6])
```
```   388 	   ]);
```
```   389
```
```   390 (* Although the script is the same, the derivation isn't polymorphic and doesn't
```
```   391    work for other types of formulas (uses STL2).
```
```   392 *)
```
```   393 qed_goal "DBImplBDAct" TLA.thy "<>[](A::action) .-> []<>A"
```
```   394   (fn _ => [Auto_tac(),
```
```   395 	    rtac ccontr 1,
```
```   396 	    auto_tac (temp_css addsimps2 more_temp_simps addEs2 [temp_conjimpE STL6])
```
```   397 	   ]);
```
```   398
```
```   399 qed_goal "BoxDmdDmdBox" TLA.thy
```
```   400    "!!sigma. [| (sigma |= []<>F); (sigma |= <>[]G) |] ==> (sigma |= []<>(F .& G))"
```
```   401    (fn _ => [rtac ccontr 1,
```
```   402 	     rewrite_goals_tac more_temp_simps,
```
```   403 	     etac (temp_conjimpE STL6) 1, atac 1,
```
```   404 	     subgoal_tac "sigma |= <>[].~F" 1,
```
```   405 	     SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1,
```
```   406 	     fast_tac (temp_cs addEs [DmdImplE,STL4E]) 1
```
```   407 	    ]);
```
```   408
```
```   409
```
```   410 (* ------------------------------------------------------------------------- *)
```
```   411 (***          TLA-specific theorems: primed formulas                       ***)
```
```   412 (* ------------------------------------------------------------------------- *)
```
```   413 section "priming";
```
```   414
```
```   415 (* ------------------------ TLA2 ------------------------------------------- *)
```
```   416 qed_goal "STL2bD_pr" TLA.thy
```
```   417   "!!sigma. (sigma |= []P) ==> (sigma |= Init(P .& P`))"
```
```   418   (fn _ => [rewrite_goals_tac Init_simps,
```
```   419 	    fast_tac (temp_cs addSIs [temp_mp primeI, STL2bD]) 1]);
```
```   420
```
```   421 (* Auxiliary lemma allows priming of boxed actions *)
```
```   422 qed_goal "BoxPrime" TLA.thy "[]P .-> [](P .& P`)"
```
```   423   (fn _ => [Auto_tac(),
```
```   424 	    etac dup_boxE 1,
```
```   425 	    auto_tac (temp_css addsimps2 [boxact_def]
```
```   426 		               addSIs2 [STL2bD_pr] addSEs2 [STL4E])
```
```   427 	   ]);
```
```   428
```
```   429 qed_goal "TLA2" TLA.thy "P .& P` .-> Q  ==>  []P .-> []Q"
```
```   430   (fn prems => [fast_tac (temp_cs addSIs prems addDs [temp_mp BoxPrime] addEs [STL4E]) 1]);
```
```   431
```
```   432 qed_goal "TLA2E" TLA.thy
```
```   433    "[| (sigma |= []P); P .& P` .-> Q |] ==> (sigma |= []Q)"
```
```   434    (fn prems => [REPEAT (resolve_tac (prems @ (prems RL [temp_mp TLA2])) 1)]);
```
```   435
```
```   436 qed_goalw "DmdPrime" TLA.thy [dmd_def] "(<>P`) .-> (<>P)"
```
```   437    (fn _ => [ fast_tac (temp_cs addSEs [TLA2E]) 1 ]);
```
```   438
```
```   439
```
```   440 (* ------------------------ INV1, stable --------------------------------------- *)
```
```   441 section "stable, invariant";
```
```   442
```
```   443 qed_goal "ind_rule" TLA.thy
```
```   444    "[| (sigma |= []H); (sigma |= Init(P)); H .-> (Init(P) .& .~[]F .-> Init(P`) .& F) |] \
```
```   445 \   ==> (sigma |= []F)"
```
```   446    (fn prems => [rtac ((temp_mp indT) RS mp) 1,
```
```   447 		 REPEAT (resolve_tac (prems @ (prems RL [STL4E])) 1)]);
```
```   448
```
```   449
```
```   450 qed_goalw "INV1" TLA.thy [stable_def,boxact_def]
```
```   451   "Init(P) .& stable(P) .-> []P"
```
```   452   (fn _ => [auto_tac (temp_css addsimps2 Init_simps addEs2 [ind_rule])]);
```
```   453 bind_thm("INV1I", temp_conjmp INV1);
```
```   454
```
```   455 qed_goalw "StableL" TLA.thy [stable_def]
```
```   456    "(P .& A .-> P`) ==> ([]A .-> stable(P))"
```
```   457    (fn [prem] => [fast_tac (temp_cs addSIs [action_mp prem] addSEs [STL4E]) 1]);
```
```   458
```
```   459 qed_goal "Stable" TLA.thy
```
```   460    "[| (sigma |= []A); P .& A .-> P` |] ==> (sigma |= stable P)"
```
```   461    (fn prems => [ REPEAT (resolve_tac (prems @ [temp_mp StableL]) 1) ]);
```
```   462
```
```   463 (* Generalization of INV1 *)
```
```   464 qed_goalw "StableBox" TLA.thy [stable_def]
```
```   465    "!!sigma. (sigma |= stable P) ==> (sigma |= [](Init P .-> []P))"
```
```   466    (fn _ => [etac dup_boxE 1,
```
```   467 	     auto_tac (temp_css addsimps2 [stable_def] addEs2 [STL4E, INV1I])
```
```   468 	    ]);
```
```   469
```
```   470 (* useful for WF2 / SF2 *)
```
```   471 qed_goal "DmdStable" TLA.thy
```
```   472    "!!sigma. [| (sigma |= stable P); (sigma |= <>P) |] ==> (sigma |= <>[]P)"
```
```   473    (fn _ => [rtac DmdImpl2 1,
```
```   474 	     etac StableBox 2,
```
```   475 	     auto_tac (temp_css addsimps2 [DmdAct])
```
```   476 	    ]);
```
```   477
```
```   478 (* ---------------- (Semi-)automatic invariant tactics ---------------------- *)
```
```   479
```
```   480 (* inv_tac reduces goals of the form ... ==> sigma |= []P *)
```
```   481 fun inv_tac css =
```
```   482    SELECT_GOAL
```
```   483      (EVERY [auto_tac css,
```
```   484              TRY (merge_box_tac 1),
```
```   485              rtac INV1I 1, (* fail if the goal is not a box *)
```
```   486              TRYALL (etac Stable)]);
```
```   487
```
```   488 (* auto_inv_tac applies inv_tac and then tries to attack the subgoals;
```
```   489    in simple cases it may be able to handle goals like MyProg .-> []Inv.
```
```   490    In these simple cases the simplifier seems to be more useful than the
```
```   491    auto-tactic, which applies too much propositional logic and simplifies
```
```   492    too late.
```
```   493 *)
```
```   494
```
```   495 fun auto_inv_tac ss =
```
```   496   SELECT_GOAL
```
```   497     ((inv_tac (claset(),ss) 1) THEN
```
```   498      (TRYALL (action_simp_tac (ss addsimps [Init_def,square_def]) [] [])));
```
```   499
```
```   500
```
```   501 qed_goalw "unless" TLA.thy [dmd_def]
```
```   502    "!!sigma. (sigma |= [](P .-> P` .| Q`)) ==> (sigma |= stable P .| <>Q`)"
```
```   503    (fn _ => [action_simp_tac (simpset()) [disjCI] [] 1,
```
```   504 	     merge_box_tac 1,
```
```   505 	     fast_tac (temp_cs addSEs [Stable]) 1
```
```   506 	    ]);
```
```   507
```
```   508
```
```   509 (* --------------------- Recursive expansions --------------------------------------- *)
```
```   510 section "recursive expansions";
```
```   511
```
```   512 (* Recursive expansions of [] and <>, restricted to state predicates to avoid looping *)
```
```   513 qed_goal "BoxRec" TLA.thy "([]\$P) .= (Init(\$P) .& ([]P\$))"
```
```   514    (fn _ => [auto_tac (temp_css addSIs2 [STL2bD]),
```
```   515 	     fast_tac (temp_cs addSEs [TLA2E]) 1,
```
```   516 	     auto_tac (temp_css addsimps2 [stable_def] addSEs2 [INV1I,STL4E])
```
```   517 	    ]);
```
```   518
```
```   519 qed_goalw "DmdRec" TLA.thy [dmd_def] "(<>\$P) .= (Init(\$P) .| (<>P\$))"
```
```   520    (fn _ => [Auto_tac(),
```
```   521 	     etac notE 1,
```
```   522 	     SELECT_GOAL (auto_tac (temp_css addsimps2 (stable_def::Init_simps)
```
```   523 				             addIs2 [INV1I] addEs2 [STL4E])) 1,
```
```   524 	     SELECT_GOAL (auto_tac (temp_css addsimps2 Init_simps addSDs2 [STL2bD])) 1,
```
```   525 	     fast_tac (temp_cs addSEs [notE,TLA2E]) 1
```
```   526 	    ]);
```
```   527
```
```   528 qed_goal "DmdRec2" TLA.thy
```
```   529    "!!sigma. [| (sigma |= <>(\$P)); (sigma |= [](.~P\$)) |] ==> (sigma |= Init(\$P))"
```
```   530    (fn _ => [dtac ((temp_unlift DmdRec) RS iffD1) 1,
```
```   531 	     SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1
```
```   532 	    ]);
```
```   533
```
```   534 (* The "=>" part of the following is a little intricate. *)
```
```   535 qed_goal "InfinitePrime" TLA.thy "([]<>\$P) .= ([]<>P\$)"
```
```   536    (fn _ => [Auto_tac(),
```
```   537 	     rtac classical 1,
```
```   538 	     rtac (temp_mp DBImplBDAct) 1,
```
```   539 	     subgoal_tac "sigma |= <>[]\$P" 1,
```
```   540 	     fast_tac (temp_cs addSEs [DmdImplE,TLA2E]) 1,
```
```   541 	     subgoal_tac "sigma |= <>[](<>\$P .& [].~P\$)" 1,
```
```   542 	     SELECT_GOAL (auto_tac (temp_css addsimps2 [boxact_def]
```
```   543 				             addSEs2 [DmdImplE,STL4E,DmdRec2])) 1,
```
```   544 	     SELECT_GOAL (auto_tac (temp_css addSIs2 [temp_mp STL6] addsimps2 more_temp_simps)) 1,
```
```   545 	     fast_tac (temp_cs addIs [temp_mp DmdPrime] addSEs [STL4E]) 1
```
```   546 	    ]);
```
```   547
```
```   548 (* ------------------------ fairness ------------------------------------------- *)
```
```   549 section "fairness";
```
```   550
```
```   551 (* alternative definitions of fairness *)
```
```   552 qed_goalw "WF_alt" TLA.thy [WF_def,dmd_def]
```
```   553    "WF(A)_v .= (([]<>.~\$(Enabled(<A>_v))) .| []<><A>_v)"
```
```   554    (fn _ => [ fast_tac temp_cs 1 ]);
```
```   555
```
```   556 qed_goalw "SF_alt" TLA.thy [SF_def,dmd_def]
```
```   557    "SF(A)_v .= ((<>[].~\$(Enabled(<A>_v))) .| []<><A>_v)"
```
```   558    (fn _ => [ fast_tac temp_cs 1 ]);
```
```   559
```
```   560 (* theorems to "box" fairness conditions *)
```
```   561 qed_goal "BoxWFI" TLA.thy
```
```   562    "!!sigma. (sigma |= WF(A)_v) ==> (sigma |= []WF(A)_v)"
```
```   563    (fn _ => [ auto_tac (temp_css addsimps2 (temp_rewrite WF_alt::more_temp_simps) addSIs2 [BoxOr]) ]);
```
```   564
```
```   565 qed_goal "WF_Box" TLA.thy "([]WF(A)_v) .= WF(A)_v"
```
```   566   (fn prems => [ fast_tac (temp_cs addSIs [BoxWFI] addSDs [STL2D]) 1 ]);
```
```   567
```
```   568 qed_goal "BoxSFI" TLA.thy
```
```   569    "!!sigma. (sigma |= SF(A)_v) ==> (sigma |= []SF(A)_v)"
```
```   570    (fn _ => [ auto_tac (temp_css addsimps2 (temp_rewrite SF_alt::more_temp_simps) addSIs2 [BoxOr]) ]);
```
```   571
```
```   572 qed_goal "SF_Box" TLA.thy "([]SF(A)_v) .= SF(A)_v"
```
```   573   (fn prems => [ fast_tac (temp_cs addSIs [BoxSFI] addSDs [STL2D]) 1 ]);
```
```   574
```
```   575 val more_temp_simps = more_temp_simps @ (map temp_rewrite [WF_Box, SF_Box]);
```
```   576
```
```   577 qed_goalw "SFImplWF" TLA.thy [SF_def,WF_def]
```
```   578   "!!sigma. (sigma |= SF(A)_v) ==> (sigma |= WF(A)_v)"
```
```   579   (fn _ => [ fast_tac (temp_cs addSDs [temp_mp DBImplBDAct]) 1 ]);
```
```   580
```
```   581 (* A tactic that "boxes" all fairness conditions. Apply more_temp_simps to "unbox". *)
```
```   582 val box_fair_tac = SELECT_GOAL (REPEAT (dresolve_tac [BoxWFI,BoxSFI] 1));
```
```   583
```
```   584
```
```   585 (* ------------------------------ leads-to ------------------------------ *)
```
```   586
```
```   587 section "~>";
```
```   588
```
```   589 qed_goalw "leadsto_init" TLA.thy [leadsto]
```
```   590    "!!sigma. [| (sigma |= Init P); (sigma |= P ~> Q) |] ==> (sigma |= <>Q)"
```
```   591    (fn _ => [ fast_tac (temp_cs addSDs [temp_mp STL2]) 1 ]);
```
```   592
```
```   593 qed_goalw "streett_leadsto" TLA.thy [leadsto]
```
```   594    "([]<>P .-> []<>Q) .= (<>(P ~> Q))"
```
```   595    (fn _ => [Auto_tac(),
```
```   596              asm_full_simp_tac (simpset() addsimps boxact_def::more_temp_simps) 1,
```
```   597              SELECT_GOAL (auto_tac (temp_css addSEs2 [DmdImplE,STL4E]
```
```   598                                              addsimps2 Init_simps)) 1,
```
```   599              SELECT_GOAL (auto_tac (temp_css addSIs2 [ImplDmdD] addSEs2 [STL4E])) 1,
```
```   600              subgoal_tac "sigma |= []<><>Q" 1,
```
```   601              asm_full_simp_tac (simpset() addsimps more_temp_simps) 1,
```
```   602              rewtac (temp_rewrite DmdAct),
```
```   603              dtac BoxDmdDmdBox 1, atac 1,
```
```   604              auto_tac (temp_css addSEs2 [DmdImplE,STL4E])
```
```   605             ]);
```
```   606
```
```   607 qed_goal "leadsto_infinite" TLA.thy
```
```   608    "!!sigma. [| (sigma |= []<>P); (sigma |= P ~> Q) |] ==> (sigma |= []<>Q)"
```
```   609    (fn _ => [rtac ((temp_unlift streett_leadsto) RS iffD2 RS mp) 1,
```
```   610              auto_tac (temp_css addSIs2 [ImplDmdD])
```
```   611             ]);
```
```   612
```
```   613 (* In particular, strong fairness is a Streett condition. The following
```
```   614    rules are sometimes easier to use than WF2 or SF2 below.
```
```   615 *)
```
```   616 qed_goalw "leadsto_SF" TLA.thy [SF_def]
```
```   617   "!!sigma. (sigma |= \$(Enabled(<A>_v)) ~> <A>_v) ==> sigma |= SF(A)_v"
```
```   618   (fn _ => [step_tac temp_cs 1,
```
```   619             rtac leadsto_infinite 1,
```
```   620             ALLGOALS atac
```
```   621            ]);
```
```   622
```
```   623 bind_thm("leadsto_WF", leadsto_SF RS SFImplWF);
```
```   624
```
```   625 (* introduce an invariant into the proof of a leadsto assertion.
```
```   626    []I => ((P ~> Q)  =  (P /\ I ~> Q))
```
```   627 *)
```
```   628 qed_goalw "INV_leadsto" TLA.thy [leadsto]
```
```   629    "!!sigma. [| (sigma |= []I); (sigma |= (P .& I) ~> Q) |] ==> (sigma |= P ~> Q)"
```
```   630    (fn _ => [etac STL4Edup 1, atac 1,
```
```   631 	     auto_tac (temp_css addsimps2 [Init_def] addSDs2 [STL2bD])
```
```   632 	    ]);
```
```   633
```
```   634 qed_goalw "leadsto_classical" TLA.thy [leadsto,dmd_def]
```
```   635    "!!sigma. (sigma |= [](Init P .& [].~Q .-> <>Q)) ==> (sigma |= P ~> Q)"
```
```   636    (fn _ => [fast_tac (temp_cs addSEs [STL4E]) 1]);
```
```   637
```
```   638 qed_goalw "leadsto_false" TLA.thy [leadsto]
```
```   639   "(P ~> #False) .= ([] .~P)"
```
```   640   (fn _ => [ auto_tac (temp_css addsimps2 boxact_def::Init_simps) ]);
```
```   641
```
```   642 (* basic leadsto properties, cf. Unity *)
```
```   643
```
```   644 qed_goal "ImplLeadsto" TLA.thy
```
```   645    "!!sigma. (sigma |= [](P .-> Q)) ==> (sigma |= (P ~> Q))"
```
```   646    (fn _ => [etac INV_leadsto 1, rewtac leadsto,
```
```   647 	     rtac (temp_unlift necT) 1,
```
```   648 	     auto_tac (temp_css addSIs2 [InitDmdD] addsimps2 [Init_def])
```
```   649 	    ]);
```
```   650
```
```   651 qed_goal "EnsuresLeadsto" TLA.thy
```
```   652    "A .& P .-> Q` ==> []A .-> (P ~> Q)"
```
```   653    (fn [prem] => [auto_tac (temp_css addSEs2 [INV_leadsto]),
```
```   654 		  rewtac leadsto,
```
```   655  		  auto_tac (temp_css addSIs2 [temp_unlift necT]),
```
```   656 		  rtac (temp_mp DmdPrime) 1, rtac InitDmdD 1,
```
```   657 		  auto_tac (action_css addsimps2 [Init_def] addSIs2 [action_mp prem])
```
```   658 		 ]);
```
```   659
```
```   660 qed_goalw "EnsuresLeadsto2" TLA.thy [leadsto]
```
```   661    "!!sigma. sigma |= [](P .-> Q`) ==> sigma |= P ~> Q"
```
```   662    (fn _ => [subgoal_tac "sigma |= []Init(P .-> Q`)" 1,
```
```   663              etac STL4E 1,
```
```   664              auto_tac (temp_css addsimps2 boxact_def::Init_simps
```
```   665                                 addIs2 [(temp_mp InitDmd) RS (temp_mp DmdPrime)])
```
```   666             ]);
```
```   667
```
```   668 qed_goal "EnsuresInfinite" TLA.thy
```
```   669    "[| (sigma |= []<>P); (sigma |= []A); A .& P .-> Q` |] ==> (sigma |= []<>Q)"
```
```   670    (fn prems => [REPEAT (resolve_tac (prems @ [leadsto_infinite,
```
```   671 					       temp_mp EnsuresLeadsto]) 1)]);
```
```   672
```
```   673 (*** Gronning's lattice rules (taken from TLP) ***)
```
```   674 section "Lattice rules";
```
```   675
```
```   676 qed_goalw "LatticeReflexivity" TLA.thy [leadsto] "F ~> F"
```
```   677    (fn _ => [REPEAT (resolve_tac [necT,InitDmd] 1)]);
```
```   678
```
```   679 qed_goalw "LatticeTransitivity" TLA.thy [leadsto]
```
```   680    "!!sigma. [| (sigma |= G ~> H); (sigma |= F ~> G) |] ==> (sigma |= F ~> H)"
```
```   681    (fn _ => [etac dup_boxE 1,  (* [][](Init G .-> H) *)
```
```   682 	     merge_box_tac 1,
```
```   683 	     auto_tac (temp_css addSEs2 [STL4E]),
```
```   684 	     rewtac (temp_rewrite DmdAct),
```
```   685 	     subgoal_tac "sigmaa |= <><> Init H" 1,
```
```   686 	     asm_full_simp_tac (simpset() addsimps more_temp_simps) 1,
```
```   687 	     fast_tac (temp_cs addSEs [DmdImpl2]) 1
```
```   688 	    ]);
```
```   689
```
```   690 qed_goalw "LatticeDisjunctionElim1" TLA.thy [leadsto]
```
```   691    "!!sigma. (sigma |= (F .| G) ~> H) ==> (sigma |= F ~> H)"
```
```   692    (fn _ => [ auto_tac (temp_css addsimps2 [Init_def] addSEs2 [STL4E]) ]);
```
```   693
```
```   694 qed_goalw "LatticeDisjunctionElim2" TLA.thy [leadsto]
```
```   695    "!!sigma. (sigma |= (F .| G) ~> H) ==> (sigma |= G ~> H)"
```
```   696    (fn _ => [ auto_tac (temp_css addsimps2 [Init_def] addSEs2 [STL4E]) ]);
```
```   697
```
```   698 qed_goalw "LatticeDisjunctionIntro" TLA.thy [leadsto]
```
```   699    "!!sigma. [| (sigma |= F ~> H); (sigma |= G ~> H) |] ==> (sigma |= (F .| G) ~> H)"
```
```   700    (fn _ => [merge_box_tac 1,
```
```   701 	     auto_tac (temp_css addsimps2 [Init_def] addSEs2 [STL4E])
```
```   702 	    ]);
```
```   703
```
```   704 qed_goal "LatticeDiamond" TLA.thy
```
```   705    "!!sigma. [| (sigma |= B ~> D); (sigma |= A ~> (B .| C)); (sigma |= C ~> D) |]  \
```
```   706 \            ==> (sigma |= A ~> D)"
```
```   707    (fn _ => [subgoal_tac "sigma |= (B .| C) ~> D" 1,
```
```   708 	     eres_inst_tac [("G", "B .| C")] LatticeTransitivity 1,
```
```   709 	     ALLGOALS (fast_tac (temp_cs addSIs [LatticeDisjunctionIntro]))
```
```   710 	    ]);
```
```   711
```
```   712 qed_goal "LatticeTriangle" TLA.thy
```
```   713    "!!sigma. [| (sigma |= B ~> D); (sigma |= A ~> (B .| D)) |] ==> (sigma |= A ~> D)"
```
```   714    (fn _ => [subgoal_tac "sigma |= (B .| D) ~> D" 1,
```
```   715 	     eres_inst_tac [("G", "B .| D")] LatticeTransitivity 1, atac 1,
```
```   716 	     auto_tac (temp_css addSIs2 [LatticeDisjunctionIntro] addIs2 [ImplLeadsto])
```
```   717 	    ]);
```
```   718
```
```   719 (*** Lamport's fairness rules ***)
```
```   720 section "Fairness rules";
```
```   721
```
```   722 qed_goalw "WF1" TLA.thy [leadsto]
```
```   723    "[| P .& N  .-> P` .| Q`;   \
```
```   724 \      P .& N .& <A>_v .-> Q`;   \
```
```   725 \      P .& N .-> \$(Enabled(<A>_v)) |]   \
```
```   726 \  ==> []N .& WF(A)_v .-> (P ~> Q)"
```
```   727    (fn [prem1,prem2,prem3]
```
```   728              => [auto_tac (temp_css addSDs2 [BoxWFI]),
```
```   729 		 etac STL4Edup 1, atac 1,
```
```   730 		 Auto_tac(),
```
```   731 		 subgoal_tac "sigmaa |= [](P .-> P` .| Q`)" 1,
```
```   732 		 auto_tac (temp_css addSDs2 [unless]),
```
```   733 		 etac (temp_conjimpE INV1) 1, atac 1,
```
```   734 		 merge_box_tac 1,
```
```   735 		 rtac STL2D 1,
```
```   736 		 rtac EnsuresInfinite 1, atac 2,
```
```   737 		 SELECT_GOAL (auto_tac (temp_css addsimps2 [WF_alt])) 1,
```
```   738 		 atac 2,
```
```   739 		 subgoal_tac "sigmaa |= [][]\$(Enabled(<A>_v))" 1,
```
```   740 		 merge_box_tac 1,
```
```   741 		 SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1,
```
```   742 		 SELECT_GOAL ((rewtac (temp_rewrite STL3)) THEN
```
```   743 			      (auto_tac (temp_css addSEs2 [STL4E] addSIs2 [action_mp prem3]))) 1,
```
```   744 		 fast_tac (action_cs addSIs [action_mp prem2]) 1,
```
```   745 		 fast_tac (temp_cs addIs [temp_mp DmdPrime]) 1,
```
```   746 		 fast_tac (temp_cs addSEs [STL4E] addSIs [action_mp prem1]) 1
```
```   747 		]);
```
```   748
```
```   749 (* Sometimes easier to use; designed for action B rather than state predicate Q *)
```
```   750 qed_goalw "WF_leadsto" TLA.thy [leadsto]
```
```   751    "[| N .& P .-> \$Enabled (<A>_v);            \
```
```   752 \      N .& <A>_v .-> B;                  \
```
```   753 \      [](N .& [.~A]_v) .-> stable P  |]  \
```
```   754 \   ==> []N .& WF(A)_v .-> (P ~> B)"
```
```   755    (fn [prem1,prem2,prem3]
```
```   756        => [auto_tac (temp_css addSDs2 [BoxWFI]),
```
```   757            etac STL4Edup 1, atac 1,
```
```   758            Auto_tac(),
```
```   759            subgoal_tac "sigmaa |= <><A>_v" 1,
```
```   760            SELECT_GOAL (auto_tac (temp_css addSEs2 [DmdImpl2,STL4E] addSIs2 [action_mp prem2])) 1,
```
```   761            rtac classical 1,
```
```   762            rtac STL2D 1,
```
```   763            auto_tac (temp_css addsimps2 WF_def::more_temp_simps addSEs2 [mp]),
```
```   764            rtac ImplDmdD 1,
```
```   765            rtac (temp_mp (prem1 RS STL4)) 1,
```
```   766            auto_tac (temp_css addsimps2 [split_box_conj]),
```
```   767            etac INV1I 1,
```
```   768            merge_act_box_tac 1,
```
```   769            auto_tac (temp_css addsimps2 [temp_rewrite not_angle] addSEs2 [temp_mp prem3])
```
```   770           ]);
```
```   771
```
```   772 qed_goalw "SF1" TLA.thy [leadsto]
```
```   773    "[| P .& N  .-> P` .| Q`;   \
```
```   774 \      P .& N .& <A>_v .-> Q`;   \
```
```   775 \      []P .& []N .& []F .-> <>\$(Enabled(<A>_v)) |]   \
```
```   776 \  ==> []N .& SF(A)_v .& []F .-> (P ~> Q)"
```
```   777    (fn [prem1,prem2,prem3] =>
```
```   778                 [auto_tac (temp_css addSDs2 [BoxSFI]),
```
```   779 		 eres_inst_tac [("F","F")] dup_boxE 1,
```
```   780 		 merge_temp_box_tac 1,
```
```   781 		 etac STL4Edup 1, atac 1,
```
```   782 		 Auto_tac(),
```
```   783 		 subgoal_tac "sigmaa |= [](P .-> P` .| Q`)" 1,
```
```   784 		 auto_tac (temp_css addSDs2 [unless]),
```
```   785 		 etac (temp_conjimpE INV1) 1, atac 1,
```
```   786 		 merge_act_box_tac 1,
```
```   787 		 rtac STL2D 1,
```
```   788 		 rtac EnsuresInfinite 1, atac 2,
```
```   789 		 SELECT_GOAL (auto_tac (temp_css addsimps2 [SF_alt])) 1,
```
```   790 		 atac 2,
```
```   791 		 subgoal_tac "sigmaa |= []<>\$(Enabled(<A>_v))" 1,
```
```   792 		 SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1,
```
```   793 		 eres_inst_tac [("F","F")] dup_boxE 1,
```
```   794 		 etac STL4Edup 1, atac 1,
```
```   795 		 fast_tac (temp_cs addSEs [STL4E] addSIs [temp_mp prem3]) 1,
```
```   796 		 fast_tac (action_cs addSIs [action_mp prem2]) 1,
```
```   797 		 fast_tac (temp_cs addIs [temp_mp DmdPrime]) 1,
```
```   798 		 fast_tac (temp_cs addSEs [STL4E] addSIs [action_mp prem1]) 1
```
```   799 		]);
```
```   800
```
```   801 qed_goal "WF2" TLA.thy
```
```   802    "[| N .& <B>_f .-> <M>_g;   \
```
```   803 \      P .& P` .& <N .& A>_f .-> B;   \
```
```   804 \      P .& \$(Enabled(<M>_g)) .-> \$(Enabled(<A>_f));   \
```
```   805 \      [](N .& [.~B]_f) .& WF(A)_f .& []F .& <>[](\$(Enabled(<M>_g))) .-> <>[]P |]   \
```
```   806 \  ==> []N .& WF(A)_f .& []F .-> WF(M)_g"
```
```   807    (fn [prem1,prem2,prem3,prem4]
```
```   808        => [Auto_tac(),
```
```   809 	   case_tac "sigma |= <>[]\$Enabled(<M>_g)" 1,
```
```   810 	   SELECT_GOAL (auto_tac (temp_css addsimps2 [WF_def,dmd_def])) 2,
```
```   811 	   case_tac "sigma |= <>[][.~B]_f" 1,
```
```   812 	   subgoal_tac "sigma |= <>[]P" 1,
```
```   813 	   asm_full_simp_tac (simpset() addsimps [WF_def]) 1,
```
```   814 	   rtac (temp_mp (prem1 RS DmdImpl RS STL4)) 1,
```
```   815 	   eres_inst_tac [("V","sigma |= <>[][.~B]_f")] thin_rl 1,
```
```   816 	   etac (temp_conjimpE STL6) 1, atac 1,
```
```   817 	   subgoal_tac "sigma |= <>[]\$Enabled(<A>_f)" 1,
```
```   818 	   dtac mp 1, atac 1,
```
```   819 	   subgoal_tac "sigma |= <>([]N .& []P .& []<><A>_f)" 1,
```
```   820 	   rtac ((temp_unlift DmdBoxDmd) RS iffD1) 1,
```
```   821 	   eres_inst_tac [("F","[]N .& []P .& []<><A>_f")] DmdImplE 1,
```
```   822 	   SELECT_GOAL (Auto_tac()) 1,
```
```   823 	   dres_inst_tac [("P","P")] (temp_mp BoxPrime) 1,
```
```   824 	   merge_act_box_tac 1,
```
```   825 	   etac InfImpl 1, atac 1,
```
```   826 	   SELECT_GOAL (auto_tac (temp_css addsimps2 [angle_def] addSIs2 [action_mp prem2])) 1,
```
```   827 	   etac BoxDmd 1,
```
```   828 	   dres_inst_tac [("F","<><A>_f"),("G","[]P")] BoxDmd 1, atac 1,
```
```   829 	   eres_inst_tac [("F","[]<><A>_f .& []P")] DmdImplE 1,
```
```   830 	   SELECT_GOAL (Auto_tac ()) 1,
```
```   831 	   rtac (temp_mp (prem3 RS STL4 RS DmdImpl)) 1,
```
```   832 	   fast_tac (temp_cs addIs [STL4E,DmdImplE]) 1,
```
```   833 	   etac (temp_conjimpE STL6) 1, atac 1,
```
```   834 	   eres_inst_tac [("V","sigma |= <>[][.~ B]_f")] thin_rl 1,
```
```   835 	   dtac BoxWFI 1,
```
```   836 	   eres_inst_tac [("F","N")] dup_boxE 1,
```
```   837 	   eres_inst_tac [("F","F")] dup_boxE 1,
```
```   838 	   merge_temp_box_tac 1,
```
```   839 	   dtac BoxDmd 1, atac 1,
```
```   840 	   eres_inst_tac [("V","sigma |= <>[](\$Enabled (<M>_g) .& [.~ B]_f)")] thin_rl 1,
```
```   841 	   rtac dup_dmdD 1,
```
```   842 	   rtac (temp_mp (prem4 RS DmdImpl)) 1,
```
```   843 	   etac DmdImplE 1,
```
```   844 	   SELECT_GOAL
```
```   845 	     (auto_tac (temp_css addsimps2 [symmetric(temp_rewrite STL5), temp_rewrite STL3]
```
```   846 		                 addIs2 [(temp_unlift WF_Box) RS iffD1, temp_mp ImplDmd])) 1,
```
```   847 	   asm_full_simp_tac (simpset() addsimps (WF_def::more_temp_simps)) 1,
```
```   848 	   etac InfImpl 1, atac 1,
```
```   849 	   SELECT_GOAL (auto_tac (temp_css addSIs2 [action_mp prem1])) 1,
```
```   850 	   ALLGOALS (asm_full_simp_tac (simpset() addsimps [square_def,angle_def]))
```
```   851 	  ]);
```
```   852
```
```   853 qed_goal "SF2" TLA.thy
```
```   854    "[| N .& <B>_f .-> <M>_g;   \
```
```   855 \      P .& P` .& <N .& A>_f .-> B;   \
```
```   856 \      P .& \$(Enabled(<M>_g)) .-> \$(Enabled(<A>_f));   \
```
```   857 \      [](N .& [.~B]_f) .& SF(A)_f .& []F .& []<>(\$(Enabled(<M>_g))) .-> <>[]P |]   \
```
```   858 \  ==> []N .& SF(A)_f .& []F .-> SF(M)_g"
```
```   859    (fn [prem1,prem2,prem3,prem4]
```
```   860        => [Auto_tac(),
```
```   861 	   case_tac "sigma |= []<>\$Enabled(<M>_g)" 1,
```
```   862 	   SELECT_GOAL (auto_tac (temp_css addsimps2 [SF_def,dmd_def])) 2,
```
```   863 	   case_tac "sigma |= <>[][.~B]_f" 1,
```
```   864 	   subgoal_tac "sigma |= <>[]P" 1,
```
```   865 	   asm_full_simp_tac (simpset() addsimps [SF_def]) 1,
```
```   866 	   rtac (temp_mp (prem1 RS DmdImpl RS STL4)) 1,
```
```   867 	   eres_inst_tac [("V","sigma |= <>[][.~B]_f")] thin_rl 1,
```
```   868 	   dtac BoxDmdDmdBox 1, atac 1,
```
```   869 	   subgoal_tac "sigma |= []<>\$Enabled(<A>_f)" 1,
```
```   870 	   dtac mp 1, atac 1,
```
```   871 	   subgoal_tac "sigma |= <>([]N .& []P .& []<><A>_f)" 1,
```
```   872 	   rtac ((temp_unlift DmdBoxDmd) RS iffD1) 1,
```
```   873 	   eres_inst_tac [("F","[]N .& []P .& []<><A>_f")] DmdImplE 1,
```
```   874 	   SELECT_GOAL (Auto_tac()) 1,
```
```   875 	   dres_inst_tac [("P","P")] (temp_mp BoxPrime) 1,
```
```   876 	   merge_act_box_tac 1,
```
```   877 	   etac InfImpl 1, atac 1,
```
```   878 	   SELECT_GOAL (auto_tac (temp_css addsimps2 [angle_def] addSIs2 [action_mp prem2])) 1,
```
```   879 	   etac BoxDmd 1,
```
```   880 	   dres_inst_tac [("F","<><A>_f"),("G","[]P")] BoxDmd 1, atac 1,
```
```   881 	   eres_inst_tac [("F","[]<><A>_f .& []P")] DmdImplE 1,
```
```   882 	   SELECT_GOAL (Auto_tac ()) 1,
```
```   883 	   rtac (temp_mp (prem3 RS DmdImpl RS STL4)) 1,
```
```   884 	   fast_tac (temp_cs addEs [STL4E,DmdImplE]) 1,
```
```   885 	   dtac BoxSFI 1,
```
```   886 	   eres_inst_tac [("F","N")] dup_boxE 1,
```
```   887 	   eres_inst_tac [("F","F")] dup_boxE 1,
```
```   888 	   eres_inst_tac [("F","<>\$Enabled (<M>_g)")] dup_boxE 1,
```
```   889 	   merge_temp_box_tac 1,
```
```   890 	   dtac (temp_conjmp BoxDmdT2) 1, atac 1,
```
```   891 	   rtac dup_dmdD 1,
```
```   892 	   rtac (temp_mp (prem4 RS DmdImpl)) 1,
```
```   893 	   SELECT_GOAL
```
```   894 	     (auto_tac (temp_css addsimps2 [symmetric(temp_rewrite STL5), temp_rewrite STL3]
```
```   895 		                 addIs2 [(temp_unlift WF_Box) RS iffD1, temp_mp ImplDmd]
```
```   896 			         addSEs2 [DmdImplE])) 1,
```
```   897 	   asm_full_simp_tac (simpset() addsimps (SF_def::more_temp_simps)) 1,
```
```   898 	   eres_inst_tac [("F",".~ [.~ B]_f")] InfImpl 1, atac 1,
```
```   899 	   SELECT_GOAL (auto_tac (temp_css addSIs2 [action_mp prem1])) 1,
```
```   900 	   ALLGOALS (asm_full_simp_tac (simpset() addsimps [square_def,angle_def]))
```
```   901 	  ]);
```
```   902
```
```   903 (* ------------------------------------------------------------------------- *)
```
```   904 (***           Liveness proofs by well-founded orderings                   ***)
```
```   905 (* ------------------------------------------------------------------------- *)
```
```   906 section "Well-founded orderings";
```
```   907
```
```   908 qed_goal "wf_dmd" TLA.thy
```
```   909   "[| (wf r);  \
```
```   910 \     !!x. sigma |= [](F x .-> <>G .| <>(REX y. #((y,x):r) .& F y))   \
```
```   911 \  |] ==> sigma |= [](F x .-> <>G)"
```
```   912   (fn prem1::prems =>
```
```   913          [cut_facts_tac [prem1] 1,
```
```   914           etac wf_induct 1,
```
```   915           subgoal_tac "sigma |= []((REX y. #((y,x):r) .& F y) .-> <>G)" 1,
```
```   916 	  cut_facts_tac prems 1,
```
```   917 	  etac STL4Edup 1, atac 1,
```
```   918 	  Auto_tac(), etac swap 1, atac 1,
```
```   919 	  rtac dup_dmdD 1,
```
```   920 	  etac DmdImpl2 1, atac 1,
```
```   921 	  subgoal_tac "sigma |= [](RALL y. #((y,x):r) .& F y .-> <>G)" 1,
```
```   922 	  fast_tac (temp_cs addSEs [STL4E]) 1,
```
```   923 	  auto_tac (temp_css addsimps2 [all_box]),
```
```   924 	  etac allE 1, etac impCE 1,
```
```   925 	  rtac (temp_unlift necT) 1,
```
```   926 	  auto_tac (temp_css addSEs2 [STL4E])
```
```   927          ]);
```
```   928
```
```   929 (* Special case: leadsto via well-foundedness *)
```
```   930 qed_goalw "wf_leadsto" TLA.thy [leadsto]
```
```   931   "[| (wf r);  \
```
```   932 \     !!x. sigma |= P x ~> (Q .| (REX y. #((y,x):r) .& P y))   \
```
```   933 \  |] ==> sigma |= P x ~> Q"
```
```   934   (fn prems => [REPEAT (resolve_tac (wf_dmd::prems) 1),
```
```   935 		resolve_tac (prems RL [STL4E]) 1,
```
```   936 		auto_tac (temp_css addsimps2 [temp_rewrite DmdOr]),
```
```   937                 fast_tac temp_cs 1,
```
```   938 		etac swap 1,
```
```   939 		rewtac (temp_rewrite DmdAct),
```
```   940 		auto_tac (temp_css addsimps2 [Init_def] addSEs2 [DmdImplE])
```
```   941 	       ]);
```
```   942
```
```   943 (* If r is well-founded, state function v cannot decrease forever *)
```
```   944 qed_goal "wf_not_box_decrease" TLA.thy
```
```   945   "!!r. wf r ==> [][ {[v\$, \$v]} .: #r ]_v .-> <>[][#False]_v"
```
```   946   (fn _ => [Auto_tac(),
```
```   947             subgoal_tac "ALL x. (sigma |= [](Init(\$v .= #x) .-> <>[][#False]_v))" 1,
```
```   948             etac allE 1,
```
```   949             dtac STL2D 1,
```
```   950             auto_tac (temp_css addsimps2 [Init_def]),
```
```   951             etac wf_dmd 1,
```
```   952             etac dup_boxE 1,
```
```   953             etac STL4E 1,
```
```   954             action_simp_tac (simpset() addsimps [con_abs]) [tempI] [] 1,
```
```   955             case_tac "sigma |= <>[][#False]_v" 1,
```
```   956             ALLGOALS Asm_full_simp_tac,
```
```   957             rewrite_goals_tac more_temp_simps,
```
```   958             dtac STL2D 1,
```
```   959             subgoal_tac "sigma |= <>(REX y. #((y, xa) : r) .& (\$v .= #y))" 1,
```
```   960             SELECT_GOAL (auto_tac (temp_css addsimps2 [DmdAct,Init_def]
```
```   961                                             addEs2 [DmdImplE])) 1,
```
```   962             subgoal_tac "sigma |= (stable (\$v .= #xa) .| <>(REX y. #((y, xa) : r) .& \$v .= #y)`)" 1,
```
```   963             case_tac "sigma |= stable (\$v .= #xa)" 1,
```
```   964             SELECT_GOAL (auto_tac (temp_css addIs2 [temp_mp DmdPrime])) 2,
```
```   965             SELECT_GOAL (rewrite_goals_tac ((symmetric (temp_rewrite NotBox))::action_rews)) 1,
```
```   966             etac swap 1,
```
```   967             subgoal_tac "sigma |= [](\$v .= #xa)" 1,
```
```   968             dres_inst_tac [("P", "\$v .= #xa")] (temp_mp BoxPrime) 1,
```
```   969             SELECT_GOAL (auto_tac (temp_css addEs2 [STL4E] addsimps2 [square_def])) 1,
```
```   970             SELECT_GOAL (auto_tac (temp_css addSIs2 [INV1I] addsimps2 [Init_def])) 1,
```
```   971             auto_tac (temp_css addsimps2 [square_def] addSIs2 [unless] addSEs2 [STL4E])
```
```   972            ]);
```
```   973
```
```   974 (* "wf ?r  ==>  <>[][{[?v\$, \$?v]} .: #?r]_?v .-> <>[][#False]_?v" *)
```
```   975 bind_thm("wf_not_dmd_box_decrease",
```
```   976          standard(rewrite_rule more_temp_simps (wf_not_box_decrease RS DmdImpl)));
```
```   977
```
```   978 (* If there are infinitely many steps where v decreases w.r.t. r, then there
```
```   979    have to be infinitely many non-stuttering steps where v doesn't decrease.
```
```   980 *)
```
```   981 qed_goal "wf_box_dmd_decrease" TLA.thy
```
```   982   "wf r ==> []<>({[v\$, \$v]} .: #r) .-> []<><.~({[v\$, \$v]} .: #r)>_v"
```
```   983   (fn [prem] => [Auto_tac(),
```
```   984                  rtac ccontr 1,
```
```   985                  asm_full_simp_tac
```
```   986                    (simpset() addsimps ([action_rewrite not_angle] @ more_temp_simps)) 1,
```
```   987                  dtac (prem RS (temp_mp wf_not_dmd_box_decrease)) 1,
```
```   988                  dtac BoxDmdDmdBox 1, atac 1,
```
```   989                  subgoal_tac "sigma |= []<>((#False)::action)" 1,
```
```   990                  SELECT_GOAL (Auto_tac()) 1,
```
```   991                  etac STL4E 1,
```
```   992                  rtac DmdImpl 1,
```
```   993                  auto_tac (action_css addsimps2 [square_def] addSEs2 [prem RS wf_irrefl])
```
```   994                 ]);
```
```   995
```
```   996 (* In particular, for natural numbers, if n decreases infinitely often
```
```   997    then it has to increase infinitely often.
```
```   998 *)
```
```   999 qed_goal "nat_box_dmd_decrease" TLA.thy
```
```  1000   "!!n::nat stfun. []<>(n\$ .< \$n) .-> []<>(\$n .< n\$)"
```
```  1001   (fn _ => [Auto_tac(),
```
```  1002             subgoal_tac "sigma |= []<><.~( {[n\$,\$n]} .: #less_than)>_n" 1,
```
```  1003             etac thin_rl 1, etac STL4E 1, rtac DmdImpl 1,
```
```  1004             SELECT_GOAL (auto_tac (claset(), simpset() addsimps [angle_def])) 1,
```
```  1005             rtac nat_less_cases 1,
```
```  1006             Auto_tac(),
```
```  1007             rtac (temp_mp wf_box_dmd_decrease) 1,
```
```  1008             auto_tac (claset() addSEs [STL4E] addSIs [DmdImpl], simpset())
```
```  1009            ]);
```
```  1010
```
```  1011 (* ------------------------------------------------------------------------- *)
```
```  1012 (***           Flexible quantification over state variables                ***)
```
```  1013 (* ------------------------------------------------------------------------- *)
```
```  1014 section "Flexible quantification";
```
```  1015
```
```  1016 qed_goal "aallI" TLA.thy
```
```  1017   "(!!x. base_var x ==> sigma |= F x) ==> sigma |= (AALL x. F(x))"
```
```  1018   (fn prems => [auto_tac (temp_css addsimps2 [aall_def] addSEs2 [eexE] addSDs2 prems)]);
```
```  1019
```
```  1020 qed_goal "aallE" TLA.thy
```
```  1021    "[| sigma |= (AALL x. F(x));  (!!sigma. sigma |= F(x) ==> P sigma) |] \
```
```  1022 \   ==> (P sigma)::bool"
```
```  1023    (fn prems => [cut_facts_tac prems 1,
```
```  1024 		 resolve_tac prems 1,
```
```  1025 		 rewrite_goals_tac (aall_def::intensional_rews),
```
```  1026 		 etac swap 1,
```
```  1027 		 auto_tac (temp_css addSIs2 [temp_mp eexI])
```
```  1028 		]);
```
```  1029
```
```  1030 (* monotonicity of quantification *)
```
```  1031 qed_goal "eex_mono" TLA.thy
```
```  1032   "[| sigma |= EEX x. F(x); !!x. F(x) .-> G(x) |] ==> sigma |= EEX x. G(x)"
```
```  1033   (fn [min,maj] => [cut_facts_tac [min] 1,
```
```  1034                     etac eexE 1,
```
```  1035                     REPEAT (ares_tac (map temp_mp [eexI,maj]) 1)
```
```  1036                    ]);
```
```  1037
```
```  1038 qed_goal "aall_mono" TLA.thy
```
```  1039   "[| sigma |= AALL x. F(x); !!x. F(x) .-> G(x) |] ==> sigma |= AALL x. G(x)"
```
```  1040   (fn [min,maj] => [cut_facts_tac [min] 1,
```
```  1041                     fast_tac (temp_cs addSIs [aallI, temp_mp maj]
```
```  1042                                       addEs [aallE]) 1
```
```  1043                    ]);
```
```  1044
```
```  1045 (* ----------------------------------------------------------------------
```
```  1046    example of a history variable: existence of a clock
```
```  1047
```
```  1048 goal TLA.thy "(EEX h. Init(\$h .= #True) .& [](h\$ .~= \$h))";
```
```  1049 br tempI 1;
```
```  1050 br historyI 1;
```
```  1051 bws action_rews;
```
```  1052 by (TRYALL (rtac impI));
```
```  1053 by (TRYALL (etac conjE));
```
```  1054 ba 3;
```
```  1055 by (Asm_full_simp_tac 3);
```
```  1056 by (auto_tac (temp_css addSIs2 [(temp_unlift Init_true) RS iffD2, temp_unlift BoxTrue]));
```
```  1057 (** solved **)
```
```  1058
```
```  1059 ---------------------------------------------------------------------- *)
```