diff -r 7454317f883c -r 13b051ebc6c5 src/HOL/Analysis/Tagged_Division.thy
--- a/src/HOL/Analysis/Tagged_Division.thy	Tue Aug 01 22:19:37 2017 +0200
+++ b/src/HOL/Analysis/Tagged_Division.thy	Wed Aug 02 16:31:42 2017 +0200
@@ -1504,7 +1504,7 @@
       done
     by (simp add: interval_split k interval_doublesplit)
 qed
-
+              
 lemma (in comm_monoid_set) operative_division:
   fixes g :: "'b::euclidean_space set \<Rightarrow> 'a"
   assumes g: "operative g" and d: "d division_of (cbox a b)" shows "F g d = g (cbox a b)"
@@ -1614,60 +1614,75 @@
         case False
         then have "\<exists>x. x \<in> division_points (cbox a b) d"
           by auto
-        then guess k c
-          unfolding split_paired_Ex division_points_def mem_Collect_eq split_conv
-          apply (elim exE conjE)
-          done
-        note this(2-4,1) note kc=this[unfolded interval_bounds[OF ab']]
-        from this(3) guess j .. note j=this
-        define d1 where "d1 = {l \<inter> {x. x\<bullet>k \<le> c} | l. l \<in> d \<and> l \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}}"
-        define d2 where "d2 = {l \<inter> {x. x\<bullet>k \<ge> c} | l. l \<in> d \<and> l \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}}"
+        then obtain k c 
+          where "k \<in> Basis" "interval_lowerbound (cbox a b) \<bullet> k < c"
+                "c < interval_upperbound (cbox a b) \<bullet> k"
+                "\<exists>i\<in>d. interval_lowerbound i \<bullet> k = c \<or> interval_upperbound i \<bullet> k = c"
+          unfolding division_points_def by auto
+        then obtain j where "a \<bullet> k < c" "c < b \<bullet> k" 
+              and "j \<in> d" and j: "interval_lowerbound j \<bullet> k = c \<or> interval_upperbound j \<bullet> k = c"
+          by (metis division_of_trivial empty_iff interval_bounds' less.prems)
+        let ?lec = "{x. x\<bullet>k \<le> c}" let ?gec = "{x. x\<bullet>k \<ge> c}"
+        define d1 where "d1 = {l \<inter> ?lec | l. l \<in> d \<and> l \<inter> ?lec \<noteq> {}}"
+        define d2 where "d2 = {l \<inter> ?gec | l. l \<in> d \<and> l \<inter> ?gec \<noteq> {}}"
         define cb where "cb = (\<Sum>i\<in>Basis. (if i = k then c else b\<bullet>i) *\<^sub>R i)"
         define ca where "ca = (\<Sum>i\<in>Basis. (if i = k then c else a\<bullet>i) *\<^sub>R i)"
-        note division_points_psubset[OF \<open>d division_of cbox a b\<close> ab kc(1-2) j]
-        note psubset_card_mono[OF _ this(1)] psubset_card_mono[OF _ this(2)]
-        then have *: "F g d1 = g (cbox a b \<inter> {x. x\<bullet>k \<le> c})" "F g d2 = g (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
-          unfolding interval_split[OF kc(4)]
-          apply (rule_tac[!] "less.hyps"[rule_format])
-          using division_split[OF \<open>d division_of cbox a b\<close>, where k=k and c=c]
-          apply (simp_all add: interval_split kc d1_def d2_def division_points_finite[OF \<open>d division_of cbox a b\<close>])
-          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"
-          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])
-            unfolding interior_cbox[symmetric] interval_split[symmetric, OF kc(4)]
-            using division_split_left_inj less as kc leq by blast
-        } 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"
-          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])
-            unfolding interior_cbox[symmetric] interval_split[symmetric,OF kc(4)]
-            using division_split_right_inj less leq as kc by blast
-        } note fxk_ge = this
-        have d1_alt: "d1 = (\<lambda>l. l \<inter> {x. x\<bullet>k \<le> c}) ` {l \<in> d. l \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}}"
+        have "division_points (cbox a b \<inter> ?lec) {l \<inter> ?lec |l. l \<in> d \<and> l \<inter> ?lec \<noteq> {}} 
+              \<subset> division_points (cbox a b) d"
+          by (rule division_points_psubset[OF \<open>d division_of cbox a b\<close> ab \<open>a \<bullet> k < c\<close> \<open>c < b \<bullet> k\<close> \<open>j \<in> d\<close> j \<open>k \<in> Basis\<close>])
+        with division_points_finite[OF \<open>d division_of cbox a b\<close>] 
+        have "card
+         (division_points (cbox a b \<inter> ?lec) {l \<inter> ?lec |l. l \<in> d \<and> l \<inter> ?lec \<noteq> {}})
+           < card (division_points (cbox a b) d)"
+          by (rule psubset_card_mono)
+        moreover have "division_points (cbox a b \<inter> {x. c \<le> x \<bullet> k}) {l \<inter> {x. c \<le> x \<bullet> k} |l. l \<in> d \<and> l \<inter> {x. c \<le> x \<bullet> k} \<noteq> {}}
+              \<subset> division_points (cbox a b) d"
+          by (rule division_points_psubset[OF \<open>d division_of cbox a b\<close> ab \<open>a \<bullet> k < c\<close> \<open>c < b \<bullet> k\<close> \<open>j \<in> d\<close> j \<open>k \<in> Basis\<close>])
+        with division_points_finite[OF \<open>d division_of cbox a b\<close>] 
+        have "card (division_points (cbox a b \<inter> ?gec) {l \<inter> ?gec |l. l \<in> d \<and> l \<inter> ?gec \<noteq> {}})
+              < card (division_points (cbox a b) d)"
+          by (rule psubset_card_mono)
+        ultimately have *: "F g d1 = g (cbox a b \<inter> ?lec)" "F g d2 = g (cbox a b \<inter> ?gec)"
+          unfolding interval_split[OF \<open>k \<in> Basis\<close>]
+          apply (rule_tac[!] less.hyps)
+          using division_split[OF \<open>d division_of cbox a b\<close>, where k=k and c=c] \<open>k \<in> Basis\<close>
+          by (simp_all add: interval_split  d1_def d2_def division_points_finite[OF \<open>d division_of cbox a b\<close>])
+        have fxk_le: "g (l \<inter> ?lec) = \<^bold>1" 
+          if "l \<in> d" "y \<in> d" "l \<inter> ?lec = y \<inter> ?lec" "l \<noteq> y" for l y
+        proof -
+          obtain u v where leq: "l = cbox u v"
+            using \<open>l \<in> d\<close> less.prems by auto
+          have "interior (cbox u v \<inter> ?lec) = {}"
+            using that division_split_left_inj leq less.prems by blast
+          then show ?thesis
+            unfolding leq interval_split[OF \<open>k \<in> Basis\<close>] using g by auto
+        qed
+        have fxk_ge: "g (l \<inter> {x. x \<bullet> k \<ge> c}) = \<^bold>1"
+          if "l \<in> d" "y \<in> d" "l \<inter> ?gec = y \<inter> ?gec" "l \<noteq> y" for l y
+        proof -
+          obtain u v where leq: "l = cbox u v"
+            using \<open>l \<in> d\<close> less.prems by auto
+          have "interior (cbox u v \<inter> ?gec) = {}"
+            using that division_split_right_inj leq less.prems by blast
+          then show ?thesis
+            unfolding leq interval_split[OF \<open>k \<in> Basis\<close>] using g by auto
+        qed
+        have d1_alt: "d1 = (\<lambda>l. l \<inter> ?lec) ` {l \<in> d. l \<inter> ?lec \<noteq> {}}"
           using d1_def by auto
