src/FOL/simpdata.ML
author nipkow
Tue Mar 18 08:43:26 1997 +0100 (1997-03-18)
changeset 2801 56948cb1a1f9
parent 2727 230f2643107e
child 3206 a3de7f32728c
permissions -rw-r--r--
Added P&P&Q <-> P&Q and P|P|Q <-> P|Q
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@1953
    44
val quant_simps = map int_prove_fun
clasohm@1459
    45
 ["(ALL x.P) <-> P",    "(EX x.P) <-> P"];
clasohm@0
    46
clasohm@0
    47
(*These are NOT supplied by default!*)
paulson@1953
    48
val distrib_simps  = map int_prove_fun
lcp@282
    49
 ["P & (Q | R) <-> P&Q | P&R", 
lcp@282
    50
  "(Q | R) & P <-> Q&P | R&P",
clasohm@0
    51
  "(P | Q --> R) <-> (P --> R) & (Q --> R)"];
clasohm@0
    52
lcp@282
    53
(** Conversion into rewrite rules **)
clasohm@0
    54
nipkow@53
    55
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
nipkow@53
    56
lcp@282
    57
(*Make atomic rewrite rules*)
lcp@429
    58
fun atomize r =
lcp@429
    59
  case concl_of r of
lcp@429
    60
    Const("Trueprop",_) $ p =>
lcp@429
    61
      (case p of
clasohm@1459
    62
         Const("op -->",_)$_$_ => atomize(r RS mp)
lcp@429
    63
       | Const("op &",_)$_$_   => atomize(r RS conjunct1) @
clasohm@1459
    64
                                  atomize(r RS conjunct2)
lcp@429
    65
       | Const("All",_)$_      => atomize(r RS spec)
clasohm@1459
    66
       | Const("True",_)       => []    (*True is DELETED*)
clasohm@1459
    67
       | Const("False",_)      => []    (*should False do something?*)
lcp@429
    68
       | _                     => [r])
lcp@429
    69
  | _ => [r];
lcp@429
    70
lcp@282
    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
lcp@981
    86
paulson@2074
    87
(*** Classical laws ***)
lcp@282
    88
clasohm@0
    89
fun prove_fun s = 
lcp@282
    90
 (writeln s;  
lcp@282
    91
  prove_goal FOL.thy s
lcp@282
    92
   (fn prems => [ (cut_facts_tac prems 1), 
clasohm@1459
    93
                  (Cla.fast_tac FOL_cs 1) ]));
lcp@745
    94
paulson@1953
    95
(*Avoids duplication of subgoals after expand_if, when the true and false 
paulson@1953
    96
  cases boil down to the same thing.*) 
paulson@1953
    97
val cases_simp = prove_fun "(P --> Q) & (~P --> Q) <-> Q";
paulson@1953
    98
paulson@1953
    99
(*At present, miniscoping is for classical logic only.  We do NOT include
paulson@1953
   100
  distribution of ALL over &, or dually that of EX over |.*)
clasohm@0
   101
paulson@1953
   102
(*Miniscoping: pushing in existential quantifiers*)
paulson@1953
   103
val ex_simps = map prove_fun 
paulson@2065
   104
                ["(EX x. x=t & P(x)) <-> P(t)",
paulson@2065
   105
                 "(EX x. t=x & P(x)) <-> P(t)",
paulson@2065
   106
                 "(EX x. P(x) & Q) <-> (EX x.P(x)) & Q",
paulson@1953
   107
                 "(EX x. P & Q(x)) <-> P & (EX x.Q(x))",
paulson@1953
   108
                 "(EX x. P(x) | Q) <-> (EX x.P(x)) | Q",
paulson@1953
   109
                 "(EX x. P | Q(x)) <-> P | (EX x.Q(x))",
paulson@1953
   110
                 "(EX x. P(x) --> Q) <-> (ALL x.P(x)) --> Q",
paulson@1953
   111
                 "(EX x. P --> Q(x)) <-> P --> (EX x.Q(x))"];
