# HG changeset patch
# User wenzelm
# Date 1358432268 -3600
# Node ID 917e76c53f827eca3249cf8843dc051a96bc7eae
# Parent  a076e01b803f7cc84d9468a030c877e9ae44f127
tuned proofs;

diff -r a076e01b803f -r 917e76c53f82 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Thu Jan 17 14:15:10 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Thu Jan 17 15:17:48 2013 +0100
@@ -89,7 +89,8 @@
       case True
       show ?thesis
         apply (rule assms[OF Suc(1)[OF True]])
-        using `?r` apply auto
+        using `?r`
+        apply auto
         done
     next
       case False
@@ -241,7 +242,8 @@
           thus ?thesis
             apply (rule_tac x=i in bexI, rule_tac x=x in exI, rule_tac x="min d e" in exI)
             unfolding ab
-            using interval_open_subset_closed[of a b] and e apply fastforce+
+            using interval_open_subset_closed[of a b] and e
+            apply fastforce+
             done
         next
           case False
@@ -285,8 +287,10 @@
                 done
               also have "\<dots> < \<bar>e\<bar> / 2 + \<bar>e\<bar> / 2"
                 apply (rule add_strict_left_mono)
-                using as unfolding mem_ball dist_norm
-                using e apply (auto simp add: field_simps)
+                using as
+                unfolding mem_ball dist_norm
+                using e
+                apply (auto simp add: field_simps)
                 done
               finally show "y\<in>ball x e"
                 unfolding mem_ball dist_norm using e by (auto simp add:field_simps)
@@ -415,7 +419,8 @@
   assumes "{a..b}\<noteq>{}"
   shows "content {a..b} = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
   apply (rule content_closed_interval)
-  using assms unfolding interval_ne_empty
+  using assms
+  unfolding interval_ne_empty
   apply assumption
   done
 
@@ -533,10 +538,10 @@
     unfolding content_def
     unfolding interval_bounds[OF ab_ne] interval_bounds[OF cd_ne]
     unfolding if_not_P[OF False] if_not_P[OF `{c..d} \<noteq> {}`]
-    apply(rule setprod_mono,rule)
+    apply (rule setprod_mono, rule)
   proof
     fix i :: 'a
-    assume i:"i\<in>Basis"
+    assume i: "i\<in>Basis"
     show "0 \<le> b \<bullet> i - a \<bullet> i" using ab_ne[THEN bspec, OF i] i by auto
     show "b \<bullet> i - a \<bullet> i \<le> d \<bullet> i - c \<bullet> i"
       using assms[unfolded subset_eq mem_interval,rule_format,OF ab_ab(2),of i]
@@ -620,7 +625,10 @@
     assume "s = {{a}}"
     moreover fix k assume "k\<in>s" 
     ultimately have"\<exists>x y. k = {x..y}"
-      apply (rule_tac x=a in exI)+ unfolding interval_sing by auto
+      apply (rule_tac x=a in exI)+
+      unfolding interval_sing
+      apply auto
+      done
   }
   ultimately show ?l unfolding division_of_def interval_sing by auto
 next
@@ -671,9 +679,9 @@
   assumes "content {a..b} = 0" "d division_of {a..b}"
   shows "\<forall>k\<in>d. content k = 0"
   unfolding forall_in_division[OF assms(2)]
-  apply(rule,rule,rule)
-  apply(drule division_ofD(2)[OF assms(2)])
-  apply(drule content_subset) unfolding assms(1)
+  apply (rule,rule,rule)
+  apply (drule division_ofD(2)[OF assms(2)])
+  apply (drule content_subset) unfolding assms(1)
 proof -
   case goal1
   thus ?case using content_pos_le[of a b] by auto
@@ -748,7 +756,9 @@
 lemma elementary_inter:
   assumes "p1 division_of s" "p2 division_of (t::('a::ordered_euclidean_space) set)"
   shows "\<exists>p. p division_of (s \<inter> t)"
-  by (rule, rule division_inter[OF assms])
+  apply rule
+  apply (rule division_inter[OF assms])
+  done
 
 lemma elementary_inters:
   assumes "finite f" "f\<noteq>{}" "\<forall>s\<in>f. \<exists>p. p division_of (s::('a::ordered_euclidean_space) set)"
@@ -775,21 +785,41 @@
 
 lemma division_disjoint_union:
   assumes "p1 division_of s1" "p2 division_of s2" "interior s1 \<inter> interior s2 = {}"
-  shows "(p1 \<union> p2) division_of (s1 \<union> s2)" proof(rule division_ofI) 
+  shows "(p1 \<union> p2) division_of (s1 \<union> s2)"
+proof (rule division_ofI)
   note d1 = division_ofD[OF assms(1)] and d2 = division_ofD[OF assms(2)]
   show "finite (p1 \<union> p2)" using d1(1) d2(1) by auto
   show "\<Union>(p1 \<union> p2) = s1 \<union> s2" using d1(6) d2(6) by auto
-  { fix k1 k2 assume as:"k1 \<in> p1 \<union> p2" "k2 \<in> p1 \<union> p2" "k1 \<noteq> k2" moreover let ?g="interior k1 \<inter> interior k2 = {}"
-  { assume as:"k1\<in>p1" "k2\<in>p2" have ?g using interior_mono[OF d1(2)[OF as(1)]] interior_mono[OF d2(2)[OF as(2)]]
-      using assms(3) by blast } moreover
-  { assume as:"k1\<in>p2" "k2\<in>p1" have ?g using interior_mono[OF d1(2)[OF as(2)]] interior_mono[OF d2(2)[OF as(1)]]
-      using assms(3) by blast} ultimately
-  show ?g using d1(5)[OF _ _ as(3)] and d2(5)[OF _ _ as(3)] by auto }
-  fix k assume k:"k \<in> p1 \<union> p2"  show "k \<subseteq> s1 \<union> s2" using k d1(2) d2(2) by auto
-  show "k \<noteq> {}" using k d1(3) d2(3) by auto show "\<exists>a b. k = {a..b}" using k d1(4) d2(4) by auto qed
+  {
+    fix k1 k2
+    assume as: "k1 \<in> p1 \<union> p2" "k2 \<in> p1 \<union> p2" "k1 \<noteq> k2"
+    moreover
+    let ?g="interior k1 \<inter> interior k2 = {}"
+    {
+      assume as: "k1\<in>p1" "k2\<in>p2"
+      have ?g
+        using interior_mono[OF d1(2)[OF as(1)]] interior_mono[OF d2(2)[OF as(2)]]
+        using assms(3) by blast
+    }
+    moreover
+    {
+      assume as: "k1\<in>p2" "k2\<in>p1"
+      have ?g
+        using interior_mono[OF d1(2)[OF as(2)]] interior_mono[OF d2(2)[OF as(1)]]
+        using assms(3) by blast
+    }
+    ultimately show ?g using d1(5)[OF _ _ as(3)] and d2(5)[OF _ _ as(3)] by auto
+  }
+  fix k
+  assume k: "k \<in> p1 \<union> p2"
+  show "k \<subseteq> s1 \<union> s2" using k d1(2) d2(2) by auto
+  show "k \<noteq> {}" using k d1(3) d2(3) by auto
+  show "\<exists>a b. k = {a..b}" using k d1(4) d2(4) by auto
+qed
 
 lemma partial_division_extend_1:
-  assumes incl: "{c..d} \<subseteq> {a..b::'a::ordered_euclidean_space}" and nonempty: "{c..d} \<noteq> {}"
+  assumes incl: "{c..d} \<subseteq> {a..b::'a::ordered_euclidean_space}"
+    and nonempty: "{c..d} \<noteq> {}"
   obtains p where "p division_of {a..b}" "{c..d} \<in> p"
 proof
   let ?B = "\<lambda>f::'a\<Rightarrow>'a \<times> 'a. {(\<Sum>i\<in>Basis. (fst (f i) \<bullet> i) *\<^sub>R i) .. (\<Sum>i\<in>Basis. (snd (f i) \<bullet> i) *\<^sub>R i)}"
@@ -800,52 +830,61 @@
     by (auto simp add: interval_eq_empty eucl_le[where 'a='a]
              intro!: image_eqI[where x="\<lambda>(i::'a)\<in>Basis. (c, d)"])
 
-  {  fix i :: 'a assume "i \<in> Basis"
+  {
+    fix i :: 'a
+    assume "i \<in> Basis"
     with incl nonempty have "a \<bullet> i \<le> c \<bullet> i" "c \<bullet> i \<le> d \<bullet> i" "d \<bullet> i \<le> b \<bullet> i"
-      unfolding interval_eq_empty subset_interval by (auto simp: not_le) }
+      unfolding interval_eq_empty subset_interval by (auto simp: not_le)
+  }
   note ord = this
 
   show "p division_of {a..b}"
   proof (rule division_ofI)
-    show "finite p"
-      unfolding p_def by (auto intro!: finite_PiE)
-    { fix k assume "k \<in> p"
+    show "finite p" unfolding p_def by (auto intro!: finite_PiE)
+    {
+      fix k
+      assume "k \<in> p"
       then obtain f where f: "f \<in> Basis \<rightarrow>\<^isub>E {(a, c), (c, d), (d, b)}" and k: "k = ?B f"
         by (auto simp: p_def)
       then show "\<exists>a b. k = {a..b}" by auto
       have "k \<subseteq> {a..b} \<and> k \<noteq> {}"
       proof (simp add: k interval_eq_empty subset_interval not_less, safe)
         fix i :: 'a assume i: "i \<in> Basis"
-        moreover with f have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
+        moreover
+        with f have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
           by (auto simp: PiE_iff)
         moreover note ord[of i]
-        ultimately show "a \<bullet> i \<le> fst (f i) \<bullet> i" "snd (f i) \<bullet> i \<le> b \<bullet> i" "fst (f i) \<bullet> i \<le> snd (f i) \<bullet> i"
+        ultimately
+        show "a \<bullet> i \<le> fst (f i) \<bullet> i" "snd (f i) \<bullet> i \<le> b \<bullet> i" "fst (f i) \<bullet> i \<le> snd (f i) \<bullet> i"
           by (auto simp: subset_iff eucl_le[where 'a='a])
       qed
       then show "k \<noteq> {}" "k \<subseteq> {a .. b}" by auto
-      { 
-      fix l assume "l \<in> p"
-      then obtain g where g: "g \<in> Basis \<rightarrow>\<^isub>E {(a, c), (c, d), (d, b)}" and l: "l = ?B g"
-        by (auto simp: p_def)
-      assume "l \<noteq> k"
-      have "\<exists>i\<in>Basis. f i \<noteq> g i"
-      proof (rule ccontr)
-        assume "\<not> (\<exists>i\<in>Basis. f i \<noteq> g i)"
-        with f g have "f = g"
-          by (auto simp: PiE_iff extensional_def intro!: ext)
-        with `l \<noteq> k` show False
-          by (simp add: l k)
-      qed
-      then guess i ..
-      moreover then have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
-          "g i = (a, c) \<or> g i = (c, d) \<or> g i = (d, b)"
-        using f g by (auto simp: PiE_iff)
-      moreover note ord[of i]
-      ultimately show "interior l \<inter> interior k = {}"
-        by (auto simp add: l k interior_closed_interval disjoint_interval intro!: bexI[of _ i]) }
-      note `k \<subseteq> { a.. b}` }
+      {
+        fix l assume "l \<in> p"
+        then obtain g where g: "g \<in> Basis \<rightarrow>\<^isub>E {(a, c), (c, d), (d, b)}" and l: "l = ?B g"
+          by (auto simp: p_def)
+        assume "l \<noteq> k"
+        have "\<exists>i\<in>Basis. f i \<noteq> g i"
+        proof (rule ccontr)
+          assume "\<not> (\<exists>i\<in>Basis. f i \<noteq> g i)"
+          with f g have "f = g"
+            by (auto simp: PiE_iff extensional_def intro!: ext)
+          with `l \<noteq> k` show False
+            by (simp add: l k)
+        qed
+        then guess i .. note * = this
+        moreover from * have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
+            "g i = (a, c) \<or> g i = (c, d) \<or> g i = (d, b)"
+          using f g by (auto simp: PiE_iff)
+        moreover note ord[of i]
+        ultimately show "interior l \<inter> interior k = {}"
+          by (auto simp add: l k interior_closed_interval disjoint_interval intro!: bexI[of _ i])
+      }
+      note `k \<subseteq> { a.. b}`
+    }
     moreover
-    { fix x assume x: "x \<in> {a .. b}"
+    {
+      fix x assume x: "x \<in> {a .. b}"
       have "\<forall>i\<in>Basis. \<exists>l. x \<bullet> i \<in> {fst l \<bullet> i .. snd l \<bullet> i} \<and> l \<in> {(a, c), (c, d), (d, b)}"
       proof
         fix i :: 'a assume "i \<in> Basis"
@@ -868,61 +907,164 @@
   qed
 qed
 
-lemma partial_division_extend_interval: assumes "p division_of (\<Union>p)" "(\<Union>p) \<subseteq> {a..b}"
-  obtains q where "p \<subseteq> q" "q division_of {a..b::'a::ordered_euclidean_space}" proof(cases "p = {}")
-  case True guess q apply(rule elementary_interval[of a b]) .
-  thus ?thesis apply- apply(rule that[of q]) unfolding True by auto next
-  case False note p = division_ofD[OF assms(1)]
-  have *:"\<forall>k\<in>p. \<exists>q. q division_of {a..b} \<and> k\<in>q" proof case goal1
-    guess c using p(4)[OF goal1] .. then guess d .. note "cd" = this
-    have *:"{c..d} \<subseteq> {a..b}" "{c..d} \<noteq> {}" using p(2,3)[OF goal1, unfolded "cd"] using assms(2) by auto
-    guess q apply(rule partial_division_extend_1[OF *]) . thus ?case unfolding "cd" by auto qed
+lemma partial_division_extend_interval:
+  assumes "p division_of (\<Union>p)" "(\<Union>p) \<subseteq> {a..b}"
+  obtains q where "p \<subseteq> q" "q division_of {a..b::'a::ordered_euclidean_space}"
+proof (cases "p = {}")
+  case True
+  guess q apply (rule elementary_interval[of a b]) .
+  thus ?thesis
+    apply -
+    apply (rule that[of q])
+    unfolding True
+    apply auto
+    done
+next
+  case False
+  note p = division_ofD[OF assms(1)]
+  have *: "\<forall>k\<in>p. \<exists>q. q division_of {a..b} \<and> k\<in>q"
+  proof
+    case goal1
+    guess c using p(4)[OF goal1] ..
+    then guess d .. note "cd" = this
+    have *: "{c..d} \<subseteq> {a..b}" "{c..d} \<noteq> {}"
+      using p(2,3)[OF goal1, unfolded "cd"] using assms(2) by auto
+    guess q apply(rule partial_division_extend_1[OF *]) .
+    thus ?case unfolding "cd" by auto
+  qed
   guess q using bchoice[OF *] .. note q = conjunctD2[OF this[rule_format]]
-  have "\<And>x. x\<in>p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x - {x})" apply(rule,rule_tac p="q x" in division_of_subset) proof-
-    fix x assume x:"x\<in>p" show "q x division_of \<Union>q x" apply-apply(rule division_ofI)
-      using division_ofD[OF q(1)[OF x]] by auto show "q x - {x} \<subseteq> q x" by auto qed
-  hence "\<exists>d. d division_of \<Inter> ((\<lambda>i. \<Union>(q i - {i})) ` p)" apply- apply(rule elementary_inters)
-    apply(rule finite_imageI[OF p(1)]) unfolding image_is_empty apply(rule False) by auto
+  have "\<And>x. x\<in>p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x - {x})"
+    apply (rule, rule_tac p="q x" in division_of_subset)
+  proof -
+    fix x
+    assume x: "x\<in>p"
+    show "q x division_of \<Union>q x"
+      apply -
+      apply (rule division_ofI)
+      using division_ofD[OF q(1)[OF x]]
+      apply auto
+      done
+    show "q x - {x} \<subseteq> q x" by auto
+  qed
+  hence "\<exists>d. d division_of \<Inter> ((\<lambda>i. \<Union>(q i - {i})) ` p)"
+    apply -
+    apply (rule elementary_inters)
+    apply (rule finite_imageI[OF p(1)])
+    unfolding image_is_empty
+    apply (rule False)
+    apply auto
+    done
   then guess d .. note d = this
-  show ?thesis apply(rule that[of "d \<union> p"]) proof-
-    have *:"\<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 *:"{a..b} = \<Inter> (\<lambda>i. \<Union>(q i - {i})) ` p \<union> \<Union>p" apply(rule *[OF False]) proof fix i assume i:"i\<in>p"
-      show "\<Union>(q i - {i}) \<union> i = {a..b}" using division_ofD(6)[OF q(1)[OF i]] using q(2)[OF i] by auto qed
-    show "d \<union> p division_of {a..b}" unfolding * apply(rule division_disjoint_union[OF d assms(1)])
-      apply(rule inter_interior_unions_intervals) apply(rule p open_interior ballI)+ proof(assumption,rule)
-      fix k assume k:"k\<in>p" have *:"\<And>u t s. u \<subseteq> s \<Longrightarrow> s \<inter> t = {} \<Longrightarrow> u \<inter> t = {}" by auto
-      show "interior (\<Inter>(\<lambda>i. \<Union>(q i - {i})) ` p) \<inter> interior k = {}" apply(rule *[of _ "interior (\<Union>(q k - {k}))"])
-        defer apply(subst Int_commute) apply(rule inter_interior_unions_intervals) proof- 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 = {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
-        have *:"\<And>x s. x \<in> s \<Longrightarrow> \<Inter>s \<subseteq> x" by auto show "interior (\<Inter>(\<lambda>i. \<Union>(q i - {i})) ` p) \<subseteq> interior (\<Union>(q k - {k}))"
-          apply(rule interior_mono *)+ using k by auto qed qed qed auto qed
+  show ?thesis
+    apply (rule that[of "d \<union> p"])
+  proof -
+    have *: "\<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 *: "{a..b} = \<Inter> (\<lambda>i. \<Union>(q i - {i})) ` p \<union> \<Union>p"
+      apply (rule *[OF False])
+    proof
+      fix i
+      assume i: "i\<in>p"
+      show "\<Union>(q i - {i}) \<union> i = {a..b}"
+        using division_ofD(6)[OF q(1)[OF i]] using q(2)[OF i] by auto
+    qed
+    show "d \<union> p division_of {a..b}"
+      unfolding *
+      apply (rule division_disjoint_union[OF d assms(1)])
+      apply (rule inter_interior_unions_intervals)
+      apply (rule p open_interior ballI)+
+    proof (assumption, rule)
+      fix k
+      assume k: "k\<in>p"
+      have *: "\<And>u t s. u \<subseteq> s \<Longrightarrow> s \<inter> t = {} \<Longrightarrow> u \<inter> t = {}" by auto
+      show "interior (\<Inter>(\<lambda>i. \<Union>(q i - {i})) ` p) \<inter> interior k = {}"
+        apply (rule *[of _ "interior (\<Union>(q k - {k}))"])
+        defer
+        apply (subst Int_commute)
+        apply (rule inter_interior_unions_intervals)
+      proof -
+        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 = {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
+        have *: "\<And>x s. x \<in> s \<Longrightarrow> \<Inter>s \<subseteq> x" by auto
+        show "interior (\<Inter>(\<lambda>i. \<Union>(q i - {i})) ` p) \<subseteq> interior (\<Union>(q k - {k}))"
+          apply (rule interior_mono *)+
+          using k by auto
+      qed
+    qed
+  qed auto
+qed
 
 lemma elementary_bounded[dest]: "p division_of s \<Longrightarrow> bounded (s::('a::ordered_euclidean_space) set)"
   unfolding division_of_def by(metis bounded_Union bounded_interval) 
 
 lemma elementary_subset_interval: "p division_of s \<Longrightarrow> \<exists>a b. s \<subseteq> {a..b::'a::ordered_euclidean_space}"
-  by(meson elementary_bounded bounded_subset_closed_interval)
-
-lemma division_union_intervals_exists: assumes "{a..b::'a::ordered_euclidean_space} \<noteq> {}"
-  obtains p where "(insert {a..b} p) division_of ({a..b} \<union> {c..d})" proof(cases "{c..d} = {}")
-  case True show ?thesis apply(rule that[of "{}"]) unfolding True using assms by auto next
-  case False note false=this show ?thesis proof(cases "{a..b} \<inter> {c..d} = {}")
-  have *:"\<And>a b. {a,b} = {a} \<union> {b}" by auto
-  case True show ?thesis apply(rule that[of "{{c..d}}"]) unfolding * apply(rule division_disjoint_union)
-    using false True assms using interior_subset by auto next
-  case False obtain u v where uv:"{a..b} \<inter> {c..d} = {u..v}" unfolding inter_interval by auto
-  have *:"{u..v} \<subseteq> {c..d}" using uv by auto
-  guess p apply(rule partial_division_extend_1[OF * False[unfolded uv]]) . note p=this division_ofD[OF this(1)]
-  have *:"{a..b} \<union> {c..d} = {a..b} \<union> \<Union>(p - {{u..v}})" "\<And>x s. insert x s = {x} \<union> s" using p(8) unfolding uv[THEN sym] by auto
-  show thesis apply(rule that[of "p - {{u..v}}"]) unfolding *(1) apply(subst *(2)) apply(rule division_disjoint_union)
-    apply(rule,rule assms) apply(rule division_of_subset[of p]) apply(rule division_of_union_self[OF p(1)]) defer
-    unfolding interior_inter[THEN sym] proof-
-    have *:"\<And>cd p uv ab. p \<subseteq> cd \<Longrightarrow> ab \<inter> cd = uv \<Longrightarrow> ab \<inter> p = uv \<inter> p" by auto
-    have "interior ({a..b} \<inter> \<Union>(p - {{u..v}})) = interior({u..v} \<inter> \<Union>(p - {{u..v}}))" 
-      apply(rule arg_cong[of _ _ interior]) apply(rule *[OF _ uv]) using p(8) by auto
-    also have "\<dots> = {}" unfolding interior_inter apply(rule inter_interior_unions_intervals) using p(6) p(7)[OF p(2)] p(3) by auto
-    finally show "interior ({a..b} \<inter> \<Union>(p - {{u..v}})) = {}" by assumption qed auto qed qed
+  by (meson elementary_bounded bounded_subset_closed_interval)
+
+lemma division_union_intervals_exists:
+  assumes "{a..b::'a::ordered_euclidean_space} \<noteq> {}"
+  obtains p where "(insert {a..b} p) division_of ({a..b} \<union> {c..d})"
+proof (cases "{c..d} = {}")
+  case True
+  show ?thesis
+    apply (rule that[of "{}"])
+    unfolding True
+    using assms
+    apply auto
+    done
+next
+  case False
+  note false=this
+  show ?thesis
+  proof (cases "{a..b} \<inter> {c..d} = {}")
+    case True
+    have *:"\<And>a b. {a,b} = {a} \<union> {b}" by auto
+    show ?thesis
+      apply (rule that[of "{{c..d}}"])
+      unfolding *
+      apply (rule division_disjoint_union)
+      using false True assms
+      using interior_subset
+      apply auto
+      done
+  next
+    case False
+    obtain u v where uv: "{a..b} \<inter> {c..d} = {u..v}"
+      unfolding inter_interval by auto
+    have *: "{u..v} \<subseteq> {c..d}" using uv by auto
+    guess p apply (rule partial_division_extend_1[OF * False[unfolded uv]]) .
+    note p=this division_ofD[OF this(1)]
+    have *: "{a..b} \<union> {c..d} = {a..b} \<union> \<Union>(p - {{u..v}})" "\<And>x s. insert x s = {x} \<union> s"
+      using p(8) unfolding uv[THEN sym] by auto
+    show ?thesis
+      apply (rule that[of "p - {{u..v}}"])
+      unfolding *(1)
+      apply (subst *(2))
+      apply (rule division_disjoint_union)
+      apply (rule, rule assms)
+      apply (rule division_of_subset[of p])
+      apply (rule division_of_union_self[OF p(1)])
+      defer
+      unfolding interior_inter[THEN sym]
+    proof -
+      have *: "\<And>cd p uv ab. p \<subseteq> cd \<Longrightarrow> ab \<inter> cd = uv \<Longrightarrow> ab \<inter> p = uv \<inter> p" by auto
+      have "interior ({a..b} \<inter> \<Union>(p - {{u..v}})) = interior({u..v} \<inter> \<Union>(p - {{u..v}}))" 
+        apply (rule arg_cong[of _ _ interior])
+        apply (rule *[OF _ uv])
+        using p(8)
+        apply auto
+        done
+      also have "\<dots> = {}"
+        unfolding interior_inter
+        apply (rule inter_interior_unions_intervals)
+        using p(6) p(7)[OF p(2)] p(3)
+        apply auto
+        done
+      finally show "interior ({a..b} \<inter> \<Union>(p - {{u..v}})) = {}" .
+    qed auto
+  qed
+qed
 
 lemma division_of_unions: assumes "finite f"  "\<And>p. p\<in>f \<Longrightarrow> p division_of (\<Union>p)"
   "\<And>k1 k2. \<lbrakk>k1 \<in> \<Union>f; k2 \<in> \<Union>f; k1 \<noteq> k2\<rbrakk> \<Longrightarrow> interior k1 \<inter> interior k2 = {}"