moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
authorhoelzl
Fri Feb 12 16:09:07 2016 +0100 (2016-02-12)
changeset 62377ace69956d018
parent 62376 85f38d5f8807
child 62378 85ed00c1fe7c
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
src/HOL/Groups.thy
src/HOL/Groups_Big.thy
src/HOL/Rings.thy
src/HOL/Series.thy
     1.1 --- a/src/HOL/Groups.thy	Wed Feb 10 18:43:19 2016 +0100
     1.2 +++ b/src/HOL/Groups.thy	Fri Feb 12 16:09:07 2016 +0100
     1.3 @@ -589,6 +589,10 @@
     1.4  
     1.5  end
     1.6  
     1.7 +text\<open>Strict monotonicity in both arguments\<close>
     1.8 +class strict_ordered_ab_semigroup_add = ordered_ab_semigroup_add +
     1.9 +  assumes add_strict_mono: "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
    1.10 +
    1.11  class ordered_cancel_ab_semigroup_add =
    1.12    ordered_ab_semigroup_add + cancel_ab_semigroup_add
    1.13  begin
    1.14 @@ -601,12 +605,11 @@
    1.15    "a < b \<Longrightarrow> a + c < b + c"
    1.16  by (simp add: add.commute [of _ c] add_strict_left_mono)
    1.17  
    1.18 -text\<open>Strict monotonicity in both arguments\<close>
    1.19 -lemma add_strict_mono:
    1.20 -  "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
    1.21 -apply (erule add_strict_right_mono [THEN less_trans])
    1.22 -apply (erule add_strict_left_mono)
    1.23 -done
    1.24 +subclass strict_ordered_ab_semigroup_add
    1.25 +  apply standard
    1.26 +  apply (erule add_strict_right_mono [THEN less_trans])
    1.27 +  apply (erule add_strict_left_mono)
    1.28 +  done
    1.29  
    1.30  lemma add_less_le_mono:
    1.31    "a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c < b + d"
    1.32 @@ -622,8 +625,7 @@
    1.33  
    1.34  end
    1.35  
    1.36 -class ordered_ab_semigroup_add_imp_le =
    1.37 -  ordered_cancel_ab_semigroup_add +
    1.38 +class ordered_ab_semigroup_add_imp_le = ordered_cancel_ab_semigroup_add +
    1.39    assumes add_le_imp_le_left: "c + a \<le> c + b \<Longrightarrow> a \<le> b"
    1.40  begin
    1.41  
    1.42 @@ -695,40 +697,20 @@
    1.43  begin
    1.44  
    1.45  lemma add_nonneg_nonneg [simp]:
    1.46 -  assumes "0 \<le> a" and "0 \<le> b" shows "0 \<le> a + b"
    1.47 -proof -
    1.48 -  have "0 + 0 \<le> a + b"
    1.49 -    using assms by (rule add_mono)
    1.50 -  then show ?thesis by simp
    1.51 -qed
    1.52 +  "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a + b"
    1.53 +  using add_mono[of 0 a 0 b] by simp
    1.54  
    1.55  lemma add_nonpos_nonpos:
    1.56 -  assumes "a \<le> 0" and "b \<le> 0" shows "a + b \<le> 0"
    1.57 -proof -
    1.58 -  have "a + b \<le> 0 + 0"
    1.59 -    using assms by (rule add_mono)
    1.60 -  then show ?thesis by simp
    1.61 -qed
    1.62 +  "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> a + b \<le> 0"
    1.63 +  using add_mono[of a 0 b 0] by simp
    1.64  
    1.65  lemma add_nonneg_eq_0_iff:
    1.66 -  assumes x: "0 \<le> x" and y: "0 \<le> y"
    1.67 -  shows "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
    1.68 -proof (intro iffI conjI)
    1.69 -  have "x = x + 0" by simp
    1.70 -  also have "x + 0 \<le> x + y" using y by (rule add_left_mono)
    1.71 -  also assume "x + y = 0"
    1.72 -  also have "0 \<le> x" using x .
    1.73 -  finally show "x = 0" .
    1.74 -next
    1.75 -  have "y = 0 + y" by simp
    1.76 -  also have "0 + y \<le> x + y" using x by (rule add_right_mono)
    1.77 -  also assume "x + y = 0"
    1.78 -  also have "0 \<le> y" using y .
    1.79 -  finally show "y = 0" .
    1.80 -next
    1.81 -  assume "x = 0 \<and> y = 0"
    1.82 -  then show "x + y = 0" by simp
    1.83 -qed
    1.84 +  "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
    1.85 +  using add_left_mono[of 0 y x] add_right_mono[of 0 x y] by auto
    1.86 +
    1.87 +lemma add_nonpos_eq_0_iff:
    1.88 +  "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
    1.89 +  using add_left_mono[of y 0 x] add_right_mono[of x 0 y] by auto
    1.90  
    1.91  lemma add_increasing:
    1.92    "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"
    1.93 @@ -738,134 +720,46 @@
    1.94    "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"
    1.95    by (simp add: add_increasing add.commute [of a])
    1.96  
    1.97 -end
    1.98 -
    1.99 -class canonically_ordered_monoid_add = comm_monoid_add + order +
   1.100 -  assumes le_iff_add: "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)"
   1.101 -begin
   1.102 -
   1.103 -subclass ordered_comm_monoid_add
   1.104 -  proof qed (auto simp: le_iff_add add_ac)
   1.105 -
   1.106 -lemma zero_le: "0 \<le> x"
   1.107 -  by (auto simp: le_iff_add)
   1.108 -
   1.109 -lemma add_eq_0_iff_both_eq_0: "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   1.110 -  by (intro add_nonneg_eq_0_iff zero_le)
   1.111 -
   1.112 -end
   1.113 -
   1.114 -class ordered_cancel_comm_monoid_diff =
   1.115 -  canonically_ordered_monoid_add + comm_monoid_diff + ordered_ab_semigroup_add_imp_le
   1.116 -begin
   1.117 -
   1.118 -context
   1.119 -  fixes a b
   1.120 -  assumes "a \<le> b"
   1.121 -begin
   1.122 -
   1.123 -lemma add_diff_inverse:
   1.124 -  "a + (b - a) = b"
   1.125 -  using \<open>a \<le> b\<close> by (auto simp add: le_iff_add)
   1.126 +lemma add_decreasing:
   1.127 +  "a \<le> 0 \<Longrightarrow> c \<le> b \<Longrightarrow> a + c \<le> b"
   1.128 +  using add_mono[of a 0 c b] by simp
   1.129  
   1.130 -lemma add_diff_assoc:
   1.131 -  "c + (b - a) = c + b - a"
   1.132 -  using \<open>a \<le> b\<close> by (auto simp add: le_iff_add add.left_commute [of c])
   1.133 -
   1.134 -lemma add_diff_assoc2:
   1.135 -  "b - a + c = b + c - a"
   1.136 -  using \<open>a \<le> b\<close> by (auto simp add: le_iff_add add.assoc)
   1.137 -
   1.138 -lemma diff_add_assoc:
   1.139 -  "c + b - a = c + (b - a)"
   1.140 -  using \<open>a \<le> b\<close> by (simp add: add.commute add_diff_assoc)
   1.141 -
   1.142 -lemma diff_add_assoc2:
   1.143 -  "b + c - a = b - a + c"
   1.144 -  using \<open>a \<le> b\<close>by (simp add: add.commute add_diff_assoc)
   1.145 +lemma add_decreasing2:
   1.146 +  "c \<le> 0 \<Longrightarrow> a \<le> b \<Longrightarrow> a + c \<le> b"
   1.147 +  using add_mono[of a b c 0] by simp
   1.148  
   1.149 -lemma diff_diff_right:
   1.150 -  "c - (b - a) = c + a - b"
   1.151 -  by (simp add: add_diff_inverse add_diff_cancel_left [of a c "b - a", symmetric] add.commute)
   1.152 -
   1.153 -lemma diff_add:
   1.154 -  "b - a + a = b"
   1.155 -  by (simp add: add.commute add_diff_inverse)
   1.156 -
   1.157 -lemma le_add_diff:
   1.158 -  "c \<le> b + c - a"
   1.159 -  by (auto simp add: add.commute diff_add_assoc2 le_iff_add)
   1.160 -
   1.161 -lemma le_imp_diff_is_add:
   1.162 -  "a \<le> b \<Longrightarrow> b - a = c \<longleftrightarrow> b = c + a"
   1.163 -  by (auto simp add: add.commute add_diff_inverse)
   1.164 +lemma add_pos_nonneg: "0 < a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 < a + b"
   1.165 +  using less_le_trans[of 0 a "a + b"] by (simp add: add_increasing2)
   1.166  
   1.167 -lemma le_diff_conv2:
   1.168 -  "c \<le> b - a \<longleftrightarrow> c + a \<le> b" (is "?P \<longleftrightarrow> ?Q")
   1.169 -proof
   1.170 -  assume ?P
   1.171 -  then have "c + a \<le> b - a + a" by (rule add_right_mono)
   1.172 -  then show ?Q by (simp add: add_diff_inverse add.commute)
   1.173 -next
   1.174 -  assume ?Q
   1.175 -  then have "a + c \<le> a + (b - a)" by (simp add: add_diff_inverse add.commute)
   1.176 -  then show ?P by simp
   1.177 -qed
   1.178 -
   1.179 -end
   1.180 +lemma add_pos_pos: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a + b"
   1.181 +  by (intro add_pos_nonneg less_imp_le)
   1.182  
   1.183 -end
   1.184 -
   1.185 -class ordered_cancel_comm_monoid_add =
   1.186 -  ordered_comm_monoid_add + cancel_ab_semigroup_add
   1.187 -begin
   1.188 -
   1.189 -subclass ordered_cancel_ab_semigroup_add ..
   1.190 -
   1.191 -lemma add_neg_nonpos:
   1.192 -  assumes "a < 0" and "b \<le> 0" shows "a + b < 0"
   1.193 -proof -
   1.194 -  have "a + b < 0 + 0"
   1.195 -    using assms by (rule add_less_le_mono)
   1.196 -  then show ?thesis by simp
   1.197 -qed
   1.198 +lemma add_nonneg_pos: "0 \<le> a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a + b"
   1.199 +  using add_pos_nonneg[of b a] by (simp add: add_commute)
   1.200  
   1.201 -lemma add_neg_neg:
   1.202 -  assumes "a < 0" and "b < 0" shows "a + b < 0"
   1.203 -by (rule add_neg_nonpos) (insert assms, auto)
   1.204 -
   1.205 -lemma add_nonpos_neg:
   1.206 -  assumes "a \<le> 0" and "b < 0" shows "a + b < 0"
   1.207 -proof -
   1.208 -  have "a + b < 0 + 0"
   1.209 -    using assms by (rule add_le_less_mono)
   1.210 -  then show ?thesis by simp
   1.211 -qed
   1.212 +lemma add_neg_nonpos: "a < 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> a + b < 0"
   1.213 +  using le_less_trans[of "a + b" a 0] by (simp add: add_decreasing2)
   1.214  
   1.215 -lemma add_pos_nonneg:
   1.216 -  assumes "0 < a" and "0 \<le> b" shows "0 < a + b"
   1.217 -proof -
   1.218 -  have "0 + 0 < a + b"
   1.219 -    using assms by (rule add_less_le_mono)
   1.220 -  then show ?thesis by simp
   1.221 -qed
   1.222 +lemma add_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> a + b < 0"
   1.223 +  by (intro add_neg_nonpos less_imp_le)
   1.224  
   1.225 -lemma add_pos_pos:
   1.226 -  assumes "0 < a" and "0 < b" shows "0 < a + b"
   1.227 -by (rule add_pos_nonneg) (insert assms, auto)
   1.228 -
   1.229 -lemma add_nonneg_pos:
   1.230 -  assumes "0 \<le> a" and "0 < b" shows "0 < a + b"
   1.231 -proof -
   1.232 -  have "0 + 0 < a + b"
   1.233 -    using assms by (rule add_le_less_mono)
   1.234 -  then show ?thesis by simp
   1.235 -qed
   1.236 +lemma add_nonpos_neg: "a \<le> 0 \<Longrightarrow> b < 0 \<Longrightarrow> a + b < 0"
   1.237 +  using add_neg_nonpos[of b a] by (simp add: add_commute)
   1.238  
   1.239  lemmas add_sign_intros =
   1.240    add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg
   1.241    add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos
   1.242  
   1.243 +end
   1.244 +
   1.245 +class strict_ordered_comm_monoid_add = comm_monoid_add + strict_ordered_ab_semigroup_add
   1.246 +
   1.247 +class ordered_cancel_comm_monoid_add = ordered_comm_monoid_add + cancel_ab_semigroup_add
   1.248 +begin
   1.249 +
   1.250 +subclass ordered_cancel_ab_semigroup_add ..
   1.251 +subclass strict_ordered_comm_monoid_add ..
   1.252 +
   1.253  lemma add_strict_increasing:
   1.254    "0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c"
   1.255    by (insert add_less_le_mono [of 0 a b c], simp)
   1.256 @@ -1409,6 +1303,86 @@
   1.257  lemmas ab_left_minus = left_minus \<comment> \<open>FIXME duplicate\<close>
   1.258  lemmas diff_diff_eq = diff_diff_add \<comment> \<open>FIXME duplicate\<close>
   1.259  
   1.260 +subsection \<open>Canonically ordered monoids\<close>
   1.261 +
   1.262 +text \<open>Canonically ordered monoids are never groups.\<close>
   1.263 +
   1.264 +class canonically_ordered_monoid_add = comm_monoid_add + order +
   1.265 +  assumes le_iff_add: "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)"
   1.266 +begin
   1.267 +
   1.268 +lemma zero_le: "0 \<le> x"
   1.269 +  by (auto simp: le_iff_add)
   1.270 +
   1.271 +subclass ordered_comm_monoid_add
   1.272 +  proof qed (auto simp: le_iff_add add_ac)
   1.273 +
   1.274 +lemma add_eq_0_iff_both_eq_0: "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   1.275 +  by (intro add_nonneg_eq_0_iff zero_le)
   1.276 +
   1.277 +end
   1.278 +
   1.279 +class ordered_cancel_comm_monoid_diff =
   1.280 +  canonically_ordered_monoid_add + comm_monoid_diff + ordered_ab_semigroup_add_imp_le
   1.281 +begin
   1.282 +
   1.283 +context
   1.284 +  fixes a b
   1.285 +  assumes "a \<le> b"
   1.286 +begin
   1.287 +
   1.288 +lemma add_diff_inverse:
   1.289 +  "a + (b - a) = b"
   1.290 +  using \<open>a \<le> b\<close> by (auto simp add: le_iff_add)
   1.291 +
   1.292 +lemma add_diff_assoc:
   1.293 +  "c + (b - a) = c + b - a"
   1.294 +  using \<open>a \<le> b\<close> by (auto simp add: le_iff_add add.left_commute [of c])
   1.295 +
   1.296 +lemma add_diff_assoc2:
   1.297 +  "b - a + c = b + c - a"
   1.298 +  using \<open>a \<le> b\<close> by (auto simp add: le_iff_add add.assoc)
   1.299 +
   1.300 +lemma diff_add_assoc:
   1.301 +  "c + b - a = c + (b - a)"
   1.302 +  using \<open>a \<le> b\<close> by (simp add: add.commute add_diff_assoc)
   1.303 +
   1.304 +lemma diff_add_assoc2:
   1.305 +  "b + c - a = b - a + c"
   1.306 +  using \<open>a \<le> b\<close>by (simp add: add.commute add_diff_assoc)
   1.307 +
   1.308 +lemma diff_diff_right:
   1.309 +  "c - (b - a) = c + a - b"
   1.310 +  by (simp add: add_diff_inverse add_diff_cancel_left [of a c "b - a", symmetric] add.commute)
   1.311 +
   1.312 +lemma diff_add:
   1.313 +  "b - a + a = b"
   1.314 +  by (simp add: add.commute add_diff_inverse)
   1.315 +
   1.316 +lemma le_add_diff:
   1.317 +  "c \<le> b + c - a"
   1.318 +  by (auto simp add: add.commute diff_add_assoc2 le_iff_add)
   1.319 +
   1.320 +lemma le_imp_diff_is_add:
   1.321 +  "a \<le> b \<Longrightarrow> b - a = c \<longleftrightarrow> b = c + a"
   1.322 +  by (auto simp add: add.commute add_diff_inverse)
   1.323 +
   1.324 +lemma le_diff_conv2:
   1.325 +  "c \<le> b - a \<longleftrightarrow> c + a \<le> b" (is "?P \<longleftrightarrow> ?Q")
   1.326 +proof
   1.327 +  assume ?P
   1.328 +  then have "c + a \<le> b - a + a" by (rule add_right_mono)
   1.329 +  then show ?Q by (simp add: add_diff_inverse add.commute)
   1.330 +next
   1.331 +  assume ?Q
   1.332 +  then have "a + c \<le> a + (b - a)" by (simp add: add_diff_inverse add.commute)
   1.333 +  then show ?P by simp
   1.334 +qed
   1.335 +
   1.336 +end
   1.337 +
   1.338 +end
   1.339 +
   1.340  subsection \<open>Tools setup\<close>
   1.341  
   1.342  lemma add_mono_thms_linordered_semiring:
   1.343 @@ -1433,4 +1407,3 @@
   1.344    code_module Groups \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
   1.345  
   1.346  end
   1.347 -
     2.1 --- a/src/HOL/Groups_Big.thy	Wed Feb 10 18:43:19 2016 +0100
     2.2 +++ b/src/HOL/Groups_Big.thy	Fri Feb 12 16:09:07 2016 +0100
     2.3 @@ -579,7 +579,7 @@
     2.4    case False then show ?thesis by simp
     2.5  qed
     2.6  
     2.7 -lemma (in ordered_cancel_comm_monoid_add) setsum_strict_mono:
     2.8 +lemma (in strict_ordered_comm_monoid_add) setsum_strict_mono:
     2.9    assumes "finite A"  "A \<noteq> {}" and "\<And>x. x \<in> A \<Longrightarrow> f x < g x"
    2.10    shows "setsum f A < setsum g A"
    2.11    using assms
    2.12 @@ -591,7 +591,7 @@
    2.13  
    2.14  lemma setsum_strict_mono_ex1:
    2.15    fixes f g :: "'i \<Rightarrow> 'a::ordered_cancel_comm_monoid_add"
    2.16 -  assumes "finite A" and "ALL x:A. f x \<le> g x" and "\<exists>a\<in>A. f a < g a"
    2.17 +  assumes "finite A" and "\<forall>x\<in>A. f x \<le> g x" and "\<exists>a\<in>A. f a < g a"
    2.18    shows "setsum f A < setsum g A"
    2.19  proof-
    2.20    from assms(3) obtain a where a: "a:A" "f a < g a" by blast
    2.21 @@ -882,15 +882,17 @@
    2.22    "(\<And>a. a \<in> A \<Longrightarrow> d dvd f a) \<Longrightarrow> d dvd setsum f A"
    2.23    by (induct A rule: infinite_finite_induct) simp_all
    2.24  
    2.25 -lemma setsum_pos2:
    2.26 -    assumes "finite I" "i \<in> I" "0 < f i" "(\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i)"
    2.27 -      shows "(0::'a::{ordered_ab_group_add,comm_monoid_add}) < setsum f I"
    2.28 +lemma (in ordered_comm_monoid_add) setsum_pos:
    2.29 +  "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 < f i) \<Longrightarrow> 0 < setsum f I"
    2.30 +  by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos)
    2.31 +
    2.32 +lemma (in ordered_comm_monoid_add) setsum_pos2:
    2.33 +  assumes I: "finite I" "i \<in> I" "0 < f i" "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
    2.34 +  shows "0 < setsum f I"
    2.35  proof -
    2.36 -  have "0 \<le> setsum f (I-{i})"
    2.37 -    using assms by (simp add: setsum_nonneg)
    2.38 -  also have "... < setsum f (I-{i}) + f i"
    2.39 -    using assms by auto
    2.40 -  also have "... = setsum f I"
    2.41 +  have "0 < f i + setsum f (I - {i})"
    2.42 +    using assms by (intro add_pos_nonneg setsum_nonneg) auto
    2.43 +  also have "\<dots> = setsum f I"
    2.44      using assms by (simp add: setsum.remove)
    2.45    finally show ?thesis .
    2.46  qed
    2.47 @@ -992,11 +994,6 @@
    2.48    finally show ?thesis by auto
    2.49  qed
    2.50  
    2.51 -lemma (in ordered_cancel_comm_monoid_add) setsum_pos:
    2.52 -  "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 < f i) \<Longrightarrow> 0 < setsum f I"
    2.53 -  by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos)
    2.54 -
    2.55 -
    2.56  subsubsection \<open>Cardinality of products\<close>
    2.57  
    2.58  lemma card_SigmaI [simp]:
     3.1 --- a/src/HOL/Rings.thy	Wed Feb 10 18:43:19 2016 +0100
     3.2 +++ b/src/HOL/Rings.thy	Fri Feb 12 16:09:07 2016 +0100
     3.3 @@ -1296,11 +1296,9 @@
     3.4  
     3.5  end
     3.6  
     3.7 -class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add
     3.8 +class ordered_semiring_0 = semiring_0 + ordered_semiring
     3.9  begin
    3.10  
    3.11 -subclass semiring_0_cancel ..
    3.12 -
    3.13  lemma mult_nonneg_nonneg[simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
    3.14  using mult_left_mono [of 0 b a] by simp
    3.15  
    3.16 @@ -1319,6 +1317,14 @@
    3.17  
    3.18  end
    3.19  
    3.20 +class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add
    3.21 +begin
    3.22 +
    3.23 +subclass semiring_0_cancel ..
    3.24 +subclass ordered_semiring_0 ..
    3.25 +
    3.26 +end
    3.27 +
    3.28  class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add
    3.29  begin
    3.30  
     4.1 --- a/src/HOL/Series.thy	Wed Feb 10 18:43:19 2016 +0100
     4.2 +++ b/src/HOL/Series.thy	Fri Feb 12 16:09:07 2016 +0100
     4.3 @@ -228,6 +228,24 @@
     4.4      by (auto intro!: antisym)
     4.5  qed (metis suminf_zero fun_eq_iff)
     4.6  
     4.7 +lemma suminf_pos_iff:
     4.8 +  "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
     4.9 +  using setsum_le_suminf[of 0] suminf_eq_zero_iff by (simp add: less_le)
    4.10 +
    4.11 +lemma suminf_pos2:
    4.12 +  assumes "summable f" "\<forall>n. 0 \<le> f n" "0 < f i"
    4.13 +  shows "0 < suminf f"
    4.14 +proof -
    4.15 +  have "0 < (\<Sum>n<Suc i. f n)"
    4.16 +    using assms by (intro setsum_pos2[where i=i]) auto
    4.17 +  also have "\<dots> \<le> suminf f"
    4.18 +    using assms by (intro setsum_le_suminf) auto
    4.19 +  finally show ?thesis .
    4.20 +qed
    4.21 +
    4.22 +lemma suminf_pos: "summable f \<Longrightarrow> \<forall>n. 0 < f n \<Longrightarrow> 0 < suminf f"
    4.23 +  by (intro suminf_pos2[where i=0]) (auto intro: less_imp_le)
    4.24 +
    4.25  end
    4.26  
    4.27  context
    4.28 @@ -244,16 +262,6 @@
    4.29  lemma setsum_less_suminf: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 < f m \<Longrightarrow> setsum f {..<n} < suminf f"
    4.30    using setsum_less_suminf2[of n n] by (simp add: less_imp_le)
    4.31  
    4.32 -lemma suminf_pos2: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < f i \<Longrightarrow> 0 < suminf f"
    4.33 -  using setsum_less_suminf2[of 0 i] by simp
    4.34 -
    4.35 -lemma suminf_pos: "summable f \<Longrightarrow> \<forall>n. 0 < f n \<Longrightarrow> 0 < suminf f"
    4.36 -  using suminf_pos2[of 0] by (simp add: less_imp_le)
    4.37 -
    4.38 -lemma suminf_pos_iff:
    4.39 -  "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
    4.40 -  using setsum_le_suminf[of f 0] suminf_eq_zero_iff[of f] by (simp add: less_le)
    4.41 -
    4.42  end
    4.43  
    4.44  lemma summableI_nonneg_bounded:
    4.45 @@ -261,23 +269,18 @@
    4.46    assumes pos[simp]: "\<And>n. 0 \<le> f n" and le: "\<And>n. (\<Sum>i<n. f i) \<le> x"
    4.47    shows "summable f"
    4.48    unfolding summable_def sums_def[abs_def]
    4.49 -proof (intro exI order_tendstoI)
    4.50 -  have [simp, intro]: "bdd_above (range (\<lambda>n. \<Sum>i<n. f i))"
    4.51 +proof (rule exI LIMSEQ_incseq_SUP)+
    4.52 +  show "bdd_above (range (\<lambda>n. setsum f {..<n}))"
    4.53      using le by (auto simp: bdd_above_def)
    4.54 -  { fix a assume "a < (SUP n. \<Sum>i<n. f i)"
    4.55 -    then obtain n where "a < (\<Sum>i<n. f i)"
    4.56 -      by (auto simp add: less_cSUP_iff)
    4.57 -    then have "\<And>m. n \<le> m \<Longrightarrow> a < (\<Sum>i<m. f i)"
    4.58 -      by (rule less_le_trans) (auto intro!: setsum_mono2)
    4.59 -    then show "eventually (\<lambda>n. a < (\<Sum>i<n. f i)) sequentially"
    4.60 -      by (auto simp: eventually_sequentially) }
    4.61 -  { fix a assume "(SUP n. \<Sum>i<n. f i) < a"
    4.62 -    moreover have "\<And>n. (\<Sum>i<n. f i) \<le> (SUP n. \<Sum>i<n. f i)"
    4.63 -      by (auto intro: cSUP_upper)
    4.64 -    ultimately show "eventually (\<lambda>n. (\<Sum>i<n. f i) < a) sequentially"
    4.65 -      by (auto intro: le_less_trans simp: eventually_sequentially) }
    4.66 +  show "incseq (\<lambda>n. setsum f {..<n})"
    4.67 +    by (auto simp: mono_def intro!: setsum_mono2)
    4.68  qed
    4.69  
    4.70 +lemma summableI[intro, simp]:
    4.71 +  fixes f:: "nat \<Rightarrow> 'a::{canonically_ordered_monoid_add, linorder_topology, complete_linorder}"
    4.72 +  shows "summable f"
    4.73 +  by (intro summableI_nonneg_bounded[where x=top] zero_le top_greatest)
    4.74 +
    4.75  subsection \<open>Infinite summability on topological monoids\<close>
    4.76  
    4.77  lemma Zero_notin_Suc: "0 \<notin> Suc ` A"