author  nipkow 
Fri, 19 Dec 2003 04:28:45 +0100  
changeset 14302  6c24235e8d5d 
parent 14208  144f45277d5a 
child 14331  8dbbb7cf3637 
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" 

13737  14 
syntax 
15 
finite :: "'a set => bool" 

16 
translations 

17 
"finite A" == "A : Finites" 

12396  18 

19 
inductive Finites 

20 
intros 

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

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

23 

24 
axclass finite \<subseteq> type 

25 
finite: "finite UNIV" 

26 

13737  27 
lemma ex_new_if_finite:  "does not depend on def of finite at all" 
28 
"\<lbrakk> ~finite(UNIV::'a set); finite A \<rbrakk> \<Longrightarrow> \<exists>a::'a. a ~: A" 

29 
by(subgoal_tac "A ~= UNIV", blast, blast) 

30 

12396  31 

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

33 
"finite F ==> 

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

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

36 
proof  

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

12396  39 
assume "finite F" 
40 
thus "P F" 

41 
proof induct 

42 
show "P {}" . 

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

44 
show "P (insert x F)" 

45 
proof cases 

46 
assume "x \<in> F" 

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

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

49 
next 

50 
assume "x \<notin> F" 

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

52 
qed 

53 
qed 

54 
qed 

55 

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

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

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

59 
P F" 

60 
proof  

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

12396  63 
assume "finite F" 
64 
thus "F \<subseteq> A ==> P F" 

65 
proof induct 

66 
show "P {}" . 

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

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

69 
show "P (insert x F)" 

70 
proof (rule insert) 

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

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

73 
with P show "P F" . 

74 
qed 

75 
qed 

76 
qed 

77 

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

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

80 
by (induct set: Finites) simp_all 

81 

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

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

84 
proof  

85 
assume "finite B" 

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

87 
proof induct 

88 
case empty 

89 
thus ?case by simp 

90 
next 

91 
case (insert F x A) 

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

93 
show "finite A" 

94 
proof cases 

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

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

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

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

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

100 
finally show ?thesis . 

101 
next 

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

103 
assume "x \<notin> A" 

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

105 
qed 

106 
qed 

107 
qed 

108 

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

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

111 

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

113 
 {* The converse obviously fails. *} 

114 
by (blast intro: finite_subset) 

115 

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

117 
apply (subst insert_is_Un) 

14208  118 
apply (simp only: finite_Un, blast) 
12396  119 
done 
120 

121 
lemma finite_empty_induct: 

122 
"finite A ==> 

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

124 
proof  

125 
assume "finite A" 

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

127 
have "P (A  A)" 

128 
proof  

129 
fix c b :: "'a set" 

130 
presume c: "finite c" and b: "finite b" 

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

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

133 
proof induct 

134 
case empty 

135 
from P1 show ?case by simp 

136 
next 

137 
case (insert F x) 

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

139 
proof (rule P2) 

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

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

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

143 
qed 

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

145 
finally show ?case . 

146 
qed 

147 
next 

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

149 
qed 

150 
thus "P {}" by simp 

151 
qed 

152 

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

154 
by (rule Diff_subset [THEN finite_subset]) 

155 

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

157 
apply (subst Diff_insert) 

158 
apply (case_tac "a : A  B") 

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

14208  160 
apply (subst insert_Diff, simp_all) 
12396  161 
done 
162 

163 

13825  164 
subsubsection {* Image and Inverse Image over Finite Sets *} 
165 

166 
lemma finite_imageI[simp]: "finite F ==> finite (h ` F)" 

167 
 {* The image of a finite set is finite. *} 

168 
by (induct set: Finites) simp_all 

169 

170 
lemma finite_range_imageI: 

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

14208  172 
apply (drule finite_imageI, simp) 
13825  173 
done 
174 

12396  175 
lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A" 
176 
proof  

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

178 
fix B :: "'a set" 

179 
assume "finite B" 

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

181 
apply induct 

182 
apply simp 

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

184 
apply clarify 

185 
apply (simp (no_asm_use) add: inj_on_def) 

14208  186 
apply (blast dest!: aux [THEN iffD1], atomize) 
12396  187 
apply (erule_tac V = "ALL A. ?PP (A)" in thin_rl) 
14208  188 
apply (frule subsetD [OF equalityD2 insertI1], clarify) 
12396  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 

