author paulson Thu, 28 Sep 2000 13:12:23 +0200 changeset 10098 ab0a3188f398 parent 10097 1db5bd97f6a3 child 10099 44da60e5331b
deleted card_0_empty_iff because it is the same as card_0_eq; renamed some variables
 src/HOL/Finite.ML file | annotate | diff | comparison | revisions
```--- 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 = {})";
-	      simpset()));
-qed "card_0_empty_iff";
-
Goal "finite A ==> card {B. B <= A & card B = 0} = 1";
-	 	            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 *)
@@ -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