src/HOL/Euclidean_Division.thy
 author wenzelm Sat Nov 04 15:24:40 2017 +0100 (19 months ago) changeset 67003 49850a679c2c parent 66886 960509bfd47e child 67051 e7e54a0b9197 permissions -rw-r--r--
more robust sorted_entries;
1 (*  Title:      HOL/Euclidean_Division.thy
2     Author:     Manuel Eberl, TU Muenchen
3     Author:     Florian Haftmann, TU Muenchen
4 *)
6 section \<open>Division in euclidean (semi)rings\<close>
8 theory Euclidean_Division
9   imports Int Lattices_Big
10 begin
12 subsection \<open>Euclidean (semi)rings with explicit division and remainder\<close>
14 class euclidean_semiring = semidom_modulo +
15   fixes euclidean_size :: "'a \<Rightarrow> nat"
16   assumes size_0 [simp]: "euclidean_size 0 = 0"
17   assumes mod_size_less:
18     "b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b"
19   assumes size_mult_mono:
20     "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
21 begin
23 lemma euclidean_size_eq_0_iff [simp]:
24   "euclidean_size b = 0 \<longleftrightarrow> b = 0"
25 proof
26   assume "b = 0"
27   then show "euclidean_size b = 0"
28     by simp
29 next
30   assume "euclidean_size b = 0"
31   show "b = 0"
32   proof (rule ccontr)
33     assume "b \<noteq> 0"
34     with mod_size_less have "euclidean_size (b mod b) < euclidean_size b" .
35     with \<open>euclidean_size b = 0\<close> show False
36       by simp
37   qed
38 qed
40 lemma euclidean_size_greater_0_iff [simp]:
41   "euclidean_size b > 0 \<longleftrightarrow> b \<noteq> 0"
42   using euclidean_size_eq_0_iff [symmetric, of b] by safe simp
44 lemma size_mult_mono': "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (b * a)"
45   by (subst mult.commute) (rule size_mult_mono)
47 lemma dvd_euclidean_size_eq_imp_dvd:
48   assumes "a \<noteq> 0" and "euclidean_size a = euclidean_size b"
49     and "b dvd a"
50   shows "a dvd b"
51 proof (rule ccontr)
52   assume "\<not> a dvd b"
53   hence "b mod a \<noteq> 0" using mod_0_imp_dvd [of b a] by blast
54   then have "b mod a \<noteq> 0" by (simp add: mod_eq_0_iff_dvd)
55   from \<open>b dvd a\<close> have "b dvd b mod a" by (simp add: dvd_mod_iff)
56   then obtain c where "b mod a = b * c" unfolding dvd_def by blast
57     with \<open>b mod a \<noteq> 0\<close> have "c \<noteq> 0" by auto
58   with \<open>b mod a = b * c\<close> have "euclidean_size (b mod a) \<ge> euclidean_size b"
59     using size_mult_mono by force
60   moreover from \<open>\<not> a dvd b\<close> and \<open>a \<noteq> 0\<close>
61   have "euclidean_size (b mod a) < euclidean_size a"
62     using mod_size_less by blast
63   ultimately show False using \<open>euclidean_size a = euclidean_size b\<close>
64     by simp
65 qed
67 lemma euclidean_size_times_unit:
68   assumes "is_unit a"
69   shows   "euclidean_size (a * b) = euclidean_size b"
70 proof (rule antisym)
71   from assms have [simp]: "a \<noteq> 0" by auto
72   thus "euclidean_size (a * b) \<ge> euclidean_size b" by (rule size_mult_mono')
73   from assms have "is_unit (1 div a)" by simp
74   hence "1 div a \<noteq> 0" by (intro notI) simp_all
75   hence "euclidean_size (a * b) \<le> euclidean_size ((1 div a) * (a * b))"
76     by (rule size_mult_mono')
77   also from assms have "(1 div a) * (a * b) = b"
78     by (simp add: algebra_simps unit_div_mult_swap)
79   finally show "euclidean_size (a * b) \<le> euclidean_size b" .
80 qed
82 lemma euclidean_size_unit:
83   "is_unit a \<Longrightarrow> euclidean_size a = euclidean_size 1"
84   using euclidean_size_times_unit [of a 1] by simp
86 lemma unit_iff_euclidean_size:
87   "is_unit a \<longleftrightarrow> euclidean_size a = euclidean_size 1 \<and> a \<noteq> 0"
88 proof safe
89   assume A: "a \<noteq> 0" and B: "euclidean_size a = euclidean_size 1"
90   show "is_unit a"
91     by (rule dvd_euclidean_size_eq_imp_dvd [OF A B]) simp_all
92 qed (auto intro: euclidean_size_unit)
94 lemma euclidean_size_times_nonunit:
95   assumes "a \<noteq> 0" "b \<noteq> 0" "\<not> is_unit a"
96   shows   "euclidean_size b < euclidean_size (a * b)"
97 proof (rule ccontr)
98   assume "\<not>euclidean_size b < euclidean_size (a * b)"
99   with size_mult_mono'[OF assms(1), of b]
100     have eq: "euclidean_size (a * b) = euclidean_size b" by simp
101   have "a * b dvd b"
102     by (rule dvd_euclidean_size_eq_imp_dvd [OF _ eq]) (insert assms, simp_all)
103   hence "a * b dvd 1 * b" by simp
104   with \<open>b \<noteq> 0\<close> have "is_unit a" by (subst (asm) dvd_times_right_cancel_iff)
105   with assms(3) show False by contradiction
106 qed
108 lemma dvd_imp_size_le:
109   assumes "a dvd b" "b \<noteq> 0"
110   shows   "euclidean_size a \<le> euclidean_size b"
111   using assms by (auto elim!: dvdE simp: size_mult_mono)
113 lemma dvd_proper_imp_size_less:
114   assumes "a dvd b" "\<not> b dvd a" "b \<noteq> 0"
115   shows   "euclidean_size a < euclidean_size b"
116 proof -
117   from assms(1) obtain c where "b = a * c" by (erule dvdE)
118   hence z: "b = c * a" by (simp add: mult.commute)
119   from z assms have "\<not>is_unit c" by (auto simp: mult.commute mult_unit_dvd_iff)
120   with z assms show ?thesis
121     by (auto intro!: euclidean_size_times_nonunit)
122 qed
124 lemma unit_imp_mod_eq_0:
125   "a mod b = 0" if "is_unit b"
126   using that by (simp add: mod_eq_0_iff_dvd unit_imp_dvd)
128 end
130 class euclidean_ring = idom_modulo + euclidean_semiring
131 begin
133 lemma dvd_diff_commute:
134   "a dvd c - b \<longleftrightarrow> a dvd b - c"
135 proof -
136   have "a dvd c - b \<longleftrightarrow> a dvd (c - b) * - 1"
137     by (subst dvd_mult_unit_iff) simp_all
138   then show ?thesis
139     by simp
140 qed
142 end
145 subsection \<open>Euclidean (semi)rings with cancel rules\<close>
147 class euclidean_semiring_cancel = euclidean_semiring +
148   assumes div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
149   and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
150 begin
152 lemma div_mult_self2 [simp]:
153   assumes "b \<noteq> 0"
154   shows "(a + b * c) div b = c + a div b"
155   using assms div_mult_self1 [of b a c] by (simp add: mult.commute)
157 lemma div_mult_self3 [simp]:
158   assumes "b \<noteq> 0"
159   shows "(c * b + a) div b = c + a div b"
162 lemma div_mult_self4 [simp]:
163   assumes "b \<noteq> 0"
164   shows "(b * c + a) div b = c + a div b"
167 lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b"
168 proof (cases "b = 0")
169   case True then show ?thesis by simp
170 next
171   case False
172   have "a + c * b = (a + c * b) div b * b + (a + c * b) mod b"
174   also from False div_mult_self1 [of b a c] have
175     "\<dots> = (c + a div b) * b + (a + c * b) mod b"
177   finally have "a = a div b * b + (a + c * b) mod b"
179   then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
181   then show ?thesis by simp
182 qed
184 lemma mod_mult_self2 [simp]:
185   "(a + b * c) mod b = a mod b"
186   by (simp add: mult.commute [of b])
188 lemma mod_mult_self3 [simp]:
189   "(c * b + a) mod b = a mod b"
192 lemma mod_mult_self4 [simp]:
193   "(b * c + a) mod b = a mod b"
196 lemma mod_mult_self1_is_0 [simp]:
197   "b * a mod b = 0"
198   using mod_mult_self2 [of 0 b a] by simp
200 lemma mod_mult_self2_is_0 [simp]:
201   "a * b mod b = 0"
202   using mod_mult_self1 [of 0 a b] by simp
205   assumes "b \<noteq> 0"
206   shows "(b + a) div b = a div b + 1"
207   using assms div_mult_self1 [of b a 1] by (simp add: add.commute)
210   assumes "b \<noteq> 0"
211   shows "(a + b) div b = a div b + 1"
215   "(b + a) mod b = a mod b"
219   "(a + b) mod b = a mod b"
220   using mod_mult_self1 [of a 1 b] by simp
222 lemma mod_div_trivial [simp]:
223   "a mod b div b = 0"
224 proof (cases "b = 0")
225   assume "b = 0"
226   thus ?thesis by simp
227 next
228   assume "b \<noteq> 0"
229   hence "a div b + a mod b div b = (a mod b + a div b * b) div b"
230     by (rule div_mult_self1 [symmetric])
231   also have "\<dots> = a div b"
232     by (simp only: mod_div_mult_eq)
233   also have "\<dots> = a div b + 0"
234     by simp
235   finally show ?thesis
237 qed
239 lemma mod_mod_trivial [simp]:
240   "a mod b mod b = a mod b"
241 proof -
242   have "a mod b mod b = (a mod b + a div b * b) mod b"
243     by (simp only: mod_mult_self1)
244   also have "\<dots> = a mod b"
245     by (simp only: mod_div_mult_eq)
246   finally show ?thesis .
247 qed
249 lemma mod_mod_cancel:
250   assumes "c dvd b"
251   shows "a mod b mod c = a mod c"
252 proof -
253   from \<open>c dvd b\<close> obtain k where "b = c * k"
254     by (rule dvdE)
255   have "a mod b mod c = a mod (c * k) mod c"
256     by (simp only: \<open>b = c * k\<close>)
257   also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"
258     by (simp only: mod_mult_self1)
259   also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
260     by (simp only: ac_simps)
261   also have "\<dots> = a mod c"
262     by (simp only: div_mult_mod_eq)
263   finally show ?thesis .
264 qed
266 lemma div_mult_mult2 [simp]:
267   "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
268   by (drule div_mult_mult1) (simp add: mult.commute)
270 lemma div_mult_mult1_if [simp]:
271   "(c * a) div (c * b) = (if c = 0 then 0 else a div b)"
272   by simp_all
274 lemma mod_mult_mult1:
275   "(c * a) mod (c * b) = c * (a mod b)"
276 proof (cases "c = 0")
277   case True then show ?thesis by simp
278 next
279   case False
280   from div_mult_mod_eq
281   have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .
282   with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)
283     = c * a + c * (a mod b)" by (simp add: algebra_simps)
284   with div_mult_mod_eq show ?thesis by simp
285 qed
287 lemma mod_mult_mult2:
288   "(a * c) mod (b * c) = (a mod b) * c"
289   using mod_mult_mult1 [of c a b] by (simp add: mult.commute)
291 lemma mult_mod_left: "(a mod b) * c = (a * c) mod (b * c)"
292   by (fact mod_mult_mult2 [symmetric])
294 lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)"
295   by (fact mod_mult_mult1 [symmetric])
297 lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
298   unfolding dvd_def by (auto simp add: mod_mult_mult1)
300 lemma div_plus_div_distrib_dvd_left:
301   "c dvd a \<Longrightarrow> (a + b) div c = a div c + b div c"
302   by (cases "c = 0") (auto elim: dvdE)
304 lemma div_plus_div_distrib_dvd_right:
305   "c dvd b \<Longrightarrow> (a + b) div c = a div c + b div c"
306   using div_plus_div_distrib_dvd_left [of c b a]
309 named_theorems mod_simps
311 text \<open>Addition respects modular equivalence.\<close>
314   "(a mod c + b) mod c = (a + b) mod c"
315 proof -
316   have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
317     by (simp only: div_mult_mod_eq)
318   also have "\<dots> = (a mod c + b + a div c * c) mod c"
319     by (simp only: ac_simps)
320   also have "\<dots> = (a mod c + b) mod c"
321     by (rule mod_mult_self1)
322   finally show ?thesis
323     by (rule sym)
324 qed
327   "(a + b mod c) mod c = (a + b) mod c"
331   "(a mod c + b mod c) mod c = (a + b) mod c"
334 lemma mod_sum_eq [mod_simps]:
335   "(\<Sum>i\<in>A. f i mod a) mod a = sum f A mod a"
336 proof (induct A rule: infinite_finite_induct)
337   case (insert i A)
338   then have "(\<Sum>i\<in>insert i A. f i mod a) mod a
339     = (f i mod a + (\<Sum>i\<in>A. f i mod a)) mod a"
340     by simp
341   also have "\<dots> = (f i + (\<Sum>i\<in>A. f i mod a) mod a) mod a"
343   also have "\<dots> = (f i + (\<Sum>i\<in>A. f i) mod a) mod a"
345   finally show ?case
346     by (simp add: insert.hyps mod_simps)
347 qed simp_all
350   assumes "a mod c = a' mod c"
351   assumes "b mod c = b' mod c"
352   shows "(a + b) mod c = (a' + b') mod c"
353 proof -
354   have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c"
355     unfolding assms ..
356   then show ?thesis
358 qed
360 text \<open>Multiplication respects modular equivalence.\<close>
362 lemma mod_mult_left_eq [mod_simps]:
363   "((a mod c) * b) mod c = (a * b) mod c"
364 proof -
365   have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
366     by (simp only: div_mult_mod_eq)
367   also have "\<dots> = (a mod c * b + a div c * b * c) mod c"
368     by (simp only: algebra_simps)
369   also have "\<dots> = (a mod c * b) mod c"
370     by (rule mod_mult_self1)
371   finally show ?thesis
372     by (rule sym)
373 qed
375 lemma mod_mult_right_eq [mod_simps]:
376   "(a * (b mod c)) mod c = (a * b) mod c"
377   using mod_mult_left_eq [of b c a] by (simp add: ac_simps)
379 lemma mod_mult_eq:
380   "((a mod c) * (b mod c)) mod c = (a * b) mod c"
381   by (simp add: mod_mult_left_eq mod_mult_right_eq)
383 lemma mod_prod_eq [mod_simps]:
384   "(\<Prod>i\<in>A. f i mod a) mod a = prod f A mod a"
385 proof (induct A rule: infinite_finite_induct)
386   case (insert i A)
387   then have "(\<Prod>i\<in>insert i A. f i mod a) mod a
388     = (f i mod a * (\<Prod>i\<in>A. f i mod a)) mod a"
389     by simp
390   also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i mod a) mod a)) mod a"
392   also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i) mod a)) mod a"
394   finally show ?case
395     by (simp add: insert.hyps mod_simps)
396 qed simp_all
398 lemma mod_mult_cong:
399   assumes "a mod c = a' mod c"
400   assumes "b mod c = b' mod c"
401   shows "(a * b) mod c = (a' * b') mod c"
402 proof -
403   have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c"
404     unfolding assms ..
405   then show ?thesis
407 qed
409 text \<open>Exponentiation respects modular equivalence.\<close>
411 lemma power_mod [mod_simps]:
412   "((a mod b) ^ n) mod b = (a ^ n) mod b"
413 proof (induct n)
414   case 0
415   then show ?case by simp
416 next
417   case (Suc n)
418   have "(a mod b) ^ Suc n mod b = (a mod b) * ((a mod b) ^ n mod b) mod b"
420   with Suc show ?case
421     by (simp add: mod_mult_left_eq mod_mult_right_eq)
422 qed
424 end
427 class euclidean_ring_cancel = euclidean_ring + euclidean_semiring_cancel
428 begin
430 subclass idom_divide ..
432 lemma div_minus_minus [simp]: "(- a) div (- b) = a div b"
433   using div_mult_mult1 [of "- 1" a b] by simp
435 lemma mod_minus_minus [simp]: "(- a) mod (- b) = - (a mod b)"
436   using mod_mult_mult1 [of "- 1" a b] by simp
438 lemma div_minus_right: "a div (- b) = (- a) div b"
439   using div_minus_minus [of "- a" b] by simp
441 lemma mod_minus_right: "a mod (- b) = - ((- a) mod b)"
442   using mod_minus_minus [of "- a" b] by simp
444 lemma div_minus1_right [simp]: "a div (- 1) = - a"
445   using div_minus_right [of a 1] by simp
447 lemma mod_minus1_right [simp]: "a mod (- 1) = 0"
448   using mod_minus_right [of a 1] by simp
450 text \<open>Negation respects modular equivalence.\<close>
452 lemma mod_minus_eq [mod_simps]:
453   "(- (a mod b)) mod b = (- a) mod b"
454 proof -
455   have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
456     by (simp only: div_mult_mod_eq)
457   also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
459   also have "\<dots> = (- (a mod b)) mod b"
460     by (rule mod_mult_self1)
461   finally show ?thesis
462     by (rule sym)
463 qed
465 lemma mod_minus_cong:
466   assumes "a mod b = a' mod b"
467   shows "(- a) mod b = (- a') mod b"
468 proof -
469   have "(- (a mod b)) mod b = (- (a' mod b)) mod b"
470     unfolding assms ..
471   then show ?thesis
473 qed
475 text \<open>Subtraction respects modular equivalence.\<close>
477 lemma mod_diff_left_eq [mod_simps]:
478   "(a mod c - b) mod c = (a - b) mod c"
479   using mod_add_cong [of a c "a mod c" "- b" "- b"]
480   by simp
482 lemma mod_diff_right_eq [mod_simps]:
483   "(a - b mod c) mod c = (a - b) mod c"
484   using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
485   by simp
487 lemma mod_diff_eq:
488   "(a mod c - b mod c) mod c = (a - b) mod c"
489   using mod_add_cong [of a c "a mod c" "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
490   by simp
492 lemma mod_diff_cong:
493   assumes "a mod c = a' mod c"
494   assumes "b mod c = b' mod c"
495   shows "(a - b) mod c = (a' - b') mod c"
496   using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"]
497   by simp
499 lemma minus_mod_self2 [simp]:
500   "(a - b) mod b = a mod b"
501   using mod_diff_right_eq [of a b b]
504 lemma minus_mod_self1 [simp]:
505   "(b - a) mod b = - a mod b"
506   using mod_add_self2 [of "- a" b] by simp
508 lemma mod_eq_dvd_iff:
509   "a mod c = b mod c \<longleftrightarrow> c dvd a - b" (is "?P \<longleftrightarrow> ?Q")
510 proof
511   assume ?P
512   then have "(a mod c - b mod c) mod c = 0"
513     by simp
514   then show ?Q
515     by (simp add: dvd_eq_mod_eq_0 mod_simps)
516 next
517   assume ?Q
518   then obtain d where d: "a - b = c * d" ..
519   then have "a = c * d + b"
521   then show ?P by simp
522 qed
524 lemma mod_eqE:
525   assumes "a mod c = b mod c"
526   obtains d where "b = a + c * d"
527 proof -
528   from assms have "c dvd a - b"
530   then obtain d where "a - b = c * d" ..
531   then have "b = a + c * - d"
533   with that show thesis .
534 qed
536 end
539 subsection \<open>Uniquely determined division\<close>
541 class unique_euclidean_semiring = euclidean_semiring +
542   assumes euclidean_size_mult: "euclidean_size (a * b) = euclidean_size a * euclidean_size b"
543   fixes division_segment :: "'a \<Rightarrow> 'a"
544   assumes is_unit_division_segment [simp]: "is_unit (division_segment a)"
545     and division_segment_mult:
546     "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> division_segment (a * b) = division_segment a * division_segment b"
547     and division_segment_mod:
548     "b \<noteq> 0 \<Longrightarrow> \<not> b dvd a \<Longrightarrow> division_segment (a mod b) = division_segment b"
549   assumes div_bounded:
550     "b \<noteq> 0 \<Longrightarrow> division_segment r = division_segment b
551     \<Longrightarrow> euclidean_size r < euclidean_size b
552     \<Longrightarrow> (q * b + r) div b = q"
553 begin
555 lemma division_segment_not_0 [simp]:
556   "division_segment a \<noteq> 0"
557   using is_unit_division_segment [of a] is_unitE [of "division_segment a"] by blast
559 lemma divmod_cases [case_names divides remainder by0]:
560   obtains
561     (divides) q where "b \<noteq> 0"
562       and "a div b = q"
563       and "a mod b = 0"
564       and "a = q * b"
565   | (remainder) q r where "b \<noteq> 0"
566       and "division_segment r = division_segment b"
567       and "euclidean_size r < euclidean_size b"
568       and "r \<noteq> 0"
569       and "a div b = q"
570       and "a mod b = r"
571       and "a = q * b + r"
572   | (by0) "b = 0"
573 proof (cases "b = 0")
574   case True
575   then show thesis
576   by (rule by0)
577 next
578   case False
579   show thesis
580   proof (cases "b dvd a")
581     case True
582     then obtain q where "a = b * q" ..
583     with \<open>b \<noteq> 0\<close> divides
584     show thesis
586   next
587     case False
588     then have "a mod b \<noteq> 0"
590     moreover from \<open>b \<noteq> 0\<close> \<open>\<not> b dvd a\<close> have "division_segment (a mod b) = division_segment b"
591       by (rule division_segment_mod)
592     moreover have "euclidean_size (a mod b) < euclidean_size b"
593       using \<open>b \<noteq> 0\<close> by (rule mod_size_less)
594     moreover have "a = a div b * b + a mod b"
596     ultimately show thesis
597       using \<open>b \<noteq> 0\<close> by (blast intro!: remainder)
598   qed
599 qed
601 lemma div_eqI:
602   "a div b = q" if "b \<noteq> 0" "division_segment r = division_segment b"
603     "euclidean_size r < euclidean_size b" "q * b + r = a"
604 proof -
605   from that have "(q * b + r) div b = q"
606     by (auto intro: div_bounded)
607   with that show ?thesis
608     by simp
609 qed
611 lemma mod_eqI:
612   "a mod b = r" if "b \<noteq> 0" "division_segment r = division_segment b"
613     "euclidean_size r < euclidean_size b" "q * b + r = a"
614 proof -
615   from that have "a div b = q"
616     by (rule div_eqI)
617   moreover have "a div b * b + a mod b = a"
618     by (fact div_mult_mod_eq)
619   ultimately have "a div b * b + a mod b = a div b * b + r"
620     using \<open>q * b + r = a\<close> by simp
621   then show ?thesis
622     by simp
623 qed
625 subclass euclidean_semiring_cancel
626 proof
627   show "(a + c * b) div b = c + a div b" if "b \<noteq> 0" for a b c
628   proof (cases a b rule: divmod_cases)
629     case by0
630     with \<open>b \<noteq> 0\<close> show ?thesis
631       by simp
632   next
633     case (divides q)
634     then show ?thesis
636   next
637     case (remainder q r)
638     then show ?thesis
639       by (auto intro: div_eqI simp add: algebra_simps)
640   qed
641 next
642   show"(c * a) div (c * b) = a div b" if "c \<noteq> 0" for a b c
643   proof (cases a b rule: divmod_cases)
644     case by0
645     then show ?thesis
646       by simp
647   next
648     case (divides q)
649     with \<open>c \<noteq> 0\<close> show ?thesis
650       by (simp add: mult.left_commute [of c])
651   next
652     case (remainder q r)
653     from \<open>b \<noteq> 0\<close> \<open>c \<noteq> 0\<close> have "b * c \<noteq> 0"
654       by simp
655     from remainder \<open>c \<noteq> 0\<close>
656     have "division_segment (r * c) = division_segment (b * c)"
657       and "euclidean_size (r * c) < euclidean_size (b * c)"
658       by (simp_all add: division_segment_mult division_segment_mod euclidean_size_mult)
659     with remainder show ?thesis
660       by (auto intro!: div_eqI [of _ "c * (a mod b)"] simp add: algebra_simps)
661         (use \<open>b * c \<noteq> 0\<close> in simp)
662   qed
663 qed
665 lemma div_mult1_eq:
666   "(a * b) div c = a * (b div c) + a * (b mod c) div c"
667 proof (cases "a * (b mod c)" c rule: divmod_cases)
668   case (divides q)
669   have "a * b = a * (b div c * c + b mod c)"
671   also have "\<dots> = (a * (b div c) + q) * c"
672     using divides by (simp add: algebra_simps)
673   finally have "(a * b) div c = \<dots> div c"
674     by simp
675   with divides show ?thesis
676     by simp
677 next
678   case (remainder q r)
679   from remainder(1-3) show ?thesis
680   proof (rule div_eqI)
681     have "a * b = a * (b div c * c + b mod c)"
683     also have "\<dots> = a * c * (b div c) + q * c + r"
684       using remainder by (simp add: algebra_simps)
685     finally show "(a * (b div c) + a * (b mod c) div c) * c + r = a * b"
686       using remainder(5-7) by (simp add: algebra_simps)
687   qed
688 next
689   case by0
690   then show ?thesis
691     by simp
692 qed
695   "(a + b) div c = a div c + b div c + (a mod c + b mod c) div c"
696 proof (cases "a mod c + b mod c" c rule: divmod_cases)
697   case (divides q)
698   have "a + b = (a div c * c + a mod c) + (b div c * c + b mod c)"
699     using mod_mult_div_eq [of a c] mod_mult_div_eq [of b c] by (simp add: ac_simps)
700   also have "\<dots> = (a div c + b div c) * c + (a mod c + b mod c)"
702   also have "\<dots> = (a div c + b div c + q) * c"
703     using divides by (simp add: algebra_simps)
704   finally have "(a + b) div c = (a div c + b div c + q) * c div c"
705     by simp
706   with divides show ?thesis
707     by simp
708 next
709   case (remainder q r)
710   from remainder(1-3) show ?thesis
711   proof (rule div_eqI)
712     have "(a div c + b div c + q) * c + r + (a mod c + b mod c) =
713         (a div c * c + a mod c) + (b div c * c + b mod c) + q * c + r"
715     also have "\<dots> = a + b + (a mod c + b mod c)"
717     finally show "(a div c + b div c + (a mod c + b mod c) div c) * c + r = a + b"
718       using remainder by simp
719   qed
720 next
721   case by0
722   then show ?thesis
723     by simp
724 qed
726 lemma div_eq_0_iff:
727   "a div b = 0 \<longleftrightarrow> euclidean_size a < euclidean_size b \<or> b = 0" (is "_ \<longleftrightarrow> ?P")
728   if "division_segment a = division_segment b"
729 proof
730   assume ?P
731   with that show "a div b = 0"
732     by (cases "b = 0") (auto intro: div_eqI)
733 next
734   assume "a div b = 0"
735   then have "a mod b = a"
736     using div_mult_mod_eq [of a b] by simp
737   with mod_size_less [of b a] show ?P
738     by auto
739 qed
741 end
743 class unique_euclidean_ring = euclidean_ring + unique_euclidean_semiring
744 begin
746 subclass euclidean_ring_cancel ..
748 end
751 subsection \<open>Euclidean division on @{typ nat}\<close>
753 instantiation nat :: normalization_semidom
754 begin
756 definition normalize_nat :: "nat \<Rightarrow> nat"
757   where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
759 definition unit_factor_nat :: "nat \<Rightarrow> nat"
760   where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
762 lemma unit_factor_simps [simp]:
763   "unit_factor 0 = (0::nat)"
764   "unit_factor (Suc n) = 1"
767 definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
768   where "m div n = (if n = 0 then 0 else Max {k::nat. k * n \<le> m})"
770 instance
771   by standard (auto simp add: divide_nat_def ac_simps unit_factor_nat_def intro: Max_eqI)
773 end
775 instantiation nat :: unique_euclidean_semiring
776 begin
778 definition euclidean_size_nat :: "nat \<Rightarrow> nat"
779   where [simp]: "euclidean_size_nat = id"
781 definition division_segment_nat :: "nat \<Rightarrow> nat"
782   where [simp]: "division_segment_nat n = 1"
784 definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
785   where "m mod n = m - (m div n * (n::nat))"
787 instance proof
788   fix m n :: nat
789   have ex: "\<exists>k. k * n \<le> l" for l :: nat
790     by (rule exI [of _ 0]) simp
791   have fin: "finite {k. k * n \<le> l}" if "n > 0" for l
792   proof -
793     from that have "{k. k * n \<le> l} \<subseteq> {k. k \<le> l}"
794       by (cases n) auto
795     then show ?thesis
796       by (rule finite_subset) simp
797   qed
798   have mult_div_unfold: "n * (m div n) = Max {l. l \<le> m \<and> n dvd l}"
799   proof (cases "n = 0")
800     case True
801     moreover have "{l. l = 0 \<and> l \<le> m} = {0::nat}"
802       by auto
803     ultimately show ?thesis
804       by simp
805   next
806     case False
807     with ex [of m] fin have "n * Max {k. k * n \<le> m} = Max (times n ` {k. k * n \<le> m})"
808       by (auto simp add: nat_mult_max_right intro: hom_Max_commute)
809     also have "times n ` {k. k * n \<le> m} = {l. l \<le> m \<and> n dvd l}"
810       by (auto simp add: ac_simps elim!: dvdE)
811     finally show ?thesis
812       using False by (simp add: divide_nat_def ac_simps)
813   qed
814   have less_eq: "m div n * n \<le> m"
815     by (auto simp add: mult_div_unfold ac_simps intro: Max.boundedI)
816   then show "m div n * n + m mod n = m"
818   assume "n \<noteq> 0"
819   show "euclidean_size (m mod n) < euclidean_size n"
820   proof -
821     have "m < Suc (m div n) * n"
822     proof (rule ccontr)
823       assume "\<not> m < Suc (m div n) * n"
824       then have "Suc (m div n) * n \<le> m"
826       moreover from \<open>n \<noteq> 0\<close> have "Max {k. k * n \<le> m} < Suc (m div n)"
828       with \<open>n \<noteq> 0\<close> ex fin have "\<And>k. k * n \<le> m \<Longrightarrow> k < Suc (m div n)"
829         by auto
830       ultimately have "Suc (m div n) < Suc (m div n)"
831         by blast
832       then show False
833         by simp
834     qed
835     with \<open>n \<noteq> 0\<close> show ?thesis
837   qed
838   show "euclidean_size m \<le> euclidean_size (m * n)"
839     using \<open>n \<noteq> 0\<close> by (cases n) simp_all
840   fix q r :: nat
841   show "(q * n + r) div n = q" if "euclidean_size r < euclidean_size n"
842   proof -
843     from that have "r < n"
844       by simp
845     have "k \<le> q" if "k * n \<le> q * n + r" for k
846     proof (rule ccontr)
847       assume "\<not> k \<le> q"
848       then have "q < k"
849         by simp
850       then obtain l where "k = Suc (q + l)"
852       with \<open>r < n\<close> that show False
854     qed
855     with \<open>n \<noteq> 0\<close> ex fin show ?thesis
856       by (auto simp add: divide_nat_def Max_eq_iff)
857   qed
858 qed simp_all
860 end
862 text \<open>Tool support\<close>
864 ML \<open>
865 structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
866 (
867   val div_name = @{const_name divide};
868   val mod_name = @{const_name modulo};
869   val mk_binop = HOLogic.mk_binop;
870   val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
871   val mk_sum = Arith_Data.mk_sum;
872   fun dest_sum tm =
873     if HOLogic.is_zero tm then []
874     else
875       (case try HOLogic.dest_Suc tm of
876         SOME t => HOLogic.Suc_zero :: dest_sum t
877       | NONE =>
878           (case try dest_plus tm of
879             SOME (t, u) => dest_sum t @ dest_sum u
880           | NONE => [tm]));
882   val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
884   val prove_eq_sums = Arith_Data.prove_conv2 all_tac
886 )
887 \<close>
889 simproc_setup cancel_div_mod_nat ("(m::nat) + n") =
890   \<open>K Cancel_Div_Mod_Nat.proc\<close>
892 lemma div_nat_eqI:
893   "m div n = q" if "n * q \<le> m" and "m < n * Suc q" for m n q :: nat
894   by (rule div_eqI [of _ "m - n * q"]) (use that in \<open>simp_all add: algebra_simps\<close>)
896 lemma mod_nat_eqI:
897   "m mod n = r" if "r < n" and "r \<le> m" and "n dvd m - r" for m n r :: nat
898   by (rule mod_eqI [of _ _ "(m - r) div n"]) (use that in \<open>simp_all add: algebra_simps\<close>)
900 lemma div_mult_self_is_m [simp]:
901   "m * n div n = m" if "n > 0" for m n :: nat
902   using that by simp
904 lemma div_mult_self1_is_m [simp]:
905   "n * m div n = m" if "n > 0" for m n :: nat
906   using that by simp
908 lemma mod_less_divisor [simp]:
909   "m mod n < n" if "n > 0" for m n :: nat
910   using mod_size_less [of n m] that by simp
912 lemma mod_le_divisor [simp]:
913   "m mod n \<le> n" if "n > 0" for m n :: nat
914   using that by (auto simp add: le_less)
916 lemma div_times_less_eq_dividend [simp]:
917   "m div n * n \<le> m" for m n :: nat
918   by (simp add: minus_mod_eq_div_mult [symmetric])
920 lemma times_div_less_eq_dividend [simp]:
921   "n * (m div n) \<le> m" for m n :: nat
922   using div_times_less_eq_dividend [of m n]
925 lemma dividend_less_div_times:
926   "m < n + (m div n) * n" if "0 < n" for m n :: nat
927 proof -
928   from that have "m mod n < n"
929     by simp
930   then show ?thesis
931     by (simp add: minus_mod_eq_div_mult [symmetric])
932 qed
934 lemma dividend_less_times_div:
935   "m < n + n * (m div n)" if "0 < n" for m n :: nat
936   using dividend_less_div_times [of n m] that
939 lemma mod_Suc_le_divisor [simp]:
940   "m mod Suc n \<le> n"
941   using mod_less_divisor [of "Suc n" m] by arith
943 lemma mod_less_eq_dividend [simp]:
944   "m mod n \<le> m" for m n :: nat
946   from div_mult_mod_eq have "m div n * n + m mod n = m" .
947   then show "m div n * n + m mod n \<le> m" by auto
948 qed
950 lemma
951   div_less [simp]: "m div n = 0"
952   and mod_less [simp]: "m mod n = m"
953   if "m < n" for m n :: nat
954   using that by (auto intro: div_eqI mod_eqI)
956 lemma le_div_geq:
957   "m div n = Suc ((m - n) div n)" if "0 < n" and "n \<le> m" for m n :: nat
958 proof -
959   from \<open>n \<le> m\<close> obtain q where "m = n + q"
961   with \<open>0 < n\<close> show ?thesis
963 qed
965 lemma le_mod_geq:
966   "m mod n = (m - n) mod n" if "n \<le> m" for m n :: nat
967 proof -
968   from \<open>n \<le> m\<close> obtain q where "m = n + q"
970   then show ?thesis
971     by simp
972 qed
974 lemma div_if:
975   "m div n = (if m < n \<or> n = 0 then 0 else Suc ((m - n) div n))"
978 lemma mod_if:
979   "m mod n = (if m < n then m else (m - n) mod n)" for m n :: nat
982 lemma div_eq_0_iff:
983   "m div n = 0 \<longleftrightarrow> m < n \<or> n = 0" for m n :: nat
986 lemma div_greater_zero_iff:
987   "m div n > 0 \<longleftrightarrow> n \<le> m \<and> n > 0" for m n :: nat
988   using div_eq_0_iff [of m n] by auto
990 lemma mod_greater_zero_iff_not_dvd:
991   "m mod n > 0 \<longleftrightarrow> \<not> n dvd m" for m n :: nat
994 lemma div_by_Suc_0 [simp]:
995   "m div Suc 0 = m"
996   using div_by_1 [of m] by simp
998 lemma mod_by_Suc_0 [simp]:
999   "m mod Suc 0 = 0"
1000   using mod_by_1 [of m] by simp
1002 lemma div2_Suc_Suc [simp]:
1003   "Suc (Suc m) div 2 = Suc (m div 2)"
1004   by (simp add: numeral_2_eq_2 le_div_geq)
1006 lemma Suc_n_div_2_gt_zero [simp]:
1007   "0 < Suc n div 2" if "n > 0" for n :: nat
1008   using that by (cases n) simp_all
1010 lemma div_2_gt_zero [simp]:
1011   "0 < n div 2" if "Suc 0 < n" for n :: nat
1012   using that Suc_n_div_2_gt_zero [of "n - 1"] by simp
1014 lemma mod2_Suc_Suc [simp]:
1015   "Suc (Suc m) mod 2 = m mod 2"
1016   by (simp add: numeral_2_eq_2 le_mod_geq)
1019   "(m + m) div 2 = m" for m :: nat
1020   by (simp add: mult_2 [symmetric])
1023   "(m + m) mod 2 = 0" for m :: nat
1024   by (simp add: mult_2 [symmetric])
1026 lemma mod2_gr_0 [simp]:
1027   "0 < m mod 2 \<longleftrightarrow> m mod 2 = 1" for m :: nat
1028 proof -
1029   have "m mod 2 < 2"
1030     by (rule mod_less_divisor) simp
1031   then have "m mod 2 = 0 \<or> m mod 2 = 1"
1032     by arith
1033   then show ?thesis
1034     by auto
1035 qed
1037 lemma mod_Suc_eq [mod_simps]:
1038   "Suc (m mod n) mod n = Suc m mod n"
1039 proof -
1040   have "(m mod n + 1) mod n = (m + 1) mod n"
1041     by (simp only: mod_simps)
1042   then show ?thesis
1043     by simp
1044 qed
1046 lemma mod_Suc_Suc_eq [mod_simps]:
1047   "Suc (Suc (m mod n)) mod n = Suc (Suc m) mod n"
1048 proof -
1049   have "(m mod n + 2) mod n = (m + 2) mod n"
1050     by (simp only: mod_simps)
1051   then show ?thesis
1052     by simp
1053 qed
1055 lemma
1056   Suc_mod_mult_self1 [simp]: "Suc (m + k * n) mod n = Suc m mod n"
1057   and Suc_mod_mult_self2 [simp]: "Suc (m + n * k) mod n = Suc m mod n"
1058   and Suc_mod_mult_self3 [simp]: "Suc (k * n + m) mod n = Suc m mod n"
1059   and Suc_mod_mult_self4 [simp]: "Suc (n * k + m) mod n = Suc m mod n"
1060   by (subst mod_Suc_eq [symmetric], simp add: mod_simps)+
1062 context
1063   fixes m n q :: nat
1064 begin
1066 private lemma eucl_rel_mult2:
1067   "m mod n + n * (m div n mod q) < n * q"
1068   if "n > 0" and "q > 0"
1069 proof -
1070   from \<open>n > 0\<close> have "m mod n < n"
1071     by (rule mod_less_divisor)
1072   from \<open>q > 0\<close> have "m div n mod q < q"
1073     by (rule mod_less_divisor)
1074   then obtain s where "q = Suc (m div n mod q + s)"
1076   moreover have "m mod n + n * (m div n mod q) < n * Suc (m div n mod q + s)"
1078   ultimately show ?thesis
1079     by simp
1080 qed
1082 lemma div_mult2_eq:
1083   "m div (n * q) = (m div n) div q"
1084 proof (cases "n = 0 \<or> q = 0")
1085   case True
1086   then show ?thesis
1087     by auto
1088 next
1089   case False
1090   with eucl_rel_mult2 show ?thesis
1091     by (auto intro: div_eqI [of _ "n * (m div n mod q) + m mod n"]
1093 qed
1095 lemma mod_mult2_eq:
1096   "m mod (n * q) = n * (m div n mod q) + m mod n"
1097 proof (cases "n = 0 \<or> q = 0")
1098   case True
1099   then show ?thesis
1100     by auto
1101 next
1102   case False
1103   with eucl_rel_mult2 show ?thesis
1104     by (auto intro: mod_eqI [of _ _ "(m div n) div q"]
1106 qed
1108 end
1110 lemma div_le_mono:
1111   "m div k \<le> n div k" if "m \<le> n" for m n k :: nat
1112 proof -
1113   from that obtain q where "n = m + q"
1115   then show ?thesis
1117 qed
1119 text \<open>Antimonotonicity of @{const divide} in second argument\<close>
1121 lemma div_le_mono2:
1122   "k div n \<le> k div m" if "0 < m" and "m \<le> n" for m n k :: nat
1123 using that proof (induct k arbitrary: m rule: less_induct)
1124   case (less k)
1125   show ?case
1126   proof (cases "n \<le> k")
1127     case False
1128     then show ?thesis
1129       by simp
1130   next
1131     case True
1132     have "(k - n) div n \<le> (k - m) div n"
1133       using less.prems
1134       by (blast intro: div_le_mono diff_le_mono2)
1135     also have "\<dots> \<le> (k - m) div m"
1136       using \<open>n \<le> k\<close> less.prems less.hyps [of "k - m" m]
1137       by simp
1138     finally show ?thesis
1139       using \<open>n \<le> k\<close> less.prems
1141   qed
1142 qed
1144 lemma div_le_dividend [simp]:
1145   "m div n \<le> m" for m n :: nat
1146   using div_le_mono2 [of 1 n m] by (cases "n = 0") simp_all
1148 lemma div_less_dividend [simp]:
1149   "m div n < m" if "1 < n" and "0 < m" for m n :: nat
1150 using that proof (induct m rule: less_induct)
1151   case (less m)
1152   show ?case
1153   proof (cases "n < m")
1154     case False
1155     with less show ?thesis
1156       by (cases "n = m") simp_all
1157   next
1158     case True
1159     then show ?thesis
1160       using less.hyps [of "m - n"] less.prems
1162   qed
1163 qed
1165 lemma div_eq_dividend_iff:
1166   "m div n = m \<longleftrightarrow> n = 1" if "m > 0" for m n :: nat
1167 proof
1168   assume "n = 1"
1169   then show "m div n = m"
1170     by simp
1171 next
1172   assume P: "m div n = m"
1173   show "n = 1"
1174   proof (rule ccontr)
1175     have "n \<noteq> 0"
1176       by (rule ccontr) (use that P in auto)
1177     moreover assume "n \<noteq> 1"
1178     ultimately have "n > 1"
1179       by simp
1180     with that have "m div n < m"
1181       by simp
1182     with P show False
1183       by simp
1184   qed
1185 qed
1187 lemma less_mult_imp_div_less:
1188   "m div n < i" if "m < i * n" for m n i :: nat
1189 proof -
1190   from that have "i * n > 0"
1191     by (cases "i * n = 0") simp_all
1192   then have "i > 0" and "n > 0"
1193     by simp_all
1194   have "m div n * n \<le> m"
1195     by simp
1196   then have "m div n * n < i * n"
1197     using that by (rule le_less_trans)
1198   with \<open>n > 0\<close> show ?thesis
1199     by simp
1200 qed
1202 text \<open>A fact for the mutilated chess board\<close>
1204 lemma mod_Suc:
1205   "Suc m mod n = (if Suc (m mod n) = n then 0 else Suc (m mod n))" (is "_ = ?rhs")
1206 proof (cases "n = 0")
1207   case True
1208   then show ?thesis
1209     by simp
1210 next
1211   case False
1212   have "Suc m mod n = Suc (m mod n) mod n"
1214   also have "\<dots> = ?rhs"
1215     using False by (auto intro!: mod_nat_eqI intro: neq_le_trans simp add: Suc_le_eq)
1216   finally show ?thesis .
1217 qed
1219 lemma Suc_times_mod_eq:
1220   "Suc (m * n) mod m = 1" if "Suc 0 < m"
1221   using that by (simp add: mod_Suc)
1223 lemma Suc_times_numeral_mod_eq [simp]:
1224   "Suc (numeral k * n) mod numeral k = 1" if "numeral k \<noteq> (1::nat)"
1225   by (rule Suc_times_mod_eq) (use that in simp)
1227 lemma Suc_div_le_mono [simp]:
1228   "m div n \<le> Suc m div n"
1231 text \<open>These lemmas collapse some needless occurrences of Suc:
1232   at least three Sucs, since two and fewer are rewritten back to Suc again!
1233   We already have some rules to simplify operands smaller than 3.\<close>
1236   "m div Suc (Suc (Suc n)) = m div (3 + n)"
1240   "m mod Suc (Suc (Suc n)) = m mod (3 + n)"
1244   "Suc (Suc (Suc m)) div n = (3 + m) div n"
1248   "Suc (Suc (Suc m)) mod n = (3 + m) mod n"
1252   Suc_div_eq_add3_div [of _ "numeral v"] for v
1255   Suc_mod_eq_add3_mod [of _ "numeral v"] for v
1257 lemma (in field_char_0) of_nat_div:
1258   "of_nat (m div n) = ((of_nat m - of_nat (m mod n)) / of_nat n)"
1259 proof -
1260   have "of_nat (m div n) = ((of_nat (m div n * n + m mod n) - of_nat (m mod n)) / of_nat n :: 'a)"
1261     unfolding of_nat_add by (cases "n = 0") simp_all
1262   then show ?thesis
1263     by simp
1264 qed
1266 text \<open>An ``induction'' law for modulus arithmetic.\<close>
1268 lemma mod_induct [consumes 3, case_names step]:
1269   "P m" if "P n" and "n < p" and "m < p"
1270     and step: "\<And>n. n < p \<Longrightarrow> P n \<Longrightarrow> P (Suc n mod p)"
1271 using \<open>m < p\<close> proof (induct m)
1272   case 0
1273   show ?case
1274   proof (rule ccontr)
1275     assume "\<not> P 0"
1276     from \<open>n < p\<close> have "0 < p"
1277       by simp
1278     from \<open>n < p\<close> obtain m where "0 < m" and "p = n + m"
1280     with \<open>P n\<close> have "P (p - m)"
1281       by simp
1282     moreover have "\<not> P (p - m)"
1283     using \<open>0 < m\<close> proof (induct m)
1284       case 0
1285       then show ?case
1286         by simp
1287     next
1288       case (Suc m)
1289       show ?case
1290       proof
1291         assume P: "P (p - Suc m)"
1292         with \<open>\<not> P 0\<close> have "Suc m < p"
1293           by (auto intro: ccontr)
1294         then have "Suc (p - Suc m) = p - m"
1295           by arith
1296         moreover from \<open>0 < p\<close> have "p - Suc m < p"
1297           by arith
1298         with P step have "P ((Suc (p - Suc m)) mod p)"
1299           by blast
1300         ultimately show False
1301           using \<open>\<not> P 0\<close> Suc.hyps by (cases "m = 0") simp_all
1302       qed
1303     qed
1304     ultimately show False
1305       by blast
1306   qed
1307 next
1308   case (Suc m)
1309   then have "m < p" and mod: "Suc m mod p = Suc m"
1310     by simp_all
1311   from \<open>m < p\<close> have "P m"
1312     by (rule Suc.hyps)
1313   with \<open>m < p\<close> have "P (Suc m mod p)"
1314     by (rule step)
1315   with mod show ?case
1316     by simp
1317 qed
1319 lemma split_div:
1320   "P (m div n) \<longleftrightarrow> (n = 0 \<longrightarrow> P 0) \<and> (n \<noteq> 0 \<longrightarrow>
1321      (\<forall>i j. j < n \<longrightarrow> m = n * i + j \<longrightarrow> P i))"
1322      (is "?P = ?Q") for m n :: nat
1323 proof (cases "n = 0")
1324   case True
1325   then show ?thesis
1326     by simp
1327 next
1328   case False
1329   show ?thesis
1330   proof
1331     assume ?P
1332     with False show ?Q
1333       by auto
1334   next
1335     assume ?Q
1336     with False have *: "\<And>i j. j < n \<Longrightarrow> m = n * i + j \<Longrightarrow> P i"
1337       by simp
1338     with False show ?P
1339       by (auto intro: * [of "m mod n"])
1340   qed
1341 qed
1343 lemma split_div':
1344   "P (m div n) \<longleftrightarrow> n = 0 \<and> P 0 \<or> (\<exists>q. (n * q \<le> m \<and> m < n * Suc q) \<and> P q)"
1345 proof (cases "n = 0")
1346   case True
1347   then show ?thesis
1348     by simp
1349 next
1350   case False
1351   then have "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> m div n = q" for q
1352     by (auto intro: div_nat_eqI dividend_less_times_div)
1353   then show ?thesis
1354     by auto
1355 qed
1357 lemma split_mod:
1358   "P (m mod n) \<longleftrightarrow> (n = 0 \<longrightarrow> P m) \<and> (n \<noteq> 0 \<longrightarrow>
1359      (\<forall>i j. j < n \<longrightarrow> m = n * i + j \<longrightarrow> P j))"
1360      (is "?P \<longleftrightarrow> ?Q") for m n :: nat
1361 proof (cases "n = 0")
1362   case True
1363   then show ?thesis
1364     by simp
1365 next
1366   case False
1367   show ?thesis
1368   proof
1369     assume ?P
1370     with False show ?Q
1371       by auto
1372   next
1373     assume ?Q
1374     with False have *: "\<And>i j. j < n \<Longrightarrow> m = n * i + j \<Longrightarrow> P j"
1375       by simp
1376     with False show ?P
1377       by (auto intro: * [of _ "m div n"])
1378   qed
1379 qed
1382 subsection \<open>Euclidean division on @{typ int}\<close>
1384 instantiation int :: normalization_semidom
1385 begin
1387 definition normalize_int :: "int \<Rightarrow> int"
1388   where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
1390 definition unit_factor_int :: "int \<Rightarrow> int"
1391   where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
1393 definition divide_int :: "int \<Rightarrow> int \<Rightarrow> int"
1394   where "k div l = (if l = 0 then 0
1395     else if sgn k = sgn l
1396       then int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
1397       else - int (nat \<bar>k\<bar> div nat \<bar>l\<bar> + of_bool (\<not> l dvd k)))"
1399 lemma divide_int_unfold:
1400   "(sgn k * int m) div (sgn l * int n) =
1401    (if sgn l = 0 \<or> sgn k = 0 \<or> n = 0 then 0
1402     else if sgn k = sgn l
1403       then int (m div n)
1404       else - int (m div n + of_bool (\<not> n dvd m)))"
1405   by (auto simp add: divide_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
1406     nat_mult_distrib dvd_int_iff)
1408 instance proof
1409   fix k :: int show "k div 0 = 0"
1411 next
1412   fix k l :: int
1413   assume "l \<noteq> 0"
1414   obtain n m and s t where k: "k = sgn s * int n" and l: "l = sgn t * int m"
1415     by (blast intro: int_sgnE elim: that)
1416   then have "k * l = sgn (s * t) * int (n * m)"
1417     by (simp add: ac_simps sgn_mult)
1418   with k l \<open>l \<noteq> 0\<close> show "k * l div l = k"
1419     by (simp only: divide_int_unfold)
1420       (auto simp add: algebra_simps sgn_mult sgn_1_pos sgn_0_0)
1421 qed (auto simp add: sgn_mult mult_sgn_abs abs_eq_iff')
1423 end
1425 instantiation int :: idom_modulo
1426 begin
1428 definition modulo_int :: "int \<Rightarrow> int \<Rightarrow> int"
1429   where "k mod l = (if l = 0 then k
1430     else if sgn k = sgn l
1431       then sgn l * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)
1432       else sgn l * (\<bar>l\<bar> * of_bool (\<not> l dvd k) - int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)))"
1434 lemma modulo_int_unfold:
1435   "(sgn k * int m) mod (sgn l * int n) =
1436    (if sgn l = 0 \<or> sgn k = 0 \<or> n = 0 then sgn k * int m
1437     else if sgn k = sgn l
1438       then sgn l * int (m mod n)
1439       else sgn l * (int (n * of_bool (\<not> n dvd m)) - int (m mod n)))"
1440   by (auto simp add: modulo_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
1441     nat_mult_distrib dvd_int_iff)
1443 instance proof
1444   fix k l :: int
1445   obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m"
1446     by (blast intro: int_sgnE elim: that)
1447   then show "k div l * l + k mod l = k"
1448     by (auto simp add: divide_int_unfold modulo_int_unfold algebra_simps dest!: sgn_not_eq_imp)
1450          distrib_left [symmetric] minus_mult_right
1451          del: of_nat_mult minus_mult_right [symmetric])
1452 qed
1454 end
1456 instantiation int :: unique_euclidean_ring
1457 begin
1459 definition euclidean_size_int :: "int \<Rightarrow> nat"
1460   where [simp]: "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
1462 definition division_segment_int :: "int \<Rightarrow> int"
1463   where "division_segment_int k = (if k \<ge> 0 then 1 else - 1)"
1465 lemma division_segment_eq_sgn:
1466   "division_segment k = sgn k" if "k \<noteq> 0" for k :: int
1467   using that by (simp add: division_segment_int_def)
1469 lemma abs_division_segment [simp]:
1470   "\<bar>division_segment k\<bar> = 1" for k :: int
1473 lemma abs_mod_less:
1474   "\<bar>k mod l\<bar> < \<bar>l\<bar>" if "l \<noteq> 0" for k l :: int
1475 proof -
1476   obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m"
1477     by (blast intro: int_sgnE elim: that)
1478   with that show ?thesis
1479     by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg
1480       abs_mult mod_greater_zero_iff_not_dvd)
1481 qed
1483 lemma sgn_mod:
1484   "sgn (k mod l) = sgn l" if "l \<noteq> 0" "\<not> l dvd k" for k l :: int
1485 proof -
1486   obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m"
1487     by (blast intro: int_sgnE elim: that)
1488   with that show ?thesis
1489     by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg
1490       sgn_mult mod_eq_0_iff_dvd int_dvd_iff)
1491 qed
1493 instance proof
1494   fix k l :: int
1495   show "division_segment (k mod l) = division_segment l" if
1496     "l \<noteq> 0" and "\<not> l dvd k"
1497     using that by (simp add: division_segment_eq_sgn dvd_eq_mod_eq_0 sgn_mod)
1498 next
1499   fix l q r :: int
1500   obtain n m and s t
1501      where l: "l = sgn s * int n" and q: "q = sgn t * int m"
1502     by (blast intro: int_sgnE elim: that)
1503   assume \<open>l \<noteq> 0\<close>
1504   with l have "s \<noteq> 0" and "n > 0"
1506   assume "division_segment r = division_segment l"
1507   moreover have "r = sgn r * \<bar>r\<bar>"
1509   moreover define u where "u = nat \<bar>r\<bar>"
1510   ultimately have "r = sgn l * int u"
1511     using division_segment_eq_sgn \<open>l \<noteq> 0\<close> by (cases "r = 0") simp_all
1512   with l \<open>n > 0\<close> have r: "r = sgn s * int u"
1514   assume "euclidean_size r < euclidean_size l"
1515   with l r \<open>s \<noteq> 0\<close> have "u < n"
1517   show "(q * l + r) div l = q"
1518   proof (cases "q = 0 \<or> r = 0")
1519     case True
1520     then show ?thesis
1521     proof
1522       assume "q = 0"
1523       then show ?thesis
1524         using l r \<open>u < n\<close> by (simp add: divide_int_unfold)
1525     next
1526       assume "r = 0"
1527       from \<open>r = 0\<close> have *: "q * l + r = sgn (t * s) * int (n * m)"
1528         using q l by (simp add: ac_simps sgn_mult)
1529       from \<open>s \<noteq> 0\<close> \<open>n > 0\<close> show ?thesis
1530         by (simp only: *, simp only: q l divide_int_unfold)
1531           (auto simp add: sgn_mult sgn_0_0 sgn_1_pos)
1532     qed
1533   next
1534     case False
1535     with q r have "t \<noteq> 0" and "m > 0" and "s \<noteq> 0" and "u > 0"
1537     moreover from \<open>0 < m\<close> \<open>u < n\<close> have "u \<le> m * n"
1538       using mult_le_less_imp_less [of 1 m u n] by simp
1539     ultimately have *: "q * l + r = sgn (s * t)
1540       * int (if t < 0 then m * n - u else m * n + u)"
1541       using l q r
1542       by (simp add: sgn_mult algebra_simps of_nat_diff)
1543     have "(m * n - u) div n = m - 1" if "u > 0"
1544       using \<open>0 < m\<close> \<open>u < n\<close> that
1545       by (auto intro: div_nat_eqI simp add: algebra_simps)
1546     moreover have "n dvd m * n - u \<longleftrightarrow> n dvd u"
1547       using \<open>u \<le> m * n\<close> dvd_diffD1 [of n "m * n" u]
1548       by auto
1549     ultimately show ?thesis
1550       using \<open>s \<noteq> 0\<close> \<open>m > 0\<close> \<open>u > 0\<close> \<open>u < n\<close> \<open>u \<le> m * n\<close>
1551       by (simp only: *, simp only: l q divide_int_unfold)
1552         (auto simp add: sgn_mult sgn_0_0 sgn_1_pos algebra_simps dest: dvd_imp_le)
1553   qed
1554 qed (use mult_le_mono2 [of 1] in \<open>auto simp add: division_segment_int_def not_le sign_simps abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\<close>)
1556 end
1558 lemma pos_mod_bound [simp]:
1559   "k mod l < l" if "l > 0" for k l :: int
1560 proof -
1561   obtain m and s where "k = sgn s * int m"
1562     by (blast intro: int_sgnE elim: that)
1563   moreover from that obtain n where "l = sgn 1 * int n"
1564     by (cases l) auto
1565   ultimately show ?thesis
1566     using that by (simp only: modulo_int_unfold)
1568 qed
1570 lemma pos_mod_sign [simp]:
1571   "0 \<le> k mod l" if "l > 0" for k l :: int
1572 proof -
1573   obtain m and s where "k = sgn s * int m"
1574     by (blast intro: int_sgnE elim: that)
1575   moreover from that obtain n where "l = sgn 1 * int n"
1576     by (cases l) auto
1577   ultimately show ?thesis
1578     using that by (simp only: modulo_int_unfold) simp
1579 qed
1582 subsection \<open>Code generation\<close>
1584 code_identifier
1585   code_module Euclidean_Division \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
1587 end