# HG changeset patch
# User hoelzl
# Date 1290762244 -3600
# Node ID 407c6122956fe4f9cfbf3b055a2c94831c0b9841
# Parent  e7aa34600c361ff4fcc6c9ef4b66b5992d56eab8# Parent  d1fc454d67357820e94f1ec58f25f9d89df3d40f
merged

diff -r d1fc454d6735 -r 407c6122956f doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Tue Nov 23 14:14:17 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Fri Nov 26 10:04:04 2010 +0100
@@ -10,7 +10,7 @@
 \usepackage{multicol}
 \usepackage{stmaryrd}
 %\usepackage[scaled=.85]{beramono}
-\usepackage{../iman,../pdfsetup}
+\usepackage{../isabelle,../iman,../pdfsetup}
 
 %\oddsidemargin=4.6mm
 %\evensidemargin=4.6mm
@@ -117,8 +117,9 @@
 arguments in the theory text.
 
 Nitpick requires the Kodkodi package for Isabelle as well as a Java 1.5 virtual
-machine called \texttt{java}. The examples presented in this manual can be found
-in Isabelle's \texttt{src/HOL/Nitpick\_Examples/Manual\_Nits.thy} theory.
+machine called \texttt{java}. To run Nitpick, you must also make sure that the
+theory \textit{Nitpick} is imported---this is rarely a problem in practice
+since it is part of \textit{Main}.
 
 Throughout this manual, we will explicitly invoke the \textbf{nitpick} command.
 Nitpick also provides an automatic mode that can be enabled via the ``Auto
@@ -129,6 +130,8 @@
 \newbox\boxA
 \setbox\boxA=\hbox{\texttt{nospam}}
 
+The examples presented in this manual can be found
+in Isabelle's \texttt{src/HOL/\allowbreak Nitpick\_Examples/Manual\_Nits.thy} theory.
 The known bugs and limitations at the time of writing are listed in
 \S\ref{known-bugs-and-limitations}. Comments and bug reports concerning Nitpick
 or this manual should be directed to
diff -r d1fc454d6735 -r 407c6122956f doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Tue Nov 23 14:14:17 2010 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Fri Nov 26 10:04:04 2010 +0100
@@ -10,7 +10,7 @@
 \usepackage{multicol}
 \usepackage{stmaryrd}
 %\usepackage[scaled=.85]{beramono}
-\usepackage{../iman,../pdfsetup}
+\usepackage{../isabelle,../iman,../pdfsetup}
 
 %\oddsidemargin=4.6mm
 %\evensidemargin=4.6mm
@@ -109,7 +109,9 @@
 \newbox\boxA
 \setbox\boxA=\hbox{\texttt{nospam}}
 
-Examples of Sledgehammer use can be found in Isabelle's
+To run Sledgehammer, you must make sure that the theory \textit{Sledgehammer} is
+imported---this is rarely a problem in practice since it is part of
+\textit{Main}. Examples of Sledgehammer use can be found in Isabelle's
 \texttt{src/HOL/Metis\_Examples} directory.
 Comments and bug reports concerning Sledgehammer or this manual should be
 directed to
diff -r d1fc454d6735 -r 407c6122956f src/HOL/Library/Ramsey.thy
--- a/src/HOL/Library/Ramsey.thy	Tue Nov 23 14:14:17 2010 +0100
+++ b/src/HOL/Library/Ramsey.thy	Fri Nov 26 10:04:04 2010 +0100
@@ -8,6 +8,113 @@
 imports Main Infinite_Set
 begin
 
