# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1503528395 -3600
# Node ID 18a6478a574ca072d9b918d4e1e73d5f6a59fa40
# Parent  001d4a9986a23cdaf00582c0746501cfb9925a62
More tidying, and renaming of theorems

diff -r 001d4a9986a2 -r 18a6478a574c src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Wed Aug 23 19:54:30 2017 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Wed Aug 23 23:46:35 2017 +0100
@@ -1643,7 +1643,7 @@
       by metis
     have "e/2 > 0"
       using e by auto
-    with henstock_lemma[OF f] 
+    with Henstock_lemma[OF f] 
     obtain \<gamma> where g: "gauge \<gamma>"
       "\<And>p. \<lbrakk>p tagged_partial_division_of cbox a b; \<gamma> fine p\<rbrakk> 
                 \<Longrightarrow> (\<Sum>(x,k) \<in> p. norm (content k *\<^sub>R f x - integral k f)) < e/2"
@@ -2101,7 +2101,7 @@
         obtain d2 where "gauge d2" 
           and d2: "\<And>p. \<lbrakk>p tagged_partial_division_of (cbox a b); d2 fine p\<rbrakk> \<Longrightarrow>
             (\<Sum>(x,k) \<in> p. norm (content k *\<^sub>R f x - integral k f)) < e/2"
-          by (blast intro: henstock_lemma [OF f(1) \<open>e/2>0\<close>])
+          by (blast intro: Henstock_lemma [OF f(1) \<open>e/2>0\<close>])
         obtain p where
           p: "p tagged_division_of (cbox a b)" "d1 fine p" "d2 fine p"
           by (rule fine_division_exists [OF gauge_Int [OF \<open>gauge d1\<close> \<open>gauge d2\<close>], of a b])
diff -r 001d4a9986a2 -r 18a6478a574c src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Aug 23 19:54:30 2017 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Aug 23 23:46:35 2017 +0100
@@ -1276,7 +1276,7 @@
     note p1=tagged_division_ofD[OF this(1)] 
     assume tdiv2: "p2 tagged_division_of (cbox a b) \<inter> {x. c \<le> x \<bullet> k}" and "\<gamma> fine p2"
     note p2=tagged_division_ofD[OF this(1)] 
