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