# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1497884867 -3600
# Node ID 0e640e04fc567c83abc09884864c3c5dfd6a4c35
# Parent  20304512a33b8b298ae1129c410d834456e652e4
New theorems; stronger theorems; tidier theorems. Also some renaming

diff -r 20304512a33b -r 0e640e04fc56 src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sat Jun 17 20:24:22 2017 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Jun 19 16:07:47 2017 +0100
@@ -1518,7 +1518,7 @@
 lemma has_contour_integral_diff:
   "\<lbrakk>(f1 has_contour_integral i1) g; (f2 has_contour_integral i2) g\<rbrakk>
          \<Longrightarrow> ((\<lambda>x. f1 x - f2 x) has_contour_integral (i1 - i2)) g"
-  by (simp add: has_integral_sub has_contour_integral_def algebra_simps)
+  by (simp add: has_integral_diff has_contour_integral_def algebra_simps)
 
 lemma has_contour_integral_lmul:
   "(f has_contour_integral i) g \<Longrightarrow> ((\<lambda>x. c * (f x)) has_contour_integral (c*i)) g"
@@ -2486,7 +2486,7 @@
                         _ 0 1 ])
             using ynz \<open>0 < B\<close> \<open>0 < C\<close>
             apply (simp_all del: le_divide_eq_numeral1)
