# HG changeset patch
# User blanchet
# Date 1678458438 -3600
# Node ID 7c25451ae2c13a9a616fc15d4876dd3b6cb1fbab
# Parent  d39027e1c8c52644c6da379c14f23f0e471a59b1
use simplifier to classify the missing assumptions in Sledgehammer's abduction mechanism

diff -r d39027e1c8c5 -r 7c25451ae2c1 src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Fri Mar 10 11:56:52 2023 +0100
+++ b/src/HOL/Sledgehammer.thy	Fri Mar 10 15:27:18 2023 +0100
@@ -35,4 +35,10 @@
 ML_file \<open>Tools/Sledgehammer/sledgehammer_commands.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_tactics.ML\<close>
 
+(*
+lemma "x - y + y = (x::nat)"
+  sledgehammer[e, abduce = 10]
+  oops
+*)
+
 end
diff -r d39027e1c8c5 -r 7c25451ae2c1 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Fri Mar 10 11:56:52 2023 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Fri Mar 10 15:27:18 2023 +0100
@@ -64,6 +64,7 @@
     int Symtab.table -> (string, string, (string, string atp_type) atp_term, string) atp_formula ->
     term
   val top_abduce_candidates : int -> term list -> term list
+  val sort_propositions_by_provability : Proof.context -> term list -> term list
 end;
 
 structure ATP_Proof_Reconstruct : ATP_PROOF_RECONSTRUCT =
@@ -859,4 +860,25 @@
     sort_top max_candidates (map_filter maybe_score candidates)
   end
 
+fun provability_status ctxt t =
+  let
+    val res = Timeout.apply (seconds 0.1)
+      (Thm.term_of o Thm.rhs_of o Simplifier.full_rewrite ctxt) (Thm.cterm_of ctxt t)
+  in
+    if res aconv @{prop True} then SOME true
+    else if res aconv @{prop False} then SOME false
+    else NONE
+  end
+  handle Timeout.TIMEOUT _ => NONE
+
+(* Put propositions that simplify to "True" first, and filter out propositions
+   that simplify to "False". *)
+fun sort_propositions_by_provability ctxt ts =
+  let
+    val statuses_ts = map (`(provability_status ctxt)) ts
+  in
+    maps (fn (SOME true, t) => [t] | _ => []) statuses_ts @
+    maps (fn (NONE, t) => [t] | _ => []) statuses_ts
+  end
+
 end;
diff -r d39027e1c8c5 -r 7c25451ae2c1 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Mar 10 11:56:52 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Mar 10 15:27:18 2023 +0100
@@ -339,11 +339,14 @@
         end
       | SOME failure =>
         let
+          val max_abduce_candidates_factor = 3 (* FUDGE *)
           val max_abduce_candidates =
             the_default default_abduce_max_candidates abduce_max_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
+            |> top_abduce_candidates (max_abduce_candidates * max_abduce_candidates_factor)
+            |> sort_propositions_by_provability ctxt
+            |> take max_abduce_candidates
         in
           if null abduce_candidates then
             (SOME failure, [], (Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure)