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