paulson@1953
   112
paulson@1953
   113
(*Miniscoping: pushing in universal quantifiers*)
paulson@1953
   114
val all_simps = map prove_fun
paulson@2065
   115
                ["(ALL x. x=t --> P(x)) <-> P(t)",
paulson@2065
   116
                 "(ALL x. t=x --> P(x)) <-> P(t)",
paulson@2065
   117
                 "(ALL x. P(x) & Q) <-> (ALL x.P(x)) & Q",
paulson@1953
   118
                 "(ALL x. P & Q(x)) <-> P & (ALL x.Q(x))",
paulson@1953
   119
                 "(ALL x. P(x) | Q) <-> (ALL x.P(x)) | Q",
paulson@1953
   120
                 "(ALL x. P | Q(x)) <-> P | (ALL x.Q(x))",
paulson@1953
   121
                 "(ALL x. P(x) --> Q) <-> (EX x.P(x)) --> Q",
paulson@1953
   122
                 "(ALL x. P --> Q(x)) <-> P --> (ALL x.Q(x))"];
paulson@1953
   123
paulson@1914
   124
fun int_prove nm thm  = qed_goal nm IFOL.thy thm
paulson@1914
   125
    (fn prems => [ (cut_facts_tac prems 1), 
paulson@2601
   126
                   (IntPr.fast_tac 1) ]);
paulson@1914
   127
paulson@1914
   128
fun prove nm thm  = qed_goal nm FOL.thy thm (fn _ => [fast_tac FOL_cs 1]);
paulson@1914
   129
paulson@1914
   130
int_prove "conj_commute" "P&Q <-> Q&P";
paulson@1914
   131
int_prove "conj_left_commute" "P&(Q&R) <-> Q&(P&R)";
paulson@1914
   132
val conj_comms = [conj_commute, conj_left_commute];
paulson@1914
   133
paulson@1914
   134
int_prove "disj_commute" "P|Q <-> Q|P";
paulson@1914
   135
int_prove "disj_left_commute" "P|(Q|R) <-> Q|(P|R)";
paulson@1914
   136
val disj_comms = [disj_commute, disj_left_commute];
paulson@1914
   137
paulson@1914
   138
int_prove "conj_disj_distribL" "P&(Q|R) <-> (P&Q | P&R)";
paulson@1914
   139
int_prove "conj_disj_distribR" "(P|Q)&R <-> (P&R | Q&R)";
paulson@1914
   140
paulson@1914
   141
int_prove "disj_conj_distribL" "P|(Q&R) <-> (P|Q) & (P|R)";
paulson@1914
   142
int_prove "disj_conj_distribR" "(P&Q)|R <-> (P|R) & (Q|R)";
paulson@1914
   143
paulson@1914
   144
int_prove "imp_conj_distrib" "(P --> (Q&R)) <-> (P-->Q) & (P-->R)";
paulson@1914
   145
int_prove "imp_conj"         "((P&Q)-->R)   <-> (P --> (Q --> R))";
paulson@1914
   146
int_prove "imp_disj"         "(P|Q --> R)   <-> (P-->R) & (Q-->R)";
paulson@1914
   147
paulson@1914
   148
int_prove "de_Morgan_disj" "(~(P | Q)) <-> (~P & ~Q)";
paulson@1914
   149
prove     "de_Morgan_conj" "(~(P & Q)) <-> (~P | ~Q)";
paulson@1914
   150
paulson@1914
   151
prove     "not_iff" "~(P <-> Q) <-> (P <-> ~Q)";
paulson@1914
   152
paulson@1914
   153
prove     "not_all" "(~ (ALL x.P(x))) <-> (EX x.~P(x))";
paulson@1914
   154
prove     "imp_all" "((ALL x.P(x)) --> Q) <-> (EX x.P(x) --> Q)";
paulson@1914
   155
