src/HOL/TLA/Action.thy
author wenzelm
Mon Feb 10 21:00:56 2014 +0100 (2014-02-10)
changeset 55382 9218fa411c15
parent 54742 7a86358a3c0b
child 56256 1e01c159e7d9
permissions -rw-r--r--
prefer vacuous definitional type classes over axiomatic ones;
wenzelm@35108
     1
(*  Title:      HOL/TLA/Action.thy 
wenzelm@35108
     2
    Author:     Stephan Merz
wenzelm@35108
     3
    Copyright:  1998 University of Munich
wenzelm@21624
     4
*)
wenzelm@3807
     5
wenzelm@21624
     6
header {* The action level of TLA as an Isabelle theory *}
wenzelm@3807
     7
wenzelm@17309
     8
theory Action
wenzelm@17309
     9
imports Stfun
wenzelm@17309
    10
begin
wenzelm@17309
    11
wenzelm@3807
    12
wenzelm@6255
    13
(** abstract syntax **)
wenzelm@6255
    14
wenzelm@42018
    15
type_synonym 'a trfun = "(state * state) => 'a"
wenzelm@42018
    16
type_synonym action   = "bool trfun"
wenzelm@6255
    17
wenzelm@55382
    18
instance prod :: (world, world) world ..
wenzelm@3807
    19
wenzelm@3807
    20
consts
wenzelm@6255
    21
  (** abstract syntax **)
wenzelm@17309
    22
  before        :: "'a stfun => 'a trfun"
wenzelm@17309
    23
  after         :: "'a stfun => 'a trfun"
wenzelm@17309
    24
  unch          :: "'a stfun => action"
wenzelm@6255
    25
wenzelm@17309
    26
  SqAct         :: "[action, 'a stfun] => action"
wenzelm@17309
    27
  AnAct         :: "[action, 'a stfun] => action"
wenzelm@17309
    28
  enabled       :: "action => stpred"
wenzelm@6255
    29
wenzelm@6255
    30
(** concrete syntax **)
wenzelm@6255
    31
wenzelm@6255
    32
syntax
wenzelm@6255
    33
  (* Syntax for writing action expressions in arbitrary contexts *)
wenzelm@35354
    34
  "_ACT"        :: "lift => 'a"                      ("(ACT _)")
wenzelm@3807
    35
wenzelm@17309
    36
  "_before"     :: "lift => lift"                    ("($_)"  [100] 99)
wenzelm@17309
    37
  "_after"      :: "lift => lift"                    ("(_$)"  [100] 99)
wenzelm@17309
    38
  "_unchanged"  :: "lift => lift"                    ("(unchanged _)" [100] 99)
wenzelm@6255
    39
wenzelm@6255
    40
  (*** Priming: same as "after" ***)
wenzelm@17309
    41
  "_prime"      :: "lift => lift"                    ("(_`)" [100] 99)
wenzelm@6255
    42
wenzelm@17309
    43
  "_SqAct"      :: "[lift, lift] => lift"            ("([_]'_(_))" [0,1000] 99)
wenzelm@17309
    44
  "_AnAct"      :: "[lift, lift] => lift"            ("(<_>'_(_))" [0,1000] 99)
wenzelm@17309
    45
  "_Enabled"    :: "lift => lift"                    ("(Enabled _)" [100] 100)
wenzelm@3807
    46
wenzelm@6255
    47
translations
wenzelm@6255
    48
  "ACT A"            =>   "(A::state*state => _)"
wenzelm@35108
    49
  "_before"          ==   "CONST before"
wenzelm@35108
    50
  "_after"           ==   "CONST after"
wenzelm@9517
    51
  "_prime"           =>   "_after"
wenzelm@35108
    52
  "_unchanged"       ==   "CONST unch"
wenzelm@35108
    53
  "_SqAct"           ==   "CONST SqAct"
wenzelm@35108
    54
  "_AnAct"           ==   "CONST AnAct"
wenzelm@35108
    55
  "_Enabled"         ==   "CONST enabled"
wenzelm@6255
    56
  "w |= [A]_v"       <=   "_SqAct A v w"
