# HG changeset patch
# User blanchet
# Date 1677654051 -3600
# Node ID bde374587d939edeb6a894c0529c9d9823cc7118
# Parent  73611eb994cff796d032c25f792f6e6a43ad87de
tweaked abduction in Sledgehammer

diff -r 73611eb994cf -r bde374587d93 src/Doc/Sledgehammer/document/root.tex
--- 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''.
diff -r 73611eb994cf -r bde374587d93 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- 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))
diff -r 73611eb994cf -r bde374587d93 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- 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;
diff -r 73611eb994cf -r bde374587d93 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- 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,