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 context linordered_idom
330 lemma of_int_le_iff [simp]:
331 "of_int w \<le> of_int z \<longleftrightarrow> w \<le> z"
332 by (cases w, cases z, simp add: of_int le minus algebra_simps of_nat_add [symmetric] del: of_nat_add)
334 text{*Special cases where either operand is zero*}
335 lemmas of_int_0_le_iff [simp] = of_int_le_iff [of 0, simplified]
336 lemmas of_int_le_0_iff [simp] = of_int_le_iff [of _ 0, simplified]
338 lemma of_int_less_iff [simp]:
339 "of_int w < of_int z \<longleftrightarrow> w < z"
340 by (simp add: not_le [symmetric] linorder_not_le [symmetric])
342 text{*Special cases where either operand is zero*}
343 lemmas of_int_0_less_iff [simp] = of_int_less_iff [of 0, simplified]
344 lemmas of_int_less_0_iff [simp] = of_int_less_iff [of _ 0, simplified]
348 text{*Class for unital rings with characteristic zero.
349 Includes non-ordered rings like the complex numbers.*}
350 class ring_char_0 = ring_1 + semiring_char_0
353 lemma of_int_eq_iff [simp]:
354 "of_int w = of_int z \<longleftrightarrow> w = z"
355 apply (cases w, cases z, simp add: of_int)
356 apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq)
357 apply (simp only: of_nat_add [symmetric] of_nat_eq_iff)
360 text{*Special cases where either operand is zero*}
361 lemmas of_int_0_eq_iff [simp] = of_int_eq_iff [of 0, simplified]
362 lemmas of_int_eq_0_iff [simp] = of_int_eq_iff [of _ 0, simplified]
366 text{*Every @{text linordered_idom} has characteristic zero.*}
367 subclass (in linordered_idom) ring_char_0 by intro_locales
369 lemma of_int_eq_id [simp]: "of_int = id"
371 fix z show "of_int z = id z"
372 by (cases z) (simp add: of_int add minus int_def diff_minus)
376 subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *}
379 nat :: "int \<Rightarrow> nat"
381 [code del]: "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
383 lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
385 have "(\<lambda>(x,y). {x-y}) respects intrel"
386 by (simp add: congruent_def) arith
388 by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
391 lemma nat_int [simp]: "nat (of_nat n) = n"
392 by (simp add: nat int_def)
394 (* FIXME: duplicates nat_0 *)
395 lemma nat_zero [simp]: "nat 0 = 0"
396 by (simp add: Zero_int_def nat)
398 lemma int_nat_eq [simp]: "of_nat (nat z) = (if 0 \<le> z then z else 0)"
399 by (cases z, simp add: nat le int_def Zero_int_def)
401 corollary nat_0_le: "0 \<le> z ==> of_nat (nat z) = z"
404 lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
405 by (cases z, simp add: nat le Zero_int_def)
407 lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"
408 apply (cases w, cases z)
409 apply (simp add: nat le linorder_not_le [symmetric] Zero_int_def, arith)
412 text{*An alternative condition is @{term "0 \<le> w"} *}
413 corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
414 by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
416 corollary nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"
417 by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
419 lemma zless_nat_conj [simp]: "(nat w < nat z) = (0 < z & w < z)"
420 apply (cases w, cases z)
421 apply (simp add: nat le Zero_int_def linorder_not_le [symmetric], arith)
426 assumes "0 \<le> z" and "\<And>m. z = of_nat m \<Longrightarrow> P"
428 using assms by (blast dest: nat_0_le sym)
430 lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = of_nat m else m=0)"
431 by (cases w, simp add: nat le int_def Zero_int_def, arith)
433 corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = of_nat m else m=0)"
434 by (simp only: eq_commute [of m] nat_eq_iff)
436 lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)"
438 apply (simp add: nat le int_def Zero_int_def linorder_not_le[symmetric], arith)
441 lemma nat_0_iff[simp]: "nat(i::int) = 0 \<longleftrightarrow> i\<le>0"
442 by(simp add: nat_eq_iff) arith
444 lemma int_eq_iff: "(of_nat m = z) = (m = nat z & 0 \<le> z)"
445 by (auto simp add: nat_eq_iff2)
447 lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)"
448 by (insert zless_nat_conj [of 0], auto)
450 lemma nat_add_distrib:
451 "[| (0::int) \<le> z; 0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"
452 by (cases z, cases z', simp add: nat add le Zero_int_def)
454 lemma nat_diff_distrib:
455 "[| (0::int) \<le> z'; z' \<le> z |] ==> nat (z-z') = nat z - nat z'"
456 by (cases z, cases z',
457 simp add: nat add minus diff_minus le Zero_int_def)
459 lemma nat_zminus_int [simp]: "nat (- (of_nat n)) = 0"
460 by (simp add: int_def minus nat Zero_int_def)
462 lemma zless_nat_eq_int_zless: "(m < nat z) = (of_nat m < z)"
463 by (cases z, simp add: nat less int_def, arith)
468 lemma of_nat_nat: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z"
469 by (cases z rule: eq_Abs_Integ)
470 (simp add: nat le of_int Zero_int_def of_nat_diff)
474 text {* For termination proofs: *}
475 lemma measure_function_int[measure_function]: "is_measure (nat o abs)" ..
478 subsection{*Lemmas about the Function @{term of_nat} and Orderings*}
480 lemma negative_zless_0: "- (of_nat (Suc n)) < (0 \<Colon> int)"
481 by (simp add: order_less_le del: of_nat_Suc)
483 lemma negative_zless [iff]: "- (of_nat (Suc n)) < (of_nat m \<Colon> int)"
484 by (rule negative_zless_0 [THEN order_less_le_trans], simp)
486 lemma negative_zle_0: "- of_nat n \<le> (0 \<Colon> int)"
487 by (simp add: minus_le_iff)
489 lemma negative_zle [iff]: "- of_nat n \<le> (of_nat m \<Colon> int)"
490 by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff])
492 lemma not_zle_0_negative [simp]: "~ (0 \<le> - (of_nat (Suc n) \<Colon> int))"
493 by (subst le_minus_iff, simp del: of_nat_Suc)
495 lemma int_zle_neg: "((of_nat n \<Colon> int) \<le> - of_nat m) = (n = 0 & m = 0)"
496 by (simp add: int_def le minus Zero_int_def)
498 lemma not_int_zless_negative [simp]: "~ ((of_nat n \<Colon> int) < - of_nat m)"
499 by (simp add: linorder_not_less)
501 lemma negative_eq_positive [simp]: "((- of_nat n \<Colon> int) = of_nat m) = (n = 0 & m = 0)"
502 by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg)
504 lemma zle_iff_zadd: "(w\<Colon>int) \<le> z \<longleftrightarrow> (\<exists>n. z = w + of_nat n)"
506 have "(w \<le> z) = (0 \<le> z - w)"
507 by (simp only: le_diff_eq add_0_left)
508 also have "\<dots> = (\<exists>n. z - w = of_nat n)"
509 by (auto elim: zero_le_imp_eq_int)
510 also have "\<dots> = (\<exists>n. z = w + of_nat n)"
511 by (simp only: algebra_simps)
512 finally show ?thesis .
515 lemma zadd_int_left: "of_nat m + (of_nat n + z) = of_nat (m + n) + (z\<Colon>int)"
518 lemma int_Suc0_eq_1: "of_nat (Suc 0) = (1\<Colon>int)"
521 text{*This version is proved for all ordered rings, not just integers!
522 It is proved here because attribute @{text arith_split} is not available
523 in theory @{text Rings}.
524 But is it really better than just rewriting with @{text abs_if}?*}
525 lemma abs_split [arith_split,no_atp]:
526 "P(abs(a::'a::linordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
527 by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
529 lemma negD: "(x \<Colon> int) < 0 \<Longrightarrow> \<exists>n. x = - (of_nat (Suc n))"
531 apply (auto simp add: le minus Zero_int_def int_def order_less_le)
532 apply (rule_tac x="y - Suc x" in exI, arith)
536 subsection {* Cases and induction *}
538 text{*Now we replace the case analysis rule by a more conventional one:
539 whether an integer is negative or not.*}
541 theorem int_cases [cases type: int, case_names nonneg neg]:
542 "[|!! n. (z \<Colon> int) = of_nat n ==> P; !! n. z = - (of_nat (Suc n)) ==> P |] ==> P"
543 apply (cases "z < 0", blast dest!: negD)
544 apply (simp add: linorder_not_less del: of_nat_Suc)
546 apply (blast dest: nat_0_le [THEN sym])
549 theorem int_induct [induct type: int, case_names nonneg neg]:
550 "[|!! n. P (of_nat n \<Colon> int); !!n. P (- (of_nat (Suc n))) |] ==> P z"
551 by (cases z rule: int_cases) auto
553 text{*Contributed by Brian Huffman*}
554 theorem int_diff_cases:
555 obtains (diff) m n where "(z\<Colon>int) = of_nat m - of_nat n"
556 apply (cases z rule: eq_Abs_Integ)
557 apply (rule_tac m=x and n=y in diff)
558 apply (simp add: int_def diff_def minus add)
562 subsection {* Binary representation *}
565 This formalization defines binary arithmetic in terms of the integers
566 rather than using a datatype. This avoids multiple representations (leading
567 zeroes, etc.) See @{text "ZF/Tools/twos-compl.ML"}, function @{text
568 int_of_binary}, for the numerical interpretation.
570 The representation expects that @{text "(m mod 2)"} is 0 or 1,
571 even if m is negative;
572 For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
573 @{text "-5 = (-3)*2 + 1"}.
575 This two's complement binary representation derives from the paper
576 "An Efficient Representation of Arithmetic for Term Rewriting" by
577 Dave Cohen and Phil Watson, Rewriting Techniques and Applications,
578 Springer LNCS 488 (240-251), 1991.
581 subsubsection {* The constructors @{term Bit0}, @{term Bit1}, @{term Pls} and @{term Min} *}
585 [code del]: "Pls = 0"
589 [code del]: "Min = - 1"
592 Bit0 :: "int \<Rightarrow> int" where
593 [code del]: "Bit0 k = k + k"
596 Bit1 :: "int \<Rightarrow> int" where
597 [code del]: "Bit1 k = 1 + k + k"
599 class number = -- {* for numeric types: nat, int, real, \dots *}
600 fixes number_of :: "int \<Rightarrow> 'a"
602 use "Tools/numeral.ML"
605 "_Numeral" :: "num_const \<Rightarrow> 'a" ("_")
607 use "Tools/numeral_syntax.ML"
608 setup Numeral_Syntax.setup
611 "Numeral0 \<equiv> number_of Pls"
614 "Numeral1 \<equiv> number_of (Bit1 Pls)"
616 lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"
617 -- {* Unfold all @{text let}s involving constants *}
621 succ :: "int \<Rightarrow> int" where
622 [code del]: "succ k = k + 1"
625 pred :: "int \<Rightarrow> int" where
626 [code del]: "pred k = k - 1"
629 max_number_of [simp] = max_def
630 [of "number_of u" "number_of v", standard]
632 min_number_of [simp] = min_def
633 [of "number_of u" "number_of v", standard]
634 -- {* unfolding @{text minx} and @{text max} on numerals *}
636 lemmas numeral_simps =
637 succ_def pred_def Pls_def Min_def Bit0_def Bit1_def
639 text {* Removal of leading zeroes *}
641 lemma Bit0_Pls [simp, code_post]:
643 unfolding numeral_simps by simp
645 lemma Bit1_Min [simp, code_post]:
647 unfolding numeral_simps by simp
649 lemmas normalize_bin_simps =
653 subsubsection {* Successor and predecessor functions *}
658 "succ Pls = Bit1 Pls"
659 unfolding numeral_simps by simp
663 unfolding numeral_simps by simp
666 "succ (Bit0 k) = Bit1 k"
667 unfolding numeral_simps by simp
670 "succ (Bit1 k) = Bit0 (succ k)"
671 unfolding numeral_simps by simp
673 lemmas succ_bin_simps [simp] =
674 succ_Pls succ_Min succ_Bit0 succ_Bit1
676 text {* Predecessor *}
680 unfolding numeral_simps by simp
683 "pred Min = Bit0 Min"
684 unfolding numeral_simps by simp
687 "pred (Bit0 k) = Bit1 (pred k)"
688 unfolding numeral_simps by simp
691 "pred (Bit1 k) = Bit0 k"
692 unfolding numeral_simps by simp
694 lemmas pred_bin_simps [simp] =
695 pred_Pls pred_Min pred_Bit0 pred_Bit1
698 subsubsection {* Binary arithmetic *}
704 unfolding numeral_simps by simp
708 unfolding numeral_simps by simp
711 "(Bit0 k) + (Bit0 l) = Bit0 (k + l)"
712 unfolding numeral_simps by simp
715 "(Bit0 k) + (Bit1 l) = Bit1 (k + l)"
716 unfolding numeral_simps by simp
719 "(Bit1 k) + (Bit0 l) = Bit1 (k + l)"
720 unfolding numeral_simps by simp
723 "(Bit1 k) + (Bit1 l) = Bit0 (k + succ l)"
724 unfolding numeral_simps by simp
728 unfolding numeral_simps by simp
732 unfolding numeral_simps by simp
734 lemmas add_bin_simps [simp] =
735 add_Pls add_Min add_Pls_right add_Min_right
736 add_Bit0_Bit0 add_Bit0_Bit1 add_Bit1_Bit0 add_Bit1_Bit1
742 unfolding numeral_simps by simp
746 unfolding numeral_simps by simp
749 "- (Bit0 k) = Bit0 (- k)"
750 unfolding numeral_simps by simp
753 "- (Bit1 k) = Bit1 (pred (- k))"
754 unfolding numeral_simps by simp
756 lemmas minus_bin_simps [simp] =
757 minus_Pls minus_Min minus_Bit0 minus_Bit1
759 text {* Subtraction *}
761 lemma diff_bin_simps [simp]:
764 "Pls - (Bit0 l) = Bit0 (Pls - l)"
765 "Pls - (Bit1 l) = Bit1 (Min - l)"
766 "Min - (Bit0 l) = Bit1 (Min - l)"
767 "Min - (Bit1 l) = Bit0 (Min - l)"
768 "(Bit0 k) - (Bit0 l) = Bit0 (k - l)"
769 "(Bit0 k) - (Bit1 l) = Bit1 (pred k - l)"
770 "(Bit1 k) - (Bit0 l) = Bit1 (k - l)"
771 "(Bit1 k) - (Bit1 l) = Bit0 (k - l)"
772 unfolding numeral_simps by simp_all
774 text {* Multiplication *}
778 unfolding numeral_simps by simp
782 unfolding numeral_simps by simp
785 "(Bit0 k) * l = Bit0 (k * l)"
786 unfolding numeral_simps int_distrib by simp
789 "(Bit1 k) * l = (Bit0 (k * l)) + l"
790 unfolding numeral_simps int_distrib by simp
792 lemmas mult_bin_simps [simp] =
793 mult_Pls mult_Min mult_Bit0 mult_Bit1
796 subsubsection {* Binary comparisons *}
798 text {* Preliminaries *}
800 lemma even_less_0_iff:
801 "a + a < 0 \<longleftrightarrow> a < (0::'a::linordered_idom)"
803 have "a + a < 0 \<longleftrightarrow> (1+1)*a < 0" by (simp add: left_distrib)
804 also have "(1+1)*a < 0 \<longleftrightarrow> a < 0"
805 by (simp add: mult_less_0_iff zero_less_two
806 order_less_not_sym [OF zero_less_two])
807 finally show ?thesis .
811 assumes le: "0 \<le> z"
812 shows "(0::int) < 1 + z"
814 have "0 \<le> z" by fact
815 also have "... < z + 1" by (rule less_add_one)
816 also have "... = 1 + z" by (simp add: add_ac)
817 finally show "0 < 1 + z" .
820 lemma odd_less_0_iff:
821 "(1 + z + z < 0) = (z < (0::int))"
822 proof (cases z rule: int_cases)
824 thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
825 le_imp_0_less [THEN order_less_imp_le])
828 thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1
829 add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric])
832 lemma bin_less_0_simps:
833 "Pls < 0 \<longleftrightarrow> False"
834 "Min < 0 \<longleftrightarrow> True"
835 "Bit0 w < 0 \<longleftrightarrow> w < 0"
836 "Bit1 w < 0 \<longleftrightarrow> w < 0"
837 unfolding numeral_simps
838 by (simp_all add: even_less_0_iff odd_less_0_iff)
840 lemma less_bin_lemma: "k < l \<longleftrightarrow> k - l < (0::int)"
843 lemma le_iff_pred_less: "k \<le> l \<longleftrightarrow> pred k < l"
844 unfolding numeral_simps
846 have "k - 1 < k" by simp
847 also assume "k \<le> l"
848 finally show "k - 1 < l" .
851 hence "(k - 1) + 1 \<le> l" by (rule zless_imp_add1_zle)
852 thus "k \<le> l" by simp
855 lemma succ_pred: "succ (pred x) = x"
856 unfolding numeral_simps by simp
860 lemma less_bin_simps [simp]:
861 "Pls < Pls \<longleftrightarrow> False"
862 "Pls < Min \<longleftrightarrow> False"
863 "Pls < Bit0 k \<longleftrightarrow> Pls < k"
864 "Pls < Bit1 k \<longleftrightarrow> Pls \<le> k"
865 "Min < Pls \<longleftrightarrow> True"
866 "Min < Min \<longleftrightarrow> False"
867 "Min < Bit0 k \<longleftrightarrow> Min < k"
868 "Min < Bit1 k \<longleftrightarrow> Min < k"
869 "Bit0 k < Pls \<longleftrightarrow> k < Pls"
870 "Bit0 k < Min \<longleftrightarrow> k \<le> Min"
871 "Bit1 k < Pls \<longleftrightarrow> k < Pls"
872 "Bit1 k < Min \<longleftrightarrow> k < Min"
873 "Bit0 k < Bit0 l \<longleftrightarrow> k < l"
874 "Bit0 k < Bit1 l \<longleftrightarrow> k \<le> l"
875 "Bit1 k < Bit0 l \<longleftrightarrow> k < l"
876 "Bit1 k < Bit1 l \<longleftrightarrow> k < l"
877 unfolding le_iff_pred_less
878 less_bin_lemma [of Pls]
879 less_bin_lemma [of Min]
880 less_bin_lemma [of "k"]
881 less_bin_lemma [of "Bit0 k"]
882 less_bin_lemma [of "Bit1 k"]
883 less_bin_lemma [of "pred Pls"]
884 less_bin_lemma [of "pred k"]
885 by (simp_all add: bin_less_0_simps succ_pred)
887 text {* Less-than-or-equal *}
889 lemma le_bin_simps [simp]:
890 "Pls \<le> Pls \<longleftrightarrow> True"
891 "Pls \<le> Min \<longleftrightarrow> False"
892 "Pls \<le> Bit0 k \<longleftrightarrow> Pls \<le> k"
893 "Pls \<le> Bit1 k \<longleftrightarrow> Pls \<le> k"
894 "Min \<le> Pls \<longleftrightarrow> True"
895 "Min \<le> Min \<longleftrightarrow> True"
896 "Min \<le> Bit0 k \<longleftrightarrow> Min < k"
897 "Min \<le> Bit1 k \<longleftrightarrow> Min \<le> k"
898 "Bit0 k \<le> Pls \<longleftrightarrow> k \<le> Pls"
899 "Bit0 k \<le> Min \<longleftrightarrow> k \<le> Min"
900 "Bit1 k \<le> Pls \<longleftrightarrow> k < Pls"
901 "Bit1 k \<le> Min \<longleftrightarrow> k \<le> Min"
902 "Bit0 k \<le> Bit0 l \<longleftrightarrow> k \<le> l"
903 "Bit0 k \<le> Bit1 l \<longleftrightarrow> k \<le> l"
904 "Bit1 k \<le> Bit0 l \<longleftrightarrow> k < l"
905 "Bit1 k \<le> Bit1 l \<longleftrightarrow> k \<le> l"
906 unfolding not_less [symmetric]
907 by (simp_all add: not_le)
911 lemma eq_bin_simps [simp]:
912 "Pls = Pls \<longleftrightarrow> True"
913 "Pls = Min \<longleftrightarrow> False"
914 "Pls = Bit0 l \<longleftrightarrow> Pls = l"
915 "Pls = Bit1 l \<longleftrightarrow> False"
916 "Min = Pls \<longleftrightarrow> False"
917 "Min = Min \<longleftrightarrow> True"
918 "Min = Bit0 l \<longleftrightarrow> False"
919 "Min = Bit1 l \<longleftrightarrow> Min = l"
920 "Bit0 k = Pls \<longleftrightarrow> k = Pls"
921 "Bit0 k = Min \<longleftrightarrow> False"
922 "Bit1 k = Pls \<longleftrightarrow> False"
923 "Bit1 k = Min \<longleftrightarrow> k = Min"
924 "Bit0 k = Bit0 l \<longleftrightarrow> k = l"
925 "Bit0 k = Bit1 l \<longleftrightarrow> False"
926 "Bit1 k = Bit0 l \<longleftrightarrow> False"
927 "Bit1 k = Bit1 l \<longleftrightarrow> k = l"
928 unfolding order_eq_iff [where 'a=int]
929 by (simp_all add: not_less)
932 subsection {* Converting Numerals to Rings: @{term number_of} *}
934 class number_ring = number + comm_ring_1 +
935 assumes number_of_eq: "number_of k = of_int k"
937 text {* self-embedding of the integers *}
939 instantiation int :: number_ring
942 definition int_number_of_def [code del]:
943 "number_of w = (of_int w \<Colon> int)"
946 qed (simp only: int_number_of_def)
950 lemma number_of_is_id:
951 "number_of (k::int) = k"
952 unfolding int_number_of_def by simp
954 lemma number_of_succ:
955 "number_of (succ k) = (1 + number_of k ::'a::number_ring)"
956 unfolding number_of_eq numeral_simps by simp
958 lemma number_of_pred:
959 "number_of (pred w) = (- 1 + number_of w ::'a::number_ring)"
960 unfolding number_of_eq numeral_simps by simp
962 lemma number_of_minus:
963 "number_of (uminus w) = (- (number_of w)::'a::number_ring)"
964 unfolding number_of_eq by (rule of_int_minus)
967 "number_of (v + w) = (number_of v + number_of w::'a::number_ring)"
968 unfolding number_of_eq by (rule of_int_add)
970 lemma number_of_diff:
971 "number_of (v - w) = (number_of v - number_of w::'a::number_ring)"
972 unfolding number_of_eq by (rule of_int_diff)
974 lemma number_of_mult:
975 "number_of (v * w) = (number_of v * number_of w::'a::number_ring)"
976 unfolding number_of_eq by (rule of_int_mult)
979 The correctness of shifting.
980 But it doesn't seem to give a measurable speed-up.
983 lemma double_number_of_Bit0:
984 "(1 + 1) * number_of w = (number_of (Bit0 w) ::'a::number_ring)"
985 unfolding number_of_eq numeral_simps left_distrib by simp
988 Converting numerals 0 and 1 to their abstract versions.
991 lemma numeral_0_eq_0 [simp, code_post]:
992 "Numeral0 = (0::'a::number_ring)"
993 unfolding number_of_eq numeral_simps by simp
995 lemma numeral_1_eq_1 [simp, code_post]:
996 "Numeral1 = (1::'a::number_ring)"
997 unfolding number_of_eq numeral_simps by simp
1000 Special-case simplification for small constants.
1004 Unary minus for the abstract constant 1. Cannot be inserted
1005 as a simprule until later: it is @{text number_of_Min} re-oriented!
1008 lemma numeral_m1_eq_minus_1:
1009 "(-1::'a::number_ring) = - 1"
1010 unfolding number_of_eq numeral_simps by simp
1012 lemma mult_minus1 [simp]:
1013 "-1 * z = -(z::'a::number_ring)"
1014 unfolding number_of_eq numeral_simps by simp
1016 lemma mult_minus1_right [simp]:
1017 "z * -1 = -(z::'a::number_ring)"
1018 unfolding number_of_eq numeral_simps by simp
1020 (*Negation of a coefficient*)
1021 lemma minus_number_of_mult [simp]:
1022 "- (number_of w) * z = number_of (uminus w) * (z::'a::number_ring)"
1023 unfolding number_of_eq by simp
1025 text {* Subtraction *}
1027 lemma diff_number_of_eq:
1028 "number_of v - number_of w =
1029 (number_of (v + uminus w)::'a::number_ring)"
1030 unfolding number_of_eq by simp
1032 lemma number_of_Pls:
1033 "number_of Pls = (0::'a::number_ring)"
1034 unfolding number_of_eq numeral_simps by simp
1036 lemma number_of_Min:
1037 "number_of Min = (- 1::'a::number_ring)"
1038 unfolding number_of_eq numeral_simps by simp
1040 lemma number_of_Bit0:
1041 "number_of (Bit0 w) = (0::'a::number_ring) + (number_of w) + (number_of w)"
1042 unfolding number_of_eq numeral_simps by simp
1044 lemma number_of_Bit1:
1045 "number_of (Bit1 w) = (1::'a::number_ring) + (number_of w) + (number_of w)"
1046 unfolding number_of_eq numeral_simps by simp
1049 subsubsection {* Equality of Binary Numbers *}
1051 text {* First version by Norbert Voelker *}
1053 definition (*for simplifying equalities*)
1054 iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool"
1056 "iszero z \<longleftrightarrow> z = 0"
1058 lemma iszero_0: "iszero 0"
1059 by (simp add: iszero_def)
1061 lemma not_iszero_1: "~ iszero 1"
1062 by (simp add: iszero_def eq_commute)
1064 lemma eq_number_of_eq [simp]:
1065 "((number_of x::'a::number_ring) = number_of y) =
1066 iszero (number_of (x + uminus y) :: 'a)"
1067 unfolding iszero_def number_of_add number_of_minus
1068 by (simp add: algebra_simps)
1070 lemma iszero_number_of_Pls:
1071 "iszero ((number_of Pls)::'a::number_ring)"
1072 unfolding iszero_def numeral_0_eq_0 ..
1074 lemma nonzero_number_of_Min:
1075 "~ iszero ((number_of Min)::'a::number_ring)"
1076 unfolding iszero_def numeral_m1_eq_minus_1 by simp
1079 subsubsection {* Comparisons, for Ordered Rings *}
1081 lemmas double_eq_0_iff = double_zero
1084 "1 + z + z \<noteq> (0::int)"
1085 proof (cases z rule: int_cases)
1087 have le: "0 \<le> z+z" by (simp add: nonneg add_increasing)
1088 thus ?thesis using le_imp_0_less [OF le]
1089 by (auto simp add: add_assoc)
1094 assume eq: "1 + z + z = 0"
1095 have "(0::int) < 1 + (of_nat n + of_nat n)"
1096 by (simp add: le_imp_0_less add_increasing)
1097 also have "... = - (1 + z + z)"
1098 by (simp add: neg add_assoc [symmetric])
1099 also have "... = 0" by (simp add: eq)
1100 finally have "0<0" ..
1105 lemma iszero_number_of_Bit0:
1106 "iszero (number_of (Bit0 w)::'a) =
1107 iszero (number_of w::'a::{ring_char_0,number_ring})"
1109 have "(of_int w + of_int w = (0::'a)) \<Longrightarrow> (w = 0)"
1111 assume eq: "of_int w + of_int w = (0::'a)"
1112 then have "of_int (w + w) = (of_int 0 :: 'a)" by simp
1113 then have "w + w = 0" by (simp only: of_int_eq_iff)
1114 then show "w = 0" by (simp only: double_eq_0_iff)
1117 by (auto simp add: iszero_def number_of_eq numeral_simps)
1120 lemma iszero_number_of_Bit1:
1121 "~ iszero (number_of (Bit1 w)::'a::{ring_char_0,number_ring})"
1123 have "1 + of_int w + of_int w \<noteq> (0::'a)"
1125 assume eq: "1 + of_int w + of_int w = (0::'a)"
1126 hence "of_int (1 + w + w) = (of_int 0 :: 'a)" by simp
1127 hence "1 + w + w = 0" by (simp only: of_int_eq_iff)
1128 with odd_nonzero show False by blast
1131 by (auto simp add: iszero_def number_of_eq numeral_simps)
1134 lemmas iszero_simps [simp] =
1135 iszero_0 not_iszero_1
1136 iszero_number_of_Pls nonzero_number_of_Min
1137 iszero_number_of_Bit0 iszero_number_of_Bit1
1138 (* iszero_number_of_Pls would never normally be used
1139 because its lhs simplifies to "iszero 0" *)
1141 subsubsection {* The Less-Than Relation *}
1143 lemma double_less_0_iff:
1144 "(a + a < 0) = (a < (0::'a::linordered_idom))"
1146 have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)
1147 also have "... = (a < 0)"
1148 by (simp add: mult_less_0_iff zero_less_two
1149 order_less_not_sym [OF zero_less_two])
1150 finally show ?thesis .
1154 "(1 + z + z < 0) = (z < (0::int))"
1155 proof (cases z rule: int_cases)
1157 thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
1158 le_imp_0_less [THEN order_less_imp_le])
1161 thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1
1162 add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric])
1165 text {* Less-Than or Equals *}
1167 text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *}
1169 lemmas le_number_of_eq_not_less =
1170 linorder_not_less [of "number_of w" "number_of v", symmetric,
1174 text {* Absolute value (@{term abs}) *}
1176 lemma abs_number_of:
1177 "abs(number_of x::'a::{linordered_idom,number_ring}) =
1178 (if number_of x < (0::'a) then -number_of x else number_of x)"
1179 by (simp add: abs_if)
1182 text {* Re-orientation of the equation nnn=x *}
1184 lemma number_of_reorient:
1185 "(number_of w = x) = (x = number_of w)"
1189 subsubsection {* Simplification of arithmetic operations on integer constants. *}
1191 lemmas arith_extra_simps [standard, simp] =
1192 number_of_add [symmetric]
1193 number_of_minus [symmetric]
1194 numeral_m1_eq_minus_1 [symmetric]
1195 number_of_mult [symmetric]
1196 diff_number_of_eq abs_number_of
1199 For making a minimal simpset, one must include these default simprules.
1200 Also include @{text simp_thms}.
1203 lemmas arith_simps =
1204 normalize_bin_simps pred_bin_simps succ_bin_simps
1205 add_bin_simps minus_bin_simps mult_bin_simps
1206 abs_zero abs_one arith_extra_simps
1208 text {* Simplification of relational operations *}
1210 lemma less_number_of [simp]:
1211 "(number_of x::'a::{linordered_idom,number_ring}) < number_of y \<longleftrightarrow> x < y"
1212 unfolding number_of_eq by (rule of_int_less_iff)
1214 lemma le_number_of [simp]:
1215 "(number_of x::'a::{linordered_idom,number_ring}) \<le> number_of y \<longleftrightarrow> x \<le> y"
1216 unfolding number_of_eq by (rule of_int_le_iff)
1218 lemma eq_number_of [simp]:
1219 "(number_of x::'a::{ring_char_0,number_ring}) = number_of y \<longleftrightarrow> x = y"
1220 unfolding number_of_eq by (rule of_int_eq_iff)
1223 less_number_of less_bin_simps
1224 le_number_of le_bin_simps
1225 eq_number_of_eq eq_bin_simps
1229 subsubsection {* Simplification of arithmetic when nested to the right. *}
1231 lemma add_number_of_left [simp]:
1232 "number_of v + (number_of w + z) =
1233 (number_of(v + w) + z::'a::number_ring)"
1234 by (simp add: add_assoc [symmetric])
1236 lemma mult_number_of_left [simp]:
1237 "number_of v * (number_of w * z) =
1238 (number_of(v * w) * z::'a::number_ring)"
1239 by (simp add: mult_assoc [symmetric])
1241 lemma add_number_of_diff1:
1242 "number_of v + (number_of w - c) =
1243 number_of(v + w) - (c::'a::number_ring)"
1244 by (simp add: diff_minus)
1246 lemma add_number_of_diff2 [simp]:
1247 "number_of v + (c - number_of w) =
1248 number_of (v + uminus w) + (c::'a::number_ring)"
1249 by (simp add: algebra_simps diff_number_of_eq [symmetric])
1254 subsection {* The Set of Integers *}
1259 definition Ints :: "'a set" where
1260 [code del]: "Ints = range of_int"
1265 lemma Ints_of_int [simp]: "of_int z \<in> \<int>"
1266 by (simp add: Ints_def)
1268 lemma Ints_of_nat [simp]: "of_nat n \<in> \<int>"
1269 apply (simp add: Ints_def)
1270 apply (rule range_eqI)
1271 apply (rule of_int_of_nat_eq [symmetric])
1274 lemma Ints_0 [simp]: "0 \<in> \<int>"
1275 apply (simp add: Ints_def)
1276 apply (rule range_eqI)
1277 apply (rule of_int_0 [symmetric])
1280 lemma Ints_1 [simp]: "1 \<in> \<int>"
1281 apply (simp add: Ints_def)
1282 apply (rule range_eqI)
1283 apply (rule of_int_1 [symmetric])
1286 lemma Ints_add [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a + b \<in> \<int>"
1287 apply (auto simp add: Ints_def)
1288 apply (rule range_eqI)
1289 apply (rule of_int_add [symmetric])
1292 lemma Ints_minus [simp]: "a \<in> \<int> \<Longrightarrow> -a \<in> \<int>"
1293 apply (auto simp add: Ints_def)
1294 apply (rule range_eqI)
1295 apply (rule of_int_minus [symmetric])
1298 lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a - b \<in> \<int>"
1299 apply (auto simp add: Ints_def)
1300 apply (rule range_eqI)
1301 apply (rule of_int_diff [symmetric])
1304 lemma Ints_mult [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a * b \<in> \<int>"
1305 apply (auto simp add: Ints_def)
1306 apply (rule range_eqI)
1307 apply (rule of_int_mult [symmetric])
1310 lemma Ints_power [simp]: "a \<in> \<int> \<Longrightarrow> a ^ n \<in> \<int>"
1311 by (induct n) simp_all
1313 lemma Ints_cases [cases set: Ints]:
1314 assumes "q \<in> \<int>"
1315 obtains (of_int) z where "q = of_int z"
1318 from `q \<in> \<int>` have "q \<in> range of_int" unfolding Ints_def .
1319 then obtain z where "q = of_int z" ..
1323 lemma Ints_induct [case_names of_int, induct set: Ints]:
1324 "q \<in> \<int> \<Longrightarrow> (\<And>z. P (of_int z)) \<Longrightarrow> P q"
1325 by (rule Ints_cases) auto
1329 text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
1331 lemma Ints_double_eq_0_iff:
1332 assumes in_Ints: "a \<in> Ints"
1333 shows "(a + a = 0) = (a = (0::'a::ring_char_0))"
1335 from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
1336 then obtain z where a: "a = of_int z" ..
1340 thus "a + a = 0" by simp
1342 assume eq: "a + a = 0"
1343 hence "of_int (z + z) = (of_int 0 :: 'a)" by (simp add: a)
1344 hence "z + z = 0" by (simp only: of_int_eq_iff)
1345 hence "z = 0" by (simp only: double_eq_0_iff)
1346 thus "a = 0" by (simp add: a)
1350 lemma Ints_odd_nonzero:
1351 assumes in_Ints: "a \<in> Ints"
1352 shows "1 + a + a \<noteq> (0::'a::ring_char_0)"
1354 from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
1355 then obtain z where a: "a = of_int z" ..
1358 assume eq: "1 + a + a = 0"
1359 hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
1360 hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
1361 with odd_nonzero show False by blast
1365 lemma Ints_number_of [simp]:
1366 "(number_of w :: 'a::number_ring) \<in> Ints"
1367 unfolding number_of_eq Ints_def by simp
1369 lemma Nats_number_of [simp]:
1370 "Int.Pls \<le> w \<Longrightarrow> (number_of w :: 'a::number_ring) \<in> Nats"
1371 unfolding Int.Pls_def number_of_eq
1372 by (simp only: of_nat_nat [symmetric] of_nat_in_Nats)
1374 lemma Ints_odd_less_0:
1375 assumes in_Ints: "a \<in> Ints"
1376 shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))"
1378 from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
1379 then obtain z where a: "a = of_int z" ..
1380 hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
1382 also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0)
1383 also have "... = (a < 0)" by (simp add: a)
1384 finally show ?thesis .
1388 subsection {* @{term setsum} and @{term setprod} *}
1390 lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
1391 apply (cases "finite A")
1392 apply (erule finite_induct, auto)
1395 lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
1396 apply (cases "finite A")
1397 apply (erule finite_induct, auto)
1400 lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
1401 apply (cases "finite A")
1402 apply (erule finite_induct, auto simp add: of_nat_mult)
1405 lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
1406 apply (cases "finite A")
1407 apply (erule finite_induct, auto)
1410 lemmas int_setsum = of_nat_setsum [where 'a=int]
1411 lemmas int_setprod = of_nat_setprod [where 'a=int]
1414 subsection{*Inequality Reasoning for the Arithmetic Simproc*}
1416 lemma add_numeral_0: "Numeral0 + a = (a::'a::number_ring)"
1419 lemma add_numeral_0_right: "a + Numeral0 = (a::'a::number_ring)"
1422 lemma mult_numeral_1: "Numeral1 * a = (a::'a::number_ring)"
1425 lemma mult_numeral_1_right: "a * Numeral1 = (a::'a::number_ring)"
1428 lemma divide_numeral_1: "a / Numeral1 = (a::'a::{number_ring,field})"
1431 lemma inverse_numeral_1:
1432 "inverse Numeral1 = (Numeral1::'a::{number_ring,field})"
1435 text{*Theorem lists for the cancellation simprocs. The use of binary numerals
1436 for 0 and 1 reduces the number of special cases.*}
1438 lemmas add_0s = add_numeral_0 add_numeral_0_right
1439 lemmas mult_1s = mult_numeral_1 mult_numeral_1_right
1440 mult_minus1 mult_minus1_right
1443 subsection{*Special Arithmetic Rules for Abstract 0 and 1*}
1445 text{*Arithmetic computations are defined for binary literals, which leaves 0
1446 and 1 as special cases. Addition already has rules for 0, but not 1.
1447 Multiplication and unary minus already have rules for both 0 and 1.*}
1450 lemma binop_eq: "[|f x y = g x y; x = x'; y = y'|] ==> f x' y' = g x' y'"
1454 lemmas add_number_of_eq = number_of_add [symmetric]
1456 text{*Allow 1 on either or both sides*}
1457 lemma one_add_one_is_two: "1 + 1 = (2::'a::number_ring)"
1458 by (simp del: numeral_1_eq_1 add: numeral_1_eq_1 [symmetric])
1460 lemmas add_special =
1462 binop_eq [of "op +", OF add_number_of_eq numeral_1_eq_1 refl, standard]
1463 binop_eq [of "op +", OF add_number_of_eq refl numeral_1_eq_1, standard]
1465 text{*Allow 1 on either or both sides (1-1 already simplifies to 0)*}
1466 lemmas diff_special =
1467 binop_eq [of "op -", OF diff_number_of_eq numeral_1_eq_1 refl, standard]
1468 binop_eq [of "op -", OF diff_number_of_eq refl numeral_1_eq_1, standard]
1470 text{*Allow 0 or 1 on either side with a binary numeral on the other*}
1472 binop_eq [of "op =", OF eq_number_of_eq numeral_0_eq_0 refl, standard]
1473 binop_eq [of "op =", OF eq_number_of_eq numeral_1_eq_1 refl, standard]
1474 binop_eq [of "op =", OF eq_number_of_eq refl numeral_0_eq_0, standard]
1475 binop_eq [of "op =", OF eq_number_of_eq refl numeral_1_eq_1, standard]
1477 text{*Allow 0 or 1 on either side with a binary numeral on the other*}
1478 lemmas less_special =
1479 binop_eq [of "op <", OF less_number_of numeral_0_eq_0 refl, standard]
1480 binop_eq [of "op <", OF less_number_of numeral_1_eq_1 refl, standard]
1481 binop_eq [of "op <", OF less_number_of refl numeral_0_eq_0, standard]
1482 binop_eq [of "op <", OF less_number_of refl numeral_1_eq_1, standard]
1484 text{*Allow 0 or 1 on either side with a binary numeral on the other*}
1486 binop_eq [of "op \<le>", OF le_number_of numeral_0_eq_0 refl, standard]
1487 binop_eq [of "op \<le>", OF le_number_of numeral_1_eq_1 refl, standard]
1488 binop_eq [of "op \<le>", OF le_number_of refl numeral_0_eq_0, standard]
1489 binop_eq [of "op \<le>", OF le_number_of refl numeral_1_eq_1, standard]
1491 lemmas arith_special[simp] =
1492 add_special diff_special eq_special less_special le_special
1495 text {* Legacy theorems *}
1497 lemmas zle_int = of_nat_le_iff [where 'a=int]
1498 lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
1500 subsection {* Setting up simplification procedures *}
1502 lemmas int_arith_rules =
1503 neg_le_iff_le numeral_0_eq_0 numeral_1_eq_1
1504 minus_zero diff_minus left_minus right_minus
1505 mult_zero_left mult_zero_right mult_Bit1 mult_1_left mult_1_right
1506 mult_minus_left mult_minus_right
1507 minus_add_distrib minus_minus mult_assoc
1508 of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
1509 of_int_0 of_int_1 of_int_add of_int_mult
1511 use "Tools/int_arith.ML"
1512 setup {* Int_Arith.global_setup *}
1513 declaration {* K Int_Arith.setup *}
1517 (fn Const (@{const_name number_of}, _) $ _ => true | _ => false)
1520 simproc_setup reorient_numeral ("number_of w = x") = Reorient_Proc.proc
1523 subsection{*Lemmas About Small Numerals*}
1525 lemma of_int_m1 [simp]: "of_int -1 = (-1 :: 'a :: number_ring)"
1527 have "(of_int -1 :: 'a) = of_int (- 1)" by simp
1528 also have "... = - of_int 1" by (simp only: of_int_minus)
1529 also have "... = -1" by simp
1530 finally show ?thesis .
1533 lemma abs_minus_one [simp]: "abs (-1) = (1::'a::{linordered_idom,number_ring})"
1534 by (simp add: abs_if)
1536 lemma abs_power_minus_one [simp]:
1537 "abs(-1 ^ n) = (1::'a::{linordered_idom,number_ring})"
1538 by (simp add: power_abs)
1540 lemma of_int_number_of_eq [simp]:
1541 "of_int (number_of v) = (number_of v :: 'a :: number_ring)"
1542 by (simp add: number_of_eq)
1544 text{*Lemmas for specialist use, NOT as default simprules*}
1545 lemma mult_2: "2 * z = (z+z::'a::number_ring)"
1546 unfolding one_add_one_is_two [symmetric] left_distrib by simp
1548 lemma mult_2_right: "z * 2 = (z+z::'a::number_ring)"
1549 by (subst mult_commute, rule mult_2)
1552 subsection{*More Inequality Reasoning*}
1554 lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
1557 lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
1560 lemma zle_diff1_eq [simp]: "(w \<le> z - (1::int)) = (w<z)"
1563 lemma zle_add1_eq_le [simp]: "(w < z + (1::int)) = (w\<le>z)"
1566 lemma int_one_le_iff_zero_less: "((1::int) \<le> z) = (0 < z)"
1570 subsection{*The functions @{term nat} and @{term int}*}
1572 text{*Simplify the terms @{term "int 0"}, @{term "int(Suc 0)"} and
1574 declare Zero_int_def [symmetric, simp]
1575 declare One_int_def [symmetric, simp]
1577 lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp]
1579 (* FIXME: duplicates nat_zero *)
1580 lemma nat_0: "nat 0 = 0"
1581 by (simp add: nat_eq_iff)
1583 lemma nat_1: "nat 1 = Suc 0"
1584 by (subst nat_eq_iff, simp)
1586 lemma nat_2: "nat 2 = Suc (Suc 0)"
1587 by (subst nat_eq_iff, simp)
1589 lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
1590 apply (insert zless_nat_conj [of 1 z])
1591 apply (auto simp add: nat_1)
1594 text{*This simplifies expressions of the form @{term "int n = z"} where
1595 z is an integer literal.*}
1596 lemmas int_eq_iff_number_of [simp] = int_eq_iff [of _ "number_of v", standard]
1598 lemma split_nat [arith_split]:
1599 "P(nat(i::int)) = ((\<forall>n. i = of_nat n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
1600 (is "?P = (?L & ?R)")
1601 proof (cases "i < 0")
1602 case True thus ?thesis by auto
1607 assume ?P thus ?L using False by clarsimp
1609 assume ?L thus ?P using False by simp
1611 with False show ?thesis by simp
1617 lemma of_int_of_nat [nitpick_simp]:
1618 "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))"
1619 proof (cases "k < 0")
1620 case True then have "0 \<le> - k" by simp
1621 then have "of_nat (nat (- k)) = of_int (- k)" by (rule of_nat_nat)
1622 with True show ?thesis by simp
1624 case False then show ?thesis by (simp add: not_less of_nat_nat)
1629 lemma nat_mult_distrib:
1632 shows "nat (z * z') = nat z * nat z'"
1633 proof (cases "0 \<le> z'")
1634 case False with assms have "z * z' \<le> 0"
1635 by (simp add: not_le mult_le_0_iff)
1636 then have "nat (z * z') = 0" by simp
1637 moreover from False have "nat z' = 0" by simp
1638 ultimately show ?thesis by simp
1640 case True with assms have ge_0: "z * z' \<ge> 0" by (simp add: zero_le_mult_iff)
1642 by (rule injD [of "of_nat :: nat \<Rightarrow> int", OF inj_of_nat])
1643 (simp only: of_nat_mult of_nat_nat [OF True]
1644 of_nat_nat [OF assms] of_nat_nat [OF ge_0], simp)
1647 lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"
1649 apply (rule_tac [2] nat_mult_distrib, auto)
1652 lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
1653 apply (cases "z=0 | w=0")
1654 apply (auto simp add: abs_if nat_mult_distrib [symmetric]
1655 nat_mult_distrib_neg [symmetric] mult_less_0_iff)
1659 subsection "Induction principles for int"
1661 text{*Well-founded segments of the integers*}
1664 int_ge_less_than :: "int => (int * int) set"
1666 "int_ge_less_than d = {(z',z). d \<le> z' & z' < z}"
1668 theorem wf_int_ge_less_than: "wf (int_ge_less_than d)"
1670 have "int_ge_less_than d \<subseteq> measure (%z. nat (z-d))"
1671 by (auto simp add: int_ge_less_than_def)
1673 by (rule wf_subset [OF wf_measure])
1676 text{*This variant looks odd, but is typical of the relations suggested
1680 int_ge_less_than2 :: "int => (int * int) set"
1682 "int_ge_less_than2 d = {(z',z). d \<le> z & z' < z}"
1684 theorem wf_int_ge_less_than2: "wf (int_ge_less_than2 d)"
1686 have "int_ge_less_than2 d \<subseteq> measure (%z. nat (1+z-d))"
1687 by (auto simp add: int_ge_less_than2_def)
1689 by (rule wf_subset [OF wf_measure])
1693 int :: "nat \<Rightarrow> int"
1695 "int \<equiv> of_nat"
1697 (* `set:int': dummy construction *)
1698 theorem int_ge_induct [case_names base step, induct set: int]:
1700 assumes ge: "k \<le> i" and
1702 step: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
1705 { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i"
1708 hence "i = k" by arith
1709 thus "P i" using base by simp
1712 then have "n = nat((i - 1) - k)" by arith
1714 have ki1: "k \<le> i - 1" using Suc.prems by arith
1716 have "P(i - 1)" by(rule Suc.hyps)
1717 from step[OF ki1 this] show ?case by simp
1720 with ge show ?thesis by fast
1723 (* `set:int': dummy construction *)
1724 theorem int_gr_induct [case_names base step, induct set: int]:
1725 assumes gr: "k < (i::int)" and
1727 step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
1729 apply(rule int_ge_induct[of "k + 1"])
1730 using gr apply arith
1732 apply (rule step, simp+)
1735 theorem int_le_induct[consumes 1,case_names base step]:
1736 assumes le: "i \<le> (k::int)" and
1738 step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
1741 { fix n have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i"
1744 hence "i = k" by arith
1745 thus "P i" using base by simp
1748 hence "n = nat(k - (i+1))" by arith
1750 have ki1: "i + 1 \<le> k" using Suc.prems by arith
1752 have "P(i+1)" by(rule Suc.hyps)
1753 from step[OF ki1 this] show ?case by simp
1756 with le show ?thesis by fast
1759 theorem int_less_induct [consumes 1,case_names base step]:
1760 assumes less: "(i::int) < k" and
1761 base: "P(k - 1)" and
1762 step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
1764 apply(rule int_le_induct[of _ "k - 1"])
1765 using less apply arith
1767 apply (rule step, simp+)
1770 subsection{*Intermediate value theorems*}
1772 lemma int_val_lemma:
1773 "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->
1774 f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
1775 unfolding One_nat_def
1776 apply (induct n, simp)
1778 apply (erule impE, simp)
1779 apply (erule_tac x = n in allE, simp)
1780 apply (case_tac "k = f (Suc n)")
1783 apply (simp add: abs_if split add: split_if_asm)
1784 apply (blast intro: le_SucI)
1787 lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
1789 lemma nat_intermed_int_val:
1790 "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;
1791 f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
1792 apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k
1794 unfolding One_nat_def
1797 apply (rule_tac x = "i+m" in exI, arith)
1801 subsection{*Products and 1, by T. M. Rasmussen*}
1803 lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))"
1806 lemma abs_zmult_eq_1:
1807 assumes mn: "\<bar>m * n\<bar> = 1"
1808 shows "\<bar>m\<bar> = (1::int)"
1810 have 0: "m \<noteq> 0 & n \<noteq> 0" using mn
1812 have "~ (2 \<le> \<bar>m\<bar>)"
1814 assume "2 \<le> \<bar>m\<bar>"
1815 hence "2*\<bar>n\<bar> \<le> \<bar>m\<bar>*\<bar>n\<bar>"
1816 by (simp add: mult_mono 0)
1817 also have "... = \<bar>m*n\<bar>"
1818 by (simp add: abs_mult)
1821 finally have "2*\<bar>n\<bar> \<le> 1" .
1822 thus "False" using 0
1825 thus ?thesis using 0
1829 lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1"
1830 by (insert abs_zmult_eq_1 [of m n], arith)
1832 lemma pos_zmult_eq_1_iff:
1833 assumes "0 < (m::int)" shows "(m * n = 1) = (m = 1 & n = 1)"
1835 from assms have "m * n = 1 ==> m = 1" by (auto dest: pos_zmult_eq_1_iff_lemma)
1836 thus ?thesis by (auto dest: pos_zmult_eq_1_iff_lemma)
1839 lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
1841 apply (frule pos_zmult_eq_1_iff_lemma)
1842 apply (simp add: mult_commute [of m])
1843 apply (frule pos_zmult_eq_1_iff_lemma, auto)
1846 lemma infinite_UNIV_int: "\<not> finite (UNIV::int set)"
1848 assume "finite (UNIV::int set)"
1849 moreover have "inj (\<lambda>i\<Colon>int. 2 * i)"
1851 ultimately have "surj (\<lambda>i\<Colon>int. 2 * i)"
1852 by (rule finite_UNIV_inj_surj)
1853 then obtain i :: int where "1 = 2 * i" by (rule surjE)
1854 then show False by (simp add: pos_zmult_eq_1_iff)
1858 subsection {* Further theorems on numerals *}
1860 subsubsection{*Special Simplification for Constants*}
1862 text{*These distributive laws move literals inside sums and differences.*}
1864 lemmas left_distrib_number_of [simp] =
1865 left_distrib [of _ _ "number_of v", standard]
1867 lemmas right_distrib_number_of [simp] =
1868 right_distrib [of "number_of v", standard]
1870 lemmas left_diff_distrib_number_of [simp] =
1871 left_diff_distrib [of _ _ "number_of v", standard]
1873 lemmas right_diff_distrib_number_of [simp] =
1874 right_diff_distrib [of "number_of v", standard]
1876 text{*These are actually for fields, like real: but where else to put them?*}
1878 lemmas zero_less_divide_iff_number_of [simp, no_atp] =
1879 zero_less_divide_iff [of "number_of w", standard]
1881 lemmas divide_less_0_iff_number_of [simp, no_atp] =
1882 divide_less_0_iff [of "number_of w", standard]
1884 lemmas zero_le_divide_iff_number_of [simp, no_atp] =
1885 zero_le_divide_iff [of "number_of w", standard]
1887 lemmas divide_le_0_iff_number_of [simp, no_atp] =
1888 divide_le_0_iff [of "number_of w", standard]
1891 text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}. It looks
1892 strange, but then other simprocs simplify the quotient.*}
1894 lemmas inverse_eq_divide_number_of [simp] =
1895 inverse_eq_divide [of "number_of w", standard]
1897 text {*These laws simplify inequalities, moving unary minus from a term
1900 lemmas less_minus_iff_number_of [simp, no_atp] =
1901 less_minus_iff [of "number_of v", standard]
1903 lemmas le_minus_iff_number_of [simp, no_atp] =
1904 le_minus_iff [of "number_of v", standard]
1906 lemmas equation_minus_iff_number_of [simp, no_atp] =
1907 equation_minus_iff [of "number_of v", standard]
1909 lemmas minus_less_iff_number_of [simp, no_atp] =
1910 minus_less_iff [of _ "number_of v", standard]
1912 lemmas minus_le_iff_number_of [simp, no_atp] =
1913 minus_le_iff [of _ "number_of v", standard]
1915 lemmas minus_equation_iff_number_of [simp, no_atp] =
1916 minus_equation_iff [of _ "number_of v", standard]
1919 text{*To Simplify Inequalities Where One Side is the Constant 1*}
1921 lemma less_minus_iff_1 [simp,no_atp]:
1922 fixes b::"'b::{linordered_idom,number_ring}"
1923 shows "(1 < - b) = (b < -1)"
1926 lemma le_minus_iff_1 [simp,no_atp]:
1927 fixes b::"'b::{linordered_idom,number_ring}"
1928 shows "(1 \<le> - b) = (b \<le> -1)"
1931 lemma equation_minus_iff_1 [simp,no_atp]:
1932 fixes b::"'b::number_ring"
1933 shows "(1 = - b) = (b = -1)"
1934 by (subst equation_minus_iff, auto)
1936 lemma minus_less_iff_1 [simp,no_atp]:
1937 fixes a::"'b::{linordered_idom,number_ring}"
1938 shows "(- a < 1) = (-1 < a)"
1941 lemma minus_le_iff_1 [simp,no_atp]:
1942 fixes a::"'b::{linordered_idom,number_ring}"
1943 shows "(- a \<le> 1) = (-1 \<le> a)"
1946 lemma minus_equation_iff_1 [simp,no_atp]:
1947 fixes a::"'b::number_ring"
1948 shows "(- a = 1) = (a = -1)"
1949 by (subst minus_equation_iff, auto)
1952 text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
1954 lemmas mult_less_cancel_left_number_of [simp, no_atp] =
1955 mult_less_cancel_left [of "number_of v", standard]
1957 lemmas mult_less_cancel_right_number_of [simp, no_atp] =
1958 mult_less_cancel_right [of _ "number_of v", standard]
1960 lemmas mult_le_cancel_left_number_of [simp, no_atp] =
1961 mult_le_cancel_left [of "number_of v", standard]
1963 lemmas mult_le_cancel_right_number_of [simp, no_atp] =
1964 mult_le_cancel_right [of _ "number_of v", standard]
1967 text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
1969 lemmas le_divide_eq_number_of1 [simp] = le_divide_eq [of _ _ "number_of w", standard]
1970 lemmas divide_le_eq_number_of1 [simp] = divide_le_eq [of _ "number_of w", standard]
1971 lemmas less_divide_eq_number_of1 [simp] = less_divide_eq [of _ _ "number_of w", standard]
1972 lemmas divide_less_eq_number_of1 [simp] = divide_less_eq [of _ "number_of w", standard]
1973 lemmas eq_divide_eq_number_of1 [simp] = eq_divide_eq [of _ _ "number_of w", standard]
1974 lemmas divide_eq_eq_number_of1 [simp] = divide_eq_eq [of _ "number_of w", standard]
1977 subsubsection{*Optional Simplification Rules Involving Constants*}
1979 text{*Simplify quotients that are compared with a literal constant.*}
1981 lemmas le_divide_eq_number_of = le_divide_eq [of "number_of w", standard]
1982 lemmas divide_le_eq_number_of = divide_le_eq [of _ _ "number_of w", standard]
1983 lemmas less_divide_eq_number_of = less_divide_eq [of "number_of w", standard]
1984 lemmas divide_less_eq_number_of = divide_less_eq [of _ _ "number_of w", standard]
1985 lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w", standard]
1986 lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w", standard]
1989 text{*Not good as automatic simprules because they cause case splits.*}
1990 lemmas divide_const_simps =
1991 le_divide_eq_number_of divide_le_eq_number_of less_divide_eq_number_of
1992 divide_less_eq_number_of eq_divide_eq_number_of divide_eq_eq_number_of
1993 le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
1995 text{*Division By @{text "-1"}*}
1997 lemma divide_minus1 [simp]:
1998 "x/-1 = -(x::'a::{field_inverse_zero, number_ring})"
2001 lemma minus1_divide [simp]:
2002 "-1 / (x::'a::{field_inverse_zero, number_ring}) = - (1/x)"
2003 by (simp add: divide_inverse)
2005 lemma half_gt_zero_iff:
2006 "(0 < r/2) = (0 < (r::'a::{linordered_field_inverse_zero,number_ring}))"
2009 lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2, standard]
2012 subsection {* The divides relation *}
2014 lemma zdvd_antisym_nonneg:
2015 "0 <= m ==> 0 <= n ==> m dvd n ==> n dvd m ==> m = (n::int)"
2016 apply (simp add: dvd_def, auto)
2017 apply (auto simp add: mult_assoc zero_le_mult_iff zmult_eq_1_iff)
2020 lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a"
2021 shows "\<bar>a\<bar> = \<bar>b\<bar>"
2023 assume "a = 0" with assms show ?thesis by simp
2025 assume "a \<noteq> 0"
2026 from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast
2027 from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast
2028 from k k' have "a = a*k*k'" by simp
2029 with mult_cancel_left1[where c="a" and b="k*k'"]
2030 have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult_assoc)
2031 hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff)
2032 thus ?thesis using k k' by auto
2035 lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
2036 apply (subgoal_tac "m = n + (m - n)")
2037 apply (erule ssubst)
2038 apply (blast intro: dvd_add, simp)
2041 lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
2043 apply (erule_tac [2] dvd_add)
2044 apply (subgoal_tac "n = (n + k * m) - k * m")
2045 apply (erule ssubst)
2046 apply (erule dvd_diff)
2050 lemma dvd_imp_le_int:
2052 assumes "i \<noteq> 0" and "d dvd i"
2053 shows "\<bar>d\<bar> \<le> \<bar>i\<bar>"
2055 from `d dvd i` obtain k where "i = d * k" ..
2056 with `i \<noteq> 0` have "k \<noteq> 0" by auto
2057 then have "1 \<le> \<bar>k\<bar>" and "0 \<le> \<bar>d\<bar>" by auto
2058 then have "\<bar>d\<bar> * 1 \<le> \<bar>d\<bar> * \<bar>k\<bar>" by (rule mult_left_mono)
2059 with `i = d * k` show ?thesis by (simp add: abs_mult)
2062 lemma zdvd_not_zless:
2064 assumes "0 < m" and "m < n"
2065 shows "\<not> n dvd m"
2067 from assms have "0 < n" by auto
2068 assume "n dvd m" then obtain k where k: "m = n * k" ..
2069 with `0 < m` have "0 < n * k" by auto
2070 with `0 < n` have "0 < k" by (simp add: zero_less_mult_iff)
2071 with k `0 < n` `m < n` have "n * k < n * 1" by simp
2072 with `0 < n` `0 < k` show False unfolding mult_less_cancel_left by auto
2075 lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)"
2078 from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast
2079 {assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp
2080 with h have False by (simp add: mult_assoc)}
2081 hence "n = m * h" by blast
2082 thus ?thesis by simp
2085 theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
2087 have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"
2090 assume A: "int y = int x * k"
2091 then show "x dvd y" proof (cases k)
2092 case (1 n) with A have "y = x * n" by (simp add: of_nat_mult [symmetric])
2093 then show ?thesis ..
2095 case (2 n) with A have "int y = int x * (- int (Suc n))" by simp
2096 also have "\<dots> = - (int x * int (Suc n))" by (simp only: mult_minus_right)
2097 also have "\<dots> = - int (x * Suc n)" by (simp only: of_nat_mult [symmetric])
2098 finally have "- int (x * Suc n) = int y" ..
2099 then show ?thesis by (simp only: negative_eq_positive) auto
2102 then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left of_nat_mult)
2105 lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
2107 assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp
2108 hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
2109 hence "nat \<bar>x\<bar> = 1" by simp
2110 thus "\<bar>x\<bar> = 1" by (cases "x < 0", auto)
2112 assume "\<bar>x\<bar>=1"
2113 then have "x = 1 \<or> x = -1" by auto
2114 then show "x dvd 1" by (auto intro: dvdI)
2117 lemma zdvd_mult_cancel1:
2118 assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
2120 assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m"
2121 by (cases "n >0", auto simp add: minus_equation_iff)
2123 assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
2124 from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
2127 lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
2128 unfolding zdvd_int by (cases "z \<ge> 0") simp_all
2130 lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
2131 unfolding zdvd_int by (cases "z \<ge> 0") simp_all
2133 lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
2134 by (auto simp add: dvd_int_iff)
2136 lemma eq_nat_nat_iff:
2137 "0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat z = nat z' \<longleftrightarrow> z = z'"
2138 by (auto elim!: nonneg_eq_int)
2141 "0 \<le> z \<Longrightarrow> nat (z ^ n) = nat z ^ n"
2142 by (induct n) (simp_all add: nat_mult_distrib)
2144 lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
2145 apply (rule_tac z=n in int_cases)
2146 apply (auto simp add: dvd_int_iff)
2147 apply (rule_tac z=z in int_cases)
2148 apply (auto simp add: dvd_imp_le)
2152 subsection {* Configuration of the code generator *}
2154 code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int"
2156 lemmas pred_succ_numeral_code [code] =
2157 pred_bin_simps succ_bin_simps
2159 lemmas plus_numeral_code [code] =
2161 arith_extra_simps(1) [where 'a = int]
2163 lemmas minus_numeral_code [code] =
2165 arith_extra_simps(2) [where 'a = int]
2166 arith_extra_simps(5) [where 'a = int]
2168 lemmas times_numeral_code [code] =
2170 arith_extra_simps(4) [where 'a = int]
2172 instantiation int :: eq
2175 definition [code del]: "eq_class.eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
2177 instance by default (simp add: eq_int_def)
2181 lemma eq_number_of_int_code [code]:
2182 "eq_class.eq (number_of k \<Colon> int) (number_of l) \<longleftrightarrow> eq_class.eq k l"
2183 unfolding eq_int_def number_of_is_id ..
2185 lemma eq_int_code [code]:
2186 "eq_class.eq Int.Pls Int.Pls \<longleftrightarrow> True"
2187 "eq_class.eq Int.Pls Int.Min \<longleftrightarrow> False"
2188 "eq_class.eq Int.Pls (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq Int.Pls k2"
2189 "eq_class.eq Int.Pls (Int.Bit1 k2) \<longleftrightarrow> False"
2190 "eq_class.eq Int.Min Int.Pls \<longleftrightarrow> False"
2191 "eq_class.eq Int.Min Int.Min \<longleftrightarrow> True"
2192 "eq_class.eq Int.Min (Int.Bit0 k2) \<longleftrightarrow> False"
2193 "eq_class.eq Int.Min (Int.Bit1 k2) \<longleftrightarrow> eq_class.eq Int.Min k2"
2194 "eq_class.eq (Int.Bit0 k1) Int.Pls \<longleftrightarrow> eq_class.eq k1 Int.Pls"
2195 "eq_class.eq (Int.Bit1 k1) Int.Pls \<longleftrightarrow> False"
2196 "eq_class.eq (Int.Bit0 k1) Int.Min \<longleftrightarrow> False"
2197 "eq_class.eq (Int.Bit1 k1) Int.Min \<longleftrightarrow> eq_class.eq k1 Int.Min"
2198 "eq_class.eq (Int.Bit0 k1) (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq k1 k2"
2199 "eq_class.eq (Int.Bit0 k1) (Int.Bit1 k2) \<longleftrightarrow> False"
2200 "eq_class.eq (Int.Bit1 k1) (Int.Bit0 k2) \<longleftrightarrow> False"
2201 "eq_class.eq (Int.Bit1 k1) (Int.Bit1 k2) \<longleftrightarrow> eq_class.eq k1 k2"
2202 unfolding eq_equals by simp_all
2204 lemma eq_int_refl [code nbe]:
2205 "eq_class.eq (k::int) k \<longleftrightarrow> True"
2206 by (rule HOL.eq_refl)
2208 lemma less_eq_number_of_int_code [code]:
2209 "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
2210 unfolding number_of_is_id ..
2212 lemma less_eq_int_code [code]:
2213 "Int.Pls \<le> Int.Pls \<longleftrightarrow> True"
2214 "Int.Pls \<le> Int.Min \<longleftrightarrow> False"
2215 "Int.Pls \<le> Int.Bit0 k \<longleftrightarrow> Int.Pls \<le> k"
2216 "Int.Pls \<le> Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
2217 "Int.Min \<le> Int.Pls \<longleftrightarrow> True"
2218 "Int.Min \<le> Int.Min \<longleftrightarrow> True"
2219 "Int.Min \<le> Int.Bit0 k \<longleftrightarrow> Int.Min < k"
2220 "Int.Min \<le> Int.Bit1 k \<longleftrightarrow> Int.Min \<le> k"
2221 "Int.Bit0 k \<le> Int.Pls \<longleftrightarrow> k \<le> Int.Pls"
2222 "Int.Bit1 k \<le> Int.Pls \<longleftrightarrow> k < Int.Pls"
2223 "Int.Bit0 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
2224 "Int.Bit1 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
2225 "Int.Bit0 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 \<le> k2"
2226 "Int.Bit0 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
2227 "Int.Bit1 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
2228 "Int.Bit1 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
2231 lemma less_number_of_int_code [code]:
2232 "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
2233 unfolding number_of_is_id ..
2235 lemma less_int_code [code]:
2236 "Int.Pls < Int.Pls \<longleftrightarrow> False"
2237 "Int.Pls < Int.Min \<longleftrightarrow> False"
2238 "Int.Pls < Int.Bit0 k \<longleftrightarrow> Int.Pls < k"
2239 "Int.Pls < Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
2240 "Int.Min < Int.Pls \<longleftrightarrow> True"
2241 "Int.Min < Int.Min \<longleftrightarrow> False"
2242 "Int.Min < Int.Bit0 k \<longleftrightarrow> Int.Min < k"
2243 "Int.Min < Int.Bit1 k \<longleftrightarrow> Int.Min < k"
2244 "Int.Bit0 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
2245 "Int.Bit1 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
2246 "Int.Bit0 k < Int.Min \<longleftrightarrow> k \<le> Int.Min"
2247 "Int.Bit1 k < Int.Min \<longleftrightarrow> k < Int.Min"
2248 "Int.Bit0 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
2249 "Int.Bit0 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
2250 "Int.Bit1 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
2251 "Int.Bit1 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 < k2"
2255 nat_aux :: "int \<Rightarrow> nat \<Rightarrow> nat" where
2256 "nat_aux i n = nat i + n"
2259 "nat_aux i n = (if i \<le> 0 then n else nat_aux (i - 1) (Suc n))" -- {* tail recursive *}
2260 by (auto simp add: nat_aux_def nat_eq_iff linorder_not_le order_less_imp_le
2261 dest: zless_imp_add1_zle)
2263 lemma [code]: "nat i = nat_aux i 0"
2264 by (simp add: nat_aux_def)
2266 hide_const (open) nat_aux
2268 lemma zero_is_num_zero [code, code_unfold_post]:
2269 "(0\<Colon>int) = Numeral0"
2272 lemma one_is_num_one [code, code_unfold_post]:
2273 "(1\<Colon>int) = Numeral1"
2279 code_modulename OCaml
2282 code_modulename Haskell
2288 val term_of_int = HOLogic.mk_number HOLogic.intT;
2292 let val j = one_of [~1, 1] * random_range 0 i
2293 in (j, fn () => term_of_int j) end;
2299 fun strip_number_of (@{term "Int.number_of :: int => int"} $ t) = t
2300 | strip_number_of t = t;
2302 fun numeral_codegen thy defs dep module b t gr =
2303 let val i = HOLogic.dest_numeral (strip_number_of t)
2305 SOME (Codegen.str (string_of_int i),
2306 snd (Codegen.invoke_tycodegen thy defs dep module false HOLogic.intT gr))
2307 end handle TERM _ => NONE;
2311 Codegen.add_codegen "numeral_codegen" numeral_codegen
2317 "number_of :: int \<Rightarrow> int" ("(_)")
2320 "uminus :: int => int" ("~")
2321 "op + :: int => int => int" ("(_ +/ _)")
2322 "op * :: int => int => int" ("(_ */ _)")
2323 "op \<le> :: int => int => bool" ("(_ <=/ _)")
2324 "op < :: int => int => bool" ("(_ </ _)")
2326 quickcheck_params [default_type = int]
2328 hide_const (open) Pls Min Bit0 Bit1 succ pred
2331 subsection {* Legacy theorems *}
2333 lemmas zminus_zminus = minus_minus [of "z::int", standard]
2334 lemmas zminus_0 = minus_zero [where 'a=int]
2335 lemmas zminus_zadd_distrib = minus_add_distrib [of "z::int" "w", standard]
2336 lemmas zadd_commute = add_commute [of "z::int" "w", standard]
2337 lemmas zadd_assoc = add_assoc [of "z1::int" "z2" "z3", standard]
2338 lemmas zadd_left_commute = add_left_commute [of "x::int" "y" "z", standard]
2339 lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute
2340 lemmas zmult_ac = mult_ac
2341 lemmas zadd_0 = add_0_left [of "z::int", standard]
2342 lemmas zadd_0_right = add_0_right [of "z::int", standard]
2343 lemmas zadd_zminus_inverse2 = left_minus [of "z::int", standard]
2344 lemmas zmult_zminus = mult_minus_left [of "z::int" "w", standard]
2345 lemmas zmult_commute = mult_commute [of "z::int" "w", standard]
2346 lemmas zmult_assoc = mult_assoc [of "z1::int" "z2" "z3", standard]
2347 lemmas zadd_zmult_distrib = left_distrib [of "z1::int" "z2" "w", standard]
2348 lemmas zadd_zmult_distrib2 = right_distrib [of "w::int" "z1" "z2", standard]
2349 lemmas zdiff_zmult_distrib = left_diff_distrib [of "z1::int" "z2" "w", standard]
2350 lemmas zdiff_zmult_distrib2 = right_diff_distrib [of "w::int" "z1" "z2", standard]
2352 lemmas zmult_1 = mult_1_left [of "z::int", standard]
2353 lemmas zmult_1_right = mult_1_right [of "z::int", standard]
2355 lemmas zle_refl = order_refl [of "w::int", standard]
2356 lemmas zle_trans = order_trans [where 'a=int and x="i" and y="j" and z="k", standard]
2357 lemmas zle_antisym = order_antisym [of "z::int" "w", standard]
2358 lemmas zle_linear = linorder_linear [of "z::int" "w", standard]
2359 lemmas zless_linear = linorder_less_linear [where 'a = int]
2361 lemmas zadd_left_mono = add_left_mono [of "i::int" "j" "k", standard]
2362 lemmas zadd_strict_right_mono = add_strict_right_mono [of "i::int" "j" "k", standard]
2363 lemmas zadd_zless_mono = add_less_le_mono [of "w'::int" "w" "z'" "z", standard]
2365 lemmas int_0_less_1 = zero_less_one [where 'a=int]
2366 lemmas int_0_neq_1 = zero_neq_one [where 'a=int]
2368 lemmas inj_int = inj_of_nat [where 'a=int]
2369 lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
2370 lemmas int_mult = of_nat_mult [where 'a=int]
2371 lemmas zmult_int = of_nat_mult [where 'a=int, symmetric]
2372 lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="n", standard]
2373 lemmas zless_int = of_nat_less_iff [where 'a=int]
2374 lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="k", standard]
2375 lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int]
2376 lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
2377 lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="n", standard]
2378 lemmas int_0 = of_nat_0 [where 'a=int]
2379 lemmas int_1 = of_nat_1 [where 'a=int]
2380 lemmas int_Suc = of_nat_Suc [where 'a=int]
2381 lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m", standard]
2382 lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
2383 lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
2384 lemmas zless_le = less_int_def
2385 lemmas int_eq_of_nat = TrueI
2387 lemma zpower_zadd_distrib:
2388 "x ^ (y + z) = ((x ^ y) * (x ^ z)::int)"
2391 lemma zero_less_zpower_abs_iff:
2392 "(0 < abs x ^ n) \<longleftrightarrow> (x \<noteq> (0::int) | n = 0)"
2393 by (rule zero_less_power_abs_iff)
2395 lemma zero_le_zpower_abs: "(0::int) \<le> abs x ^ n"
2396 by (rule zero_le_power_abs)
2398 lemma zpower_zpower:
2399 "(x ^ y) ^ z = (x ^ (y * z)::int)"
2400 by (rule power_mult [symmetric])
2403 "int (m ^ n) = int m ^ n"
2404 by (rule of_nat_power)
2406 lemmas zpower_int = int_power [symmetric]