src/FOL/simpdata.ML
author wenzelm
Thu Sep 07 20:49:19 2000 +0200 (2000-09-07)
changeset 9889 8802b140334c
parent 9851 e22db9397e17
child 10431 bb67f704d631
permissions -rw-r--r--
rulify setup;
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
clasohm@0
    21
fun int_prove_fun s = 
lcp@282
    22
 (writeln s;  
lcp@282
    23
  prove_goal IFOL.thy s
lcp@282
    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",
clasohm@1459
    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
paulson@4349
    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",
paulson@4349
    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
lcp@282
    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
oheimb@5555
    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*)
paulson@6114
    95
val mk_meta_prems = 
paulson@6114
    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
clasohm@0
   130
fun prove_fun s = 
lcp@282
   131
 (writeln s;  
wenzelm@7355
   132
  prove_goal (the_context ()) s
lcp@282
   133
   (fn prems => [ (cut_facts_tac prems 1), 
clasohm@1459
   134
                  (Cla.fast_tac FOL_cs 1) ]));
lcp@745
   135
paulson@1953
   136
(*Avoids duplication of subgoals after expand_if, when the true and false 
paulson@1953
   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 |
paulson@4349
   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*)
paulson@4349
   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*)
paulson@4349
   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
paulson@1914
   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
paulson@4349
   221
(** make simplification procedures for quantifier elimination **)
paulson@4349
   222
structure Quantifier1 = Quantifier1Fun(
paulson@4349
   223
struct
paulson@4349
   224
  (*abstract syntax*)
paulson@4349
   225
  fun dest_eq((c as Const("op =",_)) $ s $ t) = Some(c,s,t)
paulson@4349
   226
    | dest_eq _ = None;
paulson@4349
   227
  fun dest_conj((c as Const("op &",_)) $ s $ t) = Some(c,s,t)
paulson@4349
   228
    | dest_conj _ = None;
paulson@4349
   229
  val conj = FOLogic.conj
paulson@4349
   230
  val imp  = FOLogic.imp
paulson@4349
   231
  (*rules*)
paulson@4349
   232
  val iff_reflection = iff_reflection
paulson@4349
   233
  val iffI = iffI
paulson@4349
   234
  val sym  = sym
paulson@4349
   235
  val conjI= conjI
paulson@4349
   236
  val conjE= conjE
paulson@4349
   237
  val impI = impI
paulson@4349
   238
  val impE = impE
paulson@4349
   239
  val mp   = mp
paulson@4349
   240
  val exI  = exI
paulson@4349
   241
  val exE  = exE
paulson@4349
   242
  val allI = allI
paulson@4349
   243
  val allE = allE
paulson@4349
   244
end);
paulson@4349
   245
paulson@4349
   246
local
wenzelm@7355
   247
paulson@4349
   248
val ex_pattern =
wenzelm@7355
   249
  read_cterm (Theory.sign_of (the_context ())) ("EX x. P(x) & Q(x)", FOLogic.oT)
paulson@4349
   250
paulson@4349
   251
val all_pattern =
wenzelm@7355
   252
  read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x) & P'(x) --> Q(x)", FOLogic.oT)
paulson@4349
   253
paulson@4349
   254
in
paulson@4349
   255
val defEX_regroup =
paulson@4349
   256
  mk_simproc "defined EX" [ex_pattern] Quantifier1.rearrange_ex;
paulson@4349
   257
val defALL_regroup =
paulson@4349
   258
  mk_simproc "defined ALL" [all_pattern] Quantifier1.rearrange_all;
paulson@4349
   259
end;
paulson@4349
   260
paulson@4349
   261
paulson@4349
   262
(*** Case splitting ***)
clasohm@0
   263
oheimb@5304
   264
val meta_eq_to_iff = prove_goal IFOL.thy "x==y ==> x<->y"
oheimb@5304
   265
  (fn [prem] => [rewtac prem, rtac iffI 1, atac 1, atac 1]);
berghofe@1722
   266
oheimb@5304
   267
structure SplitterData =
oheimb@5304
   268
  struct
oheimb@5304
   269
  structure Simplifier = Simplifier
oheimb@5555
   270
  val mk_eq          = mk_eq
oheimb@5304
   271
  val meta_eq_to_iff = meta_eq_to_iff
oheimb@5304
   272
  val iffD           = iffD2
oheimb@5304
   273
  val disjE          = disjE
oheimb@5304
   274
  val conjE          = conjE
oheimb@5304
   275
  val exE            = exE
oheimb@5304
   276
  val contrapos      = contrapos
oheimb@5304
   277
  val contrapos2     = contrapos2
oheimb@5304
   278
  val notnotD        = notnotD
oheimb@5304
   279
  end;
berghofe@1722
   280
oheimb@5304
   281
structure Splitter = SplitterFun(SplitterData);
berghofe@1722
   282
oheimb@5304
   283
val split_tac        = Splitter.split_tac;
oheimb@5304
   284
val split_inside_tac = Splitter.split_inside_tac;
oheimb@5304
   285
val split_asm_tac    = Splitter.split_asm_tac;
oheimb@5307
   286
val op addsplits     = Splitter.addsplits;
oheimb@5307
   287
val op delsplits     = Splitter.delsplits;
oheimb@5304
   288
val Addsplits        = Splitter.Addsplits;
oheimb@5304
   289
