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