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