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