wenzelm@6255
    57
  "w |= <A>_v"       <=   "_AnAct A v w"
wenzelm@6255
    58
  "s |= Enabled A"   <=   "_Enabled A s"
wenzelm@6255
    59
  "w |= unchanged f" <=   "_unchanged f w"
wenzelm@3807
    60
wenzelm@47968
    61
axiomatization where
wenzelm@47968
    62
  unl_before:    "(ACT $v) (s,t) == v s" and
wenzelm@47968
    63
  unl_after:     "(ACT v$) (s,t) == v t" and
wenzelm@3807
    64
wenzelm@17309
    65
  unchanged_def: "(s,t) |= unchanged v == (v t = v s)"
wenzelm@47968
    66
wenzelm@47968
    67
defs
wenzelm@17309
    68
  square_def:    "ACT [A]_v == ACT (A | unchanged v)"
wenzelm@17309
    69
  angle_def:     "ACT <A>_v == ACT (A & ~ unchanged v)"
wenzelm@3807
    70
wenzelm@17309
    71
  enabled_def:   "s |= Enabled A  ==  EX u. (s,u) |= A"
wenzelm@17309
    72
wenzelm@21624
    73
wenzelm@21624
    74
(* The following assertion specializes "intI" for any world type
wenzelm@21624
    75
   which is a pair, not just for "state * state".
wenzelm@21624
    76
*)
wenzelm@21624
    77
wenzelm@21624
    78
lemma actionI [intro!]:
wenzelm@21624
    79
  assumes "!!s t. (s,t) |= A"
wenzelm@21624
    80
  shows "|- A"
haftmann@27104
    81
  apply (rule assms intI prod.induct)+
wenzelm@21624
    82
  done
wenzelm@21624
    83
wenzelm@21624
    84
lemma actionD [dest]: "|- A ==> (s,t) |= A"
wenzelm@21624
    85
  apply (erule intD)
wenzelm@21624
    86
  done
wenzelm@21624
    87
wenzelm@21624
    88
lemma pr_rews [int_rewrite]:
wenzelm@21624
    89
  "|- (#c)` = #c"
wenzelm@21624
    90
  "!!f. |- f<x>` = f<x` >"
wenzelm@21624
    91
  "!!f. |- f<x,y>` = f<x`,y` >"
wenzelm@21624
    92
  "!!f. |- f<x,y,z>` = f<x`,y`,z` >"
wenzelm@21624
    93
  "|- (! x. P x)` = (! x. (P x)`)"
wenzelm@21624
    94
  "|- (? x. P x)` = (? x. (P x)`)"
wenzelm@21624
    95
  by (rule actionI, unfold unl_after intensional_rews, rule refl)+
wenzelm@21624
    96
wenzelm@21624
    97
wenzelm@21624
    98
lemmas act_rews [simp] = unl_before unl_after unchanged_def pr_rews
wenzelm@21624
    99
wenzelm@21624
   100
lemmas action_rews = act_rews intensional_rews
wenzelm@21624
   101
wenzelm@21624
   102
wenzelm@21624
   103
(* ================ Functions to "unlift" action theorems into HOL rules ================ *)
wenzelm@21624
   104
wenzelm@21624
   105
ML {*
wenzelm@21624
   106
(* The following functions are specialized versions of the corresponding
wenzelm@21624
   107
   functions defined in Intensional.ML in that they introduce a
wenzelm@21624
   108
   "world" parameter of the form (s,t) and apply additional rewrites.
wenzelm@21624
   109
*)
wenzelm@21624
   110
wenzelm@54742
   111
fun action_unlift ctxt th =
wenzelm@54742
   112
  (rewrite_rule ctxt @{thms action_rews} (th RS @{thm actionD}))
wenzelm@54742
   113
    handle THM _ => int_unlift ctxt th;
wenzelm@21624
   114
wenzelm@21624
   115
(* Turn  |- A = B  into meta-level rewrite rule  A == B *)
wenzelm@21624
   116
val action_rewrite = int_rewrite
wenzelm@21624
   117
wenzelm@54742
   118
fun action_use ctxt th =
wenzelm@21624
   119
    case (concl_of th) of
wenzelm@21624
   120
      Const _ $ (Const ("Intensional.Valid", _) $ _) =>
wenzelm@54742
   121
              (flatten (action_unlift ctxt th) handle THM _ => th)
wenzelm@21624
   122
    | _ => th;
wenzelm@21624
   123
*}
wenzelm@21624
   124
