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
```