author  haftmann 
Fri, 01 Oct 2010 16:05:25 +0200  
changeset 39910  10097e0a9dbd 
parent 37887  2ae085b07f2f 
child 44821  a92f65e174cf 
permissions  rwrr 
24333  1 
(* 
2 
Author: Jeremy Dawson, NICTA 

24350  3 
*) 
24333  4 

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

37655  7 
theory Misc_Numeric 
25592  8 
imports Main Parity 
9 
begin 

24333  10 

39910  11 
lemma the_elemI: "y = {x} ==> the_elem y = x" 
12 
by simp 

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

13 

37591  14 
lemmas split_split = prod.split 
15 
lemmas split_split_asm = prod.split_asm 

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 

27570  48 
lemma zless2: "0 < (2 :: int)" by arith 
24333  49 

24465  50 
lemmas zless2p [simp] = zless2 [THEN zero_less_power] 
51 
lemmas zle2p [simp] = zless2p [THEN order_less_imp_le] 

52 

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

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

55 

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

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

59 
lemma emep1: 

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

61 
apply (simp add: add_commute) 

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

63 
apply (subst pos_zmod_mult_2) 

64 
apply arith 

30943
eb3dbbe971f6
zmod_zmult_zmult1 now subsumed by mod_mult_mult1
haftmann
parents:
30445
diff
changeset

65 
apply (simp add: mod_mult_mult1) 
24333  66 
done 
67 

68 
lemmas eme1p = emep1 [simplified add_commute] 

69 

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

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

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

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

78 
lemmas m1mod2k = zless2p [THEN zmod_minus1] 

24465  79 
lemmas m1mod22k = mult_pos_pos [OF zless2 zless2p, THEN zmod_minus1] 
24333  80 
lemmas p1mod22k' = zless2p [THEN order_less_imp_le, THEN pos_zmod_mult_2] 
24465  81 
lemmas z1pmod2' = zero_le_one [THEN pos_zmod_mult_2, simplified] 
82 
lemmas z1pdiv2' = zero_le_one [THEN pos_zdiv_mult_2, simplified] 

24333  83 

84 
lemma p1mod22k: 

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

86 
by (simp add: p1mod22k' add_commute) 

24465  87 

88 
lemma z1pmod2: 

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

91 
lemma z1pdiv2: 

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

30031  94 
lemmas zdiv_le_dividend = xtr3 [OF div_by_1 [symmetric] zdiv_mono2, 
24333  95 
simplified int_one_le_iff_zero_less, simplified, standard] 
24465  96 

97 
lemma axxbyy: 

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

27570  99 
a = b & m = (n :: int)" by arith 
24465  100 

101 
lemma axxmod2: 

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

104 
lemma axxdiv2: 

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

107 
lemmas iszero_minus = trans [THEN trans, 

108 
OF iszero_def neg_equal_0_iff_equal iszero_def [symmetric], standard] 

24333  109 

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

111 
standard] 

112 

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

114 

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

116 
by (simp add : zmod_zminus1_eq_if) 

24465  117 

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

119 
apply (unfold diff_int_def) 

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

24465  122 
done 
24333  123 

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

125 
apply (unfold diff_int_def) 

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

24333  128 
done 
129 

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

130 
lemma zmod_zsub_left_eq: "((a::int)  b) mod c = (a mod c  b) mod c" 
30034  131 
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

132 

24333  133 
lemma zmod_zsub_self [simp]: 
134 
"((b :: int)  a) mod a = b mod a" 

135 
by (simp add: zmod_zsub_right_eq) 

136 

137 
lemma zmod_zmult1_eq_rev: 

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

139 
apply (simp add: mult_commute) 

140 
apply (subst zmod_zmult1_eq) 

141 
apply simp 

142 
done 

143 

144 
lemmas rdmods [symmetric] = zmod_uminus [symmetric] 

