author  wenzelm 
Tue, 18 Sep 2007 16:08:00 +0200  
changeset 24630  351a308ab58d 
parent 24490  a4c2a0ffa5be 
child 24993  92dfacb32053 
permissions  rwrr 
23164  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 
*) 

7 

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

9 

10 
theory IntDiv 

11 
imports IntArith Divides FunDef 

12 
begin 

13 

14 
constdefs 

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

16 
{*definition of quotient and remainder*} 

17 
[code func]: "quorem == %((a,b), (q,r)). 

18 
a = b*q + r & 

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

20 

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

22 
{*for the division algorithm*} 

23 
[code func]: "adjust b == %(q,r). if 0 \<le> rb then (2*q + 1, rb) 

24 
else (2*q, r)" 

25 

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

27 
function 

28 
posDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" 

29 
where 

30 
"posDivAlg a b = 

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

32 
else adjust b (posDivAlg a (2*b)))" 

33 
by auto 

34 
termination by (relation "measure (%(a,b). nat(a  b + 1))") auto 

35 

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

37 
function 

38 
negDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" 

39 
where 

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

44 
termination by (relation "measure (%(a,b). nat( a  b))") auto 

45 

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

47 
constdefs 

48 
negateSnd :: "int*int => int*int" 

49 
[code func]: "negateSnd == %(q,r). (q,r)" 

50 

51 
definition 

52 
divAlg :: "int \<times> int \<Rightarrow> int \<times> int" 

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

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

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

56 
where 

57 
"divAlg = (\<lambda>(a, b). (if 0\<le>a then 

58 
if 0\<le>b then posDivAlg a b 

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

60 
else negateSnd (negDivAlg (a) (b)) 

61 
else 

62 
if 0<b then negDivAlg a b 

63 
else negateSnd (posDivAlg (a) (b))))" 

64 

65 
instance int :: Divides.div 

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

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

68 

69 
lemma divAlg_mod_div: 

70 
"divAlg (p, q) = (p div q, p mod q)" 

71 
by (auto simp add: div_def mod_def) 

72 

73 
text{* 

74 
Here is the division algorithm in ML: 

75 

76 
\begin{verbatim} 

77 
fun posDivAlg (a,b) = 

78 
if a<b then (0,a) 

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

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

81 
end 

82 

83 
fun negDivAlg (a,b) = 

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

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

86 
in if 0\<le>rb then (2*q+1, rb) else (2*q, r) 

87 
end; 

88 

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

90 

91 
fun divAlg (a,b) = if 0\<le>a then 

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

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

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

95 
else 

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

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

98 
\end{verbatim} 

99 
*} 

100 

101 

102 

103 
subsection{*Uniqueness and Monotonicity of Quotients and Remainders*} 

104 

105 
lemma unique_quotient_lemma: 

106 
"[ b*q' + r' \<le> b*q + r; 0 \<le> r'; r' < b; r < b ] 

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

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

109 
prefer 2 apply (simp add: right_diff_distrib) 

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

111 
apply (erule_tac [2] order_le_less_trans) 

112 
prefer 2 apply (simp add: right_diff_distrib right_distrib) 

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

114 
prefer 2 apply (simp add: right_diff_distrib right_distrib) 

115 
apply (simp add: mult_less_cancel_left) 

116 
done 

117 

118 
lemma unique_quotient_lemma_neg: 

119 
"[ b*q' + r' \<le> b*q + r; r \<le> 0; b < r; b < r' ] 

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

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

122 
auto) 

123 

124 
lemma unique_quotient: 

125 
"[ quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); b \<noteq> 0 ] 

126 
==> q = q'" 

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

128 
apply (blast intro: order_antisym 

129 
dest: order_eq_refl [THEN unique_quotient_lemma] 

130 
order_eq_refl [THEN unique_quotient_lemma_neg] sym)+ 

131 
done 

132 

133 

134 
lemma unique_remainder: 

135 
"[ quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); b \<noteq> 0 ] 

136 
==> r = r'" 

137 
apply (subgoal_tac "q = q'") 

138 
apply (simp add: quorem_def) 

139 
apply (blast intro: unique_quotient) 

140 
done 

141 

142 

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

144 

145 
text{*And positive divisors*} 

146 

147 
lemma adjust_eq [simp]: 

148 
"adjust b (q,r) = 

149 
(let diff = rb in 

150 
if 0 \<le> diff then (2*q + 1, diff) 

151 
else (2*q, r))" 

152 
by (simp add: Let_def adjust_def) 

153 

154 
declare posDivAlg.simps [simp del] 

155 

156 
text{*use with a simproc to avoid repeatedly proving the premise*} 

157 
lemma posDivAlg_eqn: 

158 
"0 < b ==> 

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

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

161 

162 
text{*Correctness of @{term posDivAlg}: it computes quotients correctly*} 

163 
theorem posDivAlg_correct: 

164 
assumes "0 \<le> a" and "0 < b" 

165 
shows "quorem ((a, b), posDivAlg a b)" 

166 
using prems apply (induct a b rule: posDivAlg.induct) 

167 
apply auto 

168 
apply (simp add: quorem_def) 

169 
apply (subst posDivAlg_eqn, simp add: right_distrib) 

170 
apply (case_tac "a < b") 

171 
apply simp_all 

172 
apply (erule splitE) 

173 
apply (auto simp add: right_distrib Let_def) 

174 
done 

175 

176 

177 
subsection{*Correctness of @{term negDivAlg}, the Algorithm for Negative Dividends*} 

178 

179 
text{*And positive divisors*} 

180 

181 
declare negDivAlg.simps [simp del] 

182 

183 
text{*use with a simproc to avoid repeatedly proving the premise*} 

184 
lemma negDivAlg_eqn: 

185 
"0 < b ==> 

186 
negDivAlg a b = 

187 
(if 0\<le>a+b then (1,a+b) else adjust b (negDivAlg a (2*b)))" 

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

189 