-    note tagged_division_union_interval[OF tdiv1 tdiv2] 
+    note tagged_division_Un_interval[OF tdiv1 tdiv2] 
     note p12 = tagged_division_ofD[OF this] this
     { fix a b
       assume ab: "(a, b) \<in> p1 \<inter> p2"
@@ -4116,7 +4116,7 @@
       using as by (auto simp add: field_simps)
 
     have "p \<union> {(c, {t..c})} tagged_division_of {a..c}"
-      apply (rule tagged_division_union_interval_real[of _ _ _ 1 "t"])
+      apply (rule tagged_division_Un_interval_real[of _ _ _ 1 "t"])
       using  \<open>t \<le> c\<close> by (auto simp: * ptag tagged_division_of_self_real)
     moreover
     have "d1 fine p \<union> {(c, {t..c})}"
@@ -5664,9 +5664,9 @@
 
 subsection \<open>Henstock's lemma\<close>
 
-lemma henstock_lemma_part1:
+lemma Henstock_lemma_part1:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  assumes "f integrable_on cbox a b"
+  assumes intf: "f integrable_on cbox a b"
     and "e > 0"
     and "gauge d"
     and less_e: "\<And>p. \<lbrakk>p tagged_division_of (cbox a b); d fine p\<rbrakk> \<Longrightarrow>
@@ -5689,59 +5689,52 @@
   have r: "finite r"
     using q' unfolding r_def by auto
 
-  have "\<forall>i\<in>r. \<exists>p. p tagged_division_of i \<and> d fine p \<and>
-    norm (sum (\<lambda>(x,j). content j *\<^sub>R f x) p - integral i f) < k / (real (card r) + 1)"
-    apply safe
-  proof goal_cases
-    case (1 i)
-    then have i: "i \<in> q"
-      unfolding r_def by auto
-    from q'(4)[OF this] guess u v by (elim exE) note uv=this
+  have "\<exists>p. p tagged_division_of i \<and> d fine p \<and>
+        norm (sum (\<lambda>(x,j). content j *\<^sub>R f x) p - integral i f) < k / (real (card r) + 1)"
+    if "i\<in>r" for i
+  proof -
     have *: "k / (real (card r) + 1) > 0" using k by simp
-    have "f integrable_on cbox u v"
-      apply (rule integrable_subinterval[OF assms(1)])
-      using q'(2)[OF i]
-      unfolding uv
-      apply auto
-      done
+    have i: "i \<in> q"
+      using that unfolding r_def by auto
+    then obtain u v where uv: "i = cbox u v"
+      using q'(4) by blast
+    then have "cbox u v \<subseteq> cbox a b"
+      using i q'(2) by auto  
+    then have "f integrable_on cbox u v"
+      by (rule integrable_subinterval[OF intf])
     note integrable_integral[OF this, unfolded has_integral[of f]]
     from this[rule_format,OF *] guess dd..note dd=conjunctD2[OF this,rule_format]
     note gauge_Int[OF \<open>gauge d\<close> dd(1)]
     from fine_division_exists[OF this,of u v] guess qq .
-    then show ?case
+    then show ?thesis
       apply (rule_tac x=qq in exI)
       using dd(2)[of qq]
       unfolding fine_Int uv
       apply auto
       done
   qed
-  from bchoice[OF this] guess qq..note qq=this[rule_format]
+  then obtain qq where qq: "\<And>i. i \<in> r \<Longrightarrow> qq i tagged_division_of i \<and>
+      d fine qq i \<and>
+      norm
+       ((\<Sum>(x, j) \<in> qq i. content j *\<^sub>R f x) -
+        integral i f)
+      < k / (real (card r) + 1)"
+    by metis
 
   let ?p = "p \<union> \<Union>(qq ` r)"
   have "norm ((\<Sum>(x, k)\<in>?p. content k *\<^sub>R f x) - integral (cbox a b) f) < e"
   proof (rule less_e)
     show "d fine ?p"
       by (metis (mono_tags, hide_lams) qq fine_Un fine_Union imageE p(2))
-    note * = tagged_partial_division_of_union_self[OF p(1)]
+    note * = tagged_partial_division_of_Union_self[OF p(1)]
     have "p \<union> \<Union>(qq ` r) tagged_division_of \<Union>(snd ` p) \<union> \<Union>r"
       using r
-    proof (rule tagged_division_union[OF * tagged_division_unions], goal_cases)
-      case 1
-      then show ?case
+    proof (rule tagged_division_Un[OF * tagged_division_Union])
+      show "\<And>i. i \<in> r \<Longrightarrow> qq i tagged_division_of i"
         using qq by auto
-    next
-      case 2
-      then show ?case
-        apply rule
-        apply rule
-        apply rule
-        apply(rule q'(5))
-        unfolding r_def
-        apply auto
-        done
-    next
-      case 3
-      then show ?case
+      show "\<And>i1 i2. \<lbrakk>i1 \<in> r; i2 \<in> r; i1 \<noteq> i2\<rbrakk> \<Longrightarrow> interior i1 \<inter> interior i2 = {}"
+        by (simp add: q'(5) r_def)
+      show "interior (UNION p snd) \<inter> interior (\<Union>r) = {}"
       proof (rule Int_interior_Union_intervals [OF \<open>finite r\<close>])
         show "open (interior (UNION p snd))"
           by blast
@@ -5758,9 +5751,7 @@
       qed
     qed
     moreover have "\<Union>(snd ` p) \<union> \<Union>r = cbox a b" and "{qq i |i. i \<in> r} = qq ` r"
-      unfolding Union_Un_distrib[symmetric] r_def
-      using q
-      by auto
+      using q  unfolding Union_Un_distrib[symmetric] r_def by auto
     ultimately show "?p tagged_division_of (cbox a b)"
       by fastforce
   qed
@@ -5893,7 +5884,7 @@
   finally show "?x \<le> e + k" .
 qed
 
-lemma henstock_lemma_part2:
+lemma Henstock_lemma_part2:
   fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
   assumes fed: "f integrable_on cbox a b" "e > 0" "gauge d"
     and less_e: "\<And>\<D>. \<lbrakk>\<D> tagged_division_of (cbox a b); d fine \<D>\<rbrakk> \<Longrightarrow>
@@ -5912,13 +5903,13 @@
     then have fine: "d fine Q"
       by (simp add: \<open>d fine p\<close> fine_subset)
     show "norm (\<Sum>x\<in>Q. content (snd x) *\<^sub>R f (fst x) - integral (snd x) f) \<le> e"
-      apply (rule henstock_lemma_part1[OF fed less_e, unfolded split_def])
+      apply (rule Henstock_lemma_part1[OF fed less_e, unfolded split_def])
       using Q tag tagged_partial_division_subset apply (force simp add: fine)+
       done
   qed
 qed
 
-lemma henstock_lemma:
+lemma Henstock_lemma:
   fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
   assumes intf: "f integrable_on cbox a b"
     and "e > 0"
@@ -5939,7 +5930,7 @@
     assume p: "p tagged_partial_division_of cbox a b" "\<gamma> fine p"
     have "(\<Sum>(x,K)\<in>p. norm (content K *\<^sub>R f x - integral K f)) 
           \<le> 2 * real DIM('n) * (e/(2 * (real DIM('n) + 1)))"
-      using henstock_lemma_part2[OF intf * \<open>gauge \<gamma>\<close> \<gamma> p] by metis
+      using Henstock_lemma_part2[OF intf * \<open>gauge \<gamma>\<close> \<gamma> p] by metis
     also have "... < e"
       using \<open>e > 0\<close> by (auto simp add: field_simps)
     finally
@@ -6040,8 +6031,8 @@
         using c(1) unfolding gauge_def d_def by auto
     next
       fix \<D>
-      assume p: "\<D> tagged_division_of (cbox a b)" "d fine \<D>"
-      note p'=tagged_division_ofD[OF p(1)]
+      assume ptag: "\<D> tagged_division_of (cbox a b)" and "d fine \<D>"
+      note p'=tagged_division_ofD[OF ptag]
       obtain s where s: "\<And>x. x \<in> \<D> \<Longrightarrow> m (fst x) \<le> s"
         by (metis finite_imageI finite_nat_set_iff_bounded_le p'(1) rev_image_eqI)
       have *: "\<bar>a - d\<bar> < e" if "\<bar>a - b\<bar> \<le> e/4" "\<bar>b - c\<bar> < e/2" "\<bar>c - d\<bar> < e/4" for a b c d
@@ -6050,24 +6041,26 @@
         by (auto simp add: algebra_simps)
       show "\<bar>(\<Sum>(x, k)\<in>\<D>. content k *\<^sub>R g x) - i\<bar> < e"
       proof (rule *)
-        show "\<bar>(\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R g x) - (\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f (m x) x)\<bar> \<le> e/4"
-          apply (rule order_trans[of _ "\<Sum>(x, k)\<in>\<D>. content k * (e/(4 * content (cbox a b)))"])
-          unfolding sum_subtractf[symmetric]
-          apply (rule order_trans)
-          apply (rule sum_abs)
-          apply (rule sum_mono)
-          unfolding split_paired_all split_conv
-          unfolding split_def sum_distrib_right[symmetric] scaleR_diff_right[symmetric]
-          unfolding additive_content_tagged_division[OF p(1), unfolded split_def]
-        proof -
+        have "\<bar>(\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R g x) - (\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f (m x) x)\<bar> 
+              \<le> (\<Sum>i\<in>\<D>. \<bar>(case i of (x, K) \<Rightarrow> content K *\<^sub>R g x) - (case i of (x, K) \<Rightarrow> content K *\<^sub>R f (m x) x)\<bar>)"
+          by (metis (mono_tags) sum_subtractf sum_abs) 
+        also have "... \<le> (\<Sum>(x, k)\<in>\<D>. content k * (e/(4 * content (cbox a b))))"
+        proof (rule sum_mono, simp add: split_paired_all)
           fix x K
-          assume xk: "(x, K) \<in> \<D>"
-          with p(1) have x: "x \<in> cbox a b"
+          assume xk: "(x,K) \<in> \<D>"
+          with ptag have x: "x \<in> cbox a b"
             by blast
-          then show "abs (content K *\<^sub>R (g x - f (m x) x)) \<le> content K * (e/(4 * content (cbox a b)))"
-            unfolding abs_scaleR using m[OF x] p'(4)[OF xk]
-            by (metis real_scaleR_def abs_of_nonneg less_eq_real_def measure_nonneg mult_left_mono order_refl)
-        qed (insert False, auto)
+          then have "abs (content K * (g x - f (m x) x)) \<le> content K * (e/(4 * content (cbox a b)))"
+            by (metis m[OF x] mult_nonneg_nonneg abs_of_nonneg less_eq_real_def measure_nonneg mult_left_mono order_refl)
+          then show "\<bar>content K * g x - content K * f (m x) x\<bar> \<le> content K * e / (4 * content (cbox a b))"
+            by (simp add: algebra_simps)
+        qed
+        also have "... = (e / (4 * content (cbox a b))) * (\<Sum>(x, k)\<in>\<D>. content k)"
+          by (simp add: sum_distrib_left sum_divide_distrib split_def mult.commute)
+        also have "... \<le> e/4"
+          by (metis False additive_content_tagged_division [OF ptag] nonzero_mult_divide_mult_cancel_right order_refl times_divide_eq_left)
+        finally show "\<bar>(\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R g x) - (\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f (m x) x)\<bar> \<le> e/4" .
+
       next
         have "norm ((\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f (m x) x) - (\<Sum>(x,K)\<in>\<D>. integral K (f (m x))))
               \<le> norm (\<Sum>j = 0..s. \<Sum>(x,K)\<in>{xk \<in> \<D>. m (fst xk) = j}. content K *\<^sub>R f (m x) x - integral K (f (m x)))"
@@ -6084,12 +6077,12 @@
                   norm (\<Sum>(x,k)\<in>{xk \<in> \<D>. m (fst xk) = t}. content k *\<^sub>R f t x - integral k (f t))"
               by (force intro!: sum.cong arg_cong[where f=norm])
             also have "... \<le> e/2 ^ (t + 2)"
-            proof (rule henstock_lemma_part1 [OF intf])
+            proof (rule Henstock_lemma_part1 [OF intf])
               show "{xk \<in> \<D>. m (fst xk) = t} tagged_partial_division_of cbox a b"
                 apply (rule tagged_partial_division_subset[of \<D>])
-                using p by (auto simp: tagged_division_of_def)
+                using ptag by (auto simp: tagged_division_of_def)
               show "c t fine {xk \<in> \<D>. m (fst xk) = t}"
-                using p(2) by (auto simp: fine_def d_def)
+                using \<open>d fine \<D>\<close> by (auto simp: fine_def d_def)
             qed (use c e in auto)
             finally show "norm (\<Sum>(x,K)\<in>{xk \<in> \<D>. m (fst xk) = t}. content K *\<^sub>R f (m x) x -
                                 integral K (f (m x))) \<le> e/2 ^ (t + 2)" .
@@ -6105,7 +6098,7 @@
           by simp
       next
         have comb: "integral (cbox a b) (f y) = (\<Sum>(x, k)\<in>\<D>. integral k (f y))" for y
-          using integral_combine_tagged_division_topdown[OF intf p(1)] by metis
+          using integral_combine_tagged_division_topdown[OF intf ptag] by metis
         have f_le: "\<And>y m n. \<lbrakk>y \<in> cbox a b; n\<ge>m\<rbrakk> \<Longrightarrow> f m y \<le> f n y"
           using le by (auto intro: transitive_stepwise_le)        
         have "(\<Sum>(x, k)\<in>\<D>. integral k (f r)) \<le> (\<Sum>(x, K)\<in>\<D>. integral K (f (m x)))"
@@ -6171,11 +6164,11 @@
       using bounded_increasing_convergent [OF bou] le int_f integral_le by blast
     have i': "(integral S (f k)) \<le> i" for k
     proof -
-      have *: "\<And>k. \<forall>x\<in>S. \<forall>n\<ge>k. f k x \<le> f n x"
+      have "\<And>k. \<forall>x\<in>S. \<forall>n\<ge>k. f k x \<le> f n x"
         using le  by (force intro: transitive_stepwise_le)
-      show ?thesis
+      then show ?thesis
         using tendsto_lowerbound [OF i eventually_sequentiallyI trivial_limit_sequentially]
