src/HOL/Analysis/Tagged_Division.thy
author nipkow
Sat Dec 29 15:43:53 2018 +0100 (6 months ago)
changeset 69529 4ab9657b3257
parent 69508 2a4c8a2a3f8e
child 69565 1daf07b65385
permissions -rw-r--r--
capitalize proper names in lemma names
     1 (*  Title:      HOL/Analysis/Tagged_Division.thy
     2     Author:     John Harrison
     3     Author:     Robert Himmelmann, TU Muenchen (Translation from HOL light); proofs reworked by LCP
     4 *)
     5 
     6 section%important \<open>Tagged divisions used for the Henstock-Kurzweil gauge integration\<close>
     7 (*FIXME move together with Henstock_Kurzweil_Integration.thy  *)
     8 theory Tagged_Division
     9   imports Connected
    10 begin
    11 
    12 term comm_monoid
    13 
    14 lemma sum_Sigma_product:
    15   assumes "finite S"
    16     and "\<And>i. i \<in> S \<Longrightarrow> finite (T i)"
    17   shows "(\<Sum>i\<in>S. sum (x i) (T i)) = (\<Sum>(i, j)\<in>Sigma S T. x i j)"
    18   using assms
    19 proof induct
    20   case empty
    21   then show ?case
    22     by simp
    23 next
    24   case (insert a S)
    25   show ?case
    26     by (simp add: insert.hyps(1) insert.prems sum.Sigma)
    27 qed
    28 
    29 lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
    30   scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff
    31   scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one
    32 
    33 
    34 subsection%unimportant \<open>Sundries\<close>
    35 (*FIXME restructure this entire section consists of single lemma *)
    36 
    37 text\<open>A transitive relation is well-founded if all initial segments are finite.\<close>
    38 lemma wf_finite_segments:
    39   assumes "irrefl r" and "trans r" and "\<And>x. finite {y. (y, x) \<in> r}"
    40   shows "wf (r)"
    41   apply (simp add: trans_wf_iff wf_iff_acyclic_if_finite converse_def assms)
    42   using acyclic_def assms irrefl_def trans_Restr by fastforce
    43 
    44 text\<open>For creating values between @{term u} and @{term v}.\<close>
    45 lemma scaling_mono:
    46   fixes u::"'a::linordered_field"
    47   assumes "u \<le> v" "0 \<le> r" "r \<le> s"
    48     shows "u + r * (v - u) / s \<le> v"
    49 proof -
    50   have "r/s \<le> 1" using assms
    51     using divide_le_eq_1 by fastforce
    52   then have "(r/s) * (v - u) \<le> 1 * (v - u)"
    53     by (meson diff_ge_0_iff_ge mult_right_mono \<open>u \<le> v\<close>)
    54   then show ?thesis
    55     by (simp add: field_simps)
    56 qed
    57 
    58 subsection%unimportant \<open>Some useful lemmas about intervals\<close>
    59 
    60 lemma interior_subset_union_intervals:
    61   assumes "i = cbox a b"
    62     and "j = cbox c d"
    63     and "interior j \<noteq> {}"
    64     and "i \<subseteq> j \<union> S"
    65     and "interior i \<inter> interior j = {}"
    66   shows "interior i \<subseteq> interior S"
    67 proof -
    68   have "box a b \<inter> cbox c d = {}"
    69      using Int_interval_mixed_eq_empty[of c d a b] assms
    70      unfolding interior_cbox by auto
    71   moreover
    72   have "box a b \<subseteq> cbox c d \<union> S"
    73     apply (rule order_trans,rule box_subset_cbox)
    74     using assms by auto
    75   ultimately
    76   show ?thesis
    77     unfolding assms interior_cbox
    78       by auto (metis IntI UnE empty_iff interior_maximal open_box subsetCE subsetI)
    79 qed
    80 
    81 lemma interior_Union_subset_cbox:
    82   assumes "finite f"
    83   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"
    84     and t: "closed t"
    85   shows "interior (\<Union>f) \<subseteq> t"
    86 proof -
    87   have [simp]: "s \<in> f \<Longrightarrow> closed s" for s
    88     using f by auto
    89   define E where "E = {s\<in>f. interior s = {}}"
    90   then have "finite E" "E \<subseteq> {s\<in>f. interior s = {}}"
    91     using \<open>finite f\<close> by auto
    92   then have "interior (\<Union>f) = interior (\<Union>(f - E))"
    93   proof (induction E rule: finite_subset_induct')
    94     case (insert s f')
    95     have "interior (\<Union>(f - insert s f') \<union> s) = interior (\<Union>(f - insert s f'))"
    96       using insert.hyps \<open>finite f\<close> by (intro interior_closed_Un_empty_interior) auto
    97     also have "\<Union>(f - insert s f') \<union> s = \<Union>(f - f')"
    98       using insert.hyps by auto
    99     finally show ?case
   100       by (simp add: insert.IH)
   101   qed simp
   102   also have "\<dots> \<subseteq> \<Union>(f - E)"
   103     by (rule interior_subset)
   104   also have "\<dots> \<subseteq> t"
   105   proof (rule Union_least)
   106     fix s assume "s \<in> f - E"
   107     with f[of s] obtain a b where s: "s \<in> f" "s = cbox a b" "box a b \<noteq> {}"
   108       by (fastforce simp: E_def)
   109     have "closure (interior s) \<subseteq> closure t"
   110       by (intro closure_mono f \<open>s \<in> f\<close>)
   111     with s \<open>closed t\<close> show "s \<subseteq> t"
   112       by simp
   113   qed
   114   finally show ?thesis .
   115 qed
   116 
   117 lemma Int_interior_Union_intervals:
   118     "\<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> 
   119     \<Longrightarrow> S \<inter> interior (\<Union>\<F>) = {}"
   120   using interior_Union_subset_cbox[of \<F> "UNIV - S"] by auto
   121 
   122 lemma interval_split:
   123   fixes a :: "'a::euclidean_space"
   124   assumes "k \<in> Basis"
   125   shows
   126     "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)"
   127     "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"
   128   using assms by (rule_tac set_eqI; auto simp: mem_box)+
   129 
   130 lemma interval_not_empty: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> cbox a b \<noteq> {}"
   131   by (simp add: box_ne_empty)
   132 
   133 subsection%important \<open>Bounds on intervals where they exist\<close>
   134 
   135 definition%important interval_upperbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
   136   where "interval_upperbound s = (\<Sum>i\<in>Basis. (SUP x\<in>s. x\<bullet>i) *\<^sub>R i)"
   137 
   138 definition%important interval_lowerbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
   139   where "interval_lowerbound s = (\<Sum>i\<in>Basis. (INF x\<in>s. x\<bullet>i) *\<^sub>R i)"
   140 
   141 lemma interval_upperbound[simp]:
   142   "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
   143     interval_upperbound (cbox a b) = (b::'a::euclidean_space)"
   144   unfolding interval_upperbound_def euclidean_representation_sum cbox_def
   145   by (safe intro!: cSup_eq) auto
   146 
   147 lemma interval_lowerbound[simp]:
   148   "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
   149     interval_lowerbound (cbox a b) = (a::'a::euclidean_space)"
   150   unfolding interval_lowerbound_def euclidean_representation_sum cbox_def
   151   by (safe intro!: cInf_eq) auto
   152 
   153 lemmas interval_bounds = interval_upperbound interval_lowerbound
   154 
   155 lemma%important
   156   fixes X::"real set"
   157   shows interval_upperbound_real[simp]: "interval_upperbound X = Sup X"
   158     and interval_lowerbound_real[simp]: "interval_lowerbound X = Inf X"
   159   by%unimportant (auto simp: interval_upperbound_def interval_lowerbound_def)
   160 
   161 lemma%important interval_bounds'[simp]:
   162   assumes "cbox a b \<noteq> {}"
   163   shows "interval_upperbound (cbox a b) = b"
   164     and "interval_lowerbound (cbox a b) = a"
   165   using%unimportant assms unfolding box_ne_empty by auto
   166 
   167 lemma%important interval_upperbound_Times:
   168   assumes "A \<noteq> {}" and "B \<noteq> {}"
   169   shows "interval_upperbound (A \<times> B) = (interval_upperbound A, interval_upperbound B)"
   170 proof%unimportant-
   171   from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
   172   have "(\<Sum>i\<in>Basis. (SUP x\<in>A \<times> B. x \<bullet> (i, 0)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (SUP x\<in>A. x \<bullet> i) *\<^sub>R i)"
   173       by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
   174   moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp
   175   have "(\<Sum>i\<in>Basis. (SUP x\<in>A \<times> B. x \<bullet> (0, i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (SUP x\<in>B. x \<bullet> i) *\<^sub>R i)"
   176       by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
   177   ultimately show ?thesis unfolding interval_upperbound_def
   178       by (subst sum_Basis_prod_eq) (auto simp add: sum_prod)
   179 qed
   180 
   181 lemma%important interval_lowerbound_Times:
   182   assumes "A \<noteq> {}" and "B \<noteq> {}"
   183   shows "interval_lowerbound (A \<times> B) = (interval_lowerbound A, interval_lowerbound B)"
   184 proof%unimportant-
   185   from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
   186   have "(\<Sum>i\<in>Basis. (INF x\<in>A \<times> B. x \<bullet> (i, 0)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (INF x\<in>A. x \<bullet> i) *\<^sub>R i)"
   187       by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
   188   moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp
   189   have "(\<Sum>i\<in>Basis. (INF x\<in>A \<times> B. x \<bullet> (0, i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (INF x\<in>B. x \<bullet> i) *\<^sub>R i)"
   190       by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
   191   ultimately show ?thesis unfolding interval_lowerbound_def
   192       by (subst sum_Basis_prod_eq) (auto simp add: sum_prod)
   193 qed
   194 
   195 subsection%important \<open>The notion of a gauge --- simply an open set containing the point\<close>
   196 
   197 definition%important "gauge \<gamma> \<longleftrightarrow> (\<forall>x. x \<in> \<gamma> x \<and> open (\<gamma> x))"
   198 
   199 lemma gaugeI:
   200   assumes "\<And>x. x \<in> \<gamma> x"
   201     and "\<And>x. open (\<gamma> x)"
   202   shows "gauge \<gamma>"
   203   using assms unfolding gauge_def by auto
   204 
   205 lemma gaugeD[dest]:
   206   assumes "gauge \<gamma>"
   207   shows "x \<in> \<gamma> x"
   208     and "open (\<gamma> x)"
   209   using assms unfolding gauge_def by auto
   210 
   211 lemma gauge_ball_dependent: "\<forall>x. 0 < e x \<Longrightarrow> gauge (\<lambda>x. ball x (e x))"
   212   unfolding gauge_def by auto
   213 
   214 lemma gauge_ball[intro]: "0 < e \<Longrightarrow> gauge (\<lambda>x. ball x e)"
   215   unfolding gauge_def by auto
   216 
   217 lemma gauge_trivial[intro!]: "gauge (\<lambda>x. ball x 1)"
   218   by (rule gauge_ball) auto
   219 
   220 lemma gauge_Int[intro]: "gauge \<gamma>1 \<Longrightarrow> gauge \<gamma>2 \<Longrightarrow> gauge (\<lambda>x. \<gamma>1 x \<inter> \<gamma>2 x)"
   221   unfolding gauge_def by auto
   222 
   223 lemma gauge_reflect:
   224   fixes \<gamma> :: "'a::euclidean_space \<Rightarrow> 'a set"
   225   shows "gauge \<gamma> \<Longrightarrow> gauge (\<lambda>x. uminus ` \<gamma> (- x))"
   226   using equation_minus_iff
   227   by (auto simp: gauge_def surj_def intro!: open_surjective_linear_image linear_uminus)
   228 
   229 lemma%important gauge_Inter:
   230   assumes "finite S"
   231     and "\<And>u. u\<in>S \<Longrightarrow> gauge (f u)"
   232   shows "gauge (\<lambda>x. \<Inter>{f u x | u. u \<in> S})"
   233 proof%unimportant -
   234   have *: "\<And>x. {f u x |u. u \<in> S} = (\<lambda>u. f u x) ` S"
   235     by auto
   236   show ?thesis
   237     unfolding gauge_def unfolding *
   238     using assms unfolding Ball_def Inter_iff mem_Collect_eq gauge_def by auto
   239 qed
   240 
   241 lemma%important gauge_existence_lemma:
   242   "(\<forall>x. \<exists>d :: real. p x \<longrightarrow> 0 < d \<and> q d x) \<longleftrightarrow> (\<forall>x. \<exists>d>0. p x \<longrightarrow> q d x)"
   243   by%unimportant (metis zero_less_one)
   244 
   245 subsection%unimportant \<open>Attempt a systematic general set of "offset" results for components\<close>
   246 (*FIXME Restructure *)
   247 lemma gauge_modify:
   248   assumes "(\<forall>S. open S \<longrightarrow> open {x. f(x) \<in> S})" "gauge d"
   249   shows "gauge (\<lambda>x. {y. f y \<in> d (f x)})"
   250   using assms unfolding gauge_def by force
   251 
   252 subsection%important \<open>Divisions\<close>
   253 
   254 definition%important division_of (infixl "division'_of" 40)
   255 where
   256   "s division_of i \<longleftrightarrow>
   257     finite s \<and>
   258     (\<forall>K\<in>s. K \<subseteq> i \<and> K \<noteq> {} \<and> (\<exists>a b. K = cbox a b)) \<and>
   259     (\<forall>K1\<in>s. \<forall>K2\<in>s. K1 \<noteq> K2 \<longrightarrow> interior(K1) \<inter> interior(K2) = {}) \<and>
   260     (\<Union>s = i)"
   261 
   262 lemma division_ofD[dest]:
   263   assumes "s division_of i"
   264   shows "finite s"
   265     and "\<And>K. K \<in> s \<Longrightarrow> K \<subseteq> i"
   266     and "\<And>K. K \<in> s \<Longrightarrow> K \<noteq> {}"
   267     and "\<And>K. K \<in> s \<Longrightarrow> \<exists>a b. K = cbox a b"
   268     and "\<And>K1 K2. K1 \<in> s \<Longrightarrow> K2 \<in> s \<Longrightarrow> K1 \<noteq> K2 \<Longrightarrow> interior(K1) \<inter> interior(K2) = {}"
   269     and "\<Union>s = i"
   270   using assms unfolding division_of_def by auto
   271 
   272 lemma division_ofI:
   273   assumes "finite s"
   274     and "\<And>K. K \<in> s \<Longrightarrow> K \<subseteq> i"
   275     and "\<And>K. K \<in> s \<Longrightarrow> K \<noteq> {}"
   276     and "\<And>K. K \<in> s \<Longrightarrow> \<exists>a b. K = cbox a b"
   277     and "\<And>K1 K2. K1 \<in> s \<Longrightarrow> K2 \<in> s \<Longrightarrow> K1 \<noteq> K2 \<Longrightarrow> interior K1 \<inter> interior K2 = {}"
   278     and "\<Union>s = i"
   279   shows "s division_of i"
   280   using assms unfolding division_of_def by auto
   281 
   282 lemma division_of_finite: "s division_of i \<Longrightarrow> finite s"
   283   by auto
   284 
   285 lemma division_of_self[intro]: "cbox a b \<noteq> {} \<Longrightarrow> {cbox a b} division_of (cbox a b)"
   286   unfolding division_of_def by auto
   287 
   288 lemma division_of_trivial[simp]: "s division_of {} \<longleftrightarrow> s = {}"
   289   unfolding division_of_def by auto
   290 
   291 lemma division_of_sing[simp]:
   292   "s division_of cbox a (a::'a::euclidean_space) \<longleftrightarrow> s = {cbox a a}"
   293   (is "?l = ?r")
   294 proof
   295   assume ?r
   296   moreover
   297   { fix K
   298     assume "s = {{a}}" "K\<in>s"
   299     then have "\<exists>x y. K = cbox x y"
   300       apply (rule_tac x=a in exI)+
   301       apply force
   302       done
   303   }
   304   ultimately show ?l
   305     unfolding division_of_def cbox_sing by auto
   306 next
   307   assume ?l
   308   have "x = {a}" if  "x \<in> s" for x
   309     by (metis \<open>s division_of cbox a a\<close> cbox_sing division_ofD(2) division_ofD(3) subset_singletonD that)
   310   moreover have "s \<noteq> {}"
   311     using \<open>s division_of cbox a a\<close> by auto
   312   ultimately show ?r
   313     unfolding cbox_sing by auto
   314 qed
   315 
   316 lemma elementary_empty: obtains p where "p division_of {}"
   317   unfolding division_of_trivial by auto
   318 
   319 lemma elementary_interval: obtains p where "p division_of (cbox a b)"
   320   by (metis division_of_trivial division_of_self)
   321 
   322 lemma division_contains: "s division_of i \<Longrightarrow> \<forall>x\<in>i. \<exists>k\<in>s. x \<in> k"
   323   unfolding division_of_def by auto
   324 
   325 lemma forall_in_division:
   326   "d division_of i \<Longrightarrow> (\<forall>x\<in>d. P x) \<longleftrightarrow> (\<forall>a b. cbox a b \<in> d \<longrightarrow> P (cbox a b))"
   327   unfolding division_of_def by fastforce
   328 
   329 lemma cbox_division_memE:
   330   assumes \<D>: "K \<in> \<D>" "\<D> division_of S"
   331   obtains a b where "K = cbox a b" "K \<noteq> {}" "K \<subseteq> S"
   332   using assms unfolding division_of_def by metis
   333 
   334 lemma division_of_subset:
   335   assumes "p division_of (\<Union>p)"
   336     and "q \<subseteq> p"
   337   shows "q division_of (\<Union>q)"
   338 proof (rule division_ofI)
   339   note * = division_ofD[OF assms(1)]
   340   show "finite q"
   341     using "*"(1) assms(2) infinite_super by auto
   342   {
   343     fix k
   344     assume "k \<in> q"
   345     then have kp: "k \<in> p"
   346       using assms(2) by auto
   347     show "k \<subseteq> \<Union>q"
   348       using \<open>k \<in> q\<close> by auto
   349     show "\<exists>a b. k = cbox a b"
   350       using *(4)[OF kp] by auto
   351     show "k \<noteq> {}"
   352       using *(3)[OF kp] by auto
   353   }
   354   fix k1 k2
   355   assume "k1 \<in> q" "k2 \<in> q" "k1 \<noteq> k2"
   356   then have **: "k1 \<in> p" "k2 \<in> p" "k1 \<noteq> k2"
   357     using assms(2) by auto
   358   show "interior k1 \<inter> interior k2 = {}"
   359     using *(5)[OF **] by auto
   360 qed auto
   361 
   362 lemma division_of_union_self[intro]: "p division_of s \<Longrightarrow> p division_of (\<Union>p)"
   363   unfolding division_of_def by auto
   364 
   365 lemma division_inter:
   366   fixes s1 s2 :: "'a::euclidean_space set"
   367   assumes "p1 division_of s1"
   368     and "p2 division_of s2"
   369   shows "{k1 \<inter> k2 | k1 k2. k1 \<in> p1 \<and> k2 \<in> p2 \<and> k1 \<inter> k2 \<noteq> {}} division_of (s1 \<inter> s2)"
   370   (is "?A' division_of _")
   371 proof -
   372   let ?A = "{s. s \<in>  (\<lambda>(k1,k2). k1 \<inter> k2) ` (p1 \<times> p2) \<and> s \<noteq> {}}"
   373   have *: "?A' = ?A" by auto
   374   show ?thesis
   375     unfolding *
   376   proof (rule division_ofI)
   377     have "?A \<subseteq> (\<lambda>(x, y). x \<inter> y) ` (p1 \<times> p2)"
   378       by auto
   379     moreover have "finite (p1 \<times> p2)"
   380       using assms unfolding division_of_def by auto
   381     ultimately show "finite ?A" by auto
   382     have *: "\<And>s. \<Union>{x\<in>s. x \<noteq> {}} = \<Union>s"
   383       by auto
   384     show "\<Union>?A = s1 \<inter> s2"
   385       unfolding * 
   386       using division_ofD(6)[OF assms(1)] and division_ofD(6)[OF assms(2)] by auto
   387     {
   388       fix k
   389       assume "k \<in> ?A"
   390       then obtain k1 k2 where k: "k = k1 \<inter> k2" "k1 \<in> p1" "k2 \<in> p2" "k \<noteq> {}"
   391         by auto
   392       then show "k \<noteq> {}"
   393         by auto
   394       show "k \<subseteq> s1 \<inter> s2"
   395         using division_ofD(2)[OF assms(1) k(2)] and division_ofD(2)[OF assms(2) k(3)]
   396         unfolding k by auto
   397       obtain a1 b1 where k1: "k1 = cbox a1 b1"
   398         using division_ofD(4)[OF assms(1) k(2)] by blast
   399       obtain a2 b2 where k2: "k2 = cbox a2 b2"
   400         using division_ofD(4)[OF assms(2) k(3)] by blast
   401       show "\<exists>a b. k = cbox a b"
   402         unfolding k k1 k2 unfolding Int_interval by auto
   403     }
   404     fix k1 k2
   405     assume "k1 \<in> ?A"
   406     then obtain x1 y1 where k1: "k1 = x1 \<inter> y1" "x1 \<in> p1" "y1 \<in> p2" "k1 \<noteq> {}"
   407       by auto
   408     assume "k2 \<in> ?A"
   409     then obtain x2 y2 where k2: "k2 = x2 \<inter> y2" "x2 \<in> p1" "y2 \<in> p2" "k2 \<noteq> {}"
   410       by auto
   411     assume "k1 \<noteq> k2"
   412     then have th: "x1 \<noteq> x2 \<or> y1 \<noteq> y2"
   413       unfolding k1 k2 by auto
   414     have *: "interior x1 \<inter> interior x2 = {} \<or> interior y1 \<inter> interior y2 = {} \<Longrightarrow>
   415       interior (x1 \<inter> y1) \<subseteq> interior x1 \<Longrightarrow> interior (x1 \<inter> y1) \<subseteq> interior y1 \<Longrightarrow>
   416       interior (x2 \<inter> y2) \<subseteq> interior x2 \<Longrightarrow> interior (x2 \<inter> y2) \<subseteq> interior y2 \<Longrightarrow>
   417       interior (x1 \<inter> y1) \<inter> interior (x2 \<inter> y2) = {}" by auto
   418     show "interior k1 \<inter> interior k2 = {}"
   419       unfolding k1 k2
   420       apply (rule *)
   421       using assms division_ofD(5) k1 k2(2) k2(3) th apply auto
   422       done
   423   qed
   424 qed
   425 
   426 lemma division_inter_1:
   427   assumes "d division_of i"
   428     and "cbox a (b::'a::euclidean_space) \<subseteq> i"
   429   shows "{cbox a b \<inter> k | k. k \<in> d \<and> cbox a b \<inter> k \<noteq> {}} division_of (cbox a b)"
   430 proof (cases "cbox a b = {}")
   431   case True
   432   show ?thesis
   433     unfolding True and division_of_trivial by auto
   434 next
   435   case False
   436   have *: "cbox a b \<inter> i = cbox a b" using assms(2) by auto
   437   show ?thesis
   438     using division_inter[OF division_of_self[OF False] assms(1)]
   439     unfolding * by auto
   440 qed
   441 
   442 lemma elementary_Int:
   443   fixes s t :: "'a::euclidean_space set"
   444   assumes "p1 division_of s"
   445     and "p2 division_of t"
   446   shows "\<exists>p. p division_of (s \<inter> t)"
   447 using assms division_inter by blast
   448 
   449 lemma elementary_Inter:
   450   assumes "finite f"
   451     and "f \<noteq> {}"
   452     and "\<forall>s\<in>f. \<exists>p. p division_of (s::('a::euclidean_space) set)"
   453   shows "\<exists>p. p division_of (\<Inter>f)"
   454   using assms
   455 proof (induct f rule: finite_induct)
   456   case (insert x f)
   457   show ?case
   458   proof (cases "f = {}")
   459     case True
   460     then show ?thesis
   461       unfolding True using insert by auto
   462   next
   463     case False
   464     obtain p where "p division_of \<Inter>f"
   465       using insert(3)[OF False insert(5)[unfolded ball_simps,THEN conjunct2]] ..
   466     moreover obtain px where "px division_of x"
   467       using insert(5)[rule_format,OF insertI1] ..
   468     ultimately show ?thesis
   469       by (simp add: elementary_Int Inter_insert)
   470   qed
   471 qed auto
   472 
   473 lemma division_disjoint_union:
   474   assumes "p1 division_of s1"
   475     and "p2 division_of s2"
   476     and "interior s1 \<inter> interior s2 = {}"
   477   shows "(p1 \<union> p2) division_of (s1 \<union> s2)"
   478 proof (rule division_ofI)
   479   note d1 = division_ofD[OF assms(1)]
   480   note d2 = division_ofD[OF assms(2)]
   481   show "finite (p1 \<union> p2)"
   482     using d1(1) d2(1) by auto
   483   show "\<Union>(p1 \<union> p2) = s1 \<union> s2"
   484     using d1(6) d2(6) by auto
   485   {
   486     fix k1 k2
   487     assume as: "k1 \<in> p1 \<union> p2" "k2 \<in> p1 \<union> p2" "k1 \<noteq> k2"
   488     moreover
   489     let ?g="interior k1 \<inter> interior k2 = {}"
   490     {
   491       assume as: "k1\<in>p1" "k2\<in>p2"
   492       have ?g
   493         using interior_mono[OF d1(2)[OF as(1)]] interior_mono[OF d2(2)[OF as(2)]]
   494         using assms(3) by blast
   495     }
   496     moreover
   497     {
   498       assume as: "k1\<in>p2" "k2\<in>p1"
   499       have ?g
   500         using interior_mono[OF d1(2)[OF as(2)]] interior_mono[OF d2(2)[OF as(1)]]
   501         using assms(3) by blast
   502     }
   503     ultimately show ?g
   504       using d1(5)[OF _ _ as(3)] and d2(5)[OF _ _ as(3)] by auto
   505   }
   506   fix k
   507   assume k: "k \<in> p1 \<union> p2"
   508   show "k \<subseteq> s1 \<union> s2"
   509     using k d1(2) d2(2) by auto
   510   show "k \<noteq> {}"
   511     using k d1(3) d2(3) by auto
   512   show "\<exists>a b. k = cbox a b"
   513     using k d1(4) d2(4) by auto
   514 qed
   515 
   516 lemma partial_division_extend_1:
   517   fixes a b c d :: "'a::euclidean_space"
   518   assumes incl: "cbox c d \<subseteq> cbox a b"
   519     and nonempty: "cbox c d \<noteq> {}"
   520   obtains p where "p division_of (cbox a b)" "cbox c d \<in> p"
   521 proof
   522   let ?B = "\<lambda>f::'a\<Rightarrow>'a \<times> 'a.
   523     cbox (\<Sum>i\<in>Basis. (fst (f i) \<bullet> i) *\<^sub>R i) (\<Sum>i\<in>Basis. (snd (f i) \<bullet> i) *\<^sub>R i)"
   524   define p where "p = ?B ` (Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)})"
   525 
   526   show "cbox c d \<in> p"
   527     unfolding p_def
   528     by (auto simp add: box_eq_empty cbox_def intro!: image_eqI[where x="\<lambda>(i::'a)\<in>Basis. (c, d)"])
   529   have ord: "a \<bullet> i \<le> c \<bullet> i" "c \<bullet> i \<le> d \<bullet> i" "d \<bullet> i \<le> b \<bullet> i" if "i \<in> Basis" for i
   530     using incl nonempty that
   531     unfolding box_eq_empty subset_box by (auto simp: not_le)
   532 
   533   show "p division_of (cbox a b)"
   534   proof (rule division_ofI)
   535     show "finite p"
   536       unfolding p_def by (auto intro!: finite_PiE)
   537     {
   538       fix k
   539       assume "k \<in> p"
   540       then obtain f where f: "f \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}" and k: "k = ?B f"
   541         by (auto simp: p_def)
   542       then show "\<exists>a b. k = cbox a b"
   543         by auto
   544       have "k \<subseteq> cbox a b \<and> k \<noteq> {}"
   545       proof (simp add: k box_eq_empty subset_box not_less, safe)
   546         fix i :: 'a
   547         assume i: "i \<in> Basis"
   548         with f have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
   549           by (auto simp: PiE_iff)
   550         with i ord[of i]
   551         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"
   552           by auto
   553       qed
   554       then show "k \<noteq> {}" "k \<subseteq> cbox a b"
   555         by auto
   556       {
   557         fix l
   558         assume "l \<in> p"
   559         then obtain g where g: "g \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}" and l: "l = ?B g"
   560           by (auto simp: p_def)
   561         assume "l \<noteq> k"
   562         have "\<exists>i\<in>Basis. f i \<noteq> g i"
   563         proof (rule ccontr)
   564           assume "\<not> ?thesis"
   565           with f g have "f = g"
   566             by (auto simp: PiE_iff extensional_def fun_eq_iff)
   567           with \<open>l \<noteq> k\<close> show False
   568             by (simp add: l k)
   569         qed
   570         then obtain i where *: "i \<in> Basis" "f i \<noteq> g i" ..
   571         then have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
   572                   "g i = (a, c) \<or> g i = (c, d) \<or> g i = (d, b)"
   573           using f g by (auto simp: PiE_iff)
   574         with * ord[of i] show "interior l \<inter> interior k = {}"
   575           by (auto simp add: l k disjoint_interval intro!: bexI[of _ i])
   576       }
   577       note \<open>k \<subseteq> cbox a b\<close>
   578     }
   579     moreover
   580     {
   581       fix x assume x: "x \<in> cbox a b"
   582       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)}"
   583       proof
   584         fix i :: 'a
   585         assume "i \<in> Basis"
   586         with x ord[of i]
   587         have "(a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> c \<bullet> i) \<or> (c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i) \<or>
   588             (d \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i)"
   589           by (auto simp: cbox_def)
   590         then show "\<exists>l. x \<bullet> i \<in> {fst l \<bullet> i .. snd l \<bullet> i} \<and> l \<in> {(a, c), (c, d), (d, b)}"
   591           by auto
   592       qed
   593       then obtain f where
   594         f: "\<forall>i\<in>Basis. x \<bullet> i \<in> {fst (f i) \<bullet> i..snd (f i) \<bullet> i} \<and> f i \<in> {(a, c), (c, d), (d, b)}"
   595         unfolding bchoice_iff ..
   596       moreover from f have "restrict f Basis \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}"
   597         by auto
   598       moreover from f have "x \<in> ?B (restrict f Basis)"
   599         by (auto simp: mem_box)
   600       ultimately have "\<exists>k\<in>p. x \<in> k"
   601         unfolding p_def by blast
   602     }
   603     ultimately show "\<Union>p = cbox a b"
   604       by auto
   605   qed
   606 qed
   607 
   608 proposition%important partial_division_extend_interval:
   609   assumes "p division_of (\<Union>p)" "(\<Union>p) \<subseteq> cbox a b"
   610   obtains q where "p \<subseteq> q" "q division_of cbox a (b::'a::euclidean_space)"
   611 proof%unimportant (cases "p = {}")
   612   case True
   613   obtain q where "q division_of (cbox a b)"
   614     by (rule elementary_interval)
   615   then show ?thesis
   616     using True that by blast
   617 next
   618   case False
   619   note p = division_ofD[OF assms(1)]
   620   have div_cbox: "\<forall>k\<in>p. \<exists>q. q division_of cbox a b \<and> k \<in> q"
   621   proof
   622     fix k
   623     assume kp: "k \<in> p"
   624     obtain c d where k: "k = cbox c d"
   625       using p(4)[OF kp] by blast
   626     have *: "cbox c d \<subseteq> cbox a b" "cbox c d \<noteq> {}"
   627       using p(2,3)[OF kp, unfolded k] using assms(2)
   628       by (blast intro: order.trans)+
   629     obtain q where "q division_of cbox a b" "cbox c d \<in> q"
   630       by (rule partial_division_extend_1[OF *])
   631     then show "\<exists>q. q division_of cbox a b \<and> k \<in> q"
   632       unfolding k by auto
   633   qed
   634   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"
   635     using bchoice[OF div_cbox] by blast
   636   have "q x division_of \<Union>q x" if x: "x \<in> p" for x
   637     apply (rule division_ofI)
   638     using division_ofD[OF q(1)[OF x]] by auto
   639   then have di: "\<And>x. x \<in> p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x - {x})"
   640     by (meson Diff_subset division_of_subset)
   641   have "\<exists>d. d division_of \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p)"
   642     apply (rule elementary_Inter [OF finite_imageI[OF p(1)]])
   643     apply (auto dest: di simp: False elementary_Inter [OF finite_imageI[OF p(1)]])
   644     done
   645   then obtain d where d: "d division_of \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p)" ..
   646   have "d \<union> p division_of cbox a b"
   647   proof -
   648     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
   649     have cbox_eq: "cbox a b = \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p) \<union> \<Union>p"
   650     proof (rule te[OF False], clarify)
   651       fix i
   652       assume i: "i \<in> p"
   653       show "\<Union>(q i - {i}) \<union> i = cbox a b"
   654         using division_ofD(6)[OF q(1)[OF i]] using q(2)[OF i] by auto
   655     qed
   656     { fix K
   657       assume K: "K \<in> p"
   658       note qk=division_ofD[OF q(1)[OF K]]
   659       have *: "\<And>u T S. T \<inter> S = {} \<Longrightarrow> u \<subseteq> S \<Longrightarrow> u \<inter> T = {}"
   660         by auto
   661       have "interior (\<Inter>i\<in>p. \<Union>(q i - {i})) \<inter> interior K = {}"
   662       proof (rule *[OF Int_interior_Union_intervals])
   663         show "\<And>T. T\<in>q K - {K} \<Longrightarrow> interior K \<inter> interior T = {}"
   664           using qk(5) using q(2)[OF K] by auto
   665         show "interior (\<Inter>i\<in>p. \<Union>(q i - {i})) \<subseteq> interior (\<Union>(q K - {K}))"
   666           apply (rule interior_mono)+
   667           using K by auto
   668       qed (use qk in auto)} note [simp] = this
   669     show "d \<union> p division_of (cbox a b)"
   670       unfolding cbox_eq
   671       apply (rule division_disjoint_union[OF d assms(1)])
   672       apply (rule Int_interior_Union_intervals)
   673       apply (rule p open_interior ballI)+
   674       apply simp_all
   675       done
   676   qed
   677   then show ?thesis
   678     by (meson Un_upper2 that)
   679 qed
   680 
   681 lemma elementary_bounded[dest]:
   682   fixes S :: "'a::euclidean_space set"
   683   shows "p division_of S \<Longrightarrow> bounded S"
   684   unfolding division_of_def by (metis bounded_Union bounded_cbox)
   685 
   686 lemma elementary_subset_cbox:
   687   "p division_of S \<Longrightarrow> \<exists>a b. S \<subseteq> cbox a (b::'a::euclidean_space)"
   688   by (meson bounded_subset_cbox_symmetric elementary_bounded)
   689 
   690 lemma%important division_union_intervals_exists:
   691   fixes a b :: "'a::euclidean_space"
   692   assumes "cbox a b \<noteq> {}"
   693   obtains p where "(insert (cbox a b) p) division_of (cbox a b \<union> cbox c d)"
   694 proof%unimportant (cases "cbox c d = {}")
   695   case True
   696   with assms that show ?thesis by force
   697 next
   698   case False
   699   show ?thesis
   700   proof (cases "cbox a b \<inter> cbox c d = {}")
   701     case True
   702     then show ?thesis
   703       by (metis that False assms division_disjoint_union division_of_self insert_is_Un interior_Int interior_empty)
   704   next
   705     case False
   706     obtain u v where uv: "cbox a b \<inter> cbox c d = cbox u v"
   707       unfolding Int_interval by auto
   708     have uv_sub: "cbox u v \<subseteq> cbox c d" using uv by auto
   709     obtain p where pd: "p division_of cbox c d" and "cbox u v \<in> p"
   710       by (rule partial_division_extend_1[OF uv_sub False[unfolded uv]])
   711     note p = this division_ofD[OF pd]
   712     have "interior (cbox a b \<inter> \<Union>(p - {cbox u v})) = interior(cbox u v \<inter> \<Union>(p - {cbox u v}))"
   713       apply (rule arg_cong[of _ _ interior])
   714       using p(8) uv by auto
   715     also have "\<dots> = {}"
   716       unfolding interior_Int
   717       apply (rule Int_interior_Union_intervals)
   718       using p(6) p(7)[OF p(2)] \<open>finite p\<close>
   719       apply auto
   720       done
   721     finally have [simp]: "interior (cbox a b) \<inter> interior (\<Union>(p - {cbox u v})) = {}" by simp
   722     have cbe: "cbox a b \<union> cbox c d = cbox a b \<union> \<Union>(p - {cbox u v})"
   723       using p(8) unfolding uv[symmetric] by auto
   724     have "insert (cbox a b) (p - {cbox u v}) division_of cbox a b \<union> \<Union>(p - {cbox u v})"
   725     proof -
   726       have "{cbox a b} division_of cbox a b"
   727         by (simp add: assms division_of_self)
   728       then show "insert (cbox a b) (p - {cbox u v}) division_of cbox a b \<union> \<Union>(p - {cbox u v})"
   729         by (metis (no_types) Diff_subset \<open>interior (cbox a b) \<inter> interior (\<Union>(p - {cbox u v})) = {}\<close> division_disjoint_union division_of_subset insert_is_Un p(1) p(8))
   730     qed
   731     with that[of "p - {cbox u v}"] show ?thesis by (simp add: cbe)
   732   qed
   733 qed
   734 
   735 lemma division_of_Union:
   736   assumes "finite f"
   737     and "\<And>p. p \<in> f \<Longrightarrow> p division_of (\<Union>p)"
   738     and "\<And>k1 k2. k1 \<in> \<Union>f \<Longrightarrow> k2 \<in> \<Union>f \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior k1 \<inter> interior k2 = {}"
   739   shows "\<Union>f division_of \<Union>\<Union>f"
   740   using assms  by (auto intro!: division_ofI)
   741 
   742 lemma%important elementary_union_interval:
   743   fixes a b :: "'a::euclidean_space"
   744   assumes "p division_of \<Union>p"
   745   obtains q where "q division_of (cbox a b \<union> \<Union>p)"
   746 proof%unimportant (cases "p = {} \<or> cbox a b = {}")
   747   case True
   748   obtain p where "p division_of (cbox a b)"
   749     by (rule elementary_interval)
   750   then show thesis
   751     using True assms that by auto
   752 next
   753   case False
   754   then have "p \<noteq> {}" "cbox a b \<noteq> {}"
   755     by auto
   756   note pdiv = division_ofD[OF assms]
   757   show ?thesis
   758   proof (cases "interior (cbox a b) = {}")
   759     case True
   760     show ?thesis
   761       apply (rule that [of "insert (cbox a b) p", OF division_ofI])
   762       using pdiv(1-4) True False apply auto
   763        apply (metis IntI equals0D pdiv(5))
   764       by (metis disjoint_iff_not_equal pdiv(5))
   765   next
   766     case False  
   767     have "\<forall>K\<in>p. \<exists>q. (insert (cbox a b) q) division_of (cbox a b \<union> K)"
   768     proof
   769       fix K
   770       assume kp: "K \<in> p"
   771       from pdiv(4)[OF kp] obtain c d where "K = cbox c d" by blast
   772       then show "\<exists>q. (insert (cbox a b) q) division_of (cbox a b \<union> K)"
   773         by (meson \<open>cbox a b \<noteq> {}\<close> division_union_intervals_exists)
   774     qed
   775     from bchoice[OF this] obtain q where "\<forall>x\<in>p. insert (cbox a b) (q x) division_of (cbox a b) \<union> x" ..
   776     note q = division_ofD[OF this[rule_format]]
   777     let ?D = "\<Union>{insert (cbox a b) (q K) | K. K \<in> p}"
   778     show thesis
   779     proof (rule that[OF division_ofI])
   780       have *: "{insert (cbox a b) (q K) |K. K \<in> p} = (\<lambda>K. insert (cbox a b) (q K)) ` p"
   781         by auto
   782       show "finite ?D"
   783         using "*" pdiv(1) q(1) by auto
   784       have "\<Union>?D = (\<Union>x\<in>p. \<Union>insert (cbox a b) (q x))"
   785         by auto
   786       also have "... = \<Union>{cbox a b \<union> t |t. t \<in> p}"
   787         using q(6) by auto
   788       also have "... = cbox a b \<union> \<Union>p"
   789         using \<open>p \<noteq> {}\<close> by auto
   790       finally show "\<Union>?D = cbox a b \<union> \<Union>p" .
   791       show "K \<subseteq> cbox a b \<union> \<Union>p" "K \<noteq> {}" if "K \<in> ?D" for K
   792         using q that by blast+
   793       show "\<exists>a b. K = cbox a b" if "K \<in> ?D" for K
   794         using q(4) that by auto
   795     next
   796       fix K' K
   797       assume K: "K \<in> ?D" and K': "K' \<in> ?D" "K \<noteq> K'"
   798       obtain x where x: "K \<in> insert (cbox a b) (q x)" "x\<in>p"
   799         using K by auto
   800       obtain x' where x': "K'\<in>insert (cbox a b) (q x')" "x'\<in>p"
   801         using K' by auto
   802       show "interior K \<inter> interior K' = {}"
   803       proof (cases "x = x' \<or> K  = cbox a b \<or> K' = cbox a b")
   804         case True
   805         then show ?thesis
   806           using True K' q(5) x' x by auto
   807       next
   808         case False
   809         then have as': "K \<noteq> cbox a b" "K' \<noteq> cbox a b"
   810           by auto
   811         obtain c d where K: "K = cbox c d"
   812           using q(4) x by blast
   813         have "interior K \<inter> interior (cbox a b) = {}"
   814           using as' K'(2) q(5) x by blast
   815         then have "interior K \<subseteq> interior x"
   816           by (metis \<open>interior (cbox a b) \<noteq> {}\<close> K q(2) x interior_subset_union_intervals)
   817         moreover
   818         obtain c d where c_d: "K' = cbox c d"
   819           using q(4)[OF x'(2,1)] by blast
   820         have "interior K' \<inter> interior (cbox a b) = {}"
   821           using as'(2) q(5) x' by blast
   822         then have "interior K' \<subseteq> interior x'"
   823           by (metis \<open>interior (cbox a b) \<noteq> {}\<close> c_d interior_subset_union_intervals q(2) x'(1) x'(2))
   824         moreover have "interior x \<inter> interior x' = {}"
   825           by (meson False assms division_ofD(5) x'(2) x(2))
   826         ultimately show ?thesis
   827           using \<open>interior K \<subseteq> interior x\<close> \<open>interior K' \<subseteq> interior x'\<close> by auto
   828       qed
   829     qed
   830   qed
   831 qed
   832 
   833 
   834 
   835 lemma elementary_unions_intervals:
   836   assumes fin: "finite f"
   837     and "\<And>s. s \<in> f \<Longrightarrow> \<exists>a b. s = cbox a (b::'a::euclidean_space)"
   838   obtains p where "p division_of (\<Union>f)"
   839 proof -
   840   have "\<exists>p. p division_of (\<Union>f)"
   841   proof (induct_tac f rule:finite_subset_induct)
   842     show "\<exists>p. p division_of \<Union>{}" using elementary_empty by auto
   843   next
   844     fix x F
   845     assume as: "finite F" "x \<notin> F" "\<exists>p. p division_of \<Union>F" "x\<in>f"
   846     from this(3) obtain p where p: "p division_of \<Union>F" ..
   847     from assms(2)[OF as(4)] obtain a b where x: "x = cbox a b" by blast
   848     have *: "\<Union>F = \<Union>p"
   849       using division_ofD[OF p] by auto
   850     show "\<exists>p. p division_of \<Union>insert x F"
   851       using elementary_union_interval[OF p[unfolded *], of a b]
   852       unfolding Union_insert x * by metis
   853   qed (insert assms, auto)
   854   then show ?thesis
   855     using that by auto
   856 qed
   857 
   858 lemma%important elementary_union:
   859   fixes S T :: "'a::euclidean_space set"
   860   assumes "ps division_of S" "pt division_of T"
   861   obtains p where "p division_of (S \<union> T)"
   862 proof%unimportant -
   863   have *: "S \<union> T = \<Union>ps \<union> \<Union>pt"
   864     using assms unfolding division_of_def by auto
   865   show ?thesis
   866     apply (rule elementary_unions_intervals[of "ps \<union> pt"])
   867     using assms apply auto
   868     by (simp add: * that)
   869 qed
   870 
   871 lemma%important partial_division_extend:
   872   fixes T :: "'a::euclidean_space set"
   873   assumes "p division_of S"
   874     and "q division_of T"
   875     and "S \<subseteq> T"
   876   obtains r where "p \<subseteq> r" and "r division_of T"
   877 proof%unimportant -
   878   note divp = division_ofD[OF assms(1)] and divq = division_ofD[OF assms(2)]
   879   obtain a b where ab: "T \<subseteq> cbox a b"
   880     using elementary_subset_cbox[OF assms(2)] by auto
   881   obtain r1 where "p \<subseteq> r1" "r1 division_of (cbox a b)"
   882     using assms
   883     by (metis ab dual_order.trans partial_division_extend_interval divp(6))
   884   note r1 = this division_ofD[OF this(2)]
   885   obtain p' where "p' division_of \<Union>(r1 - p)"
   886     apply (rule elementary_unions_intervals[of "r1 - p"])
   887     using r1(3,6)
   888       apply auto
   889     done
   890   then obtain r2 where r2: "r2 division_of (\<Union>(r1 - p)) \<inter> (\<Union>q)"
   891     by (metis assms(2) divq(6) elementary_Int)
   892   {
   893     fix x
   894     assume x: "x \<in> T" "x \<notin> S"
   895     then obtain R where r: "R \<in> r1" "x \<in> R"
   896       unfolding r1 using ab
   897       by (meson division_contains r1(2) subsetCE)
   898     moreover have "R \<notin> p"
   899     proof
   900       assume "R \<in> p"
   901       then have "x \<in> S" using divp(2) r by auto
   902       then show False using x by auto
   903     qed
   904     ultimately have "x\<in>\<Union>(r1 - p)" by auto
   905   }
   906   then have Teq: "T = \<Union>p \<union> (\<Union>(r1 - p) \<inter> \<Union>q)"
   907     unfolding divp divq using assms(3) by auto
   908   have "interior S \<inter> interior (\<Union>(r1-p)) = {}"
   909   proof (rule Int_interior_Union_intervals)
   910     have *: "\<And>S. (\<And>x. x \<in> S \<Longrightarrow> False) \<Longrightarrow> S = {}"
   911       by auto
   912     show "interior S \<inter> interior m = {}" if "m \<in> r1 - p" for m 
   913     proof -
   914       have "interior m \<inter> interior (\<Union>p) = {}"
   915       proof (rule Int_interior_Union_intervals)
   916         show "\<And>T. T\<in>p \<Longrightarrow> interior m \<inter> interior T = {}"
   917           by (metis DiffD1 DiffD2 that r1(1) r1(7) set_rev_mp)
   918       qed (use divp in auto)
   919       then show "interior S \<inter> interior m = {}"
   920         unfolding divp by auto
   921     qed 
   922   qed (use r1 in auto)
   923   then have "interior S \<inter> interior (\<Union>(r1-p) \<inter> (\<Union>q)) = {}"
   924     using interior_subset by auto
   925   then have div: "p \<union> r2 division_of \<Union>p \<union> \<Union>(r1 - p) \<inter> \<Union>q"
   926     by (simp add: assms(1) division_disjoint_union divp(6) r2)
   927   show ?thesis
   928     apply (rule that[of "p \<union> r2"])
   929      apply (auto simp: div Teq)
   930     done
   931 qed
   932 
   933 
   934 lemma%important division_split:
   935   fixes a :: "'a::euclidean_space"
   936   assumes "p division_of (cbox a b)"
   937     and k: "k\<in>Basis"
   938   shows "{l \<inter> {x. x\<bullet>k \<le> c} | l. l \<in> p \<and> l \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}} division_of(cbox a b \<inter> {x. x\<bullet>k \<le> c})"
   939       (is "?p1 division_of ?I1")
   940     and "{l \<inter> {x. x\<bullet>k \<ge> c} | l. l \<in> p \<and> l \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}} division_of (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
   941       (is "?p2 division_of ?I2")
   942 proof%unimportant (rule_tac[!] division_ofI)
   943   note p = division_ofD[OF assms(1)]
   944   show "finite ?p1" "finite ?p2"
   945     using p(1) by auto
   946   show "\<Union>?p1 = ?I1" "\<Union>?p2 = ?I2"
   947     unfolding p(6)[symmetric] by auto
   948   {
   949     fix K
   950     assume "K \<in> ?p1"
   951     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> {}"
   952       by blast
   953     obtain u v where uv: "l = cbox u v"
   954       using assms(1) l(2) by blast
   955     show "K \<subseteq> ?I1"
   956       using l p(2) uv by force
   957     show  "K \<noteq> {}"
   958       by (simp add: l)
   959     show  "\<exists>a b. K = cbox a b"
   960       apply (simp add: l uv p(2-3)[OF l(2)])
   961       apply (subst interval_split[OF k])
   962       apply (auto intro: order.trans)
   963       done
   964     fix K'
   965     assume "K' \<in> ?p1"
   966     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> {}"
   967       by blast
   968     assume "K \<noteq> K'"
   969     then show "interior K \<inter> interior K' = {}"
   970       unfolding l l' using p(5)[OF l(2) l'(2)] by auto
   971   }
   972   {
   973     fix K
   974     assume "K \<in> ?p2"
   975     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> {}"
   976       by blast
   977     obtain u v where uv: "l = cbox u v"
   978       using l(2) p(4) by blast
   979     show "K \<subseteq> ?I2"
   980       using l p(2) uv by force
   981     show  "K \<noteq> {}"
   982       by (simp add: l)
   983     show  "\<exists>a b. K = cbox a b"
   984       apply (simp add: l uv p(2-3)[OF l(2)])
   985       apply (subst interval_split[OF k])
   986       apply (auto intro: order.trans)
   987       done
   988     fix K'
   989     assume "K' \<in> ?p2"
   990     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> {}"
   991       by blast
   992     assume "K \<noteq> K'"
   993     then show "interior K \<inter> interior K' = {}"
   994       unfolding l l' using p(5)[OF l(2) l'(2)] by auto
   995   }
   996 qed
   997 
   998 subsection%important \<open>Tagged (partial) divisions\<close>
   999 
  1000 definition%important tagged_partial_division_of (infixr "tagged'_partial'_division'_of" 40)
  1001   where "s tagged_partial_division_of i \<longleftrightarrow>
  1002     finite s \<and>
  1003     (\<forall>x K. (x, K) \<in> s \<longrightarrow> x \<in> K \<and> K \<subseteq> i \<and> (\<exists>a b. K = cbox a b)) \<and>
  1004     (\<forall>x1 K1 x2 K2. (x1, K1) \<in> s \<and> (x2, K2) \<in> s \<and> (x1, K1) \<noteq> (x2, K2) \<longrightarrow>
  1005       interior K1 \<inter> interior K2 = {})"
  1006 
  1007 lemma tagged_partial_division_ofD[dest]:
  1008   assumes "s tagged_partial_division_of i"
  1009   shows "finite s"
  1010     and "\<And>x K. (x,K) \<in> s \<Longrightarrow> x \<in> K"
  1011     and "\<And>x K. (x,K) \<in> s \<Longrightarrow> K \<subseteq> i"
  1012     and "\<And>x K. (x,K) \<in> s \<Longrightarrow> \<exists>a b. K = cbox a b"
  1013     and "\<And>x1 K1 x2 K2. (x1,K1) \<in> s \<Longrightarrow>
  1014       (x2, K2) \<in> s \<Longrightarrow> (x1, K1) \<noteq> (x2, K2) \<Longrightarrow> interior K1 \<inter> interior K2 = {}"
  1015   using assms unfolding tagged_partial_division_of_def by blast+
  1016 
  1017 definition%important tagged_division_of (infixr "tagged'_division'_of" 40)
  1018   where "s tagged_division_of i \<longleftrightarrow> s tagged_partial_division_of i \<and> (\<Union>{K. \<exists>x. (x,K) \<in> s} = i)"
  1019 
  1020 lemma tagged_division_of_finite: "s tagged_division_of i \<Longrightarrow> finite s"
  1021   unfolding tagged_division_of_def tagged_partial_division_of_def by auto
  1022 
  1023 lemma%important tagged_division_of:
  1024   "s tagged_division_of i \<longleftrightarrow>
  1025     finite s \<and>
  1026     (\<forall>x K. (x, K) \<in> s \<longrightarrow> x \<in> K \<and> K \<subseteq> i \<and> (\<exists>a b. K = cbox a b)) \<and>
  1027     (\<forall>x1 K1 x2 K2. (x1, K1) \<in> s \<and> (x2, K2) \<in> s \<and> (x1, K1) \<noteq> (x2, K2) \<longrightarrow>
  1028       interior K1 \<inter> interior K2 = {}) \<and>
  1029     (\<Union>{K. \<exists>x. (x,K) \<in> s} = i)"
  1030   unfolding%unimportant tagged_division_of_def tagged_partial_division_of_def by auto
  1031 
  1032 lemma tagged_division_ofI:
  1033   assumes "finite s"
  1034     and "\<And>x K. (x,K) \<in> s \<Longrightarrow> x \<in> K"
  1035     and "\<And>x K. (x,K) \<in> s \<Longrightarrow> K \<subseteq> i"
  1036     and "\<And>x K. (x,K) \<in> s \<Longrightarrow> \<exists>a b. K = cbox a b"
  1037     and "\<And>x1 K1 x2 K2. (x1,K1) \<in> s \<Longrightarrow> (x2, K2) \<in> s \<Longrightarrow> (x1, K1) \<noteq> (x2, K2) \<Longrightarrow>
  1038       interior K1 \<inter> interior K2 = {}"
  1039     and "(\<Union>{K. \<exists>x. (x,K) \<in> s} = i)"
  1040   shows "s tagged_division_of i"
  1041   unfolding tagged_division_of
  1042   using assms  by fastforce
  1043 
  1044 lemma tagged_division_ofD[dest]:  (*FIXME USE A LOCALE*)
  1045   assumes "s tagged_division_of i"
  1046   shows "finite s"
  1047     and "\<And>x K. (x,K) \<in> s \<Longrightarrow> x \<in> K"
  1048     and "\<And>x K. (x,K) \<in> s \<Longrightarrow> K \<subseteq> i"
  1049     and "\<And>x K. (x,K) \<in> s \<Longrightarrow> \<exists>a b. K = cbox a b"
  1050     and "\<And>x1 K1 x2 K2. (x1, K1) \<in> s \<Longrightarrow> (x2, K2) \<in> s \<Longrightarrow> (x1, K1) \<noteq> (x2, K2) \<Longrightarrow>
  1051       interior K1 \<inter> interior K2 = {}"
  1052     and "(\<Union>{K. \<exists>x. (x,K) \<in> s} = i)"
  1053   using assms unfolding tagged_division_of by blast+
  1054 
  1055 lemma%important division_of_tagged_division:
  1056   assumes "s tagged_division_of i"
  1057   shows "(snd ` s) division_of i"
  1058 proof%unimportant (rule division_ofI)
  1059   note assm = tagged_division_ofD[OF assms]
  1060   show "\<Union>(snd ` s) = i" "finite (snd ` s)"
  1061     using assm by auto
  1062   fix k
  1063   assume k: "k \<in> snd ` s"
  1064   then obtain xk where xk: "(xk, k) \<in> s"
  1065     by auto
  1066   then show "k \<subseteq> i" "k \<noteq> {}" "\<exists>a b. k = cbox a b"
  1067     using assm by fastforce+
  1068   fix k'
  1069   assume k': "k' \<in> snd ` s" "k \<noteq> k'"
  1070   from this(1) obtain xk' where xk': "(xk', k') \<in> s"
  1071     by auto
  1072   then show "interior k \<inter> interior k' = {}"
  1073     using assm(5) k'(2) xk by blast
  1074 qed
  1075 
  1076 lemma%important partial_division_of_tagged_division:
  1077   assumes "s tagged_partial_division_of i"
  1078   shows "(snd ` s) division_of \<Union>(snd ` s)"
  1079 proof%unimportant (rule division_ofI)
  1080   note assm = tagged_partial_division_ofD[OF assms]
  1081   show "finite (snd ` s)" "\<Union>(snd ` s) = \<Union>(snd ` s)"
  1082     using assm by auto
  1083   fix k
  1084   assume k: "k \<in> snd ` s"
  1085   then obtain xk where xk: "(xk, k) \<in> s"
  1086     by auto
  1087   then show "k \<noteq> {}" "\<exists>a b. k = cbox a b" "k \<subseteq> \<Union>(snd ` s)"
  1088     using assm by auto
  1089   fix k'
  1090   assume k': "k' \<in> snd ` s" "k \<noteq> k'"
  1091   from this(1) obtain xk' where xk': "(xk', k') \<in> s"
  1092     by auto
  1093   then show "interior k \<inter> interior k' = {}"
  1094     using assm(5) k'(2) xk by auto
  1095 qed
  1096 
  1097 lemma tagged_partial_division_subset:
  1098   assumes "s tagged_partial_division_of i"
  1099     and "t \<subseteq> s"
  1100   shows "t tagged_partial_division_of i"
  1101   using assms finite_subset[OF assms(2)]
  1102   unfolding tagged_partial_division_of_def
  1103   by blast
  1104 
  1105 lemma tag_in_interval: "p tagged_division_of i \<Longrightarrow> (x, k) \<in> p \<Longrightarrow> x \<in> i"
  1106   by auto
  1107 
  1108 lemma tagged_division_of_empty: "{} tagged_division_of {}"
  1109   unfolding tagged_division_of by auto
  1110 
  1111 lemma tagged_partial_division_of_trivial[simp]: "p tagged_partial_division_of {} \<longleftrightarrow> p = {}"
  1112   unfolding tagged_partial_division_of_def by auto
  1113 
  1114 lemma tagged_division_of_trivial[simp]: "p tagged_division_of {} \<longleftrightarrow> p = {}"
  1115   unfolding tagged_division_of by auto
  1116 
  1117 lemma tagged_division_of_self: "x \<in> cbox a b \<Longrightarrow> {(x,cbox a b)} tagged_division_of (cbox a b)"
  1118   by (rule tagged_division_ofI) auto
  1119 
  1120 lemma tagged_division_of_self_real: "x \<in> {a .. b::real} \<Longrightarrow> {(x,{a .. b})} tagged_division_of {a .. b}"
  1121   unfolding box_real[symmetric]
  1122   by (rule tagged_division_of_self)
  1123 
  1124 lemma%important tagged_division_Un:
  1125   assumes "p1 tagged_division_of s1"
  1126     and "p2 tagged_division_of s2"
  1127     and "interior s1 \<inter> interior s2 = {}"
  1128   shows "(p1 \<union> p2) tagged_division_of (s1 \<union> s2)"
  1129 proof%unimportant (rule tagged_division_ofI)
  1130   note p1 = tagged_division_ofD[OF assms(1)]
  1131   note p2 = tagged_division_ofD[OF assms(2)]
  1132   show "finite (p1 \<union> p2)"
  1133     using p1(1) p2(1) by auto
  1134   show "\<Union>{k. \<exists>x. (x, k) \<in> p1 \<union> p2} = s1 \<union> s2"
  1135     using p1(6) p2(6) by blast
  1136   fix x k
  1137   assume xk: "(x, k) \<in> p1 \<union> p2"
  1138   show "x \<in> k" "\<exists>a b. k = cbox a b"
  1139     using xk p1(2,4) p2(2,4) by auto
  1140   show "k \<subseteq> s1 \<union> s2"
  1141     using xk p1(3) p2(3) by blast
  1142   fix x' k'
  1143   assume xk': "(x', k') \<in> p1 \<union> p2" "(x, k) \<noteq> (x', k')"
  1144   have *: "\<And>a b. a \<subseteq> s1 \<Longrightarrow> b \<subseteq> s2 \<Longrightarrow> interior a \<inter> interior b = {}"
  1145     using assms(3) interior_mono by blast
  1146   show "interior k \<inter> interior k' = {}"
  1147     apply (cases "(x, k) \<in> p1")
  1148     apply (meson "*" UnE assms(1) assms(2) p1(5) tagged_division_ofD(3) xk'(1) xk'(2))
  1149     by (metis "*" UnE assms(1) assms(2) inf_sup_aci(1) p2(5) tagged_division_ofD(3) xk xk'(1) xk'(2))
  1150 qed
  1151 
  1152 lemma%important tagged_division_Union:
  1153   assumes "finite I"
  1154     and tag: "\<And>i. i\<in>I \<Longrightarrow> pfn i tagged_division_of i"
  1155     and disj: "\<And>i1 i2. \<lbrakk>i1 \<in> I; i2 \<in> I; i1 \<noteq> i2\<rbrakk> \<Longrightarrow> interior(i1) \<inter> interior(i2) = {}"
  1156   shows "\<Union>(pfn ` I) tagged_division_of (\<Union>I)"
  1157 proof%unimportant (rule tagged_division_ofI)
  1158   note assm = tagged_division_ofD[OF tag]
  1159   show "finite (\<Union>(pfn ` I))"
  1160     using assms by auto
  1161   have "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>(pfn ` I)} = \<Union>((\<lambda>i. \<Union>{k. \<exists>x. (x, k) \<in> pfn i}) ` I)"
  1162     by blast
  1163   also have "\<dots> = \<Union>I"
  1164     using assm(6) by auto
  1165   finally show "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>(pfn ` I)} = \<Union>I" .
  1166   fix x k
  1167   assume xk: "(x, k) \<in> \<Union>(pfn ` I)"
  1168   then obtain i where i: "i \<in> I" "(x, k) \<in> pfn i"
  1169     by auto
  1170   show "x \<in> k" "\<exists>a b. k = cbox a b" "k \<subseteq> \<Union>I"
  1171     using assm(2-4)[OF i] using i(1) by auto
  1172   fix x' k'
  1173   assume xk': "(x', k') \<in> \<Union>(pfn ` I)" "(x, k) \<noteq> (x', k')"
  1174   then obtain i' where i': "i' \<in> I" "(x', k') \<in> pfn i'"
  1175     by auto
  1176   have *: "\<And>a b. i \<noteq> i' \<Longrightarrow> a \<subseteq> i \<Longrightarrow> b \<subseteq> i' \<Longrightarrow> interior a \<inter> interior b = {}"
  1177     using i(1) i'(1) disj interior_mono by blast
  1178   show "interior k \<inter> interior k' = {}"
  1179   proof (cases "i = i'")
  1180     case True then show ?thesis 
  1181       using assm(5) i' i xk'(2) by blast
  1182   next
  1183     case False then show ?thesis 
  1184     using "*" assm(3) i' i by auto
  1185   qed
  1186 qed
  1187 
  1188 lemma tagged_partial_division_of_Union_self:
  1189   assumes "p tagged_partial_division_of s"
  1190   shows "p tagged_division_of (\<Union>(snd ` p))"
  1191   apply (rule tagged_division_ofI)
  1192   using tagged_partial_division_ofD[OF assms]
  1193   apply auto
  1194   done
  1195 
  1196 lemma tagged_division_of_union_self:
  1197   assumes "p tagged_division_of s"
  1198   shows "p tagged_division_of (\<Union>(snd ` p))"
  1199   apply (rule tagged_division_ofI)
  1200   using tagged_division_ofD[OF assms]
  1201   apply auto
  1202   done
  1203 
  1204 lemma tagged_division_Un_interval:
  1205   fixes a :: "'a::euclidean_space"
  1206   assumes "p1 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<le> (c::real)})"
  1207     and "p2 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
  1208     and k: "k \<in> Basis"
  1209   shows "(p1 \<union> p2) tagged_division_of (cbox a b)"
  1210 proof -
  1211   have *: "cbox a b = (cbox a b \<inter> {x. x\<bullet>k \<le> c}) \<union> (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
  1212     by auto
  1213   show ?thesis
  1214     apply (subst *)
  1215     apply (rule tagged_division_Un[OF assms(1-2)])
  1216     unfolding interval_split[OF k] interior_cbox
  1217     using k
  1218     apply (auto simp add: box_def elim!: ballE[where x=k])
  1219     done
  1220 qed
  1221 
  1222 lemma tagged_division_Un_interval_real:
  1223   fixes a :: real
  1224   assumes "p1 tagged_division_of ({a .. b} \<inter> {x. x\<bullet>k \<le> (c::real)})"
  1225     and "p2 tagged_division_of ({a .. b} \<inter> {x. x\<bullet>k \<ge> c})"
  1226     and k: "k \<in> Basis"
  1227   shows "(p1 \<union> p2) tagged_division_of {a .. b}"
  1228   using assms
  1229   unfolding box_real[symmetric]
  1230   by (rule tagged_division_Un_interval)
  1231 
  1232 lemma%important tagged_division_split_left_inj:
  1233   assumes d: "d tagged_division_of i"
  1234   and tags: "(x1, K1) \<in> d" "(x2, K2) \<in> d"
  1235   and "K1 \<noteq> K2"
  1236   and eq: "K1 \<inter> {x. x \<bullet> k \<le> c} = K2 \<inter> {x. x \<bullet> k \<le> c}"
  1237     shows "interior (K1 \<inter> {x. x\<bullet>k \<le> c}) = {}"
  1238 proof%unimportant -
  1239   have "interior (K1 \<inter> K2) = {} \<or> (x2, K2) = (x1, K1)"
  1240     using tags d by (metis (no_types) interior_Int tagged_division_ofD(5))
  1241   then show ?thesis
  1242     using eq \<open>K1 \<noteq> K2\<close> by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject)
  1243 qed
  1244 
  1245 lemma tagged_division_split_right_inj:
  1246   assumes d: "d tagged_division_of i"
  1247   and tags: "(x1, K1) \<in> d" "(x2, K2) \<in> d"
  1248   and "K1 \<noteq> K2"
  1249   and eq: "K1 \<inter> {x. x\<bullet>k \<ge> c} = K2 \<inter> {x. x\<bullet>k \<ge> c}"
  1250     shows "interior (K1 \<inter> {x. x\<bullet>k \<ge> c}) = {}"
  1251 proof -
  1252   have "interior (K1 \<inter> K2) = {} \<or> (x2, K2) = (x1, K1)"
  1253     using tags d by (metis (no_types) interior_Int tagged_division_ofD(5))
  1254   then show ?thesis
  1255     using eq \<open>K1 \<noteq> K2\<close> by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject)
  1256 qed
  1257 
  1258 lemma%important (in comm_monoid_set) over_tagged_division_lemma:
  1259   assumes "p tagged_division_of i"
  1260     and "\<And>u v. box u v = {} \<Longrightarrow> d (cbox u v) = \<^bold>1"
  1261   shows "F (\<lambda>(_, k). d k) p = F d (snd ` p)"
  1262 proof%unimportant -
  1263   have *: "(\<lambda>(_ ,k). d k) = d \<circ> snd"
  1264     by (simp add: fun_eq_iff)
  1265   note assm = tagged_division_ofD[OF assms(1)]
  1266   show ?thesis
  1267     unfolding *
  1268   proof (rule reindex_nontrivial[symmetric])
  1269     show "finite p"
  1270       using assm by auto
  1271     fix x y
  1272     assume "x\<in>p" "y\<in>p" "x\<noteq>y" "snd x = snd y"
  1273     obtain a b where ab: "snd x = cbox a b"
  1274       using assm(4)[of "fst x" "snd x"] \<open>x\<in>p\<close> by auto
  1275     have "(fst x, snd y) \<in> p" "(fst x, snd y) \<noteq> y"
  1276       using \<open>x \<in> p\<close> \<open>x \<noteq> y\<close> \<open>snd x = snd y\<close> [symmetric] by auto
  1277     with \<open>x\<in>p\<close> \<open>y\<in>p\<close> have "interior (snd x) \<inter> interior (snd y) = {}"
  1278       by (intro assm(5)[of "fst x" _ "fst y"]) auto
  1279     then have "box a b = {}"
  1280       unfolding \<open>snd x = snd y\<close>[symmetric] ab by auto
  1281     then have "d (cbox a b) = \<^bold>1"
  1282       using assm(2)[of "fst x" "snd x"] \<open>x\<in>p\<close> ab[symmetric] by (intro assms(2)) auto
  1283     then show "d (snd x) = \<^bold>1"
  1284       unfolding ab by auto
  1285   qed
  1286 qed
  1287 
  1288 
  1289 subsection%important \<open>Functions closed on boxes: morphisms from boxes to monoids\<close>
  1290 
  1291 text \<open>This auxiliary structure is used to sum up over the elements of a division. Main theorem is
  1292   \<open>operative_division\<close>. Instances for the monoid are @{typ "'a option"}, @{typ real}, and
  1293   @{typ bool}.\<close>
  1294 
  1295 paragraph%important \<open>Using additivity of lifted function to encode definedness.\<close>
  1296 
  1297 definition%important lift_option :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> 'c option"
  1298 where
  1299   "lift_option f a' b' = Option.bind a' (\<lambda>a. Option.bind b' (\<lambda>b. Some (f a b)))"
  1300 
  1301 lemma lift_option_simps[simp]:
  1302   "lift_option f (Some a) (Some b) = Some (f a b)"
  1303   "lift_option f None b' = None"
  1304   "lift_option f a' None = None"
  1305   by (auto simp: lift_option_def)
  1306 
  1307 lemma%important comm_monoid_lift_option:
  1308   assumes "comm_monoid f z"
  1309   shows "comm_monoid (lift_option f) (Some z)"
  1310 proof%unimportant -
  1311   from assms interpret comm_monoid f z .
  1312   show ?thesis
  1313     by standard (auto simp: lift_option_def ac_simps split: bind_split)
  1314 qed
  1315 
  1316 lemma comm_monoid_and: "comm_monoid HOL.conj True"
  1317   by standard auto
  1318 
  1319 lemma comm_monoid_set_and: "comm_monoid_set HOL.conj True"
  1320   by (rule comm_monoid_set.intro) (fact comm_monoid_and)
  1321 
  1322 
  1323 paragraph \<open>Misc\<close>
  1324 
  1325 lemma interval_real_split:
  1326   "{a .. b::real} \<inter> {x. x \<le> c} = {a .. min b c}"
  1327   "{a .. b} \<inter> {x. c \<le> x} = {max a c .. b}"
  1328   apply (metis Int_atLeastAtMostL1 atMost_def)
  1329   apply (metis Int_atLeastAtMostL2 atLeast_def)
  1330   done
  1331 
  1332 lemma bgauge_existence_lemma: "(\<forall>x\<in>s. \<exists>d::real. 0 < d \<and> q d x) \<longleftrightarrow> (\<forall>x. \<exists>d>0. x\<in>s \<longrightarrow> q d x)"
  1333   by (meson zero_less_one)
  1334 
  1335 
  1336 paragraph \<open>Division points\<close>
  1337 
  1338 definition%important "division_points (k::('a::euclidean_space) set) d =
  1339    {(j,x). j \<in> Basis \<and> (interval_lowerbound k)\<bullet>j < x \<and> x < (interval_upperbound k)\<bullet>j \<and>
  1340      (\<exists>i\<in>d. (interval_lowerbound i)\<bullet>j = x \<or> (interval_upperbound i)\<bullet>j = x)}"
  1341 
  1342 lemma%important division_points_finite:
  1343   fixes i :: "'a::euclidean_space set"
  1344   assumes "d division_of i"
  1345   shows "finite (division_points i d)"
  1346 proof%unimportant -
  1347   note assm = division_ofD[OF assms]
  1348   let ?M = "\<lambda>j. {(j,x)|x. (interval_lowerbound i)\<bullet>j < x \<and> x < (interval_upperbound i)\<bullet>j \<and>
  1349     (\<exists>i\<in>d. (interval_lowerbound i)\<bullet>j = x \<or> (interval_upperbound i)\<bullet>j = x)}"
  1350   have *: "division_points i d = \<Union>(?M ` Basis)"
  1351     unfolding division_points_def by auto
  1352   show ?thesis
  1353     unfolding * using assm by auto
  1354 qed
  1355 
  1356 lemma%important division_points_subset:
  1357   fixes a :: "'a::euclidean_space"
  1358   assumes "d division_of (cbox a b)"
  1359     and "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"  "a\<bullet>k < c" "c < b\<bullet>k"
  1360     and k: "k \<in> Basis"
  1361   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> {}} \<subseteq>
  1362       division_points (cbox a b) d" (is ?t1)
  1363     and "division_points (cbox a b \<inter> {x. x\<bullet>k \<ge> c}) {l \<inter> {x. x\<bullet>k \<ge> c} | l . l \<in> d \<and> \<not>(l \<inter> {x. x\<bullet>k \<ge> c} = {})} \<subseteq>
  1364       division_points (cbox a b) d" (is ?t2)
  1365 proof%unimportant -
  1366   note assm = division_ofD[OF assms(1)]
  1367   have *: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
  1368     "\<forall>i\<in>Basis. a\<bullet>i \<le> (\<Sum>i\<in>Basis. (if i = k then min (b \<bullet> k) c else  b \<bullet> i) *\<^sub>R i) \<bullet> i"
  1369     "\<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"
  1370     "min (b \<bullet> k) c = c" "max (a \<bullet> k) c = c"
  1371     using assms using less_imp_le by auto
  1372    have "\<exists>i\<in>d. interval_lowerbound i \<bullet> x = y \<or> interval_upperbound i \<bullet> x = y"
  1373      if "a \<bullet> x < y" "y < (if x = k then c else b \<bullet> x)"
  1374         "interval_lowerbound i \<bullet> x = y \<or> interval_upperbound i \<bullet> x = y"
  1375         "i = l \<inter> {x. x \<bullet> k \<le> c}" "l \<in> d" "l \<inter> {x. x \<bullet> k \<le> c} \<noteq> {}"
  1376         "x \<in> Basis" for i l x y
  1377   proof -
  1378     obtain u v where l: "l = cbox u v"
  1379       using \<open>l \<in> d\<close> assms(1) by blast
  1380     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"
  1381       using that(6) unfolding l interval_split[OF k] box_ne_empty that .
  1382     have **: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i"
  1383       using l using that(6) unfolding box_ne_empty[symmetric] by auto
  1384     show ?thesis
  1385       apply (rule bexI[OF _ \<open>l \<in> d\<close>])
  1386       using that(1-3,5) \<open>x \<in> Basis\<close>
  1387       unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] that
  1388       apply (auto split: if_split_asm)
  1389       done
  1390   qed
  1391   moreover have "\<And>x y. \<lbrakk>y < (if x = k then c else b \<bullet> x)\<rbrakk> \<Longrightarrow> y < b \<bullet> x"
  1392     using \<open>c < b\<bullet>k\<close> by (auto split: if_split_asm)
  1393   ultimately show ?t1 
  1394     unfolding division_points_def interval_split[OF k, of a b]
  1395     unfolding interval_bounds[OF *(1)] interval_bounds[OF *(2)] interval_bounds[OF *(3)]
  1396     unfolding * by force
  1397   have "\<And>x y i l. (if x = k then c else a \<bullet> x) < y \<Longrightarrow> a \<bullet> x < y"
  1398     using \<open>a\<bullet>k < c\<close> by (auto split: if_split_asm)
  1399   moreover have "\<exists>i\<in>d. interval_lowerbound i \<bullet> x = y \<or>
  1400                        interval_upperbound i \<bullet> x = y"
  1401     if "(if x = k then c else a \<bullet> x) < y" "y < b \<bullet> x"
  1402       "interval_lowerbound i \<bullet> x = y \<or> interval_upperbound i \<bullet> x = y"
  1403       "i = l \<inter> {x. c \<le> x \<bullet> k}" "l \<in> d" "l \<inter> {x. c \<le> x \<bullet> k} \<noteq> {}"
  1404       "x \<in> Basis" for x y i l
  1405   proof -
  1406     obtain u v where l: "l = cbox u v"
  1407       using \<open>l \<in> d\<close> assm(4) by blast
  1408     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"
  1409       using that(6) unfolding l interval_split[OF k] box_ne_empty that .
  1410     have **: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i"
  1411       using l using that(6) unfolding box_ne_empty[symmetric] by auto
  1412     show "\<exists>i\<in>d. interval_lowerbound i \<bullet> x = y \<or> interval_upperbound i \<bullet> x = y"
  1413       apply (rule bexI[OF _ \<open>l \<in> d\<close>])
  1414       using that(1-3,5) \<open>x \<in> Basis\<close>
  1415       unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] that
  1416       apply (auto split: if_split_asm)
  1417       done
  1418   qed
  1419   ultimately show ?t2
  1420     unfolding division_points_def interval_split[OF k, of a b]
  1421     unfolding interval_bounds[OF *(1)] interval_bounds[OF *(2)] interval_bounds[OF *(3)]
  1422     unfolding *
  1423     by force
  1424 qed
  1425 
  1426 lemma%important division_points_psubset:
  1427   fixes a :: "'a::euclidean_space"
  1428   assumes d: "d division_of (cbox a b)"
  1429       and altb: "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"  "a\<bullet>k < c" "c < b\<bullet>k"
  1430       and "l \<in> d"
  1431       and disj: "interval_lowerbound l\<bullet>k = c \<or> interval_upperbound l\<bullet>k = c"
  1432       and k: "k \<in> Basis"
  1433   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>
  1434          division_points (cbox a b) d" (is "?D1 \<subset> ?D")
  1435     and "division_points (cbox a b \<inter> {x. x\<bullet>k \<ge> c}) {l \<inter> {x. x\<bullet>k \<ge> c} | l. l\<in>d \<and> l \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}} \<subset>
  1436          division_points (cbox a b) d" (is "?D2 \<subset> ?D")
  1437 proof%unimportant -
  1438   have ab: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
  1439     using altb by (auto intro!:less_imp_le)
  1440   obtain u v where l: "l = cbox u v"
  1441     using d \<open>l \<in> d\<close> by blast
  1442   have uv: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i" "\<forall>i\<in>Basis. a\<bullet>i \<le> u\<bullet>i \<and> v\<bullet>i \<le> b\<bullet>i"
  1443     apply (metis assms(5) box_ne_empty(1) cbox_division_memE d l)
  1444     by (metis assms(5) box_ne_empty(1) cbox_division_memE d l subset_box(1))
  1445   have *: "interval_upperbound (cbox a b \<inter> {x. x \<bullet> k \<le> interval_upperbound l \<bullet> k}) \<bullet> k = interval_upperbound l \<bullet> k"
  1446           "interval_upperbound (cbox a b \<inter> {x. x \<bullet> k \<le> interval_lowerbound l \<bullet> k}) \<bullet> k = interval_lowerbound l \<bullet> k"
  1447     unfolding l interval_split[OF k] interval_bounds[OF uv(1)]
  1448     using uv[rule_format, of k] ab k
  1449     by auto
  1450   have "\<exists>x. x \<in> ?D - ?D1"
  1451     using assms(3-)
  1452     unfolding division_points_def interval_bounds[OF ab]
  1453     by (force simp add: *)
  1454   moreover have "?D1 \<subseteq> ?D"
  1455     by (auto simp add: assms division_points_subset)
  1456   ultimately show "?D1 \<subset> ?D"
  1457     by blast
  1458   have *: "interval_lowerbound (cbox a b \<inter> {x. x \<bullet> k \<ge> interval_lowerbound l \<bullet> k}) \<bullet> k = interval_lowerbound l \<bullet> k"
  1459     "interval_lowerbound (cbox a b \<inter> {x. x \<bullet> k \<ge> interval_upperbound l \<bullet> k}) \<bullet> k = interval_upperbound l \<bullet> k"
  1460     unfolding l interval_split[OF k] interval_bounds[OF uv(1)]
  1461     using uv[rule_format, of k] ab k
  1462     by auto
  1463   have "\<exists>x. x \<in> ?D - ?D2"
  1464     using assms(3-)
  1465     unfolding division_points_def interval_bounds[OF ab]
  1466     by (force simp add: *)
  1467   moreover have "?D2 \<subseteq> ?D"
  1468     by (auto simp add: assms division_points_subset)
  1469   ultimately show "?D2 \<subset> ?D"
  1470     by blast
  1471 qed
  1472 
  1473 lemma division_split_left_inj:
  1474   fixes S :: "'a::euclidean_space set"
  1475   assumes div: "\<D> division_of S"
  1476     and eq: "K1 \<inter> {x::'a. x\<bullet>k \<le> c} = K2 \<inter> {x. x\<bullet>k \<le> c}"
  1477     and "K1 \<in> \<D>" "K2 \<in> \<D>" "K1 \<noteq> K2"
  1478   shows "interior (K1 \<inter> {x. x\<bullet>k \<le> c}) = {}"
  1479 proof -
  1480   have "interior K2 \<inter> interior {a. a \<bullet> k \<le> c} = interior K1 \<inter> interior {a. a \<bullet> k \<le> c}"
  1481     by (metis (no_types) eq interior_Int)
  1482   moreover have "\<And>A. interior A \<inter> interior K2 = {} \<or> A = K2 \<or> A \<notin> \<D>"
  1483     by (meson div \<open>K2 \<in> \<D>\<close> division_of_def)
  1484   ultimately show ?thesis
  1485     using \<open>K1 \<in> \<D>\<close> \<open>K1 \<noteq> K2\<close> by auto
  1486 qed
  1487 
  1488 lemma%important division_split_right_inj:
  1489   fixes S :: "'a::euclidean_space set"
  1490   assumes div: "\<D> division_of S"
  1491     and eq: "K1 \<inter> {x::'a. x\<bullet>k \<ge> c} = K2 \<inter> {x. x\<bullet>k \<ge> c}"
  1492     and "K1 \<in> \<D>" "K2 \<in> \<D>" "K1 \<noteq> K2"
  1493   shows "interior (K1 \<inter> {x. x\<bullet>k \<ge> c}) = {}"
  1494 proof%unimportant -
  1495   have "interior K2 \<inter> interior {a. a \<bullet> k \<ge> c} = interior K1 \<inter> interior {a. a \<bullet> k \<ge> c}"
  1496     by (metis (no_types) eq interior_Int)
  1497   moreover have "\<And>A. interior A \<inter> interior K2 = {} \<or> A = K2 \<or> A \<notin> \<D>"
  1498     by (meson div \<open>K2 \<in> \<D>\<close> division_of_def)
  1499   ultimately show ?thesis
  1500     using \<open>K1 \<in> \<D>\<close> \<open>K1 \<noteq> K2\<close> by auto
  1501 qed
  1502 
  1503 lemma interval_doublesplit:
  1504   fixes a :: "'a::euclidean_space"
  1505   assumes "k \<in> Basis"
  1506   shows "cbox a b \<inter> {x . \<bar>x\<bullet>k - c\<bar> \<le> (e::real)} =
  1507     cbox (\<Sum>i\<in>Basis. (if i = k then max (a\<bullet>k) (c - e) else a\<bullet>i) *\<^sub>R i)
  1508      (\<Sum>i\<in>Basis. (if i = k then min (b\<bullet>k) (c + e) else b\<bullet>i) *\<^sub>R i)"
  1509 proof -
  1510   have *: "\<And>x c e::real. \<bar>x - c\<bar> \<le> e \<longleftrightarrow> x \<ge> c - e \<and> x \<le> c + e"
  1511     by auto
  1512   have **: "\<And>s P Q. s \<inter> {x. P x \<and> Q x} = (s \<inter> {x. Q x}) \<inter> {x. P x}"
  1513     by blast
  1514   show ?thesis
  1515     unfolding * ** interval_split[OF assms] by (rule refl)
  1516 qed
  1517 
  1518 lemma%important division_doublesplit:
  1519   fixes a :: "'a::euclidean_space"
  1520   assumes "p division_of (cbox a b)"
  1521     and k: "k \<in> Basis"
  1522   shows "(\<lambda>l. l \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> e}) ` {l\<in>p. l \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> e} \<noteq> {}}
  1523          division_of  (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> e})"
  1524 proof%unimportant -
  1525   have *: "\<And>x c. \<bar>x - c\<bar> \<le> e \<longleftrightarrow> x \<ge> c - e \<and> x \<le> c + e"
  1526     by auto
  1527   have **: "\<And>p q p' q'. p division_of q \<Longrightarrow> p = p' \<Longrightarrow> q = q' \<Longrightarrow> p' division_of q'"
  1528     by auto
  1529   note division_split(1)[OF assms, where c="c+e",unfolded interval_split[OF k]]
  1530   note division_split(2)[OF this, where c="c-e" and k=k,OF k]
  1531   then show ?thesis
  1532     apply (rule **)
  1533     subgoal
  1534       apply (simp add: abs_diff_le_iff field_simps Collect_conj_eq setcompr_eq_image[symmetric])
  1535       apply (rule equalityI)
  1536       apply blast
  1537       apply clarsimp
  1538       apply (rule_tac x="l \<inter> {x. c + e \<ge> x \<bullet> k}" in exI)
  1539       apply auto
  1540       done
  1541     by (simp add: interval_split k interval_doublesplit)
  1542 qed
  1543               
  1544 paragraph \<open>Operative\<close>
  1545 
  1546 locale operative = comm_monoid_set +
  1547   fixes g :: "'b::euclidean_space set \<Rightarrow> 'a"
  1548   assumes box_empty_imp: "\<And>a b. box a b = {} \<Longrightarrow> g (cbox a b) = \<^bold>1"
  1549     and Basis_imp: "\<And>a b c k. k \<in> Basis \<Longrightarrow> g (cbox a b) = g (cbox a b \<inter> {x. x\<bullet>k \<le> c}) \<^bold>* g (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
  1550 begin
  1551 
  1552 lemma empty [simp]:
  1553   "g {} = \<^bold>1"
  1554 proof -
  1555   have *: "cbox One (-One) = ({}::'b set)"
  1556     by (auto simp: box_eq_empty inner_sum_left inner_Basis sum.If_cases ex_in_conv)
  1557   moreover have "box One (-One) = ({}::'b set)"
  1558     using box_subset_cbox[of One "-One"] by (auto simp: *)
  1559   ultimately show ?thesis
  1560     using box_empty_imp [of One "-One"] by simp
  1561 qed
  1562        
  1563 lemma%important division:
  1564   "F g d = g (cbox a b)" if "d division_of (cbox a b)"
  1565 proof%unimportant -
  1566   define C where [abs_def]: "C = card (division_points (cbox a b) d)"
  1567   then show ?thesis
  1568   using that proof (induction C arbitrary: a b d rule: less_induct)
  1569     case (less a b d)
  1570     show ?case
  1571     proof cases
  1572       assume "box a b = {}"
  1573       { fix k assume "k\<in>d"
  1574         then obtain a' b' where k: "k = cbox a' b'"
  1575           using division_ofD(4)[OF less.prems] by blast
  1576         with \<open>k\<in>d\<close> division_ofD(2)[OF less.prems] have "cbox a' b' \<subseteq> cbox a b"
  1577           by auto
  1578         then have "box a' b' \<subseteq> box a b"
  1579           unfolding subset_box by auto
  1580         then have "g k = \<^bold>1"
  1581           using box_empty_imp [of a' b'] k by (simp add: \<open>box a b = {}\<close>) }
  1582       then show "box a b = {} \<Longrightarrow> F g d = g (cbox a b)"
  1583         by (auto intro!: neutral simp: box_empty_imp)
  1584     next
  1585       assume "box a b \<noteq> {}"
  1586       then have ab: "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i" and ab': "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
  1587         by (auto simp: box_ne_empty)
  1588       show "F g d = g (cbox a b)"
  1589       proof (cases "division_points (cbox a b) d = {}")
  1590         case True
  1591         { fix u v and j :: 'b
  1592           assume j: "j \<in> Basis" and as: "cbox u v \<in> d"
  1593           then have "cbox u v \<noteq> {}"
  1594             using less.prems by blast
  1595           then have uv: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i" "u\<bullet>j \<le> v\<bullet>j"
  1596             using j unfolding box_ne_empty by auto
  1597           have *: "\<And>p r Q. \<not> j\<in>Basis \<or> p \<or> r \<or> (\<forall>x\<in>d. Q x) \<Longrightarrow> p \<or> r \<or> Q (cbox u v)"
  1598             using as j by auto
  1599           have "(j, u\<bullet>j) \<notin> division_points (cbox a b) d"
  1600                "(j, v\<bullet>j) \<notin> division_points (cbox a b) d" using True by auto
  1601           note this[unfolded de_Morgan_conj division_points_def mem_Collect_eq split_conv interval_bounds[OF ab'] bex_simps]
  1602           note *[OF this(1)] *[OF this(2)] note this[unfolded interval_bounds[OF uv(1)]]
  1603           moreover
  1604           have "a\<bullet>j \<le> u\<bullet>j" "v\<bullet>j \<le> b\<bullet>j"
  1605             using division_ofD(2,2,3)[OF \<open>d division_of cbox a b\<close> as]
  1606             apply (metis j subset_box(1) uv(1))
  1607             by (metis \<open>cbox u v \<subseteq> cbox a b\<close> j subset_box(1) uv(1))
  1608           ultimately have "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"
  1609             unfolding not_less de_Morgan_disj using ab[rule_format,of j] uv(2) j by force }
  1610         then have d': "\<forall>i\<in>d. \<exists>u v. i = cbox u v \<and>
  1611           (\<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)"
  1612           unfolding forall_in_division[OF less.prems] by blast
  1613         have "(1/2) *\<^sub>R (a+b) \<in> cbox a b"
  1614           unfolding mem_box using ab by (auto simp: inner_simps)
  1615         note this[unfolded division_ofD(6)[OF \<open>d division_of cbox a b\<close>,symmetric] Union_iff]
  1616         then obtain i where i: "i \<in> d" "(1 / 2) *\<^sub>R (a + b) \<in> i" ..
  1617         obtain u v where uv: "i = cbox u v" 
  1618                      "\<forall>j\<in>Basis. u \<bullet> j = a \<bullet> j \<and> v \<bullet> j = a \<bullet> j \<or>
  1619                                 u \<bullet> j = b \<bullet> j \<and> v \<bullet> j = b \<bullet> j \<or>
  1620                                 u \<bullet> j = a \<bullet> j \<and> v \<bullet> j = b \<bullet> j"
  1621           using d' i(1) by auto
  1622         have "cbox a b \<in> d"
  1623         proof -
  1624           have "u = a" "v = b"
  1625             unfolding euclidean_eq_iff[where 'a='b]
  1626           proof safe
  1627             fix j :: 'b
  1628             assume j: "j \<in> Basis"
  1629             note i(2)[unfolded uv mem_box,rule_format,of j]
  1630             then show "u \<bullet> j = a \<bullet> j" and "v \<bullet> j = b \<bullet> j"
  1631               using uv(2)[rule_format,of j] j by (auto simp: inner_simps)
  1632           qed
  1633           then have "i = cbox a b" using uv by auto
  1634           then show ?thesis using i by auto
  1635         qed
  1636         then have deq: "d = insert (cbox a b) (d - {cbox a b})"
  1637           by auto
  1638         have "F g (d - {cbox a b}) = \<^bold>1"
  1639         proof (intro neutral ballI)
  1640           fix x
  1641           assume x: "x \<in> d - {cbox a b}"
  1642           then have "x\<in>d"
  1643             by auto note d'[rule_format,OF this]
  1644           then obtain u v where uv: "x = cbox u v"
  1645                       "\<forall>j\<in>Basis. u \<bullet> j = a \<bullet> j \<and> v \<bullet> j = a \<bullet> j \<or>
  1646                                  u \<bullet> j = b \<bullet> j \<and> v \<bullet> j = b \<bullet> j \<or>
  1647                                  u \<bullet> j = a \<bullet> j \<and> v \<bullet> j = b \<bullet> j" 
  1648             by blast
  1649           have "u \<noteq> a \<or> v \<noteq> b"
  1650             using x[unfolded uv] by auto
  1651           then obtain j where "u\<bullet>j \<noteq> a\<bullet>j \<or> v\<bullet>j \<noteq> b\<bullet>j" and j: "j \<in> Basis"
  1652             unfolding euclidean_eq_iff[where 'a='b] by auto
  1653           then have "u\<bullet>j = v\<bullet>j"
  1654             using uv(2)[rule_format,OF j] by auto
  1655           then have "box u v = {}"
  1656             using j unfolding box_eq_empty by (auto intro!: bexI[of _ j])
  1657           then show "g x = \<^bold>1"
  1658             unfolding uv(1) by (rule box_empty_imp)
  1659         qed
  1660         then show "F g d = g (cbox a b)"
  1661           using division_ofD[OF less.prems]
  1662           apply (subst deq)
  1663           apply (subst insert)
  1664           apply auto
  1665           done
  1666       next
  1667         case False
  1668         then have "\<exists>x. x \<in> division_points (cbox a b) d"
  1669           by auto
  1670         then obtain k c 
  1671           where "k \<in> Basis" "interval_lowerbound (cbox a b) \<bullet> k < c"
  1672                 "c < interval_upperbound (cbox a b) \<bullet> k"
  1673                 "\<exists>i\<in>d. interval_lowerbound i \<bullet> k = c \<or> interval_upperbound i \<bullet> k = c"
  1674           unfolding division_points_def by auto
  1675         then obtain j where "a \<bullet> k < c" "c < b \<bullet> k" 
  1676               and "j \<in> d" and j: "interval_lowerbound j \<bullet> k = c \<or> interval_upperbound j \<bullet> k = c"
  1677           by (metis division_of_trivial empty_iff interval_bounds' less.prems)
  1678         let ?lec = "{x. x\<bullet>k \<le> c}" let ?gec = "{x. x\<bullet>k \<ge> c}"
  1679         define d1 where "d1 = {l \<inter> ?lec | l. l \<in> d \<and> l \<inter> ?lec \<noteq> {}}"
  1680         define d2 where "d2 = {l \<inter> ?gec | l. l \<in> d \<and> l \<inter> ?gec \<noteq> {}}"
  1681         define cb where "cb = (\<Sum>i\<in>Basis. (if i = k then c else b\<bullet>i) *\<^sub>R i)"
  1682         define ca where "ca = (\<Sum>i\<in>Basis. (if i = k then c else a\<bullet>i) *\<^sub>R i)"
  1683         have "division_points (cbox a b \<inter> ?lec) {l \<inter> ?lec |l. l \<in> d \<and> l \<inter> ?lec \<noteq> {}} 
  1684               \<subset> division_points (cbox a b) d"
  1685           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>])
  1686         with division_points_finite[OF \<open>d division_of cbox a b\<close>] 
  1687         have "card
  1688          (division_points (cbox a b \<inter> ?lec) {l \<inter> ?lec |l. l \<in> d \<and> l \<inter> ?lec \<noteq> {}})
  1689            < card (division_points (cbox a b) d)"
  1690           by (rule psubset_card_mono)
  1691         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> {}}
  1692               \<subset> division_points (cbox a b) d"
  1693           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>])
  1694         with division_points_finite[OF \<open>d division_of cbox a b\<close>] 
  1695         have "card (division_points (cbox a b \<inter> ?gec) {l \<inter> ?gec |l. l \<in> d \<and> l \<inter> ?gec \<noteq> {}})
  1696               < card (division_points (cbox a b) d)"
  1697           by (rule psubset_card_mono)
  1698         ultimately have *: "F g d1 = g (cbox a b \<inter> ?lec)" "F g d2 = g (cbox a b \<inter> ?gec)"
  1699           unfolding interval_split[OF \<open>k \<in> Basis\<close>]
  1700           apply (rule_tac[!] less.hyps)
  1701           using division_split[OF \<open>d division_of cbox a b\<close>, where k=k and c=c] \<open>k \<in> Basis\<close>
  1702           by (simp_all add: interval_split  d1_def d2_def division_points_finite[OF \<open>d division_of cbox a b\<close>])
  1703         have fxk_le: "g (l \<inter> ?lec) = \<^bold>1" 
  1704           if "l \<in> d" "y \<in> d" "l \<inter> ?lec = y \<inter> ?lec" "l \<noteq> y" for l y
  1705         proof -
  1706           obtain u v where leq: "l = cbox u v"
  1707             using \<open>l \<in> d\<close> less.prems by auto
  1708           have "interior (cbox u v \<inter> ?lec) = {}"
  1709             using that division_split_left_inj leq less.prems by blast
  1710           then show ?thesis
  1711             unfolding leq interval_split [OF \<open>k \<in> Basis\<close>]
  1712             by (auto intro: box_empty_imp)
  1713         qed
  1714         have fxk_ge: "g (l \<inter> {x. x \<bullet> k \<ge> c}) = \<^bold>1"
  1715           if "l \<in> d" "y \<in> d" "l \<inter> ?gec = y \<inter> ?gec" "l \<noteq> y" for l y
  1716         proof -
  1717           obtain u v where leq: "l = cbox u v"
  1718             using \<open>l \<in> d\<close> less.prems by auto
  1719           have "interior (cbox u v \<inter> ?gec) = {}"
  1720             using that division_split_right_inj leq less.prems by blast
  1721           then show ?thesis
  1722             unfolding leq interval_split[OF \<open>k \<in> Basis\<close>]
  1723             by (auto intro: box_empty_imp)
  1724         qed
  1725         have d1_alt: "d1 = (\<lambda>l. l \<inter> ?lec) ` {l \<in> d. l \<inter> ?lec \<noteq> {}}"
  1726           using d1_def by auto
  1727         have d2_alt: "d2 = (\<lambda>l. l \<inter> ?gec) ` {l \<in> d. l \<inter> ?gec \<noteq> {}}"
  1728           using d2_def by auto
  1729         have "g (cbox a b) = F g d1 \<^bold>* F g d2" (is "_ = ?prev")
  1730           unfolding * using \<open>k \<in> Basis\<close>
  1731           by (auto dest: Basis_imp)
  1732         also have "F g d1 = F (\<lambda>l. g (l \<inter> ?lec)) d"
  1733           unfolding d1_alt using division_of_finite[OF less.prems] fxk_le
  1734           by (subst reindex_nontrivial) (auto intro!: mono_neutral_cong_left)
  1735         also have "F g d2 = F (\<lambda>l. g (l \<inter> ?gec)) d"
  1736           unfolding d2_alt using division_of_finite[OF less.prems] fxk_ge
  1737           by (subst reindex_nontrivial) (auto intro!: mono_neutral_cong_left)
  1738         also have *: "\<forall>x\<in>d. g x = g (x \<inter> ?lec) \<^bold>* g (x \<inter> ?gec)"
  1739           unfolding forall_in_division[OF \<open>d division_of cbox a b\<close>]
  1740           using \<open>k \<in> Basis\<close>
  1741           by (auto dest: Basis_imp)
  1742         have "F (\<lambda>l. g (l \<inter> ?lec)) d \<^bold>* F (\<lambda>l. g (l \<inter> ?gec)) d = F g d"
  1743           using * by (simp add: distrib)
  1744         finally show ?thesis by auto
  1745       qed
  1746     qed
  1747   qed
  1748 qed
  1749 
  1750 lemma%important tagged_division:
  1751   assumes "d tagged_division_of (cbox a b)"
  1752   shows "F (\<lambda>(_, l). g l) d = g (cbox a b)"
  1753 proof%unimportant -
  1754   have "F (\<lambda>(_, k). g k) d = F g (snd ` d)"
  1755     using assms box_empty_imp by (rule over_tagged_division_lemma)
  1756   then show ?thesis
  1757     unfolding assms [THEN division_of_tagged_division, THEN division] .
  1758   qed
  1759 
  1760 end
  1761 
  1762 locale operative_real = comm_monoid_set +
  1763   fixes g :: "real set \<Rightarrow> 'a"
  1764   assumes neutral: "b \<le> a \<Longrightarrow> g {a..b} = \<^bold>1"
  1765   assumes coalesce_less: "a < c \<Longrightarrow> c < b \<Longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
  1766 begin
  1767 
  1768 sublocale operative where g = g
  1769   rewrites "box = (greaterThanLessThan :: real \<Rightarrow> _)"
  1770     and "cbox = (atLeastAtMost :: real \<Rightarrow> _)"
  1771     and "\<And>x::real. x \<in> Basis \<longleftrightarrow> x = 1"
  1772 proof -
  1773   show "operative f z g"
  1774   proof
  1775     show "g (cbox a b) = \<^bold>1" if "box a b = {}" for a b
  1776       using that by (simp add: neutral)
  1777     show "g (cbox a b) = g (cbox a b \<inter> {x. x \<bullet> k \<le> c}) \<^bold>* g (cbox a b \<inter> {x. c \<le> x \<bullet> k})"
  1778       if "k \<in> Basis" for a b c k
  1779     proof -
  1780       from that have [simp]: "k = 1"
  1781         by simp
  1782       from neutral [of 0 1] neutral [of a a for a] coalesce_less
  1783   have [simp]: "g {} = \<^bold>1" "\<And>a. g {a} = \<^bold>1"
  1784     "\<And>a b c. a < c \<Longrightarrow> c < b \<Longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
  1785     by auto
  1786       have "g {a..b} = g {a..min b c} \<^bold>* g {max a c..b}"
  1787     by (auto simp: min_def max_def le_less)
  1788       then show "g (cbox a b) = g (cbox a b \<inter> {x. x \<bullet> k \<le> c}) \<^bold>* g (cbox a b \<inter> {x. c \<le> x \<bullet> k})"
  1789         by (simp add: atMost_def [symmetric] atLeast_def [symmetric])
  1790 qed
  1791   qed
  1792   show "box = (greaterThanLessThan :: real \<Rightarrow> _)"
  1793     and "cbox = (atLeastAtMost :: real \<Rightarrow> _)"
  1794     and "\<And>x::real. x \<in> Basis \<longleftrightarrow> x = 1"
  1795     by (simp_all add: fun_eq_iff)
  1796 qed
  1797 
  1798 lemma coalesce_less_eq:
  1799   "g {a..c} \<^bold>* g {c..b} = g {a..b}" if "a \<le> c" "c \<le> b"
  1800   proof (cases "c = a \<or> c = b")
  1801     case False
  1802   with that have "a < c" "c < b"
  1803     by auto
  1804     then show ?thesis
  1805     by (rule coalesce_less)
  1806   next
  1807     case True
  1808   with that box_empty_imp [of a a] box_empty_imp [of b b] show ?thesis
  1809     by safe simp_all
  1810     qed
  1811 
  1812 end
  1813 
  1814 lemma operative_realI:
  1815   "operative_real f z g" if "operative f z g"
  1816 proof -
  1817   interpret operative f z g
  1818     using that .
  1819   show ?thesis
  1820   proof
  1821     show "g {a..b} = z" if "b \<le> a" for a b
  1822       using that box_empty_imp by simp
  1823     show "f (g {a..c}) (g {c..b}) = g {a..b}" if "a < c" "c < b" for a b c
  1824       using that
  1825     using Basis_imp [of 1 a b c]
  1826       by (simp_all add: atMost_def [symmetric] atLeast_def [symmetric] max_def min_def)
  1827 qed
  1828 qed
  1829 
  1830 
  1831 subsection%important \<open>Special case of additivity we need for the FTC\<close>
  1832 (*fix add explanation here *)
  1833 lemma%important additive_tagged_division_1:
  1834   fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
  1835   assumes "a \<le> b"
  1836     and "p tagged_division_of {a..b}"
  1837   shows "sum (\<lambda>(x,k). f(Sup k) - f(Inf k)) p = f b - f a"
  1838 proof%unimportant -
  1839   let ?f = "(\<lambda>k::(real) set. if k = {} then 0 else f(interval_upperbound k) - f(interval_lowerbound k))"
  1840   interpret operative_real plus 0 ?f
  1841     rewrites "comm_monoid_set.F (+) 0 = sum"
  1842     by standard[1] (auto simp add: sum_def)
  1843   have p_td: "p tagged_division_of cbox a b"
  1844     using assms(2) box_real(2) by presburger
  1845   have **: "cbox a b \<noteq> {}"
  1846     using assms(1) by auto
  1847   then have "f b - f a = (\<Sum>(x, l)\<in>p. if l = {} then 0 else f (interval_upperbound l) - f (interval_lowerbound l))"
  1848     proof -
  1849       have "(if cbox a b = {} then 0 else f (interval_upperbound (cbox a b)) - f (interval_lowerbound (cbox a b))) = f b - f a"
  1850         using assms by auto
  1851       then show ?thesis
  1852         using p_td assms by (simp add: tagged_division) 
  1853     qed 
  1854   then show ?thesis
  1855     using assms by (auto intro!: sum.cong)
  1856 qed
  1857 
  1858 
  1859 subsection%important \<open>Fine-ness of a partition w.r.t. a gauge\<close>
  1860 
  1861 definition%important fine  (infixr "fine" 46)
  1862   where "d fine s \<longleftrightarrow> (\<forall>(x,k) \<in> s. k \<subseteq> d x)"
  1863 
  1864 lemma fineI:
  1865   assumes "\<And>x k. (x, k) \<in> s \<Longrightarrow> k \<subseteq> d x"
  1866   shows "d fine s"
  1867   using assms unfolding fine_def by auto
  1868 
  1869 lemma fineD[dest]:
  1870   assumes "d fine s"
  1871   shows "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> d x"
  1872   using assms unfolding fine_def by auto
  1873 
  1874 lemma fine_Int: "(\<lambda>x. d1 x \<inter> d2 x) fine p \<longleftrightarrow> d1 fine p \<and> d2 fine p"
  1875   unfolding fine_def by auto
  1876 
  1877 lemma fine_Inter:
  1878  "(\<lambda>x. \<Inter>{f d x | d.  d \<in> s}) fine p \<longleftrightarrow> (\<forall>d\<in>s. (f d) fine p)"
  1879   unfolding fine_def by blast
  1880 
  1881 lemma fine_Un: "d fine p1 \<Longrightarrow> d fine p2 \<Longrightarrow> d fine (p1 \<union> p2)"
  1882   unfolding fine_def by blast
  1883 
  1884 lemma%important fine_Union: "(\<And>p. p \<in> ps \<Longrightarrow> d fine p) \<Longrightarrow> d fine (\<Union>ps)"
  1885   unfolding fine_def by auto
  1886 
  1887 lemma%unimportant fine_subset: "p \<subseteq> q \<Longrightarrow> d fine q \<Longrightarrow> d fine p"
  1888   unfolding fine_def by blast
  1889 
  1890 subsection%important \<open>Some basic combining lemmas\<close>
  1891 
  1892 lemma%important tagged_division_Union_exists:
  1893   assumes "finite I"
  1894     and "\<forall>i\<in>I. \<exists>p. p tagged_division_of i \<and> d fine p"
  1895     and "\<forall>i1\<in>I. \<forall>i2\<in>I. i1 \<noteq> i2 \<longrightarrow> interior i1 \<inter> interior i2 = {}"
  1896     and "\<Union>I = i"
  1897    obtains p where "p tagged_division_of i" and "d fine p"
  1898 proof%unimportant -
  1899   obtain pfn where pfn:
  1900     "\<And>x. x \<in> I \<Longrightarrow> pfn x tagged_division_of x"
  1901     "\<And>x. x \<in> I \<Longrightarrow> d fine pfn x"
  1902     using bchoice[OF assms(2)] by auto
  1903   show thesis
  1904     apply (rule_tac p="\<Union>(pfn ` I)" in that)
  1905     using assms(1) assms(3) assms(4) pfn(1) tagged_division_Union apply force
  1906     by (metis (mono_tags, lifting) fine_Union imageE pfn(2))
  1907 qed
  1908 (* FIXME structure here, do not have one lemma in each subsection *)
  1909 
  1910 subsection%unimportant \<open>The set we're concerned with must be closed\<close>
  1911 
  1912 lemma division_of_closed:
  1913   fixes i :: "'n::euclidean_space set"
  1914   shows "s division_of i \<Longrightarrow> closed i"
  1915   unfolding division_of_def by fastforce
  1916 
  1917 subsection%important \<open>General bisection principle for intervals; might be useful elsewhere\<close>
  1918 
  1919 lemma%important interval_bisection_step:
  1920   fixes type :: "'a::euclidean_space"
  1921   assumes emp: "P {}"
  1922     and Un: "\<And>S T. \<lbrakk>P S; P T; interior(S) \<inter> interior(T) = {}\<rbrakk> \<Longrightarrow> P (S \<union> T)"
  1923     and non: "\<not> P (cbox a (b::'a))"
  1924   obtains c d where "\<not> P (cbox c d)"
  1925     and "\<And>i. i \<in> Basis \<Longrightarrow> a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i"
  1926 proof%unimportant -
  1927   have "cbox a b \<noteq> {}"
  1928     using emp non by metis
  1929   then have ab: "\<And>i. i\<in>Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
  1930     by (force simp: mem_box)
  1931   have UN_cases: "\<lbrakk>finite \<F>;
  1932            \<And>S. S\<in>\<F> \<Longrightarrow> P S;
  1933            \<And>S. S\<in>\<F> \<Longrightarrow> \<exists>a b. S = cbox a b;
  1934            \<And>S T. S\<in>\<F> \<Longrightarrow> T\<in>\<F> \<Longrightarrow> S \<noteq> T \<Longrightarrow> interior S \<inter> interior T = {}\<rbrakk> \<Longrightarrow> P (\<Union>\<F>)" for \<F>
  1935   proof (induct \<F> rule: finite_induct)
  1936     case empty show ?case
  1937       using emp by auto
  1938   next
  1939     case (insert x f)
  1940     then show ?case
  1941       unfolding Union_insert by (metis Int_interior_Union_intervals Un insert_iff open_interior)
  1942   qed
  1943   let ?ab = "\<lambda>i. (a\<bullet>i + b\<bullet>i) / 2"
  1944   let ?A = "{cbox c d | c d::'a. \<forall>i\<in>Basis. (c\<bullet>i = a\<bullet>i) \<and> (d\<bullet>i = ?ab i) \<or>
  1945     (c\<bullet>i = ?ab i) \<and> (d\<bullet>i = b\<bullet>i)}"
  1946   have "P (\<Union>?A)" 
  1947     if "\<And>c d.  \<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i \<Longrightarrow> P (cbox c d)"
  1948   proof (rule UN_cases)
  1949     let ?B = "(\<lambda>S. cbox (\<Sum>i\<in>Basis. (if i \<in> S then a\<bullet>i else ?ab i) *\<^sub>R i::'a)
  1950                         (\<Sum>i\<in>Basis. (if i \<in> S then ?ab i else b\<bullet>i) *\<^sub>R i)) ` {s. s \<subseteq> Basis}"
  1951     have "?A \<subseteq> ?B"
  1952     proof
  1953       fix x
  1954       assume "x \<in> ?A"
  1955       then obtain c d
  1956         where x:  "x = cbox c d"
  1957           "\<And>i. i \<in> Basis \<Longrightarrow>
  1958                         c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = ?ab i \<or> c \<bullet> i = ?ab i \<and> d \<bullet> i = b \<bullet> i" 
  1959         by blast
  1960       have "c = (\<Sum>i\<in>Basis. (if c \<bullet> i = a \<bullet> i then a \<bullet> i else ?ab i) *\<^sub>R i)"
  1961            "d = (\<Sum>i\<in>Basis. (if c \<bullet> i = a \<bullet> i then ?ab i else b \<bullet> i) *\<^sub>R i)"
  1962         using x(2) ab by (fastforce simp add: euclidean_eq_iff[where 'a='a])+
  1963       then show "x \<in> ?B"
  1964         unfolding x by (rule_tac x="{i. i\<in>Basis \<and> c\<bullet>i = a\<bullet>i}" in image_eqI) auto
  1965     qed
  1966     then show "finite ?A"
  1967       by (rule finite_subset) auto
  1968   next
  1969     fix S
  1970     assume "S \<in> ?A"
  1971     then obtain c d
  1972       where s: "S = cbox c d"
  1973                "\<And>i. i \<in> Basis \<Longrightarrow> c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = ?ab i \<or> c \<bullet> i = ?ab i \<and> d \<bullet> i = b \<bullet> i"
  1974       by blast
  1975     show "P S"
  1976       unfolding s using ab s(2) by (fastforce intro!: that)
  1977     show "\<exists>a b. S = cbox a b"
  1978       unfolding s by auto
  1979     fix T
  1980     assume "T \<in> ?A"
  1981     then obtain e f where t:
  1982       "T = cbox e f"
  1983       "\<And>i. i \<in> Basis \<Longrightarrow> e \<bullet> i = a \<bullet> i \<and> f \<bullet> i = ?ab i \<or> e \<bullet> i = ?ab i \<and> f \<bullet> i = b \<bullet> i"
  1984       by blast
  1985     assume "S \<noteq> T"
  1986     then have "\<not> (c = e \<and> d = f)"
  1987       unfolding s t by auto
  1988     then obtain i where "c\<bullet>i \<noteq> e\<bullet>i \<or> d\<bullet>i \<noteq> f\<bullet>i" and i': "i \<in> Basis"
  1989       unfolding euclidean_eq_iff[where 'a='a] by auto
  1990     then have i: "c\<bullet>i \<noteq> e\<bullet>i" "d\<bullet>i \<noteq> f\<bullet>i"
  1991       using s(2) t(2) apply fastforce
  1992       using t(2)[OF i'] \<open>c \<bullet> i \<noteq> e \<bullet> i \<or> d \<bullet> i \<noteq> f \<bullet> i\<close> i' s(2) t(2) by fastforce
  1993     have *: "\<And>s t. (\<And>a. a \<in> s \<Longrightarrow> a \<in> t \<Longrightarrow> False) \<Longrightarrow> s \<inter> t = {}"
  1994       by auto
  1995     show "interior S \<inter> interior T = {}"
  1996       unfolding s t interior_cbox
  1997     proof (rule *)
  1998       fix x
  1999       assume "x \<in> box c d" "x \<in> box e f"
  2000       then have x: "c\<bullet>i < d\<bullet>i" "e\<bullet>i < f\<bullet>i" "c\<bullet>i < f\<bullet>i" "e\<bullet>i < d\<bullet>i"
  2001         unfolding mem_box using i'  by force+
  2002       show False  using s(2)[OF i'] t(2)[OF i'] and i x  
  2003         by auto
  2004     qed
  2005   qed
  2006   also have "\<Union>?A = cbox a b"
  2007   proof (rule set_eqI,rule)
  2008     fix x
  2009     assume "x \<in> \<Union>?A"
  2010     then obtain c d where x:
  2011       "x \<in> cbox c d"
  2012       "\<And>i. i \<in> Basis \<Longrightarrow> c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = ?ab i \<or> c \<bullet> i = ?ab i \<and> d \<bullet> i = b \<bullet> i"
  2013       by blast
  2014     then show "x\<in>cbox a b"
  2015       unfolding mem_box by force
  2016   next
  2017     fix x
  2018     assume x: "x \<in> cbox a b"
  2019     then have "\<forall>i\<in>Basis. \<exists>c d. (c = a\<bullet>i \<and> d = ?ab i \<or> c = ?ab i \<and> d = b\<bullet>i) \<and> c\<le>x\<bullet>i \<and> x\<bullet>i \<le> d"
  2020       (is "\<forall>i\<in>Basis. \<exists>c d. ?P i c d")
  2021       unfolding mem_box by (metis linear)
  2022     then obtain \<alpha> \<beta> where "\<forall>i\<in>Basis. (\<alpha> \<bullet> i = a \<bullet> i \<and> \<beta> \<bullet> i = ?ab i \<or>
  2023          \<alpha> \<bullet> i = ?ab i \<and> \<beta> \<bullet> i = b \<bullet> i) \<and> \<alpha> \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> \<beta> \<bullet> i"
  2024       by (auto simp: choice_Basis_iff)
  2025     then show "x\<in>\<Union>?A"
  2026       by (force simp add: mem_box)
  2027   qed
  2028   finally show thesis
  2029       by (metis (no_types, lifting) assms(3) that)
  2030 qed
  2031 
  2032 lemma%important interval_bisection:
  2033   fixes type :: "'a::euclidean_space"
  2034   assumes "P {}"
  2035     and Un: "\<And>S T. \<lbrakk>P S; P T; interior(S) \<inter> interior(T) = {}\<rbrakk> \<Longrightarrow> P (S \<union> T)"
  2036     and "\<not> P (cbox a (b::'a))"
  2037   obtains x where "x \<in> cbox a b"
  2038     and "\<forall>e>0. \<exists>c d. x \<in> cbox c d \<and> cbox c d \<subseteq> ball x e \<and> cbox c d \<subseteq> cbox a b \<and> \<not> P (cbox c d)"
  2039 proof%unimportant -
  2040   have "\<forall>x. \<exists>y. \<not> P (cbox (fst x) (snd x)) \<longrightarrow> (\<not> P (cbox (fst y) (snd y)) \<and>
  2041     (\<forall>i\<in>Basis. fst x\<bullet>i \<le> fst y\<bullet>i \<and> fst y\<bullet>i \<le> snd y\<bullet>i \<and> snd y\<bullet>i \<le> snd x\<bullet>i \<and>
  2042        2 * (snd y\<bullet>i - fst y\<bullet>i) \<le> snd x\<bullet>i - fst x\<bullet>i))" (is "\<forall>x. ?P x")
  2043   proof
  2044     show "?P x" for x
  2045     proof (cases "P (cbox (fst x) (snd x))")
  2046       case True
  2047       then show ?thesis by auto
  2048     next
  2049       case False
  2050       obtain c d where "\<not> P (cbox c d)"
  2051         "\<And>i. i \<in> Basis \<Longrightarrow>
  2052            fst x \<bullet> i \<le> c \<bullet> i \<and>
  2053            c \<bullet> i \<le> d \<bullet> i \<and>
  2054            d \<bullet> i \<le> snd x \<bullet> i \<and>
  2055            2 * (d \<bullet> i - c \<bullet> i) \<le> snd x \<bullet> i - fst x \<bullet> i"
  2056         by (blast intro: interval_bisection_step[of P, OF assms(1-2) False])
  2057       then show ?thesis
  2058         by (rule_tac x="(c,d)" in exI) auto
  2059     qed
  2060   qed
  2061   then obtain f where f:
  2062     "\<forall>x.
  2063       \<not> P (cbox (fst x) (snd x)) \<longrightarrow>
  2064       \<not> P (cbox (fst (f x)) (snd (f x))) \<and>
  2065         (\<forall>i\<in>Basis.
  2066             fst x \<bullet> i \<le> fst (f x) \<bullet> i \<and>
  2067             fst (f x) \<bullet> i \<le> snd (f x) \<bullet> i \<and>
  2068             snd (f x) \<bullet> i \<le> snd x \<bullet> i \<and>
  2069             2 * (snd (f x) \<bullet> i - fst (f x) \<bullet> i) \<le> snd x \<bullet> i - fst x \<bullet> i)" by metis
  2070   define AB A B where ab_def: "AB n = (f ^^ n) (a,b)" "A n = fst(AB n)" "B n = snd(AB n)" for n
  2071   have [simp]: "A 0 = a" "B 0 = b" and ABRAW: "\<And>n. \<not> P (cbox (A(Suc n)) (B(Suc n))) \<and>
  2072     (\<forall>i\<in>Basis. A(n)\<bullet>i \<le> A(Suc n)\<bullet>i \<and> A(Suc n)\<bullet>i \<le> B(Suc n)\<bullet>i \<and> B(Suc n)\<bullet>i \<le> B(n)\<bullet>i \<and>
  2073     2 * (B(Suc n)\<bullet>i - A(Suc n)\<bullet>i) \<le> B(n)\<bullet>i - A(n)\<bullet>i)" (is "\<And>n. ?P n")
  2074   proof -
  2075     show "A 0 = a" "B 0 = b"
  2076       unfolding ab_def by auto
  2077     note S = ab_def funpow.simps o_def id_apply
  2078     show "?P n" for n
  2079     proof (induct n)
  2080       case 0
  2081       then show ?case
  2082         unfolding S using \<open>\<not> P (cbox a b)\<close> f by auto
  2083     next
  2084       case (Suc n)
  2085       show ?case
  2086         unfolding S
  2087         apply (rule f[rule_format])
  2088         using Suc
  2089         unfolding S
  2090         apply auto
  2091         done
  2092     qed
  2093   qed
  2094   then have AB: "A(n)\<bullet>i \<le> A(Suc n)\<bullet>i" "A(Suc n)\<bullet>i \<le> B(Suc n)\<bullet>i" 
  2095                  "B(Suc n)\<bullet>i \<le> B(n)\<bullet>i" "2 * (B(Suc n)\<bullet>i - A(Suc n)\<bullet>i) \<le> B(n)\<bullet>i - A(n)\<bullet>i" 
  2096                 if "i\<in>Basis" for i n
  2097     using that by blast+
  2098   have notPAB: "\<not> P (cbox (A(Suc n)) (B(Suc n)))" for n
  2099     using ABRAW by blast
  2100   have interv: "\<exists>n. \<forall>x\<in>cbox (A n) (B n). \<forall>y\<in>cbox (A n) (B n). dist x y < e"
  2101     if e: "0 < e" for e
  2102   proof -
  2103     obtain n where n: "(\<Sum>i\<in>Basis. b \<bullet> i - a \<bullet> i) / e < 2 ^ n"
  2104       using real_arch_pow[of 2 "(sum (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis) / e"] by auto
  2105     show ?thesis
  2106     proof (rule exI [where x=n], clarify)
  2107       fix x y
  2108       assume xy: "x\<in>cbox (A n) (B n)" "y\<in>cbox (A n) (B n)"
  2109       have "dist x y \<le> sum (\<lambda>i. \<bar>(x - y)\<bullet>i\<bar>) Basis"
  2110         unfolding dist_norm by(rule norm_le_l1)
  2111       also have "\<dots> \<le> sum (\<lambda>i. B n\<bullet>i - A n\<bullet>i) Basis"
  2112       proof (rule sum_mono)
  2113         fix i :: 'a
  2114         assume i: "i \<in> Basis"
  2115         show "\<bar>(x - y) \<bullet> i\<bar> \<le> B n \<bullet> i - A n \<bullet> i"
  2116           using xy[unfolded mem_box,THEN bspec, OF i]
  2117           by (auto simp: inner_diff_left)
  2118       qed
  2119       also have "\<dots> \<le> sum (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis / 2^n"
  2120         unfolding sum_divide_distrib
  2121       proof (rule sum_mono)
  2122         show "B n \<bullet> i - A n \<bullet> i \<le> (b \<bullet> i - a \<bullet> i) / 2 ^ n" if i: "i \<in> Basis" for i
  2123         proof (induct n)
  2124           case 0
  2125           then show ?case
  2126             unfolding AB by auto
  2127         next
  2128           case (Suc n)
  2129           have "B (Suc n) \<bullet> i - A (Suc n) \<bullet> i \<le> (B n \<bullet> i - A n \<bullet> i) / 2"
  2130             using AB(3) that AB(4)[of i n] using i by auto
  2131           also have "\<dots> \<le> (b \<bullet> i - a \<bullet> i) / 2 ^ Suc n"
  2132             using Suc by (auto simp add: field_simps)
  2133           finally show ?case .
  2134         qed
  2135       qed
  2136       also have "\<dots> < e"
  2137         using n using e by (auto simp add: field_simps)
  2138       finally show "dist x y < e" .
  2139     qed
  2140   qed
  2141   {
  2142     fix n m :: nat
  2143     assume "m \<le> n" then have "cbox (A n) (B n) \<subseteq> cbox (A m) (B m)"
  2144     proof (induction rule: inc_induct)
  2145       case (step i)
  2146       show ?case
  2147         using AB by (intro order_trans[OF step.IH] subset_box_imp) auto
  2148     qed simp
  2149   } note ABsubset = this
  2150   have "\<And>n. cbox (A n) (B n) \<noteq> {}"
  2151     by (meson AB dual_order.trans interval_not_empty)
  2152   then obtain x0 where x0: "\<And>n. x0 \<in> cbox (A n) (B n)"
  2153     using decreasing_closed_nest [OF closed_cbox] ABsubset interv by blast
  2154   show thesis
  2155   proof (rule that[rule_format, of x0])
  2156     show "x0\<in>cbox a b"
  2157       using \<open>A 0 = a\<close> \<open>B 0 = b\<close> x0 by blast
  2158     fix e :: real
  2159     assume "e > 0"
  2160     from interv[OF this] obtain n
  2161       where n: "\<forall>x\<in>cbox (A n) (B n). \<forall>y\<in>cbox (A n) (B n). dist x y < e" ..
  2162     have "\<not> P (cbox (A n) (B n))"
  2163     proof (cases "0 < n")
  2164       case True then show ?thesis 
  2165         by (metis Suc_pred' notPAB) 
  2166     next
  2167       case False then show ?thesis
  2168         using \<open>A 0 = a\<close> \<open>B 0 = b\<close> \<open>\<not> P (cbox a b)\<close> by blast
  2169     qed
  2170     moreover have "cbox (A n) (B n) \<subseteq> ball x0 e"
  2171       using n using x0[of n] by auto
  2172     moreover have "cbox (A n) (B n) \<subseteq> cbox a b"
  2173       using ABsubset \<open>A 0 = a\<close> \<open>B 0 = b\<close> by blast
  2174     ultimately show "\<exists>c d. x0 \<in> cbox c d \<and> cbox c d \<subseteq> ball x0 e \<and> cbox c d \<subseteq> cbox a b \<and> \<not> P (cbox c d)"
  2175       apply (rule_tac x="A n" in exI)
  2176       apply (rule_tac x="B n" in exI)
  2177       apply (auto simp: x0)
  2178       done
  2179   qed
  2180 qed
  2181 
  2182 
  2183 subsection%important \<open>Cousin's lemma\<close>
  2184 
  2185 lemma%important fine_division_exists:
  2186   fixes a b :: "'a::euclidean_space"
  2187   assumes "gauge g"
  2188   obtains p where "p tagged_division_of (cbox a b)" "g fine p"
  2189 proof%unimportant (cases "\<exists>p. p tagged_division_of (cbox a b) \<and> g fine p")
  2190   case True
  2191   then show ?thesis
  2192     using that by auto
  2193 next
  2194   case False
  2195   assume "\<not> (\<exists>p. p tagged_division_of (cbox a b) \<and> g fine p)"
  2196   obtain x where x:
  2197       "x \<in> (cbox a b)"
  2198       "\<And>e. 0 < e \<Longrightarrow>
  2199         \<exists>c d.
  2200           x \<in> cbox c d \<and>
  2201           cbox c d \<subseteq> ball x e \<and>
  2202           cbox c d \<subseteq> (cbox a b) \<and>
  2203           \<not> (\<exists>p. p tagged_division_of cbox c d \<and> g fine p)"
  2204     apply (rule interval_bisection[of "\<lambda>s. \<exists>p. p tagged_division_of s \<and> g fine p", OF _ _ False])
  2205     apply (simp add: fine_def)
  2206     apply (metis tagged_division_Un fine_Un)
  2207     apply auto
  2208     done
  2209   obtain e where e: "e > 0" "ball x e \<subseteq> g x"
  2210     using gaugeD[OF assms, of x] unfolding open_contains_ball by auto
  2211   from x(2)[OF e(1)]
  2212   obtain c d where c_d: "x \<in> cbox c d"
  2213                         "cbox c d \<subseteq> ball x e"
  2214                         "cbox c d \<subseteq> cbox a b"
  2215                         "\<not> (\<exists>p. p tagged_division_of cbox c d \<and> g fine p)"
  2216     by blast
  2217   have "g fine {(x, cbox c d)}"
  2218     unfolding fine_def using e using c_d(2) by auto
  2219   then show ?thesis
  2220     using tagged_division_of_self[OF c_d(1)] using c_d by auto
  2221 qed
  2222 
  2223 lemma fine_division_exists_real:
  2224   fixes a b :: real
  2225   assumes "gauge g"
  2226   obtains p where "p tagged_division_of {a .. b}" "g fine p"
  2227   by (metis assms box_real(2) fine_division_exists)
  2228 
  2229 subsection%important \<open>A technical lemma about "refinement" of division\<close>
  2230 
  2231 lemma%important tagged_division_finer:
  2232   fixes p :: "('a::euclidean_space \<times> ('a::euclidean_space set)) set"
  2233   assumes ptag: "p tagged_division_of (cbox a b)"
  2234     and "gauge d"
  2235   obtains q where "q tagged_division_of (cbox a b)"
  2236     and "d fine q"
  2237     and "\<forall>(x,k) \<in> p. k \<subseteq> d(x) \<longrightarrow> (x,k) \<in> q"
  2238 proof%unimportant -
  2239   have p: "finite p" "p tagged_partial_division_of (cbox a b)"
  2240     using ptag unfolding tagged_division_of_def by auto
  2241   have "(\<exists>q. q tagged_division_of (\<Union>{k. \<exists>x. (x,k) \<in> p}) \<and> d fine q \<and> (\<forall>(x,k) \<in> p. k \<subseteq> d(x) \<longrightarrow> (x,k) \<in> q))" 
  2242     if "finite p" "p tagged_partial_division_of (cbox a b)" "gauge d" for p
  2243     using that
  2244   proof (induct p)
  2245     case empty
  2246     show ?case
  2247       by (force simp add: fine_def)
  2248   next
  2249     case (insert xk p)
  2250     obtain x k where xk: "xk = (x, k)"
  2251       using surj_pair[of xk] by metis 
  2252     obtain q1 where q1: "q1 tagged_division_of \<Union>{k. \<exists>x. (x, k) \<in> p}"
  2253                 and "d fine q1"
  2254                 and q1I: "\<And>x k. \<lbrakk>(x, k)\<in>p;  k \<subseteq> d x\<rbrakk> \<Longrightarrow> (x, k) \<in> q1"
  2255       using case_prodD tagged_partial_division_subset[OF insert(4) subset_insertI]
  2256       by (metis (mono_tags, lifting) insert.hyps(3) insert.prems(2))
  2257     have *: "\<Union>{l. \<exists>y. (y,l) \<in> insert xk p} = k \<union> \<Union>{l. \<exists>y. (y,l) \<in> p}"
  2258       unfolding xk by auto
  2259     note p = tagged_partial_division_ofD[OF insert(4)]
  2260     obtain u v where uv: "k = cbox u v"
  2261       using p(4) xk by blast
  2262     have "finite {k. \<exists>x. (x, k) \<in> p}"
  2263       apply (rule finite_subset[of _ "snd ` p"])
  2264       using image_iff apply fastforce
  2265       using insert.hyps(1) by blast
  2266     then have int: "interior (cbox u v) \<inter> interior (\<Union>{k. \<exists>x. (x, k) \<in> p}) = {}"
  2267     proof (rule Int_interior_Union_intervals)
  2268       show "open (interior (cbox u v))"
  2269         by auto
  2270       show "\<And>T. T \<in> {k. \<exists>x. (x, k) \<in> p} \<Longrightarrow> \<exists>a b. T = cbox a b"
  2271         using p(4) by auto
  2272       show "\<And>T. T \<in> {k. \<exists>x. (x, k) \<in> p} \<Longrightarrow> interior (cbox u v) \<inter> interior T = {}"
  2273         by clarify (metis insert.hyps(2) insert_iff interior_cbox p(5) uv xk)
  2274     qed
  2275     show ?case
  2276     proof (cases "cbox u v \<subseteq> d x")
  2277       case True
  2278       have "{(x, cbox u v)} tagged_division_of cbox u v"
  2279         by (simp add: p(2) uv xk tagged_division_of_self)
  2280       then have "{(x, cbox u v)} \<union> q1 tagged_division_of \<Union>{k. \<exists>x. (x, k) \<in> insert xk p}"
  2281         unfolding * uv by (metis (no_types, lifting) int q1 tagged_division_Un)
  2282       with True show ?thesis
  2283         apply (rule_tac x="{(x,cbox u v)} \<union> q1" in exI)
  2284         using \<open>d fine q1\<close> fine_def q1I uv xk apply fastforce
  2285         done
  2286     next
  2287       case False
  2288       obtain q2 where q2: "q2 tagged_division_of cbox u v" "d fine q2"
  2289         using fine_division_exists[OF assms(2)] by blast
  2290       show ?thesis
  2291         apply (rule_tac x="q2 \<union> q1" in exI)
  2292         apply (intro conjI)
  2293         unfolding * uv
  2294         apply (rule tagged_division_Un q2 q1 int fine_Un)+
  2295           apply (auto intro: q1 q2 fine_Un \<open>d fine q1\<close> simp add: False q1I uv xk)
  2296         done
  2297     qed
  2298   qed
  2299   with p 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"
  2300     by (meson \<open>gauge d\<close>)
  2301   with ptag that show ?thesis by auto
  2302 qed
  2303 
  2304 subsubsection%important \<open>Covering lemma\<close>
  2305 
  2306 text\<open> Some technical lemmas used in the approximation results that follow. Proof of the covering
  2307   lemma is an obvious multidimensional generalization of Lemma 3, p65 of Swartz's
  2308   "Introduction to Gauge Integrals". \<close>
  2309 
  2310 proposition%important covering_lemma:
  2311   assumes "S \<subseteq> cbox a b" "box a b \<noteq> {}" "gauge g"
  2312   obtains \<D> where
  2313     "countable \<D>"  "\<Union>\<D> \<subseteq> cbox a b"
  2314     "\<And>K. K \<in> \<D> \<Longrightarrow> interior K \<noteq> {} \<and> (\<exists>c d. K = cbox c d)"
  2315     "pairwise (\<lambda>A B. interior A \<inter> interior B = {}) \<D>"
  2316     "\<And>K. K \<in> \<D> \<Longrightarrow> \<exists>x \<in> S \<inter> K. K \<subseteq> g x"
  2317     "\<And>u v. cbox u v \<in> \<D> \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
  2318     "S \<subseteq> \<Union>\<D>"
  2319 proof%unimportant -
  2320   have aibi: "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i" and normab: "0 < norm(b - a)"
  2321     using \<open>box a b \<noteq> {}\<close> box_eq_empty box_sing by fastforce+
  2322   let ?K0 = "\<lambda>(n, f::'a\<Rightarrow>nat).
  2323                     cbox (\<Sum>i \<in> Basis. (a \<bullet> i + (f i / 2^n) * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i)
  2324                          (\<Sum>i \<in> Basis. (a \<bullet> i + ((f i + 1) / 2^n) * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i)"
  2325   let ?D0 = "?K0 ` (SIGMA n:UNIV. Pi\<^sub>E Basis (\<lambda>i::'a. lessThan (2^n)))"
  2326   obtain \<D>0 where count: "countable \<D>0"
  2327              and sub: "\<Union>\<D>0 \<subseteq> cbox a b"
  2328              and int:  "\<And>K. K \<in> \<D>0 \<Longrightarrow> (interior K \<noteq> {}) \<and> (\<exists>c d. K = cbox c d)"
  2329              and intdj: "\<And>A B. \<lbrakk>A \<in> \<D>0; B \<in> \<D>0\<rbrakk> \<Longrightarrow> A \<subseteq> B \<or> B \<subseteq> A \<or> interior A \<inter> interior B = {}"
  2330              and SK: "\<And>x. x \<in> S \<Longrightarrow> \<exists>K \<in> \<D>0. x \<in> K \<and> K \<subseteq> g x"
  2331              and cbox: "\<And>u v. cbox u v \<in> \<D>0 \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
  2332              and fin: "\<And>K. K \<in> \<D>0 \<Longrightarrow> finite {L \<in> \<D>0. K \<subseteq> L}"
  2333   proof
  2334     show "countable ?D0"
  2335       by (simp add: countable_PiE)
  2336   next
  2337     show "\<Union>?D0 \<subseteq> cbox a b"
  2338       apply (simp add: UN_subset_iff)
  2339       apply (intro conjI allI ballI subset_box_imp)
  2340        apply (simp add: divide_simps zero_le_mult_iff aibi)
  2341       apply (force simp: aibi scaling_mono nat_less_real_le dest: PiE_mem)
  2342       done
  2343   next
  2344     show "\<And>K. K \<in> ?D0 \<Longrightarrow> interior K \<noteq> {} \<and> (\<exists>c d. K = cbox c d)"
  2345       using \<open>box a b \<noteq> {}\<close>
  2346       by (clarsimp simp: box_eq_empty) (fastforce simp add: divide_simps dest: PiE_mem)
  2347   next
  2348     have realff: "(real w) * 2^m < (real v) * 2^n \<longleftrightarrow> w * 2^m < v * 2^n" for m n v w
  2349       using of_nat_less_iff less_imp_of_nat_less by fastforce
  2350     have *: "\<forall>v w. ?K0(m,v) \<subseteq> ?K0(n,w) \<or> ?K0(n,w) \<subseteq> ?K0(m,v) \<or> interior(?K0(m,v)) \<inter> interior(?K0(n,w)) = {}"
  2351       for m n \<comment> \<open>The symmetry argument requires a single HOL formula\<close>
  2352     proof (rule linorder_wlog [where a=m and b=n], intro allI impI)
  2353       fix v w m and n::nat
  2354       assume "m \<le> n" \<comment> \<open>WLOG we can assume @{term"m \<le> n"}, when the first disjunct becomes impossible\<close>
  2355       have "?K0(n,w) \<subseteq> ?K0(m,v) \<or> interior(?K0(m,v)) \<inter> interior(?K0(n,w)) = {}"
  2356         apply (simp add: subset_box disjoint_interval)
  2357         apply (rule ccontr)
  2358         apply (clarsimp simp add: aibi mult_le_cancel_right divide_le_cancel not_less not_le)
  2359         apply (drule_tac x=i in bspec, assumption)
  2360         using \<open>m\<le>n\<close> realff [of _ _ "1+_"] realff [of "1+_"_ "1+_"]
  2361         apply (auto simp: divide_simps add.commute not_le nat_le_iff_add realff)
  2362         apply (simp add: power_add, metis (no_types, hide_lams) mult_Suc mult_less_cancel2 not_less_eq mult.assoc)+
  2363         done
  2364       then show "?K0(m,v) \<subseteq> ?K0(n,w) \<or> ?K0(n,w) \<subseteq> ?K0(m,v) \<or> interior(?K0(m,v)) \<inter> interior(?K0(n,w)) = {}"
  2365         by meson
  2366     qed auto
  2367     show "\<And>A B. \<lbrakk>A \<in> ?D0; B \<in> ?D0\<rbrakk> \<Longrightarrow> A \<subseteq> B \<or> B \<subseteq> A \<or> interior A \<inter> interior B = {}"
  2368       apply (erule imageE SigmaE)+
  2369       using * by simp
  2370   next
  2371     show "\<exists>K \<in> ?D0. x \<in> K \<and> K \<subseteq> g x" if "x \<in> S" for x
  2372     proof (simp only: bex_simps split_paired_Bex_Sigma)
  2373       show "\<exists>n. \<exists>f \<in> Basis \<rightarrow>\<^sub>E {..<2 ^ n}. x \<in> ?K0(n,f) \<and> ?K0(n,f) \<subseteq> g x"
  2374       proof -
  2375         obtain e where "0 < e"
  2376                    and e: "\<And>y. (\<And>i. i \<in> Basis \<Longrightarrow> \<bar>x \<bullet> i - y \<bullet> i\<bar> \<le> e) \<Longrightarrow> y \<in> g x"
  2377         proof -
  2378           have "x \<in> g x" "open (g x)"
  2379             using \<open>gauge g\<close> by (auto simp: gauge_def)
  2380           then obtain \<epsilon> where "0 < \<epsilon>" and \<epsilon>: "ball x \<epsilon> \<subseteq> g x"
  2381             using openE by blast
  2382           have "norm (x - y) < \<epsilon>"
  2383                if "(\<And>i. i \<in> Basis \<Longrightarrow> \<bar>x \<bullet> i - y \<bullet> i\<bar> \<le> \<epsilon> / (2 * real DIM('a)))" for y
  2384           proof -
  2385             have "norm (x - y) \<le> (\<Sum>i\<in>Basis. \<bar>x \<bullet> i - y \<bullet> i\<bar>)"
  2386               by (metis (no_types, lifting) inner_diff_left norm_le_l1 sum.cong)
  2387             also have "... \<le> DIM('a) * (\<epsilon> / (2 * real DIM('a)))"
  2388               by (meson sum_bounded_above that)
  2389             also have "... = \<epsilon> / 2"
  2390               by (simp add: divide_simps)
  2391             also have "... < \<epsilon>"
  2392               by (simp add: \<open>0 < \<epsilon>\<close>)
  2393             finally show ?thesis .
  2394           qed
  2395           then show ?thesis
  2396             by (rule_tac e = "\<epsilon> / 2 / DIM('a)" in that) (simp_all add:  \<open>0 < \<epsilon>\<close> dist_norm subsetD [OF \<epsilon>])
  2397         qed
  2398         have xab: "x \<in> cbox a b"
  2399           using \<open>x \<in> S\<close> \<open>S \<subseteq> cbox a b\<close> by blast
  2400         obtain n where n: "norm (b - a) / 2^n < e"
  2401           using real_arch_pow_inv [of "e / norm(b - a)" "1/2"] normab \<open>0 < e\<close>
  2402           by (auto simp: divide_simps)
  2403         then have "norm (b - a) < e * 2^n"
  2404           by (auto simp: divide_simps)
  2405         then have bai: "b \<bullet> i - a \<bullet> i < e * 2 ^ n" if "i \<in> Basis" for i
  2406         proof -
  2407           have "b \<bullet> i - a \<bullet> i \<le> norm (b - a)"
  2408             by (metis abs_of_nonneg dual_order.trans inner_diff_left linear norm_ge_zero Basis_le_norm that)
  2409           also have "... < e * 2 ^ n"
  2410             using \<open>norm (b - a) < e * 2 ^ n\<close> by blast
  2411           finally show ?thesis .
  2412         qed
  2413         have D: "(a + n \<le> x \<and> x \<le> a + m) \<Longrightarrow> (a + n \<le> y \<and> y \<le> a + m) \<Longrightarrow> abs(x - y) \<le> m - n"
  2414                  for a m n x and y::real
  2415           by auto
  2416         have "\<forall>i\<in>Basis. \<exists>k<2 ^ n. (a \<bullet> i + real k * (b \<bullet> i - a \<bullet> i) / 2 ^ n \<le> x \<bullet> i \<and>
  2417                x \<bullet> i \<le> a \<bullet> i + (real k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n)"
  2418         proof
  2419           fix i::'a assume "i \<in> Basis"
  2420           consider "x \<bullet> i = b \<bullet> i" | "x \<bullet> i < b \<bullet> i"
  2421             using \<open>i \<in> Basis\<close> mem_box(2) xab by force
  2422           then show "\<exists>k<2 ^ n. (a \<bullet> i + real k * (b \<bullet> i - a \<bullet> i) / 2 ^ n \<le> x \<bullet> i \<and>
  2423                           x \<bullet> i \<le> a \<bullet> i + (real k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n)"
  2424           proof cases
  2425             case 1 then show ?thesis
  2426               by (rule_tac x = "2^n - 1" in exI) (auto simp: algebra_simps divide_simps of_nat_diff \<open>i \<in> Basis\<close> aibi)
  2427           next
  2428             case 2
  2429             then have abi_less: "a \<bullet> i < b \<bullet> i"
  2430               using \<open>i \<in> Basis\<close> xab by (auto simp: mem_box)
  2431             let ?k = "nat \<lfloor>2 ^ n * (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)\<rfloor>"
  2432             show ?thesis
  2433             proof (intro exI conjI)
  2434               show "?k < 2 ^ n"
  2435                 using aibi xab \<open>i \<in> Basis\<close>
  2436                 by (force simp: nat_less_iff floor_less_iff divide_simps 2 mem_box)
  2437             next
  2438               have "a \<bullet> i + real ?k * (b \<bullet> i - a \<bullet> i) / 2 ^ n \<le>
  2439                     a \<bullet> i + (2 ^ n * (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)) * (b \<bullet> i - a \<bullet> i) / 2 ^ n"
  2440                 apply (intro add_left_mono mult_right_mono divide_right_mono of_nat_floor)
  2441                 using aibi [OF \<open>i \<in> Basis\<close>] xab 2
  2442                   apply (simp_all add: \<open>i \<in> Basis\<close> mem_box divide_simps)
  2443                 done
  2444               also have "... = x \<bullet> i"
  2445                 using abi_less by (simp add: divide_simps)
  2446               finally show "a \<bullet> i + real ?k * (b \<bullet> i - a \<bullet> i) / 2 ^ n \<le> x \<bullet> i" .
  2447             next
  2448               have "x \<bullet> i \<le> a \<bullet> i + (2 ^ n * (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)) * (b \<bullet> i - a \<bullet> i) / 2 ^ n"
  2449                 using abi_less by (simp add: divide_simps algebra_simps)
  2450               also have "... \<le> a \<bullet> i + (real ?k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n"
  2451                 apply (intro add_left_mono mult_right_mono divide_right_mono of_nat_floor)
  2452                 using aibi [OF \<open>i \<in> Basis\<close>] xab
  2453                   apply (auto simp: \<open>i \<in> Basis\<close> mem_box divide_simps)
  2454                 done
  2455               finally show "x \<bullet> i \<le> a \<bullet> i + (real ?k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n" .
  2456             qed
  2457           qed
  2458         qed
  2459         then have "\<exists>f\<in>Basis \<rightarrow>\<^sub>E {..<2 ^ n}. x \<in> ?K0(n,f)"
  2460           apply (simp add: mem_box Bex_def)
  2461           apply (clarify dest!: bchoice)
  2462           apply (rule_tac x="restrict f Basis" in exI, simp)
  2463           done
  2464         moreover have "\<And>f. x \<in> ?K0(n,f) \<Longrightarrow> ?K0(n,f) \<subseteq> g x"
  2465           apply (clarsimp simp add: mem_box)
  2466           apply (rule e)
  2467           apply (drule bspec D, assumption)+
  2468           apply (erule order_trans)
  2469           apply (simp add: divide_simps)
  2470           using bai by (force simp: algebra_simps)
  2471         ultimately show ?thesis by auto
  2472       qed
  2473     qed
  2474   next
  2475     show "\<And>u v. cbox u v \<in> ?D0 \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
  2476       by (force simp: eq_cbox box_eq_empty field_simps dest!: aibi)
  2477   next
  2478     obtain j::'a where "j \<in> Basis"
  2479       using nonempty_Basis by blast
  2480     have "finite {L \<in> ?D0. ?K0(n,f) \<subseteq> L}" if "f \<in> Basis \<rightarrow>\<^sub>E {..<2 ^ n}" for n f
  2481     proof (rule finite_subset)
  2482       let ?B = "(\<lambda>(n, f::'a\<Rightarrow>nat). cbox (\<Sum>i\<in>Basis. (a \<bullet> i + (f i) / 2^n * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i)
  2483                                         (\<Sum>i\<in>Basis. (a \<bullet> i + ((f i) + 1) / 2^n * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i))
  2484                 ` (SIGMA m:atMost n. Pi\<^sub>E Basis (\<lambda>i::'a. lessThan (2^m)))"
  2485       have "?K0(m,g) \<in> ?B" if "g \<in> Basis \<rightarrow>\<^sub>E {..<2 ^ m}" "?K0(n,f) \<subseteq> ?K0(m,g)" for m g
  2486       proof -
  2487         have dd: "w / m \<le> v / n \<and> (v+1) / n \<le> (w+1) / m
  2488                   \<Longrightarrow> inverse n \<le> inverse m" for w m v n::real
  2489           by (auto simp: divide_simps algebra_simps)
  2490         have bjaj: "b \<bullet> j - a \<bullet> j > 0"
  2491           using \<open>j \<in> Basis\<close> \<open>box a b \<noteq> {}\<close> box_eq_empty(1) by fastforce
  2492         have "((g j) / 2 ^ m) * (b \<bullet> j - a \<bullet> j) \<le> ((f j) / 2 ^ n) * (b \<bullet> j - a \<bullet> j) \<and>
  2493               (((f j) + 1) / 2 ^ n) * (b \<bullet> j - a \<bullet> j) \<le> (((g j) + 1) / 2 ^ m) * (b \<bullet> j - a \<bullet> j)"
  2494           using that \<open>j \<in> Basis\<close> by (simp add: subset_box algebra_simps divide_simps aibi)
  2495         then have "((g j) / 2 ^ m) \<le> ((f j) / 2 ^ n) \<and>
  2496           ((real(f j) + 1) / 2 ^ n) \<le> ((real(g j) + 1) / 2 ^ m)"
  2497           by (metis bjaj mult.commute of_nat_1 of_nat_add real_mult_le_cancel_iff2)
  2498         then have "inverse (2^n) \<le> (inverse (2^m) :: real)"
  2499           by (rule dd)
  2500         then have "m \<le> n"
  2501           by auto
  2502         show ?thesis
  2503           by (rule imageI) (simp add: \<open>m \<le> n\<close> that)
  2504       qed
  2505       then show "{L \<in> ?D0. ?K0(n,f) \<subseteq> L} \<subseteq> ?B"
  2506         by auto
  2507       show "finite ?B"
  2508         by (intro finite_imageI finite_SigmaI finite_atMost finite_lessThan finite_PiE finite_Basis)
  2509     qed
  2510     then show "finite {L \<in> ?D0. K \<subseteq> L}" if "K \<in> ?D0" for K
  2511       using that by auto
  2512   qed
  2513   let ?D1 = "{K \<in> \<D>0. \<exists>x \<in> S \<inter> K. K \<subseteq> g x}"
  2514   obtain \<D> where count: "countable \<D>"
  2515              and sub: "\<Union>\<D> \<subseteq> cbox a b"  "S \<subseteq> \<Union>\<D>"
  2516              and int:  "\<And>K. K \<in> \<D> \<Longrightarrow> (interior K \<noteq> {}) \<and> (\<exists>c d. K = cbox c d)"
  2517              and intdj: "\<And>A B. \<lbrakk>A \<in> \<D>; B \<in> \<D>\<rbrakk> \<Longrightarrow> A \<subseteq> B \<or> B \<subseteq> A \<or> interior A \<inter> interior B = {}"
  2518              and SK: "\<And>K. K \<in> \<D> \<Longrightarrow> \<exists>x. x \<in> S \<inter> K \<and> K \<subseteq> g x"
  2519              and cbox: "\<And>u v. cbox u v \<in> \<D> \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
  2520              and fin: "\<And>K. K \<in> \<D> \<Longrightarrow> finite {L. L \<in> \<D> \<and> K \<subseteq> L}"
  2521   proof
  2522     show "countable ?D1" using count countable_subset
  2523       by (simp add: count countable_subset)
  2524     show "\<Union>?D1 \<subseteq> cbox a b"
  2525       using sub by blast
  2526     show "S \<subseteq> \<Union>?D1"
  2527       using SK by (force simp:)
  2528     show "\<And>K. K \<in> ?D1 \<Longrightarrow> (interior K \<noteq> {}) \<and> (\<exists>c d. K = cbox c d)"
  2529       using int by blast
  2530     show "\<And>A B. \<lbrakk>A \<in> ?D1; B \<in> ?D1\<rbrakk> \<Longrightarrow> A \<subseteq> B \<or> B \<subseteq> A \<or> interior A \<inter> interior B = {}"
  2531       using intdj by blast
  2532     show "\<And>K. K \<in> ?D1 \<Longrightarrow> \<exists>x. x \<in> S \<inter> K \<and> K \<subseteq> g x"
  2533       by auto
  2534     show "\<And>u v. cbox u v \<in> ?D1 \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
  2535       using cbox by blast
  2536     show "\<And>K. K \<in> ?D1 \<Longrightarrow> finite {L. L \<in> ?D1 \<and> K \<subseteq> L}"
  2537       using fin by simp (metis (mono_tags, lifting) Collect_mono rev_finite_subset)
  2538   qed
  2539   let ?\<D> = "{K \<in> \<D>. \<forall>K'. K' \<in> \<D> \<and> K \<noteq> K' \<longrightarrow> \<not>(K \<subseteq> K')}"
  2540   show ?thesis
  2541   proof (rule that)
  2542     show "countable ?\<D>"
  2543       by (blast intro: countable_subset [OF _ count])
  2544     show "\<Union>?\<D> \<subseteq> cbox a b"
  2545       using sub by blast
  2546     show "S \<subseteq> \<Union>?\<D>"
  2547     proof clarsimp
  2548       fix x
  2549       assume "x \<in> S"
  2550       then obtain X where "x \<in> X" "X \<in> \<D>" using \<open>S \<subseteq> \<Union>\<D>\<close> by blast
  2551       let ?R = "{(K,L). K \<in> \<D> \<and> L \<in> \<D> \<and> L \<subset> K}"
  2552       have irrR: "irrefl ?R" by (force simp: irrefl_def)
  2553       have traR: "trans ?R" by (force simp: trans_def)
  2554       have finR: "\<And>x. finite {y. (y, x) \<in> ?R}"
  2555         by simp (metis (mono_tags, lifting) fin \<open>X \<in> \<D>\<close> finite_subset mem_Collect_eq psubset_imp_subset subsetI)
  2556       have "{X \<in> \<D>. x \<in> X} \<noteq> {}"
  2557         using \<open>X \<in> \<D>\<close> \<open>x \<in> X\<close> by blast
  2558       then obtain Y where "Y \<in> {X \<in> \<D>. x \<in> X}" "\<And>Y'. (Y', Y) \<in> ?R \<Longrightarrow> Y' \<notin> {X \<in> \<D>. x \<in> X}"
  2559         by (rule wfE_min' [OF wf_finite_segments [OF irrR traR finR]]) blast
  2560       then show "\<exists>Y. Y \<in> \<D> \<and> (\<forall>K'. K' \<in> \<D> \<and> Y \<noteq> K' \<longrightarrow> \<not> Y \<subseteq> K') \<and> x \<in> Y"
  2561         by blast
  2562     qed
  2563     show "\<And>K. K \<in> ?\<D> \<Longrightarrow> interior K \<noteq> {} \<and> (\<exists>c d. K = cbox c d)"
  2564       by (blast intro: dest: int)
  2565     show "pairwise (\<lambda>A B. interior A \<inter> interior B = {}) ?\<D>"
  2566       using intdj by (simp add: pairwise_def) metis
  2567     show "\<And>K. K \<in> ?\<D> \<Longrightarrow> \<exists>x \<in> S \<inter> K. K \<subseteq> g x"
  2568       using SK by force
  2569     show "\<And>u v. cbox u v \<in> ?\<D> \<Longrightarrow> \<exists>n. \<forall>i\<in>Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
  2570       using cbox by force
  2571     qed
  2572 qed
  2573 
  2574 subsection%important \<open>Division filter\<close>
  2575 
  2576 text \<open>Divisions over all gauges towards finer divisions.\<close>
  2577 
  2578 definition%important division_filter :: "'a::euclidean_space set \<Rightarrow> ('a \<times> 'a set) set filter"
  2579   where "division_filter s = (INF g\<in>{g. gauge g}. principal {p. p tagged_division_of s \<and> g fine p})"
  2580 
  2581 lemma%important eventually_division_filter:
  2582   "(\<forall>\<^sub>F p in division_filter s. P p) \<longleftrightarrow>
  2583     (\<exists>g. gauge g \<and> (\<forall>p. p tagged_division_of s \<and> g fine p \<longrightarrow> P p))"
  2584   unfolding%unimportant division_filter_def
  2585 proof%unimportant (subst eventually_INF_base; clarsimp)
  2586   fix g1 g2 :: "'a \<Rightarrow> 'a set" show "gauge g1 \<Longrightarrow> gauge g2 \<Longrightarrow> \<exists>x. gauge x \<and>
  2587     {p. p tagged_division_of s \<and> x fine p} \<subseteq> {p. p tagged_division_of s \<and> g1 fine p} \<and>
  2588     {p. p tagged_division_of s \<and> x fine p} \<subseteq> {p. p tagged_division_of s \<and> g2 fine p}"
  2589     by (intro exI[of _ "\<lambda>x. g1 x \<inter> g2 x"]) (auto simp: fine_Int)
  2590 qed (auto simp: eventually_principal)
  2591 
  2592 lemma division_filter_not_empty: "division_filter (cbox a b) \<noteq> bot"
  2593   unfolding trivial_limit_def eventually_division_filter
  2594   by (auto elim: fine_division_exists)
  2595 
  2596 lemma%important eventually_division_filter_tagged_division:
  2597   "eventually (\<lambda>p. p tagged_division_of s) (division_filter s)"
  2598   unfolding eventually_division_filter by (intro exI[of _ "\<lambda>x. ball x 1"]) auto
  2599 
  2600 end