src/HOL/Multivariate_Analysis/Integration.thy
author wenzelm
Sun Sep 13 21:06:58 2015 +0200 (2015-09-13)
changeset 61167 34f782641caa
parent 61166 5976fe402824
child 61204 3e491e34a62e
permissions -rw-r--r--
tuned proofs;
wenzelm@53399
     1
(*  Author:     John Harrison
lp15@60428
     2
    Author:     Robert Himmelmann, TU Muenchen (Translation from HOL light); proofs reworked by LCP
wenzelm@53399
     3
*)
wenzelm@53399
     4
wenzelm@60420
     5
section \<open>Kurzweil-Henstock Gauge Integration in many dimensions.\<close>
himmelma@35172
     6
hoelzl@35292
     7
theory Integration
wenzelm@41413
     8
imports
wenzelm@41413
     9
  Derivative
wenzelm@41413
    10
  "~~/src/HOL/Library/Indicator_Function"
himmelma@35172
    11
begin
himmelma@35172
    12
lp15@60810
    13
lemma cSup_abs_le: (* TODO: move to Conditionally_Complete_Lattices.thy? *)
hoelzl@51518
    14
  fixes S :: "real set"
lp15@60810
    15
  shows "S \<noteq> {} \<Longrightarrow> (\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
hoelzl@54258
    16
  by (auto simp add: abs_le_interval_iff intro: cSup_least) (metis cSup_upper2 bdd_aboveI)
hoelzl@51518
    17
wenzelm@61165
    18
lemma cInf_abs_ge:
hoelzl@51518
    19
  fixes S :: "real set"
lp15@60810
    20
  shows "S \<noteq> {} \<Longrightarrow> (\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Inf S\<bar> \<le> a"
lp15@60810
    21
  using cSup_abs_le [of "uminus ` S"]
lp15@60810
    22
  by (fastforce simp add: Inf_real_def)
lp15@60810
    23
lp15@60810
    24
lemma cSup_asclose:
hoelzl@51475
    25
  fixes S :: "real set"
wenzelm@53399
    26
  assumes S: "S \<noteq> {}"
wenzelm@53399
    27
    and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e"
wenzelm@53399
    28
  shows "\<bar>Sup S - l\<bar> \<le> e"
wenzelm@53399
    29
proof -
wenzelm@53399
    30
  have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e"
wenzelm@53399
    31
    by arith
hoelzl@54263
    32
  have "bdd_above S"
hoelzl@54263
    33
    using b by (auto intro!: bdd_aboveI[of _ "l + e"])
hoelzl@54263
    34
  with S b show ?thesis
hoelzl@54263
    35
    unfolding th by (auto intro!: cSup_upper2 cSup_least)
hoelzl@51518
    36
qed
hoelzl@51518
    37
lp15@60810
    38
lemma cInf_asclose:
hoelzl@51518
    39
  fixes S :: "real set"
wenzelm@53399
    40
  assumes S: "S \<noteq> {}"
wenzelm@53399
    41
    and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e"
wenzelm@53399
    42
  shows "\<bar>Inf S - l\<bar> \<le> e"
hoelzl@51518
    43
proof -
hoelzl@51518
    44
  have "\<bar>- Sup (uminus ` S) - l\<bar> =  \<bar>Sup (uminus ` S) - (-l)\<bar>"
hoelzl@51518
    45
    by auto
wenzelm@53399
    46
  also have "\<dots> \<le> e"
wenzelm@53399
    47
    apply (rule cSup_asclose)
haftmann@54230
    48
    using abs_minus_add_cancel b by (auto simp add: S)
hoelzl@51518
    49
  finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
wenzelm@53399
    50
  then show ?thesis
hoelzl@51518
    51
    by (simp add: Inf_real_def)
hoelzl@51518
    52
qed
hoelzl@51518
    53
wenzelm@53399
    54
lemma cSup_finite_ge_iff:
wenzelm@53399
    55
  fixes S :: "real set"
wenzelm@53399
    56
  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Sup S \<longleftrightarrow> (\<exists>x\<in>S. a \<le> x)"
hoelzl@51518
    57
  by (metis cSup_eq_Max Max_ge_iff)
hoelzl@51475
    58
wenzelm@53399
    59
lemma cSup_finite_le_iff:
wenzelm@53399
    60
  fixes S :: "real set"
wenzelm@53399
    61
  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Sup S \<longleftrightarrow> (\<forall>x\<in>S. a \<ge> x)"
hoelzl@51518
    62
  by (metis cSup_eq_Max Max_le_iff)
hoelzl@51518
    63
wenzelm@53399
    64
lemma cInf_finite_ge_iff:
wenzelm@53399
    65
  fixes S :: "real set"
wenzelm@53399
    66
  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall>x\<in>S. a \<le> x)"
hoelzl@51518
    67
  by (metis cInf_eq_Min Min_ge_iff)
hoelzl@51518
    68
wenzelm@53399
    69
lemma cInf_finite_le_iff:
wenzelm@53399
    70
  fixes S :: "real set"
wenzelm@53399
    71
  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists>x\<in>S. a \<ge> x)"
hoelzl@51518
    72
  by (metis cInf_eq_Min Min_le_iff)
hoelzl@51475
    73
hoelzl@37489
    74
(*declare not_less[simp] not_le[simp]*)
hoelzl@37489
    75
hoelzl@37489
    76
lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
hoelzl@37489
    77
  scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff
huffman@44282
    78
  scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one
hoelzl@37489
    79
hoelzl@37489
    80
lemma real_arch_invD:
hoelzl@37489
    81
  "0 < (e::real) \<Longrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
wenzelm@49675
    82
  by (subst(asm) real_arch_inv)
wenzelm@49675
    83
wenzelm@49675
    84
wenzelm@60420
    85
subsection \<open>Sundries\<close>
himmelma@36243
    86
himmelma@35172
    87
lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
himmelma@35172
    88
lemma conjunctD3: assumes "a \<and> b \<and> c" shows a b c using assms by auto
himmelma@35172
    89
lemma conjunctD4: assumes "a \<and> b \<and> c \<and> d" shows a b c d using assms by auto
himmelma@35172
    90
lemma conjunctD5: assumes "a \<and> b \<and> c \<and> d \<and> e" shows a b c d e using assms by auto
himmelma@35172
    91
wenzelm@53399
    92
declare norm_triangle_ineq4[intro]
wenzelm@53399
    93
wenzelm@53399
    94
lemma simple_image: "{f x |x . x \<in> s} = f ` s"
wenzelm@53399
    95
  by blast
himmelma@36243
    96
wenzelm@49970
    97
lemma linear_simps:
wenzelm@49970
    98
  assumes "bounded_linear f"
wenzelm@49970
    99
  shows
wenzelm@49970
   100
    "f (a + b) = f a + f b"
wenzelm@49970
   101
    "f (a - b) = f a - f b"
wenzelm@49970
   102
    "f 0 = 0"
wenzelm@49970
   103
    "f (- a) = - f a"
wenzelm@49970
   104
    "f (s *\<^sub>R v) = s *\<^sub>R (f v)"
huffman@53600
   105
proof -
huffman@53600
   106
  interpret f: bounded_linear f by fact
huffman@53600
   107
  show "f (a + b) = f a + f b" by (rule f.add)
huffman@53600
   108
  show "f (a - b) = f a - f b" by (rule f.diff)
huffman@53600
   109
  show "f 0 = 0" by (rule f.zero)
huffman@53600
   110
  show "f (- a) = - f a" by (rule f.minus)
huffman@53600
   111
  show "f (s *\<^sub>R v) = s *\<^sub>R (f v)" by (rule f.scaleR)
huffman@53600
   112
qed
wenzelm@49675
   113
wenzelm@49675
   114
lemma bounded_linearI:
wenzelm@49675
   115
  assumes "\<And>x y. f (x + y) = f x + f y"
wenzelm@53399
   116
    and "\<And>r x. f (r *\<^sub>R x) = r *\<^sub>R f x"
wenzelm@53399
   117
    and "\<And>x. norm (f x) \<le> norm x * K"
himmelma@36243
   118
  shows "bounded_linear f"
huffman@53600
   119
  using assms by (rule bounded_linear_intro) (* FIXME: duplicate *)
hoelzl@51348
   120
hoelzl@50526
   121
lemma bounded_linear_component [intro]: "bounded_linear (\<lambda>x::'a::euclidean_space. x \<bullet> k)"
hoelzl@50526
   122
  by (rule bounded_linear_inner_left)
himmelma@36243
   123
himmelma@36243
   124
lemma transitive_stepwise_lt_eq:
himmelma@36243
   125
  assumes "(\<And>x y z::nat. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z)"
wenzelm@53399
   126
  shows "((\<forall>m. \<forall>n>m. R m n) \<longleftrightarrow> (\<forall>n. R n (Suc n)))"
wenzelm@53399
   127
  (is "?l = ?r")
wenzelm@53408
   128
proof safe
wenzelm@49675
   129
  assume ?r
wenzelm@49675
   130
  fix n m :: nat
wenzelm@49675
   131
  assume "m < n"
wenzelm@49675
   132
  then show "R m n"
wenzelm@49675
   133
  proof (induct n arbitrary: m)
wenzelm@53399
   134
    case 0
wenzelm@53399
   135
    then show ?case by auto
wenzelm@53399
   136
  next
wenzelm@49675
   137
    case (Suc n)
wenzelm@53399
   138
    show ?case
wenzelm@49675
   139
    proof (cases "m < n")
wenzelm@49675
   140
      case True
wenzelm@49675
   141
      show ?thesis
wenzelm@49675
   142
        apply (rule assms[OF Suc(1)[OF True]])
wenzelm@60420
   143
        using \<open>?r\<close>
wenzelm@50945
   144
        apply auto
wenzelm@49675
   145
        done
wenzelm@49675
   146
    next
wenzelm@49675
   147
      case False
wenzelm@53408
   148
      then have "m = n"
wenzelm@53408
   149
        using Suc(2) by auto
wenzelm@53408
   150
      then show ?thesis
wenzelm@60420
   151
        using \<open>?r\<close> by auto
wenzelm@49675
   152
    qed
wenzelm@53399
   153
  qed
wenzelm@49675
   154
qed auto
himmelma@36243
   155
himmelma@36243
   156
lemma transitive_stepwise_gt:
wenzelm@53408
   157
  assumes "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" "\<And>n. R n (Suc n)"
himmelma@36243
   158
  shows "\<forall>n>m. R m n"
wenzelm@49675
   159
proof -
wenzelm@49675
   160
  have "\<forall>m. \<forall>n>m. R m n"
wenzelm@49675
   161
    apply (subst transitive_stepwise_lt_eq)
lp15@60384
   162
    apply (blast intro: assms)+
wenzelm@49675
   163
    done
wenzelm@49970
   164
  then show ?thesis by auto
wenzelm@49675
   165
qed
himmelma@36243
   166
himmelma@36243
   167
lemma transitive_stepwise_le_eq:
himmelma@36243
   168
  assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
wenzelm@53399
   169
  shows "(\<forall>m. \<forall>n\<ge>m. R m n) \<longleftrightarrow> (\<forall>n. R n (Suc n))"
wenzelm@53399
   170
  (is "?l = ?r")
wenzelm@49675
   171
proof safe
wenzelm@49675
   172
  assume ?r
wenzelm@49675
   173
  fix m n :: nat
wenzelm@49675
   174
  assume "m \<le> n"
wenzelm@53408
   175
  then show "R m n"
wenzelm@49675
   176
  proof (induct n arbitrary: m)
wenzelm@49970
   177
    case 0
wenzelm@49970
   178
    with assms show ?case by auto
wenzelm@49970
   179
  next
wenzelm@49675
   180
    case (Suc n)
wenzelm@49675
   181
    show ?case
wenzelm@49675
   182
    proof (cases "m \<le> n")
wenzelm@49675
   183
      case True
wenzelm@60420
   184
      with Suc.hyps \<open>\<forall>n. R n (Suc n)\<close> assms show ?thesis
lp15@60384
   185
        by blast
wenzelm@49675
   186
    next
wenzelm@49675
   187
      case False
wenzelm@53408
   188
      then have "m = Suc n"
wenzelm@53408
   189
        using Suc(2) by auto
wenzelm@53408
   190
      then show ?thesis
wenzelm@53408
   191
        using assms(1) by auto
wenzelm@49675
   192
    qed
wenzelm@49970
   193
  qed
wenzelm@49675
   194
qed auto
himmelma@36243
   195
himmelma@36243
   196
lemma transitive_stepwise_le:
wenzelm@53408
   197
  assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
wenzelm@53408
   198
    and "\<And>n. R n (Suc n)"
himmelma@36243
   199
  shows "\<forall>n\<ge>m. R m n"
wenzelm@49675
   200
proof -
wenzelm@49675
   201
  have "\<forall>m. \<forall>n\<ge>m. R m n"
wenzelm@49675
   202
    apply (subst transitive_stepwise_le_eq)
lp15@60384
   203
    apply (blast intro: assms)+
wenzelm@49675
   204
    done
wenzelm@49970
   205
  then show ?thesis by auto
wenzelm@49675
   206
qed
wenzelm@49675
   207
himmelma@36243
   208
wenzelm@60420
   209
subsection \<open>Some useful lemmas about intervals.\<close>
himmelma@35172
   210
immler@56188
   211
lemma empty_as_interval: "{} = cbox One (0::'a::euclidean_space)"
immler@56188
   212
  using nonempty_Basis
immler@56188
   213
  by (fastforce simp add: set_eq_iff mem_box)
himmelma@35172
   214
wenzelm@53399
   215
lemma interior_subset_union_intervals:
immler@56188
   216
  assumes "i = cbox a b"
immler@56188
   217
    and "j = cbox c d"
wenzelm@53399
   218
    and "interior j \<noteq> {}"
wenzelm@53399
   219
    and "i \<subseteq> j \<union> s"
wenzelm@53399
   220
    and "interior i \<inter> interior j = {}"
wenzelm@49675
   221
  shows "interior i \<subseteq> interior s"
wenzelm@49675
   222
proof -
immler@56188
   223
  have "box a b \<inter> cbox c d = {}"
immler@56188
   224
     using inter_interval_mixed_eq_empty[of c d a b] and assms(3,5)
immler@56188
   225
     unfolding assms(1,2) interior_cbox by auto
wenzelm@49675
   226
  moreover
immler@56188
   227
  have "box a b \<subseteq> cbox c d \<union> s"
immler@56188
   228
    apply (rule order_trans,rule box_subset_cbox)
wenzelm@49970
   229
    using assms(4) unfolding assms(1,2)
wenzelm@49970
   230
    apply auto
wenzelm@49970
   231
    done
wenzelm@49675
   232
  ultimately
wenzelm@49675
   233
  show ?thesis
lp15@60384
   234
    unfolding assms interior_cbox
lp15@60384
   235
      by auto (metis IntI UnE empty_iff interior_maximal open_box subsetCE subsetI)
wenzelm@49675
   236
qed
wenzelm@49675
   237
wenzelm@49675
   238
lemma inter_interior_unions_intervals:
immler@56188
   239
  fixes f::"('a::euclidean_space) set set"
wenzelm@53399
   240
  assumes "finite f"
wenzelm@53399
   241
    and "open s"
immler@56188
   242
    and "\<forall>t\<in>f. \<exists>a b. t = cbox a b"
wenzelm@53399
   243
    and "\<forall>t\<in>f. s \<inter> (interior t) = {}"
wenzelm@53399
   244
  shows "s \<inter> interior (\<Union>f) = {}"
lp15@60394
   245
proof (clarsimp simp only: all_not_in_conv [symmetric])
lp15@60394
   246
  fix x
lp15@60394
   247
  assume x: "x \<in> s" "x \<in> interior (\<Union>f)"
wenzelm@49970
   248
  have lem1: "\<And>x e s U. ball x e \<subseteq> s \<inter> interior U \<longleftrightarrow> ball x e \<subseteq> s \<inter> U"
wenzelm@49970
   249
    using interior_subset
lp15@60384
   250
    by auto (meson Topology_Euclidean_Space.open_ball contra_subsetD interior_maximal mem_ball)
wenzelm@61165
   251
  have "\<exists>t\<in>f. \<exists>x. \<exists>e>0. ball x e \<subseteq> s \<inter> t"
wenzelm@61165
   252
    if "finite f" and "\<forall>t\<in>f. \<exists>a b. t = cbox a b" and "\<exists>x. x \<in> s \<inter> interior (\<Union>f)" for f
wenzelm@61165
   253
    using that
wenzelm@61165
   254
  proof (induct rule: finite_induct)
wenzelm@61165
   255
    case empty
wenzelm@61165
   256
    obtain x where "x \<in> s \<inter> interior (\<Union>{})"
wenzelm@61165
   257
      using empty(2) ..
wenzelm@61165
   258
    then have False
wenzelm@61165
   259
      unfolding Union_empty interior_empty by auto
wenzelm@61165
   260
    then show ?case by auto
wenzelm@61165
   261
  next
wenzelm@61165
   262
    case (insert i f)
wenzelm@61165
   263
    obtain x where x: "x \<in> s \<inter> interior (\<Union>insert i f)"
wenzelm@61165
   264
      using insert(5) ..
wenzelm@61165
   265
    then obtain e where e: "0 < e \<and> ball x e \<subseteq> s \<inter> interior (\<Union>insert i f)"
wenzelm@61165
   266
      unfolding open_contains_ball_eq[OF open_Int[OF assms(2) open_interior], rule_format] ..
wenzelm@61165
   267
    obtain a where "\<exists>b. i = cbox a b"
wenzelm@61165
   268
      using insert(4)[rule_format,OF insertI1] ..
wenzelm@61165
   269
    then obtain b where ab: "i = cbox a b" ..
wenzelm@61165
   270
    show ?case
wenzelm@61165
   271
    proof (cases "x \<in> i")
wenzelm@61165
   272
      case False
wenzelm@61165
   273
      then have "x \<in> UNIV - cbox a b"
wenzelm@61165
   274
        unfolding ab by auto
wenzelm@61165
   275
      then obtain d where "0 < d \<and> ball x d \<subseteq> UNIV - cbox a b"
wenzelm@61165
   276
        unfolding open_contains_ball_eq[OF open_Diff[OF open_UNIV closed_cbox],rule_format] ..
wenzelm@61165
   277
      then have "0 < d" "ball x (min d e) \<subseteq> UNIV - i"
wenzelm@61165
   278
        unfolding ab ball_min_Int by auto
wenzelm@61165
   279
      then have "ball x (min d e) \<subseteq> s \<inter> interior (\<Union>f)"
wenzelm@61165
   280
        using e unfolding lem1 unfolding  ball_min_Int by auto
wenzelm@61165
   281
      then have "x \<in> s \<inter> interior (\<Union>f)" using \<open>d>0\<close> e by auto
wenzelm@61165
   282
      then have "\<exists>t\<in>f. \<exists>x e. 0 < e \<and> ball x e \<subseteq> s \<inter> t"
wenzelm@61165
   283
        using insert.hyps(3) insert.prems(1) by blast
wenzelm@61165
   284
      then show ?thesis by auto
wenzelm@49970
   285
    next
wenzelm@61165
   286
      case True show ?thesis
wenzelm@61165
   287
      proof (cases "x\<in>box a b")
wenzelm@61165
   288
        case True
wenzelm@61165
   289
        then obtain d where "0 < d \<and> ball x d \<subseteq> box a b"
wenzelm@61165
   290
          unfolding open_contains_ball_eq[OF open_box,rule_format] ..
wenzelm@61165
   291
        then show ?thesis
wenzelm@61165
   292
          apply (rule_tac x=i in bexI, rule_tac x=x in exI, rule_tac x="min d e" in exI)
wenzelm@61165
   293
          unfolding ab
wenzelm@61165
   294
          using box_subset_cbox[of a b] and e
wenzelm@61165
   295
          apply fastforce+
wenzelm@61165
   296
          done
wenzelm@61165
   297
      next
wenzelm@49970
   298
        case False
wenzelm@61165
   299
        then obtain k where "x\<bullet>k \<le> a\<bullet>k \<or> x\<bullet>k \<ge> b\<bullet>k" and k: "k \<in> Basis"
wenzelm@61165
   300
          unfolding mem_box by (auto simp add: not_less)
wenzelm@61165
   301
        then have "x\<bullet>k = a\<bullet>k \<or> x\<bullet>k = b\<bullet>k"
wenzelm@61165
   302
          using True unfolding ab and mem_box
wenzelm@61165
   303
            apply (erule_tac x = k in ballE)
wenzelm@61165
   304
            apply auto
wenzelm@49970
   305
            done
wenzelm@61165
   306
        then have "\<exists>x. ball x (e/2) \<subseteq> s \<inter> (\<Union>f)"
wenzelm@61165
   307
        proof (rule disjE)
wenzelm@61165
   308
          let ?z = "x - (e/2) *\<^sub>R k"
wenzelm@61165
   309
          assume as: "x\<bullet>k = a\<bullet>k"
wenzelm@61165
   310
          have "ball ?z (e / 2) \<inter> i = {}"
wenzelm@61165
   311
          proof (clarsimp simp only: all_not_in_conv [symmetric])
wenzelm@61165
   312
            fix y
wenzelm@61165
   313
            assume "y \<in> ball ?z (e / 2)" and yi: "y \<in> i"
wenzelm@61165
   314
            then have "dist ?z y < e/2" by auto
wenzelm@61165
   315
            then have "\<bar>(?z - y) \<bullet> k\<bar> < e/2"
wenzelm@61165
   316
              using Basis_le_norm[OF k, of "?z - y"] unfolding dist_norm by auto
wenzelm@61165
   317
            then have "y\<bullet>k < a\<bullet>k"
wenzelm@61165
   318
              using e k
wenzelm@61165
   319
              by (auto simp add: field_simps abs_less_iff as inner_simps)
wenzelm@61165
   320
            then have "y \<notin> i"
wenzelm@61165
   321
              unfolding ab mem_box by (auto intro!: bexI[OF _ k])
wenzelm@61165
   322
            then show False using yi by auto
wenzelm@61165
   323
          qed
wenzelm@61165
   324
          moreover
wenzelm@61165
   325
          have "ball ?z (e/2) \<subseteq> s \<inter> (\<Union>insert i f)"
wenzelm@61165
   326
            apply (rule order_trans[OF _ e[THEN conjunct2, unfolded lem1]])
wenzelm@61165
   327
          proof
wenzelm@61165
   328
            fix y
wenzelm@61165
   329
            assume as: "y \<in> ball ?z (e/2)"
wenzelm@61165
   330
            have "norm (x - y) \<le> \<bar>e\<bar> / 2 + norm (x - y - (e / 2) *\<^sub>R k)"
wenzelm@61165
   331
              apply (rule order_trans,rule norm_triangle_sub[of "x - y" "(e/2) *\<^sub>R k"])
wenzelm@61165
   332
              unfolding norm_scaleR norm_Basis[OF k]
wenzelm@49970
   333
              apply auto
wenzelm@49970
   334
              done
wenzelm@61165
   335
            also have "\<dots> < \<bar>e\<bar> / 2 + \<bar>e\<bar> / 2"
