# HG changeset patch
# User hoelzl
# Date 1455126199 -3600
# Node ID 85f38d5f88079843262a90015e21cb30d54acf92
# Parent  670063003ad33ef27ecc55ee29490ece38fdde56
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.

diff -r 670063003ad3 -r 85f38d5f8807 NEWS
--- a/NEWS	Tue Feb 09 09:21:10 2016 +0100
+++ b/NEWS	Wed Feb 10 18:43:19 2016 +0100
@@ -40,6 +40,15 @@
 
 * Class semiring_Lcd merged into semiring_Gcd.  INCOMPATIBILITY.
 
+* The type class ordered_comm_monoid_add is now called
+ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add is
+introduced as the combination of ordered_ab_semigroup_add + comm_monoid_add.
+INCOMPATIBILITY.
+
+* Introduced the type classes canonically_ordered_comm_monoid_add and dioid.
+
+* Added topological_monoid
+
 * Library/Polynomial.thy contains also derivation of polynomials
 but not gcd/lcm on polynomials over fields.  This has been moved
 to a separate theory Library/Polynomial_GCD_euclidean.thy, to
@@ -144,7 +153,6 @@
 * SML/NJ is no longer supported.
 
 
-
 New in Isabelle2016 (February 2016)
 -----------------------------------
 
diff -r 670063003ad3 -r 85f38d5f8807 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Tue Feb 09 09:21:10 2016 +0100
+++ b/src/HOL/Groups.thy	Wed Feb 10 18:43:19 2016 +0100
@@ -78,7 +78,7 @@
 
 subsection \<open>Generic operations\<close>
 
-class zero = 
+class zero =
   fixes zero :: 'a  ("0")
 
 class one =
@@ -310,7 +310,7 @@
   then show "c = a - b" by simp
 qed
 
-end  
+end
 
 class comm_monoid_diff = cancel_comm_monoid_add +
   assumes zero_diff [simp]: "0 - a = 0"
@@ -428,7 +428,7 @@
   by (simp only: diff_conv_add_uminus add_0_left)
 
 lemma diff_0_right [simp]:
-  "a - 0 = a" 
+  "a - 0 = a"
   by (simp only: diff_conv_add_uminus minus_zero add_0_right)
 
 lemma diff_minus_eq_add [simp]:
@@ -436,8 +436,8 @@
   by (simp only: diff_conv_add_uminus minus_minus)
 
 lemma neg_equal_iff_equal [simp]:
-  "- a = - b \<longleftrightarrow> a = b" 
-proof 
+  "- a = - b \<longleftrightarrow> a = b"
+proof
   assume "- a = - b"
   hence "- (- a) = - (- b)" by simp
   thus "a = b" by simp
@@ -557,15 +557,15 @@
 end
 
 
-subsection \<open>(Partially) Ordered Groups\<close> 
+subsection \<open>(Partially) Ordered Groups\<close>
 
 text \<open>
   The theory of partially ordered groups is taken from the books:
   \begin{itemize}
-  \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 
+  \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979
   \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
   \end{itemize}
-  Most of the used notions can also be looked up in 
+  Most of the used notions can also be looked up in
   \begin{itemize}
   \item @{url "http://www.mathworld.com"} by Eric Weisstein et. al.
   \item \emph{Algebra I} by van der Waerden, Springer.
@@ -617,7 +617,7 @@
 lemma add_le_less_mono:
   "a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
 apply (erule add_right_mono [THEN le_less_trans])
-apply (erule add_strict_left_mono) 
+apply (erule add_strict_left_mono)
 done
 
 end
@@ -631,7 +631,7 @@
   assumes less: "c + a < c + b" shows "a < b"
 proof -
   from less have le: "c + a <= c + b" by (simp add: order_le_less)
-  have "a <= b" 
+  have "a <= b"
     apply (insert le)
     apply (drule add_le_imp_le_left)
     by (insert le, drule add_le_imp_le_left, assumption)
@@ -648,12 +648,12 @@
 lemma add_less_imp_less_right:
   "a + c < b + c \<Longrightarrow> a < b"
 apply (rule add_less_imp_less_left [of c])
-apply (simp add: add.commute)  
+apply (simp add: add.commute)
 done
 
 lemma add_less_cancel_left [simp]:
   "c + a < c + b \<longleftrightarrow> a < b"
-  by (blast intro: add_less_imp_less_left add_strict_left_mono) 
+  by (blast intro: add_less_imp_less_left add_strict_left_mono)
 
 lemma add_less_cancel_right [simp]:
   "a + c < b + c \<longleftrightarrow> a < b"
@@ -661,7 +661,7 @@
 
 lemma add_le_cancel_left [simp]:
   "c + a \<le> c + b \<longleftrightarrow> a \<le> b"
-  by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono) 
+  by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono)
 
 lemma add_le_cancel_right [simp]:
   "a + c \<le> b + c \<longleftrightarrow> a \<le> b"
@@ -689,10 +689,76 @@
 
 end
 
-class ordered_cancel_comm_monoid_diff = comm_monoid_diff + ordered_ab_semigroup_add_imp_le +
+subsection \<open>Support for reasoning about signs\<close>
+
+class ordered_comm_monoid_add = comm_monoid_add + ordered_ab_semigroup_add
+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
+
+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
+
+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
+
+lemma add_increasing:
+  "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"
+  by (insert add_mono [of 0 a b c], simp)
+
+lemma add_increasing2:
+  "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"
@@ -750,17 +816,36 @@
 
 end
 
+class ordered_cancel_comm_monoid_add =
+  ordered_comm_monoid_add + cancel_ab_semigroup_add
+begin
 
-subsection \<open>Support for reasoning about signs\<close>
+subclass ordered_cancel_ab_semigroup_add ..
 
-class ordered_comm_monoid_add =
-  ordered_cancel_ab_semigroup_add + comm_monoid_add
-begin
+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_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_pos_nonneg:
   assumes "0 < a" and "0 \<le> b" shows "0 < a + b"
 proof -
-  have "0 + 0 < a + b" 
+  have "0 + 0 < a + b"
     using assms by (rule add_less_le_mono)
   then show ?thesis by simp
 qed
@@ -772,79 +857,15 @@
 lemma add_nonneg_pos:
   assumes "0 \<le> a" and "0 < b" shows "0 < a + b"
 proof -
-  have "0 + 0 < a + b" 
+  have "0 + 0 < a + b"
     using assms by (rule add_le_less_mono)
   then show ?thesis by simp
 qed
 
-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
-
-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_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_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
-
 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
 
-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
-
-lemma add_increasing:
-  "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"
-  by (insert add_mono [of 0 a b c], simp)
-
-lemma add_increasing2:
-  "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"
-  by (simp add: add_increasing add.commute [of a])
-
 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)
