src/HOL/Int.thy
 author paulson Mon Feb 22 14:37:56 2016 +0000 (2016-02-22) changeset 62379 340738057c8c parent 62348 9a5f43dac883 child 62390 842917225d56 permissions -rw-r--r--
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
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 standard (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 standard (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 lemma zabs_less_one_iff [simp]:
194   fixes z :: int
195   shows "\<bar>z\<bar> < 1 \<longleftrightarrow> z = 0" (is "?P \<longleftrightarrow> ?Q")
196 proof
197   assume ?Q then show ?P by simp
198 next
199   assume ?P
200   with zless_imp_add1_zle [of "\<bar>z\<bar>" 1] have "\<bar>z\<bar> + 1 \<le> 1"
201     by simp
202   then have "\<bar>z\<bar> \<le> 0"
203     by simp
204   then show ?Q
205     by simp
206 qed
208 lemmas int_distrib =
209   distrib_right [of z1 z2 w]
210   distrib_left [of w z1 z2]
211   left_diff_distrib [of z1 z2 w]
212   right_diff_distrib [of w z1 z2]
213   for z1 z2 w :: int
216 subsection \<open>Embedding of the Integers into any \<open>ring_1\<close>: \<open>of_int\<close>\<close>
218 context ring_1
219 begin
221 lift_definition of_int :: "int \<Rightarrow> 'a" is "\<lambda>(i, j). of_nat i - of_nat j"
222   by (clarsimp simp add: diff_eq_eq eq_diff_eq diff_add_eq
225 lemma of_int_0 [simp]: "of_int 0 = 0"
226   by transfer simp
228 lemma of_int_1 [simp]: "of_int 1 = 1"
229   by transfer simp
231 lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z"
232   by transfer (clarsimp simp add: algebra_simps)
234 lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)"
235   by (transfer fixing: uminus) clarsimp
237 lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z"
238   using of_int_add [of w "- z"] by simp
240 lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
241   by (transfer fixing: times) (clarsimp simp add: algebra_simps of_nat_mult)
243 lemma mult_of_int_commute: "of_int x * y = y * of_int x"
244   by (transfer fixing: times) (auto simp: algebra_simps mult_of_nat_commute)
246 text\<open>Collapse nested embeddings\<close>
247 lemma of_int_of_nat_eq [simp]: "of_int (int n) = of_nat n"
248 by (induct n) auto
250 lemma of_int_numeral [simp, code_post]: "of_int (numeral k) = numeral k"
251   by (simp add: of_nat_numeral [symmetric] of_int_of_nat_eq [symmetric])
253 lemma of_int_neg_numeral [code_post]: "of_int (- numeral k) = - numeral k"
254   by simp
256 lemma of_int_power [simp]:
257   "of_int (z ^ n) = of_int z ^ n"
258   by (induct n) simp_all
260 end
262 context ring_char_0
263 begin
265 lemma of_int_eq_iff [simp]:
266    "of_int w = of_int z \<longleftrightarrow> w = z"
267   by transfer (clarsimp simp add: algebra_simps
270 text\<open>Special cases where either operand is zero\<close>
271 lemma of_int_eq_0_iff [simp]:
272   "of_int z = 0 \<longleftrightarrow> z = 0"
273   using of_int_eq_iff [of z 0] by simp
275 lemma of_int_0_eq_iff [simp]:
276   "0 = of_int z \<longleftrightarrow> z = 0"
277   using of_int_eq_iff [of 0 z] by simp
279 lemma of_int_eq_1_iff [iff]:
280    "of_int z = 1 \<longleftrightarrow> z = 1"
281   using of_int_eq_iff [of z 1] by simp
283 end
285 context linordered_idom
286 begin
288 text\<open>Every \<open>linordered_idom\<close> has characteristic zero.\<close>
289 subclass ring_char_0 ..
291 lemma of_int_le_iff [simp]:
292   "of_int w \<le> of_int z \<longleftrightarrow> w \<le> z"
293   by (transfer fixing: less_eq) (clarsimp simp add: algebra_simps
296 lemma of_int_less_iff [simp]:
297   "of_int w < of_int z \<longleftrightarrow> w < z"
298   by (simp add: less_le order_less_le)
300 lemma of_int_0_le_iff [simp]:
301   "0 \<le> of_int z \<longleftrightarrow> 0 \<le> z"
302   using of_int_le_iff [of 0 z] by simp
304 lemma of_int_le_0_iff [simp]:
305   "of_int z \<le> 0 \<longleftrightarrow> z \<le> 0"
306   using of_int_le_iff [of z 0] by simp
308 lemma of_int_0_less_iff [simp]:
309   "0 < of_int z \<longleftrightarrow> 0 < z"
310   using of_int_less_iff [of 0 z] by simp
312 lemma of_int_less_0_iff [simp]:
313   "of_int z < 0 \<longleftrightarrow> z < 0"
314   using of_int_less_iff [of z 0] by simp
316 lemma of_int_1_le_iff [simp]:
317   "1 \<le> of_int z \<longleftrightarrow> 1 \<le> z"
318   using of_int_le_iff [of 1 z] by simp
320 lemma of_int_le_1_iff [simp]:
321   "of_int z \<le> 1 \<longleftrightarrow> z \<le> 1"
322   using of_int_le_iff [of z 1] by simp
324 lemma of_int_1_less_iff [simp]:
325   "1 < of_int z \<longleftrightarrow> 1 < z"
326   using of_int_less_iff [of 1 z] by simp
328 lemma of_int_less_1_iff [simp]:
329   "of_int z < 1 \<longleftrightarrow> z < 1"
330   using of_int_less_iff [of z 1] by simp
332 lemma of_int_pos: "z > 0 \<Longrightarrow> of_int z > 0"
333   by simp
335 lemma of_int_nonneg: "z \<ge> 0 \<Longrightarrow> of_int z \<ge> 0"
336   by simp
338 lemma of_int_abs [simp]:
339   "of_int \<bar>x\<bar> = \<bar>of_int x\<bar>"
340   by (auto simp add: abs_if)
342 lemma of_int_lessD:
343   assumes "\<bar>of_int n\<bar> < x"
344   shows "n = 0 \<or> x > 1"
345 proof (cases "n = 0")
346   case True then show ?thesis by simp
347 next
348   case False
349   then have "\<bar>n\<bar> \<noteq> 0" by simp
350   then have "\<bar>n\<bar> > 0" by simp
351   then have "\<bar>n\<bar> \<ge> 1"
352     using zless_imp_add1_zle [of 0 "\<bar>n\<bar>"] by simp
353   then have "\<bar>of_int n\<bar> \<ge> 1"
354     unfolding of_int_1_le_iff [of "\<bar>n\<bar>", symmetric] by simp
355   then have "1 < x" using assms by (rule le_less_trans)
356   then show ?thesis ..
357 qed
359 lemma of_int_leD:
360   assumes "\<bar>of_int n\<bar> \<le> x"
361   shows "n = 0 \<or> 1 \<le> x"
362 proof (cases "n = 0")
363   case True then show ?thesis by simp
364 next
365   case False
366   then have "\<bar>n\<bar> \<noteq> 0" by simp
367   then have "\<bar>n\<bar> > 0" by simp
368   then have "\<bar>n\<bar> \<ge> 1"
369     using zless_imp_add1_zle [of 0 "\<bar>n\<bar>"] by simp
370   then have "\<bar>of_int n\<bar> \<ge> 1"
371     unfolding of_int_1_le_iff [of "\<bar>n\<bar>", symmetric] by simp
372   then have "1 \<le> x" using assms by (rule order_trans)
373   then show ?thesis ..
374 qed
377 end
379 text \<open>Comparisons involving @{term of_int}.\<close>
381 lemma of_int_eq_numeral_iff [iff]:
382    "of_int z = (numeral n :: 'a::ring_char_0)
383    \<longleftrightarrow> z = numeral n"
384   using of_int_eq_iff by fastforce
386 lemma of_int_le_numeral_iff [simp]:
387    "of_int z \<le> (numeral n :: 'a::linordered_idom)
388    \<longleftrightarrow> z \<le> numeral n"
389   using of_int_le_iff [of z "numeral n"] by simp
391 lemma of_int_numeral_le_iff [simp]:
392    "(numeral n :: 'a::linordered_idom) \<le> of_int z \<longleftrightarrow> numeral n \<le> z"
393   using of_int_le_iff [of "numeral n"] by simp
395 lemma of_int_less_numeral_iff [simp]:
396    "of_int z < (numeral n :: 'a::linordered_idom)
397    \<longleftrightarrow> z < numeral n"
398   using of_int_less_iff [of z "numeral n"] by simp
400 lemma of_int_numeral_less_iff [simp]:
401    "(numeral n :: 'a::linordered_idom) < of_int z \<longleftrightarrow> numeral n < z"
402   using of_int_less_iff [of "numeral n" z] by simp
404 lemma of_nat_less_of_int_iff:
405   "(of_nat n::'a::linordered_idom) < of_int x \<longleftrightarrow> int n < x"
406   by (metis of_int_of_nat_eq of_int_less_iff)
408 lemma of_int_eq_id [simp]: "of_int = id"
409 proof
410   fix z show "of_int z = id z"
411     by (cases z rule: int_diff_cases, simp)
412 qed
415 instance int :: no_top
416   apply standard
417   apply (rule_tac x="x + 1" in exI)
418   apply simp
419   done
421 instance int :: no_bot
422   apply standard
423   apply (rule_tac x="x - 1" in exI)
424   apply simp
425   done
427 subsection \<open>Magnitude of an Integer, as a Natural Number: \<open>nat\<close>\<close>
429 lift_definition nat :: "int \<Rightarrow> nat" is "\<lambda>(x, y). x - y"
430   by auto
432 lemma nat_int [simp]: "nat (int n) = n"
433   by transfer simp
435 lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
436   by transfer clarsimp
438 corollary nat_0_le: "0 \<le> z ==> int (nat z) = z"
439 by simp
441 lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
442   by transfer clarsimp
444 lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"
445   by transfer (clarsimp, arith)
447 text\<open>An alternative condition is @{term "0 \<le> w"}\<close>
448 corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
449 by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
451 corollary nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"
452 by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
454 lemma zless_nat_conj [simp]: "(nat w < nat z) = (0 < z & w < z)"
455   by transfer (clarsimp, arith)
457 lemma nonneg_eq_int:
458   fixes z :: int
459   assumes "0 \<le> z" and "\<And>m. z = int m \<Longrightarrow> P"
460   shows P
461   using assms by (blast dest: nat_0_le sym)
463 lemma nat_eq_iff:
464   "nat w = m \<longleftrightarrow> (if 0 \<le> w then w = int m else m = 0)"
465   by transfer (clarsimp simp add: le_imp_diff_is_add)
467 corollary nat_eq_iff2:
468   "m = nat w \<longleftrightarrow> (if 0 \<le> w then w = int m else m = 0)"
469   using nat_eq_iff [of w m] by auto
471 lemma nat_0 [simp]:
472   "nat 0 = 0"
473   by (simp add: nat_eq_iff)
475 lemma nat_1 [simp]:
476   "nat 1 = Suc 0"
477   by (simp add: nat_eq_iff)
479 lemma nat_numeral [simp]:
480   "nat (numeral k) = numeral k"
481   by (simp add: nat_eq_iff)
483 lemma nat_neg_numeral [simp]:
484   "nat (- numeral k) = 0"
485   by simp
487 lemma nat_2: "nat 2 = Suc (Suc 0)"
488   by simp
490 lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)"
491   by transfer (clarsimp, arith)
493 lemma nat_le_iff: "nat x \<le> n \<longleftrightarrow> x \<le> int n"
494   by transfer (clarsimp simp add: le_diff_conv)
496 lemma nat_mono: "x \<le> y \<Longrightarrow> nat x \<le> nat y"
497   by transfer auto
499 lemma nat_0_iff[simp]: "nat(i::int) = 0 \<longleftrightarrow> i\<le>0"
500   by transfer clarsimp
502 lemma int_eq_iff: "(of_nat m = z) = (m = nat z & 0 \<le> z)"
503 by (auto simp add: nat_eq_iff2)
505 lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)"
506 by (insert zless_nat_conj [of 0], auto)
509   "0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat (z + z') = nat z + nat z'"
510   by transfer clarsimp
512 lemma nat_diff_distrib':
513   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> nat (x - y) = nat x - nat y"
514   by transfer clarsimp
516 lemma nat_diff_distrib:
517   "0 \<le> z' \<Longrightarrow> z' \<le> z \<Longrightarrow> nat (z - z') = nat z - nat z'"
518   by (rule nat_diff_distrib') auto
520 lemma nat_zminus_int [simp]: "nat (- int n) = 0"
521   by transfer simp
523 lemma le_nat_iff:
524   "k \<ge> 0 \<Longrightarrow> n \<le> nat k \<longleftrightarrow> int n \<le> k"
525   by transfer auto
527 lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
528   by transfer (clarsimp simp add: less_diff_conv)
530 context ring_1
531 begin
533 lemma of_nat_nat [simp]: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z"
534   by transfer (clarsimp simp add: of_nat_diff)
536 end
538 lemma diff_nat_numeral [simp]:
539   "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
540   by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
543 text \<open>For termination proofs:\<close>
544 lemma measure_function_int[measure_function]: "is_measure (nat o abs)" ..
547 subsection\<open>Lemmas about the Function @{term of_nat} and Orderings\<close>
549 lemma negative_zless_0: "- (int (Suc n)) < (0 :: int)"
550 by (simp add: order_less_le del: of_nat_Suc)
552 lemma negative_zless [iff]: "- (int (Suc n)) < int m"
553 by (rule negative_zless_0 [THEN order_less_le_trans], simp)
555 lemma negative_zle_0: "- int n \<le> 0"
556 by (simp add: minus_le_iff)
558 lemma negative_zle [iff]: "- int n \<le> int m"
559 by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff])
561 lemma not_zle_0_negative [simp]: "~ (0 \<le> - (int (Suc n)))"
562 by (subst le_minus_iff, simp del: of_nat_Suc)
564 lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
565   by transfer simp
567 lemma not_int_zless_negative [simp]: "~ (int n < - int m)"
568 by (simp add: linorder_not_less)
570 lemma negative_eq_positive [simp]: "(- int n = of_nat m) = (n = 0 & m = 0)"
571 by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg)
574   "w \<le> z \<longleftrightarrow> (\<exists>n. z = w + int n)" (is "?P \<longleftrightarrow> ?Q")
575 proof
576   assume ?Q
577   then show ?P by auto
578 next
579   assume ?P
580   then have "0 \<le> z - w" by simp
581   then obtain n where "z - w = int n"
582     using zero_le_imp_eq_int [of "z - w"] by blast
583   then have "z = w + int n"
584     by simp
585   then show ?Q ..
586 qed
588 lemma zadd_int_left: "int m + (int n + z) = int (m + n) + z"
589 by simp
591 text\<open>This version is proved for all ordered rings, not just integers!
592       It is proved here because attribute \<open>arith_split\<close> is not available
593       in theory \<open>Rings\<close>.
594       But is it really better than just rewriting with \<open>abs_if\<close>?\<close>
595 lemma abs_split [arith_split, no_atp]:
596      "P \<bar>a::'a::linordered_idom\<bar> = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
597 by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
599 lemma negD: "x < 0 \<Longrightarrow> \<exists>n. x = - (int (Suc n))"
600 apply transfer
601 apply clarsimp
602 apply (rule_tac x="b - Suc a" in exI, arith)
603 done
605 subsection \<open>Cases and induction\<close>
607 text\<open>Now we replace the case analysis rule by a more conventional one:
608 whether an integer is negative or not.\<close>
610 text\<open>This version is symmetric in the two subgoals.\<close>
611 theorem int_cases2 [case_names nonneg nonpos, cases type: int]:
612   "\<lbrakk>!! n. z = int n \<Longrightarrow> P;  !! n. z = - (int n) \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
613 apply (cases "z < 0")
614 apply (auto simp add: linorder_not_less dest!: negD nat_0_le [THEN sym])
615 done
617 text\<open>This is the default, with a negative case.\<close>
618 theorem int_cases [case_names nonneg neg, cases type: int]:
619   "[|!! n. z = int n ==> P;  !! n. z = - (int (Suc n)) ==> P |] ==> P"
620 apply (cases "z < 0")
621 apply (blast dest!: negD)
622 apply (simp add: linorder_not_less del: of_nat_Suc)
623 apply auto
624 apply (blast dest: nat_0_le [THEN sym])
625 done
627 lemma int_cases3 [case_names zero pos neg]:
628   fixes k :: int
629   assumes "k = 0 \<Longrightarrow> P" and "\<And>n. k = int n \<Longrightarrow> n > 0 \<Longrightarrow> P"
630     and "\<And>n. k = - int n \<Longrightarrow> n > 0 \<Longrightarrow> P"
631   shows "P"
632 proof (cases k "0::int" rule: linorder_cases)
633   case equal with assms(1) show P by simp
634 next
635   case greater
636   then have "nat k > 0" by simp
637   moreover from this have "k = int (nat k)" by auto
638   ultimately show P using assms(2) by blast
639 next
640   case less
641   then have "nat (- k) > 0" by simp
642   moreover from this have "k = - int (nat (- k))" by auto
643   ultimately show P using assms(3) by blast
644 qed
646 theorem int_of_nat_induct [case_names nonneg neg, induct type: int]:
647      "[|!! n. P (int n);  !!n. P (- (int (Suc n))) |] ==> P z"
648   by (cases z) auto
650 lemma nonneg_int_cases:
651   assumes "0 \<le> k" obtains n where "k = int n"
652   using assms by (rule nonneg_eq_int)
654 lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
655   \<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close>
656   by (fact Let_numeral) \<comment> \<open>FIXME drop\<close>
658 lemma Let_neg_numeral [simp]: "Let (- numeral v) f = f (- numeral v)"
659   \<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close>
660   by (fact Let_neg_numeral) \<comment> \<open>FIXME drop\<close>
662 text \<open>Unfold \<open>min\<close> and \<open>max\<close> on numerals.\<close>
664 lemmas max_number_of [simp] =
665   max_def [of "numeral u" "numeral v"]
666   max_def [of "numeral u" "- numeral v"]
667   max_def [of "- numeral u" "numeral v"]
668   max_def [of "- numeral u" "- numeral v"] for u v
670 lemmas min_number_of [simp] =
671   min_def [of "numeral u" "numeral v"]
672   min_def [of "numeral u" "- numeral v"]
673   min_def [of "- numeral u" "numeral v"]
674   min_def [of "- numeral u" "- numeral v"] for u v
677 subsubsection \<open>Binary comparisons\<close>
679 text \<open>Preliminaries\<close>
681 lemma le_imp_0_less:
682   assumes le: "0 \<le> z"
683   shows "(0::int) < 1 + z"
684 proof -
685   have "0 \<le> z" by fact
686   also have "... < z + 1" by (rule less_add_one)
687   also have "... = 1 + z" by (simp add: ac_simps)
688   finally show "0 < 1 + z" .
689 qed
691 lemma odd_less_0_iff:
692   "(1 + z + z < 0) = (z < (0::int))"
693 proof (cases z)
694   case (nonneg n)
696                              le_imp_0_less [THEN order_less_imp_le])
697 next
698   case (neg n)
699   thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1
700     add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric])
701 qed
703 subsubsection \<open>Comparisons, for Ordered Rings\<close>
705 lemmas double_eq_0_iff = double_zero
707 lemma odd_nonzero:
708   "1 + z + z \<noteq> (0::int)"
709 proof (cases z)
710   case (nonneg n)
711   have le: "0 \<le> z+z" by (simp add: nonneg add_increasing)
712   thus ?thesis using  le_imp_0_less [OF le]
714 next
715   case (neg n)
716   show ?thesis
717   proof
718     assume eq: "1 + z + z = 0"
719     have "(0::int) < 1 + (int n + int n)"
721     also have "... = - (1 + z + z)"
722       by (simp add: neg add.assoc [symmetric])
723     also have "... = 0" by (simp add: eq)
724     finally have "0<0" ..
725     thus False by blast
726   qed
727 qed
730 subsection \<open>The Set of Integers\<close>
732 context ring_1
733 begin
735 definition Ints :: "'a set"  ("\<int>")
736   where "\<int> = range of_int"
738 lemma Ints_of_int [simp]: "of_int z \<in> \<int>"
739   by (simp add: Ints_def)
741 lemma Ints_of_nat [simp]: "of_nat n \<in> \<int>"
742   using Ints_of_int [of "of_nat n"] by simp
744 lemma Ints_0 [simp]: "0 \<in> \<int>"
745   using Ints_of_int [of "0"] by simp
747 lemma Ints_1 [simp]: "1 \<in> \<int>"
748   using Ints_of_int [of "1"] by simp
750 lemma Ints_numeral [simp]: "numeral n \<in> \<int>"
751   by (subst of_nat_numeral [symmetric], rule Ints_of_nat)
753 lemma Ints_add [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a + b \<in> \<int>"
754 apply (auto simp add: Ints_def)
755 apply (rule range_eqI)
756 apply (rule of_int_add [symmetric])
757 done
759 lemma Ints_minus [simp]: "a \<in> \<int> \<Longrightarrow> -a \<in> \<int>"
760 apply (auto simp add: Ints_def)
761 apply (rule range_eqI)
762 apply (rule of_int_minus [symmetric])
763 done
765 lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a - b \<in> \<int>"
766 apply (auto simp add: Ints_def)
767 apply (rule range_eqI)
768 apply (rule of_int_diff [symmetric])
769 done
771 lemma Ints_mult [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a * b \<in> \<int>"
772 apply (auto simp add: Ints_def)
773 apply (rule range_eqI)
774 apply (rule of_int_mult [symmetric])
775 done
777 lemma Ints_power [simp]: "a \<in> \<int> \<Longrightarrow> a ^ n \<in> \<int>"
778 by (induct n) simp_all
780 lemma Ints_cases [cases set: Ints]:
781   assumes "q \<in> \<int>"
782   obtains (of_int) z where "q = of_int z"
783   unfolding Ints_def
784 proof -
785   from \<open>q \<in> \<int>\<close> have "q \<in> range of_int" unfolding Ints_def .
786   then obtain z where "q = of_int z" ..
787   then show thesis ..
788 qed
790 lemma Ints_induct [case_names of_int, induct set: Ints]:
791   "q \<in> \<int> \<Longrightarrow> (\<And>z. P (of_int z)) \<Longrightarrow> P q"
792   by (rule Ints_cases) auto
794 lemma Nats_subset_Ints: "\<nat> \<subseteq> \<int>"
795   unfolding Nats_def Ints_def
796   by (rule subsetI, elim imageE, hypsubst, subst of_int_of_nat_eq[symmetric], rule imageI) simp_all
798 lemma Nats_altdef1: "\<nat> = {of_int n |n. n \<ge> 0}"
799 proof (intro subsetI equalityI)
800   fix x :: 'a assume "x \<in> {of_int n |n. n \<ge> 0}"
801   then obtain n where "x = of_int n" "n \<ge> 0" by (auto elim!: Ints_cases)
802   hence "x = of_nat (nat n)" by (subst of_nat_nat) simp_all
803   thus "x \<in> \<nat>" by simp
804 next
805   fix x :: 'a assume "x \<in> \<nat>"
806   then obtain n where "x = of_nat n" by (auto elim!: Nats_cases)
807   hence "x = of_int (int n)" by simp
808   also have "int n \<ge> 0" by simp
809   hence "of_int (int n) \<in> {of_int n |n. n \<ge> 0}" by blast
810   finally show "x \<in> {of_int n |n. n \<ge> 0}" .
811 qed
813 end
815 lemma (in linordered_idom) Nats_altdef2: "\<nat> = {n \<in> \<int>. n \<ge> 0}"
816 proof (intro subsetI equalityI)
817   fix x :: 'a assume "x \<in> {n \<in> \<int>. n \<ge> 0}"
818   then obtain n where "x = of_int n" "n \<ge> 0" by (auto elim!: Ints_cases)
819   hence "x = of_nat (nat n)" by (subst of_nat_nat) simp_all
820   thus "x \<in> \<nat>" by simp
821 qed (auto elim!: Nats_cases)
824 text \<open>The premise involving @{term Ints} prevents @{term "a = 1/2"}.\<close>
826 lemma Ints_double_eq_0_iff:
827   assumes in_Ints: "a \<in> \<int>"
828   shows "(a + a = 0) = (a = (0::'a::ring_char_0))"
829 proof -
830   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
831   then obtain z where a: "a = of_int z" ..
832   show ?thesis
833   proof
834     assume "a = 0"
835     thus "a + a = 0" by simp
836   next
837     assume eq: "a + a = 0"
838     hence "of_int (z + z) = (of_int 0 :: 'a)" by (simp add: a)
839     hence "z + z = 0" by (simp only: of_int_eq_iff)
840     hence "z = 0" by (simp only: double_eq_0_iff)
841     thus "a = 0" by (simp add: a)
842   qed
843 qed
845 lemma Ints_odd_nonzero:
846   assumes in_Ints: "a \<in> \<int>"
847   shows "1 + a + a \<noteq> (0::'a::ring_char_0)"
848 proof -
849   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
850   then obtain z where a: "a = of_int z" ..
851   show ?thesis
852   proof
853     assume eq: "1 + a + a = 0"
854     hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
855     hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
856     with odd_nonzero show False by blast
857   qed
858 qed
860 lemma Nats_numeral [simp]: "numeral w \<in> \<nat>"
861   using of_nat_in_Nats [of "numeral w"] by simp
863 lemma Ints_odd_less_0:
864   assumes in_Ints: "a \<in> \<int>"
865   shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))"
866 proof -
867   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
868   then obtain z where a: "a = of_int z" ..
869   hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
870     by (simp add: a)
871   also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0_iff)
872   also have "... = (a < 0)" by (simp add: a)
873   finally show ?thesis .
874 qed
877 subsection \<open>@{term setsum} and @{term setprod}\<close>
879 lemma of_nat_setsum [simp]: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
880   apply (cases "finite A")
881   apply (erule finite_induct, auto)
882   done
884 lemma of_int_setsum [simp]: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
885   apply (cases "finite A")
886   apply (erule finite_induct, auto)
887   done
889 lemma of_nat_setprod [simp]: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
890   apply (cases "finite A")
891   apply (erule finite_induct, auto simp add: of_nat_mult)
892   done
894 lemma of_int_setprod [simp]: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
895   apply (cases "finite A")
896   apply (erule finite_induct, auto)
897   done
899 lemmas int_setsum = of_nat_setsum [where 'a=int]
900 lemmas int_setprod = of_nat_setprod [where 'a=int]
903 text \<open>Legacy theorems\<close>
905 lemmas zle_int = of_nat_le_iff [where 'a=int]
906 lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
908 subsection \<open>Setting up simplification procedures\<close>
910 lemmas of_int_simps =
911   of_int_0 of_int_1 of_int_add of_int_mult
913 ML_file "Tools/int_arith.ML"
914 declaration \<open>K Int_Arith.setup\<close>
916 simproc_setup fast_arith ("(m::'a::linordered_idom) < n" |
917   "(m::'a::linordered_idom) \<le> n" |
918   "(m::'a::linordered_idom) = n") =
919   \<open>K Lin_Arith.simproc\<close>
922 subsection\<open>More Inequality Reasoning\<close>
924 lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
925 by arith
927 lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
928 by arith
930 lemma zle_diff1_eq [simp]: "(w \<le> z - (1::int)) = (w<z)"
931 by arith
933 lemma zle_add1_eq_le [simp]: "(w < z + (1::int)) = (w\<le>z)"
934 by arith
936 lemma int_one_le_iff_zero_less: "((1::int) \<le> z) = (0 < z)"
937 by arith
940 subsection\<open>The functions @{term nat} and @{term int}\<close>
942 text\<open>Simplify the term @{term "w + - z"}\<close>
944 lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
945   using zless_nat_conj [of 1 z] by auto
947 text\<open>This simplifies expressions of the form @{term "int n = z"} where
948       z is an integer literal.\<close>
949 lemmas int_eq_iff_numeral [simp] = int_eq_iff [of _ "numeral v"] for v
951 lemma split_nat [arith_split]:
952   "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
953   (is "?P = (?L & ?R)")
954 proof (cases "i < 0")
955   case True thus ?thesis by auto
956 next
957   case False
958   have "?P = ?L"
959   proof
960     assume ?P thus ?L using False by clarsimp
961   next
962     assume ?L thus ?P using False by simp
963   qed
964   with False show ?thesis by simp
965 qed
967 lemma nat_abs_int_diff: "nat \<bar>int a - int b\<bar> = (if a \<le> b then b - a else a - b)"
968   by auto
970 lemma nat_int_add: "nat (int a + int b) = a + b"
971   by auto
973 context ring_1
974 begin
976 lemma of_int_of_nat [nitpick_simp]:
977   "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))"
978 proof (cases "k < 0")
979   case True then have "0 \<le> - k" by simp
980   then have "of_nat (nat (- k)) = of_int (- k)" by (rule of_nat_nat)
981   with True show ?thesis by simp
982 next
983   case False then show ?thesis by (simp add: not_less of_nat_nat)
984 qed
986 end
988 lemma nat_mult_distrib:
989   fixes z z' :: int
990   assumes "0 \<le> z"
991   shows "nat (z * z') = nat z * nat z'"
992 proof (cases "0 \<le> z'")
993   case False with assms have "z * z' \<le> 0"
994     by (simp add: not_le mult_le_0_iff)
995   then have "nat (z * z') = 0" by simp
996   moreover from False have "nat z' = 0" by simp
997   ultimately show ?thesis by simp
998 next
999   case True with assms have ge_0: "z * z' \<ge> 0" by (simp add: zero_le_mult_iff)
1000   show ?thesis
1001     by (rule injD [of "of_nat :: nat \<Rightarrow> int", OF inj_of_nat])
1002       (simp only: of_nat_mult of_nat_nat [OF True]
1003          of_nat_nat [OF assms] of_nat_nat [OF ge_0], simp)
1004 qed
1006 lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"
1007 apply (rule trans)
1008 apply (rule_tac  nat_mult_distrib, auto)
1009 done
1011 lemma nat_abs_mult_distrib: "nat \<bar>w * z\<bar> = nat \<bar>w\<bar> * nat \<bar>z\<bar>"
1012 apply (cases "z=0 | w=0")
1013 apply (auto simp add: abs_if nat_mult_distrib [symmetric]
1014                       nat_mult_distrib_neg [symmetric] mult_less_0_iff)
1015 done
1017 lemma int_in_range_abs [simp]:
1018   "int n \<in> range abs"
1019 proof (rule range_eqI)
1020   show "int n = \<bar>int n\<bar>"
1021     by simp
1022 qed
1024 lemma range_abs_Nats [simp]:
1025   "range abs = (\<nat> :: int set)"
1026 proof -
1027   have "\<bar>k\<bar> \<in> \<nat>" for k :: int
1028     by (cases k) simp_all
1029   moreover have "k \<in> range abs" if "k \<in> \<nat>" for k :: int
1030     using that by induct simp
1031   ultimately show ?thesis by blast
1032 qed
1034 lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
1035 apply (rule sym)
1036 apply (simp add: nat_eq_iff)
1037 done
1039 lemma diff_nat_eq_if:
1040      "nat z - nat z' =
1041         (if z' < 0 then nat z
1042          else let d = z-z' in
1043               if d < 0 then 0 else nat d)"
1044 by (simp add: Let_def nat_diff_distrib [symmetric])
1046 lemma nat_numeral_diff_1 [simp]:
1047   "numeral v - (1::nat) = nat (numeral v - 1)"
1048   using diff_nat_numeral [of v Num.One] by simp
1051 subsection "Induction principles for int"
1053 text\<open>Well-founded segments of the integers\<close>
1055 definition
1056   int_ge_less_than  ::  "int => (int * int) set"
1057 where
1058   "int_ge_less_than d = {(z',z). d \<le> z' & z' < z}"
1060 theorem wf_int_ge_less_than: "wf (int_ge_less_than d)"
1061 proof -
1062   have "int_ge_less_than d \<subseteq> measure (%z. nat (z-d))"
1063     by (auto simp add: int_ge_less_than_def)
1064   thus ?thesis
1065     by (rule wf_subset [OF wf_measure])
1066 qed
1068 text\<open>This variant looks odd, but is typical of the relations suggested
1069 by RankFinder.\<close>
1071 definition
1072   int_ge_less_than2 ::  "int => (int * int) set"
1073 where
1074   "int_ge_less_than2 d = {(z',z). d \<le> z & z' < z}"
1076 theorem wf_int_ge_less_than2: "wf (int_ge_less_than2 d)"
1077 proof -
1078   have "int_ge_less_than2 d \<subseteq> measure (%z. nat (1+z-d))"
1079     by (auto simp add: int_ge_less_than2_def)
1080   thus ?thesis
1081     by (rule wf_subset [OF wf_measure])
1082 qed
1084 (* `set:int': dummy construction *)
1085 theorem int_ge_induct [case_names base step, induct set: int]:
1086   fixes i :: int
1087   assumes ge: "k \<le> i" and
1088     base: "P k" and
1089     step: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
1090   shows "P i"
1091 proof -
1092   { fix n
1093     have "\<And>i::int. n = nat (i - k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i"
1094     proof (induct n)
1095       case 0
1096       hence "i = k" by arith
1097       thus "P i" using base by simp
1098     next
1099       case (Suc n)
1100       then have "n = nat((i - 1) - k)" by arith
1101       moreover
1102       have ki1: "k \<le> i - 1" using Suc.prems by arith
1103       ultimately
1104       have "P (i - 1)" by (rule Suc.hyps)
1105       from step [OF ki1 this] show ?case by simp
1106     qed
1107   }
1108   with ge show ?thesis by fast
1109 qed
1111 (* `set:int': dummy construction *)
1112 theorem int_gr_induct [case_names base step, induct set: int]:
1113   assumes gr: "k < (i::int)" and
1114         base: "P(k+1)" and
1115         step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
1116   shows "P i"
1117 apply(rule int_ge_induct[of "k + 1"])
1118   using gr apply arith
1119  apply(rule base)
1120 apply (rule step, simp+)
1121 done
1123 theorem int_le_induct [consumes 1, case_names base step]:
1124   assumes le: "i \<le> (k::int)" and
1125         base: "P(k)" and
1126         step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
1127   shows "P i"
1128 proof -
1129   { fix n
1130     have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i"
1131     proof (induct n)
1132       case 0
1133       hence "i = k" by arith
1134       thus "P i" using base by simp
1135     next
1136       case (Suc n)
1137       hence "n = nat (k - (i + 1))" by arith
1138       moreover
1139       have ki1: "i + 1 \<le> k" using Suc.prems by arith
1140       ultimately
1141       have "P (i + 1)" by(rule Suc.hyps)
1142       from step[OF ki1 this] show ?case by simp
1143     qed
1144   }
1145   with le show ?thesis by fast
1146 qed
1148 theorem int_less_induct [consumes 1, case_names base step]:
1149   assumes less: "(i::int) < k" and
1150         base: "P(k - 1)" and
1151         step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
1152   shows "P i"
1153 apply(rule int_le_induct[of _ "k - 1"])
1154   using less apply arith
1155  apply(rule base)
1156 apply (rule step, simp+)
1157 done
1159 theorem int_induct [case_names base step1 step2]:
1160   fixes k :: int
1161   assumes base: "P k"
1162     and step1: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
1163     and step2: "\<And>i. k \<ge> i \<Longrightarrow> P i \<Longrightarrow> P (i - 1)"
1164   shows "P i"
1165 proof -
1166   have "i \<le> k \<or> i \<ge> k" by arith
1167   then show ?thesis
1168   proof
1169     assume "i \<ge> k"
1170     then show ?thesis using base
1171       by (rule int_ge_induct) (fact step1)
1172   next
1173     assume "i \<le> k"
1174     then show ?thesis using base
1175       by (rule int_le_induct) (fact step2)
1176   qed
1177 qed
1179 subsection\<open>Intermediate value theorems\<close>
1181 lemma int_val_lemma:
1182      "(\<forall>i<n::nat. \<bar>f(i+1) - f i\<bar> \<le> 1) -->
1183       f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
1184 unfolding One_nat_def
1185 apply (induct n)
1186 apply simp
1187 apply (intro strip)
1188 apply (erule impE, simp)
1189 apply (erule_tac x = n in allE, simp)
1190 apply (case_tac "k = f (Suc n)")
1191 apply force
1192 apply (erule impE)
1193  apply (simp add: abs_if split add: split_if_asm)
1194 apply (blast intro: le_SucI)
1195 done
1197 lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
1199 lemma nat_intermed_int_val:
1200      "[| \<forall>i. m \<le> i & i < n --> \<bar>f(i + 1::nat) - f i\<bar> \<le> 1; m < n;
1201          f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
1202 apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k
1203        in int_val_lemma)
1204 unfolding One_nat_def
1205 apply simp
1206 apply (erule exE)
1207 apply (rule_tac x = "i+m" in exI, arith)
1208 done
1211 subsection\<open>Products and 1, by T. M. Rasmussen\<close>
1213 lemma abs_zmult_eq_1:
1214   assumes mn: "\<bar>m * n\<bar> = 1"
1215   shows "\<bar>m\<bar> = (1::int)"
1216 proof -
1217   have 0: "m \<noteq> 0 & n \<noteq> 0" using mn
1218     by auto
1219   have "~ (2 \<le> \<bar>m\<bar>)"
1220   proof
1221     assume "2 \<le> \<bar>m\<bar>"
1222     hence "2*\<bar>n\<bar> \<le> \<bar>m\<bar>*\<bar>n\<bar>"
1223       by (simp add: mult_mono 0)
1224     also have "... = \<bar>m*n\<bar>"
1225       by (simp add: abs_mult)
1226     also have "... = 1"
1227       by (simp add: mn)
1228     finally have "2*\<bar>n\<bar> \<le> 1" .
1229     thus "False" using 0
1230       by arith
1231   qed
1232   thus ?thesis using 0
1233     by auto
1234 qed
1236 lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1"
1237 by (insert abs_zmult_eq_1 [of m n], arith)
1239 lemma pos_zmult_eq_1_iff:
1240   assumes "0 < (m::int)" shows "(m * n = 1) = (m = 1 & n = 1)"
1241 proof -
1242   from assms have "m * n = 1 ==> m = 1" by (auto dest: pos_zmult_eq_1_iff_lemma)
1243   thus ?thesis by (auto dest: pos_zmult_eq_1_iff_lemma)
1244 qed
1246 lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
1247 apply (rule iffI)
1248  apply (frule pos_zmult_eq_1_iff_lemma)
1249  apply (simp add: mult.commute [of m])
1250  apply (frule pos_zmult_eq_1_iff_lemma, auto)
1251 done
1253 lemma infinite_UNIV_int: "\<not> finite (UNIV::int set)"
1254 proof
1255   assume "finite (UNIV::int set)"
1256   moreover have "inj (\<lambda>i::int. 2 * i)"
1257     by (rule injI) simp
1258   ultimately have "surj (\<lambda>i::int. 2 * i)"
1259     by (rule finite_UNIV_inj_surj)
1260   then obtain i :: int where "1 = 2 * i" by (rule surjE)
1261   then show False by (simp add: pos_zmult_eq_1_iff)
1262 qed
1265 subsection \<open>Further theorems on numerals\<close>
1267 subsubsection\<open>Special Simplification for Constants\<close>
1269 text\<open>These distributive laws move literals inside sums and differences.\<close>
1271 lemmas distrib_right_numeral [simp] = distrib_right [of _ _ "numeral v"] for v
1272 lemmas distrib_left_numeral [simp] = distrib_left [of "numeral v"] for v
1273 lemmas left_diff_distrib_numeral [simp] = left_diff_distrib [of _ _ "numeral v"] for v
1274 lemmas right_diff_distrib_numeral [simp] = right_diff_distrib [of "numeral v"] for v
1276 text\<open>These are actually for fields, like real: but where else to put them?\<close>
1278 lemmas zero_less_divide_iff_numeral [simp, no_atp] = zero_less_divide_iff [of "numeral w"] for w
1279 lemmas divide_less_0_iff_numeral [simp, no_atp] = divide_less_0_iff [of "numeral w"] for w
1280 lemmas zero_le_divide_iff_numeral [simp, no_atp] = zero_le_divide_iff [of "numeral w"] for w
1281 lemmas divide_le_0_iff_numeral [simp, no_atp] = divide_le_0_iff [of "numeral w"] for w
1284 text \<open>Replaces \<open>inverse #nn\<close> by \<open>1/#nn\<close>.  It looks
1285   strange, but then other simprocs simplify the quotient.\<close>
1287 lemmas inverse_eq_divide_numeral [simp] =
1288   inverse_eq_divide [of "numeral w"] for w
1290 lemmas inverse_eq_divide_neg_numeral [simp] =
1291   inverse_eq_divide [of "- numeral w"] for w
1293 text \<open>These laws simplify inequalities, moving unary minus from a term
1294 into the literal.\<close>
1296 lemmas equation_minus_iff_numeral [no_atp] =
1297   equation_minus_iff [of "numeral v"] for v
1299 lemmas minus_equation_iff_numeral [no_atp] =
1300   minus_equation_iff [of _ "numeral v"] for v
1302 lemmas le_minus_iff_numeral [no_atp] =
1303   le_minus_iff [of "numeral v"] for v
1305 lemmas minus_le_iff_numeral [no_atp] =
1306   minus_le_iff [of _ "numeral v"] for v
1308 lemmas less_minus_iff_numeral [no_atp] =
1309   less_minus_iff [of "numeral v"] for v
1311 lemmas minus_less_iff_numeral [no_atp] =
1312   minus_less_iff [of _ "numeral v"] for v
1314 \<comment> \<open>FIXME maybe simproc\<close>
1317 text \<open>Cancellation of constant factors in comparisons (\<open><\<close> and \<open>\<le>\<close>)\<close>
1319 lemmas mult_less_cancel_left_numeral [simp, no_atp] = mult_less_cancel_left [of "numeral v"] for v
1320 lemmas mult_less_cancel_right_numeral [simp, no_atp] = mult_less_cancel_right [of _ "numeral v"] for v
1321 lemmas mult_le_cancel_left_numeral [simp, no_atp] = mult_le_cancel_left [of "numeral v"] for v
1322 lemmas mult_le_cancel_right_numeral [simp, no_atp] = mult_le_cancel_right [of _ "numeral v"] for v
1325 text \<open>Multiplying out constant divisors in comparisons (\<open><\<close>, \<open>\<le>\<close> and \<open>=\<close>)\<close>
1327 named_theorems divide_const_simps "simplification rules to simplify comparisons involving constant divisors"
1329 lemmas le_divide_eq_numeral1 [simp,divide_const_simps] =
1330   pos_le_divide_eq [of "numeral w", OF zero_less_numeral]
1331   neg_le_divide_eq [of "- numeral w", OF neg_numeral_less_zero] for w
1333 lemmas divide_le_eq_numeral1 [simp,divide_const_simps] =
1334   pos_divide_le_eq [of "numeral w", OF zero_less_numeral]
1335   neg_divide_le_eq [of "- numeral w", OF neg_numeral_less_zero] for w
1337 lemmas less_divide_eq_numeral1 [simp,divide_const_simps] =
1338   pos_less_divide_eq [of "numeral w", OF zero_less_numeral]
1339   neg_less_divide_eq [of "- numeral w", OF neg_numeral_less_zero] for w
1341 lemmas divide_less_eq_numeral1 [simp,divide_const_simps] =
1342   pos_divide_less_eq [of "numeral w", OF zero_less_numeral]
1343   neg_divide_less_eq [of "- numeral w", OF neg_numeral_less_zero] for w
1345 lemmas eq_divide_eq_numeral1 [simp,divide_const_simps] =
1346   eq_divide_eq [of _ _ "numeral w"]
1347   eq_divide_eq [of _ _ "- numeral w"] for w
1349 lemmas divide_eq_eq_numeral1 [simp,divide_const_simps] =
1350   divide_eq_eq [of _ "numeral w"]
1351   divide_eq_eq [of _ "- numeral w"] for w
1354 subsubsection\<open>Optional Simplification Rules Involving Constants\<close>
1356 text\<open>Simplify quotients that are compared with a literal constant.\<close>
1358 lemmas le_divide_eq_numeral [divide_const_simps] =
1359   le_divide_eq [of "numeral w"]
1360   le_divide_eq [of "- numeral w"] for w
1362 lemmas divide_le_eq_numeral [divide_const_simps] =
1363   divide_le_eq [of _ _ "numeral w"]
1364   divide_le_eq [of _ _ "- numeral w"] for w
1366 lemmas less_divide_eq_numeral [divide_const_simps] =
1367   less_divide_eq [of "numeral w"]
1368   less_divide_eq [of "- numeral w"] for w
1370 lemmas divide_less_eq_numeral [divide_const_simps] =
1371   divide_less_eq [of _ _ "numeral w"]
1372   divide_less_eq [of _ _ "- numeral w"] for w
1374 lemmas eq_divide_eq_numeral [divide_const_simps] =
1375   eq_divide_eq [of "numeral w"]
1376   eq_divide_eq [of "- numeral w"] for w
1378 lemmas divide_eq_eq_numeral [divide_const_simps] =
1379   divide_eq_eq [of _ _ "numeral w"]
1380   divide_eq_eq [of _ _ "- numeral w"] for w
1383 text\<open>Not good as automatic simprules because they cause case splits.\<close>
1384 lemmas [divide_const_simps] = le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
1387 subsection \<open>The divides relation\<close>
1389 lemma zdvd_antisym_nonneg:
1390     "0 <= m ==> 0 <= n ==> m dvd n ==> n dvd m ==> m = (n::int)"
1391   apply (simp add: dvd_def, auto)
1392   apply (auto simp add: mult.assoc zero_le_mult_iff zmult_eq_1_iff)
1393   done
1395 lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a"
1396   shows "\<bar>a\<bar> = \<bar>b\<bar>"
1397 proof cases
1398   assume "a = 0" with assms show ?thesis by simp
1399 next
1400   assume "a \<noteq> 0"
1401   from \<open>a dvd b\<close> obtain k where k:"b = a*k" unfolding dvd_def by blast
1402   from \<open>b dvd a\<close> obtain k' where k':"a = b*k'" unfolding dvd_def by blast
1403   from k k' have "a = a*k*k'" by simp
1404   with mult_cancel_left1[where c="a" and b="k*k'"]
1405   have kk':"k*k' = 1" using \<open>a\<noteq>0\<close> by (simp add: mult.assoc)
1406   hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff)
1407   thus ?thesis using k k' by auto
1408 qed
1410 lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
1411   using dvd_add_right_iff [of k "- n" m] by simp
1413 lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
1414   using dvd_add_times_triv_right_iff [of k n m] by (simp add: ac_simps)
1416 lemma dvd_imp_le_int:
1417   fixes d i :: int
1418   assumes "i \<noteq> 0" and "d dvd i"
1419   shows "\<bar>d\<bar> \<le> \<bar>i\<bar>"
1420 proof -
1421   from \<open>d dvd i\<close> obtain k where "i = d * k" ..
1422   with \<open>i \<noteq> 0\<close> have "k \<noteq> 0" by auto
1423   then have "1 \<le> \<bar>k\<bar>" and "0 \<le> \<bar>d\<bar>" by auto
1424   then have "\<bar>d\<bar> * 1 \<le> \<bar>d\<bar> * \<bar>k\<bar>" by (rule mult_left_mono)
1425   with \<open>i = d * k\<close> show ?thesis by (simp add: abs_mult)
1426 qed
1428 lemma zdvd_not_zless:
1429   fixes m n :: int
1430   assumes "0 < m" and "m < n"
1431   shows "\<not> n dvd m"
1432 proof
1433   from assms have "0 < n" by auto
1434   assume "n dvd m" then obtain k where k: "m = n * k" ..
1435   with \<open>0 < m\<close> have "0 < n * k" by auto
1436   with \<open>0 < n\<close> have "0 < k" by (simp add: zero_less_mult_iff)
1437   with k \<open>0 < n\<close> \<open>m < n\<close> have "n * k < n * 1" by simp
1438   with \<open>0 < n\<close> \<open>0 < k\<close> show False unfolding mult_less_cancel_left by auto
1439 qed
1441 lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)"
1442   shows "m dvd n"
1443 proof-
1444   from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast
1445   {assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp
1446     with h have False by (simp add: mult.assoc)}
1447   hence "n = m * h" by blast
1448   thus ?thesis by simp
1449 qed
1451 theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
1452 proof -
1453   have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"
1454   proof -
1455     fix k
1456     assume A: "int y = int x * k"
1457     then show "x dvd y"
1458     proof (cases k)
1459       case (nonneg n)
1460       with A have "y = x * n" by (simp del: of_nat_mult add: of_nat_mult [symmetric])
1461       then show ?thesis ..
1462     next
1463       case (neg n)
1464       with A have "int y = int x * (- int (Suc n))" by simp
1465       also have "\<dots> = - (int x * int (Suc n))" by (simp only: mult_minus_right)
1466       also have "\<dots> = - int (x * Suc n)" by (simp only: of_nat_mult [symmetric])
1467       finally have "- int (x * Suc n) = int y" ..
1468       then show ?thesis by (simp only: negative_eq_positive) auto
1469     qed
1470   qed
1471   then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left of_nat_mult)
1472 qed
1474 lemma zdvd1_eq[simp]: "(x::int) dvd 1 = (\<bar>x\<bar> = 1)"
1475 proof
1476   assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp
1477   hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
1478   hence "nat \<bar>x\<bar> = 1"  by simp
1479   thus "\<bar>x\<bar> = 1" by (cases "x < 0") auto
1480 next
1481   assume "\<bar>x\<bar>=1"
1482   then have "x = 1 \<or> x = -1" by auto
1483   then show "x dvd 1" by (auto intro: dvdI)
1484 qed
1486 lemma zdvd_mult_cancel1:
1487   assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
1488 proof
1489   assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m"
1490     by (cases "n >0") (auto simp add: minus_equation_iff)
1491 next
1492   assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
1493   from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
1494 qed
1496 lemma int_dvd_iff: "(int m dvd z) = (m dvd nat \<bar>z\<bar>)"
1497   unfolding zdvd_int by (cases "z \<ge> 0") simp_all
1499 lemma dvd_int_iff: "(z dvd int m) = (nat \<bar>z\<bar> dvd m)"
1500   unfolding zdvd_int by (cases "z \<ge> 0") simp_all
1502 lemma dvd_int_unfold_dvd_nat:
1503   "k dvd l \<longleftrightarrow> nat \<bar>k\<bar> dvd nat \<bar>l\<bar>"
1504   unfolding dvd_int_iff [symmetric] by simp
1506 lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
1507   by (auto simp add: dvd_int_iff)
1509 lemma eq_nat_nat_iff:
1510   "0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat z = nat z' \<longleftrightarrow> z = z'"
1511   by (auto elim!: nonneg_eq_int)
1513 lemma nat_power_eq:
1514   "0 \<le> z \<Longrightarrow> nat (z ^ n) = nat z ^ n"
1515   by (induct n) (simp_all add: nat_mult_distrib)
1517 lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
1518   apply (cases n)
1519   apply (auto simp add: dvd_int_iff)
1520   apply (cases z)
1521   apply (auto simp add: dvd_imp_le)
1522   done
1524 lemma zdvd_period:
1525   fixes a d :: int
1526   assumes "a dvd d"
1527   shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)"
1528 proof -
1529   from assms obtain k where "d = a * k" by (rule dvdE)
1530   show ?thesis
1531   proof
1532     assume "a dvd (x + t)"
1533     then obtain l where "x + t = a * l" by (rule dvdE)
1534     then have "x = a * l - t" by simp
1535     with \<open>d = a * k\<close> show "a dvd x + c * d + t" by simp
1536   next
1537     assume "a dvd x + c * d + t"
1538     then obtain l where "x + c * d + t = a * l" by (rule dvdE)
1539     then have "x = a * l - c * d - t" by simp
1540     with \<open>d = a * k\<close> show "a dvd (x + t)" by simp
1541   qed
1542 qed
1545 subsection \<open>Finiteness of intervals\<close>
1547 lemma finite_interval_int1 [iff]: "finite {i :: int. a <= i & i <= b}"
1548 proof (cases "a <= b")
1549   case True
1550   from this show ?thesis
1551   proof (induct b rule: int_ge_induct)
1552     case base
1553     have "{i. a <= i & i <= a} = {a}" by auto
1554     from this show ?case by simp
1555   next
1556     case (step b)
1557     from this have "{i. a <= i & i <= b + 1} = {i. a <= i & i <= b} \<union> {b + 1}" by auto
1558     from this step show ?case by simp
1559   qed
1560 next
1561   case False from this show ?thesis
1562     by (metis (lifting, no_types) Collect_empty_eq finite.emptyI order_trans)
1563 qed
1565 lemma finite_interval_int2 [iff]: "finite {i :: int. a <= i & i < b}"
1566 by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
1568 lemma finite_interval_int3 [iff]: "finite {i :: int. a < i & i <= b}"
1569 by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
1571 lemma finite_interval_int4 [iff]: "finite {i :: int. a < i & i < b}"
1572 by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
1575 subsection \<open>Configuration of the code generator\<close>
1577 text \<open>Constructors\<close>
1579 definition Pos :: "num \<Rightarrow> int" where
1580   [simp, code_abbrev]: "Pos = numeral"
1582 definition Neg :: "num \<Rightarrow> int" where
1583   [simp, code_abbrev]: "Neg n = - (Pos n)"
1585 code_datatype "0::int" Pos Neg
1588 text \<open>Auxiliary operations\<close>
1590 definition dup :: "int \<Rightarrow> int" where
1591   [simp]: "dup k = k + k"
1593 lemma dup_code [code]:
1594   "dup 0 = 0"
1595   "dup (Pos n) = Pos (Num.Bit0 n)"
1596   "dup (Neg n) = Neg (Num.Bit0 n)"
1597   unfolding Pos_def Neg_def
1598   by (simp_all add: numeral_Bit0)
1600 definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
1601   [simp]: "sub m n = numeral m - numeral n"
1603 lemma sub_code [code]:
1604   "sub Num.One Num.One = 0"
1605   "sub (Num.Bit0 m) Num.One = Pos (Num.BitM m)"
1606   "sub (Num.Bit1 m) Num.One = Pos (Num.Bit0 m)"
1607   "sub Num.One (Num.Bit0 n) = Neg (Num.BitM n)"
1608   "sub Num.One (Num.Bit1 n) = Neg (Num.Bit0 n)"
1609   "sub (Num.Bit0 m) (Num.Bit0 n) = dup (sub m n)"
1610   "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)"
1611   "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1"
1612   "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1"
1613   apply (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def numeral_BitM)
1614   apply (simp_all only: algebra_simps minus_diff_eq)
1615   apply (simp_all only: add.commute [of _ "- (numeral n + numeral n)"])
1616   apply (simp_all only: minus_add add.assoc left_minus)
1617   done
1619 text \<open>Implementations\<close>
1621 lemma one_int_code [code, code_unfold]:
1622   "1 = Pos Num.One"
1623   by simp
1625 lemma plus_int_code [code]:
1626   "k + 0 = (k::int)"
1627   "0 + l = (l::int)"
1628   "Pos m + Pos n = Pos (m + n)"
1629   "Pos m + Neg n = sub m n"
1630   "Neg m + Pos n = sub n m"
1631   "Neg m + Neg n = Neg (m + n)"
1632   by simp_all
1634 lemma uminus_int_code [code]:
1635   "uminus 0 = (0::int)"
1636   "uminus (Pos m) = Neg m"
1637   "uminus (Neg m) = Pos m"
1638   by simp_all
1640 lemma minus_int_code [code]:
1641   "k - 0 = (k::int)"
1642   "0 - l = uminus (l::int)"
1643   "Pos m - Pos n = sub m n"
1644   "Pos m - Neg n = Pos (m + n)"
1645   "Neg m - Pos n = Neg (m + n)"
1646   "Neg m - Neg n = sub n m"
1647   by simp_all
1649 lemma times_int_code [code]:
1650   "k * 0 = (0::int)"
1651   "0 * l = (0::int)"
1652   "Pos m * Pos n = Pos (m * n)"
1653   "Pos m * Neg n = Neg (m * n)"
1654   "Neg m * Pos n = Neg (m * n)"
1655   "Neg m * Neg n = Pos (m * n)"
1656   by simp_all
1658 instantiation int :: equal
1659 begin
1661 definition
1662   "HOL.equal k l \<longleftrightarrow> k = (l::int)"
1664 instance
1665   by standard (rule equal_int_def)
1667 end
1669 lemma equal_int_code [code]:
1670   "HOL.equal 0 (0::int) \<longleftrightarrow> True"
1671   "HOL.equal 0 (Pos l) \<longleftrightarrow> False"
1672   "HOL.equal 0 (Neg l) \<longleftrightarrow> False"
1673   "HOL.equal (Pos k) 0 \<longleftrightarrow> False"
1674   "HOL.equal (Pos k) (Pos l) \<longleftrightarrow> HOL.equal k l"
1675   "HOL.equal (Pos k) (Neg l) \<longleftrightarrow> False"
1676   "HOL.equal (Neg k) 0 \<longleftrightarrow> False"
1677   "HOL.equal (Neg k) (Pos l) \<longleftrightarrow> False"
1678   "HOL.equal (Neg k) (Neg l) \<longleftrightarrow> HOL.equal k l"
1679   by (auto simp add: equal)
1681 lemma equal_int_refl [code nbe]:
1682   "HOL.equal (k::int) k \<longleftrightarrow> True"
1683   by (fact equal_refl)
1685 lemma less_eq_int_code [code]:
1686   "0 \<le> (0::int) \<longleftrightarrow> True"
1687   "0 \<le> Pos l \<longleftrightarrow> True"
1688   "0 \<le> Neg l \<longleftrightarrow> False"
1689   "Pos k \<le> 0 \<longleftrightarrow> False"
1690   "Pos k \<le> Pos l \<longleftrightarrow> k \<le> l"
1691   "Pos k \<le> Neg l \<longleftrightarrow> False"
1692   "Neg k \<le> 0 \<longleftrightarrow> True"
1693   "Neg k \<le> Pos l \<longleftrightarrow> True"
1694   "Neg k \<le> Neg l \<longleftrightarrow> l \<le> k"
1695   by simp_all
1697 lemma less_int_code [code]:
1698   "0 < (0::int) \<longleftrightarrow> False"
1699   "0 < Pos l \<longleftrightarrow> True"
1700   "0 < Neg l \<longleftrightarrow> False"
1701   "Pos k < 0 \<longleftrightarrow> False"
1702   "Pos k < Pos l \<longleftrightarrow> k < l"
1703   "Pos k < Neg l \<longleftrightarrow> False"
1704   "Neg k < 0 \<longleftrightarrow> True"
1705   "Neg k < Pos l \<longleftrightarrow> True"
1706   "Neg k < Neg l \<longleftrightarrow> l < k"
1707   by simp_all
1709 lemma nat_code [code]:
1710   "nat (Int.Neg k) = 0"
1711   "nat 0 = 0"
1712   "nat (Int.Pos k) = nat_of_num k"
1713   by (simp_all add: nat_of_num_numeral)
1715 lemma (in ring_1) of_int_code [code]:
1716   "of_int (Int.Neg k) = - numeral k"
1717   "of_int 0 = 0"
1718   "of_int (Int.Pos k) = numeral k"
1719   by simp_all
1722 text \<open>Serializer setup\<close>
1724 code_identifier
1725   code_module Int \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
1727 quickcheck_params [default_type = int]
1729 hide_const (open) Pos Neg sub dup
1732 text \<open>De-register \<open>int\<close> as a quotient type:\<close>
1734 lifting_update int.lifting
1735 lifting_forget int.lifting
1737 end