src/HOL/Library/Binomial.thy

   
 lemma binomial_fact: 
   assumes kn: "k \<le> n" 
   shows "(of_nat (n choose k) :: 'a::field_char_0) = of_nat (fact n) / (of_nat (fact k) * of_nat (fact (n - k)))"
   using binomial_fact_lemma[OF kn]
-  by (simp add: field_simps of_nat_mult[symmetric])
+  by (simp add: field_eq_simps of_nat_mult [symmetric])
 
 lemma binomial_gbinomial: "of_nat (n choose k) = of_nat n gchoose k"
 proof-
   {assume kn: "k > n" 
     from kn binomial_eq_0[OF kn] have ?thesis 
-      by (simp add: gbinomial_pochhammer field_simps
+      by (simp add: gbinomial_pochhammer field_eq_simps
         pochhammer_of_nat_eq_0_iff)}
   moreover
   {assume "k=0" then have ?thesis by simp}
   moreover
   {assume kn: "k \<le> n" and k0: "k\<noteq> 0"

     have th0: "finite {1..n - Suc h}" "finite {n - h .. n}" 
 "{1..n - Suc h} \<inter> {n - h .. n} = {}" and eq3: "{1..n - Suc h} \<union> {n - h .. n} = {1..n}" using h kn by auto
     from eq[symmetric]
     have ?thesis using kn
       apply (simp add: binomial_fact[OF kn, where ?'a = 'a] 
-        gbinomial_pochhammer field_simps pochhammer_Suc_setprod)
+        gbinomial_pochhammer field_eq_simps pochhammer_Suc_setprod)
       apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc)
       unfolding setprod_Un_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h]
       unfolding mult_assoc[symmetric] 
       unfolding setprod_timesf[symmetric]
       apply simp

 lemma gbinomial_mult_1: "a * (a gchoose n) = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))" (is "?l = ?r")
 proof-
   have "?r = ((- 1) ^n * pochhammer (- a) n / of_nat (fact n)) * (of_nat n - (- a + of_nat n))"
     unfolding gbinomial_pochhammer
     pochhammer_Suc fact_Suc of_nat_mult right_diff_distrib power_Suc
-    by (simp add:  field_simps del: of_nat_Suc)
+    by (simp add:  field_eq_simps del: of_nat_Suc)
   also have "\<dots> = ?l" unfolding gbinomial_pochhammer
     by (simp add: ring_simps)
   finally show ?thesis ..
 qed