2100 then have ?thesis |
2100 then have ?thesis |
2101 by (simp add: fps_compose_setprod_distrib[OF c0])} |
2101 by (simp add: fps_compose_setprod_distrib[OF c0])} |
2102 ultimately show ?thesis by (cases n, auto) |
2102 ultimately show ?thesis by (cases n, auto) |
2103 qed |
2103 qed |
2104 |
2104 |
|
2105 lemma fps_compose_uminus: "- (a::'a::ring_1 fps) oo c = - (a oo c)" |
|
2106 by (simp add: fps_eq_iff fps_compose_nth ring_simps setsum_negf[symmetric]) |
|
2107 |
|
2108 lemma fps_compose_sub_distrib: |
|
2109 shows "(a - b) oo (c::'a::ring_1 fps) = (a oo c) - (b oo c)" |
|
2110 unfolding diff_minus fps_compose_uminus fps_compose_add_distrib .. |
|
2111 |
|
2112 lemma X_fps_compose:"X oo a = Abs_fps (\<lambda>n. if n = 0 then (0::'a::comm_ring_1) else a$n)" |
|
2113 by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum_delta power_Suc) |
|
2114 |
|
2115 lemma fps_inverse_compose: |
|
2116 assumes b0: "(b$0 :: 'a::field) = 0" and a0: "a$0 \<noteq> 0" |
|
2117 shows "inverse a oo b = inverse (a oo b)" |
|
2118 proof- |
|
2119 let ?ia = "inverse a" |
|
2120 let ?ab = "a oo b" |
|
2121 let ?iab = "inverse ?ab" |
|
2122 |
|
2123 from a0 have ia0: "?ia $ 0 \<noteq> 0" by (simp ) |
|
2124 from a0 have ab0: "?ab $ 0 \<noteq> 0" by (simp add: fps_compose_def) |
|
2125 thm inverse_mult_eq_1[OF ab0] |
|
2126 have "(?ia oo b) * (a oo b) = 1" |
|
2127 unfolding fps_compose_mult_distrib[OF b0, symmetric] |
|
2128 unfolding inverse_mult_eq_1[OF a0] |
|
2129 fps_compose_1 .. |
|
2130 |
|
2131 then have "(?ia oo b) * (a oo b) * ?iab = 1 * ?iab" by simp |
|
2132 then have "(?ia oo b) * (?iab * (a oo b)) = ?iab" by simp |
|
2133 then show ?thesis |
|
2134 unfolding inverse_mult_eq_1[OF ab0] by simp |
|
2135 qed |
|
2136 |
|
2137 lemma fps_divide_compose: |
|
2138 assumes c0: "(c$0 :: 'a::field) = 0" and b0: "b$0 \<noteq> 0" |
|
2139 shows "(a/b) oo c = (a oo c) / (b oo c)" |
|
2140 unfolding fps_divide_def fps_compose_mult_distrib[OF c0] |
|
2141 fps_inverse_compose[OF c0 b0] .. |
|
2142 |
|
2143 lemma gp: assumes a0: "a$0 = (0::'a::field)" |
|
2144 shows "(Abs_fps (\<lambda>n. 1)) oo a = 1/(1 - a)" (is "?one oo a = _") |
|
2145 proof- |
|
2146 have o0: "?one $ 0 \<noteq> 0" by simp |
|
2147 have th0: "(1 - X) $ 0 \<noteq> (0::'a)" by simp |
|
2148 from fps_inverse_gp[where ?'a = 'a] |
|
2149 have "inverse ?one = 1 - X" by (simp add: fps_eq_iff) |
|
2150 hence "inverse (inverse ?one) = inverse (1 - X)" by simp |
|
2151 hence th: "?one = 1/(1 - X)" unfolding fps_inverse_idempotent[OF o0] |
|
2152 by (simp add: fps_divide_def) |
|
2153 show ?thesis unfolding th |
|
2154 unfolding fps_divide_compose[OF a0 th0] |
|
2155 fps_compose_1 fps_compose_sub_distrib X_fps_compose_startby0[OF a0] .. |
|
2156 qed |
|
2157 |
|
2158 lemma fps_const_power[simp]: "fps_const (c::'a::ring_1) ^ n = fps_const (c^n)" |
|
2159 by (induct n, auto) |
|
2160 |
|
2161 lemma fps_compose_radical: |
|
2162 assumes b0: "b$0 = (0::'a::{field, ring_char_0})" |
|
2163 and ra0: "r (Suc k) (a$0) ^ Suc k = a$0" |
|
2164 and a0: "a$0 \<noteq> 0" |
|
2165 shows "fps_radical r (Suc k) a oo b = fps_radical r (Suc k) (a oo b)" |
|
2166 proof- |
|
2167 let ?r = "fps_radical r (Suc k)" |
|
2168 let ?ab = "a oo b" |
|
2169 have ab0: "?ab $ 0 = a$0" by (simp add: fps_compose_def) |
|
2170 from ab0 a0 ra0 have rab0: "?ab $ 0 \<noteq> 0" "r (Suc k) (?ab $ 0) ^ Suc k = ?ab $ 0" by simp_all |
|
2171 have th00: "r (Suc k) ((a oo b) $ 0) = (fps_radical r (Suc k) a oo b) $ 0" |
|
2172 by (simp add: ab0 fps_compose_def) |
|
2173 have th0: "(?r a oo b) ^ (Suc k) = a oo b" |
|
2174 unfolding fps_compose_power[OF b0] |
|
2175 unfolding iffD1[OF power_radical[of a r k], OF a0 ra0] .. |
|
2176 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 . |
|
2177 qed |
|
2178 |
2105 lemma fps_const_mult_apply_left: |
2179 lemma fps_const_mult_apply_left: |
2106 "fps_const c * (a oo b) = (fps_const c * a) oo b" |
2180 "fps_const c * (a oo b) = (fps_const c * a) oo b" |
2107 by (simp add: fps_eq_iff fps_compose_nth setsum_right_distrib mult_assoc) |
2181 by (simp add: fps_eq_iff fps_compose_nth setsum_right_distrib mult_assoc) |
2108 |
2182 |
2109 lemma fps_const_mult_apply_right: |
2183 lemma fps_const_mult_apply_right: |
2247 qed |
2321 qed |
2248 |
2322 |
2249 lemma E_nth_deriv[simp]: "fps_nth_deriv n (E (a::'a::{field, ring_char_0})) = (fps_const a)^n * (E a)" |
2323 lemma E_nth_deriv[simp]: "fps_nth_deriv n (E (a::'a::{field, ring_char_0})) = (fps_const a)^n * (E a)" |
2250 by (induct n, auto simp add: power_Suc) |
2324 by (induct n, auto simp add: power_Suc) |
2251 |
2325 |
2252 lemma fps_compose_uminus: "- (a::'a::ring_1 fps) oo c = - (a oo c)" |
|
2253 by (simp add: fps_eq_iff fps_compose_nth ring_simps setsum_negf[symmetric]) |
|
2254 |
|
2255 lemma fps_compose_sub_distrib: |
|
2256 shows "(a - b) oo (c::'a::ring_1 fps) = (a oo c) - (b oo c)" |
|
2257 unfolding diff_minus fps_compose_uminus fps_compose_add_distrib .. |
|
2258 |
|
2259 lemma X_fps_compose:"X oo a = Abs_fps (\<lambda>n. if n = 0 then (0::'a::comm_ring_1) else a$n)" |
|
2260 by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum_delta power_Suc) |
|
2261 |
2326 |
2262 lemma X_compose_E[simp]: "X oo E (a::'a::{field}) = E a - 1" |
2327 lemma X_compose_E[simp]: "X oo E (a::'a::{field}) = E a - 1" |
2263 by (simp add: fps_eq_iff X_fps_compose) |
2328 by (simp add: fps_eq_iff X_fps_compose) |
2264 |
2329 |
2265 lemma LE_compose: |
2330 lemma LE_compose: |