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