# HG changeset patch
# User blanchet
# Date 1677654051 -3600
# Node ID 4e8a6354c54f55baa5fcd17e4a21592e7eb714b0
# Parent  f6cb40234009d76008284a7f67a4ee750c481b29
improve ad hoc abduction in Sledgehammer

diff -r f6cb40234009 -r 4e8a6354c54f 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
@@ -805,30 +805,47 @@
     []
   else
     let
-      fun split_min seen [] (_, best_item) = (best_item, List.rev seen)
-        | split_min seen ((score, item) :: scored_items) (best_score, best_item) =
+      fun split_min accum [] (_, best_item) = (best_item, List.rev accum)
+        | split_min accum ((score, item) :: scored_items) (best_score, best_item) =
           if score < best_score then
-            split_min ((best_score, best_item) :: seen) scored_items (score, item)
+            split_min ((best_score, best_item) :: accum) scored_items (score, item)
           else
-            split_min ((score, item) :: seen) scored_items (best_score, best_item)
+            split_min ((score, item) :: accum) scored_items (best_score, best_item)
 
       val (min_item, other_scored_items) = split_min [] (tl scored_items) (hd scored_items)
     in
       min_item :: sort_top (n - 1) (filter_out (equal min_item o snd) other_scored_items)
+      |> distinct (op aconv)
     end
 
 fun top_abduce_candidates max_candidates candidates =
   let
+    (* We prefer free variables to other constructs, so that e.g. "x \<le> y" is
+       prioritized over "x \<le> 0". *)
     fun score t =
-      size_of_term t +
-      (if exists_subterm (fn Bound _ => true | Var _ => true | _ => false) t then 50 else 0) +
-      (if exists_subterm (fn Free _ => true | _ => false) t then ~10 else 0)
+      Term.fold_aterms (fn t => fn score => score + (case t of Free _ => ~1 | _ => 4)) 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",
+       it may seem an odd choice for abduction, but it sometimes arises in
+       conjunction with type class constraints, which are removed by the
+       termifier. *)
     fun maybe_score t =
       (case t of
-        @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ Free _ $ _) => NONE
+        @{prop True} => NONE
+      | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ Free _ $ _) => NONE
       | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Free _) => NONE
+      | @{const Trueprop} $ (@{const less(nat)} $ _ $ @{const zero_class.zero(nat)}) => NONE
+      | @{const Trueprop} $ (@{const less_eq(nat)} $ _ $ @{const zero_class.zero(nat)}) => NONE
+      | @{const Trueprop} $ (@{const less(nat)} $ _ $ @{const one_class.one(nat)}) => NONE
+      | @{const Trueprop} $ (@{const Not} $
+          (@{const less(nat)} $ @{const zero_class.zero(nat)} $ _)) => NONE
+      | @{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 Trueprop} $ (Const (@{const_name All}, _) $ _) => NONE
+      | @{const Trueprop} $ (Const (@{const_name Ex}, _) $ _) => NONE
       | _ => SOME (score t, t))
   in
     sort_top max_candidates (map_filter maybe_score candidates)