src/FOL/simpdata.ML
author oheimb
Wed Aug 12 17:40:18 1998 +0200 (1998-08-12)
changeset 5307 6a699d5cdef4
parent 5304 c133f16febc7
child 5496 42d13691be86
permissions -rw-r--r--
minor adaption for SML/NJ
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
val P_iff_F = int_prove_fun "~P ==> (P <-> False)";
lcp@282
    64
val iff_reflection_F = P_iff_F RS iff_reflection;
lcp@282
    65
lcp@282
    66
val P_iff_T = int_prove_fun "P ==> (P <-> True)";
lcp@282
    67
val iff_reflection_T = P_iff_T RS iff_reflection;
lcp@282
    68
lcp@282
    69
(*Make meta-equalities.  The operator below is Trueprop*)
lcp@282
    70
fun mk_meta_eq th = case concl_of th of
nipkow@394
    71
    Const("==",_)$_$_           => th
nipkow@394
    72
  | _ $ (Const("op =",_)$_$_)   => th RS eq_reflection
lcp@282
    73
  | _ $ (Const("op <->",_)$_$_) => th RS iff_reflection
lcp@282
    74
  | _ $ (Const("Not",_)$_)      => th RS iff_reflection_F
lcp@282
    75
  | _                           => th RS iff_reflection_T;
clasohm@0
    76
oheimb@5304
    77
val mksimps_pairs =
oheimb@5304
    78
  [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
oheimb@5304
    79
   ("All", [spec]), ("True", []), ("False", [])];
oheimb@5304
    80
oheimb@5304
    81
(* FIXME: move to Provers/simplifier.ML
oheimb@5304
    82
val mk_atomize:      (string * thm list) list -> thm -> thm list
oheimb@5304
    83
*)
oheimb@5304
    84
(* FIXME: move to Provers/simplifier.ML*)
oheimb@5304
    85
fun mk_atomize pairs =
oheimb@5304
    86
  let fun atoms th =
oheimb@5304
    87
        (case concl_of th of
oheimb@5304
    88
           Const("Trueprop",_) $ p =>
oheimb@5304
    89
             (case head_of p of
oheimb@5304
    90
                Const(a,_) =>
oheimb@5304
    91
                  (case assoc(pairs,a) of
oheimb@5304
    92
                     Some(rls) => flat (map atoms ([th] RL rls))
oheimb@5304
    93
                   | None => [th])
oheimb@5304
    94
              | _ => [th])
oheimb@5304
    95
         | _ => [th])
oheimb@5304
    96
  in atoms end;
oheimb@5304
    97
oheimb@5304
    98
fun mksimps pairs = (map mk_meta_eq o mk_atomize pairs o gen_all);
lcp@981
    99
paulson@2074
   100
(*** Classical laws ***)
lcp@282
   101
clasohm@0
   102
fun prove_fun s = 
lcp@282
   103
 (writeln s;  
lcp@282
   104
  prove_goal FOL.thy s
lcp@282
   105
   (fn prems => [ (cut_facts_tac prems 1), 
clasohm@1459
   106
                  (Cla.fast_tac FOL_cs 1) ]));
lcp@745
   107
paulson@1953
   108
(*Avoids duplication of subgoals after expand_if, when the true and false 
paulson@1953
   109
  cases boil down to the same thing.*) 
paulson@1953
   110
val cases_simp = prove_fun "(P --> Q) & (~P --> Q) <-> Q";
paulson@1953
   111
paulson@4349
   112
paulson@4349
   113
(*** Miniscoping: pushing quantifiers in
paulson@4349
   114
     We do NOT distribute of ALL over &, or dually that of EX over |
paulson@4349
   115
     Baaz and Leitsch, On Skolemization and Proof Complexity (1994) 
paulson@4349
   116
     show that this step can increase proof length!
paulson@4349
   117
***)
paulson@4349
   118
paulson@4349
   119
(*existential miniscoping*)
paulson@4349
   120
val int_ex_simps = map int_prove_fun 
paulson@4349
   121
		     ["(EX x. P(x) & Q) <-> (EX x. P(x)) & Q",
paulson@4349
   122
		      "(EX x. P & Q(x)) <-> P & (EX x. Q(x))",
paulson@4349
   123
		      "(EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
paulson@4349
   124
		      "(EX x. P | Q(x)) <-> P | (EX x. Q(x))"];
paulson@4349
   125
paulson@4349
   126
(*classical rules*)
paulson@4349
   127
