author  berghofe 
Wed, 24 Nov 2004 10:23:36 +0100  
changeset 15320  dfc2654eea9f 
parent 15251  bb6f072c8d10 
child 15620  8ccdc8bc66a2 
permissions  rwrr 
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 

15221  6 
*) 
7 

8 

9 
header{*The Division Operators div and mod; the Divides Relation dvd*} 

10 

11 
theory IntDiv 

12 
imports IntArith Recdef 

13 
files ("IntDiv_setup.ML") 

14 
begin 

15 

16 
declare zless_nat_conj [simp] 

17 

18 
constdefs 

19 
quorem :: "(int*int) * (int*int) => bool" 

20 
{*definition of quotient and remainder*} 

21 
"quorem == %((a,b), (q,r)). 

22 
a = b*q + r & 

23 
(if 0 < b then 0\<le>r & r<b else b<r & r \<le> 0)" 

24 

25 
adjust :: "[int, int*int] => int*int" 

26 
{*for the division algorithm*} 

27 
"adjust b == %(q,r). if 0 \<le> rb then (2*q + 1, rb) 

28 
else (2*q, r)" 

29 

30 
text{*algorithm for the case @{text "a\<ge>0, b>0"}*} 

31 
consts posDivAlg :: "int*int => int*int" 

32 
recdef posDivAlg "inv_image less_than (%(a,b). nat(a  b + 1))" 

33 
"posDivAlg (a,b) = 

34 
(if (a<b  b\<le>0) then (0,a) 

35 
else adjust b (posDivAlg(a, 2*b)))" 

13183  36 

15221  37 
text{*algorithm for the case @{text "a<0, b>0"}*} 
38 
consts negDivAlg :: "int*int => int*int" 

39 
recdef negDivAlg "inv_image less_than (%(a,b). nat( a  b))" 

40 
"negDivAlg (a,b) = 

41 
(if (0\<le>a+b  b\<le>0) then (1,a+b) 

42 
else adjust b (negDivAlg(a, 2*b)))" 

43 

44 
text{*algorithm for the general case @{term "b\<noteq>0"}*} 

45 
constdefs 

46 
negateSnd :: "int*int => int*int" 

47 
"negateSnd == %(q,r). (q,r)" 

48 

49 
divAlg :: "int*int => int*int" 

50 
{*The full division algorithm considers all possible signs for a, b 

51 
including the special case @{text "a=0, b<0"} because 

52 
@{term negDivAlg} requires @{term "a<0"}.*} 

53 
"divAlg == 

54 
%(a,b). if 0\<le>a then 

55 
if 0\<le>b then posDivAlg (a,b) 

56 
else if a=0 then (0,0) 

57 
else negateSnd (negDivAlg (a,b)) 

58 
else 

59 
if 0<b then negDivAlg (a,b) 

60 
else negateSnd (posDivAlg (a,b))" 

61 

62 
instance 

63 
int :: "Divides.div" .. {*avoid clash with 'div' token*} 

64 

65 
text{*The operators are defined with reference to the algorithm, which is 

66 
proved to satisfy the specification.*} 

67 
defs 

68 
div_def: "a div b == fst (divAlg (a,b))" 

69 
mod_def: "a mod b == snd (divAlg (a,b))" 

70 

71 

72 
text{* 

13183  73 
Here is the division algorithm in ML: 
74 

15221  75 
\begin{verbatim} 
13183  76 
fun posDivAlg (a,b) = 
77 
if a<b then (0,a) 

78 
else let val (q,r) = posDivAlg(a, 2*b) 

14288  79 
in if 0\<le>rb then (2*q+1, rb) else (2*q, r) 
13183  80 
end 
81 

82 
fun negDivAlg (a,b) = 

14288  83 
if 0\<le>a+b then (~1,a+b) 
13183  84 
else let val (q,r) = negDivAlg(a, 2*b) 
14288  85 
in if 0\<le>rb then (2*q+1, rb) else (2*q, r) 
13183  86 
end; 
87 

88 
fun negateSnd (q,r:int) = (q,~r); 

89 

14288  90 
fun divAlg (a,b) = if 0\<le>a then 
13183  91 
if b>0 then posDivAlg (a,b) 
92 
else if a=0 then (0,0) 

93 
else negateSnd (negDivAlg (~a,~b)) 

94 
else 

95 
if 0<b then negDivAlg (a,b) 

96 
else negateSnd (posDivAlg (~a,~b)); 

15221  97 
\end{verbatim} 
98 
*} 

13183  99 

100 

101 

14271  102 
subsection{*Uniqueness and Monotonicity of Quotients and Remainders*} 
13183  103 

104 
lemma unique_quotient_lemma: 

14288  105 
"[ b*q' + r' \<le> b*q + r; 0 \<le> r'; 0 < b; r < b ] 
106 
==> q' \<le> (q::int)" 

107 
apply (subgoal_tac "r' + b * (q'q) \<le> r") 

14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

108 
prefer 2 apply (simp add: right_diff_distrib) 
13183  109 
apply (subgoal_tac "0 < b * (1 + q  q') ") 
110 
apply (erule_tac [2] order_le_less_trans) 

14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

111 
prefer 2 apply (simp add: right_diff_distrib right_distrib) 
13183  112 
apply (subgoal_tac "b * q' < b * (1 + q) ") 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

113 
prefer 2 apply (simp add: right_diff_distrib right_distrib) 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

114 
apply (simp add: mult_less_cancel_left) 
13183  115 
done 
116 

117 
lemma unique_quotient_lemma_neg: 

