# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1493732057 -3600
# Node ID eba08da54c6b59e995c16609b1fccd0e10f4b846
# Parent  45632d594bdb912e02ee62250a58025b3ef6f396# Parent  378a2f11bec97318dce834933fdf4e4b4c8408c0
Automated merge with bundle:/var/folders/9z/l1x9y3bd16x9_70pdp4703jr0000gp/T/SourceTreeTemp.VldMQI

diff -r 45632d594bdb -r eba08da54c6b src/HOL/Analysis/Bochner_Integration.thy
--- a/src/HOL/Analysis/Bochner_Integration.thy	Tue May 02 11:05:04 2017 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy	Tue May 02 14:34:17 2017 +0100
@@ -444,7 +444,7 @@
 lemma simple_bochner_integral_nonneg[simp]:
   fixes f :: "'a \<Rightarrow> real"
   shows "(\<And>x. 0 \<le> f x) \<Longrightarrow> 0 \<le> simple_bochner_integral M f"
-  by (simp add: sum_nonneg simple_bochner_integral_def)
+  by (force simp add: simple_bochner_integral_def intro: sum_nonneg)
 
 lemma simple_bochner_integral_eq_nn_integral:
   assumes f: "simple_bochner_integrable M f" "\<And>x. 0 \<le> f x"
diff -r 45632d594bdb -r eba08da54c6b src/HOL/Analysis/Caratheodory.thy
--- a/src/HOL/Analysis/Caratheodory.thy	Tue May 02 11:05:04 2017 +0200
+++ b/src/HOL/Analysis/Caratheodory.thy	Tue May 02 14:34:17 2017 +0100
@@ -30,7 +30,7 @@
       then have "a < ?M fst" "b < ?M snd"
         by (auto intro!: Max_ge le_imp_less_Suc image_eqI) }
     then have "sum f (prod_decode ` {..<n}) \<le> sum f ({..<?M fst} \<times> {..<?M snd})"
-      by (auto intro!: sum_mono3)
+      by (auto intro!: sum_mono2)
     then show "\<exists>a b. sum f (prod_decode ` {..<n}) \<le> sum f ({..<a} \<times> {..<b})" by auto
   next
     fix a b
@@ -38,7 +38,7 @@
     { fix a' b' assume "a' < a" "b' < b" then have "(a', b') \<in> ?M"
         by (auto intro!: Max_ge le_imp_less_Suc image_eqI[where x="prod_encode (a', b')"]) }
     then have "sum f ({..<a} \<times> {..<b}) \<le> sum f ?M"
-      by (auto intro!: sum_mono3)
+      by (auto intro!: sum_mono2)
     then show "\<exists>n. sum f ({..<a} \<times> {..<b}) \<le> sum f (prod_decode ` {..<n})"
       by auto
   qed
diff -r 45632d594bdb -r eba08da54c6b src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue May 02 11:05:04 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue May 02 14:34:17 2017 +0100
@@ -1969,23 +1969,7 @@
       qed auto
     qed
     note p'= tagged_division_ofD[OF p[THEN conjunct1]] and p''=division_of_tagged_division[OF p[THEN conjunct1]]
-    show "norm ((\<Sum>(x, ka)\<in>p. content ka *\<^sub>R ?i x) - 0) < e"
-      unfolding diff_0_right *
-      unfolding real_scaleR_def real_norm_def
-      apply (subst abs_of_nonneg)
-      apply (rule sum_nonneg)
-      apply rule
-      unfolding split_paired_all split_conv
-      apply (rule mult_nonneg_nonneg)
-      apply (drule p'(4))
-      apply (erule exE)+
-      apply(rule_tac b=b in back_subst)
-      prefer 2
-      apply (subst(asm) eq_commute)
-      apply assumption
-      apply (subst interval_doublesplit[OF k])
-      apply (rule content_pos_le)
-      apply (rule indicator_pos_le)
+    have "(\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * indicator {x. x \<bullet> k = c} x) < e"
     proof -
       have "(\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * ?i x) \<le>
         (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}))"
@@ -2037,11 +2021,14 @@
       qed
       finally show "(\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * ?i x) < e" .
     qed
