author  berghofe 
Wed, 13 Nov 2002 15:24:42 +0100  
changeset 13704  854501b1e957 
parent 13595  7e6cdcd113a2 
child 13735  7de9342aca7a 
permissions  rwrr 
12396  1 
(* Title: HOL/Finite_Set.thy 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel 

4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 

5 
*) 

6 

7 
header {* Finite sets *} 

8 

9 
theory Finite_Set = Divides + Power + Inductive + SetInterval: 

10 

11 
subsection {* Collection of finite sets *} 

12 

13 
consts Finites :: "'a set set" 

14 

15 
inductive Finites 

16 
intros 

17 
emptyI [simp, intro!]: "{} : Finites" 

18 
insertI [simp, intro!]: "A : Finites ==> insert a A : Finites" 

19 

20 
syntax 

21 
finite :: "'a set => bool" 

22 
translations 

23 
"finite A" == "A : Finites" 

24 

25 
axclass finite \<subseteq> type 

26 
finite: "finite UNIV" 

27 

28 

29 
lemma finite_induct [case_names empty insert, induct set: Finites]: 

30 
"finite F ==> 

31 
P {} ==> (!!F x. finite F ==> x \<notin> F ==> P F ==> P (insert x F)) ==> P F" 

32 
 {* Discharging @{text "x \<notin> F"} entails extra work. *} 

33 
proof  

13421  34 
assume "P {}" and 
35 
insert: "!!F x. finite F ==> x \<notin> F ==> P F ==> P (insert x F)" 

12396  36 
assume "finite F" 
37 
thus "P F" 

38 
proof induct 

39 
show "P {}" . 

40 
fix F x assume F: "finite F" and P: "P F" 

41 
show "P (insert x F)" 

42 
proof cases 

43 
assume "x \<in> F" 

44 
hence "insert x F = F" by (rule insert_absorb) 

45 
with P show ?thesis by (simp only:) 

46 
next 

47 
assume "x \<notin> F" 

48 
from F this P show ?thesis by (rule insert) 

49 
qed 

50 
qed 

51 
qed 

52 

53 
lemma finite_subset_induct [consumes 2, case_names empty insert]: 

54 
"finite F ==> F \<subseteq> A ==> 

55 
P {} ==> (!!F a. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)) ==> 

56 
P F" 

57 
proof  

13421  58 
assume "P {}" and insert: 
59 
"!!F a. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)" 

12396  60 
assume "finite F" 
61 
thus "F \<subseteq> A ==> P F" 

62 
proof induct 

63 
show "P {}" . 

64 
fix F x assume "finite F" and "x \<notin> F" 

65 
and P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A" 

66 
show "P (insert x F)" 

67 
proof (rule insert) 

68 
from i show "x \<in> A" by blast 

69 
from i have "F \<subseteq> A" by blast 

70 
with P show "P F" . 

71 
qed 

72 
qed 

73 
qed 

74 

75 
lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)" 

76 
 {* The union of two finite sets is finite. *} 

77 
by (induct set: Finites) simp_all 

78 

79 
lemma finite_subset: "A \<subseteq> B ==> finite B ==> finite A" 

80 
 {* Every subset of a finite set is finite. *} 

81 
proof  

82 
assume "finite B" 

83 
thus "!!A. A \<subseteq> B ==> finite A" 

84 
proof induct 

85 
case empty 

86 
thus ?case by simp 

87 
next 

88 
case (insert F x A) 

89 
have A: "A \<subseteq> insert x F" and r: "A  {x} \<subseteq> F ==> finite (A  {x})" . 

90 
show "finite A" 

91 
proof cases 

92 
assume x: "x \<in> A" 

93 
with A have "A  {x} \<subseteq> F" by (simp add: subset_insert_iff) 

94 
with r have "finite (A  {x})" . 

95 
hence "finite (insert x (A  {x}))" .. 

96 
also have "insert x (A  {x}) = A" by (rule insert_Diff) 

97 
finally show ?thesis . 

98 
next 

99 
show "A \<subseteq> F ==> ?thesis" . 

100 
assume "x \<notin> A" 

101 
with A show "A \<subseteq> F" by (simp add: subset_insert_iff) 

102 
qed 

103 
qed 

104 
qed 

105 

106 
lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)" 

107 
by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI) 

108 

109 
lemma finite_Int [simp, intro]: "finite F  finite G ==> finite (F Int G)" 

110 
 {* The converse obviously fails. *} 

111 
by (blast intro: finite_subset) 

112 

113 
lemma finite_insert [simp]: "finite (insert a A) = finite A" 

114 
apply (subst insert_is_Un) 

115 
apply (simp only: finite_Un) 

116 
apply blast 

117 
done 

118 

13490
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

119 
lemma finite_imageI[simp]: "finite F ==> finite (h ` F)" 
12396  120 
 {* The image of a finite set is finite. *} 
121 
by (induct set: Finites) simp_all 

122 

123 
lemma finite_range_imageI: 

124 
"finite (range g) ==> finite (range (%x. f (g x)))" 

125 
apply (drule finite_imageI) 

126 
apply simp 

127 
done 

128 

129 
lemma finite_empty_induct: 

130 
"finite A ==> 

131 
P A ==> (!!a A. finite A ==> a:A ==> P A ==> P (A  {a})) ==> P {}" 

132 
proof  

133 
assume "finite A" 

134 
and "P A" and "!!a A. finite A ==> a:A ==> P A ==> P (A  {a})" 

135 
have "P (A  A)" 

136 
proof  

137 
fix c b :: "'a set" 

138 
presume c: "finite c" and b: "finite b" 

139 
and P1: "P b" and P2: "!!x y. finite y ==> x \<in> y ==> P y ==> P (y  {x})" 

140 
from c show "c \<subseteq> b ==> P (b  c)" 

141 
proof induct 

142 
case empty 

143 
from P1 show ?case by simp 

