src/FOL/simpdata.ML
author paulson
Wed Dec 03 10:48:16 1997 +0100 (1997-12-03)
changeset 4349 50403e5a44c0
parent 4325 e72cba5af6c5
child 4477 b3e5857d8d99
permissions -rw-r--r--
Instantiated the one-point-rule quantifier simpprocs for FOL

New file fologic.ML holds abstract syntax operations

Also, miniscoping provided for intuitionistic logic
clasohm@1459
     1
(*  Title:      FOL/simpdata
clasohm@0
     2
    ID:         $Id$
clasohm@1459
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@282
     4
    Copyright   1994  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Simplification data for FOL
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
(*** Rewrite rules ***)
clasohm@0
    10
clasohm@0
    11
fun int_prove_fun s = 
lcp@282
    12
 (writeln s;  
lcp@282
    13
  prove_goal IFOL.thy s
lcp@282
    14
   (fn prems => [ (cut_facts_tac prems 1), 
paulson@2601
    15
                  (IntPr.fast_tac 1) ]));
clasohm@0
    16
paulson@1953
    17
val conj_simps = map int_prove_fun
clasohm@1459
    18
 ["P & True <-> P",      "True & P <-> P",
clasohm@0
    19
  "P & False <-> False", "False & P <-> False",
nipkow@2801
    20
  "P & P <-> P", "P & P & Q <-> P & Q",
clasohm@1459
    21
  "P & ~P <-> False",    "~P & P <-> False",
clasohm@0
    22
  "(P & Q) & R <-> P & (Q & R)"];
clasohm@0
    23
paulson@1953
    24
val disj_simps = map int_prove_fun
clasohm@1459
    25
 ["P | True <-> True",  "True | P <-> True",
clasohm@1459
    26
  "P | False <-> P",    "False | P <-> P",
nipkow@2801
    27
  "P | P <-> P", "P | P | Q <-> P | Q",
clasohm@0
    28
  "(P | Q) | R <-> P | (Q | R)"];
clasohm@0
    29
paulson@1953
    30
val not_simps = map int_prove_fun
lcp@282
    31
 ["~(P|Q)  <-> ~P & ~Q",
clasohm@1459
    32
  "~ False <-> True",   "~ True <-> False"];
clasohm@0
    33
paulson@1953
    34
val imp_simps = map int_prove_fun
clasohm@1459
    35
 ["(P --> False) <-> ~P",       "(P --> True) <-> True",
clasohm@1459
    36
  "(False --> P) <-> True",     "(True --> P) <-> P", 
clasohm@1459
    37
  "(P --> P) <-> True",         "(P --> ~P) <-> ~P"];
clasohm@0
    38
paulson@1953
    39
val iff_simps = map int_prove_fun
clasohm@1459
    40
 ["(True <-> P) <-> P",         "(P <-> True) <-> P",
clasohm@0
    41
  "(P <-> P) <-> True",
clasohm@1459
    42
  "(False <-> P) <-> ~P",       "(P <-> False) <-> ~P"];
clasohm@0
    43
paulson@4349
    44
(*The x=t versions are needed for the simplification procedures*)
paulson@1953
    45
val quant_simps = map int_prove_fun
paulson@4349
    46
 ["(ALL x. P) <-> P",   
paulson@4349
    47
  "(ALL x. x=t --> P(x)) <-> P(t)",
paulson@4349
    48
  "(ALL x. t=x --> P(x)) <-> P(t)",
paulson@4349
    49
  "(EX x. P) <-> P",
paulson@4349
    50
  "(EX x. x=t & P(x)) <-> P(t)", 
paulson@4349
    51
  "(EX x. t=x & P(x)) <-> P(t)"];
clasohm@0
    52
clasohm@0
    53
(*These are NOT supplied by default!*)
paulson@1953
    54
val distrib_simps  = map int_prove_fun
lcp@282
    55
 ["P & (Q | R) <-> P&Q | P&R", 
lcp@282
    56
  "(Q | R) & P <-> Q&P | R&P",
clasohm@0
    57
  "(P | Q --> R) <-> (P --> R) & (Q --> R)"];
clasohm@0
    58
lcp@282
    59
(** Conversion into rewrite rules **)
clasohm@0
    60
nipkow@53
    61
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
nipkow@53
    62
lcp@282
    63
(*Make atomic rewrite rules*)
lcp@429
    64
fun atomize r =
lcp@429
    65
  case concl_of r of
lcp@429
    66
    Const("Trueprop",_) $ p =>
lcp@429
    67
      (case p of
clasohm@1459
    68
         Const("op -->",_)$_$_ => atomize(r RS mp)
lcp@429
    69
       | Const("op &",_)$_$_   => atomize(r RS conjunct1) @
clasohm@1459
    70
                                  atomize(r RS conjunct2)
lcp@429
    71
       | Const("All",_)$_      => atomize(r RS spec)
clasohm@1459
    72
       | Const("True",_)       => []    (*True is DELETED*)
clasohm@1459
    73
       | Const("False",_)      => []    (*should False do something?*)
lcp@429
    74
       | _                     => [r])
lcp@429
    75
  | _ => [r];
lcp@429
    76
lcp@282
    77
lcp@282
    78
val P_iff_F = int_prove_fun "~P ==> (P <-> False)";
lcp@282
    79
val iff_reflection_F = P_iff_F RS iff_reflection;
lcp@282
    80
lcp@282
    81
val P_iff_T = int_prove_fun "P ==> (P <-> True)";
lcp@282
    82
val iff_reflection_T = P_iff_T RS iff_reflection;
lcp@282
    83
lcp@282
    84
(*Make meta-equalities.  The operator below is Trueprop*)
lcp@282
    85
fun mk_meta_eq th = case concl_of th of
nipkow@394
    86
    Const("==",_)$_$_           => th
nipkow@394
    87
  | _ $ (Const("op =",_)$_$_)   => th RS eq_reflection
lcp@282
    88
  | _ $ (Const("op <->",_)$_$_) => th RS iff_reflection
lcp@282
    89
  | _ $ (Const("Not",_)$_)      => th RS iff_reflection_F
lcp@282
    90
  | _                           => th RS iff_reflection_T;
clasohm@0
    91
lcp@981
    92
paulson@2074
    93
(*** Classical laws ***)
lcp@282
    94
clasohm@0
    95
fun prove_fun s = 
lcp@282
    96
 (writeln s;  
lcp@282
    97
  prove_goal FOL.thy s
lcp@282
    98
   (fn prems => [ (cut_facts_tac prems 1), 
clasohm@1459
    99
                  (Cla.fast_tac FOL_cs 1) ]));
lcp@745
   100
paulson@1953
   101
(*Avoids duplication of subgoals after expand_if, when the true and false 
paulson@1953
   102
  cases boil down to the same thing.*) 
paulson@1953
   103
val cases_simp = prove_fun "(P --> Q) & (~P --> Q) <-> Q";
paulson@1953
   104
paulson@4349
   105
paulson@4349
   106
(*** Miniscoping: pushing quantifiers in
paulson@4349
   107
     We do NOT distribute of ALL over &, or dually that of EX over |
paulson@4349
   108
     Baaz and Leitsch, On Skolemization and Proof Complexity (1994) 
paulson@4349
   109
     show that this step can increase proof length!
paulson@4349
   110
***)
paulson@4349
   111
paulson@4349
   112
(*existential miniscoping*)
paulson@4349
   113
val int_ex_simps = map int_prove_fun 
paulson@4349
   114
		     ["(EX x. P(x) & Q) <-> (EX x. P(x)) & Q",
paulson@4349
   115
		      "(EX x. P & Q(x)) <-> P & (EX x. Q(x))",
paulson@4349
   116
		      "(EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
paulson@4349
   117
		      "(EX x. P | Q(x)) <-> P | (EX x. Q(x))"];
paulson@4349
   118
paulson@4349
   119
(*classical rules*)
paulson@4349
   120
val cla_ex_simps = map prove_fun 
paulson@4349
   121
                     ["(EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q",
paulson@4349
   122
		      "(EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"];
clasohm@0
   123
paulson@4349
   124
val ex_simps = int_ex_simps @ cla_ex_simps;
paulson@4349
   125
paulson@4349
   126
(*universal miniscoping*)
paulson@4349
   127
val int_all_simps = map int_prove_fun
paulson@4349
   128
		      ["(ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q",
paulson@4349
   129
		       "(ALL x. P & Q(x)) <-> P & (ALL x. Q(x))",
paulson@4349
   130
		       "(ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q",
paulson@4349
   131
		       "(ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"];
paulson@1953
   132
paulson@4349
   133
(*classical rules*)
paulson@4349
   134
val cla_all_simps = map prove_fun
paulson@4349
   135
                      ["(ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q",
paulson@4349
   136
		       "(ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"];
paulson@4349
   137
paulson@4349
   138
val all_simps = int_all_simps @ cla_all_simps;
paulson@4349
   139
paulson@4349
   140
paulson@4349
   141
(*** Named rewrite rules proved for IFOL ***)
paulson@1953
   142
paulson@1914
   143
fun int_prove nm thm  = qed_goal nm IFOL.thy thm
paulson@1914
   144
    (fn prems => [ (cut_facts_tac prems 1), 
paulson@2601
   145
                   (IntPr.fast_tac 1) ]);
paulson@1914
   146
paulson@3910
   147
fun prove nm thm  = qed_goal nm FOL.thy thm (fn _ => [Blast_tac 1]);
paulson@1914
   148
paulson@1914
   149
int_prove "conj_commute" "P&Q <-> Q&P";
paulson@1914
   150
int_prove "conj_left_commute" "P&(Q&R) <-> Q&(P&R)";
paulson@1914
   151
val conj_comms = [conj_commute, conj_left_commute];
paulson@1914
   152
paulson@1914
   153
int_prove "disj_commute" "P|Q <-> Q|P";
paulson@1914
   154
int_prove "disj_left_commute" "P|(Q|R) <-> Q|(P|R)";
paulson@1914
   155
val disj_comms = [disj_commute, disj_left_commute];
paulson@1914
   156
paulson@1914
   157
int_prove "conj_disj_distribL" "P&(Q|R) <-> (P&Q | P&R)";
paulson@1914
   158
int_prove "conj_disj_distribR" "(P|Q)&R <-> (P&R | Q&R)";
paulson@1914
   159
paulson@1914
   160
int_prove "disj_conj_distribL" "P|(Q&R) <-> (P|Q) & (P|R)";
paulson@1914
   161
int_prove "disj_conj_distribR" "(P&Q)|R <-> (P|R) & (Q|R)";
paulson@1914
   162
paulson@1914
   163
int_prove "imp_conj_distrib" "(P --> (Q&R)) <-> (P-->Q) & (P-->R)";
paulson@1914
   164
int_prove "imp_conj"         "((P&Q)-->R)   <-> (P --> (Q --> R))";
paulson@1914
   165
int_prove "imp_disj"         "(P|Q --> R)   <-> (P-->R) & (Q-->R)";
paulson@1914
   166
paulson@3910
   167
prove "imp_disj1" "(P-->Q) | R <-> (P-->Q | R)";
paulson@3910
   168
prove "imp_disj2" "Q | (P-->R) <-> (P-->Q | R)";
paulson@3910
   169
paulson@1914
   170
int_prove "de_Morgan_disj" "(~(P | Q)) <-> (~P & ~Q)";
paulson@1914
   171
prove     "de_Morgan_conj" "(~(P & Q)) <-> (~P | ~Q)";
paulson@1914
   172
paulson@1914
   173
prove     "not_iff" "~(P <-> Q) <-> (P <-> ~Q)";
paulson@1914
   174
wenzelm@3835
   175
prove     "not_all" "(~ (ALL x. P(x))) <-> (EX x.~P(x))";
wenzelm@3835
   176
prove     "imp_all" "((ALL x. P(x)) --> Q) <-> (EX x. P(x) --> Q)";
wenzelm@3835
   177
int_prove "not_ex"  "(~ (EX x. P(x))) <-> (ALL x.~P(x))";
paulson@1914
   178
int_prove "imp_ex" "((EX x. P(x)) --> Q) <-> (ALL x. P(x) --> Q)";
paulson@1914
   179
paulson@1914
   180
int_prove "ex_disj_distrib"
paulson@1914
   181
    "(EX x. P(x) | Q(x)) <-> ((EX x. P(x)) | (EX x. Q(x)))";
paulson@1914
   182
int_prove "all_conj_distrib"
paulson@1914
   183
    "(ALL x. P(x) & Q(x)) <-> ((ALL x. P(x)) & (ALL x. Q(x)))";
paulson@1914
   184
paulson@1914
   185
lcp@1088
   186
(*Used in ZF, perhaps elsewhere?*)
lcp@1088
   187
val meta_eq_to_obj_eq = prove_goal IFOL.thy "x==y ==> x=y"
lcp@1088
   188
  (fn [prem] => [rewtac prem, rtac refl 1]);
lcp@1088
   189
paulson@4349
   190
paulson@4349
   191
open Simplifier;
paulson@4349
   192
paulson@4349
   193
(** make simplification procedures for quantifier elimination **)
paulson@4349
   194
structure Quantifier1 = Quantifier1Fun(
paulson@4349
   195
struct
paulson@4349
   196
  (*abstract syntax*)
paulson@4349
   197
  fun dest_eq((c as Const("op =",_)) $ s $ t) = Some(c,s,t)
paulson@4349
   198
    | dest_eq _ = None;
paulson@4349
   199
  fun dest_conj((c as Const("op &",_)) $ s $ t) = Some(c,s,t)
paulson@4349
   200
    | dest_conj _ = None;
paulson@4349
   201
  val conj = FOLogic.conj
paulson@4349
   202
  val imp  = FOLogic.imp
paulson@4349
   203
  (*rules*)
paulson@4349
   204
  val iff_reflection = iff_reflection
paulson@4349
   205
  val iffI = iffI
paulson@4349
   206
  val sym  = sym
paulson@4349
   207
  val conjI= conjI
paulson@4349
   208
  val conjE= conjE
paulson@4349
   209
  val impI = impI
paulson@4349
   210
  val impE = impE
paulson@4349
   211
  val mp   = mp
paulson@4349
   212
  val exI  = exI
paulson@4349
   213
  val exE  = exE
paulson@4349
   214
  val allI = allI
paulson@4349
   215
  val allE = allE
paulson@4349
   216
end);
paulson@4349
   217
paulson@4349
   218
local
paulson@4349
   219
val ex_pattern =
paulson@4349
   220
  read_cterm (sign_of FOL.thy) ("EX x. P(x) & Q(x)", FOLogic.oT)
paulson@4349
   221
paulson@4349
   222
val all_pattern =
paulson@4349
   223
  read_cterm (sign_of FOL.thy) ("ALL x. P(x) & P'(x) --> Q(x)", FOLogic.oT)
paulson@4349
   224
paulson@4349
   225
in
paulson@4349
   226
val defEX_regroup =
paulson@4349
   227
  mk_simproc "defined EX" [ex_pattern] Quantifier1.rearrange_ex;
paulson@4349
   228
val defALL_regroup =
paulson@4349
   229
  mk_simproc "defined ALL" [all_pattern] Quantifier1.rearrange_all;
paulson@4349
   230
end;
paulson@4349
   231
paulson@4349
   232
paulson@4349
   233
(*** Case splitting ***)
clasohm@0
   234
lcp@1088
   235
qed_goal "meta_iffD" IFOL.thy "[| P==Q; Q |] ==> P"
clasohm@756
   236
        (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]);
