# HG changeset patch
# User hoelzl
# Date 1455885650 -3600
# Node ID 85ed00c1fe7c94571194be4bd56d4da28d9c1f2e
# Parent  ace69956d01852f7d5992a97851473d2f96eec9b
generalize more theorems to support enat and ennreal

diff -r ace69956d018 -r 85ed00c1fe7c src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Fri Feb 12 16:09:07 2016 +0100
+++ b/src/HOL/Binomial.thy	Fri Feb 19 13:40:50 2016 +0100
@@ -28,7 +28,7 @@
 lemma of_nat_fact [simp]:
   "of_nat (fact n) = fact n"
   by (induct n) (auto simp add: algebra_simps of_nat_mult)
- 
+
 lemma of_int_fact [simp]:
   "of_int (fact n) = fact n"
 proof -
@@ -56,22 +56,22 @@
 context
   assumes "SORT_CONSTRAINT('a::linordered_semidom)"
 begin
-  
+
   lemma fact_mono: "m \<le> n \<Longrightarrow> fact m \<le> (fact n :: 'a)"
     by (metis of_nat_fact of_nat_le_iff fact_mono_nat)
-  
+
   lemma fact_ge_1 [simp]: "fact n \<ge> (1 :: 'a)"
     by (metis le0 fact.simps(1) fact_mono)
-  
+
   lemma fact_gt_zero [simp]: "fact n > (0 :: 'a)"
     using fact_ge_1 less_le_trans zero_less_one by blast
-  
+
   lemma fact_ge_zero [simp]: "fact n \<ge> (0 :: 'a)"
     by (simp add: less_imp_le)
 
   lemma fact_not_neg [simp]: "~ (fact n < (0 :: 'a))"
     by (simp add: not_less_iff_gr_or_eq)
-    
+
   lemma fact_le_power:
       "fact n \<le> (of_nat (n^n) ::'a)"
   proof (induct n)
@@ -86,7 +86,7 @@
       by (metis of_nat_mult order_refl power_Suc)
     finally show ?case .
   qed simp
-  
+
 end
 
 text\<open>Note that @{term "fact 0 = fact 1"}\<close>
@@ -100,7 +100,7 @@
 lemma fact_ge_Suc_0_nat [simp]: "fact n \<ge> Suc 0"
   by (metis One_nat_def fact_ge_1)
 
-lemma dvd_fact: 
+lemma dvd_fact:
   shows "1 \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> m dvd fact n"
   by (induct n) (auto simp: dvdI le_Suc_eq)
 
@@ -112,7 +112,7 @@
 
 lemma fact_altdef: "fact n = (\<Prod>i=1..n. of_nat i)"
   by (induct n) (auto simp: atLeastAtMostSuc_conv)
-  
+
 lemma fact_altdef': "fact n = of_nat (\<Prod>{1..n})"
   by (subst fact_altdef_nat [symmetric]) simp
 
@@ -145,7 +145,7 @@
   from this \<open>m = n + d\<close> show ?thesis by simp
 qed
 
-lemma fact_num_eq_if: 
+lemma fact_num_eq_if:
     "fact m = (if m=0 then 1 else of_nat m * fact (m - 1))"
 by (cases m) auto
 
@@ -402,20 +402,20 @@
 lemma sum_choose_upper: "(\<Sum>k=0..n. k choose m) = Suc n choose Suc m"
   by (induct n) auto
 
-lemma choose_alternating_sum: 
+lemma choose_alternating_sum:
   "n > 0 \<Longrightarrow> (\<Sum>i\<le>n. (-1)^i * of_nat (n choose i)) = (0 :: 'a :: comm_ring_1)"
   using binomial_ring[of "-1 :: 'a" 1 n] by (simp add: atLeast0AtMost mult_of_nat_commute zero_power)
 
 lemma choose_even_sum:
   assumes "n > 0"
   shows   "2 * (\<Sum>i\<le>n. if even i then of_nat (n choose i) else 0) = (2 ^ n :: 'a :: comm_ring_1)"
-proof - 
+proof -
   have "2 ^ n = (\<Sum>i\<le>n. of_nat (n choose i)) + (\<Sum>i\<le>n. (-1) ^ i * of_nat (n choose i) :: 'a)"
     using choose_row_sum[of n]
     by (simp add: choose_alternating_sum assms atLeast0AtMost of_nat_setsum[symmetric] of_nat_power)
   also have "\<dots> = (\<Sum>i\<le>n. of_nat (n choose i) + (-1) ^ i * of_nat (n choose i))"
     by (simp add: setsum.distrib)
-  also have "\<dots> = 2 * (\<Sum>i\<le>n. if even i then of_nat (n choose i) else 0)" 
+  also have "\<dots> = 2 * (\<Sum>i\<le>n. if even i then of_nat (n choose i) else 0)"
     by (subst setsum_right_distrib, intro setsum.cong) simp_all
   finally show ?thesis ..
 qed
@@ -423,13 +423,13 @@
 lemma choose_odd_sum:
   assumes "n > 0"
   shows   "2 * (\<Sum>i\<le>n. if odd i then of_nat (n choose i) else 0) = (2 ^ n :: 'a :: comm_ring_1)"
-proof - 
+proof -
   have "2 ^ n = (\<Sum>i\<le>n. of_nat (n choose i)) - (\<Sum>i\<le>n. (-1) ^ i * of_nat (n choose i) :: 'a)"
     using choose_row_sum[of n]
     by (simp add: choose_alternating_sum assms atLeast0AtMost of_nat_setsum[symmetric] of_nat_power)
   also have "\<dots> = (\<Sum>i\<le>n. of_nat (n choose i) - (-1) ^ i * of_nat (n choose i))"
     by (simp add: setsum_subtractf)
-  also have "\<dots> = 2 * (\<Sum>i\<le>n. if odd i then of_nat (n choose i) else 0)" 
+  also have "\<dots> = 2 * (\<Sum>i\<le>n. if odd i then of_nat (n choose i) else 0)"
     by (subst setsum_right_distrib, intro setsum.cong) simp_all
   finally show ?thesis ..
 qed
@@ -473,7 +473,7 @@
 
 lemma pochhammer_Suc_setprod: "pochhammer a (Suc n) = setprod (\<lambda>n. a + of_nat n) {0 .. n}"
   by (simp add: pochhammer_def)
-  
+
 lemma pochhammer_of_nat: "pochhammer (of_nat x) n = of_nat (pochhammer x n)"
   by (simp add: pochhammer_def of_nat_setprod)
 
@@ -525,10 +525,10 @@
 lemma pochhammer_rec': "pochhammer z (Suc n) = (z + of_nat n) * pochhammer z n"
 proof (induction n arbitrary: z)
   case (Suc n z)
-  have "pochhammer z (Suc (Suc n)) = z * pochhammer (z + 1) (Suc n)" 
+  have "pochhammer z (Suc (Suc n)) = z * pochhammer (z + 1) (Suc n)"
     by (simp add: pochhammer_rec)
   also note Suc
-  also have "z * ((z + 1 + of_nat n) * pochhammer (z + 1) n) = 
+  also have "z * ((z + 1 + of_nat n) * pochhammer (z + 1) n) =
                (z + of_nat (Suc n)) * pochhammer z (Suc n)"
     by (simp_all add: pochhammer_rec algebra_simps)
   finally show ?case .
@@ -621,11 +621,11 @@
   unfolding pochhammer_minus
   by (simp add: of_nat_diff pochhammer_fact)
 
-lemma pochhammer_product': 
+lemma pochhammer_product':
   "pochhammer z (n + m) = pochhammer z n * pochhammer (z + of_nat n) m"
 proof (induction n arbitrary: z)
   case (Suc n z)
-  have "pochhammer z (Suc n) * pochhammer (z + of_nat (Suc n)) m = 
+  have "pochhammer z (Suc n) * pochhammer (z + of_nat (Suc n)) m =
             z * (pochhammer (z + 1) n * pochhammer (z + 1 + of_nat n) m)"
     by (simp add: pochhammer_rec ac_simps)
   also note Suc[symmetric]
@@ -634,7 +634,7 @@
   finally show ?case by simp
 qed simp
 
-lemma pochhammer_product: 
+lemma pochhammer_product:
   "m \<le> n \<Longrightarrow> pochhammer z n = pochhammer z m * pochhammer (z + of_nat m) (n - m)"
   using pochhammer_product'[of z m "n - m"] by simp
 
@@ -645,7 +645,7 @@
   case (Suc n)
   def n' \<equiv> "Suc n"
   have "pochhammer z (Suc n') * pochhammer (z + 1 / 2) (Suc n') =