-            apply (simp add: has_integral_sub has_contour_integral_linepath [symmetric] has_contour_integral_integral
+            apply (simp add: has_integral_diff has_contour_integral_linepath [symmetric] has_contour_integral_integral
                              fpi_uv f_uv contour_integrable_continuous_linepath, clarify)
             apply (simp only: **)
             apply (simp add: norm_triangle_le norm_mult cmod_diff_le del: le_divide_eq_numeral1)
diff -r 20304512a33b -r 0e640e04fc56 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sat Jun 17 20:24:22 2017 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Jun 19 16:07:47 2017 +0100
@@ -385,7 +385,7 @@
       moreover have "((\<lambda>x. if x \<in> A \<inter> box a b then 1 else 0) has_integral ?M A) (box a b)"
         by (subst has_integral_restrict) (auto intro: compl)
       ultimately have "((\<lambda>x. 1 - (if x \<in> A \<inter> box a b then 1 else 0)) has_integral ?M (box a b) - ?M A) (box a b)"
-        by (rule has_integral_sub)
+        by (rule has_integral_diff)
       then have "((\<lambda>x. (if x \<in> (UNIV - A) \<inter> box a b then 1 else 0)) has_integral ?M (box a b) - ?M A) (box a b)"
         by (rule has_integral_cong[THEN iffD1, rotated 1]) auto
       then have "((\<lambda>x. 1) has_integral ?M (box a b) - ?M A) ((UNIV - A) \<inter> box a b)"
@@ -633,7 +633,7 @@
   proof
     assume int: "(\<lambda>x. 1::real) integrable_on A"
     then have "(indicator A::'a \<Rightarrow> real) integrable_on UNIV"
-      unfolding indicator_def[abs_def] integrable_restrict_univ .
+      unfolding indicator_def[abs_def] integrable_restrict_UNIV .
     then obtain r where "((indicator A::'a\<Rightarrow>real) has_integral r) UNIV"
       by auto
     from nn_integral_has_integral_lborel[OF _ _ this] emeasure_A show False
@@ -665,7 +665,7 @@
     unfolding ennreal_max_0 by auto
   then have "((\<lambda>x. max 0 (f x)) has_integral r) UNIV" "((\<lambda>x. max 0 (- f x)) has_integral q) UNIV"
     using nn_integral_has_integral[OF _ _ r] nn_integral_has_integral[OF _ _ q] by auto
-  note has_integral_sub[OF this]
+  note has_integral_diff[OF this]
   moreover have "(\<lambda>x. max 0 (f x) - max 0 (- f x)) = f"
     by auto
   ultimately show ?thesis
@@ -696,7 +696,7 @@
       ultimately have "(?F has_integral 0) UNIV"
         using has_integral_integral_real[of ?F] by simp
       then show "(indicator N has_integral (0::real)) (cbox a b)"
-        unfolding has_integral_restrict_univ .
+        unfolding has_integral_restrict_UNIV .
     qed
   qed
 qed
@@ -874,7 +874,7 @@
   have "(?f has_integral LINT x : S | lborel. f x) UNIV"
     by (rule has_integral_integral_lborel) fact
   hence 1: "(f has_integral (set_lebesgue_integral lborel S f)) S"
-    apply (subst has_integral_restrict_univ [symmetric])
+    apply (subst has_integral_restrict_UNIV [symmetric])
     apply (rule has_integral_eq)
     by auto
   thus "f integrable_on S"
@@ -890,7 +890,7 @@
   assumes f: "set_integrable lebesgue S f"
   shows "(f has_integral (LINT x:S|lebesgue. f x)) S"
   using has_integral_integral_lebesgue[OF f]
-  by (simp_all add: indicator_def if_distrib[of "\<lambda>x. x *\<^sub>R f _"] has_integral_restrict_univ cong: if_cong)
+  by (simp_all add: indicator_def if_distrib[of "\<lambda>x. x *\<^sub>R f _"] has_integral_restrict_UNIV cong: if_cong)
 
 lemma set_lebesgue_integral_eq_integral:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
@@ -921,7 +921,7 @@
     "(\<lambda>x. norm (indicator s x *\<^sub>R f x)) = (\<lambda>x. if x \<in> s then norm (f x) else 0)"
     by auto
   ultimately show "f integrable_on s" "(\<lambda>x. norm (f x)) integrable_on s"
-    by (simp_all add: integrable_restrict_univ)
+    by (simp_all add: integrable_restrict_UNIV)
 next
   assume f: "f integrable_on s" and nf: "(\<lambda>x. norm (f x)) integrable_on s"
   show "f absolutely_integrable_on s"
@@ -934,21 +934,38 @@
   qed
 qed
 
-lemma absolutely_integrable_on_iff_nonneg:
-  fixes f :: "'a :: euclidean_space \<Rightarrow> real"
-  assumes "\<And>x. 0 \<le> f x" shows "f absolutely_integrable_on s \<longleftrightarrow> f integrable_on s"
-proof -
-  from assms have "(\<lambda>x. \<bar>f x\<bar>) = f"
-    by (intro ext) auto
-  then show ?thesis
-    unfolding absolutely_integrable_on_def by simp
-qed
+lemma absolutely_integrable_restrict_UNIV:
+  "(\<lambda>x. if x \<in> s then f x else 0) absolutely_integrable_on UNIV \<longleftrightarrow> f absolutely_integrable_on s"
+  by (intro arg_cong2[where f=integrable]) auto
 
 lemma absolutely_integrable_onI:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   shows "f integrable_on s \<Longrightarrow> (\<lambda>x. norm (f x)) integrable_on s \<Longrightarrow> f absolutely_integrable_on s"
   unfolding absolutely_integrable_on_def by auto
 
+lemma nonnegative_absolutely_integrable_1:
+  fixes f :: "'a :: euclidean_space \<Rightarrow> real"
+  assumes f: "f integrable_on A" and "\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x"
+  shows "f absolutely_integrable_on A"
+  apply (rule absolutely_integrable_onI [OF f])
+  using assms by (simp add: integrable_eq)
+
+lemma absolutely_integrable_on_iff_nonneg:
+  fixes f :: "'a :: euclidean_space \<Rightarrow> real"
+  assumes "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> f x" shows "f absolutely_integrable_on S \<longleftrightarrow> f integrable_on S"
+proof -
+  { assume "f integrable_on S"
+    then have "(\<lambda>x. if x \<in> S then f x else 0) integrable_on UNIV"
+      by (simp add: integrable_restrict_UNIV)
+    then have "(\<lambda>x. if x \<in> S then f x else 0) absolutely_integrable_on UNIV"
+      using \<open>f integrable_on S\<close> absolutely_integrable_restrict_UNIV assms nonnegative_absolutely_integrable_1 by blast
+    then have "f absolutely_integrable_on S"
+      using absolutely_integrable_restrict_UNIV by blast
+  }
+  then show ?thesis        
+    unfolding absolutely_integrable_on_def by auto
+qed
+
 lemma lmeasurable_iff_integrable_on: "S \<in> lmeasurable \<longleftrightarrow> (\<lambda>x. 1::real) integrable_on S"
   by (subst absolutely_integrable_on_iff_nonneg[symmetric])
      (simp_all add: lmeasurable_iff_integrable)
@@ -994,7 +1011,7 @@
   show "negligible S"
     unfolding negligible_def
   proof (safe intro!: has_integral_iff_nn_integral_lebesgue[THEN iffD2]
-                      has_integral_restrict_univ[where s="cbox _ _", THEN iffD1])
+                      has_integral_restrict_UNIV[where s="cbox _ _", THEN iffD1])
     fix a b
     show "(\<lambda>x. if x \<in> cbox a b then indicator S x else 0) \<in> lebesgue \<rightarrow>\<^sub>M borel"
       using S by (auto intro!: measurable_If)
