src/HOL/Finite.ML
 changeset 5416 9f029e382b5d parent 5413 9d11f2d39b13 child 5476 1c09934fe445
equal inserted replaced
5415:13a199e94877 5416:9f029e382b5d
`     3     Author:     Lawrence C Paulson & Tobias Nipkow`
`     3     Author:     Lawrence C Paulson & Tobias Nipkow`
`     4     Copyright   1995  University of Cambridge & TU Muenchen`
`     4     Copyright   1995  University of Cambridge & TU Muenchen`
`     5 `
`     5 `
`     6 Finite sets and their cardinality`
`     6 Finite sets and their cardinality`
`     7 *)`
`     7 *)`
`    10 `
`     8 `
`    11 section "finite";`
`     9 section "finite";`
`    12 `
`    10 `
`    13 (*Discharging ~ x:y entails extra work*)`
`    11 (*Discharging ~ x:y entails extra work*)`
`    14 val major::prems = Goal `
`    12 val major::prems = Goal `
`   308 by (etac less_asym 1 THEN atac 1);`
`   306 by (etac less_asym 1 THEN atac 1);`
`   309 by (hyp_subst_tac 1);`
`   307 by (hyp_subst_tac 1);`
`   310 by (Asm_full_simp_tac 1);`
`   308 by (Asm_full_simp_tac 1);`
`   311 val lemma = result();`
`   309 val lemma = result();`
`   312 `
`   310 `
`   313 Goalw [card_def]`
`   311 Goalw [card_def] "[| finite A; x ~: A |] ==> card(insert x A) = Suc(card A)";`
`   314   "[| finite A; x ~: A |] ==> card(insert x A) = Suc(card A)";`
`       `
`   315 by (etac lemma 1);`
`   312 by (etac lemma 1);`
`   316 by (assume_tac 1);`
`   313 by (assume_tac 1);`
`   317 qed "card_insert_disjoint";`
`   314 qed "card_insert_disjoint";`
`   318 Addsimps [card_insert_disjoint];`
`   315 Addsimps [card_insert_disjoint];`
`   319 `
`   316 `
`   331 by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff]) 2);`
`   328 by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff]) 2);`
`   332 by (fast_tac (claset() addss`
`   329 by (fast_tac (claset() addss`
`   333 	      (simpset() addsimps [subset_insert_iff, finite_subset])) 1);`
`   330 	      (simpset() addsimps [subset_insert_iff, finite_subset])) 1);`
`   334 qed_spec_mp "card_mono";`
`   331 qed_spec_mp "card_mono";`
`   335 `
`   332 `
`   336 Goal "[| finite A; finite B |]\`
`   333 `
`   337 \                       ==> A Int B = {} --> card(A Un B) = card A + card B";`
`   334 Goal "[| finite A; finite B |] \`
`   338 by (etac finite_induct 1);`
`   335 \     ==> card A + card B = card (A Un B) + card (A Int B)";`
`   339 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Int_insert_left])));`
`   336 by (etac finite_induct 1);`
`   340 qed_spec_mp "card_Un_disjoint";`
`   337 by (Simp_tac 1);`
`       `
`   338 by (asm_simp_tac (simpset() addsimps [insert_absorb, Int_insert_left]) 1);`
`       `
`   339 qed "card_Un_Int";`
`       `
`   340 `
`       `
`   341 Goal "[| finite A; finite B; A Int B = {} |] \`
`       `
`   342 \     ==> card (A Un B) = card A + card B";`
`       `
`   343 by (asm_simp_tac (simpset() addsimps [card_Un_Int]) 1);`
`       `
`   344 qed "card_Un_disjoint";`
`   341 `
`   345 `
`   342 Goal "[| finite A; B<=A |] ==> card A - card B = card (A - B)";`
`   346 Goal "[| finite A; B<=A |] ==> card A - card B = card (A - B)";`
`   343 by (subgoal_tac "(A-B) Un B = A" 1);`
`   347 by (subgoal_tac "(A-B) Un B = A" 1);`
`   344 by (Blast_tac 2);`
`   348 by (Blast_tac 2);`
`   345 by (rtac (add_right_cancel RS iffD1) 1);`
`   349 by (rtac (add_right_cancel RS iffD1) 1);`
`   347 by (etac ssubst 4);`
`   351 by (etac ssubst 4);`
`   348 by (Blast_tac 3);`
`   352 by (Blast_tac 3);`
`   349 by (ALLGOALS `
`   353 by (ALLGOALS `
`   350     (asm_simp_tac`
`   354     (asm_simp_tac`
`   351      (simpset() addsimps [add_commute, not_less_iff_le, `
`   355      (simpset() addsimps [add_commute, not_less_iff_le, `
`   352 			 add_diff_inverse, card_mono, finite_subset])));`
`   356 			  add_diff_inverse, card_mono, finite_subset])));`
`   353 qed "card_Diff_subset";`
`   357 qed "card_Diff_subset";`
`   354 `
`   358 `
`   355 Goal "[| finite A; x: A |] ==> Suc(card(A-{x})) = card A";`
`   359 Goal "[| finite A; x: A |] ==> Suc(card(A-{x})) = card A";`
`   356 by (res_inst_tac [("t", "A")] (insert_Diff RS subst) 1);`
`   360 by (res_inst_tac [("t", "A")] (insert_Diff RS subst) 1);`
`   357 by (assume_tac 1);`
`   361 by (assume_tac 1);`
`   374 Goal "finite A ==> card(insert x A) = Suc(card(A-{x}))";`
`   378 Goal "finite A ==> card(insert x A) = Suc(card(A-{x}))";`
`   375 by (case_tac "x:A" 1);`
`   379 by (case_tac "x:A" 1);`
`   376 by (ALLGOALS `
`   380 by (ALLGOALS `
`   377     (asm_simp_tac (simpset() addsimps [card_Suc_Diff, insert_absorb])));`
`   381     (asm_simp_tac (simpset() addsimps [card_Suc_Diff, insert_absorb])));`
`   378 qed "card_insert";`
`   382 qed "card_insert";`
`   380 `
`   383 `
`   381 Goal "finite(A) ==> inj_on f A --> card (f `` A) = card A";`
`   384 Goal "finite(A) ==> inj_on f A --> card (f `` A) = card A";`
`   382 by (etac finite_induct 1);`
`   385 by (etac finite_induct 1);`
`   383 by (ALLGOALS Asm_simp_tac);`
`   386 by (ALLGOALS Asm_simp_tac);`
`   384 by Safe_tac;`
`   387 by Safe_tac;`