src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
author hoelzl
Wed Sep 28 16:15:51 2016 +0200 (2016-09-28)
changeset 63956 b235e845c8e8
parent 63945 444eafb6e864
child 63957 c3da799b1b45
permissions -rw-r--r--
HOL-Analysis: add cover lemma ported by L. C. Paulson
wenzelm@53399
     1
(*  Author:     John Harrison
lp15@60428
     2
    Author:     Robert Himmelmann, TU Muenchen (Translation from HOL light); proofs reworked by LCP
wenzelm@53399
     3
*)
wenzelm@53399
     4
hoelzl@63594
     5
section \<open>Henstock-Kurzweil gauge integration in many dimensions.\<close>
hoelzl@63594
     6
hoelzl@63594
     7
theory Henstock_Kurzweil_Integration
wenzelm@41413
     8
imports
hoelzl@63886
     9
  Lebesgue_Measure
himmelma@35172
    10
begin
himmelma@35172
    11
hoelzl@37489
    12
lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
hoelzl@37489
    13
  scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff
huffman@44282
    14
  scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one
hoelzl@37489
    15
wenzelm@49675
    16
wenzelm@60420
    17
subsection \<open>Sundries\<close>
himmelma@36243
    18
hoelzl@63956
    19
hoelzl@63956
    20
text\<open>A transitive relation is well-founded if all initial segments are finite.\<close>
hoelzl@63956
    21
lemma wf_finite_segments:
hoelzl@63956
    22
  assumes "irrefl r" and "trans r" and "\<And>x. finite {y. (y, x) \<in> r}"
hoelzl@63956
    23
  shows "wf (r)"
hoelzl@63956
    24
  apply (simp add: trans_wf_iff wf_iff_acyclic_if_finite converse_def assms)
hoelzl@63956
    25
  using acyclic_def assms irrefl_def trans_Restr by fastforce
hoelzl@63956
    26
hoelzl@63956
    27
text\<open>For creating values between @{term u} and @{term v}.\<close>
hoelzl@63956
    28
lemma scaling_mono:
hoelzl@63956
    29
  fixes u::"'a::linordered_field"
hoelzl@63956
    30
  assumes "u \<le> v" "0 \<le> r" "r \<le> s"
hoelzl@63956
    31
    shows "u + r * (v - u) / s \<le> v"
hoelzl@63956
    32
proof -
hoelzl@63956
    33
  have "r/s \<le> 1" using assms
hoelzl@63956
    34
    using divide_le_eq_1 by fastforce
hoelzl@63956
    35
  then have "(r/s) * (v - u) \<le> 1 * (v - u)"
hoelzl@63956
    36
    by (meson diff_ge_0_iff_ge mult_right_mono \<open>u \<le> v\<close>)
hoelzl@63956
    37
  then show ?thesis
hoelzl@63956
    38
    by (simp add: field_simps)
hoelzl@63956
    39
qed
hoelzl@63956
    40
himmelma@35172
    41
lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
himmelma@35172
    42
lemma conjunctD3: assumes "a \<and> b \<and> c" shows a b c using assms by auto
himmelma@35172
    43
lemma conjunctD4: assumes "a \<and> b \<and> c \<and> d" shows a b c d using assms by auto
himmelma@35172
    44
hoelzl@63886
    45
lemma cond_cases: "(P \<Longrightarrow> Q x) \<Longrightarrow> (\<not> P \<Longrightarrow> Q y) \<Longrightarrow> Q (if P then x else y)"
hoelzl@63886
    46
  by auto
hoelzl@63886
    47
wenzelm@53399
    48
declare norm_triangle_ineq4[intro]
wenzelm@53399
    49
himmelma@36243
    50
lemma transitive_stepwise_le:
hoelzl@63886
    51
  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)"
himmelma@36243
    52
  shows "\<forall>n\<ge>m. R m n"
hoelzl@63886
    53
proof (intro allI impI)
hoelzl@63886
    54
  show "m \<le> n \<Longrightarrow> R m n" for n
hoelzl@63886
    55
    by (induction rule: dec_induct)
hoelzl@63886
    56
       (use assms in blast)+
hoelzl@63886
    57
qed
himmelma@36243
    58
wenzelm@60420
    59
subsection \<open>Some useful lemmas about intervals.\<close>
himmelma@35172
    60
immler@56188
    61
lemma empty_as_interval: "{} = cbox One (0::'a::euclidean_space)"
immler@56188
    62
  using nonempty_Basis
immler@56188
    63
  by (fastforce simp add: set_eq_iff mem_box)
himmelma@35172
    64
wenzelm@53399
    65
lemma interior_subset_union_intervals:
immler@56188
    66
  assumes "i = cbox a b"
immler@56188
    67
    and "j = cbox c d"
wenzelm@53399
    68
    and "interior j \<noteq> {}"
wenzelm@53399
    69
    and "i \<subseteq> j \<union> s"
wenzelm@53399
    70
    and "interior i \<inter> interior j = {}"
wenzelm@49675
    71
  shows "interior i \<subseteq> interior s"
wenzelm@49675
    72
proof -
immler@56188
    73
  have "box a b \<inter> cbox c d = {}"
immler@56188
    74
     using inter_interval_mixed_eq_empty[of c d a b] and assms(3,5)
immler@56188
    75
     unfolding assms(1,2) interior_cbox by auto
wenzelm@49675
    76
  moreover
immler@56188
    77
  have "box a b \<subseteq> cbox c d \<union> s"
immler@56188
    78
    apply (rule order_trans,rule box_subset_cbox)
wenzelm@49970
    79
    using assms(4) unfolding assms(1,2)
wenzelm@49970
    80
    apply auto
wenzelm@49970
    81
    done
wenzelm@49675
    82
  ultimately
wenzelm@49675
    83
  show ?thesis
lp15@60384
    84
    unfolding assms interior_cbox
lp15@60384
    85
      by auto (metis IntI UnE empty_iff interior_maximal open_box subsetCE subsetI)
wenzelm@49675
    86
qed
wenzelm@49675
    87
hoelzl@63595
    88
lemma interior_Union_subset_cbox:
wenzelm@53399
    89
  assumes "finite f"
hoelzl@63595
    90
  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"
hoelzl@63595
    91
    and t: "closed t"
hoelzl@63595
    92
  shows "interior (\<Union>f) \<subseteq> t"
hoelzl@63595
    93
proof -
hoelzl@63595
    94
  have [simp]: "s \<in> f \<Longrightarrow> closed s" for s
hoelzl@63595
    95
    using f by auto
hoelzl@63595
    96
  define E where "E = {s\<in>f. interior s = {}}"
hoelzl@63595
    97
  then have "finite E" "E \<subseteq> {s\<in>f. interior s = {}}"
hoelzl@63595
    98
    using \<open>finite f\<close> by auto
hoelzl@63595
    99
  then have "interior (\<Union>f) = interior (\<Union>(f - E))"
hoelzl@63595
   100
  proof (induction E rule: finite_subset_induct')
hoelzl@63595
   101
    case (insert s f')
hoelzl@63595
   102
    have "interior (\<Union>(f - insert s f') \<union> s) = interior (\<Union>(f - insert s f'))"
hoelzl@63595
   103
      using insert.hyps \<open>finite f\<close> by (intro interior_closed_Un_empty_interior) auto
hoelzl@63595
   104
    also have "\<Union>(f - insert s f') \<union> s = \<Union>(f - f')"
hoelzl@63595
   105
      using insert.hyps by auto
hoelzl@63595
   106
    finally show ?case
hoelzl@63595
   107
      by (simp add: insert.IH)
hoelzl@63595
   108
  qed simp
hoelzl@63595
   109
  also have "\<dots> \<subseteq> \<Union>(f - E)"
hoelzl@63595
   110
    by (rule interior_subset)
hoelzl@63595
   111
  also have "\<dots> \<subseteq> t"
hoelzl@63595
   112
  proof (rule Union_least)
hoelzl@63595
   113
    fix s assume "s \<in> f - E"
hoelzl@63595
   114
    with f[of s] obtain a b where s: "s \<in> f" "s = cbox a b" "box a b \<noteq> {}"
hoelzl@63595
   115
      by (fastforce simp: E_def)
hoelzl@63595
   116
    have "closure (interior s) \<subseteq> closure t"
hoelzl@63595
   117
      by (intro closure_mono f \<open>s \<in> f\<close>)
hoelzl@63595
   118
    with s \<open>closed t\<close> show "s \<subseteq> t"
hoelzl@63595
   119
      by (simp add: closure_box)
hoelzl@63595
   120
  qed
hoelzl@63595
   121
  finally show ?thesis .
hoelzl@63595
   122
qed
hoelzl@63595
   123
hoelzl@63595
   124
lemma inter_interior_unions_intervals:
hoelzl@63595
   125
    "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) = {}"
hoelzl@63595
   126
  using interior_Union_subset_cbox[of f "UNIV - s"] by auto
wenzelm@60420
   127
hoelzl@63886
   128
lemma interval_split:
hoelzl@63886
   129
  fixes a :: "'a::euclidean_space"
hoelzl@63886
   130
  assumes "k \<in> Basis"
hoelzl@63886
   131
  shows
hoelzl@63886
   132
    "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)"
hoelzl@63886
   133
    "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"
hoelzl@63886
   134
  apply (rule_tac[!] set_eqI)
hoelzl@63886
   135
  unfolding Int_iff mem_box mem_Collect_eq
hoelzl@63886
   136
  using assms
hoelzl@63886
   137
  apply auto
hoelzl@63886
   138
  done
hoelzl@63886
   139
hoelzl@63886
   140
lemma interval_not_empty: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> cbox a b \<noteq> {}"
hoelzl@63886
   141
  by (simp add: box_ne_empty)
hoelzl@63886
   142
wenzelm@60420
   143
subsection \<open>Bounds on intervals where they exist.\<close>
immler@56188
   144
immler@56188
   145
definition interval_upperbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
immler@56188
   146
  where "interval_upperbound s = (\<Sum>i\<in>Basis. (SUP x:s. x\<bullet>i) *\<^sub>R i)"
immler@56188
   147
immler@56188
   148
definition interval_lowerbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
hoelzl@63886
   149
  where "interval_lowerbound s = (\<Sum>i\<in>Basis. (INF x:s. x\<bullet>i) *\<^sub>R i)"
immler@56188
   150
immler@56188
   151
lemma interval_upperbound[simp]:
immler@56188
   152
  "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
immler@56188
   153
    interval_upperbound (cbox a b) = (b::'a::euclidean_space)"
haftmann@62343
   154
  unfolding interval_upperbound_def euclidean_representation_setsum cbox_def
immler@56188
   155
  by (safe intro!: cSup_eq) auto
immler@56188
   156
immler@56188
   157
lemma interval_lowerbound[simp]:
immler@56188
   158
  "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
immler@56188
   159
    interval_lowerbound (cbox a b) = (a::'a::euclidean_space)"
haftmann@62343
   160
  unfolding interval_lowerbound_def euclidean_representation_setsum cbox_def
immler@56188
   161
  by (safe intro!: cInf_eq) auto
immler@56188
   162
immler@56188
   163
lemmas interval_bounds = interval_upperbound interval_lowerbound
immler@56188
   164
immler@56188
   165
lemma
immler@56188
   166
  fixes X::"real set"
immler@56188
   167
  shows interval_upperbound_real[simp]: "interval_upperbound X = Sup X"
immler@56188
   168
    and interval_lowerbound_real[simp]: "interval_lowerbound X = Inf X"
haftmann@62343
   169
  by (auto simp: interval_upperbound_def interval_lowerbound_def)
immler@56188
   170
immler@56188
   171
lemma interval_bounds'[simp]:
immler@56188
   172
  assumes "cbox a b \<noteq> {}"
immler@56188
   173
  shows "interval_upperbound (cbox a b) = b"
immler@56188
   174
    and "interval_lowerbound (cbox a b) = a"
immler@56188
   175
  using assms unfolding box_ne_empty by auto
wenzelm@53399
   176
lp15@60615
   177
lemma interval_upperbound_Times:
hoelzl@59425
   178
  assumes "A \<noteq> {}" and "B \<noteq> {}"
hoelzl@59425
   179
  shows "interval_upperbound (A \<times> B) = (interval_upperbound A, interval_upperbound B)"
hoelzl@59425
   180
proof-
hoelzl@59425
   181
  from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
hoelzl@59425
   182
  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)"
hoelzl@59425
   183
      by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
hoelzl@59425
   184
  moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp
hoelzl@59425
   185
  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)"
hoelzl@59425
   186
      by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
hoelzl@59425
   187
  ultimately show ?thesis unfolding interval_upperbound_def
hoelzl@59425
   188
      by (subst setsum_Basis_prod_eq) (auto simp add: setsum_prod)
hoelzl@59425
   189
qed
hoelzl@59425
   190
lp15@60615
   191
lemma interval_lowerbound_Times:
hoelzl@59425
   192
  assumes "A \<noteq> {}" and "B \<noteq> {}"
hoelzl@59425
   193
  shows "interval_lowerbound (A \<times> B) = (interval_lowerbound A, interval_lowerbound B)"
hoelzl@59425
   194
proof-
hoelzl@59425
   195
  from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
hoelzl@59425
   196
  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)"
hoelzl@59425
   197
      by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
hoelzl@59425
   198
  moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp
hoelzl@59425
   199
  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)"
hoelzl@59425
   200
      by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
hoelzl@59425
   201
  ultimately show ?thesis unfolding interval_lowerbound_def
hoelzl@59425
   202
      by (subst setsum_Basis_prod_eq) (auto simp add: setsum_prod)
hoelzl@59425
   203
qed
hoelzl@59425
   204
wenzelm@60420
   205
subsection \<open>Content (length, area, volume...) of an interval.\<close>
himmelma@35172
   206
hoelzl@63886
   207
abbreviation content :: "'a::euclidean_space set \<Rightarrow> real"
hoelzl@63886
   208
  where "content s \<equiv> measure lborel s"
hoelzl@63886
   209
hoelzl@63886
   210
lemma content_cbox_cases:
hoelzl@63886
   211
  "content (cbox a b) = (if \<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i then setprod (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis else 0)"
hoelzl@63886
   212
  by (simp add: measure_lborel_cbox_eq inner_diff)
hoelzl@63886
   213
hoelzl@63886
   214
lemma content_cbox: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
hoelzl@63886
   215
  unfolding content_cbox_cases by simp
hoelzl@63886
   216
hoelzl@63886
   217
lemma content_cbox': "cbox a b \<noteq> {} \<Longrightarrow> content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
hoelzl@63886
   218
  by (simp add: box_ne_empty inner_diff)
wenzelm@49970
   219
wenzelm@53408
   220
lemma content_real: "a \<le> b \<Longrightarrow> content {a..b} = b - a"
hoelzl@63886
   221
  by simp
immler@56188
   222
wenzelm@61945
   223
lemma abs_eq_content: "\<bar>y - x\<bar> = (if x\<le>y then content {x .. y} else content {y..x})"
paulson@61204
   224
  by (auto simp: content_real)
paulson@61204
   225
hoelzl@63886
   226
lemma content_singleton: "content {a} = 0"
hoelzl@63886
   227
  by simp
hoelzl@63886
   228
hoelzl@63886
   229
lemma content_unit[iff]: "content (cbox 0 (One::'a::euclidean_space)) = 1"
hoelzl@63886
   230
  by simp
hoelzl@63886
   231
hoelzl@63886
   232
lemma content_pos_le[intro]: "0 \<le> content (cbox a b)"
hoelzl@63886
   233
  by simp
hoelzl@63886
   234
hoelzl@63886
   235
corollary content_nonneg [simp]: "~ content (cbox a b) < 0"
hoelzl@63886
   236
  using not_le by blast
hoelzl@63886
   237
hoelzl@63886
   238
lemma content_pos_lt: "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i \<Longrightarrow> 0 < content (cbox a b)"
hoelzl@63886
   239
  by (auto simp: less_imp_le inner_diff box_eq_empty intro!: setprod_pos)
hoelzl@63886
   240
hoelzl@63886
   241
lemma content_eq_0: "content (cbox a b) = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i)"
hoelzl@63886
   242
  by (auto simp: content_cbox_cases not_le intro: less_imp_le antisym eq_refl)
immler@56188
   243
immler@56188
   244
lemma content_eq_0_interior: "content (cbox a b) = 0 \<longleftrightarrow> interior(cbox a b) = {}"
hoelzl@63886
   245
  unfolding content_eq_0 interior_cbox box_eq_empty by auto
hoelzl@63886
   246
hoelzl@63886
   247
lemma content_pos_lt_eq: "0 < content (cbox a (b::'a::euclidean_space)) \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
hoelzl@63886
   248
  by (auto simp add: content_cbox_cases less_le setprod_nonneg)
wenzelm@49970
   249
wenzelm@53399
   250
lemma content_empty [simp]: "content {} = 0"
hoelzl@63886
   251
  by simp
himmelma@35172
   252
paulson@60762
   253
lemma content_real_if [simp]: "content {a..b} = (if a \<le> b then b - a else 0)"
paulson@60762
   254
  by (simp add: content_real)
paulson@60762
   255
hoelzl@63886
   256
lemma content_subset: "cbox a b \<subseteq> cbox c d \<Longrightarrow> content (cbox a b) \<le> content (cbox c d)"
hoelzl@63886
   257
  unfolding measure_def
hoelzl@63886
   258
  by (intro enn2real_mono emeasure_mono) (auto simp: emeasure_lborel_cbox_eq)
immler@56188
   259
immler@56188
   260
lemma content_lt_nz: "0 < content (cbox a b) \<longleftrightarrow> content (cbox a b) \<noteq> 0"
nipkow@44890
   261
  unfolding content_pos_lt_eq content_eq_0 unfolding not_ex not_le by fastforce
himmelma@35172
   262
lp15@60615
   263
lemma content_Pair: "content (cbox (a,c) (b,d)) = content (cbox a b) * content (cbox c d)"
hoelzl@63886
   264
  unfolding measure_lborel_cbox_eq Basis_prod_def
hoelzl@63886
   265
  apply (subst setprod.union_disjoint)
hoelzl@63886
   266
  apply (auto simp: bex_Un ball_Un)
hoelzl@63886
   267
  apply (subst (1 2) setprod.reindex_nontrivial)
hoelzl@63886
   268
  apply auto
hoelzl@63886
   269
  done
lp15@60615
   270
lp15@60615
   271
lemma content_cbox_pair_eq0_D:
lp15@60615
   272
   "content (cbox (a,c) (b,d)) = 0 \<Longrightarrow> content (cbox a b) = 0 \<or> content (cbox c d) = 0"
lp15@60615
   273
  by (simp add: content_Pair)
lp15@60615
   274
hoelzl@63886
   275
lemma content_0_subset: "content(cbox a b) = 0 \<Longrightarrow> s \<subseteq> cbox a b \<Longrightarrow> content s = 0"
hoelzl@63886
   276
  using emeasure_mono[of s "cbox a b" lborel]
hoelzl@63886
   277
  by (auto simp: measure_def enn2real_eq_0_iff emeasure_lborel_cbox_eq)
hoelzl@63593
   278
hoelzl@63593
   279
lemma content_split:
hoelzl@63593
   280
  fixes a :: "'a::euclidean_space"
hoelzl@63593
   281
  assumes "k \<in> Basis"
hoelzl@63593
   282
  shows "content (cbox a b) = content(cbox a b \<inter> {x. x\<bullet>k \<le> c}) + content(cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
hoelzl@63886
   283
  -- \<open>Prove using measure theory\<close>
hoelzl@63593
   284
proof cases
hoelzl@63593
   285
  note simps = interval_split[OF assms] content_cbox_cases
hoelzl@63593
   286
  have *: "Basis = insert k (Basis - {k})" "\<And>x. finite (Basis-{x})" "\<And>x. x\<notin>Basis-{x}"
hoelzl@63593
   287
    using assms by auto
hoelzl@63593
   288
  have *: "\<And>X Y Z. (\<Prod>i\<in>Basis. Z i (if i = k then X else Y i)) = Z k X * (\<Prod>i\<in>Basis-{k}. Z i (Y i))"
hoelzl@63593
   289
    "(\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i) = (\<Prod>i\<in>Basis-{k}. b\<bullet>i - a\<bullet>i) * (b\<bullet>k - a\<bullet>k)"