val cla_ex_simps = map prove_fun 
paulson@4349
   128
                     ["(EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q",
paulson@4349
   129
		      "(EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"];
clasohm@0
   130
paulson@4349
   131
val ex_simps = int_ex_simps @ cla_ex_simps;
paulson@4349
   132
paulson@4349
   133
(*universal miniscoping*)
paulson@4349
   134
val int_all_simps = map int_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
		       "(ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q",
paulson@4349
   138
		       "(ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"];
paulson@1953
   139
paulson@4349
   140
(*classical rules*)
paulson@4349
   141
val cla_all_simps = map prove_fun
paulson@4349
   142
                      ["(ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q",
paulson@4349
   143
		       "(ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"];
paulson@4349
   144
paulson@4349
   145
val all_simps = int_all_simps @ cla_all_simps;
paulson@4349
   146
paulson@4349
   147
paulson@4349
   148
(*** Named rewrite rules proved for IFOL ***)
paulson@1953
   149
paulson@1914
   150
fun int_prove nm thm  = qed_goal nm IFOL.thy thm
paulson@1914
   151
    (fn prems => [ (cut_facts_tac prems 1), 
paulson@2601
   152
                   (IntPr.fast_tac 1) ]);
paulson@1914
   153
paulson@3910
   154
fun prove nm thm  = qed_goal nm FOL.thy thm (fn _ => [Blast_tac 1]);
paulson@1914
   155
paulson@1914
   156
int_prove "conj_commute" "P&Q <-> Q&P";
paulson@1914
   157
int_prove "conj_left_commute" "P&(Q&R) <-> Q&(P&R)";
paulson@1914
   158
val conj_comms = [conj_commute, conj_left_commute];
paulson@1914
   159
paulson@1914
   160
int_prove "disj_commute" "P|Q <-> Q|P";
paulson@1914
   161
int_prove "disj_left_commute" "P|(Q|R) <-> Q|(P|R)";
paulson@1914
   162
val disj_comms = [disj_commute, disj_left_commute];
paulson@1914
   163
paulson@1914
   164
int_prove "conj_disj_distribL" "P&(Q|R) <-> (P&Q | P&R)";
paulson@1914
   165
int_prove "conj_disj_distribR" "(P|Q)&R <-> (P&R | Q&R)";
paulson@1914
   166
paulson@1914
   167
int_prove "disj_conj_distribL" "P|(Q&R) <-> (P|Q) & (P|R)";
paulson@1914
   168
int_prove "disj_conj_distribR" "(P&Q)|R <-> (P|R) & (Q|R)";
paulson@1914
   169
paulson@1914
   170
int_prove "imp_conj_distrib" "(P --> (Q&R)) <-> (P-->Q) & (P-->R)";
paulson@1914
   171
int_prove "imp_conj"         "((P&Q)-->R)   <-> (P --> (Q --> R))";
paulson@1914
   172
int_prove "imp_disj"         "(P|Q --> R)   <-> (P-->R) & (Q-->R)";
paulson@1914
   173
paulson@3910
   174
prove "imp_disj1" "(P-->Q) | R <-> (P-->Q | R)";
paulson@3910
   175
prove "imp_disj2" "Q | (P-->R) <-> (P-->Q | R)";
paulson@3910
   176
paulson@1914
   177
int_prove "de_Morgan_disj" "(~(P | Q)) <-> (~P & ~Q)";
paulson@1914
   178
prove     "de_Morgan_conj" "(~(P & Q)) <-> (~P | ~Q)";
paulson@1914
   179
paulson@1914
   180
prove     "not_iff" "~(P <-> Q) <-> (P <-> ~Q)";
paulson@1914
   181
wenzelm@3835
   182
prove     "not_all" "(~ (ALL x. P(x))) <-> (EX x.~P(x))";
wenzelm@3835
   183
prove     "imp_all" "((ALL x. P(x)) --> Q) <-> (EX x. P(x) --> Q)";
wenzelm@3835
   184
int_prove "not_ex"  "(~ (EX x. P(x))) <-> (ALL x.~P(x))";
paulson@1914
   185
int_prove "imp_ex" "((EX x. P(x)) --> Q) <-> (ALL x. P(x) --> Q)";
paulson@1914
   186
paulson@1914
   187
int_prove "ex_disj_distrib"
paulson@1914
   188
    "(EX x. P(x) | Q(x)) <-> ((EX x. P(x)) | (EX x. Q(x)))";
paulson@1914
   189
