--- a/src/HOL/Tools/ATP/atp_proof.ML Fri May 20 12:35:44 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Fri May 20 12:47:58 2011 +0200
@@ -3,7 +3,7 @@
Author: Claire Quigley, Cambridge University Computer Laboratory
Author: Jasmin Blanchette, TU Muenchen
-Abstract representation of ATP proofs and TSTP/Vampire/SPASS syntax.
+Abstract representation of ATP proofs and TSTP/SPASS syntax.
*)
signature ATP_PROOF =
@@ -15,7 +15,7 @@
Unprovable |
IncompleteUnprovable |
ProofMissing |
- UnsoundProof of bool |
+ UnsoundProof of bool * string list |
CantConnect |
TimedOut |
OutOfResources |
@@ -64,7 +64,7 @@
Unprovable |
IncompleteUnprovable |
ProofMissing |
- UnsoundProof of bool |
+ UnsoundProof of bool * string list |
CantConnect |
TimedOut |
OutOfResources |
@@ -117,20 +117,24 @@
" appears to be missing. You will need to install it if you want to invoke \
\remote provers."
+fun involving [] = ""
+ | involving ss = "involving " ^ commas_quote ss ^ " "
+
fun string_for_failure Unprovable =
"The problem is unprovable."
| string_for_failure IncompleteUnprovable =
"The prover gave up."
| string_for_failure ProofMissing =
"The prover claims the conjecture is a theorem but did not provide a proof."
- | string_for_failure (UnsoundProof false) =
- "The prover found a type-unsound proof (or, very unlikely, your axioms \
- \are inconsistent). Try passing the \"full_types\" option to Sledgehammer \
- \to avoid such spurious proofs."
- | string_for_failure (UnsoundProof true) =
- "The prover found a type-unsound proof even though a supposedly type-sound \
- \encoding was used (or, very unlikely, your axioms are inconsistent). You \
- \might want to report this to the Isabelle developers."
+ | string_for_failure (UnsoundProof (false, ss)) =
+ "The prover found a type-unsound proof " ^ involving ss ^
+ "(or, less likely, your axioms are inconsistent). Try passing the \
+ \\"full_types\" option to Sledgehammer to avoid such spurious proofs."
+ | string_for_failure (UnsoundProof (true, ss)) =
+ "The prover found a type-unsound proof " ^ involving ss ^
+ "even though a supposedly type-sound encoding was used (or, less likely, \
+ \your axioms are inconsistent). You might want to report this to the \
+ \Isabelle developers."
| string_for_failure CantConnect = "Cannot connect to remote server."
| string_for_failure TimedOut = "Timed out."
| string_for_failure OutOfResources = "The prover ran out of resources."
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri May 20 12:35:44 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri May 20 12:47:58 2011 +0200
@@ -27,9 +27,9 @@
val used_facts_in_atp_proof :
type_system -> int -> (string * locality) list vector -> string proof
-> (string * locality) list
- val is_unsound_proof :
+ val used_facts_in_unsound_atp_proof :
type_system -> int list list -> int -> (string * locality) list vector
- -> string proof -> bool
+ -> string proof -> string list option
val apply_on_subgoal : string -> int -> int -> string
val command_call : string -> string list -> string
val try_command_line : string -> string -> string
@@ -181,10 +181,18 @@
exists (fn Inference (name, _, []) => is_conjecture conjecture_shape name
| _ => false)
-fun is_unsound_proof type_sys conjecture_shape facts_offset fact_names =
- not o is_conjecture_referred_to_in_proof conjecture_shape andf
- forall (is_locality_global o snd)
- o used_facts_in_atp_proof type_sys facts_offset fact_names
+fun used_facts_in_unsound_atp_proof type_sys conjecture_shape facts_offset
+ fact_names atp_proof =
+ let
+ val used_facts = used_facts_in_atp_proof type_sys facts_offset fact_names
+ atp_proof
+ in
+ if forall (is_locality_global o snd) used_facts andalso
+ not (is_conjecture_referred_to_in_proof conjecture_shape atp_proof) then
+ SOME (map fst used_facts)
+ else
+ NONE
+ end
(** Soft-core proof reconstruction: Metis one-liner **)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 20 12:35:44 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 20 12:47:58 2011 +0200
@@ -577,11 +577,11 @@
val outcome =
case outcome of
NONE =>
- if is_unsound_proof type_sys conjecture_shape facts_offset
- fact_names atp_proof then
- SOME (UnsoundProof (is_type_sys_virtually_sound type_sys))
- else
- NONE
+ used_facts_in_unsound_atp_proof type_sys
+ conjecture_shape facts_offset fact_names atp_proof
+ |> Option.map (fn facts =>
+ UnsoundProof (is_type_sys_virtually_sound type_sys,
+ facts))
| SOME Unprovable =>
if null blacklist then outcome
else SOME IncompleteUnprovable
@@ -609,7 +609,7 @@
fun maybe_blacklist_facts_and_retry iter blacklist
(result as ((_, _, facts_offset, fact_names, _),
(_, _, type_sys, atp_proof,
- SOME (UnsoundProof false)))) =
+ SOME (UnsoundProof (false, _))))) =
(case used_facts_in_atp_proof type_sys facts_offset fact_names
atp_proof of
[] => result