30034  145 
zmod_zsub_left_eq zmod_zsub_right_eq mod_add_left_eq 
146 
mod_add_right_eq zmod_zmult1_eq zmod_zmult1_eq_rev 

24333  147 

148 
lemma mod_plus_right: 

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

150 
apply (induct x) 

151 
apply (simp_all add: mod_Suc) 

152 
apply arith 

153 
done 

154 

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

157 

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

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

160 

29948  161 
lemmas push_mods' = mod_add_eq [standard] 
162 
mod_mult_eq [standard] zmod_zsub_distrib [standard] 

24465  163 
zmod_uminus [symmetric, standard] 
164 

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

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

167 
lemmas mod_simps = 

30034  168 
mod_mult_self2_is_0 [THEN eq_reflection] 
169 
mod_mult_self1_is_0 [THEN eq_reflection] 

24465  170 
mod_mod_trivial [THEN eq_reflection] 
171 

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

174 
by (induct a) auto 

175 

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

177 

178 
lemma nat_mod_lem: 

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

180 
apply safe 

181 
apply (erule nat_mod_eq') 

182 
apply (erule subst) 

183 
apply (erule mod_less_divisor) 

184 
done 

185 

186 
lemma mod_nat_add: 

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

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

189 
apply (rule nat_mod_eq) 

190 
apply auto 

191 
apply (rule trans) 

192 
apply (rule le_mod_geq) 

193 
apply simp 

194 
apply (rule nat_mod_eq') 

195 
apply arith 

196 
done 

24465  197 

198 
lemma mod_nat_sub: 

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

200 
by (rule nat_mod_eq') arith 

24333  201 

202 
lemma int_mod_lem: 

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

204 
apply safe 

205 
apply (erule (1) mod_pos_pos_trivial) 

206 
apply (erule_tac [!] subst) 

207 
apply auto 

208 
done 

209 

210 
lemma int_mod_eq: 

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

212 
by clarsimp (rule mod_pos_pos_trivial) 

213 

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

215 

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

217 
apply (cases "a < n") 

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

219 
done 

220 

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

221 
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

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

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

225 
apply (cases "0 <= a") 

226 
apply (drule (1) mod_pos_pos_trivial) 

227 
apply simp 

228 
apply (rule order_trans [OF _ pos_mod_sign]) 

229 
apply simp 

230 
apply assumption 

231 
done 

232 

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

233 
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

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

236 
lemma mod_add_if_z: 

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

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

239 
by (auto intro: int_mod_eq) 

240 

241 
lemma mod_sub_if_z: 

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

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

244 
by (auto intro: int_mod_eq) 

24465  245 

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

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

248 

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

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

251 
apply (rule mcl) 

252 
prefer 2 

253 
apply (erule asm_rl) 

254 
apply (simp add: zmde ring_distribs) 

255 
done 

256 

257 
(** Rep_Integ **) 

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

30198  259 
unfolding equiv_def refl_on_def quotient_def Image_def by auto 
24465  260 

261 
lemmas Rep_Integ_ne = Integ.Rep_Integ 

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

263 

264 
lemmas riq = Integ.Rep_Integ [simplified Integ_def] 

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

266 
lemmas Rep_Integ_equiv = quotient_eq_iff 

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

268 
lemmas Rep_Integ_same = 

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

270 

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

272 
unfolding int_def by auto 

273 

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

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

276 

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

278 
apply (rule_tac z=x in eq_Abs_Integ) 

279 
apply (clarsimp simp: minus) 

280 
done 

24333  281 

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

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

285 
apply (rule_tac z=x in eq_Abs_Integ) 

286 
apply (rule_tac z=y in eq_Abs_Integ) 

287 
apply (clarsimp simp: add) 

288 
done 

289 

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

291 
by fast 

292 

293 
(* two alternative proofs of this *) 

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

37887  295 
apply (unfold diff_minus) 
24465  296 
apply (rule mem_same) 
297 
apply (rule RI_minus RI_add RI_int)+ 

298 
apply simp 

299 
done 

300 

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

302 
apply safe 

303 
apply (rule Rep_Integ_same) 

304 
prefer 2 

305 
apply (erule asm_rl) 

306 
apply (rule RI_eq_diff')+ 

307 
done 

308 

309 
lemma mod_power_lem: 

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

311 
apply clarsimp 

312 
apply safe 

30042  313 
apply (simp add: dvd_eq_mod_eq_0 [symmetric]) 
24465  314 
apply (drule le_iff_add [THEN iffD1]) 
315 
apply (force simp: zpower_zadd_distrib) 

316 
apply (rule mod_pos_pos_trivial) 

25875  317 
apply (simp) 
24465  318 
apply (rule power_strict_increasing) 
319 
apply auto 

320 
done 

24333  321 

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

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

325 

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

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

329 

24465  330 
lemma pl_pl_rels: 
331 
"a + b = c + d ==> 

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

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

335 

27570  336 
lemma minus_eq: "(m  k = m) = (k = 0  m = (0 :: nat))" by arith 
24465  337 

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

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

341 

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

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

345 

24465  346 
lemma nat_no_eq_iff: 
347 
"(number_of b :: int) >= 0 ==> (number_of c :: int) >= 0 ==> 

27570  348 
(number_of b = (number_of c :: nat)) = (b = c)" 
349 
apply (unfold nat_number_of_def) 

24465  350 
apply safe 
351 
apply (drule (2) eq_nat_nat_iff [THEN iffD1]) 

352 
apply (simp add: number_of_eq) 

353 
done 

354 

24333  355 
lemmas dme = box_equals [OF div_mod_equality add_0_right add_0_right] 
356 
lemmas dtle = xtr3 [OF dme [symmetric] le_add1] 

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

358 

359 
lemma td_gal: 

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

361 
apply safe 

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

363 
apply (erule th2) 

364 
done 

365 

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

366 
lemmas td_gal_lt = td_gal [simplified not_less [symmetric], simplified] 
24333  367 

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

369 
apply (cases b) 

370 
prefer 2 

371 
apply (rule order_refl [THEN th2]) 

372 
apply auto 

373 
done 

374 

375 
lemmas sdl = split_div_lemma [THEN iffD1, symmetric] 

376 

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

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

379 

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

381 
apply (frule given_quot) 

382 
apply (rule trans) 

383 
prefer 2 

384 
apply (erule asm_rl) 

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

386 
apply (simp add : mult_ac) 

387 
done 

388 

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

391 
apply clarify 

392 
apply (case_tac k) 

393 
apply clarsimp 

394 
apply clarify 

395 
apply (cases "b > 0") 

396 
apply (drule mult_commute [THEN xtr1]) 

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

398 
apply (clarsimp simp: le_simps) 

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

400 
apply (rule mult_mono) 

401 
apply auto 

402 
done 

403 

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

406 
apply (rule mult_right_mono) 

407 
apply (rule zless_imp_add1_zle) 

408 
apply (erule (1) mult_right_less_imp_less) 

409 
apply assumption 

410 
done 

411 

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

24465  413 

414 
lemmas less_le_mult_minus = iffD2 [OF le_diff_eq less_le_mult, 

415 
simplified left_diff_distrib, standard] 

24333  416 

417 
lemma lrlem': 

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

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

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

421 
shows "R" using d 

422 
apply safe 

423 
apply (rule R1, erule mult_le_mono1) 

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

425 
done 

426 

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

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

429 
apply safe 

430 
apply arith 

431 
apply (case_tac "sc >= n") 

432 
apply arith 

433 
apply (insert linorder_le_less_linear [of m lb]) 

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

435 
apply arith 

436 
apply simp 

437 
done 

438 

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

440 
by auto 

441 

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

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

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

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

448 
done 

24399  449 

24333  450 
end 