author paulson Mon, 25 Nov 2013 16:59:02 +0000 changeset 54586 ebc8f6bf20c0 parent 54584 2bbcbf8cf47e (current diff) parent 54585 bfbfecb3102e (diff) child 54587 19cd731eb745
mreged
```--- a/src/HOL/Library/Binomial.thy	Mon Nov 25 15:56:23 2013 +0100
+++ b/src/HOL/Library/Binomial.thy	Mon Nov 25 16:59:02 2013 +0000
@@ -91,17 +91,14 @@
{s. s \<subseteq> M \<and> card s = Suc k} \<union> {s. \<exists>t. t \<subseteq> M \<and> card t = k \<and> s = insert x t}"
apply safe
apply (auto intro: finite_subset [THEN card_insert_disjoint])
-  apply (drule_tac x = "xa - {x}" in spec)
-  by (metis card_Diff_singleton_if card_infinite diff_Suc_1 in_mono insert_Diff_single insert_absorb lessI less_nat_zero_code subset_insert_iff)
+  by (metis (full_types) Diff_insert_absorb Set.set_insert Zero_neq_Suc card_Diff_singleton_if
+     card_eq_0_iff diff_Suc_1 in_mono subset_insert_iff)

lemma finite_bex_subset [simp]:
assumes "finite B"
and "\<And>A. A \<subseteq> B \<Longrightarrow> finite {x. P x A}"
shows "finite {x. \<exists>A \<subseteq> B. P x A}"
-proof -
-  have "{x. \<exists>A\<subseteq>B. P x A} = (\<Union>A \<in> Pow B. {x. P x A})" by blast
-  with assms show ?thesis by simp
-qed
+  by (metis (no_types) assms finite_Collect_bounded_ex finite_Collect_subsets)

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
@@ -259,11 +256,8 @@
case False
from assms obtain h where "k = Suc h" by (cases k) auto
then show ?thesis
-    apply (rule_tac x="n" in bexI)
-    using assms
-    apply auto
-    done
+       (metis Suc_leI Suc_le_mono assms atLeastAtMost_iff less_eq_nat.simps(1))
qed

lemma pochhammer_of_nat_eq_0_lemma':
@@ -292,8 +286,7 @@