14288  118 
"[ b*q' + r' \<le> b*q + r; r \<le> 0; b < 0; b < r' ] 
119 
==> q \<le> (q'::int)" 

13183  120 
by (rule_tac b = "b" and r = "r'" and r' = "r" in unique_quotient_lemma, 
121 
auto) 

122 

123 
lemma unique_quotient: 

15221  124 
"[ quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); b \<noteq> 0 ] 
13183  125 
==> q = q'" 
126 
apply (simp add: quorem_def linorder_neq_iff split: split_if_asm) 

127 
apply (blast intro: order_antisym 

128 
dest: order_eq_refl [THEN unique_quotient_lemma] 

129 
order_eq_refl [THEN unique_quotient_lemma_neg] sym)+ 

130 
done 

131 

132 

133 
lemma unique_remainder: 

15221  134 
"[ quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); b \<noteq> 0 ] 
13183  135 
==> r = r'" 
136 
apply (subgoal_tac "q = q'") 

137 
apply (simp add: quorem_def) 

138 
apply (blast intro: unique_quotient) 

139 
done 

140 

141 

15221  142 
subsection{*Correctness of @{term posDivAlg}, the Algorithm for NonNegative Dividends*} 
14271  143 

144 
text{*And positive divisors*} 

13183  145 

146 
lemma adjust_eq [simp]: 

147 
"adjust b (q,r) = 

148 
(let diff = rb in 

14288  149 
if 0 \<le> diff then (2*q + 1, diff) 
13183  150 
else (2*q, r))" 
151 
by (simp add: Let_def adjust_def) 

152 

153 
declare posDivAlg.simps [simp del] 

154 

15221  155 
text{*use with a simproc to avoid repeatedly proving the premise*} 
13183  156 
lemma posDivAlg_eqn: 
157 
"0 < b ==> 

158 
posDivAlg (a,b) = (if a<b then (0,a) else adjust b (posDivAlg(a, 2*b)))" 

159 
by (rule posDivAlg.simps [THEN trans], simp) 

160 

15221  161 
text{*Correctness of @{term posDivAlg}: it computes quotients correctly*} 
162 
theorem posDivAlg_correct [rule_format]: 

14288  163 
"0 \<le> a > 0 < b > quorem ((a, b), posDivAlg (a, b))" 
13183  164 
apply (induct_tac a b rule: posDivAlg.induct, auto) 
165 
apply (simp_all add: quorem_def) 

166 
(*base case: a<b*) 

167 
apply (simp add: posDivAlg_eqn) 

168 
(*main argument*) 

169 
apply (subst posDivAlg_eqn, simp_all) 

170 
apply (erule splitE) 

14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

171 
apply (auto simp add: right_distrib Let_def) 
13183  172 
done 
173 

174 

15221  175 
subsection{*Correctness of @{term negDivAlg}, the Algorithm for Negative Dividends*} 
14271  176 

177 
text{*And positive divisors*} 

13183  178 

179 
declare negDivAlg.simps [simp del] 

180 

15221  181 
text{*use with a simproc to avoid repeatedly proving the premise*} 
13183  182 
lemma negDivAlg_eqn: 
183 
"0 < b ==> 

184 
negDivAlg (a,b) = 

14288  185 
(if 0\<le>a+b then (1,a+b) else adjust b (negDivAlg(a, 2*b)))" 
13183  186 
by (rule negDivAlg.simps [THEN trans], simp) 
187 

188 
(*Correctness of negDivAlg: it computes quotients correctly 

189 
It doesn't work if a=0 because the 0/b equals 0, not 1*) 

190 
lemma negDivAlg_correct [rule_format]: 

191 
"a < 0 > 0 < b > quorem ((a, b), negDivAlg (a, b))" 

192 
apply (induct_tac a b rule: negDivAlg.induct, auto) 

193 
apply (simp_all add: quorem_def) 

14288  194 
(*base case: 0\<le>a+b*) 
13183  195 
apply (simp add: negDivAlg_eqn) 
196 
(*main argument*) 

197 
apply (subst negDivAlg_eqn, assumption) 

198 
apply (erule splitE) 

14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

199 
apply (auto simp add: right_distrib Let_def) 
13183  200 
done 
201 

202 

14271  203 
subsection{*Existence Shown by Proving the Division Algorithm to be Correct*} 
13183  204 

205 
(*the case a=0*) 

15221  206 
lemma quorem_0: "b \<noteq> 0 ==> quorem ((0,b), (0,0))" 
13183  207 
by (auto simp add: quorem_def linorder_neq_iff) 
208 

209 
lemma posDivAlg_0 [simp]: "posDivAlg (0, b) = (0, 0)" 

210 
by (subst posDivAlg.simps, auto) 

211 

212 
lemma negDivAlg_minus1 [simp]: "negDivAlg (1, b) = (1, b  1)" 

213 
by (subst negDivAlg.simps, auto) 

214 

215 
lemma negateSnd_eq [simp]: "negateSnd(q,r) = (q,r)" 

15221  216 
by (simp add: negateSnd_def) 
13183  217 

218 
lemma quorem_neg: "quorem ((a,b), qr) ==> quorem ((a,b), negateSnd qr)" 

219 
by (auto simp add: split_ifs quorem_def) 

220 

15221  221 
lemma divAlg_correct: "b \<noteq> 0 ==> quorem ((a,b), divAlg(a,b))" 
13183  222 
by (force simp add: linorder_neq_iff quorem_0 divAlg_def quorem_neg 
223 
posDivAlg_correct negDivAlg_correct) 

224 

15221  225 
text{*Arbitrary definitions for division by zero. Useful to simplify 
226 
certain equations.*} 

13183  227 

14271  228 
lemma DIVISION_BY_ZERO [simp]: "a div (0::int) = 0 & a mod (0::int) = a" 
229 
by (simp add: div_def mod_def divAlg_def posDivAlg.simps) 

13183  230 

15221  231 

232 
text{*Basic laws about division and remainder*} 

13183  233 

234 
lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)" 

15013  235 
apply (case_tac "b = 0", simp) 
13183  236 
apply (cut_tac a = a and b = b in divAlg_correct) 
237 
apply (auto simp add: quorem_def div_def mod_def) 

238 
done 

239 

13517  240 
lemma zdiv_zmod_equality: "(b * (a div b) + (a mod b)) + k = (a::int)+k" 
241 
by(simp add: zmod_zdiv_equality[symmetric]) 

242 

243 
lemma zdiv_zmod_equality2: "((a div b) * b + (a mod b)) + k = (a::int)+k" 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15221
diff
changeset

244 
by(simp add: mult_commute zmod_zdiv_equality[symmetric]) 
13517  245 

246 
use "IntDiv_setup.ML" 

247 

14288  248 
lemma pos_mod_conj : "(0::int) < b ==> 0 \<le> a mod b & a mod b < b" 
13183  249 
apply (cut_tac a = a and b = b in divAlg_correct) 
250 
apply (auto simp add: quorem_def mod_def) 

251 
done 

252 

13788  253 
lemmas pos_mod_sign[simp] = pos_mod_conj [THEN conjunct1, standard] 
254 
and pos_mod_bound[simp] = pos_mod_conj [THEN conjunct2, standard] 

13183  255 

14288  256 
lemma neg_mod_conj : "b < (0::int) ==> a mod b \<le> 0 & b < a mod b" 
13183  257 
apply (cut_tac a = a and b = b in divAlg_correct) 
258 
apply (auto simp add: quorem_def div_def mod_def) 

259 
done 

260 

13788  261 
lemmas neg_mod_sign[simp] = neg_mod_conj [THEN conjunct1, standard] 
262 
and neg_mod_bound[simp] = neg_mod_conj [THEN conjunct2, standard] 

13183  263 

264 

13260  265 

15221  266 
subsection{*General Properties of div and mod*} 
13183  267 

15221  268 
lemma quorem_div_mod: "b \<noteq> 0 ==> quorem ((a, b), (a div b, a mod b))" 
13183  269 
apply (cut_tac a = a and b = b in zmod_zdiv_equality) 
13788  270 
apply (force simp add: quorem_def linorder_neq_iff) 
13183  271 
done 
272 

15221  273 
lemma quorem_div: "[ quorem((a,b),(q,r)); b \<noteq> 0 ] ==> a div b = q" 
13183  274 
by (simp add: quorem_div_mod [THEN unique_quotient]) 
275 

15221  276 
lemma quorem_mod: "[ quorem((a,b),(q,r)); b \<noteq> 0 ] ==> a mod b = r" 
13183  277 
by (simp add: quorem_div_mod [THEN unique_remainder]) 
278 

14288  279 
lemma div_pos_pos_trivial: "[ (0::int) \<le> a; a < b ] ==> a div b = 0" 
13183  280 
apply (rule quorem_div) 
281 
apply (auto simp add: quorem_def) 

282 
done 

283 

14288  284 
lemma div_neg_neg_trivial: "[ a \<le> (0::int); b < a ] ==> a div b = 0" 
13183  285 
apply (rule quorem_div) 
286 
apply (auto simp add: quorem_def) 

287 
done 

288 

14288  289 
lemma div_pos_neg_trivial: "[ (0::int) < a; a+b \<le> 0 ] ==> a div b = 1" 
13183  290 
apply (rule quorem_div) 
291 
apply (auto simp add: quorem_def) 

292 
done 

293 

294 
(*There is no div_neg_pos_trivial because 0 div b = 0 would supersede it*) 

295 

14288  296 
lemma mod_pos_pos_trivial: "[ (0::int) \<le> a; a < b ] ==> a mod b = a" 
13183  297 
apply (rule_tac q = 0 in quorem_mod) 
298 
apply (auto simp add: quorem_def) 

299 
done 

300 

14288  301 
lemma mod_neg_neg_trivial: "[ a \<le> (0::int); b < a ] ==> a mod b = a" 
13183  302 
apply (rule_tac q = 0 in quorem_mod) 
303 
apply (auto simp add: quorem_def) 

304 
done 

305 

14288  306 
lemma mod_pos_neg_trivial: "[ (0::int) < a; a+b \<le> 0 ] ==> a mod b = a+b" 
13183  307 
apply (rule_tac q = "1" in quorem_mod) 
308 
apply (auto simp add: quorem_def) 

309 
done 

310 

15221  311 
text{*There is no @{text mod_neg_pos_trivial}.*} 
13183  312 

313 

314 
(*Simpler laws such as a div b = (a div b) FAIL, but see just below*) 

315 
lemma zdiv_zminus_zminus [simp]: "(a) div (b) = a div (b::int)" 

15013  316 
apply (case_tac "b = 0", simp) 
13183  317 
apply (simp add: quorem_div_mod [THEN quorem_neg, simplified, 
318 
THEN quorem_div, THEN sym]) 

319 

320 
done 

321 

322 
(*Simpler laws such as a mod b = (a mod b) FAIL, but see just below*) 

323 
lemma zmod_zminus_zminus [simp]: "(a) mod (b) =  (a mod (b::int))" 

15013  324 
apply (case_tac "b = 0", simp) 
13183  325 
apply (subst quorem_div_mod [THEN quorem_neg, simplified, THEN quorem_mod], 
326 
auto) 

327 
done 

328 

15221  329 

330 
subsection{*Laws for div and mod with Unary Minus*} 

13183  331 

332 
lemma zminus1_lemma: 

333 
"quorem((a,b),(q,r)) 

334 
==> quorem ((a,b), (if r=0 then q else q  1), 

335 
(if r=0 then 0 else br))" 

14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

336 
by (force simp add: split_ifs quorem_def linorder_neq_iff right_diff_distrib) 
13183  337 

338 

339 
lemma zdiv_zminus1_eq_if: 

15221  340 
"b \<noteq> (0::int) 
13183  341 
==> (a) div b = 
342 
(if a mod b = 0 then  (a div b) else  (a div b)  1)" 

343 
by (blast intro: quorem_div_mod [THEN zminus1_lemma, THEN quorem_div]) 

344 

345 
lemma zmod_zminus1_eq_if: 

346 
"(a::int) mod b = (if a mod b = 0 then 0 else b  (a mod b))" 

15013  347 
apply (case_tac "b = 0", simp) 
13183  348 
apply (blast intro: quorem_div_mod [THEN zminus1_lemma, THEN quorem_mod]) 
349 
done 

350 

351 
lemma zdiv_zminus2: "a div (b) = (a::int) div b" 

352 
by (cut_tac a = "a" in zdiv_zminus_zminus, auto) 

353 

354 
lemma zmod_zminus2: "a mod (b) =  ((a::int) mod b)" 

355 
by (cut_tac a = "a" and b = b in zmod_zminus_zminus, auto) 

356 

357 
lemma zdiv_zminus2_eq_if: 

15221  358 
"b \<noteq> (0::int) 
13183  359 
==> a div (b) = 
360 
(if a mod b = 0 then  (a div b) else  (a div b)  1)" 

361 
by (simp add: zdiv_zminus1_eq_if zdiv_zminus2) 

362 

363 
lemma zmod_zminus2_eq_if: 

364 
"a mod (b::int) = (if a mod b = 0 then 0 else (a mod b)  b)" 

365 
by (simp add: zmod_zminus1_eq_if zmod_zminus2) 

366 

367 

14271  368 
subsection{*Division of a Number by Itself*} 
13183  369 

14288  370 
lemma self_quotient_aux1: "[ (0::int) < a; a = r + a*q; r < a ] ==> 1 \<le> q" 
13183  371 
apply (subgoal_tac "0 < a*q") 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

372 
apply (simp add: zero_less_mult_iff, arith) 
13183  373 
done 
374 

14288  375 
lemma self_quotient_aux2: "[ (0::int) < a; a = r + a*q; 0 \<le> r ] ==> q \<le> 1" 
376 
apply (subgoal_tac "0 \<le> a* (1q) ") 

14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

377 
apply (simp add: zero_le_mult_iff) 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

378 
apply (simp add: right_diff_distrib) 
13183  379 
done 
380 

15221  381 
lemma self_quotient: "[ quorem((a,a),(q,r)); a \<noteq> (0::int) ] ==> q = 1" 
13183  382 
apply (simp add: split_ifs quorem_def linorder_neq_iff) 
15221  383 
apply (rule order_antisym, safe, simp_all) 
13524  384 
apply (rule_tac [3] a = "a" and r = "r" in self_quotient_aux1) 
385 
apply (rule_tac a = "a" and r = "r" in self_quotient_aux2) 

15221  386 
apply (force intro: self_quotient_aux1 self_quotient_aux2 simp add: add_commute)+ 
13183  387 
done 
388 

15221  389 
lemma self_remainder: "[ quorem((a,a),(q,r)); a \<noteq> (0::int) ] ==> r = 0" 
13183  390 
apply (frule self_quotient, assumption) 
391 
apply (simp add: quorem_def) 

392 
done 

393 

15221  394 
lemma zdiv_self [simp]: "a \<noteq> 0 ==> a div a = (1::int)" 
13183  395 
by (simp add: quorem_div_mod [THEN self_quotient]) 
396 

397 
(*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *) 

398 
lemma zmod_self [simp]: "a mod a = (0::int)" 

15013  399 
apply (case_tac "a = 0", simp) 
13183  400 
apply (simp add: quorem_div_mod [THEN self_remainder]) 
401 
done 

402 

403 

14271  404 
subsection{*Computation of Division and Remainder*} 
13183  405 

406 
lemma zdiv_zero [simp]: "(0::int) div b = 0" 

407 
by (simp add: div_def divAlg_def) 

408 

409 
lemma div_eq_minus1: "(0::int) < b ==> 1 div b = 1" 

410 
by (simp add: div_def divAlg_def) 

411 

412 
lemma zmod_zero [simp]: "(0::int) mod b = 0" 

413 
by (simp add: mod_def divAlg_def) 

414 

415 
lemma zdiv_minus1: "(0::int) < b ==> 1 div b = 1" 

416 
by (simp add: div_def divAlg_def) 

417 

418 
lemma zmod_minus1: "(0::int) < b ==> 1 mod b = b  1" 

419 
by (simp add: mod_def divAlg_def) 

420 

15221  421 
text{*a positive, b positive *} 
13183  422 

14288  423 
lemma div_pos_pos: "[ 0 < a; 0 \<le> b ] ==> a div b = fst (posDivAlg(a,b))" 
13183  424 
by (simp add: div_def divAlg_def) 
425 

14288  426 
lemma mod_pos_pos: "[ 0 < a; 0 \<le> b ] ==> a mod b = snd (posDivAlg(a,b))" 
13183  427 
by (simp add: mod_def divAlg_def) 
428 

15221  429 
text{*a negative, b positive *} 
13183  430 

431 
lemma div_neg_pos: "[ a < 0; 0 < b ] ==> a div b = fst (negDivAlg(a,b))" 

432 
by (simp add: div_def divAlg_def) 

433 

434 
lemma mod_neg_pos: "[ a < 0; 0 < b ] ==> a mod b = snd (negDivAlg(a,b))" 

435 
by (simp add: mod_def divAlg_def) 

436 

15221  437 
text{*a positive, b negative *} 
13183  438 

439 
lemma div_pos_neg: 

440 
"[ 0 < a; b < 0 ] ==> a div b = fst (negateSnd(negDivAlg(a,b)))" 

441 
by (simp add: div_def divAlg_def) 

442 

443 
lemma mod_pos_neg: 

444 
"[ 0 < a; b < 0 ] ==> a mod b = snd (negateSnd(negDivAlg(a,b)))" 

445 
by (simp add: mod_def divAlg_def) 

446 

15221  447 
text{*a negative, b negative *} 
13183  448 

449 
lemma div_neg_neg: 

14288  450 
"[ a < 0; b \<le> 0 ] ==> a div b = fst (negateSnd(posDivAlg(a,b)))" 
13183  451 
by (simp add: div_def divAlg_def) 
452 

453 
lemma mod_neg_neg: 

14288  454 
"[ a < 0; b \<le> 0 ] ==> a mod b = snd (negateSnd(posDivAlg(a,b)))" 
13183  455 
by (simp add: mod_def divAlg_def) 
456 

457 
text {*Simplify expresions in which div and mod combine numerical constants*} 

458 

459 
declare div_pos_pos [of "number_of v" "number_of w", standard, simp] 

460 
declare div_neg_pos [of "number_of v" "number_of w", standard, simp] 

461 
declare div_pos_neg [of "number_of v" "number_of w", standard, simp] 

462 
declare div_neg_neg [of "number_of v" "number_of w", standard, simp] 

463 

464 
declare mod_pos_pos [of "number_of v" "number_of w", standard, simp] 

465 
declare mod_neg_pos [of "number_of v" "number_of w", standard, simp] 

466 
declare mod_pos_neg [of "number_of v" "number_of w", standard, simp] 

467 
declare mod_neg_neg [of "number_of v" "number_of w", standard, simp] 

468 

469 
declare posDivAlg_eqn [of "number_of v" "number_of w", standard, simp] 

470 
declare negDivAlg_eqn [of "number_of v" "number_of w", standard, simp] 

471 

472 

15221  473 
text{*Specialcase simplification *} 
13183  474 

475 
lemma zmod_1 [simp]: "a mod (1::int) = 0" 

476 
apply (cut_tac a = a and b = 1 in pos_mod_sign) 

13788  477 
apply (cut_tac [2] a = a and b = 1 in pos_mod_bound) 
478 
apply (auto simp del:pos_mod_bound pos_mod_sign) 

479 
done 

13183  480 

481 
lemma zdiv_1 [simp]: "a div (1::int) = a" 

482 
by (cut_tac a = a and b = 1 in zmod_zdiv_equality, auto) 

483 

484 
lemma zmod_minus1_right [simp]: "a mod (1::int) = 0" 

485 
apply (cut_tac a = a and b = "1" in neg_mod_sign) 

13788  486 
apply (cut_tac [2] a = a and b = "1" in neg_mod_bound) 
487 
apply (auto simp del: neg_mod_sign neg_mod_bound) 

13183  488 
done 
489 

490 
lemma zdiv_minus1_right [simp]: "a div (1::int) = a" 

491 
by (cut_tac a = a and b = "1" in zmod_zdiv_equality, auto) 

492 

493 
(** The last remaining special cases for constant arithmetic: 

494 
1 div z and 1 mod z **) 

495 

496 
declare div_pos_pos [OF int_0_less_1, of "number_of w", standard, simp] 

497 
declare div_pos_neg [OF int_0_less_1, of "number_of w", standard, simp] 

498 
declare mod_pos_pos [OF int_0_less_1, of "number_of w", standard, simp] 

499 
declare mod_pos_neg [OF int_0_less_1, of "number_of w", standard, simp] 

500 

501 
declare posDivAlg_eqn [of concl: 1 "number_of w", standard, simp] 

502 
declare negDivAlg_eqn [of concl: 1 "number_of w", standard, simp] 

503 

504 

14271  505 
subsection{*Monotonicity in the First Argument (Dividend)*} 
13183  506 

14288  507 
lemma zdiv_mono1: "[ a \<le> a'; 0 < (b::int) ] ==> a div b \<le> a' div b" 
13183  508 
apply (cut_tac a = a and b = b in zmod_zdiv_equality) 
509 
apply (cut_tac a = a' and b = b in zmod_zdiv_equality) 

510 
apply (rule unique_quotient_lemma) 

511 
apply (erule subst) 

15221  512 
apply (erule subst, simp_all) 
13183  513 
done 
514 

14288  515 
lemma zdiv_mono1_neg: "[ a \<le> a'; (b::int) < 0 ] ==> a' div b \<le> a div b" 
13183  516 
apply (cut_tac a = a and b = b in zmod_zdiv_equality) 
517 
apply (cut_tac a = a' and b = b in zmod_zdiv_equality) 

518 
apply (rule unique_quotient_lemma_neg) 

519 
apply (erule subst) 

15221  520 
apply (erule subst, simp_all) 
13183  521 
done 
6917  522 

523 

14271  524 
subsection{*Monotonicity in the Second Argument (Divisor)*} 
13183  525 

526 
lemma q_pos_lemma: 

14288  527 
"[ 0 \<le> b'*q' + r'; r' < b'; 0 < b' ] ==> 0 \<le> (q'::int)" 
13183  528 
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

529 
apply (simp add: zero_less_mult_iff) 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

530 
apply (simp add: right_distrib) 
13183  531 
done 
532 

533 
lemma zdiv_mono2_lemma: 

14288  534 
"[ b*q + r = b'*q' + r'; 0 \<le> b'*q' + r'; 
535 
r' < b'; 0 \<le> r; 0 < b'; b' \<le> b ] 

536 
==> q \<le> (q'::int)" 

13183  537 
apply (frule q_pos_lemma, assumption+) 
538 
apply (subgoal_tac "b*q < b* (q' + 1) ") 

14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

539 
apply (simp add: mult_less_cancel_left) 
13183  540 
apply (subgoal_tac "b*q = r'  r + b'*q'") 
541 
prefer 2 apply simp 

14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

542 
apply (simp (no_asm_simp) add: right_distrib) 
15221  543 
apply (subst add_commute, rule zadd_zless_mono, arith) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14353
diff
changeset

544 
apply (rule mult_right_mono, auto) 
13183  545 
done 
546 

547 
lemma zdiv_mono2: 

14288  548 
"[ (0::int) \<le> a; 0 < b'; b' \<le> b ] ==> a div b \<le> a div b'" 
15221  549 
apply (subgoal_tac "b \<noteq> 0") 
13183  550 
prefer 2 apply arith 
551 
apply (cut_tac a = a and b = b in zmod_zdiv_equality) 

552 
apply (cut_tac a = a and b = b' in zmod_zdiv_equality) 

553 
apply (rule zdiv_mono2_lemma) 

554 
apply (erule subst) 

15221  555 
apply (erule subst, simp_all) 
13183  556 
done 
557 

558 
lemma q_neg_lemma: 

14288  559 
"[ b'*q' + r' < 0; 0 \<le> r'; 0 < b' ] ==> q' \<le> (0::int)" 
13183  560 
apply (subgoal_tac "b'*q' < 0") 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

561 
apply (simp add: mult_less_0_iff, arith) 
13183  562 
done 
563 

564 
lemma zdiv_mono2_neg_lemma: 

565 
"[ b*q + r = b'*q' + r'; b'*q' + r' < 0; 

14288  566 
r < b; 0 \<le> r'; 0 < b'; b' \<le> b ] 
567 
==> q' \<le> (q::int)" 

13183  568 
apply (frule q_neg_lemma, assumption+) 
569 
apply (subgoal_tac "b*q' < b* (q + 1) ") 

14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

570 
apply (simp add: mult_less_cancel_left) 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

571 
apply (simp add: right_distrib) 
14288  572 
apply (subgoal_tac "b*q' \<le> b'*q'") 
15221  573 
prefer 2 apply (simp add: mult_right_mono_neg, arith) 
13183  574 
done 
575 

576 
lemma zdiv_mono2_neg: 

14288  577 
"[ a < (0::int); 0 < b'; b' \<le> b ] ==> a div b' \<le> a div b" 
13183  578 
apply (cut_tac a = a and b = b in zmod_zdiv_equality) 
579 
apply (cut_tac a = a and b = b' in zmod_zdiv_equality) 

580 
apply (rule zdiv_mono2_neg_lemma) 

581 
apply (erule subst) 

15221  582 
apply (erule subst, simp_all) 
13183  583 
done 
584 

585 

14271  586 
subsection{*More Algebraic Laws for div and mod*} 
13183  587 

15221  588 
text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *} 
13183  589 

590 
lemma zmult1_lemma: 

15221  591 
"[ quorem((b,c),(q,r)); c \<noteq> 0 ] 
13183  592 
==> 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

593 
by (force simp add: split_ifs quorem_def linorder_neq_iff right_distrib) 
13183  594 

595 
lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)" 

15013  596 
apply (case_tac "c = 0", simp) 
13183  597 
apply (blast intro: quorem_div_mod [THEN zmult1_lemma, THEN quorem_div]) 
598 
done 

599 

600 
lemma zmod_zmult1_eq: "(a*b) mod c = a*(b mod c) mod (c::int)" 

15013  601 
apply (case_tac "c = 0", simp) 
13183  602 
apply (blast intro: quorem_div_mod [THEN zmult1_lemma, THEN quorem_mod]) 
603 
done 

604 

605 
lemma zmod_zmult1_eq': "(a*b) mod (c::int) = ((a mod c) * b) mod c" 

606 
apply (rule trans) 

607 
apply (rule_tac s = "b*a mod c" in trans) 

608 
apply (rule_tac [2] zmod_zmult1_eq) 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15221
diff
changeset

609 
apply (simp_all add: mult_commute) 
13183  610 
done 
611 

612 
lemma zmod_zmult_distrib: "(a*b) mod (c::int) = ((a mod c) * (b mod c)) mod c" 

613 
apply (rule zmod_zmult1_eq' [THEN trans]) 

614 
apply (rule zmod_zmult1_eq) 

615 
done 

616 

15221  617 
lemma zdiv_zmult_self1 [simp]: "b \<noteq> (0::int) ==> (a*b) div b = a" 
13183  618 
by (simp add: zdiv_zmult1_eq) 
619 

15221  620 
lemma zdiv_zmult_self2 [simp]: "b \<noteq> (0::int) ==> (b*a) div b = a" 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15221
diff
changeset

621 
by (subst mult_commute, erule zdiv_zmult_self1) 
13183  622 

623 
lemma zmod_zmult_self1 [simp]: "(a*b) mod b = (0::int)" 

624 
by (simp add: zmod_zmult1_eq) 

625 

626 
lemma zmod_zmult_self2 [simp]: "(b*a) mod b = (0::int)" 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15221
diff
changeset

627 
by (simp add: mult_commute zmod_zmult1_eq) 
13183  628 

629 
lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)" 

13517  630 
proof 
631 
assume "m mod d = 0" 

14473  632 
with zmod_zdiv_equality[of m d] show "EX q::int. m = d*q" by auto 
13517  633 
next 
634 
assume "EX q::int. m = d*q" 

635 
thus "m mod d = 0" by auto 

636 
qed 

13183  637 

638 
declare zmod_eq_0_iff [THEN iffD1, dest!] 

639 

15221  640 
text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *} 
13183  641 

642 
lemma zadd1_lemma: 

15221  643 
"[ quorem((a,c),(aq,ar)); quorem((b,c),(bq,br)); c \<noteq> 0 ] 
13183  644 
==> 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

645 
by (force simp add: split_ifs quorem_def linorder_neq_iff right_distrib) 
13183  646 

647 
(*NOT suitable for rewriting: the RHS has an instance of the LHS*) 

648 
lemma zdiv_zadd1_eq: 

649 
"(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)" 

15013  650 
apply (case_tac "c = 0", simp) 
13183  651 
apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_div) 
652 
done 

653 

654 
lemma zmod_zadd1_eq: "(a+b) mod (c::int) = (a mod c + b mod c) mod c" 

15013  655 
apply (case_tac "c = 0", simp) 
13183  656 
apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_mod) 
657 
done 