-          (pochhammer z n' * pochhammer (z + 1 / 2) n') * 
+          (pochhammer z n' * pochhammer (z + 1 / 2) n') *
           ((z + of_nat n') * (z + 1/2 + of_nat n'))" (is "_ = _ * ?A")
      by (simp_all add: pochhammer_rec' mult_ac)
   also have "?A = (z + of_nat (Suc (2 * n + 1)) / 2) * (z + of_nat (Suc (Suc (2 * n + 1))) / 2)"
@@ -661,7 +661,7 @@
   shows "pochhammer (2 * z) (2 * n) = of_nat (2^(2*n)) * pochhammer z n * pochhammer (z+1/2) n"
 proof (induction n)
   case (Suc n)
-  have "pochhammer (2 * z) (2 * (Suc n)) = pochhammer (2 * z) (2 * n) * 
+  have "pochhammer (2 * z) (2 * (Suc n)) = pochhammer (2 * z) (2 * n) *
           (2 * (z + of_nat n)) * (2 * (z + of_nat n) + 1)"
     by (simp add: pochhammer_rec' ac_simps of_nat_mult)
   also note Suc
@@ -673,7 +673,7 @@
 qed simp
 
 lemma pochhammer_absorb_comp:
-  "((r :: 'a :: comm_ring_1) - of_nat k) * pochhammer (- r) k = r * pochhammer (-r + 1) k" 
+  "((r :: 'a :: comm_ring_1) - of_nat k) * pochhammer (- r) k = r * pochhammer (-r + 1) k"
   (is "?lhs = ?rhs")
 proof -
   have "?lhs = -pochhammer (-r) (Suc k)" by (subst pochhammer_rec') (simp add: algebra_simps)
@@ -714,7 +714,7 @@
   finally show ?thesis by simp
 qed
 
-lemma binomial_gbinomial: 
+lemma binomial_gbinomial:
     "of_nat (n choose k) = (of_nat n gchoose k :: 'a::field_char_0)"
 proof -
   { assume kn: "k > n"
@@ -741,7 +741,7 @@
     have ?thesis using kn
       apply (simp add: binomial_fact[OF kn, where ?'a = 'a]
         gbinomial_pochhammer field_simps pochhammer_Suc_setprod)
-      apply (simp add: pochhammer_Suc_setprod fact_altdef h 
+      apply (simp add: pochhammer_Suc_setprod fact_altdef h
         of_nat_setprod setprod.distrib[symmetric] eq' del: One_nat_def power_Suc)
       unfolding setprod.union_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h]
       unfolding mult.assoc
@@ -817,19 +817,19 @@
         (a gchoose Suc h) * (fact (Suc (Suc h))) +
         (a gchoose Suc (Suc h)) * (fact (Suc (Suc h)))"
     by (simp add: Suc field_simps del: fact.simps)
-  also have "... = (a gchoose Suc h) * of_nat (Suc (Suc h) * fact (Suc h)) + 
+  also have "... = (a gchoose Suc h) * of_nat (Suc (Suc h) * fact (Suc h)) +
                    (\<Prod>i = 0..Suc h. a - of_nat i)"
     by (metis fact.simps(2) gbinomial_mult_fact' of_nat_fact of_nat_id)
-  also have "... = (fact (Suc h) * (a gchoose Suc h)) * of_nat (Suc (Suc h)) + 
+  also have "... = (fact (Suc h) * (a gchoose Suc h)) * of_nat (Suc (Suc h)) +
                    (\<Prod>i = 0..Suc h. a - of_nat i)"
     by (simp only: fact.simps(2) mult.commute mult.left_commute of_nat_fact of_nat_id of_nat_mult)
-  also have "... =  of_nat (Suc (Suc h)) * (\<Prod>i = 0..h. a - of_nat i) + 
+  also have "... =  of_nat (Suc (Suc h)) * (\<Prod>i = 0..h. a - of_nat i) +
                     (\<Prod>i = 0..Suc h. a - of_nat i)"
     by (metis gbinomial_mult_fact mult.commute)
   also have "... = (\<Prod>i = 0..Suc h. a - of_nat i) +
                    (of_nat h * (\<Prod>i = 0..h. a - of_nat i) + 2 * (\<Prod>i = 0..h. a - of_nat i))"
     by (simp add: field_simps)
-  also have "... = 
+  also have "... =
     ((a gchoose Suc h) * (fact (Suc h)) * of_nat (Suc k)) + (\<Prod>i\<in>{0::nat..Suc h}. a - of_nat i)"
     unfolding gbinomial_mult_fact'
     by (simp add: comm_semiring_class.distrib field_simps Suc)
@@ -842,7 +842,7 @@
   also have "\<dots> = (fact (Suc k)) * ((a + 1) gchoose (Suc k))"
     unfolding gbinomial_mult_fact ..
   finally show ?thesis
-    by (metis fact_nonzero mult_cancel_left) 
+    by (metis fact_nonzero mult_cancel_left)
 qed
 
 lemma gbinomial_reduce_nat:
@@ -887,7 +887,7 @@
   case (Suc m)
   have "(\<Sum>i\<le>n. i * (n choose i)) = (\<Sum>i\<le>Suc m. i * (Suc m choose i))" by (simp add: Suc)
   also have "... = Suc m * 2 ^ m"
-    by (simp only: setsum_atMost_Suc_shift Suc_times_binomial setsum_right_distrib[symmetric]) 
+    by (simp only: setsum_atMost_Suc_shift Suc_times_binomial setsum_right_distrib[symmetric])
        (simp add: choose_row_sum')
   finally show ?thesis using Suc by simp
 qed simp_all
@@ -898,7 +898,7 @@
 proof (cases n)
   case (Suc m)
   with assms have "m > 0" by simp
-  have "(\<Sum>i\<le>n. (-1) ^ i * of_nat i * of_nat (n choose i) :: 'a) = 
+  have "(\<Sum>i\<le>n. (-1) ^ i * of_nat i * of_nat (n choose i) :: 'a) =
             (\<Sum>i\<le>Suc m. (-1) ^ i * of_nat i * of_nat (Suc m choose i))" by (simp add: Suc)
   also have "... = (\<Sum>i\<le>m. (-1) ^ (Suc i) * of_nat (Suc i * (Suc m choose Suc i)))"
     by (simp only: setsum_atMost_Suc_shift setsum_right_distrib[symmetric] of_nat_mult mult_ac) simp
@@ -940,7 +940,7 @@
   also have "(\<Sum>i\<le>n. of_nat (n choose i) * pochhammer a (Suc i) * pochhammer b (n - i)) =
                a * pochhammer ((a + 1) + b) n"
     by (subst Suc) (simp add: setsum_right_distrib pochhammer_rec mult_ac)
-  also have "(\<Sum>i\<le>n. of_nat (n choose Suc i) * pochhammer a (Suc i) * pochhammer b (n - i)) + pochhammer b (Suc n) = 
+  also have "(\<Sum>i\<le>n. of_nat (n choose Suc i) * pochhammer a (Suc i) * pochhammer b (n - i)) + pochhammer b (Suc n) =
                (\<Sum>i=0..Suc n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n - i))"
     by (subst setsum_head_Suc, simp, subst setsum_shift_bounds_cl_Suc_ivl) (simp add: atLeast0AtMost)
   also have "... = (\<Sum>i\<le>n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n - i))"
@@ -1010,7 +1010,7 @@
   "of_nat (Suc b) * ((a + 1) gchoose (Suc b)) = (a + 1) * (a gchoose b)"
 proof (cases b)
   case (Suc b)
-  hence "((a + 1) gchoose (Suc (Suc b))) = 
+  hence "((a + 1) gchoose (Suc (Suc b))) =
              (\<Prod>i = 0..Suc b. a + (1 - of_nat i)) / fact (b + 2)"
     by (simp add: field_simps gbinomial_def)
   also have "(\<Prod>i = 0..Suc b. a + (1 - of_nat i)) = (a + 1) * (\<Prod>i = 0..b. a - of_nat i)"
@@ -1024,7 +1024,7 @@
   "((a + 1) gchoose (Suc b)) = (a + 1) / of_nat (Suc b) * (a gchoose b)"
 proof (cases b)
   case (Suc b)
-  hence "((a + 1) gchoose (Suc (Suc b))) = 
+  hence "((a + 1) gchoose (Suc (Suc b))) =
              (\<Prod>i = 0..Suc b. a + (1 - of_nat i)) / fact (b + 2)"
     by (simp add: field_simps gbinomial_def)
   also have "(\<Prod>i = 0..Suc b. a + (1 - of_nat i)) = (a + 1) * (\<Prod>i = 0..b. a - of_nat i)"
@@ -1045,9 +1045,9 @@
 text \<open>The absorption identity (equation 5.5 \cite[p.~157]{GKP}):\[
 {r \choose k} = \frac{r}{k}{r - 1 \choose k - 1},\quad \textnormal{integer } k \neq 0.
 \]\<close>
-lemma gbinomial_absorption': 
+lemma gbinomial_absorption':
   "k > 0 \<Longrightarrow> (r gchoose k) = (r / of_nat(k)) * (r - 1 gchoose (k - 1))"
-  using gbinomial_rec[of "r - 1" "k - 1"] 
+  using gbinomial_rec[of "r - 1" "k - 1"]
   by (simp_all add: gbinomial_rec field_simps del: of_nat_Suc)
 
 text \<open>The absorption identity is written in the following form to avoid
@@ -1096,7 +1096,7 @@
   summation formula, operating on both indices:\[
   \sum\limits_{k \leq n}{r + k \choose k} = {r + n + 1 \choose n},
    \quad \textnormal{integer } n.
-  \] 
+  \]
 \<close>
 lemma gbinomial_parallel_sum:
 "(\<Sum>k\<le>n. (r + of_nat k) gchoose k) = (r + of_nat n + 1) gchoose n"
@@ -1108,7 +1108,7 @@
 subsection \<open>Summation on the upper index\<close>
 text \<open>
   Another summation formula is equation 5.10 of the reference material \cite[p.~160]{GKP},
-  aptly named \emph{summation on the upper index}:\[\sum_{0 \leq k \leq n} {k \choose m} = 
+  aptly named \emph{summation on the upper index}:\[\sum_{0 \leq k \leq n} {k \choose m} =
   {n + 1 \choose m + 1}, \quad \textnormal{integers } m, n \geq 0.\]
 \<close>
 lemma gbinomial_sum_up_index:
@@ -1121,7 +1121,7 @@
   thus ?case using gbinomial_Suc_Suc[of "of_nat (Suc n) :: 'a" m] by (simp add: add_ac)
 qed
 
-lemma gbinomial_index_swap: 
+lemma gbinomial_index_swap:
   "((-1) ^ m) * ((- (of_nat n) - 1) gchoose m) = ((-1) ^ n) * ((- (of_nat m) - 1) gchoose n)"
   (is "?lhs = ?rhs")
 proof -
@@ -1132,7 +1132,7 @@
   finally show ?thesis .
 qed
 
-lemma gbinomial_sum_lower_neg: 
+lemma gbinomial_sum_lower_neg:
   "(\<Sum>k\<le>m. (r gchoose k) * (- 1) ^ k) = (- 1) ^ m * (r - 1 gchoose m)" (is "?lhs = ?rhs")
 proof -
   have "?lhs = (\<Sum>k\<le>m. -(r + 1) + of_nat k gchoose k)"
@@ -1146,7 +1146,7 @@
 "(\<Sum>k\<le>m. (r gchoose k) * ((r / 2) - of_nat k)) = ((of_nat m + 1)/2) * (r gchoose (m + 1))"
 proof (induction m)
   case (Suc mm)
-  hence "(\<Sum>k\<le>Suc mm. (r gchoose k) * (r / 2 - of_nat k)) = 
+  hence "(\<Sum>k\<le>Suc mm. (r gchoose k) * (r / 2 - of_nat k)) =
              (r - of_nat (Suc mm)) * (r gchoose Suc mm) / 2" by (simp add: field_simps)
   also have "\<dots> = r * (r - 1 gchoose Suc mm) / 2" by (subst gbinomial_absorb_comp) (rule refl)
   also have "\<dots> = (of_nat (Suc mm) + 1) / 2 * (r gchoose (Suc mm + 1))"
@@ -1175,10 +1175,10 @@
   also have "\<dots> = (\<Sum>k=0..mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm - k))
                   + (\<Sum>k=0..mm. (of_nat mm + r gchoose k) * x^(Suc k) * y^(mm - k))"
     by (subst setsum.distrib [symmetric]) (simp add: algebra_simps)
-  also have "(\<Sum>k=0..mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm - k)) = 
+  also have "(\<Sum>k=0..mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm - k)) =
                (\<Sum>k<Suc mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm - k))"
     by (simp only: atLeast0AtMost lessThan_Suc_atMost)
-  also have "\<dots> = (\<Sum>k<mm. (of_nat mm + r gchoose Suc k) * x^(Suc k) * y^(mm-k)) 
+  also have "\<dots> = (\<Sum>k<mm. (of_nat mm + r gchoose Suc k) * x^(Suc k) * y^(mm-k))
                       + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)" (is "_ = ?A + ?B")
     by (subst setsum_lessThan_Suc) simp
   also have "?A = (\<Sum>k=1..mm. (of_nat mm + r gchoose k) * x^k * y^(mm - k + 1))"
@@ -1188,17 +1188,17 @@
     thus "(of_nat mm + r gchoose Suc k) * x ^ Suc k * y ^ (mm - k) =
             (of_nat mm + r gchoose Suc k) * x ^ Suc k * y ^ (mm - Suc k + 1)" by (simp only:)
   qed
-  also have "\<dots> + ?B = y * (\<Sum>k=1..mm. (G mm k)) + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)" 
+  also have "\<dots> + ?B = y * (\<Sum>k=1..mm. (G mm k)) + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)"
     unfolding G_def by (subst setsum_right_distrib) (simp add: algebra_simps)
   also have "(\<Sum>k=0..mm. (of_nat mm + r gchoose k) * x^(Suc k) * y^(mm - k)) = x * (S mm)"
       unfolding S_def by (subst setsum_right_distrib) (simp add: atLeast0AtMost algebra_simps)
   also have "(G (Suc mm) 0) = y * (G mm 0)" by (simp add: G_def)
-  finally have "S (Suc mm) = y * ((G mm 0) + (\<Sum>k=1..mm. (G mm k))) 
+  finally have "S (Suc mm) = y * ((G mm 0) + (\<Sum>k=1..mm. (G mm k)))
                 + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm) + x * (S mm)"
     by (simp add: ring_distribs)
-  also have "(G mm 0) + (\<Sum>k=1..mm. (G mm k)) = S mm" 
+  also have "(G mm 0) + (\<Sum>k=1..mm. (G mm k)) = S mm"
     by (simp add: setsum_head_Suc[symmetric] SG_def atLeast0AtMost)
-  finally have "S (Suc mm) = (x + y) * (S mm) + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)" 
+  finally have "S (Suc mm) = (x + y) * (S mm) + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)"
     by (simp add: algebra_simps)
   also have "(of_nat mm + r gchoose (Suc mm)) = (-1) ^ (Suc mm) * (-r gchoose (Suc mm))"
     by (subst gbinomial_negated_upper) simp
@@ -1208,13 +1208,13 @@
     unfolding S_def by (subst Suc.IH) simp
   also have "(x + y) * ?rhs mm = (\<Sum>n\<le>mm. ((- r gchoose n) * (- x) ^ n * (x + y) ^ (Suc mm - n)))"
     by (subst setsum_right_distrib, rule setsum.cong) (simp_all add: Suc_diff_le)
-  also have "\<dots> + (-r gchoose (Suc mm)) * (-x)^Suc mm = 
+  also have "\<dots> + (-r gchoose (Suc mm)) * (-x)^Suc mm =
                  (\<Sum>n\<le>Suc mm. (- r gchoose n) * (- x) ^ n * (x + y) ^ (Suc mm - n))" by simp
   finally show ?case unfolding S_def .
 qed simp_all
 
 lemma gbinomial_partial_sum_poly_xpos:
-  "(\<Sum>k\<le>m. (of_nat m + r gchoose k) * x^k * y^(m-k)) = 
+  "(\<Sum>k\<le>m. (of_nat m + r gchoose k) * x^k * y^(m-k)) =
      (\<Sum>k\<le>m. (of_nat k + r - 1 gchoose k) * x^k * (x + y)^(m-k))"
   apply (subst gbinomial_partial_sum_poly)
   apply (subst gbinomial_negated_upper)
@@ -1222,7 +1222,7 @@
   apply (simp add: power_mult_distrib [symmetric])
   done
 
-lemma setsum_nat_symmetry: 
+lemma setsum_nat_symmetry:
   "(\<Sum>k = 0..(m::nat). f k) = (\<Sum>k = 0..m. f (m - k))"
   by (rule setsum.reindex_bij_witness[where i="\<lambda>i. m - i" and j="\<lambda>i. m - i"]) auto
 
@@ -1247,7 +1247,7 @@
 lemma gbinomial_r_part_sum:
   "(\<Sum>k\<le>m. (2 * (of_nat m) + 1 gchoose k)) = 2 ^ (2 * m)" (is "?lhs = ?rhs")
 proof -
-  have "?lhs = of_nat (\<Sum>k\<le>m. (2 * m + 1) choose k)" 
+  have "?lhs = of_nat (\<Sum>k\<le>m. (2 * m + 1) choose k)"
     by (simp add: binomial_gbinomial of_nat_mult add_ac of_nat_setsum)
   also have "\<dots> = of_nat (2 ^ (2 * m))" by (subst binomial_r_part_sum) (rule refl)
   finally show ?thesis by (simp add: of_nat_power)
@@ -1270,7 +1270,7 @@
   assumes "k \<le> m"
   shows   "(r gchoose m) * (of_nat m gchoose k) = (r gchoose k) * (r - of_nat k gchoose (m - k))"
 proof -
-  have "(r gchoose m) * (of_nat m gchoose k) = 
+  have "(r gchoose m) * (of_nat m gchoose k) =
             (r gchoose m) * fact m / (fact k * fact (m - k))"
     using assms by (simp add: binomial_gbinomial [symmetric] binomial_fact)
   also have "\<dots> = (r gchoose k) * (r - of_nat k gchoose (m - k))" using assms
@@ -1315,7 +1315,7 @@
   apply (auto simp: of_nat_mult)
   done
 
-lemma fact_fact_dvd_fact: 
+lemma fact_fact_dvd_fact:
     "fact k * fact n dvd (fact (k+n) :: 'a :: {semiring_div,linordered_semidom})"
 by (metis add.commute add_diff_cancel_left' choose_dvd le_add2)
 
@@ -1568,12 +1568,12 @@
 qed
 
 lemma pochhammer_code [code]:
-  "pochhammer a n = (if n = 0 then 1 else 
+  "pochhammer a n = (if n = 0 then 1 else
        fold_atLeastAtMost_nat (\<lambda>n acc. (a + of_nat n) * acc) 0 (n - 1) 1)"
   by (simp add: setprod_atLeastAtMost_code pochhammer_def)
 
 lemma gbinomial_code [code]:
-  "a gchoose n = (if n = 0 then 1 else 
+  "a gchoose n = (if n = 0 then 1 else
      fold_atLeastAtMost_nat (\<lambda>n acc. (a - of_nat n) * acc) 0 (n - 1) 1 / fact n)"
   by (simp add: setprod_atLeastAtMost_code gbinomial_def)
 
@@ -1593,7 +1593,7 @@
       by (simp add: setprod.union_disjoint fact_altdef_nat)
   }
   thus ?thesis by (auto simp: binomial_altdef_nat mult_ac setprod_atLeastAtMost_code)
-qed 
+qed
 *)
 
 end
diff -r ace69956d018 -r 85ed00c1fe7c src/HOL/Decision_Procs/Polynomial_List.thy
--- a/src/HOL/Decision_Procs/Polynomial_List.thy	Fri Feb 12 16:09:07 2016 +0100
+++ b/src/HOL/Decision_Procs/Polynomial_List.thy	Fri Feb 19 13:40:50 2016 +0100
@@ -572,13 +572,7 @@
   done
 
 lemma (in comm_semiring_1) poly_divides_exp: "m \<le> n \<Longrightarrow> (p %^ m) divides (p %^ n)"
