src/HOL/Library/Formal_Power_Series.thy
 changeset 29906 80369da39838 parent 29692 121289b1ae27 child 29911 c790a70a3d19
```     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Fri Feb 13 14:41:54 2009 -0800
1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Feb 13 14:45:10 2009 -0800
1.3 @@ -9,7 +9,7 @@
1.4    imports Main Fact Parity
1.5  begin
1.6
1.7 -section {* The type of formal power series*}
1.8 +subsection {* The type of formal power series*}
1.9
1.10  typedef 'a fps = "{f :: nat \<Rightarrow> 'a. True}"
1.11    by simp
1.12 @@ -94,7 +94,7 @@
1.13  lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
1.14    by auto
1.15
1.16 -section{* Formal power series form a commutative ring with unity, if the range of sequences
1.17 +subsection{* Formal power series form a commutative ring with unity, if the range of sequences
1.18    they represent is a commutative ring with unity*}
1.19
1.21 @@ -293,7 +293,7 @@
1.22  qed
1.23  end
1.24
1.25 -section {* Selection of the nth power of the implicit variable in the infinite sum*}
1.26 +subsection {* Selection of the nth power of the implicit variable in the infinite sum*}
1.27
1.28  definition fps_nth:: "'a fps \<Rightarrow> nat \<Rightarrow> 'a" (infixl "\$" 75)
1.29    where "f \$ n = Rep_fps f n"
1.30 @@ -358,7 +358,7 @@
1.31    ultimately show ?thesis by blast
1.32  qed
1.33
1.34 -section{* Injection of the basic ring elements and multiplication by scalars *}
1.35 +subsection{* Injection of the basic ring elements and multiplication by scalars *}
1.36
1.37  definition "fps_const c = Abs_fps (\<lambda>n. if n = 0 then c else 0)"
1.38  lemma fps_const_0_eq_0[simp]: "fps_const 0 = 0" by (simp add: fps_const_def fps_eq_iff)
1.39 @@ -391,7 +391,7 @@
1.40  lemma fps_mult_right_const_nth[simp]: "(f * fps_const (c::'a::semiring_1))\$n = f\$n * c"
1.41    by (simp add: fps_mult_nth fps_const_nth cond_application_beta cond_value_iff setsum_delta' cong del: if_weak_cong)
1.42
1.43 -section {* Formal power series form an integral domain*}
1.44 +subsection {* Formal power series form an integral domain*}
1.45
1.46  instantiation fps :: (ring_1) ring_1
1.47  begin
1.48 @@ -442,7 +442,7 @@
1.49  instance ..
1.50  end
1.51
1.52 -section{* Inverses of formal power series *}
1.53 +subsection{* Inverses of formal power series *}
1.54
1.55  declare setsum_cong[fundef_cong]
1.56
1.57 @@ -561,7 +561,7 @@
1.59  qed
1.60
1.61 -section{* Formal Derivatives, and the McLauren theorem around 0*}
1.62 +subsection{* Formal Derivatives, and the McLauren theorem around 0*}
1.63
1.64  definition "fps_deriv f = Abs_fps (\<lambda>n. of_nat (n + 1) * f \$ (n + 1))"
1.65
1.66 @@ -730,7 +730,7 @@
1.67  lemma fps_deriv_maclauren_0: "(fps_nth_deriv k (f:: ('a::comm_semiring_1) fps)) \$ 0 = of_nat (fact k) * f\$(k)"
1.68    by (induct k arbitrary: f) (auto simp add: ring_simps of_nat_mult)
1.69
1.70 -section {* Powers*}
1.71 +subsection {* Powers*}
1.72
1.73  instantiation fps :: (semiring_1) power
1.74  begin
1.75 @@ -945,7 +945,7 @@
1.76    using fps_inverse_deriv[OF a0]
1.77    by (simp add: fps_divide_def ring_simps power2_eq_square fps_inverse_mult inverse_mult_eq_1'[OF a0])
1.78
1.79 -section{* The eXtractor series X*}
1.80 +subsection{* The eXtractor series X*}
1.81
1.82  lemma minus_one_power_iff: "(- (1::'a :: {recpower, comm_ring_1})) ^ n = (if even n then 1 else - 1)"
1.83    by (induct n, auto)
1.84 @@ -1015,7 +1015,7 @@
1.85  qed
1.86
1.87
1.88 -section{* Integration *}
1.89 +subsection{* Integration *}
1.90  definition "fps_integral a a0 = Abs_fps (\<lambda>n. if n = 0 then a0 else (a\$(n - 1) / of_nat n))"
1.91
1.92  lemma fps_deriv_fps_integral: "fps_deriv (fps_integral a (a0 :: 'a :: {field, ring_char_0})) = a"
1.93 @@ -1029,7 +1029,7 @@
1.94      unfolding fps_deriv_eq_iff by auto
1.95  qed
1.96
1.97 -section {* Composition of FPSs *}
1.98 +subsection {* Composition of FPSs *}
1.99  definition fps_compose :: "('a::semiring_1) fps \<Rightarrow> 'a fps \<Rightarrow> 'a fps" (infixl "oo" 55) where
1.100    fps_compose_def: "a oo b = Abs_fps (\<lambda>n. setsum (\<lambda>i. a\$i * (b^i\$n)) {0..n})"
1.101
1.102 @@ -1051,9 +1051,9 @@
1.103    by simp_all
1.104
1.105
1.106 -section {* Rules from Herbert Wilf's Generatingfunctionology*}
1.107 +subsection {* Rules from Herbert Wilf's Generatingfunctionology*}
1.108
1.109 -subsection {* Rule 1 *}
1.110 +subsubsection {* Rule 1 *}
1.111    (* {a_{n+k}}_0^infty Corresponds to (f - setsum (\<lambda>i. a_i * x^i))/x^h, for h>0*)
1.112
1.113  lemma fps_power_mult_eq_shift:
1.114 @@ -1083,7 +1083,7 @@
1.115    then show ?thesis by (simp add: fps_eq_iff)
1.116  qed
1.117
1.118 -subsection{* Rule 2*}
1.119 +subsubsection{* Rule 2*}
1.120
1.121    (* We can not reach the form of Wilf, but still near to it using rewrite rules*)
1.122    (* If f reprents {a_n} and P is a polynomial, then
1.123 @@ -1108,8 +1108,8 @@
1.124  lemma fps_mult_XD_shift: "(XD ^k) (a:: ('a::{comm_ring_1, recpower, ring_char_0}) fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a\$n)"
1.125  by (induct k arbitrary: a) (simp_all add: power_Suc XD_def fps_eq_iff ring_simps del: One_nat_def)
1.126
1.127 -subsection{* Rule 3 is trivial and is given by @{text fps_times_def}*}
1.128 -subsection{* Rule 5 --- summation and "division" by (1 - X)*}
1.129 +subsubsection{* Rule 3 is trivial and is given by @{text fps_times_def}*}
1.130 +subsubsection{* Rule 5 --- summation and "division" by (1 - X)*}
1.131
1.132  lemma fps_divide_X_minus1_setsum_lemma:
1.133    "a = ((1::('a::comm_ring_1) fps) - X) * Abs_fps (\<lambda>n. setsum (\<lambda>i. a \$ i) {0..n})"
1.134 @@ -1157,7 +1157,7 @@
1.135    finally show ?thesis by (simp add: inverse_mult_eq_1[OF th0])
1.136  qed
1.137
1.138 -subsection{* Rule 4 in its more general form: generalizes Rule 3 for an arbitrary
1.139 +subsubsection{* Rule 4 in its more general form: generalizes Rule 3 for an arbitrary
1.140    finite product of FPS, also the relvant instance of powers of a FPS*}
1.141
1.142  definition "natpermute n k = {l:: nat list. length l = k \<and> foldl op + 0 l = n}"
1.143 @@ -1447,7 +1447,7 @@
1.144  qed
1.145
1.146
1.149
1.150  declare setprod_cong[fundef_cong]
1.151  function radical :: "(nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> ('a::{field, recpower}) fps \<Rightarrow> nat \<Rightarrow> 'a" where
1.152 @@ -1832,7 +1832,7 @@
1.153  ultimately show ?thesis by blast
1.154  qed
1.155
1.156 -section{* Derivative of composition *}
1.157 +subsection{* Derivative of composition *}
1.158
1.159  lemma fps_compose_deriv:
1.160    fixes a:: "('a::idom) fps"
1.161 @@ -1898,7 +1898,7 @@
1.162    ultimately show ?thesis by (cases n, auto)
1.163  qed
1.164
1.165 -section{* Finite FPS (i.e. polynomials) and X *}
1.166 +subsection{* Finite FPS (i.e. polynomials) and X *}
1.167  lemma fps_poly_sum_X:
1.168    assumes z: "\<forall>i > n. a\$i = (0::'a::comm_ring_1)"
1.169    shows "a = setsum (\<lambda>i. fps_const (a\$i) * X^i) {0..n}" (is "a = ?r")
1.170 @@ -1911,7 +1911,7 @@
1.171    then show ?thesis unfolding fps_eq_iff by blast
1.172  qed
1.173
1.174 -section{* Compositional inverses *}
1.175 +subsection{* Compositional inverses *}
1.176
1.177
1.178  fun compinv :: "'a fps \<Rightarrow> nat \<Rightarrow> 'a::{recpower,field}" where
1.179 @@ -2217,9 +2217,9 @@
1.180    show "?dia = inverse ?d" by simp
1.181  qed
1.182
1.183 -section{* Elementary series *}
1.184 +subsection{* Elementary series *}
1.185
1.186 -subsection{* Exponential series *}
1.187 +subsubsection{* Exponential series *}
1.188  definition "E x = Abs_fps (\<lambda>n. x^n / of_nat (fact n))"
1.189
1.190  lemma E_deriv[simp]: "fps_deriv (E a) = fps_const (a::'a::{field, recpower, ring_char_0}) * E a" (is "?l = ?r")
1.191 @@ -2332,7 +2332,7 @@
1.192  lemma E_power_mult: "(E (c::'a::{field,recpower,ring_char_0}))^n = E (of_nat n * c)"
1.194
1.195 -subsection{* Logarithmic series *}
1.196 +subsubsection{* Logarithmic series *}
1.197  definition "(L::'a::{field, ring_char_0,recpower} fps)
1.198    = Abs_fps (\<lambda>n. (- 1) ^ Suc n / of_nat n)"
1.199
1.200 @@ -2366,7 +2366,7 @@
1.201      by (simp add: L_nth fps_inv_def)
1.202  qed
1.203
1.204 -subsection{* Formal trigonometric functions  *}
1.205 +subsubsection{* Formal trigonometric functions  *}
1.206
1.207  definition "fps_sin (c::'a::{field, recpower, ring_char_0}) =
1.208    Abs_fps (\<lambda>n. if even n then 0 else (- 1) ^((n - 1) div 2) * c^n /(of_nat (fact n)))"
```