+subsection{* Finite Ramsey theorem(s) *}
+
+text{* To distinguish the finite and infinite ones, lower and upper case
+names are used.
+
+This is the most basic version in terms of cliques and independent
+sets, i.e. the version for graphs and 2 colours. *}
+
+definition "clique V E = (\<forall>v\<in>V. \<forall>w\<in>V. v\<noteq>w \<longrightarrow> {v,w} : E)"
+definition "indep V E = (\<forall>v\<in>V. \<forall>w\<in>V. v\<noteq>w \<longrightarrow> \<not> {v,w} : E)"
+
+lemma ramsey2:
+  "\<exists>r\<ge>1. \<forall> (V::'a set) (E::'a set set). finite V \<and> card V \<ge> r \<longrightarrow>
+  (\<exists> R \<subseteq> V. card R = m \<and> clique R E \<or> card R = n \<and> indep R E)"
+  (is "\<exists>r\<ge>1. ?R m n r")
+proof(induct k == "m+n" arbitrary: m n)
+  case 0
+  show ?case (is "EX r. ?R r")
+  proof
+    show "?R 1" using 0
+      by (clarsimp simp: indep_def)(metis card.empty emptyE empty_subsetI)
+  qed
+next
+  case (Suc k)
+  { assume "m=0"
+    have ?case (is "EX r. ?R r")
+    proof
+      show "?R 1" using `m=0`
+        by (simp add:clique_def)(metis card.empty emptyE empty_subsetI)
+    qed
+  } moreover
+  { assume "n=0"
+    have ?case (is "EX r. ?R r")
+    proof
+      show "?R 1" using `n=0`
+        by (simp add:indep_def)(metis card.empty emptyE empty_subsetI)
+    qed
+  } moreover
+  { assume "m\<noteq>0" "n\<noteq>0"
+    hence "k = (m - 1) + n" "k = m + (n - 1)" using `Suc k = m+n` by auto
+    from Suc(1)[OF this(1)] Suc(1)[OF this(2)] 
+    obtain r1 r2 where "r1\<ge>1" "r2\<ge>1" "?R (m - 1) n r1" "?R m (n - 1) r2"
+      by auto
+    hence "r1+r2 \<ge> 1" by arith
+    moreover
+    have "?R m n (r1+r2)" (is "ALL V E. _ \<longrightarrow> ?EX V E m n")
+    proof clarify
+      fix V :: "'a set" and E :: "'a set set"
+      assume "finite V" "r1+r2 \<le> card V"
+      with `r1\<ge>1` have "V \<noteq> {}" by auto
+      then obtain v where "v : V" by blast
+      let ?M = "{w : V. w\<noteq>v & {v,w} : E}"
+      let ?N = "{w : V. w\<noteq>v & {v,w} ~: E}"
+      have "V = insert v (?M \<union> ?N)" using `v : V` by auto
+      hence "card V = card(insert v (?M \<union> ?N))" by metis
+      also have "\<dots> = card ?M + card ?N + 1" using `finite V`
+        by(fastsimp intro: card_Un_disjoint)
+      finally have "card V = card ?M + card ?N + 1" .
+      hence "r1+r2 \<le> card ?M + card ?N + 1" using `r1+r2 \<le> card V` by simp
+      hence "r1 \<le> card ?M \<or> r2 \<le> card ?N" by arith
+      moreover
+      { assume "r1 \<le> card ?M"
+        moreover have "finite ?M" using `finite V` by auto
+        ultimately have "?EX ?M E (m - 1) n" using `?R (m - 1) n r1` by blast
+        then obtain R where "R \<subseteq> ?M" "v ~: R" and
+          CI: "card R = m - 1 \<and> clique R E \<or>
+               card R = n \<and> indep R E" (is "?C \<or> ?I")
+          by blast
+        have "R <= V" using `R <= ?M` by auto
+        have "finite R" using `finite V` `R \<subseteq> V` by (metis finite_subset)
+        { assume "?I"
+          with `R <= V` have "?EX V E m n" by blast
+        } moreover
+        { assume "?C"
+          hence "clique (insert v R) E" using `R <= ?M`
+           by(auto simp:clique_def insert_commute)
+          moreover have "card(insert v R) = m"
+            using `?C` `finite R` `v ~: R` `m\<noteq>0` by simp
+          ultimately have "?EX V E m n" using `R <= V` `v : V` by blast
+        } ultimately have "?EX V E m n" using CI by blast
+      } moreover
+      { assume "r2 \<le> card ?N"
+        moreover have "finite ?N" using `finite V` by auto
+        ultimately have "?EX ?N E m (n - 1)" using `?R m (n - 1) r2` by blast
+        then obtain R where "R \<subseteq> ?N" "v ~: R" and
+          CI: "card R = m \<and> clique R E \<or>
+               card R = n - 1 \<and> indep R E" (is "?C \<or> ?I")
+          by blast
+        have "R <= V" using `R <= ?N` by auto
+        have "finite R" using `finite V` `R \<subseteq> V` by (metis finite_subset)
+        { assume "?C"
+          with `R <= V` have "?EX V E m n" by blast
+        } moreover
+        { assume "?I"
+          hence "indep (insert v R) E" using `R <= ?N`
+            by(auto simp:indep_def insert_commute)
+          moreover have "card(insert v R) = n"
+            using `?I` `finite R` `v ~: R` `n\<noteq>0` by simp
+          ultimately have "?EX V E m n" using `R <= V` `v : V` by blast
+        } ultimately have "?EX V E m n" using CI by blast
+      } ultimately show "?EX V E m n" by blast
+    qed
+    ultimately have ?case by blast
+  } ultimately show ?case by blast
+qed
+
+
 subsection {* Preliminaries *}
 
 subsubsection {* ``Axiom'' of Dependent Choice *}