-  apply (auto simp add: le_iff_add)
-  apply (induct_tac k)
-  apply (rule_tac [2] poly_divides_trans)
-  apply (auto simp add: divides_def)
-  apply (rule_tac x = p in exI)
-  apply (auto simp add: poly_mult fun_eq_iff ac_simps)
-  done
+  by (auto simp: le_iff_add divides_def poly_exp_add fun_eq_iff)
 
 lemma (in comm_semiring_1) poly_exp_divides: "(p %^ n) divides q \<Longrightarrow> m \<le> n \<Longrightarrow> (p %^ m) divides q"
   by (blast intro: poly_divides_exp poly_divides_trans)
diff -r ace69956d018 -r 85ed00c1fe7c src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Fri Feb 12 16:09:07 2016 +0100
+++ b/src/HOL/Filter.thy	Fri Feb 19 13:40:50 2016 +0100
@@ -490,7 +490,7 @@
   shows "\<forall>\<^sub>F x in \<Sqinter>i\<in>I. F' i. T P x"
 proof -
   from * obtain X where "finite X" "X \<subseteq> I" "\<forall>\<^sub>F x in \<Sqinter>i\<in>X. F i. P x"
-    unfolding eventually_INF[of _ I] by auto
+    unfolding eventually_INF[of _ _ I] by auto
   moreover then have "eventually (T P) (INFIMUM X F')"
     apply (induction X arbitrary: P)
     apply (auto simp: eventually_inf T2)
diff -r ace69956d018 -r 85ed00c1fe7c src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Fri Feb 12 16:09:07 2016 +0100
+++ b/src/HOL/Groups.thy	Fri Feb 19 13:40:50 2016 +0100
@@ -753,6 +753,13 @@
 end
 
 class strict_ordered_comm_monoid_add = comm_monoid_add + strict_ordered_ab_semigroup_add
+begin
+
+lemma pos_add_strict:
+  shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
+  using add_strict_mono [of 0 a b c] by simp
+
+end
 
 class ordered_cancel_comm_monoid_add = ordered_comm_monoid_add + cancel_ab_semigroup_add
 begin
@@ -1311,15 +1318,37 @@
   assumes le_iff_add: "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)"
 begin
 
-lemma zero_le: "0 \<le> x"
+lemma zero_le[simp]: "0 \<le> x"
   by (auto simp: le_iff_add)
 
+lemma le_zero_eq[simp]: "n \<le> 0 \<longleftrightarrow> n = 0"
+  by (auto intro: antisym)
+
+lemma not_less_zero[simp]: "\<not> n < 0"
+  by (auto simp: less_le)
+
+lemma zero_less_iff_neq_zero: "(0 < n) \<longleftrightarrow> (n \<noteq> 0)"
+  by (auto simp: less_le)
+
+text \<open>This theorem is useful with \<open>blast\<close>\<close>
+lemma gr_zeroI: "(n = 0 \<Longrightarrow> False) \<Longrightarrow> 0 < n"
+  by (rule zero_less_iff_neq_zero[THEN iffD2]) iprover
+
+lemma not_gr_zero[simp]: "(\<not> (0 < n)) \<longleftrightarrow> (n = 0)"
+  by (simp add: zero_less_iff_neq_zero)
+
 subclass ordered_comm_monoid_add
   proof qed (auto simp: le_iff_add add_ac)
 
 lemma add_eq_0_iff_both_eq_0: "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   by (intro add_nonneg_eq_0_iff zero_le)
 
+lemma gr_implies_not_zero: "m < n \<Longrightarrow> n \<noteq> 0"
+  using add_eq_0_iff_both_eq_0[of m] by (auto simp: le_iff_add less_le)
+
+lemmas zero_order = zero_le le_zero_eq not_less_zero zero_less_iff_neq_zero not_gr_zero
+  -- \<open>This should be attributed with \<open>[iff]\<close>, but then \<open>blast\<close> fails in \<open>Set\<close>.\<close>
+
 end
 
 class ordered_cancel_comm_monoid_diff =
diff -r ace69956d018 -r 85ed00c1fe7c src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Fri Feb 12 16:09:07 2016 +0100
+++ b/src/HOL/Groups_Big.thy	Fri Feb 19 13:40:50 2016 +0100
@@ -1195,6 +1195,6 @@
 
 lemma setprod_pos_nat_iff [simp]:
   "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])
+  using setprod_zero_iff by (simp del: neq0_conv add: zero_less_iff_neq_zero)
 
 end
diff -r ace69956d018 -r 85ed00c1fe7c src/HOL/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy	Fri Feb 12 16:09:07 2016 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy	Fri Feb 19 13:40:50 2016 +0100
@@ -172,26 +172,6 @@
 
 text{* ACC for abstract states, via measure functions. *}
 
-(*FIXME mv*)
-lemma setsum_strict_mono1:
-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"
-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})"
-    by(simp add:insert_absorb[OF `a:A`])
-  also have "\<dots> = setsum f (A-{a}) + setsum f {a}"
-    using `finite A` by(subst setsum.union_disjoint) auto
-  also have "setsum f (A-{a}) \<le> setsum g (A-{a})"
-    by(rule setsum_mono)(simp add: assms(2))
-  also have "setsum f {a} < setsum g {a}" using a by simp
-  also have "setsum g (A - {a}) + setsum g {a} = setsum g((A-{a}) \<union> {a})"
-    using `finite A` by(subst setsum.union_disjoint[symmetric]) auto
-  also have "\<dots> = setsum g A" by(simp add:insert_absorb[OF `a:A`])
-  finally show ?thesis by (metis add_right_mono add_strict_left_mono)
-qed
-
 lemma measure_st: assumes "(strict{(x,y::'a::SL_top). x \<sqsubseteq> y})^-1 <= measure m"
 and "\<forall>x y::'a::SL_top. x \<sqsubseteq> y \<and> y \<sqsubseteq> x \<longrightarrow> m x = m y"
 shows "(strict{(S,S'::'a::SL_top st). S \<sqsubseteq> S'})^-1 \<subseteq>
@@ -223,7 +203,7 @@
         by (fastforce simp: le_st_def lookup_def)
       have "(\<Sum>y\<in>?Y'\<inter>?X. m(?g y)+1) < (\<Sum>y\<in>?Y'\<inter>?X. m(?f y)+1)"
         using `u:?X` `u:?Y'` `m(?g u) < m(?f u)`
-        by(fastforce intro!: setsum_strict_mono1[OF _ 1])
+        by(fastforce intro!: setsum_strict_mono_ex1[OF _ 1])
       also have "\<dots> \<le> (\<Sum>y\<in>?X'. m(?f y)+1)"
         by(simp add: setsum_mono3[OF _ `?Y'\<inter>?X <= ?X'`])
       finally show ?thesis .
diff -r ace69956d018 -r 85ed00c1fe7c src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy	Fri Feb 12 16:09:07 2016 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy	Fri Feb 19 13:40:50 2016 +0100
@@ -340,7 +340,7 @@
     proof cases
       assume "x : ?Y"
       have "?L < (\<Sum>x\<in>?X\<inter>?Y. m_ivl(?f x))"
-      proof(rule setsum_strict_mono1, simp)
+      proof(rule setsum_strict_mono_ex1, simp)
         show "\<forall>x\<in>?X\<inter>?Y. m_ivl(?f x \<nabla> ?g x) \<le> m_ivl (?f x)"
           by (metis m_ivl_anti_mono widen1)
       next
@@ -395,7 +395,7 @@
     by(auto simp: le_st_def narrow_st_def lookup_def intro: n_ivl_narrow
             split: if_splits)
   have "(\<Sum>x\<in>X. n_ivl(lookup (S1 \<triangle> S2) x)) < (\<Sum>x\<in>X. n_ivl(lookup S1 x))"
-    apply(rule setsum_strict_mono1[OF `finite X`]) using 1 2 by blast+
+    apply(rule setsum_strict_mono_ex1[OF `finite X`]) using 1 2 by blast+
   thus ?thesis by(simp add: n_st_def)
 qed
 
@@ -501,7 +501,7 @@
 apply(subgoal_tac "length(annos c') = length(annos c)")
 prefer 2 apply (simp add: size_annos_same2)
 apply (auto)
-apply(rule setsum_strict_mono1)
+apply(rule setsum_strict_mono_ex1)
 apply simp
 apply (clarsimp)
 apply(erule m_o_anti_mono)
@@ -522,7 +522,7 @@
 apply(subgoal_tac "length(annos c') = length(annos c)")
 prefer 2 apply (simp add: size_annos_same2)
 apply (auto)
-apply(rule setsum_strict_mono1)
+apply(rule setsum_strict_mono_ex1)
 apply simp
 apply (clarsimp)
 apply(rule n_o_mono)
diff -r ace69956d018 -r 85ed00c1fe7c src/HOL/Library/Extended_Nat.thy
--- a/src/HOL/Library/Extended_Nat.thy	Fri Feb 12 16:09:07 2016 +0100
+++ b/src/HOL/Library/Extended_Nat.thy	Fri Feb 19 13:40:50 2016 +0100
@@ -12,6 +12,18 @@
 class infinity =
   fixes infinity :: "'a"  ("\<infinity>")
 
+context
+  fixes f :: "nat \<Rightarrow> 'a::{canonically_ordered_monoid_add, linorder_topology, complete_linorder}"
+begin
+
+lemma sums_SUP[simp, intro]: "f sums (SUP n. \<Sum>i<n. f i)"
+  unfolding sums_def by (intro LIMSEQ_SUP monoI setsum_mono2 zero_le) auto
+
+lemma suminf_eq_SUP: "suminf f = (SUP n. \<Sum>i<n. f i)"
+  using sums_SUP by (rule sums_unique[symmetric])
+
+end
+
 subsection \<open>Type definition\<close>
 
 text \<open>
@@ -71,7 +83,7 @@
 
 subsection \<open>Constructors and numbers\<close>
 
-instantiation enat :: "{zero, one}"
+instantiation enat :: zero_neq_one
 begin
 
 definition
@@ -80,7 +92,8 @@
 definition
   "1 = enat 1"
 
-instance ..
+instance
+  proof qed (simp add: zero_enat_def one_enat_def)
 
 end
 
@@ -108,7 +121,7 @@
 lemma i0_ne_infinity [simp]: "0 \<noteq> (\<infinity>::enat)"
   by (simp add: zero_enat_def)
 
-lemma zero_one_enat_neq [simp]:
+lemma zero_one_enat_neq:
   "\<not> 0 = (1::enat)"
   "\<not> 1 = (0::enat)"
   unfolding zero_enat_def one_enat_def by simp_all
@@ -183,12 +196,9 @@
 lemma iadd_Suc_right: "m + eSuc n = eSuc (m + n)"
   by (simp only: add.commute[of m] iadd_Suc)
 
-lemma iadd_is_0: "(m + n = (0::enat)) = (m = 0 \<and> n = 0)"
-  by (cases m, cases n, simp_all add: zero_enat_def)
-
 subsection \<open>Multiplication\<close>
 
-instantiation enat :: comm_semiring_1
+instantiation enat :: "{comm_semiring_1, semiring_no_zero_divisors}"
 begin
 
 definition times_enat_def [nitpick_simp]:
@@ -209,13 +219,13 @@
   show "(a * b) * c = a * (b * c)"
     unfolding times_enat_def zero_enat_def
     by (simp split: enat.split)
-  show "a * b = b * a"
+  show comm: "a * b = b * a"
     unfolding times_enat_def zero_enat_def
     by (simp split: enat.split)
   show "1 * a = a"
     unfolding times_enat_def zero_enat_def one_enat_def
     by (simp split: enat.split)
-  show "(a + b) * c = a * c + b * c"
+  show distr: "(a + b) * c = a * c + b * c"
     unfolding times_enat_def zero_enat_def
     by (simp split: enat.split add: distrib_right)
   show "0 * a = 0"
@@ -224,9 +234,10 @@
   show "a * 0 = 0"
     unfolding times_enat_def zero_enat_def
     by (simp split: enat.split)
-  show "(0::enat) \<noteq> 1"
-    unfolding zero_enat_def one_enat_def
-    by simp
+  show "a * (b + c) = a * b + a * c"
+    by (cases a b c rule: enat3_cases) (auto simp: times_enat_def zero_enat_def distrib_left)
+  show "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
+    by (cases a b rule: enat2_cases) (auto simp: times_enat_def zero_enat_def)
 qed
 
 end
@@ -249,13 +260,9 @@
   then show "inj (\<lambda>n. of_nat n :: enat)" by (simp add: of_nat_eq_enat)
 qed
 
-lemma imult_is_0 [simp]: "((m::enat) * n = 0) = (m = 0 \<or> n = 0)"
-  by (auto simp add: times_enat_def zero_enat_def split: enat.split)
-
 lemma imult_is_infinity: "((a::enat) * b = \<infinity>) = (a = \<infinity> \<and> b \<noteq> 0 \<or> b = \<infinity> \<and> a \<noteq> 0)"
   by (auto simp add: times_enat_def zero_enat_def split: enat.split)
 
-
 subsection \<open>Numerals\<close>
 
 lemma numeral_eq_enat:
@@ -368,13 +375,15 @@
     by (cases a b rule: enat2_cases) (auto simp: le_iff_add enat_ex_split)
 qed
 
-instance enat :: "ordered_comm_semiring"
+instance enat :: "{linordered_nonzero_semiring, strict_ordered_comm_monoid_add}"
 proof
   fix a b c :: enat
-  assume "a \<le> b" and "0 \<le> c" thus "c * a \<le> c * b"
+  show "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow>c * a \<le> c * b"
     unfolding times_enat_def less_eq_enat_def zero_enat_def
     by (simp split: enat.splits)
