1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Mon May 18 09:48:06 2009 +0200
     1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Mon May 18 23:42:55 2009 +0100
     1.3 @@ -2102,6 +2102,80 @@
     1.4    ultimately show ?thesis by (cases n, auto)
     1.5  qed
     1.6  
     1.7 +lemma fps_compose_uminus: "- (a::'a::ring_1 fps) oo c = - (a oo c)"
     1.8 +  by (simp add: fps_eq_iff fps_compose_nth ring_simps setsum_negf[symmetric])
     1.9 +
    1.10 +lemma fps_compose_sub_distrib:
    1.11 +  shows "(a - b) oo (c::'a::ring_1 fps) = (a oo c) - (b oo c)"
    1.12 +  unfolding diff_minus fps_compose_uminus fps_compose_add_distrib ..
    1.13 +
    1.14 +lemma X_fps_compose:"X oo a = Abs_fps (\<lambda>n. if n = 0 then (0::'a::comm_ring_1) else a$n)"
    1.15 +  by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum_delta power_Suc)
    1.16 +
    1.17 +lemma fps_inverse_compose:
    1.18 +  assumes b0: "(b$0 :: 'a::field) = 0" and a0: "a$0 \<noteq> 0"
    1.19 +  shows "inverse a oo b = inverse (a oo b)"
    1.20 +proof-
    1.21 +  let ?ia = "inverse a"
    1.22 +  let ?ab = "a oo b"
    1.23 +  let ?iab = "inverse ?ab"
    1.24 +
    1.25 +from a0 have ia0: "?ia $ 0 \<noteq> 0" by (simp )
    1.26 +from a0 have ab0: "?ab $ 0 \<noteq> 0" by (simp add: fps_compose_def)
    1.27 +thm inverse_mult_eq_1[OF ab0]
    1.28 +have "(?ia oo b) *  (a oo b) = 1"
    1.29 +unfolding fps_compose_mult_distrib[OF b0, symmetric]
    1.30 +unfolding inverse_mult_eq_1[OF a0]
    1.31 +fps_compose_1 ..
    1.32 +
    1.33 +then have "(?ia oo b) *  (a oo b) * ?iab  = 1 * ?iab" by simp
    1.34 +then have "(?ia oo b) *  (?iab * (a oo b))  = ?iab" by simp
    1.35 +then show ?thesis 
    1.36 +  unfolding inverse_mult_eq_1[OF ab0] by simp
    1.37 +qed
    1.38 +
    1.39 +lemma fps_divide_compose:
    1.40 +  assumes c0: "(c$0 :: 'a::field) = 0" and b0: "b$0 \<noteq> 0"
    1.41 +  shows "(a/b) oo c = (a oo c) / (b oo c)"
    1.42 +    unfolding fps_divide_def fps_compose_mult_distrib[OF c0]
    1.43 +    fps_inverse_compose[OF c0 b0] ..
    1.44 +
    1.45 +lemma gp: assumes a0: "a$0 = (0::'a::field)"
    1.46 +  shows "(Abs_fps (\<lambda>n. 1)) oo a = 1/(1 - a)" (is "?one oo a = _")
    1.47 +proof-
    1.48 +  have o0: "?one $ 0 \<noteq> 0" by simp
    1.49 +  have th0: "(1 - X) $ 0 \<noteq> (0::'a)" by simp  
    1.50 +  from fps_inverse_gp[where ?'a = 'a]
    1.51 +  have "inverse ?one = 1 - X" by (simp add: fps_eq_iff)
    1.52 +  hence "inverse (inverse ?one) = inverse (1 - X)" by simp
    1.53 +  hence th: "?one = 1/(1 - X)" unfolding fps_inverse_idempotent[OF o0] 
    1.54 +    by (simp add: fps_divide_def)
    1.55 +  show ?thesis unfolding th
    1.56 +    unfolding fps_divide_compose[OF a0 th0]
    1.57 +    fps_compose_1 fps_compose_sub_distrib X_fps_compose_startby0[OF a0] ..
    1.58 +qed
    1.59 +
    1.60 +lemma fps_const_power[simp]: "fps_const (c::'a::ring_1) ^ n = fps_const (c^n)"
    1.61 +by (induct n, auto)
    1.62 +
    1.63 +lemma fps_compose_radical:
    1.64 +  assumes b0: "b$0 = (0::'a::{field, ring_char_0})"
    1.65 +  and ra0: "r (Suc k) (a$0) ^ Suc k = a$0"
    1.66 +  and a0: "a$0 \<noteq> 0"
    1.67 +  shows "fps_radical r (Suc k)  a oo b = fps_radical r (Suc k) (a oo b)"
    1.68 +proof-
    1.69 +  let ?r = "fps_radical r (Suc k)"
    1.70 +  let ?ab = "a oo b"
    1.71 +  have ab0: "?ab $ 0 = a$0" by (simp add: fps_compose_def)
    1.72 +  from ab0 a0 ra0 have rab0: "?ab $ 0 \<noteq> 0" "r (Suc k) (?ab $ 0) ^ Suc k = ?ab $ 0" by simp_all
    1.73 +  have th00: "r (Suc k) ((a oo b) $ 0) = (fps_radical r (Suc k) a oo b) $ 0"
    1.74 +    by (simp add: ab0 fps_compose_def)
    1.75 +  have th0: "(?r a oo b) ^ (Suc k) = a  oo b"
    1.76 +    unfolding fps_compose_power[OF b0]
    1.77 +    unfolding iffD1[OF power_radical[of a r k], OF a0 ra0]  .. 
    1.78 +  from iffD1[OF radical_unique[where r=r and k=k and b= ?ab and a = "?r a oo b", OF rab0(2) th00 rab0(1)], OF th0] show ?thesis  . 
    1.79 +qed
    1.80 +
    1.81  lemma fps_const_mult_apply_left:
    1.82    "fps_const c * (a oo b) = (fps_const c * a) oo b"
    1.83    by (simp add: fps_eq_iff fps_compose_nth setsum_right_distrib mult_assoc)
    1.84 @@ -2249,15 +2323,6 @@
    1.85  lemma E_nth_deriv[simp]: "fps_nth_deriv n (E (a::'a::{field, ring_char_0})) = (fps_const a)^n * (E a)"
    1.86    by (induct n, auto simp add: power_Suc)
    1.87  
    1.88 -lemma fps_compose_uminus: "- (a::'a::ring_1 fps) oo c = - (a oo c)"
    1.89 -  by (simp add: fps_eq_iff fps_compose_nth ring_simps setsum_negf[symmetric])
    1.90 -
    1.91 -lemma fps_compose_sub_distrib:
    1.92 -  shows "(a - b) oo (c::'a::ring_1 fps) = (a oo c) - (b oo c)"
    1.93 -  unfolding diff_minus fps_compose_uminus fps_compose_add_distrib ..
    1.94 -
    1.95 -lemma X_fps_compose:"X oo a = Abs_fps (\<lambda>n. if n = 0 then (0::'a::comm_ring_1) else a$n)"
    1.96 -  by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum_delta power_Suc)
    1.97  
    1.98  lemma X_compose_E[simp]: "X oo E (a::'a::{field}) = E a - 1"
    1.99    by (simp add: fps_eq_iff X_fps_compose)
   1.100 @@ -2301,6 +2366,7 @@
   1.101    unfolding inverse_one_plus_X
   1.102    by (simp add: L_def fps_eq_iff power_Suc del: of_nat_Suc)
   1.103  
   1.104 +
   1.105  lemma L_nth: "L $ n = (- 1) ^ Suc n / of_nat n"
   1.106    by (simp add: L_def)
   1.107