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