src/FOLP/simpdata.ML
changeset 17480 fd19f77dcf60
parent 17325 d9d50222808e
child 26322 eaf634e975fa
equal deleted inserted replaced
17479:68a7acb5f22e 17480:fd19f77dcf60
     1 (*  Title:      FOLP/simpdata.ML
     1 (*  Title:      FOLP/simpdata.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     4     Copyright   1991  University of Cambridge
     5 
     5 
     6 Simplification data for FOLP
     6 Simplification data for FOLP.
     7 *)
     7 *)
     8 
     8 
     9 (*** Rewrite rules ***)
     9 (*** Rewrite rules ***)
    10 
    10 
    11 fun int_prove_fun_raw s = 
    11 fun int_prove_fun_raw s =
    12     (writeln s;  prove_goal IFOLP.thy s
    12     (writeln s;  prove_goal (the_context ()) s
    13        (fn prems => [ (cut_facts_tac prems 1), (IntPr.fast_tac 1) ]));
    13        (fn prems => [ (cut_facts_tac prems 1), (IntPr.fast_tac 1) ]));
    14 
    14 
    15 fun int_prove_fun s = int_prove_fun_raw ("?p : "^s);
    15 fun int_prove_fun s = int_prove_fun_raw ("?p : "^s);
    16 
    16 
    17 val conj_rews = map int_prove_fun
    17 val conj_rews = map int_prove_fun
    30 val not_rews = map int_prove_fun
    30 val not_rews = map int_prove_fun
    31  ["~ False <-> True",   "~ True <-> False"];
    31  ["~ False <-> True",   "~ True <-> False"];
    32 
    32 
    33 val imp_rews = map int_prove_fun
    33 val imp_rews = map int_prove_fun
    34  ["(P --> False) <-> ~P",       "(P --> True) <-> True",
    34  ["(P --> False) <-> ~P",       "(P --> True) <-> True",
    35   "(False --> P) <-> True",     "(True --> P) <-> P", 
    35   "(False --> P) <-> True",     "(True --> P) <-> P",
    36   "(P --> P) <-> True",         "(P --> ~P) <-> ~P"];
    36   "(P --> P) <-> True",         "(P --> ~P) <-> ~P"];
    37 
    37 
    38 val iff_rews = map int_prove_fun
    38 val iff_rews = map int_prove_fun
    39  ["(True <-> P) <-> P",         "(P <-> True) <-> P",
    39  ["(True <-> P) <-> P",         "(P <-> True) <-> P",
    40   "(P <-> P) <-> True",
    40   "(P <-> P) <-> True",
    68 val not_P_imp_P_iff_F = int_prove_fun_raw "p:~P ==> ?p:(P <-> False)";
    68 val not_P_imp_P_iff_F = int_prove_fun_raw "p:~P ==> ?p:(P <-> False)";
    69 
    69 
    70 fun mk_eq th = case concl_of th of
    70 fun mk_eq th = case concl_of th of
    71       _ $ (Const("op <->",_)$_$_) $ _ => th
    71       _ $ (Const("op <->",_)$_$_) $ _ => th
    72     | _ $ (Const("op =",_)$_$_) $ _ => th
    72     | _ $ (Const("op =",_)$_$_) $ _ => th
    73     | _ $ (Const("Not",_)$_) $ _ => th RS not_P_imp_P_iff_F 
    73     | _ $ (Const("Not",_)$_) $ _ => th RS not_P_imp_P_iff_F
    74     | _ => make_iff_T th;
    74     | _ => make_iff_T th;
    75 
    75 
    76 
    76 
    77 val mksimps_pairs =
    77 val mksimps_pairs =
    78   [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
    78   [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
   111   end;
   111   end;
   112 
   112 
   113 structure FOLP_Simp = SimpFun(FOLP_SimpData);
   113 structure FOLP_Simp = SimpFun(FOLP_SimpData);
   114 
   114 
   115 (*not a component of SIMP_DATA, but an argument of SIMP_TAC *)
   115 (*not a component of SIMP_DATA, but an argument of SIMP_TAC *)
   116 val FOLP_congs = 
   116 val FOLP_congs =
   117    [all_cong,ex_cong,eq_cong,
   117    [all_cong,ex_cong,eq_cong,
   118     conj_cong,disj_cong,imp_cong,iff_cong,not_cong] @ pred_congs;
   118     conj_cong,disj_cong,imp_cong,iff_cong,not_cong] @ pred_congs;
   119 
   119 
   120 val IFOLP_rews =
   120 val IFOLP_rews =
   121    [refl_iff_T] @ conj_rews @ disj_rews @ not_rews @ 
   121    [refl_iff_T] @ conj_rews @ disj_rews @ not_rews @
   122     imp_rews @ iff_rews @ quant_rews;
   122     imp_rews @ iff_rews @ quant_rews;
   123 
   123 
   124 open FOLP_Simp;
   124 open FOLP_Simp;
   125 
   125 
   126 val auto_ss = empty_ss setauto ares_tac [TrueI];
   126 val auto_ss = empty_ss setauto ares_tac [TrueI];
   127 
   127 
   128 val IFOLP_ss = auto_ss addcongs FOLP_congs addrews IFOLP_rews;
   128 val IFOLP_ss = auto_ss addcongs FOLP_congs addrews IFOLP_rews;
   129 
   129 
   130 (*Classical version...*)
   130 (*Classical version...*)
   131 fun prove_fun s = 
   131 fun prove_fun s =
   132     (writeln s;  prove_goal FOLP.thy s
   132     (writeln s;  prove_goal (the_context ()) s
   133        (fn prems => [ (cut_facts_tac prems 1), (Cla.fast_tac FOLP_cs 1) ]));
   133        (fn prems => [ (cut_facts_tac prems 1), (Cla.fast_tac FOLP_cs 1) ]));
   134 
   134 
   135 val cla_rews = map prove_fun
   135 val cla_rews = map prove_fun
   136  ["?p:P | ~P",          "?p:~P | P",
   136  ["?p:P | ~P",          "?p:~P | P",
   137   "?p:~ ~ P <-> P",     "?p:(~P --> P) <-> P"];
   137   "?p:~ ~ P <-> P",     "?p:(~P --> P) <-> P"];
   138 
   138 
   139 val FOLP_rews = IFOLP_rews@cla_rews;
   139 val FOLP_rews = IFOLP_rews@cla_rews;
   140 
   140 
   141 val FOLP_ss = auto_ss addcongs FOLP_congs addrews FOLP_rews;
   141 val FOLP_ss = auto_ss addcongs FOLP_congs addrews FOLP_rews;
   142 
       
   143