author huffman Tue, 29 May 2007 18:31:30 +0200 changeset 23121 5feeb93b3ba8 parent 23120 a34f204e9c88 child 23122 3d853d6f2f7d
cleaned up some proofs
```--- a/src/HOL/Hyperreal/Series.thy	Tue May 29 18:19:56 2007 +0200
+++ b/src/HOL/Hyperreal/Series.thy	Tue May 29 18:31:30 2007 +0200
@@ -147,22 +147,14 @@
done

-lemma sums_zero: "(%n. 0) sums 0";
-  apply (unfold sums_def);
-  apply simp;
-  apply (rule LIMSEQ_const);
-done;
+lemma sums_zero: "(\<lambda>n. 0) sums 0"
+unfolding sums_def by (simp add: LIMSEQ_const)

-lemma summable_zero: "summable (%n. 0)";
-  apply (rule sums_summable);
-  apply (rule sums_zero);
-done;
+lemma summable_zero: "summable (\<lambda>n. 0)"
+by (rule sums_zero [THEN sums_summable])

-lemma suminf_zero: "suminf (%n. 0) = 0";
-  apply (rule sym);
-  apply (rule sums_unique);
-  apply (rule sums_zero);
-done;
+lemma suminf_zero: "suminf (\<lambda>n. 0) = 0"
+by (rule sums_zero [THEN sums_unique, symmetric])

lemma (in bounded_linear) sums:
"(\<lambda>n. X n) sums a \<Longrightarrow> (\<lambda>n. f (X n)) sums (f a)"
@@ -174,113 +166,81 @@

lemma (in bounded_linear) suminf:
"summable (\<lambda>n. X n) \<Longrightarrow> f (\<Sum>n. X n) = (\<Sum>n. f (X n))"
-by (rule summable_sums [THEN sums, THEN sums_unique])
+by (intro sums_unique sums summable_sums)

lemma sums_mult:
fixes c :: "'a::real_normed_algebra"
shows "f sums a \<Longrightarrow> (\<lambda>n. c * f n) sums (c * a)"
-by (auto simp add: sums_def setsum_right_distrib [symmetric]
-         intro!: LIMSEQ_mult intro: LIMSEQ_const)
+by (rule bounded_linear_mult_right.sums)

lemma summable_mult:
fixes c :: "'a::real_normed_algebra"
-  shows "summable f \<Longrightarrow> summable (%n. c * f n)";
-  apply (unfold summable_def);
-  apply (auto intro: sums_mult);
-done;
+  shows "summable f \<Longrightarrow> summable (%n. c * f n)"
+by (rule bounded_linear_mult_right.summable)

lemma suminf_mult:
fixes c :: "'a::real_normed_algebra"
shows "summable f \<Longrightarrow> suminf (\<lambda>n. c * f n) = c * suminf f";
-  apply (rule sym);
-  apply (rule sums_unique);
-  apply (rule sums_mult);
-  apply (erule summable_sums);
-done;
+by (rule bounded_linear_mult_right.suminf [symmetric])

lemma sums_mult2:
fixes c :: "'a::real_normed_algebra"
shows "f sums a \<Longrightarrow> (\<lambda>n. f n * c) sums (a * c)"
-by (auto simp add: sums_def setsum_left_distrib [symmetric]
-         intro!: LIMSEQ_mult LIMSEQ_const)
+by (rule bounded_linear_mult_left.sums)

lemma summable_mult2:
fixes c :: "'a::real_normed_algebra"
shows "summable f \<Longrightarrow> summable (\<lambda>n. f n * c)"
-  apply (unfold summable_def)
-  apply (auto intro: sums_mult2)
-done
+by (rule bounded_linear_mult_left.summable)

lemma suminf_mult2:
fixes c :: "'a::real_normed_algebra"
shows "summable f \<Longrightarrow> suminf f * c = (\<Sum>n. f n * c)"
-by (auto intro!: sums_unique sums_mult2 summable_sums)
+by (rule bounded_linear_mult_left.suminf)

lemma sums_divide:
fixes c :: "'a::real_normed_field"
shows "f sums a \<Longrightarrow> (\<lambda>n. f n / c) sums (a / c)"
+by (rule bounded_linear_divide.sums)

lemma summable_divide:
fixes c :: "'a::real_normed_field"
shows "summable f \<Longrightarrow> summable (\<lambda>n. f n / c)"
-  apply (unfold summable_def);
-  apply (auto intro: sums_divide);
-done;
+by (rule bounded_linear_divide.summable)

lemma suminf_divide:
fixes c :: "'a::real_normed_field"
shows "summable f \<Longrightarrow> suminf (\<lambda>n. f n / c) = suminf f / c"
-  apply (rule sym);
-  apply (rule sums_unique);
-  apply (rule sums_divide);
-  apply (erule summable_sums);
-done;
+by (rule bounded_linear_divide.suminf [symmetric])

-lemma sums_add: "[| x sums x0; y sums y0 |] ==> (%n. x n + y n) sums (x0+y0)"
+lemma sums_add: "\<lbrakk>X sums a; Y sums b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n + Y n) sums (a + b)"

-lemma summable_add: "summable f ==> summable g ==> summable (%x. f x + g x)";
-  apply (unfold summable_def);
-  apply clarify;
-  apply (rule exI);
-  apply assumption;
-done;
+lemma summable_add: "\<lbrakk>summable X; summable Y\<rbrakk> \<Longrightarrow> summable (\<lambda>n. X n + Y n)"
+unfolding summable_def by (auto intro: sums_add)

-     "[| summable f; summable g |]
-      ==> suminf f + suminf g  = (\<Sum>n. f n + g n)"
-by (auto intro!: sums_add sums_unique summable_sums)
-
-lemma sums_diff: "[| x sums x0; y sums y0 |] ==> (%n. x n - y n) sums (x0-y0)"
-by (auto simp add: sums_def setsum_subtractf intro: LIMSEQ_diff)
+  "\<lbrakk>summable X; summable Y\<rbrakk> \<Longrightarrow> suminf X + suminf Y = (\<Sum>n. X n + Y n)"

-lemma summable_diff: "summable f ==> summable g ==> summable (%x. f x - g x)";
-  apply (unfold summable_def);
-  apply clarify;
-  apply (rule exI);
-  apply (erule sums_diff);
-  apply assumption;
-done;
+lemma sums_diff: "\<lbrakk>X sums a; Y sums b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n - Y n) sums (a - b)"
+unfolding sums_def by (simp add: setsum_subtractf LIMSEQ_diff)
+
+lemma summable_diff: "\<lbrakk>summable X; summable Y\<rbrakk> \<Longrightarrow> summable (\<lambda>n. X n - Y n)"
+unfolding summable_def by (auto intro: sums_diff)

lemma suminf_diff:
-     "[| summable f; summable g |]
-      ==> suminf f - suminf g  = (\<Sum>n. f n - g n)"
-by (auto intro!: sums_diff sums_unique summable_sums)
+  "\<lbrakk>summable X; summable Y\<rbrakk> \<Longrightarrow> suminf X - suminf Y = (\<Sum>n. X n - Y n)"
+by (intro sums_unique sums_diff summable_sums)

-lemma sums_minus: "f sums s ==> (%x. - f x) sums (- s)";
-  by (simp add: sums_def setsum_negf LIMSEQ_minus);
+lemma sums_minus: "X sums a ==> (\<lambda>n. - X n) sums (- a)"
+unfolding sums_def by (simp add: setsum_negf LIMSEQ_minus)

-lemma summable_minus: "summable f ==> summable (%x. - f x)";
-  by (auto simp add: summable_def intro: sums_minus);
+lemma summable_minus: "summable X \<Longrightarrow> summable (\<lambda>n. - X n)"
+unfolding summable_def by (auto intro: sums_minus)

-lemma suminf_minus: "summable f ==> suminf (%x. - f x) = - (suminf f)";
-  apply (rule sym);
-  apply (rule sums_unique);
-  apply (rule sums_minus);
-  apply (erule summable_sums);
-done;
+lemma suminf_minus: "summable X \<Longrightarrow> (\<Sum>n. - X n) = - (\<Sum>n. X n)"
+by (intro sums_unique [symmetric] sums_minus summable_sums)

lemma sums_group:
"[|summable f; 0 < k |] ==> (%n. setsum f {n*k..<n*k+k}) sums (suminf f)"```