int_prove "all_conj_distrib"
paulson@1914
   190
    "(ALL x. P(x) & Q(x)) <-> ((ALL x. P(x)) & (ALL x. Q(x)))";
paulson@1914
   191
paulson@1914
   192
lcp@1088
   193
(*Used in ZF, perhaps elsewhere?*)
lcp@1088
   194
val meta_eq_to_obj_eq = prove_goal IFOL.thy "x==y ==> x=y"
lcp@1088
   195
  (fn [prem] => [rewtac prem, rtac refl 1]);
lcp@1088
   196
paulson@4349
   197
paulson@4349
   198
(** make simplification procedures for quantifier elimination **)
paulson@4349
   199
structure Quantifier1 = Quantifier1Fun(
paulson@4349
   200
struct
paulson@4349
   201
  (*abstract syntax*)
paulson@4349
   202
  fun dest_eq((c as Const("op =",_)) $ s $ t) = Some(c,s,t)
paulson@4349
   203
    | dest_eq _ = None;
paulson@4349
   204
  fun dest_conj((c as Const("op &",_)) $ s $ t) = Some(c,s,t)
paulson@4349
   205
    | dest_conj _ = None;
paulson@4349
   206
  val conj = FOLogic.conj
paulson@4349
   207
  val imp  = FOLogic.imp
paulson@4349
   208
  (*rules*)
paulson@4349
   209
  val iff_reflection = iff_reflection
paulson@4349
   210
  val iffI = iffI
paulson@4349
   211
  val sym  = sym
paulson@4349
   212
  val conjI= conjI
paulson@4349
   213
  val conjE= conjE
paulson@4349
   214
  val impI = impI
paulson@4349
   215
  val impE = impE
paulson@4349
   216
  val mp   = mp
paulson@4349
   217
  val exI  = exI
paulson@4349
   218
  val exE  = exE
paulson@4349
   219
  val allI = allI
paulson@4349
   220
  val allE = allE
paulson@4349
   221
end);
paulson@4349
   222
paulson@4349
   223
local
paulson@4349
   224
val ex_pattern =
paulson@4349
   225
  read_cterm (sign_of FOL.thy) ("EX x. P(x) & Q(x)", FOLogic.oT)
paulson@4349
   226
paulson@4349
   227
val all_pattern =
paulson@4349
   228
  read_cterm (sign_of FOL.thy) ("ALL x. P(x) & P'(x) --> Q(x)", FOLogic.oT)
paulson@4349
   229
paulson@4349
   230
in
paulson@4349
   231
val defEX_regroup =
paulson@4349
   232
  mk_simproc "defined EX" [ex_pattern] Quantifier1.rearrange_ex;
paulson@4349
   233
val defALL_regroup =
paulson@4349
   234
  mk_simproc "defined ALL" [all_pattern] Quantifier1.rearrange_all;
paulson@4349
   235
end;
paulson@4349
   236
paulson@4349
   237
paulson@4349
   238
(*** Case splitting ***)
clasohm@0
   239
oheimb@5304
   240
val meta_eq_to_iff = prove_goal IFOL.thy "x==y ==> x<->y"
oheimb@5304
   241
  (fn [prem] => [rewtac prem, rtac iffI 1, atac 1, atac 1]);
berghofe@1722
   242
oheimb@5304
   243
structure SplitterData =
oheimb@5304
   244
  struct
oheimb@5304
   245
  structure Simplifier = Simplifier
oheimb@5304
   246
  val mk_meta_eq     = mk_meta_eq
oheimb@5304
   247
  val meta_eq_to_iff = meta_eq_to_iff
oheimb@5304
   248
  val iffD           = iffD2
oheimb@5304
   249
  val disjE          = disjE
oheimb@5304
   250
  val conjE          = conjE
oheimb@5304
   251
  val exE            = exE
oheimb@5304
   252
  val contrapos      = contrapos
oheimb@5304
   253
  val contrapos2     = contrapos2
oheimb@5304
   254
  val notnotD        = notnotD
oheimb@5304
   255
  end;
berghofe@1722
   256
oheimb@5304
   257
structure Splitter = SplitterFun(SplitterData);
berghofe@1722
   258
oheimb@5304
   259
val split_tac        = Splitter.split_tac;
oheimb@5304
   260
val split_inside_tac = Splitter.split_inside_tac;
oheimb@5304
   261
val split_asm_tac    = Splitter.split_asm_tac;
oheimb@5307
   262
