duplicate axioms in ATP linkup, and general fixes
authorpaulson
Thu Nov 10 17:33:14 2005 +0100 (2005-11-10)
changeset 181444edcb5fdc3b0
parent 18143 fe14f0282c60
child 18145 6757627acf59
duplicate axioms in ATP linkup, and general fixes
src/HOL/Set.thy
src/HOL/Tools/ATP/res_clasimpset.ML
src/HOL/Tools/res_axioms.ML
     1.1 --- a/src/HOL/Set.thy	Thu Nov 10 17:31:44 2005 +0100
     1.2 +++ b/src/HOL/Set.thy	Thu Nov 10 17:33:14 2005 +0100
     1.3 @@ -524,7 +524,7 @@
     1.4  lemma contra_subsetD: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
     1.5    by blast
     1.6  
     1.7 -lemma subset_refl: "A \<subseteq> A"
     1.8 +lemma subset_refl [simp,intro!]: "A \<subseteq> A"
     1.9    by fast
    1.10  
    1.11  lemma subset_trans: "A \<subseteq> B ==> B \<subseteq> C ==> A \<subseteq> C"
    1.12 @@ -600,7 +600,7 @@
    1.13  lemma UNIV_witness [intro?]: "EX x. x : UNIV"
    1.14    by simp
    1.15  
    1.16 -lemma subset_UNIV: "A \<subseteq> UNIV"
    1.17 +lemma subset_UNIV [simp]: "A \<subseteq> UNIV"
    1.18    by (rule subsetI) (rule UNIV_I)
    1.19  
    1.20  text {*
    1.21 @@ -980,8 +980,6 @@
    1.22    change_simpset (fn ss => ss setmksimps (mksimps mksimps_pairs));
    1.23  *}
    1.24  
    1.25 -declare subset_UNIV [simp] subset_refl [simp]
    1.26 -
    1.27  
    1.28  subsubsection {* The ``proper subset'' relation *}
    1.29  
     2.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Thu Nov 10 17:31:44 2005 +0100
     2.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Thu Nov 10 17:33:14 2005 +0100
     2.3 @@ -141,22 +141,28 @@
     2.4  	multi (clause, theorem) num_of_cls []
     2.5      end;
     2.6      
     2.7 +fun get_simpset_thms ctxt goal clas =
     2.8 +  let val ctab = fold_rev Symtab.update clas Symtab.empty
     2.9 +      fun unused (s,_) = not (Symtab.defined ctab s)
    2.10 +  in  ResAxioms.clausify_rules_pairs 
    2.11 +	(filter unused
    2.12 +	  (map put_name_pair 
    2.13 +	    (ReduceAxiomsN.relevant_filter (!relevant) goal
    2.14 +	      (ResAxioms.simpset_rules_of_ctxt ctxt))))
    2.15 +  end;
    2.16 +		  
    2.17  
    2.18  (*Write out the claset and simpset rules of the supplied theory.
    2.19    FIXME: argument "goal" is a hack to allow relevance filtering.
    2.20    To reduce the number of clauses produced, set ResClasimp.relevant:=1*)
    2.21  fun get_clasimp_lemmas ctxt goal = 
    2.22 -    let val claset_cls_thms =
    2.23 -              ResAxioms.clausify_rules_pairs
    2.24 -		(map put_name_pair
    2.25 +    let val claset_thms =
    2.26 +		map put_name_pair
    2.27  		  (ReduceAxiomsN.relevant_filter (!relevant) goal 
    2.28 -		    (ResAxioms.claset_rules_of_ctxt ctxt)))
    2.29 +		    (ResAxioms.claset_rules_of_ctxt ctxt))
    2.30 +	val claset_cls_thms = ResAxioms.clausify_rules_pairs claset_thms
    2.31  	val simpset_cls_thms = 
    2.32 -	      if !use_simpset then  
    2.33 -		  ResAxioms.clausify_rules_pairs 
    2.34 -		    (map put_name_pair 
    2.35 -		      (ReduceAxiomsN.relevant_filter (!relevant) goal
    2.36 -		        (ResAxioms.simpset_rules_of_ctxt ctxt))) 
    2.37 +	      if !use_simpset then get_simpset_thms ctxt goal claset_thms
    2.38  	      else []
    2.39  	val cls_thms_list = List.concat (claset_cls_thms@simpset_cls_thms)
    2.40  	(* Identify the set of clauses to be written out *)
     3.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Nov 10 17:31:44 2005 +0100
     3.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Nov 10 17:33:14 2005 +0100
     3.3 @@ -301,28 +301,34 @@
     3.4  
     3.5  (*Populate the clause cache using the supplied theorems*)
     3.6  fun skolem_cache ((name,th), thy) =
     3.7 -      (case Symtab.lookup (!clause_cache) name of
     3.8 -	  NONE => 
     3.9 -	    (case skolem thy (name, Thm.transfer thy th) of
    3.10 -	         NONE => thy
    3.11 -	       | SOME (thy',cls) => 
    3.12 -	           (change clause_cache (Symtab.update (name, (th, cls))); thy'))
    3.13 -	| SOME _ => thy);
    3.14 +  case Symtab.lookup (!clause_cache) name of
    3.15 +      NONE => 
    3.16 +	(case skolem thy (name, Thm.transfer thy th) of
    3.17 +	     NONE => thy
    3.18 +	   | SOME (thy',cls) => 
    3.19 +	       (change clause_cache (Symtab.update (name, (th, cls))); thy'))
    3.20 +    | SOME (th',cls) =>
    3.21 +        if eq_thm(th,th') then thy
    3.22 +	else (warning ("skolem_cache: Ignoring variant of theorem " ^ name); 
    3.23 +	      warning (string_of_thm th);
    3.24 +	      warning (string_of_thm th');
    3.25 +	      thy);
    3.26  
    3.27  
    3.28  (*Exported function to convert Isabelle theorems into axiom clauses*) 
    3.29  fun cnf_axiom_g cnf (name,th) =
    3.30 -    case name of
    3.31 -	  "" => cnf th (*no name, so can't cache*)
    3.32 -	| s  => case Symtab.lookup (!clause_cache) s of
    3.33 -	  	  NONE => 
    3.34 -		    let val cls = cnf th
    3.35 -		    in change clause_cache (Symtab.update (s, (th, cls))); cls end
    3.36 -	        | SOME(th',cls) =>
    3.37 -		    if eq_thm(th,th') then cls
    3.38 -		    else (*New theorem stored under the same name? Possible??*)
    3.39 -		      let val cls = cnf th
    3.40 -		      in change clause_cache (Symtab.update (s, (th, cls))); cls end;
    3.41 +  case name of
    3.42 +	"" => cnf th (*no name, so can't cache*)
    3.43 +      | s  => case Symtab.lookup (!clause_cache) s of
    3.44 +		NONE => 
    3.45 +		  let val cls = cnf th
    3.46 +		  in change clause_cache (Symtab.update (s, (th, cls))); cls end
    3.47 +	      | SOME(th',cls) =>
    3.48 +		  if eq_thm(th,th') then cls
    3.49 +		  else (warning ("cnf_axiom: duplicate or variant of theorem " ^ name); 
    3.50 +		        warning (string_of_thm th);
    3.51 +		        warning (string_of_thm th');
    3.52 +		        cls);
    3.53  
    3.54  fun pairname th = (Thm.name_of_thm th, th);
    3.55