144 
next 

145 
case (insert F x) 

146 
have "P (b  F  {x})" 

147 
proof (rule P2) 

148 
from _ b show "finite (b  F)" by (rule finite_subset) blast 

149 
from insert show "x \<in> b  F" by simp 

150 
from insert show "P (b  F)" by simp 

151 
qed 

152 
also have "b  F  {x} = b  insert x F" by (rule Diff_insert [symmetric]) 

153 
finally show ?case . 

154 
qed 

155 
next 

156 
show "A \<subseteq> A" .. 

157 
qed 

158 
thus "P {}" by simp 

159 
qed 

160 

161 
lemma finite_Diff [simp]: "finite B ==> finite (B  Ba)" 

162 
by (rule Diff_subset [THEN finite_subset]) 

163 

164 
lemma finite_Diff_insert [iff]: "finite (A  insert a B) = finite (A  B)" 

165 
apply (subst Diff_insert) 

166 
apply (case_tac "a : A  B") 

167 
apply (rule finite_insert [symmetric, THEN trans]) 

168 
apply (subst insert_Diff) 

169 
apply simp_all 

170 
done 

171 

172 

173 
lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A" 

174 
proof  

175 
have aux: "!!A. finite (A  {}) = finite A" by simp 

176 
fix B :: "'a set" 

177 
assume "finite B" 

178 
thus "!!A. f`A = B ==> inj_on f A ==> finite A" 

179 
apply induct 

180 
apply simp 

181 
apply (subgoal_tac "EX y:A. f y = x & F = f ` (A  {y})") 

182 
apply clarify 

183 
apply (simp (no_asm_use) add: inj_on_def) 

184 
apply (blast dest!: aux [THEN iffD1]) 

185 
apply atomize 

186 
apply (erule_tac V = "ALL A. ?PP (A)" in thin_rl) 

187 
apply (frule subsetD [OF equalityD2 insertI1]) 

188 
apply clarify 

189 
apply (rule_tac x = xa in bexI) 

190 
apply (simp_all add: inj_on_image_set_diff) 

191 
done 

192 
qed (rule refl) 

193 

194 

195 
subsubsection {* The finite UNION of finite sets *} 

196 

197 
lemma finite_UN_I: "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)" 

198 
by (induct set: Finites) simp_all 

199 

200 
text {* 

201 
Strengthen RHS to 

202 
@{prop "((ALL x:A. finite (B x)) & finite {x. x:A & B x ~= {}})"}? 

203 

204 
We'd need to prove 

205 
@{prop "finite C ==> ALL A B. (UNION A B) <= C > finite {x. x:A & B x ~= {}}"} 

206 
by induction. *} 

207 

208 
lemma finite_UN [simp]: "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))" 

209 
by (blast intro: finite_UN_I finite_subset) 

210 

211 

212 
subsubsection {* Sigma of finite sets *} 

213 

214 
lemma finite_SigmaI [simp]: 

215 
"finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (SIGMA a:A. B a)" 

216 
by (unfold Sigma_def) (blast intro!: finite_UN_I) 

217 

218 
lemma finite_Prod_UNIV: 

219 
"finite (UNIV::'a set) ==> finite (UNIV::'b set) ==> finite (UNIV::('a * 'b) set)" 

220 
apply (subgoal_tac "(UNIV:: ('a * 'b) set) = Sigma UNIV (%x. UNIV)") 

221 
apply (erule ssubst) 

222 
apply (erule finite_SigmaI) 

223 
apply auto 

224 
done 

225 

226 
instance unit :: finite 

227 
proof 

228 
have "finite {()}" by simp 

229 
also have "{()} = UNIV" by auto 

230 
finally show "finite (UNIV :: unit set)" . 

231 
qed 

232 

233 
instance * :: (finite, finite) finite 

234 
proof 

235 
show "finite (UNIV :: ('a \<times> 'b) set)" 

236 
proof (rule finite_Prod_UNIV) 

237 
show "finite (UNIV :: 'a set)" by (rule finite) 

238 
show "finite (UNIV :: 'b set)" by (rule finite) 

239 
qed 

240 
qed 

241 

242 

243 
subsubsection {* The powerset of a finite set *} 

244 

245 
lemma finite_Pow_iff [iff]: "finite (Pow A) = finite A" 

246 
proof 

247 
assume "finite (Pow A)" 

248 
with _ have "finite ((%x. {x}) ` A)" by (rule finite_subset) blast 

249 
thus "finite A" by (rule finite_imageD [unfolded inj_on_def]) simp 

250 
next 

251 
assume "finite A" 

252 
thus "finite (Pow A)" 

253 
by induct (simp_all add: finite_UnI finite_imageI Pow_insert) 

254 
qed 

255 

256 
lemma finite_converse [iff]: "finite (r^1) = finite r" 

257 
apply (subgoal_tac "r^1 = (%(x,y). (y,x))`r") 

258 
apply simp 

259 
apply (rule iffI) 

260 
apply (erule finite_imageD [unfolded inj_on_def]) 

261 
apply (simp split add: split_split) 

262 
apply (erule finite_imageI) 

263 
apply (simp add: converse_def image_def) 

264 
apply auto 

265 
apply (rule bexI) 

266 
prefer 2 apply assumption 

267 
apply simp 

268 
done 

269 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12718
diff
changeset

270 
lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..k(}" 
12396  271 
by (induct k) (simp_all add: lessThan_Suc) 
272 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12718
diff
changeset

273 
lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}" 
12396  274 
by (induct k) (simp_all add: atMost_Suc) 
275 

276 
lemma bounded_nat_set_is_finite: 

277 
"(ALL i:N. i < (n::nat)) ==> finite N" 

278 
 {* A bounded set of natural numbers is finite. *} 

279 
apply (rule finite_subset) 

280 
apply (rule_tac [2] finite_lessThan) 

281 
apply auto 

282 
done 

