# HG changeset patch
# User nipkow
# Date 1234680886 -3600
# Node ID 1e07290c46c3786497c6ec501e092bd0e5faac1d
# Parent  2146e512cec98e10cf19585d62aa9158a7e35cf3# Parent  214755b03df37c41db2b304716fb8ece9a0593ee
merged

diff -r 2146e512cec9 -r 1e07290c46c3 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sat Feb 14 19:01:31 2009 -0800
+++ b/src/HOL/Finite_Set.thy	Sun Feb 15 07:54:46 2009 +0100
@@ -176,7 +176,7 @@
 lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)"
 by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI)
 
-lemma finite_disjI[simp]:
+lemma finite_Collect_disjI[simp]:
   "finite{x. P x | Q x} = (finite{x. P x} & finite{x. Q x})"
 by(simp add:Collect_disj_eq)
 
@@ -184,7 +184,7 @@
   -- {* The converse obviously fails. *}
 by (blast intro: finite_subset)
 
-lemma finite_conjI [simp, intro]:
+lemma finite_Collect_conjI [simp, intro]:
   "finite{x. P x} | finite{x. Q x} ==> finite{x. P x & Q x}"
   -- {* The converse obviously fails. *}
 by(simp add:Collect_conj_eq)
@@ -247,7 +247,7 @@
   "finite(A::'a set) \<Longrightarrow> finite(-A) = finite(UNIV::'a set)"
 by(simp add:Compl_eq_Diff_UNIV)
 
-lemma finite_not[simp]:
+lemma finite_Collect_not[simp]:
   "finite{x::'a. P x} \<Longrightarrow> finite{x. ~P x} = finite(UNIV::'a set)"
 by(simp add:Collect_neg_eq)
 
@@ -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)
@@ -393,6 +393,14 @@
     by induct (simp_all add: finite_UnI finite_imageI Pow_insert)
 qed
 
+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])
diff -r 2146e512cec9 -r 1e07290c46c3 src/HOL/Library/Binomial.thy
--- a/src/HOL/Library/Binomial.thy	Sat Feb 14 19:01:31 2009 -0800
+++ b/src/HOL/Library/Binomial.thy	Sun Feb 15 07:54:46 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.