@@ -855,8 +876,7 @@
 
 end
 
-class ordered_ab_group_add =
-  ab_group_add + ordered_ab_semigroup_add
+class ordered_ab_group_add = ab_group_add + ordered_ab_semigroup_add
 begin
 
 subclass ordered_cancel_ab_semigroup_add ..
@@ -870,7 +890,7 @@
   thus "a \<le> b" by simp
 qed
 
-subclass ordered_comm_monoid_add ..
+subclass ordered_cancel_comm_monoid_add ..
 
 lemma add_less_same_cancel1 [simp]:
   "b + a < b \<longleftrightarrow> a < 0"
@@ -915,14 +935,14 @@
 lemma le_imp_neg_le:
   assumes "a \<le> b" shows "-b \<le> -a"
 proof -
-  have "-a+a \<le> -a+b" using \<open>a \<le> b\<close> by (rule add_left_mono) 
+  have "-a+a \<le> -a+b" using \<open>a \<le> b\<close> by (rule add_left_mono)
   then have "0 \<le> -a+b" by simp
-  then have "0 + (-b) \<le> (-a + b) + (-b)" by (rule add_right_mono) 
+  then have "0 + (-b) \<le> (-a + b) + (-b)" by (rule add_right_mono)
   then show ?thesis by (simp add: algebra_simps)
 qed
 
 lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b"
-proof 
+proof
   assume "- b \<le> - a"
   hence "- (- a) \<le> - (- b)" by (rule le_imp_neg_le)
   thus "a\<le>b" by simp
@@ -938,7 +958,7 @@
 by (subst neg_le_iff_le [symmetric], simp)
 
 lemma neg_less_iff_less [simp]: "- b < - a \<longleftrightarrow> a < b"
-by (force simp add: less_le) 
+by (force simp add: less_le)
 
 lemma neg_less_0_iff_less [simp]: "- a < 0 \<longleftrightarrow> 0 < a"
 by (subst neg_less_iff_less [symmetric], simp)
@@ -963,7 +983,7 @@
 lemma le_minus_iff: "a \<le> - b \<longleftrightarrow> b \<le> - a"
 proof -
   have mm: "!! a (b::'a). (-(-a)) < -b \<Longrightarrow> -(-b) < -a" by (simp only: minus_less_iff)
-  have "(- (- a) <= -b) = (b <= - a)" 
+  have "(- (- a) <= -b) = (b <= - a)"
     apply (auto simp only: le_less)
     apply (drule mm)
     apply (simp_all)
@@ -1078,18 +1098,18 @@
 subclass ordered_ab_semigroup_add_imp_le
 proof
   fix a b c :: 'a
-  assume le: "c + a <= c + b"  
+  assume le: "c + a <= c + b"
   show "a <= b"
   proof (rule ccontr)
     assume w: "~ a \<le> b"
     hence "b <= a" by (simp add: linorder_not_le)
     hence le2: "c + b <= c + a" by (rule add_left_mono)
-    have "a = b" 
+    have "a = b"
       apply (insert le)
       apply (insert le2)
       apply (drule antisym, simp_all)
       done
-    with w show False 
+    with w show False
       by (simp add: linorder_not_le [symmetric])
   qed
 qed
@@ -1192,7 +1212,7 @@
 qed
 
 lemma double_add_le_zero_iff_single_add_le_zero [simp]:
-  "a + a \<le> 0 \<longleftrightarrow> a \<le> 0" 
+  "a + a \<le> 0 \<longleftrightarrow> a \<le> 0"
 proof -
   have "\<not> a + a \<le> 0 \<longleftrightarrow> \<not> a \<le> 0"
     by (simp add: not_le)
@@ -1272,7 +1292,7 @@
   thus ?thesis by simp
 qed
 
-lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0" 
+lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0"
 proof
   assume "\<bar>a\<bar> \<le> 0"
   then have "\<bar>a\<bar> = 0" by (rule antisym) simp
@@ -1297,7 +1317,7 @@
   then show ?thesis by simp
 qed
 
-lemma abs_minus_commute: 
+lemma abs_minus_commute:
   "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
 proof -
   have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" by (simp only: abs_minus_cancel)
@@ -1318,7 +1338,7 @@
   unfolding minus_minus by (erule abs_of_nonneg)
   then show ?thesis using assms by auto
 qed
-  
+
 lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"
 by (rule abs_of_nonpos, rule less_imp_le)
 
diff -r 670063003ad3 -r 85f38d5f8807 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Tue Feb 09 09:21:10 2016 +0100
+++ b/src/HOL/Groups_Big.thy	Wed Feb 10 18:43:19 2016 +0100
@@ -111,7 +111,7 @@
 lemma setdiff_irrelevant:
   assumes "finite A"
   shows "F g (A - {x. g x = z}) = F g A"
-  using assms by (induct A) (simp_all add: insert_Diff_if) 
+  using assms by (induct A) (simp_all add: insert_Diff_if)
 
 lemma not_neutral_contains_not_neutral:
   assumes "F g A \<noteq> z"
@@ -196,9 +196,9 @@
 apply (simp add: comp_def)
 done
 
-lemma related: 
-  assumes Re: "R 1 1" 
-  and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 * y1) (x2 * y2)" 
+lemma related:
+  assumes Re: "R 1 1"
+  and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 * y1) (x2 * y2)"
   and fS: "finite S" and Rfg: "\<forall>x\<in>S. R (h x) (g x)"
   shows "R (F h S) (F g S)"
   using fS by (rule finite_subset_induct) (insert assms, auto)
@@ -305,7 +305,7 @@
     by (intro reindex_bij_betw_not_neutral[OF _ _ bij]) auto
 qed
 
-lemma delta: 
+lemma delta:
   assumes fS: "finite S"
   shows "F (\<lambda>k. if k = a then b k else 1) S = (if a \<in> S then b a else 1)"
 proof-
