2499 then have "?r b (?r c a) oo c oo fps_inv c= b oo a oo fps_inv c" by simp |
2499 then have "?r b (?r c a) oo c oo fps_inv c= b oo a oo fps_inv c" by simp |
2500 then have "?r b (?r c a) oo (c oo fps_inv c) = b oo a oo fps_inv c" |
2500 then have "?r b (?r c a) oo (c oo fps_inv c) = b oo a oo fps_inv c" |
2501 apply (subst fps_compose_assoc) |
2501 apply (subst fps_compose_assoc) |
2502 using a0 c0 by (auto simp add: fps_inv_def) |
2502 using a0 c0 by (auto simp add: fps_inv_def) |
2503 then show ?thesis unfolding fps_inv_right[OF c0 c1] by simp |
2503 then show ?thesis unfolding fps_inv_right[OF c0 c1] by simp |
|
2504 qed |
|
2505 |
|
2506 lemma fps_ginv_deriv: |
|
2507 assumes a0:"a$0 = (0::'a::{field})" and a1: "a$1 \<noteq> 0" |
|
2508 shows "fps_deriv (fps_ginv b a) = (fps_deriv b / fps_deriv a) oo fps_ginv X a" |
|
2509 proof- |
|
2510 let ?ia = "fps_ginv b a" |
|
2511 let ?iXa = "fps_ginv X a" |
|
2512 let ?d = "fps_deriv" |
|
2513 let ?dia = "?d ?ia" |
|
2514 have iXa0: "?iXa $ 0 = 0" by (simp add: fps_ginv_def) |
|
2515 have da0: "?d a $ 0 \<noteq> 0" using a1 by simp |
|
2516 from fps_ginv[OF a0 a1, of b] have "?d (?ia oo a) = fps_deriv b" by simp |
|
2517 then have "(?d ?ia oo a) * ?d a = ?d b" unfolding fps_compose_deriv[OF a0] . |
|
2518 then have "(?d ?ia oo a) * ?d a * inverse (?d a) = ?d b * inverse (?d a)" by simp |
|
2519 then have "(?d ?ia oo a) * (inverse (?d a) * ?d a) = ?d b / ?d a" |
|
2520 by (simp add: fps_divide_def) |
|
2521 then have "(?d ?ia oo a) oo ?iXa = (?d b / ?d a) oo ?iXa " |
|
2522 unfolding inverse_mult_eq_1[OF da0] by simp |
|
2523 then have "?d ?ia oo (a oo ?iXa) = (?d b / ?d a) oo ?iXa" |
|
2524 unfolding fps_compose_assoc[OF iXa0 a0] . |
|
2525 then show ?thesis unfolding fps_inv_ginv[symmetric] |
|
2526 unfolding fps_inv_right[OF a0 a1] by simp |
2504 qed |
2527 qed |
2505 |
2528 |
2506 subsection{* Elementary series *} |
2529 subsection{* Elementary series *} |
2507 |
2530 |
2508 subsubsection{* Exponential series *} |
2531 subsubsection{* Exponential series *} |