moved AFP material to Formal_Power_Series; renamed E/L/F in Formal_Power_Series
authoreberlm <eberlm@in.tum.de>
Tue Apr 04 09:01:19 2017 +0200 (2017-04-04)
changeset 65396b42167902f57
parent 65395 7504569a73c7
child 65397 9cdafcfb28bf
moved AFP material to Formal_Power_Series; renamed E/L/F in Formal_Power_Series
NEWS
src/HOL/Library/Formal_Power_Series.thy
     1.1 --- a/NEWS	Tue Apr 04 08:57:21 2017 +0200
     1.2 +++ b/NEWS	Tue Apr 04 09:01:19 2017 +0200
     1.3 @@ -50,6 +50,10 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Constants E/L/F in Library/Formal_Power_Series were renamed to
     1.8 +fps_exp/fps_ln/fps_hypergeo to avoid polluting the name space.
     1.9 +INCOMPATIBILITY.
    1.10 +
    1.11  * Constant "surj" is a full input/output abbreviation (again).
    1.12  Minor INCOMPATIBILITY.
    1.13  
     2.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Tue Apr 04 08:57:21 2017 +0200
     2.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Tue Apr 04 09:01:19 2017 +0200
     2.3 @@ -393,6 +393,11 @@
     2.4  lemma fps_of_nat: "fps_const (of_nat c) = of_nat c"
     2.5    by (induction c) (simp_all add: fps_const_add [symmetric] del: fps_const_add)
     2.6  
     2.7 +lemma numeral_neq_fps_zero [simp]: "(numeral f :: 'a :: field_char_0 fps) \<noteq> 0"
     2.8 +proof
     2.9 +  assume "numeral f = (0 :: 'a fps)"
    2.10 +  from arg_cong[of _ _ "\<lambda>F. F $ 0", OF this] show False by simp
    2.11 +qed 
    2.12  
    2.13  
    2.14  subsection \<open>The eXtractor series X\<close>
    2.15 @@ -1593,6 +1598,12 @@
    2.16  lemma fps_deriv_const[simp]: "fps_deriv (fps_const c) = 0"
    2.17    by (simp add: fps_ext fps_deriv_def fps_const_def)
    2.18  
    2.19 +lemma fps_deriv_of_nat [simp]: "fps_deriv (of_nat n) = 0"
    2.20 +  by (simp add: fps_of_nat [symmetric])
    2.21 +
    2.22 +lemma fps_deriv_numeral [simp]: "fps_deriv (numeral n) = 0"
    2.23 +  by (simp add: numeral_fps_const)    
    2.24 +
    2.25  lemma fps_deriv_mult_const_left[simp]:
    2.26    "fps_deriv (fps_const (c::'a::comm_ring_1) * f) = fps_const c * fps_deriv f"
    2.27    by simp
    2.28 @@ -3424,7 +3435,7 @@
    2.29  
    2.30  lemma fps_compose_uminus: "- (a::'a::ring_1 fps) oo c = - (a oo c)"
    2.31    by (simp add: fps_eq_iff fps_compose_nth field_simps sum_negf[symmetric])
    2.32 -
    2.33 +    
    2.34  lemma fps_compose_sub_distrib: "(a - b) oo (c::'a::ring_1 fps) = (a oo c) - (b oo c)"
    2.35    using fps_compose_add_distrib [of a "- b" c] by (simp add: fps_compose_uminus)
    2.36  
    2.37 @@ -3692,17 +3703,23 @@
    2.38    "fps_compose (f :: 'a :: comm_ring_1 fps) (fps_const c * X) = Abs_fps (\<lambda>n. c^n * f $ n)"
    2.39    by (simp add: fps_eq_iff fps_compose_def power_mult_distrib
    2.40                  if_distrib sum.delta' cong: if_cong)
    2.41 +              
    2.42 +lemma fps_compose_uminus': 
    2.43 +  "fps_compose f (-X :: 'a :: comm_ring_1 fps) = Abs_fps (\<lambda>n. (-1)^n * f $ n)"
    2.44 +  using fps_compose_linear[of f "-1"] 
    2.45 +  by (simp only: fps_const_neg [symmetric] fps_const_1_eq_1) simp
    2.46  
    2.47  subsection \<open>Elementary series\<close>
    2.48  
    2.49  subsubsection \<open>Exponential series\<close>
    2.50  
    2.51 -definition "E x = Abs_fps (\<lambda>n. x^n / of_nat (fact n))"
    2.52 -
    2.53 -lemma E_deriv[simp]: "fps_deriv (E a) = fps_const (a::'a::field_char_0) * E a" (is "?l = ?r")
    2.54 +definition "fps_exp x = Abs_fps (\<lambda>n. x^n / of_nat (fact n))"
    2.55 +
    2.56 +lemma fps_exp_deriv[simp]: "fps_deriv (fps_exp a) = fps_const (a::'a::field_char_0) * fps_exp a" 
    2.57 +  (is "?l = ?r")
    2.58  proof -
    2.59    have "?l$n = ?r $ n" for n
    2.60 -    apply (auto simp add: E_def field_simps power_Suc[symmetric]
    2.61 +    apply (auto simp add: fps_exp_def field_simps power_Suc[symmetric]
    2.62        simp del: fact_Suc of_nat_Suc power_Suc)
    2.63      apply (simp add: field_simps)
    2.64      done
    2.65 @@ -3710,8 +3727,8 @@
    2.66      by (simp add: fps_eq_iff)
    2.67  qed
    2.68  
    2.69 -lemma E_unique_ODE:
    2.70 -  "fps_deriv a = fps_const c * a \<longleftrightarrow> a = fps_const (a$0) * E (c::'a::field_char_0)"
    2.71 +lemma fps_exp_unique_ODE:
    2.72 +  "fps_deriv a = fps_const c * a \<longleftrightarrow> a = fps_const (a$0) * fps_exp (c::'a::field_char_0)"
    2.73    (is "?lhs \<longleftrightarrow> ?rhs")
    2.74  proof
    2.75    show ?rhs if ?lhs
    2.76 @@ -3732,75 +3749,107 @@
    2.77          done
    2.78      qed
    2.79      show ?thesis
    2.80 -      by (auto simp add: fps_eq_iff fps_const_mult_left E_def intro: th')
    2.81 +      by (auto simp add: fps_eq_iff fps_const_mult_left fps_exp_def intro: th')
    2.82    qed
    2.83    show ?lhs if ?rhs
    2.84 -    using that by (metis E_deriv fps_deriv_mult_const_left mult.left_commute)
    2.85 +    using that by (metis fps_exp_deriv fps_deriv_mult_const_left mult.left_commute)
    2.86  qed
    2.87  
    2.88 -lemma E_add_mult: "E (a + b) = E (a::'a::field_char_0) * E b" (is "?l = ?r")
    2.89 +lemma fps_exp_add_mult: "fps_exp (a + b) = fps_exp (a::'a::field_char_0) * fps_exp b" (is "?l = ?r")
    2.90  proof -
    2.91    have "fps_deriv ?r = fps_const (a + b) * ?r"
    2.92      by (simp add: fps_const_add[symmetric] field_simps del: fps_const_add)
    2.93    then have "?r = ?l"
    2.94 -    by (simp only: E_unique_ODE) (simp add: fps_mult_nth E_def)
    2.95 +    by (simp only: fps_exp_unique_ODE) (simp add: fps_mult_nth fps_exp_def)
    2.96    then show ?thesis ..
    2.97  qed
    2.98  
    2.99 -lemma E_nth[simp]: "E a $ n = a^n / of_nat (fact n)"
   2.100 -  by (simp add: E_def)
   2.101 -
   2.102 -lemma E0[simp]: "E (0::'a::field) = 1"
   2.103 +lemma fps_exp_nth[simp]: "fps_exp a $ n = a^n / of_nat (fact n)"
   2.104 +  by (simp add: fps_exp_def)
   2.105 +
   2.106 +lemma fps_exp_0[simp]: "fps_exp (0::'a::field) = 1"
   2.107    by (simp add: fps_eq_iff power_0_left)
   2.108  
   2.109 -lemma E_neg: "E (- a) = inverse (E (a::'a::field_char_0))"
   2.110 +lemma fps_exp_neg: "fps_exp (- a) = inverse (fps_exp (a::'a::field_char_0))"
   2.111  proof -
   2.112 -  from E_add_mult[of a "- a"] have th0: "E a * E (- a) = 1" by simp
   2.113 +  from fps_exp_add_mult[of a "- a"] have th0: "fps_exp a * fps_exp (- a) = 1" by simp
   2.114    from fps_inverse_unique[OF th0] show ?thesis by simp
   2.115  qed
   2.116  
   2.117 -lemma E_nth_deriv[simp]: "fps_nth_deriv n (E (a::'a::field_char_0)) = (fps_const a)^n * (E a)"
   2.118 +lemma fps_exp_nth_deriv[simp]: 
   2.119 +  "fps_nth_deriv n (fps_exp (a::'a::field_char_0)) = (fps_const a)^n * (fps_exp a)"
   2.120    by (induct n) auto
   2.121  
   2.122 -lemma X_compose_E[simp]: "X oo E (a::'a::field) = E a - 1"
   2.123 +lemma X_compose_fps_exp[simp]: "X oo fps_exp (a::'a::field) = fps_exp a - 1"
   2.124    by (simp add: fps_eq_iff X_fps_compose)
   2.125  
   2.126 -lemma LE_compose:
   2.127 +lemma fps_inv_fps_exp_compose:
   2.128    assumes a: "a \<noteq> 0"
   2.129 -  shows "fps_inv (E a - 1) oo (E a - 1) = X"
   2.130 -    and "(E a - 1) oo fps_inv (E a - 1) = X"
   2.131 +  shows "fps_inv (fps_exp a - 1) oo (fps_exp a - 1) = X"
   2.132 +    and "(fps_exp a - 1) oo fps_inv (fps_exp a - 1) = X"
   2.133  proof -
   2.134 -  let ?b = "E a - 1"
   2.135 +  let ?b = "fps_exp a - 1"
   2.136    have b0: "?b $ 0 = 0"
   2.137      by simp
   2.138    have b1: "?b $ 1 \<noteq> 0"
   2.139      by (simp add: a)
   2.140 -  from fps_inv[OF b0 b1] show "fps_inv (E a - 1) oo (E a - 1) = X" .
   2.141 -  from fps_inv_right[OF b0 b1] show "(E a - 1) oo fps_inv (E a - 1) = X" .
   2.142 +  from fps_inv[OF b0 b1] show "fps_inv (fps_exp a - 1) oo (fps_exp a - 1) = X" .
   2.143 +  from fps_inv_right[OF b0 b1] show "(fps_exp a - 1) oo fps_inv (fps_exp a - 1) = X" .
   2.144  qed
   2.145  
   2.146 -lemma E_power_mult: "(E (c::'a::field_char_0))^n = E (of_nat n * c)"
   2.147 -  by (induct n) (auto simp add: field_simps E_add_mult)
   2.148 -
   2.149 -lemma radical_E:
   2.150 +lemma fps_exp_power_mult: "(fps_exp (c::'a::field_char_0))^n = fps_exp (of_nat n * c)"
   2.151 +  by (induct n) (auto simp add: field_simps fps_exp_add_mult)
   2.152 +
   2.153 +lemma radical_fps_exp:
   2.154    assumes r: "r (Suc k) 1 = 1"
   2.155 -  shows "fps_radical r (Suc k) (E (c::'a::field_char_0)) = E (c / of_nat (Suc k))"
   2.156 +  shows "fps_radical r (Suc k) (fps_exp (c::'a::field_char_0)) = fps_exp (c / of_nat (Suc k))"
   2.157  proof -
   2.158    let ?ck = "(c / of_nat (Suc k))"
   2.159    let ?r = "fps_radical r (Suc k)"
   2.160    have eq0[simp]: "?ck * of_nat (Suc k) = c" "of_nat (Suc k) * ?ck = c"
   2.161      by (simp_all del: of_nat_Suc)
   2.162 -  have th0: "E ?ck ^ (Suc k) = E c" unfolding E_power_mult eq0 ..
   2.163 -  have th: "r (Suc k) (E c $0) ^ Suc k = E c $ 0"
   2.164 -    "r (Suc k) (E c $ 0) = E ?ck $ 0" "E c $ 0 \<noteq> 0" using r by simp_all
   2.165 +  have th0: "fps_exp ?ck ^ (Suc k) = fps_exp c" unfolding fps_exp_power_mult eq0 ..
   2.166 +  have th: "r (Suc k) (fps_exp c $0) ^ Suc k = fps_exp c $ 0"
   2.167 +    "r (Suc k) (fps_exp c $ 0) = fps_exp ?ck $ 0" "fps_exp c $ 0 \<noteq> 0" using r by simp_all
   2.168    from th0 radical_unique[where r=r and k=k, OF th] show ?thesis
   2.169      by auto
   2.170  qed
   2.171  
   2.172 -lemma Ec_E1_eq: "E (1::'a::field_char_0) oo (fps_const c * X) = E c"
   2.173 -  apply (auto simp add: fps_eq_iff E_def fps_compose_def power_mult_distrib)
   2.174 -  apply (simp add: cond_value_iff cond_application_beta sum.delta' cong del: if_weak_cong)
   2.175 -  done
   2.176 +lemma fps_exp_compose_linear [simp]: 
   2.177 +  "fps_exp (d::'a::field_char_0) oo (fps_const c * X) = fps_exp (c * d)"
   2.178 +  by (simp add: fps_compose_linear fps_exp_def fps_eq_iff power_mult_distrib)
   2.179 +  
   2.180 +lemma fps_fps_exp_compose_minus [simp]: 
   2.181 +  "fps_compose (fps_exp c) (-X) = fps_exp (-c :: 'a :: field_char_0)"
   2.182 +  using fps_exp_compose_linear[of c "-1 :: 'a"] 
   2.183 +  unfolding fps_const_neg [symmetric] fps_const_1_eq_1 by simp
   2.184 +
   2.185 +lemma fps_exp_eq_iff [simp]: "fps_exp c = fps_exp d \<longleftrightarrow> c = (d :: 'a :: field_char_0)"
   2.186 +proof
   2.187 +  assume "fps_exp c = fps_exp d"
   2.188 +  from arg_cong[of _ _ "\<lambda>F. F $ 1", OF this] show "c = d" by simp
   2.189 +qed simp_all
   2.190 +
   2.191 +lemma fps_exp_eq_fps_const_iff [simp]: 
   2.192 +  "fps_exp (c :: 'a :: field_char_0) = fps_const c' \<longleftrightarrow> c = 0 \<and> c' = 1"
   2.193 +proof
   2.194 +  assume "c = 0 \<and> c' = 1"
   2.195 +  thus "fps_exp c = fps_const c'" by (auto simp: fps_eq_iff)
   2.196 +next
   2.197 +  assume "fps_exp c = fps_const c'"
   2.198 +  from arg_cong[of _ _ "\<lambda>F. F $ 1", OF this] arg_cong[of _ _ "\<lambda>F. F $ 0", OF this] 
   2.199 +    show "c = 0 \<and> c' = 1" by simp_all
   2.200 +qed
   2.201 +
   2.202 +lemma fps_exp_neq_0 [simp]: "\<not>fps_exp (c :: 'a :: field_char_0) = 0"
   2.203 +  unfolding fps_const_0_eq_0 [symmetric] fps_exp_eq_fps_const_iff by simp  
   2.204 +
   2.205 +lemma fps_exp_eq_1_iff [simp]: "fps_exp (c :: 'a :: field_char_0) = 1 \<longleftrightarrow> c = 0"
   2.206 +  unfolding fps_const_1_eq_1 [symmetric] fps_exp_eq_fps_const_iff by simp
   2.207 +    
   2.208 +lemma fps_exp_neq_numeral_iff [simp]: 
   2.209 +  "fps_exp (c :: 'a :: field_char_0) = numeral n \<longleftrightarrow> c = 0 \<and> n = Num.One"
   2.210 +  unfolding numeral_fps_const fps_exp_eq_fps_const_iff by simp
   2.211  
   2.212  
   2.213  subsubsection \<open>Logarithmic series\<close>
   2.214 @@ -3810,61 +3859,67 @@
   2.215      fps_const v + X * Abs_fps (\<lambda>n. f (Suc n))"
   2.216    by (auto simp add: fps_eq_iff)
   2.217  
   2.218 -definition L :: "'a::field_char_0 \<Rightarrow> 'a fps"
   2.219 -  where "L c = fps_const (1/c) * Abs_fps (\<lambda>n. if n = 0 then 0 else (- 1) ^ (n - 1) / of_nat n)"
   2.220 -
   2.221 -lemma fps_deriv_L: "fps_deriv (L c) = fps_const (1/c) * inverse (1 + X)"
   2.222 +definition fps_ln :: "'a::field_char_0 \<Rightarrow> 'a fps"
   2.223 +  where "fps_ln c = fps_const (1/c) * Abs_fps (\<lambda>n. if n = 0 then 0 else (- 1) ^ (n - 1) / of_nat n)"
   2.224 +
   2.225 +lemma fps_ln_deriv: "fps_deriv (fps_ln c) = fps_const (1/c) * inverse (1 + X)"
   2.226    unfolding fps_inverse_X_plus1
   2.227 -  by (simp add: L_def fps_eq_iff del: of_nat_Suc)
   2.228 -
   2.229 -lemma L_nth: "L c $ n = (if n = 0 then 0 else 1/c * ((- 1) ^ (n - 1) / of_nat n))"
   2.230 -  by (simp add: L_def field_simps)
   2.231 -
   2.232 -lemma L_0[simp]: "L c $ 0 = 0" by (simp add: L_def)
   2.233 -
   2.234 -lemma L_E_inv:
   2.235 +  by (simp add: fps_ln_def fps_eq_iff del: of_nat_Suc)
   2.236 +
   2.237 +lemma fps_ln_nth: "fps_ln c $ n = (if n = 0 then 0 else 1/c * ((- 1) ^ (n - 1) / of_nat n))"
   2.238 +  by (simp add: fps_ln_def field_simps)
   2.239 +
   2.240 +lemma fps_ln_0 [simp]: "fps_ln c $ 0 = 0" by (simp add: fps_ln_def)
   2.241 +
   2.242 +lemma fps_ln_fps_exp_inv:
   2.243    fixes a :: "'a::field_char_0"
   2.244    assumes a: "a \<noteq> 0"
   2.245 -  shows "L a = fps_inv (E a - 1)"  (is "?l = ?r")
   2.246 +  shows "fps_ln a = fps_inv (fps_exp a - 1)"  (is "?l = ?r")
   2.247  proof -
   2.248 -  let ?b = "E a - 1"
   2.249 +  let ?b = "fps_exp a - 1"
   2.250    have b0: "?b $ 0 = 0" by simp
   2.251    have b1: "?b $ 1 \<noteq> 0" by (simp add: a)
   2.252 -  have "fps_deriv (E a - 1) oo fps_inv (E a - 1) =
   2.253 -    (fps_const a * (E a - 1) + fps_const a) oo fps_inv (E a - 1)"
   2.254 +  have "fps_deriv (fps_exp a - 1) oo fps_inv (fps_exp a - 1) =
   2.255 +    (fps_const a * (fps_exp a - 1) + fps_const a) oo fps_inv (fps_exp a - 1)"
   2.256      by (simp add: field_simps)
   2.257    also have "\<dots> = fps_const a * (X + 1)"
   2.258      apply (simp add: fps_compose_add_distrib fps_const_mult_apply_left[symmetric] fps_inv_right[OF b0 b1])
   2.259      apply (simp add: field_simps)
   2.260      done
   2.261 -  finally have eq: "fps_deriv (E a - 1) oo fps_inv (E a - 1) = fps_const a * (X + 1)" .
   2.262 +  finally have eq: "fps_deriv (fps_exp a - 1) oo fps_inv (fps_exp a - 1) = fps_const a * (X + 1)" .
   2.263    from fps_inv_deriv[OF b0 b1, unfolded eq]
   2.264    have "fps_deriv (fps_inv ?b) = fps_const (inverse a) / (X + 1)"
   2.265 -    using a
   2.266 -    by (simp add: fps_const_inverse eq fps_divide_def fps_inverse_mult)
   2.267 +    using a by (simp add: fps_const_inverse eq fps_divide_def fps_inverse_mult)
   2.268    then have "fps_deriv ?l = fps_deriv ?r"
   2.269 -    by (simp add: fps_deriv_L add.commute fps_divide_def divide_inverse)
   2.270 +    by (simp add: fps_ln_deriv add.commute fps_divide_def divide_inverse)
   2.271    then show ?thesis unfolding fps_deriv_eq_iff
   2.272 -    by (simp add: L_nth fps_inv_def)
   2.273 +    by (simp add: fps_ln_nth fps_inv_def)
   2.274  qed
   2.275  
   2.276 -lemma L_mult_add:
   2.277 +lemma fps_ln_mult_add:
   2.278    assumes c0: "c\<noteq>0"
   2.279      and d0: "d\<noteq>0"
   2.280 -  shows "L c + L d = fps_const (c+d) * L (c*d)"
   2.281 +  shows "fps_ln c + fps_ln d = fps_const (c+d) * fps_ln (c*d)"
   2.282    (is "?r = ?l")
   2.283  proof-
   2.284    from c0 d0 have eq: "1/c + 1/d = (c+d)/(c*d)" by (simp add: field_simps)
   2.285    have "fps_deriv ?r = fps_const (1/c + 1/d) * inverse (1 + X)"
   2.286 -    by (simp add: fps_deriv_L fps_const_add[symmetric] algebra_simps del: fps_const_add)
   2.287 +    by (simp add: fps_ln_deriv fps_const_add[symmetric] algebra_simps del: fps_const_add)
   2.288    also have "\<dots> = fps_deriv ?l"
   2.289 -    apply (simp add: fps_deriv_L)
   2.290 +    apply (simp add: fps_ln_deriv)
   2.291      apply (simp add: fps_eq_iff eq)
   2.292      done
   2.293    finally show ?thesis
   2.294      unfolding fps_deriv_eq_iff by simp
   2.295  qed
   2.296  
   2.297 +lemma X_dvd_fps_ln [simp]: "X dvd fps_ln c"
   2.298 +proof -
   2.299 +  have "fps_ln c = X * Abs_fps (\<lambda>n. (-1) ^ n / (of_nat (Suc n) * c))"
   2.300 +    by (intro fps_ext) (auto simp: fps_ln_def of_nat_diff)
   2.301 +  thus ?thesis by simp
   2.302 +qed
   2.303 +
   2.304  
   2.305  subsubsection \<open>Binomial series\<close>
   2.306  
   2.307 @@ -4458,9 +4513,9 @@
   2.308    finally show ?thesis by simp
   2.309  qed
   2.310  
   2.311 -text \<open>Connection to E c over the complex numbers --- Euler and de Moivre.\<close>
   2.312 -
   2.313 -lemma Eii_sin_cos: "E (\<i> * c) = fps_cos c + fps_const \<i> * fps_sin c"
   2.314 +text \<open>Connection to @{const "fps_exp"} over the complex numbers --- Euler and de Moivre.\<close>
   2.315 +
   2.316 +lemma fps_exp_ii_sin_cos: "fps_exp (\<i> * c) = fps_cos c + fps_const \<i> * fps_sin c"
   2.317    (is "?l = ?r")
   2.318  proof -
   2.319    have "?l $ n = ?r $ n" for n
   2.320 @@ -4480,8 +4535,8 @@
   2.321      by (simp add: fps_eq_iff)
   2.322  qed
   2.323  
   2.324 -lemma E_minus_ii_sin_cos: "E (- (\<i> * c)) = fps_cos c - fps_const \<i> * fps_sin c"
   2.325 -  unfolding minus_mult_right Eii_sin_cos by (simp add: fps_sin_even fps_cos_odd)
   2.326 +lemma fps_exp_minus_ii_sin_cos: "fps_exp (- (\<i> * c)) = fps_cos c - fps_const \<i> * fps_sin c"
   2.327 +  unfolding minus_mult_right fps_exp_ii_sin_cos by (simp add: fps_sin_even fps_cos_odd)
   2.328  
   2.329  lemma fps_const_minus: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d)"
   2.330    by (fact fps_const_sub)
   2.331 @@ -4490,30 +4545,34 @@
   2.332    by (induction c) (simp_all add: fps_const_minus [symmetric] fps_of_nat fps_const_neg [symmetric] 
   2.333                               del: fps_const_minus fps_const_neg)
   2.334  
   2.335 +lemma fps_deriv_of_int [simp]: "fps_deriv (of_int n) = 0"
   2.336 +  by (simp add: fps_of_int [symmetric])
   2.337 +
   2.338  lemma fps_numeral_fps_const: "numeral i = fps_const (numeral i :: 'a::comm_ring_1)"
   2.339    by (fact numeral_fps_const) (* FIXME: duplicate *)
   2.340  
   2.341 -lemma fps_cos_Eii: "fps_cos c = (E (\<i> * c) + E (- \<i> * c)) / fps_const 2"
   2.342 +lemma fps_cos_fps_exp_ii: "fps_cos c = (fps_exp (\<i> * c) + fps_exp (- \<i> * c)) / fps_const 2"
   2.343  proof -
   2.344    have th: "fps_cos c + fps_cos c = fps_cos c * fps_const 2"
   2.345      by (simp add: numeral_fps_const)
   2.346    show ?thesis
   2.347 -    unfolding Eii_sin_cos minus_mult_commute
   2.348 +    unfolding fps_exp_ii_sin_cos minus_mult_commute
   2.349      by (simp add: fps_sin_even fps_cos_odd numeral_fps_const fps_divide_unit fps_const_inverse th)
   2.350  qed
   2.351  
   2.352 -lemma fps_sin_Eii: "fps_sin c = (E (\<i> * c) - E (- \<i> * c)) / fps_const (2*\<i>)"
   2.353 +lemma fps_sin_fps_exp_ii: "fps_sin c = (fps_exp (\<i> * c) - fps_exp (- \<i> * c)) / fps_const (2*\<i>)"
   2.354  proof -
   2.355    have th: "fps_const \<i> * fps_sin c + fps_const \<i> * fps_sin c = fps_sin c * fps_const (2 * \<i>)"
   2.356      by (simp add: fps_eq_iff numeral_fps_const)
   2.357    show ?thesis
   2.358 -    unfolding Eii_sin_cos minus_mult_commute
   2.359 +    unfolding fps_exp_ii_sin_cos minus_mult_commute
   2.360      by (simp add: fps_sin_even fps_cos_odd fps_divide_unit fps_const_inverse th)
   2.361  qed
   2.362  
   2.363 -lemma fps_tan_Eii:
   2.364 -  "fps_tan c = (E (\<i> * c) - E (- \<i> * c)) / (fps_const \<i> * (E (\<i> * c) + E (- \<i> * c)))"
   2.365 -  unfolding fps_tan_def fps_sin_Eii fps_cos_Eii mult_minus_left E_neg
   2.366 +lemma fps_tan_fps_exp_ii:
   2.367 +  "fps_tan c = (fps_exp (\<i> * c) - fps_exp (- \<i> * c)) / 
   2.368 +      (fps_const \<i> * (fps_exp (\<i> * c) + fps_exp (- \<i> * c)))"
   2.369 +  unfolding fps_tan_def fps_sin_fps_exp_ii fps_cos_fps_exp_ii mult_minus_left fps_exp_neg
   2.370    apply (simp add: fps_divide_unit fps_inverse_mult fps_const_mult[symmetric] fps_const_inverse del: fps_const_mult)
   2.371    apply simp
   2.372    done
   2.373 @@ -4521,21 +4580,20 @@
   2.374  lemma fps_demoivre:
   2.375    "(fps_cos a + fps_const \<i> * fps_sin a)^n =
   2.376      fps_cos (of_nat n * a) + fps_const \<i> * fps_sin (of_nat n * a)"
   2.377 -  unfolding Eii_sin_cos[symmetric] E_power_mult
   2.378 +  unfolding fps_exp_ii_sin_cos[symmetric] fps_exp_power_mult
   2.379    by (simp add: ac_simps)
   2.380  
   2.381  
   2.382  subsection \<open>Hypergeometric series\<close>
   2.383  
   2.384 -(* TODO: Rename this *)
   2.385 -definition "F as bs (c::'a::{field_char_0,field}) =
   2.386 +definition "fps_hypergeo as bs (c::'a::{field_char_0,field}) =
   2.387    Abs_fps (\<lambda>n. (foldl (\<lambda>r a. r* pochhammer a n) 1 as * c^n) /
   2.388      (foldl (\<lambda>r b. r * pochhammer b n) 1 bs * of_nat (fact n)))"
   2.389  
   2.390 -lemma F_nth[simp]: "F as bs c $ n =
   2.391 +lemma fps_hypergeo_nth[simp]: "fps_hypergeo as bs c $ n =
   2.392    (foldl (\<lambda>r a. r* pochhammer a n) 1 as * c^n) /
   2.393      (foldl (\<lambda>r b. r * pochhammer b n) 1 bs * of_nat (fact n))"
   2.394 -  by (simp add: F_def)
   2.395 +  by (simp add: fps_hypergeo_def)
   2.396  
   2.397  lemma foldl_mult_start:
   2.398    fixes v :: "'a::comm_ring_1"
   2.399 @@ -4547,15 +4605,15 @@
   2.400    shows "foldr (\<lambda>x r. r * f x) as v = foldl (\<lambda>r x. r * f x) v as"
   2.401    by (induct as arbitrary: v) (auto simp add: foldl_mult_start)
   2.402  
   2.403 -lemma F_nth_alt:
   2.404 -  "F as bs c $ n = foldr (\<lambda>a r. r * pochhammer a n) as (c ^ n) /
   2.405 +lemma fps_hypergeo_nth_alt:
   2.406 +  "fps_hypergeo as bs c $ n = foldr (\<lambda>a r. r * pochhammer a n) as (c ^ n) /
   2.407      foldr (\<lambda>b r. r * pochhammer b n) bs (of_nat (fact n))"
   2.408    by (simp add: foldl_mult_start foldr_mult_foldl)
   2.409  
   2.410 -lemma F_E[simp]: "F [] [] c = E c"
   2.411 +lemma fps_hypergeo_fps_exp[simp]: "fps_hypergeo [] [] c = fps_exp c"
   2.412    by (simp add: fps_eq_iff)
   2.413  
   2.414 -lemma F_1_0[simp]: "F [1] [] c = 1/(1 - fps_const c * X)"
   2.415 +lemma fps_hypergeo_1_0[simp]: "fps_hypergeo [1] [] c = 1/(1 - fps_const c * X)"
   2.416  proof -
   2.417    let ?a = "(Abs_fps (\<lambda>n. 1)) oo (fps_const c * X)"
   2.418    have th0: "(fps_const c * X) $ 0 = 0" by simp
   2.419 @@ -4564,10 +4622,10 @@
   2.420        fps_compose_nth power_mult_distrib cond_value_iff sum.delta' cong del: if_weak_cong)
   2.421  qed
   2.422  
   2.423 -lemma F_B[simp]: "F [-a] [] (- 1) = fps_binomial a"
   2.424 +lemma fps_hypergeo_B[simp]: "fps_hypergeo [-a] [] (- 1) = fps_binomial a"
   2.425    by (simp add: fps_eq_iff gbinomial_pochhammer algebra_simps)
   2.426  
   2.427 -lemma F_0[simp]: "F as bs c $ 0 = 1"
   2.428 +lemma fps_hypergeo_0[simp]: "fps_hypergeo as bs c $ 0 = 1"
   2.429    apply simp
   2.430    apply (subgoal_tac "\<forall>as. foldl (\<lambda>(r::'a) (a::'a). r) 1 as = 1")
   2.431    apply auto
   2.432 @@ -4581,9 +4639,9 @@
   2.433    by (induct as arbitrary: v w) (auto simp add: algebra_simps)
   2.434  
   2.435  
   2.436 -lemma F_rec:
   2.437 -  "F as bs c $ Suc n = ((foldl (\<lambda>r a. r* (a + of_nat n)) c as) /
   2.438 -    (foldl (\<lambda>r b. r * (b + of_nat n)) (of_nat (Suc n)) bs )) * F as bs c $ n"
   2.439 +lemma fps_hypergeo_rec:
   2.440 +  "fps_hypergeo as bs c $ Suc n = ((foldl (\<lambda>r a. r* (a + of_nat n)) c as) /
   2.441 +    (foldl (\<lambda>r b. r * (b + of_nat n)) (of_nat (Suc n)) bs )) * fps_hypergeo as bs c $ n"
   2.442    apply (simp del: of_nat_Suc of_nat_add fact_Suc)
   2.443    apply (simp add: foldl_mult_start del: fact_Suc of_nat_Suc)
   2.444    unfolding foldl_prod_prod[unfolded foldl_mult_start] pochhammer_Suc
   2.445 @@ -4612,12 +4670,12 @@
   2.446  lemma XDp_fps_integral [simp]: "XDp 0 (fps_integral a c) = X * a"
   2.447    by (simp add: fps_eq_iff fps_integral_def)
   2.448  
   2.449 -lemma F_minus_nat:
   2.450 -  "F [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0,field}) $ k =
   2.451 +lemma fps_hypergeo_minus_nat:
   2.452 +  "fps_hypergeo [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0,field}) $ k =
   2.453      (if k \<le> n then
   2.454        pochhammer (- of_nat n) k * c ^ k / (pochhammer (- of_nat (n + m)) k * of_nat (fact k))
   2.455       else 0)"
   2.456 -  "F [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0,field}) $ k =
   2.457 +  "fps_hypergeo [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0,field}) $ k =
   2.458      (if k \<le> m then
   2.459        pochhammer (- of_nat m) k * c ^ k / (pochhammer (- of_nat (m + n)) k * of_nat (fact k))
   2.460       else 0)"