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