613 assume rp: "r > 0" |
613 assume rp: "r > 0" |
614 have th0: "(2::real) > 1" by simp |
614 have th0: "(2::real) > 1" by simp |
615 from reals_power_lt_ex[OF rp th0] |
615 from reals_power_lt_ex[OF rp th0] |
616 obtain n0 where n0: "(1/2)^n0 < r" "n0 > 0" by blast |
616 obtain n0 where n0: "(1/2)^n0 < r" "n0 > 0" by blast |
617 {fix n::nat |
617 {fix n::nat |
618 assume nn0: "n \<ge> n0" |
618 assume nn0: "n \<ge> n0" |
619 then have thnn0: "(1/2)^n <= (1/2 :: real)^n0" |
619 then have thnn0: "(1/2)^n <= (1/2 :: real)^n0" |
620 by (auto intro: power_decreasing) |
620 by (auto intro: power_decreasing) |
621 {assume "?s n = a" then have "dist (?s n) a < r" |
621 {assume "?s n = a" then have "dist (?s n) a < r" |
622 unfolding dist_eq_0_iff[of "?s n" a, symmetric] |
622 unfolding dist_eq_0_iff[of "?s n" a, symmetric] |
623 using rp by (simp del: dist_eq_0_iff)} |
623 using rp by (simp del: dist_eq_0_iff)} |
624 moreover |
624 moreover |
625 {assume neq: "?s n \<noteq> a" |
625 {assume neq: "?s n \<noteq> a" |
626 from fps_eq_least_unique[OF neq] |
626 from fps_eq_least_unique[OF neq] |
627 obtain k where k: "leastP (\<lambda>i. ?s n $ i \<noteq> a$i) k" by blast |
627 obtain k where k: "leastP (\<lambda>i. ?s n $ i \<noteq> a$i) k" by blast |
628 have th0: "\<And>(a::'a fps) b. a \<noteq> b \<longleftrightarrow> (\<exists>n. a$n \<noteq> b$n)" |
628 have th0: "\<And>(a::'a fps) b. a \<noteq> b \<longleftrightarrow> (\<exists>n. a$n \<noteq> b$n)" |
629 by (simp add: fps_eq_iff) |
629 by (simp add: fps_eq_iff) |
630 from neq have dth: "dist (?s n) a = (1/2)^k" |
630 from neq have dth: "dist (?s n) a = (1/2)^k" |
631 unfolding th0 dist_fps_def |
631 unfolding th0 dist_fps_def |
632 unfolding the1_equality[OF fps_eq_least_unique[OF neq], OF k] |
632 unfolding the1_equality[OF fps_eq_least_unique[OF neq], OF k] |
633 by (auto simp add: inverse_eq_divide power_divide) |
633 by (auto simp add: inverse_eq_divide power_divide) |
634 |
634 |
635 from k have kn: "k > n" |
635 from k have kn: "k > n" |
636 by (simp add: leastP_def setge_def fps_sum_rep_nth split:split_if_asm) |
636 by (simp add: leastP_def setge_def fps_sum_rep_nth split:split_if_asm) |
637 then have "dist (?s n) a < (1/2)^n" unfolding dth |
637 then have "dist (?s n) a < (1/2)^n" unfolding dth |
638 by (auto intro: power_strict_decreasing) |
638 by (auto intro: power_strict_decreasing) |
639 also have "\<dots> <= (1/2)^n0" using nn0 |
639 also have "\<dots> <= (1/2)^n0" using nn0 |
640 by (auto intro: power_decreasing) |
640 by (auto intro: power_decreasing) |
641 also have "\<dots> < r" using n0 by simp |
641 also have "\<dots> < r" using n0 by simp |
642 finally have "dist (?s n) a < r" .} |
642 finally have "dist (?s n) a < r" .} |
643 ultimately have "dist (?s n) a < r" by blast} |
643 ultimately have "dist (?s n) a < r" by blast} |
644 then have "\<exists>n0. \<forall> n \<ge> n0. dist (?s n) a < r " by blast} |
644 then have "\<exists>n0. \<forall> n \<ge> n0. dist (?s n) a < r " by blast} |
645 then show ?thesis unfolding LIMSEQ_def by blast |
645 then show ?thesis unfolding LIMSEQ_def by blast |
646 qed |
646 qed |
647 |
647 |
648 subsection{* Inverses of formal power series *} |
648 subsection{* Inverses of formal power series *} |
1236 let ?X = "X::('a::comm_ring_1) fps" |
1236 let ?X = "X::('a::comm_ring_1) fps" |
1237 let ?sa = "Abs_fps (\<lambda>n. setsum (\<lambda>i. a $ i) {0..n})" |
1237 let ?sa = "Abs_fps (\<lambda>n. setsum (\<lambda>i. a $ i) {0..n})" |
1238 have th0: "\<And>i. (1 - (X::'a fps)) $ i = (if i = 0 then 1 else if i = 1 then - 1 else 0)" by simp |
1238 have th0: "\<And>i. (1 - (X::'a fps)) $ i = (if i = 0 then 1 else if i = 1 then - 1 else 0)" by simp |
1239 {fix n:: nat |
1239 {fix n:: nat |
1240 {assume "n=0" hence "a$n = ((1 - ?X) * ?sa) $ n" |
1240 {assume "n=0" hence "a$n = ((1 - ?X) * ?sa) $ n" |
1241 by (simp add: fps_mult_nth)} |
1241 by (simp add: fps_mult_nth)} |
1242 moreover |
1242 moreover |
1243 {assume n0: "n \<noteq> 0" |
1243 {assume n0: "n \<noteq> 0" |
1244 then have u: "{0} \<union> ({1} \<union> {2..n}) = {0..n}" "{1}\<union>{2..n} = {1..n}" |
1244 then have u: "{0} \<union> ({1} \<union> {2..n}) = {0..n}" "{1}\<union>{2..n} = {1..n}" |
1245 "{0..n - 1}\<union>{n} = {0..n}" |
1245 "{0..n - 1}\<union>{n} = {0..n}" |
1246 by (auto simp: expand_set_eq) |
1246 by (auto simp: expand_set_eq) |
1247 have d: "{0} \<inter> ({1} \<union> {2..n}) = {}" "{1} \<inter> {2..n} = {}" |
1247 have d: "{0} \<inter> ({1} \<union> {2..n}) = {}" "{1} \<inter> {2..n} = {}" |
1248 "{0..n - 1}\<inter>{n} ={}" using n0 by simp_all |
1248 "{0..n - 1}\<inter>{n} ={}" using n0 by simp_all |
1249 have f: "finite {0}" "finite {1}" "finite {2 .. n}" |
1249 have f: "finite {0}" "finite {1}" "finite {2 .. n}" |
1250 "finite {0 .. n - 1}" "finite {n}" by simp_all |
1250 "finite {0 .. n - 1}" "finite {n}" by simp_all |
1251 have "((1 - ?X) * ?sa) $ n = setsum (\<lambda>i. (1 - ?X)$ i * ?sa $ (n - i)) {0 .. n}" |
1251 have "((1 - ?X) * ?sa) $ n = setsum (\<lambda>i. (1 - ?X)$ i * ?sa $ (n - i)) {0 .. n}" |
1252 by (simp add: fps_mult_nth) |
1252 by (simp add: fps_mult_nth) |
1253 also have "\<dots> = a$n" unfolding th0 |
1253 also have "\<dots> = a$n" unfolding th0 |
1254 unfolding setsum_Un_disjoint[OF f(1) finite_UnI[OF f(2,3)] d(1), unfolded u(1)] |
1254 unfolding setsum_Un_disjoint[OF f(1) finite_UnI[OF f(2,3)] d(1), unfolded u(1)] |
1255 unfolding setsum_Un_disjoint[OF f(2) f(3) d(2)] |
1255 unfolding setsum_Un_disjoint[OF f(2) f(3) d(2)] |
1524 {assume ?rhs then have "?lhs" by simp} |
1524 {assume ?rhs then have "?lhs" by simp} |
1525 moreover |
1525 moreover |
1526 {assume h: ?lhs |
1526 {assume h: ?lhs |
1527 {fix n have "b$n = c$n" |
1527 {fix n have "b$n = c$n" |
1528 proof(induct n rule: nat_less_induct) |
1528 proof(induct n rule: nat_less_induct) |
1529 fix n assume H: "\<forall>m<n. b$m = c$m" |
1529 fix n assume H: "\<forall>m<n. b$m = c$m" |
1530 {assume n0: "n=0" |
1530 {assume n0: "n=0" |
1531 from h have "(b oo a)$n = (c oo a)$n" by simp |
1531 from h have "(b oo a)$n = (c oo a)$n" by simp |
1532 hence "b$n = c$n" using n0 by (simp add: fps_compose_nth)} |
1532 hence "b$n = c$n" using n0 by (simp add: fps_compose_nth)} |
1533 moreover |
1533 moreover |
1534 {fix n1 assume n1: "n = Suc n1" |
1534 {fix n1 assume n1: "n = Suc n1" |
1535 have f: "finite {0 .. n1}" "finite {n}" by simp_all |
1535 have f: "finite {0 .. n1}" "finite {n}" by simp_all |
1536 have eq: "{0 .. n1} \<union> {n} = {0 .. n}" using n1 by auto |
1536 have eq: "{0 .. n1} \<union> {n} = {0 .. n}" using n1 by auto |
1537 have d: "{0 .. n1} \<inter> {n} = {}" using n1 by auto |
1537 have d: "{0 .. n1} \<inter> {n} = {}" using n1 by auto |
1538 have seq: "(\<Sum>i = 0..n1. b $ i * a ^ i $ n) = (\<Sum>i = 0..n1. c $ i * a ^ i $ n)" |
1538 have seq: "(\<Sum>i = 0..n1. b $ i * a ^ i $ n) = (\<Sum>i = 0..n1. c $ i * a ^ i $ n)" |
1539 apply (rule setsum_cong2) |
1539 apply (rule setsum_cong2) |
1540 using H n1 by auto |
1540 using H n1 by auto |
1541 have th0: "(b oo a) $n = (\<Sum>i = 0..n1. c $ i * a ^ i $ n) + b$n * (a$1)^n" |
1541 have th0: "(b oo a) $n = (\<Sum>i = 0..n1. c $ i * a ^ i $ n) + b$n * (a$1)^n" |
1542 unfolding fps_compose_nth setsum_Un_disjoint[OF f d, unfolded eq] seq |
1542 unfolding fps_compose_nth setsum_Un_disjoint[OF f d, unfolded eq] seq |
1543 using startsby_zero_power_nth_same[OF a0] |
1543 using startsby_zero_power_nth_same[OF a0] |
1544 by simp |
1544 by simp |
1545 have th1: "(c oo a) $n = (\<Sum>i = 0..n1. c $ i * a ^ i $ n) + c$n * (a$1)^n" |
1545 have th1: "(c oo a) $n = (\<Sum>i = 0..n1. c $ i * a ^ i $ n) + c$n * (a$1)^n" |
1546 unfolding fps_compose_nth setsum_Un_disjoint[OF f d, unfolded eq] |
1546 unfolding fps_compose_nth setsum_Un_disjoint[OF f d, unfolded eq] |
1547 using startsby_zero_power_nth_same[OF a0] |
1547 using startsby_zero_power_nth_same[OF a0] |
1548 by simp |
1548 by simp |
1549 from h[unfolded fps_eq_iff, rule_format, of n] th0 th1 a1 |
1549 from h[unfolded fps_eq_iff, rule_format, of n] th0 th1 a1 |
1550 have "b$n = c$n" by auto} |
1550 have "b$n = c$n" by auto} |
1551 ultimately show "b$n = c$n" by (cases n, auto) |
1551 ultimately show "b$n = c$n" by (cases n, auto) |
1552 qed} |
1552 qed} |
1553 then have ?rhs by (simp add: fps_eq_iff)} |
1553 then have ?rhs by (simp add: fps_eq_iff)} |
1554 ultimately show ?thesis by blast |
1554 ultimately show ?thesis by blast |
1555 qed |
1555 qed |
1556 |
1556 |
1578 have fths: "finite {0 ..< i}" "finite {i}" "finite {i+1..<Suc k}" by simp_all |
1578 have fths: "finite {0 ..< i}" "finite {i}" "finite {i+1..<Suc k}" by simp_all |
1579 have d: "{0 ..< i} \<inter> ({i} \<union> {i+1 ..< Suc k}) = {}" "{i} \<inter> {i+1..< Suc k} = {}" by auto |
1579 have d: "{0 ..< i} \<inter> ({i} \<union> {i+1 ..< Suc k}) = {}" "{i} \<inter> {i+1..< Suc k} = {}" by auto |
1580 have eqs: "{0..<Suc k} = {0 ..< i} \<union> ({i} \<union> {i+1 ..< Suc k})" using i by auto |
1580 have eqs: "{0..<Suc k} = {0 ..< i} \<union> ({i} \<union> {i+1 ..< Suc k})" using i by auto |
1581 from xs have "Suc n = foldl op + 0 xs" by (simp add: natpermute_def) |
1581 from xs have "Suc n = foldl op + 0 xs" by (simp add: natpermute_def) |
1582 also have "\<dots> = setsum (nth xs) {0..<Suc k}" unfolding foldl_add_setsum using xs |
1582 also have "\<dots> = setsum (nth xs) {0..<Suc k}" unfolding foldl_add_setsum using xs |
1583 by (simp add: natpermute_def) |
1583 by (simp add: natpermute_def) |
1584 also have "\<dots> = xs!i + setsum (nth xs) {0..<i} + setsum (nth xs) {i+1..<Suc k}" |
1584 also have "\<dots> = xs!i + setsum (nth xs) {0..<i} + setsum (nth xs) {i+1..<Suc k}" |
1585 unfolding eqs setsum_Un_disjoint[OF fths(1) finite_UnI[OF fths(2,3)] d(1)] |
1585 unfolding eqs setsum_Un_disjoint[OF fths(1) finite_UnI[OF fths(2,3)] d(1)] |
1586 unfolding setsum_Un_disjoint[OF fths(2) fths(3) d(2)] |
1586 unfolding setsum_Un_disjoint[OF fths(2) fths(3) d(2)] |
1587 by simp |
1587 by simp |
1588 finally have False using c' by simp} |
1588 finally have False using c' by simp} |
1589 then show "((r,Suc k,a,xs!i), r, Suc k, a, Suc n) \<in> ?R" |
1589 then show "((r,Suc k,a,xs!i), r, Suc k, a, Suc n) \<in> ?R" |
1590 apply auto by (metis not_less)} |
1590 apply auto by (metis not_less)} |
1591 {fix r k a n |
1591 {fix r k a n |
1592 show "((r,Suc k, a, 0),r, Suc k, a, Suc n) \<in> ?R" by simp} |
1592 show "((r,Suc k, a, 0),r, Suc k, a, Suc n) \<in> ?R" by simp} |
1653 let ?r = "fps_radical r (Suc k) a" |
1653 let ?r = "fps_radical r (Suc k) a" |
1654 {assume r0: "(r (Suc k) (a$0)) ^ Suc k = a$0" |
1654 {assume r0: "(r (Suc k) (a$0)) ^ Suc k = a$0" |
1655 from a0 r0 have r00: "r (Suc k) (a$0) \<noteq> 0" by auto |
1655 from a0 r0 have r00: "r (Suc k) (a$0) \<noteq> 0" by auto |
1656 {fix z have "?r ^ Suc k $ z = a$z" |
1656 {fix z have "?r ^ Suc k $ z = a$z" |
1657 proof(induct z rule: nat_less_induct) |
1657 proof(induct z rule: nat_less_induct) |
1658 fix n assume H: "\<forall>m<n. ?r ^ Suc k $ m = a$m" |
1658 fix n assume H: "\<forall>m<n. ?r ^ Suc k $ m = a$m" |
1659 {assume "n = 0" hence "?r ^ Suc k $ n = a $n" |
1659 {assume "n = 0" hence "?r ^ Suc k $ n = a $n" |
1660 using fps_radical_power_nth[of r "Suc k" a, OF r0] by simp} |
1660 using fps_radical_power_nth[of r "Suc k" a, OF r0] by simp} |
1661 moreover |
1661 moreover |
1662 {fix n1 assume n1: "n = Suc n1" |
1662 {fix n1 assume n1: "n = Suc n1" |
1663 have fK: "finite {0..k}" by simp |
1663 have fK: "finite {0..k}" by simp |
1664 have nz: "n \<noteq> 0" using n1 by arith |
1664 have nz: "n \<noteq> 0" using n1 by arith |
1665 let ?Pnk = "natpermute n (k + 1)" |
1665 let ?Pnk = "natpermute n (k + 1)" |
1666 let ?Pnkn = "{xs \<in> ?Pnk. n \<in> set xs}" |
1666 let ?Pnkn = "{xs \<in> ?Pnk. n \<in> set xs}" |
1667 let ?Pnknn = "{xs \<in> ?Pnk. n \<notin> set xs}" |
1667 let ?Pnknn = "{xs \<in> ?Pnk. n \<notin> set xs}" |
1668 have eq: "?Pnkn \<union> ?Pnknn = ?Pnk" by blast |
1668 have eq: "?Pnkn \<union> ?Pnknn = ?Pnk" by blast |
1669 have d: "?Pnkn \<inter> ?Pnknn = {}" by blast |
1669 have d: "?Pnkn \<inter> ?Pnknn = {}" by blast |
1670 have f: "finite ?Pnkn" "finite ?Pnknn" |
1670 have f: "finite ?Pnkn" "finite ?Pnknn" |
1671 using finite_Un[of ?Pnkn ?Pnknn, unfolded eq] |
1671 using finite_Un[of ?Pnkn ?Pnknn, unfolded eq] |
1672 by (metis natpermute_finite)+ |
1672 by (metis natpermute_finite)+ |
1673 let ?f = "\<lambda>v. \<Prod>j\<in>{0..k}. ?r $ v ! j" |
1673 let ?f = "\<lambda>v. \<Prod>j\<in>{0..k}. ?r $ v ! j" |
1674 have "setsum ?f ?Pnkn = setsum (\<lambda>v. ?r $ n * r (Suc k) (a $ 0) ^ k) ?Pnkn" |
1674 have "setsum ?f ?Pnkn = setsum (\<lambda>v. ?r $ n * r (Suc k) (a $ 0) ^ k) ?Pnkn" |
1675 proof(rule setsum_cong2) |
1675 proof(rule setsum_cong2) |
1676 fix v assume v: "v \<in> {xs \<in> natpermute n (k + 1). n \<in> set xs}" |
1676 fix v assume v: "v \<in> {xs \<in> natpermute n (k + 1). n \<in> set xs}" |
1677 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" |
1677 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" |
1678 from v obtain i where i: "i \<in> {0..k}" "v = replicate (k+1) 0 [i:= n]" |
1678 from v obtain i where i: "i \<in> {0..k}" "v = replicate (k+1) 0 [i:= n]" |
1679 unfolding natpermute_contain_maximal by auto |
1679 unfolding natpermute_contain_maximal by auto |
1680 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))" |
1680 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))" |
1681 apply (rule setprod_cong, simp) |
1681 apply (rule setprod_cong, simp) |
1682 using i r0 by (simp del: replicate.simps) |
1682 using i r0 by (simp del: replicate.simps) |
1683 also have "\<dots> = (fps_radical r (Suc k) a $ n) * r (Suc k) (a$0) ^ k" |
1683 also have "\<dots> = (fps_radical r (Suc k) a $ n) * r (Suc k) (a$0) ^ k" |
1684 unfolding setprod_gen_delta[OF fK] using i r0 by simp |
1684 unfolding setprod_gen_delta[OF fK] using i r0 by simp |
1685 finally show ?ths . |
1685 finally show ?ths . |
1686 qed |
1686 qed |
1687 then have "setsum ?f ?Pnkn = of_nat (k+1) * ?r $ n * r (Suc k) (a $ 0) ^ k" |
1687 then have "setsum ?f ?Pnkn = of_nat (k+1) * ?r $ n * r (Suc k) (a $ 0) ^ k" |
1688 by (simp add: natpermute_max_card[OF nz, simplified]) |
1688 by (simp add: natpermute_max_card[OF nz, simplified]) |
1689 also have "\<dots> = a$n - setsum ?f ?Pnknn" |
1689 also have "\<dots> = a$n - setsum ?f ?Pnknn" |
1690 unfolding n1 using r00 a0 by (simp add: field_simps fps_radical_def del: of_nat_Suc ) |
1690 unfolding n1 using r00 a0 by (simp add: field_simps fps_radical_def del: of_nat_Suc ) |
1691 finally have fn: "setsum ?f ?Pnkn = a$n - setsum ?f ?Pnknn" . |
1691 finally have fn: "setsum ?f ?Pnkn = a$n - setsum ?f ?Pnknn" . |
1692 have "(?r ^ Suc k)$n = setsum ?f ?Pnkn + setsum ?f ?Pnknn" |
1692 have "(?r ^ Suc k)$n = setsum ?f ?Pnkn + setsum ?f ?Pnknn" |
1693 unfolding fps_power_nth_Suc setsum_Un_disjoint[OF f d, unfolded eq] .. |
1693 unfolding fps_power_nth_Suc setsum_Un_disjoint[OF f d, unfolded eq] .. |
1694 also have "\<dots> = a$n" unfolding fn by simp |
1694 also have "\<dots> = a$n" unfolding fn by simp |
1695 finally have "?r ^ Suc k $ n = a $n" .} |
1695 finally have "?r ^ Suc k $ n = a $n" .} |
1696 ultimately show "?r ^ Suc k $ n = a $n" by (cases n, auto) |
1696 ultimately show "?r ^ Suc k $ n = a $n" by (cases n, auto) |
1697 qed } |
1697 qed } |
1698 then have ?thesis using r0 by (simp add: fps_eq_iff)} |
1698 then have ?thesis using r0 by (simp add: fps_eq_iff)} |
1699 moreover |
1699 moreover |
1700 { assume h: "(fps_radical r (Suc k) a) ^ (Suc k) = a" |
1700 { assume h: "(fps_radical r (Suc k) a) ^ (Suc k) = a" |
1715 from a0 r0 have r00: "r (Suc k) (a$0) \<noteq> 0" by auto |
1715 from a0 r0 have r00: "r (Suc k) (a$0) \<noteq> 0" by auto |
1716 {fix z have "?r ^ Suc k $ z = a$z" |
1716 {fix z have "?r ^ Suc k $ z = a$z" |
1717 proof(induct z rule: nat_less_induct) |
1717 proof(induct z rule: nat_less_induct) |
1718 fix n assume H: "\<forall>m<n. ?r ^ Suc k $ m = a$m" |
1718 fix n assume H: "\<forall>m<n. ?r ^ Suc k $ m = a$m" |
1719 {assume "n = 0" hence "?r ^ Suc k $ n = a $n" |
1719 {assume "n = 0" hence "?r ^ Suc k $ n = a $n" |
1720 using fps_radical_power_nth[of r "Suc k" a, OF r0] by simp} |
1720 using fps_radical_power_nth[of r "Suc k" a, OF r0] by simp} |
1721 moreover |
1721 moreover |
1722 {fix n1 assume n1: "n = Suc n1" |
1722 {fix n1 assume n1: "n = Suc n1" |
1723 have fK: "finite {0..k}" by simp |
1723 have fK: "finite {0..k}" by simp |
1724 have nz: "n \<noteq> 0" using n1 by arith |
1724 have nz: "n \<noteq> 0" using n1 by arith |
1725 let ?Pnk = "natpermute n (k + 1)" |
1725 let ?Pnk = "natpermute n (k + 1)" |
1726 let ?Pnkn = "{xs \<in> ?Pnk. n \<in> set xs}" |
1726 let ?Pnkn = "{xs \<in> ?Pnk. n \<in> set xs}" |
1727 let ?Pnknn = "{xs \<in> ?Pnk. n \<notin> set xs}" |
1727 let ?Pnknn = "{xs \<in> ?Pnk. n \<notin> set xs}" |
1728 have eq: "?Pnkn \<union> ?Pnknn = ?Pnk" by blast |
1728 have eq: "?Pnkn \<union> ?Pnknn = ?Pnk" by blast |
1729 have d: "?Pnkn \<inter> ?Pnknn = {}" by blast |
1729 have d: "?Pnkn \<inter> ?Pnknn = {}" by blast |
1730 have f: "finite ?Pnkn" "finite ?Pnknn" |
1730 have f: "finite ?Pnkn" "finite ?Pnknn" |
1731 using finite_Un[of ?Pnkn ?Pnknn, unfolded eq] |
1731 using finite_Un[of ?Pnkn ?Pnknn, unfolded eq] |
1732 by (metis natpermute_finite)+ |
1732 by (metis natpermute_finite)+ |
1733 let ?f = "\<lambda>v. \<Prod>j\<in>{0..k}. ?r $ v ! j" |
1733 let ?f = "\<lambda>v. \<Prod>j\<in>{0..k}. ?r $ v ! j" |
1734 have "setsum ?f ?Pnkn = setsum (\<lambda>v. ?r $ n * r (Suc k) (a $ 0) ^ k) ?Pnkn" |
1734 have "setsum ?f ?Pnkn = setsum (\<lambda>v. ?r $ n * r (Suc k) (a $ 0) ^ k) ?Pnkn" |
1735 proof(rule setsum_cong2) |
1735 proof(rule setsum_cong2) |
1736 fix v assume v: "v \<in> {xs \<in> natpermute n (k + 1). n \<in> set xs}" |
1736 fix v assume v: "v \<in> {xs \<in> natpermute n (k + 1). n \<in> set xs}" |
1737 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" |
1737 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" |
1738 from v obtain i where i: "i \<in> {0..k}" "v = replicate (k+1) 0 [i:= n]" |
1738 from v obtain i where i: "i \<in> {0..k}" "v = replicate (k+1) 0 [i:= n]" |
1739 unfolding natpermute_contain_maximal by auto |
1739 unfolding natpermute_contain_maximal by auto |
1740 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))" |
1740 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))" |
1741 apply (rule setprod_cong, simp) |
1741 apply (rule setprod_cong, simp) |
1742 using i r0 by (simp del: replicate.simps) |
1742 using i r0 by (simp del: replicate.simps) |
1743 also have "\<dots> = (fps_radical r (Suc k) a $ n) * r (Suc k) (a$0) ^ k" |
1743 also have "\<dots> = (fps_radical r (Suc k) a $ n) * r (Suc k) (a$0) ^ k" |
1744 unfolding setprod_gen_delta[OF fK] using i r0 by simp |
1744 unfolding setprod_gen_delta[OF fK] using i r0 by simp |
1745 finally show ?ths . |
1745 finally show ?ths . |
1746 qed |
1746 qed |
1747 then have "setsum ?f ?Pnkn = of_nat (k+1) * ?r $ n * r (Suc k) (a $ 0) ^ k" |
1747 then have "setsum ?f ?Pnkn = of_nat (k+1) * ?r $ n * r (Suc k) (a $ 0) ^ k" |
1748 by (simp add: natpermute_max_card[OF nz, simplified]) |
1748 by (simp add: natpermute_max_card[OF nz, simplified]) |
1749 also have "\<dots> = a$n - setsum ?f ?Pnknn" |
1749 also have "\<dots> = a$n - setsum ?f ?Pnknn" |
1750 unfolding n1 using r00 a0 by (simp add: field_simps fps_radical_def del: of_nat_Suc ) |
1750 unfolding n1 using r00 a0 by (simp add: field_simps fps_radical_def del: of_nat_Suc ) |
1751 finally have fn: "setsum ?f ?Pnkn = a$n - setsum ?f ?Pnknn" . |
1751 finally have fn: "setsum ?f ?Pnkn = a$n - setsum ?f ?Pnknn" . |
1752 have "(?r ^ Suc k)$n = setsum ?f ?Pnkn + setsum ?f ?Pnknn" |
1752 have "(?r ^ Suc k)$n = setsum ?f ?Pnkn + setsum ?f ?Pnknn" |
1753 unfolding fps_power_nth_Suc setsum_Un_disjoint[OF f d, unfolded eq] .. |
1753 unfolding fps_power_nth_Suc setsum_Un_disjoint[OF f d, unfolded eq] .. |
1754 also have "\<dots> = a$n" unfolding fn by simp |
1754 also have "\<dots> = a$n" unfolding fn by simp |
1755 finally have "?r ^ Suc k $ n = a $n" .} |
1755 finally have "?r ^ Suc k $ n = a $n" .} |
1756 ultimately show "?r ^ Suc k $ n = a $n" by (cases n, auto) |
1756 ultimately show "?r ^ Suc k $ n = a $n" by (cases n, auto) |
1757 qed } |
1757 qed } |
1758 then show ?thesis by (simp add: fps_eq_iff) |
1758 then show ?thesis by (simp add: fps_eq_iff) |
1759 qed |
1759 qed |
1760 |
1760 |
1781 have ceq: "card {0..k} = Suc k" by simp |
1781 have ceq: "card {0..k} = Suc k" by simp |
1782 have fk: "finite {0..k}" by simp |
1782 have fk: "finite {0..k}" by simp |
1783 from a0 have a0r0: "a$0 = ?r$0" by simp |
1783 from a0 have a0r0: "a$0 = ?r$0" by simp |
1784 {fix n have "a $ n = ?r $ n" |
1784 {fix n have "a $ n = ?r $ n" |
1785 proof(induct n rule: nat_less_induct) |
1785 proof(induct n rule: nat_less_induct) |
1786 fix n assume h: "\<forall>m<n. a$m = ?r $m" |
1786 fix n assume h: "\<forall>m<n. a$m = ?r $m" |
1787 {assume "n = 0" hence "a$n = ?r $n" using a0 by simp } |
1787 {assume "n = 0" hence "a$n = ?r $n" using a0 by simp } |
1788 moreover |
1788 moreover |
1789 {fix n1 assume n1: "n = Suc n1" |
1789 {fix n1 assume n1: "n = Suc n1" |
1790 have fK: "finite {0..k}" by simp |
1790 have fK: "finite {0..k}" by simp |
1791 have nz: "n \<noteq> 0" using n1 by arith |
1791 have nz: "n \<noteq> 0" using n1 by arith |
1792 let ?Pnk = "natpermute n (Suc k)" |
1792 let ?Pnk = "natpermute n (Suc k)" |
1793 let ?Pnkn = "{xs \<in> ?Pnk. n \<in> set xs}" |
1793 let ?Pnkn = "{xs \<in> ?Pnk. n \<in> set xs}" |
1794 let ?Pnknn = "{xs \<in> ?Pnk. n \<notin> set xs}" |
1794 let ?Pnknn = "{xs \<in> ?Pnk. n \<notin> set xs}" |
1795 have eq: "?Pnkn \<union> ?Pnknn = ?Pnk" by blast |
1795 have eq: "?Pnkn \<union> ?Pnknn = ?Pnk" by blast |
1796 have d: "?Pnkn \<inter> ?Pnknn = {}" by blast |
1796 have d: "?Pnkn \<inter> ?Pnknn = {}" by blast |
1797 have f: "finite ?Pnkn" "finite ?Pnknn" |
1797 have f: "finite ?Pnkn" "finite ?Pnknn" |
1798 using finite_Un[of ?Pnkn ?Pnknn, unfolded eq] |
1798 using finite_Un[of ?Pnkn ?Pnknn, unfolded eq] |
1799 by (metis natpermute_finite)+ |
1799 by (metis natpermute_finite)+ |
1800 let ?f = "\<lambda>v. \<Prod>j\<in>{0..k}. ?r $ v ! j" |
1800 let ?f = "\<lambda>v. \<Prod>j\<in>{0..k}. ?r $ v ! j" |
1801 let ?g = "\<lambda>v. \<Prod>j\<in>{0..k}. a $ v ! j" |
1801 let ?g = "\<lambda>v. \<Prod>j\<in>{0..k}. a $ v ! j" |
1802 have "setsum ?g ?Pnkn = setsum (\<lambda>v. a $ n * (?r$0)^k) ?Pnkn" |
1802 have "setsum ?g ?Pnkn = setsum (\<lambda>v. a $ n * (?r$0)^k) ?Pnkn" |
1803 proof(rule setsum_cong2) |
1803 proof(rule setsum_cong2) |
1804 fix v assume v: "v \<in> {xs \<in> natpermute n (Suc k). n \<in> set xs}" |
1804 fix v assume v: "v \<in> {xs \<in> natpermute n (Suc k). n \<in> set xs}" |
1805 let ?ths = "(\<Prod>j\<in>{0..k}. a $ v ! j) = a $ n * (?r$0)^k" |
1805 let ?ths = "(\<Prod>j\<in>{0..k}. a $ v ! j) = a $ n * (?r$0)^k" |
1806 from v obtain i where i: "i \<in> {0..k}" "v = replicate (k+1) 0 [i:= n]" |
1806 from v obtain i where i: "i \<in> {0..k}" "v = replicate (k+1) 0 [i:= n]" |
1807 unfolding Suc_eq_plus1 natpermute_contain_maximal by (auto simp del: replicate.simps) |
1807 unfolding Suc_eq_plus1 natpermute_contain_maximal by (auto simp del: replicate.simps) |
1808 have "(\<Prod>j\<in>{0..k}. a $ v ! j) = (\<Prod>j\<in>{0..k}. if j = i then a $ n else r (Suc k) (b$0))" |
1808 have "(\<Prod>j\<in>{0..k}. a $ v ! j) = (\<Prod>j\<in>{0..k}. if j = i then a $ n else r (Suc k) (b$0))" |
1809 apply (rule setprod_cong, simp) |
1809 apply (rule setprod_cong, simp) |
1810 using i a0 by (simp del: replicate.simps) |
1810 using i a0 by (simp del: replicate.simps) |
1811 also have "\<dots> = a $ n * (?r $ 0)^k" |
1811 also have "\<dots> = a $ n * (?r $ 0)^k" |
1812 unfolding setprod_gen_delta[OF fK] using i by simp |
1812 unfolding setprod_gen_delta[OF fK] using i by simp |
1813 finally show ?ths . |
1813 finally show ?ths . |
1814 qed |
1814 qed |
1815 then have th0: "setsum ?g ?Pnkn = of_nat (k+1) * a $ n * (?r $ 0)^k" |
1815 then have th0: "setsum ?g ?Pnkn = of_nat (k+1) * a $ n * (?r $ 0)^k" |
1816 by (simp add: natpermute_max_card[OF nz, simplified]) |
1816 by (simp add: natpermute_max_card[OF nz, simplified]) |
1817 have th1: "setsum ?g ?Pnknn = setsum ?f ?Pnknn" |
1817 have th1: "setsum ?g ?Pnknn = setsum ?f ?Pnknn" |
1818 proof (rule setsum_cong2, rule setprod_cong, simp) |
1818 proof (rule setsum_cong2, rule setprod_cong, simp) |
1819 fix xs i assume xs: "xs \<in> ?Pnknn" and i: "i \<in> {0..k}" |
1819 fix xs i assume xs: "xs \<in> ?Pnknn" and i: "i \<in> {0..k}" |
1820 {assume c: "n \<le> xs ! i" |
1820 {assume c: "n \<le> xs ! i" |
1821 from xs i have "xs !i \<noteq> n" by (auto simp add: in_set_conv_nth natpermute_def) |
1821 from xs i have "xs !i \<noteq> n" by (auto simp add: in_set_conv_nth natpermute_def) |
1822 with c have c': "n < xs!i" by arith |
1822 with c have c': "n < xs!i" by arith |
1823 have fths: "finite {0 ..< i}" "finite {i}" "finite {i+1..<Suc k}" by simp_all |
1823 have fths: "finite {0 ..< i}" "finite {i}" "finite {i+1..<Suc k}" by simp_all |
1824 have d: "{0 ..< i} \<inter> ({i} \<union> {i+1 ..< Suc k}) = {}" "{i} \<inter> {i+1..< Suc k} = {}" by auto |
1824 have d: "{0 ..< i} \<inter> ({i} \<union> {i+1 ..< Suc k}) = {}" "{i} \<inter> {i+1..< Suc k} = {}" by auto |
1825 have eqs: "{0..<Suc k} = {0 ..< i} \<union> ({i} \<union> {i+1 ..< Suc k})" using i by auto |
1825 have eqs: "{0..<Suc k} = {0 ..< i} \<union> ({i} \<union> {i+1 ..< Suc k})" using i by auto |
1826 from xs have "n = foldl op + 0 xs" by (simp add: natpermute_def) |
1826 from xs have "n = foldl op + 0 xs" by (simp add: natpermute_def) |
1827 also have "\<dots> = setsum (nth xs) {0..<Suc k}" unfolding foldl_add_setsum using xs |
1827 also have "\<dots> = setsum (nth xs) {0..<Suc k}" unfolding foldl_add_setsum using xs |
1828 by (simp add: natpermute_def) |
1828 by (simp add: natpermute_def) |
1829 also have "\<dots> = xs!i + setsum (nth xs) {0..<i} + setsum (nth xs) {i+1..<Suc k}" |
1829 also have "\<dots> = xs!i + setsum (nth xs) {0..<i} + setsum (nth xs) {i+1..<Suc k}" |
1830 unfolding eqs setsum_Un_disjoint[OF fths(1) finite_UnI[OF fths(2,3)] d(1)] |
1830 unfolding eqs setsum_Un_disjoint[OF fths(1) finite_UnI[OF fths(2,3)] d(1)] |
1831 unfolding setsum_Un_disjoint[OF fths(2) fths(3) d(2)] |
1831 unfolding setsum_Un_disjoint[OF fths(2) fths(3) d(2)] |
1832 by simp |
1832 by simp |
1833 finally have False using c' by simp} |
1833 finally have False using c' by simp} |
1834 then have thn: "xs!i < n" by arith |
1834 then have thn: "xs!i < n" by arith |
1835 from h[rule_format, OF thn] |
1835 from h[rule_format, OF thn] |
1836 show "a$(xs !i) = ?r$(xs!i)" . |
1836 show "a$(xs !i) = ?r$(xs!i)" . |
1837 qed |
1837 qed |
1838 have th00: "\<And>(x::'a). of_nat (Suc k) * (x * inverse (of_nat (Suc k))) = x" |
1838 have th00: "\<And>(x::'a). of_nat (Suc k) * (x * inverse (of_nat (Suc k))) = x" |
1839 by (simp add: field_simps del: of_nat_Suc) |
1839 by (simp add: field_simps del: of_nat_Suc) |
1840 from H have "b$n = a^Suc k $ n" by (simp add: fps_eq_iff) |
1840 from H have "b$n = a^Suc k $ n" by (simp add: fps_eq_iff) |
1841 also have "a ^ Suc k$n = setsum ?g ?Pnkn + setsum ?g ?Pnknn" |
1841 also have "a ^ Suc k$n = setsum ?g ?Pnkn + setsum ?g ?Pnknn" |
1842 unfolding fps_power_nth_Suc |
1842 unfolding fps_power_nth_Suc |
1843 using setsum_Un_disjoint[OF f d, unfolded Suc_eq_plus1[symmetric], |
1843 using setsum_Un_disjoint[OF f d, unfolded Suc_eq_plus1[symmetric], |
1844 unfolded eq, of ?g] by simp |
1844 unfolded eq, of ?g] by simp |
1845 also have "\<dots> = of_nat (k+1) * a $ n * (?r $ 0)^k + setsum ?f ?Pnknn" unfolding th0 th1 .. |
1845 also have "\<dots> = of_nat (k+1) * a $ n * (?r $ 0)^k + setsum ?f ?Pnknn" unfolding th0 th1 .. |
1846 finally have "of_nat (k+1) * a $ n * (?r $ 0)^k = b$n - setsum ?f ?Pnknn" by simp |
1846 finally have "of_nat (k+1) * a $ n * (?r $ 0)^k = b$n - setsum ?f ?Pnknn" by simp |
1847 then have "a$n = (b$n - setsum ?f ?Pnknn) / (of_nat (k+1) * (?r $ 0)^k)" |
1847 then have "a$n = (b$n - setsum ?f ?Pnknn) / (of_nat (k+1) * (?r $ 0)^k)" |
1848 apply - |
1848 apply - |
1849 apply (rule eq_divide_imp') |
1849 apply (rule eq_divide_imp') |
1850 using r00 |
1850 using r00 |
1851 apply (simp del: of_nat_Suc) |
1851 apply (simp del: of_nat_Suc) |
1852 by (simp add: mult_ac) |
1852 by (simp add: mult_ac) |
1853 then have "a$n = ?r $n" |
1853 then have "a$n = ?r $n" |
1854 apply (simp del: of_nat_Suc) |
1854 apply (simp del: of_nat_Suc) |
1855 unfolding fps_radical_def n1 |
1855 unfolding fps_radical_def n1 |
1856 by (simp add: field_simps n1 th00 del: of_nat_Suc)} |
1856 by (simp add: field_simps n1 th00 del: of_nat_Suc)} |
1857 ultimately show "a$n = ?r $ n" by (cases n, auto) |
1857 ultimately show "a$n = ?r $ n" by (cases n, auto) |
1858 qed} |
1858 qed} |
1859 then have "a = ?r" by (simp add: fps_eq_iff)} |
1859 then have "a = ?r" by (simp add: fps_eq_iff)} |
1860 ultimately show ?thesis by blast |
1860 ultimately show ?thesis by blast |
1861 qed |
1861 qed |
1862 |
1862 |
2853 let ?p = "%(x::'a). pochhammer (- x)" |
2853 let ?p = "%(x::'a). pochhammer (- x)" |
2854 from b have bn0: "?p b n \<noteq> 0" unfolding pochhammer_eq_0_iff by simp |
2854 from b have bn0: "?p b n \<noteq> 0" unfolding pochhammer_eq_0_iff by simp |
2855 {fix k assume kn: "k \<in> {0..n}" |
2855 {fix k assume kn: "k \<in> {0..n}" |
2856 {assume c:"pochhammer (b - of_nat n + 1) n = 0" |
2856 {assume c:"pochhammer (b - of_nat n + 1) n = 0" |
2857 then obtain j where j: "j < n" "b - of_nat n + 1 = - of_nat j" |
2857 then obtain j where j: "j < n" "b - of_nat n + 1 = - of_nat j" |
2858 unfolding pochhammer_eq_0_iff by blast |
2858 unfolding pochhammer_eq_0_iff by blast |
2859 from j have "b = of_nat n - of_nat j - of_nat 1" |
2859 from j have "b = of_nat n - of_nat j - of_nat 1" |
2860 by (simp add: algebra_simps) |
2860 by (simp add: algebra_simps) |
2861 then have "b = of_nat (n - j - 1)" |
2861 then have "b = of_nat (n - j - 1)" |
2862 using j kn by (simp add: of_nat_diff) |
2862 using j kn by (simp add: of_nat_diff) |
2863 with b have False using j by auto} |
2863 with b have False using j by auto} |
2864 then have nz: "pochhammer (1 + b - of_nat n) n \<noteq> 0" |
2864 then have nz: "pochhammer (1 + b - of_nat n) n \<noteq> 0" |
2865 by (auto simp add: algebra_simps) |
2865 by (auto simp add: algebra_simps) |
2866 |
2866 |
2867 from nz kn have nz': "pochhammer (1 + b - of_nat n) k \<noteq> 0" |
2867 from nz kn have nz': "pochhammer (1 + b - of_nat n) k \<noteq> 0" |
2868 by (simp add: pochhammer_neq_0_mono) |
2868 by (simp add: pochhammer_neq_0_mono) |
2869 {assume k0: "k = 0 \<or> n =0" |
2869 {assume k0: "k = 0 \<or> n =0" |
2870 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)" |
2870 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)" |
2871 using kn |
2871 using kn |
2872 by (cases "k=0", simp_all add: gbinomial_pochhammer)} |
2872 by (cases "k=0", simp_all add: gbinomial_pochhammer)} |
2873 moreover |
2873 moreover |
2874 {assume n0: "n \<noteq> 0" and k0: "k \<noteq> 0" |
2874 {assume n0: "n \<noteq> 0" and k0: "k \<noteq> 0" |
2875 then obtain m where m: "n = Suc m" by (cases n, auto) |
2875 then obtain m where m: "n = Suc m" by (cases n, auto) |
2876 from k0 obtain h where h: "k = Suc h" by (cases k, auto) |
2876 from k0 obtain h where h: "k = Suc h" by (cases k, auto) |
2877 {assume kn: "k = n" |
2877 {assume kn: "k = n" |
2878 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)" |
2878 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)" |
2879 using kn pochhammer_minus'[where k=k and n=n and b=b] |
2879 using kn pochhammer_minus'[where k=k and n=n and b=b] |
2880 apply (simp add: pochhammer_same) |
2880 apply (simp add: pochhammer_same) |
2881 using bn0 |
2881 using bn0 |
2882 by (simp add: field_simps power_add[symmetric])} |
2882 by (simp add: field_simps power_add[symmetric])} |
2883 moreover |
2883 moreover |
2884 {assume nk: "k \<noteq> n" |
2884 {assume nk: "k \<noteq> n" |
2885 have m1nk: "?m1 n = setprod (%i. - 1) {0..m}" |
2885 have m1nk: "?m1 n = setprod (%i. - 1) {0..m}" |
2886 "?m1 k = setprod (%i. - 1) {0..h}" |
2886 "?m1 k = setprod (%i. - 1) {0..h}" |
2887 by (simp_all add: setprod_constant m h) |
2887 by (simp_all add: setprod_constant m h) |
2888 from kn nk have kn': "k < n" by simp |
2888 from kn nk have kn': "k < n" by simp |
2889 have bnz0: "pochhammer (b - of_nat n + 1) k \<noteq> 0" |
2889 have bnz0: "pochhammer (b - of_nat n + 1) k \<noteq> 0" |
2890 using bn0 kn |
2890 using bn0 kn |
2891 unfolding pochhammer_eq_0_iff |
2891 unfolding pochhammer_eq_0_iff |
2892 apply auto |
2892 apply auto |
2893 apply (erule_tac x= "n - ka - 1" in allE) |
2893 apply (erule_tac x= "n - ka - 1" in allE) |
2894 by (auto simp add: algebra_simps of_nat_diff) |
2894 by (auto simp add: algebra_simps of_nat_diff) |
2895 have eq1: "setprod (%k. (1::'a) + of_nat m - of_nat k) {0 .. h} = setprod of_nat {Suc (m - h) .. Suc m}" |
2895 have eq1: "setprod (%k. (1::'a) + of_nat m - of_nat k) {0 .. h} = setprod of_nat {Suc (m - h) .. Suc m}" |
2896 apply (rule strong_setprod_reindex_cong[where f="%k. Suc m - k "]) |
2896 apply (rule strong_setprod_reindex_cong[where f="%k. Suc m - k "]) |
2897 using kn' h m |
2897 using kn' h m |
2898 apply (auto simp add: inj_on_def image_def) |
2898 apply (auto simp add: inj_on_def image_def) |
2899 apply (rule_tac x="Suc m - x" in bexI) |
2899 apply (rule_tac x="Suc m - x" in bexI) |
2900 apply (simp_all add: of_nat_diff) |
2900 apply (simp_all add: of_nat_diff) |
2901 done |
2901 done |
2902 |
2902 |
2903 have th1: "(?m1 k * ?p (of_nat n) k) / ?f n = 1 / of_nat(fact (n - k))" |
2903 have th1: "(?m1 k * ?p (of_nat n) k) / ?f n = 1 / of_nat(fact (n - k))" |
2904 unfolding m1nk |
2904 unfolding m1nk |
2905 |
2905 |
2906 unfolding m h pochhammer_Suc_setprod |
2906 unfolding m h pochhammer_Suc_setprod |
2907 apply (simp add: field_simps del: fact_Suc id_def) |
2907 apply (simp add: field_simps del: fact_Suc id_def) |
2908 unfolding fact_altdef_nat id_def |
2908 unfolding fact_altdef_nat id_def |
2909 unfolding of_nat_setprod |
2909 unfolding of_nat_setprod |
2910 unfolding setprod_timesf[symmetric] |
2910 unfolding setprod_timesf[symmetric] |
2911 apply auto |
2911 apply auto |
2912 unfolding eq1 |
2912 unfolding eq1 |
2913 apply (subst setprod_Un_disjoint[symmetric]) |
2913 apply (subst setprod_Un_disjoint[symmetric]) |
2914 apply (auto) |
2914 apply (auto) |
2915 apply (rule setprod_cong) |
2915 apply (rule setprod_cong) |
2916 apply auto |
2916 apply auto |
2917 done |
2917 done |
2918 have th20: "?m1 n * ?p b n = setprod (%i. b - of_nat i) {0..m}" |
2918 have th20: "?m1 n * ?p b n = setprod (%i. b - of_nat i) {0..m}" |
2919 unfolding m1nk |
2919 unfolding m1nk |
2920 unfolding m h pochhammer_Suc_setprod |
2920 unfolding m h pochhammer_Suc_setprod |
2921 unfolding setprod_timesf[symmetric] |
2921 unfolding setprod_timesf[symmetric] |
2922 apply (rule setprod_cong) |
2922 apply (rule setprod_cong) |
2923 apply auto |
2923 apply auto |
2924 done |
2924 done |
2925 have th21:"pochhammer (b - of_nat n + 1) k = setprod (%i. b - of_nat i) {n - k .. n - 1}" |
2925 have th21:"pochhammer (b - of_nat n + 1) k = setprod (%i. b - of_nat i) {n - k .. n - 1}" |
2926 unfolding h m |
2926 unfolding h m |
2927 unfolding pochhammer_Suc_setprod |
2927 unfolding pochhammer_Suc_setprod |
2928 apply (rule strong_setprod_reindex_cong[where f="%k. n - 1 - k"]) |
2928 apply (rule strong_setprod_reindex_cong[where f="%k. n - 1 - k"]) |
2929 using kn |
2929 using kn |
2930 apply (auto simp add: inj_on_def m h image_def) |
2930 apply (auto simp add: inj_on_def m h image_def) |
2931 apply (rule_tac x= "m - x" in bexI) |
2931 apply (rule_tac x= "m - x" in bexI) |
2932 by (auto simp add: of_nat_diff) |
2932 by (auto simp add: of_nat_diff) |
2933 |
2933 |
2934 have "?m1 n * ?p b n = pochhammer (b - of_nat n + 1) k * setprod (%i. b - of_nat i) {0.. n - k - 1}" |
2934 have "?m1 n * ?p b n = pochhammer (b - of_nat n + 1) k * setprod (%i. b - of_nat i) {0.. n - k - 1}" |
2935 unfolding th20 th21 |
2935 unfolding th20 th21 |
2936 unfolding h m |
2936 unfolding h m |
2937 apply (subst setprod_Un_disjoint[symmetric]) |
2937 apply (subst setprod_Un_disjoint[symmetric]) |
2938 using kn' h m |
2938 using kn' h m |
2939 apply auto |
2939 apply auto |
2940 apply (rule setprod_cong) |
2940 apply (rule setprod_cong) |
2941 apply auto |
2941 apply auto |
2942 done |
2942 done |
2943 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}" |
2943 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}" |
2944 using nz' by (simp add: field_simps) |
2944 using nz' by (simp add: field_simps) |
2945 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)" |
2945 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)" |
2946 using bnz0 |
2946 using bnz0 |
2947 by (simp add: field_simps) |
2947 by (simp add: field_simps) |
2948 also have "\<dots> = b gchoose (n - k)" |
2948 also have "\<dots> = b gchoose (n - k)" |
2949 unfolding th1 th2 |
2949 unfolding th1 th2 |
2950 using kn' by (simp add: gbinomial_def) |
2950 using kn' by (simp add: gbinomial_def) |
2951 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} |
2951 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} |
2952 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)" |
2952 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)" |
2953 by (cases "k =n", auto)} |
2953 by (cases "k =n", auto)} |
2954 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 " |
2954 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 " |
2955 using nz' |
2955 using nz' |
2956 apply (cases "n=0", auto) |
2956 apply (cases "n=0", auto) |
2957 by (cases "k", auto)} |
2957 by (cases "k", auto)} |
2958 note th00 = this |
2958 note th00 = this |
3032 fix n::nat |
3032 fix n::nat |
3033 {assume en: "odd n" |
3033 {assume en: "odd n" |
3034 from en have n0: "n \<noteq>0 " by presburger |
3034 from en have n0: "n \<noteq>0 " by presburger |
3035 have "?lhs$n = of_nat (n+1) * (fps_cos c $ (n+1))" by simp |
3035 have "?lhs$n = of_nat (n+1) * (fps_cos c $ (n+1))" by simp |
3036 also have "\<dots> = of_nat (n+1) * ((- 1)^((n + 1) div 2) * c^Suc n / of_nat (fact (Suc n)))" |
3036 also have "\<dots> = of_nat (n+1) * ((- 1)^((n + 1) div 2) * c^Suc n / of_nat (fact (Suc n)))" |
3037 using en by (simp add: fps_cos_def) |
3037 using en by (simp add: fps_cos_def) |
3038 also have "\<dots> = (- 1)^((n + 1) div 2)*c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))" |
3038 also have "\<dots> = (- 1)^((n + 1) div 2)*c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))" |
3039 unfolding fact_Suc of_nat_mult |
3039 unfolding fact_Suc of_nat_mult |
3040 by (simp add: field_simps del: of_nat_add of_nat_Suc) |
3040 by (simp add: field_simps del: of_nat_add of_nat_Suc) |
3041 also have "\<dots> = (- 1)^((n + 1) div 2) * c^Suc n / of_nat (fact n)" |
3041 also have "\<dots> = (- 1)^((n + 1) div 2) * c^Suc n / of_nat (fact n)" |
3042 by (simp add: field_simps del: of_nat_add of_nat_Suc) |
3042 by (simp add: field_simps del: of_nat_add of_nat_Suc) |
3043 also have "\<dots> = (- ((- 1)^((n - 1) div 2))) * c^Suc n / of_nat (fact n)" |
3043 also have "\<dots> = (- ((- 1)^((n - 1) div 2))) * c^Suc n / of_nat (fact n)" |
3044 unfolding th0 unfolding th1[OF en] by simp |
3044 unfolding th0 unfolding th1[OF en] by simp |
3045 finally have "?lhs $n = ?rhs$n" using en |
3045 finally have "?lhs $n = ?rhs$n" using en |
3046 by (simp add: fps_sin_def ring_simps power_Suc)} |
3046 by (simp add: fps_sin_def ring_simps power_Suc)} |
3047 then show "?lhs $ n = ?rhs $ n" |
3047 then show "?lhs $ n = ?rhs $ n" |
3048 by (cases "even n", simp_all add: fps_deriv_def fps_sin_def |
3048 by (cases "even n", simp_all add: fps_deriv_def fps_sin_def |
3049 fps_cos_def) |
3049 fps_cos_def) |
3050 qed |
3050 qed |
3051 |
3051 |
3052 lemma fps_sin_cos_sum_of_squares: |
3052 lemma fps_sin_cos_sum_of_squares: |
3053 "fps_cos c ^ 2 + fps_sin c ^ 2 = 1" (is "?lhs = 1") |
3053 "fps_cos c ^ 2 + fps_sin c ^ 2 = 1" (is "?lhs = 1") |
3054 proof- |
3054 proof- |