# HG changeset patch
# User hoelzl
# Date 1470398402 -7200
# Node ID aca2659ebba79c21a255f0336878120247d81d2a
# Parent  bd218a9320b54363495253e9ce2706b08b8821ec
clean up prove for inter_interior_unions_intervals

diff -r bd218a9320b5 -r aca2659ebba7 src/HOL/Multivariate_Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Multivariate_Analysis/Henstock_Kurzweil_Integration.thy	Thu Aug 04 19:36:31 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Henstock_Kurzweil_Integration.thy	Fri Aug 05 14:00:02 2016 +0200
@@ -168,178 +168,45 @@
       by auto (metis IntI UnE empty_iff interior_maximal open_box subsetCE subsetI)
 qed
 
-lemma inter_interior_unions_intervals:
-  fixes f::"('a::euclidean_space) set set"
+lemma interior_Union_subset_cbox:
   assumes "finite f"
-    and "open s"
-    and "\<forall>t\<in>f. \<exists>a b. t = cbox a b"
-    and "\<forall>t\<in>f. s \<inter> (interior t) = {}"
-  shows "s \<inter> interior (\<Union>f) = {}"
-proof (clarsimp simp only: all_not_in_conv [symmetric])
-  fix x
-  assume x: "x \<in> s" "x \<in> interior (\<Union>f)"
-  have lem1: "\<And>x e s U. ball x e \<subseteq> s \<inter> interior U \<longleftrightarrow> ball x e \<subseteq> s \<inter> U"
-    using interior_subset
-    by auto (meson Topology_Euclidean_Space.open_ball contra_subsetD interior_maximal mem_ball)
-  have "\<exists>t\<in>f. \<exists>x. \<exists>e>0. ball x e \<subseteq> s \<inter> t"
-    if "finite f" and "\<forall>t\<in>f. \<exists>a b. t = cbox a b" and "\<exists>x. x \<in> s \<inter> interior (\<Union>f)" for f
-    using that
-  proof (induct rule: finite_induct)
-    case empty
-    obtain x where "x \<in> s \<inter> interior (\<Union>{})"
-      using empty(2) ..
-    then have False
-      unfolding Union_empty interior_empty by auto
-    then show ?case by auto
-  next
-    case (insert i f)
-    obtain x where x: "x \<in> s \<inter> interior (\<Union>insert i f)"
-      using insert(5) ..
-    then obtain e where e: "0 < e \<and> ball x e \<subseteq> s \<inter> interior (\<Union>insert i f)"
-      unfolding open_contains_ball_eq[OF open_Int[OF assms(2) open_interior], rule_format] ..
-    obtain a where "\<exists>b. i = cbox a b"
-      using insert(4)[rule_format,OF insertI1] ..
-    then obtain b where ab: "i = cbox a b" ..
-    show ?case
-    proof (cases "x \<in> i")
-      case False
-      then have "x \<in> UNIV - cbox a b"
-        unfolding ab by auto
-      then obtain d where "0 < d \<and> ball x d \<subseteq> UNIV - cbox a b"
-        unfolding open_contains_ball_eq[OF open_Diff[OF open_UNIV closed_cbox],rule_format] ..
-      then have "0 < d" "ball x (min d e) \<subseteq> UNIV - i"
-        unfolding ab ball_min_Int by auto
-      then have "ball x (min d e) \<subseteq> s \<inter> interior (\<Union>f)"
-        using e unfolding lem1 unfolding  ball_min_Int by auto
-      then have "x \<in> s \<inter> interior (\<Union>f)" using \<open>d>0\<close> e by auto
-      then have "\<exists>t\<in>f. \<exists>x e. 0 < e \<and> ball x e \<subseteq> s \<inter> t"
-        using insert.hyps(3) insert.prems(1) by blast
-      then show ?thesis by auto
-    next
-      case True show ?thesis
-      proof (cases "x\<in>box a b")
-        case True
-        then obtain d where "0 < d \<and> ball x d \<subseteq> box a b"
-          unfolding open_contains_ball_eq[OF open_box,rule_format] ..
-        then show ?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 box_subset_cbox[of a b] and e
-          apply fastforce+
-          done
-      next
-        case False
-        then obtain k where "x\<bullet>k \<le> a\<bullet>k \<or> x\<bullet>k \<ge> b\<bullet>k" and k: "k \<in> Basis"
-          unfolding mem_box by (auto simp add: not_less)
-        then have "x\<bullet>k = a\<bullet>k \<or> x\<bullet>k = b\<bullet>k"
-          using True unfolding ab and mem_box
-            apply (erule_tac x = k in ballE)
-            apply auto
-            done
-        then have "\<exists>x. ball x (e/2) \<subseteq> s \<inter> (\<Union>f)"
-        proof (rule disjE)
-          let ?z = "x - (e/2) *\<^sub>R k"
-          assume as: "x\<bullet>k = a\<bullet>k"
-          have "ball ?z (e / 2) \<inter> i = {}"
-          proof (clarsimp simp only: all_not_in_conv [symmetric])
-            fix y
-            assume "y \<in> ball ?z (e / 2)" and yi: "y \<in> i"
-            then have "dist ?z y < e/2" by auto
-            then have "\<bar>(?z - y) \<bullet> k\<bar> < e/2"
-              using Basis_le_norm[OF k, of "?z - y"] unfolding dist_norm by auto
-            then have "y\<bullet>k < a\<bullet>k"
-              using e k
-              by (auto simp add: field_simps abs_less_iff as inner_simps)
-            then have "y \<notin> i"
-              unfolding ab mem_box by (auto intro!: bexI[OF _ k])
-            then show False using yi by auto
-          qed
-          moreover
-          have "ball ?z (e/2) \<subseteq> s \<inter> (\<Union>insert i f)"
-            apply (rule order_trans[OF _ e[THEN conjunct2, unfolded lem1]])
-          proof
-            fix y
-            assume as: "y \<in> ball ?z (e/2)"
-            have "norm (x - y) \<le> \<bar>e\<bar> / 2 + norm (x - y - (e / 2) *\<^sub>R k)"
-              apply (rule order_trans,rule norm_triangle_sub[of "x - y" "(e/2) *\<^sub>R k"])
-              unfolding norm_scaleR norm_Basis[OF k]
-              apply auto
-              done
-            also have "\<dots> < \<bar>e\<bar> / 2 + \<bar>e\<bar> / 2"
-              apply (rule add_strict_left_mono)
-              using as e
-              apply (auto simp add: field_simps dist_norm)
-              done
-            finally show "y \<in> ball x e"
-              unfolding mem_ball dist_norm using e by (auto simp add:field_simps)
-          qed
-          ultimately show ?thesis
-            apply (rule_tac x="?z" in exI)
-            unfolding Union_insert
-            apply auto
-            done
-        next
-          let ?z = "x + (e/2) *\<^sub>R k"
-          assume as: "x\<bullet>k = b\<bullet>k"
-          have "ball ?z (e / 2) \<inter> i = {}"
-          proof (clarsimp simp only: all_not_in_conv [symmetric])
-            fix y
-            assume "y \<in> ball ?z (e / 2)" and yi: "y \<in> i"
-            then have "dist ?z y < e/2"
-              by auto
-            then have "\<bar>(?z - y) \<bullet> k\<bar> < e/2"
-              using Basis_le_norm[OF k, of "?z - y"]
-              unfolding dist_norm by auto
-            then have "y\<bullet>k > b\<bullet>k"
-              using e k
-              by (auto simp add:field_simps inner_simps inner_Basis as)
-            then have "y \<notin> i"
-              unfolding ab mem_box by (auto intro!: bexI[OF _ k])
-            then show False using yi by auto
-          qed
-          moreover
-          have "ball ?z (e/2) \<subseteq> s \<inter> (\<Union>insert i f)"
-            apply (rule order_trans[OF _ e[THEN conjunct2, unfolded lem1]])
-          proof
-            fix y
-            assume as: "y\<in> ball ?z (e/2)"
-            have "norm (x - y) \<le> \<bar>e\<bar> / 2 + norm (x - y + (e / 2) *\<^sub>R k)"
-              apply (rule order_trans,rule norm_triangle_sub[of "x - y" "- (e/2) *\<^sub>R k"])
-              unfolding norm_scaleR
-              apply (auto simp: k)
-              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)
-              done
-            finally show "y \<in> ball x e"
-              unfolding mem_ball dist_norm using e by (auto simp add:field_simps)
-          qed
-          ultimately show ?thesis
-            apply (rule_tac x="?z" in exI)
-            unfolding Union_insert
-            apply auto
-            done
-        qed
-        then obtain x where "ball x (e / 2) \<subseteq> s \<inter> \<Union>f" ..
-        then have "x \<in> s \<inter> interior (\<Union>f)"
-          unfolding lem1[where U="\<Union>f", symmetric]
-          using centre_in_ball e by auto
-        then show ?thesis
-          using insert.hyps(3) insert.prems(1) by blast
-      qed
-    qed
-  qed
-  from this[OF assms(1,3)] x
-  obtain t x e where "t \<in> f" "0 < e" "ball x e \<subseteq> s \<inter> t"
-    by blast
-  then have "x \<in> s" "x \<in> interior t"
-    using open_subset_interior[OF open_ball, of x e t]
-    by auto
-  then show False
-    using \<open>t \<in> f\<close> assms(4) by auto
-qed
+  assumes f: "\<And>s. s \<in> f \<Longrightarrow> \<exists>a b. s = cbox a b" "\<And>s. s \<in> f \<Longrightarrow> interior s \<subseteq> t"
+    and t: "closed t"
+  shows "interior (\<Union>f) \<subseteq> t"
+proof -
+  have [simp]: "s \<in> f \<Longrightarrow> closed s" for s
+    using f by auto
+  define E where "E = {s\<in>f. interior s = {}}"
+  then have "finite E" "E \<subseteq> {s\<in>f. interior s = {}}"
+    using \<open>finite f\<close> by auto
+  then have "interior (\<Union>f) = interior (\<Union>(f - E))"
+  proof (induction E rule: finite_subset_induct')
+    case (insert s f')
+    have "interior (\<Union>(f - insert s f') \<union> s) = interior (\<Union>(f - insert s f'))"
+      using insert.hyps \<open>finite f\<close> by (intro interior_closed_Un_empty_interior) auto
+    also have "\<Union>(f - insert s f') \<union> s = \<Union>(f - f')"
+      using insert.hyps by auto
+    finally show ?case
+      by (simp add: insert.IH)
+  qed simp
+  also have "\<dots> \<subseteq> \<Union>(f - E)"
+    by (rule interior_subset)
+  also have "\<dots> \<subseteq> t"
+  proof (rule Union_least)
+    fix s assume "s \<in> f - E"
+    with f[of s] obtain a b where s: "s \<in> f" "s = cbox a b" "box a b \<noteq> {}"
+      by (fastforce simp: E_def)
+    have "closure (interior s) \<subseteq> closure t"
+      by (intro closure_mono f \<open>s \<in> f\<close>)
+    with s \<open>closed t\<close> show "s \<subseteq> t"
+      by (simp add: closure_box)
+  qed
+  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
 
 subsection \<open>Bounds on intervals where they exist.\<close>
 
@@ -827,7 +694,7 @@
   fixes s1 s2 :: "'a::euclidean_space set"
   assumes "p1 division_of s1"
     and "p2 division_of s2"
-  shows "{k1 \<inter> k2 | k1 k2 .k1 \<in> p1 \<and> k2 \<in> p2 \<and> k1 \<inter> k2 \<noteq> {}} division_of (s1 \<inter> s2)"
+  shows "{k1 \<inter> k2 | k1 k2. k1 \<in> p1 \<and> k2 \<in> p2 \<and> k1 \<inter> k2 \<noteq> {}} division_of (s1 \<inter> s2)"
   (is "?A' division_of _")
 proof -
   let ?A = "{s. s \<in>  (\<lambda>(k1,k2). k1 \<inter> k2) ` (p1 \<times> p2) \<and> s \<noteq> {}}"