--- 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"
--- 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) *)
--- 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)
--- 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,