src/HOL/Divides.thy
 author haftmann Sun Oct 08 22:28:20 2017 +0200 (21 months ago) changeset 66801 f3fda9777f9a parent 66800 128e9ed9f63c child 66806 a4e82b58d833 permissions -rw-r--r--
avoid fact name clashes
1 (*  Title:      HOL/Divides.thy
2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3     Copyright   1999  University of Cambridge
4 *)
6 section \<open>More on quotient and remainder\<close>
8 theory Divides
9 imports Parity
10 begin
12 subsection \<open>Quotient and remainder in integral domains with additional properties\<close>
14 class semiring_div = semidom_modulo +
15   assumes div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
16     and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
17 begin
19 lemma div_mult_self2 [simp]:
20   assumes "b \<noteq> 0"
21   shows "(a + b * c) div b = c + a div b"
22   using assms div_mult_self1 [of b a c] by (simp add: mult.commute)
24 lemma div_mult_self3 [simp]:
25   assumes "b \<noteq> 0"
26   shows "(c * b + a) div b = c + a div b"
27   using assms by (simp add: add.commute)
29 lemma div_mult_self4 [simp]:
30   assumes "b \<noteq> 0"
31   shows "(b * c + a) div b = c + a div b"
32   using assms by (simp add: add.commute)
34 lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b"
35 proof (cases "b = 0")
36   case True then show ?thesis by simp
37 next
38   case False
39   have "a + c * b = (a + c * b) div b * b + (a + c * b) mod b"
40     by (simp add: div_mult_mod_eq)
41   also from False div_mult_self1 [of b a c] have
42     "\<dots> = (c + a div b) * b + (a + c * b) mod b"
43       by (simp add: algebra_simps)
44   finally have "a = a div b * b + (a + c * b) mod b"
45     by (simp add: add.commute [of a] add.assoc distrib_right)
46   then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
47     by (simp add: div_mult_mod_eq)
48   then show ?thesis by simp
49 qed
51 lemma mod_mult_self2 [simp]:
52   "(a + b * c) mod b = a mod b"
53   by (simp add: mult.commute [of b])
55 lemma mod_mult_self3 [simp]:
56   "(c * b + a) mod b = a mod b"
57   by (simp add: add.commute)
59 lemma mod_mult_self4 [simp]:
60   "(b * c + a) mod b = a mod b"
61   by (simp add: add.commute)
63 lemma mod_mult_self1_is_0 [simp]:
64   "b * a mod b = 0"
65   using mod_mult_self2 [of 0 b a] by simp
67 lemma mod_mult_self2_is_0 [simp]:
68   "a * b mod b = 0"
69   using mod_mult_self1 [of 0 a b] by simp
71 lemma div_add_self1:
72   assumes "b \<noteq> 0"
73   shows "(b + a) div b = a div b + 1"
74   using assms div_mult_self1 [of b a 1] by (simp add: add.commute)
76 lemma div_add_self2:
77   assumes "b \<noteq> 0"
78   shows "(a + b) div b = a div b + 1"
79   using assms div_add_self1 [of b a] by (simp add: add.commute)
81 lemma mod_add_self1 [simp]:
82   "(b + a) mod b = a mod b"
83   using mod_mult_self1 [of a 1 b] by (simp add: add.commute)
85 lemma mod_add_self2 [simp]:
86   "(a + b) mod b = a mod b"
87   using mod_mult_self1 [of a 1 b] by simp
89 lemma mod_div_trivial [simp]:
90   "a mod b div b = 0"
91 proof (cases "b = 0")
92   assume "b = 0"
93   thus ?thesis by simp
94 next
95   assume "b \<noteq> 0"
96   hence "a div b + a mod b div b = (a mod b + a div b * b) div b"
97     by (rule div_mult_self1 [symmetric])
98   also have "\<dots> = a div b"
99     by (simp only: mod_div_mult_eq)
100   also have "\<dots> = a div b + 0"
101     by simp
102   finally show ?thesis
103     by (rule add_left_imp_eq)
104 qed
106 lemma mod_mod_trivial [simp]:
107   "a mod b mod b = a mod b"
108 proof -
109   have "a mod b mod b = (a mod b + a div b * b) mod b"
110     by (simp only: mod_mult_self1)
111   also have "\<dots> = a mod b"
112     by (simp only: mod_div_mult_eq)
113   finally show ?thesis .
114 qed
116 lemma mod_mod_cancel:
117   assumes "c dvd b"
118   shows "a mod b mod c = a mod c"
119 proof -
120   from \<open>c dvd b\<close> obtain k where "b = c * k"
121     by (rule dvdE)
122   have "a mod b mod c = a mod (c * k) mod c"
123     by (simp only: \<open>b = c * k\<close>)
124   also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"
125     by (simp only: mod_mult_self1)
126   also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
127     by (simp only: ac_simps)
128   also have "\<dots> = a mod c"
129     by (simp only: div_mult_mod_eq)
130   finally show ?thesis .
131 qed
133 lemma div_mult_mult2 [simp]:
134   "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
135   by (drule div_mult_mult1) (simp add: mult.commute)
137 lemma div_mult_mult1_if [simp]:
138   "(c * a) div (c * b) = (if c = 0 then 0 else a div b)"
139   by simp_all
141 lemma mod_mult_mult1:
142   "(c * a) mod (c * b) = c * (a mod b)"
143 proof (cases "c = 0")
144   case True then show ?thesis by simp
145 next
146   case False
147   from div_mult_mod_eq
148   have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .
149   with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)
150     = c * a + c * (a mod b)" by (simp add: algebra_simps)
151   with div_mult_mod_eq show ?thesis by simp
152 qed
154 lemma mod_mult_mult2:
155   "(a * c) mod (b * c) = (a mod b) * c"
156   using mod_mult_mult1 [of c a b] by (simp add: mult.commute)
158 lemma mult_mod_left: "(a mod b) * c = (a * c) mod (b * c)"
159   by (fact mod_mult_mult2 [symmetric])
161 lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)"
162   by (fact mod_mult_mult1 [symmetric])
164 lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
165   unfolding dvd_def by (auto simp add: mod_mult_mult1)
167 lemma div_plus_div_distrib_dvd_left:
168   "c dvd a \<Longrightarrow> (a + b) div c = a div c + b div c"
169   by (cases "c = 0") (auto elim: dvdE)
171 lemma div_plus_div_distrib_dvd_right:
172   "c dvd b \<Longrightarrow> (a + b) div c = a div c + b div c"
173   using div_plus_div_distrib_dvd_left [of c b a]
174   by (simp add: ac_simps)
176 named_theorems mod_simps
178 text \<open>Addition respects modular equivalence.\<close>
180 lemma mod_add_left_eq [mod_simps]:
181   "(a mod c + b) mod c = (a + b) mod c"
182 proof -
183   have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
184     by (simp only: div_mult_mod_eq)
185   also have "\<dots> = (a mod c + b + a div c * c) mod c"
186     by (simp only: ac_simps)
187   also have "\<dots> = (a mod c + b) mod c"
188     by (rule mod_mult_self1)
189   finally show ?thesis
190     by (rule sym)
191 qed
193 lemma mod_add_right_eq [mod_simps]:
194   "(a + b mod c) mod c = (a + b) mod c"
195   using mod_add_left_eq [of b c a] by (simp add: ac_simps)
197 lemma mod_add_eq:
198   "(a mod c + b mod c) mod c = (a + b) mod c"
199   by (simp add: mod_add_left_eq mod_add_right_eq)
201 lemma mod_sum_eq [mod_simps]:
202   "(\<Sum>i\<in>A. f i mod a) mod a = sum f A mod a"
203 proof (induct A rule: infinite_finite_induct)
204   case (insert i A)
205   then have "(\<Sum>i\<in>insert i A. f i mod a) mod a
206     = (f i mod a + (\<Sum>i\<in>A. f i mod a)) mod a"
207     by simp
208   also have "\<dots> = (f i + (\<Sum>i\<in>A. f i mod a) mod a) mod a"
209     by (simp add: mod_simps)
210   also have "\<dots> = (f i + (\<Sum>i\<in>A. f i) mod a) mod a"
211     by (simp add: insert.hyps)
212   finally show ?case
213     by (simp add: insert.hyps mod_simps)
214 qed simp_all
216 lemma mod_add_cong:
217   assumes "a mod c = a' mod c"
218   assumes "b mod c = b' mod c"
219   shows "(a + b) mod c = (a' + b') mod c"
220 proof -
221   have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c"
222     unfolding assms ..
223   then show ?thesis
224     by (simp add: mod_add_eq)
225 qed
227 text \<open>Multiplication respects modular equivalence.\<close>
229 lemma mod_mult_left_eq [mod_simps]:
230   "((a mod c) * b) mod c = (a * b) mod c"
231 proof -
232   have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
233     by (simp only: div_mult_mod_eq)
234   also have "\<dots> = (a mod c * b + a div c * b * c) mod c"
235     by (simp only: algebra_simps)
236   also have "\<dots> = (a mod c * b) mod c"
237     by (rule mod_mult_self1)
238   finally show ?thesis
239     by (rule sym)
240 qed
242 lemma mod_mult_right_eq [mod_simps]:
243   "(a * (b mod c)) mod c = (a * b) mod c"
244   using mod_mult_left_eq [of b c a] by (simp add: ac_simps)
246 lemma mod_mult_eq:
247   "((a mod c) * (b mod c)) mod c = (a * b) mod c"
248   by (simp add: mod_mult_left_eq mod_mult_right_eq)
250 lemma mod_prod_eq [mod_simps]:
251   "(\<Prod>i\<in>A. f i mod a) mod a = prod f A mod a"
252 proof (induct A rule: infinite_finite_induct)
253   case (insert i A)
254   then have "(\<Prod>i\<in>insert i A. f i mod a) mod a
255     = (f i mod a * (\<Prod>i\<in>A. f i mod a)) mod a"
256     by simp
257   also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i mod a) mod a)) mod a"
258     by (simp add: mod_simps)
259   also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i) mod a)) mod a"
260     by (simp add: insert.hyps)
261   finally show ?case
262     by (simp add: insert.hyps mod_simps)
263 qed simp_all
265 lemma mod_mult_cong:
266   assumes "a mod c = a' mod c"
267   assumes "b mod c = b' mod c"
268   shows "(a * b) mod c = (a' * b') mod c"
269 proof -
270   have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c"
271     unfolding assms ..
272   then show ?thesis
273     by (simp add: mod_mult_eq)
274 qed
276 text \<open>Exponentiation respects modular equivalence.\<close>
278 lemma power_mod [mod_simps]:
279   "((a mod b) ^ n) mod b = (a ^ n) mod b"
280 proof (induct n)
281   case 0
282   then show ?case by simp
283 next
284   case (Suc n)
285   have "(a mod b) ^ Suc n mod b = (a mod b) * ((a mod b) ^ n mod b) mod b"
286     by (simp add: mod_mult_right_eq)
287   with Suc show ?case
288     by (simp add: mod_mult_left_eq mod_mult_right_eq)
289 qed
291 end
293 class ring_div = comm_ring_1 + semiring_div
294 begin
296 subclass idom_divide ..
298 lemma div_minus_minus [simp]: "(- a) div (- b) = a div b"
299   using div_mult_mult1 [of "- 1" a b] by simp
301 lemma mod_minus_minus [simp]: "(- a) mod (- b) = - (a mod b)"
302   using mod_mult_mult1 [of "- 1" a b] by simp
304 lemma div_minus_right: "a div (- b) = (- a) div b"
305   using div_minus_minus [of "- a" b] by simp
307 lemma mod_minus_right: "a mod (- b) = - ((- a) mod b)"
308   using mod_minus_minus [of "- a" b] by simp
310 lemma div_minus1_right [simp]: "a div (- 1) = - a"
311   using div_minus_right [of a 1] by simp
313 lemma mod_minus1_right [simp]: "a mod (- 1) = 0"
314   using mod_minus_right [of a 1] by simp
316 text \<open>Negation respects modular equivalence.\<close>
318 lemma mod_minus_eq [mod_simps]:
319   "(- (a mod b)) mod b = (- a) mod b"
320 proof -
321   have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
322     by (simp only: div_mult_mod_eq)
323   also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
324     by (simp add: ac_simps)
325   also have "\<dots> = (- (a mod b)) mod b"
326     by (rule mod_mult_self1)
327   finally show ?thesis
328     by (rule sym)
329 qed
331 lemma mod_minus_cong:
332   assumes "a mod b = a' mod b"
333   shows "(- a) mod b = (- a') mod b"
334 proof -
335   have "(- (a mod b)) mod b = (- (a' mod b)) mod b"
336     unfolding assms ..
337   then show ?thesis
338     by (simp add: mod_minus_eq)
339 qed
341 text \<open>Subtraction respects modular equivalence.\<close>
343 lemma mod_diff_left_eq [mod_simps]:
344   "(a mod c - b) mod c = (a - b) mod c"
345   using mod_add_cong [of a c "a mod c" "- b" "- b"]
346   by simp
348 lemma mod_diff_right_eq [mod_simps]:
349   "(a - b mod c) mod c = (a - b) mod c"
350   using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
351   by simp
353 lemma mod_diff_eq:
354   "(a mod c - b mod c) mod c = (a - b) mod c"
355   using mod_add_cong [of a c "a mod c" "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
356   by simp
358 lemma mod_diff_cong:
359   assumes "a mod c = a' mod c"
360   assumes "b mod c = b' mod c"
361   shows "(a - b) mod c = (a' - b') mod c"
362   using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"]
363   by simp
365 lemma minus_mod_self2 [simp]:
366   "(a - b) mod b = a mod b"
367   using mod_diff_right_eq [of a b b]
368   by (simp add: mod_diff_right_eq)
370 lemma minus_mod_self1 [simp]:
371   "(b - a) mod b = - a mod b"
372   using mod_add_self2 [of "- a" b] by simp
374 end
377 subsection \<open>Euclidean (semi)rings with cancel rules\<close>
379 class euclidean_semiring_cancel = euclidean_semiring + semiring_div
381 class euclidean_ring_cancel = euclidean_ring + ring_div
383 context unique_euclidean_semiring
384 begin
386 subclass euclidean_semiring_cancel
387 proof
388   show "(a + c * b) div b = c + a div b" if "b \<noteq> 0" for a b c
389   proof (cases a b rule: divmod_cases)
390     case by0
391     with \<open>b \<noteq> 0\<close> show ?thesis
392       by simp
393   next
394     case (divides q)
395     then show ?thesis
396       by (simp add: ac_simps)
397   next
398     case (remainder q r)
399     then show ?thesis
400       by (auto intro: div_eqI simp add: algebra_simps)
401   qed
402 next
403   show"(c * a) div (c * b) = a div b" if "c \<noteq> 0" for a b c
404   proof (cases a b rule: divmod_cases)
405     case by0
406     then show ?thesis
407       by simp
408   next
409     case (divides q)
410     with \<open>c \<noteq> 0\<close> show ?thesis
411       by (simp add: mult.left_commute [of c])
412   next
413     case (remainder q r)
414     from \<open>b \<noteq> 0\<close> \<open>c \<noteq> 0\<close> have "b * c \<noteq> 0"
415       by simp
416     from remainder \<open>c \<noteq> 0\<close>
417     have "uniqueness_constraint (r * c) (b * c)"
418       and "euclidean_size (r * c) < euclidean_size (b * c)"
419       by (simp_all add: uniqueness_constraint_mono_mult uniqueness_constraint_mod size_mono_mult)
420     with remainder show ?thesis
421       by (auto intro!: div_eqI [of _ "c * (a mod b)"] simp add: algebra_simps)
422         (use \<open>b * c \<noteq> 0\<close> in simp)
423   qed
424 qed
426 end
428 context unique_euclidean_ring
429 begin
431 subclass euclidean_ring_cancel ..
433 end
436 subsection \<open>Parity\<close>
438 class semiring_div_parity = semiring_div + comm_semiring_1_cancel + numeral +
439   assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
440   assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
441   assumes zero_not_eq_two: "0 \<noteq> 2"
442 begin
444 lemma parity_cases [case_names even odd]:
445   assumes "a mod 2 = 0 \<Longrightarrow> P"
446   assumes "a mod 2 = 1 \<Longrightarrow> P"
447   shows P
448   using assms parity by blast
450 lemma one_div_two_eq_zero [simp]:
451   "1 div 2 = 0"
452 proof (cases "2 = 0")
453   case True then show ?thesis by simp
454 next
455   case False
456   from div_mult_mod_eq have "1 div 2 * 2 + 1 mod 2 = 1" .
457   with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
458   then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq del: mult_eq_0_iff)
459   then have "1 div 2 = 0 \<or> 2 = 0" by simp
460   with False show ?thesis by auto
461 qed
463 lemma not_mod_2_eq_0_eq_1 [simp]:
464   "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
465   by (cases a rule: parity_cases) simp_all
467 lemma not_mod_2_eq_1_eq_0 [simp]:
468   "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
469   by (cases a rule: parity_cases) simp_all
471 subclass semiring_parity
472 proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)
473   show "1 mod 2 = 1"
474     by (fact one_mod_two_eq_one)
475 next
476   fix a b
477   assume "a mod 2 = 1"
478   moreover assume "b mod 2 = 1"
479   ultimately show "(a + b) mod 2 = 0"
480     using mod_add_eq [of a 2 b] by simp
481 next
482   fix a b
483   assume "(a * b) mod 2 = 0"
484   then have "(a mod 2) * (b mod 2) mod 2 = 0"
485     by (simp add: mod_mult_eq)
486   then have "(a mod 2) * (b mod 2) = 0"
487     by (cases "a mod 2 = 0") simp_all
488   then show "a mod 2 = 0 \<or> b mod 2 = 0"
489     by (rule divisors_zero)
490 next
491   fix a
492   assume "a mod 2 = 1"
493   then have "a = a div 2 * 2 + 1"
494     using div_mult_mod_eq [of a 2] by simp
495   then show "\<exists>b. a = b + 1" ..
496 qed
498 lemma even_iff_mod_2_eq_zero:
499   "even a \<longleftrightarrow> a mod 2 = 0"
500   by (fact dvd_eq_mod_eq_0)
502 lemma odd_iff_mod_2_eq_one:
503   "odd a \<longleftrightarrow> a mod 2 = 1"
504   by (simp add: even_iff_mod_2_eq_zero)
506 lemma even_succ_div_two [simp]:
507   "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
508   by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
510 lemma odd_succ_div_two [simp]:
511   "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
512   by (auto elim!: oddE simp add: zero_not_eq_two [symmetric] add.assoc)
514 lemma even_two_times_div_two:
515   "even a \<Longrightarrow> 2 * (a div 2) = a"
516   by (fact dvd_mult_div_cancel)
518 lemma odd_two_times_div_two_succ [simp]:
519   "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
520   using mult_div_mod_eq [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
522 end
525 subsection \<open>Numeral division with a pragmatic type class\<close>
527 text \<open>
528   The following type class contains everything necessary to formulate
529   a division algorithm in ring structures with numerals, restricted
530   to its positive segments.  This is its primary motivation, and it
531   could surely be formulated using a more fine-grained, more algebraic
532   and less technical class hierarchy.
533 \<close>
535 class semiring_numeral_div = semiring_div + comm_semiring_1_cancel + linordered_semidom +
536   assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
537     and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
538     and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
539     and mod_less_eq_dividend: "0 \<le> a \<Longrightarrow> a mod b \<le> a"
540     and pos_mod_bound: "0 < b \<Longrightarrow> a mod b < b"
541     and pos_mod_sign: "0 < b \<Longrightarrow> 0 \<le> a mod b"
542     and mod_mult2_eq: "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
543     and div_mult2_eq: "0 \<le> c \<Longrightarrow> a div (b * c) = a div b div c"
544   assumes discrete: "a < b \<longleftrightarrow> a + 1 \<le> b"
545   fixes divmod :: "num \<Rightarrow> num \<Rightarrow> 'a \<times> 'a"
546     and divmod_step :: "num \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<times> 'a"
547   assumes divmod_def: "divmod m n = (numeral m div numeral n, numeral m mod numeral n)"
548     and divmod_step_def: "divmod_step l qr = (let (q, r) = qr
549     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
550     else (2 * q, r))"
551     \<comment> \<open>These are conceptually definitions but force generated code
552     to be monomorphic wrt. particular instances of this class which
553     yields a significant speedup.\<close>
554 begin
556 subclass semiring_div_parity
557 proof
558   fix a
559   show "a mod 2 = 0 \<or> a mod 2 = 1"
560   proof (rule ccontr)
561     assume "\<not> (a mod 2 = 0 \<or> a mod 2 = 1)"
562     then have "a mod 2 \<noteq> 0" and "a mod 2 \<noteq> 1" by simp_all
563     have "0 < 2" by simp
564     with pos_mod_bound pos_mod_sign have "0 \<le> a mod 2" "a mod 2 < 2" by simp_all
565     with \<open>a mod 2 \<noteq> 0\<close> have "0 < a mod 2" by simp
566     with discrete have "1 \<le> a mod 2" by simp
567     with \<open>a mod 2 \<noteq> 1\<close> have "1 < a mod 2" by simp
568     with discrete have "2 \<le> a mod 2" by simp
569     with \<open>a mod 2 < 2\<close> show False by simp
570   qed
571 next
572   show "1 mod 2 = 1"
573     by (rule mod_less) simp_all
574 next
575   show "0 \<noteq> 2"
576     by simp
577 qed
579 lemma divmod_digit_1:
580   assumes "0 \<le> a" "0 < b" and "b \<le> a mod (2 * b)"
581   shows "2 * (a div (2 * b)) + 1 = a div b" (is "?P")
582     and "a mod (2 * b) - b = a mod b" (is "?Q")
583 proof -
584   from assms mod_less_eq_dividend [of a "2 * b"] have "b \<le> a"
585     by (auto intro: trans)
586   with \<open>0 < b\<close> have "0 < a div b" by (auto intro: div_positive)
587   then have [simp]: "1 \<le> a div b" by (simp add: discrete)
588   with \<open>0 < b\<close> have mod_less: "a mod b < b" by (simp add: pos_mod_bound)
589   define w where "w = a div b mod 2"
590   with parity have w_exhaust: "w = 0 \<or> w = 1" by auto
591   have mod_w: "a mod (2 * b) = a mod b + b * w"
592     by (simp add: w_def mod_mult2_eq ac_simps)
593   from assms w_exhaust have "w = 1"
594     by (auto simp add: mod_w) (insert mod_less, auto)
595   with mod_w have mod: "a mod (2 * b) = a mod b + b" by simp
596   have "2 * (a div (2 * b)) = a div b - w"
597     by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
598   with \<open>w = 1\<close> have div: "2 * (a div (2 * b)) = a div b - 1" by simp
599   then show ?P and ?Q
600     by (simp_all add: div mod add_implies_diff [symmetric])
601 qed
603 lemma divmod_digit_0:
604   assumes "0 < b" and "a mod (2 * b) < b"
605   shows "2 * (a div (2 * b)) = a div b" (is "?P")
606     and "a mod (2 * b) = a mod b" (is "?Q")
607 proof -
608   define w where "w = a div b mod 2"
609   with parity have w_exhaust: "w = 0 \<or> w = 1" by auto
610   have mod_w: "a mod (2 * b) = a mod b + b * w"
611     by (simp add: w_def mod_mult2_eq ac_simps)
612   moreover have "b \<le> a mod b + b"
613   proof -
614     from \<open>0 < b\<close> pos_mod_sign have "0 \<le> a mod b" by blast
615     then have "0 + b \<le> a mod b + b" by (rule add_right_mono)
616     then show ?thesis by simp
617   qed
618   moreover note assms w_exhaust
619   ultimately have "w = 0" by auto
620   with mod_w have mod: "a mod (2 * b) = a mod b" by simp
621   have "2 * (a div (2 * b)) = a div b - w"
622     by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
623   with \<open>w = 0\<close> have div: "2 * (a div (2 * b)) = a div b" by simp
624   then show ?P and ?Q
625     by (simp_all add: div mod)
626 qed
628 lemma fst_divmod:
629   "fst (divmod m n) = numeral m div numeral n"
630   by (simp add: divmod_def)
632 lemma snd_divmod:
633   "snd (divmod m n) = numeral m mod numeral n"
634   by (simp add: divmod_def)
636 text \<open>
637   This is a formulation of one step (referring to one digit position)
638   in school-method division: compare the dividend at the current
639   digit position with the remainder from previous division steps
640   and evaluate accordingly.
641 \<close>
643 lemma divmod_step_eq [simp]:
644   "divmod_step l (q, r) = (if numeral l \<le> r
645     then (2 * q + 1, r - numeral l) else (2 * q, r))"
646   by (simp add: divmod_step_def)
648 text \<open>
649   This is a formulation of school-method division.
650   If the divisor is smaller than the dividend, terminate.
651   If not, shift the dividend to the right until termination
652   occurs and then reiterate single division steps in the
653   opposite direction.
654 \<close>
656 lemma divmod_divmod_step:
657   "divmod m n = (if m < n then (0, numeral m)
658     else divmod_step n (divmod m (Num.Bit0 n)))"
659 proof (cases "m < n")
660   case True then have "numeral m < numeral n" by simp
661   then show ?thesis
662     by (simp add: prod_eq_iff div_less mod_less fst_divmod snd_divmod)
663 next
664   case False
665   have "divmod m n =
666     divmod_step n (numeral m div (2 * numeral n),
667       numeral m mod (2 * numeral n))"
668   proof (cases "numeral n \<le> numeral m mod (2 * numeral n)")
669     case True
670     with divmod_step_eq
671       have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
672         (2 * (numeral m div (2 * numeral n)) + 1, numeral m mod (2 * numeral n) - numeral n)"
673         by simp
674     moreover from True divmod_digit_1 [of "numeral m" "numeral n"]
675       have "2 * (numeral m div (2 * numeral n)) + 1 = numeral m div numeral n"
676       and "numeral m mod (2 * numeral n) - numeral n = numeral m mod numeral n"
677       by simp_all
678     ultimately show ?thesis by (simp only: divmod_def)
679   next
680     case False then have *: "numeral m mod (2 * numeral n) < numeral n"
681       by (simp add: not_le)
682     with divmod_step_eq
683       have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
684         (2 * (numeral m div (2 * numeral n)), numeral m mod (2 * numeral n))"
685         by auto
686     moreover from * divmod_digit_0 [of "numeral n" "numeral m"]
687       have "2 * (numeral m div (2 * numeral n)) = numeral m div numeral n"
688       and "numeral m mod (2 * numeral n) = numeral m mod numeral n"
689       by (simp_all only: zero_less_numeral)
690     ultimately show ?thesis by (simp only: divmod_def)
691   qed
692   then have "divmod m n =
693     divmod_step n (numeral m div numeral (Num.Bit0 n),
694       numeral m mod numeral (Num.Bit0 n))"
695     by (simp only: numeral.simps distrib mult_1)
696   then have "divmod m n = divmod_step n (divmod m (Num.Bit0 n))"
697     by (simp add: divmod_def)
698   with False show ?thesis by simp
699 qed
701 text \<open>The division rewrite proper -- first, trivial results involving \<open>1\<close>\<close>
703 lemma divmod_trivial [simp]:
704   "divmod Num.One Num.One = (numeral Num.One, 0)"
705   "divmod (Num.Bit0 m) Num.One = (numeral (Num.Bit0 m), 0)"
706   "divmod (Num.Bit1 m) Num.One = (numeral (Num.Bit1 m), 0)"
707   "divmod num.One (num.Bit0 n) = (0, Numeral1)"
708   "divmod num.One (num.Bit1 n) = (0, Numeral1)"
709   using divmod_divmod_step [of "Num.One"] by (simp_all add: divmod_def)
711 text \<open>Division by an even number is a right-shift\<close>
713 lemma divmod_cancel [simp]:
714   "divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r))" (is ?P)
715   "divmod (Num.Bit1 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r + 1))" (is ?Q)
716 proof -
717   have *: "\<And>q. numeral (Num.Bit0 q) = 2 * numeral q"
718     "\<And>q. numeral (Num.Bit1 q) = 2 * numeral q + 1"
719     by (simp_all only: numeral_mult numeral.simps distrib) simp_all
720   have "1 div 2 = 0" "1 mod 2 = 1" by (auto intro: div_less mod_less)
721   then show ?P and ?Q
722     by (simp_all add: fst_divmod snd_divmod prod_eq_iff split_def * [of m] * [of n] mod_mult_mult1
723       div_mult2_eq [of _ _ 2] mod_mult2_eq [of _ _ 2]
724       add.commute del: numeral_times_numeral)
725 qed
727 text \<open>The really hard work\<close>
729 lemma divmod_steps [simp]:
730   "divmod (num.Bit0 m) (num.Bit1 n) =
731       (if m \<le> n then (0, numeral (num.Bit0 m))
732        else divmod_step (num.Bit1 n)
733              (divmod (num.Bit0 m)
734                (num.Bit0 (num.Bit1 n))))"
735   "divmod (num.Bit1 m) (num.Bit1 n) =
736       (if m < n then (0, numeral (num.Bit1 m))
737        else divmod_step (num.Bit1 n)
738              (divmod (num.Bit1 m)
739                (num.Bit0 (num.Bit1 n))))"
740   by (simp_all add: divmod_divmod_step)
742 lemmas divmod_algorithm_code = divmod_step_eq divmod_trivial divmod_cancel divmod_steps
744 text \<open>Special case: divisibility\<close>
746 definition divides_aux :: "'a \<times> 'a \<Rightarrow> bool"
747 where
748   "divides_aux qr \<longleftrightarrow> snd qr = 0"
750 lemma divides_aux_eq [simp]:
751   "divides_aux (q, r) \<longleftrightarrow> r = 0"
752   by (simp add: divides_aux_def)
754 lemma dvd_numeral_simp [simp]:
755   "numeral m dvd numeral n \<longleftrightarrow> divides_aux (divmod n m)"
756   by (simp add: divmod_def mod_eq_0_iff_dvd)
758 text \<open>Generic computation of quotient and remainder\<close>
760 lemma numeral_div_numeral [simp]:
761   "numeral k div numeral l = fst (divmod k l)"
762   by (simp add: fst_divmod)
764 lemma numeral_mod_numeral [simp]:
765   "numeral k mod numeral l = snd (divmod k l)"
766   by (simp add: snd_divmod)
768 lemma one_div_numeral [simp]:
769   "1 div numeral n = fst (divmod num.One n)"
770   by (simp add: fst_divmod)
772 lemma one_mod_numeral [simp]:
773   "1 mod numeral n = snd (divmod num.One n)"
774   by (simp add: snd_divmod)
776 text \<open>Computing congruences modulo \<open>2 ^ q\<close>\<close>
778 lemma cong_exp_iff_simps:
779   "numeral n mod numeral Num.One = 0
780     \<longleftrightarrow> True"
781   "numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) = 0
782     \<longleftrightarrow> numeral n mod numeral q = 0"
783   "numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) = 0
784     \<longleftrightarrow> False"
785   "numeral m mod numeral Num.One = (numeral n mod numeral Num.One)
786     \<longleftrightarrow> True"
787   "numeral Num.One mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
788     \<longleftrightarrow> True"
789   "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
790     \<longleftrightarrow> False"
791   "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
792     \<longleftrightarrow> (numeral n mod numeral q) = 0"
793   "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
794     \<longleftrightarrow> False"
795   "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
796     \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
797   "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
798     \<longleftrightarrow> False"
799   "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
800     \<longleftrightarrow> (numeral m mod numeral q) = 0"
801   "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
802     \<longleftrightarrow> False"
803   "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
804     \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
805   by (auto simp add: case_prod_beta dest: arg_cong [of _ _ even])
807 end
810 subsection \<open>Division on @{typ nat}\<close>
812 context
813 begin
815 text \<open>
816   We define @{const divide} and @{const modulo} on @{typ nat} by means
817   of a characteristic relation with two input arguments
818   @{term "m::nat"}, @{term "n::nat"} and two output arguments
819   @{term "q::nat"}(uotient) and @{term "r::nat"}(emainder).
820 \<close>
822 inductive eucl_rel_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool"
823   where eucl_rel_nat_by0: "eucl_rel_nat m 0 (0, m)"
824   | eucl_rel_natI: "r < n \<Longrightarrow> m = q * n + r \<Longrightarrow> eucl_rel_nat m n (q, r)"
826 text \<open>@{const eucl_rel_nat} is total:\<close>
828 qualified lemma eucl_rel_nat_ex:
829   obtains q r where "eucl_rel_nat m n (q, r)"
830 proof (cases "n = 0")
831   case True
832   with that eucl_rel_nat_by0 show thesis
833     by blast
834 next
835   case False
836   have "\<exists>q r. m = q * n + r \<and> r < n"
837   proof (induct m)
838     case 0 with \<open>n \<noteq> 0\<close>
839     have "(0::nat) = 0 * n + 0 \<and> 0 < n" by simp
840     then show ?case by blast
841   next
842     case (Suc m) then obtain q' r'
843       where m: "m = q' * n + r'" and n: "r' < n" by auto
844     then show ?case proof (cases "Suc r' < n")
845       case True
846       from m n have "Suc m = q' * n + Suc r'" by simp
847       with True show ?thesis by blast
848     next
849       case False then have "n \<le> Suc r'"
850         by (simp add: not_less)
851       moreover from n have "Suc r' \<le> n"
852         by (simp add: Suc_le_eq)
853       ultimately have "n = Suc r'" by auto
854       with m have "Suc m = Suc q' * n + 0" by simp
855       with \<open>n \<noteq> 0\<close> show ?thesis by blast
856     qed
857   qed
858   with that \<open>n \<noteq> 0\<close> eucl_rel_natI show thesis
859     by blast
860 qed
862 text \<open>@{const eucl_rel_nat} is injective:\<close>
864 qualified lemma eucl_rel_nat_unique_div:
865   assumes "eucl_rel_nat m n (q, r)"
866     and "eucl_rel_nat m n (q', r')"
867   shows "q = q'"
868 proof (cases "n = 0")
869   case True with assms show ?thesis
870     by (auto elim: eucl_rel_nat.cases)
871 next
872   case False
873   have *: "q' \<le> q" if "q' * n + r' = q * n + r" "r < n" for q r q' r' :: nat
874   proof (rule ccontr)
875     assume "\<not> q' \<le> q"
876     then have "q < q'"
877       by (simp add: not_le)
878     with that show False
879       by (auto simp add: less_iff_Suc_add algebra_simps)
880   qed
881   from \<open>n \<noteq> 0\<close> assms show ?thesis
882     by (auto intro: order_antisym elim: eucl_rel_nat.cases dest: * sym split: if_splits)
883 qed
885 qualified lemma eucl_rel_nat_unique_mod:
886   assumes "eucl_rel_nat m n (q, r)"
887     and "eucl_rel_nat m n (q', r')"
888   shows "r = r'"
889 proof -
890   from assms have "q' = q"
891     by (auto intro: eucl_rel_nat_unique_div)
892   with assms show ?thesis
893     by (auto elim!: eucl_rel_nat.cases)
894 qed
896 text \<open>
897   We instantiate divisibility on the natural numbers by
898   means of @{const eucl_rel_nat}:
899 \<close>
901 qualified definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
902   "divmod_nat m n = (THE qr. eucl_rel_nat m n qr)"
904 qualified lemma eucl_rel_nat_divmod_nat:
905   "eucl_rel_nat m n (divmod_nat m n)"
906 proof -
907   from eucl_rel_nat_ex
908     obtain q r where rel: "eucl_rel_nat m n (q, r)" .
909   then show ?thesis
910     by (auto simp add: divmod_nat_def intro: theI
911       elim: eucl_rel_nat_unique_div eucl_rel_nat_unique_mod)
912 qed
914 qualified lemma divmod_nat_unique:
915   "divmod_nat m n = (q, r)" if "eucl_rel_nat m n (q, r)"
916   using that
917   by (auto simp add: divmod_nat_def intro: eucl_rel_nat_divmod_nat elim: eucl_rel_nat_unique_div eucl_rel_nat_unique_mod)
919 qualified lemma divmod_nat_zero:
920   "divmod_nat m 0 = (0, m)"
921   by (rule divmod_nat_unique) (fact eucl_rel_nat_by0)
923 qualified lemma divmod_nat_zero_left:
924   "divmod_nat 0 n = (0, 0)"
925   by (rule divmod_nat_unique)
926     (cases n, auto intro: eucl_rel_nat_by0 eucl_rel_natI)
928 qualified lemma divmod_nat_base:
929   "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
930   by (rule divmod_nat_unique)
931     (cases n, auto intro: eucl_rel_nat_by0 eucl_rel_natI)
933 qualified lemma divmod_nat_step:
934   assumes "0 < n" and "n \<le> m"
935   shows "divmod_nat m n =
936     (Suc (fst (divmod_nat (m - n) n)), snd (divmod_nat (m - n) n))"
937 proof (rule divmod_nat_unique)
938   have "eucl_rel_nat (m - n) n (divmod_nat (m - n) n)"
939     by (fact eucl_rel_nat_divmod_nat)
940   then show "eucl_rel_nat m n (Suc
941     (fst (divmod_nat (m - n) n)), snd (divmod_nat (m - n) n))"
942     using assms
943       by (auto split: if_splits intro: eucl_rel_natI elim!: eucl_rel_nat.cases simp add: algebra_simps)
944 qed
946 end
948 instantiation nat :: "{semidom_modulo, normalization_semidom}"
949 begin
951 definition normalize_nat :: "nat \<Rightarrow> nat"
952   where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
954 definition unit_factor_nat :: "nat \<Rightarrow> nat"
955   where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
957 lemma unit_factor_simps [simp]:
958   "unit_factor 0 = (0::nat)"
959   "unit_factor (Suc n) = 1"
960   by (simp_all add: unit_factor_nat_def)
962 definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
963   where div_nat_def: "m div n = fst (Divides.divmod_nat m n)"
965 definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
966   where mod_nat_def: "m mod n = snd (Divides.divmod_nat m n)"
968 lemma fst_divmod_nat [simp]:
969   "fst (Divides.divmod_nat m n) = m div n"
970   by (simp add: div_nat_def)
972 lemma snd_divmod_nat [simp]:
973   "snd (Divides.divmod_nat m n) = m mod n"
974   by (simp add: mod_nat_def)
976 lemma divmod_nat_div_mod:
977   "Divides.divmod_nat m n = (m div n, m mod n)"
978   by (simp add: prod_eq_iff)
980 lemma div_nat_unique:
981   assumes "eucl_rel_nat m n (q, r)"
982   shows "m div n = q"
983   using assms
984   by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
986 lemma mod_nat_unique:
987   assumes "eucl_rel_nat m n (q, r)"
988   shows "m mod n = r"
989   using assms
990   by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
992 lemma eucl_rel_nat: "eucl_rel_nat m n (m div n, m mod n)"
993   using Divides.eucl_rel_nat_divmod_nat
994   by (simp add: divmod_nat_div_mod)
996 text \<open>The ''recursion'' equations for @{const divide} and @{const modulo}\<close>
998 lemma div_less [simp]:
999   fixes m n :: nat
1000   assumes "m < n"
1001   shows "m div n = 0"
1002   using assms Divides.divmod_nat_base by (simp add: prod_eq_iff)
1004 lemma le_div_geq:
1005   fixes m n :: nat
1006   assumes "0 < n" and "n \<le> m"
1007   shows "m div n = Suc ((m - n) div n)"
1008   using assms Divides.divmod_nat_step by (simp add: prod_eq_iff)
1010 lemma mod_less [simp]:
1011   fixes m n :: nat
1012   assumes "m < n"
1013   shows "m mod n = m"
1014   using assms Divides.divmod_nat_base by (simp add: prod_eq_iff)
1016 lemma le_mod_geq:
1017   fixes m n :: nat
1018   assumes "n \<le> m"
1019   shows "m mod n = (m - n) mod n"
1020   using assms Divides.divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff)
1022 lemma mod_less_divisor [simp]:
1023   fixes m n :: nat
1024   assumes "n > 0"
1025   shows "m mod n < n"
1026   using assms eucl_rel_nat [of m n]
1027     by (auto elim: eucl_rel_nat.cases)
1029 lemma mod_le_divisor [simp]:
1030   fixes m n :: nat
1031   assumes "n > 0"
1032   shows "m mod n \<le> n"
1033   using assms eucl_rel_nat [of m n]
1034     by (auto elim: eucl_rel_nat.cases)
1036 instance proof
1037   fix m n :: nat
1038   show "m div n * n + m mod n = m"
1039     using eucl_rel_nat [of m n]
1040     by (auto elim: eucl_rel_nat.cases)
1041 next
1042   fix n :: nat show "n div 0 = 0"
1043     by (simp add: div_nat_def Divides.divmod_nat_zero)
1044 next
1045   fix m n :: nat
1046   assume "n \<noteq> 0"
1047   then show "m * n div n = m"
1048     by (auto intro!: eucl_rel_natI div_nat_unique [of _ _ _ 0])
1049 qed (simp_all add: unit_factor_nat_def)
1051 end
1053 instance nat :: semiring_div
1054 proof
1055   fix m n q :: nat
1056   assume "n \<noteq> 0"
1057   then show "(q + m * n) div n = m + q div n"
1058     by (induct m) (simp_all add: le_div_geq)
1059 next
1060   fix m n q :: nat
1061   assume "m \<noteq> 0"
1062   show "(m * n) div (m * q) = n div q"
1063   proof (cases "q = 0")
1064     case True
1065     then show ?thesis
1066       by simp
1067   next
1068     case False
1069     show ?thesis
1070     proof (rule div_nat_unique [of _ _ _ "m * (n mod q)"])
1071       show "eucl_rel_nat (m * n) (m * q) (n div q, m * (n mod q))"
1072         by (rule eucl_rel_natI)
1073           (use \<open>m \<noteq> 0\<close> \<open>q \<noteq> 0\<close> div_mult_mod_eq [of n q] in \<open>auto simp add: algebra_simps distrib_left [symmetric]\<close>)
1074     qed
1075   qed
1076 qed
1078 lemma div_by_Suc_0 [simp]:
1079   "m div Suc 0 = m"
1080   using div_by_1 [of m] by simp
1082 lemma mod_by_Suc_0 [simp]:
1083   "m mod Suc 0 = 0"
1084   using mod_by_1 [of m] by simp
1086 lemma mod_greater_zero_iff_not_dvd:
1087   fixes m n :: nat
1088   shows "m mod n > 0 \<longleftrightarrow> \<not> n dvd m"
1089   by (simp add: dvd_eq_mod_eq_0)
1091 instantiation nat :: unique_euclidean_semiring
1092 begin
1094 definition [simp]:
1095   "euclidean_size_nat = (id :: nat \<Rightarrow> nat)"
1097 definition [simp]:
1098   "uniqueness_constraint_nat = (top :: nat \<Rightarrow> nat \<Rightarrow> bool)"
1100 instance
1101   by standard (use mult_le_mono2 [of 1] in \<open>simp_all add: unit_factor_nat_def mod_greater_zero_iff_not_dvd\<close>)
1103 end
1105 text \<open>Simproc for cancelling @{const divide} and @{const modulo}\<close>
1107 lemma (in semiring_modulo) cancel_div_mod_rules:
1108   "((a div b) * b + a mod b) + c = a + c"
1109   "(b * (a div b) + a mod b) + c = a + c"
1110   by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
1112 ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
1114 ML \<open>
1115 structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
1116 (
1117   val div_name = @{const_name divide};
1118   val mod_name = @{const_name modulo};
1119   val mk_binop = HOLogic.mk_binop;
1120   val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
1121   val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
1122   fun mk_sum [] = HOLogic.zero
1123     | mk_sum [t] = t
1124     | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
1125   fun dest_sum tm =
1126     if HOLogic.is_zero tm then []
1127     else
1128       (case try HOLogic.dest_Suc tm of
1129         SOME t => HOLogic.Suc_zero :: dest_sum t
1130       | NONE =>
1131           (case try dest_plus tm of
1132             SOME (t, u) => dest_sum t @ dest_sum u
1133           | NONE => [tm]));
1135   val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
1137   val prove_eq_sums = Arith_Data.prove_conv2 all_tac
1138     (Arith_Data.simp_all_tac @{thms add_0_left add_0_right ac_simps})
1139 )
1140 \<close>
1142 simproc_setup cancel_div_mod_nat ("(m::nat) + n") =
1143   \<open>K Cancel_Div_Mod_Nat.proc\<close>
1145 lemma divmod_nat_if [code]:
1146   "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
1147     let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
1148   by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
1150 lemma mod_Suc_eq [mod_simps]:
1151   "Suc (m mod n) mod n = Suc m mod n"
1152 proof -
1153   have "(m mod n + 1) mod n = (m + 1) mod n"
1154     by (simp only: mod_simps)
1155   then show ?thesis
1156     by simp
1157 qed
1159 lemma mod_Suc_Suc_eq [mod_simps]:
1160   "Suc (Suc (m mod n)) mod n = Suc (Suc m) mod n"
1161 proof -
1162   have "(m mod n + 2) mod n = (m + 2) mod n"
1163     by (simp only: mod_simps)
1164   then show ?thesis
1165     by simp
1166 qed
1169 subsubsection \<open>Quotient\<close>
1171 lemma div_geq: "0 < n \<Longrightarrow>  \<not> m < n \<Longrightarrow> m div n = Suc ((m - n) div n)"
1172 by (simp add: le_div_geq linorder_not_less)
1174 lemma div_if: "0 < n \<Longrightarrow> m div n = (if m < n then 0 else Suc ((m - n) div n))"
1175 by (simp add: div_geq)
1177 lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
1178 by simp
1180 lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"
1181 by simp
1183 lemma div_positive:
1184   fixes m n :: nat
1185   assumes "n > 0"
1186   assumes "m \<ge> n"
1187   shows "m div n > 0"
1188 proof -
1189   from \<open>m \<ge> n\<close> obtain q where "m = n + q"
1190     by (auto simp add: le_iff_add)
1191   with \<open>n > 0\<close> show ?thesis by (simp add: div_add_self1)
1192 qed
1194 lemma div_eq_0_iff: "(a div b::nat) = 0 \<longleftrightarrow> a < b \<or> b = 0"
1195   by auto (metis div_positive less_numeral_extra(3) not_less)
1198 subsubsection \<open>Remainder\<close>
1200 lemma mod_Suc_le_divisor [simp]:
1201   "m mod Suc n \<le> n"
1202   using mod_less_divisor [of "Suc n" m] by arith
1204 lemma mod_less_eq_dividend [simp]:
1205   fixes m n :: nat
1206   shows "m mod n \<le> m"
1207 proof (rule add_leD2)
1208   from div_mult_mod_eq have "m div n * n + m mod n = m" .
1209   then show "m div n * n + m mod n \<le> m" by auto
1210 qed
1212 lemma mod_geq: "\<not> m < (n::nat) \<Longrightarrow> m mod n = (m - n) mod n"
1213 by (simp add: le_mod_geq linorder_not_less)
1215 lemma mod_if: "m mod (n::nat) = (if m < n then m else (m - n) mod n)"
1216 by (simp add: le_mod_geq)
1219 subsubsection \<open>Quotient and Remainder\<close>
1221 lemma div_mult1_eq:
1222   "(a * b) div c = a * (b div c) + a * (b mod c) div (c::nat)"
1223   by (cases "c = 0")
1224      (auto simp add: algebra_simps distrib_left [symmetric]
1225      intro!: div_nat_unique [of _ _ _ "(a * (b mod c)) mod c"] eucl_rel_natI)
1227 lemma eucl_rel_nat_add1_eq:
1228   "eucl_rel_nat a c (aq, ar) \<Longrightarrow> eucl_rel_nat b c (bq, br)
1229    \<Longrightarrow> eucl_rel_nat (a + b) c (aq + bq + (ar + br) div c, (ar + br) mod c)"
1230   by (auto simp add: split_ifs algebra_simps elim!: eucl_rel_nat.cases intro: eucl_rel_nat_by0 eucl_rel_natI)
1232 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
1233 lemma div_add1_eq:
1234   "(a + b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
1235 by (blast intro: eucl_rel_nat_add1_eq [THEN div_nat_unique] eucl_rel_nat)
1237 lemma eucl_rel_nat_mult2_eq:
1238   assumes "eucl_rel_nat a b (q, r)"
1239   shows "eucl_rel_nat a (b * c) (q div c, b *(q mod c) + r)"
1240 proof (cases "c = 0")
1241   case True
1242   with assms show ?thesis
1243     by (auto intro: eucl_rel_nat_by0 elim!: eucl_rel_nat.cases simp add: ac_simps)
1244 next
1245   case False
1246   { assume "r < b"
1247     with False have "b * (q mod c) + r < b * c"
1248       apply (cut_tac m = q and n = c in mod_less_divisor)
1249       apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
1250       apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)
1251       apply (simp add: add_mult_distrib2)
1252       done
1253     then have "r + b * (q mod c) < b * c"
1254       by (simp add: ac_simps)
1255   } with assms False show ?thesis
1256     by (auto simp add: algebra_simps add_mult_distrib2 [symmetric] elim!: eucl_rel_nat.cases intro: eucl_rel_nat.intros)
1257 qed
1259 lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)"
1260 by (force simp add: eucl_rel_nat [THEN eucl_rel_nat_mult2_eq, THEN div_nat_unique])
1262 lemma mod_mult2_eq: "a mod (b * c) = b * (a div b mod c) + a mod (b::nat)"
1263 by (auto simp add: mult.commute eucl_rel_nat [THEN eucl_rel_nat_mult2_eq, THEN mod_nat_unique])
1265 instantiation nat :: semiring_numeral_div
1266 begin
1268 definition divmod_nat :: "num \<Rightarrow> num \<Rightarrow> nat \<times> nat"
1269 where
1270   divmod'_nat_def: "divmod_nat m n = (numeral m div numeral n, numeral m mod numeral n)"
1272 definition divmod_step_nat :: "num \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
1273 where
1274   "divmod_step_nat l qr = (let (q, r) = qr
1275     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
1276     else (2 * q, r))"
1278 instance
1279   by standard (auto intro: div_positive simp add: divmod'_nat_def divmod_step_nat_def mod_mult2_eq div_mult2_eq)
1281 end
1283 declare divmod_algorithm_code [where ?'a = nat, code]
1286 subsubsection \<open>Further Facts about Quotient and Remainder\<close>
1288 lemma div_le_mono:
1289   fixes m n k :: nat
1290   assumes "m \<le> n"
1291   shows "m div k \<le> n div k"
1292 proof -
1293   from assms obtain q where "n = m + q"
1294     by (auto simp add: le_iff_add)
1295   then show ?thesis
1296     by (simp add: div_add1_eq [of m q k])
1297 qed
1299 (* Antimonotonicity of div in second argument *)
1300 lemma div_le_mono2: "!!m::nat. [| 0<m; m\<le>n |] ==> (k div n) \<le> (k div m)"
1301 apply (subgoal_tac "0<n")
1302  prefer 2 apply simp
1303 apply (induct_tac k rule: nat_less_induct)
1304 apply (rename_tac "k")
1305 apply (case_tac "k<n", simp)
1306 apply (subgoal_tac "~ (k<m) ")
1307  prefer 2 apply simp
1308 apply (simp add: div_geq)
1309 apply (subgoal_tac "(k-n) div n \<le> (k-m) div n")
1310  prefer 2
1311  apply (blast intro: div_le_mono diff_le_mono2)
1312 apply (rule le_trans, simp)
1313 apply (simp)
1314 done
1316 lemma div_le_dividend [simp]: "m div n \<le> (m::nat)"
1317 apply (case_tac "n=0", simp)
1318 apply (subgoal_tac "m div n \<le> m div 1", simp)
1319 apply (rule div_le_mono2)
1320 apply (simp_all (no_asm_simp))
1321 done
1323 (* Similar for "less than" *)
1324 lemma div_less_dividend [simp]:
1325   "\<lbrakk>(1::nat) < n; 0 < m\<rbrakk> \<Longrightarrow> m div n < m"
1326 apply (induct m rule: nat_less_induct)
1327 apply (rename_tac "m")
1328 apply (case_tac "m<n", simp)
1329 apply (subgoal_tac "0<n")
1330  prefer 2 apply simp
1331 apply (simp add: div_geq)
1332 apply (case_tac "n<m")
1333  apply (subgoal_tac "(m-n) div n < (m-n) ")
1334   apply (rule impI less_trans_Suc)+
1335 apply assumption
1336   apply (simp_all)
1337 done
1339 text\<open>A fact for the mutilated chess board\<close>
1340 lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"
1341 apply (case_tac "n=0", simp)
1342 apply (induct "m" rule: nat_less_induct)
1343 apply (case_tac "Suc (na) <n")
1344 (* case Suc(na) < n *)
1345 apply (frule lessI [THEN less_trans], simp add: less_not_refl3)
1346 (* case n \<le> Suc(na) *)
1347 apply (simp add: linorder_not_less le_Suc_eq mod_geq)
1348 apply (auto simp add: Suc_diff_le le_mod_geq)
1349 done
1351 lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
1352 by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
1354 lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]
1356 (*Loses information, namely we also have r<d provided d is nonzero*)
1357 lemma mod_eqD:
1358   fixes m d r q :: nat
1359   assumes "m mod d = r"
1360   shows "\<exists>q. m = r + q * d"
1361 proof -
1362   from div_mult_mod_eq obtain q where "q * d + m mod d = m" by blast
1363   with assms have "m = r + q * d" by simp
1364   then show ?thesis ..
1365 qed
1367 lemma split_div:
1368  "P(n div k :: nat) =
1369  ((k = 0 \<longrightarrow> P 0) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P i)))"
1370  (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
1371 proof
1372   assume P: ?P
1373   show ?Q
1374   proof (cases)
1375     assume "k = 0"
1376     with P show ?Q by simp
1377   next
1378     assume not0: "k \<noteq> 0"
1379     thus ?Q
1380     proof (simp, intro allI impI)
1381       fix i j
1382       assume n: "n = k*i + j" and j: "j < k"
1383       show "P i"
1384       proof (cases)
1385         assume "i = 0"
1386         with n j P show "P i" by simp
1387       next
1388         assume "i \<noteq> 0"
1389         with not0 n j P show "P i" by(simp add:ac_simps)
1390       qed
1391     qed
1392   qed
1393 next
1394   assume Q: ?Q
1395   show ?P
1396   proof (cases)
1397     assume "k = 0"
1398     with Q show ?P by simp
1399   next
1400     assume not0: "k \<noteq> 0"
1401     with Q have R: ?R by simp
1402     from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
1403     show ?P by simp
1404   qed
1405 qed
1407 lemma split_div_lemma:
1408   assumes "0 < n"
1409   shows "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> q = ((m::nat) div n)" (is "?lhs \<longleftrightarrow> ?rhs")
1410 proof
1411   assume ?rhs
1412   with minus_mod_eq_mult_div [symmetric] have nq: "n * q = m - (m mod n)" by simp
1413   then have A: "n * q \<le> m" by simp
1414   have "n - (m mod n) > 0" using mod_less_divisor assms by auto
1415   then have "m < m + (n - (m mod n))" by simp
1416   then have "m < n + (m - (m mod n))" by simp
1417   with nq have "m < n + n * q" by simp
1418   then have B: "m < n * Suc q" by simp
1419   from A B show ?lhs ..
1420 next
1421   assume P: ?lhs
1422   then have "eucl_rel_nat m n (q, m - n * q)"
1423     by (auto intro: eucl_rel_natI simp add: ac_simps)
1424   then have "m div n = q"
1425     by (rule div_nat_unique)
1426   then show ?rhs by simp
1427 qed
1429 theorem split_div':
1430   "P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or>
1431    (\<exists>q. (n * q \<le> m \<and> m < n * (Suc q)) \<and> P q))"
1432   apply (cases "0 < n")
1433   apply (simp only: add: split_div_lemma)
1434   apply simp_all
1435   done
1437 lemma split_mod:
1438  "P(n mod k :: nat) =
1439  ((k = 0 \<longrightarrow> P n) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P j)))"
1440  (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
1441 proof
1442   assume P: ?P
1443   show ?Q
1444   proof (cases)
1445     assume "k = 0"
1446     with P show ?Q by simp
1447   next
1448     assume not0: "k \<noteq> 0"
1449     thus ?Q
1450     proof (simp, intro allI impI)
1451       fix i j
1452       assume "n = k*i + j" "j < k"
1453       thus "P j" using not0 P by (simp add: ac_simps)
1454     qed
1455   qed
1456 next
1457   assume Q: ?Q
1458   show ?P
1459   proof (cases)
1460     assume "k = 0"
1461     with Q show ?P by simp
1462   next
1463     assume not0: "k \<noteq> 0"
1464     with Q have R: ?R by simp
1465     from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
1466     show ?P by simp
1467   qed
1468 qed
1470 lemma div_eq_dividend_iff: "a \<noteq> 0 \<Longrightarrow> (a :: nat) div b = a \<longleftrightarrow> b = 1"
1471   apply rule
1472   apply (cases "b = 0")
1473   apply simp_all
1474   apply (metis (full_types) One_nat_def Suc_lessI div_less_dividend less_not_refl3)
1475   done
1477 lemma (in field_char_0) of_nat_div:
1478   "of_nat (m div n) = ((of_nat m - of_nat (m mod n)) / of_nat n)"
1479 proof -
1480   have "of_nat (m div n) = ((of_nat (m div n * n + m mod n) - of_nat (m mod n)) / of_nat n :: 'a)"
1481     unfolding of_nat_add by (cases "n = 0") simp_all
1482   then show ?thesis
1483     by simp
1484 qed
1487 subsubsection \<open>An ``induction'' law for modulus arithmetic.\<close>
1489 lemma mod_induct_0:
1490   assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
1491   and base: "P i" and i: "i<p"
1492   shows "P 0"
1493 proof (rule ccontr)
1494   assume contra: "\<not>(P 0)"
1495   from i have p: "0<p" by simp
1496   have "\<forall>k. 0<k \<longrightarrow> \<not> P (p-k)" (is "\<forall>k. ?A k")
1497   proof
1498     fix k
1499     show "?A k"
1500     proof (induct k)
1501       show "?A 0" by simp  \<comment> "by contradiction"
1502     next
1503       fix n
1504       assume ih: "?A n"
1505       show "?A (Suc n)"
1506       proof (clarsimp)
1507         assume y: "P (p - Suc n)"
1508         have n: "Suc n < p"
1509         proof (rule ccontr)
1510           assume "\<not>(Suc n < p)"
1511           hence "p - Suc n = 0"
1512             by simp
1513           with y contra show "False"
1514             by simp
1515         qed
1516         hence n2: "Suc (p - Suc n) = p-n" by arith
1517         from p have "p - Suc n < p" by arith
1518         with y step have z: "P ((Suc (p - Suc n)) mod p)"
1519           by blast
1520         show "False"
1521         proof (cases "n=0")
1522           case True
1523           with z n2 contra show ?thesis by simp
1524         next
1525           case False
1526           with p have "p-n < p" by arith
1527           with z n2 False ih show ?thesis by simp
1528         qed
1529       qed
1530     qed
1531   qed
1532   moreover
1533   from i obtain k where "0<k \<and> i+k=p"
1534     by (blast dest: less_imp_add_positive)
1535   hence "0<k \<and> i=p-k" by auto
1536   moreover
1537   note base
1538   ultimately
1539   show "False" by blast
1540 qed
1542 lemma mod_induct:
1543   assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
1544   and base: "P i" and i: "i<p" and j: "j<p"
1545   shows "P j"
1546 proof -
1547   have "\<forall>j<p. P j"
1548   proof
1549     fix j
1550     show "j<p \<longrightarrow> P j" (is "?A j")
1551     proof (induct j)
1552       from step base i show "?A 0"
1553         by (auto elim: mod_induct_0)
1554     next
1555       fix k
1556       assume ih: "?A k"
1557       show "?A (Suc k)"
1558       proof
1559         assume suc: "Suc k < p"
1560         hence k: "k<p" by simp
1561         with ih have "P k" ..
1562         with step k have "P (Suc k mod p)"
1563           by blast
1564         moreover
1565         from suc have "Suc k mod p = Suc k"
1566           by simp
1567         ultimately
1568         show "P (Suc k)" by simp
1569       qed
1570     qed
1571   qed
1572   with j show ?thesis by blast
1573 qed
1575 lemma div2_Suc_Suc [simp]: "Suc (Suc m) div 2 = Suc (m div 2)"
1576   by (simp add: numeral_2_eq_2 le_div_geq)
1578 lemma mod2_Suc_Suc [simp]: "Suc (Suc m) mod 2 = m mod 2"
1579   by (simp add: numeral_2_eq_2 le_mod_geq)
1581 lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
1582 by (simp add: mult_2 [symmetric])
1584 lemma mod2_gr_0 [simp]: "0 < (m::nat) mod 2 \<longleftrightarrow> m mod 2 = 1"
1585 proof -
1586   { fix n :: nat have  "(n::nat) < 2 \<Longrightarrow> n = 0 \<or> n = 1" by (cases n) simp_all }
1587   moreover have "m mod 2 < 2" by simp
1588   ultimately have "m mod 2 = 0 \<or> m mod 2 = 1" .
1589   then show ?thesis by auto
1590 qed
1592 text\<open>These lemmas collapse some needless occurrences of Suc:
1593     at least three Sucs, since two and fewer are rewritten back to Suc again!
1594     We already have some rules to simplify operands smaller than 3.\<close>
1596 lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
1597 by (simp add: Suc3_eq_add_3)
1599 lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
1600 by (simp add: Suc3_eq_add_3)
1602 lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
1603 by (simp add: Suc3_eq_add_3)
1605 lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
1606 by (simp add: Suc3_eq_add_3)
1608 lemmas Suc_div_eq_add3_div_numeral [simp] = Suc_div_eq_add3_div [of _ "numeral v"] for v
1609 lemmas Suc_mod_eq_add3_mod_numeral [simp] = Suc_mod_eq_add3_mod [of _ "numeral v"] for v
1611 lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1"
1612 apply (induct "m")
1613 apply (simp_all add: mod_Suc)
1614 done
1616 declare Suc_times_mod_eq [of "numeral w", simp] for w
1618 lemma Suc_div_le_mono [simp]: "n div k \<le> (Suc n) div k"
1619 by (simp add: div_le_mono)
1621 lemma Suc_n_div_2_gt_zero [simp]: "(0::nat) < n ==> 0 < (n + 1) div 2"
1622 by (cases n) simp_all
1624 lemma div_2_gt_zero [simp]: assumes A: "(1::nat) < n" shows "0 < n div 2"
1625 proof -
1626   from A have B: "0 < n - 1" and C: "n - 1 + 1 = n" by simp_all
1627   from Suc_n_div_2_gt_zero [OF B] C show ?thesis by simp
1628 qed
1630 lemma mod_mult_self3' [simp]: "Suc (k * n + m) mod n = Suc m mod n"
1631   using mod_mult_self3 [of k n "Suc m"] by simp
1633 lemma mod_Suc_eq_Suc_mod: "Suc m mod n = Suc (m mod n) mod n"
1634 apply (subst mod_Suc [of m])
1635 apply (subst mod_Suc [of "m mod n"], simp)
1636 done
1638 lemma mod_2_not_eq_zero_eq_one_nat:
1639   fixes n :: nat
1640   shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
1641   by (fact not_mod_2_eq_0_eq_1)
1643 lemma even_Suc_div_two [simp]:
1644   "even n \<Longrightarrow> Suc n div 2 = n div 2"
1645   using even_succ_div_two [of n] by simp
1647 lemma odd_Suc_div_two [simp]:
1648   "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
1649   using odd_succ_div_two [of n] by simp
1651 lemma odd_two_times_div_two_nat [simp]:
1652   assumes "odd n"
1653   shows "2 * (n div 2) = n - (1 :: nat)"
1654 proof -
1655   from assms have "2 * (n div 2) + 1 = n"
1656     by (rule odd_two_times_div_two_succ)
1657   then have "Suc (2 * (n div 2)) - 1 = n - 1"
1658     by simp
1659   then show ?thesis
1660     by simp
1661 qed
1663 lemma parity_induct [case_names zero even odd]:
1664   assumes zero: "P 0"
1665   assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
1666   assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
1667   shows "P n"
1668 proof (induct n rule: less_induct)
1669   case (less n)
1670   show "P n"
1671   proof (cases "n = 0")
1672     case True with zero show ?thesis by simp
1673   next
1674     case False
1675     with less have hyp: "P (n div 2)" by simp
1676     show ?thesis
1677     proof (cases "even n")
1678       case True
1679       with hyp even [of "n div 2"] show ?thesis
1680         by simp
1681     next
1682       case False
1683       with hyp odd [of "n div 2"] show ?thesis
1684         by simp
1685     qed
1686   qed
1687 qed
1689 lemma Suc_0_div_numeral [simp]:
1690   fixes k l :: num
1691   shows "Suc 0 div numeral k = fst (divmod Num.One k)"
1692   by (simp_all add: fst_divmod)
1694 lemma Suc_0_mod_numeral [simp]:
1695   fixes k l :: num
1696   shows "Suc 0 mod numeral k = snd (divmod Num.One k)"
1697   by (simp_all add: snd_divmod)
1700 subsection \<open>Division on @{typ int}\<close>
1702 context
1703 begin
1705 inductive eucl_rel_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool"
1706   where eucl_rel_int_by0: "eucl_rel_int k 0 (0, k)"
1707   | eucl_rel_int_dividesI: "l \<noteq> 0 \<Longrightarrow> k = q * l \<Longrightarrow> eucl_rel_int k l (q, 0)"
1708   | eucl_rel_int_remainderI: "sgn r = sgn l \<Longrightarrow> \<bar>r\<bar> < \<bar>l\<bar>
1709       \<Longrightarrow> k = q * l + r \<Longrightarrow> eucl_rel_int k l (q, r)"
1711 lemma eucl_rel_int_iff:
1712   "eucl_rel_int k l (q, r) \<longleftrightarrow>
1713     k = l * q + r \<and>
1714      (if 0 < l then 0 \<le> r \<and> r < l else if l < 0 then l < r \<and> r \<le> 0 else q = 0)"
1715   by (cases "r = 0")
1716     (auto elim!: eucl_rel_int.cases intro: eucl_rel_int_by0 eucl_rel_int_dividesI eucl_rel_int_remainderI
1717     simp add: ac_simps sgn_1_pos sgn_1_neg)
1719 lemma unique_quotient_lemma:
1720   "b * q' + r' \<le> b * q + r \<Longrightarrow> 0 \<le> r' \<Longrightarrow> r' < b \<Longrightarrow> r < b \<Longrightarrow> q' \<le> (q::int)"
1721 apply (subgoal_tac "r' + b * (q'-q) \<le> r")
1722  prefer 2 apply (simp add: right_diff_distrib)
1723 apply (subgoal_tac "0 < b * (1 + q - q') ")
1724 apply (erule_tac [2] order_le_less_trans)
1725  prefer 2 apply (simp add: right_diff_distrib distrib_left)
1726 apply (subgoal_tac "b * q' < b * (1 + q) ")
1727  prefer 2 apply (simp add: right_diff_distrib distrib_left)
1728 apply (simp add: mult_less_cancel_left)
1729 done
1731 lemma unique_quotient_lemma_neg:
1732   "b * q' + r' \<le> b*q + r \<Longrightarrow> r \<le> 0 \<Longrightarrow> b < r \<Longrightarrow> b < r' \<Longrightarrow> q \<le> (q'::int)"
1733   by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma) auto
1735 lemma unique_quotient:
1736   "eucl_rel_int a b (q, r) \<Longrightarrow> eucl_rel_int a b (q', r') \<Longrightarrow> q = q'"
1737   apply (simp add: eucl_rel_int_iff linorder_neq_iff split: if_split_asm)
1738   apply (blast intro: order_antisym
1739     dest: order_eq_refl [THEN unique_quotient_lemma]
1740     order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
1741   done
1743 lemma unique_remainder:
1744   "eucl_rel_int a b (q, r) \<Longrightarrow> eucl_rel_int a b (q', r') \<Longrightarrow> r = r'"
1745 apply (subgoal_tac "q = q'")
1746  apply (simp add: eucl_rel_int_iff)
1747 apply (blast intro: unique_quotient)
1748 done
1750 end
1752 instantiation int :: "{idom_modulo, normalization_semidom}"
1753 begin
1755 definition normalize_int :: "int \<Rightarrow> int"
1756   where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
1758 definition unit_factor_int :: "int \<Rightarrow> int"
1759   where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
1761 definition divide_int :: "int \<Rightarrow> int \<Rightarrow> int"
1762   where "k div l = (if l = 0 \<or> k = 0 then 0
1763     else if k > 0 \<and> l > 0 \<or> k < 0 \<and> l < 0
1764       then int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
1765       else
1766         if l dvd k then - int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
1767         else - int (Suc (nat \<bar>k\<bar> div nat \<bar>l\<bar>)))"
1769 definition modulo_int :: "int \<Rightarrow> int \<Rightarrow> int"
1770   where "k mod l = (if l = 0 then k else if l dvd k then 0
1771     else if k > 0 \<and> l > 0 \<or> k < 0 \<and> l < 0
1772       then sgn l * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)
1773       else sgn l * (\<bar>l\<bar> - int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)))"
1775 lemma eucl_rel_int:
1776   "eucl_rel_int k l (k div l, k mod l)"
1777 proof (cases k rule: int_cases3)
1778   case zero
1779   then show ?thesis
1780     by (simp add: eucl_rel_int_iff divide_int_def modulo_int_def)
1781 next
1782   case (pos n)
1783   then show ?thesis
1784     using div_mult_mod_eq [of n]
1785     by (cases l rule: int_cases3)
1786       (auto simp del: of_nat_mult of_nat_add
1787         simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
1788         eucl_rel_int_iff divide_int_def modulo_int_def int_dvd_iff)
1789 next
1790   case (neg n)
1791   then show ?thesis
1792     using div_mult_mod_eq [of n]
1793     by (cases l rule: int_cases3)
1794       (auto simp del: of_nat_mult of_nat_add
1795         simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
1796         eucl_rel_int_iff divide_int_def modulo_int_def int_dvd_iff)
1797 qed
1799 lemma divmod_int_unique:
1800   assumes "eucl_rel_int k l (q, r)"
1801   shows div_int_unique: "k div l = q" and mod_int_unique: "k mod l = r"
1802   using assms eucl_rel_int [of k l]
1803   using unique_quotient [of k l] unique_remainder [of k l]
1804   by auto
1806 instance proof
1807   fix k l :: int
1808   show "k div l * l + k mod l = k"
1809     using eucl_rel_int [of k l]
1810     unfolding eucl_rel_int_iff by (simp add: ac_simps)
1811 next
1812   fix k :: int show "k div 0 = 0"
1813     by (rule div_int_unique, simp add: eucl_rel_int_iff)
1814 next
1815   fix k l :: int
1816   assume "l \<noteq> 0"
1817   then show "k * l div l = k"
1818     by (auto simp add: eucl_rel_int_iff ac_simps intro: div_int_unique [of _ _ _ 0])
1819 qed (auto simp add: sgn_mult mult_sgn_abs abs_eq_iff')
1821 end
1823 lemma is_unit_int:
1824   "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
1825   by auto
1827 lemma zdiv_int:
1828   "int (a div b) = int a div int b"
1829   by (simp add: divide_int_def)
1831 lemma zmod_int:
1832   "int (a mod b) = int a mod int b"
1833   by (simp add: modulo_int_def int_dvd_iff)
1835 lemma div_abs_eq_div_nat:
1836   "\<bar>k\<bar> div \<bar>l\<bar> = int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)"
1837   by (simp add: divide_int_def)
1839 lemma mod_abs_eq_div_nat:
1840   "\<bar>k\<bar> mod \<bar>l\<bar> = int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)"
1841   by (simp add: modulo_int_def dvd_int_unfold_dvd_nat)
1843 lemma div_sgn_abs_cancel:
1844   fixes k l v :: int
1845   assumes "v \<noteq> 0"
1846   shows "(sgn v * \<bar>k\<bar>) div (sgn v * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
1847 proof -
1848   from assms have "sgn v = - 1 \<or> sgn v = 1"
1849     by (cases "v \<ge> 0") auto
1850   then show ?thesis
1851     using assms unfolding divide_int_def [of "sgn v * \<bar>k\<bar>" "sgn v * \<bar>l\<bar>"]
1852     by (fastforce simp add: not_less div_abs_eq_div_nat)
1853 qed
1855 lemma div_eq_sgn_abs:
1856   fixes k l v :: int
1857   assumes "sgn k = sgn l"
1858   shows "k div l = \<bar>k\<bar> div \<bar>l\<bar>"
1859 proof (cases "l = 0")
1860   case True
1861   then show ?thesis
1862     by simp
1863 next
1864   case False
1865   with assms have "(sgn k * \<bar>k\<bar>) div (sgn l * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
1866     by (simp add: div_sgn_abs_cancel)
1867   then show ?thesis
1868     by (simp add: sgn_mult_abs)
1869 qed
1871 lemma div_dvd_sgn_abs:
1872   fixes k l :: int
1873   assumes "l dvd k"
1874   shows "k div l = (sgn k * sgn l) * (\<bar>k\<bar> div \<bar>l\<bar>)"
1875 proof (cases "k = 0")
1876   case True
1877   then show ?thesis
1878     by simp
1879 next
1880   case False
1881   show ?thesis
1882   proof (cases "sgn l = sgn k")
1883     case True
1884     then show ?thesis
1885       by (simp add: div_eq_sgn_abs)
1886   next
1887     case False
1888     with \<open>k \<noteq> 0\<close> assms show ?thesis
1889       unfolding divide_int_def [of k l]
1890         by (auto simp add: zdiv_int)
1891   qed
1892 qed
1894 lemma div_noneq_sgn_abs:
1895   fixes k l :: int
1896   assumes "l \<noteq> 0"
1897   assumes "sgn k \<noteq> sgn l"
1898   shows "k div l = - (\<bar>k\<bar> div \<bar>l\<bar>) - of_bool (\<not> l dvd k)"
1899   using assms
1900   by (simp only: divide_int_def [of k l], auto simp add: not_less zdiv_int)
1902 lemma sgn_mod:
1903   fixes k l :: int
1904   assumes "l \<noteq> 0" "\<not> l dvd k"
1905   shows "sgn (k mod l) = sgn l"
1906 proof -
1907   from \<open>\<not> l dvd k\<close>
1908   have "k mod l \<noteq> 0"
1909     by (simp add: dvd_eq_mod_eq_0)
1910   show ?thesis
1911     using \<open>l \<noteq> 0\<close> \<open>\<not> l dvd k\<close>
1912     unfolding modulo_int_def [of k l]
1913     by (auto simp add: sgn_1_pos sgn_1_neg mod_greater_zero_iff_not_dvd nat_dvd_iff not_less
1914       zless_nat_eq_int_zless [symmetric] elim: nonpos_int_cases)
1915 qed
1917 lemma abs_mod_less:
1918   fixes k l :: int
1919   assumes "l \<noteq> 0"
1920   shows "\<bar>k mod l\<bar> < \<bar>l\<bar>"
1921   using assms unfolding modulo_int_def [of k l]
1922   by (auto simp add: not_less int_dvd_iff mod_greater_zero_iff_not_dvd elim: pos_int_cases neg_int_cases nonneg_int_cases nonpos_int_cases)
1924 instance int :: ring_div
1925 proof
1926   fix k l s :: int
1927   assume "l \<noteq> 0"
1928   then have "eucl_rel_int (k + s * l) l (s + k div l, k mod l)"
1929     using eucl_rel_int [of k l]
1930     unfolding eucl_rel_int_iff by (auto simp: algebra_simps)
1931   then show "(k + s * l) div l = s + k div l"
1932     by (rule div_int_unique)
1933 next
1934   fix k l s :: int
1935   assume "s \<noteq> 0"
1936   have "\<And>q r. eucl_rel_int k l (q, r)
1937     \<Longrightarrow> eucl_rel_int (s * k) (s * l) (q, s * r)"
1938     unfolding eucl_rel_int_iff
1939     by (rule linorder_cases [of 0 l])
1940       (use \<open>s \<noteq> 0\<close> in \<open>auto simp: algebra_simps
1941       mult_less_0_iff zero_less_mult_iff mult_strict_right_mono
1942       mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff\<close>)
1943   then have "eucl_rel_int (s * k) (s * l) (k div l, s * (k mod l))"
1944     using eucl_rel_int [of k l] .
1945   then show "(s * k) div (s * l) = k div l"
1946     by (rule div_int_unique)
1947 qed
1949 ML \<open>
1950 structure Cancel_Div_Mod_Int = Cancel_Div_Mod
1951 (
1952   val div_name = @{const_name divide};
1953   val mod_name = @{const_name modulo};
1954   val mk_binop = HOLogic.mk_binop;
1955   val mk_sum = Arith_Data.mk_sum HOLogic.intT;
1956   val dest_sum = Arith_Data.dest_sum;
1958   val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
1960   val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
1961     @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
1962 )
1963 \<close>
1965 simproc_setup cancel_div_mod_int ("(k::int) + l") =
1966   \<open>K Cancel_Div_Mod_Int.proc\<close>
1969 text\<open>Basic laws about division and remainder\<close>
1971 lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"
1972   using eucl_rel_int [of a b]
1973   by (auto simp add: eucl_rel_int_iff prod_eq_iff)
1975 lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1]
1976    and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2]
1978 lemma neg_mod_conj: "b < (0::int) \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b"
1979   using eucl_rel_int [of a b]
1980   by (auto simp add: eucl_rel_int_iff prod_eq_iff)
1982 lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1]
1983    and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2]
1986 subsubsection \<open>General Properties of div and mod\<close>
1988 lemma div_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a div b = 0"
1989 apply (rule div_int_unique)
1990 apply (auto simp add: eucl_rel_int_iff)
1991 done
1993 lemma div_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a div b = 0"
1994 apply (rule div_int_unique)
1995 apply (auto simp add: eucl_rel_int_iff)
1996 done
1998 lemma div_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a div b = -1"
1999 apply (rule div_int_unique)
2000 apply (auto simp add: eucl_rel_int_iff)
2001 done
2003 lemma div_positive_int:
2004   "k div l > 0" if "k \<ge> l" and "l > 0" for k l :: int
2005   using that by (simp add: divide_int_def div_positive)
2007 (*There is no div_neg_pos_trivial because  0 div b = 0 would supersede it*)
2009 lemma mod_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a mod b = a"
2010 apply (rule_tac q = 0 in mod_int_unique)
2011 apply (auto simp add: eucl_rel_int_iff)
2012 done
2014 lemma mod_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a mod b = a"
2015 apply (rule_tac q = 0 in mod_int_unique)
2016 apply (auto simp add: eucl_rel_int_iff)
2017 done
2019 lemma mod_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a mod b = a+b"
2020 apply (rule_tac q = "-1" in mod_int_unique)
2021 apply (auto simp add: eucl_rel_int_iff)
2022 done
2024 text\<open>There is no \<open>mod_neg_pos_trivial\<close>.\<close>
2027 subsubsection \<open>Laws for div and mod with Unary Minus\<close>
2029 lemma zminus1_lemma:
2030      "eucl_rel_int a b (q, r) ==> b \<noteq> 0
2031       ==> eucl_rel_int (-a) b (if r=0 then -q else -q - 1,
2032                           if r=0 then 0 else b-r)"
2033 by (force simp add: eucl_rel_int_iff right_diff_distrib)
2036 lemma zdiv_zminus1_eq_if:
2037      "b \<noteq> (0::int)
2038       ==> (-a) div b =
2039           (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
2040 by (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN div_int_unique])
2042 lemma zmod_zminus1_eq_if:
2043      "(-a::int) mod b = (if a mod b = 0 then 0 else  b - (a mod b))"
2044 apply (case_tac "b = 0", simp)
2045 apply (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN mod_int_unique])
2046 done
2048 lemma zmod_zminus1_not_zero:
2049   fixes k l :: int
2050   shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
2051   by (simp add: mod_eq_0_iff_dvd)
2053 lemma zmod_zminus2_not_zero:
2054   fixes k l :: int
2055   shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
2056   by (simp add: mod_eq_0_iff_dvd)
2058 lemma zdiv_zminus2_eq_if:
2059      "b \<noteq> (0::int)
2060       ==> a div (-b) =
2061           (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
2062 by (simp add: zdiv_zminus1_eq_if div_minus_right)
2064 lemma zmod_zminus2_eq_if:
2065      "a mod (-b::int) = (if a mod b = 0 then 0 else  (a mod b) - b)"
2066 by (simp add: zmod_zminus1_eq_if mod_minus_right)
2069 subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
2071 lemma zdiv_mono1: "[| a \<le> a';  0 < (b::int) |] ==> a div b \<le> a' div b"
2072 using mult_div_mod_eq [symmetric, of a b]
2073 using mult_div_mod_eq [symmetric, of a' b]
2074 apply -
2075 apply (rule unique_quotient_lemma)
2076 apply (erule subst)
2077 apply (erule subst, simp_all)
2078 done
2080 lemma zdiv_mono1_neg: "[| a \<le> a';  (b::int) < 0 |] ==> a' div b \<le> a div b"
2081 using mult_div_mod_eq [symmetric, of a b]
2082 using mult_div_mod_eq [symmetric, of a' b]
2083 apply -
2084 apply (rule unique_quotient_lemma_neg)
2085 apply (erule subst)
2086 apply (erule subst, simp_all)
2087 done
2090 subsubsection \<open>Monotonicity in the Second Argument (Divisor)\<close>
2092 lemma q_pos_lemma:
2093      "[| 0 \<le> b'*q' + r'; r' < b';  0 < b' |] ==> 0 \<le> (q'::int)"
2094 apply (subgoal_tac "0 < b'* (q' + 1) ")
2095  apply (simp add: zero_less_mult_iff)
2096 apply (simp add: distrib_left)
2097 done
2099 lemma zdiv_mono2_lemma:
2100      "[| b*q + r = b'*q' + r';  0 \<le> b'*q' + r';
2101          r' < b';  0 \<le> r;  0 < b';  b' \<le> b |]
2102       ==> q \<le> (q'::int)"
2103 apply (frule q_pos_lemma, assumption+)
2104 apply (subgoal_tac "b*q < b* (q' + 1) ")
2105  apply (simp add: mult_less_cancel_left)
2106 apply (subgoal_tac "b*q = r' - r + b'*q'")
2107  prefer 2 apply simp
2108 apply (simp (no_asm_simp) add: distrib_left)
2109 apply (subst add.commute, rule add_less_le_mono, arith)
2110 apply (rule mult_right_mono, auto)
2111 done
2113 lemma zdiv_mono2:
2114      "[| (0::int) \<le> a;  0 < b';  b' \<le> b |] ==> a div b \<le> a div b'"
2115 apply (subgoal_tac "b \<noteq> 0")
2116   prefer 2 apply arith
2117 using mult_div_mod_eq [symmetric, of a b]
2118 using mult_div_mod_eq [symmetric, of a b']
2119 apply -
2120 apply (rule zdiv_mono2_lemma)
2121 apply (erule subst)
2122 apply (erule subst, simp_all)
2123 done
2125 lemma q_neg_lemma:
2126      "[| b'*q' + r' < 0;  0 \<le> r';  0 < b' |] ==> q' \<le> (0::int)"
2127 apply (subgoal_tac "b'*q' < 0")
2128  apply (simp add: mult_less_0_iff, arith)
2129 done
2131 lemma zdiv_mono2_neg_lemma:
2132      "[| b*q + r = b'*q' + r';  b'*q' + r' < 0;
2133          r < b;  0 \<le> r';  0 < b';  b' \<le> b |]
2134       ==> q' \<le> (q::int)"
2135 apply (frule q_neg_lemma, assumption+)
2136 apply (subgoal_tac "b*q' < b* (q + 1) ")
2137  apply (simp add: mult_less_cancel_left)
2138 apply (simp add: distrib_left)
2139 apply (subgoal_tac "b*q' \<le> b'*q'")
2140  prefer 2 apply (simp add: mult_right_mono_neg, arith)
2141 done
2143 lemma zdiv_mono2_neg:
2144      "[| a < (0::int);  0 < b';  b' \<le> b |] ==> a div b' \<le> a div b"
2145 using mult_div_mod_eq [symmetric, of a b]
2146 using mult_div_mod_eq [symmetric, of a b']
2147 apply -
2148 apply (rule zdiv_mono2_neg_lemma)
2149 apply (erule subst)
2150 apply (erule subst, simp_all)
2151 done
2154 subsubsection \<open>More Algebraic Laws for div and mod\<close>
2156 text\<open>proving (a*b) div c = a * (b div c) + a * (b mod c)\<close>
2158 lemma zmult1_lemma:
2159      "[| eucl_rel_int b c (q, r) |]
2160       ==> eucl_rel_int (a * b) c (a*q + a*r div c, a*r mod c)"
2161 by (auto simp add: split_ifs eucl_rel_int_iff linorder_neq_iff distrib_left ac_simps)
2163 lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
2164 apply (case_tac "c = 0", simp)
2165 apply (blast intro: eucl_rel_int [THEN zmult1_lemma, THEN div_int_unique])
2166 done
2168 text\<open>proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c)\<close>
2170 lemma zadd1_lemma:
2171      "[| eucl_rel_int a c (aq, ar);  eucl_rel_int b c (bq, br) |]
2172       ==> eucl_rel_int (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
2173 by (force simp add: split_ifs eucl_rel_int_iff linorder_neq_iff distrib_left)
2175 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
2176 lemma zdiv_zadd1_eq:
2177      "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
2178 apply (case_tac "c = 0", simp)
2179 apply (blast intro: zadd1_lemma [OF eucl_rel_int eucl_rel_int] div_int_unique)
2180 done
2182 lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
2183 by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
2185 (* REVISIT: should this be generalized to all semiring_div types? *)
2186 lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
2189 subsubsection \<open>Proving  @{term "a div (b * c) = (a div b) div c"}\<close>
2191 (*The condition c>0 seems necessary.  Consider that 7 div ~6 = ~2 but
2192   7 div 2 div ~3 = 3 div ~3 = ~1.  The subcase (a div b) mod c = 0 seems
2193   to cause particular problems.*)
2195 text\<open>first, four lemmas to bound the remainder for the cases b<0 and b>0\<close>
2197 lemma zmult2_lemma_aux1: "[| (0::int) < c;  b < r;  r \<le> 0 |] ==> b * c < b * (q mod c) + r"
2198 apply (subgoal_tac "b * (c - q mod c) < r * 1")
2199  apply (simp add: algebra_simps)
2200 apply (rule order_le_less_trans)
2201  apply (erule_tac [2] mult_strict_right_mono)
2202  apply (rule mult_left_mono_neg)
2203   using add1_zle_eq[of "q mod c"]apply(simp add: algebra_simps)
2204  apply (simp)
2205 apply (simp)
2206 done
2208 lemma zmult2_lemma_aux2:
2209      "[| (0::int) < c;   b < r;  r \<le> 0 |] ==> b * (q mod c) + r \<le> 0"
2210 apply (subgoal_tac "b * (q mod c) \<le> 0")
2211  apply arith
2212 apply (simp add: mult_le_0_iff)
2213 done
2215 lemma zmult2_lemma_aux3: "[| (0::int) < c;  0 \<le> r;  r < b |] ==> 0 \<le> b * (q mod c) + r"
2216 apply (subgoal_tac "0 \<le> b * (q mod c) ")
2217 apply arith
2218 apply (simp add: zero_le_mult_iff)
2219 done
2221 lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 \<le> r; r < b |] ==> b * (q mod c) + r < b * c"
2222 apply (subgoal_tac "r * 1 < b * (c - q mod c) ")
2223  apply (simp add: right_diff_distrib)
2224 apply (rule order_less_le_trans)
2225  apply (erule mult_strict_right_mono)
2226  apply (rule_tac [2] mult_left_mono)
2227   apply simp
2228  using add1_zle_eq[of "q mod c"] apply (simp add: algebra_simps)
2229 apply simp
2230 done
2232 lemma zmult2_lemma: "[| eucl_rel_int a b (q, r); 0 < c |]
2233       ==> eucl_rel_int a (b * c) (q div c, b*(q mod c) + r)"
2234 by (auto simp add: mult.assoc eucl_rel_int_iff linorder_neq_iff
2235                    zero_less_mult_iff distrib_left [symmetric]
2236                    zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: if_split_asm)
2238 lemma zdiv_zmult2_eq:
2239   fixes a b c :: int
2240   shows "0 \<le> c \<Longrightarrow> a div (b * c) = (a div b) div c"
2241 apply (case_tac "b = 0", simp)
2242 apply (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN div_int_unique])
2243 done
2245 lemma zmod_zmult2_eq:
2246   fixes a b c :: int
2247   shows "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
2248 apply (case_tac "b = 0", simp)
2249 apply (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN mod_int_unique])
2250 done
2252 lemma div_pos_geq:
2253   fixes k l :: int
2254   assumes "0 < l" and "l \<le> k"
2255   shows "k div l = (k - l) div l + 1"
2256 proof -
2257   have "k = (k - l) + l" by simp
2258   then obtain j where k: "k = j + l" ..
2259   with assms show ?thesis by (simp add: div_add_self2)
2260 qed
2262 lemma mod_pos_geq:
2263   fixes k l :: int
2264   assumes "0 < l" and "l \<le> k"
2265   shows "k mod l = (k - l) mod l"
2266 proof -
2267   have "k = (k - l) + l" by simp
2268   then obtain j where k: "k = j + l" ..
2269   with assms show ?thesis by simp
2270 qed
2273 subsubsection \<open>Splitting Rules for div and mod\<close>
2275 text\<open>The proofs of the two lemmas below are essentially identical\<close>
2277 lemma split_pos_lemma:
2278  "0<k ==>
2279     P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)"
2280 apply (rule iffI, clarify)
2281  apply (erule_tac P="P x y" for x y in rev_mp)
2282  apply (subst mod_add_eq [symmetric])
2283  apply (subst zdiv_zadd1_eq)
2284  apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)
2285 txt\<open>converse direction\<close>
2286 apply (drule_tac x = "n div k" in spec)
2287 apply (drule_tac x = "n mod k" in spec, simp)
2288 done
2290 lemma split_neg_lemma:
2291  "k<0 ==>
2292     P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)"
2293 apply (rule iffI, clarify)
2294  apply (erule_tac P="P x y" for x y in rev_mp)
2295  apply (subst mod_add_eq [symmetric])
2296  apply (subst zdiv_zadd1_eq)
2297  apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)
2298 txt\<open>converse direction\<close>
2299 apply (drule_tac x = "n div k" in spec)
2300 apply (drule_tac x = "n mod k" in spec, simp)
2301 done
2303 lemma split_zdiv:
2304  "P(n div k :: int) =
2305   ((k = 0 --> P 0) &
2306    (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i)) &
2307    (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i)))"
2308 apply (case_tac "k=0", simp)
2309 apply (simp only: linorder_neq_iff)
2310 apply (erule disjE)
2311  apply (simp_all add: split_pos_lemma [of concl: "%x y. P x"]
2312                       split_neg_lemma [of concl: "%x y. P x"])
2313 done
2315 lemma split_zmod:
2316  "P(n mod k :: int) =
2317   ((k = 0 --> P n) &
2318    (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P j)) &
2319    (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P j)))"
2320 apply (case_tac "k=0", simp)
2321 apply (simp only: linorder_neq_iff)
2322 apply (erule disjE)
2323  apply (simp_all add: split_pos_lemma [of concl: "%x y. P y"]
2324                       split_neg_lemma [of concl: "%x y. P y"])
2325 done
2327 text \<open>Enable (lin)arith to deal with @{const divide} and @{const modulo}
2328   when these are applied to some constant that is of the form
2329   @{term "numeral k"}:\<close>
2330 declare split_zdiv [of _ _ "numeral k", arith_split] for k
2331 declare split_zmod [of _ _ "numeral k", arith_split] for k
2334 subsubsection \<open>Computing \<open>div\<close> and \<open>mod\<close> with shifting\<close>
2336 lemma pos_eucl_rel_int_mult_2:
2337   assumes "0 \<le> b"
2338   assumes "eucl_rel_int a b (q, r)"
2339   shows "eucl_rel_int (1 + 2*a) (2*b) (q, 1 + 2*r)"
2340   using assms unfolding eucl_rel_int_iff by auto
2342 lemma neg_eucl_rel_int_mult_2:
2343   assumes "b \<le> 0"
2344   assumes "eucl_rel_int (a + 1) b (q, r)"
2345   shows "eucl_rel_int (1 + 2*a) (2*b) (q, 2*r - 1)"
2346   using assms unfolding eucl_rel_int_iff by auto
2348 text\<open>computing div by shifting\<close>
2350 lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a"
2351   using pos_eucl_rel_int_mult_2 [OF _ eucl_rel_int]
2352   by (rule div_int_unique)
2354 lemma neg_zdiv_mult_2:
2355   assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a"
2356   using neg_eucl_rel_int_mult_2 [OF A eucl_rel_int]
2357   by (rule div_int_unique)
2359 (* FIXME: add rules for negative numerals *)
2360 lemma zdiv_numeral_Bit0 [simp]:
2361   "numeral (Num.Bit0 v) div numeral (Num.Bit0 w) =
2362     numeral v div (numeral w :: int)"
2363   unfolding numeral.simps unfolding mult_2 [symmetric]
2364   by (rule div_mult_mult1, simp)
2366 lemma zdiv_numeral_Bit1 [simp]:
2367   "numeral (Num.Bit1 v) div numeral (Num.Bit0 w) =
2368     (numeral v div (numeral w :: int))"
2369   unfolding numeral.simps
2370   unfolding mult_2 [symmetric] add.commute [of _ 1]
2371   by (rule pos_zdiv_mult_2, simp)
2373 lemma pos_zmod_mult_2:
2374   fixes a b :: int
2375   assumes "0 \<le> a"
2376   shows "(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)"
2377   using pos_eucl_rel_int_mult_2 [OF assms eucl_rel_int]
2378   by (rule mod_int_unique)
2380 lemma neg_zmod_mult_2:
2381   fixes a b :: int
2382   assumes "a \<le> 0"
2383   shows "(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1"
2384   using neg_eucl_rel_int_mult_2 [OF assms eucl_rel_int]
2385   by (rule mod_int_unique)
2387 (* FIXME: add rules for negative numerals *)
2388 lemma zmod_numeral_Bit0 [simp]:
2389   "numeral (Num.Bit0 v) mod numeral (Num.Bit0 w) =
2390     (2::int) * (numeral v mod numeral w)"
2391   unfolding numeral_Bit0 [of v] numeral_Bit0 [of w]
2392   unfolding mult_2 [symmetric] by (rule mod_mult_mult1)
2394 lemma zmod_numeral_Bit1 [simp]:
2395   "numeral (Num.Bit1 v) mod numeral (Num.Bit0 w) =
2396     2 * (numeral v mod numeral w) + (1::int)"
2397   unfolding numeral_Bit1 [of v] numeral_Bit0 [of w]
2398   unfolding mult_2 [symmetric] add.commute [of _ 1]
2399   by (rule pos_zmod_mult_2, simp)
2401 lemma zdiv_eq_0_iff:
2402  "(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")
2403 proof
2404   assume ?L
2405   have "?L \<longrightarrow> ?R" by (rule split_zdiv[THEN iffD2]) simp
2406   with \<open>?L\<close> show ?R by blast
2407 next
2408   assume ?R thus ?L
2409     by(auto simp: div_pos_pos_trivial div_neg_neg_trivial)
2410 qed
2412 lemma zmod_trival_iff:
2413   fixes i k :: int
2414   shows "i mod k = i \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i"
2415 proof -
2416   have "i mod k = i \<longleftrightarrow> i div k = 0"
2417     by safe (insert div_mult_mod_eq [of i k], auto)
2418   with zdiv_eq_0_iff
2419   show ?thesis
2420     by simp
2421 qed
2423 instantiation int :: unique_euclidean_ring
2424 begin
2426 definition [simp]:
2427   "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
2429 definition [simp]:
2430   "uniqueness_constraint_int (k :: int) l \<longleftrightarrow> unit_factor k = unit_factor l"
2432 instance
2433   by standard
2434     (use mult_le_mono2 [of 1] in \<open>auto simp add: abs_mult nat_mult_distrib sgn_mod zdiv_eq_0_iff sgn_1_pos sgn_mult split: abs_split\<close>)
2436 end
2439 subsubsection \<open>Quotients of Signs\<close>
2441 lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1"
2442 by (simp add: divide_int_def)
2444 lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
2445 by (simp add: modulo_int_def)
2447 lemma div_neg_pos_less0: "[| a < (0::int);  0 < b |] ==> a div b < 0"
2448 apply (subgoal_tac "a div b \<le> -1", force)
2449 apply (rule order_trans)
2450 apply (rule_tac a' = "-1" in zdiv_mono1)
2451 apply (auto simp add: div_eq_minus1)
2452 done
2454 lemma div_nonneg_neg_le0: "[| (0::int) \<le> a; b < 0 |] ==> a div b \<le> 0"
2455 by (drule zdiv_mono1_neg, auto)
2457 lemma div_nonpos_pos_le0: "[| (a::int) \<le> 0; b > 0 |] ==> a div b \<le> 0"
2458 by (drule zdiv_mono1, auto)
2460 text\<open>Now for some equivalences of the form \<open>a div b >=< 0 \<longleftrightarrow> \<dots>\<close>
2461 conditional upon the sign of \<open>a\<close> or \<open>b\<close>. There are many more.
2462 They should all be simp rules unless that causes too much search.\<close>
2464 lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \<le> a div b) = (0 \<le> a)"
2465 apply auto
2466 apply (drule_tac [2] zdiv_mono1)
2467 apply (auto simp add: linorder_neq_iff)
2468 apply (simp (no_asm_use) add: linorder_not_less [symmetric])
2469 apply (blast intro: div_neg_pos_less0)
2470 done
2472 lemma pos_imp_zdiv_pos_iff:
2473   "0<k \<Longrightarrow> 0 < (i::int) div k \<longleftrightarrow> k \<le> i"
2474 using pos_imp_zdiv_nonneg_iff[of k i] zdiv_eq_0_iff[of i k]
2475 by arith
2477 lemma neg_imp_zdiv_nonneg_iff:
2478   "b < (0::int) ==> (0 \<le> a div b) = (a \<le> (0::int))"
2479 apply (subst div_minus_minus [symmetric])
2480 apply (subst pos_imp_zdiv_nonneg_iff, auto)
2481 done
2483 (*But not (a div b \<le> 0 iff a\<le>0); consider a=1, b=2 when a div b = 0.*)
2484 lemma pos_imp_zdiv_neg_iff: "(0::int) < b ==> (a div b < 0) = (a < 0)"
2485 by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff)
2487 (*Again the law fails for \<le>: consider a = -1, b = -2 when a div b = 0*)
2488 lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)"
2489 by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff)
2491 lemma nonneg1_imp_zdiv_pos_iff:
2492   "(0::int) <= a \<Longrightarrow> (a div b > 0) = (a >= b & b>0)"
2493 apply rule
2494  apply rule
2495   using div_pos_pos_trivial[of a b]apply arith
2496  apply(cases "b=0")apply simp
2497  using div_nonneg_neg_le0[of a b]apply arith
2498 using int_one_le_iff_zero_less[of "a div b"] zdiv_mono1[of b a b]apply simp
2499 done
2501 lemma zmod_le_nonneg_dividend: "(m::int) \<ge> 0 ==> m mod k \<le> m"
2502 apply (rule split_zmod[THEN iffD2])
2503 apply(fastforce dest: q_pos_lemma intro: split_mult_pos_le)
2504 done
2507 subsubsection \<open>Computation of Division and Remainder\<close>
2509 instantiation int :: semiring_numeral_div
2510 begin
2512 definition divmod_int :: "num \<Rightarrow> num \<Rightarrow> int \<times> int"
2513 where
2514   "divmod_int m n = (numeral m div numeral n, numeral m mod numeral n)"
2516 definition divmod_step_int :: "num \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int"
2517 where
2518   "divmod_step_int l qr = (let (q, r) = qr
2519     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
2520     else (2 * q, r))"
2522 instance
2523   by standard (auto intro: zmod_le_nonneg_dividend simp add: divmod_int_def divmod_step_int_def
2524     pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial zmod_zmult2_eq zdiv_zmult2_eq)
2526 end
2528 declare divmod_algorithm_code [where ?'a = int, code]
2530 context
2531 begin
2533 qualified definition adjust_div :: "int \<times> int \<Rightarrow> int"
2534 where
2535   "adjust_div qr = (let (q, r) = qr in q + of_bool (r \<noteq> 0))"
2537 qualified lemma adjust_div_eq [simp, code]:
2538   "adjust_div (q, r) = q + of_bool (r \<noteq> 0)"
2539   by (simp add: adjust_div_def)
2541 qualified definition adjust_mod :: "int \<Rightarrow> int \<Rightarrow> int"
2542 where
2543   [simp]: "adjust_mod l r = (if r = 0 then 0 else l - r)"
2545 lemma minus_numeral_div_numeral [simp]:
2546   "- numeral m div numeral n = - (adjust_div (divmod m n) :: int)"
2547 proof -
2548   have "int (fst (divmod m n)) = fst (divmod m n)"
2549     by (simp only: fst_divmod divide_int_def) auto
2550   then show ?thesis
2551     by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def)
2552 qed
2554 lemma minus_numeral_mod_numeral [simp]:
2555   "- numeral m mod numeral n = adjust_mod (numeral n) (snd (divmod m n) :: int)"
2556 proof -
2557   have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
2558     using that by (simp only: snd_divmod modulo_int_def) auto
2559   then show ?thesis
2560     by (auto simp add: split_def Let_def adjust_div_def divides_aux_def modulo_int_def)
2561 qed
2563 lemma numeral_div_minus_numeral [simp]:
2564   "numeral m div - numeral n = - (adjust_div (divmod m n) :: int)"
2565 proof -
2566   have "int (fst (divmod m n)) = fst (divmod m n)"
2567     by (simp only: fst_divmod divide_int_def) auto
2568   then show ?thesis
2569     by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def)
2570 qed
2572 lemma numeral_mod_minus_numeral [simp]:
2573   "numeral m mod - numeral n = - adjust_mod (numeral n) (snd (divmod m n) :: int)"
2574 proof -
2575   have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
2576     using that by (simp only: snd_divmod modulo_int_def) auto
2577   then show ?thesis
2578     by (auto simp add: split_def Let_def adjust_div_def divides_aux_def modulo_int_def)
2579 qed
2581 lemma minus_one_div_numeral [simp]:
2582   "- 1 div numeral n = - (adjust_div (divmod Num.One n) :: int)"
2583   using minus_numeral_div_numeral [of Num.One n] by simp
2585 lemma minus_one_mod_numeral [simp]:
2586   "- 1 mod numeral n = adjust_mod (numeral n) (snd (divmod Num.One n) :: int)"
2587   using minus_numeral_mod_numeral [of Num.One n] by simp
2589 lemma one_div_minus_numeral [simp]:
2590   "1 div - numeral n = - (adjust_div (divmod Num.One n) :: int)"
2591   using numeral_div_minus_numeral [of Num.One n] by simp
2593 lemma one_mod_minus_numeral [simp]:
2594   "1 mod - numeral n = - adjust_mod (numeral n) (snd (divmod Num.One n) :: int)"
2595   using numeral_mod_minus_numeral [of Num.One n] by simp
2597 end
2600 subsubsection \<open>Further properties\<close>
2602 text \<open>Simplify expresions in which div and mod combine numerical constants\<close>
2604 lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
2605   by (rule div_int_unique [of a b q r]) (simp add: eucl_rel_int_iff)
2607 lemma int_div_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a div b = q"
2608   by (rule div_int_unique [of a b q r],
2609     simp add: eucl_rel_int_iff)
2611 lemma int_mod_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a mod b = r"
2612   by (rule mod_int_unique [of a b q r],
2613     simp add: eucl_rel_int_iff)
2615 lemma int_mod_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a mod b = r"
2616   by (rule mod_int_unique [of a b q r],
2617     simp add: eucl_rel_int_iff)
2619 lemma abs_div: "(y::int) dvd x \<Longrightarrow> \<bar>x div y\<bar> = \<bar>x\<bar> div \<bar>y\<bar>"
2620 by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
2622 text\<open>Suggested by Matthias Daum\<close>
2623 lemma int_power_div_base:
2624      "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"
2625 apply (subgoal_tac "k ^ m = k ^ ((m - Suc 0) + Suc 0)")
2626  apply (erule ssubst)
2627  apply (simp only: power_add)
2628  apply simp_all
2629 done
2631 text \<open>Distributive laws for function \<open>nat\<close>.\<close>
2633 lemma nat_div_distrib: "0 \<le> x \<Longrightarrow> nat (x div y) = nat x div nat y"
2634 apply (rule linorder_cases [of y 0])
2635 apply (simp add: div_nonneg_neg_le0)
2636 apply simp
2637 apply (simp add: nat_eq_iff pos_imp_zdiv_nonneg_iff zdiv_int)
2638 done
2640 (*Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't*)
2641 lemma nat_mod_distrib:
2642   "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x mod y) = nat x mod nat y"
2643 apply (case_tac "y = 0", simp)
2644 apply (simp add: nat_eq_iff zmod_int)
2645 done
2647 text  \<open>transfer setup\<close>
2649 lemma transfer_nat_int_functions:
2650     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
2651     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
2652   by (auto simp add: nat_div_distrib nat_mod_distrib)
2654 lemma transfer_nat_int_function_closures:
2655     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
2656     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
2657   apply (cases "y = 0")
2658   apply (auto simp add: pos_imp_zdiv_nonneg_iff)
2659   apply (cases "y = 0")
2660   apply auto
2661 done
2663 declare transfer_morphism_nat_int [transfer add return:
2664   transfer_nat_int_functions
2665   transfer_nat_int_function_closures
2666 ]
2668 lemma transfer_int_nat_functions:
2669     "(int x) div (int y) = int (x div y)"
2670     "(int x) mod (int y) = int (x mod y)"
2671   by (auto simp add: zdiv_int zmod_int)
2673 lemma transfer_int_nat_function_closures:
2674     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
2675     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
2676   by (simp_all only: is_nat_def transfer_nat_int_function_closures)
2678 declare transfer_morphism_int_nat [transfer add return:
2679   transfer_int_nat_functions
2680   transfer_int_nat_function_closures
2681 ]
2683 text\<open>Suggested by Matthias Daum\<close>
2684 lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
2685 apply (subgoal_tac "nat x div nat k < nat x")
2686  apply (simp add: nat_div_distrib [symmetric])
2687 apply (rule Divides.div_less_dividend, simp_all)
2688 done
2690 lemma (in ring_div) mod_eq_dvd_iff:
2691   "a mod c = b mod c \<longleftrightarrow> c dvd a - b" (is "?P \<longleftrightarrow> ?Q")
2692 proof
2693   assume ?P
2694   then have "(a mod c - b mod c) mod c = 0"
2695     by simp
2696   then show ?Q
2697     by (simp add: dvd_eq_mod_eq_0 mod_simps)
2698 next
2699   assume ?Q
2700   then obtain d where d: "a - b = c * d" ..
2701   then have "a = c * d + b"
2702     by (simp add: algebra_simps)
2703   then show ?P by simp
2704 qed
2706 lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y mod n" and xy:"y \<le> x"
2707   shows "\<exists>q. x = y + n * q"
2708 proof-
2709   from xy have th: "int x - int y = int (x - y)" by simp
2710   from xyn have "int x mod int n = int y mod int n"
2711     by (simp add: zmod_int [symmetric])
2712   hence "int n dvd int x - int y" by (simp only: mod_eq_dvd_iff [symmetric])
2713   hence "n dvd x - y" by (simp add: th zdvd_int)
2714   then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith
2715 qed
2717 lemma nat_mod_eq_iff: "(x::nat) mod n = y mod n \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)"
2718   (is "?lhs = ?rhs")
2719 proof
2720   assume H: "x mod n = y mod n"
2721   {assume xy: "x \<le> y"
2722     from H have th: "y mod n = x mod n" by simp
2723     from nat_mod_eq_lemma[OF th xy] have ?rhs
2724       apply clarify  apply (rule_tac x="q" in exI) by (rule exI[where x="0"], simp)}
2725   moreover
2726   {assume xy: "y \<le> x"
2727     from nat_mod_eq_lemma[OF H xy] have ?rhs
2728       apply clarify  apply (rule_tac x="0" in exI) by (rule_tac x="q" in exI, simp)}
2729   ultimately  show ?rhs using linear[of x y] by blast
2730 next
2731   assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast
2732   hence "(x + n * q1) mod n = (y + n * q2) mod n" by simp
2733   thus  ?lhs by simp
2734 qed
2736 subsubsection \<open>Dedicated simproc for calculation\<close>
2738 text \<open>
2739   There is space for improvement here: the calculation itself
2740   could be carried outside the logic, and a generic simproc
2741   (simplifier setup) for generic calculation would be helpful.
2742 \<close>
2744 simproc_setup numeral_divmod
2745   ("0 div 0 :: 'a :: semiring_numeral_div" | "0 mod 0 :: 'a :: semiring_numeral_div" |
2746    "0 div 1 :: 'a :: semiring_numeral_div" | "0 mod 1 :: 'a :: semiring_numeral_div" |
2747    "0 div - 1 :: int" | "0 mod - 1 :: int" |
2748    "0 div numeral b :: 'a :: semiring_numeral_div" | "0 mod numeral b :: 'a :: semiring_numeral_div" |
2749    "0 div - numeral b :: int" | "0 mod - numeral b :: int" |
2750    "1 div 0 :: 'a :: semiring_numeral_div" | "1 mod 0 :: 'a :: semiring_numeral_div" |
2751    "1 div 1 :: 'a :: semiring_numeral_div" | "1 mod 1 :: 'a :: semiring_numeral_div" |
2752    "1 div - 1 :: int" | "1 mod - 1 :: int" |
2753    "1 div numeral b :: 'a :: semiring_numeral_div" | "1 mod numeral b :: 'a :: semiring_numeral_div" |
2754    "1 div - numeral b :: int" |"1 mod - numeral b :: int" |
2755    "- 1 div 0 :: int" | "- 1 mod 0 :: int" | "- 1 div 1 :: int" | "- 1 mod 1 :: int" |
2756    "- 1 div - 1 :: int" | "- 1 mod - 1 :: int" | "- 1 div numeral b :: int" | "- 1 mod numeral b :: int" |
2757    "- 1 div - numeral b :: int" | "- 1 mod - numeral b :: int" |
2758    "numeral a div 0 :: 'a :: semiring_numeral_div" | "numeral a mod 0 :: 'a :: semiring_numeral_div" |
2759    "numeral a div 1 :: 'a :: semiring_numeral_div" | "numeral a mod 1 :: 'a :: semiring_numeral_div" |
2760    "numeral a div - 1 :: int" | "numeral a mod - 1 :: int" |
2761    "numeral a div numeral b :: 'a :: semiring_numeral_div" | "numeral a mod numeral b :: 'a :: semiring_numeral_div" |
2762    "numeral a div - numeral b :: int" | "numeral a mod - numeral b :: int" |
2763    "- numeral a div 0 :: int" | "- numeral a mod 0 :: int" |
2764    "- numeral a div 1 :: int" | "- numeral a mod 1 :: int" |
2765    "- numeral a div - 1 :: int" | "- numeral a mod - 1 :: int" |
2766    "- numeral a div numeral b :: int" | "- numeral a mod numeral b :: int" |
2767    "- numeral a div - numeral b :: int" | "- numeral a mod - numeral b :: int") =
2768 \<open> let
2769     val if_cong = the (Code.get_case_cong @{theory} @{const_name If});
2770     fun successful_rewrite ctxt ct =
2771       let
2772         val thm = Simplifier.rewrite ctxt ct
2773       in if Thm.is_reflexive thm then NONE else SOME thm end;
2774   in fn phi =>
2775     let
2776       val simps = Morphism.fact phi (@{thms div_0 mod_0 div_by_0 mod_by_0 div_by_1 mod_by_1
2777         one_div_numeral one_mod_numeral minus_one_div_numeral minus_one_mod_numeral
2778         one_div_minus_numeral one_mod_minus_numeral
2779         numeral_div_numeral numeral_mod_numeral minus_numeral_div_numeral minus_numeral_mod_numeral
2780         numeral_div_minus_numeral numeral_mod_minus_numeral
2781         div_minus_minus mod_minus_minus Divides.adjust_div_eq of_bool_eq one_neq_zero
2782         numeral_neq_zero neg_equal_0_iff_equal arith_simps arith_special divmod_trivial
2783         divmod_cancel divmod_steps divmod_step_eq fst_conv snd_conv numeral_One
2784         case_prod_beta rel_simps Divides.adjust_mod_def div_minus1_right mod_minus1_right
2785         minus_minus numeral_times_numeral mult_zero_right mult_1_right}
2786         @ [@{lemma "0 = 0 \<longleftrightarrow> True" by simp}]);
2787       fun prepare_simpset ctxt = HOL_ss |> Simplifier.simpset_map ctxt
2788         (Simplifier.add_cong if_cong #> fold Simplifier.add_simp simps)
2789     in fn ctxt => successful_rewrite (Simplifier.put_simpset (prepare_simpset ctxt) ctxt) end
2790   end;
2791 \<close>
2794 subsubsection \<open>Code generation\<close>
2796 lemma [code]:
2797   fixes k :: int
2798   shows
2799     "k div 0 = 0"
2800     "k mod 0 = k"
2801     "0 div k = 0"
2802     "0 mod k = 0"
2803     "k div Int.Pos Num.One = k"
2804     "k mod Int.Pos Num.One = 0"
2805     "k div Int.Neg Num.One = - k"
2806     "k mod Int.Neg Num.One = 0"
2807     "Int.Pos m div Int.Pos n = (fst (divmod m n) :: int)"
2808     "Int.Pos m mod Int.Pos n = (snd (divmod m n) :: int)"
2809     "Int.Neg m div Int.Pos n = - (Divides.adjust_div (divmod m n) :: int)"
2810     "Int.Neg m mod Int.Pos n = Divides.adjust_mod (Int.Pos n) (snd (divmod m n) :: int)"
2811     "Int.Pos m div Int.Neg n = - (Divides.adjust_div (divmod m n) :: int)"
2812     "Int.Pos m mod Int.Neg n = - Divides.adjust_mod (Int.Pos n) (snd (divmod m n) :: int)"
2813     "Int.Neg m div Int.Neg n = (fst (divmod m n) :: int)"
2814     "Int.Neg m mod Int.Neg n = - (snd (divmod m n) :: int)"
2815   by simp_all
2817 code_identifier
2818   code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
2820 lemma dvd_eq_mod_eq_0_numeral:
2821   "numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semiring_div)"
2822   by (fact dvd_eq_mod_eq_0)
2824 declare minus_div_mult_eq_mod [symmetric, nitpick_unfold]
2826 end