src/FOL/simpdata.ML
changeset 282 731b27c90d2f
parent 215 bc439e9ce958
child 371 3a853818f1d2
     1.1 --- a/src/FOL/simpdata.ML	Thu Mar 17 13:07:48 1994 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Thu Mar 17 13:54:50 1994 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title: 	FOL/simpdata
     1.5      ID:         $Id$
     1.6      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1991  University of Cambridge
     1.8 +    Copyright   1994  University of Cambridge
     1.9  
    1.10  Simplification data for FOL
    1.11  *)
    1.12 @@ -9,14 +9,16 @@
    1.13  (*** Rewrite rules ***)
    1.14  
    1.15  fun int_prove_fun s = 
    1.16 -    (writeln s;  prove_goal IFOL.thy s
    1.17 -       (fn prems => [ (cut_facts_tac prems 1), (Int.fast_tac 1) ]));
    1.18 + (writeln s;  
    1.19 +  prove_goal IFOL.thy s
    1.20 +   (fn prems => [ (cut_facts_tac prems 1), 
    1.21 +		  (Int.fast_tac 1) ]));
    1.22  
    1.23  val conj_rews = map int_prove_fun
    1.24 - ["P & True <-> P", 	"True & P <-> P",
    1.25 + ["P & True <-> P", 	 "True & P <-> P",
    1.26    "P & False <-> False", "False & P <-> False",
    1.27    "P & P <-> P",
    1.28 -  "P & ~P <-> False", 	"~P & P <-> False",
    1.29 +  "P & ~P <-> False", 	 "~P & P <-> False",
    1.30    "(P & Q) & R <-> P & (Q & R)"];
    1.31  
    1.32  val disj_rews = map int_prove_fun
    1.33 @@ -26,7 +28,8 @@
    1.34    "(P | Q) | R <-> P | (Q | R)"];
    1.35  
    1.36  val not_rews = map int_prove_fun
    1.37 - ["~ False <-> True",	"~ True <-> False"];
    1.38 + ["~(P|Q)  <-> ~P & ~Q",
    1.39 +  "~ False <-> True",	"~ True <-> False"];
    1.40  
    1.41  val imp_rews = map int_prove_fun
    1.42   ["(P --> False) <-> ~P",	"(P --> True) <-> True",
    1.43 @@ -43,79 +46,78 @@
    1.44  
    1.45  (*These are NOT supplied by default!*)
    1.46  val distrib_rews  = map int_prove_fun
    1.47 - ["~(P|Q) <-> ~P & ~Q",
    1.48 -  "P & (Q | R) <-> P&Q | P&R", "(Q | R) & P <-> Q&P | R&P",
    1.49 + ["P & (Q | R) <-> P&Q | P&R", 
    1.50 +  "(Q | R) & P <-> Q&P | R&P",
    1.51    "(P | Q --> R) <-> (P --> R) & (Q --> R)"];
    1.52  
    1.53 -val P_Imp_P_iff_T = int_prove_fun "P ==> (P <-> True)";
    1.54 -
    1.55 -fun make_iff_T th = th RS P_Imp_P_iff_T;
    1.56 -
    1.57 -val refl_iff_T = make_iff_T refl;
    1.58 -
    1.59 -val notFalseI = int_prove_fun "~False";
    1.60 -
    1.61 -(* Conversion into rewrite rules *)
    1.62 -
    1.63 -val not_P_imp_P_iff_F = int_prove_fun "~P ==> (P <-> False)";
    1.64 -
    1.65 -fun mk_meta_eq th = case concl_of th of
    1.66 -      _ $ (Const("op <->",_)$_$_) => th RS iff_reflection
    1.67 -    | _ $ (Const("op =",_)$_$_) => th RS eq_reflection
    1.68 -    | _ $ (Const("Not",_)$_) => (th RS not_P_imp_P_iff_F) RS iff_reflection
    1.69 -    | _ => (make_iff_T th) RS iff_reflection;
    1.70 -
    1.71 -fun atomize th = case concl_of th of (*The operator below is Trueprop*)
    1.72 -      _ $ (Const("op -->",_) $ _ $ _) => atomize(th RS mp)
    1.73 -    | _ $ (Const("op &",_) $ _ $ _) => atomize(th RS conjunct1) @
    1.74 -				       atomize(th RS conjunct2)
    1.75 -    | _ $ (Const("All",_) $ _) => atomize(th RS spec)
    1.76 -    | _ $ (Const("True",_)) => []
    1.77 -    | _ $ (Const("False",_)) => []
    1.78 -    | _ => [th];
    1.79 +(** Conversion into rewrite rules **)
    1.80  
    1.81  fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
    1.82  
    1.83 -fun mk_rew_rules th = map mk_meta_eq (atomize(gen_all th));
    1.84 +(*Make atomic rewrite rules*)
    1.85 +fun atomize th = case concl_of th of 
    1.86 +    _ $ (Const("op &",_) $ _ $ _)   => atomize(th RS conjunct1) @
    1.87 +				       atomize(th RS conjunct2)
    1.88 +  | _ $ (Const("op -->",_) $ _ $ _) => atomize(th RS mp)
    1.89 +  | _ $ (Const("All",_) $ _)        => atomize(th RS spec)
    1.90 +  | _ $ (Const("True",_))           => []
    1.91 +  | _ $ (Const("False",_))          => []
    1.92 +  | _                               => [th];
    1.93 +
    1.94 +val P_iff_F = int_prove_fun "~P ==> (P <-> False)";
    1.95 +val iff_reflection_F = P_iff_F RS iff_reflection;
    1.96 +
    1.97 +val P_iff_T = int_prove_fun "P ==> (P <-> True)";
    1.98 +val iff_reflection_T = P_iff_T RS iff_reflection;
    1.99 +
   1.100 +(*Make meta-equalities.  The operator below is Trueprop*)
   1.101 +fun mk_meta_eq th = case concl_of th of
   1.102 +    _ $ (Const("op =",_)$_$_)   => th RS eq_reflection
   1.103 +  | _ $ (Const("op <->",_)$_$_) => th RS iff_reflection
   1.104 +  | _ $ (Const("Not",_)$_)      => th RS iff_reflection_F
   1.105 +  | _                           => th RS iff_reflection_T;
   1.106  
   1.107  structure Induction = InductionFun(struct val spec=IFOL.spec end);
   1.108  
   1.109 -val IFOL_rews =
   1.110 -   [refl_iff_T] @ conj_rews @ disj_rews @ not_rews @ 
   1.111 -    imp_rews @ iff_rews @ quant_rews;
   1.112 -
   1.113  open Simplifier Induction;
   1.114  
   1.115  infix addcongs;
   1.116  fun ss addcongs congs =
   1.117 -  ss addeqcongs (congs RL [eq_reflection,iff_reflection]);
   1.118 +    ss addeqcongs (congs RL [eq_reflection,iff_reflection]);
   1.119 +
   1.120 +val IFOL_rews =
   1.121 +   [refl RS P_iff_T] @ conj_rews @ disj_rews @ not_rews @ 
   1.122 +    imp_rews @ iff_rews @ quant_rews;
   1.123  
   1.124 -val IFOL_ss = empty_ss
   1.125 -      setmksimps mk_rew_rules
   1.126 -      setsolver
   1.127 -        (fn prems => resolve_tac (TrueI::refl::iff_refl::notFalseI::prems)
   1.128 -                     ORELSE' atac)
   1.129 -      setsubgoaler asm_simp_tac
   1.130 -      addsimps IFOL_rews
   1.131 -      addcongs [imp_cong];
   1.132 +val notFalseI = int_prove_fun "~False";
   1.133 +val triv_rls = [TrueI,refl,iff_refl,notFalseI];
   1.134 +
   1.135 +val IFOL_ss = 
   1.136 +  empty_ss 
   1.137 +  setmksimps (map mk_meta_eq o atomize o gen_all)
   1.138 +  setsolver  (fn prems => resolve_tac (triv_rls@prems) ORELSE' assume_tac)
   1.139 +  setsubgoaler asm_simp_tac
   1.140 +  addsimps IFOL_rews
   1.141 +  addcongs [imp_cong];
   1.142  
   1.143  (*Classical version...*)
   1.144  fun prove_fun s = 
   1.145 -    (writeln s;  prove_goal FOL.thy s
   1.146 -       (fn prems => [ (cut_facts_tac prems 1), (Cla.fast_tac FOL_cs 1) ]));
   1.147 -
   1.148 + (writeln s;  
   1.149 +  prove_goal FOL.thy s
   1.150 +   (fn prems => [ (cut_facts_tac prems 1), 
   1.151 +		  (Cla.fast_tac FOL_cs 1) ]));
   1.152  val cla_rews = map prove_fun
   1.153 - ["P | ~P", 		"~P | P",
   1.154 + ["~(P&Q)  <-> ~P | ~Q",
   1.155 +  "P | ~P", 		"~P | P",
   1.156    "~ ~ P <-> P",	"(~P --> P) <-> P"];
   1.157  
   1.158  val FOL_ss = IFOL_ss addsimps cla_rews;
   1.159  
   1.160  (*** case splitting ***)
   1.161  
   1.162 -val split_tac =
   1.163 -  let val eq_reflection2 = prove_goal FOL.thy "x==y ==> x=y"
   1.164 -                             (fn [prem] => [rewtac prem, rtac refl 1])
   1.165 -      val iff_reflection2 = prove_goal FOL.thy "x==y ==> x<->y"
   1.166 -                              (fn [prem] => [rewtac prem, rtac iff_refl 1])
   1.167 -      val [iffD] = [eq_reflection2,iff_reflection2] RL [iffD2]
   1.168 -  in fn splits => mk_case_split_tac iffD (map mk_meta_eq splits) end;
   1.169 +val meta_iffD = 
   1.170 +    prove_goal FOL.thy "[| P==Q; Q |] ==> P"
   1.171 +        (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1])
   1.172 +
   1.173 +fun split_tac splits =
   1.174 +    mk_case_split_tac meta_iffD (map mk_meta_eq splits);