section -> subsection
authorhuffman
Fri Feb 13 14:45:10 2009 -0800 (2009-02-13)
changeset 2990680369da39838
parent 29905 26ee9656872a
child 29907 6b9eea61057c
section -> subsection
src/HOL/Library/Binomial.thy
src/HOL/Library/Euclidean_Space.thy
src/HOL/Library/Finite_Cartesian_Product.thy
src/HOL/Library/Formal_Power_Series.thy
     1.1 --- a/src/HOL/Library/Binomial.thy	Fri Feb 13 14:41:54 2009 -0800
     1.2 +++ b/src/HOL/Library/Binomial.thy	Fri Feb 13 14:45:10 2009 -0800
     1.3 @@ -182,7 +182,7 @@
     1.4    finally show ?case by simp
     1.5  qed
     1.6  
     1.7 -section{* Pochhammer's symbol : generalized raising factorial*}
     1.8 +subsection{* Pochhammer's symbol : generalized raising factorial*}
     1.9  
    1.10  definition "pochhammer (a::'a::comm_semiring_1) n = (if n = 0 then 1 else setprod (\<lambda>n. a + of_nat n) {0 .. n - 1})"
    1.11  
    1.12 @@ -285,7 +285,7 @@
    1.13      pochhammer_of_nat_eq_0_lemma'[of k n, where ?'a = 'a]
    1.14    by (auto simp add: not_le[symmetric])
    1.15  
    1.16 -section{* Generalized binomial coefficients *}
    1.17 +subsection{* Generalized binomial coefficients *}
    1.18  
    1.19  definition gbinomial :: "'a::{field, recpower,ring_char_0} \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
    1.20    where "a gchoose n = (if n = 0 then 1 else (setprod (\<lambda>i. a - of_nat i) {0 .. n - 1}) / of_nat (fact n))"
     2.1 --- a/src/HOL/Library/Euclidean_Space.thy	Fri Feb 13 14:41:54 2009 -0800
     2.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Fri Feb 13 14:45:10 2009 -0800
     2.3 @@ -40,7 +40,7 @@
     2.4  lemma setsum_3: "setsum f {1::nat..3} = f 1 + f 2 + f 3" 
     2.5    by (simp add: nat_number  atLeastAtMostSuc_conv add_commute)
     2.6  
     2.7 -section{* Basic componentwise operations on vectors. *}
     2.8 +subsection{* Basic componentwise operations on vectors. *}
     2.9  
    2.10  instantiation "^" :: (plus,type) plus
    2.11  begin
    2.12 @@ -106,7 +106,7 @@
    2.13  lemma dot_3[simp]: "(x::'a::{comm_monoid_add, times}^3) \<bullet> y = (x$1) * (y$1) + (x$2) * (y$2) + (x$3) * (y$3)"
    2.14    by (simp add: dot_def dimindex_def nat_number)
    2.15  
    2.16 -section {* A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space. *}
    2.17 +subsection {* A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space. *}
    2.18  
    2.19  lemmas Cart_lambda_beta' = Cart_lambda_beta[rule_format]
    2.20  method_setup vector = {*
     3.1 --- a/src/HOL/Library/Finite_Cartesian_Product.thy	Fri Feb 13 14:41:54 2009 -0800
     3.2 +++ b/src/HOL/Library/Finite_Cartesian_Product.thy	Fri Feb 13 14:45:10 2009 -0800
     3.3 @@ -33,7 +33,7 @@
     3.4  by (simp add: dimindex_def hassize_def)
     3.5  
     3.6  
     3.7 -section{* An indexing type parametrized by base type. *}
     3.8 +subsection{* An indexing type parametrized by base type. *}
     3.9  
    3.10  typedef 'a finite_image = "{1 .. DIM('a)}"
    3.11    using dimindex_ge_1 by auto
     4.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Fri Feb 13 14:41:54 2009 -0800
     4.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Feb 13 14:45:10 2009 -0800
     4.3 @@ -9,7 +9,7 @@
     4.4    imports Main Fact Parity
     4.5  begin
     4.6  
     4.7 -section {* The type of formal power series*}
     4.8 +subsection {* The type of formal power series*}
     4.9  
    4.10  typedef 'a fps = "{f :: nat \<Rightarrow> 'a. True}"
    4.11    by simp
    4.12 @@ -94,7 +94,7 @@
    4.13  lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
    4.14    by auto
    4.15  
    4.16 -section{* Formal power series form a commutative ring with unity, if the range of sequences 
    4.17 +subsection{* Formal power series form a commutative ring with unity, if the range of sequences 
    4.18    they represent is a commutative ring with unity*}
    4.19  
    4.20  instantiation fps :: (semigroup_add) semigroup_add
    4.21 @@ -293,7 +293,7 @@
    4.22  qed
    4.23  end
    4.24    
    4.25 -section {* Selection of the nth power of the implicit variable in the infinite sum*}
    4.26 +subsection {* Selection of the nth power of the implicit variable in the infinite sum*}
    4.27  
    4.28  definition fps_nth:: "'a fps \<Rightarrow> nat \<Rightarrow> 'a" (infixl "$" 75)
    4.29    where "f $ n = Rep_fps f n"
    4.30 @@ -358,7 +358,7 @@
    4.31    ultimately show ?thesis by blast
    4.32  qed
    4.33  
    4.34 -section{* Injection of the basic ring elements and multiplication by scalars *}
    4.35 +subsection{* Injection of the basic ring elements and multiplication by scalars *}
    4.36  
    4.37  definition "fps_const c = Abs_fps (\<lambda>n. if n = 0 then c else 0)"
    4.38  lemma fps_const_0_eq_0[simp]: "fps_const 0 = 0" by (simp add: fps_const_def fps_eq_iff)
    4.39 @@ -391,7 +391,7 @@
    4.40  lemma fps_mult_right_const_nth[simp]: "(f * fps_const (c::'a::semiring_1))$n = f$n * c"
    4.41    by (simp add: fps_mult_nth fps_const_nth cond_application_beta cond_value_iff setsum_delta' cong del: if_weak_cong)
    4.42  
    4.43 -section {* Formal power series form an integral domain*}
    4.44 +subsection {* Formal power series form an integral domain*}
    4.45  
    4.46  instantiation fps :: (ring_1) ring_1
    4.47  begin
    4.48 @@ -442,7 +442,7 @@
    4.49  instance ..
    4.50  end
    4.51  
    4.52 -section{* Inverses of formal power series *}
    4.53 +subsection{* Inverses of formal power series *}
    4.54  
    4.55  declare setsum_cong[fundef_cong]
    4.56  
    4.57 @@ -561,7 +561,7 @@
    4.58      by(simp add: setsum_delta)
    4.59  qed
    4.60  
    4.61 -section{* Formal Derivatives, and the McLauren theorem around 0*}
    4.62 +subsection{* Formal Derivatives, and the McLauren theorem around 0*}
    4.63  
    4.64  definition "fps_deriv f = Abs_fps (\<lambda>n. of_nat (n + 1) * f $ (n + 1))"
    4.65  
    4.66 @@ -730,7 +730,7 @@
    4.67  lemma fps_deriv_maclauren_0: "(fps_nth_deriv k (f:: ('a::comm_semiring_1) fps)) $ 0 = of_nat (fact k) * f$(k)"
    4.68    by (induct k arbitrary: f) (auto simp add: ring_simps of_nat_mult)
    4.69  
    4.70 -section {* Powers*}
    4.71 +subsection {* Powers*}
    4.72  
    4.73  instantiation fps :: (semiring_1) power
    4.74  begin
    4.75 @@ -945,7 +945,7 @@
    4.76    using fps_inverse_deriv[OF a0]
    4.77    by (simp add: fps_divide_def ring_simps power2_eq_square fps_inverse_mult inverse_mult_eq_1'[OF a0])
    4.78    
    4.79 -section{* The eXtractor series X*}
    4.80 +subsection{* The eXtractor series X*}
    4.81  
    4.82  lemma minus_one_power_iff: "(- (1::'a :: {recpower, comm_ring_1})) ^ n = (if even n then 1 else - 1)"
    4.83    by (induct n, auto)
    4.84 @@ -1015,7 +1015,7 @@
    4.85  qed
    4.86  
    4.87    
    4.88 -section{* Integration *}
    4.89 +subsection{* Integration *}
    4.90  definition "fps_integral a a0 = Abs_fps (\<lambda>n. if n = 0 then a0 else (a$(n - 1) / of_nat n))"
    4.91  
    4.92  lemma fps_deriv_fps_integral: "fps_deriv (fps_integral a (a0 :: 'a :: {field, ring_char_0})) = a"
    4.93 @@ -1029,7 +1029,7 @@
    4.94      unfolding fps_deriv_eq_iff by auto
    4.95  qed
    4.96    
    4.97 -section {* Composition of FPSs *}
    4.98 +subsection {* Composition of FPSs *}
    4.99  definition fps_compose :: "('a::semiring_1) fps \<Rightarrow> 'a fps \<Rightarrow> 'a fps" (infixl "oo" 55) where
   4.100    fps_compose_def: "a oo b = Abs_fps (\<lambda>n. setsum (\<lambda>i. a$i * (b^i$n)) {0..n})"
   4.101  
   4.102 @@ -1051,9 +1051,9 @@
   4.103    by simp_all
   4.104  
   4.105  
   4.106 -section {* Rules from Herbert Wilf's Generatingfunctionology*}
   4.107 +subsection {* Rules from Herbert Wilf's Generatingfunctionology*}
   4.108  
   4.109 -subsection {* Rule 1 *}
   4.110 +subsubsection {* Rule 1 *}
   4.111    (* {a_{n+k}}_0^infty Corresponds to (f - setsum (\<lambda>i. a_i * x^i))/x^h, for h>0*)
   4.112  
   4.113  lemma fps_power_mult_eq_shift: 
   4.114 @@ -1083,7 +1083,7 @@
   4.115    then show ?thesis by (simp add: fps_eq_iff)
   4.116  qed
   4.117  
   4.118 -subsection{* Rule 2*}
   4.119 +subsubsection{* Rule 2*}
   4.120  
   4.121    (* We can not reach the form of Wilf, but still near to it using rewrite rules*)
   4.122    (* If f reprents {a_n} and P is a polynomial, then 
   4.123 @@ -1108,8 +1108,8 @@
   4.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)"
   4.125  by (induct k arbitrary: a) (simp_all add: power_Suc XD_def fps_eq_iff ring_simps del: One_nat_def)
   4.126  
   4.127 -subsection{* Rule 3 is trivial and is given by @{text fps_times_def}*}
   4.128 -subsection{* Rule 5 --- summation and "division" by (1 - X)*}
   4.129 +subsubsection{* Rule 3 is trivial and is given by @{text fps_times_def}*}
   4.130 +subsubsection{* Rule 5 --- summation and "division" by (1 - X)*}
   4.131  
   4.132  lemma fps_divide_X_minus1_setsum_lemma:
   4.133    "a = ((1::('a::comm_ring_1) fps) - X) * Abs_fps (\<lambda>n. setsum (\<lambda>i. a $ i) {0..n})"
   4.134 @@ -1157,7 +1157,7 @@
   4.135    finally show ?thesis by (simp add: inverse_mult_eq_1[OF th0])
   4.136  qed
   4.137  
   4.138 -subsection{* Rule 4 in its more general form: generalizes Rule 3 for an arbitrary 
   4.139 +subsubsection{* Rule 4 in its more general form: generalizes Rule 3 for an arbitrary 
   4.140    finite product of FPS, also the relvant instance of powers of a FPS*}
   4.141  
   4.142  definition "natpermute n k = {l:: nat list. length l = k \<and> foldl op + 0 l = n}"
   4.143 @@ -1447,7 +1447,7 @@
   4.144  qed
   4.145  
   4.146  
   4.147 -section {* Radicals *}
   4.148 +subsection {* Radicals *}
   4.149  
   4.150  declare setprod_cong[fundef_cong]
   4.151  function radical :: "(nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> ('a::{field, recpower}) fps \<Rightarrow> nat \<Rightarrow> 'a" where
   4.152 @@ -1832,7 +1832,7 @@
   4.153  ultimately show ?thesis by blast
   4.154  qed
   4.155  
   4.156 -section{* Derivative of composition *}
   4.157 +subsection{* Derivative of composition *}
   4.158  
   4.159  lemma fps_compose_deriv: 
   4.160    fixes a:: "('a::idom) fps"
   4.161 @@ -1898,7 +1898,7 @@
   4.162    ultimately show ?thesis by (cases n, auto)
   4.163  qed
   4.164  
   4.165 -section{* Finite FPS (i.e. polynomials) and X *}
   4.166 +subsection{* Finite FPS (i.e. polynomials) and X *}
   4.167  lemma fps_poly_sum_X:
   4.168    assumes z: "\<forall>i > n. a$i = (0::'a::comm_ring_1)" 
   4.169    shows "a = setsum (\<lambda>i. fps_const (a$i) * X^i) {0..n}" (is "a = ?r")
   4.170 @@ -1911,7 +1911,7 @@
   4.171    then show ?thesis unfolding fps_eq_iff by blast
   4.172  qed
   4.173  
   4.174 -section{* Compositional inverses *}
   4.175 +subsection{* Compositional inverses *}
   4.176  
   4.177  
   4.178  fun compinv :: "'a fps \<Rightarrow> nat \<Rightarrow> 'a::{recpower,field}" where
   4.179 @@ -2217,9 +2217,9 @@
   4.180    show "?dia = inverse ?d" by simp
   4.181  qed
   4.182  
   4.183 -section{* Elementary series *}
   4.184 +subsection{* Elementary series *}
   4.185  
   4.186 -subsection{* Exponential series *}
   4.187 +subsubsection{* Exponential series *}
   4.188  definition "E x = Abs_fps (\<lambda>n. x^n / of_nat (fact n))"   
   4.189  
   4.190  lemma E_deriv[simp]: "fps_deriv (E a) = fps_const (a::'a::{field, recpower, ring_char_0}) * E a" (is "?l = ?r")
   4.191 @@ -2332,7 +2332,7 @@
   4.192  lemma E_power_mult: "(E (c::'a::{field,recpower,ring_char_0}))^n = E (of_nat n * c)"
   4.193    by (induct n, auto simp add: ring_simps E_add_mult power_Suc)
   4.194  
   4.195 -subsection{* Logarithmic series *}  
   4.196 +subsubsection{* Logarithmic series *}  
   4.197  definition "(L::'a::{field, ring_char_0,recpower} fps) 
   4.198    = Abs_fps (\<lambda>n. (- 1) ^ Suc n / of_nat n)"
   4.199  
   4.200 @@ -2366,7 +2366,7 @@
   4.201      by (simp add: L_nth fps_inv_def)
   4.202  qed
   4.203  
   4.204 -subsection{* Formal trigonometric functions  *}
   4.205 +subsubsection{* Formal trigonometric functions  *}
   4.206  
   4.207  definition "fps_sin (c::'a::{field, recpower, ring_char_0}) = 
   4.208    Abs_fps (\<lambda>n. if even n then 0 else (- 1) ^((n - 1) div 2) * c^n /(of_nat (fact n)))"