hoelzl@63593
   290
    apply (subst *(1))
hoelzl@63593
   291
    defer
hoelzl@63593
   292
    apply (subst *(1))
hoelzl@63593
   293
    unfolding setprod.insert[OF *(2-)]
hoelzl@63593
   294
    apply auto
hoelzl@63593
   295
    done
hoelzl@63593
   296
  assume as: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
hoelzl@63593
   297
  moreover
hoelzl@63593
   298
  have "\<And>x. min (b \<bullet> k) c = max (a \<bullet> k) c \<Longrightarrow>
hoelzl@63593
   299
    x * (b\<bullet>k - a\<bullet>k) = x * (max (a \<bullet> k) c - a \<bullet> k) + x * (b \<bullet> k - max (a \<bullet> k) c)"
hoelzl@63593
   300
    by  (auto simp add: field_simps)
hoelzl@63593
   301
  moreover
hoelzl@63593
   302
  have **: "(\<Prod>i\<in>Basis. ((\<Sum>i\<in>Basis. (if i = k then min (b \<bullet> k) c else b \<bullet> i) *\<^sub>R i) \<bullet> i - a \<bullet> i)) =
hoelzl@63593
   303
      (\<Prod>i\<in>Basis. (if i = k then min (b \<bullet> k) c else b \<bullet> i) - a \<bullet> i)"
hoelzl@63593
   304
    "(\<Prod>i\<in>Basis. b \<bullet> i - ((\<Sum>i\<in>Basis. (if i = k then max (a \<bullet> k) c else a \<bullet> i) *\<^sub>R i) \<bullet> i)) =
hoelzl@63593
   305
      (\<Prod>i\<in>Basis. b \<bullet> i - (if i = k then max (a \<bullet> k) c else a \<bullet> i))"
hoelzl@63593
   306
    by (auto intro!: setprod.cong)
hoelzl@63593
   307
  have "\<not> a \<bullet> k \<le> c \<Longrightarrow> \<not> c \<le> b \<bullet> k \<Longrightarrow> False"
hoelzl@63593
   308
    unfolding not_le
hoelzl@63593
   309
    using as[unfolded ,rule_format,of k] assms
hoelzl@63593
   310
    by auto
hoelzl@63593
   311
  ultimately show ?thesis
hoelzl@63593
   312
    using assms
hoelzl@63593
   313
    unfolding simps **
hoelzl@63593
   314
    unfolding *(1)[of "\<lambda>i x. b\<bullet>i - x"] *(1)[of "\<lambda>i x. x - a\<bullet>i"]
hoelzl@63593
   315
    unfolding *(2)
hoelzl@63593
   316
    by auto
hoelzl@63593
   317
next
hoelzl@63593
   318
  assume "\<not> (\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
hoelzl@63593
   319
  then have "cbox a b = {}"
hoelzl@63593
   320
    unfolding box_eq_empty by (auto simp: not_le)
hoelzl@63593
   321
  then show ?thesis
hoelzl@63593
   322
    by (auto simp: not_le)
hoelzl@63593
   323
qed
hoelzl@63593
   324
wenzelm@60420
   325
subsection \<open>The notion of a gauge --- simply an open set containing the point.\<close>
himmelma@35172
   326
wenzelm@53408
   327
definition "gauge d \<longleftrightarrow> (\<forall>x. x \<in> d x \<and> open (d x))"
wenzelm@53399
   328
wenzelm@53399
   329
lemma gaugeI:
wenzelm@53399
   330
  assumes "\<And>x. x \<in> g x"
wenzelm@53399
   331
    and "\<And>x. open (g x)"
wenzelm@53399
   332
  shows "gauge g"
himmelma@35172
   333
  using assms unfolding gauge_def by auto
himmelma@35172
   334
wenzelm@53399
   335
lemma gaugeD[dest]:
wenzelm@53399
   336
  assumes "gauge d"
wenzelm@53399
   337
  shows "x \<in> d x"
wenzelm@53399
   338
    and "open (d x)"
wenzelm@49698
   339
  using assms unfolding gauge_def by auto
himmelma@35172
   340
himmelma@35172
   341
lemma gauge_ball_dependent: "\<forall>x. 0 < e x \<Longrightarrow> gauge (\<lambda>x. ball x (e x))"
wenzelm@53399
   342
  unfolding gauge_def by auto
wenzelm@53399
   343
wenzelm@53399
   344
lemma gauge_ball[intro]: "0 < e \<Longrightarrow> gauge (\<lambda>x. ball x e)"
wenzelm@53399
   345
  unfolding gauge_def by auto
himmelma@35172
   346
lp15@60466
   347
lemma gauge_trivial[intro!]: "gauge (\<lambda>x. ball x 1)"
wenzelm@49698
   348
  by (rule gauge_ball) auto
himmelma@35172
   349
wenzelm@53408
   350
lemma gauge_inter[intro]: "gauge d1 \<Longrightarrow> gauge d2 \<Longrightarrow> gauge (\<lambda>x. d1 x \<inter> d2 x)"
wenzelm@53399
   351
  unfolding gauge_def by auto
himmelma@35172
   352
wenzelm@49698
   353
lemma gauge_inters:
wenzelm@53399
   354
  assumes "finite s"
wenzelm@53399
   355
    and "\<forall>d\<in>s. gauge (f d)"
wenzelm@60585
   356
  shows "gauge (\<lambda>x. \<Inter>{f d x | d. d \<in> s})"
wenzelm@49698
   357
proof -
wenzelm@53399
   358
  have *: "\<And>x. {f d x |d. d \<in> s} = (\<lambda>d. f d x) ` s"
wenzelm@53399
   359
    by auto
wenzelm@49698
   360
  show ?thesis
wenzelm@53399
   361
    unfolding gauge_def unfolding *
wenzelm@49698
   362
    using assms unfolding Ball_def Inter_iff mem_Collect_eq gauge_def by auto
wenzelm@49698
   363
qed
wenzelm@49698
   364
wenzelm@53399
   365
lemma gauge_existence_lemma:
wenzelm@53408
   366
  "(\<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)"
wenzelm@53399
   367
  by (metis zero_less_one)
wenzelm@49698
   368
himmelma@35172
   369
wenzelm@60420
   370
subsection \<open>Divisions.\<close>
himmelma@35172
   371
wenzelm@53408
   372
definition division_of (infixl "division'_of" 40)
wenzelm@53408
   373
where
wenzelm@53399
   374
  "s division_of i \<longleftrightarrow>
wenzelm@53399
   375
    finite s \<and>
immler@56188
   376
    (\<forall>k\<in>s. k \<subseteq> i \<and> k \<noteq> {} \<and> (\<exists>a b. k = cbox a b)) \<and>
wenzelm@53399
   377
    (\<forall>k1\<in>s. \<forall>k2\<in>s. k1 \<noteq> k2 \<longrightarrow> interior(k1) \<inter> interior(k2) = {}) \<and>
wenzelm@53399
   378
    (\<Union>s = i)"
himmelma@35172
   379
wenzelm@49698
   380
lemma division_ofD[dest]:
wenzelm@49698
   381
  assumes "s division_of i"
wenzelm@53408
   382
  shows "finite s"
wenzelm@53408
   383
    and "\<And>k. k \<in> s \<Longrightarrow> k \<subseteq> i"
wenzelm@53408
   384
    and "\<And>k. k \<in> s \<Longrightarrow> k \<noteq> {}"
immler@56188
   385
    and "\<And>k. k \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b"
wenzelm@53408
   386
    and "\<And>k1 k2. k1 \<in> s \<Longrightarrow> k2 \<in> s \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior(k1) \<inter> interior(k2) = {}"
wenzelm@53408
   387
    and "\<Union>s = i"
wenzelm@49698
   388
  using assms unfolding division_of_def by auto
himmelma@35172
   389
himmelma@35172
   390
lemma division_ofI:
wenzelm@53408
   391
  assumes "finite s"
wenzelm@53408
   392
    and "\<And>k. k \<in> s \<Longrightarrow> k \<subseteq> i"
wenzelm@53408
   393
    and "\<And>k. k \<in> s \<Longrightarrow> k \<noteq> {}"
immler@56188
   394
    and "\<And>k. k \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b"
wenzelm@53408
   395
    and "\<And>k1 k2. k1 \<in> s \<Longrightarrow> k2 \<in> s \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior k1 \<inter> interior k2 = {}"
wenzelm@53399
   396
    and "\<Union>s = i"
wenzelm@53399
   397
  shows "s division_of i"
wenzelm@53399
   398
  using assms unfolding division_of_def by auto
himmelma@35172
   399
himmelma@35172
   400
lemma division_of_finite: "s division_of i \<Longrightarrow> finite s"
himmelma@35172
   401
  unfolding division_of_def by auto
himmelma@35172
   402
immler@56188
   403
lemma division_of_self[intro]: "cbox a b \<noteq> {} \<Longrightarrow> {cbox a b} division_of (cbox a b)"
himmelma@35172
   404
  unfolding division_of_def by auto
himmelma@35172
   405
wenzelm@53399
   406
lemma division_of_trivial[simp]: "s division_of {} \<longleftrightarrow> s = {}"
wenzelm@53399
   407
  unfolding division_of_def by auto
himmelma@35172
   408
wenzelm@49698
   409
lemma division_of_sing[simp]:
immler@56188
   410
  "s division_of cbox a (a::'a::euclidean_space) \<longleftrightarrow> s = {cbox a a}"
wenzelm@53399
   411
  (is "?l = ?r")
wenzelm@49698
   412
proof
wenzelm@49698
   413
  assume ?r
wenzelm@53399
   414
  moreover
lp15@60384
   415
  { fix k
lp15@60384
   416
    assume "s = {{a}}" "k\<in>s"
lp15@60384
   417
    then have "\<exists>x y. k = cbox x y"
wenzelm@50945
   418
      apply (rule_tac x=a in exI)+
lp15@60384
   419
      apply (force simp: cbox_sing)
wenzelm@50945
   420
      done
wenzelm@49698
   421
  }
wenzelm@53399
   422
  ultimately show ?l
immler@56188
   423
    unfolding division_of_def cbox_sing by auto
wenzelm@49698
   424
next
wenzelm@49698
   425
  assume ?l
immler@56188
   426
  note * = conjunctD4[OF this[unfolded division_of_def cbox_sing]]
wenzelm@53399
   427
  {
wenzelm@53399
   428
    fix x
wenzelm@53399
   429
    assume x: "x \<in> s" have "x = {a}"
wenzelm@53408
   430
      using *(2)[rule_format,OF x] by auto
wenzelm@53399
   431
  }
wenzelm@53408
   432
  moreover have "s \<noteq> {}"
wenzelm@53408
   433
    using *(4) by auto
wenzelm@53408
   434
  ultimately show ?r
immler@56188
   435
    unfolding cbox_sing by auto
wenzelm@49698
   436
qed
himmelma@35172
   437
himmelma@35172
   438
lemma elementary_empty: obtains p where "p division_of {}"
himmelma@35172
   439
  unfolding division_of_trivial by auto
himmelma@35172
   440
immler@56188
   441
lemma elementary_interval: obtains p where "p division_of (cbox a b)"
wenzelm@49698
   442
  by (metis division_of_trivial division_of_self)
himmelma@35172
   443
himmelma@35172
   444
lemma division_contains: "s division_of i \<Longrightarrow> \<forall>x\<in>i. \<exists>k\<in>s. x \<in> k"
himmelma@35172
   445
  unfolding division_of_def by auto
himmelma@35172
   446
himmelma@35172
   447
lemma forall_in_division:
immler@56188
   448
  "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))"
nipkow@44890
   449
  unfolding division_of_def by fastforce
himmelma@35172
   450
wenzelm@53399
   451
lemma division_of_subset:
wenzelm@53399
   452
  assumes "p division_of (\<Union>p)"
wenzelm@53399
   453
    and "q \<subseteq> p"
wenzelm@53399
   454
  shows "q division_of (\<Union>q)"
wenzelm@53408
   455
proof (rule division_ofI)
wenzelm@53408
   456
  note * = division_ofD[OF assms(1)]
wenzelm@49698
   457
  show "finite q"
lp15@60384
   458
    using "*"(1) assms(2) infinite_super by auto
wenzelm@53399
   459
  {
wenzelm@53399
   460
    fix k
wenzelm@49698
   461
    assume "k \<in> q"
wenzelm@53408
   462
    then have kp: "k \<in> p"
wenzelm@53408
   463
      using assms(2) by auto
wenzelm@53408
   464
    show "k \<subseteq> \<Union>q"
wenzelm@60420
   465
      using \<open>k \<in> q\<close> by auto
immler@56188
   466
    show "\<exists>a b. k = cbox a b"
wenzelm@53408
   467
      using *(4)[OF kp] by auto
wenzelm@53408
   468
    show "k \<noteq> {}"
wenzelm@53408
   469
      using *(3)[OF kp] by auto
wenzelm@53399
   470
  }
wenzelm@49698
   471
  fix k1 k2
wenzelm@49698
   472
  assume "k1 \<in> q" "k2 \<in> q" "k1 \<noteq> k2"
wenzelm@53408
   473
  then have **: "k1 \<in> p" "k2 \<in> p" "k1 \<noteq> k2"
wenzelm@53399
   474
    using assms(2) by auto
wenzelm@53399
   475
  show "interior k1 \<inter> interior k2 = {}"
wenzelm@53408
   476
    using *(5)[OF **] by auto
wenzelm@49698
   477
qed auto
wenzelm@49698
   478
wenzelm@49698
   479
lemma division_of_union_self[intro]: "p division_of s \<Longrightarrow> p division_of (\<Union>p)"
wenzelm@49698
   480
  unfolding division_of_def by auto
himmelma@35172
   481
wenzelm@49970
   482
lemma division_of_content_0:
immler@56188
   483
  assumes "content (cbox a b) = 0" "d division_of (cbox a b)"
wenzelm@49970
   484
  shows "\<forall>k\<in>d. content k = 0"
wenzelm@49970
   485
  unfolding forall_in_division[OF assms(2)]
lp15@60384
   486
  by (metis antisym_conv assms content_pos_le content_subset division_ofD(2))
wenzelm@49970
   487
wenzelm@49970
   488
lemma division_inter:
immler@56188
   489
  fixes s1 s2 :: "'a::euclidean_space set"
wenzelm@53408
   490
  assumes "p1 division_of s1"
wenzelm@53408
   491
    and "p2 division_of s2"
hoelzl@63595
   492
  shows "{k1 \<inter> k2 | k1 k2. k1 \<in> p1 \<and> k2 \<in> p2 \<and> k1 \<inter> k2 \<noteq> {}} division_of (s1 \<inter> s2)"
wenzelm@49970
   493
  (is "?A' division_of _")
wenzelm@49970
   494
proof -
wenzelm@49970
   495
  let ?A = "{s. s \<in>  (\<lambda>(k1,k2). k1 \<inter> k2) ` (p1 \<times> p2) \<and> s \<noteq> {}}"
wenzelm@53408
   496
  have *: "?A' = ?A" by auto
wenzelm@53399
   497
  show ?thesis
wenzelm@53399
   498
    unfolding *
wenzelm@49970
   499
  proof (rule division_ofI)
wenzelm@53399
   500
    have "?A \<subseteq> (\<lambda>(x, y). x \<inter> y) ` (p1 \<times> p2)"
wenzelm@53399
   501
      by auto
wenzelm@53399
   502
    moreover have "finite (p1 \<times> p2)"
wenzelm@53399
   503
      using assms unfolding division_of_def by auto
wenzelm@49970
   504
    ultimately show "finite ?A" by auto
wenzelm@53399
   505
    have *: "\<And>s. \<Union>{x\<in>s. x \<noteq> {}} = \<Union>s"
wenzelm@53399
   506
      by auto
wenzelm@49970
   507
    show "\<Union>?A = s1 \<inter> s2"
wenzelm@49970
   508
      apply (rule set_eqI)
haftmann@62343
   509
      unfolding * and UN_iff
wenzelm@49970
   510
      using division_ofD(6)[OF assms(1)] and division_ofD(6)[OF assms(2)]
wenzelm@49970
   511
      apply auto
wenzelm@49970
   512
      done
wenzelm@53399
   513
    {
wenzelm@53399
   514
      fix k
wenzelm@53399
   515
      assume "k \<in> ?A"
wenzelm@53408
   516
      then obtain k1 k2 where k: "k = k1 \<inter> k2" "k1 \<in> p1" "k2 \<in> p2" "k \<noteq> {}"
wenzelm@53399
   517
        by auto
wenzelm@53408
   518
      then show "k \<noteq> {}"
wenzelm@53408
   519
        by auto
wenzelm@49970
   520
      show "k \<subseteq> s1 \<inter> s2"
wenzelm@49970
   521
        using division_ofD(2)[OF assms(1) k(2)] and division_ofD(2)[OF assms(2) k(3)]
wenzelm@49970
   522
        unfolding k by auto
immler@56188
   523
      obtain a1 b1 where k1: "k1 = cbox a1 b1"
wenzelm@53408
   524
        using division_ofD(4)[OF assms(1) k(2)] by blast
immler@56188
   525
      obtain a2 b2 where k2: "k2 = cbox a2 b2"
wenzelm@53408
   526
        using division_ofD(4)[OF assms(2) k(3)] by blast
immler@56188
   527
      show "\<exists>a b. k = cbox a b"
lp15@63945
   528
        unfolding k k1 k2 unfolding Int_interval by auto
wenzelm@53408
   529
    }
wenzelm@49970
   530
    fix k1 k2
wenzelm@53408
   531
    assume "k1 \<in> ?A"
wenzelm@53408
   532
    then obtain x1 y1 where k1: "k1 = x1 \<inter> y1" "x1 \<in> p1" "y1 \<in> p2" "k1 \<noteq> {}"
wenzelm@53408
   533
      by auto
wenzelm@53408
   534
    assume "k2 \<in> ?A"
wenzelm@53408
   535
    then obtain x2 y2 where k2: "k2 = x2 \<inter> y2" "x2 \<in> p1" "y2 \<in> p2" "k2 \<noteq> {}"
wenzelm@53408
   536
      by auto
wenzelm@49970
   537
    assume "k1 \<noteq> k2"
wenzelm@53399
   538
    then have th: "x1 \<noteq> x2 \<or> y1 \<noteq> y2"
wenzelm@53399
   539
      unfolding k1 k2 by auto
wenzelm@53408
   540
    have *: "interior x1 \<inter> interior x2 = {} \<or> interior y1 \<inter> interior y2 = {} \<Longrightarrow>
wenzelm@53408
   541
      interior (x1 \<inter> y1) \<subseteq> interior x1 \<Longrightarrow> interior (x1 \<inter> y1) \<subseteq> interior y1 \<Longrightarrow>
wenzelm@53408
   542
      interior (x2 \<inter> y2) \<subseteq> interior x2 \<Longrightarrow> interior (x2 \<inter> y2) \<subseteq> interior y2 \<Longrightarrow>
wenzelm@53408
   543
      interior (x1 \<inter> y1) \<inter> interior (x2 \<inter> y2) = {}" by auto
wenzelm@49970
   544
    show "interior k1 \<inter> interior k2 = {}"
wenzelm@49970
   545
      unfolding k1 k2
wenzelm@49970
   546
      apply (rule *)
lp15@60384
   547
      using assms division_ofD(5) k1 k2(2) k2(3) th apply auto
wenzelm@53399
   548
      done
wenzelm@49970
   549
  qed
wenzelm@49970
   550
qed
wenzelm@49970
   551
wenzelm@49970
   552
lemma division_inter_1:
wenzelm@53408
   553
  assumes "d division_of i"
immler@56188
   554
    and "cbox a (b::'a::euclidean_space) \<subseteq> i"
immler@56188
   555
  shows "{cbox a b \<inter> k | k. k \<in> d \<and> cbox a b \<inter> k \<noteq> {}} division_of (cbox a b)"
immler@56188
   556
proof (cases "cbox a b = {}")
wenzelm@49970
   557
  case True
wenzelm@53399
   558
  show ?thesis
wenzelm@53399
   559
    unfolding True and division_of_trivial by auto
wenzelm@49970
   560
next
wenzelm@49970
   561
  case False
immler@56188
   562
  have *: "cbox a b \<inter> i = cbox a b" using assms(2) by auto
wenzelm@53399
   563
  show ?thesis
