author chaieb Wed Aug 26 17:38:18 2009 +0100 (2009-08-26) changeset 32414 62a7aea5f50c parent 32409 7e38dedf3f7d parent 32413 b3241e8e9716 child 32416 4ea7648b6ae2
merged
```     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Wed Aug 26 16:41:37 2009 +0200
1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Wed Aug 26 17:38:18 2009 +0100
1.3 @@ -3926,14 +3926,6 @@
1.4    shows "finite s \<and> card s \<le> card t"
1.5    by (metis exchange_lemma[OF f i sp] hassize_def finite_subset card_mono)
1.6
1.7 -lemma finite_Atleast_Atmost[simp]: "finite {f x |x. x\<in> {(i::'a::finite_intvl_succ) .. j}}"
1.8 -proof-
1.9 -  have eq: "{f x |x. x\<in> {i .. j}} = f ` {i .. j}" by auto
1.10 -  show ?thesis unfolding eq
1.11 -    apply (rule finite_imageI)
1.12 -    apply (rule finite_intvl)
1.13 -    done
1.14 -qed
1.15
1.16  lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x\<in> (UNIV::'a::finite set)}"
1.17  proof-
```
```     2.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Wed Aug 26 16:41:37 2009 +0200
2.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Wed Aug 26 17:38:18 2009 +0100
2.3 @@ -2503,6 +2503,29 @@
2.4    then show ?thesis unfolding fps_inv_right[OF c0 c1] by simp
2.5  qed
2.6
2.7 +lemma fps_ginv_deriv:
2.8 +  assumes a0:"a\$0 = (0::'a::{field})" and a1: "a\$1 \<noteq> 0"
2.9 +  shows "fps_deriv (fps_ginv b a) = (fps_deriv b / fps_deriv a) oo fps_ginv X a"
2.10 +proof-
2.11 +  let ?ia = "fps_ginv b a"
2.12 +  let ?iXa = "fps_ginv X a"
2.13 +  let ?d = "fps_deriv"
2.14 +  let ?dia = "?d ?ia"
2.15 +  have iXa0: "?iXa \$ 0 = 0" by (simp add: fps_ginv_def)
2.16 +  have da0: "?d a \$ 0 \<noteq> 0" using a1 by simp
2.17 +  from fps_ginv[OF a0 a1, of b] have "?d (?ia oo a) = fps_deriv b" by simp
2.18 +  then have "(?d ?ia oo a) * ?d a = ?d b" unfolding fps_compose_deriv[OF a0] .
2.19 +  then have "(?d ?ia oo a) * ?d a * inverse (?d a) = ?d b * inverse (?d a)" by simp
2.20 +  then have "(?d ?ia oo a) * (inverse (?d a) * ?d a) = ?d b / ?d a"
2.21 +    by (simp add: fps_divide_def)
2.22 +  then have "(?d ?ia oo a) oo ?iXa =  (?d b / ?d a) oo ?iXa "
2.23 +    unfolding inverse_mult_eq_1[OF da0] by simp
2.24 +  then have "?d ?ia oo (a oo ?iXa) =  (?d b / ?d a) oo ?iXa"
2.25 +    unfolding fps_compose_assoc[OF iXa0 a0] .
2.26 +  then show ?thesis unfolding fps_inv_ginv[symmetric]
2.27 +    unfolding fps_inv_right[OF a0 a1] by simp
2.28 +qed
2.29 +
2.30  subsection{* Elementary series *}
2.31
2.32  subsubsection{* Exponential series *}
```