--- 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) *)
--- 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 =
--- 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 =