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