# HG changeset patch
# User hoelzl
# Date 1455289747 -3600
# Node ID ace69956d01852f7d5992a97851473d2f96eec9b
# Parent  85f38d5f88079843262a90015e21cb30d54acf92
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add

diff -r 85f38d5f8807 -r ace69956d018 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Wed Feb 10 18:43:19 2016 +0100
+++ b/src/HOL/Groups.thy	Fri Feb 12 16:09:07 2016 +0100
@@ -589,6 +589,10 @@
 
 end
 
+text\<open>Strict monotonicity in both arguments\<close>
+class strict_ordered_ab_semigroup_add = ordered_ab_semigroup_add +
+  assumes add_strict_mono: "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
+
 class ordered_cancel_ab_semigroup_add =
   ordered_ab_semigroup_add + cancel_ab_semigroup_add
 begin
@@ -601,12 +605,11 @@
   "a < b \<Longrightarrow> a + c < b + c"
 by (simp add: add.commute [of _ c] add_strict_left_mono)
 
-text\<open>Strict monotonicity in both arguments\<close>
-lemma add_strict_mono:
-  "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
-apply (erule add_strict_right_mono [THEN less_trans])
-apply (erule add_strict_left_mono)
-done
+subclass strict_ordered_ab_semigroup_add
+  apply standard
+  apply (erule add_strict_right_mono [THEN less_trans])
+  apply (erule add_strict_left_mono)
+  done
 
 lemma add_less_le_mono:
   "a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c < b + d"
@@ -622,8 +625,7 @@
 
 end
 
-class ordered_ab_semigroup_add_imp_le =
-  ordered_cancel_ab_semigroup_add +
+class ordered_ab_semigroup_add_imp_le = ordered_cancel_ab_semigroup_add +
   assumes add_le_imp_le_left: "c + a \<le> c + b \<Longrightarrow> a \<le> b"
 begin
 
@@ -695,40 +697,20 @@
 begin
 
 lemma add_nonneg_nonneg [simp]:
-  assumes "0 \<le> a" and "0 \<le> b" shows "0 \<le> a + b"
-proof -
-  have "0 + 0 \<le> a + b"
-    using assms by (rule add_mono)
-  then show ?thesis by simp
-qed
+  "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a + b"
+  using add_mono[of 0 a 0 b] by simp
 
 lemma add_nonpos_nonpos:
-  assumes "a \<le> 0" and "b \<le> 0" shows "a + b \<le> 0"
-proof -
-  have "a + b \<le> 0 + 0"
-    using assms by (rule add_mono)
-  then show ?thesis by simp
-qed
+  "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> a + b \<le> 0"
+  using add_mono[of a 0 b 0] by simp
 
 lemma add_nonneg_eq_0_iff:
-  assumes x: "0 \<le> x" and y: "0 \<le> y"
-  shows "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
-proof (intro iffI conjI)
-  have "x = x + 0" by simp
-  also have "x + 0 \<le> x + y" using y by (rule add_left_mono)
-  also assume "x + y = 0"
-  also have "0 \<le> x" using x .
-  finally show "x = 0" .
-next
-  have "y = 0 + y" by simp
-  also have "0 + y \<le> x + y" using x by (rule add_right_mono)
-  also assume "x + y = 0"
-  also have "0 \<le> y" using y .
-  finally show "y = 0" .
-next
-  assume "x = 0 \<and> y = 0"
-  then show "x + y = 0" by simp
-qed
+  "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
+  using add_left_mono[of 0 y x] add_right_mono[of 0 x y] by auto
+
+lemma add_nonpos_eq_0_iff:
+  "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
+  using add_left_mono[of y 0 x] add_right_mono[of x 0 y] by auto
 
 lemma add_increasing:
   "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"
@@ -738,134 +720,46 @@
   "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"
   by (simp add: add_increasing add.commute [of a])
 
