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