658 

659 
lemma mod_div_trivial [simp]: "(a mod b) div b = (0::int)" 

15013  660 
apply (case_tac "b = 0", simp) 
13788  661 
apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial) 
13183  662 
done 
663 

664 
lemma mod_mod_trivial [simp]: "(a mod b) mod b = a mod (b::int)" 

15013  665 
apply (case_tac "b = 0", simp) 
13788  666 
apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial) 
13183  667 
done 
668 

669 
lemma zmod_zadd_left_eq: "(a+b) mod (c::int) = ((a mod c) + b) mod c" 

670 
apply (rule trans [symmetric]) 

671 
apply (rule zmod_zadd1_eq, simp) 

672 
apply (rule zmod_zadd1_eq [symmetric]) 

673 
done 

674 

675 
lemma zmod_zadd_right_eq: "(a+b) mod (c::int) = (a + (b mod c)) mod c" 

676 
apply (rule trans [symmetric]) 

677 
apply (rule zmod_zadd1_eq, simp) 

678 
apply (rule zmod_zadd1_eq [symmetric]) 

679 
done 

680 

15221  681 
lemma zdiv_zadd_self1[simp]: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1" 
13183  682 
by (simp add: zdiv_zadd1_eq) 
683 

15221  684 
lemma zdiv_zadd_self2[simp]: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1" 
13183  685 
by (simp add: zdiv_zadd1_eq) 
686 

