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