-end
-
-class canonically_ordered_monoid_add = comm_monoid_add + order +
-  assumes le_iff_add: "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)"
-begin
-
-subclass ordered_comm_monoid_add
-  proof qed (auto simp: le_iff_add add_ac)
-
-lemma zero_le: "0 \<le> x"
-  by (auto simp: le_iff_add)
-
-lemma add_eq_0_iff_both_eq_0: "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
-  by (intro add_nonneg_eq_0_iff zero_le)
-
-end
-
-class ordered_cancel_comm_monoid_diff =
-  canonically_ordered_monoid_add + comm_monoid_diff + ordered_ab_semigroup_add_imp_le
-begin
-
-context
-  fixes a b
-  assumes "a \<le> b"
-begin
-
-lemma add_diff_inverse:
-  "a + (b - a) = b"
-  using \<open>a \<le> b\<close> by (auto simp add: le_iff_add)
+lemma add_decreasing:
+  "a \<le> 0 \<Longrightarrow> c \<le> b \<Longrightarrow> a + c \<le> b"
+  using add_mono[of a 0 c b] by simp
 
-lemma add_diff_assoc:
-  "c + (b - a) = c + b - a"
-  using \<open>a \<le> b\<close> by (auto simp add: le_iff_add add.left_commute [of c])
-
-lemma add_diff_assoc2:
-  "b - a + c = b + c - a"
-  using \<open>a \<le> b\<close> by (auto simp add: le_iff_add add.assoc)
-
-lemma diff_add_assoc:
-  "c + b - a = c + (b - a)"
-  using \<open>a \<le> b\<close> by (simp add: add.commute add_diff_assoc)
-
-lemma diff_add_assoc2:
-  "b + c - a = b - a + c"
-  using \<open>a \<le> b\<close>by (simp add: add.commute add_diff_assoc)
+lemma add_decreasing2:
+  "c \<le> 0 \<Longrightarrow> a \<le> b \<Longrightarrow> a + c \<le> b"
+  using add_mono[of a b c 0] by simp
 
-lemma diff_diff_right:
-  "c - (b - a) = c + a - b"
-  by (simp add: add_diff_inverse add_diff_cancel_left [of a c "b - a", symmetric] add.commute)
-
-lemma diff_add:
-  "b - a + a = b"
-  by (simp add: add.commute add_diff_inverse)
-
-lemma le_add_diff:
-  "c \<le> b + c - a"
-  by (auto simp add: add.commute diff_add_assoc2 le_iff_add)
-
-lemma le_imp_diff_is_add:
-  "a \<le> b \<Longrightarrow> b - a = c \<longleftrightarrow> b = c + a"
-  by (auto simp add: add.commute add_diff_inverse)
+lemma add_pos_nonneg: "0 < a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 < a + b"
+  using less_le_trans[of 0 a "a + b"] by (simp add: add_increasing2)
 
-lemma le_diff_conv2:
-  "c \<le> b - a \<longleftrightarrow> c + a \<le> b" (is "?P \<longleftrightarrow> ?Q")
-proof
-  assume ?P
-  then have "c + a \<le> b - a + a" by (rule add_right_mono)
-  then show ?Q by (simp add: add_diff_inverse add.commute)
-next
-  assume ?Q
-  then have "a + c \<le> a + (b - a)" by (simp add: add_diff_inverse add.commute)
-  then show ?P by simp
-qed
-
-end
+lemma add_pos_pos: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a + b"
+  by (intro add_pos_nonneg less_imp_le)
 
-end
-
-class ordered_cancel_comm_monoid_add =
-  ordered_comm_monoid_add + cancel_ab_semigroup_add
-begin
-
-subclass ordered_cancel_ab_semigroup_add ..
-
-lemma add_neg_nonpos:
-  assumes "a < 0" and "b \<le> 0" shows "a + b < 0"
-proof -
-  have "a + b < 0 + 0"
-    using assms by (rule add_less_le_mono)
-  then show ?thesis by simp
-qed
+lemma add_nonneg_pos: "0 \<le> a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a + b"
+  using add_pos_nonneg[of b a] by (simp add: add_commute)
 
-lemma add_neg_neg:
-  assumes "a < 0" and "b < 0" shows "a + b < 0"
-by (rule add_neg_nonpos) (insert assms, auto)
-
-lemma add_nonpos_neg:
-  assumes "a \<le> 0" and "b < 0" shows "a + b < 0"
-proof -
-  have "a + b < 0 + 0"
-    using assms by (rule add_le_less_mono)
-  then show ?thesis by simp
-qed
+lemma add_neg_nonpos: "a < 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> a + b < 0"
+  using le_less_trans[of "a + b" a 0] by (simp add: add_decreasing2)
 
