src/FOL/simpdata.ML
author oheimb
Thu May 31 16:52:02 2001 +0200 (2001-05-31)
changeset 11344 57b7ad51971c
parent 11232 558a4feebb04
child 11748 06eb315831ff
permissions -rw-r--r--
streamlined addIffs/delIffs, added warnings
wenzelm@9889
     1
(*  Title:      FOL/simpdata.ML
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
wenzelm@9889
     6
Simplification data for FOL.
clasohm@0
     7
*)
clasohm@0
     8
paulson@9300
     9
paulson@5496
    10
(* Elimination of True from asumptions: *)
paulson@5496
    11
paulson@5496
    12
val True_implies_equals = prove_goal IFOL.thy
paulson@5496
    13
 "(True ==> PROP P) == PROP P"
paulson@5496
    14
(K [rtac equal_intr_rule 1, atac 2,
paulson@5496
    15
          METAHYPS (fn prems => resolve_tac prems 1) 1,
paulson@5496
    16
          rtac TrueI 1]);
paulson@5496
    17
paulson@5496
    18
clasohm@0
    19
(*** Rewrite rules ***)
clasohm@0
    20
wenzelm@10431
    21
fun int_prove_fun s =
wenzelm@10431
    22
 (writeln s;
lcp@282
    23
  prove_goal IFOL.thy s
wenzelm@10431
    24
   (fn prems => [ (cut_facts_tac prems 1),
paulson@2601
    25
                  (IntPr.fast_tac 1) ]));
clasohm@0
    26
paulson@1953
    27
val conj_simps = map int_prove_fun
clasohm@1459
    28
 ["P & True <-> P",      "True & P <-> P",
clasohm@0
    29
  "P & False <-> False", "False & P <-> False",
nipkow@2801
    30
  "P & P <-> P", "P & P & Q <-> P & Q",
clasohm@1459
    31
  "P & ~P <-> False",    "~P & P <-> False",
clasohm@0
    32
  "(P & Q) & R <-> P & (Q & R)"];
clasohm@0
    33
paulson@1953
    34
val disj_simps = map int_prove_fun
clasohm@1459
    35
 ["P | True <-> True",  "True | P <-> True",
clasohm@1459
    36
  "P | False <-> P",    "False | P <-> P",
nipkow@2801
    37
  "P | P <-> P", "P | P | Q <-> P | Q",
clasohm@0
    38
  "(P | Q) | R <-> P | (Q | R)"];
clasohm@0
    39
paulson@1953
    40
val not_simps = map int_prove_fun
lcp@282
    41
 ["~(P|Q)  <-> ~P & ~Q",
clasohm@1459
    42
  "~ False <-> True",   "~ True <-> False"];
clasohm@0
    43
paulson@1953
    44
val imp_simps = map int_prove_fun
clasohm@1459
    45
 ["(P --> False) <-> ~P",       "(P --> True) <-> True",
wenzelm@10431
    46
  "(False --> P) <-> True",     "(True --> P) <-> P",
clasohm@1459
    47
  "(P --> P) <-> True",         "(P --> ~P) <-> ~P"];
clasohm@0
    48
paulson@1953
    49
val iff_simps = map int_prove_fun
clasohm@1459
    50
 ["(True <-> P) <-> P",         "(P <-> True) <-> P",
clasohm@0
    51
  "(P <-> P) <-> True",
clasohm@1459
    52
  "(False <-> P) <-> ~P",       "(P <-> False) <-> ~P"];
clasohm@0
    53
paulson@4349
    54
(*The x=t versions are needed for the simplification procedures*)
paulson@1953
    55
val quant_simps = map int_prove_fun
wenzelm@10431
    56
 ["(ALL x. P) <-> P",
paulson@4349
    57
  "(ALL x. x=t --> P(x)) <-> P(t)",
paulson@4349
    58
  "(ALL x. t=x --> P(x)) <-> P(t)",
paulson@4349
    59
  "(EX x. P) <-> P",
wenzelm@10431
    60
  "(EX x. x=t & P(x)) <-> P(t)",
paulson@4349
    61
  "(EX x. t=x & P(x)) <-> P(t)"];
clasohm@0
    62
clasohm@0
    63
