src/HOL/Finite.ML

     Author:     Lawrence C Paulson & Tobias Nipkow
     Copyright   1995  University of Cambridge & TU Muenchen
 
 Finite sets and their cardinality
 *)
-
-open Finite;
 
 section "finite";
 
 (*Discharging ~ x:y entails extra work*)
 val major::prems = Goal 

 by (etac less_asym 1 THEN atac 1);
 by (hyp_subst_tac 1);
 by (Asm_full_simp_tac 1);
 val lemma = result();
 
-Goalw [card_def]
-  "[| finite A; x ~: A |] ==> card(insert x A) = Suc(card A)";
+Goalw [card_def] "[| finite A; x ~: A |] ==> card(insert x A) = Suc(card A)";
 by (etac lemma 1);
 by (assume_tac 1);
 qed "card_insert_disjoint";
 Addsimps [card_insert_disjoint];
 

 by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff]) 2);
 by (fast_tac (claset() addss
 	      (simpset() addsimps [subset_insert_iff, finite_subset])) 1);
 qed_spec_mp "card_mono";
 
-Goal "[| finite A; finite B |]\
-\                       ==> A Int B = {} --> card(A Un B) = card A + card B";
-by (etac finite_induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [Int_insert_left])));
-qed_spec_mp "card_Un_disjoint";
+
+Goal "[| finite A; finite B |] \
+\     ==> card A + card B = card (A Un B) + card (A Int B)";
+by (etac finite_induct 1);
+by (Simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [insert_absorb, Int_insert_left]) 1);
+qed "card_Un_Int";
+
+Goal "[| finite A; finite B; A Int B = {} |] \
+\     ==> card (A Un B) = card A + card B";
+by (asm_simp_tac (simpset() addsimps [card_Un_Int]) 1);
+qed "card_Un_disjoint";
 
 Goal "[| finite A; B<=A |] ==> card A - card B = card (A - B)";
 by (subgoal_tac "(A-B) Un B = A" 1);
 by (Blast_tac 2);
 by (rtac (add_right_cancel RS iffD1) 1);

 by (etac ssubst 4);
 by (Blast_tac 3);
 by (ALLGOALS 
     (asm_simp_tac
      (simpset() addsimps [add_commute, not_less_iff_le, 
-			 add_diff_inverse, card_mono, finite_subset])));
+			  add_diff_inverse, card_mono, finite_subset])));
 qed "card_Diff_subset";
 
 Goal "[| finite A; x: A |] ==> Suc(card(A-{x})) = card A";
 by (res_inst_tac [("t", "A")] (insert_Diff RS subst) 1);
 by (assume_tac 1);

 Goal "finite A ==> card(insert x A) = Suc(card(A-{x}))";
 by (case_tac "x:A" 1);
 by (ALLGOALS 
     (asm_simp_tac (simpset() addsimps [card_Suc_Diff, insert_absorb])));
 qed "card_insert";
-Addsimps [card_insert];
 
 Goal "finite(A) ==> inj_on f A --> card (f `` A) = card A";
 by (etac finite_induct 1);
 by (ALLGOALS Asm_simp_tac);
 by Safe_tac;