# HG changeset patch
# User blanchet
# Date 1332751326 -7200
# Node ID db502663179986e8be3a29d8dbbc983747a130e2
# Parent  2a1953f0d20db029b6d3135291da4fd9fd961790
fixed Nitpick after numeral representation change (2a1953f0d20d)

diff -r 2a1953f0d20d -r db5026631799 src/HOL/Nitpick_Examples/Integer_Nits.thy
--- a/src/HOL/Nitpick_Examples/Integer_Nits.thy	Sun Mar 25 20:15:39 2012 +0200
+++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy	Mon Mar 26 10:42:06 2012 +0200
@@ -198,18 +198,7 @@
 lemma "-5 * 55 > (-260::int)"
 nitpick [unary_ints, expect = none]
 nitpick [binary_ints, expect = none]
-(* BROKEN
-Nitpicking formula...
-Trying 5 scopes:
-  card bin = 1, card int = 1, and bits = 9;
-  card bin = 2, card int = 2, and bits = 9;
-  card bin = 3, card int = 3, and bits = 9;
-  card bin = 4, card int = 4, and bits = 9;
-  card bin = 5, card int = 5, and bits = 9.
-Nitpick found no counterexample.
-*** Unexpected outcome: "none".
 nitpick [binary_ints, bits = 9, expect = genuine]
-*)
 oops
 
 lemma "nat (of_nat n) = n"
diff -r 2a1953f0d20d -r db5026631799 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Mar 25 20:15:39 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Mar 26 10:42:06 2012 +0200
@@ -1636,30 +1636,32 @@
         (hol_ctxt as {thy, ctxt, stds, whacks, total_consts, case_names,
                       def_tables, ground_thm_table, ersatz_table, ...}) =
   let
-    fun do_term depth Ts t =
+    fun do_numeral depth Ts mult T t0 t1 =
+      (if is_number_type ctxt T then
+         let
+           val j = mult * (HOLogic.dest_num t1)
+                   |> T = nat_T ? Integer.max 0
+           val s = numeral_prefix ^ signed_string_of_int j
+         in
+           if is_integer_like_type T then
+             if is_standard_datatype thy stds T then Const (s, T)
+             else funpow j (curry (op $) (suc_const T)) (zero_const T)
+           else
+             do_term depth Ts (Const (@{const_name of_int}, int_T --> T)
+                               $ Const (s, int_T))
+         end
+         handle TERM _ => raise SAME ()
+       else
+         raise SAME ())
+      handle SAME () => s_betapply [] (do_term depth Ts t0, do_term depth Ts t1)
+    and do_term depth Ts t =
       case t of
-        (t0 as Const (@{const_name Num.numeral_class.numeral},
+        (t0 as Const (@{const_name Num.neg_numeral_class.neg_numeral},
                       Type (@{type_name fun}, [_, ran_T]))) $ t1 =>
-        ((if is_number_type ctxt ran_T then
-            let
-              val j = t1 |> HOLogic.dest_num
-                         |> ran_T = nat_T ? Integer.max 0
-              val s = numeral_prefix ^ signed_string_of_int j
-            in
-              if is_integer_like_type ran_T then
-                if is_standard_datatype thy stds ran_T then
-                  Const (s, ran_T)
-                else
-                  funpow j (curry (op $) (suc_const ran_T)) (zero_const ran_T)
-              else
-                do_term depth Ts (Const (@{const_name of_int}, int_T --> ran_T)
-                                  $ Const (s, int_T))
-            end
-            handle TERM _ => raise SAME ()
-          else
-            raise SAME ())
-         handle SAME () =>
-                s_betapply [] (do_term depth Ts t0, do_term depth Ts t1))
+        do_numeral depth Ts ~1 ran_T t0 t1
+      | (t0 as Const (@{const_name Num.numeral_class.numeral},
+                      Type (@{type_name fun}, [_, ran_T]))) $ t1 =>
+        do_numeral depth Ts 1 ran_T t0 t1
       | Const (@{const_name refl_on}, T) $ Const (@{const_name top}, _) $ t2 =>
         do_const depth Ts t (@{const_name refl'}, range_type T) [t2]
       | (t0 as Const (@{const_name Sigma}, Type (_, [T1, Type (_, [T2, T3])])))