lcp@282
   237
nipkow@942
   238
local val mktac = mk_case_split_tac meta_iffD
nipkow@942
   239
in
nipkow@942
   240
fun split_tac splits = mktac (map mk_meta_eq splits)
nipkow@942
   241
end;
berghofe@1722
   242
berghofe@1722
   243
local val mktac = mk_case_split_inside_tac meta_iffD
berghofe@1722
   244
in
berghofe@1722
   245
fun split_inside_tac splits = mktac (map mk_meta_eq splits)
berghofe@1722
   246
end;
berghofe@1722
   247
oheimb@4203
   248
val split_asm_tac = mk_case_split_asm_tac split_tac 
oheimb@4203
   249
			(disjE,conjE,exE,contrapos,contrapos2,notnotD);
berghofe@1722
   250
paulson@4325
   251
paulson@4325
   252
paulson@2074
   253
(*** Standard simpsets ***)
paulson@2074
   254
paulson@2074
   255
structure Induction = InductionFun(struct val spec=IFOL.spec end);
paulson@2074
   256
paulson@4349
   257
open Induction;
paulson@2074
   258
paulson@2074
   259
(*Add congruence rules for = or <-> (instead of ==) *)
oheimb@2633
   260
infix 4 addcongs delcongs;
paulson@2074
   261
