# HG changeset patch
# User chaieb
# Date 1251304682 -3600
# Node ID b3241e8e971672fc6332c398824f9ccae1b05d7d
# Parent  8d1263a00392f26cc0c1028b4ac3e3dd0d8d12e3# Parent  63975b7f79b1c5cab845c929cc46da011f6cdb17
merged

diff -r 8d1263a00392 -r b3241e8e9716 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Wed Aug 26 17:34:32 2009 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Wed Aug 26 17:38:02 2009 +0100
@@ -2503,6 +2503,29 @@
   then show ?thesis unfolding fps_inv_right[OF c0 c1] by simp
 qed
 
+lemma fps_ginv_deriv:
+  assumes a0:"a$0 = (0::'a::{field})" and a1: "a$1 \<noteq> 0"
+  shows "fps_deriv (fps_ginv b a) = (fps_deriv b / fps_deriv a) oo fps_ginv X a"
+proof-
+  let ?ia = "fps_ginv b a"
+  let ?iXa = "fps_ginv X a"
+  let ?d = "fps_deriv"
+  let ?dia = "?d ?ia"
+  have iXa0: "?iXa $ 0 = 0" by (simp add: fps_ginv_def)
+  have da0: "?d a $ 0 \<noteq> 0" using a1 by simp
+  from fps_ginv[OF a0 a1, of b] have "?d (?ia oo a) = fps_deriv b" by simp
+  then have "(?d ?ia oo a) * ?d a = ?d b" unfolding fps_compose_deriv[OF a0] .
+  then have "(?d ?ia oo a) * ?d a * inverse (?d a) = ?d b * inverse (?d a)" by simp
+  then have "(?d ?ia oo a) * (inverse (?d a) * ?d a) = ?d b / ?d a" 
+    by (simp add: fps_divide_def)
+  then have "(?d ?ia oo a) oo ?iXa =  (?d b / ?d a) oo ?iXa "
+    unfolding inverse_mult_eq_1[OF da0] by simp
+  then have "?d ?ia oo (a oo ?iXa) =  (?d b / ?d a) oo ?iXa"
+    unfolding fps_compose_assoc[OF iXa0 a0] .
+  then show ?thesis unfolding fps_inv_ginv[symmetric]
+    unfolding fps_inv_right[OF a0 a1] by simp
+qed
+
 subsection{* Elementary series *}
 
 subsubsection{* Exponential series *}