1 (* Title: HOL/IntDiv.thy |
1 (* Title: HOL/IntDiv.thy |
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1999 University of Cambridge |
3 Copyright 1999 University of Cambridge |
5 |
4 |
6 *) |
5 *) |
7 |
6 |
8 header{*The Division Operators div and mod; the Divides Relation dvd*} |
7 header{* The Division Operators div and mod *} |
9 |
8 |
10 theory IntDiv |
9 theory IntDiv |
11 imports Int Divides FunDef |
10 imports Int Divides FunDef |
12 begin |
11 begin |
13 |
12 |
14 constdefs |
13 definition divmod_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" where |
15 quorem :: "(int*int) * (int*int) => bool" |
|
16 --{*definition of quotient and remainder*} |
14 --{*definition of quotient and remainder*} |
17 [code]: "quorem == %((a,b), (q,r)). |
15 [code]: "divmod_rel a b = (\<lambda>(q, r). a = b * q + r \<and> |
18 a = b*q + r & |
16 (if 0 < b then 0 \<le> r \<and> r < b else b < r \<and> r \<le> 0))" |
19 (if 0 < b then 0\<le>r & r<b else b<r & r \<le> 0)" |
17 |
20 |
18 definition adjust :: "int \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int" where |
21 adjust :: "[int, int*int] => int*int" |
|
22 --{*for the division algorithm*} |
19 --{*for the division algorithm*} |
23 [code]: "adjust b == %(q,r). if 0 \<le> r-b then (2*q + 1, r-b) |
20 [code]: "adjust b = (\<lambda>(q, r). if 0 \<le> r - b then (2 * q + 1, r - b) |
24 else (2*q, r)" |
21 else (2 * q, r))" |
25 |
22 |
26 text{*algorithm for the case @{text "a\<ge>0, b>0"}*} |
23 text{*algorithm for the case @{text "a\<ge>0, b>0"}*} |
27 function |
24 function posDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where |
28 posDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" |
25 "posDivAlg a b = (if a < b \<or> b \<le> 0 then (0, a) |
29 where |
26 else adjust b (posDivAlg a (2 * b)))" |
30 "posDivAlg a b = |
|
31 (if (a<b | b\<le>0) then (0,a) |
|
32 else adjust b (posDivAlg a (2*b)))" |
|
33 by auto |
27 by auto |
34 termination by (relation "measure (%(a,b). nat(a - b + 1))") auto |
28 termination by (relation "measure (\<lambda>(a, b). nat (a - b + 1))") auto |
35 |
29 |
36 text{*algorithm for the case @{text "a<0, b>0"}*} |
30 text{*algorithm for the case @{text "a<0, b>0"}*} |
37 function |
31 function negDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where |
38 negDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" |
32 "negDivAlg a b = (if 0 \<le>a + b \<or> b \<le> 0 then (-1, a + b) |
39 where |
33 else adjust b (negDivAlg a (2 * b)))" |
40 "negDivAlg a b = |
|
41 (if (0\<le>a+b | b\<le>0) then (-1,a+b) |
|
42 else adjust b (negDivAlg a (2*b)))" |
|
43 by auto |
34 by auto |
44 termination by (relation "measure (%(a,b). nat(- a - b))") auto |
35 termination by (relation "measure (\<lambda>(a, b). nat (- a - b))") auto |
45 |
36 |
46 text{*algorithm for the general case @{term "b\<noteq>0"}*} |
37 text{*algorithm for the general case @{term "b\<noteq>0"}*} |
47 constdefs |
38 definition negateSnd :: "int \<times> int \<Rightarrow> int \<times> int" where |
48 negateSnd :: "int*int => int*int" |
39 [code inline]: "negateSnd = apsnd uminus" |
49 [code]: "negateSnd == %(q,r). (q,-r)" |
40 |
50 |
41 definition divmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where |
51 definition |
|
52 divAlg :: "int \<times> int \<Rightarrow> int \<times> int" |
|
53 --{*The full division algorithm considers all possible signs for a, b |
42 --{*The full division algorithm considers all possible signs for a, b |
54 including the special case @{text "a=0, b<0"} because |
43 including the special case @{text "a=0, b<0"} because |
55 @{term negDivAlg} requires @{term "a<0"}.*} |
44 @{term negDivAlg} requires @{term "a<0"}.*} |
56 where |
45 "divmod a b = (if 0 \<le> a then if 0 \<le> b then posDivAlg a b |
57 "divAlg = (\<lambda>(a, b). (if 0\<le>a then |
46 else if a = 0 then (0, 0) |
58 if 0\<le>b then posDivAlg a b |
|
59 else if a=0 then (0, 0) |
|
60 else negateSnd (negDivAlg (-a) (-b)) |
47 else negateSnd (negDivAlg (-a) (-b)) |
61 else |
48 else |
62 if 0<b then negDivAlg a b |
49 if 0 < b then negDivAlg a b |
63 else negateSnd (posDivAlg (-a) (-b))))" |
50 else negateSnd (posDivAlg (-a) (-b)))" |
64 |
51 |
65 instantiation int :: Divides.div |
52 instantiation int :: Divides.div |
66 begin |
53 begin |
67 |
54 |
68 definition |
55 definition |
69 div_def: "a div b = fst (divAlg (a, b))" |
56 div_def: "a div b = fst (divmod a b)" |
70 |
57 |
71 definition |
58 definition |
72 mod_def: "a mod b = snd (divAlg (a, b))" |
59 mod_def: "a mod b = snd (divmod a b)" |
73 |
60 |
74 instance .. |
61 instance .. |
75 |
62 |
76 end |
63 end |
77 |
64 |
78 lemma divAlg_mod_div: |
65 lemma divmod_mod_div: |
79 "divAlg (p, q) = (p div q, p mod q)" |
66 "divmod p q = (p div q, p mod q)" |
80 by (auto simp add: div_def mod_def) |
67 by (auto simp add: div_def mod_def) |
81 |
68 |
82 text{* |
69 text{* |
83 Here is the division algorithm in ML: |
70 Here is the division algorithm in ML: |
84 |
71 |
129 ==> q \<le> (q'::int)" |
116 ==> q \<le> (q'::int)" |
130 by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma, |
117 by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma, |
131 auto) |
118 auto) |
132 |
119 |
133 lemma unique_quotient: |
120 lemma unique_quotient: |
134 "[| quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); b \<noteq> 0 |] |
121 "[| divmod_rel a b (q, r); divmod_rel a b (q', r'); b \<noteq> 0 |] |
135 ==> q = q'" |
122 ==> q = q'" |
136 apply (simp add: quorem_def linorder_neq_iff split: split_if_asm) |
123 apply (simp add: divmod_rel_def linorder_neq_iff split: split_if_asm) |
137 apply (blast intro: order_antisym |
124 apply (blast intro: order_antisym |
138 dest: order_eq_refl [THEN unique_quotient_lemma] |
125 dest: order_eq_refl [THEN unique_quotient_lemma] |
139 order_eq_refl [THEN unique_quotient_lemma_neg] sym)+ |
126 order_eq_refl [THEN unique_quotient_lemma_neg] sym)+ |
140 done |
127 done |
141 |
128 |
142 |
129 |
143 lemma unique_remainder: |
130 lemma unique_remainder: |
144 "[| quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); b \<noteq> 0 |] |
131 "[| divmod_rel a b (q, r); divmod_rel a b (q', r'); b \<noteq> 0 |] |
145 ==> r = r'" |
132 ==> r = r'" |
146 apply (subgoal_tac "q = q'") |
133 apply (subgoal_tac "q = q'") |
147 apply (simp add: quorem_def) |
134 apply (simp add: divmod_rel_def) |
148 apply (blast intro: unique_quotient) |
135 apply (blast intro: unique_quotient) |
149 done |
136 done |
150 |
137 |
151 |
138 |
152 subsection{*Correctness of @{term posDivAlg}, the Algorithm for Non-Negative Dividends*} |
139 subsection{*Correctness of @{term posDivAlg}, the Algorithm for Non-Negative Dividends*} |
213 |
200 |
214 |
201 |
215 subsection{*Existence Shown by Proving the Division Algorithm to be Correct*} |
202 subsection{*Existence Shown by Proving the Division Algorithm to be Correct*} |
216 |
203 |
217 (*the case a=0*) |
204 (*the case a=0*) |
218 lemma quorem_0: "b \<noteq> 0 ==> quorem ((0,b), (0,0))" |
205 lemma divmod_rel_0: "b \<noteq> 0 ==> divmod_rel 0 b (0, 0)" |
219 by (auto simp add: quorem_def linorder_neq_iff) |
206 by (auto simp add: divmod_rel_def linorder_neq_iff) |
220 |
207 |
221 lemma posDivAlg_0 [simp]: "posDivAlg 0 b = (0, 0)" |
208 lemma posDivAlg_0 [simp]: "posDivAlg 0 b = (0, 0)" |
222 by (subst posDivAlg.simps, auto) |
209 by (subst posDivAlg.simps, auto) |
223 |
210 |
224 lemma negDivAlg_minus1 [simp]: "negDivAlg -1 b = (-1, b - 1)" |
211 lemma negDivAlg_minus1 [simp]: "negDivAlg -1 b = (-1, b - 1)" |
225 by (subst negDivAlg.simps, auto) |
212 by (subst negDivAlg.simps, auto) |
226 |
213 |
227 lemma negateSnd_eq [simp]: "negateSnd(q,r) = (q,-r)" |
214 lemma negateSnd_eq [simp]: "negateSnd(q,r) = (q,-r)" |
228 by (simp add: negateSnd_def) |
215 by (simp add: negateSnd_def) |
229 |
216 |
230 lemma quorem_neg: "quorem ((-a,-b), qr) ==> quorem ((a,b), negateSnd qr)" |
217 lemma divmod_rel_neg: "divmod_rel (-a) (-b) qr ==> divmod_rel a b (negateSnd qr)" |
231 by (auto simp add: split_ifs quorem_def) |
218 by (auto simp add: split_ifs divmod_rel_def) |
232 |
219 |
233 lemma divAlg_correct: "b \<noteq> 0 ==> quorem ((a,b), divAlg (a, b))" |
220 lemma divmod_correct: "b \<noteq> 0 ==> divmod_rel a b (divmod a b)" |
234 by (force simp add: linorder_neq_iff quorem_0 divAlg_def quorem_neg |
221 by (force simp add: linorder_neq_iff divmod_rel_0 divmod_def divmod_rel_neg |
235 posDivAlg_correct negDivAlg_correct) |
222 posDivAlg_correct negDivAlg_correct) |
236 |
223 |
237 text{*Arbitrary definitions for division by zero. Useful to simplify |
224 text{*Arbitrary definitions for division by zero. Useful to simplify |
238 certain equations.*} |
225 certain equations.*} |
239 |
226 |
240 lemma DIVISION_BY_ZERO [simp]: "a div (0::int) = 0 & a mod (0::int) = a" |
227 lemma DIVISION_BY_ZERO [simp]: "a div (0::int) = 0 & a mod (0::int) = a" |
241 by (simp add: div_def mod_def divAlg_def posDivAlg.simps) |
228 by (simp add: div_def mod_def divmod_def posDivAlg.simps) |
242 |
229 |
243 |
230 |
244 text{*Basic laws about division and remainder*} |
231 text{*Basic laws about division and remainder*} |
245 |
232 |
246 lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)" |
233 lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)" |
247 apply (case_tac "b = 0", simp) |
234 apply (case_tac "b = 0", simp) |
248 apply (cut_tac a = a and b = b in divAlg_correct) |
235 apply (cut_tac a = a and b = b in divmod_correct) |
249 apply (auto simp add: quorem_def div_def mod_def) |
236 apply (auto simp add: divmod_rel_def div_def mod_def) |
250 done |
237 done |
251 |
238 |
252 lemma zdiv_zmod_equality: "(b * (a div b) + (a mod b)) + k = (a::int)+k" |
239 lemma zdiv_zmod_equality: "(b * (a div b) + (a mod b)) + k = (a::int)+k" |
253 by(simp add: zmod_zdiv_equality[symmetric]) |
240 by(simp add: zmod_zdiv_equality[symmetric]) |
254 |
241 |
286 |
273 |
287 Addsimprocs [cancel_zdiv_zmod_proc] |
274 Addsimprocs [cancel_zdiv_zmod_proc] |
288 *} |
275 *} |
289 |
276 |
290 lemma pos_mod_conj : "(0::int) < b ==> 0 \<le> a mod b & a mod b < b" |
277 lemma pos_mod_conj : "(0::int) < b ==> 0 \<le> a mod b & a mod b < b" |
291 apply (cut_tac a = a and b = b in divAlg_correct) |
278 apply (cut_tac a = a and b = b in divmod_correct) |
292 apply (auto simp add: quorem_def mod_def) |
279 apply (auto simp add: divmod_rel_def mod_def) |
293 done |
280 done |
294 |
281 |
295 lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1, standard] |
282 lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1, standard] |
296 and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2, standard] |
283 and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2, standard] |
297 |
284 |
298 lemma neg_mod_conj : "b < (0::int) ==> a mod b \<le> 0 & b < a mod b" |
285 lemma neg_mod_conj : "b < (0::int) ==> a mod b \<le> 0 & b < a mod b" |
299 apply (cut_tac a = a and b = b in divAlg_correct) |
286 apply (cut_tac a = a and b = b in divmod_correct) |
300 apply (auto simp add: quorem_def div_def mod_def) |
287 apply (auto simp add: divmod_rel_def div_def mod_def) |
301 done |
288 done |
302 |
289 |
303 lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1, standard] |
290 lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1, standard] |
304 and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2, standard] |
291 and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2, standard] |
305 |
292 |
306 |
293 |
307 |
294 |
308 subsection{*General Properties of div and mod*} |
295 subsection{*General Properties of div and mod*} |
309 |
296 |
310 lemma quorem_div_mod: "b \<noteq> 0 ==> quorem ((a, b), (a div b, a mod b))" |
297 lemma divmod_rel_div_mod: "b \<noteq> 0 ==> divmod_rel a b (a div b, a mod b)" |
311 apply (cut_tac a = a and b = b in zmod_zdiv_equality) |
298 apply (cut_tac a = a and b = b in zmod_zdiv_equality) |
312 apply (force simp add: quorem_def linorder_neq_iff) |
299 apply (force simp add: divmod_rel_def linorder_neq_iff) |
313 done |
300 done |
314 |
301 |
315 lemma quorem_div: "[| quorem((a,b),(q,r)); b \<noteq> 0 |] ==> a div b = q" |
302 lemma divmod_rel_div: "[| divmod_rel a b (q, r); b \<noteq> 0 |] ==> a div b = q" |
316 by (simp add: quorem_div_mod [THEN unique_quotient]) |
303 by (simp add: divmod_rel_div_mod [THEN unique_quotient]) |
317 |
304 |
318 lemma quorem_mod: "[| quorem((a,b),(q,r)); b \<noteq> 0 |] ==> a mod b = r" |
305 lemma divmod_rel_mod: "[| divmod_rel a b (q, r); b \<noteq> 0 |] ==> a mod b = r" |
319 by (simp add: quorem_div_mod [THEN unique_remainder]) |
306 by (simp add: divmod_rel_div_mod [THEN unique_remainder]) |
320 |
307 |
321 lemma div_pos_pos_trivial: "[| (0::int) \<le> a; a < b |] ==> a div b = 0" |
308 lemma div_pos_pos_trivial: "[| (0::int) \<le> a; a < b |] ==> a div b = 0" |
322 apply (rule quorem_div) |
309 apply (rule divmod_rel_div) |
323 apply (auto simp add: quorem_def) |
310 apply (auto simp add: divmod_rel_def) |
324 done |
311 done |
325 |
312 |
326 lemma div_neg_neg_trivial: "[| a \<le> (0::int); b < a |] ==> a div b = 0" |
313 lemma div_neg_neg_trivial: "[| a \<le> (0::int); b < a |] ==> a div b = 0" |
327 apply (rule quorem_div) |
314 apply (rule divmod_rel_div) |
328 apply (auto simp add: quorem_def) |
315 apply (auto simp add: divmod_rel_def) |
329 done |
316 done |
330 |
317 |
331 lemma div_pos_neg_trivial: "[| (0::int) < a; a+b \<le> 0 |] ==> a div b = -1" |
318 lemma div_pos_neg_trivial: "[| (0::int) < a; a+b \<le> 0 |] ==> a div b = -1" |
332 apply (rule quorem_div) |
319 apply (rule divmod_rel_div) |
333 apply (auto simp add: quorem_def) |
320 apply (auto simp add: divmod_rel_def) |
334 done |
321 done |
335 |
322 |
336 (*There is no div_neg_pos_trivial because 0 div b = 0 would supersede it*) |
323 (*There is no div_neg_pos_trivial because 0 div b = 0 would supersede it*) |
337 |
324 |
338 lemma mod_pos_pos_trivial: "[| (0::int) \<le> a; a < b |] ==> a mod b = a" |
325 lemma mod_pos_pos_trivial: "[| (0::int) \<le> a; a < b |] ==> a mod b = a" |
339 apply (rule_tac q = 0 in quorem_mod) |
326 apply (rule_tac q = 0 in divmod_rel_mod) |
340 apply (auto simp add: quorem_def) |
327 apply (auto simp add: divmod_rel_def) |
341 done |
328 done |
342 |
329 |
343 lemma mod_neg_neg_trivial: "[| a \<le> (0::int); b < a |] ==> a mod b = a" |
330 lemma mod_neg_neg_trivial: "[| a \<le> (0::int); b < a |] ==> a mod b = a" |
344 apply (rule_tac q = 0 in quorem_mod) |
331 apply (rule_tac q = 0 in divmod_rel_mod) |
345 apply (auto simp add: quorem_def) |
332 apply (auto simp add: divmod_rel_def) |
346 done |
333 done |
347 |
334 |
348 lemma mod_pos_neg_trivial: "[| (0::int) < a; a+b \<le> 0 |] ==> a mod b = a+b" |
335 lemma mod_pos_neg_trivial: "[| (0::int) < a; a+b \<le> 0 |] ==> a mod b = a+b" |
349 apply (rule_tac q = "-1" in quorem_mod) |
336 apply (rule_tac q = "-1" in divmod_rel_mod) |
350 apply (auto simp add: quorem_def) |
337 apply (auto simp add: divmod_rel_def) |
351 done |
338 done |
352 |
339 |
353 text{*There is no @{text mod_neg_pos_trivial}.*} |
340 text{*There is no @{text mod_neg_pos_trivial}.*} |
354 |
341 |
355 |
342 |
356 (*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*) |
343 (*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*) |
357 lemma zdiv_zminus_zminus [simp]: "(-a) div (-b) = a div (b::int)" |
344 lemma zdiv_zminus_zminus [simp]: "(-a) div (-b) = a div (b::int)" |
358 apply (case_tac "b = 0", simp) |
345 apply (case_tac "b = 0", simp) |
359 apply (simp add: quorem_div_mod [THEN quorem_neg, simplified, |
346 apply (simp add: divmod_rel_div_mod [THEN divmod_rel_neg, simplified, |
360 THEN quorem_div, THEN sym]) |
347 THEN divmod_rel_div, THEN sym]) |
361 |
348 |
362 done |
349 done |
363 |
350 |
364 (*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*) |
351 (*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*) |
365 lemma zmod_zminus_zminus [simp]: "(-a) mod (-b) = - (a mod (b::int))" |
352 lemma zmod_zminus_zminus [simp]: "(-a) mod (-b) = - (a mod (b::int))" |
366 apply (case_tac "b = 0", simp) |
353 apply (case_tac "b = 0", simp) |
367 apply (subst quorem_div_mod [THEN quorem_neg, simplified, THEN quorem_mod], |
354 apply (subst divmod_rel_div_mod [THEN divmod_rel_neg, simplified, THEN divmod_rel_mod], |
368 auto) |
355 auto) |
369 done |
356 done |
370 |
357 |
371 |
358 |
372 subsection{*Laws for div and mod with Unary Minus*} |
359 subsection{*Laws for div and mod with Unary Minus*} |
373 |
360 |
374 lemma zminus1_lemma: |
361 lemma zminus1_lemma: |
375 "quorem((a,b),(q,r)) |
362 "divmod_rel a b (q, r) |
376 ==> quorem ((-a,b), (if r=0 then -q else -q - 1), |
363 ==> divmod_rel (-a) b (if r=0 then -q else -q - 1, |
377 (if r=0 then 0 else b-r))" |
364 if r=0 then 0 else b-r)" |
378 by (force simp add: split_ifs quorem_def linorder_neq_iff right_diff_distrib) |
365 by (force simp add: split_ifs divmod_rel_def linorder_neq_iff right_diff_distrib) |
379 |
366 |
380 |
367 |
381 lemma zdiv_zminus1_eq_if: |
368 lemma zdiv_zminus1_eq_if: |
382 "b \<noteq> (0::int) |
369 "b \<noteq> (0::int) |
383 ==> (-a) div b = |
370 ==> (-a) div b = |
384 (if a mod b = 0 then - (a div b) else - (a div b) - 1)" |
371 (if a mod b = 0 then - (a div b) else - (a div b) - 1)" |
385 by (blast intro: quorem_div_mod [THEN zminus1_lemma, THEN quorem_div]) |
372 by (blast intro: divmod_rel_div_mod [THEN zminus1_lemma, THEN divmod_rel_div]) |
386 |
373 |
387 lemma zmod_zminus1_eq_if: |
374 lemma zmod_zminus1_eq_if: |
388 "(-a::int) mod b = (if a mod b = 0 then 0 else b - (a mod b))" |
375 "(-a::int) mod b = (if a mod b = 0 then 0 else b - (a mod b))" |
389 apply (case_tac "b = 0", simp) |
376 apply (case_tac "b = 0", simp) |
390 apply (blast intro: quorem_div_mod [THEN zminus1_lemma, THEN quorem_mod]) |
377 apply (blast intro: divmod_rel_div_mod [THEN zminus1_lemma, THEN divmod_rel_mod]) |
391 done |
378 done |
392 |
379 |
393 lemma zdiv_zminus2: "a div (-b) = (-a::int) div b" |
380 lemma zdiv_zminus2: "a div (-b) = (-a::int) div b" |
394 by (cut_tac a = "-a" in zdiv_zminus_zminus, auto) |
381 by (cut_tac a = "-a" in zdiv_zminus_zminus, auto) |
395 |
382 |
418 apply (subgoal_tac "0 \<le> a* (1-q) ") |
405 apply (subgoal_tac "0 \<le> a* (1-q) ") |
419 apply (simp add: zero_le_mult_iff) |
406 apply (simp add: zero_le_mult_iff) |
420 apply (simp add: right_diff_distrib) |
407 apply (simp add: right_diff_distrib) |
421 done |
408 done |
422 |
409 |
423 lemma self_quotient: "[| quorem((a,a),(q,r)); a \<noteq> (0::int) |] ==> q = 1" |
410 lemma self_quotient: "[| divmod_rel a a (q, r); a \<noteq> (0::int) |] ==> q = 1" |
424 apply (simp add: split_ifs quorem_def linorder_neq_iff) |
411 apply (simp add: split_ifs divmod_rel_def linorder_neq_iff) |
425 apply (rule order_antisym, safe, simp_all) |
412 apply (rule order_antisym, safe, simp_all) |
426 apply (rule_tac [3] a = "-a" and r = "-r" in self_quotient_aux1) |
413 apply (rule_tac [3] a = "-a" and r = "-r" in self_quotient_aux1) |
427 apply (rule_tac a = "-a" and r = "-r" in self_quotient_aux2) |
414 apply (rule_tac a = "-a" and r = "-r" in self_quotient_aux2) |
428 apply (force intro: self_quotient_aux1 self_quotient_aux2 simp add: add_commute)+ |
415 apply (force intro: self_quotient_aux1 self_quotient_aux2 simp add: add_commute)+ |
429 done |
416 done |
430 |
417 |
431 lemma self_remainder: "[| quorem((a,a),(q,r)); a \<noteq> (0::int) |] ==> r = 0" |
418 lemma self_remainder: "[| divmod_rel a a (q, r); a \<noteq> (0::int) |] ==> r = 0" |
432 apply (frule self_quotient, assumption) |
419 apply (frule self_quotient, assumption) |
433 apply (simp add: quorem_def) |
420 apply (simp add: divmod_rel_def) |
434 done |
421 done |
435 |
422 |
436 lemma zdiv_self [simp]: "a \<noteq> 0 ==> a div a = (1::int)" |
423 lemma zdiv_self [simp]: "a \<noteq> 0 ==> a div a = (1::int)" |
437 by (simp add: quorem_div_mod [THEN self_quotient]) |
424 by (simp add: divmod_rel_div_mod [THEN self_quotient]) |
438 |
425 |
439 (*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *) |
426 (*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *) |
440 lemma zmod_self [simp]: "a mod a = (0::int)" |
427 lemma zmod_self [simp]: "a mod a = (0::int)" |
441 apply (case_tac "a = 0", simp) |
428 apply (case_tac "a = 0", simp) |
442 apply (simp add: quorem_div_mod [THEN self_remainder]) |
429 apply (simp add: divmod_rel_div_mod [THEN self_remainder]) |
443 done |
430 done |
444 |
431 |
445 |
432 |
446 subsection{*Computation of Division and Remainder*} |
433 subsection{*Computation of Division and Remainder*} |
447 |
434 |
448 lemma zdiv_zero [simp]: "(0::int) div b = 0" |
435 lemma zdiv_zero [simp]: "(0::int) div b = 0" |
449 by (simp add: div_def divAlg_def) |
436 by (simp add: div_def divmod_def) |
450 |
437 |
451 lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1" |
438 lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1" |
452 by (simp add: div_def divAlg_def) |
439 by (simp add: div_def divmod_def) |
453 |
440 |
454 lemma zmod_zero [simp]: "(0::int) mod b = 0" |
441 lemma zmod_zero [simp]: "(0::int) mod b = 0" |
455 by (simp add: mod_def divAlg_def) |
442 by (simp add: mod_def divmod_def) |
456 |
443 |
457 lemma zdiv_minus1: "(0::int) < b ==> -1 div b = -1" |
444 lemma zdiv_minus1: "(0::int) < b ==> -1 div b = -1" |
458 by (simp add: div_def divAlg_def) |
445 by (simp add: div_def divmod_def) |
459 |
446 |
460 lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1" |
447 lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1" |
461 by (simp add: mod_def divAlg_def) |
448 by (simp add: mod_def divmod_def) |
462 |
449 |
463 text{*a positive, b positive *} |
450 text{*a positive, b positive *} |
464 |
451 |
465 lemma div_pos_pos: "[| 0 < a; 0 \<le> b |] ==> a div b = fst (posDivAlg a b)" |
452 lemma div_pos_pos: "[| 0 < a; 0 \<le> b |] ==> a div b = fst (posDivAlg a b)" |
466 by (simp add: div_def divAlg_def) |
453 by (simp add: div_def divmod_def) |
467 |
454 |
468 lemma mod_pos_pos: "[| 0 < a; 0 \<le> b |] ==> a mod b = snd (posDivAlg a b)" |
455 lemma mod_pos_pos: "[| 0 < a; 0 \<le> b |] ==> a mod b = snd (posDivAlg a b)" |
469 by (simp add: mod_def divAlg_def) |
456 by (simp add: mod_def divmod_def) |
470 |
457 |
471 text{*a negative, b positive *} |
458 text{*a negative, b positive *} |
472 |
459 |
473 lemma div_neg_pos: "[| a < 0; 0 < b |] ==> a div b = fst (negDivAlg a b)" |
460 lemma div_neg_pos: "[| a < 0; 0 < b |] ==> a div b = fst (negDivAlg a b)" |
474 by (simp add: div_def divAlg_def) |
461 by (simp add: div_def divmod_def) |
475 |
462 |
476 lemma mod_neg_pos: "[| a < 0; 0 < b |] ==> a mod b = snd (negDivAlg a b)" |
463 lemma mod_neg_pos: "[| a < 0; 0 < b |] ==> a mod b = snd (negDivAlg a b)" |
477 by (simp add: mod_def divAlg_def) |
464 by (simp add: mod_def divmod_def) |
478 |
465 |
479 text{*a positive, b negative *} |
466 text{*a positive, b negative *} |
480 |
467 |
481 lemma div_pos_neg: |
468 lemma div_pos_neg: |
482 "[| 0 < a; b < 0 |] ==> a div b = fst (negateSnd (negDivAlg (-a) (-b)))" |
469 "[| 0 < a; b < 0 |] ==> a div b = fst (negateSnd (negDivAlg (-a) (-b)))" |
483 by (simp add: div_def divAlg_def) |
470 by (simp add: div_def divmod_def) |
484 |
471 |
485 lemma mod_pos_neg: |
472 lemma mod_pos_neg: |
486 "[| 0 < a; b < 0 |] ==> a mod b = snd (negateSnd (negDivAlg (-a) (-b)))" |
473 "[| 0 < a; b < 0 |] ==> a mod b = snd (negateSnd (negDivAlg (-a) (-b)))" |
487 by (simp add: mod_def divAlg_def) |
474 by (simp add: mod_def divmod_def) |
488 |
475 |
489 text{*a negative, b negative *} |
476 text{*a negative, b negative *} |
490 |
477 |
491 lemma div_neg_neg: |
478 lemma div_neg_neg: |
492 "[| a < 0; b \<le> 0 |] ==> a div b = fst (negateSnd (posDivAlg (-a) (-b)))" |
479 "[| a < 0; b \<le> 0 |] ==> a div b = fst (negateSnd (posDivAlg (-a) (-b)))" |
493 by (simp add: div_def divAlg_def) |
480 by (simp add: div_def divmod_def) |
494 |
481 |
495 lemma mod_neg_neg: |
482 lemma mod_neg_neg: |
496 "[| a < 0; b \<le> 0 |] ==> a mod b = snd (negateSnd (posDivAlg (-a) (-b)))" |
483 "[| a < 0; b \<le> 0 |] ==> a mod b = snd (negateSnd (posDivAlg (-a) (-b)))" |
497 by (simp add: mod_def divAlg_def) |
484 by (simp add: mod_def divmod_def) |
498 |
485 |
499 text {*Simplify expresions in which div and mod combine numerical constants*} |
486 text {*Simplify expresions in which div and mod combine numerical constants*} |
500 |
487 |
501 lemma quoremI: |
488 lemma divmod_relI: |
502 "\<lbrakk>a == b * q + r; if 0 < b then 0 \<le> r \<and> r < b else b < r \<and> r \<le> 0\<rbrakk> |
489 "\<lbrakk>a == b * q + r; if 0 < b then 0 \<le> r \<and> r < b else b < r \<and> r \<le> 0\<rbrakk> |
503 \<Longrightarrow> quorem ((a, b), (q, r))" |
490 \<Longrightarrow> divmod_rel a b (q, r)" |
504 unfolding quorem_def by simp |
491 unfolding divmod_rel_def by simp |
505 |
492 |
506 lemmas quorem_div_eq = quoremI [THEN quorem_div, THEN eq_reflection] |
493 lemmas divmod_rel_div_eq = divmod_relI [THEN divmod_rel_div, THEN eq_reflection] |
507 lemmas quorem_mod_eq = quoremI [THEN quorem_mod, THEN eq_reflection] |
494 lemmas divmod_rel_mod_eq = divmod_relI [THEN divmod_rel_mod, THEN eq_reflection] |
508 lemmas arithmetic_simps = |
495 lemmas arithmetic_simps = |
509 arith_simps |
496 arith_simps |
510 add_special |
497 add_special |
511 OrderedGroup.add_0_left |
498 OrderedGroup.add_0_left |
512 OrderedGroup.add_0_right |
499 OrderedGroup.add_0_right |
716 subsection{*More Algebraic Laws for div and mod*} |
703 subsection{*More Algebraic Laws for div and mod*} |
717 |
704 |
718 text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *} |
705 text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *} |
719 |
706 |
720 lemma zmult1_lemma: |
707 lemma zmult1_lemma: |
721 "[| quorem((b,c),(q,r)); c \<noteq> 0 |] |
708 "[| divmod_rel b c (q, r); c \<noteq> 0 |] |
722 ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))" |
709 ==> divmod_rel (a * b) c (a*q + a*r div c, a*r mod c)" |
723 by (force simp add: split_ifs quorem_def linorder_neq_iff right_distrib) |
710 by (force simp add: split_ifs divmod_rel_def linorder_neq_iff right_distrib) |
724 |
711 |
725 lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)" |
712 lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)" |
726 apply (case_tac "c = 0", simp) |
713 apply (case_tac "c = 0", simp) |
727 apply (blast intro: quorem_div_mod [THEN zmult1_lemma, THEN quorem_div]) |
714 apply (blast intro: divmod_rel_div_mod [THEN zmult1_lemma, THEN divmod_rel_div]) |
728 done |
715 done |
729 |
716 |
730 lemma zmod_zmult1_eq: "(a*b) mod c = a*(b mod c) mod (c::int)" |
717 lemma zmod_zmult1_eq: "(a*b) mod c = a*(b mod c) mod (c::int)" |
731 apply (case_tac "c = 0", simp) |
718 apply (case_tac "c = 0", simp) |
732 apply (blast intro: quorem_div_mod [THEN zmult1_lemma, THEN quorem_mod]) |
719 apply (blast intro: divmod_rel_div_mod [THEN zmult1_lemma, THEN divmod_rel_mod]) |
733 done |
720 done |
734 |
721 |
735 lemma zmod_zmult1_eq': "(a*b) mod (c::int) = ((a mod c) * b) mod c" |
722 lemma zmod_zmult1_eq': "(a*b) mod (c::int) = ((a mod c) * b) mod c" |
736 apply (rule trans) |
723 apply (rule trans) |
737 apply (rule_tac s = "b*a mod c" in trans) |
724 apply (rule_tac s = "b*a mod c" in trans) |
758 done |
745 done |
759 |
746 |
760 text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *} |
747 text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *} |
761 |
748 |
762 lemma zadd1_lemma: |
749 lemma zadd1_lemma: |
763 "[| quorem((a,c),(aq,ar)); quorem((b,c),(bq,br)); c \<noteq> 0 |] |
750 "[| divmod_rel a c (aq, ar); divmod_rel b c (bq, br); c \<noteq> 0 |] |
764 ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))" |
751 ==> divmod_rel (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)" |
765 by (force simp add: split_ifs quorem_def linorder_neq_iff right_distrib) |
752 by (force simp add: split_ifs divmod_rel_def linorder_neq_iff right_distrib) |
766 |
753 |
767 (*NOT suitable for rewriting: the RHS has an instance of the LHS*) |
754 (*NOT suitable for rewriting: the RHS has an instance of the LHS*) |
768 lemma zdiv_zadd1_eq: |
755 lemma zdiv_zadd1_eq: |
769 "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)" |
756 "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)" |
770 apply (case_tac "c = 0", simp) |
757 apply (case_tac "c = 0", simp) |
771 apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_div) |
758 apply (blast intro: zadd1_lemma [OF divmod_rel_div_mod divmod_rel_div_mod] divmod_rel_div) |
772 done |
759 done |
773 |
760 |
774 lemma zmod_zadd1_eq: "(a+b) mod (c::int) = (a mod c + b mod c) mod c" |
761 lemma zmod_zadd1_eq: "(a+b) mod (c::int) = (a mod c + b mod c) mod c" |
775 apply (case_tac "c = 0", simp) |
762 apply (case_tac "c = 0", simp) |
776 apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_mod) |
763 apply (blast intro: zadd1_lemma [OF divmod_rel_div_mod divmod_rel_div_mod] divmod_rel_mod) |
777 done |
764 done |
778 |
765 |
779 instance int :: ring_div |
766 instance int :: ring_div |
780 proof |
767 proof |
781 fix a b c :: int |
768 fix a b c :: int |
860 apply (rule_tac [2] mult_left_mono) |
874 apply (rule_tac [2] mult_left_mono) |
861 apply (auto simp add: compare_rls add_commute [of 1] |
875 apply (auto simp add: compare_rls add_commute [of 1] |
862 add1_zle_eq pos_mod_bound) |
876 add1_zle_eq pos_mod_bound) |
863 done |
877 done |
864 |
878 |
865 lemma zmult2_lemma: "[| quorem ((a,b), (q,r)); b \<noteq> 0; 0 < c |] |
879 lemma zmult2_lemma: "[| divmod_rel a b (q, r); b \<noteq> 0; 0 < c |] |
866 ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))" |
880 ==> divmod_rel a (b * c) (q div c, b*(q mod c) + r)" |
867 by (auto simp add: mult_ac quorem_def linorder_neq_iff |
881 by (auto simp add: mult_ac divmod_rel_def linorder_neq_iff |
868 zero_less_mult_iff right_distrib [symmetric] |
882 zero_less_mult_iff right_distrib [symmetric] |
869 zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4) |
883 zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4) |
870 |
884 |
871 lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c" |
885 lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c" |
872 apply (case_tac "b = 0", simp) |
886 apply (case_tac "b = 0", simp) |
873 apply (force simp add: quorem_div_mod [THEN zmult2_lemma, THEN quorem_div]) |
887 apply (force simp add: divmod_rel_div_mod [THEN zmult2_lemma, THEN divmod_rel_div]) |
874 done |
888 done |
875 |
889 |
876 lemma zmod_zmult2_eq: |
890 lemma zmod_zmult2_eq: |
877 "(0::int) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b" |
891 "(0::int) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b" |
878 apply (case_tac "b = 0", simp) |
892 apply (case_tac "b = 0", simp) |
879 apply (force simp add: quorem_div_mod [THEN zmult2_lemma, THEN quorem_mod]) |
893 apply (force simp add: divmod_rel_div_mod [THEN zmult2_lemma, THEN divmod_rel_mod]) |
880 done |
894 done |
881 |
895 |
882 |
896 |
883 subsection{*Cancellation of Common Factors in div*} |
897 subsection{*Cancellation of Common Factors in div*} |
884 |
898 |
1358 |
1372 |
1359 lemma zdiv_int: "int (a div b) = (int a) div (int b)" |
1373 lemma zdiv_int: "int (a div b) = (int a) div (int b)" |
1360 apply (subst split_div, auto) |
1374 apply (subst split_div, auto) |
1361 apply (subst split_zdiv, auto) |
1375 apply (subst split_zdiv, auto) |
1362 apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in IntDiv.unique_quotient) |
1376 apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in IntDiv.unique_quotient) |
1363 apply (auto simp add: IntDiv.quorem_def of_nat_mult) |
1377 apply (auto simp add: IntDiv.divmod_rel_def of_nat_mult) |
1364 done |
1378 done |
1365 |
1379 |
1366 lemma zmod_int: "int (a mod b) = (int a) mod (int b)" |
1380 lemma zmod_int: "int (a mod b) = (int a) mod (int b)" |
1367 apply (subst split_mod, auto) |
1381 apply (subst split_mod, auto) |
1368 apply (subst split_zmod, auto) |
1382 apply (subst split_zmod, auto) |
1369 apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia |
1383 apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia |
1370 in unique_remainder) |
1384 in unique_remainder) |
1371 apply (auto simp add: IntDiv.quorem_def of_nat_mult) |
1385 apply (auto simp add: IntDiv.divmod_rel_def of_nat_mult) |
1372 done |
1386 done |
1373 |
1387 |
1374 text{*Suggested by Matthias Daum*} |
1388 text{*Suggested by Matthias Daum*} |
1375 lemma int_power_div_base: |
1389 lemma int_power_div_base: |
1376 "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)" |
1390 "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)" |