src/HOL/Finite.ML
changeset 5416 9f029e382b5d
parent 5413 9d11f2d39b13
child 5476 1c09934fe445
equal deleted 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 *)
     8 
       
     9 open Finite;
       
    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";
   379 Addsimps [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;