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
```