# HG changeset patch
# User paulson
# Date 904655068 -7200
# Node ID 9f029e382b5da6518a1188e54614ff1aee691a51
# Parent  13a199e94877d2083c1c3b98078e05f7a31f5093
New law card_Un_Int.  Removed card_insert from simpset

diff -r 13a199e94877 -r 9f029e382b5d src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Tue Sep 01 15:03:43 1998 +0200
+++ b/src/HOL/Finite.ML	Tue Sep 01 15:04:28 1998 +0200
@@ -6,8 +6,6 @@
 Finite sets and their cardinality
 *)
 
-open Finite;
-
 section "finite";
 
 (*Discharging ~ x:y entails extra work*)
@@ -310,8 +308,7 @@
 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";
@@ -333,11 +330,18 @@
 	      (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";
+
+Goal "[| finite A; finite B |] \
+\     ==> card A + card B = card (A Un B) + card (A Int B)";
 by (etac finite_induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [Int_insert_left])));
-qed_spec_mp "card_Un_disjoint";
+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);
@@ -349,7 +353,7 @@
 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";
@@ -376,7 +380,6 @@
 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);