# HG changeset patch # User paulson # Date 1135355874 -3600 # Node ID 0a6c24f549c307c52f0d007883958b9fbf2072b7 # Parent d2d96f12a1fc361e860e8e486d2e53fb5cf98132 the "skolem" attribute and better initialization of the clause database diff -r d2d96f12a1fc -r 0a6c24f549c3 src/HOL/Main.thy --- a/src/HOL/Main.thy Fri Dec 23 17:36:00 2005 +0100 +++ b/src/HOL/Main.thy Fri Dec 23 17:37:54 2005 +0100 @@ -18,11 +18,6 @@ claset rules into the clause cache; cf.\ theory @{text Reconstruction}. *} -declare subset_refl [intro] - text {*Ensures that this important theorem is not superseded by the - simplifier's "== True" version.*} -setup ResAxioms.clause_setup -declare subset_refl [rule del] - text {*Removed again because it harms blast's performance.*} +setup ResAxioms.setup end diff -r d2d96f12a1fc -r 0a6c24f549c3 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Fri Dec 23 17:36:00 2005 +0100 +++ b/src/HOL/Tools/res_axioms.ML Fri Dec 23 17:37:54 2005 +0100 @@ -22,12 +22,13 @@ val simpset_rules_of_ctxt : Proof.context -> (string * thm) list val clausify_rules_pairs : (string*thm) list -> (ResClause.clause*thm) list list val clausify_rules_pairsH : (string*thm) list -> (ResHolClause.clause*thm) list list - val clause_setup : (theory -> theory) list - val meson_method_setup : (theory -> theory) list val pairname : thm -> (string * thm) - val cnf_axiom_aux : thm -> thm list + val skolem_thm : thm -> thm list val cnf_rules1 : (string * thm) list -> string list -> (string * thm list) list * string list val cnf_rules2 : (string * thm) list -> string list -> (string * term list) list * string list + + val meson_method_setup : (theory -> theory) list (*Reconstruction.thy*) + val setup : (theory -> theory) list (*Main.thy*) end; structure ResAxioms : RES_AXIOMS = @@ -256,7 +257,8 @@ |> ObjectLogic.atomize_thm |> make_nnf; (*The cache prevents repeated clausification of a theorem, - and also repeated declaration of Skolem functions*) (* FIXME better use Termtab!? *) + 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) @@ -264,15 +266,16 @@ fun skolem_of_nnf th = map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns th); -(*Skolemize a named theorem, returning a modified theory.*) +(*Skolemize a named theorem, with Skolem functions as additional premises.*) (*also works for HOL*) fun skolem_thm th = - Option.map (fn nnfth => Meson.make_cnf (skolem_of_nnf nnfth) nnfth) - (SOME (to_nnf th) handle THM _ => NONE); + let val nnfth = to_nnf th + in Meson.make_cnf (skolem_of_nnf nnfth) nnfth + end + handle THM _ => []; - -(*Declare Skolem functions for a theorem, supplied in nnf and with its name*) -(*in case skolemization fails, the input theory is not changed*) +(*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 "sko" | s => Sign.base_name s) in Option.map @@ -283,20 +286,23 @@ (SOME (to_nnf th) handle THM _ => NONE) end; -(*Populate the clause cache using the supplied theorems*) -fun skolem_cache ((name,th), thy) = +(*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 NONE => (case skolem thy (name, Thm.transfer thy th) of - NONE => thy + NONE => ([th],thy) | SOME (thy',cls) => - (change clause_cache (Symtab.update (name, (th, cls))); thy')) + (change clause_cache (Symtab.update (name, (th, cls))); (cls,thy'))) | SOME (th',cls) => - if eq_thm(th,th') then thy + if eq_thm(th,th') then (cls,thy) else (warning ("skolem_cache: Ignoring variant of theorem " ^ name); warning (string_of_thm th); warning (string_of_thm th'); - thy); + ([th],thy)); + +fun skolem_cache ((name,th), thy) = #2 (skolem_cache_thm ((name,th), thy)); (*Exported function to convert Isabelle theorems into axiom clauses*) @@ -317,12 +323,7 @@ fun pairname th = (Thm.name_of_thm th, th); -(*no first-order check, so works for HOL too.*) -fun cnf_axiom_aux th = Option.getOpt (skolem_thm th, []); - - - -val cnf_axiom = cnf_axiom_g cnf_axiom_aux; +val cnf_axiom = cnf_axiom_g skolem_thm; fun meta_cnf_axiom th = @@ -444,16 +445,22 @@ val clausify_rules_pairsH = clausify_rules_pairs_auxH []; +(*These should include any plausibly-useful theorems, especially if they need + Skolem functions. FIXME: this list is VERY INCOMPLETE*) +val default_initial_thms = map pairname + [refl_def, antisym_def, sym_def, trans_def, single_valued_def, + subset_refl, Union_least, Inter_greatest]; + (*Setup function: takes a theory and installs ALL simprules and claset rules into the clause cache*) fun clause_cache_setup thy = let val simps = simpset_rules_of_thy thy and clas = claset_rules_of_thy thy - in List.foldl skolem_cache (List.foldl skolem_cache thy clas) simps end; + and thy0 = List.foldl skolem_cache thy default_initial_thms + val thy1 = List.foldl skolem_cache thy0 clas + in List.foldl skolem_cache thy1 simps end; (*Could be duplicate theorem names, due to multiple attributes*) -val clause_setup = [clause_cache_setup]; - (*** meson proof methods ***) @@ -468,4 +475,28 @@ [("meson", Method.thms_ctxt_args meson_meth, "The MESON resolution proof procedure")]]; + + +(*** The Skolemization attribute ***) + +fun conj2_rule (th1,th2) = conjI OF [th1,th2]; + +(*Conjoin a list of clauses to recreate a single theorem*) +val conj_rule = foldr1 conj2_rule; + +fun skolem_global_fun (thy, th) = + let val name = Thm.name_of_thm th + val (cls,thy') = skolem_cache_thm ((name,th), thy) + in (thy', conj_rule cls) end; + +val skolem_global = Attrib.no_args skolem_global_fun; + +fun skolem_local x = Attrib.no_args (Drule.rule_attribute (K (conj_rule o skolem_thm))) x; + +val setup_attrs = Attrib.add_attributes + [("skolem", (skolem_global, skolem_local), + "skolemization of a theorem")]; + +val setup = [clause_cache_setup, setup_attrs]; + end;