fix HOL-NSA; move lemmas
authorhoelzl
Tue Mar 18 16:29:32 2014 +0100 (2014-03-18)
changeset 561949ffbb4004c81
parent 56193 c726ecfb22b6
child 56195 c7dfd924a165
fix HOL-NSA; move lemmas
src/HOL/NSA/HSeries.thy
src/HOL/NSA/HTranscendental.thy
src/HOL/Nat.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Series.thy
src/HOL/Set_Interval.thy
     1.1 --- a/src/HOL/NSA/HSeries.thy	Tue Mar 18 15:53:48 2014 +0100
     1.2 +++ b/src/HOL/NSA/HSeries.thy	Tue Mar 18 16:29:32 2014 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4  
     1.5  definition
     1.6    NSsums  :: "[nat=>real,real] => bool"     (infixr "NSsums" 80) where
     1.7 -  "f NSsums s = (%n. setsum f {0..<n}) ----NS> s"
     1.8 +  "f NSsums s = (%n. setsum f {..<n}) ----NS> s"
     1.9  
    1.10  definition
    1.11    NSsummable :: "(nat=>real) => bool" where
    1.12 @@ -114,7 +114,11 @@
    1.13  lemma sumhr_minus_one_realpow_zero [simp]: 
    1.14       "!!N. sumhr(0, N + N, %i. (-1) ^ (i+1)) = 0"
    1.15  unfolding sumhr_app
    1.16 -by transfer (simp del: power_Suc add: mult_2 [symmetric])
    1.17 +apply transfer 
    1.18 +apply (simp del: power_Suc add: mult_2 [symmetric])
    1.19 +apply (induct_tac N)
    1.20 +apply simp_all
    1.21 +done
    1.22  
    1.23  lemma sumhr_interval_const:
    1.24       "(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na  
    1.25 @@ -158,24 +162,23 @@
    1.26  by (simp add: suminf_NSsuminf_iff [symmetric] sums_NSsums_iff sums_unique)
    1.27  
    1.28  lemma NSseries_zero:
    1.29 -  "\<forall>m. n \<le> Suc m --> f(m) = 0 ==> f NSsums (setsum f {0..<n})"
    1.30 -by (simp add: sums_NSsums_iff [symmetric] series_zero)
    1.31 +  "\<forall>m. n \<le> Suc m --> f(m) = 0 ==> f NSsums (setsum f {..<n})"
    1.32 +by (auto simp add: sums_NSsums_iff [symmetric] not_le[symmetric] intro!: sums_finite)
    1.33  
    1.34  lemma NSsummable_NSCauchy:
    1.35       "NSsummable f =  
    1.36        (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. abs (sumhr(M,N,f)) @= 0)"
    1.37 -apply (auto simp add: summable_NSsummable_iff [symmetric] 
    1.38 -       summable_convergent_sumr_iff convergent_NSconvergent_iff 
    1.39 +apply (auto simp add: summable_NSsummable_iff [symmetric]
    1.40 +       summable_iff_convergent convergent_NSconvergent_iff atLeast0LessThan[symmetric]
    1.41         NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_sumr)
    1.42  apply (cut_tac x = M and y = N in linorder_less_linear)
    1.43 -apply (auto simp add: approx_refl)
    1.44 +apply auto
    1.45  apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
    1.46  apply (rule_tac [2] approx_minus_iff [THEN iffD2])
    1.47  apply (auto dest: approx_hrabs_zero_cancel 
    1.48 -            simp add: sumhr_split_diff)
    1.49 +            simp add: sumhr_split_diff atLeast0LessThan[symmetric])
    1.50  done
    1.51  
    1.52 -
    1.53  text{*Terms of a convergent series tend to zero*}
    1.54  lemma NSsummable_NSLIMSEQ_zero: "NSsummable f ==> f ----NS> 0"
    1.55  apply (auto simp add: NSLIMSEQ_def NSsummable_NSCauchy)
     2.1 --- a/src/HOL/NSA/HTranscendental.thy	Tue Mar 18 15:53:48 2014 +0100
     2.2 +++ b/src/HOL/NSA/HTranscendental.thy	Tue Mar 18 16:29:32 2014 +0100
     2.3 @@ -215,22 +215,21 @@
     2.4  lemma HFinite_exp [simp]:
     2.5       "sumhr (0, whn, %n. inverse (real (fact n)) * x ^ n) \<in> HFinite"
     2.6  unfolding sumhr_app
     2.7 -apply (simp only: star_zero_def starfun2_star_of)
     2.8 +apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
     2.9  apply (rule NSBseqD2)
    2.10  apply (rule NSconvergent_NSBseq)
    2.11  apply (rule convergent_NSconvergent_iff [THEN iffD1])
    2.12 -apply (rule summable_convergent_sumr_iff [THEN iffD1])
    2.13 +apply (rule summable_iff_convergent [THEN iffD1])
    2.14  apply (rule summable_exp)
    2.15  done
    2.16  
    2.17  lemma exphr_zero [simp]: "exphr 0 = 1"
    2.18 -apply (simp add: exphr_def sumhr_split_add
    2.19 -                   [OF hypnat_one_less_hypnat_omega, symmetric])
    2.20 +apply (simp add: exphr_def sumhr_split_add [OF hypnat_one_less_hypnat_omega, symmetric])
    2.21  apply (rule st_unique, simp)
    2.22  apply (rule subst [where P="\<lambda>x. 1 \<approx> x", OF _ approx_refl])
    2.23  apply (rule rev_mp [OF hypnat_one_less_hypnat_omega])
    2.24  apply (rule_tac x="whn" in spec)
    2.25 -apply (unfold sumhr_app, transfer, simp)
    2.26 +apply (unfold sumhr_app, transfer, simp add: power_0_left)
    2.27  done
    2.28  
    2.29  lemma coshr_zero [simp]: "coshr 0 = 1"
    2.30 @@ -240,7 +239,7 @@
    2.31  apply (rule subst [where P="\<lambda>x. 1 \<approx> x", OF _ approx_refl])
    2.32  apply (rule rev_mp [OF hypnat_one_less_hypnat_omega])
    2.33  apply (rule_tac x="whn" in spec)
    2.34 -apply (unfold sumhr_app, transfer, simp add: cos_coeff_def)
    2.35 +apply (unfold sumhr_app, transfer, simp add: cos_coeff_def power_0_left)
    2.36  done
    2.37  
    2.38  lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) (0::hypreal) @= 1"
    2.39 @@ -271,6 +270,7 @@
    2.40  apply (simp add: exphr_def)
    2.41  apply (rule st_unique, simp)
    2.42  apply (subst starfunNat_sumr [symmetric])
    2.43 +unfolding atLeast0LessThan
    2.44  apply (rule NSLIMSEQ_D [THEN approx_sym])
    2.45  apply (rule LIMSEQ_NSLIMSEQ)
    2.46  apply (subst sums_def [symmetric])
    2.47 @@ -406,11 +406,11 @@
    2.48  
    2.49  lemma HFinite_sin [simp]: "sumhr (0, whn, %n. sin_coeff n * x ^ n) \<in> HFinite"
    2.50  unfolding sumhr_app
    2.51 -apply (simp only: star_zero_def starfun2_star_of)
    2.52 +apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
    2.53  apply (rule NSBseqD2)
    2.54  apply (rule NSconvergent_NSBseq)
    2.55  apply (rule convergent_NSconvergent_iff [THEN iffD1])
    2.56 -apply (rule summable_convergent_sumr_iff [THEN iffD1])
    2.57 +apply (rule summable_iff_convergent [THEN iffD1])
    2.58  apply (rule summable_sin)
    2.59  done
    2.60  
    2.61 @@ -429,11 +429,11 @@
    2.62  
    2.63  lemma HFinite_cos [simp]: "sumhr (0, whn, %n. cos_coeff n * x ^ n) \<in> HFinite"
    2.64  unfolding sumhr_app
    2.65 -apply (simp only: star_zero_def starfun2_star_of)
    2.66 +apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
    2.67  apply (rule NSBseqD2)
    2.68  apply (rule NSconvergent_NSBseq)
    2.69  apply (rule convergent_NSconvergent_iff [THEN iffD1])
    2.70 -apply (rule summable_convergent_sumr_iff [THEN iffD1])
    2.71 +apply (rule summable_iff_convergent [THEN iffD1])
    2.72  apply (rule summable_cos)
    2.73  done
    2.74  
     3.1 --- a/src/HOL/Nat.thy	Tue Mar 18 15:53:48 2014 +0100
     3.2 +++ b/src/HOL/Nat.thy	Tue Mar 18 16:29:32 2014 +0100
     3.3 @@ -445,6 +445,9 @@
     3.4  lemma less_Suc_eq_le [code]: "m < Suc n \<longleftrightarrow> m \<le> n"
     3.5    by (simp add: less_eq_Suc_le)
     3.6  
     3.7 +lemma Suc_less_eq2: "Suc n < m \<longleftrightarrow> (\<exists>m'. m = Suc m' \<and> n < m')"
     3.8 +  by (cases m) auto
     3.9 +
    3.10  lemma le_SucI: "m \<le> n \<Longrightarrow> m \<le> Suc n"
    3.11    by (induct m arbitrary: n)
    3.12      (simp_all add: less_eq_nat.simps(2) split: nat.splits)
    3.13 @@ -746,6 +749,9 @@
    3.14                 intro!: Nat.add_0_right [symmetric] add_Suc_right [symmetric])
    3.15    done
    3.16  
    3.17 +lemma le_Suc_ex: "(k::nat) \<le> l \<Longrightarrow> (\<exists>n. l = k + n)"
    3.18 +  by (auto simp: less_Suc_eq_le[symmetric] dest: less_imp_Suc_add)
    3.19 +
    3.20  text {* strict, in 1st argument; proof is by induction on @{text "k > 0"} *}
    3.21  lemma mult_less_mono2: "(i::nat) < j ==> 0<k ==> k * i < k * j"
    3.22  apply(auto simp: gr0_conv_Suc)
     4.1 --- a/src/HOL/Real_Vector_Spaces.thy	Tue Mar 18 15:53:48 2014 +0100
     4.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Tue Mar 18 16:29:32 2014 +0100
     4.3 @@ -747,6 +747,11 @@
     4.4    shows "\<lbrakk>norm a \<le> r; norm b \<le> s\<rbrakk> \<Longrightarrow> norm (a + b) \<le> r + s"
     4.5  by (metis add_mono_thms_linordered_semiring(1) norm_triangle_ineq order.trans)
     4.6  
     4.7 +lemma norm_setsum:
     4.8 +  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
     4.9 +  shows "norm (setsum f A) \<le> (\<Sum>i\<in>A. norm (f i))"
    4.10 +  by (induct A rule: infinite_finite_induct) (auto intro: norm_triangle_mono)
    4.11 +
    4.12  lemma abs_norm_cancel [simp]:
    4.13    fixes a :: "'a::real_normed_vector"
    4.14    shows "\<bar>norm a\<bar> = norm a"
     5.1 --- a/src/HOL/Series.thy	Tue Mar 18 15:53:48 2014 +0100
     5.2 +++ b/src/HOL/Series.thy	Tue Mar 18 16:29:32 2014 +0100
     5.3 @@ -13,74 +13,6 @@
     5.4  imports Limits
     5.5  begin
     5.6  
     5.7 -(* TODO: MOVE *)
     5.8 -lemma Suc_less_iff: "Suc n < m \<longleftrightarrow> (\<exists>m'. m = Suc m' \<and> n < m')"
     5.9 -  by (cases m) auto
    5.10 -
    5.11 -(* TODO: MOVE *)
    5.12 -lemma norm_ratiotest_lemma:
    5.13 -  fixes x y :: "'a::real_normed_vector"
    5.14 -  shows "\<lbrakk>c \<le> 0; norm x \<le> c * norm y\<rbrakk> \<Longrightarrow> x = 0"
    5.15 -apply (subgoal_tac "norm x \<le> 0", simp)
    5.16 -apply (erule order_trans)
    5.17 -apply (simp add: mult_le_0_iff)
    5.18 -done
    5.19 -
    5.20 -(* TODO: MOVE *)
    5.21 -lemma rabs_ratiotest_lemma: "[| c \<le> 0; abs x \<le> c * abs y |] ==> x = (0::real)"
    5.22 -by (erule norm_ratiotest_lemma, simp)
    5.23 -
    5.24 -(* TODO: MOVE *)
    5.25 -lemma le_Suc_ex: "(k::nat) \<le> l ==> (\<exists>n. l = k + n)"
    5.26 -apply (drule le_imp_less_or_eq)
    5.27 -apply (auto dest: less_imp_Suc_add)
    5.28 -done
    5.29 -
    5.30 -(* MOVE *)
    5.31 -lemma setsum_even_minus_one [simp]: "(\<Sum>i<2 * n. (-1) ^ Suc i) = (0::'a::ring_1)"
    5.32 -  by (induct "n") auto
    5.33 -
    5.34 -(* MOVE *)
    5.35 -lemma setsum_nat_group: "(\<Sum>m<n::nat. setsum f {m * k ..< m*k + k}) = setsum f {..< n * k}"
    5.36 -  apply (subgoal_tac "k = 0 | 0 < k", auto)
    5.37 -  apply (induct "n")
    5.38 -  apply (simp_all add: setsum_add_nat_ivl add_commute atLeast0LessThan[symmetric])
    5.39 -  done
    5.40 -
    5.41 -(* MOVE *)
    5.42 -lemma norm_setsum:
    5.43 -  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
    5.44 -  shows "norm (setsum f A) \<le> (\<Sum>i\<in>A. norm (f i))"
    5.45 -  apply (case_tac "finite A")
    5.46 -  apply (erule finite_induct)
    5.47 -  apply simp
    5.48 -  apply simp
    5.49 -  apply (erule order_trans [OF norm_triangle_ineq add_left_mono])
    5.50 -  apply simp
    5.51 -  done
    5.52 -
    5.53 -(* MOVE *)
    5.54 -lemma norm_bound_subset:
    5.55 -  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
    5.56 -  assumes "finite s" "t \<subseteq> s"
    5.57 -  assumes le: "(\<And>x. x \<in> s \<Longrightarrow> norm(f x) \<le> g x)"
    5.58 -  shows "norm (setsum f t) \<le> setsum g s"
    5.59 -proof -
    5.60 -  have "norm (setsum f t) \<le> (\<Sum>i\<in>t. norm (f i))"
    5.61 -    by (rule norm_setsum)
    5.62 -  also have "\<dots> \<le> (\<Sum>i\<in>t. g i)"
    5.63 -    using assms by (auto intro!: setsum_mono)
    5.64 -  also have "\<dots> \<le> setsum g s"
    5.65 -    using assms order.trans[OF norm_ge_zero le]
    5.66 -    by (auto intro!: setsum_mono3)
    5.67 -  finally show ?thesis .
    5.68 -qed
    5.69 -
    5.70 -(* MOVE *)
    5.71 -lemma (in linorder) lessThan_minus_lessThan [simp]:
    5.72 -  "{..< n} - {..< m} = {m ..< n}"
    5.73 -  by auto
    5.74 -
    5.75  definition
    5.76    sums :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> 'a \<Rightarrow> bool"
    5.77    (infixr "sums" 80)
    5.78 @@ -455,8 +387,7 @@
    5.79  
    5.80  text{*Absolute convergence imples normal convergence*}
    5.81  
    5.82 -lemma summable_norm_cancel:
    5.83 -  "summable (\<lambda>n. norm (f n)) \<Longrightarrow> summable f"
    5.84 +lemma summable_norm_cancel: "summable (\<lambda>n. norm (f n)) \<Longrightarrow> summable f"
    5.85    apply (simp only: summable_Cauchy, safe)
    5.86    apply (drule_tac x="e" in spec, safe)
    5.87    apply (rule_tac x="N" in exI, safe)
    5.88 @@ -471,7 +402,7 @@
    5.89  
    5.90  text {* Comparison tests *}
    5.91  
    5.92 -lemma summable_comparison_test: "\<lbrakk>\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n; summable g\<rbrakk> \<Longrightarrow> summable f"
    5.93 +lemma summable_comparison_test: "\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n \<Longrightarrow> summable g \<Longrightarrow> summable f"
    5.94    apply (simp add: summable_Cauchy, safe)
    5.95    apply (drule_tac x="e" in spec, safe)
    5.96    apply (rule_tac x = "N + Na" in exI, safe)
    5.97 @@ -516,18 +447,15 @@
    5.98      finally have "f (Suc n) = 0"
    5.99        by auto }
   5.100    then show "summable f"
   5.101 -    by (intro sums_summable[OF sums_finite, of "{.. Suc N}"]) (auto simp: not_le Suc_less_iff)
   5.102 +    by (intro sums_summable[OF sums_finite, of "{.. Suc N}"]) (auto simp: not_le Suc_less_eq2)
   5.103  qed
   5.104  
   5.105  end
   5.106  
   5.107 -lemma summable_norm_comparison_test:
   5.108 -  "\<lbrakk>\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n; summable g\<rbrakk> \<Longrightarrow> summable (\<lambda>n. norm (f n))"
   5.109 +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))"
   5.110    by (rule summable_comparison_test) auto
   5.111  
   5.112 -lemma summable_rabs_cancel:
   5.113 -  fixes f :: "nat \<Rightarrow> real"
   5.114 -  shows "summable (\<lambda>n. \<bar>f n\<bar>) \<Longrightarrow> summable f"
   5.115 +lemma summable_rabs_cancel: "summable (\<lambda>n. \<bar>f n :: real\<bar>) \<Longrightarrow> summable f"
   5.116    by (rule summable_norm_cancel) simp
   5.117  
   5.118  text{*Summability of geometric series for real algebras*}
     6.1 --- a/src/HOL/Set_Interval.thy	Tue Mar 18 15:53:48 2014 +0100
     6.2 +++ b/src/HOL/Set_Interval.thy	Tue Mar 18 16:29:32 2014 +0100
     6.3 @@ -1193,6 +1193,10 @@
     6.4   "i \<le> n \<Longrightarrow> {i..<m} - {i..<n} = {n..<(m::'a::linorder)}"
     6.5  by(auto)
     6.6  
     6.7 +lemma (in linorder) lessThan_minus_lessThan [simp]:
     6.8 +  "{..< n} - {..< m} = {m ..< n}"
     6.9 +  by auto
    6.10 +
    6.11  
    6.12  subsubsection {* Some Subset Conditions *}
    6.13  
    6.14 @@ -1409,6 +1413,11 @@
    6.15    finally show ?thesis by auto
    6.16  qed
    6.17  
    6.18 +lemma setsum_nat_group: "(\<Sum>m<n::nat. setsum f {m * k ..< m*k + k}) = setsum f {..< n * k}"
    6.19 +  apply (subgoal_tac "k = 0 | 0 < k", auto)
    6.20 +  apply (induct "n")
    6.21 +  apply (simp_all add: setsum_add_nat_ivl add_commute atLeast0LessThan[symmetric])
    6.22 +  done
    6.23  
    6.24  subsection{* Shifting bounds *}
    6.25