+    then show "norm ((\<Sum>(x, ka)\<in>p. content ka *\<^sub>R ?i x) - 0) < e"
+      unfolding * real_norm_def
+      apply (subst abs_of_nonneg)
+      using measure_nonneg  by (force simp add: indicator_def intro: sum_nonneg)+
   qed
 qed
 
 
-
 subsection \<open>Hence the main theorem about negligible sets.\<close>
 
 lemma has_integral_negligible:
@@ -3876,26 +3863,17 @@
       have *: "\<And>x s1 s2::real. 0 \<le> s1 \<Longrightarrow> x \<le> (s1 + s2) / 2 \<Longrightarrow> x - s1 \<le> s2 / 2"
         by auto
       case 2
-      show ?case
-        apply (rule *)
-        apply (rule sum_nonneg)
-        apply rule
-        apply (unfold split_paired_all split_conv)
-        defer
-        unfolding sum.union_disjoint[OF pA(2-),symmetric] pA(1)[symmetric]
-        unfolding sum_distrib_left[symmetric]
-        apply (subst additive_tagged_division_1[OF _ as(1)])
-        apply (rule assms)
+      have ge0: "0 \<le> e * (Sup k - Inf k)" if xkp: "(x, k) \<in> p \<inter> {t. fst t \<in> {a, b}}" for x k
       proof -
-        fix x k
-        assume "(x, k) \<in> p \<inter> {t. fst t \<in> {a, b}}"
-        note xk=IntD1[OF this]
-        from p(4)[OF this] guess u v by (elim exE) note uv=this
-        with p(2)[OF xk] have "cbox u v \<noteq> {}"
-          by auto
+        obtain u v where uv: "k = cbox u v"
+          by (meson Int_iff xkp p(4))
+        with p(2) that uv have "cbox u v \<noteq> {}"
+          by blast
         then show "0 \<le> e * ((Sup k) - (Inf k))"
           unfolding uv using e by (auto simp add: field_simps)
-      next
+      qed
+      have **: "norm (\<Sum>(x, k)\<in>p \<inter> {t. fst t \<in> {a, b}}. content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) \<le> e * (b - a) / 2"
+      proof -
         have *: "\<And>s f t e. sum f s = sum f t \<Longrightarrow> norm (sum f t) \<le> e \<Longrightarrow> norm (sum f s) \<le> e"
           by auto
         show "norm (\<Sum>(x, k)\<in>p \<inter> ?A. content k *\<^sub>R f' x -
@@ -4122,6 +4100,15 @@
           qed (insert p(1) ab e, auto simp add: field_simps)
         qed auto
       qed
+      show ?case
+        apply (rule * [OF sum_nonneg])
+        using ge0 apply (force simp add: )
+        unfolding sum.union_disjoint[OF pA(2-),symmetric] pA(1)[symmetric]
+        unfolding sum_distrib_left[symmetric]
+        apply (subst additive_tagged_division_1[OF _ as(1)])
+         apply (rule assms)
+        apply (rule **)
+        done
     qed
   qed
 qed
diff -r 45632d594bdb -r eba08da54c6b src/HOL/Analysis/Lebesgue_Measure.thy
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Tue May 02 11:05:04 2017 +0200
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Tue May 02 14:34:17 2017 +0100
@@ -281,7 +281,7 @@
     also have "... = (\<Sum>i\<in>S. F (r i) - F (l i)) + epsilon"
       by auto
     also have "... \<le> (\<Sum>i\<le>n. F (r i) - F (l i)) + epsilon"
-      using finS Sbound Sprop by (auto intro!: add_right_mono sum_mono3)
+      using finS Sbound Sprop by (auto intro!: add_right_mono sum_mono2)
     finally have "ennreal (F b - F a) \<le> (\<Sum>i\<le>n. ennreal (F (r i) - F (l i))) + epsilon"
       using egt0 by (simp add: ennreal_plus[symmetric] sum_nonneg del: ennreal_plus)
     then show "ennreal (F b - F a) \<le> (\<Sum>i. ennreal (F (r i) - F (l i))) + (epsilon :: real)"
diff -r 45632d594bdb -r eba08da54c6b src/HOL/Analysis/Linear_Algebra.thy
--- a/src/HOL/Analysis/Linear_Algebra.thy	Tue May 02 11:05:04 2017 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Tue May 02 14:34:17 2017 +0100
@@ -1480,12 +1480,6 @@
     and "finite S \<Longrightarrow> sum f (insert x S) = (if x \<in> S then sum f S else f x + sum f S)"
   by (auto simp add: insert_absorb)
 