-qed
+  show "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d" for a b c d :: enat
+    by (cases a b c d rule: enat2_cases[case_product enat2_cases]) auto
+qed (simp add: zero_enat_def one_enat_def)
 
 (* BH: These equations are already proven generally for any type in
 class linordered_semidom. However, enat is not in that class because
@@ -386,24 +395,12 @@
   "(numeral m :: enat) < numeral n \<longleftrightarrow> (numeral m :: nat) < numeral n"
   by (simp_all add: numeral_eq_enat)
 
-lemma i0_lb [simp]: "(0::enat) \<le> n"
-  by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
-
-lemma ile0_eq [simp]: "n \<le> (0::enat) \<longleftrightarrow> n = 0"
-  by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
-
 lemma infinity_ileE [elim!]: "\<infinity> \<le> enat m \<Longrightarrow> R"
   by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
 
 lemma infinity_ilessE [elim!]: "\<infinity> < enat m \<Longrightarrow> R"
   by simp
 
-lemma not_iless0 [simp]: "\<not> n < (0::enat)"
-  by (simp add: zero_enat_def less_enat_def split: enat.splits)
-
-lemma i0_less [simp]: "(0::enat) < n \<longleftrightarrow> n \<noteq> 0"
-  by (simp add: zero_enat_def less_enat_def split: enat.splits)
-
 lemma eSuc_ile_mono [simp]: "eSuc n \<le> eSuc m \<longleftrightarrow> n \<le> m"
   by (simp add: eSuc_def less_eq_enat_def split: enat.splits)
 
@@ -438,12 +435,11 @@
   by (simp add: zero_enat_def less_enat_def split: enat.splits)
 
 lemma enat_0_less_mult_iff: "(0 < (m::enat) * n) = (0 < m \<and> 0 < n)"
-  by (simp only: i0_less imult_is_0, simp)
+  by (simp only: zero_less_iff_neq_zero mult_eq_0_iff, simp)
 
 lemma mono_eSuc: "mono eSuc"
   by (simp add: mono_def)
 
-
 lemma min_enat_simps [simp]:
   "min (enat m) (enat n) = enat (min m n)"
   "min q 0 = 0"
@@ -470,10 +466,10 @@
   "x + y \<le> enat n \<longleftrightarrow> (\<exists>y' x'. x = enat x' \<and> y = enat y' \<and> x' + y' \<le> n)"
 by(cases x y rule: enat.exhaust[case_product enat.exhaust]) simp_all
 
-lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. enat k < Y j"
+lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j \<Longrightarrow> \<exists>j. enat k < Y j"
 apply (induct_tac k)
  apply (simp (no_asm) only: enat_0)
- apply (fast intro: le_less_trans [OF i0_lb])
+ apply (fast intro: le_less_trans [OF zero_le])
 apply (erule exE)
 apply (drule spec)
 apply (erule exE)
@@ -678,4 +674,22 @@
 lemmas enat_defs = zero_enat_def one_enat_def eSuc_def
   plus_enat_def less_eq_enat_def less_enat_def
 
+lemma iadd_is_0: "(m + n = (0::enat)) = (m = 0 \<and> n = 0)"
+  by (rule add_eq_0_iff_both_eq_0)
+
+lemma i0_lb : "(0::enat) \<le> n"
+  by (rule zero_le)
+
+lemma ile0_eq: "n \<le> (0::enat) \<longleftrightarrow> n = 0"
+  by (rule le_zero_eq)
+
+lemma not_iless0: "\<not> n < (0::enat)"
+  by (rule not_less_zero)
+
+lemma i0_less[simp]: "(0::enat) < n \<longleftrightarrow> n \<noteq> 0"
+  by (rule zero_less_iff_neq_zero)
+
+lemma imult_is_0: "((m::enat) * n = 0) = (m = 0 \<or> n = 0)"
+  by (rule mult_eq_0_iff)
+
 end
diff -r ace69956d018 -r 85ed00c1fe7c src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Fri Feb 12 16:09:07 2016 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Fri Feb 19 13:40:50 2016 +0100
@@ -8,20 +8,117 @@
   imports Extended_Real
 begin
 
+context linordered_nonzero_semiring
+begin
+
+lemma of_nat_nonneg [simp]: "0 \<le> of_nat n"
+  by (induct n) simp_all
+
+lemma of_nat_mono[simp]: "i \<le> j \<Longrightarrow> of_nat i \<le> of_nat j"
+  by (auto simp add: le_iff_add intro!: add_increasing2)
+
+end
+
+lemma of_nat_less[simp]:
+  "i < j \<Longrightarrow> of_nat i < (of_nat j::'a::{linordered_nonzero_semiring, semiring_char_0})"
+  by (auto simp: less_le)
+
+lemma of_nat_le_iff[simp]:
+  "of_nat i \<le> (of_nat j::'a::{linordered_nonzero_semiring, semiring_char_0}) \<longleftrightarrow> i \<le> j"
+proof (safe intro!: of_nat_mono)
+  assume "of_nat i \<le> (of_nat j::'a)" then show "i \<le> j"
+  proof (intro leI notI)
+    assume "j < i" from less_le_trans[OF of_nat_less[OF this] \<open>of_nat i \<le> of_nat j\<close>] show False
+      by blast
+  qed
+qed
+
+lemma (in complete_lattice) SUP_sup_const1:
+  "I \<noteq> {} \<Longrightarrow> (SUP i:I. sup c (f i)) = sup c (SUP i:I. f i)"
+  using SUP_sup_distrib[of "\<lambda>_. c" I f] by simp
+
+lemma (in complete_lattice) SUP_sup_const2:
+  "I \<noteq> {} \<Longrightarrow> (SUP i:I. sup (f i) c) = sup (SUP i:I. f i) c"
+  using SUP_sup_distrib[of f I "\<lambda>_. c"] by simp
+
+lemma one_less_of_natD:
+  "(1::'a::linordered_semidom) < of_nat n \<Longrightarrow> 1 < n"
+  using zero_le_one[where 'a='a]
+  apply (cases n)
+  apply simp
+  subgoal for n'
+    apply (cases n')
+    apply simp
+    apply simp
+    done
+  done
+
+lemma setsum_le_suminf:
+  fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
+  shows "summable f \<Longrightarrow> finite I \<Longrightarrow> \<forall>m\<in>- I. 0 \<le> f m \<Longrightarrow> setsum f I \<le> suminf f"
+  by (rule sums_le[OF _ sums_If_finite_set summable_sums]) auto
+
 typedef ennreal = "{x :: ereal. 0 \<le> x}"
-  morphisms enn2ereal e2ennreal
+  morphisms enn2ereal e2ennreal'
   by auto
 
-setup_lifting type_definition_ennreal
+definition "e2ennreal x = e2ennreal' (max 0 x)"
 
+lemma type_definition_ennreal': "type_definition enn2ereal e2ennreal {x. 0 \<le> x}"
+  using type_definition_ennreal
+  by (auto simp: type_definition_def e2ennreal_def max_absorb2)
 
-lift_definition ennreal :: "real \<Rightarrow> ennreal" is "max 0 \<circ> ereal"
+setup_lifting type_definition_ennreal'
+
+lift_definition ennreal :: "real \<Rightarrow> ennreal" is "sup 0 \<circ> ereal"
   by simp
 
 declare [[coercion ennreal]]
 declare [[coercion e2ennreal]]
 
-instantiation ennreal :: semiring_1_no_zero_divisors
+instantiation ennreal :: complete_linorder
+begin
+
+lift_definition top_ennreal :: ennreal is top by (rule top_greatest)
+lift_definition bot_ennreal :: ennreal is 0 by (rule order_refl)
+lift_definition sup_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is sup by (rule le_supI1)
+lift_definition inf_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is inf by (rule le_infI)
+
+lift_definition Inf_ennreal :: "ennreal set \<Rightarrow> ennreal" is "Inf"
+  by (rule Inf_greatest)
+
+lift_definition Sup_ennreal :: "ennreal set \<Rightarrow> ennreal" is "sup 0 \<circ> Sup"
+  by auto
+
+lift_definition less_eq_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> bool" is "op \<le>" .
+lift_definition less_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> bool" is "op <" .
+
+instance
+  by standard
+     (transfer ; auto simp: Inf_lower Inf_greatest Sup_upper Sup_least le_max_iff_disj max.absorb1)+
+
+end
+
+lemma ennreal_cases:
+  fixes x :: ennreal
+  obtains (real) r :: real where "0 \<le> r" "x = ennreal r" | (top) "x = top"
+  apply transfer
+  subgoal for x thesis
+    by (cases x) (auto simp: max.absorb2 top_ereal_def)
+  done
+
+instantiation ennreal :: infinity
+begin
+
+definition infinity_ennreal :: ennreal
+where
+  [simp]: "\<infinity> = (top::ennreal)"
+
+instance ..
+
+end
+
+instantiation ennreal :: "{semiring_1_no_zero_divisors, comm_semiring_1}"
 begin
 
 lift_definition one_ennreal :: ennreal is 1 by simp
@@ -34,6 +131,16 @@
 
 end
 
+instantiation ennreal :: minus
+begin
+
+lift_definition minus_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is "\<lambda>a b. max 0 (a - b)"
+  by simp
+
+instance ..
+
+end
+
 instance ennreal :: numeral ..
 
 instantiation ennreal :: inverse
@@ -49,32 +156,6 @@
 
 end
 
-
-instantiation ennreal :: complete_linorder
-begin
-
-lift_definition top_ennreal :: ennreal is top by simp
-lift_definition bot_ennreal :: ennreal is 0 by simp
-lift_definition sup_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is sup by (simp add: max.coboundedI1)
-lift_definition inf_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is inf by (simp add: min.boundedI)
-
-lift_definition Inf_ennreal :: "ennreal set \<Rightarrow> ennreal" is "Inf"
-  by (auto intro: Inf_greatest)
-
-lift_definition Sup_ennreal :: "ennreal set \<Rightarrow> ennreal" is "sup 0 \<circ> Sup"
-  by auto
-
-lift_definition less_eq_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> bool" is "op \<le>" .
-lift_definition less_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> bool" is "op <" .
-
-instance
-  by standard
-     (transfer ; auto simp: Inf_lower Inf_greatest Sup_upper Sup_least le_max_iff_disj max.absorb1)+
-
-end
-
-
-
 lemma ennreal_zero_less_one: "0 < (1::ennreal)"
   by transfer auto
 
@@ -89,6 +170,96 @@
   by standard
      (transfer ; auto intro: add_mono mult_mono mult_ac ereal_left_distrib ereal_mult_left_mono)+
 
+instance ennreal :: linordered_nonzero_semiring
+  proof qed (transfer; simp)
+
+declare [[coercion "of_nat :: nat \<Rightarrow> ennreal"]]
+
+lemma e2ennreal_neg: "x \<le> 0 \<Longrightarrow> e2ennreal x = 0"
+  unfolding zero_ennreal_def e2ennreal_def by (simp add: max_absorb1)
+
+lemma e2ennreal_mono: "x \<le> y \<Longrightarrow> e2ennreal x \<le> e2ennreal y"
+  by (cases "0 \<le> x" "0 \<le> y" rule: bool.exhaust[case_product bool.exhaust])
+     (auto simp: e2ennreal_neg less_eq_ennreal.abs_eq eq_onp_def)
+
+subsection \<open>Cancellation simprocs\<close>
+
+lemma ennreal_add_left_cancel: "a + b = a + c \<longleftrightarrow> a = (\<infinity>::ennreal) \<or> b = c"
+  unfolding infinity_ennreal_def by transfer (simp add: top_ereal_def ereal_add_cancel_left)
+
+lemma ennreal_add_left_cancel_le: "a + b \<le> a + c \<longleftrightarrow> a = (\<infinity>::ennreal) \<or> b \<le> c"
+  unfolding infinity_ennreal_def by transfer (simp add: ereal_add_le_add_iff top_ereal_def disj_commute)
+
+lemma ereal_add_left_cancel_less:
+  fixes a b c :: ereal
+  shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a + b < a + c \<longleftrightarrow> a \<noteq> \<infinity> \<and> b < c"
+  by (cases a b c rule: ereal3_cases) auto
+
+lemma ennreal_add_left_cancel_less: "a + b < a + c \<longleftrightarrow> a \<noteq> (\<infinity>::ennreal) \<and> b < c"
+  unfolding infinity_ennreal_def
+  by transfer (simp add: top_ereal_def ereal_add_left_cancel_less)
+
+ML \<open>
+structure Cancel_Ennreal_Common =
+struct
+  (* copied from src/HOL/Tools/nat_numeral_simprocs.ML *)
+  fun find_first_t _    _ []         = raise TERM("find_first_t", [])
+    | find_first_t past u (t::terms) =
+          if u aconv t then (rev past @ terms)
+          else find_first_t (t::past) u terms
+
+  fun dest_summing (Const (@{const_name Groups.plus}, _) $ t $ u, ts) =
+        dest_summing (t, dest_summing (u, ts))
+    | dest_summing (t, ts) = t :: ts
+
+  val mk_sum = Arith_Data.long_mk_sum
+  fun dest_sum t = dest_summing (t, [])
+  val find_first = find_first_t []
+  val trans_tac = Numeral_Simprocs.trans_tac
+  val norm_ss =
+    simpset_of (put_simpset HOL_basic_ss @{context}
+      addsimps @{thms ac_simps add_0_left add_0_right})
+  fun norm_tac ctxt = ALLGOALS (simp_tac (put_simpset norm_ss ctxt))
+  fun simplify_meta_eq ctxt cancel_th th =
+    Arith_Data.simplify_meta_eq [] ctxt
+      ([th, cancel_th] MRS trans)
+  fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
+end
+
+structure Eq_Ennreal_Cancel = ExtractCommonTermFun
+(open Cancel_Ennreal_Common
+  val mk_bal = HOLogic.mk_eq
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} @{typ ennreal}
+  fun simp_conv _ _ = SOME @{thm ennreal_add_left_cancel}
+)
+
+structure Le_Ennreal_Cancel = ExtractCommonTermFun
+(open Cancel_Ennreal_Common
+  val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}
+  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} @{typ ennreal}
+  fun simp_conv _ _ = SOME @{thm ennreal_add_left_cancel_le}
+)
+
+structure Less_Ennreal_Cancel = ExtractCommonTermFun
+(open Cancel_Ennreal_Common
+  val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less}
+  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} @{typ ennreal}
+  fun simp_conv _ _ = SOME @{thm ennreal_add_left_cancel_less}
+)
+\<close>
+
+simproc_setup ennreal_eq_cancel
+  ("(l::ennreal) + m = n" | "(l::ennreal) = m + n") =
+  \<open>fn phi => fn ctxt => fn ct => Eq_Ennreal_Cancel.proc ctxt (Thm.term_of ct)\<close>
+
+simproc_setup ennreal_le_cancel
+  ("(l::ennreal) + m \<le> n" | "(l::ennreal) \<le> m + n") =
+  \<open>fn phi => fn ctxt => fn ct => Le_Ennreal_Cancel.proc ctxt (Thm.term_of ct)\<close>
+
+simproc_setup ennreal_less_cancel
+  ("(l::ennreal) + m < n" | "(l::ennreal) < m + n") =
+  \<open>fn phi => fn ctxt => fn ct => Less_Ennreal_Cancel.proc ctxt (Thm.term_of ct)\<close>
+
 instantiation ennreal :: linear_continuum_topology
 begin
 