687 
lemma zmod_zadd_self1[simp]: "(a+b) 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 
lemma zmod_zadd_self2[simp]: "(b+a) mod a = b mod (a::int)" 

15013  693 
apply (case_tac "a = 0", simp) 
13183  694 
apply (simp add: zmod_zadd1_eq) 
695 
done 

696 

697 

14271  698 
subsection{*Proving @{term "a div (b*c) = (a div b) div c"} *} 
13183  699 

700 
(*The condition c>0 seems necessary. Consider that 7 div ~6 = ~2 but 

701 
7 div 2 div ~3 = 3 div ~3 = ~1. The subcase (a div b) mod c = 0 seems 

702 
to cause particular problems.*) 

703 

15221  704 
text{*first, four lemmas to bound the remainder for the cases b<0 and b>0 *} 
13183  705 

14288  706 
lemma zmult2_lemma_aux1: "[ (0::int) < c; b < r; r \<le> 0 ] ==> b*c < b*(q mod c) + r" 
13183  707 
apply (subgoal_tac "b * (c  q mod c) < r * 1") 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

708 
apply (simp add: right_diff_distrib) 
13183  709 
apply (rule order_le_less_trans) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14353
diff
changeset

710 
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

711 
apply (rule mult_left_mono_neg) 
15221  712 
apply (auto simp add: compare_rls add_commute [of 1] 
13183  713 
add1_zle_eq pos_mod_bound) 
714 
done 

