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