@@ -98,7 +269,7 @@
 instance
 proof
   show "\<exists>a b::ennreal. a \<noteq> b"
-    using ennreal_zero_less_one by (auto dest: order.strict_implies_not_eq)
+    using zero_neq_one by (intro exI)
   show "\<And>x y::ennreal. x < y \<Longrightarrow> \<exists>z>x. z < y"
   proof transfer
     fix x y :: ereal assume "0 \<le> x" "x < y"
@@ -121,14 +292,14 @@
     by auto
   moreover then have "0 \<le> r"
     using le_less_trans[OF \<open>0 \<le> x\<close> \<open>x < ereal (real_of_rat r)\<close>] by auto
-  ultimately show "\<exists>r. x < (max 0 \<circ> ereal) (real_of_rat r) \<and> (max 0 \<circ> ereal) (real_of_rat r) < y"
+  ultimately show "\<exists>r. x < (sup 0 \<circ> ereal) (real_of_rat r) \<and> (sup 0 \<circ> ereal) (real_of_rat r) < y"
     by (intro exI[of _ r]) (auto simp: max_absorb2)
 qed
 
 lemma enn2ereal_range: "e2ennreal ` {0..} = UNIV"
 proof -
   have "\<exists>y\<ge>0. x = e2ennreal y" for x
-    by (cases x) auto
+    by (cases x) (auto simp: e2ennreal_def max_absorb2)
   then show ?thesis
     by (auto simp: image_iff Bex_def)
 qed
@@ -138,37 +309,54 @@
 
 lemma ereal_ennreal_cases:
   obtains b where "0 \<le> a" "a = enn2ereal b" | "a < 0"
-  using e2ennreal_inverse[of a, symmetric] by (cases "0 \<le> a") (auto intro: enn2ereal_nonneg)
+  using e2ennreal'_inverse[of a, symmetric] by (cases "0 \<le> a") (auto intro: enn2ereal_nonneg)
 
 lemma enn2ereal_Iio: "enn2ereal -` {..<a} = (if 0 \<le> a then {..< e2ennreal a} else {})"
   using enn2ereal_nonneg
   by (cases a rule: ereal_ennreal_cases)
