# HG changeset patch # User nipkow # Date 1109150602 -3600 # Node ID 5188ce7316b7f65423016abfacaef2892fc06ce7 # Parent 0efa7126003ffa6075a08effc864007cc2caaebe suminf -> \ diff -r 0efa7126003f -r 5188ce7316b7 src/HOL/Hyperreal/Series.thy --- a/src/HOL/Hyperreal/Series.thy Tue Feb 22 18:42:22 2005 +0100 +++ b/src/HOL/Hyperreal/Series.thy Wed Feb 23 10:23:22 2005 +0100 @@ -26,6 +26,11 @@ suminf :: "(nat=>real) => real" "suminf f == SOME s. f sums s" +syntax + "_suminf" :: "idt => real => real" ("\_. _" [0, 10] 10) +translations + "\i. b" == "suminf (%i. b)" + lemma setsum_Suc[simp]: "setsum f {m.. (%n. x n - y n) sums (x0-y0)" by (auto simp add: sums_def setsum_subtractf intro: LIMSEQ_diff) -lemma suminf_mult: "summable f ==> suminf f * c = suminf(%n. f n * c)" +lemma suminf_mult: "summable f ==> suminf f * c = (\n. f n * c)" by (auto intro!: sums_unique sums_mult summable_sums simp add: mult_commute) -lemma suminf_mult2: "summable f ==> c * suminf f = suminf(%n. c * f n)" +lemma suminf_mult2: "summable f ==> c * suminf f = (\n. c * f n)" by (auto intro!: sums_unique sums_mult summable_sums) lemma suminf_diff: "[| summable f; summable g |] - ==> suminf f - suminf g = suminf(%n. f n - g n)" + ==> suminf f - suminf g = (\n. f n - g n)" by (auto intro!: sums_diff sums_unique summable_sums) lemma sums_minus: "x sums x0 ==> (%n. - x n) sums - x0" @@ -285,7 +290,7 @@ text{*Absolute convergence of series*} lemma summable_rabs: - "summable (%n. abs (f n)) ==> abs(suminf f) \ suminf (%n. abs(f n))" + "summable (%n. abs (f n)) ==> abs(suminf f) \ (\n. abs(f n))" by (auto intro: LIMSEQ_le LIMSEQ_imp_rabs summable_rabs_cancel summable_sumr_LIMSEQ_suminf) diff -r 0efa7126003f -r 5188ce7316b7 src/HOL/Hyperreal/Transcendental.thy --- a/src/HOL/Hyperreal/Transcendental.thy Tue Feb 22 18:42:22 2005 +0100 +++ b/src/HOL/Hyperreal/Transcendental.thy Wed Feb 23 10:23:22 2005 +0100 @@ -19,18 +19,18 @@ "sqrt x == root 2 x" exp :: "real => real" - "exp x == suminf(%n. inverse(real (fact n)) * (x ^ n))" + "exp x == \n. inverse(real (fact n)) * (x ^ n)" sin :: "real => real" - "sin x == suminf(%n. (if even(n) then 0 else - ((- 1) ^ ((n - Suc 0) div 2))/(real (fact n))) * x ^ n)" + "sin x == \n. (if even(n) then 0 else + ((- 1) ^ ((n - Suc 0) div 2))/(real (fact n))) * x ^ n" diffs :: "(nat => real) => nat => real" "diffs c == (%n. real (Suc n) * c(Suc n))" cos :: "real => real" - "cos x == suminf(%n. (if even(n) then ((- 1) ^ (n div 2))/(real (fact n)) - else 0) * x ^ n)" + "cos x == \n. (if even(n) then ((- 1) ^ (n div 2))/(real (fact n)) + else 0) * x ^ n" ln :: "real => real" "ln x == (@u. exp u = x)" @@ -452,7 +452,7 @@ lemma diffs_equiv: "summable (%n. (diffs c)(n) * (x ^ n)) ==> (%n. real n * c(n) * (x ^ (n - Suc 0))) sums - (suminf(%n. (diffs c)(n) * (x ^ n)))" + (\n. (diffs c)(n) * (x ^ n))" apply (subgoal_tac " (%n. real n * c (n) * (x ^ (n - Suc 0))) ----> 0") apply (rule_tac [2] LIMSEQ_imp_Suc) apply (drule summable_sums) @@ -571,7 +571,7 @@ apply (subgoal_tac "summable (%n. abs (g (h::real) (n::nat))) ") apply (rule_tac [2] g = "%n. f n * \h\" in summable_comparison_test) apply (rule_tac [2] x = 0 in exI, auto) -apply (rule_tac j = "suminf (%n. \g h n\)" in real_le_trans) +apply (rule_tac j = "\n. \g h n\" in real_le_trans) apply (auto intro: summable_rabs summable_le simp add: sums_summable [THEN suminf_mult]) done @@ -581,10 +581,9 @@ lemma termdiffs_aux: "[|summable (\n. diffs (diffs c) n * K ^ n); \x\ < \K\ |] - ==> (\h. suminf - (\n. c n * + ==> (\h. \n. c n * (((x + h) ^ n - x ^ n) * inverse h - - real n * x ^ (n - Suc 0)))) + real n * x ^ (n - Suc 0))) -- 0 --> 0" apply (drule dense, safe) apply (frule real_less_sum_gt_zero) @@ -648,16 +647,16 @@ summable(%n. (diffs c)(n) * (K ^ n)); summable(%n. (diffs(diffs c))(n) * (K ^ n)); \x\ < \K\ |] - ==> DERIV (%x. suminf (%n. c(n) * (x ^ n))) x :> - suminf (%n. (diffs c)(n) * (x ^ n))" + ==> DERIV (%x. \n. c(n) * (x ^ n)) x :> + (\n. (diffs c)(n) * (x ^ n))" apply (simp add: deriv_def) -apply (rule_tac g = "%h. suminf (%n. ((c (n) * ( (x + h) ^ n)) - (c (n) * (x ^ n))) * inverse h)" in LIM_trans) +apply (rule_tac g = "%h. \n. ((c (n) * ( (x + h) ^ n)) - (c (n) * (x ^ n))) * inverse h" in LIM_trans) apply (simp add: LIM_def, safe) apply (rule_tac x = "\K\ - \x\" in exI) apply (auto simp add: less_diff_eq) apply (drule abs_triangle_ineq [THEN order_le_less_trans]) apply (rule_tac y = 0 in order_le_less_trans, auto) -apply (subgoal_tac " (%n. (c n) * (x ^ n)) sums (suminf (%n. (c n) * (x ^ n))) & (%n. (c n) * ((x + xa) ^ n)) sums (suminf (%n. (c n) * ( (x + xa) ^ n))) ") +apply (subgoal_tac " (%n. (c n) * (x ^ n)) sums (\n. (c n) * (x ^ n)) & (%n. (c n) * ((x + xa) ^ n)) sums (\n. (c n) * ( (x + xa) ^ n))") apply (auto intro!: summable_sums) apply (rule_tac [2] powser_inside, rule_tac [4] powser_inside) apply (auto simp add: add_commute) @@ -666,7 +665,7 @@ apply (rule sums_unique) apply (simp add: diff_def divide_inverse add_ac mult_ac) apply (rule LIM_zero_cancel) -apply (rule_tac g = "%h. suminf (%n. c (n) * ((( ((x + h) ^ n) - (x ^ n)) * inverse h) - (real n * (x ^ (n - Suc 0)))))" in LIM_trans) +apply (rule_tac g = "%h. \n. c (n) * ((( ((x + h) ^ n) - (x ^ n)) * inverse h) - (real n * (x ^ (n - Suc 0))))" in LIM_trans) prefer 2 apply (blast intro: termdiffs_aux) apply (simp add: LIM_def, safe) apply (rule_tac x = "\K\ - \x\" in exI) @@ -677,7 +676,7 @@ apply (rule_tac [2] powser_inside, auto) apply (drule_tac c = c and x = x in diffs_equiv) apply (frule sums_unique, auto) -apply (subgoal_tac " (%n. (c n) * (x ^ n)) sums (suminf (%n. (c n) * (x ^ n))) & (%n. (c n) * ((x + xa) ^ n)) sums (suminf (%n. (c n) * ( (x + xa) ^ n))) ") +apply (subgoal_tac " (%n. (c n) * (x ^ n)) sums (\n. (c n) * (x ^ n)) & (%n. (c n) * ((x + xa) ^ n)) sums (\n. (c n) * ( (x + xa) ^ n))") apply safe apply (auto intro!: summable_sums) apply (rule_tac [2] powser_inside, rule_tac [4] powser_inside) @@ -742,33 +741,32 @@ text{*Now at last we can get the derivatives of exp, sin and cos*} lemma lemma_sin_minus: - "- sin x = - suminf(%n. - ((if even n then 0 + "- sin x = (\n. - ((if even n then 0 else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) * x ^ n))" by (auto intro!: sums_unique sums_minus sin_converges) -lemma lemma_exp_ext: "exp = (%x. suminf (%n. inverse (real (fact n)) * x ^ n))" +lemma lemma_exp_ext: "exp = (%x. \n. inverse (real (fact n)) * x ^ n)" by (auto intro!: ext simp add: exp_def) lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)" apply (simp add: exp_def) apply (subst lemma_exp_ext) -apply (subgoal_tac "DERIV (%u. suminf (%n. inverse (real (fact n)) * u ^ n)) x :> suminf (%n. diffs (%n. inverse (real (fact n))) n * x ^ n) ") +apply (subgoal_tac "DERIV (%u. \n. inverse (real (fact n)) * u ^ n) x :> (\n. diffs (%n. inverse (real (fact n))) n * x ^ n)") apply (rule_tac [2] K = "1 + \x\" in termdiffs) apply (auto intro: exp_converges [THEN sums_summable] simp add: exp_fdiffs, arith) done lemma lemma_sin_ext: - "sin = (%x. suminf(%n. + "sin = (%x. \n. (if even n then 0 else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) * - x ^ n))" + x ^ n)" by (auto intro!: ext simp add: sin_def) lemma lemma_cos_ext: - "cos = (%x. suminf(%n. + "cos = (%x. \n. (if even n then (- 1) ^ (n div 2)/(real (fact n)) else 0) * - x ^ n))" + x ^ n)" by (auto intro!: ext simp add: cos_def) lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)" @@ -792,7 +790,7 @@ lemma exp_zero [simp]: "exp 0 = 1" proof - have "(\n = 0..<1. inverse (real (fact n)) * 0 ^ n) = - suminf (\n. inverse (real (fact n)) * 0 ^ n)" + (\n. inverse (real (fact n)) * 0 ^ n)" by (rule series_zero [rule_format, THEN sums_unique], case_tac "m", auto) thus ?thesis by (simp add: exp_def) @@ -1325,7 +1323,7 @@ else (- 1) ^ ((k - Suc 0) div 2) / real (fact k)) * x ^ k) sums - suminf (\n. (if even n then 0 + (\n. (if even n then 0 else (- 1) ^ ((n - Suc 0) div 2) / real (fact n)) * x ^ n)" by (rule sin_converges [THEN sums_summable, THEN sums_group], simp) @@ -1336,7 +1334,7 @@ apply (subgoal_tac "(\n. \k = n * 2..n. (- 1) ^ n / real (fact (2 * n + 1)) * x ^ (2 * n + 1))") + sums (\n. (- 1) ^ n / real (fact (2 * n + 1)) * x ^ (2 * n + 1))") prefer 2 apply (rule sin_paired [THEN sums_summable, THEN sums_group], simp) apply (rotate_tac 2) @@ -1394,8 +1392,7 @@ (if even k then (- 1) ^ (k div 2) / real (fact k) else 0) * x ^ k) sums - suminf - (\n. (if even n then (- 1) ^ (n div 2) / real (fact n) else 0) * + (\n. (if even n then (- 1) ^ (n div 2) / real (fact n) else 0) * x ^ n)" by (rule cos_converges [THEN sums_summable, THEN sums_group], simp) thus ?thesis by (simp add: mult_ac cos_def)