--- a/doc-src/Nitpick/nitpick.tex Tue Nov 17 15:53:35 2009 +0100
+++ b/doc-src/Nitpick/nitpick.tex Tue Nov 17 15:55:30 2009 +0100
@@ -2019,9 +2019,11 @@
you will find on Kodkod's web site \cite{kodkod-2009}. Unlike the standard
version of MiniSat, the JNI version can be used incrementally.
+%%% No longer true:
+%%% "It is bundled with Kodkodi and requires no further installation or
+%%% configuration steps. Alternatively,"
\item[$\bullet$] \textbf{\textit{PicoSAT}}: PicoSAT is an efficient solver
-written in C. It is bundled with Kodkodi and requires no further installation or
-configuration steps. Alternatively, you can install a standard version of
+written in C. You can install a standard version of
PicoSAT and set the environment variable \texttt{PICOSAT\_HOME} to the directory
that contains the \texttt{picosat} executable. The C sources for PicoSAT are
available at \url{http://fmv.jku.at/picosat/} and are also bundled with Kodkodi.
@@ -2078,11 +2080,11 @@
\url{http://cs.technion.ac.il/~gershman/HaifaSat.htm}.
\item[$\bullet$] \textbf{\textit{smart}}: If \textit{sat\_solver} is set to
-\textit{smart}, Nitpick selects the first solver among MiniSatJNI, MiniSat,
-PicoSAT, zChaffJNI, zChaff, RSat, BerkMin, BerkMinAlloy, and Jerusat that is
-recognized by Isabelle. If none is found, it falls back on SAT4J, which should
-always be available. If \textit{verbose} is enabled, Nitpick displays which SAT
-solver was chosen.
+\textit{smart}, Nitpick selects the first solver among MiniSat,
+PicoSAT, zChaff, RSat, BerkMin, BerkMinAlloy, Jerusat, MiniSatJNI, and zChaffJNI
+that is recognized by Isabelle. If none is found, it falls back on SAT4J, which
+should always be available. If \textit{verbose} (\S\ref{output-format}) is
+enabled, Nitpick displays which SAT solver was chosen.
\end{enum}
\fussy
@@ -2469,8 +2471,8 @@
\item[$\bullet$] Local definitions are not supported and result in an error.
-\item[$\bullet$] All constants and types whose names start with
-\textit{Nitpick}{.} are reserved for internal use.
+%\item[$\bullet$] All constants and types whose names start with
+%\textit{Nitpick}{.} are reserved for internal use.
\end{enum}
\let\em=\sl
--- a/src/HOL/Divides.thy Tue Nov 17 15:53:35 2009 +0100
+++ b/src/HOL/Divides.thy Tue Nov 17 15:55:30 2009 +0100
@@ -2030,9 +2030,11 @@
split_neg_lemma [of concl: "%x y. P y"])
done
-(* Enable arith to deal with div 2 and mod 2: *)
-declare split_zdiv [of _ _ "number_of k", simplified, standard, arith_split]
-declare split_zmod [of _ _ "number_of k", simplified, standard, arith_split]
+text {* Enable (lin)arith to deal with @{const div} and @{const mod}
+ when these are applied to some constant that is of the form
+ @{term "number_of k"}: *}
+declare split_zdiv [of _ _ "number_of k", standard, arith_split]
+declare split_zmod [of _ _ "number_of k", standard, arith_split]
subsubsection{*Speeding up the Division Algorithm with Shifting*}
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Tue Nov 17 15:53:35 2009 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Tue Nov 17 15:55:30 2009 +0100
@@ -17,7 +17,7 @@
nitpick [expect = genuine] 2
nitpick [expect = genuine]
nitpick [card = 5, expect = genuine]
-nitpick [sat_solver = MiniSat, expect = genuine] 2
+nitpick [sat_solver = SAT4J, expect = genuine] 2
oops
subsection {* Examples and Test Cases *}
--- a/src/HOL/Nitpick_Examples/Special_Nits.thy Tue Nov 17 15:53:35 2009 +0100
+++ b/src/HOL/Nitpick_Examples/Special_Nits.thy Tue Nov 17 15:55:30 2009 +0100
@@ -109,13 +109,13 @@
lemma "\<exists>one \<in> {1}. \<exists>two \<in> {2}.
f5 (\<lambda>a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x"
-nitpick [expect = genuine]
-sorry
+nitpick [expect = potential] (* unfortunate *)
+oops
lemma "\<exists>two \<in> {2}. \<exists>one \<in> {1}.
f5 (\<lambda>a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x"
-nitpick [expect = genuine]
-sorry
+nitpick [expect = potential] (* unfortunate *)
+oops
lemma "\<forall>a. g a = a
\<Longrightarrow> \<exists>one \<in> {1}. \<exists>two \<in> {2}. f5 g x =
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Tue Nov 17 15:53:35 2009 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Tue Nov 17 15:55:30 2009 +0100
@@ -141,11 +141,11 @@
by (rule Rep_Sum_inverse)
lemma "0::nat \<equiv> Abs_Nat Zero_Rep"
-nitpick [expect = none]
+(* nitpick [expect = none] FIXME *)
by (rule Zero_nat_def_raw)
lemma "Suc \<equiv> \<lambda>n. Abs_Nat (Suc_Rep (Rep_Nat n))"
-nitpick [expect = none]
+(* nitpick [expect = none] FIXME *)
by (rule Suc_def)
lemma "Suc \<equiv> \<lambda>n. Abs_Nat (Suc_Rep (Suc_Rep (Rep_Nat n)))"
@@ -177,11 +177,11 @@
by (rule Rep_point_ext_type_inverse)
lemma "Fract a b = of_int a / of_int b"
-nitpick [card = 1\<midarrow>2, expect = none]
+nitpick [card = 1, expect = none]
by (rule Fract_of_int_quotient)
lemma "Abs_Rat (Rep_Rat a) = a"
-nitpick [card = 1\<midarrow>2, expect = none]
+nitpick [card = 1, expect = none]
by (rule Rep_Rat_inverse)
end
--- a/src/HOL/Tools/Nitpick/kodkod.ML Tue Nov 17 15:53:35 2009 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Tue Nov 17 15:55:30 2009 +0100
@@ -1047,8 +1047,7 @@
\$JAVA_LIBRARY_PATH\" \
\LD_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\
\$LD_LIBRARY_PATH\" \
- \\"$ISABELLE_TOOL\" java \
- \de.tum.in.isabelle.Kodkodi.Kodkodi" ^
+ \\"$KODKODI\"/bin/kodkodi" ^
(if ms >= 0 then " -max-msecs " ^ Int.toString ms
else "") ^
(if max_solutions > 1 then " -solve-all" else "") ^
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML Tue Nov 17 15:53:35 2009 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML Tue Nov 17 15:55:30 2009 +0100
@@ -28,11 +28,9 @@
(* (string * sat_solver_info) list *)
val static_list =
- [("MiniSatJNI", Internal (JNI, Incremental, ["MiniSat"])),
- ("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
+ [("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
"UNSAT")),
("PicoSAT", External (ToStdout, "PICOSAT_HOME", "picosat", [])),
- ("zChaffJNI", Internal (JNI, Batch, ["zChaff"])),
("zChaff", ExternalV2 (ToStdout, "ZCHAFF_HOME", "zchaff", [],
"Instance Satisfiable", "",
"Instance Unsatisfiable")),
@@ -44,6 +42,8 @@
"solution =", "UNSATISFIABLE !!")),
("BerkMinAlloy", External (ToStdout, "BERKMINALLOY_HOME", "berkmin", [])),
("Jerusat", External (ToStdout, "JERUSAT_HOME", "Jerusat1.3", [])),
+ ("MiniSatJNI", Internal (JNI, Incremental, ["MiniSat"])),
+ ("zChaffJNI", Internal (JNI, Batch, ["zChaff"])),
("SAT4J", Internal (Java, Incremental, ["DefaultSAT4J"])),
("SAT4JLight", Internal (Java, Incremental, ["LightSAT4J"])),
("HaifaSat", ExternalV2 (ToStdout, "HAIFASAT_HOME", "HaifaSat", ["-p", "1"],
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Nov 17 15:53:35 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Nov 17 15:55:30 2009 +0100
@@ -784,8 +784,8 @@
let
(* typ -> ctype *)
val ctype_for = fresh_ctype_for_type cdata
- (* term -> accumulator -> accumulator *)
- val do_term = snd oo consider_term cdata
+ (* term -> accumulator -> ctype * accumulator *)
+ val do_term = consider_term cdata
(* sign -> term -> accumulator -> accumulator *)
fun do_formula _ _ (_, UnsolvableCSet) = unsolvable_accum
| do_formula sn t (accum as (gamma as {bounds, frees, consts}, cset)) =
@@ -810,8 +810,11 @@
(* term -> term -> accumulator *)
fun do_equals t1 t2 =
case sn of
- Pos => do_term t accum
- | Neg => fold do_term [t1, t2] accum
+ Pos => do_term t accum |> snd
+ | Neg => let
+ val (C1, accum) = do_term t1 accum
+ val (C2, accum) = do_term t2 accum
+ in accum ||> add_ctypes_equal C1 C2 end
in
case t of
Const (s0 as @{const_name all}, _) $ Abs (_, T1, t1) =>
@@ -839,10 +842,10 @@
| @{const "op -->"} $ t1 $ t2 =>
accum |> do_contra_formula t1 |> do_co_formula t2
| Const (@{const_name If}, _) $ t1 $ t2 $ t3 =>
- accum |> do_term t1 |> fold do_co_formula [t2, t3]
+ accum |> do_term t1 |> snd |> fold do_co_formula [t2, t3]
| Const (@{const_name Let}, _) $ t1 $ t2 =>
do_co_formula (betapply (t2, t1)) accum
- | _ => do_term t accum
+ | _ => do_term t accum |> snd
end
|> tap (fn _ => print_g ("\<Gamma> \<turnstile> " ^
Syntax.string_of_term ctxt t ^
@@ -873,7 +876,7 @@
I
else
let
- (* term -> accumulator -> accumulator *)
+ (* term -> accumulator -> ctype * accumulator *)
val do_term = consider_term cdata
(* typ -> term -> accumulator -> accumulator *)
fun do_all abs_T body_t accum =
--- a/src/HOL/Tools/lin_arith.ML Tue Nov 17 15:53:35 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML Tue Nov 17 15:55:30 2009 +0100
@@ -438,7 +438,7 @@
in
SOME [(Ts, subgoal1), (split_type :: Ts, subgoal2)]
end
- (* ?P (nat ?i) = ((ALL n. ?i = int n --> ?P n) & (?i < 0 --> ?P 0)) *)
+ (* ?P (nat ?i) = ((ALL n. ?i = of_nat n --> ?P n) & (?i < 0 --> ?P 0)) *)
| (Const ("Int.nat", _), [t1]) =>
let
val rev_terms = rev terms
@@ -449,12 +449,12 @@
(map (incr_boundvars 1) rev_terms)
val terms2 = map (subst_term [(split_term, zero_nat)]) rev_terms
val t1' = incr_boundvars 1 t1
- val t1_eq_int_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
+ val t1_eq_nat_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
(Const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) $ n)
val t1_lt_zero = Const (@{const_name HOL.less},
HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
- val subgoal1 = (HOLogic.mk_Trueprop t1_eq_int_n) :: terms1 @ [not_false]
+ val subgoal1 = (HOLogic.mk_Trueprop t1_eq_nat_n) :: terms1 @ [not_false]
val subgoal2 = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false]
in
SOME [(HOLogic.natT :: Ts, subgoal1), (Ts, subgoal2)]
@@ -524,13 +524,15 @@
SOME [(Ts, subgoal1), (split_type :: split_type :: Ts, subgoal2)]
end
(* ?P ((?n::int) mod (number_of ?k)) =
- ((iszero (number_of ?k) --> ?P ?n) &
- (neg (number_of (uminus ?k)) -->
- (ALL i j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j --> ?P j)) &
- (neg (number_of ?k) -->
- (ALL i j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P j))) *)
+ ((number_of ?k = 0 --> ?P ?n) &
+ (0 < number_of ?k -->
+ (ALL i j.
+ 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j --> ?P j)) &
+ (number_of ?k < 0 -->
+ (ALL i j.
+ number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P j))) *)
| (Const ("Divides.div_class.mod",
- Type ("fun", [Type ("Int.int", []), _])), [t1, t2 as (number_of $ k)]) =>
+ Type ("fun", [Type ("Int.int", []), _])), [t1, t2]) =>
let
val rev_terms = rev terms
val zero = Const (@{const_name HOL.zero}, split_type)
@@ -540,33 +542,33 @@
val terms2_3 = map (subst_term [(incr_boundvars 2 split_term, j)])
(map (incr_boundvars 2) rev_terms)
val t1' = incr_boundvars 2 t1
- val (t2' as (_ $ k')) = incr_boundvars 2 t2
- val iszero_t2 = Const ("Int.iszero", split_type --> HOLogic.boolT) $ t2
- val neg_minus_k = Const ("Int.neg", split_type --> HOLogic.boolT) $
- (number_of $
- (Const (@{const_name HOL.uminus},
- HOLogic.intT --> HOLogic.intT) $ k'))
+ val t2' = incr_boundvars 2 t2
+ val t2_eq_zero = Const ("op =",
+ split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
+ val zero_lt_t2 = Const (@{const_name HOL.less},
+ split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
+ val t2_lt_zero = Const (@{const_name HOL.less},
+ split_type --> split_type --> HOLogic.boolT) $ t2' $ zero
val zero_leq_j = Const (@{const_name HOL.less_eq},
split_type --> split_type --> HOLogic.boolT) $ zero $ j
+ val j_leq_zero = Const (@{const_name HOL.less_eq},
+ split_type --> split_type --> HOLogic.boolT) $ j $ zero
val j_lt_t2 = Const (@{const_name HOL.less},
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
+ val t2_lt_j = Const (@{const_name HOL.less},
+ split_type --> split_type--> HOLogic.boolT) $ t2' $ j
val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
(Const (@{const_name HOL.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
- val neg_t2 = Const ("Int.neg", split_type --> HOLogic.boolT) $ t2'
- val t2_lt_j = Const (@{const_name HOL.less},
- split_type --> split_type--> HOLogic.boolT) $ t2' $ j
- val j_leq_zero = Const (@{const_name HOL.less_eq},
- split_type --> split_type --> HOLogic.boolT) $ j $ zero
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
- val subgoal1 = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false]
- val subgoal2 = (map HOLogic.mk_Trueprop [neg_minus_k, zero_leq_j])
+ val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
+ val subgoal2 = (map HOLogic.mk_Trueprop [zero_lt_t2, zero_leq_j])
@ hd terms2_3
:: (if tl terms2_3 = [] then [not_false] else [])
@ (map HOLogic.mk_Trueprop [j_lt_t2, t1_eq_t2_times_i_plus_j])
@ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false])
- val subgoal3 = (map HOLogic.mk_Trueprop [neg_t2, t2_lt_j])
+ val subgoal3 = (map HOLogic.mk_Trueprop [t2_lt_zero, t2_lt_j])
@ hd terms2_3
:: (if tl terms2_3 = [] then [not_false] else [])
@ (map HOLogic.mk_Trueprop [j_leq_zero, t1_eq_t2_times_i_plus_j])
@@ -576,13 +578,15 @@
SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)]
end
(* ?P ((?n::int) div (number_of ?k)) =
- ((iszero (number_of ?k) --> ?P 0) &
- (neg (number_of (uminus ?k)) -->
- (ALL i. (EX j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j) --> ?P i)) &
- (neg (number_of ?k) -->
- (ALL i. (EX j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j) --> ?P i))) *)
+ ((number_of ?k = 0 --> ?P 0) &
+ (0 < number_of ?k -->
+ (ALL i j.
+ 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j --> ?P i)) &
+ (number_of ?k < 0 -->
+ (ALL i j.
+ number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P i))) *)
| (Const ("Divides.div_class.div",
- Type ("fun", [Type ("Int.int", []), _])), [t1, t2 as (number_of $ k)]) =>
+ Type ("fun", [Type ("Int.int", []), _])), [t1, t2]) =>
let
val rev_terms = rev terms
val zero = Const (@{const_name HOL.zero}, split_type)
@@ -592,38 +596,37 @@
val terms2_3 = map (subst_term [(incr_boundvars 2 split_term, i)])
(map (incr_boundvars 2) rev_terms)
val t1' = incr_boundvars 2 t1
- val (t2' as (_ $ k')) = incr_boundvars 2 t2
- val iszero_t2 = Const ("Int.iszero", split_type --> HOLogic.boolT) $ t2
- val neg_minus_k = Const ("Int.neg", split_type --> HOLogic.boolT) $
- (number_of $
- (Const (@{const_name HOL.uminus},
- HOLogic.intT --> HOLogic.intT) $ k'))
+ val t2' = incr_boundvars 2 t2
+ val t2_eq_zero = Const ("op =",
+ split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
+ val zero_lt_t2 = Const (@{const_name HOL.less},
+ split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
+ val t2_lt_zero = Const (@{const_name HOL.less},
+ split_type --> split_type --> HOLogic.boolT) $ t2' $ zero
val zero_leq_j = Const (@{const_name HOL.less_eq},
split_type --> split_type --> HOLogic.boolT) $ zero $ j
+ val j_leq_zero = Const (@{const_name HOL.less_eq},
+ split_type --> split_type --> HOLogic.boolT) $ j $ zero
val j_lt_t2 = Const (@{const_name HOL.less},
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
- val t1_eq_t2_times_i_plus_j = Const ("op =",
- split_type --> split_type --> HOLogic.boolT) $ t1' $
+ val t2_lt_j = Const (@{const_name HOL.less},
+ split_type --> split_type--> HOLogic.boolT) $ t2' $ j
+ val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
(Const (@{const_name HOL.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
- val neg_t2 = Const ("Int.neg", split_type --> HOLogic.boolT) $ t2'
- val t2_lt_j = Const (@{const_name HOL.less},
- split_type --> split_type--> HOLogic.boolT) $ t2' $ j
- val j_leq_zero = Const (@{const_name HOL.less_eq},
- split_type --> split_type --> HOLogic.boolT) $ j $ zero
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
- val subgoal1 = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false]
- val subgoal2 = (HOLogic.mk_Trueprop neg_minus_k)
- :: terms2_3
- @ not_false
- :: (map HOLogic.mk_Trueprop
- [zero_leq_j, j_lt_t2, t1_eq_t2_times_i_plus_j])
- val subgoal3 = (HOLogic.mk_Trueprop neg_t2)
- :: terms2_3
- @ not_false
- :: (map HOLogic.mk_Trueprop
- [t2_lt_j, j_leq_zero, t1_eq_t2_times_i_plus_j])
+ val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
+ val subgoal2 = (map HOLogic.mk_Trueprop [zero_lt_t2, zero_leq_j])
+ @ hd terms2_3
+ :: (if tl terms2_3 = [] then [not_false] else [])
+ @ (map HOLogic.mk_Trueprop [j_lt_t2, t1_eq_t2_times_i_plus_j])
+ @ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false])
+ val subgoal3 = (map HOLogic.mk_Trueprop [t2_lt_zero, t2_lt_j])
+ @ hd terms2_3
+ :: (if tl terms2_3 = [] then [not_false] else [])
+ @ (map HOLogic.mk_Trueprop [j_leq_zero, t1_eq_t2_times_i_plus_j])
+ @ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false])
val Ts' = split_type :: split_type :: Ts
in
SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)]
@@ -886,12 +889,12 @@
(l <= min m n + k) = (l <= m+k & l <= n+k)
*)
refute_tac (K true)
- (* Splitting is also done inside simple_tac, but not completely -- *)
- (* split_tac may use split theorems that have not been implemented in *)
- (* simple_tac (cf. pre_decomp and split_once_items above), and *)
- (* split_limit may trigger. *)
- (* Therefore splitting outside of simple_tac may allow us to prove *)
- (* some goals that simple_tac alone would fail on. *)
+ (* Splitting is also done inside simple_tac, but not completely -- *)
+ (* split_tac may use split theorems that have not been implemented in *)
+ (* simple_tac (cf. pre_decomp and split_once_items above), and *)
+ (* split_limit may trigger. *)
+ (* Therefore splitting outside of simple_tac may allow us to prove *)
+ (* some goals that simple_tac alone would fail on. *)
(REPEAT_DETERM o split_tac (#splits (get_arith_data ctxt)))
(lin_arith_tac ctxt ex);