val op addsplits     = Splitter.addsplits;
oheimb@5307
   263
val op delsplits     = Splitter.delsplits;
oheimb@5304
   264
val Addsplits        = Splitter.Addsplits;
oheimb@5304
   265
val Delsplits        = Splitter.Delsplits;
paulson@4325
   266
paulson@4325
   267
paulson@2074
   268
(*** Standard simpsets ***)
paulson@2074
   269
paulson@2074
   270
structure Induction = InductionFun(struct val spec=IFOL.spec end);
paulson@2074
   271
paulson@4349
   272
open Induction;
paulson@2074
   273
paulson@2074
   274
(*Add congruence rules for = or <-> (instead of ==) *)
oheimb@2633
   275
infix 4 addcongs delcongs;
paulson@2074
   276
fun ss addcongs congs =
wenzelm@3566
   277
        ss addeqcongs (map standard (congs RL [eq_reflection,iff_reflection]));
oheimb@2633
   278
fun ss delcongs congs =
wenzelm@3566
   279
        ss deleqcongs (map standard (congs RL [eq_reflection,iff_reflection]));
paulson@2469
   280
wenzelm@4094
   281
fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
wenzelm@4094
   282
fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
paulson@2074
   283
paulson@5115
   284
paulson@2074
   285
val IFOL_simps =
paulson@2074
   286
   [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
paulson@2074
   287
    imp_simps @ iff_simps @ quant_simps;
paulson@2074
   288
paulson@2074
   289
val notFalseI = int_prove_fun "~False";
paulson@2074
   290
val triv_rls = [TrueI,refl,iff_refl,notFalseI];
paulson@2074
   291
oheimb@2633
   292
fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems),
oheimb@2633
   293
				 atac, etac FalseE];
oheimb@2633
   294
(*No premature instantiation of variables during simplification*)
oheimb@2633
   295
fun   safe_solver prems = FIRST'[match_tac (triv_rls@prems),
oheimb@2633
   296
				 eq_assume_tac, ematch_tac [FalseE]];
oheimb@2633
   297
paulson@3910
   298
(*No simprules, but basic infastructure for simplification*)
oheimb@2633
   299
val FOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
paulson@4349
   300
                            addsimprocs [defALL_regroup,defEX_regroup]
oheimb@2633
   301
			    setSSolver   safe_solver
oheimb@2633
   302
			    setSolver  unsafe_solver
oheimb@5304
   303
			    setmksimps (mksimps mksimps_pairs);
oheimb@5304
   304
oheimb@5304
   305
oheimb@2633
   306
paulson@3910
   307
(*intuitionistic simprules only*)
paulson@4349
   308
val IFOL_ss = FOL_basic_ss addsimps (IFOL_simps @ int_ex_simps @ int_all_simps)
oheimb@2633
   309
			   addcongs [imp_cong];
paulson@2074
   310
paulson@2074
   311
val cla_simps = 
paulson@3910
   312
    [de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2,
paulson@3910
   313
     not_all, not_ex, cases_simp] @
paulson@2074
   314
    map prove_fun
paulson@2074
   315
     ["~(P&Q)  <-> ~P | ~Q",
paulson@2074
   316
      "P | ~P",             "~P | P",
paulson@2074
   317
      "~ ~ P <-> P",        "(~P --> P) <-> P",
paulson@2074
   318
      "(~P <-> ~Q) <-> (P<->Q)"];
paulson@2074
   319
paulson@3910
   320
(*classical simprules too*)
paulson@4349
   321
val FOL_ss = IFOL_ss addsimps (cla_simps @ cla_ex_simps @ cla_all_simps);
paulson@2074
   322
wenzelm@4094
   323
simpset_ref() := FOL_ss;
oheimb@2633
   324
oheimb@2633
   325
oheimb@2633
   326
wenzelm@5219
   327
(*** integration of simplifier with classical reasoner ***)
oheimb@2633
   328
wenzelm@5219
   329
structure Clasimp = ClasimpFun
wenzelm@5219
   330
 (structure Simplifier = Simplifier and Classical = Cla and Blast = Blast
wenzelm@5220
   331
  val op addcongs = op addcongs and op delcongs = op delcongs
wenzelm@5220
   332
  and op addSaltern = op addSaltern and op addbefore = op addbefore);
wenzelm@5219
   333
oheimb@4652
   334
open Clasimp;
oheimb@2633
   335
oheimb@2633
   336
val FOL_css = (FOL_cs, FOL_ss);