src/HOL/Int.thy
author nipkow
Thu Dec 11 08:52:50 2008 +0100 (2008-12-11)
changeset 29106 25e28a4070f3
parent 28988 13d6f120992b
child 29039 8b9207f82a78
permissions -rw-r--r--
Testfile for Stefan's code generator
     1 (*  Title:      Int.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4                 Tobias Nipkow, Florian Haftmann, TU Muenchen
     5     Copyright   1994  University of Cambridge
     6 
     7 *)
     8 
     9 header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} 
    10 
    11 theory Int
    12 imports Equiv_Relations Nat Wellfounded
    13 uses
    14   ("Tools/numeral.ML")
    15   ("Tools/numeral_syntax.ML")
    16   ("~~/src/Provers/Arith/assoc_fold.ML")
    17   "~~/src/Provers/Arith/cancel_numerals.ML"
    18   "~~/src/Provers/Arith/combine_numerals.ML"
    19   ("Tools/int_arith.ML")
    20 begin
    21 
    22 subsection {* The equivalence relation underlying the integers *}
    23 
    24 definition intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set" where
    25   [code del]: "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
    26 
    27 typedef (Integ)
    28   int = "UNIV//intrel"
    29   by (auto simp add: quotient_def)
    30 
    31 instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
    32 begin
    33 
    34 definition
    35   Zero_int_def [code del]: "0 = Abs_Integ (intrel `` {(0, 0)})"
    36 
    37 definition
    38   One_int_def [code del]: "1 = Abs_Integ (intrel `` {(1, 0)})"
    39 
    40 definition
    41   add_int_def [code del]: "z + w = Abs_Integ
    42     (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u, v) \<in> Rep_Integ w.
    43       intrel `` {(x + u, y + v)})"
    44 
    45 definition
    46   minus_int_def [code del]:
    47     "- z = Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})"
    48 
    49 definition
    50   diff_int_def [code del]:  "z - w = z + (-w \<Colon> int)"
    51 
    52 definition
    53   mult_int_def [code del]: "z * w = Abs_Integ
    54     (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u,v ) \<in> Rep_Integ w.
    55       intrel `` {(x*u + y*v, x*v + y*u)})"
    56 
    57 definition
    58   le_int_def [code del]:
    59    "z \<le> w \<longleftrightarrow> (\<exists>x y u v. x+v \<le> u+y \<and> (x, y) \<in> Rep_Integ z \<and> (u, v) \<in> Rep_Integ w)"
    60 
    61 definition
    62   less_int_def [code del]: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
    63 
    64 definition
    65   zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
    66 
    67 definition
    68   zsgn_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
    69 
    70 instance ..
    71 
    72 end
    73 
    74 
    75 subsection{*Construction of the Integers*}
    76 
    77 lemma intrel_iff [simp]: "(((x,y),(u,v)) \<in> intrel) = (x+v = u+y)"
    78 by (simp add: intrel_def)
    79 
    80 lemma equiv_intrel: "equiv UNIV intrel"
    81 by (simp add: intrel_def equiv_def refl_def sym_def trans_def)
    82 
    83 text{*Reduces equality of equivalence classes to the @{term intrel} relation:
    84   @{term "(intrel `` {x} = intrel `` {y}) = ((x,y) \<in> intrel)"} *}
    85 lemmas equiv_intrel_iff [simp] = eq_equiv_class_iff [OF equiv_intrel UNIV_I UNIV_I]
    86 
    87 text{*All equivalence classes belong to set of representatives*}
    88 lemma [simp]: "intrel``{(x,y)} \<in> Integ"
    89 by (auto simp add: Integ_def intrel_def quotient_def)
    90 
    91 text{*Reduces equality on abstractions to equality on representatives:
    92   @{prop "\<lbrakk>x \<in> Integ; y \<in> Integ\<rbrakk> \<Longrightarrow> (Abs_Integ x = Abs_Integ y) = (x=y)"} *}
    93 declare Abs_Integ_inject [simp,noatp]  Abs_Integ_inverse [simp,noatp]
    94 
    95 text{*Case analysis on the representation of an integer as an equivalence
    96       class of pairs of naturals.*}
    97 lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]:
    98      "(!!x y. z = Abs_Integ(intrel``{(x,y)}) ==> P) ==> P"
    99 apply (rule Abs_Integ_cases [of z]) 
   100 apply (auto simp add: Integ_def quotient_def) 
   101 done
   102 
   103 
   104 subsection {* Arithmetic Operations *}
   105 
   106 lemma minus: "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})"
   107 proof -
   108   have "(\<lambda>(x,y). intrel``{(y,x)}) respects intrel"
   109     by (simp add: congruent_def) 
   110   thus ?thesis
   111     by (simp add: minus_int_def UN_equiv_class [OF equiv_intrel])
   112 qed
   113 
   114 lemma add:
   115      "Abs_Integ (intrel``{(x,y)}) + Abs_Integ (intrel``{(u,v)}) =
   116       Abs_Integ (intrel``{(x+u, y+v)})"
   117 proof -
   118   have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). intrel `` {(x+u, y+v)}) w) z) 
   119         respects2 intrel"
   120     by (simp add: congruent2_def)
   121   thus ?thesis
   122     by (simp add: add_int_def UN_UN_split_split_eq
   123                   UN_equiv_class2 [OF equiv_intrel equiv_intrel])
   124 qed
   125 
   126 text{*Congruence property for multiplication*}
   127 lemma mult_congruent2:
   128      "(%p1 p2. (%(x,y). (%(u,v). intrel``{(x*u + y*v, x*v + y*u)}) p2) p1)
   129       respects2 intrel"
   130 apply (rule equiv_intrel [THEN congruent2_commuteI])
   131  apply (force simp add: mult_ac, clarify) 
   132 apply (simp add: congruent_def mult_ac)  
   133 apply (rename_tac u v w x y z)
   134 apply (subgoal_tac "u*y + x*y = w*y + v*y  &  u*z + x*z = w*z + v*z")
   135 apply (simp add: mult_ac)
   136 apply (simp add: add_mult_distrib [symmetric])
   137 done
   138 
   139 lemma mult:
   140      "Abs_Integ((intrel``{(x,y)})) * Abs_Integ((intrel``{(u,v)})) =
   141       Abs_Integ(intrel `` {(x*u + y*v, x*v + y*u)})"
   142 by (simp add: mult_int_def UN_UN_split_split_eq mult_congruent2
   143               UN_equiv_class2 [OF equiv_intrel equiv_intrel])
   144 
   145 text{*The integers form a @{text comm_ring_1}*}
   146 instance int :: comm_ring_1
   147 proof
   148   fix i j k :: int
   149   show "(i + j) + k = i + (j + k)"
   150     by (cases i, cases j, cases k) (simp add: add add_assoc)
   151   show "i + j = j + i" 
   152     by (cases i, cases j) (simp add: add_ac add)
   153   show "0 + i = i"
   154     by (cases i) (simp add: Zero_int_def add)
   155   show "- i + i = 0"
   156     by (cases i) (simp add: Zero_int_def minus add)
   157   show "i - j = i + - j"
   158     by (simp add: diff_int_def)
   159   show "(i * j) * k = i * (j * k)"
   160     by (cases i, cases j, cases k) (simp add: mult ring_simps)
   161   show "i * j = j * i"
   162     by (cases i, cases j) (simp add: mult ring_simps)
   163   show "1 * i = i"
   164     by (cases i) (simp add: One_int_def mult)
   165   show "(i + j) * k = i * k + j * k"
   166     by (cases i, cases j, cases k) (simp add: add mult ring_simps)
   167   show "0 \<noteq> (1::int)"
   168     by (simp add: Zero_int_def One_int_def)
   169 qed
   170 
   171 lemma int_def: "of_nat m = Abs_Integ (intrel `` {(m, 0)})"
   172 by (induct m, simp_all add: Zero_int_def One_int_def add)
   173 
   174 
   175 subsection {* The @{text "\<le>"} Ordering *}
   176 
   177 lemma le:
   178   "(Abs_Integ(intrel``{(x,y)}) \<le> Abs_Integ(intrel``{(u,v)})) = (x+v \<le> u+y)"
   179 by (force simp add: le_int_def)
   180 
   181 lemma less:
   182   "(Abs_Integ(intrel``{(x,y)}) < Abs_Integ(intrel``{(u,v)})) = (x+v < u+y)"
   183 by (simp add: less_int_def le order_less_le)
   184 
   185 instance int :: linorder
   186 proof
   187   fix i j k :: int
   188   show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
   189     by (cases i, cases j) (simp add: le)
   190   show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
   191     by (auto simp add: less_int_def dest: antisym) 
   192   show "i \<le> i"
   193     by (cases i) (simp add: le)
   194   show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
   195     by (cases i, cases j, cases k) (simp add: le)
   196   show "i \<le> j \<or> j \<le> i"
   197     by (cases i, cases j) (simp add: le linorder_linear)
   198 qed
   199 
   200 instantiation int :: distrib_lattice
   201 begin
   202 
   203 definition
   204   "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
   205 
   206 definition
   207   "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
   208 
   209 instance
   210   by intro_classes
   211     (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
   212 
   213 end
   214 
   215 instance int :: pordered_cancel_ab_semigroup_add
   216 proof
   217   fix i j k :: int
   218   show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
   219     by (cases i, cases j, cases k) (simp add: le add)
   220 qed
   221 
   222 
   223 text{*Strict Monotonicity of Multiplication*}
   224 
   225 text{*strict, in 1st argument; proof is by induction on k>0*}
   226 lemma zmult_zless_mono2_lemma:
   227      "(i::int)<j ==> 0<k ==> of_nat k * i < of_nat k * j"
   228 apply (induct "k", simp)
   229 apply (simp add: left_distrib)
   230 apply (case_tac "k=0")
   231 apply (simp_all add: add_strict_mono)
   232 done
   233 
   234 lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = of_nat n"
   235 apply (cases k)
   236 apply (auto simp add: le add int_def Zero_int_def)
   237 apply (rule_tac x="x-y" in exI, simp)
   238 done
   239 
   240 lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = of_nat n"
   241 apply (cases k)
   242 apply (simp add: less int_def Zero_int_def)
   243 apply (rule_tac x="x-y" in exI, simp)
   244 done
   245 
   246 lemma zmult_zless_mono2: "[| i<j;  (0::int) < k |] ==> k*i < k*j"
   247 apply (drule zero_less_imp_eq_int)
   248 apply (auto simp add: zmult_zless_mono2_lemma)
   249 done
   250 
   251 text{*The integers form an ordered integral domain*}
   252 instance int :: ordered_idom
   253 proof
   254   fix i j k :: int
   255   show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
   256     by (rule zmult_zless_mono2)
   257   show "\<bar>i\<bar> = (if i < 0 then -i else i)"
   258     by (simp only: zabs_def)
   259   show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
   260     by (simp only: zsgn_def)
   261 qed
   262 
   263 instance int :: lordered_ring
   264 proof  
   265   fix k :: int
   266   show "abs k = sup k (- k)"
   267     by (auto simp add: sup_int_def zabs_def max_def less_minus_self_iff [symmetric])
   268 qed
   269 
   270 lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + (1\<Colon>int) \<le> z"
   271 apply (cases w, cases z) 
   272 apply (simp add: less le add One_int_def)
   273 done
   274 
   275 lemma zless_iff_Suc_zadd:
   276   "(w \<Colon> int) < z \<longleftrightarrow> (\<exists>n. z = w + of_nat (Suc n))"
   277 apply (cases z, cases w)
   278 apply (auto simp add: less add int_def)
   279 apply (rename_tac a b c d) 
   280 apply (rule_tac x="a+d - Suc(c+b)" in exI) 
   281 apply arith
   282 done
   283 
   284 lemmas int_distrib =
   285   left_distrib [of "z1::int" "z2" "w", standard]
   286   right_distrib [of "w::int" "z1" "z2", standard]
   287   left_diff_distrib [of "z1::int" "z2" "w", standard]
   288   right_diff_distrib [of "w::int" "z1" "z2", standard]
   289 
   290 
   291 subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}
   292 
   293 context ring_1
   294 begin
   295 
   296 definition
   297   of_int :: "int \<Rightarrow> 'a"
   298 where
   299   [code del]: "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
   300 
   301 lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
   302 proof -
   303   have "(\<lambda>(i,j). { of_nat i - (of_nat j :: 'a) }) respects intrel"
   304     by (simp add: congruent_def compare_rls of_nat_add [symmetric]
   305             del: of_nat_add) 
   306   thus ?thesis
   307     by (simp add: of_int_def UN_equiv_class [OF equiv_intrel])
   308 qed
   309 
   310 lemma of_int_0 [simp]: "of_int 0 = 0"
   311   by (simp add: of_int Zero_int_def)
   312 
   313 lemma of_int_1 [simp]: "of_int 1 = 1"
   314   by (simp add: of_int One_int_def)
   315 
   316 lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z"
   317   by (cases w, cases z, simp add: compare_rls of_int OrderedGroup.compare_rls add)
   318 
   319 lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)"
   320   by (cases z, simp add: compare_rls of_int minus)
   321 
   322 lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z"
   323   by (simp add: OrderedGroup.diff_minus diff_minus)
   324 
   325 lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
   326 apply (cases w, cases z)
   327 apply (simp add: compare_rls of_int left_diff_distrib right_diff_distrib
   328                  mult add_ac of_nat_mult)
   329 done
   330 
   331 text{*Collapse nested embeddings*}
   332 lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n"
   333   by (induct n) auto
   334 
   335 end
   336 
   337 context ordered_idom
   338 begin
   339 
   340 lemma of_int_le_iff [simp]:
   341   "of_int w \<le> of_int z \<longleftrightarrow> w \<le> z"
   342   by (cases w, cases z, simp add: of_int le minus compare_rls of_nat_add [symmetric] del: of_nat_add)
   343 
   344 text{*Special cases where either operand is zero*}
   345 lemmas of_int_0_le_iff [simp] = of_int_le_iff [of 0, simplified]
   346 lemmas of_int_le_0_iff [simp] = of_int_le_iff [of _ 0, simplified]
   347 
   348 lemma of_int_less_iff [simp]:
   349   "of_int w < of_int z \<longleftrightarrow> w < z"
   350   by (simp add: not_le [symmetric] linorder_not_le [symmetric])
   351 
   352 text{*Special cases where either operand is zero*}
   353 lemmas of_int_0_less_iff [simp] = of_int_less_iff [of 0, simplified]
   354 lemmas of_int_less_0_iff [simp] = of_int_less_iff [of _ 0, simplified]
   355 
   356 end
   357 
   358 text{*Class for unital rings with characteristic zero.
   359  Includes non-ordered rings like the complex numbers.*}
   360 class ring_char_0 = ring_1 + semiring_char_0
   361 begin
   362 
   363 lemma of_int_eq_iff [simp]:
   364    "of_int w = of_int z \<longleftrightarrow> w = z"
   365 apply (cases w, cases z, simp add: of_int)
   366 apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq)
   367 apply (simp only: of_nat_add [symmetric] of_nat_eq_iff)
   368 done
   369 
   370 text{*Special cases where either operand is zero*}
   371 lemmas of_int_0_eq_iff [simp] = of_int_eq_iff [of 0, simplified]
   372 lemmas of_int_eq_0_iff [simp] = of_int_eq_iff [of _ 0, simplified]
   373 
   374 end
   375 
   376 text{*Every @{text ordered_idom} has characteristic zero.*}
   377 subclass (in ordered_idom) ring_char_0 by intro_locales
   378 
   379 lemma of_int_eq_id [simp]: "of_int = id"
   380 proof
   381   fix z show "of_int z = id z"
   382     by (cases z) (simp add: of_int add minus int_def diff_minus)
   383 qed
   384 
   385 
   386 subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *}
   387 
   388 definition
   389   nat :: "int \<Rightarrow> nat"
   390 where
   391   [code del]: "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
   392 
   393 lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
   394 proof -
   395   have "(\<lambda>(x,y). {x-y}) respects intrel"
   396     by (simp add: congruent_def) arith
   397   thus ?thesis
   398     by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
   399 qed
   400 
   401 lemma nat_int [simp]: "nat (of_nat n) = n"
   402 by (simp add: nat int_def)
   403 
   404 lemma nat_zero [simp]: "nat 0 = 0"
   405 by (simp add: Zero_int_def nat)
   406 
   407 lemma int_nat_eq [simp]: "of_nat (nat z) = (if 0 \<le> z then z else 0)"
   408 by (cases z, simp add: nat le int_def Zero_int_def)
   409 
   410 corollary nat_0_le: "0 \<le> z ==> of_nat (nat z) = z"
   411 by simp
   412 
   413 lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
   414 by (cases z, simp add: nat le Zero_int_def)
   415 
   416 lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"
   417 apply (cases w, cases z) 
   418 apply (simp add: nat le linorder_not_le [symmetric] Zero_int_def, arith)
   419 done
   420 
   421 text{*An alternative condition is @{term "0 \<le> w"} *}
   422 corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
   423 by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 
   424 
   425 corollary nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"
   426 by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 
   427 
   428 lemma zless_nat_conj [simp]: "(nat w < nat z) = (0 < z & w < z)"
   429 apply (cases w, cases z) 
   430 apply (simp add: nat le Zero_int_def linorder_not_le [symmetric], arith)
   431 done
   432 
   433 lemma nonneg_eq_int:
   434   fixes z :: int
   435   assumes "0 \<le> z" and "\<And>m. z = of_nat m \<Longrightarrow> P"
   436   shows P
   437   using assms by (blast dest: nat_0_le sym)
   438 
   439 lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = of_nat m else m=0)"
   440 by (cases w, simp add: nat le int_def Zero_int_def, arith)
   441 
   442 corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = of_nat m else m=0)"
   443 by (simp only: eq_commute [of m] nat_eq_iff)
   444 
   445 lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)"
   446 apply (cases w)
   447 apply (simp add: nat le int_def Zero_int_def linorder_not_le [symmetric], arith)
   448 done
   449 
   450 lemma int_eq_iff: "(of_nat m = z) = (m = nat z & 0 \<le> z)"
   451 by (auto simp add: nat_eq_iff2)
   452 
   453 lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)"
   454 by (insert zless_nat_conj [of 0], auto)
   455 
   456 lemma nat_add_distrib:
   457      "[| (0::int) \<le> z;  0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"
   458 by (cases z, cases z', simp add: nat add le Zero_int_def)
   459 
   460 lemma nat_diff_distrib:
   461      "[| (0::int) \<le> z';  z' \<le> z |] ==> nat (z-z') = nat z - nat z'"
   462 by (cases z, cases z', 
   463     simp add: nat add minus diff_minus le Zero_int_def)
   464 
   465 lemma nat_zminus_int [simp]: "nat (- (of_nat n)) = 0"
   466 by (simp add: int_def minus nat Zero_int_def) 
   467 
   468 lemma zless_nat_eq_int_zless: "(m < nat z) = (of_nat m < z)"
   469 by (cases z, simp add: nat less int_def, arith)
   470 
   471 context ring_1
   472 begin
   473 
   474 lemma of_nat_nat: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z"
   475   by (cases z rule: eq_Abs_Integ)
   476    (simp add: nat le of_int Zero_int_def of_nat_diff)
   477 
   478 end
   479 
   480 
   481 subsection{*Lemmas about the Function @{term of_nat} and Orderings*}
   482 
   483 lemma negative_zless_0: "- (of_nat (Suc n)) < (0 \<Colon> int)"
   484 by (simp add: order_less_le del: of_nat_Suc)
   485 
   486 lemma negative_zless [iff]: "- (of_nat (Suc n)) < (of_nat m \<Colon> int)"
   487 by (rule negative_zless_0 [THEN order_less_le_trans], simp)
   488 
   489 lemma negative_zle_0: "- of_nat n \<le> (0 \<Colon> int)"
   490 by (simp add: minus_le_iff)
   491 
   492 lemma negative_zle [iff]: "- of_nat n \<le> (of_nat m \<Colon> int)"
   493 by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff])
   494 
   495 lemma not_zle_0_negative [simp]: "~ (0 \<le> - (of_nat (Suc n) \<Colon> int))"
   496 by (subst le_minus_iff, simp del: of_nat_Suc)
   497 
   498 lemma int_zle_neg: "((of_nat n \<Colon> int) \<le> - of_nat m) = (n = 0 & m = 0)"
   499 by (simp add: int_def le minus Zero_int_def)
   500 
   501 lemma not_int_zless_negative [simp]: "~ ((of_nat n \<Colon> int) < - of_nat m)"
   502 by (simp add: linorder_not_less)
   503 
   504 lemma negative_eq_positive [simp]: "((- of_nat n \<Colon> int) = of_nat m) = (n = 0 & m = 0)"
   505 by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg)
   506 
   507 lemma zle_iff_zadd: "(w\<Colon>int) \<le> z \<longleftrightarrow> (\<exists>n. z = w + of_nat n)"
   508 proof -
   509   have "(w \<le> z) = (0 \<le> z - w)"
   510     by (simp only: le_diff_eq add_0_left)
   511   also have "\<dots> = (\<exists>n. z - w = of_nat n)"
   512     by (auto elim: zero_le_imp_eq_int)
   513   also have "\<dots> = (\<exists>n. z = w + of_nat n)"
   514     by (simp only: group_simps)
   515   finally show ?thesis .
   516 qed
   517 
   518 lemma zadd_int_left: "of_nat m + (of_nat n + z) = of_nat (m + n) + (z\<Colon>int)"
   519 by simp
   520 
   521 lemma int_Suc0_eq_1: "of_nat (Suc 0) = (1\<Colon>int)"
   522 by simp
   523 
   524 text{*This version is proved for all ordered rings, not just integers!
   525       It is proved here because attribute @{text arith_split} is not available
   526       in theory @{text Ring_and_Field}.
   527       But is it really better than just rewriting with @{text abs_if}?*}
   528 lemma abs_split [arith_split,noatp]:
   529      "P(abs(a::'a::ordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
   530 by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
   531 
   532 lemma negD: "(x \<Colon> int) < 0 \<Longrightarrow> \<exists>n. x = - (of_nat (Suc n))"
   533 apply (cases x)
   534 apply (auto simp add: le minus Zero_int_def int_def order_less_le)
   535 apply (rule_tac x="y - Suc x" in exI, arith)
   536 done
   537 
   538 
   539 subsection {* Cases and induction *}
   540 
   541 text{*Now we replace the case analysis rule by a more conventional one:
   542 whether an integer is negative or not.*}
   543 
   544 theorem int_cases [cases type: int, case_names nonneg neg]:
   545   "[|!! n. (z \<Colon> int) = of_nat n ==> P;  !! n. z =  - (of_nat (Suc n)) ==> P |] ==> P"
   546 apply (cases "z < 0", blast dest!: negD)
   547 apply (simp add: linorder_not_less del: of_nat_Suc)
   548 apply auto
   549 apply (blast dest: nat_0_le [THEN sym])
   550 done
   551 
   552 theorem int_induct [induct type: int, case_names nonneg neg]:
   553      "[|!! n. P (of_nat n \<Colon> int);  !!n. P (- (of_nat (Suc n))) |] ==> P z"
   554   by (cases z rule: int_cases) auto
   555 
   556 text{*Contributed by Brian Huffman*}
   557 theorem int_diff_cases:
   558   obtains (diff) m n where "(z\<Colon>int) = of_nat m - of_nat n"
   559 apply (cases z rule: eq_Abs_Integ)
   560 apply (rule_tac m=x and n=y in diff)
   561 apply (simp add: int_def diff_def minus add)
   562 done
   563 
   564 
   565 subsection {* Binary representation *}
   566 
   567 text {*
   568   This formalization defines binary arithmetic in terms of the integers
   569   rather than using a datatype. This avoids multiple representations (leading
   570   zeroes, etc.)  See @{text "ZF/Tools/twos-compl.ML"}, function @{text
   571   int_of_binary}, for the numerical interpretation.
   572 
   573   The representation expects that @{text "(m mod 2)"} is 0 or 1,
   574   even if m is negative;
   575   For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
   576   @{text "-5 = (-3)*2 + 1"}.
   577   
   578   This two's complement binary representation derives from the paper 
   579   "An Efficient Representation of Arithmetic for Term Rewriting" by
   580   Dave Cohen and Phil Watson, Rewriting Techniques and Applications,
   581   Springer LNCS 488 (240-251), 1991.
   582 *}
   583 
   584 subsubsection {* The constructors @{term Bit0}, @{term Bit1}, @{term Pls} and @{term Min} *}
   585 
   586 definition
   587   Pls :: int where
   588   [code del]: "Pls = 0"
   589 
   590 definition
   591   Min :: int where
   592   [code del]: "Min = - 1"
   593 
   594 definition
   595   Bit0 :: "int \<Rightarrow> int" where
   596   [code del]: "Bit0 k = k + k"
   597 
   598 definition
   599   Bit1 :: "int \<Rightarrow> int" where
   600   [code del]: "Bit1 k = 1 + k + k"
   601 
   602 class number = type + -- {* for numeric types: nat, int, real, \dots *}
   603   fixes number_of :: "int \<Rightarrow> 'a"
   604 
   605 use "Tools/numeral.ML"
   606 
   607 syntax
   608   "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")
   609 
   610 use "Tools/numeral_syntax.ML"
   611 setup NumeralSyntax.setup
   612 
   613 abbreviation
   614   "Numeral0 \<equiv> number_of Pls"
   615 
   616 abbreviation
   617   "Numeral1 \<equiv> number_of (Bit1 Pls)"
   618 
   619 lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"
   620   -- {* Unfold all @{text let}s involving constants *}
   621   unfolding Let_def ..
   622 
   623 definition
   624   succ :: "int \<Rightarrow> int" where
   625   [code del]: "succ k = k + 1"
   626 
   627 definition
   628   pred :: "int \<Rightarrow> int" where
   629   [code del]: "pred k = k - 1"
   630 
   631 lemmas
   632   max_number_of [simp] = max_def
   633     [of "number_of u" "number_of v", standard, simp]
   634 and
   635   min_number_of [simp] = min_def 
   636     [of "number_of u" "number_of v", standard, simp]
   637   -- {* unfolding @{text minx} and @{text max} on numerals *}
   638 
   639 lemmas numeral_simps = 
   640   succ_def pred_def Pls_def Min_def Bit0_def Bit1_def
   641 
   642 text {* Removal of leading zeroes *}
   643 
   644 lemma Bit0_Pls [simp, code post]:
   645   "Bit0 Pls = Pls"
   646   unfolding numeral_simps by simp
   647 
   648 lemma Bit1_Min [simp, code post]:
   649   "Bit1 Min = Min"
   650   unfolding numeral_simps by simp
   651 
   652 lemmas normalize_bin_simps =
   653   Bit0_Pls Bit1_Min
   654 
   655 
   656 subsubsection {* Successor and predecessor functions *}
   657 
   658 text {* Successor *}
   659 
   660 lemma succ_Pls:
   661   "succ Pls = Bit1 Pls"
   662   unfolding numeral_simps by simp
   663 
   664 lemma succ_Min:
   665   "succ Min = Pls"
   666   unfolding numeral_simps by simp
   667 
   668 lemma succ_Bit0:
   669   "succ (Bit0 k) = Bit1 k"
   670   unfolding numeral_simps by simp
   671 
   672 lemma succ_Bit1:
   673   "succ (Bit1 k) = Bit0 (succ k)"
   674   unfolding numeral_simps by simp
   675 
   676 lemmas succ_bin_simps [simp] =
   677   succ_Pls succ_Min succ_Bit0 succ_Bit1
   678 
   679 text {* Predecessor *}
   680 
   681 lemma pred_Pls:
   682   "pred Pls = Min"
   683   unfolding numeral_simps by simp
   684 
   685 lemma pred_Min:
   686   "pred Min = Bit0 Min"
   687   unfolding numeral_simps by simp
   688 
   689 lemma pred_Bit0:
   690   "pred (Bit0 k) = Bit1 (pred k)"
   691   unfolding numeral_simps by simp 
   692 
   693 lemma pred_Bit1:
   694   "pred (Bit1 k) = Bit0 k"
   695   unfolding numeral_simps by simp
   696 
   697 lemmas pred_bin_simps [simp] =
   698   pred_Pls pred_Min pred_Bit0 pred_Bit1
   699 
   700 
   701 subsubsection {* Binary arithmetic *}
   702 
   703 text {* Addition *}
   704 
   705 lemma add_Pls:
   706   "Pls + k = k"
   707   unfolding numeral_simps by simp
   708 
   709 lemma add_Min:
   710   "Min + k = pred k"
   711   unfolding numeral_simps by simp
   712 
   713 lemma add_Bit0_Bit0:
   714   "(Bit0 k) + (Bit0 l) = Bit0 (k + l)"
   715   unfolding numeral_simps by simp
   716 
   717 lemma add_Bit0_Bit1:
   718   "(Bit0 k) + (Bit1 l) = Bit1 (k + l)"
   719   unfolding numeral_simps by simp
   720 
   721 lemma add_Bit1_Bit0:
   722   "(Bit1 k) + (Bit0 l) = Bit1 (k + l)"
   723   unfolding numeral_simps by simp
   724 
   725 lemma add_Bit1_Bit1:
   726   "(Bit1 k) + (Bit1 l) = Bit0 (k + succ l)"
   727   unfolding numeral_simps by simp
   728 
   729 lemma add_Pls_right:
   730   "k + Pls = k"
   731   unfolding numeral_simps by simp
   732 
   733 lemma add_Min_right:
   734   "k + Min = pred k"
   735   unfolding numeral_simps by simp
   736 
   737 lemmas add_bin_simps [simp] =
   738   add_Pls add_Min add_Pls_right add_Min_right
   739   add_Bit0_Bit0 add_Bit0_Bit1 add_Bit1_Bit0 add_Bit1_Bit1
   740 
   741 text {* Negation *}
   742 
   743 lemma minus_Pls:
   744   "- Pls = Pls"
   745   unfolding numeral_simps by simp
   746 
   747 lemma minus_Min:
   748   "- Min = Bit1 Pls"
   749   unfolding numeral_simps by simp
   750 
   751 lemma minus_Bit0:
   752   "- (Bit0 k) = Bit0 (- k)"
   753   unfolding numeral_simps by simp
   754 
   755 lemma minus_Bit1:
   756   "- (Bit1 k) = Bit1 (pred (- k))"
   757   unfolding numeral_simps by simp
   758 
   759 lemmas minus_bin_simps [simp] =
   760   minus_Pls minus_Min minus_Bit0 minus_Bit1
   761 
   762 text {* Subtraction *}
   763 
   764 lemma diff_Pls:
   765   "Pls - k = - k"
   766   unfolding numeral_simps by simp
   767 
   768 lemma diff_Min:
   769   "Min - k = pred (- k)"
   770   unfolding numeral_simps by simp
   771 
   772 lemma diff_Bit0_Bit0:
   773   "(Bit0 k) - (Bit0 l) = Bit0 (k - l)"
   774   unfolding numeral_simps by simp
   775 
   776 lemma diff_Bit0_Bit1:
   777   "(Bit0 k) - (Bit1 l) = Bit1 (pred k - l)"
   778   unfolding numeral_simps by simp
   779 
   780 lemma diff_Bit1_Bit0:
   781   "(Bit1 k) - (Bit0 l) = Bit1 (k - l)"
   782   unfolding numeral_simps by simp
   783 
   784 lemma diff_Bit1_Bit1:
   785   "(Bit1 k) - (Bit1 l) = Bit0 (k - l)"
   786   unfolding numeral_simps by simp
   787 
   788 lemma diff_Pls_right:
   789   "k - Pls = k"
   790   unfolding numeral_simps by simp
   791 
   792 lemma diff_Min_right:
   793   "k - Min = succ k"
   794   unfolding numeral_simps by simp
   795 
   796 lemmas diff_bin_simps [simp] =
   797   diff_Pls diff_Min diff_Pls_right diff_Min_right
   798   diff_Bit0_Bit0 diff_Bit0_Bit1 diff_Bit1_Bit0 diff_Bit1_Bit1
   799 
   800 text {* Multiplication *}
   801 
   802 lemma mult_Pls:
   803   "Pls * w = Pls"
   804   unfolding numeral_simps by simp
   805 
   806 lemma mult_Min:
   807   "Min * k = - k"
   808   unfolding numeral_simps by simp
   809 
   810 lemma mult_Bit0:
   811   "(Bit0 k) * l = Bit0 (k * l)"
   812   unfolding numeral_simps int_distrib by simp
   813 
   814 lemma mult_Bit1:
   815   "(Bit1 k) * l = (Bit0 (k * l)) + l"
   816   unfolding numeral_simps int_distrib by simp
   817 
   818 lemmas mult_bin_simps [simp] =
   819   mult_Pls mult_Min mult_Bit0 mult_Bit1
   820 
   821 
   822 subsubsection {* Binary comparisons *}
   823 
   824 text {* Preliminaries *}
   825 
   826 lemma even_less_0_iff:
   827   "a + a < 0 \<longleftrightarrow> a < (0::'a::ordered_idom)"
   828 proof -
   829   have "a + a < 0 \<longleftrightarrow> (1+1)*a < 0" by (simp add: left_distrib)
   830   also have "(1+1)*a < 0 \<longleftrightarrow> a < 0"
   831     by (simp add: mult_less_0_iff zero_less_two 
   832                   order_less_not_sym [OF zero_less_two])
   833   finally show ?thesis .
   834 qed
   835 
   836 lemma le_imp_0_less: 
   837   assumes le: "0 \<le> z"
   838   shows "(0::int) < 1 + z"
   839 proof -
   840   have "0 \<le> z" by fact
   841   also have "... < z + 1" by (rule less_add_one) 
   842   also have "... = 1 + z" by (simp add: add_ac)
   843   finally show "0 < 1 + z" .
   844 qed
   845 
   846 lemma odd_less_0_iff:
   847   "(1 + z + z < 0) = (z < (0::int))"
   848 proof (cases z rule: int_cases)
   849   case (nonneg n)
   850   thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
   851                              le_imp_0_less [THEN order_less_imp_le])  
   852 next
   853   case (neg n)
   854   thus ?thesis by (simp del: of_nat_Suc of_nat_add
   855     add: compare_rls of_nat_1 [symmetric] of_nat_add [symmetric])
   856 qed
   857 
   858 lemma bin_less_0_simps:
   859   "Pls < 0 \<longleftrightarrow> False"
   860   "Min < 0 \<longleftrightarrow> True"
   861   "Bit0 w < 0 \<longleftrightarrow> w < 0"
   862   "Bit1 w < 0 \<longleftrightarrow> w < 0"
   863   unfolding numeral_simps
   864   by (simp_all add: even_less_0_iff odd_less_0_iff)
   865 
   866 lemma less_bin_lemma: "k < l \<longleftrightarrow> k - l < (0::int)"
   867   by simp
   868 
   869 lemma le_iff_pred_less: "k \<le> l \<longleftrightarrow> pred k < l"
   870   unfolding numeral_simps
   871   proof
   872     have "k - 1 < k" by simp
   873     also assume "k \<le> l"
   874     finally show "k - 1 < l" .
   875   next
   876     assume "k - 1 < l"
   877     hence "(k - 1) + 1 \<le> l" by (rule zless_imp_add1_zle)
   878     thus "k \<le> l" by simp
   879   qed
   880 
   881 lemma succ_pred: "succ (pred x) = x"
   882   unfolding numeral_simps by simp
   883 
   884 text {* Less-than *}
   885 
   886 lemma less_bin_simps [simp]:
   887   "Pls < Pls \<longleftrightarrow> False"
   888   "Pls < Min \<longleftrightarrow> False"
   889   "Pls < Bit0 k \<longleftrightarrow> Pls < k"
   890   "Pls < Bit1 k \<longleftrightarrow> Pls \<le> k"
   891   "Min < Pls \<longleftrightarrow> True"
   892   "Min < Min \<longleftrightarrow> False"
   893   "Min < Bit0 k \<longleftrightarrow> Min < k"
   894   "Min < Bit1 k \<longleftrightarrow> Min < k"
   895   "Bit0 k < Pls \<longleftrightarrow> k < Pls"
   896   "Bit0 k < Min \<longleftrightarrow> k \<le> Min"
   897   "Bit1 k < Pls \<longleftrightarrow> k < Pls"
   898   "Bit1 k < Min \<longleftrightarrow> k < Min"
   899   "Bit0 k < Bit0 l \<longleftrightarrow> k < l"
   900   "Bit0 k < Bit1 l \<longleftrightarrow> k \<le> l"
   901   "Bit1 k < Bit0 l \<longleftrightarrow> k < l"
   902   "Bit1 k < Bit1 l \<longleftrightarrow> k < l"
   903   unfolding le_iff_pred_less
   904     less_bin_lemma [of Pls]
   905     less_bin_lemma [of Min]
   906     less_bin_lemma [of "k"]
   907     less_bin_lemma [of "Bit0 k"]
   908     less_bin_lemma [of "Bit1 k"]
   909     less_bin_lemma [of "pred Pls"]
   910     less_bin_lemma [of "pred k"]
   911   by (simp_all add: bin_less_0_simps succ_pred)
   912 
   913 text {* Less-than-or-equal *}
   914 
   915 lemma le_bin_simps [simp]:
   916   "Pls \<le> Pls \<longleftrightarrow> True"
   917   "Pls \<le> Min \<longleftrightarrow> False"
   918   "Pls \<le> Bit0 k \<longleftrightarrow> Pls \<le> k"
   919   "Pls \<le> Bit1 k \<longleftrightarrow> Pls \<le> k"
   920   "Min \<le> Pls \<longleftrightarrow> True"
   921   "Min \<le> Min \<longleftrightarrow> True"
   922   "Min \<le> Bit0 k \<longleftrightarrow> Min < k"
   923   "Min \<le> Bit1 k \<longleftrightarrow> Min \<le> k"
   924   "Bit0 k \<le> Pls \<longleftrightarrow> k \<le> Pls"
   925   "Bit0 k \<le> Min \<longleftrightarrow> k \<le> Min"
   926   "Bit1 k \<le> Pls \<longleftrightarrow> k < Pls"
   927   "Bit1 k \<le> Min \<longleftrightarrow> k \<le> Min"
   928   "Bit0 k \<le> Bit0 l \<longleftrightarrow> k \<le> l"
   929   "Bit0 k \<le> Bit1 l \<longleftrightarrow> k \<le> l"
   930   "Bit1 k \<le> Bit0 l \<longleftrightarrow> k < l"
   931   "Bit1 k \<le> Bit1 l \<longleftrightarrow> k \<le> l"
   932   unfolding not_less [symmetric]
   933   by (simp_all add: not_le)
   934 
   935 text {* Equality *}
   936 
   937 lemma eq_bin_simps [simp]:
   938   "Pls = Pls \<longleftrightarrow> True"
   939   "Pls = Min \<longleftrightarrow> False"
   940   "Pls = Bit0 l \<longleftrightarrow> Pls = l"
   941   "Pls = Bit1 l \<longleftrightarrow> False"
   942   "Min = Pls \<longleftrightarrow> False"
   943   "Min = Min \<longleftrightarrow> True"
   944   "Min = Bit0 l \<longleftrightarrow> False"
   945   "Min = Bit1 l \<longleftrightarrow> Min = l"
   946   "Bit0 k = Pls \<longleftrightarrow> k = Pls"
   947   "Bit0 k = Min \<longleftrightarrow> False"
   948   "Bit1 k = Pls \<longleftrightarrow> False"
   949   "Bit1 k = Min \<longleftrightarrow> k = Min"
   950   "Bit0 k = Bit0 l \<longleftrightarrow> k = l"
   951   "Bit0 k = Bit1 l \<longleftrightarrow> False"
   952   "Bit1 k = Bit0 l \<longleftrightarrow> False"
   953   "Bit1 k = Bit1 l \<longleftrightarrow> k = l"
   954   unfolding order_eq_iff [where 'a=int]
   955   by (simp_all add: not_less)
   956 
   957 
   958 subsection {* Converting Numerals to Rings: @{term number_of} *}
   959 
   960 class number_ring = number + comm_ring_1 +
   961   assumes number_of_eq: "number_of k = of_int k"
   962 
   963 text {* self-embedding of the integers *}
   964 
   965 instantiation int :: number_ring
   966 begin
   967 
   968 definition int_number_of_def [code del]:
   969   "number_of w = (of_int w \<Colon> int)"
   970 
   971 instance proof
   972 qed (simp only: int_number_of_def)
   973 
   974 end
   975 
   976 lemma number_of_is_id:
   977   "number_of (k::int) = k"
   978   unfolding int_number_of_def by simp
   979 
   980 lemma number_of_succ:
   981   "number_of (succ k) = (1 + number_of k ::'a::number_ring)"
   982   unfolding number_of_eq numeral_simps by simp
   983 
   984 lemma number_of_pred:
   985   "number_of (pred w) = (- 1 + number_of w ::'a::number_ring)"
   986   unfolding number_of_eq numeral_simps by simp
   987 
   988 lemma number_of_minus:
   989   "number_of (uminus w) = (- (number_of w)::'a::number_ring)"
   990   unfolding number_of_eq by (rule of_int_minus)
   991 
   992 lemma number_of_add:
   993   "number_of (v + w) = (number_of v + number_of w::'a::number_ring)"
   994   unfolding number_of_eq by (rule of_int_add)
   995 
   996 lemma number_of_diff:
   997   "number_of (v - w) = (number_of v - number_of w::'a::number_ring)"
   998   unfolding number_of_eq by (rule of_int_diff)
   999 
  1000 lemma number_of_mult:
  1001   "number_of (v * w) = (number_of v * number_of w::'a::number_ring)"
  1002   unfolding number_of_eq by (rule of_int_mult)
  1003 
  1004 text {*
  1005   The correctness of shifting.
  1006   But it doesn't seem to give a measurable speed-up.
  1007 *}
  1008 
  1009 lemma double_number_of_Bit0:
  1010   "(1 + 1) * number_of w = (number_of (Bit0 w) ::'a::number_ring)"
  1011   unfolding number_of_eq numeral_simps left_distrib by simp
  1012 
  1013 text {*
  1014   Converting numerals 0 and 1 to their abstract versions.
  1015 *}
  1016 
  1017 lemma numeral_0_eq_0 [simp]:
  1018   "Numeral0 = (0::'a::number_ring)"
  1019   unfolding number_of_eq numeral_simps by simp
  1020 
  1021 lemma numeral_1_eq_1 [simp]:
  1022   "Numeral1 = (1::'a::number_ring)"
  1023   unfolding number_of_eq numeral_simps by simp
  1024 
  1025 text {*
  1026   Special-case simplification for small constants.
  1027 *}
  1028 
  1029 text{*
  1030   Unary minus for the abstract constant 1. Cannot be inserted
  1031   as a simprule until later: it is @{text number_of_Min} re-oriented!
  1032 *}
  1033 
  1034 lemma numeral_m1_eq_minus_1:
  1035   "(-1::'a::number_ring) = - 1"
  1036   unfolding number_of_eq numeral_simps by simp
  1037 
  1038 lemma mult_minus1 [simp]:
  1039   "-1 * z = -(z::'a::number_ring)"
  1040   unfolding number_of_eq numeral_simps by simp
  1041 
  1042 lemma mult_minus1_right [simp]:
  1043   "z * -1 = -(z::'a::number_ring)"
  1044   unfolding number_of_eq numeral_simps by simp
  1045 
  1046 (*Negation of a coefficient*)
  1047 lemma minus_number_of_mult [simp]:
  1048    "- (number_of w) * z = number_of (uminus w) * (z::'a::number_ring)"
  1049    unfolding number_of_eq by simp
  1050 
  1051 text {* Subtraction *}
  1052 
  1053 lemma diff_number_of_eq:
  1054   "number_of v - number_of w =
  1055     (number_of (v + uminus w)::'a::number_ring)"
  1056   unfolding number_of_eq by simp
  1057 
  1058 lemma number_of_Pls:
  1059   "number_of Pls = (0::'a::number_ring)"
  1060   unfolding number_of_eq numeral_simps by simp
  1061 
  1062 lemma number_of_Min:
  1063   "number_of Min = (- 1::'a::number_ring)"
  1064   unfolding number_of_eq numeral_simps by simp
  1065 
  1066 lemma number_of_Bit0:
  1067   "number_of (Bit0 w) = (0::'a::number_ring) + (number_of w) + (number_of w)"
  1068   unfolding number_of_eq numeral_simps by simp
  1069 
  1070 lemma number_of_Bit1:
  1071   "number_of (Bit1 w) = (1::'a::number_ring) + (number_of w) + (number_of w)"
  1072   unfolding number_of_eq numeral_simps by simp
  1073 
  1074 
  1075 subsubsection {* Equality of Binary Numbers *}
  1076 
  1077 text {* First version by Norbert Voelker *}
  1078 
  1079 definition
  1080   neg  :: "'a\<Colon>ordered_idom \<Rightarrow> bool"
  1081 where
  1082   "neg Z \<longleftrightarrow> Z < 0"
  1083 
  1084 definition (*for simplifying equalities*)
  1085   iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool"
  1086 where
  1087   "iszero z \<longleftrightarrow> z = 0"
  1088 
  1089 lemma not_neg_int [simp]: "~ neg (of_nat n)"
  1090 by (simp add: neg_def)
  1091 
  1092 lemma neg_zminus_int [simp]: "neg (- (of_nat (Suc n)))"
  1093 by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc)
  1094 
  1095 lemmas neg_eq_less_0 = neg_def
  1096 
  1097 lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)"
  1098 by (simp add: neg_def linorder_not_less)
  1099 
  1100 text{*To simplify inequalities when Numeral1 can get simplified to 1*}
  1101 
  1102 lemma not_neg_0: "~ neg 0"
  1103 by (simp add: One_int_def neg_def)
  1104 
  1105 lemma not_neg_1: "~ neg 1"
  1106 by (simp add: neg_def linorder_not_less zero_le_one)
  1107 
  1108 lemma iszero_0: "iszero 0"
  1109 by (simp add: iszero_def)
  1110 
  1111 lemma not_iszero_1: "~ iszero 1"
  1112 by (simp add: iszero_def eq_commute)
  1113 
  1114 lemma neg_nat: "neg z ==> nat z = 0"
  1115 by (simp add: neg_def order_less_imp_le) 
  1116 
  1117 lemma not_neg_nat: "~ neg z ==> of_nat (nat z) = z"
  1118 by (simp add: linorder_not_less neg_def)
  1119 
  1120 lemma eq_number_of_eq:
  1121   "((number_of x::'a::number_ring) = number_of y) =
  1122    iszero (number_of (x + uminus y) :: 'a)"
  1123   unfolding iszero_def number_of_add number_of_minus
  1124   by (simp add: compare_rls)
  1125 
  1126 lemma iszero_number_of_Pls:
  1127   "iszero ((number_of Pls)::'a::number_ring)"
  1128   unfolding iszero_def numeral_0_eq_0 ..
  1129 
  1130 lemma nonzero_number_of_Min:
  1131   "~ iszero ((number_of Min)::'a::number_ring)"
  1132   unfolding iszero_def numeral_m1_eq_minus_1 by simp
  1133 
  1134 
  1135 subsubsection {* Comparisons, for Ordered Rings *}
  1136 
  1137 lemmas double_eq_0_iff = double_zero
  1138 
  1139 lemma odd_nonzero:
  1140   "1 + z + z \<noteq> (0::int)";
  1141 proof (cases z rule: int_cases)
  1142   case (nonneg n)
  1143   have le: "0 \<le> z+z" by (simp add: nonneg add_increasing) 
  1144   thus ?thesis using  le_imp_0_less [OF le]
  1145     by (auto simp add: add_assoc) 
  1146 next
  1147   case (neg n)
  1148   show ?thesis
  1149   proof
  1150     assume eq: "1 + z + z = 0"
  1151     have "(0::int) < 1 + (of_nat n + of_nat n)"
  1152       by (simp add: le_imp_0_less add_increasing) 
  1153     also have "... = - (1 + z + z)" 
  1154       by (simp add: neg add_assoc [symmetric]) 
  1155     also have "... = 0" by (simp add: eq) 
  1156     finally have "0<0" ..
  1157     thus False by blast
  1158   qed
  1159 qed
  1160 
  1161 lemma iszero_number_of_Bit0:
  1162   "iszero (number_of (Bit0 w)::'a) = 
  1163    iszero (number_of w::'a::{ring_char_0,number_ring})"
  1164 proof -
  1165   have "(of_int w + of_int w = (0::'a)) \<Longrightarrow> (w = 0)"
  1166   proof -
  1167     assume eq: "of_int w + of_int w = (0::'a)"
  1168     then have "of_int (w + w) = (of_int 0 :: 'a)" by simp
  1169     then have "w + w = 0" by (simp only: of_int_eq_iff)
  1170     then show "w = 0" by (simp only: double_eq_0_iff)
  1171   qed
  1172   thus ?thesis
  1173     by (auto simp add: iszero_def number_of_eq numeral_simps)
  1174 qed
  1175 
  1176 lemma iszero_number_of_Bit1:
  1177   "~ iszero (number_of (Bit1 w)::'a::{ring_char_0,number_ring})"
  1178 proof -
  1179   have "1 + of_int w + of_int w \<noteq> (0::'a)"
  1180   proof
  1181     assume eq: "1 + of_int w + of_int w = (0::'a)"
  1182     hence "of_int (1 + w + w) = (of_int 0 :: 'a)" by simp 
  1183     hence "1 + w + w = 0" by (simp only: of_int_eq_iff)
  1184     with odd_nonzero show False by blast
  1185   qed
  1186   thus ?thesis
  1187     by (auto simp add: iszero_def number_of_eq numeral_simps)
  1188 qed
  1189 
  1190 lemmas iszero_simps =
  1191   iszero_0 not_iszero_1
  1192   iszero_number_of_Pls nonzero_number_of_Min
  1193   iszero_number_of_Bit0 iszero_number_of_Bit1
  1194 (* iszero_number_of_Pls would never normally be used
  1195    because its lhs simplifies to "iszero 0" *)
  1196 
  1197 subsubsection {* The Less-Than Relation *}
  1198 
  1199 lemma less_number_of_eq_neg:
  1200   "((number_of x::'a::{ordered_idom,number_ring}) < number_of y)
  1201   = neg (number_of (x + uminus y) :: 'a)"
  1202 apply (subst less_iff_diff_less_0) 
  1203 apply (simp add: neg_def diff_minus number_of_add number_of_minus)
  1204 done
  1205 
  1206 text {*
  1207   If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
  1208   @{term Numeral0} IS @{term "number_of Pls"}
  1209 *}
  1210 
  1211 lemma not_neg_number_of_Pls:
  1212   "~ neg (number_of Pls ::'a::{ordered_idom,number_ring})"
  1213   by (simp add: neg_def numeral_0_eq_0)
  1214 
  1215 lemma neg_number_of_Min:
  1216   "neg (number_of Min ::'a::{ordered_idom,number_ring})"
  1217   by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)
  1218 
  1219 lemma double_less_0_iff:
  1220   "(a + a < 0) = (a < (0::'a::ordered_idom))"
  1221 proof -
  1222   have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)
  1223   also have "... = (a < 0)"
  1224     by (simp add: mult_less_0_iff zero_less_two 
  1225                   order_less_not_sym [OF zero_less_two]) 
  1226   finally show ?thesis .
  1227 qed
  1228 
  1229 lemma odd_less_0:
  1230   "(1 + z + z < 0) = (z < (0::int))";
  1231 proof (cases z rule: int_cases)
  1232   case (nonneg n)
  1233   thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
  1234                              le_imp_0_less [THEN order_less_imp_le])  
  1235 next
  1236   case (neg n)
  1237   thus ?thesis by (simp del: of_nat_Suc of_nat_add
  1238     add: compare_rls of_nat_1 [symmetric] of_nat_add [symmetric])
  1239 qed
  1240 
  1241 lemma neg_number_of_Bit0:
  1242   "neg (number_of (Bit0 w)::'a) = 
  1243   neg (number_of w :: 'a::{ordered_idom,number_ring})"
  1244 by (simp add: neg_def number_of_eq numeral_simps double_less_0_iff)
  1245 
  1246 lemma neg_number_of_Bit1:
  1247   "neg (number_of (Bit1 w)::'a) = 
  1248   neg (number_of w :: 'a::{ordered_idom,number_ring})"
  1249 proof -
  1250   have "((1::'a) + of_int w + of_int w < 0) = (of_int (1 + w + w) < (of_int 0 :: 'a))"
  1251     by simp
  1252   also have "... = (w < 0)" by (simp only: of_int_less_iff odd_less_0)
  1253   finally show ?thesis
  1254   by (simp add: neg_def number_of_eq numeral_simps)
  1255 qed
  1256 
  1257 lemmas neg_simps =
  1258   not_neg_0 not_neg_1
  1259   not_neg_number_of_Pls neg_number_of_Min
  1260   neg_number_of_Bit0 neg_number_of_Bit1
  1261 
  1262 text {* Less-Than or Equals *}
  1263 
  1264 text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *}
  1265 
  1266 lemmas le_number_of_eq_not_less =
  1267   linorder_not_less [of "number_of w" "number_of v", symmetric, 
  1268   standard]
  1269 
  1270 lemma le_number_of_eq:
  1271     "((number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y)
  1272      = (~ (neg (number_of (y + uminus x) :: 'a)))"
  1273 by (simp add: le_number_of_eq_not_less less_number_of_eq_neg)
  1274 
  1275 
  1276 text {* Absolute value (@{term abs}) *}
  1277 
  1278 lemma abs_number_of:
  1279   "abs(number_of x::'a::{ordered_idom,number_ring}) =
  1280    (if number_of x < (0::'a) then -number_of x else number_of x)"
  1281   by (simp add: abs_if)
  1282 
  1283 
  1284 text {* Re-orientation of the equation nnn=x *}
  1285 
  1286 lemma number_of_reorient:
  1287   "(number_of w = x) = (x = number_of w)"
  1288   by auto
  1289 
  1290 
  1291 subsubsection {* Simplification of arithmetic operations on integer constants. *}
  1292 
  1293 lemmas arith_extra_simps [standard, simp] =
  1294   number_of_add [symmetric]
  1295   number_of_minus [symmetric]
  1296   numeral_m1_eq_minus_1 [symmetric]
  1297   number_of_mult [symmetric]
  1298   diff_number_of_eq abs_number_of 
  1299 
  1300 text {*
  1301   For making a minimal simpset, one must include these default simprules.
  1302   Also include @{text simp_thms}.
  1303 *}
  1304 
  1305 lemmas arith_simps = 
  1306   normalize_bin_simps pred_bin_simps succ_bin_simps
  1307   add_bin_simps minus_bin_simps mult_bin_simps
  1308   abs_zero abs_one arith_extra_simps
  1309 
  1310 text {* Simplification of relational operations *}
  1311 
  1312 lemma less_number_of [simp]:
  1313   "(number_of x::'a::{ordered_idom,number_ring}) < number_of y \<longleftrightarrow> x < y"
  1314   unfolding number_of_eq by (rule of_int_less_iff)
  1315 
  1316 lemma le_number_of [simp]:
  1317   "(number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y \<longleftrightarrow> x \<le> y"
  1318   unfolding number_of_eq by (rule of_int_le_iff)
  1319 
  1320 lemma eq_number_of [simp]:
  1321   "(number_of x::'a::{ring_char_0,number_ring}) = number_of y \<longleftrightarrow> x = y"
  1322   unfolding number_of_eq by (rule of_int_eq_iff)
  1323 
  1324 lemmas rel_simps [simp] = 
  1325   less_number_of less_bin_simps
  1326   le_number_of le_bin_simps
  1327   eq_number_of_eq eq_bin_simps
  1328   iszero_simps neg_simps
  1329 
  1330 
  1331 subsubsection {* Simplification of arithmetic when nested to the right. *}
  1332 
  1333 lemma add_number_of_left [simp]:
  1334   "number_of v + (number_of w + z) =
  1335    (number_of(v + w) + z::'a::number_ring)"
  1336   by (simp add: add_assoc [symmetric])
  1337 
  1338 lemma mult_number_of_left [simp]:
  1339   "number_of v * (number_of w * z) =
  1340    (number_of(v * w) * z::'a::number_ring)"
  1341   by (simp add: mult_assoc [symmetric])
  1342 
  1343 lemma add_number_of_diff1:
  1344   "number_of v + (number_of w - c) = 
  1345   number_of(v + w) - (c::'a::number_ring)"
  1346   by (simp add: diff_minus add_number_of_left)
  1347 
  1348 lemma add_number_of_diff2 [simp]:
  1349   "number_of v + (c - number_of w) =
  1350    number_of (v + uminus w) + (c::'a::number_ring)"
  1351 apply (subst diff_number_of_eq [symmetric])
  1352 apply (simp only: compare_rls)
  1353 done
  1354 
  1355 
  1356 subsection {* The Set of Integers *}
  1357 
  1358 context ring_1
  1359 begin
  1360 
  1361 definition
  1362   Ints  :: "'a set"
  1363 where
  1364   [code del]: "Ints = range of_int"
  1365 
  1366 end
  1367 
  1368 notation (xsymbols)
  1369   Ints  ("\<int>")
  1370 
  1371 context ring_1
  1372 begin
  1373 
  1374 lemma Ints_0 [simp]: "0 \<in> \<int>"
  1375 apply (simp add: Ints_def)
  1376 apply (rule range_eqI)
  1377 apply (rule of_int_0 [symmetric])
  1378 done
  1379 
  1380 lemma Ints_1 [simp]: "1 \<in> \<int>"
  1381 apply (simp add: Ints_def)
  1382 apply (rule range_eqI)
  1383 apply (rule of_int_1 [symmetric])
  1384 done
  1385 
  1386 lemma Ints_add [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a + b \<in> \<int>"
  1387 apply (auto simp add: Ints_def)
  1388 apply (rule range_eqI)
  1389 apply (rule of_int_add [symmetric])
  1390 done
  1391 
  1392 lemma Ints_minus [simp]: "a \<in> \<int> \<Longrightarrow> -a \<in> \<int>"
  1393 apply (auto simp add: Ints_def)
  1394 apply (rule range_eqI)
  1395 apply (rule of_int_minus [symmetric])
  1396 done
  1397 
  1398 lemma Ints_mult [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a * b \<in> \<int>"
  1399 apply (auto simp add: Ints_def)
  1400 apply (rule range_eqI)
  1401 apply (rule of_int_mult [symmetric])
  1402 done
  1403 
  1404 lemma Ints_cases [cases set: Ints]:
  1405   assumes "q \<in> \<int>"
  1406   obtains (of_int) z where "q = of_int z"
  1407   unfolding Ints_def
  1408 proof -
  1409   from `q \<in> \<int>` have "q \<in> range of_int" unfolding Ints_def .
  1410   then obtain z where "q = of_int z" ..
  1411   then show thesis ..
  1412 qed
  1413 
  1414 lemma Ints_induct [case_names of_int, induct set: Ints]:
  1415   "q \<in> \<int> \<Longrightarrow> (\<And>z. P (of_int z)) \<Longrightarrow> P q"
  1416   by (rule Ints_cases) auto
  1417 
  1418 end
  1419 
  1420 lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a-b \<in> \<int>"
  1421 apply (auto simp add: Ints_def)
  1422 apply (rule range_eqI)
  1423 apply (rule of_int_diff [symmetric])
  1424 done
  1425 
  1426 text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
  1427 
  1428 lemma Ints_double_eq_0_iff:
  1429   assumes in_Ints: "a \<in> Ints"
  1430   shows "(a + a = 0) = (a = (0::'a::ring_char_0))"
  1431 proof -
  1432   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
  1433   then obtain z where a: "a = of_int z" ..
  1434   show ?thesis
  1435   proof
  1436     assume "a = 0"
  1437     thus "a + a = 0" by simp
  1438   next
  1439     assume eq: "a + a = 0"
  1440     hence "of_int (z + z) = (of_int 0 :: 'a)" by (simp add: a)
  1441     hence "z + z = 0" by (simp only: of_int_eq_iff)
  1442     hence "z = 0" by (simp only: double_eq_0_iff)
  1443     thus "a = 0" by (simp add: a)
  1444   qed
  1445 qed
  1446 
  1447 lemma Ints_odd_nonzero:
  1448   assumes in_Ints: "a \<in> Ints"
  1449   shows "1 + a + a \<noteq> (0::'a::ring_char_0)"
  1450 proof -
  1451   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
  1452   then obtain z where a: "a = of_int z" ..
  1453   show ?thesis
  1454   proof
  1455     assume eq: "1 + a + a = 0"
  1456     hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
  1457     hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
  1458     with odd_nonzero show False by blast
  1459   qed
  1460 qed 
  1461 
  1462 lemma Ints_number_of:
  1463   "(number_of w :: 'a::number_ring) \<in> Ints"
  1464   unfolding number_of_eq Ints_def by simp
  1465 
  1466 lemma Ints_odd_less_0: 
  1467   assumes in_Ints: "a \<in> Ints"
  1468   shows "(1 + a + a < 0) = (a < (0::'a::ordered_idom))";
  1469 proof -
  1470   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
  1471   then obtain z where a: "a = of_int z" ..
  1472   hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
  1473     by (simp add: a)
  1474   also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0)
  1475   also have "... = (a < 0)" by (simp add: a)
  1476   finally show ?thesis .
  1477 qed
  1478 
  1479 
  1480 subsection {* @{term setsum} and @{term setprod} *}
  1481 
  1482 text {*By Jeremy Avigad*}
  1483 
  1484 lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
  1485   apply (cases "finite A")
  1486   apply (erule finite_induct, auto)
  1487   done
  1488 
  1489 lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
  1490   apply (cases "finite A")
  1491   apply (erule finite_induct, auto)
  1492   done
  1493 
  1494 lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
  1495   apply (cases "finite A")
  1496   apply (erule finite_induct, auto simp add: of_nat_mult)
  1497   done
  1498 
  1499 lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
  1500   apply (cases "finite A")
  1501   apply (erule finite_induct, auto)
  1502   done
  1503 
  1504 lemma setprod_nonzero_nat:
  1505     "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0"
  1506   by (rule setprod_nonzero, auto)
  1507 
  1508 lemma setprod_zero_eq_nat:
  1509     "finite A ==> (setprod f A = (0::nat)) = (\<exists>x \<in> A. f x = 0)"
  1510   by (rule setprod_zero_eq, auto)
  1511 
  1512 lemma setprod_nonzero_int:
  1513     "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::int)) ==> setprod f A \<noteq> 0"
  1514   by (rule setprod_nonzero, auto)
  1515 
  1516 lemma setprod_zero_eq_int:
  1517     "finite A ==> (setprod f A = (0::int)) = (\<exists>x \<in> A. f x = 0)"
  1518   by (rule setprod_zero_eq, auto)
  1519 
  1520 lemmas int_setsum = of_nat_setsum [where 'a=int]
  1521 lemmas int_setprod = of_nat_setprod [where 'a=int]
  1522 
  1523 
  1524 subsection{*Inequality Reasoning for the Arithmetic Simproc*}
  1525 
  1526 lemma add_numeral_0: "Numeral0 + a = (a::'a::number_ring)"
  1527 by simp 
  1528 
  1529 lemma add_numeral_0_right: "a + Numeral0 = (a::'a::number_ring)"
  1530 by simp
  1531 
  1532 lemma mult_numeral_1: "Numeral1 * a = (a::'a::number_ring)"
  1533 by simp 
  1534 
  1535 lemma mult_numeral_1_right: "a * Numeral1 = (a::'a::number_ring)"
  1536 by simp
  1537 
  1538 lemma divide_numeral_1: "a / Numeral1 = (a::'a::{number_ring,field})"
  1539 by simp
  1540 
  1541 lemma inverse_numeral_1:
  1542   "inverse Numeral1 = (Numeral1::'a::{number_ring,field})"
  1543 by simp
  1544 
  1545 text{*Theorem lists for the cancellation simprocs. The use of binary numerals
  1546 for 0 and 1 reduces the number of special cases.*}
  1547 
  1548 lemmas add_0s = add_numeral_0 add_numeral_0_right
  1549 lemmas mult_1s = mult_numeral_1 mult_numeral_1_right 
  1550                  mult_minus1 mult_minus1_right
  1551 
  1552 
  1553 subsection{*Special Arithmetic Rules for Abstract 0 and 1*}
  1554 
  1555 text{*Arithmetic computations are defined for binary literals, which leaves 0
  1556 and 1 as special cases. Addition already has rules for 0, but not 1.
  1557 Multiplication and unary minus already have rules for both 0 and 1.*}
  1558 
  1559 
  1560 lemma binop_eq: "[|f x y = g x y; x = x'; y = y'|] ==> f x' y' = g x' y'"
  1561 by simp
  1562 
  1563 
  1564 lemmas add_number_of_eq = number_of_add [symmetric]
  1565 
  1566 text{*Allow 1 on either or both sides*}
  1567 lemma one_add_one_is_two: "1 + 1 = (2::'a::number_ring)"
  1568 by (simp del: numeral_1_eq_1 add: numeral_1_eq_1 [symmetric] add_number_of_eq)
  1569 
  1570 lemmas add_special =
  1571     one_add_one_is_two
  1572     binop_eq [of "op +", OF add_number_of_eq numeral_1_eq_1 refl, standard]
  1573     binop_eq [of "op +", OF add_number_of_eq refl numeral_1_eq_1, standard]
  1574 
  1575 text{*Allow 1 on either or both sides (1-1 already simplifies to 0)*}
  1576 lemmas diff_special =
  1577     binop_eq [of "op -", OF diff_number_of_eq numeral_1_eq_1 refl, standard]
  1578     binop_eq [of "op -", OF diff_number_of_eq refl numeral_1_eq_1, standard]
  1579 
  1580 text{*Allow 0 or 1 on either side with a binary numeral on the other*}
  1581 lemmas eq_special =
  1582     binop_eq [of "op =", OF eq_number_of_eq numeral_0_eq_0 refl, standard]
  1583     binop_eq [of "op =", OF eq_number_of_eq numeral_1_eq_1 refl, standard]
  1584     binop_eq [of "op =", OF eq_number_of_eq refl numeral_0_eq_0, standard]
  1585     binop_eq [of "op =", OF eq_number_of_eq refl numeral_1_eq_1, standard]
  1586 
  1587 text{*Allow 0 or 1 on either side with a binary numeral on the other*}
  1588 lemmas less_special =
  1589   binop_eq [of "op <", OF less_number_of numeral_0_eq_0 refl, standard]
  1590   binop_eq [of "op <", OF less_number_of numeral_1_eq_1 refl, standard]
  1591   binop_eq [of "op <", OF less_number_of refl numeral_0_eq_0, standard]
  1592   binop_eq [of "op <", OF less_number_of refl numeral_1_eq_1, standard]
  1593 
  1594 text{*Allow 0 or 1 on either side with a binary numeral on the other*}
  1595 lemmas le_special =
  1596     binop_eq [of "op \<le>", OF le_number_of numeral_0_eq_0 refl, standard]
  1597     binop_eq [of "op \<le>", OF le_number_of numeral_1_eq_1 refl, standard]
  1598     binop_eq [of "op \<le>", OF le_number_of refl numeral_0_eq_0, standard]
  1599     binop_eq [of "op \<le>", OF le_number_of refl numeral_1_eq_1, standard]
  1600 
  1601 lemmas arith_special[simp] = 
  1602        add_special diff_special eq_special less_special le_special
  1603 
  1604 
  1605 lemma min_max_01: "min (0::int) 1 = 0 & min (1::int) 0 = 0 &
  1606                    max (0::int) 1 = 1 & max (1::int) 0 = 1"
  1607 by(simp add:min_def max_def)
  1608 
  1609 lemmas min_max_special[simp] =
  1610  min_max_01
  1611  max_def[of "0::int" "number_of v", standard, simp]
  1612  min_def[of "0::int" "number_of v", standard, simp]
  1613  max_def[of "number_of u" "0::int", standard, simp]
  1614  min_def[of "number_of u" "0::int", standard, simp]
  1615  max_def[of "1::int" "number_of v", standard, simp]
  1616  min_def[of "1::int" "number_of v", standard, simp]
  1617  max_def[of "number_of u" "1::int", standard, simp]
  1618  min_def[of "number_of u" "1::int", standard, simp]
  1619 
  1620 text {* Legacy theorems *}
  1621 
  1622 lemmas zle_int = of_nat_le_iff [where 'a=int]
  1623 lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
  1624 
  1625 use "~~/src/Provers/Arith/assoc_fold.ML"
  1626 use "Tools/int_arith.ML"
  1627 declaration {* K int_arith_setup *}
  1628 
  1629 
  1630 subsection{*Lemmas About Small Numerals*}
  1631 
  1632 lemma of_int_m1 [simp]: "of_int -1 = (-1 :: 'a :: number_ring)"
  1633 proof -
  1634   have "(of_int -1 :: 'a) = of_int (- 1)" by simp
  1635   also have "... = - of_int 1" by (simp only: of_int_minus)
  1636   also have "... = -1" by simp
  1637   finally show ?thesis .
  1638 qed
  1639 
  1640 lemma abs_minus_one [simp]: "abs (-1) = (1::'a::{ordered_idom,number_ring})"
  1641 by (simp add: abs_if)
  1642 
  1643 lemma abs_power_minus_one [simp]:
  1644      "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring,recpower})"
  1645 by (simp add: power_abs)
  1646 
  1647 lemma of_int_number_of_eq:
  1648      "of_int (number_of v) = (number_of v :: 'a :: number_ring)"
  1649 by (simp add: number_of_eq) 
  1650 
  1651 text{*Lemmas for specialist use, NOT as default simprules*}
  1652 lemma mult_2: "2 * z = (z+z::'a::number_ring)"
  1653 proof -
  1654   have "2*z = (1 + 1)*z" by simp
  1655   also have "... = z+z" by (simp add: left_distrib)
  1656   finally show ?thesis .
  1657 qed
  1658 
  1659 lemma mult_2_right: "z * 2 = (z+z::'a::number_ring)"
  1660 by (subst mult_commute, rule mult_2)
  1661 
  1662 
  1663 subsection{*More Inequality Reasoning*}
  1664 
  1665 lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
  1666 by arith
  1667 
  1668 lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
  1669 by arith
  1670 
  1671 lemma zle_diff1_eq [simp]: "(w \<le> z - (1::int)) = (w<z)"
  1672 by arith
  1673 
  1674 lemma zle_add1_eq_le [simp]: "(w < z + (1::int)) = (w\<le>z)"
  1675 by arith
  1676 
  1677 lemma int_one_le_iff_zero_less: "((1::int) \<le> z) = (0 < z)"
  1678 by arith
  1679 
  1680 
  1681 subsection{*The functions @{term nat} and @{term int}*}
  1682 
  1683 text{*Simplify the terms @{term "int 0"}, @{term "int(Suc 0)"} and
  1684   @{term "w + - z"}*}
  1685 declare Zero_int_def [symmetric, simp]
  1686 declare One_int_def [symmetric, simp]
  1687 
  1688 lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp]
  1689 
  1690 lemma nat_0: "nat 0 = 0"
  1691 by (simp add: nat_eq_iff)
  1692 
  1693 lemma nat_1: "nat 1 = Suc 0"
  1694 by (subst nat_eq_iff, simp)
  1695 
  1696 lemma nat_2: "nat 2 = Suc (Suc 0)"
  1697 by (subst nat_eq_iff, simp)
  1698 
  1699 lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
  1700 apply (insert zless_nat_conj [of 1 z])
  1701 apply (auto simp add: nat_1)
  1702 done
  1703 
  1704 text{*This simplifies expressions of the form @{term "int n = z"} where
  1705       z is an integer literal.*}
  1706 lemmas int_eq_iff_number_of [simp] = int_eq_iff [of _ "number_of v", standard]
  1707 
  1708 lemma split_nat [arith_split]:
  1709   "P(nat(i::int)) = ((\<forall>n. i = of_nat n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
  1710   (is "?P = (?L & ?R)")
  1711 proof (cases "i < 0")
  1712   case True thus ?thesis by auto
  1713 next
  1714   case False
  1715   have "?P = ?L"
  1716   proof
  1717     assume ?P thus ?L using False by clarsimp
  1718   next
  1719     assume ?L thus ?P using False by simp
  1720   qed
  1721   with False show ?thesis by simp
  1722 qed
  1723 
  1724 context ring_1
  1725 begin
  1726 
  1727 lemma of_int_of_nat:
  1728   "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))"
  1729 proof (cases "k < 0")
  1730   case True then have "0 \<le> - k" by simp
  1731   then have "of_nat (nat (- k)) = of_int (- k)" by (rule of_nat_nat)
  1732   with True show ?thesis by simp
  1733 next
  1734   case False then show ?thesis by (simp add: not_less of_nat_nat)
  1735 qed
  1736 
  1737 end
  1738 
  1739 lemma nat_mult_distrib:
  1740   fixes z z' :: int
  1741   assumes "0 \<le> z"
  1742   shows "nat (z * z') = nat z * nat z'"
  1743 proof (cases "0 \<le> z'")
  1744   case False with assms have "z * z' \<le> 0"
  1745     by (simp add: not_le mult_le_0_iff)
  1746   then have "nat (z * z') = 0" by simp
  1747   moreover from False have "nat z' = 0" by simp
  1748   ultimately show ?thesis by simp
  1749 next
  1750   case True with assms have ge_0: "z * z' \<ge> 0" by (simp add: zero_le_mult_iff)
  1751   show ?thesis
  1752     by (rule injD [of "of_nat :: nat \<Rightarrow> int", OF inj_of_nat])
  1753       (simp only: of_nat_mult of_nat_nat [OF True]
  1754          of_nat_nat [OF assms] of_nat_nat [OF ge_0], simp)
  1755 qed
  1756 
  1757 lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"
  1758 apply (rule trans)
  1759 apply (rule_tac [2] nat_mult_distrib, auto)
  1760 done
  1761 
  1762 lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
  1763 apply (cases "z=0 | w=0")
  1764 apply (auto simp add: abs_if nat_mult_distrib [symmetric] 
  1765                       nat_mult_distrib_neg [symmetric] mult_less_0_iff)
  1766 done
  1767 
  1768 
  1769 subsection "Induction principles for int"
  1770 
  1771 text{*Well-founded segments of the integers*}
  1772 
  1773 definition
  1774   int_ge_less_than  ::  "int => (int * int) set"
  1775 where
  1776   "int_ge_less_than d = {(z',z). d \<le> z' & z' < z}"
  1777 
  1778 theorem wf_int_ge_less_than: "wf (int_ge_less_than d)"
  1779 proof -
  1780   have "int_ge_less_than d \<subseteq> measure (%z. nat (z-d))"
  1781     by (auto simp add: int_ge_less_than_def)
  1782   thus ?thesis 
  1783     by (rule wf_subset [OF wf_measure]) 
  1784 qed
  1785 
  1786 text{*This variant looks odd, but is typical of the relations suggested
  1787 by RankFinder.*}
  1788 
  1789 definition
  1790   int_ge_less_than2 ::  "int => (int * int) set"
  1791 where
  1792   "int_ge_less_than2 d = {(z',z). d \<le> z & z' < z}"
  1793 
  1794 theorem wf_int_ge_less_than2: "wf (int_ge_less_than2 d)"
  1795 proof -
  1796   have "int_ge_less_than2 d \<subseteq> measure (%z. nat (1+z-d))" 
  1797     by (auto simp add: int_ge_less_than2_def)
  1798   thus ?thesis 
  1799     by (rule wf_subset [OF wf_measure]) 
  1800 qed
  1801 
  1802 abbreviation
  1803   int :: "nat \<Rightarrow> int"
  1804 where
  1805   "int \<equiv> of_nat"
  1806 
  1807 (* `set:int': dummy construction *)
  1808 theorem int_ge_induct [case_names base step, induct set: int]:
  1809   fixes i :: int
  1810   assumes ge: "k \<le> i" and
  1811     base: "P k" and
  1812     step: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
  1813   shows "P i"
  1814 proof -
  1815   { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i"
  1816     proof (induct n)
  1817       case 0
  1818       hence "i = k" by arith
  1819       thus "P i" using base by simp
  1820     next
  1821       case (Suc n)
  1822       then have "n = nat((i - 1) - k)" by arith
  1823       moreover
  1824       have ki1: "k \<le> i - 1" using Suc.prems by arith
  1825       ultimately
  1826       have "P(i - 1)" by(rule Suc.hyps)
  1827       from step[OF ki1 this] show ?case by simp
  1828     qed
  1829   }
  1830   with ge show ?thesis by fast
  1831 qed
  1832 
  1833 (* `set:int': dummy construction *)
  1834 theorem int_gr_induct [case_names base step, induct set: int]:
  1835   assumes gr: "k < (i::int)" and
  1836         base: "P(k+1)" and
  1837         step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
  1838   shows "P i"
  1839 apply(rule int_ge_induct[of "k + 1"])
  1840   using gr apply arith
  1841  apply(rule base)
  1842 apply (rule step, simp+)
  1843 done
  1844 
  1845 theorem int_le_induct[consumes 1,case_names base step]:
  1846   assumes le: "i \<le> (k::int)" and
  1847         base: "P(k)" and
  1848         step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
  1849   shows "P i"
  1850 proof -
  1851   { fix n have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i"
  1852     proof (induct n)
  1853       case 0
  1854       hence "i = k" by arith
  1855       thus "P i" using base by simp
  1856     next
  1857       case (Suc n)
  1858       hence "n = nat(k - (i+1))" by arith
  1859       moreover
  1860       have ki1: "i + 1 \<le> k" using Suc.prems by arith
  1861       ultimately
  1862       have "P(i+1)" by(rule Suc.hyps)
  1863       from step[OF ki1 this] show ?case by simp
  1864     qed
  1865   }
  1866   with le show ?thesis by fast
  1867 qed
  1868 
  1869 theorem int_less_induct [consumes 1,case_names base step]:
  1870   assumes less: "(i::int) < k" and
  1871         base: "P(k - 1)" and
  1872         step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
  1873   shows "P i"
  1874 apply(rule int_le_induct[of _ "k - 1"])
  1875   using less apply arith
  1876  apply(rule base)
  1877 apply (rule step, simp+)
  1878 done
  1879 
  1880 subsection{*Intermediate value theorems*}
  1881 
  1882 lemma int_val_lemma:
  1883      "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->  
  1884       f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
  1885 apply (induct n, simp)
  1886 apply (intro strip)
  1887 apply (erule impE, simp)
  1888 apply (erule_tac x = n in allE, simp)
  1889 apply (case_tac "k = f (n+1) ")
  1890 apply force
  1891 apply (erule impE)
  1892  apply (simp add: abs_if split add: split_if_asm)
  1893 apply (blast intro: le_SucI)
  1894 done
  1895 
  1896 lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
  1897 
  1898 lemma nat_intermed_int_val:
  1899      "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;  
  1900          f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
  1901 apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k 
  1902        in int_val_lemma)
  1903 apply simp
  1904 apply (erule exE)
  1905 apply (rule_tac x = "i+m" in exI, arith)
  1906 done
  1907 
  1908 
  1909 subsection{*Products and 1, by T. M. Rasmussen*}
  1910 
  1911 lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))"
  1912 by arith
  1913 
  1914 lemma abs_zmult_eq_1: "(\<bar>m * n\<bar> = 1) ==> \<bar>m\<bar> = (1::int)"
  1915 apply (cases "\<bar>n\<bar>=1") 
  1916 apply (simp add: abs_mult) 
  1917 apply (rule ccontr) 
  1918 apply (auto simp add: linorder_neq_iff abs_mult) 
  1919 apply (subgoal_tac "2 \<le> \<bar>m\<bar> & 2 \<le> \<bar>n\<bar>")
  1920  prefer 2 apply arith 
  1921 apply (subgoal_tac "2*2 \<le> \<bar>m\<bar> * \<bar>n\<bar>", simp) 
  1922 apply (rule mult_mono, auto) 
  1923 done
  1924 
  1925 lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1"
  1926 by (insert abs_zmult_eq_1 [of m n], arith)
  1927 
  1928 lemma pos_zmult_eq_1_iff: "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)"
  1929 apply (auto dest: pos_zmult_eq_1_iff_lemma) 
  1930 apply (simp add: mult_commute [of m]) 
  1931 apply (frule pos_zmult_eq_1_iff_lemma, auto) 
  1932 done
  1933 
  1934 lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
  1935 apply (rule iffI) 
  1936  apply (frule pos_zmult_eq_1_iff_lemma)
  1937  apply (simp add: mult_commute [of m]) 
  1938  apply (frule pos_zmult_eq_1_iff_lemma, auto) 
  1939 done
  1940 
  1941 (* Could be simplified but Presburger only becomes available too late *)
  1942 lemma infinite_UNIV_int: "~finite(UNIV::int set)"
  1943 proof
  1944   assume "finite(UNIV::int set)"
  1945   moreover have "~(EX i::int. 2*i = 1)"
  1946     by (auto simp: pos_zmult_eq_1_iff)
  1947   ultimately show False using finite_UNIV_inj_surj[of "%n::int. n+n"]
  1948     by (simp add:inj_on_def surj_def) (blast intro:sym)
  1949 qed
  1950 
  1951 
  1952 subsection{*Integer Powers*} 
  1953 
  1954 instantiation int :: recpower
  1955 begin
  1956 
  1957 primrec power_int where
  1958   "p ^ 0 = (1\<Colon>int)"
  1959   | "p ^ (Suc n) = (p\<Colon>int) * (p ^ n)"
  1960 
  1961 instance proof
  1962   fix z :: int
  1963   fix n :: nat
  1964   show "z ^ 0 = 1" by simp
  1965   show "z ^ Suc n = z * (z ^ n)" by simp
  1966 qed
  1967 
  1968 end
  1969 
  1970 lemma zpower_zadd_distrib: "x ^ (y + z) = ((x ^ y) * (x ^ z)::int)"
  1971   by (rule Power.power_add)
  1972 
  1973 lemma zpower_zpower: "(x ^ y) ^ z = (x ^ (y * z)::int)"
  1974   by (rule Power.power_mult [symmetric])
  1975 
  1976 lemma zero_less_zpower_abs_iff [simp]:
  1977   "(0 < abs x ^ n) \<longleftrightarrow> (x \<noteq> (0::int) | n = 0)"
  1978   by (induct n) (auto simp add: zero_less_mult_iff)
  1979 
  1980 lemma zero_le_zpower_abs [simp]: "(0::int) \<le> abs x ^ n"
  1981   by (induct n) (auto simp add: zero_le_mult_iff)
  1982 
  1983 lemma of_int_power:
  1984   "of_int (z ^ n) = (of_int z ^ n :: 'a::{recpower, ring_1})"
  1985   by (induct n) (simp_all add: power_Suc)
  1986 
  1987 lemma int_power: "int (m^n) = (int m) ^ n"
  1988   by (rule of_nat_power)
  1989 
  1990 lemmas zpower_int = int_power [symmetric]
  1991 
  1992 subsection {* Configuration of the code generator *}
  1993 
  1994 code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int"
  1995 
  1996 lemmas pred_succ_numeral_code [code] =
  1997   pred_bin_simps succ_bin_simps
  1998 
  1999 lemmas plus_numeral_code [code] =
  2000   add_bin_simps
  2001   arith_extra_simps(1) [where 'a = int]
  2002 
  2003 lemmas minus_numeral_code [code] =
  2004   minus_bin_simps
  2005   arith_extra_simps(2) [where 'a = int]
  2006   arith_extra_simps(5) [where 'a = int]
  2007 
  2008 lemmas times_numeral_code [code] =
  2009   mult_bin_simps
  2010   arith_extra_simps(4) [where 'a = int]
  2011 
  2012 instantiation int :: eq
  2013 begin
  2014 
  2015 definition [code del]: "eq_class.eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
  2016 
  2017 instance by default (simp add: eq_int_def)
  2018 
  2019 end
  2020 
  2021 lemma eq_number_of_int_code [code]:
  2022   "eq_class.eq (number_of k \<Colon> int) (number_of l) \<longleftrightarrow> eq_class.eq k l"
  2023   unfolding eq_int_def number_of_is_id ..
  2024 
  2025 lemma eq_int_code [code]:
  2026   "eq_class.eq Int.Pls Int.Pls \<longleftrightarrow> True"
  2027   "eq_class.eq Int.Pls Int.Min \<longleftrightarrow> False"
  2028   "eq_class.eq Int.Pls (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq Int.Pls k2"
  2029   "eq_class.eq Int.Pls (Int.Bit1 k2) \<longleftrightarrow> False"
  2030   "eq_class.eq Int.Min Int.Pls \<longleftrightarrow> False"
  2031   "eq_class.eq Int.Min Int.Min \<longleftrightarrow> True"
  2032   "eq_class.eq Int.Min (Int.Bit0 k2) \<longleftrightarrow> False"
  2033   "eq_class.eq Int.Min (Int.Bit1 k2) \<longleftrightarrow> eq_class.eq Int.Min k2"
  2034   "eq_class.eq (Int.Bit0 k1) Int.Pls \<longleftrightarrow> eq_class.eq k1 Int.Pls"
  2035   "eq_class.eq (Int.Bit1 k1) Int.Pls \<longleftrightarrow> False"
  2036   "eq_class.eq (Int.Bit0 k1) Int.Min \<longleftrightarrow> False"
  2037   "eq_class.eq (Int.Bit1 k1) Int.Min \<longleftrightarrow> eq_class.eq k1 Int.Min"
  2038   "eq_class.eq (Int.Bit0 k1) (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq k1 k2"
  2039   "eq_class.eq (Int.Bit0 k1) (Int.Bit1 k2) \<longleftrightarrow> False"
  2040   "eq_class.eq (Int.Bit1 k1) (Int.Bit0 k2) \<longleftrightarrow> False"
  2041   "eq_class.eq (Int.Bit1 k1) (Int.Bit1 k2) \<longleftrightarrow> eq_class.eq k1 k2"
  2042   unfolding eq_equals by simp_all
  2043 
  2044 lemma eq_int_refl [code nbe]:
  2045   "eq_class.eq (k::int) k \<longleftrightarrow> True"
  2046   by (rule HOL.eq_refl)
  2047 
  2048 lemma less_eq_number_of_int_code [code]:
  2049   "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
  2050   unfolding number_of_is_id ..
  2051 
  2052 lemma less_eq_int_code [code]:
  2053   "Int.Pls \<le> Int.Pls \<longleftrightarrow> True"
  2054   "Int.Pls \<le> Int.Min \<longleftrightarrow> False"
  2055   "Int.Pls \<le> Int.Bit0 k \<longleftrightarrow> Int.Pls \<le> k"
  2056   "Int.Pls \<le> Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
  2057   "Int.Min \<le> Int.Pls \<longleftrightarrow> True"
  2058   "Int.Min \<le> Int.Min \<longleftrightarrow> True"
  2059   "Int.Min \<le> Int.Bit0 k \<longleftrightarrow> Int.Min < k"
  2060   "Int.Min \<le> Int.Bit1 k \<longleftrightarrow> Int.Min \<le> k"
  2061   "Int.Bit0 k \<le> Int.Pls \<longleftrightarrow> k \<le> Int.Pls"
  2062   "Int.Bit1 k \<le> Int.Pls \<longleftrightarrow> k < Int.Pls"
  2063   "Int.Bit0 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
  2064   "Int.Bit1 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
  2065   "Int.Bit0 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 \<le> k2"
  2066   "Int.Bit0 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
  2067   "Int.Bit1 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
  2068   "Int.Bit1 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
  2069   by simp_all
  2070 
  2071 lemma less_number_of_int_code [code]:
  2072   "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
  2073   unfolding number_of_is_id ..
  2074 
  2075 lemma less_int_code [code]:
  2076   "Int.Pls < Int.Pls \<longleftrightarrow> False"
  2077   "Int.Pls < Int.Min \<longleftrightarrow> False"
  2078   "Int.Pls < Int.Bit0 k \<longleftrightarrow> Int.Pls < k"
  2079   "Int.Pls < Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
  2080   "Int.Min < Int.Pls \<longleftrightarrow> True"
  2081   "Int.Min < Int.Min \<longleftrightarrow> False"
  2082   "Int.Min < Int.Bit0 k \<longleftrightarrow> Int.Min < k"
  2083   "Int.Min < Int.Bit1 k \<longleftrightarrow> Int.Min < k"
  2084   "Int.Bit0 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
  2085   "Int.Bit1 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
  2086   "Int.Bit0 k < Int.Min \<longleftrightarrow> k \<le> Int.Min"
  2087   "Int.Bit1 k < Int.Min \<longleftrightarrow> k < Int.Min"
  2088   "Int.Bit0 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
  2089   "Int.Bit0 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
  2090   "Int.Bit1 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
  2091   "Int.Bit1 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 < k2"
  2092   by simp_all
  2093 
  2094 definition
  2095   nat_aux :: "int \<Rightarrow> nat \<Rightarrow> nat" where
  2096   "nat_aux i n = nat i + n"
  2097 
  2098 lemma [code]:
  2099   "nat_aux i n = (if i \<le> 0 then n else nat_aux (i - 1) (Suc n))"  -- {* tail recursive *}
  2100   by (auto simp add: nat_aux_def nat_eq_iff linorder_not_le order_less_imp_le
  2101     dest: zless_imp_add1_zle)
  2102 
  2103 lemma [code]: "nat i = nat_aux i 0"
  2104   by (simp add: nat_aux_def)
  2105 
  2106 hide (open) const nat_aux
  2107 
  2108 lemma zero_is_num_zero [code, code inline, symmetric, code post]:
  2109   "(0\<Colon>int) = Numeral0" 
  2110   by simp
  2111 
  2112 lemma one_is_num_one [code, code inline, symmetric, code post]:
  2113   "(1\<Colon>int) = Numeral1" 
  2114   by simp
  2115 
  2116 code_modulename SML
  2117   Int Integer
  2118 
  2119 code_modulename OCaml
  2120   Int Integer
  2121 
  2122 code_modulename Haskell
  2123   Int Integer
  2124 
  2125 types_code
  2126   "int" ("int")
  2127 attach (term_of) {*
  2128 val term_of_int = HOLogic.mk_number HOLogic.intT;
  2129 *}
  2130 attach (test) {*
  2131 fun gen_int i =
  2132   let val j = one_of [~1, 1] * random_range 0 i
  2133   in (j, fn () => term_of_int j) end;
  2134 *}
  2135 
  2136 setup {*
  2137 let
  2138 
  2139 fun strip_number_of (@{term "Int.number_of :: int => int"} $ t) = t
  2140   | strip_number_of t = t;
  2141 
  2142 fun numeral_codegen thy defs dep module b t gr =
  2143   let val i = HOLogic.dest_numeral (strip_number_of t)
  2144   in
  2145     SOME (Codegen.str (string_of_int i),
  2146       snd (Codegen.invoke_tycodegen thy defs dep module false HOLogic.intT gr))
  2147   end handle TERM _ => NONE;
  2148 
  2149 in
  2150 
  2151 Codegen.add_codegen "numeral_codegen" numeral_codegen
  2152 
  2153 end
  2154 *}
  2155 
  2156 consts_code
  2157   "number_of :: int \<Rightarrow> int"    ("(_)")
  2158   "0 :: int"                   ("0")
  2159   "1 :: int"                   ("1")
  2160   "uminus :: int => int"       ("~")
  2161   "op + :: int => int => int"  ("(_ +/ _)")
  2162   "op * :: int => int => int"  ("(_ */ _)")
  2163   "op \<le> :: int => int => bool" ("(_ <=/ _)")
  2164   "op < :: int => int => bool" ("(_ </ _)")
  2165 
  2166 quickcheck_params [default_type = int]
  2167 
  2168 hide (open) const Pls Min Bit0 Bit1 succ pred
  2169 
  2170 
  2171 subsection {* Legacy theorems *}
  2172 
  2173 lemmas zminus_zminus = minus_minus [of "z::int", standard]
  2174 lemmas zminus_0 = minus_zero [where 'a=int]
  2175 lemmas zminus_zadd_distrib = minus_add_distrib [of "z::int" "w", standard]
  2176 lemmas zadd_commute = add_commute [of "z::int" "w", standard]
  2177 lemmas zadd_assoc = add_assoc [of "z1::int" "z2" "z3", standard]
  2178 lemmas zadd_left_commute = add_left_commute [of "x::int" "y" "z", standard]
  2179 lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute
  2180 lemmas zmult_ac = OrderedGroup.mult_ac
  2181 lemmas zadd_0 = OrderedGroup.add_0_left [of "z::int", standard]
  2182 lemmas zadd_0_right = OrderedGroup.add_0_left [of "z::int", standard]
  2183 lemmas zadd_zminus_inverse2 = left_minus [of "z::int", standard]
  2184 lemmas zmult_zminus = mult_minus_left [of "z::int" "w", standard]
  2185 lemmas zmult_commute = mult_commute [of "z::int" "w", standard]
  2186 lemmas zmult_assoc = mult_assoc [of "z1::int" "z2" "z3", standard]
  2187 lemmas zadd_zmult_distrib = left_distrib [of "z1::int" "z2" "w", standard]
  2188 lemmas zadd_zmult_distrib2 = right_distrib [of "w::int" "z1" "z2", standard]
  2189 lemmas zdiff_zmult_distrib = left_diff_distrib [of "z1::int" "z2" "w", standard]
  2190 lemmas zdiff_zmult_distrib2 = right_diff_distrib [of "w::int" "z1" "z2", standard]
  2191 
  2192 lemmas zmult_1 = mult_1_left [of "z::int", standard]
  2193 lemmas zmult_1_right = mult_1_right [of "z::int", standard]
  2194 
  2195 lemmas zle_refl = order_refl [of "w::int", standard]
  2196 lemmas zle_trans = order_trans [where 'a=int and x="i" and y="j" and z="k", standard]
  2197 lemmas zle_anti_sym = order_antisym [of "z::int" "w", standard]
  2198 lemmas zle_linear = linorder_linear [of "z::int" "w", standard]
  2199 lemmas zless_linear = linorder_less_linear [where 'a = int]
  2200 
  2201 lemmas zadd_left_mono = add_left_mono [of "i::int" "j" "k", standard]
  2202 lemmas zadd_strict_right_mono = add_strict_right_mono [of "i::int" "j" "k", standard]
  2203 lemmas zadd_zless_mono = add_less_le_mono [of "w'::int" "w" "z'" "z", standard]
  2204 
  2205 lemmas int_0_less_1 = zero_less_one [where 'a=int]
  2206 lemmas int_0_neq_1 = zero_neq_one [where 'a=int]
  2207 
  2208 lemmas inj_int = inj_of_nat [where 'a=int]
  2209 lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
  2210 lemmas int_mult = of_nat_mult [where 'a=int]
  2211 lemmas zmult_int = of_nat_mult [where 'a=int, symmetric]
  2212 lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="n", standard]
  2213 lemmas zless_int = of_nat_less_iff [where 'a=int]
  2214 lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="k", standard]
  2215 lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int]
  2216 lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
  2217 lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="n", standard]
  2218 lemmas int_0 = of_nat_0 [where 'a=int]
  2219 lemmas int_1 = of_nat_1 [where 'a=int]
  2220 lemmas int_Suc = of_nat_Suc [where 'a=int]
  2221 lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m", standard]
  2222 lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
  2223 lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
  2224 lemmas zless_le = less_int_def
  2225 lemmas int_eq_of_nat = TrueI
  2226 
  2227 end