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