@@ -317,9 +317,9 @@
   { assume a: "a \<in> S"
     let ?A = "S - {a}"
     let ?B = "{a}"
-    have eq: "S = ?A \<union> ?B" using a by blast 
+    have eq: "S = ?A \<union> ?B" using a by blast
     have dj: "?A \<inter> ?B = {}" by simp
-    from fS have fAB: "finite ?A" "finite ?B" by auto  
+    from fS have fAB: "finite ?A" "finite ?B" by auto
     have "F ?f S = F ?f ?A * F ?f ?B"
       using union_disjoint [OF fAB dj, of ?f, unfolded eq [symmetric]]
       by simp
@@ -327,7 +327,7 @@
   ultimately show ?thesis by blast
 qed
 
-lemma delta': 
+lemma delta':
   assumes fS: "finite S"
   shows "F (\<lambda>k. if a = k then b k else 1) S = (if a \<in> S then b a else 1)"
   using delta [OF fS, of a b, symmetric] by (auto intro: cong)
@@ -338,10 +338,10 @@
   shows "F (\<lambda>x. if P x then h x else g x) A =
     F h (A \<inter> {x. P x}) * F g (A \<inter> - {x. P x})"
 proof -
-  have a: "A = A \<inter> {x. P x} \<union> A \<inter> -{x. P x}" 
-          "(A \<inter> {x. P x}) \<inter> (A \<inter> -{x. P x}) = {}" 
+  have a: "A = A \<inter> {x. P x} \<union> A \<inter> -{x. P x}"
+          "(A \<inter> {x. P x}) \<inter> (A \<inter> -{x. P x}) = {}"
     by blast+
-  from fA 
+  from fA
   have f: "finite (A \<inter> {x. P x})" "finite (A \<inter> -{x. P x})" by auto
   let ?g = "\<lambda>x. if P x then h x else g x"
   from union_disjoint [OF f a(2), of ?g] a(1)
@@ -352,8 +352,8 @@
 lemma cartesian_product:
    "F (\<lambda>x. F (g x) B) A = F (case_prod g) (A \<times> B)"
 apply (rule sym)
-apply (cases "finite A") 
- apply (cases "finite B") 
+apply (cases "finite A")
+ apply (cases "finite B")
   apply (simp add: Sigma)
  apply (cases "A={}", simp)
  apply simp
@@ -512,7 +512,7 @@
 
 text \<open>TODO generalization candidates\<close>
 
-lemma setsum_image_gen:
+lemma (in comm_monoid_add) setsum_image_gen:
   assumes fS: "finite S"
   shows "setsum g S = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)"
 proof-
@@ -557,13 +557,13 @@
     thus ?case by auto
   next
     case (insert x F)
-    thus ?case using le finiteB 
+    thus ?case using le finiteB
       by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
   qed
 qed
 
-lemma setsum_mono:
-  assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, ordered_ab_semigroup_add}))"
+lemma (in ordered_comm_monoid_add) setsum_mono:
+  assumes le: "\<And>i. i\<in>K \<Longrightarrow> f i \<le> g i"
   shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
 proof (cases "finite K")
   case True
@@ -579,10 +579,8 @@
   case False then show ?thesis by simp
 qed
 
-lemma setsum_strict_mono:
-  fixes f :: "'a \<Rightarrow> 'b::{ordered_cancel_ab_semigroup_add,comm_monoid_add}"
-  assumes "finite A"  "A \<noteq> {}"
-    and "!!x. x:A \<Longrightarrow> f x < g x"
+lemma (in ordered_cancel_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
 proof (induct rule: finite_ne_induct)
@@ -592,9 +590,9 @@
 qed
 
 lemma setsum_strict_mono_ex1:
-fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add, ordered_cancel_ab_semigroup_add}"
-assumes "finite A" and "ALL x:A. f x \<le> g x" and "EX a:A. f a < g a"
-shows "setsum f A < setsum g A"
+  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"
+  shows "setsum f A < setsum g A"
 proof-
   from assms(3) obtain a where a: "a:A" "f a < g a" by blast
   have "setsum f A = setsum f ((A-{a}) \<union> {a})"
@@ -624,8 +622,8 @@
   "(\<And>x. x \<in> A \<Longrightarrow> g x \<le> f x) \<Longrightarrow> (\<Sum>x\<in>A. f x - g x::nat) = (\<Sum>x\<in>A. f x) - (\<Sum>x\<in>A. g x)"
   by (induction A rule: infinite_finite_induct) (auto simp: setsum_mono)
 
-lemma setsum_nonneg:
-  assumes nn: "\<forall>x\<in>A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
+lemma (in ordered_comm_monoid_add) setsum_nonneg:
+  assumes nn: "\<forall>x\<in>A. 0 \<le> f x"
   shows "0 \<le> setsum f A"
 proof (cases "finite A")
   case True thus ?thesis using nn
@@ -640,8 +638,8 @@
   case False thus ?thesis by simp
 qed
 
-lemma setsum_nonpos:
-  assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{ordered_ab_semigroup_add,comm_monoid_add})"
+lemma (in ordered_comm_monoid_add) setsum_nonpos:
+  assumes np: "\<forall>x\<in>A. f x \<le> 0"
   shows "setsum f A \<le> 0"
 proof (cases "finite A")
   case True thus ?thesis using np
@@ -656,30 +654,28 @@
   case False thus ?thesis by simp
 qed
 
-lemma setsum_nonneg_leq_bound:
-  fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
+lemma (in ordered_comm_monoid_add) setsum_nonneg_eq_0_iff:
+  "finite A \<Longrightarrow> \<forall>x\<in>A. 0 \<le> f x \<Longrightarrow> setsum f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
+  by (induct set: finite, simp) (simp add: add_nonneg_eq_0_iff setsum_nonneg)
+
+lemma (in ordered_comm_monoid_add) setsum_nonneg_0:
+  "finite s \<Longrightarrow> (\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0) \<Longrightarrow> (\<Sum> i \<in> s. f i) = 0 \<Longrightarrow> i \<in> s \<Longrightarrow> f i = 0"
+  by (simp add: setsum_nonneg_eq_0_iff)
+
+lemma (in ordered_comm_monoid_add) setsum_nonneg_leq_bound:
   assumes "finite s" "\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0" "(\<Sum>i \<in> s. f i) = B" "i \<in> s"
   shows "f i \<le> B"
 proof -
-  have "0 \<le> (\<Sum> i \<in> s - {i}. f i)" and "0 \<le> f i"
-    using assms by (auto intro!: setsum_nonneg)
-  moreover
-  have "(\<Sum> i \<in> s - {i}. f i) + f i = B"
-    using assms by (simp add: setsum_diff1)
-  ultimately show ?thesis by auto
+  have "f i \<le> f i + (\<Sum>i \<in> s - {i}. f i)"
+    using assms by (intro add_increasing2 setsum_nonneg) auto
+  also have "\<dots> = B"
+    using setsum.remove[of s i f] assms by simp
+  finally show ?thesis by auto
 qed
 
-lemma setsum_nonneg_0:
-  fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
-  assumes "finite s" and pos: "\<And> i. i \<in> s \<Longrightarrow> f i \<ge> 0"
-  and "(\<Sum> i \<in> s. f i) = 0" and i: "i \<in> s"
-  shows "f i = 0"
-  using setsum_nonneg_leq_bound[OF assms] pos[OF i] by auto
-
-lemma setsum_mono2:
-fixes f :: "'a \<Rightarrow> 'b :: ordered_comm_monoid_add"
-assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
-shows "setsum f A \<le> setsum f B"
+lemma (in ordered_comm_monoid_add) setsum_mono2:
+  assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
+  shows "setsum f A \<le> setsum f B"
 proof -
   have "setsum f A \<le> setsum f A + setsum f (B-A)"
     by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
