author  paulson 
Thu, 20 Feb 2003 11:10:24 +0100  
changeset 13825  ef4c41e7956a 
parent 13737  e564c3d2d174 
child 14208  144f45277d5a 
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) 

118 
apply (simp only: finite_Un) 

119 
apply blast 

120 
done 

121 

122 
lemma finite_empty_induct: 

123 
"finite A ==> 

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

125 
proof  

126 
assume "finite A" 

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

128 
have "P (A  A)" 

129 
proof  

130 
fix c b :: "'a set" 

131 
presume c: "finite c" and b: "finite b" 

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

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

134 
proof induct 

135 
case empty 

136 
from P1 show ?case by simp 

137 
next 

138 
case (insert F x) 

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

140 
proof (rule P2) 

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

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

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

144 
qed 

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

146 
finally show ?case . 

147 
qed 

148 
next 

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

150 
qed 

151 
thus "P {}" by simp 

152 
qed 

153 

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

155 
by (rule Diff_subset [THEN finite_subset]) 

156 

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

158 
apply (subst Diff_insert) 

159 
apply (case_tac "a : A  B") 

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

161 
apply (subst insert_Diff) 

162 
apply simp_all 

163 
done 

164 

165 

13825  166 
subsubsection {* Image and Inverse Image over Finite Sets *} 
167 

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

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

170 
by (induct set: Finites) simp_all 

171 

172 
lemma finite_range_imageI: 

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

174 
apply (drule finite_imageI) 

175 
apply simp 

176 
done 

177 

12396  178 
lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A" 
179 
proof  

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

181 
fix B :: "'a set" 

182 
assume "finite B" 

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

184 
apply induct 

185 
apply simp 

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

187 
apply clarify 

188 
apply (simp (no_asm_use) add: inj_on_def) 

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

190 
apply atomize 

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

192 
apply (frule subsetD [OF equalityD2 insertI1]) 

193 
apply clarify 

194 
apply (rule_tac x = xa in bexI) 

195 
apply (simp_all add: inj_on_image_set_diff) 

196 
done 

197 
qed (rule refl) 

198 

199 

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

202 
is included in a singleton. *} 

203 
apply (auto simp add: inj_on_def) 

204 
apply (blast intro: the_equality [symmetric]) 

205 
done 

206 

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

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

209 
is finite. *} 

210 
apply (induct set: Finites, simp_all) 

211 
apply (subst vimage_insert) 

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

213 
done 

214 

215 

12396  216 
subsubsection {* The finite UNION of finite sets *} 
217 

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

219 
by (induct set: Finites) simp_all 

220 

221 
text {* 

222 
Strengthen RHS to 

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

224 

225 
We'd need to prove 

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

227 
by induction. *} 

228 

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

230 
by (blast intro: finite_UN_I finite_subset) 

231 

232 

233 
subsubsection {* Sigma of finite sets *} 

234 

235 
lemma finite_SigmaI [simp]: 

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

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

238 

239 
lemma finite_Prod_UNIV: 

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

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

242 
apply (erule ssubst) 

243 
apply (erule finite_SigmaI) 

244 
apply auto 

245 
done 

246 

247 
instance unit :: finite 

248 
proof 

249 
have "finite {()}" by simp 

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

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

252 
qed 

253 

254 
instance * :: (finite, finite) finite 

255 
proof 

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

257 
proof (rule finite_Prod_UNIV) 

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

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

260 
qed 

261 
qed 

262 

263 

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

265 

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

267 
proof 

268 
assume "finite (Pow A)" 

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

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

271 
next 

272 
assume "finite A" 

273 
thus "finite (Pow A)" 

274 
by induct (simp_all add: finite_UnI finite_imageI Pow_insert) 

275 
qed 

276 

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

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

279 
apply simp 

280 
apply (rule iffI) 

281 
apply (erule finite_imageD [unfolded inj_on_def]) 

282 
apply (simp split add: split_split) 

283 
apply (erule finite_imageI) 

284 
apply (simp add: converse_def image_def) 

285 
apply auto 

286 
apply (rule bexI) 

287 
prefer 2 apply assumption 

288 
apply simp 

289 
done 

290 

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

291 
lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..k(}" 
12396  292 
by (induct k) (simp_all add: lessThan_Suc) 
293 

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

294 
lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}" 
12396  295 
by (induct k) (simp_all add: atMost_Suc) 
296 

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

299 
by (simp add: greaterThanLessThan_def) 

300 

301 
lemma finite_atLeastLessThan [iff]: 

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

303 
by (simp add: atLeastLessThan_def) 

