# HG changeset patch # User blanchet # Date 1277739148 -7200 # Node ID f73cd4069f6973c0eaea2793786421bea7797f6e # Parent c8d2d84d60111b20c7177b71eec2d8ca159329b1 always perform "inline" skolemization, polymorphism or not, Skolem cache or not diff -r c8d2d84d6011 -r f73cd4069f69 src/HOL/Tools/Sledgehammer/clausifier.ML --- a/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Jun 28 17:31:38 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Jun 28 17:32:28 2010 +0200 @@ -92,92 +92,39 @@ else (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length -fun rhs_extra_types lhsT rhs = - let val lhs_vars = Term.add_tfreesT lhsT [] - fun add_new_TFrees (TFree v) = - if member (op =) lhs_vars v then I else insert (op =) (TFree v) - | add_new_TFrees _ = I - val rhs_consts = fold_aterms (fn Const c => insert (op =) c | _ => I) rhs [] - in fold (#2 #> Term.fold_atyps add_new_TFrees) rhs_consts [] end; - -fun skolem_type_and_args bound_T body = - let - val args1 = OldTerm.term_frees body - val Ts1 = map type_of args1 - val Ts2 = rhs_extra_types (Ts1 ---> bound_T) body - val args2 = map (fn T => Free (gensym "vsk", T)) Ts2 - in (Ts2 ---> Ts1 ---> bound_T, args2 @ args1) end - -(* Traverse a theorem, declaring Skolem function definitions. String "s" is the - suggested prefix for the Skolem constants. *) -fun declare_skolem_funs s th thy = - let - val skolem_count = Unsynchronized.ref 0 (* FIXME ??? *) - fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p))) - (axs, thy) = - (*Existential: declare a Skolem function, then insert into body and continue*) - let - val id = skolem_name s (Unsynchronized.inc skolem_count) s' - val (cT, args) = skolem_type_and_args T body - val rhs = list_abs_free (map dest_Free args, - HOLogic.choice_const T $ body) - (*Forms a lambda-abstraction over the formal parameters*) - val (c, thy) = - Sign.declare_const ((Binding.conceal (Binding.name id), cT), NoSyn) thy - val cdef = id ^ "_def" - val ((_, ax), thy) = - Thm.add_def true false (Binding.name cdef, Logic.mk_equals (c, rhs)) thy - val ax' = Drule.export_without_context ax - in dec_sko (subst_bound (list_comb (c, args), p)) (ax' :: axs, thy) end - | dec_sko (Const (@{const_name All}, _) $ (Abs (a, T, p))) thx = - (*Universal quant: insert a free variable into body and continue*) - let val fname = Name.variant (OldTerm.add_term_names (p, [])) a - in dec_sko (subst_bound (Free (fname, T), p)) thx end - | dec_sko (@{const "op &"} $ p $ q) thx = dec_sko q (dec_sko p thx) - | dec_sko (@{const "op |"} $ p $ q) thx = dec_sko q (dec_sko p thx) - | dec_sko (@{const Trueprop} $ p) thx = dec_sko p thx - | dec_sko _ thx = thx - in dec_sko (prop_of th) ([], thy) end - fun mk_skolem_id t = let val T = fastype_of t in Const (@{const_name skolem_id}, T --> T) $ t end -fun quasi_beta_eta_contract (Abs (s, T, t')) = - Abs (s, T, quasi_beta_eta_contract t') - | quasi_beta_eta_contract t = Envir.beta_eta_contract t +fun beta_eta_under_lambdas (Abs (s, T, t')) = + Abs (s, T, beta_eta_under_lambdas t') + | beta_eta_under_lambdas t = Envir.beta_eta_contract t (*Traverse a theorem, accumulating Skolem function definitions.*) -fun assume_skolem_funs s th = +fun assume_skolem_funs th = let - val skolem_count = Unsynchronized.ref 0 (* FIXME ??? *) - fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p))) defs = + fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p))) rhss = (*Existential: declare a Skolem function, then insert into body and continue*) let - val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*) - val args = subtract (op =) skos (OldTerm.term_frees body) (*the formal parameters*) + val args = OldTerm.term_frees body val Ts = map type_of args val cT = Ts ---> T (* FIXME: use "skolem_type_and_args" *) - val id = skolem_name s (Unsynchronized.inc skolem_count) s' - val c = Free (id, cT) (* FIXME: needed? ### *) (* Forms a lambda-abstraction over the formal parameters *) val rhs = list_abs_free (map dest_Free args, - HOLogic.choice_const T - $ quasi_beta_eta_contract body) + HOLogic.choice_const T $ beta_eta_under_lambdas body) |> mk_skolem_id - val def = Logic.mk_equals (c, rhs) val comb = list_comb (rhs, args) - in dec_sko (subst_bound (comb, p)) (def :: defs) end - | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) defs = + in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end + | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss = (*Universal quant: insert a free variable into body and continue*) let val fname = Name.variant (OldTerm.add_term_names (p,[])) a - in dec_sko (subst_bound (Free(fname,T), p)) defs end - | dec_sko (@{const "op &"} $ p $ q) defs = dec_sko q (dec_sko p defs) - | dec_sko (@{const "op |"} $ p $ q) defs = dec_sko q (dec_sko p defs) - | dec_sko (@{const Trueprop} $ p) defs = dec_sko p defs - | dec_sko _ defs = defs + in dec_sko (subst_bound (Free(fname,T), p)) rhss end + | dec_sko (@{const "op &"} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q + | dec_sko (@{const "op |"} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q + | dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss + | dec_sko _ rhss = rhss in dec_sko (prop_of th) [] end; @@ -286,9 +233,6 @@ (*cterms are used throughout for efficiency*) val cTrueprop = Thm.cterm_of @{theory HOL} HOLogic.Trueprop; -(*cterm version of mk_cTrueprop*) -fun c_mkTrueprop A = Thm.capply cTrueprop A; - (*Given an abstraction over n variables, replace the bound variables by free ones. Return the body, along with the list of free variables.*) fun c_variant_abs_multi (ct0, vars) = @@ -296,38 +240,36 @@ in c_variant_abs_multi (ct, cv::vars) end handle CTERM _ => (ct0, rev vars); -(*Given the definition of a Skolem function, return a theorem to replace - an existential formula by a use of that function. +val skolem_id_def_raw = @{thms skolem_id_def_raw} + +(* Given the definition of a Skolem function, return a theorem to replace + an existential formula by a use of that function. Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *) -fun skolem_theorem_of_def inline def = +fun skolem_theorem_of_def thy rhs0 = let - val (c, rhs) = def |> Drule.legacy_freeze_thaw |> #1 |> cprop_of - |> Thm.dest_equals - val rhs' = rhs |> inline ? (snd o Thm.dest_comb) - val (ch, frees) = c_variant_abs_multi (rhs', []) - val (chilbert, cabs) = ch |> Thm.dest_comb - val thy = Thm.theory_of_cterm chilbert - val t = Thm.term_of chilbert - val T = - case t of - Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T - | _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [t]) - val cex = Thm.cterm_of thy (HOLogic.exists_const T) - val ex_tm = c_mkTrueprop (Thm.capply cex cabs) - and conc = - Drule.list_comb (if inline then rhs else c, frees) - |> Drule.beta_conv cabs |> c_mkTrueprop - fun tacf [prem] = - (if inline then rewrite_goals_tac @{thms skolem_id_def_raw} - else rewrite_goals_tac [def]) - THEN rtac ((prem |> inline ? rewrite_rule @{thms skolem_id_def_raw}) - RS @{thm someI_ex}) 1 - in Goal.prove_internal [ex_tm] conc tacf - |> forall_intr_list frees - |> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*) - |> Thm.varifyT_global - end; - + val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> Thm.cterm_of thy + val rhs' = rhs |> Thm.dest_comb |> snd + val (ch, frees) = c_variant_abs_multi (rhs', []) + val (hilbert, cabs) = ch |> Thm.dest_comb |>> term_of + val T = + case hilbert of + Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T + | _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [hilbert]) + val cex = Thm.cterm_of thy (HOLogic.exists_const T) + val ex_tm = Thm.capply cTrueprop (Thm.capply cex cabs) + and conc = + Drule.list_comb (rhs, frees) + |> Drule.beta_conv cabs |> Thm.capply cTrueprop + fun tacf [prem] = + rewrite_goals_tac skolem_id_def_raw + THEN rtac ((prem |> rewrite_rule skolem_id_def_raw) + RS @{thm someI_ex}) 1 + in + Goal.prove_internal [ex_tm] conc tacf + |> forall_intr_list frees + |> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*) + |> Thm.varifyT_global + end (*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*) fun to_nnf th ctxt0 = @@ -338,12 +280,6 @@ |> Meson.make_nnf ctxt in (th3, ctxt) end; -(*Generate Skolem functions for a theorem supplied in nnf*) -fun skolem_theorems_of_assume s th = - map (skolem_theorem_of_def true o Thm.assume o cterm_of (theory_of_thm th)) - (assume_skolem_funs s th) - - (*** Blacklisting (more in "Sledgehammer_Fact_Filter") ***) val max_lambda_nesting = 3 @@ -396,25 +332,23 @@ ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits", "split_asm", "cases", "ext_cases"]; -fun fake_name th = - if Thm.has_name_hint th then flatten_name (Thm.get_name_hint th) - else gensym "unknown_thm_"; - (*Skolemize a named theorem, with Skolem functions as additional premises.*) -fun skolemize_theorem s th = - if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse +fun skolemize_theorem thy th = + if member (op =) multi_base_blacklist + (Long_Name.base_name (Thm.get_name_hint th)) orelse is_theorem_bad_for_atps th then [] else let val ctxt0 = Variable.global_thm_context th val (nnfth, ctxt) = to_nnf th ctxt0 - val defs = skolem_theorems_of_assume s nnfth - val (cnfs, ctxt) = Meson.make_cnf defs nnfth ctxt + val sko_ths = map (skolem_theorem_of_def thy) (assume_skolem_funs nnfth) + val (cnfs, ctxt) = Meson.make_cnf sko_ths nnfth ctxt in cnfs |> map introduce_combinators |> Variable.export ctxt ctxt0 |> Meson.finish_cnf + |> map Thm.close_derivation end handle THM _ => [] @@ -429,19 +363,13 @@ (Thmtab.merge (K true) (cache1, cache2), Symtab.merge (K true) (seen1, seen2)); ); -val lookup_cache = Thmtab.lookup o #1 o ThmCache.get; -val already_seen = Symtab.defined o #2 o ThmCache.get; - -val update_cache = ThmCache.map o apfst o Thmtab.update; -fun mark_seen name = ThmCache.map (apsnd (Symtab.update (name, ()))); - (* Convert Isabelle theorems into axiom clauses. *) fun cnf_axiom thy th0 = let val th = Thm.transfer thy th0 in - case lookup_cache thy th of + case Thmtab.lookup (#1 (ThmCache.get thy)) th of SOME cls => cls - | NONE => map Thm.close_derivation (skolemize_theorem (fake_name th) th) - end; + | NONE => skolemize_theorem thy th + end (**** Translate a set of theorems into CNF ****) @@ -463,60 +391,34 @@ (**** Convert all facts of the theory into FOL or HOL clauses ****) -local - -fun skolem_def (name, th) thy = - let val ctxt0 = Variable.global_thm_context th in - case try (to_nnf th) ctxt0 of - NONE => (NONE, thy) - | SOME (nnfth, ctxt) => - let val (defs, thy') = declare_skolem_funs (flatten_name name) nnfth thy - in (SOME (th, ctxt0, ctxt, nnfth, defs), thy') end - end; - -fun skolem_cnfs (th, ctxt0, ctxt, nnfth, defs) = - let - val (cnfs, ctxt) = - Meson.make_cnf (map (skolem_theorem_of_def false) defs) nnfth ctxt - val cnfs' = cnfs - |> map introduce_combinators - |> Variable.export ctxt ctxt0 - |> Meson.finish_cnf - |> map Thm.close_derivation; - in (th, cnfs') end; - -in - fun saturate_cache thy = let - val facts = PureThy.facts_of thy; + val (cache, seen) = ThmCache.get thy + val facts = PureThy.facts_of thy val new_facts = (facts, []) |-> Facts.fold_static (fn (name, ths) => - if Facts.is_concealed facts name orelse already_seen thy name then I - else cons (name, ths)); + if Facts.is_concealed facts name orelse Symtab.defined seen name then I + else cons (name, ths)) val new_thms = (new_facts, []) |-> fold (fn (name, ths) => if member (op =) multi_base_blacklist (Long_Name.base_name name) then I else fold_index (fn (i, th) => - if is_theorem_bad_for_atps th orelse - is_some (lookup_cache thy th) then + if is_theorem_bad_for_atps th orelse Thmtab.defined cache th then I else cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths) + val entries = + Par_List.map (fn (_, th) => (th, skolemize_theorem thy th)) + (sort_distinct (Thm.thm_ord o pairself snd) new_thms) in - if null new_facts then + if null entries then NONE else - let - val (defs, thy') = thy - |> fold (mark_seen o #1) new_facts - |> fold_map skolem_def (sort_distinct (Thm.thm_ord o pairself snd) new_thms) - |>> map_filter I; - val cache_entries = Par_List.map skolem_cnfs defs; - in SOME (fold update_cache cache_entries thy') end - end; - -end; + thy |> ThmCache.map (fn p => p |>> fold Thmtab.update entries + ||> fold Symtab.update + (map (rpair () o #1) new_facts)) + |> SOME + end (* For emergency use where the Skolem cache causes problems. *) val auto_saturate_cache = Unsynchronized.ref true diff -r c8d2d84d6011 -r f73cd4069f69 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jun 28 17:31:38 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jun 28 17:32:28 2010 +0200 @@ -194,8 +194,7 @@ (* Sledgehammer the given subgoal *) fun run {atps = [], ...} _ _ _ _ = error "No ATP is set." - | run (params as {atps, timeout, ...}) i relevance_override minimize_command - state = + | run (params as {atps, ...}) i relevance_override minimize_command state = case subgoal_count state of 0 => priority "No subgoal!" | n => diff -r c8d2d84d6011 -r f73cd4069f69 src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Mon Jun 28 17:31:38 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Mon Jun 28 17:32:28 2010 +0200 @@ -190,25 +190,24 @@ (* Find the minimal arity of each function mentioned in the term. Also, note which uses are not at top level, to see if "hBOOL" is needed. *) -fun count_constants_term top_level t the_const_tab = - let - val (head, args) = strip_combterm_comb t - val n = length args - val the_const_tab = the_const_tab |> fold (count_constants_term false) args - in - case head of - CombConst ((a, _), _, ty) => - (* Predicate or function version of "equal"? *) - let val a = if a = "equal" andalso not top_level then "c_fequal" else a in - the_const_tab - |> Symtab.map_default - (a, {min_arity = n, max_arity = n, sub_level = false}) - (fn {min_arity, max_arity, sub_level} => - {min_arity = Int.min (n, min_arity), - max_arity = Int.max (n, max_arity), - sub_level = sub_level orelse not top_level}) - end - | _ => the_const_tab +fun count_constants_term top_level t = + let val (head, args) = strip_combterm_comb t in + (case head of + CombConst ((a, _), _, _) => + let + (* Predicate or function version of "equal"? *) + val a = if a = "equal" andalso not top_level then "c_fequal" else a + val n = length args + in + Symtab.map_default + (a, {min_arity = n, max_arity = 0, sub_level = false}) + (fn {min_arity, max_arity, sub_level} => + {min_arity = Int.min (n, min_arity), + max_arity = Int.max (n, max_arity), + sub_level = sub_level orelse not top_level}) + end + | _ => I) + #> fold (count_constants_term false) args end fun count_constants_literal (Literal (_, t)) = count_constants_term true t fun count_constants_clause (HOLClause {literals, ...}) =