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