190 
(*Correctness of negDivAlg: it computes quotients correctly 

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

192 
lemma negDivAlg_correct: 

193 
assumes "a < 0" and "b > 0" 

194 
shows "quorem ((a, b), negDivAlg a b)" 

195 
using prems apply (induct a b rule: negDivAlg.induct) 

196 
apply (auto simp add: linorder_not_le) 

197 
apply (simp add: quorem_def) 

198 
apply (subst negDivAlg_eqn, assumption) 

199 
apply (case_tac "a + b < (0\<Colon>int)") 

200 
apply simp_all 

201 
apply (erule splitE) 

202 
apply (auto simp add: right_distrib Let_def) 

203 
done 

204 

205 

206 
subsection{*Existence Shown by Proving the Division Algorithm to be Correct*} 

207 

208 
(*the case a=0*) 

209 
lemma quorem_0: "b \<noteq> 0 ==> quorem ((0,b), (0,0))" 

210 
by (auto simp add: quorem_def linorder_neq_iff) 

211 

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

213 
by (subst posDivAlg.simps, auto) 

214 

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

216 
by (subst negDivAlg.simps, auto) 

217 

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

219 
by (simp add: negateSnd_def) 

220 

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

222 
by (auto simp add: split_ifs quorem_def) 

223 

224 
lemma divAlg_correct: "b \<noteq> 0 ==> quorem ((a,b), divAlg (a, b))" 

225 
by (force simp add: linorder_neq_iff quorem_0 divAlg_def quorem_neg 

226 
posDivAlg_correct negDivAlg_correct) 

227 

228 
text{*Arbitrary definitions for division by zero. Useful to simplify 

229 
certain equations.*} 

230 

231 
lemma DIVISION_BY_ZERO [simp]: "a div (0::int) = 0 & a mod (0::int) = a" 

232 
by (simp add: div_def mod_def divAlg_def posDivAlg.simps) 

233 

234 

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

236 

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

238 
apply (case_tac "b = 0", simp) 

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

240 
apply (auto simp add: quorem_def div_def mod_def) 

241 
done 

242 

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

244 
by(simp add: zmod_zdiv_equality[symmetric]) 

245 

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

247 
by(simp add: mult_commute zmod_zdiv_equality[symmetric]) 

248 

249 
text {* Tool setup *} 

250 

251 
ML_setup {* 

252 
local 

253 

254 
structure CancelDivMod = CancelDivModFun( 

255 
struct 

256 
val div_name = @{const_name Divides.div}; 

257 
val mod_name = @{const_name Divides.mod}; 

258 
val mk_binop = HOLogic.mk_binop; 

259 
val mk_sum = Int_Numeral_Simprocs.mk_sum HOLogic.intT; 

260 
val dest_sum = Int_Numeral_Simprocs.dest_sum; 

261 
val div_mod_eqs = 

262 
map mk_meta_eq [@{thm zdiv_zmod_equality}, 

263 
@{thm zdiv_zmod_equality2}]; 

264 
val trans = trans; 

265 
val prove_eq_sums = 

266 
let 

23365  267 
val simps = @{thm diff_int_def} :: Int_Numeral_Simprocs.add_0s @ @{thms zadd_ac} 
23164  268 
in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all_tac simps) end; 
269 
end) 

270 

271 
in 

272 

273 
val cancel_zdiv_zmod_proc = NatArithUtils.prep_simproc 

274 
("cancel_zdiv_zmod", ["(m::int) + n"], K CancelDivMod.proc) 

275 

276 
end; 

277 

278 
Addsimprocs [cancel_zdiv_zmod_proc] 

279 
*} 

280 

281 
lemma pos_mod_conj : "(0::int) < b ==> 0 \<le> a mod b & a mod b < b" 

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

283 
apply (auto simp add: quorem_def mod_def) 

284 
done 

285 

286 
lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1, standard] 

287 
and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2, standard] 

288 

289 
lemma neg_mod_conj : "b < (0::int) ==> a mod b \<le> 0 & b < a mod b" 

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

291 
apply (auto simp add: quorem_def div_def mod_def) 

292 
done 

293 

294 
lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1, standard] 

295 
and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2, standard] 

296 

297 

298 

299 
subsection{*General Properties of div and mod*} 

300 

301 
lemma quorem_div_mod: "b \<noteq> 0 ==> quorem ((a, b), (a div b, a mod b))" 

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

303 
apply (force simp add: quorem_def linorder_neq_iff) 

304 
done 

305 

306 
lemma quorem_div: "[ quorem((a,b),(q,r)); b \<noteq> 0 ] ==> a div b = q" 

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

308 

309 
lemma quorem_mod: "[ quorem((a,b),(q,r)); b \<noteq> 0 ] ==> a mod b = r" 

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

311 

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

313 
apply (rule quorem_div) 

314 
apply (auto simp add: quorem_def) 

315 
done 

316 

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

318 
apply (rule quorem_div) 

319 
apply (auto simp add: quorem_def) 

320 
done 

321 

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

323 
apply (rule quorem_div) 

324 
apply (auto simp add: quorem_def) 

325 
done 

326 

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

328 

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

330 
apply (rule_tac q = 0 in quorem_mod) 

331 
apply (auto simp add: quorem_def) 

332 
done 

333 

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

335 
apply (rule_tac q = 0 in quorem_mod) 

336 
apply (auto simp add: quorem_def) 

337 
done 

338 

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

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

341 
apply (auto simp add: quorem_def) 

342 
done 

343 

344 
text{*There is no @{text mod_neg_pos_trivial}.*} 

345 

346 

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

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

349 
apply (case_tac "b = 0", simp) 

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

351 
THEN quorem_div, THEN sym]) 

352 

353 
done 

354 

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

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

357 
apply (case_tac "b = 0", simp) 

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

359 
auto) 

360 
done 

361 

362 

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

364 

365 
lemma zminus1_lemma: 

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

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

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

369 
by (force simp add: split_ifs quorem_def linorder_neq_iff right_diff_distrib) 

370 

371 

372 
lemma zdiv_zminus1_eq_if: 

373 
"b \<noteq> (0::int) 

374 
==> (a) div b = 

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

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

377 

378 
lemma zmod_zminus1_eq_if: 

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

380 
apply (case_tac "b = 0", simp) 

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

382 
done 

383 

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

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

386 

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

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

389 

390 
lemma zdiv_zminus2_eq_if: 

391 
"b \<noteq> (0::int) 

392 
==> a div (b) = 

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

394 
by (simp add: zdiv_zminus1_eq_if zdiv_zminus2) 

395 

396 
lemma zmod_zminus2_eq_if: 

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

398 
by (simp add: zmod_zminus1_eq_if zmod_zminus2) 

399 

400 

401 
subsection{*Division of a Number by Itself*} 

402 

403 
lemma self_quotient_aux1: "[ (0::int) < a; a = r + a*q; r < a ] ==> 1 \<le> q" 

404 
apply (subgoal_tac "0 < a*q") 

405 
apply (simp add: zero_less_mult_iff, arith) 

406 
done 

407 

408 
lemma self_quotient_aux2: "[ (0::int) < a; a = r + a*q; 0 \<le> r ] ==> q \<le> 1" 

409 
apply (subgoal_tac "0 \<le> a* (1q) ") 

410 
apply (simp add: zero_le_mult_iff) 

411 
apply (simp add: right_diff_distrib) 

412 
done 

413 

414 
lemma self_quotient: "[ quorem((a,a),(q,r)); a \<noteq> (0::int) ] ==> q = 1" 

415 
apply (simp add: split_ifs quorem_def linorder_neq_iff) 

416 
apply (rule order_antisym, safe, simp_all) 

417 
apply (rule_tac [3] a = "a" and r = "r" in self_quotient_aux1) 

418 
apply (rule_tac a = "a" and r = "r" in self_quotient_aux2) 

419 
apply (force intro: self_quotient_aux1 self_quotient_aux2 simp add: add_commute)+ 

420 
done 

421 

422 
lemma self_remainder: "[ quorem((a,a),(q,r)); a \<noteq> (0::int) ] ==> r = 0" 

423 
apply (frule self_quotient, assumption) 

424 
apply (simp add: quorem_def) 

425 
done 

426 

427 
lemma zdiv_self [simp]: "a \<noteq> 0 ==> a div a = (1::int)" 

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

429 

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

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

432 
apply (case_tac "a = 0", simp) 

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

434 
done 

435 

436 

437 
subsection{*Computation of Division and Remainder*} 

438 

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

440 
by (simp add: div_def divAlg_def) 

441 

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

443 
by (simp add: div_def divAlg_def) 

444 

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

446 
by (simp add: mod_def divAlg_def) 

447 

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

449 
by (simp add: div_def divAlg_def) 

450 

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

452 
by (simp add: mod_def divAlg_def) 

453 

454 
text{*a positive, b positive *} 

455 

456 
lemma div_pos_pos: "[ 0 < a; 0 \<le> b ] ==> a div b = fst (posDivAlg a b)" 

457 
by (simp add: div_def divAlg_def) 

458 

459 
lemma mod_pos_pos: "[ 0 < a; 0 \<le> b ] ==> a mod b = snd (posDivAlg a b)" 

460 
by (simp add: mod_def divAlg_def) 

461 

462 
text{*a negative, b positive *} 

463 

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

465 
by (simp add: div_def divAlg_def) 