(*These are NOT supplied by default!*)
paulson@1953
    64
val distrib_simps  = map int_prove_fun
wenzelm@10431
    65
 ["P & (Q | R) <-> P&Q | P&R",
lcp@282
    66
  "(Q | R) & P <-> Q&P | R&P",
clasohm@0
    67
  "(P | Q --> R) <-> (P --> R) & (Q --> R)"];
clasohm@0
    68
lcp@282
    69
(** Conversion into rewrite rules **)
clasohm@0
    70
nipkow@53
    71
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
nipkow@53
    72
lcp@282
    73
val P_iff_F = int_prove_fun "~P ==> (P <-> False)";
lcp@282
    74
val iff_reflection_F = P_iff_F RS iff_reflection;
lcp@282
    75
lcp@282
    76
val P_iff_T = int_prove_fun "P ==> (P <-> True)";
lcp@282
    77
val iff_reflection_T = P_iff_T RS iff_reflection;
lcp@282
    78
lcp@282
    79
(*Make meta-equalities.  The operator below is Trueprop*)
oheimb@5555
    80
lcp@282
    81
fun mk_meta_eq th = case concl_of th of
oheimb@5555
    82
    _ $ (Const("op =",_)$_$_)   => th RS eq_reflection
oheimb@5555
    83
  | _ $ (Const("op <->",_)$_$_) => th RS iff_reflection
wenzelm@10431
    84
  | _                           =>
oheimb@5555
    85
  error("conclusion must be a =-equality or <->");;
oheimb@5555
    86
oheimb@5555
    87
fun mk_eq th = case concl_of th of
nipkow@394
    88
    Const("==",_)$_$_           => th
oheimb@5555
    89
  | _ $ (Const("op =",_)$_$_)   => mk_meta_eq th
oheimb@5555
    90
  | _ $ (Const("op <->",_)$_$_) => mk_meta_eq th
lcp@282
    91
  | _ $ (Const("Not",_)$_)      => th RS iff_reflection_F
lcp@282
    92
  | _                           => th RS iff_reflection_T;
clasohm@0
    93
paulson@6114
    94
(*Replace premises x=y, X<->Y by X==Y*)
wenzelm@10431
    95
val mk_meta_prems =
wenzelm@10431
    96
    rule_by_tactic
paulson@6114
    97
      (REPEAT_FIRST (resolve_tac [meta_eq_to_obj_eq, def_imp_iff]));
paulson@6114
    98
wenzelm@9713
    99
(*Congruence rules for = or <-> (instead of ==)*)
paulson@6114
   100
fun mk_meta_cong rl =
paulson@6114
   101
  standard(mk_meta_eq (mk_meta_prems rl))
paulson@6114
   102
  handle THM _ =>
paulson@6114
   103
  error("Premises and conclusion of congruence rules must use =-equality or <->");
oheimb@5555
   104
oheimb@5304
   105
val mksimps_pairs =
oheimb@5304
   106
  [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
oheimb@5304
   107
   ("All", [spec]), ("True", []), ("False", [])];
oheimb@5304
   108
oheimb@5555
   109
(* ###FIXME: move to Provers/simplifier.ML
oheimb@5304
   110
val mk_atomize:      (string * thm list) list -> thm -> thm list
oheimb@5304
   111
*)
oheimb@5555
   112