@@ -2209,16 +2226,12 @@
   qed
 qed
 
-lemma absolutely_integrable_restrict_univ:
-  "(\<lambda>x. if x \<in> s then f x else 0) absolutely_integrable_on UNIV \<longleftrightarrow> f absolutely_integrable_on s"
-  by (intro arg_cong2[where f=integrable]) auto
-
 lemma absolutely_integrable_add[intro]:
   fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   shows "f absolutely_integrable_on s \<Longrightarrow> g absolutely_integrable_on s \<Longrightarrow> (\<lambda>x. f x + g x) absolutely_integrable_on s"
   by (rule set_integral_add)
 
-lemma absolutely_integrable_sub[intro]:
+lemma absolutely_integrable_diff[intro]:
   fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   shows "f absolutely_integrable_on s \<Longrightarrow> g absolutely_integrable_on s \<Longrightarrow> (\<lambda>x. f x - g x) absolutely_integrable_on s"
   by (rule set_integral_diff)
diff -r 20304512a33b -r 0e640e04fc56 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sat Jun 17 20:24:22 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Jun 19 16:07:47 2017 +0100
@@ -188,6 +188,12 @@
 lemma property_empty_interval: "\<forall>a b. content (cbox a b) = 0 \<longrightarrow> P (cbox a b) \<Longrightarrow> P {}"
   using content_empty unfolding empty_as_interval by auto
 
