fixed Nitpick after numeral representation change (2a1953f0d20d)
authorblanchet
Mon Mar 26 10:42:06 2012 +0200 (2012-03-26)
changeset 47109db5026631799
parent 47108 2a1953f0d20d
child 47110 f067afe98049
child 47111 a4476e55a241
fixed Nitpick after numeral representation change (2a1953f0d20d)
src/HOL/Nitpick_Examples/Integer_Nits.thy
src/HOL/Tools/Nitpick/nitpick_hol.ML
     1.1 --- a/src/HOL/Nitpick_Examples/Integer_Nits.thy	Sun Mar 25 20:15:39 2012 +0200
     1.2 +++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy	Mon Mar 26 10:42:06 2012 +0200
     1.3 @@ -198,18 +198,7 @@
     1.4  lemma "-5 * 55 > (-260::int)"
     1.5  nitpick [unary_ints, expect = none]
     1.6  nitpick [binary_ints, expect = none]
     1.7 -(* BROKEN
     1.8 -Nitpicking formula...
     1.9 -Trying 5 scopes:
    1.10 -  card bin = 1, card int = 1, and bits = 9;
    1.11 -  card bin = 2, card int = 2, and bits = 9;
    1.12 -  card bin = 3, card int = 3, and bits = 9;
    1.13 -  card bin = 4, card int = 4, and bits = 9;
    1.14 -  card bin = 5, card int = 5, and bits = 9.
    1.15 -Nitpick found no counterexample.
    1.16 -*** Unexpected outcome: "none".
    1.17  nitpick [binary_ints, bits = 9, expect = genuine]
    1.18 -*)
    1.19  oops
    1.20  
    1.21  lemma "nat (of_nat n) = n"
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Mar 25 20:15:39 2012 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Mar 26 10:42:06 2012 +0200
     2.3 @@ -1636,30 +1636,32 @@
     2.4          (hol_ctxt as {thy, ctxt, stds, whacks, total_consts, case_names,
     2.5                        def_tables, ground_thm_table, ersatz_table, ...}) =
     2.6    let
     2.7 -    fun do_term depth Ts t =
     2.8 +    fun do_numeral depth Ts mult T t0 t1 =
     2.9 +      (if is_number_type ctxt T then
    2.10 +         let
    2.11 +           val j = mult * (HOLogic.dest_num t1)
    2.12 +                   |> T = nat_T ? Integer.max 0
    2.13 +           val s = numeral_prefix ^ signed_string_of_int j
    2.14 +         in
    2.15 +           if is_integer_like_type T then
    2.16 +             if is_standard_datatype thy stds T then Const (s, T)
    2.17 +             else funpow j (curry (op $) (suc_const T)) (zero_const T)
    2.18 +           else
    2.19 +             do_term depth Ts (Const (@{const_name of_int}, int_T --> T)
    2.20 +                               $ Const (s, int_T))
    2.21 +         end
    2.22 +         handle TERM _ => raise SAME ()
    2.23 +       else
    2.24 +         raise SAME ())
    2.25 +      handle SAME () => s_betapply [] (do_term depth Ts t0, do_term depth Ts t1)
    2.26 +    and do_term depth Ts t =
    2.27        case t of
    2.28 -        (t0 as Const (@{const_name Num.numeral_class.numeral},
    2.29 +        (t0 as Const (@{const_name Num.neg_numeral_class.neg_numeral},
    2.30                        Type (@{type_name fun}, [_, ran_T]))) $ t1 =>
    2.31 -        ((if is_number_type ctxt ran_T then
    2.32 -            let
    2.33 -              val j = t1 |> HOLogic.dest_num
    2.34 -                         |> ran_T = nat_T ? Integer.max 0
    2.35 -              val s = numeral_prefix ^ signed_string_of_int j
    2.36 -            in
    2.37 -              if is_integer_like_type ran_T then
    2.38 -                if is_standard_datatype thy stds ran_T then
    2.39 -                  Const (s, ran_T)
    2.40 -                else
    2.41 -                  funpow j (curry (op $) (suc_const ran_T)) (zero_const ran_T)
    2.42 -              else
    2.43 -                do_term depth Ts (Const (@{const_name of_int}, int_T --> ran_T)
    2.44 -                                  $ Const (s, int_T))
    2.45 -            end
    2.46 -            handle TERM _ => raise SAME ()
    2.47 -          else
    2.48 -            raise SAME ())
    2.49 -         handle SAME () =>
    2.50 -                s_betapply [] (do_term depth Ts t0, do_term depth Ts t1))
    2.51 +        do_numeral depth Ts ~1 ran_T t0 t1
    2.52 +      | (t0 as Const (@{const_name Num.numeral_class.numeral},
    2.53 +                      Type (@{type_name fun}, [_, ran_T]))) $ t1 =>
    2.54 +        do_numeral depth Ts 1 ran_T t0 t1
    2.55        | Const (@{const_name refl_on}, T) $ Const (@{const_name top}, _) $ t2 =>
    2.56          do_const depth Ts t (@{const_name refl'}, range_type T) [t2]
    2.57        | (t0 as Const (@{const_name Sigma}, Type (_, [T1, Type (_, [T2, T3])])))