wenzelm@54742
   125
attribute_setup action_unlift =
wenzelm@54742
   126
  {* Scan.succeed (Thm.rule_attribute (action_unlift o Context.proof_of)) *}
wenzelm@54742
   127
attribute_setup action_rewrite =
wenzelm@54742
   128
  {* Scan.succeed (Thm.rule_attribute (action_rewrite o Context.proof_of)) *}
wenzelm@54742
   129
attribute_setup action_use =
wenzelm@54742
   130
  {* Scan.succeed (Thm.rule_attribute (action_use o Context.proof_of)) *}
wenzelm@21624
   131
wenzelm@21624
   132
wenzelm@21624
   133
(* =========================== square / angle brackets =========================== *)
wenzelm@21624
   134
wenzelm@21624
   135
lemma idle_squareI: "(s,t) |= unchanged v ==> (s,t) |= [A]_v"
wenzelm@21624
   136
  by (simp add: square_def)
wenzelm@21624
   137
wenzelm@21624
   138
lemma busy_squareI: "(s,t) |= A ==> (s,t) |= [A]_v"
wenzelm@21624
   139
  by (simp add: square_def)
wenzelm@21624
   140
  
wenzelm@21624
   141
lemma squareE [elim]:
wenzelm@21624
   142
  "[| (s,t) |= [A]_v; A (s,t) ==> B (s,t); v t = v s ==> B (s,t) |] ==> B (s,t)"
wenzelm@21624
   143
  apply (unfold square_def action_rews)
wenzelm@21624
   144
  apply (erule disjE)
wenzelm@21624
   145
  apply simp_all
wenzelm@21624
   146
  done
wenzelm@21624
   147
wenzelm@21624
   148
lemma squareCI [intro]: "[| v t ~= v s ==> A (s,t) |] ==> (s,t) |= [A]_v"
wenzelm@21624
   149
  apply (unfold square_def action_rews)
wenzelm@21624
   150
  apply (rule disjCI)
wenzelm@21624
   151
  apply (erule (1) meta_mp)
wenzelm@21624
   152
  done
wenzelm@21624
   153
wenzelm@21624
   154
lemma angleI [intro]: "!!s t. [| A (s,t); v t ~= v s |] ==> (s,t) |= <A>_v"
wenzelm@21624
   155
  by (simp add: angle_def)
wenzelm@21624
   156
wenzelm@21624
   157
lemma angleE [elim]: "[| (s,t) |= <A>_v; [| A (s,t); v t ~= v s |] ==> R |] ==> R"
wenzelm@21624
   158
  apply (unfold angle_def action_rews)
wenzelm@21624
   159
  apply (erule conjE)
wenzelm@21624
   160
  apply simp
wenzelm@21624
   161
  done
wenzelm@21624
   162
wenzelm@21624
   163
lemma square_simulation:
wenzelm@21624
   164
   "!!f. [| |- unchanged f & ~B --> unchanged g;    
wenzelm@21624
   165
            |- A & ~unchanged g --> B               
wenzelm@21624
   166
         |] ==> |- [A]_f --> [B]_g"
wenzelm@21624
   167
  apply clarsimp
wenzelm@21624
   168
  apply (erule squareE)
wenzelm@21624
   169
  apply (auto simp add: square_def)
wenzelm@21624
   170
  done
wenzelm@21624
   171
wenzelm@21624
   172
lemma not_square: "|- (~ [A]_v) = <~A>_v"
wenzelm@21624
   173
  by (auto simp: square_def angle_def)
wenzelm@21624
   174
wenzelm@21624
   175
lemma not_angle: "|- (~ <A>_v) = [~A]_v"
wenzelm@21624
   176
  by (auto simp: square_def angle_def)
wenzelm@21624
   177
wenzelm@21624
   178