715 

15221  716 
lemma zmult2_lemma_aux2: 
717 
"[ (0::int) < c; b < r; r \<le> 0 ] ==> b * (q mod c) + r \<le> 0" 

14288  718 
apply (subgoal_tac "b * (q mod c) \<le> 0") 
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: mult_le_0_iff) 
13183  721 
done 
722 

14288  723 
lemma zmult2_lemma_aux3: "[ (0::int) < c; 0 \<le> r; r < b ] ==> 0 \<le> b * (q mod c) + r" 
724 
apply (subgoal_tac "0 \<le> b * (q mod c) ") 

13183  725 
apply arith 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

726 
apply (simp add: zero_le_mult_iff) 
13183  727 
done 
728 

14288  729 
lemma zmult2_lemma_aux4: "[ (0::int) < c; 0 \<le> r; r < b ] ==> b * (q mod c) + r < b * c" 
13183  730 
apply (subgoal_tac "r * 1 < b * (c  q mod c) ") 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

731 
apply (simp add: right_diff_distrib) 
13183  732 
apply (rule order_less_le_trans) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14353
diff
changeset

733 
apply (erule mult_strict_right_mono) 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

734 
apply (rule_tac [2] mult_left_mono) 
15221  735 
apply (auto simp add: compare_rls add_commute [of 1] 
13183  736 
add1_zle_eq pos_mod_bound) 
737 
done 

738 

15221  739 
lemma zmult2_lemma: "[ quorem ((a,b), (q,r)); b \<noteq> 0; 0 < c ] 
13183  740 
==> quorem ((a, b*c), (q div c, b*(q mod c) + r))" 
14271  741 
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

742 
zero_less_mult_iff right_distrib [symmetric] 
13524  743 
zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4) 
13183  744 

745 
lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c" 

15013  746 
apply (case_tac "b = 0", simp) 
13183  747 
apply (force simp add: quorem_div_mod [THEN zmult2_lemma, THEN quorem_div]) 
748 
done 

749 

750 
lemma zmod_zmult2_eq: 

751 
"(0::int) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b" 

15013  752 
apply (case_tac "b = 0", simp) 
13183  753 
apply (force simp add: quorem_div_mod [THEN zmult2_lemma, THEN quorem_mod]) 
754 
done 

755 

756 

14271  757 
subsection{*Cancellation of Common Factors in div*} 
13183  758 

15221  759 
lemma zdiv_zmult_zmult1_aux1: 
760 
"[ (0::int) < b; c \<noteq> 0 ] ==> (c*a) div (c*b) = a div b" 

13183  761 
by (subst zdiv_zmult2_eq, auto) 
762 

15221  763 
lemma zdiv_zmult_zmult1_aux2: 
764 
"[ b < (0::int); c \<noteq> 0 ] ==> (c*a) div (c*b) = a div b" 

13183  765 
apply (subgoal_tac " (c * (a)) div (c * (b)) = (a) div (b) ") 
13524  766 
apply (rule_tac [2] zdiv_zmult_zmult1_aux1, auto) 
13183  767 
done 
768 

15221  769 
lemma zdiv_zmult_zmult1: "c \<noteq> (0::int) ==> (c*a) div (c*b) = a div b" 
15013  770 
apply (case_tac "b = 0", simp) 
13524  771 
apply (auto simp add: linorder_neq_iff zdiv_zmult_zmult1_aux1 zdiv_zmult_zmult1_aux2) 
13183  772 
done 
773 

15221  774 
lemma zdiv_zmult_zmult2: "c \<noteq> (0::int) ==> (a*c) div (b*c) = a div b" 
13183  775 
apply (drule zdiv_zmult_zmult1) 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15221
diff
changeset

