src/HOL/Int.thy
 author webertj Fri Oct 19 15:12:52 2012 +0200 (2012-10-19) changeset 49962 a8cc904a6820 parent 48891 c0eafbd55de3 child 51112 da97167e03f7 permissions -rw-r--r--
Renamed {left,right}_distrib to distrib_{right,left}.
1 (*  Title:      HOL/Int.thy
2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3     Author:     Tobias Nipkow, Florian Haftmann, TU Muenchen
4 *)
6 header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *}
8 theory Int
9 imports Equiv_Relations Wellfounded Quotient
10 begin
12 subsection {* Definition of integers as a quotient type *}
14 definition intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" where
15   "intrel = (\<lambda>(x, y) (u, v). x + v = u + y)"
17 lemma intrel_iff [simp]: "intrel (x, y) (u, v) \<longleftrightarrow> x + v = u + y"
18   by (simp add: intrel_def)
20 quotient_type int = "nat \<times> nat" / "intrel"
21   morphisms Rep_Integ Abs_Integ
22 proof (rule equivpI)
23   show "reflp intrel"
24     unfolding reflp_def by auto
25   show "symp intrel"
26     unfolding symp_def by auto
27   show "transp intrel"
28     unfolding transp_def by auto
29 qed
31 lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]:
32      "(!!x y. z = Abs_Integ (x, y) ==> P) ==> P"
33 by (induct z) auto
35 subsection {* Integers form a commutative ring *}
37 instantiation int :: comm_ring_1
38 begin
40 lift_definition zero_int :: "int" is "(0, 0)"
41   by simp
43 lift_definition one_int :: "int" is "(1, 0)"
44   by simp
46 lift_definition plus_int :: "int \<Rightarrow> int \<Rightarrow> int"
47   is "\<lambda>(x, y) (u, v). (x + u, y + v)"
48   by clarsimp
50 lift_definition uminus_int :: "int \<Rightarrow> int"
51   is "\<lambda>(x, y). (y, x)"
52   by clarsimp
54 lift_definition minus_int :: "int \<Rightarrow> int \<Rightarrow> int"
55   is "\<lambda>(x, y) (u, v). (x + v, y + u)"
56   by clarsimp
58 lift_definition times_int :: "int \<Rightarrow> int \<Rightarrow> int"
59   is "\<lambda>(x, y) (u, v). (x*u + y*v, x*v + y*u)"
60 proof (clarsimp)
61   fix s t u v w x y z :: nat
62   assume "s + v = u + t" and "w + z = y + x"
63   hence "(s + v) * w + (u + t) * x + u * (w + z) + v * (y + x)
64        = (u + t) * w + (s + v) * x + u * (y + x) + v * (w + z)"
65     by simp
66   thus "(s * w + t * x) + (u * z + v * y) = (u * y + v * z) + (s * x + t * w)"
67     by (simp add: algebra_simps)
68 qed
70 instance
71   by default (transfer, clarsimp simp: algebra_simps)+
73 end
75 abbreviation int :: "nat \<Rightarrow> int" where
76   "int \<equiv> of_nat"
78 lemma int_def: "int n = Abs_Integ (n, 0)"
79   by (induct n, simp add: zero_int.abs_eq,
80     simp add: one_int.abs_eq plus_int.abs_eq)
82 lemma int_transfer [transfer_rule]:
83   "(fun_rel (op =) cr_int) (\<lambda>n. (n, 0)) int"
84   unfolding fun_rel_def cr_int_def int_def by simp
86 lemma int_diff_cases:
87   obtains (diff) m n where "z = int m - int n"
88   by transfer clarsimp
90 subsection {* Integers are totally ordered *}
92 instantiation int :: linorder
93 begin
95 lift_definition less_eq_int :: "int \<Rightarrow> int \<Rightarrow> bool"
96   is "\<lambda>(x, y) (u, v). x + v \<le> u + y"
97   by auto
99 lift_definition less_int :: "int \<Rightarrow> int \<Rightarrow> bool"
100   is "\<lambda>(x, y) (u, v). x + v < u + y"
101   by auto
103 instance
104   by default (transfer, force)+
106 end
108 instantiation int :: distrib_lattice
109 begin
111 definition
112   "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
114 definition
115   "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
117 instance
118   by intro_classes
119     (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
121 end
123 subsection {* Ordering properties of arithmetic operations *}
125 instance int :: ordered_cancel_ab_semigroup_add
126 proof
127   fix i j k :: int
128   show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
129     by transfer clarsimp
130 qed
132 text{*Strict Monotonicity of Multiplication*}
134 text{*strict, in 1st argument; proof is by induction on k>0*}
135 lemma zmult_zless_mono2_lemma:
136      "(i::int)<j ==> 0<k ==> int k * i < int k * j"
137 apply (induct k)
138 apply simp
139 apply (simp add: distrib_right)
140 apply (case_tac "k=0")
142 done
144 lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = int n"
145 apply transfer
146 apply clarsimp
147 apply (rule_tac x="a - b" in exI, simp)
148 done
150 lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = int n"
151 apply transfer
152 apply clarsimp
153 apply (rule_tac x="a - b" in exI, simp)
154 done
156 lemma zmult_zless_mono2: "[| i<j;  (0::int) < k |] ==> k*i < k*j"
157 apply (drule zero_less_imp_eq_int)
158 apply (auto simp add: zmult_zless_mono2_lemma)
159 done
161 text{*The integers form an ordered integral domain*}
162 instantiation int :: linordered_idom
163 begin
165 definition
166   zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
168 definition
169   zsgn_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
171 instance proof
172   fix i j k :: int
173   show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
174     by (rule zmult_zless_mono2)
175   show "\<bar>i\<bar> = (if i < 0 then -i else i)"
176     by (simp only: zabs_def)
177   show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
178     by (simp only: zsgn_def)
179 qed
181 end
183 lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + (1\<Colon>int) \<le> z"
184   by transfer clarsimp
187   "(w \<Colon> int) < z \<longleftrightarrow> (\<exists>n. z = w + int (Suc n))"
188 apply transfer
189 apply auto
190 apply (rename_tac a b c d)
191 apply (rule_tac x="c+b - Suc(a+d)" in exI)
192 apply arith
193 done
195 lemmas int_distrib =
196   distrib_right [of z1 z2 w]
197   distrib_left [of w z1 z2]
198   left_diff_distrib [of z1 z2 w]
199   right_diff_distrib [of w z1 z2]
200   for z1 z2 w :: int
203 subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}
205 context ring_1
206 begin
208 lift_definition of_int :: "int \<Rightarrow> 'a" is "\<lambda>(i, j). of_nat i - of_nat j"
209   by (clarsimp simp add: diff_eq_eq eq_diff_eq diff_add_eq
212 lemma of_int_0 [simp]: "of_int 0 = 0"
213   by transfer simp
215 lemma of_int_1 [simp]: "of_int 1 = 1"
216   by transfer simp
218 lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z"
219   by transfer (clarsimp simp add: algebra_simps)
221 lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)"
222   by (transfer fixing: uminus) clarsimp
224 lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z"
225 by (simp add: diff_minus Groups.diff_minus)
227 lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
228   by (transfer fixing: times) (clarsimp simp add: algebra_simps of_nat_mult)
230 text{*Collapse nested embeddings*}
231 lemma of_int_of_nat_eq [simp]: "of_int (int n) = of_nat n"
232 by (induct n) auto
234 lemma of_int_numeral [simp, code_post]: "of_int (numeral k) = numeral k"
235   by (simp add: of_nat_numeral [symmetric] of_int_of_nat_eq [symmetric])
237 lemma of_int_neg_numeral [simp, code_post]: "of_int (neg_numeral k) = neg_numeral k"
238   unfolding neg_numeral_def neg_numeral_class.neg_numeral_def
239   by (simp only: of_int_minus of_int_numeral)
241 lemma of_int_power:
242   "of_int (z ^ n) = of_int z ^ n"
243   by (induct n) simp_all
245 end
247 context ring_char_0
248 begin
250 lemma of_int_eq_iff [simp]:
251    "of_int w = of_int z \<longleftrightarrow> w = z"
252   by transfer (clarsimp simp add: algebra_simps
255 text{*Special cases where either operand is zero*}
256 lemma of_int_eq_0_iff [simp]:
257   "of_int z = 0 \<longleftrightarrow> z = 0"
258   using of_int_eq_iff [of z 0] by simp
260 lemma of_int_0_eq_iff [simp]:
261   "0 = of_int z \<longleftrightarrow> z = 0"
262   using of_int_eq_iff [of 0 z] by simp
264 end
266 context linordered_idom
267 begin
269 text{*Every @{text linordered_idom} has characteristic zero.*}
270 subclass ring_char_0 ..
272 lemma of_int_le_iff [simp]:
273   "of_int w \<le> of_int z \<longleftrightarrow> w \<le> z"
274   by (transfer fixing: less_eq) (clarsimp simp add: algebra_simps
277 lemma of_int_less_iff [simp]:
278   "of_int w < of_int z \<longleftrightarrow> w < z"
279   by (simp add: less_le order_less_le)
281 lemma of_int_0_le_iff [simp]:
282   "0 \<le> of_int z \<longleftrightarrow> 0 \<le> z"
283   using of_int_le_iff [of 0 z] by simp
285 lemma of_int_le_0_iff [simp]:
286   "of_int z \<le> 0 \<longleftrightarrow> z \<le> 0"
287   using of_int_le_iff [of z 0] by simp
289 lemma of_int_0_less_iff [simp]:
290   "0 < of_int z \<longleftrightarrow> 0 < z"
291   using of_int_less_iff [of 0 z] by simp
293 lemma of_int_less_0_iff [simp]:
294   "of_int z < 0 \<longleftrightarrow> z < 0"
295   using of_int_less_iff [of z 0] by simp
297 end
299 lemma of_int_eq_id [simp]: "of_int = id"
300 proof
301   fix z show "of_int z = id z"
302     by (cases z rule: int_diff_cases, simp)
303 qed
306 subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *}
308 lift_definition nat :: "int \<Rightarrow> nat" is "\<lambda>(x, y). x - y"
309   by auto
311 lemma nat_int [simp]: "nat (int n) = n"
312   by transfer simp
314 lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
315   by transfer clarsimp
317 corollary nat_0_le: "0 \<le> z ==> int (nat z) = z"
318 by simp
320 lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
321   by transfer clarsimp
323 lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"
324   by transfer (clarsimp, arith)
326 text{*An alternative condition is @{term "0 \<le> w"} *}
327 corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
328 by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
330 corollary nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"
331 by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
333 lemma zless_nat_conj [simp]: "(nat w < nat z) = (0 < z & w < z)"
334   by transfer (clarsimp, arith)
336 lemma nonneg_eq_int:
337   fixes z :: int
338   assumes "0 \<le> z" and "\<And>m. z = int m \<Longrightarrow> P"
339   shows P
340   using assms by (blast dest: nat_0_le sym)
342 lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)"
343   by transfer (clarsimp simp add: le_imp_diff_is_add)
345 corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)"
346 by (simp only: eq_commute [of m] nat_eq_iff)
348 lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)"
349   by transfer (clarsimp, arith)
351 lemma nat_le_iff: "nat x \<le> n \<longleftrightarrow> x \<le> int n"
352   by transfer (clarsimp simp add: le_diff_conv)
354 lemma nat_mono: "x \<le> y \<Longrightarrow> nat x \<le> nat y"
355   by transfer auto
357 lemma nat_0_iff[simp]: "nat(i::int) = 0 \<longleftrightarrow> i\<le>0"
358   by transfer clarsimp
360 lemma int_eq_iff: "(of_nat m = z) = (m = nat z & 0 \<le> z)"
361 by (auto simp add: nat_eq_iff2)
363 lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)"
364 by (insert zless_nat_conj [of 0], auto)
367      "[| (0::int) \<le> z;  0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"
368   by transfer clarsimp
370 lemma nat_diff_distrib:
371      "[| (0::int) \<le> z';  z' \<le> z |] ==> nat (z-z') = nat z - nat z'"
372   by transfer clarsimp
374 lemma nat_zminus_int [simp]: "nat (- int n) = 0"
375   by transfer simp
377 lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
378   by transfer (clarsimp simp add: less_diff_conv)
380 context ring_1
381 begin
383 lemma of_nat_nat: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z"
384   by transfer (clarsimp simp add: of_nat_diff)
386 end
388 text {* For termination proofs: *}
389 lemma measure_function_int[measure_function]: "is_measure (nat o abs)" ..
392 subsection{*Lemmas about the Function @{term of_nat} and Orderings*}
394 lemma negative_zless_0: "- (int (Suc n)) < (0 \<Colon> int)"
395 by (simp add: order_less_le del: of_nat_Suc)
397 lemma negative_zless [iff]: "- (int (Suc n)) < int m"
398 by (rule negative_zless_0 [THEN order_less_le_trans], simp)
400 lemma negative_zle_0: "- int n \<le> 0"
401 by (simp add: minus_le_iff)
403 lemma negative_zle [iff]: "- int n \<le> int m"
404 by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff])
406 lemma not_zle_0_negative [simp]: "~ (0 \<le> - (int (Suc n)))"
407 by (subst le_minus_iff, simp del: of_nat_Suc)
409 lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
410   by transfer simp
412 lemma not_int_zless_negative [simp]: "~ (int n < - int m)"
413 by (simp add: linorder_not_less)
415 lemma negative_eq_positive [simp]: "(- int n = of_nat m) = (n = 0 & m = 0)"
416 by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg)
418 lemma zle_iff_zadd: "w \<le> z \<longleftrightarrow> (\<exists>n. z = w + int n)"
419 proof -
420   have "(w \<le> z) = (0 \<le> z - w)"
421     by (simp only: le_diff_eq add_0_left)
422   also have "\<dots> = (\<exists>n. z - w = of_nat n)"
423     by (auto elim: zero_le_imp_eq_int)
424   also have "\<dots> = (\<exists>n. z = w + of_nat n)"
425     by (simp only: algebra_simps)
426   finally show ?thesis .
427 qed
429 lemma zadd_int_left: "int m + (int n + z) = int (m + n) + z"
430 by simp
432 lemma int_Suc0_eq_1: "int (Suc 0) = 1"
433 by simp
435 text{*This version is proved for all ordered rings, not just integers!
436       It is proved here because attribute @{text arith_split} is not available
437       in theory @{text Rings}.
438       But is it really better than just rewriting with @{text abs_if}?*}
439 lemma abs_split [arith_split,no_atp]:
440      "P(abs(a::'a::linordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
441 by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
443 lemma negD: "x < 0 \<Longrightarrow> \<exists>n. x = - (int (Suc n))"
444 apply transfer
445 apply clarsimp
446 apply (rule_tac x="b - Suc a" in exI, arith)
447 done
450 subsection {* Cases and induction *}
452 text{*Now we replace the case analysis rule by a more conventional one:
453 whether an integer is negative or not.*}
455 theorem int_cases [case_names nonneg neg, cases type: int]:
456   "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
457 apply (cases "z < 0")
458 apply (blast dest!: negD)
459 apply (simp add: linorder_not_less del: of_nat_Suc)
460 apply auto
461 apply (blast dest: nat_0_le [THEN sym])
462 done
464 theorem int_of_nat_induct [case_names nonneg neg, induct type: int]:
465      "[|!! n. P (int n);  !!n. P (- (int (Suc n))) |] ==> P z"
466   by (cases z) auto
468 lemma nonneg_int_cases:
469   assumes "0 \<le> k" obtains n where "k = int n"
470   using assms by (cases k, simp, simp del: of_nat_Suc)
472 lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
473   -- {* Unfold all @{text let}s involving constants *}
474   unfolding Let_def ..
476 lemma Let_neg_numeral [simp]: "Let (neg_numeral v) f = f (neg_numeral v)"
477   -- {* Unfold all @{text let}s involving constants *}
478   unfolding Let_def ..
480 text {* Unfold @{text min} and @{text max} on numerals. *}
482 lemmas max_number_of [simp] =
483   max_def [of "numeral u" "numeral v"]
484   max_def [of "numeral u" "neg_numeral v"]
485   max_def [of "neg_numeral u" "numeral v"]
486   max_def [of "neg_numeral u" "neg_numeral v"] for u v
488 lemmas min_number_of [simp] =
489   min_def [of "numeral u" "numeral v"]
490   min_def [of "numeral u" "neg_numeral v"]
491   min_def [of "neg_numeral u" "numeral v"]
492   min_def [of "neg_numeral u" "neg_numeral v"] for u v
495 subsubsection {* Binary comparisons *}
497 text {* Preliminaries *}
499 lemma even_less_0_iff:
500   "a + a < 0 \<longleftrightarrow> a < (0::'a::linordered_idom)"
501 proof -
502   have "a + a < 0 \<longleftrightarrow> (1+1)*a < 0" by (simp add: distrib_right del: one_add_one)
503   also have "(1+1)*a < 0 \<longleftrightarrow> a < 0"
504     by (simp add: mult_less_0_iff zero_less_two
505                   order_less_not_sym [OF zero_less_two])
506   finally show ?thesis .
507 qed
509 lemma le_imp_0_less:
510   assumes le: "0 \<le> z"
511   shows "(0::int) < 1 + z"
512 proof -
513   have "0 \<le> z" by fact
514   also have "... < z + 1" by (rule less_add_one)
515   also have "... = 1 + z" by (simp add: add_ac)
516   finally show "0 < 1 + z" .
517 qed
519 lemma odd_less_0_iff:
520   "(1 + z + z < 0) = (z < (0::int))"
521 proof (cases z)
522   case (nonneg n)
524                              le_imp_0_less [THEN order_less_imp_le])
525 next
526   case (neg n)
527   thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1
528     add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric])
529 qed
531 subsubsection {* Comparisons, for Ordered Rings *}
533 lemmas double_eq_0_iff = double_zero
535 lemma odd_nonzero:
536   "1 + z + z \<noteq> (0::int)"
537 proof (cases z)
538   case (nonneg n)
539   have le: "0 \<le> z+z" by (simp add: nonneg add_increasing)
540   thus ?thesis using  le_imp_0_less [OF le]
542 next
543   case (neg n)
544   show ?thesis
545   proof
546     assume eq: "1 + z + z = 0"
547     have "(0::int) < 1 + (int n + int n)"
549     also have "... = - (1 + z + z)"
550       by (simp add: neg add_assoc [symmetric])
551     also have "... = 0" by (simp add: eq)
552     finally have "0<0" ..
553     thus False by blast
554   qed
555 qed
558 subsection {* The Set of Integers *}
560 context ring_1
561 begin
563 definition Ints  :: "'a set" where
564   "Ints = range of_int"
566 notation (xsymbols)
567   Ints  ("\<int>")
569 lemma Ints_of_int [simp]: "of_int z \<in> \<int>"
570   by (simp add: Ints_def)
572 lemma Ints_of_nat [simp]: "of_nat n \<in> \<int>"
573   using Ints_of_int [of "of_nat n"] by simp
575 lemma Ints_0 [simp]: "0 \<in> \<int>"
576   using Ints_of_int [of "0"] by simp
578 lemma Ints_1 [simp]: "1 \<in> \<int>"
579   using Ints_of_int [of "1"] by simp
581 lemma Ints_add [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a + b \<in> \<int>"
582 apply (auto simp add: Ints_def)
583 apply (rule range_eqI)
584 apply (rule of_int_add [symmetric])
585 done
587 lemma Ints_minus [simp]: "a \<in> \<int> \<Longrightarrow> -a \<in> \<int>"
588 apply (auto simp add: Ints_def)
589 apply (rule range_eqI)
590 apply (rule of_int_minus [symmetric])
591 done
593 lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a - b \<in> \<int>"
594 apply (auto simp add: Ints_def)
595 apply (rule range_eqI)
596 apply (rule of_int_diff [symmetric])
597 done
599 lemma Ints_mult [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a * b \<in> \<int>"
600 apply (auto simp add: Ints_def)
601 apply (rule range_eqI)
602 apply (rule of_int_mult [symmetric])
603 done
605 lemma Ints_power [simp]: "a \<in> \<int> \<Longrightarrow> a ^ n \<in> \<int>"
606 by (induct n) simp_all
608 lemma Ints_cases [cases set: Ints]:
609   assumes "q \<in> \<int>"
610   obtains (of_int) z where "q = of_int z"
611   unfolding Ints_def
612 proof -
613   from `q \<in> \<int>` have "q \<in> range of_int" unfolding Ints_def .
614   then obtain z where "q = of_int z" ..
615   then show thesis ..
616 qed
618 lemma Ints_induct [case_names of_int, induct set: Ints]:
619   "q \<in> \<int> \<Longrightarrow> (\<And>z. P (of_int z)) \<Longrightarrow> P q"
620   by (rule Ints_cases) auto
622 end
624 text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
626 lemma Ints_double_eq_0_iff:
627   assumes in_Ints: "a \<in> Ints"
628   shows "(a + a = 0) = (a = (0::'a::ring_char_0))"
629 proof -
630   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
631   then obtain z where a: "a = of_int z" ..
632   show ?thesis
633   proof
634     assume "a = 0"
635     thus "a + a = 0" by simp
636   next
637     assume eq: "a + a = 0"
638     hence "of_int (z + z) = (of_int 0 :: 'a)" by (simp add: a)
639     hence "z + z = 0" by (simp only: of_int_eq_iff)
640     hence "z = 0" by (simp only: double_eq_0_iff)
641     thus "a = 0" by (simp add: a)
642   qed
643 qed
645 lemma Ints_odd_nonzero:
646   assumes in_Ints: "a \<in> Ints"
647   shows "1 + a + a \<noteq> (0::'a::ring_char_0)"
648 proof -
649   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
650   then obtain z where a: "a = of_int z" ..
651   show ?thesis
652   proof
653     assume eq: "1 + a + a = 0"
654     hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
655     hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
656     with odd_nonzero show False by blast
657   qed
658 qed
660 lemma Nats_numeral [simp]: "numeral w \<in> Nats"
661   using of_nat_in_Nats [of "numeral w"] by simp
663 lemma Ints_odd_less_0:
664   assumes in_Ints: "a \<in> Ints"
665   shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))"
666 proof -
667   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
668   then obtain z where a: "a = of_int z" ..
669   hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
670     by (simp add: a)
671   also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0_iff)
672   also have "... = (a < 0)" by (simp add: a)
673   finally show ?thesis .
674 qed
677 subsection {* @{term setsum} and @{term setprod} *}
679 lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
680   apply (cases "finite A")
681   apply (erule finite_induct, auto)
682   done
684 lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
685   apply (cases "finite A")
686   apply (erule finite_induct, auto)
687   done
689 lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
690   apply (cases "finite A")
691   apply (erule finite_induct, auto simp add: of_nat_mult)
692   done
694 lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
695   apply (cases "finite A")
696   apply (erule finite_induct, auto)
697   done
699 lemmas int_setsum = of_nat_setsum [where 'a=int]
700 lemmas int_setprod = of_nat_setprod [where 'a=int]
703 text {* Legacy theorems *}
705 lemmas zle_int = of_nat_le_iff [where 'a=int]
706 lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
707 lemmas numeral_1_eq_1 = numeral_One
709 subsection {* Setting up simplification procedures *}
711 lemmas int_arith_rules =
712   neg_le_iff_le numeral_One
713   minus_zero diff_minus left_minus right_minus
714   mult_zero_left mult_zero_right mult_1_left mult_1_right
715   mult_minus_left mult_minus_right
716   minus_add_distrib minus_minus mult_assoc
717   of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
718   of_int_0 of_int_1 of_int_add of_int_mult
720 ML_file "Tools/int_arith.ML"
721 declaration {* K Int_Arith.setup *}
723 simproc_setup fast_arith ("(m::'a::linordered_idom) < n" |
724   "(m::'a::linordered_idom) <= n" |
725   "(m::'a::linordered_idom) = n") =
726   {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *}
729 subsection{*Lemmas About Small Numerals*}
731 lemma abs_power_minus_one [simp]:
732   "abs(-1 ^ n) = (1::'a::linordered_idom)"
733 by (simp add: power_abs)
736 subsection{*More Inequality Reasoning*}
738 lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
739 by arith
741 lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
742 by arith
744 lemma zle_diff1_eq [simp]: "(w \<le> z - (1::int)) = (w<z)"
745 by arith
747 lemma zle_add1_eq_le [simp]: "(w < z + (1::int)) = (w\<le>z)"
748 by arith
750 lemma int_one_le_iff_zero_less: "((1::int) \<le> z) = (0 < z)"
751 by arith
754 subsection{*The functions @{term nat} and @{term int}*}
756 text{*Simplify the term @{term "w + - z"}*}
757 lemmas diff_int_def_symmetric = diff_def [where 'a=int, symmetric, simp]
759 lemma nat_0 [simp]: "nat 0 = 0"
760 by (simp add: nat_eq_iff)
762 lemma nat_1 [simp]: "nat 1 = Suc 0"
763 by (subst nat_eq_iff, simp)
765 lemma nat_2: "nat 2 = Suc (Suc 0)"
766 by (subst nat_eq_iff, simp)
768 lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
769 apply (insert zless_nat_conj [of 1 z])
770 apply auto
771 done
773 text{*This simplifies expressions of the form @{term "int n = z"} where
774       z is an integer literal.*}
775 lemmas int_eq_iff_numeral [simp] = int_eq_iff [of _ "numeral v"] for v
777 lemma split_nat [arith_split]:
778   "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
779   (is "?P = (?L & ?R)")
780 proof (cases "i < 0")
781   case True thus ?thesis by auto
782 next
783   case False
784   have "?P = ?L"
785   proof
786     assume ?P thus ?L using False by clarsimp
787   next
788     assume ?L thus ?P using False by simp
789   qed
790   with False show ?thesis by simp
791 qed
793 context ring_1
794 begin
796 lemma of_int_of_nat [nitpick_simp]:
797   "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))"
798 proof (cases "k < 0")
799   case True then have "0 \<le> - k" by simp
800   then have "of_nat (nat (- k)) = of_int (- k)" by (rule of_nat_nat)
801   with True show ?thesis by simp
802 next
803   case False then show ?thesis by (simp add: not_less of_nat_nat)
804 qed
806 end
808 lemma nat_mult_distrib:
809   fixes z z' :: int
810   assumes "0 \<le> z"
811   shows "nat (z * z') = nat z * nat z'"
812 proof (cases "0 \<le> z'")
813   case False with assms have "z * z' \<le> 0"
814     by (simp add: not_le mult_le_0_iff)
815   then have "nat (z * z') = 0" by simp
816   moreover from False have "nat z' = 0" by simp
817   ultimately show ?thesis by simp
818 next
819   case True with assms have ge_0: "z * z' \<ge> 0" by (simp add: zero_le_mult_iff)
820   show ?thesis
821     by (rule injD [of "of_nat :: nat \<Rightarrow> int", OF inj_of_nat])
822       (simp only: of_nat_mult of_nat_nat [OF True]
823          of_nat_nat [OF assms] of_nat_nat [OF ge_0], simp)
824 qed
826 lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"
827 apply (rule trans)
828 apply (rule_tac  nat_mult_distrib, auto)
829 done
831 lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
832 apply (cases "z=0 | w=0")
833 apply (auto simp add: abs_if nat_mult_distrib [symmetric]
834                       nat_mult_distrib_neg [symmetric] mult_less_0_iff)
835 done
837 lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
838 apply (rule sym)
839 apply (simp add: nat_eq_iff)
840 done
842 lemma diff_nat_eq_if:
843      "nat z - nat z' =
844         (if z' < 0 then nat z
845          else let d = z-z' in
846               if d < 0 then 0 else nat d)"
847 by (simp add: Let_def nat_diff_distrib [symmetric])
849 (* nat_diff_distrib has too-strong premises *)
850 lemma nat_diff_distrib': "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x - y) = nat x - nat y"
851 apply (rule int_int_eq [THEN iffD1], clarsimp)
852 apply (subst of_nat_diff)
853 apply (rule nat_mono, simp_all)
854 done
856 lemma nat_numeral [simp, code_abbrev]:
857   "nat (numeral k) = numeral k"
858   by (simp add: nat_eq_iff)
860 lemma nat_neg_numeral [simp]:
861   "nat (neg_numeral k) = 0"
862   by simp
864 lemma diff_nat_numeral [simp]:
865   "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
866   by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
868 lemma nat_numeral_diff_1 [simp]:
869   "numeral v - (1::nat) = nat (numeral v - 1)"
870   using diff_nat_numeral [of v Num.One] by simp
872 lemmas nat_arith = diff_nat_numeral
875 subsection "Induction principles for int"
877 text{*Well-founded segments of the integers*}
879 definition
880   int_ge_less_than  ::  "int => (int * int) set"
881 where
882   "int_ge_less_than d = {(z',z). d \<le> z' & z' < z}"
884 theorem wf_int_ge_less_than: "wf (int_ge_less_than d)"
885 proof -
886   have "int_ge_less_than d \<subseteq> measure (%z. nat (z-d))"
887     by (auto simp add: int_ge_less_than_def)
888   thus ?thesis
889     by (rule wf_subset [OF wf_measure])
890 qed
892 text{*This variant looks odd, but is typical of the relations suggested
893 by RankFinder.*}
895 definition
896   int_ge_less_than2 ::  "int => (int * int) set"
897 where
898   "int_ge_less_than2 d = {(z',z). d \<le> z & z' < z}"
900 theorem wf_int_ge_less_than2: "wf (int_ge_less_than2 d)"
901 proof -
902   have "int_ge_less_than2 d \<subseteq> measure (%z. nat (1+z-d))"
903     by (auto simp add: int_ge_less_than2_def)
904   thus ?thesis
905     by (rule wf_subset [OF wf_measure])
906 qed
908 (* `set:int': dummy construction *)
909 theorem int_ge_induct [case_names base step, induct set: int]:
910   fixes i :: int
911   assumes ge: "k \<le> i" and
912     base: "P k" and
913     step: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
914   shows "P i"
915 proof -
916   { fix n
917     have "\<And>i::int. n = nat (i - k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i"
918     proof (induct n)
919       case 0
920       hence "i = k" by arith
921       thus "P i" using base by simp
922     next
923       case (Suc n)
924       then have "n = nat((i - 1) - k)" by arith
925       moreover
926       have ki1: "k \<le> i - 1" using Suc.prems by arith
927       ultimately
928       have "P (i - 1)" by (rule Suc.hyps)
929       from step [OF ki1 this] show ?case by simp
930     qed
931   }
932   with ge show ?thesis by fast
933 qed
935 (* `set:int': dummy construction *)
936 theorem int_gr_induct [case_names base step, induct set: int]:
937   assumes gr: "k < (i::int)" and
938         base: "P(k+1)" and
939         step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
940   shows "P i"
941 apply(rule int_ge_induct[of "k + 1"])
942   using gr apply arith
943  apply(rule base)
944 apply (rule step, simp+)
945 done
947 theorem int_le_induct [consumes 1, case_names base step]:
948   assumes le: "i \<le> (k::int)" and
949         base: "P(k)" and
950         step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
951   shows "P i"
952 proof -
953   { fix n
954     have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i"
955     proof (induct n)
956       case 0
957       hence "i = k" by arith
958       thus "P i" using base by simp
959     next
960       case (Suc n)
961       hence "n = nat (k - (i + 1))" by arith
962       moreover
963       have ki1: "i + 1 \<le> k" using Suc.prems by arith
964       ultimately
965       have "P (i + 1)" by(rule Suc.hyps)
966       from step[OF ki1 this] show ?case by simp
967     qed
968   }
969   with le show ?thesis by fast
970 qed
972 theorem int_less_induct [consumes 1, case_names base step]:
973   assumes less: "(i::int) < k" and
974         base: "P(k - 1)" and
975         step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
976   shows "P i"
977 apply(rule int_le_induct[of _ "k - 1"])
978   using less apply arith
979  apply(rule base)
980 apply (rule step, simp+)
981 done
983 theorem int_induct [case_names base step1 step2]:
984   fixes k :: int
985   assumes base: "P k"
986     and step1: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
987     and step2: "\<And>i. k \<ge> i \<Longrightarrow> P i \<Longrightarrow> P (i - 1)"
988   shows "P i"
989 proof -
990   have "i \<le> k \<or> i \<ge> k" by arith
991   then show ?thesis
992   proof
993     assume "i \<ge> k"
994     then show ?thesis using base
995       by (rule int_ge_induct) (fact step1)
996   next
997     assume "i \<le> k"
998     then show ?thesis using base
999       by (rule int_le_induct) (fact step2)
1000   qed
1001 qed
1003 subsection{*Intermediate value theorems*}
1005 lemma int_val_lemma:
1006      "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->
1007       f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
1008 unfolding One_nat_def
1009 apply (induct n)
1010 apply simp
1011 apply (intro strip)
1012 apply (erule impE, simp)
1013 apply (erule_tac x = n in allE, simp)
1014 apply (case_tac "k = f (Suc n)")
1015 apply force
1016 apply (erule impE)
1017  apply (simp add: abs_if split add: split_if_asm)
1018 apply (blast intro: le_SucI)
1019 done
1021 lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
1023 lemma nat_intermed_int_val:
1024      "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;
1025          f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
1026 apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k
1027        in int_val_lemma)
1028 unfolding One_nat_def
1029 apply simp
1030 apply (erule exE)
1031 apply (rule_tac x = "i+m" in exI, arith)
1032 done
1035 subsection{*Products and 1, by T. M. Rasmussen*}
1037 lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))"
1038 by arith
1040 lemma abs_zmult_eq_1:
1041   assumes mn: "\<bar>m * n\<bar> = 1"
1042   shows "\<bar>m\<bar> = (1::int)"
1043 proof -
1044   have 0: "m \<noteq> 0 & n \<noteq> 0" using mn
1045     by auto
1046   have "~ (2 \<le> \<bar>m\<bar>)"
1047   proof
1048     assume "2 \<le> \<bar>m\<bar>"
1049     hence "2*\<bar>n\<bar> \<le> \<bar>m\<bar>*\<bar>n\<bar>"
1050       by (simp add: mult_mono 0)
1051     also have "... = \<bar>m*n\<bar>"
1052       by (simp add: abs_mult)
1053     also have "... = 1"
1054       by (simp add: mn)
1055     finally have "2*\<bar>n\<bar> \<le> 1" .
1056     thus "False" using 0
1057       by arith
1058   qed
1059   thus ?thesis using 0
1060     by auto
1061 qed
1063 ML_val {* @{const_name neg_numeral} *}
1065 lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1"
1066 by (insert abs_zmult_eq_1 [of m n], arith)
1068 lemma pos_zmult_eq_1_iff:
1069   assumes "0 < (m::int)" shows "(m * n = 1) = (m = 1 & n = 1)"
1070 proof -
1071   from assms have "m * n = 1 ==> m = 1" by (auto dest: pos_zmult_eq_1_iff_lemma)
1072   thus ?thesis by (auto dest: pos_zmult_eq_1_iff_lemma)
1073 qed
1075 lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
1076 apply (rule iffI)
1077  apply (frule pos_zmult_eq_1_iff_lemma)
1078  apply (simp add: mult_commute [of m])
1079  apply (frule pos_zmult_eq_1_iff_lemma, auto)
1080 done
1082 lemma infinite_UNIV_int: "\<not> finite (UNIV::int set)"
1083 proof
1084   assume "finite (UNIV::int set)"
1085   moreover have "inj (\<lambda>i\<Colon>int. 2 * i)"
1086     by (rule injI) simp
1087   ultimately have "surj (\<lambda>i\<Colon>int. 2 * i)"
1088     by (rule finite_UNIV_inj_surj)
1089   then obtain i :: int where "1 = 2 * i" by (rule surjE)
1090   then show False by (simp add: pos_zmult_eq_1_iff)
1091 qed
1094 subsection {* Further theorems on numerals *}
1096 subsubsection{*Special Simplification for Constants*}
1098 text{*These distributive laws move literals inside sums and differences.*}
1100 lemmas distrib_right_numeral [simp] = distrib_right [of _ _ "numeral v"] for v
1101 lemmas distrib_left_numeral [simp] = distrib_left [of "numeral v"] for v
1102 lemmas left_diff_distrib_numeral [simp] = left_diff_distrib [of _ _ "numeral v"] for v
1103 lemmas right_diff_distrib_numeral [simp] = right_diff_distrib [of "numeral v"] for v
1105 text{*These are actually for fields, like real: but where else to put them?*}
1107 lemmas zero_less_divide_iff_numeral [simp, no_atp] = zero_less_divide_iff [of "numeral w"] for w
1108 lemmas divide_less_0_iff_numeral [simp, no_atp] = divide_less_0_iff [of "numeral w"] for w
1109 lemmas zero_le_divide_iff_numeral [simp, no_atp] = zero_le_divide_iff [of "numeral w"] for w
1110 lemmas divide_le_0_iff_numeral [simp, no_atp] = divide_le_0_iff [of "numeral w"] for w
1113 text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}.  It looks
1114   strange, but then other simprocs simplify the quotient.*}
1116 lemmas inverse_eq_divide_numeral [simp] =
1117   inverse_eq_divide [of "numeral w"] for w
1119 lemmas inverse_eq_divide_neg_numeral [simp] =
1120   inverse_eq_divide [of "neg_numeral w"] for w
1122 text {*These laws simplify inequalities, moving unary minus from a term
1123 into the literal.*}
1125 lemmas le_minus_iff_numeral [simp, no_atp] =
1126   le_minus_iff [of "numeral v"]
1127   le_minus_iff [of "neg_numeral v"] for v
1129 lemmas equation_minus_iff_numeral [simp, no_atp] =
1130   equation_minus_iff [of "numeral v"]
1131   equation_minus_iff [of "neg_numeral v"] for v
1133 lemmas minus_less_iff_numeral [simp, no_atp] =
1134   minus_less_iff [of _ "numeral v"]
1135   minus_less_iff [of _ "neg_numeral v"] for v
1137 lemmas minus_le_iff_numeral [simp, no_atp] =
1138   minus_le_iff [of _ "numeral v"]
1139   minus_le_iff [of _ "neg_numeral v"] for v
1141 lemmas minus_equation_iff_numeral [simp, no_atp] =
1142   minus_equation_iff [of _ "numeral v"]
1143   minus_equation_iff [of _ "neg_numeral v"] for v
1145 text{*To Simplify Inequalities Where One Side is the Constant 1*}
1147 lemma less_minus_iff_1 [simp,no_atp]:
1148   fixes b::"'b::linordered_idom"
1149   shows "(1 < - b) = (b < -1)"
1150 by auto
1152 lemma le_minus_iff_1 [simp,no_atp]:
1153   fixes b::"'b::linordered_idom"
1154   shows "(1 \<le> - b) = (b \<le> -1)"
1155 by auto
1157 lemma equation_minus_iff_1 [simp,no_atp]:
1158   fixes b::"'b::ring_1"
1159   shows "(1 = - b) = (b = -1)"
1160 by (subst equation_minus_iff, auto)
1162 lemma minus_less_iff_1 [simp,no_atp]:
1163   fixes a::"'b::linordered_idom"
1164   shows "(- a < 1) = (-1 < a)"
1165 by auto
1167 lemma minus_le_iff_1 [simp,no_atp]:
1168   fixes a::"'b::linordered_idom"
1169   shows "(- a \<le> 1) = (-1 \<le> a)"
1170 by auto
1172 lemma minus_equation_iff_1 [simp,no_atp]:
1173   fixes a::"'b::ring_1"
1174   shows "(- a = 1) = (a = -1)"
1175 by (subst minus_equation_iff, auto)
1178 text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
1180 lemmas mult_less_cancel_left_numeral [simp, no_atp] = mult_less_cancel_left [of "numeral v"] for v
1181 lemmas mult_less_cancel_right_numeral [simp, no_atp] = mult_less_cancel_right [of _ "numeral v"] for v
1182 lemmas mult_le_cancel_left_numeral [simp, no_atp] = mult_le_cancel_left [of "numeral v"] for v
1183 lemmas mult_le_cancel_right_numeral [simp, no_atp] = mult_le_cancel_right [of _ "numeral v"] for v
1186 text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
1188 lemmas le_divide_eq_numeral1 [simp] =
1189   pos_le_divide_eq [of "numeral w", OF zero_less_numeral]
1190   neg_le_divide_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w
1192 lemmas divide_le_eq_numeral1 [simp] =
1193   pos_divide_le_eq [of "numeral w", OF zero_less_numeral]
1194   neg_divide_le_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w
1196 lemmas less_divide_eq_numeral1 [simp] =
1197   pos_less_divide_eq [of "numeral w", OF zero_less_numeral]
1198   neg_less_divide_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w
1200 lemmas divide_less_eq_numeral1 [simp] =
1201   pos_divide_less_eq [of "numeral w", OF zero_less_numeral]
1202   neg_divide_less_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w
1204 lemmas eq_divide_eq_numeral1 [simp] =
1205   eq_divide_eq [of _ _ "numeral w"]
1206   eq_divide_eq [of _ _ "neg_numeral w"] for w
1208 lemmas divide_eq_eq_numeral1 [simp] =
1209   divide_eq_eq [of _ "numeral w"]
1210   divide_eq_eq [of _ "neg_numeral w"] for w
1212 subsubsection{*Optional Simplification Rules Involving Constants*}
1214 text{*Simplify quotients that are compared with a literal constant.*}
1216 lemmas le_divide_eq_numeral =
1217   le_divide_eq [of "numeral w"]
1218   le_divide_eq [of "neg_numeral w"] for w
1220 lemmas divide_le_eq_numeral =
1221   divide_le_eq [of _ _ "numeral w"]
1222   divide_le_eq [of _ _ "neg_numeral w"] for w
1224 lemmas less_divide_eq_numeral =
1225   less_divide_eq [of "numeral w"]
1226   less_divide_eq [of "neg_numeral w"] for w
1228 lemmas divide_less_eq_numeral =
1229   divide_less_eq [of _ _ "numeral w"]
1230   divide_less_eq [of _ _ "neg_numeral w"] for w
1232 lemmas eq_divide_eq_numeral =
1233   eq_divide_eq [of "numeral w"]
1234   eq_divide_eq [of "neg_numeral w"] for w
1236 lemmas divide_eq_eq_numeral =
1237   divide_eq_eq [of _ _ "numeral w"]
1238   divide_eq_eq [of _ _ "neg_numeral w"] for w
1241 text{*Not good as automatic simprules because they cause case splits.*}
1242 lemmas divide_const_simps =
1243   le_divide_eq_numeral divide_le_eq_numeral less_divide_eq_numeral
1244   divide_less_eq_numeral eq_divide_eq_numeral divide_eq_eq_numeral
1245   le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
1247 text{*Division By @{text "-1"}*}
1249 lemma divide_minus1 [simp]: "(x::'a::field) / -1 = - x"
1250   unfolding minus_one [symmetric]
1251   unfolding nonzero_minus_divide_right [OF one_neq_zero, symmetric]
1252   by simp
1254 lemma minus1_divide [simp]: "-1 / (x::'a::field) = - (1 / x)"
1255   unfolding minus_one [symmetric] by (rule divide_minus_left)
1257 lemma half_gt_zero_iff:
1258      "(0 < r/2) = (0 < (r::'a::linordered_field_inverse_zero))"
1259 by auto
1261 lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2]
1263 lemma divide_Numeral1: "(x::'a::field) / Numeral1 = x"
1264   by simp
1267 subsection {* The divides relation *}
1269 lemma zdvd_antisym_nonneg:
1270     "0 <= m ==> 0 <= n ==> m dvd n ==> n dvd m ==> m = (n::int)"
1271   apply (simp add: dvd_def, auto)
1272   apply (auto simp add: mult_assoc zero_le_mult_iff zmult_eq_1_iff)
1273   done
1275 lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a"
1276   shows "\<bar>a\<bar> = \<bar>b\<bar>"
1277 proof cases
1278   assume "a = 0" with assms show ?thesis by simp
1279 next
1280   assume "a \<noteq> 0"
1281   from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast
1282   from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast
1283   from k k' have "a = a*k*k'" by simp
1284   with mult_cancel_left1[where c="a" and b="k*k'"]
1285   have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult_assoc)
1286   hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff)
1287   thus ?thesis using k k' by auto
1288 qed
1290 lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
1291   apply (subgoal_tac "m = n + (m - n)")
1292    apply (erule ssubst)
1293    apply (blast intro: dvd_add, simp)
1294   done
1296 lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
1297 apply (rule iffI)
1298  apply (erule_tac  dvd_add)
1299  apply (subgoal_tac "n = (n + k * m) - k * m")
1300   apply (erule ssubst)
1301   apply (erule dvd_diff)
1302   apply(simp_all)
1303 done
1305 lemma dvd_imp_le_int:
1306   fixes d i :: int
1307   assumes "i \<noteq> 0" and "d dvd i"
1308   shows "\<bar>d\<bar> \<le> \<bar>i\<bar>"
1309 proof -
1310   from `d dvd i` obtain k where "i = d * k" ..
1311   with `i \<noteq> 0` have "k \<noteq> 0" by auto
1312   then have "1 \<le> \<bar>k\<bar>" and "0 \<le> \<bar>d\<bar>" by auto
1313   then have "\<bar>d\<bar> * 1 \<le> \<bar>d\<bar> * \<bar>k\<bar>" by (rule mult_left_mono)
1314   with `i = d * k` show ?thesis by (simp add: abs_mult)
1315 qed
1317 lemma zdvd_not_zless:
1318   fixes m n :: int
1319   assumes "0 < m" and "m < n"
1320   shows "\<not> n dvd m"
1321 proof
1322   from assms have "0 < n" by auto
1323   assume "n dvd m" then obtain k where k: "m = n * k" ..
1324   with `0 < m` have "0 < n * k" by auto
1325   with `0 < n` have "0 < k" by (simp add: zero_less_mult_iff)
1326   with k `0 < n` `m < n` have "n * k < n * 1" by simp
1327   with `0 < n` `0 < k` show False unfolding mult_less_cancel_left by auto
1328 qed
1330 lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)"
1331   shows "m dvd n"
1332 proof-
1333   from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast
1334   {assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp
1335     with h have False by (simp add: mult_assoc)}
1336   hence "n = m * h" by blast
1337   thus ?thesis by simp
1338 qed
1340 theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
1341 proof -
1342   have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"
1343   proof -
1344     fix k
1345     assume A: "int y = int x * k"
1346     then show "x dvd y"
1347     proof (cases k)
1348       case (nonneg n)
1349       with A have "y = x * n" by (simp add: of_nat_mult [symmetric])
1350       then show ?thesis ..
1351     next
1352       case (neg n)
1353       with A have "int y = int x * (- int (Suc n))" by simp
1354       also have "\<dots> = - (int x * int (Suc n))" by (simp only: mult_minus_right)
1355       also have "\<dots> = - int (x * Suc n)" by (simp only: of_nat_mult [symmetric])
1356       finally have "- int (x * Suc n) = int y" ..
1357       then show ?thesis by (simp only: negative_eq_positive) auto
1358     qed
1359   qed
1360   then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left of_nat_mult)
1361 qed
1363 lemma zdvd1_eq[simp]: "(x::int) dvd 1 = (\<bar>x\<bar> = 1)"
1364 proof
1365   assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp
1366   hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
1367   hence "nat \<bar>x\<bar> = 1"  by simp
1368   thus "\<bar>x\<bar> = 1" by (cases "x < 0") auto
1369 next
1370   assume "\<bar>x\<bar>=1"
1371   then have "x = 1 \<or> x = -1" by auto
1372   then show "x dvd 1" by (auto intro: dvdI)
1373 qed
1375 lemma zdvd_mult_cancel1:
1376   assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
1377 proof
1378   assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m"
1379     by (cases "n >0") (auto simp add: minus_equation_iff)
1380 next
1381   assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
1382   from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
1383 qed
1385 lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
1386   unfolding zdvd_int by (cases "z \<ge> 0") simp_all
1388 lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
1389   unfolding zdvd_int by (cases "z \<ge> 0") simp_all
1391 lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
1392   by (auto simp add: dvd_int_iff)
1394 lemma eq_nat_nat_iff:
1395   "0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat z = nat z' \<longleftrightarrow> z = z'"
1396   by (auto elim!: nonneg_eq_int)
1398 lemma nat_power_eq:
1399   "0 \<le> z \<Longrightarrow> nat (z ^ n) = nat z ^ n"
1400   by (induct n) (simp_all add: nat_mult_distrib)
1402 lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
1403   apply (cases n)
1404   apply (auto simp add: dvd_int_iff)
1405   apply (cases z)
1406   apply (auto simp add: dvd_imp_le)
1407   done
1409 lemma zdvd_period:
1410   fixes a d :: int
1411   assumes "a dvd d"
1412   shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)"
1413 proof -
1414   from assms obtain k where "d = a * k" by (rule dvdE)
1415   show ?thesis
1416   proof
1417     assume "a dvd (x + t)"
1418     then obtain l where "x + t = a * l" by (rule dvdE)
1419     then have "x = a * l - t" by simp
1420     with `d = a * k` show "a dvd x + c * d + t" by simp
1421   next
1422     assume "a dvd x + c * d + t"
1423     then obtain l where "x + c * d + t = a * l" by (rule dvdE)
1424     then have "x = a * l - c * d - t" by simp
1425     with `d = a * k` show "a dvd (x + t)" by simp
1426   qed
1427 qed
1430 subsection {* Finiteness of intervals *}
1432 lemma finite_interval_int1 [iff]: "finite {i :: int. a <= i & i <= b}"
1433 proof (cases "a <= b")
1434   case True
1435   from this show ?thesis
1436   proof (induct b rule: int_ge_induct)
1437     case base
1438     have "{i. a <= i & i <= a} = {a}" by auto
1439     from this show ?case by simp
1440   next
1441     case (step b)
1442     from this have "{i. a <= i & i <= b + 1} = {i. a <= i & i <= b} \<union> {b + 1}" by auto
1443     from this step show ?case by simp
1444   qed
1445 next
1446   case False from this show ?thesis
1447     by (metis (lifting, no_types) Collect_empty_eq finite.emptyI order_trans)
1448 qed
1450 lemma finite_interval_int2 [iff]: "finite {i :: int. a <= i & i < b}"
1451 by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
1453 lemma finite_interval_int3 [iff]: "finite {i :: int. a < i & i <= b}"
1454 by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
1456 lemma finite_interval_int4 [iff]: "finite {i :: int. a < i & i < b}"
1457 by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
1460 subsection {* Configuration of the code generator *}
1462 text {* Constructors *}
1464 definition Pos :: "num \<Rightarrow> int" where
1465   [simp, code_abbrev]: "Pos = numeral"
1467 definition Neg :: "num \<Rightarrow> int" where
1468   [simp, code_abbrev]: "Neg = neg_numeral"
1470 code_datatype "0::int" Pos Neg
1473 text {* Auxiliary operations *}
1475 definition dup :: "int \<Rightarrow> int" where
1476   [simp]: "dup k = k + k"
1478 lemma dup_code [code]:
1479   "dup 0 = 0"
1480   "dup (Pos n) = Pos (Num.Bit0 n)"
1481   "dup (Neg n) = Neg (Num.Bit0 n)"
1482   unfolding Pos_def Neg_def neg_numeral_def
1483   by (simp_all add: numeral_Bit0)
1485 definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
1486   [simp]: "sub m n = numeral m - numeral n"
1488 lemma sub_code [code]:
1489   "sub Num.One Num.One = 0"
1490   "sub (Num.Bit0 m) Num.One = Pos (Num.BitM m)"
1491   "sub (Num.Bit1 m) Num.One = Pos (Num.Bit0 m)"
1492   "sub Num.One (Num.Bit0 n) = Neg (Num.BitM n)"
1493   "sub Num.One (Num.Bit1 n) = Neg (Num.Bit0 n)"
1494   "sub (Num.Bit0 m) (Num.Bit0 n) = dup (sub m n)"
1495   "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)"
1496   "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1"
1497   "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1"
1498   unfolding sub_def dup_def numeral.simps Pos_def Neg_def
1499     neg_numeral_def numeral_BitM
1500   by (simp_all only: algebra_simps)
1503 text {* Implementations *}
1505 lemma one_int_code [code, code_unfold]:
1506   "1 = Pos Num.One"
1507   by simp
1509 lemma plus_int_code [code]:
1510   "k + 0 = (k::int)"
1511   "0 + l = (l::int)"
1512   "Pos m + Pos n = Pos (m + n)"
1513   "Pos m + Neg n = sub m n"
1514   "Neg m + Pos n = sub n m"
1515   "Neg m + Neg n = Neg (m + n)"
1516   by simp_all
1518 lemma uminus_int_code [code]:
1519   "uminus 0 = (0::int)"
1520   "uminus (Pos m) = Neg m"
1521   "uminus (Neg m) = Pos m"
1522   by simp_all
1524 lemma minus_int_code [code]:
1525   "k - 0 = (k::int)"
1526   "0 - l = uminus (l::int)"
1527   "Pos m - Pos n = sub m n"
1528   "Pos m - Neg n = Pos (m + n)"
1529   "Neg m - Pos n = Neg (m + n)"
1530   "Neg m - Neg n = sub n m"
1531   by simp_all
1533 lemma times_int_code [code]:
1534   "k * 0 = (0::int)"
1535   "0 * l = (0::int)"
1536   "Pos m * Pos n = Pos (m * n)"
1537   "Pos m * Neg n = Neg (m * n)"
1538   "Neg m * Pos n = Neg (m * n)"
1539   "Neg m * Neg n = Pos (m * n)"
1540   by simp_all
1542 instantiation int :: equal
1543 begin
1545 definition
1546   "HOL.equal k l \<longleftrightarrow> k = (l::int)"
1548 instance by default (rule equal_int_def)
1550 end
1552 lemma equal_int_code [code]:
1553   "HOL.equal 0 (0::int) \<longleftrightarrow> True"
1554   "HOL.equal 0 (Pos l) \<longleftrightarrow> False"
1555   "HOL.equal 0 (Neg l) \<longleftrightarrow> False"
1556   "HOL.equal (Pos k) 0 \<longleftrightarrow> False"
1557   "HOL.equal (Pos k) (Pos l) \<longleftrightarrow> HOL.equal k l"
1558   "HOL.equal (Pos k) (Neg l) \<longleftrightarrow> False"
1559   "HOL.equal (Neg k) 0 \<longleftrightarrow> False"
1560   "HOL.equal (Neg k) (Pos l) \<longleftrightarrow> False"
1561   "HOL.equal (Neg k) (Neg l) \<longleftrightarrow> HOL.equal k l"
1562   by (auto simp add: equal)
1564 lemma equal_int_refl [code nbe]:
1565   "HOL.equal (k::int) k \<longleftrightarrow> True"
1566   by (fact equal_refl)
1568 lemma less_eq_int_code [code]:
1569   "0 \<le> (0::int) \<longleftrightarrow> True"
1570   "0 \<le> Pos l \<longleftrightarrow> True"
1571   "0 \<le> Neg l \<longleftrightarrow> False"
1572   "Pos k \<le> 0 \<longleftrightarrow> False"
1573   "Pos k \<le> Pos l \<longleftrightarrow> k \<le> l"
1574   "Pos k \<le> Neg l \<longleftrightarrow> False"
1575   "Neg k \<le> 0 \<longleftrightarrow> True"
1576   "Neg k \<le> Pos l \<longleftrightarrow> True"
1577   "Neg k \<le> Neg l \<longleftrightarrow> l \<le> k"
1578   by simp_all
1580 lemma less_int_code [code]:
1581   "0 < (0::int) \<longleftrightarrow> False"
1582   "0 < Pos l \<longleftrightarrow> True"
1583   "0 < Neg l \<longleftrightarrow> False"
1584   "Pos k < 0 \<longleftrightarrow> False"
1585   "Pos k < Pos l \<longleftrightarrow> k < l"
1586   "Pos k < Neg l \<longleftrightarrow> False"
1587   "Neg k < 0 \<longleftrightarrow> True"
1588   "Neg k < Pos l \<longleftrightarrow> True"
1589   "Neg k < Neg l \<longleftrightarrow> l < k"
1590   by simp_all
1592 lemma nat_code [code]:
1593   "nat (Int.Neg k) = 0"
1594   "nat 0 = 0"
1595   "nat (Int.Pos k) = nat_of_num k"
1596   by (simp_all add: nat_of_num_numeral nat_numeral)
1598 lemma (in ring_1) of_int_code [code]:
1599   "of_int (Int.Neg k) = neg_numeral k"
1600   "of_int 0 = 0"
1601   "of_int (Int.Pos k) = numeral k"
1602   by simp_all
1605 text {* Serializer setup *}
1607 code_modulename SML
1608   Int Arith
1610 code_modulename OCaml
1611   Int Arith
1614   Int Arith
1616 quickcheck_params [default_type = int]
1618 hide_const (open) Pos Neg sub dup
1621 subsection {* Legacy theorems *}
1623 lemmas inj_int = inj_of_nat [where 'a=int]
1624 lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
1625 lemmas int_mult = of_nat_mult [where 'a=int]
1626 lemmas zmult_int = of_nat_mult [where 'a=int, symmetric]
1627 lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="n"] for n
1628 lemmas zless_int = of_nat_less_iff [where 'a=int]
1629 lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="k"] for k
1630 lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int]
1631 lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
1632 lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="n"] for n
1633 lemmas int_0 = of_nat_0 [where 'a=int]
1634 lemmas int_1 = of_nat_1 [where 'a=int]
1635 lemmas int_Suc = of_nat_Suc [where 'a=int]
1636 lemmas int_numeral = of_nat_numeral [where 'a=int]
1637 lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m"] for m
1638 lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
1639 lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
1640 lemmas zpower_numeral_even = power_numeral_even [where 'a=int]
1641 lemmas zpower_numeral_odd = power_numeral_odd [where 'a=int]
1643 lemma zpower_zpower:
1644   "(x ^ y) ^ z = (x ^ (y * z)::int)"
1645   by (rule power_mult [symmetric])
1647 lemma int_power:
1648   "int (m ^ n) = int m ^ n"
1649   by (rule of_nat_power)
1651 lemmas zpower_int = int_power [symmetric]
1653 text {* De-register @{text "int"} as a quotient type: *}
1655 lemmas [transfer_rule del] =
1656   int.id_abs_transfer int.rel_eq_transfer zero_int.transfer one_int.transfer
1657   plus_int.transfer uminus_int.transfer minus_int.transfer times_int.transfer
1658   int_transfer less_eq_int.transfer less_int.transfer of_int.transfer
1659   nat.transfer
1661 declare Quotient_int [quot_del]
1663 end