wenzelm@61165
   336
              apply (rule add_strict_left_mono)
wenzelm@61165
   337
              using as e
wenzelm@61165
   338
              apply (auto simp add: field_simps dist_norm)
wenzelm@49970
   339
              done
wenzelm@61165
   340
            finally show "y \<in> ball x e"
wenzelm@61165
   341
              unfolding mem_ball dist_norm using e by (auto simp add:field_simps)
wenzelm@61165
   342
          qed
wenzelm@61165
   343
          ultimately show ?thesis
wenzelm@61165
   344
            apply (rule_tac x="?z" in exI)
wenzelm@61165
   345
            unfolding Union_insert
wenzelm@61165
   346
            apply auto
wenzelm@61165
   347
            done
wenzelm@61165
   348
        next
wenzelm@61165
   349
          let ?z = "x + (e/2) *\<^sub>R k"
wenzelm@61165
   350
          assume as: "x\<bullet>k = b\<bullet>k"
wenzelm@61165
   351
          have "ball ?z (e / 2) \<inter> i = {}"
wenzelm@61165
   352
          proof (clarsimp simp only: all_not_in_conv [symmetric])
wenzelm@61165
   353
            fix y
wenzelm@61165
   354
            assume "y \<in> ball ?z (e / 2)" and yi: "y \<in> i"
wenzelm@61165
   355
            then have "dist ?z y < e/2"
wenzelm@61165
   356
              by auto
wenzelm@61165
   357
            then have "\<bar>(?z - y) \<bullet> k\<bar> < e/2"
wenzelm@61165
   358
              using Basis_le_norm[OF k, of "?z - y"]
wenzelm@61165
   359
              unfolding dist_norm by auto
wenzelm@61165
   360
            then have "y\<bullet>k > b\<bullet>k"
wenzelm@61165
   361
              using e k
wenzelm@61165
   362
              by (auto simp add:field_simps inner_simps inner_Basis as)
wenzelm@61165
   363
            then have "y \<notin> i"
wenzelm@61165
   364
              unfolding ab mem_box by (auto intro!: bexI[OF _ k])
wenzelm@61165
   365
            then show False using yi by auto
wenzelm@61165
   366
          qed
wenzelm@61165
   367
          moreover
wenzelm@61165
   368
          have "ball ?z (e/2) \<subseteq> s \<inter> (\<Union>insert i f)"
wenzelm@61165
   369
            apply (rule order_trans[OF _ e[THEN conjunct2, unfolded lem1]])
wenzelm@61165
   370
          proof
wenzelm@61165
   371
            fix y
wenzelm@61165
   372
            assume as: "y\<in> ball ?z (e/2)"
wenzelm@61165
   373
            have "norm (x - y) \<le> \<bar>e\<bar> / 2 + norm (x - y + (e / 2) *\<^sub>R k)"
wenzelm@61165
   374
              apply (rule order_trans,rule norm_triangle_sub[of "x - y" "- (e/2) *\<^sub>R k"])
wenzelm@61165
   375
              unfolding norm_scaleR
wenzelm@61165
   376
              apply (auto simp: k)
wenzelm@49970
   377
              done
wenzelm@61165
   378
            also have "\<dots> < \<bar>e\<bar> / 2 + \<bar>e\<bar> / 2"
wenzelm@61165
   379
              apply (rule add_strict_left_mono)
wenzelm@61165
   380
              using as unfolding mem_ball dist_norm
wenzelm@61165
   381
              using e apply (auto simp add: field_simps)
wenzelm@61165
   382
              done
wenzelm@61165
   383
            finally show "y \<in> ball x e"
wenzelm@61165
   384
              unfolding mem_ball dist_norm using e by (auto simp add:field_simps)
wenzelm@53399
   385
          qed
wenzelm@61165
   386
          ultimately show ?thesis
wenzelm@61165
   387
            apply (rule_tac x="?z" in exI)
wenzelm@61165
   388
            unfolding Union_insert
wenzelm@61165
   389
            apply auto
wenzelm@61165
   390
            done
wenzelm@49970
   391
        qed
wenzelm@61165
   392
        then obtain x where "ball x (e / 2) \<subseteq> s \<inter> \<Union>f" ..
wenzelm@61165
   393
        then have "x \<in> s \<inter> interior (\<Union>f)"
wenzelm@61165
   394
          unfolding lem1[where U="\<Union>f", symmetric]
wenzelm@61165
   395
          using centre_in_ball e by auto
wenzelm@61165
   396
        then show ?thesis
wenzelm@61165
   397
          using insert.hyps(3) insert.prems(1) by blast
wenzelm@49970
   398
      qed
wenzelm@49970
   399
    qed
wenzelm@49970
   400
  qed
lp15@60394
   401
  from this[OF assms(1,3)] x
wenzelm@53408
   402
  obtain t x e where "t \<in> f" "0 < e" "ball x e \<subseteq> s \<inter> t"
wenzelm@53408
   403
    by blast
wenzelm@53408
   404
  then have "x \<in> s" "x \<in> interior t"
wenzelm@53399
   405
    using open_subset_interior[OF open_ball, of x e t]
wenzelm@53408
   406
    by auto
wenzelm@53399
   407
  then show False
wenzelm@60420
   408
    using \<open>t \<in> f\<close> assms(4) by auto
wenzelm@60420
   409
qed
wenzelm@60420
   410
wenzelm@60420
   411
subsection \<open>Bounds on intervals where they exist.\<close>
immler@56188
   412
immler@56188
   413
definition interval_upperbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
immler@56188
   414
  where "interval_upperbound s = (\<Sum>i\<in>Basis. (SUP x:s. x\<bullet>i) *\<^sub>R i)"
immler@56188
   415
immler@56188
   416
definition interval_lowerbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
immler@56188
   417
   where "interval_lowerbound s = (\<Sum>i\<in>Basis. (INF x:s. x\<bullet>i) *\<^sub>R i)"
immler@56188
   418
immler@56188
   419
lemma interval_upperbound[simp]:
immler@56188
   420
  "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
