author  wenzelm 
Wed, 11 Mar 2009 19:27:04 +0100  
changeset 30445  757ba2bb2b39 
parent 30242  aea5d7fa7ef5 
child 30943  eb3dbbe971f6 
permissions  rwrr 
24333  1 
(* 
2 
Author: Jeremy Dawson, NICTA 

24350  3 
*) 
24333  4 

24350  5 
header {* Useful Numerical Lemmas *} 
24333  6 

25592  7 
theory Num_Lemmas 
8 
imports Main Parity 

9 
begin 

24333  10 

26560  11 
lemma contentsI: "y = {x} ==> contents y = x" 
12 
unfolding contents_def by auto  {* FIXME move *} 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26072
diff
changeset

13 

30445
757ba2bb2b39
renamed (unused?) "split.splits" to split_splits  it was only accepted by accident;
wenzelm
parents:
30242
diff
changeset

14 
lemmas split_split = prod.split [unfolded prod_case_split] 
24465  15 
lemmas split_split_asm = prod.split_asm [unfolded prod_case_split] 
30445
757ba2bb2b39
renamed (unused?) "split.splits" to split_splits  it was only accepted by accident;
wenzelm
parents:
30242
diff
changeset

16 
lemmas split_splits = split_split split_split_asm 
24465  17 

18 
lemmas funpow_0 = funpow.simps(1) 

24333  19 
lemmas funpow_Suc = funpow.simps(2) 
24465  20 

27570  21 
lemma nonemptyE: "S ~= {} ==> (!!x. x : S ==> R) ==> R" by auto 
24333  22 

27570  23 
lemma gt_or_eq_0: "0 < y \<or> 0 = (y::nat)" by arith 
24333  24 

24465  25 
declare iszero_0 [iff] 
26 

24333  27 
lemmas xtr1 = xtrans(1) 
28 
lemmas xtr2 = xtrans(2) 

29 
lemmas xtr3 = xtrans(3) 

30 
lemmas xtr4 = xtrans(4) 

31 
lemmas xtr5 = xtrans(5) 

32 
lemmas xtr6 = xtrans(6) 

33 
lemmas xtr7 = xtrans(7) 

34 
lemmas xtr8 = xtrans(8) 

35 

24465  36 
lemmas nat_simps = diff_add_inverse2 diff_add_inverse 
37 
lemmas nat_iffs = le_add1 le_add2 

38 

27570  39 
lemma sum_imp_diff: "j = k + i ==> j  i = (k :: nat)" by arith 
24465  40 

24333  41 
lemma nobm1: 
42 
"0 < (number_of w :: nat) ==> 

27570  43 
number_of w  (1 :: nat) = number_of (Int.pred w)" 
24333  44 
apply (unfold nat_number_of_def One_nat_def nat_1 [symmetric] pred_def) 
45 
apply (simp add: number_of_eq nat_diff_distrib [symmetric]) 

46 
done 

24465  47 

48 
lemma of_int_power: 

49 
"of_int (a ^ n) = (of_int a ^ n :: 'a :: {recpower, comm_ring_1})" 

50 
by (induct n) (auto simp add: power_Suc) 

24333  51 

27570  52 
lemma zless2: "0 < (2 :: int)" by arith 
24333  53 

24465  54 
lemmas zless2p [simp] = zless2 [THEN zero_less_power] 
55 
lemmas zle2p [simp] = zless2p [THEN order_less_imp_le] 

56 

57 
lemmas pos_mod_sign2 = zless2 [THEN pos_mod_sign [where b = "2::int"]] 

58 
lemmas pos_mod_bound2 = zless2 [THEN pos_mod_bound [where b = "2::int"]] 

59 

60 
 "the inverse(s) of @{text number_of}" 

27570  61 
lemma nmod2: "n mod (2::int) = 0  n mod 2 = 1" by arith 
24333  62 

63 
lemma emep1: 

64 
"even n ==> even d ==> 0 <= d ==> (n + 1) mod (d :: int) = (n mod d) + 1" 

65 
apply (simp add: add_commute) 

