--- 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
--- 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, ...}) =