(* ###FIXME: move to Provers/simplifier.ML *)
oheimb@5304
   113
fun mk_atomize pairs =
oheimb@5304
   114
  let fun atoms th =
oheimb@5304
   115
        (case concl_of th of
oheimb@5304
   116
           Const("Trueprop",_) $ p =>
oheimb@5304
   117
             (case head_of p of
oheimb@5304
   118
                Const(a,_) =>
oheimb@5304
   119
                  (case assoc(pairs,a) of
oheimb@5304
   120
                     Some(rls) => flat (map atoms ([th] RL rls))
oheimb@5304
   121
                   | None => [th])
oheimb@5304
   122
              | _ => [th])
oheimb@5304
   123
         | _ => [th])
oheimb@5304
   124
  in atoms end;
oheimb@5304
   125
oheimb@5555
   126
fun mksimps pairs = (map mk_eq o mk_atomize pairs o gen_all);
lcp@981
   127
paulson@2074
   128
(*** Classical laws ***)
lcp@282
   129
wenzelm@10431
   130
fun prove_fun s =
wenzelm@10431
   131
 (writeln s;
wenzelm@7355
   132
  prove_goal (the_context ()) s
wenzelm@10431
   133
   (fn prems => [ (cut_facts_tac prems 1),
clasohm@1459
   134
                  (Cla.fast_tac FOL_cs 1) ]));
lcp@745
   135
wenzelm@10431
   136
(*Avoids duplication of subgoals after expand_if, when the true and false
wenzelm@10431
   137
  cases boil down to the same thing.*)
paulson@1953
   138
val cases_simp = prove_fun "(P --> Q) & (~P --> Q) <-> Q";
paulson@1953
   139
paulson@4349
   140
paulson@4349
   141
(*** Miniscoping: pushing quantifiers in
paulson@4349
   142
     We do NOT distribute of ALL over &, or dually that of EX over |
wenzelm@10431
   143
     Baaz and Leitsch, On Skolemization and Proof Complexity (1994)
paulson@4349
   144
     show that this step can increase proof length!
paulson@4349
   145
***)
paulson@4349
   146
paulson@4349
   147
(*existential miniscoping*)
wenzelm@10431
   148
val int_ex_simps = map int_prove_fun
wenzelm@9713
   149
                     ["(EX x. P(x) & Q) <-> (EX x. P(x)) & Q",
wenzelm@9713
   150
                      "(EX x. P & Q(x)) <-> P & (EX x. Q(x))",
wenzelm@9713
   151
                      "(EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
wenzelm@9713
   152
                      "(EX x. P | Q(x)) <-> P | (EX x. Q(x))"];
paulson@4349
   153
paulson@4349
   154
(*classical rules*)
wenzelm@10431
   155
val cla_ex_simps = map prove_fun
paulson@4349
   156
                     ["(EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q",
wenzelm@9713
   157
                      "(EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"];
clasohm@0
   158
paulson@4349
   159
val ex_simps = int_ex_simps @ cla_ex_simps;
paulson@4349
   160
paulson@4349
   161
(*universal miniscoping*)
paulson@4349
   162
val int_all_simps = map int_prove_fun
wenzelm@9713
   163
                      ["(ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q",
wenzelm@9713
   164
                       "(ALL x. P & Q(x)) <-> P & (ALL x. Q(x))",
wenzelm@9713
   165
                       "(ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q",
wenzelm@9713
   166
                       "(ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"];
paulson@1953
   167
paulson@4349
   168
(*classical rules*)
paulson@4349
   169
val cla_all_simps = map prove_fun
paulson@4349
   170
                      ["(ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q",
wenzelm@9713
   171
                       "(ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"];
paulson@4349
   172
paulson@4349
   173
val all_simps = int_all_simps @ cla_all_simps;
paulson@4349
   174
paulson@4349
   175
paulson@4349
   176
(*** Named rewrite rules proved for IFOL ***)
paulson@1953
   177
paulson@1914
   178
fun int_prove nm thm  = qed_goal nm IFOL.thy thm
wenzelm@10431
   179
    (fn prems => [ (cut_facts_tac prems 1),
paulson@2601
   180
                   (IntPr.fast_tac 1) ]);
paulson@1914
   181
wenzelm@7355
   182
fun prove nm thm  = qed_goal nm (the_context ()) thm (fn _ => [Blast_tac 1]);
paulson@1914
   183
paulson@1914
   184
int_prove "conj_commute" "P&Q <-> Q&P";
paulson@1914
   185
int_prove "conj_left_commute" "P&(Q&R) <-> Q&(P&R)";
paulson@1914
   186
val conj_comms = [conj_commute, conj_left_commute];
paulson@1914
   187
paulson@1914
   188
int_prove "disj_commute" "P|Q <-> Q|P";
paulson@1914
   189
int_prove "disj_left_commute" "P|(Q|R) <-> Q|(P|R)";
paulson@1914
   190
val disj_comms = [disj_commute, disj_left_commute];
paulson@1914
   191
paulson@1914
   192
int_prove "conj_disj_distribL" "P&(Q|R) <-> (P&Q | P&R)";
paulson@1914
   193
int_prove "conj_disj_distribR" "(P|Q)&R <-> (P&R | Q&R)";
paulson@1914
   194
paulson@1914
   195
int_prove "disj_conj_distribL" "P|(Q&R) <-> (P|Q) & (P|R)";
paulson@1914
   196
int_prove "disj_conj_distribR" "(P&Q)|R <-> (P|R) & (Q|R)";
paulson@1914
   197
paulson@1914
   198
int_prove "imp_conj_distrib" "(P --> (Q&R)) <-> (P-->Q) & (P-->R)";
paulson@1914
   199
int_prove "imp_conj"         "((P&Q)-->R)   <-> (P --> (Q --> R))";
paulson@1914
   200
int_prove "imp_disj"         "(P|Q --> R)   <-> (P-->R) & (Q-->R)";
paulson@1914
   201
paulson@3910
   202
prove "imp_disj1" "(P-->Q) | R <-> (P-->Q | R)";
paulson@3910
   203
prove "imp_disj2" "Q | (P-->R) <-> (P-->Q | R)";
paulson@3910
   204
paulson@1914
   205
int_prove "de_Morgan_disj" "(~(P | Q)) <-> (~P & ~Q)";
paulson@1914
   206
prove     "de_Morgan_conj" "(~(P & Q)) <-> (~P | ~Q)";
paulson@1914
   207
paulson@1914
   208
prove     "not_iff" "~(P <-> Q) <-> (P <-> ~Q)";
paulson@1914
   209
wenzelm@3835
   210
prove     "not_all" "(~ (ALL x. P(x))) <-> (EX x.~P(x))";
wenzelm@3835
   211
prove     "imp_all" "((ALL x. P(x)) --> Q) <-> (EX x. P(x) --> Q)";
wenzelm@3835
   212
int_prove "not_ex"  "(~ (EX x. P(x))) <-> (ALL x.~P(x))";
paulson@1914
   213
int_prove "imp_ex" "((EX x. P(x)) --> Q) <-> (ALL x. P(x) --> Q)";
paulson@1914
   214
paulson@1914
   215
int_prove "ex_disj_distrib"
paulson@1914
   216
    "(EX x. P(x) | Q(x)) <-> ((EX x. P(x)) | (EX x. Q(x)))";
paulson@1914
   217
int_prove "all_conj_distrib"
paulson@1914
   218
    "(ALL x. P(x) & Q(x)) <-> ((ALL x. P(x)) & (ALL x. Q(x)))";
paulson@1914
   219
paulson@1914
   220
nipkow@11232
   221
local
nipkow@11232
   222
val uncurry = prove_goal (the_context()) "P --> Q --> R ==> P & Q --> R"
nipkow@11232
   223
              (fn prems => [cut_facts_tac prems 1, Blast_tac 1]);
nipkow@11232
   224
nipkow@11232
   225
val iff_allI = allI RS
nipkow@11232
   226
    prove_goal (the_context()) "ALL x. P(x) <-> Q(x) ==> (ALL x. P(x)) <-> (ALL x. Q(x))"
nipkow@11232
   227
               (fn prems => [cut_facts_tac prems 1, Blast_tac 1])
nipkow@11232
   228
in
nipkow@11232
   229
paulson@4349
   230
(** make simplification procedures for quantifier elimination **)
paulson@4349
   231
structure Quantifier1 = Quantifier1Fun(
paulson@4349
   232
struct
paulson@4349
   233
  (*abstract syntax*)
paulson@4349
   234
  fun dest_eq((c as Const("op =",_)) $ s $ t) = Some(c,s,t)
paulson@4349
   235
    | dest_eq _ = None;
paulson@4349
   236
  fun dest_conj((c as Const("op &",_)) $ s $ t) = Some(c,s,t)
paulson@4349
   237
    | dest_conj _ = None;
nipkow@11232
   238
  fun dest_imp((c as Const("op -->",_)) $ s $ t) = Some(c,s,t)
nipkow@11232
   239
    | dest_imp _ = None;
paulson@4349
   240
  val conj = FOLogic.conj
paulson@4349
   241
  val imp  = FOLogic.imp
paulson@4349
   242
  (*rules*)
paulson@4349
   243
  val iff_reflection = iff_reflection
paulson@4349
   244
  val iffI = iffI
paulson@4349
   245
  val conjI= conjI
paulson@4349
   246
  val conjE= conjE
paulson@4349
   247
  val impI = impI
paulson@4349
   248
  val mp   = mp
nipkow@11232
   249
  val uncurry = uncurry
paulson@4349
   250
  val exI  = exI
paulson@4349
   251
  val exE  = exE
nipkow@11232
   252
  val iff_allI = iff_allI
paulson@4349
   253
end);
paulson@4349
   254
nipkow@11232
   255
end;
nipkow@11232
   256
paulson@4349
   257
local
wenzelm@7355
   258
paulson@4349
   259
val ex_pattern =
wenzelm@7355
   260
  read_cterm (Theory.sign_of (the_context ())) ("EX x. P(x) & Q(x)", FOLogic.oT)
paulson@4349
   261
paulson@4349
   262
val all_pattern =
nipkow@11232
   263
  read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x) --> Q(x)", FOLogic.oT)