diff -r d1fc454d6735 -r 407c6122956f src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Nov 23 14:14:17 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Nov 26 10:04:04 2010 +0100
@@ -526,12 +526,10 @@
       val (prover_name, _) = get_prover ctxt args
       val minimize = AList.defined (op =) args minimizeK
       val metis_ft = AList.defined (op =) args metis_ftK
-      val trivial = false
-(* FIXME
+      val trivial =
        TimeLimit.timeLimit try_outer_timeout
                                    (Try.invoke_try (SOME try_inner_timeout)) pre
                     handle TimeLimit.TimeOut => false
-*)
       fun apply_reconstructor m1 m2 =
         if metis_ft
         then
diff -r d1fc454d6735 -r 407c6122956f src/HOL/Nat_Numeral.thy
--- a/src/HOL/Nat_Numeral.thy	Tue Nov 23 14:14:17 2010 +0100
+++ b/src/HOL/Nat_Numeral.thy	Fri Nov 26 10:04:04 2010 +0100
@@ -674,7 +674,7 @@
 lemma nat_number_of_Pls: "Numeral0 = (0::nat)"
   by (simp add: nat_number_of_def)
 
-lemma nat_number_of_Min: "number_of Int.Min = (0::nat)"
+lemma nat_number_of_Min [no_atp]: "number_of Int.Min = (0::nat)"
   apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
   done
 
diff -r d1fc454d6735 -r 407c6122956f src/HOL/Quotient_Examples/FSet.thy
--- a/src/HOL/Quotient_Examples/FSet.thy	Tue Nov 23 14:14:17 2010 +0100
+++ b/src/HOL/Quotient_Examples/FSet.thy	Fri Nov 26 10:04:04 2010 +0100
@@ -25,7 +25,7 @@
   unfolding reflp_def symp_def transp_def
   by auto
 
-text {* Cset type *}
+text {* The @{text fset} type *}
 
 quotient_type
   'a fset = "'a list" / "list_eq"
