src/FOL/simpdata.ML
author lcp
Tue Mar 07 13:15:25 1995 +0100 (1995-03-07)
changeset 928 cb31a4e97f75
parent 784 b5adfdad0663
child 942 d9edeb96b51c
permissions -rw-r--r--
Moved declaration of ~= to a syntax section
     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_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  ["~(P|Q)  <-> ~P & ~Q",
    32   "~ False <-> True",	"~ True <-> False"];
    33 
    34 val imp_rews = 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_rews = 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_rews = map int_prove_fun
    45  ["(ALL x.P) <-> P",	"(EX x.P) <-> P"];
    46 
    47 (*These are NOT supplied by default!*)
    48 val distrib_rews  = 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 bind_thm("conj_commute", int_prove_fun "P&Q <-> Q&P");
    54 bind_thm("disj_commute", int_prove_fun "P|Q <-> Q|P");
    55 
    56 (** Conversion into rewrite rules **)
    57 
    58 fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
    59 
    60 (*Make atomic rewrite rules*)
    61 fun atomize r =
    62   case concl_of r of
    63     Const("Trueprop",_) $ p =>
    64       (case p of
    65 	 Const("op -->",_)$_$_ => atomize(r RS mp)
    66        | Const("op &",_)$_$_   => atomize(r RS conjunct1) @
    67 	  		          atomize(r RS conjunct2)
    68        | Const("All",_)$_      => atomize(r RS spec)
    69        | Const("True",_)       => []	(*True is DELETED*)
    70        | Const("False",_)      => []	(*should False do something?*)
    71        | _                     => [r])
    72   | _ => [r];
    73 
    74 
    75 val P_iff_F = int_prove_fun "~P ==> (P <-> False)";
    76 val iff_reflection_F = P_iff_F RS iff_reflection;
    77 
    78 val P_iff_T = int_prove_fun "P ==> (P <-> True)";
    79 val iff_reflection_T = P_iff_T RS iff_reflection;
    80 
    81 (*Make meta-equalities.  The operator below is Trueprop*)
    82 fun mk_meta_eq th = case concl_of th of
    83     Const("==",_)$_$_           => th
    84   | _ $ (Const("op =",_)$_$_)   => th RS eq_reflection
    85   | _ $ (Const("op <->",_)$_$_) => th RS iff_reflection
    86   | _ $ (Const("Not",_)$_)      => th RS iff_reflection_F
    87   | _                           => th RS iff_reflection_T;
    88 
    89 structure Induction = InductionFun(struct val spec=IFOL.spec end);
    90 
    91 open Simplifier Induction;
    92 
    93 infix addcongs;
    94 fun ss addcongs congs =
    95     ss addeqcongs (congs RL [eq_reflection,iff_reflection]);
    96 
    97 val IFOL_rews =
    98    [refl RS P_iff_T] @ conj_rews @ disj_rews @ not_rews @ 
    99     imp_rews @ iff_rews @ quant_rews;
   100 
   101 val notFalseI = int_prove_fun "~False";
   102 val triv_rls = [TrueI,refl,iff_refl,notFalseI];
   103 
   104 val IFOL_ss = 
   105   empty_ss 
   106   setmksimps (map mk_meta_eq o atomize o gen_all)
   107   setsolver  (fn prems => resolve_tac (triv_rls@prems) 
   108 	                  ORELSE' assume_tac
   109 	                  ORELSE' etac FalseE)
   110   setsubgoaler asm_simp_tac
   111   addsimps IFOL_rews
   112   addcongs [imp_cong];
   113 
   114 (*Classical version...*)
   115 fun prove_fun s = 
   116  (writeln s;  
   117   prove_goal FOL.thy s
   118    (fn prems => [ (cut_facts_tac prems 1), 
   119 		  (Cla.fast_tac FOL_cs 1) ]));
   120 
   121 val cla_rews = map prove_fun
   122  ["~(P&Q)  <-> ~P | ~Q",
   123   "P | ~P", 		"~P | P",
   124   "~ ~ P <-> P",	"(~P --> P) <-> P"];
   125 
   126 val FOL_ss = IFOL_ss addsimps cla_rews;
   127 
   128 (*** case splitting ***)
   129 
   130 qed_goal "meta_iffD" FOL.thy "[| P==Q; Q |] ==> P"
   131         (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]);
   132 
   133 fun split_tac splits =
   134     mk_case_split_tac meta_iffD (map mk_meta_eq splits);