# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1415374808 0
# Node ID a3be9a47e2d72950e8f095b9568e9ffa5e24d043
# Parent  229765cc3414674969a20cfecbe71267330e0dd1
Tidying up. Removing unnecessary conditions from some theorems.

diff -r 229765cc3414 -r a3be9a47e2d7 src/HOL/Algebra/Exponent.thy
--- a/src/HOL/Algebra/Exponent.thy	Fri Nov 07 11:28:37 2014 +0100
+++ b/src/HOL/Algebra/Exponent.thy	Fri Nov 07 15:40:08 2014 +0000
@@ -256,11 +256,8 @@
   @{term "exponent p (Suc (j + k) choose Suc k) + exponent p (Suc k)"}
   the common terms cancel, proving the conclusion.*}
  apply (simp del: bad_Sucs add: exponent_mult_add)
-txt{*Establishing the equation requires first applying 
-   @{text Suc_times_binomial_eq} ...*}
-apply (simp del: bad_Sucs add: Suc_times_binomial_eq [symmetric])
-txt{*...then @{text exponent_mult_add} and the quantified premise.*}
-apply (simp del: bad_Sucs add: exponent_mult_add)
+apply (simp del: bad_Sucs add: mult_ac Suc_times_binomial exponent_mult_add)
+
 done
 
 (*The lemma above, with two changes of variables*)
@@ -308,11 +305,10 @@
                     a + exponent p m")
  apply (simp add: exponent_mult_add)
 txt{*one subgoal left!*}
-apply (subst times_binomial_minus1_eq, simp, simp)
-apply (subst exponent_mult_add, simp)
-apply (simp (no_asm_simp))
-apply arith
-apply (simp del: bad_Sucs add: exponent_mult_add const_p_fac_right)
+apply (auto simp: mult_ac)
+apply (subst times_binomial_minus1_eq, simp)
+apply (simp add: diff_le_mono exponent_mult_add)
+apply (metis const_p_fac_right mult.commute)
 done
 
 end
diff -r 229765cc3414 -r a3be9a47e2d7 src/HOL/Number_Theory/Binomial.thy
--- a/src/HOL/Number_Theory/Binomial.thy	Fri Nov 07 11:28:37 2014 +0100
+++ b/src/HOL/Number_Theory/Binomial.thy	Fri Nov 07 15:40:08 2014 +0000
@@ -59,26 +59,26 @@
   by (metis binomial_eq_0_iff not_less0 not_less zero_less_binomial)
 
 lemma Suc_times_binomial_eq:
-  "k \<le> n \<Longrightarrow> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"
-  apply (induct n arbitrary: k, simp)
+  "Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"
+  apply (induct n arbitrary: k, simp add: binomial.simps)
   apply (case_tac k)
    apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq binomial_eq_0)
   done
 
 text{*The absorption property*}
 lemma Suc_times_binomial:
-  "k \<le> n \<Longrightarrow> (Suc n choose Suc k) * Suc k = Suc n * (n choose k)"
-  by (rule Suc_times_binomial_eq [symmetric])
+  "Suc k * (Suc n choose Suc k) = Suc n * (n choose k)"
+  using Suc_times_binomial_eq by auto
 
 text{*This is the well-known version of absorption, but it's harder to use because of the
   need to reason about division.*}
 lemma binomial_Suc_Suc_eq_times:
-    "k \<le> n \<Longrightarrow> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"
+    "(Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"
   by (simp add: Suc_times_binomial_eq del: mult_Suc mult_Suc_right)
 
 text{*Another version of absorption, with -1 instead of Suc.*}
 lemma times_binomial_minus1_eq:
-  "k \<le> n \<Longrightarrow> 0 < k \<Longrightarrow> (n choose k) * k = n * ((n - 1) choose (k - 1))"
+  "0 < k \<Longrightarrow> k * (n choose k) = n * ((n - 1) choose (k - 1))"
   using Suc_times_binomial_eq [where n = "n - 1" and k = "k - 1"]
   by (auto split add: nat_diff_split)
 
@@ -665,6 +665,7 @@
     by (simp add: binomial_altdef_nat mult.commute)
 qed
 
+text{*The "Subset of a Subset" identity*}
 lemma choose_mult:
   assumes "k\<le>m" "m\<le>n"
     shows "(n choose m) * (m choose k) = (n choose k) * ((n-k) choose (m-k))"
@@ -674,14 +675,6 @@
 
 subsection {* Binomial coefficients *}
 
-lemma choose_plus_one_nat:
-     "((n::nat) + 1) choose (k + 1) =(n choose (k + 1)) + (n choose k)"
-  by (simp add: choose_reduce_nat)
-
-lemma choose_Suc_nat: 
-     "(Suc n) choose (Suc k) = (n choose (Suc k)) + (n choose k)"
-  by (simp add: choose_reduce_nat)
-
 lemma choose_one: "(n::nat) choose 1 = n"
   by simp