src/HOL/Library/Formal_Power_Series.thy
changeset 31790 05c92381363c
parent 31776 151c3f5f28f9
child 31968 0314441a53a6
     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Tue Jun 23 21:07:39 2009 +0200
     1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Wed Jun 24 09:41:14 2009 +0200
     1.3 @@ -1615,7 +1615,7 @@
     1.4  	  fix v assume v: "v \<in> {xs \<in> natpermute n (Suc k). n \<in> set xs}"
     1.5  	  let ?ths = "(\<Prod>j\<in>{0..k}. a $ v ! j) = a $ n * (?r$0)^k"
     1.6  	  from v obtain i where i: "i \<in> {0..k}" "v = replicate (k+1) 0 [i:= n]"
     1.7 -	    unfolding Suc_plus1 natpermute_contain_maximal by (auto simp del: replicate.simps)
     1.8 +	    unfolding Suc_eq_plus1 natpermute_contain_maximal by (auto simp del: replicate.simps)
     1.9  	  have "(\<Prod>j\<in>{0..k}. a $ v ! j) = (\<Prod>j\<in>{0..k}. if j = i then a $ n else r (Suc k) (b$0))"
    1.10  	    apply (rule setprod_cong, simp)
    1.11  	    using i a0 by (simp del: replicate.simps)
    1.12 @@ -1651,7 +1651,7 @@
    1.13  	from H have "b$n = a^Suc k $ n" by (simp add: fps_eq_iff)
    1.14  	also have "a ^ Suc k$n = setsum ?g ?Pnkn + setsum ?g ?Pnknn"
    1.15  	  unfolding fps_power_nth_Suc
    1.16 -	  using setsum_Un_disjoint[OF f d, unfolded Suc_plus1[symmetric],
    1.17 +	  using setsum_Un_disjoint[OF f d, unfolded Suc_eq_plus1[symmetric],
    1.18  	    unfolded eq, of ?g] by simp
    1.19  	also have "\<dots> = of_nat (k+1) * a $ n * (?r $ 0)^k + setsum ?f ?Pnknn" unfolding th0 th1 ..
    1.20  	finally have "of_nat (k+1) * a $ n * (?r $ 0)^k = b$n - setsum ?f ?Pnknn" by simp