fun ss addcongs congs =
wenzelm@3566
   262
        ss addeqcongs (map standard (congs RL [eq_reflection,iff_reflection]));
oheimb@2633
   263
fun ss delcongs congs =
wenzelm@3566
   264
        ss deleqcongs (map standard (congs RL [eq_reflection,iff_reflection]));
paulson@2469
   265
wenzelm@4094
   266
fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
wenzelm@4094
   267
fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
paulson@2074
   268
paulson@4325
   269
infix 4 addsplits;
paulson@4325
   270
fun ss addsplits splits = ss addloop (split_tac splits);
paulson@4325
   271
paulson@2074
   272
val IFOL_simps =
paulson@2074
   273
   [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
paulson@2074
   274
    imp_simps @ iff_simps @ quant_simps;
paulson@2074
   275
paulson@2074
   276
val notFalseI = int_prove_fun "~False";
paulson@2074
   277
val triv_rls = [TrueI,refl,iff_refl,notFalseI];
paulson@2074
   278
oheimb@2633
   279
fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems),
oheimb@2633
   280
				 atac, etac FalseE];
oheimb@2633
   281
(*No premature instantiation of variables during simplification*)
oheimb@2633
   282
fun   safe_solver prems = FIRST'[match_tac (triv_rls@prems),
oheimb@2633
   283
				 eq_assume_tac, ematch_tac [FalseE]];
