--- a/doc-src/Nitpick/nitpick.tex Tue Feb 23 11:05:32 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex Tue Feb 23 12:14:29 2010 +0100
@@ -154,7 +154,7 @@
15~seconds (instead of 30~seconds). This was done by adding the line
\prew
-\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1, \,\,\textit{timeout} = 15$\,s$]
+\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1, \,\textit{timeout} = 15$\,s$]
\postw
after the \textbf{begin} keyword. The JNI version of MiniSat is bundled with
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Feb 23 11:05:32 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Feb 23 12:14:29 2010 +0100
@@ -149,7 +149,7 @@
"\<lbrakk>even' m; even' n\<rbrakk> \<Longrightarrow> even' (m + n)"
lemma "\<exists>n \<in> {0, 2, 4, 6, 8}. \<not> even' n"
-nitpick [card nat = 10, unary_ints, verbose, show_consts] (* FIXME: should be genuine *)
+nitpick [card nat = 10, unary_ints, verbose, show_consts]
oops
lemma "even' (n - 2) \<Longrightarrow> even' n"
--- a/src/HOL/Nitpick_Examples/Special_Nits.thy Tue Feb 23 11:05:32 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Special_Nits.thy Tue Feb 23 12:14:29 2010 +0100
@@ -110,12 +110,12 @@
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 = potential] (* unfortunate *)
+nitpick [expect = genuine]
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 = potential] (* unfortunate *)
+nitpick [expect = genuine]
oops
lemma "\<forall>a. g a = a
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Tue Feb 23 11:05:32 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Tue Feb 23 12:14:29 2010 +0100
@@ -143,11 +143,11 @@
by (rule Rep_Sum_inverse)
lemma "0::nat \<equiv> Abs_Nat Zero_Rep"
-(* nitpick [expect = none] FIXME *)
+nitpick [expect = none]
by (rule Zero_nat_def_raw)
lemma "Suc \<equiv> \<lambda>n. Abs_Nat (Suc_Rep (Rep_Nat n))"
-(* nitpick [expect = none] FIXME *)
+nitpick [expect = none]
by (rule Suc_def)
lemma "Suc \<equiv> \<lambda>n. Abs_Nat (Suc_Rep (Suc_Rep (Rep_Nat n)))"
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Feb 23 11:05:32 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Feb 23 12:14:29 2010 +0100
@@ -1595,12 +1595,7 @@
KK.Atom (offset_of_type ofs nat_T)
else
fold kk_join (map to_integer [u1, u2]) (KK.Rel nat_subtract_rel)
- | Op2 (Apply, _, R, u1, u2) =>
- if is_Cst Unrep u2 andalso is_set_type (type_of u1) andalso
- is_FreeName u1 then
- false_atom
- else
- to_apply R u1 u2
+ | Op2 (Apply, _, R, u1, u2) => to_apply R u1 u2
| Op2 (Lambda, _, R as Opt (Atom (1, j0)), u1, u2) =>
to_guard [u1, u2] R (KK.Atom j0)
| Op2 (Lambda, _, Func (_, Formula Neut), u1, u2) =>
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Feb 23 11:05:32 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Feb 23 12:14:29 2010 +0100
@@ -95,7 +95,6 @@
val nickname_of : nut -> string
val is_skolem_name : nut -> bool
val is_eval_name : nut -> bool
- val is_FreeName : nut -> bool
val is_Cst : cst -> nut -> bool
val fold_nut : (nut -> 'a -> 'a) -> nut -> 'a -> 'a
val map_nut : (nut -> nut) -> nut -> nut
@@ -369,8 +368,6 @@
fun is_eval_name u =
String.isPrefix eval_prefix (nickname_of u)
handle NUT ("Nitpick_Nut.nickname_of", _) => false
-fun is_FreeName (FreeName _) = true
- | is_FreeName _ = false
(* cst -> nut -> bool *)
fun is_Cst cst (Cst (cst', _, _)) = (cst = cst')
| is_Cst _ _ = false
@@ -794,9 +791,9 @@
end
(* A nut is said to be constructive if whenever it evaluates to unknown in our
- three-valued logic, it would evaluate to a unrepresentable value ("unrep")
+ three-valued logic, it would evaluate to a unrepresentable value ("Unrep")
according to the HOL semantics. For example, "Suc n" is constructive if "n"
- is representable or "Unrep", because unknown implies unrep. *)
+ is representable or "Unrep", because unknown implies "Unrep". *)
(* nut -> bool *)
fun is_constructive u =
is_Cst Unrep u orelse
@@ -819,6 +816,16 @@
fun unknown_boolean T R =
Cst (case R of Formula Pos => False | Formula Neg => True | _ => Unknown,
T, R)
+(* nut -> bool *)
+fun is_fully_representable_set u =
+ not (is_opt_rep (rep_of u)) andalso
+ case u of
+ FreeName _ => true
+ | Op1 (SingletonSet, _, _, _) => true
+ | Op2 (oper, _, _, u1, u2) =>
+ member (op =) [Union, SetDifference, Intersect] oper andalso
+ forall is_fully_representable_set [u1, u2]
+ | _ => false
(* op1 -> typ -> rep -> nut -> nut *)
fun s_op1 oper T R u1 =
@@ -860,7 +867,7 @@
if is_constructive u1 then
Cst (Unrep, T, R)
else if is_boolean_type T then
- if is_FreeName u1 then Cst (False, T, Formula Neut)
+ if is_fully_representable_set u1 then Cst (False, T, Formula Neut)
else unknown_boolean T R
else case u1 of
Op2 (Apply, _, _, ConstName (@{const_name List.append}, _, _), _) =>
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Feb 23 11:05:32 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Feb 23 12:14:29 2010 +0100
@@ -1091,7 +1091,8 @@
else
accum |> fold (add_nondef_axiom depth)
(nondef_props_for_const thy false nondef_table x)
- |> is_funky_typedef thy (range_type T)
+ |> (is_funky_typedef thy (range_type T) orelse
+ range_type T = nat_T)
? fold (add_maybe_def_axiom depth)
(nondef_props_for_const thy true
(extra_table def_table s) x)
@@ -1101,7 +1102,8 @@
else
accum |> fold (add_nondef_axiom depth)
(nondef_props_for_const thy false nondef_table x)
- |> is_funky_typedef thy (range_type T)
+ |> (is_funky_typedef thy (range_type T) orelse
+ range_type T = nat_T)
? fold (add_maybe_def_axiom depth)
(nondef_props_for_const thy true
(extra_table def_table s) x)