--- a/src/HOL/NSA/HSeries.thy Tue Mar 18 15:53:48 2014 +0100
+++ b/src/HOL/NSA/HSeries.thy Tue Mar 18 16:29:32 2014 +0100
@@ -18,7 +18,7 @@
definition
NSsums :: "[nat=>real,real] => bool" (infixr "NSsums" 80) where
- "f NSsums s = (%n. setsum f {0..<n}) ----NS> s"
+ "f NSsums s = (%n. setsum f {..<n}) ----NS> s"
definition
NSsummable :: "(nat=>real) => bool" where
@@ -114,7 +114,11 @@
lemma sumhr_minus_one_realpow_zero [simp]:
"!!N. sumhr(0, N + N, %i. (-1) ^ (i+1)) = 0"
unfolding sumhr_app
-by transfer (simp del: power_Suc add: mult_2 [symmetric])
+apply transfer
+apply (simp del: power_Suc add: mult_2 [symmetric])
+apply (induct_tac N)
+apply simp_all
+done
lemma sumhr_interval_const:
"(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na
@@ -158,24 +162,23 @@
by (simp add: suminf_NSsuminf_iff [symmetric] sums_NSsums_iff sums_unique)
lemma NSseries_zero:
- "\<forall>m. n \<le> Suc m --> f(m) = 0 ==> f NSsums (setsum f {0..<n})"
-by (simp add: sums_NSsums_iff [symmetric] series_zero)
+ "\<forall>m. n \<le> Suc m --> f(m) = 0 ==> f NSsums (setsum f {..<n})"
+by (auto simp add: sums_NSsums_iff [symmetric] not_le[symmetric] intro!: sums_finite)
lemma NSsummable_NSCauchy:
"NSsummable f =
(\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. abs (sumhr(M,N,f)) @= 0)"
-apply (auto simp add: summable_NSsummable_iff [symmetric]
- summable_convergent_sumr_iff convergent_NSconvergent_iff
+apply (auto simp add: summable_NSsummable_iff [symmetric]
+ summable_iff_convergent convergent_NSconvergent_iff atLeast0LessThan[symmetric]
NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_sumr)
apply (cut_tac x = M and y = N in linorder_less_linear)
-apply (auto simp add: approx_refl)
+apply auto
apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
apply (rule_tac [2] approx_minus_iff [THEN iffD2])
apply (auto dest: approx_hrabs_zero_cancel
- simp add: sumhr_split_diff)
+ simp add: sumhr_split_diff atLeast0LessThan[symmetric])
done
-
text{*Terms of a convergent series tend to zero*}
lemma NSsummable_NSLIMSEQ_zero: "NSsummable f ==> f ----NS> 0"
apply (auto simp add: NSLIMSEQ_def NSsummable_NSCauchy)
--- a/src/HOL/NSA/HTranscendental.thy Tue Mar 18 15:53:48 2014 +0100
+++ b/src/HOL/NSA/HTranscendental.thy Tue Mar 18 16:29:32 2014 +0100
@@ -215,22 +215,21 @@
lemma HFinite_exp [simp]:
"sumhr (0, whn, %n. inverse (real (fact n)) * x ^ n) \<in> HFinite"
unfolding sumhr_app
-apply (simp only: star_zero_def starfun2_star_of)
+apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
apply (rule NSBseqD2)
apply (rule NSconvergent_NSBseq)
apply (rule convergent_NSconvergent_iff [THEN iffD1])
-apply (rule summable_convergent_sumr_iff [THEN iffD1])
+apply (rule summable_iff_convergent [THEN iffD1])
apply (rule summable_exp)
done
lemma exphr_zero [simp]: "exphr 0 = 1"
-apply (simp add: exphr_def sumhr_split_add
- [OF hypnat_one_less_hypnat_omega, symmetric])
+apply (simp add: exphr_def sumhr_split_add [OF hypnat_one_less_hypnat_omega, symmetric])
apply (rule st_unique, simp)
apply (rule subst [where P="\<lambda>x. 1 \<approx> x", OF _ approx_refl])
apply (rule rev_mp [OF hypnat_one_less_hypnat_omega])
apply (rule_tac x="whn" in spec)
-apply (unfold sumhr_app, transfer, simp)
+apply (unfold sumhr_app, transfer, simp add: power_0_left)
done
lemma coshr_zero [simp]: "coshr 0 = 1"
@@ -240,7 +239,7 @@
apply (rule subst [where P="\<lambda>x. 1 \<approx> x", OF _ approx_refl])
apply (rule rev_mp [OF hypnat_one_less_hypnat_omega])
apply (rule_tac x="whn" in spec)
-apply (unfold sumhr_app, transfer, simp add: cos_coeff_def)
+apply (unfold sumhr_app, transfer, simp add: cos_coeff_def power_0_left)
done
lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) (0::hypreal) @= 1"
@@ -271,6 +270,7 @@
apply (simp add: exphr_def)
apply (rule st_unique, simp)
apply (subst starfunNat_sumr [symmetric])
+unfolding atLeast0LessThan
apply (rule NSLIMSEQ_D [THEN approx_sym])
apply (rule LIMSEQ_NSLIMSEQ)
apply (subst sums_def [symmetric])
@@ -406,11 +406,11 @@
lemma HFinite_sin [simp]: "sumhr (0, whn, %n. sin_coeff n * x ^ n) \<in> HFinite"
unfolding sumhr_app
-apply (simp only: star_zero_def starfun2_star_of)
+apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
apply (rule NSBseqD2)
apply (rule NSconvergent_NSBseq)
apply (rule convergent_NSconvergent_iff [THEN iffD1])
-apply (rule summable_convergent_sumr_iff [THEN iffD1])
+apply (rule summable_iff_convergent [THEN iffD1])
apply (rule summable_sin)
done
@@ -429,11 +429,11 @@
lemma HFinite_cos [simp]: "sumhr (0, whn, %n. cos_coeff n * x ^ n) \<in> HFinite"
unfolding sumhr_app
-apply (simp only: star_zero_def starfun2_star_of)
+apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
apply (rule NSBseqD2)
apply (rule NSconvergent_NSBseq)
apply (rule convergent_NSconvergent_iff [THEN iffD1])
-apply (rule summable_convergent_sumr_iff [THEN iffD1])
+apply (rule summable_iff_convergent [THEN iffD1])
apply (rule summable_cos)
done
--- a/src/HOL/Nat.thy Tue Mar 18 15:53:48 2014 +0100
+++ b/src/HOL/Nat.thy Tue Mar 18 16:29:32 2014 +0100
@@ -445,6 +445,9 @@
lemma less_Suc_eq_le [code]: "m < Suc n \<longleftrightarrow> m \<le> n"
by (simp add: less_eq_Suc_le)
+lemma Suc_less_eq2: "Suc n < m \<longleftrightarrow> (\<exists>m'. m = Suc m' \<and> n < m')"
+ by (cases m) auto
+
lemma le_SucI: "m \<le> n \<Longrightarrow> m \<le> Suc n"
by (induct m arbitrary: n)
(simp_all add: less_eq_nat.simps(2) split: nat.splits)
@@ -746,6 +749,9 @@
intro!: Nat.add_0_right [symmetric] add_Suc_right [symmetric])
done
+lemma le_Suc_ex: "(k::nat) \<le> l \<Longrightarrow> (\<exists>n. l = k + n)"
+ by (auto simp: less_Suc_eq_le[symmetric] dest: less_imp_Suc_add)
+
text {* strict, in 1st argument; proof is by induction on @{text "k > 0"} *}
lemma mult_less_mono2: "(i::nat) < j ==> 0<k ==> k * i < k * j"
apply(auto simp: gr0_conv_Suc)
--- a/src/HOL/Real_Vector_Spaces.thy Tue Mar 18 15:53:48 2014 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Tue Mar 18 16:29:32 2014 +0100
@@ -747,6 +747,11 @@
shows "\<lbrakk>norm a \<le> r; norm b \<le> s\<rbrakk> \<Longrightarrow> norm (a + b) \<le> r + s"
by (metis add_mono_thms_linordered_semiring(1) norm_triangle_ineq order.trans)
+lemma norm_setsum:
+ fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+ shows "norm (setsum f A) \<le> (\<Sum>i\<in>A. norm (f i))"
+ by (induct A rule: infinite_finite_induct) (auto intro: norm_triangle_mono)
+
lemma abs_norm_cancel [simp]:
fixes a :: "'a::real_normed_vector"
shows "\<bar>norm a\<bar> = norm a"
--- a/src/HOL/Series.thy Tue Mar 18 15:53:48 2014 +0100
+++ b/src/HOL/Series.thy Tue Mar 18 16:29:32 2014 +0100
@@ -13,74 +13,6 @@
imports Limits
begin
-(* TODO: MOVE *)
-lemma Suc_less_iff: "Suc n < m \<longleftrightarrow> (\<exists>m'. m = Suc m' \<and> n < m')"
- by (cases m) auto
-
-(* TODO: MOVE *)
-lemma norm_ratiotest_lemma:
- fixes x y :: "'a::real_normed_vector"
- shows "\<lbrakk>c \<le> 0; norm x \<le> c * norm y\<rbrakk> \<Longrightarrow> x = 0"
-apply (subgoal_tac "norm x \<le> 0", simp)
-apply (erule order_trans)
-apply (simp add: mult_le_0_iff)
-done
-
-(* TODO: MOVE *)
-lemma rabs_ratiotest_lemma: "[| c \<le> 0; abs x \<le> c * abs y |] ==> x = (0::real)"
-by (erule norm_ratiotest_lemma, simp)
-
-(* TODO: MOVE *)
-lemma le_Suc_ex: "(k::nat) \<le> l ==> (\<exists>n. l = k + n)"
-apply (drule le_imp_less_or_eq)
-apply (auto dest: less_imp_Suc_add)
-done
-
-(* MOVE *)
-lemma setsum_even_minus_one [simp]: "(\<Sum>i<2 * n. (-1) ^ Suc i) = (0::'a::ring_1)"
- by (induct "n") auto
-
-(* MOVE *)
-lemma setsum_nat_group: "(\<Sum>m<n::nat. setsum f {m * k ..< m*k + k}) = setsum f {..< n * k}"
- apply (subgoal_tac "k = 0 | 0 < k", auto)
- apply (induct "n")
- apply (simp_all add: setsum_add_nat_ivl add_commute atLeast0LessThan[symmetric])
- done
-
-(* MOVE *)
-lemma norm_setsum:
- fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
- shows "norm (setsum f A) \<le> (\<Sum>i\<in>A. norm (f i))"
- apply (case_tac "finite A")
- apply (erule finite_induct)
- apply simp
- apply simp
- apply (erule order_trans [OF norm_triangle_ineq add_left_mono])
- apply simp
- done
-
-(* MOVE *)
-lemma norm_bound_subset:
- fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
- assumes "finite s" "t \<subseteq> s"
- assumes le: "(\<And>x. x \<in> s \<Longrightarrow> norm(f x) \<le> g x)"
- shows "norm (setsum f t) \<le> setsum g s"
-proof -
- have "norm (setsum f t) \<le> (\<Sum>i\<in>t. norm (f i))"
- by (rule norm_setsum)
- also have "\<dots> \<le> (\<Sum>i\<in>t. g i)"
- using assms by (auto intro!: setsum_mono)
- also have "\<dots> \<le> setsum g s"
- using assms order.trans[OF norm_ge_zero le]
- by (auto intro!: setsum_mono3)
- finally show ?thesis .
-qed
-
-(* MOVE *)
-lemma (in linorder) lessThan_minus_lessThan [simp]:
- "{..< n} - {..< m} = {m ..< n}"
- by auto
-
definition
sums :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> 'a \<Rightarrow> bool"
(infixr "sums" 80)
@@ -455,8 +387,7 @@
text{*Absolute convergence imples normal convergence*}
-lemma summable_norm_cancel:
- "summable (\<lambda>n. norm (f n)) \<Longrightarrow> summable f"
+lemma summable_norm_cancel: "summable (\<lambda>n. norm (f n)) \<Longrightarrow> summable f"
apply (simp only: summable_Cauchy, safe)
apply (drule_tac x="e" in spec, safe)
apply (rule_tac x="N" in exI, safe)
@@ -471,7 +402,7 @@
text {* Comparison tests *}
-lemma summable_comparison_test: "\<lbrakk>\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n; summable g\<rbrakk> \<Longrightarrow> summable f"
+lemma summable_comparison_test: "\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n \<Longrightarrow> summable g \<Longrightarrow> summable f"
apply (simp add: summable_Cauchy, safe)
apply (drule_tac x="e" in spec, safe)
apply (rule_tac x = "N + Na" in exI, safe)
@@ -516,18 +447,15 @@
finally have "f (Suc n) = 0"
by auto }
then show "summable f"
- by (intro sums_summable[OF sums_finite, of "{.. Suc N}"]) (auto simp: not_le Suc_less_iff)
+ by (intro sums_summable[OF sums_finite, of "{.. Suc N}"]) (auto simp: not_le Suc_less_eq2)
qed
end
-lemma summable_norm_comparison_test:
- "\<lbrakk>\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n; summable g\<rbrakk> \<Longrightarrow> summable (\<lambda>n. norm (f n))"
+lemma summable_norm_comparison_test: "\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n \<Longrightarrow> summable g \<Longrightarrow> summable (\<lambda>n. norm (f n))"
by (rule summable_comparison_test) auto
-lemma summable_rabs_cancel:
- fixes f :: "nat \<Rightarrow> real"
- shows "summable (\<lambda>n. \<bar>f n\<bar>) \<Longrightarrow> summable f"
+lemma summable_rabs_cancel: "summable (\<lambda>n. \<bar>f n :: real\<bar>) \<Longrightarrow> summable f"
by (rule summable_norm_cancel) simp
text{*Summability of geometric series for real algebras*}
--- a/src/HOL/Set_Interval.thy Tue Mar 18 15:53:48 2014 +0100
+++ b/src/HOL/Set_Interval.thy Tue Mar 18 16:29:32 2014 +0100
@@ -1193,6 +1193,10 @@
"i \<le> n \<Longrightarrow> {i..<m} - {i..<n} = {n..<(m::'a::linorder)}"
by(auto)
+lemma (in linorder) lessThan_minus_lessThan [simp]:
+ "{..< n} - {..< m} = {m ..< n}"
+ by auto
+
subsubsection {* Some Subset Conditions *}
@@ -1409,6 +1413,11 @@
finally show ?thesis by auto
qed
+lemma setsum_nat_group: "(\<Sum>m<n::nat. setsum f {m * k ..< m*k + k}) = setsum f {..< n * k}"
+ apply (subgoal_tac "k = 0 | 0 < k", auto)
+ apply (induct "n")
+ apply (simp_all add: setsum_add_nat_ivl add_commute atLeast0LessThan[symmetric])
+ done
subsection{* Shifting bounds *}