+lemma interval_bounds_nz_content [simp]:
+  assumes "content (cbox a b) \<noteq> 0"
+  shows "interval_upperbound (cbox a b) = b"
+    and "interval_lowerbound (cbox a b) = a"
+  by (metis assms content_empty interval_bounds')+
+
 subsection \<open>Gauge integral\<close>
 
 text \<open>Case distinction to define it first on compact intervals first, then use a limit. This is only
@@ -569,7 +575,7 @@
   qed
 qed
 
-lemma has_integral_sub:
+lemma has_integral_diff:
   "(f has_integral k) s \<Longrightarrow> (g has_integral l) s \<Longrightarrow>
     ((\<lambda>x. f x - g x) has_integral (k - l)) s"
   using has_integral_add[OF _ has_integral_neg, of f k s g l]
@@ -606,7 +612,7 @@
 
 lemma integral_diff: "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow>
     integral s (\<lambda>x. f x - g x) = integral s f - integral s g"
-  by (rule integral_unique) (metis integrable_integral has_integral_sub)
+  by (rule integral_unique) (metis integrable_integral has_integral_diff)
 
 lemma integrable_0: "(\<lambda>x. 0) integrable_on s"
   unfolding integrable_on_def using has_integral_0 by auto
@@ -635,7 +641,7 @@
 
 lemma integrable_diff:
   "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow> (\<lambda>x. f x - g x) integrable_on s"
-  unfolding integrable_on_def by(auto intro: has_integral_sub)
+  unfolding integrable_on_def by(auto intro: has_integral_diff)
 
 lemma integrable_linear:
   "f integrable_on s \<Longrightarrow> bounded_linear h \<Longrightarrow> (h \<circ> f) integrable_on s"
@@ -680,7 +686,7 @@
   assumes "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
     and "(f has_integral k) s"
   shows "(g has_integral k) s"
-  using has_integral_sub[OF assms(2), of "\<lambda>x. f x - g x" 0]
+  using has_integral_diff[OF assms(2), of "\<lambda>x. f x - g x" 0]
   using has_integral_is_0[of s "\<lambda>x. f x - g x"]
   using assms(1)
   by auto
@@ -774,22 +780,10 @@
   shows "(f has_integral 0) (cbox a a)"
     and "(f has_integral 0) {a}"
 proof -
-  have *: "{a} = cbox a a"
-    apply (rule set_eqI)
-    unfolding mem_box singleton_iff euclidean_eq_iff[where 'a='a]
-    apply safe
-    prefer 3
-    apply (erule_tac x=b in ballE)
-    apply (auto simp add: field_simps)
-    done
-  show "(f has_integral 0) (cbox a a)" "(f has_integral 0) {a}"
-    unfolding *
-    apply (rule_tac[!] has_integral_null)
-    unfolding content_eq_0_interior
-    unfolding interior_cbox
-    using box_sing
-    apply auto
-    done
+  show "(f has_integral 0) (cbox a a)"
+     by (rule has_integral_null) simp
+  then show "(f has_integral 0) {a}"
+    by simp
 qed
 
 lemma integrable_on_refl[intro]: "f integrable_on cbox a a"
@@ -994,7 +988,7 @@
     unfolding k1 interval_split[OF \<open>k \<in> Basis\<close>]
     unfolding content_eq_0_interior
     unfolding interval_split[OF \<open>k \<in> Basis\<close>, symmetric] k1[symmetric]
-    by (rule tagged_division_split_left_inj[OF assms])
+    by (metis tagged_division_split_left_inj assms)
 qed
 
 lemma tagged_division_split_right_inj_content:
@@ -1008,7 +1002,7 @@
     unfolding k1 interval_split[OF \<open>k \<in> Basis\<close>]
     unfolding content_eq_0_interior
     unfolding interval_split[OF \<open>k \<in> Basis\<close>, symmetric] k1[symmetric]
-    by (rule tagged_division_split_right_inj[OF assms])
+    by (metis tagged_division_split_right_inj assms)
 qed
 
 lemma has_integral_split:
@@ -3149,7 +3143,7 @@
       then have Idiff: "?I a y - ?I a x = ?I x y"
         using False x by (simp add: algebra_simps integral_combine)
       have fux_int: "((\<lambda>u. f u - f x) has_integral integral {x..y} f - (y - x) *\<^sub>R f x) {x..y}"
-        apply (rule has_integral_sub)
+        apply (rule has_integral_diff)
         using x y apply (force intro: integrable_integral [OF integrable_subinterval_real [OF f]])
         using has_integral_const_real [of "f x" x y] False
         apply (simp add: )
@@ -3167,7 +3161,7 @@
       then have Idiff: "?I a x - ?I a y = ?I y x"
         using True x y by (simp add: algebra_simps integral_combine)
       have fux_int: "((\<lambda>u. f u - f x) has_integral integral {y..x} f - (x - y) *\<^sub>R f x) {y..x}"
-        apply (rule has_integral_sub)
+        apply (rule has_integral_diff)
         using x y apply (force intro: integrable_integral [OF integrable_subinterval_real [OF f]])
         using has_integral_const_real [of "f x" y x] True
         apply (simp add: )
@@ -5069,7 +5063,7 @@
     done
 qed
 
-lemma has_integral_restrict_univ:
+lemma has_integral_restrict_UNIV:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   shows "((\<lambda>x. if x \<in> s then f x else 0) has_integral i) UNIV \<longleftrightarrow> (f has_integral i) s"
   by auto
@@ -5088,8 +5082,8 @@
     done
   then show ?thesis
     using assms(3)
-    apply (subst has_integral_restrict_univ[symmetric])
-    apply (subst(asm) has_integral_restrict_univ[symmetric])
+    apply (subst has_integral_restrict_UNIV[symmetric])
+    apply (subst(asm) has_integral_restrict_UNIV[symmetric])
     apply auto
     done
 qed
@@ -5108,11 +5102,11 @@
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   shows "f integrable_on s \<Longrightarrow> integral UNIV (\<lambda>x. if x \<in> s then f x else 0) = integral s f"
   apply (rule integral_unique)
-  unfolding has_integral_restrict_univ
+  unfolding has_integral_restrict_UNIV
   apply auto
   done
 
-lemma integrable_restrict_univ:
+lemma integrable_restrict_UNIV:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   shows "(\<lambda>x. if x \<in> s then f x else 0) integrable_on UNIV \<longleftrightarrow> f integrable_on s"
   unfolding integrable_on_def
@@ -5164,7 +5158,7 @@
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   assumes "negligible ((s - t) \<union> (t - s))"
   shows "(f has_integral y) s \<longleftrightarrow> (f has_integral y) t"
-  unfolding has_integral_restrict_univ[symmetric,of f]
+  unfolding has_integral_restrict_UNIV[symmetric,of f]
   apply (rule has_integral_spike_eq[OF assms])
   by (auto split: if_split_asm)
 
@@ -5195,7 +5189,7 @@
     and as: "s \<subseteq> t" "(f has_integral i) s" "(f has_integral j) t" "\<forall>x\<in>t. 0 \<le> f(x)\<bullet>k"
   shows "i\<bullet>k \<le> j\<bullet>k"
 proof -
-  note has_integral_restrict_univ[symmetric, of f]
+  note has_integral_restrict_UNIV[symmetric, of f]
   note as(2-3)[unfolded this] note * = has_integral_component_le[OF k this]
   show ?thesis
     apply (rule *)
@@ -5667,7 +5661,7 @@
     and "negligible (s \<inter> t)"
   shows "(f has_integral (i + j)) (s \<union> t)"
 proof -
-  note * = has_integral_restrict_univ[symmetric, of f]
+  note * = has_integral_restrict_UNIV[symmetric, of f]
   show ?thesis
     unfolding *
     apply (rule has_integral_spike[OF assms(3)])
@@ -5700,7 +5694,7 @@
     and "\<forall>s\<in>t. \<forall>s'\<in>t. s \<noteq> s' \<longrightarrow> negligible (s \<inter> s')"
   shows "(f has_integral (sum i t)) (\<Union>t)"
 proof -
-  note * = has_integral_restrict_univ[symmetric, of f]
+  note * = has_integral_restrict_UNIV[symmetric, of f]
   have **: "negligible (\<Union>((\<lambda>(a,b). a \<inter> b) ` {(a,b). a \<in> t \<and> b \<in> {y. y \<in> t \<and> a \<noteq> y}}))"
     apply (rule negligible_Union)
     apply (rule finite_imageI)
@@ -6541,9 +6535,9 @@
       (\<lambda>x. if x \<in> t \<inter> s then f k x else 0)"
       by (rule ext) auto
     have int': "\<And>k a b. f k integrable_on cbox a b \<inter> s"
-      apply (subst integrable_restrict_univ[symmetric])
+      apply (subst integrable_restrict_UNIV[symmetric])
       apply (subst ifif[symmetric])
-      apply (subst integrable_restrict_univ)
+      apply (subst integrable_restrict_UNIV)
       apply (rule int)
       done
     have "\<And>a b. (\<lambda>x. if x \<in> s then g x else 0) integrable_on cbox a b \<and>
@@ -7237,7 +7231,7 @@
           (prod (f b) (g b) - prod (f a) (g a))) {a..b}"
     using deriv by (intro fundamental_theorem_of_calculus_interior_strong[OF s le])
                    (auto intro!: continuous_intros continuous_on has_vector_derivative)