paulson@4349
   264
paulson@4349
   265
in
paulson@4349
   266
val defEX_regroup =
paulson@4349
   267
  mk_simproc "defined EX" [ex_pattern] Quantifier1.rearrange_ex;
paulson@4349
   268
val defALL_regroup =
paulson@4349
   269
  mk_simproc "defined ALL" [all_pattern] Quantifier1.rearrange_all;
paulson@4349
   270
end;
paulson@4349
   271
paulson@4349
   272
paulson@4349
   273
(*** Case splitting ***)
clasohm@0
   274
oheimb@5304
   275
val meta_eq_to_iff = prove_goal IFOL.thy "x==y ==> x<->y"
oheimb@5304
   276
  (fn [prem] => [rewtac prem, rtac iffI 1, atac 1, atac 1]);
berghofe@1722
   277
oheimb@5304
   278
structure SplitterData =
oheimb@5304
   279
  struct
oheimb@5304
   280
  structure Simplifier = Simplifier
oheimb@5555
   281
  val mk_eq          = mk_eq
oheimb@5304
   282
  val meta_eq_to_iff = meta_eq_to_iff
oheimb@5304
   283
  val iffD           = iffD2
oheimb@5304
   284
  val disjE          = disjE
oheimb@5304
   285
  val conjE          = conjE