@@ -689,8 +685,7 @@
   finally show ?thesis .
 qed
 
-lemma setsum_le_included:
-  fixes f :: "'a \<Rightarrow> 'b::ordered_comm_monoid_add"
+lemma (in ordered_comm_monoid_add) setsum_le_included:
   assumes "finite s" "finite t"
   and "\<forall>y\<in>t. 0 \<le> g y" "(\<forall>x\<in>s. \<exists>y\<in>t. i y = x \<and> f x \<le> g y)"
   shows "setsum f s \<le> setsum g t"
@@ -710,25 +705,15 @@
   finally show ?thesis .
 qed
 
-lemma setsum_mono3: "finite B ==> A <= B ==> 
-    ALL x: B - A. 
-      0 <= ((f x)::'a::{comm_monoid_add,ordered_ab_semigroup_add}) ==>
-        setsum f A <= setsum f B"
-  apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
-  apply (erule ssubst)
-  apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
-  apply simp
-  apply (rule add_left_mono)
-  apply (erule setsum_nonneg)
-  apply (subst setsum.union_disjoint [THEN sym])
-  apply (erule finite_subset, assumption)
-  apply (rule finite_subset)
-  prefer 2
-  apply assumption
-  apply (auto simp add: sup_absorb2)
-done
+lemma (in ordered_comm_monoid_add) setsum_mono3:
+  "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> \<forall>x\<in>B - A. 0 \<le> f x \<Longrightarrow> setsum f A \<le> setsum f B"
+  by (rule setsum_mono2) auto
 
-lemma setsum_right_distrib: 
+lemma (in canonically_ordered_monoid_add) setsum_eq_0_iff [simp]:
+  "finite F \<Longrightarrow> (setsum f F = 0) = (\<forall>a\<in>F. f a = 0)"
+  by (intro ballI setsum_nonneg_eq_0_iff zero_le)
+
+lemma setsum_right_distrib:
   fixes f :: "'a => ('b::semiring_0)"
   shows "r * setsum f A = setsum (%n. r * f n) A"
 proof (cases "finite A")
@@ -771,7 +756,7 @@
   case False thus ?thesis by simp
 qed
 
-lemma setsum_abs[iff]: 
+lemma setsum_abs[iff]:
   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   shows "\<bar>setsum f A\<bar> \<le> setsum (%i. \<bar>f i\<bar>) A"
 proof (cases "finite A")
@@ -792,7 +777,7 @@
   shows "0 \<le> setsum (%i. \<bar>f i\<bar>) A"
   by (simp add: setsum_nonneg)
 
-lemma abs_setsum_abs[simp]: 
+lemma abs_setsum_abs[simp]:
   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   shows "\<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar> = (\<Sum>a\<in>A. \<bar>f a\<bar>)"
 proof (cases "finite A")
@@ -836,10 +821,6 @@
 apply (erule finite_induct, auto)
 done
 
-lemma setsum_eq_0_iff [simp]:
-  "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
-  by (induct set: finite) auto
-
 lemma setsum_eq_Suc0_iff: "finite A \<Longrightarrow>
   setsum f A = Suc 0 \<longleftrightarrow> (EX a:A. f a = Suc 0 & (ALL b:A. a\<noteq>b \<longrightarrow> f b = 0))"
 apply(erule finite_induct)
@@ -862,7 +843,7 @@
 apply (drule_tac a = a in mk_disjoint_insert, auto)
 done
 
-lemma setsum_diff_nat: 
+lemma setsum_diff_nat:
 assumes "finite B" and "B \<subseteq> A"
 shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
 using assms
@@ -945,11 +926,11 @@
 done
 
 lemma setsum_Suc: "setsum (\<lambda>x. Suc(f x)) A = setsum f A + card A"
-  using setsum.distrib[of f "\<lambda>_. 1" A] 
+  using setsum.distrib[of f "\<lambda>_. 1" A]
   by simp
 
 lemma setsum_bounded_above:
-  assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"
+  assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_comm_monoid_add})"
   shows "setsum f A \<le> of_nat (card A) * K"
 proof (cases "finite A")
   case True
@@ -959,14 +940,14 @@
 qed
 
 lemma setsum_bounded_above_strict:
-  assumes "\<And>i. i\<in>A \<Longrightarrow> f i < (K::'a::{ordered_cancel_ab_semigroup_add,semiring_1})"
+  assumes "\<And>i. i\<in>A \<Longrightarrow> f i < (K::'a::{ordered_cancel_comm_monoid_add,semiring_1})"
           "card A > 0"
   shows "setsum f A < of_nat (card A) * K"
 using assms setsum_strict_mono[where A=A and g = "%x. K"]
 by (simp add: card_gt_0_iff)
 
 lemma setsum_bounded_below:
-  assumes le: "\<And>i. i\<in>A \<Longrightarrow> (K::'a::{semiring_1, ordered_ab_semigroup_add}) \<le> f i"
+  assumes le: "\<And>i. i\<in>A \<Longrightarrow> (K::'a::{semiring_1, ordered_comm_monoid_add}) \<le> f i"
   shows "of_nat (card A) * K \<le> setsum f A"
 proof (cases "finite A")
   case True
@@ -1011,7 +992,7 @@
   finally show ?thesis by auto
 qed
 
-lemma (in ordered_comm_monoid_add) setsum_pos: 
+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)
 
@@ -1057,7 +1038,7 @@
 syntax
   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(2\<Prod>_\<in>_./ _)" [0, 51, 10] 10)
 translations \<comment> \<open>Beware of argument permutation!\<close>
-  "\<Prod>i\<in>A. b" == "CONST setprod (\<lambda>i. b) A" 
+  "\<Prod>i\<in>A. b" == "CONST setprod (\<lambda>i. b) A"
 
 text \<open>Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter \<open>\<Prod>x|P. e\<close>.\<close>
 
@@ -1071,7 +1052,7 @@
 context comm_monoid_mult
 begin
 
-lemma setprod_dvd_setprod: 
+lemma setprod_dvd_setprod:
   "(\<And>a. a \<in> A \<Longrightarrow> f a dvd g a) \<Longrightarrow> setprod f A dvd setprod g A"
 proof (induct A rule: infinite_finite_induct)
   case infinite then show ?case by (auto intro: dvdI)
@@ -1167,7 +1148,7 @@
   qed
 qed
 
