src/Sequents/simpdata.ML
author nipkow
Tue Sep 21 19:11:07 1999 +0200 (1999-09-21)
changeset 7570 a9391550eea1
parent 7123 4ab38de3fd20
child 9259 103acc345f75
permissions -rw-r--r--
Mod because of new solver interface.
     1 (*  Title:      Sequents/simpdata.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson
     4     Copyright   1999  University of Cambridge
     5 
     6 Instantiation of the generic simplifier for LK
     7 
     8 Borrows from the DC simplifier of Soren Heilmann.
     9 *)
    10 
    11 (*** Rewrite rules ***)
    12 
    13 fun prove_fun s = 
    14  (writeln s;  
    15   prove_goal LK.thy s
    16    (fn prems => [ (cut_facts_tac prems 1), 
    17                   (fast_tac (pack() add_safes [subst]) 1) ]));
    18 
    19 val conj_simps = map prove_fun
    20  ["|- P & True <-> P",      "|- True & P <-> P",
    21   "|- P & False <-> False", "|- False & P <-> False",
    22   "|- P & P <-> P", "        |- P & P & Q <-> P & Q",
    23   "|- P & ~P <-> False",    "|- ~P & P <-> False",
    24   "|- (P & Q) & R <-> P & (Q & R)"];
    25 
    26 val disj_simps = map prove_fun
    27  ["|- P | True <-> True",  "|- True | P <-> True",
    28   "|- P | False <-> P",    "|- False | P <-> P",
    29   "|- P | P <-> P",        "|- P | P | Q <-> P | Q",
    30   "|- (P | Q) | R <-> P | (Q | R)"];
    31 
    32 val not_simps = map prove_fun
    33  ["|- ~ False <-> True",   "|- ~ True <-> False"];
    34 
    35 val imp_simps = map prove_fun
    36  ["|- (P --> False) <-> ~P",       "|- (P --> True) <-> True",
    37   "|- (False --> P) <-> True",     "|- (True --> P) <-> P", 
    38   "|- (P --> P) <-> True",         "|- (P --> ~P) <-> ~P"];
    39 
    40 val iff_simps = map prove_fun
    41  ["|- (True <-> P) <-> P",         "|- (P <-> True) <-> P",
    42   "|- (P <-> P) <-> True",
    43   "|- (False <-> P) <-> ~P",       "|- (P <-> False) <-> ~P"];
    44 
    45 
    46 val quant_simps = map prove_fun
    47  ["|- (ALL x. P) <-> P",   
    48   "|- (ALL x. x=t --> P(x)) <-> P(t)",
    49   "|- (ALL x. t=x --> P(x)) <-> P(t)",
    50   "|- (EX x. P) <-> P",
    51   "|- (EX x. x=t & P(x)) <-> P(t)", 
    52   "|- (EX x. t=x & P(x)) <-> P(t)"];
    53 
    54 (*** Miniscoping: pushing quantifiers in
    55      We do NOT distribute of ALL over &, or dually that of EX over |
    56      Baaz and Leitsch, On Skolemization and Proof Complexity (1994) 
    57      show that this step can increase proof length!
    58 ***)
    59 
    60 (*existential miniscoping*)
    61 val ex_simps = map prove_fun 
    62                    ["|- (EX x. P(x) & Q) <-> (EX x. P(x)) & Q",
    63 		    "|- (EX x. P & Q(x)) <-> P & (EX x. Q(x))",
    64 		    "|- (EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
    65 		    "|- (EX x. P | Q(x)) <-> P | (EX x. Q(x))",
    66 		    "|- (EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q",
    67 		    "|- (EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"];
    68 
    69 (*universal miniscoping*)
    70 val all_simps = map prove_fun
    71                     ["|- (ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q",
    72 		     "|- (ALL x. P & Q(x)) <-> P & (ALL x. Q(x))",
    73 		     "|- (ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q",
    74 		     "|- (ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))",
    75 		     "|- (ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q",
    76 		     "|- (ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"];
    77 
    78 (*These are NOT supplied by default!*)
    79 val distrib_simps  = map prove_fun
    80  ["|- P & (Q | R) <-> P&Q | P&R", 
    81   "|- (Q | R) & P <-> Q&P | R&P",
    82   "|- (P | Q --> R) <-> (P --> R) & (Q --> R)"];
    83 
    84 (** Conversion into rewrite rules **)
    85 
    86 fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
    87 
    88 
    89 (*Make atomic rewrite rules*)
    90 fun atomize r =
    91  case concl_of r of
    92    Const("Trueprop",_) $ Abs(_,_,a) $ Abs(_,_,c) =>
    93      (case (forms_of_seq a, forms_of_seq c) of
    94 	([], [p]) =>
    95 	  (case p of
    96 	       Const("op -->",_)$_$_ => atomize(r RS mp_R)
    97 	     | Const("op &",_)$_$_   => atomize(r RS conjunct1) @
    98 		   atomize(r RS conjunct2)
    99 	     | Const("All",_)$_      => atomize(r RS spec)
   100 	     | Const("True",_)       => []    (*True is DELETED*)
   101 	     | Const("False",_)      => []    (*should False do something?*)
   102 	     | _                     => [r])
   103       | _ => [])  (*ignore theorem unless it has precisely one conclusion*)
   104  | _ => [r];
   105 
   106 
   107 qed_goal "P_iff_F" LK.thy "|- ~P ==> |- (P <-> False)"
   108     (fn prems => [lemma_tac (hd prems) 1, fast_tac LK_pack 1]);
   109 val iff_reflection_F = P_iff_F RS iff_reflection;
   110 
   111 qed_goal "P_iff_T" LK.thy "|- P ==> |- (P <-> True)"
   112     (fn prems => [lemma_tac (hd prems) 1, fast_tac LK_pack 1]);
   113 val iff_reflection_T = P_iff_T RS iff_reflection;
   114 
   115 (*Make meta-equalities.*)
   116 fun mk_meta_eq th = case concl_of th of
   117     Const("==",_)$_$_           => th
   118   | Const("Trueprop",_) $ Abs(_,_,a) $ Abs(_,_,c) =>
   119 	(case (forms_of_seq a, forms_of_seq c) of
   120 	     ([], [p]) => 
   121 		 (case p of
   122 		      (Const("op =",_)$_$_)   => th RS eq_reflection
   123 		    | (Const("op <->",_)$_$_) => th RS iff_reflection
   124 		    | (Const("Not",_)$_)      => th RS iff_reflection_F
   125 		    | _                       => th RS iff_reflection_T)
   126 	   | _ => error ("addsimps: unable to use theorem\n" ^
   127 			 string_of_thm th));
   128 
   129 
   130 (*Replace premises x=y, X<->Y by X==Y*)
   131 val mk_meta_prems = 
   132     rule_by_tactic 
   133       (REPEAT_FIRST (resolve_tac [meta_eq_to_obj_eq, def_imp_iff]));
   134 
   135 fun mk_meta_cong rl =
   136   standard(mk_meta_eq (mk_meta_prems rl))
   137   handle THM _ =>
   138   error("Premises and conclusion of congruence rules must use =-equality or <->");
   139 
   140 
   141 (*** Named rewrite rules ***)
   142 
   143 fun prove nm thm  = qed_goal nm LK.thy thm
   144     (fn prems => [ (cut_facts_tac prems 1), 
   145                    (fast_tac LK_pack 1) ]);
   146 
   147 prove "conj_commute" "|- P&Q <-> Q&P";
   148 prove "conj_left_commute" "|- P&(Q&R) <-> Q&(P&R)";
   149 val conj_comms = [conj_commute, conj_left_commute];
   150 
   151 prove "disj_commute" "|- P|Q <-> Q|P";
   152 prove "disj_left_commute" "|- P|(Q|R) <-> Q|(P|R)";
   153 val disj_comms = [disj_commute, disj_left_commute];
   154 
   155 prove "conj_disj_distribL" "|- P&(Q|R) <-> (P&Q | P&R)";
   156 prove "conj_disj_distribR" "|- (P|Q)&R <-> (P&R | Q&R)";
   157 
   158 prove "disj_conj_distribL" "|- P|(Q&R) <-> (P|Q) & (P|R)";
   159 prove "disj_conj_distribR" "|- (P&Q)|R <-> (P|R) & (Q|R)";
   160 
   161 prove "imp_conj_distrib" "|- (P --> (Q&R)) <-> (P-->Q) & (P-->R)";
   162 prove "imp_conj"         "|- ((P&Q)-->R)   <-> (P --> (Q --> R))";
   163 prove "imp_disj"         "|- (P|Q --> R)   <-> (P-->R) & (Q-->R)";
   164 
   165 prove "imp_disj1" "|- (P-->Q) | R <-> (P-->Q | R)";
   166 prove "imp_disj2" "|- Q | (P-->R) <-> (P-->Q | R)";
   167 
   168 prove "de_Morgan_disj" "|- (~(P | Q)) <-> (~P & ~Q)";
   169 prove "de_Morgan_conj" "|- (~(P & Q)) <-> (~P | ~Q)";
   170 
   171 prove "not_iff" "|- ~(P <-> Q) <-> (P <-> ~Q)";
   172 
   173 
   174 val [p1,p2] = Goal 
   175     "[| |- P <-> P';  |- P' ==> |- Q <-> Q' |] ==> |- (P-->Q) <-> (P'-->Q')";
   176 by (lemma_tac p1 1);
   177 by (Safe_tac 1);
   178 by (REPEAT (rtac cut 1 
   179 	    THEN
   180 	    DEPTH_SOLVE_1 (resolve_tac [thinL, thinR, p2 COMP monotonic] 1)
   181 	    THEN
   182 	    Safe_tac 1));
   183 qed "imp_cong";
   184 
   185 val [p1,p2] = Goal 
   186     "[| |- P <-> P';  |- P' ==> |- Q <-> Q' |] ==> |- (P&Q) <-> (P'&Q')";
   187 by (lemma_tac p1 1);
   188 by (Safe_tac 1);
   189 by (REPEAT (rtac cut 1 
   190 	    THEN
   191 	    DEPTH_SOLVE_1 (resolve_tac [thinL, thinR, p2 COMP monotonic] 1)
   192 	    THEN
   193 	    Safe_tac 1));
   194 qed "conj_cong";
   195 
   196 Goal "|- (x=y) <-> (y=x)";
   197 by (fast_tac (pack() add_safes [subst]) 1);
   198 qed "eq_sym_conv";
   199 
   200 
   201 (** if-then-else rules **)
   202 
   203 Goalw [If_def] "|- (if True then x else y) = x";
   204 by (Fast_tac 1);
   205 qed "if_True";
   206 
   207 Goalw [If_def] "|- (if False then x else y) = y";
   208 by (Fast_tac 1);
   209 qed "if_False";
   210 
   211 Goalw [If_def] "|- P ==> |- (if P then x else y) = x";
   212 by (etac (thinR RS cut) 1);
   213 by (Fast_tac 1);
   214 qed "if_P";
   215 
   216 Goalw [If_def] "|- ~P ==> |- (if P then x else y) = y";
   217 by (etac (thinR RS cut) 1);
   218 by (Fast_tac 1);
   219 qed "if_not_P";
   220 
   221 
   222 open Simplifier;
   223 
   224 (*** Standard simpsets ***)
   225 
   226 (*Add congruence rules for = or <-> (instead of ==) *)
   227 infix 4 addcongs delcongs;
   228 fun ss addcongs congs = ss addeqcongs (map mk_meta_cong congs);
   229 fun ss delcongs congs = ss deleqcongs (map mk_meta_cong congs);
   230 
   231 fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
   232 fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
   233 
   234 val triv_rls = [FalseL, TrueR, basic, refl, iff_refl, reflexive_thm];
   235 
   236 fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems),
   237 				 assume_tac];
   238 (*No premature instantiation of variables during simplification*)
   239 fun   safe_solver prems = FIRST'[fn i => DETERM (match_tac (triv_rls@prems) i),
   240 				 eq_assume_tac];
   241 
   242 (*No simprules, but basic infrastructure for simplification*)
   243 val LK_basic_ss = empty_ss setsubgoaler asm_simp_tac
   244 			   setSSolver   (mk_solver "safe" safe_solver)
   245 			   setSolver    (mk_solver "unsafe" unsafe_solver)
   246 			   setmksimps   (map mk_meta_eq o atomize o gen_all);
   247 
   248 val LK_simps =
   249    [triv_forall_equality, (* prunes params *)
   250     refl RS P_iff_T] @ 
   251     conj_simps @ disj_simps @ not_simps @ 
   252     imp_simps @ iff_simps @quant_simps @ all_simps @ ex_simps @
   253     [de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2] @
   254     map prove_fun
   255      ["|- P | ~P",             "|- ~P | P",
   256       "|- ~ ~ P <-> P",        "|- (~P --> P) <-> P",
   257       "|- (~P <-> ~Q) <-> (P<->Q)"];
   258 
   259 val LK_ss = LK_basic_ss addsimps LK_simps addeqcongs [left_cong]
   260 					  addcongs [imp_cong];
   261 
   262 simpset_ref() := LK_ss;
   263 
   264 
   265 (* To create substition rules *)
   266 
   267 qed_goal "eq_imp_subst" LK.thy "|- a=b ==> $H, A(a), $G |- $E, A(b), $F"
   268   (fn prems =>
   269    [cut_facts_tac prems 1,
   270     asm_simp_tac LK_basic_ss 1]);
   271 
   272 Goal "|- P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))";
   273 by (res_inst_tac [ ("P","Q") ] cut 1);
   274 by (simp_tac (simpset() addsimps [if_P]) 2);
   275 by (res_inst_tac [ ("P","~Q") ] cut 1);
   276 by (simp_tac (simpset() addsimps [if_not_P]) 2);
   277 by (Fast_tac 1);
   278 qed "split_if";
   279 
   280 Goal "|- (if P then x else x) = x";
   281 by (lemma_tac split_if 1);
   282 by (Fast_tac 1);
   283 qed "if_cancel";
   284 
   285 Goal "|- (if x=y then y else x) = x";
   286 by (lemma_tac split_if 1);
   287 by (Safe_tac 1);
   288 by (rtac symL 1);
   289 by (rtac basic 1);
   290 qed "if_eq_cancel";
   291 
   292 (*Putting in automatic case splits seems to require a lot of work.*)