oheimb@5304
   286
  val exE            = exE
oheimb@5304
   287
  val contrapos      = contrapos
oheimb@5304
   288
  val contrapos2     = contrapos2
oheimb@5304
   289
  val notnotD        = notnotD
oheimb@5304
   290
  end;
berghofe@1722
   291
oheimb@5304
   292
structure Splitter = SplitterFun(SplitterData);
berghofe@1722
   293
oheimb@5304
   294
val split_tac        = Splitter.split_tac;
oheimb@5304
   295
val split_inside_tac = Splitter.split_inside_tac;
oheimb@5304
   296
val split_asm_tac    = Splitter.split_asm_tac;
oheimb@5307
   297
val op addsplits     = Splitter.addsplits;
oheimb@5307
   298
val op delsplits     = Splitter.delsplits;
oheimb@5304
   299
val Addsplits        = Splitter.Addsplits;
oheimb@5304
   300
val Delsplits        = Splitter.Delsplits;
paulson@4325
   301
paulson@4325
   302
paulson@2074
   303
(*** Standard simpsets ***)
paulson@2074
   304
paulson@2074
   305
structure Induction = InductionFun(struct val spec=IFOL.spec end);
paulson@2074
   306
paulson@4349
   307
open Induction;
paulson@2074
   308
oheimb@5555
   309
paulson@5496
   310