oheimb@2633
   284
paulson@3910
   285
(*No simprules, but basic infastructure for simplification*)
oheimb@2633
   286
val FOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
paulson@4349
   287
                            addsimprocs [defALL_regroup,defEX_regroup]
oheimb@2633
   288
			    setSSolver   safe_solver
oheimb@2633
   289
			    setSolver  unsafe_solver
oheimb@2633
   290
			    setmksimps (map mk_meta_eq o atomize o gen_all);
oheimb@2633
   291
paulson@3910
   292
(*intuitionistic simprules only*)
paulson@4349
   293
val IFOL_ss = FOL_basic_ss addsimps (IFOL_simps @ int_ex_simps @ int_all_simps)
oheimb@2633
   294
			   addcongs [imp_cong];
paulson@2074
   295
paulson@2074
   296
val cla_simps = 
paulson@3910
   297
    [de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2,
paulson@3910
   298
     not_all, not_ex, cases_simp] @
paulson@2074
   299
    map prove_fun
paulson@2074
   300
     ["~(P&Q)  <-> ~P | ~Q",
paulson@2074
   301
      "P | ~P",             "~P | P",
paulson@2074
   302
      "~ ~ P <-> P",        "(~P --> P) <-> P",
paulson@2074
   303
      "(~P <-> ~Q) <-> (P<->Q)"];