466 

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

468 
by (simp add: mod_def divAlg_def) 

469 

470 
text{*a positive, b negative *} 

471 

472 
lemma div_pos_neg: 

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

474 
by (simp add: div_def divAlg_def) 

475 

476 
lemma mod_pos_neg: 

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

478 
by (simp add: mod_def divAlg_def) 

479 

480 
text{*a negative, b negative *} 

481 

482 
lemma div_neg_neg: 

483 
"[ a < 0; b \<le> 0 ] ==> a div b = fst (negateSnd (posDivAlg (a) (b)))" 

484 
by (simp add: div_def divAlg_def) 

485 

486 
lemma mod_neg_neg: 

487 
"[ a < 0; b \<le> 0 ] ==> a mod b = snd (negateSnd (posDivAlg (a) (b)))" 

488 
by (simp add: mod_def divAlg_def) 

489 

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

491 

24481  492 
lemma quoremI: 
493 
"\<lbrakk>a == b * q + r; if 0 < b then 0 \<le> r \<and> r < b else b < r \<and> r \<le> 0\<rbrakk> 

494 
\<Longrightarrow> quorem ((a, b), (q, r))" 

495 
unfolding quorem_def by simp 

496 

497 
lemmas quorem_div_eq = quoremI [THEN quorem_div, THEN eq_reflection] 

498 
lemmas quorem_mod_eq = quoremI [THEN quorem_mod, THEN eq_reflection] 

499 
lemmas arithmetic_simps = 

500 
arith_simps 

501 
add_special 

502 
OrderedGroup.add_0_left 

503 
OrderedGroup.add_0_right 

504 
mult_zero_left 

505 
mult_zero_right 

506 
mult_1_left 

507 
mult_1_right 

508 

509 
(* simprocs adapted from HOL/ex/Binary.thy *) 