-  from has_integral_sub[OF this int] show ?thesis by (simp add: algebra_simps)
+  from has_integral_diff[OF this int] show ?thesis by (simp add: algebra_simps)
 qed
 
 lemma integration_by_parts_interior:
diff -r 20304512a33b -r 0e640e04fc56 src/HOL/Analysis/Tagged_Division.thy
--- a/src/HOL/Analysis/Tagged_Division.thy	Sat Jun 17 20:24:22 2017 +0200
+++ b/src/HOL/Analysis/Tagged_Division.thy	Mon Jun 19 16:07:47 2017 +0100
@@ -1496,7 +1496,7 @@
     apply (erule disjE)
     apply (rule_tac x="(k,(interval_lowerbound l)\<bullet>k)" in exI, force simp add: *)
     apply (rule_tac x="(k,(interval_upperbound l)\<bullet>k)" in exI, force simp add: *)
-    done
+    done           
   moreover have "?D1 \<subseteq> ?D"
     by (auto simp add: assms division_points_subset)
   ultimately show "?D1 \<subset> ?D"
@@ -1521,47 +1521,33 @@
 qed
 
 lemma division_split_left_inj:
-  fixes type :: "'a::euclidean_space"
-  assumes "d division_of i"
-    and "k1 \<in> d"
-    and "k2 \<in> d"
-    and "k1 \<noteq> k2"
-    and "k1 \<inter> {x::'a. x\<bullet>k \<le> c} = k2 \<inter> {x. x\<bullet>k \<le> c}"
-    and k: "k\<in>Basis"
-  shows "interior (k1 \<inter> {x. x\<bullet>k \<le> c}) = {}"
+  fixes S :: "'a::euclidean_space set"
+  assumes div: "\<D> division_of S"
+    and eq: "K1 \<inter> {x::'a. x\<bullet>k \<le> c} = K2 \<inter> {x. x\<bullet>k \<le> c}"
+    and "K1 \<in> \<D>" "K2 \<in> \<D>" "K1 \<noteq> K2"
+  shows "interior (K1 \<inter> {x. x\<bullet>k \<le> c}) = {}"
 proof -