66 
apply (safe dest!: even_equiv_def [THEN iffD1]) 

67 
apply (subst pos_zmod_mult_2) 

68 
apply arith 

69 
apply (simp add: zmod_zmult_zmult1) 

70 
done 

71 

72 
lemmas eme1p = emep1 [simplified add_commute] 

73 

27570  74 
lemma le_diff_eq': "(a \<le> c  b) = (b + a \<le> (c::int))" by arith 
24465  75 

27570  76 
lemma less_diff_eq': "(a < c  b) = (b + a < (c::int))" by arith 
24465  77 

27570  78 
lemma diff_le_eq': "(a  b \<le> c) = (a \<le> b + (c::int))" by arith 
24465  79 

27570  80 
lemma diff_less_eq': "(a  b < c) = (a < b + (c::int))" by arith 
24333  81 

82 
lemmas m1mod2k = zless2p [THEN zmod_minus1] 

24465  83 
lemmas m1mod22k = mult_pos_pos [OF zless2 zless2p, THEN zmod_minus1] 
24333  84 
lemmas p1mod22k' = zless2p [THEN order_less_imp_le, THEN pos_zmod_mult_2] 
24465  85 
lemmas z1pmod2' = zero_le_one [THEN pos_zmod_mult_2, simplified] 
86 
lemmas z1pdiv2' = zero_le_one [THEN pos_zdiv_mult_2, simplified] 

24333  87 

88 
lemma p1mod22k: 

89 
"(2 * b + 1) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n) + (1::int)" 

