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