--- a/doc-src/Nitpick/nitpick.tex Mon Aug 09 11:45:30 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex Mon Aug 09 12:42:25 2010 +0200
@@ -719,9 +719,9 @@
& \phantom{fun\,~\textit{HOLogic.mk\_number}~T~(}{-}~\textit{snd}~(\textit{HOLogic.dest\_number~t2\/})) \\[-2pt]
& \phantom{fun}\!{\mid}\,~\textit{my\_int\_postproc}~\_~\_~\_~\_~t = t \\[-2pt]
{*}\}\end{aligned}$ \\[2\smallskipamount]
-$\textbf{setup}~\,\{{*} \\
+$\textbf{declaration}~\,\{{*} \\
\!\begin{aligned}[t]
-& \textit{Nitpick\_Model.register\_term\_postprocessor\_global\/}~\!\begin{aligned}[t]
+& \textit{Nitpick\_Model.register\_term\_postprocessor}~\!\begin{aligned}[t]
& @\{\textrm{typ}~\textit{my\_int}\} \\[-2pt]
& \textit{my\_int\_postproc}\end{aligned} \\[-2pt]
{*}\}\end{aligned}$
@@ -1237,11 +1237,13 @@
where \textit{xs} is of type $'a~\textit{list}$ and \textit{ys} is of type
$'b~\textit{list}$. A priori, Nitpick would need to consider $1\,000$ scopes to
-exhaust the specification \textit{card}~= 1--10. However, our intuition tells us
-that any counterexample found with a small scope would still be a counterexample
-in a larger scope---by simply ignoring the fresh $'a$ and $'b$ values provided
-by the larger scope. Nitpick comes to the same conclusion after a careful
-inspection of the formula and the relevant definitions:
+exhaust the specification \textit{card}~= 1--10 (10 cardinalies for $'a$
+$\times$ 10 cardinalities for $'b$ $\times$ 10 cardinalities for the datatypes).
+However, our intuition tells us that any counterexample found with a small scope
+would still be a counterexample in a larger scope---by simply ignoring the fresh
+$'a$ and $'b$ values provided by the larger scope. Nitpick comes to the same
+conclusion after a careful inspection of the formula and the relevant
+definitions:
\prew
\textbf{nitpick}~[\textit{verbose}] \\[2\smallskipamount]
@@ -1312,10 +1314,11 @@
As insinuated in \S\ref{natural-numbers-and-integers} and
\S\ref{inductive-datatypes}, \textit{nat}, \textit{int}, and inductive datatypes
are normally monotonic and treated as such. The same is true for record types,
-\textit{rat}, \textit{real}, and some \textbf{typedef}'d types. Thus, given the
+\textit{rat}, and \textit{real}. Thus, given the
cardinality specification 1--10, a formula involving \textit{nat}, \textit{int},
\textit{int~list}, \textit{rat}, and \textit{rat~list} will lead Nitpick to
-consider only 10~scopes instead of $10\,000$.
+consider only 10~scopes instead of $10\,000$. On the other hand,
+\textbf{typedef}s and quotient types are generally nonmonotonic.
\subsection{Inductive Properties}
\label{inductive-properties}
@@ -2787,10 +2790,11 @@
\textit{Nitpick\_HOL} structure:
\prew
-$\textbf{val}\,~\textit{register\_codatatype\_global\/} : {}$ \\
-$\hbox{}\quad\textit{typ} \rightarrow \textit{string} \rightarrow \textit{styp~list} \rightarrow \textit{theory} \rightarrow \textit{theory}$ \\
-$\textbf{val}\,~\textit{unregister\_codatatype\_global\/} :\,
-\textit{typ} \rightarrow \textit{theory} \rightarrow \textit{theory}$
+$\textbf{val}\,~\textit{register\_codatatype\/} : {}$ \\
+$\hbox{}\quad\textit{morphism} \rightarrow \textit{typ} \rightarrow \textit{string} \rightarrow (\textit{string} \times \textit{typ})\;\textit{list} \rightarrow \textit{Context.generic} {}$ \\
+$\hbox{}\quad{\rightarrow}\; \textit{Context.generic}$ \\
+$\textbf{val}\,~\textit{unregister\_codatatype\/} : {}$ \\
+$\hbox{}\quad\textit{morphism} \rightarrow \textit{typ} \rightarrow \textit{Context.generic} \rightarrow \textit{Context.generic} {}$
\postw
The type $'a~\textit{llist}$ of lazy lists is already registered; had it
@@ -2798,24 +2802,25 @@
to your theory file:
\prew
-$\textbf{setup}~\,\{{*}$ \\
-$\hbox{}\qquad\textit{Nitpick\_HOL.register\_codatatype\_global\/}~@\{\antiq{typ}~``\kern1pt'a~\textit{llist\/}\textrm{''}\}$ \\
-$\hbox{}\qquad\qquad @\{\antiq{const\_name}~ \textit{llist\_case}\}$ \\
-$\hbox{}\qquad\qquad (\textit{map}~\textit{dest\_Const}~[@\{\antiq{term}~\textit{LNil}\},\, @\{\antiq{term}~\textit{LCons}\}])$ \\
+$\textbf{declaration}~\,\{{*}$ \\
+$\hbox{}\quad\textit{Nitpick\_HOL.register\_codatatype}~@\{\antiq{typ}~``\kern1pt'a~\textit{llist\/}\textrm{''}\}$ \\
+$\hbox{}\qquad\quad @\{\antiq{const\_name}~ \textit{llist\_case}\}$ \\
+$\hbox{}\qquad\quad (\textit{map}~\textit{dest\_Const}~[@\{\antiq{term}~\textit{LNil}\},\, @\{\antiq{term}~\textit{LCons}\}])$ \\
${*}\}$
\postw
-The \textit{register\_codatatype\_global\/} function takes a coinductive type, its
-case function, and the list of its constructors. The case function must take its
-arguments in the order that the constructors are listed. If no case function
-with the correct signature is available, simply pass the empty string.
+The \textit{register\_codatatype} function takes a coinductive datatype, its
+case function, and the list of its constructors (in addition to the current
+morphism and generic proof context). The case function must take its arguments
+in the order that the constructors are listed. If no case function with the
+correct signature is available, simply pass the empty string.
On the other hand, if your goal is to cripple Nitpick, add the following line to
your theory file and try to check a few conjectures about lazy lists:
\prew
-$\textbf{setup}~\,\{{*}$ \\
-$\hbox{}\qquad\textit{Nitpick\_HOL.unregister\_codatatype\_global\/}~@\{\antiq{typ}~``\kern1pt'a~\textit{llist\/}\textrm{''}\}$ \\
+$\textbf{declaration}~\,\{{*}$ \\
+$\hbox{}\quad\textit{Nitpick\_HOL.unregister\_codatatype}~@\{\antiq{typ}~``\kern1pt'a~\textit{llist\/}\textrm{''}\}$ \\
${*}\}$
\postw
@@ -2835,10 +2840,11 @@
\prew
$\textbf{type}\,~\textit{term\_postprocessor}\,~{=} {}$ \\
$\hbox{}\quad\textit{Proof.context} \rightarrow \textit{string} \rightarrow (\textit{typ} \rightarrow \textit{term~list\/}) \rightarrow \textit{typ} \rightarrow \textit{term} \rightarrow \textit{term}$ \\
-$\textbf{val}\,~\textit{register\_term\_postprocessor\_global\/} : {}$ \\
-$\hbox{}\quad\textit{typ} \rightarrow \textit{term\_postprocessor} \rightarrow \textit{theory} \rightarrow \textit{theory}$ \\
-$\textbf{val}\,~\textit{unregister\_term\_postprocessor\_global\/} :\,
-\textit{typ} \rightarrow \textit{theory} \rightarrow \textit{theory}$
+$\textbf{val}\,~\textit{register\_term\_postprocessor} : {}$ \\
+$\hbox{}\quad\textit{typ} \rightarrow \textit{term\_postprocessor} \rightarrow \textit{morphism} \rightarrow \textit{Context.generic}$ \\
+$\hbox{}\quad{\rightarrow}\; \textit{Context.generic}$ \\
+$\textbf{val}\,~\textit{unregister\_term\_postprocessor} : {}$ \\
+$\hbox{}\quad\textit{typ} \rightarrow \textit{morphism} \rightarrow \textit{Context.generic} \rightarrow \textit{Context.generic}$
\postw
\S\ref{typedefs-quotient-types-records-rationals-and-reals} and
--- a/src/HOL/IsaMakefile Mon Aug 09 11:45:30 2010 +0200
+++ b/src/HOL/IsaMakefile Mon Aug 09 12:42:25 2010 +0200
@@ -321,9 +321,10 @@
Tools/Sledgehammer/metis_tactics.ML \
Tools/Sledgehammer/sledgehammer.ML \
Tools/Sledgehammer/sledgehammer_fact_filter.ML \
- Tools/Sledgehammer/sledgehammer_fact_minimizer.ML \
+ Tools/Sledgehammer/sledgehammer_fact_minimize.ML \
Tools/Sledgehammer/sledgehammer_isar.ML \
Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML \
+ Tools/Sledgehammer/sledgehammer_translate.ML \
Tools/Sledgehammer/sledgehammer_util.ML \
Tools/SMT/cvc3_solver.ML \
Tools/SMT/smtlib_interface.ML \
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Aug 09 11:45:30 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Aug 09 12:42:25 2010 +0200
@@ -391,7 +391,7 @@
val params = Sledgehammer_Isar.default_params thy
[("atps", prover_name), ("minimize_timeout", Int.toString timeout ^ " s")]
val minimize =
- Sledgehammer_Fact_Minimizer.minimize_theorems params 1 (subgoal_count st)
+ Sledgehammer_Fact_Minimize.minimize_theorems params 1 (subgoal_count st)
val _ = log separator
in
case minimize st (these (!named_thms)) of
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Aug 09 11:45:30 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Aug 09 12:42:25 2010 +0200
@@ -128,9 +128,8 @@
| my_int_postproc _ _ _ _ t = t
*}
-setup {*
-Nitpick_Model.register_term_postprocessor_global @{typ my_int}
- my_int_postproc
+declare {*
+Nitpick_Model.register_term_postprocessor @{typ my_int} my_int_postproc
*}
lemma "add x y = add x x"
@@ -213,8 +212,8 @@
"iterates f a = LCons a (iterates f (f a))"
sorry
-setup {*
-Nitpick_HOL.register_codatatype_global @{typ "'a llist"} ""
+declare {*
+Nitpick_HOL.register_codatatype @{typ "'a llist"} ""
(map dest_Const [@{term LNil}, @{term LCons}])
*}
--- a/src/HOL/Sledgehammer.thy Mon Aug 09 11:45:30 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Mon Aug 09 12:42:25 2010 +0200
@@ -20,9 +20,10 @@
("Tools/Sledgehammer/metis_tactics.ML")
("Tools/Sledgehammer/sledgehammer_util.ML")
("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
+ ("Tools/Sledgehammer/sledgehammer_translate.ML")
("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
("Tools/Sledgehammer/sledgehammer.ML")
- ("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML")
+ ("Tools/Sledgehammer/sledgehammer_fact_minimize.ML")
("Tools/Sledgehammer/sledgehammer_isar.ML")
begin
@@ -100,10 +101,11 @@
use "Tools/Sledgehammer/sledgehammer_util.ML"
use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
+use "Tools/Sledgehammer/sledgehammer_translate.ML"
use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
use "Tools/Sledgehammer/sledgehammer.ML"
setup Sledgehammer.setup
-use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML"
+use "Tools/Sledgehammer/sledgehammer_fact_minimize.ML"
use "Tools/Sledgehammer/sledgehammer_isar.ML"
setup Metis_Tactics.setup
--- a/src/HOL/Tools/ATP/atp_systems.ML Mon Aug 09 11:45:30 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Mon Aug 09 12:42:25 2010 +0200
@@ -140,7 +140,7 @@
"# Cannot determine problem status within resource limit"),
(OutOfResources, "SZS status: ResourceOut"),
(OutOfResources, "SZS status ResourceOut")],
- max_new_relevant_facts_per_iter = 90 (* FIXME *),
+ max_new_relevant_facts_per_iter = 60 (* FIXME *),
prefers_theory_relevant = false,
explicit_forall = false}
val e = ("e", e_config)
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Aug 09 11:45:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Aug 09 12:42:25 2010 +0200
@@ -144,16 +144,19 @@
val eta_expand : typ list -> term -> int -> term
val distinctness_formula : typ -> term list -> term
val register_frac_type :
- string -> (string * string) list -> Proof.context -> Proof.context
+ string -> (string * string) list -> morphism -> Context.generic
+ -> Context.generic
val register_frac_type_global :
string -> (string * string) list -> theory -> theory
- val unregister_frac_type : string -> Proof.context -> Proof.context
+ val unregister_frac_type :
+ string -> morphism -> Context.generic -> Context.generic
val unregister_frac_type_global : string -> theory -> theory
val register_codatatype :
- typ -> string -> styp list -> Proof.context -> Proof.context
+ typ -> string -> styp list -> morphism -> Context.generic -> Context.generic
val register_codatatype_global :
typ -> string -> styp list -> theory -> theory
- val unregister_codatatype : typ -> Proof.context -> Proof.context
+ val unregister_codatatype :
+ typ -> morphism -> Context.generic -> Context.generic
val unregister_codatatype_global : typ -> theory -> theory
val datatype_constrs : hol_context -> typ -> styp list
val binarized_and_boxed_datatype_constrs :
@@ -631,11 +634,15 @@
val {frac_types, codatatypes} = Data.get generic
val frac_types = AList.update (op =) (frac_s, ersaetze) frac_types
in Data.put {frac_types = frac_types, codatatypes = codatatypes} generic end
-val register_frac_type = Context.proof_map oo register_frac_type_generic
+(* TODO: Consider morphism. *)
+fun register_frac_type frac_s ersaetze (_ : morphism) =
+ register_frac_type_generic frac_s ersaetze
val register_frac_type_global = Context.theory_map oo register_frac_type_generic
fun unregister_frac_type_generic frac_s = register_frac_type_generic frac_s []
-val unregister_frac_type = Context.proof_map o unregister_frac_type_generic
+(* TODO: Consider morphism. *)
+fun unregister_frac_type frac_s (_ : morphism) =
+ unregister_frac_type_generic frac_s
val unregister_frac_type_global =
Context.theory_map o unregister_frac_type_generic
@@ -656,12 +663,16 @@
val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs))
codatatypes
in Data.put {frac_types = frac_types, codatatypes = codatatypes} generic end
-val register_codatatype = Context.proof_map ooo register_codatatype_generic
+(* TODO: Consider morphism. *)
+fun register_codatatype co_T case_name constr_xs (_ : morphism) =
+ register_codatatype_generic co_T case_name constr_xs
val register_codatatype_global =
Context.theory_map ooo register_codatatype_generic
fun unregister_codatatype_generic co_T = register_codatatype_generic co_T "" []
-val unregister_codatatype = Context.proof_map o unregister_codatatype_generic
+(* TODO: Consider morphism. *)
+fun unregister_codatatype co_T (_ : morphism) =
+ unregister_codatatype_generic co_T
val unregister_codatatype_global =
Context.theory_map o unregister_codatatype_generic
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Aug 09 11:45:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Aug 09 12:42:25 2010 +0200
@@ -25,10 +25,11 @@
val unknown : string
val unrep : unit -> string
val register_term_postprocessor :
- typ -> term_postprocessor -> Proof.context -> Proof.context
+ typ -> term_postprocessor -> morphism -> Context.generic -> Context.generic
val register_term_postprocessor_global :
typ -> term_postprocessor -> theory -> theory
- val unregister_term_postprocessor : typ -> Proof.context -> Proof.context
+ val unregister_term_postprocessor :
+ typ -> morphism -> Context.generic -> Context.generic
val unregister_term_postprocessor_global : typ -> theory -> theory
val tuple_list_for_name :
nut NameTable.table -> Kodkod.raw_bound list -> nut -> int list list
@@ -158,15 +159,18 @@
| ord => ord)
| _ => Term_Ord.fast_term_ord tp
-fun register_term_postprocessor_generic T p = Data.map (cons (T, p))
-val register_term_postprocessor =
- Context.proof_map oo register_term_postprocessor_generic
+fun register_term_postprocessor_generic T postproc =
+ Data.map (cons (T, postproc))
+(* TODO: Consider morphism. *)
+fun register_term_postprocessor T postproc (_ : morphism) =
+ register_term_postprocessor_generic T postproc
val register_term_postprocessor_global =
Context.theory_map oo register_term_postprocessor_generic
fun unregister_term_postprocessor_generic T = Data.map (AList.delete (op =) T)
-val unregister_term_postprocessor =
- Context.proof_map o unregister_term_postprocessor_generic
+(* TODO: Consider morphism. *)
+fun unregister_term_postprocessor T (_ : morphism) =
+ unregister_term_postprocessor_generic T
val unregister_term_postprocessor_global =
Context.theory_map o unregister_term_postprocessor_generic
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Aug 09 11:45:30 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Aug 09 12:42:25 2010 +0200
@@ -55,7 +55,7 @@
let
val args = OldTerm.term_frees body
val Ts = map type_of args
- val cT = Ts ---> T (* FIXME: use "skolem_type_and_args" *)
+ val cT = Ts ---> T
(* Forms a lambda-abstraction over the formal parameters *)
val rhs =
list_abs_free (map dest_Free args,
@@ -78,11 +78,10 @@
(*Returns the vars of a theorem*)
fun vars_of_thm th =
- map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []);
+ map (cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []);
val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
-(* ### FIXME: removes only one lambda? *)
(* Removes the lambdas from an equation of the form "t = (%x. u)".
(Cf. "extensionalize_term" in "ATP_Systems".) *)
fun extensionalize_theorem th =
@@ -101,7 +100,7 @@
val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C}));
val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S}));
-(*FIXME: requires more use of cterm constructors*)
+(* FIXME: Requires more use of cterm constructors. *)
fun abstract ct =
let
val thy = theory_of_cterm ct
@@ -182,7 +181,7 @@
TrueI)
(*cterms are used throughout for efficiency*)
-val cTrueprop = Thm.cterm_of @{theory HOL} HOLogic.Trueprop;
+val cTrueprop = cterm_of @{theory HOL} HOLogic.Trueprop;
(*Given an abstraction over n variables, replace the bound variables by free
ones. Return the body, along with the list of free variables.*)
@@ -198,7 +197,7 @@
Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *)
fun skolem_theorem_of_def thy rhs0 =
let
- val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> Thm.cterm_of thy
+ val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> 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
@@ -206,7 +205,7 @@
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 cex = cterm_of thy (HOLogic.exists_const T)
val ex_tm = Thm.capply cTrueprop (Thm.capply cex cabs)
val conc =
Drule.list_comb (rhs, frees)
@@ -231,8 +230,8 @@
|> Meson.make_nnf ctxt
in (th3, ctxt) end;
-(* Skolemize a named theorem, with Skolem functions as additional premises. *)
-fun skolemize_theorem thy th =
+(* Convert a theorem to CNF, with Skolem functions as additional premises. *)
+fun cnf_axiom thy th =
let
val ctxt0 = Variable.global_thm_context th
val (nnfth, ctxt) = to_nnf th ctxt0
@@ -247,8 +246,4 @@
end
handle THM _ => []
-(* Convert Isabelle theorems into axiom clauses. *)
-(* FIXME: is transfer necessary? *)
-fun cnf_axiom thy = skolemize_theorem thy o Thm.transfer thy
-
end;
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Aug 09 11:45:30 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Aug 09 12:42:25 2010 +0200
@@ -574,23 +574,21 @@
fun real_literal (_, (c, _)) = not (String.isPrefix class_prefix c);
-(* FIXME: use "fold" instead *)
-fun translate _ _ _ thpairs [] = thpairs
- | translate ctxt mode skolems thpairs ((fol_th, inf) :: infpairs) =
- let val _ = trace_msg (fn () => "=============================================")
- val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
- val _ = trace_msg (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
- val th = Meson.flexflex_first_order (step ctxt mode skolems
- thpairs (fol_th, inf))
- val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
- val _ = trace_msg (fn () => "=============================================")
- val n_metis_lits =
- length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
- in
- if nprems_of th = n_metis_lits then ()
- else raise METIS ("translate", "Proof reconstruction has gone wrong.");
- translate ctxt mode skolems ((fol_th, th) :: thpairs) infpairs
- end;
+fun translate_one ctxt mode skolems (fol_th, inf) thpairs =
+ let
+ val _ = trace_msg (fn () => "=============================================")
+ val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
+ val _ = trace_msg (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
+ val th = Meson.flexflex_first_order (step ctxt mode skolems
+ thpairs (fol_th, inf))
+ val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
+ val _ = trace_msg (fn () => "=============================================")
+ val n_metis_lits =
+ length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
+ val _ =
+ if nprems_of th = n_metis_lits then ()
+ else raise METIS ("translate", "Proof reconstruction has gone wrong.")
+ in (fol_th, th) :: thpairs end
(*Determining which axiom clauses are actually used*)
fun used_axioms axioms (th, Metis.Proof.Axiom _) = SOME (lookth axioms th)
@@ -744,7 +742,7 @@
val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
(*add constraints arising from converting goal to clause form*)
val proof = Metis.Proof.proof mth
- val result = translate ctxt' mode skolems axioms proof
+ val result = fold (translate_one ctxt' mode skolems) proof axioms
and used = map_filter (used_axioms axioms) proof
val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Aug 09 11:45:30 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Aug 09 12:42:25 2010 +0200
@@ -39,7 +39,7 @@
atp_run_time_in_msecs: int,
output: string,
proof: string,
- internal_thm_names: string Vector.vector,
+ axiom_names: string Vector.vector,
conjecture_shape: int list list}
type prover = params -> minimize_command -> problem -> prover_result
@@ -64,6 +64,7 @@
open Metis_Clauses
open Sledgehammer_Util
open Sledgehammer_Fact_Filter
+open Sledgehammer_Translate
open Sledgehammer_Proof_Reconstruct
@@ -73,9 +74,6 @@
"Async_Manager". *)
val das_Tool = "Sledgehammer"
-(* Freshness almost guaranteed! *)
-val sledgehammer_weak_prefix = "Sledgehammer:"
-
fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs"
fun running_atps () = Async_Manager.running_threads das_Tool "ATPs"
val messages = Async_Manager.thread_messages das_Tool "ATP"
@@ -112,7 +110,7 @@
atp_run_time_in_msecs: int,
output: string,
proof: string,
- internal_thm_names: string Vector.vector,
+ axiom_names: string Vector.vector,
conjecture_shape: int list list}
type prover = params -> minimize_command -> problem -> prover_result
@@ -158,470 +156,6 @@
else
failure))
-
-(* Clause preparation *)
-
-datatype fol_formula =
- FOLFormula of {name: string,
- kind: kind,
- combformula: (name, combterm) formula,
- ctypes_sorts: typ list}
-
-fun mk_anot phi = AConn (ANot, [phi])
-fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
-fun mk_ahorn [] phi = phi
- | mk_ahorn (phi :: phis) psi =
- AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])
-
-(* ### FIXME: reintroduce
-fun make_formula_table xs =
- fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty
-(* Remove existing axioms from the conjecture, as this can
- dramatically boost an ATP's performance (for some reason). *)
-fun subtract_cls axioms =
- filter_out (Termtab.defined (make_formula_table axioms) o prop_of)
-*)
-
-fun combformula_for_prop thy =
- let
- val do_term = combterm_from_term thy
- fun do_quant bs q s T t' =
- do_formula ((s, T) :: bs) t'
- #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
- and do_conn bs c t1 t2 =
- do_formula bs t1 ##>> do_formula bs t2
- #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))
- and do_formula bs t =
- case t of
- @{const Not} $ t1 =>
- do_formula bs t1 #>> (fn phi => AConn (ANot, [phi]))
- | Const (@{const_name All}, _) $ Abs (s, T, t') =>
- do_quant bs AForall s T t'
- | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
- do_quant bs AExists s T t'
- | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2
- | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2
- | @{const "op -->"} $ t1 $ t2 => do_conn bs AImplies t1 t2
- | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
- do_conn bs AIff t1 t2
- | _ => (fn ts => do_term bs (Envir.eta_contract t)
- |>> AAtom ||> union (op =) ts)
- in do_formula [] end
-
-(* Converts an elim-rule into an equivalent theorem that does not have the
- predicate variable. Leaves other theorems unchanged. We simply instantiate
- the conclusion variable to False. (Cf. "transform_elim_term" in
- "ATP_Systems".) *)
-(* FIXME: test! *)
-fun transform_elim_term t =
- case Logic.strip_imp_concl t of
- @{const Trueprop} $ Var (z, @{typ bool}) =>
- subst_Vars [(z, @{const True})] t
- | Var (z, @{typ prop}) => subst_Vars [(z, @{prop True})] t
- | _ => t
-
-fun presimplify_term thy =
- Skip_Proof.make_thm thy
- #> Meson.presimplify
- #> prop_of
-
-fun concealed_bound_name j = sledgehammer_weak_prefix ^ Int.toString j
-fun conceal_bounds Ts t =
- subst_bounds (map (Free o apfst concealed_bound_name)
- (0 upto length Ts - 1 ~~ Ts), t)
-fun reveal_bounds Ts =
- subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
- (0 upto length Ts - 1 ~~ Ts))
-
-fun introduce_combinators_in_term ctxt kind t =
- let
- val thy = ProofContext.theory_of ctxt
- fun aux Ts t =
- case t of
- @{const Not} $ t1 => @{const Not} $ aux Ts t1
- | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
- t0 $ Abs (s, T, aux (T :: Ts) t')
- | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
- t0 $ Abs (s, T, aux (T :: Ts) t')
- | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
- $ t1 $ t2 =>
- t0 $ aux Ts t1 $ aux Ts t2
- | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
- t
- else
- let
- val t = t |> conceal_bounds Ts
- |> Envir.eta_contract
- val ([t], ctxt') = Variable.import_terms true [t] ctxt
- in
- t |> cterm_of thy
- |> Clausifier.introduce_combinators_in_cterm
- |> singleton (Variable.export ctxt' ctxt)
- |> prop_of |> Logic.dest_equals |> snd
- |> reveal_bounds Ts
- end
- in t |> not (Meson.is_fol_term thy t) ? aux [] end
- handle THM _ =>
- (* A type variable of sort "{}" will make abstraction fail. *)
- case kind of
- Axiom => HOLogic.true_const
- | Conjecture => HOLogic.false_const
-
-(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
- same in Sledgehammer to prevent the discovery of unreplable proofs. *)
-fun freeze_term t =
- let
- fun aux (t $ u) = aux t $ aux u
- | aux (Abs (s, T, t)) = Abs (s, T, aux t)
- | aux (Var ((s, i), T)) =
- Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
- | aux t = t
- in t |> exists_subterm is_Var t ? aux end
-
-(* making axiom and conjecture formulas *)
-fun make_formula ctxt presimp (name, kind, t) =
- let
- val thy = ProofContext.theory_of ctxt
- val t = t |> transform_elim_term
- |> Object_Logic.atomize_term thy
- val t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop
- |> extensionalize_term
- |> presimp ? presimplify_term thy
- |> perhaps (try (HOLogic.dest_Trueprop))
- |> introduce_combinators_in_term ctxt kind
- |> kind = Conjecture ? freeze_term
- val (combformula, ctypes_sorts) = combformula_for_prop thy t []
- in
- FOLFormula {name = name, combformula = combformula, kind = kind,
- ctypes_sorts = ctypes_sorts}
- end
-
-fun make_axiom ctxt presimp (name, th) =
- (name, make_formula ctxt presimp (name, Axiom, prop_of th))
-fun make_conjectures ctxt ts =
- map2 (fn j => fn t => make_formula ctxt true (Int.toString j, Conjecture, t))
- (0 upto length ts - 1) ts
-
-(** Helper facts **)
-
-fun count_combterm (CombConst ((s, _), _, _)) =
- Symtab.map_entry s (Integer.add 1)
- | count_combterm (CombVar _) = I
- | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2]
-fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
- | count_combformula (AConn (_, phis)) = fold count_combformula phis
- | count_combformula (AAtom tm) = count_combterm tm
-fun count_fol_formula (FOLFormula {combformula, ...}) =
- count_combformula combformula
-
-val optional_helpers =
- [(["c_COMBI", "c_COMBK"], @{thms COMBI_def COMBK_def}),
- (["c_COMBB", "c_COMBC"], @{thms COMBB_def COMBC_def}),
- (["c_COMBS"], @{thms COMBS_def})]
-val optional_typed_helpers =
- [(["c_True", "c_False"], @{thms True_or_False}),
- (["c_If"], @{thms if_True if_False True_or_False})]
-val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
-
-val init_counters =
- Symtab.make (maps (maps (map (rpair 0) o fst))
- [optional_helpers, optional_typed_helpers])
-
-fun get_helper_facts ctxt is_FO full_types conjectures axioms =
- let
- val ct = fold (fold count_fol_formula) [conjectures, axioms] init_counters
- fun is_needed c = the (Symtab.lookup ct c) > 0
- in
- (optional_helpers
- |> full_types ? append optional_typed_helpers
- |> maps (fn (ss, ths) =>
- if exists is_needed ss then map (`Thm.get_name_hint) ths
- else [])) @
- (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers)
- |> map (snd o make_axiom ctxt false)
- end
-
-fun meta_not t = @{const "==>"} $ t $ @{prop False}
-
-fun prepare_formulas ctxt full_types hyp_ts concl_t axcls =
- let
- val thy = ProofContext.theory_of ctxt
- val goal_t = Logic.list_implies (hyp_ts, concl_t)
- val is_FO = Meson.is_fol_term thy goal_t
- val axtms = map (prop_of o snd) axcls
- val subs = tfree_classes_of_terms [goal_t]
- val supers = tvar_classes_of_terms axtms
- val tycons = type_consts_of_terms thy (goal_t :: axtms)
- (* TFrees in the conjecture; TVars in the axioms *)
- val conjectures = map meta_not hyp_ts @ [concl_t] |> make_conjectures ctxt
- val (clnames, axioms) = ListPair.unzip (map (make_axiom ctxt true) axcls)
- val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms
- val (supers', arity_clauses) = make_arity_clauses thy tycons supers
- val class_rel_clauses = make_class_rel_clauses thy subs supers'
- in
- (Vector.fromList clnames,
- (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses))
- end
-
-fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
-
-fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])
- | fo_term_for_combtyp (CombTFree name) = ATerm (name, [])
- | fo_term_for_combtyp (CombType (name, tys)) =
- ATerm (name, map fo_term_for_combtyp tys)
-
-fun fo_literal_for_type_literal (TyLitVar (class, name)) =
- (true, ATerm (class, [ATerm (name, [])]))
- | fo_literal_for_type_literal (TyLitFree (class, name)) =
- (true, ATerm (class, [ATerm (name, [])]))
-
-fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
-
-fun fo_term_for_combterm full_types =
- let
- fun aux top_level u =
- let
- val (head, args) = strip_combterm_comb u
- val (x, ty_args) =
- case head of
- CombConst (name as (s, s'), _, ty_args) =>
- if s = "equal" then
- (if top_level andalso length args = 2 then name
- else ("c_fequal", @{const_name fequal}), [])
- else if top_level then
- case s of
- "c_False" => (("$false", s'), [])
- | "c_True" => (("$true", s'), [])
- | _ => (name, if full_types then [] else ty_args)
- else
- (name, if full_types then [] else ty_args)
- | CombVar (name, _) => (name, [])
- | CombApp _ => raise Fail "impossible \"CombApp\""
- val t = ATerm (x, map fo_term_for_combtyp ty_args @
- map (aux false) args)
- in
- if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t
- end
- in aux true end
-
-fun formula_for_combformula full_types =
- let
- fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
- | aux (AConn (c, phis)) = AConn (c, map aux phis)
- | aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm)
- in aux end
-
-fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) =
- mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
- (type_literals_for_types ctypes_sorts))
- (formula_for_combformula full_types combformula)
-
-fun problem_line_for_fact prefix full_types
- (formula as FOLFormula {name, kind, ...}) =
- Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula)
-
-fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
- superclass, ...}) =
- let val ty_arg = ATerm (("T", "T"), []) in
- Fof (class_rel_clause_prefix ^ ascii_of name, Axiom,
- AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
- AAtom (ATerm (superclass, [ty_arg]))]))
- end
-
-fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
- (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
- | fo_literal_for_arity_literal (TVarLit (c, sort)) =
- (false, ATerm (c, [ATerm (sort, [])]))
-
-fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits,
- ...}) =
- Fof (arity_clause_prefix ^ ascii_of name, Axiom,
- mk_ahorn (map (formula_for_fo_literal o apfst not
- o fo_literal_for_arity_literal) premLits)
- (formula_for_fo_literal
- (fo_literal_for_arity_literal conclLit)))
-
-fun problem_line_for_conjecture full_types
- (FOLFormula {name, kind, combformula, ...}) =
- Fof (conjecture_prefix ^ name, kind,
- formula_for_combformula full_types combformula)
-
-fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) =
- map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
-
-fun problem_line_for_free_type lit =
- Fof (tfrees_name, Conjecture, mk_anot (formula_for_fo_literal lit))
-fun problem_lines_for_free_types conjectures =
- let
- val litss = map free_type_literals_for_conjecture conjectures
- val lits = fold (union (op =)) litss []
- in map problem_line_for_free_type lits end
-
-(** "hBOOL" and "hAPP" **)
-
-type const_info = {min_arity: int, max_arity: int, sub_level: bool}
-
-fun consider_term top_level (ATerm ((s, _), ts)) =
- (if is_tptp_variable s then
- I
- else
- let val n = length ts in
- Symtab.map_default
- (s, {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)
- #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts
-fun consider_formula (AQuant (_, _, phi)) = consider_formula phi
- | consider_formula (AConn (_, phis)) = fold consider_formula phis
- | consider_formula (AAtom tm) = consider_term true tm
-
-fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi
-fun consider_problem problem = fold (fold consider_problem_line o snd) problem
-
-fun const_table_for_problem explicit_apply problem =
- if explicit_apply then NONE
- else SOME (Symtab.empty |> consider_problem problem)
-
-val tc_fun = make_fixed_type_const @{type_name fun}
-
-fun min_arity_of thy full_types NONE s =
- (if s = "equal" orelse s = type_wrapper_name orelse
- String.isPrefix type_const_prefix s orelse
- String.isPrefix class_prefix s then
- 16383 (* large number *)
- else if full_types then
- 0
- else case strip_prefix_and_undo_ascii const_prefix s of
- SOME s' => num_type_args thy (invert_const s')
- | NONE => 0)
- | min_arity_of _ _ (SOME the_const_tab) s =
- case Symtab.lookup the_const_tab s of
- SOME ({min_arity, ...} : const_info) => min_arity
- | NONE => 0
-
-fun full_type_of (ATerm ((s, _), [ty, _])) =
- if s = type_wrapper_name then ty else raise Fail "expected type wrapper"
- | full_type_of _ = raise Fail "expected type wrapper"
-
-fun list_hAPP_rev _ t1 [] = t1
- | list_hAPP_rev NONE t1 (t2 :: ts2) =
- ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2])
- | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) =
- let val ty' = ATerm (`make_fixed_type_const @{type_name fun},
- [full_type_of t2, ty]) in
- ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])
- end
-
-fun repair_applications_in_term thy full_types const_tab =
- let
- fun aux opt_ty (ATerm (name as (s, _), ts)) =
- if s = type_wrapper_name then
- case ts of
- [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2])
- | _ => raise Fail "malformed type wrapper"
- else
- let
- val ts = map (aux NONE) ts
- val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts
- in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
- in aux NONE end
-
-fun boolify t = ATerm (`I "hBOOL", [t])
-
-(* True if the constant ever appears outside of the top-level position in
- literals, or if it appears with different arities (e.g., because of different
- type instantiations). If false, the constant always receives all of its
- arguments and is used as a predicate. *)
-fun is_predicate NONE s =
- s = "equal" orelse String.isPrefix type_const_prefix s orelse
- String.isPrefix class_prefix s
- | is_predicate (SOME the_const_tab) s =
- case Symtab.lookup the_const_tab s of
- SOME {min_arity, max_arity, sub_level} =>
- not sub_level andalso min_arity = max_arity
- | NONE => false
-
-fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) =
- if s = type_wrapper_name then
- case ts of
- [_, t' as ATerm ((s', _), _)] =>
- if is_predicate const_tab s' then t' else boolify t
- | _ => raise Fail "malformed type wrapper"
- else
- t |> not (is_predicate const_tab s) ? boolify
-
-fun close_universally phi =
- let
- fun term_vars bounds (ATerm (name as (s, _), tms)) =
- (is_tptp_variable s andalso not (member (op =) bounds name))
- ? insert (op =) name
- #> fold (term_vars bounds) tms
- fun formula_vars bounds (AQuant (q, xs, phi)) =
- formula_vars (xs @ bounds) phi
- | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
- | formula_vars bounds (AAtom tm) = term_vars bounds tm
- in
- case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi)
- end
-
-fun repair_formula thy explicit_forall full_types const_tab =
- let
- fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
- | aux (AConn (c, phis)) = AConn (c, map aux phis)
- | aux (AAtom tm) =
- AAtom (tm |> repair_applications_in_term thy full_types const_tab
- |> repair_predicates_in_term const_tab)
- in aux #> explicit_forall ? close_universally end
-
-fun repair_problem_line thy explicit_forall full_types const_tab
- (Fof (ident, kind, phi)) =
- Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi)
-fun repair_problem_with_const_table thy =
- map o apsnd o map ooo repair_problem_line thy
-
-fun repair_problem thy explicit_forall full_types explicit_apply problem =
- repair_problem_with_const_table thy explicit_forall full_types
- (const_table_for_problem explicit_apply problem) problem
-
-fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply
- file (conjectures, axioms, helper_facts, class_rel_clauses,
- arity_clauses) =
- let
- val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms
- val helper_lines =
- map (problem_line_for_fact helper_prefix full_types) helper_facts
- val conjecture_lines =
- map (problem_line_for_conjecture full_types) conjectures
- val tfree_lines = problem_lines_for_free_types conjectures
- val class_rel_lines =
- map problem_line_for_class_rel_clause class_rel_clauses
- val arity_lines = map problem_line_for_arity_clause arity_clauses
- (* Reordering these might or might not confuse the proof reconstruction
- code or the SPASS Flotter hack. *)
- val problem =
- [("Relevant facts", axiom_lines),
- ("Class relationships", class_rel_lines),
- ("Arity declarations", arity_lines),
- ("Helper facts", helper_lines),
- ("Conjectures", conjecture_lines),
- ("Type variables", tfree_lines)]
- |> repair_problem thy explicit_forall full_types explicit_apply
- val (problem, pool) = nice_tptp_problem readable_names problem
- val conjecture_offset =
- length axiom_lines + length class_rel_lines + length arity_lines
- + length helper_lines
- val _ = File.write_list file (strings_for_tptp_problem problem)
- in
- (case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
- conjecture_offset)
- end
-
fun extract_clause_sequence output =
let
val tokens_of = String.tokens (not o Char.isAlphaNum)
@@ -684,7 +218,6 @@
let
val (ctxt, (_, th)) = goal;
val thy = ProofContext.theory_of ctxt
- (* ### FIXME: (1) preprocessing for "if" etc. *)
val (params, hyp_ts, concl_t) = strip_subgoal th subgoal
val the_axioms =
case axioms of
@@ -694,8 +227,6 @@
max_new_relevant_facts_per_iter
(the_default prefers_theory_relevant theory_relevant)
relevance_override goal hyp_ts concl_t
- val (internal_thm_names, formulas) =
- prepare_formulas ctxt full_types hyp_ts concl_t the_axioms
(* path to unique problem file *)
val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
@@ -760,9 +291,10 @@
known_failures output
in (output, msecs, proof, outcome) end
val readable_names = debug andalso overlord
- val (pool, conjecture_offset) =
- write_tptp_file thy readable_names explicit_forall full_types
- explicit_apply probfile formulas
+ val (problem, pool, conjecture_offset, axiom_names) =
+ prepare_problem ctxt readable_names explicit_forall full_types
+ explicit_apply hyp_ts concl_t the_axioms
+ val _ = File.write_list probfile (strings_for_tptp_problem problem)
val conjecture_shape =
conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
|> map single
@@ -773,7 +305,7 @@
|> (fn (output, msecs, proof, outcome) =>
(output, msecs0 + msecs, proof, outcome))
| result => result)
- in ((pool, conjecture_shape), result) end
+ in ((pool, conjecture_shape, axiom_names), result) end
else
error ("Bad executable: " ^ Path.implode command ^ ".")
@@ -787,24 +319,24 @@
else
File.write (Path.explode (Path.implode probfile ^ "_proof")) output
- val ((pool, conjecture_shape), (output, msecs, proof, outcome)) =
+ val ((pool, conjecture_shape, axiom_names),
+ (output, msecs, proof, outcome)) =
with_path cleanup export run_on (prob_pathname subgoal)
- val (conjecture_shape, internal_thm_names) =
+ val (conjecture_shape, axiom_names) =
repair_conjecture_shape_and_theorem_names output conjecture_shape
- internal_thm_names
+ axiom_names
val (message, used_thm_names) =
case outcome of
NONE =>
proof_text isar_proof
(pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
- (full_types, minimize_command, proof, internal_thm_names, th,
- subgoal)
+ (full_types, minimize_command, proof, axiom_names, th, subgoal)
| SOME failure => (string_for_failure failure ^ "\n", [])
in
{outcome = outcome, message = message, pool = pool,
used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs,
- output = output, proof = proof, internal_thm_names = internal_thm_names,
+ output = output, proof = proof, axiom_names = axiom_names,
conjecture_shape = conjecture_shape}
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Aug 09 11:45:30 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Aug 09 12:42:25 2010 +0200
@@ -312,7 +312,6 @@
if member Thm.eq_thm add_thms th then 1.0
else if member Thm.eq_thm del_thms th then 0.0
else formula_weight const_tab rel_const_tab consts_typs
-val _ = (if Real.isFinite weight then () else error ("*** " ^ Real.toString weight)) (*###*)
in
if weight >= threshold orelse
(defs_relevant andalso defines thy th rel_const_tab) then
@@ -557,7 +556,7 @@
val thy = ProofContext.theory_of ctxt
val add_thms = maps (ProofContext.get_fact ctxt) add
val has_override = not (null add) orelse not (null del)
-(*###
+(* FIXME:
val is_FO = forall Meson.is_fol_term thy (concl_t :: hyp_ts)
*)
val axioms =
@@ -567,7 +566,7 @@
|> not has_override ? make_unique
|> filter (fn (_, th) =>
member Thm.eq_thm add_thms th orelse
- ((* ### FIXME: keep? (not is_FO orelse is_quasi_fol_theorem thy th) andalso*)
+ ((* FIXME: keep? (not is_FO orelse is_quasi_fol_theorem thy th) andalso*)
not (is_dangerous_term full_types (prop_of th))))
in
relevance_filter ctxt relevance_threshold relevance_convergence
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Mon Aug 09 12:42:25 2010 +0200
@@ -0,0 +1,173 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML
+ Author: Philipp Meyer, TU Muenchen
+ Author: Jasmin Blanchette, TU Muenchen
+
+Minimization of theorem list for Metis using automatic theorem provers.
+*)
+
+signature SLEDGEHAMMER_FACT_MINIMIZE =
+sig
+ type params = Sledgehammer.params
+
+ val minimize_theorems :
+ params -> int -> int -> Proof.state -> (string * thm list) list
+ -> (string * thm list) list option * string
+ val run_minimize : params -> int -> Facts.ref list -> Proof.state -> unit
+end;
+
+structure Sledgehammer_Fact_Minimize : SLEDGEHAMMER_FACT_MINIMIZE =
+struct
+
+open Sledgehammer_Util
+open Sledgehammer_Fact_Filter
+open Sledgehammer_Proof_Reconstruct
+open Sledgehammer
+
+(* wrapper for calling external prover *)
+
+fun string_for_failure Unprovable = "Unprovable."
+ | string_for_failure TimedOut = "Timed out."
+ | string_for_failure _ = "Unknown error."
+
+fun n_theorems name_thms_pairs =
+ let val n = length name_thms_pairs in
+ string_of_int n ^ " theorem" ^ plural_s n ^
+ (if n > 0 then
+ ": " ^ space_implode " "
+ (name_thms_pairs
+ |> map (perhaps (try (unprefix chained_prefix)))
+ |> sort_distinct string_ord)
+ else
+ "")
+ end
+
+fun test_theorems ({debug, verbose, overlord, atps, full_types,
+ relevance_threshold, relevance_convergence, theory_relevant,
+ defs_relevant, isar_proof, isar_shrink_factor,
+ ...} : params)
+ (prover : prover) explicit_apply timeout subgoal state
+ name_thms_pairs =
+ let
+ val _ =
+ priority ("Testing " ^ n_theorems (map fst name_thms_pairs) ^ "...")
+ val params =
+ {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
+ full_types = full_types, explicit_apply = explicit_apply,
+ relevance_threshold = relevance_threshold,
+ relevance_convergence = relevance_convergence,
+ theory_relevant = theory_relevant, defs_relevant = defs_relevant,
+ isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
+ timeout = timeout, minimize_timeout = timeout}
+ val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
+ val {context = ctxt, facts, goal} = Proof.goal state
+ val problem =
+ {subgoal = subgoal, goal = (ctxt, (facts, goal)),
+ relevance_override = {add = [], del = [], only = false},
+ axioms = SOME axioms}
+ val result as {outcome, used_thm_names, ...} =
+ prover params (K "") problem
+ in
+ priority (case outcome of
+ NONE =>
+ if length used_thm_names = length name_thms_pairs then
+ "Found proof."
+ else
+ "Found proof with " ^ n_theorems used_thm_names ^ "."
+ | SOME failure => string_for_failure failure);
+ result
+ end
+
+(* minimalization of thms *)
+
+fun filter_used_facts used =
+ filter (member (op =) used o perhaps (try (unprefix chained_prefix)) o fst)
+
+fun sublinear_minimize _ [] p = p
+ | sublinear_minimize test (x :: xs) (seen, result) =
+ case test (xs @ seen) of
+ result as {outcome = NONE, proof, used_thm_names, ...}
+ : prover_result =>
+ sublinear_minimize test (filter_used_facts used_thm_names xs)
+ (filter_used_facts used_thm_names seen, result)
+ | _ => sublinear_minimize test xs (x :: seen, result)
+
+(* Give the ATP some slack. The ATP gets further slack because the Sledgehammer
+ preprocessing time is included in the estimate below but isn't part of the
+ timeout. *)
+val fudge_msecs = 250
+
+fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set."
+ | minimize_theorems
+ (params as {debug, verbose, overlord, atps as atp :: _, full_types,
+ relevance_threshold, relevance_convergence, theory_relevant,
+ defs_relevant, isar_proof, isar_shrink_factor,
+ minimize_timeout, ...})
+ i n state name_thms_pairs =
+ let
+ val thy = Proof.theory_of state
+ val prover = get_prover_fun thy atp
+ val msecs = Time.toMilliseconds minimize_timeout
+ val _ =
+ priority ("Sledgehammer minimize: ATP " ^ quote atp ^
+ " with a time limit of " ^ string_of_int msecs ^ " ms.")
+ val {context = ctxt, goal, ...} = Proof.goal state
+ val (_, hyp_ts, concl_t) = strip_subgoal goal i
+ val explicit_apply =
+ not (forall (Meson.is_fol_term thy)
+ (concl_t :: hyp_ts @ maps (map prop_of o snd) name_thms_pairs))
+ fun do_test timeout =
+ test_theorems params prover explicit_apply timeout i state
+ val timer = Timer.startRealTimer ()
+ in
+ (case do_test minimize_timeout name_thms_pairs of
+ result as {outcome = NONE, pool, used_thm_names,
+ conjecture_shape, ...} =>
+ let
+ val time = Timer.checkRealTimer timer
+ val new_timeout =
+ Int.min (msecs, Time.toMilliseconds time + fudge_msecs)
+ |> Time.fromMilliseconds
+ val (min_thms, {proof, axiom_names, ...}) =
+ sublinear_minimize (do_test new_timeout)
+ (filter_used_facts used_thm_names name_thms_pairs) ([], result)
+ val n = length min_thms
+ val _ = priority (cat_lines
+ ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^
+ (case filter (String.isPrefix chained_prefix o fst) min_thms of
+ [] => ""
+ | chained => " (including " ^ Int.toString (length chained) ^
+ " chained)") ^ ".")
+ in
+ (SOME min_thms,
+ proof_text isar_proof
+ (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
+ (full_types, K "", proof, axiom_names, goal, i) |> fst)
+ end
+ | {outcome = SOME TimedOut, ...} =>
+ (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
+ \option (e.g., \"timeout = " ^
+ string_of_int (10 + msecs div 1000) ^ " s\").")
+ | {outcome = SOME UnknownError, ...} =>
+ (* Failure sometimes mean timeout, unfortunately. *)
+ (NONE, "Failure: No proof was found with the current time limit. You \
+ \can increase the time limit using the \"timeout\" \
+ \option (e.g., \"timeout = " ^
+ string_of_int (10 + msecs div 1000) ^ " s\").")
+ | {message, ...} => (NONE, "ATP error: " ^ message))
+ handle ERROR msg => (NONE, "Error: " ^ msg)
+ end
+
+fun run_minimize params i refs state =
+ let
+ val ctxt = Proof.context_of state
+ val chained_ths = #facts (Proof.goal state)
+ val name_thms_pairs = map (name_thms_pair_from_ref ctxt chained_ths) refs
+ in
+ case subgoal_count state of
+ 0 => priority "No subgoal!"
+ | n =>
+ (kill_atps ();
+ priority (#2 (minimize_theorems params i n state name_thms_pairs)))
+ end
+
+end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Mon Aug 09 11:45:30 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,174 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
- Author: Philipp Meyer, TU Muenchen
- Author: Jasmin Blanchette, TU Muenchen
-
-Minimization of theorem list for Metis using automatic theorem provers.
-*)
-
-signature SLEDGEHAMMER_FACT_MINIMIZER =
-sig
- type params = Sledgehammer.params
-
- val minimize_theorems :
- params -> int -> int -> Proof.state -> (string * thm list) list
- -> (string * thm list) list option * string
- val run_minimizer : params -> int -> Facts.ref list -> Proof.state -> unit
-end;
-
-structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER =
-struct
-
-open ATP_Systems
-open Sledgehammer_Util
-open Sledgehammer_Fact_Filter
-open Sledgehammer_Proof_Reconstruct
-open Sledgehammer
-
-(* wrapper for calling external prover *)
-
-fun string_for_failure Unprovable = "Unprovable."
- | string_for_failure TimedOut = "Timed out."
- | string_for_failure _ = "Unknown error."
-
-fun n_theorems name_thms_pairs =
- let val n = length name_thms_pairs in
- string_of_int n ^ " theorem" ^ plural_s n ^
- (if n > 0 then
- ": " ^ space_implode " "
- (name_thms_pairs
- |> map (perhaps (try (unprefix chained_prefix)))
- |> sort_distinct string_ord)
- else
- "")
- end
-
-fun test_theorems ({debug, verbose, overlord, atps, full_types,
- relevance_threshold, relevance_convergence, theory_relevant,
- defs_relevant, isar_proof, isar_shrink_factor,
- ...} : params)
- (prover : prover) explicit_apply timeout subgoal state
- name_thms_pairs =
- let
- val _ =
- priority ("Testing " ^ n_theorems (map fst name_thms_pairs) ^ "...")
- val params =
- {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
- full_types = full_types, explicit_apply = explicit_apply,
- relevance_threshold = relevance_threshold,
- relevance_convergence = relevance_convergence,
- theory_relevant = theory_relevant, defs_relevant = defs_relevant,
- isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
- timeout = timeout, minimize_timeout = timeout}
- val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
- val {context = ctxt, facts, goal} = Proof.goal state
- val problem =
- {subgoal = subgoal, goal = (ctxt, (facts, goal)),
- relevance_override = {add = [], del = [], only = false},
- axioms = SOME axioms}
- val result as {outcome, used_thm_names, ...} =
- prover params (K "") problem
- in
- priority (case outcome of
- NONE =>
- if length used_thm_names = length name_thms_pairs then
- "Found proof."
- else
- "Found proof with " ^ n_theorems used_thm_names ^ "."
- | SOME failure => string_for_failure failure);
- result
- end
-
-(* minimalization of thms *)
-
-fun filter_used_facts used =
- filter (member (op =) used o perhaps (try (unprefix chained_prefix)) o fst)
-
-fun sublinear_minimize _ [] p = p
- | sublinear_minimize test (x :: xs) (seen, result) =
- case test (xs @ seen) of
- result as {outcome = NONE, proof, used_thm_names, ...}
- : prover_result =>
- sublinear_minimize test (filter_used_facts used_thm_names xs)
- (filter_used_facts used_thm_names seen, result)
- | _ => sublinear_minimize test xs (x :: seen, result)
-
-(* Give the ATP some slack. The ATP gets further slack because the Sledgehammer
- preprocessing time is included in the estimate below but isn't part of the
- timeout. *)
-val fudge_msecs = 250
-
-fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set."
- | minimize_theorems
- (params as {debug, verbose, overlord, atps as atp :: _, full_types,
- relevance_threshold, relevance_convergence, theory_relevant,
- defs_relevant, isar_proof, isar_shrink_factor,
- minimize_timeout, ...})
- i n state name_thms_pairs =
- let
- val thy = Proof.theory_of state
- val prover = get_prover_fun thy atp
- val msecs = Time.toMilliseconds minimize_timeout
- val _ =
- priority ("Sledgehammer minimizer: ATP " ^ quote atp ^
- " with a time limit of " ^ string_of_int msecs ^ " ms.")
- val {context = ctxt, goal, ...} = Proof.goal state
- val (_, hyp_ts, concl_t) = strip_subgoal goal i
- val explicit_apply =
- not (forall (Meson.is_fol_term thy)
- (concl_t :: hyp_ts @ maps (map prop_of o snd) name_thms_pairs))
- fun do_test timeout =
- test_theorems params prover explicit_apply timeout i state
- val timer = Timer.startRealTimer ()
- in
- (case do_test minimize_timeout name_thms_pairs of
- result as {outcome = NONE, pool, used_thm_names,
- conjecture_shape, ...} =>
- let
- val time = Timer.checkRealTimer timer
- val new_timeout =
- Int.min (msecs, Time.toMilliseconds time + fudge_msecs)
- |> Time.fromMilliseconds
- val (min_thms, {proof, internal_thm_names, ...}) =
- sublinear_minimize (do_test new_timeout)
- (filter_used_facts used_thm_names name_thms_pairs) ([], result)
- val n = length min_thms
- val _ = priority (cat_lines
- ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^
- (case filter (String.isPrefix chained_prefix o fst) min_thms of
- [] => ""
- | chained => " (including " ^ Int.toString (length chained) ^
- " chained)") ^ ".")
- in
- (SOME min_thms,
- proof_text isar_proof
- (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
- (full_types, K "", proof, internal_thm_names, goal, i) |> fst)
- end
- | {outcome = SOME TimedOut, ...} =>
- (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
- \option (e.g., \"timeout = " ^
- string_of_int (10 + msecs div 1000) ^ " s\").")
- | {outcome = SOME UnknownError, ...} =>
- (* Failure sometimes mean timeout, unfortunately. *)
- (NONE, "Failure: No proof was found with the current time limit. You \
- \can increase the time limit using the \"timeout\" \
- \option (e.g., \"timeout = " ^
- string_of_int (10 + msecs div 1000) ^ " s\").")
- | {message, ...} => (NONE, "ATP error: " ^ message))
- handle ERROR msg => (NONE, "Error: " ^ msg)
- end
-
-fun run_minimizer params i refs state =
- let
- val ctxt = Proof.context_of state
- val chained_ths = #facts (Proof.goal state)
- val name_thms_pairs = map (name_thms_pair_from_ref ctxt chained_ths) refs
- in
- case subgoal_count state of
- 0 => priority "No subgoal!"
- | n =>
- (kill_atps ();
- priority (#2 (minimize_theorems params i n state name_thms_pairs)))
- end
-
-end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Aug 09 11:45:30 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Aug 09 12:42:25 2010 +0200
@@ -20,7 +20,7 @@
open ATP_Systems
open Sledgehammer_Util
open Sledgehammer
-open Sledgehammer_Fact_Minimizer
+open Sledgehammer_Fact_Minimize
(** Sledgehammer commands **)
@@ -226,9 +226,9 @@
(minimize_command override_params i) state
end
else if subcommand = minimizeN then
- run_minimizer (get_params thy (map (apfst minimizize_raw_param_name)
- override_params))
- (the_default 1 opt_i) (#add relevance_override) state
+ run_minimize (get_params thy (map (apfst minimizize_raw_param_name)
+ override_params))
+ (the_default 1 opt_i) (#add relevance_override) state
else if subcommand = messagesN then
messages opt_i
else if subcommand = available_atpsN then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Aug 09 11:45:30 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Aug 09 12:42:25 2010 +0200
@@ -10,12 +10,6 @@
sig
type minimize_command = string list -> string
- val axiom_prefix : string
- val conjecture_prefix : string
- val helper_prefix : string
- val class_rel_clause_prefix : string
- val arity_clause_prefix : string
- val tfrees_name : string
val metis_line: bool -> int -> int -> string list -> string
val metis_proof_text:
bool * minimize_command * string * string vector * thm * int
@@ -37,16 +31,10 @@
open Metis_Clauses
open Sledgehammer_Util
open Sledgehammer_Fact_Filter
+open Sledgehammer_Translate
type minimize_command = string list -> string
-val axiom_prefix = "ax_"
-val conjecture_prefix = "conj_"
-val helper_prefix = "help_"
-val class_rel_clause_prefix = "clrel_";
-val arity_clause_prefix = "arity_"
-val tfrees_name = "tfrees"
-
(* Simple simplifications to ensure that sort annotations don't leave a trail of
spurious "True"s. *)
fun s_not @{const False} = @{const True}
@@ -71,9 +59,9 @@
fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2])
fun index_in_shape x = find_index (exists (curry (op =) x))
-fun is_axiom_number thm_names num =
- num > 0 andalso num <= Vector.length thm_names andalso
- Vector.sub (thm_names, num - 1) <> ""
+fun is_axiom_number axiom_names num =
+ num > 0 andalso num <= Vector.length axiom_names andalso
+ Vector.sub (axiom_names, num - 1) <> ""
fun is_conjecture_number conjecture_shape num =
index_in_shape num conjecture_shape >= 0
@@ -491,10 +479,10 @@
(* Discard axioms; consolidate adjacent lines that prove the same formula, since
they differ only in type information.*)
fun add_line _ _ (line as Definition _) lines = line :: lines
- | add_line conjecture_shape thm_names (Inference (num, t, [])) lines =
+ | add_line conjecture_shape axiom_names (Inference (num, t, [])) lines =
(* No dependencies: axiom, conjecture, or (for Vampire) internal axioms or
definitions. *)
- if is_axiom_number thm_names num then
+ if is_axiom_number axiom_names num then
(* Axioms are not proof lines. *)
if is_only_type_information t then
map (replace_deps_in_line (num, [])) lines
@@ -540,10 +528,10 @@
fun add_desired_line _ _ _ _ (line as Definition (num, _, _)) (j, lines) =
(j, line :: map (replace_deps_in_line (num, [])) lines)
- | add_desired_line isar_shrink_factor conjecture_shape thm_names frees
+ | add_desired_line isar_shrink_factor conjecture_shape axiom_names frees
(Inference (num, t, deps)) (j, lines) =
(j + 1,
- if is_axiom_number thm_names num orelse
+ if is_axiom_number axiom_names num orelse
is_conjecture_number conjecture_shape num orelse
(not (is_only_type_information t) andalso
null (Term.add_tvars t []) andalso
@@ -562,16 +550,18 @@
(108) is extracted. For SPASS, lines have the form "108[0:Inp] ...", where
the first number (108) is extracted. For Vampire, we look for
"108. ... [input]". *)
-fun used_facts_in_atp_proof thm_names atp_proof =
+fun used_facts_in_atp_proof axiom_names atp_proof =
let
fun axiom_name num =
let val j = Int.fromString num |> the_default ~1 in
- if is_axiom_number thm_names j then SOME (Vector.sub (thm_names, j - 1))
- else NONE
+ if is_axiom_number axiom_names j then
+ SOME (Vector.sub (axiom_names, j - 1))
+ else
+ NONE
end
val tokens_of =
String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_")
- val thm_name_list = Vector.foldr (op ::) [] thm_names
+ val thm_name_list = Vector.foldr (op ::) [] axiom_names
fun do_line ("fof" :: num :: "axiom" :: (rest as _ :: _)) =
(case strip_prefix_and_undo_ascii axiom_prefix (List.last rest) of
SOME name =>
@@ -617,16 +607,16 @@
val unprefix_chained = perhaps (try (unprefix chained_prefix))
-fun used_facts thm_names =
- used_facts_in_atp_proof thm_names
+fun used_facts axiom_names =
+ used_facts_in_atp_proof axiom_names
#> List.partition (String.isPrefix chained_prefix)
#>> map (unprefix chained_prefix)
#> pairself (sort_distinct string_ord)
-fun metis_proof_text (full_types, minimize_command, atp_proof, thm_names, goal,
- i) =
+fun metis_proof_text (full_types, minimize_command, atp_proof, axiom_names,
+ goal, i) =
let
- val (chained_lemmas, other_lemmas) = used_facts thm_names atp_proof
+ val (chained_lemmas, other_lemmas) = used_facts axiom_names atp_proof
val lemmas = other_lemmas @ chained_lemmas
val n = Logic.count_prems (prop_of goal)
in
@@ -656,9 +646,9 @@
fun smart_case_split [] facts = ByMetis facts
| smart_case_split proofs facts = CaseSplit (proofs, facts)
-fun add_fact_from_dep thm_names num =
- if is_axiom_number thm_names num then
- apsnd (insert (op =) (Vector.sub (thm_names, num - 1)))
+fun add_fact_from_dep axiom_names num =
+ if is_axiom_number axiom_names num then
+ apsnd (insert (op =) (Vector.sub (axiom_names, num - 1)))
else
apfst (insert (op =) (raw_prefix, num))
@@ -667,27 +657,27 @@
fun step_for_line _ _ (Definition (_, t1, t2)) = Let (t1, t2)
| step_for_line _ _ (Inference (num, t, [])) = Assume ((raw_prefix, num), t)
- | step_for_line thm_names j (Inference (num, t, deps)) =
+ | step_for_line axiom_names j (Inference (num, t, deps)) =
Have (if j = 1 then [Show] else [], (raw_prefix, num),
forall_vars t,
- ByMetis (fold (add_fact_from_dep thm_names) deps ([], [])))
+ ByMetis (fold (add_fact_from_dep axiom_names) deps ([], [])))
fun proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor
- atp_proof conjecture_shape thm_names params frees =
+ atp_proof conjecture_shape axiom_names params frees =
let
val lines =
atp_proof ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
|> parse_proof pool
|> sort (int_ord o pairself raw_step_number)
|> decode_lines ctxt full_types tfrees
- |> rpair [] |-> fold_rev (add_line conjecture_shape thm_names)
+ |> rpair [] |-> fold_rev (add_line conjecture_shape axiom_names)
|> rpair [] |-> fold_rev add_nontrivial_line
|> rpair (0, []) |-> fold_rev (add_desired_line isar_shrink_factor
- conjecture_shape thm_names frees)
+ conjecture_shape axiom_names frees)
|> snd
in
(if null params then [] else [Fix params]) @
- map2 (step_for_line thm_names) (length lines downto 1) lines
+ map2 (step_for_line axiom_names) (length lines downto 1) lines
end
(* When redirecting proofs, we keep information about the labels seen so far in
@@ -995,8 +985,8 @@
in do_proof end
fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
- (other_params as (full_types, _, atp_proof, thm_names, goal,
- i)) =
+ (other_params as (full_types, _, atp_proof, axiom_names,
+ goal, i)) =
let
val (params, hyp_ts, concl_t) = strip_subgoal goal i
val frees = fold Term.add_frees (concl_t :: hyp_ts) []
@@ -1005,7 +995,7 @@
val (one_line_proof, lemma_names) = metis_proof_text other_params
fun isar_proof_for () =
case proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor
- atp_proof conjecture_shape thm_names params
+ atp_proof conjecture_shape axiom_names params
frees
|> redirect_proof conjecture_shape hyp_ts concl_t
|> kill_duplicate_assumptions_in_proof
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Mon Aug 09 12:42:25 2010 +0200
@@ -0,0 +1,505 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_translate.ML
+ Author: Fabian Immler, TU Muenchen
+ Author: Makarius
+ Author: Jasmin Blanchette, TU Muenchen
+
+Translation of HOL to FOL.
+*)
+
+signature SLEDGEHAMMER_TRANSLATE =
+sig
+ type 'a problem = 'a ATP_Problem.problem
+
+ val axiom_prefix : string
+ val conjecture_prefix : string
+ val helper_prefix : string
+ val class_rel_clause_prefix : string
+ val arity_clause_prefix : string
+ val tfrees_name : string
+ val prepare_problem :
+ Proof.context -> bool -> bool -> bool -> bool -> term list -> term
+ -> (string * thm) list
+ -> string problem * string Symtab.table * int * string Vector.vector
+end;
+
+structure Sledgehammer_Translate : SLEDGEHAMMER_TRANSLATE =
+struct
+
+open ATP_Problem
+open Metis_Clauses
+open Sledgehammer_Util
+
+val axiom_prefix = "ax_"
+val conjecture_prefix = "conj_"
+val helper_prefix = "help_"
+val class_rel_clause_prefix = "clrel_";
+val arity_clause_prefix = "arity_"
+val tfrees_name = "tfrees"
+
+(* Freshness almost guaranteed! *)
+val sledgehammer_weak_prefix = "Sledgehammer:"
+
+datatype fol_formula =
+ FOLFormula of {name: string,
+ kind: kind,
+ combformula: (name, combterm) formula,
+ ctypes_sorts: typ list}
+
+fun mk_anot phi = AConn (ANot, [phi])
+fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
+fun mk_ahorn [] phi = phi
+ | mk_ahorn (phi :: phis) psi =
+ AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])
+
+fun combformula_for_prop thy =
+ let
+ val do_term = combterm_from_term thy
+ fun do_quant bs q s T t' =
+ do_formula ((s, T) :: bs) t'
+ #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
+ and do_conn bs c t1 t2 =
+ do_formula bs t1 ##>> do_formula bs t2
+ #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))
+ and do_formula bs t =
+ case t of
+ @{const Not} $ t1 =>
+ do_formula bs t1 #>> (fn phi => AConn (ANot, [phi]))
+ | Const (@{const_name All}, _) $ Abs (s, T, t') =>
+ do_quant bs AForall s T t'
+ | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
+ do_quant bs AExists s T t'
+ | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2
+ | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2
+ | @{const "op -->"} $ t1 $ t2 => do_conn bs AImplies t1 t2
+ | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
+ do_conn bs AIff t1 t2
+ | _ => (fn ts => do_term bs (Envir.eta_contract t)
+ |>> AAtom ||> union (op =) ts)
+ in do_formula [] end
+
+(* Converts an elim-rule into an equivalent theorem that does not have the
+ predicate variable. Leaves other theorems unchanged. We simply instantiate
+ the conclusion variable to False. (Cf. "transform_elim_term" in
+ "ATP_Systems".) *)
+fun transform_elim_term t =
+ case Logic.strip_imp_concl t of
+ @{const Trueprop} $ Var (z, @{typ bool}) =>
+ subst_Vars [(z, @{const False})] t
+ | Var (z, @{typ prop}) => subst_Vars [(z, @{prop False})] t
+ | _ => t
+
+fun presimplify_term thy =
+ Skip_Proof.make_thm thy
+ #> Meson.presimplify
+ #> prop_of
+
+fun concealed_bound_name j = sledgehammer_weak_prefix ^ Int.toString j
+fun conceal_bounds Ts t =
+ subst_bounds (map (Free o apfst concealed_bound_name)
+ (0 upto length Ts - 1 ~~ Ts), t)
+fun reveal_bounds Ts =
+ subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
+ (0 upto length Ts - 1 ~~ Ts))
+
+fun introduce_combinators_in_term ctxt kind t =
+ let
+ val thy = ProofContext.theory_of ctxt
+ fun aux Ts t =
+ case t of
+ @{const Not} $ t1 => @{const Not} $ aux Ts t1
+ | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
+ t0 $ Abs (s, T, aux (T :: Ts) t')
+ | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
+ t0 $ Abs (s, T, aux (T :: Ts) t')
+ | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
+ $ t1 $ t2 =>
+ t0 $ aux Ts t1 $ aux Ts t2
+ | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
+ t
+ else
+ let
+ val t = t |> conceal_bounds Ts
+ |> Envir.eta_contract
+ val ([t], ctxt') = Variable.import_terms true [t] ctxt
+ in
+ t |> cterm_of thy
+ |> Clausifier.introduce_combinators_in_cterm
+ |> singleton (Variable.export ctxt' ctxt)
+ |> prop_of |> Logic.dest_equals |> snd
+ |> reveal_bounds Ts
+ end
+ in t |> not (Meson.is_fol_term thy t) ? aux [] end
+ handle THM _ =>
+ (* A type variable of sort "{}" will make abstraction fail. *)
+ case kind of
+ Axiom => HOLogic.true_const
+ | Conjecture => HOLogic.false_const
+
+(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
+ same in Sledgehammer to prevent the discovery of unreplable proofs. *)
+fun freeze_term t =
+ let
+ fun aux (t $ u) = aux t $ aux u
+ | aux (Abs (s, T, t)) = Abs (s, T, aux t)
+ | aux (Var ((s, i), T)) =
+ Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
+ | aux t = t
+ in t |> exists_subterm is_Var t ? aux end
+
+(* making axiom and conjecture formulas *)
+fun make_formula ctxt presimp (name, kind, t) =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val t = t |> transform_elim_term
+ |> Object_Logic.atomize_term thy
+ val t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop
+ |> extensionalize_term
+ |> presimp ? presimplify_term thy
+ |> perhaps (try (HOLogic.dest_Trueprop))
+ |> introduce_combinators_in_term ctxt kind
+ |> kind = Conjecture ? freeze_term
+ val (combformula, ctypes_sorts) = combformula_for_prop thy t []
+ in
+ FOLFormula {name = name, combformula = combformula, kind = kind,
+ ctypes_sorts = ctypes_sorts}
+ end
+
+fun make_axiom ctxt presimp (name, th) =
+ (name, make_formula ctxt presimp (name, Axiom, prop_of th))
+fun make_conjectures ctxt ts =
+ map2 (fn j => fn t => make_formula ctxt true (Int.toString j, Conjecture, t))
+ (0 upto length ts - 1) ts
+
+(** Helper facts **)
+
+fun count_combterm (CombConst ((s, _), _, _)) =
+ Symtab.map_entry s (Integer.add 1)
+ | count_combterm (CombVar _) = I
+ | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2]
+fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
+ | count_combformula (AConn (_, phis)) = fold count_combformula phis
+ | count_combformula (AAtom tm) = count_combterm tm
+fun count_fol_formula (FOLFormula {combformula, ...}) =
+ count_combformula combformula
+
+val optional_helpers =
+ [(["c_COMBI", "c_COMBK"], @{thms COMBI_def COMBK_def}),
+ (["c_COMBB", "c_COMBC"], @{thms COMBB_def COMBC_def}),
+ (["c_COMBS"], @{thms COMBS_def})]
+val optional_typed_helpers =
+ [(["c_True", "c_False"], @{thms True_or_False}),
+ (["c_If"], @{thms if_True if_False True_or_False})]
+val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
+
+val init_counters =
+ Symtab.make (maps (maps (map (rpair 0) o fst))
+ [optional_helpers, optional_typed_helpers])
+
+fun get_helper_facts ctxt is_FO full_types conjectures axioms =
+ let
+ val ct = fold (fold count_fol_formula) [conjectures, axioms] init_counters
+ fun is_needed c = the (Symtab.lookup ct c) > 0
+ in
+ (optional_helpers
+ |> full_types ? append optional_typed_helpers
+ |> maps (fn (ss, ths) =>
+ if exists is_needed ss then map (`Thm.get_name_hint) ths
+ else [])) @
+ (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers)
+ |> map (snd o make_axiom ctxt false)
+ end
+
+fun meta_not t = @{const "==>"} $ t $ @{prop False}
+
+fun prepare_formulas ctxt full_types hyp_ts concl_t axioms =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val axiom_ts = map (prop_of o snd) axioms
+ val hyp_ts =
+ if null hyp_ts then
+ []
+ else
+ (* Remove existing axioms from the conjecture, as this can dramatically
+ boost an ATP's performance (for some reason). *)
+ let
+ val axiom_table = fold (Termtab.update o rpair ()) axiom_ts
+ Termtab.empty
+ in hyp_ts |> filter_out (Termtab.defined axiom_table) end
+ val goal_t = Logic.list_implies (hyp_ts, concl_t)
+ val is_FO = Meson.is_fol_term thy goal_t
+ val subs = tfree_classes_of_terms [goal_t]
+ val supers = tvar_classes_of_terms axiom_ts
+ val tycons = type_consts_of_terms thy (goal_t :: axiom_ts)
+ (* TFrees in the conjecture; TVars in the axioms *)
+ val conjectures = map meta_not hyp_ts @ [concl_t] |> make_conjectures ctxt
+ val (axiom_names, axioms) =
+ ListPair.unzip (map (make_axiom ctxt true) axioms)
+ val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms
+ val (supers', arity_clauses) = make_arity_clauses thy tycons supers
+ val class_rel_clauses = make_class_rel_clauses thy subs supers'
+ in
+ (Vector.fromList axiom_names,
+ (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses))
+ end
+
+fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
+
+fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])
+ | fo_term_for_combtyp (CombTFree name) = ATerm (name, [])
+ | fo_term_for_combtyp (CombType (name, tys)) =
+ ATerm (name, map fo_term_for_combtyp tys)
+
+fun fo_literal_for_type_literal (TyLitVar (class, name)) =
+ (true, ATerm (class, [ATerm (name, [])]))
+ | fo_literal_for_type_literal (TyLitFree (class, name)) =
+ (true, ATerm (class, [ATerm (name, [])]))
+
+fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
+
+fun fo_term_for_combterm full_types =
+ let
+ fun aux top_level u =
+ let
+ val (head, args) = strip_combterm_comb u
+ val (x, ty_args) =
+ case head of
+ CombConst (name as (s, s'), _, ty_args) =>
+ if s = "equal" then
+ (if top_level andalso length args = 2 then name
+ else ("c_fequal", @{const_name fequal}), [])
+ else if top_level then
+ case s of
+ "c_False" => (("$false", s'), [])
+ | "c_True" => (("$true", s'), [])
+ | _ => (name, if full_types then [] else ty_args)
+ else
+ (name, if full_types then [] else ty_args)
+ | CombVar (name, _) => (name, [])
+ | CombApp _ => raise Fail "impossible \"CombApp\""
+ val t = ATerm (x, map fo_term_for_combtyp ty_args @
+ map (aux false) args)
+ in
+ if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t
+ end
+ in aux true end
+
+fun formula_for_combformula full_types =
+ let
+ fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
+ | aux (AConn (c, phis)) = AConn (c, map aux phis)
+ | aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm)
+ in aux end
+
+fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) =
+ mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
+ (type_literals_for_types ctypes_sorts))
+ (formula_for_combformula full_types combformula)
+
+fun problem_line_for_fact prefix full_types
+ (formula as FOLFormula {name, kind, ...}) =
+ Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula)
+
+fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
+ superclass, ...}) =
+ let val ty_arg = ATerm (("T", "T"), []) in
+ Fof (class_rel_clause_prefix ^ ascii_of name, Axiom,
+ AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
+ AAtom (ATerm (superclass, [ty_arg]))]))
+ end
+
+fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
+ (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
+ | fo_literal_for_arity_literal (TVarLit (c, sort)) =
+ (false, ATerm (c, [ATerm (sort, [])]))
+
+fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits,
+ ...}) =
+ Fof (arity_clause_prefix ^ ascii_of name, Axiom,
+ mk_ahorn (map (formula_for_fo_literal o apfst not
+ o fo_literal_for_arity_literal) premLits)
+ (formula_for_fo_literal
+ (fo_literal_for_arity_literal conclLit)))
+
+fun problem_line_for_conjecture full_types
+ (FOLFormula {name, kind, combformula, ...}) =
+ Fof (conjecture_prefix ^ name, kind,
+ formula_for_combformula full_types combformula)
+
+fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) =
+ map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
+
+fun problem_line_for_free_type lit =
+ Fof (tfrees_name, Conjecture, mk_anot (formula_for_fo_literal lit))
+fun problem_lines_for_free_types conjectures =
+ let
+ val litss = map free_type_literals_for_conjecture conjectures
+ val lits = fold (union (op =)) litss []
+ in map problem_line_for_free_type lits end
+
+(** "hBOOL" and "hAPP" **)
+
+type const_info = {min_arity: int, max_arity: int, sub_level: bool}
+
+fun consider_term top_level (ATerm ((s, _), ts)) =
+ (if is_tptp_variable s then
+ I
+ else
+ let val n = length ts in
+ Symtab.map_default
+ (s, {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)
+ #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts
+fun consider_formula (AQuant (_, _, phi)) = consider_formula phi
+ | consider_formula (AConn (_, phis)) = fold consider_formula phis
+ | consider_formula (AAtom tm) = consider_term true tm
+
+fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi
+fun consider_problem problem = fold (fold consider_problem_line o snd) problem
+
+fun const_table_for_problem explicit_apply problem =
+ if explicit_apply then NONE
+ else SOME (Symtab.empty |> consider_problem problem)
+
+fun min_arity_of thy full_types NONE s =
+ (if s = "equal" orelse s = type_wrapper_name orelse
+ String.isPrefix type_const_prefix s orelse
+ String.isPrefix class_prefix s then
+ 16383 (* large number *)
+ else if full_types then
+ 0
+ else case strip_prefix_and_undo_ascii const_prefix s of
+ SOME s' => num_type_args thy (invert_const s')
+ | NONE => 0)
+ | min_arity_of _ _ (SOME the_const_tab) s =
+ case Symtab.lookup the_const_tab s of
+ SOME ({min_arity, ...} : const_info) => min_arity
+ | NONE => 0
+
+fun full_type_of (ATerm ((s, _), [ty, _])) =
+ if s = type_wrapper_name then ty else raise Fail "expected type wrapper"
+ | full_type_of _ = raise Fail "expected type wrapper"
+
+fun list_hAPP_rev _ t1 [] = t1
+ | list_hAPP_rev NONE t1 (t2 :: ts2) =
+ ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2])
+ | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) =
+ let val ty' = ATerm (`make_fixed_type_const @{type_name fun},
+ [full_type_of t2, ty]) in
+ ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])
+ end
+
+fun repair_applications_in_term thy full_types const_tab =
+ let
+ fun aux opt_ty (ATerm (name as (s, _), ts)) =
+ if s = type_wrapper_name then
+ case ts of
+ [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2])
+ | _ => raise Fail "malformed type wrapper"
+ else
+ let
+ val ts = map (aux NONE) ts
+ val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts
+ in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
+ in aux NONE end
+
+fun boolify t = ATerm (`I "hBOOL", [t])
+
+(* True if the constant ever appears outside of the top-level position in
+ literals, or if it appears with different arities (e.g., because of different
+ type instantiations). If false, the constant always receives all of its
+ arguments and is used as a predicate. *)
+fun is_predicate NONE s =
+ s = "equal" orelse String.isPrefix type_const_prefix s orelse
+ String.isPrefix class_prefix s
+ | is_predicate (SOME the_const_tab) s =
+ case Symtab.lookup the_const_tab s of
+ SOME {min_arity, max_arity, sub_level} =>
+ not sub_level andalso min_arity = max_arity
+ | NONE => false
+
+fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) =
+ if s = type_wrapper_name then
+ case ts of
+ [_, t' as ATerm ((s', _), _)] =>
+ if is_predicate const_tab s' then t' else boolify t
+ | _ => raise Fail "malformed type wrapper"
+ else
+ t |> not (is_predicate const_tab s) ? boolify
+
+fun close_universally phi =
+ let
+ fun term_vars bounds (ATerm (name as (s, _), tms)) =
+ (is_tptp_variable s andalso not (member (op =) bounds name))
+ ? insert (op =) name
+ #> fold (term_vars bounds) tms
+ fun formula_vars bounds (AQuant (q, xs, phi)) =
+ formula_vars (xs @ bounds) phi
+ | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
+ | formula_vars bounds (AAtom tm) = term_vars bounds tm
+ in
+ case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi)
+ end
+
+fun repair_formula thy explicit_forall full_types const_tab =
+ let
+ fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
+ | aux (AConn (c, phis)) = AConn (c, map aux phis)
+ | aux (AAtom tm) =
+ AAtom (tm |> repair_applications_in_term thy full_types const_tab
+ |> repair_predicates_in_term const_tab)
+ in aux #> explicit_forall ? close_universally end
+
+fun repair_problem_line thy explicit_forall full_types const_tab
+ (Fof (ident, kind, phi)) =
+ Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi)
+fun repair_problem_with_const_table thy =
+ map o apsnd o map ooo repair_problem_line thy
+
+fun repair_problem thy explicit_forall full_types explicit_apply problem =
+ repair_problem_with_const_table thy explicit_forall full_types
+ (const_table_for_problem explicit_apply problem) problem
+
+fun prepare_problem ctxt readable_names explicit_forall full_types
+ explicit_apply hyp_ts concl_t axiom_ts =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val (axiom_names, (conjectures, axioms, helper_facts, class_rel_clauses,
+ arity_clauses)) =
+ prepare_formulas ctxt full_types hyp_ts concl_t axiom_ts
+ val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms
+ val helper_lines =
+ map (problem_line_for_fact helper_prefix full_types) helper_facts
+ val conjecture_lines =
+ map (problem_line_for_conjecture full_types) conjectures
+ val tfree_lines = problem_lines_for_free_types conjectures
+ val class_rel_lines =
+ map problem_line_for_class_rel_clause class_rel_clauses
+ val arity_lines = map problem_line_for_arity_clause arity_clauses
+ (* Reordering these might or might not confuse the proof reconstruction
+ code or the SPASS Flotter hack. *)
+ val problem =
+ [("Relevant facts", axiom_lines),
+ ("Class relationships", class_rel_lines),
+ ("Arity declarations", arity_lines),
+ ("Helper facts", helper_lines),
+ ("Conjectures", conjecture_lines),
+ ("Type variables", tfree_lines)]
+ |> repair_problem thy explicit_forall full_types explicit_apply
+ val (problem, pool) = nice_tptp_problem readable_names problem
+ val conjecture_offset =
+ length axiom_lines + length class_rel_lines + length arity_lines
+ + length helper_lines
+ in
+ (problem,
+ case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
+ conjecture_offset, axiom_names)
+ end
+
+end;