wenzelm@53399
   564
    using division_inter[OF division_of_self[OF False] assms(1)]
wenzelm@53399
   565
    unfolding * by auto
wenzelm@49970
   566
qed
wenzelm@49970
   567
wenzelm@49970
   568
lemma elementary_inter:
immler@56188
   569
  fixes s t :: "'a::euclidean_space set"
wenzelm@53408
   570
  assumes "p1 division_of s"
wenzelm@53408
   571
    and "p2 division_of t"
himmelma@35172
   572
  shows "\<exists>p. p division_of (s \<inter> t)"
lp15@60384
   573
using assms division_inter by blast
wenzelm@49970
   574
wenzelm@49970
   575
lemma elementary_inters:
wenzelm@53408
   576
  assumes "finite f"
wenzelm@53408
   577
    and "f \<noteq> {}"
immler@56188
   578
    and "\<forall>s\<in>f. \<exists>p. p division_of (s::('a::euclidean_space) set)"
wenzelm@60585
   579
  shows "\<exists>p. p division_of (\<Inter>f)"
wenzelm@49970
   580
  using assms
wenzelm@49970
   581
proof (induct f rule: finite_induct)
wenzelm@49970
   582
  case (insert x f)
wenzelm@49970
   583
  show ?case
wenzelm@49970
   584
  proof (cases "f = {}")
wenzelm@49970
   585
    case True
wenzelm@53399
   586
    then show ?thesis
wenzelm@53399
   587
      unfolding True using insert by auto
wenzelm@49970
   588
  next
wenzelm@49970
   589
    case False
wenzelm@53408
   590
    obtain p where "p division_of \<Inter>f"
wenzelm@53408
   591
      using insert(3)[OF False insert(5)[unfolded ball_simps,THEN conjunct2]] ..
wenzelm@53408
   592
    moreover obtain px where "px division_of x"
wenzelm@53408
   593
      using insert(5)[rule_format,OF insertI1] ..
wenzelm@49970
   594
    ultimately show ?thesis
lp15@60384
   595
      by (simp add: elementary_inter Inter_insert)
wenzelm@49970
   596
  qed
wenzelm@49970
   597
qed auto
himmelma@35172
   598
himmelma@35172
   599
lemma division_disjoint_union:
wenzelm@53408
   600
  assumes "p1 division_of s1"
wenzelm@53408
   601
    and "p2 division_of s2"
wenzelm@53408
   602
    and "interior s1 \<inter> interior s2 = {}"
wenzelm@50945
   603
  shows "(p1 \<union> p2) division_of (s1 \<union> s2)"
wenzelm@50945
   604
proof (rule division_ofI)
wenzelm@53408
   605
  note d1 = division_ofD[OF assms(1)]
wenzelm@53408
   606
  note d2 = division_ofD[OF assms(2)]
wenzelm@53408
   607
  show "finite (p1 \<union> p2)"
wenzelm@53408
   608
    using d1(1) d2(1) by auto
wenzelm@53408
   609
  show "\<Union>(p1 \<union> p2) = s1 \<union> s2"
wenzelm@53408
   610
    using d1(6) d2(6) by auto
wenzelm@50945
   611
  {
wenzelm@50945
   612
    fix k1 k2
wenzelm@50945
   613
    assume as: "k1 \<in> p1 \<union> p2" "k2 \<in> p1 \<union> p2" "k1 \<noteq> k2"
wenzelm@50945
   614
    moreover
wenzelm@50945
   615
    let ?g="interior k1 \<inter> interior k2 = {}"
wenzelm@50945
   616
    {
wenzelm@50945
   617
      assume as: "k1\<in>p1" "k2\<in>p2"
wenzelm@50945
   618
      have ?g
wenzelm@50945
   619
        using interior_mono[OF d1(2)[OF as(1)]] interior_mono[OF d2(2)[OF as(2)]]
wenzelm@50945
   620
        using assms(3) by blast
wenzelm@50945
   621
    }
wenzelm@50945
   622
    moreover
wenzelm@50945
   623
    {
wenzelm@50945
   624
      assume as: "k1\<in>p2" "k2\<in>p1"
wenzelm@50945
   625
      have ?g
wenzelm@50945
   626
        using interior_mono[OF d1(2)[OF as(2)]] interior_mono[OF d2(2)[OF as(1)]]
wenzelm@50945
   627
        using assms(3) by blast
wenzelm@50945
   628
    }
wenzelm@53399
   629
    ultimately show ?g
wenzelm@53399
   630
      using d1(5)[OF _ _ as(3)] and d2(5)[OF _ _ as(3)] by auto
wenzelm@50945
   631
  }
wenzelm@50945
   632
  fix k
wenzelm@50945
   633
  assume k: "k \<in> p1 \<union> p2"
wenzelm@53408
   634
  show "k \<subseteq> s1 \<union> s2"
wenzelm@53408
   635
    using k d1(2) d2(2) by auto
wenzelm@53408
   636
  show "k \<noteq> {}"
wenzelm@53408
   637
    using k d1(3) d2(3) by auto
immler@56188
   638
  show "\<exists>a b. k = cbox a b"
wenzelm@53408
   639
    using k d1(4) d2(4) by auto
wenzelm@50945
   640
qed
himmelma@35172
   641
himmelma@35172
   642
lemma partial_division_extend_1:
immler@56188
   643
  fixes a b c d :: "'a::euclidean_space"
immler@56188
   644
  assumes incl: "cbox c d \<subseteq> cbox a b"
immler@56188
   645
    and nonempty: "cbox c d \<noteq> {}"
immler@56188
   646
  obtains p where "p division_of (cbox a b)" "cbox c d \<in> p"
hoelzl@50526
   647
proof
wenzelm@53408
   648
  let ?B = "\<lambda>f::'a\<Rightarrow>'a \<times> 'a.
immler@56188
   649
    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)"
wenzelm@63040
   650
  define p where "p = ?B ` (Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)})"
hoelzl@50526
   651
immler@56188
   652
  show "cbox c d \<in> p"
hoelzl@50526
   653
    unfolding p_def
immler@56188
   654
    by (auto simp add: box_eq_empty cbox_def intro!: image_eqI[where x="\<lambda>(i::'a)\<in>Basis. (c, d)"])
wenzelm@50945
   655
  {
wenzelm@50945
   656
    fix i :: 'a
wenzelm@50945
   657
    assume "i \<in> Basis"
hoelzl@50526
   658
    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"
immler@56188
   659
      unfolding box_eq_empty subset_box by (auto simp: not_le)
wenzelm@50945
   660
  }
hoelzl@50526
   661
  note ord = this
hoelzl@50526
   662
immler@56188
   663
  show "p division_of (cbox a b)"
hoelzl@50526
   664
  proof (rule division_ofI)
wenzelm@53399
   665
    show "finite p"
wenzelm@53399
   666
      unfolding p_def by (auto intro!: finite_PiE)
wenzelm@50945
   667
    {
wenzelm@50945
   668
      fix k
wenzelm@50945
   669
      assume "k \<in> p"
wenzelm@53015
   670
      then obtain f where f: "f \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}" and k: "k = ?B f"
hoelzl@50526
   671
        by (auto simp: p_def)
immler@56188
   672
      then show "\<exists>a b. k = cbox a b"
wenzelm@53408
   673
        by auto
immler@56188
   674
      have "k \<subseteq> cbox a b \<and> k \<noteq> {}"
immler@56188
   675
      proof (simp add: k box_eq_empty subset_box not_less, safe)
wenzelm@53374
   676
        fix i :: 'a
wenzelm@53374
   677
        assume i: "i \<in> Basis"
wenzelm@50945
   678
        with f have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
hoelzl@50526
   679
          by (auto simp: PiE_iff)
wenzelm@53374
   680
        with i ord[of i]
wenzelm@50945
   681
        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"
immler@54776
   682
          by auto
hoelzl@50526
   683
      qed
immler@56188
   684
      then show "k \<noteq> {}" "k \<subseteq> cbox a b"
wenzelm@53408
   685
        by auto
wenzelm@50945
   686
      {
wenzelm@53408
   687
        fix l
wenzelm@53408
   688
        assume "l \<in> p"
wenzelm@53015
   689
        then obtain g where g: "g \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}" and l: "l = ?B g"
wenzelm@50945
   690
          by (auto simp: p_def)
wenzelm@50945
   691
        assume "l \<noteq> k"
wenzelm@50945
   692
        have "\<exists>i\<in>Basis. f i \<noteq> g i"
wenzelm@50945
   693
        proof (rule ccontr)
wenzelm@53408
   694
          assume "\<not> ?thesis"
wenzelm@50945
   695
          with f g have "f = g"
wenzelm@50945
   696
            by (auto simp: PiE_iff extensional_def intro!: ext)
wenzelm@60420
   697
          with \<open>l \<noteq> k\<close> show False
wenzelm@50945
   698
            by (simp add: l k)
wenzelm@50945
   699
        qed
wenzelm@53408
   700
        then obtain i where *: "i \<in> Basis" "f i \<noteq> g i" ..
wenzelm@53408
   701
        then have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
lp15@60384
   702
                  "g i = (a, c) \<or> g i = (c, d) \<or> g i = (d, b)"
wenzelm@50945
   703
          using f g by (auto simp: PiE_iff)
wenzelm@53408
   704
        with * ord[of i] show "interior l \<inter> interior k = {}"
immler@56188
   705
          by (auto simp add: l k interior_cbox disjoint_interval intro!: bexI[of _ i])
wenzelm@50945
   706
      }
wenzelm@60420
   707
      note \<open>k \<subseteq> cbox a b\<close>
wenzelm@50945
   708
    }
hoelzl@50526
   709
    moreover
wenzelm@50945
   710
    {
immler@56188
   711
      fix x assume x: "x \<in> cbox a b"
hoelzl@50526
   712
      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)}"
hoelzl@50526
   713
      proof
wenzelm@53408
   714
        fix i :: 'a
wenzelm@53408
   715
        assume "i \<in> Basis"
wenzelm@53399
   716
        with x ord[of i]
hoelzl@50526
   717
        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>
hoelzl@50526
   718
            (d \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i)"
immler@56188
   719
          by (auto simp: cbox_def)
hoelzl@50526
   720
        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)}"
hoelzl@50526
   721
          by auto
hoelzl@50526
   722
      qed
wenzelm@53408
   723
      then obtain f where
wenzelm@53408
   724
        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)}"
wenzelm@53408
   725
        unfolding bchoice_iff ..
wenzelm@53374
   726
      moreover from f have "restrict f Basis \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}"
hoelzl@50526
   727
        by auto
hoelzl@50526
   728
      moreover from f have "x \<in> ?B (restrict f Basis)"
immler@56188
   729
        by (auto simp: mem_box)
hoelzl@50526
   730
      ultimately have "\<exists>k\<in>p. x \<in> k"
wenzelm@53408
   731
        unfolding p_def by blast
wenzelm@53408
   732
    }
immler@56188
   733
    ultimately show "\<Union>p = cbox a b"
hoelzl@50526
   734
      by auto
hoelzl@50526
   735
  qed
hoelzl@50526
   736
qed
himmelma@35172
   737
wenzelm@50945
   738
lemma partial_division_extend_interval:
immler@56188
   739
  assumes "p division_of (\<Union>p)" "(\<Union>p) \<subseteq> cbox a b"
immler@56188
   740
  obtains q where "p \<subseteq> q" "q division_of cbox a (b::'a::euclidean_space)"
wenzelm@50945
   741
proof (cases "p = {}")
wenzelm@50945
   742
  case True
immler@56188
   743
  obtain q where "q division_of (cbox a b)"
wenzelm@53408
   744
    by (rule elementary_interval)
wenzelm@53399
   745
  then show ?thesis
lp15@60384
   746
    using True that by blast
wenzelm@50945
   747
next
wenzelm@50945
   748
  case False
wenzelm@50945
   749
  note p = division_ofD[OF assms(1)]
lp15@60428
   750
  have div_cbox: "\<forall>k\<in>p. \<exists>q. q division_of cbox a b \<and> k \<in> q"
wenzelm@50945
   751
  proof
wenzelm@61165
   752
    fix k
wenzelm@61165
   753
    assume kp: "k \<in> p"
immler@56188
   754
    obtain c d where k: "k = cbox c d"
wenzelm@61165
   755
      using p(4)[OF kp] by blast
immler@56188
   756
    have *: "cbox c d \<subseteq> cbox a b" "cbox c d \<noteq> {}"
wenzelm@61165
   757
      using p(2,3)[OF kp, unfolded k] using assms(2)
immler@54776
   758
      by (blast intro: order.trans)+
immler@56188
   759
    obtain q where "q division_of cbox a b" "cbox c d \<in> q"
wenzelm@53408
   760
      by (rule partial_division_extend_1[OF *])
wenzelm@61165
   761
    then show "\<exists>q. q division_of cbox a b \<and> k \<in> q"
wenzelm@53408
   762
      unfolding k by auto
wenzelm@50945
   763
  qed
immler@56188
   764
  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"
lp15@60428
   765
    using bchoice[OF div_cbox] by blast
lp15@60394
   766
  { fix x
wenzelm@53408
   767
    assume x: "x \<in> p"
lp15@60394
   768
    have "q x division_of \<Union>q x"
wenzelm@50945
   769
      apply (rule division_ofI)
wenzelm@50945
   770
      using division_ofD[OF q(1)[OF x]]
wenzelm@50945
   771
      apply auto
lp15@60394
   772
      done }
lp15@60394
   773
  then have "\<And>x. x \<in> p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x - {x})"
lp15@60394
   774
    by (meson Diff_subset division_of_subset)
wenzelm@60585
   775
  then have "\<exists>d. d division_of \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p)"
wenzelm@50945
   776
    apply -
lp15@60394
   777
    apply (rule elementary_inters [OF finite_imageI[OF p(1)]])
lp15@60394
   778
    apply (auto simp: False elementary_inters [OF finite_imageI[OF p(1)]])
wenzelm@50945
   779
    done
wenzelm@53408
   780
  then obtain d where d: "d division_of \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p)" ..
lp15@60394
   781
  have "d \<union> p division_of cbox a b"
wenzelm@50945
   782
  proof -
lp15@60394
   783
    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
lp15@60428
   784
    have cbox_eq: "cbox a b = \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p) \<union> \<Union>p"
lp15@60394
   785
    proof (rule te[OF False], clarify)
wenzelm@50945
   786
      fix i
wenzelm@53408
   787
      assume i: "i \<in> p"
immler@56188
   788
      show "\<Union>(q i - {i}) \<union> i = cbox a b"
wenzelm@50945
   789
        using division_ofD(6)[OF q(1)[OF i]] using q(2)[OF i] by auto
wenzelm@50945
   790
    qed
lp15@60428
   791
    { fix k
wenzelm@53408
   792
      assume k: "k \<in> p"
lp15@60428
   793
      have *: "\<And>u t s. t \<inter> s = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<inter> t = {}"
wenzelm@53408
   794
        by auto
lp15@60428
   795
      have "interior (\<Inter>i\<in>p. \<Union>(q i - {i})) \<inter> interior k = {}"
lp15@60428
   796
      proof (rule *[OF inter_interior_unions_intervals])
wenzelm@50945
   797
        note qk=division_ofD[OF q(1)[OF k]]
immler@56188
   798
        show "finite (q k - {k})" "open (interior k)" "\<forall>t\<in>q k - {k}. \<exists>a b. t = cbox a b"
wenzelm@53408
   799
          using qk by auto
wenzelm@50945
   800
        show "\<forall>t\<in>q k - {k}. interior k \<inter> interior t = {}"
wenzelm@50945
   801
          using qk(5) using q(2)[OF k] by auto
lp15@60428
   802
        show "interior (\<Inter>i\<in>p. \<Union>(q i - {i})) \<subseteq> interior (\<Union>(q k - {k}))"
lp15@60428
   803
          apply (rule interior_mono)+
wenzelm@53408
   804
          using k
wenzelm@53408
   805
          apply auto
wenzelm@53408
   806
          done
lp15@60428
   807
      qed } note [simp] = this
lp15@60428
   808
    show "d \<union> p division_of (cbox a b)"
lp15@60428
   809
      unfolding cbox_eq
lp15@60428
   810
      apply (rule division_disjoint_union[OF d assms(1)])
lp15@60428
   811
      apply (rule inter_interior_unions_intervals)
lp15@60428
   812
      apply (rule p open_interior ballI)+
lp15@60615
   813
      apply simp_all
lp15@60428
   814
      done
lp15@60394
   815
  qed
lp15@60394
   816
  then show ?thesis
lp15@60394
   817
    by (meson Un_upper2 that)
wenzelm@50945
   818
qed
himmelma@35172
   819
wenzelm@53399
   820
lemma elementary_bounded[dest]:
immler@56188
   821
  fixes s :: "'a::euclidean_space set"
wenzelm@53408
   822
  shows "p division_of s \<Longrightarrow> bounded s"
immler@56189
   823
  unfolding division_of_def by (metis bounded_Union bounded_cbox)
wenzelm@53399
   824
immler@56188
   825
lemma elementary_subset_cbox:
immler@56188
   826
  "p division_of s \<Longrightarrow> \<exists>a b. s \<subseteq> cbox a (b::'a::euclidean_space)"
immler@56188
   827
  by (meson elementary_bounded bounded_subset_cbox)
wenzelm@50945
   828
wenzelm@50945
   829
lemma division_union_intervals_exists:
immler@56188
   830
  fixes a b :: "'a::euclidean_space"
immler@56188
   831
  assumes "cbox a b \<noteq> {}"
immler@56188
   832
  obtains p where "(insert (cbox a b) p) division_of (cbox a b \<union> cbox c d)"
immler@56188
   833
proof (cases "cbox c d = {}")
wenzelm@50945
   834
  case True
wenzelm@50945
   835
  show ?thesis
wenzelm@50945
   836
    apply (rule that[of "{}"])
wenzelm@50945
   837
    unfolding True
wenzelm@50945
   838
    using assms
wenzelm@50945
   839
    apply auto
wenzelm@50945
   840
    done
wenzelm@50945
   841
next
wenzelm@50945
   842
  case False
wenzelm@50945
   843
  show ?thesis
immler@56188
   844
  proof (cases "cbox a b \<inter> cbox c d = {}")
wenzelm@50945
   845
    case True
lp15@62618
   846
    then show ?thesis
lp15@62618
   847
      by (metis that False assms division_disjoint_union division_of_self insert_is_Un interior_Int interior_empty)
wenzelm@50945
   848
  next
wenzelm@50945
   849
    case False
immler@56188
   850
    obtain u v where uv: "cbox a b \<inter> cbox c d = cbox u v"
lp15@63945
   851
      unfolding Int_interval by auto
lp15@60428
   852
    have uv_sub: "cbox u v \<subseteq> cbox c d" using uv by auto
immler@56188
   853
    obtain p where "p division_of cbox c d" "cbox u v \<in> p"
lp15@60428
   854
      by (rule partial_division_extend_1[OF uv_sub False[unfolded uv]])
wenzelm@53408
   855
    note p = this division_ofD[OF this(1)]
lp15@60428
   856
    have "interior (cbox a b \<inter> \<Union>(p - {cbox u v})) = interior(cbox u v \<inter> \<Union>(p - {cbox u v}))"
lp15@60428
   857
      apply (rule arg_cong[of _ _ interior])
lp15@60428
   858
      using p(8) uv by auto
lp15@60428
   859
    also have "\<dots> = {}"
paulson@61518
   860
      unfolding interior_Int
lp15@60428
   861
      apply (rule inter_interior_unions_intervals)
lp15@60428
   862
      using p(6) p(7)[OF p(2)] p(3)
lp15@60428
   863
      apply auto
lp15@60428
   864
      done
lp15@60428
   865
    finally have [simp]: "interior (cbox a b) \<inter> interior (\<Union>(p - {cbox u v})) = {}" by simp
lp15@60615
   866
    have cbe: "cbox a b \<union> cbox c d = cbox a b \<union> \<Union>(p - {cbox u v})"
wenzelm@53399
   867
      using p(8) unfolding uv[symmetric] by auto
lp15@62618
   868
    have "insert (cbox a b) (p - {cbox u v}) division_of cbox a b \<union> \<Union>(p - {cbox u v})"
lp15@62618
   869
    proof -
lp15@62618
   870
      have "{cbox a b} division_of cbox a b"