-lemma sum_norm_le:
-  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
-  assumes fg: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> g x"
-  shows "norm (sum f S) \<le> sum g S"
-  by (rule order_trans [OF norm_sum sum_mono]) (simp add: fg)
-
 lemma sum_norm_bound:
   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   assumes K: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> K"
diff -r 45632d594bdb -r eba08da54c6b src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Tue May 02 11:05:04 2017 +0200
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Tue May 02 14:34:17 2017 +0100
@@ -1143,7 +1143,7 @@
     unfolding nn_integral_sum[OF f] ..
   also have "\<dots> = \<integral>\<^sup>+x. (SUP n. \<Sum>i<n. f i x) \<partial>M" using f all_pos
     by (intro nn_integral_monotone_convergence_SUP_AE[symmetric])
-       (elim AE_mp, auto simp: sum_nonneg simp del: sum_lessThan_Suc intro!: AE_I2 sum_mono3)
+       (elim AE_mp, auto simp: sum_nonneg simp del: sum_lessThan_Suc intro!: AE_I2 sum_mono2)
   also have "\<dots> = \<integral>\<^sup>+x. (\<Sum>i. f i x) \<partial>M" using all_pos
     by (intro nn_integral_cong_AE) (auto simp: suminf_eq_SUP)
   finally show ?thesis by simp
diff -r 45632d594bdb -r eba08da54c6b src/HOL/Analysis/Polytope.thy
--- a/src/HOL/Analysis/Polytope.thy	Tue May 02 11:05:04 2017 +0200
+++ b/src/HOL/Analysis/Polytope.thy	Tue May 02 14:34:17 2017 +0100
@@ -311,7 +311,7 @@
     proof (cases "sum c (S - T) = 0")
       case True
       have ci0: "\<And>i. i \<in> (S - T) \<Longrightarrow> c i = 0"
-        using True cge0 by (simp add: \<open>finite S\<close> sum_nonneg_eq_0_iff)
+        using True cge0 fin(2) sum_nonneg_eq_0_iff by auto
       have a0: "a i = 0" if "i \<in> (S - T)" for i
         using ci0 [OF that] u01 a [of i] b [of i] that
         by (simp add: c_def Groups.ordered_comm_monoid_add_class.add_nonneg_eq_0_iff)
@@ -2775,7 +2775,7 @@
         by (simp add: \<open>0 < e\<close>)
       finally show ?thesis .
     qed
