src/HOL/Int.thy
 author haftmann Sun Oct 12 17:05:34 2014 +0200 (2014-10-12) changeset 58649 a62065b5e1e2 parent 58512 dc4d76dfa8f0 child 58650 1ddba8bcbb58 permissions -rw-r--r--
generalized and consolidated some theorems concerning divisibility
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 Power Quotient Fun_Def
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)" .
42 lift_definition one_int :: "int" is "(1, 0)" .
44 lift_definition plus_int :: "int \<Rightarrow> int \<Rightarrow> int"
45   is "\<lambda>(x, y) (u, v). (x + u, y + v)"
46   by clarsimp
48 lift_definition uminus_int :: "int \<Rightarrow> int"
49   is "\<lambda>(x, y). (y, x)"
50   by clarsimp
52 lift_definition minus_int :: "int \<Rightarrow> int \<Rightarrow> int"
53   is "\<lambda>(x, y) (u, v). (x + v, y + u)"
54   by clarsimp
56 lift_definition times_int :: "int \<Rightarrow> int \<Rightarrow> int"
57   is "\<lambda>(x, y) (u, v). (x*u + y*v, x*v + y*u)"
58 proof (clarsimp)
59   fix s t u v w x y z :: nat
60   assume "s + v = u + t" and "w + z = y + x"
61   hence "(s + v) * w + (u + t) * x + u * (w + z) + v * (y + x)
62        = (u + t) * w + (s + v) * x + u * (y + x) + v * (w + z)"
63     by simp
64   thus "(s * w + t * x) + (u * z + v * y) = (u * y + v * z) + (s * x + t * w)"
65     by (simp add: algebra_simps)
66 qed
68 instance
69   by default (transfer, clarsimp simp: algebra_simps)+
71 end
73 abbreviation int :: "nat \<Rightarrow> int" where
74   "int \<equiv> of_nat"
76 lemma int_def: "int n = Abs_Integ (n, 0)"
77   by (induct n, simp add: zero_int.abs_eq,
78     simp add: one_int.abs_eq plus_int.abs_eq)
80 lemma int_transfer [transfer_rule]:
81   "(rel_fun (op =) pcr_int) (\<lambda>n. (n, 0)) int"
82   unfolding rel_fun_def int.pcr_cr_eq cr_int_def int_def by simp
84 lemma int_diff_cases:
85   obtains (diff) m n where "z = int m - int n"
86   by transfer clarsimp
88 subsection {* Integers are totally ordered *}
90 instantiation int :: linorder
91 begin
93 lift_definition less_eq_int :: "int \<Rightarrow> int \<Rightarrow> bool"
94   is "\<lambda>(x, y) (u, v). x + v \<le> u + y"
95   by auto
97 lift_definition less_int :: "int \<Rightarrow> int \<Rightarrow> bool"
98   is "\<lambda>(x, y) (u, v). x + v < u + y"
99   by auto
101 instance
102   by default (transfer, force)+
104 end
106 instantiation int :: distrib_lattice
107 begin
109 definition
110   "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
112 definition
113   "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
115 instance
116   by intro_classes
117     (auto simp add: inf_int_def sup_int_def max_min_distrib2)
119 end
121 subsection {* Ordering properties of arithmetic operations *}
123 instance int :: ordered_cancel_ab_semigroup_add
124 proof
125   fix i j k :: int
126   show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
127     by transfer clarsimp
128 qed
130 text{*Strict Monotonicity of Multiplication*}
132 text{*strict, in 1st argument; proof is by induction on k>0*}
133 lemma zmult_zless_mono2_lemma:
134      "(i::int)<j ==> 0<k ==> int k * i < int k * j"
135 apply (induct k)
136 apply simp
137 apply (simp add: distrib_right)
138 apply (case_tac "k=0")
140 done
142 lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = int n"
143 apply transfer
144 apply clarsimp
145 apply (rule_tac x="a - b" in exI, simp)
146 done
148 lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = int n"
149 apply transfer
150 apply clarsimp
151 apply (rule_tac x="a - b" in exI, simp)
152 done
154 lemma zmult_zless_mono2: "[| i<j;  (0::int) < k |] ==> k*i < k*j"
155 apply (drule zero_less_imp_eq_int)
156 apply (auto simp add: zmult_zless_mono2_lemma)
157 done
159 text{*The integers form an ordered integral domain*}
160 instantiation int :: linordered_idom
161 begin
163 definition
164   zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
166 definition
167   zsgn_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
169 instance proof
170   fix i j k :: int
171   show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
172     by (rule zmult_zless_mono2)
173   show "\<bar>i\<bar> = (if i < 0 then -i else i)"
174     by (simp only: zabs_def)
175   show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
176     by (simp only: zsgn_def)
177 qed
179 end
181 lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + (1\<Colon>int) \<le> z"
182   by transfer clarsimp
185   "(w \<Colon> int) < z \<longleftrightarrow> (\<exists>n. z = w + int (Suc n))"
186 apply transfer
187 apply auto
188 apply (rename_tac a b c d)
189 apply (rule_tac x="c+b - Suc(a+d)" in exI)
190 apply arith
191 done
193 lemmas int_distrib =
194   distrib_right [of z1 z2 w]
195   distrib_left [of w z1 z2]
196   left_diff_distrib [of z1 z2 w]
197   right_diff_distrib [of w z1 z2]
198   for z1 z2 w :: int
201 subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}
203 context ring_1
204 begin
206 lift_definition of_int :: "int \<Rightarrow> 'a" is "\<lambda>(i, j). of_nat i - of_nat j"
207   by (clarsimp simp add: diff_eq_eq eq_diff_eq diff_add_eq
210 lemma of_int_0 [simp]: "of_int 0 = 0"
211   by transfer simp
213 lemma of_int_1 [simp]: "of_int 1 = 1"
214   by transfer simp
216 lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z"
217   by transfer (clarsimp simp add: algebra_simps)
219 lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)"
220   by (transfer fixing: uminus) clarsimp
222 lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z"
223   using of_int_add [of w "- z"] by simp
225 lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
226   by (transfer fixing: times) (clarsimp simp add: algebra_simps of_nat_mult)
228 text{*Collapse nested embeddings*}
229 lemma of_int_of_nat_eq [simp]: "of_int (int n) = of_nat n"
230 by (induct n) auto
232 lemma of_int_numeral [simp, code_post]: "of_int (numeral k) = numeral k"
233   by (simp add: of_nat_numeral [symmetric] of_int_of_nat_eq [symmetric])
235 lemma of_int_neg_numeral [code_post]: "of_int (- numeral k) = - numeral k"
236   by simp
238 lemma of_int_power:
239   "of_int (z ^ n) = of_int z ^ n"
240   by (induct n) simp_all
242 end
244 context ring_char_0
245 begin
247 lemma of_int_eq_iff [simp]:
248    "of_int w = of_int z \<longleftrightarrow> w = z"
249   by transfer (clarsimp simp add: algebra_simps
252 text{*Special cases where either operand is zero*}
253 lemma of_int_eq_0_iff [simp]:
254   "of_int z = 0 \<longleftrightarrow> z = 0"
255   using of_int_eq_iff [of z 0] by simp
257 lemma of_int_0_eq_iff [simp]:
258   "0 = of_int z \<longleftrightarrow> z = 0"
259   using of_int_eq_iff [of 0 z] by simp
261 end
263 context linordered_idom
264 begin
266 text{*Every @{text linordered_idom} has characteristic zero.*}
267 subclass ring_char_0 ..
269 lemma of_int_le_iff [simp]:
270   "of_int w \<le> of_int z \<longleftrightarrow> w \<le> z"
271   by (transfer fixing: less_eq) (clarsimp simp add: algebra_simps
274 lemma of_int_less_iff [simp]:
275   "of_int w < of_int z \<longleftrightarrow> w < z"
276   by (simp add: less_le order_less_le)
278 lemma of_int_0_le_iff [simp]:
279   "0 \<le> of_int z \<longleftrightarrow> 0 \<le> z"
280   using of_int_le_iff [of 0 z] by simp
282 lemma of_int_le_0_iff [simp]:
283   "of_int z \<le> 0 \<longleftrightarrow> z \<le> 0"
284   using of_int_le_iff [of z 0] by simp
286 lemma of_int_0_less_iff [simp]:
287   "0 < of_int z \<longleftrightarrow> 0 < z"
288   using of_int_less_iff [of 0 z] by simp
290 lemma of_int_less_0_iff [simp]:
291   "of_int z < 0 \<longleftrightarrow> z < 0"
292   using of_int_less_iff [of z 0] by simp
294 end
296 lemma of_nat_less_of_int_iff:
297   "(of_nat n::'a::linordered_idom) < of_int x \<longleftrightarrow> int n < x"
298   by (metis of_int_of_nat_eq of_int_less_iff)
300 lemma of_int_eq_id [simp]: "of_int = id"
301 proof
302   fix z show "of_int z = id z"
303     by (cases z rule: int_diff_cases, simp)
304 qed
307 instance int :: no_top
308   apply default
309   apply (rule_tac x="x + 1" in exI)
310   apply simp
311   done
313 instance int :: no_bot
314   apply default
315   apply (rule_tac x="x - 1" in exI)
316   apply simp
317   done
319 subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *}
321 lift_definition nat :: "int \<Rightarrow> nat" is "\<lambda>(x, y). x - y"
322   by auto
324 lemma nat_int [simp]: "nat (int n) = n"
325   by transfer simp
327 lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
328   by transfer clarsimp
330 corollary nat_0_le: "0 \<le> z ==> int (nat z) = z"
331 by simp
333 lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
334   by transfer clarsimp
336 lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"
337   by transfer (clarsimp, arith)
339 text{*An alternative condition is @{term "0 \<le> w"} *}
340 corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
341 by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
343 corollary nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"
344 by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
346 lemma zless_nat_conj [simp]: "(nat w < nat z) = (0 < z & w < z)"
347   by transfer (clarsimp, arith)
349 lemma nonneg_eq_int:
350   fixes z :: int
351   assumes "0 \<le> z" and "\<And>m. z = int m \<Longrightarrow> P"
352   shows P
353   using assms by (blast dest: nat_0_le sym)
355 lemma nat_eq_iff:
356   "nat w = m \<longleftrightarrow> (if 0 \<le> w then w = int m else m = 0)"
357   by transfer (clarsimp simp add: le_imp_diff_is_add)
359 corollary nat_eq_iff2:
360   "m = nat w \<longleftrightarrow> (if 0 \<le> w then w = int m else m = 0)"
361   using nat_eq_iff [of w m] by auto
363 lemma nat_0 [simp]:
364   "nat 0 = 0"
365   by (simp add: nat_eq_iff)
367 lemma nat_1 [simp]:
368   "nat 1 = Suc 0"
369   by (simp add: nat_eq_iff)
371 lemma nat_numeral [simp]:
372   "nat (numeral k) = numeral k"
373   by (simp add: nat_eq_iff)
375 lemma nat_neg_numeral [simp]:
376   "nat (- numeral k) = 0"
377   by simp
379 lemma nat_2: "nat 2 = Suc (Suc 0)"
380   by simp
382 lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)"
383   by transfer (clarsimp, arith)
385 lemma nat_le_iff: "nat x \<le> n \<longleftrightarrow> x \<le> int n"
386   by transfer (clarsimp simp add: le_diff_conv)
388 lemma nat_mono: "x \<le> y \<Longrightarrow> nat x \<le> nat y"
389   by transfer auto
391 lemma nat_0_iff[simp]: "nat(i::int) = 0 \<longleftrightarrow> i\<le>0"
392   by transfer clarsimp
394 lemma int_eq_iff: "(of_nat m = z) = (m = nat z & 0 \<le> z)"
395 by (auto simp add: nat_eq_iff2)
397 lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)"
398 by (insert zless_nat_conj [of 0], auto)
401   "0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat (z + z') = nat z + nat z'"
402   by transfer clarsimp
404 lemma nat_diff_distrib':
405   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> nat (x - y) = nat x - nat y"
406   by transfer clarsimp
408 lemma nat_diff_distrib:
409   "0 \<le> z' \<Longrightarrow> z' \<le> z \<Longrightarrow> nat (z - z') = nat z - nat z'"
410   by (rule nat_diff_distrib') auto
412 lemma nat_zminus_int [simp]: "nat (- int n) = 0"
413   by transfer simp
415 lemma le_nat_iff:
416   "k \<ge> 0 \<Longrightarrow> n \<le> nat k \<longleftrightarrow> int n \<le> k"
417   by transfer auto
419 lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
420   by transfer (clarsimp simp add: less_diff_conv)
422 context ring_1
423 begin
425 lemma of_nat_nat: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z"
426   by transfer (clarsimp simp add: of_nat_diff)
428 end
430 lemma diff_nat_numeral [simp]:
431   "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
432   by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
435 text {* For termination proofs: *}
436 lemma measure_function_int[measure_function]: "is_measure (nat o abs)" ..
439 subsection{*Lemmas about the Function @{term of_nat} and Orderings*}
441 lemma negative_zless_0: "- (int (Suc n)) < (0 \<Colon> int)"
442 by (simp add: order_less_le del: of_nat_Suc)
444 lemma negative_zless [iff]: "- (int (Suc n)) < int m"
445 by (rule negative_zless_0 [THEN order_less_le_trans], simp)
447 lemma negative_zle_0: "- int n \<le> 0"
448 by (simp add: minus_le_iff)
450 lemma negative_zle [iff]: "- int n \<le> int m"
451 by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff])
453 lemma not_zle_0_negative [simp]: "~ (0 \<le> - (int (Suc n)))"
454 by (subst le_minus_iff, simp del: of_nat_Suc)
456 lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
457   by transfer simp
459 lemma not_int_zless_negative [simp]: "~ (int n < - int m)"
460 by (simp add: linorder_not_less)
462 lemma negative_eq_positive [simp]: "(- int n = of_nat m) = (n = 0 & m = 0)"
463 by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg)
465 lemma zle_iff_zadd: "w \<le> z \<longleftrightarrow> (\<exists>n. z = w + int n)"
466 proof -
467   have "(w \<le> z) = (0 \<le> z - w)"
468     by (simp only: le_diff_eq add_0_left)
469   also have "\<dots> = (\<exists>n. z - w = of_nat n)"
470     by (auto elim: zero_le_imp_eq_int)
471   also have "\<dots> = (\<exists>n. z = w + of_nat n)"
472     by (simp only: algebra_simps)
473   finally show ?thesis .
474 qed
476 lemma zadd_int_left: "int m + (int n + z) = int (m + n) + z"
477 by simp
479 lemma int_Suc0_eq_1: "int (Suc 0) = 1"
480 by simp
482 text{*This version is proved for all ordered rings, not just integers!
483       It is proved here because attribute @{text arith_split} is not available
484       in theory @{text Rings}.
485       But is it really better than just rewriting with @{text abs_if}?*}
486 lemma abs_split [arith_split, no_atp]:
487      "P(abs(a::'a::linordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
488 by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
490 lemma negD: "x < 0 \<Longrightarrow> \<exists>n. x = - (int (Suc n))"
491 apply transfer
492 apply clarsimp
493 apply (rule_tac x="b - Suc a" in exI, arith)
494 done
497 subsection {* Cases and induction *}
499 text{*Now we replace the case analysis rule by a more conventional one:
500 whether an integer is negative or not.*}
502 theorem int_cases [case_names nonneg neg, cases type: int]:
503   "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
504 apply (cases "z < 0")
505 apply (blast dest!: negD)
506 apply (simp add: linorder_not_less del: of_nat_Suc)
507 apply auto
508 apply (blast dest: nat_0_le [THEN sym])
509 done
511 theorem int_of_nat_induct [case_names nonneg neg, induct type: int]:
512      "[|!! n. P (int n);  !!n. P (- (int (Suc n))) |] ==> P z"
513   by (cases z) auto
515 lemma nonneg_int_cases:
516   assumes "0 \<le> k" obtains n where "k = int n"
517   using assms by (rule nonneg_eq_int)
519 lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
520   -- {* Unfold all @{text let}s involving constants *}
521   by (fact Let_numeral) -- {* FIXME drop *}
523 lemma Let_neg_numeral [simp]: "Let (- numeral v) f = f (- numeral v)"
524   -- {* Unfold all @{text let}s involving constants *}
525   by (fact Let_neg_numeral) -- {* FIXME drop *}
527 text {* Unfold @{text min} and @{text max} on numerals. *}
529 lemmas max_number_of [simp] =
530   max_def [of "numeral u" "numeral v"]
531   max_def [of "numeral u" "- numeral v"]
532   max_def [of "- numeral u" "numeral v"]
533   max_def [of "- numeral u" "- numeral v"] for u v
535 lemmas min_number_of [simp] =
536   min_def [of "numeral u" "numeral v"]
537   min_def [of "numeral u" "- numeral v"]
538   min_def [of "- numeral u" "numeral v"]
539   min_def [of "- numeral u" "- numeral v"] for u v
542 subsubsection {* Binary comparisons *}
544 text {* Preliminaries *}
546 lemma even_less_0_iff:
547   "a + a < 0 \<longleftrightarrow> a < (0::'a::linordered_idom)"
548 proof -
549   have "a + a < 0 \<longleftrightarrow> (1+1)*a < 0" by (simp add: distrib_right del: one_add_one)
550   also have "(1+1)*a < 0 \<longleftrightarrow> a < 0"
551     by (simp add: mult_less_0_iff zero_less_two
552                   order_less_not_sym [OF zero_less_two])
553   finally show ?thesis .
554 qed
556 lemma le_imp_0_less:
557   assumes le: "0 \<le> z"
558   shows "(0::int) < 1 + z"
559 proof -
560   have "0 \<le> z" by fact
561   also have "... < z + 1" by (rule less_add_one)
562   also have "... = 1 + z" by (simp add: ac_simps)
563   finally show "0 < 1 + z" .
564 qed
566 lemma odd_less_0_iff:
567   "(1 + z + z < 0) = (z < (0::int))"
568 proof (cases z)
569   case (nonneg n)
571                              le_imp_0_less [THEN order_less_imp_le])
572 next
573   case (neg n)
574   thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1
575     add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric])
576 qed
578 subsubsection {* Comparisons, for Ordered Rings *}
580 lemmas double_eq_0_iff = double_zero
582 lemma odd_nonzero:
583   "1 + z + z \<noteq> (0::int)"
584 proof (cases z)
585   case (nonneg n)
586   have le: "0 \<le> z+z" by (simp add: nonneg add_increasing)
587   thus ?thesis using  le_imp_0_less [OF le]
589 next
590   case (neg n)
591   show ?thesis
592   proof
593     assume eq: "1 + z + z = 0"
594     have "(0::int) < 1 + (int n + int n)"
596     also have "... = - (1 + z + z)"
597       by (simp add: neg add.assoc [symmetric])
598     also have "... = 0" by (simp add: eq)
599     finally have "0<0" ..
600     thus False by blast
601   qed
602 qed
605 subsection {* The Set of Integers *}
607 context ring_1
608 begin
610 definition Ints  :: "'a set" where
611   "Ints = range of_int"
613 notation (xsymbols)
614   Ints  ("\<int>")
616 lemma Ints_of_int [simp]: "of_int z \<in> \<int>"
617   by (simp add: Ints_def)
619 lemma Ints_of_nat [simp]: "of_nat n \<in> \<int>"
620   using Ints_of_int [of "of_nat n"] by simp
622 lemma Ints_0 [simp]: "0 \<in> \<int>"
623   using Ints_of_int [of "0"] by simp
625 lemma Ints_1 [simp]: "1 \<in> \<int>"
626   using Ints_of_int [of "1"] by simp
628 lemma Ints_add [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a + b \<in> \<int>"
629 apply (auto simp add: Ints_def)
630 apply (rule range_eqI)
631 apply (rule of_int_add [symmetric])
632 done
634 lemma Ints_minus [simp]: "a \<in> \<int> \<Longrightarrow> -a \<in> \<int>"
635 apply (auto simp add: Ints_def)
636 apply (rule range_eqI)
637 apply (rule of_int_minus [symmetric])
638 done
640 lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a - b \<in> \<int>"
641 apply (auto simp add: Ints_def)
642 apply (rule range_eqI)
643 apply (rule of_int_diff [symmetric])
644 done
646 lemma Ints_mult [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a * b \<in> \<int>"
647 apply (auto simp add: Ints_def)
648 apply (rule range_eqI)
649 apply (rule of_int_mult [symmetric])
650 done
652 lemma Ints_power [simp]: "a \<in> \<int> \<Longrightarrow> a ^ n \<in> \<int>"
653 by (induct n) simp_all
655 lemma Ints_cases [cases set: Ints]:
656   assumes "q \<in> \<int>"
657   obtains (of_int) z where "q = of_int z"
658   unfolding Ints_def
659 proof -
660   from `q \<in> \<int>` have "q \<in> range of_int" unfolding Ints_def .
661   then obtain z where "q = of_int z" ..
662   then show thesis ..
663 qed
665 lemma Ints_induct [case_names of_int, induct set: Ints]:
666   "q \<in> \<int> \<Longrightarrow> (\<And>z. P (of_int z)) \<Longrightarrow> P q"
667   by (rule Ints_cases) auto
669 end
671 text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
673 lemma Ints_double_eq_0_iff:
674   assumes in_Ints: "a \<in> Ints"
675   shows "(a + a = 0) = (a = (0::'a::ring_char_0))"
676 proof -
677   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
678   then obtain z where a: "a = of_int z" ..
679   show ?thesis
680   proof
681     assume "a = 0"
682     thus "a + a = 0" by simp
683   next
684     assume eq: "a + a = 0"
685     hence "of_int (z + z) = (of_int 0 :: 'a)" by (simp add: a)
686     hence "z + z = 0" by (simp only: of_int_eq_iff)
687     hence "z = 0" by (simp only: double_eq_0_iff)
688     thus "a = 0" by (simp add: a)
689   qed
690 qed
692 lemma Ints_odd_nonzero:
693   assumes in_Ints: "a \<in> Ints"
694   shows "1 + a + a \<noteq> (0::'a::ring_char_0)"
695 proof -
696   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
697   then obtain z where a: "a = of_int z" ..
698   show ?thesis
699   proof
700     assume eq: "1 + a + a = 0"
701     hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
702     hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
703     with odd_nonzero show False by blast
704   qed
705 qed
707 lemma Nats_numeral [simp]: "numeral w \<in> Nats"
708   using of_nat_in_Nats [of "numeral w"] by simp
710 lemma Ints_odd_less_0:
711   assumes in_Ints: "a \<in> Ints"
712   shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))"
713 proof -
714   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
715   then obtain z where a: "a = of_int z" ..
716   hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
717     by (simp add: a)
718   also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0_iff)
719   also have "... = (a < 0)" by (simp add: a)
720   finally show ?thesis .
721 qed
724 subsection {* @{term setsum} and @{term setprod} *}
726 lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
727   apply (cases "finite A")
728   apply (erule finite_induct, auto)
729   done
731 lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
732   apply (cases "finite A")
733   apply (erule finite_induct, auto)
734   done
736 lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
737   apply (cases "finite A")
738   apply (erule finite_induct, auto simp add: of_nat_mult)
739   done
741 lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
742   apply (cases "finite A")
743   apply (erule finite_induct, auto)
744   done
746 lemmas int_setsum = of_nat_setsum [where 'a=int]
747 lemmas int_setprod = of_nat_setprod [where 'a=int]
750 text {* Legacy theorems *}
752 lemmas zle_int = of_nat_le_iff [where 'a=int]
753 lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
754 lemmas numeral_1_eq_1 = numeral_One
756 subsection {* Setting up simplification procedures *}
758 lemmas of_int_simps =
759   of_int_0 of_int_1 of_int_add of_int_mult
761 lemmas int_arith_rules =
762   numeral_One more_arith_simps of_nat_simps of_int_simps
764 ML_file "Tools/int_arith.ML"
765 declaration {* K Int_Arith.setup *}
767 simproc_setup fast_arith ("(m::'a::linordered_idom) < n" |
768   "(m::'a::linordered_idom) <= n" |
769   "(m::'a::linordered_idom) = n") =
770   {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *}
773 subsection{*More Inequality Reasoning*}
775 lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
776 by arith
778 lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
779 by arith
781 lemma zle_diff1_eq [simp]: "(w \<le> z - (1::int)) = (w<z)"
782 by arith
784 lemma zle_add1_eq_le [simp]: "(w < z + (1::int)) = (w\<le>z)"
785 by arith
787 lemma int_one_le_iff_zero_less: "((1::int) \<le> z) = (0 < z)"
788 by arith
791 subsection{*The functions @{term nat} and @{term int}*}
793 text{*Simplify the term @{term "w + - z"}*}
795 lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
796 apply (insert zless_nat_conj [of 1 z])
797 apply auto
798 done
800 text{*This simplifies expressions of the form @{term "int n = z"} where
801       z is an integer literal.*}
802 lemmas int_eq_iff_numeral [simp] = int_eq_iff [of _ "numeral v"] for v
804 lemma split_nat [arith_split]:
805   "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
806   (is "?P = (?L & ?R)")
807 proof (cases "i < 0")
808   case True thus ?thesis by auto
809 next
810   case False
811   have "?P = ?L"
812   proof
813     assume ?P thus ?L using False by clarsimp
814   next
815     assume ?L thus ?P using False by simp
816   qed
817   with False show ?thesis by simp
818 qed
820 context ring_1
821 begin
823 lemma of_int_of_nat [nitpick_simp]:
824   "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))"
825 proof (cases "k < 0")
826   case True then have "0 \<le> - k" by simp
827   then have "of_nat (nat (- k)) = of_int (- k)" by (rule of_nat_nat)
828   with True show ?thesis by simp
829 next
830   case False then show ?thesis by (simp add: not_less of_nat_nat)
831 qed
833 end
835 lemma nat_mult_distrib:
836   fixes z z' :: int
837   assumes "0 \<le> z"
838   shows "nat (z * z') = nat z * nat z'"
839 proof (cases "0 \<le> z'")
840   case False with assms have "z * z' \<le> 0"
841     by (simp add: not_le mult_le_0_iff)
842   then have "nat (z * z') = 0" by simp
843   moreover from False have "nat z' = 0" by simp
844   ultimately show ?thesis by simp
845 next
846   case True with assms have ge_0: "z * z' \<ge> 0" by (simp add: zero_le_mult_iff)
847   show ?thesis
848     by (rule injD [of "of_nat :: nat \<Rightarrow> int", OF inj_of_nat])
849       (simp only: of_nat_mult of_nat_nat [OF True]
850          of_nat_nat [OF assms] of_nat_nat [OF ge_0], simp)
851 qed
853 lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"
854 apply (rule trans)
855 apply (rule_tac  nat_mult_distrib, auto)
856 done
858 lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
859 apply (cases "z=0 | w=0")
860 apply (auto simp add: abs_if nat_mult_distrib [symmetric]
861                       nat_mult_distrib_neg [symmetric] mult_less_0_iff)
862 done
864 lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
865 apply (rule sym)
866 apply (simp add: nat_eq_iff)
867 done
869 lemma diff_nat_eq_if:
870      "nat z - nat z' =
871         (if z' < 0 then nat z
872          else let d = z-z' in
873               if d < 0 then 0 else nat d)"
874 by (simp add: Let_def nat_diff_distrib [symmetric])
876 lemma nat_numeral_diff_1 [simp]:
877   "numeral v - (1::nat) = nat (numeral v - 1)"
878   using diff_nat_numeral [of v Num.One] by simp
881 subsection "Induction principles for int"
883 text{*Well-founded segments of the integers*}
885 definition
886   int_ge_less_than  ::  "int => (int * int) set"
887 where
888   "int_ge_less_than d = {(z',z). d \<le> z' & z' < z}"
890 theorem wf_int_ge_less_than: "wf (int_ge_less_than d)"
891 proof -
892   have "int_ge_less_than d \<subseteq> measure (%z. nat (z-d))"
893     by (auto simp add: int_ge_less_than_def)
894   thus ?thesis
895     by (rule wf_subset [OF wf_measure])
896 qed
898 text{*This variant looks odd, but is typical of the relations suggested
899 by RankFinder.*}
901 definition
902   int_ge_less_than2 ::  "int => (int * int) set"
903 where
904   "int_ge_less_than2 d = {(z',z). d \<le> z & z' < z}"
906 theorem wf_int_ge_less_than2: "wf (int_ge_less_than2 d)"
907 proof -
908   have "int_ge_less_than2 d \<subseteq> measure (%z. nat (1+z-d))"
909     by (auto simp add: int_ge_less_than2_def)
910   thus ?thesis
911     by (rule wf_subset [OF wf_measure])
912 qed
914 (* `set:int': dummy construction *)
915 theorem int_ge_induct [case_names base step, induct set: int]:
916   fixes i :: int
917   assumes ge: "k \<le> i" and
918     base: "P k" and
919     step: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
920   shows "P i"
921 proof -
922   { fix n
923     have "\<And>i::int. n = nat (i - k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i"
924     proof (induct n)
925       case 0
926       hence "i = k" by arith
927       thus "P i" using base by simp
928     next
929       case (Suc n)
930       then have "n = nat((i - 1) - k)" by arith
931       moreover
932       have ki1: "k \<le> i - 1" using Suc.prems by arith
933       ultimately
934       have "P (i - 1)" by (rule Suc.hyps)
935       from step [OF ki1 this] show ?case by simp
936     qed
937   }
938   with ge show ?thesis by fast
939 qed
941 (* `set:int': dummy construction *)
942 theorem int_gr_induct [case_names base step, induct set: int]:
943   assumes gr: "k < (i::int)" and
944         base: "P(k+1)" and
945         step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
946   shows "P i"
947 apply(rule int_ge_induct[of "k + 1"])
948   using gr apply arith
949  apply(rule base)
950 apply (rule step, simp+)
951 done
953 theorem int_le_induct [consumes 1, case_names base step]:
954   assumes le: "i \<le> (k::int)" and
955         base: "P(k)" and
956         step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
957   shows "P i"
958 proof -
959   { fix n
960     have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i"
961     proof (induct n)
962       case 0
963       hence "i = k" by arith
964       thus "P i" using base by simp
965     next
966       case (Suc n)
967       hence "n = nat (k - (i + 1))" by arith
968       moreover
969       have ki1: "i + 1 \<le> k" using Suc.prems by arith
970       ultimately
971       have "P (i + 1)" by(rule Suc.hyps)
972       from step[OF ki1 this] show ?case by simp
973     qed
974   }
975   with le show ?thesis by fast
976 qed
978 theorem int_less_induct [consumes 1, case_names base step]:
979   assumes less: "(i::int) < k" and
980         base: "P(k - 1)" and
981         step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
982   shows "P i"
983 apply(rule int_le_induct[of _ "k - 1"])
984   using less apply arith
985  apply(rule base)
986 apply (rule step, simp+)
987 done
989 theorem int_induct [case_names base step1 step2]:
990   fixes k :: int
991   assumes base: "P k"
992     and step1: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
993     and step2: "\<And>i. k \<ge> i \<Longrightarrow> P i \<Longrightarrow> P (i - 1)"
994   shows "P i"
995 proof -
996   have "i \<le> k \<or> i \<ge> k" by arith
997   then show ?thesis
998   proof
999     assume "i \<ge> k"
1000     then show ?thesis using base
1001       by (rule int_ge_induct) (fact step1)
1002   next
1003     assume "i \<le> k"
1004     then show ?thesis using base
1005       by (rule int_le_induct) (fact step2)
1006   qed
1007 qed
1009 subsection{*Intermediate value theorems*}
1011 lemma int_val_lemma:
1012      "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->
1013       f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
1014 unfolding One_nat_def
1015 apply (induct n)
1016 apply simp
1017 apply (intro strip)
1018 apply (erule impE, simp)
1019 apply (erule_tac x = n in allE, simp)
1020 apply (case_tac "k = f (Suc n)")
1021 apply force
1022 apply (erule impE)
1023  apply (simp add: abs_if split add: split_if_asm)
1024 apply (blast intro: le_SucI)
1025 done
1027 lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
1029 lemma nat_intermed_int_val:
1030      "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;
1031          f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
1032 apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k
1033        in int_val_lemma)
1034 unfolding One_nat_def
1035 apply simp
1036 apply (erule exE)
1037 apply (rule_tac x = "i+m" in exI, arith)
1038 done
1041 subsection{*Products and 1, by T. M. Rasmussen*}
1043 lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))"
1044 by arith
1046 lemma abs_zmult_eq_1:
1047   assumes mn: "\<bar>m * n\<bar> = 1"
1048   shows "\<bar>m\<bar> = (1::int)"
1049 proof -
1050   have 0: "m \<noteq> 0 & n \<noteq> 0" using mn
1051     by auto
1052   have "~ (2 \<le> \<bar>m\<bar>)"
1053   proof
1054     assume "2 \<le> \<bar>m\<bar>"
1055     hence "2*\<bar>n\<bar> \<le> \<bar>m\<bar>*\<bar>n\<bar>"
1056       by (simp add: mult_mono 0)
1057     also have "... = \<bar>m*n\<bar>"
1058       by (simp add: abs_mult)
1059     also have "... = 1"
1060       by (simp add: mn)
1061     finally have "2*\<bar>n\<bar> \<le> 1" .
1062     thus "False" using 0
1063       by arith
1064   qed
1065   thus ?thesis using 0
1066     by auto
1067 qed
1069 lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1"
1070 by (insert abs_zmult_eq_1 [of m n], arith)
1072 lemma pos_zmult_eq_1_iff:
1073   assumes "0 < (m::int)" shows "(m * n = 1) = (m = 1 & n = 1)"
1074 proof -
1075   from assms have "m * n = 1 ==> m = 1" by (auto dest: pos_zmult_eq_1_iff_lemma)
1076   thus ?thesis by (auto dest: pos_zmult_eq_1_iff_lemma)
1077 qed
1079 lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
1080 apply (rule iffI)
1081  apply (frule pos_zmult_eq_1_iff_lemma)
1082  apply (simp add: mult.commute [of m])
1083  apply (frule pos_zmult_eq_1_iff_lemma, auto)
1084 done
1086 lemma infinite_UNIV_int: "\<not> finite (UNIV::int set)"
1087 proof
1088   assume "finite (UNIV::int set)"
1089   moreover have "inj (\<lambda>i\<Colon>int. 2 * i)"
1090     by (rule injI) simp
1091   ultimately have "surj (\<lambda>i\<Colon>int. 2 * i)"
1092     by (rule finite_UNIV_inj_surj)
1093   then obtain i :: int where "1 = 2 * i" by (rule surjE)
1094   then show False by (simp add: pos_zmult_eq_1_iff)
1095 qed
1098 subsection {* Further theorems on numerals *}
1100 subsubsection{*Special Simplification for Constants*}
1102 text{*These distributive laws move literals inside sums and differences.*}
1104 lemmas distrib_right_numeral [simp] = distrib_right [of _ _ "numeral v"] for v
1105 lemmas distrib_left_numeral [simp] = distrib_left [of "numeral v"] for v
1106 lemmas left_diff_distrib_numeral [simp] = left_diff_distrib [of _ _ "numeral v"] for v
1107 lemmas right_diff_distrib_numeral [simp] = right_diff_distrib [of "numeral v"] for v
1109 text{*These are actually for fields, like real: but where else to put them?*}
1111 lemmas zero_less_divide_iff_numeral [simp, no_atp] = zero_less_divide_iff [of "numeral w"] for w
1112 lemmas divide_less_0_iff_numeral [simp, no_atp] = divide_less_0_iff [of "numeral w"] for w
1113 lemmas zero_le_divide_iff_numeral [simp, no_atp] = zero_le_divide_iff [of "numeral w"] for w
1114 lemmas divide_le_0_iff_numeral [simp, no_atp] = divide_le_0_iff [of "numeral w"] for w
1117 text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}.  It looks
1118   strange, but then other simprocs simplify the quotient.*}
1120 lemmas inverse_eq_divide_numeral [simp] =
1121   inverse_eq_divide [of "numeral w"] for w
1123 lemmas inverse_eq_divide_neg_numeral [simp] =
1124   inverse_eq_divide [of "- numeral w"] for w
1126 text {*These laws simplify inequalities, moving unary minus from a term
1127 into the literal.*}
1129 lemmas equation_minus_iff_numeral [no_atp] =
1130   equation_minus_iff [of "numeral v"] for v
1132 lemmas minus_equation_iff_numeral [no_atp] =
1133   minus_equation_iff [of _ "numeral v"] for v
1135 lemmas le_minus_iff_numeral [no_atp] =
1136   le_minus_iff [of "numeral v"] for v
1138 lemmas minus_le_iff_numeral [no_atp] =
1139   minus_le_iff [of _ "numeral v"] for v
1141 lemmas less_minus_iff_numeral [no_atp] =
1142   less_minus_iff [of "numeral v"] for v
1144 lemmas minus_less_iff_numeral [no_atp] =
1145   minus_less_iff [of _ "numeral v"] for v
1147 -- {* FIXME maybe simproc *}
1150 text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
1152 lemmas mult_less_cancel_left_numeral [simp, no_atp] = mult_less_cancel_left [of "numeral v"] for v
1153 lemmas mult_less_cancel_right_numeral [simp, no_atp] = mult_less_cancel_right [of _ "numeral v"] for v
1154 lemmas mult_le_cancel_left_numeral [simp, no_atp] = mult_le_cancel_left [of "numeral v"] for v
1155 lemmas mult_le_cancel_right_numeral [simp, no_atp] = mult_le_cancel_right [of _ "numeral v"] for v
1158 text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
1160 lemmas le_divide_eq_numeral1 [simp] =
1161   pos_le_divide_eq [of "numeral w", OF zero_less_numeral]
1162   neg_le_divide_eq [of "- numeral w", OF neg_numeral_less_zero] for w
1164 lemmas divide_le_eq_numeral1 [simp] =
1165   pos_divide_le_eq [of "numeral w", OF zero_less_numeral]
1166   neg_divide_le_eq [of "- numeral w", OF neg_numeral_less_zero] for w
1168 lemmas less_divide_eq_numeral1 [simp] =
1169   pos_less_divide_eq [of "numeral w", OF zero_less_numeral]
1170   neg_less_divide_eq [of "- numeral w", OF neg_numeral_less_zero] for w
1172 lemmas divide_less_eq_numeral1 [simp] =
1173   pos_divide_less_eq [of "numeral w", OF zero_less_numeral]
1174   neg_divide_less_eq [of "- numeral w", OF neg_numeral_less_zero] for w
1176 lemmas eq_divide_eq_numeral1 [simp] =
1177   eq_divide_eq [of _ _ "numeral w"]
1178   eq_divide_eq [of _ _ "- numeral w"] for w
1180 lemmas divide_eq_eq_numeral1 [simp] =
1181   divide_eq_eq [of _ "numeral w"]
1182   divide_eq_eq [of _ "- numeral w"] for w
1185 subsubsection{*Optional Simplification Rules Involving Constants*}
1187 text{*Simplify quotients that are compared with a literal constant.*}
1189 lemmas le_divide_eq_numeral =
1190   le_divide_eq [of "numeral w"]
1191   le_divide_eq [of "- numeral w"] for w
1193 lemmas divide_le_eq_numeral =
1194   divide_le_eq [of _ _ "numeral w"]
1195   divide_le_eq [of _ _ "- numeral w"] for w
1197 lemmas less_divide_eq_numeral =
1198   less_divide_eq [of "numeral w"]
1199   less_divide_eq [of "- numeral w"] for w
1201 lemmas divide_less_eq_numeral =
1202   divide_less_eq [of _ _ "numeral w"]
1203   divide_less_eq [of _ _ "- numeral w"] for w
1205 lemmas eq_divide_eq_numeral =
1206   eq_divide_eq [of "numeral w"]
1207   eq_divide_eq [of "- numeral w"] for w
1209 lemmas divide_eq_eq_numeral =
1210   divide_eq_eq [of _ _ "numeral w"]
1211   divide_eq_eq [of _ _ "- numeral w"] for w
1214 text{*Not good as automatic simprules because they cause case splits.*}
1215 lemmas divide_const_simps =
1216   le_divide_eq_numeral divide_le_eq_numeral less_divide_eq_numeral
1217   divide_less_eq_numeral eq_divide_eq_numeral divide_eq_eq_numeral
1218   le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
1221 subsection {* The divides relation *}
1223 lemma zdvd_antisym_nonneg:
1224     "0 <= m ==> 0 <= n ==> m dvd n ==> n dvd m ==> m = (n::int)"
1225   apply (simp add: dvd_def, auto)
1226   apply (auto simp add: mult.assoc zero_le_mult_iff zmult_eq_1_iff)
1227   done
1229 lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a"
1230   shows "\<bar>a\<bar> = \<bar>b\<bar>"
1231 proof cases
1232   assume "a = 0" with assms show ?thesis by simp
1233 next
1234   assume "a \<noteq> 0"
1235   from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast
1236   from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast
1237   from k k' have "a = a*k*k'" by simp
1238   with mult_cancel_left1[where c="a" and b="k*k'"]
1239   have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult.assoc)
1240   hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff)
1241   thus ?thesis using k k' by auto
1242 qed
1244 lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
1245   using dvd_add_right_iff [of k "- n" m] by simp
1247 lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
1248   using dvd_add_times_triv_right_iff [of k n m] by (simp add: ac_simps)
1250 lemma dvd_imp_le_int:
1251   fixes d i :: int
1252   assumes "i \<noteq> 0" and "d dvd i"
1253   shows "\<bar>d\<bar> \<le> \<bar>i\<bar>"
1254 proof -
1255   from `d dvd i` obtain k where "i = d * k" ..
1256   with `i \<noteq> 0` have "k \<noteq> 0" by auto
1257   then have "1 \<le> \<bar>k\<bar>" and "0 \<le> \<bar>d\<bar>" by auto
1258   then have "\<bar>d\<bar> * 1 \<le> \<bar>d\<bar> * \<bar>k\<bar>" by (rule mult_left_mono)
1259   with `i = d * k` show ?thesis by (simp add: abs_mult)
1260 qed
1262 lemma zdvd_not_zless:
1263   fixes m n :: int
1264   assumes "0 < m" and "m < n"
1265   shows "\<not> n dvd m"
1266 proof
1267   from assms have "0 < n" by auto
1268   assume "n dvd m" then obtain k where k: "m = n * k" ..
1269   with `0 < m` have "0 < n * k" by auto
1270   with `0 < n` have "0 < k" by (simp add: zero_less_mult_iff)
1271   with k `0 < n` `m < n` have "n * k < n * 1" by simp
1272   with `0 < n` `0 < k` show False unfolding mult_less_cancel_left by auto
1273 qed
1275 lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)"
1276   shows "m dvd n"
1277 proof-
1278   from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast
1279   {assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp
1280     with h have False by (simp add: mult.assoc)}
1281   hence "n = m * h" by blast
1282   thus ?thesis by simp
1283 qed
1285 theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
1286 proof -
1287   have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"
1288   proof -
1289     fix k
1290     assume A: "int y = int x * k"
1291     then show "x dvd y"
1292     proof (cases k)
1293       case (nonneg n)
1294       with A have "y = x * n" by (simp add: of_nat_mult [symmetric])
1295       then show ?thesis ..
1296     next
1297       case (neg n)
1298       with A have "int y = int x * (- int (Suc n))" by simp
1299       also have "\<dots> = - (int x * int (Suc n))" by (simp only: mult_minus_right)
1300       also have "\<dots> = - int (x * Suc n)" by (simp only: of_nat_mult [symmetric])
1301       finally have "- int (x * Suc n) = int y" ..
1302       then show ?thesis by (simp only: negative_eq_positive) auto
1303     qed
1304   qed
1305   then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left of_nat_mult)
1306 qed
1308 lemma zdvd1_eq[simp]: "(x::int) dvd 1 = (\<bar>x\<bar> = 1)"
1309 proof
1310   assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp
1311   hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
1312   hence "nat \<bar>x\<bar> = 1"  by simp
1313   thus "\<bar>x\<bar> = 1" by (cases "x < 0") auto
1314 next
1315   assume "\<bar>x\<bar>=1"
1316   then have "x = 1 \<or> x = -1" by auto
1317   then show "x dvd 1" by (auto intro: dvdI)
1318 qed
1320 lemma zdvd_mult_cancel1:
1321   assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
1322 proof
1323   assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m"
1324     by (cases "n >0") (auto simp add: minus_equation_iff)
1325 next
1326   assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
1327   from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
1328 qed
1330 lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
1331   unfolding zdvd_int by (cases "z \<ge> 0") simp_all
1333 lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
1334   unfolding zdvd_int by (cases "z \<ge> 0") simp_all
1336 lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
1337   by (auto simp add: dvd_int_iff)
1339 lemma eq_nat_nat_iff:
1340   "0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat z = nat z' \<longleftrightarrow> z = z'"
1341   by (auto elim!: nonneg_eq_int)
1343 lemma nat_power_eq:
1344   "0 \<le> z \<Longrightarrow> nat (z ^ n) = nat z ^ n"
1345   by (induct n) (simp_all add: nat_mult_distrib)
1347 lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
1348   apply (cases n)
1349   apply (auto simp add: dvd_int_iff)
1350   apply (cases z)
1351   apply (auto simp add: dvd_imp_le)
1352   done
1354 lemma zdvd_period:
1355   fixes a d :: int
1356   assumes "a dvd d"
1357   shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)"
1358 proof -
1359   from assms obtain k where "d = a * k" by (rule dvdE)
1360   show ?thesis
1361   proof
1362     assume "a dvd (x + t)"
1363     then obtain l where "x + t = a * l" by (rule dvdE)
1364     then have "x = a * l - t" by simp
1365     with `d = a * k` show "a dvd x + c * d + t" by simp
1366   next
1367     assume "a dvd x + c * d + t"
1368     then obtain l where "x + c * d + t = a * l" by (rule dvdE)
1369     then have "x = a * l - c * d - t" by simp
1370     with `d = a * k` show "a dvd (x + t)" by simp
1371   qed
1372 qed
1375 subsection {* Finiteness of intervals *}
1377 lemma finite_interval_int1 [iff]: "finite {i :: int. a <= i & i <= b}"
1378 proof (cases "a <= b")
1379   case True
1380   from this show ?thesis
1381   proof (induct b rule: int_ge_induct)
1382     case base
1383     have "{i. a <= i & i <= a} = {a}" by auto
1384     from this show ?case by simp
1385   next
1386     case (step b)
1387     from this have "{i. a <= i & i <= b + 1} = {i. a <= i & i <= b} \<union> {b + 1}" by auto
1388     from this step show ?case by simp
1389   qed
1390 next
1391   case False from this show ?thesis
1392     by (metis (lifting, no_types) Collect_empty_eq finite.emptyI order_trans)
1393 qed
1395 lemma finite_interval_int2 [iff]: "finite {i :: int. a <= i & i < b}"
1396 by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
1398 lemma finite_interval_int3 [iff]: "finite {i :: int. a < i & i <= b}"
1399 by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
1401 lemma finite_interval_int4 [iff]: "finite {i :: int. a < i & i < b}"
1402 by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
1405 subsection {* Configuration of the code generator *}
1407 text {* Constructors *}
1409 definition Pos :: "num \<Rightarrow> int" where
1410   [simp, code_abbrev]: "Pos = numeral"
1412 definition Neg :: "num \<Rightarrow> int" where
1413   [simp, code_abbrev]: "Neg n = - (Pos n)"
1415 code_datatype "0::int" Pos Neg
1418 text {* Auxiliary operations *}
1420 definition dup :: "int \<Rightarrow> int" where
1421   [simp]: "dup k = k + k"
1423 lemma dup_code [code]:
1424   "dup 0 = 0"
1425   "dup (Pos n) = Pos (Num.Bit0 n)"
1426   "dup (Neg n) = Neg (Num.Bit0 n)"
1427   unfolding Pos_def Neg_def
1428   by (simp_all add: numeral_Bit0)
1430 definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
1431   [simp]: "sub m n = numeral m - numeral n"
1433 lemma sub_code [code]:
1434   "sub Num.One Num.One = 0"
1435   "sub (Num.Bit0 m) Num.One = Pos (Num.BitM m)"
1436   "sub (Num.Bit1 m) Num.One = Pos (Num.Bit0 m)"
1437   "sub Num.One (Num.Bit0 n) = Neg (Num.BitM n)"
1438   "sub Num.One (Num.Bit1 n) = Neg (Num.Bit0 n)"
1439   "sub (Num.Bit0 m) (Num.Bit0 n) = dup (sub m n)"
1440   "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)"
1441   "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1"
1442   "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1"
1443   apply (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def numeral_BitM)
1444   apply (simp_all only: algebra_simps minus_diff_eq)
1445   apply (simp_all only: add.commute [of _ "- (numeral n + numeral n)"])
1446   apply (simp_all only: minus_add add.assoc left_minus)
1447   done
1449 text {* Implementations *}
1451 lemma one_int_code [code, code_unfold]:
1452   "1 = Pos Num.One"
1453   by simp
1455 lemma plus_int_code [code]:
1456   "k + 0 = (k::int)"
1457   "0 + l = (l::int)"
1458   "Pos m + Pos n = Pos (m + n)"
1459   "Pos m + Neg n = sub m n"
1460   "Neg m + Pos n = sub n m"
1461   "Neg m + Neg n = Neg (m + n)"
1462   by simp_all
1464 lemma uminus_int_code [code]:
1465   "uminus 0 = (0::int)"
1466   "uminus (Pos m) = Neg m"
1467   "uminus (Neg m) = Pos m"
1468   by simp_all
1470 lemma minus_int_code [code]:
1471   "k - 0 = (k::int)"
1472   "0 - l = uminus (l::int)"
1473   "Pos m - Pos n = sub m n"
1474   "Pos m - Neg n = Pos (m + n)"
1475   "Neg m - Pos n = Neg (m + n)"
1476   "Neg m - Neg n = sub n m"
1477   by simp_all
1479 lemma times_int_code [code]:
1480   "k * 0 = (0::int)"
1481   "0 * l = (0::int)"
1482   "Pos m * Pos n = Pos (m * n)"
1483   "Pos m * Neg n = Neg (m * n)"
1484   "Neg m * Pos n = Neg (m * n)"
1485   "Neg m * Neg n = Pos (m * n)"
1486   by simp_all
1488 instantiation int :: equal
1489 begin
1491 definition
1492   "HOL.equal k l \<longleftrightarrow> k = (l::int)"
1494 instance by default (rule equal_int_def)
1496 end
1498 lemma equal_int_code [code]:
1499   "HOL.equal 0 (0::int) \<longleftrightarrow> True"
1500   "HOL.equal 0 (Pos l) \<longleftrightarrow> False"
1501   "HOL.equal 0 (Neg l) \<longleftrightarrow> False"
1502   "HOL.equal (Pos k) 0 \<longleftrightarrow> False"
1503   "HOL.equal (Pos k) (Pos l) \<longleftrightarrow> HOL.equal k l"
1504   "HOL.equal (Pos k) (Neg l) \<longleftrightarrow> False"
1505   "HOL.equal (Neg k) 0 \<longleftrightarrow> False"
1506   "HOL.equal (Neg k) (Pos l) \<longleftrightarrow> False"
1507   "HOL.equal (Neg k) (Neg l) \<longleftrightarrow> HOL.equal k l"
1508   by (auto simp add: equal)
1510 lemma equal_int_refl [code nbe]:
1511   "HOL.equal (k::int) k \<longleftrightarrow> True"
1512   by (fact equal_refl)
1514 lemma less_eq_int_code [code]:
1515   "0 \<le> (0::int) \<longleftrightarrow> True"
1516   "0 \<le> Pos l \<longleftrightarrow> True"
1517   "0 \<le> Neg l \<longleftrightarrow> False"
1518   "Pos k \<le> 0 \<longleftrightarrow> False"
1519   "Pos k \<le> Pos l \<longleftrightarrow> k \<le> l"
1520   "Pos k \<le> Neg l \<longleftrightarrow> False"
1521   "Neg k \<le> 0 \<longleftrightarrow> True"
1522   "Neg k \<le> Pos l \<longleftrightarrow> True"
1523   "Neg k \<le> Neg l \<longleftrightarrow> l \<le> k"
1524   by simp_all
1526 lemma less_int_code [code]:
1527   "0 < (0::int) \<longleftrightarrow> False"
1528   "0 < Pos l \<longleftrightarrow> True"
1529   "0 < Neg l \<longleftrightarrow> False"
1530   "Pos k < 0 \<longleftrightarrow> False"
1531   "Pos k < Pos l \<longleftrightarrow> k < l"
1532   "Pos k < Neg l \<longleftrightarrow> False"
1533   "Neg k < 0 \<longleftrightarrow> True"
1534   "Neg k < Pos l \<longleftrightarrow> True"
1535   "Neg k < Neg l \<longleftrightarrow> l < k"
1536   by simp_all
1538 lemma nat_code [code]:
1539   "nat (Int.Neg k) = 0"
1540   "nat 0 = 0"
1541   "nat (Int.Pos k) = nat_of_num k"
1542   by (simp_all add: nat_of_num_numeral)
1544 lemma (in ring_1) of_int_code [code]:
1545   "of_int (Int.Neg k) = - numeral k"
1546   "of_int 0 = 0"
1547   "of_int (Int.Pos k) = numeral k"
1548   by simp_all
1551 text {* Serializer setup *}
1553 code_identifier
1554   code_module Int \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
1556 quickcheck_params [default_type = int]
1558 hide_const (open) Pos Neg sub dup
1561 subsection {* Legacy theorems *}
1563 lemmas inj_int = inj_of_nat [where 'a=int]
1564 lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
1565 lemmas int_mult = of_nat_mult [where 'a=int]
1566 lemmas zmult_int = of_nat_mult [where 'a=int, symmetric]
1567 lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="n"] for n
1568 lemmas zless_int = of_nat_less_iff [where 'a=int]
1569 lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="k"] for k
1570 lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int]
1571 lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
1572 lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="n"] for n
1573 lemmas int_0 = of_nat_0 [where 'a=int]
1574 lemmas int_1 = of_nat_1 [where 'a=int]
1575 lemmas int_Suc = of_nat_Suc [where 'a=int]
1576 lemmas int_numeral = of_nat_numeral [where 'a=int]
1577 lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m"] for m
1578 lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
1579 lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
1580 lemmas zpower_numeral_even = power_numeral_even [where 'a=int]
1581 lemmas zpower_numeral_odd = power_numeral_odd [where 'a=int]
1583 lemma zpower_zpower:
1584   "(x ^ y) ^ z = (x ^ (y * z)::int)"
1585   by (rule power_mult [symmetric])
1587 lemma int_power:
1588   "int (m ^ n) = int m ^ n"
1589   by (fact of_nat_power)
1591 lemmas zpower_int = int_power [symmetric]
1593 text {* De-register @{text "int"} as a quotient type: *}
1595 lifting_update int.lifting
1596 lifting_forget int.lifting
1598 end