immler@56188
   421
    interval_upperbound (cbox a b) = (b::'a::euclidean_space)"
immler@56188
   422
  unfolding interval_upperbound_def euclidean_representation_setsum cbox_def SUP_def
immler@56188
   423
  by (safe intro!: cSup_eq) auto
immler@56188
   424
immler@56188
   425
lemma interval_lowerbound[simp]:
immler@56188
   426
  "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
immler@56188
   427
    interval_lowerbound (cbox a b) = (a::'a::euclidean_space)"
immler@56188
   428
  unfolding interval_lowerbound_def euclidean_representation_setsum cbox_def INF_def
immler@56188
   429
  by (safe intro!: cInf_eq) auto
immler@56188
   430
immler@56188
   431
lemmas interval_bounds = interval_upperbound interval_lowerbound
immler@56188
   432
immler@56188
   433
lemma
immler@56188
   434
  fixes X::"real set"
immler@56188
   435
  shows interval_upperbound_real[simp]: "interval_upperbound X = Sup X"
immler@56188
   436
    and interval_lowerbound_real[simp]: "interval_lowerbound X = Inf X"
immler@56188
   437
  by (auto simp: interval_upperbound_def interval_lowerbound_def SUP_def INF_def)
immler@56188
   438
immler@56188
   439
lemma interval_bounds'[simp]:
immler@56188
   440
  assumes "cbox a b \<noteq> {}"
immler@56188
   441
  shows "interval_upperbound (cbox a b) = b"
immler@56188
   442
    and "interval_lowerbound (cbox a b) = a"
immler@56188
   443
  using assms unfolding box_ne_empty by auto
wenzelm@53399
   444
hoelzl@59425
   445
lp15@60615
   446
lemma interval_upperbound_Times:
hoelzl@59425
   447
  assumes "A \<noteq> {}" and "B \<noteq> {}"
hoelzl@59425
   448
  shows "interval_upperbound (A \<times> B) = (interval_upperbound A, interval_upperbound B)"
hoelzl@59425
   449
proof-
hoelzl@59425
   450
  from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
hoelzl@59425
   451
  have "(\<Sum>i\<in>Basis. (SUP x:A \<times> B. x \<bullet> (i, 0)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (SUP x:A. x \<bullet> i) *\<^sub>R i)"
hoelzl@59425
   452
      by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
hoelzl@59425
   453
  moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp
hoelzl@59425
   454
  have "(\<Sum>i\<in>Basis. (SUP x:A \<times> B. x \<bullet> (0, i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (SUP x:B. x \<bullet> i) *\<^sub>R i)"
hoelzl@59425
   455
      by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
hoelzl@59425
   456
  ultimately show ?thesis unfolding interval_upperbound_def
hoelzl@59425
   457
      by (subst setsum_Basis_prod_eq) (auto simp add: setsum_prod)
hoelzl@59425
   458
qed
hoelzl@59425
   459
lp15@60615
   460
lemma interval_lowerbound_Times:
hoelzl@59425
   461
  assumes "A \<noteq> {}" and "B \<noteq> {}"
hoelzl@59425
   462
  shows "interval_lowerbound (A \<times> B) = (interval_lowerbound A, interval_lowerbound B)"
hoelzl@59425
   463
proof-
hoelzl@59425
   464
  from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
hoelzl@59425
   465
  have "(\<Sum>i\<in>Basis. (INF x:A \<times> B. x \<bullet> (i, 0)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (INF x:A. x \<bullet> i) *\<^sub>R i)"
hoelzl@59425
   466
      by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
hoelzl@59425
   467
  moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp
hoelzl@59425
   468
  have "(\<Sum>i\<in>Basis. (INF x:A \<times> B. x \<bullet> (0, i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (INF x:B. x \<bullet> i) *\<^sub>R i)"
hoelzl@59425
   469
      by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
hoelzl@59425
   470
  ultimately show ?thesis unfolding interval_lowerbound_def
hoelzl@59425
   471
      by (subst setsum_Basis_prod_eq) (auto simp add: setsum_prod)
hoelzl@59425
   472
qed
hoelzl@59425
   473
wenzelm@60420
   474
subsection \<open>Content (length, area, volume...) of an interval.\<close>
himmelma@35172
   475
immler@56188
   476
definition "content (s::('a::euclidean_space) set) =
immler@56188
   477
  (if s = {} then 0 else (\<Prod>i\<in>Basis. (interval_upperbound s)\<bullet>i - (interval_lowerbound s)\<bullet>i))"
immler@56188
   478
immler@56188
   479
lemma interval_not_empty: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> cbox a b \<noteq> {}"
immler@56188
   480
  unfolding box_eq_empty unfolding not_ex not_less by auto
immler@56188
   481
immler@56188
   482
lemma content_cbox:
immler@56188
   483
  fixes a :: "'a::euclidean_space"
hoelzl@50526
   484
  assumes "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
immler@56188
   485
  shows "content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
wenzelm@49970
   486
  using interval_not_empty[OF assms]
immler@54777
   487
  unfolding content_def
lp15@60384
   488
  by auto
immler@56188
   489
immler@56188
   490
lemma content_cbox':
immler@56188
   491
  fixes a :: "'a::euclidean_space"
immler@56188
   492
  assumes "cbox a b \<noteq> {}"
immler@56188
   493
  shows "content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
lp15@60384
   494
    using assms box_ne_empty(1) content_cbox by blast
wenzelm@49970
   495
wenzelm@53408
   496
lemma content_real: "a \<le> b \<Longrightarrow> content {a..b} = b - a"
immler@56188
   497
  by (auto simp: interval_upperbound_def interval_lowerbound_def SUP_def INF_def content_def)
immler@56188
   498
hoelzl@50104
   499
lemma content_singleton[simp]: "content {a} = 0"
hoelzl@50104
   500
proof -
immler@56188
   501
  have "content (cbox a a) = 0"
immler@56188
   502
    by (subst content_cbox) (auto simp: ex_in_conv)
immler@56188
   503
  then show ?thesis by (simp add: cbox_sing)
immler@56188
   504
qed
immler@56188
   505
lp15@60615
   506
lemma content_unit[iff]: "content(cbox 0 (One::'a::euclidean_space)) = 1"
immler@56188
   507
 proof -
immler@56188
   508
   have *: "\<forall>i\<in>Basis. (0::'a)\<bullet>i \<le> (One::'a)\<bullet>i"
immler@56188
   509
    by auto
immler@56188
   510
  have "0 \<in> cbox 0 (One::'a)"
immler@56188
   511
    unfolding mem_box by auto
immler@56188
   512
  then show ?thesis
haftmann@57418
   513
     unfolding content_def interval_bounds[OF *] using setprod.neutral_const by auto
immler@56188
   514
 qed
wenzelm@49970
   515
wenzelm@49970
   516
lemma content_pos_le[intro]:
immler@56188
   517
  fixes a::"'a::euclidean_space"
immler@56188
   518
  shows "0 \<le> content (cbox a b)"
immler@56188
   519
proof (cases "cbox a b = {}")
immler@56188
   520
  case False
immler@56188
   521
  then have *: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
immler@56188
   522
    unfolding box_ne_empty .
immler@56188
   523
  have "0 \<le> (\<Prod>i\<in>Basis. interval_upperbound (cbox a b) \<bullet> i - interval_lowerbound (cbox a b) \<bullet> i)"
immler@56188
   524
    apply (rule setprod_nonneg)
immler@56188
   525
    unfolding interval_bounds[OF *]
immler@56188
   526
    using *
immler@56188
   527
    apply auto
immler@56188
   528
    done
immler@56188
   529
  also have "\<dots> = content (cbox a b)" using False by (simp add: content_def)
immler@56188
   530
  finally show ?thesis .
immler@56188
   531
qed (simp add: content_def)
wenzelm@49970
   532
lp15@60615
   533
corollary content_nonneg [simp]:
lp15@60615
   534
  fixes a::"'a::euclidean_space"
lp15@60615
   535
  shows "~ content (cbox a b) < 0"
lp15@60615
   536
using not_le by blast
lp15@60615
   537
wenzelm@49970
   538
lemma content_pos_lt:
immler@56188
   539
  fixes a :: "'a::euclidean_space"
hoelzl@50526
   540
  assumes "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
immler@56188
   541
  shows "0 < content (cbox a b)"
immler@54777
   542
  using assms
immler@56188
   543
  by (auto simp: content_def box_eq_empty intro!: setprod_pos)
wenzelm@49970
   544
wenzelm@53408
   545
lemma content_eq_0:
immler@56188
   546
  "content (cbox a b) = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i)"
immler@56188
   547
  by (auto simp: content_def box_eq_empty intro!: setprod_pos bexI)
himmelma@35172
   548
wenzelm@53408
   549
lemma cond_cases: "(P \<Longrightarrow> Q x) \<Longrightarrow> (\<not> P \<Longrightarrow> Q y) \<Longrightarrow> Q (if P then x else y)"
wenzelm@53399
   550
  by auto
himmelma@35172
   551
immler@56188
   552
lemma content_cbox_cases:
immler@56188
   553
  "content (cbox a (b::'a::euclidean_space)) =
hoelzl@50526
   554
    (if \<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i then setprod (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis else 0)"
immler@56188
   555
  by (auto simp: not_le content_eq_0 intro: less_imp_le content_cbox)
immler@56188
   556
immler@56188
   557
lemma content_eq_0_interior: "content (cbox a b) = 0 \<longleftrightarrow> interior(cbox a b) = {}"
immler@56188
   558
  unfolding content_eq_0 interior_cbox box_eq_empty
wenzelm@53408
   559
  by auto
himmelma@35172
   560
wenzelm@53399
   561
lemma content_pos_lt_eq:
immler@56188
   562
  "0 < content (cbox a (b::'a::euclidean_space)) \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
lp15@60394
   563
proof (rule iffI)
immler@56188
   564
  assume "0 < content (cbox a b)"
immler@56188
   565
  then have "content (cbox a b) \<noteq> 0" by auto
wenzelm@53399
   566
  then show "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
wenzelm@49970
   567
    unfolding content_eq_0 not_ex not_le by fastforce
lp15@60394
   568
next
lp15@60394
   569
  assume "\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i"
lp15@60394
   570
  then show "0 < content (cbox a b)"
lp15@60394
   571
    by (metis content_pos_lt)
wenzelm@49970
   572
qed
wenzelm@49970
   573
wenzelm@53399
   574
lemma content_empty [simp]: "content {} = 0"
wenzelm@53399
   575
  unfolding content_def by auto
himmelma@35172
   576
paulson@60762
   577
lemma content_real_if [simp]: "content {a..b} = (if a \<le> b then b - a else 0)"
paulson@60762
   578
  by (simp add: content_real)
paulson@60762
   579
wenzelm@49698
   580
lemma content_subset:
immler@56188
   581
  assumes "cbox a b \<subseteq> cbox c d"
immler@56188
   582
  shows "content (cbox a b) \<le> content (cbox c d)"
immler@56188
   583
proof (cases "cbox a b = {}")
immler@56188
   584
  case True
immler@56188
   585
  then show ?thesis
immler@56188
   586
    using content_pos_le[of c d] by auto
immler@56188
   587
next
immler@56188
   588
  case False
immler@56188
   589
  then have ab_ne: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
immler@56188
   590
    unfolding box_ne_empty by auto
immler@56188
   591
  then have ab_ab: "a\<in>cbox a b" "b\<in>cbox a b"
immler@56188
   592
    unfolding mem_box by auto
immler@56188
   593
  have "cbox c d \<noteq> {}" using assms False by auto
immler@56188
   594
  then have cd_ne: "\<forall>i\<in>Basis. c \<bullet> i \<le> d \<bullet> i"
immler@56188
   595
    using assms unfolding box_ne_empty by auto
lp15@60394
   596
  have "\<And>i. i \<in> Basis \<Longrightarrow> 0 \<le> b \<bullet> i - a \<bullet> i"
lp15@60394
   597
    using ab_ne by (metis diff_le_iff(1))
lp15@60394
   598
  moreover
lp15@60394
   599
  have "\<And>i. i \<in> Basis \<Longrightarrow> b \<bullet> i - a \<bullet> i \<le> d \<bullet> i - c \<bullet> i"
lp15@60394
   600
    using assms[unfolded subset_eq mem_box,rule_format,OF ab_ab(2)]
lp15@60394
   601
          assms[unfolded subset_eq mem_box,rule_format,OF ab_ab(1)]
lp15@60394
   602
      by (metis diff_mono)
lp15@60394
   603
  ultimately show ?thesis
lp15@60394
   604
    unfolding content_def interval_bounds[OF ab_ne] interval_bounds[OF cd_ne]
wenzelm@60420
   605
    by (simp add: setprod_mono if_not_P[OF False] if_not_P[OF \<open>cbox c d \<noteq> {}\<close>])
immler@56188
   606
qed
immler@56188
   607
immler@56188
   608
lemma content_lt_nz: "0 < content (cbox a b) \<longleftrightarrow> content (cbox a b) \<noteq> 0"
nipkow@44890
   609
  unfolding content_pos_lt_eq content_eq_0 unfolding not_ex not_le by fastforce
himmelma@35172
   610
hoelzl@59425
   611
lemma content_times[simp]: "content (A \<times> B) = content A * content B"
hoelzl@59425
   612
proof (cases "A \<times> B = {}")
hoelzl@59425
   613
  let ?ub1 = "interval_upperbound" and ?lb1 = "interval_lowerbound"
hoelzl@59425
   614
  let ?ub2 = "interval_upperbound" and ?lb2 = "interval_lowerbound"
hoelzl@59425
   615
  assume nonempty: "A \<times> B \<noteq> {}"
lp15@60615
   616
  hence "content (A \<times> B) = (\<Prod>i\<in>Basis. (?ub1 A, ?ub2 B) \<bullet> i - (?lb1 A, ?lb2 B) \<bullet> i)"
hoelzl@59425
   617
      unfolding content_def by (simp add: interval_upperbound_Times interval_lowerbound_Times)
hoelzl@59425
   618
  also have "... = content A * content B" unfolding content_def using nonempty
hoelzl@59425
   619
    apply (subst Basis_prod_def, subst setprod.union_disjoint, force, force, force, simp)
hoelzl@59425
   620
    apply (subst (1 2) setprod.reindex, auto intro: inj_onI)
hoelzl@59425
   621
    done
hoelzl@59425
   622
  finally show ?thesis .
hoelzl@59425
   623
qed (auto simp: content_def)
hoelzl@59425
   624
lp15@60615
   625
lemma content_Pair: "content (cbox (a,c) (b,d)) = content (cbox a b) * content (cbox c d)"
lp15@60615
   626
  by (simp add: cbox_Pair_eq)
lp15@60615
   627
lp15@60615
   628
lemma content_cbox_pair_eq0_D:
lp15@60615
   629
   "content (cbox (a,c) (b,d)) = 0 \<Longrightarrow> content (cbox a b) = 0 \<or> content (cbox c d) = 0"
lp15@60615
   630
  by (simp add: content_Pair)
lp15@60615
   631
lp15@60615
   632
lemma content_eq_0_gen:
lp15@60615
   633
  fixes s :: "'a::euclidean_space set"
lp15@60615
   634
  assumes "bounded s"
lp15@60615
   635
  shows "content s = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. \<exists>v. \<forall>x \<in> s. x \<bullet> i = v)"  (is "_ = ?rhs")
lp15@60615
   636
proof safe
lp15@60615
   637
  assume "content s = 0" then show ?rhs
lp15@60615
   638
    apply (clarsimp simp: ex_in_conv content_def split: split_if_asm)
lp15@60615
   639
    apply (rule_tac x=a in bexI)
lp15@60615
   640
    apply (rule_tac x="interval_lowerbound s \<bullet> a" in exI)
lp15@60615
   641
    apply (clarsimp simp: interval_upperbound_def interval_lowerbound_def)
lp15@60615
   642
    apply (drule cSUP_eq_cINF_D)
lp15@60615
   643
    apply (auto simp: bounded_inner_imp_bdd_above [OF assms]  bounded_inner_imp_bdd_below [OF assms])
lp15@60615
   644
    done
lp15@60615
   645
next
lp15@60615
   646
  fix i a
lp15@60615
   647
  assume "i \<in> Basis" "\<forall>x\<in>s. x \<bullet> i = a"
lp15@60615
   648
  then show "content s = 0"
lp15@60615
   649
    apply (clarsimp simp: content_def)
lp15@60615
   650
    apply (rule_tac x=i in bexI)
lp15@60615
   651
    apply (auto simp: interval_upperbound_def interval_lowerbound_def)
lp15@60615
   652
    done
lp15@60615
   653
qed
lp15@60615
   654
lp15@60615
   655
lemma content_0_subset_gen:
lp15@60615
   656
  fixes a :: "'a::euclidean_space"
lp15@60615
   657
  assumes "content t = 0" "s \<subseteq> t" "bounded t" shows "content s = 0"
lp15@60615
   658
proof -
lp15@60615
   659
  have "bounded s"
lp15@60615
   660
    using assms by (metis bounded_subset)
lp15@60615
   661
  then show ?thesis
lp15@60615
   662
    using assms
lp15@60615
   663
    by (auto simp: content_eq_0_gen)
lp15@60615
   664
qed
lp15@60615
   665
lp15@60615
   666
lemma content_0_subset: "\<lbrakk>content(cbox a b) = 0; s \<subseteq> cbox a b\<rbrakk> \<Longrightarrow> content s = 0"
lp15@60615
   667
  by (simp add: content_0_subset_gen bounded_cbox)
lp15@60615
   668
wenzelm@49698
   669
wenzelm@60420
   670
subsection \<open>The notion of a gauge --- simply an open set containing the point.\<close>
himmelma@35172
   671
wenzelm@53408
   672
definition "gauge d \<longleftrightarrow> (\<forall>x. x \<in> d x \<and> open (d x))"
wenzelm@53399
   673
wenzelm@53399
   674
lemma gaugeI:
wenzelm@53399
   675
  assumes "\<And>x. x \<in> g x"
wenzelm@53399
   676
    and "\<And>x. open (g x)"
wenzelm@53399
   677
  shows "gauge g"
himmelma@35172
   678
  using assms unfolding gauge_def by auto
himmelma@35172
   679
wenzelm@53399
   680
lemma gaugeD[dest]:
wenzelm@53399
   681
  assumes "gauge d"
wenzelm@53399
   682
  shows "x \<in> d x"
wenzelm@53399
   683
    and "open (d x)"
wenzelm@49698
   684
  using assms unfolding gauge_def by auto
himmelma@35172
   685
himmelma@35172
   686
lemma gauge_ball_dependent: "\<forall>x. 0 < e x \<Longrightarrow> gauge (\<lambda>x. ball x (e x))"
wenzelm@53399
   687
  unfolding gauge_def by auto
wenzelm@53399
   688
wenzelm@53399
   689
lemma gauge_ball[intro]: "0 < e \<Longrightarrow> gauge (\<lambda>x. ball x e)"
wenzelm@53399
   690
  unfolding gauge_def by auto
himmelma@35172
   691
lp15@60466
   692
lemma gauge_trivial[intro!]: "gauge (\<lambda>x. ball x 1)"
wenzelm@49698
   693
  by (rule gauge_ball) auto
himmelma@35172
   694
wenzelm@53408
   695
lemma gauge_inter[intro]: "gauge d1 \<Longrightarrow> gauge d2 \<Longrightarrow> gauge (\<lambda>x. d1 x \<inter> d2 x)"
wenzelm@53399
   696
  unfolding gauge_def by auto
himmelma@35172
   697
wenzelm@49698
   698
lemma gauge_inters:
wenzelm@53399
   699
  assumes "finite s"
wenzelm@53399
   700
    and "\<forall>d\<in>s. gauge (f d)"
wenzelm@60585
   701
  shows "gauge (\<lambda>x. \<Inter>{f d x | d. d \<in> s})"
wenzelm@49698
   702
proof -
wenzelm@53399
   703
  have *: "\<And>x. {f d x |d. d \<in> s} = (\<lambda>d. f d x) ` s"
wenzelm@53399
   704
    by auto
wenzelm@49698
   705
  show ?thesis
wenzelm@53399
   706
    unfolding gauge_def unfolding *
wenzelm@49698
   707
    using assms unfolding Ball_def Inter_iff mem_Collect_eq gauge_def by auto
wenzelm@49698
   708
qed
wenzelm@49698
   709
wenzelm@53399
   710
lemma gauge_existence_lemma:
wenzelm@53408
   711
  "(\<forall>x. \<exists>d :: real. p x \<longrightarrow> 0 < d \<and> q d x) \<longleftrightarrow> (\<forall>x. \<exists>d>0. p x \<longrightarrow> q d x)"
wenzelm@53399
   712
  by (metis zero_less_one)
wenzelm@49698
   713
himmelma@35172
   714
wenzelm@60420
   715
subsection \<open>Divisions.\<close>
himmelma@35172
   716
wenzelm@53408
   717
definition division_of (infixl "division'_of" 40)
wenzelm@53408
   718
where
wenzelm@53399
   719
  "s division_of i \<longleftrightarrow>
wenzelm@53399
   720
    finite s \<and>
immler@56188
   721
    (\<forall>k\<in>s. k \<subseteq> i \<and> k \<noteq> {} \<and> (\<exists>a b. k = cbox a b)) \<and>
wenzelm@53399
   722
    (\<forall>k1\<in>s. \<forall>k2\<in>s. k1 \<noteq> k2 \<longrightarrow> interior(k1) \<inter> interior(k2) = {}) \<and>
wenzelm@53399
   723
    (\<Union>s = i)"
himmelma@35172
   724
wenzelm@49698
   725
lemma division_ofD[dest]:
wenzelm@49698
   726
  assumes "s division_of i"
wenzelm@53408
   727
  shows "finite s"
wenzelm@53408
   728
    and "\<And>k. k \<in> s \<Longrightarrow> k \<subseteq> i"
wenzelm@53408
   729
    and "\<And>k. k \<in> s \<Longrightarrow> k \<noteq> {}"
immler@56188
   730
    and "\<And>k. k \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b"
wenzelm@53408
   731
    and "\<And>k1 k2. k1 \<in> s \<Longrightarrow> k2 \<in> s \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior(k1) \<inter> interior(k2) = {}"
wenzelm@53408
   732
    and "\<Union>s = i"
wenzelm@49698
   733
  using assms unfolding division_of_def by auto
himmelma@35172
   734
himmelma@35172
   735
lemma division_ofI:
wenzelm@53408
   736
  assumes "finite s"
wenzelm@53408
   737
    and "\<And>k. k \<in> s \<Longrightarrow> k \<subseteq> i"
wenzelm@53408
   738
    and "\<And>k. k \<in> s \<Longrightarrow> k \<noteq> {}"
immler@56188
   739
    and "\<And>k. k \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b"
wenzelm@53408
   740
    and "\<And>k1 k2. k1 \<in> s \<Longrightarrow> k2 \<in> s \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior k1 \<inter> interior k2 = {}"
wenzelm@53399
   741
    and "\<Union>s = i"
wenzelm@53399
   742
  shows "s division_of i"
wenzelm@53399
   743
  using assms unfolding division_of_def by auto
himmelma@35172
   744
himmelma@35172
   745
lemma division_of_finite: "s division_of i \<Longrightarrow> finite s"
himmelma@35172
   746
  unfolding division_of_def by auto
himmelma@35172
   747
immler@56188
   748
lemma division_of_self[intro]: "cbox a b \<noteq> {} \<Longrightarrow> {cbox a b} division_of (cbox a b)"
himmelma@35172
   749
  unfolding division_of_def by auto
himmelma@35172
   750
wenzelm@53399
   751
lemma division_of_trivial[simp]: "s division_of {} \<longleftrightarrow> s = {}"
wenzelm@53399
   752
  unfolding division_of_def by auto
himmelma@35172
   753
wenzelm@49698
   754
lemma division_of_sing[simp]:
immler@56188
   755
  "s division_of cbox a (a::'a::euclidean_space) \<longleftrightarrow> s = {cbox a a}"
wenzelm@53399
   756
  (is "?l = ?r")
wenzelm@49698
   757
proof
wenzelm@49698
   758
  assume ?r
wenzelm@53399
   759
  moreover
lp15@60384
   760
  { fix k
lp15@60384
   761
    assume "s = {{a}}" "k\<in>s"
lp15@60384
   762
    then have "\<exists>x y. k = cbox x y"
wenzelm@50945
   763
      apply (rule_tac x=a in exI)+
lp15@60384
   764
      apply (force simp: cbox_sing)
wenzelm@50945
   765
      done
wenzelm@49698
   766
  }
wenzelm@53399
   767
  ultimately show ?l
immler@56188
   768
    unfolding division_of_def cbox_sing by auto
wenzelm@49698
   769
next
wenzelm@49698
   770
  assume ?l
immler@56188
   771
  note * = conjunctD4[OF this[unfolded division_of_def cbox_sing]]
wenzelm@53399
   772
  {
wenzelm@53399
   773
    fix x
wenzelm@53399
   774
    assume x: "x \<in> s" have "x = {a}"
wenzelm@53408
   775
      using *(2)[rule_format,OF x] by auto
wenzelm@53399
   776
  }
wenzelm@53408
   777
  moreover have "s \<noteq> {}"
wenzelm@53408
   778
    using *(4) by auto
wenzelm@53408
   779
  ultimately show ?r
immler@56188
   780
    unfolding cbox_sing by auto
wenzelm@49698
   781
qed
himmelma@35172
   782
himmelma@35172
   783
lemma elementary_empty: obtains p where "p division_of {}"
himmelma@35172
   784
  unfolding division_of_trivial by auto
himmelma@35172
   785
immler@56188
   786
lemma elementary_interval: obtains p where "p division_of (cbox a b)"
wenzelm@49698
   787
  by (metis division_of_trivial division_of_self)
himmelma@35172
   788
himmelma@35172
   789
lemma division_contains: "s division_of i \<Longrightarrow> \<forall>x\<in>i. \<exists>k\<in>s. x \<in> k"
himmelma@35172
   790
  unfolding division_of_def by auto
himmelma@35172
   791
himmelma@35172
   792
lemma forall_in_division:
immler@56188
   793
  "d division_of i \<Longrightarrow> (\<forall>x\<in>d. P x) \<longleftrightarrow> (\<forall>a b. cbox a b \<in> d \<longrightarrow> P (cbox a b))"
nipkow@44890
   794
  unfolding division_of_def by fastforce
himmelma@35172
   795
wenzelm@53399
   796
lemma division_of_subset:
wenzelm@53399
   797
  assumes "p division_of (\<Union>p)"
wenzelm@53399
   798
    and "q \<subseteq> p"
wenzelm@53399
   799
  shows "q division_of (\<Union>q)"
wenzelm@53408
   800
proof (rule division_ofI)
wenzelm@53408
   801
  note * = division_ofD[OF assms(1)]
wenzelm@49698
   802
  show "finite q"
lp15@60384
   803
    using "*"(1) assms(2) infinite_super by auto
wenzelm@53399
   804
  {
wenzelm@53399
   805
    fix k
wenzelm@49698
   806
    assume "k \<in> q"
wenzelm@53408
   807
    then have kp: "k \<in> p"
wenzelm@53408
   808
      using assms(2) by auto
wenzelm@53408
   809
    show "k \<subseteq> \<Union>q"
wenzelm@60420
   810
      using \<open>k \<in> q\<close> by auto
immler@56188
   811
    show "\<exists>a b. k = cbox a b"
wenzelm@53408
   812
      using *(4)[OF kp] by auto
wenzelm@53408
   813
    show "k \<noteq> {}"
wenzelm@53408
   814
      using *(3)[OF kp] by auto
wenzelm@53399
   815
  }
wenzelm@49698
   816
  fix k1 k2
wenzelm@49698
   817
  assume "k1 \<in> q" "k2 \<in> q" "k1 \<noteq> k2"
wenzelm@53408
   818
  then have **: "k1 \<in> p" "k2 \<in> p" "k1 \<noteq> k2"
wenzelm@53399
   819
    using assms(2) by auto
wenzelm@53399
   820
  show "interior k1 \<inter> interior k2 = {}"
wenzelm@53408
   821
    using *(5)[OF **] by auto
wenzelm@49698
   822
qed auto
wenzelm@49698
   823
wenzelm@49698
   824
lemma division_of_union_self[intro]: "p division_of s \<Longrightarrow> p division_of (\<Union>p)"
wenzelm@49698
   825
  unfolding division_of_def by auto
himmelma@35172
   826
wenzelm@49970
   827
lemma division_of_content_0:
immler@56188
   828
  assumes "content (cbox a b) = 0" "d division_of (cbox a b)"
wenzelm@49970
   829
  shows "\<forall>k\<in>d. content k = 0"
wenzelm@49970
   830
  unfolding forall_in_division[OF assms(2)]
lp15@60384
   831
  by (metis antisym_conv assms content_pos_le content_subset division_ofD(2))
wenzelm@49970
   832
wenzelm@49970
   833
lemma division_inter:
immler@56188
   834
  fixes s1 s2 :: "'a::euclidean_space set"
wenzelm@53408
   835
  assumes "p1 division_of s1"
wenzelm@53408
   836
    and "p2 division_of s2"
wenzelm@49970
   837
  shows "{k1 \<inter> k2 | k1 k2 .k1 \<in> p1 \<and> k2 \<in> p2 \<and> k1 \<inter> k2 \<noteq> {}} division_of (s1 \<inter> s2)"
wenzelm@49970
   838
  (is "?A' division_of _")
wenzelm@49970
   839
proof -
wenzelm@49970
   840
  let ?A = "{s. s \<in>  (\<lambda>(k1,k2). k1 \<inter> k2) ` (p1 \<times> p2) \<and> s \<noteq> {}}"
wenzelm@53408
   841
  have *: "?A' = ?A" by auto
wenzelm@53399
   842
  show ?thesis
wenzelm@53399
   843
    unfolding *
wenzelm@49970
   844
  proof (rule division_ofI)
wenzelm@53399
   845
    have "?A \<subseteq> (\<lambda>(x, y). x \<inter> y) ` (p1 \<times> p2)"
wenzelm@53399
   846
      by auto
wenzelm@53399
   847
    moreover have "finite (p1 \<times> p2)"
wenzelm@53399
   848
      using assms unfolding division_of_def by auto
wenzelm@49970
   849
    ultimately show "finite ?A" by auto
wenzelm@53399
   850
    have *: "\<And>s. \<Union>{x\<in>s. x \<noteq> {}} = \<Union>s"
wenzelm@53399
   851
      by auto
wenzelm@49970
   852
    show "\<Union>?A = s1 \<inter> s2"
wenzelm@49970
   853
      apply (rule set_eqI)
wenzelm@49970
   854
      unfolding * and Union_image_eq UN_iff
wenzelm@49970
   855
      using division_ofD(6)[OF assms(1)] and division_ofD(6)[OF assms(2)]
wenzelm@49970
   856
      apply auto
wenzelm@49970
   857
      done
wenzelm@53399
   858
    {
wenzelm@53399
   859
      fix k
wenzelm@53399
   860
      assume "k \<in> ?A"
wenzelm@53408
   861
      then obtain k1 k2 where k: "k = k1 \<inter> k2" "k1 \<in> p1" "k2 \<in> p2" "k \<noteq> {}"
wenzelm@53399
   862
        by auto
wenzelm@53408
   863
      then show "k \<noteq> {}"
wenzelm@53408
   864
        by auto
wenzelm@49970
   865
      show "k \<subseteq> s1 \<inter> s2"
wenzelm@49970
   866
        using division_ofD(2)[OF assms(1) k(2)] and division_ofD(2)[OF assms(2) k(3)]
wenzelm@49970
   867
        unfolding k by auto
immler@56188
   868
      obtain a1 b1 where k1: "k1 = cbox a1 b1"
wenzelm@53408
   869
        using division_ofD(4)[OF assms(1) k(2)] by blast
immler@56188
   870
      obtain a2 b2 where k2: "k2 = cbox a2 b2"
wenzelm@53408
   871
        using division_ofD(4)[OF assms(2) k(3)] by blast
immler@56188
   872
      show "\<exists>a b. k = cbox a b"
wenzelm@53408
   873
        unfolding k k1 k2 unfolding inter_interval by auto
wenzelm@53408
   874
    }
wenzelm@49970
   875
    fix k1 k2
wenzelm@53408
   876
    assume "k1 \<in> ?A"
wenzelm@53408
   877
    then obtain x1 y1 where k1: "k1 = x1 \<inter> y1" "x1 \<in> p1" "y1 \<in> p2" "k1 \<noteq> {}"
wenzelm@53408
   878
      by auto
wenzelm@53408
   879
    assume "k2 \<in> ?A"
wenzelm@53408
   880
    then obtain x2 y2 where k2: "k2 = x2 \<inter> y2" "x2 \<in> p1" "y2 \<in> p2" "k2 \<noteq> {}"
wenzelm@53408
   881
      by auto
wenzelm@49970
   882
    assume "k1 \<noteq> k2"
wenzelm@53399
   883
    then have th: "x1 \<noteq> x2 \<or> y1 \<noteq> y2"
wenzelm@53399
   884
      unfolding k1 k2 by auto
wenzelm@53408
   885
    have *: "interior x1 \<inter> interior x2 = {} \<or> interior y1 \<inter> interior y2 = {} \<Longrightarrow>
wenzelm@53408
   886
      interior (x1 \<inter> y1) \<subseteq> interior x1 \<Longrightarrow> interior (x1 \<inter> y1) \<subseteq> interior y1 \<Longrightarrow>
wenzelm@53408
   887
      interior (x2 \<inter> y2) \<subseteq> interior x2 \<Longrightarrow> interior (x2 \<inter> y2) \<subseteq> interior y2 \<Longrightarrow>
wenzelm@53408
   888
      interior (x1 \<inter> y1) \<inter> interior (x2 \<inter> y2) = {}" by auto
wenzelm@49970
   889
    show "interior k1 \<inter> interior k2 = {}"
wenzelm@49970
   890
      unfolding k1 k2
wenzelm@49970
   891
      apply (rule *)
lp15@60384
   892
      using assms division_ofD(5) k1 k2(2) k2(3) th apply auto
wenzelm@53399
   893
      done
wenzelm@49970
   894
  qed
wenzelm@49970
   895
qed
wenzelm@49970
   896
wenzelm@49970
   897
lemma division_inter_1:
wenzelm@53408
   898
  assumes "d division_of i"
immler@56188
   899
    and "cbox a (b::'a::euclidean_space) \<subseteq> i"
immler@56188
   900
  shows "{cbox a b \<inter> k | k. k \<in> d \<and> cbox a b \<inter> k \<noteq> {}} division_of (cbox a b)"
immler@56188
   901
proof (cases "cbox a b = {}")
wenzelm@49970
   902
  case True
wenzelm@53399
   903
  show ?thesis
wenzelm@53399
   904
    unfolding True and division_of_trivial by auto
wenzelm@49970
   905
next
wenzelm@49970
   906
  case False
immler@56188
   907
  have *: "cbox a b \<inter> i = cbox a b" using assms(2) by auto
wenzelm@53399
   908
  show ?thesis
wenzelm@53399
   909
    using division_inter[OF division_of_self[OF False] assms(1)]
wenzelm@53399
   910
    unfolding * by auto
wenzelm@49970
   911
qed
wenzelm@49970
   912
wenzelm@49970
   913
lemma elementary_inter:
immler@56188
   914
  fixes s t :: "'a::euclidean_space set"
wenzelm@53408
   915
  assumes "p1 division_of s"
wenzelm@53408
   916
    and "p2 division_of t"
himmelma@35172
   917
  shows "\<exists>p. p division_of (s \<inter> t)"
lp15@60384
   918
using assms division_inter by blast
wenzelm@49970
   919
wenzelm@49970
   920
lemma elementary_inters:
wenzelm@53408
   921
  assumes "finite f"
wenzelm@53408
   922
    and "f \<noteq> {}"
immler@56188
   923
    and "\<forall>s\<in>f. \<exists>p. p division_of (s::('a::euclidean_space) set)"
wenzelm@60585
   924
  shows "\<exists>p. p division_of (\<Inter>f)"
wenzelm@49970
   925
  using assms
wenzelm@49970
   926
proof (induct f rule: finite_induct)
wenzelm@49970
   927
  case (insert x f)
wenzelm@49970
   928
  show ?case
wenzelm@49970
   929
  proof (cases "f = {}")
wenzelm@49970
   930
    case True
wenzelm@53399
   931
    then show ?thesis
wenzelm@53399
   932
      unfolding True using insert by auto
wenzelm@49970
   933
  next
wenzelm@49970
   934
    case False
wenzelm@53408
   935
    obtain p where "p division_of \<Inter>f"
wenzelm@53408
   936
      using insert(3)[OF False insert(5)[unfolded ball_simps,THEN conjunct2]] ..
wenzelm@53408
   937
    moreover obtain px where "px division_of x"
wenzelm@53408
   938
      using insert(5)[rule_format,OF insertI1] ..
wenzelm@49970
   939
    ultimately show ?thesis
lp15@60384
   940
      by (simp add: elementary_inter Inter_insert)
wenzelm@49970
   941
  qed
wenzelm@49970
   942
qed auto
himmelma@35172
   943
himmelma@35172
   944
lemma division_disjoint_union:
wenzelm@53408
   945
  assumes "p1 division_of s1"
wenzelm@53408
   946
    and "p2 division_of s2"
wenzelm@53408
   947
    and "interior s1 \<inter> interior s2 = {}"
wenzelm@50945
   948
  shows "(p1 \<union> p2) division_of (s1 \<union> s2)"
wenzelm@50945
   949
proof (rule division_ofI)
wenzelm@53408
   950
  note d1 = division_ofD[OF assms(1)]
wenzelm@53408
   951
  note d2 = division_ofD[OF assms(2)]
wenzelm@53408
   952
  show "finite (p1 \<union> p2)"
wenzelm@53408
   953
    using d1(1) d2(1) by auto
wenzelm@53408
   954
  show "\<Union>(p1 \<union> p2) = s1 \<union> s2"
wenzelm@53408
   955
    using d1(6) d2(6) by auto
wenzelm@50945
   956
  {
wenzelm@50945
   957
    fix k1 k2
wenzelm@50945
   958
    assume as: "k1 \<in> p1 \<union> p2" "k2 \<in> p1 \<union> p2" "k1 \<noteq> k2"
wenzelm@50945
   959
    moreover
wenzelm@50945
   960
    let ?g="interior k1 \<inter> interior k2 = {}"
wenzelm@50945
   961
    {
wenzelm@50945
   962
      assume as: "k1\<in>p1" "k2\<in>p2"
wenzelm@50945
   963
      have ?g
wenzelm@50945
   964
        using interior_mono[OF d1(2)[OF as(1)]] interior_mono[OF d2(2)[OF as(2)]]
wenzelm@50945
   965
        using assms(3) by blast
wenzelm@50945
   966
    }
wenzelm@50945
   967
    moreover
wenzelm@50945
   968
    {
wenzelm@50945
   969
      assume as: "k1\<in>p2" "k2\<in>p1"
wenzelm@50945
   970
      have ?g
wenzelm@50945
   971
        using interior_mono[OF d1(2)[OF as(2)]] interior_mono[OF d2(2)[OF as(1)]]
wenzelm@50945
   972
        using assms(3) by blast
wenzelm@50945
   973
    }
wenzelm@53399
   974
    ultimately show ?g
wenzelm@53399
   975
      using d1(5)[OF _ _ as(3)] and d2(5)[OF _ _ as(3)] by auto
wenzelm@50945
   976
  }
wenzelm@50945
   977
  fix k
wenzelm@50945
   978
  assume k: "k \<in> p1 \<union> p2"
wenzelm@53408
   979
  show "k \<subseteq> s1 \<union> s2"
wenzelm@53408
   980
    using k d1(2) d2(2) by auto
wenzelm@53408
   981
  show "k \<noteq> {}"
wenzelm@53408
   982
    using k d1(3) d2(3) by auto
immler@56188
   983
  show "\<exists>a b. k = cbox a b"
wenzelm@53408
   984
    using k d1(4) d2(4) by auto
wenzelm@50945
   985
qed
himmelma@35172
   986
himmelma@35172
   987
lemma partial_division_extend_1:
immler@56188
   988
  fixes a b c d :: "'a::euclidean_space"
immler@56188
   989
  assumes incl: "cbox c d \<subseteq> cbox a b"
immler@56188
   990
    and nonempty: "cbox c d \<noteq> {}"
immler@56188
   991
  obtains p where "p division_of (cbox a b)" "cbox c d \<in> p"
hoelzl@50526
   992
proof
wenzelm@53408
   993
  let ?B = "\<lambda>f::'a\<Rightarrow>'a \<times> 'a.
immler@56188
   994
    cbox (\<Sum>i\<in>Basis. (fst (f i) \<bullet> i) *\<^sub>R i) (\<Sum>i\<in>Basis. (snd (f i) \<bullet> i) *\<^sub>R i)"
wenzelm@53015
   995
  def p \<equiv> "?B ` (Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)})"
hoelzl@50526
   996
immler@56188
   997
  show "cbox c d \<in> p"
hoelzl@50526
   998
    unfolding p_def
immler@56188
   999
    by (auto simp add: box_eq_empty cbox_def intro!: image_eqI[where x="\<lambda>(i::'a)\<in>Basis. (c, d)"])
wenzelm@50945
  1000
  {
wenzelm@50945
  1001
    fix i :: 'a
wenzelm@50945
  1002
    assume "i \<in> Basis"
hoelzl@50526
  1003
    with incl nonempty have "a \<bullet> i \<le> c \<bullet> i" "c \<bullet> i \<le> d \<bullet> i" "d \<bullet> i \<le> b \<bullet> i"
immler@56188
  1004
      unfolding box_eq_empty subset_box by (auto simp: not_le)
wenzelm@50945
  1005
  }
hoelzl@50526
  1006
  note ord = this
hoelzl@50526
  1007
immler@56188
  1008
  show "p division_of (cbox a b)"
hoelzl@50526
  1009
  proof (rule division_ofI)
wenzelm@53399
  1010
    show "finite p"
wenzelm@53399
  1011
      unfolding p_def by (auto intro!: finite_PiE)
wenzelm@50945
  1012
    {
wenzelm@50945
  1013
      fix k
wenzelm@50945
  1014
      assume "k \<in> p"
wenzelm@53015
  1015
      then obtain f where f: "f \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}" and k: "k = ?B f"
hoelzl@50526
  1016
        by (auto simp: p_def)
immler@56188
  1017
      then show "\<exists>a b. k = cbox a b"
wenzelm@53408
  1018
        by auto
immler@56188
  1019
      have "k \<subseteq> cbox a b \<and> k \<noteq> {}"
immler@56188
  1020
      proof (simp add: k box_eq_empty subset_box not_less, safe)
wenzelm@53374
  1021
        fix i :: 'a
wenzelm@53374
  1022
        assume i: "i \<in> Basis"
wenzelm@50945
  1023
        with f have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
hoelzl@50526
  1024
          by (auto simp: PiE_iff)
wenzelm@53374
  1025
        with i ord[of i]
wenzelm@50945
  1026
        show "a \<bullet> i \<le> fst (f i) \<bullet> i" "snd (f i) \<bullet> i \<le> b \<bullet> i" "fst (f i) \<bullet> i \<le> snd (f i) \<bullet> i"
immler@54776
  1027
          by auto
hoelzl@50526
  1028
      qed
immler@56188
  1029
      then show "k \<noteq> {}" "k \<subseteq> cbox a b"
wenzelm@53408
  1030
        by auto
wenzelm@50945
  1031
      {
wenzelm@53408
  1032
        fix l
wenzelm@53408
  1033
        assume "l \<in> p"
wenzelm@53015
  1034
        then obtain g where g: "g \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}" and l: "l = ?B g"
wenzelm@50945
  1035
          by (auto simp: p_def)
wenzelm@50945
  1036
        assume "l \<noteq> k"
wenzelm@50945
  1037
        have "\<exists>i\<in>Basis. f i \<noteq> g i"
wenzelm@50945
  1038
        proof (rule ccontr)
wenzelm@53408
  1039
          assume "\<not> ?thesis"
wenzelm@50945
  1040
          with f g have "f = g"
wenzelm@50945
  1041
            by (auto simp: PiE_iff extensional_def intro!: ext)
wenzelm@60420
  1042
          with \<open>l \<noteq> k\<close> show False
wenzelm@50945
  1043
            by (simp add: l k)
wenzelm@50945
  1044
        qed
wenzelm@53408
  1045
        then obtain i where *: "i \<in> Basis" "f i \<noteq> g i" ..
wenzelm@53408
  1046
        then have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
lp15@60384
  1047
                  "g i = (a, c) \<or> g i = (c, d) \<or> g i = (d, b)"
wenzelm@50945
  1048
          using f g by (auto simp: PiE_iff)
wenzelm@53408
  1049
        with * ord[of i] show "interior l \<inter> interior k = {}"
immler@56188
  1050
          by (auto simp add: l k interior_cbox disjoint_interval intro!: bexI[of _ i])
wenzelm@50945
  1051
      }
wenzelm@60420
  1052
      note \<open>k \<subseteq> cbox a b\<close>
wenzelm@50945
  1053
    }
hoelzl@50526
  1054
    moreover
wenzelm@50945
  1055
    {
immler@56188
  1056
      fix x assume x: "x \<in> cbox a b"
hoelzl@50526
  1057
      have "\<forall>i\<in>Basis. \<exists>l. x \<bullet> i \<in> {fst l \<bullet> i .. snd l \<bullet> i} \<and> l \<in> {(a, c), (c, d), (d, b)}"
hoelzl@50526
  1058
      proof
wenzelm@53408
  1059
        fix i :: 'a
wenzelm@53408
  1060
        assume "i \<in> Basis"
wenzelm@53399
  1061
        with x ord[of i]
hoelzl@50526
  1062
        have "(a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> c \<bullet> i) \<or> (c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i) \<or>
hoelzl@50526
  1063
            (d \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i)"
immler@56188
  1064
          by (auto simp: cbox_def)
hoelzl@50526
  1065
        then show "\<exists>l. x \<bullet> i \<in> {fst l \<bullet> i .. snd l \<bullet> i} \<and> l \<in> {(a, c), (c, d), (d, b)}"
hoelzl@50526
  1066
          by auto
hoelzl@50526
  1067
      qed
wenzelm@53408
  1068
      then obtain f where
wenzelm@53408
  1069
        f: "\<forall>i\<in>Basis. x \<bullet> i \<in> {fst (f i) \<bullet> i..snd (f i) \<bullet> i} \<and> f i \<in> {(a, c), (c, d), (d, b)}"
wenzelm@53408
  1070
        unfolding bchoice_iff ..
wenzelm@53374
  1071
      moreover from f have "restrict f Basis \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}"
hoelzl@50526
  1072
        by auto
hoelzl@50526
  1073
      moreover from f have "x \<in> ?B (restrict f Basis)"
immler@56188
  1074
        by (auto simp: mem_box)
hoelzl@50526
  1075
      ultimately have "\<exists>k\<in>p. x \<in> k"
wenzelm@53408
  1076
        unfolding p_def by blast
wenzelm@53408
  1077
    }
immler@56188
  1078
    ultimately show "\<Union>p = cbox a b"
hoelzl@50526
  1079
      by auto
hoelzl@50526
  1080
  qed
hoelzl@50526
  1081
qed
himmelma@35172
  1082
wenzelm@50945
  1083
lemma partial_division_extend_interval:
immler@56188
  1084
  assumes "p division_of (\<Union>p)" "(\<Union>p) \<subseteq> cbox a b"
immler@56188
  1085
  obtains q where "p \<subseteq> q" "q division_of cbox a (b::'a::euclidean_space)"
wenzelm@50945
  1086
proof (cases "p = {}")
wenzelm@50945
  1087
  case True
immler@56188
  1088
  obtain q where "q division_of (cbox a b)"
wenzelm@53408
  1089
    by (rule elementary_interval)
wenzelm@53399
  1090
  then show ?thesis
lp15@60384
  1091
    using True that by blast
wenzelm@50945
  1092
next
wenzelm@50945
  1093
  case False
wenzelm@50945
  1094
  note p = division_ofD[OF assms(1)]
lp15@60428
  1095
  have div_cbox: "\<forall>k\<in>p. \<exists>q. q division_of cbox a b \<and> k \<in> q"
wenzelm@50945
  1096
  proof
wenzelm@61165
  1097
    fix k
wenzelm@61165
  1098
    assume kp: "k \<in> p"
immler@56188
  1099
    obtain c d where k: "k = cbox c d"
wenzelm@61165
  1100
      using p(4)[OF kp] by blast
immler@56188
  1101
    have *: "cbox c d \<subseteq> cbox a b" "cbox c d \<noteq> {}"
wenzelm@61165
  1102
      using p(2,3)[OF kp, unfolded k] using assms(2)
immler@54776
  1103
      by (blast intro: order.trans)+
immler@56188
  1104
    obtain q where "q division_of cbox a b" "cbox c d \<in> q"
wenzelm@53408
  1105
      by (rule partial_division_extend_1[OF *])
wenzelm@61165
  1106
    then show "\<exists>q. q division_of cbox a b \<and> k \<in> q"
wenzelm@53408
  1107
      unfolding k by auto
wenzelm@50945
  1108
  qed
immler@56188
  1109
  obtain q where q: "\<And>x. x \<in> p \<Longrightarrow> q x division_of cbox a b" "\<And>x. x \<in> p \<Longrightarrow> x \<in> q x"
lp15@60428
  1110
    using bchoice[OF div_cbox] by blast
lp15@60394
  1111
  { fix x
wenzelm@53408
  1112
    assume x: "x \<in> p"
lp15@60394
  1113
    have "q x division_of \<Union>q x"
wenzelm@50945
  1114
      apply (rule division_ofI)
wenzelm@50945
  1115
      using division_ofD[OF q(1)[OF x]]
wenzelm@50945
  1116
      apply auto
lp15@60394
  1117
      done }
lp15@60394
  1118
  then have "\<And>x. x \<in> p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x - {x})"
lp15@60394
  1119
    by (meson Diff_subset division_of_subset)
wenzelm@60585
  1120
  then have "\<exists>d. d division_of \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p)"
wenzelm@50945
  1121
    apply -
lp15@60394
  1122
    apply (rule elementary_inters [OF finite_imageI[OF p(1)]])
lp15@60394
  1123
    apply (auto simp: False elementary_inters [OF finite_imageI[OF p(1)]])
wenzelm@50945
  1124
    done
wenzelm@53408
  1125
  then obtain d where d: "d division_of \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p)" ..
lp15@60394
  1126
  have "d \<union> p division_of cbox a b"
wenzelm@50945
  1127
  proof -
lp15@60394
  1128
    have te: "\<And>s f t. s \<noteq> {} \<Longrightarrow> \<forall>i\<in>s. f i \<union> i = t \<Longrightarrow> t = \<Inter>(f ` s) \<union> \<Union>s" by auto
lp15@60428
  1129
    have cbox_eq: "cbox a b = \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p) \<union> \<Union>p"
lp15@60394
  1130
    proof (rule te[OF False], clarify)
wenzelm@50945
  1131
      fix i
wenzelm@53408
  1132
      assume i: "i \<in> p"
immler@56188
  1133
      show "\<Union>(q i - {i}) \<union> i = cbox a b"
wenzelm@50945
  1134
        using division_ofD(6)[OF q(1)[OF i]] using q(2)[OF i] by auto
wenzelm@50945
  1135
    qed
lp15@60428
  1136
    { fix k
wenzelm@53408
  1137
      assume k: "k \<in> p"
lp15@60428
  1138
      have *: "\<And>u t s. t \<inter> s = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<inter> t = {}"
wenzelm@53408
  1139
        by auto
lp15@60428
  1140
      have "interior (\<Inter>i\<in>p. \<Union>(q i - {i})) \<inter> interior k = {}"
lp15@60428
  1141
      proof (rule *[OF inter_interior_unions_intervals])
wenzelm@50945
  1142
        note qk=division_ofD[OF q(1)[OF k]]
immler@56188
  1143
        show "finite (q k - {k})" "open (interior k)" "\<forall>t\<in>q k - {k}. \<exists>a b. t = cbox a b"
wenzelm@53408
  1144
          using qk by auto
wenzelm@50945
  1145
        show "\<forall>t\<in>q k - {k}. interior k \<inter> interior t = {}"
wenzelm@50945
  1146
          using qk(5) using q(2)[OF k] by auto
lp15@60428
  1147
        show "interior (\<Inter>i\<in>p. \<Union>(q i - {i})) \<subseteq> interior (\<Union>(q k - {k}))"
lp15@60428
  1148
          apply (rule interior_mono)+
wenzelm@53408
  1149
          using k
wenzelm@53408
  1150
          apply auto
wenzelm@53408
  1151
          done
lp15@60428
  1152
      qed } note [simp] = this
lp15@60428
  1153
    show "d \<union> p division_of (cbox a b)"
lp15@60428
  1154
      unfolding cbox_eq
lp15@60428
  1155
      apply (rule division_disjoint_union[OF d assms(1)])
lp15@60428
  1156
      apply (rule inter_interior_unions_intervals)
lp15@60428
  1157
      apply (rule p open_interior ballI)+
lp15@60615
  1158
      apply simp_all
lp15@60428
  1159
      done
lp15@60394
  1160
  qed
lp15@60394
  1161
  then show ?thesis
lp15@60394
  1162
    by (meson Un_upper2 that)
wenzelm@50945
  1163
qed
himmelma@35172
  1164
wenzelm@53399
  1165
lemma elementary_bounded[dest]:
immler@56188
  1166
  fixes s :: "'a::euclidean_space set"
wenzelm@53408
  1167
  shows "p division_of s \<Longrightarrow> bounded s"
immler@56189
  1168
  unfolding division_of_def by (metis bounded_Union bounded_cbox)
wenzelm@53399
  1169
immler@56188
  1170
lemma elementary_subset_cbox:
immler@56188
  1171
  "p division_of s \<Longrightarrow> \<exists>a b. s \<subseteq> cbox a (b::'a::euclidean_space)"
immler@56188
  1172
  by (meson elementary_bounded bounded_subset_cbox)
wenzelm@50945
  1173
wenzelm@50945
  1174
lemma division_union_intervals_exists:
immler@56188
  1175
  fixes a b :: "'a::euclidean_space"
immler@56188
  1176
  assumes "cbox a b \<noteq> {}"
immler@56188
  1177
  obtains p where "(insert (cbox a b) p) division_of (cbox a b \<union> cbox c d)"
immler@56188
  1178
proof (cases "cbox c d = {}")
wenzelm@50945
  1179
  case True
wenzelm@50945
  1180
  show ?thesis
wenzelm@50945
  1181
    apply (rule that[of "{}"])
wenzelm@50945
  1182
    unfolding True
wenzelm@50945
  1183
    using assms
wenzelm@50945
  1184
    apply auto
wenzelm@50945
  1185
    done
wenzelm@50945
  1186
next
wenzelm@50945
  1187
  case False
wenzelm@50945
  1188
  show ?thesis
immler@56188
  1189
  proof (cases "cbox a b \<inter> cbox c d = {}")
wenzelm@50945
  1190
    case True
wenzelm@50945
  1191
    show ?thesis
immler@56188
  1192
      apply (rule that[of "{cbox c d}"])
lp15@60428
  1193
      apply (subst insert_is_Un)
wenzelm@50945
  1194
      apply (rule division_disjoint_union)
lp15@60428
  1195
      using \<open>cbox c d \<noteq> {}\<close> True assms interior_subset
wenzelm@50945
  1196
      apply auto
wenzelm@50945
  1197
      done
wenzelm@50945
  1198
  next
wenzelm@50945
  1199
    case False
immler@56188
  1200
    obtain u v where uv: "cbox a b \<inter> cbox c d = cbox u v"
wenzelm@50945
  1201
      unfolding inter_interval by auto
lp15@60428
  1202
    have uv_sub: "cbox u v \<subseteq> cbox c d" using uv by auto
immler@56188
  1203
    obtain p where "p division_of cbox c d" "cbox u v \<in> p"
lp15@60428
  1204
      by (rule partial_division_extend_1[OF uv_sub False[unfolded uv]])
wenzelm@53408
  1205
    note p = this division_ofD[OF this(1)]
lp15@60428
  1206
    have "interior (cbox a b \<inter> \<Union>(p - {cbox u v})) = interior(cbox u v \<inter> \<Union>(p - {cbox u v}))"
lp15@60428
  1207
      apply (rule arg_cong[of _ _ interior])
lp15@60428
  1208
      using p(8) uv by auto
lp15@60428
  1209
    also have "\<dots> = {}"
lp15@60428
  1210
      unfolding interior_inter
lp15@60428
  1211
      apply (rule inter_interior_unions_intervals)
lp15@60428
  1212
      using p(6) p(7)[OF p(2)] p(3)
lp15@60428
  1213
      apply auto
lp15@60428
  1214
      done
lp15@60428
  1215
    finally have [simp]: "interior (cbox a b) \<inter> interior (\<Union>(p - {cbox u v})) = {}" by simp
lp15@60615
  1216
    have cbe: "cbox a b \<union> cbox c d = cbox a b \<union> \<Union>(p - {cbox u v})"
wenzelm@53399
  1217
      using p(8) unfolding uv[symmetric] by auto
wenzelm@50945
  1218
    show ?thesis
immler@56188
  1219
      apply (rule that[of "p - {cbox u v}"])
lp15@60428
  1220
      apply (simp add: cbe)
lp15@60428
  1221
      apply (subst insert_is_Un)
wenzelm@50945
  1222
      apply (rule division_disjoint_union)
lp15@60428
  1223
      apply (simp_all add: assms division_of_self)
lp15@60428
  1224
      by (metis Diff_subset division_of_subset p(1) p(8))
wenzelm@50945
  1225
  qed
wenzelm@50945
  1226
qed
himmelma@35172
  1227
wenzelm@53399
  1228
lemma division_of_unions:
wenzelm@53399
  1229
  assumes "finite f"
wenzelm@53408
  1230
    and "\<And>p. p \<in> f \<Longrightarrow> p division_of (\<Union>p)"
wenzelm@53399
  1231
    and "\<And>k1 k2. k1 \<in> \<Union>f \<Longrightarrow> k2 \<in> \<Union>f \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior k1 \<inter> interior k2 = {}"
wenzelm@53399
  1232
  shows "\<Union>f division_of \<Union>\<Union>f"
lp15@60384
  1233
  using assms
lp15@60384
  1234
  by (auto intro!: division_ofI)
wenzelm@53399
  1235
wenzelm@53399
  1236
lemma elementary_union_interval:
immler@56188
  1237
  fixes a b :: "'a::euclidean_space"
wenzelm@53399
  1238
  assumes "p division_of \<Union>p"
immler@56188
  1239
  obtains q where "q division_of (cbox a b \<union> \<Union>p)"
wenzelm@53399
  1240
proof -
wenzelm@53399
  1241
  note assm = division_ofD[OF assms]
wenzelm@53408
  1242
  have lem1: "\<And>f s. \<Union>\<Union>(f ` s) = \<Union>((\<lambda>x. \<Union>(f x)) ` s)"
wenzelm@53399
  1243
    by auto
wenzelm@53399
  1244
  have lem2: "\<And>f s. f \<noteq> {} \<Longrightarrow> \<Union>{s \<union> t |t. t \<in> f} = s \<union> \<Union>f"
wenzelm@53399
  1245
    by auto
wenzelm@53399
  1246
  {
wenzelm@53399
  1247
    presume "p = {} \<Longrightarrow> thesis"
immler@56188
  1248
      "cbox a b = {} \<Longrightarrow> thesis"
immler@56188
  1249
      "cbox a b \<noteq> {} \<Longrightarrow> interior (cbox a b) = {} \<Longrightarrow> thesis"
immler@56188
  1250
      "p \<noteq> {} \<Longrightarrow> interior (cbox a b)\<noteq>{} \<Longrightarrow> cbox a b \<noteq> {} \<Longrightarrow> thesis"
wenzelm@53399
  1251
    then show thesis by auto
wenzelm@53399
  1252
  next
wenzelm@53399
  1253
    assume as: "p = {}"
immler@56188
  1254
    obtain p where "p division_of (cbox a b)"
wenzelm@53408
  1255
      by (rule elementary_interval)
wenzelm@53399
  1256
    then show thesis
lp15@60384
  1257
      using as that by auto
wenzelm@53399
  1258
  next
immler@56188
  1259
    assume as: "cbox a b = {}"
wenzelm@53399
  1260
    show thesis
lp15@60384
  1261
      using as assms that by auto
wenzelm@53399
  1262
  next
immler@56188
  1263
    assume as: "interior (cbox a b) = {}" "cbox a b \<noteq> {}"
wenzelm@53399
  1264
    show thesis
immler@56188
  1265
      apply (rule that[of "insert (cbox a b) p"],rule division_ofI)
wenzelm@53399
  1266
      unfolding finite_insert
wenzelm@53399
  1267
      apply (rule assm(1)) unfolding Union_insert
wenzelm@53399
  1268
      using assm(2-4) as
wenzelm@53399
  1269
      apply -
immler@54775
  1270
      apply (fast dest: assm(5))+
wenzelm@53399
  1271
      done
wenzelm@53399
  1272
  next
immler@56188
  1273
    assume as: "p \<noteq> {}" "interior (cbox a b) \<noteq> {}" "cbox a b \<noteq> {}"
immler@56188
  1274
    have "\<forall>k\<in>p. \<exists>q. (insert (cbox a b) q) division_of (cbox a b \<union> k)"
lp15@60615
  1275
    proof
wenzelm@61165
  1276
      fix k
wenzelm@61165
  1277
      assume kp: "k \<in> p"
wenzelm@61165
  1278
      from assm(4)[OF kp] obtain c d where "k = cbox c d" by blast
wenzelm@61165
  1279
      then show "\<exists>q. (insert (cbox a b) q) division_of (cbox a b \<union> k)"
lp15@60384
  1280
        by (meson as(3) division_union_intervals_exists)
wenzelm@53399
  1281
    qed
immler@56188
  1282
    from bchoice[OF this] obtain q where "\<forall>x\<in>p. insert (cbox a b) (q x) division_of (cbox a b) \<union> x" ..
wenzelm@53408
  1283
    note q = division_ofD[OF this[rule_format]]
immler@56188
  1284
    let ?D = "\<Union>{insert (cbox a b) (q k) | k. k \<in> p}"
lp15@60615
  1285
    show thesis
lp15@60428
  1286
    proof (rule that[OF division_ofI])
immler@56188
  1287
      have *: "{insert (cbox a b) (q k) |k. k \<in> p} = (\<lambda>k. insert (cbox a b) (q k)) ` p"
wenzelm@53399
  1288
        by auto
wenzelm@53399
  1289
      show "finite ?D"
lp15@60384
  1290
        using "*" assm(1) q(1) by auto
immler@56188
  1291
      show "\<Union>?D = cbox a b \<union> \<Union>p"
wenzelm@53399
  1292
        unfolding * lem1
immler@56188
  1293
        unfolding lem2[OF as(1), of "cbox a b", symmetric]
wenzelm@53399
  1294
        using q(6)
wenzelm@53399
  1295
        by auto
wenzelm@53399
  1296
      fix k
wenzelm@53408
  1297
      assume k: "k \<in> ?D"
immler@56188
  1298
      then show "k \<subseteq> cbox a b \<union> \<Union>p"
wenzelm@53408
  1299
        using q(2) by auto
wenzelm@53399
  1300
      show "k \<noteq> {}"
wenzelm@53408
  1301
        using q(3) k by auto
immler@56188
  1302
      show "\<exists>a b. k = cbox a b"
wenzelm@53408
  1303
        using q(4) k by auto
wenzelm@53399
  1304
      fix k'
wenzelm@53408
  1305
      assume k': "k' \<in> ?D" "k \<noteq> k'"
immler@56188
  1306
      obtain x where x: "k \<in> insert (cbox a b) (q x)" "x\<in>p"
wenzelm@53408
  1307
        using k by auto
immler@56188
  1308
      obtain x' where x': "k'\<in>insert (cbox a b) (q x')" "x'\<in>p"
wenzelm@53399
  1309
        using k' by auto
wenzelm@53399
  1310
      show "interior k \<inter> interior k' = {}"
wenzelm@53399
  1311
      proof (cases "x = x'")
wenzelm@53399
  1312
        case True
wenzelm@53399
  1313
        show ?thesis
lp15@60384
  1314
          using True k' q(5) x' x by auto
wenzelm@53399
  1315
      next
wenzelm@53399
  1316
        case False
wenzelm@53399
  1317
        {
immler@56188
  1318
          presume "k = cbox a b \<Longrightarrow> ?thesis"
immler@56188
  1319
            and "k' = cbox a b \<Longrightarrow> ?thesis"
immler@56188
  1320
            and "k \<noteq> cbox a b \<Longrightarrow> k' \<noteq> cbox a b \<Longrightarrow> ?thesis"
wenzelm@53399
  1321
          then show ?thesis by auto
wenzelm@53399
  1322
        next
immler@56188
  1323
          assume as': "k  = cbox a b"
wenzelm@53399
  1324
          show ?thesis
lp15@60384
  1325
            using as' k' q(5) x' by auto
wenzelm@53399
  1326
        next
immler@56188
  1327
          assume as': "k' = cbox a b"
wenzelm@53399
  1328
          show ?thesis
lp15@60384
  1329
            using as' k'(2) q(5) x by auto
wenzelm@53399
  1330
        }
immler@56188
  1331
        assume as': "k \<noteq> cbox a b" "k' \<noteq> cbox a b"
immler@56188
  1332
        obtain c d where k: "k = cbox c d"
wenzelm@53408
  1333
          using q(4)[OF x(2,1)] by blast
immler@56188
  1334
        have "interior k \<inter> interior (cbox a b) = {}"
lp15@60384
  1335
          using as' k'(2) q(5) x by auto
wenzelm@53399
  1336
        then have "interior k \<subseteq> interior x"
lp15@60384
  1337
        using interior_subset_union_intervals
lp15@60384
  1338
          by (metis as(2) k q(2) x interior_subset_union_intervals)
wenzelm@53399
  1339
        moreover
immler@56188
  1340
        obtain c d where c_d: "k' = cbox c d"
wenzelm@53408
  1341
          using q(4)[OF x'(2,1)] by blast
immler@56188
  1342
        have "interior k' \<inter> interior (cbox a b) = {}"
lp15@60384
  1343
          using as'(2) q(5) x' by auto
wenzelm@53399
  1344
        then have "interior k' \<subseteq> interior x'"
lp15@60384
  1345
          by (metis as(2) c_d interior_subset_union_intervals q(2) x'(1) x'(2))
wenzelm@53399
  1346
        ultimately show ?thesis
wenzelm@53399
  1347
          using assm(5)[OF x(2) x'(2) False] by auto
wenzelm@53399
  1348
      qed
wenzelm@53399
  1349
    qed
wenzelm@53399
  1350
  }
wenzelm@53399
  1351
qed
himmelma@35172
  1352
himmelma@35172
  1353
lemma elementary_unions_intervals:
wenzelm@53399
  1354
  assumes fin: "finite f"
immler@56188
  1355
    and "\<And>s. s \<in> f \<Longrightarrow> \<exists>a b. s = cbox a (b::'a::euclidean_space)"
wenzelm@53399
  1356
  obtains p where "p division_of (\<Union>f)"
wenzelm@53399
  1357
proof -
wenzelm@53399
  1358
  have "\<exists>p. p division_of (\<Union>f)"
wenzelm@53399
  1359
  proof (induct_tac f rule:finite_subset_induct)
himmelma@35172
  1360
    show "\<exists>p. p division_of \<Union>{}" using elementary_empty by auto
wenzelm@53399
  1361
  next
wenzelm@53399
  1362
    fix x F
wenzelm@53399
  1363
    assume as: "finite F" "x \<notin> F" "\<exists>p. p division_of \<Union>F" "x\<in>f"
wenzelm@53408
  1364
    from this(3) obtain p where p: "p division_of \<Union>F" ..
immler@56188
  1365
    from assms(2)[OF as(4)] obtain a b where x: "x = cbox a b" by blast
wenzelm@53399
  1366
    have *: "\<Union>F = \<Union>p"
wenzelm@53399
  1367
      using division_ofD[OF p] by auto
wenzelm@53399
  1368
    show "\<exists>p. p division_of \<Union>insert x F"
wenzelm@53399
  1369
      using elementary_union_interval[OF p[unfolded *], of a b]
lp15@59765
  1370
      unfolding Union_insert x * by metis
wenzelm@53408
  1371
  qed (insert assms, auto)
wenzelm@53399
  1372
  then show ?thesis
lp15@60384
  1373
    using that by auto
wenzelm@53399
  1374
qed
wenzelm@53399
  1375
wenzelm@53399
  1376
lemma elementary_union:
immler@56188
  1377
  fixes s t :: "'a::euclidean_space set"
lp15@60384
  1378
  assumes "ps division_of s" "pt division_of t"
himmelma@35172
  1379
  obtains p where "p division_of (s \<union> t)"
wenzelm@53399
  1380
proof -
lp15@60384
  1381
  have *: "s \<union> t = \<Union>ps \<union> \<Union>pt"
wenzelm@53399
  1382
    using assms unfolding division_of_def by auto
wenzelm@53399
  1383
  show ?thesis
wenzelm@53408
  1384
    apply (rule elementary_unions_intervals[of "ps \<union> pt"])
lp15@60384
  1385
    using assms apply auto
lp15@60384
  1386
    by (simp add: * that)
wenzelm@53399
  1387
qed
wenzelm@53399
  1388
wenzelm@53399
  1389
lemma partial_division_extend:
immler@56188
  1390
  fixes t :: "'a::euclidean_space set"
wenzelm@53399
  1391
  assumes "p division_of s"
wenzelm@53399
  1392
    and "q division_of t"
wenzelm@53399
  1393
    and "s \<subseteq> t"
wenzelm@53399
  1394
  obtains r where "p \<subseteq> r" and "r division_of t"
wenzelm@53399
  1395
proof -
himmelma@35172
  1396
  note divp = division_ofD[OF assms(1)] and divq = division_ofD[OF assms(2)]
immler@56188
  1397
  obtain a b where ab: "t \<subseteq> cbox a b"
immler@56188
  1398
    using elementary_subset_cbox[OF assms(2)] by auto
immler@56188
  1399
  obtain r1 where "p \<subseteq> r1" "r1 division_of (cbox a b)"
lp15@60384
  1400
    using assms
lp15@60384
  1401
    by (metis ab dual_order.trans partial_division_extend_interval divp(6))
wenzelm@53399
  1402
  note r1 = this division_ofD[OF this(2)]
wenzelm@53408
  1403
  obtain p' where "p' division_of \<Union>(r1 - p)"
wenzelm@53399
  1404
    apply (rule elementary_unions_intervals[of "r1 - p"])
wenzelm@53399
  1405
    using r1(3,6)
wenzelm@53399
  1406
    apply auto
wenzelm@53399
  1407
    done
wenzelm@53399
  1408
  then obtain r2 where r2: "r2 division_of (\<Union>(r1 - p)) \<inter> (\<Union>q)"
lp15@60384
  1409
    by (metis assms(2) divq(6) elementary_inter)
wenzelm@53399
  1410
  {
wenzelm@53399
  1411
    fix x
wenzelm@53399
  1412
    assume x: "x \<in> t" "x \<notin> s"
wenzelm@53399
  1413
    then have "x\<in>\<Union>r1"
wenzelm@53399
  1414
      unfolding r1 using ab by auto
wenzelm@53408
  1415
    then obtain r where r: "r \<in> r1" "x \<in> r"
wenzelm@53408
  1416
      unfolding Union_iff ..
wenzelm@53399
  1417
    moreover
wenzelm@53399
  1418
    have "r \<notin> p"
wenzelm@53399
  1419
    proof
wenzelm@53399
  1420
      assume "r \<in> p"
wenzelm@53399
  1421
      then have "x \<in> s" using divp(2) r by auto
wenzelm@53399
  1422
      then show False using x by auto
wenzelm@53399
  1423
    qed
wenzelm@53399
  1424
    ultimately have "x\<in>\<Union>(r1 - p)" by auto
wenzelm@53399
  1425
  }
wenzelm@53399
  1426
  then have *: "t = \<Union>p \<union> (\<Union>(r1 - p) \<inter> \<Union>q)"
wenzelm@53399
  1427
    unfolding divp divq using assms(3) by auto
wenzelm@53399
  1428
  show ?thesis
wenzelm@53399
  1429
    apply (rule that[of "p \<union> r2"])
wenzelm@53399
  1430
    unfolding *
wenzelm@53399
  1431
    defer
wenzelm@53399
  1432
    apply (rule division_disjoint_union)
wenzelm@53399
  1433
    unfolding divp(6)
wenzelm@53399
  1434
    apply(rule assms r2)+
wenzelm@53399
  1435
  proof -
wenzelm@53399
  1436
    have "interior s \<inter> interior (\<Union>(r1-p)) = {}"
wenzelm@53399
  1437
    proof (rule inter_interior_unions_intervals)
immler@56188
  1438
      show "finite (r1 - p)" and "open (interior s)" and "\<forall>t\<in>r1-p. \<exists>a b. t = cbox a b"
wenzelm@53399
  1439
        using r1 by auto
wenzelm@53399
  1440
      have *: "\<And>s. (\<And>x. x \<in> s \<Longrightarrow> False) \<Longrightarrow> s = {}"
wenzelm@53399
  1441
        by auto
wenzelm@53399
  1442
      show "\<forall>t\<in>r1-p. interior s \<inter> interior t = {}"
wenzelm@53399
  1443
      proof
wenzelm@53399
  1444
        fix m x
wenzelm@53399
  1445
        assume as: "m \<in> r1 - p"
wenzelm@53399
  1446
        have "interior m \<inter> interior (\<Union>p) = {}"
wenzelm@53399
  1447
        proof (rule inter_interior_unions_intervals)
immler@56188
  1448
          show "finite p" and "open (interior m)" and "\<forall>t\<in>p. \<exists>a b. t = cbox a b"
wenzelm@53399
  1449
            using divp by auto
wenzelm@53399
  1450
          show "\<forall>t\<in>p. interior m \<inter> interior t = {}"
lp15@60384
  1451
            by (metis DiffD1 DiffD2 as r1(1) r1(7) set_rev_mp)
wenzelm@53399
  1452
        qed
wenzelm@53399
  1453
        then show "interior s \<inter> interior m = {}"
wenzelm@53399
  1454
          unfolding divp by auto
wenzelm@53399
  1455
      qed
wenzelm@53399
  1456
    qed
wenzelm@53399
  1457
    then show "interior s \<inter> interior (\<Union>(r1-p) \<inter> (\<Union>q)) = {}"
wenzelm@53399
  1458
      using interior_subset by auto
wenzelm@53399
  1459
  qed auto
wenzelm@53399
  1460
qed
wenzelm@53399
  1461
himmelma@35172
  1462
wenzelm@60420
  1463
subsection \<open>Tagged (partial) divisions.\<close>
himmelma@35172
  1464
wenzelm@53408
  1465
definition tagged_partial_division_of (infixr "tagged'_partial'_division'_of" 40)
wenzelm@53408
  1466
  where "s tagged_partial_division_of i \<longleftrightarrow>
wenzelm@53408
  1467
    finite s \<and>
immler@56188
  1468
    (\<forall>x k. (x, k) \<in> s \<longrightarrow> x \<in> k \<and> k \<subseteq> i \<and> (\<exists>a b. k = cbox a b)) \<and>
wenzelm@53408
  1469
    (\<forall>x1 k1 x2 k2. (x1, k1) \<in> s \<and> (x2, k2) \<in> s \<and> (x1, k1) \<noteq> (x2, k2) \<longrightarrow>
wenzelm@53408
  1470
      interior k1 \<inter> interior k2 = {})"
wenzelm@53408
  1471
wenzelm@53408
  1472
lemma tagged_partial_division_ofD[dest]:
wenzelm@53408
  1473
  assumes "s tagged_partial_division_of i"
wenzelm@53408
  1474
  shows "finite s"
wenzelm@53408
  1475
    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> x \<in> k"
wenzelm@53408
  1476
    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> i"
immler@56188
  1477
    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b"
wenzelm@53408
  1478
    and "\<And>x1 k1 x2 k2. (x1,k1) \<in> s \<Longrightarrow>
wenzelm@53408
  1479
      (x2, k2) \<in> s \<Longrightarrow> (x1, k1) \<noteq> (x2, k2) \<Longrightarrow> interior k1 \<inter> interior k2 = {}"
wenzelm@53408
  1480
  using assms unfolding tagged_partial_division_of_def by blast+
wenzelm@53408
  1481
wenzelm@53408
  1482
definition tagged_division_of (infixr "tagged'_division'_of" 40)
wenzelm@53408
  1483
  where "s tagged_division_of i \<longleftrightarrow> s tagged_partial_division_of i \<and> (\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
himmelma@35172
  1484
huffman@44167
  1485
lemma tagged_division_of_finite: "s tagged_division_of i \<Longrightarrow> finite s"
himmelma@35172
  1486
  unfolding tagged_division_of_def tagged_partial_division_of_def by auto
himmelma@35172
  1487
himmelma@35172
  1488
lemma tagged_division_of:
wenzelm@53408
  1489
  "s tagged_division_of i \<longleftrightarrow>
wenzelm@53408
  1490
    finite s \<and>
immler@56188
  1491
    (\<forall>x k. (x, k) \<in> s \<longrightarrow> x \<in> k \<and> k \<subseteq> i \<and> (\<exists>a b. k = cbox a b)) \<and>
wenzelm@53408
  1492
    (\<forall>x1 k1 x2 k2. (x1, k1) \<in> s \<and> (x2, k2) \<in> s \<and> (x1, k1) \<noteq> (x2, k2) \<longrightarrow>
wenzelm@53408
  1493
      interior k1 \<inter> interior k2 = {}) \<and>
wenzelm@53408
  1494
    (\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
himmelma@35172
  1495
  unfolding tagged_division_of_def tagged_partial_division_of_def by auto
himmelma@35172
  1496
wenzelm@53408
  1497
lemma tagged_division_ofI:
wenzelm@53408
  1498
  assumes "finite s"
wenzelm@53408
  1499
    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> x \<in> k"
wenzelm@53408
  1500
    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> i"
immler@56188
  1501
    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b"
wenzelm@53408
  1502
    and "\<And>x1 k1 x2 k2. (x1,k1) \<in> s \<Longrightarrow> (x2, k2) \<in> s \<Longrightarrow> (x1, k1) \<noteq> (x2, k2) \<Longrightarrow>
wenzelm@53408
  1503
      interior k1 \<inter> interior k2 = {}"
wenzelm@53408
  1504
    and "(\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
himmelma@35172
  1505
  shows "s tagged_division_of i"
wenzelm@53408
  1506
  unfolding tagged_division_of
lp15@60384
  1507
  using assms
lp15@60384
  1508
  apply auto
lp15@60384
  1509
  apply fastforce+
wenzelm@53408
  1510
  done
wenzelm@53408
  1511
lp15@60384
  1512
lemma tagged_division_ofD[dest]:  (*FIXME USE A LOCALE*)
wenzelm@53408
  1513
  assumes "s tagged_division_of i"
wenzelm@53408
  1514
  shows "finite s"
wenzelm@53408
  1515
    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> x \<in> k"
wenzelm@53408
  1516
    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> i"
immler@56188
  1517
    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b"
wenzelm@53408
  1518
    and "\<And>x1 k1 x2 k2. (x1, k1) \<in> s \<Longrightarrow> (x2, k2) \<in> s \<Longrightarrow> (x1, k1) \<noteq> (x2, k2) \<Longrightarrow>
wenzelm@53408
  1519
      interior k1 \<inter> interior k2 = {}"
wenzelm@53408
  1520
    and "(\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
wenzelm@53408
  1521
  using assms unfolding tagged_division_of by blast+
wenzelm@53408
  1522
wenzelm@53408
  1523
lemma division_of_tagged_division:
wenzelm@53408
  1524
  assumes "s tagged_division_of i"
wenzelm@53408
  1525
  shows "(snd ` s) division_of i"
wenzelm@53408
  1526
proof (rule division_ofI)
wenzelm@53408
  1527
  note assm = tagged_division_ofD[OF assms]
wenzelm@53408
  1528
  show "\<Union>(snd ` s) = i" "finite (snd ` s)"
wenzelm@53408
  1529
    using assm by auto
wenzelm@53408
  1530
  fix k
wenzelm@53408
  1531
  assume k: "k \<in> snd ` s"
wenzelm@53408
  1532
  then obtain xk where xk: "(xk, k) \<in> s"
wenzelm@53408
  1533
    by auto
immler@56188
  1534
  then show "k \<subseteq> i" "k \<noteq> {}" "\<exists>a b. k = cbox a b"
wenzelm@53408
  1535
    using assm by fastforce+
wenzelm@53408
  1536
  fix k'
wenzelm@53408
  1537
  assume k': "k' \<in> snd ` s" "k \<noteq> k'"
wenzelm@53408
  1538
  from this(1) obtain xk' where xk': "(xk', k') \<in> s"
wenzelm@53408
  1539
    by auto
wenzelm@53408
  1540
  then show "interior k \<inter> interior k' = {}"
lp15@60384
  1541
    using assm(5) k'(2) xk by blast
himmelma@35172
  1542
qed
himmelma@35172
  1543
wenzelm@53408
  1544
lemma partial_division_of_tagged_division:
wenzelm@53408
  1545
  assumes "s tagged_partial_division_of i"
himmelma@35172
  1546
  shows "(snd ` s) division_of \<Union>(snd ` s)"
wenzelm@53408
  1547
proof (rule division_ofI)
wenzelm@53408
  1548
  note assm = tagged_partial_division_ofD[OF assms]
wenzelm@53408
  1549
  show "finite (snd ` s)" "\<Union>(snd ` s) = \<Union>(snd ` s)"
wenzelm@53408
  1550
    using assm by auto
wenzelm@53408
  1551
  fix k
wenzelm@53408
  1552
  assume k: "k \<in> snd ` s"
wenzelm@53408
  1553
  then obtain xk where xk: "(xk, k) \<in> s"
wenzelm@53408
  1554
    by auto
immler@56188
  1555
  then show "k \<noteq> {}" "\<exists>a b. k = cbox a b" "k \<subseteq> \<Union>(snd ` s)"
wenzelm@53408
  1556
    using assm by auto
wenzelm@53408
  1557
  fix k'
wenzelm@53408
  1558
  assume k': "k' \<in> snd ` s" "k \<noteq> k'"
wenzelm@53408
  1559
  from this(1) obtain xk' where xk': "(xk', k') \<in> s"
wenzelm@53408
  1560
    by auto
wenzelm@53408
  1561
  then show "interior k \<inter> interior k' = {}"
lp15@60384
  1562
    using assm(5) k'(2) xk by auto
himmelma@35172
  1563
qed
himmelma@35172
  1564
wenzelm@53408
  1565
lemma tagged_partial_division_subset:
wenzelm@53408
  1566
  assumes "s tagged_partial_division_of i"
wenzelm@53408
  1567
    and "t \<subseteq> s"
himmelma@35172
  1568
  shows "t tagged_partial_division_of i"
wenzelm@53408
  1569
  using assms
wenzelm@53408
  1570
  unfolding tagged_partial_division_of_def
wenzelm@53408
  1571
  using finite_subset[OF assms(2)]
wenzelm@53408
  1572
  by blast
wenzelm@53408
  1573
wenzelm@53408
  1574
lemma setsum_over_tagged_division_lemma:
wenzelm@53408
  1575
  assumes "p tagged_division_of i"
immler@56188
  1576
    and "\<And>u v. cbox u v \<noteq> {} \<Longrightarrow> content (cbox u v) = 0 \<Longrightarrow> d (cbox u v) = 0"
himmelma@35172
  1577
  shows "setsum (\<lambda>(x,k). d k) p = setsum d (snd ` p)"
wenzelm@53408
  1578
proof -
wenzelm@53408
  1579
  have *: "(\<lambda>(x,k). d k) = d \<circ> snd"
wenzelm@53408
  1580
    unfolding o_def by (rule ext) auto
hoelzl@57129
  1581
  note assm = tagged_division_ofD[OF assms(1)]
wenzelm@53408
  1582
  show ?thesis
wenzelm@53408
  1583
    unfolding *
haftmann@57418
  1584
  proof (rule setsum.reindex_nontrivial[symmetric])
wenzelm@53408
  1585
    show "finite p"
wenzelm@53408
  1586
      using assm by auto
wenzelm@53408
  1587
    fix x y
hoelzl@57129
  1588
    assume "x\<in>p" "y\<in>p" "x\<noteq>y" "snd x = snd y"
immler@56188
  1589
    obtain a b where ab: "snd x = cbox a b"
wenzelm@60420
  1590
      using assm(4)[of "fst x" "snd x"] \<open>x\<in>p\<close> by auto
wenzelm@53408
  1591
    have "(fst x, snd y) \<in> p" "(fst x, snd y) \<noteq> y"
wenzelm@60420
  1592
      by (metis pair_collapse \<open>x\<in>p\<close> \<open>snd x = snd y\<close> \<open>x \<noteq> y\<close>)+
wenzelm@60420
  1593
    with \<open>x\<in>p\<close> \<open>y\<in>p\<close> have "interior (snd x) \<inter> interior (snd y) = {}"
hoelzl@57129
  1594
      by (intro assm(5)[of "fst x" _ "fst y"]) auto
immler@56188
  1595
    then have "content (cbox a b) = 0"
wenzelm@60420
  1596
      unfolding \<open>snd x = snd y\<close>[symmetric] ab content_eq_0_interior by auto
immler@56188
  1597
    then have "d (cbox a b) = 0"
wenzelm@60420
  1598
      using assm(2)[of "fst x" "snd x"] \<open>x\<in>p\<close> ab[symmetric] by (intro assms(2)) auto
wenzelm@53408
  1599
    then show "d (snd x) = 0"
wenzelm@53408
  1600
      unfolding ab by auto
wenzelm@53408
  1601
  qed
wenzelm@53408
  1602
qed
wenzelm@53408
  1603
wenzelm@53408
  1604
lemma tag_in_interval: "p tagged_division_of i \<Longrightarrow> (x, k) \<in> p \<Longrightarrow> x \<in> i"
wenzelm@53408
  1605
  by auto
himmelma@35172
  1606
himmelma@35172
  1607
lemma tagged_division_of_empty: "{} tagged_division_of {}"
himmelma@35172
  1608
  unfolding tagged_division_of by auto
himmelma@35172
  1609
wenzelm@53408
  1610
lemma tagged_partial_division_of_trivial[simp]: "p tagged_partial_division_of {} \<longleftrightarrow> p = {}"
himmelma@35172
  1611
  unfolding tagged_partial_division_of_def by auto
himmelma@35172
  1612
wenzelm@53408
  1613
lemma tagged_division_of_trivial[simp]: "p tagged_division_of {} \<longleftrightarrow> p = {}"
himmelma@35172
  1614
  unfolding tagged_division_of by auto
himmelma@35172
  1615
immler@56188
  1616
lemma tagged_division_of_self: "x \<in> cbox a b \<Longrightarrow> {(x,cbox a b)} tagged_division_of (cbox a b)"
wenzelm@53408
  1617
  by (rule tagged_division_ofI) auto
himmelma@35172
  1618
immler@56188
  1619
lemma tagged_division_of_self_real: "x \<in> {a .. b::real} \<Longrightarrow> {(x,{a .. b})} tagged_division_of {a .. b}"
immler@56188
  1620
  unfolding box_real[symmetric]
immler@56188
  1621
  by (rule tagged_division_of_self)
immler@56188
  1622
himmelma@35172
  1623
lemma tagged_division_union:
wenzelm@53408
  1624
  assumes "p1 tagged_division_of s1"
wenzelm@53408
  1625
    and "p2 tagged_division_of s2"
wenzelm@53408
  1626
    and "interior s1 \<inter> interior s2 = {}"
himmelma@35172
  1627
  shows "(p1 \<union> p2) tagged_division_of (s1 \<union> s2)"
wenzelm@53408
  1628
proof (rule tagged_division_ofI)
wenzelm@53408
  1629
  note p1 = tagged_division_ofD[OF assms(1)]
wenzelm@53408
  1630
  note p2 = tagged_division_ofD[OF assms(2)]
wenzelm@53408
  1631
  show "finite (p1 \<union> p2)"
wenzelm@53408
  1632
    using p1(1) p2(1) by auto
wenzelm@53408
  1633
  show "\<Union>{k. \<exists>x. (x, k) \<in> p1 \<union> p2} = s1 \<union> s2"
wenzelm@53408
  1634
    using p1(6) p2(6) by blast
wenzelm@53408
  1635
  fix x k
wenzelm@53408
  1636
  assume xk: "(x, k) \<in> p1 \<union> p2"
immler@56188
  1637
  show "x \<in> k" "\<exists>a b. k = cbox a b"
wenzelm@53408
  1638
    using xk p1(2,4) p2(2,4) by auto
wenzelm@53408
  1639
  show "k \<subseteq> s1 \<union> s2"
wenzelm@53408
  1640
    using xk p1(3) p2(3) by blast
wenzelm@53408
  1641
  fix x' k'
wenzelm@53408
  1642
  assume xk': "(x', k') \<in> p1 \<union> p2" "(x, k) \<noteq> (x', k')"
wenzelm@53408
  1643
  have *: "\<And>a b. a \<subseteq> s1 \<Longrightarrow> b \<subseteq> s2 \<Longrightarrow> interior a \<inter> interior b = {}"
wenzelm@53408
  1644
    using assms(3) interior_mono by blast
wenzelm@53408
  1645
  show "interior k \<inter> interior k' = {}"
wenzelm@53408
  1646
    apply (cases "(x, k) \<in> p1")
lp15@60384
  1647
    apply (meson "*" UnE assms(1) assms(2) p1(5) tagged_division_ofD(3) xk'(1) xk'(2))
lp15@60384
  1648
    by (metis "*" UnE assms(1) assms(2) inf_sup_aci(1) p2(5) tagged_division_ofD(3) xk xk'(1) xk'(2))
wenzelm@53408
  1649
qed
himmelma@35172
  1650
himmelma@35172
  1651
lemma tagged_division_unions:
wenzelm@53408
  1652
  assumes "finite iset"
wenzelm@53408
  1653
    and "\<forall>i\<in>iset. pfn i tagged_division_of i"
wenzelm@53408
  1654
    and "\<forall>i1\<in>iset. \<forall>i2\<in>iset. i1 \<noteq> i2 \<longrightarrow> interior(i1) \<inter> interior(i2) = {}"
himmelma@35172
  1655
  shows "\<Union>(pfn ` iset) tagged_division_of (\<Union>iset)"
wenzelm@53408
  1656
proof (rule tagged_division_ofI)
himmelma@35172
  1657
  note assm = tagged_division_ofD[OF assms(2)[rule_format]]
wenzelm@53408
  1658
  show "finite (\<Union>(pfn ` iset))"
wenzelm@53408
  1659
    apply (rule finite_Union)
wenzelm@53408
  1660
    using assms
wenzelm@53408
  1661
    apply auto
wenzelm@53408
  1662
    done
wenzelm@53408
  1663
  have "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>(pfn ` iset)} = \<Union>((\<lambda>i. \<Union>{k. \<exists>x. (x, k) \<in> pfn i}) ` iset)"
wenzelm@53408
  1664
    by blast
wenzelm@53408
  1665
  also have "\<dots> = \<Union>iset"
wenzelm@53408
  1666
    using assm(6) by auto
wenzelm@53399
  1667
  finally show "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>(pfn ` iset)} = \<Union>iset" .
wenzelm@53408
  1668
  fix x k
wenzelm@53408
  1669
  assume xk: "(x, k) \<in> \<Union>(pfn ` iset)"
wenzelm@53408
  1670
  then obtain i where i: "i \<in> iset" "(x, k) \<in> pfn i"
wenzelm@53408
  1671
    by auto
immler@56188
  1672
  show "x \<in> k" "\<exists>a b. k = cbox a b" "k \<subseteq> \<Union>iset"
wenzelm@53408
  1673
    using assm(2-4)[OF i] using i(1) by auto
wenzelm@53408
  1674
  fix x' k'
wenzelm@53408
  1675
  assume xk': "(x', k') \<in> \<Union>(pfn ` iset)" "(x, k) \<noteq> (x', k')"
wenzelm@53408
  1676
  then obtain i' where i': "i' \<in> iset" "(x', k') \<in> pfn i'"
wenzelm@53408
  1677
    by auto
wenzelm@53408
  1678
  have *: "\<And>a b. i \<noteq> i' \<Longrightarrow> a \<subseteq> i \<Longrightarrow> b \<subseteq> i' \<Longrightarrow> interior a \<inter> interior b = {}"
wenzelm@53408
  1679
    using i(1) i'(1)
wenzelm@53408
  1680
    using assms(3)[rule_format] interior_mono
wenzelm@53408
  1681
    by blast
wenzelm@53408
  1682
  show "interior k \<inter> interior k' = {}"
wenzelm@53408
  1683
    apply (cases "i = i'")
lp15@60384
  1684
    using assm(5) i' i(2) xk'(2) apply blast
lp15@60384
  1685
    using "*" assm(3) i' i by auto
himmelma@35172
  1686
qed
himmelma@35172
  1687
himmelma@35172
  1688
lemma tagged_partial_division_of_union_self:
wenzelm@53408
  1689
  assumes "p tagged_partial_division_of s"
himmelma@35172
  1690
  shows "p tagged_division_of (\<Union>(snd ` p))"
wenzelm@53408
  1691
  apply (rule tagged_division_ofI)
wenzelm@53408
  1692
  using tagged_partial_division_ofD[OF assms]
wenzelm@53408
  1693
  apply auto
wenzelm@53408
  1694
  done
wenzelm@53408
  1695
wenzelm@53408
  1696
lemma tagged_division_of_union_self:
wenzelm@53408
  1697
  assumes "p tagged_division_of s"
wenzelm@53408
  1698
  shows "p tagged_division_of (\<Union>(snd ` p))"
wenzelm@53408
  1699
  apply (rule tagged_division_ofI)
wenzelm@53408
  1700
  using tagged_division_ofD[OF assms]
wenzelm@53408
  1701
  apply auto
wenzelm@53408
  1702
  done
wenzelm@53408
  1703
himmelma@35172
  1704
wenzelm@60420
  1705
subsection \<open>Fine-ness of a partition w.r.t. a gauge.\<close>
himmelma@35172
  1706
wenzelm@53408
  1707
definition fine  (infixr "fine" 46)
wenzelm@53408
  1708
  where "d fine s \<longleftrightarrow> (\<forall>(x,k) \<in> s. k \<subseteq> d x)"
wenzelm@53408
  1709
wenzelm@53408
  1710
lemma fineI:
wenzelm@53408
  1711
  assumes "\<And>x k. (x, k) \<in> s \<Longrightarrow> k \<subseteq> d x"
wenzelm@53408
  1712
  shows "d fine s"
wenzelm@53408
  1713
  using assms unfolding fine_def by auto
wenzelm@53408
  1714
wenzelm@53408
  1715
lemma fineD[dest]:
wenzelm@53408
  1716
  assumes "d fine s"
wenzelm@53408
  1717
  shows "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> d x"
wenzelm@53408
  1718
  using assms unfolding fine_def by auto
himmelma@35172
  1719
himmelma@35172
  1720
lemma fine_inter: "(\<lambda>x. d1 x \<inter> d2 x) fine p \<longleftrightarrow> d1 fine p \<and> d2 fine p"
himmelma@35172
  1721
  unfolding fine_def by auto
himmelma@35172
  1722
himmelma@35172
  1723
lemma fine_inters:
wenzelm@60585
  1724
 "(\<lambda>x. \<Inter>{f d x | d.  d \<in> s}) fine p \<longleftrightarrow> (\<forall>d\<in>s. (f d) fine p)"
himmelma@35172
  1725
  unfolding fine_def by blast
himmelma@35172
  1726
wenzelm@53408
  1727
lemma fine_union: "d fine p1 \<Longrightarrow> d fine p2 \<Longrightarrow> d fine (p1 \<union> p2)"
himmelma@35172
  1728
  unfolding fine_def by blast
himmelma@35172
  1729
wenzelm@53408
  1730
lemma fine_unions: "(\<And>p. p \<in> ps \<Longrightarrow> d fine p) \<Longrightarrow> d fine (\<Union>ps)"
himmelma@35172
  1731
  unfolding fine_def by auto
himmelma@35172
  1732
wenzelm@53408
  1733
lemma fine_subset: "p \<subseteq> q \<Longrightarrow> d fine q \<Longrightarrow> d fine p"
himmelma@35172
  1734
  unfolding fine_def by blast
himmelma@35172
  1735
wenzelm@53408
  1736
wenzelm@60420
  1737
subsection \<open>Gauge integral. Define on compact intervals first, then use a limit.\<close>
himmelma@35172
  1738
wenzelm@53408
  1739
definition has_integral_compact_interval (infixr "has'_integral'_compact'_interval" 46)
wenzelm@53408
  1740
  where "(f has_integral_compact_interval y) i \<longleftrightarrow>
wenzelm@53408
  1741
    (\<forall>e>0. \<exists>d. gauge d \<and>
wenzelm@53408
  1742
      (\<forall>p. p tagged_division_of i \<and> d fine p \<longrightarrow>
wenzelm@53408
  1743
        norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - y) < e))"
wenzelm@53408
  1744
wenzelm@53408
  1745
definition has_integral ::
immler@56188
  1746
    "('n::euclidean_space \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'b \<Rightarrow> 'n set \<Rightarrow> bool"
wenzelm@53408
  1747
  (infixr "has'_integral" 46)
wenzelm@53408
  1748
  where "(f has_integral y) i \<longleftrightarrow>
immler@56188
  1749
    (if \<exists>a b. i = cbox a b
wenzelm@53408
  1750
     then (f has_integral_compact_interval y) i
immler@56188
  1751
     else (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
immler@56188
  1752
      (\<exists>z. ((\<lambda>x. if x \<in> i then f x else 0) has_integral_compact_interval z) (cbox a b) \<and>
wenzelm@53408
  1753
        norm (z - y) < e)))"
himmelma@35172
  1754
himmelma@35172
  1755
lemma has_integral:
immler@56188
  1756
  "(f has_integral y) (cbox a b) \<longleftrightarrow>
wenzelm@53408
  1757
    (\<forall>e>0. \<exists>d. gauge d \<and>
immler@56188
  1758
      (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
wenzelm@53408
  1759
        norm (setsum (\<lambda>(x,k). content(k) *\<^sub>R f x) p - y) < e))"
wenzelm@53408
  1760
  unfolding has_integral_def has_integral_compact_interval_def
wenzelm@53408
  1761
  by auto
wenzelm@53408
  1762
immler@56188
  1763
lemma has_integral_real:
immler@56188
  1764
  "(f has_integral y) {a .. b::real} \<longleftrightarrow>
immler@56188
  1765
    (\<forall>e>0. \<exists>d. gauge d \<and>
immler@56188
  1766
      (\<forall>p. p tagged_division_of {a .. b} \<and> d fine p \<longrightarrow>
immler@56188
  1767
        norm (setsum (\<lambda>(x,k). content(k) *\<^sub>R f x) p - y) < e))"
immler@56188
  1768
  unfolding box_real[symmetric]
immler@56188
  1769
  by (rule has_integral)
immler@56188
  1770
wenzelm@53408
  1771
lemma has_integralD[dest]:
immler@56188
  1772
  assumes "(f has_integral y) (cbox a b)"
wenzelm@53408
  1773
    and "e > 0"
wenzelm@53408
  1774
  obtains d where "gauge d"
immler@56188
  1775
    and "\<And>p. p tagged_division_of (cbox a b) \<Longrightarrow> d fine p \<Longrightarrow>
wenzelm@53408
  1776
      norm (setsum (\<lambda>(x,k). content(k) *\<^sub>R f(x)) p - y) < e"
himmelma@35172
  1777
  using assms unfolding has_integral by auto
himmelma@35172
  1778
himmelma@35172
  1779
lemma has_integral_alt:
wenzelm@53408
  1780
  "(f has_integral y) i \<longleftrightarrow>
immler@56188
  1781
    (if \<exists>a b. i = cbox a b
wenzelm@53408
  1782
     then (f has_integral y) i
immler@56188
  1783
     else (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
immler@56188
  1784
      (\<exists>z. ((\<lambda>x. if x \<in> i then f(x) else 0) has_integral z) (cbox a b) \<and> norm (z - y) < e)))"
wenzelm@53408
  1785
  unfolding has_integral
wenzelm@53408
  1786
  unfolding has_integral_compact_interval_def has_integral_def
wenzelm@53408
  1787
  by auto
himmelma@35172
  1788
himmelma@35172
  1789
lemma has_integral_altD:
wenzelm@53408
  1790
  assumes "(f has_integral y) i"
immler@56188
  1791
    and "\<not> (\<exists>a b. i = cbox a b)"
wenzelm@53408
  1792
    and "e>0"
wenzelm@53408
  1793
  obtains B where "B > 0"
immler@56188
  1794
    and "\<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
immler@56188
  1795
      (\<exists>z. ((\<lambda>x. if x \<in> i then f(x) else 0) has_integral z) (cbox a b) \<and> norm(z - y) < e)"
wenzelm@53408
  1796
  using assms
wenzelm@53408
  1797
  unfolding has_integral
wenzelm@53408
  1798
  unfolding has_integral_compact_interval_def has_integral_def
wenzelm@53408
  1799
  by auto
wenzelm@53408
  1800
wenzelm@53408
  1801
definition integrable_on (infixr "integrable'_on" 46)
wenzelm@53408
  1802
  where "f integrable_on i \<longleftrightarrow> (\<exists>y. (f has_integral y) i)"
wenzelm@53408
  1803
wenzelm@53408
  1804
definition "integral i f = (SOME y. (f has_integral y) i)"
himmelma@35172
  1805
wenzelm@53409
  1806
lemma integrable_integral[dest]: "f integrable_on i \<Longrightarrow> (f has_integral (integral i f)) i"
wenzelm@53409
  1807
  unfolding integrable_on_def integral_def by (rule someI_ex)
himmelma@35172
  1808
himmelma@35172
  1809
lemma has_integral_integrable[intro]: "(f has_integral i) s \<Longrightarrow> f integrable_on s"
himmelma@35172
  1810
  unfolding integrable_on_def by auto
himmelma@35172
  1811
wenzelm@53409
  1812
lemma has_integral_integral: "f integrable_on s \<longleftrightarrow> (f has_integral (integral s f)) s"
himmelma@35172
  1813
  by auto
himmelma@35172
  1814
himmelma@35172
  1815
lemma setsum_content_null:
immler@56188
  1816
  assumes "content (cbox a b) = 0"
immler@56188
  1817
    and "p tagged_division_of (cbox a b)"
himmelma@35172
  1818
  shows "setsum (\<lambda>(x,k). content k *\<^sub>R f x) p = (0::'a::real_normed_vector)"
haftmann@57418
  1819
proof (rule setsum.neutral, rule)
wenzelm@53409
  1820
  fix y
wenzelm@53409
  1821
  assume y: "y \<in> p"
wenzelm@53409
  1822
  obtain x k where xk: "y = (x, k)"
wenzelm@53409
  1823
    using surj_pair[of y] by blast
himmelma@35172
  1824
  note assm = tagged_division_ofD(3-4)[OF assms(2) y[unfolded xk]]
immler@56188
  1825
  from this(2) obtain c d where k: "k = cbox c d" by blast
wenzelm@53409
  1826
  have "(\<lambda>(x, k). content k *\<^sub>R f x) y = content k *\<^sub>R f x"
wenzelm@53409
  1827
    unfolding xk by auto
wenzelm@53409
  1828
  also have "\<dots> = 0"
wenzelm@53409
  1829
    using content_subset[OF assm(1)[unfolded k]] content_pos_le[of c d]
wenzelm@53409
  1830
    unfolding assms(1) k
wenzelm@53409
  1831
    by auto
himmelma@35172
  1832
  finally show "(\<lambda>(x, k). content k *\<^sub>R f x) y = 0" .
himmelma@35172
  1833
qed
himmelma@35172
  1834
wenzelm@53409
  1835
wenzelm@60420
  1836
subsection \<open>Some basic combining lemmas.\<close>
himmelma@35172
  1837
himmelma@35172
  1838
lemma tagged_division_unions_exists:
wenzelm@53409
  1839
  assumes "finite iset"
wenzelm@53409
  1840
    and "\<forall>i\<in>iset. \<exists>p. p tagged_division_of i \<and> d fine p"
wenzelm@53409
  1841
    and "\<forall>i1\<in>iset. \<forall>i2\<in>iset. i1 \<noteq> i2 \<longrightarrow> interior i1 \<inter> interior i2 = {}"
wenzelm@53409
  1842
    and "\<Union>iset = i"
wenzelm@53409
  1843
   obtains p where "p tagged_division_of i" and "d fine p"
wenzelm@53409
  1844
proof -
wenzelm@53409
  1845
  obtain pfn where pfn:
wenzelm@53409
  1846
    "\<And>x. x \<in> iset \<Longrightarrow> pfn x tagged_division_of x"
wenzelm@53409
  1847
    "\<And>x. x \<in> iset \<Longrightarrow> d fine pfn x"
wenzelm@53409
  1848
    using bchoice[OF assms(2)] by auto
wenzelm@53409
  1849
  show thesis
wenzelm@53409
  1850
    apply (rule_tac p="\<Union>(pfn ` iset)" in that)
lp15@60384
  1851
    using assms(1) assms(3) assms(4) pfn(1) tagged_division_unions apply force
lp15@60384
  1852
    by (metis (mono_tags, lifting) fine_unions imageE pfn(2))
himmelma@35172
  1853
qed
himmelma@35172
  1854
wenzelm@53409
  1855
wenzelm@60420
  1856
subsection \<open>The set we're concerned with must be closed.\<close>
himmelma@35172
  1857
wenzelm@53409
  1858
lemma division_of_closed:
immler@56189
  1859
  fixes i :: "'n::euclidean_space set"
wenzelm@53409
  1860
  shows "s division_of i \<Longrightarrow> closed i"
nipkow@44890
  1861
  unfolding division_of_def by fastforce
himmelma@35172
  1862
wenzelm@60420
  1863
subsection \<open>General bisection principle for intervals; might be useful elsewhere.\<close>
himmelma@35172
  1864
wenzelm@53409
  1865
lemma interval_bisection_step:
immler@56188
  1866
  fixes type :: "'a::euclidean_space"
wenzelm@53409
  1867
  assumes "P {}"
wenzelm@53409
  1868
    and "\<forall>s t. P s \<and> P t \<and> interior(s) \<inter> interior(t) = {} \<longrightarrow> P (s \<union> t)"
immler@56188
  1869
    and "\<not> P (cbox a (b::'a))"
immler@56188
  1870
  obtains c d where "\<not> P (cbox c d)"
wenzelm@53409
  1871
    and "\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i"
wenzelm@53409
  1872
proof -
immler@56188
  1873
  have "cbox a b \<noteq> {}"
immler@54776
  1874
    using assms(1,3) by metis
wenzelm@53409
  1875
  then have ab: "\<And>i. i\<in>Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
immler@56188
  1876
    by (force simp: mem_box)
lp15@60428
  1877
  { fix f
lp15@60428
  1878
    have "\<lbrakk>finite f;
lp15@60428
  1879
           \<And>s. s\<in>f \<Longrightarrow> P s;
lp15@60428
  1880
           \<And>s. s\<in>f \<Longrightarrow> \<exists>a b. s = cbox a b;
lp15@60428
  1881
           \<And>s t. s\<in>f \<Longrightarrow> t\<in>f \<Longrightarrow> s \<noteq> t \<Longrightarrow> interior s \<inter> interior t = {}\<rbrakk> \<Longrightarrow> P (\<Union>f)"
wenzelm@53409
  1882
    proof (induct f rule: finite_induct)
wenzelm@53409
  1883
      case empty
wenzelm@53409
  1884
      show ?case
wenzelm@53409
  1885
        using assms(1) by auto
wenzelm@53409
  1886
    next
wenzelm@53409
  1887
      case (insert x f)
wenzelm@53409
  1888
      show ?case
wenzelm@53409
  1889
        unfolding Union_insert
wenzelm@53409
  1890
        apply (rule assms(2)[rule_format])
lp15@60384
  1891
        using inter_interior_unions_intervals [of f "interior x"]
lp15@60384
  1892
        apply (auto simp: insert)
lp15@60428
  1893
        by (metis IntI empty_iff insert.hyps(2) insert.prems(3) insert_iff)
lp15@60428
  1894
    qed
lp15@60428
  1895
  } note UN_cases = this
immler@56188
  1896
  let ?A = "{cbox c d | c d::'a. \<forall>i\<in>Basis. (c\<bullet>i = a\<bullet>i) \<and> (d\<bullet>i = (a\<bullet>i + b\<bullet>i) / 2) \<or>
wenzelm@53409
  1897
    (c\<bullet>i = (a\<bullet>i + b\<bullet>i) / 2) \<and> (d\<bullet>i = b\<bullet>i)}"
hoelzl@50526
  1898
  let ?PP = "\<lambda>c d. \<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i"
wenzelm@53409
  1899
  {
immler@56188
  1900
    presume "\<forall>c d. ?PP c d \<longrightarrow> P (cbox c d) \<Longrightarrow> False"
wenzelm@53409
  1901
    then show thesis
wenzelm@53409
  1902
      unfolding atomize_not not_all
lp15@60384
  1903
      by (blast intro: that)
wenzelm@53409
  1904
  }
immler@56188
  1905
  assume as: "\<forall>c d. ?PP c d \<longrightarrow> P (cbox c d)"
wenzelm@60585
  1906
  have "P (\<Union>?A)"
lp15@60428
  1907
  proof (rule UN_cases)
immler@56188
  1908
    let ?B = "(\<lambda>s. cbox (\<Sum>i\<in>Basis. (if i \<in> s then a\<bullet>i else (a\<bullet>i + b\<bullet>i) / 2) *\<^sub>R i::'a)
immler@56188
  1909
      (\<Sum>i\<in>Basis. (if i \<in> s then (a\<bullet>i + b\<bullet>i) / 2 else b\<bullet>i) *\<^sub>R i)) ` {s. s \<subseteq> Basis}"
wenzelm@53409
  1910
    have "?A \<subseteq> ?B"
wenzelm@53409
  1911
    proof
wenzelm@61165
  1912
      fix x
wenzelm@61165
  1913
      assume "x \<in> ?A"
lp15@60615
  1914
      then obtain c d
lp15@60428
  1915
        where x:  "x = cbox c d"
lp15@60428
  1916
                  "\<And>i. i \<in> Basis \<Longrightarrow>
lp15@60428
  1917
                        c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
lp15@60428
  1918
                        c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i" by blast
wenzelm@53409
  1919
      show "x \<in> ?B"
lp15@60428
  1920
        unfolding image_iff x
wenzelm@53409
  1921
        apply (rule_tac x="{i. i\<in>Basis \<and> c\<bullet>i = a\<bullet>i}" in bexI)
lp15@60428
  1922
        apply (rule arg_cong2 [where f = cbox])
lp15@60428
  1923
        using x(2) ab
lp15@60428
  1924
        apply (auto simp add: euclidean_eq_iff[where 'a='a])
lp15@60428
  1925
        by fastforce
wenzelm@53409
  1926
    qed
wenzelm@53409
  1927
    then show "finite ?A"
wenzelm@53409
  1928
      by (rule finite_subset) auto
lp15@60428
  1929
  next
wenzelm@53409
  1930
    fix s
wenzelm@53409
  1931
    assume "s \<in> ?A"
lp15@60428
  1932
    then obtain c d
lp15@60428
  1933
      where s: "s = cbox c d"
lp15@60428
  1934
               "\<And>i. i \<in> Basis \<Longrightarrow>
lp15@60428
  1935
                     c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
lp15@60428
  1936
                     c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i"
wenzelm@53409
  1937
      by blast
wenzelm@53409
  1938
    show "P s"
wenzelm@53409
  1939
      unfolding s
wenzelm@53409
  1940
      apply (rule as[rule_format])
lp15@60394
  1941
      using ab s(2) by force
immler@56188
  1942
    show "\<exists>a b. s = cbox a b"
wenzelm@53409
  1943
      unfolding s by auto
wenzelm@53409
  1944
    fix t
wenzelm@53409
  1945
    assume "t \<in> ?A"
wenzelm@53409
  1946
    then obtain e f where t:
immler@56188
  1947
      "t = cbox e f"
wenzelm@53409
  1948
      "\<And>i. i \<in> Basis \<Longrightarrow>
wenzelm@53409
  1949
        e \<bullet> i = a \<bullet> i \<and> f \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
wenzelm@53409
  1950
        e \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> f \<bullet> i = b \<bullet> i"
wenzelm@53409
  1951
      by blast
wenzelm@53409
  1952
    assume "s \<noteq> t"
wenzelm@53409
  1953
    then have "\<not> (c = e \<and> d = f)"
wenzelm@53409
  1954
      unfolding s t by auto
wenzelm@53409
  1955
    then obtain i where "c\<bullet>i \<noteq> e\<bullet>i \<or> d\<bullet>i \<noteq> f\<bullet>i" and i': "i \<in> Basis"
hoelzl@50526
  1956
      unfolding euclidean_eq_iff[where 'a='a] by auto
wenzelm@53409
  1957
    then have i: "c\<bullet>i \<noteq> e\<bullet>i" "d\<bullet>i \<noteq> f\<bullet>i"
lp15@60394
  1958
      using s(2) t(2) apply fastforce
wenzelm@60420
  1959
      using t(2)[OF i'] \<open>c \<bullet> i \<noteq> e \<bullet> i \<or> d \<bullet> i \<noteq> f \<bullet> i\<close> i' s(2) t(2) by fastforce
wenzelm@53409
  1960
    have *: "\<And>s t. (\<And>a. a \<in> s \<Longrightarrow> a \<in> t \<Longrightarrow> False) \<Longrightarrow> s \<inter> t = {}"
wenzelm@53409
  1961
      by auto
wenzelm@53409
  1962
    show "interior s \<inter> interior t = {}"
immler@56188
  1963
      unfolding s t interior_cbox
wenzelm@53409
  1964
    proof (rule *)
wenzelm@53409
  1965
      fix x
immler@54775
  1966
      assume "x \<in> box c d" "x \<in> box e f"
wenzelm@53409
  1967
      then have x: "c\<bullet>i < d\<bullet>i" "e\<bullet>i < f\<bullet>i" "c\<bullet>i < f\<bullet>i" "e\<bullet>i < d\<bullet>i"
immler@56188
  1968
        unfolding mem_box using i'
lp15@60394
  1969
        by force+
lp15@60394
  1970
      show False  using s(2)[OF i']
lp15@60394
  1971
      proof safe
wenzelm@53409
  1972
        assume as: "c \<bullet> i = a \<bullet> i" "d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2"
wenzelm@53409
  1973
        show False
wenzelm@53409
  1974
          using t(2)[OF i'] and i x unfolding as by (fastforce simp add:field_simps)
wenzelm@53409
  1975
      next
wenzelm@53409
  1976
        assume as: "c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2" "d \<bullet> i = b \<bullet> i"
wenzelm@53409
  1977
        show False
wenzelm@53409
  1978
          using t(2)[OF i'] and i x unfolding as by(fastforce simp add:field_simps)
wenzelm@53409
  1979
      qed
wenzelm@53409
  1980
    qed
wenzelm@53409
  1981
  qed
wenzelm@60585
  1982
  also have "\<Union>?A = cbox a b"
wenzelm@53409
  1983
  proof (rule set_eqI,rule)
wenzelm@53409
  1984
    fix x
wenzelm@53409
  1985
    assume "x \<in> \<Union>?A"
wenzelm@53409
  1986
    then obtain c d where x:
immler@56188
  1987
      "x \<in> cbox c d"
wenzelm@53409
  1988
      "\<And>i. i \<in> Basis \<Longrightarrow>
wenzelm@53409
  1989
        c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
lp15@60615
  1990
        c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i"
lp15@60394
  1991
      by blast
immler@56188
  1992
    show "x\<in>cbox a b"
immler@56188
  1993
      unfolding mem_box
wenzelm@53409
  1994
    proof safe
wenzelm@53409
  1995
      fix i :: 'a
wenzelm@53409
  1996
      assume i: "i \<in> Basis"
wenzelm@53409
  1997
      then show "a \<bullet> i \<le> x \<bullet> i" "x \<bullet> i \<le> b \<bullet> i"
immler@56188
  1998
        using x(2)[OF i] x(1)[unfolded mem_box,THEN bspec, OF i] by auto
wenzelm@53409
  1999
    qed
wenzelm@53409
  2000
  next
wenzelm@53409
  2001
    fix x
immler@56188
  2002
    assume x: "x \<in> cbox a b"
wenzelm@53409
  2003
    have "\<forall>i\<in>Basis.
wenzelm@53409
  2004
      \<exists>c d. (c = a\<bullet>i \<and> d = (a\<bullet>i + b\<bullet>i) / 2 \<or> c = (a\<bullet>i + b\<bullet>i) / 2 \<and> d = b\<bullet>i) \<and> c\<le>x\<bullet>i \<and> x\<bullet>i \<le> d"
wenzelm@53409
  2005
      (is "\<forall>i\<in>Basis. \<exists>c d. ?P i c d")
immler@56188
  2006
      unfolding mem_box
hoelzl@50526
  2007
    proof
wenzelm@53409
  2008
      fix i :: 'a
wenzelm@53409
  2009
      assume i: "i \<in> Basis"
hoelzl@50526
  2010
      have "?P i (a\<bullet>i) ((a \<bullet> i + b \<bullet> i) / 2) \<or> ?P i ((a \<bullet> i + b \<bullet> i) / 2) (b\<bullet>i)"
immler@56188
  2011
        using x[unfolded mem_box,THEN bspec, OF i] by auto
wenzelm@53409
  2012
      then show "\<exists>c d. ?P i c d"
wenzelm@53409
  2013
        by blast
hoelzl@50526
  2014
    qed
wenzelm@53409
  2015
    then show "x\<in>\<Union>?A"
hoelzl@50526
  2016
      unfolding Union_iff Bex_def mem_Collect_eq choice_Basis_iff
lp15@60384
  2017
      apply auto
immler@56188
  2018
      apply (rule_tac x="cbox xa xaa" in exI)
immler@56188
  2019
      unfolding mem_box
wenzelm@53409
  2020
      apply auto
wenzelm@53409
  2021
      done
wenzelm@53409
  2022
  qed
wenzelm@53409
  2023
  finally show False
wenzelm@53409
  2024
    using assms by auto
wenzelm@53409
  2025
qed
wenzelm@53409
  2026
wenzelm@53409
  2027
lemma interval_bisection:
immler@56188
  2028
  fixes type :: "'a::euclidean_space"
wenzelm@53409
  2029
  assumes "P {}"
wenzelm@53409
  2030
    and "(\<forall>s t. P s \<and> P t \<and> interior(s) \<inter> interior(t) = {} \<longrightarrow> P(s \<union> t))"
immler@56188
  2031
    and "\<not> P (cbox a (b::'a))"
immler@56188
  2032
  obtains x where "x \<in> cbox a b"
immler@56188
  2033
    and "\<forall>e>0. \<exists>c d. x \<in> cbox c d \<and> cbox c d \<subseteq> ball x e \<and> cbox c d \<subseteq> cbox a b \<and> \<not> P (cbox c d)"
immler@56188
  2034
proof -
immler@56188
  2035
  have "\<forall>x. \<exists>y. \<not> P (cbox (fst x) (snd x)) \<longrightarrow> (\<not> P (cbox (fst y) (snd y)) \<and>
hoelzl@50526
  2036
    (\<forall>i\<in>Basis. fst x\<bullet>i \<le> fst y\<bullet>i \<and> fst y\<bullet>i \<le> snd y\<bullet>i \<and> snd y\<bullet>i \<le> snd x\<bullet>i \<and>
wenzelm@61165
  2037
       2 * (snd y\<bullet>i - fst y\<bullet>i) \<le> snd x\<bullet>i - fst x\<bullet>i))" (is "\<forall>x. ?P x")
wenzelm@53409
  2038
  proof
wenzelm@61165
  2039
    show "?P x" for x
wenzelm@61165
  2040
    proof (cases "P (cbox (fst x) (snd x))")
wenzelm@61165
  2041
      case True
wenzelm@61165
  2042
      then show ?thesis by auto
wenzelm@53409
  2043
    next
wenzelm@61165
  2044
      case as: False
immler@56188
  2045
      obtain c d where "\<not> P (cbox c d)"
wenzelm@53409
  2046
        "\<forall>i\<in>Basis.
wenzelm@53409
  2047
           fst x \<bullet> i \<le> c \<bullet> i \<and>
wenzelm@53409
  2048
           c \<bullet> i \<le> d \<bullet> i \<and>
wenzelm@53409
  2049
           d \<bullet> i \<le> snd x \<bullet> i \<and>
wenzelm@53409
  2050
           2 * (d \<bullet> i - c \<bullet> i) \<le> snd x \<bullet> i - fst x \<bullet> i"
wenzelm@53409
  2051
        by (rule interval_bisection_step[of P, OF assms(1-2) as])
wenzelm@53409
  2052
      then show ?thesis
wenzelm@53409
  2053
        apply -
wenzelm@53409
  2054
        apply (rule_tac x="(c,d)" in exI)
wenzelm@53409
  2055
        apply auto
wenzelm@53409
  2056
        done
wenzelm@53409
  2057
    qed
wenzelm@53409
  2058
  qed
wenzelm@55751
  2059
  then obtain f where f:
wenzelm@55751
  2060
    "\<forall>x.
immler@56188
  2061
      \<not> P (cbox (fst x) (snd x)) \<longrightarrow>
immler@56188
  2062
      \<not> P (cbox (fst (f x)) (snd (f x))) \<and>
wenzelm@55751
  2063
        (\<forall>i\<in>Basis.
wenzelm@55751
  2064
            fst x \<bullet> i \<le> fst (f x) \<bullet> i \<and>
wenzelm@55751
  2065
            fst (f x) \<bullet> i \<le> snd (f x) \<bullet> i \<and>
wenzelm@55751
  2066
            snd (f x) \<bullet> i \<le> snd x \<bullet> i \<and>
wenzelm@55751
  2067
            2 * (snd (f x) \<bullet> i - fst (f x) \<bullet> i) \<le> snd x \<bullet> i - fst x \<bullet> i)"
wenzelm@53409
  2068
    apply -
wenzelm@53409
  2069
    apply (drule choice)
wenzelm@55751
  2070
    apply blast
wenzelm@55751
  2071
    done
wenzelm@53409
  2072
  def AB \<equiv> "\<lambda>n. (f ^^ n) (a,b)"
wenzelm@53409
  2073
  def A \<equiv> "\<lambda>n. fst(AB n)"
wenzelm@53409
  2074
  def B \<equiv> "\<lambda>n. snd(AB n)"
wenzelm@53409
  2075
  note ab_def = A_def B_def AB_def
immler@56188
  2076
  have "A 0 = a" "B 0 = b" "\<And>n. \<not> P (cbox (A(Suc n)) (B(Suc n))) \<and>
wenzelm@53399
  2077
    (\<forall>i\<in>Basis. A(n)\<bullet>i \<le> A(Suc n)\<bullet>i \<and> A(Suc n)\<bullet>i \<le> B(Suc n)\<bullet>i \<and> B(Suc n)\<bullet>i \<le> B(n)\<bullet>i \<and>
hoelzl@50526
  2078
    2 * (B(Suc n)\<bullet>i - A(Suc n)\<bullet>i) \<le> B(n)\<bullet>i - A(n)\<bullet>i)" (is "\<And>n. ?P n")
wenzelm@53409
  2079
  proof -
wenzelm@53409
  2080
    show "A 0 = a" "B 0 = b"
wenzelm@53409
  2081
      unfolding ab_def by auto
wenzelm@53409
  2082
    note S = ab_def funpow.simps o_def id_apply
wenzelm@61165
  2083
    show "?P n" for n
wenzelm@53409
  2084
    proof (induct n)
wenzelm@53409
  2085
      case 0
wenzelm@53409
  2086
      then show ?case
wenzelm@53409
  2087
        unfolding S
wenzelm@53409
  2088
        apply (rule f[rule_format]) using assms(3)
wenzelm@53409
  2089
        apply auto
wenzelm@53409
  2090
        done
wenzelm@53409
  2091
    next
wenzelm@53409
  2092
      case (Suc n)
wenzelm@53409
  2093
      show ?case
wenzelm@53409
  2094
        unfolding S
wenzelm@53409
  2095
        apply (rule f[rule_format])
wenzelm@53409
  2096
        using Suc
wenzelm@53409
  2097
        unfolding S
wenzelm@53409
  2098
        apply auto
wenzelm@53409
  2099
        done
wenzelm@53409
  2100
    qed
wenzelm@53409
  2101
  qed
wenzelm@53409
  2102
  note AB = this(1-2) conjunctD2[OF this(3),rule_format]
wenzelm@53409
  2103
wenzelm@61165
  2104
  have interv: "\<exists>n. \<forall>x\<in>cbox (A n) (B n). \<forall>y\<in>cbox (A n) (B n). dist x y < e"
wenzelm@61165
  2105
    if e: "0 < e" for e
wenzelm@53409
  2106
  proof -
wenzelm@53409
  2107
    obtain n where n: "(\<Sum>i\<in>Basis. b \<bullet> i - a \<bullet> i) / e < 2 ^ n"
wenzelm@53409
  2108
      using real_arch_pow2[of "(setsum (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis) / e"] ..
wenzelm@61165
  2109
    show ?thesis
lp15@60396
  2110
    proof (rule exI [where x=n], clarify)
wenzelm@53409
  2111
      fix x y
immler@56188
  2112
      assume xy: "x\<in>cbox (A n) (B n)" "y\<in>cbox (A n) (B n)"
wenzelm@53409
  2113
      have "dist x y \<le> setsum (\<lambda>i. abs((x - y)\<bullet>i)) Basis"
wenzelm@53409
  2114
        unfolding dist_norm by(rule norm_le_l1)
hoelzl@50526
  2115
      also have "\<dots> \<le> setsum (\<lambda>i. B n\<bullet>i - A n\<bullet>i) Basis"
wenzelm@53409
  2116
      proof (rule setsum_mono)
wenzelm@53409
  2117
        fix i :: 'a
wenzelm@53409
  2118
        assume i: "i \<in> Basis"
wenzelm@53409
  2119
        show "\<bar>(x - y) \<bullet> i\<bar> \<le> B n \<bullet> i - A n \<bullet> i"
immler@56188
  2120
          using xy[unfolded mem_box,THEN bspec, OF i]
wenzelm@53409
  2121
          by (auto simp: inner_diff_left)
wenzelm@53409
  2122
      qed
wenzelm@53409
  2123
      also have "\<dots> \<le> setsum (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis / 2^n"
wenzelm@53409
  2124
        unfolding setsum_divide_distrib
wenzelm@53409
  2125
      proof (rule setsum_mono)
wenzelm@61165
  2126
        show "B n \<bullet> i - A n \<bullet> i \<le> (b \<bullet> i - a \<bullet> i) / 2 ^ n" if i: "i \<in> Basis" for i
wenzelm@53409
  2127
        proof (induct n)
wenzelm@53409
  2128
          case 0
wenzelm@53409
  2129
          then show ?case
wenzelm@53409
  2130
            unfolding AB by auto
wenzelm@53409
  2131
        next
wenzelm@53409
  2132
          case (Suc n)
wenzelm@53409
  2133
          have "B (Suc n) \<bullet> i - A (Suc n) \<bullet> i \<le> (B n \<bullet> i - A n \<bullet> i) / 2"
wenzelm@61165
  2134
            using AB(4)[of i n] using i by auto
wenzelm@53409
  2135
          also have "\<dots> \<le> (b \<bullet> i - a \<bullet> i) / 2 ^ Suc n"
wenzelm@61165
  2136
            using Suc by (auto simp add: field_simps)
wenzelm@53409
  2137
          finally show ?case .
wenzelm@53409
  2138
        qed
wenzelm@53409
  2139
      qed
wenzelm@53409
  2140
      also have "\<dots> < e"
wenzelm@61165
  2141
        using n using e by (auto simp add: field_simps)
wenzelm@53409
  2142
      finally show "dist x y < e" .
wenzelm@53409
  2143
    qed
wenzelm@53409
  2144
  qed
wenzelm@53409
  2145
  {
wenzelm@53409
  2146
    fix n m :: nat
immler@56188
  2147
    assume "m \<le> n" then have "cbox (A n) (B n) \<subseteq> cbox (A m) (B m)"
hoelzl@54411
  2148
    proof (induction rule: inc_induct)
wenzelm@53409
  2149
      case (step i)
wenzelm@53409
  2150
      show ?case
immler@56188
  2151
        using AB(4) by (intro order_trans[OF step.IH] subset_box_imp) auto
wenzelm@53409
  2152
    qed simp
wenzelm@53409
  2153
  } note ABsubset = this
immler@56188
  2154
  have "\<exists>a. \<forall>n. a\<in> cbox (A n) (B n)"
immler@56188
  2155
    by (rule decreasing_closed_nest[rule_format,OF closed_cbox _ ABsubset interv])
immler@54776
  2156
      (metis nat.exhaust AB(1-3) assms(1,3))
immler@56188
  2157
  then obtain x0 where x0: "\<And>n. x0 \<in> cbox (A n) (B n)"
wenzelm@53409
  2158
    by blast
wenzelm@53409
  2159
  show thesis
wenzelm@53409
  2160
  proof (rule that[rule_format, of x0])
immler@56188
  2161
    show "x0\<in>cbox a b"
wenzelm@53409
  2162
      using x0[of 0] unfolding AB .
wenzelm@53409
  2163
    fix e :: real
wenzelm@53409
  2164
    assume "e > 0"
wenzelm@53409
  2165
    from interv[OF this] obtain n
immler@56188
  2166
      where n: "\<forall>x\<in>cbox (A n) (B n). \<forall>y\<in>cbox (A n) (B n). dist x y < e" ..
lp15@60396
  2167
    have "\<not> P (cbox (A n) (B n))"
lp15@60396
  2168
      apply (cases "0 < n")
lp15@60396
  2169
      using AB(3)[of "n - 1"] assms(3) AB(1-2)
lp15@60396
  2170
      apply auto
lp15@60396
  2171
      done
lp15@60396
  2172
    moreover have "cbox (A n) (B n) \<subseteq> ball x0 e"
lp15@60396
  2173
      using n using x0[of n] by auto
lp15@60396
  2174
    moreover have "cbox (A n) (B n) \<subseteq> cbox a b"
lp15@60396
  2175
      unfolding AB(1-2)[symmetric] by (rule ABsubset) auto
lp15@60396
  2176
    ultimately show "\<exists>c d. x0 \<in> cbox c d \<and> cbox c d \<subseteq> ball x0 e \<and> cbox c d \<subseteq> cbox a b \<and> \<not> P (cbox c d)"
wenzelm@53409
  2177
      apply (rule_tac x="A n" in exI)
wenzelm@53409
  2178
      apply (rule_tac x="B n" in exI)
lp15@60396
  2179
      apply (auto simp: x0)
lp15@60396
  2180
      done
wenzelm@53409
  2181
  qed
wenzelm@53409
  2182
qed
wenzelm@53409
  2183
himmelma@35172
  2184
wenzelm@60420
  2185
subsection \<open>Cousin's lemma.\<close>
himmelma@35172
  2186
wenzelm@53409
  2187
lemma fine_division_exists:
immler@56188
  2188
  fixes a b :: "'a::euclidean_space"
wenzelm@53409
  2189
  assumes "gauge g"
immler@56188
  2190
  obtains p where "p tagged_division_of (cbox a b)" "g fine p"
immler@56188
  2191
proof -
immler@56188
  2192
  presume "\<not> (\<exists>p. p tagged_division_of (cbox a b) \<and> g fine p) \<Longrightarrow> False"
immler@56188
  2193
  then obtain p where "p tagged_division_of (cbox a b)" "g fine p"
wenzelm@53410
  2194
    by blast
wenzelm@53409
  2195
  then show thesis ..
wenzelm@53409
  2196
next
immler@56188
  2197
  assume as: "\<not> (\<exists>p. p tagged_division_of (cbox a b) \<and> g fine p)"
wenzelm@55751
  2198
  obtain x where x:
lp15@60428
  2199
      "x \<in> (cbox a b)"
lp15@60428
  2200
      "\<And>e. 0 < e \<Longrightarrow>
lp15@60428
  2201
        \<exists>c d.
lp15@60428
  2202
          x \<in> cbox c d \<and>
lp15@60428
  2203
          cbox c d \<subseteq> ball x e \<and>
lp15@60428
  2204
          cbox c d \<subseteq> (cbox a b) \<and>
lp15@60428
  2205
          \<not> (\<exists>p. p tagged_division_of cbox c d \<and> g fine p)"
lp15@60428
  2206
    apply (rule interval_bisection[of "\<lambda>s. \<exists>p. p tagged_division_of s \<and> g fine p", OF _ _ as])
lp15@60428
  2207
    apply (simp add: fine_def)
lp15@60428
  2208
    apply (metis tagged_division_union fine_union)
lp15@60428
  2209
    apply (auto simp: )
lp15@60428
  2210
    done
wenzelm@53410
  2211
  obtain e where e: "e > 0" "ball x e \<subseteq> g x"
wenzelm@53409
  2212
    using gaugeD[OF assms, of x] unfolding open_contains_ball by auto
lp15@60615
  2213
  from x(2)[OF e(1)]
lp15@60396
  2214
  obtain c d where c_d: "x \<in> cbox c d"
lp15@60396
  2215
                        "cbox c d \<subseteq> ball x e"
lp15@60396
  2216
                        "cbox c d \<subseteq> cbox a b"
lp15@60396
  2217
                        "\<not> (\<exists>p. p tagged_division_of cbox c d \<and> g fine p)"
wenzelm@53410
  2218
    by blast
immler@56188
  2219
  have "g fine {(x, cbox c d)}"
wenzelm@53409
  2220
    unfolding fine_def using e using c_d(2) by auto
wenzelm@53410
  2221
  then show False
wenzelm@53410
  2222
    using tagged_division_of_self[OF c_d(1)] using c_d by auto
wenzelm@53409
  2223
qed
wenzelm@53409
  2224
immler@56188
  2225
lemma fine_division_exists_real:
immler@56188
  2226
  fixes a b :: real
immler@56188
  2227
  assumes "gauge g"
immler@56188
  2228
  obtains p where "p tagged_division_of {a .. b}" "g fine p"
immler@56188
  2229
  by (metis assms box_real(2) fine_division_exists)
himmelma@35172
  2230
wenzelm@60420
  2231
subsection \<open>Basic theorems about integrals.\<close>
himmelma@35172
  2232
wenzelm@53409
  2233
lemma has_integral_unique:
immler@56188
  2234
  fixes f :: "'n::euclidean_space \<Rightarrow> 'a::real_normed_vector"
wenzelm@53410
  2235
  assumes "(f has_integral k1) i"
wenzelm@53410
  2236
    and "(f has_integral k2) i"
wenzelm@53409
  2237
  shows "k1 = k2"
wenzelm@53410
  2238
proof (rule ccontr)
wenzelm@53842
  2239
  let ?e = "norm (k1 - k2) / 2"
wenzelm@61165
  2240
  assume as: "k1 \<noteq> k2"
wenzelm@53410
  2241
  then have e: "?e > 0"
wenzelm@53410
  2242
    by auto
wenzelm@61165
  2243
  have lem: False
wenzelm@61165
  2244
    if f_k1: "(f has_integral k1) (cbox a b)"
wenzelm@61165
  2245
    and f_k2: "(f has_integral k2) (cbox a b)"
wenzelm@61165
  2246
    and "k1 \<noteq> k2"
wenzelm@61165
  2247
    for f :: "'n \<Rightarrow> 'a" and a b k1 k2
wenzelm@53410
  2248
  proof -
wenzelm@53410
  2249
    let ?e = "norm (k1 - k2) / 2"
wenzelm@61165
  2250
    from \<open>k1 \<noteq> k2\<close> have e: "?e > 0" by auto
wenzelm@55751
  2251
    obtain d1 where d1:
wenzelm@55751
  2252
        "gauge d1"
immler@56188
  2253
        "\<And>p. p tagged_division_of cbox a b \<Longrightarrow>
wenzelm@55751
  2254
          d1 fine p \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k1) < norm (k1 - k2) / 2"
wenzelm@61165
  2255
      by (rule has_integralD[OF f_k1 e]) blast
wenzelm@55751
  2256
    obtain d2 where d2:
wenzelm@55751
  2257
        "gauge d2"
immler@56188
  2258
        "\<And>p. p tagged_division_of cbox a b \<Longrightarrow>
wenzelm@55751
  2259
          d2 fine p \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k2) < norm (k1 - k2) / 2"
wenzelm@61165
  2260
      by (rule has_integralD[OF f_k2 e]) blast
wenzelm@55751
  2261
    obtain p where p:
immler@56188
  2262
        "p tagged_division_of cbox a b"
wenzelm@55751
  2263
        "(\<lambda>x. d1 x \<inter> d2 x) fine p"
wenzelm@55751
  2264
      by (rule fine_division_exists[OF gauge_inter[OF d1(1) d2(1)]])
wenzelm@53410
  2265
    let ?c = "(\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)"
wenzelm@53410
  2266
    have "norm (k1 - k2) \<le> norm (?c - k2) + norm (?c - k1)"
wenzelm@53410
  2267
      using norm_triangle_ineq4[of "k1 - ?c" "k2 - ?c"]
wenzelm@53410
  2268
      by (auto simp add:algebra_simps norm_minus_commute)
himmelma@35172
  2269
    also have "\<dots> < norm (k1 - k2) / 2 + norm (k1 - k2) / 2"
wenzelm@53410
  2270
      apply (rule add_strict_mono)
wenzelm@53410
  2271
      apply (rule_tac[!] d2(2) d1(2))
wenzelm@53410
  2272
      using p unfolding fine_def
wenzelm@53410
  2273
      apply auto
wenzelm@53410
  2274
      done
himmelma@35172
  2275
    finally show False by auto
wenzelm@53410
  2276
  qed
wenzelm@53410
  2277
  {
immler@56188
  2278
    presume "\<not> (\<exists>a b. i = cbox a b) \<Longrightarrow> False"
wenzelm@53410
  2279
    then show False
lp15@60396
  2280
      using as assms lem by blast
wenzelm@53410
  2281
  }
immler@56188
  2282
  assume as: "\<not> (\<exists>a b. i = cbox a b)"
wenzelm@55751
  2283
  obtain B1 where B1:
wenzelm@55751
  2284
      "0 < B1"
immler@56188
  2285
      "\<And>a b. ball 0 B1 \<subseteq> cbox a b \<Longrightarrow>
immler@56188
  2286
        \<exists>z. ((\<lambda>x. if x \<in> i then f x else 0) has_integral z) (cbox a b) \<and>
wenzelm@55751
  2287
          norm (z - k1) < norm (k1 - k2) / 2"
wenzelm@55751
  2288
    by (rule has_integral_altD[OF assms(1) as,OF e]) blast
wenzelm@55751
  2289
  obtain B2 where B2:
wenzelm@55751
  2290
      "0 < B2"
immler@56188
  2291
      "\<And>a b. ball 0 B2 \<subseteq> cbox a b \<Longrightarrow>
immler@56188
  2292
        \<exists>z. ((\<lambda>x. if x \<in> i then f x else 0) has_integral z) (cbox a b) \<and>
wenzelm@55751
  2293
          norm (z - k2) < norm (k1 - k2) / 2"
wenzelm@55751
  2294
    by (rule has_integral_altD[OF assms(2) as,OF e]) blast
immler@56188
  2295
  have "\<exists>a b::'n. ball 0 B1 \<union> ball 0 B2 \<subseteq> cbox a b"
immler@56188
  2296
    apply (rule bounded_subset_cbox)
wenzelm@53410
  2297
    using bounded_Un bounded_ball
wenzelm@53410
  2298
    apply auto
wenzelm@53410
  2299
    done
immler@56188
  2300
  then obtain a b :: 'n where ab: "ball 0 B1 \<subseteq> cbox a b" "ball 0 B2 \<subseteq> cbox a b"
wenzelm@53410
  2301
    by blast
wenzelm@53410
  2302
  obtain w where w:
immler@56188
  2303
    "((\<lambda>x. if x \<in> i then f x else 0) has_integral w) (cbox a b)"
wenzelm@53410
  2304
    "norm (w - k1) < norm (k1 - k2) / 2"
wenzelm@53410
  2305
    using B1(2)[OF ab(1)] by blast
wenzelm@53410
  2306
  obtain z where z:
immler@56188
  2307
    "((\<lambda>x. if x \<in> i then f x else 0) has_integral z) (cbox a b)"
wenzelm@53410
  2308
    "norm (z - k2) < norm (k1 - k2) / 2"
wenzelm@53410
  2309
    using B2(2)[OF ab(2)] by blast
wenzelm@53410
  2310
  have "z = w"
wenzelm@53410
  2311
    using lem[OF w(1) z(1)] by auto
wenzelm@53410
  2312
  then have "norm (k1 - k2) \<le> norm (z - k2) + norm (w - k1)"
wenzelm@53410
  2313
    using norm_triangle_ineq4 [of "k1 - w" "k2 - z"]
wenzelm@53410
  2314
    by (auto simp add: norm_minus_commute)
wenzelm@53410
  2315
  also have "\<dots> < norm (k1 - k2) / 2 + norm (k1 - k2) / 2"
wenzelm@53410
  2316
    apply (rule add_strict_mono)
wenzelm@53410
  2317
    apply (rule_tac[!] z(2) w(2))
wenzelm@53410
  2318
    done
wenzelm@53410
  2319
  finally show False by auto
wenzelm@53410
  2320
qed
wenzelm@53410
  2321
wenzelm@53410
  2322
lemma integral_unique [intro]: "(f has_integral y) k \<Longrightarrow> integral k f = y"
wenzelm@53410
  2323
  unfolding integral_def
wenzelm@53410
  2324
  by (rule some_equality) (auto intro: has_integral_unique)
wenzelm@53410
  2325
wenzelm@53410
  2326
lemma has_integral_is_0:
immler@56188
  2327
  fixes f :: "'n::euclidean_space \<Rightarrow> 'a::real_normed_vector"
wenzelm@53410
  2328
  assumes "\<forall>x\<in>s. f x = 0"
wenzelm@53410
  2329
  shows "(f has_integral 0) s"
wenzelm@53410
  2330
proof -
wenzelm@53410
  2331
  have lem: "\<And>a b. \<And>f::'n \<Rightarrow> 'a.
immler@56188
  2332
    (\<forall>x\<in>cbox a b. f(x) = 0) \<Longrightarrow> (f has_integral 0) (cbox a b)"
wenzelm@53410
  2333
    unfolding has_integral
lp15@60396
  2334
  proof clarify
wenzelm@53410
  2335
    fix a b e
wenzelm@53410
  2336
    fix f :: "'n \<Rightarrow> 'a"
immler@56188
  2337
    assume as: "\<forall>x\<in>cbox a b. f x = 0" "0 < (e::real)"
wenzelm@61165
  2338
    have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) < e"
wenzelm@61165
  2339
      if p: "p tagged_division_of cbox a b" for p
wenzelm@53410
  2340
    proof -
wenzelm@53410
  2341
      have "(\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) = 0"
haftmann@57418
  2342
      proof (rule setsum.neutral, rule)
wenzelm@53410
  2343
        fix x
wenzelm@53410
  2344
        assume x: "x \<in> p"
wenzelm@53410
  2345
        have "f (fst x) = 0"
wenzelm@61165
  2346
          using tagged_division_ofD(2-3)[OF p, of "fst x" "snd x"] using as x by auto
wenzelm@53410
  2347
        then show "(\<lambda>(x, k). content k *\<^sub>R f x) x = 0"
wenzelm@53410
  2348
          apply (subst surjective_pairing[of x])
wenzelm@53410
  2349
          unfolding split_conv
wenzelm@53410
  2350
          apply auto
wenzelm@53410
  2351
          done
wenzelm@53410
  2352
      qed
wenzelm@61165
  2353
      then show ?thesis
wenzelm@53410
  2354
        using as by auto
lp15@60396
  2355
    qed
lp15@60396
  2356
    then show "\<exists>d. gauge d \<and>
wenzelm@61165
  2357
        (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) < e)"
lp15@60396
  2358
      by auto
wenzelm@53410
  2359
  qed
wenzelm@53410
  2360
  {
immler@56188
  2361
    presume "\<not> (\<exists>a b. s = cbox a b) \<Longrightarrow> ?thesis"
lp15@60396
  2362
    with assms lem show ?thesis
lp15@60396
  2363
      by blast
wenzelm@53410
  2364
  }
wenzelm@53410
  2365
  have *: "(\<lambda>x. if x \<in> s then f x else 0) = (\<lambda>x. 0)"
wenzelm@53410
  2366
    apply (rule ext)
wenzelm@53410
  2367
    using assms
wenzelm@53410
  2368
    apply auto
wenzelm@53410
  2369
    done
immler@56188
  2370
  assume "\<not> (\<exists>a b. s = cbox a b)"
wenzelm@53410
  2371
  then show ?thesis
lp15@60396
  2372
    using lem
lp15@60396
  2373
    by (subst has_integral_alt) (force simp add: *)
wenzelm@53410
  2374
qed
himmelma@35172
  2375
immler@56188
  2376
lemma has_integral_0[simp]: "((\<lambda>x::'n::euclidean_space. 0) has_integral 0) s"
wenzelm@53410
  2377
  by (rule has_integral_is_0) auto
himmelma@35172
  2378
himmelma@35172
  2379
lemma has_integral_0_eq[simp]: "((\<lambda>x. 0) has_integral i) s \<longleftrightarrow> i = 0"
himmelma@35172
  2380
  using has_integral_unique[OF has_integral_0] by auto
himmelma@35172
  2381
wenzelm@53410
  2382
lemma has_integral_linear:
immler@56188
  2383
  fixes f :: "'n::euclidean_space \<Rightarrow> 'a::real_normed_vector"
wenzelm@53410
  2384
  assumes "(f has_integral y) s"
wenzelm@53410
  2385
    and "bounded_linear h"
wenzelm@53410
  2386
  shows "((h o f) has_integral ((h y))) s"
wenzelm@53410
  2387
proof -
wenzelm@53410
  2388
  interpret bounded_linear h
wenzelm@53410
  2389
    using assms(2) .
wenzelm@53410
  2390
  from pos_bounded obtain B where B: "0 < B" "\<And>x. norm (h x) \<le> norm x * B"
wenzelm@53410
  2391
    by blast
wenzelm@53410
  2392
  have lem: "\<And>(f :: 'n \<Rightarrow> 'a) y a b.
immler@56188
  2393
    (f has_integral y) (cbox a b) \<Longrightarrow> ((h o f) has_integral h y) (cbox a b)"
wenzelm@61165
  2394
    unfolding has_integral
wenzelm@61166
  2395
  proof (clarify, goal_cases)
wenzelm@61167
  2396
    case prems: (1 f y a b e)
wenzelm@53410
  2397
    from pos_bounded
wenzelm@53410
  2398
    obtain B where B: "0 < B" "\<And>x. norm (h x) \<le> norm x * B"
wenzelm@53410
  2399
      by blast
wenzelm@61167
  2400
    have "e / B > 0" using prems(2) B by simp
lp15@60615
  2401
    then obtain g
lp15@60428
  2402
      where g: "gauge g"
lp15@60428
  2403
               "\<And>p. p tagged_division_of (cbox a b) \<Longrightarrow> g fine p \<Longrightarrow>
lp15@60428
  2404
                    norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - y) < e / B"
wenzelm@61167
  2405
        using prems(1) by auto
wenzelm@61165
  2406
    {
wenzelm@61165
  2407
      fix p
immler@56188
  2408
      assume as: "p tagged_division_of (cbox a b)" "g fine p"
lp15@60428
  2409
      have hc: "\<And>x k. h ((\<lambda>(x, k). content k *\<^sub>R f x) x) = (\<lambda>(x, k). h (content k *\<^sub>R f x)) x"
wenzelm@53410
  2410
        by auto
lp15@60428
  2411
      then have "(\<Sum>(x, k)\<in>p. content k *\<^sub>R (h \<circ> f) x) = setsum (h \<circ> (\<lambda>(x, k). content k *\<^sub>R f x)) p"
lp15@60428
  2412
        unfolding o_def unfolding scaleR[symmetric] hc by simp
wenzelm@53410
  2413
      also have "\<dots> = h (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)"
wenzelm@53410
  2414
        using setsum[of "\<lambda>(x,k). content k *\<^sub>R f x" p] using as by auto
lp15@60428
  2415
      finally have "(\<Sum>(x, k)\<in>p. content k *\<^sub>R (h \<circ> f) x) = h (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)" .
lp15@60428
  2416
      then have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (h \<circ> f) x) - h y) < e"
lp15@60428
  2417
        apply (simp add: diff[symmetric])
wenzelm@53410
  2418
        apply (rule le_less_trans[OF B(2)])
wenzelm@53410
  2419
        using g(2)[OF as] B(1)
wenzelm@53410
  2420
        apply (auto simp add: field_simps)
wenzelm@53410
  2421
        done
lp15@60428
  2422
    }
lp15@60428
  2423
    with g show ?case
lp15@60428
  2424
      by (rule_tac x=g in exI) auto
wenzelm@53410
  2425
  qed
wenzelm@53410
  2426
  {
immler@56188
  2427
    presume "\<not> (\<exists>a b. s = cbox a b) \<Longrightarrow> ?thesis"
wenzelm@53410
  2428
    then show ?thesis
lp15@60396
  2429
      using assms(1) lem by blast
wenzelm@53410
  2430
  }
immler@56188
  2431
  assume as: "\<not> (\<exists>a b. s = cbox a b)"
wenzelm@53410
  2432
  then show ?thesis
lp15@60396
  2433
  proof (subst has_integral_alt, clarsimp)
wenzelm@53410
  2434
    fix e :: real
wenzelm@53410
  2435
    assume e: "e > 0"
nipkow@56541
  2436
    have *: "0 < e/B" using e B(1) by simp
wenzelm@53410
  2437
    obtain M where M:
wenzelm@53410
  2438
      "M > 0"
immler@56188
  2439
      "\<And>a b. ball 0 M \<subseteq> cbox a b \<Longrightarrow>
immler@56188
  2440
        \<exists>z. ((\<lambda>x. if x \<in> s then f x else 0) has_integral z) (cbox a b) \<and> norm (z - y) < e / B"
wenzelm@53410
  2441
      using has_integral_altD[OF assms(1) as *] by blast
immler@56188
  2442
    show "\<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
immler@56188
  2443
      (\<exists>z. ((\<lambda>x. if x \<in> s then (h \<circ> f) x else 0) has_integral z) (cbox a b) \<and> norm (z - h y) < e)"
wenzelm@61166
  2444
    proof (rule_tac x=M in exI, clarsimp simp add: M, goal_cases)
wenzelm@61167
  2445
      case prems: (1 a b)
wenzelm@53410
  2446
      obtain z where z:
immler@56188
  2447
        "((\<lambda>x. if x \<in> s then f x else 0) has_integral z) (cbox a b)"
wenzelm@53410
  2448
        "norm (z - y) < e / B"
wenzelm@61167
  2449
        using M(2)[OF prems(1)] by blast
wenzelm@53410
  2450
      have *: "(\<lambda>x. if x \<in> s then (h \<circ> f) x else 0) = h \<circ> (\<lambda>x. if x \<in> s then f x else 0)"
lp15@60396
  2451
        using zero by auto
wenzelm@53410
  2452
      show ?case
wenzelm@53410
  2453
        apply (rule_tac x="h z" in exI)
wenzelm@61165
  2454
        apply (simp add: * lem z(1))
wenzelm@61165
  2455
        apply (metis B diff le_less_trans pos_less_divide_eq z(2))
wenzelm@61165
  2456
        done
wenzelm@53410
  2457
    qed
wenzelm@53410
  2458
  qed
wenzelm@53410
  2459
qed
wenzelm@53410
  2460
lp15@60615
  2461
lemma has_integral_scaleR_left:
hoelzl@57447
  2462
  "(f has_integral y) s \<Longrightarrow> ((\<lambda>x. f x *\<^sub>R c) has_integral (y *\<^sub>R c)) s"
hoelzl@57447
  2463
  using has_integral_linear[OF _ bounded_linear_scaleR_left] by (simp add: comp_def)
hoelzl@57447
  2464
hoelzl@57447
  2465
lemma has_integral_mult_left:
hoelzl@57447
  2466
  fixes c :: "_ :: {real_normed_algebra}"
hoelzl@57447
  2467
  shows "(f has_integral y) s \<Longrightarrow> ((\<lambda>x. f x * c) has_integral (y * c)) s"
hoelzl@57447
  2468
  using has_integral_linear[OF _ bounded_linear_mult_left] by (simp add: comp_def)
hoelzl@57447
  2469
lp15@60615
  2470
corollary integral_mult_left:
lp15@60615
  2471
  fixes c:: "'a::real_normed_algebra"
lp15@60615
  2472
  shows "f integrable_on s \<Longrightarrow> integral s (\<lambda>x. f x * c) = integral s f * c"
lp15@60615
  2473
  by (blast intro:  has_integral_mult_left)
lp15@60615
  2474
paulson@60762
  2475
lemma has_integral_mult_right:
paulson@60762
  2476
  fixes c :: "'a :: real_normed_algebra"
paulson@60762
  2477
  shows "(f has_integral y) i \<Longrightarrow> ((\<lambda>x. c * f x) has_integral (c * y)) i"
paulson@60762
  2478
  using has_integral_linear[OF _ bounded_linear_mult_right] by (simp add: comp_def)
wenzelm@61165
  2479
wenzelm@53410
  2480
lemma has_integral_cmul: "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_integral (c *\<^sub>R k)) s"
wenzelm@53410
  2481
  unfolding o_def[symmetric]
lp15@60396
  2482
  by (metis has_integral_linear bounded_linear_scaleR_right)