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