283 

284 

285 
subsubsection {* Finiteness of transitive closure *} 

286 

287 
text {* (Thanks to Sidi Ehmety) *} 

288 

289 
lemma finite_Field: "finite r ==> finite (Field r)" 

290 
 {* A finite relation has a finite field (@{text "= domain \<union> range"}. *} 

291 
apply (induct set: Finites) 

292 
apply (auto simp add: Field_def Domain_insert Range_insert) 

293 
done 

294 

295 
lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r" 

296 
apply clarify 

297 
apply (erule trancl_induct) 

298 
apply (auto simp add: Field_def) 

299 
done 

300 

301 
lemma finite_trancl: "finite (r^+) = finite r" 

302 
apply auto 

303 
prefer 2 

304 
apply (rule trancl_subset_Field2 [THEN finite_subset]) 

305 
apply (rule finite_SigmaI) 

306 
prefer 3 

13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
13595
diff
changeset

307 
apply (blast intro: r_into_trancl' finite_subset) 
12396  308 
apply (auto simp add: finite_Field) 
309 
done 

310 

311 

312 
subsection {* Finite cardinality *} 

313 

314 
text {* 

315 
This definition, although traditional, is ugly to work with: @{text 

316 
"card A == LEAST n. EX f. A = {f i  i. i < n}"}. Therefore we have 

317 
switched to an inductive one: 

318 
*} 

319 

320 
consts cardR :: "('a set \<times> nat) set" 

321 

322 
inductive cardR 

323 
intros 

324 
EmptyI: "({}, 0) : cardR" 

325 
InsertI: "(A, n) : cardR ==> a \<notin> A ==> (insert a A, Suc n) : cardR" 

326 

327 
constdefs 

328 
card :: "'a set => nat" 

329 
"card A == THE n. (A, n) : cardR" 

330 

331 
inductive_cases cardR_emptyE: "({}, n) : cardR" 

332 
inductive_cases cardR_insertE: "(insert a A,n) : cardR" 

333 

334 
lemma cardR_SucD: "(A, n) : cardR ==> a : A > (EX m. n = Suc m)" 

335 
by (induct set: cardR) simp_all 

336 

337 
lemma cardR_determ_aux1: 

338 
"(A, m): cardR ==> (!!n a. m = Suc n ==> a:A ==> (A  {a}, n) : cardR)" 

339 
apply (induct set: cardR) 

340 
apply auto 

341 
apply (simp add: insert_Diff_if) 

342 
apply auto 

343 
apply (drule cardR_SucD) 

344 
apply (blast intro!: cardR.intros) 

345 
done 

346 

347 
lemma cardR_determ_aux2: "(insert a A, Suc m) : cardR ==> a \<notin> A ==> (A, m) : cardR" 

348 
by (drule cardR_determ_aux1) auto 

349 

350 
lemma cardR_determ: "(A, m): cardR ==> (!!n. (A, n) : cardR ==> n = m)" 

351 
apply (induct set: cardR) 

352 
apply (safe elim!: cardR_emptyE cardR_insertE) 

353 
apply (rename_tac B b m) 

354 
apply (case_tac "a = b") 

355 
apply (subgoal_tac "A = B") 

356 
prefer 2 apply (blast elim: equalityE) 

357 
apply blast 

358 
apply (subgoal_tac "EX C. A = insert b C & B = insert a C") 

359 
prefer 2 

360 
apply (rule_tac x = "A Int B" in exI) 

361 
apply (blast elim: equalityE) 

362 
apply (frule_tac A = B in cardR_SucD) 

363 
apply (blast intro!: cardR.intros dest!: cardR_determ_aux2) 

364 
done 

365 

366 
lemma cardR_imp_finite: "(A, n) : cardR ==> finite A" 

367 
by (induct set: cardR) simp_all 

368 

369 
lemma finite_imp_cardR: "finite A ==> EX n. (A, n) : cardR" 

370 
by (induct set: Finites) (auto intro!: cardR.intros) 

371 

372 
lemma card_equality: "(A,n) : cardR ==> card A = n" 

373 
by (unfold card_def) (blast intro: cardR_determ) 

374 

375 
lemma card_empty [simp]: "card {} = 0" 

376 
by (unfold card_def) (blast intro!: cardR.intros elim!: cardR_emptyE) 

377 

378 
lemma card_insert_disjoint [simp]: 

379 
"finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)" 

380 
proof  

381 
assume x: "x \<notin> A" 

382 
hence aux: "!!n. ((insert x A, n) : cardR) = (EX m. (A, m) : cardR & n = Suc m)" 

383 
apply (auto intro!: cardR.intros) 

384 
apply (rule_tac A1 = A in finite_imp_cardR [THEN exE]) 

385 
apply (force dest: cardR_imp_finite) 

386 
apply (blast intro!: cardR.intros intro: cardR_determ) 

387 
done 

388 
assume "finite A" 

389 
thus ?thesis 

390 
apply (simp add: card_def aux) 

391 
apply (rule the_equality) 

392 
apply (auto intro: finite_imp_cardR 

393 
cong: conj_cong simp: card_def [symmetric] card_equality) 

394 
done 

395 
qed 

396 

397 
lemma card_0_eq [simp]: "finite A ==> (card A = 0) = (A = {})" 

398 
apply auto 

399 
apply (drule_tac a = x in mk_disjoint_insert) 

400 
apply clarify 

401 
apply (rotate_tac 1) 

402 
apply auto 

403 
done 

404 

405 
lemma card_insert_if: 

406 
"finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))" 

407 
by (simp add: insert_absorb) 

408 

409 
lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A  {x})) = card A" 

410 
apply (rule_tac t = A in insert_Diff [THEN subst]) 

411 
apply assumption 

412 
apply simp 

413 
done 

414 

415 
lemma card_Diff_singleton: 

416 
"finite A ==> x: A ==> card (A  {x}) = card A  1" 

