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.38      by (simp add: fps_divide_def)
    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.56      by (simp add: mult_commute)
    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