author  nipkow 
Fri, 15 Nov 2002 18:02:25 +0100  
changeset 13716  73de0ef7cb25 
parent 13601  fd3e3d6b37b2 
child 13788  fd03c4ab89d4 
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 

6 
The division operators div, mod and the divides relation "dvd" 

13183  7 

8 
Here is the division algorithm in ML: 

9 

10 
fun posDivAlg (a,b) = 

11 
if a<b then (0,a) 

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

13 
in if 0<=rb then (2*q+1, rb) else (2*q, r) 

14 
end 

15 

16 
fun negDivAlg (a,b) = 

17 
if 0<=a+b then (~1,a+b) 

18 
else let val (q,r) = negDivAlg(a, 2*b) 

19 
in if 0<=rb then (2*q+1, rb) else (2*q, r) 

20 
end; 

21 

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

23 

24 
fun divAlg (a,b) = if 0<=a then 

25 
if b>0 then posDivAlg (a,b) 

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

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

28 
else 

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

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

6917  31 
*) 
32 

13183  33 

13517  34 
theory IntDiv = IntArith + Recdef 
35 
files ("IntDiv_setup.ML"): 

13183  36 

37 
declare zless_nat_conj [simp] 

6917  38 

39 
constdefs 

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

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

42 
a = b*q + r & 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset

43 
(if 0 < b then 0<=r & r<b else b<r & r <= 0)" 
6917  44 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset

45 
adjust :: "[int, int*int] => int*int" 
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset

46 
"adjust b == %(q,r). if 0 <= rb then (2*q + 1, rb) 
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset

47 
else (2*q, r)" 
6917  48 

49 
(** the division algorithm **) 

50 

51 
(*for the case a>=0, b>0*) 

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

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset

53 
recdef posDivAlg "inv_image less_than (%(a,b). nat(a  b + 1))" 
6917  54 
"posDivAlg (a,b) = 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset

55 
(if (a<b  b<=0) then (0,a) 
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset

56 
else adjust b (posDivAlg(a, 2*b)))" 
6917  57 

58 
(*for the case a<0, b>0*) 

59 
consts negDivAlg :: "int*int => int*int" 

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

61 
"negDivAlg (a,b) = 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset

62 
(if (0<=a+b  b<=0) then (1,a+b) 
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset

63 
else adjust b (negDivAlg(a, 2*b)))" 
6917  64 

65 
(*for the general case b~=0*) 

66 

67 
constdefs 

68 
negateSnd :: "int*int => int*int" 

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

70 

71 
(*The full division algorithm considers all possible signs for a, b 

72 
including the special case a=0, b<0, because negDivAlg requires a<0*) 

73 
divAlg :: "int*int => int*int" 

74 
"divAlg == 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset

75 
%(a,b). if 0<=a then 
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset

76 
if 0<=b then posDivAlg (a,b) 
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset

77 
else if a=0 then (0,0) 
6917  78 
else negateSnd (negDivAlg (a,b)) 
79 
else 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset

80 
if 0<b then negDivAlg (a,b) 
6917  81 
else negateSnd (posDivAlg (a,b))" 
82 

83 
instance 

13183  84 
int :: "Divides.div" .. (*avoid clash with 'div' token*) 
6917  85 

86 
defs 

13183  87 
div_def: "a div b == fst (divAlg (a,b))" 
88 
mod_def: "a mod b == snd (divAlg (a,b))" 

89 

90 

91 

92 
(*** Uniqueness and monotonicity of quotients and remainders ***) 

93 

94 
lemma unique_quotient_lemma: 

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

96 
==> q' <= (q::int)" 

97 
apply (subgoal_tac "r' + b * (q'q) <= r") 

98 
prefer 2 apply (simp add: zdiff_zmult_distrib2) 

99 
apply (subgoal_tac "0 < b * (1 + q  q') ") 

100 
apply (erule_tac [2] order_le_less_trans) 

101 
prefer 2 apply (simp add: zdiff_zmult_distrib2 zadd_zmult_distrib2) 

102 
apply (subgoal_tac "b * q' < b * (1 + q) ") 

103 
prefer 2 apply (simp add: zdiff_zmult_distrib2 zadd_zmult_distrib2) 

104 
apply (simp add: zmult_zless_cancel1) 

105 
done 

106 

107 
lemma unique_quotient_lemma_neg: 

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