int_prove "not_ex"  "(~ (EX x.P(x))) <-> (ALL x.~P(x))";
paulson@1914
   156
int_prove "imp_ex" "((EX x. P(x)) --> Q) <-> (ALL x. P(x) --> Q)";
paulson@1914
   157
paulson@1914
   158
int_prove "ex_disj_distrib"
paulson@1914
   159
    "(EX x. P(x) | Q(x)) <-> ((EX x. P(x)) | (EX x. Q(x)))";
paulson@1914
   160
int_prove "all_conj_distrib"
paulson@1914
   161
    "(ALL x. P(x) & Q(x)) <-> ((ALL x. P(x)) & (ALL x. Q(x)))";
paulson@1914
   162
paulson@1914
   163
lcp@1088
   164
(*Used in ZF, perhaps elsewhere?*)
lcp@1088
   165
val meta_eq_to_obj_eq = prove_goal IFOL.thy "x==y ==> x=y"
lcp@1088
   166
  (fn [prem] => [rewtac prem, rtac refl 1]);
lcp@1088
   167
clasohm@0
   168
(*** case splitting ***)
clasohm@0
   169
lcp@1088
   170
qed_goal "meta_iffD" IFOL.thy "[| P==Q; Q |] ==> P"
clasohm@756
   171
        (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]);
lcp@282
   172
nipkow@942
   173
local val mktac = mk_case_split_tac meta_iffD
nipkow@942
   174
in
nipkow@942
   175
fun split_tac splits = mktac (map mk_meta_eq splits)
nipkow@942
   176
end;
berghofe@1722
   177
berghofe@1722
   178
local val mktac = mk_case_split_inside_tac meta_iffD
berghofe@1722
   179
in
berghofe@1722
   180
fun split_inside_tac splits = mktac (map mk_meta_eq splits)
berghofe@1722
   181
end;
berghofe@1722
   182
berghofe@1722
   183
paulson@2074
   184
(*** Standard simpsets ***)
paulson@2074
   185
paulson@2074
   186
structure Induction = InductionFun(struct val spec=IFOL.spec end);
paulson@2074
   187
paulson@2074
   188
open Simplifier Induction;
paulson@2074
   189
paulson@2074
   190
(*Add congruence rules for = or <-> (instead of ==) *)
oheimb@2633
   191
infix 4 addcongs delcongs;
paulson@2074
   192
fun ss addcongs congs =
paulson@2469
   193
        ss addeqcongs (congs RL [eq_reflection,iff_reflection]);
oheimb@2633
   194
fun ss delcongs congs =
oheimb@2633
   195
        ss deleqcongs (congs RL [eq_reflection,iff_reflection]);
paulson@2469
   196
paulson@2469
   197
fun Addcongs congs = (simpset := !simpset addcongs congs);
oheimb@2633
   198
fun Delcongs congs = (simpset := !simpset delcongs congs);
paulson@2074
   199
paulson@2074
   200
val IFOL_simps =
paulson@2074
   201
   [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
paulson@2074
   202
    imp_simps @ iff_simps @ quant_simps;
paulson@2074
   203
paulson@2074
   204
val notFalseI = int_prove_fun "~False";
paulson@2074
   205
val triv_rls = [TrueI,refl,iff_refl,notFalseI];
paulson@2074
   206
oheimb@2633
   207
fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems),
oheimb@2633
   208
				 atac, etac FalseE];
oheimb@2633
   209
(*No premature instantiation of variables during simplification*)
oheimb@2633
   210
fun   safe_solver prems = FIRST'[match_tac (triv_rls@prems),
oheimb@2633
   211
				 eq_assume_tac, ematch_tac [FalseE]];
oheimb@2633
   212
oheimb@2633
   213
val FOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
oheimb@2633
   214
			    setSSolver   safe_solver
oheimb@2633
   215
			    setSolver  unsafe_solver
