src/HOL/Int.thy
 author haftmann Wed Feb 17 21:51:57 2016 +0100 (2016-02-17) changeset 62347 2230b7047376 parent 62128 3201ddb00097 child 62348 9a5f43dac883 permissions -rw-r--r--
generalized some lemmas;
moved some lemmas in more appropriate places;
deleted potentially dangerous simp rule
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)
573 lemma zle_iff_zadd: "w \<le> z \<longleftrightarrow> (\<exists>n. z = w + int n)"
574 proof -
575   have "(w \<le> z) = (0 \<le> z - w)"
576     by (simp only: le_diff_eq add_0_left)
577   also have "\<dots> = (\<exists>n. z - w = of_nat n)"
578     by (auto elim: zero_le_imp_eq_int)
579   also have "\<dots> = (\<exists>n. z = w + of_nat n)"
580     by (simp only: algebra_simps)
581   finally show ?thesis .
582 qed
584 lemma zadd_int_left: "int m + (int n + z) = int (m + n) + z"
585 by simp
587 text\<open>This version is proved for all ordered rings, not just integers!
588       It is proved here because attribute \<open>arith_split\<close> is not available
589       in theory \<open>Rings\<close>.
590       But is it really better than just rewriting with \<open>abs_if\<close>?\<close>
591 lemma abs_split [arith_split, no_atp]:
592      "P \<bar>a::'a::linordered_idom\<bar> = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
593 by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
595 lemma negD: "x < 0 \<Longrightarrow> \<exists>n. x = - (int (Suc n))"
596 apply transfer
597 apply clarsimp
598 apply (rule_tac x="b - Suc a" in exI, arith)
599 done
601 subsection \<open>Cases and induction\<close>
603 text\<open>Now we replace the case analysis rule by a more conventional one:
604 whether an integer is negative or not.\<close>
606 text\<open>This version is symmetric in the two subgoals.\<close>
607 theorem int_cases2 [case_names nonneg nonpos, cases type: int]:
608   "\<lbrakk>!! n. z = int n \<Longrightarrow> P;  !! n. z = - (int n) \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
609 apply (cases "z < 0")
610 apply (auto simp add: linorder_not_less dest!: negD nat_0_le [THEN sym])
611 done
613 text\<open>This is the default, with a negative case.\<close>
614 theorem int_cases [case_names nonneg neg, cases type: int]:
615   "[|!! n. z = int n ==> P;  !! n. z = - (int (Suc n)) ==> P |] ==> P"
616 apply (cases "z < 0")
617 apply (blast dest!: negD)
618 apply (simp add: linorder_not_less del: of_nat_Suc)
619 apply auto
620 apply (blast dest: nat_0_le [THEN sym])
621 done
623 lemma int_cases3 [case_names zero pos neg]:
624   fixes k :: int
625   assumes "k = 0 \<Longrightarrow> P" and "\<And>n. k = int n \<Longrightarrow> n > 0 \<Longrightarrow> P"
626     and "\<And>n. k = - int n \<Longrightarrow> n > 0 \<Longrightarrow> P"
627   shows "P"
628 proof (cases k "0::int" rule: linorder_cases)
629   case equal with assms(1) show P by simp
630 next
631   case greater
632   then have "nat k > 0" by simp
633   moreover from this have "k = int (nat k)" by auto
634   ultimately show P using assms(2) by blast
635 next
636   case less
637   then have "nat (- k) > 0" by simp
638   moreover from this have "k = - int (nat (- k))" by auto
639   ultimately show P using assms(3) by blast
640 qed
642 theorem int_of_nat_induct [case_names nonneg neg, induct type: int]:
643      "[|!! n. P (int n);  !!n. P (- (int (Suc n))) |] ==> P z"
644   by (cases z) auto
646 lemma nonneg_int_cases:
647   assumes "0 \<le> k" obtains n where "k = int n"
648   using assms by (rule nonneg_eq_int)
650 lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
651   \<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close>
652   by (fact Let_numeral) \<comment> \<open>FIXME drop\<close>
654 lemma Let_neg_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_neg_numeral) \<comment> \<open>FIXME drop\<close>
658 text \<open>Unfold \<open>min\<close> and \<open>max\<close> on numerals.\<close>
660 lemmas max_number_of [simp] =
661   max_def [of "numeral u" "numeral v"]
662   max_def [of "numeral u" "- numeral v"]
663   max_def [of "- numeral u" "numeral v"]
664   max_def [of "- numeral u" "- numeral v"] for u v
666 lemmas min_number_of [simp] =
667   min_def [of "numeral u" "numeral v"]
668   min_def [of "numeral u" "- numeral v"]
669   min_def [of "- numeral u" "numeral v"]
670   min_def [of "- numeral u" "- numeral v"] for u v
673 subsubsection \<open>Binary comparisons\<close>
675 text \<open>Preliminaries\<close>
677 lemma le_imp_0_less:
678   assumes le: "0 \<le> z"
679   shows "(0::int) < 1 + z"
680 proof -
681   have "0 \<le> z" by fact
682   also have "... < z + 1" by (rule less_add_one)
683   also have "... = 1 + z" by (simp add: ac_simps)
684   finally show "0 < 1 + z" .
685 qed
687 lemma odd_less_0_iff:
688   "(1 + z + z < 0) = (z < (0::int))"
689 proof (cases z)
690   case (nonneg n)
692                              le_imp_0_less [THEN order_less_imp_le])
693 next
694   case (neg n)
695   thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1
696     add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric])
697 qed
699 subsubsection \<open>Comparisons, for Ordered Rings\<close>
701 lemmas double_eq_0_iff = double_zero
703 lemma odd_nonzero:
704   "1 + z + z \<noteq> (0::int)"
705 proof (cases z)
706   case (nonneg n)
707   have le: "0 \<le> z+z" by (simp add: nonneg add_increasing)
708   thus ?thesis using  le_imp_0_less [OF le]
710 next
711   case (neg n)
712   show ?thesis
713   proof
714     assume eq: "1 + z + z = 0"
715     have "(0::int) < 1 + (int n + int n)"
717     also have "... = - (1 + z + z)"
718       by (simp add: neg add.assoc [symmetric])
719     also have "... = 0" by (simp add: eq)
720     finally have "0<0" ..
721     thus False by blast
722   qed
723 qed
726 subsection \<open>The Set of Integers\<close>
728 context ring_1
729 begin
731 definition Ints :: "'a set"  ("\<int>")
732   where "\<int> = range of_int"
734 lemma Ints_of_int [simp]: "of_int z \<in> \<int>"
735   by (simp add: Ints_def)
737 lemma Ints_of_nat [simp]: "of_nat n \<in> \<int>"
738   using Ints_of_int [of "of_nat n"] by simp
740 lemma Ints_0 [simp]: "0 \<in> \<int>"
741   using Ints_of_int [of "0"] by simp
743 lemma Ints_1 [simp]: "1 \<in> \<int>"
744   using Ints_of_int [of "1"] by simp
746 lemma Ints_numeral [simp]: "numeral n \<in> \<int>"
747   by (subst of_nat_numeral [symmetric], rule Ints_of_nat)
749 lemma Ints_add [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a + b \<in> \<int>"
750 apply (auto simp add: Ints_def)
751 apply (rule range_eqI)
752 apply (rule of_int_add [symmetric])
753 done
755 lemma Ints_minus [simp]: "a \<in> \<int> \<Longrightarrow> -a \<in> \<int>"
756 apply (auto simp add: Ints_def)
757 apply (rule range_eqI)
758 apply (rule of_int_minus [symmetric])
759 done
761 lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a - b \<in> \<int>"
762 apply (auto simp add: Ints_def)
763 apply (rule range_eqI)
764 apply (rule of_int_diff [symmetric])
765 done
767 lemma Ints_mult [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a * b \<in> \<int>"
768 apply (auto simp add: Ints_def)
769 apply (rule range_eqI)
770 apply (rule of_int_mult [symmetric])
771 done
773 lemma Ints_power [simp]: "a \<in> \<int> \<Longrightarrow> a ^ n \<in> \<int>"
774 by (induct n) simp_all
776 lemma Ints_cases [cases set: Ints]:
777   assumes "q \<in> \<int>"
778   obtains (of_int) z where "q = of_int z"
779   unfolding Ints_def
780 proof -
781   from \<open>q \<in> \<int>\<close> have "q \<in> range of_int" unfolding Ints_def .
782   then obtain z where "q = of_int z" ..
783   then show thesis ..
784 qed
786 lemma Ints_induct [case_names of_int, induct set: Ints]:
787   "q \<in> \<int> \<Longrightarrow> (\<And>z. P (of_int z)) \<Longrightarrow> P q"
788   by (rule Ints_cases) auto
790 lemma Nats_subset_Ints: "\<nat> \<subseteq> \<int>"
791   unfolding Nats_def Ints_def
792   by (rule subsetI, elim imageE, hypsubst, subst of_int_of_nat_eq[symmetric], rule imageI) simp_all
794 lemma Nats_altdef1: "\<nat> = {of_int n |n. n \<ge> 0}"
795 proof (intro subsetI equalityI)
796   fix x :: 'a assume "x \<in> {of_int n |n. n \<ge> 0}"
797   then obtain n where "x = of_int n" "n \<ge> 0" by (auto elim!: Ints_cases)
798   hence "x = of_nat (nat n)" by (subst of_nat_nat) simp_all
799   thus "x \<in> \<nat>" by simp
800 next
801   fix x :: 'a assume "x \<in> \<nat>"
802   then obtain n where "x = of_nat n" by (auto elim!: Nats_cases)
803   hence "x = of_int (int n)" by simp
804   also have "int n \<ge> 0" by simp
805   hence "of_int (int n) \<in> {of_int n |n. n \<ge> 0}" by blast
806   finally show "x \<in> {of_int n |n. n \<ge> 0}" .
807 qed
809 end
811 lemma (in linordered_idom) Nats_altdef2: "\<nat> = {n \<in> \<int>. n \<ge> 0}"
812 proof (intro subsetI equalityI)
813   fix x :: 'a assume "x \<in> {n \<in> \<int>. n \<ge> 0}"
814   then obtain n where "x = of_int n" "n \<ge> 0" by (auto elim!: Ints_cases)
815   hence "x = of_nat (nat n)" by (subst of_nat_nat) simp_all
816   thus "x \<in> \<nat>" by simp
817 qed (auto elim!: Nats_cases)
820 text \<open>The premise involving @{term Ints} prevents @{term "a = 1/2"}.\<close>
822 lemma Ints_double_eq_0_iff:
823   assumes in_Ints: "a \<in> \<int>"
824   shows "(a + a = 0) = (a = (0::'a::ring_char_0))"
825 proof -
826   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
827   then obtain z where a: "a = of_int z" ..
828   show ?thesis
829   proof
830     assume "a = 0"
831     thus "a + a = 0" by simp
832   next
833     assume eq: "a + a = 0"
834     hence "of_int (z + z) = (of_int 0 :: 'a)" by (simp add: a)
835     hence "z + z = 0" by (simp only: of_int_eq_iff)
836     hence "z = 0" by (simp only: double_eq_0_iff)
837     thus "a = 0" by (simp add: a)
838   qed
839 qed
841 lemma Ints_odd_nonzero:
842   assumes in_Ints: "a \<in> \<int>"
843   shows "1 + a + a \<noteq> (0::'a::ring_char_0)"
844 proof -
845   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
846   then obtain z where a: "a = of_int z" ..
847   show ?thesis
848   proof
849     assume eq: "1 + a + a = 0"
850     hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
851     hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
852     with odd_nonzero show False by blast
853   qed
854 qed
856 lemma Nats_numeral [simp]: "numeral w \<in> \<nat>"
857   using of_nat_in_Nats [of "numeral w"] by simp
859 lemma Ints_odd_less_0:
860   assumes in_Ints: "a \<in> \<int>"
861   shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))"
862 proof -
863   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
864   then obtain z where a: "a = of_int z" ..
865   hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
866     by (simp add: a)
867   also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0_iff)
868   also have "... = (a < 0)" by (simp add: a)
869   finally show ?thesis .
870 qed
873 subsection \<open>@{term setsum} and @{term setprod}\<close>
875 lemma of_nat_setsum [simp]: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
876   apply (cases "finite A")
877   apply (erule finite_induct, auto)
878   done
880 lemma of_int_setsum [simp]: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
881   apply (cases "finite A")
882   apply (erule finite_induct, auto)
883   done
885 lemma of_nat_setprod [simp]: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
886   apply (cases "finite A")
887   apply (erule finite_induct, auto simp add: of_nat_mult)
888   done
890 lemma of_int_setprod [simp]: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
891   apply (cases "finite A")
892   apply (erule finite_induct, auto)
893   done
895 lemmas int_setsum = of_nat_setsum [where 'a=int]
896 lemmas int_setprod = of_nat_setprod [where 'a=int]
899 text \<open>Legacy theorems\<close>
901 lemmas zle_int = of_nat_le_iff [where 'a=int]
902 lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
904 subsection \<open>Setting up simplification procedures\<close>
906 lemmas of_int_simps =
907   of_int_0 of_int_1 of_int_add of_int_mult
909 ML_file "Tools/int_arith.ML"
910 declaration \<open>K Int_Arith.setup\<close>
912 simproc_setup fast_arith ("(m::'a::linordered_idom) < n" |
913   "(m::'a::linordered_idom) \<le> n" |
914   "(m::'a::linordered_idom) = n") =
915   \<open>K Lin_Arith.simproc\<close>
918 subsection\<open>More Inequality Reasoning\<close>
920 lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
921 by arith
923 lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
924 by arith
926 lemma zle_diff1_eq [simp]: "(w \<le> z - (1::int)) = (w<z)"
927 by arith
929 lemma zle_add1_eq_le [simp]: "(w < z + (1::int)) = (w\<le>z)"
930 by arith
932 lemma int_one_le_iff_zero_less: "((1::int) \<le> z) = (0 < z)"
933 by arith
936 subsection\<open>The functions @{term nat} and @{term int}\<close>
938 text\<open>Simplify the term @{term "w + - z"}\<close>
940 lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
941   using zless_nat_conj [of 1 z] by auto
943 text\<open>This simplifies expressions of the form @{term "int n = z"} where
944       z is an integer literal.\<close>
945 lemmas int_eq_iff_numeral [simp] = int_eq_iff [of _ "numeral v"] for v
947 lemma split_nat [arith_split]:
948   "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
949   (is "?P = (?L & ?R)")
950 proof (cases "i < 0")
951   case True thus ?thesis by auto
952 next
953   case False
954   have "?P = ?L"
955   proof
956     assume ?P thus ?L using False by clarsimp
957   next
958     assume ?L thus ?P using False by simp
959   qed
960   with False show ?thesis by simp
961 qed
963 lemma nat_abs_int_diff: "nat \<bar>int a - int b\<bar> = (if a \<le> b then b - a else a - b)"
964   by auto
966 lemma nat_int_add: "nat (int a + int b) = a + b"
967   by auto
969 context ring_1
970 begin
972 lemma of_int_of_nat [nitpick_simp]:
973   "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))"
974 proof (cases "k < 0")
975   case True then have "0 \<le> - k" by simp
976   then have "of_nat (nat (- k)) = of_int (- k)" by (rule of_nat_nat)
977   with True show ?thesis by simp
978 next
979   case False then show ?thesis by (simp add: not_less of_nat_nat)
980 qed
982 end
984 lemma nat_mult_distrib:
985   fixes z z' :: int
986   assumes "0 \<le> z"
987   shows "nat (z * z') = nat z * nat z'"
988 proof (cases "0 \<le> z'")
989   case False with assms have "z * z' \<le> 0"
990     by (simp add: not_le mult_le_0_iff)
991   then have "nat (z * z') = 0" by simp
992   moreover from False have "nat z' = 0" by simp
993   ultimately show ?thesis by simp
994 next
995   case True with assms have ge_0: "z * z' \<ge> 0" by (simp add: zero_le_mult_iff)
996   show ?thesis
997     by (rule injD [of "of_nat :: nat \<Rightarrow> int", OF inj_of_nat])
998       (simp only: of_nat_mult of_nat_nat [OF True]
999          of_nat_nat [OF assms] of_nat_nat [OF ge_0], simp)
1000 qed
1002 lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"
1003 apply (rule trans)
1004 apply (rule_tac  nat_mult_distrib, auto)
1005 done
1007 lemma nat_abs_mult_distrib: "nat \<bar>w * z\<bar> = nat \<bar>w\<bar> * nat \<bar>z\<bar>"
1008 apply (cases "z=0 | w=0")
1009 apply (auto simp add: abs_if nat_mult_distrib [symmetric]
1010                       nat_mult_distrib_neg [symmetric] mult_less_0_iff)
1011 done
1013 lemma int_in_range_abs [simp]:
1014   "int n \<in> range abs"
1015 proof (rule range_eqI)
1016   show "int n = \<bar>int n\<bar>"
1017     by simp
1018 qed
1020 lemma range_abs_Nats [simp]:
1021   "range abs = (\<nat> :: int set)"
1022 proof -
1023   have "\<bar>k\<bar> \<in> \<nat>" for k :: int
1024     by (cases k) simp_all
1025   moreover have "k \<in> range abs" if "k \<in> \<nat>" for k :: int
1026     using that by induct simp
1027   ultimately show ?thesis by blast
1028 qed
1030 lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
1031 apply (rule sym)
1032 apply (simp add: nat_eq_iff)
1033 done
1035 lemma diff_nat_eq_if:
1036      "nat z - nat z' =
1037         (if z' < 0 then nat z
1038          else let d = z-z' in
1039               if d < 0 then 0 else nat d)"
1040 by (simp add: Let_def nat_diff_distrib [symmetric])
1042 lemma nat_numeral_diff_1 [simp]:
1043   "numeral v - (1::nat) = nat (numeral v - 1)"
1044   using diff_nat_numeral [of v Num.One] by simp
1047 subsection "Induction principles for int"
1049 text\<open>Well-founded segments of the integers\<close>
1051 definition
1052   int_ge_less_than  ::  "int => (int * int) set"
1053 where
1054   "int_ge_less_than d = {(z',z). d \<le> z' & z' < z}"
1056 theorem wf_int_ge_less_than: "wf (int_ge_less_than d)"
1057 proof -
1058   have "int_ge_less_than d \<subseteq> measure (%z. nat (z-d))"
1059     by (auto simp add: int_ge_less_than_def)
1060   thus ?thesis
1061     by (rule wf_subset [OF wf_measure])
1062 qed
1064 text\<open>This variant looks odd, but is typical of the relations suggested
1065 by RankFinder.\<close>
1067 definition
1068   int_ge_less_than2 ::  "int => (int * int) set"
1069 where
1070   "int_ge_less_than2 d = {(z',z). d \<le> z & z' < z}"
1072 theorem wf_int_ge_less_than2: "wf (int_ge_less_than2 d)"
1073 proof -
1074   have "int_ge_less_than2 d \<subseteq> measure (%z. nat (1+z-d))"
1075     by (auto simp add: int_ge_less_than2_def)
1076   thus ?thesis
1077     by (rule wf_subset [OF wf_measure])
1078 qed
1080 (* `set:int': dummy construction *)
1081 theorem int_ge_induct [case_names base step, induct set: int]:
1082   fixes i :: int
1083   assumes ge: "k \<le> i" and
1084     base: "P k" and
1085     step: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
1086   shows "P i"
1087 proof -
1088   { fix n
1089     have "\<And>i::int. n = nat (i - k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i"
1090     proof (induct n)
1091       case 0
1092       hence "i = k" by arith
1093       thus "P i" using base by simp
1094     next
1095       case (Suc n)
1096       then have "n = nat((i - 1) - k)" by arith
1097       moreover
1098       have ki1: "k \<le> i - 1" using Suc.prems by arith
1099       ultimately
1100       have "P (i - 1)" by (rule Suc.hyps)
1101       from step [OF ki1 this] show ?case by simp
1102     qed
1103   }
1104   with ge show ?thesis by fast
1105 qed
1107 (* `set:int': dummy construction *)
1108 theorem int_gr_induct [case_names base step, induct set: int]:
1109   assumes gr: "k < (i::int)" and
1110         base: "P(k+1)" and
1111         step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
1112   shows "P i"
1113 apply(rule int_ge_induct[of "k + 1"])
1114   using gr apply arith
1115  apply(rule base)
1116 apply (rule step, simp+)
1117 done
1119 theorem int_le_induct [consumes 1, case_names base step]:
1120   assumes le: "i \<le> (k::int)" and
1121         base: "P(k)" and
1122         step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
1123   shows "P i"
1124 proof -
1125   { fix n
1126     have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i"
1127     proof (induct n)
1128       case 0
1129       hence "i = k" by arith
1130       thus "P i" using base by simp
1131     next
1132       case (Suc n)
1133       hence "n = nat (k - (i + 1))" by arith
1134       moreover
1135       have ki1: "i + 1 \<le> k" using Suc.prems by arith
1136       ultimately
1137       have "P (i + 1)" by(rule Suc.hyps)
1138       from step[OF ki1 this] show ?case by simp
1139     qed
1140   }
1141   with le show ?thesis by fast
1142 qed
1144 theorem int_less_induct [consumes 1, case_names base step]:
1145   assumes less: "(i::int) < k" and
1146         base: "P(k - 1)" and
1147         step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
1148   shows "P i"
1149 apply(rule int_le_induct[of _ "k - 1"])
1150   using less apply arith
1151  apply(rule base)
1152 apply (rule step, simp+)
1153 done
1155 theorem int_induct [case_names base step1 step2]:
1156   fixes k :: int
1157   assumes base: "P k"
1158     and step1: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
1159     and step2: "\<And>i. k \<ge> i \<Longrightarrow> P i \<Longrightarrow> P (i - 1)"
1160   shows "P i"
1161 proof -
1162   have "i \<le> k \<or> i \<ge> k" by arith
1163   then show ?thesis
1164   proof
1165     assume "i \<ge> k"
1166     then show ?thesis using base
1167       by (rule int_ge_induct) (fact step1)
1168   next
1169     assume "i \<le> k"
1170     then show ?thesis using base
1171       by (rule int_le_induct) (fact step2)
1172   qed
1173 qed
1175 subsection\<open>Intermediate value theorems\<close>
1177 lemma int_val_lemma:
1178      "(\<forall>i<n::nat. \<bar>f(i+1) - f i\<bar> \<le> 1) -->
1179       f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
1180 unfolding One_nat_def
1181 apply (induct n)
1182 apply simp
1183 apply (intro strip)
1184 apply (erule impE, simp)
1185 apply (erule_tac x = n in allE, simp)
1186 apply (case_tac "k = f (Suc n)")
1187 apply force
1188 apply (erule impE)
1189  apply (simp add: abs_if split add: split_if_asm)
1190 apply (blast intro: le_SucI)
1191 done
1193 lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
1195 lemma nat_intermed_int_val:
1196      "[| \<forall>i. m \<le> i & i < n --> \<bar>f(i + 1::nat) - f i\<bar> \<le> 1; m < n;
1197          f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
1198 apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k
1199        in int_val_lemma)
1200 unfolding One_nat_def
1201 apply simp
1202 apply (erule exE)
1203 apply (rule_tac x = "i+m" in exI, arith)
1204 done
1207 subsection\<open>Products and 1, by T. M. Rasmussen\<close>
1209 lemma abs_zmult_eq_1:
1210   assumes mn: "\<bar>m * n\<bar> = 1"
1211   shows "\<bar>m\<bar> = (1::int)"
1212 proof -
1213   have 0: "m \<noteq> 0 & n \<noteq> 0" using mn
1214     by auto
1215   have "~ (2 \<le> \<bar>m\<bar>)"
1216   proof
1217     assume "2 \<le> \<bar>m\<bar>"
1218     hence "2*\<bar>n\<bar> \<le> \<bar>m\<bar>*\<bar>n\<bar>"
1219       by (simp add: mult_mono 0)
1220     also have "... = \<bar>m*n\<bar>"
1221       by (simp add: abs_mult)
1222     also have "... = 1"
1223       by (simp add: mn)
1224     finally have "2*\<bar>n\<bar> \<le> 1" .
1225     thus "False" using 0
1226       by arith
1227   qed
1228   thus ?thesis using 0
1229     by auto
1230 qed
1232 lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1"
1233 by (insert abs_zmult_eq_1 [of m n], arith)
1235 lemma pos_zmult_eq_1_iff:
1236   assumes "0 < (m::int)" shows "(m * n = 1) = (m = 1 & n = 1)"
1237 proof -
1238   from assms have "m * n = 1 ==> m = 1" by (auto dest: pos_zmult_eq_1_iff_lemma)
1239   thus ?thesis by (auto dest: pos_zmult_eq_1_iff_lemma)
1240 qed
1242 lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
1243 apply (rule iffI)
1244  apply (frule pos_zmult_eq_1_iff_lemma)
1245  apply (simp add: mult.commute [of m])
1246  apply (frule pos_zmult_eq_1_iff_lemma, auto)
1247 done
1249 lemma infinite_UNIV_int: "\<not> finite (UNIV::int set)"
1250 proof
1251   assume "finite (UNIV::int set)"
1252   moreover have "inj (\<lambda>i::int. 2 * i)"
1253     by (rule injI) simp
1254   ultimately have "surj (\<lambda>i::int. 2 * i)"
1255     by (rule finite_UNIV_inj_surj)
1256   then obtain i :: int where "1 = 2 * i" by (rule surjE)
1257   then show False by (simp add: pos_zmult_eq_1_iff)
1258 qed
1261 subsection \<open>Further theorems on numerals\<close>
1263 subsubsection\<open>Special Simplification for Constants\<close>
1265 text\<open>These distributive laws move literals inside sums and differences.\<close>
1267 lemmas distrib_right_numeral [simp] = distrib_right [of _ _ "numeral v"] for v
1268 lemmas distrib_left_numeral [simp] = distrib_left [of "numeral v"] for v
1269 lemmas left_diff_distrib_numeral [simp] = left_diff_distrib [of _ _ "numeral v"] for v
1270 lemmas right_diff_distrib_numeral [simp] = right_diff_distrib [of "numeral v"] for v
1272 text\<open>These are actually for fields, like real: but where else to put them?\<close>
1274 lemmas zero_less_divide_iff_numeral [simp, no_atp] = zero_less_divide_iff [of "numeral w"] for w
1275 lemmas divide_less_0_iff_numeral [simp, no_atp] = divide_less_0_iff [of "numeral w"] for w
1276 lemmas zero_le_divide_iff_numeral [simp, no_atp] = zero_le_divide_iff [of "numeral w"] for w
1277 lemmas divide_le_0_iff_numeral [simp, no_atp] = divide_le_0_iff [of "numeral w"] for w
1280 text \<open>Replaces \<open>inverse #nn\<close> by \<open>1/#nn\<close>.  It looks
1281   strange, but then other simprocs simplify the quotient.\<close>
1283 lemmas inverse_eq_divide_numeral [simp] =
1284   inverse_eq_divide [of "numeral w"] for w
1286 lemmas inverse_eq_divide_neg_numeral [simp] =
1287   inverse_eq_divide [of "- numeral w"] for w
1289 text \<open>These laws simplify inequalities, moving unary minus from a term
1290 into the literal.\<close>
1292 lemmas equation_minus_iff_numeral [no_atp] =
1293   equation_minus_iff [of "numeral v"] for v
1295 lemmas minus_equation_iff_numeral [no_atp] =
1296   minus_equation_iff [of _ "numeral v"] for v
1298 lemmas le_minus_iff_numeral [no_atp] =
1299   le_minus_iff [of "numeral v"] for v
1301 lemmas minus_le_iff_numeral [no_atp] =
1302   minus_le_iff [of _ "numeral v"] for v
1304 lemmas less_minus_iff_numeral [no_atp] =
1305   less_minus_iff [of "numeral v"] for v
1307 lemmas minus_less_iff_numeral [no_atp] =
1308   minus_less_iff [of _ "numeral v"] for v
1310 \<comment> \<open>FIXME maybe simproc\<close>
1313 text \<open>Cancellation of constant factors in comparisons (\<open><\<close> and \<open>\<le>\<close>)\<close>
1315 lemmas mult_less_cancel_left_numeral [simp, no_atp] = mult_less_cancel_left [of "numeral v"] for v
1316 lemmas mult_less_cancel_right_numeral [simp, no_atp] = mult_less_cancel_right [of _ "numeral v"] for v
1317 lemmas mult_le_cancel_left_numeral [simp, no_atp] = mult_le_cancel_left [of "numeral v"] for v
1318 lemmas mult_le_cancel_right_numeral [simp, no_atp] = mult_le_cancel_right [of _ "numeral v"] for v
1321 text \<open>Multiplying out constant divisors in comparisons (\<open><\<close>, \<open>\<le>\<close> and \<open>=\<close>)\<close>
1323 named_theorems divide_const_simps "simplification rules to simplify comparisons involving constant divisors"
1325 lemmas le_divide_eq_numeral1 [simp,divide_const_simps] =
1326   pos_le_divide_eq [of "numeral w", OF zero_less_numeral]
1327   neg_le_divide_eq [of "- numeral w", OF neg_numeral_less_zero] for w
1329 lemmas divide_le_eq_numeral1 [simp,divide_const_simps] =
1330   pos_divide_le_eq [of "numeral w", OF zero_less_numeral]
1331   neg_divide_le_eq [of "- numeral w", OF neg_numeral_less_zero] for w
1333 lemmas less_divide_eq_numeral1 [simp,divide_const_simps] =
1334   pos_less_divide_eq [of "numeral w", OF zero_less_numeral]
1335   neg_less_divide_eq [of "- numeral w", OF neg_numeral_less_zero] for w
1337 lemmas divide_less_eq_numeral1 [simp,divide_const_simps] =
1338   pos_divide_less_eq [of "numeral w", OF zero_less_numeral]
1339   neg_divide_less_eq [of "- numeral w", OF neg_numeral_less_zero] for w
1341 lemmas eq_divide_eq_numeral1 [simp,divide_const_simps] =
1342   eq_divide_eq [of _ _ "numeral w"]
1343   eq_divide_eq [of _ _ "- numeral w"] for w
1345 lemmas divide_eq_eq_numeral1 [simp,divide_const_simps] =
1346   divide_eq_eq [of _ "numeral w"]
1347   divide_eq_eq [of _ "- numeral w"] for w
1350 subsubsection\<open>Optional Simplification Rules Involving Constants\<close>
1352 text\<open>Simplify quotients that are compared with a literal constant.\<close>
1354 lemmas le_divide_eq_numeral [divide_const_simps] =
1355   le_divide_eq [of "numeral w"]
1356   le_divide_eq [of "- numeral w"] for w
1358 lemmas divide_le_eq_numeral [divide_const_simps] =
1359   divide_le_eq [of _ _ "numeral w"]
1360   divide_le_eq [of _ _ "- numeral w"] for w
1362 lemmas less_divide_eq_numeral [divide_const_simps] =
1363   less_divide_eq [of "numeral w"]
1364   less_divide_eq [of "- numeral w"] for w
1366 lemmas divide_less_eq_numeral [divide_const_simps] =
1367   divide_less_eq [of _ _ "numeral w"]
1368   divide_less_eq [of _ _ "- numeral w"] for w
1370 lemmas eq_divide_eq_numeral [divide_const_simps] =
1371   eq_divide_eq [of "numeral w"]
1372   eq_divide_eq [of "- numeral w"] for w
1374 lemmas divide_eq_eq_numeral [divide_const_simps] =
1375   divide_eq_eq [of _ _ "numeral w"]
1376   divide_eq_eq [of _ _ "- numeral w"] for w
1379 text\<open>Not good as automatic simprules because they cause case splits.\<close>
1380 lemmas [divide_const_simps] = le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
1383 subsection \<open>The divides relation\<close>
1385 lemma zdvd_antisym_nonneg:
1386     "0 <= m ==> 0 <= n ==> m dvd n ==> n dvd m ==> m = (n::int)"
1387   apply (simp add: dvd_def, auto)
1388   apply (auto simp add: mult.assoc zero_le_mult_iff zmult_eq_1_iff)
1389   done
1391 lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a"
1392   shows "\<bar>a\<bar> = \<bar>b\<bar>"
1393 proof cases
1394   assume "a = 0" with assms show ?thesis by simp
1395 next
1396   assume "a \<noteq> 0"
1397   from \<open>a dvd b\<close> obtain k where k:"b = a*k" unfolding dvd_def by blast
1398   from \<open>b dvd a\<close> obtain k' where k':"a = b*k'" unfolding dvd_def by blast
1399   from k k' have "a = a*k*k'" by simp
1400   with mult_cancel_left1[where c="a" and b="k*k'"]
1401   have kk':"k*k' = 1" using \<open>a\<noteq>0\<close> by (simp add: mult.assoc)
1402   hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff)
1403   thus ?thesis using k k' by auto
1404 qed
1406 lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
1407   using dvd_add_right_iff [of k "- n" m] by simp
1409 lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
1410   using dvd_add_times_triv_right_iff [of k n m] by (simp add: ac_simps)
1412 lemma dvd_imp_le_int:
1413   fixes d i :: int
1414   assumes "i \<noteq> 0" and "d dvd i"
1415   shows "\<bar>d\<bar> \<le> \<bar>i\<bar>"
1416 proof -
1417   from \<open>d dvd i\<close> obtain k where "i = d * k" ..
1418   with \<open>i \<noteq> 0\<close> have "k \<noteq> 0" by auto
1419   then have "1 \<le> \<bar>k\<bar>" and "0 \<le> \<bar>d\<bar>" by auto
1420   then have "\<bar>d\<bar> * 1 \<le> \<bar>d\<bar> * \<bar>k\<bar>" by (rule mult_left_mono)
1421   with \<open>i = d * k\<close> show ?thesis by (simp add: abs_mult)
1422 qed
1424 lemma zdvd_not_zless:
1425   fixes m n :: int
1426   assumes "0 < m" and "m < n"
1427   shows "\<not> n dvd m"
1428 proof
1429   from assms have "0 < n" by auto
1430   assume "n dvd m" then obtain k where k: "m = n * k" ..
1431   with \<open>0 < m\<close> have "0 < n * k" by auto
1432   with \<open>0 < n\<close> have "0 < k" by (simp add: zero_less_mult_iff)
1433   with k \<open>0 < n\<close> \<open>m < n\<close> have "n * k < n * 1" by simp
1434   with \<open>0 < n\<close> \<open>0 < k\<close> show False unfolding mult_less_cancel_left by auto
1435 qed
1437 lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)"
1438   shows "m dvd n"
1439 proof-
1440   from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast
1441   {assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp
1442     with h have False by (simp add: mult.assoc)}
1443   hence "n = m * h" by blast
1444   thus ?thesis by simp
1445 qed
1447 theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
1448 proof -
1449   have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"
1450   proof -
1451     fix k
1452     assume A: "int y = int x * k"
1453     then show "x dvd y"
1454     proof (cases k)
1455       case (nonneg n)
1456       with A have "y = x * n" by (simp del: of_nat_mult add: of_nat_mult [symmetric])
1457       then show ?thesis ..
1458     next
1459       case (neg n)
1460       with A have "int y = int x * (- int (Suc n))" by simp
1461       also have "\<dots> = - (int x * int (Suc n))" by (simp only: mult_minus_right)
1462       also have "\<dots> = - int (x * Suc n)" by (simp only: of_nat_mult [symmetric])
1463       finally have "- int (x * Suc n) = int y" ..
1464       then show ?thesis by (simp only: negative_eq_positive) auto
1465     qed
1466   qed
1467   then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left of_nat_mult)
1468 qed
1470 lemma zdvd1_eq[simp]: "(x::int) dvd 1 = (\<bar>x\<bar> = 1)"
1471 proof
1472   assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp
1473   hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
1474   hence "nat \<bar>x\<bar> = 1"  by simp
1475   thus "\<bar>x\<bar> = 1" by (cases "x < 0") auto
1476 next
1477   assume "\<bar>x\<bar>=1"
1478   then have "x = 1 \<or> x = -1" by auto
1479   then show "x dvd 1" by (auto intro: dvdI)
1480 qed
1482 lemma zdvd_mult_cancel1:
1483   assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
1484 proof
1485   assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m"
1486     by (cases "n >0") (auto simp add: minus_equation_iff)
1487 next
1488   assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
1489   from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
1490 qed
1492 lemma int_dvd_iff: "(int m dvd z) = (m dvd nat \<bar>z\<bar>)"
1493   unfolding zdvd_int by (cases "z \<ge> 0") simp_all
1495 lemma dvd_int_iff: "(z dvd int m) = (nat \<bar>z\<bar> dvd m)"
1496   unfolding zdvd_int by (cases "z \<ge> 0") simp_all
1498 lemma dvd_int_unfold_dvd_nat:
1499   "k dvd l \<longleftrightarrow> nat \<bar>k\<bar> dvd nat \<bar>l\<bar>"
1500   unfolding dvd_int_iff [symmetric] by simp
1502 lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
1503   by (auto simp add: dvd_int_iff)
1505 lemma eq_nat_nat_iff:
1506   "0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat z = nat z' \<longleftrightarrow> z = z'"
1507   by (auto elim!: nonneg_eq_int)
1509 lemma nat_power_eq:
1510   "0 \<le> z \<Longrightarrow> nat (z ^ n) = nat z ^ n"
1511   by (induct n) (simp_all add: nat_mult_distrib)
1513 lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
1514   apply (cases n)
1515   apply (auto simp add: dvd_int_iff)
1516   apply (cases z)
1517   apply (auto simp add: dvd_imp_le)
1518   done
1520 lemma zdvd_period:
1521   fixes a d :: int
1522   assumes "a dvd d"
1523   shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)"
1524 proof -
1525   from assms obtain k where "d = a * k" by (rule dvdE)
1526   show ?thesis
1527   proof
1528     assume "a dvd (x + t)"
1529     then obtain l where "x + t = a * l" by (rule dvdE)
1530     then have "x = a * l - t" by simp
1531     with \<open>d = a * k\<close> show "a dvd x + c * d + t" by simp
1532   next
1533     assume "a dvd x + c * d + t"
1534     then obtain l where "x + c * d + t = a * l" by (rule dvdE)
1535     then have "x = a * l - c * d - t" by simp
1536     with \<open>d = a * k\<close> show "a dvd (x + t)" by simp
1537   qed
1538 qed
1541 subsection \<open>Finiteness of intervals\<close>
1543 lemma finite_interval_int1 [iff]: "finite {i :: int. a <= i & i <= b}"
1544 proof (cases "a <= b")
1545   case True
1546   from this show ?thesis
1547   proof (induct b rule: int_ge_induct)
1548     case base
1549     have "{i. a <= i & i <= a} = {a}" by auto
1550     from this show ?case by simp
1551   next
1552     case (step b)
1553     from this have "{i. a <= i & i <= b + 1} = {i. a <= i & i <= b} \<union> {b + 1}" by auto
1554     from this step show ?case by simp
1555   qed
1556 next
1557   case False from this show ?thesis
1558     by (metis (lifting, no_types) Collect_empty_eq finite.emptyI order_trans)
1559 qed
1561 lemma finite_interval_int2 [iff]: "finite {i :: int. a <= i & i < b}"
1562 by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
1564 lemma finite_interval_int3 [iff]: "finite {i :: int. a < i & i <= b}"
1565 by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
1567 lemma finite_interval_int4 [iff]: "finite {i :: int. a < i & i < b}"
1568 by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
1571 subsection \<open>Configuration of the code generator\<close>
1573 text \<open>Constructors\<close>
1575 definition Pos :: "num \<Rightarrow> int" where
1576   [simp, code_abbrev]: "Pos = numeral"
1578 definition Neg :: "num \<Rightarrow> int" where
1579   [simp, code_abbrev]: "Neg n = - (Pos n)"
1581 code_datatype "0::int" Pos Neg
1584 text \<open>Auxiliary operations\<close>
1586 definition dup :: "int \<Rightarrow> int" where
1587   [simp]: "dup k = k + k"
1589 lemma dup_code [code]:
1590   "dup 0 = 0"
1591   "dup (Pos n) = Pos (Num.Bit0 n)"
1592   "dup (Neg n) = Neg (Num.Bit0 n)"
1593   unfolding Pos_def Neg_def
1594   by (simp_all add: numeral_Bit0)
1596 definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
1597   [simp]: "sub m n = numeral m - numeral n"
1599 lemma sub_code [code]:
1600   "sub Num.One Num.One = 0"
1601   "sub (Num.Bit0 m) Num.One = Pos (Num.BitM m)"
1602   "sub (Num.Bit1 m) Num.One = Pos (Num.Bit0 m)"
1603   "sub Num.One (Num.Bit0 n) = Neg (Num.BitM n)"
1604   "sub Num.One (Num.Bit1 n) = Neg (Num.Bit0 n)"
1605   "sub (Num.Bit0 m) (Num.Bit0 n) = dup (sub m n)"
1606   "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)"
1607   "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1"
1608   "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1"
1609   apply (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def numeral_BitM)
1610   apply (simp_all only: algebra_simps minus_diff_eq)
1611   apply (simp_all only: add.commute [of _ "- (numeral n + numeral n)"])
1612   apply (simp_all only: minus_add add.assoc left_minus)
1613   done
1615 text \<open>Implementations\<close>
1617 lemma one_int_code [code, code_unfold]:
1618   "1 = Pos Num.One"
1619   by simp
1621 lemma plus_int_code [code]:
1622   "k + 0 = (k::int)"
1623   "0 + l = (l::int)"
1624   "Pos m + Pos n = Pos (m + n)"
1625   "Pos m + Neg n = sub m n"
1626   "Neg m + Pos n = sub n m"
1627   "Neg m + Neg n = Neg (m + n)"
1628   by simp_all
1630 lemma uminus_int_code [code]:
1631   "uminus 0 = (0::int)"
1632   "uminus (Pos m) = Neg m"
1633   "uminus (Neg m) = Pos m"
1634   by simp_all
1636 lemma minus_int_code [code]:
1637   "k - 0 = (k::int)"
1638   "0 - l = uminus (l::int)"
1639   "Pos m - Pos n = sub m n"
1640   "Pos m - Neg n = Pos (m + n)"
1641   "Neg m - Pos n = Neg (m + n)"
1642   "Neg m - Neg n = sub n m"
1643   by simp_all
1645 lemma times_int_code [code]:
1646   "k * 0 = (0::int)"
1647   "0 * l = (0::int)"
1648   "Pos m * Pos n = Pos (m * n)"
1649   "Pos m * Neg n = Neg (m * n)"
1650   "Neg m * Pos n = Neg (m * n)"
1651   "Neg m * Neg n = Pos (m * n)"
1652   by simp_all
1654 instantiation int :: equal
1655 begin
1657 definition
1658   "HOL.equal k l \<longleftrightarrow> k = (l::int)"
1660 instance
1661   by standard (rule equal_int_def)
1663 end
1665 lemma equal_int_code [code]:
1666   "HOL.equal 0 (0::int) \<longleftrightarrow> True"
1667   "HOL.equal 0 (Pos l) \<longleftrightarrow> False"
1668   "HOL.equal 0 (Neg l) \<longleftrightarrow> False"
1669   "HOL.equal (Pos k) 0 \<longleftrightarrow> False"
1670   "HOL.equal (Pos k) (Pos l) \<longleftrightarrow> HOL.equal k l"
1671   "HOL.equal (Pos k) (Neg l) \<longleftrightarrow> False"
1672   "HOL.equal (Neg k) 0 \<longleftrightarrow> False"
1673   "HOL.equal (Neg k) (Pos l) \<longleftrightarrow> False"
1674   "HOL.equal (Neg k) (Neg l) \<longleftrightarrow> HOL.equal k l"
1675   by (auto simp add: equal)
1677 lemma equal_int_refl [code nbe]:
1678   "HOL.equal (k::int) k \<longleftrightarrow> True"
1679   by (fact equal_refl)
1681 lemma less_eq_int_code [code]:
1682   "0 \<le> (0::int) \<longleftrightarrow> True"
1683   "0 \<le> Pos l \<longleftrightarrow> True"
1684   "0 \<le> Neg l \<longleftrightarrow> False"
1685   "Pos k \<le> 0 \<longleftrightarrow> False"
1686   "Pos k \<le> Pos l \<longleftrightarrow> k \<le> l"
1687   "Pos k \<le> Neg l \<longleftrightarrow> False"
1688   "Neg k \<le> 0 \<longleftrightarrow> True"
1689   "Neg k \<le> Pos l \<longleftrightarrow> True"
1690   "Neg k \<le> Neg l \<longleftrightarrow> l \<le> k"
1691   by simp_all
1693 lemma less_int_code [code]:
1694   "0 < (0::int) \<longleftrightarrow> False"
1695   "0 < Pos l \<longleftrightarrow> True"
1696   "0 < Neg l \<longleftrightarrow> False"
1697   "Pos k < 0 \<longleftrightarrow> False"
1698   "Pos k < Pos l \<longleftrightarrow> k < l"
1699   "Pos k < Neg l \<longleftrightarrow> False"
1700   "Neg k < 0 \<longleftrightarrow> True"
1701   "Neg k < Pos l \<longleftrightarrow> True"
1702   "Neg k < Neg l \<longleftrightarrow> l < k"
1703   by simp_all
1705 lemma nat_code [code]:
1706   "nat (Int.Neg k) = 0"
1707   "nat 0 = 0"
1708   "nat (Int.Pos k) = nat_of_num k"
1709   by (simp_all add: nat_of_num_numeral)
1711 lemma (in ring_1) of_int_code [code]:
1712   "of_int (Int.Neg k) = - numeral k"
1713   "of_int 0 = 0"
1714   "of_int (Int.Pos k) = numeral k"
1715   by simp_all
1718 text \<open>Serializer setup\<close>
1720 code_identifier
1721   code_module Int \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
1723 quickcheck_params [default_type = int]
1725 hide_const (open) Pos Neg sub dup
1728 subsection \<open>Legacy theorems\<close>
1730 lemmas inj_int = inj_of_nat [where 'a=int]
1731 lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
1732 lemmas int_mult = of_nat_mult [where 'a=int]
1733 lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="n"] for n
1734 lemmas zless_int = of_nat_less_iff [where 'a=int]
1735 lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="k"] for k
1736 lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int]
1737 lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
1738 lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="n"] for n
1739 lemmas int_0 = of_nat_0 [where 'a=int]
1740 lemmas int_1 = of_nat_1 [where 'a=int]
1741 lemmas int_Suc = of_nat_Suc [where 'a=int]
1742 lemmas int_numeral = of_nat_numeral [where 'a=int]
1743 lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m"] for m
1744 lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
1745 lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
1746 lemmas zpower_numeral_even = power_numeral_even [where 'a=int]
1747 lemmas zpower_numeral_odd = power_numeral_odd [where 'a=int]
1749 text \<open>De-register \<open>int\<close> as a quotient type:\<close>
1751 lifting_update int.lifting
1752 lifting_forget int.lifting
1754 text\<open>Also the class for fields with characteristic zero.\<close>
1755 class field_char_0 = field + ring_char_0
1756 subclass (in linordered_field) field_char_0 ..
1758 end