109 
==> q <= (q'::int)" 

110 
by (rule_tac b = "b" and r = "r'" and r' = "r" in unique_quotient_lemma, 

111 
auto) 

112 

113 
lemma unique_quotient: 

114 
"[ quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); b ~= 0 ] 

115 
==> q = q'" 

116 
apply (simp add: quorem_def linorder_neq_iff split: split_if_asm) 

117 
apply (blast intro: order_antisym 

118 
dest: order_eq_refl [THEN unique_quotient_lemma] 

119 
order_eq_refl [THEN unique_quotient_lemma_neg] sym)+ 

120 
done 

121 

122 

123 
lemma unique_remainder: 

124 
"[ quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); b ~= 0 ] 

125 
==> r = r'" 

126 
apply (subgoal_tac "q = q'") 

127 
apply (simp add: quorem_def) 

128 
apply (blast intro: unique_quotient) 

129 
done 

130 

131 

132 
(*** Correctness of posDivAlg, the division algorithm for a>=0 and b>0 ***) 

133 

134 
lemma adjust_eq [simp]: 

135 
"adjust b (q,r) = 

136 
(let diff = rb in 

137 
if 0 <= diff then (2*q + 1, diff) 

138 
else (2*q, r))" 

139 
by (simp add: Let_def adjust_def) 

140 

141 
declare posDivAlg.simps [simp del] 

142 

143 
(**use with a simproc to avoid repeatedly proving the premise*) 

144 
lemma posDivAlg_eqn: 

145 
"0 < b ==> 

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

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

148 

149 
(*Correctness of posDivAlg: it computes quotients correctly*) 

150 
lemma posDivAlg_correct [rule_format]: 

151 
"0 <= a > 0 < b > quorem ((a, b), posDivAlg (a, b))" 

152 
apply (induct_tac a b rule: posDivAlg.induct, auto) 

153 
apply (simp_all add: quorem_def) 

154 
(*base case: a<b*) 

155 
apply (simp add: posDivAlg_eqn) 

156 
(*main argument*) 

157 
apply (subst posDivAlg_eqn, simp_all) 

158 
apply (erule splitE) 

159 
apply (auto simp add: zadd_zmult_distrib2 Let_def) 

160 
done 

161 

162 

163 
(*** Correctness of negDivAlg, the division algorithm for a<0 and b>0 ***) 

164 

165 
declare negDivAlg.simps [simp del] 

166 

167 
(**use with a simproc to avoid repeatedly proving the premise*) 

168 
lemma negDivAlg_eqn: 

169 
"0 < b ==> 

170 
negDivAlg (a,b) = 

171 
(if 0<=a+b then (1,a+b) else adjust b (negDivAlg(a, 2*b)))" 

172 
by (rule negDivAlg.simps [THEN trans], simp) 

173 

174 
(*Correctness of negDivAlg: it computes quotients correctly 

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

176 
lemma negDivAlg_correct [rule_format]: 

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

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

179 
apply (simp_all add: quorem_def) 

180 
(*base case: 0<=a+b*) 

181 
apply (simp add: negDivAlg_eqn) 

182 
(*main argument*) 

183 
apply (subst negDivAlg_eqn, assumption) 

184 
apply (erule splitE) 

185 
apply (auto simp add: zadd_zmult_distrib2 Let_def) 

186 
done 

187 

188 

189 
(*** Existence shown by proving the division algorithm to be correct ***) 

190 

191 
(*the case a=0*) 

192 
lemma quorem_0: "b ~= 0 ==> quorem ((0,b), (0,0))" 

193 
by (auto simp add: quorem_def linorder_neq_iff) 

194 

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

196 
by (subst posDivAlg.simps, auto) 

197 

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

199 
by (subst negDivAlg.simps, auto) 

200 

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

202 
by (unfold negateSnd_def, auto) 

203 

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

205 
by (auto simp add: split_ifs quorem_def) 

206 

207 
lemma divAlg_correct: "b ~= 0 ==> quorem ((a,b), divAlg(a,b))" 

208 
by (force simp add: linorder_neq_iff quorem_0 divAlg_def quorem_neg 

209 
posDivAlg_correct negDivAlg_correct) 

210 

211 
(** Arbitrary definitions for division by zero. Useful to simplify 

212 
certain equations **) 

213 

214 
lemma DIVISION_BY_ZERO: "a div (0::int) = 0 & a mod (0::int) = a" 

215 
by (simp add: div_def mod_def divAlg_def posDivAlg.simps) (*NOT for adding to default simpset*) 

216 

217 
(** Basic laws about division and remainder **) 

218 

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

220 
apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO) 

221 
apply (cut_tac a = a and b = b in divAlg_correct) 

222 
apply (auto simp add: quorem_def div_def mod_def) 

223 
done 

224 

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

227 

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

229 
by(simp add: zmult_commute zmod_zdiv_equality[symmetric]) 

230 

231 
use "IntDiv_setup.ML" 

232 

13183  233 
lemma pos_mod_conj : "(0::int) < b ==> 0 <= a mod b & a mod b < b" 
234 
apply (cut_tac a = a and b = b in divAlg_correct) 

235 
apply (auto simp add: quorem_def mod_def) 

236 
done 

237 

238 
lemmas pos_mod_sign = pos_mod_conj [THEN conjunct1, standard] 

239 
and pos_mod_bound = pos_mod_conj [THEN conjunct2, standard] 

240 

241 
lemma neg_mod_conj : "b < (0::int) ==> a mod b <= 0 & b < a mod b" 

242 
apply (cut_tac a = a and b = b in divAlg_correct) 

243 
apply (auto simp add: quorem_def div_def mod_def) 

244 
done 

245 

246 
lemmas neg_mod_sign = neg_mod_conj [THEN conjunct1, standard] 

247 
and neg_mod_bound = neg_mod_conj [THEN conjunct2, standard] 

248 

249 

13260  250 

13183  251 
(** proving general properties of div and mod **) 
252 

253 
lemma quorem_div_mod: "b ~= 0 ==> quorem ((a, b), (a div b, a mod b))" 

254 
apply (cut_tac a = a and b = b in zmod_zdiv_equality) 

255 
apply (force simp add: quorem_def linorder_neq_iff pos_mod_sign pos_mod_bound 

256 
neg_mod_sign neg_mod_bound) 

257 
done 

258 

259 
lemma quorem_div: "[ quorem((a,b),(q,r)); b ~= 0 ] ==> a div b = q" 

260 
by (simp add: quorem_div_mod [THEN unique_quotient]) 

261 

262 
lemma quorem_mod: "[ quorem((a,b),(q,r)); b ~= 0 ] ==> a mod b = r" 

263 
by (simp add: quorem_div_mod [THEN unique_remainder]) 

264 

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

266 
apply (rule quorem_div) 

267 
apply (auto simp add: quorem_def) 

268 
done 

269 

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

271 
apply (rule quorem_div) 

272 
apply (auto simp add: quorem_def) 

273 
done 

274 

275 
lemma div_pos_neg_trivial: "[ (0::int) < a; a+b <= 0 ] ==> a div b = 1" 

276 
apply (rule quorem_div) 

277 
apply (auto simp add: quorem_def) 

278 
done 

279 

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

281 

282 
lemma mod_pos_pos_trivial: "[ (0::int) <= a; a < b ] ==> a mod b = a" 

283 
apply (rule_tac q = 0 in quorem_mod) 

284 
apply (auto simp add: quorem_def) 

285 
done 

286 

287 
lemma mod_neg_neg_trivial: "[ a <= (0::int); b < a ] ==> a mod b = a" 

288 
apply (rule_tac q = 0 in quorem_mod) 

289 
apply (auto simp add: quorem_def) 

290 
done 

291 

292 
lemma mod_pos_neg_trivial: "[ (0::int) < a; a+b <= 0 ] ==> a mod b = a+b" 

293 
apply (rule_tac q = "1" in quorem_mod) 

294 
apply (auto simp add: quorem_def) 

295 
done 

296 

297 
(*There is no mod_neg_pos_trivial...*) 

298 

299 

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

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

302 
apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO) 

303 
apply (simp add: quorem_div_mod [THEN quorem_neg, simplified, 

304 
THEN quorem_div, THEN sym]) 

305 

306 
done 