776 
apply (auto simp add: mult_commute) 
13183  777 
done 
778 

779 

780 

14271  781 
subsection{*Distribution of Factors over mod*} 
13183  782 

15221  783 
lemma zmod_zmult_zmult1_aux1: 
784 
"[ (0::int) < b; c \<noteq> 0 ] ==> (c*a) mod (c*b) = c * (a mod b)" 

13183  785 
by (subst zmod_zmult2_eq, auto) 
786 

15221  787 
lemma zmod_zmult_zmult1_aux2: 
788 
"[ b < (0::int); c \<noteq> 0 ] ==> (c*a) mod (c*b) = c * (a mod b)" 

13183  789 
apply (subgoal_tac " (c * (a)) mod (c * (b)) = c * ((a) mod (b))") 
13524  790 
apply (rule_tac [2] zmod_zmult_zmult1_aux1, auto) 
13183  791 
done 
792 

793 
lemma zmod_zmult_zmult1: "(c*a) mod (c*b) = (c::int) * (a mod b)" 

15013  794 
apply (case_tac "b = 0", simp) 
795 
apply (case_tac "c = 0", simp) 

13524  796 
apply (auto simp add: linorder_neq_iff zmod_zmult_zmult1_aux1 zmod_zmult_zmult1_aux2) 
13183  797 
done 
798 

799 
lemma zmod_zmult_zmult2: "(a*c) mod (b*c) = (a mod b) * (c::int)" 

800 
apply (cut_tac c = c in zmod_zmult_zmult1) 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15221
diff
changeset

801 
apply (auto simp add: mult_commute) 
13183  802 
done 
803 

804 

14271  805 
subsection {*Splitting Rules for div and mod*} 
13260  806 

807 
text{*The proofs of the two lemmas below are essentially identical*} 

808 

809 
lemma split_pos_lemma: 

810 
"0<k ==> 

14288  811 
P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j > P i j)" 
15221  812 
apply (rule iffI, clarify) 
13260  813 
apply (erule_tac P="P ?x ?y" in rev_mp) 
814 
apply (subst zmod_zadd1_eq) 

815 
apply (subst zdiv_zadd1_eq) 

816 
apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial) 

817 
txt{*converse direction*} 

818 
apply (drule_tac x = "n div k" in spec) 

15221  819 
apply (drule_tac x = "n mod k" in spec, simp) 
13260  820 
done 
821 

822 
lemma split_neg_lemma: 

823 
"k<0 ==> 

14288  824 
P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j > P i j)" 
15221  825 
apply (rule iffI, clarify) 
13260  826 
apply (erule_tac P="P ?x ?y" in rev_mp) 
827 
apply (subst zmod_zadd1_eq) 

828 
apply (subst zdiv_zadd1_eq) 

829 
apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial) 

830 
txt{*converse direction*} 

831 
apply (drule_tac x = "n div k" in spec) 

15221  832 
apply (drule_tac x = "n mod k" in spec, simp) 
13260  833 
done 
834 

835 
lemma split_zdiv: 

836 
"P(n div k :: int) = 

837 
((k = 0 > P 0) & 

14288  838 
(0<k > (\<forall>i j. 0\<le>j & j<k & n = k*i + j > P i)) & 
839 
(k<0 > (\<forall>i j. k<j & j\<le>0 & n = k*i + j > P i)))" 

15221  840 
apply (case_tac "k=0", simp) 
13260  841 
apply (simp only: linorder_neq_iff) 
842 
apply (erule disjE) 

843 
apply (simp_all add: split_pos_lemma [of concl: "%x y. P x"] 

844 
split_neg_lemma [of concl: "%x y. P x"]) 

845 
done 

846 

847 
lemma split_zmod: 

848 
"P(n mod k :: int) = 

849 
((k = 0 > P n) & 

14288  850 
(0<k > (\<forall>i j. 0\<le>j & j<k & n = k*i + j > P j)) & 
851 
(k<0 > (\<forall>i j. k<j & j\<le>0 & n = k*i + j > P j)))" 

15221  852 
apply (case_tac "k=0", simp) 
13260  853 
apply (simp only: linorder_neq_iff) 
854 
apply (erule disjE) 

855 
apply (simp_all add: split_pos_lemma [of concl: "%x y. P y"] 

856 
split_neg_lemma [of concl: "%x y. P y"]) 

857 
done 

858 

859 
(* 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

860 
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

861 
declare split_zmod [of _ _ "number_of k", simplified, standard, arith_split] 
13260  862 

863 

14271  864 
subsection{*Speeding up the Division Algorithm with Shifting*} 
13183  865 

15221  866 
text{*computing div by shifting *} 
13183  867 

14288  868 
lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a" 
869 
proof cases 

870 
assume "a=0" 

871 
thus ?thesis by simp 

872 
next 

873 
assume "a\<noteq>0" and le_a: "0\<le>a" 

874 
hence a_pos: "1 \<le> a" by arith 

875 
hence one_less_a2: "1 < 2*a" by arith 

876 
hence le_2a: "2 * (1 + b mod a) \<le> 2 * a" 

15221  877 
by (simp add: mult_le_cancel_left add_commute [of 1] add1_zle_eq) 
14288  878 
with a_pos have "0 \<le> b mod a" by simp 
879 
hence le_addm: "0 \<le> 1 mod (2*a) + 2*(b mod a)" 

880 
by (simp add: mod_pos_pos_trivial one_less_a2) 

881 
with le_2a 

882 
have "(1 mod (2*a) + 2*(b mod a)) div (2*a) = 0" 

883 
by (simp add: div_pos_pos_trivial le_addm mod_pos_pos_trivial one_less_a2 

884 
right_distrib) 

885 
thus ?thesis 

886 
by (subst zdiv_zadd1_eq, 

887 
simp add: zdiv_zmult_zmult1 zmod_zmult_zmult1 one_less_a2 

888 
div_pos_pos_trivial) 

889 
qed 

13183  890 

14288  891 
lemma neg_zdiv_mult_2: "a \<le> (0::int) ==> (1 + 2*b) div (2*a) = (b+1) div a" 
13183  892 
apply (subgoal_tac " (1 + 2* (b  1)) div (2 * (a)) = (b  1) div (a) ") 
893 
apply (rule_tac [2] pos_zdiv_mult_2) 

14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

894 
apply (auto simp add: minus_mult_right [symmetric] right_diff_distrib) 
13183  895 
apply (subgoal_tac " (1  (2 * b)) =  (1 + (2 * b))") 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

896 
apply (simp only: zdiv_zminus_zminus diff_minus minus_add_distrib [symmetric], 
13183  897 
simp) 
898 
done 

899 

900 

901 
(*Not clear why this must be proved separately; probably number_of causes 

902 
simplification problems*) 

14288  903 
lemma not_0_le_lemma: "~ 0 \<le> x ==> x \<le> (0::int)" 
13183  904 
by auto 
905 

906 
lemma zdiv_number_of_BIT[simp]: 

907 
"number_of (v BIT b) div number_of (w BIT False) = 

14288  908 
(if ~b  (0::int) \<le> number_of w 
13183  909 
then number_of v div (number_of w) 
910 
else (number_of v + (1::int)) div (number_of w))" 

15013  911 
apply (simp only: number_of_eq Bin_simps UNIV_I split: split_if) 
912 
apply (simp add: zdiv_zmult_zmult1 pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac) 

13183  913 
done 
914 

915 

15013  916 
subsection{*Computing mod by Shifting (proofs resemble those for div)*} 
13183  917 

918 
lemma pos_zmod_mult_2: 

14288  919 
"(0::int) \<le> a ==> (1 + 2*b) mod (2*a) = 1 + 2 * (b mod a)" 
15013  920 
apply (case_tac "a = 0", simp) 
13183  921 
apply (subgoal_tac "1 < a * 2") 
922 
prefer 2 apply arith 

14288  923 
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

924 
apply (rule_tac [2] mult_left_mono) 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15221
diff
changeset

925 
apply (auto simp add: add_commute [of 1] mult_commute add1_zle_eq 
13183  926 
pos_mod_bound) 
927 
apply (subst zmod_zadd1_eq) 

928 
apply (simp add: zmod_zmult_zmult2 mod_pos_pos_trivial) 

929 
apply (rule mod_pos_pos_trivial) 

14288  930 
apply (auto simp add: mod_pos_pos_trivial left_distrib) 
15221  931 
apply (subgoal_tac "0 \<le> b mod a", arith, simp) 
13183  932 
done 
933 

934 
lemma neg_zmod_mult_2: 

14288  935 
"a \<le> (0::int) ==> (1 + 2*b) mod (2*a) = 2 * ((b+1) mod a)  1" 
13183  936 
apply (subgoal_tac "(1 + 2* (b  1)) mod (2* (a)) = 
937 
1 + 2* ((b  1) mod (a))") 

938 
apply (rule_tac [2] pos_zmod_mult_2) 

14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

939 
apply (auto simp add: minus_mult_right [symmetric] right_diff_distrib) 
13183  940 
apply (subgoal_tac " (1  (2 * b)) =  (1 + (2 * b))") 
941 
prefer 2 apply simp 

14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

942 
apply (simp only: zmod_zminus_zminus diff_minus minus_add_distrib [symmetric]) 
13183  943 
done 
944 

945 
lemma zmod_number_of_BIT [simp]: 

946 
"number_of (v BIT b) mod number_of (w BIT False) = 

947 
(if b then 

14288  948 
if (0::int) \<le> number_of w 
13183  949 
then 2 * (number_of v mod number_of w) + 1 
950 
else 2 * ((number_of v + (1::int)) mod number_of w)  1 

951 
else 2 * (number_of v mod number_of w))" 

15013  952 
apply (simp only: number_of_eq Bin_simps UNIV_I split: split_if) 
953 
apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2 

954 
not_0_le_lemma neg_zmod_mult_2 add_ac) 

13183  955 
done 
956 

957 

958 

15013  959 
subsection{*Quotients of Signs*} 
13183  960 

961 
lemma div_neg_pos_less0: "[ a < (0::int); 0 < b ] ==> a div b < 0" 

14288  962 
apply (subgoal_tac "a div b \<le> 1", force) 
13183  963 
apply (rule order_trans) 
964 
apply (rule_tac a' = "1" in zdiv_mono1) 

965 
apply (auto simp add: zdiv_minus1) 

966 
done 

967 

14288  968 
lemma div_nonneg_neg_le0: "[ (0::int) \<le> a; b < 0 ] ==> a div b \<le> 0" 
13183  969 
by (drule zdiv_mono1_neg, auto) 
970 

14288  971 
lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \<le> a div b) = (0 \<le> a)" 
13183  972 
apply auto 
973 
apply (drule_tac [2] zdiv_mono1) 

974 
apply (auto simp add: linorder_neq_iff) 

975 
apply (simp (no_asm_use) add: linorder_not_less [symmetric]) 

976 
apply (blast intro: div_neg_pos_less0) 

977 
done 

978 

979 
lemma neg_imp_zdiv_nonneg_iff: 

14288  980 
"b < (0::int) ==> (0 \<le> a div b) = (a \<le> (0::int))" 
13183  981 
apply (subst zdiv_zminus_zminus [symmetric]) 
982 
apply (subst pos_imp_zdiv_nonneg_iff, auto) 

983 
done 

984 

14288  985 
(*But not (a div b \<le> 0 iff a\<le>0); consider a=1, b=2 when a div b = 0.*) 
13183  986 
lemma pos_imp_zdiv_neg_iff: "(0::int) < b ==> (a div b < 0) = (a < 0)" 
987 
by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff) 

