# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1501511901 -3600
# Node ID 829f1f62b08700197a301125b2400d47e7b7684c
# Parent  1b4aa3e3e4e69de2caaec5766c7b5d5bb1cc1caf
more cleanup of Tagged_Division

diff -r 1b4aa3e3e4e6 -r 829f1f62b087 src/HOL/Analysis/Tagged_Division.thy
--- a/src/HOL/Analysis/Tagged_Division.thy	Sun Jul 30 21:44:23 2017 +0100
+++ b/src/HOL/Analysis/Tagged_Division.thy	Mon Jul 31 15:38:21 2017 +0100
@@ -795,20 +795,20 @@
       by (metis disjoint_iff_not_equal pdiv(5))
   next
     case False  
-    have "\<forall>k\<in>p. \<exists>q. (insert (cbox a b) q) division_of (cbox a b \<union> k)"
+    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 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)"
+      fix K
+      assume kp: "K \<in> p"
+      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 \<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]]
-    let ?D = "\<Union>{insert (cbox a b) (q k) | k. k \<in> p}"
+    let ?D = "\<Union>{insert (cbox a b) (q K) | K. K \<in> p}"
     show thesis
     proof (rule that[OF division_ofI])
-      have *: "{insert (cbox a b) (q k) |k. k \<in> p} = (\<lambda>k. insert (cbox a b) (q k)) ` p"
+      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 "*" pdiv(1) q(1) by auto
@@ -820,43 +820,43 @@
         unfolding * lem1
         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
+      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
+      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' \<or> k  = cbox a b \<or> k' = cbox a b")
+      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' \<or> K  = cbox a b \<or> K' = cbox a b")
         case True
         then show ?thesis
-          using True k' q(5) x' x by auto
+          using True K' q(5) x' x by auto
       next
         case False
-        then have 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"
-          by (metis \<open>interior (cbox a b) \<noteq> {}\<close> k q(2) x interior_subset_union_intervals)
+        obtain c d where K: "K = cbox c d"
+          using q(4) x 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"
+          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"
+        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) = {}"
+        have "interior K' \<inter> interior (cbox a b) = {}"
           using as'(2) q(5) x' by blast
-        then have "interior k' \<subseteq> interior x'"
+        then have "interior K' \<subseteq> interior x'"
           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 \<open>interior k \<subseteq> interior x\<close> \<open>interior k' \<subseteq> interior x'\<close> by auto
+          using \<open>interior K \<subseteq> interior x\<close> \<open>interior K' \<subseteq> interior x'\<close> by auto
       qed
     qed
   qed
@@ -888,11 +888,11 @@
 qed
 
 lemma elementary_union:
-  fixes s t :: "'a::euclidean_space set"
-  assumes "ps division_of s" "pt division_of t"
-  obtains p where "p division_of (s \<union> t)"
+  fixes S T :: "'a::euclidean_space set"
+  assumes "ps division_of S" "pt division_of T"
+  obtains p where "p division_of (S \<union> T)"
 proof -
-  have *: "s \<union> t = \<Union>ps \<union> \<Union>pt"
+  have *: "S \<union> T = \<Union>ps \<union> \<Union>pt"
     using assms unfolding division_of_def by auto
   show ?thesis
     apply (rule elementary_unions_intervals[of "ps \<union> pt"])
@@ -901,14 +901,14 @@
 qed
 
 lemma partial_division_extend:
-  fixes t :: "'a::euclidean_space set"
-  assumes "p division_of s"
-    and "q division_of t"
-    and "s \<subseteq> t"
-  obtains r where "p \<subseteq> r" and "r division_of t"
+  fixes T :: "'a::euclidean_space set"
+  assumes "p division_of S"
+    and "q division_of T"
+    and "S \<subseteq> T"
+  obtains r where "p \<subseteq> r" and "r division_of T"
 proof -
   note divp = division_ofD[OF assms(1)] and divq = division_ofD[OF assms(2)]
-  obtain a b where ab: "t \<subseteq> cbox a b"
+  obtain a b where ab: "T \<subseteq> cbox a b"
     using elementary_subset_cbox[OF assms(2)] by auto
   obtain r1 where "p \<subseteq> r1" "r1 division_of (cbox a b)"
     using assms
