src/FOL/simpdata.ML

 (*  Title: 	FOL/simpdata
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1991  University of Cambridge
+    Copyright   1994  University of Cambridge
 
 Simplification data for FOL
 *)
 
 (*** Rewrite rules ***)
 
 fun int_prove_fun s = 
-    (writeln s;  prove_goal IFOL.thy s
-       (fn prems => [ (cut_facts_tac prems 1), (Int.fast_tac 1) ]));
+ (writeln s;  
+  prove_goal IFOL.thy s
+   (fn prems => [ (cut_facts_tac prems 1), 
+		  (Int.fast_tac 1) ]));
 
 val conj_rews = map int_prove_fun
- ["P & True <-> P", 	"True & P <-> P",
+ ["P & True <-> P", 	 "True & P <-> P",
   "P & False <-> False", "False & P <-> False",
   "P & P <-> P",
-  "P & ~P <-> False", 	"~P & P <-> False",
+  "P & ~P <-> False", 	 "~P & P <-> False",
   "(P & Q) & R <-> P & (Q & R)"];
 
 val disj_rews = map int_prove_fun
  ["P | True <-> True", 	"True | P <-> True",
   "P | False <-> P", 	"False | P <-> P",
   "P | P <-> P",
   "(P | Q) | R <-> P | (Q | R)"];
 
 val not_rews = map int_prove_fun
- ["~ False <-> True",	"~ True <-> False"];
+ ["~(P|Q)  <-> ~P & ~Q",
+  "~ False <-> True",	"~ True <-> False"];
 
 val imp_rews = map int_prove_fun
  ["(P --> False) <-> ~P",	"(P --> True) <-> True",
   "(False --> P) <-> True",	"(True --> P) <-> P", 
   "(P --> P) <-> True",		"(P --> ~P) <-> ~P"];

 val quant_rews = map int_prove_fun
  ["(ALL x.P) <-> P",	"(EX x.P) <-> P"];
 
 (*These are NOT supplied by default!*)
 val distrib_rews  = map int_prove_fun
- ["~(P|Q) <-> ~P & ~Q",
-  "P & (Q | R) <-> P&Q | P&R", "(Q | R) & P <-> Q&P | R&P",
+ ["P & (Q | R) <-> P&Q | P&R", 
+  "(Q | R) & P <-> Q&P | R&P",
   "(P | Q --> R) <-> (P --> R) & (Q --> R)"];
 
-val P_Imp_P_iff_T = int_prove_fun "P ==> (P <-> True)";
-
-fun make_iff_T th = th RS P_Imp_P_iff_T;
-
-val refl_iff_T = make_iff_T refl;
-
-val notFalseI = int_prove_fun "~False";
-
-(* Conversion into rewrite rules *)
-
-val not_P_imp_P_iff_F = int_prove_fun "~P ==> (P <-> False)";
-
-fun mk_meta_eq th = case concl_of th of
-      _ $ (Const("op <->",_)$_$_) => th RS iff_reflection
-    | _ $ (Const("op =",_)$_$_) => th RS eq_reflection
-    | _ $ (Const("Not",_)$_) => (th RS not_P_imp_P_iff_F) RS iff_reflection
-    | _ => (make_iff_T th) RS iff_reflection;
-
-fun atomize th = case concl_of th of (*The operator below is Trueprop*)
-      _ $ (Const("op -->",_) $ _ $ _) => atomize(th RS mp)
-    | _ $ (Const("op &",_) $ _ $ _) => atomize(th RS conjunct1) @
-				       atomize(th RS conjunct2)
-    | _ $ (Const("All",_) $ _) => atomize(th RS spec)
-    | _ $ (Const("True",_)) => []
-    | _ $ (Const("False",_)) => []
-    | _ => [th];
+(** Conversion into rewrite rules **)
 
 fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
 
-fun mk_rew_rules th = map mk_meta_eq (atomize(gen_all th));
+(*Make atomic rewrite rules*)
+fun atomize th = case concl_of th of 
+    _ $ (Const("op &",_) $ _ $ _)   => atomize(th RS conjunct1) @
+				       atomize(th RS conjunct2)
+  | _ $ (Const("op -->",_) $ _ $ _) => atomize(th RS mp)
+  | _ $ (Const("All",_) $ _)        => atomize(th RS spec)
+  | _ $ (Const("True",_))           => []
+  | _ $ (Const("False",_))          => []
+  | _                               => [th];
+
+val P_iff_F = int_prove_fun "~P ==> (P <-> False)";
+val iff_reflection_F = P_iff_F RS iff_reflection;
+
+val P_iff_T = int_prove_fun "P ==> (P <-> True)";
+val iff_reflection_T = P_iff_T RS iff_reflection;
+
+(*Make meta-equalities.  The operator below is Trueprop*)
+fun mk_meta_eq th = case concl_of th of
+    _ $ (Const("op =",_)$_$_)   => th RS eq_reflection
+  | _ $ (Const("op <->",_)$_$_) => th RS iff_reflection
+  | _ $ (Const("Not",_)$_)      => th RS iff_reflection_F
+  | _                           => th RS iff_reflection_T;
 
 structure Induction = InductionFun(struct val spec=IFOL.spec end);
-
-val IFOL_rews =
-   [refl_iff_T] @ conj_rews @ disj_rews @ not_rews @ 
-    imp_rews @ iff_rews @ quant_rews;
 
 open Simplifier Induction;
 
 infix addcongs;
 fun ss addcongs congs =
-  ss addeqcongs (congs RL [eq_reflection,iff_reflection]);
+    ss addeqcongs (congs RL [eq_reflection,iff_reflection]);
 
-val IFOL_ss = empty_ss
-      setmksimps mk_rew_rules
-      setsolver
-        (fn prems => resolve_tac (TrueI::refl::iff_refl::notFalseI::prems)
-                     ORELSE' atac)
-      setsubgoaler asm_simp_tac
-      addsimps IFOL_rews
-      addcongs [imp_cong];
+val IFOL_rews =
+   [refl RS P_iff_T] @ conj_rews @ disj_rews @ not_rews @ 
+    imp_rews @ iff_rews @ quant_rews;
+
+val notFalseI = int_prove_fun "~False";
+val triv_rls = [TrueI,refl,iff_refl,notFalseI];
+
+val IFOL_ss = 
+  empty_ss 
+  setmksimps (map mk_meta_eq o atomize o gen_all)
+  setsolver  (fn prems => resolve_tac (triv_rls@prems) ORELSE' assume_tac)
+  setsubgoaler asm_simp_tac
+  addsimps IFOL_rews
+  addcongs [imp_cong];
 
 (*Classical version...*)
 fun prove_fun s = 
-    (writeln s;  prove_goal FOL.thy s
-       (fn prems => [ (cut_facts_tac prems 1), (Cla.fast_tac FOL_cs 1) ]));
-
+ (writeln s;  
+  prove_goal FOL.thy s
+   (fn prems => [ (cut_facts_tac prems 1), 
+		  (Cla.fast_tac FOL_cs 1) ]));
 val cla_rews = map prove_fun
- ["P | ~P", 		"~P | P",
+ ["~(P&Q)  <-> ~P | ~Q",
+  "P | ~P", 		"~P | P",
   "~ ~ P <-> P",	"(~P --> P) <-> P"];
 
 val FOL_ss = IFOL_ss addsimps cla_rews;
 
 (*** case splitting ***)
 
-val split_tac =
-  let val eq_reflection2 = prove_goal FOL.thy "x==y ==> x=y"
-                             (fn [prem] => [rewtac prem, rtac refl 1])
-      val iff_reflection2 = prove_goal FOL.thy "x==y ==> x<->y"
-                              (fn [prem] => [rewtac prem, rtac iff_refl 1])
-      val [iffD] = [eq_reflection2,iff_reflection2] RL [iffD2]
-  in fn splits => mk_case_split_tac iffD (map mk_meta_eq splits) end;
+val meta_iffD = 
+    prove_goal FOL.thy "[| P==Q; Q |] ==> P"
+        (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1])
+
+fun split_tac splits =
+    mk_case_split_tac meta_iffD (map mk_meta_eq splits);