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