1331 done |
1330 done |
1332 |
1331 |
1333 lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B" |
1332 lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B" |
1334 by (erule psubsetI, blast) |
1333 by (erule psubsetI, blast) |
1335 |
1334 |
|
1335 lemma card_le_inj: |
|
1336 assumes fA: "finite A" |
|
1337 and fB: "finite B" |
|
1338 and c: "card A \<le> card B" |
|
1339 shows "\<exists>f. f ` A \<subseteq> B \<and> inj_on f A" |
|
1340 using fA fB c |
|
1341 proof (induct arbitrary: B rule: finite_induct) |
|
1342 case empty |
|
1343 then show ?case by simp |
|
1344 next |
|
1345 case (insert x s t) |
|
1346 then show ?case |
|
1347 proof (induct rule: finite_induct[OF "insert.prems"(1)]) |
|
1348 case 1 |
|
1349 then show ?case by simp |
|
1350 next |
|
1351 case (2 y t) |
|
1352 from "2.prems"(1,2,5) "2.hyps"(1,2) have cst: "card s \<le> card t" |
|
1353 by simp |
|
1354 from "2.prems"(3) [OF "2.hyps"(1) cst] |
|
1355 obtain f where "f ` s \<subseteq> t" "inj_on f s" |
|
1356 by blast |
|
1357 with "2.prems"(2) "2.hyps"(2) show ?case |
|
1358 apply - |
|
1359 apply (rule exI[where x = "\<lambda>z. if z = x then y else f z"]) |
|
1360 apply (auto simp add: inj_on_def) |
|
1361 done |
|
1362 qed |
|
1363 qed |
|
1364 |
|
1365 lemma card_subset_eq: |
|
1366 assumes fB: "finite B" |
|
1367 and AB: "A \<subseteq> B" |
|
1368 and c: "card A = card B" |
|
1369 shows "A = B" |
|
1370 proof - |
|
1371 from fB AB have fA: "finite A" |
|
1372 by (auto intro: finite_subset) |
|
1373 from fA fB have fBA: "finite (B - A)" |
|
1374 by auto |
|
1375 have e: "A \<inter> (B - A) = {}" |
|
1376 by blast |
|
1377 have eq: "A \<union> (B - A) = B" |
|
1378 using AB by blast |
|
1379 from card_Un_disjoint[OF fA fBA e, unfolded eq c] have "card (B - A) = 0" |
|
1380 by arith |
|
1381 then have "B - A = {}" |
|
1382 unfolding card_eq_0_iff using fA fB by simp |
|
1383 with AB show "A = B" |
|
1384 by blast |
|
1385 qed |
|
1386 |
1336 lemma insert_partition: |
1387 lemma insert_partition: |
1337 "\<lbrakk> x \<notin> F; \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<rbrakk> |
1388 "\<lbrakk> x \<notin> F; \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<rbrakk> |
1338 \<Longrightarrow> x \<inter> \<Union> F = {}" |
1389 \<Longrightarrow> x \<inter> \<Union> F = {}" |
1339 by auto |
1390 by auto |
1340 |
1391 |
1355 then have "finite B" using fin finite_subset by blast |
1406 then have "finite B" using fin finite_subset by blast |
1356 ultimately |
1407 ultimately |
1357 have "P B" using ih by simp |
1408 have "P B" using ih by simp |
1358 } |
1409 } |
1359 with fin show "P A" using major by blast |
1410 with fin show "P A" using major by blast |
|
1411 qed |
|
1412 |
|
1413 lemma finite_induct_select[consumes 1, case_names empty select]: |
|
1414 assumes "finite S" |
|
1415 assumes "P {}" |
|
1416 assumes select: "\<And>T. T \<subset> S \<Longrightarrow> P T \<Longrightarrow> \<exists>s\<in>S - T. P (insert s T)" |
|
1417 shows "P S" |
|
1418 proof - |
|
1419 have "0 \<le> card S" by simp |
|
1420 then have "\<exists>T \<subseteq> S. card T = card S \<and> P T" |
|
1421 proof (induct rule: dec_induct) |
|
1422 case base with `P {}` show ?case |
|
1423 by (intro exI[of _ "{}"]) auto |
|
1424 next |
|
1425 case (step n) |
|
1426 then obtain T where T: "T \<subseteq> S" "card T = n" "P T" |
|
1427 by auto |
|
1428 with `n < card S` have "T \<subset> S" "P T" |
|
1429 by auto |
|
1430 with select[of T] obtain s where "s \<in> S" "s \<notin> T" "P (insert s T)" |
|
1431 by auto |
|
1432 with step(2) T `finite S` show ?case |
|
1433 by (intro exI[of _ "insert s T"]) (auto dest: finite_subset) |
|
1434 qed |
|
1435 with `finite S` show "P S" |
|
1436 by (auto dest: card_subset_eq) |
1360 qed |
1437 qed |
1361 |
1438 |
1362 text{* main cardinality theorem *} |
1439 text{* main cardinality theorem *} |
1363 lemma card_partition [rule_format]: |
1440 lemma card_partition [rule_format]: |
1364 "finite C ==> |
1441 "finite C ==> |