--- a/doc-src/Sledgehammer/sledgehammer.tex Fri Aug 20 15:29:36 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Fri Aug 20 16:28:53 2010 +0200
@@ -343,6 +343,7 @@
\item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}.
\item[$\bullet$] \qtybf{bool\_or\_smart\/}: \textit{true}, \textit{false}, or \textit{smart}.
\item[$\bullet$] \qtybf{int\/}: An integer.
+\item[$\bullet$] \qtybf{int\_or\_smart\/}: An integer or \textit{smart}.
\item[$\bullet$] \qtybf{time}: An integer followed by $\textit{min}$ (minutes), $s$ (seconds), or \textit{ms}
(milliseconds), or the keyword \textit{none} ($\infty$ years).
\end{enum}
@@ -384,24 +385,31 @@
Vampire, set the environment variable \texttt{VAMPIRE\_HOME} to the directory
that contains the \texttt{vampire} executable.
-\item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E executes
+\item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E runs
on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
\item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of
-Vampire executes on Geoff Sutcliffe's Miami servers. Version 9 is used.
+Vampire runs on Geoff Sutcliffe's Miami servers. Version 9 is used.
+\item[$\bullet$] \textbf{\textit{remote\_sine\_e}:} SInE-E is a metaprover
+developed by Kry\v stof Hoder \cite{sine} based on E. The remote version of
+SInE runs on Geoff Sutcliffe's Miami servers.
+
+\item[$\bullet$] \textbf{\textit{remote\_snark}:} SNARK is a prover
+developed by Stickel et al.\ \cite{snark}. The remote version of
+SNARK runs on Geoff Sutcliffe's Miami servers.
\end{enum}
-By default, Sledgehammer will run E, SPASS, and Vampire in parallel. For E and
-SPASS, it will use any locally installed version if available, falling back
-on the remote versions if necessary. For historical reasons, the default value
-of this option can be overridden using the option ``Sledgehammer: ATPs'' from
-the ``Isabelle'' menu in Proof General.
+By default, Sledgehammer will run E, SPASS, Vampire, and SInE-E in parallel.
+For at most two of E, SPASS, and Vampire, it will use any locally installed
+version if available. For historical reasons, the default value of this option
+can be overridden using the option ``Sledgehammer: ATPs'' from the ``Isabelle''
+menu in Proof General.
It is a good idea to run several ATPs in parallel, although it could slow down
-your machine. Tobias Nipkow observed that running E, SPASS, and Vampire together
-for 5 seconds yields the same success rate as running the most effective of
-these (Vampire) for 120 seconds \cite{boehme-nipkow-2010}.
+your machine. Running E, SPASS, and Vampire together for 5 seconds yields about
+the same success rate as running the most effective of these (Vampire) for 120
+seconds \cite{boehme-nipkow-2010}.
\opnodefault{atp}{string}
Alias for \textit{atps}.
@@ -433,7 +441,12 @@
the ATPs significantly. For historical reasons, the default value of this option
can be overridden using the option ``Sledgehammer: ATPs'' from the ``Isabelle''
menu in Proof General.
+\end{enum}
+\subsection{Relevance Filter}
+\label{relevance-filter}
+
+\begin{enum}
\opdefault{relevance\_threshold}{int}{50}
Specifies the threshold above which facts are considered relevant by the
relevance filter. The option ranges from 0 to 100, where 0 means that all
@@ -444,6 +457,12 @@
filter. This quotient is used by the relevance filter to scale down the
relevance of facts at each iteration of the filter.
+\opdefault{max\_relevant\_per\_iter}{int\_or\_smart}{\textit{smart}}
+Specifies the maximum number of facts that may be added during one iteration of
+the relevance filter. If the option is set to \textit{smart}, it is set to a
+value that was empirically found to be appropriate for the ATP. A typical value
+would be 50.
+
\opsmartx{theory\_relevant}{theory\_irrelevant}
Specifies whether the theory from which a fact comes should be taken into
consideration by the relevance filter. If the option is set to \textit{smart},
@@ -495,10 +514,6 @@
proof. For historical reasons, the default value of this option can be
overridden using the option ``Sledgehammer: Time Limit'' from the ``Isabelle''
menu in Proof General.
-
-\opdefault{minimize\_timeout}{time}{$\mathbf{5}$\,s}
-Specifies the maximum amount of time that the ATPs should spend looking for a
-proof for \textbf{sledgehammer}~\textit{minimize}.
\end{enum}
\let\em=\sl
--- a/doc-src/manual.bib Fri Aug 20 15:29:36 2010 +0200
+++ b/doc-src/manual.bib Fri Aug 20 16:28:53 2010 +0200
@@ -591,6 +591,11 @@
number = 5,
month = May}
+@misc{sine,
+ author = "Kry\v{s}tof Hoder",
+ title = "SInE (Sumo Inference Engine)",
+ note = "\url{http://www.cs.man.ac.uk/~hoderk/sine/}"}
+
@book{Hudak-Haskell,author={Paul Hudak},
title={The Haskell School of Expression},publisher=CUP,year=2000}
@@ -714,6 +719,15 @@
title = {The Objective Caml system -- Documentation and user's manual},
note = {\url{http://caml.inria.fr/pub/docs/manual-ocaml/}}}
+@incollection{lochbihler-2010,
+ title = "Coinduction",
+ author = "Andreas Lochbihler",
+ booktitle = "The Archive of Formal Proofs",
+ editor = "Gerwin Klein and Tobias Nipkow and Lawrence C. Paulson",
+ publisher = "\url{http://afp.sourceforge.net/entries/Coinductive.shtml}",
+ month = "Feb.",
+ year = 2010}
+
@InProceedings{lowe-fdr,
author = {Gavin Lowe},
title = {Breaking and Fixing the {Needham}-{Schroeder} Public-Key
@@ -1335,6 +1349,12 @@
crossref = {tphols96},
pages = {381-397}}
+@inproceedings{snark,
+ author = {M. Stickel and R. Waldinger and M. Lowry and T. Pressburger and I. Underwood},
+ title = {Deductive composition of astronomical software from subroutine libraries},
+ pages = "341--355",
+ crossref = {cade12}}
+
@book{suppes72,
author = {Patrick Suppes},
title = {Axiomatic Set Theory},
@@ -1819,12 +1839,3 @@
key = "Wikipedia",
title = "Wikipedia: {AA} Tree",
note = "\url{http://en.wikipedia.org/wiki/AA_tree}"}
-
-@incollection{lochbihler-2010,
- title = "Coinduction",
- author = "Andreas Lochbihler",
- booktitle = "The Archive of Formal Proofs",
- editor = "Gerwin Klein and Tobias Nipkow and Lawrence C. Paulson",
- publisher = "\url{http://afp.sourceforge.net/entries/Coinductive.shtml}",
- month = "Feb.",
- year = 2010}
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Aug 20 15:29:36 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Aug 20 16:28:53 2010 +0200
@@ -389,7 +389,7 @@
|> Option.map (fst o read_int o explode)
|> the_default 5
val params = Sledgehammer_Isar.default_params thy
- [("atps", prover_name), ("minimize_timeout", Int.toString timeout ^ " s")]
+ [("atps", prover_name), ("timeout", Int.toString timeout ^ " s")]
val minimize =
Sledgehammer_Fact_Minimize.minimize_theorems params 1 (subgoal_count st)
val _ = log separator
--- a/src/HOL/Sledgehammer.thy Fri Aug 20 15:29:36 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Fri Aug 20 16:28:53 2010 +0200
@@ -31,28 +31,31 @@
[no_atp]: "skolem_id = (\<lambda>x. x)"
definition COMBI :: "'a \<Rightarrow> 'a" where
-[no_atp]: "COMBI P \<equiv> P"
+[no_atp]: "COMBI P = P"
definition COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" where
-[no_atp]: "COMBK P Q \<equiv> P"
+[no_atp]: "COMBK P Q = P"
definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where [no_atp]:
-"COMBB P Q R \<equiv> P (Q R)"
+"COMBB P Q R = P (Q R)"
definition COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
-[no_atp]: "COMBC P Q R \<equiv> P R Q"
+[no_atp]: "COMBC P Q R = P R Q"
definition COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where
-[no_atp]: "COMBS P Q R \<equiv> P R (Q R)"
+[no_atp]: "COMBS P Q R = P R (Q R)"
definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
-"fequal X Y \<equiv> (X = Y)"
+"fequal X Y \<longleftrightarrow> (X = Y)"
+
+lemma fequal_imp_equal [no_atp]: "\<not> fequal X Y \<or> X = Y"
+by (simp add: fequal_def)
-lemma fequal_imp_equal [no_atp]: "fequal X Y \<Longrightarrow> X = Y"
- by (simp add: fequal_def)
+lemma equal_imp_fequal [no_atp]: "\<not> X = Y \<or> fequal X Y"
+by (simp add: fequal_def)
-lemma equal_imp_fequal [no_atp]: "X = Y \<Longrightarrow> fequal X Y"
- by (simp add: fequal_def)
+lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y"
+by auto
text{*Theorems for translation to combinators*}
--- a/src/HOL/Tools/ATP/async_manager.ML Fri Aug 20 15:29:36 2010 +0200
+++ b/src/HOL/Tools/ATP/async_manager.ML Fri Aug 20 16:28:53 2010 +0200
@@ -72,8 +72,8 @@
val message' =
desc ^ "\n" ^ message ^
(if verbose then
- "Total time: " ^ Int.toString (Time.toMilliseconds
- (Time.- (now, birth_time))) ^ " ms.\n"
+ "\nTotal time: " ^ Int.toString (Time.toMilliseconds
+ (Time.- (now, birth_time))) ^ " ms."
else
"")
val messages' = (tool, message') :: messages;
--- a/src/HOL/Tools/ATP/atp_problem.ML Fri Aug 20 15:29:36 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Fri Aug 20 16:28:53 2010 +0200
@@ -15,7 +15,7 @@
AConn of connective * ('a, 'b) formula list |
AAtom of 'b
- datatype kind = Axiom | Conjecture
+ datatype kind = Axiom | Hypothesis | Conjecture
datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
type 'a problem = (string * 'a problem_line list) list
@@ -42,7 +42,7 @@
AConn of connective * ('a, 'b) formula list |
AAtom of 'b
-datatype kind = Axiom | Conjecture
+datatype kind = Axiom | Hypothesis | Conjecture
datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
type 'a problem = (string * 'a problem_line list) list
@@ -76,8 +76,11 @@
fun string_for_problem_line (Fof (ident, kind, phi)) =
"fof(" ^ ident ^ ", " ^
- (case kind of Axiom => "axiom" | Conjecture => "conjecture") ^ ",\n" ^
- " (" ^ string_for_formula phi ^ ")).\n"
+ (case kind of
+ Axiom => "axiom"
+ | Hypothesis => "hypothesis"
+ | Conjecture => "conjecture") ^
+ ",\n (" ^ string_for_formula phi ^ ")).\n"
fun strings_for_tptp_problem problem =
"% This file was generated by Isabelle (most likely Sledgehammer)\n\
\% " ^ timestamp () ^ "\n" ::
--- a/src/HOL/Tools/ATP/atp_systems.ML Fri Aug 20 15:29:36 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Aug 20 16:28:53 2010 +0200
@@ -18,8 +18,8 @@
arguments: bool -> Time.time -> string,
proof_delims: (string * string) list,
known_failures: (failure * string) list,
- max_new_relevant_facts_per_iter: int,
- prefers_theory_relevant: bool,
+ default_max_relevant_per_iter: int,
+ default_theory_relevant: bool,
explicit_forall: bool}
val string_for_failure : failure -> string
@@ -49,8 +49,8 @@
arguments: bool -> Time.time -> string,
proof_delims: (string * string) list,
known_failures: (failure * string) list,
- max_new_relevant_facts_per_iter: int,
- prefers_theory_relevant: bool,
+ default_max_relevant_per_iter: int,
+ default_theory_relevant: bool,
explicit_forall: bool}
val missing_message_tail =
@@ -144,8 +144,8 @@
"# Cannot determine problem status within resource limit"),
(OutOfResources, "SZS status: ResourceOut"),
(OutOfResources, "SZS status ResourceOut")],
- max_new_relevant_facts_per_iter = 50 (* FIXME *),
- prefers_theory_relevant = false,
+ default_max_relevant_per_iter = 50 (* FIXME *),
+ default_theory_relevant = false,
explicit_forall = false}
val e = ("e", e_config)
@@ -171,8 +171,8 @@
(MalformedInput, "Undefined symbol"),
(MalformedInput, "Free Variable"),
(SpassTooOld, "tptp2dfg")],
- max_new_relevant_facts_per_iter = 35 (* FIXME *),
- prefers_theory_relevant = true,
+ default_max_relevant_per_iter = 35 (* FIXME *),
+ default_theory_relevant = true,
explicit_forall = true}
val spass = ("spass", spass_config)
@@ -185,7 +185,7 @@
required_execs = [],
arguments = fn _ => fn timeout =>
"--mode casc -t " ^ string_of_int (to_generous_secs timeout) ^
- " --input_file",
+ " --thanks Andrei --input_file",
proof_delims =
[("=========== Refutation ==========",
"======= End of refutation ======="),
@@ -196,10 +196,9 @@
(IncompleteUnprovable, "CANNOT PROVE"),
(TimedOut, "SZS status Timeout"),
(Unprovable, "Satisfiability detected"),
- (OutOfResources, "Refutation not found"),
(VampireTooOld, "not a valid option")],
- max_new_relevant_facts_per_iter = 45 (* FIXME *),
- prefers_theory_relevant = false,
+ default_max_relevant_per_iter = 45 (* FIXME *),
+ default_theory_relevant = false,
explicit_forall = false}
val vampire = ("vampire", vampire_config)
@@ -220,52 +219,73 @@
fun refresh_systems_on_tptp () =
Synchronized.change systems (fn _ => get_systems ())
-fun get_system prefix = Synchronized.change_result systems (fn systems =>
- (if null systems then get_systems () else systems)
- |> `(find_first (String.isPrefix prefix)));
+fun get_system prefix =
+ Synchronized.change_result systems
+ (fn systems => (if null systems then get_systems () else systems)
+ |> `(find_first (String.isPrefix prefix)))
fun the_system prefix =
(case get_system prefix of
NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP.")
| SOME sys => sys);
-fun remote_config atp_prefix
- ({proof_delims, known_failures, max_new_relevant_facts_per_iter,
- prefers_theory_relevant, ...} : prover_config) : prover_config =
+fun remote_config system_prefix proof_delims known_failures
+ default_max_relevant_per_iter default_theory_relevant =
{exec = ("ISABELLE_ATP", "scripts/remote_atp"),
required_execs = [],
arguments = fn _ => fn timeout =>
" -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
- the_system atp_prefix,
+ the_system system_prefix,
proof_delims = insert (op =) tstp_proof_delims proof_delims,
known_failures =
known_failures @ known_perl_failures @
[(TimedOut, "says Timeout")],
- max_new_relevant_facts_per_iter = max_new_relevant_facts_per_iter,
- prefers_theory_relevant = prefers_theory_relevant,
+ default_max_relevant_per_iter = default_max_relevant_per_iter,
+ default_theory_relevant = default_theory_relevant,
explicit_forall = true}
-val remote_name = prefix "remote_"
-fun remote_prover (name, config) atp_prefix =
- (remote_name name, remote_config atp_prefix config)
+fun remotify_config system_prefix
+ ({proof_delims, known_failures, default_max_relevant_per_iter,
+ default_theory_relevant, ...} : prover_config) : prover_config =
+ remote_config system_prefix proof_delims known_failures
+ default_max_relevant_per_iter default_theory_relevant
-val remote_e = remote_prover e "EP---"
-val remote_vampire = remote_prover vampire "Vampire---9"
+val remotify_name = prefix "remote_"
+fun remote_prover name system_prefix proof_delims known_failures
+ default_max_relevant_per_iter default_theory_relevant =
+ (remotify_name name,
+ remote_config system_prefix proof_delims known_failures
+ default_max_relevant_per_iter default_theory_relevant)
+fun remotify_prover (name, config) system_prefix =
+ (remotify_name name, remotify_config system_prefix config)
+val remote_e = remotify_prover e "EP---"
+val remote_vampire = remotify_prover vampire "Vampire---9"
+val remote_sine_e =
+ remote_prover "sine_e" "SInE---" []
+ [(Unprovable, "says Unknown")] 150 (* FIXME *) false
+val remote_snark =
+ remote_prover "snark" "SNARK---" [("refutation.", "end_refutation.")] []
+ 50 (* FIXME *) false
(* Setup *)
fun is_installed ({exec, required_execs, ...} : prover_config) =
forall (curry (op <>) "" o getenv o fst) (exec :: required_execs)
fun maybe_remote (name, config) =
- name |> not (is_installed config) ? remote_name
+ name |> not (is_installed config) ? remotify_name
fun default_atps_param_value () =
space_implode " " ([maybe_remote e] @
(if is_installed (snd spass) then [fst spass] else []) @
- [remote_name (fst vampire)])
+ [if forall (is_installed o snd) [e, spass] then
+ remotify_name (fst vampire)
+ else
+ maybe_remote vampire,
+ fst remote_sine_e])
-val provers = [e, spass, vampire, remote_e, remote_vampire]
+val provers = [e, spass, vampire, remote_e, remote_vampire, remote_sine_e,
+ remote_snark]
val setup = fold add_prover provers
end;
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Fri Aug 20 15:29:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Fri Aug 20 16:28:53 2010 +0200
@@ -7,6 +7,7 @@
signature CLAUSIFIER =
sig
+ val transform_elim_theorem : thm -> thm
val introduce_combinators_in_cterm : cterm -> thm
val introduce_combinators_in_theorem : thm -> thm
val cnf_axiom: theory -> thm -> thm list
@@ -83,7 +84,7 @@
val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
(* Removes the lambdas from an equation of the form "t = (%x. u)".
- (Cf. "extensionalize_term" in "ATP_Systems".) *)
+ (Cf. "extensionalize_term" in "Sledgehammer_Translate".) *)
fun extensionalize_theorem th =
case prop_of th of
_ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _]))
@@ -223,12 +224,13 @@
(* Converts an Isabelle theorem (intro, elim or simp format, even higher-order)
into NNF. *)
fun to_nnf th ctxt0 =
- let val th1 = th |> transform_elim_theorem |> zero_var_indexes
- val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
- val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize
- |> extensionalize_theorem
- |> Meson.make_nnf ctxt
- in (th3, ctxt) end;
+ let
+ val th1 = th |> transform_elim_theorem |> zero_var_indexes
+ val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
+ val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize
+ |> extensionalize_theorem
+ |> Meson.make_nnf ctxt
+ in (th3, ctxt) end
(* Convert a theorem to CNF, with Skolem functions as additional premises. *)
fun cnf_axiom thy th =
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Aug 20 15:29:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Aug 20 16:28:53 2010 +0200
@@ -66,8 +66,10 @@
(* HOL to FOL (Isabelle to Metis) *)
(* ------------------------------------------------------------------------- *)
-fun fn_isa_to_met "equal" = "="
- | fn_isa_to_met x = x;
+fun fn_isa_to_met_sublevel "equal" = "=" (* FIXME: "c_fequal" *)
+ | fn_isa_to_met_sublevel x = x
+fun fn_isa_to_met_toplevel "equal" = "="
+ | fn_isa_to_met_toplevel x = x
fun metis_lit b c args = (b, (c, args));
@@ -89,7 +91,7 @@
| _ => raise METIS ("hol_term_to_fol_FO", "non first-order combterm")
fun hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
- Metis.Term.Fn (fn_isa_to_met a, map metis_term_from_combtyp tylist)
+ Metis.Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_combtyp tylist)
| hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s
| hol_term_to_fol_HO (CombApp (tm1, tm2)) =
Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
@@ -99,7 +101,7 @@
fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis.Term.Var s, ty)
| hol_term_to_fol_FT (CombConst((a, _), ty, _)) =
- wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty)
+ wrap_type (Metis.Term.Fn(fn_isa_to_met_sublevel a, []), ty)
| hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) =
wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
combtyp_of tm)
@@ -108,7 +110,7 @@
let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm
val tylits = if p = "equal" then [] else map metis_term_from_combtyp tys
val lits = map hol_term_to_fol_FO tms
- in metis_lit pos (fn_isa_to_met p) (tylits @ lits) end
+ in metis_lit pos (fn_isa_to_met_toplevel p) (tylits @ lits) end
| hol_literal_to_fol HO (FOLLiteral (pos, tm)) =
(case strip_combterm_comb tm of
(CombConst(("equal", _), _, _), tms) =>
@@ -224,13 +226,16 @@
fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
+fun smart_invert_const "fequal" = @{const_name "op ="}
+ | smart_invert_const s = invert_const s
+
fun hol_type_from_metis_term _ (Metis.Term.Var v) =
(case strip_prefix_and_undo_ascii tvar_prefix v of
SOME w => make_tvar w
| NONE => make_tvar v)
| hol_type_from_metis_term ctxt (Metis.Term.Fn(x, tys)) =
(case strip_prefix_and_undo_ascii type_const_prefix x of
- SOME tc => Term.Type (invert_const tc,
+ SOME tc => Term.Type (smart_invert_const tc,
map (hol_type_from_metis_term ctxt) tys)
| NONE =>
case strip_prefix_and_undo_ascii tfree_prefix x of
@@ -265,7 +270,7 @@
| applic_to_tt (a,ts) =
case strip_prefix_and_undo_ascii const_prefix a of
SOME b =>
- let val c = invert_const b
+ let val c = smart_invert_const b
val ntypes = num_type_args thy c
val nterms = length ts - ntypes
val tts = map tm_to_tt ts
@@ -283,7 +288,7 @@
| NONE => (*Not a constant. Is it a type constructor?*)
case strip_prefix_and_undo_ascii type_const_prefix a of
SOME b =>
- Type (Term.Type (invert_const b, types_of (map tm_to_tt ts)))
+ Type (Term.Type (smart_invert_const b, types_of (map tm_to_tt ts)))
| NONE => (*Maybe a TFree. Should then check that ts=[].*)
case strip_prefix_and_undo_ascii tfree_prefix a of
SOME b => Type (mk_tfree ctxt b)
@@ -311,7 +316,7 @@
Const (@{const_name "op ="}, HOLogic.typeT)
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
(case strip_prefix_and_undo_ascii const_prefix x of
- SOME c => Const (invert_const c, dummyT)
+ SOME c => Const (smart_invert_const c, dummyT)
| NONE => (*Not a constant. Is it a fixed variable??*)
case strip_prefix_and_undo_ascii fixed_var_prefix x of
SOME v => Free (v, hol_type_from_metis_term ctxt ty)
@@ -325,7 +330,7 @@
list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
| cvt (t as Metis.Term.Fn (x, [])) =
(case strip_prefix_and_undo_ascii const_prefix x of
- SOME c => Const (invert_const c, dummyT)
+ SOME c => Const (smart_invert_const c, dummyT)
| NONE => (*Not a constant. Is it a fixed variable??*)
case strip_prefix_and_undo_ascii fixed_var_prefix x of
SOME v => Free (v, dummyT)
@@ -598,9 +603,6 @@
(* Translation of HO Clauses *)
(* ------------------------------------------------------------------------- *)
-fun cnf_helper_theorem thy raw th =
- if raw then th else the_single (Clausifier.cnf_axiom thy th)
-
fun type_ext thy tms =
let val subs = tfree_classes_of_terms tms
val supers = tvar_classes_of_terms tms
@@ -650,15 +652,16 @@
| string_of_mode FT = "FT"
val helpers =
- [("c_COMBI", (false, @{thms COMBI_def})),
- ("c_COMBK", (false, @{thms COMBK_def})),
- ("c_COMBB", (false, @{thms COMBB_def})),
- ("c_COMBC", (false, @{thms COMBC_def})),
- ("c_COMBS", (false, @{thms COMBS_def})),
- ("c_fequal", (false, @{thms fequal_imp_equal equal_imp_fequal})),
- ("c_True", (true, @{thms True_or_False})),
- ("c_False", (true, @{thms True_or_False})),
- ("c_If", (true, @{thms if_True if_False True_or_False}))]
+ [("c_COMBI", (false, map (`I) @{thms COMBI_def})),
+ ("c_COMBK", (false, map (`I) @{thms COMBK_def})),
+ ("c_COMBB", (false, map (`I) @{thms COMBB_def})),
+ ("c_COMBC", (false, map (`I) @{thms COMBC_def})),
+ ("c_COMBS", (false, map (`I) @{thms COMBS_def})),
+ ("c_fequal", (false, map (rpair @{thm equal_imp_equal})
+ @{thms fequal_imp_equal equal_imp_fequal})),
+ ("c_True", (true, map (`I) @{thms True_or_False})),
+ ("c_False", (true, map (`I) @{thms True_or_False})),
+ ("c_If", (true, map (`I) @{thms if_True if_False True_or_False}))]
fun is_quasi_fol_clause thy =
Meson.is_fol_term thy o snd o conceal_skolem_terms ~1 [] o prop_of
@@ -673,18 +676,20 @@
| set_mode FT = FT
val mode = set_mode mode0
(*transform isabelle clause to metis clause *)
- fun add_thm is_conjecture ith {axioms, tfrees, skolems} : logic_map =
+ fun add_thm is_conjecture (metis_ith, isa_ith) {axioms, tfrees, skolems}
+ : logic_map =
let
val (mth, tfree_lits, skolems) =
- hol_thm_to_fol is_conjecture ctxt mode (length axioms) skolems ith
+ hol_thm_to_fol is_conjecture ctxt mode (length axioms) skolems
+ metis_ith
in
- {axioms = (mth, Meson.make_meta_clause ith) :: axioms,
+ {axioms = (mth, Meson.make_meta_clause isa_ith) :: axioms,
tfrees = union (op =) tfree_lits tfrees, skolems = skolems}
end;
val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolems = []}
- |> fold (add_thm true) cls
+ |> fold (add_thm true o `I) cls
|> add_tfrees
- |> fold (add_thm false) ths
+ |> fold (add_thm false o `I) ths
val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
fun is_used c =
exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists
@@ -695,11 +700,12 @@
let
val helper_ths =
helpers |> filter (is_used o fst)
- |> maps (fn (_, (raw, thms)) =>
- if mode = FT orelse not raw then
- map (cnf_helper_theorem @{theory} raw) thms
+ |> maps (fn (c, (needs_full_types, thms)) =>
+ if not (is_used c) orelse
+ needs_full_types andalso mode <> FT then
+ []
else
- [])
+ thms)
in lmap |> fold (add_thm false) helper_ths end
in (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap) end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Aug 20 15:29:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Aug 20 16:28:53 2010 +0200
@@ -20,12 +20,12 @@
explicit_apply: bool,
relevance_threshold: real,
relevance_convergence: real,
+ max_relevant_per_iter: int option,
theory_relevant: bool option,
defs_relevant: bool,
isar_proof: bool,
isar_shrink_factor: int,
- timeout: Time.time,
- minimize_timeout: Time.time}
+ timeout: Time.time}
type problem =
{subgoal: int,
goal: Proof.context * (thm list * thm),
@@ -89,12 +89,12 @@
explicit_apply: bool,
relevance_threshold: real,
relevance_convergence: real,
+ max_relevant_per_iter: int option,
theory_relevant: bool option,
defs_relevant: bool,
isar_proof: bool,
isar_shrink_factor: int,
- timeout: Time.time,
- minimize_timeout: Time.time}
+ timeout: Time.time}
type problem =
{subgoal: int,
@@ -208,10 +208,11 @@
fun prover_fun atp_name
{exec, required_execs, arguments, proof_delims, known_failures,
- max_new_relevant_facts_per_iter, prefers_theory_relevant,
+ default_max_relevant_per_iter, default_theory_relevant,
explicit_forall}
({debug, verbose, overlord, full_types, explicit_apply,
- relevance_threshold, relevance_convergence, theory_relevant,
+ relevance_threshold, relevance_convergence,
+ max_relevant_per_iter, theory_relevant,
defs_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
minimize_command
({subgoal, goal, relevance_override, axioms} : problem) =
@@ -231,8 +232,10 @@
(print_d (fn () => "Selecting relevant facts for " ^ quote atp_name ^
".");
relevant_facts full_types relevance_threshold relevance_convergence
- defs_relevant max_new_relevant_facts_per_iter
- (the_default prefers_theory_relevant theory_relevant)
+ defs_relevant
+ (the_default default_max_relevant_per_iter
+ max_relevant_per_iter)
+ (the_default default_theory_relevant theory_relevant)
relevance_override goal hyp_ts concl_t
|> tap ((fn n => print_v (fn () =>
"Selected " ^ string_of_int n ^ " fact" ^ plural_s n ^
@@ -331,21 +334,19 @@
()
else
File.write (Path.explode (Path.implode probfile ^ "_proof")) output
-
val ((pool, conjecture_shape, axiom_names),
(output, msecs, proof, outcome)) =
with_path cleanup export run_on (prob_pathname subgoal)
val (conjecture_shape, axiom_names) =
repair_conjecture_shape_and_theorem_names output conjecture_shape
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, axiom_names, th, subgoal)
- | SOME failure => (string_for_failure failure ^ "\n", [])
+ | SOME failure => (string_for_failure failure, [])
in
{outcome = outcome, message = message, pool = pool,
used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Aug 20 15:29:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Aug 20 16:28:53 2010 +0200
@@ -12,8 +12,6 @@
val trace : bool Unsynchronized.ref
val chained_prefix : string
- val name_thms_pair_from_ref :
- Proof.context -> thm list -> Facts.ref -> string * thm list
val relevant_facts :
bool -> real -> real -> bool -> int -> bool -> relevance_override
-> Proof.context * (thm list * 'a) -> term list -> term
@@ -37,27 +35,11 @@
(* Used to label theorems chained into the goal. *)
val chained_prefix = sledgehammer_prefix ^ "chained_"
-fun name_thms_pair_from_ref ctxt chained_ths xref =
- let
- val ths = ProofContext.get_fact ctxt xref
- val name = Facts.string_of_ref xref
- |> forall (member Thm.eq_thm chained_ths) ths
- ? prefix chained_prefix
- in (name, ths) end
-
(***************************************************************)
(* Relevance Filtering *)
(***************************************************************)
-fun strip_Trueprop_and_all (@{const Trueprop} $ t) =
- strip_Trueprop_and_all t
- | strip_Trueprop_and_all (Const (@{const_name all}, _) $ Abs (_, _, t)) =
- strip_Trueprop_and_all t
- | strip_Trueprop_and_all (Const (@{const_name All}, _) $ Abs (_, _, t)) =
- strip_Trueprop_and_all t
- | strip_Trueprop_and_all t = t
-
(*** constants with types ***)
(*An abstraction of Isabelle types*)
@@ -82,9 +64,9 @@
(*Pairs a constant with the list of its type instantiations (using const_typ)*)
fun const_with_typ thy (c,typ) =
- let val tvars = Sign.const_typargs thy (c,typ)
- in (c, map const_typ_of tvars) end
- handle TYPE _ => (c,[]); (*Variable (locale constant): monomorphic*)
+ let val tvars = Sign.const_typargs thy (c,typ) in
+ (c, map const_typ_of tvars) end
+ handle TYPE _ => (c, []) (*Variable (locale constant): monomorphic*)
(*Add a const/type pair to the table, but a [] entry means a standard connective,
which we ignore.*)
@@ -95,52 +77,64 @@
val fresh_prefix = "Sledgehammer.Fresh."
val flip = Option.map not
(* These are typically simplified away by "Meson.presimplify". *)
-val boring_consts = [@{const_name If}, @{const_name Let}]
+val boring_consts =
+ [@{const_name If}, @{const_name Let} (* TODO: , @{const_name Set.member}, @{const_name Collect} *)]
fun get_consts_typs thy pos ts =
let
- (* Free variables are included, as well as constants, to handle locales.
- "skolem_id" is included to increase the complexity of theorems containing
- Skolem functions. In non-CNF form, "Ex" is included but each occurrence
- is considered fresh, to simulate the effect of Skolemization. *)
+ (* We include free variables, as well as constants, to handle locales. For
+ each quantifiers that must necessarily be skolemized by the ATP, we
+ introduce a fresh constant to simulate the effect of Skolemization. *)
fun do_term t =
case t of
Const x => add_const_type_to_table (const_with_typ thy x)
- | Free x => add_const_type_to_table (const_with_typ thy x)
- | (t as Const (@{const_name skolem_id}, _)) $ _ => do_term t
+ | Free (s, _) => add_const_type_to_table (s, [])
| t1 $ t2 => do_term t1 #> do_term t2
| Abs (_, _, t) =>
(* Abstractions lead to combinators, so we add a penalty for them. *)
add_const_type_to_table (gensym fresh_prefix, [])
#> do_term t
| _ => I
- fun do_quantifier sweet_pos pos body_t =
+ fun do_quantifier will_surely_be_skolemized body_t =
do_formula pos body_t
- #> (if pos = SOME sweet_pos then I
- else add_const_type_to_table (gensym fresh_prefix, []))
- and do_equality T t1 t2 =
- fold (if T = @{typ bool} orelse T = @{typ prop} then do_formula NONE
- else do_term) [t1, t2]
+ #> (if will_surely_be_skolemized then
+ add_const_type_to_table (gensym fresh_prefix, [])
+ else
+ I)
+ and do_term_or_formula T =
+ if T = @{typ bool} orelse T = @{typ prop} then do_formula NONE
+ else do_term
and do_formula pos t =
case t of
Const (@{const_name all}, _) $ Abs (_, _, body_t) =>
- do_quantifier false pos body_t
+ do_quantifier (pos = SOME false) body_t
| @{const "==>"} $ t1 $ t2 =>
do_formula (flip pos) t1 #> do_formula pos t2
| Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
- do_equality T t1 t2
+ fold (do_term_or_formula T) [t1, t2]
| @{const Trueprop} $ t1 => do_formula pos t1
| @{const Not} $ t1 => do_formula (flip pos) t1
| Const (@{const_name All}, _) $ Abs (_, _, body_t) =>
- do_quantifier false pos body_t
+ do_quantifier (pos = SOME false) body_t
| Const (@{const_name Ex}, _) $ Abs (_, _, body_t) =>
- do_quantifier true pos body_t
+ do_quantifier (pos = SOME true) body_t
| @{const "op &"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
| @{const "op |"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
| @{const "op -->"} $ t1 $ t2 =>
do_formula (flip pos) t1 #> do_formula pos t2
| Const (@{const_name "op ="}, Type (_, [T, _])) $ t1 $ t2 =>
- do_equality T t1 t2
+ fold (do_term_or_formula T) [t1, t2]
+ | Const (@{const_name If}, Type (_, [_, Type (_, [T, _])]))
+ $ t1 $ t2 $ t3 =>
+ do_formula NONE t1 #> fold (do_term_or_formula T) [t2, t3]
+ | Const (@{const_name Ex1}, _) $ Abs (_, _, body_t) =>
+ do_quantifier (is_some pos) body_t
+ | Const (@{const_name Ball}, _) $ t1 $ Abs (_, _, body_t) =>
+ do_quantifier (pos = SOME false)
+ (HOLogic.mk_imp (incr_boundvars 1 t1 $ Bound 0, body_t))
+ | Const (@{const_name Bex}, _) $ t1 $ Abs (_, _, body_t) =>
+ do_quantifier (pos = SOME true)
+ (HOLogic.mk_conj (incr_boundvars 1 t1 $ Bound 0, body_t))
| (t0 as Const (_, @{typ bool})) $ t1 =>
do_term t0 #> do_formula pos t1 (* theory constant *)
| _ => do_term t
@@ -186,7 +180,7 @@
fun count_axiom_consts theory_relevant thy (_, th) =
let
fun do_const (a, T) =
- let val (c, cts) = const_with_typ thy (a,T) in
+ let val (c, cts) = const_with_typ thy (a, T) in
(* Two-dimensional table update. Constant maps to types maps to
count. *)
CTtab.map_default (cts, 0) (Integer.add 1)
@@ -194,7 +188,6 @@
end
fun do_term (Const x) = do_const x
| do_term (Free x) = do_const x
- | do_term (Const (x as (@{const_name skolem_id}, _)) $ _) = do_const x
| do_term (t $ u) = do_term t #> do_term u
| do_term (Abs (_, _, t)) = do_term t
| do_term _ = I
@@ -233,7 +226,7 @@
fun add_expand_pairs (x,ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys;
fun consts_typs_of_term thy t =
- Symtab.fold add_expand_pairs (get_consts_typs thy (SOME false) [t]) []
+ Symtab.fold add_expand_pairs (get_consts_typs thy (SOME true) [t]) []
fun pair_consts_typs_axiom theory_relevant thy axiom =
(axiom, axiom |> snd |> theory_const_prop_of theory_relevant
@@ -270,82 +263,36 @@
(* Limit the number of new facts, to prevent runaway acceptance. *)
fun take_best max_new (newpairs : (annotated_thm * real) list) =
- let val nnew = length newpairs
- in
- if nnew <= max_new then (map #1 newpairs, [])
+ let val nnew = length newpairs in
+ if nnew <= max_new then
+ (map #1 newpairs, [])
else
- let val cls = sort compare_pairs newpairs
- val accepted = List.take (cls, max_new)
+ let
+ val newpairs = sort compare_pairs newpairs
+ val accepted = List.take (newpairs, max_new)
in
trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^
- ", exceeds the limit of " ^ Int.toString (max_new)));
+ ", exceeds the limit of " ^ Int.toString max_new));
trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
trace_msg (fn () => "Actually passed: " ^
space_implode ", " (map (fst o fst o fst) accepted));
-
- (map #1 accepted, map #1 (List.drop (cls, max_new)))
+ (map #1 accepted, map #1 (List.drop (newpairs, max_new)))
end
end;
-fun relevant_facts ctxt relevance_convergence defs_relevant max_new
- ({add, del, ...} : relevance_override) const_tab =
- let
- val thy = ProofContext.theory_of ctxt
- val add_thms = maps (ProofContext.get_fact ctxt) add
- val del_thms = maps (ProofContext.get_fact ctxt) del
- fun iter threshold rel_const_tab =
- let
- fun relevant ([], _) [] = [] (* Nothing added this iteration *)
- | relevant (newpairs, rejects) [] =
- let
- val (newrels, more_rejects) = take_best max_new newpairs
- val new_consts = maps #2 newrels
- val rel_const_tab =
- rel_const_tab |> fold add_const_type_to_table new_consts
- val threshold =
- threshold + (1.0 - threshold) / relevance_convergence
- in
- trace_msg (fn () => "relevant this iteration: " ^
- Int.toString (length newrels));
- map #1 newrels @ iter threshold rel_const_tab
- (more_rejects @ rejects)
- end
- | relevant (newrels, rejects)
- ((ax as (clsthm as (name, th), consts_typs)) :: axs) =
- let
- val weight =
- 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
- in
- if weight >= threshold orelse
- (defs_relevant andalso defines thy th rel_const_tab) then
- (trace_msg (fn () =>
- name ^ " passes: " ^ Real.toString weight
- (* ^ " consts: " ^ commas (map fst consts_typs) *));
- relevant ((ax, weight) :: newrels, rejects) axs)
- else
- relevant (newrels, ax :: rejects) axs
- end
- in
- trace_msg (fn () => "relevant_facts, current threshold: " ^
- Real.toString threshold);
- relevant ([], [])
- end
- in iter end
-
fun relevance_filter ctxt relevance_threshold relevance_convergence
- defs_relevant max_new theory_relevant relevance_override
- thy axioms goal_ts =
+ defs_relevant max_new theory_relevant
+ ({add, del, ...} : relevance_override) axioms goal_ts =
if relevance_threshold > 1.0 then
[]
else if relevance_threshold < 0.0 then
axioms
else
let
+ val thy = ProofContext.theory_of ctxt
val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
Symtab.empty
- val goal_const_tab = get_consts_typs thy (SOME true) goal_ts
+ val goal_const_tab = get_consts_typs thy (SOME false) goal_ts
val relevance_threshold = 0.8 * relevance_threshold (* FIXME *)
val _ =
trace_msg (fn () => "Initial constants: " ^
@@ -353,12 +300,56 @@
|> Symtab.dest
|> filter (curry (op <>) [] o snd)
|> map fst))
- val relevant =
- relevant_facts ctxt relevance_convergence defs_relevant max_new
- relevance_override const_tab relevance_threshold
- goal_const_tab
- (map (pair_consts_typs_axiom theory_relevant thy)
- axioms)
+ val add_thms = maps (ProofContext.get_fact ctxt) add
+ val del_thms = maps (ProofContext.get_fact ctxt) del
+ fun iter threshold rel_const_tab =
+ let
+ fun relevant ([], rejects) [] =
+ (* Nothing was added this iteration: Add "add:" facts. *)
+ if null add_thms then
+ []
+ else
+ map_filter (fn (p as (name, th), _) =>
+ if member Thm.eq_thm add_thms th then SOME p
+ else NONE) rejects
+ | relevant (newpairs, rejects) [] =
+ let
+ val (newrels, more_rejects) = take_best max_new newpairs
+ val new_consts = maps #2 newrels
+ val rel_const_tab =
+ rel_const_tab |> fold add_const_type_to_table new_consts
+ val threshold =
+ threshold + (1.0 - threshold) / relevance_convergence
+ in
+ trace_msg (fn () => "relevant this iteration: " ^
+ Int.toString (length newrels));
+ map #1 newrels @ iter threshold rel_const_tab
+ (more_rejects @ rejects)
+ end
+ | relevant (newrels, rejects)
+ ((ax as ((name, th), consts_typs)) :: axs) =
+ let
+ val weight =
+ if member Thm.eq_thm del_thms th then 0.0
+ else formula_weight const_tab rel_const_tab consts_typs
+ in
+ if weight >= threshold orelse
+ (defs_relevant andalso defines thy th rel_const_tab) then
+ (trace_msg (fn () =>
+ name ^ " passes: " ^ Real.toString weight
+ (* ^ " consts: " ^ commas (map fst consts_typs) *));
+ relevant ((ax, weight) :: newrels, rejects) axs)
+ else
+ relevant (newrels, ax :: rejects) axs
+ end
+ in
+ trace_msg (fn () => "relevant_facts, current threshold: " ^
+ Real.toString threshold);
+ relevant ([], [])
+ end
+ val relevant = iter relevance_threshold goal_const_tab
+ (map (pair_consts_typs_axiom theory_relevant thy)
+ axioms)
in
trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant));
relevant
@@ -438,7 +429,7 @@
exists_sledgehammer_const t orelse is_strange_thm thm
end
-fun all_name_thms_pairs ctxt chained_ths =
+fun all_name_thms_pairs ctxt add_thms chained_ths =
let
val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
val local_facts = ProofContext.facts_of ctxt;
@@ -447,21 +438,22 @@
fun valid_facts facts =
(facts, []) |-> Facts.fold_static (fn (name, ths0) =>
- if Facts.is_concealed facts name orelse
- (respect_no_atp andalso is_package_def name) orelse
- member (op =) multi_base_blacklist (Long_Name.base_name name) orelse
- String.isSuffix "_def_raw" (* FIXME: crude hack *) name then
+ if (Facts.is_concealed facts name orelse
+ (respect_no_atp andalso is_package_def name) orelse
+ member (op =) multi_base_blacklist (Long_Name.base_name name) orelse
+ String.isSuffix "_def_raw" (* FIXME: crude hack *) name) andalso
+ forall (not o member Thm.eq_thm add_thms) ths0 then
I
else
let
fun check_thms a =
(case try (ProofContext.get_thms ctxt) a of
NONE => false
- | SOME ths1 => Thm.eq_thms (ths0, ths1));
-
+ | SOME ths1 => Thm.eq_thms (ths0, ths1))
val name1 = Facts.extern facts name;
val name2 = Name_Space.extern full_space name;
- val ths = filter_out is_theorem_bad_for_atps ths0
+ val ths = filter (fn th => not (is_theorem_bad_for_atps th) orelse
+ member Thm.eq_thm add_thms th) ths0
in
case find_first check_thms [name1, name2, name] of
NONE => I
@@ -518,54 +510,70 @@
| too_general_eqterms (Bound j) t = not (loose_bvar1 (t, j))
| too_general_eqterms _ _ = false
-fun too_general_equality (Const (@{const_name "op ="}, _) $ t1 $ t2) =
- too_general_eqterms t1 t2 orelse too_general_eqterms t2 t1
- | too_general_equality _ = false
+val is_exhaustive_finite =
+ let
+ fun do_equals t1 t2 =
+ too_general_eqterms t1 t2 orelse too_general_eqterms t2 t1
+ fun do_formula pos t =
+ case (pos, t) of
+ (_, @{const Trueprop} $ t1) => do_formula pos t1
+ | (true, Const (@{const_name all}, _) $ Abs (_, _, t')) =>
+ do_formula pos t'
+ | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) =>
+ do_formula pos t'
+ | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) =>
+ do_formula pos t'
+ | (_, @{const "==>"} $ t1 $ t2) =>
+ do_formula (not pos) t1 andalso do_formula pos t2
+ | (_, @{const "op -->"} $ t1 $ t2) =>
+ do_formula (not pos) t1 andalso do_formula pos t2
+ | (_, @{const Not} $ t1) => do_formula (not pos) t1
+ | (true, @{const "op |"} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
+ | (false, @{const "op &"} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
+ | (true, Const (@{const_name "op ="}, _) $ t1 $ t2) => do_equals t1 t2
+ | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
+ | (_, @{const False}) => true
+ | (_, @{const True}) => true
+ | _ => false
+ in do_formula true end
-fun has_typed_var tycons = exists_subterm
- (fn Var (_, Type (a, _)) => member (op =) tycons a | _ => false);
+
+fun has_bound_or_var_of_type tycons =
+ exists_subterm (fn Var (_, Type (s, _)) => member (op =) tycons s
+ | Abs (_, Type (s, _), _) => member (op =) tycons s
+ | _ => false)
(* Facts are forbidden to contain variables of these types. The typical reason
is that they lead to unsoundness. Note that "unit" satisfies numerous
equations like "?x = ()". The resulting clauses will have no type constraint,
yielding false proofs. Even "bool" leads to many unsound proofs, though only
for higher-order problems. *)
-val dangerous_types = [@{type_name unit}, @{type_name bool}];
+val dangerous_types = [@{type_name unit}, @{type_name bool}, @{type_name prop}];
(* Facts containing variables of type "unit" or "bool" or of the form
"ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types
are omitted. *)
-fun is_dangerous_term _ @{prop True} = true
- | is_dangerous_term full_types t =
- not full_types andalso
- (has_typed_var dangerous_types t orelse
- forall too_general_equality (HOLogic.disjuncts (strip_Trueprop_and_all t)))
+fun is_dangerous_term full_types t =
+ not full_types andalso
+ (has_bound_or_var_of_type dangerous_types t orelse is_exhaustive_finite t)
fun relevant_facts full_types relevance_threshold relevance_convergence
defs_relevant max_new theory_relevant
(relevance_override as {add, del, only})
(ctxt, (chained_ths, _)) hyp_ts concl_t =
let
- 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 =
checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
- (map (name_thms_pair_from_ref ctxt chained_ths) add @
- (if only then [] else all_name_thms_pairs ctxt chained_ths))
- |> 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*)
- not (is_dangerous_term full_types (prop_of th))))
+ (if only then [] else all_name_thms_pairs ctxt add_thms chained_ths)
+ |> make_unique
+ |> map (apsnd Clausifier.transform_elim_theorem)
+ |> filter (fn (_, th) => member Thm.eq_thm add_thms th orelse
+ not (is_dangerous_term full_types (prop_of th)))
in
relevance_filter ctxt relevance_threshold relevance_convergence
defs_relevant max_new theory_relevant relevance_override
- thy axioms (concl_t :: hyp_ts)
- |> has_override ? make_unique
+ axioms (concl_t :: hyp_ts)
|> sort_wrt fst
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Fri Aug 20 15:29:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Fri Aug 20 16:28:53 2010 +0200
@@ -18,6 +18,7 @@
structure Sledgehammer_Fact_Minimize : SLEDGEHAMMER_FACT_MINIMIZE =
struct
+open ATP_Systems
open Sledgehammer_Util
open Sledgehammer_Fact_Filter
open Sledgehammer_Proof_Reconstruct
@@ -42,9 +43,9 @@
end
fun test_theorems ({debug, verbose, overlord, atps, full_types,
- relevance_threshold, relevance_convergence, theory_relevant,
- defs_relevant, isar_proof, isar_shrink_factor,
- ...} : params)
+ relevance_threshold, relevance_convergence,
+ defs_relevant, isar_proof, isar_shrink_factor, ...}
+ : params)
(prover : prover) explicit_apply timeout subgoal state
name_thms_pairs =
let
@@ -55,9 +56,9 @@
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}
+ max_relevant_per_iter = NONE, theory_relevant = NONE,
+ defs_relevant = defs_relevant, isar_proof = isar_proof,
+ isar_shrink_factor = isar_shrink_factor, 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 =
@@ -93,32 +94,29 @@
(* 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
+val fudge_msecs = 1000
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, ...})
+ (params as {debug, atps = atp :: _, full_types, isar_proof,
+ isar_shrink_factor, 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 msecs = Time.toMilliseconds timeout
+ val _ = priority ("Sledgehammer minimize: ATP " ^ quote atp ^ ".")
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))
+ (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
+ (case do_test timeout name_thms_pairs of
result as {outcome = NONE, pool, used_thm_names,
conjecture_shape, ...} =>
let
@@ -156,6 +154,14 @@
handle ERROR msg => (NONE, "Error: " ^ msg)
end
+fun name_thms_pair_from_ref ctxt chained_ths xref =
+ let
+ val ths = ProofContext.get_fact ctxt xref
+ val name = Facts.string_of_ref xref
+ |> forall (member Thm.eq_thm chained_ths) ths
+ ? prefix chained_prefix
+ in (name, ths) end
+
fun run_minimize params i refs state =
let
val ctxt = Proof.context_of state
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Aug 20 15:29:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Aug 20 16:28:53 2010 +0200
@@ -69,11 +69,11 @@
("explicit_apply", "false"),
("relevance_threshold", "50"),
("relevance_convergence", "320"),
+ ("max_relevant_per_iter", "smart"),
("theory_relevant", "smart"),
("defs_relevant", "false"),
("isar_proof", "false"),
- ("isar_shrink_factor", "1"),
- ("minimize_timeout", "5 s")]
+ ("isar_shrink_factor", "1")]
val alias_params =
[("atp", "atps")]
@@ -89,7 +89,7 @@
val params_for_minimize =
["debug", "verbose", "overlord", "full_types", "isar_proof",
- "isar_shrink_factor", "minimize_timeout"]
+ "isar_shrink_factor", "timeout"]
val property_dependent_params = ["atps", "full_types", "timeout"]
@@ -158,6 +158,10 @@
SOME n => n
| NONE => error ("Parameter " ^ quote name ^
" must be assigned an integer value.")
+ fun lookup_int_option name =
+ case lookup name of
+ SOME "smart" => NONE
+ | _ => SOME (lookup_int name)
val debug = lookup_bool "debug"
val verbose = debug orelse lookup_bool "verbose"
val overlord = lookup_bool "overlord"
@@ -168,20 +172,21 @@
0.01 * Real.fromInt (lookup_int "relevance_threshold")
val relevance_convergence =
0.01 * Real.fromInt (lookup_int "relevance_convergence")
+ val max_relevant_per_iter = lookup_int_option "max_relevant_per_iter"
val theory_relevant = lookup_bool_option "theory_relevant"
val defs_relevant = lookup_bool "defs_relevant"
val isar_proof = lookup_bool "isar_proof"
val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
val timeout = lookup_time "timeout"
- val minimize_timeout = lookup_time "minimize_timeout"
in
{debug = debug, verbose = verbose, overlord = overlord, atps = atps,
full_types = full_types, explicit_apply = explicit_apply,
relevance_threshold = relevance_threshold,
relevance_convergence = relevance_convergence,
+ max_relevant_per_iter = max_relevant_per_iter,
theory_relevant = theory_relevant, defs_relevant = defs_relevant,
isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
- timeout = timeout, minimize_timeout = minimize_timeout}
+ timeout = timeout}
end
fun get_params thy = extract_params (default_raw_params thy)
@@ -200,9 +205,6 @@
val kill_atpsN = "kill_atps"
val refresh_tptpN = "refresh_tptp"
-fun minimizize_raw_param_name "timeout" = "minimize_timeout"
- | minimizize_raw_param_name name = name
-
val is_raw_param_relevant_for_minimize =
member (op =) params_for_minimize o fst o unalias_raw_param
fun string_for_raw_param (key, values) =
@@ -226,9 +228,8 @@
(minimize_command override_params i) state
end
else if subcommand = minimizeN then
- run_minimize (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 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 Fri Aug 20 15:29:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Aug 20 16:28:53 2010 +0200
@@ -10,7 +10,6 @@
sig
type minimize_command = string list -> string
- val metis_line: bool -> int -> int -> string list -> string
val metis_proof_text:
bool * minimize_command * string * string vector * thm * int
-> string * string list
@@ -547,6 +546,17 @@
(** EXTRACTING LEMMAS **)
+(* Like "split_line", but ignores "\n" that follow a comma (as in SNARK's
+ output). *)
+val split_proof_lines =
+ let
+ fun aux [] [] = []
+ | aux line [] = [implode (rev line)]
+ | aux line ("," :: "\n" :: rest) = aux ("," :: line) rest
+ | aux line ("\n" :: rest) = aux line [] @ aux [] rest
+ | aux line (s :: rest) = aux (s :: line) rest
+ in aux [] o explode end
+
(* A list consisting of the first number in each line is returned. For TSTP,
interesting lines have the form "fof(108, axiom, ...)", where the number
(108) is extracted. For SPASS, lines have the form "108[0:Inp] ...", where
@@ -564,16 +574,19 @@
val tokens_of =
String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_")
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 =>
- if member (op =) rest "file" then SOME name else axiom_name num
- | NONE => axiom_name num)
+ fun do_line (tag :: num :: "axiom" :: (rest as _ :: _)) =
+ if tag = "cnf" orelse tag = "fof" then
+ (case strip_prefix_and_undo_ascii axiom_prefix (List.last rest) of
+ SOME name =>
+ if member (op =) rest "file" then SOME name else axiom_name num
+ | NONE => axiom_name num)
+ else
+ NONE
| do_line (num :: "0" :: "Inp" :: _) = axiom_name num
| do_line (num :: rest) =
(case List.last rest of "input" => axiom_name num | _ => NONE)
| do_line _ = NONE
- in atp_proof |> split_lines |> map_filter (do_line o tokens_of) end
+ in atp_proof |> split_proof_lines |> map_filter (do_line o tokens_of) end
val indent_size = 2
val no_label = ("", ~1)
@@ -598,14 +611,14 @@
metis_using ls ^ metis_apply i n ^ metis_call full_types ss
fun metis_line full_types i n ss =
"Try this command: " ^
- Markup.markup Markup.sendback (metis_command full_types i n ([], ss)) ^ ".\n"
+ Markup.markup Markup.sendback (metis_command full_types i n ([], ss)) ^ "."
fun minimize_line _ [] = ""
| minimize_line minimize_command facts =
case minimize_command facts of
"" => ""
| command =>
- "To minimize the number of lemmas, try this: " ^
- Markup.markup Markup.sendback command ^ ".\n"
+ "\nTo minimize the number of lemmas, try this: " ^
+ Markup.markup Markup.sendback command ^ "."
val unprefix_chained = perhaps (try (unprefix chained_prefix))
@@ -984,7 +997,7 @@
(if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
do_indent 0 ^ "proof -\n" ^
do_steps "" "" 1 proof ^
- do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n"
+ do_indent 0 ^ (if n <> 1 then "next" else "qed")
in do_proof end
fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
@@ -1006,14 +1019,14 @@
|> kill_useless_labels_in_proof
|> relabel_proof
|> string_for_proof ctxt full_types i n of
- "" => "No structured proof available.\n"
- | proof => "\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
+ "" => "\nNo structured proof available."
+ | proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
val isar_proof =
if debug then
isar_proof_for ()
else
try isar_proof_for ()
- |> the_default "Warning: The Isar proof construction failed.\n"
+ |> the_default "\nWarning: The Isar proof construction failed."
in (one_line_proof ^ isar_proof, lemma_names) end
fun proof_text isar_proof isar_params other_params =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Fri Aug 20 15:29:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Fri Aug 20 16:28:53 2010 +0200
@@ -79,17 +79,6 @@
|>> 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
@@ -103,6 +92,25 @@
subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
(0 upto length Ts - 1 ~~ Ts))
+(* Removes the lambdas from an equation of the form "t = (%x. u)".
+ (Cf. "extensionalize_theorem" in "Clausifier".) *)
+fun extensionalize_term t =
+ let
+ fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t'
+ | aux j (t as Const (s, Type (_, [Type (_, [_, T']),
+ Type (_, [_, res_T])]))
+ $ t2 $ Abs (var_s, var_T, t')) =
+ if s = @{const_name "op ="} orelse s = @{const_name "=="} then
+ let val var_t = Var ((var_s, j), var_T) in
+ Const (s, T' --> T' --> res_T)
+ $ betapply (t2, var_t) $ subst_bound (var_t, t')
+ |> aux (j + 1)
+ end
+ else
+ t
+ | aux _ t = t
+ in aux (maxidx_of_term t + 1) t end
+
fun introduce_combinators_in_term ctxt kind t =
let val thy = ProofContext.theory_of ctxt in
if Meson.is_fol_term thy t then
@@ -135,9 +143,8 @@
in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
handle THM _ =>
(* A type variable of sort "{}" will make abstraction fail. *)
- case kind of
- Axiom => HOLogic.true_const
- | Conjecture => HOLogic.false_const
+ if kind = Conjecture then HOLogic.false_const
+ else HOLogic.true_const
end
(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
@@ -151,18 +158,33 @@
| aux t = t
in t |> exists_subterm is_Var t ? aux end
+(* "Object_Logic.atomize_term" isn't as powerful as it could be; for example,
+ it leaves metaequalities over "prop"s alone. *)
+val atomize_term =
+ let
+ fun aux (@{const Trueprop} $ t1) = t1
+ | aux (Const (@{const_name all}, _) $ Abs (s, T, t')) =
+ HOLogic.all_const T $ Abs (s, T, aux t')
+ | aux (@{const "==>"} $ t1 $ t2) = HOLogic.mk_imp (pairself aux (t1, t2))
+ | aux (Const (@{const_name "=="}, Type (_, [@{typ prop}, _])) $ t1 $ t2) =
+ HOLogic.eq_const HOLogic.boolT $ aux t1 $ aux t2
+ | aux (Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2) =
+ HOLogic.eq_const T $ t1 $ t2
+ | aux _ = raise Fail "aux"
+ in perhaps (try aux) end
+
(* making axiom and conjecture formulas *)
-fun make_formula ctxt presimp (name, kind, t) =
+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 |> Envir.beta_eta_contract
+ |> atomize_term
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
+ |> kind <> Axiom ? freeze_term
val (combformula, ctypes_sorts) = combformula_for_prop thy t []
in
FOLFormula {name = name, combformula = combformula, kind = kind,
@@ -170,10 +192,13 @@
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
+ (name, make_formula ctxt presimp name Axiom (prop_of th))
+fun make_conjecture ctxt ts =
+ let val last = length ts - 1 in
+ map2 (fn j => make_formula ctxt true (Int.toString j)
+ (if j = last then Conjecture else Hypothesis))
+ (0 upto last) ts
+ end
(** Helper facts **)
@@ -194,7 +219,7 @@
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 mandatory_helpers = @{thms fequal_def}
val init_counters =
Symtab.make (maps (maps (map (rpair 0) o fst))
@@ -214,8 +239,6 @@
|> 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
@@ -236,7 +259,7 @@
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 conjectures = make_conjecture ctxt (hyp_ts @ [concl_t])
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
@@ -336,7 +359,7 @@
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))
+ Fof (tfrees_name, Hypothesis, formula_for_fo_literal lit)
fun problem_lines_for_free_types conjectures =
let
val litss = map free_type_literals_for_conjecture conjectures
@@ -420,8 +443,8 @@
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
+ s = "equal" orelse s = "$false" orelse s = "$true" 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} =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Aug 20 15:29:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Aug 20 16:28:53 2010 +0200
@@ -15,7 +15,6 @@
val nat_subscript : int -> string
val unyxml : string -> string
val maybe_quote : string -> string
- val extensionalize_term : term -> term
val monomorphic_term : Type.tyenv -> term -> term
val specialize_type : theory -> (string * typ) -> term -> term
val subgoal_count : Proof.state -> int
@@ -101,25 +100,6 @@
Keyword.is_keyword s) ? quote
end
-(* Removes the lambdas from an equation of the form "t = (%x. u)".
- (Cf. "extensionalize_theorem" in "Clausifier".) *)
-fun extensionalize_term t =
- let
- fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t'
- | aux j (t as Const (s, Type (_, [Type (_, [_, T']),
- Type (_, [_, res_T])]))
- $ t2 $ Abs (var_s, var_T, t')) =
- if s = @{const_name "op ="} orelse s = @{const_name "=="} then
- let val var_t = Var ((var_s, j), var_T) in
- Const (s, T' --> T' --> res_T)
- $ betapply (t2, var_t) $ subst_bound (var_t, t')
- |> aux (j + 1)
- end
- else
- t
- | aux _ t = t
- in aux (maxidx_of_term t + 1) t end
-
fun monomorphic_term subst t =
map_types (map_type_tvar (fn v =>
case Type.lookup subst v of
--- a/src/HOL/Tools/meson.ML Fri Aug 20 15:29:36 2010 +0200
+++ b/src/HOL/Tools/meson.ML Fri Aug 20 16:28:53 2010 +0200
@@ -520,7 +520,7 @@
forward_res ctxt (make_nnf1 ctxt)
(tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
handle THM ("tryres", _, _) => th
- else th;
+ else th
(*The simplification removes defined quantifiers and occurrences of True and False.
nnf_ss also includes the one-point simprocs,
@@ -539,8 +539,7 @@
#> simplify nnf_ss
fun make_nnf ctxt th = case prems_of th of
- [] => th |> presimplify
- |> make_nnf1 ctxt
+ [] => th |> presimplify |> make_nnf1 ctxt
| _ => raise THM ("make_nnf: premises in argument", 0, [th]);
(*Pull existential quantifiers to front. This accomplishes Skolemization for