diff -r d1fc454d6735 -r 407c6122956f src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Nov 23 14:14:17 2010 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Fri Nov 26 10:04:04 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 d1fc454d6735 -r 407c6122956f src/HOL/Tools/SMT/lib/scripts/remote_smt
--- a/src/HOL/Tools/SMT/lib/scripts/remote_smt	Tue Nov 23 14:14:17 2010 +0100
+++ b/src/HOL/Tools/SMT/lib/scripts/remote_smt	Fri Nov 26 10:04:04 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 d1fc454d6735 -r 407c6122956f src/HOL/Tools/SMT/smt_builtin.ML
--- a/src/HOL/Tools/SMT/smt_builtin.ML	Tue Nov 23 14:14:17 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_builtin.ML	Fri Nov 26 10:04:04 2010 +0100
@@ -9,8 +9,8 @@
 
 signature SMT_BUILTIN =
 sig
+  val is_builtin: Proof.context -> string * typ -> bool
   val is_partially_builtin: Proof.context -> string * typ -> bool
-  val is_builtin: Proof.context -> string * typ -> bool
 end
 
 structure SMT_Builtin: SMT_BUILTIN =
@@ -69,8 +69,8 @@
   (@{const_name HOL.eq}, K true),
 
   (* numerals *)
-  (@{const_name zero_class.zero}, is_arithT_dom),
-  (@{const_name one_class.one}, is_arithT_dom),
+  (@{const_name zero_class.zero}, is_arithT),
+  (@{const_name one_class.one}, is_arithT),
   (@{const_name Int.Pls}, K true),
   (@{const_name Int.Min}, K true),
   (@{const_name Int.Bit0}, K true),
@@ -109,8 +109,8 @@
     SOME proper_type => proper_type T
   | NONE => false)
 
-fun is_partially_builtin _ = lookup_builtin builtins
+fun is_builtin _ = lookup_builtin builtins
 
-fun is_builtin _ = lookup_builtin all_builtins
+fun is_partially_builtin _ = lookup_builtin all_builtins
 
 end
diff -r d1fc454d6735 -r 407c6122956f src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Tue Nov 23 14:14:17 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Nov 26 10:04:04 2010 +0100
@@ -35,6 +35,26 @@
 
 
 
