2253 hence "inverse ?d * ?d * ?dia = inverse ?d * 1" by simp |
2253 hence "inverse ?d * ?d * ?dia = inverse ?d * 1" by simp |
2254 with inverse_mult_eq_1[OF th0] |
2254 with inverse_mult_eq_1[OF th0] |
2255 show "?dia = inverse ?d" by simp |
2255 show "?dia = inverse ?d" by simp |
2256 qed |
2256 qed |
2257 |
2257 |
|
2258 lemma fps_ginv_deriv: |
|
2259 assumes a0:"a$0 = (0::'a::{field})" and a1: "a$1 \<noteq> 0" |
|
2260 shows "fps_deriv (fps_ginv b a) = (fps_deriv b / fps_deriv a) oo fps_ginv X a" |
|
2261 proof- |
|
2262 let ?ia = "fps_ginv b a" |
|
2263 let ?iXa = "fps_ginv X a" |
|
2264 let ?d = "fps_deriv" |
|
2265 let ?dia = "?d ?ia" |
|
2266 have iXa0: "?iXa $ 0 = 0" by (simp add: fps_ginv_def) |
|
2267 have da0: "?d a $ 0 \<noteq> 0" using a1 by simp |
|
2268 from fps_ginv[OF a0 a1, of b] have "?d (?ia oo a) = fps_deriv b" by simp |
|
2269 then have "(?d ?ia oo a) * ?d a = ?d b" unfolding fps_compose_deriv[OF a0] . |
|
2270 then have "(?d ?ia oo a) * ?d a * inverse (?d a) = ?d b * inverse (?d a)" by simp |
|
2271 then have "(?d ?ia oo a) * (inverse (?d a) * ?d a) = ?d b / ?d a" |
|
2272 by (simp add: fps_divide_def) |
|
2273 then have "(?d ?ia oo a) oo ?iXa = (?d b / ?d a) oo ?iXa " |
|
2274 unfolding inverse_mult_eq_1[OF da0] by simp |
|
2275 then have "?d ?ia oo (a oo ?iXa) = (?d b / ?d a) oo ?iXa" |
|
2276 unfolding fps_compose_assoc[OF iXa0 a0] . |
|
2277 then show ?thesis unfolding fps_inv_ginv[symmetric] |
|
2278 unfolding fps_inv_right[OF a0 a1] by simp |
|
2279 qed |
|
2280 |
2258 subsection{* Elementary series *} |
2281 subsection{* Elementary series *} |
2259 |
2282 |
2260 subsubsection{* Exponential series *} |
2283 subsubsection{* Exponential series *} |
2261 definition "E x = Abs_fps (\<lambda>n. x^n / of_nat (fact n))" |
2284 definition "E x = Abs_fps (\<lambda>n. x^n / of_nat (fact n))" |
2262 |
2285 |