lp15@62618
   871
        by (simp add: assms division_of_self)
lp15@62618
   872
      then show "insert (cbox a b) (p - {cbox u v}) division_of cbox a b \<union> \<Union>(p - {cbox u v})"
lp15@62618
   873
        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))
lp15@62618
   874
    qed
lp15@62618
   875
    with that[of "p - {cbox u v}"] show ?thesis by (simp add: cbe)
wenzelm@50945
   876
  qed
wenzelm@50945
   877
qed
himmelma@35172
   878
wenzelm@53399
   879
lemma division_of_unions:
wenzelm@53399
   880
  assumes "finite f"
wenzelm@53408
   881
    and "\<And>p. p \<in> f \<Longrightarrow> p division_of (\<Union>p)"
wenzelm@53399
   882
    and "\<And>k1 k2. k1 \<in> \<Union>f \<Longrightarrow> k2 \<in> \<Union>f \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior k1 \<inter> interior k2 = {}"
wenzelm@53399
   883
  shows "\<Union>f division_of \<Union>\<Union>f"
lp15@60384
   884
  using assms
lp15@60384
   885
  by (auto intro!: division_ofI)
wenzelm@53399
   886
wenzelm@53399
   887
lemma elementary_union_interval:
immler@56188
   888
  fixes a b :: "'a::euclidean_space"
wenzelm@53399
   889
  assumes "p division_of \<Union>p"
immler@56188
   890
  obtains q where "q division_of (cbox a b \<union> \<Union>p)"
wenzelm@53399
   891
proof -
wenzelm@53399
   892
  note assm = division_ofD[OF assms]
wenzelm@53408
   893
  have lem1: "\<And>f s. \<Union>\<Union>(f ` s) = \<Union>((\<lambda>x. \<Union>(f x)) ` s)"
wenzelm@53399
   894
    by auto
wenzelm@53399
   895
  have lem2: "\<And>f s. f \<noteq> {} \<Longrightarrow> \<Union>{s \<union> t |t. t \<in> f} = s \<union> \<Union>f"
wenzelm@53399
   896
    by auto
wenzelm@53399
   897
  {
wenzelm@53399
   898
    presume "p = {} \<Longrightarrow> thesis"
immler@56188
   899
      "cbox a b = {} \<Longrightarrow> thesis"
immler@56188
   900
      "cbox a b \<noteq> {} \<Longrightarrow> interior (cbox a b) = {} \<Longrightarrow> thesis"
immler@56188
   901
      "p \<noteq> {} \<Longrightarrow> interior (cbox a b)\<noteq>{} \<Longrightarrow> cbox a b \<noteq> {} \<Longrightarrow> thesis"
wenzelm@53399
   902
    then show thesis by auto
wenzelm@53399
   903
  next
wenzelm@53399
   904
    assume as: "p = {}"
immler@56188
   905
    obtain p where "p division_of (cbox a b)"
wenzelm@53408
   906
      by (rule elementary_interval)
wenzelm@53399
   907
    then show thesis
lp15@60384
   908
      using as that by auto
wenzelm@53399
   909
  next
immler@56188
   910
    assume as: "cbox a b = {}"
wenzelm@53399
   911
    show thesis
lp15@60384
   912
      using as assms that by auto
wenzelm@53399
   913
  next
immler@56188
   914
    assume as: "interior (cbox a b) = {}" "cbox a b \<noteq> {}"
wenzelm@53399
   915
    show thesis
immler@56188
   916
      apply (rule that[of "insert (cbox a b) p"],rule division_ofI)
wenzelm@53399
   917
      unfolding finite_insert
wenzelm@53399
   918
      apply (rule assm(1)) unfolding Union_insert
wenzelm@53399
   919
      using assm(2-4) as
wenzelm@53399
   920
      apply -
immler@54775
   921
      apply (fast dest: assm(5))+
wenzelm@53399
   922
      done
wenzelm@53399
   923
  next
immler@56188
   924
    assume as: "p \<noteq> {}" "interior (cbox a b) \<noteq> {}" "cbox a b \<noteq> {}"
immler@56188
   925
    have "\<forall>k\<in>p. \<exists>q. (insert (cbox a b) q) division_of (cbox a b \<union> k)"
lp15@60615
   926
    proof
wenzelm@61165
   927
      fix k
wenzelm@61165
   928
      assume kp: "k \<in> p"
wenzelm@61165
   929
      from assm(4)[OF kp] obtain c d where "k = cbox c d" by blast
wenzelm@61165
   930
      then show "\<exists>q. (insert (cbox a b) q) division_of (cbox a b \<union> k)"
lp15@60384
   931
        by (meson as(3) division_union_intervals_exists)
wenzelm@53399
   932
    qed
immler@56188
   933
    from bchoice[OF this] obtain q where "\<forall>x\<in>p. insert (cbox a b) (q x) division_of (cbox a b) \<union> x" ..
wenzelm@53408
   934
    note q = division_ofD[OF this[rule_format]]
immler@56188
   935
    let ?D = "\<Union>{insert (cbox a b) (q k) | k. k \<in> p}"
lp15@60615
   936
    show thesis
lp15@60428
   937
    proof (rule that[OF division_ofI])
immler@56188
   938
      have *: "{insert (cbox a b) (q k) |k. k \<in> p} = (\<lambda>k. insert (cbox a b) (q k)) ` p"
wenzelm@53399
   939
        by auto
wenzelm@53399
   940
      show "finite ?D"
lp15@60384
   941
        using "*" assm(1) q(1) by auto
immler@56188
   942
      show "\<Union>?D = cbox a b \<union> \<Union>p"
wenzelm@53399
   943
        unfolding * lem1
immler@56188
   944
        unfolding lem2[OF as(1), of "cbox a b", symmetric]
wenzelm@53399
   945
        using q(6)
wenzelm@53399
   946
        by auto
wenzelm@53399
   947
      fix k
wenzelm@53408
   948
      assume k: "k \<in> ?D"
immler@56188
   949
      then show "k \<subseteq> cbox a b \<union> \<Union>p"
wenzelm@53408
   950
        using q(2) by auto
wenzelm@53399
   951
      show "k \<noteq> {}"
wenzelm@53408
   952
        using q(3) k by auto
immler@56188
   953
      show "\<exists>a b. k = cbox a b"
wenzelm@53408
   954
        using q(4) k by auto
wenzelm@53399
   955
      fix k'
wenzelm@53408
   956
      assume k': "k' \<in> ?D" "k \<noteq> k'"
immler@56188
   957
      obtain x where x: "k \<in> insert (cbox a b) (q x)" "x\<in>p"
wenzelm@53408
   958
        using k by auto
immler@56188
   959
      obtain x' where x': "k'\<in>insert (cbox a b) (q x')" "x'\<in>p"
wenzelm@53399
   960
        using k' by auto
wenzelm@53399
   961
      show "interior k \<inter> interior k' = {}"
wenzelm@53399
   962
      proof (cases "x = x'")
wenzelm@53399
   963
        case True
wenzelm@53399
   964
        show ?thesis
lp15@60384
   965
          using True k' q(5) x' x by auto
wenzelm@53399
   966
      next
wenzelm@53399
   967
        case False
wenzelm@53399
   968
        {
immler@56188
   969
          presume "k = cbox a b \<Longrightarrow> ?thesis"
immler@56188
   970
            and "k' = cbox a b \<Longrightarrow> ?thesis"
immler@56188
   971
            and "k \<noteq> cbox a b \<Longrightarrow> k' \<noteq> cbox a b \<Longrightarrow> ?thesis"
lp15@62618
   972
          then show ?thesis by linarith
wenzelm@53399
   973
        next
immler@56188
   974
          assume as': "k  = cbox a b"
wenzelm@53399
   975
          show ?thesis
lp15@63469
   976
            using as' k' q(5) x' by blast
wenzelm@53399
   977
        next
immler@56188
   978
          assume as': "k' = cbox a b"
wenzelm@53399
   979
          show ?thesis
lp15@62618
   980
            using as' k'(2) q(5) x by blast
wenzelm@53399
   981
        }
immler@56188
   982
        assume as': "k \<noteq> cbox a b" "k' \<noteq> cbox a b"
immler@56188
   983
        obtain c d where k: "k = cbox c d"
wenzelm@53408
   984
          using q(4)[OF x(2,1)] by blast
immler@56188
   985
        have "interior k \<inter> interior (cbox a b) = {}"
lp15@62618
   986
          using as' k'(2) q(5) x by blast
wenzelm@53399
   987
        then have "interior k \<subseteq> interior x"
lp15@60384
   988
        using interior_subset_union_intervals
lp15@60384
   989
          by (metis as(2) k q(2) x interior_subset_union_intervals)
wenzelm@53399
   990
        moreover
immler@56188
   991
        obtain c d where c_d: "k' = cbox c d"
wenzelm@53408
   992
          using q(4)[OF x'(2,1)] by blast
immler@56188
   993
        have "interior k' \<inter> interior (cbox a b) = {}"
lp15@62618
   994
          using as'(2) q(5) x' by blast
wenzelm@53399
   995
        then have "interior k' \<subseteq> interior x'"
lp15@60384
   996
          by (metis as(2) c_d interior_subset_union_intervals q(2) x'(1) x'(2))
wenzelm@53399
   997
        ultimately show ?thesis
wenzelm@53399
   998
          using assm(5)[OF x(2) x'(2) False] by auto
wenzelm@53399
   999
      qed
wenzelm@53399
  1000
    qed
wenzelm@53399
  1001
  }
wenzelm@53399
  1002
qed
himmelma@35172
  1003
himmelma@35172
  1004
lemma elementary_unions_intervals:
wenzelm@53399
  1005
  assumes fin: "finite f"
immler@56188
  1006
    and "\<And>s. s \<in> f \<Longrightarrow> \<exists>a b. s = cbox a (b::'a::euclidean_space)"
wenzelm@53399
  1007
  obtains p where "p division_of (\<Union>f)"
wenzelm@53399
  1008
proof -
wenzelm@53399
  1009
  have "\<exists>p. p division_of (\<Union>f)"
wenzelm@53399
  1010
  proof (induct_tac f rule:finite_subset_induct)
himmelma@35172
  1011
    show "\<exists>p. p division_of \<Union>{}" using elementary_empty by auto
wenzelm@53399
  1012
  next
wenzelm@53399
  1013
    fix x F
wenzelm@53399
  1014
    assume as: "finite F" "x \<notin> F" "\<exists>p. p division_of \<Union>F" "x\<in>f"
wenzelm@53408
  1015
    from this(3) obtain p where p: "p division_of \<Union>F" ..
immler@56188
  1016
    from assms(2)[OF as(4)] obtain a b where x: "x = cbox a b" by blast
wenzelm@53399
  1017
    have *: "\<Union>F = \<Union>p"
wenzelm@53399
  1018
      using division_ofD[OF p] by auto
wenzelm@53399
  1019
    show "\<exists>p. p division_of \<Union>insert x F"
wenzelm@53399
  1020
      using elementary_union_interval[OF p[unfolded *], of a b]
lp15@59765
  1021
      unfolding Union_insert x * by metis
wenzelm@53408
  1022
  qed (insert assms, auto)
wenzelm@53399
  1023
  then show ?thesis
lp15@60384
  1024
    using that by auto
wenzelm@53399
  1025
qed
wenzelm@53399
  1026
wenzelm@53399
  1027
lemma elementary_union:
immler@56188
  1028
  fixes s t :: "'a::euclidean_space set"
lp15@60384
  1029
  assumes "ps division_of s" "pt division_of t"
himmelma@35172
  1030
  obtains p where "p division_of (s \<union> t)"
wenzelm@53399
  1031
proof -
lp15@60384
  1032
  have *: "s \<union> t = \<Union>ps \<union> \<Union>pt"
wenzelm@53399
  1033
    using assms unfolding division_of_def by auto
wenzelm@53399
  1034
  show ?thesis
wenzelm@53408
  1035
    apply (rule elementary_unions_intervals[of "ps \<union> pt"])
lp15@60384
  1036
    using assms apply auto
lp15@60384
  1037
    by (simp add: * that)
wenzelm@53399
  1038
qed
wenzelm@53399
  1039
wenzelm@53399
  1040
lemma partial_division_extend:
immler@56188
  1041
  fixes t :: "'a::euclidean_space set"
wenzelm@53399
  1042
  assumes "p division_of s"
wenzelm@53399
  1043
    and "q division_of t"
wenzelm@53399
  1044
    and "s \<subseteq> t"
wenzelm@53399
  1045
  obtains r where "p \<subseteq> r" and "r division_of t"
wenzelm@53399
  1046
proof -
himmelma@35172
  1047
  note divp = division_ofD[OF assms(1)] and divq = division_ofD[OF assms(2)]
immler@56188
  1048
  obtain a b where ab: "t \<subseteq> cbox a b"
immler@56188
  1049
    using elementary_subset_cbox[OF assms(2)] by auto
immler@56188
  1050
  obtain r1 where "p \<subseteq> r1" "r1 division_of (cbox a b)"
lp15@60384
  1051
    using assms
lp15@60384
  1052
    by (metis ab dual_order.trans partial_division_extend_interval divp(6))
wenzelm@53399
  1053
  note r1 = this division_ofD[OF this(2)]
wenzelm@53408
  1054
  obtain p' where "p' division_of \<Union>(r1 - p)"
wenzelm@53399
  1055
    apply (rule elementary_unions_intervals[of "r1 - p"])
wenzelm@53399
  1056
    using r1(3,6)
wenzelm@53399
  1057
    apply auto
wenzelm@53399
  1058
    done
wenzelm@53399
  1059
  then obtain r2 where r2: "r2 division_of (\<Union>(r1 - p)) \<inter> (\<Union>q)"
lp15@60384
  1060
    by (metis assms(2) divq(6) elementary_inter)
wenzelm@53399
  1061
  {
wenzelm@53399
  1062
    fix x
wenzelm@53399
  1063
    assume x: "x \<in> t" "x \<notin> s"
wenzelm@53399
  1064
    then have "x\<in>\<Union>r1"
wenzelm@53399
  1065
      unfolding r1 using ab by auto
wenzelm@53408
  1066
    then obtain r where r: "r \<in> r1" "x \<in> r"
wenzelm@53408
  1067
      unfolding Union_iff ..
wenzelm@53399
  1068
    moreover
wenzelm@53399
  1069
    have "r \<notin> p"
wenzelm@53399
  1070
    proof
wenzelm@53399
  1071
      assume "r \<in> p"
wenzelm@53399
  1072
      then have "x \<in> s" using divp(2) r by auto
wenzelm@53399
  1073
      then show False using x by auto
wenzelm@53399
  1074
    qed
wenzelm@53399
  1075
    ultimately have "x\<in>\<Union>(r1 - p)" by auto
wenzelm@53399
  1076
  }
wenzelm@53399
  1077
  then have *: "t = \<Union>p \<union> (\<Union>(r1 - p) \<inter> \<Union>q)"
wenzelm@53399
  1078
    unfolding divp divq using assms(3) by auto
wenzelm@53399
  1079
  show ?thesis
wenzelm@53399
  1080
    apply (rule that[of "p \<union> r2"])
wenzelm@53399
  1081
    unfolding *
wenzelm@53399
  1082
    defer
wenzelm@53399
  1083
    apply (rule division_disjoint_union)
wenzelm@53399
  1084
    unfolding divp(6)
wenzelm@53399
  1085
    apply(rule assms r2)+
wenzelm@53399
  1086
  proof -
wenzelm@53399
  1087
    have "interior s \<inter> interior (\<Union>(r1-p)) = {}"
wenzelm@53399
  1088
    proof (rule inter_interior_unions_intervals)
immler@56188
  1089
      show "finite (r1 - p)" and "open (interior s)" and "\<forall>t\<in>r1-p. \<exists>a b. t = cbox a b"
wenzelm@53399
  1090
        using r1 by auto
wenzelm@53399
  1091
      have *: "\<And>s. (\<And>x. x \<in> s \<Longrightarrow> False) \<Longrightarrow> s = {}"
wenzelm@53399
  1092
        by auto
wenzelm@53399
  1093
      show "\<forall>t\<in>r1-p. interior s \<inter> interior t = {}"
wenzelm@53399
  1094
      proof
wenzelm@53399
  1095
        fix m x
wenzelm@53399
  1096
        assume as: "m \<in> r1 - p"
wenzelm@53399
  1097
        have "interior m \<inter> interior (\<Union>p) = {}"
wenzelm@53399
  1098
        proof (rule inter_interior_unions_intervals)
immler@56188
  1099
          show "finite p" and "open (interior m)" and "\<forall>t\<in>p. \<exists>a b. t = cbox a b"
wenzelm@53399
  1100
            using divp by auto
wenzelm@53399
  1101
          show "\<forall>t\<in>p. interior m \<inter> interior t = {}"
lp15@60384
  1102
            by (metis DiffD1 DiffD2 as r1(1) r1(7) set_rev_mp)
wenzelm@53399
  1103
        qed
wenzelm@53399
  1104
        then show "interior s \<inter> interior m = {}"
wenzelm@53399
  1105
          unfolding divp by auto
wenzelm@53399
  1106
      qed
wenzelm@53399
  1107
    qed
wenzelm@53399
  1108
    then show "interior s \<inter> interior (\<Union>(r1-p) \<inter> (\<Union>q)) = {}"
wenzelm@53399
  1109
      using interior_subset by auto
wenzelm@53399
  1110
  qed auto
wenzelm@53399
  1111
qed
wenzelm@53399
  1112
hoelzl@63593
  1113
lemma division_split_left_inj:
hoelzl@63593
  1114
  fixes type :: "'a::euclidean_space"
hoelzl@63593
  1115
  assumes "d division_of i"
hoelzl@63593
  1116
    and "k1 \<in> d"
hoelzl@63593
  1117
    and "k2 \<in> d"
hoelzl@63593
  1118
    and "k1 \<noteq> k2"
hoelzl@63593
  1119
    and "k1 \<inter> {x::'a. x\<bullet>k \<le> c} = k2 \<inter> {x. x\<bullet>k \<le> c}"
hoelzl@63593
  1120
    and k: "k\<in>Basis"
hoelzl@63593
  1121
  shows "content(k1 \<inter> {x. x\<bullet>k \<le> c}) = 0"
hoelzl@63593
  1122
proof -
hoelzl@63593
  1123
  note d=division_ofD[OF assms(1)]
hoelzl@63593
  1124
  have *: "\<And>(a::'a) b c. content (cbox a b \<inter> {x. x\<bullet>k \<le> c}) = 0 \<longleftrightarrow>
hoelzl@63593
  1125
    interior(cbox a b \<inter> {x. x\<bullet>k \<le> c}) = {}"
hoelzl@63593
  1126
    unfolding  interval_split[OF k] content_eq_0_interior by auto
hoelzl@63593
  1127
  guess u1 v1 using d(4)[OF assms(2)] by (elim exE) note uv1=this
hoelzl@63593
  1128
  guess u2 v2 using d(4)[OF assms(3)] by (elim exE) note uv2=this
hoelzl@63593
  1129
  have **: "\<And>s t u. s \<inter> t = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<subseteq> t \<Longrightarrow> u = {}"
hoelzl@63593
  1130
    by auto
hoelzl@63593
  1131
  show ?thesis
hoelzl@63593
  1132
    unfolding uv1 uv2 *
hoelzl@63593
  1133
    apply (rule **[OF d(5)[OF assms(2-4)]])
hoelzl@63593
  1134
    apply (simp add: uv1)
hoelzl@63593
  1135
    using assms(5) uv1 by auto
hoelzl@63593
  1136
qed
hoelzl@63593
  1137
hoelzl@63593
  1138
lemma division_split_right_inj:
hoelzl@63593
  1139
  fixes type :: "'a::euclidean_space"
hoelzl@63593
  1140
  assumes "d division_of i"
hoelzl@63593
  1141
    and "k1 \<in> d"
hoelzl@63593
  1142
    and "k2 \<in> d"
hoelzl@63593
  1143
    and "k1 \<noteq> k2"
hoelzl@63593
  1144
    and "k1 \<inter> {x::'a. x\<bullet>k \<ge> c} = k2 \<inter> {x. x\<bullet>k \<ge> c}"
hoelzl@63593
  1145
    and k: "k \<in> Basis"
hoelzl@63593
  1146
  shows "content (k1 \<inter> {x. x\<bullet>k \<ge> c}) = 0"
hoelzl@63593
  1147
proof -
hoelzl@63593
  1148
  note d=division_ofD[OF assms(1)]
hoelzl@63593
  1149
  have *: "\<And>a b::'a. \<And>c. content(cbox a b \<inter> {x. x\<bullet>k \<ge> c}) = 0 \<longleftrightarrow>
hoelzl@63593
  1150
    interior(cbox a b \<inter> {x. x\<bullet>k \<ge> c}) = {}"
hoelzl@63593
  1151
    unfolding interval_split[OF k] content_eq_0_interior by auto
hoelzl@63593
  1152
  guess u1 v1 using d(4)[OF assms(2)] by (elim exE) note uv1=this
hoelzl@63593
  1153
  guess u2 v2 using d(4)[OF assms(3)] by (elim exE) note uv2=this
hoelzl@63593
  1154
  have **: "\<And>s t u. s \<inter> t = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<subseteq> t \<Longrightarrow> u = {}"
hoelzl@63593
  1155
    by auto
hoelzl@63593
  1156
  show ?thesis
hoelzl@63593
  1157
    unfolding uv1 uv2 *
hoelzl@63593
  1158
    apply (rule **[OF d(5)[OF assms(2-4)]])
hoelzl@63593
  1159
    apply (simp add: uv1)
hoelzl@63593
  1160
    using assms(5) uv1 by auto
hoelzl@63593
  1161
qed
hoelzl@63593
  1162
hoelzl@63593
  1163
hoelzl@63593
  1164
lemma division_split:
hoelzl@63593
  1165
  fixes a :: "'a::euclidean_space"
hoelzl@63593
  1166
  assumes "p division_of (cbox a b)"
hoelzl@63593
  1167
    and k: "k\<in>Basis"
hoelzl@63593
  1168
  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})"
