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