304 

305 
lemma finite_greaterThanAtMost [iff]: 

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

307 
by (simp add: greaterThanAtMost_def) 

308 

309 
lemma finite_atLeastAtMost [iff]: 

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

311 
by (simp add: atLeastAtMost_def) 

312 

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

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

316 
apply (rule finite_subset) 

317 
apply (rule_tac [2] finite_lessThan) 

318 
apply auto 

319 
done 

320 

321 

322 
subsubsection {* Finiteness of transitive closure *} 

323 

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

325 

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

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

328 
apply (induct set: Finites) 

329 
apply (auto simp add: Field_def Domain_insert Range_insert) 

330 
done 

331 

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

333 
apply clarify 

334 
apply (erule trancl_induct) 

335 
apply (auto simp add: Field_def) 

336 
done 

337 

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

339 
apply auto 

340 
prefer 2 

341 
apply (rule trancl_subset_Field2 [THEN finite_subset]) 

342 
apply (rule finite_SigmaI) 

343 
prefer 3 

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

344 
apply (blast intro: r_into_trancl' finite_subset) 
12396  345 
apply (auto simp add: finite_Field) 
346 
done 

347 

348 

349 
subsection {* Finite cardinality *} 

350 

351 
text {* 

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

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

354 
switched to an inductive one: 

355 
*} 

356 

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

358 

359 
inductive cardR 

360 
intros 

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

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

363 

364 
constdefs 

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

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

367 

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

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

370 

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

372 
by (induct set: cardR) simp_all 

373 

374 
lemma cardR_determ_aux1: 

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

376 
apply (induct set: cardR) 

377 
apply auto 

378 
apply (simp add: insert_Diff_if) 

379 
apply auto 

380 
apply (drule cardR_SucD) 

381 
apply (blast intro!: cardR.intros) 

382 
done 

383 

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

385 
by (drule cardR_determ_aux1) auto 

386 

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

388 
apply (induct set: cardR) 

389 
apply (safe elim!: cardR_emptyE cardR_insertE) 

390 
apply (rename_tac B b m) 

391 
apply (case_tac "a = b") 

392 
apply (subgoal_tac "A = B") 

393 
prefer 2 apply (blast elim: equalityE) 

394 
apply blast 

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

396 
prefer 2 

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

398 
apply (blast elim: equalityE) 

399 
apply (frule_tac A = B in cardR_SucD) 

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

401 
done 

402 

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

404 
by (induct set: cardR) simp_all 

405 

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

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

408 

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

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

411 

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

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

414 

415 
lemma card_insert_disjoint [simp]: 

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

417 
proof  

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

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

420 
apply (auto intro!: cardR.intros) 

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

422 
apply (force dest: cardR_imp_finite) 

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

424 
done 

425 
assume "finite A" 

426 
thus ?thesis 

427 
apply (simp add: card_def aux) 

428 
apply (rule the_equality) 

429 
apply (auto intro: finite_imp_cardR 

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

431 
done 

432 
qed 

433 

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

435 
apply auto 

436 
apply (drule_tac a = x in mk_disjoint_insert) 

437 
apply clarify 

438 
apply (rotate_tac 1) 

439 
apply auto 

440 
done 

441 

442 
lemma card_insert_if: 

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

444 
by (simp add: insert_absorb) 

445 

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

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

448 
apply assumption 

449 
apply simp 

450 
done 

451 

452 
lemma card_Diff_singleton: 

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

454 
by (simp add: card_Suc_Diff1 [symmetric]) 

455 

456 
lemma card_Diff_singleton_if: 

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

458 
by (simp add: card_Diff_singleton) 

459 

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

461 
by (simp add: card_insert_if card_Suc_Diff1) 

462 

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

464 
by (simp add: card_insert_if) 

465 

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

467 
apply (induct set: Finites) 

468 
apply simp 

469 
apply clarify 

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

471 
prefer 2 apply (blast intro: finite_subset) 

472 
apply atomize 

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

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

475 
apply (case_tac "card A") 

476 
apply auto 

477 
done 

478 

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

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

481 
apply (blast dest: card_seteq) 

482 
done 

483 

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

485 
apply (case_tac "A = B") 

486 
apply simp 

487 
apply (simp add: linorder_not_less [symmetric]) 

488 
apply (blast dest: card_seteq intro: order_less_imp_le) 

489 
done 

490 

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

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

493 
apply (induct set: Finites) 

494 
apply simp 

495 
apply (simp add: insert_absorb Int_insert_left) 

496 
done 

497 

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

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

500 
by (simp add: card_Un_Int) 

501 

502 
lemma card_Diff_subset: 

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

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

505 
prefer 2 apply blast 

506 
apply (rule add_right_cancel [THEN iffD1]) 

507 
apply (rule card_Un_disjoint [THEN subst]) 

508 
apply (erule_tac [4] ssubst) 

509 
prefer 3 apply blast 

510 
apply (simp_all add: add_commute not_less_iff_le 

511 
add_diff_inverse card_mono finite_subset) 

512 
done 

513 

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

515 
apply (rule Suc_less_SucD) 

516 
apply (simp add: card_Suc_Diff1) 

517 
done 

518 

519 
lemma card_Diff2_less: 

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

521 
apply (case_tac "x = y") 

522 
apply (simp add: card_Diff1_less) 

523 
apply (rule less_trans) 

524 
prefer 2 apply (auto intro!: card_Diff1_less) 

525 
done 

526 

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

528 
apply (case_tac "x : A") 

529 
apply (simp_all add: card_Diff1_less less_imp_le) 

530 
done 

531 

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

533 
apply (erule psubsetI) 

534 
apply blast 

535 
done 

536 

537 

538 
subsubsection {* Cardinality of image *} 

539 

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

541 
apply (induct set: Finites) 

542 
apply simp 

543 
apply (simp add: le_SucI finite_imageI card_insert_if) 

544 
done 

545 

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

547 
apply (induct set: Finites) 

548 
apply simp_all 

549 
apply atomize 

550 
apply safe 

551 
apply (unfold inj_on_def) 

552 
apply blast 

553 
apply (subst card_insert_disjoint) 

554 
apply (erule finite_imageI) 

555 
apply blast 

556 
apply blast 

557 
done 

558 

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

560 
by (simp add: card_seteq card_image) 

561 

562 

563 
subsubsection {* Cardinality of the Powerset *} 

564 

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

566 
apply (induct set: Finites) 

567 
apply (simp_all add: Pow_insert) 

568 
apply (subst card_Un_disjoint) 

569 
apply blast 

570 
apply (blast intro: finite_imageI) 

571 
apply blast 

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

573 
apply (simp add: card_image Pow_insert) 

574 
apply (unfold inj_on_def) 

575 
apply (blast elim!: equalityE) 

576 
done 

577 

578 
text {* 

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

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

581 
*} 

582 

583 
lemma dvd_partition: 

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

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

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

587 
k dvd card (Union C)" 

588 
apply (induct set: Finites) 

589 
apply simp_all 

590 
apply clarify 

591 
apply (subst card_Un_disjoint) 

592 
apply (auto simp add: dvd_add disjoint_eq_subset_Compl) 

593 
done 

594 

595 

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

597 

598 
text {* 

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

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

601 
*} 

602 

603 
consts 

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

605 

606 
inductive "foldSet f e" 

607 
intros 

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

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

610 

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

612 

613 
constdefs 

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

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

616 

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

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

619 
apply auto 

620 
done 

621 

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

623 
by (induct set: foldSet) auto 

624 

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

626 
by (induct set: Finites) auto 

627 

628 

629 
subsubsection {* Leftcommutative operations *} 

630 

631 
locale LC = 

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

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

634 

635 
lemma (in LC) foldSet_determ_aux: 

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

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

638 
apply (induct n) 

639 
apply (auto simp add: less_Suc_eq) 

640 
apply (erule foldSet.cases) 

641 
apply blast 

642 
apply (erule foldSet.cases) 

643 
apply blast 

644 
apply clarify 

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

646 
apply (erule rev_mp) 

647 
apply (simp add: less_Suc_eq_le) 

648 
apply (rule impI) 

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

650 
apply (subgoal_tac "Aa = Ab") 

651 
prefer 2 apply (blast elim!: equalityE) 

652 
apply blast 

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

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

655 
prefer 2 apply (blast elim!: equalityE) 

656 
apply clarify 

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

658 
prefer 2 apply blast 

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

660 
prefer 2 

661 
apply (rule Suc_le_mono [THEN subst]) 

662 
apply (simp add: card_Suc_Diff1) 

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

664 
apply (blast intro: foldSet_imp_finite finite_Diff) 

665 
apply (frule (1) Diff1_foldSet) 

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

667 
prefer 2 apply (blast del: equalityCE) 

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

669 
prefer 2 apply simp 

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

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

672 
apply (simp (no_asm_simp) add: left_commute) 

673 
done 

674 

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

676 
by (blast intro: foldSet_determ_aux [rule_format]) 

677 

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

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

680 

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

682 
by (unfold fold_def) blast 

683 

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

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

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

687 
apply auto 

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

689 
apply (fastsimp dest: foldSet_imp_finite) 

690 
apply (blast intro: foldSet_determ) 

691 
done 

692 

693 
lemma (in LC) fold_insert: 

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

695 
apply (unfold fold_def) 

696 
apply (simp add: fold_insert_aux) 

697 
apply (rule the_equality) 

698 
apply (auto intro: finite_imp_foldSet 

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

700 
done 

701 

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

703 
apply (induct set: Finites) 

704 
apply simp 

705 
apply (simp add: left_commute fold_insert) 

706 
done 

707 

708 
lemma (in LC) fold_nest_Un_Int: 

709 
"finite A ==> finite B 

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

711 
apply (induct set: Finites) 

712 
apply simp 

713 
apply (simp add: fold_insert fold_commute Int_insert_left insert_absorb) 

714 
done 

715 

716 
lemma (in LC) fold_nest_Un_disjoint: 

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

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

719 
by (simp add: fold_nest_Un_Int) 

720 

721 
declare foldSet_imp_finite [simp del] 

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

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

724 

725 

726 

727 
subsubsection {* Commutative monoids *} 

728 

729 
text {* 

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

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

732 
*} 

733 

734 
locale ACe = 

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

736 
and e :: 'a 

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

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

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

740 

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

742 
proof  

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

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

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

746 
finally show ?thesis . 

747 
qed 

748 

12718  749 
lemmas (in ACe) AC = assoc commute left_commute 
12396  750 

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

754 
thus ?thesis by (subst commute) 

755 
qed 

756 

757 
lemma (in ACe) fold_Un_Int: 

758 
"finite A ==> finite B ==> 

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

760 
apply (induct set: Finites) 

761 
apply simp 

13400  762 
apply (simp add: AC insert_absorb Int_insert_left 
13421  763 
LC.fold_insert [OF LC.intro]) 
12396  764 
done 
765 

766 
lemma (in ACe) fold_Un_disjoint: 

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

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

769 
by (simp add: fold_Un_Int) 

770 

771 
lemma (in ACe) fold_Un_disjoint2: 

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

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

774 
proof  

775 
assume b: "finite B" 

776 
assume "finite A" 

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

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

779 
proof induct 

780 
case empty 

781 
thus ?case by simp 

782 
next 

783 
case (insert F x) 

13571  784 
have "fold (f o g) e (insert x F \<union> B) = fold (f o g) e (insert x (F \<union> B))" 
12396  785 
by simp 
13571  786 
also have "... = (f o g) x (fold (f o g) e (F \<union> B))" 
13400  787 
by (rule LC.fold_insert [OF LC.intro]) 
13421  788 
(insert b insert, auto simp add: left_commute) 
13571  789 
also from insert have "fold (f o g) e (F \<union> B) = 
790 
fold (f o g) e F \<cdot> fold (f o g) e B" by blast 

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

12396  792 
by (simp add: AC) 
13571  793 
also have "(f o g) x (fold (f o g) e F) = fold (f o g) e (insert x F)" 
13400  794 
by (rule LC.fold_insert [OF LC.intro, symmetric]) (insert b insert, 
13421  795 
auto simp add: left_commute) 
12396  796 
finally show ?case . 
797 
qed 

798 
qed 

799 

800 

801 
subsection {* Generalized summation over a set *} 

802 

803 
constdefs 

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

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

806 

807 
syntax 

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

809 
syntax (xsymbols) 

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

811 
translations 

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

813 

814 

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

816 
by (simp add: setsum_def) 

817 

818 
lemma setsum_insert [simp]: 

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

13365  820 
by (simp add: setsum_def 
13421  821 
LC.fold_insert [OF LC.intro] plus_ac0_left_commute) 
12396  822 

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

824 
apply (case_tac "finite A") 

825 
prefer 2 apply (simp add: setsum_def) 

826 
apply (erule finite_induct) 

827 
apply auto 

828 
done 

829 

830 
lemma setsum_eq_0_iff [simp]: 

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

832 
by (induct set: Finites) auto 

833 

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

835 
apply (case_tac "finite A") 

836 
prefer 2 apply (simp add: setsum_def) 

837 
apply (erule rev_mp) 

838 
apply (erule finite_induct) 

839 
apply auto 

840 
done 

841 

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

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

844 
by (induct set: Finites) auto 

845 

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

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

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

849 
apply (induct set: Finites) 

850 
apply simp 

851 
apply (simp add: plus_ac0 Int_insert_left insert_absorb) 

852 
done 

853 

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

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

856 
apply (subst setsum_Un_Int [symmetric]) 

857 
apply auto 

858 
done 

859 

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

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

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

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

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

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

865 
setsum f (UNION I A) = setsum (\<lambda>i. setsum f (A i)) I" 
12396  866 
apply (induct set: Finites) 
867 
apply simp 

868 
apply atomize 

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

870 
prefer 2 apply blast 

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

872 
prefer 2 apply blast 

873 
apply (simp add: setsum_Un_disjoint) 

874 
done 

875 

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

877 
apply (case_tac "finite A") 

878 
prefer 2 apply (simp add: setsum_def) 

879 
apply (erule finite_induct) 

880 
apply auto 

881 
apply (simp add: plus_ac0) 

882 
done 

883 

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

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

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

887 
apply (subst setsum_Un_Int [symmetric]) 

888 
apply auto 

889 
done 

890 

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

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

893 
apply (case_tac "finite A") 

894 
prefer 2 apply (simp add: setsum_def) 

895 
apply (erule finite_induct) 

896 
apply (auto simp add: insert_Diff_if) 

897 
apply (drule_tac a = a in mk_disjoint_insert) 

898 
apply auto 

899 
done 

900 

901 
lemma setsum_cong: 

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

903 
apply (case_tac "finite B") 

904 
prefer 2 apply (simp add: setsum_def) 

905 
apply simp 

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

907 
apply simp 

908 
apply (erule finite_induct) 

909 
apply simp 

910 
apply (simp add: subset_insert_iff) 

911 
apply clarify 

912 
apply (subgoal_tac "finite C") 

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

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

915 
prefer 2 apply blast 

916 
apply (erule ssubst) 

917 
apply (drule spec) 

918 
apply (erule (1) notE impE) 

919 
apply (simp add: Ball_def) 

920 
done 

921 

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

922 
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

923 

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

924 
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

925 

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

926 
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

927 
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

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

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

930 
case empty thus ?case by simp 
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 
case (insert S x) 
44bdc150211b
Added Mi and Max on sets, hid Min and Pls on numerals.
nipkow
parents:
13421
diff
changeset

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

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

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

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

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

938 
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

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

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

941 
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

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

943 
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

944 
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

945 
qed 
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 

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

949 
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

950 
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

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

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

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

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

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

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

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

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

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

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

961 
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

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

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

964 
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

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

966 
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

967 
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

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

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

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

971 

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

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

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

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

975 

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

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

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

978 

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

979 
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

980 
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

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

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

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

984 
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

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

986 
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

987 
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

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

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

990 

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

991 
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

992 
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

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

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

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

996 
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

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

998 
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

999 
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

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

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

1002 

12396  1003 

1004 
text {* 

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

1006 
Kammüller, tidied by LCP. 

1007 
*} 

1008 

1009 
lemma card_s_0_eq_empty: 

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

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

1012 
apply (simp cong add: rev_conj_cong) 

1013 
done 

1014 

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

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

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

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

1019 
apply safe 

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

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

1022 
apply (subgoal_tac "x ~: xa") 

1023 
apply auto 

1024 
apply (erule rev_mp, subst card_Diff_singleton) 

1025 
apply (auto intro: finite_subset) 

1026 
done 

1027 

1028 
lemma card_inj_on_le: 

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

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

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

12396  1035 
by (auto intro: le_anti_sym card_inj_on_le) 
1036 

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

1039 
@{term x} into each.*} 

1040 
lemma constr_bij: 

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

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

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

13595  1045 
apply (auto elim!: equalityE simp add: inj_on_def) 
1046 
apply (subst Diff_insert0, auto) 

1047 
txt {* finiteness of the two sets *} 

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

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

1050 
apply fast+ 

12396  1051 
done 
1052 

1053 
text {* 

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

1055 
*} 

1056 

1057 
lemma n_sub_lemma: 

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

1059 
apply (induct k) 

1060 
apply (simp add: card_s_0_eq_empty) 

1061 
apply atomize 

1062 
apply (rotate_tac 1, erule finite_induct) 

13421  1063 
apply (simp_all (no_asm_simp) cong add: conj_cong 
1064 
add: card_s_0_eq_empty choose_deconstruct) 

12396  1065 
apply (subst card_Un_disjoint) 
1066 
prefer 4 apply (force simp add: constr_bij) 

1067 
prefer 3 apply force 

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

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

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

1071 
done 

1072 

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

12396  1075 
by (simp add: n_sub_lemma) 
1076 

1077 
end 