src/HOL/Int.thy
 author wenzelm Wed Sep 09 20:57:21 2015 +0200 (2015-09-09) changeset 61144 5e94dfead1c2 parent 61076 bdc1e2f0a86a child 61169 4de9ff3ea29a permissions -rw-r--r--
simplified simproc programming interfaces;
1 (*  Title:      HOL/Int.thy
2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3     Author:     Tobias Nipkow, Florian Haftmann, TU Muenchen
4 *)
6 section \<open>The Integers as Equivalence Classes over Pairs of Natural Numbers\<close>
8 theory Int
9 imports Equiv_Relations Power Quotient Fun_Def
10 begin
12 subsection \<open>Definition of integers as a quotient type\<close>
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 \<open>Integers form a commutative ring\<close>
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 \<open>Integers are totally ordered\<close>
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 :: int \<Rightarrow> int \<Rightarrow> int) = min"
112 definition
113   "(sup :: 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 \<open>Ordering properties of arithmetic operations\<close>
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\<open>Strict Monotonicity of Multiplication\<close>
132 text\<open>strict, in 1st argument; proof is by induction on k>0\<close>
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\<open>The integers form an ordered integral domain\<close>
160 instantiation int :: linordered_idom
161 begin
163 definition
164   zabs_def: "\<bar>i::int\<bar> = (if i < 0 then - i else i)"
166 definition
167   zsgn_def: "sgn (i::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::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::int) \<le> z"
182   by transfer clarsimp
185   "(w :: 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 \<open>Embedding of the Integers into any @{text ring_1}: @{text of_int}\<close>
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\<open>Collapse nested embeddings\<close>
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\<open>Special cases where either operand is zero\<close>
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\<open>Every @{text linordered_idom} has characteristic zero.\<close>
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 \<open>Magnitude of an Integer, as a Natural Number: @{text nat}\<close>
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\<open>An alternative condition is @{term "0 \<le> w"}\<close>
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 \<open>For termination proofs:\<close>
436 lemma measure_function_int[measure_function]: "is_measure (nat o abs)" ..
439 subsection\<open>Lemmas about the Function @{term of_nat} and Orderings\<close>
441 lemma negative_zless_0: "- (int (Suc n)) < (0 :: 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\<open>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}?\<close>
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
496 subsection \<open>Cases and induction\<close>
498 text\<open>Now we replace the case analysis rule by a more conventional one:
499 whether an integer is negative or not.\<close>
501 text\<open>This version is symmetric in the two subgoals.\<close>
502 theorem int_cases2 [case_names nonneg nonpos, cases type: int]:
503   "\<lbrakk>!! n. z = int n \<Longrightarrow> P;  !! n. z = - (int n) \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
504 apply (cases "z < 0")
505 apply (auto simp add: linorder_not_less dest!: negD nat_0_le [THEN sym])
506 done
508 text\<open>This is the default, with a negative case.\<close>
509 theorem int_cases [case_names nonneg neg, cases type: int]:
510   "[|!! n. z = int n ==> P;  !! n. z = - (int (Suc n)) ==> P |] ==> P"
511 apply (cases "z < 0")
512 apply (blast dest!: negD)
513 apply (simp add: linorder_not_less del: of_nat_Suc)
514 apply auto
515 apply (blast dest: nat_0_le [THEN sym])
516 done
518 lemma int_cases3 [case_names zero pos neg]:
519   fixes k :: int
520   assumes "k = 0 \<Longrightarrow> P" and "\<And>n. k = int n \<Longrightarrow> n > 0 \<Longrightarrow> P"
521     and "\<And>n. k = - int n \<Longrightarrow> n > 0 \<Longrightarrow> P"
522   shows "P"
523 proof (cases k "0::int" rule: linorder_cases)
524   case equal with assms(1) show P by simp
525 next
526   case greater
527   then have "nat k > 0" by simp
528   moreover from this have "k = int (nat k)" by auto
529   ultimately show P using assms(2) by blast
530 next
531   case less
532   then have "nat (- k) > 0" by simp
533   moreover from this have "k = - int (nat (- k))" by auto
534   ultimately show P using assms(3) by blast
535 qed
537 theorem int_of_nat_induct [case_names nonneg neg, induct type: int]:
538      "[|!! n. P (int n);  !!n. P (- (int (Suc n))) |] ==> P z"
539   by (cases z) auto
541 lemma nonneg_int_cases:
542   assumes "0 \<le> k" obtains n where "k = int n"
543   using assms by (rule nonneg_eq_int)
545 lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
546   -- \<open>Unfold all @{text let}s involving constants\<close>
547   by (fact Let_numeral) -- \<open>FIXME drop\<close>
549 lemma Let_neg_numeral [simp]: "Let (- numeral v) f = f (- numeral v)"
550   -- \<open>Unfold all @{text let}s involving constants\<close>
551   by (fact Let_neg_numeral) -- \<open>FIXME drop\<close>
553 text \<open>Unfold @{text min} and @{text max} on numerals.\<close>
555 lemmas max_number_of [simp] =
556   max_def [of "numeral u" "numeral v"]
557   max_def [of "numeral u" "- numeral v"]
558   max_def [of "- numeral u" "numeral v"]
559   max_def [of "- numeral u" "- numeral v"] for u v
561 lemmas min_number_of [simp] =
562   min_def [of "numeral u" "numeral v"]
563   min_def [of "numeral u" "- numeral v"]
564   min_def [of "- numeral u" "numeral v"]
565   min_def [of "- numeral u" "- numeral v"] for u v
568 subsubsection \<open>Binary comparisons\<close>
570 text \<open>Preliminaries\<close>
572 lemma le_imp_0_less:
573   assumes le: "0 \<le> z"
574   shows "(0::int) < 1 + z"
575 proof -
576   have "0 \<le> z" by fact
577   also have "... < z + 1" by (rule less_add_one)
578   also have "... = 1 + z" by (simp add: ac_simps)
579   finally show "0 < 1 + z" .
580 qed
582 lemma odd_less_0_iff:
583   "(1 + z + z < 0) = (z < (0::int))"
584 proof (cases z)
585   case (nonneg n)
587                              le_imp_0_less [THEN order_less_imp_le])
588 next
589   case (neg n)
590   thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1
591     add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric])
592 qed
594 subsubsection \<open>Comparisons, for Ordered Rings\<close>
596 lemmas double_eq_0_iff = double_zero
598 lemma odd_nonzero:
599   "1 + z + z \<noteq> (0::int)"
600 proof (cases z)
601   case (nonneg n)
602   have le: "0 \<le> z+z" by (simp add: nonneg add_increasing)
603   thus ?thesis using  le_imp_0_less [OF le]
605 next
606   case (neg n)
607   show ?thesis
608   proof
609     assume eq: "1 + z + z = 0"
610     have "(0::int) < 1 + (int n + int n)"
612     also have "... = - (1 + z + z)"
613       by (simp add: neg add.assoc [symmetric])
614     also have "... = 0" by (simp add: eq)
615     finally have "0<0" ..
616     thus False by blast
617   qed
618 qed
621 subsection \<open>The Set of Integers\<close>
623 context ring_1
624 begin
626 definition Ints :: "'a set"  ("\<int>")
627   where "\<int> = range of_int"
629 lemma Ints_of_int [simp]: "of_int z \<in> \<int>"
630   by (simp add: Ints_def)
632 lemma Ints_of_nat [simp]: "of_nat n \<in> \<int>"
633   using Ints_of_int [of "of_nat n"] by simp
635 lemma Ints_0 [simp]: "0 \<in> \<int>"
636   using Ints_of_int [of "0"] by simp
638 lemma Ints_1 [simp]: "1 \<in> \<int>"
639   using Ints_of_int [of "1"] by simp
641 lemma Ints_add [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a + b \<in> \<int>"
642 apply (auto simp add: Ints_def)
643 apply (rule range_eqI)
644 apply (rule of_int_add [symmetric])
645 done
647 lemma Ints_minus [simp]: "a \<in> \<int> \<Longrightarrow> -a \<in> \<int>"
648 apply (auto simp add: Ints_def)
649 apply (rule range_eqI)
650 apply (rule of_int_minus [symmetric])
651 done
653 lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a - b \<in> \<int>"
654 apply (auto simp add: Ints_def)
655 apply (rule range_eqI)
656 apply (rule of_int_diff [symmetric])
657 done
659 lemma Ints_mult [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a * b \<in> \<int>"
660 apply (auto simp add: Ints_def)
661 apply (rule range_eqI)
662 apply (rule of_int_mult [symmetric])
663 done
665 lemma Ints_power [simp]: "a \<in> \<int> \<Longrightarrow> a ^ n \<in> \<int>"
666 by (induct n) simp_all
668 lemma Ints_cases [cases set: Ints]:
669   assumes "q \<in> \<int>"
670   obtains (of_int) z where "q = of_int z"
671   unfolding Ints_def
672 proof -
673   from \<open>q \<in> \<int>\<close> have "q \<in> range of_int" unfolding Ints_def .
674   then obtain z where "q = of_int z" ..
675   then show thesis ..
676 qed
678 lemma Ints_induct [case_names of_int, induct set: Ints]:
679   "q \<in> \<int> \<Longrightarrow> (\<And>z. P (of_int z)) \<Longrightarrow> P q"
680   by (rule Ints_cases) auto
682 end
684 text \<open>The premise involving @{term Ints} prevents @{term "a = 1/2"}.\<close>
686 lemma Ints_double_eq_0_iff:
687   assumes in_Ints: "a \<in> \<int>"
688   shows "(a + a = 0) = (a = (0::'a::ring_char_0))"
689 proof -
690   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
691   then obtain z where a: "a = of_int z" ..
692   show ?thesis
693   proof
694     assume "a = 0"
695     thus "a + a = 0" by simp
696   next
697     assume eq: "a + a = 0"
698     hence "of_int (z + z) = (of_int 0 :: 'a)" by (simp add: a)
699     hence "z + z = 0" by (simp only: of_int_eq_iff)
700     hence "z = 0" by (simp only: double_eq_0_iff)
701     thus "a = 0" by (simp add: a)
702   qed
703 qed
705 lemma Ints_odd_nonzero:
706   assumes in_Ints: "a \<in> \<int>"
707   shows "1 + a + a \<noteq> (0::'a::ring_char_0)"
708 proof -
709   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
710   then obtain z where a: "a = of_int z" ..
711   show ?thesis
712   proof
713     assume eq: "1 + a + a = 0"
714     hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
715     hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
716     with odd_nonzero show False by blast
717   qed
718 qed
720 lemma Nats_numeral [simp]: "numeral w \<in> \<nat>"
721   using of_nat_in_Nats [of "numeral w"] by simp
723 lemma Ints_odd_less_0:
724   assumes in_Ints: "a \<in> \<int>"
725   shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))"
726 proof -
727   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
728   then obtain z where a: "a = of_int z" ..
729   hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
730     by (simp add: a)
731   also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0_iff)
732   also have "... = (a < 0)" by (simp add: a)
733   finally show ?thesis .
734 qed
737 subsection \<open>@{term setsum} and @{term setprod}\<close>
739 lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
740   apply (cases "finite A")
741   apply (erule finite_induct, auto)
742   done
744 lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
745   apply (cases "finite A")
746   apply (erule finite_induct, auto)
747   done
749 lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
750   apply (cases "finite A")
751   apply (erule finite_induct, auto simp add: of_nat_mult)
752   done
754 lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
755   apply (cases "finite A")
756   apply (erule finite_induct, auto)
757   done
759 lemmas int_setsum = of_nat_setsum [where 'a=int]
760 lemmas int_setprod = of_nat_setprod [where 'a=int]
763 text \<open>Legacy theorems\<close>
765 lemmas zle_int = of_nat_le_iff [where 'a=int]
766 lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
767 lemmas numeral_1_eq_1 = numeral_One
769 subsection \<open>Setting up simplification procedures\<close>
771 lemmas of_int_simps =
772   of_int_0 of_int_1 of_int_add of_int_mult
774 ML_file "Tools/int_arith.ML"
775 declaration \<open>K Int_Arith.setup\<close>
777 simproc_setup fast_arith ("(m::'a::linordered_idom) < n" |
778   "(m::'a::linordered_idom) \<le> n" |
779   "(m::'a::linordered_idom) = n") =
780   \<open>K Lin_Arith.simproc\<close>
783 subsection\<open>More Inequality Reasoning\<close>
785 lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
786 by arith
788 lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
789 by arith
791 lemma zle_diff1_eq [simp]: "(w \<le> z - (1::int)) = (w<z)"
792 by arith
794 lemma zle_add1_eq_le [simp]: "(w < z + (1::int)) = (w\<le>z)"
795 by arith
797 lemma int_one_le_iff_zero_less: "((1::int) \<le> z) = (0 < z)"
798 by arith
801 subsection\<open>The functions @{term nat} and @{term int}\<close>
803 text\<open>Simplify the term @{term "w + - z"}\<close>
805 lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
806   using zless_nat_conj [of 1 z] by auto
808 text\<open>This simplifies expressions of the form @{term "int n = z"} where
809       z is an integer literal.\<close>
810 lemmas int_eq_iff_numeral [simp] = int_eq_iff [of _ "numeral v"] for v
812 lemma split_nat [arith_split]:
813   "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
814   (is "?P = (?L & ?R)")
815 proof (cases "i < 0")
816   case True thus ?thesis by auto
817 next
818   case False
819   have "?P = ?L"
820   proof
821     assume ?P thus ?L using False by clarsimp
822   next
823     assume ?L thus ?P using False by simp
824   qed
825   with False show ?thesis by simp
826 qed
828 lemma nat_abs_int_diff: "nat \<bar>int a - int b\<bar> = (if a \<le> b then b - a else a - b)"
829   by auto
831 lemma nat_int_add: "nat (int a + int b) = a + b"
832   by auto
834 context ring_1
835 begin
837 lemma of_int_of_nat [nitpick_simp]:
838   "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))"
839 proof (cases "k < 0")
840   case True then have "0 \<le> - k" by simp
841   then have "of_nat (nat (- k)) = of_int (- k)" by (rule of_nat_nat)
842   with True show ?thesis by simp
843 next
844   case False then show ?thesis by (simp add: not_less of_nat_nat)
845 qed
847 end
849 lemma nat_mult_distrib:
850   fixes z z' :: int
851   assumes "0 \<le> z"
852   shows "nat (z * z') = nat z * nat z'"
853 proof (cases "0 \<le> z'")
854   case False with assms have "z * z' \<le> 0"
855     by (simp add: not_le mult_le_0_iff)
856   then have "nat (z * z') = 0" by simp
857   moreover from False have "nat z' = 0" by simp
858   ultimately show ?thesis by simp
859 next
860   case True with assms have ge_0: "z * z' \<ge> 0" by (simp add: zero_le_mult_iff)
861   show ?thesis
862     by (rule injD [of "of_nat :: nat \<Rightarrow> int", OF inj_of_nat])
863       (simp only: of_nat_mult of_nat_nat [OF True]
864          of_nat_nat [OF assms] of_nat_nat [OF ge_0], simp)
865 qed
867 lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"
868 apply (rule trans)
869 apply (rule_tac  nat_mult_distrib, auto)
870 done
872 lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
873 apply (cases "z=0 | w=0")
874 apply (auto simp add: abs_if nat_mult_distrib [symmetric]
875                       nat_mult_distrib_neg [symmetric] mult_less_0_iff)
876 done
878 lemma int_in_range_abs [simp]:
879   "int n \<in> range abs"
880 proof (rule range_eqI)
881   show "int n = \<bar>int n\<bar>"
882     by simp
883 qed
885 lemma range_abs_Nats [simp]:
886   "range abs = (\<nat> :: int set)"
887 proof -
888   have "\<bar>k\<bar> \<in> \<nat>" for k :: int
889     by (cases k) simp_all
890   moreover have "k \<in> range abs" if "k \<in> \<nat>" for k :: int
891     using that by induct simp
892   ultimately show ?thesis by blast
893 qed
895 lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
896 apply (rule sym)
897 apply (simp add: nat_eq_iff)
898 done
900 lemma diff_nat_eq_if:
901      "nat z - nat z' =
902         (if z' < 0 then nat z
903          else let d = z-z' in
904               if d < 0 then 0 else nat d)"
905 by (simp add: Let_def nat_diff_distrib [symmetric])
907 lemma nat_numeral_diff_1 [simp]:
908   "numeral v - (1::nat) = nat (numeral v - 1)"
909   using diff_nat_numeral [of v Num.One] by simp
912 subsection "Induction principles for int"
914 text\<open>Well-founded segments of the integers\<close>
916 definition
917   int_ge_less_than  ::  "int => (int * int) set"
918 where
919   "int_ge_less_than d = {(z',z). d \<le> z' & z' < z}"
921 theorem wf_int_ge_less_than: "wf (int_ge_less_than d)"
922 proof -
923   have "int_ge_less_than d \<subseteq> measure (%z. nat (z-d))"
924     by (auto simp add: int_ge_less_than_def)
925   thus ?thesis
926     by (rule wf_subset [OF wf_measure])
927 qed
929 text\<open>This variant looks odd, but is typical of the relations suggested
930 by RankFinder.\<close>
932 definition
933   int_ge_less_than2 ::  "int => (int * int) set"
934 where
935   "int_ge_less_than2 d = {(z',z). d \<le> z & z' < z}"
937 theorem wf_int_ge_less_than2: "wf (int_ge_less_than2 d)"
938 proof -
939   have "int_ge_less_than2 d \<subseteq> measure (%z. nat (1+z-d))"
940     by (auto simp add: int_ge_less_than2_def)
941   thus ?thesis
942     by (rule wf_subset [OF wf_measure])
943 qed
945 (* `set:int': dummy construction *)
946 theorem int_ge_induct [case_names base step, induct set: int]:
947   fixes i :: int
948   assumes ge: "k \<le> i" and
949     base: "P k" and
950     step: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
951   shows "P i"
952 proof -
953   { fix n
954     have "\<And>i::int. n = nat (i - k) \<Longrightarrow> k \<le> i \<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       then have "n = nat((i - 1) - k)" by arith
962       moreover
963       have ki1: "k \<le> i - 1" 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 ge show ?thesis by fast
970 qed
972 (* `set:int': dummy construction *)
973 theorem int_gr_induct [case_names base step, induct set: int]:
974   assumes gr: "k < (i::int)" and
975         base: "P(k+1)" and
976         step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
977   shows "P i"
978 apply(rule int_ge_induct[of "k + 1"])
979   using gr apply arith
980  apply(rule base)
981 apply (rule step, simp+)
982 done
984 theorem int_le_induct [consumes 1, case_names base step]:
985   assumes le: "i \<le> (k::int)" and
986         base: "P(k)" and
987         step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
988   shows "P i"
989 proof -
990   { fix n
991     have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i"
992     proof (induct n)
993       case 0
994       hence "i = k" by arith
995       thus "P i" using base by simp
996     next
997       case (Suc n)
998       hence "n = nat (k - (i + 1))" by arith
999       moreover
1000       have ki1: "i + 1 \<le> k" using Suc.prems by arith
1001       ultimately
1002       have "P (i + 1)" by(rule Suc.hyps)
1003       from step[OF ki1 this] show ?case by simp
1004     qed
1005   }
1006   with le show ?thesis by fast
1007 qed
1009 theorem int_less_induct [consumes 1, case_names base step]:
1010   assumes less: "(i::int) < k" and
1011         base: "P(k - 1)" and
1012         step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
1013   shows "P i"
1014 apply(rule int_le_induct[of _ "k - 1"])
1015   using less apply arith
1016  apply(rule base)
1017 apply (rule step, simp+)
1018 done
1020 theorem int_induct [case_names base step1 step2]:
1021   fixes k :: int
1022   assumes base: "P k"
1023     and step1: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
1024     and step2: "\<And>i. k \<ge> i \<Longrightarrow> P i \<Longrightarrow> P (i - 1)"
1025   shows "P i"
1026 proof -
1027   have "i \<le> k \<or> i \<ge> k" by arith
1028   then show ?thesis
1029   proof
1030     assume "i \<ge> k"
1031     then show ?thesis using base
1032       by (rule int_ge_induct) (fact step1)
1033   next
1034     assume "i \<le> k"
1035     then show ?thesis using base
1036       by (rule int_le_induct) (fact step2)
1037   qed
1038 qed
1040 subsection\<open>Intermediate value theorems\<close>
1042 lemma int_val_lemma:
1043      "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->
1044       f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
1045 unfolding One_nat_def
1046 apply (induct n)
1047 apply simp
1048 apply (intro strip)
1049 apply (erule impE, simp)
1050 apply (erule_tac x = n in allE, simp)
1051 apply (case_tac "k = f (Suc n)")
1052 apply force
1053 apply (erule impE)
1054  apply (simp add: abs_if split add: split_if_asm)
1055 apply (blast intro: le_SucI)
1056 done
1058 lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
1060 lemma nat_intermed_int_val:
1061      "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;
1062          f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
1063 apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k
1064        in int_val_lemma)
1065 unfolding One_nat_def
1066 apply simp
1067 apply (erule exE)
1068 apply (rule_tac x = "i+m" in exI, arith)
1069 done
1072 subsection\<open>Products and 1, by T. M. Rasmussen\<close>
1074 lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))"
1075 by arith
1077 lemma abs_zmult_eq_1:
1078   assumes mn: "\<bar>m * n\<bar> = 1"
1079   shows "\<bar>m\<bar> = (1::int)"
1080 proof -
1081   have 0: "m \<noteq> 0 & n \<noteq> 0" using mn
1082     by auto
1083   have "~ (2 \<le> \<bar>m\<bar>)"
1084   proof
1085     assume "2 \<le> \<bar>m\<bar>"
1086     hence "2*\<bar>n\<bar> \<le> \<bar>m\<bar>*\<bar>n\<bar>"
1087       by (simp add: mult_mono 0)
1088     also have "... = \<bar>m*n\<bar>"
1089       by (simp add: abs_mult)
1090     also have "... = 1"
1091       by (simp add: mn)
1092     finally have "2*\<bar>n\<bar> \<le> 1" .
1093     thus "False" using 0
1094       by arith
1095   qed
1096   thus ?thesis using 0
1097     by auto
1098 qed
1100 lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1"
1101 by (insert abs_zmult_eq_1 [of m n], arith)
1103 lemma pos_zmult_eq_1_iff:
1104   assumes "0 < (m::int)" shows "(m * n = 1) = (m = 1 & n = 1)"
1105 proof -
1106   from assms have "m * n = 1 ==> m = 1" by (auto dest: pos_zmult_eq_1_iff_lemma)
1107   thus ?thesis by (auto dest: pos_zmult_eq_1_iff_lemma)
1108 qed
1110 lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
1111 apply (rule iffI)
1112  apply (frule pos_zmult_eq_1_iff_lemma)
1113  apply (simp add: mult.commute [of m])
1114  apply (frule pos_zmult_eq_1_iff_lemma, auto)
1115 done
1117 lemma infinite_UNIV_int: "\<not> finite (UNIV::int set)"
1118 proof
1119   assume "finite (UNIV::int set)"
1120   moreover have "inj (\<lambda>i::int. 2 * i)"
1121     by (rule injI) simp
1122   ultimately have "surj (\<lambda>i::int. 2 * i)"
1123     by (rule finite_UNIV_inj_surj)
1124   then obtain i :: int where "1 = 2 * i" by (rule surjE)
1125   then show False by (simp add: pos_zmult_eq_1_iff)
1126 qed
1129 subsection \<open>Further theorems on numerals\<close>
1131 subsubsection\<open>Special Simplification for Constants\<close>
1133 text\<open>These distributive laws move literals inside sums and differences.\<close>
1135 lemmas distrib_right_numeral [simp] = distrib_right [of _ _ "numeral v"] for v
1136 lemmas distrib_left_numeral [simp] = distrib_left [of "numeral v"] for v
1137 lemmas left_diff_distrib_numeral [simp] = left_diff_distrib [of _ _ "numeral v"] for v
1138 lemmas right_diff_distrib_numeral [simp] = right_diff_distrib [of "numeral v"] for v
1140 text\<open>These are actually for fields, like real: but where else to put them?\<close>
1142 lemmas zero_less_divide_iff_numeral [simp, no_atp] = zero_less_divide_iff [of "numeral w"] for w
1143 lemmas divide_less_0_iff_numeral [simp, no_atp] = divide_less_0_iff [of "numeral w"] for w
1144 lemmas zero_le_divide_iff_numeral [simp, no_atp] = zero_le_divide_iff [of "numeral w"] for w
1145 lemmas divide_le_0_iff_numeral [simp, no_atp] = divide_le_0_iff [of "numeral w"] for w
1148 text \<open>Replaces @{text "inverse #nn"} by @{text "1/#nn"}.  It looks
1149   strange, but then other simprocs simplify the quotient.\<close>
1151 lemmas inverse_eq_divide_numeral [simp] =
1152   inverse_eq_divide [of "numeral w"] for w
1154 lemmas inverse_eq_divide_neg_numeral [simp] =
1155   inverse_eq_divide [of "- numeral w"] for w
1157 text \<open>These laws simplify inequalities, moving unary minus from a term
1158 into the literal.\<close>
1160 lemmas equation_minus_iff_numeral [no_atp] =
1161   equation_minus_iff [of "numeral v"] for v
1163 lemmas minus_equation_iff_numeral [no_atp] =
1164   minus_equation_iff [of _ "numeral v"] for v
1166 lemmas le_minus_iff_numeral [no_atp] =
1167   le_minus_iff [of "numeral v"] for v
1169 lemmas minus_le_iff_numeral [no_atp] =
1170   minus_le_iff [of _ "numeral v"] for v
1172 lemmas less_minus_iff_numeral [no_atp] =
1173   less_minus_iff [of "numeral v"] for v
1175 lemmas minus_less_iff_numeral [no_atp] =
1176   minus_less_iff [of _ "numeral v"] for v
1178 -- \<open>FIXME maybe simproc\<close>
1181 text \<open>Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"})\<close>
1183 lemmas mult_less_cancel_left_numeral [simp, no_atp] = mult_less_cancel_left [of "numeral v"] for v
1184 lemmas mult_less_cancel_right_numeral [simp, no_atp] = mult_less_cancel_right [of _ "numeral v"] for v
1185 lemmas mult_le_cancel_left_numeral [simp, no_atp] = mult_le_cancel_left [of "numeral v"] for v
1186 lemmas mult_le_cancel_right_numeral [simp, no_atp] = mult_le_cancel_right [of _ "numeral v"] for v
1189 text \<open>Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="})\<close>
1191 lemmas le_divide_eq_numeral1 [simp] =
1192   pos_le_divide_eq [of "numeral w", OF zero_less_numeral]
1193   neg_le_divide_eq [of "- numeral w", OF neg_numeral_less_zero] for w
1195 lemmas divide_le_eq_numeral1 [simp] =
1196   pos_divide_le_eq [of "numeral w", OF zero_less_numeral]
1197   neg_divide_le_eq [of "- numeral w", OF neg_numeral_less_zero] for w
1199 lemmas less_divide_eq_numeral1 [simp] =
1200   pos_less_divide_eq [of "numeral w", OF zero_less_numeral]
1201   neg_less_divide_eq [of "- numeral w", OF neg_numeral_less_zero] for w
1203 lemmas divide_less_eq_numeral1 [simp] =
1204   pos_divide_less_eq [of "numeral w", OF zero_less_numeral]
1205   neg_divide_less_eq [of "- numeral w", OF neg_numeral_less_zero] for w
1207 lemmas eq_divide_eq_numeral1 [simp] =
1208   eq_divide_eq [of _ _ "numeral w"]
1209   eq_divide_eq [of _ _ "- numeral w"] for w
1211 lemmas divide_eq_eq_numeral1 [simp] =
1212   divide_eq_eq [of _ "numeral w"]
1213   divide_eq_eq [of _ "- numeral w"] for w
1216 subsubsection\<open>Optional Simplification Rules Involving Constants\<close>
1218 text\<open>Simplify quotients that are compared with a literal constant.\<close>
1220 lemmas le_divide_eq_numeral =
1221   le_divide_eq [of "numeral w"]
1222   le_divide_eq [of "- numeral w"] for w
1224 lemmas divide_le_eq_numeral =
1225   divide_le_eq [of _ _ "numeral w"]
1226   divide_le_eq [of _ _ "- numeral w"] for w
1228 lemmas less_divide_eq_numeral =
1229   less_divide_eq [of "numeral w"]
1230   less_divide_eq [of "- numeral w"] for w
1232 lemmas divide_less_eq_numeral =
1233   divide_less_eq [of _ _ "numeral w"]
1234   divide_less_eq [of _ _ "- numeral w"] for w
1236 lemmas eq_divide_eq_numeral =
1237   eq_divide_eq [of "numeral w"]
1238   eq_divide_eq [of "- numeral w"] for w
1240 lemmas divide_eq_eq_numeral =
1241   divide_eq_eq [of _ _ "numeral w"]
1242   divide_eq_eq [of _ _ "- numeral w"] for w
1245 text\<open>Not good as automatic simprules because they cause case splits.\<close>
1246 lemmas divide_const_simps =
1247   le_divide_eq_numeral divide_le_eq_numeral less_divide_eq_numeral
1248   divide_less_eq_numeral eq_divide_eq_numeral divide_eq_eq_numeral
1249   le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
1252 subsection \<open>The divides relation\<close>
1254 lemma zdvd_antisym_nonneg:
1255     "0 <= m ==> 0 <= n ==> m dvd n ==> n dvd m ==> m = (n::int)"
1256   apply (simp add: dvd_def, auto)
1257   apply (auto simp add: mult.assoc zero_le_mult_iff zmult_eq_1_iff)
1258   done
1260 lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a"
1261   shows "\<bar>a\<bar> = \<bar>b\<bar>"
1262 proof cases
1263   assume "a = 0" with assms show ?thesis by simp
1264 next
1265   assume "a \<noteq> 0"
1266   from \<open>a dvd b\<close> obtain k where k:"b = a*k" unfolding dvd_def by blast
1267   from \<open>b dvd a\<close> obtain k' where k':"a = b*k'" unfolding dvd_def by blast
1268   from k k' have "a = a*k*k'" by simp
1269   with mult_cancel_left1[where c="a" and b="k*k'"]
1270   have kk':"k*k' = 1" using \<open>a\<noteq>0\<close> by (simp add: mult.assoc)
1271   hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff)
1272   thus ?thesis using k k' by auto
1273 qed
1275 lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
1276   using dvd_add_right_iff [of k "- n" m] by simp
1278 lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
1279   using dvd_add_times_triv_right_iff [of k n m] by (simp add: ac_simps)
1281 lemma dvd_imp_le_int:
1282   fixes d i :: int
1283   assumes "i \<noteq> 0" and "d dvd i"
1284   shows "\<bar>d\<bar> \<le> \<bar>i\<bar>"
1285 proof -
1286   from \<open>d dvd i\<close> obtain k where "i = d * k" ..
1287   with \<open>i \<noteq> 0\<close> have "k \<noteq> 0" by auto
1288   then have "1 \<le> \<bar>k\<bar>" and "0 \<le> \<bar>d\<bar>" by auto
1289   then have "\<bar>d\<bar> * 1 \<le> \<bar>d\<bar> * \<bar>k\<bar>" by (rule mult_left_mono)
1290   with \<open>i = d * k\<close> show ?thesis by (simp add: abs_mult)
1291 qed
1293 lemma zdvd_not_zless:
1294   fixes m n :: int
1295   assumes "0 < m" and "m < n"
1296   shows "\<not> n dvd m"
1297 proof
1298   from assms have "0 < n" by auto
1299   assume "n dvd m" then obtain k where k: "m = n * k" ..
1300   with \<open>0 < m\<close> have "0 < n * k" by auto
1301   with \<open>0 < n\<close> have "0 < k" by (simp add: zero_less_mult_iff)
1302   with k \<open>0 < n\<close> \<open>m < n\<close> have "n * k < n * 1" by simp
1303   with \<open>0 < n\<close> \<open>0 < k\<close> show False unfolding mult_less_cancel_left by auto
1304 qed
1306 lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)"
1307   shows "m dvd n"
1308 proof-
1309   from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast
1310   {assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp
1311     with h have False by (simp add: mult.assoc)}
1312   hence "n = m * h" by blast
1313   thus ?thesis by simp
1314 qed
1316 theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
1317 proof -
1318   have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"
1319   proof -
1320     fix k
1321     assume A: "int y = int x * k"
1322     then show "x dvd y"
1323     proof (cases k)
1324       case (nonneg n)
1325       with A have "y = x * n" by (simp add: of_nat_mult [symmetric])
1326       then show ?thesis ..
1327     next
1328       case (neg n)
1329       with A have "int y = int x * (- int (Suc n))" by simp
1330       also have "\<dots> = - (int x * int (Suc n))" by (simp only: mult_minus_right)
1331       also have "\<dots> = - int (x * Suc n)" by (simp only: of_nat_mult [symmetric])
1332       finally have "- int (x * Suc n) = int y" ..
1333       then show ?thesis by (simp only: negative_eq_positive) auto
1334     qed
1335   qed
1336   then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left of_nat_mult)
1337 qed
1339 lemma zdvd1_eq[simp]: "(x::int) dvd 1 = (\<bar>x\<bar> = 1)"
1340 proof
1341   assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp
1342   hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
1343   hence "nat \<bar>x\<bar> = 1"  by simp
1344   thus "\<bar>x\<bar> = 1" by (cases "x < 0") auto
1345 next
1346   assume "\<bar>x\<bar>=1"
1347   then have "x = 1 \<or> x = -1" by auto
1348   then show "x dvd 1" by (auto intro: dvdI)
1349 qed
1351 lemma zdvd_mult_cancel1:
1352   assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
1353 proof
1354   assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m"
1355     by (cases "n >0") (auto simp add: minus_equation_iff)
1356 next
1357   assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
1358   from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
1359 qed
1361 lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
1362   unfolding zdvd_int by (cases "z \<ge> 0") simp_all
1364 lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
1365   unfolding zdvd_int by (cases "z \<ge> 0") simp_all
1367 lemma dvd_int_unfold_dvd_nat:
1368   "k dvd l \<longleftrightarrow> nat \<bar>k\<bar> dvd nat \<bar>l\<bar>"
1369   unfolding dvd_int_iff [symmetric] by simp
1371 lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
1372   by (auto simp add: dvd_int_iff)
1374 lemma eq_nat_nat_iff:
1375   "0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat z = nat z' \<longleftrightarrow> z = z'"
1376   by (auto elim!: nonneg_eq_int)
1378 lemma nat_power_eq:
1379   "0 \<le> z \<Longrightarrow> nat (z ^ n) = nat z ^ n"
1380   by (induct n) (simp_all add: nat_mult_distrib)
1382 lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
1383   apply (cases n)
1384   apply (auto simp add: dvd_int_iff)
1385   apply (cases z)
1386   apply (auto simp add: dvd_imp_le)
1387   done
1389 lemma zdvd_period:
1390   fixes a d :: int
1391   assumes "a dvd d"
1392   shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)"
1393 proof -
1394   from assms obtain k where "d = a * k" by (rule dvdE)
1395   show ?thesis
1396   proof
1397     assume "a dvd (x + t)"
1398     then obtain l where "x + t = a * l" by (rule dvdE)
1399     then have "x = a * l - t" by simp
1400     with \<open>d = a * k\<close> show "a dvd x + c * d + t" by simp
1401   next
1402     assume "a dvd x + c * d + t"
1403     then obtain l where "x + c * d + t = a * l" by (rule dvdE)
1404     then have "x = a * l - c * d - t" by simp
1405     with \<open>d = a * k\<close> show "a dvd (x + t)" by simp
1406   qed
1407 qed
1410 subsection \<open>Finiteness of intervals\<close>
1412 lemma finite_interval_int1 [iff]: "finite {i :: int. a <= i & i <= b}"
1413 proof (cases "a <= b")
1414   case True
1415   from this show ?thesis
1416   proof (induct b rule: int_ge_induct)
1417     case base
1418     have "{i. a <= i & i <= a} = {a}" by auto
1419     from this show ?case by simp
1420   next
1421     case (step b)
1422     from this have "{i. a <= i & i <= b + 1} = {i. a <= i & i <= b} \<union> {b + 1}" by auto
1423     from this step show ?case by simp
1424   qed
1425 next
1426   case False from this show ?thesis
1427     by (metis (lifting, no_types) Collect_empty_eq finite.emptyI order_trans)
1428 qed
1430 lemma finite_interval_int2 [iff]: "finite {i :: int. a <= i & i < b}"
1431 by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
1433 lemma finite_interval_int3 [iff]: "finite {i :: int. a < i & i <= b}"
1434 by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
1436 lemma finite_interval_int4 [iff]: "finite {i :: int. a < i & i < b}"
1437 by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
1440 subsection \<open>Configuration of the code generator\<close>
1442 text \<open>Constructors\<close>
1444 definition Pos :: "num \<Rightarrow> int" where
1445   [simp, code_abbrev]: "Pos = numeral"
1447 definition Neg :: "num \<Rightarrow> int" where
1448   [simp, code_abbrev]: "Neg n = - (Pos n)"
1450 code_datatype "0::int" Pos Neg
1453 text \<open>Auxiliary operations\<close>
1455 definition dup :: "int \<Rightarrow> int" where
1456   [simp]: "dup k = k + k"
1458 lemma dup_code [code]:
1459   "dup 0 = 0"
1460   "dup (Pos n) = Pos (Num.Bit0 n)"
1461   "dup (Neg n) = Neg (Num.Bit0 n)"
1462   unfolding Pos_def Neg_def
1463   by (simp_all add: numeral_Bit0)
1465 definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
1466   [simp]: "sub m n = numeral m - numeral n"
1468 lemma sub_code [code]:
1469   "sub Num.One Num.One = 0"
1470   "sub (Num.Bit0 m) Num.One = Pos (Num.BitM m)"
1471   "sub (Num.Bit1 m) Num.One = Pos (Num.Bit0 m)"
1472   "sub Num.One (Num.Bit0 n) = Neg (Num.BitM n)"
1473   "sub Num.One (Num.Bit1 n) = Neg (Num.Bit0 n)"
1474   "sub (Num.Bit0 m) (Num.Bit0 n) = dup (sub m n)"
1475   "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)"
1476   "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1"
1477   "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1"
1478   apply (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def numeral_BitM)
1479   apply (simp_all only: algebra_simps minus_diff_eq)
1480   apply (simp_all only: add.commute [of _ "- (numeral n + numeral n)"])
1481   apply (simp_all only: minus_add add.assoc left_minus)
1482   done
1484 text \<open>Implementations\<close>
1486 lemma one_int_code [code, code_unfold]:
1487   "1 = Pos Num.One"
1488   by simp
1490 lemma plus_int_code [code]:
1491   "k + 0 = (k::int)"
1492   "0 + l = (l::int)"
1493   "Pos m + Pos n = Pos (m + n)"
1494   "Pos m + Neg n = sub m n"
1495   "Neg m + Pos n = sub n m"
1496   "Neg m + Neg n = Neg (m + n)"
1497   by simp_all
1499 lemma uminus_int_code [code]:
1500   "uminus 0 = (0::int)"
1501   "uminus (Pos m) = Neg m"
1502   "uminus (Neg m) = Pos m"
1503   by simp_all
1505 lemma minus_int_code [code]:
1506   "k - 0 = (k::int)"
1507   "0 - l = uminus (l::int)"
1508   "Pos m - Pos n = sub m n"
1509   "Pos m - Neg n = Pos (m + n)"
1510   "Neg m - Pos n = Neg (m + n)"
1511   "Neg m - Neg n = sub n m"
1512   by simp_all
1514 lemma times_int_code [code]:
1515   "k * 0 = (0::int)"
1516   "0 * l = (0::int)"
1517   "Pos m * Pos n = Pos (m * n)"
1518   "Pos m * Neg n = Neg (m * n)"
1519   "Neg m * Pos n = Neg (m * n)"
1520   "Neg m * Neg n = Pos (m * n)"
1521   by simp_all
1523 instantiation int :: equal
1524 begin
1526 definition
1527   "HOL.equal k l \<longleftrightarrow> k = (l::int)"
1529 instance by default (rule equal_int_def)
1531 end
1533 lemma equal_int_code [code]:
1534   "HOL.equal 0 (0::int) \<longleftrightarrow> True"
1535   "HOL.equal 0 (Pos l) \<longleftrightarrow> False"
1536   "HOL.equal 0 (Neg l) \<longleftrightarrow> False"
1537   "HOL.equal (Pos k) 0 \<longleftrightarrow> False"
1538   "HOL.equal (Pos k) (Pos l) \<longleftrightarrow> HOL.equal k l"
1539   "HOL.equal (Pos k) (Neg l) \<longleftrightarrow> False"
1540   "HOL.equal (Neg k) 0 \<longleftrightarrow> False"
1541   "HOL.equal (Neg k) (Pos l) \<longleftrightarrow> False"
1542   "HOL.equal (Neg k) (Neg l) \<longleftrightarrow> HOL.equal k l"
1543   by (auto simp add: equal)
1545 lemma equal_int_refl [code nbe]:
1546   "HOL.equal (k::int) k \<longleftrightarrow> True"
1547   by (fact equal_refl)
1549 lemma less_eq_int_code [code]:
1550   "0 \<le> (0::int) \<longleftrightarrow> True"
1551   "0 \<le> Pos l \<longleftrightarrow> True"
1552   "0 \<le> Neg l \<longleftrightarrow> False"
1553   "Pos k \<le> 0 \<longleftrightarrow> False"
1554   "Pos k \<le> Pos l \<longleftrightarrow> k \<le> l"
1555   "Pos k \<le> Neg l \<longleftrightarrow> False"
1556   "Neg k \<le> 0 \<longleftrightarrow> True"
1557   "Neg k \<le> Pos l \<longleftrightarrow> True"
1558   "Neg k \<le> Neg l \<longleftrightarrow> l \<le> k"
1559   by simp_all
1561 lemma less_int_code [code]:
1562   "0 < (0::int) \<longleftrightarrow> False"
1563   "0 < Pos l \<longleftrightarrow> True"
1564   "0 < Neg l \<longleftrightarrow> False"
1565   "Pos k < 0 \<longleftrightarrow> False"
1566   "Pos k < Pos l \<longleftrightarrow> k < l"
1567   "Pos k < Neg l \<longleftrightarrow> False"
1568   "Neg k < 0 \<longleftrightarrow> True"
1569   "Neg k < Pos l \<longleftrightarrow> True"
1570   "Neg k < Neg l \<longleftrightarrow> l < k"
1571   by simp_all
1573 lemma nat_code [code]:
1574   "nat (Int.Neg k) = 0"
1575   "nat 0 = 0"
1576   "nat (Int.Pos k) = nat_of_num k"
1577   by (simp_all add: nat_of_num_numeral)
1579 lemma (in ring_1) of_int_code [code]:
1580   "of_int (Int.Neg k) = - numeral k"
1581   "of_int 0 = 0"
1582   "of_int (Int.Pos k) = numeral k"
1583   by simp_all
1586 text \<open>Serializer setup\<close>
1588 code_identifier
1589   code_module Int \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
1591 quickcheck_params [default_type = int]
1593 hide_const (open) Pos Neg sub dup
1596 subsection \<open>Legacy theorems\<close>
1598 lemmas inj_int = inj_of_nat [where 'a=int]
1599 lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
1600 lemmas int_mult = of_nat_mult [where 'a=int]
1601 lemmas zmult_int = of_nat_mult [where 'a=int, symmetric]
1602 lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="n"] for n
1603 lemmas zless_int = of_nat_less_iff [where 'a=int]
1604 lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="k"] for k
1605 lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int]
1606 lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
1607 lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="n"] for n
1608 lemmas int_0 = of_nat_0 [where 'a=int]
1609 lemmas int_1 = of_nat_1 [where 'a=int]
1610 lemmas int_Suc = of_nat_Suc [where 'a=int]
1611 lemmas int_numeral = of_nat_numeral [where 'a=int]
1612 lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m"] for m
1613 lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
1614 lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
1615 lemmas zpower_numeral_even = power_numeral_even [where 'a=int]
1616 lemmas zpower_numeral_odd = power_numeral_odd [where 'a=int]
1618 lemma zpower_zpower:
1619   "(x ^ y) ^ z = (x ^ (y * z)::int)"
1620   by (rule power_mult [symmetric])
1622 lemma int_power:
1623   "int (m ^ n) = int m ^ n"
1624   by (fact of_nat_power)
1626 lemmas zpower_int = int_power [symmetric]
1628 text \<open>De-register @{text "int"} as a quotient type:\<close>
1630 lifting_update int.lifting
1631 lifting_forget int.lifting
1633 text\<open>Also the class for fields with characteristic zero.\<close>
1634 class field_char_0 = field + ring_char_0
1635 subclass (in linordered_field) field_char_0 ..
1637 end