more finiteness

--- a/src/HOL/Finite_Set.thy	Sat Feb 14 19:27:26 2009 +0100
+++ b/src/HOL/Finite_Set.thy	Sun Feb 15 07:54:16 2009 +0100
@@ -325,9 +325,9 @@
   @{prop "finite C ==> ALL A B. (UNION A B) <= C --> finite {x. x:A & B x \<noteq> {}}"}
   by induction. *}
 
-lemma finite_UN [simp]: "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))"
-  by (blast intro: finite_UN_I finite_subset)
-
+lemma finite_UN [simp]:
+  "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))"
+by (blast intro: finite_UN_I finite_subset)
 
 lemma finite_Plus: "[| finite A; finite B |] ==> finite (A <+> B)"
 by (simp add: Plus_def)
@@ -396,6 +396,12 @@
 lemma finite_Collect_subsets[simp,intro]: "finite A \<Longrightarrow> finite{B. B \<subseteq> A}"
 by(simp add: Pow_def[symmetric])
 
+lemma finite_bex_subset[simp]:
+  "finite B \<Longrightarrow> finite{x. EX A<=B. P x A} = (ALL A<=B. finite{x. P x A})"
+apply(subgoal_tac "{x. EX A<=B. P x A} = (UN A:Pow B. {x. P x A})")
+ apply auto
+done
+
 lemma finite_UnionD: "finite(\<Union>A) \<Longrightarrow> finite A"
 by(blast intro: finite_subset[OF subset_Pow_Union])
 

--- a/src/HOL/Library/Binomial.thy	Sat Feb 14 19:27:26 2009 +0100
+++ b/src/HOL/Library/Binomial.thy	Sun Feb 15 07:54:16 2009 +0100
@@ -106,6 +106,21 @@
   apply (erule rev_mp, subst card_Diff_singleton)
   apply (auto intro: finite_subset)
   done
+(*
+lemma "finite(UN y. {x. P x y})"
+apply simp
+lemma Collect_ex_eq
+
+lemma "{x. EX y. P x y} = (UN y. {x. P x y})"
+apply blast
+*)
+
+lemma finite_bex_subset[simp]:
+  "finite B \<Longrightarrow> (!!A. A<=B \<Longrightarrow> finite{x. P x A}) \<Longrightarrow> finite{x. EX A<=B. P x A}"
+apply(subgoal_tac "{x. EX A<=B. P x A} = (UN A:Pow B. {x. P x A})")
+ apply simp
+apply blast
+done
 
 text{*There are as many subsets of @{term A} having cardinality @{term k}
  as there are sets obtained from the former by inserting a fixed element
@@ -114,14 +129,10 @@
    "[|finite A; x \<notin> A|] ==>
     card {B. EX C. C <= A & card(C) = k & B = insert x C} =
     card {B. B <= A & card(B) = k}"
-  apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq)
-       apply (auto elim!: equalityE simp add: inj_on_def)
-    apply (subst Diff_insert0, auto)
-   txt {* finiteness of the two sets *}
-   apply (rule_tac [2] B = "Pow (A)" in finite_subset)
-   apply (rule_tac B = "Pow (insert x A)" in finite_subset)
-   apply fast+
-  done
+apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq)
+     apply (auto elim!: equalityE simp add: inj_on_def)
+apply (subst Diff_insert0, auto)
+done
 
 text {*
   Main theorem: combinatorial statement about number of subsets of a set.