2800 from iffD1[OF fps_binomial_ODE_unique[of "inverse (1 + X)" "- 1"] th'] eq |
2799 from iffD1[OF fps_binomial_ODE_unique[of "inverse (1 + X)" "- 1"] th'] eq |
2801 show ?thesis by (simp add: fps_inverse_def) |
2800 show ?thesis by (simp add: fps_inverse_def) |
2802 qed |
2801 qed |
2803 |
2802 |
2804 text{* Vandermonde's Identity as a consequence *} |
2803 text{* Vandermonde's Identity as a consequence *} |
2805 lemma gbinomial_Vandermond: "setsum (\<lambda>k. (a gchoose k) * (b gchoose (n - k))) {0..n} = (a + b) gchoose n" |
2804 lemma gbinomial_Vandermonde: "setsum (\<lambda>k. (a gchoose k) * (b gchoose (n - k))) {0..n} = (a + b) gchoose n" |
2806 proof- |
2805 proof- |
2807 let ?ba = "fps_binomial a" |
2806 let ?ba = "fps_binomial a" |
2808 let ?bb = "fps_binomial b" |
2807 let ?bb = "fps_binomial b" |
2809 let ?bab = "fps_binomial (a + b)" |
2808 let ?bab = "fps_binomial (a + b)" |
2810 from fps_binomial_add_mult[of a b] have "?bab $ n = (?ba * ?bb)$n" by simp |
2809 from fps_binomial_add_mult[of a b] have "?bab $ n = (?ba * ?bb)$n" by simp |
2811 then show ?thesis by (simp add: fps_mult_nth) |
2810 then show ?thesis by (simp add: fps_mult_nth) |
2812 qed |
2811 qed |
2813 |
2812 |
2814 lemma binomial_Vandermond: "setsum (\<lambda>k. (a choose k) * (b choose (n - k))) {0..n} = (a + b) choose n" |
2813 lemma binomial_Vandermonde: "setsum (\<lambda>k. (a choose k) * (b choose (n - k))) {0..n} = (a + b) choose n" |
2815 using gbinomial_Vandermond[of "(of_nat a)" "of_nat b" n] |
2814 using gbinomial_Vandermonde[of "(of_nat a)" "of_nat b" n] |
2816 |
2815 |
2817 apply (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric] of_nat_add[symmetric]) |
2816 apply (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric] of_nat_add[symmetric]) |
2818 by simp |
2817 by simp |
2819 |
|
2820 lemma binomial_symmetric: assumes kn: "k \<le> n" |
|
2821 shows "n choose k = n choose (n - k)" |
|
2822 proof- |
|
2823 from kn have kn': "n - k \<le> n" by arith |
|
2824 from binomial_fact_lemma[OF kn] binomial_fact_lemma[OF kn'] |
|
2825 have "fact k * fact (n - k) * (n choose k) = fact (n - k) * fact (n - (n - k)) * (n choose (n - k))" by simp |
|
2826 then show ?thesis using kn by simp |
|
2827 qed |
|
2828 |
2818 |
2829 lemma binomial_Vandermond_same: "setsum (\<lambda>k. (n choose k)^2) {0..n} = (2*n) choose n" |
2819 lemma binomial_Vandermonde_same: "setsum (\<lambda>k. (n choose k)^2) {0..n} = (2*n) choose n" |
2830 using binomial_Vandermond[of n n n,symmetric] |
2820 using binomial_Vandermonde[of n n n,symmetric] |
2831 unfolding nat_mult_2 apply (simp add: power2_eq_square) |
2821 unfolding nat_mult_2 apply (simp add: power2_eq_square) |
2832 apply (rule setsum_cong2) |
2822 apply (rule setsum_cong2) |
2833 by (auto intro: binomial_symmetric) |
2823 by (auto intro: binomial_symmetric) |
2834 |
2824 |
|
2825 lemma Vandermonde_pochhammer_lemma: |
|
2826 fixes a :: "'a::field_char_0" |
|
2827 assumes b: "\<forall> j\<in>{0 ..<n}. b \<noteq> of_nat j" |
|
2828 shows "setsum (%k. (pochhammer (- a) k * pochhammer (- (of_nat n)) k) / (of_nat (fact k) * pochhammer (b - of_nat n + 1) k)) {0..n} = pochhammer (- (a+ b)) n / pochhammer (- b) n" (is "?l = ?r") |
|
2829 proof- |
|
2830 let ?m1 = "%m. (- 1 :: 'a) ^ m" |
|
2831 let ?f = "%m. of_nat (fact m)" |
|
2832 let ?p = "%(x::'a). pochhammer (- x)" |
|
2833 from b have bn0: "?p b n \<noteq> 0" unfolding pochhammer_eq_0_iff by simp |
|
2834 {fix k assume kn: "k \<in> {0..n}" |
|
2835 {assume c:"pochhammer (b - of_nat n + 1) n = 0" |
|
2836 then obtain j where j: "j < n" "b - of_nat n + 1 = - of_nat j" |
|
2837 unfolding pochhammer_eq_0_iff by blast |
|
2838 from j have "b = of_nat n - of_nat j - of_nat 1" |
|
2839 by (simp add: algebra_simps) |
|
2840 then have "b = of_nat (n - j - 1)" |
|
2841 using j kn by (simp add: of_nat_diff) |
|
2842 with b have False using j by auto} |
|
2843 then have nz: "pochhammer (1 + b - of_nat n) n \<noteq> 0" |
|
2844 by (auto simp add: algebra_simps) |
|
2845 |
|
2846 from nz kn have nz': "pochhammer (1 + b - of_nat n) k \<noteq> 0" |
|
2847 by (simp add: pochhammer_neq_0_mono) |
|
2848 {assume k0: "k = 0 \<or> n =0" |
|
2849 then have "b gchoose (n - k) = (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)" |
|
2850 using kn |
|
2851 by (cases "k=0", simp_all add: gbinomial_pochhammer)} |
|
2852 moreover |
|
2853 {assume n0: "n \<noteq> 0" and k0: "k \<noteq> 0" |
|
2854 then obtain m where m: "n = Suc m" by (cases n, auto) |
|
2855 from k0 obtain h where h: "k = Suc h" by (cases k, auto) |
|
2856 {assume kn: "k = n" |
|
2857 then have "b gchoose (n - k) = (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)" |
|
2858 using kn pochhammer_minus'[where k=k and n=n and b=b] |
|
2859 apply (simp add: pochhammer_same) |
|
2860 using bn0 |
|
2861 by (simp add: field_simps power_add[symmetric])} |
|
2862 moreover |
|
2863 {assume nk: "k \<noteq> n" |
|
2864 have m1nk: "?m1 n = setprod (%i. - 1) {0..m}" |
|
2865 "?m1 k = setprod (%i. - 1) {0..h}" |
|
2866 by (simp_all add: setprod_constant m h) |
|
2867 from kn nk have kn': "k < n" by simp |
|
2868 have bnz0: "pochhammer (b - of_nat n + 1) k \<noteq> 0" |
|
2869 using bn0 kn |
|
2870 unfolding pochhammer_eq_0_iff |
|
2871 apply auto |
|
2872 apply (erule_tac x= "n - ka - 1" in allE) |
|
2873 by (auto simp add: algebra_simps of_nat_diff) |
|
2874 have eq1: "setprod (%k. (1::'a) + of_nat m - of_nat k) {0 .. h} = setprod of_nat {Suc (m - h) .. Suc m}" |
|
2875 apply (rule strong_setprod_reindex_cong[where f="%k. Suc m - k "]) |
|
2876 using kn' h m |
|
2877 apply (auto simp add: inj_on_def image_def) |
|
2878 apply (rule_tac x="Suc m - x" in bexI) |
|
2879 apply (simp_all add: of_nat_diff) |
|
2880 done |
|
2881 |
|
2882 have th1: "(?m1 k * ?p (of_nat n) k) / ?f n = 1 / of_nat(fact (n - k))" |
|
2883 unfolding m1nk |
|
2884 |
|
2885 unfolding m h pochhammer_Suc_setprod |
|
2886 apply (simp add: field_simps del: fact_Suc id_def) |
|
2887 unfolding fact_setprod id_def |
|
2888 unfolding of_nat_setprod |
|
2889 unfolding setprod_timesf[symmetric] |
|
2890 apply auto |
|
2891 unfolding eq1 |
|
2892 apply (subst setprod_Un_disjoint[symmetric]) |
|
2893 apply (auto) |
|
2894 apply (rule setprod_cong) |
|
2895 apply auto |
|
2896 done |
|
2897 have th20: "?m1 n * ?p b n = setprod (%i. b - of_nat i) {0..m}" |
|
2898 unfolding m1nk |
|
2899 unfolding m h pochhammer_Suc_setprod |
|
2900 unfolding setprod_timesf[symmetric] |
|
2901 apply (rule setprod_cong) |
|
2902 apply auto |
|
2903 done |
|
2904 have th21:"pochhammer (b - of_nat n + 1) k = setprod (%i. b - of_nat i) {n - k .. n - 1}" |
|
2905 unfolding h m |
|
2906 unfolding pochhammer_Suc_setprod |
|
2907 apply (rule strong_setprod_reindex_cong[where f="%k. n - 1 - k"]) |
|
2908 using kn |
|
2909 apply (auto simp add: inj_on_def m h image_def) |
|
2910 apply (rule_tac x= "m - x" in bexI) |
|
2911 by (auto simp add: of_nat_diff) |
|
2912 |
|
2913 have "?m1 n * ?p b n = pochhammer (b - of_nat n + 1) k * setprod (%i. b - of_nat i) {0.. n - k - 1}" |
|
2914 unfolding th20 th21 |
|
2915 unfolding h m |
|
2916 apply (subst setprod_Un_disjoint[symmetric]) |
|
2917 using kn' h m |
|
2918 apply auto |
|
2919 apply (rule setprod_cong) |
|
2920 apply auto |
|
2921 done |
|
2922 then have th2: "(?m1 n * ?p b n)/pochhammer (b - of_nat n + 1) k = setprod (%i. b - of_nat i) {0.. n - k - 1}" |
|
2923 using nz' by (simp add: field_simps) |
|
2924 have "(?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k) = ((?m1 k * ?p (of_nat n) k) / ?f n) * ((?m1 n * ?p b n)/pochhammer (b - of_nat n + 1) k)" |
|
2925 using bnz0 |
|
2926 by (simp add: field_simps) |
|
2927 also have "\<dots> = b gchoose (n - k)" |
|
2928 unfolding th1 th2 |
|
2929 using kn' by (simp add: gbinomial_def) |
|
2930 finally have "b gchoose (n - k) = (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)" by simp} |
|
2931 ultimately have "b gchoose (n - k) = (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)" |
|
2932 by (cases "k =n", auto)} |
|
2933 ultimately have "b gchoose (n - k) = (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)" "pochhammer (1 + b - of_nat n) k \<noteq> 0 " |
|
2934 using nz' |
|
2935 apply (cases "n=0", auto) |
|
2936 by (cases "k", auto)} |
|
2937 note th00 = this |
|
2938 have "?r = ((a + b) gchoose n) * (of_nat (fact n)/ (?m1 n * pochhammer (- b) n))" |
|
2939 unfolding gbinomial_pochhammer |
|
2940 using bn0 by (auto simp add: field_simps) |
|
2941 also have "\<dots> = ?l" |
|
2942 unfolding gbinomial_Vandermonde[symmetric] |
|
2943 apply (simp add: th00) |
|
2944 unfolding gbinomial_pochhammer |
|
2945 using bn0 apply (simp add: setsum_left_distrib setsum_right_distrib field_simps) |
|
2946 apply (rule setsum_cong2) |
|
2947 apply (drule th00(2)) |
|
2948 by (simp add: field_simps power_add[symmetric]) |
|
2949 finally show ?thesis by simp |
|
2950 qed |
|
2951 |
|
2952 |
|
2953 lemma Vandermonde_pochhammer: |
|
2954 fixes a :: "'a::field_char_0" |
|
2955 assumes c: "ALL i : {0..< n}. c \<noteq> - of_nat i" |
|
2956 shows "setsum (%k. (pochhammer a k * pochhammer (- (of_nat n)) k) / (of_nat (fact k) * pochhammer c k)) {0..n} = pochhammer (c - a) n / pochhammer c n" |
|
2957 proof- |
|
2958 let ?a = "- a" |
|
2959 let ?b = "c + of_nat n - 1" |
|
2960 have h: "\<forall> j \<in>{0..< n}. ?b \<noteq> of_nat j" using c |
|
2961 apply (auto simp add: algebra_simps of_nat_diff) |
|
2962 apply (erule_tac x= "n - j - 1" in ballE) |
|
2963 by (auto simp add: of_nat_diff algebra_simps) |
|
2964 have th0: "pochhammer (- (?a + ?b)) n = (- 1)^n * pochhammer (c - a) n" |
|
2965 unfolding pochhammer_minus[OF le_refl] |
|
2966 by (simp add: algebra_simps) |
|
2967 have th1: "pochhammer (- ?b) n = (- 1)^n * pochhammer c n" |
|
2968 unfolding pochhammer_minus[OF le_refl] |
|
2969 by simp |
|
2970 have nz: "pochhammer c n \<noteq> 0" using c |
|
2971 by (simp add: pochhammer_eq_0_iff) |
|
2972 from Vandermonde_pochhammer_lemma[where a = "?a" and b="?b" and n=n, OF h, unfolded th0 th1] |
|
2973 show ?thesis using nz by (simp add: field_simps setsum_right_distrib) |
|
2974 qed |
2835 |
2975 |
2836 subsubsection{* Formal trigonometric functions *} |
2976 subsubsection{* Formal trigonometric functions *} |
2837 |
2977 |
2838 definition "fps_sin (c::'a::field_char_0) = |
2978 definition "fps_sin (c::'a::field_char_0) = |
2839 Abs_fps (\<lambda>n. if even n then 0 else (- 1) ^((n - 1) div 2) * c^n /(of_nat (fact n)))" |
2979 Abs_fps (\<lambda>n. if even n then 0 else (- 1) ^((n - 1) div 2) * c^n /(of_nat (fact n)))" |
3088 |
3228 |
3089 lemma fps_demoivre: "(fps_cos a + fps_const ii * fps_sin a)^n = fps_cos (of_nat n * a) + fps_const ii * fps_sin (of_nat n * a)" |
3229 lemma fps_demoivre: "(fps_cos a + fps_const ii * fps_sin a)^n = fps_cos (of_nat n * a) + fps_const ii * fps_sin (of_nat n * a)" |
3090 unfolding Eii_sin_cos[symmetric] E_power_mult |
3230 unfolding Eii_sin_cos[symmetric] E_power_mult |
3091 by (simp add: mult_ac) |
3231 by (simp add: mult_ac) |
3092 |
3232 |
|
3233 subsection {* Hypergeometric series *} |
|
3234 |
|
3235 |
|
3236 definition "F as bs (c::'a::{field_char_0, division_by_zero}) = Abs_fps (%n. (foldl (%r a. r* pochhammer a n) 1 as * c^n)/ (foldl (%r b. r * pochhammer b n) 1 bs * of_nat (fact n)))" |
|
3237 |
|
3238 lemma F_nth[simp]: "F as bs c $ n = (foldl (%r a. r* pochhammer a n) 1 as * c^n)/ (foldl (%r b. r * pochhammer b n) 1 bs * of_nat (fact n))" |
|
3239 by (simp add: F_def) |
|
3240 |
|
3241 lemma foldl_mult_start: |
|
3242 "foldl (%r x. r * f x) (v::'a::comm_ring_1) as * x = foldl (%r x. r * f x) (v * x) as " |
|
3243 by (induct as arbitrary: x v, auto simp add: algebra_simps) |
|
3244 |
|
3245 lemma foldr_mult_foldl: "foldr (%x r. r * f x) as v = foldl (%r x. r * f x) (v :: 'a::comm_ring_1) as" |
|
3246 by (induct as arbitrary: v, auto simp add: foldl_mult_start) |
|
3247 |
|
3248 lemma F_nth_alt: "F as bs c $ n = foldr (\<lambda>a r. r * pochhammer a n) as (c ^ n) / |
|
3249 foldr (\<lambda>b r. r * pochhammer b n) bs (of_nat (fact n))" |
|
3250 by (simp add: foldl_mult_start foldr_mult_foldl) |
|
3251 |
|
3252 lemma F_E[simp]: "F [] [] c = E c" |
|
3253 by (simp add: fps_eq_iff) |
|
3254 |
|
3255 lemma F_1_0[simp]: "F [1] [] c = 1/(1 - fps_const c * X)" |
|
3256 proof- |
|
3257 let ?a = "(Abs_fps (\<lambda>n. 1)) oo (fps_const c * X)" |
|
3258 thm gp |
|
3259 have th0: "(fps_const c * X) $ 0 = 0" by simp |
|
3260 show ?thesis unfolding gp[OF th0, symmetric] |
|
3261 by (auto simp add: fps_eq_iff pochhammer_fact[symmetric] fps_compose_nth power_mult_distrib cond_value_iff setsum_delta' cong del: if_weak_cong) |
|
3262 qed |
|
3263 |
|
3264 lemma F_B[simp]: "F [-a] [] (- 1) = fps_binomial a" |
|
3265 by (simp add: fps_eq_iff gbinomial_pochhammer algebra_simps) |
|
3266 |
|
3267 lemma F_0[simp]: "F as bs c $0 = 1" |
|
3268 apply simp |
|
3269 apply (subgoal_tac "ALL as. foldl (%(r::'a) (a::'a). r) 1 as = 1") |
|
3270 apply auto |
|
3271 apply (induct_tac as, auto) |
|
3272 done |
|
3273 |
|
3274 lemma foldl_prod_prod: "foldl (%(r::'b::comm_ring_1) (x::'a::comm_ring_1). r * f x) v as * foldl (%r x. r * g x) w as = foldl (%r x. r * f x * g x) (v*w) as" |
|
3275 by (induct as arbitrary: v w, auto simp add: algebra_simps) |
|
3276 |
|
3277 |
|
3278 lemma F_rec: "F as bs c $ Suc n = ((foldl (%r a. r* (a + of_nat n)) c as)/ (foldl (%r b. r * (b + of_nat n)) (of_nat (Suc n)) bs )) * F as bs c $ n" |
|
3279 apply (simp del: of_nat_Suc of_nat_add fact_Suc) |
|
3280 apply (simp add: foldl_mult_start del: fact_Suc of_nat_Suc) |
|
3281 unfolding foldl_prod_prod[unfolded foldl_mult_start] pochhammer_Suc |
|
3282 by (simp add: algebra_simps of_nat_mult) |
|
3283 |
|
3284 lemma XD_nth[simp]: "XD a $ n = (if n=0 then 0 else of_nat n * a$n)" |
|
3285 by (simp add: XD_def) |
|
3286 |
|
3287 lemma XD_0th[simp]: "XD a $ 0 = 0" by simp |
|
3288 lemma XD_Suc[simp]:" XD a $ Suc n = of_nat (Suc n) * a $ Suc n" by simp |
|
3289 |
|
3290 definition "XDp c a = XD a + fps_const c * a" |
|
3291 |
|
3292 lemma XDp_nth[simp]: "XDp c a $ n = (c + of_nat n) * a$n" |
|
3293 by (simp add: XDp_def algebra_simps) |
|
3294 |
|
3295 lemma XDp_commute: |
|
3296 shows "XDp b o XDp (c::'a::comm_ring_1) = XDp c o XDp b" |
|
3297 by (auto simp add: XDp_def expand_fun_eq fps_eq_iff algebra_simps) |
|
3298 |
|
3299 lemma XDp0[simp]: "XDp 0 = XD" |
|
3300 by (simp add: expand_fun_eq fps_eq_iff) |
|
3301 |
|
3302 lemma XDp_fps_integral[simp]:"XDp 0 (fps_integral a c) = X * a" |
|
3303 by (simp add: fps_eq_iff fps_integral_def) |
|
3304 |
|
3305 lemma F_minus_nat: |
|
3306 "F [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0, division_by_zero}) $ k = (if k <= n then pochhammer (- of_nat n) k * c ^ k / |
|
3307 (pochhammer (- of_nat (n + m)) k * of_nat (fact k)) else 0)" |
|
3308 "F [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0, division_by_zero}) $ k = (if k <= m then pochhammer (- of_nat m) k * c ^ k / |
|
3309 (pochhammer (- of_nat (m + n)) k * of_nat (fact k)) else 0)" |
|
3310 by (auto simp add: pochhammer_eq_0_iff) |
|
3311 |
|
3312 lemma setsum_eq_if: "setsum f {(n::nat) .. m} = (if m < n then 0 else f n + setsum f {n+1 .. m})" |
|
3313 apply simp |
|
3314 apply (subst setsum_insert[symmetric]) |
|
3315 by (auto simp add: not_less setsum_head_Suc) |
|
3316 |
|
3317 lemma pochhammer_rec_if: |
|
3318 "pochhammer a n = (if n = 0 then 1 else a * pochhammer (a + 1) (n - 1))" |
|
3319 by (cases n, simp_all add: pochhammer_rec) |
|
3320 |
|
3321 lemma XDp_foldr_nth[simp]: "foldr (%c r. XDp c o r) cs (%c. XDp c a) c0 $ n = |
|
3322 foldr (%c r. (c + of_nat n) * r) cs (c0 + of_nat n) * a$n" |
|
3323 by (induct cs arbitrary: c0, auto simp add: algebra_simps) |
|
3324 |
|
3325 lemma genric_XDp_foldr_nth: |
|
3326 assumes |
|
3327 f: "ALL n c a. f c a $ n = (of_nat n + k c) * a$n" |
|
3328 |
|
3329 shows "foldr (%c r. f c o r) cs (%c. g c a) c0 $ n = |
|
3330 foldr (%c r. (k c + of_nat n) * r) cs (g c0 a $ n)" |
|
3331 by (induct cs arbitrary: c0, auto simp add: algebra_simps f ) |
|
3332 |
3093 end |
3333 end |