src/FOL/simpdata.ML
author paulson
Thu Sep 05 18:28:01 1996 +0200 (1996-09-05)
changeset 1953 832ccc1dba95
parent 1914 86b095835de9
child 1961 d33a5d59a29a
permissions -rw-r--r--
Introduction of miniscoping for FOL
     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                   (Int.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 structure Induction = InductionFun(struct val spec=IFOL.spec end);
    87 
    88 open Simplifier Induction;
    89 
    90 (*Add congruence rules for = or <-> (instead of ==) *)
    91 infix 4 addcongs;
    92 fun ss addcongs congs =
    93     ss addeqcongs (congs RL [eq_reflection,iff_reflection]);
    94 
    95 (*Add a simpset to a classical set!*)
    96 infix 4 addss;
    97 fun cs addss ss = cs addbefore asm_full_simp_tac ss 1;
    98 
    99 
   100 val IFOL_simps =
   101    [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
   102     imp_simps @ iff_simps @ quant_simps;
   103 
   104 val notFalseI = int_prove_fun "~False";
   105 val triv_rls = [TrueI,refl,iff_refl,notFalseI];
   106 
   107 val IFOL_ss = 
   108   empty_ss 
   109   setmksimps (map mk_meta_eq o atomize o gen_all)
   110   setsolver  (fn prems => resolve_tac (triv_rls@prems) 
   111                           ORELSE' assume_tac
   112                           ORELSE' etac FalseE)
   113   setsubgoaler asm_simp_tac
   114   addsimps IFOL_simps
   115   addcongs [imp_cong];
   116 
   117 (*Classical version...*)
   118 fun prove_fun s = 
   119  (writeln s;  
   120   prove_goal FOL.thy s
   121    (fn prems => [ (cut_facts_tac prems 1), 
   122                   (Cla.fast_tac FOL_cs 1) ]));
   123 
   124 (*Avoids duplication of subgoals after expand_if, when the true and false 
   125   cases boil down to the same thing.*) 
   126 val cases_simp = prove_fun "(P --> Q) & (~P --> Q) <-> Q";
   127 
   128 val cla_simps = 
   129     cases_simp::
   130     map prove_fun
   131      ["~(P&Q)  <-> ~P | ~Q",
   132       "P | ~P",             "~P | P",
   133       "~ ~ P <-> P",        "(~P --> P) <-> P",
   134       "(~P <-> ~Q) <-> (P<->Q)"];
   135 
   136 (*At present, miniscoping is for classical logic only.  We do NOT include
   137   distribution of ALL over &, or dually that of EX over |.*)
   138 
   139 (*Miniscoping: pushing in existential quantifiers*)
   140 val ex_simps = map prove_fun 
   141                 ["(EX x. P) <-> P",
   142                  "(EX x. P(x) & Q) <-> (EX x.P(x)) & Q",
   143                  "(EX x. P & Q(x)) <-> P & (EX x.Q(x))",
   144                  "(EX x. P(x) | Q) <-> (EX x.P(x)) | Q",
   145                  "(EX x. P | Q(x)) <-> P | (EX x.Q(x))",
   146                  "(EX x. P(x) --> Q) <-> (ALL x.P(x)) --> Q",
   147                  "(EX x. P --> Q(x)) <-> P --> (EX x.Q(x))"];
   148 
   149 (*Miniscoping: pushing in universal quantifiers*)
   150 val all_simps = map prove_fun
   151                 ["(ALL x. P) <-> P",
   152                  "(ALL x. P(x) & Q) <-> (ALL x.P(x)) & Q",
   153                  "(ALL x. P & Q(x)) <-> P & (ALL x.Q(x))",
   154                  "(ALL x. P(x) | Q) <-> (ALL x.P(x)) | Q",
   155                  "(ALL x. P | Q(x)) <-> P | (ALL x.Q(x))",
   156                  "(ALL x. P(x) --> Q) <-> (EX x.P(x)) --> Q",
   157                  "(ALL x. P --> Q(x)) <-> P --> (ALL x.Q(x))"];
   158 
   159 val FOL_ss = IFOL_ss addsimps (cla_simps @ ex_simps @ all_simps);
   160 
   161 fun int_prove nm thm  = qed_goal nm IFOL.thy thm
   162     (fn prems => [ (cut_facts_tac prems 1), 
   163                    (Int.fast_tac 1) ]);
   164 
   165 fun prove nm thm  = qed_goal nm FOL.thy thm (fn _ => [fast_tac FOL_cs 1]);
   166 
   167 int_prove "conj_commute" "P&Q <-> Q&P";
   168 int_prove "conj_left_commute" "P&(Q&R) <-> Q&(P&R)";
   169 val conj_comms = [conj_commute, conj_left_commute];
   170 
   171 int_prove "disj_commute" "P|Q <-> Q|P";
   172 int_prove "disj_left_commute" "P|(Q|R) <-> Q|(P|R)";
   173 val disj_comms = [disj_commute, disj_left_commute];
   174 
   175 int_prove "conj_disj_distribL" "P&(Q|R) <-> (P&Q | P&R)";
   176 int_prove "conj_disj_distribR" "(P|Q)&R <-> (P&R | Q&R)";
   177 
   178 int_prove "disj_conj_distribL" "P|(Q&R) <-> (P|Q) & (P|R)";
   179 int_prove "disj_conj_distribR" "(P&Q)|R <-> (P|R) & (Q|R)";
   180 
   181 int_prove "imp_conj_distrib" "(P --> (Q&R)) <-> (P-->Q) & (P-->R)";
   182 int_prove "imp_conj"         "((P&Q)-->R)   <-> (P --> (Q --> R))";
   183 int_prove "imp_disj"         "(P|Q --> R)   <-> (P-->R) & (Q-->R)";
   184 
   185 int_prove "de_Morgan_disj" "(~(P | Q)) <-> (~P & ~Q)";
   186 prove     "de_Morgan_conj" "(~(P & Q)) <-> (~P | ~Q)";
   187 
   188 prove     "not_iff" "~(P <-> Q) <-> (P <-> ~Q)";
   189 
   190 prove     "not_all" "(~ (ALL x.P(x))) <-> (EX x.~P(x))";
   191 prove     "imp_all" "((ALL x.P(x)) --> Q) <-> (EX x.P(x) --> Q)";
   192 int_prove "not_ex"  "(~ (EX x.P(x))) <-> (ALL x.~P(x))";
   193 int_prove "imp_ex" "((EX x. P(x)) --> Q) <-> (ALL x. P(x) --> Q)";
   194 
   195 int_prove "ex_disj_distrib"
   196     "(EX x. P(x) | Q(x)) <-> ((EX x. P(x)) | (EX x. Q(x)))";
   197 int_prove "all_conj_distrib"
   198     "(ALL x. P(x) & Q(x)) <-> ((ALL x. P(x)) & (ALL x. Q(x)))";
   199 
   200 
   201 (*Used in ZF, perhaps elsewhere?*)
   202 val meta_eq_to_obj_eq = prove_goal IFOL.thy "x==y ==> x=y"
   203   (fn [prem] => [rewtac prem, rtac refl 1]);
   204 
   205 (*** case splitting ***)
   206 
   207 qed_goal "meta_iffD" IFOL.thy "[| P==Q; Q |] ==> P"
   208         (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]);
   209 
   210 local val mktac = mk_case_split_tac meta_iffD
   211 in
   212 fun split_tac splits = mktac (map mk_meta_eq splits)
   213 end;
   214 
   215 local val mktac = mk_case_split_inside_tac meta_iffD
   216 in
   217 fun split_inside_tac splits = mktac (map mk_meta_eq splits)
   218 end;
   219 
   220