13825  195 
lemma inj_vimage_singleton: "inj f ==> f`{a} \<subseteq> {THE x. f x = a}" 
196 
 {* The inverse image of a singleton under an injective function 

197 
is included in a singleton. *} 

198 
apply (auto simp add: inj_on_def) 

199 
apply (blast intro: the_equality [symmetric]) 

200 
done 

201 

202 
lemma finite_vimageI: "[finite F; inj h] ==> finite (h ` F)" 

203 
 {* The inverse image of a finite set under an injective function 

204 
is finite. *} 

205 
apply (induct set: Finites, simp_all) 

206 
apply (subst vimage_insert) 

207 
apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton]) 

208 
done 

209 

210 

12396  211 
subsubsection {* The finite UNION of finite sets *} 
212 

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

214 
by (induct set: Finites) simp_all 

215 

216 
text {* 

217 
Strengthen RHS to 

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

219 

220 
We'd need to prove 

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

222 
by induction. *} 

223 

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

225 
by (blast intro: finite_UN_I finite_subset) 

226 

227 

228 
subsubsection {* Sigma of finite sets *} 

229 

230 
lemma finite_SigmaI [simp]: 

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

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

233 

234 
lemma finite_Prod_UNIV: 

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

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

237 
apply (erule ssubst) 

14208  238 
apply (erule finite_SigmaI, auto) 
12396  239 
done 
240 

241 
instance unit :: finite 

242 
proof 

243 
have "finite {()}" by simp 

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

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

246 
qed 

247 

248 
instance * :: (finite, finite) finite 

249 
proof 

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

251 
proof (rule finite_Prod_UNIV) 

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

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

254 
qed 

255 
qed 

256 

257 

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

259 

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

261 
proof 

262 
assume "finite (Pow A)" 

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

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

265 
next 

266 
assume "finite A" 

267 
thus "finite (Pow A)" 

268 
by induct (simp_all add: finite_UnI finite_imageI Pow_insert) 

269 
qed 

270 

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

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

273 
apply simp 

274 
apply (rule iffI) 

275 
apply (erule finite_imageD [unfolded inj_on_def]) 

276 
apply (simp split add: split_split) 

277 
apply (erule finite_imageI) 

14208  278 
apply (simp add: converse_def image_def, auto) 
12396  279 
apply (rule bexI) 
280 
prefer 2 apply assumption 

281 
apply simp 

282 
done 

283 

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

284 
lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..k(}" 
12396  285 
by (induct k) (simp_all add: lessThan_Suc) 
286 

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

287 
lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}" 
12396  288 
by (induct k) (simp_all add: atMost_Suc) 
289 

13735  290 
lemma finite_greaterThanLessThan [iff]: 
291 
fixes l :: nat shows "finite {)l..u(}" 

292 
by (simp add: greaterThanLessThan_def) 

293 

294 
lemma finite_atLeastLessThan [iff]: 

295 
fixes l :: nat shows "finite {l..u(}" 

296 
by (simp add: atLeastLessThan_def) 

297 

298 
lemma finite_greaterThanAtMost [iff]: 

299 
fixes l :: nat shows "finite {)l..u}" 

300 
by (simp add: greaterThanAtMost_def) 

301 

302 
lemma finite_atLeastAtMost [iff]: 

303 
fixes l :: nat shows "finite {l..u}" 

304 
by (simp add: atLeastAtMost_def) 

305 

12396  306 
lemma bounded_nat_set_is_finite: 
307 
"(ALL i:N. i < (n::nat)) ==> finite N" 

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

309 
apply (rule finite_subset) 

14208  310 
apply (rule_tac [2] finite_lessThan, auto) 
12396  311 
done 
312 

313 

314 
subsubsection {* Finiteness of transitive closure *} 

315 

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

317 

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

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

320 
apply (induct set: Finites) 

321 
apply (auto simp add: Field_def Domain_insert Range_insert) 

322 
done 

323 

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

325 
apply clarify 

326 
apply (erule trancl_induct) 

327 
apply (auto simp add: Field_def) 

328 
done 

329 

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

331 
apply auto 

332 
prefer 2 

