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