author | obua |
Mon, 02 Aug 2004 16:06:13 +0200 | |
changeset 15101 | d027515e2aa6 |
parent 15013 | 34264f5e4691 |
child 15131 | c69542757a4d |
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) |
|
14288 | 13 |
in if 0\<le>r-b then (2*q+1, r-b) else (2*q, r) |
13183 | 14 |
end |
15 |
||
16 |
fun negDivAlg (a,b) = |
|
14288 | 17 |
if 0\<le>a+b then (~1,a+b) |
13183 | 18 |
else let val (q,r) = negDivAlg(a, 2*b) |
14288 | 19 |
in if 0\<le>r-b then (2*q+1, r-b) else (2*q, r) |
13183 | 20 |
end; |
21 |
||
22 |
fun negateSnd (q,r:int) = (q,~r); |
|
23 |
||
14288 | 24 |
fun divAlg (a,b) = if 0\<le>a then |
13183 | 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 & |
|
14288 | 43 |
(if 0 < b then 0\<le>r & r<b else b<r & r \<le> 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" |
14288 | 46 |
"adjust b == %(q,r). if 0 \<le> r-b then (2*q + 1, r-b) |
11868
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) = |
14288 | 55 |
(if (a<b | b\<le>0) then (0,a) |
11868
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) = |
|
14288 | 62 |
(if (0\<le>a+b | b\<le>0) then (-1,a+b) |
11868
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 == |
|
14288 | 75 |
%(a,b). if 0\<le>a then |
76 |
if 0\<le>b then posDivAlg (a,b) |
|
11868
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 |
||
14271 | 92 |
subsection{*Uniqueness and Monotonicity of Quotients and Remainders*} |
13183 | 93 |
|
94 |
lemma unique_quotient_lemma: |
|
14288 | 95 |
"[| b*q' + r' \<le> b*q + r; 0 \<le> r'; 0 < b; r < b |] |
96 |
==> q' \<le> (q::int)" |
|
97 |
apply (subgoal_tac "r' + b * (q'-q) \<le> r") |
|
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
98 |
prefer 2 apply (simp add: right_diff_distrib) |
13183 | 99 |
apply (subgoal_tac "0 < b * (1 + q - q') ") |
100 |
apply (erule_tac [2] order_le_less_trans) |
|
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
101 |
prefer 2 apply (simp add: right_diff_distrib right_distrib) |
13183 | 102 |
apply (subgoal_tac "b * q' < b * (1 + q) ") |
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
103 |
prefer 2 apply (simp add: right_diff_distrib right_distrib) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
104 |
apply (simp add: mult_less_cancel_left) |
13183 | 105 |
done |
106 |
||
107 |
lemma unique_quotient_lemma_neg: |
|
14288 | 108 |
"[| b*q' + r' \<le> b*q + r; r \<le> 0; b < 0; b < r' |] |
109 |
==> q \<le> (q'::int)" |
|
13183 | 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 |
||
14271 | 132 |
subsection{*Correctness of posDivAlg, the Algorithm for Non-Negative Dividends*} |
133 |
||
134 |
text{*And positive divisors*} |
|
13183 | 135 |
|
136 |
lemma adjust_eq [simp]: |
|
137 |
"adjust b (q,r) = |
|
138 |
(let diff = r-b in |
|
14288 | 139 |
if 0 \<le> diff then (2*q + 1, diff) |
13183 | 140 |
else (2*q, r))" |
141 |
by (simp add: Let_def adjust_def) |
|
142 |
||
143 |
declare posDivAlg.simps [simp del] |
|
144 |
||
145 |
(**use with a simproc to avoid repeatedly proving the premise*) |
|
146 |
lemma posDivAlg_eqn: |
|
147 |
"0 < b ==> |
|
148 |
posDivAlg (a,b) = (if a<b then (0,a) else adjust b (posDivAlg(a, 2*b)))" |
|
149 |
by (rule posDivAlg.simps [THEN trans], simp) |
|
150 |
||
151 |
(*Correctness of posDivAlg: it computes quotients correctly*) |
|
152 |
lemma posDivAlg_correct [rule_format]: |
|
14288 | 153 |
"0 \<le> a --> 0 < b --> quorem ((a, b), posDivAlg (a, b))" |
13183 | 154 |
apply (induct_tac a b rule: posDivAlg.induct, auto) |
155 |
apply (simp_all add: quorem_def) |
|
156 |
(*base case: a<b*) |
|
157 |
apply (simp add: posDivAlg_eqn) |
|
158 |
(*main argument*) |
|
159 |
apply (subst posDivAlg_eqn, simp_all) |
|
160 |
apply (erule splitE) |
|
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
161 |
apply (auto simp add: right_distrib Let_def) |
13183 | 162 |
done |
163 |
||
164 |
||
14271 | 165 |
subsection{*Correctness of negDivAlg, the Algorithm for Negative Dividends*} |
166 |
||
167 |
text{*And positive divisors*} |
|
13183 | 168 |
|
169 |
declare negDivAlg.simps [simp del] |
|
170 |
||
171 |
(**use with a simproc to avoid repeatedly proving the premise*) |
|
172 |
lemma negDivAlg_eqn: |
|
173 |
"0 < b ==> |
|
174 |
negDivAlg (a,b) = |
|
14288 | 175 |
(if 0\<le>a+b then (-1,a+b) else adjust b (negDivAlg(a, 2*b)))" |
13183 | 176 |
by (rule negDivAlg.simps [THEN trans], simp) |
177 |
||
178 |
(*Correctness of negDivAlg: it computes quotients correctly |
|
179 |
It doesn't work if a=0 because the 0/b equals 0, not -1*) |
|
180 |
lemma negDivAlg_correct [rule_format]: |
|
181 |
"a < 0 --> 0 < b --> quorem ((a, b), negDivAlg (a, b))" |
|
182 |
apply (induct_tac a b rule: negDivAlg.induct, auto) |
|
183 |
apply (simp_all add: quorem_def) |
|
14288 | 184 |
(*base case: 0\<le>a+b*) |
13183 | 185 |
apply (simp add: negDivAlg_eqn) |
186 |
(*main argument*) |
|
187 |
apply (subst negDivAlg_eqn, assumption) |
|
188 |
apply (erule splitE) |
|
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
189 |
apply (auto simp add: right_distrib Let_def) |
13183 | 190 |
done |
191 |
||
192 |
||
14271 | 193 |
subsection{*Existence Shown by Proving the Division Algorithm to be Correct*} |
13183 | 194 |
|
195 |
(*the case a=0*) |
|
196 |
lemma quorem_0: "b ~= 0 ==> quorem ((0,b), (0,0))" |
|
197 |
by (auto simp add: quorem_def linorder_neq_iff) |
|
198 |
||
199 |
lemma posDivAlg_0 [simp]: "posDivAlg (0, b) = (0, 0)" |
|
200 |
by (subst posDivAlg.simps, auto) |
|
201 |
||
202 |
lemma negDivAlg_minus1 [simp]: "negDivAlg (-1, b) = (-1, b - 1)" |
|
203 |
by (subst negDivAlg.simps, auto) |
|
204 |
||
205 |
lemma negateSnd_eq [simp]: "negateSnd(q,r) = (q,-r)" |
|
206 |
by (unfold negateSnd_def, auto) |
|
207 |
||
208 |
lemma quorem_neg: "quorem ((-a,-b), qr) ==> quorem ((a,b), negateSnd qr)" |
|
209 |
by (auto simp add: split_ifs quorem_def) |
|
210 |
||
211 |
lemma divAlg_correct: "b ~= 0 ==> quorem ((a,b), divAlg(a,b))" |
|
212 |
by (force simp add: linorder_neq_iff quorem_0 divAlg_def quorem_neg |
|
213 |
posDivAlg_correct negDivAlg_correct) |
|
214 |
||
215 |
(** Arbitrary definitions for division by zero. Useful to simplify |
|
216 |
certain equations **) |
|
217 |
||
14271 | 218 |
lemma DIVISION_BY_ZERO [simp]: "a div (0::int) = 0 & a mod (0::int) = a" |
219 |
by (simp add: div_def mod_def divAlg_def posDivAlg.simps) |
|
13183 | 220 |
|
221 |
(** Basic laws about division and remainder **) |
|
222 |
||
223 |
lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)" |
|
15013 | 224 |
apply (case_tac "b = 0", simp) |
13183 | 225 |
apply (cut_tac a = a and b = b in divAlg_correct) |
226 |
apply (auto simp add: quorem_def div_def mod_def) |
|
227 |
done |
|
228 |
||
13517 | 229 |
lemma zdiv_zmod_equality: "(b * (a div b) + (a mod b)) + k = (a::int)+k" |
230 |
by(simp add: zmod_zdiv_equality[symmetric]) |
|
231 |
||
232 |
lemma zdiv_zmod_equality2: "((a div b) * b + (a mod b)) + k = (a::int)+k" |
|
233 |
by(simp add: zmult_commute zmod_zdiv_equality[symmetric]) |
|
234 |
||
235 |
use "IntDiv_setup.ML" |
|
236 |
||
14288 | 237 |
lemma pos_mod_conj : "(0::int) < b ==> 0 \<le> a mod b & a mod b < b" |
13183 | 238 |
apply (cut_tac a = a and b = b in divAlg_correct) |
239 |
apply (auto simp add: quorem_def mod_def) |
|
240 |
done |
|
241 |
||
13788 | 242 |
lemmas pos_mod_sign[simp] = pos_mod_conj [THEN conjunct1, standard] |
243 |
and pos_mod_bound[simp] = pos_mod_conj [THEN conjunct2, standard] |
|
13183 | 244 |
|
14288 | 245 |
lemma neg_mod_conj : "b < (0::int) ==> a mod b \<le> 0 & b < a mod b" |
13183 | 246 |
apply (cut_tac a = a and b = b in divAlg_correct) |
247 |
apply (auto simp add: quorem_def div_def mod_def) |
|
248 |
done |
|
249 |
||
13788 | 250 |
lemmas neg_mod_sign[simp] = neg_mod_conj [THEN conjunct1, standard] |
251 |
and neg_mod_bound[simp] = neg_mod_conj [THEN conjunct2, standard] |
|
13183 | 252 |
|
253 |
||
13260 | 254 |
|
13183 | 255 |
(** proving general properties of div and mod **) |
256 |
||
257 |
lemma quorem_div_mod: "b ~= 0 ==> quorem ((a, b), (a div b, a mod b))" |
|
258 |
apply (cut_tac a = a and b = b in zmod_zdiv_equality) |
|
13788 | 259 |
apply (force simp add: quorem_def linorder_neq_iff) |
13183 | 260 |
done |
261 |
||
262 |
lemma quorem_div: "[| quorem((a,b),(q,r)); b ~= 0 |] ==> a div b = q" |
|
263 |
by (simp add: quorem_div_mod [THEN unique_quotient]) |
|
264 |
||
265 |
lemma quorem_mod: "[| quorem((a,b),(q,r)); b ~= 0 |] ==> a mod b = r" |
|
266 |
by (simp add: quorem_div_mod [THEN unique_remainder]) |
|
267 |
||
14288 | 268 |
lemma div_pos_pos_trivial: "[| (0::int) \<le> a; a < b |] ==> a div b = 0" |
13183 | 269 |
apply (rule quorem_div) |
270 |
apply (auto simp add: quorem_def) |
|
271 |
done |
|
272 |
||
14288 | 273 |
lemma div_neg_neg_trivial: "[| a \<le> (0::int); b < a |] ==> a div b = 0" |
13183 | 274 |
apply (rule quorem_div) |
275 |
apply (auto simp add: quorem_def) |
|
276 |
done |
|
277 |
||
14288 | 278 |
lemma div_pos_neg_trivial: "[| (0::int) < a; a+b \<le> 0 |] ==> a div b = -1" |
13183 | 279 |
apply (rule quorem_div) |
280 |
apply (auto simp add: quorem_def) |
|
281 |
done |
|
282 |
||
283 |
(*There is no div_neg_pos_trivial because 0 div b = 0 would supersede it*) |
|
284 |
||
14288 | 285 |
lemma mod_pos_pos_trivial: "[| (0::int) \<le> a; a < b |] ==> a mod b = a" |
13183 | 286 |
apply (rule_tac q = 0 in quorem_mod) |
287 |
apply (auto simp add: quorem_def) |
|
288 |
done |
|
289 |
||
14288 | 290 |
lemma mod_neg_neg_trivial: "[| a \<le> (0::int); b < a |] ==> a mod b = a" |
13183 | 291 |
apply (rule_tac q = 0 in quorem_mod) |
292 |
apply (auto simp add: quorem_def) |
|
293 |
done |
|
294 |
||
14288 | 295 |
lemma mod_pos_neg_trivial: "[| (0::int) < a; a+b \<le> 0 |] ==> a mod b = a+b" |
13183 | 296 |
apply (rule_tac q = "-1" in quorem_mod) |
297 |
apply (auto simp add: quorem_def) |
|
298 |
done |
|
299 |
||
300 |
(*There is no mod_neg_pos_trivial...*) |
|
301 |
||
302 |
||
303 |
(*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*) |
|
304 |
lemma zdiv_zminus_zminus [simp]: "(-a) div (-b) = a div (b::int)" |
|
15013 | 305 |
apply (case_tac "b = 0", simp) |
13183 | 306 |
apply (simp add: quorem_div_mod [THEN quorem_neg, simplified, |
307 |
THEN quorem_div, THEN sym]) |
|
308 |
||
309 |
done |
|
310 |
||
311 |
(*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*) |
|
312 |
lemma zmod_zminus_zminus [simp]: "(-a) mod (-b) = - (a mod (b::int))" |
|
15013 | 313 |
apply (case_tac "b = 0", simp) |
13183 | 314 |
apply (subst quorem_div_mod [THEN quorem_neg, simplified, THEN quorem_mod], |
315 |
auto) |
|
316 |
done |
|
317 |
||
14271 | 318 |
subsection{*div, mod and unary minus*} |
13183 | 319 |
|
320 |
lemma zminus1_lemma: |
|
321 |
"quorem((a,b),(q,r)) |
|
322 |
==> quorem ((-a,b), (if r=0 then -q else -q - 1), |
|
323 |
(if r=0 then 0 else b-r))" |
|
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
324 |
by (force simp add: split_ifs quorem_def linorder_neq_iff right_diff_distrib) |
13183 | 325 |
|
326 |
||
327 |
lemma zdiv_zminus1_eq_if: |
|
328 |
"b ~= (0::int) |
|
329 |
==> (-a) div b = |
|
330 |
(if a mod b = 0 then - (a div b) else - (a div b) - 1)" |
|
331 |
by (blast intro: quorem_div_mod [THEN zminus1_lemma, THEN quorem_div]) |
|
332 |
||
333 |
lemma zmod_zminus1_eq_if: |
|
334 |
"(-a::int) mod b = (if a mod b = 0 then 0 else b - (a mod b))" |
|
15013 | 335 |
apply (case_tac "b = 0", simp) |
13183 | 336 |
apply (blast intro: quorem_div_mod [THEN zminus1_lemma, THEN quorem_mod]) |
337 |
done |
|
338 |
||
339 |
lemma zdiv_zminus2: "a div (-b) = (-a::int) div b" |
|
340 |
by (cut_tac a = "-a" in zdiv_zminus_zminus, auto) |
|
341 |
||
342 |
lemma zmod_zminus2: "a mod (-b) = - ((-a::int) mod b)" |
|
343 |
by (cut_tac a = "-a" and b = b in zmod_zminus_zminus, auto) |
|
344 |
||
345 |
lemma zdiv_zminus2_eq_if: |
|
346 |
"b ~= (0::int) |
|
347 |
==> a div (-b) = |
|
348 |
(if a mod b = 0 then - (a div b) else - (a div b) - 1)" |
|
349 |
by (simp add: zdiv_zminus1_eq_if zdiv_zminus2) |
|
350 |
||
351 |
lemma zmod_zminus2_eq_if: |
|
352 |
"a mod (-b::int) = (if a mod b = 0 then 0 else (a mod b) - b)" |
|
353 |
by (simp add: zmod_zminus1_eq_if zmod_zminus2) |
|
354 |
||
355 |
||
14271 | 356 |
subsection{*Division of a Number by Itself*} |
13183 | 357 |
|
14288 | 358 |
lemma self_quotient_aux1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 \<le> q" |
13183 | 359 |
apply (subgoal_tac "0 < a*q") |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
360 |
apply (simp add: zero_less_mult_iff, arith) |
13183 | 361 |
done |
362 |
||
14288 | 363 |
lemma self_quotient_aux2: "[| (0::int) < a; a = r + a*q; 0 \<le> r |] ==> q \<le> 1" |
364 |
apply (subgoal_tac "0 \<le> a* (1-q) ") |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
365 |
apply (simp add: zero_le_mult_iff) |
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
366 |
apply (simp add: right_diff_distrib) |
13183 | 367 |
done |
368 |
||
369 |
lemma self_quotient: "[| quorem((a,a),(q,r)); a ~= (0::int) |] ==> q = 1" |
|
370 |
apply (simp add: split_ifs quorem_def linorder_neq_iff) |
|
13601 | 371 |
apply (rule order_antisym, safe, simp_all (no_asm_use)) |
13524 | 372 |
apply (rule_tac [3] a = "-a" and r = "-r" in self_quotient_aux1) |
373 |
apply (rule_tac a = "-a" and r = "-r" in self_quotient_aux2) |
|
13601 | 374 |
apply (force intro: self_quotient_aux1 self_quotient_aux2 simp only: zadd_commute zmult_zminus)+ |
13183 | 375 |
done |
376 |
||
377 |
lemma self_remainder: "[| quorem((a,a),(q,r)); a ~= (0::int) |] ==> r = 0" |
|
378 |
apply (frule self_quotient, assumption) |
|
379 |
apply (simp add: quorem_def) |
|
380 |
done |
|
381 |
||
382 |
lemma zdiv_self [simp]: "a ~= 0 ==> a div a = (1::int)" |
|
383 |
by (simp add: quorem_div_mod [THEN self_quotient]) |
|
384 |
||
385 |
(*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *) |
|
386 |
lemma zmod_self [simp]: "a mod a = (0::int)" |
|
15013 | 387 |
apply (case_tac "a = 0", simp) |
13183 | 388 |
apply (simp add: quorem_div_mod [THEN self_remainder]) |
389 |
done |
|
390 |
||
391 |
||
14271 | 392 |
subsection{*Computation of Division and Remainder*} |
13183 | 393 |
|
394 |
lemma zdiv_zero [simp]: "(0::int) div b = 0" |
|
395 |
by (simp add: div_def divAlg_def) |
|
396 |
||
397 |
lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1" |
|
398 |
by (simp add: div_def divAlg_def) |
|
399 |
||
400 |
lemma zmod_zero [simp]: "(0::int) mod b = 0" |
|
401 |
by (simp add: mod_def divAlg_def) |
|
402 |
||
403 |
lemma zdiv_minus1: "(0::int) < b ==> -1 div b = -1" |
|
404 |
by (simp add: div_def divAlg_def) |
|
405 |
||
406 |
lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1" |
|
407 |
by (simp add: mod_def divAlg_def) |
|
408 |
||
409 |
(** a positive, b positive **) |
|
410 |
||
14288 | 411 |
lemma div_pos_pos: "[| 0 < a; 0 \<le> b |] ==> a div b = fst (posDivAlg(a,b))" |
13183 | 412 |
by (simp add: div_def divAlg_def) |
413 |
||
14288 | 414 |
lemma mod_pos_pos: "[| 0 < a; 0 \<le> b |] ==> a mod b = snd (posDivAlg(a,b))" |
13183 | 415 |
by (simp add: mod_def divAlg_def) |
416 |
||
417 |
(** a negative, b positive **) |
|
418 |
||
419 |
lemma div_neg_pos: "[| a < 0; 0 < b |] ==> a div b = fst (negDivAlg(a,b))" |
|
420 |
by (simp add: div_def divAlg_def) |
|
421 |
||
422 |
lemma mod_neg_pos: "[| a < 0; 0 < b |] ==> a mod b = snd (negDivAlg(a,b))" |
|
423 |
by (simp add: mod_def divAlg_def) |
|
424 |
||
425 |
(** a positive, b negative **) |
|
426 |
||
427 |
lemma div_pos_neg: |
|
428 |
"[| 0 < a; b < 0 |] ==> a div b = fst (negateSnd(negDivAlg(-a,-b)))" |
|
429 |
by (simp add: div_def divAlg_def) |
|
430 |
||
431 |
lemma mod_pos_neg: |
|
432 |
"[| 0 < a; b < 0 |] ==> a mod b = snd (negateSnd(negDivAlg(-a,-b)))" |
|
433 |
by (simp add: mod_def divAlg_def) |
|
434 |
||
435 |
(** a negative, b negative **) |
|
436 |
||
437 |
lemma div_neg_neg: |
|
14288 | 438 |
"[| a < 0; b \<le> 0 |] ==> a div b = fst (negateSnd(posDivAlg(-a,-b)))" |
13183 | 439 |
by (simp add: div_def divAlg_def) |
440 |
||
441 |
lemma mod_neg_neg: |
|
14288 | 442 |
"[| a < 0; b \<le> 0 |] ==> a mod b = snd (negateSnd(posDivAlg(-a,-b)))" |
13183 | 443 |
by (simp add: mod_def divAlg_def) |
444 |
||
445 |
text {*Simplify expresions in which div and mod combine numerical constants*} |
|
446 |
||
447 |
declare div_pos_pos [of "number_of v" "number_of w", standard, simp] |
|
448 |
declare div_neg_pos [of "number_of v" "number_of w", standard, simp] |
|
449 |
declare div_pos_neg [of "number_of v" "number_of w", standard, simp] |
|
450 |
declare div_neg_neg [of "number_of v" "number_of w", standard, simp] |
|
451 |
||
452 |
declare mod_pos_pos [of "number_of v" "number_of w", standard, simp] |
|
453 |
declare mod_neg_pos [of "number_of v" "number_of w", standard, simp] |
|
454 |
declare mod_pos_neg [of "number_of v" "number_of w", standard, simp] |
|
455 |
declare mod_neg_neg [of "number_of v" "number_of w", standard, simp] |
|
456 |
||
457 |
declare posDivAlg_eqn [of "number_of v" "number_of w", standard, simp] |
|
458 |
declare negDivAlg_eqn [of "number_of v" "number_of w", standard, simp] |
|
459 |
||
460 |
||
461 |
(** Special-case simplification **) |
|
462 |
||
463 |
lemma zmod_1 [simp]: "a mod (1::int) = 0" |
|
464 |
apply (cut_tac a = a and b = 1 in pos_mod_sign) |
|
13788 | 465 |
apply (cut_tac [2] a = a and b = 1 in pos_mod_bound) |
466 |
apply (auto simp del:pos_mod_bound pos_mod_sign) |
|
467 |
done |
|
13183 | 468 |
|
469 |
lemma zdiv_1 [simp]: "a div (1::int) = a" |
|
470 |
by (cut_tac a = a and b = 1 in zmod_zdiv_equality, auto) |
|
471 |
||
472 |
lemma zmod_minus1_right [simp]: "a mod (-1::int) = 0" |
|
473 |
apply (cut_tac a = a and b = "-1" in neg_mod_sign) |
|
13788 | 474 |
apply (cut_tac [2] a = a and b = "-1" in neg_mod_bound) |
475 |
apply (auto simp del: neg_mod_sign neg_mod_bound) |
|
13183 | 476 |
done |
477 |
||
478 |
lemma zdiv_minus1_right [simp]: "a div (-1::int) = -a" |
|
479 |
by (cut_tac a = a and b = "-1" in zmod_zdiv_equality, auto) |
|
480 |
||
481 |
(** The last remaining special cases for constant arithmetic: |
|
482 |
1 div z and 1 mod z **) |
|
483 |
||
484 |
declare div_pos_pos [OF int_0_less_1, of "number_of w", standard, simp] |
|
485 |
declare div_pos_neg [OF int_0_less_1, of "number_of w", standard, simp] |
|
486 |
declare mod_pos_pos [OF int_0_less_1, of "number_of w", standard, simp] |
|
487 |
declare mod_pos_neg [OF int_0_less_1, of "number_of w", standard, simp] |
|
488 |
||
489 |
declare posDivAlg_eqn [of concl: 1 "number_of w", standard, simp] |
|
490 |
declare negDivAlg_eqn [of concl: 1 "number_of w", standard, simp] |
|
491 |
||
492 |
||
14271 | 493 |
subsection{*Monotonicity in the First Argument (Dividend)*} |
13183 | 494 |
|
14288 | 495 |
lemma zdiv_mono1: "[| a \<le> a'; 0 < (b::int) |] ==> a div b \<le> a' div b" |
13183 | 496 |
apply (cut_tac a = a and b = b in zmod_zdiv_equality) |
497 |
apply (cut_tac a = a' and b = b in zmod_zdiv_equality) |
|
498 |
apply (rule unique_quotient_lemma) |
|
499 |
apply (erule subst) |
|
500 |
apply (erule subst) |
|
13788 | 501 |
apply (simp_all) |
13183 | 502 |
done |
503 |
||
14288 | 504 |
lemma zdiv_mono1_neg: "[| a \<le> a'; (b::int) < 0 |] ==> a' div b \<le> a div b" |
13183 | 505 |
apply (cut_tac a = a and b = b in zmod_zdiv_equality) |
506 |
apply (cut_tac a = a' and b = b in zmod_zdiv_equality) |
|
507 |
apply (rule unique_quotient_lemma_neg) |
|
508 |
apply (erule subst) |
|
509 |
apply (erule subst) |
|
13788 | 510 |
apply (simp_all) |
13183 | 511 |
done |
6917 | 512 |
|
513 |
||
14271 | 514 |
subsection{*Monotonicity in the Second Argument (Divisor)*} |
13183 | 515 |
|
516 |
lemma q_pos_lemma: |
|
14288 | 517 |
"[| 0 \<le> b'*q' + r'; r' < b'; 0 < b' |] ==> 0 \<le> (q'::int)" |
13183 | 518 |
apply (subgoal_tac "0 < b'* (q' + 1) ") |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
519 |
apply (simp add: zero_less_mult_iff) |
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
520 |
apply (simp add: right_distrib) |
13183 | 521 |
done |
522 |
||
523 |
lemma zdiv_mono2_lemma: |
|
14288 | 524 |
"[| b*q + r = b'*q' + r'; 0 \<le> b'*q' + r'; |
525 |
r' < b'; 0 \<le> r; 0 < b'; b' \<le> b |] |
|
526 |
==> q \<le> (q'::int)" |
|
13183 | 527 |
apply (frule q_pos_lemma, assumption+) |
528 |
apply (subgoal_tac "b*q < b* (q' + 1) ") |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
529 |
apply (simp add: mult_less_cancel_left) |
13183 | 530 |
apply (subgoal_tac "b*q = r' - r + b'*q'") |
531 |
prefer 2 apply simp |
|
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
532 |
apply (simp (no_asm_simp) add: right_distrib) |
13183 | 533 |
apply (subst zadd_commute, rule zadd_zless_mono, arith) |
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14353
diff
changeset
|
534 |
apply (rule mult_right_mono, auto) |
13183 | 535 |
done |
536 |
||
537 |
lemma zdiv_mono2: |
|
14288 | 538 |
"[| (0::int) \<le> a; 0 < b'; b' \<le> b |] ==> a div b \<le> a div b'" |
13183 | 539 |
apply (subgoal_tac "b ~= 0") |
540 |
prefer 2 apply arith |
|
541 |
apply (cut_tac a = a and b = b in zmod_zdiv_equality) |
|
542 |
apply (cut_tac a = a and b = b' in zmod_zdiv_equality) |
|
543 |
apply (rule zdiv_mono2_lemma) |
|
544 |
apply (erule subst) |
|
545 |
apply (erule subst) |
|
13788 | 546 |
apply (simp_all) |
13183 | 547 |
done |
548 |
||
549 |
lemma q_neg_lemma: |
|
14288 | 550 |
"[| b'*q' + r' < 0; 0 \<le> r'; 0 < b' |] ==> q' \<le> (0::int)" |
13183 | 551 |
apply (subgoal_tac "b'*q' < 0") |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
552 |
apply (simp add: mult_less_0_iff, arith) |
13183 | 553 |
done |
554 |
||
555 |
lemma zdiv_mono2_neg_lemma: |
|
556 |
"[| b*q + r = b'*q' + r'; b'*q' + r' < 0; |
|
14288 | 557 |
r < b; 0 \<le> r'; 0 < b'; b' \<le> b |] |
558 |
==> q' \<le> (q::int)" |
|
13183 | 559 |
apply (frule q_neg_lemma, assumption+) |
560 |
apply (subgoal_tac "b*q' < b* (q + 1) ") |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
561 |
apply (simp add: mult_less_cancel_left) |
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
562 |
apply (simp add: right_distrib) |
14288 | 563 |
apply (subgoal_tac "b*q' \<le> b'*q'") |
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14353
diff
changeset
|
564 |
prefer 2 apply (simp add: mult_right_mono_neg) |
13183 | 565 |
apply (subgoal_tac "b'*q' < b + b*q") |
566 |
apply arith |
|
567 |
apply simp |
|
568 |
done |
|
569 |
||
570 |
lemma zdiv_mono2_neg: |
|
14288 | 571 |
"[| a < (0::int); 0 < b'; b' \<le> b |] ==> a div b' \<le> a div b" |
13183 | 572 |
apply (cut_tac a = a and b = b in zmod_zdiv_equality) |
573 |
apply (cut_tac a = a and b = b' in zmod_zdiv_equality) |
|
574 |
apply (rule zdiv_mono2_neg_lemma) |
|
575 |
apply (erule subst) |
|
576 |
apply (erule subst) |
|
13788 | 577 |
apply (simp_all) |
13183 | 578 |
done |
579 |
||
580 |
||
14271 | 581 |
subsection{*More Algebraic Laws for div and mod*} |
13183 | 582 |
|
583 |
(** proving (a*b) div c = a * (b div c) + a * (b mod c) **) |
|
584 |
||
585 |
lemma zmult1_lemma: |
|
586 |
"[| quorem((b,c),(q,r)); c ~= 0 |] |
|
587 |
==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))" |
|
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
588 |
by (force simp add: split_ifs quorem_def linorder_neq_iff right_distrib) |
13183 | 589 |
|
590 |
lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)" |
|
15013 | 591 |
apply (case_tac "c = 0", simp) |
13183 | 592 |
apply (blast intro: quorem_div_mod [THEN zmult1_lemma, THEN quorem_div]) |
593 |
done |
|
594 |
||
595 |
lemma zmod_zmult1_eq: "(a*b) mod c = a*(b mod c) mod (c::int)" |
|
15013 | 596 |
apply (case_tac "c = 0", simp) |
13183 | 597 |
apply (blast intro: quorem_div_mod [THEN zmult1_lemma, THEN quorem_mod]) |
598 |
done |
|
599 |
||
600 |
lemma zmod_zmult1_eq': "(a*b) mod (c::int) = ((a mod c) * b) mod c" |
|
601 |
apply (rule trans) |
|
602 |
apply (rule_tac s = "b*a mod c" in trans) |
|
603 |
apply (rule_tac [2] zmod_zmult1_eq) |
|
604 |
apply (simp_all add: zmult_commute) |
|
605 |
done |
|
606 |
||
607 |
lemma zmod_zmult_distrib: "(a*b) mod (c::int) = ((a mod c) * (b mod c)) mod c" |
|
608 |
apply (rule zmod_zmult1_eq' [THEN trans]) |
|
609 |
apply (rule zmod_zmult1_eq) |
|
610 |
done |
|
611 |
||
612 |
lemma zdiv_zmult_self1 [simp]: "b ~= (0::int) ==> (a*b) div b = a" |
|
613 |
by (simp add: zdiv_zmult1_eq) |
|
614 |
||
615 |
lemma zdiv_zmult_self2 [simp]: "b ~= (0::int) ==> (b*a) div b = a" |
|
616 |
by (subst zmult_commute, erule zdiv_zmult_self1) |
|
617 |
||
618 |
lemma zmod_zmult_self1 [simp]: "(a*b) mod b = (0::int)" |
|
619 |
by (simp add: zmod_zmult1_eq) |
|
620 |
||
621 |
lemma zmod_zmult_self2 [simp]: "(b*a) mod b = (0::int)" |
|
622 |
by (simp add: zmult_commute zmod_zmult1_eq) |
|
623 |
||
624 |
lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)" |
|
13517 | 625 |
proof |
626 |
assume "m mod d = 0" |
|
14473 | 627 |
with zmod_zdiv_equality[of m d] show "EX q::int. m = d*q" by auto |
13517 | 628 |
next |
629 |
assume "EX q::int. m = d*q" |
|
630 |
thus "m mod d = 0" by auto |
|
631 |
qed |
|
13183 | 632 |
|
633 |
declare zmod_eq_0_iff [THEN iffD1, dest!] |
|
634 |
||
635 |
(** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **) |
|
636 |
||
637 |
lemma zadd1_lemma: |
|
638 |
"[| quorem((a,c),(aq,ar)); quorem((b,c),(bq,br)); c ~= 0 |] |
|
639 |
==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))" |
|
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
640 |
by (force simp add: split_ifs quorem_def linorder_neq_iff right_distrib) |
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)" |
|
15013 | 645 |
apply (case_tac "c = 0", simp) |
13183 | 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" |
|
15013 | 650 |
apply (case_tac "c = 0", simp) |
13183 | 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)" |
|
15013 | 655 |
apply (case_tac "b = 0", simp) |
13788 | 656 |
apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial) |
13183 | 657 |
done |
658 |
||
659 |
lemma mod_mod_trivial [simp]: "(a mod b) mod b = a mod (b::int)" |
|
15013 | 660 |
apply (case_tac "b = 0", simp) |
13788 | 661 |
apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial) |
13183 | 662 |
done |
663 |
||
664 |
lemma zmod_zadd_left_eq: "(a+b) mod (c::int) = ((a mod c) + b) mod c" |
|
665 |
apply (rule trans [symmetric]) |
|
666 |
apply (rule zmod_zadd1_eq, simp) |
|
667 |
apply (rule zmod_zadd1_eq [symmetric]) |
|
668 |
done |
|
669 |
||
670 |
lemma zmod_zadd_right_eq: "(a+b) mod (c::int) = (a + (b mod c)) mod c" |
|
671 |
apply (rule trans [symmetric]) |
|
672 |
apply (rule zmod_zadd1_eq, simp) |
|
673 |
apply (rule zmod_zadd1_eq [symmetric]) |
|
674 |
done |
|
675 |
||
676 |
lemma zdiv_zadd_self1[simp]: "a ~= (0::int) ==> (a+b) div a = b div a + 1" |
|
677 |
by (simp add: zdiv_zadd1_eq) |
|
678 |
||
679 |
lemma zdiv_zadd_self2[simp]: "a ~= (0::int) ==> (b+a) div a = b div a + 1" |
|
680 |
by (simp add: zdiv_zadd1_eq) |
|
681 |
||
682 |
lemma zmod_zadd_self1[simp]: "(a+b) mod a = b mod (a::int)" |
|
15013 | 683 |
apply (case_tac "a = 0", simp) |
13183 | 684 |
apply (simp add: zmod_zadd1_eq) |
685 |
done |
|
686 |
||
687 |
lemma zmod_zadd_self2[simp]: "(b+a) mod a = b mod (a::int)" |
|
15013 | 688 |
apply (case_tac "a = 0", simp) |
13183 | 689 |
apply (simp add: zmod_zadd1_eq) |
690 |
done |
|
691 |
||
692 |
||
14271 | 693 |
subsection{*Proving @{term "a div (b*c) = (a div b) div c"} *} |
13183 | 694 |
|
695 |
(*The condition c>0 seems necessary. Consider that 7 div ~6 = ~2 but |
|
696 |
7 div 2 div ~3 = 3 div ~3 = ~1. The subcase (a div b) mod c = 0 seems |
|
697 |
to cause particular problems.*) |
|
698 |
||
699 |
(** first, four lemmas to bound the remainder for the cases b<0 and b>0 **) |
|
700 |
||
14288 | 701 |
lemma zmult2_lemma_aux1: "[| (0::int) < c; b < r; r \<le> 0 |] ==> b*c < b*(q mod c) + r" |
13183 | 702 |
apply (subgoal_tac "b * (c - q mod c) < r * 1") |
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
703 |
apply (simp add: right_diff_distrib) |
13183 | 704 |
apply (rule order_le_less_trans) |
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14353
diff
changeset
|
705 |
apply (erule_tac [2] mult_strict_right_mono) |
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14353
diff
changeset
|
706 |
apply (rule mult_left_mono_neg) |
14271 | 707 |
apply (auto simp add: compare_rls zadd_commute [of 1] |
13183 | 708 |
add1_zle_eq pos_mod_bound) |
709 |
done |
|
710 |
||
14288 | 711 |
lemma zmult2_lemma_aux2: "[| (0::int) < c; b < r; r \<le> 0 |] ==> b * (q mod c) + r \<le> 0" |
712 |
apply (subgoal_tac "b * (q mod c) \<le> 0") |
|
13183 | 713 |
apply arith |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
714 |
apply (simp add: mult_le_0_iff) |
13183 | 715 |
done |
716 |
||
14288 | 717 |
lemma zmult2_lemma_aux3: "[| (0::int) < c; 0 \<le> r; r < b |] ==> 0 \<le> b * (q mod c) + r" |
718 |
apply (subgoal_tac "0 \<le> b * (q mod c) ") |
|
13183 | 719 |
apply arith |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
720 |
apply (simp add: zero_le_mult_iff) |
13183 | 721 |
done |
722 |
||
14288 | 723 |
lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 \<le> r; r < b |] ==> b * (q mod c) + r < b * c" |
13183 | 724 |
apply (subgoal_tac "r * 1 < b * (c - q mod c) ") |
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
725 |
apply (simp add: right_diff_distrib) |
13183 | 726 |
apply (rule order_less_le_trans) |
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14353
diff
changeset
|
727 |
apply (erule mult_strict_right_mono) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
728 |
apply (rule_tac [2] mult_left_mono) |
14271 | 729 |
apply (auto simp add: compare_rls zadd_commute [of 1] |
13183 | 730 |
add1_zle_eq pos_mod_bound) |
731 |
done |
|
732 |
||
733 |
lemma zmult2_lemma: "[| quorem ((a,b), (q,r)); b ~= 0; 0 < c |] |
|
734 |
==> quorem ((a, b*c), (q div c, b*(q mod c) + r))" |
|
14271 | 735 |
by (auto simp add: mult_ac quorem_def linorder_neq_iff |
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
736 |
zero_less_mult_iff right_distrib [symmetric] |
13524 | 737 |
zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4) |
13183 | 738 |
|
739 |
lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c" |
|
15013 | 740 |
apply (case_tac "b = 0", simp) |
13183 | 741 |
apply (force simp add: quorem_div_mod [THEN zmult2_lemma, THEN quorem_div]) |
742 |
done |
|
743 |
||
744 |
lemma zmod_zmult2_eq: |
|
745 |
"(0::int) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b" |
|
15013 | 746 |
apply (case_tac "b = 0", simp) |
13183 | 747 |
apply (force simp add: quorem_div_mod [THEN zmult2_lemma, THEN quorem_mod]) |
748 |
done |
|
749 |
||
750 |
||
14271 | 751 |
subsection{*Cancellation of Common Factors in div*} |
13183 | 752 |
|
13524 | 753 |
lemma zdiv_zmult_zmult1_aux1: "[| (0::int) < b; c ~= 0 |] ==> (c*a) div (c*b) = a div b" |
13183 | 754 |
by (subst zdiv_zmult2_eq, auto) |
755 |
||
13524 | 756 |
lemma zdiv_zmult_zmult1_aux2: "[| b < (0::int); c ~= 0 |] ==> (c*a) div (c*b) = a div b" |
13183 | 757 |
apply (subgoal_tac " (c * (-a)) div (c * (-b)) = (-a) div (-b) ") |
13524 | 758 |
apply (rule_tac [2] zdiv_zmult_zmult1_aux1, auto) |
13183 | 759 |
done |
760 |
||
761 |
lemma zdiv_zmult_zmult1: "c ~= (0::int) ==> (c*a) div (c*b) = a div b" |
|
15013 | 762 |
apply (case_tac "b = 0", simp) |
13524 | 763 |
apply (auto simp add: linorder_neq_iff zdiv_zmult_zmult1_aux1 zdiv_zmult_zmult1_aux2) |
13183 | 764 |
done |
765 |
||
766 |
lemma zdiv_zmult_zmult2: "c ~= (0::int) ==> (a*c) div (b*c) = a div b" |
|
767 |
apply (drule zdiv_zmult_zmult1) |
|
768 |
apply (auto simp add: zmult_commute) |
|
769 |
done |
|
770 |
||
771 |
||
772 |
||
14271 | 773 |
subsection{*Distribution of Factors over mod*} |
13183 | 774 |
|
13524 | 775 |
lemma zmod_zmult_zmult1_aux1: "[| (0::int) < b; c ~= 0 |] ==> (c*a) mod (c*b) = c * (a mod b)" |
13183 | 776 |
by (subst zmod_zmult2_eq, auto) |
777 |
||
13524 | 778 |
lemma zmod_zmult_zmult1_aux2: "[| b < (0::int); c ~= 0 |] ==> (c*a) mod (c*b) = c * (a mod b)" |
13183 | 779 |
apply (subgoal_tac " (c * (-a)) mod (c * (-b)) = c * ((-a) mod (-b))") |
13524 | 780 |
apply (rule_tac [2] zmod_zmult_zmult1_aux1, auto) |
13183 | 781 |
done |
782 |
||
783 |
lemma zmod_zmult_zmult1: "(c*a) mod (c*b) = (c::int) * (a mod b)" |
|
15013 | 784 |
apply (case_tac "b = 0", simp) |
785 |
apply (case_tac "c = 0", simp) |
|
13524 | 786 |
apply (auto simp add: linorder_neq_iff zmod_zmult_zmult1_aux1 zmod_zmult_zmult1_aux2) |
13183 | 787 |
done |
788 |
||
789 |
lemma zmod_zmult_zmult2: "(a*c) mod (b*c) = (a mod b) * (c::int)" |
|
790 |
apply (cut_tac c = c in zmod_zmult_zmult1) |
|
791 |
apply (auto simp add: zmult_commute) |
|
792 |
done |
|
793 |
||
794 |
||
14271 | 795 |
subsection {*Splitting Rules for div and mod*} |
13260 | 796 |
|
797 |
text{*The proofs of the two lemmas below are essentially identical*} |
|
798 |
||
799 |
lemma split_pos_lemma: |
|
800 |
"0<k ==> |
|
14288 | 801 |
P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)" |
13260 | 802 |
apply (rule iffI) |
803 |
apply clarify |
|
804 |
apply (erule_tac P="P ?x ?y" in rev_mp) |
|
805 |
apply (subst zmod_zadd1_eq) |
|
806 |
apply (subst zdiv_zadd1_eq) |
|
807 |
apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial) |
|
808 |
txt{*converse direction*} |
|
809 |
apply (drule_tac x = "n div k" in spec) |
|
810 |
apply (drule_tac x = "n mod k" in spec) |
|
13788 | 811 |
apply (simp) |
13260 | 812 |
done |
813 |
||
814 |
lemma split_neg_lemma: |
|
815 |
"k<0 ==> |
|
14288 | 816 |
P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)" |
13260 | 817 |
apply (rule iffI) |
818 |
apply clarify |
|
819 |
apply (erule_tac P="P ?x ?y" in rev_mp) |
|
820 |
apply (subst zmod_zadd1_eq) |
|
821 |
apply (subst zdiv_zadd1_eq) |
|
822 |
apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial) |
|
823 |
txt{*converse direction*} |
|
824 |
apply (drule_tac x = "n div k" in spec) |
|
825 |
apply (drule_tac x = "n mod k" in spec) |
|
13788 | 826 |
apply (simp) |
13260 | 827 |
done |
828 |
||
829 |
lemma split_zdiv: |
|
830 |
"P(n div k :: int) = |
|
831 |
((k = 0 --> P 0) & |
|
14288 | 832 |
(0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i)) & |
833 |
(k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i)))" |
|
13260 | 834 |
apply (case_tac "k=0") |
15013 | 835 |
apply (simp) |
13260 | 836 |
apply (simp only: linorder_neq_iff) |
837 |
apply (erule disjE) |
|
838 |
apply (simp_all add: split_pos_lemma [of concl: "%x y. P x"] |
|
839 |
split_neg_lemma [of concl: "%x y. P x"]) |
|
840 |
done |
|
841 |
||
842 |
lemma split_zmod: |
|
843 |
"P(n mod k :: int) = |
|
844 |
((k = 0 --> P n) & |
|
14288 | 845 |
(0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P j)) & |
846 |
(k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P j)))" |
|
13260 | 847 |
apply (case_tac "k=0") |
15013 | 848 |
apply (simp) |
13260 | 849 |
apply (simp only: linorder_neq_iff) |
850 |
apply (erule disjE) |
|
851 |
apply (simp_all add: split_pos_lemma [of concl: "%x y. P y"] |
|
852 |
split_neg_lemma [of concl: "%x y. P y"]) |
|
853 |
done |
|
854 |
||
855 |
(* 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
|
856 |
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
|
857 |
declare split_zmod [of _ _ "number_of k", simplified, standard, arith_split] |
13260 | 858 |
|
859 |
||
14271 | 860 |
subsection{*Speeding up the Division Algorithm with Shifting*} |
13183 | 861 |
|
862 |
(** computing div by shifting **) |
|
863 |
||
14288 | 864 |
lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a" |
865 |
proof cases |
|
866 |
assume "a=0" |
|
867 |
thus ?thesis by simp |
|
868 |
next |
|
869 |
assume "a\<noteq>0" and le_a: "0\<le>a" |
|
870 |
hence a_pos: "1 \<le> a" by arith |
|
871 |
hence one_less_a2: "1 < 2*a" by arith |
|
872 |
hence le_2a: "2 * (1 + b mod a) \<le> 2 * a" |
|
873 |
by (simp add: mult_le_cancel_left zadd_commute [of 1] add1_zle_eq) |
|
874 |
with a_pos have "0 \<le> b mod a" by simp |
|
875 |
hence le_addm: "0 \<le> 1 mod (2*a) + 2*(b mod a)" |
|
876 |
by (simp add: mod_pos_pos_trivial one_less_a2) |
|
877 |
with le_2a |
|
878 |
have "(1 mod (2*a) + 2*(b mod a)) div (2*a) = 0" |
|
879 |
by (simp add: div_pos_pos_trivial le_addm mod_pos_pos_trivial one_less_a2 |
|
880 |
right_distrib) |
|
881 |
thus ?thesis |
|
882 |
by (subst zdiv_zadd1_eq, |
|
883 |
simp add: zdiv_zmult_zmult1 zmod_zmult_zmult1 one_less_a2 |
|
884 |
div_pos_pos_trivial) |
|
885 |
qed |
|
13183 | 886 |
|
14288 | 887 |
lemma neg_zdiv_mult_2: "a \<le> (0::int) ==> (1 + 2*b) div (2*a) = (b+1) div a" |
13183 | 888 |
apply (subgoal_tac " (1 + 2* (-b - 1)) div (2 * (-a)) = (-b - 1) div (-a) ") |
889 |
apply (rule_tac [2] pos_zdiv_mult_2) |
|
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
890 |
apply (auto simp add: minus_mult_right [symmetric] right_diff_distrib) |
13183 | 891 |
apply (subgoal_tac " (-1 - (2 * b)) = - (1 + (2 * b))") |
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
892 |
apply (simp only: zdiv_zminus_zminus diff_minus minus_add_distrib [symmetric], |
13183 | 893 |
simp) |
894 |
done |
|
895 |
||
896 |
||
897 |
(*Not clear why this must be proved separately; probably number_of causes |
|
898 |
simplification problems*) |
|
14288 | 899 |
lemma not_0_le_lemma: "~ 0 \<le> x ==> x \<le> (0::int)" |
13183 | 900 |
by auto |
901 |
||
902 |
lemma zdiv_number_of_BIT[simp]: |
|
903 |
"number_of (v BIT b) div number_of (w BIT False) = |
|
14288 | 904 |
(if ~b | (0::int) \<le> number_of w |
13183 | 905 |
then number_of v div (number_of w) |
906 |
else (number_of v + (1::int)) div (number_of w))" |
|
15013 | 907 |
apply (simp only: number_of_eq Bin_simps UNIV_I split: split_if) |
908 |
apply (simp add: zdiv_zmult_zmult1 pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac) |
|
13183 | 909 |
done |
910 |
||
911 |
||
15013 | 912 |
subsection{*Computing mod by Shifting (proofs resemble those for div)*} |
13183 | 913 |
|
914 |
lemma pos_zmod_mult_2: |
|
14288 | 915 |
"(0::int) \<le> a ==> (1 + 2*b) mod (2*a) = 1 + 2 * (b mod a)" |
15013 | 916 |
apply (case_tac "a = 0", simp) |
14288 | 917 |
apply (subgoal_tac "1 \<le> a") |
13183 | 918 |
prefer 2 apply arith |
919 |
apply (subgoal_tac "1 < a * 2") |
|
920 |
prefer 2 apply arith |
|
14288 | 921 |
apply (subgoal_tac "2* (1 + b mod a) \<le> 2*a") |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
922 |
apply (rule_tac [2] mult_left_mono) |
13183 | 923 |
apply (auto simp add: zadd_commute [of 1] zmult_commute add1_zle_eq |
924 |
pos_mod_bound) |
|
925 |
apply (subst zmod_zadd1_eq) |
|
926 |
apply (simp add: zmod_zmult_zmult2 mod_pos_pos_trivial) |
|
927 |
apply (rule mod_pos_pos_trivial) |
|
14288 | 928 |
apply (auto simp add: mod_pos_pos_trivial left_distrib) |
929 |
apply (subgoal_tac "0 \<le> b mod a", arith) |
|
13788 | 930 |
apply (simp) |
13183 | 931 |
done |
932 |
||
933 |
lemma neg_zmod_mult_2: |
|
14288 | 934 |
"a \<le> (0::int) ==> (1 + 2*b) mod (2*a) = 2 * ((b+1) mod a) - 1" |
13183 | 935 |
apply (subgoal_tac "(1 + 2* (-b - 1)) mod (2* (-a)) = |
936 |
1 + 2* ((-b - 1) mod (-a))") |
|
937 |
apply (rule_tac [2] pos_zmod_mult_2) |
|
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
938 |
apply (auto simp add: minus_mult_right [symmetric] right_diff_distrib) |
13183 | 939 |
apply (subgoal_tac " (-1 - (2 * b)) = - (1 + (2 * b))") |
940 |
prefer 2 apply simp |
|
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
941 |
apply (simp only: zmod_zminus_zminus diff_minus minus_add_distrib [symmetric]) |
13183 | 942 |
done |
943 |
||
944 |
lemma zmod_number_of_BIT [simp]: |
|
945 |
"number_of (v BIT b) mod number_of (w BIT False) = |
|
946 |
(if b then |
|
14288 | 947 |
if (0::int) \<le> number_of w |
13183 | 948 |
then 2 * (number_of v mod number_of w) + 1 |
949 |
else 2 * ((number_of v + (1::int)) mod number_of w) - 1 |
|
950 |
else 2 * (number_of v mod number_of w))" |
|
15013 | 951 |
apply (simp only: number_of_eq Bin_simps UNIV_I split: split_if) |
952 |
apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2 |
|
953 |
not_0_le_lemma neg_zmod_mult_2 add_ac) |
|
13183 | 954 |
done |
955 |
||
956 |
||
957 |
||
15013 | 958 |
subsection{*Quotients of Signs*} |
13183 | 959 |
|
960 |
lemma div_neg_pos_less0: "[| a < (0::int); 0 < b |] ==> a div b < 0" |
|
14288 | 961 |
apply (subgoal_tac "a div b \<le> -1", force) |
13183 | 962 |
apply (rule order_trans) |
963 |
apply (rule_tac a' = "-1" in zdiv_mono1) |
|
964 |
apply (auto simp add: zdiv_minus1) |
|
965 |
done |
|
966 |
||
14288 | 967 |
lemma div_nonneg_neg_le0: "[| (0::int) \<le> a; b < 0 |] ==> a div b \<le> 0" |
13183 | 968 |
by (drule zdiv_mono1_neg, auto) |
969 |
||
14288 | 970 |
lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \<le> a div b) = (0 \<le> a)" |
13183 | 971 |
apply auto |
972 |
apply (drule_tac [2] zdiv_mono1) |
|
973 |
apply (auto simp add: linorder_neq_iff) |
|
974 |
apply (simp (no_asm_use) add: linorder_not_less [symmetric]) |
|
975 |
apply (blast intro: div_neg_pos_less0) |
|
976 |
done |
|
977 |
||
978 |
lemma neg_imp_zdiv_nonneg_iff: |
|
14288 | 979 |
"b < (0::int) ==> (0 \<le> a div b) = (a \<le> (0::int))" |
13183 | 980 |
apply (subst zdiv_zminus_zminus [symmetric]) |
981 |
apply (subst pos_imp_zdiv_nonneg_iff, auto) |
|
982 |
done |
|
983 |
||
14288 | 984 |
(*But not (a div b \<le> 0 iff a\<le>0); consider a=1, b=2 when a div b = 0.*) |
13183 | 985 |
lemma pos_imp_zdiv_neg_iff: "(0::int) < b ==> (a div b < 0) = (a < 0)" |
986 |
by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff) |
|
987 |
||
14288 | 988 |
(*Again the law fails for \<le>: consider a = -1, b = -2 when a div b = 0*) |
13183 | 989 |
lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)" |
990 |
by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff) |
|
991 |
||
13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
992 |
|
14271 | 993 |
subsection {* The Divides Relation *} |
13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
994 |
|
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
995 |
lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))" |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
996 |
by(simp add:dvd_def zmod_eq_0_iff) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
997 |
|
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
998 |
lemma zdvd_0_right [iff]: "(m::int) dvd 0" |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
999 |
apply (unfold dvd_def) |
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
1000 |
apply (blast intro: mult_zero_right [symmetric]) |
13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1001 |
done |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1002 |
|
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1003 |
lemma zdvd_0_left [iff]: "(0 dvd (m::int)) = (m = 0)" |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1004 |
by (unfold dvd_def, auto) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1005 |
|
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1006 |
lemma zdvd_1_left [iff]: "1 dvd (m::int)" |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1007 |
by (unfold dvd_def, simp) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1008 |
|
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1009 |
lemma zdvd_refl [simp]: "m dvd (m::int)" |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1010 |
apply (unfold dvd_def) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1011 |
apply (blast intro: zmult_1_right [symmetric]) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1012 |
done |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1013 |
|
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1014 |
lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)" |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1015 |
apply (unfold dvd_def) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1016 |
apply (blast intro: zmult_assoc) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1017 |
done |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1018 |
|
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1019 |
lemma zdvd_zminus_iff: "(m dvd -n) = (m dvd (n::int))" |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1020 |
apply (unfold dvd_def, auto) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1021 |
apply (rule_tac [!] x = "-k" in exI, auto) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1022 |
done |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1023 |
|
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1024 |
lemma zdvd_zminus2_iff: "(-m dvd n) = (m dvd (n::int))" |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1025 |
apply (unfold dvd_def, auto) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1026 |
apply (rule_tac [!] x = "-k" in exI, auto) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1027 |
done |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1028 |
|
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1029 |
lemma zdvd_anti_sym: |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1030 |
"0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)" |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1031 |
apply (unfold dvd_def, auto) |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1032 |
apply (simp add: zmult_assoc zmult_eq_self_iff zero_less_mult_iff zmult_eq_1_iff) |
13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1033 |
done |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1034 |
|
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1035 |
lemma zdvd_zadd: "k dvd m ==> k dvd n ==> k dvd (m + n :: int)" |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1036 |
apply (unfold dvd_def) |
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
1037 |
apply (blast intro: right_distrib [symmetric]) |
13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1038 |
done |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1039 |
|
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1040 |
lemma zdvd_zdiff: "k dvd m ==> k dvd n ==> k dvd (m - n :: int)" |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1041 |
apply (unfold dvd_def) |
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
1042 |
apply (blast intro: right_diff_distrib [symmetric]) |
13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1043 |
done |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1044 |
|
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1045 |
lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)" |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1046 |
apply (subgoal_tac "m = n + (m - n)") |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1047 |
apply (erule ssubst) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1048 |
apply (blast intro: zdvd_zadd, simp) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1049 |
done |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1050 |
|
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1051 |
lemma zdvd_zmult: "k dvd (n::int) ==> k dvd m * n" |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1052 |
apply (unfold dvd_def) |
14271 | 1053 |
apply (blast intro: mult_left_commute) |
13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1054 |
done |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1055 |
|
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1056 |
lemma zdvd_zmult2: "k dvd (m::int) ==> k dvd m * n" |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1057 |
apply (subst zmult_commute) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1058 |
apply (erule zdvd_zmult) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1059 |
done |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1060 |
|
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1061 |
lemma [iff]: "(k::int) dvd m * k" |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1062 |
apply (rule zdvd_zmult) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1063 |
apply (rule zdvd_refl) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1064 |
done |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1065 |
|
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1066 |
lemma [iff]: "(k::int) dvd k * m" |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1067 |
apply (rule zdvd_zmult2) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1068 |
apply (rule zdvd_refl) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1069 |
done |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1070 |
|
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1071 |
lemma zdvd_zmultD2: "j * k dvd n ==> j dvd (n::int)" |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1072 |
apply (unfold dvd_def) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1073 |
apply (simp add: zmult_assoc, blast) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1074 |
done |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1075 |
|
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1076 |
lemma zdvd_zmultD: "j * k dvd n ==> k dvd (n::int)" |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1077 |
apply (rule zdvd_zmultD2) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1078 |
apply (subst zmult_commute, assumption) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1079 |
done |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1080 |
|
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1081 |
lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n" |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1082 |
apply (unfold dvd_def, clarify) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1083 |
apply (rule_tac x = "k * ka" in exI) |
14271 | 1084 |
apply (simp add: mult_ac) |
13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1085 |
done |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1086 |
|
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1087 |
lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))" |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1088 |
apply (rule iffI) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1089 |
apply (erule_tac [2] zdvd_zadd) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1090 |
apply (subgoal_tac "n = (n + k * m) - k * m") |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1091 |
apply (erule ssubst) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1092 |
apply (erule zdvd_zdiff, simp_all) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1093 |
done |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1094 |
|
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1095 |
lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n" |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1096 |
apply (unfold dvd_def) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1097 |
apply (auto simp add: zmod_zmult_zmult1) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1098 |
done |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1099 |
|
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1100 |
lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)" |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1101 |
apply (subgoal_tac "k dvd n * (m div n) + m mod n") |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1102 |
apply (simp add: zmod_zdiv_equality [symmetric]) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1103 |
apply (simp only: zdvd_zadd zdvd_zmult2) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1104 |
done |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1105 |
|
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1106 |
lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)" |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1107 |
apply (unfold dvd_def, auto) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1108 |
apply (subgoal_tac "0 < n") |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1109 |
prefer 2 |
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14353
diff
changeset
|
1110 |
apply (blast intro: order_less_trans) |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1111 |
apply (simp add: zero_less_mult_iff) |
13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1112 |
apply (subgoal_tac "n * k < n * 1") |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
1113 |
apply (drule mult_less_cancel_left [THEN iffD1], auto) |
13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1114 |
done |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1115 |
|
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1116 |
lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))" |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1117 |
apply (auto simp add: dvd_def nat_abs_mult_distrib) |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1118 |
apply (auto simp add: nat_eq_iff abs_if split add: split_if_asm) |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1119 |
apply (rule_tac x = "-(int k)" in exI) |
13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1120 |
apply (auto simp add: zmult_int [symmetric]) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1121 |
done |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1122 |
|
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1123 |
lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)" |
15003 | 1124 |
apply (auto simp add: dvd_def abs_if zmult_int [symmetric]) |
13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1125 |
apply (rule_tac [3] x = "nat k" in exI) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1126 |
apply (rule_tac [2] x = "-(int k)" in exI) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1127 |
apply (rule_tac x = "nat (-k)" in exI) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1128 |
apply (cut_tac [3] k = m in int_less_0_conv) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1129 |
apply (cut_tac k = m in int_less_0_conv) |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1130 |
apply (auto simp add: zero_le_mult_iff mult_less_0_iff |
13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1131 |
nat_mult_distrib [symmetric] nat_eq_iff2) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1132 |
done |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1133 |
|
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1134 |
lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)" |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1135 |
apply (auto simp add: dvd_def zmult_int [symmetric]) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1136 |
apply (rule_tac x = "nat k" in exI) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1137 |
apply (cut_tac k = m in int_less_0_conv) |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1138 |
apply (auto simp add: zero_le_mult_iff mult_less_0_iff |
13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1139 |
nat_mult_distrib [symmetric] nat_eq_iff2) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1140 |
done |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1141 |
|
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1142 |
lemma zminus_dvd_iff [iff]: "(-z dvd w) = (z dvd (w::int))" |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1143 |
apply (auto simp add: dvd_def) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1144 |
apply (rule_tac [!] x = "-k" in exI, auto) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1145 |
done |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1146 |
|
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1147 |
lemma dvd_zminus_iff [iff]: "(z dvd -w) = (z dvd (w::int))" |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1148 |
apply (auto simp add: dvd_def) |
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14353
diff
changeset
|
1149 |
apply (drule minus_equation_iff [THEN iffD1]) |
13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1150 |
apply (rule_tac [!] x = "-k" in exI, auto) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1151 |
done |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1152 |
|
14288 | 1153 |
lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)" |
13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1154 |
apply (rule_tac z=n in int_cases) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1155 |
apply (auto simp add: dvd_int_iff) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1156 |
apply (rule_tac z=z in int_cases) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1157 |
apply (auto simp add: dvd_imp_le) |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1158 |
done |
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1159 |
|
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset
|
1160 |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1161 |
subsection{*Integer Powers*} |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1162 |
|
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1163 |
instance int :: power .. |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1164 |
|
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1165 |
primrec |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1166 |
"p ^ 0 = 1" |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1167 |
"p ^ (Suc n) = (p::int) * (p ^ n)" |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1168 |
|
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1169 |
|
15003 | 1170 |
instance int :: recpower |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1171 |
proof |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1172 |
fix z :: int |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1173 |
fix n :: nat |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1174 |
show "z^0 = 1" by simp |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1175 |
show "z^(Suc n) = z * (z^n)" by simp |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1176 |
qed |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1177 |
|
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1178 |
|
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1179 |
lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m" |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1180 |
apply (induct_tac "y", auto) |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1181 |
apply (rule zmod_zmult1_eq [THEN trans]) |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1182 |
apply (simp (no_asm_simp)) |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1183 |
apply (rule zmod_zmult_distrib [symmetric]) |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1184 |
done |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1185 |
|
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1186 |
lemma zpower_zadd_distrib: "x^(y+z) = ((x^y)*(x^z)::int)" |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1187 |
by (rule Power.power_add) |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1188 |
|
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1189 |
lemma zpower_zpower: "(x^y)^z = (x^(y*z)::int)" |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1190 |
by (rule Power.power_mult [symmetric]) |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1191 |
|
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1192 |
lemma zero_less_zpower_abs_iff [simp]: |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1193 |
"(0 < (abs x)^n) = (x \<noteq> (0::int) | n=0)" |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1194 |
apply (induct_tac "n") |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1195 |
apply (auto simp add: zero_less_mult_iff) |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1196 |
done |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1197 |
|
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1198 |
lemma zero_le_zpower_abs [simp]: "(0::int) <= (abs x)^n" |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1199 |
apply (induct_tac "n") |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1200 |
apply (auto simp add: zero_le_mult_iff) |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1201 |
done |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1202 |
|
15101 | 1203 |
lemma zdiv_int: "int (a div b) = (int a) div (int b)" |
1204 |
apply (subst split_div, auto) |
|
1205 |
apply (subst split_zdiv, auto) |
|
1206 |
apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in IntDiv.unique_quotient) |
|
1207 |
apply (auto simp add: IntDiv.quorem_def int_eq_of_nat) |
|
1208 |
done |
|
1209 |
||
1210 |
lemma zmod_int: "int (a mod b) = (int a) mod (int b)" |
|
1211 |
apply (subst split_mod, auto) |
|
1212 |
apply (subst split_zmod, auto) |
|
1213 |
apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia in IntDiv.unique_remainder) |
|
1214 |
apply (auto simp add: IntDiv.quorem_def int_eq_of_nat) |
|
1215 |
done |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1216 |
|
13183 | 1217 |
ML |
1218 |
{* |
|
1219 |
val quorem_def = thm "quorem_def"; |
|
1220 |
||
1221 |
val unique_quotient = thm "unique_quotient"; |
|
1222 |
val unique_remainder = thm "unique_remainder"; |
|
1223 |
val adjust_eq = thm "adjust_eq"; |
|
1224 |
val posDivAlg_eqn = thm "posDivAlg_eqn"; |
|
1225 |
val posDivAlg_correct = thm "posDivAlg_correct"; |
|
1226 |
val negDivAlg_eqn = thm "negDivAlg_eqn"; |
|
1227 |
val negDivAlg_correct = thm "negDivAlg_correct"; |
|
1228 |
val quorem_0 = thm "quorem_0"; |
|
1229 |
val posDivAlg_0 = thm "posDivAlg_0"; |
|
1230 |
val negDivAlg_minus1 = thm "negDivAlg_minus1"; |
|
1231 |
val negateSnd_eq = thm "negateSnd_eq"; |
|
1232 |
val quorem_neg = thm "quorem_neg"; |
|
1233 |
val divAlg_correct = thm "divAlg_correct"; |
|
1234 |
val DIVISION_BY_ZERO = thm "DIVISION_BY_ZERO"; |
|
1235 |
val zmod_zdiv_equality = thm "zmod_zdiv_equality"; |
|
1236 |
val pos_mod_conj = thm "pos_mod_conj"; |
|
1237 |
val pos_mod_sign = thm "pos_mod_sign"; |
|
1238 |
val neg_mod_conj = thm "neg_mod_conj"; |
|
1239 |
val neg_mod_sign = thm "neg_mod_sign"; |
|
1240 |
val quorem_div_mod = thm "quorem_div_mod"; |
|
1241 |
val quorem_div = thm "quorem_div"; |
|
1242 |
val quorem_mod = thm "quorem_mod"; |
|
1243 |
val div_pos_pos_trivial = thm "div_pos_pos_trivial"; |
|
1244 |
val div_neg_neg_trivial = thm "div_neg_neg_trivial"; |
|
1245 |
val div_pos_neg_trivial = thm "div_pos_neg_trivial"; |
|
1246 |
val mod_pos_pos_trivial = thm "mod_pos_pos_trivial"; |
|
1247 |
val mod_neg_neg_trivial = thm "mod_neg_neg_trivial"; |
|
1248 |
val mod_pos_neg_trivial = thm "mod_pos_neg_trivial"; |
|
1249 |
val zdiv_zminus_zminus = thm "zdiv_zminus_zminus"; |
|
1250 |
val zmod_zminus_zminus = thm "zmod_zminus_zminus"; |
|
1251 |
val zdiv_zminus1_eq_if = thm "zdiv_zminus1_eq_if"; |
|
1252 |
val zmod_zminus1_eq_if = thm "zmod_zminus1_eq_if"; |
|
1253 |
val zdiv_zminus2 = thm "zdiv_zminus2"; |
|
1254 |
val zmod_zminus2 = thm "zmod_zminus2"; |
|
1255 |
val zdiv_zminus2_eq_if = thm "zdiv_zminus2_eq_if"; |
|
1256 |
val zmod_zminus2_eq_if = thm "zmod_zminus2_eq_if"; |
|
1257 |
val self_quotient = thm "self_quotient"; |
|
1258 |
val self_remainder = thm "self_remainder"; |
|
1259 |
val zdiv_self = thm "zdiv_self"; |
|
1260 |
val zmod_self = thm "zmod_self"; |
|
1261 |
val zdiv_zero = thm "zdiv_zero"; |
|
1262 |
val div_eq_minus1 = thm "div_eq_minus1"; |
|
1263 |
val zmod_zero = thm "zmod_zero"; |
|
1264 |
val zdiv_minus1 = thm "zdiv_minus1"; |
|
1265 |
val zmod_minus1 = thm "zmod_minus1"; |
|
1266 |
val div_pos_pos = thm "div_pos_pos"; |
|
1267 |
val mod_pos_pos = thm "mod_pos_pos"; |
|
1268 |
val div_neg_pos = thm "div_neg_pos"; |
|
1269 |
val mod_neg_pos = thm "mod_neg_pos"; |
|
1270 |
val div_pos_neg = thm "div_pos_neg"; |
|
1271 |
val mod_pos_neg = thm "mod_pos_neg"; |
|
1272 |
val div_neg_neg = thm "div_neg_neg"; |
|
1273 |
val mod_neg_neg = thm "mod_neg_neg"; |
|
1274 |
val zmod_1 = thm "zmod_1"; |
|
1275 |
val zdiv_1 = thm "zdiv_1"; |
|
1276 |
val zmod_minus1_right = thm "zmod_minus1_right"; |
|
1277 |
val zdiv_minus1_right = thm "zdiv_minus1_right"; |
|
1278 |
val zdiv_mono1 = thm "zdiv_mono1"; |
|
1279 |
val zdiv_mono1_neg = thm "zdiv_mono1_neg"; |
|
1280 |
val zdiv_mono2 = thm "zdiv_mono2"; |
|
1281 |
val zdiv_mono2_neg = thm "zdiv_mono2_neg"; |
|
1282 |
val zdiv_zmult1_eq = thm "zdiv_zmult1_eq"; |
|
1283 |
val zmod_zmult1_eq = thm "zmod_zmult1_eq"; |
|
1284 |
val zmod_zmult1_eq' = thm "zmod_zmult1_eq'"; |
|
1285 |
val zmod_zmult_distrib = thm "zmod_zmult_distrib"; |
|
1286 |
val zdiv_zmult_self1 = thm "zdiv_zmult_self1"; |
|
1287 |
val zdiv_zmult_self2 = thm "zdiv_zmult_self2"; |
|
1288 |
val zmod_zmult_self1 = thm "zmod_zmult_self1"; |
|
1289 |
val zmod_zmult_self2 = thm "zmod_zmult_self2"; |
|
1290 |
val zmod_eq_0_iff = thm "zmod_eq_0_iff"; |
|
1291 |
val zdiv_zadd1_eq = thm "zdiv_zadd1_eq"; |
|
1292 |
val zmod_zadd1_eq = thm "zmod_zadd1_eq"; |
|
1293 |
val mod_div_trivial = thm "mod_div_trivial"; |
|
1294 |
val mod_mod_trivial = thm "mod_mod_trivial"; |
|
1295 |
val zmod_zadd_left_eq = thm "zmod_zadd_left_eq"; |
|
1296 |
val zmod_zadd_right_eq = thm "zmod_zadd_right_eq"; |
|
1297 |
val zdiv_zadd_self1 = thm "zdiv_zadd_self1"; |
|
1298 |
val zdiv_zadd_self2 = thm "zdiv_zadd_self2"; |
|
1299 |
val zmod_zadd_self1 = thm "zmod_zadd_self1"; |
|
1300 |
val zmod_zadd_self2 = thm "zmod_zadd_self2"; |
|
1301 |
val zdiv_zmult2_eq = thm "zdiv_zmult2_eq"; |
|
1302 |
val zmod_zmult2_eq = thm "zmod_zmult2_eq"; |
|
1303 |
val zdiv_zmult_zmult1 = thm "zdiv_zmult_zmult1"; |
|
1304 |
val zdiv_zmult_zmult2 = thm "zdiv_zmult_zmult2"; |
|
1305 |
val zmod_zmult_zmult1 = thm "zmod_zmult_zmult1"; |
|
1306 |
val zmod_zmult_zmult2 = thm "zmod_zmult_zmult2"; |
|
1307 |
val pos_zdiv_mult_2 = thm "pos_zdiv_mult_2"; |
|
1308 |
val neg_zdiv_mult_2 = thm "neg_zdiv_mult_2"; |
|
1309 |
val zdiv_number_of_BIT = thm "zdiv_number_of_BIT"; |
|
1310 |
val pos_zmod_mult_2 = thm "pos_zmod_mult_2"; |
|
1311 |
val neg_zmod_mult_2 = thm "neg_zmod_mult_2"; |
|
1312 |
val zmod_number_of_BIT = thm "zmod_number_of_BIT"; |
|
1313 |
val div_neg_pos_less0 = thm "div_neg_pos_less0"; |
|
1314 |
val div_nonneg_neg_le0 = thm "div_nonneg_neg_le0"; |
|
1315 |
val pos_imp_zdiv_nonneg_iff = thm "pos_imp_zdiv_nonneg_iff"; |
|
1316 |
val neg_imp_zdiv_nonneg_iff = thm "neg_imp_zdiv_nonneg_iff"; |
|
1317 |
val pos_imp_zdiv_neg_iff = thm "pos_imp_zdiv_neg_iff"; |
|
1318 |
val neg_imp_zdiv_neg_iff = thm "neg_imp_zdiv_neg_iff"; |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1319 |
|
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1320 |
val zpower_zmod = thm "zpower_zmod"; |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1321 |
val zpower_zadd_distrib = thm "zpower_zadd_distrib"; |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1322 |
val zpower_zpower = thm "zpower_zpower"; |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1323 |
val zero_less_zpower_abs_iff = thm "zero_less_zpower_abs_iff"; |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset
|
1324 |
val zero_le_zpower_abs = thm "zero_le_zpower_abs"; |
13183 | 1325 |
*} |
1326 |
||
6917 | 1327 |
end |