307 

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

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

310 
apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO) 

311 
apply (subst quorem_div_mod [THEN quorem_neg, simplified, THEN quorem_mod], 

312 
auto) 

313 
done 

314 

315 
(*** div, mod and unary minus ***) 

316 

317 
lemma zminus1_lemma: 

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

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

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

321 
by (force simp add: split_ifs quorem_def linorder_neq_iff zdiff_zmult_distrib2) 

322 

323 

324 
lemma zdiv_zminus1_eq_if: 

325 
"b ~= (0::int) 

326 
==> (a) div b = 

327 
(if a mod b = 0 then  (a div b) else  (a div b)  1)" 

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

329 

330 
lemma zmod_zminus1_eq_if: 

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

332 
apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO) 

333 
apply (blast intro: quorem_div_mod [THEN zminus1_lemma, THEN quorem_mod]) 

334 
done 

335 

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

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

338 

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

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

341 

342 
lemma zdiv_zminus2_eq_if: 

343 
"b ~= (0::int) 

344 
==> a div (b) = 

345 
(if a mod b = 0 then  (a div b) else  (a div b)  1)" 

346 
by (simp add: zdiv_zminus1_eq_if zdiv_zminus2) 

347 

348 
lemma zmod_zminus2_eq_if: 

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

350 
by (simp add: zmod_zminus1_eq_if zmod_zminus2) 

351 

352 

353 
(*** division of a number by itself ***) 

354 

13524  355 
lemma self_quotient_aux1: "[ (0::int) < a; a = r + a*q; r < a ] ==> 1 <= q" 
13183  356 
apply (subgoal_tac "0 < a*q") 
357 
apply (simp add: int_0_less_mult_iff, arith) 

358 
done 

359 

13524  360 
lemma self_quotient_aux2: "[ (0::int) < a; a = r + a*q; 0 <= r ] ==> q <= 1" 
13183  361 
apply (subgoal_tac "0 <= a* (1q) ") 
362 
apply (simp add: int_0_le_mult_iff) 

363 
apply (simp add: zdiff_zmult_distrib2) 

364 
done 

365 

366 
lemma self_quotient: "[ quorem((a,a),(q,r)); a ~= (0::int) ] ==> q = 1" 

367 
apply (simp add: split_ifs quorem_def linorder_neq_iff) 

13601  368 
apply (rule order_antisym, safe, simp_all (no_asm_use)) 
13524  369 
apply (rule_tac [3] a = "a" and r = "r" in self_quotient_aux1) 
370 
apply (rule_tac a = "a" and r = "r" in self_quotient_aux2) 

13601  371 
apply (force intro: self_quotient_aux1 self_quotient_aux2 simp only: zadd_commute zmult_zminus)+ 
13183  372 
done 
373 

374 
lemma self_remainder: "[ quorem((a,a),(q,r)); a ~= (0::int) ] ==> r = 0" 

375 
apply (frule self_quotient, assumption) 

376 
apply (simp add: quorem_def) 

377 
done 

378 

379 
lemma zdiv_self [simp]: "a ~= 0 ==> a div a = (1::int)" 

380 
by (simp add: quorem_div_mod [THEN self_quotient]) 

381 

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

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

384 
apply (case_tac "a = 0", simp add: DIVISION_BY_ZERO) 

385 
apply (simp add: quorem_div_mod [THEN self_remainder]) 

386 
done 

387 

388 

389 
(*** Computation of division and remainder ***) 

390 

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

392 
by (simp add: div_def divAlg_def) 

393 

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

395 
by (simp add: div_def divAlg_def) 

396 

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

398 
by (simp add: mod_def divAlg_def) 

399 

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

401 
by (simp add: div_def divAlg_def) 

402 

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

404 
by (simp add: mod_def divAlg_def) 

405 

406 
(** a positive, b positive **) 

407 

408 
lemma div_pos_pos: "[ 0 < a; 0 <= b ] ==> a div b = fst (posDivAlg(a,b))" 

409 
by (simp add: div_def divAlg_def) 

410 

411 
lemma mod_pos_pos: "[ 0 < a; 0 <= b ] ==> a mod b = snd (posDivAlg(a,b))" 

412 
by (simp add: mod_def divAlg_def) 

413 

414 
(** a negative, b positive **) 

415 

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

417 
by (simp add: div_def divAlg_def) 

418 

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

420 
by (simp add: mod_def divAlg_def) 

421 

422 
(** a positive, b negative **) 

423 

424 
lemma div_pos_neg: 

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

426 
by (simp add: div_def divAlg_def) 

427 

428 
lemma mod_pos_neg: 

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

430 
by (simp add: mod_def divAlg_def) 

431 

432 
(** a negative, b negative **) 

433 

434 
lemma div_neg_neg: 

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

436 
by (simp add: div_def divAlg_def) 

437 

438 
lemma mod_neg_neg: 

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

440 
by (simp add: mod_def divAlg_def) 

441 

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

443 

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

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

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

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

448 

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

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

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

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

453 

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

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

456 

457 

458 
(** Specialcase simplification **) 

459 

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

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

462 
apply (cut_tac [2] a = a and b = 1 in pos_mod_bound, auto) 

463 
done 

464 

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

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

467 

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

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

470 
apply (cut_tac [2] a = a and b = "1" in neg_mod_bound, auto) 

471 
done 

472 

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

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

475 

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

477 
1 div z and 1 mod z **) 

478 

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

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

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

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

483 

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

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

486 

487 

488 
(*** Monotonicity in the first argument (divisor) ***) 

489 

490 
lemma zdiv_mono1: "[ a <= a'; 0 < (b::int) ] ==> a div b <= a' div b" 

491 
apply (cut_tac a = a and b = b in zmod_zdiv_equality) 

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

493 
apply (rule unique_quotient_lemma) 

494 
apply (erule subst) 

495 
apply (erule subst) 

496 
apply (simp_all add: pos_mod_sign pos_mod_bound) 

497 
done 

498 

499 
lemma zdiv_mono1_neg: "[ a <= a'; (b::int) < 0 ] ==> a' div b <= a div b" 

500 
apply (cut_tac a = a and b = b in zmod_zdiv_equality) 

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

502 
apply (rule unique_quotient_lemma_neg) 

503 
apply (erule subst) 

504 
apply (erule subst) 