510 
ML {* 

511 
local 

512 
infix ==; 

513 
val op == = Logic.mk_equals; 

514 
fun plus m n = @{term "plus :: int \<Rightarrow> int \<Rightarrow> int"} $ m $ n; 

515 
fun mult m n = @{term "times :: int \<Rightarrow> int \<Rightarrow> int"} $ m $ n; 

516 

517 
val binary_ss = HOL_basic_ss addsimps @{thms arithmetic_simps}; 

518 
fun prove ctxt prop = 

519 
Goal.prove ctxt [] [] prop (fn _ => ALLGOALS (full_simp_tac binary_ss)); 

520 

521 
fun binary_proc proc ss ct = 

522 
(case Thm.term_of ct of 

523 
_ $ t $ u => 

524 
(case try (pairself (`(snd o HOLogic.dest_number))) (t, u) of 

525 
SOME args => proc (Simplifier.the_context ss) args 

526 
 NONE => NONE) 

527 
 _ => NONE); 

528 
in 

529 

530 
fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) => 

531 
if n = 0 then NONE 

532 
else 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24490
diff
changeset

533 
let val (k, l) = Integer.div_mod m n; 
24481  534 
fun mk_num x = HOLogic.mk_number HOLogic.intT x; 
535 
in SOME (rule OF [prove ctxt (t == plus (mult u (mk_num k)) (mk_num l))]) 

536 
end); 

537 

538 
end; 

539 
*} 

540 

541 
simproc_setup binary_int_div ("number_of m div number_of n :: int") = 

542 
{* K (divmod_proc (@{thm quorem_div_eq})) *} 

543 

544 
simproc_setup binary_int_mod ("number_of m mod number_of n :: int") = 

545 
{* K (divmod_proc (@{thm quorem_mod_eq})) *} 

546 

547 
(* The following 8 lemmas are made unnecessary by the above simprocs: *) 

548 

549 
lemmas div_pos_pos_number_of = 

23164  550 
div_pos_pos [of "number_of v" "number_of w", standard] 
551 

24481  552 
lemmas div_neg_pos_number_of = 
23164  553 
div_neg_pos [of "number_of v" "number_of w", standard] 
554 

24481  555 
lemmas div_pos_neg_number_of = 
23164  556 
div_pos_neg [of "number_of v" "number_of w", standard] 
557 

24481  558 
lemmas div_neg_neg_number_of = 
23164  559 
div_neg_neg [of "number_of v" "number_of w", standard] 
560 

561 

24481  562 
lemmas mod_pos_pos_number_of = 
23164  563 
mod_pos_pos [of "number_of v" "number_of w", standard] 
564 

24481  565 
lemmas mod_neg_pos_number_of = 
23164  566 
mod_neg_pos [of "number_of v" "number_of w", standard] 
567 

24481  568 
lemmas mod_pos_neg_number_of = 
23164  569 
mod_pos_neg [of "number_of v" "number_of w", standard] 
570 

24481  571 
lemmas mod_neg_neg_number_of = 
23164  572 
mod_neg_neg [of "number_of v" "number_of w", standard] 
573 

574 

575 
lemmas posDivAlg_eqn_number_of [simp] = 

576 
posDivAlg_eqn [of "number_of v" "number_of w", standard] 

577 

578 
lemmas negDivAlg_eqn_number_of [simp] = 

579 
negDivAlg_eqn [of "number_of v" "number_of w", standard] 

580 

581 

582 
text{*Specialcase simplification *} 

583 

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

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

586 
apply (cut_tac [2] a = a and b = 1 in pos_mod_bound) 

587 
apply (auto simp del:pos_mod_bound pos_mod_sign) 

588 
done 

589 

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

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

592 

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

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

595 
apply (cut_tac [2] a = a and b = "1" in neg_mod_bound) 

596 
apply (auto simp del: neg_mod_sign neg_mod_bound) 

597 
done 

598 

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

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

601 

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

603 
1 div z and 1 mod z **) 

604 

605 
lemmas div_pos_pos_1_number_of [simp] = 

606 
div_pos_pos [OF int_0_less_1, of "number_of w", standard] 

607 

608 
lemmas div_pos_neg_1_number_of [simp] = 

609 
div_pos_neg [OF int_0_less_1, of "number_of w", standard] 

610 

611 
lemmas mod_pos_pos_1_number_of [simp] = 

612 
mod_pos_pos [OF int_0_less_1, of "number_of w", standard] 

613 

614 
lemmas mod_pos_neg_1_number_of [simp] = 

615 
mod_pos_neg [OF int_0_less_1, of "number_of w", standard] 

616 

617 

618 
lemmas posDivAlg_eqn_1_number_of [simp] = 

619 
posDivAlg_eqn [of concl: 1 "number_of w", standard] 

620 

621 
lemmas negDivAlg_eqn_1_number_of [simp] = 

622 
negDivAlg_eqn [of concl: 1 "number_of w", standard] 

623 

624 

625 

626 
subsection{*Monotonicity in the First Argument (Dividend)*} 

627 

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

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

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

631 
apply (rule unique_quotient_lemma) 

632 
apply (erule subst) 

633 
apply (erule subst, simp_all) 

634 
done 

635 

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

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

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

639 
apply (rule unique_quotient_lemma_neg) 

640 
apply (erule subst) 

641 
apply (erule subst, simp_all) 

642 
done 

643 

644 

645 
subsection{*Monotonicity in the Second Argument (Divisor)*} 

646 

647 
lemma q_pos_lemma: 

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

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

650 
apply (simp add: zero_less_mult_iff) 

651 
apply (simp add: right_distrib) 

652 
done 

653 

654 
lemma zdiv_mono2_lemma: 

655 
"[ b*q + r = b'*q' + r'; 0 \<le> b'*q' + r'; 

656 
r' < b'; 0 \<le> r; 0 < b'; b' \<le> b ] 

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

658 
apply (frule q_pos_lemma, assumption+) 

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

660 
apply (simp add: mult_less_cancel_left) 

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

662 
prefer 2 apply simp 

663 
apply (simp (no_asm_simp) add: right_distrib) 

664 
apply (subst add_commute, rule zadd_zless_mono, arith) 

665 
apply (rule mult_right_mono, auto) 

666 
done 

667 

668 
lemma zdiv_mono2: 

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

670 
apply (subgoal_tac "b \<noteq> 0") 

671 
prefer 2 apply arith 

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

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

674 
apply (rule zdiv_mono2_lemma) 

675 
apply (erule subst) 

676 
apply (erule subst, simp_all) 

677 
done 

678 

679 
lemma q_neg_lemma: 

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

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

682 
apply (simp add: mult_less_0_iff, arith) 

683 
done 

684 

685 
lemma zdiv_mono2_neg_lemma: 

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

687 
r < b; 0 \<le> r'; 0 < b'; b' \<le> b ] 

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

689 
apply (frule q_neg_lemma, assumption+) 

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

691 
apply (simp add: mult_less_cancel_left) 

692 
apply (simp add: right_distrib) 

693 
apply (subgoal_tac "b*q' \<le> b'*q'") 

694 
prefer 2 apply (simp add: mult_right_mono_neg, arith) 

695 
done 

696 

697 
lemma zdiv_mono2_neg: 

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

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

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

701 
apply (rule zdiv_mono2_neg_lemma) 

702 
apply (erule subst) 

703 
apply (erule subst, simp_all) 

704 
done 

705 

706 
subsection{*More Algebraic Laws for div and mod*} 

707 

708 
text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *} 

709 

710 
lemma zmult1_lemma: 

711 
"[ quorem((b,c),(q,r)); c \<noteq> 0 ] 

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

713 
by (force simp add: split_ifs quorem_def linorder_neq_iff right_distrib) 

714 

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

716 
apply (case_tac "c = 0", simp) 

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

718 
done 

719 

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

721 
apply (case_tac "c = 0", simp) 

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

723 
done 

724 

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

726 
apply (rule trans) 

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

728 
apply (rule_tac [2] zmod_zmult1_eq) 

729 
apply (simp_all add: mult_commute) 

730 
done 

731 

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

733 
apply (rule zmod_zmult1_eq' [THEN trans]) 

734 
apply (rule zmod_zmult1_eq) 

735 
done 

736 

737 
lemma zdiv_zmult_self1 [simp]: "b \<noteq> (0::int) ==> (a*b) div b = a" 

738 
by (simp add: zdiv_zmult1_eq) 

739 

740 
lemma zdiv_zmult_self2 [simp]: "b \<noteq> (0::int) ==> (b*a) div b = a" 

741 
by (subst mult_commute, erule zdiv_zmult_self1) 

742 

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

744 
by (simp add: zmod_zmult1_eq) 

745 

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

747 
by (simp add: mult_commute zmod_zmult1_eq) 

748 

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

750 
proof 

751 
assume "m mod d = 0" 

752 
with zmod_zdiv_equality[of m d] show "EX q::int. m = d*q" by auto 

753 
next 

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

755 
thus "m mod d = 0" by auto 

756 
qed 

757 

758 
lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1] 

759 

760 
text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *} 

761 

762 
lemma zadd1_lemma: 

763 
"[ quorem((a,c),(aq,ar)); quorem((b,c),(bq,br)); c \<noteq> 0 ] 

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

765 
by (force simp add: split_ifs quorem_def linorder_neq_iff right_distrib) 

766 

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

768 
lemma zdiv_zadd1_eq: 

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

770 
apply (case_tac "c = 0", simp) 

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

772 
done 

773 

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

775 
apply (case_tac "c = 0", simp) 

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

777 
done 

778 

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

780 
apply (case_tac "b = 0", simp) 

781 
apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial) 

782 
done 

783 

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

785 
apply (case_tac "b = 0", simp) 

786 
apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial) 

787 
done 

788 

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

790 
apply (rule trans [symmetric]) 

791 
apply (rule zmod_zadd1_eq, simp) 

792 
apply (rule zmod_zadd1_eq [symmetric]) 

793 
done 

794 

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

796 
apply (rule trans [symmetric]) 

797 
apply (rule zmod_zadd1_eq, simp) 

798 
apply (rule zmod_zadd1_eq [symmetric]) 

799 
done 

800 

801 
lemma zdiv_zadd_self1[simp]: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1" 

802 
by (simp add: zdiv_zadd1_eq) 

803 

804 
lemma zdiv_zadd_self2[simp]: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1" 

805 
by (simp add: zdiv_zadd1_eq) 

806 

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

808 
apply (case_tac "a = 0", simp) 

809 
apply (simp add: zmod_zadd1_eq) 

810 
done 

811 

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

813 
apply (case_tac "a = 0", simp) 

814 
apply (simp add: zmod_zadd1_eq) 

815 
done 

816 

817 

23983  818 
lemma zmod_zdiff1_eq: fixes a::int 
819 
shows "(a  b) mod c = (a mod c  b mod c) mod c" (is "?l = ?r") 

820 
proof  

821 
have "?l = (c + (a mod c  b mod c)) mod c" 

822 
using zmod_zadd1_eq[of a "b" c] by(simp add:ring_simps zmod_zminus1_eq_if) 

823 
also have "\<dots> = ?r" by simp 

824 
finally show ?thesis . 

825 
qed 

826 

23164  827 
subsection{*Proving @{term "a div (b*c) = (a div b) div c"} *} 
828 

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

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

831 
to cause particular problems.*) 

832 

833 
text{*first, four lemmas to bound the remainder for the cases b<0 and b>0 *} 

834 

835 
lemma zmult2_lemma_aux1: "[ (0::int) < c; b < r; r \<le> 0 ] ==> b*c < b*(q mod c) + r" 

836 
apply (subgoal_tac "b * (c  q mod c) < r * 1") 

837 
apply (simp add: right_diff_distrib) 

838 
apply (rule order_le_less_trans) 

839 
apply (erule_tac [2] mult_strict_right_mono) 

840 
apply (rule mult_left_mono_neg) 

841 
apply (auto simp add: compare_rls add_commute [of 1] 

842 
add1_zle_eq pos_mod_bound) 

843 
done 

844 

845 
lemma zmult2_lemma_aux2: 

846 
"[ (0::int) < c; b < r; r \<le> 0 ] ==> b * (q mod c) + r \<le> 0" 

847 
apply (subgoal_tac "b * (q mod c) \<le> 0") 

848 
apply arith 

849 
apply (simp add: mult_le_0_iff) 

850 
done 

851 

852 
lemma zmult2_lemma_aux3: "[ (0::int) < c; 0 \<le> r; r < b ] ==> 0 \<le> b * (q mod c) + r" 

853 
apply (subgoal_tac "0 \<le> b * (q mod c) ") 

854 
apply arith 

855 
apply (simp add: zero_le_mult_iff) 

856 
done 

857 

858 
lemma zmult2_lemma_aux4: "[ (0::int) < c; 0 \<le> r; r < b ] ==> b * (q mod c) + r < b * c" 

859 
apply (subgoal_tac "r * 1 < b * (c  q mod c) ") 

860 
apply (simp add: right_diff_distrib) 

861 
apply (rule order_less_le_trans) 

862 
apply (erule mult_strict_right_mono) 

863 
apply (rule_tac [2] mult_left_mono) 

864 
apply (auto simp add: compare_rls add_commute [of 1] 

865 
add1_zle_eq pos_mod_bound) 

866 
done 

867 

868 
lemma zmult2_lemma: "[ quorem ((a,b), (q,r)); b \<noteq> 0; 0 < c ] 

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

870 
by (auto simp add: mult_ac quorem_def linorder_neq_iff 

871 
zero_less_mult_iff right_distrib [symmetric] 

872 
zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4) 

873 

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

875 
apply (case_tac "b = 0", simp) 

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

877 
done 

878 

879 
lemma zmod_zmult2_eq: 

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

881 
apply (case_tac "b = 0", simp) 

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

883 
done 

884 

885 

886 
subsection{*Cancellation of Common Factors in div*} 

887 

888 
lemma zdiv_zmult_zmult1_aux1: 

889 
"[ (0::int) < b; c \<noteq> 0 ] ==> (c*a) div (c*b) = a div b" 

890 
by (subst zdiv_zmult2_eq, auto) 

891 

892 
lemma zdiv_zmult_zmult1_aux2: 

893 
"[ b < (0::int); c \<noteq> 0 ] ==> (c*a) div (c*b) = a div b" 

894 
apply (subgoal_tac " (c * (a)) div (c * (b)) = (a) div (b) ") 

895 
apply (rule_tac [2] zdiv_zmult_zmult1_aux1, auto) 

896 
done 

897 

898 
lemma zdiv_zmult_zmult1: "c \<noteq> (0::int) ==> (c*a) div (c*b) = a div b" 

899 
apply (case_tac "b = 0", simp) 

900 
apply (auto simp add: linorder_neq_iff zdiv_zmult_zmult1_aux1 zdiv_zmult_zmult1_aux2) 

901 
done 

902 

23401  903 
lemma zdiv_zmult_zmult1_if[simp]: 
904 
"(k*m) div (k*n) = (if k = (0::int) then 0 else m div n)" 

905 
by (simp add:zdiv_zmult_zmult1) 

906 

907 
(* 

23164  908 
lemma zdiv_zmult_zmult2: "c \<noteq> (0::int) ==> (a*c) div (b*c) = a div b" 
909 
apply (drule zdiv_zmult_zmult1) 

910 
apply (auto simp add: mult_commute) 

911 
done 

23401  912 
*) 
23164  913 

914 

915 
subsection{*Distribution of Factors over mod*} 

916 

917 
lemma zmod_zmult_zmult1_aux1: 

918 
"[ (0::int) < b; c \<noteq> 0 ] ==> (c*a) mod (c*b) = c * (a mod b)" 

919 
by (subst zmod_zmult2_eq, auto) 

920 

921 
lemma zmod_zmult_zmult1_aux2: 

922 
"[ b < (0::int); c \<noteq> 0 ] ==> (c*a) mod (c*b) = c * (a mod b)" 

923 
apply (subgoal_tac " (c * (a)) mod (c * (b)) = c * ((a) mod (b))") 

924 
apply (rule_tac [2] zmod_zmult_zmult1_aux1, auto) 

925 
done 

926 

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

928 
apply (case_tac "b = 0", simp) 

929 
apply (case_tac "c = 0", simp) 

930 
apply (auto simp add: linorder_neq_iff zmod_zmult_zmult1_aux1 zmod_zmult_zmult1_aux2) 

931 
done 

932 

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

934 
apply (cut_tac c = c in zmod_zmult_zmult1) 

935 
apply (auto simp add: mult_commute) 

936 
done 

937 

24490  938 
lemma zmod_zmod_cancel: 
939 
assumes "n dvd m" shows "(k::int) mod m mod n = k mod n" 

940 
proof  

941 
from `n dvd m` obtain r where "m = n*r" by(auto simp:dvd_def) 

942 
have "k mod n = (m * (k div m) + k mod m) mod n" 

943 
using zmod_zdiv_equality[of k m] by simp 

944 
also have "\<dots> = (m * (k div m) mod n + k mod m mod n) mod n" 

945 
by(subst zmod_zadd1_eq, rule refl) 

946 
also have "m * (k div m) mod n = 0" using `m = n*r` 

947 
by(simp add:mult_ac) 

948 
finally show ?thesis by simp 

949 
qed 

950 

23164  951 

952 
subsection {*Splitting Rules for div and mod*} 

953 

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

955 

956 
lemma split_pos_lemma: 

957 
"0<k ==> 

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

959 
apply (rule iffI, clarify) 

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

961 
apply (subst zmod_zadd1_eq) 

962 
apply (subst zdiv_zadd1_eq) 

963 
apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial) 

964 
txt{*converse direction*} 

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

966 
apply (drule_tac x = "n mod k" in spec, simp) 

967 
done 

968 

969 
lemma split_neg_lemma: 

970 
"k<0 ==> 

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

972 
apply (rule iffI, clarify) 

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

974 
apply (subst zmod_zadd1_eq) 

975 
apply (subst zdiv_zadd1_eq) 

976 
apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial) 

977 
txt{*converse direction*} 

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

979 
apply (drule_tac x = "n mod k" in spec, simp) 

980 
done 

981 

982 
lemma split_zdiv: 

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

984 
((k = 0 > P 0) & 

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

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

987 
apply (case_tac "k=0", simp) 

988 
apply (simp only: linorder_neq_iff) 

989 
apply (erule disjE) 

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

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

992 
done 

993 

994 
lemma split_zmod: 

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

996 
((k = 0 > P n) & 

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

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

999 
apply (case_tac "k=0", simp) 

1000 
apply (simp only: linorder_neq_iff) 

1001 
apply (erule disjE) 

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

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

1004 
done 

1005 

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

1007 
declare split_zdiv [of _ _ "number_of k", simplified, standard, arith_split] 

1008 
declare split_zmod [of _ _ "number_of k", simplified, standard, arith_split] 

1009 

1010 

1011 
subsection{*Speeding up the Division Algorithm with Shifting*} 

1012 

1013 
text{*computing div by shifting *} 

1014 

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

1016 
proof cases 

1017 
assume "a=0" 

1018 
thus ?thesis by simp 

1019 
next 

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

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

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

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

1024 
by (simp add: mult_le_cancel_left add_commute [of 1] add1_zle_eq) 

1025 
with a_pos have "0 \<le> b mod a" by simp 

1026 
hence le_addm: "0 \<le> 1 mod (2*a) + 2*(b mod a)" 

1027 
by (simp add: mod_pos_pos_trivial one_less_a2) 

1028 
with le_2a 

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

1030 
by (simp add: div_pos_pos_trivial le_addm mod_pos_pos_trivial one_less_a2 

1031 
right_distrib) 

1032 
thus ?thesis 

1033 
by (subst zdiv_zadd1_eq, 

1034 
simp add: zdiv_zmult_zmult1 zmod_zmult_zmult1 one_less_a2 

1035 
div_pos_pos_trivial) 

1036 
qed 

1037 

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

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

1040 
apply (rule_tac [2] pos_zdiv_mult_2) 

1041 
apply (auto simp add: minus_mult_right [symmetric] right_diff_distrib) 

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

1043 
apply (simp only: zdiv_zminus_zminus diff_minus minus_add_distrib [symmetric], 

1044 
simp) 

1045 
done 

1046 

1047 

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

1049 
simplification problems*) 

1050 
lemma not_0_le_lemma: "~ 0 \<le> x ==> x \<le> (0::int)" 

1051 
by auto 

1052 

1053 
lemma zdiv_number_of_BIT[simp]: 

1054 
"number_of (v BIT b) div number_of (w BIT bit.B0) = 

1055 
(if b=bit.B0  (0::int) \<le> number_of w 

1056 
then number_of v div (number_of w) 

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

1058 
apply (simp only: number_of_eq numeral_simps UNIV_I split: split_if) 

1059 
apply (simp add: zdiv_zmult_zmult1 pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac 

1060 
split: bit.split) 

1061 
done 

1062 

1063 

1064 
subsection{*Computing mod by Shifting (proofs resemble those for div)*} 

1065 

1066 
lemma pos_zmod_mult_2: 

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

1068 
apply (case_tac "a = 0", simp) 

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

1070 
prefer 2 apply arith 

1071 
apply (subgoal_tac "2* (1 + b mod a) \<le> 2*a") 

1072 
apply (rule_tac [2] mult_left_mono) 

1073 
apply (auto simp add: add_commute [of 1] mult_commute add1_zle_eq 

1074 
pos_mod_bound) 

1075 
apply (subst zmod_zadd1_eq) 

1076 
apply (simp add: zmod_zmult_zmult2 mod_pos_pos_trivial) 

1077 
apply (rule mod_pos_pos_trivial) 

1078 
apply (auto simp add: mod_pos_pos_trivial left_distrib) 

1079 
apply (subgoal_tac "0 \<le> b mod a", arith, simp) 

1080 
done 

1081 

1082 
lemma neg_zmod_mult_2: 

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

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

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

1086 
apply (rule_tac [2] pos_zmod_mult_2) 

1087 
apply (auto simp add: minus_mult_right [symmetric] right_diff_distrib) 

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

1089 
prefer 2 apply simp 

1090 
apply (simp only: zmod_zminus_zminus diff_minus minus_add_distrib [symmetric]) 

1091 
done 

1092 

1093 
lemma zmod_number_of_BIT [simp]: 

1094 
"number_of (v BIT b) mod number_of (w BIT bit.B0) = 

1095 
(case b of 

1096 
bit.B0 => 2 * (number_of v mod number_of w) 

1097 
 bit.B1 => if (0::int) \<le> number_of w 

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

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

1100 
apply (simp only: number_of_eq numeral_simps UNIV_I split: bit.split) 

1101 
apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2 

1102 
not_0_le_lemma neg_zmod_mult_2 add_ac) 

1103 
done 

1104 

1105 

1106 
subsection{*Quotients of Signs*} 

1107 

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

1109 
apply (subgoal_tac "a div b \<le> 1", force) 

1110 
apply (rule order_trans) 

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

1112 
apply (auto simp add: zdiv_minus1) 

1113 
done 

1114 

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

1116 
by (drule zdiv_mono1_neg, auto) 

1117 

1118 
lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \<le> a div b) = (0 \<le> a)" 

1119 
apply auto 

1120 
apply (drule_tac [2] zdiv_mono1) 

1121 
apply (auto simp add: linorder_neq_iff) 

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

1123 
apply (blast intro: div_neg_pos_less0) 

1124 
done 

1125 

1126 
lemma neg_imp_zdiv_nonneg_iff: 

1127 
"b < (0::int) ==> (0 \<le> a div b) = (a \<le> (0::int))" 

1128 
apply (subst zdiv_zminus_zminus [symmetric]) 

1129 
apply (subst pos_imp_zdiv_nonneg_iff, auto) 

1130 
done 

1131 

1132 
(*But not (a div b \<le> 0 iff a\<le>0); consider a=1, b=2 when a div b = 0.*) 

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

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

1135 

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

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

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

1139 

1140 

1141 
subsection {* The Divides Relation *} 

1142 

1143 
lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))" 

23512  1144 
by (simp add: dvd_def zmod_eq_0_iff) 
1145 

23684
8c508c4dc53b
introduced (auxiliary) class dvd_mod for more convenient code generation
haftmann
parents:
23512
diff
changeset

1146 
instance int :: dvd_mod 
8c508c4dc53b
introduced (auxiliary) class dvd_mod for more convenient code generation
haftmann
parents:
23512
diff
changeset

1147 
by default (simp add: times_class.dvd [symmetric] zdvd_iff_zmod_eq_0) 
23164  1148 

1149 
lemmas zdvd_iff_zmod_eq_0_number_of [simp] = 

1150 
zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard] 

1151 

1152 
lemma zdvd_0_right [iff]: "(m::int) dvd 0" 

23512  1153 
by (simp add: dvd_def) 
23164  1154 

24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24195
diff
changeset

1155 
lemma zdvd_0_left [iff,noatp]: "(0 dvd (m::int)) = (m = 0)" 
23164  1156 
by (simp add: dvd_def) 
1157 

1158 
lemma zdvd_1_left [iff]: "1 dvd (m::int)" 

1159 
by (simp add: dvd_def) 

1160 

1161 
lemma zdvd_refl [simp]: "m dvd (m::int)" 

23512  1162 
by (auto simp add: dvd_def intro: zmult_1_right [symmetric]) 
23164  1163 

1164 
lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)" 

23512  1165 
by (auto simp add: dvd_def intro: mult_assoc) 
23164  1166 

1167 
lemma zdvd_zminus_iff: "(m dvd n) = (m dvd (n::int))" 

1168 
apply (simp add: dvd_def, auto) 

1169 
apply (rule_tac [!] x = "k" in exI, auto) 

1170 
done 

1171 

1172 
lemma zdvd_zminus2_iff: "(m dvd n) = (m dvd (n::int))" 

1173 
apply (simp add: dvd_def, auto) 

1174 
apply (rule_tac [!] x = "k" in exI, auto) 

1175 
done 

1176 
lemma zdvd_abs1: "( \<bar>i::int\<bar> dvd j) = (i dvd j)" 

1177 
apply (cases "i > 0", simp) 

1178 
apply (simp add: dvd_def) 

1179 
apply (rule iffI) 

1180 
apply (erule exE) 

1181 
apply (rule_tac x=" k" in exI, simp) 

1182 
apply (erule exE) 

1183 
apply (rule_tac x=" k" in exI, simp) 

1184 
done 

1185 
lemma zdvd_abs2: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)" 

1186 
apply (cases "j > 0", simp) 

1187 
apply (simp add: dvd_def) 

1188 
apply (rule iffI) 

1189 
apply (erule exE) 

1190 
apply (rule_tac x=" k" in exI, simp) 

1191 
apply (erule exE) 

1192 
apply (rule_tac x=" k" in exI, simp) 

1193 
done 

1194 

1195 
lemma zdvd_anti_sym: 

1196 
"0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)" 

1197 
apply (simp add: dvd_def, auto) 

1198 
apply (simp add: mult_assoc zero_less_mult_iff zmult_eq_1_iff) 

1199 
done 

1200 

1201 
lemma zdvd_zadd: "k dvd m ==> k dvd n ==> k dvd (m + n :: int)" 

1202 
apply (simp add: dvd_def) 

1203 
apply (blast intro: right_distrib [symmetric]) 

1204 
done 

1205 

1206 
lemma zdvd_dvd_eq: assumes anz:"a \<noteq> 0" and ab: "(a::int) dvd b" and ba:"b dvd a" 

1207 
shows "\<bar>a\<bar> = \<bar>b\<bar>" 

1208 
proof 

1209 
from ab obtain k where k:"b = a*k" unfolding dvd_def by blast 

1210 
from ba obtain k' where k':"a = b*k'" unfolding dvd_def by blast 

1211 
from k k' have "a = a*k*k'" by simp 

1212 
with mult_cancel_left1[where c="a" and b="k*k'"] 

1213 
have kk':"k*k' = 1" using anz by (simp add: mult_assoc) 

1214 
hence "k = 1 \<and> k' = 1 \<or> k = 1 \<and> k' = 1" by (simp add: zmult_eq_1_iff) 

1215 
thus ?thesis using k k' by auto 

1216 
qed 

1217 

1218 
lemma zdvd_zdiff: "k dvd m ==> k dvd n ==> k dvd (m  n :: int)" 

1219 
apply (simp add: dvd_def) 

1220 
apply (blast intro: right_diff_distrib [symmetric]) 

1221 
done 

1222 

1223 
lemma zdvd_zdiffD: "k dvd m  n ==> k dvd n ==> k dvd (m::int)" 

1224 
apply (subgoal_tac "m = n + (m  n)") 

1225 
apply (erule ssubst) 

1226 
apply (blast intro: zdvd_zadd, simp) 

1227 
done 

1228 

1229 
lemma zdvd_zmult: "k dvd (n::int) ==> k dvd m * n" 

1230 
apply (simp add: dvd_def) 

1231 
apply (blast intro: mult_left_commute) 

1232 
done 

1233 

1234 
lemma zdvd_zmult2: "k dvd (m::int) ==> k dvd m * n" 

1235 
apply (subst mult_commute) 

1236 
apply (erule zdvd_zmult) 

1237 
done 

1238 

1239 
lemma zdvd_triv_right [iff]: "(k::int) dvd m * k" 

1240 
apply (rule zdvd_zmult) 

1241 
apply (rule zdvd_refl) 

1242 
done 

1243 

1244 
lemma zdvd_triv_left [iff]: "(k::int) dvd k * m" 

1245 
apply (rule zdvd_zmult2) 

1246 
apply (rule zdvd_refl) 

1247 
done 

1248 

1249 
lemma zdvd_zmultD2: "j * k dvd n ==> j dvd (n::int)" 

1250 
apply (simp add: dvd_def) 

1251 
apply (simp add: mult_assoc, blast) 

1252 
done 

1253 

1254 
lemma zdvd_zmultD: "j * k dvd n ==> k dvd (n::int)" 

1255 
apply (rule zdvd_zmultD2) 

1256 
apply (subst mult_commute, assumption) 

1257 
done 

1258 

1259 
lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n" 

1260 
apply (simp add: dvd_def, clarify) 

1261 
apply (rule_tac x = "k * ka" in exI) 

1262 
apply (simp add: mult_ac) 

1263 
done 

1264 

1265 
lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))" 

1266 
apply (rule iffI) 

1267 
apply (erule_tac [2] zdvd_zadd) 

1268 
apply (subgoal_tac "n = (n + k * m)  k * m") 

1269 
apply (erule ssubst) 

1270 
apply (erule zdvd_zdiff, simp_all) 

1271 
done 

1272 

1273 
lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n" 

1274 
apply (simp add: dvd_def) 

1275 
apply (auto simp add: zmod_zmult_zmult1) 

1276 
done 

1277 

1278 
lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)" 

1279 
apply (subgoal_tac "k dvd n * (m div n) + m mod n") 

1280 
apply (simp add: zmod_zdiv_equality [symmetric]) 

1281 
apply (simp only: zdvd_zadd zdvd_zmult2) 

1282 
done 

1283 

1284 
lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)" 

1285 
apply (simp add: dvd_def, auto) 

1286 
apply (subgoal_tac "0 < n") 

1287 
prefer 2 

1288 
apply (blast intro: order_less_trans) 

1289 
apply (simp add: zero_less_mult_iff) 

1290 
apply (subgoal_tac "n * k < n * 1") 

1291 
apply (drule mult_less_cancel_left [THEN iffD1], auto) 

1292 
done 

1293 
lemma zmult_div_cancel: "(n::int) * (m div n) = m  (m mod n)" 

1294 
using zmod_zdiv_equality[where a="m" and b="n"] 

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23431
diff
changeset

1295 
by (simp add: ring_simps) 
23164  1296 

1297 
lemma zdvd_mult_div_cancel:"(n::int) dvd m \<Longrightarrow> n * (m div n) = m" 

1298 
apply (subgoal_tac "m mod n = 0") 

1299 
apply (simp add: zmult_div_cancel) 

1300 
apply (simp only: zdvd_iff_zmod_eq_0) 

1301 
done 

1302 

1303 
lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)" 

1304 
shows "m dvd n" 

1305 
proof 

1306 
from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast 

1307 
{assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp 

1308 
with h have False by (simp add: mult_assoc)} 

1309 
hence "n = m * h" by blast 

1310 
thus ?thesis by blast 

1311 
qed 

1312 

23969  1313 
lemma zdvd_zmult_cancel_disj[simp]: 
1314 
"(k*m) dvd (k*n) = (k=0  m dvd (n::int))" 

1315 
by (auto simp: zdvd_zmult_mono dest: zdvd_mult_cancel) 

1316 

1317 

23164  1318 
theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))" 
1319 
apply (simp split add: split_nat) 

1320 
apply (rule iffI) 

1321 
apply (erule exE) 

1322 
apply (rule_tac x = "int x" in exI) 

1323 
apply simp 

1324 
apply (erule exE) 

1325 
apply (rule_tac x = "nat x" in exI) 

1326 
apply (erule conjE) 

1327 
apply (erule_tac x = "nat x" in allE) 

1328 
apply simp 

1329 
done 

1330 

23365  1331 
theorem zdvd_int: "(x dvd y) = (int x dvd int y)" 
23431
25ca91279a9b
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
huffman
parents:
23401
diff
changeset

1332 
apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric] 
25ca91279a9b
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
huffman
parents:
23401
diff
changeset

1333 
nat_0_le cong add: conj_cong) 
23164  1334 
apply (rule iffI) 
1335 
apply iprover 

1336 
apply (erule exE) 

1337 
apply (case_tac "x=0") 

1338 
apply (rule_tac x=0 in exI) 

1339 
apply simp 

1340 
apply (case_tac "0 \<le> k") 

1341 
apply iprover 

1342 
apply (simp add: linorder_not_le) 

23431
25ca91279a9b
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
huffman
parents:
23401
diff
changeset

1343 
apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]]) 
23164  1344 
apply assumption 
1345 
apply (simp add: mult_ac) 

1346 
done 

1347 

1348 
lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)" 

1349 
proof 

1350 
assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by (simp add: zdvd_abs1) 

1351 
hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int) 

1352 
hence "nat \<bar>x\<bar> = 1" by simp 

1353 
thus "\<bar>x\<bar> = 1" by (cases "x < 0", auto) 

1354 
next 

1355 
assume "\<bar>x\<bar>=1" thus "x dvd 1" 

1356 
by(cases "x < 0",simp_all add: minus_equation_iff zdvd_iff_zmod_eq_0) 

1357 
qed 

1358 
lemma zdvd_mult_cancel1: 

1359 
assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)" 

1360 
proof 

1361 
assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m" 

1362 
by (cases "n >0", auto simp add: zdvd_zminus2_iff minus_equation_iff) 

1363 
next 

1364 
assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp 

1365 
from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq) 

1366 
qed 

1367 

23365  1368 
lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))" 
23164  1369 
apply (auto simp add: dvd_def nat_abs_mult_distrib) 
23365  1370 
apply (auto simp add: nat_eq_iff abs_if split add: split_if_asm) 
1371 
apply (rule_tac x = "(int k)" in exI) 

23431
25ca91279a9b
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
huffman
parents:
23401
diff
changeset

1372 
apply (auto simp add: int_mult) 
23306
cdb027d0637e
add int_of_nat versions of lemmas about int::nat=>int
huffman
parents:
23164
diff
changeset

1373 
done 
cdb027d0637e
add int_of_nat versions of lemmas about int::nat=>int
huffman
parents:
23164
diff
changeset

1374 

23365  1375 
lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)" 
23431
25ca91279a9b
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
huffman
parents:
23401
diff
changeset

1376 
apply (auto simp add: dvd_def abs_if int_mult) 
23306
cdb027d0637e
add int_of_nat versions of lemmas about int::nat=>int
huffman
parents:
23164
diff
changeset

1377 
apply (rule_tac [3] x = "nat k" in exI) 
23365  1378 
apply (rule_tac [2] x = "(int k)" in exI) 
23306
cdb027d0637e
add int_of_nat versions of lemmas about int::nat=>int
huffman
parents:
23164
diff
changeset

1379 
apply (rule_tac x = "nat (k)" in exI) 
23431
25ca91279a9b
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
huffman
parents:
23401
diff
changeset

1380 
apply (cut_tac [3] k = m in int_less_0_conv) 
25ca91279a9b
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
huffman
parents:
23401
diff
changeset

1381 
apply (cut_tac k = m in int_less_0_conv) 
23306
cdb027d0637e
add int_of_nat versions of lemmas about int::nat=>int
huffman
parents:
23164
diff
changeset

1382 
apply (auto simp add: zero_le_mult_iff mult_less_0_iff 
23365  1383 
nat_mult_distrib [symmetric] nat_eq_iff2) 
23164  1384 
done 
1385 

1386 
lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)" 

23431
25ca91279a9b
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
huffman
parents:
23401
diff
changeset

1387 
apply (auto simp add: dvd_def int_mult) 
23365  1388 
apply (rule_tac x = "nat k" in exI) 
23431
25ca91279a9b
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
huffman
parents:
23401
diff
changeset

1389 
apply (cut_tac k = m in int_less_0_conv) 
23365  1390 
apply (auto simp add: zero_le_mult_iff mult_less_0_iff 
1391 
nat_mult_distrib [symmetric] nat_eq_iff2) 

1392 
done 

23164  1393 

1394 
lemma zminus_dvd_iff [iff]: "(z dvd w) = (z dvd (w::int))" 

1395 
apply (auto simp add: dvd_def) 

1396 
apply (rule_tac [!] x = "k" in exI, auto) 

1397 
done 

1398 

1399 
lemma dvd_zminus_iff [iff]: "(z dvd w) = (z dvd (w::int))" 

1400 
apply (auto simp add: dvd_def) 

1401 
apply (drule minus_equation_iff [THEN iffD1]) 

1402 
apply (rule_tac [!] x = "k" in exI, auto) 

1403 
done 

1404 

1405 
lemma zdvd_imp_le: "[ z dvd n; 0 < n ] ==> z \<le> (n::int)" 

23365  1406 
apply (rule_tac z=n in int_cases) 
1407 
apply (auto simp add: dvd_int_iff) 

1408 
apply (rule_tac z=z in int_cases) 

23307
2fe3345035c7
modify proofs to avoid referring to int::nat=>int
huffman
parents:
23306
diff
changeset

1409 
apply (auto simp add: dvd_imp_le) 
23164  1410 
done 
1411 

1412 

1413 
subsection{*Integer Powers*} 

1414 

1415 
instance int :: power .. 

1416 

1417 
primrec 

1418 
"p ^ 0 = 1" 

1419 
"p ^ (Suc n) = (p::int) * (p ^ n)" 

1420 

1421 

1422 
instance int :: recpower 

1423 
proof 

1424 
fix z :: int 

1425 
fix n :: nat 

1426 
show "z^0 = 1" by simp 

1427 
show "z^(Suc n) = z * (z^n)" by simp 

1428 
qed 

1429 

24391  1430 
lemma of_int_power: 
1431 
"of_int (z ^ n) = (of_int z ^ n :: 'a::{recpower, ring_1})" 

1432 
by (induct n) (simp_all add: power_Suc) 

23164  1433 

1434 
lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m" 

1435 
apply (induct "y", auto) 

1436 
apply (rule zmod_zmult1_eq [THEN trans]) 

1437 
apply (simp (no_asm_simp)) 

1438 
apply (rule zmod_zmult_distrib [symmetric]) 

1439 
done 

1440 

1441 
lemma zpower_zadd_distrib: "x^(y+z) = ((x^y)*(x^z)::int)" 

1442 
by (rule Power.power_add) 

1443 

1444 
lemma zpower_zpower: "(x^y)^z = (x^(y*z)::int)" 

1445 
by (rule Power.power_mult [symmetric]) 

1446 

1447 
lemma zero_less_zpower_abs_iff [simp]: 

1448 
"(0 < (abs x)^n) = (x \<noteq> (0::int)  n=0)" 

1449 
apply (induct "n") 

1450 
apply (auto simp add: zero_less_mult_iff) 

1451 
done 

1452 

1453 
lemma zero_le_zpower_abs [simp]: "(0::int) <= (abs x)^n" 

1454 
apply (induct "n") 

1455 
apply (auto simp add: zero_le_mult_iff) 

1456 
done 

1457 

1458 
lemma int_power: "int (m^n) = (int m) ^ n" 

23365  1459 
by (rule of_nat_power) 
23164  1460 

1461 
text{*Compatibility binding*} 

1462 
lemmas zpower_int = int_power [symmetric] 

1463 

23365  1464 
lemma zdiv_int: "int (a div b) = (int a) div (int b)" 
23164  1465 
apply (subst split_div, auto) 
1466 
apply (subst split_zdiv, auto) 

23365  1467 
apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in IntDiv.unique_quotient) 
23431
25ca91279a9b
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
huffman
parents:
23401
diff
changeset

1468 
apply (auto simp add: IntDiv.quorem_def of_nat_mult) 
23164  1469 
done 
1470 

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

23365  1472 
apply (subst split_mod, auto) 
1473 
apply (subst split_zmod, auto) 

1474 
apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia 

1475 
in unique_remainder) 

23431
25ca91279a9b
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
huffman
parents:
23401
diff
changeset

1476 
apply (auto simp add: IntDiv.quorem_def of_nat_mult) 
23365  1477 
done 
23164  1478 

1479 
text{*Suggested by Matthias Daum*} 

1480 
lemma int_power_div_base: 

1481 
"\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m  Suc 0)" 

1482 
apply (subgoal_tac "k ^ m = k ^ ((m  1) + 1)") 

1483 
apply (erule ssubst) 

1484 
apply (simp only: power_add) 

1485 
apply simp_all 

1486 
done 

1487 

23853  1488 
text {* by Brian Huffman *} 
1489 
lemma zminus_zmod: " ((x::int) mod m) mod m =  x mod m" 

1490 
by (simp only: zmod_zminus1_eq_if mod_mod_trivial) 

1491 

1492 
lemma zdiff_zmod_left: "(x mod m  y) mod m = (x  y) mod (m::int)" 

1493 
by (simp only: diff_def zmod_zadd_left_eq [symmetric]) 

1494 

1495 
lemma zdiff_zmod_right: "(x  y mod m) mod m = (x  y) mod (m::int)" 

1496 
proof  

1497 
have "(x +  (y mod m) mod m) mod m = (x +  y mod m) mod m" 

1498 
by (simp only: zminus_zmod) 

1499 
hence "(x +  (y mod m)) mod m = (x +  y) mod m" 

1500 
by (simp only: zmod_zadd_right_eq [symmetric]) 

1501 
thus "(x  y mod m) mod m = (x  y) mod m" 

1502 
by (simp only: diff_def) 

1503 
qed 

1504 

1505 
lemmas zmod_simps = 

1506 
IntDiv.zmod_zadd_left_eq [symmetric] 

1507 
IntDiv.zmod_zadd_right_eq [symmetric] 

1508 
< 