src/HOL/Int.thy
author haftmann
Wed Dec 03 15:58:44 2008 +0100 (2008-12-03)
changeset 28952 15a4b2cf8c34
parent 28724 4656aacba2bc
child 28958 74c60b78969c
permissions -rw-r--r--
made repository layout more coherent with logical distribution structure; stripped some $Id$s
     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 definition
   585   Pls :: int where
   586   [code del]: "Pls = 0"
   587 
   588 definition
   589   Min :: int where
   590   [code del]: "Min = - 1"
   591 
   592 definition
   593   Bit0 :: "int \<Rightarrow> int" where
   594   [code del]: "Bit0 k = k + k"
   595 
   596 definition
   597   Bit1 :: "int \<Rightarrow> int" where
   598   [code del]: "Bit1 k = 1 + k + k"
   599 
   600 class number = type + -- {* for numeric types: nat, int, real, \dots *}
   601   fixes number_of :: "int \<Rightarrow> 'a"
   602 
   603 use "Tools/numeral.ML"
   604 
   605 syntax
   606   "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")
   607 
   608 use "Tools/numeral_syntax.ML"
   609 setup NumeralSyntax.setup
   610 
   611 abbreviation
   612   "Numeral0 \<equiv> number_of Pls"
   613 
   614 abbreviation
   615   "Numeral1 \<equiv> number_of (Bit1 Pls)"
   616 
   617 lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"
   618   -- {* Unfold all @{text let}s involving constants *}
   619   unfolding Let_def ..
   620 
   621 definition
   622   succ :: "int \<Rightarrow> int" where
   623   [code del]: "succ k = k + 1"
   624 
   625 definition
   626   pred :: "int \<Rightarrow> int" where
   627   [code del]: "pred k = k - 1"
   628 
   629 lemmas
   630   max_number_of [simp] = max_def
   631     [of "number_of u" "number_of v", standard, simp]
   632 and
   633   min_number_of [simp] = min_def 
   634     [of "number_of u" "number_of v", standard, simp]
   635   -- {* unfolding @{text minx} and @{text max} on numerals *}
   636 
   637 lemmas numeral_simps = 
   638   succ_def pred_def Pls_def Min_def Bit0_def Bit1_def
   639 
   640 text {* Removal of leading zeroes *}
   641 
   642 lemma Bit0_Pls [simp, code post]:
   643   "Bit0 Pls = Pls"
   644   unfolding numeral_simps by simp
   645 
   646 lemma Bit1_Min [simp, code post]:
   647   "Bit1 Min = Min"
   648   unfolding numeral_simps by simp
   649 
   650 lemmas normalize_bin_simps =
   651   Bit0_Pls Bit1_Min
   652 
   653 
   654 subsection {* The Functions @{term succ}, @{term pred} and @{term uminus} *}
   655 
   656 lemma succ_Pls [simp]:
   657   "succ Pls = Bit1 Pls"
   658   unfolding numeral_simps by simp
   659 
   660 lemma succ_Min [simp]:
   661   "succ Min = Pls"
   662   unfolding numeral_simps by simp
   663 
   664 lemma succ_Bit0 [simp]:
   665   "succ (Bit0 k) = Bit1 k"
   666   unfolding numeral_simps by simp
   667 
   668 lemma succ_Bit1 [simp]:
   669   "succ (Bit1 k) = Bit0 (succ k)"
   670   unfolding numeral_simps by simp
   671 
   672 lemmas succ_bin_simps =
   673   succ_Pls succ_Min succ_Bit0 succ_Bit1
   674 
   675 lemma pred_Pls [simp]:
   676   "pred Pls = Min"
   677   unfolding numeral_simps by simp
   678 
   679 lemma pred_Min [simp]:
   680   "pred Min = Bit0 Min"
   681   unfolding numeral_simps by simp
   682 
   683 lemma pred_Bit0 [simp]:
   684   "pred (Bit0 k) = Bit1 (pred k)"
   685   unfolding numeral_simps by simp 
   686 
   687 lemma pred_Bit1 [simp]:
   688   "pred (Bit1 k) = Bit0 k"
   689   unfolding numeral_simps by simp
   690 
   691 lemmas pred_bin_simps =
   692   pred_Pls pred_Min pred_Bit0 pred_Bit1
   693 
   694 lemma minus_Pls [simp]:
   695   "- Pls = Pls"
   696   unfolding numeral_simps by simp 
   697 
   698 lemma minus_Min [simp]:
   699   "- Min = Bit1 Pls"
   700   unfolding numeral_simps by simp 
   701 
   702 lemma minus_Bit0 [simp]:
   703   "- (Bit0 k) = Bit0 (- k)"
   704   unfolding numeral_simps by simp 
   705 
   706 lemma minus_Bit1 [simp]:
   707   "- (Bit1 k) = Bit1 (pred (- k))"
   708   unfolding numeral_simps by simp
   709 
   710 lemmas minus_bin_simps =
   711   minus_Pls minus_Min minus_Bit0 minus_Bit1
   712 
   713 
   714 subsection {*
   715   Binary Addition and Multiplication: @{term "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"}
   716     and @{term "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"}
   717 *}
   718 
   719 lemma add_Pls [simp]:
   720   "Pls + k = k"
   721   unfolding numeral_simps by simp 
   722 
   723 lemma add_Min [simp]:
   724   "Min + k = pred k"
   725   unfolding numeral_simps by simp
   726 
   727 lemma add_Bit0_Bit0 [simp]:
   728   "(Bit0 k) + (Bit0 l) = Bit0 (k + l)"
   729   unfolding numeral_simps by simp_all 
   730 
   731 lemma add_Bit0_Bit1 [simp]:
   732   "(Bit0 k) + (Bit1 l) = Bit1 (k + l)"
   733   unfolding numeral_simps by simp_all 
   734 
   735 lemma add_Bit1_Bit0 [simp]:
   736   "(Bit1 k) + (Bit0 l) = Bit1 (k + l)"
   737   unfolding numeral_simps by simp
   738 
   739 lemma add_Bit1_Bit1 [simp]:
   740   "(Bit1 k) + (Bit1 l) = Bit0 (k + succ l)"
   741   unfolding numeral_simps by simp
   742 
   743 lemma add_Pls_right [simp]:
   744   "k + Pls = k"
   745   unfolding numeral_simps by simp 
   746 
   747 lemma add_Min_right [simp]:
   748   "k + Min = pred k"
   749   unfolding numeral_simps by simp
   750 
   751 lemmas add_bin_simps =
   752   add_Pls add_Min add_Pls_right add_Min_right
   753   add_Bit0_Bit0 add_Bit0_Bit1 add_Bit1_Bit0 add_Bit1_Bit1
   754 
   755 lemma mult_Pls [simp]:
   756   "Pls * w = Pls"
   757   unfolding numeral_simps by simp 
   758 
   759 lemma mult_Min [simp]:
   760   "Min * k = - k"
   761   unfolding numeral_simps by simp
   762 
   763 lemma mult_Bit0 [simp]:
   764   "(Bit0 k) * l = Bit0 (k * l)"
   765   unfolding numeral_simps int_distrib by simp
   766 
   767 lemma mult_Bit1 [simp]:
   768   "(Bit1 k) * l = (Bit0 (k * l)) + l"
   769   unfolding numeral_simps int_distrib by simp 
   770 
   771 lemmas mult_bin_simps =
   772   mult_Pls mult_Min mult_Bit0 mult_Bit1
   773 
   774 
   775 subsection {* Converting Numerals to Rings: @{term number_of} *}
   776 
   777 class number_ring = number + comm_ring_1 +
   778   assumes number_of_eq: "number_of k = of_int k"
   779 
   780 text {* self-embedding of the integers *}
   781 
   782 instantiation int :: number_ring
   783 begin
   784 
   785 definition int_number_of_def [code del]:
   786   "number_of w = (of_int w \<Colon> int)"
   787 
   788 instance proof
   789 qed (simp only: int_number_of_def)
   790 
   791 end
   792 
   793 lemma number_of_is_id:
   794   "number_of (k::int) = k"
   795   unfolding int_number_of_def by simp
   796 
   797 lemma number_of_succ:
   798   "number_of (succ k) = (1 + number_of k ::'a::number_ring)"
   799   unfolding number_of_eq numeral_simps by simp
   800 
   801 lemma number_of_pred:
   802   "number_of (pred w) = (- 1 + number_of w ::'a::number_ring)"
   803   unfolding number_of_eq numeral_simps by simp
   804 
   805 lemma number_of_minus:
   806   "number_of (uminus w) = (- (number_of w)::'a::number_ring)"
   807   unfolding number_of_eq numeral_simps by simp
   808 
   809 lemma number_of_add:
   810   "number_of (v + w) = (number_of v + number_of w::'a::number_ring)"
   811   unfolding number_of_eq numeral_simps by simp
   812 
   813 lemma number_of_mult:
   814   "number_of (v * w) = (number_of v * number_of w::'a::number_ring)"
   815   unfolding number_of_eq numeral_simps by simp
   816 
   817 text {*
   818   The correctness of shifting.
   819   But it doesn't seem to give a measurable speed-up.
   820 *}
   821 
   822 lemma double_number_of_Bit0:
   823   "(1 + 1) * number_of w = (number_of (Bit0 w) ::'a::number_ring)"
   824   unfolding number_of_eq numeral_simps left_distrib by simp
   825 
   826 text {*
   827   Converting numerals 0 and 1 to their abstract versions.
   828 *}
   829 
   830 lemma numeral_0_eq_0 [simp]:
   831   "Numeral0 = (0::'a::number_ring)"
   832   unfolding number_of_eq numeral_simps by simp
   833 
   834 lemma numeral_1_eq_1 [simp]:
   835   "Numeral1 = (1::'a::number_ring)"
   836   unfolding number_of_eq numeral_simps by simp
   837 
   838 text {*
   839   Special-case simplification for small constants.
   840 *}
   841 
   842 text{*
   843   Unary minus for the abstract constant 1. Cannot be inserted
   844   as a simprule until later: it is @{text number_of_Min} re-oriented!
   845 *}
   846 
   847 lemma numeral_m1_eq_minus_1:
   848   "(-1::'a::number_ring) = - 1"
   849   unfolding number_of_eq numeral_simps by simp
   850 
   851 lemma mult_minus1 [simp]:
   852   "-1 * z = -(z::'a::number_ring)"
   853   unfolding number_of_eq numeral_simps by simp
   854 
   855 lemma mult_minus1_right [simp]:
   856   "z * -1 = -(z::'a::number_ring)"
   857   unfolding number_of_eq numeral_simps by simp
   858 
   859 (*Negation of a coefficient*)
   860 lemma minus_number_of_mult [simp]:
   861    "- (number_of w) * z = number_of (uminus w) * (z::'a::number_ring)"
   862    unfolding number_of_eq by simp
   863 
   864 text {* Subtraction *}
   865 
   866 lemma diff_number_of_eq:
   867   "number_of v - number_of w =
   868     (number_of (v + uminus w)::'a::number_ring)"
   869   unfolding number_of_eq by simp
   870 
   871 lemma number_of_Pls:
   872   "number_of Pls = (0::'a::number_ring)"
   873   unfolding number_of_eq numeral_simps by simp
   874 
   875 lemma number_of_Min:
   876   "number_of Min = (- 1::'a::number_ring)"
   877   unfolding number_of_eq numeral_simps by simp
   878 
   879 lemma number_of_Bit0:
   880   "number_of (Bit0 w) = (0::'a::number_ring) + (number_of w) + (number_of w)"
   881   unfolding number_of_eq numeral_simps by simp
   882 
   883 lemma number_of_Bit1:
   884   "number_of (Bit1 w) = (1::'a::number_ring) + (number_of w) + (number_of w)"
   885   unfolding number_of_eq numeral_simps by simp
   886 
   887 
   888 subsection {* Equality of Binary Numbers *}
   889 
   890 text {* First version by Norbert Voelker *}
   891 
   892 definition
   893   neg  :: "'a\<Colon>ordered_idom \<Rightarrow> bool"
   894 where
   895   "neg Z \<longleftrightarrow> Z < 0"
   896 
   897 definition (*for simplifying equalities*)
   898   iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool"
   899 where
   900   "iszero z \<longleftrightarrow> z = 0"
   901 
   902 lemma not_neg_int [simp]: "~ neg (of_nat n)"
   903 by (simp add: neg_def)
   904 
   905 lemma neg_zminus_int [simp]: "neg (- (of_nat (Suc n)))"
   906 by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc)
   907 
   908 lemmas neg_eq_less_0 = neg_def
   909 
   910 lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)"
   911 by (simp add: neg_def linorder_not_less)
   912 
   913 text{*To simplify inequalities when Numeral1 can get simplified to 1*}
   914 
   915 lemma not_neg_0: "~ neg 0"
   916 by (simp add: One_int_def neg_def)
   917 
   918 lemma not_neg_1: "~ neg 1"
   919 by (simp add: neg_def linorder_not_less zero_le_one)
   920 
   921 lemma iszero_0: "iszero 0"
   922 by (simp add: iszero_def)
   923 
   924 lemma not_iszero_1: "~ iszero 1"
   925 by (simp add: iszero_def eq_commute)
   926 
   927 lemma neg_nat: "neg z ==> nat z = 0"
   928 by (simp add: neg_def order_less_imp_le) 
   929 
   930 lemma not_neg_nat: "~ neg z ==> of_nat (nat z) = z"
   931 by (simp add: linorder_not_less neg_def)
   932 
   933 lemma eq_number_of_eq:
   934   "((number_of x::'a::number_ring) = number_of y) =
   935    iszero (number_of (x + uminus y) :: 'a)"
   936   unfolding iszero_def number_of_add number_of_minus
   937   by (simp add: compare_rls)
   938 
   939 lemma iszero_number_of_Pls:
   940   "iszero ((number_of Pls)::'a::number_ring)"
   941   unfolding iszero_def numeral_0_eq_0 ..
   942 
   943 lemma nonzero_number_of_Min:
   944   "~ iszero ((number_of Min)::'a::number_ring)"
   945   unfolding iszero_def numeral_m1_eq_minus_1 by simp
   946 
   947 
   948 subsection {* Comparisons, for Ordered Rings *}
   949 
   950 lemmas double_eq_0_iff = double_zero
   951 
   952 lemma le_imp_0_less: 
   953   assumes le: "0 \<le> z"
   954   shows "(0::int) < 1 + z"
   955 proof -
   956   have "0 \<le> z" by fact
   957   also have "... < z + 1" by (rule less_add_one) 
   958   also have "... = 1 + z" by (simp add: add_ac)
   959   finally show "0 < 1 + z" .
   960 qed
   961 
   962 lemma odd_nonzero:
   963   "1 + z + z \<noteq> (0::int)";
   964 proof (cases z rule: int_cases)
   965   case (nonneg n)
   966   have le: "0 \<le> z+z" by (simp add: nonneg add_increasing) 
   967   thus ?thesis using  le_imp_0_less [OF le]
   968     by (auto simp add: add_assoc) 
   969 next
   970   case (neg n)
   971   show ?thesis
   972   proof
   973     assume eq: "1 + z + z = 0"
   974     have "(0::int) < 1 + (of_nat n + of_nat n)"
   975       by (simp add: le_imp_0_less add_increasing) 
   976     also have "... = - (1 + z + z)" 
   977       by (simp add: neg add_assoc [symmetric]) 
   978     also have "... = 0" by (simp add: eq) 
   979     finally have "0<0" ..
   980     thus False by blast
   981   qed
   982 qed
   983 
   984 lemma iszero_number_of_Bit0:
   985   "iszero (number_of (Bit0 w)::'a) = 
   986    iszero (number_of w::'a::{ring_char_0,number_ring})"
   987 proof -
   988   have "(of_int w + of_int w = (0::'a)) \<Longrightarrow> (w = 0)"
   989   proof -
   990     assume eq: "of_int w + of_int w = (0::'a)"
   991     then have "of_int (w + w) = (of_int 0 :: 'a)" by simp
   992     then have "w + w = 0" by (simp only: of_int_eq_iff)
   993     then show "w = 0" by (simp only: double_eq_0_iff)
   994   qed
   995   thus ?thesis
   996     by (auto simp add: iszero_def number_of_eq numeral_simps)
   997 qed
   998 
   999 lemma iszero_number_of_Bit1:
  1000   "~ iszero (number_of (Bit1 w)::'a::{ring_char_0,number_ring})"
  1001 proof -
  1002   have "1 + of_int w + of_int w \<noteq> (0::'a)"
  1003   proof
  1004     assume eq: "1 + of_int w + of_int w = (0::'a)"
  1005     hence "of_int (1 + w + w) = (of_int 0 :: 'a)" by simp 
  1006     hence "1 + w + w = 0" by (simp only: of_int_eq_iff)
  1007     with odd_nonzero show False by blast
  1008   qed
  1009   thus ?thesis
  1010     by (auto simp add: iszero_def number_of_eq numeral_simps)
  1011 qed
  1012 
  1013 
  1014 subsection {* The Less-Than Relation *}
  1015 
  1016 lemma less_number_of_eq_neg:
  1017   "((number_of x::'a::{ordered_idom,number_ring}) < number_of y)
  1018   = neg (number_of (x + uminus y) :: 'a)"
  1019 apply (subst less_iff_diff_less_0) 
  1020 apply (simp add: neg_def diff_minus number_of_add number_of_minus)
  1021 done
  1022 
  1023 text {*
  1024   If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
  1025   @{term Numeral0} IS @{term "number_of Pls"}
  1026 *}
  1027 
  1028 lemma not_neg_number_of_Pls:
  1029   "~ neg (number_of Pls ::'a::{ordered_idom,number_ring})"
  1030   by (simp add: neg_def numeral_0_eq_0)
  1031 
  1032 lemma neg_number_of_Min:
  1033   "neg (number_of Min ::'a::{ordered_idom,number_ring})"
  1034   by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)
  1035 
  1036 lemma double_less_0_iff:
  1037   "(a + a < 0) = (a < (0::'a::ordered_idom))"
  1038 proof -
  1039   have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)
  1040   also have "... = (a < 0)"
  1041     by (simp add: mult_less_0_iff zero_less_two 
  1042                   order_less_not_sym [OF zero_less_two]) 
  1043   finally show ?thesis .
  1044 qed
  1045 
  1046 lemma odd_less_0:
  1047   "(1 + z + z < 0) = (z < (0::int))";
  1048 proof (cases z rule: int_cases)
  1049   case (nonneg n)
  1050   thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
  1051                              le_imp_0_less [THEN order_less_imp_le])  
  1052 next
  1053   case (neg n)
  1054   thus ?thesis by (simp del: of_nat_Suc of_nat_add
  1055     add: compare_rls of_nat_1 [symmetric] of_nat_add [symmetric])
  1056 qed
  1057 
  1058 lemma neg_number_of_Bit0:
  1059   "neg (number_of (Bit0 w)::'a) = 
  1060   neg (number_of w :: 'a::{ordered_idom,number_ring})"
  1061 by (simp add: neg_def number_of_eq numeral_simps double_less_0_iff)
  1062 
  1063 lemma neg_number_of_Bit1:
  1064   "neg (number_of (Bit1 w)::'a) = 
  1065   neg (number_of w :: 'a::{ordered_idom,number_ring})"
  1066 proof -
  1067   have "((1::'a) + of_int w + of_int w < 0) = (of_int (1 + w + w) < (of_int 0 :: 'a))"
  1068     by simp
  1069   also have "... = (w < 0)" by (simp only: of_int_less_iff odd_less_0)
  1070   finally show ?thesis
  1071   by (simp add: neg_def number_of_eq numeral_simps)
  1072 qed
  1073 
  1074 
  1075 text {* Less-Than or Equals *}
  1076 
  1077 text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *}
  1078 
  1079 lemmas le_number_of_eq_not_less =
  1080   linorder_not_less [of "number_of w" "number_of v", symmetric, 
  1081   standard]
  1082 
  1083 lemma le_number_of_eq:
  1084     "((number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y)
  1085      = (~ (neg (number_of (y + uminus x) :: 'a)))"
  1086 by (simp add: le_number_of_eq_not_less less_number_of_eq_neg)
  1087 
  1088 
  1089 text {* Absolute value (@{term abs}) *}
  1090 
  1091 lemma abs_number_of:
  1092   "abs(number_of x::'a::{ordered_idom,number_ring}) =
  1093    (if number_of x < (0::'a) then -number_of x else number_of x)"
  1094   by (simp add: abs_if)
  1095 
  1096 
  1097 text {* Re-orientation of the equation nnn=x *}
  1098 
  1099 lemma number_of_reorient:
  1100   "(number_of w = x) = (x = number_of w)"
  1101   by auto
  1102 
  1103 
  1104 subsection {* Simplification of arithmetic operations on integer constants. *}
  1105 
  1106 lemmas arith_extra_simps [standard, simp] =
  1107   number_of_add [symmetric]
  1108   number_of_minus [symmetric] numeral_m1_eq_minus_1 [symmetric]
  1109   number_of_mult [symmetric]
  1110   diff_number_of_eq abs_number_of 
  1111 
  1112 text {*
  1113   For making a minimal simpset, one must include these default simprules.
  1114   Also include @{text simp_thms}.
  1115 *}
  1116 
  1117 lemmas arith_simps = 
  1118   normalize_bin_simps pred_bin_simps succ_bin_simps
  1119   add_bin_simps minus_bin_simps mult_bin_simps
  1120   abs_zero abs_one arith_extra_simps
  1121 
  1122 text {* Simplification of relational operations *}
  1123 
  1124 lemmas rel_simps [simp] = 
  1125   eq_number_of_eq iszero_0 nonzero_number_of_Min
  1126   iszero_number_of_Bit0 iszero_number_of_Bit1
  1127   less_number_of_eq_neg
  1128   not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1
  1129   neg_number_of_Min neg_number_of_Bit0 neg_number_of_Bit1
  1130   le_number_of_eq
  1131 (* iszero_number_of_Pls would never be used
  1132    because its lhs simplifies to "iszero 0" *)
  1133 
  1134 
  1135 subsection {* Simplification of arithmetic when nested to the right. *}
  1136 
  1137 lemma add_number_of_left [simp]:
  1138   "number_of v + (number_of w + z) =
  1139    (number_of(v + w) + z::'a::number_ring)"
  1140   by (simp add: add_assoc [symmetric])
  1141 
  1142 lemma mult_number_of_left [simp]:
  1143   "number_of v * (number_of w * z) =
  1144    (number_of(v * w) * z::'a::number_ring)"
  1145   by (simp add: mult_assoc [symmetric])
  1146 
  1147 lemma add_number_of_diff1:
  1148   "number_of v + (number_of w - c) = 
  1149   number_of(v + w) - (c::'a::number_ring)"
  1150   by (simp add: diff_minus add_number_of_left)
  1151 
  1152 lemma add_number_of_diff2 [simp]:
  1153   "number_of v + (c - number_of w) =
  1154    number_of (v + uminus w) + (c::'a::number_ring)"
  1155 apply (subst diff_number_of_eq [symmetric])
  1156 apply (simp only: compare_rls)
  1157 done
  1158 
  1159 
  1160 subsection {* The Set of Integers *}
  1161 
  1162 context ring_1
  1163 begin
  1164 
  1165 definition
  1166   Ints  :: "'a set"
  1167 where
  1168   [code del]: "Ints = range of_int"
  1169 
  1170 end
  1171 
  1172 notation (xsymbols)
  1173   Ints  ("\<int>")
  1174 
  1175 context ring_1
  1176 begin
  1177 
  1178 lemma Ints_0 [simp]: "0 \<in> \<int>"
  1179 apply (simp add: Ints_def)
  1180 apply (rule range_eqI)
  1181 apply (rule of_int_0 [symmetric])
  1182 done
  1183 
  1184 lemma Ints_1 [simp]: "1 \<in> \<int>"
  1185 apply (simp add: Ints_def)
  1186 apply (rule range_eqI)
  1187 apply (rule of_int_1 [symmetric])
  1188 done
  1189 
  1190 lemma Ints_add [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a + b \<in> \<int>"
  1191 apply (auto simp add: Ints_def)
  1192 apply (rule range_eqI)
  1193 apply (rule of_int_add [symmetric])
  1194 done
  1195 
  1196 lemma Ints_minus [simp]: "a \<in> \<int> \<Longrightarrow> -a \<in> \<int>"
  1197 apply (auto simp add: Ints_def)
  1198 apply (rule range_eqI)
  1199 apply (rule of_int_minus [symmetric])
  1200 done
  1201 
  1202 lemma Ints_mult [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a * b \<in> \<int>"
  1203 apply (auto simp add: Ints_def)
  1204 apply (rule range_eqI)
  1205 apply (rule of_int_mult [symmetric])
  1206 done
  1207 
  1208 lemma Ints_cases [cases set: Ints]:
  1209   assumes "q \<in> \<int>"
  1210   obtains (of_int) z where "q = of_int z"
  1211   unfolding Ints_def
  1212 proof -
  1213   from `q \<in> \<int>` have "q \<in> range of_int" unfolding Ints_def .
  1214   then obtain z where "q = of_int z" ..
  1215   then show thesis ..
  1216 qed
  1217 
  1218 lemma Ints_induct [case_names of_int, induct set: Ints]:
  1219   "q \<in> \<int> \<Longrightarrow> (\<And>z. P (of_int z)) \<Longrightarrow> P q"
  1220   by (rule Ints_cases) auto
  1221 
  1222 end
  1223 
  1224 lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a-b \<in> \<int>"
  1225 apply (auto simp add: Ints_def)
  1226 apply (rule range_eqI)
  1227 apply (rule of_int_diff [symmetric])
  1228 done
  1229 
  1230 text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
  1231 
  1232 lemma Ints_double_eq_0_iff:
  1233   assumes in_Ints: "a \<in> Ints"
  1234   shows "(a + a = 0) = (a = (0::'a::ring_char_0))"
  1235 proof -
  1236   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
  1237   then obtain z where a: "a = of_int z" ..
  1238   show ?thesis
  1239   proof
  1240     assume "a = 0"
  1241     thus "a + a = 0" by simp
  1242   next
  1243     assume eq: "a + a = 0"
  1244     hence "of_int (z + z) = (of_int 0 :: 'a)" by (simp add: a)
  1245     hence "z + z = 0" by (simp only: of_int_eq_iff)
  1246     hence "z = 0" by (simp only: double_eq_0_iff)
  1247     thus "a = 0" by (simp add: a)
  1248   qed
  1249 qed
  1250 
  1251 lemma Ints_odd_nonzero:
  1252   assumes in_Ints: "a \<in> Ints"
  1253   shows "1 + a + a \<noteq> (0::'a::ring_char_0)"
  1254 proof -
  1255   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
  1256   then obtain z where a: "a = of_int z" ..
  1257   show ?thesis
  1258   proof
  1259     assume eq: "1 + a + a = 0"
  1260     hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
  1261     hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
  1262     with odd_nonzero show False by blast
  1263   qed
  1264 qed 
  1265 
  1266 lemma Ints_number_of:
  1267   "(number_of w :: 'a::number_ring) \<in> Ints"
  1268   unfolding number_of_eq Ints_def by simp
  1269 
  1270 lemma Ints_odd_less_0: 
  1271   assumes in_Ints: "a \<in> Ints"
  1272   shows "(1 + a + a < 0) = (a < (0::'a::ordered_idom))";
  1273 proof -
  1274   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
  1275   then obtain z where a: "a = of_int z" ..
  1276   hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
  1277     by (simp add: a)
  1278   also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0)
  1279   also have "... = (a < 0)" by (simp add: a)
  1280   finally show ?thesis .
  1281 qed
  1282 
  1283 
  1284 subsection {* @{term setsum} and @{term setprod} *}
  1285 
  1286 text {*By Jeremy Avigad*}
  1287 
  1288 lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
  1289   apply (cases "finite A")
  1290   apply (erule finite_induct, auto)
  1291   done
  1292 
  1293 lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
  1294   apply (cases "finite A")
  1295   apply (erule finite_induct, auto)
  1296   done
  1297 
  1298 lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
  1299   apply (cases "finite A")
  1300   apply (erule finite_induct, auto simp add: of_nat_mult)
  1301   done
  1302 
  1303 lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
  1304   apply (cases "finite A")
  1305   apply (erule finite_induct, auto)
  1306   done
  1307 
  1308 lemma setprod_nonzero_nat:
  1309     "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0"
  1310   by (rule setprod_nonzero, auto)
  1311 
  1312 lemma setprod_zero_eq_nat:
  1313     "finite A ==> (setprod f A = (0::nat)) = (\<exists>x \<in> A. f x = 0)"
  1314   by (rule setprod_zero_eq, auto)
  1315 
  1316 lemma setprod_nonzero_int:
  1317     "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::int)) ==> setprod f A \<noteq> 0"
  1318   by (rule setprod_nonzero, auto)
  1319 
  1320 lemma setprod_zero_eq_int:
  1321     "finite A ==> (setprod f A = (0::int)) = (\<exists>x \<in> A. f x = 0)"
  1322   by (rule setprod_zero_eq, auto)
  1323 
  1324 lemmas int_setsum = of_nat_setsum [where 'a=int]
  1325 lemmas int_setprod = of_nat_setprod [where 'a=int]
  1326 
  1327 
  1328 subsection{*Inequality Reasoning for the Arithmetic Simproc*}
  1329 
  1330 lemma add_numeral_0: "Numeral0 + a = (a::'a::number_ring)"
  1331 by simp 
  1332 
  1333 lemma add_numeral_0_right: "a + Numeral0 = (a::'a::number_ring)"
  1334 by simp
  1335 
  1336 lemma mult_numeral_1: "Numeral1 * a = (a::'a::number_ring)"
  1337 by simp 
  1338 
  1339 lemma mult_numeral_1_right: "a * Numeral1 = (a::'a::number_ring)"
  1340 by simp
  1341 
  1342 lemma divide_numeral_1: "a / Numeral1 = (a::'a::{number_ring,field})"
  1343 by simp
  1344 
  1345 lemma inverse_numeral_1:
  1346   "inverse Numeral1 = (Numeral1::'a::{number_ring,field})"
  1347 by simp
  1348 
  1349 text{*Theorem lists for the cancellation simprocs. The use of binary numerals
  1350 for 0 and 1 reduces the number of special cases.*}
  1351 
  1352 lemmas add_0s = add_numeral_0 add_numeral_0_right
  1353 lemmas mult_1s = mult_numeral_1 mult_numeral_1_right 
  1354                  mult_minus1 mult_minus1_right
  1355 
  1356 
  1357 subsection{*Special Arithmetic Rules for Abstract 0 and 1*}
  1358 
  1359 text{*Arithmetic computations are defined for binary literals, which leaves 0
  1360 and 1 as special cases. Addition already has rules for 0, but not 1.
  1361 Multiplication and unary minus already have rules for both 0 and 1.*}
  1362 
  1363 
  1364 lemma binop_eq: "[|f x y = g x y; x = x'; y = y'|] ==> f x' y' = g x' y'"
  1365 by simp
  1366 
  1367 
  1368 lemmas add_number_of_eq = number_of_add [symmetric]
  1369 
  1370 text{*Allow 1 on either or both sides*}
  1371 lemma one_add_one_is_two: "1 + 1 = (2::'a::number_ring)"
  1372 by (simp del: numeral_1_eq_1 add: numeral_1_eq_1 [symmetric] add_number_of_eq)
  1373 
  1374 lemmas add_special =
  1375     one_add_one_is_two
  1376     binop_eq [of "op +", OF add_number_of_eq numeral_1_eq_1 refl, standard]
  1377     binop_eq [of "op +", OF add_number_of_eq refl numeral_1_eq_1, standard]
  1378 
  1379 text{*Allow 1 on either or both sides (1-1 already simplifies to 0)*}
  1380 lemmas diff_special =
  1381     binop_eq [of "op -", OF diff_number_of_eq numeral_1_eq_1 refl, standard]
  1382     binop_eq [of "op -", OF diff_number_of_eq refl numeral_1_eq_1, standard]
  1383 
  1384 text{*Allow 0 or 1 on either side with a binary numeral on the other*}
  1385 lemmas eq_special =
  1386     binop_eq [of "op =", OF eq_number_of_eq numeral_0_eq_0 refl, standard]
  1387     binop_eq [of "op =", OF eq_number_of_eq numeral_1_eq_1 refl, standard]
  1388     binop_eq [of "op =", OF eq_number_of_eq refl numeral_0_eq_0, standard]
  1389     binop_eq [of "op =", OF eq_number_of_eq refl numeral_1_eq_1, standard]
  1390 
  1391 text{*Allow 0 or 1 on either side with a binary numeral on the other*}
  1392 lemmas less_special =
  1393   binop_eq [of "op <", OF less_number_of_eq_neg numeral_0_eq_0 refl, standard]
  1394   binop_eq [of "op <", OF less_number_of_eq_neg numeral_1_eq_1 refl, standard]
  1395   binop_eq [of "op <", OF less_number_of_eq_neg refl numeral_0_eq_0, standard]
  1396   binop_eq [of "op <", OF less_number_of_eq_neg refl numeral_1_eq_1, standard]
  1397 
  1398 text{*Allow 0 or 1 on either side with a binary numeral on the other*}
  1399 lemmas le_special =
  1400     binop_eq [of "op \<le>", OF le_number_of_eq numeral_0_eq_0 refl, standard]
  1401     binop_eq [of "op \<le>", OF le_number_of_eq numeral_1_eq_1 refl, standard]
  1402     binop_eq [of "op \<le>", OF le_number_of_eq refl numeral_0_eq_0, standard]
  1403     binop_eq [of "op \<le>", OF le_number_of_eq refl numeral_1_eq_1, standard]
  1404 
  1405 lemmas arith_special[simp] = 
  1406        add_special diff_special eq_special less_special le_special
  1407 
  1408 
  1409 lemma min_max_01: "min (0::int) 1 = 0 & min (1::int) 0 = 0 &
  1410                    max (0::int) 1 = 1 & max (1::int) 0 = 1"
  1411 by(simp add:min_def max_def)
  1412 
  1413 lemmas min_max_special[simp] =
  1414  min_max_01
  1415  max_def[of "0::int" "number_of v", standard, simp]
  1416  min_def[of "0::int" "number_of v", standard, simp]
  1417  max_def[of "number_of u" "0::int", standard, simp]
  1418  min_def[of "number_of u" "0::int", standard, simp]
  1419  max_def[of "1::int" "number_of v", standard, simp]
  1420  min_def[of "1::int" "number_of v", standard, simp]
  1421  max_def[of "number_of u" "1::int", standard, simp]
  1422  min_def[of "number_of u" "1::int", standard, simp]
  1423 
  1424 text {* Legacy theorems *}
  1425 
  1426 lemmas zle_int = of_nat_le_iff [where 'a=int]
  1427 lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
  1428 
  1429 use "~~/src/Provers/Arith/assoc_fold.ML"
  1430 use "Tools/int_arith.ML"
  1431 declaration {* K int_arith_setup *}
  1432 
  1433 
  1434 subsection{*Lemmas About Small Numerals*}
  1435 
  1436 lemma of_int_m1 [simp]: "of_int -1 = (-1 :: 'a :: number_ring)"
  1437 proof -
  1438   have "(of_int -1 :: 'a) = of_int (- 1)" by simp
  1439   also have "... = - of_int 1" by (simp only: of_int_minus)
  1440   also have "... = -1" by simp
  1441   finally show ?thesis .
  1442 qed
  1443 
  1444 lemma abs_minus_one [simp]: "abs (-1) = (1::'a::{ordered_idom,number_ring})"
  1445 by (simp add: abs_if)
  1446 
  1447 lemma abs_power_minus_one [simp]:
  1448      "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring,recpower})"
  1449 by (simp add: power_abs)
  1450 
  1451 lemma of_int_number_of_eq:
  1452      "of_int (number_of v) = (number_of v :: 'a :: number_ring)"
  1453 by (simp add: number_of_eq) 
  1454 
  1455 text{*Lemmas for specialist use, NOT as default simprules*}
  1456 lemma mult_2: "2 * z = (z+z::'a::number_ring)"
  1457 proof -
  1458   have "2*z = (1 + 1)*z" by simp
  1459   also have "... = z+z" by (simp add: left_distrib)
  1460   finally show ?thesis .
  1461 qed
  1462 
  1463 lemma mult_2_right: "z * 2 = (z+z::'a::number_ring)"
  1464 by (subst mult_commute, rule mult_2)
  1465 
  1466 
  1467 subsection{*More Inequality Reasoning*}
  1468 
  1469 lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
  1470 by arith
  1471 
  1472 lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
  1473 by arith
  1474 
  1475 lemma zle_diff1_eq [simp]: "(w \<le> z - (1::int)) = (w<z)"
  1476 by arith
  1477 
  1478 lemma zle_add1_eq_le [simp]: "(w < z + (1::int)) = (w\<le>z)"
  1479 by arith
  1480 
  1481 lemma int_one_le_iff_zero_less: "((1::int) \<le> z) = (0 < z)"
  1482 by arith
  1483 
  1484 
  1485 subsection{*The Functions @{term nat} and @{term int}*}
  1486 
  1487 text{*Simplify the terms @{term "int 0"}, @{term "int(Suc 0)"} and
  1488   @{term "w + - z"}*}
  1489 declare Zero_int_def [symmetric, simp]
  1490 declare One_int_def [symmetric, simp]
  1491 
  1492 lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp]
  1493 
  1494 lemma nat_0: "nat 0 = 0"
  1495 by (simp add: nat_eq_iff)
  1496 
  1497 lemma nat_1: "nat 1 = Suc 0"
  1498 by (subst nat_eq_iff, simp)
  1499 
  1500 lemma nat_2: "nat 2 = Suc (Suc 0)"
  1501 by (subst nat_eq_iff, simp)
  1502 
  1503 lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
  1504 apply (insert zless_nat_conj [of 1 z])
  1505 apply (auto simp add: nat_1)
  1506 done
  1507 
  1508 text{*This simplifies expressions of the form @{term "int n = z"} where
  1509       z is an integer literal.*}
  1510 lemmas int_eq_iff_number_of [simp] = int_eq_iff [of _ "number_of v", standard]
  1511 
  1512 lemma split_nat [arith_split]:
  1513   "P(nat(i::int)) = ((\<forall>n. i = of_nat n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
  1514   (is "?P = (?L & ?R)")
  1515 proof (cases "i < 0")
  1516   case True thus ?thesis by auto
  1517 next
  1518   case False
  1519   have "?P = ?L"
  1520   proof
  1521     assume ?P thus ?L using False by clarsimp
  1522   next
  1523     assume ?L thus ?P using False by simp
  1524   qed
  1525   with False show ?thesis by simp
  1526 qed
  1527 
  1528 context ring_1
  1529 begin
  1530 
  1531 lemma of_int_of_nat:
  1532   "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))"
  1533 proof (cases "k < 0")
  1534   case True then have "0 \<le> - k" by simp
  1535   then have "of_nat (nat (- k)) = of_int (- k)" by (rule of_nat_nat)
  1536   with True show ?thesis by simp
  1537 next
  1538   case False then show ?thesis by (simp add: not_less of_nat_nat)
  1539 qed
  1540 
  1541 end
  1542 
  1543 lemma nat_mult_distrib:
  1544   fixes z z' :: int
  1545   assumes "0 \<le> z"
  1546   shows "nat (z * z') = nat z * nat z'"
  1547 proof (cases "0 \<le> z'")
  1548   case False with assms have "z * z' \<le> 0"
  1549     by (simp add: not_le mult_le_0_iff)
  1550   then have "nat (z * z') = 0" by simp
  1551   moreover from False have "nat z' = 0" by simp
  1552   ultimately show ?thesis by simp
  1553 next
  1554   case True with assms have ge_0: "z * z' \<ge> 0" by (simp add: zero_le_mult_iff)
  1555   show ?thesis
  1556     by (rule injD [of "of_nat :: nat \<Rightarrow> int", OF inj_of_nat])
  1557       (simp only: of_nat_mult of_nat_nat [OF True]
  1558          of_nat_nat [OF assms] of_nat_nat [OF ge_0], simp)
  1559 qed
  1560 
  1561 lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"
  1562 apply (rule trans)
  1563 apply (rule_tac [2] nat_mult_distrib, auto)
  1564 done
  1565 
  1566 lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
  1567 apply (cases "z=0 | w=0")
  1568 apply (auto simp add: abs_if nat_mult_distrib [symmetric] 
  1569                       nat_mult_distrib_neg [symmetric] mult_less_0_iff)
  1570 done
  1571 
  1572 
  1573 subsection "Induction principles for int"
  1574 
  1575 text{*Well-founded segments of the integers*}
  1576 
  1577 definition
  1578   int_ge_less_than  ::  "int => (int * int) set"
  1579 where
  1580   "int_ge_less_than d = {(z',z). d \<le> z' & z' < z}"
  1581 
  1582 theorem wf_int_ge_less_than: "wf (int_ge_less_than d)"
  1583 proof -
  1584   have "int_ge_less_than d \<subseteq> measure (%z. nat (z-d))"
  1585     by (auto simp add: int_ge_less_than_def)
  1586   thus ?thesis 
  1587     by (rule wf_subset [OF wf_measure]) 
  1588 qed
  1589 
  1590 text{*This variant looks odd, but is typical of the relations suggested
  1591 by RankFinder.*}
  1592 
  1593 definition
  1594   int_ge_less_than2 ::  "int => (int * int) set"
  1595 where
  1596   "int_ge_less_than2 d = {(z',z). d \<le> z & z' < z}"
  1597 
  1598 theorem wf_int_ge_less_than2: "wf (int_ge_less_than2 d)"
  1599 proof -
  1600   have "int_ge_less_than2 d \<subseteq> measure (%z. nat (1+z-d))" 
  1601     by (auto simp add: int_ge_less_than2_def)
  1602   thus ?thesis 
  1603     by (rule wf_subset [OF wf_measure]) 
  1604 qed
  1605 
  1606 abbreviation
  1607   int :: "nat \<Rightarrow> int"
  1608 where
  1609   "int \<equiv> of_nat"
  1610 
  1611 (* `set:int': dummy construction *)
  1612 theorem int_ge_induct [case_names base step, induct set: int]:
  1613   fixes i :: int
  1614   assumes ge: "k \<le> i" and
  1615     base: "P k" and
  1616     step: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
  1617   shows "P i"
  1618 proof -
  1619   { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i"
  1620     proof (induct n)
  1621       case 0
  1622       hence "i = k" by arith
  1623       thus "P i" using base by simp
  1624     next
  1625       case (Suc n)
  1626       then have "n = nat((i - 1) - k)" by arith
  1627       moreover
  1628       have ki1: "k \<le> i - 1" using Suc.prems by arith
  1629       ultimately
  1630       have "P(i - 1)" by(rule Suc.hyps)
  1631       from step[OF ki1 this] show ?case by simp
  1632     qed
  1633   }
  1634   with ge show ?thesis by fast
  1635 qed
  1636 
  1637 (* `set:int': dummy construction *)
  1638 theorem int_gr_induct [case_names base step, induct set: int]:
  1639   assumes gr: "k < (i::int)" and
  1640         base: "P(k+1)" and
  1641         step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
  1642   shows "P i"
  1643 apply(rule int_ge_induct[of "k + 1"])
  1644   using gr apply arith
  1645  apply(rule base)
  1646 apply (rule step, simp+)
  1647 done
  1648 
  1649 theorem int_le_induct[consumes 1,case_names base step]:
  1650   assumes le: "i \<le> (k::int)" and
  1651         base: "P(k)" and
  1652         step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
  1653   shows "P i"
  1654 proof -
  1655   { fix n have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i"
  1656     proof (induct n)
  1657       case 0
  1658       hence "i = k" by arith
  1659       thus "P i" using base by simp
  1660     next
  1661       case (Suc n)
  1662       hence "n = nat(k - (i+1))" by arith
  1663       moreover
  1664       have ki1: "i + 1 \<le> k" using Suc.prems by arith
  1665       ultimately
  1666       have "P(i+1)" by(rule Suc.hyps)
  1667       from step[OF ki1 this] show ?case by simp
  1668     qed
  1669   }
  1670   with le show ?thesis by fast
  1671 qed
  1672 
  1673 theorem int_less_induct [consumes 1,case_names base step]:
  1674   assumes less: "(i::int) < k" and
  1675         base: "P(k - 1)" and
  1676         step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
  1677   shows "P i"
  1678 apply(rule int_le_induct[of _ "k - 1"])
  1679   using less apply arith
  1680  apply(rule base)
  1681 apply (rule step, simp+)
  1682 done
  1683 
  1684 subsection{*Intermediate value theorems*}
  1685 
  1686 lemma int_val_lemma:
  1687      "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->  
  1688       f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
  1689 apply (induct n, simp)
  1690 apply (intro strip)
  1691 apply (erule impE, simp)
  1692 apply (erule_tac x = n in allE, simp)
  1693 apply (case_tac "k = f (n+1) ")
  1694 apply force
  1695 apply (erule impE)
  1696  apply (simp add: abs_if split add: split_if_asm)
  1697 apply (blast intro: le_SucI)
  1698 done
  1699 
  1700 lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
  1701 
  1702 lemma nat_intermed_int_val:
  1703      "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;  
  1704          f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
  1705 apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k 
  1706        in int_val_lemma)
  1707 apply simp
  1708 apply (erule exE)
  1709 apply (rule_tac x = "i+m" in exI, arith)
  1710 done
  1711 
  1712 
  1713 subsection{*Products and 1, by T. M. Rasmussen*}
  1714 
  1715 lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))"
  1716 by arith
  1717 
  1718 lemma abs_zmult_eq_1: "(\<bar>m * n\<bar> = 1) ==> \<bar>m\<bar> = (1::int)"
  1719 apply (cases "\<bar>n\<bar>=1") 
  1720 apply (simp add: abs_mult) 
  1721 apply (rule ccontr) 
  1722 apply (auto simp add: linorder_neq_iff abs_mult) 
  1723 apply (subgoal_tac "2 \<le> \<bar>m\<bar> & 2 \<le> \<bar>n\<bar>")
  1724  prefer 2 apply arith 
  1725 apply (subgoal_tac "2*2 \<le> \<bar>m\<bar> * \<bar>n\<bar>", simp) 
  1726 apply (rule mult_mono, auto) 
  1727 done
  1728 
  1729 lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1"
  1730 by (insert abs_zmult_eq_1 [of m n], arith)
  1731 
  1732 lemma pos_zmult_eq_1_iff: "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)"
  1733 apply (auto dest: pos_zmult_eq_1_iff_lemma) 
  1734 apply (simp add: mult_commute [of m]) 
  1735 apply (frule pos_zmult_eq_1_iff_lemma, auto) 
  1736 done
  1737 
  1738 lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
  1739 apply (rule iffI) 
  1740  apply (frule pos_zmult_eq_1_iff_lemma)
  1741  apply (simp add: mult_commute [of m]) 
  1742  apply (frule pos_zmult_eq_1_iff_lemma, auto) 
  1743 done
  1744 
  1745 (* Could be simplified but Presburger only becomes available too late *)
  1746 lemma infinite_UNIV_int: "~finite(UNIV::int set)"
  1747 proof
  1748   assume "finite(UNIV::int set)"
  1749   moreover have "~(EX i::int. 2*i = 1)"
  1750     by (auto simp: pos_zmult_eq_1_iff)
  1751   ultimately show False using finite_UNIV_inj_surj[of "%n::int. n+n"]
  1752     by (simp add:inj_on_def surj_def) (blast intro:sym)
  1753 qed
  1754 
  1755 
  1756 subsection{*Integer Powers*} 
  1757 
  1758 instantiation int :: recpower
  1759 begin
  1760 
  1761 primrec power_int where
  1762   "p ^ 0 = (1\<Colon>int)"
  1763   | "p ^ (Suc n) = (p\<Colon>int) * (p ^ n)"
  1764 
  1765 instance proof
  1766   fix z :: int
  1767   fix n :: nat
  1768   show "z ^ 0 = 1" by simp
  1769   show "z ^ Suc n = z * (z ^ n)" by simp
  1770 qed
  1771 
  1772 end
  1773 
  1774 lemma zpower_zadd_distrib: "x ^ (y + z) = ((x ^ y) * (x ^ z)::int)"
  1775   by (rule Power.power_add)
  1776 
  1777 lemma zpower_zpower: "(x ^ y) ^ z = (x ^ (y * z)::int)"
  1778   by (rule Power.power_mult [symmetric])
  1779 
  1780 lemma zero_less_zpower_abs_iff [simp]:
  1781   "(0 < abs x ^ n) \<longleftrightarrow> (x \<noteq> (0::int) | n = 0)"
  1782   by (induct n) (auto simp add: zero_less_mult_iff)
  1783 
  1784 lemma zero_le_zpower_abs [simp]: "(0::int) \<le> abs x ^ n"
  1785   by (induct n) (auto simp add: zero_le_mult_iff)
  1786 
  1787 lemma of_int_power:
  1788   "of_int (z ^ n) = (of_int z ^ n :: 'a::{recpower, ring_1})"
  1789   by (induct n) (simp_all add: power_Suc)
  1790 
  1791 lemma int_power: "int (m^n) = (int m) ^ n"
  1792   by (rule of_nat_power)
  1793 
  1794 lemmas zpower_int = int_power [symmetric]
  1795 
  1796 subsection {* Configuration of the code generator *}
  1797 
  1798 code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int"
  1799 
  1800 lemmas pred_succ_numeral_code [code] =
  1801   pred_bin_simps succ_bin_simps
  1802 
  1803 lemmas plus_numeral_code [code] =
  1804   add_bin_simps
  1805   arith_extra_simps(1) [where 'a = int]
  1806 
  1807 lemmas minus_numeral_code [code] =
  1808   minus_bin_simps
  1809   arith_extra_simps(2) [where 'a = int]
  1810   arith_extra_simps(5) [where 'a = int]
  1811 
  1812 lemmas times_numeral_code [code] =
  1813   mult_bin_simps
  1814   arith_extra_simps(4) [where 'a = int]
  1815 
  1816 instantiation int :: eq
  1817 begin
  1818 
  1819 definition [code del]: "eq_class.eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
  1820 
  1821 instance by default (simp add: eq_int_def)
  1822 
  1823 end
  1824 
  1825 lemma eq_number_of_int_code [code]:
  1826   "eq_class.eq (number_of k \<Colon> int) (number_of l) \<longleftrightarrow> eq_class.eq k l"
  1827   unfolding eq_int_def number_of_is_id ..
  1828 
  1829 lemma eq_int_code [code]:
  1830   "eq_class.eq Int.Pls Int.Pls \<longleftrightarrow> True"
  1831   "eq_class.eq Int.Pls Int.Min \<longleftrightarrow> False"
  1832   "eq_class.eq Int.Pls (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq Int.Pls k2"
  1833   "eq_class.eq Int.Pls (Int.Bit1 k2) \<longleftrightarrow> False"
  1834   "eq_class.eq Int.Min Int.Pls \<longleftrightarrow> False"
  1835   "eq_class.eq Int.Min Int.Min \<longleftrightarrow> True"
  1836   "eq_class.eq Int.Min (Int.Bit0 k2) \<longleftrightarrow> False"
  1837   "eq_class.eq Int.Min (Int.Bit1 k2) \<longleftrightarrow> eq_class.eq Int.Min k2"
  1838   "eq_class.eq (Int.Bit0 k1) Int.Pls \<longleftrightarrow> eq_class.eq Int.Pls k1"
  1839   "eq_class.eq (Int.Bit1 k1) Int.Pls \<longleftrightarrow> False"
  1840   "eq_class.eq (Int.Bit0 k1) Int.Min \<longleftrightarrow> False"
  1841   "eq_class.eq (Int.Bit1 k1) Int.Min \<longleftrightarrow> eq_class.eq Int.Min k1"
  1842   "eq_class.eq (Int.Bit0 k1) (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq k1 k2"
  1843   "eq_class.eq (Int.Bit0 k1) (Int.Bit1 k2) \<longleftrightarrow> False"
  1844   "eq_class.eq (Int.Bit1 k1) (Int.Bit0 k2) \<longleftrightarrow> False"
  1845   "eq_class.eq (Int.Bit1 k1) (Int.Bit1 k2) \<longleftrightarrow> eq_class.eq k1 k2"
  1846   unfolding eq_number_of_int_code [symmetric, of Int.Pls] 
  1847     eq_number_of_int_code [symmetric, of Int.Min]
  1848     eq_number_of_int_code [symmetric, of "Int.Bit0 k1"]
  1849     eq_number_of_int_code [symmetric, of "Int.Bit1 k1"]
  1850     eq_number_of_int_code [symmetric, of "Int.Bit0 k2"]
  1851     eq_number_of_int_code [symmetric, of "Int.Bit1 k2"]
  1852   by (simp_all add: eq Pls_def,
  1853     simp_all only: Min_def succ_def pred_def number_of_is_id)
  1854     (auto simp add: iszero_def)
  1855 
  1856 lemma eq_int_refl [code nbe]:
  1857   "eq_class.eq (k::int) k \<longleftrightarrow> True"
  1858   by (rule HOL.eq_refl)
  1859 
  1860 lemma less_eq_number_of_int_code [code]:
  1861   "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
  1862   unfolding number_of_is_id ..
  1863 
  1864 lemma less_eq_int_code [code]:
  1865   "Int.Pls \<le> Int.Pls \<longleftrightarrow> True"
  1866   "Int.Pls \<le> Int.Min \<longleftrightarrow> False"
  1867   "Int.Pls \<le> Int.Bit0 k \<longleftrightarrow> Int.Pls \<le> k"
  1868   "Int.Pls \<le> Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
  1869   "Int.Min \<le> Int.Pls \<longleftrightarrow> True"
  1870   "Int.Min \<le> Int.Min \<longleftrightarrow> True"
  1871   "Int.Min \<le> Int.Bit0 k \<longleftrightarrow> Int.Min < k"
  1872   "Int.Min \<le> Int.Bit1 k \<longleftrightarrow> Int.Min \<le> k"
  1873   "Int.Bit0 k \<le> Int.Pls \<longleftrightarrow> k \<le> Int.Pls"
  1874   "Int.Bit1 k \<le> Int.Pls \<longleftrightarrow> k < Int.Pls"
  1875   "Int.Bit0 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
  1876   "Int.Bit1 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
  1877   "Int.Bit0 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 \<le> k2"
  1878   "Int.Bit0 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
  1879   "Int.Bit1 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
  1880   "Int.Bit1 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
  1881   unfolding less_eq_number_of_int_code [symmetric, of Int.Pls] 
  1882     less_eq_number_of_int_code [symmetric, of Int.Min]
  1883     less_eq_number_of_int_code [symmetric, of "Int.Bit0 k1"]
  1884     less_eq_number_of_int_code [symmetric, of "Int.Bit1 k1"]
  1885     less_eq_number_of_int_code [symmetric, of "Int.Bit0 k2"]
  1886     less_eq_number_of_int_code [symmetric, of "Int.Bit1 k2"]
  1887   by (simp_all add: Pls_def, simp_all only: Min_def succ_def pred_def number_of_is_id)
  1888     (auto simp add: neg_def linorder_not_less group_simps
  1889       zle_add1_eq_le [symmetric] del: iffI , auto simp only: Bit0_def Bit1_def)
  1890 
  1891 lemma less_number_of_int_code [code]:
  1892   "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
  1893   unfolding number_of_is_id ..
  1894 
  1895 lemma less_int_code [code]:
  1896   "Int.Pls < Int.Pls \<longleftrightarrow> False"
  1897   "Int.Pls < Int.Min \<longleftrightarrow> False"
  1898   "Int.Pls < Int.Bit0 k \<longleftrightarrow> Int.Pls < k"
  1899   "Int.Pls < Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
  1900   "Int.Min < Int.Pls \<longleftrightarrow> True"
  1901   "Int.Min < Int.Min \<longleftrightarrow> False"
  1902   "Int.Min < Int.Bit0 k \<longleftrightarrow> Int.Min < k"
  1903   "Int.Min < Int.Bit1 k \<longleftrightarrow> Int.Min < k"
  1904   "Int.Bit0 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
  1905   "Int.Bit1 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
  1906   "Int.Bit0 k < Int.Min \<longleftrightarrow> k \<le> Int.Min"
  1907   "Int.Bit1 k < Int.Min \<longleftrightarrow> k < Int.Min"
  1908   "Int.Bit0 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
  1909   "Int.Bit0 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
  1910   "Int.Bit1 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
  1911   "Int.Bit1 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 < k2"
  1912   unfolding less_number_of_int_code [symmetric, of Int.Pls] 
  1913     less_number_of_int_code [symmetric, of Int.Min]
  1914     less_number_of_int_code [symmetric, of "Int.Bit0 k1"]
  1915     less_number_of_int_code [symmetric, of "Int.Bit1 k1"]
  1916     less_number_of_int_code [symmetric, of "Int.Bit0 k2"]
  1917     less_number_of_int_code [symmetric, of "Int.Bit1 k2"]
  1918   by (simp_all add: Pls_def, simp_all only: Min_def succ_def pred_def number_of_is_id)
  1919     (auto simp add: neg_def group_simps zle_add1_eq_le [symmetric] del: iffI,
  1920       auto simp only: Bit0_def Bit1_def)
  1921 
  1922 definition
  1923   nat_aux :: "int \<Rightarrow> nat \<Rightarrow> nat" where
  1924   "nat_aux i n = nat i + n"
  1925 
  1926 lemma [code]:
  1927   "nat_aux i n = (if i \<le> 0 then n else nat_aux (i - 1) (Suc n))"  -- {* tail recursive *}
  1928   by (auto simp add: nat_aux_def nat_eq_iff linorder_not_le order_less_imp_le
  1929     dest: zless_imp_add1_zle)
  1930 
  1931 lemma [code]: "nat i = nat_aux i 0"
  1932   by (simp add: nat_aux_def)
  1933 
  1934 hide (open) const nat_aux
  1935 
  1936 lemma zero_is_num_zero [code, code inline, symmetric, code post]:
  1937   "(0\<Colon>int) = Numeral0" 
  1938   by simp
  1939 
  1940 lemma one_is_num_one [code, code inline, symmetric, code post]:
  1941   "(1\<Colon>int) = Numeral1" 
  1942   by simp
  1943 
  1944 code_modulename SML
  1945   Int Integer
  1946 
  1947 code_modulename OCaml
  1948   Int Integer
  1949 
  1950 code_modulename Haskell
  1951   Int Integer
  1952 
  1953 types_code
  1954   "int" ("int")
  1955 attach (term_of) {*
  1956 val term_of_int = HOLogic.mk_number HOLogic.intT;
  1957 *}
  1958 attach (test) {*
  1959 fun gen_int i =
  1960   let val j = one_of [~1, 1] * random_range 0 i
  1961   in (j, fn () => term_of_int j) end;
  1962 *}
  1963 
  1964 setup {*
  1965 let
  1966 
  1967 fun strip_number_of (@{term "Int.number_of :: int => int"} $ t) = t
  1968   | strip_number_of t = t;
  1969 
  1970 fun numeral_codegen thy defs dep module b t gr =
  1971   let val i = HOLogic.dest_numeral (strip_number_of t)
  1972   in
  1973     SOME (Codegen.str (string_of_int i),
  1974       snd (Codegen.invoke_tycodegen thy defs dep module false HOLogic.intT gr))
  1975   end handle TERM _ => NONE;
  1976 
  1977 in
  1978 
  1979 Codegen.add_codegen "numeral_codegen" numeral_codegen
  1980 
  1981 end
  1982 *}
  1983 
  1984 consts_code
  1985   "number_of :: int \<Rightarrow> int"    ("(_)")
  1986   "0 :: int"                   ("0")
  1987   "1 :: int"                   ("1")
  1988   "uminus :: int => int"       ("~")
  1989   "op + :: int => int => int"  ("(_ +/ _)")
  1990   "op * :: int => int => int"  ("(_ */ _)")
  1991   "op \<le> :: int => int => bool" ("(_ <=/ _)")
  1992   "op < :: int => int => bool" ("(_ </ _)")
  1993 
  1994 quickcheck_params [default_type = int]
  1995 
  1996 hide (open) const Pls Min Bit0 Bit1 succ pred
  1997 
  1998 
  1999 subsection {* Legacy theorems *}
  2000 
  2001 lemmas zminus_zminus = minus_minus [of "z::int", standard]
  2002 lemmas zminus_0 = minus_zero [where 'a=int]
  2003 lemmas zminus_zadd_distrib = minus_add_distrib [of "z::int" "w", standard]
  2004 lemmas zadd_commute = add_commute [of "z::int" "w", standard]
  2005 lemmas zadd_assoc = add_assoc [of "z1::int" "z2" "z3", standard]
  2006 lemmas zadd_left_commute = add_left_commute [of "x::int" "y" "z", standard]
  2007 lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute
  2008 lemmas zmult_ac = OrderedGroup.mult_ac
  2009 lemmas zadd_0 = OrderedGroup.add_0_left [of "z::int", standard]
  2010 lemmas zadd_0_right = OrderedGroup.add_0_left [of "z::int", standard]
  2011 lemmas zadd_zminus_inverse2 = left_minus [of "z::int", standard]
  2012 lemmas zmult_zminus = mult_minus_left [of "z::int" "w", standard]
  2013 lemmas zmult_commute = mult_commute [of "z::int" "w", standard]
  2014 lemmas zmult_assoc = mult_assoc [of "z1::int" "z2" "z3", standard]
  2015 lemmas zadd_zmult_distrib = left_distrib [of "z1::int" "z2" "w", standard]
  2016 lemmas zadd_zmult_distrib2 = right_distrib [of "w::int" "z1" "z2", standard]
  2017 lemmas zdiff_zmult_distrib = left_diff_distrib [of "z1::int" "z2" "w", standard]
  2018 lemmas zdiff_zmult_distrib2 = right_diff_distrib [of "w::int" "z1" "z2", standard]
  2019 
  2020 lemmas zmult_1 = mult_1_left [of "z::int", standard]
  2021 lemmas zmult_1_right = mult_1_right [of "z::int", standard]
  2022 
  2023 lemmas zle_refl = order_refl [of "w::int", standard]
  2024 lemmas zle_trans = order_trans [where 'a=int and x="i" and y="j" and z="k", standard]
  2025 lemmas zle_anti_sym = order_antisym [of "z::int" "w", standard]
  2026 lemmas zle_linear = linorder_linear [of "z::int" "w", standard]
  2027 lemmas zless_linear = linorder_less_linear [where 'a = int]
  2028 
  2029 lemmas zadd_left_mono = add_left_mono [of "i::int" "j" "k", standard]
  2030 lemmas zadd_strict_right_mono = add_strict_right_mono [of "i::int" "j" "k", standard]
  2031 lemmas zadd_zless_mono = add_less_le_mono [of "w'::int" "w" "z'" "z", standard]
  2032 
  2033 lemmas int_0_less_1 = zero_less_one [where 'a=int]
  2034 lemmas int_0_neq_1 = zero_neq_one [where 'a=int]
  2035 
  2036 lemmas inj_int = inj_of_nat [where 'a=int]
  2037 lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
  2038 lemmas int_mult = of_nat_mult [where 'a=int]
  2039 lemmas zmult_int = of_nat_mult [where 'a=int, symmetric]
  2040 lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="n", standard]
  2041 lemmas zless_int = of_nat_less_iff [where 'a=int]
  2042 lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="k", standard]
  2043 lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int]
  2044 lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
  2045 lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="n", standard]
  2046 lemmas int_0 = of_nat_0 [where 'a=int]
  2047 lemmas int_1 = of_nat_1 [where 'a=int]
  2048 lemmas int_Suc = of_nat_Suc [where 'a=int]
  2049 lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m", standard]
  2050 lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
  2051 lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
  2052 lemmas zless_le = less_int_def
  2053 lemmas int_eq_of_nat = TrueI
  2054 
  2055 end