505 
apply (simp_all add: neg_mod_sign neg_mod_bound) 

506 
done 

6917  507 

508 

13183  509 
(*** Monotonicity in the second argument (dividend) ***) 
510 

511 
lemma q_pos_lemma: 

512 
"[ 0 <= b'*q' + r'; r' < b'; 0 < b' ] ==> 0 <= (q'::int)" 

513 
apply (subgoal_tac "0 < b'* (q' + 1) ") 

514 
apply (simp add: int_0_less_mult_iff) 

515 
apply (simp add: zadd_zmult_distrib2) 

516 
done 

517 

518 
lemma zdiv_mono2_lemma: 

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

520 
r' < b'; 0 <= r; 0 < b'; b' <= b ] 

521 
==> q <= (q'::int)" 

522 
apply (frule q_pos_lemma, assumption+) 

523 
apply (subgoal_tac "b*q < b* (q' + 1) ") 

524 
apply (simp add: zmult_zless_cancel1) 

525 
apply (subgoal_tac "b*q = r'  r + b'*q'") 

526 
prefer 2 apply simp 

527 
apply (simp (no_asm_simp) add: zadd_zmult_distrib2) 

528 
apply (subst zadd_commute, rule zadd_zless_mono, arith) 

529 
apply (rule zmult_zle_mono1, auto) 

530 
done 

531 

532 
lemma zdiv_mono2: 

533 
"[ (0::int) <= a; 0 < b'; b' <= b ] ==> a div b <= a div b'" 

534 
apply (subgoal_tac "b ~= 0") 

535 
prefer 2 apply arith 

536 
apply (cut_tac a = a and b = b in zmod_zdiv_equality) 

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

538 
apply (rule zdiv_mono2_lemma) 

539 
apply (erule subst) 

540 
apply (erule subst) 

541 
apply (simp_all add: pos_mod_sign pos_mod_bound) 

542 
done 

543 

544 
lemma q_neg_lemma: 

545 
"[ b'*q' + r' < 0; 0 <= r'; 0 < b' ] ==> q' <= (0::int)" 

546 
apply (subgoal_tac "b'*q' < 0") 

547 
apply (simp add: zmult_less_0_iff, arith) 

548 
done 

549 

550 
lemma zdiv_mono2_neg_lemma: 

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

552 
r < b; 0 <= r'; 0 < b'; b' <= b ] 

553 
==> q' <= (q::int)" 

554 
apply (frule q_neg_lemma, assumption+) 

555 
apply (subgoal_tac "b*q' < b* (q + 1) ") 

556 
apply (simp add: zmult_zless_cancel1) 

557 
apply (simp add: zadd_zmult_distrib2) 

558 
apply (subgoal_tac "b*q' <= b'*q'") 

559 
prefer 2 apply (simp add: zmult_zle_mono1_neg) 

560 
apply (subgoal_tac "b'*q' < b + b*q") 

561 
apply arith 

562 
apply simp 

563 
done 

564 

565 
lemma zdiv_mono2_neg: 

566 
"[ a < (0::int); 0 < b'; b' <= b ] ==> a div b' <= a div b" 

567 
apply (cut_tac a = a and b = b in zmod_zdiv_equality) 

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

569 
apply (rule zdiv_mono2_neg_lemma) 

570 
apply (erule subst) 

571 
apply (erule subst) 

572 
apply (simp_all add: pos_mod_sign pos_mod_bound) 

573 
done 

574 

575 

576 
(*** More algebraic laws for div and mod ***) 

577 

578 
(** proving (a*b) div c = a * (b div c) + a * (b mod c) **) 

579 

580 
lemma zmult1_lemma: 

581 
"[ quorem((b,c),(q,r)); c ~= 0 ] 

582 
==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))" 

583 
by (force simp add: split_ifs quorem_def linorder_neq_iff zadd_zmult_distrib2 

13517  584 
pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound) 
13183  585 

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

587 
apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO) 

588 
apply (blast intro: quorem_div_mod [THEN zmult1_lemma, THEN quorem_div]) 

589 
done 

590 

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

592 
apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO) 

593 
apply (blast intro: quorem_div_mod [THEN zmult1_lemma, THEN quorem_mod]) 

594 
done 

595 

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

597 
apply (rule trans) 

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

599 
apply (rule_tac [2] zmod_zmult1_eq) 

600 
apply (simp_all add: zmult_commute) 

601 
done 

602 

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

604 
apply (rule zmod_zmult1_eq' [THEN trans]) 

605 
apply (rule zmod_zmult1_eq) 

606 
done 

607 

608 
lemma zdiv_zmult_self1 [simp]: "b ~= (0::int) ==> (a*b) div b = a" 

609 
by (simp add: zdiv_zmult1_eq) 

610 

611 
lemma zdiv_zmult_self2 [simp]: "b ~= (0::int) ==> (b*a) div b = a" 

612 
by (subst zmult_commute, erule zdiv_zmult_self1) 

613 

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

615 
by (simp add: zmod_zmult1_eq) 

616 

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

618 
by (simp add: zmult_commute zmod_zmult1_eq) 

619 

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

13517  621 
proof 
622 
assume "m mod d = 0" 

623 
from this zmod_zdiv_equality[of m d] show "EX q::int. m = d*q" by auto 

624 
next 

625 
assume "EX q::int. m = d*q" 

626 
thus "m mod d = 0" by auto 

627 
qed 

13183  628 

629 
declare zmod_eq_0_iff [THEN iffD1, dest!] 

630 

13716  631 
lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))" 
632 
by(simp add:dvd_def zmod_eq_0_iff) 

13183  633 

634 
(** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **) 

635 

636 
lemma zadd1_lemma: 

637 
"[ quorem((a,c),(aq,ar)); quorem((b,c),(bq,br)); c ~= 0 ] 

638 
==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))" 

639 
by (force simp add: split_ifs quorem_def linorder_neq_iff zadd_zmult_distrib2 

13517  640 
pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound) 
13183  641 

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

643 
lemma zdiv_zadd1_eq: 

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

645 
apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO) 

646 
apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_div) 

647 
done 

648 

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

650 
apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO) 

651 
apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_mod) 

652 
done 

653 

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

655 
apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO) 

656 
apply (auto simp add: linorder_neq_iff pos_mod_sign pos_mod_bound 

657 
div_pos_pos_trivial neg_mod_sign neg_mod_bound div_neg_neg_trivial) 

