author | chaieb |

Tue May 19 14:13:23 2009 +0100 (2009-05-19) | |

changeset 32410 | 624bd2ea7c1e |

parent 31131 | d9752181691a |

child 32411 | 63975b7f79b1 |

Derivative of general reverses

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 *}