417 
by (simp add: card_Suc_Diff1 [symmetric]) 

418 

419 
lemma card_Diff_singleton_if: 

420 
"finite A ==> card (A{x}) = (if x : A then card A  1 else card A)" 

421 
by (simp add: card_Diff_singleton) 

422 

423 
lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A  {x}))" 

424 
by (simp add: card_insert_if card_Suc_Diff1) 

425 

426 
lemma card_insert_le: "finite A ==> card A <= card (insert x A)" 

427 
by (simp add: card_insert_if) 

428 

429 
lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)" 

430 
apply (induct set: Finites) 

431 
apply simp 

432 
apply clarify 

433 
apply (subgoal_tac "finite A & A  {x} <= F") 

434 
prefer 2 apply (blast intro: finite_subset) 

435 
apply atomize 

436 
apply (drule_tac x = "A  {x}" in spec) 

437 
apply (simp add: card_Diff_singleton_if split add: split_if_asm) 

438 
apply (case_tac "card A") 

439 
apply auto 

440 
done 

441 

442 
lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B" 

443 
apply (simp add: psubset_def linorder_not_le [symmetric]) 

444 
apply (blast dest: card_seteq) 

445 
done 

446 

447 
lemma card_mono: "finite B ==> A <= B ==> card A <= card B" 

448 
apply (case_tac "A = B") 

449 
apply simp 

450 
apply (simp add: linorder_not_less [symmetric]) 

451 
apply (blast dest: card_seteq intro: order_less_imp_le) 

452 
done 

453 

454 
lemma card_Un_Int: "finite A ==> finite B 

455 
==> card A + card B = card (A Un B) + card (A Int B)" 

456 
apply (induct set: Finites) 

457 
apply simp 

458 
apply (simp add: insert_absorb Int_insert_left) 

459 
done 

460 

461 
lemma card_Un_disjoint: "finite A ==> finite B 

462 
==> A Int B = {} ==> card (A Un B) = card A + card B" 

463 
by (simp add: card_Un_Int) 

464 

465 
lemma card_Diff_subset: 

466 
"finite A ==> B <= A ==> card A  card B = card (A  B)" 

467 
apply (subgoal_tac "(A  B) Un B = A") 

468 
prefer 2 apply blast 

469 
apply (rule add_right_cancel [THEN iffD1]) 

470 
apply (rule card_Un_disjoint [THEN subst]) 

471 
apply (erule_tac [4] ssubst) 

472 
prefer 3 apply blast 

473 
apply (simp_all add: add_commute not_less_iff_le 

474 
add_diff_inverse card_mono finite_subset) 

475 
done 

476 

477 
lemma card_Diff1_less: "finite A ==> x: A ==> card (A  {x}) < card A" 

478 
apply (rule Suc_less_SucD) 

479 
apply (simp add: card_Suc_Diff1) 

480 
done 

481 

482 
lemma card_Diff2_less: 

483 
"finite A ==> x: A ==> y: A ==> card (A  {x}  {y}) < card A" 

484 
apply (case_tac "x = y") 

485 
apply (simp add: card_Diff1_less) 

486 
apply (rule less_trans) 

487 
prefer 2 apply (auto intro!: card_Diff1_less) 

488 
done 

489 

490 
lemma card_Diff1_le: "finite A ==> card (A  {x}) <= card A" 

491 
apply (case_tac "x : A") 

492 
apply (simp_all add: card_Diff1_less less_imp_le) 

493 
done 

494 

495 
lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B" 

496 
apply (erule psubsetI) 

497 
apply blast 

498 
done 

499 

500 

501 
subsubsection {* Cardinality of image *} 

502 

503 
lemma card_image_le: "finite A ==> card (f ` A) <= card A" 

504 
apply (induct set: Finites) 

505 
apply simp 

506 
apply (simp add: le_SucI finite_imageI card_insert_if) 

507 
done 

508 

509 
lemma card_image: "finite A ==> inj_on f A ==> card (f ` A) = card A" 

510 
apply (induct set: Finites) 

511 
apply simp_all 

512 
apply atomize 

513 
apply safe 

514 
apply (unfold inj_on_def) 

515 
apply blast 

516 
apply (subst card_insert_disjoint) 

517 
apply (erule finite_imageI) 

518 
apply blast 

519 
apply blast 

520 
done 

521 

522 
lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A" 

523 
by (simp add: card_seteq card_image) 

524 

525 

526 
subsubsection {* Cardinality of the Powerset *} 

527 

528 
lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A" (* FIXME numeral 2 (!?) *) 

529 
apply (induct set: Finites) 

530 
apply (simp_all add: Pow_insert) 

531 
apply (subst card_Un_disjoint) 

532 
apply blast 

533 
apply (blast intro: finite_imageI) 

534 
apply blast 

535 
apply (subgoal_tac "inj_on (insert x) (Pow F)") 

536 
apply (simp add: card_image Pow_insert) 

537 
apply (unfold inj_on_def) 

538 
apply (blast elim!: equalityE) 

539 
done 

540 

541 
text {* 

542 
\medskip Relates to equivalence classes. Based on a theorem of 

543 
F. Kammüller's. The @{prop "finite C"} premise is redundant. 

544 
*} 

545 

546 
lemma dvd_partition: 

547 
"finite C ==> finite (Union C) ==> 

548 
ALL c : C. k dvd card c ==> 

549 
(ALL c1: C. ALL c2: C. c1 ~= c2 > c1 Int c2 = {}) ==> 

550 
k dvd card (Union C)" 

551 
apply (induct set: Finites) 

552 
apply simp_all 

553 
apply clarify 

554 
apply (subst card_Un_disjoint) 

555 
apply (auto simp add: dvd_add disjoint_eq_subset_Compl) 

556 
done 

557 

558 

559 
subsection {* A fold functional for finite sets *} 

560 