-     (auto simp add: vimage_def set_eq_iff ennreal.enn2ereal_inverse less_ennreal.rep_eq
+     (auto simp add: vimage_def set_eq_iff ennreal.enn2ereal_inverse less_ennreal.rep_eq e2ennreal_def max_absorb2
            intro: le_less_trans less_imp_le)
 
 lemma enn2ereal_Ioi: "enn2ereal -` {a <..} = (if 0 \<le> a then {e2ennreal a <..} else UNIV)"
   using enn2ereal_nonneg
   by (cases a rule: ereal_ennreal_cases)
-     (auto simp add: vimage_def set_eq_iff ennreal.enn2ereal_inverse less_ennreal.rep_eq
+     (auto simp add: vimage_def set_eq_iff ennreal.enn2ereal_inverse less_ennreal.rep_eq e2ennreal_def max_absorb2
            intro: less_le_trans)
 
-lemma continuous_e2ennreal: "continuous_on {0 ..} e2ennreal"
-  by (rule continuous_onI_mono)
-     (auto simp add: less_eq_ennreal.abs_eq eq_onp_def enn2ereal_range)
+lemma continuous_on_e2ennreal: "continuous_on A e2ennreal"
+proof (rule continuous_on_subset)
+  show "continuous_on ({0..} \<union> {..0}) e2ennreal"
+  proof (rule continuous_on_closed_Un)
+    show "continuous_on {0 ..} e2ennreal"
+      by (rule continuous_onI_mono)
+         (auto simp add: less_eq_ennreal.abs_eq eq_onp_def enn2ereal_range)
+    show "continuous_on {.. 0} e2ennreal"
+      by (subst continuous_on_cong[OF refl, of _ _ "\<lambda>_. 0"])
+         (auto simp add: e2ennreal_neg continuous_on_const)
+  qed auto
+  show "A \<subseteq> {0..} \<union> {..0::ereal}"
+    by auto
+qed
 
-lemma continuous_enn2ereal: "continuous_on UNIV enn2ereal"
+lemma continuous_at_e2ennreal: "continuous (at x within A) e2ennreal"
+  by (rule continuous_on_imp_continuous_within[OF continuous_on_e2ennreal, of _ UNIV]) auto
+
+lemma continuous_on_enn2ereal: "continuous_on UNIV enn2ereal"
   by (rule continuous_on_generate_topology[OF open_generated_order])
      (auto simp add: enn2ereal_Iio enn2ereal_Ioi)
 
+lemma continuous_at_enn2ereal: "continuous (at x within A) enn2ereal"
+  by (rule continuous_on_imp_continuous_within[OF continuous_on_enn2ereal]) auto
+
 lemma transfer_enn2ereal_continuous_on [transfer_rule]:
   "rel_fun (op =) (rel_fun (rel_fun op = pcr_ennreal) op =) continuous_on continuous_on"
 proof -
   have "continuous_on A f" if "continuous_on A (\<lambda>x. enn2ereal (f x))" for A and f :: "'a \<Rightarrow> ennreal"
-    using continuous_on_compose2[OF continuous_e2ennreal that]
-    by (auto simp: ennreal.enn2ereal_inverse subset_eq enn2ereal_nonneg)
+    using continuous_on_compose2[OF continuous_on_e2ennreal[of "{0..}"] that]
+    by (auto simp: ennreal.enn2ereal_inverse subset_eq enn2ereal_nonneg e2ennreal_def max_absorb2)
   moreover
   have "continuous_on A (\<lambda>x. enn2ereal (f x))" if "continuous_on A f" for A and f :: "'a \<Rightarrow> ennreal"
-    using continuous_on_compose2[OF continuous_enn2ereal that] by auto
+    using continuous_on_compose2[OF continuous_on_enn2ereal that] by auto
   ultimately
   show ?thesis
     by (auto simp add: rel_fun_def ennreal.pcr_cr_eq cr_ennreal_def)
@@ -180,12 +368,484 @@
   by (transfer fixing: A) (auto intro!: tendsto_add_ereal_nonneg simp: continuous_on_def)
 
 lemma continuous_on_inverse_ennreal[continuous_intros]:
-  fixes f :: "_ \<Rightarrow> ennreal"
+  fixes f :: "'a::topological_space \<Rightarrow> ennreal"
   shows "continuous_on A f \<Longrightarrow> continuous_on A (\<lambda>x. inverse (f x))"
 proof (transfer fixing: A)
-  show "pred_fun (op \<le> 0) f \<Longrightarrow> continuous_on A (\<lambda>x. inverse (f x))" if "continuous_on A f"
-    for f :: "_ \<Rightarrow> ereal"
+  show "pred_fun (\<lambda>_. True)  (op \<le> 0) f \<Longrightarrow> continuous_on A (\<lambda>x. inverse (f x))" if "continuous_on A f"
+    for f :: "'a \<Rightarrow> ereal"
     using continuous_on_compose2[OF continuous_on_inverse_ereal that] by (auto simp: subset_eq)
 qed
 
+instance ennreal :: topological_comm_monoid_add
+proof
+  show "((\<lambda>x. fst x + snd x) \<longlongrightarrow> a + b) (nhds a \<times>\<^sub>F nhds b)" for a b :: ennreal
+    using continuous_on_add_ennreal[of UNIV fst snd]
+    using tendsto_at_iff_tendsto_nhds[symmetric, of "\<lambda>x::(ennreal \<times> ennreal). fst x + snd x"]
+    by (auto simp: continuous_on_eq_continuous_at)
+       (simp add: isCont_def nhds_prod[symmetric])
+qed
+
+lemma ennreal_zero_less_top[simp]: "0 < (top::ennreal)"
+  by transfer (simp add: top_ereal_def)
+
+lemma ennreal_one_less_top[simp]: "1 < (top::ennreal)"
+  by transfer (simp add: top_ereal_def)
+
+lemma ennreal_zero_neq_top[simp]: "0 \<noteq> (top::ennreal)"
+  by transfer (simp add: top_ereal_def)
+
+lemma ennreal_top_neq_zero[simp]: "(top::ennreal) \<noteq> 0"
+  by transfer (simp add: top_ereal_def)
+
+lemma ennreal_top_neq_one[simp]: "top \<noteq> (1::ennreal)"
+  by transfer (simp add: top_ereal_def one_ereal_def ereal_max[symmetric] del: ereal_max)
+
+lemma ennreal_one_neq_top[simp]: "1 \<noteq> (top::ennreal)"
+  by transfer (simp add: top_ereal_def one_ereal_def ereal_max[symmetric] del: ereal_max)
+
+lemma ennreal_add_less_top[simp]:
+  fixes a b :: ennreal
+  shows "a + b < top \<longleftrightarrow> a < top \<and> b < top"
+  by transfer (auto simp: top_ereal_def)
+
+lemma ennreal_add_eq_top[simp]:
+  fixes a b :: ennreal
+  shows "a + b = top \<longleftrightarrow> a = top \<or> b = top"
+  by transfer (auto simp: top_ereal_def)
+
+lemma ennreal_setsum_less_top[simp]:
+  fixes f :: "'a \<Rightarrow> ennreal"
+  shows "finite I \<Longrightarrow> (\<Sum>i\<in>I. f i) < top \<longleftrightarrow> (\<forall>i\<in>I. f i < top)"
+  by (induction I rule: finite_induct) auto
+
+lemma ennreal_setsum_eq_top[simp]:
+  fixes f :: "'a \<Rightarrow> ennreal"
+  shows "finite I \<Longrightarrow> (\<Sum>i\<in>I. f i) = top \<longleftrightarrow> (\<exists>i\<in>I. f i = top)"
+  by (induction I rule: finite_induct) auto
+
+lemma enn2ereal_eq_top_iff[simp]: "enn2ereal x = \<infinity> \<longleftrightarrow> x = top"
+  by transfer (simp add: top_ereal_def)
+
+lemma ennreal_top_top: "top - top = (top::ennreal)"
+  by transfer (auto simp: top_ereal_def max_def)
+
+lemma ennreal_minus_zero[simp]: "a - (0::ennreal) = a"
+  by transfer (auto simp: max_def)
+
+lemma ennreal_add_diff_cancel_right[simp]:
+  fixes x y z :: ennreal shows "y \<noteq> top \<Longrightarrow> (x + y) - y = x"
+  apply transfer
+  subgoal for x y
+    apply (cases x y rule: ereal2_cases)
+    apply (auto split: split_max simp: top_ereal_def)
+    done
+  done
+
+lemma ennreal_add_diff_cancel_left[simp]:
+  fixes x y z :: ennreal shows "y \<noteq> top \<Longrightarrow> (y + x) - y = x"
+  by (simp add: add.commute)
+
+lemma
+  fixes a b :: ennreal
+  shows "a - b = 0 \<Longrightarrow> a \<le> b"
+  apply transfer
+  subgoal for a b
+    apply (cases a b rule: ereal2_cases)
+    apply (auto simp: not_le max_def split: if_splits)
+    done
+  done
+
+lemma ennreal_minus_cancel:
+  fixes a b c :: ennreal
+  shows "c \<noteq> top \<Longrightarrow> a \<le> c \<Longrightarrow> b \<le> c \<Longrightarrow> c - a = c - b \<Longrightarrow> a = b"
+  apply transfer
+  subgoal for a b c
+    by (cases a b c rule: ereal3_cases)
+       (auto simp: top_ereal_def max_def split: if_splits)
+  done
+
+lemma enn2ereal_ennreal[simp]: "0 \<le> x \<Longrightarrow> enn2ereal (ennreal x) = x"
+  by transfer (simp add: max_absorb2)
+
+lemma tendsto_ennrealD:
+  assumes lim: "((\<lambda>x. ennreal (f x)) \<longlongrightarrow> ennreal x) F"
+  assumes *: "\<forall>\<^sub>F x in F. 0 \<le> f x" and x: "0 \<le> x"
+  shows "(f \<longlongrightarrow> x) F"
+  using continuous_on_tendsto_compose[OF continuous_on_enn2ereal lim]
+  apply simp
+  apply (subst (asm) tendsto_cong)
+  using *
+  apply eventually_elim
+  apply (auto simp: max_absorb2 \<open>0 \<le> x\<close>)
+  done
+
+lemma tendsto_ennreal_iff[simp]:
+  "\<forall>\<^sub>F x in F. 0 \<le> f x \<Longrightarrow> 0 \<le> x \<Longrightarrow> ((\<lambda>x. ennreal (f x)) \<longlongrightarrow> ennreal x) F \<longleftrightarrow> (f \<longlongrightarrow> x) F"
+  by (auto dest: tendsto_ennrealD)
+     (auto simp: ennreal_def
+           intro!: continuous_on_tendsto_compose[OF continuous_on_e2ennreal[of UNIV]] tendsto_max)
+
+lemma ennreal_zero[simp]: "ennreal 0 = 0"
+  by (simp add: ennreal_def max.absorb1 zero_ennreal.abs_eq)
+
+lemma ennreal_plus[simp]:
+  "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> ennreal (a + b) = ennreal a + ennreal b"
+  by (transfer fixing: a b) (auto simp: max_absorb2)
+
+lemma ennreal_inj[simp]:
+  "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> ennreal a = ennreal b \<longleftrightarrow> a = b"
+  by (transfer fixing: a b) (auto simp: max_absorb2)
+
+lemma ennreal_le_iff[simp]: "0 \<le> y \<Longrightarrow> ennreal x \<le> ennreal y \<longleftrightarrow> x \<le> y"
+  by (auto simp: ennreal_def zero_ereal_def less_eq_ennreal.abs_eq eq_onp_def split: split_max)
+
+lemma setsum_ennreal[simp]: "(\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> (\<Sum>i\<in>I. ennreal (f i)) = ennreal (setsum f I)"
+  by (induction I rule: infinite_finite_induct) (auto simp: setsum_nonneg)
+
+lemma sums_ennreal[simp]: "(\<And>i. 0 \<le> f i) \<Longrightarrow> 0 \<le> x \<Longrightarrow> (\<lambda>i. ennreal (f i)) sums ennreal x \<longleftrightarrow> f sums x"
+  unfolding sums_def by (simp add: always_eventually setsum_nonneg)
+
+lemma summable_suminf_not_top: "(\<And>i. 0 \<le> f i) \<Longrightarrow> (\<Sum>i. ennreal (f i)) \<noteq> top \<Longrightarrow> summable f"
+  using summable_sums[OF summableI, of "\<lambda>i. ennreal (f i)"]
+  by (cases "\<Sum>i. ennreal (f i)" rule: ennreal_cases)
+     (auto simp: summable_def)
+
+lemma suminf_ennreal[simp]:
+  "(\<And>i. 0 \<le> f i) \<Longrightarrow> (\<Sum>i. ennreal (f i)) \<noteq> top \<Longrightarrow> (\<Sum>i. ennreal (f i)) = ennreal (\<Sum>i. f i)"
+  by (rule sums_unique[symmetric]) (simp add: summable_suminf_not_top suminf_nonneg summable_sums)
+
+lemma suminf_less_top: "(\<Sum>i. f i :: ennreal) < top \<Longrightarrow> f i < top"
+  using le_less_trans[OF setsum_le_suminf[OF summableI, of "{i}" f]] by simp
+
+lemma add_top:
+  fixes x :: "'a::{order_top, ordered_comm_monoid_add}"
+  shows "0 \<le> x \<Longrightarrow> x + top = top"
+  by (intro top_le add_increasing order_refl)
+
+lemma top_add:
+  fixes x :: "'a::{order_top, ordered_comm_monoid_add}"
+  shows "0 \<le> x \<Longrightarrow> top + x = top"
+  by (intro top_le add_increasing2 order_refl)
+
+lemma enn2ereal_top: "enn2ereal top = \<infinity>"
+  by transfer (simp add: top_ereal_def)
+
+lemma e2ennreal_infty: "e2ennreal \<infinity> = top"
+  by (simp add: top_ennreal.abs_eq top_ereal_def)
+
+lemma sup_const_add_ennreal:
+  fixes a b c :: "ennreal"
+  shows "sup (c + a) (c + b) = c + sup a b"
+  apply transfer
+  subgoal for a b c
+    apply (cases a b c rule: ereal3_cases)
+    apply (auto simp: ereal_max[symmetric] simp del: ereal_max)
+    apply (auto simp: top_ereal_def[symmetric] sup_ereal_def[symmetric]
+                simp del: sup_ereal_def)
+    apply (auto simp add: top_ereal_def)
+    done
+  done
+
+lemma bot_ennreal: "bot = (0::ennreal)"
+  by transfer rule
+
+lemma le_lfp: "mono f \<Longrightarrow> x \<le> lfp f \<Longrightarrow> f x \<le> lfp f"
+  by (subst lfp_unfold) (auto dest: monoD)
+
+lemma lfp_transfer:
+  assumes \<alpha>: "sup_continuous \<alpha>" and f: "sup_continuous f" and mg: "mono g"
+  assumes bot: "\<alpha> bot \<le> lfp g" and eq: "\<And>x. x \<le> lfp f \<Longrightarrow> \<alpha> (f x) = g (\<alpha> x)"
+  shows "\<alpha> (lfp f) = lfp g"
+proof (rule antisym)
+  note mf = sup_continuous_mono[OF f]
+  have f_le_lfp: "(f ^^ i) bot \<le> lfp f" for i
+    by (induction i) (auto intro: le_lfp mf)
+
+  have "\<alpha> ((f ^^ i) bot) \<le> lfp g" for i
+    by (induction i) (auto simp: bot eq f_le_lfp intro!: le_lfp mg)
+  then show "\<alpha> (lfp f) \<le> lfp g"
+    unfolding sup_continuous_lfp[OF f]
+    by (subst \<alpha>[THEN sup_continuousD])
+       (auto intro!: mono_funpow sup_continuous_mono[OF f] SUP_least)
+
+  show "lfp g \<le> \<alpha> (lfp f)"
+    by (rule lfp_lowerbound) (simp add: eq[symmetric] lfp_unfold[OF mf, symmetric])
+qed
+
+lemma sup_continuous_applyD: "sup_continuous f \<Longrightarrow> sup_continuous (\<lambda>x. f x h)"
+  using sup_continuous_apply[THEN sup_continuous_compose] .
+
+lemma INF_ennreal_add_const:
+  fixes f g :: "nat \<Rightarrow> ennreal"
+  shows "(INF i. f i + c) = (INF i. f i) + c"
+  using continuous_at_Inf_mono[of "\<lambda>x. x + c" "f`UNIV"]
+  using continuous_add[of "at_right (Inf (range f))", of "\<lambda>x. x" "\<lambda>x. c"]
+  by (auto simp: mono_def)
+
+lemma INF_ennreal_const_add:
+  fixes f g :: "nat \<Rightarrow> ennreal"
+  shows "(INF i. c + f i) = c + (INF i. f i)"
+  using INF_ennreal_add_const[of f c] by (simp add: ac_simps)
+
+lemma sup_continuous_e2ennreal[order_continuous_intros]:
+  assumes f: "sup_continuous f" shows "sup_continuous (\<lambda>x. e2ennreal (f x))"
+  apply (rule sup_continuous_compose[OF _ f])
+  apply (rule continuous_at_left_imp_sup_continuous)
+  apply (auto simp: mono_def e2ennreal_mono continuous_at_e2ennreal)
+  done
+
+lemma sup_continuous_enn2ereal[order_continuous_intros]:
+  assumes f: "sup_continuous f" shows "sup_continuous (\<lambda>x. enn2ereal (f x))"
+  apply (rule sup_continuous_compose[OF _ f])
+  apply (rule continuous_at_left_imp_sup_continuous)
+  apply (simp_all add: mono_def less_eq_ennreal.rep_eq continuous_at_enn2ereal)
+  done
+
+lemma ennreal_1[simp]: "ennreal 1 = 1"
+  by transfer (simp add: max_absorb2)
+
+lemma ennreal_of_nat_eq_real_of_nat: "of_nat i = ennreal (of_nat i)"
+  by (induction i) simp_all
+
+lemma ennreal_SUP_of_nat_eq_top: "(SUP x. of_nat x :: ennreal) = top"
+proof (intro antisym top_greatest le_SUP_iff[THEN iffD2] allI impI)
+  fix y :: ennreal assume "y < top"
+  then obtain r where "y = ennreal r"
+    by (cases y rule: ennreal_cases) auto
+  then show "\<exists>i\<in>UNIV. y < of_nat i"
+    using ex_less_of_nat[of "max 1 r"] zero_less_one
+    by (auto simp: ennreal_of_nat_eq_real_of_nat ennreal_def less_ennreal.abs_eq eq_onp_def max.absorb2
+             dest!: one_less_of_natD intro: less_trans)
+qed
+
+lemma ennreal_SUP_eq_top:
+  fixes f :: "'a \<Rightarrow> ennreal"
+  assumes "\<And>n. \<exists>i\<in>I. of_nat n \<le> f i"
+  shows "(SUP i : I. f i) = top"
+proof -
+  have "(SUP x. of_nat x :: ennreal) \<le> (SUP i : I. f i)"
+    using assms by (auto intro!: SUP_least intro: SUP_upper2)
+  then show ?thesis
+    by (auto simp: ennreal_SUP_of_nat_eq_top top_unique)
+qed
+
+lemma sup_continuous_SUP[order_continuous_intros]:
+  fixes M :: "_ \<Rightarrow> _ \<Rightarrow> 'a::complete_lattice"
+  assumes M: "\<And>i. i \<in> I \<Longrightarrow> sup_continuous (M i)"
+  shows  "sup_continuous (SUP i:I. M i)"
+  unfolding sup_continuous_def by (auto simp add: sup_continuousD[OF M] intro: SUP_commute)
+
+lemma sup_continuous_apply_SUP[order_continuous_intros]:
+  fixes M :: "_ \<Rightarrow> _ \<Rightarrow> 'a::complete_lattice"
+  shows "(\<And>i. i \<in> I \<Longrightarrow> sup_continuous (M i)) \<Longrightarrow> sup_continuous (\<lambda>x. SUP i:I. M i x)"
+  unfolding SUP_apply[symmetric] by (rule sup_continuous_SUP)
+
+lemma sup_continuous_lfp'[order_continuous_intros]:
+  assumes 1: "sup_continuous f"
+  assumes 2: "\<And>g. sup_continuous g \<Longrightarrow> sup_continuous (f g)"
+  shows "sup_continuous (lfp f)"
+proof -
+  have "sup_continuous ((f ^^ i) bot)" for i
+  proof (induction i)
+    case (Suc i) then show ?case
+      by (auto intro!: 2)
+  qed (simp add: bot_fun_def sup_continuous_const)
+  then show ?thesis
+    unfolding sup_continuous_lfp[OF 1] by (intro order_continuous_intros)
+qed
+
+lemma sup_continuous_lfp''[order_continuous_intros]:
+  assumes 1: "\<And>s. sup_continuous (f s)"
+  assumes 2: "\<And>g. sup_continuous g \<Longrightarrow> sup_continuous (\<lambda>s. f s (g s))"
+  shows "sup_continuous (\<lambda>x. lfp (f x))"
+proof -
+  have "sup_continuous (\<lambda>x. (f x ^^ i) bot)" for i
+  proof (induction i)
+    case (Suc i) then show ?case
+      by (auto intro!: 2)
+  qed (simp add: bot_fun_def sup_continuous_const)
+  then show ?thesis
+    unfolding sup_continuous_lfp[OF 1] by (intro order_continuous_intros)
+qed
+
+lemma ennreal_INF_const_minus:
+  fixes f :: "'a \<Rightarrow> ennreal"
+  shows "I \<noteq> {} \<Longrightarrow> (SUP x:I. c - f x) = c - (INF x:I. f x)"
+  by (transfer fixing: I)
+     (simp add: sup_max[symmetric] SUP_sup_const1 SUP_ereal_minus_right del: sup_ereal_def)
+
+lemma ennreal_diff_add_assoc:
+  fixes a b c :: ennreal
+  shows "a \<le> b \<Longrightarrow> c + b - a = c + (b - a)"
+  apply transfer
+  subgoal for a b c
+    apply (cases a b c rule: ereal3_cases)
+    apply (auto simp: field_simps max_absorb2)
+    done
+  done
+
+lemma ennreal_top_minus[simp]:
+  fixes c :: ennreal
+  shows "top - c = top"
+  by transfer (auto simp: top_ereal_def max_absorb2)
+
+lemma le_ennreal_iff:
+  "0 \<le> r \<Longrightarrow> x \<le> ennreal r \<longleftrightarrow> (\<exists>q\<ge>0. x = ennreal q \<and> q \<le> r)"
+  apply (transfer fixing: r)
+  subgoal for x
+    by (cases x) (auto simp: max_absorb2 cong: conj_cong)
+  done
+
+lemma ennreal_minus: "0 \<le> q \<Longrightarrow> q \<le> r \<Longrightarrow> ennreal r - ennreal q = ennreal (r - q)"
+  by transfer (simp add: max_absorb2)
+
+lemma ennreal_tendsto_const_minus:
+  fixes g :: "'a \<Rightarrow> ennreal"
+  assumes ae: "\<forall>\<^sub>F x in F. g x \<le> c"
+  assumes g: "((\<lambda>x. c - g x) \<longlongrightarrow> 0) F"
+  shows "(g \<longlongrightarrow> c) F"
+proof (cases c rule: ennreal_cases)
+  case top with tendsto_unique[OF _ g, of "top"] show ?thesis
+    by (cases "F = bot") auto
+next
+  case (real r)
+  then have "\<forall>x. \<exists>q\<ge>0. g x \<le> c \<longrightarrow> (g x = ennreal q \<and> q \<le> r)"
+    by (auto simp: le_ennreal_iff)
+  then obtain f where *: "\<And>x. g x \<le> c \<Longrightarrow> 0 \<le> f x" "\<And>x. g x \<le> c \<Longrightarrow> g x = ennreal (f x)" "\<And>x. g x \<le> c \<Longrightarrow> f x \<le> r"
+    by metis
+  from ae have ae2: "\<forall>\<^sub>F x in F. c - g x = ennreal (r - f x) \<and> f x \<le> r \<and> g x = ennreal (f x) \<and> 0 \<le> f x"
+  proof eventually_elim
+    fix x assume "g x \<le> c" with *[of x] \<open>0 \<le> r\<close> show "c - g x = ennreal (r - f x) \<and> f x \<le> r \<and> g x = ennreal (f x) \<and> 0 \<le> f x"
+      by (auto simp: real ennreal_minus)
+  qed
+  with g have "((\<lambda>x. ennreal (r - f x)) \<longlongrightarrow> ennreal 0) F"
+    by (auto simp add: tendsto_cong eventually_conj_iff)
+  with ae2 have "((\<lambda>x. r - f x) \<longlongrightarrow> 0) F"
+    by (subst (asm) tendsto_ennreal_iff) (auto elim: eventually_mono)
+  then have "(f \<longlongrightarrow> r) F"
+    by (rule Lim_transform2[OF tendsto_const])
+  with ae2 have "((\<lambda>x. ennreal (f x)) \<longlongrightarrow> ennreal r) F"
+    by (subst tendsto_ennreal_iff) (auto elim: eventually_mono simp: real)
+  with ae2 show ?thesis
+    by (auto simp: real tendsto_cong eventually_conj_iff)
+qed
+
+lemma ereal_add_diff_cancel:
+  fixes a b :: ereal
+  shows "\<bar>b\<bar> \<noteq> \<infinity> \<Longrightarrow> (a + b) - b = a"
+  by (cases a b rule: ereal2_cases) auto
+
+lemma ennreal_add_diff_cancel:
+  fixes a b :: ennreal
+  shows "b \<noteq> \<infinity> \<Longrightarrow> (a + b) - b = a"
+  unfolding infinity_ennreal_def
+  by transfer (simp add: max_absorb2 top_ereal_def ereal_add_diff_cancel)
+
+lemma ennreal_mult_eq_top_iff:
+  fixes a b :: ennreal
+  shows "a * b = top \<longleftrightarrow> (a = top \<and> b \<noteq> 0) \<or> (b = top \<and> a \<noteq> 0)"
+  by transfer (auto simp: top_ereal_def)
+
+lemma ennreal_top_eq_mult_iff:
+  fixes a b :: ennreal
+  shows "top = a * b \<longleftrightarrow> (a = top \<and> b \<noteq> 0) \<or> (b = top \<and> a \<noteq> 0)"
+  using ennreal_mult_eq_top_iff[of a b] by auto
+
+lemma ennreal_mult: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> ennreal (a * b) = ennreal a * ennreal b"
+  by transfer (simp add: max_absorb2)
+
+lemma setsum_enn2ereal[simp]: "(\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> (\<Sum>i\<in>I. enn2ereal (f i)) = enn2ereal (setsum f I)"
+  by (induction I rule: infinite_finite_induct) (auto simp: setsum_nonneg zero_ennreal.rep_eq plus_ennreal.rep_eq)
+
+lemma e2ennreal_enn2ereal[simp]: "e2ennreal (enn2ereal x) = x"
+  by (simp add: e2ennreal_def max_absorb2 enn2ereal_nonneg ennreal.enn2ereal_inverse)
+
+lemma tendsto_enn2ereal_iff[simp]: "((\<lambda>i. enn2ereal (f i)) \<longlongrightarrow> enn2ereal x) F \<longleftrightarrow> (f \<longlongrightarrow> x) F"
+  using continuous_on_enn2ereal[THEN continuous_on_tendsto_compose, of f x F]
+    continuous_on_e2ennreal[THEN continuous_on_tendsto_compose, of "\<lambda>x. enn2ereal (f x)" "enn2ereal x" F UNIV]
+  by auto
+
+lemma sums_enn2ereal[simp]: "(\<lambda>i. enn2ereal (f i)) sums enn2ereal x \<longleftrightarrow> f sums x"
+  unfolding sums_def by (simp add: always_eventually setsum_nonneg setsum_enn2ereal)
+
+lemma suminf_enn2real[simp]: "(\<Sum>i. enn2ereal (f i)) = enn2ereal (suminf f)"
+  by (rule sums_unique[symmetric]) (simp add: summable_sums)
+
+lemma pcr_ennreal_enn2ereal[simp]: "pcr_ennreal (enn2ereal x) x"
+  by (simp add: ennreal.pcr_cr_eq cr_ennreal_def)
+
+lemma rel_fun_eq_pcr_ennreal: "rel_fun op = pcr_ennreal f g \<longleftrightarrow> f = enn2ereal \<circ> g"
+  by (auto simp: rel_fun_def ennreal.pcr_cr_eq cr_ennreal_def)
+
+lemma transfer_e2ennreal_suminf [transfer_rule]: "rel_fun (rel_fun op = pcr_ennreal) pcr_ennreal suminf suminf"
+  by (auto simp: rel_funI rel_fun_eq_pcr_ennreal comp_def)
+
+lemma ennreal_suminf_cmult[simp]: "(\<Sum>i. r * f i) = r * (\<Sum>i. f i::ennreal)"
+  by transfer (auto intro!: suminf_cmult_ereal)
+
+lemma ennreal_suminf_SUP_eq_directed:
+  fixes f :: "'a \<Rightarrow> nat \<Rightarrow> ennreal"
+  assumes *: "\<And>N i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> finite N \<Longrightarrow> \<exists>k\<in>I. \<forall>n\<in>N. f i n \<le> f k n \<and> f j n \<le> f k n"
+  shows "(\<Sum>n. SUP i:I. f i n) = (SUP i:I. \<Sum>n. f i n)"
+proof cases
+  assume "I \<noteq> {}"
+  then obtain i where "i \<in> I" by auto
+  from * show ?thesis
+    by (transfer fixing: I)
+       (auto simp: max_absorb2 SUP_upper2[OF \<open>i \<in> I\<close>] suminf_nonneg summable_ereal_pos \<open>I \<noteq> {}\<close>
+             intro!: suminf_SUP_eq_directed)
+qed (simp add: bot_ennreal)
+
+lemma ennreal_eq_zero_iff[simp]: "0 \<le> x \<Longrightarrow> ennreal x = 0 \<longleftrightarrow> x = 0"
+  by transfer (auto simp: max_absorb2)
+
+lemma ennreal_neq_top[simp]: "ennreal r \<noteq> top"
+  by transfer (simp add: top_ereal_def zero_ereal_def ereal_max[symmetric] del: ereal_max)
+
+lemma ennreal_of_nat_neq_top[simp]: "of_nat i \<noteq> (top::ennreal)"
+  by (induction i) auto
+
+lemma ennreal_suminf_neq_top: "summable f \<Longrightarrow> (\<And>i. 0 \<le> f i) \<Longrightarrow> (\<Sum>i. ennreal (f i)) \<noteq> top"
+  using sums_ennreal[of f "suminf f"]
+  by (simp add: suminf_nonneg sums_unique[symmetric] summable_sums_iff[symmetric] del: sums_ennreal)
+
+instance ennreal :: semiring_char_0
+proof (standard, safe intro!: linorder_injI)
+  have *: "1 + of_nat k \<noteq> (0::ennreal)" for k
+    using add_pos_nonneg[OF zero_less_one, of "of_nat k :: ennreal"] by auto
+  fix x y :: nat assume "x < y" "of_nat x = (of_nat y::ennreal)" then show False
+    by (auto simp add: less_iff_Suc_add *)
+qed
+
+lemma ennreal_suminf_lessD: "(\<Sum>i. f i :: ennreal) < x \<Longrightarrow> f i < x"
+  using le_less_trans[OF setsum_le_suminf[OF summableI, of "{i}" f]] by simp
+
+lemma ennreal_less_top[simp]: "ennreal x < top"
+  by transfer (simp add: top_ereal_def max_def)
+
+lemma ennreal_le_epsilon:
+  "(\<And>e::real. y < top \<Longrightarrow> 0 < e \<Longrightarrow> x \<le> y + ennreal e) \<Longrightarrow> x \<le> y"
+  apply (cases y rule: ennreal_cases)
+  apply (cases x rule: ennreal_cases)
+  apply (auto simp del: ennreal_plus simp add: top_unique ennreal_plus[symmetric]
+    intro: zero_less_one field_le_epsilon)
+  done
+
+lemma ennreal_less_zero_iff[simp]: "0 < ennreal x \<longleftrightarrow> 0 < x"
+  by transfer (auto simp: max_def)
+
+lemma suminf_ennreal_eq:
+  "(\<And>i. 0 \<le> f i) \<Longrightarrow> f sums x \<Longrightarrow> (\<Sum>i. ennreal (f i)) = ennreal x"
+  using suminf_nonneg[of f] sums_unique[of f x]
+  by (intro sums_unique[symmetric]) (auto simp: summable_sums_iff)
+
+lemma transfer_e2ennreal_sumset [transfer_rule]:
+  "rel_fun (rel_fun op = pcr_ennreal) (rel_fun op = pcr_ennreal) setsum setsum"
+  by (auto intro!: rel_funI simp: rel_fun_eq_pcr_ennreal comp_def)
+
+lemma ennreal_suminf_bound_add:
+  fixes f :: "nat \<Rightarrow> ennreal"
+  shows "(\<And>N. (\<Sum>n<N. f n) + y \<le> x) \<Longrightarrow> suminf f + y \<le> x"
+  by transfer (auto intro!: suminf_bound_add)
+
 end
diff -r ace69956d018 -r 85ed00c1fe7c src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Fri Feb 12 16:09:07 2016 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Fri Feb 19 13:40:50 2016 +0100
@@ -40,7 +40,7 @@
 qed
 
 lemma continuous_at_left_imp_sup_continuous:
-  fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology}"
+  fixes f :: "'a::{complete_linorder, linorder_topology} \<Rightarrow> 'b::{complete_linorder, linorder_topology}"
   assumes "mono f" "\<And>x. continuous (at_left x) f"
   shows "sup_continuous f"
   unfolding sup_continuous_def
@@ -50,7 +50,8 @@
 qed
 
 lemma sup_continuous_at_left:
-  fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology, first_countable_topology}"
+  fixes f :: "'a::{complete_linorder, linorder_topology, first_countable_topology} \<Rightarrow>
+    'b::{complete_linorder, linorder_topology}"
   assumes f: "sup_continuous f"
   shows "continuous (at_left x) f"
 proof cases