@@ -917,54 +917,49 @@
   obtain p' where "p' division_of \<Union>(r1 - p)"
     apply (rule elementary_unions_intervals[of "r1 - p"])
     using r1(3,6)
-    apply auto
+      apply auto
     done
   then obtain r2 where r2: "r2 division_of (\<Union>(r1 - p)) \<inter> (\<Union>q)"
     by (metis assms(2) divq(6) elementary_inter)
   {
     fix x
-    assume x: "x \<in> t" "x \<notin> s"
-    then have "x\<in>\<Union>r1"
-      unfolding r1 using ab by auto
-    then obtain r where r: "r \<in> r1" "x \<in> r"
-      unfolding Union_iff ..
-    moreover
-    have "r \<notin> p"
+    assume x: "x \<in> T" "x \<notin> S"
+    then obtain R where r: "R \<in> r1" "x \<in> R"
+      unfolding r1 using ab
+      by (meson division_contains r1(2) subsetCE)
+    moreover have "R \<notin> p"
     proof
-      assume "r \<in> p"
-      then have "x \<in> s" using divp(2) r by auto
+      assume "R \<in> p"
+      then have "x \<in> S" using divp(2) r by auto
       then show False using x by auto
     qed
     ultimately have "x\<in>\<Union>(r1 - p)" by auto
   }
-  then have *: "t = \<Union>p \<union> (\<Union>(r1 - p) \<inter> \<Union>q)"
+  then have Teq: "T = \<Union>p \<union> (\<Union>(r1 - p) \<inter> \<Union>q)"
     unfolding divp divq using assms(3) by auto
+  have "interior S \<inter> interior (\<Union>(r1-p)) = {}"
+  proof (rule Int_interior_Union_intervals)
+    have *: "\<And>S. (\<And>x. x \<in> S \<Longrightarrow> False) \<Longrightarrow> S = {}"
+      by auto
+    show "interior S \<inter> interior m = {}" if "m \<in> r1 - p" for m 
+    proof -
+      have "interior m \<inter> interior (\<Union>p) = {}"
+      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 (use r1 in auto)
+  then have "interior S \<inter> interior (\<Union>(r1-p) \<inter> (\<Union>q)) = {}"
+    using interior_subset by auto
+  then have div: "p \<union> r2 division_of \<Union>p \<union> \<Union>(r1 - p) \<inter> \<Union>q"
+    by (simp add: assms(1) division_disjoint_union divp(6) r2)
   show ?thesis
     apply (rule that[of "p \<union> r2"])
-    unfolding *
-    defer
-    apply (rule division_disjoint_union)
-    unfolding divp(6)
-    apply(rule assms r2)+
-  proof -
-    have "interior s \<inter> interior (\<Union>(r1-p)) = {}"
-    proof (rule Int_interior_Union_intervals)
-      have *: "\<And>s. (\<And>x. x \<in> s \<Longrightarrow> False) \<Longrightarrow> s = {}"
-        by auto
-      show "interior s \<inter> interior m = {}" if "m \<in> r1 - p" for m 
-      proof -
-        have "interior m \<inter> interior (\<Union>p) = {}"
-        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 (use r1 in auto)
-    then show "interior s \<inter> interior (\<Union>(r1-p) \<inter> (\<Union>q)) = {}"
-      using interior_subset by auto
-  qed auto
+     apply (auto simp: div Teq)
+    done
 qed
 
 
@@ -983,45 +978,51 @@
   show "\<Union>?p1 = ?I1" "\<Union>?p2 = ?I2"
     unfolding p(6)[symmetric] by auto
   {
-    fix k
-    assume "k \<in> ?p1"
-    then guess l unfolding mem_Collect_eq by (elim exE conjE) note l=this
-    guess u v using p(4)[OF l(2)] by (elim exE) note uv=this
-    show "k \<subseteq> ?I1"
+    fix K
+    assume "K \<in> ?p1"
+    then obtain l where l: "K = l \<inter> {x. x \<bullet> k \<le> c}" "l \<in> p" "l \<inter> {x. x \<bullet> k \<le> c} \<noteq> {}"
+      by blast
+    obtain u v where uv: "l = cbox u v"
+      using assms(1) l(2) by blast
+    show "K \<subseteq> ?I1"
       using l p(2) uv by force
-    show  "k \<noteq> {}"
+    show  "K \<noteq> {}"
       by (simp add: l)
-    show  "\<exists>a b. k = cbox a b"
+    show  "\<exists>a b. K = cbox a b"
       apply (simp add: l uv p(2-3)[OF l(2)])
       apply (subst interval_split[OF k])
       apply (auto intro: order.trans)
       done
-    fix k'
-    assume "k' \<in> ?p1"
-    then guess l' unfolding mem_Collect_eq by (elim exE conjE) note l'=this
-    assume "k \<noteq> k'"
-    then show "interior k \<inter> interior k' = {}"
+    fix K'
+    assume "K' \<in> ?p1"
+    then obtain l' where l': "K' = l' \<inter> {x. x \<bullet> k \<le> c}" "l' \<in> p" "l' \<inter> {x. x \<bullet> k \<le> c} \<noteq> {}"
+      by blast
+    assume "K \<noteq> K'"
+    then show "interior K \<inter> interior K' = {}"
       unfolding l l' using p(5)[OF l(2) l'(2)] by auto
   }
   {
-    fix k
-    assume "k \<in> ?p2"
-    then guess l unfolding mem_Collect_eq by (elim exE conjE) note l=this
-    guess u v using p(4)[OF l(2)] by (elim exE) note uv=this
-    show "k \<subseteq> ?I2"
+    fix K
+    assume "K \<in> ?p2"
+    then obtain l where l: "K = l \<inter> {x. c \<le> x \<bullet> k}" "l \<in> p" "l \<inter> {x. c \<le> x \<bullet> k} \<noteq> {}"
+      by blast
+    obtain u v where uv: "l = cbox u v"
+      using l(2) p(4) by blast
+    show "K \<subseteq> ?I2"
       using l p(2) uv by force
-    show  "k \<noteq> {}"
+    show  "K \<noteq> {}"
       by (simp add: l)
-    show  "\<exists>a b. k = cbox a b"
+    show  "\<exists>a b. K = cbox a b"
       apply (simp add: l uv p(2-3)[OF l(2)])
       apply (subst interval_split[OF k])
       apply (auto intro: order.trans)
       done
-    fix k'
-    assume "k' \<in> ?p2"
-    then guess l' unfolding mem_Collect_eq by (elim exE conjE) note l'=this
-    assume "k \<noteq> k'"
-    then show "interior k \<inter> interior k' = {}"
+    fix K'
+    assume "K' \<in> ?p2"
+    then obtain l' where l': "K' = l' \<inter> {x. c \<le> x \<bullet> k}" "l' \<in> p" "l' \<inter> {x. c \<le> x \<bullet> k} \<noteq> {}"
+      by blast
+    assume "K \<noteq> K'"
+    then show "interior K \<inter> interior K' = {}"
       unfolding l l' using p(5)[OF l(2) l'(2)] by auto
   }
 qed
@@ -1070,10 +1071,7 @@
     and "(\<Union>{K. \<exists>x. (x,K) \<in> s} = i)"
   shows "s tagged_division_of i"
   unfolding tagged_division_of
-  using assms
-  apply auto
-  apply fastforce+
-  done
+  using assms  by fastforce
 
 lemma tagged_division_ofD[dest]:  (*FIXME USE A LOCALE*)
   assumes "s tagged_division_of i"
@@ -1325,67 +1323,58 @@
     "\<forall>i\<in>Basis. (\<Sum>i\<in>Basis. (if i = k then max (a \<bullet> k) c else a \<bullet> i) *\<^sub>R i) \<bullet> i \<le> b\<bullet>i"
     "min (b \<bullet> k) c = c" "max (a \<bullet> k) c = c"
     using assms using less_imp_le by auto
-  show ?t1 (*FIXME a horrible mess*)
+   have "\<exists>i\<in>d. interval_lowerbound i \<bullet> x = y \<or> interval_upperbound i \<bullet> x = y"
+     if "a \<bullet> x < y" "y < (if x = k then c else b \<bullet> x)"
+        "interval_lowerbound i \<bullet> x = y \<or> interval_upperbound i \<bullet> x = y"
+        "i = l \<inter> {x. x \<bullet> k \<le> c}" "l \<in> d" "l \<inter> {x. x \<bullet> k \<le> c} \<noteq> {}"
+        "x \<in> Basis" for i l x y
+  proof -
+    obtain u v where l: "l = cbox u v"
+      using \<open>l \<in> d\<close> assms(1) by blast
+    have *: "\<forall>i\<in>Basis. u \<bullet> i \<le> (\<Sum>i\<in>Basis. (if i = k then min (v \<bullet> k) c else v \<bullet> i) *\<^sub>R i) \<bullet> i"
+      using that(6) unfolding l interval_split[OF k] box_ne_empty that .
+    have **: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i"
+      using l using that(6) unfolding box_ne_empty[symmetric] by auto
+    show ?thesis
+      apply (rule bexI[OF _ \<open>l \<in> d\<close>])
+      using that(1-3,5) \<open>x \<in> Basis\<close>
+      unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] that
+      apply (auto split: if_split_asm)
+      done
+  qed
+  moreover have "\<And>x y. \<lbrakk>y < (if x = k then c else b \<bullet> x)\<rbrakk> \<Longrightarrow> y < b \<bullet> x"
+    using \<open>c < b\<bullet>k\<close> by (auto split: if_split_asm)
+  ultimately show ?t1 
+    unfolding division_points_def interval_split[OF k, of a b]
+    unfolding interval_bounds[OF *(1)] interval_bounds[OF *(2)] interval_bounds[OF *(3)]
+    unfolding * by force
+  have "\<And>x y i l. (if x = k then c else a \<bullet> x) < y \<Longrightarrow> a \<bullet> x < y"
+    using \<open>a\<bullet>k < c\<close> by (auto split: if_split_asm)
+  moreover have "\<exists>i\<in>d. interval_lowerbound i \<bullet> x = y \<or>
+                       interval_upperbound i \<bullet> x = y"
+    if "(if x = k then c else a \<bullet> x) < y" "y < b \<bullet> x"
+      "interval_lowerbound i \<bullet> x = y \<or> interval_upperbound i \<bullet> x = y"
+      "i = l \<inter> {x. c \<le> x \<bullet> k}" "l \<in> d" "l \<inter> {x. c \<le> x \<bullet> k} \<noteq> {}"
+      "x \<in> Basis" for x y i l
+  proof -
+    obtain u v where l: "l = cbox u v"
+      using \<open>l \<in> d\<close> assm(4) by blast
+    have *: "\<forall>i\<in>Basis. (\<Sum>i\<in>Basis. (if i = k then max (u \<bullet> k) c else u \<bullet> i) *\<^sub>R i) \<bullet> i \<le> v \<bullet> i"
+      using that(6) unfolding l interval_split[OF k] box_ne_empty that .
+    have **: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i"
+      using l using that(6) unfolding box_ne_empty[symmetric] by auto
+    show "\<exists>i\<in>d. interval_lowerbound i \<bullet> x = y \<or> interval_upperbound i \<bullet> x = y"
+      apply (rule bexI[OF _ \<open>l \<in> d\<close>])
+      using that(1-3,5) \<open>x \<in> Basis\<close>
+      unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] that
+      apply (auto split: if_split_asm)
+      done
+  qed
+  ultimately show ?t2
     unfolding division_points_def interval_split[OF k, of a b]
     unfolding interval_bounds[OF *(1)] interval_bounds[OF *(2)] interval_bounds[OF *(3)]
     unfolding *
-    apply (rule subsetI)
-    unfolding mem_Collect_eq split_beta
-    apply (erule bexE conjE)+
-    apply (simp add: )
-    apply (erule exE conjE)+
-  proof
-    fix i l x
-    assume as:
-      "a \<bullet> fst x < snd x" "snd x < (if fst x = k then c else b \<bullet> fst x)"
-      "interval_lowerbound i \<bullet> fst x = snd x \<or> interval_upperbound i \<bullet> fst x = snd x"
-      "i = l \<inter> {x. x \<bullet> k \<le> c}" "l \<in> d" "l \<inter> {x. x \<bullet> k \<le> c} \<noteq> {}"
-      and fstx: "fst x \<in> Basis"
-    from assm(4)[OF this(5)] guess u v apply-by(erule exE)+ note l=this
-    have *: "\<forall>i\<in>Basis. u \<bullet> i \<le> (\<Sum>i\<in>Basis. (if i = k then min (v \<bullet> k) c else v \<bullet> i) *\<^sub>R i) \<bullet> i"
-      using as(6) unfolding l interval_split[OF k] box_ne_empty as .
-    have **: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i"
-      using l using as(6) unfolding box_ne_empty[symmetric] by auto
-    show "\<exists>i\<in>d. interval_lowerbound i \<bullet> fst x = snd x \<or> interval_upperbound i \<bullet> fst x = snd x"
-      apply (rule bexI[OF _ \<open>l \<in> d\<close>])
-      using as(1-3,5) fstx
-      unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] as
-      apply (auto split: if_split_asm)
-      done
-    show "snd x < b \<bullet> fst x"
-      using as(2) \<open>c < b\<bullet>k\<close> by (auto split: if_split_asm)
-  qed
-  show ?t2
-    unfolding division_points_def interval_split[OF k, of a b]
-    unfolding interval_bounds[OF *(1)] interval_bounds[OF *(2)] interval_bounds[OF *(3)]
-    unfolding *
-    unfolding subset_eq
-    apply rule
-    unfolding mem_Collect_eq split_beta
-    apply (erule bexE conjE)+
-    apply (simp only: mem_Collect_eq inner_sum_left_Basis simp_thms)
-    apply (erule exE conjE)+
-  proof
-    fix i l x
-    assume as:
-      "(if fst x = k then c else a \<bullet> fst x) < snd x" "snd x < b \<bullet> fst x"
-      "interval_lowerbound i \<bullet> fst x = snd x \<or> interval_upperbound i \<bullet> fst x = snd x"
-      "i = l \<inter> {x. c \<le> x \<bullet> k}" "l \<in> d" "l \<inter> {x. c \<le> x \<bullet> k} \<noteq> {}"
-      and fstx: "fst x \<in> Basis"
-    from assm(4)[OF this(5)] guess u v by (elim exE) note l=this
-    have *: "\<forall>i\<in>Basis. (\<Sum>i\<in>Basis. (if i = k then max (u \<bullet> k) c else u \<bullet> i) *\<^sub>R i) \<bullet> i \<le> v \<bullet> i"
-      using as(6) unfolding l interval_split[OF k] box_ne_empty as .
-    have **: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i"
-      using l using as(6) unfolding box_ne_empty[symmetric] by auto
-    show "\<exists>i\<in>d. interval_lowerbound i \<bullet> fst x = snd x \<or> interval_upperbound i \<bullet> fst x = snd x"
-      apply (rule bexI[OF _ \<open>l \<in> d\<close>])
-      using as(1-3,5) fstx
-      unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] as
-      apply (auto split: if_split_asm)
-      done
-    show "a \<bullet> fst x < snd x"
-      using as(1) \<open>a\<bullet>k < c\<close> by (auto split: if_split_asm)
-   qed
+    by force
 qed
 
 lemma division_points_psubset:
@@ -1393,7 +1382,7 @@
   assumes "d division_of (cbox a b)"
       and "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"  "a\<bullet>k < c" "c < b\<bullet>k"
       and "l \<in> d"
-      and "interval_lowerbound l\<bullet>k = c \<or> interval_upperbound l\<bullet>k = c"
+      and disj: "interval_lowerbound l\<bullet>k = c \<or> interval_upperbound l\<bullet>k = c"
       and k: "k \<in> Basis"
   shows "division_points (cbox a b \<inter> {x. x\<bullet>k \<le> c}) {l \<inter> {x. x\<bullet>k \<le> c} | l. l\<in>d \<and> l \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}} \<subset>
          division_points (cbox a b) d" (is "?D1 \<subset> ?D")
@@ -1571,8 +1560,12 @@
         have "(1/2) *\<^sub>R (a+b) \<in> cbox a b"
           unfolding mem_box using ab by (auto simp: inner_simps)
         note this[unfolded division_ofD(6)[OF \<open>d division_of cbox a b\<close>,symmetric] Union_iff]
-        then guess i .. note i=this
-        guess u v using d'[rule_format,OF i(1)] by (elim exE conjE) note uv=this
+        then obtain i where i: "i \<in> d" "(1 / 2) *\<^sub>R (a + b) \<in> i" ..
+        obtain u v where uv: "i = cbox u v" 
+                     "\<forall>j\<in>Basis. u \<bullet> j = a \<bullet> j \<and> v \<bullet> j = a \<bullet> j \<or>
+                                u \<bullet> j = b \<bullet> j \<and> v \<bullet> j = b \<bullet> j \<or>
+                                u \<bullet> j = a \<bullet> j \<and> v \<bullet> j = b \<bullet> j"
+          using d' i(1) by auto
         have "cbox a b \<in> d"
         proof -
           have "u = a" "v = b"
@@ -1595,7 +1588,11 @@
           assume x: "x \<in> d - {cbox a b}"
           then have "x\<in>d"
             by auto note d'[rule_format,OF this]
-          then guess u v by (elim exE conjE) note uv=this
+          then obtain u v where uv: "x = cbox u v"
+                      "\<forall>j\<in>Basis. u \<bullet> j = a \<bullet> j \<and> v \<bullet> j = a \<bullet> j \<or>
+                                 u \<bullet> j = b \<bullet> j \<and> v \<bullet> j = b \<bullet> j \<or>
+                                 u \<bullet> j = a \<bullet> j \<and> v \<bullet> j = b \<bullet> j" 
+            by blast
           have "u \<noteq> a \<or> v \<noteq> b"
             using x[unfolded uv] by auto
           then obtain j where "u\<bullet>j \<noteq> a\<bullet>j \<or> v\<bullet>j \<noteq> b\<bullet>j" and j: "j \<in> Basis"
@@ -1637,7 +1634,8 @@
           done
         { fix l y
           assume as: "l \<in> d" "y \<in> d" "l \<inter> {x. x \<bullet> k \<le> c} = y \<inter> {x. x \<bullet> k \<le> c}" "l \<noteq> y"
-          from division_ofD(4)[OF \<open>d division_of cbox a b\<close> this(1)] guess u v by (elim exE) note leq=this
+          then obtain u v where leq: "l = cbox u v"
+            by (meson cbox_division_memE less.prems)
           have "g (l \<inter> {x. x \<bullet> k \<le> c}) = \<^bold>1"
             unfolding leq interval_split[OF kc(4)]
             apply (rule operativeD[OF g])
@@ -1646,7 +1644,8 @@
         } note fxk_le = this
         { fix l y
           assume as: "l \<in> d" "y \<in> d" "l \<inter> {x. c \<le> x \<bullet> k} = y \<inter> {x. c \<le> x \<bullet> k}" "l \<noteq> y"
-          from division_ofD(4)[OF \<open>d division_of cbox a b\<close> this(1)] guess u v by (elim exE) note leq=this
+          then obtain u v where leq: "l = cbox u v"
+            by (meson cbox_division_memE less.prems)
           have "g (l \<inter> {x. x \<bullet> k \<ge> c}) = \<^bold>1"
             unfolding leq interval_split[OF kc(4)]
             apply (rule operativeD(1)[OF g])
@@ -2340,13 +2339,11 @@
       unfolding tagged_division_of_def
       by auto
     presume "\<And>p. finite p \<Longrightarrow> ?P p"
-    from this[rule_format,OF * assms(2)] guess q .. note q=this
-    then show ?thesis
-      apply -
-      apply (rule that[of q])
-      unfolding tagged_division_ofD[OF assms(1)]
-      apply auto
-      done
+    from this[rule_format,OF * assms(2)] 
+    obtain q where q: "q tagged_division_of \<Union>{k. \<exists>x. (x, k) \<in> p}" "d fine q" "(\<forall>(x, k)\<in>p. k \<subseteq> d x \<longrightarrow> (x, k) \<in> q)"
+      by auto
+    with that[of q] show ?thesis
+      using assms(1) by auto
   }
   fix p :: "('a::euclidean_space \<times> ('a::euclidean_space set)) set"
   assume as: "finite p"