src/HOL/TLA/Action.ML
author wenzelm
Wed Oct 08 11:50:33 1997 +0200 (1997-10-08)
changeset 3807 82a99b090d9d
child 3945 ae9c61d69888
permissions -rw-r--r--
A formalization of TLA in HOL -- by Stephan Merz;
wenzelm@3807
     1
(* 
wenzelm@3807
     2
    File:	 Action.ML
wenzelm@3807
     3
    Author:      Stephan Merz
wenzelm@3807
     4
    Copyright:   1997 University of Munich
wenzelm@3807
     5
wenzelm@3807
     6
Lemmas and tactics for TLA actions.
wenzelm@3807
     7
*)
wenzelm@3807
     8
wenzelm@3807
     9
val act_rews = [pairSF_def RS eq_reflection,unl_before,unl_after,unchanged_def,
wenzelm@3807
    10
                pr_con,pr_before,pr_lift,pr_lift2,pr_lift3,pr_all,pr_ex];
wenzelm@3807
    11
wenzelm@3807
    12
val action_rews = act_rews @ intensional_rews;
wenzelm@3807
    13
wenzelm@3807
    14
qed_goal "actionI" Action.thy "(!!s t. ([[s,t]] |= A)) ==> A"
wenzelm@3807
    15
  (fn [prem] => [REPEAT (resolve_tac [prem,intI,state2_ext] 1)]);
wenzelm@3807
    16
wenzelm@3807
    17
qed_goal "actionD" Action.thy "A ==> ([[s,t]] |= A)"
wenzelm@3807
    18
  (fn [prem] => [REPEAT (resolve_tac [prem,intD] 1)]);
wenzelm@3807
    19
wenzelm@3807
    20
wenzelm@3807
    21
wenzelm@3807
    22
(* ================ Functions to "unlift" action theorems into HOL rules ================ *)
wenzelm@3807
    23
wenzelm@3807
    24
(* Basic unlifting introduces a world parameter and applies basic rewrites, e.g.
wenzelm@3807
    25
   A .= B    gets   ([[s,t]] |= A) = ([[s,t]] |= B)
wenzelm@3807
    26
   A .-> B   gets   ([[s,t]] |= A) --> ([[s,t]] |= B)
wenzelm@3807
    27
*)
wenzelm@3807
    28
fun action_unlift th = rewrite_rule action_rews (th RS actionD);
wenzelm@3807
    29
wenzelm@3807
    30
(* A .-> B   becomes   A [[s,t]] ==> B [[s,t]] *)
wenzelm@3807
    31
fun action_mp th = zero_var_indexes ((action_unlift th) RS mp);
wenzelm@3807
    32
wenzelm@3807
    33
(* A .-> B   becomes   [| A[[s,t]]; B[[s,t]] ==> R |] ==> R 
wenzelm@3807
    34
   so that it can be used as an elimination rule
wenzelm@3807
    35
*)
wenzelm@3807
    36
fun action_impE th = zero_var_indexes ((action_unlift th) RS impE);
wenzelm@3807
    37
wenzelm@3807
    38
(* A .& B .-> C  becomes  [| A[[s,t]]; B[[s,t]] |] ==> C[[s,t]] *)
wenzelm@3807
    39
fun action_conjmp th = zero_var_indexes (conjI RS (action_mp th));
wenzelm@3807
    40
wenzelm@3807
    41
(* A .& B .-> C  becomes  [| A[[s,t]]; B[[s,t]]; (C[[s,t]] ==> R) |] ==> R *)
wenzelm@3807
    42
fun action_conjimpE th = zero_var_indexes (conjI RS (action_impE th));
wenzelm@3807
    43
wenzelm@3807
    44
(* Turn  A .= B  into meta-level rewrite rule  A == B *)
wenzelm@3807
    45
fun action_rewrite th = (rewrite_rule action_rews (th RS inteq_reflection));
wenzelm@3807
    46
wenzelm@3807
    47
(* ===================== Update simpset and classical prover ============================= *)
wenzelm@3807
    48
wenzelm@3807
    49
(* Make the simplifier use action_unlift rather than int_unlift 
wenzelm@3807
    50
   when action simplifications are added.
wenzelm@3807
    51
*)
wenzelm@3807
    52
fun maybe_unlift th =
wenzelm@3807
    53
    (case concl_of th of
wenzelm@3807
    54
         Const("TrueInt",_) $ p 
wenzelm@3807
    55
           => (action_unlift th
wenzelm@3807
    56
                  handle _ => int_unlift th)
wenzelm@3807
    57
       | _ => th);