561 
text {* 

562 
For @{text n} nonnegative we have @{text "fold f e {x1, ..., xn} = 

563 
f x1 (... (f xn e))"} where @{text f} is at least leftcommutative. 

564 
*} 

565 

566 
consts 

567 
foldSet :: "('b => 'a => 'a) => 'a => ('b set \<times> 'a) set" 

568 

569 
inductive "foldSet f e" 

570 
intros 

571 
emptyI [intro]: "({}, e) : foldSet f e" 

572 
insertI [intro]: "x \<notin> A ==> (A, y) : foldSet f e ==> (insert x A, f x y) : foldSet f e" 

573 

574 
inductive_cases empty_foldSetE [elim!]: "({}, x) : foldSet f e" 

575 

576 
constdefs 

577 
fold :: "('b => 'a => 'a) => 'a => 'b set => 'a" 

578 
"fold f e A == THE x. (A, x) : foldSet f e" 

579 

580 
lemma Diff1_foldSet: "(A  {x}, y) : foldSet f e ==> x: A ==> (A, f x y) : foldSet f e" 

581 
apply (erule insert_Diff [THEN subst], rule foldSet.intros) 

582 
apply auto 

583 
done 

584 

585 
lemma foldSet_imp_finite [simp]: "(A, x) : foldSet f e ==> finite A" 

586 
by (induct set: foldSet) auto 

587 

588 
lemma finite_imp_foldSet: "finite A ==> EX x. (A, x) : foldSet f e" 

589 
by (induct set: Finites) auto 

590 

591 

592 
subsubsection {* Leftcommutative operations *} 

593 

594 
locale LC = 

595 
fixes f :: "'b => 'a => 'a" (infixl "\<cdot>" 70) 

596 
assumes left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)" 

597 

598 
lemma (in LC) foldSet_determ_aux: 

599 
"ALL A x. card A < n > (A, x) : foldSet f e > 

600 
(ALL y. (A, y) : foldSet f e > y = x)" 

601 
apply (induct n) 

602 
apply (auto simp add: less_Suc_eq) 

603 
apply (erule foldSet.cases) 

604 
apply blast 

605 
apply (erule foldSet.cases) 

606 
apply blast 

607 
apply clarify 

608 
txt {* force simplification of @{text "card A < card (insert ...)"}. *} 

609 
apply (erule rev_mp) 

610 
apply (simp add: less_Suc_eq_le) 

611 
apply (rule impI) 

612 
apply (rename_tac Aa xa ya Ab xb yb, case_tac "xa = xb") 

613 
apply (subgoal_tac "Aa = Ab") 

614 
prefer 2 apply (blast elim!: equalityE) 

615 
apply blast 

616 
txt {* case @{prop "xa \<notin> xb"}. *} 

617 
apply (subgoal_tac "Aa  {xb} = Ab  {xa} & xb : Aa & xa : Ab") 

618 
prefer 2 apply (blast elim!: equalityE) 

619 
apply clarify 

620 
apply (subgoal_tac "Aa = insert xb Ab  {xa}") 

621 
prefer 2 apply blast 

622 
apply (subgoal_tac "card Aa <= card Ab") 

623 
prefer 2 

624 
apply (rule Suc_le_mono [THEN subst]) 

625 
apply (simp add: card_Suc_Diff1) 

626 
apply (rule_tac A1 = "Aa  {xb}" and f1 = f in finite_imp_foldSet [THEN exE]) 

627 
apply (blast intro: foldSet_imp_finite finite_Diff) 

628 
apply (frule (1) Diff1_foldSet) 

629 
apply (subgoal_tac "ya = f xb x") 

630 
prefer 2 apply (blast del: equalityCE) 

631 
apply (subgoal_tac "(Ab  {xa}, x) : foldSet f e") 

632 
prefer 2 apply simp 

633 
apply (subgoal_tac "yb = f xa x") 

634 
prefer 2 apply (blast del: equalityCE dest: Diff1_foldSet) 

635 
apply (simp (no_asm_simp) add: left_commute) 

636 
done 

637 

638 
lemma (in LC) foldSet_determ: "(A, x) : foldSet f e ==> (A, y) : foldSet f e ==> y = x" 

639 
by (blast intro: foldSet_determ_aux [rule_format]) 

640 

641 
lemma (in LC) fold_equality: "(A, y) : foldSet f e ==> fold f e A = y" 

642 
by (unfold fold_def) (blast intro: foldSet_determ) 

643 

644 
lemma fold_empty [simp]: "fold f e {} = e" 

645 
by (unfold fold_def) blast 

646 

647 
lemma (in LC) fold_insert_aux: "x \<notin> A ==> 

648 
((insert x A, v) : foldSet f e) = 

649 
(EX y. (A, y) : foldSet f e & v = f x y)" 

650 
apply auto 

651 
apply (rule_tac A1 = A and f1 = f in finite_imp_foldSet [THEN exE]) 

652 
apply (fastsimp dest: foldSet_imp_finite) 

653 
apply (blast intro: foldSet_determ) 

654 
done 

655 

656 
lemma (in LC) fold_insert: 

657 
"finite A ==> x \<notin> A ==> fold f e (insert x A) = f x (fold f e A)" 

658 
apply (unfold fold_def) 

659 
apply (simp add: fold_insert_aux) 

660 
apply (rule the_equality) 

661 
apply (auto intro: finite_imp_foldSet 

662 
cong add: conj_cong simp add: fold_def [symmetric] fold_equality) 

663 
done 

664 

665 
lemma (in LC) fold_commute: "finite A ==> (!!e. f x (fold f e A) = fold f (f x e) A)" 

666 
apply (induct set: Finites) 

667 
apply simp 

668 
apply (simp add: left_commute fold_insert) 

669 
done 

670 

671 
lemma (in LC) fold_nest_Un_Int: 

672 
"finite A ==> finite B 

