# HG changeset patch
# User paulson
# Date 1385398048 0
# Node ID bfbfecb3102ed9f49ea5a05ae5262920c373fe07
# Parent  3936fb5803d683b31e229e81289f0318225ebf07
Small simplifications to proofs

diff -r 3936fb5803d6 -r bfbfecb3102e src/HOL/Library/Binomial.thy
--- a/src/HOL/Library/Binomial.thy	Mon Nov 25 16:00:09 2013 +0000
+++ b/src/HOL/Library/Binomial.thy	Mon Nov 25 16:47:28 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 (simp add: pochhammer_Suc_setprod)
-    apply (rule_tac x="n" in bexI)
-    using assms
-    apply auto
-    done
+    by (simp add: pochhammer_Suc_setprod)
+       (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 @@
   apply (auto simp add: pochhammer_of_nat_eq_0_iff)
   apply (cases n)
    apply (auto simp add: pochhammer_def algebra_simps group_add_class.eq_neg_iff_add_eq_0)
-  apply (rule_tac x=x in exI)
-  apply auto
+  apply (metis leD not_less_eq)
   done