oheimb@2633
   216
			    setmksimps (map mk_meta_eq o atomize o gen_all);
oheimb@2633
   217
oheimb@2633
   218
val IFOL_ss = FOL_basic_ss addsimps IFOL_simps
oheimb@2633
   219
			   addcongs [imp_cong];
paulson@2074
   220
paulson@2074
   221
val cla_simps = 
paulson@2074
   222
    [de_Morgan_conj, de_Morgan_disj, not_all, not_ex, cases_simp] @
paulson@2074
   223
    map prove_fun
paulson@2074
   224
     ["~(P&Q)  <-> ~P | ~Q",
paulson@2074
   225
      "P | ~P",             "~P | P",
paulson@2074
   226
      "~ ~ P <-> P",        "(~P --> P) <-> P",
paulson@2074
   227
      "(~P <-> ~Q) <-> (P<->Q)"];
paulson@2074
   228
paulson@2074
   229
val FOL_ss = IFOL_ss addsimps (cla_simps @ ex_simps @ all_simps);
paulson@2074
   230
paulson@2469
   231
paulson@2469
   232
paulson@2469
   233
(*** Install simpsets and datatypes in theory structure ***)
paulson@2469
   234
paulson@2469
   235
simpset := FOL_ss;
paulson@2469
   236
paulson@2469
   237
exception SS_DATA of simpset;
paulson@2469
   238
paulson@2469
   239
let fun merge [] = SS_DATA empty_ss
paulson@2469
   240
      | merge ss = let val ss = map (fn SS_DATA x => x) ss;
paulson@2469
   241
                   in SS_DATA (foldl merge_ss (hd ss, tl ss)) end;
paulson@2469
   242
paulson@2469
   243
    fun put (SS_DATA ss) = simpset := ss;
paulson@2469
   244
paulson@2469
   245
    fun get () = SS_DATA (!simpset);
paulson@2469
   246
in add_thydata "FOL"
paulson@2469
   247
     ("simpset", ThyMethods {merge = merge, put = put, get = get})
paulson@2469
   248
end;
paulson@2469
   249
paulson@2469
   250
paulson@2469
   251
add_thy_reader_file "thy_data.ML";
oheimb@2633
   252
oheimb@2633
   253
oheimb@2633
   254
oheimb@2633
   255
oheimb@2633
   256
(*** Integration of simplifier with classical reasoner ***)
oheimb@2633
   257
oheimb@2633
   258
(* rot_eq_tac rotates the first equality premise of subgoal i to the front,
oheimb@2633
   259
   fails if there is no equaliy or if an equality is already at the front *)
oheimb@2633
   260
fun rot_eq_tac i = let
oheimb@2633
   261
  fun is_eq (Const ("Trueprop", _) $ (Const("op ="  ,_) $ _ $ _)) = true
oheimb@2633
   262
  |   is_eq (Const ("Trueprop", _) $ (Const("op <->",_) $ _ $ _)) = true
oheimb@2633
   263
  |   is_eq _ = false;
oheimb@2633
   264
  fun find_eq n [] = None
oheimb@2633
   265
  |   find_eq n (t :: ts) = if (is_eq t) then Some n else find_eq (n + 1) ts;
oheimb@2633
   266
  fun rot_eq state = let val (_, _, Bi, _) = dest_state (state, i) in
oheimb@2633
   267
	    (case find_eq 0 (Logic.strip_assums_hyp Bi) of
oheimb@2633
   268
	      None   => no_tac
oheimb@2633
   269
	    | Some 0 => no_tac
oheimb@2633
   270
	    | Some n => rotate_tac n i) end;
oheimb@2633
   271
in STATE rot_eq end;
oheimb@2633
   272
oheimb@2633
   273
oheimb@2633
   274
fun safe_asm_more_full_simp_tac ss = TRY o rot_eq_tac THEN' 
oheimb@2633
   275
				     safe_asm_full_simp_tac ss;
oheimb@2633
   276