988 

14288  989 
(*Again the law fails for \<le>: consider a = 1, b = 2 when a div b = 0*) 
13183  990 
lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)" 
991 
by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff) 

992 

13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

993 

14271  994 
subsection {* The Divides Relation *} 
13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

995 

8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

996 
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

997 
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

998 

8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

999 
lemma zdvd_0_right [iff]: "(m::int) dvd 0" 
15221  1000 
by (simp add: dvd_def) 
13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1001 

8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1002 
lemma zdvd_0_left [iff]: "(0 dvd (m::int)) = (m = 0)" 
15221  1003 
by (simp add: dvd_def) 
13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1004 

8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1005 
lemma zdvd_1_left [iff]: "1 dvd (m::int)" 
15221  1006 
by (simp add: dvd_def) 
13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1007 

8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1008 
lemma zdvd_refl [simp]: "m dvd (m::int)" 
15221  1009 
by (auto simp add: dvd_def intro: zmult_1_right [symmetric]) 
13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1010 

8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1011 
lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)" 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15221
diff
changeset

1012 
by (auto simp add: dvd_def intro: mult_assoc) 
13837
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_zminus_iff: "(m dvd n) = (m dvd (n::int))" 
15221  1015 
apply (simp add: dvd_def, auto) 
13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1016 
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

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_zminus2_iff: "(m dvd n) = (m dvd (n::int))" 
15221  1020 
apply (simp add: dvd_def, auto) 
13837
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_anti_sym: 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1025 
"0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)" 
15221  1026 
apply (simp add: dvd_def, auto) 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15221
diff
changeset

1027 
apply (simp add: mult_assoc 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

1028 
done 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1029 

8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1030 
lemma zdvd_zadd: "k dvd m ==> k dvd n ==> k dvd (m + n :: int)" 
15221  1031 
apply (simp add: dvd_def) 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

1032 
apply (blast intro: right_distrib [symmetric]) 
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_zdiff: "k dvd m ==> k dvd n ==> k dvd (m  n :: int)" 
15221  1036 
apply (simp add: dvd_def) 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

1037 
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

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_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

1041 
apply (subgoal_tac "m = n + (m  n)") 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1042 
apply (erule ssubst) 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1043 
apply (blast intro: zdvd_zadd, simp) 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1044 
done 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1045 

8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1046 
lemma zdvd_zmult: "k dvd (n::int) ==> k dvd m * n" 
15221  1047 
apply (simp add: dvd_def) 
14271  1048 
apply (blast intro: mult_left_commute) 
13837
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_zmult2: "k dvd (m::int) ==> k dvd m * n" 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15221
diff
changeset

1052 
apply (subst mult_commute) 
13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1053 
apply (erule zdvd_zmult) 
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 [iff]: "(k::int) dvd m * k" 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1057 
apply (rule zdvd_zmult) 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1058 
apply (rule zdvd_refl) 
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 k * m" 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1062 
apply (rule zdvd_zmult2) 
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 zdvd_zmultD2: "j * k dvd n ==> j dvd (n::int)" 
15221  1067 
apply (simp add: dvd_def) 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15221
diff
changeset

1068 
apply (simp add: mult_assoc, blast) 
13837
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_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

1072 
apply (rule zdvd_zmultD2) 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15221
diff
changeset

1073 
apply (subst mult_commute, assumption) 
13837
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_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n" 
15221  1077 
apply (simp add: dvd_def, clarify) 
13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1078 
apply (rule_tac x = "k * ka" in exI) 
14271  1079 
apply (simp add: mult_ac) 
13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1080 
done 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1081 

8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1082 
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

1083 
apply (rule iffI) 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1084 
apply (erule_tac [2] zdvd_zadd) 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1085 
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

1086 
apply (erule ssubst) 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1087 
apply (erule zdvd_zdiff, simp_all) 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1088 
done 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1089 

8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1090 
lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n" 
15221  1091 
apply (simp add: dvd_def) 
13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1092 
apply (auto simp add: zmod_zmult_zmult1) 
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_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

1096 
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

1097 
apply (simp add: zmod_zdiv_equality [symmetric]) 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1098 
apply (simp only: zdvd_zadd zdvd_zmult2) 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1099 
done 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1100 

8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1101 
lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)" 
15221  1102 
apply (simp add: dvd_def, auto) 
13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1103 
apply (subgoal_tac "0 < n") 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1104 
prefer 2 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14353
diff
changeset

1105 
apply (blast intro: order_less_trans) 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1106 
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

1107 
apply (subgoal_tac "n * k < n * 1") 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

1108 
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

1109 
done 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1110 

8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1111 
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

1112 
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

1113 
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

1114 
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

1115 
apply (auto simp add: zmult_int [symmetric]) 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1116 
done 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1117 

8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1118 
lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)" 
15003  1119 
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

1120 
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

1121 
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

1122 
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

1123 
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

1124 
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

1125 
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

1126 
nat_mult_distrib [symmetric] nat_eq_iff2) 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1127 
done 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1128 

