--- a/src/HOL/Library/Euclidean_Space.thy Wed Aug 26 16:41:37 2009 +0200
+++ b/src/HOL/Library/Euclidean_Space.thy Wed Aug 26 17:38:18 2009 +0100
@@ -3926,14 +3926,6 @@
shows "finite s \<and> card s \<le> card t"
by (metis exchange_lemma[OF f i sp] hassize_def finite_subset card_mono)
-lemma finite_Atleast_Atmost[simp]: "finite {f x |x. x\<in> {(i::'a::finite_intvl_succ) .. j}}"
-proof-
- have eq: "{f x |x. x\<in> {i .. j}} = f ` {i .. j}" by auto
- show ?thesis unfolding eq
- apply (rule finite_imageI)
- apply (rule finite_intvl)
- done
-qed
lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x\<in> (UNIV::'a::finite set)}"
proof-
--- a/src/HOL/Library/Formal_Power_Series.thy Wed Aug 26 16:41:37 2009 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Wed Aug 26 17:38:18 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 *}