-  note d=division_ofD[OF assms(1)]
-  guess u1 v1 using d(4)[OF assms(2)] by (elim exE) note uv1=this
-  guess u2 v2 using d(4)[OF assms(3)] by (elim exE) note uv2=this
-  have **: "\<And>s t u. s \<inter> t = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<subseteq> t \<Longrightarrow> u = {}"
-    by auto
-  show ?thesis
-    unfolding uv1 uv2
-    apply (rule **[OF d(5)[OF assms(2-4)]])
-    apply (simp add: uv1)
-    using assms(5) uv1 by auto
+  have "interior K2 \<inter> interior {a. a \<bullet> k \<le> c} = interior K1 \<inter> interior {a. a \<bullet> k \<le> c}"
+    by (metis (no_types) eq interior_Int)
+  moreover have "\<And>A. interior A \<inter> interior K2 = {} \<or> A = K2 \<or> A \<notin> \<D>"
+    by (meson div \<open>K2 \<in> \<D>\<close> division_of_def)
+  ultimately show ?thesis
+    using \<open>K1 \<in> \<D>\<close> \<open>K1 \<noteq> K2\<close> by auto
 qed
 
 lemma division_split_right_inj:
-  fixes type :: "'a::euclidean_space"
-  assumes "d division_of i"
-    and "k1 \<in> d"
-    and "k2 \<in> d"
-    and "k1 \<noteq> k2"
-    and "k1 \<inter> {x::'a. x\<bullet>k \<ge> c} = k2 \<inter> {x. x\<bullet>k \<ge> c}"
-    and k: "k \<in> Basis"
-  shows "interior (k1 \<inter> {x. x\<bullet>k \<ge> c}) = {}"
+  fixes S :: "'a::euclidean_space set"
+  assumes div: "\<D> division_of S"
+    and eq: "K1 \<inter> {x::'a. x\<bullet>k \<ge> c} = K2 \<inter> {x. x\<bullet>k \<ge> c}"
+    and "K1 \<in> \<D>" "K2 \<in> \<D>" "K1 \<noteq> K2"
+  shows "interior (K1 \<inter> {x. x\<bullet>k \<ge> c}) = {}"
 proof -