@@ -71,13 +72,14 @@
 qed
 
 lemma sup_continuous_iff_at_left:
-  fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology, first_countable_topology}"
+  fixes f :: "'a::{complete_linorder, linorder_topology, first_countable_topology} \<Rightarrow>
+    'b::{complete_linorder, linorder_topology}"
   shows "sup_continuous f \<longleftrightarrow> (\<forall>x. continuous (at_left x) f) \<and> mono f"
   using sup_continuous_at_left[of f] continuous_at_left_imp_sup_continuous[of f]
     sup_continuous_mono[of f] by auto
 
 lemma continuous_at_right_imp_inf_continuous:
-  fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology}"
+  fixes f :: "'a::{complete_linorder, linorder_topology} \<Rightarrow> 'b::{complete_linorder, linorder_topology}"
   assumes "mono f" "\<And>x. continuous (at_right x) f"
   shows "inf_continuous f"
   unfolding inf_continuous_def
@@ -87,7 +89,8 @@
 qed
 
 lemma inf_continuous_at_right:
-  fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology, first_countable_topology}"
+  fixes f :: "'a::{complete_linorder, linorder_topology, first_countable_topology} \<Rightarrow>
+    'b::{complete_linorder, linorder_topology}"
   assumes f: "inf_continuous f"
   shows "continuous (at_right x) f"
 proof cases
@@ -108,7 +111,8 @@
 qed
 
 lemma inf_continuous_iff_at_right:
-  fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology, first_countable_topology}"
+  fixes f :: "'a::{complete_linorder, linorder_topology, first_countable_topology} \<Rightarrow>
+    'b::{complete_linorder, linorder_topology}"
   shows "inf_continuous f \<longleftrightarrow> (\<forall>x. continuous (at_right x) f) \<and> mono f"
   using inf_continuous_at_right[of f] continuous_at_right_imp_inf_continuous[of f]
     inf_continuous_mono[of f] by auto
diff -r ace69956d018 -r 85ed00c1fe7c src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Feb 12 16:09:07 2016 +0100
+++ b/src/HOL/Library/Multiset.thy	Fri Feb 19 13:40:50 2016 +0100
@@ -305,6 +305,9 @@
 interpretation subset_mset: ordered_cancel_comm_monoid_diff  "op +" 0 "op \<le>#" "op <#" "op -"
   by standard (simp, fact mset_le_exists_conv)
 
+declare subset_mset.zero_order[simp del]
+  -- \<open>this removes some simp rules not in the usual order for multisets\<close>
+
 lemma mset_le_mono_add_right_cancel [simp]: "(A::'a multiset) + C \<le># B + C \<longleftrightarrow> A \<le># B"
   by (fact subset_mset.add_le_cancel_right)
 
@@ -382,7 +385,7 @@
   by (fact subset_mset.add_less_imp_less_right)
 
 lemma mset_less_empty_nonempty: "{#} <# S \<longleftrightarrow> S \<noteq> {#}"
-  by (auto simp: subset_mset_def subseteq_mset_def)
+  by (fact subset_mset.zero_less_iff_neq_zero)
 
 lemma mset_less_diff_self: "c \<in># B \<Longrightarrow> B - {#c#} <# B"
   by (auto simp: subset_mset_def subseteq_mset_def multiset_eq_iff)
diff -r ace69956d018 -r 85ed00c1fe7c src/HOL/NSA/HyperNat.thy
--- a/src/HOL/NSA/HyperNat.thy	Fri Feb 12 16:09:07 2016 +0100
+++ b/src/HOL/NSA/HyperNat.thy	Fri Feb 19 13:40:50 2016 +0100
@@ -2,7 +2,7 @@
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
 
-Converted to Isar and polished by lcp    
+Converted to Isar and polished by lcp
 *)
 
 section\<open>Hypernatural numbers\<close>
@@ -108,7 +108,7 @@
 by transfer (rule le_add2)
 
 lemma hypnat_add_one_self_less [simp]: "(x::hypnat) < x + (1::hypnat)"
-by (insert add_strict_left_mono [OF zero_less_one], auto)
+  by (fact less_add_one)
 
 lemma hypnat_neq0_conv [iff]: "!!n. (n \<noteq> 0) = (0 < (n::hypnat))"
 by transfer (rule neq0_conv)
@@ -117,14 +117,10 @@
 by (auto simp add: linorder_not_less [symmetric])
 
 lemma hypnat_gt_zero_iff2: "(0 < n) = (\<exists>m. n = m + (1::hypnat))"
-apply safe
- apply (rule_tac x = "n - (1::hypnat) " in exI)
- apply (simp add: hypnat_gt_zero_iff) 
-apply (insert add_le_less_mono [OF _ zero_less_one, of 0], auto) 
-done
+  by (auto intro!: add_nonneg_pos exI[of _ "n - 1"] simp: hypnat_gt_zero_iff)
 
 lemma hypnat_add_self_not_less: "~ (x + y < (x::hypnat))"
-by (simp add: linorder_not_le [symmetric] add.commute [of x]) 
+by (simp add: linorder_not_le [symmetric] add.commute [of x])
 
 lemma hypnat_diff_split:
     "P(a - b::hypnat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
@@ -132,12 +128,12 @@
 proof (cases "a<b" rule: case_split)
   case True
     thus ?thesis
