src/HOL/Library/Formal_Power_Series.thy
changeset 65396 b42167902f57
parent 64786 340db65fd2c1
child 65398 a14fa655b48c
equal deleted inserted replaced
65395:7504569a73c7 65396:b42167902f57
   391   by (simp add: numeral_fps_const)
   391   by (simp add: numeral_fps_const)
   392 
   392 
   393 lemma fps_of_nat: "fps_const (of_nat c) = of_nat c"
   393 lemma fps_of_nat: "fps_const (of_nat c) = of_nat c"
   394   by (induction c) (simp_all add: fps_const_add [symmetric] del: fps_const_add)
   394   by (induction c) (simp_all add: fps_const_add [symmetric] del: fps_const_add)
   395 
   395 
       
   396 lemma numeral_neq_fps_zero [simp]: "(numeral f :: 'a :: field_char_0 fps) \<noteq> 0"
       
   397 proof
       
   398   assume "numeral f = (0 :: 'a fps)"
       
   399   from arg_cong[of _ _ "\<lambda>F. F $ 0", OF this] show False by simp
       
   400 qed 
   396 
   401 
   397 
   402 
   398 subsection \<open>The eXtractor series X\<close>
   403 subsection \<open>The eXtractor series X\<close>
   399 
   404 
   400 lemma minus_one_power_iff: "(- (1::'a::comm_ring_1)) ^ n = (if even n then 1 else - 1)"
   405 lemma minus_one_power_iff: "(- (1::'a::comm_ring_1)) ^ n = (if even n then 1 else - 1)"
  1590   "fps_deriv ((f:: 'a::comm_ring_1 fps) - g) = fps_deriv f - fps_deriv g"
  1595   "fps_deriv ((f:: 'a::comm_ring_1 fps) - g) = fps_deriv f - fps_deriv g"
  1591   using fps_deriv_add [of f "- g"] by simp
  1596   using fps_deriv_add [of f "- g"] by simp
  1592 
  1597 
  1593 lemma fps_deriv_const[simp]: "fps_deriv (fps_const c) = 0"
  1598 lemma fps_deriv_const[simp]: "fps_deriv (fps_const c) = 0"
  1594   by (simp add: fps_ext fps_deriv_def fps_const_def)
  1599   by (simp add: fps_ext fps_deriv_def fps_const_def)
       
  1600 
       
  1601 lemma fps_deriv_of_nat [simp]: "fps_deriv (of_nat n) = 0"
       
  1602   by (simp add: fps_of_nat [symmetric])
       
  1603 
       
  1604 lemma fps_deriv_numeral [simp]: "fps_deriv (numeral n) = 0"
       
  1605   by (simp add: numeral_fps_const)    
  1595 
  1606 
  1596 lemma fps_deriv_mult_const_left[simp]:
  1607 lemma fps_deriv_mult_const_left[simp]:
  1597   "fps_deriv (fps_const (c::'a::comm_ring_1) * f) = fps_const c * fps_deriv f"
  1608   "fps_deriv (fps_const (c::'a::comm_ring_1) * f) = fps_const c * fps_deriv f"
  1598   by simp
  1609   by simp
  1599 
  1610 
  3422     by (simp add: fps_compose_prod_distrib[OF c0])
  3433     by (simp add: fps_compose_prod_distrib[OF c0])
  3423 qed
  3434 qed
  3424 
  3435 
  3425 lemma fps_compose_uminus: "- (a::'a::ring_1 fps) oo c = - (a oo c)"
  3436 lemma fps_compose_uminus: "- (a::'a::ring_1 fps) oo c = - (a oo c)"
  3426   by (simp add: fps_eq_iff fps_compose_nth field_simps sum_negf[symmetric])
  3437   by (simp add: fps_eq_iff fps_compose_nth field_simps sum_negf[symmetric])
  3427 
  3438     
  3428 lemma fps_compose_sub_distrib: "(a - b) oo (c::'a::ring_1 fps) = (a oo c) - (b oo c)"
  3439 lemma fps_compose_sub_distrib: "(a - b) oo (c::'a::ring_1 fps) = (a oo c) - (b oo c)"
  3429   using fps_compose_add_distrib [of a "- b" c] by (simp add: fps_compose_uminus)
  3440   using fps_compose_add_distrib [of a "- b" c] by (simp add: fps_compose_uminus)
  3430 
  3441 
  3431 lemma X_fps_compose: "X oo a = Abs_fps (\<lambda>n. if n = 0 then (0::'a::comm_ring_1) else a$n)"
  3442 lemma X_fps_compose: "X oo a = Abs_fps (\<lambda>n. if n = 0 then (0::'a::comm_ring_1) else a$n)"
  3432   by (simp add: fps_eq_iff fps_compose_nth mult_delta_left sum.delta)
  3443   by (simp add: fps_eq_iff fps_compose_nth mult_delta_left sum.delta)
  3690 
  3701 
  3691 lemma fps_compose_linear:
  3702 lemma fps_compose_linear:
  3692   "fps_compose (f :: 'a :: comm_ring_1 fps) (fps_const c * X) = Abs_fps (\<lambda>n. c^n * f $ n)"
  3703   "fps_compose (f :: 'a :: comm_ring_1 fps) (fps_const c * X) = Abs_fps (\<lambda>n. c^n * f $ n)"
  3693   by (simp add: fps_eq_iff fps_compose_def power_mult_distrib
  3704   by (simp add: fps_eq_iff fps_compose_def power_mult_distrib
  3694                 if_distrib sum.delta' cong: if_cong)
  3705                 if_distrib sum.delta' cong: if_cong)
       
  3706               
       
  3707 lemma fps_compose_uminus': 
       
  3708   "fps_compose f (-X :: 'a :: comm_ring_1 fps) = Abs_fps (\<lambda>n. (-1)^n * f $ n)"
       
  3709   using fps_compose_linear[of f "-1"] 
       
  3710   by (simp only: fps_const_neg [symmetric] fps_const_1_eq_1) simp
  3695 
  3711 
  3696 subsection \<open>Elementary series\<close>
  3712 subsection \<open>Elementary series\<close>
  3697 
  3713 
  3698 subsubsection \<open>Exponential series\<close>
  3714 subsubsection \<open>Exponential series\<close>
  3699 
  3715 
  3700 definition "E x = Abs_fps (\<lambda>n. x^n / of_nat (fact n))"
  3716 definition "fps_exp x = Abs_fps (\<lambda>n. x^n / of_nat (fact n))"
  3701 
  3717 
  3702 lemma E_deriv[simp]: "fps_deriv (E a) = fps_const (a::'a::field_char_0) * E a" (is "?l = ?r")
  3718 lemma fps_exp_deriv[simp]: "fps_deriv (fps_exp a) = fps_const (a::'a::field_char_0) * fps_exp a" 
       
  3719   (is "?l = ?r")
  3703 proof -
  3720 proof -
  3704   have "?l$n = ?r $ n" for n
  3721   have "?l$n = ?r $ n" for n
  3705     apply (auto simp add: E_def field_simps power_Suc[symmetric]
  3722     apply (auto simp add: fps_exp_def field_simps power_Suc[symmetric]
  3706       simp del: fact_Suc of_nat_Suc power_Suc)
  3723       simp del: fact_Suc of_nat_Suc power_Suc)
  3707     apply (simp add: field_simps)
  3724     apply (simp add: field_simps)
  3708     done
  3725     done
  3709   then show ?thesis
  3726   then show ?thesis
  3710     by (simp add: fps_eq_iff)
  3727     by (simp add: fps_eq_iff)
  3711 qed
  3728 qed
  3712 
  3729 
  3713 lemma E_unique_ODE:
  3730 lemma fps_exp_unique_ODE:
  3714   "fps_deriv a = fps_const c * a \<longleftrightarrow> a = fps_const (a$0) * E (c::'a::field_char_0)"
  3731   "fps_deriv a = fps_const c * a \<longleftrightarrow> a = fps_const (a$0) * fps_exp (c::'a::field_char_0)"
  3715   (is "?lhs \<longleftrightarrow> ?rhs")
  3732   (is "?lhs \<longleftrightarrow> ?rhs")
  3716 proof
  3733 proof
  3717   show ?rhs if ?lhs
  3734   show ?rhs if ?lhs
  3718   proof -
  3735   proof -
  3719     from that have th: "\<And>n. a $ Suc n = c * a$n / of_nat (Suc n)"
  3736     from that have th: "\<And>n. a $ Suc n = c * a$n / of_nat (Suc n)"
  3730         apply (simp add: field_simps del: of_nat_Suc fact_Suc)
  3747         apply (simp add: field_simps del: of_nat_Suc fact_Suc)
  3731         apply simp
  3748         apply simp
  3732         done
  3749         done
  3733     qed
  3750     qed
  3734     show ?thesis
  3751     show ?thesis
  3735       by (auto simp add: fps_eq_iff fps_const_mult_left E_def intro: th')
  3752       by (auto simp add: fps_eq_iff fps_const_mult_left fps_exp_def intro: th')
  3736   qed
  3753   qed
  3737   show ?lhs if ?rhs
  3754   show ?lhs if ?rhs
  3738     using that by (metis E_deriv fps_deriv_mult_const_left mult.left_commute)
  3755     using that by (metis fps_exp_deriv fps_deriv_mult_const_left mult.left_commute)
  3739 qed
  3756 qed
  3740 
  3757 
  3741 lemma E_add_mult: "E (a + b) = E (a::'a::field_char_0) * E b" (is "?l = ?r")
  3758 lemma fps_exp_add_mult: "fps_exp (a + b) = fps_exp (a::'a::field_char_0) * fps_exp b" (is "?l = ?r")
  3742 proof -
  3759 proof -
  3743   have "fps_deriv ?r = fps_const (a + b) * ?r"
  3760   have "fps_deriv ?r = fps_const (a + b) * ?r"
  3744     by (simp add: fps_const_add[symmetric] field_simps del: fps_const_add)
  3761     by (simp add: fps_const_add[symmetric] field_simps del: fps_const_add)
  3745   then have "?r = ?l"
  3762   then have "?r = ?l"
  3746     by (simp only: E_unique_ODE) (simp add: fps_mult_nth E_def)
  3763     by (simp only: fps_exp_unique_ODE) (simp add: fps_mult_nth fps_exp_def)
  3747   then show ?thesis ..
  3764   then show ?thesis ..
  3748 qed
  3765 qed
  3749 
  3766 
  3750 lemma E_nth[simp]: "E a $ n = a^n / of_nat (fact n)"
  3767 lemma fps_exp_nth[simp]: "fps_exp a $ n = a^n / of_nat (fact n)"
  3751   by (simp add: E_def)
  3768   by (simp add: fps_exp_def)
  3752 
  3769 
  3753 lemma E0[simp]: "E (0::'a::field) = 1"
  3770 lemma fps_exp_0[simp]: "fps_exp (0::'a::field) = 1"
  3754   by (simp add: fps_eq_iff power_0_left)
  3771   by (simp add: fps_eq_iff power_0_left)
  3755 
  3772 
  3756 lemma E_neg: "E (- a) = inverse (E (a::'a::field_char_0))"
  3773 lemma fps_exp_neg: "fps_exp (- a) = inverse (fps_exp (a::'a::field_char_0))"
  3757 proof -
  3774 proof -
  3758   from E_add_mult[of a "- a"] have th0: "E a * E (- a) = 1" by simp
  3775   from fps_exp_add_mult[of a "- a"] have th0: "fps_exp a * fps_exp (- a) = 1" by simp
  3759   from fps_inverse_unique[OF th0] show ?thesis by simp
  3776   from fps_inverse_unique[OF th0] show ?thesis by simp
  3760 qed
  3777 qed
  3761 
  3778 
  3762 lemma E_nth_deriv[simp]: "fps_nth_deriv n (E (a::'a::field_char_0)) = (fps_const a)^n * (E a)"
  3779 lemma fps_exp_nth_deriv[simp]: 
       
  3780   "fps_nth_deriv n (fps_exp (a::'a::field_char_0)) = (fps_const a)^n * (fps_exp a)"
  3763   by (induct n) auto
  3781   by (induct n) auto
  3764 
  3782 
  3765 lemma X_compose_E[simp]: "X oo E (a::'a::field) = E a - 1"
  3783 lemma X_compose_fps_exp[simp]: "X oo fps_exp (a::'a::field) = fps_exp a - 1"
  3766   by (simp add: fps_eq_iff X_fps_compose)
  3784   by (simp add: fps_eq_iff X_fps_compose)
  3767 
  3785 
  3768 lemma LE_compose:
  3786 lemma fps_inv_fps_exp_compose:
  3769   assumes a: "a \<noteq> 0"
  3787   assumes a: "a \<noteq> 0"
  3770   shows "fps_inv (E a - 1) oo (E a - 1) = X"
  3788   shows "fps_inv (fps_exp a - 1) oo (fps_exp a - 1) = X"
  3771     and "(E a - 1) oo fps_inv (E a - 1) = X"
  3789     and "(fps_exp a - 1) oo fps_inv (fps_exp a - 1) = X"
  3772 proof -
  3790 proof -
  3773   let ?b = "E a - 1"
  3791   let ?b = "fps_exp a - 1"
  3774   have b0: "?b $ 0 = 0"
  3792   have b0: "?b $ 0 = 0"
  3775     by simp
  3793     by simp
  3776   have b1: "?b $ 1 \<noteq> 0"
  3794   have b1: "?b $ 1 \<noteq> 0"
  3777     by (simp add: a)
  3795     by (simp add: a)
  3778   from fps_inv[OF b0 b1] show "fps_inv (E a - 1) oo (E a - 1) = X" .
  3796   from fps_inv[OF b0 b1] show "fps_inv (fps_exp a - 1) oo (fps_exp a - 1) = X" .
  3779   from fps_inv_right[OF b0 b1] show "(E a - 1) oo fps_inv (E a - 1) = X" .
  3797   from fps_inv_right[OF b0 b1] show "(fps_exp a - 1) oo fps_inv (fps_exp a - 1) = X" .
  3780 qed
  3798 qed
  3781 
  3799 
  3782 lemma E_power_mult: "(E (c::'a::field_char_0))^n = E (of_nat n * c)"
  3800 lemma fps_exp_power_mult: "(fps_exp (c::'a::field_char_0))^n = fps_exp (of_nat n * c)"
  3783   by (induct n) (auto simp add: field_simps E_add_mult)
  3801   by (induct n) (auto simp add: field_simps fps_exp_add_mult)
  3784 
  3802 
  3785 lemma radical_E:
  3803 lemma radical_fps_exp:
  3786   assumes r: "r (Suc k) 1 = 1"
  3804   assumes r: "r (Suc k) 1 = 1"
  3787   shows "fps_radical r (Suc k) (E (c::'a::field_char_0)) = E (c / of_nat (Suc k))"
  3805   shows "fps_radical r (Suc k) (fps_exp (c::'a::field_char_0)) = fps_exp (c / of_nat (Suc k))"
  3788 proof -
  3806 proof -
  3789   let ?ck = "(c / of_nat (Suc k))"
  3807   let ?ck = "(c / of_nat (Suc k))"
  3790   let ?r = "fps_radical r (Suc k)"
  3808   let ?r = "fps_radical r (Suc k)"
  3791   have eq0[simp]: "?ck * of_nat (Suc k) = c" "of_nat (Suc k) * ?ck = c"
  3809   have eq0[simp]: "?ck * of_nat (Suc k) = c" "of_nat (Suc k) * ?ck = c"
  3792     by (simp_all del: of_nat_Suc)
  3810     by (simp_all del: of_nat_Suc)
  3793   have th0: "E ?ck ^ (Suc k) = E c" unfolding E_power_mult eq0 ..
  3811   have th0: "fps_exp ?ck ^ (Suc k) = fps_exp c" unfolding fps_exp_power_mult eq0 ..
  3794   have th: "r (Suc k) (E c $0) ^ Suc k = E c $ 0"
  3812   have th: "r (Suc k) (fps_exp c $0) ^ Suc k = fps_exp c $ 0"
  3795     "r (Suc k) (E c $ 0) = E ?ck $ 0" "E c $ 0 \<noteq> 0" using r by simp_all
  3813     "r (Suc k) (fps_exp c $ 0) = fps_exp ?ck $ 0" "fps_exp c $ 0 \<noteq> 0" using r by simp_all
  3796   from th0 radical_unique[where r=r and k=k, OF th] show ?thesis
  3814   from th0 radical_unique[where r=r and k=k, OF th] show ?thesis
  3797     by auto
  3815     by auto
  3798 qed
  3816 qed
  3799 
  3817 
  3800 lemma Ec_E1_eq: "E (1::'a::field_char_0) oo (fps_const c * X) = E c"
  3818 lemma fps_exp_compose_linear [simp]: 
  3801   apply (auto simp add: fps_eq_iff E_def fps_compose_def power_mult_distrib)
  3819   "fps_exp (d::'a::field_char_0) oo (fps_const c * X) = fps_exp (c * d)"
  3802   apply (simp add: cond_value_iff cond_application_beta sum.delta' cong del: if_weak_cong)
  3820   by (simp add: fps_compose_linear fps_exp_def fps_eq_iff power_mult_distrib)
  3803   done
  3821   
       
  3822 lemma fps_fps_exp_compose_minus [simp]: 
       
  3823   "fps_compose (fps_exp c) (-X) = fps_exp (-c :: 'a :: field_char_0)"
       
  3824   using fps_exp_compose_linear[of c "-1 :: 'a"] 
       
  3825   unfolding fps_const_neg [symmetric] fps_const_1_eq_1 by simp
       
  3826 
       
  3827 lemma fps_exp_eq_iff [simp]: "fps_exp c = fps_exp d \<longleftrightarrow> c = (d :: 'a :: field_char_0)"
       
  3828 proof
       
  3829   assume "fps_exp c = fps_exp d"
       
  3830   from arg_cong[of _ _ "\<lambda>F. F $ 1", OF this] show "c = d" by simp
       
  3831 qed simp_all
       
  3832 
       
  3833 lemma fps_exp_eq_fps_const_iff [simp]: 
       
  3834   "fps_exp (c :: 'a :: field_char_0) = fps_const c' \<longleftrightarrow> c = 0 \<and> c' = 1"
       
  3835 proof
       
  3836   assume "c = 0 \<and> c' = 1"
       
  3837   thus "fps_exp c = fps_const c'" by (auto simp: fps_eq_iff)
       
  3838 next
       
  3839   assume "fps_exp c = fps_const c'"
       
  3840   from arg_cong[of _ _ "\<lambda>F. F $ 1", OF this] arg_cong[of _ _ "\<lambda>F. F $ 0", OF this] 
       
  3841     show "c = 0 \<and> c' = 1" by simp_all
       
  3842 qed
       
  3843 
       
  3844 lemma fps_exp_neq_0 [simp]: "\<not>fps_exp (c :: 'a :: field_char_0) = 0"
       
  3845   unfolding fps_const_0_eq_0 [symmetric] fps_exp_eq_fps_const_iff by simp  
       
  3846 
       
  3847 lemma fps_exp_eq_1_iff [simp]: "fps_exp (c :: 'a :: field_char_0) = 1 \<longleftrightarrow> c = 0"
       
  3848   unfolding fps_const_1_eq_1 [symmetric] fps_exp_eq_fps_const_iff by simp
       
  3849     
       
  3850 lemma fps_exp_neq_numeral_iff [simp]: 
       
  3851   "fps_exp (c :: 'a :: field_char_0) = numeral n \<longleftrightarrow> c = 0 \<and> n = Num.One"
       
  3852   unfolding numeral_fps_const fps_exp_eq_fps_const_iff by simp
  3804 
  3853 
  3805 
  3854 
  3806 subsubsection \<open>Logarithmic series\<close>
  3855 subsubsection \<open>Logarithmic series\<close>
  3807 
  3856 
  3808 lemma Abs_fps_if_0:
  3857 lemma Abs_fps_if_0:
  3809   "Abs_fps (\<lambda>n. if n = 0 then (v::'a::ring_1) else f n) =
  3858   "Abs_fps (\<lambda>n. if n = 0 then (v::'a::ring_1) else f n) =
  3810     fps_const v + X * Abs_fps (\<lambda>n. f (Suc n))"
  3859     fps_const v + X * Abs_fps (\<lambda>n. f (Suc n))"
  3811   by (auto simp add: fps_eq_iff)
  3860   by (auto simp add: fps_eq_iff)
  3812 
  3861 
  3813 definition L :: "'a::field_char_0 \<Rightarrow> 'a fps"
  3862 definition fps_ln :: "'a::field_char_0 \<Rightarrow> 'a fps"
  3814   where "L c = fps_const (1/c) * Abs_fps (\<lambda>n. if n = 0 then 0 else (- 1) ^ (n - 1) / of_nat n)"
  3863   where "fps_ln c = fps_const (1/c) * Abs_fps (\<lambda>n. if n = 0 then 0 else (- 1) ^ (n - 1) / of_nat n)"
  3815 
  3864 
  3816 lemma fps_deriv_L: "fps_deriv (L c) = fps_const (1/c) * inverse (1 + X)"
  3865 lemma fps_ln_deriv: "fps_deriv (fps_ln c) = fps_const (1/c) * inverse (1 + X)"
  3817   unfolding fps_inverse_X_plus1
  3866   unfolding fps_inverse_X_plus1
  3818   by (simp add: L_def fps_eq_iff del: of_nat_Suc)
  3867   by (simp add: fps_ln_def fps_eq_iff del: of_nat_Suc)
  3819 
  3868 
  3820 lemma L_nth: "L c $ n = (if n = 0 then 0 else 1/c * ((- 1) ^ (n - 1) / of_nat n))"
  3869 lemma fps_ln_nth: "fps_ln c $ n = (if n = 0 then 0 else 1/c * ((- 1) ^ (n - 1) / of_nat n))"
  3821   by (simp add: L_def field_simps)
  3870   by (simp add: fps_ln_def field_simps)
  3822 
  3871 
  3823 lemma L_0[simp]: "L c $ 0 = 0" by (simp add: L_def)
  3872 lemma fps_ln_0 [simp]: "fps_ln c $ 0 = 0" by (simp add: fps_ln_def)
  3824 
  3873 
  3825 lemma L_E_inv:
  3874 lemma fps_ln_fps_exp_inv:
  3826   fixes a :: "'a::field_char_0"
  3875   fixes a :: "'a::field_char_0"
  3827   assumes a: "a \<noteq> 0"
  3876   assumes a: "a \<noteq> 0"
  3828   shows "L a = fps_inv (E a - 1)"  (is "?l = ?r")
  3877   shows "fps_ln a = fps_inv (fps_exp a - 1)"  (is "?l = ?r")
  3829 proof -
  3878 proof -
  3830   let ?b = "E a - 1"
  3879   let ?b = "fps_exp a - 1"
  3831   have b0: "?b $ 0 = 0" by simp
  3880   have b0: "?b $ 0 = 0" by simp
  3832   have b1: "?b $ 1 \<noteq> 0" by (simp add: a)
  3881   have b1: "?b $ 1 \<noteq> 0" by (simp add: a)
  3833   have "fps_deriv (E a - 1) oo fps_inv (E a - 1) =
  3882   have "fps_deriv (fps_exp a - 1) oo fps_inv (fps_exp a - 1) =
  3834     (fps_const a * (E a - 1) + fps_const a) oo fps_inv (E a - 1)"
  3883     (fps_const a * (fps_exp a - 1) + fps_const a) oo fps_inv (fps_exp a - 1)"
  3835     by (simp add: field_simps)
  3884     by (simp add: field_simps)
  3836   also have "\<dots> = fps_const a * (X + 1)"
  3885   also have "\<dots> = fps_const a * (X + 1)"
  3837     apply (simp add: fps_compose_add_distrib fps_const_mult_apply_left[symmetric] fps_inv_right[OF b0 b1])
  3886     apply (simp add: fps_compose_add_distrib fps_const_mult_apply_left[symmetric] fps_inv_right[OF b0 b1])
  3838     apply (simp add: field_simps)
  3887     apply (simp add: field_simps)
  3839     done
  3888     done
  3840   finally have eq: "fps_deriv (E a - 1) oo fps_inv (E a - 1) = fps_const a * (X + 1)" .
  3889   finally have eq: "fps_deriv (fps_exp a - 1) oo fps_inv (fps_exp a - 1) = fps_const a * (X + 1)" .
  3841   from fps_inv_deriv[OF b0 b1, unfolded eq]
  3890   from fps_inv_deriv[OF b0 b1, unfolded eq]
  3842   have "fps_deriv (fps_inv ?b) = fps_const (inverse a) / (X + 1)"
  3891   have "fps_deriv (fps_inv ?b) = fps_const (inverse a) / (X + 1)"
  3843     using a
  3892     using a by (simp add: fps_const_inverse eq fps_divide_def fps_inverse_mult)
  3844     by (simp add: fps_const_inverse eq fps_divide_def fps_inverse_mult)
       
  3845   then have "fps_deriv ?l = fps_deriv ?r"
  3893   then have "fps_deriv ?l = fps_deriv ?r"
  3846     by (simp add: fps_deriv_L add.commute fps_divide_def divide_inverse)
  3894     by (simp add: fps_ln_deriv add.commute fps_divide_def divide_inverse)
  3847   then show ?thesis unfolding fps_deriv_eq_iff
  3895   then show ?thesis unfolding fps_deriv_eq_iff
  3848     by (simp add: L_nth fps_inv_def)
  3896     by (simp add: fps_ln_nth fps_inv_def)
  3849 qed
  3897 qed
  3850 
  3898 
  3851 lemma L_mult_add:
  3899 lemma fps_ln_mult_add:
  3852   assumes c0: "c\<noteq>0"
  3900   assumes c0: "c\<noteq>0"
  3853     and d0: "d\<noteq>0"
  3901     and d0: "d\<noteq>0"
  3854   shows "L c + L d = fps_const (c+d) * L (c*d)"
  3902   shows "fps_ln c + fps_ln d = fps_const (c+d) * fps_ln (c*d)"
  3855   (is "?r = ?l")
  3903   (is "?r = ?l")
  3856 proof-
  3904 proof-
  3857   from c0 d0 have eq: "1/c + 1/d = (c+d)/(c*d)" by (simp add: field_simps)
  3905   from c0 d0 have eq: "1/c + 1/d = (c+d)/(c*d)" by (simp add: field_simps)
  3858   have "fps_deriv ?r = fps_const (1/c + 1/d) * inverse (1 + X)"
  3906   have "fps_deriv ?r = fps_const (1/c + 1/d) * inverse (1 + X)"
  3859     by (simp add: fps_deriv_L fps_const_add[symmetric] algebra_simps del: fps_const_add)
  3907     by (simp add: fps_ln_deriv fps_const_add[symmetric] algebra_simps del: fps_const_add)
  3860   also have "\<dots> = fps_deriv ?l"
  3908   also have "\<dots> = fps_deriv ?l"
  3861     apply (simp add: fps_deriv_L)
  3909     apply (simp add: fps_ln_deriv)
  3862     apply (simp add: fps_eq_iff eq)
  3910     apply (simp add: fps_eq_iff eq)
  3863     done
  3911     done
  3864   finally show ?thesis
  3912   finally show ?thesis
  3865     unfolding fps_deriv_eq_iff by simp
  3913     unfolding fps_deriv_eq_iff by simp
       
  3914 qed
       
  3915 
       
  3916 lemma X_dvd_fps_ln [simp]: "X dvd fps_ln c"
       
  3917 proof -
       
  3918   have "fps_ln c = X * Abs_fps (\<lambda>n. (-1) ^ n / (of_nat (Suc n) * c))"
       
  3919     by (intro fps_ext) (auto simp: fps_ln_def of_nat_diff)
       
  3920   thus ?thesis by simp
  3866 qed
  3921 qed
  3867 
  3922 
  3868 
  3923 
  3869 subsubsection \<open>Binomial series\<close>
  3924 subsubsection \<open>Binomial series\<close>
  3870 
  3925 
  4456              del: fps_const_neg)
  4511              del: fps_const_neg)
  4457   also note fps_sin_cos_sum_of_squares
  4512   also note fps_sin_cos_sum_of_squares
  4458   finally show ?thesis by simp
  4513   finally show ?thesis by simp
  4459 qed
  4514 qed
  4460 
  4515 
  4461 text \<open>Connection to E c over the complex numbers --- Euler and de Moivre.\<close>
  4516 text \<open>Connection to @{const "fps_exp"} over the complex numbers --- Euler and de Moivre.\<close>
  4462 
  4517 
  4463 lemma Eii_sin_cos: "E (\<i> * c) = fps_cos c + fps_const \<i> * fps_sin c"
  4518 lemma fps_exp_ii_sin_cos: "fps_exp (\<i> * c) = fps_cos c + fps_const \<i> * fps_sin c"
  4464   (is "?l = ?r")
  4519   (is "?l = ?r")
  4465 proof -
  4520 proof -
  4466   have "?l $ n = ?r $ n" for n
  4521   have "?l $ n = ?r $ n" for n
  4467   proof (cases "even n")
  4522   proof (cases "even n")
  4468     case True
  4523     case True
  4478   qed
  4533   qed
  4479   then show ?thesis
  4534   then show ?thesis
  4480     by (simp add: fps_eq_iff)
  4535     by (simp add: fps_eq_iff)
  4481 qed
  4536 qed
  4482 
  4537 
  4483 lemma E_minus_ii_sin_cos: "E (- (\<i> * c)) = fps_cos c - fps_const \<i> * fps_sin c"
  4538 lemma fps_exp_minus_ii_sin_cos: "fps_exp (- (\<i> * c)) = fps_cos c - fps_const \<i> * fps_sin c"
  4484   unfolding minus_mult_right Eii_sin_cos by (simp add: fps_sin_even fps_cos_odd)
  4539   unfolding minus_mult_right fps_exp_ii_sin_cos by (simp add: fps_sin_even fps_cos_odd)
  4485 
  4540 
  4486 lemma fps_const_minus: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d)"
  4541 lemma fps_const_minus: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d)"
  4487   by (fact fps_const_sub)
  4542   by (fact fps_const_sub)
  4488 
  4543 
  4489 lemma fps_of_int: "fps_const (of_int c) = of_int c"
  4544 lemma fps_of_int: "fps_const (of_int c) = of_int c"
  4490   by (induction c) (simp_all add: fps_const_minus [symmetric] fps_of_nat fps_const_neg [symmetric] 
  4545   by (induction c) (simp_all add: fps_const_minus [symmetric] fps_of_nat fps_const_neg [symmetric] 
  4491                              del: fps_const_minus fps_const_neg)
  4546                              del: fps_const_minus fps_const_neg)
  4492 
  4547 
       
  4548 lemma fps_deriv_of_int [simp]: "fps_deriv (of_int n) = 0"
       
  4549   by (simp add: fps_of_int [symmetric])
       
  4550 
  4493 lemma fps_numeral_fps_const: "numeral i = fps_const (numeral i :: 'a::comm_ring_1)"
  4551 lemma fps_numeral_fps_const: "numeral i = fps_const (numeral i :: 'a::comm_ring_1)"
  4494   by (fact numeral_fps_const) (* FIXME: duplicate *)
  4552   by (fact numeral_fps_const) (* FIXME: duplicate *)
  4495 
  4553 
  4496 lemma fps_cos_Eii: "fps_cos c = (E (\<i> * c) + E (- \<i> * c)) / fps_const 2"
  4554 lemma fps_cos_fps_exp_ii: "fps_cos c = (fps_exp (\<i> * c) + fps_exp (- \<i> * c)) / fps_const 2"
  4497 proof -
  4555 proof -
  4498   have th: "fps_cos c + fps_cos c = fps_cos c * fps_const 2"
  4556   have th: "fps_cos c + fps_cos c = fps_cos c * fps_const 2"
  4499     by (simp add: numeral_fps_const)
  4557     by (simp add: numeral_fps_const)
  4500   show ?thesis
  4558   show ?thesis
  4501     unfolding Eii_sin_cos minus_mult_commute
  4559     unfolding fps_exp_ii_sin_cos minus_mult_commute
  4502     by (simp add: fps_sin_even fps_cos_odd numeral_fps_const fps_divide_unit fps_const_inverse th)
  4560     by (simp add: fps_sin_even fps_cos_odd numeral_fps_const fps_divide_unit fps_const_inverse th)
  4503 qed
  4561 qed
  4504 
  4562 
  4505 lemma fps_sin_Eii: "fps_sin c = (E (\<i> * c) - E (- \<i> * c)) / fps_const (2*\<i>)"
  4563 lemma fps_sin_fps_exp_ii: "fps_sin c = (fps_exp (\<i> * c) - fps_exp (- \<i> * c)) / fps_const (2*\<i>)"
  4506 proof -
  4564 proof -
  4507   have th: "fps_const \<i> * fps_sin c + fps_const \<i> * fps_sin c = fps_sin c * fps_const (2 * \<i>)"
  4565   have th: "fps_const \<i> * fps_sin c + fps_const \<i> * fps_sin c = fps_sin c * fps_const (2 * \<i>)"
  4508     by (simp add: fps_eq_iff numeral_fps_const)
  4566     by (simp add: fps_eq_iff numeral_fps_const)
  4509   show ?thesis
  4567   show ?thesis
  4510     unfolding Eii_sin_cos minus_mult_commute
  4568     unfolding fps_exp_ii_sin_cos minus_mult_commute
  4511     by (simp add: fps_sin_even fps_cos_odd fps_divide_unit fps_const_inverse th)
  4569     by (simp add: fps_sin_even fps_cos_odd fps_divide_unit fps_const_inverse th)
  4512 qed
  4570 qed
  4513 
  4571 
  4514 lemma fps_tan_Eii:
  4572 lemma fps_tan_fps_exp_ii:
  4515   "fps_tan c = (E (\<i> * c) - E (- \<i> * c)) / (fps_const \<i> * (E (\<i> * c) + E (- \<i> * c)))"
  4573   "fps_tan c = (fps_exp (\<i> * c) - fps_exp (- \<i> * c)) / 
  4516   unfolding fps_tan_def fps_sin_Eii fps_cos_Eii mult_minus_left E_neg
  4574       (fps_const \<i> * (fps_exp (\<i> * c) + fps_exp (- \<i> * c)))"
       
  4575   unfolding fps_tan_def fps_sin_fps_exp_ii fps_cos_fps_exp_ii mult_minus_left fps_exp_neg
  4517   apply (simp add: fps_divide_unit fps_inverse_mult fps_const_mult[symmetric] fps_const_inverse del: fps_const_mult)
  4576   apply (simp add: fps_divide_unit fps_inverse_mult fps_const_mult[symmetric] fps_const_inverse del: fps_const_mult)
  4518   apply simp
  4577   apply simp
  4519   done
  4578   done
  4520 
  4579 
  4521 lemma fps_demoivre:
  4580 lemma fps_demoivre:
  4522   "(fps_cos a + fps_const \<i> * fps_sin a)^n =
  4581   "(fps_cos a + fps_const \<i> * fps_sin a)^n =
  4523     fps_cos (of_nat n * a) + fps_const \<i> * fps_sin (of_nat n * a)"
  4582     fps_cos (of_nat n * a) + fps_const \<i> * fps_sin (of_nat n * a)"
  4524   unfolding Eii_sin_cos[symmetric] E_power_mult
  4583   unfolding fps_exp_ii_sin_cos[symmetric] fps_exp_power_mult
  4525   by (simp add: ac_simps)
  4584   by (simp add: ac_simps)
  4526 
  4585 
  4527 
  4586 
  4528 subsection \<open>Hypergeometric series\<close>
  4587 subsection \<open>Hypergeometric series\<close>
  4529 
  4588 
  4530 (* TODO: Rename this *)
  4589 definition "fps_hypergeo as bs (c::'a::{field_char_0,field}) =
  4531 definition "F as bs (c::'a::{field_char_0,field}) =
       
  4532   Abs_fps (\<lambda>n. (foldl (\<lambda>r a. r* pochhammer a n) 1 as * c^n) /
  4590   Abs_fps (\<lambda>n. (foldl (\<lambda>r a. r* pochhammer a n) 1 as * c^n) /
  4533     (foldl (\<lambda>r b. r * pochhammer b n) 1 bs * of_nat (fact n)))"
  4591     (foldl (\<lambda>r b. r * pochhammer b n) 1 bs * of_nat (fact n)))"
  4534 
  4592 
  4535 lemma F_nth[simp]: "F as bs c $ n =
  4593 lemma fps_hypergeo_nth[simp]: "fps_hypergeo as bs c $ n =
  4536   (foldl (\<lambda>r a. r* pochhammer a n) 1 as * c^n) /
  4594   (foldl (\<lambda>r a. r* pochhammer a n) 1 as * c^n) /
  4537     (foldl (\<lambda>r b. r * pochhammer b n) 1 bs * of_nat (fact n))"
  4595     (foldl (\<lambda>r b. r * pochhammer b n) 1 bs * of_nat (fact n))"
  4538   by (simp add: F_def)
  4596   by (simp add: fps_hypergeo_def)
  4539 
  4597 
  4540 lemma foldl_mult_start:
  4598 lemma foldl_mult_start:
  4541   fixes v :: "'a::comm_ring_1"
  4599   fixes v :: "'a::comm_ring_1"
  4542   shows "foldl (\<lambda>r x. r * f x) v as * x = foldl (\<lambda>r x. r * f x) (v * x) as "
  4600   shows "foldl (\<lambda>r x. r * f x) v as * x = foldl (\<lambda>r x. r * f x) (v * x) as "
  4543   by (induct as arbitrary: x v) (auto simp add: algebra_simps)
  4601   by (induct as arbitrary: x v) (auto simp add: algebra_simps)
  4545 lemma foldr_mult_foldl:
  4603 lemma foldr_mult_foldl:
  4546   fixes v :: "'a::comm_ring_1"
  4604   fixes v :: "'a::comm_ring_1"
  4547   shows "foldr (\<lambda>x r. r * f x) as v = foldl (\<lambda>r x. r * f x) v as"
  4605   shows "foldr (\<lambda>x r. r * f x) as v = foldl (\<lambda>r x. r * f x) v as"
  4548   by (induct as arbitrary: v) (auto simp add: foldl_mult_start)
  4606   by (induct as arbitrary: v) (auto simp add: foldl_mult_start)
  4549 
  4607 
  4550 lemma F_nth_alt:
  4608 lemma fps_hypergeo_nth_alt:
  4551   "F as bs c $ n = foldr (\<lambda>a r. r * pochhammer a n) as (c ^ n) /
  4609   "fps_hypergeo as bs c $ n = foldr (\<lambda>a r. r * pochhammer a n) as (c ^ n) /
  4552     foldr (\<lambda>b r. r * pochhammer b n) bs (of_nat (fact n))"
  4610     foldr (\<lambda>b r. r * pochhammer b n) bs (of_nat (fact n))"
  4553   by (simp add: foldl_mult_start foldr_mult_foldl)
  4611   by (simp add: foldl_mult_start foldr_mult_foldl)
  4554 
  4612 
  4555 lemma F_E[simp]: "F [] [] c = E c"
  4613 lemma fps_hypergeo_fps_exp[simp]: "fps_hypergeo [] [] c = fps_exp c"
  4556   by (simp add: fps_eq_iff)
  4614   by (simp add: fps_eq_iff)
  4557 
  4615 
  4558 lemma F_1_0[simp]: "F [1] [] c = 1/(1 - fps_const c * X)"
  4616 lemma fps_hypergeo_1_0[simp]: "fps_hypergeo [1] [] c = 1/(1 - fps_const c * X)"
  4559 proof -
  4617 proof -
  4560   let ?a = "(Abs_fps (\<lambda>n. 1)) oo (fps_const c * X)"
  4618   let ?a = "(Abs_fps (\<lambda>n. 1)) oo (fps_const c * X)"
  4561   have th0: "(fps_const c * X) $ 0 = 0" by simp
  4619   have th0: "(fps_const c * X) $ 0 = 0" by simp
  4562   show ?thesis unfolding gp[OF th0, symmetric]
  4620   show ?thesis unfolding gp[OF th0, symmetric]
  4563     by (auto simp add: fps_eq_iff pochhammer_fact[symmetric]
  4621     by (auto simp add: fps_eq_iff pochhammer_fact[symmetric]
  4564       fps_compose_nth power_mult_distrib cond_value_iff sum.delta' cong del: if_weak_cong)
  4622       fps_compose_nth power_mult_distrib cond_value_iff sum.delta' cong del: if_weak_cong)
  4565 qed
  4623 qed
  4566 
  4624 
  4567 lemma F_B[simp]: "F [-a] [] (- 1) = fps_binomial a"
  4625 lemma fps_hypergeo_B[simp]: "fps_hypergeo [-a] [] (- 1) = fps_binomial a"
  4568   by (simp add: fps_eq_iff gbinomial_pochhammer algebra_simps)
  4626   by (simp add: fps_eq_iff gbinomial_pochhammer algebra_simps)
  4569 
  4627 
  4570 lemma F_0[simp]: "F as bs c $ 0 = 1"
  4628 lemma fps_hypergeo_0[simp]: "fps_hypergeo as bs c $ 0 = 1"
  4571   apply simp
  4629   apply simp
  4572   apply (subgoal_tac "\<forall>as. foldl (\<lambda>(r::'a) (a::'a). r) 1 as = 1")
  4630   apply (subgoal_tac "\<forall>as. foldl (\<lambda>(r::'a) (a::'a). r) 1 as = 1")
  4573   apply auto
  4631   apply auto
  4574   apply (induct_tac as)
  4632   apply (induct_tac as)
  4575   apply auto
  4633   apply auto
  4579   "foldl (\<lambda>(r::'b::comm_ring_1) (x::'a::comm_ring_1). r * f x) v as * foldl (\<lambda>r x. r * g x) w as =
  4637   "foldl (\<lambda>(r::'b::comm_ring_1) (x::'a::comm_ring_1). r * f x) v as * foldl (\<lambda>r x. r * g x) w as =
  4580     foldl (\<lambda>r x. r * f x * g x) (v * w) as"
  4638     foldl (\<lambda>r x. r * f x * g x) (v * w) as"
  4581   by (induct as arbitrary: v w) (auto simp add: algebra_simps)
  4639   by (induct as arbitrary: v w) (auto simp add: algebra_simps)
  4582 
  4640 
  4583 
  4641 
  4584 lemma F_rec:
  4642 lemma fps_hypergeo_rec:
  4585   "F as bs c $ Suc n = ((foldl (\<lambda>r a. r* (a + of_nat n)) c as) /
  4643   "fps_hypergeo as bs c $ Suc n = ((foldl (\<lambda>r a. r* (a + of_nat n)) c as) /
  4586     (foldl (\<lambda>r b. r * (b + of_nat n)) (of_nat (Suc n)) bs )) * F as bs c $ n"
  4644     (foldl (\<lambda>r b. r * (b + of_nat n)) (of_nat (Suc n)) bs )) * fps_hypergeo as bs c $ n"
  4587   apply (simp del: of_nat_Suc of_nat_add fact_Suc)
  4645   apply (simp del: of_nat_Suc of_nat_add fact_Suc)
  4588   apply (simp add: foldl_mult_start del: fact_Suc of_nat_Suc)
  4646   apply (simp add: foldl_mult_start del: fact_Suc of_nat_Suc)
  4589   unfolding foldl_prod_prod[unfolded foldl_mult_start] pochhammer_Suc
  4647   unfolding foldl_prod_prod[unfolded foldl_mult_start] pochhammer_Suc
  4590   apply (simp add: algebra_simps)
  4648   apply (simp add: algebra_simps)
  4591   done
  4649   done
  4610   by (simp add: fun_eq_iff fps_eq_iff)
  4668   by (simp add: fun_eq_iff fps_eq_iff)
  4611 
  4669 
  4612 lemma XDp_fps_integral [simp]: "XDp 0 (fps_integral a c) = X * a"
  4670 lemma XDp_fps_integral [simp]: "XDp 0 (fps_integral a c) = X * a"
  4613   by (simp add: fps_eq_iff fps_integral_def)
  4671   by (simp add: fps_eq_iff fps_integral_def)
  4614 
  4672 
  4615 lemma F_minus_nat:
  4673 lemma fps_hypergeo_minus_nat:
  4616   "F [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0,field}) $ k =
  4674   "fps_hypergeo [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0,field}) $ k =
  4617     (if k \<le> n then
  4675     (if k \<le> n then
  4618       pochhammer (- of_nat n) k * c ^ k / (pochhammer (- of_nat (n + m)) k * of_nat (fact k))
  4676       pochhammer (- of_nat n) k * c ^ k / (pochhammer (- of_nat (n + m)) k * of_nat (fact k))
  4619      else 0)"
  4677      else 0)"
  4620   "F [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0,field}) $ k =
  4678   "fps_hypergeo [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0,field}) $ k =
  4621     (if k \<le> m then
  4679     (if k \<le> m then
  4622       pochhammer (- of_nat m) k * c ^ k / (pochhammer (- of_nat (m + n)) k * of_nat (fact k))
  4680       pochhammer (- of_nat m) k * c ^ k / (pochhammer (- of_nat (m + n)) k * of_nat (fact k))
  4623      else 0)"
  4681      else 0)"
  4624   by (auto simp add: pochhammer_eq_0_iff)
  4682   by (auto simp add: pochhammer_eq_0_iff)
  4625 
  4683