hoelzl@63593
  1169
      (is "?p1 division_of ?I1")
hoelzl@63593
  1170
    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})"
hoelzl@63593
  1171
      (is "?p2 division_of ?I2")
hoelzl@63593
  1172
proof (rule_tac[!] division_ofI)
hoelzl@63593
  1173
  note p = division_ofD[OF assms(1)]
hoelzl@63593
  1174
  show "finite ?p1" "finite ?p2"
hoelzl@63593
  1175
    using p(1) by auto
hoelzl@63593
  1176
  show "\<Union>?p1 = ?I1" "\<Union>?p2 = ?I2"
hoelzl@63593
  1177
    unfolding p(6)[symmetric] by auto
hoelzl@63593
  1178
  {
hoelzl@63593
  1179
    fix k
hoelzl@63593
  1180
    assume "k \<in> ?p1"
hoelzl@63593
  1181
    then guess l unfolding mem_Collect_eq by (elim exE conjE) note l=this
hoelzl@63593
  1182
    guess u v using p(4)[OF l(2)] by (elim exE) note uv=this
hoelzl@63593
  1183
    show "k \<subseteq> ?I1"
hoelzl@63593
  1184
      using l p(2) uv by force
hoelzl@63593
  1185
    show  "k \<noteq> {}"
hoelzl@63593
  1186
      by (simp add: l)
hoelzl@63593
  1187
    show  "\<exists>a b. k = cbox a b"
hoelzl@63593
  1188
      apply (simp add: l uv p(2-3)[OF l(2)])
hoelzl@63593
  1189
      apply (subst interval_split[OF k])
hoelzl@63593
  1190
      apply (auto intro: order.trans)
hoelzl@63593
  1191
      done
hoelzl@63593
  1192
    fix k'
hoelzl@63593
  1193
    assume "k' \<in> ?p1"
hoelzl@63593
  1194
    then guess l' unfolding mem_Collect_eq by (elim exE conjE) note l'=this
hoelzl@63593
  1195
    assume "k \<noteq> k'"
hoelzl@63593
  1196
    then show "interior k \<inter> interior k' = {}"
hoelzl@63593
  1197
      unfolding l l' using p(5)[OF l(2) l'(2)] by auto
hoelzl@63593
  1198
  }
hoelzl@63593
  1199
  {
hoelzl@63593
  1200
    fix k
hoelzl@63593
  1201
    assume "k \<in> ?p2"
hoelzl@63593
  1202
    then guess l unfolding mem_Collect_eq by (elim exE conjE) note l=this
hoelzl@63593
  1203
    guess u v using p(4)[OF l(2)] by (elim exE) note uv=this
hoelzl@63593
  1204
    show "k \<subseteq> ?I2"
hoelzl@63593
  1205
      using l p(2) uv by force
hoelzl@63593
  1206
    show  "k \<noteq> {}"
hoelzl@63593
  1207
      by (simp add: l)
hoelzl@63593
  1208
    show  "\<exists>a b. k = cbox a b"
hoelzl@63593
  1209
      apply (simp add: l uv p(2-3)[OF l(2)])
hoelzl@63593
  1210
      apply (subst interval_split[OF k])
hoelzl@63593
  1211
      apply (auto intro: order.trans)
hoelzl@63593
  1212
      done
hoelzl@63593
  1213
    fix k'
hoelzl@63593
  1214
    assume "k' \<in> ?p2"
hoelzl@63593
  1215
    then guess l' unfolding mem_Collect_eq by (elim exE conjE) note l'=this
hoelzl@63593
  1216
    assume "k \<noteq> k'"
hoelzl@63593
  1217
    then show "interior k \<inter> interior k' = {}"
hoelzl@63593
  1218
      unfolding l l' using p(5)[OF l(2) l'(2)] by auto
hoelzl@63593
  1219
  }
hoelzl@63593
  1220
qed
himmelma@35172
  1221
wenzelm@60420
  1222
subsection \<open>Tagged (partial) divisions.\<close>
himmelma@35172
  1223
wenzelm@53408
  1224
definition tagged_partial_division_of (infixr "tagged'_partial'_division'_of" 40)
wenzelm@53408
  1225
  where "s tagged_partial_division_of i \<longleftrightarrow>
wenzelm@53408
  1226
    finite s \<and>
immler@56188
  1227
    (\<forall>x k. (x, k) \<in> s \<longrightarrow> x \<in> k \<and> k \<subseteq> i \<and> (\<exists>a b. k = cbox a b)) \<and>
wenzelm@53408
  1228
    (\<forall>x1 k1 x2 k2. (x1, k1) \<in> s \<and> (x2, k2) \<in> s \<and> (x1, k1) \<noteq> (x2, k2) \<longrightarrow>
wenzelm@53408
  1229
      interior k1 \<inter> interior k2 = {})"
wenzelm@53408
  1230
wenzelm@53408
  1231
lemma tagged_partial_division_ofD[dest]:
wenzelm@53408
  1232
  assumes "s tagged_partial_division_of i"
wenzelm@53408
  1233
  shows "finite s"
wenzelm@53408
  1234
    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> x \<in> k"
wenzelm@53408
  1235
    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> i"
immler@56188
  1236
    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b"
wenzelm@53408
  1237
    and "\<And>x1 k1 x2 k2. (x1,k1) \<in> s \<Longrightarrow>
wenzelm@53408
  1238
      (x2, k2) \<in> s \<Longrightarrow> (x1, k1) \<noteq> (x2, k2) \<Longrightarrow> interior k1 \<inter> interior k2 = {}"
wenzelm@53408
  1239
  using assms unfolding tagged_partial_division_of_def by blast+
wenzelm@53408
  1240
wenzelm@53408
  1241
definition tagged_division_of (infixr "tagged'_division'_of" 40)
wenzelm@53408
  1242
  where "s tagged_division_of i \<longleftrightarrow> s tagged_partial_division_of i \<and> (\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
himmelma@35172
  1243
huffman@44167
  1244
lemma tagged_division_of_finite: "s tagged_division_of i \<Longrightarrow> finite s"
himmelma@35172
  1245
  unfolding tagged_division_of_def tagged_partial_division_of_def by auto
himmelma@35172
  1246
himmelma@35172
  1247
lemma tagged_division_of:
wenzelm@53408
  1248
  "s tagged_division_of i \<longleftrightarrow>
wenzelm@53408
  1249
    finite s \<and>
immler@56188
  1250
    (\<forall>x k. (x, k) \<in> s \<longrightarrow> x \<in> k \<and> k \<subseteq> i \<and> (\<exists>a b. k = cbox a b)) \<and>
wenzelm@53408
  1251
    (\<forall>x1 k1 x2 k2. (x1, k1) \<in> s \<and> (x2, k2) \<in> s \<and> (x1, k1) \<noteq> (x2, k2) \<longrightarrow>
wenzelm@53408
  1252
      interior k1 \<inter> interior k2 = {}) \<and>
wenzelm@53408
  1253
    (\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
himmelma@35172
  1254
  unfolding tagged_division_of_def tagged_partial_division_of_def by auto
himmelma@35172
  1255
wenzelm@53408
  1256
lemma tagged_division_ofI:
wenzelm@53408
  1257
  assumes "finite s"
wenzelm@53408
  1258
    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> x \<in> k"
wenzelm@53408
  1259
    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> i"
immler@56188
  1260
    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b"
wenzelm@53408
  1261
    and "\<And>x1 k1 x2 k2. (x1,k1) \<in> s \<Longrightarrow> (x2, k2) \<in> s \<Longrightarrow> (x1, k1) \<noteq> (x2, k2) \<Longrightarrow>
wenzelm@53408
  1262
      interior k1 \<inter> interior k2 = {}"
wenzelm@53408
  1263
    and "(\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
himmelma@35172
  1264
  shows "s tagged_division_of i"
wenzelm@53408
  1265
  unfolding tagged_division_of
lp15@60384
  1266
  using assms
lp15@60384
  1267
  apply auto
lp15@60384
  1268
  apply fastforce+
wenzelm@53408
  1269
  done
wenzelm@53408
  1270
lp15@60384
  1271
lemma tagged_division_ofD[dest]:  (*FIXME USE A LOCALE*)
wenzelm@53408
  1272
  assumes "s tagged_division_of i"
wenzelm@53408
  1273
  shows "finite s"
wenzelm@53408
  1274
    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> x \<in> k"
wenzelm@53408
  1275
    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> i"
immler@56188
  1276
    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b"
wenzelm@53408
  1277
    and "\<And>x1 k1 x2 k2. (x1, k1) \<in> s \<Longrightarrow> (x2, k2) \<in> s \<Longrightarrow> (x1, k1) \<noteq> (x2, k2) \<Longrightarrow>
wenzelm@53408
  1278
      interior k1 \<inter> interior k2 = {}"
wenzelm@53408
  1279
    and "(\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
wenzelm@53408
  1280
  using assms unfolding tagged_division_of by blast+
wenzelm@53408
  1281
wenzelm@53408
  1282
lemma division_of_tagged_division:
wenzelm@53408
  1283
  assumes "s tagged_division_of i"
wenzelm@53408
  1284
  shows "(snd ` s) division_of i"
wenzelm@53408
  1285
proof (rule division_ofI)
wenzelm@53408
  1286
  note assm = tagged_division_ofD[OF assms]
wenzelm@53408
  1287
  show "\<Union>(snd ` s) = i" "finite (snd ` s)"
wenzelm@53408
  1288
    using assm by auto
wenzelm@53408
  1289
  fix k
wenzelm@53408
  1290
  assume k: "k \<in> snd ` s"
wenzelm@53408
  1291
  then obtain xk where xk: "(xk, k) \<in> s"
wenzelm@53408
  1292
    by auto
immler@56188
  1293
  then show "k \<subseteq> i" "k \<noteq> {}" "\<exists>a b. k = cbox a b"
wenzelm@53408
  1294
    using assm by fastforce+
wenzelm@53408
  1295
  fix k'
wenzelm@53408
  1296
  assume k': "k' \<in> snd ` s" "k \<noteq> k'"
wenzelm@53408
  1297
  from this(1) obtain xk' where xk': "(xk', k') \<in> s"
wenzelm@53408
  1298
    by auto
wenzelm@53408
  1299
  then show "interior k \<inter> interior k' = {}"
lp15@60384
  1300
    using assm(5) k'(2) xk by blast
himmelma@35172
  1301
qed
himmelma@35172
  1302
wenzelm@53408
  1303
lemma partial_division_of_tagged_division:
wenzelm@53408
  1304
  assumes "s tagged_partial_division_of i"
himmelma@35172
  1305
  shows "(snd ` s) division_of \<Union>(snd ` s)"
wenzelm@53408
  1306
proof (rule division_ofI)
wenzelm@53408
  1307
  note assm = tagged_partial_division_ofD[OF assms]
wenzelm@53408
  1308
  show "finite (snd ` s)" "\<Union>(snd ` s) = \<Union>(snd ` s)"
wenzelm@53408
  1309
    using assm by auto
wenzelm@53408
  1310
  fix k
wenzelm@53408
  1311
  assume k: "k \<in> snd ` s"
wenzelm@53408
  1312
  then obtain xk where xk: "(xk, k) \<in> s"
wenzelm@53408
  1313
    by auto
immler@56188
  1314
  then show "k \<noteq> {}" "\<exists>a b. k = cbox a b" "k \<subseteq> \<Union>(snd ` s)"
wenzelm@53408
  1315
    using assm by auto
wenzelm@53408
  1316
  fix k'
wenzelm@53408
  1317
  assume k': "k' \<in> snd ` s" "k \<noteq> k'"
wenzelm@53408
  1318
  from this(1) obtain xk' where xk': "(xk', k') \<in> s"
wenzelm@53408
  1319
    by auto
wenzelm@53408
  1320
  then show "interior k \<inter> interior k' = {}"
lp15@60384
  1321
    using assm(5) k'(2) xk by auto
himmelma@35172
  1322
qed
himmelma@35172
  1323
wenzelm@53408
  1324
lemma tagged_partial_division_subset:
wenzelm@53408
  1325
  assumes "s tagged_partial_division_of i"
wenzelm@53408
  1326
    and "t \<subseteq> s"
himmelma@35172
  1327
  shows "t tagged_partial_division_of i"
wenzelm@53408
  1328
  using assms
wenzelm@53408
  1329
  unfolding tagged_partial_division_of_def
wenzelm@53408
  1330
  using finite_subset[OF assms(2)]
wenzelm@53408
  1331
  by blast
wenzelm@53408
  1332
hoelzl@63593
  1333
lemma (in comm_monoid_set) over_tagged_division_lemma:
wenzelm@53408
  1334
  assumes "p tagged_division_of i"
hoelzl@63593
  1335
    and "\<And>u v. cbox u v \<noteq> {} \<Longrightarrow> content (cbox u v) = 0 \<Longrightarrow> d (cbox u v) = \<^bold>1"
hoelzl@63593
  1336
  shows "F (\<lambda>(x,k). d k) p = F d (snd ` p)"
wenzelm@53408
  1337
proof -
wenzelm@53408
  1338
  have *: "(\<lambda>(x,k). d k) = d \<circ> snd"
wenzelm@53408
  1339
    unfolding o_def by (rule ext) auto
hoelzl@57129
  1340
  note assm = tagged_division_ofD[OF assms(1)]
wenzelm@53408
  1341
  show ?thesis
wenzelm@53408
  1342
    unfolding *
hoelzl@63593
  1343
  proof (rule reindex_nontrivial[symmetric])
wenzelm@53408
  1344
    show "finite p"
wenzelm@53408
  1345
      using assm by auto
wenzelm@53408
  1346
    fix x y
hoelzl@57129
  1347
    assume "x\<in>p" "y\<in>p" "x\<noteq>y" "snd x = snd y"
immler@56188
  1348
    obtain a b where ab: "snd x = cbox a b"
wenzelm@60420
  1349
      using assm(4)[of "fst x" "snd x"] \<open>x\<in>p\<close> by auto
wenzelm@53408
  1350
    have "(fst x, snd y) \<in> p" "(fst x, snd y) \<noteq> y"
haftmann@61424
  1351
      by (metis prod.collapse \<open>x\<in>p\<close> \<open>snd x = snd y\<close> \<open>x \<noteq> y\<close>)+
wenzelm@60420
  1352
    with \<open>x\<in>p\<close> \<open>y\<in>p\<close> have "interior (snd x) \<inter> interior (snd y) = {}"
hoelzl@57129
  1353
      by (intro assm(5)[of "fst x" _ "fst y"]) auto
immler@56188
  1354
    then have "content (cbox a b) = 0"
wenzelm@60420
  1355
      unfolding \<open>snd x = snd y\<close>[symmetric] ab content_eq_0_interior by auto
hoelzl@63593
  1356
    then have "d (cbox a b) = \<^bold>1"
wenzelm@60420
  1357
      using assm(2)[of "fst x" "snd x"] \<open>x\<in>p\<close> ab[symmetric] by (intro assms(2)) auto
hoelzl@63593
  1358
    then show "d (snd x) = \<^bold>1"
wenzelm@53408
  1359
      unfolding ab by auto
wenzelm@53408
  1360
  qed
wenzelm@53408
  1361
qed
wenzelm@53408
  1362
wenzelm@53408
  1363
lemma tag_in_interval: "p tagged_division_of i \<Longrightarrow> (x, k) \<in> p \<Longrightarrow> x \<in> i"
wenzelm@53408
  1364
  by auto
himmelma@35172
  1365
himmelma@35172
  1366
lemma tagged_division_of_empty: "{} tagged_division_of {}"
himmelma@35172
  1367
  unfolding tagged_division_of by auto
himmelma@35172
  1368
wenzelm@53408
  1369
lemma tagged_partial_division_of_trivial[simp]: "p tagged_partial_division_of {} \<longleftrightarrow> p = {}"
himmelma@35172
  1370
  unfolding tagged_partial_division_of_def by auto
himmelma@35172
  1371
wenzelm@53408
  1372
lemma tagged_division_of_trivial[simp]: "p tagged_division_of {} \<longleftrightarrow> p = {}"
himmelma@35172
  1373
  unfolding tagged_division_of by auto
himmelma@35172
  1374
immler@56188
  1375
lemma tagged_division_of_self: "x \<in> cbox a b \<Longrightarrow> {(x,cbox a b)} tagged_division_of (cbox a b)"
wenzelm@53408
  1376
  by (rule tagged_division_ofI) auto
himmelma@35172
  1377
immler@56188
  1378
lemma tagged_division_of_self_real: "x \<in> {a .. b::real} \<Longrightarrow> {(x,{a .. b})} tagged_division_of {a .. b}"
immler@56188
  1379
  unfolding box_real[symmetric]
immler@56188
  1380
  by (rule tagged_division_of_self)
immler@56188
  1381
himmelma@35172
  1382
lemma tagged_division_union:
wenzelm@53408
  1383
  assumes "p1 tagged_division_of s1"
wenzelm@53408
  1384
    and "p2 tagged_division_of s2"
wenzelm@53408
  1385
    and "interior s1 \<inter> interior s2 = {}"
himmelma@35172
  1386
  shows "(p1 \<union> p2) tagged_division_of (s1 \<union> s2)"
wenzelm@53408
  1387
proof (rule tagged_division_ofI)
wenzelm@53408
  1388
  note p1 = tagged_division_ofD[OF assms(1)]
wenzelm@53408
  1389
  note p2 = tagged_division_ofD[OF assms(2)]
wenzelm@53408
  1390
  show "finite (p1 \<union> p2)"
wenzelm@53408
  1391
    using p1(1) p2(1) by auto
wenzelm@53408
  1392
  show "\<Union>{k. \<exists>x. (x, k) \<in> p1 \<union> p2} = s1 \<union> s2"
wenzelm@53408
  1393
    using p1(6) p2(6) by blast
wenzelm@53408
  1394
  fix x k
wenzelm@53408
  1395
  assume xk: "(x, k) \<in> p1 \<union> p2"
immler@56188
  1396
  show "x \<in> k" "\<exists>a b. k = cbox a b"
wenzelm@53408
  1397
    using xk p1(2,4) p2(2,4) by auto
wenzelm@53408
  1398
  show "k \<subseteq> s1 \<union> s2"
wenzelm@53408
  1399
    using xk p1(3) p2(3) by blast
wenzelm@53408
  1400
  fix x' k'
wenzelm@53408
  1401
  assume xk': "(x', k') \<in> p1 \<union> p2" "(x, k) \<noteq> (x', k')"
wenzelm@53408
  1402
  have *: "\<And>a b. a \<subseteq> s1 \<Longrightarrow> b \<subseteq> s2 \<Longrightarrow> interior a \<inter> interior b = {}"