-  qed (auto simp: eq poly aff face  \<open>finite \<F>'\<close>)
+  qed (auto simp: eq poly aff face \<open>finite \<F>'\<close>)
 qed
 
 end
diff -r 45632d594bdb -r eba08da54c6b src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Tue May 02 11:05:04 2017 +0200
+++ b/src/HOL/Groups_Big.thy	Tue May 02 14:34:17 2017 +0100
@@ -675,7 +675,7 @@
 context ordered_comm_monoid_add
 begin
 
-lemma sum_nonneg: "\<forall>x\<in>A. 0 \<le> f x \<Longrightarrow> 0 \<le> sum f A"
+lemma sum_nonneg: "(\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x) \<Longrightarrow> 0 \<le> sum f A"
 proof (induct A rule: infinite_finite_induct)
   case infinite
   then show ?case by simp
@@ -688,7 +688,7 @@
   with insert show ?case by simp
 qed
 
-lemma sum_nonpos: "\<forall>x\<in>A. f x \<le> 0 \<Longrightarrow> sum f A \<le> 0"
+lemma sum_nonpos: "(\<And>x. x \<in> A \<Longrightarrow> f x \<le> 0) \<Longrightarrow> sum f A \<le> 0"
 proof (induct A rule: infinite_finite_induct)
   case infinite
   then show ?case by simp
@@ -702,7 +702,7 @@
 qed
 
 lemma sum_nonneg_eq_0_iff:
-  "finite A \<Longrightarrow> \<forall>x\<in>A. 0 \<le> f x \<Longrightarrow> sum f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
+  "finite A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x) \<Longrightarrow> sum f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
   by (induct set: finite) (simp_all add: add_nonneg_eq_0_iff sum_nonneg)
 
 lemma sum_nonneg_0:
@@ -727,7 +727,7 @@
   shows "sum f A \<le> sum f B"
 proof -
   have "sum f A \<le> sum f A + sum f (B-A)"
-    by(simp add: add_increasing2[OF sum_nonneg] nn Ball_def)
+    by (auto intro: add_increasing2 [OF sum_nonneg] nn)
   also from fin finite_subset[OF sub fin] have "\<dots> = sum f (A \<union> (B-A))"
     by (simp add: sum.union_disjoint del: Un_Diff_cancel)
   also from sub have "A \<union> (B-A) = B" by blast
@@ -755,9 +755,6 @@
   finally show ?thesis .
 qed
 
-lemma sum_mono3: "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> \<forall>x\<in>B - A. 0 \<le> f x \<Longrightarrow> sum f A \<le> sum f B"
-  by (rule sum_mono2) auto
-
 end
 
 lemma (in canonically_ordered_monoid_add) sum_eq_0_iff [simp]:
@@ -1210,12 +1207,19 @@
   for c :: "nat \<Rightarrow> 'a::field"
   using sum_zero_power [of "\<lambda>i. c i / d i" A] by auto
 
-lemma (in field) prod_inversef:
-  "finite A \<Longrightarrow> prod (inverse \<circ> f) A = inverse (prod f A)"
-  by (induct A rule: finite_induct) simp_all
+lemma (in field) prod_inversef: "prod (inverse \<circ> f) A = inverse (prod f A)"
+ proof (cases "finite A")
+   case True
+   then show ?thesis
+     by (induct A rule: finite_induct) simp_all
+ next
+   case False
+   then show ?thesis
+     by auto
+ qed
 
-lemma (in field) prod_dividef: "finite A \<Longrightarrow> (\<Prod>x\<in>A. f x / g x) = prod f A / prod g A"
-  using prod_inversef [of A g] by (simp add: divide_inverse prod.distrib)
+lemma (in field) prod_dividef: "(\<Prod>x\<in>A. f x / g x) = prod f A / prod g A"
+  using prod_inversef [of g A] by (simp add: divide_inverse prod.distrib)
 
 lemma prod_Un:
   fixes f :: "'b \<Rightarrow> 'a :: field"
diff -r 45632d594bdb -r eba08da54c6b src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Tue May 02 11:05:04 2017 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Tue May 02 14:34:17 2017 +0100
@@ -223,7 +223,7 @@
 lemma suminf_eq_SUP_real:
   assumes X: "summable X" "\<And>i. 0 \<le> X i" shows "suminf X = (SUP i. \<Sum>n<i. X n::real)"
   by (intro LIMSEQ_unique[OF summable_LIMSEQ] X LIMSEQ_incseq_SUP)
-     (auto intro!: bdd_aboveI2[where M="\<Sum>i. X i"] sum_le_suminf X monoI sum_mono3)
+     (auto intro!: bdd_aboveI2[where M="\<Sum>i. X i"] sum_le_suminf X monoI sum_mono2)
 
 subsection \<open>Defining the extended non-negative reals\<close>
 
diff -r 45632d594bdb -r eba08da54c6b src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Tue May 02 11:05:04 2017 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Tue May 02 14:34:17 2017 +0100
@@ -3394,7 +3394,7 @@
     also have "\<dots> = (\<Sum>i\<in>(\<lambda>i. i + k) ` {..<n}. f i)"
       by (subst sum.reindex) auto
     also have "\<dots> \<le> sum f {..<n + k}"
-      by (intro sum_mono3) (auto simp: f)
+      by (intro sum_mono2) (auto simp: f)
     finally show "(\<Sum>i<n. f (i + k)) \<le> sum f {..<n + k}" .
   qed
 qed
diff -r 45632d594bdb -r eba08da54c6b src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Tue May 02 11:05:04 2017 +0200
+++ b/src/HOL/Limits.thy	Tue May 02 14:34:17 2017 +0100
@@ -824,6 +824,10 @@
   for f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra}"
   by (induct n) (simp_all add: tendsto_mult)
 
+lemma tendsto_null_power: "\<lbrakk>(f \<longlongrightarrow> 0) F; 0 < n\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x ^ n) \<longlongrightarrow> 0) F"
+    for f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra_1}"
+  using tendsto_power [of f 0 F n] by (simp add: power_0_left)
+
 lemma continuous_power [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. (f x)^n)"
   for f :: "'a::t2_space \<Rightarrow> 'b::{power,real_normed_algebra}"
   unfolding continuous_def by (rule tendsto_power)