658 
done 

659 

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

661 
apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO) 

662 
apply (force simp add: linorder_neq_iff pos_mod_sign pos_mod_bound 

663 
mod_pos_pos_trivial neg_mod_sign neg_mod_bound 

664 
mod_neg_neg_trivial) 

665 
done 

666 

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

668 
apply (rule trans [symmetric]) 

669 
apply (rule zmod_zadd1_eq, simp) 

670 
apply (rule zmod_zadd1_eq [symmetric]) 

671 
done 

672 

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

674 
apply (rule trans [symmetric]) 

675 
apply (rule zmod_zadd1_eq, simp) 

676 
apply (rule zmod_zadd1_eq [symmetric]) 

677 
done 

678 

679 
lemma zdiv_zadd_self1[simp]: "a ~= (0::int) ==> (a+b) div a = b div a + 1" 

680 
by (simp add: zdiv_zadd1_eq) 

681 

682 
lemma zdiv_zadd_self2[simp]: "a ~= (0::int) ==> (b+a) div a = b div a + 1" 

683 
by (simp add: zdiv_zadd1_eq) 

684 

685 
lemma zmod_zadd_self1[simp]: "(a+b) mod a = b mod (a::int)" 

686 
apply (case_tac "a = 0", simp add: DIVISION_BY_ZERO) 

687 
apply (simp add: zmod_zadd1_eq) 

688 
done 

689 

690 
lemma zmod_zadd_self2[simp]: "(b+a) mod a = b mod (a::int)" 

691 
apply (case_tac "a = 0", simp add: DIVISION_BY_ZERO) 

692 
apply (simp add: zmod_zadd1_eq) 

693 
done 

694 

695 

696 
(*** proving a div (b*c) = (a div b) div c ***) 

697 

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

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

700 
to cause particular problems.*) 

701 

702 
(** first, four lemmas to bound the remainder for the cases b<0 and b>0 **) 

703 

13524  704 
lemma zmult2_lemma_aux1: "[ (0::int) < c; b < r; r <= 0 ] ==> b*c < b*(q mod c) + r" 
13183  705 
apply (subgoal_tac "b * (c  q mod c) < r * 1") 
706 
apply (simp add: zdiff_zmult_distrib2) 

707 
apply (rule order_le_less_trans) 

708 
apply (erule_tac [2] zmult_zless_mono1) 

709 
apply (rule zmult_zle_mono2_neg) 

710 
apply (auto simp add: zcompare_rls zadd_commute [of 1] 

711 
add1_zle_eq pos_mod_bound) 

712 
done 

713 

13524  714 
lemma zmult2_lemma_aux2: "[ (0::int) < c; b < r; r <= 0 ] ==> b * (q mod c) + r <= 0" 
13183  715 
apply (subgoal_tac "b * (q mod c) <= 0") 
716 
apply arith 

717 
apply (simp add: zmult_le_0_iff pos_mod_sign) 

718 
done 

719 

13524  720 
lemma zmult2_lemma_aux3: "[ (0::int) < c; 0 <= r; r < b ] ==> 0 <= b * (q mod c) + r" 
13183  721 
apply (subgoal_tac "0 <= b * (q mod c) ") 
722 
apply arith 

723 
apply (simp add: int_0_le_mult_iff pos_mod_sign) 

724 
done 

725 

13524  726 
lemma zmult2_lemma_aux4: "[ (0::int) < c; 0 <= r; r < b ] ==> b * (q mod c) + r < b * c" 
13183  727 
apply (subgoal_tac "r * 1 < b * (c  q mod c) ") 
728 
apply (simp add: zdiff_zmult_distrib2) 

729 
apply (rule order_less_le_trans) 

730 
apply (erule zmult_zless_mono1) 

731 
apply (rule_tac [2] zmult_zle_mono2) 

732 
apply (auto simp add: zcompare_rls zadd_commute [of 1] 

733 
add1_zle_eq pos_mod_bound) 

734 
done 

735 

736 
lemma zmult2_lemma: "[ quorem ((a,b), (q,r)); b ~= 0; 0 < c ] 

737 
==> quorem ((a, b*c), (q div c, b*(q mod c) + r))" 

13517  738 
by (auto simp add: zmult_ac quorem_def linorder_neq_iff 
13183  739 
int_0_less_mult_iff zadd_zmult_distrib2 [symmetric] 
13524  740 
zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4) 
13183  741 

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

743 
apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO) 

744 
apply (force simp add: quorem_div_mod [THEN zmult2_lemma, THEN quorem_div]) 

745 
done 

746 

747 
lemma zmod_zmult2_eq: 

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

749 
apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO) 

750 
apply (force simp add: quorem_div_mod [THEN zmult2_lemma, THEN quorem_mod]) 

751 
done 

752 

753 

754 
(*** Cancellation of common factors in div ***) 

755 

13524  756 
lemma zdiv_zmult_zmult1_aux1: "[ (0::int) < b; c ~= 0 ] ==> (c*a) div (c*b) = a div b" 
13183  757 
by (subst zdiv_zmult2_eq, auto) 
758 

13524  759 
lemma zdiv_zmult_zmult1_aux2: "[ b < (0::int); c ~= 0 ] ==> (c*a) div (c*b) = a div b" 
13183  760 
apply (subgoal_tac " (c * (a)) div (c * (b)) = (a) div (b) ") 
13524  761 
apply (rule_tac [2] zdiv_zmult_zmult1_aux1, auto) 
13183  762 
done 
763 

764 
lemma zdiv_zmult_zmult1: "c ~= (0::int) ==> (c*a) div (c*b) = a div b" 

765 
apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO) 

13524  766 
apply (auto simp add: linorder_neq_iff zdiv_zmult_zmult1_aux1 zdiv_zmult_zmult1_aux2) 
13183  767 
done 
768 

769 
lemma zdiv_zmult_zmult2: "c ~= (0::int) ==> (a*c) div (b*c) = a div b" 

770 
apply (drule zdiv_zmult_zmult1) 

771 
apply (auto simp add: zmult_commute) 

772 
done 

773 

774 

775 

776 
(*** Distribution of factors over mod ***) 

777 

