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