1973 |
1976 |
1974 lemma inverse_fps_of_nat: |
1977 lemma inverse_fps_of_nat: |
1975 "inverse (of_nat n :: 'a :: {semiring_1,times,uminus,inverse} fps) = |
1978 "inverse (of_nat n :: 'a :: {semiring_1,times,uminus,inverse} fps) = |
1976 fps_const (inverse (of_nat n))" |
1979 fps_const (inverse (of_nat n))" |
1977 by (simp add: fps_of_nat fps_const_inverse[symmetric]) |
1980 by (simp add: fps_of_nat fps_const_inverse[symmetric]) |
1978 |
|
1979 lemma sum_zero_lemma: |
|
1980 fixes n::nat |
|
1981 assumes "0 < n" |
|
1982 shows "(\<Sum>i = 0..n. if n = i then 1 else if n - i = 1 then - 1 else 0) = (0::'a::field)" |
|
1983 proof - |
|
1984 let ?f = "\<lambda>i. if n = i then 1 else if n - i = 1 then - 1 else 0" |
|
1985 let ?g = "\<lambda>i. if i = n then 1 else if i = n - 1 then - 1 else 0" |
|
1986 let ?h = "\<lambda>i. if i=n - 1 then - 1 else 0" |
|
1987 have th1: "sum ?f {0..n} = sum ?g {0..n}" |
|
1988 by (rule sum.cong) auto |
|
1989 have th2: "sum ?g {0..n - 1} = sum ?h {0..n - 1}" |
|
1990 apply (rule sum.cong) |
|
1991 using assms |
|
1992 apply auto |
|
1993 done |
|
1994 have eq: "{0 .. n} = {0.. n - 1} \<union> {n}" |
|
1995 by auto |
|
1996 from assms have d: "{0.. n - 1} \<inter> {n} = {}" |
|
1997 by auto |
|
1998 have f: "finite {0.. n - 1}" "finite {n}" |
|
1999 by auto |
|
2000 show ?thesis |
|
2001 unfolding th1 |
|
2002 apply (simp add: sum.union_disjoint[OF f d, unfolded eq[symmetric]] del: One_nat_def) |
|
2003 unfolding th2 |
|
2004 apply simp |
|
2005 done |
|
2006 qed |
|
2007 |
1981 |
2008 lemma fps_lr_inverse_mult_ring1: |
1982 lemma fps_lr_inverse_mult_ring1: |
2009 fixes f g :: "'a::ring_1 fps" |
1983 fixes f g :: "'a::ring_1 fps" |
2010 assumes x: "x * f$0 = 1" "f$0 * x = 1" |
1984 assumes x: "x * f$0 = 1" "f$0 * x = 1" |
2011 and y: "y * g$0 = 1" "g$0 * y = 1" |
1985 and y: "y * g$0 = 1" "g$0 * y = 1" |
3899 by simp |
3874 by simp |
3900 then have ys: "?ys \<in> natpermute (n - ?m) (k - h)" |
3875 then have ys: "?ys \<in> natpermute (n - ?m) (k - h)" |
3901 using l assms ls by (auto simp add: natpermute_def simp del: append_take_drop_id) |
3876 using l assms ls by (auto simp add: natpermute_def simp del: append_take_drop_id) |
3902 from ls have m: "?m \<in> {0..n}" |
3877 from ls have m: "?m \<in> {0..n}" |
3903 by (simp add: l_take_drop del: append_take_drop_id) |
3878 by (simp add: l_take_drop del: append_take_drop_id) |
3904 from xs ys ls show "l \<in> ?R" |
3879 have "sum_list (take h l) \<le> sum_list l" |
3905 apply auto |
3880 using l_take_drop ls m by presburger |
3906 apply (rule bexI [where x = "?m"]) |
3881 with xs ys ls l show "l \<in> ?R" |
3907 apply (rule exI [where x = "?xs"]) |
3882 by simp (metis append_take_drop_id m) |
3908 apply (rule exI [where x = "?ys"]) |
|
3909 using ls l |
|
3910 apply (auto simp add: natpermute_def l_take_drop simp del: append_take_drop_id) |
|
3911 apply simp |
|
3912 done |
|
3913 qed |
3883 qed |
3914 qed |
3884 qed |
3915 |
3885 |
3916 lemma natpermute_0: "natpermute n 0 = (if n = 0 then {[]} else {})" |
3886 lemma natpermute_0: "natpermute n 0 = (if n = 0 then {[]} else {})" |
3917 by (auto simp add: natpermute_def) |
3887 by (auto simp add: natpermute_def) |
3918 |
3888 |
3919 lemma natpermute_0'[simp]: "natpermute 0 k = (if k = 0 then {[]} else {replicate k 0})" |
3889 lemma natpermute_0'[simp]: "natpermute 0 k = (if k = 0 then {[]} else {replicate k 0})" |
3920 apply (auto simp add: set_replicate_conv_if natpermute_def) |
3890 by (auto simp add: set_replicate_conv_if natpermute_def replicate_length_same) |
3921 apply (rule nth_equalityI) |
|
3922 apply simp_all |
|
3923 done |
|
3924 |
3891 |
3925 lemma natpermute_finite: "finite (natpermute n k)" |
3892 lemma natpermute_finite: "finite (natpermute n k)" |
3926 proof (induct k arbitrary: n) |
3893 proof (induct k arbitrary: n) |
3927 case 0 |
3894 case 0 |
3928 then show ?case |
3895 then show ?case |
3929 apply (subst natpermute_split[of 0 0, simplified]) |
3896 by (simp add: natpermute_0) |
3930 apply (simp add: natpermute_0) |
|
3931 done |
|
3932 next |
3897 next |
3933 case (Suc k) |
3898 case (Suc k) |
3934 then show ?case unfolding natpermute_split [of k "Suc k", simplified] |
3899 then show ?case |
3935 apply - |
3900 using natpermute_split [of k "Suc k"] finite_UN_I by simp |
3936 apply (rule finite_UN_I) |
|
3937 apply simp |
|
3938 unfolding One_nat_def[symmetric] natlist_trivial_1 |
|
3939 apply simp |
|
3940 done |
|
3941 qed |
3901 qed |
3942 |
3902 |
3943 lemma natpermute_contain_maximal: |
3903 lemma natpermute_contain_maximal: |
3944 "{xs \<in> natpermute n (k + 1). n \<in> set xs} = (\<Union>i\<in>{0 .. k}. {(replicate (k + 1) 0) [i:=n]})" |
3904 "{xs \<in> natpermute n (k + 1). n \<in> set xs} = (\<Union>i\<in>{0 .. k}. {(replicate (k + 1) 0) [i:=n]})" |
3945 (is "?A = ?B") |
3905 (is "?A = ?B") |
4023 fix m n assume H: "\<forall>m' < m. \<forall>n. ?P m' n" |
3979 fix m n assume H: "\<forall>m' < m. \<forall>n. ?P m' n" |
4024 show "?P m n" |
3980 show "?P m n" |
4025 proof (cases m) |
3981 proof (cases m) |
4026 case 0 |
3982 case 0 |
4027 then show ?thesis |
3983 then show ?thesis |
4028 apply simp |
3984 by simp |
4029 unfolding natlist_trivial_1[where n = n, unfolded One_nat_def] |
|
4030 apply simp |
|
4031 done |
|
4032 next |
3985 next |
4033 case (Suc k) |
3986 case (Suc k) |
4034 then have km: "k < m" by arith |
3987 then have km: "k < m" by arith |
4035 have u0: "{0 .. k} \<union> {m} = {0..m}" |
3988 have u0: "{0 .. k} \<union> {m} = {0..m}" |
4036 using Suc by (simp add: set_eq_iff) presburger |
3989 using Suc by (simp add: set_eq_iff) presburger |
4037 have f0: "finite {0 .. k}" "finite {m}" by auto |
3990 have f0: "finite {0 .. k}" "finite {m}" by auto |
4038 have d0: "{0 .. k} \<inter> {m} = {}" using Suc by auto |
3991 have d0: "{0 .. k} \<inter> {m} = {}" using Suc by auto |
4039 have "(prod a {0 .. m}) $ n = (prod a {0 .. k} * a m) $ n" |
3992 have "(prod a {0 .. m}) $ n = (prod a {0 .. k} * a m) $ n" |
4040 unfolding prod.union_disjoint[OF f0 d0, unfolded u0] by simp |
3993 unfolding prod.union_disjoint[OF f0 d0, unfolded u0] by simp |
4041 also have "\<dots> = (\<Sum>i = 0..n. (\<Sum>v\<in>natpermute i (k + 1). \<Prod>j\<in>{0..k}. a j $ v ! j) * a m $ (n - i))" |
3994 also have "\<dots> = (\<Sum>i = 0..n. (\<Sum>v\<in>natpermute i (k + 1). |
4042 unfolding fps_mult_nth H[rule_format, OF km] .. |
3995 (\<Prod>j = 0..k. a j $ v ! j) * a m $ (n - i)))" |
|
3996 unfolding fps_mult_nth H[rule_format, OF km] sum_distrib_right .. |
|
3997 also have "... = (\<Sum>i = 0..n. |
|
3998 \<Sum>v\<in>(\<lambda>l1. l1 @ [n - i]) ` natpermute i (Suc k). |
|
3999 (\<Prod>j = 0..k. a j $ v ! j) * a (Suc k) $ v ! Suc k)" |
|
4000 by (intro sum.cong [OF refl sym] sum.reindex_cong) (auto simp: inj_on_def natpermute_def nth_append Suc) |
|
4001 also have "... = (\<Sum>v\<in>(\<Union>x\<in>{0..n}. {l1 @ [n - x] |l1. l1 \<in> natpermute x (Suc k)}). |
|
4002 (\<Prod>j = 0..k. a j $ v ! j) * a (Suc k) $ v ! Suc k)" |
|
4003 by (subst sum.UNION_disjoint) (auto simp add: natpermute_finite setcompr_eq_image) |
4043 also have "\<dots> = (\<Sum>v\<in>natpermute n (m + 1). \<Prod>j\<in>{0..m}. a j $ v ! j)" |
4004 also have "\<dots> = (\<Sum>v\<in>natpermute n (m + 1). \<Prod>j\<in>{0..m}. a j $ v ! j)" |
4044 apply (simp add: Suc) |
4005 using natpermute_split[of m "m + 1"] by (simp add: Suc) |
4045 unfolding natpermute_split[of m "m + 1", simplified, of n, |
|
4046 unfolded natlist_trivial_1[unfolded One_nat_def] Suc] |
|
4047 apply (subst sum.UNION_disjoint) |
|
4048 apply simp |
|
4049 apply simp |
|
4050 unfolding image_Collect[symmetric] |
|
4051 apply clarsimp |
|
4052 apply (rule finite_imageI) |
|
4053 apply (rule natpermute_finite) |
|
4054 apply (clarsimp simp add: set_eq_iff) |
|
4055 apply auto |
|
4056 apply (rule sum.cong) |
|
4057 apply (rule refl) |
|
4058 unfolding sum_distrib_right |
|
4059 apply (rule sym) |
|
4060 apply (rule_tac l = "\<lambda>xs. xs @ [n - x]" in sum.reindex_cong) |
|
4061 apply (simp add: inj_on_def) |
|
4062 apply auto |
|
4063 unfolding prod.union_disjoint[OF f0 d0, unfolded u0, unfolded Suc] |
|
4064 apply (clarsimp simp add: natpermute_def nth_append) |
|
4065 done |
|
4066 finally show ?thesis . |
4006 finally show ?thesis . |
4067 qed |
4007 qed |
4068 qed |
4008 qed |
4069 |
4009 |
4070 text \<open>The special form for powers.\<close> |
4010 text \<open>The special form for powers.\<close> |
4330 unfolding sum.union_disjoint[OF fths(2) fths(3) d(2)] |
4267 unfolding sum.union_disjoint[OF fths(2) fths(3) d(2)] |
4331 by simp |
4268 by simp |
4332 finally show ?thesis using c' by simp |
4269 finally show ?thesis using c' by simp |
4333 qed |
4270 qed |
4334 then show "((r, Suc k, a, xs!i), r, Suc k, a, Suc n) \<in> ?R" |
4271 then show "((r, Suc k, a, xs!i), r, Suc k, a, Suc n) \<in> ?R" |
4335 apply auto |
4272 using not_less by auto |
4336 apply (metis not_less) |
|
4337 done |
|
4338 next |
4273 next |
4339 fix r :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" |
4274 fix r :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" |
4340 and a :: "'a fps" |
4275 and a :: "'a fps" |
4341 and k n |
4276 and k n |
4342 show "((r, Suc k, a, 0), r, Suc k, a, Suc n) \<in> ?R" by simp |
4277 show "((r, Suc k, a, 0), r, Suc k, a, Suc n) \<in> ?R" by simp |
4343 } |
4278 } |
4344 qed |
4279 qed |
4345 |
4280 |
4346 definition "fps_radical r n a = Abs_fps (radical r n a)" |
4281 definition "fps_radical r n a = Abs_fps (radical r n a)" |
4347 |
4282 |
|
4283 lemma radical_0 [simp]: "\<And>n. 0 < n \<Longrightarrow> radical r 0 a n = 0" |
|
4284 using radical.elims by blast |
|
4285 |
4348 lemma fps_radical0[simp]: "fps_radical r 0 a = 1" |
4286 lemma fps_radical0[simp]: "fps_radical r 0 a = 1" |
4349 apply (auto simp add: fps_eq_iff fps_radical_def) |
4287 by (auto simp add: fps_eq_iff fps_radical_def) |
4350 apply (case_tac n) |
|
4351 apply auto |
|
4352 done |
|
4353 |
4288 |
4354 lemma fps_radical_nth_0[simp]: "fps_radical r n a $ 0 = (if n = 0 then 1 else r n (a$0))" |
4289 lemma fps_radical_nth_0[simp]: "fps_radical r n a $ 0 = (if n = 0 then 1 else r n (a$0))" |
4355 by (cases n) (simp_all add: fps_radical_def) |
4290 by (cases n) (simp_all add: fps_radical_def) |
4356 |
4291 |
4357 lemma fps_radical_power_nth[simp]: |
4292 lemma fps_radical_power_nth[simp]: |
4445 then show ?thesis |
4380 then show ?thesis |
4446 unfolding fps_power_nth_Suc |
4381 unfolding fps_power_nth_Suc |
4447 by (simp add: prod_constant del: replicate.simps) |
4382 by (simp add: prod_constant del: replicate.simps) |
4448 qed |
4383 qed |
4449 qed |
4384 qed |
4450 |
|
4451 (* |
|
4452 lemma power_radical: |
|
4453 fixes a:: "'a::field_char_0 fps" |
|
4454 assumes r0: "(r (Suc k) (a$0)) ^ Suc k = a$0" and a0: "a$0 \<noteq> 0" |
|
4455 shows "(fps_radical r (Suc k) a) ^ (Suc k) = a" |
|
4456 proof- |
|
4457 let ?r = "fps_radical r (Suc k) a" |
|
4458 from a0 r0 have r00: "r (Suc k) (a$0) \<noteq> 0" by auto |
|
4459 {fix z have "?r ^ Suc k $ z = a$z" |
|
4460 proof(induct z rule: nat_less_induct) |
|
4461 fix n assume H: "\<forall>m<n. ?r ^ Suc k $ m = a$m" |
|
4462 {assume "n = 0" then have "?r ^ Suc k $ n = a $n" |
|
4463 using fps_radical_power_nth[of r "Suc k" a, OF r0] by simp} |
|
4464 moreover |
|
4465 {fix n1 assume n1: "n = Suc n1" |
|
4466 have fK: "finite {0..k}" by simp |
|
4467 have nz: "n \<noteq> 0" using n1 by arith |
|
4468 let ?Pnk = "natpermute n (k + 1)" |
|
4469 let ?Pnkn = "{xs \<in> ?Pnk. n \<in> set xs}" |
|
4470 let ?Pnknn = "{xs \<in> ?Pnk. n \<notin> set xs}" |
|
4471 have eq: "?Pnkn \<union> ?Pnknn = ?Pnk" by blast |
|
4472 have d: "?Pnkn \<inter> ?Pnknn = {}" by blast |
|
4473 have f: "finite ?Pnkn" "finite ?Pnknn" |
|
4474 using finite_Un[of ?Pnkn ?Pnknn, unfolded eq] |
|
4475 by (metis natpermute_finite)+ |
|
4476 let ?f = "\<lambda>v. \<Prod>j\<in>{0..k}. ?r $ v ! j" |
|
4477 have "sum ?f ?Pnkn = sum (\<lambda>v. ?r $ n * r (Suc k) (a $ 0) ^ k) ?Pnkn" |
|
4478 proof(rule sum.cong2) |
|
4479 fix v assume v: "v \<in> {xs \<in> natpermute n (k + 1). n \<in> set xs}" |
|
4480 let ?ths = "(\<Prod>j\<in>{0..k}. fps_radical r (Suc k) a $ v ! j) = fps_radical r (Suc k) a $ n * r (Suc k) (a $ 0) ^ k" |
|
4481 from v obtain i where i: "i \<in> {0..k}" "v = replicate (k+1) 0 [i:= n]" |
|
4482 unfolding natpermute_contain_maximal by auto |
|
4483 have "(\<Prod>j\<in>{0..k}. fps_radical r (Suc k) a $ v ! j) = (\<Prod>j\<in>{0..k}. if j = i then fps_radical r (Suc k) a $ n else r (Suc k) (a$0))" |
|
4484 apply (rule prod.cong, simp) |
|
4485 using i r0 by (simp del: replicate.simps) |
|
4486 also have "\<dots> = (fps_radical r (Suc k) a $ n) * r (Suc k) (a$0) ^ k" |
|
4487 unfolding prod_gen_delta[OF fK] using i r0 by simp |
|
4488 finally show ?ths . |
|
4489 qed |
|
4490 then have "sum ?f ?Pnkn = of_nat (k+1) * ?r $ n * r (Suc k) (a $ 0) ^ k" |
|
4491 by (simp add: natpermute_max_card[OF nz, simplified]) |
|
4492 also have "\<dots> = a$n - sum ?f ?Pnknn" |
|
4493 unfolding n1 using r00 a0 by (simp add: field_simps fps_radical_def del: of_nat_Suc ) |
|
4494 finally have fn: "sum ?f ?Pnkn = a$n - sum ?f ?Pnknn" . |
|
4495 have "(?r ^ Suc k)$n = sum ?f ?Pnkn + sum ?f ?Pnknn" |
|
4496 unfolding fps_power_nth_Suc sum.union_disjoint[OF f d, unfolded eq] .. |
|
4497 also have "\<dots> = a$n" unfolding fn by simp |
|
4498 finally have "?r ^ Suc k $ n = a $n" .} |
|
4499 ultimately show "?r ^ Suc k $ n = a $n" by (cases n, auto) |
|
4500 qed } |
|
4501 then show ?thesis by (simp add: fps_eq_iff) |
|
4502 qed |
|
4503 |
|
4504 *) |
|
4505 lemma eq_divide_imp': |
|
4506 fixes c :: "'a::field" |
|
4507 shows "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c" |
|
4508 by (simp add: field_simps) |
|
4509 |
4385 |
4510 lemma radical_unique: |
4386 lemma radical_unique: |
4511 assumes r0: "(r (Suc k) (b$0)) ^ Suc k = b$0" |
4387 assumes r0: "(r (Suc k) (b$0)) ^ Suc k = b$0" |
4512 and a0: "r (Suc k) (b$0 ::'a::field_char_0) = a$0" |
4388 and a0: "r (Suc k) (b$0 ::'a::field_char_0) = a$0" |
4513 and b0: "b$0 \<noteq> 0" |
4389 and b0: "b$0 \<noteq> 0" |
4598 unfolding fps_power_nth_Suc |
4471 unfolding fps_power_nth_Suc |
4599 using sum.union_disjoint[OF f d, unfolded Suc_eq_plus1[symmetric], |
4472 using sum.union_disjoint[OF f d, unfolded Suc_eq_plus1[symmetric], |
4600 unfolded eq, of ?g] by simp |
4473 unfolded eq, of ?g] by simp |
4601 also have "\<dots> = of_nat (k+1) * a $ n * (?r $ 0)^k + sum ?f ?Pnknn" |
4474 also have "\<dots> = of_nat (k+1) * a $ n * (?r $ 0)^k + sum ?f ?Pnknn" |
4602 unfolding th0 th1 .. |
4475 unfolding th0 th1 .. |
4603 finally have "of_nat (k+1) * a $ n * (?r $ 0)^k = b$n - sum ?f ?Pnknn" |
4476 finally have \<section>: "of_nat (k+1) * a $ n * (?r $ 0)^k = b$n - sum ?f ?Pnknn" |
4604 by simp |
4477 by simp |
4605 then have "a$n = (b$n - sum ?f ?Pnknn) / (of_nat (k+1) * (?r $ 0)^k)" |
4478 have "a$n = (b$n - sum ?f ?Pnknn) / (of_nat (k+1) * (?r $ 0)^k)" |
4606 apply - |
4479 apply (rule eq_divide_imp) |
4607 apply (rule eq_divide_imp') |
4480 using r00 \<section> by (simp_all add: ac_simps del: of_nat_Suc) |
4608 using r00 |
|
4609 apply (simp del: of_nat_Suc) |
|
4610 apply (simp add: ac_simps) |
|
4611 done |
|
4612 then show ?thesis |
4481 then show ?thesis |
4613 apply (simp del: of_nat_Suc) |
|
4614 unfolding fps_radical_def Suc |
4482 unfolding fps_radical_def Suc |
4615 apply (simp add: field_simps Suc th00 del: of_nat_Suc) |
4483 by (simp del: of_nat_Suc) |
4616 done |
|
4617 qed |
4484 qed |
4618 qed |
4485 qed |
4619 then show ?rhs by (simp add: fps_eq_iff) |
4486 then show ?rhs by (simp add: fps_eq_iff) |
4620 qed |
4487 qed |
4621 qed |
4488 qed |
4818 also have "\<dots> = sum (\<lambda>i. of_nat i * a$i * (((b^(i - 1)) * fps_deriv b))$n) {0.. Suc n}" |
4685 also have "\<dots> = sum (\<lambda>i. of_nat i * a$i * (((b^(i - 1)) * fps_deriv b))$n) {0.. Suc n}" |
4819 unfolding fps_mult_left_const_nth by (simp add: field_simps) |
4686 unfolding fps_mult_left_const_nth by (simp add: field_simps) |
4820 also have "\<dots> = sum (\<lambda>i. of_nat i * a$i * (sum (\<lambda>j. (b^ (i - 1))$j * (fps_deriv b)$(n - j)) {0..n})) {0.. Suc n}" |
4687 also have "\<dots> = sum (\<lambda>i. of_nat i * a$i * (sum (\<lambda>j. (b^ (i - 1))$j * (fps_deriv b)$(n - j)) {0..n})) {0.. Suc n}" |
4821 unfolding fps_mult_nth .. |
4688 unfolding fps_mult_nth .. |
4822 also have "\<dots> = sum (\<lambda>i. of_nat i * a$i * (sum (\<lambda>j. (b^ (i - 1))$j * (fps_deriv b)$(n - j)) {0..n})) {1.. Suc n}" |
4689 also have "\<dots> = sum (\<lambda>i. of_nat i * a$i * (sum (\<lambda>j. (b^ (i - 1))$j * (fps_deriv b)$(n - j)) {0..n})) {1.. Suc n}" |
4823 apply (rule sum.mono_neutral_right) |
4690 by (intro sum.mono_neutral_right) (auto simp add: mult_delta_left not_le) |
4824 apply (auto simp add: mult_delta_left not_le) |
|
4825 done |
|
4826 also have "\<dots> = sum (\<lambda>i. of_nat (i + 1) * a$(i+1) * (sum (\<lambda>j. (b^ i)$j * of_nat (n - j + 1) * b$(n - j + 1)) {0..n})) {0.. n}" |
4691 also have "\<dots> = sum (\<lambda>i. of_nat (i + 1) * a$(i+1) * (sum (\<lambda>j. (b^ i)$j * of_nat (n - j + 1) * b$(n - j + 1)) {0..n})) {0.. n}" |
4827 unfolding fps_deriv_nth |
4692 unfolding fps_deriv_nth |
4828 by (rule sum.reindex_cong [of Suc]) (simp_all add: mult.assoc) |
4693 by (rule sum.reindex_cong [of Suc]) (simp_all add: mult.assoc) |
4829 finally have th0: "(fps_deriv (a oo b))$n = |
4694 finally have th0: "(fps_deriv (a oo b))$n = |
4830 sum (\<lambda>i. of_nat (i + 1) * a$(i+1) * (sum (\<lambda>j. (b^ i)$j * of_nat (n - j + 1) * b$(n - j + 1)) {0..n})) {0.. n}" . |
4695 sum (\<lambda>i. of_nat (i + 1) * a$(i+1) * (sum (\<lambda>j. (b^ i)$j * of_nat (n - j + 1) * b$(n - j + 1)) {0..n})) {0.. n}" . |
4831 |
4696 |
4832 have "(((fps_deriv a) oo b) * (fps_deriv b))$n = sum (\<lambda>i. (fps_deriv b)$ (n - i) * ((fps_deriv a) oo b)$i) {0..n}" |
4697 have "(((fps_deriv a) oo b) * (fps_deriv b))$n = sum (\<lambda>i. (fps_deriv b)$ (n - i) * ((fps_deriv a) oo b)$i) {0..n}" |
4833 unfolding fps_mult_nth by (simp add: ac_simps) |
4698 unfolding fps_mult_nth by (simp add: ac_simps) |
4834 also have "\<dots> = sum (\<lambda>i. sum (\<lambda>j. of_nat (n - i +1) * b$(n - i + 1) * of_nat (j + 1) * a$(j+1) * (b^j)$i) {0..n}) {0..n}" |
4699 also have "\<dots> = sum (\<lambda>i. sum (\<lambda>j. of_nat (n - i +1) * b$(n - i + 1) * of_nat (j + 1) * a$(j+1) * (b^j)$i) {0..n}) {0..n}" |
4835 unfolding fps_deriv_nth fps_compose_nth sum_distrib_left mult.assoc |
4700 unfolding fps_deriv_nth fps_compose_nth sum_distrib_left mult.assoc |
4836 apply (rule sum.cong) |
4701 by (auto simp: subset_eq b0 startsby_zero_power_prefix sum.mono_neutral_left intro: sum.cong) |
4837 apply (rule refl) |
|
4838 apply (rule sum.mono_neutral_left) |
|
4839 apply (simp_all add: subset_eq) |
|
4840 apply clarify |
|
4841 apply (subgoal_tac "b^i$x = 0") |
|
4842 apply simp |
|
4843 apply (rule startsby_zero_power_prefix[OF b0, rule_format]) |
|
4844 apply simp |
|
4845 done |
|
4846 also have "\<dots> = sum (\<lambda>i. of_nat (i + 1) * a$(i+1) * (sum (\<lambda>j. (b^ i)$j * of_nat (n - j + 1) * b$(n - j + 1)) {0..n})) {0.. n}" |
4702 also have "\<dots> = sum (\<lambda>i. of_nat (i + 1) * a$(i+1) * (sum (\<lambda>j. (b^ i)$j * of_nat (n - j + 1) * b$(n - j + 1)) {0..n})) {0.. n}" |
4847 unfolding sum_distrib_left |
4703 unfolding sum_distrib_left |
4848 apply (subst sum.swap) |
4704 by (subst sum.swap) (force intro: sum.cong) |
4849 apply (rule sum.cong, rule refl)+ |
|
4850 apply simp |
|
4851 done |
|
4852 finally show ?thesis |
4705 finally show ?thesis |
4853 unfolding th0 by simp |
4706 unfolding th0 by simp |
4854 qed |
4707 qed |
4855 then show ?thesis by (simp add: fps_eq_iff) |
4708 then show ?thesis by (simp add: fps_eq_iff) |
4856 qed |
4709 qed |
5002 sum (\<lambda>(k,m). a$k * b$m * (c^k * d^m) $ n) {(k,m). k + m \<le> n}" (is "?l = ?r") |
4858 sum (\<lambda>(k,m). a$k * b$m * (c^k * d^m) $ n) {(k,m). k + m \<le> n}" (is "?l = ?r") |
5003 proof - |
4859 proof - |
5004 let ?S = "{(k::nat, m::nat). k + m \<le> n}" |
4860 let ?S = "{(k::nat, m::nat). k + m \<le> n}" |
5005 have s: "?S \<subseteq> {0..n} \<times> {0..n}" by (simp add: subset_eq) |
4861 have s: "?S \<subseteq> {0..n} \<times> {0..n}" by (simp add: subset_eq) |
5006 have f: "finite {(k::nat, m::nat). k + m \<le> n}" |
4862 have f: "finite {(k::nat, m::nat). k + m \<le> n}" |
5007 apply (rule finite_subset[OF s]) |
4863 by (auto intro: finite_subset[OF s]) |
5008 apply auto |
4864 have "?r = (\<Sum>(k, m) \<in> {(k, m). k + m \<le> n}. \<Sum>j = 0..n. a $ k * b $ m * (c ^ k $ j * d ^ m $ (n - j)))" |
5009 done |
4865 by (simp add: fps_mult_nth sum_distrib_left) |
5010 have "?r = sum (\<lambda>i. sum (\<lambda>(k,m). a$k * (c^k)$i * b$m * (d^m) $ (n - i)) {(k,m). k + m \<le> n}) {0..n}" |
4866 also have "\<dots> = (\<Sum>i = 0..n. \<Sum>(k,m)\<in>{(k,m). k+m \<le> n}. a $ k * c ^ k $ i * b $ m * d ^ m $ (n-i))" |
5011 apply (simp add: fps_mult_nth sum_distrib_left) |
4867 unfolding sum.swap [where A = "{0..n}"] by (auto simp add: field_simps intro: sum.cong) |
5012 apply (subst sum.swap) |
4868 also have "... = (\<Sum>i = 0..n. |
5013 apply (rule sum.cong) |
4869 \<Sum>q = 0..i. \<Sum>j = 0..n - i. a $ q * c ^ q $ i * (b $ j * d ^ j $ (n - i)))" |
5014 apply (auto simp add: field_simps) |
4870 apply (rule sum.cong [OF refl]) |
5015 done |
4871 apply (simp add: sum.cartesian_product mult.assoc) |
|
4872 apply (rule sum.mono_neutral_right[OF f], force) |
|
4873 by clarsimp (meson c0 d0 leI startsby_zero_power_prefix) |
5016 also have "\<dots> = ?l" |
4874 also have "\<dots> = ?l" |
5017 apply (simp add: fps_mult_nth fps_compose_nth sum_product) |
4875 by (simp add: fps_mult_nth fps_compose_nth sum_product) |
5018 apply (rule sum.cong) |
|
5019 apply (rule refl) |
|
5020 apply (simp add: sum.cartesian_product mult.assoc) |
|
5021 apply (rule sum.mono_neutral_right[OF f]) |
|
5022 apply (simp add: subset_eq) |
|
5023 apply presburger |
|
5024 apply clarsimp |
|
5025 apply (rule ccontr) |
|
5026 apply (clarsimp simp add: not_le) |
|
5027 apply (case_tac "x < aa") |
|
5028 apply simp |
|
5029 apply (frule_tac startsby_zero_power_prefix[rule_format, OF c0]) |
|
5030 apply blast |
|
5031 apply simp |
|
5032 apply (frule_tac startsby_zero_power_prefix[rule_format, OF d0]) |
|
5033 apply blast |
|
5034 done |
|
5035 finally show ?thesis by simp |
4876 finally show ?thesis by simp |
5036 qed |
4877 qed |
5037 |
|
5038 lemma product_composition_lemma': |
|
5039 assumes c0: "c$0 = (0::'a::idom)" |
|
5040 and d0: "d$0 = 0" |
|
5041 shows "((a oo c) * (b oo d))$n = |
|
5042 sum (\<lambda>k. sum (\<lambda>m. a$k * b$m * (c^k * d^m) $ n) {0..n}) {0..n}" (is "?l = ?r") |
|
5043 unfolding product_composition_lemma[OF c0 d0] |
|
5044 unfolding sum.cartesian_product |
|
5045 apply (rule sum.mono_neutral_left) |
|
5046 apply simp |
|
5047 apply (clarsimp simp add: subset_eq) |
|
5048 apply clarsimp |
|
5049 apply (rule ccontr) |
|
5050 apply (subgoal_tac "(c^aa * d^ba) $ n = 0") |
|
5051 apply simp |
|
5052 unfolding fps_mult_nth |
|
5053 apply (rule sum.neutral) |
|
5054 apply (clarsimp simp add: not_le) |
|
5055 apply (case_tac "x < aa") |
|
5056 apply (rule startsby_zero_power_prefix[OF c0, rule_format]) |
|
5057 apply simp |
|
5058 apply (subgoal_tac "n - x < ba") |
|
5059 apply (frule_tac k = "ba" in startsby_zero_power_prefix[OF d0, rule_format]) |
|
5060 apply simp |
|
5061 apply arith |
|
5062 done |
|
5063 |
|
5064 |
4878 |
5065 lemma sum_pair_less_iff: |
4879 lemma sum_pair_less_iff: |
5066 "sum (\<lambda>((k::nat),m). a k * b m * c (k + m)) {(k,m). k + m \<le> n} = |
4880 "sum (\<lambda>((k::nat),m). a k * b m * c (k + m)) {(k,m). k + m \<le> n} = |
5067 sum (\<lambda>s. sum (\<lambda>i. a i * b (s - i) * c s) {0..s}) {0..n}" |
4881 sum (\<lambda>s. sum (\<lambda>i. a i * b (s - i) * c s) {0..s}) {0..n}" |
5068 (is "?l = ?r") |
4882 (is "?l = ?r") |
5069 proof - |
4883 proof - |
5070 let ?KM = "{(k,m). k + m \<le> n}" |
4884 have th0: "{(k, m). k + m \<le> n} = (\<Union>s\<in>{0..n}. \<Union>i\<in>{0..s}. {(i, s - i)})" |
5071 let ?f = "\<lambda>s. \<Union>i\<in>{0..s}. {(i, s - i)}" |
|
5072 have th0: "?KM = \<Union> (?f ` {0..n})" |
|
5073 by auto |
4885 by auto |
5074 show "?l = ?r " |
4886 show "?l = ?r" |
5075 unfolding th0 |
4887 unfolding th0 |
5076 apply (subst sum.UNION_disjoint) |
4888 by (simp add: sum.UNION_disjoint eq_diff_iff disjoint_iff) |
5077 apply auto |
|
5078 apply (subst sum.UNION_disjoint) |
|
5079 apply auto |
|
5080 done |
|
5081 qed |
4889 qed |
5082 |
4890 |
5083 lemma fps_compose_mult_distrib_lemma: |
4891 lemma fps_compose_mult_distrib_lemma: |
5084 assumes c0: "c$0 = (0::'a::idom)" |
4892 assumes c0: "c$0 = (0::'a::idom)" |
5085 shows "((a oo c) * (b oo c))$n = sum (\<lambda>s. sum (\<lambda>i. a$i * b$(s - i) * (c^s) $ n) {0..s}) {0..n}" |
4893 shows "((a oo c) * (b oo c))$n = sum (\<lambda>s. sum (\<lambda>i. a$i * b$(s - i) * (c^s) $ n) {0..s}) {0..n}" |
5087 unfolding sum_pair_less_iff[where a = "\<lambda>k. a$k" and b="\<lambda>m. b$m" and c="\<lambda>s. (c ^ s)$n" and n = n] .. |
4895 unfolding sum_pair_less_iff[where a = "\<lambda>k. a$k" and b="\<lambda>m. b$m" and c="\<lambda>s. (c ^ s)$n" and n = n] .. |
5088 |
4896 |
5089 lemma fps_compose_mult_distrib: |
4897 lemma fps_compose_mult_distrib: |
5090 assumes c0: "c $ 0 = (0::'a::idom)" |
4898 assumes c0: "c $ 0 = (0::'a::idom)" |
5091 shows "(a * b) oo c = (a oo c) * (b oo c)" |
4899 shows "(a * b) oo c = (a oo c) * (b oo c)" |
5092 apply (simp add: fps_eq_iff fps_compose_mult_distrib_lemma [OF c0]) |
4900 proof (clarsimp simp add: fps_eq_iff fps_compose_mult_distrib_lemma [OF c0]) |
5093 apply (simp add: fps_compose_nth fps_mult_nth sum_distrib_right) |
4901 show "(a * b oo c) $ n = (\<Sum>s = 0..n. \<Sum>i = 0..s. a $ i * b $ (s - i) * c ^ s $ n)" for n |
5094 done |
4902 by (simp add: fps_compose_nth fps_mult_nth sum_distrib_right) |
|
4903 qed |
|
4904 |
5095 |
4905 |
5096 lemma fps_compose_prod_distrib: |
4906 lemma fps_compose_prod_distrib: |
5097 assumes c0: "c$0 = (0::'a::idom)" |
4907 assumes c0: "c$0 = (0::'a::idom)" |
5098 shows "prod a S oo c = prod (\<lambda>k. a k oo c) S" |
4908 shows "prod a S oo c = prod (\<lambda>k. a k oo c) S" |
5099 apply (cases "finite S") |
4909 proof (induct S rule: infinite_finite_induct) |
5100 apply simp_all |
4910 next |
5101 apply (induct S rule: finite_induct) |
4911 case (insert) |
5102 apply simp |
4912 then show ?case |
5103 apply (simp add: fps_compose_mult_distrib[OF c0]) |
4913 by (simp add: fps_compose_mult_distrib[OF c0]) |
5104 done |
4914 qed auto |
5105 |
4915 |
5106 lemma fps_compose_divide: |
4916 lemma fps_compose_divide: |
5107 assumes [simp]: "g dvd f" "h $ 0 = 0" |
4917 assumes [simp]: "g dvd f" "h $ 0 = 0" |
5108 shows "fps_compose f h = fps_compose (f / g :: 'a :: field fps) h * fps_compose g h" |
4918 shows "fps_compose f h = fps_compose (f / g :: 'a :: field fps) h * fps_compose g h" |
5109 proof - |
4919 proof - |
5226 have "?l$n = (sum (\<lambda>i. (fps_const (a$i) * b^i) oo c) {0..n})$n" |
5036 have "?l$n = (sum (\<lambda>i. (fps_const (a$i) * b^i) oo c) {0..n})$n" |
5227 by (simp add: fps_compose_nth fps_compose_power[OF c0] fps_const_mult_apply_left |
5037 by (simp add: fps_compose_nth fps_compose_power[OF c0] fps_const_mult_apply_left |
5228 sum_distrib_left mult.assoc fps_sum_nth) |
5038 sum_distrib_left mult.assoc fps_sum_nth) |
5229 also have "\<dots> = ((sum (\<lambda>i. fps_const (a$i) * b^i) {0..n}) oo c)$n" |
5039 also have "\<dots> = ((sum (\<lambda>i. fps_const (a$i) * b^i) {0..n}) oo c)$n" |
5230 by (simp add: fps_compose_sum_distrib) |
5040 by (simp add: fps_compose_sum_distrib) |
|
5041 also have "... = (\<Sum>i = 0..n. \<Sum>j = 0..n. a $ j * (b ^ j $ i * c ^ i $ n))" |
|
5042 by (simp add: fps_compose_nth fps_sum_nth sum_distrib_right mult.assoc) |
|
5043 also have "... = (\<Sum>i = 0..n. \<Sum>j = 0..i. a $ j * (b ^ j $ i * c ^ i $ n))" |
|
5044 by (intro sum.cong [OF refl] sum.mono_neutral_right; simp add: b0 startsby_zero_power_prefix) |
5231 also have "\<dots> = ?r$n" |
5045 also have "\<dots> = ?r$n" |
5232 apply (simp add: fps_compose_nth fps_sum_nth sum_distrib_right mult.assoc) |
5046 by (simp add: fps_compose_nth sum_distrib_right mult.assoc) |
5233 apply (rule sum.cong) |
|
5234 apply (rule refl) |
|
5235 apply (rule sum.mono_neutral_right) |
|
5236 apply (auto simp add: not_le) |
|
5237 apply (erule startsby_zero_power_prefix[OF b0, rule_format]) |
|
5238 done |
|
5239 finally show ?thesis . |
5047 finally show ?thesis . |
5240 qed |
5048 qed |
5241 then show ?thesis |
5049 then show ?thesis |
5242 by (simp add: fps_eq_iff) |
5050 by (simp add: fps_eq_iff) |
5243 qed |
5051 qed |
5639 have eq: "?l = ?r \<longleftrightarrow> ?lhs" |
5430 have eq: "?l = ?r \<longleftrightarrow> ?lhs" |
5640 proof - |
5431 proof - |
5641 have x10: "?x1 $ 0 \<noteq> 0" by simp |
5432 have x10: "?x1 $ 0 \<noteq> 0" by simp |
5642 have "?l = ?r \<longleftrightarrow> inverse ?x1 * ?l = inverse ?x1 * ?r" by simp |
5433 have "?l = ?r \<longleftrightarrow> inverse ?x1 * ?l = inverse ?x1 * ?r" by simp |
5643 also have "\<dots> \<longleftrightarrow> ?da = (fps_const c * a) / ?x1" |
5434 also have "\<dots> \<longleftrightarrow> ?da = (fps_const c * a) / ?x1" |
5644 apply (simp only: fps_divide_def mult.assoc[symmetric] inverse_mult_eq_1[OF x10]) |
5435 unfolding fps_divide_def mult.assoc[symmetric] inverse_mult_eq_1[OF x10] |
5645 apply (simp add: field_simps) |
5436 by (simp add: field_simps) |
5646 done |
|
5647 finally show ?thesis . |
5437 finally show ?thesis . |
5648 qed |
5438 qed |
5649 |
5439 |
5650 show ?rhs if ?lhs |
5440 show ?rhs if ?lhs |
5651 proof - |
5441 proof - |
5652 from eq that have h: "?l = ?r" .. |
5442 from eq that have h: "?l = ?r" .. |
5653 have th0: "a$ Suc n = ((c - of_nat n) / of_nat (Suc n)) * a $n" for n |
5443 have th0: "a$ Suc n = ((c - of_nat n) / of_nat (Suc n)) * a $n" for n |
5654 proof - |
5444 proof - |
5655 from h have "?l $ n = ?r $ n" by simp |
5445 from h have "?l $ n = ?r $ n" by simp |
5656 then show ?thesis |
5446 then show ?thesis |
5657 apply (simp add: field_simps del: of_nat_Suc) |
5447 by (simp add: field_simps del: of_nat_Suc split: if_split_asm) |
5658 apply (cases n) |
|
5659 apply (simp_all add: field_simps del: of_nat_Suc) |
|
5660 done |
|
5661 qed |
5448 qed |
5662 have th1: "a $ n = (c gchoose n) * a $ 0" for n |
5449 have th1: "a $ n = (c gchoose n) * a $ 0" for n |
5663 proof (induct n) |
5450 proof (induct n) |
5664 case 0 |
5451 case 0 |
5665 then show ?case by simp |
5452 then show ?case by simp |
5666 next |
5453 next |
5667 case (Suc m) |
5454 case (Suc m) |
5668 then show ?case |
5455 have "(c - of_nat m) * (c gchoose m) = (c gchoose Suc m) * of_nat (Suc m)" |
|
5456 by (metis gbinomial_absorb_comp gbinomial_absorption mult.commute) |
|
5457 with Suc show ?case |
5669 unfolding th0 |
5458 unfolding th0 |
5670 apply (simp add: field_simps del: of_nat_Suc) |
5459 by (simp add: divide_simps del: of_nat_Suc) |
5671 unfolding mult.assoc[symmetric] gbinomial_mult_1 |
|
5672 apply (simp add: field_simps) |
|
5673 done |
|
5674 qed |
5460 qed |
5675 show ?thesis |
5461 show ?thesis |
5676 apply (simp add: fps_eq_iff) |
5462 by (metis expand_fps_eq fps_binomial_nth fps_mult_right_const_nth mult.commute th1) |
5677 apply (subst th1) |
|
5678 apply (simp add: field_simps) |
|
5679 done |
|
5680 qed |
5463 qed |
5681 |
5464 |
5682 show ?lhs if ?rhs |
5465 show ?lhs if ?rhs |
5683 proof - |
5466 proof - |
5684 have th00: "x * (a $ 0 * y) = a $ 0 * (x * y)" for x y |
5467 have th00: "x * (a $ 0 * y) = a $ 0 * (x * y)" for x y |
5685 by (simp add: mult.commute) |
5468 by (simp add: mult.commute) |
5686 have "?l = ?r" |
5469 have "?l = (1 + fps_X) * fps_deriv (fps_const (a $ 0) * fps_binomial c)" |
5687 apply (subst \<open>?rhs\<close>) |
5470 using that by auto |
5688 apply (subst (2) \<open>?rhs\<close>) |
5471 also have "... = fps_const c * (fps_const (a $ 0) * fps_binomial c)" |
5689 apply (clarsimp simp add: fps_eq_iff field_simps) |
5472 proof (clarsimp simp add: fps_eq_iff algebra_simps) |
5690 unfolding mult.assoc[symmetric] th00 gbinomial_mult_1 |
5473 show "a $ 0 * (c gchoose Suc n) + (of_nat n * ((c gchoose n) * a $ 0) + of_nat n * (a $ 0 * (c gchoose Suc n))) |
5691 apply (simp add: field_simps gbinomial_mult_1) |
5474 = c * ((c gchoose n) * a $ 0)" for n |
5692 done |
5475 unfolding mult.assoc[symmetric] |
|
5476 by (simp add: field_simps gbinomial_mult_1) |
|
5477 qed |
|
5478 also have "... = ?r" |
|
5479 using that by auto |
|
5480 finally have "?l = ?r" . |
5693 with eq show ?thesis .. |
5481 with eq show ?thesis .. |
5694 qed |
5482 qed |
5695 qed |
5483 qed |
5696 |
5484 |
5697 lemma fps_binomial_ODE_unique': |
5485 lemma fps_binomial_ODE_unique': |
5810 fps_inverse_power [symmetric] inverse_mult_eq_1' |
5598 fps_inverse_power [symmetric] inverse_mult_eq_1' |
5811 del: fps_const_power) |
5599 del: fps_const_power) |
5812 |
5600 |
5813 |
5601 |
5814 lemma one_minus_const_fps_X_neg_power': |
5602 lemma one_minus_const_fps_X_neg_power': |
5815 "n > 0 \<Longrightarrow> inverse ((1 - fps_const (c :: 'a :: field_char_0) * fps_X) ^ n) = |
5603 fixes c :: "'a :: field_char_0" |
5816 Abs_fps (\<lambda>k. of_nat ((n + k - 1) choose k) * c^k)" |
5604 assumes "n > 0" |
5817 apply (rule fps_ext) |
5605 shows "inverse ((1 - fps_const c * fps_X) ^ n) = Abs_fps (\<lambda>k. of_nat ((n + k - 1) choose k) * c^k)" |
5818 apply (subst one_minus_fps_X_const_neg_power, subst fps_const_neg, subst fps_compose_linear) |
5606 proof - |
5819 apply (simp add: power_mult_distrib [symmetric] mult.assoc [symmetric] |
5607 have \<section>: "\<And>j. Abs_fps (\<lambda>na. (- c) ^ na * fps_binomial (- of_nat n) $ na) $ j = |
5820 gbinomial_minus binomial_gbinomial of_nat_diff) |
5608 Abs_fps (\<lambda>k. of_nat (n + k - 1 choose k) * c ^ k) $ j" |
5821 done |
5609 using assms |
|
5610 by (simp add: gbinomial_minus binomial_gbinomial of_nat_diff flip: power_mult_distrib mult.assoc) |
|
5611 show ?thesis |
|
5612 apply (rule fps_ext) |
|
5613 using \<section> |
|
5614 by (metis (no_types, lifting) one_minus_fps_X_const_neg_power fps_const_neg fps_compose_linear fps_nth_Abs_fps) |
|
5615 qed |
5822 |
5616 |
5823 text \<open>Vandermonde's Identity as a consequence.\<close> |
5617 text \<open>Vandermonde's Identity as a consequence.\<close> |
5824 lemma gbinomial_Vandermonde: |
5618 lemma gbinomial_Vandermonde: |
5825 "sum (\<lambda>k. (a gchoose k) * (b gchoose (n - k))) {0..n} = (a + b) gchoose n" |
5619 "sum (\<lambda>k. (a gchoose k) * (b gchoose (n - k))) {0..n} = (a + b) gchoose n" |
5826 proof - |
5620 proof - |
5899 from neq(1) obtain h where h: "k = Suc h" |
5691 from neq(1) obtain h where h: "k = Suc h" |
5900 by (cases k) auto |
5692 by (cases k) auto |
5901 show ?thesis |
5693 show ?thesis |
5902 proof (cases "k = n") |
5694 proof (cases "k = n") |
5903 case True |
5695 case True |
5904 then show ?thesis |
5696 with pochhammer_minus'[where k=k and b=b] bn0 show ?thesis |
5905 using pochhammer_minus'[where k=k and b=b] |
5697 by (simp add: pochhammer_same) |
5906 apply (simp add: pochhammer_same) |
|
5907 using bn0 |
|
5908 apply (simp add: field_simps power_add[symmetric]) |
|
5909 done |
|
5910 next |
5698 next |
5911 case False |
5699 case False |
5912 with kn have kn': "k < n" |
5700 with kn have kn': "k < n" |
5913 by simp |
5701 by simp |
|
5702 have "h \<le> m" |
|
5703 using \<open>k \<le> n\<close> h m by blast |
5914 have m1nk: "?m1 n = prod (\<lambda>i. - 1) {..m}" "?m1 k = prod (\<lambda>i. - 1) {0..h}" |
5704 have m1nk: "?m1 n = prod (\<lambda>i. - 1) {..m}" "?m1 k = prod (\<lambda>i. - 1) {0..h}" |
5915 by (simp_all add: prod_constant m h) |
5705 by (simp_all add: m h) |
5916 have bnz0: "pochhammer (b - of_nat n + 1) k \<noteq> 0" |
5706 have bnz0: "pochhammer (b - of_nat n + 1) k \<noteq> 0" |
5917 using bn0 kn |
5707 using bn0 kn |
5918 unfolding pochhammer_eq_0_iff |
5708 unfolding pochhammer_eq_0_iff |
5919 apply auto |
5709 by (metis add.commute add_diff_eq nz' pochhammer_eq_0_iff) |
5920 apply (erule_tac x= "n - ka - 1" in allE) |
|
5921 apply (auto simp add: algebra_simps of_nat_diff) |
|
5922 done |
|
5923 have eq1: "prod (\<lambda>k. (1::'a) + of_nat m - of_nat k) {..h} = |
5710 have eq1: "prod (\<lambda>k. (1::'a) + of_nat m - of_nat k) {..h} = |
5924 prod of_nat {Suc (m - h) .. Suc m}" |
5711 prod of_nat {Suc (m - h) .. Suc m}" |
5925 using kn' h m |
5712 using kn' h m |
5926 by (intro prod.reindex_bij_witness[where i="\<lambda>k. Suc m - k" and j="\<lambda>k. Suc m - k"]) |
5713 by (intro prod.reindex_bij_witness[where i="\<lambda>k. Suc m - k" and j="\<lambda>k. Suc m - k"]) |
5927 (auto simp: of_nat_diff) |
5714 (auto simp: of_nat_diff) |
5928 have th1: "(?m1 k * ?p (of_nat n) k) / ?f n = 1 / of_nat(fact (n - k))" |
5715 have "(\<Prod>i = 0..<k. 1 + of_nat n - of_nat k + of_nat i) = (\<Prod>x = n - k..<n. (1::'a) + of_nat x)" |
5929 apply (simp add: pochhammer_minus field_simps) |
5716 using \<open>k \<le> n\<close> |
5930 using \<open>k \<le> n\<close> apply (simp add: fact_split [of k n]) |
|
5931 apply (simp add: pochhammer_prod) |
|
5932 using prod.atLeastLessThan_shift_bounds [where ?'a = 'a, of "\<lambda>i. 1 + of_nat i" 0 "n - k" k] |
5717 using prod.atLeastLessThan_shift_bounds [where ?'a = 'a, of "\<lambda>i. 1 + of_nat i" 0 "n - k" k] |
5933 apply (auto simp add: of_nat_diff field_simps) |
5718 by (auto simp add: of_nat_diff field_simps) |
5934 done |
5719 then have "fact (n - k) * pochhammer ((1::'a) + of_nat n - of_nat k) k = fact n" |
5935 have th20: "?m1 n * ?p b n = prod (\<lambda>i. b - of_nat i) {0..m}" |
5720 using \<open>k \<le> n\<close> |
5936 apply (simp add: pochhammer_minus field_simps m) |
5721 by (auto simp add: fact_split [of k n] pochhammer_prod field_simps) |
5937 apply (auto simp add: pochhammer_prod_rev of_nat_diff prod.atLeast_Suc_atMost_Suc_shift simp del: prod.cl_ivl_Suc) |
5722 then have th1: "(?m1 k * ?p (of_nat n) k) / ?f n = 1 / of_nat(fact (n - k))" |
5938 done |
5723 by (simp add: pochhammer_minus field_simps) |
5939 have th21:"pochhammer (b - of_nat n + 1) k = prod (\<lambda>i. b - of_nat i) {n - k .. n - 1}" |
5724 have "?m1 n * ?p b n = pochhammer (b - of_nat m) (Suc m)" |
5940 using kn apply (simp add: pochhammer_prod_rev m h prod.atLeast_Suc_atMost_Suc_shift del: prod.op_ivl_Suc del: prod.cl_ivl_Suc) |
5725 by (simp add: pochhammer_minus field_simps m) |
5941 using prod.atLeastAtMost_shift_0 [of "m - h" m, where ?'a = 'a] |
5726 also have "... = (\<Prod>i = 0..m. b - of_nat i)" |
5942 apply (auto simp add: of_nat_diff field_simps) |
5727 by (auto simp add: pochhammer_prod_rev of_nat_diff prod.atLeast_Suc_atMost_Suc_shift simp del: prod.cl_ivl_Suc) |
5943 done |
5728 finally have th20: "?m1 n * ?p b n = prod (\<lambda>i. b - of_nat i) {0..m}" . |
|
5729 have "(\<Prod>x = 0..h. b - of_nat m + of_nat (h - x)) = (\<Prod>i = m - h..m. b - of_nat i)" |
|
5730 using \<open>h \<le> m\<close> prod.atLeastAtMost_shift_0 [of "m - h" m, where ?'a = 'a] |
|
5731 by (auto simp add: of_nat_diff field_simps) |
|
5732 then have th21:"pochhammer (b - of_nat n + 1) k = prod (\<lambda>i. b - of_nat i) {n - k .. n - 1}" |
|
5733 using kn by (simp add: pochhammer_prod_rev m h prod.atLeast_Suc_atMost_Suc_shift del: prod.op_ivl_Suc del: prod.cl_ivl_Suc) |
5944 have "?m1 n * ?p b n = |
5734 have "?m1 n * ?p b n = |
5945 prod (\<lambda>i. b - of_nat i) {0.. n - k - 1} * pochhammer (b - of_nat n + 1) k" |
5735 prod (\<lambda>i. b - of_nat i) {0.. n - k - 1} * pochhammer (b - of_nat n + 1) k" |
5946 using kn' m h unfolding th20 th21 apply simp |
5736 using kn' m h unfolding th20 th21 |
5947 apply (subst prod.union_disjoint [symmetric]) |
5737 by (auto simp flip: prod.union_disjoint intro: prod.cong) |
5948 apply auto |
|
5949 apply (rule prod.cong) |
|
5950 apply auto |
|
5951 done |
|
5952 then have th2: "(?m1 n * ?p b n)/pochhammer (b - of_nat n + 1) k = |
5738 then have th2: "(?m1 n * ?p b n)/pochhammer (b - of_nat n + 1) k = |
5953 prod (\<lambda>i. b - of_nat i) {0.. n - k - 1}" |
5739 prod (\<lambda>i. b - of_nat i) {0.. n - k - 1}" |
5954 using nz' by (simp add: field_simps) |
5740 using nz' by (simp add: field_simps) |
5955 have "(?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k) = |
5741 have "(?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k) = |
5956 ((?m1 k * ?p (of_nat n) k) / ?f n) * ((?m1 n * ?p b n)/pochhammer (b - of_nat n + 1) k)" |
5742 ((?m1 k * ?p (of_nat n) k) / ?f n) * ((?m1 n * ?p b n)/pochhammer (b - of_nat n + 1) k)" |
5957 using bnz0 |
5743 using bnz0 |
5958 by (simp add: field_simps) |
5744 by (simp add: field_simps) |
5959 also have "\<dots> = b gchoose (n - k)" |
5745 also have "\<dots> = b gchoose (n - k)" |
5960 unfolding th1 th2 |
5746 unfolding th1 th2 |
5961 using kn' m h |
5747 using kn' m h |
5962 apply (simp add: field_simps gbinomial_mult_fact) |
5748 by (auto simp: field_simps gbinomial_mult_fact intro: prod.cong) |
5963 apply (rule prod.cong) |
|
5964 apply auto |
|
5965 done |
|
5966 finally show ?thesis by simp |
5749 finally show ?thesis by simp |
5967 qed |
5750 qed |
5968 qed |
5751 qed |
5969 then show ?gchoose and ?pochhammer |
5752 then show ?gchoose and ?pochhammer |
5970 apply (cases "n = 0") |
5753 using nz' by force+ |
5971 using nz' |
|
5972 apply auto |
|
5973 done |
|
5974 qed |
5754 qed |
5975 have "?r = ((a + b) gchoose n) * (of_nat (fact n) / (?m1 n * pochhammer (- b) n))" |
5755 have "?r = ((a + b) gchoose n) * (of_nat (fact n) / (?m1 n * pochhammer (- b) n))" |
5976 unfolding gbinomial_pochhammer |
5756 unfolding gbinomial_pochhammer |
5977 using bn0 by (auto simp add: field_simps) |
5757 using bn0 by (auto simp add: field_simps) |
5978 also have "\<dots> = ?l" |
5758 also have "\<dots> = ?l" |
|
5759 using bn0 |
5979 unfolding gbinomial_Vandermonde[symmetric] |
5760 unfolding gbinomial_Vandermonde[symmetric] |
5980 apply (simp add: th00) |
5761 apply (simp add: th00) |
5981 unfolding gbinomial_pochhammer |
5762 by (simp add: gbinomial_pochhammer sum_distrib_right sum_distrib_left field_simps) |
5982 using bn0 |
|
5983 apply (simp add: sum_distrib_right sum_distrib_left field_simps) |
|
5984 done |
|
5985 finally show ?thesis by simp |
5763 finally show ?thesis by simp |
5986 qed |
5764 qed |
5987 |
5765 |
5988 lemma Vandermonde_pochhammer: |
5766 lemma Vandermonde_pochhammer: |
5989 fixes a :: "'a::field_char_0" |
5767 fixes a :: "'a::field_char_0" |
6084 |
5863 |
6085 lemma fps_sin_cos_sum_of_squares: "(fps_cos c)\<^sup>2 + (fps_sin c)\<^sup>2 = 1" |
5864 lemma fps_sin_cos_sum_of_squares: "(fps_cos c)\<^sup>2 + (fps_sin c)\<^sup>2 = 1" |
6086 (is "?lhs = _") |
5865 (is "?lhs = _") |
6087 proof - |
5866 proof - |
6088 have "fps_deriv ?lhs = 0" |
5867 have "fps_deriv ?lhs = 0" |
6089 apply (simp add: fps_deriv_power fps_sin_deriv fps_cos_deriv) |
5868 by (simp add: fps_deriv_power fps_sin_deriv fps_cos_deriv field_simps flip: fps_const_neg) |
6090 apply (simp add: field_simps fps_const_neg[symmetric] del: fps_const_neg) |
|
6091 done |
|
6092 then have "?lhs = fps_const (?lhs $ 0)" |
5869 then have "?lhs = fps_const (?lhs $ 0)" |
6093 unfolding fps_deriv_eq_0_iff . |
5870 unfolding fps_deriv_eq_0_iff . |
6094 also have "\<dots> = 1" |
5871 also have "\<dots> = 1" |
6095 by (simp add: fps_eq_iff numeral_2_eq_2 fps_mult_nth fps_cos_def fps_sin_def) |
5872 by (simp add: fps_eq_iff numeral_2_eq_2 fps_mult_nth fps_cos_def fps_sin_def) |
6096 finally show ?thesis . |
5873 finally show ?thesis . |
6097 qed |
5874 qed |
6098 |
5875 |
6099 lemma fps_sin_nth_0 [simp]: "fps_sin c $ 0 = 0" |
5876 lemma fps_sin_nth_0 [simp]: "fps_sin c $ 0 = 0" |
6100 unfolding fps_sin_def by simp |
5877 unfolding fps_sin_def by simp |
6101 |
5878 |
6102 lemma fps_sin_nth_1 [simp]: "fps_sin c $ 1 = c" |
5879 lemma fps_sin_nth_1 [simp]: "fps_sin c $ Suc 0 = c" |
6103 unfolding fps_sin_def by simp |
5880 unfolding fps_sin_def by simp |
6104 |
5881 |
6105 lemma fps_sin_nth_add_2: |
5882 lemma fps_sin_nth_add_2: |
6106 "fps_sin c $ (n + 2) = - (c * c * fps_sin c $ n / (of_nat (n + 1) * of_nat (n + 2)))" |
5883 "fps_sin c $ (n + 2) = - (c * c * fps_sin c $ n / (of_nat (n + 1) * of_nat (n + 2)))" |
6107 unfolding fps_sin_def |
5884 proof (cases n) |
6108 apply (cases n) |
5885 case (Suc n') |
6109 apply simp |
5886 then show ?thesis |
6110 apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq del: of_nat_Suc fact_Suc) |
5887 unfolding fps_sin_def by (simp add: field_simps) |
6111 apply simp |
5888 qed (auto simp: fps_sin_def) |
6112 done |
5889 |
6113 |
5890 |
6114 lemma fps_cos_nth_0 [simp]: "fps_cos c $ 0 = 1" |
5891 lemma fps_cos_nth_0 [simp]: "fps_cos c $ 0 = 1" |
6115 unfolding fps_cos_def by simp |
5892 unfolding fps_cos_def by simp |
6116 |
5893 |
6117 lemma fps_cos_nth_1 [simp]: "fps_cos c $ 1 = 0" |
5894 lemma fps_cos_nth_1 [simp]: "fps_cos c $ Suc 0 = 0" |
6118 unfolding fps_cos_def by simp |
5895 unfolding fps_cos_def by simp |
6119 |
5896 |
6120 lemma fps_cos_nth_add_2: |
5897 lemma fps_cos_nth_add_2: |
6121 "fps_cos c $ (n + 2) = - (c * c * fps_cos c $ n / (of_nat (n + 1) * of_nat (n + 2)))" |
5898 "fps_cos c $ (n + 2) = - (c * c * fps_cos c $ n / (of_nat (n + 1) * of_nat (n + 2)))" |
6122 unfolding fps_cos_def |
5899 proof (cases n) |
6123 apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq del: of_nat_Suc fact_Suc) |
5900 case (Suc n') |
6124 apply simp |
5901 then show ?thesis |
6125 done |
5902 unfolding fps_cos_def by (simp add: field_simps) |
|
5903 qed (auto simp: fps_cos_def) |
6126 |
5904 |
6127 lemma nat_add_1_add_1: "(n::nat) + 1 + 1 = n + 2" |
5905 lemma nat_add_1_add_1: "(n::nat) + 1 + 1 = n + 2" |
6128 by simp |
5906 by simp |
6129 |
5907 |
6130 lemma eq_fps_sin: |
5908 lemma eq_fps_sin: |
6131 assumes 0: "a $ 0 = 0" |
5909 assumes a0: "a $ 0 = 0" |
6132 and 1: "a $ 1 = c" |
5910 and a1: "a $ 1 = c" |
6133 and 2: "fps_deriv (fps_deriv a) = - (fps_const c * fps_const c * a)" |
5911 and a2: "fps_deriv (fps_deriv a) = - (fps_const c * fps_const c * a)" |
6134 shows "a = fps_sin c" |
5912 shows "fps_sin c = a" |
6135 apply (rule fps_ext) |
5913 proof (rule fps_ext) |
6136 apply (induct_tac n rule: nat_induct2) |
5914 fix n |
6137 apply (simp add: 0) |
5915 show "fps_sin c $ n = a $ n" |
6138 apply (simp add: 1 del: One_nat_def) |
5916 proof (induction n rule: nat_induct2) |
6139 apply (rename_tac m, cut_tac f="\<lambda>a. a $ m" in arg_cong [OF 2]) |
5917 case (step n) |
6140 apply (simp add: nat_add_1_add_1 fps_sin_nth_add_2 |
5918 then have "of_nat (n + 1) * (of_nat (n + 2) * a $ (n + 2)) = |
6141 del: One_nat_def of_nat_Suc of_nat_add add_2_eq_Suc') |
5919 - (c * c * fps_sin c $ n)" |
6142 apply (subst minus_divide_left) |
5920 using a2 |
6143 apply (subst nonzero_eq_divide_eq) |
5921 by (metis fps_const_mult fps_deriv_nth fps_mult_left_const_nth fps_neg_nth nat_add_1_add_1) |
6144 apply (simp del: of_nat_add of_nat_Suc) |
5922 with step show ?case |
6145 apply (simp only: ac_simps) |
5923 by (metis (no_types, lifting) a0 add.commute add.inverse_inverse fps_sin_nth_0 fps_sin_nth_add_2 mult_divide_mult_cancel_left_if mult_minus_right nonzero_mult_div_cancel_left not_less_zero of_nat_eq_0_iff plus_1_eq_Suc zero_less_Suc) |
6146 done |
5924 qed (use assms in auto) |
|
5925 qed |
6147 |
5926 |
6148 lemma eq_fps_cos: |
5927 lemma eq_fps_cos: |
6149 assumes 0: "a $ 0 = 1" |
5928 assumes a0: "a $ 0 = 1" |
6150 and 1: "a $ 1 = 0" |
5929 and a1: "a $ 1 = 0" |
6151 and 2: "fps_deriv (fps_deriv a) = - (fps_const c * fps_const c * a)" |
5930 and a2: "fps_deriv (fps_deriv a) = - (fps_const c * fps_const c * a)" |
6152 shows "a = fps_cos c" |
5931 shows "fps_cos c = a" |
6153 apply (rule fps_ext) |
5932 proof (rule fps_ext) |
6154 apply (induct_tac n rule: nat_induct2) |
5933 fix n |
6155 apply (simp add: 0) |
5934 show "fps_cos c $ n = a $ n" |
6156 apply (simp add: 1 del: One_nat_def) |
5935 proof (induction n rule: nat_induct2) |
6157 apply (rename_tac m, cut_tac f="\<lambda>a. a $ m" in arg_cong [OF 2]) |
5936 case (step n) |
6158 apply (simp add: nat_add_1_add_1 fps_cos_nth_add_2 |
5937 then have "of_nat (n + 1) * (of_nat (n + 2) * a $ (n + 2)) = |
6159 del: One_nat_def of_nat_Suc of_nat_add add_2_eq_Suc') |
5938 - (c * c * fps_cos c $ n)" |
6160 apply (subst minus_divide_left) |
5939 using a2 |
6161 apply (subst nonzero_eq_divide_eq) |
5940 by (metis fps_const_mult fps_deriv_nth fps_mult_left_const_nth fps_neg_nth nat_add_1_add_1) |
6162 apply (simp del: of_nat_add of_nat_Suc) |
5941 with step show ?case |
6163 apply (simp only: ac_simps) |
5942 by (metis (no_types, lifting) a0 add.commute add.inverse_inverse fps_cos_nth_0 fps_cos_nth_add_2 mult_divide_mult_cancel_left_if mult_minus_right nonzero_mult_div_cancel_left not_less_zero of_nat_eq_0_iff plus_1_eq_Suc zero_less_Suc) |
6164 done |
5943 qed (use assms in auto) |
|
5944 qed |
6165 |
5945 |
6166 lemma fps_sin_add: "fps_sin (a + b) = fps_sin a * fps_cos b + fps_cos a * fps_sin b" |
5946 lemma fps_sin_add: "fps_sin (a + b) = fps_sin a * fps_cos b + fps_cos a * fps_sin b" |
6167 apply (rule eq_fps_sin [symmetric], simp, simp del: One_nat_def) |
5947 proof - |
6168 apply (simp del: fps_const_neg fps_const_add fps_const_mult |
5948 have "fps_deriv (fps_deriv (fps_sin a * fps_cos b + fps_cos a * fps_sin b)) = |
6169 add: fps_const_add [symmetric] fps_const_neg [symmetric] |
5949 - (fps_const (a + b) * fps_const (a + b) * (fps_sin a * fps_cos b + fps_cos a * fps_sin b))" |
6170 fps_sin_deriv fps_cos_deriv algebra_simps) |
5950 by (simp flip: fps_const_neg fps_const_add fps_const_mult |
6171 done |
5951 add: fps_sin_deriv fps_cos_deriv algebra_simps) |
|
5952 then show ?thesis |
|
5953 by (auto intro: eq_fps_sin) |
|
5954 qed |
|
5955 |
6172 |
5956 |
6173 lemma fps_cos_add: "fps_cos (a + b) = fps_cos a * fps_cos b - fps_sin a * fps_sin b" |
5957 lemma fps_cos_add: "fps_cos (a + b) = fps_cos a * fps_cos b - fps_sin a * fps_sin b" |
6174 apply (rule eq_fps_cos [symmetric], simp, simp del: One_nat_def) |
5958 proof - |
6175 apply (simp del: fps_const_neg fps_const_add fps_const_mult |
5959 have "fps_deriv |
6176 add: fps_const_add [symmetric] fps_const_neg [symmetric] |
5960 (fps_deriv (fps_cos a * fps_cos b - fps_sin a * fps_sin b)) = |
6177 fps_sin_deriv fps_cos_deriv algebra_simps) |
5961 - (fps_const (a + b) * fps_const (a + b) * |
6178 done |
5962 (fps_cos a * fps_cos b - fps_sin a * fps_sin b))" |
|
5963 by (simp flip: fps_const_neg fps_const_add fps_const_mult |
|
5964 add: fps_sin_deriv fps_cos_deriv algebra_simps) |
|
5965 then show ?thesis |
|
5966 by (auto intro: eq_fps_cos) |
|
5967 qed |
6179 |
5968 |
6180 lemma fps_sin_even: "fps_sin (- c) = - fps_sin c" |
5969 lemma fps_sin_even: "fps_sin (- c) = - fps_sin c" |
6181 by (simp add: fps_eq_iff fps_sin_def) |
5970 by (simp add: fps_eq_iff fps_sin_def) |
6182 |
5971 |
6183 lemma fps_cos_odd: "fps_cos (- c) = fps_cos c" |
5972 lemma fps_cos_odd: "fps_cos (- c) = fps_cos c" |
6299 |
6086 |
6300 lemma fps_hypergeo_B[simp]: "fps_hypergeo [-a] [] (- 1) = fps_binomial a" |
6087 lemma fps_hypergeo_B[simp]: "fps_hypergeo [-a] [] (- 1) = fps_binomial a" |
6301 by (simp add: fps_eq_iff gbinomial_pochhammer algebra_simps) |
6088 by (simp add: fps_eq_iff gbinomial_pochhammer algebra_simps) |
6302 |
6089 |
6303 lemma fps_hypergeo_0[simp]: "fps_hypergeo as bs c $ 0 = 1" |
6090 lemma fps_hypergeo_0[simp]: "fps_hypergeo as bs c $ 0 = 1" |
6304 apply simp |
6091 proof - |
6305 apply (subgoal_tac "\<forall>as. foldl (\<lambda>(r::'a) (a::'a). r) 1 as = 1") |
6092 have "foldl (\<lambda>(r::'a) (a::'a). r) 1 as = 1" for as |
6306 apply auto |
6093 by (induction as) auto |
6307 apply (induct_tac as) |
6094 then show ?thesis |
6308 apply auto |
6095 by auto |
6309 done |
6096 qed |
6310 |
6097 |
6311 lemma foldl_prod_prod: |
6098 lemma foldl_prod_prod: |
6312 "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 = |
6099 "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 = |
6313 foldl (\<lambda>r x. r * f x * g x) (v * w) as" |
6100 foldl (\<lambda>r x. r * f x * g x) (v * w) as" |
6314 by (induct as arbitrary: v w) (simp_all add: algebra_simps) |
6101 by (induct as arbitrary: v w) (simp_all add: algebra_simps) |
6315 |
6102 |
6316 |
6103 |
6317 lemma fps_hypergeo_rec: |
6104 lemma fps_hypergeo_rec: |
6318 "fps_hypergeo as bs c $ Suc n = ((foldl (\<lambda>r a. r* (a + of_nat n)) c as) / |
6105 "fps_hypergeo as bs c $ Suc n = ((foldl (\<lambda>r a. r* (a + of_nat n)) c as) / |
6319 (foldl (\<lambda>r b. r * (b + of_nat n)) (of_nat (Suc n)) bs )) * fps_hypergeo as bs c $ n" |
6106 (foldl (\<lambda>r b. r * (b + of_nat n)) (of_nat (Suc n)) bs )) * fps_hypergeo as bs c $ n" |
6320 apply (simp del: of_nat_Suc of_nat_add fact_Suc) |
6107 apply (simp add: foldl_mult_start del: of_nat_Suc of_nat_add fact_Suc) |
6321 apply (simp add: foldl_mult_start del: fact_Suc of_nat_Suc) |
|
6322 unfolding foldl_prod_prod[unfolded foldl_mult_start] pochhammer_Suc |
6108 unfolding foldl_prod_prod[unfolded foldl_mult_start] pochhammer_Suc |
6323 apply (simp add: algebra_simps) |
6109 by (simp add: algebra_simps) |
6324 done |
|
6325 |
6110 |
6326 lemma fps_XD_nth[simp]: "fps_XD a $ n = of_nat n * a$n" |
6111 lemma fps_XD_nth[simp]: "fps_XD a $ n = of_nat n * a$n" |
6327 by (simp add: fps_XD_def) |
6112 by (simp add: fps_XD_def) |
6328 |
6113 |
6329 lemma fps_XD_0th[simp]: "fps_XD a $ 0 = 0" |
6114 lemma fps_XD_0th[simp]: "fps_XD a $ 0 = 0" |