# HG changeset patch
# User paulson
# Date 1131640394 -3600
# Node ID 4edcb5fdc3b063fb67ead8e80c6d04361cf70a7a
# Parent  fe14f0282c60dd698baa85617f49e50cf76558a1
duplicate axioms in ATP linkup, and general fixes

diff -r fe14f0282c60 -r 4edcb5fdc3b0 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Nov 10 17:31:44 2005 +0100
+++ b/src/HOL/Set.thy	Thu Nov 10 17:33:14 2005 +0100
@@ -524,7 +524,7 @@
 lemma contra_subsetD: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
   by blast
 
-lemma subset_refl: "A \<subseteq> A"
+lemma subset_refl [simp,intro!]: "A \<subseteq> A"
   by fast
 
 lemma subset_trans: "A \<subseteq> B ==> B \<subseteq> C ==> A \<subseteq> C"
@@ -600,7 +600,7 @@
 lemma UNIV_witness [intro?]: "EX x. x : UNIV"
   by simp
 
-lemma subset_UNIV: "A \<subseteq> UNIV"
+lemma subset_UNIV [simp]: "A \<subseteq> UNIV"
   by (rule subsetI) (rule UNIV_I)
 
 text {*
@@ -980,8 +980,6 @@
   change_simpset (fn ss => ss setmksimps (mksimps mksimps_pairs));
 *}
 
-declare subset_UNIV [simp] subset_refl [simp]
-
 
 subsubsection {* The ``proper subset'' relation *}
 
diff -r fe14f0282c60 -r 4edcb5fdc3b0 src/HOL/Tools/ATP/res_clasimpset.ML
--- a/src/HOL/Tools/ATP/res_clasimpset.ML	Thu Nov 10 17:31:44 2005 +0100
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Thu Nov 10 17:33:14 2005 +0100
@@ -141,22 +141,28 @@
 	multi (clause, theorem) num_of_cls []
     end;
     
+fun get_simpset_thms ctxt goal clas =
+  let val ctab = fold_rev Symtab.update clas Symtab.empty
+      fun unused (s,_) = not (Symtab.defined ctab s)
+  in  ResAxioms.clausify_rules_pairs 
+	(filter unused
+	  (map put_name_pair 
+	    (ReduceAxiomsN.relevant_filter (!relevant) goal
+	      (ResAxioms.simpset_rules_of_ctxt ctxt))))
+  end;
+		  
 
 (*Write out the claset and simpset rules of the supplied theory.
   FIXME: argument "goal" is a hack to allow relevance filtering.
   To reduce the number of clauses produced, set ResClasimp.relevant:=1*)
 fun get_clasimp_lemmas ctxt goal = 
-    let val claset_cls_thms =
-              ResAxioms.clausify_rules_pairs
-		(map put_name_pair
+    let val claset_thms =
+		map put_name_pair
 		  (ReduceAxiomsN.relevant_filter (!relevant) goal 
-		    (ResAxioms.claset_rules_of_ctxt ctxt)))
+		    (ResAxioms.claset_rules_of_ctxt ctxt))
+	val claset_cls_thms = ResAxioms.clausify_rules_pairs claset_thms
 	val simpset_cls_thms = 
-	      if !use_simpset then  
-		  ResAxioms.clausify_rules_pairs 
-		    (map put_name_pair 
-		      (ReduceAxiomsN.relevant_filter (!relevant) goal
-		        (ResAxioms.simpset_rules_of_ctxt ctxt))) 
+	      if !use_simpset then get_simpset_thms ctxt goal claset_thms
 	      else []
 	val cls_thms_list = List.concat (claset_cls_thms@simpset_cls_thms)
 	(* Identify the set of clauses to be written out *)
diff -r fe14f0282c60 -r 4edcb5fdc3b0 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Thu Nov 10 17:31:44 2005 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Thu Nov 10 17:33:14 2005 +0100
@@ -301,28 +301,34 @@
 
 (*Populate the clause cache using the supplied theorems*)
 fun skolem_cache ((name,th), thy) =
-      (case Symtab.lookup (!clause_cache) name of
-	  NONE => 
-	    (case skolem thy (name, Thm.transfer thy th) of
-	         NONE => thy
-	       | SOME (thy',cls) => 
-	           (change clause_cache (Symtab.update (name, (th, cls))); thy'))
-	| SOME _ => thy);
+  case Symtab.lookup (!clause_cache) name of
+      NONE => 
+	(case skolem thy (name, Thm.transfer thy th) of
+	     NONE => thy
+	   | SOME (thy',cls) => 
+	       (change clause_cache (Symtab.update (name, (th, cls))); thy'))
+    | SOME (th',cls) =>
+        if eq_thm(th,th') then thy
+	else (warning ("skolem_cache: Ignoring variant of theorem " ^ name); 
+	      warning (string_of_thm th);
+	      warning (string_of_thm th');
+	      thy);
 
 
 (*Exported function to convert Isabelle theorems into axiom clauses*) 
 fun cnf_axiom_g cnf (name,th) =
-    case name of
-	  "" => cnf th (*no name, so can't cache*)
-	| s  => case Symtab.lookup (!clause_cache) s of
-	  	  NONE => 
-		    let val cls = cnf th
-		    in change clause_cache (Symtab.update (s, (th, cls))); cls end
-	        | SOME(th',cls) =>
-		    if eq_thm(th,th') then cls
-		    else (*New theorem stored under the same name? Possible??*)
-		      let val cls = cnf th
-		      in change clause_cache (Symtab.update (s, (th, cls))); cls end;
+  case name of
+	"" => cnf th (*no name, so can't cache*)
+      | s  => case Symtab.lookup (!clause_cache) s of
+		NONE => 
+		  let val cls = cnf th
+		  in change clause_cache (Symtab.update (s, (th, cls))); cls end
+	      | SOME(th',cls) =>
+		  if eq_thm(th,th') then cls
+		  else (warning ("cnf_axiom: duplicate or variant of theorem " ^ name); 
+		        warning (string_of_thm th);
+		        warning (string_of_thm th');
+		        cls);
 
 fun pairname th = (Thm.name_of_thm th, th);