wenzelm@21624
   179
(* ============================== Facts about ENABLED ============================== *)
wenzelm@21624
   180
wenzelm@21624
   181
lemma enabledI: "|- A --> $Enabled A"
wenzelm@21624
   182
  by (auto simp add: enabled_def)
wenzelm@21624
   183
wenzelm@21624
   184
lemma enabledE: "[| s |= Enabled A; !!u. A (s,u) ==> Q |] ==> Q"
wenzelm@21624
   185
  apply (unfold enabled_def)
wenzelm@21624
   186
  apply (erule exE)
wenzelm@21624
   187
  apply simp
wenzelm@21624
   188
  done
wenzelm@21624
   189
wenzelm@21624
   190
lemma notEnabledD: "|- ~$Enabled G --> ~ G"
wenzelm@21624
   191
  by (auto simp add: enabled_def)
wenzelm@21624
   192
wenzelm@21624
   193
(* Monotonicity *)
wenzelm@21624
   194
lemma enabled_mono:
wenzelm@21624
   195
  assumes min: "s |= Enabled F"
wenzelm@21624
   196
    and maj: "|- F --> G"
wenzelm@21624
   197
  shows "s |= Enabled G"
wenzelm@21624
   198
  apply (rule min [THEN enabledE])
wenzelm@21624
   199
  apply (rule enabledI [action_use])
wenzelm@21624
   200
  apply (erule maj [action_use])
wenzelm@21624
   201
  done
wenzelm@21624
   202
wenzelm@21624
   203
(* stronger variant *)
wenzelm@21624
   204
lemma enabled_mono2:
wenzelm@21624
   205
  assumes min: "s |= Enabled F"
wenzelm@21624
   206
    and maj: "!!t. F (s,t) ==> G (s,t)"
wenzelm@21624
   207
  shows "s |= Enabled G"
wenzelm@21624
   208
  apply (rule min [THEN enabledE])
wenzelm@21624
   209
  apply (rule enabledI [action_use])
wenzelm@21624
   210
  apply (erule maj)
wenzelm@21624
   211
  done
wenzelm@21624
   212
wenzelm@21624
   213
lemma enabled_disj1: "|- Enabled F --> Enabled (F | G)"
wenzelm@21624
   214
  by (auto elim!: enabled_mono)
wenzelm@21624
   215
wenzelm@21624
   216
lemma enabled_disj2: "|- Enabled G --> Enabled (F | G)"
wenzelm@21624
   217
  by (auto elim!: enabled_mono)
wenzelm@21624
   218
wenzelm@21624
   219
lemma enabled_conj1: "|- Enabled (F & G) --> Enabled F"
wenzelm@21624
   220
  by (auto elim!: enabled_mono)
wenzelm@21624
   221
wenzelm@21624
   222
lemma enabled_conj2: "|- Enabled (F & G) --> Enabled G"
wenzelm@21624
   223
  by (auto elim!: enabled_mono)
wenzelm@21624
   224
wenzelm@21624
   225
lemma enabled_conjE:
wenzelm@21624
   226
    "[| s |= Enabled (F & G); [| s |= Enabled F; s |= Enabled G |] ==> Q |] ==> Q"
wenzelm@21624
   227
  apply (frule enabled_conj1 [action_use])
wenzelm@21624
   228
  apply (drule enabled_conj2 [action_use])
wenzelm@21624
   229
  apply simp
wenzelm@21624
   230
  done
wenzelm@21624
   231
wenzelm@21624
   232
lemma enabled_disjD: "|- Enabled (F | G) --> Enabled F | Enabled G"
wenzelm@21624
   233
  by (auto simp add: enabled_def)
wenzelm@21624
   234
wenzelm@21624
   235
lemma enabled_disj: "|- Enabled (F | G) = (Enabled F | Enabled G)"
wenzelm@21624
   236
  apply clarsimp
wenzelm@21624
   237
  apply (rule iffI)
wenzelm@21624
   238
   apply (erule enabled_disjD [action_use])
wenzelm@21624
   239
  apply (erule disjE enabled_disj1 [action_use] enabled_disj2 [action_use])+
