# HG changeset patch
# User blanchet
# Date 1300447232 -3600
# Node ID 33b7d118e9dcf1f1e06f53ff0538ecfe7929ddc3
# Parent  1d7735ae42737d184d11876010a34891e9e730c3
optimize Kodkod bounds of nat-like datatypes

diff -r 1d7735ae4273 -r 33b7d118e9dc src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri Mar 18 12:05:23 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri Mar 18 12:20:32 2011 +0100
@@ -300,6 +300,11 @@
   | bound_for_plain_rel _ _ u =
     raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u])
 
+fun is_datatype_nat_like ({typ, constrs, ...} : datatype_spec) =
+  case constrs |> map (snd o #const) |> List.partition is_fun_type of
+    ([Type (_, Ts1)], [T2]) => forall (curry (op =) typ) (T2 :: Ts1)
+  | _ => false
+
 fun bound_for_sel_rel ctxt debug need_vals dtypes
         (FreeRel (x, T as Type (@{type_name fun}, [T1, T2]),
                   R as Func (Atom (_, j0), R2), nick)) =
@@ -344,7 +349,10 @@
                 index_seq delta (epsilon - delta)
                 |> map (fn j =>
                            KK.TupleProduct (KK.TupleSet [KK.Tuple [j + j0]],
-                                            KK.TupleAtomSeq (j, j0)))
+                                            if is_datatype_nat_like dtype then
+                                              KK.TupleAtomSeq (1, j + j0 - 1)
+                                            else
+                                              KK.TupleAtomSeq (j, j0)))
                 |> foldl1 KK.TupleUnion
               else
                 KK.TupleProduct (upper_bound_ts (), upper_bound_for_rep R2)]