-lemma add_pos_nonneg:
-  assumes "0 < a" and "0 \<le> b" shows "0 < a + b"
-proof -
-  have "0 + 0 < a + b"
-    using assms by (rule add_less_le_mono)
-  then show ?thesis by simp
-qed
+lemma add_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> a + b < 0"
+  by (intro add_neg_nonpos less_imp_le)
 
-lemma add_pos_pos:
-  assumes "0 < a" and "0 < b" shows "0 < a + b"
-by (rule add_pos_nonneg) (insert assms, auto)
-
-lemma add_nonneg_pos:
-  assumes "0 \<le> a" and "0 < b" shows "0 < a + b"
-proof -
-  have "0 + 0 < a + b"
-    using assms by (rule add_le_less_mono)
-  then show ?thesis by simp
-qed
+lemma add_nonpos_neg: "a \<le> 0 \<Longrightarrow> b < 0 \<Longrightarrow> a + b < 0"
+  using add_neg_nonpos[of b a] by (simp add: add_commute)
 
 lemmas add_sign_intros =
   add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg
   add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos
 
+end
+
+class strict_ordered_comm_monoid_add = comm_monoid_add + strict_ordered_ab_semigroup_add
+
+class ordered_cancel_comm_monoid_add = ordered_comm_monoid_add + cancel_ab_semigroup_add
+begin
+
+subclass ordered_cancel_ab_semigroup_add ..
+subclass strict_ordered_comm_monoid_add ..
+
 lemma add_strict_increasing:
   "0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c"
   by (insert add_less_le_mono [of 0 a b c], simp)
@@ -1409,6 +1303,86 @@
 lemmas ab_left_minus = left_minus \<comment> \<open>FIXME duplicate\<close>
 lemmas diff_diff_eq = diff_diff_add \<comment> \<open>FIXME duplicate\<close>
 
+subsection \<open>Canonically ordered monoids\<close>
+
+text \<open>Canonically ordered monoids are never groups.\<close>
+
+class canonically_ordered_monoid_add = comm_monoid_add + order +
+  assumes le_iff_add: "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)"
+begin
+
+lemma zero_le: "0 \<le> x"
+  by (auto simp: le_iff_add)
+
+subclass ordered_comm_monoid_add
+  proof qed (auto simp: le_iff_add add_ac)
+
+lemma add_eq_0_iff_both_eq_0: "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
+  by (intro add_nonneg_eq_0_iff zero_le)
+
+end
+
+class ordered_cancel_comm_monoid_diff =
+  canonically_ordered_monoid_add + comm_monoid_diff + ordered_ab_semigroup_add_imp_le
+begin
+
+context
+  fixes a b
+  assumes "a \<le> b"
+begin
+
+lemma add_diff_inverse:
+  "a + (b - a) = b"
+  using \<open>a \<le> b\<close> by (auto simp add: le_iff_add)
+
+lemma add_diff_assoc:
+  "c + (b - a) = c + b - a"
+  using \<open>a \<le> b\<close> by (auto simp add: le_iff_add add.left_commute [of c])
+
+lemma add_diff_assoc2:
+  "b - a + c = b + c - a"
+  using \<open>a \<le> b\<close> by (auto simp add: le_iff_add add.assoc)
+
+lemma diff_add_assoc:
+  "c + b - a = c + (b - a)"
+  using \<open>a \<le> b\<close> by (simp add: add.commute add_diff_assoc)
+
+lemma diff_add_assoc2:
+  "b + c - a = b - a + c"
+  using \<open>a \<le> b\<close>by (simp add: add.commute add_diff_assoc)
+
+lemma diff_diff_right:
+  "c - (b - a) = c + a - b"
+  by (simp add: add_diff_inverse add_diff_cancel_left [of a c "b - a", symmetric] add.commute)
+
+lemma diff_add:
+  "b - a + a = b"
+  by (simp add: add.commute add_diff_inverse)
+
+lemma le_add_diff:
+  "c \<le> b + c - a"
+  by (auto simp add: add.commute diff_add_assoc2 le_iff_add)
+
+lemma le_imp_diff_is_add:
+  "a \<le> b \<Longrightarrow> b - a = c \<longleftrightarrow> b = c + a"
+  by (auto simp add: add.commute add_diff_inverse)
+
+lemma le_diff_conv2:
+  "c \<le> b - a \<longleftrightarrow> c + a \<le> b" (is "?P \<longleftrightarrow> ?Q")
+proof
+  assume ?P
+  then have "c + a \<le> b - a + a" by (rule add_right_mono)
+  then show ?Q by (simp add: add_diff_inverse add.commute)
+next
+  assume ?Q
+  then have "a + c \<le> a + (b - a)" by (simp add: add_diff_inverse add.commute)
+  then show ?P by simp
+qed
+
+end
+
+end
+
 subsection \<open>Tools setup\<close>
 
 lemma add_mono_thms_linordered_semiring:
