# HG changeset patch
# User blanchet
# Date 1259065338 -3600
# Node ID 9db7854eafc75143cda2509a5325eb9150331866
# Parent  d8958955ecb51d673e52803cc98e77e363a51010
fix soundness bug in Nitpick's handling of negative literals (e.g., -1::rat)

diff -r d8958955ecb5 -r 9db7854eafc7 src/HOL/Tools/Nitpick/HISTORY
--- a/src/HOL/Tools/Nitpick/HISTORY	Tue Nov 24 12:29:08 2009 +0100
+++ b/src/HOL/Tools/Nitpick/HISTORY	Tue Nov 24 13:22:18 2009 +0100
@@ -11,7 +11,7 @@
     the formula to falsify
   * Added support for codatatype view of datatypes
   * Fixed soundness bugs related to sets, sets of sets, (co)inductive
-    predicates, typedefs, and "finite"
+    predicates, typedefs, "finite", and negative literals
   * Fixed monotonicity check
   * Fixed error when processing definitions
   * Fixed error in "star_linear_preds" optimization
diff -r d8958955ecb5 -r 9db7854eafc7 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Nov 24 12:29:08 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Nov 24 13:22:18 2009 +0100
@@ -1440,7 +1440,7 @@
         ((if is_number_type thy ran_T then
             let
               val j = t1 |> HOLogic.dest_numeral
-                         |> ran_T <> int_T ? curry Int.max 0
+                         |> ran_T = nat_T ? Integer.max 0
               val s = numeral_prefix ^ signed_string_of_int j
             in
               if is_integer_type ran_T then
@@ -1656,7 +1656,7 @@
        let
          val binders_T = HOLogic.mk_tupleT (binder_types T)
          val rel_T = HOLogic.mk_prodT (binders_T, binders_T) --> bool_T
-         val j = List.foldl Int.max 0 (map maxidx_of_term intro_ts) + 1
+         val j = fold Integer.max (map maxidx_of_term intro_ts) 0 + 1
          val rel = (("R", j), rel_T)
          val prop = Const (@{const_name wf}, rel_T --> bool_T) $ Var rel ::
                     map (wf_constraint_for_triple rel) triples
@@ -2922,7 +2922,7 @@
   let
     val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2)
     val Ts = binder_types T
-    val max_j = fold (fold (curry Int.max)) [js1, js2] ~1
+    val max_j = fold (fold Integer.max) [js1, js2] ~1
     val (eqs, (args1, args2)) =
       fold (fn j => case pairself (fn ps => AList.lookup (op =) ps j)
                                   (js1 ~~ ts1, js2 ~~ ts2) of