8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1129 
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

1130 
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

1131 
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

1132 
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

1133 
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

1134 
nat_mult_distrib [symmetric] nat_eq_iff2) 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1135 
done 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1136 

8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1137 
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

1138 
apply (auto simp add: dvd_def) 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1139 
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

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 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

1143 
apply (auto simp add: dvd_def) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14353
diff
changeset

1144 
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

1145 
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

1146 
done 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1147 

14288  1148 
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

1149 
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

1150 
apply (auto simp add: dvd_int_iff) 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1151 
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

1152 
apply (auto simp add: dvd_imp_le) 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1153 
done 
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1154 

8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13788
diff
changeset

1155 

14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1156 
subsection{*Integer Powers*} 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1157 

79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1158 
instance int :: power .. 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1159 

79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1160 
primrec 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1161 
"p ^ 0 = 1" 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1162 
"p ^ (Suc n) = (p::int) * (p ^ n)" 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1163 

79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1164 

15003  1165 
instance int :: recpower 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1166 
proof 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1167 
fix z :: int 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1168 
fix n :: nat 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1169 
show "z^0 = 1" by simp 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1170 
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

1171 
qed 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1172 

79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1173 

79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1174 
lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m" 
15251  1175 
apply (induct "y", auto) 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1176 
apply (rule zmod_zmult1_eq [THEN trans]) 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1177 
apply (simp (no_asm_simp)) 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1178 
apply (rule zmod_zmult_distrib [symmetric]) 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1179 
done 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1180 

79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1181 
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

1182 
by (rule Power.power_add) 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1183 

79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1184 
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

1185 
by (rule Power.power_mult [symmetric]) 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1186 

79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1187 
lemma zero_less_zpower_abs_iff [simp]: 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1188 
"(0 < (abs x)^n) = (x \<noteq> (0::int)  n=0)" 
15251  1189 
apply (induct "n") 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1190 
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

1191 
done 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1192 

79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1193 
lemma zero_le_zpower_abs [simp]: "(0::int) <= (abs x)^n" 
15251  1194 
apply (induct "n") 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1195 
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

1196 
done 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1197 

15320  1198 
theorem zpower_int: "(int m)^n = int (m^n)" 
1199 
by (induct n) (simp_all add: zmult_int) 

1200 

15101  1201 
lemma zdiv_int: "int (a div b) = (int a) div (int b)" 
1202 
apply (subst split_div, auto) 

1203 
apply (subst split_zdiv, auto) 

1204 
apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in IntDiv.unique_quotient) 

1205 
apply (auto simp add: IntDiv.quorem_def int_eq_of_nat) 

1206 
done 

1207 

1208 
lemma zmod_int: "int (a mod b) = (int a) mod (int b)" 

1209 
apply (subst split_mod, auto) 

1210 
apply (subst split_zmod, auto) 

1211 
apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia in IntDiv.unique_remainder) 

1212 
apply (auto simp add: IntDiv.quorem_def int_eq_of_nat) 

1213 
done 

14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

1214 

13183  1215 
ML 
1216 
{* 

1217 
val quorem_def = thm "quorem_def"; 

1218 

1219 
val unique_quotient = thm "unique_quotient"; 

1220 
val unique_remainder = thm "unique_remainder"; 

1221 
val adjust_eq = thm "adjust_eq"; 

1222 
val posDivAlg_eqn = thm "posDivAlg_eqn"; 

1223 
val posDivAlg_correct = thm "posDivAlg_correct"; 

1224 
val negDivAlg_eqn = thm "negDivAlg_eqn"; 

1225 
val negDivAlg_correct = thm "negDivAlg_correct"; 

1226 
val quorem_0 = thm "quorem_0"; 

1227 
val posDivAlg_0 = thm "posDivAlg_0"; 

1228 
val negDivAlg_minus1 = thm "negDivAlg_minus1"; 

1229 
val negateSnd_eq = thm "negateSnd_eq"; 

1230 
val quorem_neg = thm "quorem_neg"; 

1231 
val divAlg_correct = thm "divAlg_correct"; 

1232 
val DIVISION_BY_ZERO = thm "DIVISION_BY_ZERO"; 

1233 
val zmod_zdiv_equality = thm "zmod_zdiv_equality"; 

1234 
val pos_mod_conj = thm "pos_mod_conj"; 

1235 
val pos_mod_sign = thm "pos_mod_sign"; 

1236 
val neg_mod_conj = thm "neg_mod_conj"; 

1237 
val neg_mod_sign = thm "neg_mod_sign"; 

1238 
val quorem_div_mod = thm "quorem_div_mod"; 

1239 
val quorem_div = thm "quorem_div"; 

1240 
val quorem_mod = thm "quorem_mod"; 

1241 
val div_pos_pos_trivial = thm "div_pos_pos_trivial"; 

1242 
val div_neg_neg_trivial = thm "div_neg_neg_trivial"; 

1243 
val div_pos_neg_trivial = thm "div_pos_neg_trivial"; 

1244 
val mod_pos_pos_trivial = thm "mod_pos_pos_trivial"; 

1245 
val mod_neg_neg_trivial = thm "mod_neg_neg_trivial"; 

1246 
val mod_pos_neg_trivial = thm "mod_pos_neg_trivial"; 

1247 
val zdiv_zminus_zminus = thm "zdiv_zminus_zminus"; 

1248 
val zmod_zminus_zminus = thm "zmod_zminus_zminus"; 

1249 
val zdiv_zminus1_eq_if = thm "zdiv_zminus1_eq_if"; 

1250 
val zmod_zminus1_eq_if = thm "zmod_zminus1_eq_if"; 

1251 
val zdiv_zminus2 = thm "zdiv_zminus2"; 

1252 
val zmod_zminus2 = thm "zmod_zminus2"; 

1253 
val zdiv_zminus2_eq_if = thm "zdiv_zminus2_eq_if"; 

1254 
val zmod_zminus2_eq_if = thm "zmod_zminus2_eq_if"; 

1255 
val self_quotient = thm "self_quotient"; 

1256 
val self_remainder = thm "self_remainder"; 

1257 
val zdiv_self = thm "zdiv_self"; 

1258 
val zmod_self = thm "zmod_self"; 

1259 
val zdiv_zero = thm "zdiv_zero"; 

1260 
val div_eq_minus1 = thm "div_eq_minus1"; 

1261 
val zmod_zero = thm "zmod_zero"; 

1262 
val zdiv_minus1 = thm "zdiv_minus1"; 

1263 
val zmod_minus1 = thm "zmod_minus1"; 

1264 
val div_pos_pos = thm "div_pos_pos"; 

1265 
val mod_pos_pos = thm "mod_pos_pos"; 

1266 
val div_neg_pos = thm "div_neg_pos"; 

1267 
val mod_neg_pos = thm "mod_neg_pos"; 

1268 
val div_pos_neg = thm "div_pos_neg"; 

1269 
val mod_pos_neg = thm "mod_pos_neg"; 

1270 
val div_neg_neg = thm "div_neg_neg"; 

1271 
val mod_neg_neg = thm "mod_neg_neg"; 

1272 
val zmod_1 = thm "zmod_1"; 

1273 
val zdiv_1 = thm "zdiv_1"; 

1274 
val zmod_minus1_right = thm "zmod_minus1_right"; 

1275 
val zdiv_minus1_right = thm "zdiv_minus1_right"; 

1276 
val zdiv_mono1 = thm "zdiv_mono1"; 

1277 
val zdiv_mono1_neg = thm "zdiv_mono1_neg"; 

1278 
val zdiv_mono2 = thm "zdiv_mono2"; 

1279 
val zdiv_mono2_neg = thm "zdiv_mono2_neg"; 

1280 
val zdiv_zmult1_eq = thm "zdiv_zmult1_eq"; 

1281 
val zmod_zmult1_eq = thm "zmod_zmult1_eq"; 

1282 
val zmod_zmult1_eq' = thm "zmod_zmult1_eq'"; 

1283 
val zmod_zmult_distrib = thm "zmod_zmult_distrib"; 

1284 
val zdiv_zmult_self1 = thm "zdiv_zmult_self1"; 

1285 
val zdiv_zmult_self2 = thm "zdiv_zmult_self2"; 

1286 
val zmod_zmult_self1 = thm "zmod_zmult_self1"; 