(*an unsatisfactory fix for the incomplete asm_full_simp_tac!
oheimb@2633
   277
  better: asm_really_full_simp_tac, a yet to be implemented version of
oheimb@2633
   278
			asm_full_simp_tac that applies all equalities in the
oheimb@2633
   279
			premises to all the premises *)
oheimb@2633
   280
oheimb@2633
   281
(*Add a simpset to a classical set!*)
oheimb@2633
   282
infix 4 addss;
oheimb@2633
   283
fun cs addss ss = cs addSaltern (CHANGED o (safe_asm_more_full_simp_tac ss));
oheimb@2633
   284
oheimb@2633
   285
(*old version, for compatibility with unstable old proofs*)
oheimb@2633
   286
infix 4 unsafe_addss;
oheimb@2633
   287
fun cs unsafe_addss ss = cs addbefore asm_full_simp_tac ss;
oheimb@2633
   288
oheimb@2633
   289
fun Addss ss = (claset := !claset addss ss);
oheimb@2633
   290
oheimb@2633
   291
(*Designed to be idempotent, except if best_tac instantiates variables
oheimb@2633
   292
  in some of the subgoals*)
oheimb@2633
   293
(*old version, for compatibility with unstable old proofs*)
oheimb@2633
   294
fun unsafe_auto_tac (cs,ss) = 
oheimb@2633
   295
    ALLGOALS (asm_full_simp_tac ss) THEN
oheimb@2633
   296
    REPEAT (safe_tac cs THEN ALLGOALS (asm_full_simp_tac ss)) THEN
oheimb@2633
   297
    REPEAT (FIRSTGOAL (best_tac (cs addss ss))) THEN
oheimb@2633
   298
    prune_params_tac;
oheimb@2633
   299
oheimb@2633
   300
type clasimpset = (claset * simpset);
oheimb@2633
   301
oheimb@2633
   302
val FOL_css = (FOL_cs, FOL_ss);
oheimb@2633
   303
oheimb@2633
   304
fun pair_upd1 f ((a,b),x) = (f(a,x), b);
oheimb@2633
   305
fun pair_upd2 f ((a,b),x) = (a, f(b,x));
oheimb@2633
   306
oheimb@2633
   307
infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2
oheimb@2633
   308
	addsimps2 delsimps2 addcongs2 delcongs2;
paulson@2727
   309
fun op addSIs2   arg = pair_upd1 (op addSIs) arg;
paulson@2727
   310
fun op addSEs2   arg = pair_upd1 (op addSEs) arg;
paulson@2727
   311
fun op addSDs2   arg = pair_upd1 (op addSDs) arg;
paulson@2727
   312
fun op addIs2    arg = pair_upd1 (op addIs ) arg;
paulson@2727
   313
fun op addEs2    arg = pair_upd1 (op addEs ) arg;
paulson@2727
   314
fun op addDs2    arg = pair_upd1 (op addDs ) arg;
paulson@2727
   315
fun op addsimps2 arg = pair_upd2 (op addsimps) arg;
paulson@2727
   316
fun op delsimps2 arg = pair_upd2 (op delsimps) arg;
paulson@2727
   317
fun op addcongs2 arg = pair_upd2 (op addcongs) arg;
paulson@2727
   318
fun op delcongs2 arg = pair_upd2 (op delcongs) arg;
oheimb@2633
   319
oheimb@2633
   320
fun auto_tac (cs,ss) = let val cs' = cs addss ss in
oheimb@2633
   321
EVERY [	TRY (safe_tac cs'),
oheimb@2633
   322
	REPEAT (FIRSTGOAL (fast_tac cs')),
oheimb@2633
   323
	prune_params_tac] end;
oheimb@2633
   324
oheimb@2633
   325
fun Auto_tac () = auto_tac (!claset, !simpset);
oheimb@2633
   326
oheimb@2633
   327
fun auto () = by (Auto_tac ());