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