wenzelm@3807
    58
wenzelm@3807
    59
simpset := !simpset setmksimps ((mksimps mksimps_pairs) o maybe_unlift);
wenzelm@3807
    60
wenzelm@3807
    61
(* make act_rews be always active -- intensional_rews has been added before *)
wenzelm@3807
    62
Addsimps act_rews;
wenzelm@3807
    63
wenzelm@3807
    64
use "cladata.ML";        (* local version! *)
wenzelm@3807
    65
wenzelm@3807
    66
(* ================================ action_simp_tac ================================== *)
wenzelm@3807
    67
wenzelm@3807
    68
(* A dumb simplification tactic with just a little first-order logic:
wenzelm@3807
    69
   should plug in only "very safe" rules that can be applied blindly.
wenzelm@3807
    70
   Note that it applies whatever simplifications are currently active.
wenzelm@3807
    71
*)
wenzelm@3807
    72
fun action_simp_tac ss intros elims i =
wenzelm@3807
    73
    (asm_full_simp_tac 
wenzelm@3807
    74
         (ss setloop ((resolve_tac (intros @ [refl,impI,conjI,actionI,allI]))
wenzelm@3807
    75
		      ORELSE' (eresolve_tac (elims @ [conjE,disjE,exE_prop]))))
wenzelm@3807
    76
         i);
wenzelm@3807
    77
(* default version without additional plug-in rules *)
wenzelm@3807
    78
fun Action_simp_tac i = (action_simp_tac (!simpset) [] [] i);
wenzelm@3807
    79
wenzelm@3807
    80
wenzelm@3807
    81
(* ==================== Simplification of abstractions ==================== *)
wenzelm@3807
    82
wenzelm@3807
    83
(* Somewhat obscure simplifications, rarely necessary to get rid
wenzelm@3807
    84
   of abstractions that may be introduced by higher-order unification.
wenzelm@3807
    85
*)
wenzelm@3807
    86
wenzelm@3807
    87
qed_goal "pr_con_abs" Action.thy "(%w. c)` .= #c"
wenzelm@3807
    88
  (fn _ => [rtac actionI 1,
wenzelm@3807
    89
            rewrite_goals_tac (con_abs::action_rews),
wenzelm@3807
    90
            rtac refl 1
wenzelm@3807
    91
           ]);
wenzelm@3807
    92
wenzelm@3807
    93
qed_goal "pr_lift_abs" Action.thy "(%w. f(x w))` .= f[x`]"
wenzelm@3807
    94
  (fn _ => [rtac actionI 1,
wenzelm@3807
    95
              (* give all rewrites to the engine and it loops! *)
wenzelm@3807
    96
            rewrite_goals_tac intensional_rews,
wenzelm@3807
    97
            rewtac lift_abs,
wenzelm@3807
    98
            rewtac pr_lift,
wenzelm@3807
    99
            rewtac unl_lift,
wenzelm@3807
   100
            rtac refl 1
wenzelm@3807
   101
           ]);
wenzelm@3807
   102
wenzelm@3807
   103
qed_goal "pr_lift2_abs" Action.thy "(%w. f(x w) (y w))` .= f[x`,y`]"
wenzelm@3807
   104
  (fn _ => [rtac actionI 1,
wenzelm@3807
   105
            rewrite_goals_tac intensional_rews,
wenzelm@3807
   106
            rewtac lift2_abs,
wenzelm@3807
   107
            rewtac pr_lift2,
wenzelm@3807
   108
            rewtac unl_lift2,
wenzelm@3807
   109
            rtac refl 1
wenzelm@3807
   110
           ]);
wenzelm@3807
   111
wenzelm@3807
   112
qed_goal "pr_lift2_abs_con1" Action.thy "(%w. f x (y w))` .= f[#x, y`]"
wenzelm@3807
   113
  (fn _ => [rtac actionI 1,
wenzelm@3807
   114
            rewrite_goals_tac intensional_rews,
wenzelm@3807
   115
            rewtac lift2_abs_con1,
wenzelm@3807
   116
            rewtac pr_lift2,
wenzelm@3807
   117
            rewtac unl_lift2,
wenzelm@3807
   118
            rewtac pr_con,
wenzelm@3807
   119
            rewtac unl_con,
wenzelm@3807
   120
            rtac refl 1
wenzelm@3807
   121
           ]);
wenzelm@3807
   122
wenzelm@3807
   123
qed_goal "pr_lift2_abs_con2" Action.thy "(%w. f (x w) y)` .= f[x`, #y]"
wenzelm@3807
   124
  (fn _ => [rtac actionI 1,
wenzelm@3807
   125
            rewrite_goals_tac intensional_rews,
wenzelm@3807
   126
            rewtac lift2_abs_con2,
wenzelm@3807
   127
            rewtac pr_lift2,
wenzelm@3807
   128
            rewtac unl_lift2,
wenzelm@3807
   129
            rewtac pr_con,
wenzelm@3807
   130
            rewtac unl_con,
wenzelm@3807
   131
            rtac refl 1
wenzelm@3807
   132
           ]);
wenzelm@3807
   133
wenzelm@3807
   134
qed_goal "pr_lift3_abs" Action.thy "(%w. f(x w) (y w) (z w))` .= f[x`,y`,z`]"
wenzelm@3807
   135
  (fn _ => [rtac actionI 1,
wenzelm@3807
   136
            rewrite_goals_tac intensional_rews,
wenzelm@3807
   137
            rewtac lift3_abs,
wenzelm@3807
   138
            rewtac pr_lift3,
wenzelm@3807
   139
            rewtac unl_lift3,
wenzelm@3807
   140
            rtac refl 1
wenzelm@3807
   141
           ]);
wenzelm@3807
   142
wenzelm@3807
   143
qed_goal "pr_lift3_abs_con1" Action.thy "(%w. f x (y w) (z w))` .= f[#x, y`, z`]"
wenzelm@3807
   144
  (fn _ => [rtac actionI 1,
wenzelm@3807
   145
            rewrite_goals_tac intensional_rews,
wenzelm@3807
   146
            rewtac lift3_abs_con1,
wenzelm@3807
   147
            rewtac pr_lift3,
wenzelm@3807
   148
            rewtac unl_lift3,
wenzelm@3807
   149
            rewtac pr_con,
wenzelm@3807
   150
            rewtac unl_con,
wenzelm@3807
   151
            rtac refl 1
wenzelm@3807
   152
           ]);
wenzelm@3807
   153
wenzelm@3807
   154
qed_goal "pr_lift3_abs_con2" Action.thy "(%w. f (x w) y (z w))` .= f[x`, #y, z`]"
wenzelm@3807
   155
  (fn _ => [rtac actionI 1,
wenzelm@3807
   156
            rewrite_goals_tac intensional_rews,
wenzelm@3807
   157
            rewtac lift3_abs_con2,
wenzelm@3807
   158
            rewtac pr_lift3,
wenzelm@3807
   159
            rewtac unl_lift3,
wenzelm@3807
   160
            rewtac pr_con,
wenzelm@3807
   161
            rewtac unl_con,
wenzelm@3807
   162
            rtac refl 1
wenzelm@3807
   163
           ]);
wenzelm@3807
   164
wenzelm@3807
   165
qed_goal "pr_lift3_abs_con3" Action.thy "(%w. f (x w) (y w) z)` .= f[x`, y`, #z]"
wenzelm@3807
   166
  (fn _ => [rtac actionI 1,
wenzelm@3807
   167
            rewrite_goals_tac intensional_rews,
wenzelm@3807
   168
            rewtac lift3_abs_con3,
wenzelm@3807
   169
            rewtac pr_lift3,
wenzelm@3807
   170
            rewtac unl_lift3,
wenzelm@3807
   171
            rewtac pr_con,
wenzelm@3807
   172
            rewtac unl_con,
wenzelm@3807
   173
            rtac refl 1
wenzelm@3807
   174
           ]);
wenzelm@3807
   175
wenzelm@3807
   176
qed_goal "pr_lift3_abs_con12" Action.thy "(%w. f x y (z w))` .= f[#x, #y, z`]"
wenzelm@3807
   177
  (fn _ => [rtac actionI 1,
wenzelm@3807
   178
            rewrite_goals_tac intensional_rews,
wenzelm@3807
   179
            rewtac lift3_abs_con12,
wenzelm@3807
   180
            rewtac pr_lift3,
wenzelm@3807
   181
            rewtac unl_lift3,
wenzelm@3807
   182
            rewtac pr_con,
wenzelm@3807
   183
            rewtac unl_con,
wenzelm@3807
   184
            rtac refl 1
wenzelm@3807
   185
           ]);
wenzelm@3807
   186
wenzelm@3807
   187
qed_goal "pr_lift3_abs_con13" Action.thy "(%w. f x (y w) z)` .= f[#x, y`, #z]"
wenzelm@3807
   188
  (fn _ => [rtac actionI 1,
wenzelm@3807
   189
            rewrite_goals_tac intensional_rews,
wenzelm@3807
   190
            rewtac lift3_abs_con13,
wenzelm@3807
   191
            rewtac pr_lift3,
wenzelm@3807
   192
            rewtac unl_lift3,
wenzelm@3807
   193
            rewtac pr_con,
wenzelm@3807
   194
            rewtac unl_con,
wenzelm@3807
   195
            rtac refl 1
wenzelm@3807
   196
           ]);
wenzelm@3807
   197
wenzelm@3807
   198
qed_goal "pr_lift3_abs_con23" Action.thy "(%w. f (x w) y z)` .= f[x`, #y, #z]"
wenzelm@3807
   199
  (fn _ => [rtac actionI 1,
wenzelm@3807
   200
            rewrite_goals_tac intensional_rews,
wenzelm@3807
   201
            rewtac lift3_abs_con23,
wenzelm@3807
   202
            rewtac pr_lift3,
wenzelm@3807
   203
            rewtac unl_lift3,
wenzelm@3807
   204
            rewtac pr_con,
wenzelm@3807
   205
            rewtac unl_con,
wenzelm@3807
   206
            rtac refl 1
wenzelm@3807
   207
           ]);
wenzelm@3807
   208
wenzelm@3807
   209
(* We don't add these as default rewrite rules, because they are
wenzelm@3807
   210
   rarely needed and may slow down automatic proofs.
wenzelm@3807
   211
*)
wenzelm@3807
   212
val pr_abs_rews = map (fn th => th RS inteq_reflection) 
wenzelm@3807
   213
                      [pr_con_abs,
wenzelm@3807
   214
                       pr_lift_abs,pr_lift2_abs,pr_lift2_abs_con1,pr_lift2_abs_con2,
wenzelm@3807
   215
                       pr_lift3_abs,pr_lift3_abs_con1,pr_lift3_abs_con2,pr_lift3_abs_con3,
wenzelm@3807
   216
                       pr_lift3_abs_con12,pr_lift3_abs_con13,pr_lift3_abs_con23];
wenzelm@3807
   217
wenzelm@3807
   218
(* =========================== square / angle brackets =========================== *)
wenzelm@3807
   219
wenzelm@3807
   220
qed_goalw "idle_squareI" Action.thy [square_def]
wenzelm@3807
   221
   "!!s t. ([[s,t]] |= unchanged v) ==> ([[s,t]] |= [A]_v)"
wenzelm@3807
   222
   (fn _ => [ Auto_tac() ]);
wenzelm@3807
   223
wenzelm@3807
   224
qed_goalw "busy_squareI" Action.thy [square_def]
wenzelm@3807
   225
   "!!s t. ([[s,t]] |= A) ==> ([[s,t]] |= [A]_v)"
wenzelm@3807
   226
   (fn _ => [ Auto_tac() ]);
wenzelm@3807
   227
wenzelm@3807
   228
qed_goalw "square_simulation" Action.thy [square_def]
wenzelm@3807
   229
   "[| unchanged f .& .~B .-> unchanged g;   \
wenzelm@3807
   230
\      A .& .~unchanged g .-> B              \
wenzelm@3807
   231
\   |] ==> [A]_f .-> [B]_g"
wenzelm@3807
   232
   (fn [p1,p2] => [Auto_tac(),
wenzelm@3807
   233
                   etac (action_conjimpE p2) 1,
wenzelm@3807
   234
                   etac swap 3, etac (action_conjimpE p1) 3,
wenzelm@3807
   235
                   ALLGOALS atac
wenzelm@3807
   236
                  ]);
wenzelm@3807
   237
                   
wenzelm@3807
   238
qed_goalw "not_square" Action.thy [square_def,angle_def]
wenzelm@3807
   239
   "(.~ [A]_v) .= <.~A>_v"
wenzelm@3807
   240
   (fn _ => [ Auto_tac() ]);
wenzelm@3807
   241
wenzelm@3807
   242
qed_goalw "not_angle" Action.thy [square_def,angle_def]
wenzelm@3807
   243
   "(.~ <A>_v) .= [.~A]_v"
wenzelm@3807
   244
   (fn _ => [ Auto_tac() ]);
wenzelm@3807
   245
wenzelm@3807
   246
(* ============================== Facts about ENABLED ============================== *)
wenzelm@3807
   247
wenzelm@3807
   248
qed_goalw "enabledI" Action.thy [enabled_def]
wenzelm@3807
   249
  "A [[s,t]] ==> (Enabled A) s"
wenzelm@3807
   250
  (fn prems => [ REPEAT (resolve_tac (exI::prems) 1) ]);
wenzelm@3807
   251
wenzelm@3807
   252
qed_goalw "enabledE" Action.thy [enabled_def]
wenzelm@3807
   253
  "[| (Enabled A) s; !!u. A[[s,u]] ==> PROP R |] ==> PROP R"
wenzelm@3807
   254
  (fn prems => [cut_facts_tac prems 1,
wenzelm@3807
   255
                etac exE_prop 1,
wenzelm@3807
   256
                resolve_tac prems 1, atac 1
wenzelm@3807
   257
               ]);
wenzelm@3807
   258
wenzelm@3807
   259
qed_goal "notEnabledD" Action.thy
wenzelm@3807
   260
  "!!G. ~ (Enabled G s) ==> ~ G [[s,t]]"
wenzelm@3807
   261
  (fn _ => [ auto_tac (action_css addsimps2 [enabled_def]) ]);
wenzelm@3807
   262
wenzelm@3807
   263
(* Monotonicity *)
wenzelm@3807
   264
qed_goal "enabled_mono" Action.thy
wenzelm@3807
   265
  "[| (Enabled F) s; F .-> G |] ==> (Enabled G) s"
wenzelm@3807
   266
  (fn [min,maj] => [rtac (min RS enabledE) 1,
wenzelm@3807
   267
                    rtac enabledI 1,
wenzelm@3807
   268
                    etac (action_mp maj) 1
wenzelm@3807
   269
                   ]);
wenzelm@3807
   270
wenzelm@3807
   271
(* stronger variant *)
wenzelm@3807
   272
qed_goal "enabled_mono2" Action.thy
wenzelm@3807
   273
   "[| (Enabled F) s; !!t. (F [[s,t]] ==> G[[s,t]] ) |] ==> (Enabled G) s"
wenzelm@3807
   274
   (fn [min,maj] => [rtac (min RS enabledE) 1,
wenzelm@3807
   275
		     rtac enabledI 1,
wenzelm@3807
   276
		     etac maj 1
wenzelm@3807
   277
		    ]);
wenzelm@3807
   278
wenzelm@3807
   279
qed_goal "enabled_disj1" Action.thy
wenzelm@3807
   280
  "!!s. (Enabled F) s ==> (Enabled (F .| G)) s"
wenzelm@3807
   281
  (fn _ => [etac enabled_mono 1, Auto_tac()
wenzelm@3807
   282
	   ]);
wenzelm@3807
   283
wenzelm@3807
   284
qed_goal "enabled_disj2" Action.thy
wenzelm@3807
   285
  "!!s. (Enabled G) s ==> (Enabled (F .| G)) s"
wenzelm@3807
   286
  (fn _ => [etac enabled_mono 1, Auto_tac()
wenzelm@3807
   287
	   ]);
wenzelm@3807
   288
wenzelm@3807
   289
qed_goal "enabled_conj1" Action.thy
wenzelm@3807
   290
  "!!s. (Enabled (F .& G)) s ==> (Enabled F) s"
wenzelm@3807
   291
  (fn _ => [etac enabled_mono 1, Auto_tac()
wenzelm@3807
   292
           ]);
wenzelm@3807
   293
wenzelm@3807
   294
qed_goal "enabled_conj2" Action.thy
wenzelm@3807
   295
  "!!s. (Enabled (F .& G)) s ==> (Enabled G) s"
wenzelm@3807
   296
  (fn _ => [etac enabled_mono 1, Auto_tac()
wenzelm@3807
   297
           ]);
wenzelm@3807
   298
wenzelm@3807
   299
qed_goal "enabled_conjE" Action.thy
wenzelm@3807
   300
  "[| (Enabled (F .& G)) s; [| (Enabled F) s; (Enabled G) s |] ==> PROP R |] ==> PROP R"
wenzelm@3807
   301
  (fn prems => [cut_facts_tac prems 1, resolve_tac prems 1,
wenzelm@3807
   302
                etac enabled_conj1 1, etac enabled_conj2 1]);
wenzelm@3807
   303
wenzelm@3807
   304
qed_goal "enabled_disjD" Action.thy
wenzelm@3807
   305
  "!!s. (Enabled (F .| G)) s ==> ((Enabled F) s) | ((Enabled G) s)"
wenzelm@3807
   306
  (fn _ => [etac enabledE 1,
wenzelm@3807
   307
            auto_tac (action_css addSDs2 [notEnabledD] addSEs2 [enabledI])
wenzelm@3807
   308
           ]);
wenzelm@3807
   309
wenzelm@3807
   310
qed_goal "enabled_disj" Action.thy
wenzelm@3807
   311
  "(Enabled (F .| G)) s = ( (Enabled F) s | (Enabled G) s )"
wenzelm@3807
   312
  (fn _ => [rtac iffI 1,
wenzelm@3807
   313
            etac enabled_disjD 1,
wenzelm@3807
   314
            REPEAT (eresolve_tac [disjE,enabled_disj1,enabled_disj2] 1)
wenzelm@3807
   315
           ]);
wenzelm@3807
   316
wenzelm@3807
   317
qed_goal "enabled_ex" Action.thy
wenzelm@3807
   318
  "(Enabled (REX x. F x)) s = (EX x. (Enabled (F x)) s)"
wenzelm@3807
   319
  (fn _ => [ auto_tac (action_css addsimps2 [enabled_def]) ]);
wenzelm@3807
   320
	    
wenzelm@3807
   321
wenzelm@3807
   322
(* A rule that combines enabledI and baseE, but generates fewer possible instantiations *)
wenzelm@3807
   323
qed_goal "base_enabled" Action.thy
wenzelm@3807
   324
  "[| base_var(v); !!u. v u = c s ==> A [[s,u]] |] ==> Enabled A s"
wenzelm@3807
   325
  (fn prems => [cut_facts_tac prems 1,
wenzelm@3807
   326
		etac baseE 1, rtac enabledI 1,
wenzelm@3807
   327
		REPEAT (ares_tac prems 1)]);
wenzelm@3807
   328
wenzelm@3807
   329
wenzelm@3807
   330
(* ---------------- enabled_tac: tactic to prove (Enabled A) -------------------- *)
wenzelm@3807
   331
(* "Enabled A" can be proven as follows:
wenzelm@3807
   332
   - Assume that we know which state variables are "base variables";
wenzelm@3807
   333
     this should be expressed by a theorem of the form "base_var <x,y,z,...>".
wenzelm@3807
   334
   - Resolve this theorem with baseE to introduce a constant for the value of the
wenzelm@3807
   335
     variables in the successor state, and resolve the goal with the result.
wenzelm@3807
   336
   - E-resolve with PairVarE so that we have one constant per variable.
wenzelm@3807
   337
   - Resolve with enabledI and do some rewriting.
wenzelm@3807
   338
   - Solve for the unknowns using standard HOL reasoning.
wenzelm@3807
   339
   The following tactic combines these steps except the final one.
wenzelm@3807
   340
*)
wenzelm@3807
   341
wenzelm@3807
   342
fun enabled_tac base_vars i =
wenzelm@3807
   343
    EVERY [(* apply actionI (plus rewriting) if the goal is of the form $(Enabled A),
wenzelm@3807
   344
	      do nothing if it is of the form (Enabled A) s *)
wenzelm@3807
   345
	   TRY ((rtac actionI i) THEN (SELECT_GOAL (rewrite_goals_tac action_rews) i)),
wenzelm@3807
   346
	   rtac (base_vars RS base_enabled) i,
wenzelm@3807
   347
	   REPEAT_DETERM (etac PairVarE i),
wenzelm@3807
   348
	   (SELECT_GOAL (rewrite_goals_tac action_rews) i)
wenzelm@3807
   349
	  ];
wenzelm@3807
   350
wenzelm@3807
   351
(* Example of use:
wenzelm@3807
   352
wenzelm@3807
   353
val [prem] = goal Action.thy "base_var <x,y,z> ==> $x .-> $Enabled ($x .& (y$ .= #False))";
wenzelm@3807
   354
by (REPEAT ((CHANGED (Action_simp_tac 1)) ORELSE (enabled_tac prem 1)));
wenzelm@3807
   355
wenzelm@3807
   356
*)