src/HOL/Library/Binomial.thy
changeset 39302 d7728f65b353
parent 39198 f967a16dfcdd
child 46507 1b24c24017dd
     1.1 --- a/src/HOL/Library/Binomial.thy	Mon Sep 13 08:43:48 2010 +0200
     1.2 +++ b/src/HOL/Library/Binomial.thy	Mon Sep 13 11:13:15 2010 +0200
     1.3 @@ -236,7 +236,7 @@
     1.4      have th1: "(\<Prod>n\<in>{1\<Colon>nat..n}. a + of_nat n) =
     1.5        (\<Prod>n\<in>{0\<Colon>nat..n - 1}. a + 1 + of_nat n)"
     1.6        apply (rule setprod_reindex_cong [where f = Suc])
     1.7 -      using n0 by (auto simp add: ext_iff field_simps)
     1.8 +      using n0 by (auto simp add: fun_eq_iff field_simps)
     1.9      have ?thesis apply (simp add: pochhammer_def)
    1.10      unfolding setprod_insert[OF th0, unfolded eq]
    1.11      using th1 by (simp add: field_simps)}
    1.12 @@ -248,7 +248,7 @@
    1.13    
    1.14    apply (cases n, simp_all add: of_nat_setprod pochhammer_Suc_setprod)
    1.15    apply (rule setprod_reindex_cong[where f=Suc])
    1.16 -  by (auto simp add: ext_iff)
    1.17 +  by (auto simp add: fun_eq_iff)
    1.18  
    1.19  lemma pochhammer_of_nat_eq_0_lemma: assumes kn: "k > n"
    1.20    shows "pochhammer (- (of_nat n :: 'a:: idom)) k = 0"
    1.21 @@ -315,7 +315,7 @@
    1.22        apply (rule strong_setprod_reindex_cong[where f = "%i. h - i"])
    1.23        apply (auto simp add: inj_on_def image_def h )
    1.24        apply (rule_tac x="h - x" in bexI)
    1.25 -      by (auto simp add: ext_iff h of_nat_diff)}
    1.26 +      by (auto simp add: fun_eq_iff h of_nat_diff)}
    1.27    ultimately show ?thesis by (cases k, auto)
    1.28  qed
    1.29  
    1.30 @@ -410,11 +410,11 @@
    1.31      have eq': "(\<Prod>i\<in>{0..h}. of_nat n + - (of_nat i :: 'a)) = (\<Prod>i\<in>{n - h..n}. of_nat i)"
    1.32        apply (rule strong_setprod_reindex_cong[where f="op - n"])
    1.33        using h kn 
    1.34 -      apply (simp_all add: inj_on_def image_iff Bex_def set_ext_iff)
    1.35 +      apply (simp_all add: inj_on_def image_iff Bex_def set_eq_iff)
    1.36        apply clarsimp
    1.37        apply (presburger)
    1.38        apply presburger
    1.39 -      by (simp add: ext_iff field_simps of_nat_add[symmetric] del: of_nat_add)
    1.40 +      by (simp add: fun_eq_iff field_simps of_nat_add[symmetric] del: of_nat_add)
    1.41      have th0: "finite {1..n - Suc h}" "finite {n - h .. n}" 
    1.42  "{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
    1.43      from eq[symmetric]