673 
==> fold f (fold f e B) A = fold f (fold f e (A Int B)) (A Un B)" 

674 
apply (induct set: Finites) 

675 
apply simp 

676 
apply (simp add: fold_insert fold_commute Int_insert_left insert_absorb) 

677 
done 

678 

679 
lemma (in LC) fold_nest_Un_disjoint: 

680 
"finite A ==> finite B ==> A Int B = {} 

681 
==> fold f e (A Un B) = fold f (fold f e B) A" 

682 
by (simp add: fold_nest_Un_Int) 

683 

684 
declare foldSet_imp_finite [simp del] 

685 
empty_foldSetE [rule del] foldSet.intros [rule del] 

686 
 {* Delete rules to do with @{text foldSet} relation. *} 

687 

688 

689 

690 
subsubsection {* Commutative monoids *} 

691 

692 
text {* 

693 
We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"} 

694 
instead of @{text "'b => 'a => 'a"}. 

695 
*} 

696 

697 
locale ACe = 

698 
fixes f :: "'a => 'a => 'a" (infixl "\<cdot>" 70) 

699 
and e :: 'a 

700 
assumes ident [simp]: "x \<cdot> e = x" 

701 
and commute: "x \<cdot> y = y \<cdot> x" 

702 
and assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" 

703 

704 
lemma (in ACe) left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)" 

705 
proof  

706 
have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp only: commute) 

707 
also have "... = y \<cdot> (z \<cdot> x)" by (simp only: assoc) 

708 
also have "z \<cdot> x = x \<cdot> z" by (simp only: commute) 

709 
finally show ?thesis . 

710 
qed 

711 

12718  712 
lemmas (in ACe) AC = assoc commute left_commute 
12396  713 

12693  714 
lemma (in ACe) left_ident [simp]: "e \<cdot> x = x" 
12396  715 
proof  
716 
have "x \<cdot> e = x" by (rule ident) 

717 
thus ?thesis by (subst commute) 

718 
qed 

719 

720 
lemma (in ACe) fold_Un_Int: 

721 
"finite A ==> finite B ==> 

722 
fold f e A \<cdot> fold f e B = fold f e (A Un B) \<cdot> fold f e (A Int B)" 

723 
apply (induct set: Finites) 

724 
apply simp 

13400  725 
apply (simp add: AC insert_absorb Int_insert_left 
13421  726 
LC.fold_insert [OF LC.intro]) 
12396  727 
done 
728 

729 
lemma (in ACe) fold_Un_disjoint: 

730 
"finite A ==> finite B ==> A Int B = {} ==> 

731 
fold f e (A Un B) = fold f e A \<cdot> fold f e B" 

732 
by (simp add: fold_Un_Int) 

733 

734 
lemma (in ACe) fold_Un_disjoint2: 

735 
"finite A ==> finite B ==> A Int B = {} ==> 

736 
fold (f o g) e (A Un B) = fold (f o g) e A \<cdot> fold (f o g) e B" 

737 
proof  

738 
assume b: "finite B" 

739 
assume "finite A" 

740 
thus "A Int B = {} ==> 

741 
fold (f o g) e (A Un B) = fold (f o g) e A \<cdot> fold (f o g) e B" 

742 
proof induct 

743 
case empty 

744 
thus ?case by simp 

745 
next 

746 
case (insert F x) 

13571  747 
have "fold (f o g) e (insert x F \<union> B) = fold (f o g) e (insert x (F \<union> B))" 
12396  748 
by simp 
13571  749 
also have "... = (f o g) x (fold (f o g) e (F \<union> B))" 
13400  750 
by (rule LC.fold_insert [OF LC.intro]) 
13421  751 
(insert b insert, auto simp add: left_commute) 
13571  752 
also from insert have "fold (f o g) e (F \<union> B) = 
753 
fold (f o g) e F \<cdot> fold (f o g) e B" by blast 

754 
also have "(f o g) x ... = (f o g) x (fold (f o g) e F) \<cdot> fold (f o g) e B" 

12396  755 
by (simp add: AC) 
13571  756 
also have "(f o g) x (fold (f o g) e F) = fold (f o g) e (insert x F)" 
13400  757 
by (rule LC.fold_insert [OF LC.intro, symmetric]) (insert b insert, 
13421  758 
auto simp add: left_commute) 
12396  759 
finally show ?case . 
760 
qed 

761 
qed 

762 

763 

764 
subsection {* Generalized summation over a set *} 

765 

766 
constdefs 

767 
setsum :: "('a => 'b) => 'a set => 'b::plus_ac0" 

768 
"setsum f A == if finite A then fold (op + o f) 0 A else 0" 

769 

770 
syntax 

771 
"_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("\<Sum>_:_. _" [0, 51, 10] 10) 

772 
syntax (xsymbols) 

773 
"_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("\<Sum>_\<in>_. _" [0, 51, 10] 10) 

774 
translations 

775 
"\<Sum>i:A. b" == "setsum (%i. b) A"  {* Beware of argument permutation! *} 

776 

777 

778 
lemma setsum_empty [simp]: "setsum f {} = 0" 

779 
by (simp add: setsum_def) 

780 

781 
lemma setsum_insert [simp]: 

782 
"finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F" 

13365  783 
by (simp add: setsum_def 
13421  784 
LC.fold_insert [OF LC.intro] plus_ac0_left_commute) 
12396  785 

786 
lemma setsum_0: "setsum (\<lambda>i. 0) A = 0" 

787 
apply (case_tac "finite A") 

788 
prefer 2 apply (simp add: setsum_def) 

789 
apply (erule finite_induct) 

790 
apply auto 

791 
done 

792 

793 
lemma setsum_eq_0_iff [simp]: 

794 
"finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))" 

795 
by (induct set: Finites) auto 

796 

797 
lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a" 

798 
apply (case_tac "finite A") 

799 
prefer 2 apply (simp add: setsum_def) 