333 
apply (rule trancl_subset_Field2 [THEN finite_subset]) 

334 
apply (rule finite_SigmaI) 

335 
prefer 3 

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

336 
apply (blast intro: r_into_trancl' finite_subset) 
12396  337 
apply (auto simp add: finite_Field) 
338 
done 

339 

340 

341 
subsection {* Finite cardinality *} 

342 

343 
text {* 

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

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

346 
switched to an inductive one: 

347 
*} 

348 

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

350 

351 
inductive cardR 

352 
intros 

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

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

355 

356 
constdefs 

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

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

359 

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

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

362 

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

364 
by (induct set: cardR) simp_all 

365 

366 
lemma cardR_determ_aux1: 

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

14208  368 
apply (induct set: cardR, auto) 
369 
apply (simp add: insert_Diff_if, auto) 

12396  370 
apply (drule cardR_SucD) 
371 
apply (blast intro!: cardR.intros) 

372 
done 

373 

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

375 
by (drule cardR_determ_aux1) auto 

376 

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

378 
apply (induct set: cardR) 

379 
apply (safe elim!: cardR_emptyE cardR_insertE) 

380 
apply (rename_tac B b m) 

381 
apply (case_tac "a = b") 

382 
apply (subgoal_tac "A = B") 

14208  383 
prefer 2 apply (blast elim: equalityE, blast) 
12396  384 
apply (subgoal_tac "EX C. A = insert b C & B = insert a C") 
385 
prefer 2 

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

387 
apply (blast elim: equalityE) 

388 
apply (frule_tac A = B in cardR_SucD) 

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

390 
done 

391 

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

393 
by (induct set: cardR) simp_all 

394 

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

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

397 

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

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

400 

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

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

403 

404 
lemma card_insert_disjoint [simp]: 

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

406 
proof  

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

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

409 
apply (auto intro!: cardR.intros) 

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

411 
apply (force dest: cardR_imp_finite) 

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

413 
done 

414 
assume "finite A" 

415 
thus ?thesis 

416 
apply (simp add: card_def aux) 

417 
apply (rule the_equality) 

418 
apply (auto intro: finite_imp_cardR 

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

420 
done 

421 
qed 

422 

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

424 
apply auto 

14208  425 
apply (drule_tac a = x in mk_disjoint_insert, clarify) 
426 
apply (rotate_tac 1, auto) 

12396  427 
done 
428 

429 
lemma card_insert_if: 

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

431 
by (simp add: insert_absorb) 

432 

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

14302  434 
apply(rule_tac t = A in insert_Diff [THEN subst], assumption) 
435 
apply(simp del:insert_Diff_single) 

436 
done 

12396  437 

438 
lemma card_Diff_singleton: 

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

440 
by (simp add: card_Suc_Diff1 [symmetric]) 

441 

442 
lemma card_Diff_singleton_if: 

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

444 
by (simp add: card_Diff_singleton) 

445 

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

447 
by (simp add: card_insert_if card_Suc_Diff1) 

448 

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

450 
by (simp add: card_insert_if) 

451 

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

14208  453 
apply (induct set: Finites, simp, clarify) 
12396  454 
apply (subgoal_tac "finite A & A  {x} <= F") 
14208  455 
prefer 2 apply (blast intro: finite_subset, atomize) 
12396  456 
apply (drule_tac x = "A  {x}" in spec) 
457 
apply (simp add: card_Diff_singleton_if split add: split_if_asm) 

14208  458 
apply (case_tac "card A", auto) 
12396  459 
done 
460 

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

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

463 
apply (blast dest: card_seteq) 

464 
done 

465 

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

14208  467 
apply (case_tac "A = B", simp) 
12396  468 
apply (simp add: linorder_not_less [symmetric]) 
469 
apply (blast dest: card_seteq intro: order_less_imp_le) 

470 
done 

471 

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

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

14208  474 
apply (induct set: Finites, simp) 
12396  475 
apply (simp add: insert_absorb Int_insert_left) 
476 
done 

477 

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

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

480 
by (simp add: card_Un_Int) 

481 

482 
lemma card_Diff_subset: 

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

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

485 
prefer 2 apply blast 

486 
apply (rule add_right_cancel [THEN iffD1]) 

487 
apply (rule card_Un_disjoint [THEN subst]) 

488 
apply (erule_tac [4] ssubst) 

489 
prefer 3 apply blast 

490 
apply (simp_all add: add_commute not_less_iff_le 

491 
add_diff_inverse card_mono finite_subset) 

492 
done 

493 

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

495 
apply (rule Suc_less_SucD) 

496 
apply (simp add: card_Suc_Diff1) 

497 
done 

498 

499 
lemma card_Diff2_less: 

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

501 
apply (case_tac "x = y") 

502 
apply (simp add: card_Diff1_less) 

503 
apply (rule less_trans) 

504 
prefer 2 apply (auto intro!: card_Diff1_less) 

505 
done 

506 

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

508 
apply (case_tac "x : A") 

509 
apply (simp_all add: card_Diff1_less less_imp_le) 

510 
done 

511 

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

14208  513 
by (erule psubsetI, blast) 
12396  514 

515 

516 
subsubsection {* Cardinality of image *} 

517 

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

14208  519 
apply (induct set: Finites, simp) 
12396  520 
apply (simp add: le_SucI finite_imageI card_insert_if) 
521 
done 

522 

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

14208  524 
apply (induct set: Finites, simp_all, atomize) 
12396  525 
apply safe 
14208  526 
apply (unfold inj_on_def, blast) 
12396  527 
apply (subst card_insert_disjoint) 
14208  528 
apply (erule finite_imageI, blast, blast) 
12396  529 
done 
530 

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

532 
by (simp add: card_seteq card_image) 

533 

534 

535 
subsubsection {* Cardinality of the Powerset *} 

536 

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

538 
apply (induct set: Finites) 

539 
apply (simp_all add: Pow_insert) 

14208  540 
apply (subst card_Un_disjoint, blast) 
541 
apply (blast intro: finite_imageI, blast) 

12396  542 
apply (subgoal_tac "inj_on (insert x) (Pow F)") 
543 
apply (simp add: card_image Pow_insert) 

544 
apply (unfold inj_on_def) 

545 
apply (blast elim!: equalityE) 

546 
done 

547 

548 
text {* 

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

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

551 
*} 

552 

553 
lemma dvd_partition: 

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

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

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

557 
k dvd card (Union C)" 

14208  558 
apply (induct set: Finites, simp_all, clarify) 
12396  559 
apply (subst card_Un_disjoint) 
560 
apply (auto simp add: dvd_add disjoint_eq_subset_Compl) 

561 
done 

562 

563 

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

565 

566 
text {* 

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

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

569 
*} 

570 

571 
consts 

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

573 

574 
inductive "foldSet f e" 

575 
intros 

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

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

578 

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

580 

581 
constdefs 

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

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

584 

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

14208  586 
by (erule insert_Diff [THEN subst], rule foldSet.intros, auto) 
12396  587 

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

589 
by (induct set: foldSet) auto 

590 

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

592 
by (induct set: Finites) auto 

593 

594 

595 
subsubsection {* Leftcommutative operations *} 

596 

597 
locale LC = 

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

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

600 

601 
lemma (in LC) foldSet_determ_aux: 

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

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

604 
apply (induct n) 

605 
apply (auto simp add: less_Suc_eq) 

14208  606 
apply (erule foldSet.cases, blast) 
607 
apply (erule foldSet.cases, blast, clarify) 

12396  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") 

14208  614 
prefer 2 apply (blast elim!: equalityE, blast) 
12396  615 
txt {* case @{prop "xa \<notin> xb"}. *} 
616 
apply (subgoal_tac "Aa  {xb} = Ab  {xa} & xb : Aa & xa : Ab") 

14208  617 
prefer 2 apply (blast elim!: equalityE, clarify) 
12396  618 
apply (subgoal_tac "Aa = insert xb Ab  {xa}") 
619 
prefer 2 apply blast 

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

621 
prefer 2 

622 
apply (rule Suc_le_mono [THEN subst]) 

623 
apply (simp add: card_Suc_Diff1) 

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

625 
apply (blast intro: foldSet_imp_finite finite_Diff) 

626 
apply (frule (1) Diff1_foldSet) 

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

628 
prefer 2 apply (blast del: equalityCE) 

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

630 
prefer 2 apply simp 

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

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

633 
apply (simp (no_asm_simp) add: left_commute) 

634 
done 

635 

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

637 
by (blast intro: foldSet_determ_aux [rule_format]) 

638 

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

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

641 

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

643 
by (unfold fold_def) blast 

644 

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

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

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

648 
apply auto 

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

650 
apply (fastsimp dest: foldSet_imp_finite) 

651 
apply (blast intro: foldSet_determ) 

652 
done 

653 

654 
lemma (in LC) fold_insert: 

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

656 
apply (unfold fold_def) 

657 
apply (simp add: fold_insert_aux) 

658 
apply (rule the_equality) 

659 
apply (auto intro: finite_imp_foldSet 

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

661 
done 

662 

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

14208  664 
apply (induct set: Finites, simp) 
12396  665 
apply (simp add: left_commute fold_insert) 
666 
done 

667 

668 
lemma (in LC) fold_nest_Un_Int: 

669 
"finite A ==> finite B 

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

14208  671 
apply (induct set: Finites, simp) 
12396  672 
apply (simp add: fold_insert fold_commute Int_insert_left insert_absorb) 
673 
done 

674 

675 
lemma (in LC) fold_nest_Un_disjoint: 

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

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

678 
by (simp add: fold_nest_Un_Int) 

679 

680 
declare foldSet_imp_finite [simp del] 

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

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

683 

684 

685 

686 
subsubsection {* Commutative monoids *} 

687 

688 
text {* 

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

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

691 
*} 

692 

693 
locale ACe = 

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

695 
and e :: 'a 

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

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

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

699 

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

701 
proof  

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

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

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

705 
finally show ?thesis . 

706 
qed 

707 

12718  708 
lemmas (in ACe) AC = assoc commute left_commute 
12396  709 

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

713 
thus ?thesis by (subst commute) 

714 
qed 

715 

716 
lemma (in ACe) fold_Un_Int: 

717 
"finite A ==> finite B ==> 

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

14208  719 
apply (induct set: Finites, simp) 
13400  720 
apply (simp add: AC insert_absorb Int_insert_left 
13421  721 
LC.fold_insert [OF LC.intro]) 
12396  722 
done 
723 

724 
lemma (in ACe) fold_Un_disjoint: 

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

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

727 
by (simp add: fold_Un_Int) 

728 

729 
lemma (in ACe) fold_Un_disjoint2: 

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

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

732 
proof  

733 
assume b: "finite B" 

734 
assume "finite A" 

735 
thus "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 induct 

738 
case empty 

739 
thus ?case by simp 

740 
next 

741 
case (insert F x) 

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

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

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

756 
qed 

757 

758 

759 
subsection {* Generalized summation over a set *} 

760 

761 
constdefs 

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

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

764 

765 
syntax 

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

767 
syntax (xsymbols) 

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

769 
translations 

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

771 

772 

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

774 
by (simp add: setsum_def) 

775 

776 
lemma setsum_insert [simp]: 

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

13365  778 
by (simp add: setsum_def 
13421  779 
LC.fold_insert [OF LC.intro] plus_ac0_left_commute) 
12396  780 

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

782 
apply (case_tac "finite A") 

783 
prefer 2 apply (simp add: setsum_def) 

14208  784 
apply (erule finite_induct, auto) 
12396  785 
done 
786 

787 
lemma setsum_eq_0_iff [simp]: 

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

789 
by (induct set: Finites) auto 

790 

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

792 
apply (case_tac "finite A") 

793 
prefer 2 apply (simp add: setsum_def) 

794 
apply (erule rev_mp) 

14208  795 
apply (erule finite_induct, auto) 
12396  796 
done 
797 

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

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

800 
by (induct set: Finites) auto 

801 

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

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

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

14208  805 
apply (induct set: Finites, simp) 
12396  806 
apply (simp add: plus_ac0 Int_insert_left insert_absorb) 
807 
done 

808 

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

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

14208  811 
apply (subst setsum_Un_Int [symmetric], auto) 
12396  812 
done 
813 

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

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

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

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

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

818 
(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

819 
setsum f (UNION I A) = setsum (\<lambda>i. setsum f (A i)) I" 
14208  820 
apply (induct set: Finites, simp, atomize) 
12396  821 
apply (subgoal_tac "ALL i:F. x \<noteq> i") 
822 
prefer 2 apply blast 

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

824 
prefer 2 apply blast 

825 
apply (simp add: setsum_Un_disjoint) 

826 
done 

827 

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

829 
apply (case_tac "finite A") 

830 
prefer 2 apply (simp add: setsum_def) 

14208  831 
apply (erule finite_induct, auto) 
12396  832 
apply (simp add: plus_ac0) 
833 
done 

834 

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

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

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

14208  838 
apply (subst setsum_Un_Int [symmetric], auto) 
12396  839 
done 
840 

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

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

843 
apply (case_tac "finite A") 

844 
prefer 2 apply (simp add: setsum_def) 

845 
apply (erule finite_induct) 

846 
apply (auto simp add: insert_Diff_if) 

14208  847 
apply (drule_tac a = a in mk_disjoint_insert, auto) 
12396  848 
done 
849 

850 
lemma setsum_cong: 

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

852 
apply (case_tac "finite B") 

14208  853 
prefer 2 apply (simp add: setsum_def, simp) 
12396  854 
apply (subgoal_tac "ALL C. C <= B > (ALL x:C. f x = g x) > setsum f C = setsum g C") 
855 
apply simp 

14208  856 
apply (erule finite_induct, simp) 
857 
apply (simp add: subset_insert_iff, clarify) 

12396  858 
apply (subgoal_tac "finite C") 
859 
prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl]) 

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

861 
prefer 2 apply blast 

862 
apply (erule ssubst) 

863 
apply (drule spec) 

864 
apply (erule (1) notE impE) 

14302  865 
apply (simp add: Ball_def del:insert_Diff_single) 
12396  866 
done 
867 

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

868 
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

869 

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

870 
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

871 

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

872 
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

873 
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

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

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

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

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

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

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

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

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

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

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

884 
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

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

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

887 
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

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

889 
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

890 
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

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

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

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

894 

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

895 
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

896 
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

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

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

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

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

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

902 
show ?case 
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 "S = {}" thus ?thesis by simp 
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 nonempty: "S \<noteq> {}" 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

907 
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

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

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

910 
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

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

912 
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

913 
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

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

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

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

917 

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

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

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

920 
"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

921 

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

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

923 
"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

924 

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

925 
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

926 
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

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

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

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

930 
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

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

932 
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

933 
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

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

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

936 

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

937 
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

938 
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

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

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

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

942 
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

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

944 
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

945 
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

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

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

948 

12396  949 

950 
text {* 

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

952 
Kammüller, tidied by LCP. 

953 
*} 

954 

955 
lemma card_s_0_eq_empty: 

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

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

958 
apply (simp cong add: rev_conj_cong) 

959 
done 

960 

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

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

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

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

965 
apply safe 

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

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

14208  968 
apply (subgoal_tac "x ~: xa", auto) 
12396  969 
apply (erule rev_mp, subst card_Diff_singleton) 
970 
apply (auto intro: finite_subset) 

971 
done 

972 

973 
lemma card_inj_on_le: 

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

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

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

12396  980 
by (auto intro: le_anti_sym card_inj_on_le) 
981 

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

984 
@{term x} into each.*} 

985 
lemma constr_bij: 

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

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

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

13595  990 
apply (auto elim!: equalityE simp add: inj_on_def) 
991 
apply (subst Diff_insert0, auto) 

992 
txt {* finiteness of the two sets *} 

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

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

995 
apply fast+ 

12396  996 
done 
997 

998 
text {* 

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

1000 
*} 

1001 

1002 
lemma n_sub_lemma: 

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

1004 
apply (induct k) 

14208  1005 
apply (simp add: card_s_0_eq_empty, atomize) 
12396  1006 
apply (rotate_tac 1, erule finite_induct) 
13421  1007 
apply (simp_all (no_asm_simp) cong add: conj_cong 
1008 
add: card_s_0_eq_empty choose_deconstruct) 

12396  1009 
apply (subst card_Un_disjoint) 
1010 
prefer 4 apply (force simp add: constr_bij) 

1011 
prefer 3 apply force 

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

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

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

1015 
done 

1016 

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

12396  1019 
by (simp add: n_sub_lemma) 
1020 

1021 
end 