moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
--- 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
-
--- 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]:
--- 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
--- 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"