13524  778 
lemma zmod_zmult_zmult1_aux1: "[ (0::int) < b; c ~= 0 ] ==> (c*a) mod (c*b) = c * (a mod b)" 
13183  779 
by (subst zmod_zmult2_eq, auto) 
780 

13524  781 
lemma zmod_zmult_zmult1_aux2: "[ b < (0::int); c ~= 0 ] ==> (c*a) mod (c*b) = c * (a mod b)" 
13183  782 
apply (subgoal_tac " (c * (a)) mod (c * (b)) = c * ((a) mod (b))") 
13524  783 
apply (rule_tac [2] zmod_zmult_zmult1_aux1, auto) 
13183  784 
done 
785 

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

787 
apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO) 

788 
apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO) 

13524  789 
apply (auto simp add: linorder_neq_iff zmod_zmult_zmult1_aux1 zmod_zmult_zmult1_aux2) 
13183  790 
done 
791 

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

793 
apply (cut_tac c = c in zmod_zmult_zmult1) 

794 
apply (auto simp add: zmult_commute) 

795 
done 

796 

797 

13260  798 
subsection {*splitting rules for div and mod*} 
799 

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

801 

802 
lemma split_pos_lemma: 

803 
"0<k ==> 

804 
P(n div k :: int)(n mod k) = (\<forall>i j. 0<=j & j<k & n = k*i + j > P i j)" 

805 
apply (rule iffI) 

806 
apply clarify 

807 
apply (erule_tac P="P ?x ?y" in rev_mp) 

808 
apply (subst zmod_zadd1_eq) 

809 
apply (subst zdiv_zadd1_eq) 

810 
apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial) 

811 
txt{*converse direction*} 

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

813 
apply (drule_tac x = "n mod k" in spec) 

13517  814 
apply (simp add: pos_mod_bound pos_mod_sign) 
13260  815 
done 
816 

817 
lemma split_neg_lemma: 

818 
"k<0 ==> 

819 
P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j<=0 & n = k*i + j > P i j)" 

820 
apply (rule iffI) 

821 
apply clarify 

822 
apply (erule_tac P="P ?x ?y" in rev_mp) 

823 
apply (subst zmod_zadd1_eq) 

824 
apply (subst zdiv_zadd1_eq) 

825 
apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial) 

826 
txt{*converse direction*} 

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

828 
apply (drule_tac x = "n mod k" in spec) 

13517  829 
apply (simp add: neg_mod_bound neg_mod_sign) 
13260  830 
done 
831 

832 
lemma split_zdiv: 

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

834 
((k = 0 > P 0) & 

835 
(0<k > (\<forall>i j. 0<=j & j<k & n = k*i + j > P i)) & 

836 
(k<0 > (\<forall>i j. k<j & j<=0 & n = k*i + j > P i)))" 

837 
apply (case_tac "k=0") 

838 
apply (simp add: DIVISION_BY_ZERO) 

839 
apply (simp only: linorder_neq_iff) 

840 
apply (erule disjE) 

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

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

843 
done 

844 

845 
lemma split_zmod: 

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

847 
((k = 0 > P n) & 

848 
(0<k > (\<forall>i j. 0<=j & j<k & n = k*i + j > P j)) & 

849 
(k<0 > (\<forall>i j. k<j & j<=0 & n = k*i + j > P j)))" 

850 
apply (case_tac "k=0") 

851 
apply (simp add: DIVISION_BY_ZERO) 

852 
apply (simp only: linorder_neq_iff) 

853 
apply (erule disjE) 

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

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

856 
done 

857 

858 
(* Enable arith to deal with div 2 and mod 2: *) 

13266
2a6ad4357d72
modified Larry's changes to make div/mod a numeral work in arith.
nipkow
parents:
13260
diff
changeset

859 
declare split_zdiv [of _ _ "number_of k", simplified, standard, arith_split] 
2a6ad4357d72
modified Larry's changes to make div/mod a numeral work in arith.
nipkow
parents:
13260
diff
changeset

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

862 

863 
subsection{*Speeding up the division algorithm with shifting*} 

13183  864 

865 
(** computing div by shifting **) 

866 

867 
lemma pos_zdiv_mult_2: "(0::int) <= a ==> (1 + 2*b) div (2*a) = b div a" 

868 
apply (case_tac "a = 0", simp add: DIVISION_BY_ZERO) 

869 
apply (subgoal_tac "1 <= a") 

870 
prefer 2 apply arith 

871 
apply (subgoal_tac "1 < a * 2") 

872 
prefer 2 apply arith 

873 
apply (subgoal_tac "2* (1 + b mod a) <= 2*a") 

874 
apply (rule_tac [2] zmult_zle_mono2) 

875 
apply (auto simp add: zadd_commute [of 1] zmult_commute add1_zle_eq 

876 
pos_mod_bound) 

877 
apply (subst zdiv_zadd1_eq) 

878 
apply (simp add: zdiv_zmult_zmult2 zmod_zmult_zmult2 div_pos_pos_trivial) 

879 
apply (subst div_pos_pos_trivial) 

880 
apply (auto simp add: mod_pos_pos_trivial) 

881 
apply (subgoal_tac "0 <= b mod a", arith) 

882 
apply (simp add: pos_mod_sign) 

883 
done 

884 

885 

886 
lemma neg_zdiv_mult_2: "a <= (0::int) ==> (1 + 2*b) div (2*a) = (b+1) div a" 

887 
apply (subgoal_tac " (1 + 2* (b  1)) div (2 * (a)) = (b  1) div (a) ") 

888 
apply (rule_tac [2] pos_zdiv_mult_2) 

889 
apply (auto simp add: zmult_zminus_right) 

890 
apply (subgoal_tac " (1  (2 * b)) =  (1 + (2 * b))") 

891 
apply (simp only: zdiv_zminus_zminus zdiff_def zminus_zadd_distrib [symmetric], 

892 
simp) 

893 
done 

894 

895 

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

897 
simplification problems*) 

898 
lemma not_0_le_lemma: "~ 0 <= x ==> x <= (0::int)" 

899 
by auto 

900 

901 
lemma zdiv_number_of_BIT[simp]: 

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

903 
(if ~b  (0::int) <= number_of w 

904 
then number_of v div (number_of w) 

905 
else (number_of v + (1::int)) div (number_of w))" 

906 
apply (simp only: zadd_assoc number_of_BIT) 

