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
```