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