-lemma (in field) setprod_inversef: 
+lemma (in field) setprod_inversef:
   "finite A \<Longrightarrow> setprod (inverse \<circ> f) A = inverse (setprod f A)"
   by (induct A rule: finite_induct) simp_all
 
@@ -1195,15 +1176,13 @@
   by (induct A rule: infinite_finite_induct) simp_all
 
 lemma (in linordered_semidom) setprod_mono:
-  assumes "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i"
-  shows "setprod f A \<le> setprod g A"
-  using assms by (induct A rule: infinite_finite_induct)
-    (auto intro!: setprod_nonneg mult_mono)
+  "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i \<Longrightarrow> setprod f A \<le> setprod g A"
+  by (induct A rule: infinite_finite_induct) (auto intro!: setprod_nonneg mult_mono)
 
 lemma (in linordered_semidom) setprod_mono_strict:
     assumes"finite A" "\<forall>i\<in>A. 0 \<le> f i \<and> f i < g i" "A \<noteq> {}"
     shows "setprod f A < setprod g A"
-using assms 
+using assms
 apply (induct A rule: finite_induct)
 apply (simp add: )
 apply (force intro: mult_strict_mono' setprod_nonneg)
@@ -1221,11 +1200,4 @@
   "finite A \<Longrightarrow> setprod f A > 0 \<longleftrightarrow> (\<forall>a\<in>A. f a > (0::nat))"
   using setprod_zero_iff by (simp del:neq0_conv add:neq0_conv [symmetric])
 
-lemma setsum_nonneg_eq_0_iff:
-  fixes f :: "'a \<Rightarrow> 'b::ordered_ab_group_add"
-  shows "\<lbrakk>finite A; \<forall>x\<in>A. 0 \<le> f x\<rbrakk> \<Longrightarrow> setsum f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
-  apply (induct set: finite, simp)
-  apply (simp add: add_nonneg_eq_0_iff setsum_nonneg)
-  done
-
 end
diff -r 670063003ad3 -r 85f38d5f8807 src/HOL/Library/Convex.thy
--- a/src/HOL/Library/Convex.thy	Tue Feb 09 09:21:10 2016 +0100
+++ b/src/HOL/Library/Convex.thy	Wed Feb 10 18:43:19 2016 +0100
@@ -565,7 +565,7 @@
     then have "(\<Sum> j \<in> s. a j) = 0"
       using insert by auto
     then have "\<And>j. j \<in> s \<Longrightarrow> a j = 0"
-      using setsum_nonneg_0[where 'b=real] insert by fastforce
+      using insert by (fastforce simp: setsum_nonneg_eq_0_iff)
     then show ?thesis
       using insert by auto
   next
diff -r 670063003ad3 -r 85f38d5f8807 src/HOL/Library/Extended_Nat.thy
--- a/src/HOL/Library/Extended_Nat.thy	Tue Feb 09 09:21:10 2016 +0100
+++ b/src/HOL/Library/Extended_Nat.thy	Wed Feb 10 18:43:19 2016 +0100
@@ -62,6 +62,9 @@
 lemma not_enat_eq [iff]: "(\<forall>y. x \<noteq> enat y) = (x = \<infinity>)"
   by (cases x) auto
 
+lemma enat_ex_split: "(\<exists>c::enat. P c) \<longleftrightarrow> P \<infinity> \<or> (\<exists>c::nat. P c)"
+  by (metis enat.exhaust)
+
 primrec the_enat :: "enat \<Rightarrow> nat"
   where "the_enat (enat n) = n"
 
@@ -359,11 +362,16 @@
 
 end
 
-instance enat :: ordered_comm_semiring
+instance enat :: dioid
+proof
+  fix a b :: enat show "(a \<le> b) = (\<exists>c. b = a + c)"
+    by (cases a b rule: enat2_cases) (auto simp: le_iff_add enat_ex_split)
+qed
+
+instance enat :: "ordered_comm_semiring"
 proof
   fix a b c :: enat
-  assume "a \<le> b" and "0 \<le> c"
-  thus "c * a \<le> c * b"
+  assume "a \<le> b" and "0 \<le> c" thus "c * a \<le> c * b"
     unfolding times_enat_def less_eq_enat_def zero_enat_def
     by (simp split: enat.splits)
 qed
diff -r 670063003ad3 -r 85f38d5f8807 src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Tue Feb 09 09:21:10 2016 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Wed Feb 10 18:43:19 2016 +0100
@@ -78,6 +78,13 @@
 lemma ennreal_zero_less_one: "0 < (1::ennreal)"
   by transfer auto
 
+instance ennreal :: dioid
+proof (standard; transfer)
+  fix a b :: ereal assume "0 \<le> a" "0 \<le> b" then show "(a \<le> b) = (\<exists>c\<in>Collect (op \<le> 0). b = a + c)"
+    unfolding ereal_ex_split Bex_def
+    by (cases a b rule: ereal2_cases) (auto intro!: exI[of _ "real_of_ereal (b - a)"])
+qed
+
 instance ennreal :: ordered_comm_semiring
   by standard
      (transfer ; auto intro: add_mono mult_mono mult_ac ereal_left_distrib ereal_mult_left_mono)+
diff -r 670063003ad3 -r 85f38d5f8807 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Tue Feb 09 09:21:10 2016 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Wed Feb 10 18:43:19 2016 +0100
@@ -19,6 +19,26 @@
 
 \<close>
 
+lemma image_eqD: "f ` A = B \<Longrightarrow> \<forall>x\<in>A. f x \<in> B"
+  by auto
+
+lemma incseq_setsumI2:
+  fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::ordered_comm_monoid_add"
+  shows "(\<And>n. n \<in> A \<Longrightarrow> mono (f n)) \<Longrightarrow> mono (\<lambda>i. \<Sum>n\<in>A. f n i)"
+  unfolding incseq_def by (auto intro: setsum_mono)
+
+lemma incseq_setsumI:
+  fixes f :: "nat \<Rightarrow> 'a::ordered_comm_monoid_add"
+  assumes "\<And>i. 0 \<le> f i"
+  shows "incseq (\<lambda>i. setsum f {..< i})"
+proof (intro incseq_SucI)
+  fix n
+  have "setsum f {..< n} + 0 \<le> setsum f {..<n} + f n"
+    using assms by (rule add_left_mono)
+  then show "setsum f {..< n} \<le> setsum f {..< Suc n}"
+    by auto
+qed
+
 lemma continuous_at_left_imp_sup_continuous:
   fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology}"
   assumes "mono f" "\<And>x. continuous (at_left x) f"
@@ -535,7 +555,7 @@
 instance ereal :: dense_linorder
   by standard (blast dest: ereal_dense2)
 
-instance ereal :: ordered_ab_semigroup_add
+instance ereal :: ordered_comm_monoid_add
 proof
   fix a b c :: ereal
   assume "a \<le> b"
@@ -742,28 +762,6 @@
   shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a + b"
   using add_mono[of 0 a 0 b] by simp
 
-lemma image_eqD: "f ` A = B \<Longrightarrow> \<forall>x\<in>A. f x \<in> B"
-  by auto
-
-lemma incseq_setsumI:
-  fixes f :: "nat \<Rightarrow> 'a::{comm_monoid_add,ordered_ab_semigroup_add}"
-  assumes "\<And>i. 0 \<le> f i"
-  shows "incseq (\<lambda>i. setsum f {..< i})"
-proof (intro incseq_SucI)
-  fix n
-  have "setsum f {..< n} + 0 \<le> setsum f {..<n} + f n"
-    using assms by (rule add_left_mono)
-  then show "setsum f {..< n} \<le> setsum f {..< Suc n}"
-    by auto
-qed
-
-lemma incseq_setsumI2:
-  fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::{comm_monoid_add,ordered_ab_semigroup_add}"
-  assumes "\<And>n. n \<in> A \<Longrightarrow> incseq (f n)"
-  shows "incseq (\<lambda>i. \<Sum>n\<in>A. f n i)"
-  using assms
-  unfolding incseq_def by (auto intro: setsum_mono)
-
 lemma setsum_ereal[simp]: "(\<Sum>x\<in>A. ereal (f x)) = ereal (\<Sum>x\<in>A. f x)"
 proof (cases "finite A")
   case True
diff -r 670063003ad3 -r 85f38d5f8807 src/HOL/Library/Function_Algebras.thy
--- a/src/HOL/Library/Function_Algebras.thy	Tue Feb 09 09:21:10 2016 +0100
+++ b/src/HOL/Library/Function_Algebras.thy	Wed Feb 10 18:43:19 2016 +0100
@@ -153,7 +153,7 @@
 
 instance "fun" :: (type, semiring_1_cancel) semiring_1_cancel ..
 
-instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel 
+instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel
   by standard (auto simp add: times_fun_def algebra_simps)
 
 instance "fun" :: (type, semiring_char_0) semiring_char_0
@@ -188,11 +188,21 @@
 
 instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add ..
 
+instance "fun" :: (type, ordered_cancel_comm_monoid_add) ordered_cancel_comm_monoid_add ..
+
 instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
 
 instance "fun" :: (type, ordered_semiring) ordered_semiring
   by standard (auto simp add: le_fun_def intro: mult_left_mono mult_right_mono)
 
+instance "fun" :: (type, dioid) dioid
+proof standard
+  fix a b :: "'a \<Rightarrow> 'b"
+  show "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)"
+    unfolding le_fun_def plus_fun_def fun_eq_iff choice_iff[symmetric, of "\<lambda>x c. b x = a x + c"]
+    by (intro arg_cong[where f=All] ext canonically_ordered_monoid_add_class.le_iff_add)
+qed
+
 instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring
   by standard (fact mult_left_mono)
 
diff -r 670063003ad3 -r 85f38d5f8807 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Feb 09 09:21:10 2016 +0100
+++ b/src/HOL/Library/Multiset.thy	Wed Feb 10 18:43:19 2016 +0100
@@ -302,7 +302,7 @@
    apply (auto intro: multiset_eq_iff [THEN iffD2])
   done
 
-interpretation subset_mset: ordered_cancel_comm_monoid_diff  "op +" "op -" 0 "op \<le>#" "op <#"
+interpretation subset_mset: ordered_cancel_comm_monoid_diff  "op +" 0 "op \<le>#" "op <#" "op -"
   by standard (simp, fact mset_le_exists_conv)
 
 lemma mset_le_mono_add_right_cancel [simp]: "(A::'a multiset) + C \<le># B + C \<longleftrightarrow> A \<le># B"
diff -r 670063003ad3 -r 85f38d5f8807 src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy	Tue Feb 09 09:21:10 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy	Wed Feb 10 18:43:19 2016 +0100
@@ -65,7 +65,7 @@
   shows "a\<bullet>i \<le> x\<bullet>i" "x\<bullet>i \<le> b\<bullet>i"
   using assms
   unfolding euclidean_inner[of a i] euclidean_inner[of x i] euclidean_inner[of b i]
-  by (auto intro!: setsum_mono mult_right_mono simp: eucl_le)
+  by (auto intro!: ordered_comm_monoid_add_class.setsum_mono mult_right_mono simp: eucl_le)
 
 lemma inner_nonneg_nonneg:
   shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a \<bullet> b"
diff -r 670063003ad3 -r 85f38d5f8807 src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Tue Feb 09 09:21:10 2016 +0100
+++ b/src/HOL/NSA/StarDef.thy	Wed Feb 10 18:43:19 2016 +0100
@@ -140,7 +140,7 @@
 done
 
 lemma transfer_fun_eq [transfer_intro]:
-  "\<lbrakk>\<And>X. f (star_n X) = g (star_n X) 
+  "\<lbrakk>\<And>X. f (star_n X) = g (star_n X)
     \<equiv> eventually (\<lambda>n. F n (X n) = G n (X n)) \<U>\<rbrakk>
       \<Longrightarrow> f = g \<equiv> eventually (\<lambda>n. F n = G n) \<U>"
 by (simp only: fun_eq_iff transfer_all)
@@ -806,9 +806,10 @@
 by (intro_classes, transfer, rule add_le_imp_le_left)
 
 instance star :: (ordered_comm_monoid_add) ordered_comm_monoid_add ..
+instance star :: (ordered_cancel_comm_monoid_add) ordered_cancel_comm_monoid_add ..
 instance star :: (ordered_ab_group_add) ordered_ab_group_add ..
 
-instance star :: (ordered_ab_group_add_abs) ordered_ab_group_add_abs 
+instance star :: (ordered_ab_group_add_abs) ordered_ab_group_add_abs
   by intro_classes (transfer,
     simp add: abs_ge_self abs_leI abs_triangle_ineq)+
 
@@ -820,12 +821,12 @@
 instance star :: (semiring) semiring
   by (intro_classes; transfer) (fact distrib_right distrib_left)+
 
-instance star :: (semiring_0) semiring_0 
+instance star :: (semiring_0) semiring_0
   by (intro_classes; transfer) simp_all
 
 instance star :: (semiring_0_cancel) semiring_0_cancel ..
 
-instance star :: (comm_semiring) comm_semiring 
+instance star :: (comm_semiring) comm_semiring
   by (intro_classes; transfer) (fact distrib_right)
 
 instance star :: (comm_semiring_0) comm_semiring_0 ..
@@ -846,7 +847,7 @@
   by (intro_classes; transfer) (fact no_zero_divisors)
 
 instance star :: (semiring_1_no_zero_divisors) semiring_1_no_zero_divisors ..
-  
+
 instance star :: (semiring_no_zero_divisors_cancel) semiring_no_zero_divisors_cancel
   by (intro_classes; transfer) simp_all
 
@@ -865,7 +866,7 @@
 
 instance star :: (ring_no_zero_divisors) ring_no_zero_divisors ..
 instance star :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors ..
-instance star :: (idom) idom .. 
+instance star :: (idom) idom ..
 instance star :: (idom_divide) idom_divide ..
 
 instance star :: (division_ring) division_ring
@@ -919,7 +920,7 @@
   "(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x"
 proof (rule eq_reflection, rule ext, rule ext)
   fix n :: nat
-  show "\<And>x::'a star. x ^ n = ( *f* (\<lambda>x. x ^ n)) x" 
+  show "\<And>x::'a star. x ^ n = ( *f* (\<lambda>x. x ^ n)) x"
   proof (induct n)
     case 0
     have "\<And>x::'a star. ( *f* (\<lambda>x. 1)) x = 1"
diff -r 670063003ad3 -r 85f38d5f8807 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Feb 09 09:21:10 2016 +0100
+++ b/src/HOL/Nat.thy	Wed Feb 10 18:43:19 2016 +0100
@@ -735,8 +735,11 @@
 lemma add_diff_inverse_nat: "~  m < n ==> n + (m - n) = (m::nat)"
 by (induct m n rule: diff_induct) simp_all
 
-
-text\<open>The naturals form an ordered \<open>semidom\<close>\<close>
+lemma nat_le_iff_add: "(m::nat) \<le> n = (\<exists>k. n = m + k)"
+using nat_add_left_cancel_le[of m 0] by (auto dest: le_Suc_ex)
+
+text\<open>The naturals form an ordered \<open>semidom\<close> and a \<open>dioid\<close>\<close>
+
 instance nat :: linordered_semidom
 proof
   show "0 < (1::nat)" by simp
@@ -745,8 +748,16 @@
   show "\<And>m n :: nat. m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m * n \<noteq> 0" by simp
   show "\<And>m n :: nat. n \<le> m ==> (m - n) + n = (m::nat)"
     by (simp add: add_diff_inverse_nat add.commute linorder_not_less)
-qed 
-
+qed
+
+instance nat :: dioid
+  proof qed (rule nat_le_iff_add)
+
+instance nat :: ordered_cancel_comm_monoid_add
+  proof qed
+
+instance nat :: ordered_cancel_comm_monoid_diff
+  proof qed
 
 subsubsection \<open>@{term min} and @{term max}\<close>
 
@@ -1079,14 +1090,6 @@
 lemma diff_le_self [simp]: "m - n \<le> (m::nat)"
 by (induct m n rule: diff_induct) (simp_all add: le_SucI)
 
-lemma le_iff_add: "(m::nat) \<le> n = (\<exists>k. n = m + k)"
-  by (auto simp: le_add1 dest!: le_add_diff_inverse sym [of _ n])
-
-instance nat :: ordered_cancel_comm_monoid_diff
-proof
-  show "\<And>m n :: nat. m \<le> n \<longleftrightarrow> (\<exists>q. n = m + q)" by (fact le_iff_add)
-qed
-
 lemma less_imp_diff_less: "(j::nat) < k ==> j - n < k"
 by (rule le_less_trans, rule diff_le_self)
 
@@ -1488,7 +1491,7 @@
   by (simp add: not_less)
 
 lemma of_nat_less_iff [simp]: "of_nat m < of_nat n \<longleftrightarrow> m < n"
-  by (induct m n rule: diff_induct, simp_all add: add_pos_nonneg)
+  by (induct m n rule: diff_induct) (simp_all add: add_pos_nonneg)
 
 lemma of_nat_le_iff [simp]: "of_nat m \<le> of_nat n \<longleftrightarrow> m \<le> n"
   by (simp add: not_less [symmetric] linorder_not_less [symmetric])
diff -r 670063003ad3 -r 85f38d5f8807 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Tue Feb 09 09:21:10 2016 +0100
+++ b/src/HOL/Rings.thy	Wed Feb 10 18:43:19 2016 +0100
@@ -635,7 +635,7 @@
   case False then have "a * 0 div a = 0"
     by (rule nonzero_mult_divide_cancel_left)
   then show ?thesis by simp
-qed 
+qed
 
 lemma divide_1 [simp]:
   "a div 1 = a"
@@ -663,16 +663,16 @@
   with assms have "c = b * d" by (simp add: ac_simps)
   then show ?Q ..
 next
-  assume ?Q then obtain d where "c = b * d" .. 
+  assume ?Q then obtain d where "c = b * d" ..
   then have "a * c = a * b * d" by (simp add: ac_simps)
   then show ?P ..
 qed
-  
+
 lemma dvd_times_right_cancel_iff [simp]:
   assumes "a \<noteq> 0"
   shows "b * a dvd c * a \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
 using dvd_times_left_cancel_iff [of a b c] assms by (simp add: ac_simps)
-  
+
 lemma div_dvd_iff_mult:
   assumes "b \<noteq> 0" and "b dvd a"
   shows "a div b dvd c \<longleftrightarrow> a dvd c * b"
@@ -991,7 +991,7 @@
     and unit_factor_0 [simp]: "unit_factor 0 = 0"
   assumes is_unit_normalize:
     "is_unit a  \<Longrightarrow> normalize a = 1"
-  assumes unit_factor_is_unit [iff]: 
+  assumes unit_factor_is_unit [iff]:
     "a \<noteq> 0 \<Longrightarrow> is_unit (unit_factor a)"
   assumes unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
 begin
@@ -1012,8 +1012,8 @@
 
 lemma unit_factor_self [simp]:
   "unit_factor a dvd a"
-  by (cases "a = 0") simp_all 
-  
+  by (cases "a = 0") simp_all
+
 lemma normalize_mult_unit_factor [simp]:
   "normalize a * unit_factor a = a"
   using unit_factor_mult_normalize [of a] by (simp add: ac_simps)
@@ -1023,7 +1023,7 @@
 proof
   assume ?P
   moreover have "unit_factor a * normalize a = a" by simp
-  ultimately show ?Q by simp 
+  ultimately show ?Q by simp
 next
   assume ?Q then show ?P by simp
 qed
@@ -1033,14 +1033,14 @@
 proof
   assume ?P
   moreover have "unit_factor a * normalize a = a" by simp
-  ultimately show ?Q by simp 
+  ultimately show ?Q by simp
 next
   assume ?Q then show ?P by simp
 qed
 
 lemma is_unit_unit_factor:
   assumes "is_unit a" shows "unit_factor a = a"
-proof - 
+proof -
   from assms have "normalize a = 1" by (rule is_unit_normalize)
   moreover from unit_factor_mult_normalize have "unit_factor a * normalize a = a" .
   ultimately show ?thesis by simp
@@ -1069,13 +1069,13 @@
     using \<open>a \<noteq> 0\<close> by simp
   ultimately show ?Q by simp
 qed
-  
+
 lemma div_normalize [simp]:
   "a div normalize a = unit_factor a"
 proof (cases "a = 0")
   case True then show ?thesis by simp
 next
-  case False then have "normalize a \<noteq> 0" by simp 
+  case False then have "normalize a \<noteq> 0" by simp
   with nonzero_mult_divide_cancel_right
   have "unit_factor a * normalize a div normalize a = unit_factor a" by blast
   then show ?thesis by simp
@@ -1086,7 +1086,7 @@
 proof (cases "a = 0")
   case True then show ?thesis by simp
 next
-  case False then have "unit_factor a \<noteq> 0" by simp 
+  case False then have "unit_factor a \<noteq> 0" by simp
   with nonzero_mult_divide_cancel_left
   have "unit_factor a * normalize a div unit_factor a = normalize a" by blast
   then show ?thesis by simp
@@ -1126,7 +1126,7 @@
     using False by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric])
   finally show ?thesis .
 qed
