# HG changeset patch
# User blanchet
# Date 1677654051 -3600
# Node ID e51aa922079a35fb1f7d32e134f99afe0ba6e545
# Parent  cdf5f392ea78a6412a3e067a95e477889183ce95
tweaked Sledgehammer interaction

diff -r cdf5f392ea78 -r e51aa922079a 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
@@ -44,10 +44,9 @@
     bool -> int Symtab.table ->
     (string, string, (string, string atp_type) atp_term, string) atp_formula -> term
 
+  val is_conjecture_used_in_proof : string atp_proof -> bool
   val used_facts_in_atp_proof : Proof.context -> (string * stature) list -> string atp_proof ->
     (string * stature) list
-  val used_facts_in_unsound_atp_proof : Proof.context -> (string * stature) list -> 'a atp_proof ->
-    string list option
   val atp_proof_prefers_lifting : string atp_proof -> bool
   val is_typed_helper_used_in_atp_proof : string atp_proof -> bool
   val replace_dependencies_in_line : atp_step_name * atp_step_name list -> ('a, 'b) atp_step ->
@@ -513,6 +512,8 @@
 fun is_axiom_used_in_proof pred =
   exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false)
 
+val is_conjecture_used_in_proof = is_axiom_used_in_proof (is_some o resolve_conjecture)
+
 fun add_fact ctxt facts ((num, ss), _, _, rule, deps) =
   (if member (op =) [agsyhol_core_rule, leo2_extcnf_equal_neg_rule] rule orelse
       String.isPrefix satallax_tab_rule_prefix rule then
@@ -524,19 +525,6 @@
 fun used_facts_in_atp_proof ctxt facts atp_proof =
   if null atp_proof then facts else fold (add_fact ctxt facts) atp_proof []
 
-fun used_facts_in_unsound_atp_proof _ _ [] = NONE
-  | used_facts_in_unsound_atp_proof ctxt facts atp_proof =
-    let
-      val used_facts = used_facts_in_atp_proof ctxt facts atp_proof
-      val all_global_facts = forall (fn (_, (sc, _)) => sc = Global) used_facts
-      val axiom_used = is_axiom_used_in_proof (is_some o resolve_conjecture) atp_proof
-    in
-      if all_global_facts andalso not axiom_used then
-        SOME (map fst used_facts)
-      else
-        NONE
-    end
-
 val ascii_of_lam_fact_prefix = ascii_of lam_fact_prefix
 
 (* overapproximation (good enough) *)
diff -r cdf5f392ea78 -r e51aa922079a src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Mar 01 08:00:51 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Mar 01 08:00:51 2023 +0100
@@ -261,7 +261,7 @@
             [] => "The goal is inconsistent"
           | facts => "The goal is falsified by these facts: " ^ commas facts)
         else
-          "The following facts are inconsistent: " ^
+          "Derived \"False\" from these facts alone: " ^
           commas (map fst used_facts)))
 
 fun check_expected_outcome ctxt prover_name expect outcome =
diff -r cdf5f392ea78 -r e51aa922079a 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
@@ -249,15 +249,7 @@
 
         val outcome =
           (case outcome of
-            NONE =>
-            (case used_facts_in_unsound_atp_proof ctxt (map fst facts) atp_proof of
-              SOME facts =>
-              let
-                val failure = UnsoundProof (is_type_enc_sound type_enc, sort string_ord facts)
-              in
-                if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure
-              end
-            | NONE => (found_something name; NONE))
+            NONE => (found_something name; NONE)
           | _ => outcome)
       in
         (atp_problem_data,
@@ -302,6 +294,13 @@
         NONE =>
         let
           val used_facts = sort_by fst (used_facts_in_atp_proof ctxt (map fst used_from) atp_proof)
+          val _ =
+            if mode = Normal andalso not (is_conjecture_used_in_proof atp_proof)
+               andalso not (Logic.get_goal (Thm.prop_of goal) subgoal aconv @{prop False}) then
+              warning ("Derived \"False\" from these facts alone: " ^ commas (map fst used_facts))
+            else
+              ()
+
           val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
           val preferred = Metis_Method (NONE, NONE)
           val preferred_methss =