--- a/src/Doc/Sledgehammer/document/root.tex Wed Mar 01 08:00:51 2023 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Wed Mar 01 08:00:51 2023 +0100
@@ -284,7 +284,7 @@
\prew
\slshape
-e: Candidate for missing hypothesis: \\
+e: Candidate missing assumption: \\
length ys = length xs
\postw
@@ -829,16 +829,16 @@
used or if a flawed lemma was introduced with \textbf{sorry}.
\opdefault{abduce}{smart\_int}{smart}
-Specifies the maximum number of candidate missing hypotheses that may be
+Specifies the maximum number of candidate missing assumptions that may be
displayed. These hypotheses are discovered heuristically by a process called
abduction (which stands in contrast to deduction)---that is, they are guessed
and found to be sufficient to prove the goal.
Abduction is currently supported only by E. If the option is set to
\textit{smart} (the default), abduction is enabled only in some of the E time
-slices, and only one candidate missing hypothesis is displayed. You can disable
-abduction altogether by setting the option to 0 or enable it in all time slices
-by setting it to a nonzero value.
+slices, and at most one candidate missing assumption is displayed. You can
+disable abduction altogether by setting the option to 0 or enable it in all
+time slices by setting it to a nonzero value.
\optrueonly{dont\_abduce}
Alias for ``\textit{abduce} = 0''.
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Mar 01 08:00:51 2023 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Mar 01 08:00:51 2023 +0100
@@ -823,7 +823,7 @@
(* We prefer free variables to other constructs, so that e.g. "x \<le> y" is
prioritized over "x \<le> 0". *)
fun score t =
- Term.fold_aterms (fn t => fn score => score + (case t of Free _ => ~1 | _ => 4)) t 0
+ Term.fold_aterms (fn t => fn score => score + (case t of Free _ => 1 | _ => 2)) t 0
(* Equations of the form "x = ..." or "... = x" or similar are too specific
to be useful. Quantified formulas are also filtered out. As for "True",
@@ -843,7 +843,7 @@
| @{const Trueprop} $ (@{const Not} $
(@{const less_eq(nat)} $ @{const zero_class.zero(nat)} $ _)) => NONE
| @{const Trueprop} $ (@{const Not} $
- (@{const less(nat)} $ @{const one_class.one(nat)} $ _)) => NONE
+ (@{const less_eq(nat)} $ @{const one_class.one(nat)} $ _)) => NONE
| @{const Trueprop} $ (Const (@{const_name All}, _) $ _) => NONE
| @{const Trueprop} $ (Const (@{const_name Ex}, _) $ _) => NONE
| _ => SOME (score t, t))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Mar 01 08:00:51 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Mar 01 08:00:51 2023 +0100
@@ -530,7 +530,7 @@
one_line_proof_text ctxt num_chained) one_line_params
fun abduce_text ctxt tms =
- "Candidate" ^ plural_s (length tms) ^ " for missing hypothesis:\n" ^
+ "Candidate missing assumption" ^ plural_s (length tms) ^ ":\n" ^
cat_lines (map (Syntax.string_of_term ctxt) tms)
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Wed Mar 01 08:00:51 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Wed Mar 01 08:00:51 2023 +0100
@@ -346,15 +346,15 @@
let
val max_abduce_candidates =
the_default default_abduce_max_candidates abduce_max_candidates
- val abduce_candidates =
- map (termify_atp_abduce_candidate ctxt name format type_enc pool lifted sym_tab)
- atp_abduce_candidates
+ val abduce_candidates = atp_abduce_candidates
+ |> map (termify_atp_abduce_candidate ctxt name format type_enc pool lifted sym_tab)
+ |> top_abduce_candidates max_abduce_candidates
in
if null abduce_candidates then
(SOME failure, [], (Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure)
else
(NONE, [], (Auto_Method (* dummy *), []), fn _ =>
- abduce_text ctxt (top_abduce_candidates max_abduce_candidates abduce_candidates))
+ abduce_text ctxt abduce_candidates)
end)
in
{outcome = outcome, used_facts = used_facts, used_from = used_from,