val Delsplits        = Splitter.Delsplits;
paulson@4325
   290
paulson@4325
   291
paulson@2074
   292
(*** Standard simpsets ***)
paulson@2074
   293
paulson@2074
   294
structure Induction = InductionFun(struct val spec=IFOL.spec end);
paulson@2074
   295
paulson@4349
   296
open Induction;
paulson@2074
   297
oheimb@5555
   298
paulson@5496
   299
val meta_simps =
paulson@5496
   300
   [triv_forall_equality,  (* prunes params *)
paulson@5496
   301
    True_implies_equals];  (* prune asms `True' *)
paulson@5496
   302
paulson@2074
   303
val IFOL_simps =
paulson@6114
   304
    [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
paulson@2074
   305
    imp_simps @ iff_simps @ quant_simps;
paulson@2074
   306
paulson@2074
   307
val notFalseI = int_prove_fun "~False";
paulson@6114
   308
val triv_rls = [TrueI,refl,reflexive_thm,iff_refl,notFalseI];
paulson@2074
   309
oheimb@2633
   310
fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems),
wenzelm@9713
   311
                                 atac, etac FalseE];
oheimb@2633
   312
(*No premature instantiation of variables during simplification*)
oheimb@2633
   313
fun   safe_solver prems = FIRST'[match_tac (triv_rls@prems),
wenzelm@9713
   314
                                 eq_assume_tac, ematch_tac [FalseE]];
oheimb@2633
   315
paulson@3910
   316
(*No simprules, but basic infastructure for simplification*)
wenzelm@9713
   317
val FOL_basic_ss =
wenzelm@9713
   318
  empty_ss setsubgoaler asm_simp_tac
wenzelm@9713
   319
    addsimprocs [defALL_regroup, defEX_regroup]
wenzelm@9713
   320
    setSSolver (mk_solver "FOL safe" safe_solver)
wenzelm@9713
   321
    setSolver (mk_solver "FOL unsafe" unsafe_solver)
wenzelm@9713
   322
    setmksimps (mksimps mksimps_pairs)
wenzelm@9713
   323
    setmkcong mk_meta_cong;
oheimb@5304
   324
oheimb@2633
   325
paulson@3910
   326
(*intuitionistic simprules only*)
wenzelm@9713
   327
val IFOL_ss =
wenzelm@9713
   328
    FOL_basic_ss addsimps (meta_simps @ IFOL_simps @
wenzelm@9713
   329
                           int_ex_simps @ int_all_simps)
paulson@5496
   330
                 addcongs [imp_cong];
paulson@2074
   331
wenzelm@9713
   332
val cla_simps =
paulson@3910
   333
    [de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2,
paulson@3910
   334
     not_all, not_ex, cases_simp] @
paulson@2074
   335
    map prove_fun
paulson@2074
   336
     ["~(P&Q)  <-> ~P | ~Q",
paulson@2074
   337
      "P | ~P",             "~P | P",
paulson@2074
   338
      "~ ~ P <-> P",        "(~P --> P) <-> P",
paulson@2074
   339
      "(~P <-> ~Q) <-> (P<->Q)"];
paulson@2074
   340
paulson@3910
   341
(*classical simprules too*)
paulson@4349
   342
val FOL_ss = IFOL_ss addsimps (cla_simps @ cla_ex_simps @ cla_all_simps);
paulson@2074
   343
wenzelm@7355
   344
val simpsetup = [fn thy => (simpset_ref_of thy := FOL_ss; thy)];
oheimb@2633
   345
oheimb@2633
   346
wenzelm@5219
   347
(*** integration of simplifier with classical reasoner ***)
oheimb@2633
   348
wenzelm@5219
   349
structure Clasimp = ClasimpFun
wenzelm@8472
   350
 (structure Simplifier = Simplifier and Splitter = Splitter
wenzelm@9851
   351
  and Classical  = Cla and Blast = Blast
wenzelm@9851
   352
  val dest_Trueprop = FOLogic.dest_Trueprop
wenzelm@9851
   353
  val iff_const = FOLogic.iff val not_const = FOLogic.not
wenzelm@9851
   354
  val notE = notE val iffD1 = iffD1 val iffD2 = iffD2
wenzelm@9851
   355
  val cla_make_elim = cla_make_elim);
oheimb@4652
   356
open Clasimp;
oheimb@2633
   357
oheimb@2633
   358
val FOL_css = (FOL_cs, FOL_ss);
wenzelm@9889
   359
wenzelm@9889
   360
wenzelm@9889
   361
(* rulify setup *)
wenzelm@9889
   362
wenzelm@9889
   363
local
wenzelm@9889
   364
  val ss = FOL_basic_ss addsimps (Drule.norm_hhf_eq :: map Thm.symmetric (thms "atomize"));
wenzelm@9889
   365
in
wenzelm@9889
   366
wenzelm@9889
   367
structure Rulify = RulifyFun
wenzelm@9889
   368
 (val make_meta = Simplifier.simplify ss
wenzelm@9889
   369
  val full_make_meta = Simplifier.full_simplify ss);
wenzelm@9889
   370
wenzelm@9889
   371
structure BasicRulify: BASIC_RULIFY = Rulify;
wenzelm@9889
   372
open BasicRulify;
wenzelm@9889
   373
wenzelm@9889
   374
end;