src/FOLP/simpdata.ML
author haftmann
Tue Sep 20 08:21:49 2005 +0200 (2005-09-20)
changeset 17496 26535df536ae
parent 17480 fd19f77dcf60
child 26322 eaf634e975fa
permissions -rw-r--r--
slight adaptions to library changes
     1 (*  Title:      FOLP/simpdata.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     5 
     6 Simplification data for FOLP.
     7 *)
     8 
     9 (*** Rewrite rules ***)
    10 
    11 fun int_prove_fun_raw s =
    12     (writeln s;  prove_goal (the_context ()) s
    13        (fn prems => [ (cut_facts_tac prems 1), (IntPr.fast_tac 1) ]));
    14 
    15 fun int_prove_fun s = int_prove_fun_raw ("?p : "^s);
    16 
    17 val conj_rews = 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_rews = 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_rews = map int_prove_fun
    31  ["~ False <-> True",   "~ True <-> False"];
    32 
    33 val imp_rews = map int_prove_fun
    34  ["(P --> False) <-> ~P",       "(P --> True) <-> True",
    35   "(False --> P) <-> True",     "(True --> P) <-> P",
    36   "(P --> P) <-> True",         "(P --> ~P) <-> ~P"];
    37 
    38 val iff_rews = map int_prove_fun
    39  ["(True <-> P) <-> P",         "(P <-> True) <-> P",
    40   "(P <-> P) <-> True",
    41   "(False <-> P) <-> ~P",       "(P <-> False) <-> ~P"];
    42 
    43 val quant_rews = map int_prove_fun
    44  ["(ALL x. P) <-> P",    "(EX x. P) <-> P"];
    45 
    46 (*These are NOT supplied by default!*)
    47 val distrib_rews  = map int_prove_fun
    48  ["~(P|Q) <-> ~P & ~Q",
    49   "P & (Q | R) <-> P&Q | P&R", "(Q | R) & P <-> Q&P | R&P",
    50   "(P | Q --> R) <-> (P --> R) & (Q --> R)",
    51   "~(EX x. NORM(P(x))) <-> (ALL x. ~NORM(P(x)))",
    52   "((EX x. NORM(P(x))) --> Q) <-> (ALL x. NORM(P(x)) --> Q)",
    53   "(EX x. NORM(P(x))) & NORM(Q) <-> (EX x. NORM(P(x)) & NORM(Q))",
    54   "NORM(Q) & (EX x. NORM(P(x))) <-> (EX x. NORM(Q) & NORM(P(x)))"];
    55 
    56 val P_Imp_P_iff_T = int_prove_fun_raw "p:P ==> ?p:(P <-> True)";
    57 
    58 fun make_iff_T th = th RS P_Imp_P_iff_T;
    59 
    60 val refl_iff_T = make_iff_T refl;
    61 
    62 val norm_thms = [(norm_eq RS sym, norm_eq),
    63                  (NORM_iff RS iff_sym, NORM_iff)];
    64 
    65 
    66 (* Conversion into rewrite rules *)
    67 
    68 val not_P_imp_P_iff_F = int_prove_fun_raw "p:~P ==> ?p:(P <-> False)";
    69 
    70 fun mk_eq th = case concl_of th of
    71       _ $ (Const("op <->",_)$_$_) $ _ => th
    72     | _ $ (Const("op =",_)$_$_) $ _ => th
    73     | _ $ (Const("Not",_)$_) $ _ => th RS not_P_imp_P_iff_F
    74     | _ => make_iff_T th;
    75 
    76 
    77 val mksimps_pairs =
    78   [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
    79    ("All", [spec]), ("True", []), ("False", [])];
    80 
    81 fun mk_atomize pairs =
    82   let fun atoms th =
    83         (case concl_of th of
    84            Const("Trueprop",_) $ p =>
    85              (case head_of p of
    86                 Const(a,_) =>
    87                   (case AList.lookup (op =) pairs a of
    88                      SOME(rls) => List.concat (map atoms ([th] RL rls))
    89                    | NONE => [th])
    90               | _ => [th])
    91          | _ => [th])
    92   in atoms end;
    93 
    94 fun mk_rew_rules th = map mk_eq (mk_atomize mksimps_pairs th);
    95 
    96 (*destruct function for analysing equations*)
    97 fun dest_red(_ $ (red $ lhs $ rhs) $ _) = (red,lhs,rhs)
    98   | dest_red t = raise TERM("FOL/dest_red", [t]);
    99 
   100 structure FOLP_SimpData : SIMP_DATA =
   101   struct
   102   val refl_thms         = [refl, iff_refl]
   103   val trans_thms        = [trans, iff_trans]
   104   val red1              = iffD1
   105   val red2              = iffD2
   106   val mk_rew_rules      = mk_rew_rules
   107   val case_splits       = []         (*NO IF'S!*)
   108   val norm_thms         = norm_thms
   109   val subst_thms        = [subst];
   110   val dest_red          = dest_red
   111   end;
   112 
   113 structure FOLP_Simp = SimpFun(FOLP_SimpData);
   114 
   115 (*not a component of SIMP_DATA, but an argument of SIMP_TAC *)
   116 val FOLP_congs =
   117    [all_cong,ex_cong,eq_cong,
   118     conj_cong,disj_cong,imp_cong,iff_cong,not_cong] @ pred_congs;
   119 
   120 val IFOLP_rews =
   121    [refl_iff_T] @ conj_rews @ disj_rews @ not_rews @
   122     imp_rews @ iff_rews @ quant_rews;
   123 
   124 open FOLP_Simp;
   125 
   126 val auto_ss = empty_ss setauto ares_tac [TrueI];
   127 
   128 val IFOLP_ss = auto_ss addcongs FOLP_congs addrews IFOLP_rews;
   129 
   130 (*Classical version...*)
   131 fun prove_fun s =
   132     (writeln s;  prove_goal (the_context ()) s
   133        (fn prems => [ (cut_facts_tac prems 1), (Cla.fast_tac FOLP_cs 1) ]));
   134 
   135 val cla_rews = map prove_fun
   136  ["?p:P | ~P",          "?p:~P | P",
   137   "?p:~ ~ P <-> P",     "?p:(~P --> P) <-> P"];
   138 
   139 val FOLP_rews = IFOLP_rews@cla_rews;
   140 
   141 val FOLP_ss = auto_ss addcongs FOLP_congs addrews FOLP_rews;