--- 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
--- 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
--- 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 *}
--- 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
--- 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
--- 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"
--- 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."
--- 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; }
--- 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
--- 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
--- 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 =
--- 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 ^
--- 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