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