800 
apply (erule rev_mp) 

801 
apply (erule finite_induct) 

802 
apply auto 

803 
done 

804 

805 
lemma card_eq_setsum: "finite A ==> card A = setsum (\<lambda>x. 1) A" 

806 
 {* Could allow many @{text "card"} proofs to be simplified. *} 

807 
by (induct set: Finites) auto 

808 

809 
lemma setsum_Un_Int: "finite A ==> finite B 

810 
==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B" 

811 
 {* The reversed orientation looks more natural, but LOOPS as a simprule! *} 

812 
apply (induct set: Finites) 

813 
apply simp 

814 
apply (simp add: plus_ac0 Int_insert_left insert_absorb) 

815 
done 

816 

817 
lemma setsum_Un_disjoint: "finite A ==> finite B 

818 
==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B" 

819 
apply (subst setsum_Un_Int [symmetric]) 

820 
apply auto 

821 
done 

822 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12718
diff
changeset

823 
lemma setsum_UN_disjoint: 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12718
diff
changeset

824 
fixes f :: "'a => 'b::plus_ac0" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12718
diff
changeset

825 
shows 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12718
diff
changeset

826 
"finite I ==> (ALL i:I. finite (A i)) ==> 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12718
diff
changeset

827 
(ALL i:I. ALL j:I. i \<noteq> j > A i Int A j = {}) ==> 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12718
diff
changeset

828 
setsum f (UNION I A) = setsum (\<lambda>i. setsum f (A i)) I" 
12396  829 
apply (induct set: Finites) 
830 
apply simp 

831 
apply atomize 

832 
apply (subgoal_tac "ALL i:F. x \<noteq> i") 

833 
prefer 2 apply blast 

834 
apply (subgoal_tac "A x Int UNION F A = {}") 

835 
prefer 2 apply blast 

836 
apply (simp add: setsum_Un_disjoint) 

837 
done 

838 

839 
lemma setsum_addf: "setsum (\<lambda>x. f x + g x) A = (setsum f A + setsum g A)" 

840 
apply (case_tac "finite A") 

841 
prefer 2 apply (simp add: setsum_def) 

842 
apply (erule finite_induct) 

843 
apply auto 

844 
apply (simp add: plus_ac0) 

845 
done 

846 

847 
lemma setsum_Un: "finite A ==> finite B ==> 

848 
(setsum f (A Un B) :: nat) = setsum f A + setsum f B  setsum f (A Int B)" 

849 
 {* For the natural numbers, we have subtraction. *} 

850 
apply (subst setsum_Un_Int [symmetric]) 

851 
apply auto 

852 
done 

853 

854 
lemma setsum_diff1: "(setsum f (A  {a}) :: nat) = 

855 
(if a:A then setsum f A  f a else setsum f A)" 

856 
apply (case_tac "finite A") 

857 
prefer 2 apply (simp add: setsum_def) 

858 
apply (erule finite_induct) 

859 
apply (auto simp add: insert_Diff_if) 

860 
apply (drule_tac a = a in mk_disjoint_insert) 

861 
apply auto 

862 
done 

863 

864 
lemma setsum_cong: 

865 
"A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B" 

866 
apply (case_tac "finite B") 

867 
prefer 2 apply (simp add: setsum_def) 

868 
apply simp 

869 
apply (subgoal_tac "ALL C. C <= B > (ALL x:C. f x = g x) > setsum f C = setsum g C") 

870 
apply simp 

871 
apply (erule finite_induct) 

872 
apply simp 

873 
apply (simp add: subset_insert_iff) 

874 
apply clarify 

875 
apply (subgoal_tac "finite C") 

876 
prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl]) 

877 
apply (subgoal_tac "C = insert x (C  {x})") 

878 
prefer 2 apply blast 

879 
apply (erule ssubst) 

880 
apply (drule spec) 

881 
apply (erule (1) notE impE) 

882 
apply (simp add: Ball_def) 

883 
done 

884 

13490
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

885 
subsubsection{* Min and Max of finite linearly ordered sets *} 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

886 

44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

887 
text{* Seemed easier to define directly than via fold. *} 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

888 

44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

889 
lemma ex_Max: fixes S :: "('a::linorder)set" 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

890 
assumes fin: "finite S" shows "S \<noteq> {} \<Longrightarrow> \<exists>m\<in>S. \<forall>s \<in> S. s \<le> m" 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

891 
using fin 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

892 
proof (induct) 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

893 
case empty thus ?case by simp 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

894 
next 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

895 
case (insert S x) 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

896 
show ?case 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

897 
proof (cases) 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

898 
assume "S = {}" thus ?thesis by simp 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

899 
next 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

900 
assume nonempty: "S \<noteq> {}" 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

901 
then obtain m where m: "m\<in>S" "\<forall>s\<in>S. s \<le> m" using insert by blast 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

902 
show ?thesis 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

903 
proof (cases) 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

904 
assume "x \<le> m" thus ?thesis using m by blast 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

905 
next 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

906 
assume "\<not> x \<le> m" thus ?thesis using m 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

907 
by(simp add:linorder_not_le order_less_le)(blast intro: order_trans) 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

908 
qed 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

909 
qed 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

910 
qed 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

911 

44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

912 
lemma ex_Min: fixes S :: "('a::linorder)set" 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

913 
assumes fin: "finite S" shows "S \<noteq> {} \<Longrightarrow> \<exists>m\<in>S. \<forall>s \<in> S. m \<le> s" 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

914 
using fin 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

915 
proof (induct) 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

916 
case empty thus ?case by simp 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

917 
next 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

918 
case (insert S x) 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

919 
show ?case 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

920 
proof (cases) 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

921 
assume "S = {}" thus ?thesis by simp 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

922 
next 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

923 
assume nonempty: "S \<noteq> {}" 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

924 
then obtain m where m: "m\<in>S" "\<forall>s\<in>S. m \<le> s" using insert by blast 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

