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