-      by (auto simp add: hypnat_add_self_not_less order_less_imp_le 
+      by (auto simp add: hypnat_add_self_not_less order_less_imp_le
                          hypnat_diff_is_0_eq [THEN iffD2])
 next
   case False
     thus ?thesis
-      by (auto simp add: linorder_not_less dest: order_le_less_trans) 
+      by (auto simp add: linorder_not_less dest: order_le_less_trans)
 qed
 
 subsection\<open>Properties of the set of embedded natural numbers\<close>
@@ -163,10 +159,10 @@
 
 lemma of_nat_eq_add [rule_format]:
      "\<forall>d::hypnat. of_nat m = of_nat n + d --> d \<in> range of_nat"
-apply (induct n) 
-apply (auto simp add: add.assoc) 
-apply (case_tac x) 
-apply (auto simp add: add.commute [of 1]) 
+apply (induct n)
+apply (auto simp add: add.assoc)
+apply (case_tac x)
+apply (auto simp add: add.commute [of 1])
 done
 
 lemma Nats_diff [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> (a-b :: hypnat) \<in> Nats"
@@ -337,7 +333,7 @@
 done
 
 
-subsubsection\<open>Alternative Characterization of @{term HNatInfinite} using 
+subsubsection\<open>Alternative Characterization of @{term HNatInfinite} using
 Free Ultrafilter\<close>
 
 lemma HNatInfinite_FreeUltrafilterNat:
@@ -353,7 +349,7 @@
 
 lemma HNatInfinite_FreeUltrafilterNat_iff:
      "(star_n X \<in> HNatInfinite) = (\<forall>u. eventually (\<lambda>n. u < X n) FreeUltrafilterNat)"
-by (rule iffI [OF HNatInfinite_FreeUltrafilterNat 
+by (rule iffI [OF HNatInfinite_FreeUltrafilterNat
                  FreeUltrafilterNat_HNatInfinite])
 
 subsection \<open>Embedding of the Hypernaturals into other types\<close>
diff -r ace69956d018 -r 85ed00c1fe7c src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Fri Feb 12 16:09:07 2016 +0100
+++ b/src/HOL/NSA/StarDef.thy	Fri Feb 19 13:40:50 2016 +0100
@@ -987,7 +987,8 @@
 lemma star_of_of_int [simp]: "star_of (of_int z) = of_int z"
 by transfer (rule refl)
 
-instance star :: (semiring_char_0) semiring_char_0 proof
+instance star :: (semiring_char_0) semiring_char_0
+proof
   have "inj (star_of :: 'a \<Rightarrow> 'a star)" by (rule injI) simp
   then have "inj (star_of \<circ> of_nat :: nat \<Rightarrow> 'a star)" using inj_of_nat by (rule inj_comp)
   then show "inj (of_nat :: nat \<Rightarrow> 'a star)" by (simp add: comp_def)
diff -r ace69956d018 -r 85ed00c1fe7c src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Fri Feb 12 16:09:07 2016 +0100
+++ b/src/HOL/Nat.thy	Fri Feb 19 13:40:50 2016 +0100
@@ -752,6 +752,10 @@
 
 instance nat :: dioid
   proof qed (rule nat_le_iff_add)
+declare le0[simp del] -- \<open>This is now @{thm zero_le}\<close>
+declare le_0_eq[simp del] -- \<open>This is now @{thm le_zero_eq}\<close>
+declare not_less0[simp del] -- \<open>This is now @{thm not_less_zero}\<close>
+declare not_gr0[simp del] -- \<open>This is now @{thm not_gr_zero}\<close>
 
 instance nat :: ordered_cancel_comm_monoid_add
   proof qed
diff -r ace69956d018 -r 85ed00c1fe7c src/HOL/Quotient_Examples/Int_Pow.thy
--- a/src/HOL/Quotient_Examples/Int_Pow.thy	Fri Feb 12 16:09:07 2016 +0100
+++ b/src/HOL/Quotient_Examples/Int_Pow.thy	Fri Feb 19 13:40:50 2016 +0100
@@ -5,12 +5,12 @@
 
 theory Int_Pow
 imports Main "~~/src/HOL/Algebra/Group"
-begin                          
+begin
 
 (*
   This file demonstrates how to restore Lifting/Transfer enviromenent.
 
-  We want to define int_pow (a power with an integer exponent) by directly accessing 
+  We want to define int_pow (a power with an integer exponent) by directly accessing
   the representation type "nat * nat" that was used to define integers.
 *)
 
@@ -19,7 +19,7 @@
 
 (* first some additional lemmas that are missing in monoid *)
 
-lemma Units_nat_pow_Units [intro, simp]: 
+lemma Units_nat_pow_Units [intro, simp]:
   "a \<in> Units G \<Longrightarrow> a (^) (c :: nat) \<in> Units G" by (induct c) auto
 
 lemma Units_r_cancel [simp]:
@@ -47,13 +47,13 @@
   with G show ?thesis by (simp del: Units_l_inv)
 qed
 
-lemma mult_same_comm: 
-  assumes [simp, intro]: "a \<in> Units G" 
+lemma mult_same_comm:
+  assumes [simp, intro]: "a \<in> Units G"
   shows "a (^) (m::nat) \<otimes> inv (a (^) (n::nat)) = inv (a (^) n) \<otimes> a (^) m"
 proof (cases "m\<ge>n")
   have [simp]: "a \<in> carrier G" using `a \<in> _` by (rule Units_closed)
   case True
-    then obtain k where *:"m = k + n" and **:"m = n + k" by (metis Nat.le_iff_add add.commute)
+    then obtain k where *:"m = k + n" and **:"m = n + k" by (metis le_iff_add add.commute)
     have "a (^) (m::nat) \<otimes> inv (a (^) (n::nat)) = a (^) k"
       using * by (auto simp add: nat_pow_mult[symmetric] m_assoc)
     also have "\<dots> = inv (a (^) n) \<otimes> a (^) m"
@@ -62,8 +62,8 @@
 next
   have [simp]: "a \<in> carrier G" using `a \<in> _` by (rule Units_closed)
   case False
-    then obtain k where *:"n = k + m" and **:"n = m + k" 
-      by (metis Nat.le_iff_add add.commute nat_le_linear)
+    then obtain k where *:"n = k + m" and **:"n = m + k"
+      by (metis le_iff_add add.commute nat_le_linear)
     have "a (^) (m::nat) \<otimes> inv (a (^) (n::nat)) = inv(a (^) k)"
       using * by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric] inv_mult_units)
     also have "\<dots> = inv (a (^) n) \<otimes> a (^) m"
@@ -71,7 +71,7 @@
     finally show ?thesis .
 qed
 
-lemma mult_inv_same_comm: 
+lemma mult_inv_same_comm:
   "a \<in> Units G \<Longrightarrow> inv (a (^) (m::nat)) \<otimes> inv (a (^) (n::nat)) = inv (a (^) n) \<otimes> inv (a (^) m)"
 by (simp add: inv_mult_units[symmetric] nat_pow_mult ac_simps Units_closed)
 
@@ -86,21 +86,21 @@
 proof(cases "b\<ge>c")
   have [simp]: "a \<in> carrier G" using `a \<in> _` by (rule Units_closed)
   case True
-    then obtain n where "b = n + c" by (metis Nat.le_iff_add add.commute)
+    then obtain n where "b = n + c" by (metis le_iff_add add.commute)
     then have "d = n + e" using eq by arith
-    from `b = _` have "a (^) b \<otimes> inv (a (^) c) = a (^) n" 
+    from `b = _` have "a (^) b \<otimes> inv (a (^) c) = a (^) n"
       by (auto simp add: nat_pow_mult[symmetric] m_assoc)
-    also from `d = _`  have "\<dots> = a (^) d \<otimes> inv (a (^) e)"   
+    also from `d = _`  have "\<dots> = a (^) d \<otimes> inv (a (^) e)"
       by (auto simp add: nat_pow_mult[symmetric] m_assoc)
     finally show ?thesis .
 next
   have [simp]: "a \<in> carrier G" using `a \<in> _` by (rule Units_closed)
   case False
-    then obtain n where "c = n + b" by (metis Nat.le_iff_add add.commute nat_le_linear)
+    then obtain n where "c = n + b" by (metis le_iff_add add.commute nat_le_linear)
     then have "e = n + d" using eq by arith
-    from `c = _` have "a (^) b \<otimes> inv (a (^) c) = inv (a (^) n)" 
+    from `c = _` have "a (^) b \<otimes> inv (a (^) c) = inv (a (^) n)"
       by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric] inv_mult_units)
-    also from `e = _` have "\<dots> = a (^) d \<otimes> inv (a (^) e)"   
+    also from `e = _` have "\<dots> = a (^) d \<otimes> inv (a (^) e)"
       by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric] inv_mult_units)
     finally show ?thesis .
 qed
@@ -110,12 +110,12 @@
   it doesn't contain a test z < 0 when a (^) z is being defined.
 *)
 
-lift_definition int_pow :: "('a, 'm) monoid_scheme \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow> 'a" is 
-  "\<lambda>G a (n1, n2). if a \<in> Units G \<and> monoid G then (a (^)\<^bsub>G\<^esub> n1) \<otimes>\<^bsub>G\<^esub> (inv\<^bsub>G\<^esub> (a (^)\<^bsub>G\<^esub> n2)) else \<one>\<^bsub>G\<^esub>" 
+lift_definition int_pow :: "('a, 'm) monoid_scheme \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow> 'a" is
+  "\<lambda>G a (n1, n2). if a \<in> Units G \<and> monoid G then (a (^)\<^bsub>G\<^esub> n1) \<otimes>\<^bsub>G\<^esub> (inv\<^bsub>G\<^esub> (a (^)\<^bsub>G\<^esub> n2)) else \<one>\<^bsub>G\<^esub>"
 unfolding intrel_def by (auto intro: monoid.int_pow_rsp)
 
 (*
-  Thus, for example, the proof of distributivity of int_pow and addition 
+  Thus, for example, the proof of distributivity of int_pow and addition
   doesn't require a substantial number of case distinctions.
 *)
 
@@ -125,7 +125,7 @@
 proof -
   {
     fix k l m :: nat
-    have "a (^) l \<otimes> (inv (a (^) m) \<otimes> inv (a (^) k)) = (a (^) l \<otimes> inv (a (^) k)) \<otimes> inv (a (^) m)" 
+    have "a (^) l \<otimes> (inv (a (^) m) \<otimes> inv (a (^) k)) = (a (^) l \<otimes> inv (a (^) k)) \<otimes> inv (a (^) m)"
       (is "?lhs = _")
       by (simp add: mult_inv_same_comm m_assoc Units_closed)
     also have "\<dots> = (inv (a (^) k) \<otimes> a (^) l) \<otimes> inv (a (^) m)"
diff -r ace69956d018 -r 85ed00c1fe7c src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Fri Feb 12 16:09:07 2016 +0100
+++ b/src/HOL/Rings.thy	Fri Feb 19 13:40:50 2016 +0100
@@ -1312,7 +1312,7 @@
 lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0"
 by (drule mult_right_mono [of b 0], auto)
 
-lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0"
+lemma split_mult_neg_le: "(0 \<le> a \<and> b \<le> 0) \<or> (a \<le> 0 \<and> 0 \<le> b) \<Longrightarrow> a * b \<le> 0"
 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
 
 end
@@ -1735,17 +1735,51 @@
 
 end
 
-class linordered_semidom = semidom + linordered_comm_semiring_strict +
+class zero_less_one = order + zero + one +
   assumes zero_less_one [simp]: "0 < 1"
+
+class linordered_nonzero_semiring = ordered_comm_semiring + monoid_mult + linorder + zero_less_one
+begin
+
+subclass zero_neq_one
+  proof qed (insert zero_less_one, blast)
+
+subclass comm_semiring_1
+  proof qed (rule mult_1_left)
+
+lemma zero_le_one [simp]: "0 \<le> 1"
+by (rule zero_less_one [THEN less_imp_le])
+
+lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"
+by (simp add: not_le)
+
+lemma not_one_less_zero [simp]: "\<not> 1 < 0"
+by (simp add: not_less)
+
+lemma mult_left_le: "c \<le> 1 \<Longrightarrow> 0 \<le> a \<Longrightarrow> a * c \<le> a"
+  using mult_left_mono[of c 1 a] by simp
+
+lemma mult_le_one: "a \<le> 1 \<Longrightarrow> 0 \<le> b \<Longrightarrow> b \<le> 1 \<Longrightarrow> a * b \<le> 1"
+  using mult_mono[of a 1 b 1] by simp
+
+lemma zero_less_two: "0 < 1 + 1"
+  using add_pos_pos[OF zero_less_one zero_less_one] .
+
+end
+
+class linordered_semidom = semidom + linordered_comm_semiring_strict + zero_less_one +
   assumes le_add_diff_inverse2 [simp]: "b \<le> a \<Longrightarrow> a - b + b = a"
 begin
 
+subclass linordered_nonzero_semiring
+  proof qed
+
 text \<open>Addition is the inverse of subtraction.\<close>
 
 lemma le_add_diff_inverse [simp]: "b \<le> a \<Longrightarrow> b + (a - b) = a"
   by (frule le_add_diff_inverse2) (simp add: add.commute)
 
-lemma add_diff_inverse: "~ a<b \<Longrightarrow> b + (a - b) = a"
+lemma add_diff_inverse: "\<not> a < b \<Longrightarrow> b + (a - b) = a"
   by simp
 
 lemma add_le_imp_le_diff:
@@ -1771,36 +1805,14 @@
     by (simp add: add.commute diff_diff_add)
 qed
 
-lemma pos_add_strict:
-  shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
-  using add_strict_mono [of 0 a b c] by simp
-
-lemma zero_le_one [simp]: "0 \<le> 1"
-by (rule zero_less_one [THEN less_imp_le])
-
-lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"
-by (simp add: not_le)
-
-lemma not_one_less_zero [simp]: "\<not> 1 < 0"
-by (simp add: not_less)
-
 lemma less_1_mult:
-  assumes "1 < m" and "1 < n"
-  shows "1 < m * n"
-  using assms mult_strict_mono [of 1 m 1 n]
-    by (simp add:  less_trans [OF zero_less_one])
-
-lemma mult_left_le: "c \<le> 1 \<Longrightarrow> 0 \<le> a \<Longrightarrow> a * c \<le> a"
-  using mult_left_mono[of c 1 a] by simp
-
-lemma mult_le_one: "a \<le> 1 \<Longrightarrow> 0 \<le> b \<Longrightarrow> b \<le> 1 \<Longrightarrow> a * b \<le> 1"
-  using mult_mono[of a 1 b 1] by simp
+  "1 < m \<Longrightarrow> 1 < n \<Longrightarrow> 1 < m * n"
+  using mult_strict_mono [of 1 m 1 n] by (simp add: less_trans [OF zero_less_one])
 
 end
 
-class linordered_idom = comm_ring_1 +
-  linordered_comm_semiring_strict + ordered_ab_group_add +
-  abs_if + sgn_if
+class linordered_idom =
+  comm_ring_1 + linordered_comm_semiring_strict + ordered_ab_group_add + abs_if + sgn_if
 begin
 
 subclass linordered_semiring_1_strict ..
@@ -1962,9 +1974,6 @@
   thus ?thesis by simp
 qed
 
-lemma zero_less_two: "0 < 1 + 1"
-by (blast intro: less_trans zero_less_one less_add_one)
-
 end
 
 context linordered_idom