src/HOL/Library/Formal_Power_Series.thy
 changeset 30273 ecd6f0ca62ea parent 29915 2146e512cec9 child 30488 5c4c3a9e9102
```     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Thu Mar 05 00:16:28 2009 +0100
1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Wed Mar 04 17:12:23 2009 -0800
1.3 @@ -1303,7 +1303,7 @@
1.4  lemma fps_power_nth:
1.5    fixes m :: nat and a :: "('a::comm_ring_1) fps"
1.6    shows "(a ^m)\$n = (if m=0 then 1\$n else setsum (\<lambda>v. setprod (\<lambda>j. a \$ (v!j)) {0..m - 1}) (natpermute n m))"
1.7 -  by (cases m, simp_all add: fps_power_nth_Suc)
1.8 +  by (cases m, simp_all add: fps_power_nth_Suc del: power_Suc)
1.9
1.10  lemma fps_nth_power_0:
1.11    fixes m :: nat and a :: "('a::{comm_ring_1, recpower}) fps"
1.12 @@ -1314,7 +1314,7 @@
1.13    {fix n assume m: "m = Suc n"
1.14      have c: "m = card {0..n}" using m by simp
1.15     have "(a ^m)\$0 = setprod (\<lambda>i. a\$0) {0..n}"
1.16 -     apply (simp add: m fps_power_nth del: replicate.simps)
1.17 +     apply (simp add: m fps_power_nth del: replicate.simps power_Suc)
1.18       apply (rule setprod_cong)
1.19       by (simp_all del: replicate.simps)
1.20     also have "\<dots> = (a\$0) ^ m"
1.21 @@ -1613,7 +1613,7 @@
1.22    shows "(fps_radical r (Suc k) (a ^ Suc k)) = a"
1.23  proof-
1.24    let ?ak = "a^ Suc k"
1.25 -  have ak0: "?ak \$ 0 = (a\$0) ^ Suc k" by (simp add: fps_nth_power_0)
1.26 +  have ak0: "?ak \$ 0 = (a\$0) ^ Suc k" by (simp add: fps_nth_power_0 del: power_Suc)
1.27    from r0 have th0: "r (Suc k) (a ^ Suc k \$ 0) ^ Suc k = a ^ Suc k \$ 0" using ak0 by auto
1.28    from r0 ak0 have th1: "r (Suc k) (a ^ Suc k \$ 0) = a \$ 0" by auto
1.29    from ak0 a0 have ak00: "?ak \$ 0 \<noteq>0 " by auto
1.30 @@ -1634,7 +1634,7 @@
1.31    from power_radical[of r, OF r0 a0]
1.32    have "fps_deriv (?r ^ Suc k) = fps_deriv a" by simp
1.33    hence "fps_deriv ?r * ?w = fps_deriv a"
1.34 -    by (simp add: fps_deriv_power mult_ac)
1.35 +    by (simp add: fps_deriv_power mult_ac del: power_Suc)
1.36    hence "?iw * fps_deriv ?r * ?w = ?iw * fps_deriv a" by simp
1.37    hence "fps_deriv ?r * (?iw * ?w) = fps_deriv a / ?w"
1.39 @@ -1663,7 +1663,7 @@
1.40    have ab0: "(a*b) \$ 0 \<noteq> 0" using a0 b0 by (simp add: fps_mult_nth)
1.41    from radical_unique[of r h "a*b" "fps_radical r (Suc h) a * fps_radical r (Suc h) b", OF r0[unfolded k] th0 ab0, symmetric]
1.42      power_radical[of r, OF ra0[unfolded k] a0] power_radical[of r, OF rb0[unfolded k] b0] k
1.43 -  have ?thesis by (auto simp add: power_mult_distrib)}
1.44 +  have ?thesis by (auto simp add: power_mult_distrib simp del: power_Suc)}
1.45  ultimately show ?thesis by (cases k, auto)
1.46  qed
1.47
1.48 @@ -1684,7 +1684,8 @@
1.49      from ra0 a0 have th00: "r (Suc h) (a\$0) \<noteq> 0" by auto
1.50      have ria0': "r (Suc h) (inverse a \$ 0) ^ Suc h = inverse a\$0"
1.51      using ria0 ra0 a0
1.52 -    by (simp add: fps_inverse_def  nonzero_power_inverse[OF th00, symmetric])
1.53 +    by (simp add: fps_inverse_def  nonzero_power_inverse[OF th00, symmetric]
1.54 +             del: power_Suc)
1.55    from inverse_mult_eq_1[OF a0] have th0: "a * inverse a = 1"
1.57    from radical_unique[where a=1 and b=1 and r=r and k=h, simplified, OF r1[unfolded k]]
1.58 @@ -1848,7 +1849,8 @@
1.59        moreover
1.60        {fix n1 assume n1: "n = Suc n1"
1.61  	have "?i \$ n = setsum (\<lambda>i. (fps_inv a \$ i) * (a^i)\$n) {0 .. n1} + fps_inv a \$ Suc n1 * (a \$ 1)^ Suc n1"
1.62 -	  by (simp add: fps_compose_nth n1 startsby_zero_power_nth_same[OF a0])
1.63 +	  by (simp add: fps_compose_nth n1 startsby_zero_power_nth_same[OF a0]
1.64 +                   del: power_Suc)
1.65  	also have "\<dots> = setsum (\<lambda>i. (fps_inv a \$ i) * (a^i)\$n) {0 .. n1} + (X\$ Suc n1 - setsum (\<lambda>i. (fps_inv a \$ i) * (a^i)\$n) {0 .. n1})"
1.66  	  using a0 a1 n1 by (simp add: fps_inv_def)
1.67  	also have "\<dots> = X\$n" using n1 by simp
1.68 @@ -1878,7 +1880,8 @@
1.69        moreover
1.70        {fix n1 assume n1: "n = Suc n1"
1.71  	have "?i \$ n = setsum (\<lambda>i. (fps_ginv b a \$ i) * (a^i)\$n) {0 .. n1} + fps_ginv b a \$ Suc n1 * (a \$ 1)^ Suc n1"
1.72 -	  by (simp add: fps_compose_nth n1 startsby_zero_power_nth_same[OF a0])
1.73 +	  by (simp add: fps_compose_nth n1 startsby_zero_power_nth_same[OF a0]
1.74 +                   del: power_Suc)
1.75  	also have "\<dots> = setsum (\<lambda>i. (fps_ginv b a \$ i) * (a^i)\$n) {0 .. n1} + (b\$ Suc n1 - setsum (\<lambda>i. (fps_ginv b a \$ i) * (a^i)\$n) {0 .. n1})"
1.76  	  using a0 a1 n1 by (simp add: fps_ginv_def)
1.77  	also have "\<dots> = b\$n" using n1 by simp
1.78 @@ -2086,7 +2089,7 @@
1.79    {fix h assume h: "k = Suc h"
1.80      {fix n
1.81        {assume kn: "k>n" hence "?l \$ n = ?r \$n" using a0 startsby_zero_power_prefix[OF a0] h
1.82 -	  by (simp add: fps_compose_nth)}
1.83 +	  by (simp add: fps_compose_nth del: power_Suc)}
1.84        moreover
1.85        {assume kn: "k \<le> n"
1.86  	hence "?l\$n = ?r\$n"
1.87 @@ -2138,7 +2141,7 @@
1.88  proof-
1.89    {fix n
1.90      have "?l\$n = ?r \$ n"
1.91 -  apply (auto simp add: E_def field_simps power_Suc[symmetric]simp del: fact_Suc of_nat_Suc)
1.92 +  apply (auto simp add: E_def field_simps power_Suc[symmetric]simp del: fact_Suc of_nat_Suc power_Suc)
1.93    by (simp add: of_nat_mult ring_simps)}
1.94  then show ?thesis by (simp add: fps_eq_iff)
1.95  qed
```