1.1 --- a/src/HOL/Finite.ML	Fri Jun 16 13:13:55 2000 +0200
     1.2 +++ b/src/HOL/Finite.ML	Fri Jun 16 13:15:04 2000 +0200
     1.3 @@ -41,7 +41,7 @@
     1.4  (*Every subset of a finite set is finite*)
     1.5  Goal "finite B ==> ALL A. A<=B --> finite A";
     1.6  by (etac finite_induct 1);
     1.7 -by (Simp_tac 1);
     1.8 + by (simp_tac (simpset() addsimps [subset_empty]) 1);
     1.9  by (safe_tac (claset() addSDs [subset_insert_iff RS iffD1]));
    1.10  by (eres_inst_tac [("t","A")] (insert_Diff RS subst) 2);
    1.11  by (ALLGOALS Asm_simp_tac);
    1.12 @@ -343,6 +343,10 @@
    1.13  by (asm_simp_tac (simpset() addsimps [card_Suc_Diff1 RS sym]) 1);
    1.14  qed "card_Diff_singleton";
    1.15  
    1.16 +Goal "finite A ==> card (A-{x}) = (if x:A then card A - 1 else card A)";
    1.17 +by (asm_simp_tac (simpset() addsimps [card_Diff_singleton]) 1);
    1.18 +qed "card_Diff_singleton_if";
    1.19 +
    1.20  Goal "finite A ==> card(insert x A) = Suc(card(A-{x}))";
    1.21  by (asm_simp_tac (simpset() addsimps [card_insert_if,card_Suc_Diff1]) 1);
    1.22  qed "card_insert";
    1.23 @@ -351,18 +355,30 @@
    1.24  by (asm_simp_tac (simpset() addsimps [card_insert_if]) 1);
    1.25  qed "card_insert_le";
    1.26  
    1.27 -Goal  "finite A ==> !B. B <= A --> card(B) <= card(A)";
    1.28 +Goal "finite B ==> ALL A. A <= B --> card B <= card A --> A = B";
    1.29  by (etac finite_induct 1);
    1.30 -by (Simp_tac 1);
    1.31 + by (simp_tac (simpset() addsimps [subset_empty]) 1);
    1.32  by (Clarify_tac 1);
    1.33 -by (case_tac "x:B" 1);
    1.34 - by (dres_inst_tac [("A","B")] mk_disjoint_insert 1);
    1.35 - by (asm_full_simp_tac (simpset() addsimps [le_SucI, subset_insert_iff]) 2);
    1.36 -by (force_tac (claset(),
    1.37 -	       simpset() addsimps [subset_insert_iff, finite_subset]
    1.38 -			 delsimps [insert_subset]) 1);
    1.39 -qed_spec_mp "card_mono";
    1.40 +by (subgoal_tac "finite A & A-{x} <= F" 1);
    1.41 + by (blast_tac (claset() addIs [finite_subset]) 2); 
    1.42 +by (dres_inst_tac [("x","A-{x}")] spec 1); 
    1.43 +by (asm_full_simp_tac (simpset() addsimps [card_Diff_singleton_if]
    1.44 +                                 addsplits [split_if_asm]) 1); 
    1.45 +by (case_tac "card A" 1);
    1.46 +by Auto_tac; 
    1.47 +qed_spec_mp "card_seteq";
    1.48  
    1.49 +Goalw [psubset_def] "[| finite B;  A < B |] ==> card A < card B";
    1.50 +by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
    1.51 +by (blast_tac (claset() addDs [card_seteq]) 1); 
    1.52 +qed "psubset_card_mono" ;
    1.53 +
    1.54 +Goal "[| finite B;  A <= B |] ==> card A <= card B";
    1.55 +by (case_tac "A=B" 1);
    1.56 + by (Asm_simp_tac 1); 
    1.57 +by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
    1.58 +by (blast_tac (claset() addDs [card_seteq] addIs [order_less_imp_le]) 1); 
    1.59 +qed "card_mono" ;
    1.60  
    1.61  Goal "[| finite A; finite B |] \
    1.62  \     ==> card A + card B = card (A Un B) + card (A Int B)";
    1.63 @@ -399,30 +415,6 @@
    1.64  by (ALLGOALS (asm_simp_tac (simpset() addsimps [card_Diff1_less, less_imp_le])));
    1.65  qed "card_Diff1_le";
    1.66  
    1.67 -Goalw [psubset_def] "finite B ==> !A. A < B --> card(A) < card(B)";
    1.68 -by (etac finite_induct 1);
    1.69 -by (Simp_tac 1);
    1.70 -by (Clarify_tac 1);
    1.71 -by (case_tac "x:A" 1);
    1.72 -(*1*)
    1.73 -by (dres_inst_tac [("A","A")]mk_disjoint_insert 1);
    1.74 -by (Clarify_tac 1);
    1.75 -by (rotate_tac ~3 1);
    1.76 -by (asm_full_simp_tac (simpset() addsimps [finite_subset]) 1);
    1.77 -by (Blast_tac 1);
    1.78 -(*2*)
    1.79 -by (eres_inst_tac [("P","?a<?b")] notE 1);
    1.80 -by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff]) 1);
    1.81 -by (case_tac "A=F" 1);
    1.82 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_SucI])));
    1.83 -qed_spec_mp "psubset_card" ;
    1.84 -
    1.85 -Goal "[| A <= B; card B <= card A; finite B |] ==> A = B";
    1.86 -by (case_tac "A < B" 1);
    1.87 -by (datac psubset_card 1 1);
    1.88 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [psubset_eq])));
    1.89 -qed "card_seteq";
    1.90 -
    1.91  Goal "[| finite B; A <= B; card A < card B |] ==> A < B";
    1.92  by (etac psubsetI 1);
    1.93  by (Blast_tac 1);
    1.94 @@ -432,8 +424,9 @@
    1.95  
    1.96  Goal "finite A ==> card (f `` A) <= card A";
    1.97  by (etac finite_induct 1);
    1.98 -by (Simp_tac 1);
    1.99 -by (asm_simp_tac (simpset() addsimps [le_SucI,finite_imageI,card_insert_if]) 1);
   1.100 + by (Simp_tac 1);
   1.101 +by (asm_simp_tac (simpset() addsimps [le_SucI, finite_imageI, 
   1.102 +				      card_insert_if]) 1);
   1.103  qed "card_image_le";
   1.104  
   1.105  Goal "finite(A) ==> inj_on f A --> card (f `` A) = card A";
   1.106 @@ -449,9 +442,7 @@
   1.107  qed_spec_mp "card_image";
   1.108  
   1.109  Goal "[| finite A; f``A <= A; inj_on f A |] ==> f``A = A";
   1.110 -by (etac card_seteq 1);
   1.111 -by (dtac (card_image RS sym) 1);
   1.112 -by Auto_tac;
   1.113 +by (asm_simp_tac (simpset() addsimps [card_seteq, card_image]) 1);
   1.114  qed "endo_inj_surj";
   1.115  
   1.116  (*** Cardinality of the Powerset ***)
   1.117 @@ -814,30 +805,23 @@
   1.118  (* Main theorem: combinatorial theorem about number of subsets of a set *)
   1.119  Goal "(ALL A. finite A --> card {s. s <= A & card s = k} = (card A choose k))";
   1.120  by (induct_tac "k" 1);
   1.121 -by (simp_tac (simpset() addsimps [card_s_0_eq_empty]) 1);
   1.122 + by (simp_tac (simpset() addsimps [card_s_0_eq_empty]) 1);
   1.123  (* first 0 case finished *)
   1.124  (* prepare finite set induction *)
   1.125  by (rtac allI 1 THEN rtac impI 1);
   1.126  (* second induction *)
   1.127  by (etac finite_induct 1);
   1.128  by (ALLGOALS
   1.129 -    (simp_tac (simpset() addcongs [conj_cong] addsimps [card_s_0_eq_empty])));
   1.130 -by (stac choose_deconstruct 1);
   1.131 -by (assume_tac 1);
   1.132 -by (assume_tac 1);
   1.133 +    (asm_simp_tac (simpset() addcongs [conj_cong] 
   1.134 +                             addsimps [subset_empty, card_s_0_eq_empty, 
   1.135 +				       choose_deconstruct])));
   1.136  by (stac card_Un_disjoint 1);
   1.137 -by (Force_tac 3);
   1.138 -(** LEVEL 10 **)
   1.139 -(* use bijection *)
   1.140 -by (force_tac (claset(), simpset() addsimps [constr_bij]) 3);
   1.141 -(* finite goal *)
   1.142 -by (res_inst_tac [("B","Pow F")] finite_subset 1);
   1.143 -by (Blast_tac 1);
   1.144 -by (etac (finite_Pow_iff RS iffD2) 1);
   1.145 -(* finite goal *)
   1.146 -by (res_inst_tac [("B","Pow (insert x F)")] finite_subset 1);
   1.147 -by (Blast_tac 1);
   1.148 -by (blast_tac (claset() addIs [finite_Pow_iff RS iffD2]) 1);
   1.149 +   by (force_tac (claset(), simpset() addsimps [constr_bij]) 4);
   1.150 +  by (Force_tac 3);
   1.151 + by (blast_tac (claset() addIs [finite_Pow_iff RS iffD2, 
   1.152 +			 inst "B" "Pow (insert ?x ?F)" finite_subset]) 2);
   1.153 +by (blast_tac (claset() addIs [finite_Pow_iff RS iffD2 
   1.154 +			       RSN (2, finite_subset)]) 1);
   1.155  qed "n_sub_lemma";
   1.156  
   1.157  Goal "finite M ==> card {s. s <= M & card(s) = k} = ((card M) choose k)";