@@ -1433,4 +1407,3 @@
   code_module Groups \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
 end
-
diff -r 85f38d5f8807 -r ace69956d018 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Wed Feb 10 18:43:19 2016 +0100
+++ b/src/HOL/Groups_Big.thy	Fri Feb 12 16:09:07 2016 +0100
@@ -579,7 +579,7 @@
   case False then show ?thesis by simp
 qed
 
-lemma (in ordered_cancel_comm_monoid_add) setsum_strict_mono:
+lemma (in strict_ordered_comm_monoid_add) setsum_strict_mono:
   assumes "finite A"  "A \<noteq> {}" and "\<And>x. x \<in> A \<Longrightarrow> f x < g x"
   shows "setsum f A < setsum g A"
   using assms
@@ -591,7 +591,7 @@
 
 lemma setsum_strict_mono_ex1:
   fixes f g :: "'i \<Rightarrow> 'a::ordered_cancel_comm_monoid_add"
-  assumes "finite A" and "ALL x:A. f x \<le> g x" and "\<exists>a\<in>A. f a < g a"
+  assumes "finite A" and "\<forall>x\<in>A. f x \<le> g x" and "\<exists>a\<in>A. f a < g a"
   shows "setsum f A < setsum g A"
 proof-
   from assms(3) obtain a where a: "a:A" "f a < g a" by blast
@@ -882,15 +882,17 @@
   "(\<And>a. a \<in> A \<Longrightarrow> d dvd f a) \<Longrightarrow> d dvd setsum f A"
   by (induct A rule: infinite_finite_induct) simp_all
 
-lemma setsum_pos2:
-    assumes "finite I" "i \<in> I" "0 < f i" "(\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i)"
-      shows "(0::'a::{ordered_ab_group_add,comm_monoid_add}) < setsum f I"
+lemma (in ordered_comm_monoid_add) setsum_pos:
+  "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 < f i) \<Longrightarrow> 0 < setsum f I"
+  by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos)
+
+lemma (in ordered_comm_monoid_add) setsum_pos2:
+  assumes I: "finite I" "i \<in> I" "0 < f i" "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
+  shows "0 < setsum f I"
 proof -
-  have "0 \<le> setsum f (I-{i})"
-    using assms by (simp add: setsum_nonneg)
-  also have "... < setsum f (I-{i}) + f i"
-    using assms by auto
-  also have "... = setsum f I"
+  have "0 < f i + setsum f (I - {i})"
+    using assms by (intro add_pos_nonneg setsum_nonneg) auto
+  also have "\<dots> = setsum f I"
     using assms by (simp add: setsum.remove)
   finally show ?thesis .
 qed
@@ -992,11 +994,6 @@
   finally show ?thesis by auto
 qed
 
-lemma (in ordered_cancel_comm_monoid_add) setsum_pos:
-  "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 < f i) \<Longrightarrow> 0 < setsum f I"
-  by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos)
-
-
 subsubsection \<open>Cardinality of products\<close>
 
 lemma card_SigmaI [simp]:
diff -r 85f38d5f8807 -r ace69956d018 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Wed Feb 10 18:43:19 2016 +0100
+++ b/src/HOL/Rings.thy	Fri Feb 12 16:09:07 2016 +0100
@@ -1296,11 +1296,9 @@
 
 end
 
-class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add
+class ordered_semiring_0 = semiring_0 + ordered_semiring
 begin
 
