# HG changeset patch # User wenzelm # Date 1213302591 -7200 # Node ID b1483d423512074ca07eca7c8a4a5356a376a166 # Parent 0fc4c0f97a1b4db7595b9566f0af49c81660df38 export just one setup function; more antiquotations; to_nnf: import open, avoiding internal variables (bounds); ThmCache: added table of seen fact names; reorganized skolem_thm/skolem_fact/saturate_skolem_cache: maintain seen fact names, ensure idempotent operation for Theory.at_end; removed obsolete skolem attribute (NB: official fact name unavailable here); diff -r 0fc4c0f97a1b -r b1483d423512 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Thu Jun 12 22:29:50 2008 +0200 +++ b/src/HOL/Tools/res_axioms.ML Thu Jun 12 22:29:51 2008 +0200 @@ -9,7 +9,7 @@ sig val cnf_axiom: theory -> thm -> thm list val pairname: thm -> string * thm - val multi_base_blacklist: string list + val multi_base_blacklist: string list val bad_for_atp: thm -> bool val type_has_empty_sort: typ -> bool val cnf_rules_pairs: theory -> (string * thm) list -> (thm * (string * int)) list @@ -20,8 +20,6 @@ val claset_rules_of: Proof.context -> (string * thm) list (*FIXME DELETE*) val simpset_rules_of: Proof.context -> (string * thm) list (*FIXME DELETE*) val atpset_rules_of: Proof.context -> (string * thm) list - val meson_method_setup: theory -> theory - val clause_cache_endtheory: theory -> theory option val suppress_endtheory: bool ref (*for emergency use where endtheory causes problems*) val setup: theory -> theory end; @@ -36,7 +34,7 @@ | type_has_empty_sort (TVar (_, [])) = true | type_has_empty_sort (Type (_, Ts)) = exists type_has_empty_sort Ts | type_has_empty_sort _ = false; - + (**** Transformation of Elimination Rules into First-Order Formulas****) val cfalse = cterm_of HOL.thy HOLogic.false_const; @@ -161,15 +159,9 @@ val monomorphic = not o Term.exists_type (Term.exists_subtype Term.is_TVar); -val abs_S = @{thm"abs_S"}; -val abs_K = @{thm"abs_K"}; -val abs_I = @{thm"abs_I"}; -val abs_B = @{thm"abs_B"}; -val abs_C = @{thm"abs_C"}; - -val [f_B,g_B] = map (cterm_of @{theory}) (term_vars (prop_of abs_B)); -val [g_C,f_C] = map (cterm_of @{theory}) (term_vars (prop_of abs_C)); -val [f_S,g_S] = map (cterm_of @{theory}) (term_vars (prop_of abs_S)); +val [f_B,g_B] = map (cterm_of @{theory}) (term_vars (prop_of @{thm abs_B})); +val [g_C,f_C] = map (cterm_of @{theory}) (term_vars (prop_of @{thm abs_C})); +val [f_S,g_S] = map (cterm_of @{theory}) (term_vars (prop_of @{thm abs_S})); (*FIXME: requires more use of cterm constructors*) fun abstract ct = @@ -178,37 +170,37 @@ val thy = theory_of_cterm ct val Type("fun",[xT,bodyT]) = typ_of (ctyp_of_term ct) val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT - fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] abs_K + fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] @{thm abs_K} in case body of Const _ => makeK() | Free _ => makeK() | Var _ => makeK() (*though Var isn't expected*) - | Bound 0 => instantiate' [SOME cxT] [] abs_I (*identity: I*) + | Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*) | rator$rand => - if loose_bvar1 (rator,0) then (*C or S*) + if loose_bvar1 (rator,0) then (*C or S*) if loose_bvar1 (rand,0) then (*S*) let val crator = cterm_of thy (Abs(x,xT,rator)) val crand = cterm_of thy (Abs(x,xT,rand)) - val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] abs_S - val (_,rhs) = Thm.dest_equals (cprop_of abs_S') + val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S} + val (_,rhs) = Thm.dest_equals (cprop_of abs_S') in Thm.transitive abs_S' (Conv.binop_conv abstract rhs) end else (*C*) let val crator = cterm_of thy (Abs(x,xT,rator)) - val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] abs_C - val (_,rhs) = Thm.dest_equals (cprop_of abs_C') + val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] @{thm abs_C} + val (_,rhs) = Thm.dest_equals (cprop_of abs_C') in Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs) end - else if loose_bvar1 (rand,0) then (*B or eta*) + else if loose_bvar1 (rand,0) then (*B or eta*) if rand = Bound 0 then eta_conversion ct else (*B*) let val crand = cterm_of thy (Abs(x,xT,rand)) val crator = cterm_of thy rator - val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] abs_B - val (_,rhs) = Thm.dest_equals (cprop_of abs_B') + val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B} + val (_,rhs) = Thm.dest_equals (cprop_of abs_B') in Thm.transitive abs_B' (Conv.arg_conv abstract rhs) end @@ -235,16 +227,16 @@ | t1 $ t2 => let val (ct1,ct2) = Thm.dest_comb ct in combination (combinators_aux ct1) (combinators_aux ct2) end; - + fun combinators th = - if lambda_free (prop_of th) then th + if lambda_free (prop_of th) then th else let val _ = Output.debug (fn()=>"Conversion to combinators: " ^ Display.string_of_thm th); val th = Drule.eta_contraction_rule th val eqth = combinators_aux (cprop_of th) val _ = Output.debug (fn()=>"Conversion result: " ^ Display.string_of_thm eqth); in equal_elim eqth th end - handle THM (msg,_,_) => + handle THM (msg,_,_) => (warning ("Error in the combinator translation of " ^ Display.string_of_thm th); warning (" Exception message: " ^ msg); TrueI); (*A type variable of sort {} will cause make abstraction fail.*) @@ -287,7 +279,7 @@ (*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*) fun to_nnf th ctxt0 = let val th1 = th |> transform_elim |> zero_var_indexes - val ((_,[th2]),ctxt) = Variable.import_thms false [th1] ctxt0 + val ((_,[th2]),ctxt) = Variable.import_thms true [th1] ctxt0 val th3 = th2 |> Conv.fconv_rule ObjectLogic.atomize |> Meson.make_nnf |> strip_lambdas ~1 in (th3, ctxt) end; @@ -301,10 +293,10 @@ | ths' => error (msg ^ "\n" ^ cat_lines (map Display.string_of_thm ths')); -(*** Blacklisting (duplicated in ResAtp? ***) +(*** Blacklisting (duplicated in ResAtp?) ***) val max_lambda_nesting = 3; - + fun excessive_lambdas (f$t, k) = excessive_lambdas (f,k) orelse excessive_lambdas (t,k) | excessive_lambdas (Abs(_,_,t), k) = k=0 orelse excessive_lambdas (t,k-1) | excessive_lambdas _ = false; @@ -320,25 +312,25 @@ (*The max apply_depth of any metis call in MetisExamples (on 31-10-2007) was 11.*) val max_apply_depth = 15; - + fun apply_depth (f$t) = Int.max (apply_depth f, apply_depth t + 1) | apply_depth (Abs(_,_,t)) = apply_depth t | apply_depth _ = 0; -fun too_complex t = - apply_depth t > max_apply_depth orelse +fun too_complex t = + apply_depth t > max_apply_depth orelse Meson.too_many_clauses NONE t orelse excessive_lambdas_fm [] t; - + fun is_strange_thm th = case head_of (concl_of th) of Const (a,_) => (a <> "Trueprop" andalso a <> "==") | _ => false; -fun bad_for_atp th = - PureThy.is_internal th - orelse too_complex (prop_of th) - orelse exists_type type_has_empty_sort (prop_of th) +fun bad_for_atp th = + PureThy.is_internal th + orelse too_complex (prop_of th) + orelse exists_type type_has_empty_sort (prop_of th) orelse is_strange_thm th; val multi_base_blacklist = @@ -356,78 +348,66 @@ if PureThy.has_name_hint th then PureThy.get_name_hint th else Display.string_of_thm th; +(*Skolemize a named theorem, with Skolem functions as additional premises.*) +fun skolem_thm (s, th) = + if member (op =) multi_base_blacklist (Sign.base_name s) orelse bad_for_atp th then [] + else + let + val ctxt0 = Variable.thm_context th + val (nnfth, ctxt1) = to_nnf th ctxt0 + val (cnfs, ctxt2) = Meson.make_cnf (assume_skolem_of_def s nnfth) nnfth ctxt1 + in cnfs |> map combinators |> Variable.export ctxt2 ctxt0 |> Meson.finish_cnf end + handle THM _ => []; + (*Declare Skolem functions for a theorem, supplied in nnf and with its name. It returns a modified theory, unless skolemization fails.*) -fun skolem th0 thy = +fun skolem (name, th0) thy = let val th = Thm.transfer thy th0 val ctxt0 = Variable.thm_context th - val _ = Output.debug (fn () => "skolemizing " ^ name_or_string th) in - Option.map - (fn (nnfth,ctxt1) => - let - val _ = Output.debug (fn () => " initial nnf: " ^ Display.string_of_thm nnfth) - val s = fake_name th - val (defs,thy') = declare_skofuns s nnfth thy - val (cnfs,ctxt2) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt1 - val _ = Output.debug (fn () => Int.toString (length cnfs) ^ " clauses yielded") - val cnfs' = cnfs |> map combinators |> Variable.export ctxt2 ctxt0 - |> Meson.finish_cnf |> map Thm.close_derivation - in (cnfs', thy') end - handle Clausify_failure thy_e => ([],thy_e) - ) - (try (to_nnf th) ctxt0) + try (to_nnf th) ctxt0 |> Option.map (fn (nnfth, ctxt1) => + let + val s = flatten_name name + val (defs, thy') = declare_skofuns s nnfth thy + val (cnfs, ctxt2) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt1 + val cnfs' = cnfs |> map combinators |> Variable.export ctxt2 ctxt0 + |> Meson.finish_cnf |> map Thm.close_derivation + in (cnfs', thy') end + handle Clausify_failure thy_e => ([], thy_e)) (* FIXME !? *) end; (*The cache prevents repeated clausification of a theorem, and also repeated declaration of Skolem functions.*) structure ThmCache = TheoryDataFun ( - type T = thm list Thmtab.table; - val empty = Thmtab.empty; + type T = thm list Thmtab.table * unit Symtab.table + val empty = (Thmtab.empty, Symtab.empty) val copy = I; val extend = I; - fun merge _ tabs : T = Thmtab.merge (K true) tabs; + fun merge _ ((cache1, seen1), (cache2, seen2)) : T = + (Thmtab.merge (K true) (cache1, cache2), Symtab.merge (K true) (seen1, seen2)); ); -(*Populate the clause cache using the supplied theorem. Return the clausal form - and modified theory.*) -fun skolem_cache_thm th thy = - case Thmtab.lookup (ThmCache.get thy) th of - NONE => - (case skolem th thy of - NONE => ([th],thy) - | SOME (cls,thy') => - (Output.debug (fn () => "skolem_cache_thm: " ^ Int.toString (length cls) ^ - " clauses inserted into cache: " ^ name_or_string th); - (cls, ThmCache.map (Thmtab.update (th,cls)) thy'))) - | SOME cls => (cls,thy); +val lookup_cache = Thmtab.lookup o #1 o ThmCache.get; +val already_seen = Symtab.defined o #2 o ThmCache.get; -(*Skolemize a named theorem, with Skolem functions as additional premises.*) -fun skolem_thm (s,th) = - if (Sign.base_name s) mem_string multi_base_blacklist orelse bad_for_atp th then [] - else - let val ctxt0 = Variable.thm_context th - val (nnfth,ctxt1) = to_nnf th ctxt0 - val (cnfs,ctxt2) = Meson.make_cnf (assume_skolem_of_def s nnfth) nnfth ctxt1 - in cnfs |> map combinators |> Variable.export ctxt2 ctxt0 |> Meson.finish_cnf end - handle THM _ => []; +val update_cache = ThmCache.map o apfst o Thmtab.update; +fun mark_seen name = ThmCache.map (apsnd (Symtab.update (name, ()))); (*Exported function to convert Isabelle theorems into axiom clauses*) fun cnf_axiom thy th0 = - let val th = Thm.transfer thy th0 - in - case Thmtab.lookup (ThmCache.get thy) th of - NONE => (Output.debug (fn () => "cnf_axiom: " ^ name_or_string th); - map Thm.close_derivation (skolem_thm (fake_name th, th))) - | SOME cls => cls + let val th = Thm.transfer thy th0 in + case lookup_cache thy th of + NONE => map Thm.close_derivation (skolem_thm (fake_name th, th)) + | SOME cls => cls end; -fun pairname th = (PureThy.get_name_hint th, th); (**** Extract and Clausify theorems from a theory's claset and simpset ****) +fun pairname th = (PureThy.get_name_hint th, th); + fun rules_of_claset cs = let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs val intros = safeIs @ hazIs @@ -467,35 +447,41 @@ fun cnf_rules_pairs thy l = cnf_rules_pairs_aux thy [] (rev l); -(**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****) +(**** Convert all facts of the theory into clauses (ResClause.clause, or ResHolClause.clause) ****) -(*Setup function: takes a theory and installs ALL known theorems into the clause cache*) - -val mark_skolemized = Sign.add_consts_i [("ResAxioms_endtheory", HOLogic.boolT, NoSyn)]; +(*Populate the clause cache using the supplied theorem. Return the clausal form + and modified theory.*) +fun skolem_cache_thm (name, th) thy = + if bad_for_atp th then thy + else + (case lookup_cache thy th of + SOME _ => thy + | NONE => + (case skolem (name, th) thy of + NONE => thy + | SOME (cls, thy') => update_cache (th, cls) thy')); -fun skolem_cache th thy = - if bad_for_atp th then thy else #2 (skolem_cache_thm th thy); +fun skolem_cache_fact (name, ths) (changed, thy) = + if (Sign.base_name name) mem_string multi_base_blacklist orelse already_seen thy name + then (changed, thy) + else (true, thy |> mark_seen name |> fold skolem_cache_thm (PureThy.name_multi name ths)); -fun skolem_cache_list (a,ths) thy = - if (Sign.base_name a) mem_string multi_base_blacklist then thy - else fold skolem_cache ths thy; +fun saturate_skolem_cache thy = + (case Facts.fold_static skolem_cache_fact (PureThy.facts_of thy) (false, thy) of + (false, _) => NONE + | (true, thy') => SOME thy'); + -val skolem_cache_theorems_of = Symtab.fold skolem_cache_list o #2 o PureThy.theorems_of; -fun skolem_cache_node thy = skolem_cache_theorems_of thy thy; -fun skolem_cache_all thy = fold skolem_cache_theorems_of (thy :: Theory.ancestors_of thy) thy; +val suppress_endtheory = ref false; + +fun clause_cache_endtheory thy = + if ! suppress_endtheory then NONE + else saturate_skolem_cache thy; + (*The cache can be kept smaller by inspecting the prop of each thm. Can ignore all that are lambda_free, but then the individual theory caches become much bigger.*) -val suppress_endtheory = ref false; - -(*The new constant is a hack to prevent multiple execution*) -fun clause_cache_endtheory thy = - if !suppress_endtheory then NONE - else - (Output.debug (fn () => "RexAxioms end theory action: " ^ Context.str_of_thy thy); - Option.map skolem_cache_node (try mark_skolemized thy) ); - (*** meson proof methods ***) @@ -538,13 +524,6 @@ "MESON resolution proof procedure")]; -(** Attribute for converting a theorem into clauses **) - -val clausify = Attrib.syntax (Scan.lift Args.nat - >> (fn i => Thm.rule_attribute (fn context => fn th => - Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i)))); - - (*** Converting a subgoal into negated conjecture clauses. ***) val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac]; @@ -573,28 +552,30 @@ REPEAT_DETERM_N (length ts) o (etac thin_rl)] end); - -(** The Skolemization attribute **) - -fun conj2_rule (th1,th2) = conjI OF [th1,th2]; - -(*Conjoin a list of theorems to form a single theorem*) -fun conj_rule [] = TrueI - | conj_rule ths = foldr1 conj2_rule ths; - -fun skolem_attr (Context.Theory thy, th) = - let val (cls, thy') = skolem_cache_thm th thy - in (Context.Theory thy', conj_rule cls) end - | skolem_attr (context, th) = (context, th) - -val setup_attrs = Attrib.add_attributes - [("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem"), - ("clausify", clausify, "conversion of theorem to clauses")]; - val setup_methods = Method.add_methods [("neg_clausify", Method.no_args (Method.SIMPLE_METHOD' neg_clausify_tac), "conversion of goal to conjecture clauses")]; -val setup = mark_skolemized #> skolem_cache_all #> ThmCache.init #> setup_attrs #> setup_methods; + +(** Attribute for converting a theorem into clauses **) + +val clausify = Attrib.syntax (Scan.lift Args.nat + >> (fn i => Thm.rule_attribute (fn context => fn th => + Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i)))); + +val setup_attrs = Attrib.add_attributes + [("clausify", clausify, "conversion of theorem to clauses")]; + + + +(** setup **) + +val setup = + meson_method_setup #> + setup_methods #> + setup_attrs #> + perhaps saturate_skolem_cache #> + Theory.at_end clause_cache_endtheory; end; +