# HG changeset patch
# User blanchet
# Date 1677654051 -3600
# Node ID 51dac6fcdd0e8b00dd0e0f830a8a47137d3121bc
# Parent  110988ad5b4cdfe196d5a466d03c775a784e6831
reverted 0506c3273814 -- the message is still useful

diff -r 110988ad5b4c -r 51dac6fcdd0e src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Mar 01 08:00:51 2023 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Mar 01 08:00:51 2023 +0100
@@ -24,6 +24,7 @@
     ProofMissing |
     ProofIncomplete |
     ProofUnparsable |
+    UnsoundProof of bool * string list |
     TimedOut |
     Inappropriate |
     OutOfResources |
@@ -144,6 +145,7 @@
   ProofMissing |
   ProofIncomplete |
   ProofUnparsable |
+  UnsoundProof of bool * string list |
   TimedOut |
   Inappropriate |
   OutOfResources |
@@ -160,12 +162,21 @@
   else
     ""
 
+fun from_lemmas [] = ""
+  | from_lemmas ss = " from " ^ space_implode " " (Try.serial_commas "and" (map quote ss))
+
 fun string_of_atp_failure MaybeUnprovable = "Problem maybe unprovable"
-  | string_of_atp_failure Unprovable = "Unprovable problem"
+  | string_of_atp_failure Unprovable = "Problem unprovable"
   | string_of_atp_failure GaveUp = "Gave up"
   | string_of_atp_failure ProofMissing = "Proof missing"
   | string_of_atp_failure ProofIncomplete = "Proof incomplete"
   | string_of_atp_failure ProofUnparsable = "Proof unparsable"
+  | string_of_atp_failure (UnsoundProof (false, ss)) =
+    "Derived the lemma \"False\"" ^ from_lemmas ss ^
+    ", likely due to the use of an unsound type encoding"
+  | string_of_atp_failure (UnsoundProof (true, ss)) =
+    "Derived the lemma \"False\"" ^ from_lemmas ss ^
+    ", likely due to inconsistent axioms or \"sorry\"d lemmas"
   | string_of_atp_failure TimedOut = "Timed out"
   | string_of_atp_failure Inappropriate = "Problem outside the prover's scope"
   | string_of_atp_failure OutOfResources = "Out of resources"
diff -r 110988ad5b4c -r 51dac6fcdd0e 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
@@ -46,6 +46,8 @@
 
   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 ->
@@ -522,6 +524,19 @@
 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 110988ad5b4c -r 51dac6fcdd0e src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Wed Mar 01 08:00:51 2023 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML	Wed Mar 01 08:00:51 2023 +0100
@@ -62,8 +62,7 @@
 val timestamp = timestamp_format o Time.now
 
 (* This hash function is recommended in "Compilers: Principles, Techniques, and
-   Tools" by Aho, Sethi, and Ullman. The "hashpjw" function, which they
-   particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *)
+   Tools" by Aho, Sethi, and Ullman. *)
 fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
 fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)
 fun hashw_string (s : string, w) = CharVector.foldl hashw_char w s
@@ -416,8 +415,8 @@
 
 val map_prod = Ctr_Sugar_Util.map_prod
 
-(* Compare the length of a list with an integer n while traversing at most n elements of the list.
-*)
+(* Compare the length of a list with an integer n while traversing at most n
+elements of the list. *)
 fun compare_length_with [] n = if n < 0 then GREATER else if n = 0 then EQUAL else LESS
   | compare_length_with (_ :: xs) n = if n <= 0 then GREATER else compare_length_with xs (n - 1)
 
diff -r 110988ad5b4c -r 51dac6fcdd0e 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
@@ -247,10 +247,18 @@
           (state, subgoal, name, "Running command in " ^
              string_of_int (Time.toMilliseconds run_time) ^ " ms"))
 
-        val _ =
+        val outcome =
           (case outcome of
-            NONE => found_something name
-          | _ => ())
+            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))
+          | _ => outcome)
       in
         (atp_problem_data,
          (output, run_time, facts, atp_problem, tstplike_proof, atp_proof, atp_abduce_candidates,