src/HOL/Library/Formal_Power_Series.thy
 changeset 32410 624bd2ea7c1e parent 31075 a9d6cf6de9a8 child 32411 63975b7f79b1
```     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Wed May 13 17:13:33 2009 +0100
1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Tue May 19 14:13:23 2009 +0100
1.3 @@ -2182,6 +2182,29 @@
1.4    show "?dia = inverse ?d" by simp
1.5  qed
1.6
1.7 +lemma fps_ginv_deriv:
1.8 +  assumes a0:"a\$0 = (0::'a::{field})" and a1: "a\$1 \<noteq> 0"
1.9 +  shows "fps_deriv (fps_ginv b a) = (fps_deriv b / fps_deriv a) oo fps_ginv X a"
1.10 +proof-
1.11 +  let ?ia = "fps_ginv b a"
1.12 +  let ?iXa = "fps_ginv X a"
1.13 +  let ?d = "fps_deriv"
1.14 +  let ?dia = "?d ?ia"
1.15 +  have iXa0: "?iXa \$ 0 = 0" by (simp add: fps_ginv_def)
1.16 +  have da0: "?d a \$ 0 \<noteq> 0" using a1 by simp
1.17 +  from fps_ginv[OF a0 a1, of b] have "?d (?ia oo a) = fps_deriv b" by simp
1.18 +  then have "(?d ?ia oo a) * ?d a = ?d b" unfolding fps_compose_deriv[OF a0] .
1.19 +  then have "(?d ?ia oo a) * ?d a * inverse (?d a) = ?d b * inverse (?d a)" by simp
1.20 +  then have "(?d ?ia oo a) * (inverse (?d a) * ?d a) = ?d b / ?d a"
1.21 +    by (simp add: fps_divide_def)
1.22 +  then have "(?d ?ia oo a) oo ?iXa =  (?d b / ?d a) oo ?iXa "
1.23 +    unfolding inverse_mult_eq_1[OF da0] by simp
1.24 +  then have "?d ?ia oo (a oo ?iXa) =  (?d b / ?d a) oo ?iXa"
1.25 +    unfolding fps_compose_assoc[OF iXa0 a0] .
1.26 +  then show ?thesis unfolding fps_inv_ginv[symmetric]
1.27 +    unfolding fps_inv_right[OF a0 a1] by simp
1.28 +qed
1.29 +
1.30  subsection{* Elementary series *}
1.31
1.32  subsubsection{* Exponential series *}
```