- 
+
 lemma unit_factor_idem [simp]:
   "unit_factor (unit_factor a) = unit_factor a"
   by (cases "a = 0") (auto intro: is_unit_unit_factor)
@@ -1134,7 +1134,7 @@
 lemma normalize_unit_factor [simp]:
   "a \<noteq> 0 \<Longrightarrow> normalize (unit_factor a) = 1"
   by (rule is_unit_normalize) simp
-  
+
 lemma normalize_idem [simp]:
   "normalize (normalize a) = normalize a"
 proof (cases "a = 0")
@@ -1257,7 +1257,7 @@
   proof (cases "a = 0 \<or> b = 0")
     case True with \<open>?P\<close> show ?thesis by auto
   next
-    case False 
+    case False
     then have "b dvd normalize b * unit_factor a" and "normalize b * unit_factor a dvd b"
       by (simp_all add: mult_unit_dvd_iff dvd_mult_unit_iff)
     with * show ?thesis by simp
@@ -1277,7 +1277,7 @@
 
 end
 
-class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +
+class ordered_semiring = semiring + ordered_comm_monoid_add +
   assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
 begin
@@ -1324,7 +1324,7 @@
 
 subclass ordered_cancel_semiring ..
 
-subclass ordered_comm_monoid_add ..
+subclass ordered_cancel_comm_monoid_add ..
 
 lemma mult_left_less_imp_less:
   "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
