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