paulson@2074
   304
paulson@3910
   305
(*classical simprules too*)
paulson@4349
   306
val FOL_ss = IFOL_ss addsimps (cla_simps @ cla_ex_simps @ cla_all_simps);
paulson@2074
   307
wenzelm@4094
   308
simpset_ref() := FOL_ss;
oheimb@2633
   309
oheimb@2633
   310
oheimb@2633
   311
oheimb@2633
   312
(*** Integration of simplifier with classical reasoner ***)
oheimb@2633
   313
oheimb@2633
   314
(* rot_eq_tac rotates the first equality premise of subgoal i to the front,
oheimb@2633
   315
   fails if there is no equaliy or if an equality is already at the front *)
paulson@3537
   316
local
oheimb@2633
   317
  fun is_eq (Const ("Trueprop", _) $ (Const("op ="  ,_) $ _ $ _)) = true
paulson@3537
   318
    | is_eq (Const ("Trueprop", _) $ (Const("op <->",_) $ _ $ _)) = true
paulson@3537
   319
    | is_eq _ = false;
oheimb@4188
   320
  val find_eq = find_index is_eq;
paulson@3537
   321
in
paulson@3537
   322
val rot_eq_tac = 
oheimb@4188
   323
     SUBGOAL (fn (Bi,i) => let val n = find_eq (Logic.strip_assums_hyp Bi) in
oheimb@4188
   324
		if n>0 then rotate_tac n i else no_tac end)
