--- 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 *}
--- 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 *)
--- 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);