wenzelm@53408
  1403
    using assms(3) interior_mono by blast
wenzelm@53408
  1404
  show "interior k \<inter> interior k' = {}"
wenzelm@53408
  1405
    apply (cases "(x, k) \<in> p1")
lp15@60384
  1406
    apply (meson "*" UnE assms(1) assms(2) p1(5) tagged_division_ofD(3) xk'(1) xk'(2))
lp15@60384
  1407
    by (metis "*" UnE assms(1) assms(2) inf_sup_aci(1) p2(5) tagged_division_ofD(3) xk xk'(1) xk'(2))
wenzelm@53408
  1408
qed
himmelma@35172
  1409
himmelma@35172
  1410
lemma tagged_division_unions:
wenzelm@53408
  1411
  assumes "finite iset"
wenzelm@53408
  1412
    and "\<forall>i\<in>iset. pfn i tagged_division_of i"
wenzelm@53408
  1413
    and "\<forall>i1\<in>iset. \<forall>i2\<in>iset. i1 \<noteq> i2 \<longrightarrow> interior(i1) \<inter> interior(i2) = {}"
himmelma@35172
  1414
  shows "\<Union>(pfn ` iset) tagged_division_of (\<Union>iset)"
wenzelm@53408
  1415
proof (rule tagged_division_ofI)
himmelma@35172
  1416
  note assm = tagged_division_ofD[OF assms(2)[rule_format]]
wenzelm@53408
  1417
  show "finite (\<Union>(pfn ` iset))"
hoelzl@63940
  1418
    using assms by auto
wenzelm@53408
  1419
  have "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>(pfn ` iset)} = \<Union>((\<lambda>i. \<Union>{k. \<exists>x. (x, k) \<in> pfn i}) ` iset)"
wenzelm@53408
  1420
    by blast
wenzelm@53408
  1421
  also have "\<dots> = \<Union>iset"
wenzelm@53408
  1422
    using assm(6) by auto
wenzelm@53399
  1423
  finally show "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>(pfn ` iset)} = \<Union>iset" .
wenzelm@53408
  1424
  fix x k
wenzelm@53408
  1425
  assume xk: "(x, k) \<in> \<Union>(pfn ` iset)"
wenzelm@53408
  1426
  then obtain i where i: "i \<in> iset" "(x, k) \<in> pfn i"
wenzelm@53408
  1427
    by auto
immler@56188
  1428
  show "x \<in> k" "\<exists>a b. k = cbox a b" "k \<subseteq> \<Union>iset"
wenzelm@53408
  1429
    using assm(2-4)[OF i] using i(1) by auto
wenzelm@53408
  1430
  fix x' k'
wenzelm@53408
  1431
  assume xk': "(x', k') \<in> \<Union>(pfn ` iset)" "(x, k) \<noteq> (x', k')"
wenzelm@53408
  1432
  then obtain i' where i': "i' \<in> iset" "(x', k') \<in> pfn i'"
wenzelm@53408
  1433
    by auto
wenzelm@53408
  1434
  have *: "\<And>a b. i \<noteq> i' \<Longrightarrow> a \<subseteq> i \<Longrightarrow> b \<subseteq> i' \<Longrightarrow> interior a \<inter> interior b = {}"
wenzelm@53408
  1435
    using i(1) i'(1)
wenzelm@53408
  1436
    using assms(3)[rule_format] interior_mono
wenzelm@53408
  1437
    by blast
wenzelm@53408
  1438
  show "interior k \<inter> interior k' = {}"
wenzelm@53408
  1439
    apply (cases "i = i'")
lp15@60384
  1440
    using assm(5) i' i(2) xk'(2) apply blast
lp15@60384
  1441
    using "*" assm(3) i' i by auto
himmelma@35172
  1442
qed
himmelma@35172
  1443
himmelma@35172
  1444
lemma tagged_partial_division_of_union_self:
wenzelm@53408
  1445
  assumes "p tagged_partial_division_of s"
himmelma@35172
  1446
  shows "p tagged_division_of (\<Union>(snd ` p))"
wenzelm@53408
  1447
  apply (rule tagged_division_ofI)
wenzelm@53408
  1448
  using tagged_partial_division_ofD[OF assms]
wenzelm@53408
  1449
  apply auto
wenzelm@53408
  1450
  done
wenzelm@53408
  1451
wenzelm@53408
  1452
lemma tagged_division_of_union_self:
wenzelm@53408
  1453
  assumes "p tagged_division_of s"
wenzelm@53408
  1454
  shows "p tagged_division_of (\<Union>(snd ` p))"
wenzelm@53408
  1455
  apply (rule tagged_division_ofI)
wenzelm@53408
  1456
  using tagged_division_ofD[OF assms]
wenzelm@53408
  1457
  apply auto
wenzelm@53408
  1458
  done
wenzelm@53408
  1459
hoelzl@63593
  1460
subsection \<open>Functions closed on boxes: morphisms from boxes to monoids\<close>
hoelzl@63593
  1461
hoelzl@63593
  1462
text \<open>This auxiliary structure is used to sum up over the elements of a division. Main theorem is
hoelzl@63593
  1463
  @{text operative_division}. Instances for the monoid are @{typ "'a option"}, @{typ real}, and
hoelzl@63593
  1464
  @{typ bool}.\<close>
hoelzl@63593
  1465
hoelzl@63593
  1466
lemma property_empty_interval: "\<forall>a b. content (cbox a b) = 0 \<longrightarrow> P (cbox a b) \<Longrightarrow> P {}"
hoelzl@63593
  1467
  using content_empty unfolding empty_as_interval by auto
hoelzl@63593
  1468
hoelzl@63593
  1469
paragraph \<open>Using additivity of lifted function to encode definedness.\<close>
hoelzl@63593
  1470
hoelzl@63593
  1471
definition lift_option :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> 'c option"
hoelzl@63593
  1472
where
hoelzl@63593
  1473
  "lift_option f a' b' = Option.bind a' (\<lambda>a. Option.bind b' (\<lambda>b. Some (f a b)))"
hoelzl@63593
  1474
hoelzl@63593
  1475
lemma lift_option_simps[simp]:
hoelzl@63593
  1476
  "lift_option f (Some a) (Some b) = Some (f a b)"
hoelzl@63593
  1477
  "lift_option f None b' = None"
hoelzl@63593
  1478
  "lift_option f a' None = None"
hoelzl@63593
  1479
  by (auto simp: lift_option_def)
hoelzl@63593
  1480
haftmann@63659
  1481
lemma comm_monoid_lift_option:
haftmann@63659
  1482
  assumes "comm_monoid f z"
haftmann@63659
  1483
  shows "comm_monoid (lift_option f) (Some z)"
haftmann@63659
  1484
proof -
haftmann@63659
  1485
  from assms interpret comm_monoid f z .
haftmann@63659
  1486
  show ?thesis
haftmann@63659
  1487
    by standard (auto simp: lift_option_def ac_simps split: bind_split)
haftmann@63659
  1488
qed
haftmann@63659
  1489
haftmann@63659
  1490
lemma comm_monoid_and: "comm_monoid HOL.conj True"
haftmann@63659
  1491
  by standard auto
haftmann@63659
  1492
haftmann@63659
  1493
lemma comm_monoid_set_and: "comm_monoid_set HOL.conj True"
haftmann@63659
  1494
  by (rule comm_monoid_set.intro) (fact comm_monoid_and)
hoelzl@63593
  1495
hoelzl@63593
  1496
paragraph \<open>Operative\<close>
hoelzl@63593
  1497
hoelzl@63593
  1498
definition (in comm_monoid) operative :: "('b::euclidean_space set \<Rightarrow> 'a) \<Rightarrow> bool"
hoelzl@63593
  1499
  where "operative g \<longleftrightarrow>
hoelzl@63593
  1500
    (\<forall>a b. content (cbox a b) = 0 \<longrightarrow> g (cbox a b) = \<^bold>1) \<and>
hoelzl@63593
  1501
    (\<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}))"
hoelzl@63593
  1502
hoelzl@63593
  1503
lemma (in comm_monoid) operativeD[dest]:
hoelzl@63593
  1504
  assumes "operative g"
hoelzl@63593
  1505
  shows "\<And>a b. content (cbox a b) = 0 \<Longrightarrow> g (cbox a b) = \<^bold>1"
hoelzl@63593
  1506
    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})"
hoelzl@63593
  1507
  using assms unfolding operative_def by auto
hoelzl@63593
  1508
hoelzl@63593
  1509
lemma (in comm_monoid) operative_empty: "operative g \<Longrightarrow> g {} = \<^bold>1"
hoelzl@63593
  1510
  unfolding operative_def by (rule property_empty_interval) auto
hoelzl@63593
  1511
hoelzl@63593
  1512
lemma operative_content[intro]: "add.operative content"
hoelzl@63593
  1513
  by (force simp add: add.operative_def content_split[symmetric])
hoelzl@63593
  1514
hoelzl@63593
  1515
definition "division_points (k::('a::euclidean_space) set) d =
hoelzl@63593
  1516
   {(j,x). j \<in> Basis \<and> (interval_lowerbound k)\<bullet>j < x \<and> x < (interval_upperbound k)\<bullet>j \<and>
hoelzl@63593
  1517
     (\<exists>i\<in>d. (interval_lowerbound i)\<bullet>j = x \<or> (interval_upperbound i)\<bullet>j = x)}"
hoelzl@63593
  1518
hoelzl@63593
  1519
lemma division_points_finite:
hoelzl@63593
  1520
  fixes i :: "'a::euclidean_space set"
hoelzl@63593
  1521
  assumes "d division_of i"
hoelzl@63593
  1522
  shows "finite (division_points i d)"
hoelzl@63593
  1523
proof -
hoelzl@63593
  1524
  note assm = division_ofD[OF assms]
hoelzl@63593
  1525
  let ?M = "\<lambda>j. {(j,x)|x. (interval_lowerbound i)\<bullet>j < x \<and> x < (interval_upperbound i)\<bullet>j \<and>
hoelzl@63593
  1526
    (\<exists>i\<in>d. (interval_lowerbound i)\<bullet>j = x \<or> (interval_upperbound i)\<bullet>j = x)}"
hoelzl@63593
  1527
  have *: "division_points i d = \<Union>(?M ` Basis)"
hoelzl@63593
  1528
    unfolding division_points_def by auto
hoelzl@63593
  1529
  show ?thesis
hoelzl@63593
  1530
    unfolding * using assm by auto
hoelzl@63593
  1531
qed
hoelzl@63593
  1532
hoelzl@63593
  1533
lemma division_points_subset:
hoelzl@63593
  1534
  fixes a :: "'a::euclidean_space"
hoelzl@63593
  1535
  assumes "d division_of (cbox a b)"
hoelzl@63593
  1536
    and "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"  "a\<bullet>k < c" "c < b\<bullet>k"
hoelzl@63593
  1537
    and k: "k \<in> Basis"
hoelzl@63593
  1538
  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>
hoelzl@63593
  1539
      division_points (cbox a b) d" (is ?t1)
hoelzl@63593
  1540
    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>
hoelzl@63593
  1541
      division_points (cbox a b) d" (is ?t2)
hoelzl@63593
  1542
proof -
hoelzl@63593
  1543
  note assm = division_ofD[OF assms(1)]
hoelzl@63593
  1544
  have *: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
hoelzl@63593
  1545
    "\<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"
hoelzl@63593
  1546
    "\<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"
hoelzl@63593
  1547
    "min (b \<bullet> k) c = c" "max (a \<bullet> k) c = c"
hoelzl@63593
  1548
    using assms using less_imp_le by auto
hoelzl@63593
  1549
  show ?t1 (*FIXME a horrible mess*)
hoelzl@63593
  1550
    unfolding division_points_def interval_split[OF k, of a b]
hoelzl@63593
  1551
    unfolding interval_bounds[OF *(1)] interval_bounds[OF *(2)] interval_bounds[OF *(3)]
hoelzl@63593
  1552
    unfolding *
hoelzl@63593
  1553
    apply (rule subsetI)
hoelzl@63593
  1554
    unfolding mem_Collect_eq split_beta
hoelzl@63593
  1555
    apply (erule bexE conjE)+
hoelzl@63593
  1556
    apply (simp add: )
hoelzl@63593
  1557
    apply (erule exE conjE)+
hoelzl@63593
  1558
  proof
hoelzl@63593
  1559
    fix i l x
hoelzl@63593
  1560
    assume as:
hoelzl@63593
  1561
      "a \<bullet> fst x < snd x" "snd x < (if fst x = k then c else b \<bullet> fst x)"
hoelzl@63593
  1562
      "interval_lowerbound i \<bullet> fst x = snd x \<or> interval_upperbound i \<bullet> fst x = snd x"
hoelzl@63593
  1563
      "i = l \<inter> {x. x \<bullet> k \<le> c}" "l \<in> d" "l \<inter> {x. x \<bullet> k \<le> c} \<noteq> {}"
hoelzl@63593
  1564
      and fstx: "fst x \<in> Basis"
hoelzl@63593
  1565
    from assm(4)[OF this(5)] guess u v apply-by(erule exE)+ note l=this
hoelzl@63593
  1566
    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"
hoelzl@63593
  1567
      using as(6) unfolding l interval_split[OF k] box_ne_empty as .
hoelzl@63593
  1568
    have **: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i"
hoelzl@63593
  1569
      using l using as(6) unfolding box_ne_empty[symmetric] by auto
hoelzl@63593
  1570
    show "\<exists>i\<in>d. interval_lowerbound i \<bullet> fst x = snd x \<or> interval_upperbound i \<bullet> fst x = snd x"
hoelzl@63593
  1571
      apply (rule bexI[OF _ \<open>l \<in> d\<close>])
hoelzl@63593
  1572
      using as(1-3,5) fstx
hoelzl@63593
  1573
      unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] as
hoelzl@63593
  1574
      apply (auto split: if_split_asm)
hoelzl@63593
  1575
      done
hoelzl@63593
  1576
    show "snd x < b \<bullet> fst x"
hoelzl@63593
  1577
      using as(2) \<open>c < b\<bullet>k\<close> by (auto split: if_split_asm)
hoelzl@63593
  1578
  qed
hoelzl@63593
  1579
  show ?t2
hoelzl@63593
  1580
    unfolding division_points_def interval_split[OF k, of a b]
hoelzl@63593
  1581
    unfolding interval_bounds[OF *(1)] interval_bounds[OF *(2)] interval_bounds[OF *(3)]
hoelzl@63593
  1582
    unfolding *
hoelzl@63593
  1583
    unfolding subset_eq
hoelzl@63593
  1584
    apply rule
hoelzl@63593
  1585
    unfolding mem_Collect_eq split_beta
hoelzl@63593
  1586
    apply (erule bexE conjE)+
hoelzl@63593
  1587
    apply (simp only: mem_Collect_eq inner_setsum_left_Basis simp_thms)
hoelzl@63593
  1588
    apply (erule exE conjE)+
hoelzl@63593
  1589
  proof
hoelzl@63593
  1590
    fix i l x
hoelzl@63593
  1591
    assume as:
hoelzl@63593
  1592
      "(if fst x = k then c else a \<bullet> fst x) < snd x" "snd x < b \<bullet> fst x"
hoelzl@63593
  1593
      "interval_lowerbound i \<bullet> fst x = snd x \<or> interval_upperbound i \<bullet> fst x = snd x"
hoelzl@63593
  1594
      "i = l \<inter> {x. c \<le> x \<bullet> k}" "l \<in> d" "l \<inter> {x. c \<le> x \<bullet> k} \<noteq> {}"
hoelzl@63593
  1595
      and fstx: "fst x \<in> Basis"
hoelzl@63593
  1596
    from assm(4)[OF this(5)] guess u v by (elim exE) note l=this
hoelzl@63593
  1597
    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"
hoelzl@63593
  1598
      using as(6) unfolding l interval_split[OF k] box_ne_empty as .
hoelzl@63593
  1599
    have **: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i"
hoelzl@63593
  1600
      using l using as(6) unfolding box_ne_empty[symmetric] by auto
hoelzl@63593
  1601
    show "\<exists>i\<in>d. interval_lowerbound i \<bullet> fst x = snd x \<or> interval_upperbound i \<bullet> fst x = snd x"
hoelzl@63593
  1602
      apply (rule bexI[OF _ \<open>l \<in> d\<close>])
hoelzl@63593
  1603
      using as(1-3,5) fstx
hoelzl@63593
  1604
      unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] as
hoelzl@63593
  1605
      apply (auto split: if_split_asm)
hoelzl@63593
  1606
      done
hoelzl@63593
  1607
    show "a \<bullet> fst x < snd x"
hoelzl@63593
  1608
      using as(1) \<open>a\<bullet>k < c\<close> by (auto split: if_split_asm)
hoelzl@63593
  1609
   qed
hoelzl@63593
  1610
qed
hoelzl@63593
  1611
hoelzl@63593
  1612
lemma division_points_psubset:
hoelzl@63593
  1613
  fixes a :: "'a::euclidean_space"
hoelzl@63593
  1614
  assumes "d division_of (cbox a b)"
hoelzl@63593
  1615
      and "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"  "a\<bullet>k < c" "c < b\<bullet>k"
hoelzl@63593
  1616
      and "l \<in> d"
hoelzl@63593
  1617
      and "interval_lowerbound l\<bullet>k = c \<or> interval_upperbound l\<bullet>k = c"
hoelzl@63593
  1618
      and k: "k \<in> Basis"
hoelzl@63593
  1619
  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>
hoelzl@63593
  1620
         division_points (cbox a b) d" (is "?D1 \<subset> ?D")
hoelzl@63593
  1621
    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>
hoelzl@63593
  1622
         division_points (cbox a b) d" (is "?D2 \<subset> ?D")
hoelzl@63593
  1623
proof -
hoelzl@63593
  1624
  have ab: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
hoelzl@63593
  1625
    using assms(2) by (auto intro!:less_imp_le)
hoelzl@63593
  1626
  guess u v using division_ofD(4)[OF assms(1,5)] by (elim exE) note l=this
hoelzl@63593
  1627
  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"
hoelzl@63593
  1628
    using division_ofD(2,2,3)[OF assms(1,5)] unfolding l box_ne_empty
hoelzl@63593
  1629
    using subset_box(1)
hoelzl@63593
  1630
    apply auto
hoelzl@63593
  1631
    apply blast+
hoelzl@63593
  1632
    done
hoelzl@63593
  1633
  have *: "interval_upperbound (cbox a b \<inter> {x. x \<bullet> k \<le> interval_upperbound l \<bullet> k}) \<bullet> k = interval_upperbound l \<bullet> k"
hoelzl@63593
  1634
          "interval_upperbound (cbox a b \<inter> {x. x \<bullet> k \<le> interval_lowerbound l \<bullet> k}) \<bullet> k = interval_lowerbound l \<bullet> k"
hoelzl@63593
  1635
    unfolding l interval_split[OF k] interval_bounds[OF uv(1)]
hoelzl@63593
  1636
    using uv[rule_format, of k] ab k
hoelzl@63593
  1637
    by auto
hoelzl@63593
  1638
  have "\<exists>x. x \<in> ?D - ?D1"
hoelzl@63593
  1639
    using assms(3-)
hoelzl@63593
  1640
    unfolding division_points_def interval_bounds[OF ab]
hoelzl@63593
  1641
    apply -
hoelzl@63593
  1642
    apply (erule disjE)
hoelzl@63593
  1643
    apply (rule_tac x="(k,(interval_lowerbound l)\<bullet>k)" in exI, force simp add: *)
hoelzl@63593
  1644
    apply (rule_tac x="(k,(interval_upperbound l)\<bullet>k)" in exI, force simp add: *)
hoelzl@63593
  1645
    done
hoelzl@63593
  1646
  moreover have "?D1 \<subseteq> ?D"
hoelzl@63593
  1647
    by (auto simp add: assms division_points_subset)
hoelzl@63593
  1648
  ultimately show "?D1 \<subset> ?D"
hoelzl@63593
  1649
    by blast
hoelzl@63593
  1650
  have *: "interval_lowerbound (cbox a b \<inter> {x. x \<bullet> k \<ge> interval_lowerbound l \<bullet> k}) \<bullet> k = interval_lowerbound l \<bullet> k"