+(* instantiate elimination rules *)
+ 
+local
+  val (cpfalse, cfalse) = `U.mk_cprop (Thm.cterm_of @{theory} @{const False})
+
+  fun inst f ct thm =
+    let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
+    in Thm.instantiate ([], [(cv, ct)]) thm end
+in
+
+fun instantiate_elim thm =
+  (case Thm.concl_of thm of
+    @{const Trueprop} $ Var (_, @{typ bool}) => inst Thm.dest_arg cfalse thm
+  | Var _ => inst I cpfalse thm
+  | _ => thm)
+
+end
+
+
+
 (* simplification of trivial distincts (distinct should have at least
    three elements in the argument list) *)
 
@@ -243,7 +263,7 @@
     | _ =>
         (case Term.strip_comb (Thm.term_of ct) of
           (Const (c as (_, T)), ts) =>
-            if SMT_Builtin.is_builtin ctxt c
+            if SMT_Builtin.is_partially_builtin ctxt c
             then eta_args_conv norm_conv
               (length (Term.binder_types T) - length ts)
             else args_conv o norm_conv
@@ -520,6 +540,7 @@
       else SOME (i, f ctxt' thm)
   in
     irules
+    |> map (apsnd instantiate_elim)
     |> trivial_distinct ctxt
     |> rewrite_bool_cases ctxt
     |> normalize_numerals ctxt
diff -r d1fc454d6735 -r 407c6122956f src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML	Tue Nov 23 14:14:17 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Fri Nov 26 10:04:04 2010 +0100
@@ -402,6 +402,9 @@
               | NONE => transs h T ts))
       | (h as Free (_, T), ts) => transs h T ts
       | (Bound i, []) => pair (SVar i)
+      | (Abs (_, _, t1 $ Bound 0), []) =>
+        if not (loose_bvar1 (t1, 0)) then trans t1 (* eta-reduce on the fly *)
+        else raise TERM ("smt_translate", [t])
       | _ => raise TERM ("smt_translate", [t]))
 
     and transs t T ts =
diff -r d1fc454d6735 -r 407c6122956f src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Nov 23 14:14:17 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Nov 26 10:04:04 2010 +0100
@@ -104,8 +104,9 @@
     else is_atp_installed thy name
   end
 
-val smt_default_max_relevant = 200 (* FUDGE *)
-val auto_max_relevant_divisor = 2 (* FUDGE *)
+(* FUDGE *)
+val smt_default_max_relevant = 225
+val auto_max_relevant_divisor = 2
 
 fun default_max_relevant_for_prover thy name =
   if is_smt_prover name then smt_default_max_relevant
@@ -412,19 +413,27 @@
 (* "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
 
+(* FUDGE *)
 val smt_max_iter = 8
 val smt_iter_fact_divisor = 2
 val smt_iter_min_msecs = 5000
@@ -475,9 +484,9 @@
           | SOME (SMT_Failure.Abnormal_Termination code) =>
             (if verbose then
                "The SMT solver invoked with " ^ string_of_int num_facts ^
-               " fact" ^ plural_s num_facts ^ " terminated abnormally with exit\
-               \code " ^ string_of_int code ^ "."
-               |> (if debug then error else warning)
+               " fact" ^ plural_s num_facts ^ " terminated abnormally with \
+               \exit code " ^ string_of_int code ^ "."
+               |> warning
              else
                ();
              true (* kind of *))
@@ -509,19 +518,18 @@
 
 val smt_metis_timeout = seconds 0.5
 
-fun can_apply_metis state i ths =
-  can_apply smt_metis_timeout (fn ctxt => Metis_Tactics.metis_tac ctxt ths)
-            state i
+fun can_apply_metis debug state i ths =
+  can_apply smt_metis_timeout
+            (Config.put Metis_Tactics.verbose debug
+             #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i
 
 fun run_smt_solver auto remote (params as {debug, ...}) minimize_command
         ({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
   let
     val repair_context =
-      Config.put Metis_Tactics.verbose debug
-      #> Config.put SMT_Config.verbose debug
+      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} =
@@ -532,8 +540,10 @@
         NONE =>
         let
           val method =
-            if can_apply_metis state subgoal (map snd used_facts) then "metis"
-            else "smt"
+            if can_apply_metis debug state subgoal (map snd used_facts) then
+              "metis"
+            else
+              "smt"
         in
           try_command_line (proof_banner auto)
                            (apply_on_subgoal subgoal subgoal_count ^
diff -r d1fc454d6735 -r 407c6122956f src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Tue Nov 23 14:14:17 2010 +0100
+++ b/src/Pure/Concurrent/par_list.ML	Fri Nov 26 10:04:04 2010 +0100
@@ -26,20 +26,26 @@
 structure Par_List: PAR_LIST =
 struct
 
-fun raw_map f xs =
+fun managed_results f xs =
   if Multithreading.enabled () andalso not (Multithreading.self_critical ()) then
-    let val shared_group = Task_Queue.new_group (Future.worker_group ())
-    in Future.join_results (map (fn x => Future.fork_group shared_group (fn () => f x)) xs) end
+    let
+      val shared_group = Task_Queue.new_group (Future.worker_group ());
+      val results =
+        Future.join_results (map (fn x => Future.fork_group shared_group (fn () => f x)) xs)
+          handle exn =>
+            (if Exn.is_interrupt exn then Future.cancel_group shared_group else (); reraise exn);
+    in results end
   else map (Exn.capture f) xs;
 
-fun map f xs = Exn.release_first (raw_map f xs);
+fun map f xs = Exn.release_first (managed_results f xs);
 
 fun get_some f xs =
   let
     exception FOUND of 'b option;
     fun found (Exn.Exn (FOUND some)) = some
       | found _ = NONE;
-    val results = raw_map (fn x => (case f x of NONE => () | some => raise FOUND some)) xs;
+    val results =
+      managed_results (fn x => (case f x of NONE => () | some => raise FOUND some)) xs;
   in
     (case get_first found results of
       SOME y => SOME y