diff -r 45632d594bdb -r eba08da54c6b src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Tue May 02 11:05:04 2017 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Tue May 02 14:34:17 2017 +0100
@@ -871,7 +871,7 @@
 
 lemma sum_norm_le:
   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
-  assumes fg: "\<forall>x \<in> S. norm (f x) \<le> g x"
+  assumes fg: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> g x"
   shows "norm (sum f S) \<le> sum g S"
   by (rule order_trans [OF norm_sum sum_mono]) (simp add: fg)
 
diff -r 45632d594bdb -r eba08da54c6b src/HOL/Series.thy
--- a/src/HOL/Series.thy	Tue May 02 11:05:04 2017 +0200
+++ b/src/HOL/Series.thy	Tue May 02 14:34:17 2017 +0100
@@ -1062,7 +1062,7 @@
     have "(\<Sum>i<n. f (g i)) = sum f (g ` {..<n})"
       by (simp add: sum.reindex)
     also have "\<dots> \<le> (\<Sum>i<m. f i)"
-      by (rule sum_mono3) (auto simp add: pos n[rule_format])
+      by (rule sum_mono2) (auto simp add: pos n[rule_format])
     also have "\<dots> \<le> suminf f"
       using \<open>summable f\<close> by (rule sum_le_suminf) (simp add: pos)
     finally show "(\<Sum>i<n. (f \<circ>  g) i) \<le> suminf f"
@@ -1097,7 +1097,7 @@
     also have "\<dots> = (\<Sum>i\<in>g -` {..<n}. (f \<circ> g) i)"
       by (rule sum.reindex_cong[where l=g])(auto)
     also have "\<dots> \<le> (\<Sum>i<m. (f \<circ> g) i)"
-      by (rule sum_mono3)(auto simp add: pos n)
+      by (rule sum_mono2)(auto simp add: pos n)
     also have "\<dots> \<le> suminf (f \<circ> g)"
       using \<open>summable (f \<circ> g)\<close> by (rule sum_le_suminf) (simp add: pos)
     finally show "sum f {..<n} \<le> suminf (f \<circ> g)" .
diff -r 45632d594bdb -r eba08da54c6b src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue May 02 11:05:04 2017 +0200
+++ b/src/HOL/Transcendental.thy	Tue May 02 14:34:17 2017 +0100
@@ -197,7 +197,7 @@
   also have "(\<Sum>k\<in>{0,2*n}. (2*n) choose k) \<le> (\<Sum>k\<le>1. (n choose k)\<^sup>2)"
     by (cases n) simp_all
   also from assms have "\<dots> \<le> (\<Sum>k\<le>n. (n choose k)\<^sup>2)"
-    by (intro sum_mono3) auto
+    by (intro sum_mono2) auto
   also have "\<dots> = (2*n) choose n" by (rule choose_square_sum)
   also have "(\<Sum>k\<in>{0<..<2*n}. (2*n) choose k) \<le> (\<Sum>k\<in>{0<..<2*n}. (2*n) choose n)"
     by (intro sum_mono binomial_maximum')
@@ -1774,13 +1774,13 @@
   for x :: real
   by (simp add: order_eq_iff)
 
-lemma ln_add_one_self_le_self [simp]: "0 \<le> x \<Longrightarrow> ln (1 + x) \<le> x"
+lemma ln_add_one_self_le_self: "0 \<le> x \<Longrightarrow> ln (1 + x) \<le> x"
   for x :: real
   by (rule exp_le_cancel_iff [THEN iffD1]) (simp add: exp_ge_add_one_self_aux)
 
 lemma ln_less_self [simp]: "0 < x \<Longrightarrow> ln x < x"
   for x :: real
-  by (rule order_less_le_trans [where y = "ln (1 + x)"]) simp_all
+  by (rule order_less_le_trans [where y = "ln (1 + x)"]) (simp_all add: ln_add_one_self_le_self)
 
 lemma ln_ge_iff: "\<And>x::real. 0 < x \<Longrightarrow> y \<le> ln x \<longleftrightarrow> exp y \<le> x"
   using exp_le_cancel_iff exp_total by force