paulson@3537
   325
end;
oheimb@2633
   326
oheimb@2633
   327
oheimb@2633
   328
fun safe_asm_more_full_simp_tac ss = TRY o rot_eq_tac THEN' 
oheimb@2633
   329
				     safe_asm_full_simp_tac ss;
oheimb@2633
   330
(*an unsatisfactory fix for the incomplete asm_full_simp_tac!
oheimb@2633
   331
  better: asm_really_full_simp_tac, a yet to be implemented version of
oheimb@2633
   332
			asm_full_simp_tac that applies all equalities in the
oheimb@2633
   333
			premises to all the premises *)
oheimb@2633
   334
oheimb@2633
   335
(*Add a simpset to a classical set!*)
oheimb@3206
   336
infix 4 addSss addss;
oheimb@3206
   337
fun cs addSss ss = cs addSaltern (CHANGED o (safe_asm_more_full_simp_tac ss));
oheimb@3206
   338
fun cs addss  ss = cs addbefore                        asm_full_simp_tac ss;
oheimb@2633
   339
wenzelm@4094
   340
fun Addss ss = (claset_ref() := claset() addss ss);
oheimb@2633
   341
oheimb@2633
   342
(*Designed to be idempotent, except if best_tac instantiates variables
oheimb@2633
   343
  in some of the subgoals*)
oheimb@2633
   344
oheimb@2633
   345
type clasimpset = (claset * simpset);
oheimb@2633
   346
oheimb@2633
   347
val FOL_css = (FOL_cs, FOL_ss);
oheimb@2633
   348
oheimb@2633
   349
fun pair_upd1 f ((a,b),x) = (f(a,x), b);
oheimb@2633
   350
fun pair_upd2 f ((a,b),x) = (a, f(b,x));
oheimb@2633
   351
oheimb@2633
   352
infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2
oheimb@2633
   353
	addsimps2 delsimps2 addcongs2 delcongs2;
paulson@2727
   354
fun op addSIs2   arg = pair_upd1 (op addSIs) arg;
paulson@2727
   355
fun op addSEs2   arg = pair_upd1 (op addSEs) arg;
paulson@2727
   356
fun op addSDs2   arg = pair_upd1 (op addSDs) arg;
paulson@2727
   357
fun op addIs2    arg = pair_upd1 (op addIs ) arg;
paulson@2727
   358
fun op addEs2    arg = pair_upd1 (op addEs ) arg;
paulson@2727
   359
fun op addDs2    arg = pair_upd1 (op addDs ) arg;
paulson@2727
   360
fun op addsimps2 arg = pair_upd2 (op addsimps) arg;
paulson@2727
   361
fun op delsimps2 arg = pair_upd2 (op delsimps) arg;
paulson@2727
   362
fun op addcongs2 arg = pair_upd2 (op addcongs) arg;
paulson@2727
   363
fun op delcongs2 arg = pair_upd2 (op delcongs) arg;
oheimb@2633
   364
oheimb@3206
   365
fun auto_tac (cs,ss) = 
oheimb@3206
   366
    let val cs' = cs addss ss 
oheimb@3206
   367
    in  EVERY [TRY (safe_tac cs'),
oheimb@3206
   368
	       REPEAT (FIRSTGOAL (fast_tac cs')),
oheimb@3206
   369
               TRY (safe_tac (cs addSss ss)),
oheimb@3206
   370
	       prune_params_tac] 
oheimb@3206
   371
    end;
oheimb@2633
   372
wenzelm@4094
   373
fun Auto_tac () = auto_tac (claset(), simpset());
oheimb@2633
   374
oheimb@2633
   375
fun auto () = by (Auto_tac ());