90 
by (simp add: p1mod22k' add_commute) 

24465  91 

92 
lemma z1pmod2: 

27570  93 
"(2 * b + 1) mod 2 = (1::int)" by arith 
24465  94 

95 
lemma z1pdiv2: 

27570  96 
"(2 * b + 1) div 2 = (b::int)" by arith 
24333  97 

30031  98 
lemmas zdiv_le_dividend = xtr3 [OF div_by_1 [symmetric] zdiv_mono2, 
24333  99 
simplified int_one_le_iff_zero_less, simplified, standard] 
24465  100 

101 
lemma axxbyy: 

102 
"a + m + m = b + n + n ==> (a = 0  a = 1) ==> (b = 0  b = 1) ==> 

27570  103 
a = b & m = (n :: int)" by arith 
24465  104 

105 
lemma axxmod2: 

27570  106 
"(1 + x + x) mod 2 = (1 :: int) & (0 + x + x) mod 2 = (0 :: int)" by arith 
24465  107 

108 
lemma axxdiv2: 

27570  109 
"(1 + x + x) div 2 = (x :: int) & (0 + x + x) div 2 = (x :: int)" by arith 
24465  110 

111 
lemmas iszero_minus = trans [THEN trans, 

112 
OF iszero_def neg_equal_0_iff_equal iszero_def [symmetric], standard] 

24333  113 

114 
lemmas zadd_diff_inverse = trans [OF diff_add_cancel [symmetric] add_commute, 

115 
standard] 

116 

117 
lemmas add_diff_cancel2 = add_commute [THEN diff_eq_eq [THEN iffD2], standard] 

118 

119 
lemma zmod_uminus: " ((a :: int) mod b) mod b = a mod b" 

120 
by (simp add : zmod_zminus1_eq_if) 

24465  121 

122 
lemma zmod_zsub_distrib: "((a::int)  b) mod c = (a mod c  b mod c) mod c" 

123 
apply (unfold diff_int_def) 

29948  124 
apply (rule trans [OF _ mod_add_eq [symmetric]]) 
125 
apply (simp add: zmod_uminus mod_add_eq [symmetric]) 

24465  126 
done 
24333  127 

128 
lemma zmod_zsub_right_eq: "((a::int)  b) mod c = (a  b mod c) mod c" 

129 
apply (unfold diff_int_def) 

30034  130 
apply (rule trans [OF _ mod_add_right_eq [symmetric]]) 
131 
apply (simp add : zmod_uminus mod_add_right_eq [symmetric]) 

24333  132 
done 
133 

25349
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
24465
diff
changeset

134 
lemma zmod_zsub_left_eq: "((a::int)  b) mod c = (a mod c  b) mod c" 
30034  135 
by (rule mod_add_left_eq [where b = " b", simplified diff_int_def [symmetric]]) 
25349
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
24465
diff
changeset

136 

24333  137 
lemma zmod_zsub_self [simp]: 
138 
"((b :: int)  a) mod a = b mod a" 

139 
by (simp add: zmod_zsub_right_eq) 

140 

141 
lemma zmod_zmult1_eq_rev: 

142 
"b * a mod c = b mod c * a mod (c::int)" 

143 
apply (simp add: mult_commute) 

144 
apply (subst zmod_zmult1_eq) 

145 
apply simp 

146 
done 

147 

148 
lemmas rdmods [symmetric] = zmod_uminus [symmetric] 

30034  149 
zmod_zsub_left_eq zmod_zsub_right_eq mod_add_left_eq 
150 
mod_add_right_eq zmod_zmult1_eq zmod_zmult1_eq_rev 

24333  151 

152 
lemma mod_plus_right: 

153 
"((a + x) mod m = (b + x) mod m) = (a mod m = b mod (m :: nat))" 

154 
apply (induct x) 

155 
apply (simp_all add: mod_Suc) 

156 
apply arith 

157 
done 

158 

24465  159 
lemma nat_minus_mod: "(n  n mod m) mod m = (0 :: nat)" 
160 
by (induct n) (simp_all add : mod_Suc) 

161 

162 
lemmas nat_minus_mod_plus_right = trans [OF nat_minus_mod mod_0 [symmetric], 

163 
THEN mod_plus_right [THEN iffD2], standard, simplified] 

164 

29948  165 
lemmas push_mods' = mod_add_eq [standard] 
166 
mod_mult_eq [standard] zmod_zsub_distrib [standard] 

24465  167 
zmod_uminus [symmetric, standard] 
168 

169 
lemmas push_mods = push_mods' [THEN eq_reflection, standard] 

170 
lemmas pull_mods = push_mods [symmetric] rdmods [THEN eq_reflection, standard] 

171 
lemmas mod_simps = 

30034  172 
mod_mult_self2_is_0 [THEN eq_reflection] 
173 
mod_mult_self1_is_0 [THEN eq_reflection] 

24465  174 
mod_mod_trivial [THEN eq_reflection] 
175 

24333  176 
lemma nat_mod_eq: 
177 
"!!b. b < n ==> a mod n = b mod n ==> a mod n = (b :: nat)" 

178 
by (induct a) auto 

179 

180 
lemmas nat_mod_eq' = refl [THEN [2] nat_mod_eq] 

181 

182 
lemma nat_mod_lem: 

183 
"(0 :: nat) < n ==> b < n = (b mod n = b)" 

184 
apply safe 

185 
apply (erule nat_mod_eq') 

186 
apply (erule subst) 

187 
apply (erule mod_less_divisor) 

188 
done 

189 

190 
lemma mod_nat_add: 

191 
"(x :: nat) < z ==> y < z ==> 

192 
(x + y) mod z = (if x + y < z then x + y else x + y  z)" 

193 
apply (rule nat_mod_eq) 

194 
apply auto 

195 
apply (rule trans) 

196 
apply (rule le_mod_geq) 

197 
apply simp 

198 
apply (rule nat_mod_eq') 

199 
apply arith 

200 
done 

24465  201 

202 
lemma mod_nat_sub: 

203 
"(x :: nat) < z ==> (x  y) mod z = x  y" 

204 
by (rule nat_mod_eq') arith 

24333  205 

206 
lemma int_mod_lem: 

207 
"(0 :: int) < n ==> (0 <= b & b < n) = (b mod n = b)" 

208 
apply safe 

209 
apply (erule (1) mod_pos_pos_trivial) 

210 
apply (erule_tac [!] subst) 

211 
apply auto 

212 
done 

213 

214 
lemma int_mod_eq: 

215 
"(0 :: int) <= b ==> b < n ==> a mod n = b mod n ==> a mod n = b" 

216 
by clarsimp (rule mod_pos_pos_trivial) 

217 

218 
lemmas int_mod_eq' = refl [THEN [3] int_mod_eq] 

219 

220 
lemma int_mod_le: "0 <= a ==> 0 < (n :: int) ==> a mod n <= a" 

221 
apply (cases "a < n") 

222 
apply (auto dest: mod_pos_pos_trivial pos_mod_bound [where a=a]) 

223 
done 

224 

25349
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
24465
diff
changeset

225 
lemma int_mod_le': "0 <= b  n ==> 0 < (n :: int) ==> b mod n <= b  n" 
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
24465
diff
changeset

226 
by (rule int_mod_le [where a = "b  n" and n = n, simplified]) 
24333  227 

228 
lemma int_mod_ge: "a < n ==> 0 < (n :: int) ==> a <= a mod n" 

229 
apply (cases "0 <= a") 

230 
apply (drule (1) mod_pos_pos_trivial) 

231 
apply simp 

232 
apply (rule order_trans [OF _ pos_mod_sign]) 

233 
apply simp 

234 
apply assumption 

235 
done 

236 

25349
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
24465
diff
changeset

237 
lemma int_mod_ge': "b < 0 ==> 0 < (n :: int) ==> b + n <= b mod n" 
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
24465
diff
changeset

238 
by (rule int_mod_ge [where a = "b + n" and n = n, simplified]) 
24333  239 

240 
lemma mod_add_if_z: 

241 
"(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==> 

242 
(x + y) mod z = (if x + y < z then x + y else x + y  z)" 

243 
by (auto intro: int_mod_eq) 

244 

245 
lemma mod_sub_if_z: 

246 
"(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==> 

247 
(x  y) mod z = (if y <= x then x  y else x  y + z)" 

248 
by (auto intro: int_mod_eq) 

24465  249 

250 
lemmas zmde = zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2], symmetric] 

251 
lemmas mcl = mult_cancel_left [THEN iffD1, THEN make_pos_rule] 

252 

253 
(* already have this for naturals, div_mult_self1/2, but not for ints *) 

254 
lemma zdiv_mult_self: "m ~= (0 :: int) ==> (a + m * n) div m = a div m + n" 

255 
apply (rule mcl) 

256 
prefer 2 

257 
apply (erule asm_rl) 

258 
apply (simp add: zmde ring_distribs) 

259 
done 

260 

261 
(** Rep_Integ **) 

262 
lemma eqne: "equiv A r ==> X : A // r ==> X ~= {}" 

30198  263 
unfolding equiv_def refl_on_def quotient_def Image_def by auto 
24465  264 

265 
lemmas Rep_Integ_ne = Integ.Rep_Integ 

266 
[THEN equiv_intrel [THEN eqne, simplified Integ_def [symmetric]], standard] 

267 

268 
lemmas riq = Integ.Rep_Integ [simplified Integ_def] 

269 
lemmas intrel_refl = refl [THEN equiv_intrel_iff [THEN iffD1], standard] 

270 
lemmas Rep_Integ_equiv = quotient_eq_iff 

271 
[OF equiv_intrel riq riq, simplified Integ.Rep_Integ_inject, standard] 

272 
lemmas Rep_Integ_same = 

273 
Rep_Integ_equiv [THEN intrel_refl [THEN rev_iffD2], standard] 

274 

275 
lemma RI_int: "(a, 0) : Rep_Integ (int a)" 

276 
unfolding int_def by auto 

277 

278 
lemmas RI_intrel [simp] = UNIV_I [THEN quotientI, 

279 
THEN Integ.Abs_Integ_inverse [simplified Integ_def], standard] 

280 

281 
lemma RI_minus: "(a, b) : Rep_Integ x ==> (b, a) : Rep_Integ ( x)" 

282 
apply (rule_tac z=x in eq_Abs_Integ) 

283 
apply (clarsimp simp: minus) 

284 
done 

24333  285 

24465  286 
lemma RI_add: 
287 
"(a, b) : Rep_Integ x ==> (c, d) : Rep_Integ y ==> 

288 
(a + c, b + d) : Rep_Integ (x + y)" 

289 
apply (rule_tac z=x in eq_Abs_Integ) 

290 
apply (rule_tac z=y in eq_Abs_Integ) 

291 
apply (clarsimp simp: add) 

292 
done 

293 

294 
lemma mem_same: "a : S ==> a = b ==> b : S" 

295 
by fast 

296 

297 
(* two alternative proofs of this *) 

298 
lemma RI_eq_diff': "(a, b) : Rep_Integ (int a  int b)" 

299 
apply (unfold diff_def) 

300 
apply (rule mem_same) 

301 
apply (rule RI_minus RI_add RI_int)+ 

302 
apply simp 

303 
done 

304 

305 
lemma RI_eq_diff: "((a, b) : Rep_Integ x) = (int a  int b = x)" 

306 
apply safe 

307 
apply (rule Rep_Integ_same) 

308 
prefer 2 

309 
apply (erule asm_rl) 

310 
apply (rule RI_eq_diff')+ 

311 
done 

312 

313 
lemma mod_power_lem: 

314 
"a > 1 ==> a ^ n mod a ^ m = (if m <= n then 0 else (a :: int) ^ n)" 

315 
apply clarsimp 

316 
apply safe 

30042  317 
apply (simp add: dvd_eq_mod_eq_0 [symmetric]) 
24465  318 
apply (drule le_iff_add [THEN iffD1]) 
319 
apply (force simp: zpower_zadd_distrib) 

320 
apply (rule mod_pos_pos_trivial) 

25875  321 
apply (simp) 
24465  322 
apply (rule power_strict_increasing) 
323 
apply auto 

324 
done 

24333  325 

27570  326 
lemma min_pm [simp]: "min a b + (a  b) = (a :: nat)" by arith 
24333  327 

328 
lemmas min_pm1 [simp] = trans [OF add_commute min_pm] 

329 

27570  330 
lemma rev_min_pm [simp]: "min b a + (a  b) = (a::nat)" by arith 
24333  331 

332 
lemmas rev_min_pm1 [simp] = trans [OF add_commute rev_min_pm] 

333 

24465  334 
lemma pl_pl_rels: 
335 
"a + b = c + d ==> 

27570  336 
a >= c & b <= d  a <= c & b >= (d :: nat)" by arith 
24465  337 

338 
lemmas pl_pl_rels' = add_commute [THEN [2] trans, THEN pl_pl_rels] 

339 

27570  340 
lemma minus_eq: "(m  k = m) = (k = 0  m = (0 :: nat))" by arith 
24465  341 

27570  342 
lemma pl_pl_mm: "(a :: nat) + b = c + d ==> a  c = d  b" by arith 
24465  343 

344 
lemmas pl_pl_mm' = add_commute [THEN [2] trans, THEN pl_pl_mm] 

345 

27570  346 
lemma min_minus [simp] : "min m (m  k) = (m  k :: nat)" by arith 
24333  347 

348 
lemmas min_minus' [simp] = trans [OF min_max.inf_commute min_minus] 

349 

24465  350 
lemma nat_no_eq_iff: 
351 
"(number_of b :: int) >= 0 ==> (number_of c :: int) >= 0 ==> 

27570  352 
(number_of b = (number_of c :: nat)) = (b = c)" 
353 
apply (unfold nat_number_of_def) 

24465  354 
apply safe 
355 
apply (drule (2) eq_nat_nat_iff [THEN iffD1]) 

356 
apply (simp add: number_of_eq) 

357 
done 

358 

24333  359 
lemmas dme = box_equals [OF div_mod_equality add_0_right add_0_right] 
360 
lemmas dtle = xtr3 [OF dme [symmetric] le_add1] 

361 
lemmas th2 = order_trans [OF order_refl [THEN [2] mult_le_mono] dtle] 

362 

363 
lemma td_gal: 

364 
"0 < c ==> (a >= b * c) = (a div c >= (b :: nat))" 

365 
apply safe 

366 
apply (erule (1) xtr4 [OF div_le_mono div_mult_self_is_m]) 

367 
apply (erule th2) 

368 
done 

369 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25937
diff
changeset

370 
lemmas td_gal_lt = td_gal [simplified not_less [symmetric], simplified] 
24333  371 

372 
lemma div_mult_le: "(a :: nat) div b * b <= a" 

373 
apply (cases b) 

374 
prefer 2 

375 
apply (rule order_refl [THEN th2]) 

376 
apply auto 

377 
done 

378 

379 
lemmas sdl = split_div_lemma [THEN iffD1, symmetric] 

380 

381 
lemma given_quot: "f > (0 :: nat) ==> (f * l + (f  1)) div f = l" 

382 
by (rule sdl, assumption) (simp (no_asm)) 

383 

384 
lemma given_quot_alt: "f > (0 :: nat) ==> (l * f + f  Suc 0) div f = l" 

385 
apply (frule given_quot) 

386 
apply (rule trans) 

387 
prefer 2 

388 
apply (erule asm_rl) 

389 
apply (rule_tac f="%n. n div f" in arg_cong) 

390 
apply (simp add : mult_ac) 

391 
done 

392 

24465  393 
lemma diff_mod_le: "(a::nat) < d ==> b dvd d ==> a  a mod b <= d  b" 
394 
apply (unfold dvd_def) 

395 
apply clarify 

396 
apply (case_tac k) 

397 
apply clarsimp 

398 
apply clarify 

399 
apply (cases "b > 0") 

400 
apply (drule mult_commute [THEN xtr1]) 

401 
apply (frule (1) td_gal_lt [THEN iffD1]) 

402 
apply (clarsimp simp: le_simps) 

403 
apply (rule mult_div_cancel [THEN [2] xtr4]) 

404 
apply (rule mult_mono) 

405 
apply auto 

406 
done 

407 

24333  408 
lemma less_le_mult': 
409 
"w * c < b * c ==> 0 \<le> c ==> (w + 1) * c \<le> b * (c::int)" 

410 
apply (rule mult_right_mono) 

411 
apply (rule zless_imp_add1_zle) 

412 
apply (erule (1) mult_right_less_imp_less) 

413 
apply assumption 

414 
done 

415 

416 
lemmas less_le_mult = less_le_mult' [simplified left_distrib, simplified] 

24465  417 

418 
lemmas less_le_mult_minus = iffD2 [OF le_diff_eq less_le_mult, 

419 
simplified left_diff_distrib, standard] 

24333  420 

421 
lemma lrlem': 

422 
assumes d: "(i::nat) \<le> j \<or> m < j'" 

423 
assumes R1: "i * k \<le> j * k \<Longrightarrow> R" 

424 
assumes R2: "Suc m * k' \<le> j' * k' \<Longrightarrow> R" 

425 
shows "R" using d 

426 
apply safe 

427 
apply (rule R1, erule mult_le_mono1) 

428 
apply (rule R2, erule Suc_le_eq [THEN iffD2 [THEN mult_le_mono1]]) 

429 
done 

430 

431 
lemma lrlem: "(0::nat) < sc ==> 

432 
(sc  n + (n + lb * n) <= m * n) = (sc + lb * n <= m * n)" 

433 
apply safe 

434 
apply arith 

435 
apply (case_tac "sc >= n") 

436 
apply arith 

437 
apply (insert linorder_le_less_linear [of m lb]) 

438 
apply (erule_tac k=n and k'=n in lrlem') 

439 
apply arith 

440 
apply simp 

441 
done 

442 

443 
lemma gen_minus: "0 < n ==> f n = f (Suc (n  1))" 

444 
by auto 

445 

27570  446 
lemma mpl_lem: "j <= (i :: nat) ==> k < j ==> i  j + k < i" by arith 
24333  447 

24465  448 
lemma nonneg_mod_div: 
449 
"0 <= a ==> 0 <= b ==> 0 <= (a mod b :: int) & 0 <= a div b" 

450 
apply (cases "b = 0", clarsimp) 

451 
apply (auto intro: pos_imp_zdiv_nonneg_iff [THEN iffD2]) 

452 
done 

24399  453 

24333  454 
end 