src/HOL/Analysis/Tagged_Division.thy
author paulson <lp15@cam.ac.uk>
Tue May 08 10:32:07 2018 +0100 (17 months ago)
changeset 68120 2f161c6910f7
parent 67968 a5ad4c015d1c
child 68302 b6567edf3b3d
permissions -rw-r--r--
tidying more messy proofs
     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 \<open>Tagged divisions used for the Henstock-Kurzweil gauge integration\<close>
     7 
     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 \<open>Sundries\<close>
    35 
    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 \<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 \<open>Bounds on intervals where they exist\<close>
   134 
   135 definition interval_upperbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
   136   where "interval_upperbound s = (\<Sum>i\<in>Basis. (SUP x:s. x\<bullet>i) *\<^sub>R i)"
   137 
   138 definition interval_lowerbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
   139   where "interval_lowerbound s = (\<Sum>i\<in>Basis. (INF x: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
   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 (auto simp: interval_upperbound_def interval_lowerbound_def)
   160 
   161 lemma 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 assms unfolding box_ne_empty by auto
   166 
   167 lemma 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-
   171   from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
   172   have "(\<Sum>i\<in>Basis. (SUP x:A \<times> B. x \<bullet> (i, 0)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (SUP x: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:A \<times> B. x \<bullet> (0, i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (SUP x: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 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-
   185   from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
   186   have "(\<Sum>i\<in>Basis. (INF x:A \<times> B. x \<bullet> (i, 0)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (INF x: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:A \<times> B. x \<bullet> (0, i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (INF x: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 \<open>The notion of a gauge --- simply an open set containing the point\<close>
   196 
   197 definition "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 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 -
   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 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 (metis zero_less_one)
   244 
   245 subsection \<open>Attempt a systematic general set of "offset" results for components\<close>
   246 
   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 \<open>Divisions\<close>
   253 
   254 definition 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 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 (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 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 (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 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 (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 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 -
   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 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 -
   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 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 (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 \<open>Tagged (partial) divisions\<close>
   999 
  1000 definition 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 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 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 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 division_of_tagged_division:
  1056   assumes "s tagged_division_of i"
  1057   shows "(snd ` s) division_of i"
  1058 proof (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 partial_division_of_tagged_division:
  1077   assumes "s tagged_partial_division_of i"
  1078   shows "(snd ` s) division_of \<Union>(snd ` s)"
  1079 proof (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 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 (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 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 (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 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 -
  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 (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 -
  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 \<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 \<open>Using additivity of lifted function to encode definedness.\<close>
  1296 
  1297 definition 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 comm_monoid_lift_option:
  1308   assumes "comm_monoid f z"
  1309   shows "comm_monoid (lift_option f) (Some z)"
  1310 proof -
  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 "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 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 -
  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 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> ~(l \<inter> {x. x\<bullet>k \<ge> c} = {})} \<subseteq>
  1364       division_points (cbox a b) d" (is ?t2)
  1365 proof -
  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 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 -
  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 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 -
  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 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 -
  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 division:
  1564   "F g d = g (cbox a b)" if "d division_of (cbox a b)"
  1565 proof -
  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 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 -
  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 \<open>Special case of additivity we need for the FTC\<close>
  1832 
  1833 lemma 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 -
  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 \<open>Fine-ness of a partition w.r.t. a gauge\<close>
  1860 
  1861 definition 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 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 fine_subset: "p \<subseteq> q \<Longrightarrow> d fine q \<Longrightarrow> d fine p"
  1888   unfolding fine_def by blast
  1889 
  1890 subsection \<open>Some basic combining lemmas\<close>
  1891 
  1892 lemma 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 -
  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 
  1909 
  1910 subsection \<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 \<open>General bisection principle for intervals; might be useful elsewhere\<close>
  1918 
  1919 lemma 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 -
  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 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 -
  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 "\<exists>a. \<forall>n. a\<in> cbox (A n) (B n)"
  2151   proof (rule decreasing_closed_nest)
  2152     show "\<forall>n. closed (cbox (A n) (B n))"
  2153       by (simp add: closed_cbox)
  2154     show "\<forall>n. cbox (A n) (B n) \<noteq> {}"
  2155       by (meson AB dual_order.trans interval_not_empty)
  2156   qed (use ABsubset interv in auto)
  2157   then obtain x0 where x0: "\<And>n. x0 \<in> cbox (A n) (B n)"
  2158     by blast
  2159   show thesis
  2160   proof (rule that[rule_format, of x0])
  2161     show "x0\<in>cbox a b"
  2162       using \<open>A 0 = a\<close> \<open>B 0 = b\<close> x0 by blast
  2163     fix e :: real
  2164     assume "e > 0"
  2165     from interv[OF this] obtain n
  2166       where n: "\<forall>x\<in>cbox (A n) (B n). \<forall>y\<in>cbox (A n) (B n). dist x y < e" ..
  2167     have "\<not> P (cbox (A n) (B n))"
  2168     proof (cases "0 < n")
  2169       case True then show ?thesis 
  2170         by (metis Suc_pred' notPAB) 
  2171     next
  2172       case False then show ?thesis
  2173         using \<open>A 0 = a\<close> \<open>B 0 = b\<close> \<open>\<not> P (cbox a b)\<close> by blast
  2174     qed
  2175     moreover have "cbox (A n) (B n) \<subseteq> ball x0 e"
  2176       using n using x0[of n] by auto
  2177     moreover have "cbox (A n) (B n) \<subseteq> cbox a b"
  2178       using ABsubset \<open>A 0 = a\<close> \<open>B 0 = b\<close> by blast
  2179     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)"
  2180       apply (rule_tac x="A n" in exI)
  2181       apply (rule_tac x="B n" in exI)
  2182       apply (auto simp: x0)
  2183       done
  2184   qed
  2185 qed
  2186 
  2187 
  2188 subsection \<open>Cousin's lemma\<close>
  2189 
  2190 lemma fine_division_exists:
  2191   fixes a b :: "'a::euclidean_space"
  2192   assumes "gauge g"
  2193   obtains p where "p tagged_division_of (cbox a b)" "g fine p"
  2194 proof (cases "\<exists>p. p tagged_division_of (cbox a b) \<and> g fine p")
  2195   case True
  2196   then show ?thesis
  2197     using that by auto
  2198 next
  2199   case False
  2200   assume "\<not> (\<exists>p. p tagged_division_of (cbox a b) \<and> g fine p)"
  2201   obtain x where x:
  2202       "x \<in> (cbox a b)"
  2203       "\<And>e. 0 < e \<Longrightarrow>
  2204         \<exists>c d.
  2205           x \<in> cbox c d \<and>
  2206           cbox c d \<subseteq> ball x e \<and>
  2207           cbox c d \<subseteq> (cbox a b) \<and>
  2208           \<not> (\<exists>p. p tagged_division_of cbox c d \<and> g fine p)"
  2209     apply (rule interval_bisection[of "\<lambda>s. \<exists>p. p tagged_division_of s \<and> g fine p", OF _ _ False])
  2210     apply (simp add: fine_def)
  2211     apply (metis tagged_division_Un fine_Un)
  2212     apply auto
  2213     done
  2214   obtain e where e: "e > 0" "ball x e \<subseteq> g x"
  2215     using gaugeD[OF assms, of x] unfolding open_contains_ball by auto
  2216   from x(2)[OF e(1)]
  2217   obtain c d where c_d: "x \<in> cbox c d"
  2218                         "cbox c d \<subseteq> ball x e"
  2219                         "cbox c d \<subseteq> cbox a b"
  2220                         "\<not> (\<exists>p. p tagged_division_of cbox c d \<and> g fine p)"
  2221     by blast
  2222   have "g fine {(x, cbox c d)}"
  2223     unfolding fine_def using e using c_d(2) by auto
  2224   then show ?thesis
  2225     using tagged_division_of_self[OF c_d(1)] using c_d by auto
  2226 qed
  2227 
  2228 lemma fine_division_exists_real:
  2229   fixes a b :: real
  2230   assumes "gauge g"
  2231   obtains p where "p tagged_division_of {a .. b}" "g fine p"
  2232   by (metis assms box_real(2) fine_division_exists)
  2233 
  2234 subsection \<open>A technical lemma about "refinement" of division\<close>
  2235 
  2236 lemma tagged_division_finer:
  2237   fixes p :: "('a::euclidean_space \<times> ('a::euclidean_space set)) set"
  2238   assumes ptag: "p tagged_division_of (cbox a b)"
  2239     and "gauge d"
  2240   obtains q where "q tagged_division_of (cbox a b)"
  2241     and "d fine q"
  2242     and "\<forall>(x,k) \<in> p. k \<subseteq> d(x) \<longrightarrow> (x,k) \<in> q"
  2243 proof -
  2244   have p: "finite p" "p tagged_partial_division_of (cbox a b)"
  2245     using ptag unfolding tagged_division_of_def by auto
  2246   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))" 
  2247     if "finite p" "p tagged_partial_division_of (cbox a b)" "gauge d" for p
  2248     using that
  2249   proof (induct p)
  2250     case empty
  2251     show ?case
  2252       by (force simp add: fine_def)
  2253   next
  2254     case (insert xk p)
  2255     obtain x k where xk: "xk = (x, k)"
  2256       using surj_pair[of xk] by metis 
  2257     obtain q1 where q1: "q1 tagged_division_of \<Union>{k. \<exists>x. (x, k) \<in> p}"
  2258                 and "d fine q1"
  2259                 and q1I: "\<And>x k. \<lbrakk>(x, k)\<in>p;  k \<subseteq> d x\<rbrakk> \<Longrightarrow> (x, k) \<in> q1"
  2260       using case_prodD tagged_partial_division_subset[OF insert(4) subset_insertI]
  2261       by (metis (mono_tags, lifting) insert.hyps(3) insert.prems(2))
  2262     have *: "\<Union>{l. \<exists>y. (y,l) \<in> insert xk p} = k \<union> \<Union>{l. \<exists>y. (y,l) \<in> p}"
  2263       unfolding xk by auto
  2264     note p = tagged_partial_division_ofD[OF insert(4)]
  2265     obtain u v where uv: "k = cbox u v"
  2266       using p(4) xk by blast
  2267     have "finite {k. \<exists>x. (x, k) \<in> p}"
  2268       apply (rule finite_subset[of _ "snd ` p"])
  2269       using image_iff apply fastforce
  2270       using insert.hyps(1) by blast
  2271     then have int: "interior (cbox u v) \<inter> interior (\<Union>{k. \<exists>x. (x, k) \<in> p}) = {}"
  2272     proof (rule Int_interior_Union_intervals)
  2273       show "open (interior (cbox u v))"
  2274         by auto
  2275       show "\<And>T. T \<in> {k. \<exists>x. (x, k) \<in> p} \<Longrightarrow> \<exists>a b. T = cbox a b"
  2276         using p(4) by auto
  2277       show "\<And>T. T \<in> {k. \<exists>x. (x, k) \<in> p} \<Longrightarrow> interior (cbox u v) \<inter> interior T = {}"
  2278         by clarify (metis insert.hyps(2) insert_iff interior_cbox p(5) uv xk)
  2279     qed
  2280     show ?case
  2281     proof (cases "cbox u v \<subseteq> d x")
  2282       case True
  2283       have "{(x, cbox u v)} tagged_division_of cbox u v"
  2284         by (simp add: p(2) uv xk tagged_division_of_self)
  2285       then have "{(x, cbox u v)} \<union> q1 tagged_division_of \<Union>{k. \<exists>x. (x, k) \<in> insert xk p}"
  2286         unfolding * uv by (metis (no_types, lifting) int q1 tagged_division_Un)
  2287       with True show ?thesis
  2288         apply (rule_tac x="{(x,cbox u v)} \<union> q1" in exI)
  2289         using \<open>d fine q1\<close> fine_def q1I uv xk apply fastforce
  2290         done
  2291     next
  2292       case False
  2293       obtain q2 where q2: "q2 tagged_division_of cbox u v" "d fine q2"
  2294         using fine_division_exists[OF assms(2)] by blast
  2295       show ?thesis
  2296         apply (rule_tac x="q2 \<union> q1" in exI)
  2297         apply (intro conjI)
  2298         unfolding * uv
  2299         apply (rule tagged_division_Un q2 q1 int fine_Un)+
  2300           apply (auto intro: q1 q2 fine_Un \<open>d fine q1\<close> simp add: False q1I uv xk)
  2301         done
  2302     qed
  2303   qed
  2304   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"
  2305     by (meson \<open>gauge d\<close>)
  2306   with ptag that show ?thesis by auto
  2307 qed
  2308 
  2309 subsubsection \<open>Covering lemma\<close>
  2310 
  2311 text\<open> Some technical lemmas used in the approximation results that follow. Proof of the covering
  2312   lemma is an obvious multidimensional generalization of Lemma 3, p65 of Swartz's
  2313   "Introduction to Gauge Integrals". \<close>
  2314 
  2315 proposition covering_lemma:
  2316   assumes "S \<subseteq> cbox a b" "box a b \<noteq> {}" "gauge g"
  2317   obtains \<D> where
  2318     "countable \<D>"  "\<Union>\<D> \<subseteq> cbox a b"
  2319     "\<And>K. K \<in> \<D> \<Longrightarrow> interior K \<noteq> {} \<and> (\<exists>c d. K = cbox c d)"
  2320     "pairwise (\<lambda>A B. interior A \<inter> interior B = {}) \<D>"
  2321     "\<And>K. K \<in> \<D> \<Longrightarrow> \<exists>x \<in> S \<inter> K. K \<subseteq> g x"
  2322     "\<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"
  2323     "S \<subseteq> \<Union>\<D>"
  2324 proof -
  2325   have aibi: "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i" and normab: "0 < norm(b - a)"
  2326     using \<open>box a b \<noteq> {}\<close> box_eq_empty box_sing by fastforce+
  2327   let ?K0 = "\<lambda>(n, f::'a\<Rightarrow>nat).
  2328                     cbox (\<Sum>i \<in> Basis. (a \<bullet> i + (f i / 2^n) * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i)
  2329                          (\<Sum>i \<in> Basis. (a \<bullet> i + ((f i + 1) / 2^n) * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i)"
  2330   let ?D0 = "?K0 ` (SIGMA n:UNIV. Pi\<^sub>E Basis (\<lambda>i::'a. lessThan (2^n)))"
  2331   obtain \<D>0 where count: "countable \<D>0"
  2332              and sub: "\<Union>\<D>0 \<subseteq> cbox a b"
  2333              and int:  "\<And>K. K \<in> \<D>0 \<Longrightarrow> (interior K \<noteq> {}) \<and> (\<exists>c d. K = cbox c d)"
  2334              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 = {}"
  2335              and SK: "\<And>x. x \<in> S \<Longrightarrow> \<exists>K \<in> \<D>0. x \<in> K \<and> K \<subseteq> g x"
  2336              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"
  2337              and fin: "\<And>K. K \<in> \<D>0 \<Longrightarrow> finite {L \<in> \<D>0. K \<subseteq> L}"
  2338   proof
  2339     show "countable ?D0"
  2340       by (simp add: countable_PiE)
  2341   next
  2342     show "\<Union>?D0 \<subseteq> cbox a b"
  2343       apply (simp add: UN_subset_iff)
  2344       apply (intro conjI allI ballI subset_box_imp)
  2345        apply (simp add: divide_simps zero_le_mult_iff aibi)
  2346       apply (force simp: aibi scaling_mono nat_less_real_le dest: PiE_mem)
  2347       done
  2348   next
  2349     show "\<And>K. K \<in> ?D0 \<Longrightarrow> interior K \<noteq> {} \<and> (\<exists>c d. K = cbox c d)"
  2350       using \<open>box a b \<noteq> {}\<close>
  2351       by (clarsimp simp: box_eq_empty) (fastforce simp add: divide_simps dest: PiE_mem)
  2352   next
  2353     have realff: "(real w) * 2^m < (real v) * 2^n \<longleftrightarrow> w * 2^m < v * 2^n" for m n v w
  2354       using of_nat_less_iff less_imp_of_nat_less by fastforce
  2355     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)) = {}"
  2356       for m n \<comment> \<open>The symmetry argument requires a single HOL formula\<close>
  2357     proof (rule linorder_wlog [where a=m and b=n], intro allI impI)
  2358       fix v w m and n::nat
  2359       assume "m \<le> n" \<comment> \<open>WLOG we can assume @{term"m \<le> n"}, when the first disjunct becomes impossible\<close>
  2360       have "?K0(n,w) \<subseteq> ?K0(m,v) \<or> interior(?K0(m,v)) \<inter> interior(?K0(n,w)) = {}"
  2361         apply (simp add: subset_box disjoint_interval)
  2362         apply (rule ccontr)
  2363         apply (clarsimp simp add: aibi mult_le_cancel_right divide_le_cancel not_less not_le)
  2364         apply (drule_tac x=i in bspec, assumption)
  2365         using \<open>m\<le>n\<close> realff [of _ _ "1+_"] realff [of "1+_"_ "1+_"]
  2366         apply (auto simp: divide_simps add.commute not_le nat_le_iff_add realff)
  2367         apply (simp add: power_add, metis (no_types, hide_lams) mult_Suc mult_less_cancel2 not_less_eq mult.assoc)+
  2368         done
  2369       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)) = {}"
  2370         by meson
  2371     qed auto
  2372     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 = {}"
  2373       apply (erule imageE SigmaE)+
  2374       using * by simp
  2375   next
  2376     show "\<exists>K \<in> ?D0. x \<in> K \<and> K \<subseteq> g x" if "x \<in> S" for x
  2377     proof (simp only: bex_simps split_paired_Bex_Sigma)
  2378       show "\<exists>n. \<exists>f \<in> Basis \<rightarrow>\<^sub>E {..<2 ^ n}. x \<in> ?K0(n,f) \<and> ?K0(n,f) \<subseteq> g x"
  2379       proof -
  2380         obtain e where "0 < e"
  2381                    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"
  2382         proof -
  2383           have "x \<in> g x" "open (g x)"
  2384             using \<open>gauge g\<close> by (auto simp: gauge_def)
  2385           then obtain \<epsilon> where "0 < \<epsilon>" and \<epsilon>: "ball x \<epsilon> \<subseteq> g x"
  2386             using openE by blast
  2387           have "norm (x - y) < \<epsilon>"
  2388                if "(\<And>i. i \<in> Basis \<Longrightarrow> \<bar>x \<bullet> i - y \<bullet> i\<bar> \<le> \<epsilon> / (2 * real DIM('a)))" for y
  2389           proof -
  2390             have "norm (x - y) \<le> (\<Sum>i\<in>Basis. \<bar>x \<bullet> i - y \<bullet> i\<bar>)"
  2391               by (metis (no_types, lifting) inner_diff_left norm_le_l1 sum.cong)
  2392             also have "... \<le> DIM('a) * (\<epsilon> / (2 * real DIM('a)))"
  2393               by (meson sum_bounded_above that)
  2394             also have "... = \<epsilon> / 2"
  2395               by (simp add: divide_simps)
  2396             also have "... < \<epsilon>"
  2397               by (simp add: \<open>0 < \<epsilon>\<close>)
  2398             finally show ?thesis .
  2399           qed
  2400           then show ?thesis
  2401             by (rule_tac e = "\<epsilon> / 2 / DIM('a)" in that) (simp_all add:  \<open>0 < \<epsilon>\<close> dist_norm subsetD [OF \<epsilon>])
  2402         qed
  2403         have xab: "x \<in> cbox a b"
  2404           using \<open>x \<in> S\<close> \<open>S \<subseteq> cbox a b\<close> by blast
  2405         obtain n where n: "norm (b - a) / 2^n < e"
  2406           using real_arch_pow_inv [of "e / norm(b - a)" "1/2"] normab \<open>0 < e\<close>
  2407           by (auto simp: divide_simps)
  2408         then have "norm (b - a) < e * 2^n"
  2409           by (auto simp: divide_simps)
  2410         then have bai: "b \<bullet> i - a \<bullet> i < e * 2 ^ n" if "i \<in> Basis" for i
  2411         proof -
  2412           have "b \<bullet> i - a \<bullet> i \<le> norm (b - a)"
  2413             by (metis abs_of_nonneg dual_order.trans inner_diff_left linear norm_ge_zero Basis_le_norm that)
  2414           also have "... < e * 2 ^ n"
  2415             using \<open>norm (b - a) < e * 2 ^ n\<close> by blast
  2416           finally show ?thesis .
  2417         qed
  2418         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"
  2419                  for a m n x and y::real
  2420           by auto
  2421         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>
  2422                x \<bullet> i \<le> a \<bullet> i + (real k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n)"
  2423         proof
  2424           fix i::'a assume "i \<in> Basis"
  2425           consider "x \<bullet> i = b \<bullet> i" | "x \<bullet> i < b \<bullet> i"
  2426             using \<open>i \<in> Basis\<close> mem_box(2) xab by force
  2427           then show "\<exists>k<2 ^ n. (a \<bullet> i + real k * (b \<bullet> i - a \<bullet> i) / 2 ^ n \<le> x \<bullet> i \<and>
  2428                           x \<bullet> i \<le> a \<bullet> i + (real k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n)"
  2429           proof cases
  2430             case 1 then show ?thesis
  2431               by (rule_tac x = "2^n - 1" in exI) (auto simp: algebra_simps divide_simps of_nat_diff \<open>i \<in> Basis\<close> aibi)
  2432           next
  2433             case 2
  2434             then have abi_less: "a \<bullet> i < b \<bullet> i"
  2435               using \<open>i \<in> Basis\<close> xab by (auto simp: mem_box)
  2436             let ?k = "nat \<lfloor>2 ^ n * (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)\<rfloor>"
  2437             show ?thesis
  2438             proof (intro exI conjI)
  2439               show "?k < 2 ^ n"
  2440                 using aibi xab \<open>i \<in> Basis\<close>
  2441                 by (force simp: nat_less_iff floor_less_iff divide_simps 2 mem_box)
  2442             next
  2443               have "a \<bullet> i + real ?k * (b \<bullet> i - a \<bullet> i) / 2 ^ n \<le>
  2444                     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"
  2445                 apply (intro add_left_mono mult_right_mono divide_right_mono of_nat_floor)
  2446                 using aibi [OF \<open>i \<in> Basis\<close>] xab 2
  2447                   apply (simp_all add: \<open>i \<in> Basis\<close> mem_box divide_simps)
  2448                 done
  2449               also have "... = x \<bullet> i"
  2450                 using abi_less by (simp add: divide_simps)
  2451               finally show "a \<bullet> i + real ?k * (b \<bullet> i - a \<bullet> i) / 2 ^ n \<le> x \<bullet> i" .
  2452             next
  2453               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"
  2454                 using abi_less by (simp add: divide_simps algebra_simps)
  2455               also have "... \<le> a \<bullet> i + (real ?k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n"
  2456                 apply (intro add_left_mono mult_right_mono divide_right_mono of_nat_floor)
  2457                 using aibi [OF \<open>i \<in> Basis\<close>] xab
  2458                   apply (auto simp: \<open>i \<in> Basis\<close> mem_box divide_simps)
  2459                 done
  2460               finally show "x \<bullet> i \<le> a \<bullet> i + (real ?k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n" .
  2461             qed
  2462           qed
  2463         qed
  2464         then have "\<exists>f\<in>Basis \<rightarrow>\<^sub>E {..<2 ^ n}. x \<in> ?K0(n,f)"
  2465           apply (simp add: mem_box Bex_def)
  2466           apply (clarify dest!: bchoice)
  2467           apply (rule_tac x="restrict f Basis" in exI, simp)
  2468           done
  2469         moreover have "\<And>f. x \<in> ?K0(n,f) \<Longrightarrow> ?K0(n,f) \<subseteq> g x"
  2470           apply (clarsimp simp add: mem_box)
  2471           apply (rule e)
  2472           apply (drule bspec D, assumption)+
  2473           apply (erule order_trans)
  2474           apply (simp add: divide_simps)
  2475           using bai by (force simp: algebra_simps)
  2476         ultimately show ?thesis by auto
  2477       qed
  2478     qed
  2479   next
  2480     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"
  2481       by (force simp: eq_cbox box_eq_empty field_simps dest!: aibi)
  2482   next
  2483     obtain j::'a where "j \<in> Basis"
  2484       using nonempty_Basis by blast
  2485     have "finite {L \<in> ?D0. ?K0(n,f) \<subseteq> L}" if "f \<in> Basis \<rightarrow>\<^sub>E {..<2 ^ n}" for n f
  2486     proof (rule finite_subset)
  2487       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)
  2488                                         (\<Sum>i\<in>Basis. (a \<bullet> i + ((f i) + 1) / 2^n * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i))
  2489                 ` (SIGMA m:atMost n. Pi\<^sub>E Basis (\<lambda>i::'a. lessThan (2^m)))"
  2490       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
  2491       proof -
  2492         have dd: "w / m \<le> v / n \<and> (v+1) / n \<le> (w+1) / m
  2493                   \<Longrightarrow> inverse n \<le> inverse m" for w m v n::real
  2494           by (auto simp: divide_simps algebra_simps)
  2495         have bjaj: "b \<bullet> j - a \<bullet> j > 0"
  2496           using \<open>j \<in> Basis\<close> \<open>box a b \<noteq> {}\<close> box_eq_empty(1) by fastforce
  2497         have "((g j) / 2 ^ m) * (b \<bullet> j - a \<bullet> j) \<le> ((f j) / 2 ^ n) * (b \<bullet> j - a \<bullet> j) \<and>
  2498               (((f j) + 1) / 2 ^ n) * (b \<bullet> j - a \<bullet> j) \<le> (((g j) + 1) / 2 ^ m) * (b \<bullet> j - a \<bullet> j)"
  2499           using that \<open>j \<in> Basis\<close> by (simp add: subset_box algebra_simps divide_simps aibi)
  2500         then have "((g j) / 2 ^ m) \<le> ((f j) / 2 ^ n) \<and>
  2501           ((real(f j) + 1) / 2 ^ n) \<le> ((real(g j) + 1) / 2 ^ m)"
  2502           by (metis bjaj mult.commute of_nat_1 of_nat_add real_mult_le_cancel_iff2)
  2503         then have "inverse (2^n) \<le> (inverse (2^m) :: real)"
  2504           by (rule dd)
  2505         then have "m \<le> n"
  2506           by auto
  2507         show ?thesis
  2508           by (rule imageI) (simp add: \<open>m \<le> n\<close> that)
  2509       qed
  2510       then show "{L \<in> ?D0. ?K0(n,f) \<subseteq> L} \<subseteq> ?B"
  2511         by auto
  2512       show "finite ?B"
  2513         by (intro finite_imageI finite_SigmaI finite_atMost finite_lessThan finite_PiE finite_Basis)
  2514     qed
  2515     then show "finite {L \<in> ?D0. K \<subseteq> L}" if "K \<in> ?D0" for K
  2516       using that by auto
  2517   qed
  2518   let ?D1 = "{K \<in> \<D>0. \<exists>x \<in> S \<inter> K. K \<subseteq> g x}"
  2519   obtain \<D> where count: "countable \<D>"
  2520              and sub: "\<Union>\<D> \<subseteq> cbox a b"  "S \<subseteq> \<Union>\<D>"
  2521              and int:  "\<And>K. K \<in> \<D> \<Longrightarrow> (interior K \<noteq> {}) \<and> (\<exists>c d. K = cbox c d)"
  2522              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 = {}"
  2523              and SK: "\<And>K. K \<in> \<D> \<Longrightarrow> \<exists>x. x \<in> S \<inter> K \<and> K \<subseteq> g x"
  2524              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"
  2525              and fin: "\<And>K. K \<in> \<D> \<Longrightarrow> finite {L. L \<in> \<D> \<and> K \<subseteq> L}"
  2526   proof
  2527     show "countable ?D1" using count countable_subset
  2528       by (simp add: count countable_subset)
  2529     show "\<Union>?D1 \<subseteq> cbox a b"
  2530       using sub by blast
  2531     show "S \<subseteq> \<Union>?D1"
  2532       using SK by (force simp:)
  2533     show "\<And>K. K \<in> ?D1 \<Longrightarrow> (interior K \<noteq> {}) \<and> (\<exists>c d. K = cbox c d)"
  2534       using int by blast
  2535     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 = {}"
  2536       using intdj by blast
  2537     show "\<And>K. K \<in> ?D1 \<Longrightarrow> \<exists>x. x \<in> S \<inter> K \<and> K \<subseteq> g x"
  2538       by auto
  2539     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"
  2540       using cbox by blast
  2541     show "\<And>K. K \<in> ?D1 \<Longrightarrow> finite {L. L \<in> ?D1 \<and> K \<subseteq> L}"
  2542       using fin by simp (metis (mono_tags, lifting) Collect_mono rev_finite_subset)
  2543   qed
  2544   let ?\<D> = "{K \<in> \<D>. \<forall>K'. K' \<in> \<D> \<and> K \<noteq> K' \<longrightarrow> ~(K \<subseteq> K')}"
  2545   show ?thesis
  2546   proof (rule that)
  2547     show "countable ?\<D>"
  2548       by (blast intro: countable_subset [OF _ count])
  2549     show "\<Union>?\<D> \<subseteq> cbox a b"
  2550       using sub by blast
  2551     show "S \<subseteq> \<Union>?\<D>"
  2552     proof clarsimp
  2553       fix x
  2554       assume "x \<in> S"
  2555       then obtain X where "x \<in> X" "X \<in> \<D>" using \<open>S \<subseteq> \<Union>\<D>\<close> by blast
  2556       let ?R = "{(K,L). K \<in> \<D> \<and> L \<in> \<D> \<and> L \<subset> K}"
  2557       have irrR: "irrefl ?R" by (force simp: irrefl_def)
  2558       have traR: "trans ?R" by (force simp: trans_def)
  2559       have finR: "\<And>x. finite {y. (y, x) \<in> ?R}"
  2560         by simp (metis (mono_tags, lifting) fin \<open>X \<in> \<D>\<close> finite_subset mem_Collect_eq psubset_imp_subset subsetI)
  2561       have "{X \<in> \<D>. x \<in> X} \<noteq> {}"
  2562         using \<open>X \<in> \<D>\<close> \<open>x \<in> X\<close> by blast
  2563       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}"
  2564         by (rule wfE_min' [OF wf_finite_segments [OF irrR traR finR]]) blast
  2565       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"
  2566         by blast
  2567     qed
  2568     show "\<And>K. K \<in> ?\<D> \<Longrightarrow> interior K \<noteq> {} \<and> (\<exists>c d. K = cbox c d)"
  2569       by (blast intro: dest: int)
  2570     show "pairwise (\<lambda>A B. interior A \<inter> interior B = {}) ?\<D>"
  2571       using intdj by (simp add: pairwise_def) metis
  2572     show "\<And>K. K \<in> ?\<D> \<Longrightarrow> \<exists>x \<in> S \<inter> K. K \<subseteq> g x"
  2573       using SK by force
  2574     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"
  2575       using cbox by force
  2576     qed
  2577 qed
  2578 
  2579 subsection \<open>Division filter\<close>
  2580 
  2581 text \<open>Divisions over all gauges towards finer divisions.\<close>
  2582 
  2583 definition division_filter :: "'a::euclidean_space set \<Rightarrow> ('a \<times> 'a set) set filter"
  2584   where "division_filter s = (INF g:{g. gauge g}. principal {p. p tagged_division_of s \<and> g fine p})"
  2585 
  2586 lemma eventually_division_filter:
  2587   "(\<forall>\<^sub>F p in division_filter s. P p) \<longleftrightarrow>
  2588     (\<exists>g. gauge g \<and> (\<forall>p. p tagged_division_of s \<and> g fine p \<longrightarrow> P p))"
  2589   unfolding division_filter_def
  2590 proof (subst eventually_INF_base; clarsimp)
  2591   fix g1 g2 :: "'a \<Rightarrow> 'a set" show "gauge g1 \<Longrightarrow> gauge g2 \<Longrightarrow> \<exists>x. gauge x \<and>
  2592     {p. p tagged_division_of s \<and> x fine p} \<subseteq> {p. p tagged_division_of s \<and> g1 fine p} \<and>
  2593     {p. p tagged_division_of s \<and> x fine p} \<subseteq> {p. p tagged_division_of s \<and> g2 fine p}"
  2594     by (intro exI[of _ "\<lambda>x. g1 x \<inter> g2 x"]) (auto simp: fine_Int)
  2595 qed (auto simp: eventually_principal)
  2596 
  2597 lemma division_filter_not_empty: "division_filter (cbox a b) \<noteq> bot"
  2598   unfolding trivial_limit_def eventually_division_filter
  2599   by (auto elim: fine_division_exists)
  2600 
  2601 lemma eventually_division_filter_tagged_division:
  2602   "eventually (\<lambda>p. p tagged_division_of s) (division_filter s)"
  2603   unfolding eventually_division_filter by (intro exI[of _ "\<lambda>x. ball x 1"]) auto
  2604 
  2605 end