-        by (meson "*" int_f integral_le)
+        by (meson int_f integral_le)
     qed
 
     let ?f = "(\<lambda>k x. if x \<in> S then f k x else 0)"
diff -r 001d4a9986a2 -r 18a6478a574c src/HOL/Analysis/Improper_Integral.thy
--- a/src/HOL/Analysis/Improper_Integral.thy	Wed Aug 23 19:54:30 2017 +0100
+++ b/src/HOL/Analysis/Improper_Integral.thy	Wed Aug 23 23:46:35 2017 +0100
@@ -658,7 +658,7 @@
            if "S tagged_partial_division_of cbox a b" "\<gamma> fine S" "h \<in> F" for S h
       proof -
         have "(\<Sum>(x,K) \<in> S. norm (content K *\<^sub>R h x - integral K h)) \<le> 2 * real DIM('b) * (\<epsilon>/(5 * Suc DIM('b)))"
-        proof (rule henstock_lemma_part2 [of h a b])
+        proof (rule Henstock_lemma_part2 [of h a b])
           show "h integrable_on cbox a b"
             using that F equiintegrable_on_def by metis
           show "gauge \<gamma>"
@@ -778,7 +778,7 @@
       qed
       also have "... = (\<Sum>K\<in>snd ` S. \<epsilon>/4 * (b \<bullet> i - a \<bullet> i) / content (cbox a b) * content K
                                      / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i))"
-        apply (rule sum.over_tagged_division_lemma [OF tagged_partial_division_of_union_self [OF S]])
+        apply (rule sum.over_tagged_division_lemma [OF tagged_partial_division_of_Union_self [OF S]])
         apply (simp add: box_eq_empty(1) content_eq_0)
         done
       also have "... = \<epsilon>/2 * ((b \<bullet> i - a \<bullet> i) / (2 * content (cbox a b)) * (\<Sum>K\<in>snd ` S. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)))"
@@ -789,7 +789,7 @@
               \<le> 2 * content (cbox a b)"
         proof (rule sum_content_area_over_thin_division)
           show "snd ` S division_of \<Union>(snd ` S)"
-            by (auto intro: S tagged_partial_division_of_union_self division_of_tagged_division)
+            by (auto intro: S tagged_partial_division_of_Union_self division_of_tagged_division)
           show "UNION S snd \<subseteq> cbox a b"
             using S by force
           show "a \<bullet> i \<le> c \<bullet> i" "c \<bullet> i \<le> b \<bullet> i"
@@ -861,7 +861,7 @@
         if "T tagged_partial_division_of cbox a b" "\<gamma>1 fine T" "h \<in> F" for T h
       proof -
         have "(\<Sum>(x,K) \<in> T. norm (?CI K h x)) \<le> 2 * real DIM('b) * (\<epsilon>/(7 * Suc DIM('b)))"
-        proof (rule henstock_lemma_part2 [of h a b])
+        proof (rule Henstock_lemma_part2 [of h a b])
           show "h integrable_on cbox a b"
             using that F equiintegrable_on_def by metis
           show "gauge \<gamma>1"
@@ -985,7 +985,7 @@
                     obtain u v where uv: "L = cbox u v"
                       using T'_tagged \<open>(x, L) \<in> A\<close> \<open>A \<subseteq> T''\<close> \<open>T'' \<subseteq> T'\<close> by blast
                     have "A tagged_division_of UNION A snd"
-                      using A_tagged tagged_partial_division_of_union_self by auto
+                      using A_tagged tagged_partial_division_of_Union_self by auto
                     then have "interior (K \<inter> {x. x \<bullet> i \<le> c}) = {}"
                       apply (rule tagged_division_split_left_inj [OF _ \<open>(x,K) \<in> A\<close> \<open>(x,L) \<in> A\<close>])
                       using that eq \<open>i \<in> Basis\<close> by auto
@@ -1014,7 +1014,7 @@
                     obtain u v where uv: "L = cbox u v"
                       using T'_tagged \<open>(x, L) \<in> B\<close> \<open>B \<subseteq> T''\<close> \<open>T'' \<subseteq> T'\<close> by blast
                     have "B tagged_division_of UNION B snd"
-                      using B_tagged tagged_partial_division_of_union_self by auto
+                      using B_tagged tagged_partial_division_of_Union_self by auto
                     then have "interior (K \<inter> {x. c \<le> x \<bullet> i}) = {}"
                       apply (rule tagged_division_split_right_inj [OF _ \<open>(x,K) \<in> B\<close> \<open>(x,L) \<in> B\<close>])
                       using that eq \<open>i \<in> Basis\<close> by auto
diff -r 001d4a9986a2 -r 18a6478a574c src/HOL/Analysis/Tagged_Division.thy
--- a/src/HOL/Analysis/Tagged_Division.thy	Wed Aug 23 19:54:30 2017 +0100
+++ b/src/HOL/Analysis/Tagged_Division.thy	Wed Aug 23 23:46:35 2017 +0100
@@ -1120,7 +1120,7 @@
   unfolding box_real[symmetric]
   by (rule tagged_division_of_self)
 
-lemma tagged_division_union:
+lemma tagged_division_Un:
   assumes "p1 tagged_division_of s1"
     and "p2 tagged_division_of s2"
     and "interior s1 \<inter> interior s2 = {}"
@@ -1148,13 +1148,13 @@
     by (metis "*" UnE assms(1) assms(2) inf_sup_aci(1) p2(5) tagged_division_ofD(3) xk xk'(1) xk'(2))
 qed
 
-lemma tagged_division_unions:
+lemma tagged_division_Union:
   assumes "finite I"
-    and "\<forall>i\<in>I. pfn i tagged_division_of i"
-    and "\<forall>i1\<in>I. \<forall>i2\<in>I. i1 \<noteq> i2 \<longrightarrow> interior(i1) \<inter> interior(i2) = {}"
+    and tag: "\<And>i. i\<in>I \<Longrightarrow> pfn i tagged_division_of i"
+    and disj: "\<And>i1 i2. \<lbrakk>i1 \<in> I; i2 \<in> I; i1 \<noteq> i2\<rbrakk> \<Longrightarrow> interior(i1) \<inter> interior(i2) = {}"
   shows "\<Union>(pfn ` I) tagged_division_of (\<Union>I)"
 proof (rule tagged_division_ofI)
-  note assm = tagged_division_ofD[OF assms(2)[rule_format]]
+  note assm = tagged_division_ofD[OF tag]
   show "finite (\<Union>(pfn ` I))"
     using assms by auto
   have "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>(pfn ` I)} = \<Union>((\<lambda>i. \<Union>{k. \<exists>x. (x, k) \<in> pfn i}) ` I)"
@@ -1173,16 +1173,18 @@
   then obtain i' where i': "i' \<in> I" "(x', k') \<in> pfn i'"
     by auto
   have *: "\<And>a b. i \<noteq> i' \<Longrightarrow> a \<subseteq> i \<Longrightarrow> b \<subseteq> i' \<Longrightarrow> interior a \<inter> interior b = {}"
-    using i(1) i'(1)
-    using assms(3)[rule_format] interior_mono
-    by blast
+    using i(1) i'(1) disj interior_mono by blast
   show "interior k \<inter> interior k' = {}"
