author | nipkow |
Fri, 15 Nov 2002 18:02:25 +0100 | |
changeset 13716 | 73de0ef7cb25 |
parent 13601 | fd3e3d6b37b2 |
child 13788 | fd03c4ab89d4 |
permissions | -rw-r--r-- |
6917 | 1 |
(* Title: HOL/IntDiv.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1999 University of Cambridge |
|
5 |
||
6 |
The division operators div, mod and the divides relation "dvd" |
|
13183 | 7 |
|
8 |
Here is the division algorithm in ML: |
|
9 |
||
10 |
fun posDivAlg (a,b) = |
|
11 |
if a<b then (0,a) |
|
12 |
else let val (q,r) = posDivAlg(a, 2*b) |
|
13 |
in if 0<=r-b then (2*q+1, r-b) else (2*q, r) |
|
14 |
end |
|
15 |
||
16 |
fun negDivAlg (a,b) = |
|
17 |
if 0<=a+b then (~1,a+b) |
|
18 |
else let val (q,r) = negDivAlg(a, 2*b) |
|
19 |
in if 0<=r-b then (2*q+1, r-b) else (2*q, r) |
|
20 |
end; |
|
21 |
||
22 |
fun negateSnd (q,r:int) = (q,~r); |
|
23 |
||
24 |
fun divAlg (a,b) = if 0<=a then |
|
25 |
if b>0 then posDivAlg (a,b) |
|
26 |
else if a=0 then (0,0) |
|
27 |
else negateSnd (negDivAlg (~a,~b)) |
|
28 |
else |
|
29 |
if 0<b then negDivAlg (a,b) |
|
30 |
else negateSnd (posDivAlg (~a,~b)); |
|
6917 | 31 |
*) |
32 |
||
13183 | 33 |
|
13517 | 34 |
theory IntDiv = IntArith + Recdef |
35 |
files ("IntDiv_setup.ML"): |
|
13183 | 36 |
|
37 |
declare zless_nat_conj [simp] |
|
6917 | 38 |
|
39 |
constdefs |
|
40 |
quorem :: "(int*int) * (int*int) => bool" |
|
41 |
"quorem == %((a,b), (q,r)). |
|
42 |
a = b*q + r & |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
43 |
(if 0 < b then 0<=r & r<b else b<r & r <= 0)" |
6917 | 44 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
45 |
adjust :: "[int, int*int] => int*int" |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
46 |
"adjust b == %(q,r). if 0 <= r-b then (2*q + 1, r-b) |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
47 |
else (2*q, r)" |
6917 | 48 |
|
49 |
(** the division algorithm **) |
|
50 |
||
51 |
(*for the case a>=0, b>0*) |
|
52 |
consts posDivAlg :: "int*int => int*int" |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
53 |
recdef posDivAlg "inv_image less_than (%(a,b). nat(a - b + 1))" |
6917 | 54 |
"posDivAlg (a,b) = |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
55 |
(if (a<b | b<=0) then (0,a) |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
56 |
else adjust b (posDivAlg(a, 2*b)))" |
6917 | 57 |
|
58 |
(*for the case a<0, b>0*) |
|
59 |
consts negDivAlg :: "int*int => int*int" |
|
60 |
recdef negDivAlg "inv_image less_than (%(a,b). nat(- a - b))" |
|
61 |
"negDivAlg (a,b) = |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
62 |
(if (0<=a+b | b<=0) then (-1,a+b) |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
63 |
else adjust b (negDivAlg(a, 2*b)))" |
6917 | 64 |
|
65 |
(*for the general case b~=0*) |
|
66 |
||
67 |
constdefs |
|
68 |
negateSnd :: "int*int => int*int" |
|
69 |
"negateSnd == %(q,r). (q,-r)" |
|
70 |
||
71 |
(*The full division algorithm considers all possible signs for a, b |
|
72 |
including the special case a=0, b<0, because negDivAlg requires a<0*) |
|
73 |
divAlg :: "int*int => int*int" |
|
74 |
"divAlg == |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
75 |
%(a,b). if 0<=a then |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
76 |
if 0<=b then posDivAlg (a,b) |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
77 |
else if a=0 then (0,0) |
6917 | 78 |
else negateSnd (negDivAlg (-a,-b)) |
79 |
else |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
80 |
if 0<b then negDivAlg (a,b) |
6917 | 81 |
else negateSnd (posDivAlg (-a,-b))" |
82 |
||
83 |
instance |
|
13183 | 84 |
int :: "Divides.div" .. (*avoid clash with 'div' token*) |
6917 | 85 |
|
86 |
defs |
|
13183 | 87 |
div_def: "a div b == fst (divAlg (a,b))" |
88 |
mod_def: "a mod b == snd (divAlg (a,b))" |
|
89 |
||
90 |
||
91 |
||
92 |
(*** Uniqueness and monotonicity of quotients and remainders ***) |
|
93 |
||
94 |
lemma unique_quotient_lemma: |
|
95 |
"[| b*q' + r' <= b*q + r; 0 <= r'; 0 < b; r < b |] |
|
96 |
==> q' <= (q::int)" |
|
97 |
apply (subgoal_tac "r' + b * (q'-q) <= r") |
|
98 |
prefer 2 apply (simp add: zdiff_zmult_distrib2) |
|
99 |
apply (subgoal_tac "0 < b * (1 + q - q') ") |
|
100 |
apply (erule_tac [2] order_le_less_trans) |
|
101 |
prefer 2 apply (simp add: zdiff_zmult_distrib2 zadd_zmult_distrib2) |
|
102 |
apply (subgoal_tac "b * q' < b * (1 + q) ") |
|
103 |
prefer 2 apply (simp add: zdiff_zmult_distrib2 zadd_zmult_distrib2) |
|
104 |
apply (simp add: zmult_zless_cancel1) |
|
105 |
done |
|
106 |
||
107 |
lemma unique_quotient_lemma_neg: |
|
108 |
"[| b*q' + r' <= b*q + r; r <= 0; b < 0; b < r' |] |
|
109 |
==> q <= (q'::int)" |
|
110 |
by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma, |
|
111 |
auto) |
|
112 |
||
113 |
lemma unique_quotient: |
|
114 |
"[| quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); b ~= 0 |] |
|
115 |
==> q = q'" |
|
116 |
apply (simp add: quorem_def linorder_neq_iff split: split_if_asm) |
|
117 |
apply (blast intro: order_antisym |
|
118 |
dest: order_eq_refl [THEN unique_quotient_lemma] |
|
119 |
order_eq_refl [THEN unique_quotient_lemma_neg] sym)+ |
|
120 |
done |
|
121 |
||
122 |
||
123 |
lemma unique_remainder: |
|
124 |
"[| quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); b ~= 0 |] |
|
125 |
==> r = r'" |
|
126 |
apply (subgoal_tac "q = q'") |
|
127 |
apply (simp add: quorem_def) |
|
128 |
apply (blast intro: unique_quotient) |
|
129 |
done |
|
130 |
||
131 |
||
132 |
(*** Correctness of posDivAlg, the division algorithm for a>=0 and b>0 ***) |
|
133 |
||
134 |
lemma adjust_eq [simp]: |
|
135 |
"adjust b (q,r) = |
|
136 |
(let diff = r-b in |
|
137 |
if 0 <= diff then (2*q + 1, diff) |
|
138 |
else (2*q, r))" |
|
139 |
by (simp add: Let_def adjust_def) |
|
140 |
||
141 |
declare posDivAlg.simps [simp del] |
|
142 |
||
143 |
(**use with a simproc to avoid repeatedly proving the premise*) |
|
144 |
lemma posDivAlg_eqn: |
|
145 |
"0 < b ==> |
|
146 |
posDivAlg (a,b) = (if a<b then (0,a) else adjust b (posDivAlg(a, 2*b)))" |
|
147 |
by (rule posDivAlg.simps [THEN trans], simp) |
|
148 |
||
149 |
(*Correctness of posDivAlg: it computes quotients correctly*) |
|
150 |
lemma posDivAlg_correct [rule_format]: |
|
151 |
"0 <= a --> 0 < b --> quorem ((a, b), posDivAlg (a, b))" |
|
152 |
apply (induct_tac a b rule: posDivAlg.induct, auto) |
|
153 |
apply (simp_all add: quorem_def) |
|
154 |
(*base case: a<b*) |
|
155 |
apply (simp add: posDivAlg_eqn) |
|
156 |
(*main argument*) |
|
157 |
apply (subst posDivAlg_eqn, simp_all) |
|
158 |
apply (erule splitE) |
|
159 |
apply (auto simp add: zadd_zmult_distrib2 Let_def) |
|
160 |
done |
|
161 |
||
162 |
||
163 |
(*** Correctness of negDivAlg, the division algorithm for a<0 and b>0 ***) |
|
164 |
||
165 |
declare negDivAlg.simps [simp del] |
|
166 |
||
167 |
(**use with a simproc to avoid repeatedly proving the premise*) |
|
168 |
lemma negDivAlg_eqn: |
|
169 |
"0 < b ==> |
|
170 |
negDivAlg (a,b) = |
|
171 |
(if 0<=a+b then (-1,a+b) else adjust b (negDivAlg(a, 2*b)))" |
|
172 |
by (rule negDivAlg.simps [THEN trans], simp) |
|
173 |
||
174 |
(*Correctness of negDivAlg: it computes quotients correctly |
|
175 |
It doesn't work if a=0 because the 0/b equals 0, not -1*) |
|
176 |
lemma negDivAlg_correct [rule_format]: |
|
177 |
"a < 0 --> 0 < b --> quorem ((a, b), negDivAlg (a, b))" |
|
178 |
apply (induct_tac a b rule: negDivAlg.induct, auto) |
|
179 |
apply (simp_all add: quorem_def) |
|
180 |
(*base case: 0<=a+b*) |
|
181 |
apply (simp add: negDivAlg_eqn) |
|
182 |
(*main argument*) |
|
183 |
apply (subst negDivAlg_eqn, assumption) |
|
184 |
apply (erule splitE) |
|
185 |
apply (auto simp add: zadd_zmult_distrib2 Let_def) |
|
186 |
done |
|
187 |
||
188 |
||
189 |
(*** Existence shown by proving the division algorithm to be correct ***) |
|
190 |
||
191 |
(*the case a=0*) |
|
192 |
lemma quorem_0: "b ~= 0 ==> quorem ((0,b), (0,0))" |
|
193 |
by (auto simp add: quorem_def linorder_neq_iff) |
|
194 |
||
195 |
lemma posDivAlg_0 [simp]: "posDivAlg (0, b) = (0, 0)" |
|
196 |
by (subst posDivAlg.simps, auto) |
|
197 |
||
198 |
lemma negDivAlg_minus1 [simp]: "negDivAlg (-1, b) = (-1, b - 1)" |
|
199 |
by (subst negDivAlg.simps, auto) |
|
200 |
||
201 |
lemma negateSnd_eq [simp]: "negateSnd(q,r) = (q,-r)" |
|
202 |
by (unfold negateSnd_def, auto) |
|
203 |
||
204 |
lemma quorem_neg: "quorem ((-a,-b), qr) ==> quorem ((a,b), negateSnd qr)" |
|
205 |
by (auto simp add: split_ifs quorem_def) |
|
206 |
||
207 |
lemma divAlg_correct: "b ~= 0 ==> quorem ((a,b), divAlg(a,b))" |
|
208 |
by (force simp add: linorder_neq_iff quorem_0 divAlg_def quorem_neg |
|
209 |
posDivAlg_correct negDivAlg_correct) |
|
210 |
||
211 |
(** Arbitrary definitions for division by zero. Useful to simplify |
|
212 |
certain equations **) |
|
213 |
||
214 |
lemma DIVISION_BY_ZERO: "a div (0::int) = 0 & a mod (0::int) = a" |
|
215 |
by (simp add: div_def mod_def divAlg_def posDivAlg.simps) (*NOT for adding to default simpset*) |
|
216 |
||
217 |
(** Basic laws about division and remainder **) |
|
218 |
||
219 |
lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)" |
|
220 |
apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO) |
|
221 |
apply (cut_tac a = a and b = b in divAlg_correct) |
|
222 |
apply (auto simp add: quorem_def div_def mod_def) |
|
223 |
done |
|
224 |
||
13517 | 225 |
lemma zdiv_zmod_equality: "(b * (a div b) + (a mod b)) + k = (a::int)+k" |
226 |
by(simp add: zmod_zdiv_equality[symmetric]) |
|
227 |
||
228 |
lemma zdiv_zmod_equality2: "((a div b) * b + (a mod b)) + k = (a::int)+k" |
|
229 |
by(simp add: zmult_commute zmod_zdiv_equality[symmetric]) |
|
230 |
||
231 |
use "IntDiv_setup.ML" |
|
232 |
||
13183 | 233 |
lemma pos_mod_conj : "(0::int) < b ==> 0 <= a mod b & a mod b < b" |
234 |
apply (cut_tac a = a and b = b in divAlg_correct) |
|
235 |
apply (auto simp add: quorem_def mod_def) |
|
236 |
done |
|
237 |
||
238 |
lemmas pos_mod_sign = pos_mod_conj [THEN conjunct1, standard] |
|
239 |
and pos_mod_bound = pos_mod_conj [THEN conjunct2, standard] |
|
240 |
||
241 |
lemma neg_mod_conj : "b < (0::int) ==> a mod b <= 0 & b < a mod b" |
|
242 |
apply (cut_tac a = a and b = b in divAlg_correct) |
|
243 |
apply (auto simp add: quorem_def div_def mod_def) |
|
244 |
done |
|
245 |
||
246 |
lemmas neg_mod_sign = neg_mod_conj [THEN conjunct1, standard] |
|
247 |
and neg_mod_bound = neg_mod_conj [THEN conjunct2, standard] |
|
248 |
||
249 |
||
13260 | 250 |
|
13183 | 251 |
(** proving general properties of div and mod **) |
252 |
||
253 |
lemma quorem_div_mod: "b ~= 0 ==> quorem ((a, b), (a div b, a mod b))" |
|
254 |
apply (cut_tac a = a and b = b in zmod_zdiv_equality) |
|
255 |
apply (force simp add: quorem_def linorder_neq_iff pos_mod_sign pos_mod_bound |
|
256 |
neg_mod_sign neg_mod_bound) |
|
257 |
done |
|
258 |
||
259 |
lemma quorem_div: "[| quorem((a,b),(q,r)); b ~= 0 |] ==> a div b = q" |
|
260 |
by (simp add: quorem_div_mod [THEN unique_quotient]) |
|
261 |
||
262 |
lemma quorem_mod: "[| quorem((a,b),(q,r)); b ~= 0 |] ==> a mod b = r" |
|
263 |
by (simp add: quorem_div_mod [THEN unique_remainder]) |
|
264 |
||
265 |
lemma div_pos_pos_trivial: "[| (0::int) <= a; a < b |] ==> a div b = 0" |
|
266 |
apply (rule quorem_div) |
|
267 |
apply (auto simp add: quorem_def) |
|
268 |
done |
|
269 |
||
270 |
lemma div_neg_neg_trivial: "[| a <= (0::int); b < a |] ==> a div b = 0" |
|
271 |
apply (rule quorem_div) |
|
272 |
apply (auto simp add: quorem_def) |
|
273 |
done |
|
274 |
||
275 |
lemma div_pos_neg_trivial: "[| (0::int) < a; a+b <= 0 |] ==> a div b = -1" |
|
276 |
apply (rule quorem_div) |
|
277 |
apply (auto simp add: quorem_def) |
|
278 |
done |
|
279 |
||
280 |
(*There is no div_neg_pos_trivial because 0 div b = 0 would supersede it*) |
|
281 |
||
282 |
lemma mod_pos_pos_trivial: "[| (0::int) <= a; a < b |] ==> a mod b = a" |
|
283 |
apply (rule_tac q = 0 in quorem_mod) |
|
284 |
apply (auto simp add: quorem_def) |
|
285 |
done |
|
286 |
||
287 |
lemma mod_neg_neg_trivial: "[| a <= (0::int); b < a |] ==> a mod b = a" |
|
288 |
apply (rule_tac q = 0 in quorem_mod) |
|
289 |
apply (auto simp add: quorem_def) |
|
290 |
done |
|
291 |
||
292 |
lemma mod_pos_neg_trivial: "[| (0::int) < a; a+b <= 0 |] ==> a mod b = a+b" |
|
293 |
apply (rule_tac q = "-1" in quorem_mod) |
|
294 |
apply (auto simp add: quorem_def) |
|
295 |
done |
|
296 |
||
297 |
(*There is no mod_neg_pos_trivial...*) |
|
298 |
||
299 |
||
300 |
(*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*) |
|
301 |
lemma zdiv_zminus_zminus [simp]: "(-a) div (-b) = a div (b::int)" |
|
302 |
apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO) |
|
303 |
apply (simp add: quorem_div_mod [THEN quorem_neg, simplified, |
|
304 |
THEN quorem_div, THEN sym]) |
|
305 |
||
306 |
done |
|
307 |
||
308 |
(*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*) |
|
309 |
lemma zmod_zminus_zminus [simp]: "(-a) mod (-b) = - (a mod (b::int))" |
|
310 |
apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO) |
|
311 |
apply (subst quorem_div_mod [THEN quorem_neg, simplified, THEN quorem_mod], |
|
312 |
auto) |
|
313 |
done |
|
314 |
||
315 |
(*** div, mod and unary minus ***) |
|
316 |
||
317 |
lemma zminus1_lemma: |
|
318 |
"quorem((a,b),(q,r)) |
|
319 |
==> quorem ((-a,b), (if r=0 then -q else -q - 1), |
|
320 |
(if r=0 then 0 else b-r))" |
|
321 |
by (force simp add: split_ifs quorem_def linorder_neq_iff zdiff_zmult_distrib2) |
|
322 |
||
323 |
||
324 |
lemma zdiv_zminus1_eq_if: |
|
325 |
"b ~= (0::int) |
|
326 |
==> (-a) div b = |
|
327 |
(if a mod b = 0 then - (a div b) else - (a div b) - 1)" |
|
328 |
by (blast intro: quorem_div_mod [THEN zminus1_lemma, THEN quorem_div]) |
|
329 |
||
330 |
lemma zmod_zminus1_eq_if: |
|
331 |
"(-a::int) mod b = (if a mod b = 0 then 0 else b - (a mod b))" |
|
332 |
apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO) |
|
333 |
apply (blast intro: quorem_div_mod [THEN zminus1_lemma, THEN quorem_mod]) |
|
334 |
done |
|
335 |
||
336 |
lemma zdiv_zminus2: "a div (-b) = (-a::int) div b" |
|
337 |
by (cut_tac a = "-a" in zdiv_zminus_zminus, auto) |
|
338 |
||
339 |
lemma zmod_zminus2: "a mod (-b) = - ((-a::int) mod b)" |
|
340 |
by (cut_tac a = "-a" and b = b in zmod_zminus_zminus, auto) |
|
341 |
||
342 |
lemma zdiv_zminus2_eq_if: |
|
343 |
"b ~= (0::int) |
|
344 |
==> a div (-b) = |
|
345 |
(if a mod b = 0 then - (a div b) else - (a div b) - 1)" |
|
346 |
by (simp add: zdiv_zminus1_eq_if zdiv_zminus2) |
|
347 |
||
348 |
lemma zmod_zminus2_eq_if: |
|
349 |
"a mod (-b::int) = (if a mod b = 0 then 0 else (a mod b) - b)" |
|
350 |
by (simp add: zmod_zminus1_eq_if zmod_zminus2) |
|
351 |
||
352 |
||
353 |
(*** division of a number by itself ***) |
|
354 |
||
13524 | 355 |
lemma self_quotient_aux1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 <= q" |
13183 | 356 |
apply (subgoal_tac "0 < a*q") |
357 |
apply (simp add: int_0_less_mult_iff, arith) |
|
358 |
done |
|
359 |
||
13524 | 360 |
lemma self_quotient_aux2: "[| (0::int) < a; a = r + a*q; 0 <= r |] ==> q <= 1" |
13183 | 361 |
apply (subgoal_tac "0 <= a* (1-q) ") |
362 |
apply (simp add: int_0_le_mult_iff) |
|
363 |
apply (simp add: zdiff_zmult_distrib2) |
|
364 |
done |
|
365 |
||
366 |
lemma self_quotient: "[| quorem((a,a),(q,r)); a ~= (0::int) |] ==> q = 1" |
|
367 |
apply (simp add: split_ifs quorem_def linorder_neq_iff) |
|
13601 | 368 |
apply (rule order_antisym, safe, simp_all (no_asm_use)) |
13524 | 369 |
apply (rule_tac [3] a = "-a" and r = "-r" in self_quotient_aux1) |
370 |
apply (rule_tac a = "-a" and r = "-r" in self_quotient_aux2) |
|
13601 | 371 |
apply (force intro: self_quotient_aux1 self_quotient_aux2 simp only: zadd_commute zmult_zminus)+ |
13183 | 372 |
done |
373 |
||
374 |
lemma self_remainder: "[| quorem((a,a),(q,r)); a ~= (0::int) |] ==> r = 0" |
|
375 |
apply (frule self_quotient, assumption) |
|
376 |
apply (simp add: quorem_def) |
|
377 |
done |
|
378 |
||
379 |
lemma zdiv_self [simp]: "a ~= 0 ==> a div a = (1::int)" |
|
380 |
by (simp add: quorem_div_mod [THEN self_quotient]) |
|
381 |
||
382 |
(*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *) |
|
383 |
lemma zmod_self [simp]: "a mod a = (0::int)" |
|
384 |
apply (case_tac "a = 0", simp add: DIVISION_BY_ZERO) |
|
385 |
apply (simp add: quorem_div_mod [THEN self_remainder]) |
|
386 |
done |
|
387 |
||
388 |
||
389 |
(*** Computation of division and remainder ***) |
|
390 |
||
391 |
lemma zdiv_zero [simp]: "(0::int) div b = 0" |
|
392 |
by (simp add: div_def divAlg_def) |
|
393 |
||
394 |
lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1" |
|
395 |
by (simp add: div_def divAlg_def) |
|
396 |
||
397 |
lemma zmod_zero [simp]: "(0::int) mod b = 0" |
|
398 |
by (simp add: mod_def divAlg_def) |
|
399 |
||
400 |
lemma zdiv_minus1: "(0::int) < b ==> -1 div b = -1" |
|
401 |
by (simp add: div_def divAlg_def) |
|
402 |
||
403 |
lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1" |
|
404 |
by (simp add: mod_def divAlg_def) |
|
405 |
||
406 |
(** a positive, b positive **) |
|
407 |
||
408 |
lemma div_pos_pos: "[| 0 < a; 0 <= b |] ==> a div b = fst (posDivAlg(a,b))" |
|
409 |
by (simp add: div_def divAlg_def) |
|
410 |
||
411 |
lemma mod_pos_pos: "[| 0 < a; 0 <= b |] ==> a mod b = snd (posDivAlg(a,b))" |
|
412 |
by (simp add: mod_def divAlg_def) |
|
413 |
||
414 |
(** a negative, b positive **) |
|
415 |
||
416 |
lemma div_neg_pos: "[| a < 0; 0 < b |] ==> a div b = fst (negDivAlg(a,b))" |
|
417 |
by (simp add: div_def divAlg_def) |
|
418 |
||
419 |
lemma mod_neg_pos: "[| a < 0; 0 < b |] ==> a mod b = snd (negDivAlg(a,b))" |
|
420 |
by (simp add: mod_def divAlg_def) |
|
421 |
||
422 |
(** a positive, b negative **) |
|
423 |
||
424 |
lemma div_pos_neg: |
|
425 |
"[| 0 < a; b < 0 |] ==> a div b = fst (negateSnd(negDivAlg(-a,-b)))" |
|
426 |
by (simp add: div_def divAlg_def) |
|
427 |
||
428 |
lemma mod_pos_neg: |
|
429 |
"[| 0 < a; b < 0 |] ==> a mod b = snd (negateSnd(negDivAlg(-a,-b)))" |
|
430 |
by (simp add: mod_def divAlg_def) |
|
431 |
||
432 |
(** a negative, b negative **) |
|
433 |
||
434 |
lemma div_neg_neg: |
|
435 |
"[| a < 0; b <= 0 |] ==> a div b = fst (negateSnd(posDivAlg(-a,-b)))" |
|
436 |
by (simp add: div_def divAlg_def) |
|
437 |
||
438 |
lemma mod_neg_neg: |
|
439 |
"[| a < 0; b <= 0 |] ==> a mod b = snd (negateSnd(posDivAlg(-a,-b)))" |
|
440 |
by (simp add: mod_def divAlg_def) |
|
441 |
||
442 |
text {*Simplify expresions in which div and mod combine numerical constants*} |
|
443 |
||
444 |
declare div_pos_pos [of "number_of v" "number_of w", standard, simp] |
|
445 |
declare div_neg_pos [of "number_of v" "number_of w", standard, simp] |
|
446 |
declare div_pos_neg [of "number_of v" "number_of w", standard, simp] |
|
447 |
declare div_neg_neg [of "number_of v" "number_of w", standard, simp] |
|
448 |
||
449 |
declare mod_pos_pos [of "number_of v" "number_of w", standard, simp] |
|
450 |
declare mod_neg_pos [of "number_of v" "number_of w", standard, simp] |
|
451 |
declare mod_pos_neg [of "number_of v" "number_of w", standard, simp] |
|
452 |
declare mod_neg_neg [of "number_of v" "number_of w", standard, simp] |
|
453 |
||
454 |
declare posDivAlg_eqn [of "number_of v" "number_of w", standard, simp] |
|
455 |
declare negDivAlg_eqn [of "number_of v" "number_of w", standard, simp] |
|
456 |
||
457 |
||
458 |
(** Special-case simplification **) |
|
459 |
||
460 |
lemma zmod_1 [simp]: "a mod (1::int) = 0" |
|
461 |
apply (cut_tac a = a and b = 1 in pos_mod_sign) |
|
462 |
apply (cut_tac [2] a = a and b = 1 in pos_mod_bound, auto) |
|
463 |
done |
|
464 |
||
465 |
lemma zdiv_1 [simp]: "a div (1::int) = a" |
|
466 |
by (cut_tac a = a and b = 1 in zmod_zdiv_equality, auto) |
|
467 |
||
468 |
lemma zmod_minus1_right [simp]: "a mod (-1::int) = 0" |
|
469 |
apply (cut_tac a = a and b = "-1" in neg_mod_sign) |
|
470 |
apply (cut_tac [2] a = a and b = "-1" in neg_mod_bound, auto) |
|
471 |
done |
|
472 |
||
473 |
lemma zdiv_minus1_right [simp]: "a div (-1::int) = -a" |
|
474 |
by (cut_tac a = a and b = "-1" in zmod_zdiv_equality, auto) |
|
475 |
||
476 |
(** The last remaining special cases for constant arithmetic: |
|
477 |
1 div z and 1 mod z **) |
|
478 |
||
479 |
declare div_pos_pos [OF int_0_less_1, of "number_of w", standard, simp] |
|
480 |
declare div_pos_neg [OF int_0_less_1, of "number_of w", standard, simp] |
|
481 |
declare mod_pos_pos [OF int_0_less_1, of "number_of w", standard, simp] |
|
482 |
declare mod_pos_neg [OF int_0_less_1, of "number_of w", standard, simp] |
|
483 |
||
484 |
declare posDivAlg_eqn [of concl: 1 "number_of w", standard, simp] |
|
485 |
declare negDivAlg_eqn [of concl: 1 "number_of w", standard, simp] |
|
486 |
||
487 |
||
488 |
(*** Monotonicity in the first argument (divisor) ***) |
|
489 |
||
490 |
lemma zdiv_mono1: "[| a <= a'; 0 < (b::int) |] ==> a div b <= a' div b" |
|
491 |
apply (cut_tac a = a and b = b in zmod_zdiv_equality) |
|
492 |
apply (cut_tac a = a' and b = b in zmod_zdiv_equality) |
|
493 |
apply (rule unique_quotient_lemma) |
|
494 |
apply (erule subst) |
|
495 |
apply (erule subst) |
|
496 |
apply (simp_all add: pos_mod_sign pos_mod_bound) |
|
497 |
done |
|
498 |
||
499 |
lemma zdiv_mono1_neg: "[| a <= a'; (b::int) < 0 |] ==> a' div b <= a div b" |
|
500 |
apply (cut_tac a = a and b = b in zmod_zdiv_equality) |
|
501 |
apply (cut_tac a = a' and b = b in zmod_zdiv_equality) |
|
502 |
apply (rule unique_quotient_lemma_neg) |
|
503 |
apply (erule subst) |
|
504 |
apply (erule subst) |
|
505 |
apply (simp_all add: neg_mod_sign neg_mod_bound) |
|
506 |
done |
|
6917 | 507 |
|
508 |
||
13183 | 509 |
(*** Monotonicity in the second argument (dividend) ***) |
510 |
||
511 |
lemma q_pos_lemma: |
|
512 |
"[| 0 <= b'*q' + r'; r' < b'; 0 < b' |] ==> 0 <= (q'::int)" |
|
513 |
apply (subgoal_tac "0 < b'* (q' + 1) ") |
|
514 |
apply (simp add: int_0_less_mult_iff) |
|
515 |
apply (simp add: zadd_zmult_distrib2) |
|
516 |
done |
|
517 |
||
518 |
lemma zdiv_mono2_lemma: |
|
519 |
"[| b*q + r = b'*q' + r'; 0 <= b'*q' + r'; |
|
520 |
r' < b'; 0 <= r; 0 < b'; b' <= b |] |
|
521 |
==> q <= (q'::int)" |
|
522 |
apply (frule q_pos_lemma, assumption+) |
|
523 |
apply (subgoal_tac "b*q < b* (q' + 1) ") |
|
524 |
apply (simp add: zmult_zless_cancel1) |
|
525 |
apply (subgoal_tac "b*q = r' - r + b'*q'") |
|
526 |
prefer 2 apply simp |
|
527 |
apply (simp (no_asm_simp) add: zadd_zmult_distrib2) |
|
528 |
apply (subst zadd_commute, rule zadd_zless_mono, arith) |
|
529 |
apply (rule zmult_zle_mono1, auto) |
|
530 |
done |
|
531 |
||
532 |
lemma zdiv_mono2: |
|
533 |
"[| (0::int) <= a; 0 < b'; b' <= b |] ==> a div b <= a div b'" |
|
534 |
apply (subgoal_tac "b ~= 0") |
|
535 |
prefer 2 apply arith |
|
536 |
apply (cut_tac a = a and b = b in zmod_zdiv_equality) |
|
537 |
apply (cut_tac a = a and b = b' in zmod_zdiv_equality) |
|
538 |
apply (rule zdiv_mono2_lemma) |
|
539 |
apply (erule subst) |
|
540 |
apply (erule subst) |
|
541 |
apply (simp_all add: pos_mod_sign pos_mod_bound) |
|
542 |
done |
|
543 |
||
544 |
lemma q_neg_lemma: |
|
545 |
"[| b'*q' + r' < 0; 0 <= r'; 0 < b' |] ==> q' <= (0::int)" |
|
546 |
apply (subgoal_tac "b'*q' < 0") |
|
547 |
apply (simp add: zmult_less_0_iff, arith) |
|
548 |
done |
|
549 |
||
550 |
lemma zdiv_mono2_neg_lemma: |
|
551 |
"[| b*q + r = b'*q' + r'; b'*q' + r' < 0; |
|
552 |
r < b; 0 <= r'; 0 < b'; b' <= b |] |
|
553 |
==> q' <= (q::int)" |
|
554 |
apply (frule q_neg_lemma, assumption+) |
|
555 |
apply (subgoal_tac "b*q' < b* (q + 1) ") |
|
556 |
apply (simp add: zmult_zless_cancel1) |
|
557 |
apply (simp add: zadd_zmult_distrib2) |
|
558 |
apply (subgoal_tac "b*q' <= b'*q'") |
|
559 |
prefer 2 apply (simp add: zmult_zle_mono1_neg) |
|
560 |
apply (subgoal_tac "b'*q' < b + b*q") |
|
561 |
apply arith |
|
562 |
apply simp |
|
563 |
done |
|
564 |
||
565 |
lemma zdiv_mono2_neg: |
|
566 |
"[| a < (0::int); 0 < b'; b' <= b |] ==> a div b' <= a div b" |
|
567 |
apply (cut_tac a = a and b = b in zmod_zdiv_equality) |
|
568 |
apply (cut_tac a = a and b = b' in zmod_zdiv_equality) |
|
569 |
apply (rule zdiv_mono2_neg_lemma) |
|
570 |
apply (erule subst) |
|
571 |
apply (erule subst) |
|
572 |
apply (simp_all add: pos_mod_sign pos_mod_bound) |
|
573 |
done |
|
574 |
||
575 |
||
576 |
(*** More algebraic laws for div and mod ***) |
|
577 |
||
578 |
(** proving (a*b) div c = a * (b div c) + a * (b mod c) **) |
|
579 |
||
580 |
lemma zmult1_lemma: |
|
581 |
"[| quorem((b,c),(q,r)); c ~= 0 |] |
|
582 |
==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))" |
|
583 |
by (force simp add: split_ifs quorem_def linorder_neq_iff zadd_zmult_distrib2 |
|
13517 | 584 |
pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound) |
13183 | 585 |
|
586 |
lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)" |
|
587 |
apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO) |
|
588 |
apply (blast intro: quorem_div_mod [THEN zmult1_lemma, THEN quorem_div]) |
|
589 |
done |
|
590 |
||
591 |
lemma zmod_zmult1_eq: "(a*b) mod c = a*(b mod c) mod (c::int)" |
|
592 |
apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO) |
|
593 |
apply (blast intro: quorem_div_mod [THEN zmult1_lemma, THEN quorem_mod]) |
|
594 |
done |
|
595 |
||
596 |
lemma zmod_zmult1_eq': "(a*b) mod (c::int) = ((a mod c) * b) mod c" |
|
597 |
apply (rule trans) |
|
598 |
apply (rule_tac s = "b*a mod c" in trans) |
|
599 |
apply (rule_tac [2] zmod_zmult1_eq) |
|
600 |
apply (simp_all add: zmult_commute) |
|
601 |
done |
|
602 |
||
603 |
lemma zmod_zmult_distrib: "(a*b) mod (c::int) = ((a mod c) * (b mod c)) mod c" |
|
604 |
apply (rule zmod_zmult1_eq' [THEN trans]) |
|
605 |
apply (rule zmod_zmult1_eq) |
|
606 |
done |
|
607 |
||
608 |
lemma zdiv_zmult_self1 [simp]: "b ~= (0::int) ==> (a*b) div b = a" |
|
609 |
by (simp add: zdiv_zmult1_eq) |
|
610 |
||
611 |
lemma zdiv_zmult_self2 [simp]: "b ~= (0::int) ==> (b*a) div b = a" |
|
612 |
by (subst zmult_commute, erule zdiv_zmult_self1) |
|
613 |
||
614 |
lemma zmod_zmult_self1 [simp]: "(a*b) mod b = (0::int)" |
|
615 |
by (simp add: zmod_zmult1_eq) |
|
616 |
||
617 |
lemma zmod_zmult_self2 [simp]: "(b*a) mod b = (0::int)" |
|
618 |
by (simp add: zmult_commute zmod_zmult1_eq) |
|
619 |
||
620 |
lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)" |
|
13517 | 621 |
proof |
622 |
assume "m mod d = 0" |
|
623 |
from this zmod_zdiv_equality[of m d] show "EX q::int. m = d*q" by auto |
|
624 |
next |
|
625 |
assume "EX q::int. m = d*q" |
|
626 |
thus "m mod d = 0" by auto |
|
627 |
qed |
|
13183 | 628 |
|
629 |
declare zmod_eq_0_iff [THEN iffD1, dest!] |
|
630 |
||
13716 | 631 |
lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))" |
632 |
by(simp add:dvd_def zmod_eq_0_iff) |
|
13183 | 633 |
|
634 |
(** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **) |
|
635 |
||
636 |
lemma zadd1_lemma: |
|
637 |
"[| quorem((a,c),(aq,ar)); quorem((b,c),(bq,br)); c ~= 0 |] |
|
638 |
==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))" |
|
639 |
by (force simp add: split_ifs quorem_def linorder_neq_iff zadd_zmult_distrib2 |
|
13517 | 640 |
pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound) |
13183 | 641 |
|
642 |
(*NOT suitable for rewriting: the RHS has an instance of the LHS*) |
|
643 |
lemma zdiv_zadd1_eq: |
|
644 |
"(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)" |
|
645 |
apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO) |
|
646 |
apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_div) |
|
647 |
done |
|
648 |
||
649 |
lemma zmod_zadd1_eq: "(a+b) mod (c::int) = (a mod c + b mod c) mod c" |
|
650 |
apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO) |
|
651 |
apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_mod) |
|
652 |
done |
|
653 |
||
654 |
lemma mod_div_trivial [simp]: "(a mod b) div b = (0::int)" |
|
655 |
apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO) |
|
656 |
apply (auto simp add: linorder_neq_iff pos_mod_sign pos_mod_bound |
|
657 |
div_pos_pos_trivial neg_mod_sign neg_mod_bound div_neg_neg_trivial) |
|
658 |
done |
|
659 |
||
660 |
lemma mod_mod_trivial [simp]: "(a mod b) mod b = a mod (b::int)" |
|
661 |
apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO) |
|
662 |
apply (force simp add: linorder_neq_iff pos_mod_sign pos_mod_bound |
|
663 |
mod_pos_pos_trivial neg_mod_sign neg_mod_bound |
|
664 |
mod_neg_neg_trivial) |
|
665 |
done |
|
666 |
||
667 |
lemma zmod_zadd_left_eq: "(a+b) mod (c::int) = ((a mod c) + b) mod c" |
|
668 |
apply (rule trans [symmetric]) |
|
669 |
apply (rule zmod_zadd1_eq, simp) |
|
670 |
apply (rule zmod_zadd1_eq [symmetric]) |
|
671 |
done |
|
672 |
||
673 |
lemma zmod_zadd_right_eq: "(a+b) mod (c::int) = (a + (b mod c)) mod c" |
|
674 |
apply (rule trans [symmetric]) |
|
675 |
apply (rule zmod_zadd1_eq, simp) |
|
676 |
apply (rule zmod_zadd1_eq [symmetric]) |
|
677 |
done |
|
678 |
||
679 |
lemma zdiv_zadd_self1[simp]: "a ~= (0::int) ==> (a+b) div a = b div a + 1" |
|
680 |
by (simp add: zdiv_zadd1_eq) |
|
681 |
||
682 |
lemma zdiv_zadd_self2[simp]: "a ~= (0::int) ==> (b+a) div a = b div a + 1" |
|
683 |
by (simp add: zdiv_zadd1_eq) |
|
684 |
||
685 |
lemma zmod_zadd_self1[simp]: "(a+b) mod a = b mod (a::int)" |
|
686 |
apply (case_tac "a = 0", simp add: DIVISION_BY_ZERO) |
|
687 |
apply (simp add: zmod_zadd1_eq) |
|
688 |
done |
|
689 |
||
690 |
lemma zmod_zadd_self2[simp]: "(b+a) mod a = b mod (a::int)" |
|
691 |
apply (case_tac "a = 0", simp add: DIVISION_BY_ZERO) |
|
692 |
apply (simp add: zmod_zadd1_eq) |
|
693 |
done |
|
694 |
||
695 |
||
696 |
(*** proving a div (b*c) = (a div b) div c ***) |
|
697 |
||
698 |
(*The condition c>0 seems necessary. Consider that 7 div ~6 = ~2 but |
|
699 |
7 div 2 div ~3 = 3 div ~3 = ~1. The subcase (a div b) mod c = 0 seems |
|
700 |
to cause particular problems.*) |
|
701 |
||
702 |
(** first, four lemmas to bound the remainder for the cases b<0 and b>0 **) |
|
703 |
||
13524 | 704 |
lemma zmult2_lemma_aux1: "[| (0::int) < c; b < r; r <= 0 |] ==> b*c < b*(q mod c) + r" |
13183 | 705 |
apply (subgoal_tac "b * (c - q mod c) < r * 1") |
706 |
apply (simp add: zdiff_zmult_distrib2) |
|
707 |
apply (rule order_le_less_trans) |
|
708 |
apply (erule_tac [2] zmult_zless_mono1) |
|
709 |
apply (rule zmult_zle_mono2_neg) |
|
710 |
apply (auto simp add: zcompare_rls zadd_commute [of 1] |
|
711 |
add1_zle_eq pos_mod_bound) |
|
712 |
done |
|
713 |
||
13524 | 714 |
lemma zmult2_lemma_aux2: "[| (0::int) < c; b < r; r <= 0 |] ==> b * (q mod c) + r <= 0" |
13183 | 715 |
apply (subgoal_tac "b * (q mod c) <= 0") |
716 |
apply arith |
|
717 |
apply (simp add: zmult_le_0_iff pos_mod_sign) |
|
718 |
done |
|
719 |
||
13524 | 720 |
lemma zmult2_lemma_aux3: "[| (0::int) < c; 0 <= r; r < b |] ==> 0 <= b * (q mod c) + r" |
13183 | 721 |
apply (subgoal_tac "0 <= b * (q mod c) ") |
722 |
apply arith |
|
723 |
apply (simp add: int_0_le_mult_iff pos_mod_sign) |
|
724 |
done |
|
725 |
||
13524 | 726 |
lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 <= r; r < b |] ==> b * (q mod c) + r < b * c" |
13183 | 727 |
apply (subgoal_tac "r * 1 < b * (c - q mod c) ") |
728 |
apply (simp add: zdiff_zmult_distrib2) |
|
729 |
apply (rule order_less_le_trans) |
|
730 |
apply (erule zmult_zless_mono1) |
|
731 |
apply (rule_tac [2] zmult_zle_mono2) |
|
732 |
apply (auto simp add: zcompare_rls zadd_commute [of 1] |
|
733 |
add1_zle_eq pos_mod_bound) |
|
734 |
done |
|
735 |
||
736 |
lemma zmult2_lemma: "[| quorem ((a,b), (q,r)); b ~= 0; 0 < c |] |
|
737 |
==> quorem ((a, b*c), (q div c, b*(q mod c) + r))" |
|
13517 | 738 |
by (auto simp add: zmult_ac quorem_def linorder_neq_iff |
13183 | 739 |
int_0_less_mult_iff zadd_zmult_distrib2 [symmetric] |
13524 | 740 |
zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4) |
13183 | 741 |
|
742 |
lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c" |
|
743 |
apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO) |
|
744 |
apply (force simp add: quorem_div_mod [THEN zmult2_lemma, THEN quorem_div]) |
|
745 |
done |
|
746 |
||
747 |
lemma zmod_zmult2_eq: |
|
748 |
"(0::int) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b" |
|
749 |
apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO) |
|
750 |
apply (force simp add: quorem_div_mod [THEN zmult2_lemma, THEN quorem_mod]) |
|
751 |
done |
|
752 |
||
753 |
||
754 |
(*** Cancellation of common factors in div ***) |
|
755 |
||
13524 | 756 |
lemma zdiv_zmult_zmult1_aux1: "[| (0::int) < b; c ~= 0 |] ==> (c*a) div (c*b) = a div b" |
13183 | 757 |
by (subst zdiv_zmult2_eq, auto) |
758 |
||
13524 | 759 |
lemma zdiv_zmult_zmult1_aux2: "[| b < (0::int); c ~= 0 |] ==> (c*a) div (c*b) = a div b" |
13183 | 760 |
apply (subgoal_tac " (c * (-a)) div (c * (-b)) = (-a) div (-b) ") |
13524 | 761 |
apply (rule_tac [2] zdiv_zmult_zmult1_aux1, auto) |
13183 | 762 |
done |
763 |
||
764 |
lemma zdiv_zmult_zmult1: "c ~= (0::int) ==> (c*a) div (c*b) = a div b" |
|
765 |
apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO) |
|
13524 | 766 |
apply (auto simp add: linorder_neq_iff zdiv_zmult_zmult1_aux1 zdiv_zmult_zmult1_aux2) |
13183 | 767 |
done |
768 |
||
769 |
lemma zdiv_zmult_zmult2: "c ~= (0::int) ==> (a*c) div (b*c) = a div b" |
|
770 |
apply (drule zdiv_zmult_zmult1) |
|
771 |
apply (auto simp add: zmult_commute) |
|
772 |
done |
|
773 |
||
774 |
||
775 |
||
776 |
(*** Distribution of factors over mod ***) |
|
777 |
||
13524 | 778 |
lemma zmod_zmult_zmult1_aux1: "[| (0::int) < b; c ~= 0 |] ==> (c*a) mod (c*b) = c * (a mod b)" |
13183 | 779 |
by (subst zmod_zmult2_eq, auto) |
780 |
||
13524 | 781 |
lemma zmod_zmult_zmult1_aux2: "[| b < (0::int); c ~= 0 |] ==> (c*a) mod (c*b) = c * (a mod b)" |
13183 | 782 |
apply (subgoal_tac " (c * (-a)) mod (c * (-b)) = c * ((-a) mod (-b))") |
13524 | 783 |
apply (rule_tac [2] zmod_zmult_zmult1_aux1, auto) |
13183 | 784 |
done |
785 |
||
786 |
lemma zmod_zmult_zmult1: "(c*a) mod (c*b) = (c::int) * (a mod b)" |
|
787 |
apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO) |
|
788 |
apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO) |
|
13524 | 789 |
apply (auto simp add: linorder_neq_iff zmod_zmult_zmult1_aux1 zmod_zmult_zmult1_aux2) |
13183 | 790 |
done |
791 |
||
792 |
lemma zmod_zmult_zmult2: "(a*c) mod (b*c) = (a mod b) * (c::int)" |
|
793 |
apply (cut_tac c = c in zmod_zmult_zmult1) |
|
794 |
apply (auto simp add: zmult_commute) |
|
795 |
done |
|
796 |
||
797 |
||
13260 | 798 |
subsection {*splitting rules for div and mod*} |
799 |
||
800 |
text{*The proofs of the two lemmas below are essentially identical*} |
|
801 |
||
802 |
lemma split_pos_lemma: |
|
803 |
"0<k ==> |
|
804 |
P(n div k :: int)(n mod k) = (\<forall>i j. 0<=j & j<k & n = k*i + j --> P i j)" |
|
805 |
apply (rule iffI) |
|
806 |
apply clarify |
|
807 |
apply (erule_tac P="P ?x ?y" in rev_mp) |
|
808 |
apply (subst zmod_zadd1_eq) |
|
809 |
apply (subst zdiv_zadd1_eq) |
|
810 |
apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial) |
|
811 |
txt{*converse direction*} |
|
812 |
apply (drule_tac x = "n div k" in spec) |
|
813 |
apply (drule_tac x = "n mod k" in spec) |
|
13517 | 814 |
apply (simp add: pos_mod_bound pos_mod_sign) |
13260 | 815 |
done |
816 |
||
817 |
lemma split_neg_lemma: |
|
818 |
"k<0 ==> |
|
819 |
P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j<=0 & n = k*i + j --> P i j)" |
|
820 |
apply (rule iffI) |
|
821 |
apply clarify |
|
822 |
apply (erule_tac P="P ?x ?y" in rev_mp) |
|
823 |
apply (subst zmod_zadd1_eq) |
|
824 |
apply (subst zdiv_zadd1_eq) |
|
825 |
apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial) |
|
826 |
txt{*converse direction*} |
|
827 |
apply (drule_tac x = "n div k" in spec) |
|
828 |
apply (drule_tac x = "n mod k" in spec) |
|
13517 | 829 |
apply (simp add: neg_mod_bound neg_mod_sign) |
13260 | 830 |
done |
831 |
||
832 |
lemma split_zdiv: |
|
833 |
"P(n div k :: int) = |
|
834 |
((k = 0 --> P 0) & |
|
835 |
(0<k --> (\<forall>i j. 0<=j & j<k & n = k*i + j --> P i)) & |
|
836 |
(k<0 --> (\<forall>i j. k<j & j<=0 & n = k*i + j --> P i)))" |
|
837 |
apply (case_tac "k=0") |
|
838 |
apply (simp add: DIVISION_BY_ZERO) |
|
839 |
apply (simp only: linorder_neq_iff) |
|
840 |
apply (erule disjE) |
|
841 |
apply (simp_all add: split_pos_lemma [of concl: "%x y. P x"] |
|
842 |
split_neg_lemma [of concl: "%x y. P x"]) |
|
843 |
done |
|
844 |
||
845 |
lemma split_zmod: |
|
846 |
"P(n mod k :: int) = |
|
847 |
((k = 0 --> P n) & |
|
848 |
(0<k --> (\<forall>i j. 0<=j & j<k & n = k*i + j --> P j)) & |
|
849 |
(k<0 --> (\<forall>i j. k<j & j<=0 & n = k*i + j --> P j)))" |
|
850 |
apply (case_tac "k=0") |
|
851 |
apply (simp add: DIVISION_BY_ZERO) |
|
852 |
apply (simp only: linorder_neq_iff) |
|
853 |
apply (erule disjE) |
|
854 |
apply (simp_all add: split_pos_lemma [of concl: "%x y. P y"] |
|
855 |
split_neg_lemma [of concl: "%x y. P y"]) |
|
856 |
done |
|
857 |
||
858 |
(* Enable arith to deal with div 2 and mod 2: *) |
|
13266
2a6ad4357d72
modified Larry's changes to make div/mod a numeral work in arith.
nipkow
parents:
13260
diff
changeset
|
859 |
declare split_zdiv [of _ _ "number_of k", simplified, standard, arith_split] |
2a6ad4357d72
modified Larry's changes to make div/mod a numeral work in arith.
nipkow
parents:
13260
diff
changeset
|
860 |
declare split_zmod [of _ _ "number_of k", simplified, standard, arith_split] |
13260 | 861 |
|
862 |
||
863 |
subsection{*Speeding up the division algorithm with shifting*} |
|
13183 | 864 |
|
865 |
(** computing div by shifting **) |
|
866 |
||
867 |
lemma pos_zdiv_mult_2: "(0::int) <= a ==> (1 + 2*b) div (2*a) = b div a" |
|
868 |
apply (case_tac "a = 0", simp add: DIVISION_BY_ZERO) |
|
869 |
apply (subgoal_tac "1 <= a") |
|
870 |
prefer 2 apply arith |
|
871 |
apply (subgoal_tac "1 < a * 2") |
|
872 |
prefer 2 apply arith |
|
873 |
apply (subgoal_tac "2* (1 + b mod a) <= 2*a") |
|
874 |
apply (rule_tac [2] zmult_zle_mono2) |
|
875 |
apply (auto simp add: zadd_commute [of 1] zmult_commute add1_zle_eq |
|
876 |
pos_mod_bound) |
|
877 |
apply (subst zdiv_zadd1_eq) |
|
878 |
apply (simp add: zdiv_zmult_zmult2 zmod_zmult_zmult2 div_pos_pos_trivial) |
|
879 |
apply (subst div_pos_pos_trivial) |
|
880 |
apply (auto simp add: mod_pos_pos_trivial) |
|
881 |
apply (subgoal_tac "0 <= b mod a", arith) |
|
882 |
apply (simp add: pos_mod_sign) |
|
883 |
done |
|
884 |
||
885 |
||
886 |
lemma neg_zdiv_mult_2: "a <= (0::int) ==> (1 + 2*b) div (2*a) = (b+1) div a" |
|
887 |
apply (subgoal_tac " (1 + 2* (-b - 1)) div (2 * (-a)) = (-b - 1) div (-a) ") |
|
888 |
apply (rule_tac [2] pos_zdiv_mult_2) |
|
889 |
apply (auto simp add: zmult_zminus_right) |
|
890 |
apply (subgoal_tac " (-1 - (2 * b)) = - (1 + (2 * b))") |
|
891 |
apply (simp only: zdiv_zminus_zminus zdiff_def zminus_zadd_distrib [symmetric], |
|
892 |
simp) |
|
893 |
done |
|
894 |
||
895 |
||
896 |
(*Not clear why this must be proved separately; probably number_of causes |
|
897 |
simplification problems*) |
|
898 |
lemma not_0_le_lemma: "~ 0 <= x ==> x <= (0::int)" |
|
899 |
by auto |
|
900 |
||
901 |
lemma zdiv_number_of_BIT[simp]: |
|
902 |
"number_of (v BIT b) div number_of (w BIT False) = |
|
903 |
(if ~b | (0::int) <= number_of w |
|
904 |
then number_of v div (number_of w) |
|
905 |
else (number_of v + (1::int)) div (number_of w))" |
|
906 |
apply (simp only: zadd_assoc number_of_BIT) |
|
907 |
(*create subgoal because the next step can't simplify numerals*) |
|
908 |
apply (subgoal_tac "2 ~= (0::int) ") |
|
909 |
apply (simp del: bin_arith_extra_simps |
|
13260 | 910 |
add: zdiv_zmult_zmult1 pos_zdiv_mult_2 not_0_le_lemma neg_zdiv_mult_2, simp) |
13183 | 911 |
done |
912 |
||
913 |
||
914 |
(** computing mod by shifting (proofs resemble those for div) **) |
|
915 |
||
916 |
lemma pos_zmod_mult_2: |
|
917 |
"(0::int) <= a ==> (1 + 2*b) mod (2*a) = 1 + 2 * (b mod a)" |
|
918 |
apply (case_tac "a = 0", simp add: DIVISION_BY_ZERO) |
|
919 |
apply (subgoal_tac "1 <= a") |
|
920 |
prefer 2 apply arith |
|
921 |
apply (subgoal_tac "1 < a * 2") |
|
922 |
prefer 2 apply arith |
|
923 |
apply (subgoal_tac "2* (1 + b mod a) <= 2*a") |
|
924 |
apply (rule_tac [2] zmult_zle_mono2) |
|
925 |
apply (auto simp add: zadd_commute [of 1] zmult_commute add1_zle_eq |
|
926 |
pos_mod_bound) |
|
927 |
apply (subst zmod_zadd1_eq) |
|
928 |
apply (simp add: zmod_zmult_zmult2 mod_pos_pos_trivial) |
|
929 |
apply (rule mod_pos_pos_trivial) |
|
930 |
apply (auto simp add: mod_pos_pos_trivial) |
|
931 |
apply (subgoal_tac "0 <= b mod a", arith) |
|
932 |
apply (simp add: pos_mod_sign) |
|
933 |
done |
|
934 |
||
935 |
||
936 |
lemma neg_zmod_mult_2: |
|
937 |
"a <= (0::int) ==> (1 + 2*b) mod (2*a) = 2 * ((b+1) mod a) - 1" |
|
938 |
apply (subgoal_tac "(1 + 2* (-b - 1)) mod (2* (-a)) = |
|
939 |
1 + 2* ((-b - 1) mod (-a))") |
|
940 |
apply (rule_tac [2] pos_zmod_mult_2) |
|
941 |
apply (auto simp add: zmult_zminus_right) |
|
942 |
apply (subgoal_tac " (-1 - (2 * b)) = - (1 + (2 * b))") |
|
943 |
prefer 2 apply simp |
|
944 |
apply (simp only: zmod_zminus_zminus zdiff_def zminus_zadd_distrib [symmetric]) |
|
945 |
done |
|
946 |
||
947 |
lemma zmod_number_of_BIT [simp]: |
|
948 |
"number_of (v BIT b) mod number_of (w BIT False) = |
|
949 |
(if b then |
|
950 |
if (0::int) <= number_of w |
|
951 |
then 2 * (number_of v mod number_of w) + 1 |
|
952 |
else 2 * ((number_of v + (1::int)) mod number_of w) - 1 |
|
953 |
else 2 * (number_of v mod number_of w))" |
|
954 |
apply (simp only: zadd_assoc number_of_BIT) |
|
955 |
apply (simp del: bin_arith_extra_simps bin_rel_simps |
|
13260 | 956 |
add: zmod_zmult_zmult1 pos_zmod_mult_2 not_0_le_lemma neg_zmod_mult_2, simp) |
13183 | 957 |
done |
958 |
||
959 |
||
960 |
||
961 |
(** Quotients of signs **) |
|
962 |
||
963 |
lemma div_neg_pos_less0: "[| a < (0::int); 0 < b |] ==> a div b < 0" |
|
964 |
apply (subgoal_tac "a div b <= -1", force) |
|
965 |
apply (rule order_trans) |
|
966 |
apply (rule_tac a' = "-1" in zdiv_mono1) |
|
967 |
apply (auto simp add: zdiv_minus1) |
|
968 |
done |
|
969 |
||
970 |
lemma div_nonneg_neg_le0: "[| (0::int) <= a; b < 0 |] ==> a div b <= 0" |
|
971 |
by (drule zdiv_mono1_neg, auto) |
|
972 |
||
973 |
lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 <= a div b) = (0 <= a)" |
|
974 |
apply auto |
|
975 |
apply (drule_tac [2] zdiv_mono1) |
|
976 |
apply (auto simp add: linorder_neq_iff) |
|
977 |
apply (simp (no_asm_use) add: linorder_not_less [symmetric]) |
|
978 |
apply (blast intro: div_neg_pos_less0) |
|
979 |
done |
|
980 |
||
981 |
lemma neg_imp_zdiv_nonneg_iff: |
|
982 |
"b < (0::int) ==> (0 <= a div b) = (a <= (0::int))" |
|
983 |
apply (subst zdiv_zminus_zminus [symmetric]) |
|
984 |
apply (subst pos_imp_zdiv_nonneg_iff, auto) |
|
985 |
done |
|
986 |
||
987 |
(*But not (a div b <= 0 iff a<=0); consider a=1, b=2 when a div b = 0.*) |
|
988 |
lemma pos_imp_zdiv_neg_iff: "(0::int) < b ==> (a div b < 0) = (a < 0)" |
|
989 |
by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff) |
|
990 |
||
991 |
(*Again the law fails for <=: consider a = -1, b = -2 when a div b = 0*) |
|
992 |
lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)" |
|
993 |
by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff) |
|
994 |
||
995 |
ML |
|
996 |
{* |
|
997 |
val quorem_def = thm "quorem_def"; |
|
998 |
||
999 |
val unique_quotient = thm "unique_quotient"; |
|
1000 |
val unique_remainder = thm "unique_remainder"; |
|
1001 |
val adjust_eq = thm "adjust_eq"; |
|
1002 |
val posDivAlg_eqn = thm "posDivAlg_eqn"; |
|
1003 |
val posDivAlg_correct = thm "posDivAlg_correct"; |
|
1004 |
val negDivAlg_eqn = thm "negDivAlg_eqn"; |
|
1005 |
val negDivAlg_correct = thm "negDivAlg_correct"; |
|
1006 |
val quorem_0 = thm "quorem_0"; |
|
1007 |
val posDivAlg_0 = thm "posDivAlg_0"; |
|
1008 |
val negDivAlg_minus1 = thm "negDivAlg_minus1"; |
|
1009 |
val negateSnd_eq = thm "negateSnd_eq"; |
|
1010 |
val quorem_neg = thm "quorem_neg"; |
|
1011 |
val divAlg_correct = thm "divAlg_correct"; |
|
1012 |
val DIVISION_BY_ZERO = thm "DIVISION_BY_ZERO"; |
|
1013 |
val zmod_zdiv_equality = thm "zmod_zdiv_equality"; |
|
1014 |
val pos_mod_conj = thm "pos_mod_conj"; |
|
1015 |
val pos_mod_sign = thm "pos_mod_sign"; |
|
1016 |
val neg_mod_conj = thm "neg_mod_conj"; |
|
1017 |
val neg_mod_sign = thm "neg_mod_sign"; |
|
1018 |
val quorem_div_mod = thm "quorem_div_mod"; |
|
1019 |
val quorem_div = thm "quorem_div"; |
|
1020 |
val quorem_mod = thm "quorem_mod"; |
|
1021 |
val div_pos_pos_trivial = thm "div_pos_pos_trivial"; |
|
1022 |
val div_neg_neg_trivial = thm "div_neg_neg_trivial"; |
|
1023 |
val div_pos_neg_trivial = thm "div_pos_neg_trivial"; |
|
1024 |
val mod_pos_pos_trivial = thm "mod_pos_pos_trivial"; |
|
1025 |
val mod_neg_neg_trivial = thm "mod_neg_neg_trivial"; |
|
1026 |
val mod_pos_neg_trivial = thm "mod_pos_neg_trivial"; |
|
1027 |
val zdiv_zminus_zminus = thm "zdiv_zminus_zminus"; |
|
1028 |
val zmod_zminus_zminus = thm "zmod_zminus_zminus"; |
|
1029 |
val zdiv_zminus1_eq_if = thm "zdiv_zminus1_eq_if"; |
|
1030 |
val zmod_zminus1_eq_if = thm "zmod_zminus1_eq_if"; |
|
1031 |
val zdiv_zminus2 = thm "zdiv_zminus2"; |
|
1032 |
val zmod_zminus2 = thm "zmod_zminus2"; |
|
1033 |
val zdiv_zminus2_eq_if = thm "zdiv_zminus2_eq_if"; |
|
1034 |
val zmod_zminus2_eq_if = thm "zmod_zminus2_eq_if"; |
|
1035 |
val self_quotient = thm "self_quotient"; |
|
1036 |
val self_remainder = thm "self_remainder"; |
|
1037 |
val zdiv_self = thm "zdiv_self"; |
|
1038 |
val zmod_self = thm "zmod_self"; |
|
1039 |
val zdiv_zero = thm "zdiv_zero"; |
|
1040 |
val div_eq_minus1 = thm "div_eq_minus1"; |
|
1041 |
val zmod_zero = thm "zmod_zero"; |
|
1042 |
val zdiv_minus1 = thm "zdiv_minus1"; |
|
1043 |
val zmod_minus1 = thm "zmod_minus1"; |
|
1044 |
val div_pos_pos = thm "div_pos_pos"; |
|
1045 |
val mod_pos_pos = thm "mod_pos_pos"; |
|
1046 |
val div_neg_pos = thm "div_neg_pos"; |
|
1047 |
val mod_neg_pos = thm "mod_neg_pos"; |
|
1048 |
val div_pos_neg = thm "div_pos_neg"; |
|
1049 |
val mod_pos_neg = thm "mod_pos_neg"; |
|
1050 |
val div_neg_neg = thm "div_neg_neg"; |
|
1051 |
val mod_neg_neg = thm "mod_neg_neg"; |
|
1052 |
val zmod_1 = thm "zmod_1"; |
|
1053 |
val zdiv_1 = thm "zdiv_1"; |
|
1054 |
val zmod_minus1_right = thm "zmod_minus1_right"; |
|
1055 |
val zdiv_minus1_right = thm "zdiv_minus1_right"; |
|
1056 |
val zdiv_mono1 = thm "zdiv_mono1"; |
|
1057 |
val zdiv_mono1_neg = thm "zdiv_mono1_neg"; |
|
1058 |
val zdiv_mono2 = thm "zdiv_mono2"; |
|
1059 |
val zdiv_mono2_neg = thm "zdiv_mono2_neg"; |
|
1060 |
val zdiv_zmult1_eq = thm "zdiv_zmult1_eq"; |
|
1061 |
val zmod_zmult1_eq = thm "zmod_zmult1_eq"; |
|
1062 |
val zmod_zmult1_eq' = thm "zmod_zmult1_eq'"; |
|
1063 |
val zmod_zmult_distrib = thm "zmod_zmult_distrib"; |
|
1064 |
val zdiv_zmult_self1 = thm "zdiv_zmult_self1"; |
|
1065 |
val zdiv_zmult_self2 = thm "zdiv_zmult_self2"; |
|
1066 |
val zmod_zmult_self1 = thm "zmod_zmult_self1"; |
|
1067 |
val zmod_zmult_self2 = thm "zmod_zmult_self2"; |
|
1068 |
val zmod_eq_0_iff = thm "zmod_eq_0_iff"; |
|
1069 |
val zdiv_zadd1_eq = thm "zdiv_zadd1_eq"; |
|
1070 |
val zmod_zadd1_eq = thm "zmod_zadd1_eq"; |
|
1071 |
val mod_div_trivial = thm "mod_div_trivial"; |
|
1072 |
val mod_mod_trivial = thm "mod_mod_trivial"; |
|
1073 |
val zmod_zadd_left_eq = thm "zmod_zadd_left_eq"; |
|
1074 |
val zmod_zadd_right_eq = thm "zmod_zadd_right_eq"; |
|
1075 |
val zdiv_zadd_self1 = thm "zdiv_zadd_self1"; |
|
1076 |
val zdiv_zadd_self2 = thm "zdiv_zadd_self2"; |
|
1077 |
val zmod_zadd_self1 = thm "zmod_zadd_self1"; |
|
1078 |
val zmod_zadd_self2 = thm "zmod_zadd_self2"; |
|
1079 |
val zdiv_zmult2_eq = thm "zdiv_zmult2_eq"; |
|
1080 |
val zmod_zmult2_eq = thm "zmod_zmult2_eq"; |
|
1081 |
val zdiv_zmult_zmult1 = thm "zdiv_zmult_zmult1"; |
|
1082 |
val zdiv_zmult_zmult2 = thm "zdiv_zmult_zmult2"; |
|
1083 |
val zmod_zmult_zmult1 = thm "zmod_zmult_zmult1"; |
|
1084 |
val zmod_zmult_zmult2 = thm "zmod_zmult_zmult2"; |
|
1085 |
val pos_zdiv_mult_2 = thm "pos_zdiv_mult_2"; |
|
1086 |
val neg_zdiv_mult_2 = thm "neg_zdiv_mult_2"; |
|
1087 |
val zdiv_number_of_BIT = thm "zdiv_number_of_BIT"; |
|
1088 |
val pos_zmod_mult_2 = thm "pos_zmod_mult_2"; |
|
1089 |
val neg_zmod_mult_2 = thm "neg_zmod_mult_2"; |
|
1090 |
val zmod_number_of_BIT = thm "zmod_number_of_BIT"; |
|
1091 |
val div_neg_pos_less0 = thm "div_neg_pos_less0"; |
|
1092 |
val div_nonneg_neg_le0 = thm "div_nonneg_neg_le0"; |
|
1093 |
val pos_imp_zdiv_nonneg_iff = thm "pos_imp_zdiv_nonneg_iff"; |
|
1094 |
val neg_imp_zdiv_nonneg_iff = thm "neg_imp_zdiv_nonneg_iff"; |
|
1095 |
val pos_imp_zdiv_neg_iff = thm "pos_imp_zdiv_neg_iff"; |
|
1096 |
val neg_imp_zdiv_neg_iff = thm "neg_imp_zdiv_neg_iff"; |
|
1097 |
*} |
|
1098 |
||
6917 | 1099 |
end |