diff -r 1943db7bc34c -r e4b18828a817 src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Sun Aug 25 20:57:09 2013 +0200 +++ b/src/HOL/Library/Formal_Power_Series.thy Sun Aug 25 21:25:17 2013 +0200 @@ -139,7 +139,8 @@ qed lemma fps_mult_assoc_lemma: - fixes k :: nat and f :: "nat \ nat \ nat \ 'a::comm_monoid_add" + fixes k :: nat + and f :: "nat \ nat \ nat \ 'a::comm_monoid_add" shows "(\j=0..k. \i=0..j. f i (j - i) (n - j)) = (\j=0..k. \i=0..k - j. f j i (n - j - i))" by (induct k) (simp_all add: Suc_diff_le setsum_addf add_assoc) @@ -254,7 +255,7 @@ instance fps :: (semiring_0) semiring_0 proof - fix a:: "'a fps" + fix a :: "'a fps" show "0 * a = 0" by (simp add: fps_ext fps_mult_nth) show "a * 0 = 0" by (simp add: fps_ext fps_mult_nth) qed @@ -392,22 +393,19 @@ by (induct n) auto definition "X = Abs_fps (\n. if n = 1 then 1 else 0)" -lemma X_mult_nth[simp]: "(X * (f :: ('a::semiring_1) fps)) $n = (if n = 0 then 0 else f $ (n - 1))" -proof - - { - assume n: "n \ 0" - have "(X * f) $n = (\i = 0..n. X $ i * f $ (n - i))" - by (simp add: fps_mult_nth) - also have "\ = f $ (n - 1)" - using n by (simp add: X_def mult_delta_left setsum_delta) - finally have ?thesis using n by simp - } - moreover - { - assume n: "n=0" - hence ?thesis by (simp add: fps_mult_nth X_def) - } - ultimately show ?thesis by blast + +lemma X_mult_nth [simp]: + "(X * (f :: ('a::semiring_1) fps)) $n = (if n = 0 then 0 else f $ (n - 1))" +proof (cases "n = 0") + case False + have "(X * f) $n = (\i = 0..n. X $ i * f $ (n - i))" + by (simp add: fps_mult_nth) + also have "\ = f $ (n - 1)" + using False by (simp add: X_def mult_delta_left setsum_delta) + finally show ?thesis using False by simp +next + case True + then show ?thesis by (simp add: fps_mult_nth X_def) qed lemma X_mult_right_nth[simp]: @@ -911,17 +909,12 @@ lemma fps_deriv_setsum: "fps_deriv (setsum f S) = setsum (\i. fps_deriv (f i :: ('a::comm_ring_1) fps)) S" -proof - - { - assume "\ finite S" - then have ?thesis by simp - } - moreover - { - assume fS: "finite S" - have ?thesis by (induct rule: finite_induct [OF fS]) simp_all - } - ultimately show ?thesis by blast +proof (cases "finite S") + case False + then show ?thesis by simp +next + case True + show ?thesis by (induct rule: finite_induct [OF True]) simp_all qed lemma fps_deriv_eq_0_iff [simp]: @@ -959,10 +952,7 @@ lemma fps_deriv_eq_iff_ex: "(fps_deriv f = fps_deriv g) \ (\(c::'a::{idom,semiring_char_0}). f = fps_const c + g)" - apply auto - unfolding fps_deriv_eq_iff - apply blast - done + by (auto simp: fps_deriv_eq_iff) fun fps_nth_deriv :: "nat \ ('a::semiring_1) fps \ 'a fps" @@ -1272,14 +1262,16 @@ "fps_integral (fps_const a * f + fps_const b * g) (a*a0 + b*b0) = fps_const a * fps_integral f a0 + fps_const b * fps_integral g b0" (is "?l = ?r") -proof- +proof - have "fps_deriv ?l = fps_deriv ?r" by (simp add: fps_deriv_fps_integral) moreover have "?l$0 = ?r$0" by (simp add: fps_integral_def) ultimately show ?thesis unfolding fps_deriv_eq_iff by auto qed + subsection {* Composition of FPSs *} + definition fps_compose :: "('a::semiring_1) fps \ 'a fps \ 'a fps" (infixl "oo" 55) where fps_compose_def: "a oo b = Abs_fps (\n. setsum (\i. a$i * (b^i$n)) {0..n})" @@ -1341,7 +1333,8 @@ then show ?thesis by (simp add: fps_eq_iff) qed -subsubsection{* Rule 2*} + +subsubsection {* Rule 2*} (* We can not reach the form of Wilf, but still near to it using rewrite rules*) (* If f reprents {a_n} and P is a polynomial, then @@ -1372,12 +1365,14 @@ "(XD ^^ k) (a:: ('a::{comm_ring_1}) fps) = Abs_fps (\n. (of_nat n ^ k) * a$n)" by (induct k arbitrary: a) (simp_all add: XD_def fps_eq_iff field_simps del: One_nat_def) + subsubsection{* Rule 3 is trivial and is given by @{text fps_times_def}*} + subsubsection{* Rule 5 --- summation and "division" by (1 - X)*} lemma fps_divide_X_minus1_setsum_lemma: "a = ((1::('a::comm_ring_1) fps) - X) * Abs_fps (\n. setsum (\i. a $ i) {0..n})" -proof- +proof - let ?X = "X::('a::comm_ring_1) fps" let ?sa = "Abs_fps (\n. setsum (\i. a $ i) {0..n})" have th0: "\i. (1 - (X::'a fps)) $ i = (if i = 0 then 1 else if i = 1 then - 1 else 0)" @@ -1417,7 +1412,7 @@ qed lemma fps_divide_X_minus1_setsum: - "a /((1::('a::field) fps) - X) = Abs_fps (\n. setsum (\i. a $ i) {0..n})" + "a /((1::('a::field) fps) - X) = Abs_fps (\n. setsum (\i. a $ i) {0..n})" proof - let ?X = "1 - (X::('a::field) fps)" have th0: "?X $ 0 \ 0" by simp @@ -1429,6 +1424,7 @@ finally show ?thesis by (simp add: inverse_mult_eq_1[OF th0]) qed + subsubsection{* Rule 4 in its more general form: generalizes Rule 3 for an arbitrary finite product of FPS, also the relvant instance of powers of a FPS*} @@ -1445,9 +1441,8 @@ shows "listsum xs \ n" and "listsum ys \ n" proof - from h have "listsum (xs @ ys) = n" by (simp add: natpermute_def) - hence *: "listsum xs + listsum ys = n" by simp - from * show "listsum xs \ n" by simp - from * show "listsum ys \ n" by simp + hence "listsum xs + listsum ys = n" by simp + then show "listsum xs \ n" and "listsum ys \ n" by simp_all qed lemma natpermute_split: @@ -1667,23 +1662,17 @@ lemma fps_nth_power_0: fixes m :: nat and a :: "('a::{comm_ring_1}) fps" shows "(a ^m)$0 = (a$0) ^ m" -proof - - { - assume "m = 0" - hence ?thesis by simp - } - moreover - { - fix n - assume m: "m = Suc n" - have c: "m = card {0..n}" using m by simp - have "(a ^m)$0 = setprod (\i. a$0) {0..n}" - by (simp add: m fps_power_nth del: replicate.simps power_Suc) - also have "\ = (a$0) ^ m" - unfolding c by (rule setprod_constant) simp - finally have ?thesis . - } - ultimately show ?thesis by (cases m) auto +proof (cases m) + case 0 + then show ?thesis by simp +next + case (Suc n) + then have c: "m = card {0..n}" by simp + have "(a ^m)$0 = setprod (\i. a$0) {0..n}" + by (simp add: Suc fps_power_nth del: replicate.simps power_Suc) + also have "\ = (a$0) ^ m" + unfolding c by (rule setprod_constant) simp + finally show ?thesis . qed lemma fps_compose_inj_right: @@ -2316,8 +2305,7 @@ done also have "\ = setsum (\i. of_nat (i + 1) * a$(i+1) * (setsum (\j. (b^ i)$j * of_nat (n - j + 1) * b$(n - j + 1)) {0..n})) {0.. n}" unfolding fps_deriv_nth - apply (rule setsum_reindex_cong [where f = Suc]) - by (auto simp add: mult_assoc) + by (rule setsum_reindex_cong [where f = Suc]) (auto simp add: mult_assoc) finally have th0: "(fps_deriv (a oo b))$n = setsum (\i. of_nat (i + 1) * a$(i+1) * (setsum (\j. (b^ i)$j * of_nat (n - j + 1) * b$(n - j + 1)) {0..n})) {0.. n}" . @@ -2626,8 +2614,10 @@ apply (simp add: fps_compose_mult_distrib[OF c0]) done -lemma fps_compose_power: assumes c0: "c$0 = (0::'a::idom)" - shows "(a oo c)^n = a^n oo c" (is "?l = ?r") +lemma fps_compose_power: + assumes c0: "c$0 = (0::'a::idom)" + shows "(a oo c)^n = a^n oo c" + (is "?l = ?r") proof (cases n) case 0 then show ?thesis by simp @@ -2844,14 +2834,16 @@ then have "?r b (?r c a) oo ?r c a oo a = b oo a" by simp then have "?r b (?r c a) oo (?r c a oo a) = b oo a" apply (subst fps_compose_assoc) - using a0 c0 apply (auto simp add: fps_ginv_def) + using a0 c0 + apply (auto simp add: fps_ginv_def) done then have "?r b (?r c a) oo c = b oo a" unfolding fps_ginv[OF a0 a1] . then have "?r b (?r c a) oo c oo fps_inv c= b oo a oo fps_inv c" by simp then have "?r b (?r c a) oo (c oo fps_inv c) = b oo a oo fps_inv c" apply (subst fps_compose_assoc) - using a0 c0 apply (auto simp add: fps_inv_def) + using a0 c0 + apply (auto simp add: fps_inv_def) done then show ?thesis unfolding fps_inv_right[OF c0 c1] by simp qed @@ -2883,13 +2875,16 @@ subsection{* Elementary series *} subsubsection{* Exponential series *} + definition "E x = Abs_fps (\n. x^n / of_nat (fact n))" lemma E_deriv[simp]: "fps_deriv (E a) = fps_const (a::'a::field_char_0) * E a" (is "?l = ?r") proof - - { fix n + { + fix n have "?l$n = ?r $ n" - apply (auto simp add: E_def field_simps power_Suc[symmetric]simp del: fact_Suc of_nat_Suc power_Suc) + apply (auto simp add: E_def field_simps power_Suc[symmetric] + simp del: fact_Suc of_nat_Suc power_Suc) apply (simp add: of_nat_mult field_simps) done } @@ -2960,7 +2955,7 @@ assumes a: "a\0" shows "fps_inv (E a - 1) oo (E a - 1) = X" and "(E a - 1) oo fps_inv (E a - 1) = X" -proof- +proof - let ?b = "E a - 1" have b0: "?b $ 0 = 0" by simp have b1: "?b $ 1 \ 0" by (simp add: a) @@ -2968,7 +2963,6 @@ from fps_inv_right[OF b0 b1] show "(E a - 1) oo fps_inv (E a - 1) = X" . qed - lemma fps_const_inverse: "a \ 0 \ inverse (fps_const (a::'a::field)) = fps_const (inverse a)" apply (auto simp add: fps_eq_iff fps_inverse_def) @@ -3034,6 +3028,7 @@ unfolding of_nat_add[symmetric] of_nat_power[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric] by simp + subsubsection{* Logarithmic series *} lemma Abs_fps_if_0: @@ -3206,15 +3201,17 @@ lemma binomial_Vandermonde: "setsum (\k. (a choose k) * (b choose (n - k))) {0..n} = (a + b) choose n" using gbinomial_Vandermonde[of "(of_nat a)" "of_nat b" n] - apply (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric] of_nat_add[symmetric]) - by simp + apply simp + done lemma binomial_Vandermonde_same: "setsum (\k. (n choose k)\<^sup>2) {0..n} = (2*n) choose n" using binomial_Vandermonde[of n n n,symmetric] - unfolding mult_2 apply (simp add: power2_eq_square) + unfolding mult_2 + apply (simp add: power2_eq_square) apply (rule setsum_cong2) - by (auto intro: binomial_symmetric) + apply (auto intro: binomial_symmetric) + done lemma Vandermonde_pochhammer_lemma: fixes a :: "'a::field_char_0" @@ -3244,17 +3241,19 @@ using kn by (cases "k=0", simp_all add: gbinomial_pochhammer)} moreover - {assume n0: "n \ 0" and k0: "k \ 0" + { assume n0: "n \ 0" and k0: "k \ 0" then obtain m where m: "n = Suc m" by (cases n, auto) from k0 obtain h where h: "k = Suc h" by (cases k, auto) - {assume kn: "k = n" + { assume kn: "k = n" 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)" using kn pochhammer_minus'[where k=k and n=n and b=b] apply (simp add: pochhammer_same) using bn0 - by (simp add: field_simps power_add[symmetric])} + apply (simp add: field_simps power_add[symmetric]) + done + } moreover - {assume nk: "k \ n" + { assume nk: "k \ n" have m1nk: "?m1 n = setprod (%i. - 1) {0..m}" "?m1 k = setprod (%i. - 1) {0..h}" by (simp_all add: setprod_constant m h) @@ -3323,11 +3322,16 @@ using kn' by (simp add: gbinomial_def) 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} 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)" - by (cases "k =n", auto)} + by (cases "k = n") auto + } 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 \ 0 " + apply (cases "n = 0") using nz' - apply (cases "n=0", auto) - by (cases "k", auto)} + apply auto + apply (cases k) + apply auto + done + } note th00 = this have "?r = ((a + b) gchoose n) * (of_nat (fact n)/ (?m1 n * pochhammer (- b) n))" unfolding gbinomial_pochhammer @@ -3345,16 +3349,18 @@ lemma Vandermonde_pochhammer: - fixes a :: "'a::field_char_0" + fixes a :: "'a::field_char_0" assumes c: "ALL i : {0..< n}. c \ - of_nat i" - shows "setsum (%k. (pochhammer a k * pochhammer (- (of_nat n)) k) / (of_nat (fact k) * pochhammer c k)) {0..n} = pochhammer (c - a) n / pochhammer c n" -proof- + shows "setsum (%k. (pochhammer a k * pochhammer (- (of_nat n)) k) / + (of_nat (fact k) * pochhammer c k)) {0..n} = pochhammer (c - a) n / pochhammer c n" +proof - let ?a = "- a" let ?b = "c + of_nat n - 1" have h: "\ j \{0..< n}. ?b \ of_nat j" using c apply (auto simp add: algebra_simps of_nat_diff) apply (erule_tac x= "n - j - 1" in ballE) - by (auto simp add: of_nat_diff algebra_simps) + apply (auto simp add: of_nat_diff algebra_simps) + done have th0: "pochhammer (- (?a + ?b)) n = (- 1)^n * pochhammer (c - a) n" unfolding pochhammer_minus[OF le_refl] by (simp add: algebra_simps) @@ -3367,6 +3373,7 @@ show ?thesis using nz by (simp add: field_simps setsum_right_distrib) qed + subsubsection{* Formal trigonometric functions *} definition "fps_sin (c::'a::field_char_0) = @@ -3379,7 +3386,7 @@ "fps_deriv (fps_sin c) = fps_const c * fps_cos c" (is "?lhs = ?rhs") proof (rule fps_ext) - fix n::nat + fix n :: nat { assume en: "even n" have "?lhs$n = of_nat (n+1) * (fps_sin c $ (n+1))" by simp @@ -3394,7 +3401,7 @@ by (simp add: fps_cos_def field_simps) } then show "?lhs $ n = ?rhs $ n" - by (cases "even n", simp_all add: fps_deriv_def fps_sin_def fps_cos_def) + by (cases "even n") (simp_all add: fps_deriv_def fps_sin_def fps_cos_def) qed lemma fps_cos_deriv: "fps_deriv (fps_cos c) = fps_const (- c)* (fps_sin c)" @@ -3439,30 +3446,30 @@ qed lemma divide_eq_iff: "a \ (0::'a::field) \ x / a = y \ x = y * a" -by auto + by auto lemma eq_divide_iff: "a \ (0::'a::field) \ x = y / a \ x * a = y" -by auto + by auto lemma fps_sin_nth_0 [simp]: "fps_sin c $ 0 = 0" -unfolding fps_sin_def by simp + unfolding fps_sin_def by simp lemma fps_sin_nth_1 [simp]: "fps_sin c $ 1 = c" -unfolding fps_sin_def by simp + unfolding fps_sin_def by simp lemma fps_sin_nth_add_2: "fps_sin c $ (n + 2) = - (c * c * fps_sin c $ n / (of_nat(n+1) * of_nat(n+2)))" -unfolding fps_sin_def -apply (cases n, simp) -apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc) -apply (simp add: of_nat_mult del: of_nat_Suc mult_Suc) -done + unfolding fps_sin_def + apply (cases n, simp) + apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc) + apply (simp add: of_nat_mult del: of_nat_Suc mult_Suc) + done lemma fps_cos_nth_0 [simp]: "fps_cos c $ 0 = 1" -unfolding fps_cos_def by simp + unfolding fps_cos_def by simp lemma fps_cos_nth_1 [simp]: "fps_cos c $ 1 = 0" -unfolding fps_cos_def by simp + unfolding fps_cos_def by simp lemma fps_cos_nth_add_2: "fps_cos c $ (n + 2) = - (c * c * fps_cos c $ n / (of_nat(n+1) * of_nat(n+2)))"