# HG changeset patch # User paulson # Date 1174316282 -3600 # Node ID 7c51f1a799f35aca62270dfee30d74e0d2cb75fd # Parent 0d52e5157124cb43544b382ea8b6a4d32e515091 Removal of axiom names from the theorem cache diff -r 0d52e5157124 -r 7c51f1a799f3 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Mon Mar 19 15:57:20 2007 +0100 +++ b/src/HOL/Tools/res_axioms.ML Mon Mar 19 15:58:02 2007 +0100 @@ -415,8 +415,8 @@ (*The cache prevents repeated clausification of a theorem, and also repeated declaration of Skolem functions*) - (* FIXME better use Termtab!? No, we MUST use theory data!!*) -val clause_cache = ref (Symtab.empty : (thm * thm list) Symtab.table) + (* FIXME use theory data!!*) +val clause_cache = ref (Thmtab.empty : thm list Thmtab.table) (*Generate Skolem functions for a theorem supplied in nnf*) @@ -466,9 +466,9 @@ (*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 => flatten_name s) - val _ = Output.debug (fn () => "skolemizing " ^ name ^ ": ") +fun skolem thy th = + let val cname = (case PureThy.get_name_hint th of "" => gensym "" | s => flatten_name s) + val _ = Output.debug (fn () => "skolemizing " ^ cname ^ ": ") in Option.map (fn nnfth => let val (thy',defs) = declare_skofuns cname nnfth thy @@ -481,50 +481,31 @@ (*Populate the clause cache using the supplied theorem. Return the clausal form and modified theory.*) -fun skolem_cache_thm (name,th) thy = - case Symtab.lookup (!clause_cache) name of +fun skolem_cache_thm th thy = + case Thmtab.lookup (!clause_cache) th of NONE => - (case skolem thy (name, Thm.transfer thy th) of + (case skolem thy (Thm.transfer thy th) of NONE => ([th],thy) | SOME (cls,thy') => - (if null cls then warning ("skolem_cache: empty clause set for " ^ name) + (if null cls + then warning ("skolem_cache: empty clause set for " ^ string_of_thm th) else (); - change clause_cache (Symtab.update (name, (th, cls))); + change clause_cache (Thmtab.update (th, cls)); (cls,thy'))) - | SOME (th',cls) => - if Thm.eq_thm(th,th') then (cls,thy) - else (Output.debug (fn () => "skolem_cache: Ignoring variant of theorem " ^ name); - Output.debug (fn () => string_of_thm th); - Output.debug (fn () => string_of_thm th'); - getOpt (skolem thy (name, Thm.transfer thy th), ([th],thy))); + | SOME cls => (cls,thy); (*Exported function to convert Isabelle theorems into axiom clauses*) -fun cnf_axiom (name,th) = - (Output.debug (fn () => "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 Goal.close_result (skolem_thm th) - in Output.debug (fn () => "inserted into cache"); - change clause_cache (Symtab.update (s, (th, cls))); cls - end - | SOME(th',cls) => - if Thm.eq_thm(th,th') then cls - else - (Output.debug (fn () => "cnf_axiom: duplicate or variant of theorem " ^ name); - Output.debug (fn () => string_of_thm th); - Output.debug (fn () => string_of_thm th'); - skolem_thm th) - ); +fun cnf_axiom th = + case Thmtab.lookup (!clause_cache) th of + NONE => + let val cls = map Goal.close_result (skolem_thm th) + in Output.debug (fn () => "inserted into cache"); + change clause_cache (Thmtab.update (th, cls)); cls + end + | SOME cls => cls; fun pairname th = (PureThy.get_name_hint th, th); -(*Principally for debugging*) -fun cnf_name s = - let val th = thm s - in cnf_axiom (PureThy.get_name_hint th, th) end; - (**** Extract and Clausify theorems from a theory's claset and simpset ****) fun rules_of_claset cs = @@ -551,20 +532,20 @@ fun atpset_rules_of ctxt = map pairname (ResAtpset.get_atpset ctxt); -(**** Translate a set of classical/simplifier rules into CNF (still as type "thm") ****) +(**** Translate a set of theorems into CNF ****) (* classical rules: works for both FOL and HOL *) fun cnf_rules [] err_list = ([],err_list) | cnf_rules ((name,th) :: ths) err_list = let val (ts,es) = cnf_rules ths err_list - in (cnf_axiom (name,th) :: ts,es) handle _ => (ts, (th::es)) end; + in (cnf_axiom th :: ts,es) handle _ => (ts, (th::es)) end; fun pair_name_cls k (n, []) = [] | pair_name_cls k (n, cls::clss) = (cls, (n,k)) :: pair_name_cls (k+1) (n, clss) fun cnf_rules_pairs_aux pairs [] = pairs | cnf_rules_pairs_aux pairs ((name,th)::ths) = - let val pairs' = (pair_name_cls 0 (name, cnf_axiom(name,th))) @ pairs + let val pairs' = (pair_name_cls 0 (name, cnf_axiom th)) @ pairs handle THM _ => pairs | ResClause.CLAUSE _ => pairs in cnf_rules_pairs_aux pairs' ths end; @@ -576,7 +557,7 @@ (*Setup function: takes a theory and installs ALL known theorems into the clause cache*) -fun skolem_cache (name,th) thy = +fun skolem_cache th thy = let val prop = Thm.prop_of th in if lambda_free prop @@ -584,7 +565,7 @@ but there are problems with re-use of abstraction functions if we don't do them now, even for monomorphic theorems.*) then thy - else #2 (skolem_cache_thm (name,th) thy) + else #2 (skolem_cache_thm th thy) end; (*The cache can be kept smaller by augmenting the condition above with @@ -592,16 +573,15 @@ 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; +fun clause_cache_setup thy = fold skolem_cache (map #2 (PureThy.all_thms_of thy)) thy; (*** meson proof methods ***) fun skolem_use_cache_thm th = - case Symtab.lookup (!clause_cache) (PureThy.get_name_hint th) of + case Thmtab.lookup (!clause_cache) th of NONE => skolem_thm th - | SOME (th',cls) => - if Thm.eq_thm(th,th') then cls else skolem_thm th; + | SOME cls => cls; fun cnf_rules_of_ths ths = List.concat (map skolem_use_cache_thm ths); @@ -612,7 +592,7 @@ (** Attribute for converting a theorem into clauses **) -fun meta_cnf_axiom th = map Meson.make_meta_clause (cnf_axiom (pairname th)); +fun meta_cnf_axiom th = map Meson.make_meta_clause (cnf_axiom th); fun clausify_rule (th,i) = List.nth (meta_cnf_axiom th, i) @@ -623,7 +603,10 @@ (*** Converting a subgoal into negated conjecture clauses. ***) val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac]; -val neg_clausify = Meson.finish_cnf o assume_abstract_list o make_clauses; + +(*finish_cnf removes tautologies and functional reflexivity axioms, but by calling Thm.varifyT + it can introduce TVars, which we don't want in conjecture clauses.*) +val neg_clausify = map Thm.freezeT o Meson.finish_cnf o assume_abstract_list o make_clauses; fun neg_conjecture_clauses st0 n = let val st = Seq.hd (neg_skolemize_tac n st0) @@ -654,8 +637,7 @@ | conj_rule ths = foldr1 conj2_rule ths; fun skolem_attr (Context.Theory thy, th) = - let val name = PureThy.get_name_hint th - val (cls, thy') = skolem_cache_thm (name, th) thy + let val (cls, thy') = skolem_cache_thm th thy in (Context.Theory thy', conj_rule cls) end | skolem_attr (context, th) = (context, conj_rule (skolem_use_cache_thm th));