925 
show ?thesis 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

926 
proof (cases) 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

927 
assume "m \<le> x" thus ?thesis using m by blast 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

928 
next 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

929 
assume "\<not> m \<le> x" thus ?thesis using m 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

930 
by(simp add:linorder_not_le order_less_le)(blast intro: order_trans) 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

931 
qed 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

932 
qed 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

933 
qed 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

934 

44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

935 
constdefs 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

936 
Min :: "('a::linorder)set \<Rightarrow> 'a" 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

937 
"Min S \<equiv> THE m. m \<in> S \<and> (\<forall>s \<in> S. m \<le> s)" 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

938 

44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

939 
Max :: "('a::linorder)set \<Rightarrow> 'a" 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

940 
"Max S \<equiv> THE m. m \<in> S \<and> (\<forall>s \<in> S. s \<le> m)" 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

941 

44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

942 
lemma Min[simp]: assumes a: "finite S" "S \<noteq> {}" 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

943 
shows "Min S \<in> S \<and> (\<forall>s \<in> S. Min S \<le> s)" (is "?P(Min S)") 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

944 
proof (unfold Min_def, rule theI') 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

945 
show "\<exists>!m. ?P m" 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

946 
proof (rule ex_ex1I) 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

947 
show "\<exists>m. ?P m" using ex_Min[OF a] by blast 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

948 
next 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

949 
fix m1 m2 assume "?P m1" "?P m2" 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

950 
thus "m1 = m2" by (blast dest:order_antisym) 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

951 
qed 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

952 
qed 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

953 

44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

954 
lemma Max[simp]: assumes a: "finite S" "S \<noteq> {}" 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

955 
shows "Max S \<in> S \<and> (\<forall>s \<in> S. s \<le> Max S)" (is "?P(Max S)") 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

956 
proof (unfold Max_def, rule theI') 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

957 
show "\<exists>!m. ?P m" 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

958 
proof (rule ex_ex1I) 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

959 
show "\<exists>m. ?P m" using ex_Max[OF a] by blast 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

960 
next 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

961 
fix m1 m2 assume "?P m1" "?P m2" 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

962 
thus "m1 = m2" by (blast dest:order_antisym) 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

963 
qed 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

964 
qed 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

965 

12396  966 

967 
text {* 

968 
\medskip Basic theorem about @{text "choose"}. By Florian 

969 
Kammüller, tidied by LCP. 

970 
*} 

971 

972 
lemma card_s_0_eq_empty: 

973 
"finite A ==> card {B. B \<subseteq> A & card B = 0} = 1" 

974 
apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq]) 

975 
apply (simp cong add: rev_conj_cong) 

976 
done 

977 

978 
lemma choose_deconstruct: "finite M ==> x \<notin> M 

979 
==> {s. s <= insert x M & card(s) = Suc k} 

980 
= {s. s <= M & card(s) = Suc k} Un 

981 
{s. EX t. t <= M & card(t) = k & s = insert x t}" 

982 
apply safe 

983 
apply (auto intro: finite_subset [THEN card_insert_disjoint]) 

984 
apply (drule_tac x = "xa  {x}" in spec) 

985 
apply (subgoal_tac "x ~: xa") 

986 
apply auto 

987 
apply (erule rev_mp, subst card_Diff_singleton) 

988 
apply (auto intro: finite_subset) 

989 
done 

990 

991 
lemma card_inj_on_le: 

13595  992 
"[inj_on f A; f ` A \<subseteq> B; finite A; finite B ] ==> card A <= card B" 
12396  993 
by (auto intro: card_mono simp add: card_image [symmetric]) 
994 

13595  995 
lemma card_bij_eq: 
996 
"[inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A; 

997 
finite A; finite B ] ==> card A = card B" 

12396  998 
by (auto intro: le_anti_sym card_inj_on_le) 
999 

13595  1000 
text{*There are as many subsets of @{term A} having cardinality @{term k} 
1001 
as there are sets obtained from the former by inserting a fixed element 

1002 
@{term x} into each.*} 

1003 
lemma constr_bij: 

1004 
"[finite A; x \<notin> A] ==> 

1005 
card {B. EX C. C <= A & card(C) = k & B = insert x C} = 

12396  1006 
card {B. B <= A & card(B) = k}" 
1007 
apply (rule_tac f = "%s. s  {x}" and g = "insert x" in card_bij_eq) 

13595  1008 
apply (auto elim!: equalityE simp add: inj_on_def) 
1009 
apply (subst Diff_insert0, auto) 

1010 
txt {* finiteness of the two sets *} 

1011 
apply (rule_tac [2] B = "Pow (A)" in finite_subset) 

1012 
apply (rule_tac B = "Pow (insert x A)" in finite_subset) 

1013 
apply fast+ 

12396  1014 
done 
1015 

1016 
text {* 

1017 
Main theorem: combinatorial statement about number of subsets of a set. 

1018 
*} 

1019 

1020 
lemma n_sub_lemma: 

1021 
"!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)" 

1022 
apply (induct k) 

1023 
apply (simp add: card_s_0_eq_empty) 

1024 
apply atomize 

1025 
apply (rotate_tac 1, erule finite_induct) 

13421  1026 
apply (simp_all (no_asm_simp) cong add: conj_cong 
1027 
add: card_s_0_eq_empty choose_deconstruct) 

12396  1028 
apply (subst card_Un_disjoint) 
1029 
prefer 4 apply (force simp add: constr_bij) 

1030 
prefer 3 apply force 

1031 
prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2] 

1032 
finite_subset [of _ "Pow (insert x F)", standard]) 

1033 
apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset]) 

1034 
done 

1035 

13421  1036 
theorem n_subsets: 
1037 
"finite A ==> card {B. B <= A & card B = k} = (card A choose k)" 

12396  1038 
by (simp add: n_sub_lemma) 
1039 

1040 
end 