2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
3 Tobias Nipkow, Florian Haftmann, TU Muenchen
4 Copyright 1994 University of Cambridge
8 header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *}
11 imports Equiv_Relations Nat Wellfounded
14 ("Tools/numeral_syntax.ML")
15 ("Tools/int_arith.ML")
18 subsection {* The equivalence relation underlying the integers *}
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 }"
25 by (auto simp add: quotient_def)
27 instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
31 Zero_int_def [code del]: "0 = Abs_Integ (intrel `` {(0, 0)})"
34 One_int_def [code del]: "1 = Abs_Integ (intrel `` {(1, 0)})"
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)})"
42 minus_int_def [code del]:
43 "- z = Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})"
46 diff_int_def [code del]: "z - w = z + (-w \<Colon> int)"
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)})"
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)"
58 less_int_def [code del]: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
61 zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
64 zsgn_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
71 subsection{*Construction of the Integers*}
73 lemma intrel_iff [simp]: "(((x,y),(u,v)) \<in> intrel) = (x+v = u+y)"
74 by (simp add: intrel_def)
76 lemma equiv_intrel: "equiv UNIV intrel"
77 by (simp add: intrel_def equiv_def refl_on_def sym_def trans_def)
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]
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)
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,no_atp] Abs_Integ_inverse [simp,no_atp]
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)
100 subsection {* Arithmetic Operations *}
102 lemma minus: "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})"
104 have "(\<lambda>(x,y). intrel``{(y,x)}) respects intrel"
105 by (simp add: congruent_def)
107 by (simp add: minus_int_def UN_equiv_class [OF equiv_intrel])
111 "Abs_Integ (intrel``{(x,y)}) + Abs_Integ (intrel``{(u,v)}) =
112 Abs_Integ (intrel``{(x+u, y+v)})"
114 have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). intrel `` {(x+u, y+v)}) w) z)
116 by (simp add: congruent2_def)
118 by (simp add: add_int_def UN_UN_split_split_eq
119 UN_equiv_class2 [OF equiv_intrel equiv_intrel])
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)
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])
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])
141 text{*The integers form a @{text comm_ring_1}*}
142 instance int :: comm_ring_1
145 show "(i + j) + k = i + (j + k)"
146 by (cases i, cases j, cases k) (simp add: add add_assoc)
148 by (cases i, cases j) (simp add: add_ac add)
150 by (cases i) (simp add: Zero_int_def add)
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)
158 by (cases i, cases j) (simp add: mult algebra_simps)
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)
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)
171 subsection {* The @{text "\<le>"} Ordering *}
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)
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)
181 instance int :: linorder
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)
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)
196 instantiation int :: distrib_lattice
200 "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
203 "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
207 (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
211 instance int :: ordered_cancel_ab_semigroup_add
214 show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
215 by (cases i, cases j, cases k) (simp add: le add)
219 text{*Strict Monotonicity of Multiplication*}
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)
230 lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = of_nat n"
232 apply (auto simp add: le add int_def Zero_int_def)
233 apply (rule_tac x="x-y" in exI, simp)
236 lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = of_nat n"
238 apply (simp add: less int_def Zero_int_def)
239 apply (rule_tac x="x-y" in exI, simp)
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)
247 text{*The integers form an ordered integral domain*}
248 instance int :: linordered_idom
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)
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)
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)
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]
280 subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}
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 })"
288 lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
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]
294 by (simp add: of_int_def UN_equiv_class [OF equiv_intrel])
297 lemma of_int_0 [simp]: "of_int 0 = 0"
298 by (simp add: of_int Zero_int_def)
300 lemma of_int_1 [simp]: "of_int 1 = 1"
301 by (simp add: of_int One_int_def)
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)
306 lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)"
307 by (cases z, simp add: algebra_simps of_int minus)
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)
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)
317 text{*Collapse nested embeddings*}
318 lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n"
322 "of_int (z ^ n) = of_int z ^ n"
323 by (induct n) simp_all
327 text{*Class for unital rings with characteristic zero.
328 Includes non-ordered rings like the complex numbers.*}
329 class ring_char_0 = ring_1 + semiring_char_0
332 lemma of_int_eq_iff [simp]:
333 "of_int w = of_int z \<longleftrightarrow> w = z"
334 apply (cases w, cases z, simp add: of_int)
335 apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq)
336 apply (simp only: of_nat_add [symmetric] of_nat_eq_iff)
339 text{*Special cases where either operand is zero*}
340 lemma of_int_eq_0_iff [simp]:
341 "of_int z = 0 \<longleftrightarrow> z = 0"
342 using of_int_eq_iff [of z 0] by simp
344 lemma of_int_0_eq_iff [simp]:
345 "0 = of_int z \<longleftrightarrow> z = 0"
346 using of_int_eq_iff [of 0 z] by simp
350 context linordered_idom
353 text{*Every @{text linordered_idom} has characteristic zero.*}
354 subclass ring_char_0 ..
356 lemma of_int_le_iff [simp]:
357 "of_int w \<le> of_int z \<longleftrightarrow> w \<le> z"
358 by (cases w, cases z, simp add: of_int le minus algebra_simps of_nat_add [symmetric] del: of_nat_add)
360 lemma of_int_less_iff [simp]:
361 "of_int w < of_int z \<longleftrightarrow> w < z"
362 by (simp add: less_le order_less_le)
364 lemma of_int_0_le_iff [simp]:
365 "0 \<le> of_int z \<longleftrightarrow> 0 \<le> z"
366 using of_int_le_iff [of 0 z] by simp
368 lemma of_int_le_0_iff [simp]:
369 "of_int z \<le> 0 \<longleftrightarrow> z \<le> 0"
370 using of_int_le_iff [of z 0] by simp
372 lemma of_int_0_less_iff [simp]:
373 "0 < of_int z \<longleftrightarrow> 0 < z"
374 using of_int_less_iff [of 0 z] by simp
376 lemma of_int_less_0_iff [simp]:
377 "of_int z < 0 \<longleftrightarrow> z < 0"
378 using of_int_less_iff [of z 0] by simp
382 lemma of_int_eq_id [simp]: "of_int = id"
384 fix z show "of_int z = id z"
385 by (cases z) (simp add: of_int add minus int_def diff_minus)
389 subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *}
392 nat :: "int \<Rightarrow> nat"
394 [code del]: "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
396 lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
398 have "(\<lambda>(x,y). {x-y}) respects intrel"
399 by (simp add: congruent_def) arith
401 by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
404 lemma nat_int [simp]: "nat (of_nat n) = n"
405 by (simp add: nat int_def)
407 (* FIXME: duplicates nat_0 *)
408 lemma nat_zero [simp]: "nat 0 = 0"
409 by (simp add: Zero_int_def nat)
411 lemma int_nat_eq [simp]: "of_nat (nat z) = (if 0 \<le> z then z else 0)"
412 by (cases z, simp add: nat le int_def Zero_int_def)
414 corollary nat_0_le: "0 \<le> z ==> of_nat (nat z) = z"
417 lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
418 by (cases z, simp add: nat le Zero_int_def)
420 lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"
421 apply (cases w, cases z)
422 apply (simp add: nat le linorder_not_le [symmetric] Zero_int_def, arith)
425 text{*An alternative condition is @{term "0 \<le> w"} *}
426 corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
427 by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
429 corollary nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"
430 by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
432 lemma zless_nat_conj [simp]: "(nat w < nat z) = (0 < z & w < z)"
433 apply (cases w, cases z)
434 apply (simp add: nat le Zero_int_def linorder_not_le [symmetric], arith)
439 assumes "0 \<le> z" and "\<And>m. z = of_nat m \<Longrightarrow> P"
441 using assms by (blast dest: nat_0_le sym)
443 lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = of_nat m else m=0)"
444 by (cases w, simp add: nat le int_def Zero_int_def, arith)
446 corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = of_nat m else m=0)"
447 by (simp only: eq_commute [of m] nat_eq_iff)
449 lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)"
451 apply (simp add: nat le int_def Zero_int_def linorder_not_le[symmetric], arith)
454 lemma nat_0_iff[simp]: "nat(i::int) = 0 \<longleftrightarrow> i\<le>0"
455 by(simp add: nat_eq_iff) arith
457 lemma int_eq_iff: "(of_nat m = z) = (m = nat z & 0 \<le> z)"
458 by (auto simp add: nat_eq_iff2)
460 lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)"
461 by (insert zless_nat_conj [of 0], auto)
463 lemma nat_add_distrib:
464 "[| (0::int) \<le> z; 0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"
465 by (cases z, cases z', simp add: nat add le Zero_int_def)
467 lemma nat_diff_distrib:
468 "[| (0::int) \<le> z'; z' \<le> z |] ==> nat (z-z') = nat z - nat z'"
469 by (cases z, cases z',
470 simp add: nat add minus diff_minus le Zero_int_def)
472 lemma nat_zminus_int [simp]: "nat (- (of_nat n)) = 0"
473 by (simp add: int_def minus nat Zero_int_def)
475 lemma zless_nat_eq_int_zless: "(m < nat z) = (of_nat m < z)"
476 by (cases z, simp add: nat less int_def, arith)
481 lemma of_nat_nat: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z"
482 by (cases z rule: eq_Abs_Integ)
483 (simp add: nat le of_int Zero_int_def of_nat_diff)
487 text {* For termination proofs: *}
488 lemma measure_function_int[measure_function]: "is_measure (nat o abs)" ..
491 subsection{*Lemmas about the Function @{term of_nat} and Orderings*}
493 lemma negative_zless_0: "- (of_nat (Suc n)) < (0 \<Colon> int)"
494 by (simp add: order_less_le del: of_nat_Suc)
496 lemma negative_zless [iff]: "- (of_nat (Suc n)) < (of_nat m \<Colon> int)"
497 by (rule negative_zless_0 [THEN order_less_le_trans], simp)
499 lemma negative_zle_0: "- of_nat n \<le> (0 \<Colon> int)"
500 by (simp add: minus_le_iff)
502 lemma negative_zle [iff]: "- of_nat n \<le> (of_nat m \<Colon> int)"
503 by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff])
505 lemma not_zle_0_negative [simp]: "~ (0 \<le> - (of_nat (Suc n) \<Colon> int))"
506 by (subst le_minus_iff, simp del: of_nat_Suc)
508 lemma int_zle_neg: "((of_nat n \<Colon> int) \<le> - of_nat m) = (n = 0 & m = 0)"
509 by (simp add: int_def le minus Zero_int_def)
511 lemma not_int_zless_negative [simp]: "~ ((of_nat n \<Colon> int) < - of_nat m)"
512 by (simp add: linorder_not_less)
514 lemma negative_eq_positive [simp]: "((- of_nat n \<Colon> int) = of_nat m) = (n = 0 & m = 0)"
515 by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg)
517 lemma zle_iff_zadd: "(w\<Colon>int) \<le> z \<longleftrightarrow> (\<exists>n. z = w + of_nat n)"
519 have "(w \<le> z) = (0 \<le> z - w)"
520 by (simp only: le_diff_eq add_0_left)
521 also have "\<dots> = (\<exists>n. z - w = of_nat n)"
522 by (auto elim: zero_le_imp_eq_int)
523 also have "\<dots> = (\<exists>n. z = w + of_nat n)"
524 by (simp only: algebra_simps)
525 finally show ?thesis .
528 lemma zadd_int_left: "of_nat m + (of_nat n + z) = of_nat (m + n) + (z\<Colon>int)"
531 lemma int_Suc0_eq_1: "of_nat (Suc 0) = (1\<Colon>int)"
534 text{*This version is proved for all ordered rings, not just integers!
535 It is proved here because attribute @{text arith_split} is not available
536 in theory @{text Rings}.
537 But is it really better than just rewriting with @{text abs_if}?*}
538 lemma abs_split [arith_split,no_atp]:
539 "P(abs(a::'a::linordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
540 by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
542 lemma negD: "(x \<Colon> int) < 0 \<Longrightarrow> \<exists>n. x = - (of_nat (Suc n))"
544 apply (auto simp add: le minus Zero_int_def int_def order_less_le)
545 apply (rule_tac x="y - Suc x" in exI, arith)
549 subsection {* Cases and induction *}
551 text{*Now we replace the case analysis rule by a more conventional one:
552 whether an integer is negative or not.*}
554 theorem int_cases [cases type: int, case_names nonneg neg]:
555 "[|!! n. (z \<Colon> int) = of_nat n ==> P; !! n. z = - (of_nat (Suc n)) ==> P |] ==> P"
556 apply (cases "z < 0", blast dest!: negD)
557 apply (simp add: linorder_not_less del: of_nat_Suc)
559 apply (blast dest: nat_0_le [THEN sym])
562 theorem int_induct [induct type: int, case_names nonneg neg]:
563 "[|!! n. P (of_nat n \<Colon> int); !!n. P (- (of_nat (Suc n))) |] ==> P z"
564 by (cases z rule: int_cases) auto
566 text{*Contributed by Brian Huffman*}
567 theorem int_diff_cases:
568 obtains (diff) m n where "(z\<Colon>int) = of_nat m - of_nat n"
569 apply (cases z rule: eq_Abs_Integ)
570 apply (rule_tac m=x and n=y in diff)
571 apply (simp add: int_def diff_def minus add)
575 subsection {* Binary representation *}
578 This formalization defines binary arithmetic in terms of the integers
579 rather than using a datatype. This avoids multiple representations (leading
580 zeroes, etc.) See @{text "ZF/Tools/twos-compl.ML"}, function @{text
581 int_of_binary}, for the numerical interpretation.
583 The representation expects that @{text "(m mod 2)"} is 0 or 1,
584 even if m is negative;
585 For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
586 @{text "-5 = (-3)*2 + 1"}.
588 This two's complement binary representation derives from the paper
589 "An Efficient Representation of Arithmetic for Term Rewriting" by
590 Dave Cohen and Phil Watson, Rewriting Techniques and Applications,
591 Springer LNCS 488 (240-251), 1991.
594 subsubsection {* The constructors @{term Bit0}, @{term Bit1}, @{term Pls} and @{term Min} *}
598 [code del]: "Pls = 0"
602 [code del]: "Min = - 1"
605 Bit0 :: "int \<Rightarrow> int" where
606 [code del]: "Bit0 k = k + k"
609 Bit1 :: "int \<Rightarrow> int" where
610 [code del]: "Bit1 k = 1 + k + k"
612 class number = -- {* for numeric types: nat, int, real, \dots *}
613 fixes number_of :: "int \<Rightarrow> 'a"
615 use "Tools/numeral.ML"
618 "_Numeral" :: "num_const \<Rightarrow> 'a" ("_")
620 use "Tools/numeral_syntax.ML"
621 setup Numeral_Syntax.setup
624 "Numeral0 \<equiv> number_of Pls"
627 "Numeral1 \<equiv> number_of (Bit1 Pls)"
629 lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"
630 -- {* Unfold all @{text let}s involving constants *}
634 succ :: "int \<Rightarrow> int" where
635 [code del]: "succ k = k + 1"
638 pred :: "int \<Rightarrow> int" where
639 [code del]: "pred k = k - 1"
642 max_number_of [simp] = max_def
643 [of "number_of u" "number_of v", standard]
645 min_number_of [simp] = min_def
646 [of "number_of u" "number_of v", standard]
647 -- {* unfolding @{text minx} and @{text max} on numerals *}
649 lemmas numeral_simps =
650 succ_def pred_def Pls_def Min_def Bit0_def Bit1_def
652 text {* Removal of leading zeroes *}
654 lemma Bit0_Pls [simp, code_post]:
656 unfolding numeral_simps by simp
658 lemma Bit1_Min [simp, code_post]:
660 unfolding numeral_simps by simp
662 lemmas normalize_bin_simps =
666 subsubsection {* Successor and predecessor functions *}
671 "succ Pls = Bit1 Pls"
672 unfolding numeral_simps by simp
676 unfolding numeral_simps by simp
679 "succ (Bit0 k) = Bit1 k"
680 unfolding numeral_simps by simp
683 "succ (Bit1 k) = Bit0 (succ k)"
684 unfolding numeral_simps by simp
686 lemmas succ_bin_simps [simp] =
687 succ_Pls succ_Min succ_Bit0 succ_Bit1
689 text {* Predecessor *}
693 unfolding numeral_simps by simp
696 "pred Min = Bit0 Min"
697 unfolding numeral_simps by simp
700 "pred (Bit0 k) = Bit1 (pred k)"
701 unfolding numeral_simps by simp
704 "pred (Bit1 k) = Bit0 k"
705 unfolding numeral_simps by simp
707 lemmas pred_bin_simps [simp] =
708 pred_Pls pred_Min pred_Bit0 pred_Bit1
711 subsubsection {* Binary arithmetic *}
717 unfolding numeral_simps by simp
721 unfolding numeral_simps by simp
724 "(Bit0 k) + (Bit0 l) = Bit0 (k + l)"
725 unfolding numeral_simps by simp
728 "(Bit0 k) + (Bit1 l) = Bit1 (k + l)"
729 unfolding numeral_simps by simp
732 "(Bit1 k) + (Bit0 l) = Bit1 (k + l)"
733 unfolding numeral_simps by simp
736 "(Bit1 k) + (Bit1 l) = Bit0 (k + succ l)"
737 unfolding numeral_simps by simp
741 unfolding numeral_simps by simp
745 unfolding numeral_simps by simp
747 lemmas add_bin_simps [simp] =
748 add_Pls add_Min add_Pls_right add_Min_right
749 add_Bit0_Bit0 add_Bit0_Bit1 add_Bit1_Bit0 add_Bit1_Bit1
755 unfolding numeral_simps by simp
759 unfolding numeral_simps by simp
762 "- (Bit0 k) = Bit0 (- k)"
763 unfolding numeral_simps by simp
766 "- (Bit1 k) = Bit1 (pred (- k))"
767 unfolding numeral_simps by simp
769 lemmas minus_bin_simps [simp] =
770 minus_Pls minus_Min minus_Bit0 minus_Bit1
772 text {* Subtraction *}
774 lemma diff_bin_simps [simp]:
777 "Pls - (Bit0 l) = Bit0 (Pls - l)"
778 "Pls - (Bit1 l) = Bit1 (Min - l)"
779 "Min - (Bit0 l) = Bit1 (Min - l)"
780 "Min - (Bit1 l) = Bit0 (Min - l)"
781 "(Bit0 k) - (Bit0 l) = Bit0 (k - l)"
782 "(Bit0 k) - (Bit1 l) = Bit1 (pred k - l)"
783 "(Bit1 k) - (Bit0 l) = Bit1 (k - l)"
784 "(Bit1 k) - (Bit1 l) = Bit0 (k - l)"
785 unfolding numeral_simps by simp_all
787 text {* Multiplication *}
791 unfolding numeral_simps by simp
795 unfolding numeral_simps by simp
798 "(Bit0 k) * l = Bit0 (k * l)"
799 unfolding numeral_simps int_distrib by simp
802 "(Bit1 k) * l = (Bit0 (k * l)) + l"
803 unfolding numeral_simps int_distrib by simp
805 lemmas mult_bin_simps [simp] =
806 mult_Pls mult_Min mult_Bit0 mult_Bit1
809 subsubsection {* Binary comparisons *}
811 text {* Preliminaries *}
813 lemma even_less_0_iff:
814 "a + a < 0 \<longleftrightarrow> a < (0::'a::linordered_idom)"
816 have "a + a < 0 \<longleftrightarrow> (1+1)*a < 0" by (simp add: left_distrib)
817 also have "(1+1)*a < 0 \<longleftrightarrow> a < 0"
818 by (simp add: mult_less_0_iff zero_less_two
819 order_less_not_sym [OF zero_less_two])
820 finally show ?thesis .
824 assumes le: "0 \<le> z"
825 shows "(0::int) < 1 + z"
827 have "0 \<le> z" by fact
828 also have "... < z + 1" by (rule less_add_one)
829 also have "... = 1 + z" by (simp add: add_ac)
830 finally show "0 < 1 + z" .
833 lemma odd_less_0_iff:
834 "(1 + z + z < 0) = (z < (0::int))"
835 proof (cases z rule: int_cases)
837 thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
838 le_imp_0_less [THEN order_less_imp_le])
841 thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1
842 add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric])
845 lemma bin_less_0_simps:
846 "Pls < 0 \<longleftrightarrow> False"
847 "Min < 0 \<longleftrightarrow> True"
848 "Bit0 w < 0 \<longleftrightarrow> w < 0"
849 "Bit1 w < 0 \<longleftrightarrow> w < 0"
850 unfolding numeral_simps
851 by (simp_all add: even_less_0_iff odd_less_0_iff)
853 lemma less_bin_lemma: "k < l \<longleftrightarrow> k - l < (0::int)"
856 lemma le_iff_pred_less: "k \<le> l \<longleftrightarrow> pred k < l"
857 unfolding numeral_simps
859 have "k - 1 < k" by simp
860 also assume "k \<le> l"
861 finally show "k - 1 < l" .
864 hence "(k - 1) + 1 \<le> l" by (rule zless_imp_add1_zle)
865 thus "k \<le> l" by simp
868 lemma succ_pred: "succ (pred x) = x"
869 unfolding numeral_simps by simp
873 lemma less_bin_simps [simp]:
874 "Pls < Pls \<longleftrightarrow> False"
875 "Pls < Min \<longleftrightarrow> False"
876 "Pls < Bit0 k \<longleftrightarrow> Pls < k"
877 "Pls < Bit1 k \<longleftrightarrow> Pls \<le> k"
878 "Min < Pls \<longleftrightarrow> True"
879 "Min < Min \<longleftrightarrow> False"
880 "Min < Bit0 k \<longleftrightarrow> Min < k"
881 "Min < Bit1 k \<longleftrightarrow> Min < k"
882 "Bit0 k < Pls \<longleftrightarrow> k < Pls"
883 "Bit0 k < Min \<longleftrightarrow> k \<le> Min"
884 "Bit1 k < Pls \<longleftrightarrow> k < Pls"
885 "Bit1 k < Min \<longleftrightarrow> k < Min"
886 "Bit0 k < Bit0 l \<longleftrightarrow> k < l"
887 "Bit0 k < Bit1 l \<longleftrightarrow> k \<le> l"
888 "Bit1 k < Bit0 l \<longleftrightarrow> k < l"
889 "Bit1 k < Bit1 l \<longleftrightarrow> k < l"
890 unfolding le_iff_pred_less
891 less_bin_lemma [of Pls]
892 less_bin_lemma [of Min]
893 less_bin_lemma [of "k"]
894 less_bin_lemma [of "Bit0 k"]
895 less_bin_lemma [of "Bit1 k"]
896 less_bin_lemma [of "pred Pls"]
897 less_bin_lemma [of "pred k"]
898 by (simp_all add: bin_less_0_simps succ_pred)
900 text {* Less-than-or-equal *}
902 lemma le_bin_simps [simp]:
903 "Pls \<le> Pls \<longleftrightarrow> True"
904 "Pls \<le> Min \<longleftrightarrow> False"
905 "Pls \<le> Bit0 k \<longleftrightarrow> Pls \<le> k"
906 "Pls \<le> Bit1 k \<longleftrightarrow> Pls \<le> k"
907 "Min \<le> Pls \<longleftrightarrow> True"
908 "Min \<le> Min \<longleftrightarrow> True"
909 "Min \<le> Bit0 k \<longleftrightarrow> Min < k"
910 "Min \<le> Bit1 k \<longleftrightarrow> Min \<le> k"
911 "Bit0 k \<le> Pls \<longleftrightarrow> k \<le> Pls"
912 "Bit0 k \<le> Min \<longleftrightarrow> k \<le> Min"
913 "Bit1 k \<le> Pls \<longleftrightarrow> k < Pls"
914 "Bit1 k \<le> Min \<longleftrightarrow> k \<le> Min"
915 "Bit0 k \<le> Bit0 l \<longleftrightarrow> k \<le> l"
916 "Bit0 k \<le> Bit1 l \<longleftrightarrow> k \<le> l"
917 "Bit1 k \<le> Bit0 l \<longleftrightarrow> k < l"
918 "Bit1 k \<le> Bit1 l \<longleftrightarrow> k \<le> l"
919 unfolding not_less [symmetric]
920 by (simp_all add: not_le)
924 lemma eq_bin_simps [simp]:
925 "Pls = Pls \<longleftrightarrow> True"
926 "Pls = Min \<longleftrightarrow> False"
927 "Pls = Bit0 l \<longleftrightarrow> Pls = l"
928 "Pls = Bit1 l \<longleftrightarrow> False"
929 "Min = Pls \<longleftrightarrow> False"
930 "Min = Min \<longleftrightarrow> True"
931 "Min = Bit0 l \<longleftrightarrow> False"
932 "Min = Bit1 l \<longleftrightarrow> Min = l"
933 "Bit0 k = Pls \<longleftrightarrow> k = Pls"
934 "Bit0 k = Min \<longleftrightarrow> False"
935 "Bit1 k = Pls \<longleftrightarrow> False"
936 "Bit1 k = Min \<longleftrightarrow> k = Min"
937 "Bit0 k = Bit0 l \<longleftrightarrow> k = l"
938 "Bit0 k = Bit1 l \<longleftrightarrow> False"
939 "Bit1 k = Bit0 l \<longleftrightarrow> False"
940 "Bit1 k = Bit1 l \<longleftrightarrow> k = l"
941 unfolding order_eq_iff [where 'a=int]
942 by (simp_all add: not_less)
945 subsection {* Converting Numerals to Rings: @{term number_of} *}
947 class number_ring = number + comm_ring_1 +
948 assumes number_of_eq: "number_of k = of_int k"
950 text {* self-embedding of the integers *}
952 instantiation int :: number_ring
955 definition int_number_of_def [code del]:
956 "number_of w = (of_int w \<Colon> int)"
959 qed (simp only: int_number_of_def)
963 lemma number_of_is_id:
964 "number_of (k::int) = k"
965 unfolding int_number_of_def by simp
967 lemma number_of_succ:
968 "number_of (succ k) = (1 + number_of k ::'a::number_ring)"
969 unfolding number_of_eq numeral_simps by simp
971 lemma number_of_pred:
972 "number_of (pred w) = (- 1 + number_of w ::'a::number_ring)"
973 unfolding number_of_eq numeral_simps by simp
975 lemma number_of_minus:
976 "number_of (uminus w) = (- (number_of w)::'a::number_ring)"
977 unfolding number_of_eq by (rule of_int_minus)
980 "number_of (v + w) = (number_of v + number_of w::'a::number_ring)"
981 unfolding number_of_eq by (rule of_int_add)
983 lemma number_of_diff:
984 "number_of (v - w) = (number_of v - number_of w::'a::number_ring)"
985 unfolding number_of_eq by (rule of_int_diff)
987 lemma number_of_mult:
988 "number_of (v * w) = (number_of v * number_of w::'a::number_ring)"
989 unfolding number_of_eq by (rule of_int_mult)
992 The correctness of shifting.
993 But it doesn't seem to give a measurable speed-up.
996 lemma double_number_of_Bit0:
997 "(1 + 1) * number_of w = (number_of (Bit0 w) ::'a::number_ring)"
998 unfolding number_of_eq numeral_simps left_distrib by simp
1001 Converting numerals 0 and 1 to their abstract versions.
1004 lemma numeral_0_eq_0 [simp, code_post]:
1005 "Numeral0 = (0::'a::number_ring)"
1006 unfolding number_of_eq numeral_simps by simp
1008 lemma numeral_1_eq_1 [simp, code_post]:
1009 "Numeral1 = (1::'a::number_ring)"
1010 unfolding number_of_eq numeral_simps by simp
1013 Special-case simplification for small constants.
1017 Unary minus for the abstract constant 1. Cannot be inserted
1018 as a simprule until later: it is @{text number_of_Min} re-oriented!
1021 lemma numeral_m1_eq_minus_1:
1022 "(-1::'a::number_ring) = - 1"
1023 unfolding number_of_eq numeral_simps by simp
1025 lemma mult_minus1 [simp]:
1026 "-1 * z = -(z::'a::number_ring)"
1027 unfolding number_of_eq numeral_simps by simp
1029 lemma mult_minus1_right [simp]:
1030 "z * -1 = -(z::'a::number_ring)"
1031 unfolding number_of_eq numeral_simps by simp
1033 (*Negation of a coefficient*)
1034 lemma minus_number_of_mult [simp]:
1035 "- (number_of w) * z = number_of (uminus w) * (z::'a::number_ring)"
1036 unfolding number_of_eq by simp
1038 text {* Subtraction *}
1040 lemma diff_number_of_eq:
1041 "number_of v - number_of w =
1042 (number_of (v + uminus w)::'a::number_ring)"
1043 unfolding number_of_eq by simp
1045 lemma number_of_Pls:
1046 "number_of Pls = (0::'a::number_ring)"
1047 unfolding number_of_eq numeral_simps by simp
1049 lemma number_of_Min:
1050 "number_of Min = (- 1::'a::number_ring)"
1051 unfolding number_of_eq numeral_simps by simp
1053 lemma number_of_Bit0:
1054 "number_of (Bit0 w) = (0::'a::number_ring) + (number_of w) + (number_of w)"
1055 unfolding number_of_eq numeral_simps by simp
1057 lemma number_of_Bit1:
1058 "number_of (Bit1 w) = (1::'a::number_ring) + (number_of w) + (number_of w)"
1059 unfolding number_of_eq numeral_simps by simp
1062 subsubsection {* Equality of Binary Numbers *}
1064 text {* First version by Norbert Voelker *}
1066 definition (*for simplifying equalities*) iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool" where
1067 "iszero z \<longleftrightarrow> z = 0"
1069 lemma iszero_0: "iszero 0"
1070 by (simp add: iszero_def)
1072 lemma iszero_Numeral0: "iszero (Numeral0 :: 'a::number_ring)"
1073 by (simp add: iszero_0)
1075 lemma not_iszero_1: "\<not> iszero 1"
1076 by (simp add: iszero_def)
1078 lemma not_iszero_Numeral1: "\<not> iszero (Numeral1 :: 'a::number_ring)"
1079 by (simp add: not_iszero_1)
1081 lemma eq_number_of_eq [simp]:
1082 "((number_of x::'a::number_ring) = number_of y) =
1083 iszero (number_of (x + uminus y) :: 'a)"
1084 unfolding iszero_def number_of_add number_of_minus
1085 by (simp add: algebra_simps)
1087 lemma iszero_number_of_Pls:
1088 "iszero ((number_of Pls)::'a::number_ring)"
1089 unfolding iszero_def numeral_0_eq_0 ..
1091 lemma nonzero_number_of_Min:
1092 "~ iszero ((number_of Min)::'a::number_ring)"
1093 unfolding iszero_def numeral_m1_eq_minus_1 by simp
1096 subsubsection {* Comparisons, for Ordered Rings *}
1098 lemmas double_eq_0_iff = double_zero
1101 "1 + z + z \<noteq> (0::int)"
1102 proof (cases z rule: int_cases)
1104 have le: "0 \<le> z+z" by (simp add: nonneg add_increasing)
1105 thus ?thesis using le_imp_0_less [OF le]
1106 by (auto simp add: add_assoc)
1111 assume eq: "1 + z + z = 0"
1112 have "(0::int) < 1 + (of_nat n + of_nat n)"
1113 by (simp add: le_imp_0_less add_increasing)
1114 also have "... = - (1 + z + z)"
1115 by (simp add: neg add_assoc [symmetric])
1116 also have "... = 0" by (simp add: eq)
1117 finally have "0<0" ..
1122 lemma iszero_number_of_Bit0:
1123 "iszero (number_of (Bit0 w)::'a) =
1124 iszero (number_of w::'a::{ring_char_0,number_ring})"
1126 have "(of_int w + of_int w = (0::'a)) \<Longrightarrow> (w = 0)"
1128 assume eq: "of_int w + of_int w = (0::'a)"
1129 then have "of_int (w + w) = (of_int 0 :: 'a)" by simp
1130 then have "w + w = 0" by (simp only: of_int_eq_iff)
1131 then show "w = 0" by (simp only: double_eq_0_iff)
1134 by (auto simp add: iszero_def number_of_eq numeral_simps)
1137 lemma iszero_number_of_Bit1:
1138 "~ iszero (number_of (Bit1 w)::'a::{ring_char_0,number_ring})"
1140 have "1 + of_int w + of_int w \<noteq> (0::'a)"
1142 assume eq: "1 + of_int w + of_int w = (0::'a)"
1143 hence "of_int (1 + w + w) = (of_int 0 :: 'a)" by simp
1144 hence "1 + w + w = 0" by (simp only: of_int_eq_iff)
1145 with odd_nonzero show False by blast
1148 by (auto simp add: iszero_def number_of_eq numeral_simps)
1151 lemmas iszero_simps [simp] =
1152 iszero_0 not_iszero_1
1153 iszero_number_of_Pls nonzero_number_of_Min
1154 iszero_number_of_Bit0 iszero_number_of_Bit1
1155 (* iszero_number_of_Pls would never normally be used
1156 because its lhs simplifies to "iszero 0" *)
1158 subsubsection {* The Less-Than Relation *}
1160 lemma double_less_0_iff:
1161 "(a + a < 0) = (a < (0::'a::linordered_idom))"
1163 have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)
1164 also have "... = (a < 0)"
1165 by (simp add: mult_less_0_iff zero_less_two
1166 order_less_not_sym [OF zero_less_two])
1167 finally show ?thesis .
1171 "(1 + z + z < 0) = (z < (0::int))"
1172 proof (cases z rule: int_cases)
1174 thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
1175 le_imp_0_less [THEN order_less_imp_le])
1178 thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1
1179 add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric])
1182 text {* Less-Than or Equals *}
1184 text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *}
1186 lemmas le_number_of_eq_not_less =
1187 linorder_not_less [of "number_of w" "number_of v", symmetric,
1191 text {* Absolute value (@{term abs}) *}
1193 lemma abs_number_of:
1194 "abs(number_of x::'a::{linordered_idom,number_ring}) =
1195 (if number_of x < (0::'a) then -number_of x else number_of x)"
1196 by (simp add: abs_if)
1199 text {* Re-orientation of the equation nnn=x *}
1201 lemma number_of_reorient:
1202 "(number_of w = x) = (x = number_of w)"
1206 subsubsection {* Simplification of arithmetic operations on integer constants. *}
1208 lemmas arith_extra_simps [standard, simp] =
1209 number_of_add [symmetric]
1210 number_of_minus [symmetric]
1211 numeral_m1_eq_minus_1 [symmetric]
1212 number_of_mult [symmetric]
1213 diff_number_of_eq abs_number_of
1216 For making a minimal simpset, one must include these default simprules.
1217 Also include @{text simp_thms}.
1220 lemmas arith_simps =
1221 normalize_bin_simps pred_bin_simps succ_bin_simps
1222 add_bin_simps minus_bin_simps mult_bin_simps
1223 abs_zero abs_one arith_extra_simps
1225 text {* Simplification of relational operations *}
1227 lemma less_number_of [simp]:
1228 "(number_of x::'a::{linordered_idom,number_ring}) < number_of y \<longleftrightarrow> x < y"
1229 unfolding number_of_eq by (rule of_int_less_iff)
1231 lemma le_number_of [simp]:
1232 "(number_of x::'a::{linordered_idom,number_ring}) \<le> number_of y \<longleftrightarrow> x \<le> y"
1233 unfolding number_of_eq by (rule of_int_le_iff)
1235 lemma eq_number_of [simp]:
1236 "(number_of x::'a::{ring_char_0,number_ring}) = number_of y \<longleftrightarrow> x = y"
1237 unfolding number_of_eq by (rule of_int_eq_iff)
1240 less_number_of less_bin_simps
1241 le_number_of le_bin_simps
1242 eq_number_of_eq eq_bin_simps
1246 subsubsection {* Simplification of arithmetic when nested to the right. *}
1248 lemma add_number_of_left [simp]:
1249 "number_of v + (number_of w + z) =
1250 (number_of(v + w) + z::'a::number_ring)"
1251 by (simp add: add_assoc [symmetric])
1253 lemma mult_number_of_left [simp]:
1254 "number_of v * (number_of w * z) =
1255 (number_of(v * w) * z::'a::number_ring)"
1256 by (simp add: mult_assoc [symmetric])
1258 lemma add_number_of_diff1:
1259 "number_of v + (number_of w - c) =
1260 number_of(v + w) - (c::'a::number_ring)"
1261 by (simp add: diff_minus)
1263 lemma add_number_of_diff2 [simp]:
1264 "number_of v + (c - number_of w) =
1265 number_of (v + uminus w) + (c::'a::number_ring)"
1266 by (simp add: algebra_simps diff_number_of_eq [symmetric])
1271 subsection {* The Set of Integers *}
1276 definition Ints :: "'a set" where
1277 [code del]: "Ints = range of_int"
1282 lemma Ints_of_int [simp]: "of_int z \<in> \<int>"
1283 by (simp add: Ints_def)
1285 lemma Ints_of_nat [simp]: "of_nat n \<in> \<int>"
1286 apply (simp add: Ints_def)
1287 apply (rule range_eqI)
1288 apply (rule of_int_of_nat_eq [symmetric])
1291 lemma Ints_0 [simp]: "0 \<in> \<int>"
1292 apply (simp add: Ints_def)
1293 apply (rule range_eqI)
1294 apply (rule of_int_0 [symmetric])
1297 lemma Ints_1 [simp]: "1 \<in> \<int>"
1298 apply (simp add: Ints_def)
1299 apply (rule range_eqI)
1300 apply (rule of_int_1 [symmetric])
1303 lemma Ints_add [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a + b \<in> \<int>"
1304 apply (auto simp add: Ints_def)
1305 apply (rule range_eqI)
1306 apply (rule of_int_add [symmetric])
1309 lemma Ints_minus [simp]: "a \<in> \<int> \<Longrightarrow> -a \<in> \<int>"
1310 apply (auto simp add: Ints_def)
1311 apply (rule range_eqI)
1312 apply (rule of_int_minus [symmetric])
1315 lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a - b \<in> \<int>"
1316 apply (auto simp add: Ints_def)
1317 apply (rule range_eqI)
1318 apply (rule of_int_diff [symmetric])
1321 lemma Ints_mult [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a * b \<in> \<int>"
1322 apply (auto simp add: Ints_def)
1323 apply (rule range_eqI)
1324 apply (rule of_int_mult [symmetric])
1327 lemma Ints_power [simp]: "a \<in> \<int> \<Longrightarrow> a ^ n \<in> \<int>"
1328 by (induct n) simp_all
1330 lemma Ints_cases [cases set: Ints]:
1331 assumes "q \<in> \<int>"
1332 obtains (of_int) z where "q = of_int z"
1335 from `q \<in> \<int>` have "q \<in> range of_int" unfolding Ints_def .
1336 then obtain z where "q = of_int z" ..
1340 lemma Ints_induct [case_names of_int, induct set: Ints]:
1341 "q \<in> \<int> \<Longrightarrow> (\<And>z. P (of_int z)) \<Longrightarrow> P q"
1342 by (rule Ints_cases) auto
1346 text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
1348 lemma Ints_double_eq_0_iff:
1349 assumes in_Ints: "a \<in> Ints"
1350 shows "(a + a = 0) = (a = (0::'a::ring_char_0))"
1352 from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
1353 then obtain z where a: "a = of_int z" ..
1357 thus "a + a = 0" by simp
1359 assume eq: "a + a = 0"
1360 hence "of_int (z + z) = (of_int 0 :: 'a)" by (simp add: a)
1361 hence "z + z = 0" by (simp only: of_int_eq_iff)
1362 hence "z = 0" by (simp only: double_eq_0_iff)
1363 thus "a = 0" by (simp add: a)
1367 lemma Ints_odd_nonzero:
1368 assumes in_Ints: "a \<in> Ints"
1369 shows "1 + a + a \<noteq> (0::'a::ring_char_0)"
1371 from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
1372 then obtain z where a: "a = of_int z" ..
1375 assume eq: "1 + a + a = 0"
1376 hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
1377 hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
1378 with odd_nonzero show False by blast
1382 lemma Ints_number_of [simp]:
1383 "(number_of w :: 'a::number_ring) \<in> Ints"
1384 unfolding number_of_eq Ints_def by simp
1386 lemma Nats_number_of [simp]:
1387 "Int.Pls \<le> w \<Longrightarrow> (number_of w :: 'a::number_ring) \<in> Nats"
1388 unfolding Int.Pls_def number_of_eq
1389 by (simp only: of_nat_nat [symmetric] of_nat_in_Nats)
1391 lemma Ints_odd_less_0:
1392 assumes in_Ints: "a \<in> Ints"
1393 shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))"
1395 from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
1396 then obtain z where a: "a = of_int z" ..
1397 hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
1399 also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0)
1400 also have "... = (a < 0)" by (simp add: a)
1401 finally show ?thesis .
1405 subsection {* @{term setsum} and @{term setprod} *}
1407 lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
1408 apply (cases "finite A")
1409 apply (erule finite_induct, auto)
1412 lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
1413 apply (cases "finite A")
1414 apply (erule finite_induct, auto)
1417 lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
1418 apply (cases "finite A")
1419 apply (erule finite_induct, auto simp add: of_nat_mult)
1422 lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
1423 apply (cases "finite A")
1424 apply (erule finite_induct, auto)
1427 lemmas int_setsum = of_nat_setsum [where 'a=int]
1428 lemmas int_setprod = of_nat_setprod [where 'a=int]
1431 subsection{*Inequality Reasoning for the Arithmetic Simproc*}
1433 lemma add_numeral_0: "Numeral0 + a = (a::'a::number_ring)"
1436 lemma add_numeral_0_right: "a + Numeral0 = (a::'a::number_ring)"
1439 lemma mult_numeral_1: "Numeral1 * a = (a::'a::number_ring)"
1442 lemma mult_numeral_1_right: "a * Numeral1 = (a::'a::number_ring)"
1445 lemma divide_numeral_1: "a / Numeral1 = (a::'a::{number_ring,field})"
1448 lemma inverse_numeral_1:
1449 "inverse Numeral1 = (Numeral1::'a::{number_ring,field})"
1452 text{*Theorem lists for the cancellation simprocs. The use of binary numerals
1453 for 0 and 1 reduces the number of special cases.*}
1455 lemmas add_0s = add_numeral_0 add_numeral_0_right
1456 lemmas mult_1s = mult_numeral_1 mult_numeral_1_right
1457 mult_minus1 mult_minus1_right
1460 subsection{*Special Arithmetic Rules for Abstract 0 and 1*}
1462 text{*Arithmetic computations are defined for binary literals, which leaves 0
1463 and 1 as special cases. Addition already has rules for 0, but not 1.
1464 Multiplication and unary minus already have rules for both 0 and 1.*}
1467 lemma binop_eq: "[|f x y = g x y; x = x'; y = y'|] ==> f x' y' = g x' y'"
1471 lemmas add_number_of_eq = number_of_add [symmetric]
1473 text{*Allow 1 on either or both sides*}
1474 lemma one_add_one_is_two: "1 + 1 = (2::'a::number_ring)"
1475 by (simp del: numeral_1_eq_1 add: numeral_1_eq_1 [symmetric])
1477 lemmas add_special =
1479 binop_eq [of "op +", OF add_number_of_eq numeral_1_eq_1 refl, standard]
1480 binop_eq [of "op +", OF add_number_of_eq refl numeral_1_eq_1, standard]
1482 text{*Allow 1 on either or both sides (1-1 already simplifies to 0)*}
1483 lemmas diff_special =
1484 binop_eq [of "op -", OF diff_number_of_eq numeral_1_eq_1 refl, standard]
1485 binop_eq [of "op -", OF diff_number_of_eq refl numeral_1_eq_1, standard]
1487 text{*Allow 0 or 1 on either side with a binary numeral on the other*}
1489 binop_eq [of "op =", OF eq_number_of_eq numeral_0_eq_0 refl, standard]
1490 binop_eq [of "op =", OF eq_number_of_eq numeral_1_eq_1 refl, standard]
1491 binop_eq [of "op =", OF eq_number_of_eq refl numeral_0_eq_0, standard]
1492 binop_eq [of "op =", OF eq_number_of_eq refl numeral_1_eq_1, standard]
1494 text{*Allow 0 or 1 on either side with a binary numeral on the other*}
1495 lemmas less_special =
1496 binop_eq [of "op <", OF less_number_of numeral_0_eq_0 refl, standard]
1497 binop_eq [of "op <", OF less_number_of numeral_1_eq_1 refl, standard]
1498 binop_eq [of "op <", OF less_number_of refl numeral_0_eq_0, standard]
1499 binop_eq [of "op <", OF less_number_of refl numeral_1_eq_1, standard]
1501 text{*Allow 0 or 1 on either side with a binary numeral on the other*}
1503 binop_eq [of "op \<le>", OF le_number_of numeral_0_eq_0 refl, standard]
1504 binop_eq [of "op \<le>", OF le_number_of numeral_1_eq_1 refl, standard]
1505 binop_eq [of "op \<le>", OF le_number_of refl numeral_0_eq_0, standard]
1506 binop_eq [of "op \<le>", OF le_number_of refl numeral_1_eq_1, standard]
1508 lemmas arith_special[simp] =
1509 add_special diff_special eq_special less_special le_special
1512 text {* Legacy theorems *}
1514 lemmas zle_int = of_nat_le_iff [where 'a=int]
1515 lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
1517 subsection {* Setting up simplification procedures *}
1519 lemmas int_arith_rules =
1520 neg_le_iff_le numeral_0_eq_0 numeral_1_eq_1
1521 minus_zero diff_minus left_minus right_minus
1522 mult_zero_left mult_zero_right mult_Bit1 mult_1_left mult_1_right
1523 mult_minus_left mult_minus_right
1524 minus_add_distrib minus_minus mult_assoc
1525 of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
1526 of_int_0 of_int_1 of_int_add of_int_mult
1528 use "Tools/int_arith.ML"
1529 setup {* Int_Arith.global_setup *}
1530 declaration {* K Int_Arith.setup *}
1534 (fn Const (@{const_name number_of}, _) $ _ => true | _ => false)
1537 simproc_setup reorient_numeral ("number_of w = x") = Reorient_Proc.proc
1540 subsection{*Lemmas About Small Numerals*}
1542 lemma of_int_m1 [simp]: "of_int -1 = (-1 :: 'a :: number_ring)"
1544 have "(of_int -1 :: 'a) = of_int (- 1)" by simp
1545 also have "... = - of_int 1" by (simp only: of_int_minus)
1546 also have "... = -1" by simp
1547 finally show ?thesis .
1550 lemma abs_minus_one [simp]: "abs (-1) = (1::'a::{linordered_idom,number_ring})"
1551 by (simp add: abs_if)
1553 lemma abs_power_minus_one [simp]:
1554 "abs(-1 ^ n) = (1::'a::{linordered_idom,number_ring})"
1555 by (simp add: power_abs)
1557 lemma of_int_number_of_eq [simp]:
1558 "of_int (number_of v) = (number_of v :: 'a :: number_ring)"
1559 by (simp add: number_of_eq)
1561 text{*Lemmas for specialist use, NOT as default simprules*}
1562 lemma mult_2: "2 * z = (z+z::'a::number_ring)"
1563 unfolding one_add_one_is_two [symmetric] left_distrib by simp
1565 lemma mult_2_right: "z * 2 = (z+z::'a::number_ring)"
1566 by (subst mult_commute, rule mult_2)
1569 subsection{*More Inequality Reasoning*}
1571 lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
1574 lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
1577 lemma zle_diff1_eq [simp]: "(w \<le> z - (1::int)) = (w<z)"
1580 lemma zle_add1_eq_le [simp]: "(w < z + (1::int)) = (w\<le>z)"
1583 lemma int_one_le_iff_zero_less: "((1::int) \<le> z) = (0 < z)"
1587 subsection{*The functions @{term nat} and @{term int}*}
1589 text{*Simplify the terms @{term "int 0"}, @{term "int(Suc 0)"} and
1591 declare Zero_int_def [symmetric, simp]
1592 declare One_int_def [symmetric, simp]
1594 lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp]
1596 (* FIXME: duplicates nat_zero *)
1597 lemma nat_0: "nat 0 = 0"
1598 by (simp add: nat_eq_iff)
1600 lemma nat_1: "nat 1 = Suc 0"
1601 by (subst nat_eq_iff, simp)
1603 lemma nat_2: "nat 2 = Suc (Suc 0)"
1604 by (subst nat_eq_iff, simp)
1606 lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
1607 apply (insert zless_nat_conj [of 1 z])
1608 apply (auto simp add: nat_1)
1611 text{*This simplifies expressions of the form @{term "int n = z"} where
1612 z is an integer literal.*}
1613 lemmas int_eq_iff_number_of [simp] = int_eq_iff [of _ "number_of v", standard]
1615 lemma split_nat [arith_split]:
1616 "P(nat(i::int)) = ((\<forall>n. i = of_nat n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
1617 (is "?P = (?L & ?R)")
1618 proof (cases "i < 0")
1619 case True thus ?thesis by auto
1624 assume ?P thus ?L using False by clarsimp
1626 assume ?L thus ?P using False by simp
1628 with False show ?thesis by simp
1634 lemma of_int_of_nat [nitpick_simp]:
1635 "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))"
1636 proof (cases "k < 0")
1637 case True then have "0 \<le> - k" by simp
1638 then have "of_nat (nat (- k)) = of_int (- k)" by (rule of_nat_nat)
1639 with True show ?thesis by simp
1641 case False then show ?thesis by (simp add: not_less of_nat_nat)
1646 lemma nat_mult_distrib:
1649 shows "nat (z * z') = nat z * nat z'"
1650 proof (cases "0 \<le> z'")
1651 case False with assms have "z * z' \<le> 0"
1652 by (simp add: not_le mult_le_0_iff)
1653 then have "nat (z * z') = 0" by simp
1654 moreover from False have "nat z' = 0" by simp
1655 ultimately show ?thesis by simp
1657 case True with assms have ge_0: "z * z' \<ge> 0" by (simp add: zero_le_mult_iff)
1659 by (rule injD [of "of_nat :: nat \<Rightarrow> int", OF inj_of_nat])
1660 (simp only: of_nat_mult of_nat_nat [OF True]
1661 of_nat_nat [OF assms] of_nat_nat [OF ge_0], simp)
1664 lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"
1666 apply (rule_tac [2] nat_mult_distrib, auto)
1669 lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
1670 apply (cases "z=0 | w=0")
1671 apply (auto simp add: abs_if nat_mult_distrib [symmetric]
1672 nat_mult_distrib_neg [symmetric] mult_less_0_iff)
1676 subsection "Induction principles for int"
1678 text{*Well-founded segments of the integers*}
1681 int_ge_less_than :: "int => (int * int) set"
1683 "int_ge_less_than d = {(z',z). d \<le> z' & z' < z}"
1685 theorem wf_int_ge_less_than: "wf (int_ge_less_than d)"
1687 have "int_ge_less_than d \<subseteq> measure (%z. nat (z-d))"
1688 by (auto simp add: int_ge_less_than_def)
1690 by (rule wf_subset [OF wf_measure])
1693 text{*This variant looks odd, but is typical of the relations suggested
1697 int_ge_less_than2 :: "int => (int * int) set"
1699 "int_ge_less_than2 d = {(z',z). d \<le> z & z' < z}"
1701 theorem wf_int_ge_less_than2: "wf (int_ge_less_than2 d)"
1703 have "int_ge_less_than2 d \<subseteq> measure (%z. nat (1+z-d))"
1704 by (auto simp add: int_ge_less_than2_def)
1706 by (rule wf_subset [OF wf_measure])
1710 int :: "nat \<Rightarrow> int"
1712 "int \<equiv> of_nat"
1714 (* `set:int': dummy construction *)
1715 theorem int_ge_induct [case_names base step, induct set: int]:
1717 assumes ge: "k \<le> i" and
1719 step: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
1722 { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i"
1725 hence "i = k" by arith
1726 thus "P i" using base by simp
1729 then have "n = nat((i - 1) - k)" by arith
1731 have ki1: "k \<le> i - 1" using Suc.prems by arith
1733 have "P(i - 1)" by(rule Suc.hyps)
1734 from step[OF ki1 this] show ?case by simp
1737 with ge show ?thesis by fast
1740 (* `set:int': dummy construction *)
1741 theorem int_gr_induct [case_names base step, induct set: int]:
1742 assumes gr: "k < (i::int)" and
1744 step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
1746 apply(rule int_ge_induct[of "k + 1"])
1747 using gr apply arith
1749 apply (rule step, simp+)
1752 theorem int_le_induct[consumes 1,case_names base step]:
1753 assumes le: "i \<le> (k::int)" and
1755 step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
1758 { fix n have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i"
1761 hence "i = k" by arith
1762 thus "P i" using base by simp
1765 hence "n = nat(k - (i+1))" by arith
1767 have ki1: "i + 1 \<le> k" using Suc.prems by arith
1769 have "P(i+1)" by(rule Suc.hyps)
1770 from step[OF ki1 this] show ?case by simp
1773 with le show ?thesis by fast
1776 theorem int_less_induct [consumes 1,case_names base step]:
1777 assumes less: "(i::int) < k" and
1778 base: "P(k - 1)" and
1779 step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
1781 apply(rule int_le_induct[of _ "k - 1"])
1782 using less apply arith
1784 apply (rule step, simp+)
1787 theorem int_bidirectional_induct [case_names base step1 step2]:
1790 and step1: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
1791 and step2: "\<And>i. k \<ge> i \<Longrightarrow> P i \<Longrightarrow> P (i - 1)"
1794 have "i \<le> k \<or> i \<ge> k" by arith
1795 then show ?thesis proof
1796 assume "i \<ge> k" then show ?thesis using base
1797 by (rule int_ge_induct) (fact step1)
1799 assume "i \<le> k" then show ?thesis using base
1800 by (rule int_le_induct) (fact step2)
1804 subsection{*Intermediate value theorems*}
1806 lemma int_val_lemma:
1807 "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->
1808 f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
1809 unfolding One_nat_def
1810 apply (induct n, simp)
1812 apply (erule impE, simp)
1813 apply (erule_tac x = n in allE, simp)
1814 apply (case_tac "k = f (Suc n)")
1817 apply (simp add: abs_if split add: split_if_asm)
1818 apply (blast intro: le_SucI)
1821 lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
1823 lemma nat_intermed_int_val:
1824 "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;
1825 f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
1826 apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k
1828 unfolding One_nat_def
1831 apply (rule_tac x = "i+m" in exI, arith)
1835 subsection{*Products and 1, by T. M. Rasmussen*}
1837 lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))"
1840 lemma abs_zmult_eq_1:
1841 assumes mn: "\<bar>m * n\<bar> = 1"
1842 shows "\<bar>m\<bar> = (1::int)"
1844 have 0: "m \<noteq> 0 & n \<noteq> 0" using mn
1846 have "~ (2 \<le> \<bar>m\<bar>)"
1848 assume "2 \<le> \<bar>m\<bar>"
1849 hence "2*\<bar>n\<bar> \<le> \<bar>m\<bar>*\<bar>n\<bar>"
1850 by (simp add: mult_mono 0)
1851 also have "... = \<bar>m*n\<bar>"
1852 by (simp add: abs_mult)
1855 finally have "2*\<bar>n\<bar> \<le> 1" .
1856 thus "False" using 0
1859 thus ?thesis using 0
1863 lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1"
1864 by (insert abs_zmult_eq_1 [of m n], arith)
1866 lemma pos_zmult_eq_1_iff:
1867 assumes "0 < (m::int)" shows "(m * n = 1) = (m = 1 & n = 1)"
1869 from assms have "m * n = 1 ==> m = 1" by (auto dest: pos_zmult_eq_1_iff_lemma)
1870 thus ?thesis by (auto dest: pos_zmult_eq_1_iff_lemma)
1873 lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
1875 apply (frule pos_zmult_eq_1_iff_lemma)
1876 apply (simp add: mult_commute [of m])
1877 apply (frule pos_zmult_eq_1_iff_lemma, auto)
1880 lemma infinite_UNIV_int: "\<not> finite (UNIV::int set)"
1882 assume "finite (UNIV::int set)"
1883 moreover have "inj (\<lambda>i\<Colon>int. 2 * i)"
1885 ultimately have "surj (\<lambda>i\<Colon>int. 2 * i)"
1886 by (rule finite_UNIV_inj_surj)
1887 then obtain i :: int where "1 = 2 * i" by (rule surjE)
1888 then show False by (simp add: pos_zmult_eq_1_iff)
1892 subsection {* Further theorems on numerals *}
1894 subsubsection{*Special Simplification for Constants*}
1896 text{*These distributive laws move literals inside sums and differences.*}
1898 lemmas left_distrib_number_of [simp] =
1899 left_distrib [of _ _ "number_of v", standard]
1901 lemmas right_distrib_number_of [simp] =
1902 right_distrib [of "number_of v", standard]
1904 lemmas left_diff_distrib_number_of [simp] =
1905 left_diff_distrib [of _ _ "number_of v", standard]
1907 lemmas right_diff_distrib_number_of [simp] =
1908 right_diff_distrib [of "number_of v", standard]
1910 text{*These are actually for fields, like real: but where else to put them?*}
1912 lemmas zero_less_divide_iff_number_of [simp, no_atp] =
1913 zero_less_divide_iff [of "number_of w", standard]
1915 lemmas divide_less_0_iff_number_of [simp, no_atp] =
1916 divide_less_0_iff [of "number_of w", standard]
1918 lemmas zero_le_divide_iff_number_of [simp, no_atp] =
1919 zero_le_divide_iff [of "number_of w", standard]
1921 lemmas divide_le_0_iff_number_of [simp, no_atp] =
1922 divide_le_0_iff [of "number_of w", standard]
1925 text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}. It looks
1926 strange, but then other simprocs simplify the quotient.*}
1928 lemmas inverse_eq_divide_number_of [simp] =
1929 inverse_eq_divide [of "number_of w", standard]
1931 text {*These laws simplify inequalities, moving unary minus from a term
1934 lemmas less_minus_iff_number_of [simp, no_atp] =
1935 less_minus_iff [of "number_of v", standard]
1937 lemmas le_minus_iff_number_of [simp, no_atp] =
1938 le_minus_iff [of "number_of v", standard]
1940 lemmas equation_minus_iff_number_of [simp, no_atp] =
1941 equation_minus_iff [of "number_of v", standard]
1943 lemmas minus_less_iff_number_of [simp, no_atp] =
1944 minus_less_iff [of _ "number_of v", standard]
1946 lemmas minus_le_iff_number_of [simp, no_atp] =
1947 minus_le_iff [of _ "number_of v", standard]
1949 lemmas minus_equation_iff_number_of [simp, no_atp] =
1950 minus_equation_iff [of _ "number_of v", standard]
1953 text{*To Simplify Inequalities Where One Side is the Constant 1*}
1955 lemma less_minus_iff_1 [simp,no_atp]:
1956 fixes b::"'b::{linordered_idom,number_ring}"
1957 shows "(1 < - b) = (b < -1)"
1960 lemma le_minus_iff_1 [simp,no_atp]:
1961 fixes b::"'b::{linordered_idom,number_ring}"
1962 shows "(1 \<le> - b) = (b \<le> -1)"
1965 lemma equation_minus_iff_1 [simp,no_atp]:
1966 fixes b::"'b::number_ring"
1967 shows "(1 = - b) = (b = -1)"
1968 by (subst equation_minus_iff, auto)
1970 lemma minus_less_iff_1 [simp,no_atp]:
1971 fixes a::"'b::{linordered_idom,number_ring}"
1972 shows "(- a < 1) = (-1 < a)"
1975 lemma minus_le_iff_1 [simp,no_atp]:
1976 fixes a::"'b::{linordered_idom,number_ring}"
1977 shows "(- a \<le> 1) = (-1 \<le> a)"
1980 lemma minus_equation_iff_1 [simp,no_atp]:
1981 fixes a::"'b::number_ring"
1982 shows "(- a = 1) = (a = -1)"
1983 by (subst minus_equation_iff, auto)
1986 text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
1988 lemmas mult_less_cancel_left_number_of [simp, no_atp] =
1989 mult_less_cancel_left [of "number_of v", standard]
1991 lemmas mult_less_cancel_right_number_of [simp, no_atp] =
1992 mult_less_cancel_right [of _ "number_of v", standard]
1994 lemmas mult_le_cancel_left_number_of [simp, no_atp] =
1995 mult_le_cancel_left [of "number_of v", standard]
1997 lemmas mult_le_cancel_right_number_of [simp, no_atp] =
1998 mult_le_cancel_right [of _ "number_of v", standard]
2001 text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
2003 lemmas le_divide_eq_number_of1 [simp] = le_divide_eq [of _ _ "number_of w", standard]
2004 lemmas divide_le_eq_number_of1 [simp] = divide_le_eq [of _ "number_of w", standard]
2005 lemmas less_divide_eq_number_of1 [simp] = less_divide_eq [of _ _ "number_of w", standard]
2006 lemmas divide_less_eq_number_of1 [simp] = divide_less_eq [of _ "number_of w", standard]
2007 lemmas eq_divide_eq_number_of1 [simp] = eq_divide_eq [of _ _ "number_of w", standard]
2008 lemmas divide_eq_eq_number_of1 [simp] = divide_eq_eq [of _ "number_of w", standard]
2011 subsubsection{*Optional Simplification Rules Involving Constants*}
2013 text{*Simplify quotients that are compared with a literal constant.*}
2015 lemmas le_divide_eq_number_of = le_divide_eq [of "number_of w", standard]
2016 lemmas divide_le_eq_number_of = divide_le_eq [of _ _ "number_of w", standard]
2017 lemmas less_divide_eq_number_of = less_divide_eq [of "number_of w", standard]
2018 lemmas divide_less_eq_number_of = divide_less_eq [of _ _ "number_of w", standard]
2019 lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w", standard]
2020 lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w", standard]
2023 text{*Not good as automatic simprules because they cause case splits.*}
2024 lemmas divide_const_simps =
2025 le_divide_eq_number_of divide_le_eq_number_of less_divide_eq_number_of
2026 divide_less_eq_number_of eq_divide_eq_number_of divide_eq_eq_number_of
2027 le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
2029 text{*Division By @{text "-1"}*}
2031 lemma divide_minus1 [simp]:
2032 "x/-1 = -(x::'a::{field_inverse_zero, number_ring})"
2035 lemma minus1_divide [simp]:
2036 "-1 / (x::'a::{field_inverse_zero, number_ring}) = - (1/x)"
2037 by (simp add: divide_inverse)
2039 lemma half_gt_zero_iff:
2040 "(0 < r/2) = (0 < (r::'a::{linordered_field_inverse_zero,number_ring}))"
2043 lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2, standard]
2045 lemma divide_Numeral1:
2046 "(x::'a::{field, number_ring}) / Numeral1 = x"
2049 lemma divide_Numeral0:
2050 "(x::'a::{field_inverse_zero, number_ring}) / Numeral0 = 0"
2054 subsection {* The divides relation *}
2056 lemma zdvd_antisym_nonneg:
2057 "0 <= m ==> 0 <= n ==> m dvd n ==> n dvd m ==> m = (n::int)"
2058 apply (simp add: dvd_def, auto)
2059 apply (auto simp add: mult_assoc zero_le_mult_iff zmult_eq_1_iff)
2062 lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a"
2063 shows "\<bar>a\<bar> = \<bar>b\<bar>"
2065 assume "a = 0" with assms show ?thesis by simp
2067 assume "a \<noteq> 0"
2068 from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast
2069 from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast
2070 from k k' have "a = a*k*k'" by simp
2071 with mult_cancel_left1[where c="a" and b="k*k'"]
2072 have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult_assoc)
2073 hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff)
2074 thus ?thesis using k k' by auto
2077 lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
2078 apply (subgoal_tac "m = n + (m - n)")
2079 apply (erule ssubst)
2080 apply (blast intro: dvd_add, simp)
2083 lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
2085 apply (erule_tac [2] dvd_add)
2086 apply (subgoal_tac "n = (n + k * m) - k * m")
2087 apply (erule ssubst)
2088 apply (erule dvd_diff)
2092 lemma dvd_imp_le_int:
2094 assumes "i \<noteq> 0" and "d dvd i"
2095 shows "\<bar>d\<bar> \<le> \<bar>i\<bar>"
2097 from `d dvd i` obtain k where "i = d * k" ..
2098 with `i \<noteq> 0` have "k \<noteq> 0" by auto
2099 then have "1 \<le> \<bar>k\<bar>" and "0 \<le> \<bar>d\<bar>" by auto
2100 then have "\<bar>d\<bar> * 1 \<le> \<bar>d\<bar> * \<bar>k\<bar>" by (rule mult_left_mono)
2101 with `i = d * k` show ?thesis by (simp add: abs_mult)
2104 lemma zdvd_not_zless:
2106 assumes "0 < m" and "m < n"
2107 shows "\<not> n dvd m"
2109 from assms have "0 < n" by auto
2110 assume "n dvd m" then obtain k where k: "m = n * k" ..
2111 with `0 < m` have "0 < n * k" by auto
2112 with `0 < n` have "0 < k" by (simp add: zero_less_mult_iff)
2113 with k `0 < n` `m < n` have "n * k < n * 1" by simp
2114 with `0 < n` `0 < k` show False unfolding mult_less_cancel_left by auto
2117 lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)"
2120 from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast
2121 {assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp
2122 with h have False by (simp add: mult_assoc)}
2123 hence "n = m * h" by blast
2124 thus ?thesis by simp
2127 theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
2129 have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"
2132 assume A: "int y = int x * k"
2133 then show "x dvd y" proof (cases k)
2134 case (1 n) with A have "y = x * n" by (simp add: of_nat_mult [symmetric])
2135 then show ?thesis ..
2137 case (2 n) with A have "int y = int x * (- int (Suc n))" by simp
2138 also have "\<dots> = - (int x * int (Suc n))" by (simp only: mult_minus_right)
2139 also have "\<dots> = - int (x * Suc n)" by (simp only: of_nat_mult [symmetric])
2140 finally have "- int (x * Suc n) = int y" ..
2141 then show ?thesis by (simp only: negative_eq_positive) auto
2144 then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left of_nat_mult)
2147 lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
2149 assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp
2150 hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
2151 hence "nat \<bar>x\<bar> = 1" by simp
2152 thus "\<bar>x\<bar> = 1" by (cases "x < 0", auto)
2154 assume "\<bar>x\<bar>=1"
2155 then have "x = 1 \<or> x = -1" by auto
2156 then show "x dvd 1" by (auto intro: dvdI)
2159 lemma zdvd_mult_cancel1:
2160 assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
2162 assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m"
2163 by (cases "n >0", auto simp add: minus_equation_iff)
2165 assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
2166 from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
2169 lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
2170 unfolding zdvd_int by (cases "z \<ge> 0") simp_all
2172 lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
2173 unfolding zdvd_int by (cases "z \<ge> 0") simp_all
2175 lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
2176 by (auto simp add: dvd_int_iff)
2178 lemma eq_nat_nat_iff:
2179 "0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat z = nat z' \<longleftrightarrow> z = z'"
2180 by (auto elim!: nonneg_eq_int)
2183 "0 \<le> z \<Longrightarrow> nat (z ^ n) = nat z ^ n"
2184 by (induct n) (simp_all add: nat_mult_distrib)
2186 lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
2187 apply (rule_tac z=n in int_cases)
2188 apply (auto simp add: dvd_int_iff)
2189 apply (rule_tac z=z in int_cases)
2190 apply (auto simp add: dvd_imp_le)
2196 shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)"
2198 from assms obtain k where "d = a * k" by (rule dvdE)
2200 assume "a dvd (x + t)"
2201 then obtain l where "x + t = a * l" by (rule dvdE)
2202 then have "x = a * l - t" by simp
2203 with `d = a * k` show "a dvd x + c * d + t" by simp
2205 assume "a dvd x + c * d + t"
2206 then obtain l where "x + c * d + t = a * l" by (rule dvdE)
2207 then have "x = a * l - c * d - t" by simp
2208 with `d = a * k` show "a dvd (x + t)" by simp
2213 subsection {* Configuration of the code generator *}
2215 code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int"
2217 lemmas pred_succ_numeral_code [code] =
2218 pred_bin_simps succ_bin_simps
2220 lemmas plus_numeral_code [code] =
2222 arith_extra_simps(1) [where 'a = int]
2224 lemmas minus_numeral_code [code] =
2226 arith_extra_simps(2) [where 'a = int]
2227 arith_extra_simps(5) [where 'a = int]
2229 lemmas times_numeral_code [code] =
2231 arith_extra_simps(4) [where 'a = int]
2233 instantiation int :: eq
2236 definition [code del]: "eq_class.eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
2238 instance by default (simp add: eq_int_def)
2242 lemma eq_number_of_int_code [code]:
2243 "eq_class.eq (number_of k \<Colon> int) (number_of l) \<longleftrightarrow> eq_class.eq k l"
2244 unfolding eq_int_def number_of_is_id ..
2246 lemma eq_int_code [code]:
2247 "eq_class.eq Int.Pls Int.Pls \<longleftrightarrow> True"
2248 "eq_class.eq Int.Pls Int.Min \<longleftrightarrow> False"
2249 "eq_class.eq Int.Pls (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq Int.Pls k2"
2250 "eq_class.eq Int.Pls (Int.Bit1 k2) \<longleftrightarrow> False"
2251 "eq_class.eq Int.Min Int.Pls \<longleftrightarrow> False"
2252 "eq_class.eq Int.Min Int.Min \<longleftrightarrow> True"
2253 "eq_class.eq Int.Min (Int.Bit0 k2) \<longleftrightarrow> False"
2254 "eq_class.eq Int.Min (Int.Bit1 k2) \<longleftrightarrow> eq_class.eq Int.Min k2"
2255 "eq_class.eq (Int.Bit0 k1) Int.Pls \<longleftrightarrow> eq_class.eq k1 Int.Pls"
2256 "eq_class.eq (Int.Bit1 k1) Int.Pls \<longleftrightarrow> False"
2257 "eq_class.eq (Int.Bit0 k1) Int.Min \<longleftrightarrow> False"
2258 "eq_class.eq (Int.Bit1 k1) Int.Min \<longleftrightarrow> eq_class.eq k1 Int.Min"
2259 "eq_class.eq (Int.Bit0 k1) (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq k1 k2"
2260 "eq_class.eq (Int.Bit0 k1) (Int.Bit1 k2) \<longleftrightarrow> False"
2261 "eq_class.eq (Int.Bit1 k1) (Int.Bit0 k2) \<longleftrightarrow> False"
2262 "eq_class.eq (Int.Bit1 k1) (Int.Bit1 k2) \<longleftrightarrow> eq_class.eq k1 k2"
2263 unfolding eq_equals by simp_all
2265 lemma eq_int_refl [code nbe]:
2266 "eq_class.eq (k::int) k \<longleftrightarrow> True"
2267 by (rule HOL.eq_refl)
2269 lemma less_eq_number_of_int_code [code]:
2270 "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
2271 unfolding number_of_is_id ..
2273 lemma less_eq_int_code [code]:
2274 "Int.Pls \<le> Int.Pls \<longleftrightarrow> True"
2275 "Int.Pls \<le> Int.Min \<longleftrightarrow> False"
2276 "Int.Pls \<le> Int.Bit0 k \<longleftrightarrow> Int.Pls \<le> k"
2277 "Int.Pls \<le> Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
2278 "Int.Min \<le> Int.Pls \<longleftrightarrow> True"
2279 "Int.Min \<le> Int.Min \<longleftrightarrow> True"
2280 "Int.Min \<le> Int.Bit0 k \<longleftrightarrow> Int.Min < k"
2281 "Int.Min \<le> Int.Bit1 k \<longleftrightarrow> Int.Min \<le> k"
2282 "Int.Bit0 k \<le> Int.Pls \<longleftrightarrow> k \<le> Int.Pls"
2283 "Int.Bit1 k \<le> Int.Pls \<longleftrightarrow> k < Int.Pls"
2284 "Int.Bit0 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
2285 "Int.Bit1 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
2286 "Int.Bit0 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 \<le> k2"
2287 "Int.Bit0 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
2288 "Int.Bit1 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
2289 "Int.Bit1 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
2292 lemma less_number_of_int_code [code]:
2293 "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
2294 unfolding number_of_is_id ..
2296 lemma less_int_code [code]:
2297 "Int.Pls < Int.Pls \<longleftrightarrow> False"
2298 "Int.Pls < Int.Min \<longleftrightarrow> False"
2299 "Int.Pls < Int.Bit0 k \<longleftrightarrow> Int.Pls < k"
2300 "Int.Pls < Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
2301 "Int.Min < Int.Pls \<longleftrightarrow> True"
2302 "Int.Min < Int.Min \<longleftrightarrow> False"
2303 "Int.Min < Int.Bit0 k \<longleftrightarrow> Int.Min < k"
2304 "Int.Min < Int.Bit1 k \<longleftrightarrow> Int.Min < k"
2305 "Int.Bit0 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
2306 "Int.Bit1 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
2307 "Int.Bit0 k < Int.Min \<longleftrightarrow> k \<le> Int.Min"
2308 "Int.Bit1 k < Int.Min \<longleftrightarrow> k < Int.Min"
2309 "Int.Bit0 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
2310 "Int.Bit0 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
2311 "Int.Bit1 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
2312 "Int.Bit1 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 < k2"
2316 nat_aux :: "int \<Rightarrow> nat \<Rightarrow> nat" where
2317 "nat_aux i n = nat i + n"
2320 "nat_aux i n = (if i \<le> 0 then n else nat_aux (i - 1) (Suc n))" -- {* tail recursive *}
2321 by (auto simp add: nat_aux_def nat_eq_iff linorder_not_le order_less_imp_le
2322 dest: zless_imp_add1_zle)
2324 lemma [code]: "nat i = nat_aux i 0"
2325 by (simp add: nat_aux_def)
2327 hide_const (open) nat_aux
2329 lemma zero_is_num_zero [code, code_unfold_post]:
2330 "(0\<Colon>int) = Numeral0"
2333 lemma one_is_num_one [code, code_unfold_post]:
2334 "(1\<Colon>int) = Numeral1"
2340 code_modulename OCaml
2343 code_modulename Haskell
2349 val term_of_int = HOLogic.mk_number HOLogic.intT;
2353 let val j = one_of [~1, 1] * random_range 0 i
2354 in (j, fn () => term_of_int j) end;
2360 fun strip_number_of (@{term "Int.number_of :: int => int"} $ t) = t
2361 | strip_number_of t = t;
2363 fun numeral_codegen thy defs dep module b t gr =
2364 let val i = HOLogic.dest_numeral (strip_number_of t)
2366 SOME (Codegen.str (string_of_int i),
2367 snd (Codegen.invoke_tycodegen thy defs dep module false HOLogic.intT gr))
2368 end handle TERM _ => NONE;
2372 Codegen.add_codegen "numeral_codegen" numeral_codegen
2378 "number_of :: int \<Rightarrow> int" ("(_)")
2381 "uminus :: int => int" ("~")
2382 "op + :: int => int => int" ("(_ +/ _)")
2383 "op * :: int => int => int" ("(_ */ _)")
2384 "op \<le> :: int => int => bool" ("(_ <=/ _)")
2385 "op < :: int => int => bool" ("(_ </ _)")
2387 quickcheck_params [default_type = int]
2389 hide_const (open) Pls Min Bit0 Bit1 succ pred
2392 subsection {* Legacy theorems *}
2394 lemmas zminus_zminus = minus_minus [of "z::int", standard]
2395 lemmas zminus_0 = minus_zero [where 'a=int]
2396 lemmas zminus_zadd_distrib = minus_add_distrib [of "z::int" "w", standard]
2397 lemmas zadd_commute = add_commute [of "z::int" "w", standard]
2398 lemmas zadd_assoc = add_assoc [of "z1::int" "z2" "z3", standard]
2399 lemmas zadd_left_commute = add_left_commute [of "x::int" "y" "z", standard]
2400 lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute
2401 lemmas zmult_ac = mult_ac
2402 lemmas zadd_0 = add_0_left [of "z::int", standard]
2403 lemmas zadd_0_right = add_0_right [of "z::int", standard]
2404 lemmas zadd_zminus_inverse2 = left_minus [of "z::int", standard]
2405 lemmas zmult_zminus = mult_minus_left [of "z::int" "w", standard]
2406 lemmas zmult_commute = mult_commute [of "z::int" "w", standard]
2407 lemmas zmult_assoc = mult_assoc [of "z1::int" "z2" "z3", standard]
2408 lemmas zadd_zmult_distrib = left_distrib [of "z1::int" "z2" "w", standard]
2409 lemmas zadd_zmult_distrib2 = right_distrib [of "w::int" "z1" "z2", standard]
2410 lemmas zdiff_zmult_distrib = left_diff_distrib [of "z1::int" "z2" "w", standard]
2411 lemmas zdiff_zmult_distrib2 = right_diff_distrib [of "w::int" "z1" "z2", standard]
2413 lemmas zmult_1 = mult_1_left [of "z::int", standard]
2414 lemmas zmult_1_right = mult_1_right [of "z::int", standard]
2416 lemmas zle_refl = order_refl [of "w::int", standard]
2417 lemmas zle_trans = order_trans [where 'a=int and x="i" and y="j" and z="k", standard]
2418 lemmas zle_antisym = order_antisym [of "z::int" "w", standard]
2419 lemmas zle_linear = linorder_linear [of "z::int" "w", standard]
2420 lemmas zless_linear = linorder_less_linear [where 'a = int]
2422 lemmas zadd_left_mono = add_left_mono [of "i::int" "j" "k", standard]
2423 lemmas zadd_strict_right_mono = add_strict_right_mono [of "i::int" "j" "k", standard]
2424 lemmas zadd_zless_mono = add_less_le_mono [of "w'::int" "w" "z'" "z", standard]
2426 lemmas int_0_less_1 = zero_less_one [where 'a=int]
2427 lemmas int_0_neq_1 = zero_neq_one [where 'a=int]
2429 lemmas inj_int = inj_of_nat [where 'a=int]
2430 lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
2431 lemmas int_mult = of_nat_mult [where 'a=int]
2432 lemmas zmult_int = of_nat_mult [where 'a=int, symmetric]
2433 lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="n", standard]
2434 lemmas zless_int = of_nat_less_iff [where 'a=int]
2435 lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="k", standard]
2436 lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int]
2437 lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
2438 lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="n", standard]
2439 lemmas int_0 = of_nat_0 [where 'a=int]
2440 lemmas int_1 = of_nat_1 [where 'a=int]
2441 lemmas int_Suc = of_nat_Suc [where 'a=int]
2442 lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m", standard]
2443 lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
2444 lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
2445 lemmas zless_le = less_int_def
2446 lemmas int_eq_of_nat = TrueI
2448 lemma zpower_zadd_distrib:
2449 "x ^ (y + z) = ((x ^ y) * (x ^ z)::int)"
2452 lemma zero_less_zpower_abs_iff:
2453 "(0 < abs x ^ n) \<longleftrightarrow> (x \<noteq> (0::int) | n = 0)"
2454 by (rule zero_less_power_abs_iff)
2456 lemma zero_le_zpower_abs: "(0::int) \<le> abs x ^ n"
2457 by (rule zero_le_power_abs)
2459 lemma zpower_zpower:
2460 "(x ^ y) ^ z = (x ^ (y * z)::int)"
2461 by (rule power_mult [symmetric])
2464 "int (m ^ n) = int m ^ n"
2465 by (rule of_nat_power)
2467 lemmas zpower_int = int_power [symmetric]