wenzelm@21624
   240
  done
wenzelm@21624
   241
wenzelm@21624
   242
lemma enabled_ex: "|- Enabled (EX x. F x) = (EX x. Enabled (F x))"
wenzelm@21624
   243
  by (force simp add: enabled_def)
wenzelm@21624
   244
wenzelm@21624
   245
wenzelm@21624
   246
(* A rule that combines enabledI and baseE, but generates fewer instantiations *)
wenzelm@21624
   247
lemma base_enabled:
wenzelm@21624
   248
    "[| basevars vs; EX c. ! u. vs u = c --> A(s,u) |] ==> s |= Enabled A"
wenzelm@21624
   249
  apply (erule exE)
wenzelm@21624
   250
  apply (erule baseE)
wenzelm@21624
   251
  apply (rule enabledI [action_use])
wenzelm@21624
   252
  apply (erule allE)
wenzelm@21624
   253
  apply (erule mp)
wenzelm@21624
   254
  apply assumption
wenzelm@21624
   255
  done
wenzelm@21624
   256
wenzelm@21624
   257
(* ======================= action_simp_tac ============================== *)
wenzelm@21624
   258
wenzelm@21624
   259
ML {*
wenzelm@21624
   260
(* A dumb simplification-based tactic with just a little first-order logic:
wenzelm@21624
   261
   should plug in only "very safe" rules that can be applied blindly.
wenzelm@21624
   262
   Note that it applies whatever simplifications are currently active.
wenzelm@21624
   263
*)
wenzelm@54742
   264
fun action_simp_tac ctxt intros elims =
wenzelm@21624
   265
    asm_full_simp_tac
wenzelm@54742
   266
         (ctxt setloop (fn _ => (resolve_tac ((map (action_use ctxt) intros)
wenzelm@24180
   267
                                    @ [refl,impI,conjI,@{thm actionI},@{thm intI},allI]))
wenzelm@54742
   268
                      ORELSE' (eresolve_tac ((map (action_use ctxt) elims)
wenzelm@21624
   269
                                             @ [conjE,disjE,exE]))));
wenzelm@21624
   270
*}
wenzelm@21624
   271
wenzelm@21624
   272
(* ---------------- enabled_tac: tactic to prove (Enabled A) -------------------- *)
wenzelm@21624
   273
wenzelm@21624
   274
ML {*
wenzelm@21624
   275
(* "Enabled A" can be proven as follows:
wenzelm@21624
   276
   - Assume that we know which state variables are "base variables"
wenzelm@21624
   277
     this should be expressed by a theorem of the form "basevars (x,y,z,...)".
wenzelm@21624
   278
   - Resolve this theorem with baseE to introduce a constant for the value of the
wenzelm@21624
   279
     variables in the successor state, and resolve the goal with the result.
wenzelm@21624
   280
   - Resolve with enabledI and do some rewriting.
wenzelm@21624
   281
   - Solve for the unknowns using standard HOL reasoning.
wenzelm@21624
   282
   The following tactic combines these steps except the final one.
wenzelm@21624
   283
*)
wenzelm@21624
   284
wenzelm@42785
   285
fun enabled_tac ctxt base_vars =
wenzelm@42793
   286
  clarsimp_tac (ctxt addSIs [base_vars RS @{thm base_enabled}]);
wenzelm@21624
   287
*}
wenzelm@21624
   288
wenzelm@42785
   289
method_setup enabled = {*
wenzelm@42785
   290
  Attrib.thm >> (fn th => fn ctxt => SIMPLE_METHOD' (enabled_tac ctxt th))
wenzelm@42814
   291
*}
wenzelm@42785
   292
wenzelm@21624
   293
(* Example *)
wenzelm@21624
   294
wenzelm@21624
   295
lemma
wenzelm@21624
   296
  assumes "basevars (x,y,z)"
wenzelm@21624
   297
  shows "|- x --> Enabled ($x & (y$ = #False))"
wenzelm@42785
   298
  apply (enabled assms)
wenzelm@21624
   299
  apply auto
wenzelm@21624
   300
  done
wenzelm@21624
   301
wenzelm@21624
   302
end