-  note d=division_ofD[OF assms(1)]
-  guess u1 v1 using d(4)[OF assms(2)] by (elim exE) note uv1=this
-  guess u2 v2 using d(4)[OF assms(3)] by (elim exE) note uv2=this
-  have **: "\<And>s t u. s \<inter> t = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<subseteq> t \<Longrightarrow> u = {}"
-    by auto
-  show ?thesis
-    unfolding uv1 uv2
-    apply (rule **[OF d(5)[OF assms(2-4)]])
-    apply (simp add: uv1)
-    using assms(5) uv1 by auto
+  have "interior K2 \<inter> interior {a. a \<bullet> k \<ge> c} = interior K1 \<inter> interior {a. a \<bullet> k \<ge> c}"
+    by (metis (no_types) eq interior_Int)
+  moreover have "\<And>A. interior A \<inter> interior K2 = {} \<or> A = K2 \<or> A \<notin> \<D>"
+    by (meson div \<open>K2 \<in> \<D>\<close> division_of_def)
+  ultimately show ?thesis
+    using \<open>K1 \<in> \<D>\<close> \<open>K1 \<noteq> K2\<close> by auto
 qed
 
 lemma interval_doublesplit:
@@ -1912,18 +1898,30 @@
   by (rule tagged_division_union_interval)
 
 lemma tagged_division_split_left_inj:
-  "d tagged_division_of i \<Longrightarrow> (x1, k1) \<in> d \<Longrightarrow> (x2, k2) \<in> d \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow>
-    k1 \<inter> {x. x\<bullet>k \<le> c} = k2 \<inter> {x. x\<bullet>k \<le> c} \<Longrightarrow> k \<in> Basis \<Longrightarrow>
-    interior (k1 \<inter> {x. x\<bullet>k \<le> c}) = {}"
-  by (intro division_split_left_inj[of "snd`d" i k1 k2, OF division_of_tagged_division])
-     (auto simp add: snd_def[abs_def] image_iff split: prod.split )
+  assumes d: "d tagged_division_of i"
+  and "k1 \<noteq> k2"
+  and tags: "(x1, k1) \<in> d" "(x2, k2) \<in> d"
+  and eq: "k1 \<inter> {x. x \<bullet> k \<le> c} = k2 \<inter> {x. x \<bullet> k \<le> c}"
+    shows "interior (k1 \<inter> {x. x\<bullet>k \<le> c}) = {}"
+proof -
+  have "interior (k1 \<inter> k2) = {} \<or> (x2, k2) = (x1, k1)"
+    using tags d by (metis (no_types) interior_Int tagged_division_ofD(5))
+  then show ?thesis
+    using eq \<open>k1 \<noteq> k2\<close> by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject)
+qed
 
 lemma tagged_division_split_right_inj:
-  "d tagged_division_of i \<Longrightarrow> (x1, k1) \<in> d \<Longrightarrow> (x2, k2) \<in> d \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow>
-    k1 \<inter> {x. x\<bullet>k \<ge> c} = k2 \<inter> {x. x\<bullet>k \<ge> c} \<Longrightarrow> k \<in> Basis \<Longrightarrow>
-    interior (k1 \<inter> {x. x\<bullet>k \<ge> c}) = {}"
-  by (intro division_split_right_inj[of "snd`d" i k1 k2, OF division_of_tagged_division])
-     (auto simp add: snd_def[abs_def] image_iff split: prod.split )
+  assumes d: "d tagged_division_of i"
+  and "k1 \<noteq> k2"
+  and tags: "(x1, k1) \<in> d" "(x2, k2) \<in> d"
+  and eq: "k1 \<inter> {x. x\<bullet>k \<ge> c} = k2 \<inter> {x. x\<bullet>k \<ge> c}"
+    shows "interior (k1 \<inter> {x. x\<bullet>k \<ge> c}) = {}"
+proof -
+  have "interior (k1 \<inter> k2) = {} \<or> (x2, k2) = (x1, k1)"
+    using tags d by (metis (no_types) interior_Int tagged_division_ofD(5))
+  then show ?thesis
+    using eq \<open>k1 \<noteq> k2\<close> by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject)
+qed
 
 subsection \<open>Special case of additivity we need for the FTC.\<close>
 
