use class field_char_0 for fps definitions
authorhuffman
Thu May 28 00:47:17 2009 -0700 (2009-05-28)
changeset 31273da95bc889ad2
parent 31272 703183ff0926
child 31274 d2b5c6b07988
use class field_char_0 for fps definitions
src/HOL/Library/Formal_Power_Series.thy
     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Wed May 27 21:46:50 2009 -0700
     1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Thu May 28 00:47:17 2009 -0700
     1.3 @@ -5,7 +5,7 @@
     1.4  header{* A formalization of formal power series *}
     1.5  
     1.6  theory Formal_Power_Series
     1.7 -imports Main Fact Parity
     1.8 +imports Main Fact Parity Rational
     1.9  begin
    1.10  
    1.11  subsection {* The type of formal power series*}
    1.12 @@ -392,8 +392,8 @@
    1.13  begin
    1.14  definition number_of_fps_def: "(number_of k::'a fps) = of_int k"
    1.15  
    1.16 -instance 
    1.17 -by (intro_classes, rule number_of_fps_def)
    1.18 +instance proof
    1.19 +qed (rule number_of_fps_def)
    1.20  end
    1.21  
    1.22  subsection{* Inverses of formal power series *}
    1.23 @@ -923,12 +923,19 @@
    1.24  
    1.25  
    1.26  subsection{* Integration *}
    1.27 -definition "fps_integral a a0 = Abs_fps (\<lambda>n. if n = 0 then a0 else (a$(n - 1) / of_nat n))"
    1.28 +
    1.29 +definition
    1.30 +  fps_integral :: "'a::field_char_0 fps \<Rightarrow> 'a \<Rightarrow> 'a fps" where
    1.31 +  "fps_integral a a0 = Abs_fps (\<lambda>n. if n = 0 then a0 else (a$(n - 1) / of_nat n))"
    1.32  
    1.33 -lemma fps_deriv_fps_integral: "fps_deriv (fps_integral a (a0 :: 'a :: {field, ring_char_0})) = a"
    1.34 -  by (simp add: fps_integral_def fps_deriv_def fps_eq_iff field_simps del: of_nat_Suc)
    1.35 +lemma fps_deriv_fps_integral: "fps_deriv (fps_integral a a0) = a"
    1.36 +  unfolding fps_integral_def fps_deriv_def
    1.37 +  by (simp add: fps_eq_iff del: of_nat_Suc)
    1.38  
    1.39 -lemma fps_integral_linear: "fps_integral (fps_const (a::'a::{field, ring_char_0}) * f + fps_const b * g) (a*a0 + b*b0) = fps_const a * fps_integral f a0 + fps_const b * fps_integral g b0" (is "?l = ?r")
    1.40 +lemma fps_integral_linear:
    1.41 +  "fps_integral (fps_const a * f + fps_const b * g) (a*a0 + b*b0) =
    1.42 +    fps_const a * fps_integral f a0 + fps_const b * fps_integral g b0"
    1.43 +  (is "?l = ?r")
    1.44  proof-
    1.45    have "fps_deriv ?l = fps_deriv ?r" by (simp add: fps_deriv_fps_integral)
    1.46    moreover have "?l$0 = ?r$0" by (simp add: fps_integral_def)
    1.47 @@ -1438,7 +1445,7 @@
    1.48  qed
    1.49  
    1.50  lemma power_radical:
    1.51 -  fixes a:: "'a ::{field, ring_char_0} fps"
    1.52 +  fixes a:: "'a::field_char_0 fps"
    1.53    assumes a0: "a$0 \<noteq> 0"
    1.54    shows "(r (Suc k) (a$0)) ^ Suc k = a$0 \<longleftrightarrow> (fps_radical r (Suc k) a) ^ (Suc k) = a"
    1.55  proof-
    1.56 @@ -1499,7 +1506,7 @@
    1.57  
    1.58  (*
    1.59  lemma power_radical:
    1.60 -  fixes a:: "'a ::{field, ring_char_0} fps"
    1.61 +  fixes a:: "'a::field_char_0 fps"
    1.62    assumes r0: "(r (Suc k) (a$0)) ^ Suc k = a$0" and a0: "a$0 \<noteq> 0"
    1.63    shows "(fps_radical r (Suc k) a) ^ (Suc k) = a"
    1.64  proof-
    1.65 @@ -1561,7 +1568,7 @@
    1.66  
    1.67  lemma radical_unique:
    1.68    assumes r0: "(r (Suc k) (b$0)) ^ Suc k = b$0"
    1.69 -  and a0: "r (Suc k) (b$0 ::'a::{field, ring_char_0}) = a$0" and b0: "b$0 \<noteq> 0"
    1.70 +  and a0: "r (Suc k) (b$0 ::'a::field_char_0) = a$0" and b0: "b$0 \<noteq> 0"
    1.71    shows "a^(Suc k) = b \<longleftrightarrow> a = fps_radical r (Suc k) b"
    1.72  proof-
    1.73    let ?r = "fps_radical r (Suc k) b"
    1.74 @@ -1655,7 +1662,7 @@
    1.75  
    1.76  lemma radical_power:
    1.77    assumes r0: "r (Suc k) ((a$0) ^ Suc k) = a$0"
    1.78 -  and a0: "(a$0 ::'a::{field, ring_char_0}) \<noteq> 0"
    1.79 +  and a0: "(a$0 ::'a::field_char_0) \<noteq> 0"
    1.80    shows "(fps_radical r (Suc k) (a ^ Suc k)) = a"
    1.81  proof-
    1.82    let ?ak = "a^ Suc k"
    1.83 @@ -1667,7 +1674,7 @@
    1.84  qed
    1.85  
    1.86  lemma fps_deriv_radical:
    1.87 -  fixes a:: "'a ::{field, ring_char_0} fps"
    1.88 +  fixes a:: "'a::field_char_0 fps"
    1.89    assumes r0: "(r (Suc k) (a$0)) ^ Suc k = a$0" and a0: "a$0 \<noteq> 0"
    1.90    shows "fps_deriv (fps_radical r (Suc k) a) = fps_deriv a / (fps_const (of_nat (Suc k)) * (fps_radical r (Suc k) a) ^ k)"
    1.91  proof-
    1.92 @@ -1688,7 +1695,7 @@
    1.93  qed
    1.94  
    1.95  lemma radical_mult_distrib:
    1.96 -  fixes a:: "'a ::{field, ring_char_0} fps"
    1.97 +  fixes a:: "'a::field_char_0 fps"
    1.98    assumes
    1.99    k: "k > 0"
   1.100    and ra0: "r k (a $ 0) ^ k = a $ 0"
   1.101 @@ -1722,7 +1729,7 @@
   1.102  
   1.103  (*
   1.104  lemma radical_mult_distrib:
   1.105 -  fixes a:: "'a ::{field, ring_char_0} fps"
   1.106 +  fixes a:: "'a::field_char_0 fps"
   1.107    assumes
   1.108    ra0: "r k (a $ 0) ^ k = a $ 0"
   1.109    and rb0: "r k (b $ 0) ^ k = b $ 0"
   1.110 @@ -1752,7 +1759,7 @@
   1.111    by (simp add: fps_divide_def)
   1.112  
   1.113  lemma radical_divide:
   1.114 -  fixes a:: "'a ::{field, ring_char_0} fps"
   1.115 +  fixes a :: "'a::field_char_0 fps"
   1.116    assumes
   1.117    kp: "k>0"
   1.118    and ra0: "(r k (a $ 0)) ^ k = a $ 0"
   1.119 @@ -1790,7 +1797,7 @@
   1.120  qed
   1.121  
   1.122  lemma radical_inverse:
   1.123 -  fixes a:: "'a ::{field, ring_char_0} fps"
   1.124 +  fixes a :: "'a::field_char_0 fps"
   1.125    assumes
   1.126    k: "k>0"
   1.127    and ra0: "r k (a $ 0) ^ k = a $ 0"
   1.128 @@ -2159,7 +2166,7 @@
   1.129  by (induct n, auto)
   1.130  
   1.131  lemma fps_compose_radical:
   1.132 -  assumes b0: "b$0 = (0::'a::{field, ring_char_0})"
   1.133 +  assumes b0: "b$0 = (0::'a::field_char_0)"
   1.134    and ra0: "r (Suc k) (a$0) ^ Suc k = a$0"
   1.135    and a0: "a$0 \<noteq> 0"
   1.136    shows "fps_radical r (Suc k)  a oo b = fps_radical r (Suc k) (a oo b)"
   1.137 @@ -2260,7 +2267,7 @@
   1.138  subsubsection{* Exponential series *}
   1.139  definition "E x = Abs_fps (\<lambda>n. x^n / of_nat (fact n))"
   1.140  
   1.141 -lemma E_deriv[simp]: "fps_deriv (E a) = fps_const (a::'a::{field, ring_char_0}) * E a" (is "?l = ?r")
   1.142 +lemma E_deriv[simp]: "fps_deriv (E a) = fps_const (a::'a::field_char_0) * E a" (is "?l = ?r")
   1.143  proof-
   1.144    {fix n
   1.145      have "?l$n = ?r $ n"
   1.146 @@ -2270,7 +2277,7 @@
   1.147  qed
   1.148  
   1.149  lemma E_unique_ODE:
   1.150 -  "fps_deriv a = fps_const c * a \<longleftrightarrow> a = fps_const (a$0) * E (c :: 'a::{field, ring_char_0})"
   1.151 +  "fps_deriv a = fps_const c * a \<longleftrightarrow> a = fps_const (a$0) * E (c :: 'a::field_char_0)"
   1.152    (is "?lhs \<longleftrightarrow> ?rhs")
   1.153  proof-
   1.154    {assume d: ?lhs
   1.155 @@ -2297,7 +2304,7 @@
   1.156  ultimately show ?thesis by blast
   1.157  qed
   1.158  
   1.159 -lemma E_add_mult: "E (a + b) = E (a::'a::{ring_char_0, field}) * E b" (is "?l = ?r")
   1.160 +lemma E_add_mult: "E (a + b) = E (a::'a::field_char_0) * E b" (is "?l = ?r")
   1.161  proof-
   1.162    have "fps_deriv (?r) = fps_const (a+b) * ?r"
   1.163      by (simp add: fps_const_add[symmetric] ring_simps del: fps_const_add)
   1.164 @@ -2312,7 +2319,7 @@
   1.165  lemma E0[simp]: "E (0::'a::{field}) = 1"
   1.166    by (simp add: fps_eq_iff power_0_left)
   1.167  
   1.168 -lemma E_neg: "E (- a) = inverse (E (a::'a::{ring_char_0, field}))"
   1.169 +lemma E_neg: "E (- a) = inverse (E (a::'a::field_char_0))"
   1.170  proof-
   1.171    from E_add_mult[of a "- a"] have th0: "E a * E (- a) = 1"
   1.172      by (simp )
   1.173 @@ -2320,7 +2327,7 @@
   1.174    from fps_inverse_unique[OF th1 th0] show ?thesis by simp
   1.175  qed
   1.176  
   1.177 -lemma E_nth_deriv[simp]: "fps_nth_deriv n (E (a::'a::{field, ring_char_0})) = (fps_const a)^n * (E a)"
   1.178 +lemma E_nth_deriv[simp]: "fps_nth_deriv n (E (a::'a::field_char_0)) = (fps_const a)^n * (E a)"
   1.179    by (induct n, auto simp add: power_Suc)
   1.180  
   1.181  
   1.182 @@ -2355,11 +2362,11 @@
   1.183    from fps_inverse_unique[OF th' th] show ?thesis .
   1.184  qed
   1.185  
   1.186 -lemma E_power_mult: "(E (c::'a::{field,ring_char_0}))^n = E (of_nat n * c)"
   1.187 +lemma E_power_mult: "(E (c::'a::field_char_0))^n = E (of_nat n * c)"
   1.188    by (induct n, auto simp add: ring_simps E_add_mult power_Suc)
   1.189  
   1.190  subsubsection{* Logarithmic series *}
   1.191 -definition "(L::'a::{field, ring_char_0} fps)
   1.192 +definition "(L::'a::field_char_0 fps)
   1.193    = Abs_fps (\<lambda>n. (- 1) ^ Suc n / of_nat n)"
   1.194  
   1.195  lemma fps_deriv_L: "fps_deriv L = inverse (1 + X)"
   1.196 @@ -2371,7 +2378,7 @@
   1.197    by (simp add: L_def)
   1.198  
   1.199  lemma L_E_inv:
   1.200 -  assumes a: "a\<noteq> (0::'a::{field,division_by_zero,ring_char_0})"
   1.201 +  assumes a: "a \<noteq> (0::'a::{field_char_0,division_by_zero})"
   1.202    shows "L = fps_const a * fps_inv (E a - 1)" (is "?l = ?r")
   1.203  proof-
   1.204    let ?b = "E a - 1"
   1.205 @@ -2395,16 +2402,17 @@
   1.206  
   1.207  subsubsection{* Formal trigonometric functions  *}
   1.208  
   1.209 -definition "fps_sin (c::'a::{field, ring_char_0}) =
   1.210 +definition "fps_sin (c::'a::field_char_0) =
   1.211    Abs_fps (\<lambda>n. if even n then 0 else (- 1) ^((n - 1) div 2) * c^n /(of_nat (fact n)))"
   1.212  
   1.213 -definition "fps_cos (c::'a::{field, ring_char_0}) = Abs_fps (\<lambda>n. if even n then (- 1) ^ (n div 2) * c^n / (of_nat (fact n)) else 0)"
   1.214 +definition "fps_cos (c::'a::field_char_0) =
   1.215 +  Abs_fps (\<lambda>n. if even n then (- 1) ^ (n div 2) * c^n / (of_nat (fact n)) else 0)"
   1.216  
   1.217  lemma fps_sin_deriv:
   1.218    "fps_deriv (fps_sin c) = fps_const c * fps_cos c"
   1.219    (is "?lhs = ?rhs")
   1.220 -proof-
   1.221 -  {fix n::nat
   1.222 +proof (rule fps_ext)
   1.223 +  fix n::nat
   1.224      {assume en: "even n"
   1.225        have "?lhs$n = of_nat (n+1) * (fps_sin c $ (n+1))" by simp
   1.226        also have "\<dots> = of_nat (n+1) * ((- 1)^(n div 2) * c^Suc n / of_nat (fact (Suc n)))"
   1.227 @@ -2416,18 +2424,18 @@
   1.228  	by (simp add: field_simps del: of_nat_add of_nat_Suc)
   1.229        finally have "?lhs $n = ?rhs$n" using en
   1.230  	by (simp add: fps_cos_def ring_simps power_Suc )}
   1.231 -    then have "?lhs $ n = ?rhs $ n"
   1.232 -      by (cases "even n", simp_all add: fps_deriv_def fps_sin_def fps_cos_def) }
   1.233 -  then show ?thesis by (auto simp add: fps_eq_iff)
   1.234 +    then show "?lhs $ n = ?rhs $ n"
   1.235 +      by (cases "even n", simp_all add: fps_deriv_def fps_sin_def fps_cos_def)
   1.236  qed
   1.237  
   1.238  lemma fps_cos_deriv:
   1.239    "fps_deriv (fps_cos c) = fps_const (- c)* (fps_sin c)"
   1.240    (is "?lhs = ?rhs")
   1.241 -proof-
   1.242 +proof (rule fps_ext)
   1.243    have th0: "\<And>n. - ((- 1::'a) ^ n) = (- 1)^Suc n" by (simp add: power_Suc)
   1.244 -  have th1: "\<And>n. odd n\<Longrightarrow> Suc ((n - 1) div 2) = Suc n div 2" by presburger (* FIXME: VERY slow! *)
   1.245 -  {fix n::nat
   1.246 +  have th1: "\<And>n. odd n \<Longrightarrow> Suc ((n - 1) div 2) = Suc n div 2"
   1.247 +    by (case_tac n, simp_all)
   1.248 +  fix n::nat
   1.249      {assume en: "odd n"
   1.250        from en have n0: "n \<noteq>0 " by presburger
   1.251        have "?lhs$n = of_nat (n+1) * (fps_cos c $ (n+1))" by simp
   1.252 @@ -2442,10 +2450,9 @@
   1.253  	unfolding th0 unfolding th1[OF en] by simp
   1.254        finally have "?lhs $n = ?rhs$n" using en
   1.255  	by (simp add: fps_sin_def ring_simps power_Suc)}
   1.256 -    then have "?lhs $ n = ?rhs $ n"
   1.257 +    then show "?lhs $ n = ?rhs $ n"
   1.258        by (cases "even n", simp_all add: fps_deriv_def fps_sin_def
   1.259 -	fps_cos_def) }
   1.260 -  then show ?thesis by (auto simp add: fps_eq_iff)
   1.261 +	fps_cos_def)
   1.262  qed
   1.263  
   1.264  lemma fps_sin_cos_sum_of_squares: