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