1.1 --- a/doc-src/Nitpick/nitpick.tex	Tue Feb 23 11:05:32 2010 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Tue Feb 23 12:14:29 2010 +0100
     1.3 @@ -154,7 +154,7 @@
     1.4  15~seconds (instead of 30~seconds). This was done by adding the line
     1.5  
     1.6  \prew
     1.7 -\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1, \,\,\textit{timeout} = 15$\,s$]
     1.8 +\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1, \,\textit{timeout} = 15$\,s$]
     1.9  \postw
    1.10  
    1.11  after the \textbf{begin} keyword. The JNI version of MiniSat is bundled with

     2.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue Feb 23 11:05:32 2010 +0100
     2.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue Feb 23 12:14:29 2010 +0100
     2.3 @@ -149,7 +149,7 @@
     2.4  "\<lbrakk>even' m; even' n\<rbrakk> \<Longrightarrow> even' (m + n)"
     2.5  
     2.6  lemma "\<exists>n \<in> {0, 2, 4, 6, 8}. \<not> even' n"
     2.7 -nitpick [card nat = 10, unary_ints, verbose, show_consts] (* FIXME: should be genuine *)
     2.8 +nitpick [card nat = 10, unary_ints, verbose, show_consts]
     2.9  oops
    2.10  
    2.11  lemma "even' (n - 2) \<Longrightarrow> even' n"

     3.1 --- a/src/HOL/Nitpick_Examples/Special_Nits.thy	Tue Feb 23 11:05:32 2010 +0100
     3.2 +++ b/src/HOL/Nitpick_Examples/Special_Nits.thy	Tue Feb 23 12:14:29 2010 +0100
     3.3 @@ -110,12 +110,12 @@
     3.4  
     3.5  lemma "\<exists>one \<in> {1}. \<exists>two \<in> {2}.
     3.6         f5 (\<lambda>a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x"
     3.7 -nitpick [expect = potential] (* unfortunate *)
     3.8 +nitpick [expect = genuine]
     3.9  oops
    3.10  
    3.11  lemma "\<exists>two \<in> {2}. \<exists>one \<in> {1}.
    3.12         f5 (\<lambda>a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x"
    3.13 -nitpick [expect = potential] (* unfortunate *)
    3.14 +nitpick [expect = genuine]
    3.15  oops
    3.16  
    3.17  lemma "\<forall>a. g a = a

     4.1 --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Tue Feb 23 11:05:32 2010 +0100
     4.2 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Tue Feb 23 12:14:29 2010 +0100
     4.3 @@ -143,11 +143,11 @@
     4.4  by (rule Rep_Sum_inverse)
     4.5  
     4.6  lemma "0::nat \<equiv> Abs_Nat Zero_Rep"
     4.7 -(* nitpick [expect = none] FIXME *)
     4.8 +nitpick [expect = none]
     4.9  by (rule Zero_nat_def_raw)
    4.10  
    4.11  lemma "Suc \<equiv> \<lambda>n. Abs_Nat (Suc_Rep (Rep_Nat n))"
    4.12 -(* nitpick [expect = none] FIXME *)
    4.13 +nitpick [expect = none]
    4.14  by (rule Suc_def)
    4.15  
    4.16  lemma "Suc \<equiv> \<lambda>n. Abs_Nat (Suc_Rep (Suc_Rep (Rep_Nat n)))"

     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Feb 23 11:05:32 2010 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Feb 23 12:14:29 2010 +0100
     5.3 @@ -1595,12 +1595,7 @@
     5.4            KK.Atom (offset_of_type ofs nat_T)
     5.5          else
     5.6            fold kk_join (map to_integer [u1, u2]) (KK.Rel nat_subtract_rel)
     5.7 -      | Op2 (Apply, _, R, u1, u2) =>
     5.8 -        if is_Cst Unrep u2 andalso is_set_type (type_of u1) andalso
     5.9 -           is_FreeName u1 then
    5.10 -          false_atom
    5.11 -        else
    5.12 -          to_apply R u1 u2
    5.13 +      | Op2 (Apply, _, R, u1, u2) => to_apply R u1 u2
    5.14        | Op2 (Lambda, _, R as Opt (Atom (1, j0)), u1, u2) =>
    5.15          to_guard [u1, u2] R (KK.Atom j0)
    5.16        | Op2 (Lambda, _, Func (_, Formula Neut), u1, u2) =>

     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Feb 23 11:05:32 2010 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Feb 23 12:14:29 2010 +0100
     6.3 @@ -95,7 +95,6 @@
     6.4    val nickname_of : nut -> string
     6.5    val is_skolem_name : nut -> bool
     6.6    val is_eval_name : nut -> bool
     6.7 -  val is_FreeName : nut -> bool
     6.8    val is_Cst : cst -> nut -> bool
     6.9    val fold_nut : (nut -> 'a -> 'a) -> nut -> 'a -> 'a
    6.10    val map_nut : (nut -> nut) -> nut -> nut
    6.11 @@ -369,8 +368,6 @@
    6.12  fun is_eval_name u =
    6.13    String.isPrefix eval_prefix (nickname_of u)
    6.14    handle NUT ("Nitpick_Nut.nickname_of", _) => false
    6.15 -fun is_FreeName (FreeName _) = true
    6.16 -  | is_FreeName _ = false
    6.17  (* cst -> nut -> bool *)
    6.18  fun is_Cst cst (Cst (cst', _, _)) = (cst = cst')
    6.19    | is_Cst _ _ = false
    6.20 @@ -794,9 +791,9 @@
    6.21    end
    6.22  
    6.23  (* A nut is said to be constructive if whenever it evaluates to unknown in our
    6.24 -   three-valued logic, it would evaluate to a unrepresentable value ("unrep")
    6.25 +   three-valued logic, it would evaluate to a unrepresentable value ("Unrep")
    6.26     according to the HOL semantics. For example, "Suc n" is constructive if "n"
    6.27 -   is representable or "Unrep", because unknown implies unrep. *)
    6.28 +   is representable or "Unrep", because unknown implies "Unrep". *)
    6.29  (* nut -> bool *)
    6.30  fun is_constructive u =
    6.31    is_Cst Unrep u orelse
    6.32 @@ -819,6 +816,16 @@
    6.33  fun unknown_boolean T R =
    6.34    Cst (case R of Formula Pos => False | Formula Neg => True | _ => Unknown,
    6.35         T, R)
    6.36 +(* nut -> bool *)
    6.37 +fun is_fully_representable_set u =
    6.38 +  not (is_opt_rep (rep_of u)) andalso
    6.39 +  case u of
    6.40 +    FreeName _ => true
    6.41 +  | Op1 (SingletonSet, _, _, _) => true
    6.42 +  | Op2 (oper, _, _, u1, u2) =>
    6.43 +    member (op =) [Union, SetDifference, Intersect] oper andalso
    6.44 +    forall is_fully_representable_set [u1, u2]
    6.45 +  | _ => false
    6.46  
    6.47  (* op1 -> typ -> rep -> nut -> nut *)
    6.48  fun s_op1 oper T R u1 =
    6.49 @@ -860,7 +867,7 @@
    6.50          if is_constructive u1 then
    6.51            Cst (Unrep, T, R)
    6.52          else if is_boolean_type T then
    6.53 -          if is_FreeName u1 then Cst (False, T, Formula Neut)
    6.54 +          if is_fully_representable_set u1 then Cst (False, T, Formula Neut)
    6.55            else unknown_boolean T R
    6.56          else case u1 of
    6.57            Op2 (Apply, _, _, ConstName (@{const_name List.append}, _, _), _) =>

     7.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Feb 23 11:05:32 2010 +0100
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Feb 23 12:14:29 2010 +0100
     7.3 @@ -1091,7 +1091,8 @@
     7.4                 else
     7.5                   accum |> fold (add_nondef_axiom depth)
     7.6                                 (nondef_props_for_const thy false nondef_table x)
     7.7 -                       |> is_funky_typedef thy (range_type T)
     7.8 +                       |> (is_funky_typedef thy (range_type T) orelse
     7.9 +                           range_type T = nat_T)
    7.10                            ? fold (add_maybe_def_axiom depth)
    7.11                                   (nondef_props_for_const thy true
    7.12                                                      (extra_table def_table s) x)
    7.13 @@ -1101,7 +1102,8 @@
    7.14                 else
    7.15                   accum |> fold (add_nondef_axiom depth)
    7.16                                 (nondef_props_for_const thy false nondef_table x)
    7.17 -                       |> is_funky_typedef thy (range_type T)
    7.18 +                       |> (is_funky_typedef thy (range_type T) orelse
    7.19 +                           range_type T = nat_T)
    7.20                            ? fold (add_maybe_def_axiom depth)
    7.21                                   (nondef_props_for_const thy true
    7.22                                                      (extra_table def_table s) x)