2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
3 Author: Tobias Nipkow, Florian Haftmann, TU Muenchen
6 header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *}
9 imports Equiv_Relations Nat Wellfounded
12 ("Tools/numeral_syntax.ML")
13 ("Tools/int_arith.ML")
16 subsection {* The equivalence relation underlying the integers *}
18 definition intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set" where
19 "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
23 by (auto simp add: quotient_def)
25 instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
29 Zero_int_def: "0 = Abs_Integ (intrel `` {(0, 0)})"
32 One_int_def: "1 = Abs_Integ (intrel `` {(1, 0)})"
35 add_int_def: "z + w = Abs_Integ
36 (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u, v) \<in> Rep_Integ w.
37 intrel `` {(x + u, y + v)})"
41 "- z = Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})"
44 diff_int_def: "z - w = z + (-w \<Colon> int)"
47 mult_int_def: "z * w = Abs_Integ
48 (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u,v ) \<in> Rep_Integ w.
49 intrel `` {(x*u + y*v, x*v + y*u)})"
53 "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 less_int_def: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
59 zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
62 zsgn_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
69 subsection{*Construction of the Integers*}
71 lemma intrel_iff [simp]: "(((x,y),(u,v)) \<in> intrel) = (x+v = u+y)"
72 by (simp add: intrel_def)
74 lemma equiv_intrel: "equiv UNIV intrel"
75 by (simp add: intrel_def equiv_def refl_on_def sym_def trans_def)
77 text{*Reduces equality of equivalence classes to the @{term intrel} relation:
78 @{term "(intrel `` {x} = intrel `` {y}) = ((x,y) \<in> intrel)"} *}
79 lemmas equiv_intrel_iff [simp] = eq_equiv_class_iff [OF equiv_intrel UNIV_I UNIV_I]
81 text{*All equivalence classes belong to set of representatives*}
82 lemma [simp]: "intrel``{(x,y)} \<in> Integ"
83 by (auto simp add: Integ_def intrel_def quotient_def)
85 text{*Reduces equality on abstractions to equality on representatives:
86 @{prop "\<lbrakk>x \<in> Integ; y \<in> Integ\<rbrakk> \<Longrightarrow> (Abs_Integ x = Abs_Integ y) = (x=y)"} *}
87 declare Abs_Integ_inject [simp,no_atp] Abs_Integ_inverse [simp,no_atp]
89 text{*Case analysis on the representation of an integer as an equivalence
90 class of pairs of naturals.*}
91 lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]:
92 "(!!x y. z = Abs_Integ(intrel``{(x,y)}) ==> P) ==> P"
93 apply (rule Abs_Integ_cases [of z])
94 apply (auto simp add: Integ_def quotient_def)
98 subsection {* Arithmetic Operations *}
100 lemma minus: "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})"
102 have "(\<lambda>(x,y). intrel``{(y,x)}) respects intrel"
103 by (auto simp add: congruent_def)
105 by (simp add: minus_int_def UN_equiv_class [OF equiv_intrel])
109 "Abs_Integ (intrel``{(x,y)}) + Abs_Integ (intrel``{(u,v)}) =
110 Abs_Integ (intrel``{(x+u, y+v)})"
112 have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). intrel `` {(x+u, y+v)}) w) z)
114 by (auto simp add: congruent2_def)
116 by (simp add: add_int_def UN_UN_split_split_eq
117 UN_equiv_class2 [OF equiv_intrel equiv_intrel])
120 text{*Congruence property for multiplication*}
121 lemma mult_congruent2:
122 "(%p1 p2. (%(x,y). (%(u,v). intrel``{(x*u + y*v, x*v + y*u)}) p2) p1)
124 apply (rule equiv_intrel [THEN congruent2_commuteI])
125 apply (force simp add: mult_ac, clarify)
126 apply (simp add: congruent_def mult_ac)
127 apply (rename_tac u v w x y z)
128 apply (subgoal_tac "u*y + x*y = w*y + v*y & u*z + x*z = w*z + v*z")
129 apply (simp add: mult_ac)
130 apply (simp add: add_mult_distrib [symmetric])
134 "Abs_Integ((intrel``{(x,y)})) * Abs_Integ((intrel``{(u,v)})) =
135 Abs_Integ(intrel `` {(x*u + y*v, x*v + y*u)})"
136 by (simp add: mult_int_def UN_UN_split_split_eq mult_congruent2
137 UN_equiv_class2 [OF equiv_intrel equiv_intrel])
139 text{*The integers form a @{text comm_ring_1}*}
140 instance int :: comm_ring_1
143 show "(i + j) + k = i + (j + k)"
144 by (cases i, cases j, cases k) (simp add: add add_assoc)
146 by (cases i, cases j) (simp add: add_ac add)
148 by (cases i) (simp add: Zero_int_def add)
150 by (cases i) (simp add: Zero_int_def minus add)
151 show "i - j = i + - j"
152 by (simp add: diff_int_def)
153 show "(i * j) * k = i * (j * k)"
154 by (cases i, cases j, cases k) (simp add: mult algebra_simps)
156 by (cases i, cases j) (simp add: mult algebra_simps)
158 by (cases i) (simp add: One_int_def mult)
159 show "(i + j) * k = i * k + j * k"
160 by (cases i, cases j, cases k) (simp add: add mult algebra_simps)
161 show "0 \<noteq> (1::int)"
162 by (simp add: Zero_int_def One_int_def)
165 abbreviation int :: "nat \<Rightarrow> int" where
166 "int \<equiv> of_nat"
168 lemma int_def: "int m = Abs_Integ (intrel `` {(m, 0)})"
169 by (induct m) (simp_all add: Zero_int_def One_int_def add)
172 subsection {* The @{text "\<le>"} Ordering *}
175 "(Abs_Integ(intrel``{(x,y)}) \<le> Abs_Integ(intrel``{(u,v)})) = (x+v \<le> u+y)"
176 by (force simp add: le_int_def)
179 "(Abs_Integ(intrel``{(x,y)}) < Abs_Integ(intrel``{(u,v)})) = (x+v < u+y)"
180 by (simp add: less_int_def le order_less_le)
182 instance int :: linorder
185 show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
186 by (cases i, cases j) (simp add: le)
187 show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
188 by (auto simp add: less_int_def dest: antisym)
190 by (cases i) (simp add: le)
191 show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
192 by (cases i, cases j, cases k) (simp add: le)
193 show "i \<le> j \<or> j \<le> i"
194 by (cases i, cases j) (simp add: le linorder_linear)
197 instantiation int :: distrib_lattice
201 "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
204 "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
208 (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
212 instance int :: ordered_cancel_ab_semigroup_add
215 show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
216 by (cases i, cases j, cases k) (simp add: le add)
220 text{*Strict Monotonicity of Multiplication*}
222 text{*strict, in 1st argument; proof is by induction on k>0*}
223 lemma zmult_zless_mono2_lemma:
224 "(i::int)<j ==> 0<k ==> int k * i < int k * j"
227 apply (simp add: left_distrib)
228 apply (case_tac "k=0")
229 apply (simp_all add: add_strict_mono)
232 lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = int n"
234 apply (auto simp add: le add int_def Zero_int_def)
235 apply (rule_tac x="x-y" in exI, simp)
238 lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = int n"
240 apply (simp add: less int_def Zero_int_def)
241 apply (rule_tac x="x-y" in exI, simp)
244 lemma zmult_zless_mono2: "[| i<j; (0::int) < k |] ==> k*i < k*j"
245 apply (drule zero_less_imp_eq_int)
246 apply (auto simp add: zmult_zless_mono2_lemma)
249 text{*The integers form an ordered integral domain*}
250 instance int :: linordered_idom
253 show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
254 by (rule zmult_zless_mono2)
255 show "\<bar>i\<bar> = (if i < 0 then -i else i)"
256 by (simp only: zabs_def)
257 show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
258 by (simp only: zsgn_def)
261 lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + (1\<Colon>int) \<le> z"
262 apply (cases w, cases z)
263 apply (simp add: less le add One_int_def)
266 lemma zless_iff_Suc_zadd:
267 "(w \<Colon> int) < z \<longleftrightarrow> (\<exists>n. z = w + int (Suc n))"
268 apply (cases z, cases w)
269 apply (auto simp add: less add int_def)
270 apply (rename_tac a b c d)
271 apply (rule_tac x="a+d - Suc(c+b)" in exI)
276 left_distrib [of "z1::int" "z2" "w", standard]
277 right_distrib [of "w::int" "z1" "z2", standard]
278 left_diff_distrib [of "z1::int" "z2" "w", standard]
279 right_diff_distrib [of "w::int" "z1" "z2", standard]
282 subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}
287 definition of_int :: "int \<Rightarrow> 'a" where
288 "of_int z = the_elem (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
290 lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
292 have "(\<lambda>(i,j). { of_nat i - (of_nat j :: 'a) }) respects intrel"
293 by (auto simp add: congruent_def) (simp add: algebra_simps of_nat_add [symmetric]
296 by (simp add: of_int_def UN_equiv_class [OF equiv_intrel])
299 lemma of_int_0 [simp]: "of_int 0 = 0"
300 by (simp add: of_int Zero_int_def)
302 lemma of_int_1 [simp]: "of_int 1 = 1"
303 by (simp add: of_int One_int_def)
305 lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z"
306 by (cases w, cases z) (simp add: algebra_simps of_int add)
308 lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)"
309 by (cases z) (simp add: algebra_simps of_int minus)
311 lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z"
312 by (simp add: diff_minus Groups.diff_minus)
314 lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
315 apply (cases w, cases z)
316 apply (simp add: algebra_simps of_int mult of_nat_mult)
319 text{*Collapse nested embeddings*}
320 lemma of_int_of_nat_eq [simp]: "of_int (int n) = of_nat n"
324 "of_int (z ^ n) = of_int z ^ n"
325 by (induct n) simp_all
329 text{*Class for unital rings with characteristic zero.
330 Includes non-ordered rings like the complex numbers.*}
331 class ring_char_0 = ring_1 + semiring_char_0
334 lemma of_int_eq_iff [simp]:
335 "of_int w = of_int z \<longleftrightarrow> w = z"
336 apply (cases w, cases z)
337 apply (simp add: of_int)
338 apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq)
339 apply (simp only: of_nat_add [symmetric] of_nat_eq_iff)
342 text{*Special cases where either operand is zero*}
343 lemma of_int_eq_0_iff [simp]:
344 "of_int z = 0 \<longleftrightarrow> z = 0"
345 using of_int_eq_iff [of z 0] by simp
347 lemma of_int_0_eq_iff [simp]:
348 "0 = of_int z \<longleftrightarrow> z = 0"
349 using of_int_eq_iff [of 0 z] by simp
353 context linordered_idom
356 text{*Every @{text linordered_idom} has characteristic zero.*}
357 subclass ring_char_0 ..
359 lemma of_int_le_iff [simp]:
360 "of_int w \<le> of_int z \<longleftrightarrow> w \<le> z"
361 by (cases w, cases z)
362 (simp add: of_int le minus algebra_simps of_nat_add [symmetric] del: of_nat_add)
364 lemma of_int_less_iff [simp]:
365 "of_int w < of_int z \<longleftrightarrow> w < z"
366 by (simp add: less_le order_less_le)
368 lemma of_int_0_le_iff [simp]:
369 "0 \<le> of_int z \<longleftrightarrow> 0 \<le> z"
370 using of_int_le_iff [of 0 z] by simp
372 lemma of_int_le_0_iff [simp]:
373 "of_int z \<le> 0 \<longleftrightarrow> z \<le> 0"
374 using of_int_le_iff [of z 0] by simp
376 lemma of_int_0_less_iff [simp]:
377 "0 < of_int z \<longleftrightarrow> 0 < z"
378 using of_int_less_iff [of 0 z] by simp
380 lemma of_int_less_0_iff [simp]:
381 "of_int z < 0 \<longleftrightarrow> z < 0"
382 using of_int_less_iff [of z 0] by simp
386 lemma of_int_eq_id [simp]: "of_int = id"
388 fix z show "of_int z = id z"
389 by (cases z) (simp add: of_int add minus int_def diff_minus)
393 subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *}
395 definition nat :: "int \<Rightarrow> nat" where
396 "nat z = the_elem (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
398 lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
400 have "(\<lambda>(x,y). {x-y}) respects intrel"
401 by (auto simp add: congruent_def)
403 by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
406 lemma nat_int [simp]: "nat (int n) = n"
407 by (simp add: nat int_def)
409 lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
410 by (cases z) (simp add: nat le int_def Zero_int_def)
412 corollary nat_0_le: "0 \<le> z ==> int (nat z) = z"
415 lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
416 by (cases z) (simp add: nat le Zero_int_def)
418 lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"
419 apply (cases w, cases z)
420 apply (simp add: nat le linorder_not_le [symmetric] Zero_int_def, arith)
423 text{*An alternative condition is @{term "0 \<le> w"} *}
424 corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
425 by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
427 corollary nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"
428 by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
430 lemma zless_nat_conj [simp]: "(nat w < nat z) = (0 < z & w < z)"
431 apply (cases w, cases z)
432 apply (simp add: nat le Zero_int_def linorder_not_le [symmetric], arith)
437 assumes "0 \<le> z" and "\<And>m. z = int m \<Longrightarrow> P"
439 using assms by (blast dest: nat_0_le sym)
441 lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)"
442 by (cases w) (simp add: nat le int_def Zero_int_def, arith)
444 corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)"
445 by (simp only: eq_commute [of m] nat_eq_iff)
447 lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)"
449 apply (simp add: nat le int_def Zero_int_def linorder_not_le[symmetric], arith)
452 lemma nat_le_iff: "nat x \<le> n \<longleftrightarrow> x \<le> int n"
453 by (cases x, simp add: nat le int_def le_diff_conv)
455 lemma nat_mono: "x \<le> y \<Longrightarrow> nat x \<le> nat y"
456 by (cases x, cases y, simp add: nat le)
458 lemma nat_0_iff[simp]: "nat(i::int) = 0 \<longleftrightarrow> i\<le>0"
459 by(simp add: nat_eq_iff) arith
461 lemma int_eq_iff: "(of_nat m = z) = (m = nat z & 0 \<le> z)"
462 by (auto simp add: nat_eq_iff2)
464 lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)"
465 by (insert zless_nat_conj [of 0], auto)
467 lemma nat_add_distrib:
468 "[| (0::int) \<le> z; 0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"
469 by (cases z, cases z') (simp add: nat add le Zero_int_def)
471 lemma nat_diff_distrib:
472 "[| (0::int) \<le> z'; z' \<le> z |] ==> nat (z-z') = nat z - nat z'"
473 by (cases z, cases z')
474 (simp add: nat add minus diff_minus le Zero_int_def)
476 lemma nat_zminus_int [simp]: "nat (- int n) = 0"
477 by (simp add: int_def minus nat Zero_int_def)
479 lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
480 by (cases z) (simp add: nat less int_def, arith)
485 lemma of_nat_nat: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z"
486 by (cases z rule: eq_Abs_Integ)
487 (simp add: nat le of_int Zero_int_def of_nat_diff)
491 text {* For termination proofs: *}
492 lemma measure_function_int[measure_function]: "is_measure (nat o abs)" ..
495 subsection{*Lemmas about the Function @{term of_nat} and Orderings*}
497 lemma negative_zless_0: "- (int (Suc n)) < (0 \<Colon> int)"
498 by (simp add: order_less_le del: of_nat_Suc)
500 lemma negative_zless [iff]: "- (int (Suc n)) < int m"
501 by (rule negative_zless_0 [THEN order_less_le_trans], simp)
503 lemma negative_zle_0: "- int n \<le> 0"
504 by (simp add: minus_le_iff)
506 lemma negative_zle [iff]: "- int n \<le> int m"
507 by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff])
509 lemma not_zle_0_negative [simp]: "~ (0 \<le> - (int (Suc n)))"
510 by (subst le_minus_iff, simp del: of_nat_Suc)
512 lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
513 by (simp add: int_def le minus Zero_int_def)
515 lemma not_int_zless_negative [simp]: "~ (int n < - int m)"
516 by (simp add: linorder_not_less)
518 lemma negative_eq_positive [simp]: "(- int n = of_nat m) = (n = 0 & m = 0)"
519 by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg)
521 lemma zle_iff_zadd: "w \<le> z \<longleftrightarrow> (\<exists>n. z = w + int n)"
523 have "(w \<le> z) = (0 \<le> z - w)"
524 by (simp only: le_diff_eq add_0_left)
525 also have "\<dots> = (\<exists>n. z - w = of_nat n)"
526 by (auto elim: zero_le_imp_eq_int)
527 also have "\<dots> = (\<exists>n. z = w + of_nat n)"
528 by (simp only: algebra_simps)
529 finally show ?thesis .
532 lemma zadd_int_left: "int m + (int n + z) = int (m + n) + z"
535 lemma int_Suc0_eq_1: "int (Suc 0) = 1"
538 text{*This version is proved for all ordered rings, not just integers!
539 It is proved here because attribute @{text arith_split} is not available
540 in theory @{text Rings}.
541 But is it really better than just rewriting with @{text abs_if}?*}
542 lemma abs_split [arith_split,no_atp]:
543 "P(abs(a::'a::linordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
544 by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
546 lemma negD: "x < 0 \<Longrightarrow> \<exists>n. x = - (int (Suc n))"
548 apply (auto simp add: le minus Zero_int_def int_def order_less_le)
549 apply (rule_tac x="y - Suc x" in exI, arith)
553 subsection {* Cases and induction *}
555 text{*Now we replace the case analysis rule by a more conventional one:
556 whether an integer is negative or not.*}
558 theorem int_cases [case_names nonneg neg, cases type: int]:
559 "[|!! n. z = int n ==> P; !! n. z = - (int (Suc n)) ==> P |] ==> P"
560 apply (cases "z < 0")
561 apply (blast dest!: negD)
562 apply (simp add: linorder_not_less del: of_nat_Suc)
564 apply (blast dest: nat_0_le [THEN sym])
567 theorem int_of_nat_induct [case_names nonneg neg, induct type: int]:
568 "[|!! n. P (int n); !!n. P (- (int (Suc n))) |] ==> P z"
571 text{*Contributed by Brian Huffman*}
572 theorem int_diff_cases:
573 obtains (diff) m n where "z = int m - int n"
574 apply (cases z rule: eq_Abs_Integ)
575 apply (rule_tac m=x and n=y in diff)
576 apply (simp add: int_def minus add diff_minus)
580 subsection {* Binary representation *}
583 This formalization defines binary arithmetic in terms of the integers
584 rather than using a datatype. This avoids multiple representations (leading
585 zeroes, etc.) See @{text "ZF/Tools/twos-compl.ML"}, function @{text
586 int_of_binary}, for the numerical interpretation.
588 The representation expects that @{text "(m mod 2)"} is 0 or 1,
589 even if m is negative;
590 For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
591 @{text "-5 = (-3)*2 + 1"}.
593 This two's complement binary representation derives from the paper
594 "An Efficient Representation of Arithmetic for Term Rewriting" by
595 Dave Cohen and Phil Watson, Rewriting Techniques and Applications,
596 Springer LNCS 488 (240-251), 1991.
599 subsubsection {* The constructors @{term Bit0}, @{term Bit1}, @{term Pls} and @{term Min} *}
601 definition Pls :: int where
604 definition Min :: int where
607 definition Bit0 :: "int \<Rightarrow> int" where
610 definition Bit1 :: "int \<Rightarrow> int" where
613 class number = -- {* for numeric types: nat, int, real, \dots *}
614 fixes number_of :: "int \<Rightarrow> 'a"
616 use "Tools/numeral.ML"
619 "_Numeral" :: "num_const \<Rightarrow> 'a" ("_")
621 use "Tools/numeral_syntax.ML"
622 setup Numeral_Syntax.setup
625 "Numeral0 \<equiv> number_of Pls"
628 "Numeral1 \<equiv> number_of (Bit1 Pls)"
630 lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"
631 -- {* Unfold all @{text let}s involving constants *}
634 definition succ :: "int \<Rightarrow> int" where
637 definition pred :: "int \<Rightarrow> int" where
641 max_number_of [simp] = max_def
642 [of "number_of u" "number_of v", standard]
644 min_number_of [simp] = min_def
645 [of "number_of u" "number_of v", standard]
646 -- {* unfolding @{text minx} and @{text max} on numerals *}
648 lemmas numeral_simps =
649 succ_def pred_def Pls_def Min_def Bit0_def Bit1_def
651 text {* Removal of leading zeroes *}
653 lemma Bit0_Pls [simp, code_post]:
655 unfolding numeral_simps by simp
657 lemma Bit1_Min [simp, code_post]:
659 unfolding numeral_simps by simp
661 lemmas normalize_bin_simps =
665 subsubsection {* Successor and predecessor functions *}
670 "succ Pls = Bit1 Pls"
671 unfolding numeral_simps by simp
675 unfolding numeral_simps by simp
678 "succ (Bit0 k) = Bit1 k"
679 unfolding numeral_simps by simp
682 "succ (Bit1 k) = Bit0 (succ k)"
683 unfolding numeral_simps by simp
685 lemmas succ_bin_simps [simp] =
686 succ_Pls succ_Min succ_Bit0 succ_Bit1
688 text {* Predecessor *}
692 unfolding numeral_simps by simp
695 "pred Min = Bit0 Min"
696 unfolding numeral_simps by simp
699 "pred (Bit0 k) = Bit1 (pred k)"
700 unfolding numeral_simps by simp
703 "pred (Bit1 k) = Bit0 k"
704 unfolding numeral_simps by simp
706 lemmas pred_bin_simps [simp] =
707 pred_Pls pred_Min pred_Bit0 pred_Bit1
710 subsubsection {* Binary arithmetic *}
716 unfolding numeral_simps by simp
720 unfolding numeral_simps by simp
723 "(Bit0 k) + (Bit0 l) = Bit0 (k + l)"
724 unfolding numeral_simps by simp
727 "(Bit0 k) + (Bit1 l) = Bit1 (k + l)"
728 unfolding numeral_simps by simp
731 "(Bit1 k) + (Bit0 l) = Bit1 (k + l)"
732 unfolding numeral_simps by simp
735 "(Bit1 k) + (Bit1 l) = Bit0 (k + succ l)"
736 unfolding numeral_simps by simp
740 unfolding numeral_simps by simp
744 unfolding numeral_simps by simp
746 lemmas add_bin_simps [simp] =
747 add_Pls add_Min add_Pls_right add_Min_right
748 add_Bit0_Bit0 add_Bit0_Bit1 add_Bit1_Bit0 add_Bit1_Bit1
754 unfolding numeral_simps by simp
758 unfolding numeral_simps by simp
761 "- (Bit0 k) = Bit0 (- k)"
762 unfolding numeral_simps by simp
765 "- (Bit1 k) = Bit1 (pred (- k))"
766 unfolding numeral_simps by simp
768 lemmas minus_bin_simps [simp] =
769 minus_Pls minus_Min minus_Bit0 minus_Bit1
771 text {* Subtraction *}
773 lemma diff_bin_simps [simp]:
776 "Pls - (Bit0 l) = Bit0 (Pls - l)"
777 "Pls - (Bit1 l) = Bit1 (Min - l)"
778 "Min - (Bit0 l) = Bit1 (Min - l)"
779 "Min - (Bit1 l) = Bit0 (Min - l)"
780 "(Bit0 k) - (Bit0 l) = Bit0 (k - l)"
781 "(Bit0 k) - (Bit1 l) = Bit1 (pred k - l)"
782 "(Bit1 k) - (Bit0 l) = Bit1 (k - l)"
783 "(Bit1 k) - (Bit1 l) = Bit0 (k - l)"
784 unfolding numeral_simps by simp_all
786 text {* Multiplication *}
790 unfolding numeral_simps by simp
794 unfolding numeral_simps by simp
797 "(Bit0 k) * l = Bit0 (k * l)"
798 unfolding numeral_simps int_distrib by simp
801 "(Bit1 k) * l = (Bit0 (k * l)) + l"
802 unfolding numeral_simps int_distrib by simp
804 lemmas mult_bin_simps [simp] =
805 mult_Pls mult_Min mult_Bit0 mult_Bit1
808 subsubsection {* Binary comparisons *}
810 text {* Preliminaries *}
812 lemma even_less_0_iff:
813 "a + a < 0 \<longleftrightarrow> a < (0::'a::linordered_idom)"
815 have "a + a < 0 \<longleftrightarrow> (1+1)*a < 0" by (simp add: left_distrib)
816 also have "(1+1)*a < 0 \<longleftrightarrow> a < 0"
817 by (simp add: mult_less_0_iff zero_less_two
818 order_less_not_sym [OF zero_less_two])
819 finally show ?thesis .
823 assumes le: "0 \<le> z"
824 shows "(0::int) < 1 + z"
826 have "0 \<le> z" by fact
827 also have "... < z + 1" by (rule less_add_one)
828 also have "... = 1 + z" by (simp add: add_ac)
829 finally show "0 < 1 + z" .
832 lemma odd_less_0_iff:
833 "(1 + z + z < 0) = (z < (0::int))"
836 thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
837 le_imp_0_less [THEN order_less_imp_le])
840 thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1
841 add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric])
844 lemma bin_less_0_simps:
845 "Pls < 0 \<longleftrightarrow> False"
846 "Min < 0 \<longleftrightarrow> True"
847 "Bit0 w < 0 \<longleftrightarrow> w < 0"
848 "Bit1 w < 0 \<longleftrightarrow> w < 0"
849 unfolding numeral_simps
850 by (simp_all add: even_less_0_iff odd_less_0_iff)
852 lemma less_bin_lemma: "k < l \<longleftrightarrow> k - l < (0::int)"
855 lemma le_iff_pred_less: "k \<le> l \<longleftrightarrow> pred k < l"
856 unfolding numeral_simps
858 have "k - 1 < k" by simp
859 also assume "k \<le> l"
860 finally show "k - 1 < l" .
863 hence "(k - 1) + 1 \<le> l" by (rule zless_imp_add1_zle)
864 thus "k \<le> l" by simp
867 lemma succ_pred: "succ (pred x) = x"
868 unfolding numeral_simps by simp
872 lemma less_bin_simps [simp]:
873 "Pls < Pls \<longleftrightarrow> False"
874 "Pls < Min \<longleftrightarrow> False"
875 "Pls < Bit0 k \<longleftrightarrow> Pls < k"
876 "Pls < Bit1 k \<longleftrightarrow> Pls \<le> k"
877 "Min < Pls \<longleftrightarrow> True"
878 "Min < Min \<longleftrightarrow> False"
879 "Min < Bit0 k \<longleftrightarrow> Min < k"
880 "Min < Bit1 k \<longleftrightarrow> Min < k"
881 "Bit0 k < Pls \<longleftrightarrow> k < Pls"
882 "Bit0 k < Min \<longleftrightarrow> k \<le> Min"
883 "Bit1 k < Pls \<longleftrightarrow> k < Pls"
884 "Bit1 k < Min \<longleftrightarrow> k < Min"
885 "Bit0 k < Bit0 l \<longleftrightarrow> k < l"
886 "Bit0 k < Bit1 l \<longleftrightarrow> k \<le> l"
887 "Bit1 k < Bit0 l \<longleftrightarrow> k < l"
888 "Bit1 k < Bit1 l \<longleftrightarrow> k < l"
889 unfolding le_iff_pred_less
890 less_bin_lemma [of Pls]
891 less_bin_lemma [of Min]
892 less_bin_lemma [of "k"]
893 less_bin_lemma [of "Bit0 k"]
894 less_bin_lemma [of "Bit1 k"]
895 less_bin_lemma [of "pred Pls"]
896 less_bin_lemma [of "pred k"]
897 by (simp_all add: bin_less_0_simps succ_pred)
899 text {* Less-than-or-equal *}
901 lemma le_bin_simps [simp]:
902 "Pls \<le> Pls \<longleftrightarrow> True"
903 "Pls \<le> Min \<longleftrightarrow> False"
904 "Pls \<le> Bit0 k \<longleftrightarrow> Pls \<le> k"
905 "Pls \<le> Bit1 k \<longleftrightarrow> Pls \<le> k"
906 "Min \<le> Pls \<longleftrightarrow> True"
907 "Min \<le> Min \<longleftrightarrow> True"
908 "Min \<le> Bit0 k \<longleftrightarrow> Min < k"
909 "Min \<le> Bit1 k \<longleftrightarrow> Min \<le> k"
910 "Bit0 k \<le> Pls \<longleftrightarrow> k \<le> Pls"
911 "Bit0 k \<le> Min \<longleftrightarrow> k \<le> Min"
912 "Bit1 k \<le> Pls \<longleftrightarrow> k < Pls"
913 "Bit1 k \<le> Min \<longleftrightarrow> k \<le> Min"
914 "Bit0 k \<le> Bit0 l \<longleftrightarrow> k \<le> l"
915 "Bit0 k \<le> Bit1 l \<longleftrightarrow> k \<le> l"
916 "Bit1 k \<le> Bit0 l \<longleftrightarrow> k < l"
917 "Bit1 k \<le> Bit1 l \<longleftrightarrow> k \<le> l"
918 unfolding not_less [symmetric]
919 by (simp_all add: not_le)
923 lemma eq_bin_simps [simp]:
924 "Pls = Pls \<longleftrightarrow> True"
925 "Pls = Min \<longleftrightarrow> False"
926 "Pls = Bit0 l \<longleftrightarrow> Pls = l"
927 "Pls = Bit1 l \<longleftrightarrow> False"
928 "Min = Pls \<longleftrightarrow> False"
929 "Min = Min \<longleftrightarrow> True"
930 "Min = Bit0 l \<longleftrightarrow> False"
931 "Min = Bit1 l \<longleftrightarrow> Min = l"
932 "Bit0 k = Pls \<longleftrightarrow> k = Pls"
933 "Bit0 k = Min \<longleftrightarrow> False"
934 "Bit1 k = Pls \<longleftrightarrow> False"
935 "Bit1 k = Min \<longleftrightarrow> k = Min"
936 "Bit0 k = Bit0 l \<longleftrightarrow> k = l"
937 "Bit0 k = Bit1 l \<longleftrightarrow> False"
938 "Bit1 k = Bit0 l \<longleftrightarrow> False"
939 "Bit1 k = Bit1 l \<longleftrightarrow> k = l"
940 unfolding order_eq_iff [where 'a=int]
941 by (simp_all add: not_less)
944 subsection {* Converting Numerals to Rings: @{term number_of} *}
946 class number_ring = number + comm_ring_1 +
947 assumes number_of_eq: "number_of k = of_int k"
949 class number_semiring = number + comm_semiring_1 +
950 assumes number_of_int: "number_of (int n) = of_nat n"
952 instance number_ring \<subseteq> number_semiring
954 fix n show "number_of (int n) = (of_nat n :: 'a)"
955 unfolding number_of_eq by (rule of_int_of_nat_eq)
958 text {* self-embedding of the integers *}
960 instantiation int :: number_ring
964 int_number_of_def: "number_of w = (of_int w \<Colon> int)"
967 qed (simp only: int_number_of_def)
971 lemma number_of_is_id:
972 "number_of (k::int) = k"
973 unfolding int_number_of_def by simp
975 lemma number_of_succ:
976 "number_of (succ k) = (1 + number_of k ::'a::number_ring)"
977 unfolding number_of_eq numeral_simps by simp
979 lemma number_of_pred:
980 "number_of (pred w) = (- 1 + number_of w ::'a::number_ring)"
981 unfolding number_of_eq numeral_simps by simp
983 lemma number_of_minus:
984 "number_of (uminus w) = (- (number_of w)::'a::number_ring)"
985 unfolding number_of_eq by (rule of_int_minus)
988 "number_of (v + w) = (number_of v + number_of w::'a::number_ring)"
989 unfolding number_of_eq by (rule of_int_add)
991 lemma number_of_diff:
992 "number_of (v - w) = (number_of v - number_of w::'a::number_ring)"
993 unfolding number_of_eq by (rule of_int_diff)
995 lemma number_of_mult:
996 "number_of (v * w) = (number_of v * number_of w::'a::number_ring)"
997 unfolding number_of_eq by (rule of_int_mult)
1000 The correctness of shifting.
1001 But it doesn't seem to give a measurable speed-up.
1004 lemma double_number_of_Bit0:
1005 "(1 + 1) * number_of w = (number_of (Bit0 w) ::'a::number_ring)"
1006 unfolding number_of_eq numeral_simps left_distrib by simp
1009 Converting numerals 0 and 1 to their abstract versions.
1012 lemma semiring_numeral_0_eq_0:
1013 "Numeral0 = (0::'a::number_semiring)"
1014 using number_of_int [where 'a='a and n=0]
1015 unfolding numeral_simps by simp
1017 lemma semiring_numeral_1_eq_1:
1018 "Numeral1 = (1::'a::number_semiring)"
1019 using number_of_int [where 'a='a and n=1]
1020 unfolding numeral_simps by simp
1022 lemma numeral_0_eq_0 [simp, code_post]:
1023 "Numeral0 = (0::'a::number_ring)"
1024 by (rule semiring_numeral_0_eq_0)
1026 lemma numeral_1_eq_1 [simp, code_post]:
1027 "Numeral1 = (1::'a::number_ring)"
1028 by (rule semiring_numeral_1_eq_1)
1031 Special-case simplification for small constants.
1035 Unary minus for the abstract constant 1. Cannot be inserted
1036 as a simprule until later: it is @{text number_of_Min} re-oriented!
1039 lemma numeral_m1_eq_minus_1:
1040 "(-1::'a::number_ring) = - 1"
1041 unfolding number_of_eq numeral_simps by simp
1043 lemma mult_minus1 [simp]:
1044 "-1 * z = -(z::'a::number_ring)"
1045 unfolding number_of_eq numeral_simps by simp
1047 lemma mult_minus1_right [simp]:
1048 "z * -1 = -(z::'a::number_ring)"
1049 unfolding number_of_eq numeral_simps by simp
1051 (*Negation of a coefficient*)
1052 lemma minus_number_of_mult [simp]:
1053 "- (number_of w) * z = number_of (uminus w) * (z::'a::number_ring)"
1054 unfolding number_of_eq by simp
1056 text {* Subtraction *}
1058 lemma diff_number_of_eq:
1059 "number_of v - number_of w =
1060 (number_of (v + uminus w)::'a::number_ring)"
1061 unfolding number_of_eq by simp
1063 lemma number_of_Pls:
1064 "number_of Pls = (0::'a::number_ring)"
1065 unfolding number_of_eq numeral_simps by simp
1067 lemma number_of_Min:
1068 "number_of Min = (- 1::'a::number_ring)"
1069 unfolding number_of_eq numeral_simps by simp
1071 lemma number_of_Bit0:
1072 "number_of (Bit0 w) = (0::'a::number_ring) + (number_of w) + (number_of w)"
1073 unfolding number_of_eq numeral_simps by simp
1075 lemma number_of_Bit1:
1076 "number_of (Bit1 w) = (1::'a::number_ring) + (number_of w) + (number_of w)"
1077 unfolding number_of_eq numeral_simps by simp
1080 subsubsection {* Equality of Binary Numbers *}
1082 text {* First version by Norbert Voelker *}
1084 definition (*for simplifying equalities*) iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool" where
1085 "iszero z \<longleftrightarrow> z = 0"
1087 lemma iszero_0: "iszero 0"
1088 by (simp add: iszero_def)
1090 lemma iszero_Numeral0: "iszero (Numeral0 :: 'a::number_ring)"
1091 by (simp add: iszero_0)
1093 lemma not_iszero_1: "\<not> iszero 1"
1094 by (simp add: iszero_def)
1096 lemma not_iszero_Numeral1: "\<not> iszero (Numeral1 :: 'a::number_ring)"
1097 by (simp add: not_iszero_1)
1099 lemma eq_number_of_eq [simp]:
1100 "((number_of x::'a::number_ring) = number_of y) =
1101 iszero (number_of (x + uminus y) :: 'a)"
1102 unfolding iszero_def number_of_add number_of_minus
1103 by (simp add: algebra_simps)
1105 lemma iszero_number_of_Pls:
1106 "iszero ((number_of Pls)::'a::number_ring)"
1107 unfolding iszero_def numeral_0_eq_0 ..
1109 lemma nonzero_number_of_Min:
1110 "~ iszero ((number_of Min)::'a::number_ring)"
1111 unfolding iszero_def numeral_m1_eq_minus_1 by simp
1114 subsubsection {* Comparisons, for Ordered Rings *}
1116 lemmas double_eq_0_iff = double_zero
1119 "1 + z + z \<noteq> (0::int)"
1122 have le: "0 \<le> z+z" by (simp add: nonneg add_increasing)
1123 thus ?thesis using le_imp_0_less [OF le]
1124 by (auto simp add: add_assoc)
1129 assume eq: "1 + z + z = 0"
1130 have "(0::int) < 1 + (int n + int n)"
1131 by (simp add: le_imp_0_less add_increasing)
1132 also have "... = - (1 + z + z)"
1133 by (simp add: neg add_assoc [symmetric])
1134 also have "... = 0" by (simp add: eq)
1135 finally have "0<0" ..
1140 lemma iszero_number_of_Bit0:
1141 "iszero (number_of (Bit0 w)::'a) =
1142 iszero (number_of w::'a::{ring_char_0,number_ring})"
1144 have "(of_int w + of_int w = (0::'a)) \<Longrightarrow> (w = 0)"
1146 assume eq: "of_int w + of_int w = (0::'a)"
1147 then have "of_int (w + w) = (of_int 0 :: 'a)" by simp
1148 then have "w + w = 0" by (simp only: of_int_eq_iff)
1149 then show "w = 0" by (simp only: double_eq_0_iff)
1152 by (auto simp add: iszero_def number_of_eq numeral_simps)
1155 lemma iszero_number_of_Bit1:
1156 "~ iszero (number_of (Bit1 w)::'a::{ring_char_0,number_ring})"
1158 have "1 + of_int w + of_int w \<noteq> (0::'a)"
1160 assume eq: "1 + of_int w + of_int w = (0::'a)"
1161 hence "of_int (1 + w + w) = (of_int 0 :: 'a)" by simp
1162 hence "1 + w + w = 0" by (simp only: of_int_eq_iff)
1163 with odd_nonzero show False by blast
1166 by (auto simp add: iszero_def number_of_eq numeral_simps)
1169 lemmas iszero_simps [simp] =
1170 iszero_0 not_iszero_1
1171 iszero_number_of_Pls nonzero_number_of_Min
1172 iszero_number_of_Bit0 iszero_number_of_Bit1
1173 (* iszero_number_of_Pls would never normally be used
1174 because its lhs simplifies to "iszero 0" *)
1176 subsubsection {* The Less-Than Relation *}
1178 lemma double_less_0_iff:
1179 "(a + a < 0) = (a < (0::'a::linordered_idom))"
1181 have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)
1182 also have "... = (a < 0)"
1183 by (simp add: mult_less_0_iff zero_less_two
1184 order_less_not_sym [OF zero_less_two])
1185 finally show ?thesis .
1189 "(1 + z + z < 0) = (z < (0::int))"
1193 by (simp add: linorder_not_less add_assoc add_increasing
1194 le_imp_0_less [THEN order_less_imp_le])
1198 by (simp del: of_nat_Suc of_nat_add of_nat_1
1199 add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric])
1202 text {* Less-Than or Equals *}
1204 text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *}
1206 lemmas le_number_of_eq_not_less =
1207 linorder_not_less [of "number_of w" "number_of v", symmetric,
1211 text {* Absolute value (@{term abs}) *}
1213 lemma abs_number_of:
1214 "abs(number_of x::'a::{linordered_idom,number_ring}) =
1215 (if number_of x < (0::'a) then -number_of x else number_of x)"
1216 by (simp add: abs_if)
1219 text {* Re-orientation of the equation nnn=x *}
1221 lemma number_of_reorient:
1222 "(number_of w = x) = (x = number_of w)"
1226 subsubsection {* Simplification of arithmetic operations on integer constants. *}
1228 lemmas arith_extra_simps [standard, simp] =
1229 number_of_add [symmetric]
1230 number_of_minus [symmetric]
1231 numeral_m1_eq_minus_1 [symmetric]
1232 number_of_mult [symmetric]
1233 diff_number_of_eq abs_number_of
1236 For making a minimal simpset, one must include these default simprules.
1237 Also include @{text simp_thms}.
1240 lemmas arith_simps =
1241 normalize_bin_simps pred_bin_simps succ_bin_simps
1242 add_bin_simps minus_bin_simps mult_bin_simps
1243 abs_zero abs_one arith_extra_simps
1245 text {* Simplification of relational operations *}
1247 lemma less_number_of [simp]:
1248 "(number_of x::'a::{linordered_idom,number_ring}) < number_of y \<longleftrightarrow> x < y"
1249 unfolding number_of_eq by (rule of_int_less_iff)
1251 lemma le_number_of [simp]:
1252 "(number_of x::'a::{linordered_idom,number_ring}) \<le> number_of y \<longleftrightarrow> x \<le> y"
1253 unfolding number_of_eq by (rule of_int_le_iff)
1255 lemma eq_number_of [simp]:
1256 "(number_of x::'a::{ring_char_0,number_ring}) = number_of y \<longleftrightarrow> x = y"
1257 unfolding number_of_eq by (rule of_int_eq_iff)
1260 less_number_of less_bin_simps
1261 le_number_of le_bin_simps
1262 eq_number_of_eq eq_bin_simps
1266 subsubsection {* Simplification of arithmetic when nested to the right. *}
1268 lemma add_number_of_left [simp]:
1269 "number_of v + (number_of w + z) =
1270 (number_of(v + w) + z::'a::number_ring)"
1271 by (simp add: add_assoc [symmetric])
1273 lemma mult_number_of_left [simp]:
1274 "number_of v * (number_of w * z) =
1275 (number_of(v * w) * z::'a::number_ring)"
1276 by (simp add: mult_assoc [symmetric])
1278 lemma add_number_of_diff1:
1279 "number_of v + (number_of w - c) =
1280 number_of(v + w) - (c::'a::number_ring)"
1281 by (simp add: diff_minus)
1283 lemma add_number_of_diff2 [simp]:
1284 "number_of v + (c - number_of w) =
1285 number_of (v + uminus w) + (c::'a::number_ring)"
1286 by (simp add: algebra_simps diff_number_of_eq [symmetric])
1291 subsection {* The Set of Integers *}
1296 definition Ints :: "'a set" where
1297 "Ints = range of_int"
1302 lemma Ints_of_int [simp]: "of_int z \<in> \<int>"
1303 by (simp add: Ints_def)
1305 lemma Ints_of_nat [simp]: "of_nat n \<in> \<int>"
1306 apply (simp add: Ints_def)
1307 apply (rule range_eqI)
1308 apply (rule of_int_of_nat_eq [symmetric])
1311 lemma Ints_0 [simp]: "0 \<in> \<int>"
1312 apply (simp add: Ints_def)
1313 apply (rule range_eqI)
1314 apply (rule of_int_0 [symmetric])
1317 lemma Ints_1 [simp]: "1 \<in> \<int>"
1318 apply (simp add: Ints_def)
1319 apply (rule range_eqI)
1320 apply (rule of_int_1 [symmetric])
1323 lemma Ints_add [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a + b \<in> \<int>"
1324 apply (auto simp add: Ints_def)
1325 apply (rule range_eqI)
1326 apply (rule of_int_add [symmetric])
1329 lemma Ints_minus [simp]: "a \<in> \<int> \<Longrightarrow> -a \<in> \<int>"
1330 apply (auto simp add: Ints_def)
1331 apply (rule range_eqI)
1332 apply (rule of_int_minus [symmetric])
1335 lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a - b \<in> \<int>"
1336 apply (auto simp add: Ints_def)
1337 apply (rule range_eqI)
1338 apply (rule of_int_diff [symmetric])
1341 lemma Ints_mult [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a * b \<in> \<int>"
1342 apply (auto simp add: Ints_def)
1343 apply (rule range_eqI)
1344 apply (rule of_int_mult [symmetric])
1347 lemma Ints_power [simp]: "a \<in> \<int> \<Longrightarrow> a ^ n \<in> \<int>"
1348 by (induct n) simp_all
1350 lemma Ints_cases [cases set: Ints]:
1351 assumes "q \<in> \<int>"
1352 obtains (of_int) z where "q = of_int z"
1355 from `q \<in> \<int>` have "q \<in> range of_int" unfolding Ints_def .
1356 then obtain z where "q = of_int z" ..
1360 lemma Ints_induct [case_names of_int, induct set: Ints]:
1361 "q \<in> \<int> \<Longrightarrow> (\<And>z. P (of_int z)) \<Longrightarrow> P q"
1362 by (rule Ints_cases) auto
1366 text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
1368 lemma Ints_double_eq_0_iff:
1369 assumes in_Ints: "a \<in> Ints"
1370 shows "(a + a = 0) = (a = (0::'a::ring_char_0))"
1372 from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
1373 then obtain z where a: "a = of_int z" ..
1377 thus "a + a = 0" by simp
1379 assume eq: "a + a = 0"
1380 hence "of_int (z + z) = (of_int 0 :: 'a)" by (simp add: a)
1381 hence "z + z = 0" by (simp only: of_int_eq_iff)
1382 hence "z = 0" by (simp only: double_eq_0_iff)
1383 thus "a = 0" by (simp add: a)
1387 lemma Ints_odd_nonzero:
1388 assumes in_Ints: "a \<in> Ints"
1389 shows "1 + a + a \<noteq> (0::'a::ring_char_0)"
1391 from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
1392 then obtain z where a: "a = of_int z" ..
1395 assume eq: "1 + a + a = 0"
1396 hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
1397 hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
1398 with odd_nonzero show False by blast
1402 lemma Ints_number_of [simp]:
1403 "(number_of w :: 'a::number_ring) \<in> Ints"
1404 unfolding number_of_eq Ints_def by simp
1406 lemma Nats_number_of [simp]:
1407 "Int.Pls \<le> w \<Longrightarrow> (number_of w :: 'a::number_ring) \<in> Nats"
1408 unfolding Int.Pls_def number_of_eq
1409 by (simp only: of_nat_nat [symmetric] of_nat_in_Nats)
1411 lemma Ints_odd_less_0:
1412 assumes in_Ints: "a \<in> Ints"
1413 shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))"
1415 from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
1416 then obtain z where a: "a = of_int z" ..
1417 hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
1419 also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0)
1420 also have "... = (a < 0)" by (simp add: a)
1421 finally show ?thesis .
1425 subsection {* @{term setsum} and @{term setprod} *}
1427 lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
1428 apply (cases "finite A")
1429 apply (erule finite_induct, auto)
1432 lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
1433 apply (cases "finite A")
1434 apply (erule finite_induct, auto)
1437 lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
1438 apply (cases "finite A")
1439 apply (erule finite_induct, auto simp add: of_nat_mult)
1442 lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
1443 apply (cases "finite A")
1444 apply (erule finite_induct, auto)
1447 lemmas int_setsum = of_nat_setsum [where 'a=int]
1448 lemmas int_setprod = of_nat_setprod [where 'a=int]
1451 subsection{*Inequality Reasoning for the Arithmetic Simproc*}
1453 lemma add_numeral_0: "Numeral0 + a = (a::'a::number_ring)"
1456 lemma add_numeral_0_right: "a + Numeral0 = (a::'a::number_ring)"
1459 lemma mult_numeral_1: "Numeral1 * a = (a::'a::number_ring)"
1462 lemma mult_numeral_1_right: "a * Numeral1 = (a::'a::number_ring)"
1465 lemma divide_numeral_1: "a / Numeral1 = (a::'a::{number_ring,field})"
1468 lemma inverse_numeral_1:
1469 "inverse Numeral1 = (Numeral1::'a::{number_ring,field})"
1472 text{*Theorem lists for the cancellation simprocs. The use of binary numerals
1473 for 0 and 1 reduces the number of special cases.*}
1475 lemmas add_0s = add_numeral_0 add_numeral_0_right
1476 lemmas mult_1s = mult_numeral_1 mult_numeral_1_right
1477 mult_minus1 mult_minus1_right
1480 subsection{*Special Arithmetic Rules for Abstract 0 and 1*}
1482 text{*Arithmetic computations are defined for binary literals, which leaves 0
1483 and 1 as special cases. Addition already has rules for 0, but not 1.
1484 Multiplication and unary minus already have rules for both 0 and 1.*}
1487 lemma binop_eq: "[|f x y = g x y; x = x'; y = y'|] ==> f x' y' = g x' y'"
1491 lemmas add_number_of_eq = number_of_add [symmetric]
1493 text{*Allow 1 on either or both sides*}
1494 lemma semiring_one_add_one_is_two: "1 + 1 = (2::'a::number_semiring)"
1495 using number_of_int [where 'a='a and n="Suc (Suc 0)"]
1496 by (simp add: numeral_simps)
1498 lemma one_add_one_is_two: "1 + 1 = (2::'a::number_ring)"
1499 by (rule semiring_one_add_one_is_two)
1501 lemmas add_special =
1503 binop_eq [of "op +", OF add_number_of_eq numeral_1_eq_1 refl, standard]
1504 binop_eq [of "op +", OF add_number_of_eq refl numeral_1_eq_1, standard]
1506 text{*Allow 1 on either or both sides (1-1 already simplifies to 0)*}
1507 lemmas diff_special =
1508 binop_eq [of "op -", OF diff_number_of_eq numeral_1_eq_1 refl, standard]
1509 binop_eq [of "op -", OF diff_number_of_eq refl numeral_1_eq_1, standard]
1511 text{*Allow 0 or 1 on either side with a binary numeral on the other*}
1513 binop_eq [of "op =", OF eq_number_of_eq numeral_0_eq_0 refl, standard]
1514 binop_eq [of "op =", OF eq_number_of_eq numeral_1_eq_1 refl, standard]
1515 binop_eq [of "op =", OF eq_number_of_eq refl numeral_0_eq_0, standard]
1516 binop_eq [of "op =", OF eq_number_of_eq refl numeral_1_eq_1, standard]
1518 text{*Allow 0 or 1 on either side with a binary numeral on the other*}
1519 lemmas less_special =
1520 binop_eq [of "op <", OF less_number_of numeral_0_eq_0 refl, standard]
1521 binop_eq [of "op <", OF less_number_of numeral_1_eq_1 refl, standard]
1522 binop_eq [of "op <", OF less_number_of refl numeral_0_eq_0, standard]
1523 binop_eq [of "op <", OF less_number_of refl numeral_1_eq_1, standard]
1525 text{*Allow 0 or 1 on either side with a binary numeral on the other*}
1527 binop_eq [of "op \<le>", OF le_number_of numeral_0_eq_0 refl, standard]
1528 binop_eq [of "op \<le>", OF le_number_of numeral_1_eq_1 refl, standard]
1529 binop_eq [of "op \<le>", OF le_number_of refl numeral_0_eq_0, standard]
1530 binop_eq [of "op \<le>", OF le_number_of refl numeral_1_eq_1, standard]
1532 lemmas arith_special[simp] =
1533 add_special diff_special eq_special less_special le_special
1536 text {* Legacy theorems *}
1538 lemmas zle_int = of_nat_le_iff [where 'a=int]
1539 lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
1541 subsection {* Setting up simplification procedures *}
1543 lemmas int_arith_rules =
1544 neg_le_iff_le numeral_0_eq_0 numeral_1_eq_1
1545 minus_zero diff_minus left_minus right_minus
1546 mult_zero_left mult_zero_right mult_Bit1 mult_1_left mult_1_right
1547 mult_minus_left mult_minus_right
1548 minus_add_distrib minus_minus mult_assoc
1549 of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
1550 of_int_0 of_int_1 of_int_add of_int_mult
1552 use "Tools/int_arith.ML"
1553 declaration {* K Int_Arith.setup *}
1555 simproc_setup fast_arith ("(m::'a::{linordered_idom,number_ring}) < n" |
1556 "(m::'a::{linordered_idom,number_ring}) <= n" |
1557 "(m::'a::{linordered_idom,number_ring}) = n") =
1558 {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *}
1562 (fn Const (@{const_name number_of}, _) $ _ => true | _ => false)
1565 simproc_setup reorient_numeral ("number_of w = x") = Reorient_Proc.proc
1568 subsection{*Lemmas About Small Numerals*}
1570 lemma of_int_m1 [simp]: "of_int -1 = (-1 :: 'a :: number_ring)"
1572 have "(of_int -1 :: 'a) = of_int (- 1)" by simp
1573 also have "... = - of_int 1" by (simp only: of_int_minus)
1574 also have "... = -1" by simp
1575 finally show ?thesis .
1578 lemma abs_minus_one [simp]: "abs (-1) = (1::'a::{linordered_idom,number_ring})"
1579 by (simp add: abs_if)
1581 lemma abs_power_minus_one [simp]:
1582 "abs(-1 ^ n) = (1::'a::{linordered_idom,number_ring})"
1583 by (simp add: power_abs)
1585 lemma of_int_number_of_eq [simp]:
1586 "of_int (number_of v) = (number_of v :: 'a :: number_ring)"
1587 by (simp add: number_of_eq)
1589 text{*Lemmas for specialist use, NOT as default simprules*}
1590 (* TODO: see if semiring duplication can be removed without breaking proofs *)
1591 lemma semiring_mult_2: "2 * z = (z+z::'a::number_semiring)"
1592 unfolding semiring_one_add_one_is_two [symmetric] left_distrib by simp
1594 lemma semiring_mult_2_right: "z * 2 = (z+z::'a::number_semiring)"
1595 by (subst mult_commute, rule semiring_mult_2)
1597 lemma mult_2: "2 * z = (z+z::'a::number_ring)"
1598 by (rule semiring_mult_2)
1600 lemma mult_2_right: "z * 2 = (z+z::'a::number_ring)"
1601 by (rule semiring_mult_2_right)
1604 subsection{*More Inequality Reasoning*}
1606 lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
1609 lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
1612 lemma zle_diff1_eq [simp]: "(w \<le> z - (1::int)) = (w<z)"
1615 lemma zle_add1_eq_le [simp]: "(w < z + (1::int)) = (w\<le>z)"
1618 lemma int_one_le_iff_zero_less: "((1::int) \<le> z) = (0 < z)"
1622 subsection{*The functions @{term nat} and @{term int}*}
1624 text{*Simplify the terms @{term "int 0"}, @{term "int(Suc 0)"} and
1626 declare Zero_int_def [symmetric, simp]
1627 declare One_int_def [symmetric, simp]
1629 lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp]
1631 lemma nat_0 [simp]: "nat 0 = 0"
1632 by (simp add: nat_eq_iff)
1634 lemma nat_1: "nat 1 = Suc 0"
1635 by (subst nat_eq_iff, simp)
1637 lemma nat_2: "nat 2 = Suc (Suc 0)"
1638 by (subst nat_eq_iff, simp)
1640 lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
1641 apply (insert zless_nat_conj [of 1 z])
1642 apply (auto simp add: nat_1)
1645 text{*This simplifies expressions of the form @{term "int n = z"} where
1646 z is an integer literal.*}
1647 lemmas int_eq_iff_number_of [simp] = int_eq_iff [of _ "number_of v", standard]
1649 lemma split_nat [arith_split]:
1650 "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
1651 (is "?P = (?L & ?R)")
1652 proof (cases "i < 0")
1653 case True thus ?thesis by auto
1658 assume ?P thus ?L using False by clarsimp
1660 assume ?L thus ?P using False by simp
1662 with False show ?thesis by simp
1668 lemma of_int_of_nat [nitpick_simp]:
1669 "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))"
1670 proof (cases "k < 0")
1671 case True then have "0 \<le> - k" by simp
1672 then have "of_nat (nat (- k)) = of_int (- k)" by (rule of_nat_nat)
1673 with True show ?thesis by simp
1675 case False then show ?thesis by (simp add: not_less of_nat_nat)
1680 lemma nat_mult_distrib:
1683 shows "nat (z * z') = nat z * nat z'"
1684 proof (cases "0 \<le> z'")
1685 case False with assms have "z * z' \<le> 0"
1686 by (simp add: not_le mult_le_0_iff)
1687 then have "nat (z * z') = 0" by simp
1688 moreover from False have "nat z' = 0" by simp
1689 ultimately show ?thesis by simp
1691 case True with assms have ge_0: "z * z' \<ge> 0" by (simp add: zero_le_mult_iff)
1693 by (rule injD [of "of_nat :: nat \<Rightarrow> int", OF inj_of_nat])
1694 (simp only: of_nat_mult of_nat_nat [OF True]
1695 of_nat_nat [OF assms] of_nat_nat [OF ge_0], simp)
1698 lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"
1700 apply (rule_tac [2] nat_mult_distrib, auto)
1703 lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
1704 apply (cases "z=0 | w=0")
1705 apply (auto simp add: abs_if nat_mult_distrib [symmetric]
1706 nat_mult_distrib_neg [symmetric] mult_less_0_iff)
1710 subsection "Induction principles for int"
1712 text{*Well-founded segments of the integers*}
1715 int_ge_less_than :: "int => (int * int) set"
1717 "int_ge_less_than d = {(z',z). d \<le> z' & z' < z}"
1719 theorem wf_int_ge_less_than: "wf (int_ge_less_than d)"
1721 have "int_ge_less_than d \<subseteq> measure (%z. nat (z-d))"
1722 by (auto simp add: int_ge_less_than_def)
1724 by (rule wf_subset [OF wf_measure])
1727 text{*This variant looks odd, but is typical of the relations suggested
1731 int_ge_less_than2 :: "int => (int * int) set"
1733 "int_ge_less_than2 d = {(z',z). d \<le> z & z' < z}"
1735 theorem wf_int_ge_less_than2: "wf (int_ge_less_than2 d)"
1737 have "int_ge_less_than2 d \<subseteq> measure (%z. nat (1+z-d))"
1738 by (auto simp add: int_ge_less_than2_def)
1740 by (rule wf_subset [OF wf_measure])
1743 (* `set:int': dummy construction *)
1744 theorem int_ge_induct [case_names base step, induct set: int]:
1746 assumes ge: "k \<le> i" and
1748 step: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
1752 have "\<And>i::int. n = nat (i - k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i"
1755 hence "i = k" by arith
1756 thus "P i" using base by simp
1759 then have "n = nat((i - 1) - k)" by arith
1761 have ki1: "k \<le> i - 1" using Suc.prems by arith
1763 have "P (i - 1)" by (rule Suc.hyps)
1764 from step [OF ki1 this] show ?case by simp
1767 with ge show ?thesis by fast
1770 (* `set:int': dummy construction *)
1771 theorem int_gr_induct [case_names base step, induct set: int]:
1772 assumes gr: "k < (i::int)" and
1774 step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
1776 apply(rule int_ge_induct[of "k + 1"])
1777 using gr apply arith
1779 apply (rule step, simp+)
1782 theorem int_le_induct [consumes 1, case_names base step]:
1783 assumes le: "i \<le> (k::int)" and
1785 step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
1789 have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i"
1792 hence "i = k" by arith
1793 thus "P i" using base by simp
1796 hence "n = nat (k - (i + 1))" by arith
1798 have ki1: "i + 1 \<le> k" using Suc.prems by arith
1800 have "P (i + 1)" by(rule Suc.hyps)
1801 from step[OF ki1 this] show ?case by simp
1804 with le show ?thesis by fast
1807 theorem int_less_induct [consumes 1, case_names base step]:
1808 assumes less: "(i::int) < k" and
1809 base: "P(k - 1)" and
1810 step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
1812 apply(rule int_le_induct[of _ "k - 1"])
1813 using less apply arith
1815 apply (rule step, simp+)
1818 theorem int_induct [case_names base step1 step2]:
1821 and step1: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
1822 and step2: "\<And>i. k \<ge> i \<Longrightarrow> P i \<Longrightarrow> P (i - 1)"
1825 have "i \<le> k \<or> i \<ge> k" by arith
1829 then show ?thesis using base
1830 by (rule int_ge_induct) (fact step1)
1833 then show ?thesis using base
1834 by (rule int_le_induct) (fact step2)
1838 subsection{*Intermediate value theorems*}
1840 lemma int_val_lemma:
1841 "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->
1842 f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
1843 unfolding One_nat_def
1847 apply (erule impE, simp)
1848 apply (erule_tac x = n in allE, simp)
1849 apply (case_tac "k = f (Suc n)")
1852 apply (simp add: abs_if split add: split_if_asm)
1853 apply (blast intro: le_SucI)
1856 lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
1858 lemma nat_intermed_int_val:
1859 "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;
1860 f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
1861 apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k
1863 unfolding One_nat_def
1866 apply (rule_tac x = "i+m" in exI, arith)
1870 subsection{*Products and 1, by T. M. Rasmussen*}
1872 lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))"
1875 lemma abs_zmult_eq_1:
1876 assumes mn: "\<bar>m * n\<bar> = 1"
1877 shows "\<bar>m\<bar> = (1::int)"
1879 have 0: "m \<noteq> 0 & n \<noteq> 0" using mn
1881 have "~ (2 \<le> \<bar>m\<bar>)"
1883 assume "2 \<le> \<bar>m\<bar>"
1884 hence "2*\<bar>n\<bar> \<le> \<bar>m\<bar>*\<bar>n\<bar>"
1885 by (simp add: mult_mono 0)
1886 also have "... = \<bar>m*n\<bar>"
1887 by (simp add: abs_mult)
1890 finally have "2*\<bar>n\<bar> \<le> 1" .
1891 thus "False" using 0
1894 thus ?thesis using 0
1898 lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1"
1899 by (insert abs_zmult_eq_1 [of m n], arith)
1901 lemma pos_zmult_eq_1_iff:
1902 assumes "0 < (m::int)" shows "(m * n = 1) = (m = 1 & n = 1)"
1904 from assms have "m * n = 1 ==> m = 1" by (auto dest: pos_zmult_eq_1_iff_lemma)
1905 thus ?thesis by (auto dest: pos_zmult_eq_1_iff_lemma)
1908 lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
1910 apply (frule pos_zmult_eq_1_iff_lemma)
1911 apply (simp add: mult_commute [of m])
1912 apply (frule pos_zmult_eq_1_iff_lemma, auto)
1915 lemma infinite_UNIV_int: "\<not> finite (UNIV::int set)"
1917 assume "finite (UNIV::int set)"
1918 moreover have "inj (\<lambda>i\<Colon>int. 2 * i)"
1920 ultimately have "surj (\<lambda>i\<Colon>int. 2 * i)"
1921 by (rule finite_UNIV_inj_surj)
1922 then obtain i :: int where "1 = 2 * i" by (rule surjE)
1923 then show False by (simp add: pos_zmult_eq_1_iff)
1927 subsection {* Further theorems on numerals *}
1929 subsubsection{*Special Simplification for Constants*}
1931 text{*These distributive laws move literals inside sums and differences.*}
1933 lemmas left_distrib_number_of [simp] =
1934 left_distrib [of _ _ "number_of v", standard]
1936 lemmas right_distrib_number_of [simp] =
1937 right_distrib [of "number_of v", standard]
1939 lemmas left_diff_distrib_number_of [simp] =
1940 left_diff_distrib [of _ _ "number_of v", standard]
1942 lemmas right_diff_distrib_number_of [simp] =
1943 right_diff_distrib [of "number_of v", standard]
1945 text{*These are actually for fields, like real: but where else to put them?*}
1947 lemmas zero_less_divide_iff_number_of [simp, no_atp] =
1948 zero_less_divide_iff [of "number_of w", standard]
1950 lemmas divide_less_0_iff_number_of [simp, no_atp] =
1951 divide_less_0_iff [of "number_of w", standard]
1953 lemmas zero_le_divide_iff_number_of [simp, no_atp] =
1954 zero_le_divide_iff [of "number_of w", standard]
1956 lemmas divide_le_0_iff_number_of [simp, no_atp] =
1957 divide_le_0_iff [of "number_of w", standard]
1960 text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}. It looks
1961 strange, but then other simprocs simplify the quotient.*}
1963 lemmas inverse_eq_divide_number_of [simp] =
1964 inverse_eq_divide [of "number_of w", standard]
1966 text {*These laws simplify inequalities, moving unary minus from a term
1969 lemmas less_minus_iff_number_of [simp, no_atp] =
1970 less_minus_iff [of "number_of v", standard]
1972 lemmas le_minus_iff_number_of [simp, no_atp] =
1973 le_minus_iff [of "number_of v", standard]
1975 lemmas equation_minus_iff_number_of [simp, no_atp] =
1976 equation_minus_iff [of "number_of v", standard]
1978 lemmas minus_less_iff_number_of [simp, no_atp] =
1979 minus_less_iff [of _ "number_of v", standard]
1981 lemmas minus_le_iff_number_of [simp, no_atp] =
1982 minus_le_iff [of _ "number_of v", standard]
1984 lemmas minus_equation_iff_number_of [simp, no_atp] =
1985 minus_equation_iff [of _ "number_of v", standard]
1988 text{*To Simplify Inequalities Where One Side is the Constant 1*}
1990 lemma less_minus_iff_1 [simp,no_atp]:
1991 fixes b::"'b::{linordered_idom,number_ring}"
1992 shows "(1 < - b) = (b < -1)"
1995 lemma le_minus_iff_1 [simp,no_atp]:
1996 fixes b::"'b::{linordered_idom,number_ring}"
1997 shows "(1 \<le> - b) = (b \<le> -1)"
2000 lemma equation_minus_iff_1 [simp,no_atp]:
2001 fixes b::"'b::number_ring"
2002 shows "(1 = - b) = (b = -1)"
2003 by (subst equation_minus_iff, auto)
2005 lemma minus_less_iff_1 [simp,no_atp]:
2006 fixes a::"'b::{linordered_idom,number_ring}"
2007 shows "(- a < 1) = (-1 < a)"
2010 lemma minus_le_iff_1 [simp,no_atp]:
2011 fixes a::"'b::{linordered_idom,number_ring}"
2012 shows "(- a \<le> 1) = (-1 \<le> a)"
2015 lemma minus_equation_iff_1 [simp,no_atp]:
2016 fixes a::"'b::number_ring"
2017 shows "(- a = 1) = (a = -1)"
2018 by (subst minus_equation_iff, auto)
2021 text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
2023 lemmas mult_less_cancel_left_number_of [simp, no_atp] =
2024 mult_less_cancel_left [of "number_of v", standard]
2026 lemmas mult_less_cancel_right_number_of [simp, no_atp] =
2027 mult_less_cancel_right [of _ "number_of v", standard]
2029 lemmas mult_le_cancel_left_number_of [simp, no_atp] =
2030 mult_le_cancel_left [of "number_of v", standard]
2032 lemmas mult_le_cancel_right_number_of [simp, no_atp] =
2033 mult_le_cancel_right [of _ "number_of v", standard]
2036 text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
2038 lemmas le_divide_eq_number_of1 [simp] = le_divide_eq [of _ _ "number_of w", standard]
2039 lemmas divide_le_eq_number_of1 [simp] = divide_le_eq [of _ "number_of w", standard]
2040 lemmas less_divide_eq_number_of1 [simp] = less_divide_eq [of _ _ "number_of w", standard]
2041 lemmas divide_less_eq_number_of1 [simp] = divide_less_eq [of _ "number_of w", standard]
2042 lemmas eq_divide_eq_number_of1 [simp] = eq_divide_eq [of _ _ "number_of w", standard]
2043 lemmas divide_eq_eq_number_of1 [simp] = divide_eq_eq [of _ "number_of w", standard]
2046 subsubsection{*Optional Simplification Rules Involving Constants*}
2048 text{*Simplify quotients that are compared with a literal constant.*}
2050 lemmas le_divide_eq_number_of = le_divide_eq [of "number_of w", standard]
2051 lemmas divide_le_eq_number_of = divide_le_eq [of _ _ "number_of w", standard]
2052 lemmas less_divide_eq_number_of = less_divide_eq [of "number_of w", standard]
2053 lemmas divide_less_eq_number_of = divide_less_eq [of _ _ "number_of w", standard]
2054 lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w", standard]
2055 lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w", standard]
2058 text{*Not good as automatic simprules because they cause case splits.*}
2059 lemmas divide_const_simps =
2060 le_divide_eq_number_of divide_le_eq_number_of less_divide_eq_number_of
2061 divide_less_eq_number_of eq_divide_eq_number_of divide_eq_eq_number_of
2062 le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
2064 text{*Division By @{text "-1"}*}
2066 lemma divide_minus1 [simp]:
2067 "x/-1 = -(x::'a::{field_inverse_zero, number_ring})"
2070 lemma minus1_divide [simp]:
2071 "-1 / (x::'a::{field_inverse_zero, number_ring}) = - (1/x)"
2072 by (simp add: divide_inverse)
2074 lemma half_gt_zero_iff:
2075 "(0 < r/2) = (0 < (r::'a::{linordered_field_inverse_zero,number_ring}))"
2078 lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2, standard]
2080 lemma divide_Numeral1:
2081 "(x::'a::{field, number_ring}) / Numeral1 = x"
2084 lemma divide_Numeral0:
2085 "(x::'a::{field_inverse_zero, number_ring}) / Numeral0 = 0"
2089 subsection {* The divides relation *}
2091 lemma zdvd_antisym_nonneg:
2092 "0 <= m ==> 0 <= n ==> m dvd n ==> n dvd m ==> m = (n::int)"
2093 apply (simp add: dvd_def, auto)
2094 apply (auto simp add: mult_assoc zero_le_mult_iff zmult_eq_1_iff)
2097 lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a"
2098 shows "\<bar>a\<bar> = \<bar>b\<bar>"
2100 assume "a = 0" with assms show ?thesis by simp
2102 assume "a \<noteq> 0"
2103 from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast
2104 from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast
2105 from k k' have "a = a*k*k'" by simp
2106 with mult_cancel_left1[where c="a" and b="k*k'"]
2107 have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult_assoc)
2108 hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff)
2109 thus ?thesis using k k' by auto
2112 lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
2113 apply (subgoal_tac "m = n + (m - n)")
2114 apply (erule ssubst)
2115 apply (blast intro: dvd_add, simp)
2118 lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
2120 apply (erule_tac [2] dvd_add)
2121 apply (subgoal_tac "n = (n + k * m) - k * m")
2122 apply (erule ssubst)
2123 apply (erule dvd_diff)
2127 lemma dvd_imp_le_int:
2129 assumes "i \<noteq> 0" and "d dvd i"
2130 shows "\<bar>d\<bar> \<le> \<bar>i\<bar>"
2132 from `d dvd i` obtain k where "i = d * k" ..
2133 with `i \<noteq> 0` have "k \<noteq> 0" by auto
2134 then have "1 \<le> \<bar>k\<bar>" and "0 \<le> \<bar>d\<bar>" by auto
2135 then have "\<bar>d\<bar> * 1 \<le> \<bar>d\<bar> * \<bar>k\<bar>" by (rule mult_left_mono)
2136 with `i = d * k` show ?thesis by (simp add: abs_mult)
2139 lemma zdvd_not_zless:
2141 assumes "0 < m" and "m < n"
2142 shows "\<not> n dvd m"
2144 from assms have "0 < n" by auto
2145 assume "n dvd m" then obtain k where k: "m = n * k" ..
2146 with `0 < m` have "0 < n * k" by auto
2147 with `0 < n` have "0 < k" by (simp add: zero_less_mult_iff)
2148 with k `0 < n` `m < n` have "n * k < n * 1" by simp
2149 with `0 < n` `0 < k` show False unfolding mult_less_cancel_left by auto
2152 lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)"
2155 from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast
2156 {assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp
2157 with h have False by (simp add: mult_assoc)}
2158 hence "n = m * h" by blast
2159 thus ?thesis by simp
2162 theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
2164 have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"
2167 assume A: "int y = int x * k"
2171 with A have "y = x * n" by (simp add: of_nat_mult [symmetric])
2172 then show ?thesis ..
2175 with A have "int y = int x * (- int (Suc n))" by simp
2176 also have "\<dots> = - (int x * int (Suc n))" by (simp only: mult_minus_right)
2177 also have "\<dots> = - int (x * Suc n)" by (simp only: of_nat_mult [symmetric])
2178 finally have "- int (x * Suc n) = int y" ..
2179 then show ?thesis by (simp only: negative_eq_positive) auto
2182 then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left of_nat_mult)
2185 lemma zdvd1_eq[simp]: "(x::int) dvd 1 = (\<bar>x\<bar> = 1)"
2187 assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp
2188 hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
2189 hence "nat \<bar>x\<bar> = 1" by simp
2190 thus "\<bar>x\<bar> = 1" by (cases "x < 0") auto
2192 assume "\<bar>x\<bar>=1"
2193 then have "x = 1 \<or> x = -1" by auto
2194 then show "x dvd 1" by (auto intro: dvdI)
2197 lemma zdvd_mult_cancel1:
2198 assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
2200 assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m"
2201 by (cases "n >0") (auto simp add: minus_equation_iff)
2203 assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
2204 from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
2207 lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
2208 unfolding zdvd_int by (cases "z \<ge> 0") simp_all
2210 lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
2211 unfolding zdvd_int by (cases "z \<ge> 0") simp_all
2213 lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
2214 by (auto simp add: dvd_int_iff)
2216 lemma eq_nat_nat_iff:
2217 "0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat z = nat z' \<longleftrightarrow> z = z'"
2218 by (auto elim!: nonneg_eq_int)
2221 "0 \<le> z \<Longrightarrow> nat (z ^ n) = nat z ^ n"
2222 by (induct n) (simp_all add: nat_mult_distrib)
2224 lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
2226 apply (auto simp add: dvd_int_iff)
2228 apply (auto simp add: dvd_imp_le)
2234 shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)"
2236 from assms obtain k where "d = a * k" by (rule dvdE)
2239 assume "a dvd (x + t)"
2240 then obtain l where "x + t = a * l" by (rule dvdE)
2241 then have "x = a * l - t" by simp
2242 with `d = a * k` show "a dvd x + c * d + t" by simp
2244 assume "a dvd x + c * d + t"
2245 then obtain l where "x + c * d + t = a * l" by (rule dvdE)
2246 then have "x = a * l - c * d - t" by simp
2247 with `d = a * k` show "a dvd (x + t)" by simp
2252 subsection {* Configuration of the code generator *}
2254 code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int"
2256 lemmas pred_succ_numeral_code [code] =
2257 pred_bin_simps succ_bin_simps
2259 lemmas plus_numeral_code [code] =
2261 arith_extra_simps(1) [where 'a = int]
2263 lemmas minus_numeral_code [code] =
2265 arith_extra_simps(2) [where 'a = int]
2266 arith_extra_simps(5) [where 'a = int]
2268 lemmas times_numeral_code [code] =
2270 arith_extra_simps(4) [where 'a = int]
2272 instantiation int :: equal
2276 "HOL.equal k l \<longleftrightarrow> k - l = (0\<Colon>int)"
2278 instance by default (simp add: equal_int_def)
2282 lemma eq_number_of_int_code [code]:
2283 "HOL.equal (number_of k \<Colon> int) (number_of l) \<longleftrightarrow> HOL.equal k l"
2284 unfolding equal_int_def number_of_is_id ..
2286 lemma eq_int_code [code]:
2287 "HOL.equal Int.Pls Int.Pls \<longleftrightarrow> True"
2288 "HOL.equal Int.Pls Int.Min \<longleftrightarrow> False"
2289 "HOL.equal Int.Pls (Int.Bit0 k2) \<longleftrightarrow> HOL.equal Int.Pls k2"
2290 "HOL.equal Int.Pls (Int.Bit1 k2) \<longleftrightarrow> False"
2291 "HOL.equal Int.Min Int.Pls \<longleftrightarrow> False"
2292 "HOL.equal Int.Min Int.Min \<longleftrightarrow> True"
2293 "HOL.equal Int.Min (Int.Bit0 k2) \<longleftrightarrow> False"
2294 "HOL.equal Int.Min (Int.Bit1 k2) \<longleftrightarrow> HOL.equal Int.Min k2"
2295 "HOL.equal (Int.Bit0 k1) Int.Pls \<longleftrightarrow> HOL.equal k1 Int.Pls"
2296 "HOL.equal (Int.Bit1 k1) Int.Pls \<longleftrightarrow> False"
2297 "HOL.equal (Int.Bit0 k1) Int.Min \<longleftrightarrow> False"
2298 "HOL.equal (Int.Bit1 k1) Int.Min \<longleftrightarrow> HOL.equal k1 Int.Min"
2299 "HOL.equal (Int.Bit0 k1) (Int.Bit0 k2) \<longleftrightarrow> HOL.equal k1 k2"
2300 "HOL.equal (Int.Bit0 k1) (Int.Bit1 k2) \<longleftrightarrow> False"
2301 "HOL.equal (Int.Bit1 k1) (Int.Bit0 k2) \<longleftrightarrow> False"
2302 "HOL.equal (Int.Bit1 k1) (Int.Bit1 k2) \<longleftrightarrow> HOL.equal k1 k2"
2303 unfolding equal_eq by simp_all
2305 lemma eq_int_refl [code nbe]:
2306 "HOL.equal (k::int) k \<longleftrightarrow> True"
2307 by (rule equal_refl)
2309 lemma less_eq_number_of_int_code [code]:
2310 "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
2311 unfolding number_of_is_id ..
2313 lemma less_eq_int_code [code]:
2314 "Int.Pls \<le> Int.Pls \<longleftrightarrow> True"
2315 "Int.Pls \<le> Int.Min \<longleftrightarrow> False"
2316 "Int.Pls \<le> Int.Bit0 k \<longleftrightarrow> Int.Pls \<le> k"
2317 "Int.Pls \<le> Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
2318 "Int.Min \<le> Int.Pls \<longleftrightarrow> True"
2319 "Int.Min \<le> Int.Min \<longleftrightarrow> True"
2320 "Int.Min \<le> Int.Bit0 k \<longleftrightarrow> Int.Min < k"
2321 "Int.Min \<le> Int.Bit1 k \<longleftrightarrow> Int.Min \<le> k"
2322 "Int.Bit0 k \<le> Int.Pls \<longleftrightarrow> k \<le> Int.Pls"
2323 "Int.Bit1 k \<le> Int.Pls \<longleftrightarrow> k < Int.Pls"
2324 "Int.Bit0 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
2325 "Int.Bit1 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
2326 "Int.Bit0 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 \<le> k2"
2327 "Int.Bit0 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
2328 "Int.Bit1 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
2329 "Int.Bit1 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
2332 lemma less_number_of_int_code [code]:
2333 "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
2334 unfolding number_of_is_id ..
2336 lemma less_int_code [code]:
2337 "Int.Pls < Int.Pls \<longleftrightarrow> False"
2338 "Int.Pls < Int.Min \<longleftrightarrow> False"
2339 "Int.Pls < Int.Bit0 k \<longleftrightarrow> Int.Pls < k"
2340 "Int.Pls < Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
2341 "Int.Min < Int.Pls \<longleftrightarrow> True"
2342 "Int.Min < Int.Min \<longleftrightarrow> False"
2343 "Int.Min < Int.Bit0 k \<longleftrightarrow> Int.Min < k"
2344 "Int.Min < Int.Bit1 k \<longleftrightarrow> Int.Min < k"
2345 "Int.Bit0 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
2346 "Int.Bit1 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
2347 "Int.Bit0 k < Int.Min \<longleftrightarrow> k \<le> Int.Min"
2348 "Int.Bit1 k < Int.Min \<longleftrightarrow> k < Int.Min"
2349 "Int.Bit0 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
2350 "Int.Bit0 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
2351 "Int.Bit1 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
2352 "Int.Bit1 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 < k2"
2356 nat_aux :: "int \<Rightarrow> nat \<Rightarrow> nat" where
2357 "nat_aux i n = nat i + n"
2360 "nat_aux i n = (if i \<le> 0 then n else nat_aux (i - 1) (Suc n))" -- {* tail recursive *}
2361 by (auto simp add: nat_aux_def nat_eq_iff linorder_not_le order_less_imp_le
2362 dest: zless_imp_add1_zle)
2364 lemma [code]: "nat i = nat_aux i 0"
2365 by (simp add: nat_aux_def)
2367 hide_const (open) nat_aux
2369 lemma zero_is_num_zero [code, code_unfold_post]:
2370 "(0\<Colon>int) = Numeral0"
2373 lemma one_is_num_one [code, code_unfold_post]:
2374 "(1\<Colon>int) = Numeral1"
2380 code_modulename OCaml
2383 code_modulename Haskell
2389 val term_of_int = HOLogic.mk_number HOLogic.intT;
2393 let val j = one_of [~1, 1] * random_range 0 i
2394 in (j, fn () => term_of_int j) end;
2400 fun strip_number_of (@{term "Int.number_of :: int => int"} $ t) = t
2401 | strip_number_of t = t;
2403 fun numeral_codegen thy mode defs dep module b t gr =
2404 let val i = HOLogic.dest_numeral (strip_number_of t)
2406 SOME (Codegen.str (string_of_int i),
2407 snd (Codegen.invoke_tycodegen thy mode defs dep module false HOLogic.intT gr))
2408 end handle TERM _ => NONE;
2412 Codegen.add_codegen "numeral_codegen" numeral_codegen
2418 "number_of :: int \<Rightarrow> int" ("(_)")
2421 "uminus :: int => int" ("~")
2422 "op + :: int => int => int" ("(_ +/ _)")
2423 "op * :: int => int => int" ("(_ */ _)")
2424 "op \<le> :: int => int => bool" ("(_ <=/ _)")
2425 "op < :: int => int => bool" ("(_ </ _)")
2427 quickcheck_params [default_type = int]
2429 hide_const (open) Pls Min Bit0 Bit1 succ pred
2432 subsection {* Legacy theorems *}
2434 lemmas zminus_zminus = minus_minus [of "z::int", standard]
2435 lemmas zminus_0 = minus_zero [where 'a=int]
2436 lemmas zminus_zadd_distrib = minus_add_distrib [of "z::int" "w", standard]
2437 lemmas zadd_commute = add_commute [of "z::int" "w", standard]
2438 lemmas zadd_assoc = add_assoc [of "z1::int" "z2" "z3", standard]
2439 lemmas zadd_left_commute = add_left_commute [of "x::int" "y" "z", standard]
2440 lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute
2441 lemmas zmult_ac = mult_ac
2442 lemmas zadd_0 = add_0_left [of "z::int", standard]
2443 lemmas zadd_0_right = add_0_right [of "z::int", standard]
2444 lemmas zadd_zminus_inverse2 = left_minus [of "z::int", standard]
2445 lemmas zmult_zminus = mult_minus_left [of "z::int" "w", standard]
2446 lemmas zmult_commute = mult_commute [of "z::int" "w", standard]
2447 lemmas zmult_assoc = mult_assoc [of "z1::int" "z2" "z3", standard]
2448 lemmas zadd_zmult_distrib = left_distrib [of "z1::int" "z2" "w", standard]
2449 lemmas zadd_zmult_distrib2 = right_distrib [of "w::int" "z1" "z2", standard]
2450 lemmas zdiff_zmult_distrib = left_diff_distrib [of "z1::int" "z2" "w", standard]
2451 lemmas zdiff_zmult_distrib2 = right_diff_distrib [of "w::int" "z1" "z2", standard]
2453 lemmas zmult_1 = mult_1_left [of "z::int", standard]
2454 lemmas zmult_1_right = mult_1_right [of "z::int", standard]
2456 lemmas zle_refl = order_refl [of "w::int", standard]
2457 lemmas zle_trans = order_trans [where 'a=int and x="i" and y="j" and z="k", standard]
2458 lemmas zle_antisym = order_antisym [of "z::int" "w", standard]
2459 lemmas zle_linear = linorder_linear [of "z::int" "w", standard]
2460 lemmas zless_linear = linorder_less_linear [where 'a = int]
2462 lemmas zadd_left_mono = add_left_mono [of "i::int" "j" "k", standard]
2463 lemmas zadd_strict_right_mono = add_strict_right_mono [of "i::int" "j" "k", standard]
2464 lemmas zadd_zless_mono = add_less_le_mono [of "w'::int" "w" "z'" "z", standard]
2466 lemmas int_0_less_1 = zero_less_one [where 'a=int]
2467 lemmas int_0_neq_1 = zero_neq_one [where 'a=int]
2469 lemmas inj_int = inj_of_nat [where 'a=int]
2470 lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
2471 lemmas int_mult = of_nat_mult [where 'a=int]
2472 lemmas zmult_int = of_nat_mult [where 'a=int, symmetric]
2473 lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="n", standard]
2474 lemmas zless_int = of_nat_less_iff [where 'a=int]
2475 lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="k", standard]
2476 lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int]
2477 lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
2478 lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="n", standard]
2479 lemmas int_0 = of_nat_0 [where 'a=int]
2480 lemmas int_1 = of_nat_1 [where 'a=int]
2481 lemmas int_Suc = of_nat_Suc [where 'a=int]
2482 lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m", standard]
2483 lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
2484 lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
2485 lemmas zless_le = less_int_def
2486 lemmas int_eq_of_nat = TrueI
2488 lemma zpower_zadd_distrib:
2489 "x ^ (y + z) = ((x ^ y) * (x ^ z)::int)"
2492 lemma zero_less_zpower_abs_iff:
2493 "(0 < abs x ^ n) \<longleftrightarrow> (x \<noteq> (0::int) | n = 0)"
2494 by (rule zero_less_power_abs_iff)
2496 lemma zero_le_zpower_abs: "(0::int) \<le> abs x ^ n"
2497 by (rule zero_le_power_abs)
2499 lemma zpower_zpower:
2500 "(x ^ y) ^ z = (x ^ (y * z)::int)"
2501 by (rule power_mult [symmetric])
2504 "int (m ^ n) = int m ^ n"
2505 by (rule of_nat_power)
2507 lemmas zpower_int = int_power [symmetric]