# HG changeset patch
# User blanchet
# Date 1305888478 -7200
# Node ID e336ef6313aa1e4921c4cdc328445b8e03a9357d
# Parent  d1aad0957eb2360ab16c30f617f6d7cc6b9715a7
more informative message when Sledgehammer finds an unsound proof

diff -r d1aad0957eb2 -r e336ef6313aa src/HOL/Tools/ATP/atp_proof.ML
--- 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."
diff -r d1aad0957eb2 -r e336ef6313aa src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
--- 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 **)
 
diff -r d1aad0957eb2 -r e336ef6313aa src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- 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