907 
(*create subgoal because the next step can't simplify numerals*) 

908 
apply (subgoal_tac "2 ~= (0::int) ") 

909 
apply (simp del: bin_arith_extra_simps 

13260  910 
add: zdiv_zmult_zmult1 pos_zdiv_mult_2 not_0_le_lemma neg_zdiv_mult_2, simp) 
13183  911 
done 
912 

913 

914 
(** computing mod by shifting (proofs resemble those for div) **) 

915 

916 
lemma pos_zmod_mult_2: 

917 
"(0::int) <= a ==> (1 + 2*b) mod (2*a) = 1 + 2 * (b mod a)" 

918 
apply (case_tac "a = 0", simp add: DIVISION_BY_ZERO) 

919 
apply (subgoal_tac "1 <= a") 

920 
prefer 2 apply arith 

921 
apply (subgoal_tac "1 < a * 2") 

922 
prefer 2 apply arith 

923 
apply (subgoal_tac "2* (1 + b mod a) <= 2*a") 

924 
apply (rule_tac [2] zmult_zle_mono2) 

925 
apply (auto simp add: zadd_commute [of 1] zmult_commute add1_zle_eq 

926 
pos_mod_bound) 

927 
apply (subst zmod_zadd1_eq) 

928 
apply (simp add: zmod_zmult_zmult2 mod_pos_pos_trivial) 

929 
apply (rule mod_pos_pos_trivial) 

930 
apply (auto simp add: mod_pos_pos_trivial) 

931 
apply (subgoal_tac "0 <= b mod a", arith) 

932 
apply (simp add: pos_mod_sign) 

933 
done 

934 

935 

936 
lemma neg_zmod_mult_2: 

937 
"a <= (0::int) ==> (1 + 2*b) mod (2*a) = 2 * ((b+1) mod a)  1" 

938 
apply (subgoal_tac "(1 + 2* (b  1)) mod (2* (a)) = 

939 
1 + 2* ((b  1) mod (a))") 

940 
apply (rule_tac [2] pos_zmod_mult_2) 

941 
apply (auto simp add: zmult_zminus_right) 

942 
apply (subgoal_tac " (1  (2 * b)) =  (1 + (2 * b))") 

943 
prefer 2 apply simp 

944 
apply (simp only: zmod_zminus_zminus zdiff_def zminus_zadd_distrib [symmetric]) 

945 
done 

946 

947 
lemma zmod_number_of_BIT [simp]: 

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

949 
(if b then 

950 
if (0::int) <= number_of w 

951 
then 2 * (number_of v mod number_of w) + 1 

952 
else 2 * ((number_of v + (1::int)) mod number_of w)  1 

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

954 
apply (simp only: zadd_assoc number_of_BIT) 

955 
apply (simp del: bin_arith_extra_simps bin_rel_simps 

13260  956 
add: zmod_zmult_zmult1 pos_zmod_mult_2 not_0_le_lemma neg_zmod_mult_2, simp) 
13183  957 
done 
958 

959 

960 

961 
(** Quotients of signs **) 

962 

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

964 
apply (subgoal_tac "a div b <= 1", force) 

965 
apply (rule order_trans) 

966 
apply (rule_tac a' = "1" in zdiv_mono1) 

967 
apply (auto simp add: zdiv_minus1) 

968 
done 

969 

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

971 
by (drule zdiv_mono1_neg, auto) 

972 

973 
lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 <= a div b) = (0 <= a)" 

974 
apply auto 

975 
apply (drule_tac [2] zdiv_mono1) 

976 
apply (auto simp add: linorder_neq_iff) 

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

978 
apply (blast intro: div_neg_pos_less0) 

979 
done 

980 

981 
lemma neg_imp_zdiv_nonneg_iff: 

982 
"b < (0::int) ==> (0 <= a div b) = (a <= (0::int))" 

983 
apply (subst zdiv_zminus_zminus [symmetric]) 

984 
apply (subst pos_imp_zdiv_nonneg_iff, auto) 

985 
done 

986 

987 
(*But not (a div b <= 0 iff a<=0); consider a=1, b=2 when a div b = 0.*) 

988 
lemma pos_imp_zdiv_neg_iff: "(0::int) < b ==> (a div b < 0) = (a < 0)" 

989 
by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff) 

990 

991 
(*Again the law fails for <=: consider a = 1, b = 2 when a div b = 0*) 

992 
lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)" 

993 
by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff) 

994 

995 
ML 

