# 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..<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)
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) \<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
 
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 \<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)
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 "\<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"
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 \<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*}
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 \<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 *}