# HG changeset patch
# User paulson
# Date 970139543 -7200
# Node ID ab0a3188f398db9dd56f87636b5522ff3705f35c
# Parent  1db5bd97f6a31b6e7e62cf5d81194a76a9ac3f93
deleted card_0_empty_iff because it is the same as card_0_eq;
renamed some variables

diff -r 1db5bd97f6a3 -r ab0a3188f398 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Wed Sep 27 19:51:11 2000 +0200
+++ b/src/HOL/Finite.ML	Thu Sep 28 13:12:23 2000 +0200
@@ -803,14 +803,9 @@
 
 (*** Basic theorem about "choose".  By Florian Kammueller, tidied by LCP ***)
 
-Goal "finite S ==> (card S = 0) = (S = {})"; 
-by (auto_tac (claset() addDs [card_Suc_Diff1],
-	      simpset()));
-qed "card_0_empty_iff";
-
 Goal "finite A ==> card {B. B <= A & card B = 0} = 1";
 by (asm_simp_tac (simpset() addcongs [conj_cong]
-	 	            addsimps [finite_subset RS card_0_empty_iff]) 1);
+	 	            addsimps [finite_subset RS card_0_eq]) 1);
 by (simp_tac (simpset() addcongs [rev_conj_cong]) 1);
 qed "card_s_0_eq_empty";
 
@@ -840,12 +835,12 @@
 by (auto_tac (claset() addIs [le_anti_sym,card_inj_on_le], simpset()));
 qed "card_bij_eq";
 
-Goal "[| finite M; x ~: M |]  \
-\     ==> card{s. EX t. t <= M & card(t) = k & s = insert x t} = \
-\         card {s. s <= M & card(s) = k}";
+Goal "[| finite A; x ~: A |]  \
+\     ==> card{B. EX C. C <= A & card(C) = k & B = insert x C} = \
+\         card {B. B <= A & card(B) = k}";
 by (res_inst_tac [("f", "%s. s - {x}"), ("g","insert x")] card_bij_eq 1);
-by (res_inst_tac [("B","Pow(insert x M)")] finite_subset 1);
-by (res_inst_tac [("B","Pow(M)")] finite_subset 3);
+by (res_inst_tac [("B","Pow(insert x A)")] finite_subset 1);
+by (res_inst_tac [("B","Pow(A)")] finite_subset 3);
 by (REPEAT(Fast_tac 1));
 (* arity *)
 by (auto_tac (claset() addSEs [equalityE], simpset() addsimps [inj_on_def]));
@@ -854,7 +849,7 @@
 qed "constr_bij";
 
 (* Main theorem: combinatorial theorem about number of subsets of a set *)
-Goal "(ALL A. finite A --> card {s. s <= A & card s = k} = (card A choose k))";
+Goal "(ALL A. finite A --> card {B. B <= A & card B = k} = (card A choose k))";
 by (induct_tac "k" 1);
  by (simp_tac (simpset() addsimps [card_s_0_eq_empty]) 1);
 (* first 0 case finished *)
@@ -864,7 +859,7 @@
 by (etac finite_induct 1);
 by (ALLGOALS
     (asm_simp_tac (simpset() addcongs [conj_cong] 
-                             addsimps [card_s_0_eq_empty,choose_deconstruct])));
+                     addsimps [card_s_0_eq_empty, choose_deconstruct])));
 by (stac card_Un_disjoint 1);
    by (force_tac (claset(), simpset() addsimps [constr_bij]) 4);
   by (Force_tac 3);
@@ -874,6 +869,6 @@
 			       RSN (2, finite_subset)]) 1);
 qed "n_sub_lemma";
 
-Goal "finite M ==> card {s. s <= M & card(s) = k} = ((card M) choose k)";
+Goal "finite A ==> card {B. B <= A & card(B) = k} = ((card A) choose k)";
 by (asm_simp_tac (simpset() addsimps [n_sub_lemma]) 1);
 qed "n_subsets";