-        have d2_alt: "d2 = (\<lambda>l. l \<inter> {x. x\<bullet>k \<ge> c}) ` {l \<in> d. l \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}}"
+        have d2_alt: "d2 = (\<lambda>l. l \<inter> ?gec) ` {l \<in> d. l \<inter> ?gec \<noteq> {}}"
           using d2_def by auto
         have "g (cbox a b) = F g d1 \<^bold>* F g d2" (is "_ = ?prev")
-          unfolding * using g kc(4) by blast
-        also have "F g d1 = F (\<lambda>l. g (l \<inter> {x. x\<bullet>k \<le> c})) d"
+          unfolding * using g \<open>k \<in> Basis\<close> by blast
+        also have "F g d1 = F (\<lambda>l. g (l \<inter> ?lec)) d"
           unfolding d1_alt using division_of_finite[OF less.prems] fxk_le
           by (subst reindex_nontrivial) (auto intro!: mono_neutral_cong_left simp: operative_empty[OF g])
-        also have "F g d2 = F (\<lambda>l. g (l \<inter> {x. x\<bullet>k \<ge> c})) d"
+        also have "F g d2 = F (\<lambda>l. g (l \<inter> ?gec)) d"
           unfolding d2_alt using division_of_finite[OF less.prems] fxk_ge
           by (subst reindex_nontrivial) (auto intro!: mono_neutral_cong_left simp: operative_empty[OF g])
-        also have *: "\<forall>x\<in>d. g x = g (x \<inter> {x. x \<bullet> k \<le> c}) \<^bold>* g (x \<inter> {x. c \<le> x \<bullet> k})"
+        also have *: "\<forall>x\<in>d. g x = g (x \<inter> ?lec) \<^bold>* g (x \<inter> ?gec)"
           unfolding forall_in_division[OF \<open>d division_of cbox a b\<close>]
-          using g kc(4) by blast
-        have "F (\<lambda>l. g (l \<inter> {x. x\<bullet>k \<le> c})) d \<^bold>* F (\<lambda>l. g (l \<inter> {x. x\<bullet>k \<ge> c})) d = F g d"
+          using g \<open>k \<in> Basis\<close> by blast
+        have "F (\<lambda>l. g (l \<inter> ?lec)) d \<^bold>* F (\<lambda>l. g (l \<inter> ?gec)) d = F g d"
           using * by (simp add: distrib)
         finally show ?thesis by auto
       qed