# HG changeset patch # User paulson # Date 1161335180 -7200 # Node ID 8d0245c5ed9e43933f38a99ed01d6d22db500d7e # Parent 0a898140fea2eed06cf2f11c61d843d3c666a84c Fixed the "exception Empty" bug in elim2Fol Also added a check to suppress elimination rules that would yield too many clauses More debugging info diff -r 0a898140fea2 -r 8d0245c5ed9e src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Fri Oct 20 11:04:15 2006 +0200 +++ b/src/HOL/Tools/res_axioms.ML Fri Oct 20 11:06:20 2006 +0200 @@ -12,6 +12,7 @@ val elimR2Fol : thm -> term val transform_elim : thm -> thm val cnf_axiom : (string * thm) -> thm list + val cnf_name : string -> thm list val meta_cnf_axiom : thm -> thm list val claset_rules_of_thy : theory -> (string * thm) list val simpset_rules_of_thy : theory -> (string * thm) list @@ -96,7 +97,8 @@ if (is_neg P concl) then (strip_concl' prems bvs Q) else strip_concl (HOLogic.dest_Trueprop P::prems) bvs concl Q | strip_concl prems bvs concl Q = - if concl aconv Q then add_EX (foldr1 HOLogic.mk_conj prems) bvs + if concl aconv Q andalso not (null prems) + then add_EX (foldr1 HOLogic.mk_conj prems) bvs else raise ELIMR2FOL (*expected conclusion not found!*) fun trans_elim (major,[],_) = HOLogic.Not $ major @@ -123,11 +125,14 @@ (* convert an elim-rule into an equivalent theorem that does not have the predicate variable. Leave other theorems unchanged.*) fun transform_elim th = - let val ctm = cterm_of (sign_of_thm th) (HOLogic.mk_Trueprop (elimR2Fol th)) - in Goal.prove_raw [] ctm (fn _ => elimRule_tac th) end + let val t = HOLogic.mk_Trueprop (elimR2Fol th) + in + if Meson.too_many_clauses t then TrueI + else Goal.prove_raw [] (cterm_of (sign_of_thm th) t) (fn _ => elimRule_tac th) + end handle ELIMR2FOL => th (*not an elimination rule*) | exn => (warning ("transform_elim failed: " ^ Toplevel.exn_message exn ^ - " for theorem " ^ string_of_thm th); th) + " for theorem " ^ Thm.name_of_thm th ^ ": " ^ string_of_thm th); th) (**** Transformation of Clasets and Simpsets into First-Order Axioms ****) @@ -157,9 +162,10 @@ (*Traverse a theorem, declaring Skolem function definitions. String s is the suggested prefix for the Skolem constant. Result is a new theory*) fun declare_skofuns s th thy = - let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (thy, axs) = + let val nref = ref 0 + fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (thy, axs) = (*Existential: declare a Skolem function, then insert into body and continue*) - let val cname = Name.internal (gensym ("sko_" ^ s ^ "_")) + let val cname = Name.internal (s ^ "_sko" ^ Int.toString (inc nref)) val args = term_frees xtp (*get the formal parameter list*) val Ts = map type_of args val cT = Ts ---> T @@ -516,7 +522,6 @@ else (thy, map Drule.eta_contraction_rule ths); (*Skolemize a named theorem, with Skolem functions as additional premises.*) -(*also works for HOL*) fun skolem_thm th = let val nnfth = to_nnf th in Meson.make_cnf (skolem_of_nnf nnfth) nnfth @@ -524,10 +529,13 @@ end handle THM _ => []; +(*Keep the full complexity of the original name*) +fun flatten_name s = space_implode "_X" (NameSpace.unpack s); + (*Declare Skolem functions for a theorem, supplied in nnf and with its name. It returns a modified theory, unless skolemization fails.*) fun skolem thy (name,th) = - let val cname = (case name of "" => gensym "" | s => Sign.base_name s) + let val cname = (case name of "" => gensym "" | s => flatten_name s) val _ = Output.debug ("skolemizing " ^ name ^ ": ") in Option.map (fn nnfth => @@ -563,24 +571,32 @@ (*Exported function to convert Isabelle theorems into axiom clauses*) fun cnf_axiom (name,th) = + (Output.debug ("cnf_axiom called, theorem name = " ^ name); case name of "" => skolem_thm th (*no name, so can't cache*) | s => case Symtab.lookup (!clause_cache) s of NONE => let val cls = map Drule.local_standard (skolem_thm th) - in change clause_cache (Symtab.update (s, (th, cls))); cls end + in Output.debug "inserted into cache"; + change clause_cache (Symtab.update (s, (th, cls))); cls + end | SOME(th',cls) => if eq_thm(th,th') then cls else (Output.debug ("cnf_axiom: duplicate or variant of theorem " ^ name); Output.debug (string_of_thm th); Output.debug (string_of_thm th'); - cls); + cls) + ); fun pairname th = (Thm.name_of_thm th, th); fun meta_cnf_axiom th = map Meson.make_meta_clause (cnf_axiom (pairname th)); +(*Principally for debugging*) +fun cnf_name s = + let val th = thm s + in cnf_axiom (Thm.name_of_thm th, th) end; (**** Extract and Clausify theorems from a theory's claset and simpset ****) @@ -644,7 +660,7 @@ fun skolem_cache (name,th) thy = let val prop = Thm.prop_of th in - if lambda_free prop orelse (not abstract_lambdas andalso monomorphic prop) + if lambda_free prop (*Monomorphic theorems can be Skolemized on demand, but there are problems with re-use of abstraction functions if we don't do them now, even for monomorphic theorems.*) @@ -652,12 +668,23 @@ else #2 (skolem_cache_thm (name,th) thy) end; +(*The cache can be kept smaller by augmenting the condition above with + orelse (not abstract_lambdas andalso monomorphic prop). + However, while this step does not reduce the time needed to build HOL, + it doubles the time taken by the first call to the ATP link-up.*) + fun clause_cache_setup thy = fold skolem_cache (PureThy.all_thms_of thy) thy; (*** meson proof methods ***) -fun cnf_rules_of_ths ths = List.concat (#1 (cnf_rules (map pairname ths) [])); +fun skolem_use_cache_thm th = + case Symtab.lookup (!clause_cache) (Thm.name_of_thm th) of + NONE => skolem_thm th + | SOME (th',cls) => + if eq_thm(th,th') then cls else skolem_thm th; + +fun cnf_rules_of_ths ths = List.concat (map skolem_use_cache_thm ths); fun meson_meth ths ctxt = Method.SIMPLE_METHOD' HEADGOAL @@ -682,7 +709,7 @@ let val name = Thm.name_of_thm th val (cls, thy') = skolem_cache_thm (name, th) thy in (Context.Theory thy', conj_rule cls) end - | skolem_attr (context, th) = (context, conj_rule (skolem_thm th)); + | skolem_attr (context, th) = (context, conj_rule (skolem_use_cache_thm th)); val setup_attrs = Attrib.add_attributes [("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem")];