1.1 --- a/src/HOL/Library/Binomial.thy Mon Nov 25 16:00:09 2013 +0000
1.2 +++ b/src/HOL/Library/Binomial.thy Mon Nov 25 16:47:28 2013 +0000
1.3 @@ -91,17 +91,14 @@
1.4 {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}"
1.5 apply safe
1.6 apply (auto intro: finite_subset [THEN card_insert_disjoint])
1.7 - apply (drule_tac x = "xa - {x}" in spec)
1.8 - 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)
1.9 + by (metis (full_types) Diff_insert_absorb Set.set_insert Zero_neq_Suc card_Diff_singleton_if
1.10 + card_eq_0_iff diff_Suc_1 in_mono subset_insert_iff)
1.11
1.12 lemma finite_bex_subset [simp]:
1.13 assumes "finite B"
1.14 and "\<And>A. A \<subseteq> B \<Longrightarrow> finite {x. P x A}"
1.15 shows "finite {x. \<exists>A \<subseteq> B. P x A}"
1.16 -proof -
1.17 - have "{x. \<exists>A\<subseteq>B. P x A} = (\<Union>A \<in> Pow B. {x. P x A})" by blast
1.18 - with assms show ?thesis by simp
1.19 -qed
1.20 + by (metis (no_types) assms finite_Collect_bounded_ex finite_Collect_subsets)
1.21
1.22 text{*There are as many subsets of @{term A} having cardinality @{term k}
1.23 as there are sets obtained from the former by inserting a fixed element
1.24 @@ -259,11 +256,8 @@
1.25 case False
1.26 from assms obtain h where "k = Suc h" by (cases k) auto
1.27 then show ?thesis
1.28 - apply (simp add: pochhammer_Suc_setprod)
1.29 - apply (rule_tac x="n" in bexI)
1.30 - using assms
1.31 - apply auto
1.32 - done
1.33 + by (simp add: pochhammer_Suc_setprod)
1.34 + (metis Suc_leI Suc_le_mono assms atLeastAtMost_iff less_eq_nat.simps(1))
1.35 qed
1.36
1.37 lemma pochhammer_of_nat_eq_0_lemma':
1.38 @@ -292,8 +286,7 @@
1.39 apply (auto simp add: pochhammer_of_nat_eq_0_iff)
1.40 apply (cases n)
1.41 apply (auto simp add: pochhammer_def algebra_simps group_add_class.eq_neg_iff_add_eq_0)
1.42 - apply (rule_tac x=x in exI)
1.43 - apply auto
1.44 + apply (metis leD not_less_eq)
1.45 done
1.46
1.47