40 by (rtac (major RS finite_induct) 1); |
40 by (rtac (major RS finite_induct) 1); |
41 by (ALLGOALS (asm_simp_tac (simpset() addsimps prems))); |
41 by (ALLGOALS (asm_simp_tac (simpset() addsimps prems))); |
42 qed "finite_UnI"; |
42 qed "finite_UnI"; |
43 |
43 |
44 (*Every subset of a finite set is finite*) |
44 (*Every subset of a finite set is finite*) |
45 Goal "!!B. finite B ==> ALL A. A<=B --> finite A"; |
45 Goal "finite B ==> ALL A. A<=B --> finite A"; |
46 by (etac finite_induct 1); |
46 by (etac finite_induct 1); |
47 by (Simp_tac 1); |
47 by (Simp_tac 1); |
48 by (safe_tac (claset() addSDs [subset_insert_iff RS iffD1])); |
48 by (safe_tac (claset() addSDs [subset_insert_iff RS iffD1])); |
49 by (eres_inst_tac [("t","A")] (insert_Diff RS subst) 2); |
49 by (eres_inst_tac [("t","A")] (insert_Diff RS subst) 2); |
50 by (ALLGOALS Asm_simp_tac); |
50 by (ALLGOALS Asm_simp_tac); |
51 val lemma = result(); |
51 val lemma = result(); |
52 |
52 |
53 Goal "!!A. [| A<=B; finite B |] ==> finite A"; |
53 Goal "[| A<=B; finite B |] ==> finite A"; |
54 by (dtac lemma 1); |
54 by (dtac lemma 1); |
55 by (Blast_tac 1); |
55 by (Blast_tac 1); |
56 qed "finite_subset"; |
56 qed "finite_subset"; |
57 |
57 |
58 Goal "finite(F Un G) = (finite F & finite G)"; |
58 Goal "finite(F Un G) = (finite F & finite G)"; |
109 by (ALLGOALS Asm_simp_tac); |
109 by (ALLGOALS Asm_simp_tac); |
110 qed "finite_Diff_singleton"; |
110 qed "finite_Diff_singleton"; |
111 AddIffs [finite_Diff_singleton]; |
111 AddIffs [finite_Diff_singleton]; |
112 |
112 |
113 (*Lemma for proving finite_imageD*) |
113 (*Lemma for proving finite_imageD*) |
114 Goal "!!A. finite B ==> !A. f``A = B --> inj_on f A --> finite A"; |
114 Goal "finite B ==> !A. f``A = B --> inj_on f A --> finite A"; |
115 by (etac finite_induct 1); |
115 by (etac finite_induct 1); |
116 by (ALLGOALS Asm_simp_tac); |
116 by (ALLGOALS Asm_simp_tac); |
117 by (Clarify_tac 1); |
117 by (Clarify_tac 1); |
118 by (subgoal_tac "EX y:A. f y = x & F = f``(A-{y})" 1); |
118 by (subgoal_tac "EX y:A. f y = x & F = f``(A-{y})" 1); |
119 by (Clarify_tac 1); |
119 by (Clarify_tac 1); |
125 by (res_inst_tac [("x","xa")] bexI 1); |
125 by (res_inst_tac [("x","xa")] bexI 1); |
126 by (ALLGOALS |
126 by (ALLGOALS |
127 (asm_full_simp_tac (simpset() addsimps [inj_on_image_set_diff]))); |
127 (asm_full_simp_tac (simpset() addsimps [inj_on_image_set_diff]))); |
128 val lemma = result(); |
128 val lemma = result(); |
129 |
129 |
130 Goal "!!A. [| finite(f``A); inj_on f A |] ==> finite A"; |
130 Goal "[| finite(f``A); inj_on f A |] ==> finite A"; |
131 by (dtac lemma 1); |
131 by (dtac lemma 1); |
132 by (Blast_tac 1); |
132 by (Blast_tac 1); |
133 qed "finite_imageD"; |
133 qed "finite_imageD"; |
134 |
134 |
135 (** The finite UNION of finite sets **) |
135 (** The finite UNION of finite sets **) |
149 bind_thm("finite_SigmaI", ballI RSN (2,result())); |
149 bind_thm("finite_SigmaI", ballI RSN (2,result())); |
150 Addsimps [finite_SigmaI]; |
150 Addsimps [finite_SigmaI]; |
151 |
151 |
152 (** The powerset of a finite set **) |
152 (** The powerset of a finite set **) |
153 |
153 |
154 Goal "!!A. finite(Pow A) ==> finite A"; |
154 Goal "finite(Pow A) ==> finite A"; |
155 by (subgoal_tac "finite ((%x.{x})``A)" 1); |
155 by (subgoal_tac "finite ((%x.{x})``A)" 1); |
156 by (rtac finite_subset 2); |
156 by (rtac finite_subset 2); |
157 by (assume_tac 3); |
157 by (assume_tac 3); |
158 by (ALLGOALS |
158 by (ALLGOALS |
159 (fast_tac (claset() addSDs [rewrite_rule [inj_on_def] finite_imageD]))); |
159 (fast_tac (claset() addSDs [rewrite_rule [inj_on_def] finite_imageD]))); |
271 by (Asm_simp_tac 1); |
271 by (Asm_simp_tac 1); |
272 by (Simp_tac 1); |
272 by (Simp_tac 1); |
273 by (Blast_tac 1); |
273 by (Blast_tac 1); |
274 val lemma = result(); |
274 val lemma = result(); |
275 |
275 |
276 Goal "!!A. [| finite A; x ~: A |] ==> \ |
276 Goal "[| finite A; x ~: A |] ==> \ |
277 \ (LEAST n. ? f. insert x A = {f i|i. i<n}) = Suc(LEAST n. ? f. A={f i|i. i<n})"; |
277 \ (LEAST n. ? f. insert x A = {f i|i. i<n}) = Suc(LEAST n. ? f. A={f i|i. i<n})"; |
278 by (rtac Least_equality 1); |
278 by (rtac Least_equality 1); |
279 by (dtac finite_has_card 1); |
279 by (dtac finite_has_card 1); |
280 by (etac exE 1); |
280 by (etac exE 1); |
281 by (dres_inst_tac [("P","%n.? f. A={f i|i. i<n}")] LeastI 1); |
281 by (dres_inst_tac [("P","%n.? f. A={f i|i. i<n}")] LeastI 1); |
307 by (etac lemma 1); |
307 by (etac lemma 1); |
308 by (assume_tac 1); |
308 by (assume_tac 1); |
309 qed "card_insert_disjoint"; |
309 qed "card_insert_disjoint"; |
310 Addsimps [card_insert_disjoint]; |
310 Addsimps [card_insert_disjoint]; |
311 |
311 |
312 Goal "!!A. finite A ==> card A <= card (insert x A)"; |
312 Goal "finite A ==> card A <= card (insert x A)"; |
313 by (case_tac "x: A" 1); |
313 by (case_tac "x: A" 1); |
314 by (ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb]))); |
314 by (ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb]))); |
315 qed "card_insert_le"; |
315 qed "card_insert_le"; |
316 |
316 |
317 Goal "!!A. finite A ==> !B. B <= A --> card(B) <= card(A)"; |
317 Goal "finite A ==> !B. B <= A --> card(B) <= card(A)"; |
318 by (etac finite_induct 1); |
318 by (etac finite_induct 1); |
319 by (Simp_tac 1); |
319 by (Simp_tac 1); |
320 by (Clarify_tac 1); |
320 by (Clarify_tac 1); |
321 by (case_tac "x:B" 1); |
321 by (case_tac "x:B" 1); |
322 by (dres_inst_tac [("A","B")] mk_disjoint_insert 1); |
322 by (dres_inst_tac [("A","B")] mk_disjoint_insert 1); |
323 by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff]) 2); |
323 by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff]) 2); |
324 by (fast_tac (claset() addss |
324 by (fast_tac (claset() addss |
325 (simpset() addsimps [subset_insert_iff, finite_subset])) 1); |
325 (simpset() addsimps [subset_insert_iff, finite_subset])) 1); |
326 qed_spec_mp "card_mono"; |
326 qed_spec_mp "card_mono"; |
327 |
327 |
328 Goal "!!A B. [| finite A; finite B |]\ |
328 Goal "[| finite A; finite B |]\ |
329 \ ==> A Int B = {} --> card(A Un B) = card A + card B"; |
329 \ ==> A Int B = {} --> card(A Un B) = card A + card B"; |
330 by (etac finite_induct 1); |
330 by (etac finite_induct 1); |
331 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Int_insert_left]))); |
331 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Int_insert_left]))); |
332 qed_spec_mp "card_Un_disjoint"; |
332 qed_spec_mp "card_Un_disjoint"; |
333 |
333 |
334 Goal "!!A. [| finite A; B<=A |] ==> card A - card B = card (A - B)"; |
334 Goal "[| finite A; B<=A |] ==> card A - card B = card (A - B)"; |
335 by (subgoal_tac "(A-B) Un B = A" 1); |
335 by (subgoal_tac "(A-B) Un B = A" 1); |
336 by (Blast_tac 2); |
336 by (Blast_tac 2); |
337 by (rtac (add_right_cancel RS iffD1) 1); |
337 by (rtac (add_right_cancel RS iffD1) 1); |
338 by (rtac (card_Un_disjoint RS subst) 1); |
338 by (rtac (card_Un_disjoint RS subst) 1); |
339 by (etac ssubst 4); |
339 by (etac ssubst 4); |
342 (asm_simp_tac |
342 (asm_simp_tac |
343 (simpset() addsimps [add_commute, not_less_iff_le, |
343 (simpset() addsimps [add_commute, not_less_iff_le, |
344 add_diff_inverse, card_mono, finite_subset]))); |
344 add_diff_inverse, card_mono, finite_subset]))); |
345 qed "card_Diff_subset"; |
345 qed "card_Diff_subset"; |
346 |
346 |
347 Goal "!!A. [| finite A; x: A |] ==> Suc(card(A-{x})) = card A"; |
347 Goal "[| finite A; x: A |] ==> Suc(card(A-{x})) = card A"; |
348 by (res_inst_tac [("t", "A")] (insert_Diff RS subst) 1); |
348 by (res_inst_tac [("t", "A")] (insert_Diff RS subst) 1); |
349 by (assume_tac 1); |
349 by (assume_tac 1); |
350 by (Asm_simp_tac 1); |
350 by (Asm_simp_tac 1); |
351 qed "card_Suc_Diff"; |
351 qed "card_Suc_Diff"; |
352 |
352 |
353 Goal "!!A. [| finite A; x: A |] ==> card(A-{x}) < card A"; |
353 Goal "[| finite A; x: A |] ==> card(A-{x}) < card A"; |
354 by (rtac Suc_less_SucD 1); |
354 by (rtac Suc_less_SucD 1); |
355 by (asm_simp_tac (simpset() addsimps [card_Suc_Diff]) 1); |
355 by (asm_simp_tac (simpset() addsimps [card_Suc_Diff]) 1); |
356 qed "card_Diff"; |
356 qed "card_Diff"; |
357 |
357 |
358 Goal "!!A. finite A ==> card(A-{x}) <= card A"; |
358 Goal "finite A ==> card(A-{x}) <= card A"; |
359 by (case_tac "x: A" 1); |
359 by (case_tac "x: A" 1); |
360 by (ALLGOALS (asm_simp_tac (simpset() addsimps [card_Diff, less_imp_le]))); |
360 by (ALLGOALS (asm_simp_tac (simpset() addsimps [card_Diff, less_imp_le]))); |
361 qed "card_Diff_le"; |
361 qed "card_Diff_le"; |
362 |
362 |
363 |
363 |
364 (*** Cardinality of the Powerset ***) |
364 (*** Cardinality of the Powerset ***) |
365 |
365 |
366 Goal "!!A. finite A ==> card(insert x A) = Suc(card(A-{x}))"; |
366 Goal "finite A ==> card(insert x A) = Suc(card(A-{x}))"; |
367 by (case_tac "x:A" 1); |
367 by (case_tac "x:A" 1); |
368 by (ALLGOALS |
368 by (ALLGOALS |
369 (asm_simp_tac (simpset() addsimps [card_Suc_Diff, insert_absorb]))); |
369 (asm_simp_tac (simpset() addsimps [card_Suc_Diff, insert_absorb]))); |
370 qed "card_insert"; |
370 qed "card_insert"; |
371 Addsimps [card_insert]; |
371 Addsimps [card_insert]; |
372 |
372 |
373 Goal "!!A. finite(A) ==> inj_on f A --> card (f `` A) = card A"; |
373 Goal "finite(A) ==> inj_on f A --> card (f `` A) = card A"; |
374 by (etac finite_induct 1); |
374 by (etac finite_induct 1); |
375 by (ALLGOALS Asm_simp_tac); |
375 by (ALLGOALS Asm_simp_tac); |
376 by Safe_tac; |
376 by Safe_tac; |
377 by (rewtac inj_on_def); |
377 by (rewtac inj_on_def); |
378 by (Blast_tac 1); |
378 by (Blast_tac 1); |
380 by (etac finite_imageI 1); |
380 by (etac finite_imageI 1); |
381 by (Blast_tac 1); |
381 by (Blast_tac 1); |
382 by (Blast_tac 1); |
382 by (Blast_tac 1); |
383 qed_spec_mp "card_image"; |
383 qed_spec_mp "card_image"; |
384 |
384 |
385 Goal "!!A. finite A ==> card (Pow A) = 2 ^ card A"; |
385 Goal "finite A ==> card (Pow A) = 2 ^ card A"; |
386 by (etac finite_induct 1); |
386 by (etac finite_induct 1); |
387 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Pow_insert]))); |
387 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Pow_insert]))); |
388 by (stac card_Un_disjoint 1); |
388 by (stac card_Un_disjoint 1); |
389 by (EVERY (map (blast_tac (claset() addIs [finite_imageI])) [3,2,1])); |
389 by (EVERY (map (blast_tac (claset() addIs [finite_imageI])) [3,2,1])); |
390 by (subgoal_tac "inj_on (insert x) (Pow F)" 1); |
390 by (subgoal_tac "inj_on (insert x) (Pow F)" 1); |
416 qed_spec_mp "psubset_card" ; |
416 qed_spec_mp "psubset_card" ; |
417 |
417 |
418 |
418 |
419 (*Relates to equivalence classes. Based on a theorem of F. Kammueller's. |
419 (*Relates to equivalence classes. Based on a theorem of F. Kammueller's. |
420 The "finite C" premise is redundant*) |
420 The "finite C" premise is redundant*) |
421 Goal "!!C. finite C ==> finite (Union C) --> \ |
421 Goal "finite C ==> finite (Union C) --> \ |
422 \ (! c : C. k dvd card c) --> \ |
422 \ (! c : C. k dvd card c) --> \ |
423 \ (! c1: C. ! c2: C. c1 ~= c2 --> c1 Int c2 = {}) \ |
423 \ (! c1: C. ! c2: C. c1 ~= c2 --> c1 Int c2 = {}) \ |
424 \ --> k dvd card(Union C)"; |
424 \ --> k dvd card(Union C)"; |
425 by (etac finite_induct 1); |
425 by (etac finite_induct 1); |
426 by (ALLGOALS Asm_simp_tac); |
426 by (ALLGOALS Asm_simp_tac); |