hoelzl@63593
  1651
    "interval_lowerbound (cbox a b \<inter> {x. x \<bullet> k \<ge> interval_upperbound l \<bullet> k}) \<bullet> k = interval_upperbound l \<bullet> k"
hoelzl@63593
  1652
    unfolding l interval_split[OF k] interval_bounds[OF uv(1)]
hoelzl@63593
  1653
    using uv[rule_format, of k] ab k
hoelzl@63593
  1654
    by auto
hoelzl@63593
  1655
  have "\<exists>x. x \<in> ?D - ?D2"
hoelzl@63593
  1656
    using assms(3-)
hoelzl@63593
  1657
    unfolding division_points_def interval_bounds[OF ab]
hoelzl@63593
  1658
    apply -
hoelzl@63593
  1659
    apply (erule disjE)
hoelzl@63593
  1660
    apply (rule_tac x="(k,(interval_lowerbound l)\<bullet>k)" in exI, force simp add: *)
hoelzl@63593
  1661
    apply (rule_tac x="(k,(interval_upperbound l)\<bullet>k)" in exI, force simp add: *)
hoelzl@63593
  1662
    done
hoelzl@63593
  1663
  moreover have "?D2 \<subseteq> ?D"
hoelzl@63593
  1664
    by (auto simp add: assms division_points_subset)
hoelzl@63593
  1665
  ultimately show "?D2 \<subset> ?D"
hoelzl@63593
  1666
    by blast
hoelzl@63593
  1667
qed
hoelzl@63593
  1668
hoelzl@63593
  1669
lemma (in comm_monoid_set) operative_division:
hoelzl@63593
  1670
  fixes g :: "'b::euclidean_space set \<Rightarrow> 'a"
hoelzl@63593
  1671
  assumes g: "operative g" and d: "d division_of (cbox a b)" shows "F g d = g (cbox a b)"
hoelzl@63593
  1672
proof -
hoelzl@63593
  1673
  define C where [abs_def]: "C = card (division_points (cbox a b) d)"
hoelzl@63593
  1674
  then show ?thesis
hoelzl@63593
  1675
    using d
hoelzl@63593
  1676
  proof (induction C arbitrary: a b d rule: less_induct)
hoelzl@63593
  1677
    case (less a b d)
hoelzl@63593
  1678
    show ?case
hoelzl@63593
  1679
    proof cases
hoelzl@63593
  1680
      show "content (cbox a b) = 0 \<Longrightarrow> F g d = g (cbox a b)"
hoelzl@63593
  1681
        using division_of_content_0[OF _ less.prems] operativeD(1)[OF  g] division_ofD(4)[OF less.prems]
hoelzl@63593
  1682
        by (fastforce intro!: neutral)
hoelzl@63593
  1683
    next
hoelzl@63593
  1684
      assume "content (cbox a b) \<noteq> 0"
hoelzl@63593
  1685
      note ab = this[unfolded content_lt_nz[symmetric] content_pos_lt_eq]
hoelzl@63593
  1686
      then have ab': "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
hoelzl@63593
  1687
        by (auto intro!: less_imp_le)
hoelzl@63593
  1688
      show "F g d = g (cbox a b)"
hoelzl@63593
  1689
      proof (cases "division_points (cbox a b) d = {}")
hoelzl@63593
  1690
        case True
hoelzl@63593
  1691
        { fix u v and j :: 'b
hoelzl@63593
  1692
          assume j: "j \<in> Basis" and as: "cbox u v \<in> d"
hoelzl@63593
  1693
          then have "cbox u v \<noteq> {}"
hoelzl@63593
  1694
            using less.prems by blast
hoelzl@63593
  1695
          then have uv: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i" "u\<bullet>j \<le> v\<bullet>j"
hoelzl@63593
  1696
            using j unfolding box_ne_empty by auto
hoelzl@63593
  1697
          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)"
hoelzl@63593
  1698
            using as j by auto
hoelzl@63593
  1699
          have "(j, u\<bullet>j) \<notin> division_points (cbox a b) d"
hoelzl@63593
  1700
               "(j, v\<bullet>j) \<notin> division_points (cbox a b) d" using True by auto
hoelzl@63593
  1701
          note this[unfolded de_Morgan_conj division_points_def mem_Collect_eq split_conv interval_bounds[OF ab'] bex_simps]
hoelzl@63593
  1702
          note *[OF this(1)] *[OF this(2)] note this[unfolded interval_bounds[OF uv(1)]]
hoelzl@63593
  1703
          moreover
hoelzl@63593
  1704
          have "a\<bullet>j \<le> u\<bullet>j" "v\<bullet>j \<le> b\<bullet>j"
hoelzl@63593
  1705
            using division_ofD(2,2,3)[OF \<open>d division_of cbox a b\<close> as]
hoelzl@63593
  1706
            apply (metis j subset_box(1) uv(1))
hoelzl@63593
  1707
            by (metis \<open>cbox u v \<subseteq> cbox a b\<close> j subset_box(1) uv(1))
hoelzl@63593
  1708
          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"
hoelzl@63593
  1709
            unfolding not_less de_Morgan_disj using ab[rule_format,of j] uv(2) j by force }
hoelzl@63593
  1710
        then have d': "\<forall>i\<in>d. \<exists>u v. i = cbox u v \<and>
hoelzl@63593
  1711
          (\<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)"
hoelzl@63593
  1712
          unfolding forall_in_division[OF less.prems] by blast
hoelzl@63593
  1713
        have "(1/2) *\<^sub>R (a+b) \<in> cbox a b"
hoelzl@63593
  1714
          unfolding mem_box using ab by(auto intro!: less_imp_le simp: inner_simps)
hoelzl@63593
  1715
        note this[unfolded division_ofD(6)[OF \<open>d division_of cbox a b\<close>,symmetric] Union_iff]
hoelzl@63593
  1716
        then guess i .. note i=this
hoelzl@63593
  1717
        guess u v using d'[rule_format,OF i(1)] by (elim exE conjE) note uv=this
hoelzl@63593
  1718
        have "cbox a b \<in> d"
hoelzl@63593
  1719
        proof -
hoelzl@63593
  1720
          have "u = a" "v = b"
hoelzl@63593
  1721
            unfolding euclidean_eq_iff[where 'a='b]
hoelzl@63593
  1722
          proof safe
hoelzl@63593
  1723
            fix j :: 'b
hoelzl@63593
  1724
            assume j: "j \<in> Basis"
hoelzl@63593
  1725
            note i(2)[unfolded uv mem_box,rule_format,of j]
hoelzl@63593
  1726
            then show "u \<bullet> j = a \<bullet> j" and "v \<bullet> j = b \<bullet> j"
hoelzl@63593
  1727
              using uv(2)[rule_format,of j] j by (auto simp: inner_simps)
hoelzl@63593
  1728
          qed
hoelzl@63593
  1729
          then have "i = cbox a b" using uv by auto
hoelzl@63593
  1730
          then show ?thesis using i by auto
hoelzl@63593
  1731
        qed
hoelzl@63593
  1732
        then have deq: "d = insert (cbox a b) (d - {cbox a b})"
hoelzl@63593
  1733
          by auto
hoelzl@63593
  1734
        have "F g (d - {cbox a b}) = \<^bold>1"
hoelzl@63593
  1735
        proof (intro neutral ballI)
hoelzl@63593
  1736
          fix x
hoelzl@63593
  1737
          assume x: "x \<in> d - {cbox a b}"
hoelzl@63593
  1738
          then have "x\<in>d"
hoelzl@63593
  1739
            by auto note d'[rule_format,OF this]
hoelzl@63593
  1740
          then guess u v by (elim exE conjE) note uv=this
hoelzl@63593
  1741
          have "u \<noteq> a \<or> v \<noteq> b"
hoelzl@63593
  1742
            using x[unfolded uv] by auto
hoelzl@63593
  1743
          then obtain j where "u\<bullet>j \<noteq> a\<bullet>j \<or> v\<bullet>j \<noteq> b\<bullet>j" and j: "j \<in> Basis"
hoelzl@63593
  1744
            unfolding euclidean_eq_iff[where 'a='b] by auto
hoelzl@63593
  1745
          then have "u\<bullet>j = v\<bullet>j"
hoelzl@63593
  1746
            using uv(2)[rule_format,OF j] by auto
hoelzl@63593
  1747
          then have "content (cbox u v) = 0"
hoelzl@63593
  1748
            unfolding content_eq_0 using j
hoelzl@63593
  1749
            by force
hoelzl@63593
  1750
          then show "g x = \<^bold>1"
hoelzl@63593
  1751
            unfolding uv(1) by (rule operativeD(1)[OF g])
hoelzl@63593
  1752
        qed
hoelzl@63593
  1753
        then show "F g d = g (cbox a b)"
hoelzl@63593
  1754
          using division_ofD[OF less.prems]
hoelzl@63593
  1755
          apply (subst deq)
hoelzl@63593
  1756
          apply (subst insert)
hoelzl@63593
  1757
          apply auto
hoelzl@63593
  1758
          done
hoelzl@63593
  1759
      next
hoelzl@63593
  1760
        case False
hoelzl@63593
  1761
        then have "\<exists>x. x \<in> division_points (cbox a b) d"
hoelzl@63593
  1762
          by auto
hoelzl@63593
  1763
        then guess k c
hoelzl@63593
  1764
          unfolding split_paired_Ex division_points_def mem_Collect_eq split_conv
hoelzl@63593
  1765
          apply (elim exE conjE)
hoelzl@63593
  1766
          done
hoelzl@63593
  1767
        note this(2-4,1) note kc=this[unfolded interval_bounds[OF ab']]
hoelzl@63593
  1768
        from this(3) guess j .. note j=this
hoelzl@63593
  1769
        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> {}}"
hoelzl@63593
  1770
        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> {}}"
hoelzl@63593
  1771
        define cb where "cb = (\<Sum>i\<in>Basis. (if i = k then c else b\<bullet>i) *\<^sub>R i)"
hoelzl@63593
  1772
        define ca where "ca = (\<Sum>i\<in>Basis. (if i = k then c else a\<bullet>i) *\<^sub>R i)"
hoelzl@63593
  1773
        note division_points_psubset[OF \<open>d division_of cbox a b\<close> ab kc(1-2) j]
hoelzl@63593
  1774
        note psubset_card_mono[OF _ this(1)] psubset_card_mono[OF _ this(2)]
hoelzl@63593
  1775
        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})"
hoelzl@63593
  1776
          unfolding interval_split[OF kc(4)]
hoelzl@63593
  1777
          apply (rule_tac[!] "less.hyps"[rule_format])
hoelzl@63593
  1778
          using division_split[OF \<open>d division_of cbox a b\<close>, where k=k and c=c]
hoelzl@63593
  1779
          apply (simp_all add: interval_split kc d1_def d2_def division_points_finite[OF \<open>d division_of cbox a b\<close>])
hoelzl@63593
  1780
          done
hoelzl@63593
  1781
        { fix l y
hoelzl@63593
  1782
          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"
hoelzl@63593
  1783
          from division_ofD(4)[OF \<open>d division_of cbox a b\<close> this(1)] guess u v by (elim exE) note leq=this
hoelzl@63593
  1784
          have "g (l \<inter> {x. x \<bullet> k \<le> c}) = \<^bold>1"
hoelzl@63593
  1785
            unfolding leq interval_split[OF kc(4)]
hoelzl@63593
  1786
            apply (rule operativeD[OF g])
hoelzl@63593
  1787
            unfolding interval_split[symmetric, OF kc(4)]
hoelzl@63593
  1788
            using division_split_left_inj less as kc leq by blast
hoelzl@63593
  1789
        } note fxk_le = this
hoelzl@63593
  1790
        { fix l y
hoelzl@63593
  1791
          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"
hoelzl@63593
  1792
          from division_ofD(4)[OF \<open>d division_of cbox a b\<close> this(1)] guess u v by (elim exE) note leq=this
hoelzl@63593
  1793
          have "g (l \<inter> {x. x \<bullet> k \<ge> c}) = \<^bold>1"
hoelzl@63593
  1794
            unfolding leq interval_split[OF kc(4)]
hoelzl@63593
  1795
            apply (rule operativeD(1)[OF g])
hoelzl@63593
  1796
            unfolding interval_split[symmetric,OF kc(4)]
hoelzl@63593
  1797
            using division_split_right_inj less leq as kc by blast
hoelzl@63593
  1798
        } note fxk_ge = this
hoelzl@63593
  1799
        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> {}}"
hoelzl@63593
  1800
          using d1_def by auto
hoelzl@63593
  1801
        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> {}}"
hoelzl@63593
  1802
          using d2_def by auto
hoelzl@63593
  1803
        have "g (cbox a b) = F g d1 \<^bold>* F g d2" (is "_ = ?prev")
hoelzl@63593
  1804
          unfolding * using g kc(4) by blast
hoelzl@63593
  1805
        also have "F g d1 = F (\<lambda>l. g (l \<inter> {x. x\<bullet>k \<le> c})) d"
hoelzl@63593
  1806
          unfolding d1_alt using division_of_finite[OF less.prems] fxk_le
hoelzl@63593
  1807
          by (subst reindex_nontrivial) (auto intro!: mono_neutral_cong_left simp: operative_empty[OF g])
hoelzl@63593
  1808
        also have "F g d2 = F (\<lambda>l. g (l \<inter> {x. x\<bullet>k \<ge> c})) d"
hoelzl@63593
  1809
          unfolding d2_alt using division_of_finite[OF less.prems] fxk_ge
hoelzl@63593
  1810
          by (subst reindex_nontrivial) (auto intro!: mono_neutral_cong_left simp: operative_empty[OF g])
hoelzl@63593
  1811
        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})"
hoelzl@63593
  1812
          unfolding forall_in_division[OF \<open>d division_of cbox a b\<close>]
hoelzl@63593
  1813
          using g kc(4) by blast
hoelzl@63593
  1814
        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"
hoelzl@63593
  1815
          using * by (simp add: distrib)
hoelzl@63593
  1816
        finally show ?thesis by auto
hoelzl@63593
  1817
      qed
hoelzl@63593
  1818
    qed
hoelzl@63593
  1819
  qed
hoelzl@63593
  1820
qed
hoelzl@63593
  1821
hoelzl@63593
  1822
lemma (in comm_monoid_set) operative_tagged_division:
hoelzl@63593
  1823
  assumes f: "operative g" and d: "d tagged_division_of (cbox a b)"
hoelzl@63593
  1824
  shows "F (\<lambda>(x, l). g l) d = g (cbox a b)"
hoelzl@63593
  1825
  unfolding d[THEN division_of_tagged_division, THEN operative_division[OF f], symmetric]
hoelzl@63593
  1826
  by (simp add: f[THEN operativeD(1)] over_tagged_division_lemma[OF d])
hoelzl@63593
  1827
hoelzl@63593
  1828
lemma additive_content_division: "d division_of (cbox a b) \<Longrightarrow> setsum content d = content (cbox a b)"
hoelzl@63593
  1829
  by (metis operative_content setsum.operative_division)
hoelzl@63593
  1830
hoelzl@63593
  1831
lemma additive_content_tagged_division:
hoelzl@63593
  1832
  "d tagged_division_of (cbox a b) \<Longrightarrow> setsum (\<lambda>(x,l). content l) d = content (cbox a b)"
hoelzl@63593
  1833
  unfolding setsum.operative_tagged_division[OF operative_content, symmetric] by blast
hoelzl@63593
  1834
hoelzl@63593
  1835
lemma content_real_eq_0: "content {a .. b::real} = 0 \<longleftrightarrow> a \<ge> b"
hoelzl@63593
  1836
  by (metis atLeastatMost_empty_iff2 content_empty content_real diff_self eq_iff le_cases le_iff_diff_le_0)
hoelzl@63593
  1837
hoelzl@63593
  1838
lemma interval_real_split:
hoelzl@63593
  1839
  "{a .. b::real} \<inter> {x. x \<le> c} = {a .. min b c}"
hoelzl@63593
  1840
  "{a .. b} \<inter> {x. c \<le> x} = {max a c .. b}"
hoelzl@63593
  1841
  apply (metis Int_atLeastAtMostL1 atMost_def)
hoelzl@63593
  1842
  apply (metis Int_atLeastAtMostL2 atLeast_def)
hoelzl@63593
  1843
  done
hoelzl@63593
  1844
hoelzl@63593
  1845
lemma (in comm_monoid) operative_1_lt:
hoelzl@63593
  1846
  "operative (g :: real set \<Rightarrow> 'a) \<longleftrightarrow>
hoelzl@63593
  1847
    ((\<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}))"
hoelzl@63593
  1848
  apply (simp add: operative_def content_real_eq_0 atMost_def[symmetric] atLeast_def[symmetric]
hoelzl@63593
  1849
              del: content_real_if)
hoelzl@63593
  1850
proof safe
hoelzl@63593
  1851
  fix a b c :: real
hoelzl@63593
  1852
  assume *: "\<forall>a b c. g {a..b} = g {a..min b c} \<^bold>* g {max a c..b}"
hoelzl@63593
  1853
  assume "a < c" "c < b"
hoelzl@63593
  1854
  with *[rule_format, of a b c] show "g {a..c} \<^bold>* g {c..b} = g {a..b}"
hoelzl@63593
  1855
    by (simp add: less_imp_le min.absorb2 max.absorb2)
hoelzl@63593
  1856
next
hoelzl@63593
  1857
  fix a b c :: real
hoelzl@63593
  1858
  assume as: "\<forall>a b. b \<le> a \<longrightarrow> g {a..b} = \<^bold>1"
hoelzl@63593
  1859
    "\<forall>a b c. a < c \<and> c < b \<longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
hoelzl@63593
  1860
  from as(1)[rule_format, of 0 1] as(1)[rule_format, of a a for a] as(2)
hoelzl@63593
  1861
  have [simp]: "g {} = \<^bold>1" "\<And>a. g {a} = \<^bold>1"
hoelzl@63593
  1862
    "\<And>a b c. a < c \<Longrightarrow> c < b \<Longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
hoelzl@63593
  1863
    by auto
hoelzl@63593
  1864
  show "g {a..b} = g {a..min b c} \<^bold>* g {max a c..b}"
hoelzl@63593
  1865
    by (auto simp: min_def max_def le_less)
hoelzl@63593
  1866
qed
hoelzl@63593
  1867
hoelzl@63593
  1868
lemma (in comm_monoid) operative_1_le:
hoelzl@63593
  1869
  "operative (g :: real set \<Rightarrow> 'a) \<longleftrightarrow>
hoelzl@63593
  1870
    ((\<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}))"
hoelzl@63593
  1871
  unfolding operative_1_lt
hoelzl@63593
  1872
proof safe
hoelzl@63593
  1873
  fix a b c :: real
hoelzl@63593
  1874
  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"
hoelzl@63593
  1875
  show "g {a..c} \<^bold>* g {c..b} = g {a..b}"
hoelzl@63593
  1876
    apply (rule as(1)[rule_format])
hoelzl@63593
  1877
    using as(2-)
hoelzl@63593
  1878
    apply auto
hoelzl@63593
  1879
    done
hoelzl@63593
  1880
next
hoelzl@63593
  1881
  fix a b c :: real
hoelzl@63593
  1882
  assume "\<forall>a b. b \<le> a \<longrightarrow> g {a .. b} = \<^bold>1"
hoelzl@63593
  1883
    and "\<forall>a b c. a < c \<and> c < b \<longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
hoelzl@63593
  1884
    and "a \<le> c"
hoelzl@63593
  1885
    and "c \<le> b"
hoelzl@63593
  1886
  note as = this[rule_format]
hoelzl@63593
  1887
  show "g {a..c} \<^bold>* g {c..b} = g {a..b}"
hoelzl@63593
  1888
  proof (cases "c = a \<or> c = b")
hoelzl@63593
  1889
    case False
hoelzl@63593
  1890
    then show ?thesis
hoelzl@63593
  1891
      apply -
hoelzl@63593
  1892
      apply (subst as(2))
hoelzl@63593
  1893
      using as(3-)
hoelzl@63593
  1894
      apply auto
hoelzl@63593
  1895
      done
hoelzl@63593
  1896
  next
hoelzl@63593
  1897
    case True
hoelzl@63593
  1898
    then show ?thesis
hoelzl@63593
  1899
    proof
hoelzl@63593
  1900
      assume *: "c = a"
