# HG changeset patch
# User boehmes
# Date 1290613873 -3600
# Node ID 1aa56a048dce7eb31fee7837f94da84e84a19a04
# Parent  4725ed462387d898a47494053f0f0136962697f4# Parent  c7ba327eb58cffd7d3a045f2660159780c916f2a
merged

diff -r 4725ed462387 -r 1aa56a048dce src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Wed Nov 24 15:33:35 2010 +0100
+++ b/src/HOL/Enum.thy	Wed Nov 24 16:51:13 2010 +0100
@@ -19,7 +19,7 @@
 
 lemma enum_all: "set enum = UNIV" unfolding UNIV_enum ..
 
-lemma in_enum [intro]: "x \<in> set enum"
+lemma in_enum: "x \<in> set enum"
   unfolding enum_all by auto
 
 lemma enum_eq_I:
@@ -167,9 +167,9 @@
   proof (rule UNIV_eq_I)
     fix f :: "'a \<Rightarrow> 'b"
     have "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))"
-      by (auto simp add: map_of_zip_map fun_eq_iff)
+      by (auto simp add: map_of_zip_map fun_eq_iff intro: in_enum)
     then show "f \<in> set enum"
-      by (auto simp add: enum_fun_def set_n_lists)
+      by (auto simp add: enum_fun_def set_n_lists intro: in_enum)
   qed
 next
   from map_of_zip_enum_inject
diff -r 4725ed462387 -r 1aa56a048dce src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Nov 24 15:33:35 2010 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Nov 24 16:51:13 2010 +0100
@@ -71,9 +71,9 @@
 fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
 val strip_spaces_except_between_ident_chars = strip_spaces is_ident_char
 
-val missing_message_tail =
-  " appears to be missing. You will need to install it if you want to run \
-  \ATPs remotely."
+fun missing_message_tail prover =
+  " appears to be missing. You will need to install it if you want to run " ^
+  prover ^ "s remotely."
 
 fun string_for_failure prover Unprovable =
     "The " ^ prover ^ " problem is unprovable."
@@ -96,9 +96,9 @@
     "Isabelle requires a more recent version of Vampire. To install it, follow \
     \the instructions from the Sledgehammer manual (\"isabelle doc\
     \ sledgehammer\")."
-  | string_for_failure _ NoPerl = "Perl" ^ missing_message_tail
-  | string_for_failure _ NoLibwwwPerl =
-    "The Perl module \"libwww-perl\"" ^ missing_message_tail
+  | string_for_failure prover NoPerl = "Perl" ^ missing_message_tail prover
+  | string_for_failure prover NoLibwwwPerl =
+    "The Perl module \"libwww-perl\"" ^ missing_message_tail prover
   | string_for_failure prover MalformedInput =
     "The " ^ prover ^ " problem is malformed. Please report this to the Isabelle \
     \developers."
diff -r 4725ed462387 -r 1aa56a048dce src/HOL/Tools/SMT/lib/scripts/remote_smt
--- a/src/HOL/Tools/SMT/lib/scripts/remote_smt	Wed Nov 24 15:33:35 2010 +0100
+++ b/src/HOL/Tools/SMT/lib/scripts/remote_smt	Wed Nov 24 16:51:13 2010 +0100
@@ -26,6 +26,6 @@
   "Options" => join(" ", @options),
   "Problem" => [$problem_file] ],
   "Content_Type" => "form-data");
-if (not $response->is_success) { die "HTTP-Error: " . $response->message; }
+if (not $response->is_success) { die "HTTP error: " . $response->message; }
 else { print $response->content; }
 
diff -r 4725ed462387 -r 1aa56a048dce src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Nov 24 15:33:35 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Nov 24 16:51:13 2010 +0100
@@ -412,16 +412,23 @@
 (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until
    these are sorted out properly in the SMT module, we have to interpret these
    ourselves. *)
-
-val z3_malformed_input_codes = [103, 110]
-val sigsegv_code = 139
+val remote_smt_failures =
+  [(22, CantConnect),
+   (127, NoPerl),
+   (2, NoLibwwwPerl)]
+val z3_failures =
+  [(103, MalformedInput),
+   (110, MalformedInput)]
+val unix_failures =
+  [(139, Crashed)]
+val smt_failures = remote_smt_failures @ z3_failures @ unix_failures
 
 fun failure_from_smt_failure (SMT_Failure.Counterexample _) = Unprovable
   | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
   | failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) =
-    if member (op =) z3_malformed_input_codes code then MalformedInput
-    else if code = sigsegv_code then Crashed
-    else IncompleteUnprovable
+    (case AList.lookup (op =) smt_failures code of
+       SOME failure => failure
+     | NONE => UnknownError)
   | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
   | failure_from_smt_failure _ = UnknownError
 
@@ -521,7 +528,6 @@
       #> Config.put SMT_Config.verbose debug
       #> Config.put SMT_Config.monomorph_limit smt_monomorph_limit
     val state = state |> Proof.map_context repair_context
-    val ctxt = Proof.context_of state
     val thy = Proof.theory_of state
     val smt_fact = Option.map (apsnd (Thm.transfer thy)) o try dest_Untranslated
     val {outcome, used_facts, run_time_in_msecs} =