@@ -1934,22 +1932,21 @@
   shows "sum (\<lambda>(x,k). f(Sup k) - f(Inf k)) p = f b - f a"
 proof -
   let ?f = "(\<lambda>k::(real) set. if k = {} then 0 else f(interval_upperbound k) - f(interval_lowerbound k))"
-  have ***: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
-    using assms by auto
+  have p_td: "p tagged_division_of cbox a b"
+    using assms(2) box_real(2) by presburger
   have *: "add.operative ?f"
-    unfolding add.operative_1_lt box_eq_empty
-    by auto
+    unfolding add.operative_1_lt box_eq_empty by auto
   have **: "cbox a b \<noteq> {}"
     using assms(1) by auto
-  note sum.operative_tagged_division[OF * assms(2)[simplified box_real[symmetric]]]
-  note * = this[unfolded if_not_P[OF **] interval_bounds[OF ***],symmetric]
-  show ?thesis
-    unfolding *
-    apply (rule sum.cong)
-    unfolding split_paired_all split_conv
-    using assms(2)
-    apply auto
-    done
+  then have "f b - f a = (\<Sum>(x, l)\<in>p. if l = {} then 0 else f (interval_upperbound l) - f (interval_lowerbound l))"
+    proof -
+      have "(if cbox a b = {} then 0 else f (interval_upperbound (cbox a b)) - f (interval_lowerbound (cbox a b))) = f b - f a"
+        using assms by auto
+      then show ?thesis
+        using p_td assms by (simp add: "*" sum.operative_tagged_division)
+    qed 
+  then show ?thesis
+    using assms by (auto intro!: sum.cong)
 qed
 
 lemma bgauge_existence_lemma: "(\<forall>x\<in>s. \<exists>d::real. 0 < d \<and> q d x) \<longleftrightarrow> (\<forall>x. \<exists>d>0. x\<in>s \<longrightarrow> q d x)"
diff -r 20304512a33b -r 0e640e04fc56 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sat Jun 17 20:24:22 2017 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Jun 19 16:07:47 2017 +0100
@@ -1438,8 +1438,8 @@
 
 lemma
   fixes a :: "'a::euclidean_space"
-  shows cbox_sing: "cbox a a = {a}"
-    and box_sing: "box a a = {}"
+  shows cbox_sing [simp]: "cbox a a = {a}"
+    and box_sing [simp]: "box a a = {}"
   unfolding set_eq_iff mem_box eq_iff [symmetric]
   by (auto intro!: euclidean_eqI[where 'a='a])
      (metis all_not_in_conv nonempty_Basis)
diff -r 20304512a33b -r 0e640e04fc56 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Sat Jun 17 20:24:22 2017 +0200
+++ b/src/HOL/Groups_Big.thy	Mon Jun 19 16:07:47 2017 +0100
@@ -643,8 +643,8 @@
 
 lemma member_le_sum:
   fixes f :: "_ \<Rightarrow> 'b::{semiring_1, ordered_comm_monoid_add}"
-  assumes le: "\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x"
-    and "i \<in> A"
+  assumes "i \<in> A"
+    and le: "\<And>x. x \<in> A - {i} \<Longrightarrow> 0 \<le> f x"
     and "finite A"
   shows "f i \<le> sum f A"
 proof -