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