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