# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1501447463 -3600
# Node ID 1b4aa3e3e4e69de2caaec5766c7b5d5bb1cc1caf
# Parent  5ff9fe3fee664f7e506d50b4c3a07866bffffa2a
partial cleanup of the horrible Tagged_Division

diff -r 5ff9fe3fee66 -r 1b4aa3e3e4e6 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Jul 28 15:36:32 2017 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Jul 30 21:44:23 2017 +0100
@@ -6020,25 +6020,20 @@
     next
       case 3
       then show ?case
-        apply (rule inter_interior_unions_intervals)
-        apply fact
-        apply rule
-        apply rule
+      proof (rule Int_interior_Union_intervals [OF \<open>finite r\<close>])
+        show "open (interior (UNION p snd))"
+          by blast
+        show "\<And>T. T \<in> r \<Longrightarrow> \<exists>a b. T = cbox a b"
         apply (rule q')
-        defer
-        apply rule
-        apply (subst Int_commute)
-        apply (rule inter_interior_unions_intervals)
-        apply (rule finite_imageI)
-        apply (rule p')
-        apply rule
-        defer
-        apply rule
-        apply (rule q')
-        using q(1) p'
-        unfolding r_def
-        apply auto
-        done
+          using r_def by blast
+        have "finite (snd ` p)"
+          by (simp add: p'(1))
+        then show "\<And>T. T \<in> r \<Longrightarrow> interior (UNION p snd) \<inter> interior T = {}"
+          apply (subst Int_commute)
+          apply (rule Int_interior_Union_intervals)
+          using \<open>r \<equiv> q - snd ` p\<close>  q'(5) q(1) apply auto
+          by (simp add: p'(4))
+      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
diff -r 5ff9fe3fee66 -r 1b4aa3e3e4e6 src/HOL/Analysis/Tagged_Division.thy
--- a/src/HOL/Analysis/Tagged_Division.thy	Fri Jul 28 15:36:32 2017 +0100
+++ b/src/HOL/Analysis/Tagged_Division.thy	Sun Jul 30 21:44:23 2017 +0100
@@ -10,7 +10,7 @@
   Topology_Euclidean_Space
 begin
 
-lemma finite_product_dependent:
+lemma finite_product_dependent: (*FIXME DELETE*)
   assumes "finite s"
     and "\<And>x. x \<in> s \<Longrightarrow> finite (t x)"
   shows "finite {(i, j) |i j. i \<in> s \<and> j \<in> t i}"
@@ -77,19 +77,17 @@
   assumes "i = cbox a b"
     and "j = cbox c d"
     and "interior j \<noteq> {}"
-    and "i \<subseteq> j \<union> s"
+    and "i \<subseteq> j \<union> S"
     and "interior i \<inter> interior j = {}"
-  shows "interior i \<subseteq> interior s"
+  shows "interior i \<subseteq> interior S"
 proof -
   have "box a b \<inter> cbox c d = {}"
-     using inter_interval_mixed_eq_empty[of c d a b] and assms(3,5)
-     unfolding assms(1,2) interior_cbox by auto
+     using inter_interval_mixed_eq_empty[of c d a b] assms
+     unfolding interior_cbox by auto
   moreover
-  have "box a b \<subseteq> cbox c d \<union> s"
+  have "box a b \<subseteq> cbox c d \<union> S"
     apply (rule order_trans,rule box_subset_cbox)
-    using assms(4) unfolding assms(1,2)
-    apply auto
-    done
+    using assms by auto
   ultimately
   show ?thesis
     unfolding assms interior_cbox
@@ -132,9 +130,10 @@
   finally show ?thesis .
 qed
 
-lemma inter_interior_unions_intervals:
-    "finite f \<Longrightarrow> open s \<Longrightarrow> \<forall>t\<in>f. \<exists>a b. t = cbox a b \<Longrightarrow> \<forall>t\<in>f. s \<inter> (interior t) = {} \<Longrightarrow> s \<inter> interior (\<Union>f) = {}"
-  using interior_Union_subset_cbox[of f "UNIV - s"] by auto
+lemma Int_interior_Union_intervals:
+    "\<lbrakk>finite \<F>; open S; \<And>T. T\<in>\<F> \<Longrightarrow> \<exists>a b. T = cbox a b; \<And>T. T\<in>\<F> \<Longrightarrow> S \<inter> (interior T) = {}\<rbrakk> 
+    \<Longrightarrow> S \<inter> interior (\<Union>\<F>) = {}"
+  using interior_Union_subset_cbox[of \<F> "UNIV - S"] by auto
 
 lemma interval_split:
   fixes a :: "'a::euclidean_space"
@@ -142,11 +141,7 @@
   shows
     "cbox a b \<inter> {x. x\<bullet>k \<le> c} = cbox a (\<Sum>i\<in>Basis. (if i = k then min (b\<bullet>k) c else b\<bullet>i) *\<^sub>R i)"
     "cbox a b \<inter> {x. x\<bullet>k \<ge> c} = cbox (\<Sum>i\<in>Basis. (if i = k then max (a\<bullet>k) c else a\<bullet>i) *\<^sub>R i) b"
-  apply (rule_tac[!] set_eqI)
-  unfolding Int_iff mem_box mem_Collect_eq
-  using assms
-  apply auto
-  done
+  using assms by (rule_tac set_eqI; auto simp: mem_box)+
 
 lemma interval_not_empty: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> cbox a b \<noteq> {}"
   by (simp add: box_ne_empty)
@@ -242,17 +237,17 @@
   unfolding gauge_def by auto
 
 lemma gauge_reflect:
-  fixes \<D> :: "'a::euclidean_space \<Rightarrow> 'a set"
-  shows "gauge \<D> \<Longrightarrow> gauge (\<lambda>x. uminus ` \<D> (- x))"
+  fixes \<gamma> :: "'a::euclidean_space \<Rightarrow> 'a set"
+  shows "gauge \<gamma> \<Longrightarrow> gauge (\<lambda>x. uminus ` \<gamma> (- x))"
   using equation_minus_iff
   by (auto simp: gauge_def surj_def intro!: open_surjective_linear_image linear_uminus)
 
 lemma gauge_Inter:
-  assumes "finite s"
-    and "\<And>d. d\<in>s \<Longrightarrow> gauge (f d)"
-  shows "gauge (\<lambda>x. \<Inter>{f d x | d. d \<in> s})"
+  assumes "finite S"
+    and "\<And>d. d\<in>S \<Longrightarrow> gauge (f d)"
+  shows "gauge (\<lambda>x. \<Inter>{f d x | d. d \<in> S})"
 proof -
-  have *: "\<And>x. {f d x |d. d \<in> s} = (\<lambda>d. f d x) ` s"
+  have *: "\<And>x. {f d x |d. d \<in> S} = (\<lambda>d. f d x) ` S"
     by auto
   show ?thesis
     unfolding gauge_def unfolding *
@@ -266,16 +261,9 @@
 subsection \<open>Attempt a systematic general set of "offset" results for components.\<close>
 
 lemma gauge_modify:
-  assumes "(\<forall>s. open s \<longrightarrow> open {x. f(x) \<in> s})" "gauge d"
+  assumes "(\<forall>S. open S \<longrightarrow> open {x. f(x) \<in> S})" "gauge d"
   shows "gauge (\<lambda>x. {y. f y \<in> d (f x)})"
-  using assms
-  unfolding gauge_def
-  apply safe
-  defer
-  apply (erule_tac x="f x" in allE)
-  apply (erule_tac x="d (f x)" in allE)
-  apply auto
-  done
+  using assms unfolding gauge_def by force
 
 subsection \<open>Divisions.\<close>
 
@@ -671,24 +659,19 @@
   qed
   obtain q where q: "\<And>x. x \<in> p \<Longrightarrow> q x division_of cbox a b" "\<And>x. x \<in> p \<Longrightarrow> x \<in> q x"
     using bchoice[OF div_cbox] by blast
-  { fix x
-    assume x: "x \<in> p"
-    have "q x division_of \<Union>q x"
-      apply (rule division_ofI)
-      using division_ofD[OF q(1)[OF x]]
-      apply auto
-      done }
-  then have "\<And>x. x \<in> p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x - {x})"
+  have "q x division_of \<Union>q x" if x: "x \<in> p" for x
+    apply (rule division_ofI)
+    using division_ofD[OF q(1)[OF x]] by auto
+  then have di: "\<And>x. x \<in> p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x - {x})"
     by (meson Diff_subset division_of_subset)
-  then have "\<exists>d. d division_of \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p)"
-    apply -
+  have "\<exists>d. d division_of \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p)"
     apply (rule elementary_inters [OF finite_imageI[OF p(1)]])
-    apply (auto simp: False elementary_inters [OF finite_imageI[OF p(1)]])
+    apply (auto dest: di simp: False elementary_inters [OF finite_imageI[OF p(1)]])
     done
   then obtain d where d: "d division_of \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p)" ..
   have "d \<union> p division_of cbox a b"
   proof -
-    have te: "\<And>s f t. s \<noteq> {} \<Longrightarrow> \<forall>i\<in>s. f i \<union> i = t \<Longrightarrow> t = \<Inter>(f ` s) \<union> \<Union>s" by auto
+    have te: "\<And>S f T. S \<noteq> {} \<Longrightarrow> \<forall>i\<in>S. f i \<union> i = T \<Longrightarrow> T = \<Inter>(f ` S) \<union> \<Union>S" by auto
     have cbox_eq: "cbox a b = \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p) \<union> \<Union>p"
     proof (rule te[OF False], clarify)
       fix i
@@ -696,27 +679,23 @@
       show "\<Union>(q i - {i}) \<union> i = cbox a b"
         using division_ofD(6)[OF q(1)[OF i]] using q(2)[OF i] by auto
     qed
-    { fix k
-      assume k: "k \<in> p"
-      have *: "\<And>u t s. t \<inter> s = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<inter> t = {}"
+    { fix K
+      assume K: "K \<in> p"
+      note qk=division_ofD[OF q(1)[OF K]]
+      have *: "\<And>u T S. T \<inter> S = {} \<Longrightarrow> u \<subseteq> S \<Longrightarrow> u \<inter> T = {}"
         by auto
-      have "interior (\<Inter>i\<in>p. \<Union>(q i - {i})) \<inter> interior k = {}"
-      proof (rule *[OF inter_interior_unions_intervals])
-        note qk=division_ofD[OF q(1)[OF k]]
-        show "finite (q k - {k})" "open (interior k)" "\<forall>t\<in>q k - {k}. \<exists>a b. t = cbox a b"
-          using qk by auto
-        show "\<forall>t\<in>q k - {k}. interior k \<inter> interior t = {}"
-          using qk(5) using q(2)[OF k] by auto
-        show "interior (\<Inter>i\<in>p. \<Union>(q i - {i})) \<subseteq> interior (\<Union>(q k - {k}))"
+      have "interior (\<Inter>i\<in>p. \<Union>(q i - {i})) \<inter> interior K = {}"
+      proof (rule *[OF Int_interior_Union_intervals])
+        show "\<And>T. T\<in>q K - {K} \<Longrightarrow> interior K \<inter> interior T = {}"
+          using qk(5) using q(2)[OF K] by auto
+        show "interior (\<Inter>i\<in>p. \<Union>(q i - {i})) \<subseteq> interior (\<Union>(q K - {K}))"
           apply (rule interior_mono)+
-          using k
-          apply auto
-          done
-      qed } note [simp] = this
+          using K by auto
+      qed (use qk in auto)} note [simp] = this
     show "d \<union> p division_of (cbox a b)"
       unfolding cbox_eq
       apply (rule division_disjoint_union[OF d assms(1)])
-      apply (rule inter_interior_unions_intervals)
+      apply (rule Int_interior_Union_intervals)
       apply (rule p open_interior ballI)+
       apply simp_all
       done
@@ -726,12 +705,12 @@
 qed
 
 lemma elementary_bounded[dest]:
-  fixes s :: "'a::euclidean_space set"
-  shows "p division_of s \<Longrightarrow> bounded s"
+  fixes S :: "'a::euclidean_space set"
+  shows "p division_of S \<Longrightarrow> bounded S"
   unfolding division_of_def by (metis bounded_Union bounded_cbox)
 
 lemma elementary_subset_cbox:
-  "p division_of s \<Longrightarrow> \<exists>a b. s \<subseteq> cbox a (b::'a::euclidean_space)"
+  "p division_of S \<Longrightarrow> \<exists>a b. S \<subseteq> cbox a (b::'a::euclidean_space)"
   by (meson elementary_bounded bounded_subset_cbox)
 
 lemma division_union_intervals_exists:
@@ -758,16 +737,16 @@
     obtain u v where uv: "cbox a b \<inter> cbox c d = cbox u v"
       unfolding Int_interval by auto
     have uv_sub: "cbox u v \<subseteq> cbox c d" using uv by auto
-    obtain p where "p division_of cbox c d" "cbox u v \<in> p"
+    obtain p where pd: "p division_of cbox c d" and "cbox u v \<in> p"
       by (rule partial_division_extend_1[OF uv_sub False[unfolded uv]])
-    note p = this division_ofD[OF this(1)]
+    note p = this division_ofD[OF pd]
     have "interior (cbox a b \<inter> \<Union>(p - {cbox u v})) = interior(cbox u v \<inter> \<Union>(p - {cbox u v}))"
       apply (rule arg_cong[of _ _ interior])
       using p(8) uv by auto
     also have "\<dots> = {}"
       unfolding interior_Int
-      apply (rule inter_interior_unions_intervals)
-      using p(6) p(7)[OF p(2)] p(3)
+      apply (rule Int_interior_Union_intervals)
+      using p(6) p(7)[OF p(2)] \<open>finite p\<close>
       apply auto
       done
     finally have [simp]: "interior (cbox a b) \<inter> interior (\<Union>(p - {cbox u v})) = {}" by simp
@@ -784,59 +763,45 @@
   qed
 qed
 
-lemma division_of_unions:
+lemma division_of_Union:
   assumes "finite f"
     and "\<And>p. p \<in> f \<Longrightarrow> p division_of (\<Union>p)"
     and "\<And>k1 k2. k1 \<in> \<Union>f \<Longrightarrow> k2 \<in> \<Union>f \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior k1 \<inter> interior k2 = {}"
   shows "\<Union>f division_of \<Union>\<Union>f"
-  using assms
-  by (auto intro!: division_ofI)
+  using assms  by (auto intro!: division_ofI)
 
 lemma elementary_union_interval:
   fixes a b :: "'a::euclidean_space"
   assumes "p division_of \<Union>p"
   obtains q where "q division_of (cbox a b \<union> \<Union>p)"
-proof -
-  note assm = division_ofD[OF assms]
-  have lem1: "\<And>f s. \<Union>\<Union>(f ` s) = \<Union>((\<lambda>x. \<Union>(f x)) ` s)"
-    by auto
-  have lem2: "\<And>f s. f \<noteq> {} \<Longrightarrow> \<Union>{s \<union> t |t. t \<in> f} = s \<union> \<Union>f"
+proof (cases "p = {} \<or> cbox a b = {}")
+  case True
+  obtain p where "p division_of (cbox a b)"
+    by (rule elementary_interval)
+  then show thesis
+    using True assms that by auto
+next
+  case False
+  then have "p \<noteq> {}" "cbox a b \<noteq> {}"
     by auto
-  {
-    presume "p = {} \<Longrightarrow> thesis"
-      "cbox a b = {} \<Longrightarrow> thesis"
-      "cbox a b \<noteq> {} \<Longrightarrow> interior (cbox a b) = {} \<Longrightarrow> thesis"
-      "p \<noteq> {} \<Longrightarrow> interior (cbox a b)\<noteq>{} \<Longrightarrow> cbox a b \<noteq> {} \<Longrightarrow> thesis"
-    then show thesis by auto
+  note pdiv = division_ofD[OF assms]
+  show ?thesis
+  proof (cases "interior (cbox a b) = {}")
+    case True
+    show ?thesis
+      apply (rule that [of "insert (cbox a b) p", OF division_ofI])
+      using pdiv(1-4) True False apply auto
+       apply (metis IntI equals0D pdiv(5))
+      by (metis disjoint_iff_not_equal pdiv(5))
   next
-    assume as: "p = {}"
-    obtain p where "p division_of (cbox a b)"
-      by (rule elementary_interval)
-    then show thesis
-      using as that by auto
-  next
-    assume as: "cbox a b = {}"
-    show thesis
-      using as assms that by auto
-  next
-    assume as: "interior (cbox a b) = {}" "cbox a b \<noteq> {}"
-    show thesis
-      apply (rule that[of "insert (cbox a b) p"],rule division_ofI)
-      unfolding finite_insert
-      apply (rule assm(1)) unfolding Union_insert
-      using assm(2-4) as
-      apply -
-      apply (fast dest: assm(5))+
-      done
-  next
-    assume as: "p \<noteq> {}" "interior (cbox a b) \<noteq> {}" "cbox a b \<noteq> {}"
+    case False  
     have "\<forall>k\<in>p. \<exists>q. (insert (cbox a b) q) division_of (cbox a b \<union> k)"
     proof
       fix k
       assume kp: "k \<in> p"
-      from assm(4)[OF kp] obtain c d where "k = cbox c d" by blast
+      from pdiv(4)[OF kp] obtain c d where "k = cbox c d" by blast
       then show "\<exists>q. (insert (cbox a b) q) division_of (cbox a b \<union> k)"
-        by (meson as(3) division_union_intervals_exists)
+        by (meson \<open>cbox a b \<noteq> {}\<close> division_union_intervals_exists)
     qed
     from bchoice[OF this] obtain q where "\<forall>x\<in>p. insert (cbox a b) (q x) division_of (cbox a b) \<union> x" ..
     note q = division_ofD[OF this[rule_format]]
@@ -846,69 +811,59 @@
       have *: "{insert (cbox a b) (q k) |k. k \<in> p} = (\<lambda>k. insert (cbox a b) (q k)) ` p"
         by auto
       show "finite ?D"
-        using "*" assm(1) q(1) by auto
+        using "*" pdiv(1) q(1) by auto
+      have lem1: "\<And>f s. \<Union>\<Union>(f ` s) = \<Union>((\<lambda>x. \<Union>(f x)) ` s)"
+        by auto
+      have lem2: "\<And>f s. f \<noteq> {} \<Longrightarrow> \<Union>{s \<union> t |t. t \<in> f} = s \<union> \<Union>f"
+        by auto
       show "\<Union>?D = cbox a b \<union> \<Union>p"
         unfolding * lem1
-        unfolding lem2[OF as(1), of "cbox a b", symmetric]
-        using q(6)
-        by auto
-      fix k
-      assume k: "k \<in> ?D"
-      then show "k \<subseteq> cbox a b \<union> \<Union>p"
-        using q(2) by auto
-      show "k \<noteq> {}"
-        using q(3) k by auto
-      show "\<exists>a b. k = cbox a b"
-        using q(4) k by auto
-      fix k'
-      assume k': "k' \<in> ?D" "k \<noteq> k'"
+        unfolding lem2[OF \<open>p \<noteq> {}\<close>, of "cbox a b", symmetric]
+        using q(6)  by auto
+      show "k \<subseteq> cbox a b \<union> \<Union>p" "k \<noteq> {}" if "k \<in> ?D" for k
+        using q that by blast+
+      show "\<exists>a b. k = cbox a b" if "k \<in> ?D" for k
+        using q(4) that by auto
+    next
+      fix k' k
+      assume k: "k \<in> ?D" and k': "k' \<in> ?D" "k \<noteq> k'"
       obtain x where x: "k \<in> insert (cbox a b) (q x)" "x\<in>p"
         using k by auto
       obtain x' where x': "k'\<in>insert (cbox a b) (q x')" "x'\<in>p"
         using k' by auto
       show "interior k \<inter> interior k' = {}"
-      proof (cases "x = x'")
+      proof (cases "x = x' \<or> k  = cbox a b \<or> k' = cbox a b")
         case True
-        show ?thesis
+        then show ?thesis
           using True k' q(5) x' x by auto
       next
         case False
-        {
-          presume "k = cbox a b \<Longrightarrow> ?thesis"
-            and "k' = cbox a b \<Longrightarrow> ?thesis"
-            and "k \<noteq> cbox a b \<Longrightarrow> k' \<noteq> cbox a b \<Longrightarrow> ?thesis"
-          then show ?thesis by linarith
-        next
-          assume as': "k  = cbox a b"
-          show ?thesis
-            using as' k' q(5) x' by blast
-        next
-          assume as': "k' = cbox a b"
-          show ?thesis
-            using as' k'(2) q(5) x by blast
-        }
-        assume as': "k \<noteq> cbox a b" "k' \<noteq> cbox a b"
+        then have as': "k \<noteq> cbox a b" "k' \<noteq> cbox a b"
+          by auto
         obtain c d where k: "k = cbox c d"
           using q(4)[OF x(2,1)] by blast
         have "interior k \<inter> interior (cbox a b) = {}"
           using as' k'(2) q(5) x by blast
         then have "interior k \<subseteq> interior x"
-        using interior_subset_union_intervals
-          by (metis as(2) k q(2) x interior_subset_union_intervals)
+          by (metis \<open>interior (cbox a b) \<noteq> {}\<close> k q(2) x interior_subset_union_intervals)
         moreover
         obtain c d where c_d: "k' = cbox c d"
           using q(4)[OF x'(2,1)] by blast
         have "interior k' \<inter> interior (cbox a b) = {}"
           using as'(2) q(5) x' by blast
         then have "interior k' \<subseteq> interior x'"
-          by (metis as(2) c_d interior_subset_union_intervals q(2) x'(1) x'(2))
+          by (metis \<open>interior (cbox a b) \<noteq> {}\<close> c_d interior_subset_union_intervals q(2) x'(1) x'(2))
+        moreover have "interior x \<inter> interior x' = {}"
+          by (meson False assms division_ofD(5) x'(2) x(2))
         ultimately show ?thesis
-          using assm(5)[OF x(2) x'(2) False] by auto
+          using \<open>interior k \<subseteq> interior x\<close> \<open>interior k' \<subseteq> interior x'\<close> by auto
       qed
     qed
-  }
+  qed
 qed
 
+
+
 lemma elementary_unions_intervals:
   assumes fin: "finite f"
     and "\<And>s. s \<in> f \<Longrightarrow> \<exists>a b. s = cbox a (b::'a::euclidean_space)"
@@ -993,26 +948,20 @@
     apply(rule assms r2)+
   proof -
     have "interior s \<inter> interior (\<Union>(r1-p)) = {}"
-    proof (rule inter_interior_unions_intervals)
-      show "finite (r1 - p)" and "open (interior s)" and "\<forall>t\<in>r1-p. \<exists>a b. t = cbox a b"
-        using r1 by auto
+    proof (rule Int_interior_Union_intervals)
       have *: "\<And>s. (\<And>x. x \<in> s \<Longrightarrow> False) \<Longrightarrow> s = {}"
         by auto
-      show "\<forall>t\<in>r1-p. interior s \<inter> interior t = {}"
-      proof
-        fix m x
-        assume as: "m \<in> r1 - p"
+      show "interior s \<inter> interior m = {}" if "m \<in> r1 - p" for m 
+      proof -
         have "interior m \<inter> interior (\<Union>p) = {}"
-        proof (rule inter_interior_unions_intervals)
-          show "finite p" and "open (interior m)" and "\<forall>t\<in>p. \<exists>a b. t = cbox a b"
-            using divp by auto
-          show "\<forall>t\<in>p. interior m \<inter> interior t = {}"
-            by (metis DiffD1 DiffD2 as r1(1) r1(7) set_rev_mp)
-        qed
+        proof (rule Int_interior_Union_intervals)
+          show "\<And>t. t\<in>p \<Longrightarrow> interior m \<inter> interior t = {}"
+            by (metis DiffD1 DiffD2 that r1(1) r1(7) set_rev_mp)
+        qed (use divp in auto)
         then show "interior s \<inter> interior m = {}"
           unfolding divp by auto
-      qed
-    qed
+      qed 
+    qed (use r1 in auto)
     then show "interior s \<inter> interior (\<Union>(r1-p) \<inter> (\<Union>q)) = {}"
       using interior_subset by auto
   qed auto
@@ -2023,7 +1972,7 @@
       show ?case
         unfolding Union_insert
         apply (rule assms(2)[rule_format])
-        using inter_interior_unions_intervals [of f "interior x"]
+        using Int_interior_Union_intervals [of f "interior x"]
         apply (auto simp: insert)
         by (metis IntI empty_iff insert.hyps(2) insert.prems(3) insert_iff)
     qed
@@ -2434,9 +2383,8 @@
       apply auto
       done
     then have int: "interior (cbox u v) \<inter> interior (\<Union>{k. \<exists>x. (x, k) \<in> p}) = {}"
-      apply (rule inter_interior_unions_intervals)
+      apply (rule Int_interior_Union_intervals)
       apply (rule open_interior)
-      apply (rule_tac[!] ballI)
       unfolding mem_Collect_eq
       apply (erule_tac[!] exE)
       apply (drule p(4)[OF insertI2])