@@ -1742,14 +1742,14 @@
 lemma add_diff_inverse: "~ a<b \<Longrightarrow> b + (a - b) = a"
   by simp
 
-lemma add_le_imp_le_diff: 
+lemma add_le_imp_le_diff:
   shows "i + k \<le> n \<Longrightarrow> i \<le> n - k"
   apply (subst add_le_cancel_right [where c=k, symmetric])
   apply (frule le_add_diff_inverse2)
   apply (simp only: add.assoc [symmetric])
   using add_implies_diff by fastforce
 
-lemma add_le_add_imp_diff_le: 
+lemma add_le_add_imp_diff_le:
   assumes a1: "i + k \<le> n"
       and a2: "n \<le> j + k"
   shows "\<lbrakk>i + k \<le> n; n \<le> j + k\<rbrakk> \<Longrightarrow> n - k \<le> j"
@@ -2034,6 +2034,20 @@
 
 end
 
+subsection \<open>Dioids\<close>
+
+text \<open>Dioids are the alternative extensions of semirings, a semiring can either be a ring or a dioid
+but never both.\<close>
+
+class dioid = semiring_1 + canonically_ordered_monoid_add
+begin
+
+subclass ordered_semiring
+  proof qed (auto simp: le_iff_add distrib_left distrib_right)
+
+end
+
+
 hide_fact (open) comm_mult_left_mono comm_mult_strict_left_mono distrib
 
 code_identifier
