src/HOL/Numeral.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 24630 351a308ab58d
child 25089 04b8456f7754
permissions -rw-r--r--
Name.uu, Name.aT;
     1 (*  Title:      HOL/Numeral.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 *)
     6 
     7 header {* Arithmetic on Binary Integers *}
     8 
     9 theory Numeral
    10 imports Datatype IntDef
    11 uses
    12   ("Tools/numeral.ML")
    13   ("Tools/numeral_syntax.ML")
    14 begin
    15 
    16 subsection {* Binary representation *}
    17 
    18 text {*
    19   This formalization defines binary arithmetic in terms of the integers
    20   rather than using a datatype. This avoids multiple representations (leading
    21   zeroes, etc.)  See @{text "ZF/Tools/twos-compl.ML"}, function @{text
    22   int_of_binary}, for the numerical interpretation.
    23 
    24   The representation expects that @{text "(m mod 2)"} is 0 or 1,
    25   even if m is negative;
    26   For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
    27   @{text "-5 = (-3)*2 + 1"}.
    28 *}
    29 
    30 datatype bit = B0 | B1
    31 
    32 text{*
    33   Type @{typ bit} avoids the use of type @{typ bool}, which would make
    34   all of the rewrite rules higher-order.
    35 *}
    36 
    37 definition
    38   Pls :: int where
    39   [code func del]: "Pls = 0"
    40 
    41 definition
    42   Min :: int where
    43   [code func del]: "Min = - 1"
    44 
    45 definition
    46   Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
    47   [code func del]: "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
    48 
    49 class number = type + -- {* for numeric types: nat, int, real, \dots *}
    50   fixes number_of :: "int \<Rightarrow> 'a"
    51 
    52 use "Tools/numeral.ML"
    53 
    54 syntax
    55   "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")
    56 
    57 use "Tools/numeral_syntax.ML"
    58 setup NumeralSyntax.setup
    59 
    60 abbreviation
    61   "Numeral0 \<equiv> number_of Pls"
    62 
    63 abbreviation
    64   "Numeral1 \<equiv> number_of (Pls BIT B1)"
    65 
    66 lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"
    67   -- {* Unfold all @{text let}s involving constants *}
    68   unfolding Let_def ..
    69 
    70 definition
    71   succ :: "int \<Rightarrow> int" where
    72   [code func del]: "succ k = k + 1"
    73 
    74 definition
    75   pred :: "int \<Rightarrow> int" where
    76   [code func del]: "pred k = k - 1"
    77 
    78 lemmas
    79   max_number_of [simp] = max_def
    80     [of "number_of u" "number_of v", standard, simp]
    81 and
    82   min_number_of [simp] = min_def 
    83     [of "number_of u" "number_of v", standard, simp]
    84   -- {* unfolding @{text minx} and @{text max} on numerals *}
    85 
    86 lemmas numeral_simps = 
    87   succ_def pred_def Pls_def Min_def Bit_def
    88 
    89 text {* Removal of leading zeroes *}
    90 
    91 lemma Pls_0_eq [simp, code post]:
    92   "Pls BIT B0 = Pls"
    93   unfolding numeral_simps by simp
    94 
    95 lemma Min_1_eq [simp, code post]:
    96   "Min BIT B1 = Min"
    97   unfolding numeral_simps by simp
    98 
    99 
   100 subsection {* The Functions @{term succ}, @{term pred} and @{term uminus} *}
   101 
   102 lemma succ_Pls [simp]:
   103   "succ Pls = Pls BIT B1"
   104   unfolding numeral_simps by simp
   105 
   106 lemma succ_Min [simp]:
   107   "succ Min = Pls"
   108   unfolding numeral_simps by simp
   109 
   110 lemma succ_1 [simp]:
   111   "succ (k BIT B1) = succ k BIT B0"
   112   unfolding numeral_simps by simp
   113 
   114 lemma succ_0 [simp]:
   115   "succ (k BIT B0) = k BIT B1"
   116   unfolding numeral_simps by simp
   117 
   118 lemma pred_Pls [simp]:
   119   "pred Pls = Min"
   120   unfolding numeral_simps by simp
   121 
   122 lemma pred_Min [simp]:
   123   "pred Min = Min BIT B0"
   124   unfolding numeral_simps by simp
   125 
   126 lemma pred_1 [simp]:
   127   "pred (k BIT B1) = k BIT B0"
   128   unfolding numeral_simps by simp
   129 
   130 lemma pred_0 [simp]:
   131   "pred (k BIT B0) = pred k BIT B1"
   132   unfolding numeral_simps by simp 
   133 
   134 lemma minus_Pls [simp]:
   135   "- Pls = Pls"
   136   unfolding numeral_simps by simp 
   137 
   138 lemma minus_Min [simp]:
   139   "- Min = Pls BIT B1"
   140   unfolding numeral_simps by simp 
   141 
   142 lemma minus_1 [simp]:
   143   "- (k BIT B1) = pred (- k) BIT B1"
   144   unfolding numeral_simps by simp 
   145 
   146 lemma minus_0 [simp]:
   147   "- (k BIT B0) = (- k) BIT B0"
   148   unfolding numeral_simps by simp 
   149 
   150 
   151 subsection {*
   152   Binary Addition and Multiplication: @{term "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"}
   153     and @{term "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"}
   154 *}
   155 
   156 lemma add_Pls [simp]:
   157   "Pls + k = k"
   158   unfolding numeral_simps by simp 
   159 
   160 lemma add_Min [simp]:
   161   "Min + k = pred k"
   162   unfolding numeral_simps by simp
   163 
   164 lemma add_BIT_11 [simp]:
   165   "(k BIT B1) + (l BIT B1) = (k + succ l) BIT B0"
   166   unfolding numeral_simps by simp
   167 
   168 lemma add_BIT_10 [simp]:
   169   "(k BIT B1) + (l BIT B0) = (k + l) BIT B1"
   170   unfolding numeral_simps by simp
   171 
   172 lemma add_BIT_0 [simp]:
   173   "(k BIT B0) + (l BIT b) = (k + l) BIT b"
   174   unfolding numeral_simps by simp 
   175 
   176 lemma add_Pls_right [simp]:
   177   "k + Pls = k"
   178   unfolding numeral_simps by simp 
   179 
   180 lemma add_Min_right [simp]:
   181   "k + Min = pred k"
   182   unfolding numeral_simps by simp 
   183 
   184 lemma mult_Pls [simp]:
   185   "Pls * w = Pls"
   186   unfolding numeral_simps by simp 
   187 
   188 lemma mult_Min [simp]:
   189   "Min * k = - k"
   190   unfolding numeral_simps by simp 
   191 
   192 lemma mult_num1 [simp]:
   193   "(k BIT B1) * l = ((k * l) BIT B0) + l"
   194   unfolding numeral_simps int_distrib by simp 
   195 
   196 lemma mult_num0 [simp]:
   197   "(k BIT B0) * l = (k * l) BIT B0"
   198   unfolding numeral_simps int_distrib by simp 
   199 
   200 
   201 
   202 subsection {* Converting Numerals to Rings: @{term number_of} *}
   203 
   204 axclass number_ring \<subseteq> number, comm_ring_1
   205   number_of_eq: "number_of k = of_int k"
   206 
   207 text {* self-embedding of the integers *}
   208 
   209 instance int :: number_ring
   210   int_number_of_def: "number_of w \<equiv> of_int w"
   211   by intro_classes (simp only: int_number_of_def)
   212 
   213 lemmas [code func del] = int_number_of_def
   214 
   215 lemma number_of_is_id:
   216   "number_of (k::int) = k"
   217   unfolding int_number_of_def by simp
   218 
   219 lemma number_of_succ:
   220   "number_of (succ k) = (1 + number_of k ::'a::number_ring)"
   221   unfolding number_of_eq numeral_simps by simp
   222 
   223 lemma number_of_pred:
   224   "number_of (pred w) = (- 1 + number_of w ::'a::number_ring)"
   225   unfolding number_of_eq numeral_simps by simp
   226 
   227 lemma number_of_minus:
   228   "number_of (uminus w) = (- (number_of w)::'a::number_ring)"
   229   unfolding number_of_eq numeral_simps by simp
   230 
   231 lemma number_of_add:
   232   "number_of (v + w) = (number_of v + number_of w::'a::number_ring)"
   233   unfolding number_of_eq numeral_simps by simp
   234 
   235 lemma number_of_mult:
   236   "number_of (v * w) = (number_of v * number_of w::'a::number_ring)"
   237   unfolding number_of_eq numeral_simps by simp
   238 
   239 text {*
   240   The correctness of shifting.
   241   But it doesn't seem to give a measurable speed-up.
   242 *}
   243 
   244 lemma double_number_of_BIT:
   245   "(1 + 1) * number_of w = (number_of (w BIT B0) ::'a::number_ring)"
   246   unfolding number_of_eq numeral_simps left_distrib by simp
   247 
   248 text {*
   249   Converting numerals 0 and 1 to their abstract versions.
   250 *}
   251 
   252 lemma numeral_0_eq_0 [simp]:
   253   "Numeral0 = (0::'a::number_ring)"
   254   unfolding number_of_eq numeral_simps by simp
   255 
   256 lemma numeral_1_eq_1 [simp]:
   257   "Numeral1 = (1::'a::number_ring)"
   258   unfolding number_of_eq numeral_simps by simp
   259 
   260 text {*
   261   Special-case simplification for small constants.
   262 *}
   263 
   264 text{*
   265   Unary minus for the abstract constant 1. Cannot be inserted
   266   as a simprule until later: it is @{text number_of_Min} re-oriented!
   267 *}
   268 
   269 lemma numeral_m1_eq_minus_1:
   270   "(-1::'a::number_ring) = - 1"
   271   unfolding number_of_eq numeral_simps by simp
   272 
   273 lemma mult_minus1 [simp]:
   274   "-1 * z = -(z::'a::number_ring)"
   275   unfolding number_of_eq numeral_simps by simp
   276 
   277 lemma mult_minus1_right [simp]:
   278   "z * -1 = -(z::'a::number_ring)"
   279   unfolding number_of_eq numeral_simps by simp
   280 
   281 (*Negation of a coefficient*)
   282 lemma minus_number_of_mult [simp]:
   283    "- (number_of w) * z = number_of (uminus w) * (z::'a::number_ring)"
   284    unfolding number_of_eq by simp
   285 
   286 text {* Subtraction *}
   287 
   288 lemma diff_number_of_eq:
   289   "number_of v - number_of w =
   290     (number_of (v + uminus w)::'a::number_ring)"
   291   unfolding number_of_eq by simp
   292 
   293 lemma number_of_Pls:
   294   "number_of Pls = (0::'a::number_ring)"
   295   unfolding number_of_eq numeral_simps by simp
   296 
   297 lemma number_of_Min:
   298   "number_of Min = (- 1::'a::number_ring)"
   299   unfolding number_of_eq numeral_simps by simp
   300 
   301 lemma number_of_BIT:
   302   "number_of(w BIT x) = (case x of B0 => 0 | B1 => (1::'a::number_ring))
   303     + (number_of w) + (number_of w)"
   304   unfolding number_of_eq numeral_simps by (simp split: bit.split)
   305 
   306 
   307 subsection {* Equality of Binary Numbers *}
   308 
   309 text {* First version by Norbert Voelker *}
   310 
   311 lemma eq_number_of_eq:
   312   "((number_of x::'a::number_ring) = number_of y) =
   313    iszero (number_of (x + uminus y) :: 'a)"
   314   unfolding iszero_def number_of_add number_of_minus
   315   by (simp add: compare_rls)
   316 
   317 lemma iszero_number_of_Pls:
   318   "iszero ((number_of Pls)::'a::number_ring)"
   319   unfolding iszero_def numeral_0_eq_0 ..
   320 
   321 lemma nonzero_number_of_Min:
   322   "~ iszero ((number_of Min)::'a::number_ring)"
   323   unfolding iszero_def numeral_m1_eq_minus_1 by simp
   324 
   325 
   326 subsection {* Comparisons, for Ordered Rings *}
   327 
   328 lemma double_eq_0_iff:
   329   "(a + a = 0) = (a = (0::'a::ordered_idom))"
   330 proof -
   331   have "a + a = (1 + 1) * a" unfolding left_distrib by simp
   332   with zero_less_two [where 'a = 'a]
   333   show ?thesis by force
   334 qed
   335 
   336 lemma le_imp_0_less: 
   337   assumes le: "0 \<le> z"
   338   shows "(0::int) < 1 + z"
   339 proof -
   340   have "0 \<le> z" by fact
   341   also have "... < z + 1" by (rule less_add_one) 
   342   also have "... = 1 + z" by (simp add: add_ac)
   343   finally show "0 < 1 + z" .
   344 qed
   345 
   346 lemma odd_nonzero:
   347   "1 + z + z \<noteq> (0::int)";
   348 proof (cases z rule: int_cases)
   349   case (nonneg n)
   350   have le: "0 \<le> z+z" by (simp add: nonneg add_increasing) 
   351   thus ?thesis using  le_imp_0_less [OF le]
   352     by (auto simp add: add_assoc) 
   353 next
   354   case (neg n)
   355   show ?thesis
   356   proof
   357     assume eq: "1 + z + z = 0"
   358     have "0 < 1 + (int n + int n)"
   359       by (simp add: le_imp_0_less add_increasing) 
   360     also have "... = - (1 + z + z)" 
   361       by (simp add: neg add_assoc [symmetric]) 
   362     also have "... = 0" by (simp add: eq) 
   363     finally have "0<0" ..
   364     thus False by blast
   365   qed
   366 qed
   367 
   368 text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
   369 
   370 lemma Ints_double_eq_0_iff:
   371   assumes in_Ints: "a \<in> Ints"
   372   shows "(a + a = 0) = (a = (0::'a::ring_char_0))"
   373 proof -
   374   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
   375   then obtain z where a: "a = of_int z" ..
   376   show ?thesis
   377   proof
   378     assume "a = 0"
   379     thus "a + a = 0" by simp
   380   next
   381     assume eq: "a + a = 0"
   382     hence "of_int (z + z) = (of_int 0 :: 'a)" by (simp add: a)
   383     hence "z + z = 0" by (simp only: of_int_eq_iff)
   384     hence "z = 0" by (simp only: double_eq_0_iff)
   385     thus "a = 0" by (simp add: a)
   386   qed
   387 qed
   388 
   389 lemma Ints_odd_nonzero:
   390   assumes in_Ints: "a \<in> Ints"
   391   shows "1 + a + a \<noteq> (0::'a::ring_char_0)"
   392 proof -
   393   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
   394   then obtain z where a: "a = of_int z" ..
   395   show ?thesis
   396   proof
   397     assume eq: "1 + a + a = 0"
   398     hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
   399     hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
   400     with odd_nonzero show False by blast
   401   qed
   402 qed 
   403 
   404 lemma Ints_number_of:
   405   "(number_of w :: 'a::number_ring) \<in> Ints"
   406   unfolding number_of_eq Ints_def by simp
   407 
   408 lemma iszero_number_of_BIT:
   409   "iszero (number_of (w BIT x)::'a) = 
   410    (x = B0 \<and> iszero (number_of w::'a::{ring_char_0,number_ring}))"
   411   by (simp add: iszero_def number_of_eq numeral_simps Ints_double_eq_0_iff 
   412     Ints_odd_nonzero Ints_def split: bit.split)
   413 
   414 lemma iszero_number_of_0:
   415   "iszero (number_of (w BIT B0) :: 'a::{ring_char_0,number_ring}) = 
   416   iszero (number_of w :: 'a)"
   417   by (simp only: iszero_number_of_BIT simp_thms)
   418 
   419 lemma iszero_number_of_1:
   420   "~ iszero (number_of (w BIT B1)::'a::{ring_char_0,number_ring})"
   421   by (simp add: iszero_number_of_BIT) 
   422 
   423 
   424 subsection {* The Less-Than Relation *}
   425 
   426 lemma less_number_of_eq_neg:
   427   "((number_of x::'a::{ordered_idom,number_ring}) < number_of y)
   428   = neg (number_of (x + uminus y) :: 'a)"
   429 apply (subst less_iff_diff_less_0) 
   430 apply (simp add: neg_def diff_minus number_of_add number_of_minus)
   431 done
   432 
   433 text {*
   434   If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
   435   @{term Numeral0} IS @{term "number_of Pls"}
   436 *}
   437 
   438 lemma not_neg_number_of_Pls:
   439   "~ neg (number_of Pls ::'a::{ordered_idom,number_ring})"
   440   by (simp add: neg_def numeral_0_eq_0)
   441 
   442 lemma neg_number_of_Min:
   443   "neg (number_of Min ::'a::{ordered_idom,number_ring})"
   444   by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)
   445 
   446 lemma double_less_0_iff:
   447   "(a + a < 0) = (a < (0::'a::ordered_idom))"
   448 proof -
   449   have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)
   450   also have "... = (a < 0)"
   451     by (simp add: mult_less_0_iff zero_less_two 
   452                   order_less_not_sym [OF zero_less_two]) 
   453   finally show ?thesis .
   454 qed
   455 
   456 lemma odd_less_0:
   457   "(1 + z + z < 0) = (z < (0::int))";
   458 proof (cases z rule: int_cases)
   459   case (nonneg n)
   460   thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
   461                              le_imp_0_less [THEN order_less_imp_le])  
   462 next
   463   case (neg n)
   464   thus ?thesis by (simp del: of_nat_Suc of_nat_add
   465     add: compare_rls of_nat_1 [symmetric] of_nat_add [symmetric])
   466 qed
   467 
   468 text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
   469 
   470 lemma Ints_odd_less_0: 
   471   assumes in_Ints: "a \<in> Ints"
   472   shows "(1 + a + a < 0) = (a < (0::'a::ordered_idom))";
   473 proof -
   474   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
   475   then obtain z where a: "a = of_int z" ..
   476   hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
   477     by (simp add: a)
   478   also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0)
   479   also have "... = (a < 0)" by (simp add: a)
   480   finally show ?thesis .
   481 qed
   482 
   483 lemma neg_number_of_BIT:
   484   "neg (number_of (w BIT x)::'a) = 
   485   neg (number_of w :: 'a::{ordered_idom,number_ring})"
   486   by (simp add: neg_def number_of_eq numeral_simps double_less_0_iff
   487     Ints_odd_less_0 Ints_def split: bit.split)
   488 
   489 
   490 text {* Less-Than or Equals *}
   491 
   492 text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *}
   493 
   494 lemmas le_number_of_eq_not_less =
   495   linorder_not_less [of "number_of w" "number_of v", symmetric, 
   496   standard]
   497 
   498 lemma le_number_of_eq:
   499     "((number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y)
   500      = (~ (neg (number_of (y + uminus x) :: 'a)))"
   501 by (simp add: le_number_of_eq_not_less less_number_of_eq_neg)
   502 
   503 
   504 text {* Absolute value (@{term abs}) *}
   505 
   506 lemma abs_number_of:
   507   "abs(number_of x::'a::{ordered_idom,number_ring}) =
   508    (if number_of x < (0::'a) then -number_of x else number_of x)"
   509   by (simp add: abs_if)
   510 
   511 
   512 text {* Re-orientation of the equation nnn=x *}
   513 
   514 lemma number_of_reorient:
   515   "(number_of w = x) = (x = number_of w)"
   516   by auto
   517 
   518 
   519 subsection {* Simplification of arithmetic operations on integer constants. *}
   520 
   521 lemmas arith_extra_simps [standard, simp] =
   522   number_of_add [symmetric]
   523   number_of_minus [symmetric] numeral_m1_eq_minus_1 [symmetric]
   524   number_of_mult [symmetric]
   525   diff_number_of_eq abs_number_of 
   526 
   527 text {*
   528   For making a minimal simpset, one must include these default simprules.
   529   Also include @{text simp_thms}.
   530 *}
   531 
   532 lemmas arith_simps = 
   533   bit.distinct
   534   Pls_0_eq Min_1_eq
   535   pred_Pls pred_Min pred_1 pred_0
   536   succ_Pls succ_Min succ_1 succ_0
   537   add_Pls add_Min add_BIT_0 add_BIT_10 add_BIT_11
   538   minus_Pls minus_Min minus_1 minus_0
   539   mult_Pls mult_Min mult_num1 mult_num0 
   540   add_Pls_right add_Min_right
   541   abs_zero abs_one arith_extra_simps
   542 
   543 text {* Simplification of relational operations *}
   544 
   545 lemmas rel_simps [simp] = 
   546   eq_number_of_eq iszero_0 nonzero_number_of_Min
   547   iszero_number_of_0 iszero_number_of_1
   548   less_number_of_eq_neg
   549   not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1
   550   neg_number_of_Min neg_number_of_BIT
   551   le_number_of_eq
   552 (* iszero_number_of_Pls would never be used
   553    because its lhs simplifies to "iszero 0" *)
   554 
   555 
   556 subsection {* Simplification of arithmetic when nested to the right. *}
   557 
   558 lemma add_number_of_left [simp]:
   559   "number_of v + (number_of w + z) =
   560    (number_of(v + w) + z::'a::number_ring)"
   561   by (simp add: add_assoc [symmetric])
   562 
   563 lemma mult_number_of_left [simp]:
   564   "number_of v * (number_of w * z) =
   565    (number_of(v * w) * z::'a::number_ring)"
   566   by (simp add: mult_assoc [symmetric])
   567 
   568 lemma add_number_of_diff1:
   569   "number_of v + (number_of w - c) = 
   570   number_of(v + w) - (c::'a::number_ring)"
   571   by (simp add: diff_minus add_number_of_left)
   572 
   573 lemma add_number_of_diff2 [simp]:
   574   "number_of v + (c - number_of w) =
   575    number_of (v + uminus w) + (c::'a::number_ring)"
   576 apply (subst diff_number_of_eq [symmetric])
   577 apply (simp only: compare_rls)
   578 done
   579 
   580 
   581 subsection {* Configuration of the code generator *}
   582 
   583 instance int :: eq ..
   584 
   585 code_datatype Pls Min Bit "number_of \<Colon> int \<Rightarrow> int"
   586 
   587 definition
   588   int_aux :: "nat \<Rightarrow> int \<Rightarrow> int" where
   589   "int_aux n i = int n + i"
   590 
   591 lemma [code]:
   592   "int_aux 0 i  = i"
   593   "int_aux (Suc n) i = int_aux n (i + 1)" -- {* tail recursive *}
   594   by (simp add: int_aux_def)+
   595 
   596 lemma [code unfold]:
   597   "int n = int_aux n 0"
   598   by (simp add: int_aux_def)
   599 
   600 definition
   601   nat_aux :: "int \<Rightarrow> nat \<Rightarrow> nat" where
   602   "nat_aux i n = nat i + n"
   603 
   604 lemma [code]:
   605   "nat_aux i n = (if i \<le> 0 then n else nat_aux (i - 1) (Suc n))"  -- {* tail recursive *}
   606   by (auto simp add: nat_aux_def nat_eq_iff linorder_not_le order_less_imp_le
   607     dest: zless_imp_add1_zle)
   608 
   609 lemma [code]: "nat i = nat_aux i 0"
   610   by (simp add: nat_aux_def)
   611 
   612 lemma zero_is_num_zero [code func, code inline, symmetric, code post]:
   613   "(0\<Colon>int) = Numeral0" 
   614   by simp
   615 
   616 lemma one_is_num_one [code func, code inline, symmetric, code post]:
   617   "(1\<Colon>int) = Numeral1" 
   618   by simp 
   619 
   620 code_modulename SML
   621   IntDef Integer
   622 
   623 code_modulename OCaml
   624   IntDef Integer
   625 
   626 code_modulename Haskell
   627   IntDef Integer
   628 
   629 code_modulename SML
   630   Numeral Integer
   631 
   632 code_modulename OCaml
   633   Numeral Integer
   634 
   635 code_modulename Haskell
   636   Numeral Integer
   637 
   638 types_code
   639   "int" ("int")
   640 attach (term_of) {*
   641 val term_of_int = HOLogic.mk_number HOLogic.intT;
   642 *}
   643 attach (test) {*
   644 fun gen_int i = one_of [~1, 1] * random_range 0 i;
   645 *}
   646 
   647 setup {*
   648 let
   649 
   650 fun strip_number_of (@{term "Numeral.number_of :: int => int"} $ t) = t
   651   | strip_number_of t = t;
   652 
   653 fun numeral_codegen thy defs gr dep module b t =
   654   let val i = HOLogic.dest_numeral (strip_number_of t)
   655   in
   656     SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, HOLogic.intT)),
   657       Pretty.str (string_of_int i))
   658   end handle TERM _ => NONE;
   659 
   660 in
   661 
   662 Codegen.add_codegen "numeral_codegen" numeral_codegen
   663 
   664 end
   665 *}
   666 
   667 consts_code
   668   "number_of :: int \<Rightarrow> int"    ("(_)")
   669   "0 :: int"                   ("0")
   670   "1 :: int"                   ("1")
   671   "uminus :: int => int"       ("~")
   672   "op + :: int => int => int"  ("(_ +/ _)")
   673   "op * :: int => int => int"  ("(_ */ _)")
   674   "op \<le> :: int => int => bool" ("(_ <=/ _)")
   675   "op < :: int => int => bool" ("(_ </ _)")
   676 
   677 quickcheck_params [default_type = int]
   678 
   679 (*setup continues in theory Presburger*)
   680 
   681 hide (open) const Pls Min B0 B1 succ pred
   682 
   683 end