val meta_simps =
paulson@5496
   311
   [triv_forall_equality,  (* prunes params *)
paulson@5496
   312
    True_implies_equals];  (* prune asms `True' *)
paulson@5496
   313
paulson@2074
   314
val IFOL_simps =
wenzelm@10431
   315
    [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @
paulson@2074
   316
    imp_simps @ iff_simps @ quant_simps;
paulson@2074
   317
paulson@2074
   318
val notFalseI = int_prove_fun "~False";
paulson@6114
   319
val triv_rls = [TrueI,refl,reflexive_thm,iff_refl,notFalseI];
paulson@2074
   320
oheimb@2633
   321
fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems),
wenzelm@9713
   322
                                 atac, etac FalseE];
oheimb@2633
   323
(*No premature instantiation of variables during simplification*)
oheimb@2633
   324
fun   safe_solver prems = FIRST'[match_tac (triv_rls@prems),
wenzelm@9713
   325
                                 eq_assume_tac, ematch_tac [FalseE]];
oheimb@2633
   326
paulson@3910
   327
(*No simprules, but basic infastructure for simplification*)
wenzelm@10431
   328
val FOL_basic_ss = empty_ss
wenzelm@10431
   329
  setsubgoaler asm_simp_tac
wenzelm@10431
   330
  setSSolver (mk_solver "FOL safe" safe_solver)
wenzelm@10431
   331
  setSolver (mk_solver "FOL unsafe" unsafe_solver)
wenzelm@10431
   332
  setmksimps (mksimps mksimps_pairs)
wenzelm@10431
   333
  setmkcong mk_meta_cong;
oheimb@5304
   334
oheimb@2633
   335
paulson@3910
   336
(*intuitionistic simprules only*)
wenzelm@10431
   337
val IFOL_ss = FOL_basic_ss
wenzelm@10431
   338
  addsimps (meta_simps @ IFOL_simps @ int_ex_simps @ int_all_simps)
wenzelm@10431
   339
  addsimprocs [defALL_regroup, defEX_regroup]    
wenzelm@10431
   340
  addcongs [imp_cong];
paulson@2074
   341
wenzelm@9713
   342
val cla_simps =
paulson@3910
   343
    [de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2,
paulson@3910
   344
     not_all, not_ex, cases_simp] @
paulson@2074
   345
    map prove_fun
paulson@2074
   346
     ["~(P&Q)  <-> ~P | ~Q",
paulson@2074
   347
      "P | ~P",             "~P | P",
paulson@2074
   348
      "~ ~ P <-> P",        "(~P --> P) <-> P",
paulson@2074
   349
      "(~P <-> ~Q) <-> (P<->Q)"];
paulson@2074
   350
paulson@3910
   351
(*classical simprules too*)
paulson@4349
   352
val FOL_ss = IFOL_ss addsimps (cla_simps @ cla_ex_simps @ cla_all_simps);
paulson@2074
   353
wenzelm@7355
   354
val simpsetup = [fn thy => (simpset_ref_of thy := FOL_ss; thy)];
oheimb@2633
   355
oheimb@2633
   356
wenzelm@5219
   357
(*** integration of simplifier with classical reasoner ***)
oheimb@2633
   358
wenzelm@5219
   359
structure Clasimp = ClasimpFun
wenzelm@8472
   360
 (structure Simplifier = Simplifier and Splitter = Splitter
wenzelm@9851
   361
  and Classical  = Cla and Blast = Blast
oheimb@11344
   362
  val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE
wenzelm@9851
   363
  val cla_make_elim = cla_make_elim);
oheimb@4652
   364
open Clasimp;
oheimb@2633
   365
oheimb@2633
   366
val FOL_css = (FOL_cs, FOL_ss);
wenzelm@9889
   367
wenzelm@9889
   368
wenzelm@9889
   369
(* rulify setup *)
wenzelm@9889
   370
wenzelm@9889
   371
local
wenzelm@9889
   372
  val ss = FOL_basic_ss addsimps (Drule.norm_hhf_eq :: map Thm.symmetric (thms "atomize"));
wenzelm@9889
   373
in
wenzelm@9889
   374
wenzelm@9889
   375
structure Rulify = RulifyFun
wenzelm@9889
   376
 (val make_meta = Simplifier.simplify ss
wenzelm@9889
   377
  val full_make_meta = Simplifier.full_simplify ss);
wenzelm@9889
   378
wenzelm@9889
   379
structure BasicRulify: BASIC_RULIFY = Rulify;
wenzelm@9889
   380
open BasicRulify;
wenzelm@9889
   381
wenzelm@9889
   382
end;