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