diff -r 670063003ad3 -r 85f38d5f8807 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Tue Feb 09 09:21:10 2016 +0100
+++ b/src/HOL/Series.thy	Wed Feb 10 18:43:19 2016 +0100
@@ -211,22 +211,6 @@
 lemma suminf_nonneg: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 \<le> suminf f"
   using setsum_le_suminf[of 0] by simp
 
-lemma setsum_less_suminf2: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 \<le> f m \<Longrightarrow> n \<le> i \<Longrightarrow> 0 < f i \<Longrightarrow> setsum f {..<n} < suminf f"
-  using
-    setsum_le_suminf[of "Suc i"]
-    add_strict_increasing[of "f i" "setsum f {..<n}" "setsum f {..<i}"]
-    setsum_mono2[of "{..<i}" "{..<n}" f]
-  by (auto simp: less_imp_le ac_simps)
-
-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_le_const: "summable f \<Longrightarrow> (\<And>n. setsum f {..<n} \<le> x) \<Longrightarrow> suminf f \<le> x"
   by (metis LIMSEQ_le_const2 summable_LIMSEQ)
 
@@ -244,8 +228,31 @@
     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)
+end
+
+context
+  fixes f :: "nat \<Rightarrow> 'a::{ordered_cancel_comm_monoid_add, linorder_topology}"
+begin
+
+lemma setsum_less_suminf2: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 \<le> f m \<Longrightarrow> n \<le> i \<Longrightarrow> 0 < f i \<Longrightarrow> setsum f {..<n} < suminf f"
+  using
+    setsum_le_suminf[of f "Suc i"]
+    add_strict_increasing[of "f i" "setsum f {..<n}" "setsum f {..<i}"]
+    setsum_mono2[of "{..<i}" "{..<n}" f]
+  by (auto simp: less_imp_le ac_simps)
+
+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
 
diff -r 670063003ad3 -r 85f38d5f8807 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Tue Feb 09 09:21:10 2016 +0100
+++ b/src/HOL/Set_Interval.thy	Wed Feb 10 18:43:19 2016 +0100
@@ -1870,7 +1870,7 @@
 proof (cases "i \<le> j")
   case True
   then show ?thesis
-    by (metis Nat.le_iff_add setprod_int_plus_eq)
+    by (metis le_iff_add setprod_int_plus_eq)
 next
   case False
   then show ?thesis