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.
authorhoelzl
Wed Feb 10 18:43:19 2016 +0100 (2016-02-10)
changeset 6237685f38d5f8807
parent 62375 670063003ad3
child 62377 ace69956d018
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.
NEWS
src/HOL/Groups.thy
src/HOL/Groups_Big.thy
src/HOL/Library/Convex.thy
src/HOL/Library/Extended_Nat.thy
src/HOL/Library/Extended_Nonnegative_Real.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Function_Algebras.thy
src/HOL/Library/Multiset.thy
src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy
src/HOL/NSA/StarDef.thy
src/HOL/Nat.thy
src/HOL/Rings.thy
src/HOL/Series.thy
src/HOL/Set_Interval.thy
     1.1 --- a/NEWS	Tue Feb 09 09:21:10 2016 +0100
     1.2 +++ b/NEWS	Wed Feb 10 18:43:19 2016 +0100
     1.3 @@ -40,6 +40,15 @@
     1.4  
     1.5  * Class semiring_Lcd merged into semiring_Gcd.  INCOMPATIBILITY.
     1.6  
     1.7 +* The type class ordered_comm_monoid_add is now called
     1.8 +ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add is
     1.9 +introduced as the combination of ordered_ab_semigroup_add + comm_monoid_add.
    1.10 +INCOMPATIBILITY.
    1.11 +
    1.12 +* Introduced the type classes canonically_ordered_comm_monoid_add and dioid.
    1.13 +
    1.14 +* Added topological_monoid
    1.15 +
    1.16  * Library/Polynomial.thy contains also derivation of polynomials
    1.17  but not gcd/lcm on polynomials over fields.  This has been moved
    1.18  to a separate theory Library/Polynomial_GCD_euclidean.thy, to
    1.19 @@ -144,7 +153,6 @@
    1.20  * SML/NJ is no longer supported.
    1.21  
    1.22  
    1.23 -
    1.24  New in Isabelle2016 (February 2016)
    1.25  -----------------------------------
    1.26  
     2.1 --- a/src/HOL/Groups.thy	Tue Feb 09 09:21:10 2016 +0100
     2.2 +++ b/src/HOL/Groups.thy	Wed Feb 10 18:43:19 2016 +0100
     2.3 @@ -78,7 +78,7 @@
     2.4  
     2.5  subsection \<open>Generic operations\<close>
     2.6  
     2.7 -class zero = 
     2.8 +class zero =
     2.9    fixes zero :: 'a  ("0")
    2.10  
    2.11  class one =
    2.12 @@ -310,7 +310,7 @@
    2.13    then show "c = a - b" by simp
    2.14  qed
    2.15  
    2.16 -end  
    2.17 +end
    2.18  
    2.19  class comm_monoid_diff = cancel_comm_monoid_add +
    2.20    assumes zero_diff [simp]: "0 - a = 0"
    2.21 @@ -428,7 +428,7 @@
    2.22    by (simp only: diff_conv_add_uminus add_0_left)
    2.23  
    2.24  lemma diff_0_right [simp]:
    2.25 -  "a - 0 = a" 
    2.26 +  "a - 0 = a"
    2.27    by (simp only: diff_conv_add_uminus minus_zero add_0_right)
    2.28  
    2.29  lemma diff_minus_eq_add [simp]:
    2.30 @@ -436,8 +436,8 @@
    2.31    by (simp only: diff_conv_add_uminus minus_minus)
    2.32  
    2.33  lemma neg_equal_iff_equal [simp]:
    2.34 -  "- a = - b \<longleftrightarrow> a = b" 
    2.35 -proof 
    2.36 +  "- a = - b \<longleftrightarrow> a = b"
    2.37 +proof
    2.38    assume "- a = - b"
    2.39    hence "- (- a) = - (- b)" by simp
    2.40    thus "a = b" by simp
    2.41 @@ -557,15 +557,15 @@
    2.42  end
    2.43  
    2.44  
    2.45 -subsection \<open>(Partially) Ordered Groups\<close> 
    2.46 +subsection \<open>(Partially) Ordered Groups\<close>
    2.47  
    2.48  text \<open>
    2.49    The theory of partially ordered groups is taken from the books:
    2.50    \begin{itemize}
    2.51 -  \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 
    2.52 +  \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979
    2.53    \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
    2.54    \end{itemize}
    2.55 -  Most of the used notions can also be looked up in 
    2.56 +  Most of the used notions can also be looked up in
    2.57    \begin{itemize}
    2.58    \item @{url "http://www.mathworld.com"} by Eric Weisstein et. al.
    2.59    \item \emph{Algebra I} by van der Waerden, Springer.
    2.60 @@ -617,7 +617,7 @@
    2.61  lemma add_le_less_mono:
    2.62    "a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
    2.63  apply (erule add_right_mono [THEN le_less_trans])
    2.64 -apply (erule add_strict_left_mono) 
    2.65 +apply (erule add_strict_left_mono)
    2.66  done
    2.67  
    2.68  end
    2.69 @@ -631,7 +631,7 @@
    2.70    assumes less: "c + a < c + b" shows "a < b"
    2.71  proof -
    2.72    from less have le: "c + a <= c + b" by (simp add: order_le_less)
    2.73 -  have "a <= b" 
    2.74 +  have "a <= b"
    2.75      apply (insert le)
    2.76      apply (drule add_le_imp_le_left)
    2.77      by (insert le, drule add_le_imp_le_left, assumption)
    2.78 @@ -648,12 +648,12 @@
    2.79  lemma add_less_imp_less_right:
    2.80    "a + c < b + c \<Longrightarrow> a < b"
    2.81  apply (rule add_less_imp_less_left [of c])
    2.82 -apply (simp add: add.commute)  
    2.83 +apply (simp add: add.commute)
    2.84  done
    2.85  
    2.86  lemma add_less_cancel_left [simp]:
    2.87    "c + a < c + b \<longleftrightarrow> a < b"
    2.88 -  by (blast intro: add_less_imp_less_left add_strict_left_mono) 
    2.89 +  by (blast intro: add_less_imp_less_left add_strict_left_mono)
    2.90  
    2.91  lemma add_less_cancel_right [simp]:
    2.92    "a + c < b + c \<longleftrightarrow> a < b"
    2.93 @@ -661,7 +661,7 @@
    2.94  
    2.95  lemma add_le_cancel_left [simp]:
    2.96    "c + a \<le> c + b \<longleftrightarrow> a \<le> b"
    2.97 -  by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono) 
    2.98 +  by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono)
    2.99  
   2.100  lemma add_le_cancel_right [simp]:
   2.101    "a + c \<le> b + c \<longleftrightarrow> a \<le> b"
   2.102 @@ -689,10 +689,76 @@
   2.103  
   2.104  end
   2.105  
   2.106 -class ordered_cancel_comm_monoid_diff = comm_monoid_diff + ordered_ab_semigroup_add_imp_le +
   2.107 +subsection \<open>Support for reasoning about signs\<close>
   2.108 +
   2.109 +class ordered_comm_monoid_add = comm_monoid_add + ordered_ab_semigroup_add
   2.110 +begin
   2.111 +
   2.112 +lemma add_nonneg_nonneg [simp]:
   2.113 +  assumes "0 \<le> a" and "0 \<le> b" shows "0 \<le> a + b"
   2.114 +proof -
   2.115 +  have "0 + 0 \<le> a + b"
   2.116 +    using assms by (rule add_mono)
   2.117 +  then show ?thesis by simp
   2.118 +qed
   2.119 +
   2.120 +lemma add_nonpos_nonpos:
   2.121 +  assumes "a \<le> 0" and "b \<le> 0" shows "a + b \<le> 0"
   2.122 +proof -
   2.123 +  have "a + b \<le> 0 + 0"
   2.124 +    using assms by (rule add_mono)
   2.125 +  then show ?thesis by simp
   2.126 +qed
   2.127 +
   2.128 +lemma add_nonneg_eq_0_iff:
   2.129 +  assumes x: "0 \<le> x" and y: "0 \<le> y"
   2.130 +  shows "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   2.131 +proof (intro iffI conjI)
   2.132 +  have "x = x + 0" by simp
   2.133 +  also have "x + 0 \<le> x + y" using y by (rule add_left_mono)
   2.134 +  also assume "x + y = 0"
   2.135 +  also have "0 \<le> x" using x .
   2.136 +  finally show "x = 0" .
   2.137 +next
   2.138 +  have "y = 0 + y" by simp
   2.139 +  also have "0 + y \<le> x + y" using x by (rule add_right_mono)
   2.140 +  also assume "x + y = 0"
   2.141 +  also have "0 \<le> y" using y .
   2.142 +  finally show "y = 0" .
   2.143 +next
   2.144 +  assume "x = 0 \<and> y = 0"
   2.145 +  then show "x + y = 0" by simp
   2.146 +qed
   2.147 +
   2.148 +lemma add_increasing:
   2.149 +  "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"
   2.150 +  by (insert add_mono [of 0 a b c], simp)
   2.151 +
   2.152 +lemma add_increasing2:
   2.153 +  "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"
   2.154 +  by (simp add: add_increasing add.commute [of a])
   2.155 +
   2.156 +end
   2.157 +
   2.158 +class canonically_ordered_monoid_add = comm_monoid_add + order +
   2.159    assumes le_iff_add: "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)"
   2.160  begin
   2.161  
   2.162 +subclass ordered_comm_monoid_add
   2.163 +  proof qed (auto simp: le_iff_add add_ac)
   2.164 +
   2.165 +lemma zero_le: "0 \<le> x"
   2.166 +  by (auto simp: le_iff_add)
   2.167 +
   2.168 +lemma add_eq_0_iff_both_eq_0: "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   2.169 +  by (intro add_nonneg_eq_0_iff zero_le)
   2.170 +
   2.171 +end
   2.172 +
   2.173 +class ordered_cancel_comm_monoid_diff =
   2.174 +  canonically_ordered_monoid_add + comm_monoid_diff + ordered_ab_semigroup_add_imp_le
   2.175 +begin
   2.176 +
   2.177  context
   2.178    fixes a b
   2.179    assumes "a \<le> b"
   2.180 @@ -750,17 +816,36 @@
   2.181  
   2.182  end
   2.183  
   2.184 +class ordered_cancel_comm_monoid_add =
   2.185 +  ordered_comm_monoid_add + cancel_ab_semigroup_add
   2.186 +begin
   2.187  
   2.188 -subsection \<open>Support for reasoning about signs\<close>
   2.189 +subclass ordered_cancel_ab_semigroup_add ..
   2.190  
   2.191 -class ordered_comm_monoid_add =
   2.192 -  ordered_cancel_ab_semigroup_add + comm_monoid_add
   2.193 -begin
   2.194 +lemma add_neg_nonpos:
   2.195 +  assumes "a < 0" and "b \<le> 0" shows "a + b < 0"
   2.196 +proof -
   2.197 +  have "a + b < 0 + 0"
   2.198 +    using assms by (rule add_less_le_mono)
   2.199 +  then show ?thesis by simp
   2.200 +qed
   2.201 +
   2.202 +lemma add_neg_neg:
   2.203 +  assumes "a < 0" and "b < 0" shows "a + b < 0"
   2.204 +by (rule add_neg_nonpos) (insert assms, auto)
   2.205 +
   2.206 +lemma add_nonpos_neg:
   2.207 +  assumes "a \<le> 0" and "b < 0" shows "a + b < 0"
   2.208 +proof -
   2.209 +  have "a + b < 0 + 0"
   2.210 +    using assms by (rule add_le_less_mono)
   2.211 +  then show ?thesis by simp
   2.212 +qed
   2.213  
   2.214  lemma add_pos_nonneg:
   2.215    assumes "0 < a" and "0 \<le> b" shows "0 < a + b"
   2.216  proof -
   2.217 -  have "0 + 0 < a + b" 
   2.218 +  have "0 + 0 < a + b"
   2.219      using assms by (rule add_less_le_mono)
   2.220    then show ?thesis by simp
   2.221  qed
   2.222 @@ -772,79 +857,15 @@
   2.223  lemma add_nonneg_pos:
   2.224    assumes "0 \<le> a" and "0 < b" shows "0 < a + b"
   2.225  proof -
   2.226 -  have "0 + 0 < a + b" 
   2.227 +  have "0 + 0 < a + b"
   2.228      using assms by (rule add_le_less_mono)
   2.229    then show ?thesis by simp
   2.230  qed
   2.231  
   2.232 -lemma add_nonneg_nonneg [simp]:
   2.233 -  assumes "0 \<le> a" and "0 \<le> b" shows "0 \<le> a + b"
   2.234 -proof -
   2.235 -  have "0 + 0 \<le> a + b" 
   2.236 -    using assms by (rule add_mono)
   2.237 -  then show ?thesis by simp
   2.238 -qed
   2.239 -
   2.240 -lemma add_neg_nonpos:
   2.241 -  assumes "a < 0" and "b \<le> 0" shows "a + b < 0"
   2.242 -proof -
   2.243 -  have "a + b < 0 + 0"
   2.244 -    using assms by (rule add_less_le_mono)
   2.245 -  then show ?thesis by simp
   2.246 -qed
   2.247 -
   2.248 -lemma add_neg_neg: 
   2.249 -  assumes "a < 0" and "b < 0" shows "a + b < 0"
   2.250 -by (rule add_neg_nonpos) (insert assms, auto)
   2.251 -
   2.252 -lemma add_nonpos_neg:
   2.253 -  assumes "a \<le> 0" and "b < 0" shows "a + b < 0"
   2.254 -proof -
   2.255 -  have "a + b < 0 + 0"
   2.256 -    using assms by (rule add_le_less_mono)
   2.257 -  then show ?thesis by simp
   2.258 -qed
   2.259 -
   2.260 -lemma add_nonpos_nonpos:
   2.261 -  assumes "a \<le> 0" and "b \<le> 0" shows "a + b \<le> 0"
   2.262 -proof -
   2.263 -  have "a + b \<le> 0 + 0"
   2.264 -    using assms by (rule add_mono)
   2.265 -  then show ?thesis by simp
   2.266 -qed
   2.267 -
   2.268  lemmas add_sign_intros =
   2.269    add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg
   2.270    add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos
   2.271  
   2.272 -lemma add_nonneg_eq_0_iff:
   2.273 -  assumes x: "0 \<le> x" and y: "0 \<le> y"
   2.274 -  shows "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   2.275 -proof (intro iffI conjI)
   2.276 -  have "x = x + 0" by simp
   2.277 -  also have "x + 0 \<le> x + y" using y by (rule add_left_mono)
   2.278 -  also assume "x + y = 0"
   2.279 -  also have "0 \<le> x" using x .
   2.280 -  finally show "x = 0" .
   2.281 -next
   2.282 -  have "y = 0 + y" by simp
   2.283 -  also have "0 + y \<le> x + y" using x by (rule add_right_mono)
   2.284 -  also assume "x + y = 0"
   2.285 -  also have "0 \<le> y" using y .
   2.286 -  finally show "y = 0" .
   2.287 -next
   2.288 -  assume "x = 0 \<and> y = 0"
   2.289 -  then show "x + y = 0" by simp
   2.290 -qed
   2.291 -
   2.292 -lemma add_increasing:
   2.293 -  "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"
   2.294 -  by (insert add_mono [of 0 a b c], simp)
   2.295 -
   2.296 -lemma add_increasing2:
   2.297 -  "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"
   2.298 -  by (simp add: add_increasing add.commute [of a])
   2.299 -
   2.300  lemma add_strict_increasing:
   2.301    "0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c"
   2.302    by (insert add_less_le_mono [of 0 a b c], simp)
   2.303 @@ -855,8 +876,7 @@
   2.304  
   2.305  end
   2.306  
   2.307 -class ordered_ab_group_add =
   2.308 -  ab_group_add + ordered_ab_semigroup_add
   2.309 +class ordered_ab_group_add = ab_group_add + ordered_ab_semigroup_add
   2.310  begin
   2.311  
   2.312  subclass ordered_cancel_ab_semigroup_add ..
   2.313 @@ -870,7 +890,7 @@
   2.314    thus "a \<le> b" by simp
   2.315  qed
   2.316  
   2.317 -subclass ordered_comm_monoid_add ..
   2.318 +subclass ordered_cancel_comm_monoid_add ..
   2.319  
   2.320  lemma add_less_same_cancel1 [simp]:
   2.321    "b + a < b \<longleftrightarrow> a < 0"
   2.322 @@ -915,14 +935,14 @@
   2.323  lemma le_imp_neg_le:
   2.324    assumes "a \<le> b" shows "-b \<le> -a"
   2.325  proof -
   2.326 -  have "-a+a \<le> -a+b" using \<open>a \<le> b\<close> by (rule add_left_mono) 
   2.327 +  have "-a+a \<le> -a+b" using \<open>a \<le> b\<close> by (rule add_left_mono)
   2.328    then have "0 \<le> -a+b" by simp
   2.329 -  then have "0 + (-b) \<le> (-a + b) + (-b)" by (rule add_right_mono) 
   2.330 +  then have "0 + (-b) \<le> (-a + b) + (-b)" by (rule add_right_mono)
   2.331    then show ?thesis by (simp add: algebra_simps)
   2.332  qed
   2.333  
   2.334  lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b"
   2.335 -proof 
   2.336 +proof
   2.337    assume "- b \<le> - a"
   2.338    hence "- (- a) \<le> - (- b)" by (rule le_imp_neg_le)
   2.339    thus "a\<le>b" by simp
   2.340 @@ -938,7 +958,7 @@
   2.341  by (subst neg_le_iff_le [symmetric], simp)
   2.342  
   2.343  lemma neg_less_iff_less [simp]: "- b < - a \<longleftrightarrow> a < b"
   2.344 -by (force simp add: less_le) 
   2.345 +by (force simp add: less_le)
   2.346  
   2.347  lemma neg_less_0_iff_less [simp]: "- a < 0 \<longleftrightarrow> 0 < a"
   2.348  by (subst neg_less_iff_less [symmetric], simp)
   2.349 @@ -963,7 +983,7 @@
   2.350  lemma le_minus_iff: "a \<le> - b \<longleftrightarrow> b \<le> - a"
   2.351  proof -
   2.352    have mm: "!! a (b::'a). (-(-a)) < -b \<Longrightarrow> -(-b) < -a" by (simp only: minus_less_iff)
   2.353 -  have "(- (- a) <= -b) = (b <= - a)" 
   2.354 +  have "(- (- a) <= -b) = (b <= - a)"
   2.355      apply (auto simp only: le_less)
   2.356      apply (drule mm)
   2.357      apply (simp_all)
   2.358 @@ -1078,18 +1098,18 @@
   2.359  subclass ordered_ab_semigroup_add_imp_le
   2.360  proof
   2.361    fix a b c :: 'a
   2.362 -  assume le: "c + a <= c + b"  
   2.363 +  assume le: "c + a <= c + b"
   2.364    show "a <= b"
   2.365    proof (rule ccontr)
   2.366      assume w: "~ a \<le> b"
   2.367      hence "b <= a" by (simp add: linorder_not_le)
   2.368      hence le2: "c + b <= c + a" by (rule add_left_mono)
   2.369 -    have "a = b" 
   2.370 +    have "a = b"
   2.371        apply (insert le)
   2.372        apply (insert le2)
   2.373        apply (drule antisym, simp_all)
   2.374        done
   2.375 -    with w show False 
   2.376 +    with w show False
   2.377        by (simp add: linorder_not_le [symmetric])
   2.378    qed
   2.379  qed
   2.380 @@ -1192,7 +1212,7 @@
   2.381  qed
   2.382  
   2.383  lemma double_add_le_zero_iff_single_add_le_zero [simp]:
   2.384 -  "a + a \<le> 0 \<longleftrightarrow> a \<le> 0" 
   2.385 +  "a + a \<le> 0 \<longleftrightarrow> a \<le> 0"
   2.386  proof -
   2.387    have "\<not> a + a \<le> 0 \<longleftrightarrow> \<not> a \<le> 0"
   2.388      by (simp add: not_le)
   2.389 @@ -1272,7 +1292,7 @@
   2.390    thus ?thesis by simp
   2.391  qed
   2.392  
   2.393 -lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0" 
   2.394 +lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0"
   2.395  proof
   2.396    assume "\<bar>a\<bar> \<le> 0"
   2.397    then have "\<bar>a\<bar> = 0" by (rule antisym) simp
   2.398 @@ -1297,7 +1317,7 @@
   2.399    then show ?thesis by simp
   2.400  qed
   2.401  
   2.402 -lemma abs_minus_commute: 
   2.403 +lemma abs_minus_commute:
   2.404    "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
   2.405  proof -
   2.406    have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" by (simp only: abs_minus_cancel)
   2.407 @@ -1318,7 +1338,7 @@
   2.408    unfolding minus_minus by (erule abs_of_nonneg)
   2.409    then show ?thesis using assms by auto
   2.410  qed
   2.411 -  
   2.412 +
   2.413  lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"
   2.414  by (rule abs_of_nonpos, rule less_imp_le)
   2.415  
     3.1 --- a/src/HOL/Groups_Big.thy	Tue Feb 09 09:21:10 2016 +0100
     3.2 +++ b/src/HOL/Groups_Big.thy	Wed Feb 10 18:43:19 2016 +0100
     3.3 @@ -111,7 +111,7 @@
     3.4  lemma setdiff_irrelevant:
     3.5    assumes "finite A"
     3.6    shows "F g (A - {x. g x = z}) = F g A"
     3.7 -  using assms by (induct A) (simp_all add: insert_Diff_if) 
     3.8 +  using assms by (induct A) (simp_all add: insert_Diff_if)
     3.9  
    3.10  lemma not_neutral_contains_not_neutral:
    3.11    assumes "F g A \<noteq> z"
    3.12 @@ -196,9 +196,9 @@
    3.13  apply (simp add: comp_def)
    3.14  done
    3.15  
    3.16 -lemma related: 
    3.17 -  assumes Re: "R 1 1" 
    3.18 -  and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 * y1) (x2 * y2)" 
    3.19 +lemma related:
    3.20 +  assumes Re: "R 1 1"
    3.21 +  and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 * y1) (x2 * y2)"
    3.22    and fS: "finite S" and Rfg: "\<forall>x\<in>S. R (h x) (g x)"
    3.23    shows "R (F h S) (F g S)"
    3.24    using fS by (rule finite_subset_induct) (insert assms, auto)
    3.25 @@ -305,7 +305,7 @@
    3.26      by (intro reindex_bij_betw_not_neutral[OF _ _ bij]) auto
    3.27  qed
    3.28  
    3.29 -lemma delta: 
    3.30 +lemma delta:
    3.31    assumes fS: "finite S"
    3.32    shows "F (\<lambda>k. if k = a then b k else 1) S = (if a \<in> S then b a else 1)"
    3.33  proof-
    3.34 @@ -317,9 +317,9 @@
    3.35    { assume a: "a \<in> S"
    3.36      let ?A = "S - {a}"
    3.37      let ?B = "{a}"
    3.38 -    have eq: "S = ?A \<union> ?B" using a by blast 
    3.39 +    have eq: "S = ?A \<union> ?B" using a by blast
    3.40      have dj: "?A \<inter> ?B = {}" by simp
    3.41 -    from fS have fAB: "finite ?A" "finite ?B" by auto  
    3.42 +    from fS have fAB: "finite ?A" "finite ?B" by auto
    3.43      have "F ?f S = F ?f ?A * F ?f ?B"
    3.44        using union_disjoint [OF fAB dj, of ?f, unfolded eq [symmetric]]
    3.45        by simp
    3.46 @@ -327,7 +327,7 @@
    3.47    ultimately show ?thesis by blast
    3.48  qed
    3.49  
    3.50 -lemma delta': 
    3.51 +lemma delta':
    3.52    assumes fS: "finite S"
    3.53    shows "F (\<lambda>k. if a = k then b k else 1) S = (if a \<in> S then b a else 1)"
    3.54    using delta [OF fS, of a b, symmetric] by (auto intro: cong)
    3.55 @@ -338,10 +338,10 @@
    3.56    shows "F (\<lambda>x. if P x then h x else g x) A =
    3.57      F h (A \<inter> {x. P x}) * F g (A \<inter> - {x. P x})"
    3.58  proof -
    3.59 -  have a: "A = A \<inter> {x. P x} \<union> A \<inter> -{x. P x}" 
    3.60 -          "(A \<inter> {x. P x}) \<inter> (A \<inter> -{x. P x}) = {}" 
    3.61 +  have a: "A = A \<inter> {x. P x} \<union> A \<inter> -{x. P x}"
    3.62 +          "(A \<inter> {x. P x}) \<inter> (A \<inter> -{x. P x}) = {}"
    3.63      by blast+
    3.64 -  from fA 
    3.65 +  from fA
    3.66    have f: "finite (A \<inter> {x. P x})" "finite (A \<inter> -{x. P x})" by auto
    3.67    let ?g = "\<lambda>x. if P x then h x else g x"
    3.68    from union_disjoint [OF f a(2), of ?g] a(1)
    3.69 @@ -352,8 +352,8 @@
    3.70  lemma cartesian_product:
    3.71     "F (\<lambda>x. F (g x) B) A = F (case_prod g) (A \<times> B)"
    3.72  apply (rule sym)
    3.73 -apply (cases "finite A") 
    3.74 - apply (cases "finite B") 
    3.75 +apply (cases "finite A")
    3.76 + apply (cases "finite B")
    3.77    apply (simp add: Sigma)
    3.78   apply (cases "A={}", simp)
    3.79   apply simp
    3.80 @@ -512,7 +512,7 @@
    3.81  
    3.82  text \<open>TODO generalization candidates\<close>
    3.83  
    3.84 -lemma setsum_image_gen:
    3.85 +lemma (in comm_monoid_add) setsum_image_gen:
    3.86    assumes fS: "finite S"
    3.87    shows "setsum g S = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)"
    3.88  proof-
    3.89 @@ -557,13 +557,13 @@
    3.90      thus ?case by auto
    3.91    next
    3.92      case (insert x F)
    3.93 -    thus ?case using le finiteB 
    3.94 +    thus ?case using le finiteB
    3.95        by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
    3.96    qed
    3.97  qed
    3.98  
    3.99 -lemma setsum_mono:
   3.100 -  assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, ordered_ab_semigroup_add}))"
   3.101 +lemma (in ordered_comm_monoid_add) setsum_mono:
   3.102 +  assumes le: "\<And>i. i\<in>K \<Longrightarrow> f i \<le> g i"
   3.103    shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
   3.104  proof (cases "finite K")
   3.105    case True
   3.106 @@ -579,10 +579,8 @@
   3.107    case False then show ?thesis by simp
   3.108  qed
   3.109  
   3.110 -lemma setsum_strict_mono:
   3.111 -  fixes f :: "'a \<Rightarrow> 'b::{ordered_cancel_ab_semigroup_add,comm_monoid_add}"
   3.112 -  assumes "finite A"  "A \<noteq> {}"
   3.113 -    and "!!x. x:A \<Longrightarrow> f x < g x"
   3.114 +lemma (in ordered_cancel_comm_monoid_add) setsum_strict_mono:
   3.115 +  assumes "finite A"  "A \<noteq> {}" and "\<And>x. x \<in> A \<Longrightarrow> f x < g x"
   3.116    shows "setsum f A < setsum g A"
   3.117    using assms
   3.118  proof (induct rule: finite_ne_induct)
   3.119 @@ -592,9 +590,9 @@
   3.120  qed
   3.121  
   3.122  lemma setsum_strict_mono_ex1:
   3.123 -fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add, ordered_cancel_ab_semigroup_add}"
   3.124 -assumes "finite A" and "ALL x:A. f x \<le> g x" and "EX a:A. f a < g a"
   3.125 -shows "setsum f A < setsum g A"
   3.126 +  fixes f g :: "'i \<Rightarrow> 'a::ordered_cancel_comm_monoid_add"
   3.127 +  assumes "finite A" and "ALL x:A. f x \<le> g x" and "\<exists>a\<in>A. f a < g a"
   3.128 +  shows "setsum f A < setsum g A"
   3.129  proof-
   3.130    from assms(3) obtain a where a: "a:A" "f a < g a" by blast
   3.131    have "setsum f A = setsum f ((A-{a}) \<union> {a})"
   3.132 @@ -624,8 +622,8 @@
   3.133    "(\<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)"
   3.134    by (induction A rule: infinite_finite_induct) (auto simp: setsum_mono)
   3.135  
   3.136 -lemma setsum_nonneg:
   3.137 -  assumes nn: "\<forall>x\<in>A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
   3.138 +lemma (in ordered_comm_monoid_add) setsum_nonneg:
   3.139 +  assumes nn: "\<forall>x\<in>A. 0 \<le> f x"
   3.140    shows "0 \<le> setsum f A"
   3.141  proof (cases "finite A")
   3.142    case True thus ?thesis using nn
   3.143 @@ -640,8 +638,8 @@
   3.144    case False thus ?thesis by simp
   3.145  qed
   3.146  
   3.147 -lemma setsum_nonpos:
   3.148 -  assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{ordered_ab_semigroup_add,comm_monoid_add})"
   3.149 +lemma (in ordered_comm_monoid_add) setsum_nonpos:
   3.150 +  assumes np: "\<forall>x\<in>A. f x \<le> 0"
   3.151    shows "setsum f A \<le> 0"
   3.152  proof (cases "finite A")
   3.153    case True thus ?thesis using np
   3.154 @@ -656,30 +654,28 @@
   3.155    case False thus ?thesis by simp
   3.156  qed
   3.157  
   3.158 -lemma setsum_nonneg_leq_bound:
   3.159 -  fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
   3.160 +lemma (in ordered_comm_monoid_add) setsum_nonneg_eq_0_iff:
   3.161 +  "finite A \<Longrightarrow> \<forall>x\<in>A. 0 \<le> f x \<Longrightarrow> setsum f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
   3.162 +  by (induct set: finite, simp) (simp add: add_nonneg_eq_0_iff setsum_nonneg)
   3.163 +
   3.164 +lemma (in ordered_comm_monoid_add) setsum_nonneg_0:
   3.165 +  "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"
   3.166 +  by (simp add: setsum_nonneg_eq_0_iff)
   3.167 +
   3.168 +lemma (in ordered_comm_monoid_add) setsum_nonneg_leq_bound:
   3.169    assumes "finite s" "\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0" "(\<Sum>i \<in> s. f i) = B" "i \<in> s"
   3.170    shows "f i \<le> B"
   3.171  proof -
   3.172 -  have "0 \<le> (\<Sum> i \<in> s - {i}. f i)" and "0 \<le> f i"
   3.173 -    using assms by (auto intro!: setsum_nonneg)
   3.174 -  moreover
   3.175 -  have "(\<Sum> i \<in> s - {i}. f i) + f i = B"
   3.176 -    using assms by (simp add: setsum_diff1)
   3.177 -  ultimately show ?thesis by auto
   3.178 +  have "f i \<le> f i + (\<Sum>i \<in> s - {i}. f i)"
   3.179 +    using assms by (intro add_increasing2 setsum_nonneg) auto
   3.180 +  also have "\<dots> = B"
   3.181 +    using setsum.remove[of s i f] assms by simp
   3.182 +  finally show ?thesis by auto
   3.183  qed
   3.184  
   3.185 -lemma setsum_nonneg_0:
   3.186 -  fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
   3.187 -  assumes "finite s" and pos: "\<And> i. i \<in> s \<Longrightarrow> f i \<ge> 0"
   3.188 -  and "(\<Sum> i \<in> s. f i) = 0" and i: "i \<in> s"
   3.189 -  shows "f i = 0"
   3.190 -  using setsum_nonneg_leq_bound[OF assms] pos[OF i] by auto
   3.191 -
   3.192 -lemma setsum_mono2:
   3.193 -fixes f :: "'a \<Rightarrow> 'b :: ordered_comm_monoid_add"
   3.194 -assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
   3.195 -shows "setsum f A \<le> setsum f B"
   3.196 +lemma (in ordered_comm_monoid_add) setsum_mono2:
   3.197 +  assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
   3.198 +  shows "setsum f A \<le> setsum f B"
   3.199  proof -
   3.200    have "setsum f A \<le> setsum f A + setsum f (B-A)"
   3.201      by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
   3.202 @@ -689,8 +685,7 @@
   3.203    finally show ?thesis .
   3.204  qed
   3.205  
   3.206 -lemma setsum_le_included:
   3.207 -  fixes f :: "'a \<Rightarrow> 'b::ordered_comm_monoid_add"
   3.208 +lemma (in ordered_comm_monoid_add) setsum_le_included:
   3.209    assumes "finite s" "finite t"
   3.210    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)"
   3.211    shows "setsum f s \<le> setsum g t"
   3.212 @@ -710,25 +705,15 @@
   3.213    finally show ?thesis .
   3.214  qed
   3.215  
   3.216 -lemma setsum_mono3: "finite B ==> A <= B ==> 
   3.217 -    ALL x: B - A. 
   3.218 -      0 <= ((f x)::'a::{comm_monoid_add,ordered_ab_semigroup_add}) ==>
   3.219 -        setsum f A <= setsum f B"
   3.220 -  apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
   3.221 -  apply (erule ssubst)
   3.222 -  apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
   3.223 -  apply simp
   3.224 -  apply (rule add_left_mono)
   3.225 -  apply (erule setsum_nonneg)
   3.226 -  apply (subst setsum.union_disjoint [THEN sym])
   3.227 -  apply (erule finite_subset, assumption)
   3.228 -  apply (rule finite_subset)
   3.229 -  prefer 2
   3.230 -  apply assumption
   3.231 -  apply (auto simp add: sup_absorb2)
   3.232 -done
   3.233 +lemma (in ordered_comm_monoid_add) setsum_mono3:
   3.234 +  "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> \<forall>x\<in>B - A. 0 \<le> f x \<Longrightarrow> setsum f A \<le> setsum f B"
   3.235 +  by (rule setsum_mono2) auto
   3.236  
   3.237 -lemma setsum_right_distrib: 
   3.238 +lemma (in canonically_ordered_monoid_add) setsum_eq_0_iff [simp]:
   3.239 +  "finite F \<Longrightarrow> (setsum f F = 0) = (\<forall>a\<in>F. f a = 0)"
   3.240 +  by (intro ballI setsum_nonneg_eq_0_iff zero_le)
   3.241 +
   3.242 +lemma setsum_right_distrib:
   3.243    fixes f :: "'a => ('b::semiring_0)"
   3.244    shows "r * setsum f A = setsum (%n. r * f n) A"
   3.245  proof (cases "finite A")
   3.246 @@ -771,7 +756,7 @@
   3.247    case False thus ?thesis by simp
   3.248  qed
   3.249  
   3.250 -lemma setsum_abs[iff]: 
   3.251 +lemma setsum_abs[iff]:
   3.252    fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   3.253    shows "\<bar>setsum f A\<bar> \<le> setsum (%i. \<bar>f i\<bar>) A"
   3.254  proof (cases "finite A")
   3.255 @@ -792,7 +777,7 @@
   3.256    shows "0 \<le> setsum (%i. \<bar>f i\<bar>) A"
   3.257    by (simp add: setsum_nonneg)
   3.258  
   3.259 -lemma abs_setsum_abs[simp]: 
   3.260 +lemma abs_setsum_abs[simp]:
   3.261    fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   3.262    shows "\<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar> = (\<Sum>a\<in>A. \<bar>f a\<bar>)"
   3.263  proof (cases "finite A")
   3.264 @@ -836,10 +821,6 @@
   3.265  apply (erule finite_induct, auto)
   3.266  done
   3.267  
   3.268 -lemma setsum_eq_0_iff [simp]:
   3.269 -  "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   3.270 -  by (induct set: finite) auto
   3.271 -
   3.272  lemma setsum_eq_Suc0_iff: "finite A \<Longrightarrow>
   3.273    setsum f A = Suc 0 \<longleftrightarrow> (EX a:A. f a = Suc 0 & (ALL b:A. a\<noteq>b \<longrightarrow> f b = 0))"
   3.274  apply(erule finite_induct)
   3.275 @@ -862,7 +843,7 @@
   3.276  apply (drule_tac a = a in mk_disjoint_insert, auto)
   3.277  done
   3.278  
   3.279 -lemma setsum_diff_nat: 
   3.280 +lemma setsum_diff_nat:
   3.281  assumes "finite B" and "B \<subseteq> A"
   3.282  shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
   3.283  using assms
   3.284 @@ -945,11 +926,11 @@
   3.285  done
   3.286  
   3.287  lemma setsum_Suc: "setsum (\<lambda>x. Suc(f x)) A = setsum f A + card A"
   3.288 -  using setsum.distrib[of f "\<lambda>_. 1" A] 
   3.289 +  using setsum.distrib[of f "\<lambda>_. 1" A]
   3.290    by simp
   3.291  
   3.292  lemma setsum_bounded_above:
   3.293 -  assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"
   3.294 +  assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_comm_monoid_add})"
   3.295    shows "setsum f A \<le> of_nat (card A) * K"
   3.296  proof (cases "finite A")
   3.297    case True
   3.298 @@ -959,14 +940,14 @@
   3.299  qed
   3.300  
   3.301  lemma setsum_bounded_above_strict:
   3.302 -  assumes "\<And>i. i\<in>A \<Longrightarrow> f i < (K::'a::{ordered_cancel_ab_semigroup_add,semiring_1})"
   3.303 +  assumes "\<And>i. i\<in>A \<Longrightarrow> f i < (K::'a::{ordered_cancel_comm_monoid_add,semiring_1})"
   3.304            "card A > 0"
   3.305    shows "setsum f A < of_nat (card A) * K"
   3.306  using assms setsum_strict_mono[where A=A and g = "%x. K"]
   3.307  by (simp add: card_gt_0_iff)
   3.308  
   3.309  lemma setsum_bounded_below:
   3.310 -  assumes le: "\<And>i. i\<in>A \<Longrightarrow> (K::'a::{semiring_1, ordered_ab_semigroup_add}) \<le> f i"
   3.311 +  assumes le: "\<And>i. i\<in>A \<Longrightarrow> (K::'a::{semiring_1, ordered_comm_monoid_add}) \<le> f i"
   3.312    shows "of_nat (card A) * K \<le> setsum f A"
   3.313  proof (cases "finite A")
   3.314    case True
   3.315 @@ -1011,7 +992,7 @@
   3.316    finally show ?thesis by auto
   3.317  qed
   3.318  
   3.319 -lemma (in ordered_comm_monoid_add) setsum_pos: 
   3.320 +lemma (in ordered_cancel_comm_monoid_add) setsum_pos:
   3.321    "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 < f i) \<Longrightarrow> 0 < setsum f I"
   3.322    by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos)
   3.323  
   3.324 @@ -1057,7 +1038,7 @@
   3.325  syntax
   3.326    "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(2\<Prod>_\<in>_./ _)" [0, 51, 10] 10)
   3.327  translations \<comment> \<open>Beware of argument permutation!\<close>
   3.328 -  "\<Prod>i\<in>A. b" == "CONST setprod (\<lambda>i. b) A" 
   3.329 +  "\<Prod>i\<in>A. b" == "CONST setprod (\<lambda>i. b) A"
   3.330  
   3.331  text \<open>Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter \<open>\<Prod>x|P. e\<close>.\<close>
   3.332  
   3.333 @@ -1071,7 +1052,7 @@
   3.334  context comm_monoid_mult
   3.335  begin
   3.336  
   3.337 -lemma setprod_dvd_setprod: 
   3.338 +lemma setprod_dvd_setprod:
   3.339    "(\<And>a. a \<in> A \<Longrightarrow> f a dvd g a) \<Longrightarrow> setprod f A dvd setprod g A"
   3.340  proof (induct A rule: infinite_finite_induct)
   3.341    case infinite then show ?case by (auto intro: dvdI)
   3.342 @@ -1167,7 +1148,7 @@
   3.343    qed
   3.344  qed
   3.345  
   3.346 -lemma (in field) setprod_inversef: 
   3.347 +lemma (in field) setprod_inversef:
   3.348    "finite A \<Longrightarrow> setprod (inverse \<circ> f) A = inverse (setprod f A)"
   3.349    by (induct A rule: finite_induct) simp_all
   3.350  
   3.351 @@ -1195,15 +1176,13 @@
   3.352    by (induct A rule: infinite_finite_induct) simp_all
   3.353  
   3.354  lemma (in linordered_semidom) setprod_mono:
   3.355 -  assumes "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i"
   3.356 -  shows "setprod f A \<le> setprod g A"
   3.357 -  using assms by (induct A rule: infinite_finite_induct)
   3.358 -    (auto intro!: setprod_nonneg mult_mono)
   3.359 +  "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i \<Longrightarrow> setprod f A \<le> setprod g A"
   3.360 +  by (induct A rule: infinite_finite_induct) (auto intro!: setprod_nonneg mult_mono)
   3.361  
   3.362  lemma (in linordered_semidom) setprod_mono_strict:
   3.363      assumes"finite A" "\<forall>i\<in>A. 0 \<le> f i \<and> f i < g i" "A \<noteq> {}"
   3.364      shows "setprod f A < setprod g A"
   3.365 -using assms 
   3.366 +using assms
   3.367  apply (induct A rule: finite_induct)
   3.368  apply (simp add: )
   3.369  apply (force intro: mult_strict_mono' setprod_nonneg)
   3.370 @@ -1221,11 +1200,4 @@
   3.371    "finite A \<Longrightarrow> setprod f A > 0 \<longleftrightarrow> (\<forall>a\<in>A. f a > (0::nat))"
   3.372    using setprod_zero_iff by (simp del:neq0_conv add:neq0_conv [symmetric])
   3.373  
   3.374 -lemma setsum_nonneg_eq_0_iff:
   3.375 -  fixes f :: "'a \<Rightarrow> 'b::ordered_ab_group_add"
   3.376 -  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)"
   3.377 -  apply (induct set: finite, simp)
   3.378 -  apply (simp add: add_nonneg_eq_0_iff setsum_nonneg)
   3.379 -  done
   3.380 -
   3.381  end
     4.1 --- a/src/HOL/Library/Convex.thy	Tue Feb 09 09:21:10 2016 +0100
     4.2 +++ b/src/HOL/Library/Convex.thy	Wed Feb 10 18:43:19 2016 +0100
     4.3 @@ -565,7 +565,7 @@
     4.4      then have "(\<Sum> j \<in> s. a j) = 0"
     4.5        using insert by auto
     4.6      then have "\<And>j. j \<in> s \<Longrightarrow> a j = 0"
     4.7 -      using setsum_nonneg_0[where 'b=real] insert by fastforce
     4.8 +      using insert by (fastforce simp: setsum_nonneg_eq_0_iff)
     4.9      then show ?thesis
    4.10        using insert by auto
    4.11    next
     5.1 --- a/src/HOL/Library/Extended_Nat.thy	Tue Feb 09 09:21:10 2016 +0100
     5.2 +++ b/src/HOL/Library/Extended_Nat.thy	Wed Feb 10 18:43:19 2016 +0100
     5.3 @@ -62,6 +62,9 @@
     5.4  lemma not_enat_eq [iff]: "(\<forall>y. x \<noteq> enat y) = (x = \<infinity>)"
     5.5    by (cases x) auto
     5.6  
     5.7 +lemma enat_ex_split: "(\<exists>c::enat. P c) \<longleftrightarrow> P \<infinity> \<or> (\<exists>c::nat. P c)"
     5.8 +  by (metis enat.exhaust)
     5.9 +
    5.10  primrec the_enat :: "enat \<Rightarrow> nat"
    5.11    where "the_enat (enat n) = n"
    5.12  
    5.13 @@ -359,11 +362,16 @@
    5.14  
    5.15  end
    5.16  
    5.17 -instance enat :: ordered_comm_semiring
    5.18 +instance enat :: dioid
    5.19 +proof
    5.20 +  fix a b :: enat show "(a \<le> b) = (\<exists>c. b = a + c)"
    5.21 +    by (cases a b rule: enat2_cases) (auto simp: le_iff_add enat_ex_split)
    5.22 +qed
    5.23 +
    5.24 +instance enat :: "ordered_comm_semiring"
    5.25  proof
    5.26    fix a b c :: enat
    5.27 -  assume "a \<le> b" and "0 \<le> c"
    5.28 -  thus "c * a \<le> c * b"
    5.29 +  assume "a \<le> b" and "0 \<le> c" thus "c * a \<le> c * b"
    5.30      unfolding times_enat_def less_eq_enat_def zero_enat_def
    5.31      by (simp split: enat.splits)
    5.32  qed
     6.1 --- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Tue Feb 09 09:21:10 2016 +0100
     6.2 +++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Wed Feb 10 18:43:19 2016 +0100
     6.3 @@ -78,6 +78,13 @@
     6.4  lemma ennreal_zero_less_one: "0 < (1::ennreal)"
     6.5    by transfer auto
     6.6  
     6.7 +instance ennreal :: dioid
     6.8 +proof (standard; transfer)
     6.9 +  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)"
    6.10 +    unfolding ereal_ex_split Bex_def
    6.11 +    by (cases a b rule: ereal2_cases) (auto intro!: exI[of _ "real_of_ereal (b - a)"])
    6.12 +qed
    6.13 +
    6.14  instance ennreal :: ordered_comm_semiring
    6.15    by standard
    6.16       (transfer ; auto intro: add_mono mult_mono mult_ac ereal_left_distrib ereal_mult_left_mono)+
     7.1 --- a/src/HOL/Library/Extended_Real.thy	Tue Feb 09 09:21:10 2016 +0100
     7.2 +++ b/src/HOL/Library/Extended_Real.thy	Wed Feb 10 18:43:19 2016 +0100
     7.3 @@ -19,6 +19,26 @@
     7.4  
     7.5  \<close>
     7.6  
     7.7 +lemma image_eqD: "f ` A = B \<Longrightarrow> \<forall>x\<in>A. f x \<in> B"
     7.8 +  by auto
     7.9 +
    7.10 +lemma incseq_setsumI2:
    7.11 +  fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::ordered_comm_monoid_add"
    7.12 +  shows "(\<And>n. n \<in> A \<Longrightarrow> mono (f n)) \<Longrightarrow> mono (\<lambda>i. \<Sum>n\<in>A. f n i)"
    7.13 +  unfolding incseq_def by (auto intro: setsum_mono)
    7.14 +
    7.15 +lemma incseq_setsumI:
    7.16 +  fixes f :: "nat \<Rightarrow> 'a::ordered_comm_monoid_add"
    7.17 +  assumes "\<And>i. 0 \<le> f i"
    7.18 +  shows "incseq (\<lambda>i. setsum f {..< i})"
    7.19 +proof (intro incseq_SucI)
    7.20 +  fix n
    7.21 +  have "setsum f {..< n} + 0 \<le> setsum f {..<n} + f n"
    7.22 +    using assms by (rule add_left_mono)
    7.23 +  then show "setsum f {..< n} \<le> setsum f {..< Suc n}"
    7.24 +    by auto
    7.25 +qed
    7.26 +
    7.27  lemma continuous_at_left_imp_sup_continuous:
    7.28    fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology}"
    7.29    assumes "mono f" "\<And>x. continuous (at_left x) f"
    7.30 @@ -535,7 +555,7 @@
    7.31  instance ereal :: dense_linorder
    7.32    by standard (blast dest: ereal_dense2)
    7.33  
    7.34 -instance ereal :: ordered_ab_semigroup_add
    7.35 +instance ereal :: ordered_comm_monoid_add
    7.36  proof
    7.37    fix a b c :: ereal
    7.38    assume "a \<le> b"
    7.39 @@ -742,28 +762,6 @@
    7.40    shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a + b"
    7.41    using add_mono[of 0 a 0 b] by simp
    7.42  
    7.43 -lemma image_eqD: "f ` A = B \<Longrightarrow> \<forall>x\<in>A. f x \<in> B"
    7.44 -  by auto
    7.45 -
    7.46 -lemma incseq_setsumI:
    7.47 -  fixes f :: "nat \<Rightarrow> 'a::{comm_monoid_add,ordered_ab_semigroup_add}"
    7.48 -  assumes "\<And>i. 0 \<le> f i"
    7.49 -  shows "incseq (\<lambda>i. setsum f {..< i})"
    7.50 -proof (intro incseq_SucI)
    7.51 -  fix n
    7.52 -  have "setsum f {..< n} + 0 \<le> setsum f {..<n} + f n"
    7.53 -    using assms by (rule add_left_mono)
    7.54 -  then show "setsum f {..< n} \<le> setsum f {..< Suc n}"
    7.55 -    by auto
    7.56 -qed
    7.57 -
    7.58 -lemma incseq_setsumI2:
    7.59 -  fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::{comm_monoid_add,ordered_ab_semigroup_add}"
    7.60 -  assumes "\<And>n. n \<in> A \<Longrightarrow> incseq (f n)"
    7.61 -  shows "incseq (\<lambda>i. \<Sum>n\<in>A. f n i)"
    7.62 -  using assms
    7.63 -  unfolding incseq_def by (auto intro: setsum_mono)
    7.64 -
    7.65  lemma setsum_ereal[simp]: "(\<Sum>x\<in>A. ereal (f x)) = ereal (\<Sum>x\<in>A. f x)"
    7.66  proof (cases "finite A")
    7.67    case True
     8.1 --- a/src/HOL/Library/Function_Algebras.thy	Tue Feb 09 09:21:10 2016 +0100
     8.2 +++ b/src/HOL/Library/Function_Algebras.thy	Wed Feb 10 18:43:19 2016 +0100
     8.3 @@ -153,7 +153,7 @@
     8.4  
     8.5  instance "fun" :: (type, semiring_1_cancel) semiring_1_cancel ..
     8.6  
     8.7 -instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel 
     8.8 +instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel
     8.9    by standard (auto simp add: times_fun_def algebra_simps)
    8.10  
    8.11  instance "fun" :: (type, semiring_char_0) semiring_char_0
    8.12 @@ -188,11 +188,21 @@
    8.13  
    8.14  instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add ..
    8.15  
    8.16 +instance "fun" :: (type, ordered_cancel_comm_monoid_add) ordered_cancel_comm_monoid_add ..
    8.17 +
    8.18  instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
    8.19  
    8.20  instance "fun" :: (type, ordered_semiring) ordered_semiring
    8.21    by standard (auto simp add: le_fun_def intro: mult_left_mono mult_right_mono)
    8.22  
    8.23 +instance "fun" :: (type, dioid) dioid
    8.24 +proof standard
    8.25 +  fix a b :: "'a \<Rightarrow> 'b"
    8.26 +  show "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)"
    8.27 +    unfolding le_fun_def plus_fun_def fun_eq_iff choice_iff[symmetric, of "\<lambda>x c. b x = a x + c"]
    8.28 +    by (intro arg_cong[where f=All] ext canonically_ordered_monoid_add_class.le_iff_add)
    8.29 +qed
    8.30 +
    8.31  instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring
    8.32    by standard (fact mult_left_mono)
    8.33  
     9.1 --- a/src/HOL/Library/Multiset.thy	Tue Feb 09 09:21:10 2016 +0100
     9.2 +++ b/src/HOL/Library/Multiset.thy	Wed Feb 10 18:43:19 2016 +0100
     9.3 @@ -302,7 +302,7 @@
     9.4     apply (auto intro: multiset_eq_iff [THEN iffD2])
     9.5    done
     9.6  
     9.7 -interpretation subset_mset: ordered_cancel_comm_monoid_diff  "op +" "op -" 0 "op \<le>#" "op <#"
     9.8 +interpretation subset_mset: ordered_cancel_comm_monoid_diff  "op +" 0 "op \<le>#" "op <#" "op -"
     9.9    by standard (simp, fact mset_le_exists_conv)
    9.10  
    9.11  lemma mset_le_mono_add_right_cancel [simp]: "(A::'a multiset) + C \<le># B + C \<longleftrightarrow> A \<le># B"
    10.1 --- a/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy	Tue Feb 09 09:21:10 2016 +0100
    10.2 +++ b/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy	Wed Feb 10 18:43:19 2016 +0100
    10.3 @@ -65,7 +65,7 @@
    10.4    shows "a\<bullet>i \<le> x\<bullet>i" "x\<bullet>i \<le> b\<bullet>i"
    10.5    using assms
    10.6    unfolding euclidean_inner[of a i] euclidean_inner[of x i] euclidean_inner[of b i]
    10.7 -  by (auto intro!: setsum_mono mult_right_mono simp: eucl_le)
    10.8 +  by (auto intro!: ordered_comm_monoid_add_class.setsum_mono mult_right_mono simp: eucl_le)
    10.9  
   10.10  lemma inner_nonneg_nonneg:
   10.11    shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a \<bullet> b"
    11.1 --- a/src/HOL/NSA/StarDef.thy	Tue Feb 09 09:21:10 2016 +0100
    11.2 +++ b/src/HOL/NSA/StarDef.thy	Wed Feb 10 18:43:19 2016 +0100
    11.3 @@ -140,7 +140,7 @@
    11.4  done
    11.5  
    11.6  lemma transfer_fun_eq [transfer_intro]:
    11.7 -  "\<lbrakk>\<And>X. f (star_n X) = g (star_n X) 
    11.8 +  "\<lbrakk>\<And>X. f (star_n X) = g (star_n X)
    11.9      \<equiv> eventually (\<lambda>n. F n (X n) = G n (X n)) \<U>\<rbrakk>
   11.10        \<Longrightarrow> f = g \<equiv> eventually (\<lambda>n. F n = G n) \<U>"
   11.11  by (simp only: fun_eq_iff transfer_all)
   11.12 @@ -806,9 +806,10 @@
   11.13  by (intro_classes, transfer, rule add_le_imp_le_left)
   11.14  
   11.15  instance star :: (ordered_comm_monoid_add) ordered_comm_monoid_add ..
   11.16 +instance star :: (ordered_cancel_comm_monoid_add) ordered_cancel_comm_monoid_add ..
   11.17  instance star :: (ordered_ab_group_add) ordered_ab_group_add ..
   11.18  
   11.19 -instance star :: (ordered_ab_group_add_abs) ordered_ab_group_add_abs 
   11.20 +instance star :: (ordered_ab_group_add_abs) ordered_ab_group_add_abs
   11.21    by intro_classes (transfer,
   11.22      simp add: abs_ge_self abs_leI abs_triangle_ineq)+
   11.23  
   11.24 @@ -820,12 +821,12 @@
   11.25  instance star :: (semiring) semiring
   11.26    by (intro_classes; transfer) (fact distrib_right distrib_left)+
   11.27  
   11.28 -instance star :: (semiring_0) semiring_0 
   11.29 +instance star :: (semiring_0) semiring_0
   11.30    by (intro_classes; transfer) simp_all
   11.31  
   11.32  instance star :: (semiring_0_cancel) semiring_0_cancel ..
   11.33  
   11.34 -instance star :: (comm_semiring) comm_semiring 
   11.35 +instance star :: (comm_semiring) comm_semiring
   11.36    by (intro_classes; transfer) (fact distrib_right)
   11.37  
   11.38  instance star :: (comm_semiring_0) comm_semiring_0 ..
   11.39 @@ -846,7 +847,7 @@
   11.40    by (intro_classes; transfer) (fact no_zero_divisors)
   11.41  
   11.42  instance star :: (semiring_1_no_zero_divisors) semiring_1_no_zero_divisors ..
   11.43 -  
   11.44 +
   11.45  instance star :: (semiring_no_zero_divisors_cancel) semiring_no_zero_divisors_cancel
   11.46    by (intro_classes; transfer) simp_all
   11.47  
   11.48 @@ -865,7 +866,7 @@
   11.49  
   11.50  instance star :: (ring_no_zero_divisors) ring_no_zero_divisors ..
   11.51  instance star :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors ..
   11.52 -instance star :: (idom) idom .. 
   11.53 +instance star :: (idom) idom ..
   11.54  instance star :: (idom_divide) idom_divide ..
   11.55  
   11.56  instance star :: (division_ring) division_ring
   11.57 @@ -919,7 +920,7 @@
   11.58    "(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x"
   11.59  proof (rule eq_reflection, rule ext, rule ext)
   11.60    fix n :: nat
   11.61 -  show "\<And>x::'a star. x ^ n = ( *f* (\<lambda>x. x ^ n)) x" 
   11.62 +  show "\<And>x::'a star. x ^ n = ( *f* (\<lambda>x. x ^ n)) x"
   11.63    proof (induct n)
   11.64      case 0
   11.65      have "\<And>x::'a star. ( *f* (\<lambda>x. 1)) x = 1"
    12.1 --- a/src/HOL/Nat.thy	Tue Feb 09 09:21:10 2016 +0100
    12.2 +++ b/src/HOL/Nat.thy	Wed Feb 10 18:43:19 2016 +0100
    12.3 @@ -735,8 +735,11 @@
    12.4  lemma add_diff_inverse_nat: "~  m < n ==> n + (m - n) = (m::nat)"
    12.5  by (induct m n rule: diff_induct) simp_all
    12.6  
    12.7 -
    12.8 -text\<open>The naturals form an ordered \<open>semidom\<close>\<close>
    12.9 +lemma nat_le_iff_add: "(m::nat) \<le> n = (\<exists>k. n = m + k)"
   12.10 +using nat_add_left_cancel_le[of m 0] by (auto dest: le_Suc_ex)
   12.11 +
   12.12 +text\<open>The naturals form an ordered \<open>semidom\<close> and a \<open>dioid\<close>\<close>
   12.13 +
   12.14  instance nat :: linordered_semidom
   12.15  proof
   12.16    show "0 < (1::nat)" by simp
   12.17 @@ -745,8 +748,16 @@
   12.18    show "\<And>m n :: nat. m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m * n \<noteq> 0" by simp
   12.19    show "\<And>m n :: nat. n \<le> m ==> (m - n) + n = (m::nat)"
   12.20      by (simp add: add_diff_inverse_nat add.commute linorder_not_less)
   12.21 -qed 
   12.22 -
   12.23 +qed
   12.24 +
   12.25 +instance nat :: dioid
   12.26 +  proof qed (rule nat_le_iff_add)
   12.27 +
   12.28 +instance nat :: ordered_cancel_comm_monoid_add
   12.29 +  proof qed
   12.30 +
   12.31 +instance nat :: ordered_cancel_comm_monoid_diff
   12.32 +  proof qed
   12.33  
   12.34  subsubsection \<open>@{term min} and @{term max}\<close>
   12.35  
   12.36 @@ -1079,14 +1090,6 @@
   12.37  lemma diff_le_self [simp]: "m - n \<le> (m::nat)"
   12.38  by (induct m n rule: diff_induct) (simp_all add: le_SucI)
   12.39  
   12.40 -lemma le_iff_add: "(m::nat) \<le> n = (\<exists>k. n = m + k)"
   12.41 -  by (auto simp: le_add1 dest!: le_add_diff_inverse sym [of _ n])
   12.42 -
   12.43 -instance nat :: ordered_cancel_comm_monoid_diff
   12.44 -proof
   12.45 -  show "\<And>m n :: nat. m \<le> n \<longleftrightarrow> (\<exists>q. n = m + q)" by (fact le_iff_add)
   12.46 -qed
   12.47 -
   12.48  lemma less_imp_diff_less: "(j::nat) < k ==> j - n < k"
   12.49  by (rule le_less_trans, rule diff_le_self)
   12.50  
   12.51 @@ -1488,7 +1491,7 @@
   12.52    by (simp add: not_less)
   12.53  
   12.54  lemma of_nat_less_iff [simp]: "of_nat m < of_nat n \<longleftrightarrow> m < n"
   12.55 -  by (induct m n rule: diff_induct, simp_all add: add_pos_nonneg)
   12.56 +  by (induct m n rule: diff_induct) (simp_all add: add_pos_nonneg)
   12.57  
   12.58  lemma of_nat_le_iff [simp]: "of_nat m \<le> of_nat n \<longleftrightarrow> m \<le> n"
   12.59    by (simp add: not_less [symmetric] linorder_not_less [symmetric])
    13.1 --- a/src/HOL/Rings.thy	Tue Feb 09 09:21:10 2016 +0100
    13.2 +++ b/src/HOL/Rings.thy	Wed Feb 10 18:43:19 2016 +0100
    13.3 @@ -635,7 +635,7 @@
    13.4    case False then have "a * 0 div a = 0"
    13.5      by (rule nonzero_mult_divide_cancel_left)
    13.6    then show ?thesis by simp
    13.7 -qed 
    13.8 +qed
    13.9  
   13.10  lemma divide_1 [simp]:
   13.11    "a div 1 = a"
   13.12 @@ -663,16 +663,16 @@
   13.13    with assms have "c = b * d" by (simp add: ac_simps)
   13.14    then show ?Q ..
   13.15  next
   13.16 -  assume ?Q then obtain d where "c = b * d" .. 
   13.17 +  assume ?Q then obtain d where "c = b * d" ..
   13.18    then have "a * c = a * b * d" by (simp add: ac_simps)
   13.19    then show ?P ..
   13.20  qed
   13.21 -  
   13.22 +
   13.23  lemma dvd_times_right_cancel_iff [simp]:
   13.24    assumes "a \<noteq> 0"
   13.25    shows "b * a dvd c * a \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
   13.26  using dvd_times_left_cancel_iff [of a b c] assms by (simp add: ac_simps)
   13.27 -  
   13.28 +
   13.29  lemma div_dvd_iff_mult:
   13.30    assumes "b \<noteq> 0" and "b dvd a"
   13.31    shows "a div b dvd c \<longleftrightarrow> a dvd c * b"
   13.32 @@ -991,7 +991,7 @@
   13.33      and unit_factor_0 [simp]: "unit_factor 0 = 0"
   13.34    assumes is_unit_normalize:
   13.35      "is_unit a  \<Longrightarrow> normalize a = 1"
   13.36 -  assumes unit_factor_is_unit [iff]: 
   13.37 +  assumes unit_factor_is_unit [iff]:
   13.38      "a \<noteq> 0 \<Longrightarrow> is_unit (unit_factor a)"
   13.39    assumes unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
   13.40  begin
   13.41 @@ -1012,8 +1012,8 @@
   13.42  
   13.43  lemma unit_factor_self [simp]:
   13.44    "unit_factor a dvd a"
   13.45 -  by (cases "a = 0") simp_all 
   13.46 -  
   13.47 +  by (cases "a = 0") simp_all
   13.48 +
   13.49  lemma normalize_mult_unit_factor [simp]:
   13.50    "normalize a * unit_factor a = a"
   13.51    using unit_factor_mult_normalize [of a] by (simp add: ac_simps)
   13.52 @@ -1023,7 +1023,7 @@
   13.53  proof
   13.54    assume ?P
   13.55    moreover have "unit_factor a * normalize a = a" by simp
   13.56 -  ultimately show ?Q by simp 
   13.57 +  ultimately show ?Q by simp
   13.58  next
   13.59    assume ?Q then show ?P by simp
   13.60  qed
   13.61 @@ -1033,14 +1033,14 @@
   13.62  proof
   13.63    assume ?P
   13.64    moreover have "unit_factor a * normalize a = a" by simp
   13.65 -  ultimately show ?Q by simp 
   13.66 +  ultimately show ?Q by simp
   13.67  next
   13.68    assume ?Q then show ?P by simp
   13.69  qed
   13.70  
   13.71  lemma is_unit_unit_factor:
   13.72    assumes "is_unit a" shows "unit_factor a = a"
   13.73 -proof - 
   13.74 +proof -
   13.75    from assms have "normalize a = 1" by (rule is_unit_normalize)
   13.76    moreover from unit_factor_mult_normalize have "unit_factor a * normalize a = a" .
   13.77    ultimately show ?thesis by simp
   13.78 @@ -1069,13 +1069,13 @@
   13.79      using \<open>a \<noteq> 0\<close> by simp
   13.80    ultimately show ?Q by simp
   13.81  qed
   13.82 -  
   13.83 +
   13.84  lemma div_normalize [simp]:
   13.85    "a div normalize a = unit_factor a"
   13.86  proof (cases "a = 0")
   13.87    case True then show ?thesis by simp
   13.88  next
   13.89 -  case False then have "normalize a \<noteq> 0" by simp 
   13.90 +  case False then have "normalize a \<noteq> 0" by simp
   13.91    with nonzero_mult_divide_cancel_right
   13.92    have "unit_factor a * normalize a div normalize a = unit_factor a" by blast
   13.93    then show ?thesis by simp
   13.94 @@ -1086,7 +1086,7 @@
   13.95  proof (cases "a = 0")
   13.96    case True then show ?thesis by simp
   13.97  next
   13.98 -  case False then have "unit_factor a \<noteq> 0" by simp 
   13.99 +  case False then have "unit_factor a \<noteq> 0" by simp
  13.100    with nonzero_mult_divide_cancel_left
  13.101    have "unit_factor a * normalize a div unit_factor a = normalize a" by blast
  13.102    then show ?thesis by simp
  13.103 @@ -1126,7 +1126,7 @@
  13.104      using False by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric])
  13.105    finally show ?thesis .
  13.106  qed
  13.107 - 
  13.108 +
  13.109  lemma unit_factor_idem [simp]:
  13.110    "unit_factor (unit_factor a) = unit_factor a"
  13.111    by (cases "a = 0") (auto intro: is_unit_unit_factor)
  13.112 @@ -1134,7 +1134,7 @@
  13.113  lemma normalize_unit_factor [simp]:
  13.114    "a \<noteq> 0 \<Longrightarrow> normalize (unit_factor a) = 1"
  13.115    by (rule is_unit_normalize) simp
  13.116 -  
  13.117 +
  13.118  lemma normalize_idem [simp]:
  13.119    "normalize (normalize a) = normalize a"
  13.120  proof (cases "a = 0")
  13.121 @@ -1257,7 +1257,7 @@
  13.122    proof (cases "a = 0 \<or> b = 0")
  13.123      case True with \<open>?P\<close> show ?thesis by auto
  13.124    next
  13.125 -    case False 
  13.126 +    case False
  13.127      then have "b dvd normalize b * unit_factor a" and "normalize b * unit_factor a dvd b"
  13.128        by (simp_all add: mult_unit_dvd_iff dvd_mult_unit_iff)
  13.129      with * show ?thesis by simp
  13.130 @@ -1277,7 +1277,7 @@
  13.131  
  13.132  end
  13.133  
  13.134 -class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +
  13.135 +class ordered_semiring = semiring + ordered_comm_monoid_add +
  13.136    assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
  13.137    assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
  13.138  begin
  13.139 @@ -1324,7 +1324,7 @@
  13.140  
  13.141  subclass ordered_cancel_semiring ..
  13.142  
  13.143 -subclass ordered_comm_monoid_add ..
  13.144 +subclass ordered_cancel_comm_monoid_add ..
  13.145  
  13.146  lemma mult_left_less_imp_less:
  13.147    "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
  13.148 @@ -1742,14 +1742,14 @@
  13.149  lemma add_diff_inverse: "~ a<b \<Longrightarrow> b + (a - b) = a"
  13.150    by simp
  13.151  
  13.152 -lemma add_le_imp_le_diff: 
  13.153 +lemma add_le_imp_le_diff:
  13.154    shows "i + k \<le> n \<Longrightarrow> i \<le> n - k"
  13.155    apply (subst add_le_cancel_right [where c=k, symmetric])
  13.156    apply (frule le_add_diff_inverse2)
  13.157    apply (simp only: add.assoc [symmetric])
  13.158    using add_implies_diff by fastforce
  13.159  
  13.160 -lemma add_le_add_imp_diff_le: 
  13.161 +lemma add_le_add_imp_diff_le:
  13.162    assumes a1: "i + k \<le> n"
  13.163        and a2: "n \<le> j + k"
  13.164    shows "\<lbrakk>i + k \<le> n; n \<le> j + k\<rbrakk> \<Longrightarrow> n - k \<le> j"
  13.165 @@ -2034,6 +2034,20 @@
  13.166  
  13.167  end
  13.168  
  13.169 +subsection \<open>Dioids\<close>
  13.170 +
  13.171 +text \<open>Dioids are the alternative extensions of semirings, a semiring can either be a ring or a dioid
  13.172 +but never both.\<close>
  13.173 +
  13.174 +class dioid = semiring_1 + canonically_ordered_monoid_add
  13.175 +begin
  13.176 +
  13.177 +subclass ordered_semiring
  13.178 +  proof qed (auto simp: le_iff_add distrib_left distrib_right)
  13.179 +
  13.180 +end
  13.181 +
  13.182 +
  13.183  hide_fact (open) comm_mult_left_mono comm_mult_strict_left_mono distrib
  13.184  
  13.185  code_identifier
    14.1 --- a/src/HOL/Series.thy	Tue Feb 09 09:21:10 2016 +0100
    14.2 +++ b/src/HOL/Series.thy	Wed Feb 10 18:43:19 2016 +0100
    14.3 @@ -211,22 +211,6 @@
    14.4  lemma suminf_nonneg: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 \<le> suminf f"
    14.5    using setsum_le_suminf[of 0] by simp
    14.6  
    14.7 -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"
    14.8 -  using
    14.9 -    setsum_le_suminf[of "Suc i"]
   14.10 -    add_strict_increasing[of "f i" "setsum f {..<n}" "setsum f {..<i}"]
   14.11 -    setsum_mono2[of "{..<i}" "{..<n}" f]
   14.12 -  by (auto simp: less_imp_le ac_simps)
   14.13 -
   14.14 -lemma setsum_less_suminf: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 < f m \<Longrightarrow> setsum f {..<n} < suminf f"
   14.15 -  using setsum_less_suminf2[of n n] by (simp add: less_imp_le)
   14.16 -
   14.17 -lemma suminf_pos2: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < f i \<Longrightarrow> 0 < suminf f"
   14.18 -  using setsum_less_suminf2[of 0 i] by simp
   14.19 -
   14.20 -lemma suminf_pos: "summable f \<Longrightarrow> \<forall>n. 0 < f n \<Longrightarrow> 0 < suminf f"
   14.21 -  using suminf_pos2[of 0] by (simp add: less_imp_le)
   14.22 -
   14.23  lemma suminf_le_const: "summable f \<Longrightarrow> (\<And>n. setsum f {..<n} \<le> x) \<Longrightarrow> suminf f \<le> x"
   14.24    by (metis LIMSEQ_le_const2 summable_LIMSEQ)
   14.25  
   14.26 @@ -244,8 +228,31 @@
   14.27      by (auto intro!: antisym)
   14.28  qed (metis suminf_zero fun_eq_iff)
   14.29  
   14.30 -lemma suminf_pos_iff: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
   14.31 -  using setsum_le_suminf[of 0] suminf_eq_zero_iff by (simp add: less_le)
   14.32 +end
   14.33 +
   14.34 +context
   14.35 +  fixes f :: "nat \<Rightarrow> 'a::{ordered_cancel_comm_monoid_add, linorder_topology}"
   14.36 +begin
   14.37 +
   14.38 +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"
   14.39 +  using
   14.40 +    setsum_le_suminf[of f "Suc i"]
   14.41 +    add_strict_increasing[of "f i" "setsum f {..<n}" "setsum f {..<i}"]
   14.42 +    setsum_mono2[of "{..<i}" "{..<n}" f]
   14.43 +  by (auto simp: less_imp_le ac_simps)
   14.44 +
   14.45 +lemma setsum_less_suminf: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 < f m \<Longrightarrow> setsum f {..<n} < suminf f"
   14.46 +  using setsum_less_suminf2[of n n] by (simp add: less_imp_le)
   14.47 +
   14.48 +lemma suminf_pos2: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < f i \<Longrightarrow> 0 < suminf f"
   14.49 +  using setsum_less_suminf2[of 0 i] by simp
   14.50 +
   14.51 +lemma suminf_pos: "summable f \<Longrightarrow> \<forall>n. 0 < f n \<Longrightarrow> 0 < suminf f"
   14.52 +  using suminf_pos2[of 0] by (simp add: less_imp_le)
   14.53 +
   14.54 +lemma suminf_pos_iff:
   14.55 +  "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
   14.56 +  using setsum_le_suminf[of f 0] suminf_eq_zero_iff[of f] by (simp add: less_le)
   14.57  
   14.58  end
   14.59  
    15.1 --- a/src/HOL/Set_Interval.thy	Tue Feb 09 09:21:10 2016 +0100
    15.2 +++ b/src/HOL/Set_Interval.thy	Wed Feb 10 18:43:19 2016 +0100
    15.3 @@ -1870,7 +1870,7 @@
    15.4  proof (cases "i \<le> j")
    15.5    case True
    15.6    then show ?thesis
    15.7 -    by (metis Nat.le_iff_add setprod_int_plus_eq)
    15.8 +    by (metis le_iff_add setprod_int_plus_eq)
    15.9  next
   15.10    case False
   15.11    then show ?thesis