-    apply (cases "i = i'")
-    using assm(5) i' i(2) xk'(2) apply blast
+  proof (cases "i = i'")
+    case True then show ?thesis 
+      using assm(5) i' i xk'(2) by blast
+  next
+    case False then show ?thesis 
     using "*" assm(3) i' i by auto
+  qed
 qed
 
-lemma tagged_partial_division_of_union_self:
+lemma tagged_partial_division_of_Union_self:
   assumes "p tagged_partial_division_of s"
   shows "p tagged_division_of (\<Union>(snd ` p))"
   apply (rule tagged_division_ofI)
@@ -1753,7 +1755,7 @@
   qed
 qed
 
-lemma tagged_division_union_interval:
+lemma tagged_division_Un_interval:
   fixes a :: "'a::euclidean_space"
   assumes "p1 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<le> (c::real)})"
     and "p2 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
@@ -1764,14 +1766,14 @@
     by auto
   show ?thesis
     apply (subst *)
-    apply (rule tagged_division_union[OF assms(1-2)])
+    apply (rule tagged_division_Un[OF assms(1-2)])
     unfolding interval_split[OF k] interior_cbox
     using k
     apply (auto simp add: box_def elim!: ballE[where x=k])
     done
 qed
 
-lemma tagged_division_union_interval_real:
+lemma tagged_division_Un_interval_real:
   fixes a :: real
   assumes "p1 tagged_division_of ({a .. b} \<inter> {x. x\<bullet>k \<le> (c::real)})"
     and "p2 tagged_division_of ({a .. b} \<inter> {x. x\<bullet>k \<ge> c})"
@@ -1779,7 +1781,7 @@
   shows "(p1 \<union> p2) tagged_division_of {a .. b}"
   using assms
   unfolding box_real[symmetric]
-  by (rule tagged_division_union_interval)
+  by (rule tagged_division_Un_interval)
 
 lemma tagged_division_split_left_inj:
   assumes d: "d tagged_division_of i"
@@ -1882,7 +1884,7 @@
     using bchoice[OF assms(2)] by auto
   show thesis
     apply (rule_tac p="\<Union>(pfn ` I)" in that)
-    using assms(1) assms(3) assms(4) pfn(1) tagged_division_unions apply force
+    using assms(1) assms(3) assms(4) pfn(1) tagged_division_Union apply force
     by (metis (mono_tags, lifting) fine_Union imageE pfn(2))
 qed
 
@@ -2233,7 +2235,7 @@
           \<not> (\<exists>p. p tagged_division_of cbox c d \<and> g fine p)"
     apply (rule interval_bisection[of "\<lambda>s. \<exists>p. p tagged_division_of s \<and> g fine p", OF _ _ False])
     apply (simp add: fine_def)
-    apply (metis tagged_division_union fine_Un)
+    apply (metis tagged_division_Un fine_Un)
     apply auto
     done
   obtain e where e: "e > 0" "ball x e \<subseteq> g x"
@@ -2324,7 +2326,7 @@
       have "{(x, cbox u v)} tagged_division_of cbox u v"
         by (simp add: p(2) uv xk tagged_division_of_self)
       then have "{(x, cbox u v)} \<union> q1 tagged_division_of \<Union>{k. \<exists>x. (x, k) \<in> insert xk p}"
-        unfolding * uv by (metis (no_types, lifting) int q1 tagged_division_union)
+        unfolding * uv by (metis (no_types, lifting) int q1 tagged_division_Un)
       with True show ?thesis
         apply (rule_tac x="{(x,cbox u v)} \<union> q1" in exI)
         using \<open>d fine q1\<close> fine_def q1I uv xk apply fastforce
@@ -2337,7 +2339,7 @@
         apply (rule_tac x="q2 \<union> q1" in exI)
         apply (intro conjI)
         unfolding * uv
-        apply (rule tagged_division_union q2 q1 int fine_Un)+
+        apply (rule tagged_division_Un q2 q1 int fine_Un)+
           apply (auto intro: q1 q2 fine_Un \<open>d fine q1\<close> simp add: False q1I uv xk)
         done
     qed