hoelzl@63593
  1901
      then have "g {a .. c} = \<^bold>1"
hoelzl@63593
  1902
        apply -
hoelzl@63593
  1903
        apply (rule as(1)[rule_format])
hoelzl@63593
  1904
        apply auto
hoelzl@63593
  1905
        done
hoelzl@63593
  1906
      then show ?thesis
hoelzl@63593
  1907
        unfolding * by auto
hoelzl@63593
  1908
    next
hoelzl@63593
  1909
      assume *: "c = b"
hoelzl@63593
  1910
      then have "g {c .. b} = \<^bold>1"
hoelzl@63593
  1911
        apply -
hoelzl@63593
  1912
        apply (rule as(1)[rule_format])
hoelzl@63593
  1913
        apply auto
hoelzl@63593
  1914
        done
hoelzl@63593
  1915
      then show ?thesis
hoelzl@63593
  1916
        unfolding * by auto
hoelzl@63593
  1917
    qed
hoelzl@63593
  1918
  qed
hoelzl@63593
  1919
qed
himmelma@35172
  1920
wenzelm@60420
  1921
subsection \<open>Fine-ness of a partition w.r.t. a gauge.\<close>
himmelma@35172
  1922
wenzelm@53408
  1923
definition fine  (infixr "fine" 46)
wenzelm@53408
  1924
  where "d fine s \<longleftrightarrow> (\<forall>(x,k) \<in> s. k \<subseteq> d x)"
wenzelm@53408
  1925
wenzelm@53408
  1926
lemma fineI:
wenzelm@53408
  1927
  assumes "\<And>x k. (x, k) \<in> s \<Longrightarrow> k \<subseteq> d x"
wenzelm@53408
  1928
  shows "d fine s"
wenzelm@53408
  1929
  using assms unfolding fine_def by auto
wenzelm@53408
  1930
wenzelm@53408
  1931
lemma fineD[dest]:
wenzelm@53408
  1932
  assumes "d fine s"
wenzelm@53408
  1933
  shows "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> d x"
wenzelm@53408
  1934
  using assms unfolding fine_def by auto
himmelma@35172
  1935
himmelma@35172
  1936
lemma fine_inter: "(\<lambda>x. d1 x \<inter> d2 x) fine p \<longleftrightarrow> d1 fine p \<and> d2 fine p"
himmelma@35172
  1937
  unfolding fine_def by auto
himmelma@35172
  1938
himmelma@35172
  1939
lemma fine_inters:
wenzelm@60585
  1940
 "(\<lambda>x. \<Inter>{f d x | d.  d \<in> s}) fine p \<longleftrightarrow> (\<forall>d\<in>s. (f d) fine p)"
himmelma@35172
  1941
  unfolding fine_def by blast
himmelma@35172
  1942
wenzelm@53408
  1943
lemma fine_union: "d fine p1 \<Longrightarrow> d fine p2 \<Longrightarrow> d fine (p1 \<union> p2)"
himmelma@35172
  1944
  unfolding fine_def by blast
himmelma@35172
  1945
wenzelm@53408
  1946
lemma fine_unions: "(\<And>p. p \<in> ps \<Longrightarrow> d fine p) \<Longrightarrow> d fine (\<Union>ps)"
himmelma@35172
  1947
  unfolding fine_def by auto
himmelma@35172
  1948
wenzelm@53408
  1949
lemma fine_subset: "p \<subseteq> q \<Longrightarrow> d fine q \<Longrightarrow> d fine p"
himmelma@35172
  1950
  unfolding fine_def by blast
himmelma@35172
  1951
wenzelm@60420
  1952
subsection \<open>Some basic combining lemmas.\<close>
himmelma@35172
  1953
himmelma@35172
  1954
lemma tagged_division_unions_exists:
wenzelm@53409
  1955
  assumes "finite iset"
wenzelm@53409
  1956
    and "\<forall>i\<in>iset. \<exists>p. p tagged_division_of i \<and> d fine p"
wenzelm@53409
  1957
    and "\<forall>i1\<in>iset. \<forall>i2\<in>iset. i1 \<noteq> i2 \<longrightarrow> interior i1 \<inter> interior i2 = {}"
wenzelm@53409
  1958
    and "\<Union>iset = i"
wenzelm@53409
  1959
   obtains p where "p tagged_division_of i" and "d fine p"
wenzelm@53409
  1960
proof -
wenzelm@53409
  1961
  obtain pfn where pfn:
wenzelm@53409
  1962
    "\<And>x. x \<in> iset \<Longrightarrow> pfn x tagged_division_of x"
wenzelm@53409
  1963
    "\<And>x. x \<in> iset \<Longrightarrow> d fine pfn x"
wenzelm@53409
  1964
    using bchoice[OF assms(2)] by auto
wenzelm@53409
  1965
  show thesis
wenzelm@53409
  1966
    apply (rule_tac p="\<Union>(pfn ` iset)" in that)
lp15@60384
  1967
    using assms(1) assms(3) assms(4) pfn(1) tagged_division_unions apply force
lp15@60384
  1968
    by (metis (mono_tags, lifting) fine_unions imageE pfn(2))
himmelma@35172
  1969
qed
himmelma@35172
  1970
wenzelm@53409
  1971
wenzelm@60420
  1972
subsection \<open>The set we're concerned with must be closed.\<close>
himmelma@35172
  1973
wenzelm@53409
  1974
lemma division_of_closed:
immler@56189
  1975
  fixes i :: "'n::euclidean_space set"
wenzelm@53409
  1976
  shows "s division_of i \<Longrightarrow> closed i"
nipkow@44890
  1977
  unfolding division_of_def by fastforce
himmelma@35172
  1978
wenzelm@60420
  1979
subsection \<open>General bisection principle for intervals; might be useful elsewhere.\<close>
himmelma@35172
  1980
wenzelm@53409
  1981
lemma interval_bisection_step:
immler@56188
  1982
  fixes type :: "'a::euclidean_space"
wenzelm@53409
  1983
  assumes "P {}"
wenzelm@53409
  1984
    and "\<forall>s t. P s \<and> P t \<and> interior(s) \<inter> interior(t) = {} \<longrightarrow> P (s \<union> t)"
immler@56188
  1985
    and "\<not> P (cbox a (b::'a))"
immler@56188
  1986
  obtains c d where "\<not> P (cbox c d)"
wenzelm@53409
  1987
    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"
wenzelm@53409
  1988
proof -
immler@56188
  1989
  have "cbox a b \<noteq> {}"
immler@54776
  1990
    using assms(1,3) by metis
wenzelm@53409
  1991
  then have ab: "\<And>i. i\<in>Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
immler@56188
  1992
    by (force simp: mem_box)
lp15@60428
  1993
  { fix f
lp15@60428
  1994
    have "\<lbrakk>finite f;
lp15@60428
  1995
           \<And>s. s\<in>f \<Longrightarrow> P s;
lp15@60428
  1996
           \<And>s. s\<in>f \<Longrightarrow> \<exists>a b. s = cbox a b;
lp15@60428
  1997
           \<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)"
wenzelm@53409
  1998
    proof (induct f rule: finite_induct)
wenzelm@53409
  1999
      case empty
wenzelm@53409
  2000
      show ?case
wenzelm@53409
  2001
        using assms(1) by auto
wenzelm@53409
  2002
    next
wenzelm@53409
  2003
      case (insert x f)
wenzelm@53409
  2004
      show ?case
wenzelm@53409
  2005
        unfolding Union_insert
wenzelm@53409
  2006
        apply (rule assms(2)[rule_format])
lp15@60384
  2007
        using inter_interior_unions_intervals [of f "interior x"]
lp15@60384
  2008
        apply (auto simp: insert)
lp15@60428
  2009
        by (metis IntI empty_iff insert.hyps(2) insert.prems(3) insert_iff)
lp15@60428
  2010
    qed
lp15@60428
  2011
  } note UN_cases = this
immler@56188
  2012
  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>
wenzelm@53409
  2013
    (c\<bullet>i = (a\<bullet>i + b\<bullet>i) / 2) \<and> (d\<bullet>i = b\<bullet>i)}"
hoelzl@50526
  2014
  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"
wenzelm@53409
  2015
  {
immler@56188
  2016
    presume "\<forall>c d. ?PP c d \<longrightarrow> P (cbox c d) \<Longrightarrow> False"
wenzelm@53409
  2017
    then show thesis
wenzelm@53409
  2018
      unfolding atomize_not not_all
lp15@60384
  2019
      by (blast intro: that)
wenzelm@53409
  2020
  }
immler@56188
  2021
  assume as: "\<forall>c d. ?PP c d \<longrightarrow> P (cbox c d)"
wenzelm@60585
  2022
  have "P (\<Union>?A)"
lp15@60428
  2023
  proof (rule UN_cases)
immler@56188
  2024
    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)
immler@56188
  2025
      (\<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}"
wenzelm@53409
  2026
    have "?A \<subseteq> ?B"
wenzelm@53409
  2027
    proof
wenzelm@61165
  2028
      fix x
wenzelm@61165
  2029
      assume "x \<in> ?A"
lp15@60615
  2030
      then obtain c d
lp15@60428
  2031
        where x:  "x = cbox c d"
lp15@60428
  2032
                  "\<And>i. i \<in> Basis \<Longrightarrow>
lp15@60428
  2033
                        c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
lp15@60428
  2034
                        c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i" by blast
wenzelm@53409
  2035
      show "x \<in> ?B"
lp15@60428
  2036
        unfolding image_iff x
wenzelm@53409
  2037
        apply (rule_tac x="{i. i\<in>Basis \<and> c\<bullet>i = a\<bullet>i}" in bexI)
lp15@60428
  2038
        apply (rule arg_cong2 [where f = cbox])
lp15@60428
  2039
        using x(2) ab
lp15@60428
  2040
        apply (auto simp add: euclidean_eq_iff[where 'a='a])
lp15@60428
  2041
        by fastforce
wenzelm@53409
  2042
    qed
wenzelm@53409
  2043
    then show "finite ?A"
wenzelm@53409
  2044
      by (rule finite_subset) auto
lp15@60428
  2045
  next
wenzelm@53409
  2046
    fix s
wenzelm@53409
  2047
    assume "s \<in> ?A"
lp15@60428
  2048
    then obtain c d
lp15@60428
  2049
      where s: "s = cbox c d"
lp15@60428
  2050
               "\<And>i. i \<in> Basis \<Longrightarrow>
lp15@60428
  2051
                     c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
lp15@60428
  2052
                     c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i"
wenzelm@53409
  2053
      by blast
wenzelm@53409
  2054
    show "P s"
wenzelm@53409
  2055
      unfolding s
wenzelm@53409
  2056
      apply (rule as[rule_format])
lp15@60394
  2057
      using ab s(2) by force
immler@56188
  2058
    show "\<exists>a b. s = cbox a b"
wenzelm@53409
  2059
      unfolding s by auto
wenzelm@53409
  2060
    fix t
wenzelm@53409
  2061
    assume "t \<in> ?A"
wenzelm@53409
  2062
    then obtain e f where t:
immler@56188
  2063
      "t = cbox e f"
wenzelm@53409
  2064
      "\<And>i. i \<in> Basis \<Longrightarrow>
wenzelm@53409
  2065
        e \<bullet> i = a \<bullet> i \<and> f \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
wenzelm@53409
  2066
        e \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> f \<bullet> i = b \<bullet> i"
wenzelm@53409
  2067
      by blast
wenzelm@53409
  2068
    assume "s \<noteq> t"
wenzelm@53409
  2069
    then have "\<not> (c = e \<and> d = f)"
wenzelm@53409
  2070
      unfolding s t by auto
wenzelm@53409
  2071
    then obtain i where "c\<bullet>i \<noteq> e\<bullet>i \<or> d\<bullet>i \<noteq> f\<bullet>i" and i': "i \<in> Basis"
hoelzl@50526
  2072
      unfolding euclidean_eq_iff[where 'a='a] by auto
wenzelm@53409
  2073
    then have i: "c\<bullet>i \<noteq> e\<bullet>i" "d\<bullet>i \<noteq> f\<bullet>i"
lp15@60394
  2074
      using s(2) t(2) apply fastforce
wenzelm@60420
  2075
      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
wenzelm@53409
  2076
    have *: "\<And>s t. (\<And>a. a \<in> s \<Longrightarrow> a \<in> t \<Longrightarrow> False) \<Longrightarrow> s \<inter> t = {}"
wenzelm@53409
  2077
      by auto
wenzelm@53409
  2078
    show "interior s \<inter> interior t = {}"
immler@56188
  2079
      unfolding s t interior_cbox
wenzelm@53409
  2080
    proof (rule *)
wenzelm@53409
  2081
      fix x
immler@54775
  2082
      assume "x \<in> box c d" "x \<in> box e f"
wenzelm@53409
  2083
      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"
immler@56188
  2084
        unfolding mem_box using i'
lp15@60394
  2085
        by force+
lp15@60394
  2086
      show False  using s(2)[OF i']
lp15@60394
  2087
      proof safe
wenzelm@53409
  2088
        assume as: "c \<bullet> i = a \<bullet> i" "d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2"
wenzelm@53409
  2089
        show False
wenzelm@53409
  2090
          using t(2)[OF i'] and i x unfolding as by (fastforce simp add:field_simps)
wenzelm@53409
  2091
      next
wenzelm@53409
  2092
        assume as: "c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2" "d \<bullet> i = b \<bullet> i"
wenzelm@53409
  2093
        show False
wenzelm@53409
  2094
          using t(2)[OF i'] and i x unfolding as by(fastforce simp add:field_simps)
wenzelm@53409
  2095
      qed
wenzelm@53409
  2096
    qed
wenzelm@53409
  2097
  qed
wenzelm@60585
  2098
  also have "\<Union>?A = cbox a b"
wenzelm@53409
  2099
  proof (rule set_eqI,rule)
wenzelm@53409
  2100
    fix x
wenzelm@53409
  2101
    assume "x \<in> \<Union>?A"
wenzelm@53409
  2102
    then obtain c d where x:
immler@56188
  2103
      "x \<in> cbox c d"
wenzelm@53409
  2104
      "\<And>i. i \<in> Basis \<Longrightarrow>
wenzelm@53409
  2105
        c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
lp15@60615
  2106
        c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i"
lp15@60394
  2107
      by blast
immler@56188
  2108
    show "x\<in>cbox a b"
immler@56188
  2109
      unfolding mem_box
wenzelm@53409
  2110
    proof safe
wenzelm@53409
  2111
      fix i :: 'a
wenzelm@53409
  2112
      assume i: "i \<in> Basis"
wenzelm@53409
  2113
      then show "a \<bullet> i \<le> x \<bullet> i" "x \<bullet> i \<le> b \<bullet> i"
immler@56188
  2114
        using x(2)[OF i] x(1)[unfolded mem_box,THEN bspec, OF i] by auto
wenzelm@53409
  2115
    qed
wenzelm@53409
  2116
  next
wenzelm@53409
  2117
    fix x
immler@56188
  2118
    assume x: "x \<in> cbox a b"
wenzelm@53409
  2119
    have "\<forall>i\<in>Basis.
wenzelm@53409
  2120
      \<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"
wenzelm@53409
  2121
      (is "\<forall>i\<in>Basis. \<exists>c d. ?P i c d")
immler@56188
  2122
      unfolding mem_box
hoelzl@50526
  2123
    proof
wenzelm@53409
  2124
      fix i :: 'a
wenzelm@53409
  2125
      assume i: "i \<in> Basis"
hoelzl@50526
  2126
      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)"
immler@56188
  2127
        using x[unfolded mem_box,THEN bspec, OF i] by auto
wenzelm@53409
  2128
      then show "\<exists>c d. ?P i c d"
wenzelm@53409
  2129
        by blast
hoelzl@50526
  2130
    qed
wenzelm@53409
  2131
    then show "x\<in>\<Union>?A"
hoelzl@50526
  2132
      unfolding Union_iff Bex_def mem_Collect_eq choice_Basis_iff
lp15@60384
  2133
      apply auto
immler@56188
  2134
      apply (rule_tac x="cbox xa xaa" in exI)
immler@56188
  2135
      unfolding mem_box
wenzelm@53409
  2136
      apply auto
wenzelm@53409
  2137
      done
wenzelm@53409
  2138
  qed
wenzelm@53409
  2139
  finally show False
wenzelm@53409
  2140
    using assms by auto
wenzelm@53409
  2141
qed
wenzelm@53409
  2142
wenzelm@53409
  2143
lemma interval_bisection:
immler@56188
  2144
  fixes type :: "'a::euclidean_space"
wenzelm@53409
  2145
  assumes "P {}"
wenzelm@53409
  2146
    and "(\<forall>s t. P s \<and> P t \<and> interior(s) \<inter> interior(t) = {} \<longrightarrow> P(s \<union> t))"
immler@56188
  2147
    and "\<not> P (cbox a (b::'a))"
immler@56188
  2148
  obtains x where "x \<in> cbox a b"
immler@56188
  2149
    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)"
immler@56188
  2150
proof -
immler@56188
  2151
  have "\<forall>x. \<exists>y. \<not> P (cbox (fst x) (snd x)) \<longrightarrow> (\<not> P (cbox (fst y) (snd y)) \<and>
hoelzl@50526
  2152
    (\<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>
wenzelm@61165
  2153
       2 * (snd y\<bullet>i - fst y\<bullet>i) \<le> snd x\<bullet>i - fst x\<bullet>i))" (is "\<forall>x. ?P x")
wenzelm@53409
  2154
  proof
wenzelm@61165
  2155
    show "?P x" for x
wenzelm@61165
  2156
    proof (cases "P (cbox (fst x) (snd x))")
wenzelm@61165
  2157
      case True
wenzelm@61165
  2158
      then show ?thesis by auto
wenzelm@53409
  2159
    next
wenzelm@61165
  2160
      case as: False
immler@56188
  2161
      obtain c d where "\<not> P (cbox c d)"
wenzelm@53409
  2162
        "\<forall>i\<in>Basis.
wenzelm@53409
  2163
           fst x \<bullet> i \<le> c \<bullet> i \<and>
wenzelm@53409
  2164
           c \<bullet> i \<le> d \<bullet> i \<and>
wenzelm@53409
  2165
           d \<bullet> i \<le> snd x \<bullet> i \<and>
wenzelm@53409
  2166
           2 * (d \<bullet> i - c \<bullet> i) \<le> snd x \<bullet> i - fst x \<bullet> i"
wenzelm@53409
  2167
        by (rule interval_bisection_step[of P, OF assms(1-2) as])
wenzelm@53409
  2168
      then show ?thesis
wenzelm@53409
  2169
        apply -
wenzelm@53409
  2170
        apply (rule_tac x="(c,d)" in exI)
wenzelm@53409
  2171
        apply auto
wenzelm@53409
  2172
        done
wenzelm@53409
  2173
    qed
wenzelm@53409
  2174
  qed
wenzelm@55751
  2175
  then obtain f where f:
wenzelm@55751
  2176
    "\<forall>x.
immler@56188
  2177
      \<not> P (cbox (fst x) (snd x)) \<longrightarrow>
immler@56188
  2178
      \<not> P (cbox (fst (f x)) (snd (f x))) \<and>
wenzelm@55751
  2179
        (\<forall>i\<in>Basis.
wenzelm@55751
  2180
            fst x \<bullet> i \<le> fst (f x) \<bullet> i \<and>
wenzelm@55751
  2181
            fst (f x) \<bullet> i \<le> snd (f x) \<bullet> i \<and>
wenzelm@55751
  2182
            snd (f x) \<bullet> i \<le> snd x \<bullet> i \<and>
wenzelm@55751
  2183
            2 * (snd (f x) \<bullet> i - fst (f x) \<bullet> i) \<le> snd x \<bullet> i - fst x \<bullet> i)"
wenzelm@53409
  2184
    apply -
wenzelm@53409
  2185
    apply (drule choice)
wenzelm@55751
  2186
    apply blast
wenzelm@55751
  2187
    done
wenzelm@63040
  2188
  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
immler@56188
  2189
  have "A 0 = a" "B 0 = b" "\<And>n. \<not> P (cbox (A(Suc n)) (B(Suc n))) \<and>
wenzelm@53399
  2190
    (\<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>
hoelzl@50526
  2191
    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")
wenzelm@53409
  2192
  proof -
wenzelm@53409
  2193
    show "A 0 = a" "B 0 = b"