-subclass semiring_0_cancel ..
-
 lemma mult_nonneg_nonneg[simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
 using mult_left_mono [of 0 b a] by simp
 
@@ -1319,6 +1317,14 @@
 
 end
 
+class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add
+begin
+
+subclass semiring_0_cancel ..
+subclass ordered_semiring_0 ..
+
+end
+
 class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add
 begin
 
diff -r 85f38d5f8807 -r ace69956d018 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Wed Feb 10 18:43:19 2016 +0100
+++ b/src/HOL/Series.thy	Fri Feb 12 16:09:07 2016 +0100
@@ -228,6 +228,24 @@
     by (auto intro!: antisym)
 qed (metis suminf_zero fun_eq_iff)
 
+lemma suminf_pos_iff:
+  "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
+  using setsum_le_suminf[of 0] suminf_eq_zero_iff by (simp add: less_le)
+
+lemma suminf_pos2:
+  assumes "summable f" "\<forall>n. 0 \<le> f n" "0 < f i"
+  shows "0 < suminf f"
+proof -
+  have "0 < (\<Sum>n<Suc i. f n)"
+    using assms by (intro setsum_pos2[where i=i]) auto
+  also have "\<dots> \<le> suminf f"
+    using assms by (intro setsum_le_suminf) auto
+  finally show ?thesis .
+qed
+
+lemma suminf_pos: "summable f \<Longrightarrow> \<forall>n. 0 < f n \<Longrightarrow> 0 < suminf f"
+  by (intro suminf_pos2[where i=0]) (auto intro: less_imp_le)
+
 end
 
 context
@@ -244,16 +262,6 @@
 lemma setsum_less_suminf: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 < f m \<Longrightarrow> setsum f {..<n} < suminf f"
   using setsum_less_suminf2[of n n] by (simp add: less_imp_le)
 
-lemma suminf_pos2: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < f i \<Longrightarrow> 0 < suminf f"
-  using setsum_less_suminf2[of 0 i] by simp
-
-lemma suminf_pos: "summable f \<Longrightarrow> \<forall>n. 0 < f n \<Longrightarrow> 0 < suminf f"
-  using suminf_pos2[of 0] by (simp add: less_imp_le)
-
-lemma suminf_pos_iff:
-  "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
-  using setsum_le_suminf[of f 0] suminf_eq_zero_iff[of f] by (simp add: less_le)
-
 end
 
 lemma summableI_nonneg_bounded:
@@ -261,23 +269,18 @@
   assumes pos[simp]: "\<And>n. 0 \<le> f n" and le: "\<And>n. (\<Sum>i<n. f i) \<le> x"
   shows "summable f"
   unfolding summable_def sums_def[abs_def]
-proof (intro exI order_tendstoI)
-  have [simp, intro]: "bdd_above (range (\<lambda>n. \<Sum>i<n. f i))"
+proof (rule exI LIMSEQ_incseq_SUP)+
+  show "bdd_above (range (\<lambda>n. setsum f {..<n}))"
     using le by (auto simp: bdd_above_def)
-  { fix a assume "a < (SUP n. \<Sum>i<n. f i)"
-    then obtain n where "a < (\<Sum>i<n. f i)"
-      by (auto simp add: less_cSUP_iff)
-    then have "\<And>m. n \<le> m \<Longrightarrow> a < (\<Sum>i<m. f i)"
-      by (rule less_le_trans) (auto intro!: setsum_mono2)
-    then show "eventually (\<lambda>n. a < (\<Sum>i<n. f i)) sequentially"
-      by (auto simp: eventually_sequentially) }
-  { fix a assume "(SUP n. \<Sum>i<n. f i) < a"
-    moreover have "\<And>n. (\<Sum>i<n. f i) \<le> (SUP n. \<Sum>i<n. f i)"
-      by (auto intro: cSUP_upper)
-    ultimately show "eventually (\<lambda>n. (\<Sum>i<n. f i) < a) sequentially"
-      by (auto intro: le_less_trans simp: eventually_sequentially) }
+  show "incseq (\<lambda>n. setsum f {..<n})"
+    by (auto simp: mono_def intro!: setsum_mono2)
 qed
 
+lemma summableI[intro, simp]:
+  fixes f:: "nat \<Rightarrow> 'a::{canonically_ordered_monoid_add, linorder_topology, complete_linorder}"
+  shows "summable f"
+  by (intro summableI_nonneg_bounded[where x=top] zero_le top_greatest)
+
 subsection \<open>Infinite summability on topological monoids\<close>
 
 lemma Zero_notin_Suc: "0 \<notin> Suc ` A"