src/HOL/Divides.thy
 author haftmann Sat Oct 17 13:18:43 2015 +0200 (2015-10-17) changeset 61433 a4c0de1df3d8 parent 61275 053ec04ea866 child 61649 268d88ec9087 permissions -rw-r--r--
qualify some names stemming from internal bootstrap constructions
1 (*  Title:      HOL/Divides.thy
2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3     Copyright   1999  University of Cambridge
4 *)
6 section \<open>The division operators div and mod\<close>
8 theory Divides
9 imports Parity
10 begin
12 subsection \<open>Abstract division in commutative semirings.\<close>
14 class div = dvd + divide +
15   fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "mod" 70)
17 class semiring_div = semidom + div +
18   assumes mod_div_equality: "a div b * b + a mod b = a"
19     and div_by_0 [simp]: "a div 0 = 0"
20     and div_0 [simp]: "0 div a = 0"
21     and div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
22     and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
23 begin
25 subclass algebraic_semidom
26 proof
27   fix b a
28   assume "b \<noteq> 0"
29   then show "a * b div b = a"
30     using div_mult_self1 [of b 0 a] by (simp add: ac_simps)
31 qed simp
33 lemma div_by_1:
34   "a div 1 = a"
35   by (fact divide_1)
37 lemma div_mult_self1_is_id:
38   "b \<noteq> 0 \<Longrightarrow> b * a div b = a"
39   by (fact nonzero_mult_divide_cancel_left)
41 lemma div_mult_self2_is_id:
42   "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
43   by (fact nonzero_mult_divide_cancel_right)
45 text \<open>@{const divide} and @{const mod}\<close>
47 lemma mod_div_equality2: "b * (a div b) + a mod b = a"
48   unfolding mult.commute [of b]
49   by (rule mod_div_equality)
51 lemma mod_div_equality': "a mod b + a div b * b = a"
52   using mod_div_equality [of a b]
53   by (simp only: ac_simps)
55 lemma div_mod_equality: "((a div b) * b + a mod b) + c = a + c"
58 lemma div_mod_equality2: "(b * (a div b) + a mod b) + c = a + c"
61 lemma mod_by_0 [simp]: "a mod 0 = a"
62   using mod_div_equality [of a zero] by simp
64 lemma mod_0 [simp]: "0 mod a = 0"
65   using mod_div_equality [of zero a] div_0 by simp
67 lemma div_mult_self2 [simp]:
68   assumes "b \<noteq> 0"
69   shows "(a + b * c) div b = c + a div b"
70   using assms div_mult_self1 [of b a c] by (simp add: mult.commute)
72 lemma div_mult_self3 [simp]:
73   assumes "b \<noteq> 0"
74   shows "(c * b + a) div b = c + a div b"
77 lemma div_mult_self4 [simp]:
78   assumes "b \<noteq> 0"
79   shows "(b * c + a) div b = c + a div b"
82 lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b"
83 proof (cases "b = 0")
84   case True then show ?thesis by simp
85 next
86   case False
87   have "a + c * b = (a + c * b) div b * b + (a + c * b) mod b"
89   also from False div_mult_self1 [of b a c] have
90     "\<dots> = (c + a div b) * b + (a + c * b) mod b"
92   finally have "a = a div b * b + (a + c * b) mod b"
94   then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
96   then show ?thesis by simp
97 qed
99 lemma mod_mult_self2 [simp]:
100   "(a + b * c) mod b = a mod b"
101   by (simp add: mult.commute [of b])
103 lemma mod_mult_self3 [simp]:
104   "(c * b + a) mod b = a mod b"
107 lemma mod_mult_self4 [simp]:
108   "(b * c + a) mod b = a mod b"
111 lemma mod_mult_self1_is_0 [simp]:
112   "b * a mod b = 0"
113   using mod_mult_self2 [of 0 b a] by simp
115 lemma mod_mult_self2_is_0 [simp]:
116   "a * b mod b = 0"
117   using mod_mult_self1 [of 0 a b] by simp
119 lemma mod_by_1 [simp]:
120   "a mod 1 = 0"
121 proof -
122   from mod_div_equality [of a one] div_by_1 have "a + a mod 1 = a" by simp
123   then have "a + a mod 1 = a + 0" by simp
124   then show ?thesis by (rule add_left_imp_eq)
125 qed
127 lemma mod_self [simp]:
128   "a mod a = 0"
129   using mod_mult_self2_is_0 [of 1] by simp
132   assumes "b \<noteq> 0"
133   shows "(b + a) div b = a div b + 1"
134   using assms div_mult_self1 [of b a 1] by (simp add: add.commute)
137   assumes "b \<noteq> 0"
138   shows "(a + b) div b = a div b + 1"
142   "(b + a) mod b = a mod b"
146   "(a + b) mod b = a mod b"
147   using mod_mult_self1 [of a 1 b] by simp
149 lemma mod_div_decomp:
150   fixes a b
151   obtains q r where "q = a div b" and "r = a mod b"
152     and "a = q * b + r"
153 proof -
154   from mod_div_equality have "a = a div b * b + a mod b" by simp
155   moreover have "a div b = a div b" ..
156   moreover have "a mod b = a mod b" ..
157   note that ultimately show thesis by blast
158 qed
160 lemma dvd_imp_mod_0 [simp]:
161   assumes "a dvd b"
162   shows "b mod a = 0"
163 proof -
164   from assms obtain c where "b = a * c" ..
165   then have "b mod a = a * c mod a" by simp
166   then show "b mod a = 0" by simp
167 qed
169 lemma mod_eq_0_iff_dvd:
170   "a mod b = 0 \<longleftrightarrow> b dvd a"
171 proof
172   assume "b dvd a"
173   then show "a mod b = 0" by simp
174 next
175   assume "a mod b = 0"
176   with mod_div_equality [of a b] have "a div b * b = a" by simp
177   then have "a = b * (a div b)" by (simp add: ac_simps)
178   then show "b dvd a" ..
179 qed
181 lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]:
182   "a dvd b \<longleftrightarrow> b mod a = 0"
185 lemma mod_div_trivial [simp]:
186   "a mod b div b = 0"
187 proof (cases "b = 0")
188   assume "b = 0"
189   thus ?thesis by simp
190 next
191   assume "b \<noteq> 0"
192   hence "a div b + a mod b div b = (a mod b + a div b * b) div b"
193     by (rule div_mult_self1 [symmetric])
194   also have "\<dots> = a div b"
195     by (simp only: mod_div_equality')
196   also have "\<dots> = a div b + 0"
197     by simp
198   finally show ?thesis
200 qed
202 lemma mod_mod_trivial [simp]:
203   "a mod b mod b = a mod b"
204 proof -
205   have "a mod b mod b = (a mod b + a div b * b) mod b"
206     by (simp only: mod_mult_self1)
207   also have "\<dots> = a mod b"
208     by (simp only: mod_div_equality')
209   finally show ?thesis .
210 qed
212 lemma dvd_mod_imp_dvd:
213   assumes "k dvd m mod n" and "k dvd n"
214   shows "k dvd m"
215 proof -
216   from assms have "k dvd (m div n) * n + m mod n"
217     by (simp only: dvd_add dvd_mult)
218   then show ?thesis by (simp add: mod_div_equality)
219 qed
221 text \<open>Addition respects modular equivalence.\<close>
223 lemma mod_add_left_eq: -- \<open>FIXME reorient\<close>
224   "(a + b) mod c = (a mod c + b) mod c"
225 proof -
226   have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
227     by (simp only: mod_div_equality)
228   also have "\<dots> = (a mod c + b + a div c * c) mod c"
229     by (simp only: ac_simps)
230   also have "\<dots> = (a mod c + b) mod c"
231     by (rule mod_mult_self1)
232   finally show ?thesis .
233 qed
235 lemma mod_add_right_eq: -- \<open>FIXME reorient\<close>
236   "(a + b) mod c = (a + b mod c) mod c"
237 proof -
238   have "(a + b) mod c = (a + (b div c * c + b mod c)) mod c"
239     by (simp only: mod_div_equality)
240   also have "\<dots> = (a + b mod c + b div c * c) mod c"
241     by (simp only: ac_simps)
242   also have "\<dots> = (a + b mod c) mod c"
243     by (rule mod_mult_self1)
244   finally show ?thesis .
245 qed
247 lemma mod_add_eq: -- \<open>FIXME reorient\<close>
248   "(a + b) mod c = (a mod c + b mod c) mod c"
252   assumes "a mod c = a' mod c"
253   assumes "b mod c = b' mod c"
254   shows "(a + b) mod c = (a' + b') mod c"
255 proof -
256   have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c"
257     unfolding assms ..
258   thus ?thesis
259     by (simp only: mod_add_eq [symmetric])
260 qed
262 text \<open>Multiplication respects modular equivalence.\<close>
264 lemma mod_mult_left_eq: -- \<open>FIXME reorient\<close>
265   "(a * b) mod c = ((a mod c) * b) mod c"
266 proof -
267   have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
268     by (simp only: mod_div_equality)
269   also have "\<dots> = (a mod c * b + a div c * b * c) mod c"
270     by (simp only: algebra_simps)
271   also have "\<dots> = (a mod c * b) mod c"
272     by (rule mod_mult_self1)
273   finally show ?thesis .
274 qed
276 lemma mod_mult_right_eq: -- \<open>FIXME reorient\<close>
277   "(a * b) mod c = (a * (b mod c)) mod c"
278 proof -
279   have "(a * b) mod c = (a * (b div c * c + b mod c)) mod c"
280     by (simp only: mod_div_equality)
281   also have "\<dots> = (a * (b mod c) + a * (b div c) * c) mod c"
282     by (simp only: algebra_simps)
283   also have "\<dots> = (a * (b mod c)) mod c"
284     by (rule mod_mult_self1)
285   finally show ?thesis .
286 qed
288 lemma mod_mult_eq: -- \<open>FIXME reorient\<close>
289   "(a * b) mod c = ((a mod c) * (b mod c)) mod c"
290 by (rule trans [OF mod_mult_left_eq mod_mult_right_eq])
292 lemma mod_mult_cong:
293   assumes "a mod c = a' mod c"
294   assumes "b mod c = b' mod c"
295   shows "(a * b) mod c = (a' * b') mod c"
296 proof -
297   have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c"
298     unfolding assms ..
299   thus ?thesis
300     by (simp only: mod_mult_eq [symmetric])
301 qed
303 text \<open>Exponentiation respects modular equivalence.\<close>
305 lemma power_mod: "(a mod b) ^ n mod b = a ^ n mod b"
306 apply (induct n, simp_all)
307 apply (rule mod_mult_right_eq [THEN trans])
308 apply (simp (no_asm_simp))
309 apply (rule mod_mult_eq [symmetric])
310 done
312 lemma mod_mod_cancel:
313   assumes "c dvd b"
314   shows "a mod b mod c = a mod c"
315 proof -
316   from \<open>c dvd b\<close> obtain k where "b = c * k"
317     by (rule dvdE)
318   have "a mod b mod c = a mod (c * k) mod c"
319     by (simp only: \<open>b = c * k\<close>)
320   also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"
321     by (simp only: mod_mult_self1)
322   also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
323     by (simp only: ac_simps)
324   also have "\<dots> = a mod c"
325     by (simp only: mod_div_equality)
326   finally show ?thesis .
327 qed
329 lemma div_mult_mult2 [simp]:
330   "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
331   by (drule div_mult_mult1) (simp add: mult.commute)
333 lemma div_mult_mult1_if [simp]:
334   "(c * a) div (c * b) = (if c = 0 then 0 else a div b)"
335   by simp_all
337 lemma mod_mult_mult1:
338   "(c * a) mod (c * b) = c * (a mod b)"
339 proof (cases "c = 0")
340   case True then show ?thesis by simp
341 next
342   case False
343   from mod_div_equality
344   have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .
345   with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)
346     = c * a + c * (a mod b)" by (simp add: algebra_simps)
347   with mod_div_equality show ?thesis by simp
348 qed
350 lemma mod_mult_mult2:
351   "(a * c) mod (b * c) = (a mod b) * c"
352   using mod_mult_mult1 [of c a b] by (simp add: mult.commute)
354 lemma mult_mod_left: "(a mod b) * c = (a * c) mod (b * c)"
355   by (fact mod_mult_mult2 [symmetric])
357 lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)"
358   by (fact mod_mult_mult1 [symmetric])
360 lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
361   unfolding dvd_def by (auto simp add: mod_mult_mult1)
363 lemma dvd_mod_iff: "k dvd n \<Longrightarrow> k dvd (m mod n) \<longleftrightarrow> k dvd m"
364 by (blast intro: dvd_mod_imp_dvd dvd_mod)
366 end
368 class ring_div = comm_ring_1 + semiring_div
369 begin
371 subclass idom_divide ..
373 text \<open>Negation respects modular equivalence.\<close>
375 lemma mod_minus_eq: "(- a) mod b = (- (a mod b)) mod b"
376 proof -
377   have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
378     by (simp only: mod_div_equality)
379   also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
381   also have "\<dots> = (- (a mod b)) mod b"
382     by (rule mod_mult_self1)
383   finally show ?thesis .
384 qed
386 lemma mod_minus_cong:
387   assumes "a mod b = a' mod b"
388   shows "(- a) mod b = (- a') mod b"
389 proof -
390   have "(- (a mod b)) mod b = (- (a' mod b)) mod b"
391     unfolding assms ..
392   thus ?thesis
393     by (simp only: mod_minus_eq [symmetric])
394 qed
396 text \<open>Subtraction respects modular equivalence.\<close>
398 lemma mod_diff_left_eq:
399   "(a - b) mod c = (a mod c - b) mod c"
400   using mod_add_cong [of a c "a mod c" "- b" "- b"] by simp
402 lemma mod_diff_right_eq:
403   "(a - b) mod c = (a - b mod c) mod c"
404   using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b] by simp
406 lemma mod_diff_eq:
407   "(a - b) mod c = (a mod c - b mod c) mod c"
408   using mod_add_cong [of a c "a mod c" "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b] by simp
410 lemma mod_diff_cong:
411   assumes "a mod c = a' mod c"
412   assumes "b mod c = b' mod c"
413   shows "(a - b) mod c = (a' - b') mod c"
414   using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"] by simp
416 lemma dvd_neg_div: "y dvd x \<Longrightarrow> -x div y = - (x div y)"
417 apply (case_tac "y = 0") apply simp
418 apply (auto simp add: dvd_def)
419 apply (subgoal_tac "-(y * k) = y * - k")
420  apply (simp only:)
421  apply (erule div_mult_self1_is_id)
422 apply simp
423 done
425 lemma dvd_div_neg: "y dvd x \<Longrightarrow> x div -y = - (x div y)"
426 apply (case_tac "y = 0") apply simp
427 apply (auto simp add: dvd_def)
428 apply (subgoal_tac "y * k = -y * -k")
429  apply (erule ssubst, rule div_mult_self1_is_id)
430  apply simp
431 apply simp
432 done
434 lemma div_diff [simp]:
435   "z dvd x \<Longrightarrow> z dvd y \<Longrightarrow> (x - y) div z = x div z - y div z"
436   using div_add [of _ _ "- y"] by (simp add: dvd_neg_div)
438 lemma div_minus_minus [simp]: "(-a) div (-b) = a div b"
439   using div_mult_mult1 [of "- 1" a b]
440   unfolding neg_equal_0_iff_equal by simp
442 lemma mod_minus_minus [simp]: "(-a) mod (-b) = - (a mod b)"
443   using mod_mult_mult1 [of "- 1" a b] by simp
445 lemma div_minus_right: "a div (-b) = (-a) div b"
446   using div_minus_minus [of "-a" b] by simp
448 lemma mod_minus_right: "a mod (-b) = - ((-a) mod b)"
449   using mod_minus_minus [of "-a" b] by simp
451 lemma div_minus1_right [simp]: "a div (-1) = -a"
452   using div_minus_right [of a 1] by simp
454 lemma mod_minus1_right [simp]: "a mod (-1) = 0"
455   using mod_minus_right [of a 1] by simp
457 lemma minus_mod_self2 [simp]:
458   "(a - b) mod b = a mod b"
461 lemma minus_mod_self1 [simp]:
462   "(b - a) mod b = - a mod b"
463   using mod_add_self2 [of "- a" b] by simp
465 end
468 subsubsection \<open>Parity and division\<close>
470 class semiring_div_parity = semiring_div + comm_semiring_1_cancel + numeral +
471   assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
472   assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
473   assumes zero_not_eq_two: "0 \<noteq> 2"
474 begin
476 lemma parity_cases [case_names even odd]:
477   assumes "a mod 2 = 0 \<Longrightarrow> P"
478   assumes "a mod 2 = 1 \<Longrightarrow> P"
479   shows P
480   using assms parity by blast
482 lemma one_div_two_eq_zero [simp]:
483   "1 div 2 = 0"
484 proof (cases "2 = 0")
485   case True then show ?thesis by simp
486 next
487   case False
488   from mod_div_equality have "1 div 2 * 2 + 1 mod 2 = 1" .
489   with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
490   then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq del: mult_eq_0_iff)
491   then have "1 div 2 = 0 \<or> 2 = 0" by simp
492   with False show ?thesis by auto
493 qed
495 lemma not_mod_2_eq_0_eq_1 [simp]:
496   "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
497   by (cases a rule: parity_cases) simp_all
499 lemma not_mod_2_eq_1_eq_0 [simp]:
500   "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
501   by (cases a rule: parity_cases) simp_all
503 subclass semiring_parity
504 proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)
505   show "1 mod 2 = 1"
506     by (fact one_mod_two_eq_one)
507 next
508   fix a b
509   assume "a mod 2 = 1"
510   moreover assume "b mod 2 = 1"
511   ultimately show "(a + b) mod 2 = 0"
512     using mod_add_eq [of a b 2] by simp
513 next
514   fix a b
515   assume "(a * b) mod 2 = 0"
516   then have "(a mod 2) * (b mod 2) = 0"
517     by (cases "a mod 2 = 0") (simp_all add: mod_mult_eq [of a b 2])
518   then show "a mod 2 = 0 \<or> b mod 2 = 0"
519     by (rule divisors_zero)
520 next
521   fix a
522   assume "a mod 2 = 1"
523   then have "a = a div 2 * 2 + 1" using mod_div_equality [of a 2] by simp
524   then show "\<exists>b. a = b + 1" ..
525 qed
527 lemma even_iff_mod_2_eq_zero:
528   "even a \<longleftrightarrow> a mod 2 = 0"
529   by (fact dvd_eq_mod_eq_0)
531 lemma even_succ_div_two [simp]:
532   "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
533   by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
535 lemma odd_succ_div_two [simp]:
536   "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
539 lemma even_two_times_div_two:
540   "even a \<Longrightarrow> 2 * (a div 2) = a"
541   by (fact dvd_mult_div_cancel)
543 lemma odd_two_times_div_two_succ [simp]:
544   "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
545   using mod_div_equality2 [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
547 end
550 subsection \<open>Generic numeral division with a pragmatic type class\<close>
552 text \<open>
553   The following type class contains everything necessary to formulate
554   a division algorithm in ring structures with numerals, restricted
555   to its positive segments.  This is its primary motiviation, and it
556   could surely be formulated using a more fine-grained, more algebraic
557   and less technical class hierarchy.
558 \<close>
560 class semiring_numeral_div = semiring_div + comm_semiring_1_cancel + linordered_semidom +
561   assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
562     and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
563     and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
564     and mod_less_eq_dividend: "0 \<le> a \<Longrightarrow> a mod b \<le> a"
565     and pos_mod_bound: "0 < b \<Longrightarrow> a mod b < b"
566     and pos_mod_sign: "0 < b \<Longrightarrow> 0 \<le> a mod b"
567     and mod_mult2_eq: "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
568     and div_mult2_eq: "0 \<le> c \<Longrightarrow> a div (b * c) = a div b div c"
569   assumes discrete: "a < b \<longleftrightarrow> a + 1 \<le> b"
570   fixes divmod :: "num \<Rightarrow> num \<Rightarrow> 'a \<times> 'a"
571     and divmod_step :: "num \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<times> 'a"
572   assumes divmod_def: "divmod m n = (numeral m div numeral n, numeral m mod numeral n)"
573     and divmod_step_def: "divmod_step l qr = (let (q, r) = qr
574     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
575     else (2 * q, r))"
576     -- \<open>These are conceptually definitions but force generated code
577     to be monomorphic wrt. particular instances of this class which
578     yields a significant speedup.\<close>
580 begin
582 lemma mult_div_cancel:
583   "b * (a div b) = a - a mod b"
584 proof -
585   have "b * (a div b) + a mod b = a"
586     using mod_div_equality [of a b] by (simp add: ac_simps)
587   then have "b * (a div b) + a mod b - a mod b = a - a mod b"
588     by simp
589   then show ?thesis
590     by simp
591 qed
593 subclass semiring_div_parity
594 proof
595   fix a
596   show "a mod 2 = 0 \<or> a mod 2 = 1"
597   proof (rule ccontr)
598     assume "\<not> (a mod 2 = 0 \<or> a mod 2 = 1)"
599     then have "a mod 2 \<noteq> 0" and "a mod 2 \<noteq> 1" by simp_all
600     have "0 < 2" by simp
601     with pos_mod_bound pos_mod_sign have "0 \<le> a mod 2" "a mod 2 < 2" by simp_all
602     with \<open>a mod 2 \<noteq> 0\<close> have "0 < a mod 2" by simp
603     with discrete have "1 \<le> a mod 2" by simp
604     with \<open>a mod 2 \<noteq> 1\<close> have "1 < a mod 2" by simp
605     with discrete have "2 \<le> a mod 2" by simp
606     with \<open>a mod 2 < 2\<close> show False by simp
607   qed
608 next
609   show "1 mod 2 = 1"
610     by (rule mod_less) simp_all
611 next
612   show "0 \<noteq> 2"
613     by simp
614 qed
616 lemma divmod_digit_1:
617   assumes "0 \<le> a" "0 < b" and "b \<le> a mod (2 * b)"
618   shows "2 * (a div (2 * b)) + 1 = a div b" (is "?P")
619     and "a mod (2 * b) - b = a mod b" (is "?Q")
620 proof -
621   from assms mod_less_eq_dividend [of a "2 * b"] have "b \<le> a"
622     by (auto intro: trans)
623   with \<open>0 < b\<close> have "0 < a div b" by (auto intro: div_positive)
624   then have [simp]: "1 \<le> a div b" by (simp add: discrete)
625   with \<open>0 < b\<close> have mod_less: "a mod b < b" by (simp add: pos_mod_bound)
626   def w \<equiv> "a div b mod 2" with parity have w_exhaust: "w = 0 \<or> w = 1" by auto
627   have mod_w: "a mod (2 * b) = a mod b + b * w"
628     by (simp add: w_def mod_mult2_eq ac_simps)
629   from assms w_exhaust have "w = 1"
630     by (auto simp add: mod_w) (insert mod_less, auto)
631   with mod_w have mod: "a mod (2 * b) = a mod b + b" by simp
632   have "2 * (a div (2 * b)) = a div b - w"
633     by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps)
634   with \<open>w = 1\<close> have div: "2 * (a div (2 * b)) = a div b - 1" by simp
635   then show ?P and ?Q
637 qed
639 lemma divmod_digit_0:
640   assumes "0 < b" and "a mod (2 * b) < b"
641   shows "2 * (a div (2 * b)) = a div b" (is "?P")
642     and "a mod (2 * b) = a mod b" (is "?Q")
643 proof -
644   def w \<equiv> "a div b mod 2" with parity have w_exhaust: "w = 0 \<or> w = 1" by auto
645   have mod_w: "a mod (2 * b) = a mod b + b * w"
646     by (simp add: w_def mod_mult2_eq ac_simps)
647   moreover have "b \<le> a mod b + b"
648   proof -
649     from \<open>0 < b\<close> pos_mod_sign have "0 \<le> a mod b" by blast
650     then have "0 + b \<le> a mod b + b" by (rule add_right_mono)
651     then show ?thesis by simp
652   qed
653   moreover note assms w_exhaust
654   ultimately have "w = 0" by auto
655   with mod_w have mod: "a mod (2 * b) = a mod b" by simp
656   have "2 * (a div (2 * b)) = a div b - w"
657     by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps)
658   with \<open>w = 0\<close> have div: "2 * (a div (2 * b)) = a div b" by simp
659   then show ?P and ?Q
660     by (simp_all add: div mod)
661 qed
663 lemma fst_divmod:
664   "fst (divmod m n) = numeral m div numeral n"
667 lemma snd_divmod:
668   "snd (divmod m n) = numeral m mod numeral n"
671 text \<open>
672   This is a formulation of one step (referring to one digit position)
673   in school-method division: compare the dividend at the current
674   digit position with the remainder from previous division steps
675   and evaluate accordingly.
676 \<close>
678 lemma divmod_step_eq [simp]:
679   "divmod_step l (q, r) = (if numeral l \<le> r
680     then (2 * q + 1, r - numeral l) else (2 * q, r))"
683 text \<open>
684   This is a formulation of school-method division.
685   If the divisor is smaller than the dividend, terminate.
686   If not, shift the dividend to the right until termination
687   occurs and then reiterate single division steps in the
688   opposite direction.
689 \<close>
691 lemma divmod_divmod_step:
692   "divmod m n = (if m < n then (0, numeral m)
693     else divmod_step n (divmod m (Num.Bit0 n)))"
694 proof (cases "m < n")
695   case True then have "numeral m < numeral n" by simp
696   then show ?thesis
697     by (simp add: prod_eq_iff div_less mod_less fst_divmod snd_divmod)
698 next
699   case False
700   have "divmod m n =
701     divmod_step n (numeral m div (2 * numeral n),
702       numeral m mod (2 * numeral n))"
703   proof (cases "numeral n \<le> numeral m mod (2 * numeral n)")
704     case True
705     with divmod_step_eq
706       have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
707         (2 * (numeral m div (2 * numeral n)) + 1, numeral m mod (2 * numeral n) - numeral n)"
708         by simp
709     moreover from True divmod_digit_1 [of "numeral m" "numeral n"]
710       have "2 * (numeral m div (2 * numeral n)) + 1 = numeral m div numeral n"
711       and "numeral m mod (2 * numeral n) - numeral n = numeral m mod numeral n"
712       by simp_all
713     ultimately show ?thesis by (simp only: divmod_def)
714   next
715     case False then have *: "numeral m mod (2 * numeral n) < numeral n"
717     with divmod_step_eq
718       have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
719         (2 * (numeral m div (2 * numeral n)), numeral m mod (2 * numeral n))"
720         by auto
721     moreover from * divmod_digit_0 [of "numeral n" "numeral m"]
722       have "2 * (numeral m div (2 * numeral n)) = numeral m div numeral n"
723       and "numeral m mod (2 * numeral n) = numeral m mod numeral n"
724       by (simp_all only: zero_less_numeral)
725     ultimately show ?thesis by (simp only: divmod_def)
726   qed
727   then have "divmod m n =
728     divmod_step n (numeral m div numeral (Num.Bit0 n),
729       numeral m mod numeral (Num.Bit0 n))"
730     by (simp only: numeral.simps distrib mult_1)
731   then have "divmod m n = divmod_step n (divmod m (Num.Bit0 n))"
733   with False show ?thesis by simp
734 qed
736 text \<open>The division rewrite proper -- first, trivial results involving @{text 1}\<close>
738 lemma divmod_trivial [simp]:
739   "divmod Num.One Num.One = (numeral Num.One, 0)"
740   "divmod (Num.Bit0 m) Num.One = (numeral (Num.Bit0 m), 0)"
741   "divmod (Num.Bit1 m) Num.One = (numeral (Num.Bit1 m), 0)"
742   "divmod num.One (num.Bit0 n) = (0, Numeral1)"
743   "divmod num.One (num.Bit1 n) = (0, Numeral1)"
744   using divmod_divmod_step [of "Num.One"] by (simp_all add: divmod_def)
746 text \<open>Division by an even number is a right-shift\<close>
748 lemma divmod_cancel [simp]:
749   "divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r))" (is ?P)
750   "divmod (Num.Bit1 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r + 1))" (is ?Q)
751 proof -
752   have *: "\<And>q. numeral (Num.Bit0 q) = 2 * numeral q"
753     "\<And>q. numeral (Num.Bit1 q) = 2 * numeral q + 1"
754     by (simp_all only: numeral_mult numeral.simps distrib) simp_all
755   have "1 div 2 = 0" "1 mod 2 = 1" by (auto intro: div_less mod_less)
756   then show ?P and ?Q
757     by (simp_all add: fst_divmod snd_divmod prod_eq_iff split_def * [of m] * [of n] mod_mult_mult1
758       div_mult2_eq [of _ _ 2] mod_mult2_eq [of _ _ 2]
760 qed
762 text \<open>The really hard work\<close>
764 lemma divmod_steps [simp]:
765   "divmod (num.Bit0 m) (num.Bit1 n) =
766       (if m \<le> n then (0, numeral (num.Bit0 m))
767        else divmod_step (num.Bit1 n)
768              (divmod (num.Bit0 m)
769                (num.Bit0 (num.Bit1 n))))"
770   "divmod (num.Bit1 m) (num.Bit1 n) =
771       (if m < n then (0, numeral (num.Bit1 m))
772        else divmod_step (num.Bit1 n)
773              (divmod (num.Bit1 m)
774                (num.Bit0 (num.Bit1 n))))"
777 lemmas divmod_algorithm_code = divmod_step_eq divmod_trivial divmod_cancel divmod_steps
779 text \<open>Special case: divisibility\<close>
781 definition divides_aux :: "'a \<times> 'a \<Rightarrow> bool"
782 where
783   "divides_aux qr \<longleftrightarrow> snd qr = 0"
785 lemma divides_aux_eq [simp]:
786   "divides_aux (q, r) \<longleftrightarrow> r = 0"
789 lemma dvd_numeral_simp [simp]:
790   "numeral m dvd numeral n \<longleftrightarrow> divides_aux (divmod n m)"
791   by (simp add: divmod_def mod_eq_0_iff_dvd)
793 text \<open>Generic computation of quotient and remainder\<close>
795 lemma numeral_div_numeral [simp]:
796   "numeral k div numeral l = fst (divmod k l)"
799 lemma numeral_mod_numeral [simp]:
800   "numeral k mod numeral l = snd (divmod k l)"
803 lemma one_div_numeral [simp]:
804   "1 div numeral n = fst (divmod num.One n)"
807 lemma one_mod_numeral [simp]:
808   "1 mod numeral n = snd (divmod num.One n)"
811 end
814 subsection \<open>Division on @{typ nat}\<close>
816 context
817 begin
819 text \<open>
820   We define @{const divide} and @{const mod} on @{typ nat} by means
821   of a characteristic relation with two input arguments
822   @{term "m::nat"}, @{term "n::nat"} and two output arguments
823   @{term "q::nat"}(uotient) and @{term "r::nat"}(emainder).
824 \<close>
826 definition divmod_nat_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool" where
827   "divmod_nat_rel m n qr \<longleftrightarrow>
828     m = fst qr * n + snd qr \<and>
829       (if n = 0 then fst qr = 0 else if n > 0 then 0 \<le> snd qr \<and> snd qr < n else n < snd qr \<and> snd qr \<le> 0)"
831 text \<open>@{const divmod_nat_rel} is total:\<close>
833 qualified lemma divmod_nat_rel_ex:
834   obtains q r where "divmod_nat_rel m n (q, r)"
835 proof (cases "n = 0")
836   case True  with that show thesis
837     by (auto simp add: divmod_nat_rel_def)
838 next
839   case False
840   have "\<exists>q r. m = q * n + r \<and> r < n"
841   proof (induct m)
842     case 0 with \<open>n \<noteq> 0\<close>
843     have "(0::nat) = 0 * n + 0 \<and> 0 < n" by simp
844     then show ?case by blast
845   next
846     case (Suc m) then obtain q' r'
847       where m: "m = q' * n + r'" and n: "r' < n" by auto
848     then show ?case proof (cases "Suc r' < n")
849       case True
850       from m n have "Suc m = q' * n + Suc r'" by simp
851       with True show ?thesis by blast
852     next
853       case False then have "n \<le> Suc r'" by auto
854       moreover from n have "Suc r' \<le> n" by auto
855       ultimately have "n = Suc r'" by auto
856       with m have "Suc m = Suc q' * n + 0" by simp
857       with \<open>n \<noteq> 0\<close> show ?thesis by blast
858     qed
859   qed
860   with that show thesis
861     using \<open>n \<noteq> 0\<close> by (auto simp add: divmod_nat_rel_def)
862 qed
864 text \<open>@{const divmod_nat_rel} is injective:\<close>
866 qualified lemma divmod_nat_rel_unique:
867   assumes "divmod_nat_rel m n qr"
868     and "divmod_nat_rel m n qr'"
869   shows "qr = qr'"
870 proof (cases "n = 0")
871   case True with assms show ?thesis
872     by (cases qr, cases qr')
874 next
875   case False
876   have aux: "\<And>q r q' r'. q' * n + r' = q * n + r \<Longrightarrow> r < n \<Longrightarrow> q' \<le> (q::nat)"
877   apply (rule leI)
880   done
881   from \<open>n \<noteq> 0\<close> assms have *: "fst qr = fst qr'"
882     by (auto simp add: divmod_nat_rel_def intro: order_antisym dest: aux sym)
883   with assms have "snd qr = snd qr'"
885   with * show ?thesis by (cases qr, cases qr') simp
886 qed
888 text \<open>
889   We instantiate divisibility on the natural numbers by
890   means of @{const divmod_nat_rel}:
891 \<close>
893 qualified definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
894   "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)"
896 qualified lemma divmod_nat_rel_divmod_nat:
897   "divmod_nat_rel m n (divmod_nat m n)"
898 proof -
899   from divmod_nat_rel_ex
900     obtain qr where rel: "divmod_nat_rel m n qr" .
901   then show ?thesis
902   by (auto simp add: divmod_nat_def intro: theI elim: divmod_nat_rel_unique)
903 qed
905 qualified lemma divmod_nat_unique:
906   assumes "divmod_nat_rel m n qr"
907   shows "divmod_nat m n = qr"
908   using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
910 qualified lemma divmod_nat_zero: "divmod_nat m 0 = (0, m)"
911   by (simp add: Divides.divmod_nat_unique divmod_nat_rel_def)
913 qualified lemma divmod_nat_zero_left: "divmod_nat 0 n = (0, 0)"
914   by (simp add: Divides.divmod_nat_unique divmod_nat_rel_def)
916 qualified lemma divmod_nat_base: "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
917   by (simp add: divmod_nat_unique divmod_nat_rel_def)
919 qualified lemma divmod_nat_step:
920   assumes "0 < n" and "n \<le> m"
921   shows "divmod_nat m n = apfst Suc (divmod_nat (m - n) n)"
922 proof (rule divmod_nat_unique)
923   have "divmod_nat_rel (m - n) n (divmod_nat (m - n) n)"
924     by (fact divmod_nat_rel_divmod_nat)
925   then show "divmod_nat_rel m n (apfst Suc (divmod_nat (m - n) n))"
926     unfolding divmod_nat_rel_def using assms by auto
927 qed
929 end
931 instantiation nat :: semiring_div
932 begin
934 definition divide_nat where
935   div_nat_def: "m div n = fst (Divides.divmod_nat m n)"
937 definition mod_nat where
938   "m mod n = snd (Divides.divmod_nat m n)"
940 lemma fst_divmod_nat [simp]:
941   "fst (Divides.divmod_nat m n) = m div n"
944 lemma snd_divmod_nat [simp]:
945   "snd (Divides.divmod_nat m n) = m mod n"
948 lemma divmod_nat_div_mod:
949   "Divides.divmod_nat m n = (m div n, m mod n)"
952 lemma div_nat_unique:
953   assumes "divmod_nat_rel m n (q, r)"
954   shows "m div n = q"
955   using assms by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
957 lemma mod_nat_unique:
958   assumes "divmod_nat_rel m n (q, r)"
959   shows "m mod n = r"
960   using assms by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
962 lemma divmod_nat_rel: "divmod_nat_rel m n (m div n, m mod n)"
963   using Divides.divmod_nat_rel_divmod_nat by (simp add: divmod_nat_div_mod)
965 text \<open>The ''recursion'' equations for @{const divide} and @{const mod}\<close>
967 lemma div_less [simp]:
968   fixes m n :: nat
969   assumes "m < n"
970   shows "m div n = 0"
971   using assms Divides.divmod_nat_base by (simp add: prod_eq_iff)
973 lemma le_div_geq:
974   fixes m n :: nat
975   assumes "0 < n" and "n \<le> m"
976   shows "m div n = Suc ((m - n) div n)"
977   using assms Divides.divmod_nat_step by (simp add: prod_eq_iff)
979 lemma mod_less [simp]:
980   fixes m n :: nat
981   assumes "m < n"
982   shows "m mod n = m"
983   using assms Divides.divmod_nat_base by (simp add: prod_eq_iff)
985 lemma le_mod_geq:
986   fixes m n :: nat
987   assumes "n \<le> m"
988   shows "m mod n = (m - n) mod n"
989   using assms Divides.divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff)
991 instance proof
992   fix m n :: nat
993   show "m div n * n + m mod n = m"
994     using divmod_nat_rel [of m n] by (simp add: divmod_nat_rel_def)
995 next
996   fix m n q :: nat
997   assume "n \<noteq> 0"
998   then show "(q + m * n) div n = m + q div n"
999     by (induct m) (simp_all add: le_div_geq)
1000 next
1001   fix m n q :: nat
1002   assume "m \<noteq> 0"
1003   hence "\<And>a b. divmod_nat_rel n q (a, b) \<Longrightarrow> divmod_nat_rel (m * n) (m * q) (a, m * b)"
1004     unfolding divmod_nat_rel_def
1005     by (auto split: split_if_asm, simp_all add: algebra_simps)
1006   moreover from divmod_nat_rel have "divmod_nat_rel n q (n div q, n mod q)" .
1007   ultimately have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))" .
1008   thus "(m * n) div (m * q) = n div q" by (rule div_nat_unique)
1009 next
1010   fix n :: nat show "n div 0 = 0"
1011     by (simp add: div_nat_def Divides.divmod_nat_zero)
1012 next
1013   fix n :: nat show "0 div n = 0"
1014     by (simp add: div_nat_def Divides.divmod_nat_zero_left)
1015 qed
1017 end
1019 instantiation nat :: normalization_semidom
1020 begin
1022 definition normalize_nat
1023   where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
1025 definition unit_factor_nat
1026   where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
1028 lemma unit_factor_simps [simp]:
1029   "unit_factor 0 = (0::nat)"
1030   "unit_factor (Suc n) = 1"
1033 instance
1034   by standard (simp_all add: unit_factor_nat_def)
1036 end
1038 lemma divmod_nat_if [code]:
1039   "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
1040     let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
1041   by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
1043 text \<open>Simproc for cancelling @{const divide} and @{const mod}\<close>
1045 ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
1047 ML \<open>
1048 structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
1049 (
1050   val div_name = @{const_name divide};
1051   val mod_name = @{const_name mod};
1052   val mk_binop = HOLogic.mk_binop;
1053   val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
1054   val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
1055   fun mk_sum [] = HOLogic.zero
1056     | mk_sum [t] = t
1057     | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
1058   fun dest_sum tm =
1059     if HOLogic.is_zero tm then []
1060     else
1061       (case try HOLogic.dest_Suc tm of
1062         SOME t => HOLogic.Suc_zero :: dest_sum t
1063       | NONE =>
1064           (case try dest_plus tm of
1065             SOME (t, u) => dest_sum t @ dest_sum u
1066           | NONE => [tm]));
1068   val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
1070   val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
1072 )
1073 \<close>
1075 simproc_setup cancel_div_mod_nat ("(m::nat) + n") = \<open>K Cancel_Div_Mod_Nat.proc\<close>
1078 subsubsection \<open>Quotient\<close>
1080 lemma div_geq: "0 < n \<Longrightarrow>  \<not> m < n \<Longrightarrow> m div n = Suc ((m - n) div n)"
1081 by (simp add: le_div_geq linorder_not_less)
1083 lemma div_if: "0 < n \<Longrightarrow> m div n = (if m < n then 0 else Suc ((m - n) div n))"
1086 lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
1087 by simp
1089 lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"
1090 by simp
1092 lemma div_positive:
1093   fixes m n :: nat
1094   assumes "n > 0"
1095   assumes "m \<ge> n"
1096   shows "m div n > 0"
1097 proof -
1098   from \<open>m \<ge> n\<close> obtain q where "m = n + q"
1100   with \<open>n > 0\<close> show ?thesis by simp
1101 qed
1103 lemma div_eq_0_iff: "(a div b::nat) = 0 \<longleftrightarrow> a < b \<or> b = 0"
1104   by (metis div_less div_positive div_by_0 gr0I less_numeral_extra(3) not_less)
1106 subsubsection \<open>Remainder\<close>
1108 lemma mod_less_divisor [simp]:
1109   fixes m n :: nat
1110   assumes "n > 0"
1111   shows "m mod n < (n::nat)"
1112   using assms divmod_nat_rel [of m n] unfolding divmod_nat_rel_def by auto
1114 lemma mod_Suc_le_divisor [simp]:
1115   "m mod Suc n \<le> n"
1116   using mod_less_divisor [of "Suc n" m] by arith
1118 lemma mod_less_eq_dividend [simp]:
1119   fixes m n :: nat
1120   shows "m mod n \<le> m"
1122   from mod_div_equality have "m div n * n + m mod n = m" .
1123   then show "m div n * n + m mod n \<le> m" by auto
1124 qed
1126 lemma mod_geq: "\<not> m < (n::nat) \<Longrightarrow> m mod n = (m - n) mod n"
1127 by (simp add: le_mod_geq linorder_not_less)
1129 lemma mod_if: "m mod (n::nat) = (if m < n then m else (m - n) mod n)"
1132 lemma mod_1 [simp]: "m mod Suc 0 = 0"
1133 by (induct m) (simp_all add: mod_geq)
1135 (* a simple rearrangement of mod_div_equality: *)
1136 lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"
1137   using mod_div_equality2 [of n m] by arith
1139 lemma mod_le_divisor[simp]: "0 < n \<Longrightarrow> m mod n \<le> (n::nat)"
1140   apply (drule mod_less_divisor [where m = m])
1141   apply simp
1142   done
1144 subsubsection \<open>Quotient and Remainder\<close>
1146 lemma divmod_nat_rel_mult1_eq:
1147   "divmod_nat_rel b c (q, r)
1148    \<Longrightarrow> divmod_nat_rel (a * b) c (a * q + a * r div c, a * r mod c)"
1149 by (auto simp add: split_ifs divmod_nat_rel_def algebra_simps)
1151 lemma div_mult1_eq:
1152   "(a * b) div c = a * (b div c) + a * (b mod c) div (c::nat)"
1153 by (blast intro: divmod_nat_rel_mult1_eq [THEN div_nat_unique] divmod_nat_rel)
1156   "divmod_nat_rel a c (aq, ar) \<Longrightarrow> divmod_nat_rel b c (bq, br)
1157    \<Longrightarrow> divmod_nat_rel (a + b) c (aq + bq + (ar + br) div c, (ar + br) mod c)"
1158 by (auto simp add: split_ifs divmod_nat_rel_def algebra_simps)
1160 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
1162   "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
1163 by (blast intro: divmod_nat_rel_add1_eq [THEN div_nat_unique] divmod_nat_rel)
1165 lemma divmod_nat_rel_mult2_eq:
1166   assumes "divmod_nat_rel a b (q, r)"
1167   shows "divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)"
1168 proof -
1169   { assume "r < b" and "0 < c"
1170     then have "b * (q mod c) + r < b * c"
1171       apply (cut_tac m = q and n = c in mod_less_divisor)
1172       apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
1173       apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)
1175       done
1176     then have "r + b * (q mod c) < b * c"
1178   } with assms show ?thesis
1180 qed
1182 lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)"
1183 by (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_nat_unique])
1185 lemma mod_mult2_eq: "a mod (b * c) = b * (a div b mod c) + a mod (b::nat)"
1186 by (auto simp add: mult.commute divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN mod_nat_unique])
1188 instantiation nat :: semiring_numeral_div
1189 begin
1191 definition divmod_nat :: "num \<Rightarrow> num \<Rightarrow> nat \<times> nat"
1192 where
1193   divmod'_nat_def: "divmod_nat m n = (numeral m div numeral n, numeral m mod numeral n)"
1195 definition divmod_step_nat :: "num \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
1196 where
1197   "divmod_step_nat l qr = (let (q, r) = qr
1198     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
1199     else (2 * q, r))"
1201 instance
1202   by standard (auto intro: div_positive simp add: divmod'_nat_def divmod_step_nat_def mod_mult2_eq div_mult2_eq)
1204 end
1206 declare divmod_algorithm_code [where ?'a = nat, code]
1209 subsubsection \<open>Further Facts about Quotient and Remainder\<close>
1211 lemma div_1 [simp]:
1212   "m div Suc 0 = m"
1213   using div_by_1 [of m] by simp
1215 (* Monotonicity of div in first argument *)
1216 lemma div_le_mono [rule_format (no_asm)]:
1217     "\<forall>m::nat. m \<le> n --> (m div k) \<le> (n div k)"
1218 apply (case_tac "k=0", simp)
1219 apply (induct "n" rule: nat_less_induct, clarify)
1220 apply (case_tac "n<k")
1221 (* 1  case n<k *)
1222 apply simp
1223 (* 2  case n >= k *)
1224 apply (case_tac "m<k")
1225 (* 2.1  case m<k *)
1226 apply simp
1227 (* 2.2  case m>=k *)
1228 apply (simp add: div_geq diff_le_mono)
1229 done
1231 (* Antimonotonicity of div in second argument *)
1232 lemma div_le_mono2: "!!m::nat. [| 0<m; m\<le>n |] ==> (k div n) \<le> (k div m)"
1233 apply (subgoal_tac "0<n")
1234  prefer 2 apply simp
1235 apply (induct_tac k rule: nat_less_induct)
1236 apply (rename_tac "k")
1237 apply (case_tac "k<n", simp)
1238 apply (subgoal_tac "~ (k<m) ")
1239  prefer 2 apply simp
1241 apply (subgoal_tac "(k-n) div n \<le> (k-m) div n")
1242  prefer 2
1243  apply (blast intro: div_le_mono diff_le_mono2)
1244 apply (rule le_trans, simp)
1245 apply (simp)
1246 done
1248 lemma div_le_dividend [simp]: "m div n \<le> (m::nat)"
1249 apply (case_tac "n=0", simp)
1250 apply (subgoal_tac "m div n \<le> m div 1", simp)
1251 apply (rule div_le_mono2)
1252 apply (simp_all (no_asm_simp))
1253 done
1255 (* Similar for "less than" *)
1256 lemma div_less_dividend [simp]:
1257   "\<lbrakk>(1::nat) < n; 0 < m\<rbrakk> \<Longrightarrow> m div n < m"
1258 apply (induct m rule: nat_less_induct)
1259 apply (rename_tac "m")
1260 apply (case_tac "m<n", simp)
1261 apply (subgoal_tac "0<n")
1262  prefer 2 apply simp
1264 apply (case_tac "n<m")
1265  apply (subgoal_tac "(m-n) div n < (m-n) ")
1266   apply (rule impI less_trans_Suc)+
1267 apply assumption
1268   apply (simp_all)
1269 done
1271 text\<open>A fact for the mutilated chess board\<close>
1272 lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"
1273 apply (case_tac "n=0", simp)
1274 apply (induct "m" rule: nat_less_induct)
1275 apply (case_tac "Suc (na) <n")
1276 (* case Suc(na) < n *)
1277 apply (frule lessI [THEN less_trans], simp add: less_not_refl3)
1278 (* case n \<le> Suc(na) *)
1279 apply (simp add: linorder_not_less le_Suc_eq mod_geq)
1280 apply (auto simp add: Suc_diff_le le_mod_geq)
1281 done
1283 lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
1284 by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
1286 lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]
1288 (*Loses information, namely we also have r<d provided d is nonzero*)
1289 lemma mod_eqD:
1290   fixes m d r q :: nat
1291   assumes "m mod d = r"
1292   shows "\<exists>q. m = r + q * d"
1293 proof -
1294   from mod_div_equality obtain q where "q * d + m mod d = m" by blast
1295   with assms have "m = r + q * d" by simp
1296   then show ?thesis ..
1297 qed
1299 lemma split_div:
1300  "P(n div k :: nat) =
1301  ((k = 0 \<longrightarrow> P 0) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P i)))"
1302  (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
1303 proof
1304   assume P: ?P
1305   show ?Q
1306   proof (cases)
1307     assume "k = 0"
1308     with P show ?Q by simp
1309   next
1310     assume not0: "k \<noteq> 0"
1311     thus ?Q
1312     proof (simp, intro allI impI)
1313       fix i j
1314       assume n: "n = k*i + j" and j: "j < k"
1315       show "P i"
1316       proof (cases)
1317         assume "i = 0"
1318         with n j P show "P i" by simp
1319       next
1320         assume "i \<noteq> 0"
1321         with not0 n j P show "P i" by(simp add:ac_simps)
1322       qed
1323     qed
1324   qed
1325 next
1326   assume Q: ?Q
1327   show ?P
1328   proof (cases)
1329     assume "k = 0"
1330     with Q show ?P by simp
1331   next
1332     assume not0: "k \<noteq> 0"
1333     with Q have R: ?R by simp
1334     from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
1335     show ?P by simp
1336   qed
1337 qed
1339 lemma split_div_lemma:
1340   assumes "0 < n"
1341   shows "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> q = ((m::nat) div n)" (is "?lhs \<longleftrightarrow> ?rhs")
1342 proof
1343   assume ?rhs
1344   with mult_div_cancel have nq: "n * q = m - (m mod n)" by simp
1345   then have A: "n * q \<le> m" by simp
1346   have "n - (m mod n) > 0" using mod_less_divisor assms by auto
1347   then have "m < m + (n - (m mod n))" by simp
1348   then have "m < n + (m - (m mod n))" by simp
1349   with nq have "m < n + n * q" by simp
1350   then have B: "m < n * Suc q" by simp
1351   from A B show ?lhs ..
1352 next
1353   assume P: ?lhs
1354   then have "divmod_nat_rel m n (q, m - n * q)"
1355     unfolding divmod_nat_rel_def by (auto simp add: ac_simps)
1356   then have "m div n = q"
1357     by (rule div_nat_unique)
1358   then show ?rhs by simp
1359 qed
1361 theorem split_div':
1362   "P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or>
1363    (\<exists>q. (n * q \<le> m \<and> m < n * (Suc q)) \<and> P q))"
1364   apply (cases "0 < n")
1365   apply (simp only: add: split_div_lemma)
1366   apply simp_all
1367   done
1369 lemma split_mod:
1370  "P(n mod k :: nat) =
1371  ((k = 0 \<longrightarrow> P n) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P j)))"
1372  (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
1373 proof
1374   assume P: ?P
1375   show ?Q
1376   proof (cases)
1377     assume "k = 0"
1378     with P show ?Q by simp
1379   next
1380     assume not0: "k \<noteq> 0"
1381     thus ?Q
1382     proof (simp, intro allI impI)
1383       fix i j
1384       assume "n = k*i + j" "j < k"
1385       thus "P j" using not0 P by (simp add: ac_simps)
1386     qed
1387   qed
1388 next
1389   assume Q: ?Q
1390   show ?P
1391   proof (cases)
1392     assume "k = 0"
1393     with Q show ?P by simp
1394   next
1395     assume not0: "k \<noteq> 0"
1396     with Q have R: ?R by simp
1397     from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
1398     show ?P by simp
1399   qed
1400 qed
1402 theorem mod_div_equality' [nitpick_unfold]: "(m::nat) mod n = m - (m div n) * n"
1403   using mod_div_equality [of m n] by arith
1405 lemma div_mod_equality': "(m::nat) div n * n = m - m mod n"
1406   using mod_div_equality [of m n] by arith
1407 (* FIXME: very similar to mult_div_cancel *)
1409 lemma div_eq_dividend_iff: "a \<noteq> 0 \<Longrightarrow> (a :: nat) div b = a \<longleftrightarrow> b = 1"
1410   apply rule
1411   apply (cases "b = 0")
1412   apply simp_all
1413   apply (metis (full_types) One_nat_def Suc_lessI div_less_dividend less_not_refl3)
1414   done
1417 subsubsection \<open>An ``induction'' law for modulus arithmetic.\<close>
1419 lemma mod_induct_0:
1420   assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
1421   and base: "P i" and i: "i<p"
1422   shows "P 0"
1423 proof (rule ccontr)
1424   assume contra: "\<not>(P 0)"
1425   from i have p: "0<p" by simp
1426   have "\<forall>k. 0<k \<longrightarrow> \<not> P (p-k)" (is "\<forall>k. ?A k")
1427   proof
1428     fix k
1429     show "?A k"
1430     proof (induct k)
1431       show "?A 0" by simp  -- "by contradiction"
1432     next
1433       fix n
1434       assume ih: "?A n"
1435       show "?A (Suc n)"
1436       proof (clarsimp)
1437         assume y: "P (p - Suc n)"
1438         have n: "Suc n < p"
1439         proof (rule ccontr)
1440           assume "\<not>(Suc n < p)"
1441           hence "p - Suc n = 0"
1442             by simp
1443           with y contra show "False"
1444             by simp
1445         qed
1446         hence n2: "Suc (p - Suc n) = p-n" by arith
1447         from p have "p - Suc n < p" by arith
1448         with y step have z: "P ((Suc (p - Suc n)) mod p)"
1449           by blast
1450         show "False"
1451         proof (cases "n=0")
1452           case True
1453           with z n2 contra show ?thesis by simp
1454         next
1455           case False
1456           with p have "p-n < p" by arith
1457           with z n2 False ih show ?thesis by simp
1458         qed
1459       qed
1460     qed
1461   qed
1462   moreover
1463   from i obtain k where "0<k \<and> i+k=p"
1465   hence "0<k \<and> i=p-k" by auto
1466   moreover
1467   note base
1468   ultimately
1469   show "False" by blast
1470 qed
1472 lemma mod_induct:
1473   assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
1474   and base: "P i" and i: "i<p" and j: "j<p"
1475   shows "P j"
1476 proof -
1477   have "\<forall>j<p. P j"
1478   proof
1479     fix j
1480     show "j<p \<longrightarrow> P j" (is "?A j")
1481     proof (induct j)
1482       from step base i show "?A 0"
1483         by (auto elim: mod_induct_0)
1484     next
1485       fix k
1486       assume ih: "?A k"
1487       show "?A (Suc k)"
1488       proof
1489         assume suc: "Suc k < p"
1490         hence k: "k<p" by simp
1491         with ih have "P k" ..
1492         with step k have "P (Suc k mod p)"
1493           by blast
1494         moreover
1495         from suc have "Suc k mod p = Suc k"
1496           by simp
1497         ultimately
1498         show "P (Suc k)" by simp
1499       qed
1500     qed
1501   qed
1502   with j show ?thesis by blast
1503 qed
1505 lemma div2_Suc_Suc [simp]: "Suc (Suc m) div 2 = Suc (m div 2)"
1506   by (simp add: numeral_2_eq_2 le_div_geq)
1508 lemma mod2_Suc_Suc [simp]: "Suc (Suc m) mod 2 = m mod 2"
1509   by (simp add: numeral_2_eq_2 le_mod_geq)
1511 lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
1512 by (simp add: mult_2 [symmetric])
1514 lemma mod2_gr_0 [simp]: "0 < (m::nat) mod 2 \<longleftrightarrow> m mod 2 = 1"
1515 proof -
1516   { fix n :: nat have  "(n::nat) < 2 \<Longrightarrow> n = 0 \<or> n = 1" by (cases n) simp_all }
1517   moreover have "m mod 2 < 2" by simp
1518   ultimately have "m mod 2 = 0 \<or> m mod 2 = 1" .
1519   then show ?thesis by auto
1520 qed
1522 text\<open>These lemmas collapse some needless occurrences of Suc:
1523     at least three Sucs, since two and fewer are rewritten back to Suc again!
1524     We already have some rules to simplify operands smaller than 3.\<close>
1526 lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
1529 lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
1532 lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
1535 lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
1538 lemmas Suc_div_eq_add3_div_numeral [simp] = Suc_div_eq_add3_div [of _ "numeral v"] for v
1539 lemmas Suc_mod_eq_add3_mod_numeral [simp] = Suc_mod_eq_add3_mod [of _ "numeral v"] for v
1541 lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1"
1542 apply (induct "m")
1544 done
1546 declare Suc_times_mod_eq [of "numeral w", simp] for w
1548 lemma mod_greater_zero_iff_not_dvd:
1549   fixes m n :: nat
1550   shows "m mod n > 0 \<longleftrightarrow> \<not> n dvd m"
1553 lemma Suc_div_le_mono [simp]: "n div k \<le> (Suc n) div k"
1556 lemma Suc_n_div_2_gt_zero [simp]: "(0::nat) < n ==> 0 < (n + 1) div 2"
1557 by (cases n) simp_all
1559 lemma div_2_gt_zero [simp]: assumes A: "(1::nat) < n" shows "0 < n div 2"
1560 proof -
1561   from A have B: "0 < n - 1" and C: "n - 1 + 1 = n" by simp_all
1562   from Suc_n_div_2_gt_zero [OF B] C show ?thesis by simp
1563 qed
1565 lemma mod_mult_self4 [simp]: "Suc (k*n + m) mod n = Suc m mod n"
1566 proof -
1567   have "Suc (k * n + m) mod n = (k * n + Suc m) mod n" by simp
1568   also have "... = Suc m mod n" by (rule mod_mult_self3)
1569   finally show ?thesis .
1570 qed
1572 lemma mod_Suc_eq_Suc_mod: "Suc m mod n = Suc (m mod n) mod n"
1573 apply (subst mod_Suc [of m])
1574 apply (subst mod_Suc [of "m mod n"], simp)
1575 done
1577 lemma mod_2_not_eq_zero_eq_one_nat:
1578   fixes n :: nat
1579   shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
1580   by (fact not_mod_2_eq_0_eq_1)
1582 lemma even_Suc_div_two [simp]:
1583   "even n \<Longrightarrow> Suc n div 2 = n div 2"
1584   using even_succ_div_two [of n] by simp
1586 lemma odd_Suc_div_two [simp]:
1587   "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
1588   using odd_succ_div_two [of n] by simp
1590 lemma odd_two_times_div_two_nat [simp]:
1591   assumes "odd n"
1592   shows "2 * (n div 2) = n - (1 :: nat)"
1593 proof -
1594   from assms have "2 * (n div 2) + 1 = n"
1595     by (rule odd_two_times_div_two_succ)
1596   then have "Suc (2 * (n div 2)) - 1 = n - 1"
1597     by simp
1598   then show ?thesis
1599     by simp
1600 qed
1602 lemma parity_induct [case_names zero even odd]:
1603   assumes zero: "P 0"
1604   assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
1605   assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
1606   shows "P n"
1607 proof (induct n rule: less_induct)
1608   case (less n)
1609   show "P n"
1610   proof (cases "n = 0")
1611     case True with zero show ?thesis by simp
1612   next
1613     case False
1614     with less have hyp: "P (n div 2)" by simp
1615     show ?thesis
1616     proof (cases "even n")
1617       case True
1618       with hyp even [of "n div 2"] show ?thesis
1619         by simp
1620     next
1621       case False
1622       with hyp odd [of "n div 2"] show ?thesis
1623         by simp
1624     qed
1625   qed
1626 qed
1628 lemma Suc_0_div_numeral [simp]:
1629   fixes k l :: num
1630   shows "Suc 0 div numeral k = fst (divmod Num.One k)"
1633 lemma Suc_0_mod_numeral [simp]:
1634   fixes k l :: num
1635   shows "Suc 0 mod numeral k = snd (divmod Num.One k)"
1639 subsection \<open>Division on @{typ int}\<close>
1641 definition divmod_int_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" -- \<open>definition of quotient and remainder\<close>
1642   where "divmod_int_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
1643     (if 0 < b then 0 \<le> r \<and> r < b else if b < 0 then b < r \<and> r \<le> 0 else q = 0))"
1645 lemma unique_quotient_lemma:
1646   "b * q' + r' \<le> b * q + r \<Longrightarrow> 0 \<le> r' \<Longrightarrow> r' < b \<Longrightarrow> r < b \<Longrightarrow> q' \<le> (q::int)"
1647 apply (subgoal_tac "r' + b * (q'-q) \<le> r")
1648  prefer 2 apply (simp add: right_diff_distrib)
1649 apply (subgoal_tac "0 < b * (1 + q - q') ")
1650 apply (erule_tac [2] order_le_less_trans)
1651  prefer 2 apply (simp add: right_diff_distrib distrib_left)
1652 apply (subgoal_tac "b * q' < b * (1 + q) ")
1653  prefer 2 apply (simp add: right_diff_distrib distrib_left)
1655 done
1657 lemma unique_quotient_lemma_neg:
1658   "b * q' + r' \<le> b*q + r \<Longrightarrow> r \<le> 0 \<Longrightarrow> b < r \<Longrightarrow> b < r' \<Longrightarrow> q \<le> (q'::int)"
1659   by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma) auto
1661 lemma unique_quotient:
1662   "divmod_int_rel a b (q, r) \<Longrightarrow> divmod_int_rel a b (q', r') \<Longrightarrow> q = q'"
1663 apply (simp add: divmod_int_rel_def linorder_neq_iff split: split_if_asm)
1664 apply (blast intro: order_antisym
1665              dest: order_eq_refl [THEN unique_quotient_lemma]
1666              order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
1667 done
1669 lemma unique_remainder:
1670   "divmod_int_rel a b (q, r) \<Longrightarrow> divmod_int_rel a b (q', r') \<Longrightarrow> r = r'"
1671 apply (subgoal_tac "q = q'")
1673 apply (blast intro: unique_quotient)
1674 done
1676 instantiation int :: Divides.div
1677 begin
1679 definition divide_int
1680   where "k div l = (if l = 0 \<or> k = 0 then 0
1681     else if k > 0 \<and> l > 0 \<or> k < 0 \<and> l < 0
1682       then int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
1683       else
1684         if l dvd k then - int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
1685         else - int (Suc (nat \<bar>k\<bar> div nat \<bar>l\<bar>)))"
1687 definition mod_int
1688   where "k mod l = (if l = 0 then k else if l dvd k then 0
1689     else if k > 0 \<and> l > 0 \<or> k < 0 \<and> l < 0
1690       then sgn l * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)
1691       else sgn l * (\<bar>l\<bar> - int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)))"
1693 instance ..
1695 end
1697 lemma divmod_int_rel:
1698   "divmod_int_rel k l (k div l, k mod l)"
1699   apply (cases k rule: int_cases3)
1700   apply (simp add: mod_greater_zero_iff_not_dvd not_le divmod_int_rel_def divide_int_def mod_int_def algebra_simps int_dvd_iff of_nat_mult [symmetric])
1701   apply (cases l rule: int_cases3)
1702   apply (simp add: mod_greater_zero_iff_not_dvd not_le divmod_int_rel_def divide_int_def mod_int_def algebra_simps int_dvd_iff of_nat_mult [symmetric])
1703   apply (simp add: mod_greater_zero_iff_not_dvd not_le divmod_int_rel_def divide_int_def mod_int_def algebra_simps int_dvd_iff of_nat_mult [symmetric])
1705   apply (simp add: mod_greater_zero_iff_not_dvd not_le divmod_int_rel_def divide_int_def mod_int_def algebra_simps int_dvd_iff of_nat_mult [symmetric])
1707   apply (cases l rule: int_cases3)
1708   apply (simp_all add: mod_greater_zero_iff_not_dvd not_le divmod_int_rel_def divide_int_def mod_int_def algebra_simps int_dvd_iff of_nat_mult [symmetric])
1710   done
1712 instantiation int :: ring_div
1713 begin
1715 subsubsection \<open>Uniqueness and Monotonicity of Quotients and Remainders\<close>
1717 lemma divmod_int_unique:
1718   assumes "divmod_int_rel k l (q, r)"
1719   shows div_int_unique: "k div l = q" and mod_int_unique: "k mod l = r"
1720   using assms divmod_int_rel [of k l]
1721   using unique_quotient [of k l] unique_remainder [of k l]
1722   by auto
1724 instance
1725 proof
1726   fix a b :: int
1727   show "a div b * b + a mod b = a"
1728     using divmod_int_rel [of a b]
1729     unfolding divmod_int_rel_def by (simp add: mult.commute)
1730 next
1731   fix a b c :: int
1732   assume "b \<noteq> 0"
1733   hence "divmod_int_rel (a + c * b) b (c + a div b, a mod b)"
1734     using divmod_int_rel [of a b]
1735     unfolding divmod_int_rel_def by (auto simp: algebra_simps)
1736   thus "(a + c * b) div b = c + a div b"
1737     by (rule div_int_unique)
1738 next
1739   fix a b c :: int
1740   assume "c \<noteq> 0"
1741   hence "\<And>q r. divmod_int_rel a b (q, r)
1742     \<Longrightarrow> divmod_int_rel (c * a) (c * b) (q, c * r)"
1743     unfolding divmod_int_rel_def
1744     by - (rule linorder_cases [of 0 b], auto simp: algebra_simps
1745       mult_less_0_iff zero_less_mult_iff mult_strict_right_mono
1746       mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff)
1747   hence "divmod_int_rel (c * a) (c * b) (a div b, c * (a mod b))"
1748     using divmod_int_rel [of a b] .
1749   thus "(c * a) div (c * b) = a div b"
1750     by (rule div_int_unique)
1751 next
1752   fix a :: int show "a div 0 = 0"
1753     by (rule div_int_unique, simp add: divmod_int_rel_def)
1754 next
1755   fix a :: int show "0 div a = 0"
1756     by (rule div_int_unique, auto simp add: divmod_int_rel_def)
1757 qed
1759 end
1761 lemma is_unit_int:
1762   "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
1763   by auto
1765 instantiation int :: normalization_semidom
1766 begin
1768 definition normalize_int
1769   where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
1771 definition unit_factor_int
1772   where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
1774 instance
1775 proof
1776   fix k :: int
1777   assume "k \<noteq> 0"
1778   then have "\<bar>sgn k\<bar> = 1"
1779     by (cases "0::int" k rule: linorder_cases) simp_all
1780   then show "is_unit (unit_factor k)"
1781     by simp
1782 qed (simp_all add: sgn_times mult_sgn_abs)
1784 end
1786 text\<open>Basic laws about division and remainder\<close>
1788 lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
1789   by (fact mod_div_equality2 [symmetric])
1791 lemma zdiv_int: "int (a div b) = int a div int b"
1794 lemma zmod_int: "int (a mod b) = int a mod int b"
1795   by (simp add: mod_int_def int_dvd_iff)
1797 text \<open>Tool setup\<close>
1799 ML \<open>
1800 structure Cancel_Div_Mod_Int = Cancel_Div_Mod
1801 (
1802   val div_name = @{const_name Rings.divide};
1803   val mod_name = @{const_name mod};
1804   val mk_binop = HOLogic.mk_binop;
1805   val mk_sum = Arith_Data.mk_sum HOLogic.intT;
1806   val dest_sum = Arith_Data.dest_sum;
1808   val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
1810   val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
1812 )
1813 \<close>
1815 simproc_setup cancel_div_mod_int ("(k::int) + l") = \<open>K Cancel_Div_Mod_Int.proc\<close>
1817 lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"
1818   using divmod_int_rel [of a b]
1819   by (auto simp add: divmod_int_rel_def prod_eq_iff)
1821 lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1]
1822    and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2]
1824 lemma neg_mod_conj: "b < (0::int) \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b"
1825   using divmod_int_rel [of a b]
1826   by (auto simp add: divmod_int_rel_def prod_eq_iff)
1828 lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1]
1829    and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2]
1832 subsubsection \<open>General Properties of div and mod\<close>
1834 lemma div_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a div b = 0"
1835 apply (rule div_int_unique)
1836 apply (auto simp add: divmod_int_rel_def)
1837 done
1839 lemma div_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a div b = 0"
1840 apply (rule div_int_unique)
1841 apply (auto simp add: divmod_int_rel_def)
1842 done
1844 lemma div_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a div b = -1"
1845 apply (rule div_int_unique)
1846 apply (auto simp add: divmod_int_rel_def)
1847 done
1849 (*There is no div_neg_pos_trivial because  0 div b = 0 would supersede it*)
1851 lemma mod_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a mod b = a"
1852 apply (rule_tac q = 0 in mod_int_unique)
1853 apply (auto simp add: divmod_int_rel_def)
1854 done
1856 lemma mod_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a mod b = a"
1857 apply (rule_tac q = 0 in mod_int_unique)
1858 apply (auto simp add: divmod_int_rel_def)
1859 done
1861 lemma mod_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a mod b = a+b"
1862 apply (rule_tac q = "-1" in mod_int_unique)
1863 apply (auto simp add: divmod_int_rel_def)
1864 done
1866 text\<open>There is no @{text mod_neg_pos_trivial}.\<close>
1869 subsubsection \<open>Laws for div and mod with Unary Minus\<close>
1871 lemma zminus1_lemma:
1872      "divmod_int_rel a b (q, r) ==> b \<noteq> 0
1873       ==> divmod_int_rel (-a) b (if r=0 then -q else -q - 1,
1874                           if r=0 then 0 else b-r)"
1875 by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_diff_distrib)
1878 lemma zdiv_zminus1_eq_if:
1879      "b \<noteq> (0::int)
1880       ==> (-a) div b =
1881           (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
1882 by (blast intro: divmod_int_rel [THEN zminus1_lemma, THEN div_int_unique])
1884 lemma zmod_zminus1_eq_if:
1885      "(-a::int) mod b = (if a mod b = 0 then 0 else  b - (a mod b))"
1886 apply (case_tac "b = 0", simp)
1887 apply (blast intro: divmod_int_rel [THEN zminus1_lemma, THEN mod_int_unique])
1888 done
1890 lemma zmod_zminus1_not_zero:
1891   fixes k l :: int
1892   shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
1893   unfolding zmod_zminus1_eq_if by auto
1895 lemma zdiv_zminus2_eq_if:
1896      "b \<noteq> (0::int)
1897       ==> a div (-b) =
1898           (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
1899 by (simp add: zdiv_zminus1_eq_if div_minus_right)
1901 lemma zmod_zminus2_eq_if:
1902      "a mod (-b::int) = (if a mod b = 0 then 0 else  (a mod b) - b)"
1903 by (simp add: zmod_zminus1_eq_if mod_minus_right)
1905 lemma zmod_zminus2_not_zero:
1906   fixes k l :: int
1907   shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
1908   unfolding zmod_zminus2_eq_if by auto
1911 subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
1913 lemma zdiv_mono1: "[| a \<le> a';  0 < (b::int) |] ==> a div b \<le> a' div b"
1914 apply (cut_tac a = a and b = b in zmod_zdiv_equality)
1915 apply (cut_tac a = a' and b = b in zmod_zdiv_equality)
1916 apply (rule unique_quotient_lemma)
1917 apply (erule subst)
1918 apply (erule subst, simp_all)
1919 done
1921 lemma zdiv_mono1_neg: "[| a \<le> a';  (b::int) < 0 |] ==> a' div b \<le> a div b"
1922 apply (cut_tac a = a and b = b in zmod_zdiv_equality)
1923 apply (cut_tac a = a' and b = b in zmod_zdiv_equality)
1924 apply (rule unique_quotient_lemma_neg)
1925 apply (erule subst)
1926 apply (erule subst, simp_all)
1927 done
1930 subsubsection \<open>Monotonicity in the Second Argument (Divisor)\<close>
1932 lemma q_pos_lemma:
1933      "[| 0 \<le> b'*q' + r'; r' < b';  0 < b' |] ==> 0 \<le> (q'::int)"
1934 apply (subgoal_tac "0 < b'* (q' + 1) ")
1937 done
1939 lemma zdiv_mono2_lemma:
1940      "[| b*q + r = b'*q' + r';  0 \<le> b'*q' + r';
1941          r' < b';  0 \<le> r;  0 < b';  b' \<le> b |]
1942       ==> q \<le> (q'::int)"
1943 apply (frule q_pos_lemma, assumption+)
1944 apply (subgoal_tac "b*q < b* (q' + 1) ")
1946 apply (subgoal_tac "b*q = r' - r + b'*q'")
1947  prefer 2 apply simp
1948 apply (simp (no_asm_simp) add: distrib_left)
1950 apply (rule mult_right_mono, auto)
1951 done
1953 lemma zdiv_mono2:
1954      "[| (0::int) \<le> a;  0 < b';  b' \<le> b |] ==> a div b \<le> a div b'"
1955 apply (subgoal_tac "b \<noteq> 0")
1956  prefer 2 apply arith
1957 apply (cut_tac a = a and b = b in zmod_zdiv_equality)
1958 apply (cut_tac a = a and b = b' in zmod_zdiv_equality)
1959 apply (rule zdiv_mono2_lemma)
1960 apply (erule subst)
1961 apply (erule subst, simp_all)
1962 done
1964 lemma q_neg_lemma:
1965      "[| b'*q' + r' < 0;  0 \<le> r';  0 < b' |] ==> q' \<le> (0::int)"
1966 apply (subgoal_tac "b'*q' < 0")
1967  apply (simp add: mult_less_0_iff, arith)
1968 done
1970 lemma zdiv_mono2_neg_lemma:
1971      "[| b*q + r = b'*q' + r';  b'*q' + r' < 0;
1972          r < b;  0 \<le> r';  0 < b';  b' \<le> b |]
1973       ==> q' \<le> (q::int)"
1974 apply (frule q_neg_lemma, assumption+)
1975 apply (subgoal_tac "b*q' < b* (q + 1) ")
1978 apply (subgoal_tac "b*q' \<le> b'*q'")
1979  prefer 2 apply (simp add: mult_right_mono_neg, arith)
1980 done
1982 lemma zdiv_mono2_neg:
1983      "[| a < (0::int);  0 < b';  b' \<le> b |] ==> a div b' \<le> a div b"
1984 apply (cut_tac a = a and b = b in zmod_zdiv_equality)
1985 apply (cut_tac a = a and b = b' in zmod_zdiv_equality)
1986 apply (rule zdiv_mono2_neg_lemma)
1987 apply (erule subst)
1988 apply (erule subst, simp_all)
1989 done
1992 subsubsection \<open>More Algebraic Laws for div and mod\<close>
1994 text\<open>proving (a*b) div c = a * (b div c) + a * (b mod c)\<close>
1996 lemma zmult1_lemma:
1997      "[| divmod_int_rel b c (q, r) |]
1998       ==> divmod_int_rel (a * b) c (a*q + a*r div c, a*r mod c)"
1999 by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left ac_simps)
2001 lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
2002 apply (case_tac "c = 0", simp)
2003 apply (blast intro: divmod_int_rel [THEN zmult1_lemma, THEN div_int_unique])
2004 done
2006 text\<open>proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c)\<close>
2009      "[| divmod_int_rel a c (aq, ar);  divmod_int_rel b c (bq, br) |]
2010       ==> divmod_int_rel (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
2011 by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left)
2013 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
2015      "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
2016 apply (case_tac "c = 0", simp)
2017 apply (blast intro: zadd1_lemma [OF divmod_int_rel divmod_int_rel] div_int_unique)
2018 done
2020 lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
2021 by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
2023 (* REVISIT: should this be generalized to all semiring_div types? *)
2024 lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
2026 lemma zmod_zdiv_equality' [nitpick_unfold]:
2027   "(m::int) mod n = m - (m div n) * n"
2028   using mod_div_equality [of m n] by arith
2031 subsubsection \<open>Proving  @{term "a div (b * c) = (a div b) div c"}\<close>
2033 (*The condition c>0 seems necessary.  Consider that 7 div ~6 = ~2 but
2034   7 div 2 div ~3 = 3 div ~3 = ~1.  The subcase (a div b) mod c = 0 seems
2035   to cause particular problems.*)
2037 text\<open>first, four lemmas to bound the remainder for the cases b<0 and b>0\<close>
2039 lemma zmult2_lemma_aux1: "[| (0::int) < c;  b < r;  r \<le> 0 |] ==> b * c < b * (q mod c) + r"
2040 apply (subgoal_tac "b * (c - q mod c) < r * 1")
2042 apply (rule order_le_less_trans)
2043  apply (erule_tac [2] mult_strict_right_mono)
2044  apply (rule mult_left_mono_neg)
2046  apply (simp)
2047 apply (simp)
2048 done
2050 lemma zmult2_lemma_aux2:
2051      "[| (0::int) < c;   b < r;  r \<le> 0 |] ==> b * (q mod c) + r \<le> 0"
2052 apply (subgoal_tac "b * (q mod c) \<le> 0")
2053  apply arith
2055 done
2057 lemma zmult2_lemma_aux3: "[| (0::int) < c;  0 \<le> r;  r < b |] ==> 0 \<le> b * (q mod c) + r"
2058 apply (subgoal_tac "0 \<le> b * (q mod c) ")
2059 apply arith
2061 done
2063 lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 \<le> r; r < b |] ==> b * (q mod c) + r < b * c"
2064 apply (subgoal_tac "r * 1 < b * (c - q mod c) ")
2066 apply (rule order_less_le_trans)
2067  apply (erule mult_strict_right_mono)
2068  apply (rule_tac [2] mult_left_mono)
2069   apply simp
2071 apply simp
2072 done
2074 lemma zmult2_lemma: "[| divmod_int_rel a b (q, r); 0 < c |]
2075       ==> divmod_int_rel a (b * c) (q div c, b*(q mod c) + r)"
2076 by (auto simp add: mult.assoc divmod_int_rel_def linorder_neq_iff
2077                    zero_less_mult_iff distrib_left [symmetric]
2078                    zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: split_if_asm)
2080 lemma zdiv_zmult2_eq:
2081   fixes a b c :: int
2082   shows "0 \<le> c \<Longrightarrow> a div (b * c) = (a div b) div c"
2083 apply (case_tac "b = 0", simp)
2084 apply (force simp add: le_less divmod_int_rel [THEN zmult2_lemma, THEN div_int_unique])
2085 done
2087 lemma zmod_zmult2_eq:
2088   fixes a b c :: int
2089   shows "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
2090 apply (case_tac "b = 0", simp)
2091 apply (force simp add: le_less divmod_int_rel [THEN zmult2_lemma, THEN mod_int_unique])
2092 done
2094 lemma div_pos_geq:
2095   fixes k l :: int
2096   assumes "0 < l" and "l \<le> k"
2097   shows "k div l = (k - l) div l + 1"
2098 proof -
2099   have "k = (k - l) + l" by simp
2100   then obtain j where k: "k = j + l" ..
2101   with assms show ?thesis by simp
2102 qed
2104 lemma mod_pos_geq:
2105   fixes k l :: int
2106   assumes "0 < l" and "l \<le> k"
2107   shows "k mod l = (k - l) mod l"
2108 proof -
2109   have "k = (k - l) + l" by simp
2110   then obtain j where k: "k = j + l" ..
2111   with assms show ?thesis by simp
2112 qed
2115 subsubsection \<open>Splitting Rules for div and mod\<close>
2117 text\<open>The proofs of the two lemmas below are essentially identical\<close>
2119 lemma split_pos_lemma:
2120  "0<k ==>
2121     P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)"
2122 apply (rule iffI, clarify)
2123  apply (erule_tac P="P x y" for x y in rev_mp)
2126  apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)
2127 txt\<open>converse direction\<close>
2128 apply (drule_tac x = "n div k" in spec)
2129 apply (drule_tac x = "n mod k" in spec, simp)
2130 done
2132 lemma split_neg_lemma:
2133  "k<0 ==>
2134     P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)"
2135 apply (rule iffI, clarify)
2136  apply (erule_tac P="P x y" for x y in rev_mp)
2139  apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)
2140 txt\<open>converse direction\<close>
2141 apply (drule_tac x = "n div k" in spec)
2142 apply (drule_tac x = "n mod k" in spec, simp)
2143 done
2145 lemma split_zdiv:
2146  "P(n div k :: int) =
2147   ((k = 0 --> P 0) &
2148    (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i)) &
2149    (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i)))"
2150 apply (case_tac "k=0", simp)
2151 apply (simp only: linorder_neq_iff)
2152 apply (erule disjE)
2153  apply (simp_all add: split_pos_lemma [of concl: "%x y. P x"]
2154                       split_neg_lemma [of concl: "%x y. P x"])
2155 done
2157 lemma split_zmod:
2158  "P(n mod k :: int) =
2159   ((k = 0 --> P n) &
2160    (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P j)) &
2161    (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P j)))"
2162 apply (case_tac "k=0", simp)
2163 apply (simp only: linorder_neq_iff)
2164 apply (erule disjE)
2165  apply (simp_all add: split_pos_lemma [of concl: "%x y. P y"]
2166                       split_neg_lemma [of concl: "%x y. P y"])
2167 done
2169 text \<open>Enable (lin)arith to deal with @{const divide} and @{const mod}
2170   when these are applied to some constant that is of the form
2171   @{term "numeral k"}:\<close>
2172 declare split_zdiv [of _ _ "numeral k", arith_split] for k
2173 declare split_zmod [of _ _ "numeral k", arith_split] for k
2176 subsubsection \<open>Computing @{text "div"} and @{text "mod"} with shifting\<close>
2178 lemma pos_divmod_int_rel_mult_2:
2179   assumes "0 \<le> b"
2180   assumes "divmod_int_rel a b (q, r)"
2181   shows "divmod_int_rel (1 + 2*a) (2*b) (q, 1 + 2*r)"
2182   using assms unfolding divmod_int_rel_def by auto
2184 declaration \<open>K (Lin_Arith.add_simps @{thms uminus_numeral_One})\<close>
2186 lemma neg_divmod_int_rel_mult_2:
2187   assumes "b \<le> 0"
2188   assumes "divmod_int_rel (a + 1) b (q, r)"
2189   shows "divmod_int_rel (1 + 2*a) (2*b) (q, 2*r - 1)"
2190   using assms unfolding divmod_int_rel_def by auto
2192 text\<open>computing div by shifting\<close>
2194 lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a"
2195   using pos_divmod_int_rel_mult_2 [OF _ divmod_int_rel]
2196   by (rule div_int_unique)
2198 lemma neg_zdiv_mult_2:
2199   assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a"
2200   using neg_divmod_int_rel_mult_2 [OF A divmod_int_rel]
2201   by (rule div_int_unique)
2203 (* FIXME: add rules for negative numerals *)
2204 lemma zdiv_numeral_Bit0 [simp]:
2205   "numeral (Num.Bit0 v) div numeral (Num.Bit0 w) =
2206     numeral v div (numeral w :: int)"
2207   unfolding numeral.simps unfolding mult_2 [symmetric]
2208   by (rule div_mult_mult1, simp)
2210 lemma zdiv_numeral_Bit1 [simp]:
2211   "numeral (Num.Bit1 v) div numeral (Num.Bit0 w) =
2212     (numeral v div (numeral w :: int))"
2213   unfolding numeral.simps
2214   unfolding mult_2 [symmetric] add.commute [of _ 1]
2215   by (rule pos_zdiv_mult_2, simp)
2217 lemma pos_zmod_mult_2:
2218   fixes a b :: int
2219   assumes "0 \<le> a"
2220   shows "(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)"
2221   using pos_divmod_int_rel_mult_2 [OF assms divmod_int_rel]
2222   by (rule mod_int_unique)
2224 lemma neg_zmod_mult_2:
2225   fixes a b :: int
2226   assumes "a \<le> 0"
2227   shows "(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1"
2228   using neg_divmod_int_rel_mult_2 [OF assms divmod_int_rel]
2229   by (rule mod_int_unique)
2231 (* FIXME: add rules for negative numerals *)
2232 lemma zmod_numeral_Bit0 [simp]:
2233   "numeral (Num.Bit0 v) mod numeral (Num.Bit0 w) =
2234     (2::int) * (numeral v mod numeral w)"
2235   unfolding numeral_Bit0 [of v] numeral_Bit0 [of w]
2236   unfolding mult_2 [symmetric] by (rule mod_mult_mult1)
2238 lemma zmod_numeral_Bit1 [simp]:
2239   "numeral (Num.Bit1 v) mod numeral (Num.Bit0 w) =
2240     2 * (numeral v mod numeral w) + (1::int)"
2241   unfolding numeral_Bit1 [of v] numeral_Bit0 [of w]
2242   unfolding mult_2 [symmetric] add.commute [of _ 1]
2243   by (rule pos_zmod_mult_2, simp)
2245 lemma zdiv_eq_0_iff:
2246  "(i::int) div k = 0 \<longleftrightarrow> k=0 \<or> 0\<le>i \<and> i<k \<or> i\<le>0 \<and> k<i" (is "?L = ?R")
2247 proof
2248   assume ?L
2249   have "?L \<longrightarrow> ?R" by (rule split_zdiv[THEN iffD2]) simp
2250   with \<open>?L\<close> show ?R by blast
2251 next
2252   assume ?R thus ?L
2253     by(auto simp: div_pos_pos_trivial div_neg_neg_trivial)
2254 qed
2257 subsubsection \<open>Quotients of Signs\<close>
2259 lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1"
2262 lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
2265 lemma div_neg_pos_less0: "[| a < (0::int);  0 < b |] ==> a div b < 0"
2266 apply (subgoal_tac "a div b \<le> -1", force)
2267 apply (rule order_trans)
2268 apply (rule_tac a' = "-1" in zdiv_mono1)
2269 apply (auto simp add: div_eq_minus1)
2270 done
2272 lemma div_nonneg_neg_le0: "[| (0::int) \<le> a; b < 0 |] ==> a div b \<le> 0"
2273 by (drule zdiv_mono1_neg, auto)
2275 lemma div_nonpos_pos_le0: "[| (a::int) \<le> 0; b > 0 |] ==> a div b \<le> 0"
2276 by (drule zdiv_mono1, auto)
2278 text\<open>Now for some equivalences of the form @{text"a div b >=< 0 \<longleftrightarrow> \<dots>"}
2279 conditional upon the sign of @{text a} or @{text b}. There are many more.
2280 They should all be simp rules unless that causes too much search.\<close>
2282 lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \<le> a div b) = (0 \<le> a)"
2283 apply auto
2284 apply (drule_tac [2] zdiv_mono1)
2285 apply (auto simp add: linorder_neq_iff)
2286 apply (simp (no_asm_use) add: linorder_not_less [symmetric])
2287 apply (blast intro: div_neg_pos_less0)
2288 done
2290 lemma pos_imp_zdiv_pos_iff:
2291   "0<k \<Longrightarrow> 0 < (i::int) div k \<longleftrightarrow> k \<le> i"
2292 using pos_imp_zdiv_nonneg_iff[of k i] zdiv_eq_0_iff[of i k]
2293 by arith
2295 lemma neg_imp_zdiv_nonneg_iff:
2296   "b < (0::int) ==> (0 \<le> a div b) = (a \<le> (0::int))"
2297 apply (subst div_minus_minus [symmetric])
2298 apply (subst pos_imp_zdiv_nonneg_iff, auto)
2299 done
2301 (*But not (a div b \<le> 0 iff a\<le>0); consider a=1, b=2 when a div b = 0.*)
2302 lemma pos_imp_zdiv_neg_iff: "(0::int) < b ==> (a div b < 0) = (a < 0)"
2303 by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff)
2305 (*Again the law fails for \<le>: consider a = -1, b = -2 when a div b = 0*)
2306 lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)"
2307 by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff)
2309 lemma nonneg1_imp_zdiv_pos_iff:
2310   "(0::int) <= a \<Longrightarrow> (a div b > 0) = (a >= b & b>0)"
2311 apply rule
2312  apply rule
2313   using div_pos_pos_trivial[of a b]apply arith
2314  apply(cases "b=0")apply simp
2315  using div_nonneg_neg_le0[of a b]apply arith
2316 using int_one_le_iff_zero_less[of "a div b"] zdiv_mono1[of b a b]apply simp
2317 done
2319 lemma zmod_le_nonneg_dividend: "(m::int) \<ge> 0 ==> m mod k \<le> m"
2320 apply (rule split_zmod[THEN iffD2])
2321 apply(fastforce dest: q_pos_lemma intro: split_mult_pos_le)
2322 done
2324 lemma zmult_div_cancel:
2325   "(n::int) * (m div n) = m - (m mod n)"
2326   using zmod_zdiv_equality [where a="m" and b="n"]
2327   by (simp add: algebra_simps) (* FIXME: generalize *)
2330 subsubsection \<open>Computation of Division and Remainder\<close>
2332 instantiation int :: semiring_numeral_div
2333 begin
2335 definition divmod_int :: "num \<Rightarrow> num \<Rightarrow> int \<times> int"
2336 where
2337   "divmod_int m n = (numeral m div numeral n, numeral m mod numeral n)"
2339 definition divmod_step_int :: "num \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int"
2340 where
2341   "divmod_step_int l qr = (let (q, r) = qr
2342     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
2343     else (2 * q, r))"
2345 instance
2346   by standard (auto intro: zmod_le_nonneg_dividend simp add: divmod_int_def divmod_step_int_def
2347     pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial zmod_zmult2_eq zdiv_zmult2_eq)
2349 end
2351 declare divmod_algorithm_code [where ?'a = int, code]
2353 context
2354 begin
2356 qualified definition adjust_div :: "int \<times> int \<Rightarrow> int"
2357 where
2358   "adjust_div qr = (let (q, r) = qr in q + of_bool (r \<noteq> 0))"
2360 qualified lemma adjust_div_eq [simp, code]:
2361   "adjust_div (q, r) = q + of_bool (r \<noteq> 0)"
2364 qualified definition adjust_mod :: "int \<Rightarrow> int \<Rightarrow> int"
2365 where
2366   [simp]: "adjust_mod l r = (if r = 0 then 0 else l - r)"
2368 lemma minus_numeral_div_numeral [simp]:
2369   "- numeral m div numeral n = - (adjust_div (divmod m n) :: int)"
2370 proof -
2371   have "int (fst (divmod m n)) = fst (divmod m n)"
2372     by (simp only: fst_divmod divide_int_def) auto
2373   then show ?thesis
2375 qed
2377 lemma minus_numeral_mod_numeral [simp]:
2378   "- numeral m mod numeral n = adjust_mod (numeral n) (snd (divmod m n) :: int)"
2379 proof -
2380   have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
2381     using that by (simp only: snd_divmod mod_int_def) auto
2382   then show ?thesis
2384 qed
2386 lemma numeral_div_minus_numeral [simp]:
2387   "numeral m div - numeral n = - (adjust_div (divmod m n) :: int)"
2388 proof -
2389   have "int (fst (divmod m n)) = fst (divmod m n)"
2390     by (simp only: fst_divmod divide_int_def) auto
2391   then show ?thesis
2393 qed
2395 lemma numeral_mod_minus_numeral [simp]:
2396   "numeral m mod - numeral n = - adjust_mod (numeral n) (snd (divmod m n) :: int)"
2397 proof -
2398   have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
2399     using that by (simp only: snd_divmod mod_int_def) auto
2400   then show ?thesis
2402 qed
2404 lemma minus_one_div_numeral [simp]:
2405   "- 1 div numeral n = - (adjust_div (divmod Num.One n) :: int)"
2406   using minus_numeral_div_numeral [of Num.One n] by simp
2408 lemma minus_one_mod_numeral [simp]:
2409   "- 1 mod numeral n = adjust_mod (numeral n) (snd (divmod Num.One n) :: int)"
2410   using minus_numeral_mod_numeral [of Num.One n] by simp
2412 lemma one_div_minus_numeral [simp]:
2413   "1 div - numeral n = - (adjust_div (divmod Num.One n) :: int)"
2414   using numeral_div_minus_numeral [of Num.One n] by simp
2416 lemma one_mod_minus_numeral [simp]:
2417   "1 mod - numeral n = - adjust_mod (numeral n) (snd (divmod Num.One n) :: int)"
2418   using numeral_mod_minus_numeral [of Num.One n] by simp
2420 end
2423 subsubsection \<open>Further properties\<close>
2425 text \<open>Simplify expresions in which div and mod combine numerical constants\<close>
2427 lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
2428   by (rule div_int_unique [of a b q r]) (simp add: divmod_int_rel_def)
2430 lemma int_div_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a div b = q"
2431   by (rule div_int_unique [of a b q r],
2434 lemma int_mod_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a mod b = r"
2435   by (rule mod_int_unique [of a b q r],
2438 lemma int_mod_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a mod b = r"
2439   by (rule mod_int_unique [of a b q r],
2442 lemma abs_div: "(y::int) dvd x \<Longrightarrow> abs (x div y) = abs x div abs y"
2443 by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
2445 text\<open>Suggested by Matthias Daum\<close>
2446 lemma int_power_div_base:
2447      "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"
2448 apply (subgoal_tac "k ^ m = k ^ ((m - Suc 0) + Suc 0)")
2449  apply (erule ssubst)
2451  apply simp_all
2452 done
2454 text \<open>by Brian Huffman\<close>
2455 lemma zminus_zmod: "- ((x::int) mod m) mod m = - x mod m"
2456 by (rule mod_minus_eq [symmetric])
2458 lemma zdiff_zmod_left: "(x mod m - y) mod m = (x - y) mod (m::int)"
2459 by (rule mod_diff_left_eq [symmetric])
2461 lemma zdiff_zmod_right: "(x - y mod m) mod m = (x - y) mod (m::int)"
2462 by (rule mod_diff_right_eq [symmetric])
2464 lemmas zmod_simps =
2467   mod_mult_right_eq[symmetric]
2468   mod_mult_left_eq [symmetric]
2469   power_mod
2470   zminus_zmod zdiff_zmod_left zdiff_zmod_right
2472 text \<open>Distributive laws for function @{text nat}.\<close>
2474 lemma nat_div_distrib: "0 \<le> x \<Longrightarrow> nat (x div y) = nat x div nat y"
2475 apply (rule linorder_cases [of y 0])
2477 apply simp
2478 apply (simp add: nat_eq_iff pos_imp_zdiv_nonneg_iff zdiv_int)
2479 done
2481 (*Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't*)
2482 lemma nat_mod_distrib:
2483   "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x mod y) = nat x mod nat y"
2484 apply (case_tac "y = 0", simp)
2485 apply (simp add: nat_eq_iff zmod_int)
2486 done
2488 text  \<open>transfer setup\<close>
2490 lemma transfer_nat_int_functions:
2491     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
2492     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
2493   by (auto simp add: nat_div_distrib nat_mod_distrib)
2495 lemma transfer_nat_int_function_closures:
2496     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
2497     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
2498   apply (cases "y = 0")
2499   apply (auto simp add: pos_imp_zdiv_nonneg_iff)
2500   apply (cases "y = 0")
2501   apply auto
2502 done
2504 declare transfer_morphism_nat_int [transfer add return:
2505   transfer_nat_int_functions
2506   transfer_nat_int_function_closures
2507 ]
2509 lemma transfer_int_nat_functions:
2510     "(int x) div (int y) = int (x div y)"
2511     "(int x) mod (int y) = int (x mod y)"
2512   by (auto simp add: zdiv_int zmod_int)
2514 lemma transfer_int_nat_function_closures:
2515     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
2516     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
2517   by (simp_all only: is_nat_def transfer_nat_int_function_closures)
2519 declare transfer_morphism_int_nat [transfer add return:
2520   transfer_int_nat_functions
2521   transfer_int_nat_function_closures
2522 ]
2524 text\<open>Suggested by Matthias Daum\<close>
2525 lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
2526 apply (subgoal_tac "nat x div nat k < nat x")
2527  apply (simp add: nat_div_distrib [symmetric])
2528 apply (rule Divides.div_less_dividend, simp_all)
2529 done
2531 lemma zmod_eq_dvd_iff: "(x::int) mod n = y mod n \<longleftrightarrow> n dvd x - y"
2532 proof
2533   assume H: "x mod n = y mod n"
2534   hence "x mod n - y mod n = 0" by simp
2535   hence "(x mod n - y mod n) mod n = 0" by simp
2536   hence "(x - y) mod n = 0" by (simp add: mod_diff_eq[symmetric])
2537   thus "n dvd x - y" by (simp add: dvd_eq_mod_eq_0)
2538 next
2539   assume H: "n dvd x - y"
2540   then obtain k where k: "x-y = n*k" unfolding dvd_def by blast
2541   hence "x = n*k + y" by simp
2542   hence "x mod n = (n*k + y) mod n" by simp
2543   thus "x mod n = y mod n" by (simp add: mod_add_left_eq)
2544 qed
2546 lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y  mod n" and xy:"y \<le> x"
2547   shows "\<exists>q. x = y + n * q"
2548 proof-
2549   from xy have th: "int x - int y = int (x - y)" by simp
2550   from xyn have "int x mod int n = int y mod int n"
2551     by (simp add: zmod_int [symmetric])
2552   hence "int n dvd int x - int y" by (simp only: zmod_eq_dvd_iff[symmetric])
2553   hence "n dvd x - y" by (simp add: th zdvd_int)
2554   then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith
2555 qed
2557 lemma nat_mod_eq_iff: "(x::nat) mod n = y mod n \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)"
2558   (is "?lhs = ?rhs")
2559 proof
2560   assume H: "x mod n = y mod n"
2561   {assume xy: "x \<le> y"
2562     from H have th: "y mod n = x mod n" by simp
2563     from nat_mod_eq_lemma[OF th xy] have ?rhs
2564       apply clarify  apply (rule_tac x="q" in exI) by (rule exI[where x="0"], simp)}
2565   moreover
2566   {assume xy: "y \<le> x"
2567     from nat_mod_eq_lemma[OF H xy] have ?rhs
2568       apply clarify  apply (rule_tac x="0" in exI) by (rule_tac x="q" in exI, simp)}
2569   ultimately  show ?rhs using linear[of x y] by blast
2570 next
2571   assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast
2572   hence "(x + n * q1) mod n = (y + n * q2) mod n" by simp
2573   thus  ?lhs by simp
2574 qed
2576 subsubsection \<open>Dedicated simproc for calculation\<close>
2578 text \<open>
2579   There is space for improvement here: the calculation itself
2580   could be carried outside the logic, and a generic simproc
2581   (simplifier setup) for generic calculation would be helpful.
2582 \<close>
2584 simproc_setup numeral_divmod
2585   ("0 div 0 :: 'a :: semiring_numeral_div" | "0 mod 0 :: 'a :: semiring_numeral_div" |
2586    "0 div 1 :: 'a :: semiring_numeral_div" | "0 mod 1 :: 'a :: semiring_numeral_div" |
2587    "0 div - 1 :: int" | "0 mod - 1 :: int" |
2588    "0 div numeral b :: 'a :: semiring_numeral_div" | "0 mod numeral b :: 'a :: semiring_numeral_div" |
2589    "0 div - numeral b :: int" | "0 mod - numeral b :: int" |
2590    "1 div 0 :: 'a :: semiring_numeral_div" | "1 mod 0 :: 'a :: semiring_numeral_div" |
2591    "1 div 1 :: 'a :: semiring_numeral_div" | "1 mod 1 :: 'a :: semiring_numeral_div" |
2592    "1 div - 1 :: int" | "1 mod - 1 :: int" |
2593    "1 div numeral b :: 'a :: semiring_numeral_div" | "1 mod numeral b :: 'a :: semiring_numeral_div" |
2594    "1 div - numeral b :: int" |"1 mod - numeral b :: int" |
2595    "- 1 div 0 :: int" | "- 1 mod 0 :: int" | "- 1 div 1 :: int" | "- 1 mod 1 :: int" |
2596    "- 1 div - 1 :: int" | "- 1 mod - 1 :: int" | "- 1 div numeral b :: int" | "- 1 mod numeral b :: int" |
2597    "- 1 div - numeral b :: int" | "- 1 mod - numeral b :: int" |
2598    "numeral a div 0 :: 'a :: semiring_numeral_div" | "numeral a mod 0 :: 'a :: semiring_numeral_div" |
2599    "numeral a div 1 :: 'a :: semiring_numeral_div" | "numeral a mod 1 :: 'a :: semiring_numeral_div" |
2600    "numeral a div - 1 :: int" | "numeral a mod - 1 :: int" |
2601    "numeral a div numeral b :: 'a :: semiring_numeral_div" | "numeral a mod numeral b :: 'a :: semiring_numeral_div" |
2602    "numeral a div - numeral b :: int" | "numeral a mod - numeral b :: int" |
2603    "- numeral a div 0 :: int" | "- numeral a mod 0 :: int" |
2604    "- numeral a div 1 :: int" | "- numeral a mod 1 :: int" |
2605    "- numeral a div - 1 :: int" | "- numeral a mod - 1 :: int" |
2606    "- numeral a div numeral b :: int" | "- numeral a mod numeral b :: int" |
2607    "- numeral a div - numeral b :: int" | "- numeral a mod - numeral b :: int") =
2608 \<open> let
2609     val if_cong = the (Code.get_case_cong @{theory} @{const_name If});
2610     fun successful_rewrite ctxt ct =
2611       let
2612         val thm = Simplifier.rewrite ctxt ct
2613       in if Thm.is_reflexive thm then NONE else SOME thm end;
2614   in fn phi =>
2615     let
2616       val simps = Morphism.fact phi (@{thms div_0 mod_0 div_by_0 mod_by_0 div_by_1 mod_by_1
2617         one_div_numeral one_mod_numeral minus_one_div_numeral minus_one_mod_numeral
2618         one_div_minus_numeral one_mod_minus_numeral
2619         numeral_div_numeral numeral_mod_numeral minus_numeral_div_numeral minus_numeral_mod_numeral
2620         numeral_div_minus_numeral numeral_mod_minus_numeral
2621         div_minus_minus mod_minus_minus Divides.adjust_div_eq of_bool_eq one_neq_zero
2622         numeral_neq_zero neg_equal_0_iff_equal arith_simps arith_special divmod_trivial
2623         divmod_cancel divmod_steps divmod_step_eq fst_conv snd_conv numeral_One
2624         case_prod_beta rel_simps Divides.adjust_mod_def div_minus1_right mod_minus1_right
2625         minus_minus numeral_times_numeral mult_zero_right mult_1_right}
2626         @ [@{lemma "0 = 0 \<longleftrightarrow> True" by simp}]);
2627       fun prepare_simpset ctxt = HOL_ss |> Simplifier.simpset_map ctxt
2629     in fn ctxt => successful_rewrite (Simplifier.put_simpset (prepare_simpset ctxt) ctxt) end
2630   end;
2631 \<close>
2634 subsubsection \<open>Code generation\<close>
2636 lemma [code]:
2637   fixes k :: int
2638   shows
2639     "k div 0 = 0"
2640     "k mod 0 = k"
2641     "0 div k = 0"
2642     "0 mod k = 0"
2643     "k div Int.Pos Num.One = k"
2644     "k mod Int.Pos Num.One = 0"
2645     "k div Int.Neg Num.One = - k"
2646     "k mod Int.Neg Num.One = 0"
2647     "Int.Pos m div Int.Pos n = (fst (divmod m n) :: int)"
2648     "Int.Pos m mod Int.Pos n = (snd (divmod m n) :: int)"
2649     "Int.Neg m div Int.Pos n = - (Divides.adjust_div (divmod m n) :: int)"
2650     "Int.Neg m mod Int.Pos n = Divides.adjust_mod (Int.Pos n) (snd (divmod m n) :: int)"
2651     "Int.Pos m div Int.Neg n = - (Divides.adjust_div (divmod m n) :: int)"
2652     "Int.Pos m mod Int.Neg n = - Divides.adjust_mod (Int.Pos n) (snd (divmod m n) :: int)"
2653     "Int.Neg m div Int.Neg n = (fst (divmod m n) :: int)"
2654     "Int.Neg m mod Int.Neg n = - (snd (divmod m n) :: int)"
2655   by simp_all
2657 code_identifier
2658   code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
2660 lemma dvd_eq_mod_eq_0_numeral:
2661   "numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semiring_div)"
2662   by (fact dvd_eq_mod_eq_0)
2664 end