# HG changeset patch # User hoelzl # Date 1395156572 -3600 # Node ID 9ffbb4004c81ac7f43c5d83b43ba71afb71a8ca0 # Parent c726ecfb22b660fa387ce2409478d6e0b1b42ab9 fix HOL-NSA; move lemmas diff -r c726ecfb22b6 -r 9ffbb4004c81 src/HOL/NSA/HSeries.thy --- 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.. s" + "f NSsums s = (%n. setsum f {.. 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: "(\n. m \ Suc n --> f n = r) & m \ na @@ -158,24 +162,23 @@ by (simp add: suminf_NSsuminf_iff [symmetric] sums_NSsums_iff sums_unique) lemma NSseries_zero: - "\m. n \ Suc m --> f(m) = 0 ==> f NSsums (setsum f {0..m. n \ Suc m --> f(m) = 0 ==> f NSsums (setsum f {..M \ HNatInfinite. \N \ 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) diff -r c726ecfb22b6 -r 9ffbb4004c81 src/HOL/NSA/HTranscendental.thy --- 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) \ 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="\x. 1 \ 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="\x. 1 \ 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) \ 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) \ 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 diff -r c726ecfb22b6 -r 9ffbb4004c81 src/HOL/Nat.thy --- 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 \ m \ n" by (simp add: less_eq_Suc_le) +lemma Suc_less_eq2: "Suc n < m \ (\m'. m = Suc m' \ n < m')" + by (cases m) auto + lemma le_SucI: "m \ n \ m \ 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) \ l \ (\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 * i < k * j" apply(auto simp: gr0_conv_Suc) diff -r c726ecfb22b6 -r 9ffbb4004c81 src/HOL/Real_Vector_Spaces.thy --- 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 "\norm a \ r; norm b \ s\ \ norm (a + b) \ r + s" by (metis add_mono_thms_linordered_semiring(1) norm_triangle_ineq order.trans) +lemma norm_setsum: + fixes f :: "'a \ 'b::real_normed_vector" + shows "norm (setsum f A) \ (\i\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 "\norm a\ = norm a" diff -r c726ecfb22b6 -r 9ffbb4004c81 src/HOL/Series.thy --- 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 \ (\m'. m = Suc m' \ n < m')" - by (cases m) auto - -(* TODO: MOVE *) -lemma norm_ratiotest_lemma: - fixes x y :: "'a::real_normed_vector" - shows "\c \ 0; norm x \ c * norm y\ \ x = 0" -apply (subgoal_tac "norm x \ 0", simp) -apply (erule order_trans) -apply (simp add: mult_le_0_iff) -done - -(* TODO: MOVE *) -lemma rabs_ratiotest_lemma: "[| c \ 0; abs x \ c * abs y |] ==> x = (0::real)" -by (erule norm_ratiotest_lemma, simp) - -(* TODO: MOVE *) -lemma le_Suc_ex: "(k::nat) \ l ==> (\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]: "(\i<2 * n. (-1) ^ Suc i) = (0::'a::ring_1)" - by (induct "n") auto - -(* MOVE *) -lemma setsum_nat_group: "(\m 'b::real_normed_vector" - shows "norm (setsum f A) \ (\i\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 \ 'b::real_normed_vector" - assumes "finite s" "t \ s" - assumes le: "(\x. x \ s \ norm(f x) \ g x)" - shows "norm (setsum f t) \ setsum g s" -proof - - have "norm (setsum f t) \ (\i\t. norm (f i))" - by (rule norm_setsum) - also have "\ \ (\i\t. g i)" - using assms by (auto intro!: setsum_mono) - also have "\ \ 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 \ 'a::{topological_space, comm_monoid_add}) \ 'a \ bool" (infixr "sums" 80) @@ -455,8 +387,7 @@ text{*Absolute convergence imples normal convergence*} -lemma summable_norm_cancel: - "summable (\n. norm (f n)) \ summable f" +lemma summable_norm_cancel: "summable (\n. norm (f n)) \ 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: "\\N. \n\N. norm (f n) \ g n; summable g\ \ summable f" +lemma summable_comparison_test: "\N. \n\N. norm (f n) \ g n \ summable g \ 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: - "\\N. \n\N. norm (f n) \ g n; summable g\ \ summable (\n. norm (f n))" +lemma summable_norm_comparison_test: "\N. \n\N. norm (f n) \ g n \ summable g \ summable (\n. norm (f n))" by (rule summable_comparison_test) auto -lemma summable_rabs_cancel: - fixes f :: "nat \ real" - shows "summable (\n. \f n\) \ summable f" +lemma summable_rabs_cancel: "summable (\n. \f n :: real\) \ summable f" by (rule summable_norm_cancel) simp text{*Summability of geometric series for real algebras*} diff -r c726ecfb22b6 -r 9ffbb4004c81 src/HOL/Set_Interval.thy --- 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 \ n \ {i..m