996 
{* 

997 
val quorem_def = thm "quorem_def"; 

998 

999 
val unique_quotient = thm "unique_quotient"; 

1000 
val unique_remainder = thm "unique_remainder"; 

1001 
val adjust_eq = thm "adjust_eq"; 

1002 
val posDivAlg_eqn = thm "posDivAlg_eqn"; 

1003 
val posDivAlg_correct = thm "posDivAlg_correct"; 

1004 
val negDivAlg_eqn = thm "negDivAlg_eqn"; 

1005 
val negDivAlg_correct = thm "negDivAlg_correct"; 

1006 
val quorem_0 = thm "quorem_0"; 

1007 
val posDivAlg_0 = thm "posDivAlg_0"; 

1008 
val negDivAlg_minus1 = thm "negDivAlg_minus1"; 

1009 
val negateSnd_eq = thm "negateSnd_eq"; 

1010 
val quorem_neg = thm "quorem_neg"; 

1011 
val divAlg_correct = thm "divAlg_correct"; 

1012 
val DIVISION_BY_ZERO = thm "DIVISION_BY_ZERO"; 

1013 
val zmod_zdiv_equality = thm "zmod_zdiv_equality"; 

1014 
val pos_mod_conj = thm "pos_mod_conj"; 

1015 
val pos_mod_sign = thm "pos_mod_sign"; 

1016 
val neg_mod_conj = thm "neg_mod_conj"; 

1017 
val neg_mod_sign = thm "neg_mod_sign"; 

1018 
val quorem_div_mod = thm "quorem_div_mod"; 

1019 
val quorem_div = thm "quorem_div"; 

1020 
val quorem_mod = thm "quorem_mod"; 

1021 
val div_pos_pos_trivial = thm "div_pos_pos_trivial"; 

1022 
val div_neg_neg_trivial = thm "div_neg_neg_trivial"; 

1023 
val div_pos_neg_trivial = thm "div_pos_neg_trivial"; 

1024 
val mod_pos_pos_trivial = thm "mod_pos_pos_trivial"; 

1025 
val mod_neg_neg_trivial = thm "mod_neg_neg_trivial"; 

1026 
val mod_pos_neg_trivial = thm "mod_pos_neg_trivial"; 

1027 
val zdiv_zminus_zminus = thm "zdiv_zminus_zminus"; 

1028 
val zmod_zminus_zminus = thm "zmod_zminus_zminus"; 

1029 
val zdiv_zminus1_eq_if = thm "zdiv_zminus1_eq_if"; 

1030 
val zmod_zminus1_eq_if = thm "zmod_zminus1_eq_if"; 

1031 
val zdiv_zminus2 = thm "zdiv_zminus2"; 

1032 
val zmod_zminus2 = thm "zmod_zminus2"; 

1033 
val zdiv_zminus2_eq_if = thm "zdiv_zminus2_eq_if"; 

1034 
val zmod_zminus2_eq_if = thm "zmod_zminus2_eq_if"; 

1035 
val self_quotient = thm "self_quotient"; 

1036 
val self_remainder = thm "self_remainder"; 

1037 
val zdiv_self = thm "zdiv_self"; 

1038 
val zmod_self = thm "zmod_self"; 

1039 
val zdiv_zero = thm "zdiv_zero"; 

1040 
val div_eq_minus1 = thm "div_eq_minus1"; 

1041 
val zmod_zero = thm "zmod_zero"; 

1042 
val zdiv_minus1 = thm "zdiv_minus1"; 

1043 
val zmod_minus1 = thm "zmod_minus1"; 

1044 
val div_pos_pos = thm "div_pos_pos"; 

1045 
val mod_pos_pos = thm "mod_pos_pos"; 

1046 
val div_neg_pos = thm "div_neg_pos"; 

1047 
val mod_neg_pos = thm "mod_neg_pos"; 

1048 
val div_pos_neg = thm "div_pos_neg"; 

1049 
val mod_pos_neg = thm "mod_pos_neg"; 

1050 
val div_neg_neg = thm "div_neg_neg"; 

1051 
val mod_neg_neg = thm "mod_neg_neg"; 

1052 
val zmod_1 = thm "zmod_1"; 

1053 
val zdiv_1 = thm "zdiv_1"; 

1054 
val zmod_minus1_right = thm "zmod_minus1_right"; 

1055 
val zdiv_minus1_right = thm "zdiv_minus1_right"; 

1056 
val zdiv_mono1 = thm "zdiv_mono1"; 

1057 
val zdiv_mono1_neg = thm "zdiv_mono1_neg"; 

1058 
val zdiv_mono2 = thm "zdiv_mono2"; 

1059 
val zdiv_mono2_neg = thm "zdiv_mono2_neg"; 

1060 
val zdiv_zmult1_eq = thm "zdiv_zmult1_eq"; 

1061 
val zmod_zmult1_eq = thm "zmod_zmult1_eq"; 

1062 
val zmod_zmult1_eq' = thm "zmod_zmult1_eq'"; 

1063 
val zmod_zmult_distrib = thm "zmod_zmult_distrib"; 

1064 
val zdiv_zmult_self1 = thm "zdiv_zmult_self1"; 

1065 
val zdiv_zmult_self2 = thm "zdiv_zmult_self2"; 

1066 
val zmod_zmult_self1 = thm "zmod_zmult_self1"; 

1067 
val zmod_zmult_self2 = thm "zmod_zmult_self2"; 

1068 
val zmod_eq_0_iff = thm "zmod_eq_0_iff"; 

1069 
val zdiv_zadd1_eq = thm "zdiv_zadd1_eq"; 

1070 
val zmod_zadd1_eq = thm "zmod_zadd1_eq"; 

1071 
val mod_div_trivial = thm "mod_div_trivial"; 

1072 
val mod_mod_trivial = thm "mod_mod_trivial"; 

1073 
val zmod_zadd_left_eq = thm "zmod_zadd_left_eq"; 

1074 
val zmod_zadd_right_eq = thm "zmod_zadd_right_eq"; 

1075 
val zdiv_zadd_self1 = thm "zdiv_zadd_self1"; 

1076 
val zdiv_zadd_self2 = thm "zdiv_zadd_self2"; 

1077 
val zmod_zadd_self1 = thm "zmod_zadd_self1"; 

1078 
val zmod_zadd_self2 = thm "zmod_zadd_self2"; 

1079 
val zdiv_zmult2_eq = thm "zdiv_zmult2_eq"; 

1080 
val zmod_zmult2_eq = thm "zmod_zmult2_eq"; 

1081 
val zdiv_zmult_zmult1 = thm "zdiv_zmult_zmult1"; 

1082 
val zdiv_zmult_zmult2 = thm "zdiv_zmult_zmult2"; 

1083 
val zmod_zmult_zmult1 = thm "zmod_zmult_zmult1"; 

1084 
val zmod_zmult_zmult2 = thm "zmod_zmult_zmult2"; 

1085 
val pos_zdiv_mult_2 = thm "pos_zdiv_mult_2"; 

1086 
val neg_zdiv_mult_2 = thm "neg_zdiv_mult_2"; 

1087 
val zdiv_number_of_BIT = thm "zdiv_number_of_BIT"; 

1088 
val pos_zmod_mult_2 = thm "pos_zmod_mult_2"; 

1089 
val neg_zmod_mult_2 = thm "neg_zmod_mult_2"; 

1090 
val zmod_number_of_BIT = thm "zmod_number_of_BIT"; 

1091 
val div_neg_pos_less0 = thm "div_neg_pos_less0"; 

1092 
val div_nonneg_neg_le0 = thm "div_nonneg_neg_le0"; 

1093 
val pos_imp_zdiv_nonneg_iff = thm "pos_imp_zdiv_nonneg_iff"; 

1094 
val neg_imp_zdiv_nonneg_iff = thm "neg_imp_zdiv_nonneg_iff"; 

1095 
val pos_imp_zdiv_neg_iff = thm "pos_imp_zdiv_neg_iff"; 

1096 
val neg_imp_zdiv_neg_iff = thm "neg_imp_zdiv_neg_iff"; 

1097 
*} 

1098 

6917  1099 
end 