src/HOL/Multivariate_Analysis/Integration.thy
author hoelzl
Mon Aug 23 19:35:57 2010 +0200 (2010-08-23)
changeset 38656 d5d342611edb
parent 37665 579258a77fec
child 39302 d7728f65b353
permissions -rw-r--r--
Rewrite the Probability theory.

Introduced pinfreal as real numbers with infinity.
Use pinfreal as value for measures.
Introduces Lebesgue Measure based on the integral in Multivariate Analysis.
Proved Radon Nikodym for arbitrary sigma finite measure spaces.
himmelma@35172
     1
hoelzl@37489
     2
header {* Kurzweil-Henstock Gauge Integration in many dimensions. *}
himmelma@35172
     3
(*  Author:                     John Harrison
himmelma@35172
     4
    Translation from HOL light: Robert Himmelmann, TU Muenchen *)
himmelma@35172
     5
hoelzl@35292
     6
theory Integration
hoelzl@37665
     7
  imports Derivative "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Indicator_Function
himmelma@35172
     8
begin
himmelma@35172
     9
boehmes@36899
    10
declare [[smt_certificates="~~/src/HOL/Multivariate_Analysis/Integration.certs"]]
hoelzl@37489
    11
declare [[smt_fixed=false]]
himmelma@35172
    12
declare [[z3_proofs=true]]
himmelma@35172
    13
boehmes@36899
    14
setup {* Arith_Data.add_tactic "Ferrante-Rackoff" (K FerranteRackoff.dlo_tac) *}
boehmes@36899
    15
hoelzl@37489
    16
(*declare not_less[simp] not_le[simp]*)
hoelzl@37489
    17
hoelzl@37489
    18
lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
hoelzl@37489
    19
  scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff
hoelzl@37489
    20
  scaleR_cancel_left scaleR_cancel_right scaleR.add_right scaleR.add_left real_vector_class.scaleR_one
hoelzl@37489
    21
hoelzl@37489
    22
lemma real_arch_invD:
hoelzl@37489
    23
  "0 < (e::real) \<Longrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
hoelzl@37489
    24
  by(subst(asm) real_arch_inv)
himmelma@36243
    25
subsection {* Sundries *}
himmelma@36243
    26
hoelzl@37489
    27
(*declare basis_component[simp]*)
hoelzl@37489
    28
himmelma@35172
    29
lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
himmelma@35172
    30
lemma conjunctD3: assumes "a \<and> b \<and> c" shows a b c using assms by auto
himmelma@35172
    31
lemma conjunctD4: assumes "a \<and> b \<and> c \<and> d" shows a b c d using assms by auto
himmelma@35172
    32
lemma conjunctD5: assumes "a \<and> b \<and> c \<and> d \<and> e" shows a b c d e using assms by auto
himmelma@35172
    33
hoelzl@37489
    34
declare norm_triangle_ineq4[intro] 
himmelma@35172
    35
himmelma@36243
    36
lemma simple_image: "{f x |x . x \<in> s} = f ` s" by blast
himmelma@36243
    37
himmelma@36243
    38
lemma linear_simps:  assumes "bounded_linear f"
himmelma@36243
    39
  shows "f (a + b) = f a + f b" "f (a - b) = f a - f b" "f 0 = 0" "f (- a) = - f a" "f (s *\<^sub>R v) = s *\<^sub>R (f v)"
himmelma@36243
    40
  apply(rule_tac[!] additive.add additive.minus additive.diff additive.zero bounded_linear.scaleR)
himmelma@36243
    41
  using assms unfolding bounded_linear_def additive_def by auto
himmelma@36243
    42
himmelma@36243
    43
lemma bounded_linearI:assumes "\<And>x y. f (x + y) = f x + f y"
himmelma@36243
    44
  "\<And>r x. f (r *\<^sub>R x) = r *\<^sub>R f x" "\<And>x. norm (f x) \<le> norm x * K"
himmelma@36243
    45
  shows "bounded_linear f"
himmelma@36243
    46
  unfolding bounded_linear_def additive_def bounded_linear_axioms_def using assms by auto
himmelma@36243
    47
 
himmelma@36243
    48
lemma real_le_inf_subset:
himmelma@36243
    49
  assumes "t \<noteq> {}" "t \<subseteq> s" "\<exists>b. b <=* s" shows "Inf s <= Inf (t::real set)"
himmelma@36243
    50
  apply(rule isGlb_le_isLb) apply(rule Inf[OF assms(1)])
himmelma@36243
    51
  using assms apply-apply(erule exE) apply(rule_tac x=b in exI)
himmelma@36243
    52
  unfolding isLb_def setge_def by auto
himmelma@36243
    53
himmelma@36243
    54
lemma real_ge_sup_subset:
himmelma@36243
    55
  assumes "t \<noteq> {}" "t \<subseteq> s" "\<exists>b. s *<= b" shows "Sup s >= Sup (t::real set)"
himmelma@36243
    56
  apply(rule isLub_le_isUb) apply(rule Sup[OF assms(1)])
himmelma@36243
    57
  using assms apply-apply(erule exE) apply(rule_tac x=b in exI)
himmelma@36243
    58
  unfolding isUb_def setle_def by auto
himmelma@36243
    59
hoelzl@37489
    60
lemma bounded_linear_component[intro]: "bounded_linear (\<lambda>x::'a::euclidean_space. x $$ k)"
himmelma@36243
    61
  apply(rule bounded_linearI[where K=1]) 
himmelma@36243
    62
  using component_le_norm[of _ k] unfolding real_norm_def by auto
himmelma@36243
    63
himmelma@36243
    64
lemma transitive_stepwise_lt_eq:
himmelma@36243
    65
  assumes "(\<And>x y z::nat. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z)"
himmelma@36243
    66
  shows "((\<forall>m. \<forall>n>m. R m n) \<longleftrightarrow> (\<forall>n. R n (Suc n)))" (is "?l = ?r")
himmelma@36243
    67
proof(safe) assume ?r fix n m::nat assume "m < n" thus "R m n" apply-
himmelma@36243
    68
  proof(induct n arbitrary: m) case (Suc n) show ?case 
himmelma@36243
    69
    proof(cases "m < n") case True
himmelma@36243
    70
      show ?thesis apply(rule assms[OF Suc(1)[OF True]]) using `?r` by auto
himmelma@36243
    71
    next case False hence "m = n" using Suc(2) by auto
himmelma@36243
    72
      thus ?thesis using `?r` by auto
himmelma@36243
    73
    qed qed auto qed auto
himmelma@36243
    74
himmelma@36243
    75
lemma transitive_stepwise_gt:
himmelma@36243
    76
  assumes "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" "\<And>n. R n (Suc n) "
himmelma@36243
    77
  shows "\<forall>n>m. R m n"
himmelma@36243
    78
proof- have "\<forall>m. \<forall>n>m. R m n" apply(subst transitive_stepwise_lt_eq)
himmelma@36243
    79
    apply(rule assms) apply(assumption,assumption) using assms(2) by auto
himmelma@36243
    80
  thus ?thesis by auto qed
himmelma@36243
    81
himmelma@36243
    82
lemma transitive_stepwise_le_eq:
himmelma@36243
    83
  assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
himmelma@36243
    84
  shows "(\<forall>m. \<forall>n\<ge>m. R m n) \<longleftrightarrow> (\<forall>n. R n (Suc n))" (is "?l = ?r")
himmelma@36243
    85
proof safe assume ?r fix m n::nat assume "m\<le>n" thus "R m n" apply-
himmelma@36243
    86
  proof(induct n arbitrary: m) case (Suc n) show ?case 
himmelma@36243
    87
    proof(cases "m \<le> n") case True show ?thesis apply(rule assms(2))
himmelma@36243
    88
        apply(rule Suc(1)[OF True]) using `?r` by auto
himmelma@36243
    89
    next case False hence "m = Suc n" using Suc(2) by auto
himmelma@36243
    90
      thus ?thesis using assms(1) by auto
himmelma@36243
    91
    qed qed(insert assms(1), auto) qed auto
himmelma@36243
    92
himmelma@36243
    93
lemma transitive_stepwise_le:
himmelma@36243
    94
  assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" "\<And>n. R n (Suc n) "
himmelma@36243
    95
  shows "\<forall>n\<ge>m. R m n"
himmelma@36243
    96
proof- have "\<forall>m. \<forall>n\<ge>m. R m n" apply(subst transitive_stepwise_le_eq)
himmelma@36243
    97
    apply(rule assms) apply(rule assms,assumption,assumption) using assms(3) by auto
himmelma@36243
    98
  thus ?thesis by auto qed
himmelma@36243
    99
himmelma@35172
   100
subsection {* Some useful lemmas about intervals. *}
himmelma@35172
   101
hoelzl@37489
   102
abbreviation One  where "One \<equiv> ((\<chi>\<chi> i. 1)::_::ordered_euclidean_space)"
hoelzl@37489
   103
hoelzl@37489
   104
lemma empty_as_interval: "{} = {One..0}"
hoelzl@37489
   105
  apply(rule set_ext,rule) defer unfolding mem_interval
himmelma@35172
   106
  using UNIV_witness[where 'a='n] apply(erule_tac exE,rule_tac x=x in allE) by auto
himmelma@35172
   107
himmelma@35172
   108
lemma interior_subset_union_intervals: 
hoelzl@37489
   109
  assumes "i = {a..b::'a::ordered_euclidean_space}" "j = {c..d}" "interior j \<noteq> {}" "i \<subseteq> j \<union> s" "interior(i) \<inter> interior(j) = {}"
himmelma@35172
   110
  shows "interior i \<subseteq> interior s" proof-
himmelma@35172
   111
  have "{a<..<b} \<inter> {c..d} = {}" using inter_interval_mixed_eq_empty[of c d a b] and assms(3,5)
himmelma@35172
   112
    unfolding assms(1,2) interior_closed_interval by auto
himmelma@35172
   113
  moreover have "{a<..<b} \<subseteq> {c..d} \<union> s" apply(rule order_trans,rule interval_open_subset_closed)
himmelma@35172
   114
    using assms(4) unfolding assms(1,2) by auto
himmelma@35172
   115
  ultimately show ?thesis apply-apply(rule interior_maximal) defer apply(rule open_interior)
himmelma@35172
   116
    unfolding assms(1,2) interior_closed_interval by auto qed
himmelma@35172
   117
hoelzl@37489
   118
lemma inter_interior_unions_intervals: fixes f::"('a::ordered_euclidean_space) set set"
himmelma@35172
   119
  assumes "finite f" "open s" "\<forall>t\<in>f. \<exists>a b. t = {a..b}" "\<forall>t\<in>f. s \<inter> (interior t) = {}"
himmelma@35172
   120
  shows "s \<inter> interior(\<Union>f) = {}" proof(rule ccontr,unfold ex_in_conv[THEN sym]) case goal1
himmelma@35172
   121
  have lem1:"\<And>x e s U. ball x e \<subseteq> s \<inter> interior U \<longleftrightarrow> ball x e \<subseteq> s \<inter> U" apply rule  defer apply(rule_tac Int_greatest)
himmelma@35172
   122
    unfolding open_subset_interior[OF open_ball]  using interior_subset by auto
himmelma@35172
   123
  have lem2:"\<And>x s P. \<exists>x\<in>s. P x \<Longrightarrow> \<exists>x\<in>insert x s. P x" by auto
himmelma@35172
   124
  have "\<And>f. finite f \<Longrightarrow> (\<forall>t\<in>f. \<exists>a b. t = {a..b}) \<Longrightarrow> (\<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)" proof- case goal1
himmelma@35172
   125
  thus ?case proof(induct rule:finite_induct) 
himmelma@35172
   126
    case empty from this(2) guess x .. hence False unfolding Union_empty interior_empty by auto thus ?case by auto next
himmelma@35172
   127
    case (insert i f) guess x using insert(5) .. note x = this
himmelma@35172
   128
    then guess e unfolding open_contains_ball_eq[OF open_Int[OF assms(2) open_interior],rule_format] .. note e=this
himmelma@35172
   129
    guess a using insert(4)[rule_format,OF insertI1] .. then guess b .. note ab = this
himmelma@35172
   130
    show ?case proof(cases "x\<in>i") case False hence "x \<in> UNIV - {a..b}" unfolding ab by auto
himmelma@35172
   131
      then guess d unfolding open_contains_ball_eq[OF open_Diff[OF open_UNIV closed_interval],rule_format] ..
hoelzl@37489
   132
      hence "0 < d" "ball x (min d e) \<subseteq> UNIV - i" unfolding ab ball_min_Int by auto
hoelzl@37489
   133
      hence "ball x (min d e) \<subseteq> s \<inter> interior (\<Union>f)" using e unfolding lem1 unfolding  ball_min_Int by auto
hoelzl@37489
   134
      hence "x \<in> s \<inter> interior (\<Union>f)" using `d>0` e by auto
himmelma@35172
   135
      hence "\<exists>t\<in>f. \<exists>x e. 0 < e \<and> ball x e \<subseteq> s \<inter> t" apply-apply(rule insert(3)) using insert(4) by auto thus ?thesis by auto next
himmelma@35172
   136
    case True show ?thesis proof(cases "x\<in>{a<..<b}")
himmelma@35172
   137
      case True then guess d unfolding open_contains_ball_eq[OF open_interval,rule_format] ..
himmelma@35172
   138
      thus ?thesis apply(rule_tac x=i in bexI,rule_tac x=x in exI,rule_tac x="min d e" in exI)
himmelma@35172
   139
	unfolding ab using interval_open_subset_closed[of a b] and e by fastsimp+ next
hoelzl@37489
   140
    case False then obtain k where "x$$k \<le> a$$k \<or> x$$k \<ge> b$$k" and k:"k<DIM('a)" unfolding mem_interval by(auto simp add:not_less) 
hoelzl@37489
   141
    hence "x$$k = a$$k \<or> x$$k = b$$k" using True unfolding ab and mem_interval apply(erule_tac x=k in allE) by auto
himmelma@35172
   142
    hence "\<exists>x. ball x (e/2) \<subseteq> s \<inter> (\<Union>f)" proof(erule_tac disjE)
hoelzl@37489
   143
      let ?z = "x - (e/2) *\<^sub>R basis k" assume as:"x$$k = a$$k" have "ball ?z (e / 2) \<inter> i = {}" apply(rule ccontr) unfolding ex_in_conv[THEN sym] proof(erule exE)
himmelma@35172
   144
	fix y assume "y \<in> ball ?z (e / 2) \<inter> i" hence "dist ?z y < e/2" and yi:"y\<in>i" by auto
hoelzl@37489
   145
	hence "\<bar>(?z - y) $$ k\<bar> < e/2" using component_le_norm[of "?z - y" k] unfolding dist_norm by auto
hoelzl@37489
   146
	hence "y$$k < a$$k" using e[THEN conjunct1] k by(auto simp add:field_simps basis_component as)
hoelzl@37489
   147
	hence "y \<notin> i" unfolding ab mem_interval not_all apply(rule_tac x=k in exI) using k by auto thus False using yi by auto qed
himmelma@35172
   148
      moreover have "ball ?z (e/2) \<subseteq> s \<inter> (\<Union>insert i f)" apply(rule order_trans[OF _ e[THEN conjunct2, unfolded lem1]]) proof
himmelma@35172
   149
	fix y assume as:"y\<in> ball ?z (e/2)" have "norm (x - y) \<le> \<bar>e\<bar> / 2 + norm (x - y - (e / 2) *\<^sub>R basis k)"
himmelma@35172
   150
	   apply-apply(rule order_trans,rule norm_triangle_sub[of "x - y" "(e/2) *\<^sub>R basis k"])
himmelma@35172
   151
	  unfolding norm_scaleR norm_basis by auto
huffman@36587
   152
	also have "\<dots> < \<bar>e\<bar> / 2 + \<bar>e\<bar> / 2" apply(rule add_strict_left_mono) using as unfolding mem_ball dist_norm using e by(auto simp add:field_simps)
huffman@36587
   153
	finally show "y\<in>ball x e" unfolding mem_ball dist_norm using e by(auto simp add:field_simps) qed
himmelma@35172
   154
      ultimately show ?thesis apply(rule_tac x="?z" in exI) unfolding Union_insert by auto
hoelzl@37489
   155
    next let ?z = "x + (e/2) *\<^sub>R basis k" assume as:"x$$k = b$$k" have "ball ?z (e / 2) \<inter> i = {}" apply(rule ccontr) unfolding ex_in_conv[THEN sym] proof(erule exE)
himmelma@35172
   156
	fix y assume "y \<in> ball ?z (e / 2) \<inter> i" hence "dist ?z y < e/2" and yi:"y\<in>i" by auto
hoelzl@37489
   157
	hence "\<bar>(?z - y) $$ k\<bar> < e/2" using component_le_norm[of "?z - y" k] unfolding dist_norm by auto
hoelzl@37489
   158
	hence "y$$k > b$$k" using e[THEN conjunct1] k by(auto simp add:field_simps as)
hoelzl@37489
   159
	hence "y \<notin> i" unfolding ab mem_interval not_all using k by(rule_tac x=k in exI,auto) thus False using yi by auto qed
himmelma@35172
   160
      moreover have "ball ?z (e/2) \<subseteq> s \<inter> (\<Union>insert i f)" apply(rule order_trans[OF _ e[THEN conjunct2, unfolded lem1]]) proof
himmelma@35172
   161
	fix y assume as:"y\<in> ball ?z (e/2)" have "norm (x - y) \<le> \<bar>e\<bar> / 2 + norm (x - y + (e / 2) *\<^sub>R basis k)"
himmelma@35172
   162
	   apply-apply(rule order_trans,rule norm_triangle_sub[of "x - y" "- (e/2) *\<^sub>R basis k"])
hoelzl@37489
   163
	  unfolding norm_scaleR by auto
huffman@36587
   164
	also have "\<dots> < \<bar>e\<bar> / 2 + \<bar>e\<bar> / 2" apply(rule add_strict_left_mono) using as unfolding mem_ball dist_norm using e by(auto simp add:field_simps)
huffman@36587
   165
	finally show "y\<in>ball x e" unfolding mem_ball dist_norm using e by(auto simp add:field_simps) qed
himmelma@35172
   166
      ultimately show ?thesis apply(rule_tac x="?z" in exI) unfolding Union_insert by auto qed 
himmelma@35172
   167
    then guess x .. hence "x \<in> s \<inter> interior (\<Union>f)" unfolding lem1[where U="\<Union>f",THEN sym] using centre_in_ball e[THEN conjunct1] by auto
himmelma@35172
   168
    thus ?thesis apply-apply(rule lem2,rule insert(3)) using insert(4) by auto qed qed qed qed note * = this
himmelma@35172
   169
  guess t using *[OF assms(1,3) goal1]  .. from this(2) guess x .. then guess e ..
himmelma@35172
   170
  hence "x \<in> s" "x\<in>interior t" defer using open_subset_interior[OF open_ball, of x e t] by auto
himmelma@35172
   171
  thus False using `t\<in>f` assms(4) by auto qed
hoelzl@37489
   172
himmelma@35172
   173
subsection {* Bounds on intervals where they exist. *}
himmelma@35172
   174
hoelzl@37489
   175
definition "interval_upperbound (s::('a::ordered_euclidean_space) set) = ((\<chi>\<chi> i. Sup {a. \<exists>x\<in>s. x$$i = a})::'a)"
hoelzl@37489
   176
hoelzl@37489
   177
definition "interval_lowerbound (s::('a::ordered_euclidean_space) set) = ((\<chi>\<chi> i. Inf {a. \<exists>x\<in>s. x$$i = a})::'a)"
hoelzl@37489
   178
hoelzl@37489
   179
lemma interval_upperbound[simp]: assumes "\<forall>i<DIM('a::ordered_euclidean_space). a$$i \<le> (b::'a)$$i" shows "interval_upperbound {a..b} = b"
hoelzl@37489
   180
  using assms unfolding interval_upperbound_def apply(subst euclidean_eq[where 'a='a]) apply safe
hoelzl@37489
   181
  unfolding euclidean_lambda_beta' apply(erule_tac x=i in allE)
himmelma@35172
   182
  apply(rule Sup_unique) unfolding setle_def apply rule unfolding mem_Collect_eq apply(erule bexE) unfolding mem_interval defer
hoelzl@37489
   183
  apply(rule,rule) apply(rule_tac x="b$$i" in bexI) defer unfolding mem_Collect_eq apply(rule_tac x=b in bexI)
himmelma@35172
   184
  unfolding mem_interval using assms by auto
himmelma@35172
   185
hoelzl@37489
   186
lemma interval_lowerbound[simp]: assumes "\<forall>i<DIM('a::ordered_euclidean_space). a$$i \<le> (b::'a)$$i" shows "interval_lowerbound {a..b} = a"
hoelzl@37489
   187
  using assms unfolding interval_lowerbound_def apply(subst euclidean_eq[where 'a='a]) apply safe
hoelzl@37489
   188
  unfolding euclidean_lambda_beta' apply(erule_tac x=i in allE)
himmelma@35172
   189
  apply(rule Inf_unique) unfolding setge_def apply rule unfolding mem_Collect_eq apply(erule bexE) unfolding mem_interval defer
hoelzl@37489
   190
  apply(rule,rule) apply(rule_tac x="a$$i" in bexI) defer unfolding mem_Collect_eq apply(rule_tac x=a in bexI)
hoelzl@37489
   191
  unfolding mem_interval using assms by auto 
himmelma@35172
   192
himmelma@35172
   193
lemmas interval_bounds = interval_upperbound interval_lowerbound
himmelma@35172
   194
himmelma@35172
   195
lemma interval_bounds'[simp]: assumes "{a..b}\<noteq>{}" shows "interval_upperbound {a..b} = b" "interval_lowerbound {a..b} = a"
himmelma@35172
   196
  using assms unfolding interval_ne_empty by auto
himmelma@35172
   197
himmelma@35172
   198
subsection {* Content (length, area, volume...) of an interval. *}
himmelma@35172
   199
hoelzl@37489
   200
definition "content (s::('a::ordered_euclidean_space) set) =
hoelzl@37489
   201
       (if s = {} then 0 else (\<Prod>i<DIM('a). (interval_upperbound s)$$i - (interval_lowerbound s)$$i))"
hoelzl@37489
   202
hoelzl@37489
   203
lemma interval_not_empty:"\<forall>i<DIM('a). a$$i \<le> b$$i \<Longrightarrow> {a..b::'a::ordered_euclidean_space} \<noteq> {}"
hoelzl@37489
   204
  unfolding interval_eq_empty unfolding not_ex not_less by auto
hoelzl@37489
   205
hoelzl@37489
   206
lemma content_closed_interval: fixes a::"'a::ordered_euclidean_space" assumes "\<forall>i<DIM('a). a$$i \<le> b$$i"
hoelzl@37489
   207
  shows "content {a..b} = (\<Prod>i<DIM('a). b$$i - a$$i)"
himmelma@35172
   208
  using interval_not_empty[OF assms] unfolding content_def interval_upperbound[OF assms] interval_lowerbound[OF assms] by auto
himmelma@35172
   209
hoelzl@37489
   210
lemma content_closed_interval': fixes a::"'a::ordered_euclidean_space" assumes "{a..b}\<noteq>{}" shows "content {a..b} = (\<Prod>i<DIM('a). b$$i - a$$i)"
himmelma@35172
   211
  apply(rule content_closed_interval) using assms unfolding interval_ne_empty .
himmelma@35172
   212
hoelzl@37489
   213
lemma content_real:assumes "a\<le>b" shows "content {a..b} = b-a"
hoelzl@37489
   214
proof- have *:"{..<Suc 0} = {0}" by auto
hoelzl@37489
   215
  show ?thesis unfolding content_def using assms by(auto simp: *)
hoelzl@37489
   216
qed
hoelzl@37489
   217
hoelzl@37489
   218
lemma content_unit[intro]: "content{0..One::'a::ordered_euclidean_space} = 1" proof-
hoelzl@37489
   219
  have *:"\<forall>i<DIM('a). (0::'a)$$i \<le> (One::'a)$$i" by auto
hoelzl@37489
   220
  have "0 \<in> {0..One::'a}" unfolding mem_interval by auto
himmelma@35172
   221
  thus ?thesis unfolding content_def interval_bounds[OF *] using setprod_1 by auto qed
himmelma@35172
   222
hoelzl@37489
   223
lemma content_pos_le[intro]: fixes a::"'a::ordered_euclidean_space" shows "0 \<le> content {a..b}" proof(cases "{a..b}={}")
hoelzl@37489
   224
  case False hence *:"\<forall>i<DIM('a). a $$ i \<le> b $$ i" unfolding interval_ne_empty by assumption
hoelzl@37489
   225
  have "(\<Prod>i<DIM('a). interval_upperbound {a..b} $$ i - interval_lowerbound {a..b} $$ i) \<ge> 0"
himmelma@35172
   226
    apply(rule setprod_nonneg) unfolding interval_bounds[OF *] using * apply(erule_tac x=x in allE) by auto
himmelma@35172
   227
  thus ?thesis unfolding content_def by(auto simp del:interval_bounds') qed(unfold content_def, auto)
himmelma@35172
   228
hoelzl@37489
   229
lemma content_pos_lt: fixes a::"'a::ordered_euclidean_space" assumes "\<forall>i<DIM('a). a$$i < b$$i" shows "0 < content {a..b}"
hoelzl@37489
   230
proof- have help_lemma1: "\<forall>i<DIM('a). a$$i < b$$i \<Longrightarrow> \<forall>i<DIM('a). a$$i \<le> ((b$$i)::real)" apply(rule,erule_tac x=i in allE) by auto
himmelma@35172
   231
  show ?thesis unfolding content_closed_interval[OF help_lemma1[OF assms]] apply(rule setprod_pos)
himmelma@35172
   232
    using assms apply(erule_tac x=x in allE) by auto qed
himmelma@35172
   233
hoelzl@37489
   234
lemma content_eq_0: "content{a..b::'a::ordered_euclidean_space} = 0 \<longleftrightarrow> (\<exists>i<DIM('a). b$$i \<le> a$$i)" proof(cases "{a..b} = {}")
himmelma@35172
   235
  case True thus ?thesis unfolding content_def if_P[OF True] unfolding interval_eq_empty apply-
himmelma@35172
   236
    apply(rule,erule exE) apply(rule_tac x=i in exI) by auto next
hoelzl@37489
   237
  case False note this[unfolded interval_eq_empty not_ex not_less]
hoelzl@37489
   238
  hence as:"\<forall>i<DIM('a). b $$ i \<ge> a $$ i" by fastsimp
hoelzl@37489
   239
  show ?thesis unfolding content_def if_not_P[OF False] setprod_zero_iff[OF finite_lessThan]
himmelma@35172
   240
    apply(rule) apply(erule_tac[!] exE bexE) unfolding interval_bounds[OF as] apply(rule_tac x=x in exI) defer
himmelma@35172
   241
    apply(rule_tac x=i in bexI) using as apply(erule_tac x=i in allE) by auto qed
himmelma@35172
   242
himmelma@35172
   243
lemma cond_cases:"(P \<Longrightarrow> Q x) \<Longrightarrow> (\<not> P \<Longrightarrow> Q y) \<Longrightarrow> Q (if P then x else y)" by auto
himmelma@35172
   244
himmelma@35172
   245
lemma content_closed_interval_cases:
hoelzl@37489
   246
  "content {a..b::'a::ordered_euclidean_space} = (if \<forall>i<DIM('a). a$$i \<le> b$$i then setprod (\<lambda>i. b$$i - a$$i) {..<DIM('a)} else 0)" apply(rule cond_cases) 
himmelma@35172
   247
  apply(rule content_closed_interval) unfolding content_eq_0 not_all not_le defer apply(erule exE,rule_tac x=x in exI) by auto
himmelma@35172
   248
himmelma@35172
   249
lemma content_eq_0_interior: "content {a..b} = 0 \<longleftrightarrow> interior({a..b}) = {}"
himmelma@35172
   250
  unfolding content_eq_0 interior_closed_interval interval_eq_empty by auto
himmelma@35172
   251
hoelzl@37489
   252
(*lemma content_eq_0_1: "content {a..b::real^1} = 0 \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a"
hoelzl@37489
   253
  unfolding content_eq_0 by auto*)
hoelzl@37489
   254
hoelzl@37489
   255
lemma content_pos_lt_eq: "0 < content {a..b::'a::ordered_euclidean_space} \<longleftrightarrow> (\<forall>i<DIM('a). a$$i < b$$i)"
himmelma@35172
   256
  apply(rule) defer apply(rule content_pos_lt,assumption) proof- assume "0 < content {a..b}"
hoelzl@37489
   257
  hence "content {a..b} \<noteq> 0" by auto thus "\<forall>i<DIM('a). a$$i < b$$i" unfolding content_eq_0 not_ex not_le by fastsimp qed
himmelma@35172
   258
himmelma@35172
   259
lemma content_empty[simp]: "content {} = 0" unfolding content_def by auto
himmelma@35172
   260
hoelzl@37489
   261
lemma content_subset: assumes "{a..b} \<subseteq> {c..d}" shows "content {a..b::'a::ordered_euclidean_space} \<le> content {c..d}" proof(cases "{a..b}={}")
himmelma@35172
   262
  case True thus ?thesis using content_pos_le[of c d] by auto next
hoelzl@37489
   263
  case False hence ab_ne:"\<forall>i<DIM('a). a $$ i \<le> b $$ i" unfolding interval_ne_empty by auto
himmelma@35172
   264
  hence ab_ab:"a\<in>{a..b}" "b\<in>{a..b}" unfolding mem_interval by auto
himmelma@35172
   265
  have "{c..d} \<noteq> {}" using assms False by auto
hoelzl@37489
   266
  hence cd_ne:"\<forall>i<DIM('a). c $$ i \<le> d $$ i" using assms unfolding interval_ne_empty by auto
himmelma@35172
   267
  show ?thesis unfolding content_def unfolding interval_bounds[OF ab_ne] interval_bounds[OF cd_ne]
hoelzl@37489
   268
    unfolding if_not_P[OF False] if_not_P[OF `{c..d} \<noteq> {}`] apply(rule setprod_mono,rule) proof
hoelzl@37489
   269
    fix i assume i:"i\<in>{..<DIM('a)}"
hoelzl@37489
   270
    show "0 \<le> b $$ i - a $$ i" using ab_ne[THEN spec[where x=i]] i by auto
hoelzl@37489
   271
    show "b $$ i - a $$ i \<le> d $$ i - c $$ i"
himmelma@35172
   272
      using assms[unfolded subset_eq mem_interval,rule_format,OF ab_ab(2),of i]
hoelzl@37489
   273
      using assms[unfolded subset_eq mem_interval,rule_format,OF ab_ab(1),of i] using i by auto qed qed
himmelma@35172
   274
himmelma@35172
   275
lemma content_lt_nz: "0 < content {a..b} \<longleftrightarrow> content {a..b} \<noteq> 0"
hoelzl@37489
   276
  unfolding content_pos_lt_eq content_eq_0 unfolding not_ex not_le by fastsimp
himmelma@35172
   277
himmelma@35172
   278
subsection {* The notion of a gauge --- simply an open set containing the point. *}
himmelma@35172
   279
himmelma@35172
   280
definition gauge where "gauge d \<longleftrightarrow> (\<forall>x. x\<in>(d x) \<and> open(d x))"
himmelma@35172
   281
himmelma@35172
   282
lemma gaugeI:assumes "\<And>x. x\<in>g x" "\<And>x. open (g x)" shows "gauge g"
himmelma@35172
   283
  using assms unfolding gauge_def by auto
himmelma@35172
   284
himmelma@35172
   285
lemma gaugeD[dest]: assumes "gauge d" shows "x\<in>d x" "open (d x)" using assms unfolding gauge_def by auto
himmelma@35172
   286
himmelma@35172
   287
lemma gauge_ball_dependent: "\<forall>x. 0 < e x \<Longrightarrow> gauge (\<lambda>x. ball x (e x))"
himmelma@35172
   288
  unfolding gauge_def by auto 
himmelma@35172
   289
himmelma@35751
   290
lemma gauge_ball[intro]: "0 < e \<Longrightarrow> gauge (\<lambda>x. ball x e)" unfolding gauge_def by auto 
himmelma@35172
   291
himmelma@35172
   292
lemma gauge_trivial[intro]: "gauge (\<lambda>x. ball x 1)" apply(rule gauge_ball) by auto
himmelma@35172
   293
himmelma@35751
   294
lemma gauge_inter[intro]: "gauge d1 \<Longrightarrow> gauge d2 \<Longrightarrow> gauge (\<lambda>x. (d1 x) \<inter> (d2 x))"
himmelma@35172
   295
  unfolding gauge_def by auto 
himmelma@35172
   296
himmelma@35172
   297
lemma gauge_inters: assumes "finite s" "\<forall>d\<in>s. gauge (f d)" shows "gauge(\<lambda>x. \<Inter> {f d x | d. d \<in> s})" proof-
himmelma@35172
   298
  have *:"\<And>x. {f d x |d. d \<in> s} = (\<lambda>d. f d x) ` s" by auto show ?thesis
himmelma@35172
   299
  unfolding gauge_def unfolding * 
himmelma@35172
   300
  using assms unfolding Ball_def Inter_iff mem_Collect_eq gauge_def by auto qed
himmelma@35172
   301
himmelma@35172
   302
lemma gauge_existence_lemma: "(\<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)" by(meson zero_less_one)
himmelma@35172
   303
himmelma@35172
   304
subsection {* Divisions. *}
himmelma@35172
   305
himmelma@35172
   306
definition division_of (infixl "division'_of" 40) where
himmelma@35172
   307
  "s division_of i \<equiv>
himmelma@35172
   308
        finite s \<and>
himmelma@35172
   309
        (\<forall>k\<in>s. k \<subseteq> i \<and> k \<noteq> {} \<and> (\<exists>a b. k = {a..b})) \<and>
himmelma@35172
   310
        (\<forall>k1\<in>s. \<forall>k2\<in>s. k1 \<noteq> k2 \<longrightarrow> interior(k1) \<inter> interior(k2) = {}) \<and>
himmelma@35172
   311
        (\<Union>s = i)"
himmelma@35172
   312
himmelma@35172
   313
lemma division_ofD[dest]: assumes  "s division_of i"
himmelma@35172
   314
  shows"finite s" "\<And>k. k\<in>s \<Longrightarrow> k \<subseteq> i" "\<And>k. k\<in>s \<Longrightarrow>  k \<noteq> {}" "\<And>k. k\<in>s \<Longrightarrow> (\<exists>a b. k = {a..b})"
himmelma@35172
   315
  "\<And>k1 k2. \<lbrakk>k1\<in>s; k2\<in>s; k1 \<noteq> k2\<rbrakk> \<Longrightarrow> interior(k1) \<inter> interior(k2) = {}" "\<Union>s = i" using assms unfolding division_of_def by auto
himmelma@35172
   316
himmelma@35172
   317
lemma division_ofI:
himmelma@35172
   318
  assumes "finite s" "\<And>k. k\<in>s \<Longrightarrow> k \<subseteq> i" "\<And>k. k\<in>s \<Longrightarrow>  k \<noteq> {}" "\<And>k. k\<in>s \<Longrightarrow> (\<exists>a b. k = {a..b})"
himmelma@35172
   319
  "\<And>k1 k2. \<lbrakk>k1\<in>s; k2\<in>s; k1 \<noteq> k2\<rbrakk> \<Longrightarrow> interior(k1) \<inter> interior(k2) = {}" "\<Union>s = i"
himmelma@35172
   320
  shows "s division_of i" using assms unfolding division_of_def by auto
himmelma@35172
   321
himmelma@35172
   322
lemma division_of_finite: "s division_of i \<Longrightarrow> finite s"
himmelma@35172
   323
  unfolding division_of_def by auto
himmelma@35172
   324
himmelma@35172
   325
lemma division_of_self[intro]: "{a..b} \<noteq> {} \<Longrightarrow> {{a..b}} division_of {a..b}"
himmelma@35172
   326
  unfolding division_of_def by auto
himmelma@35172
   327
himmelma@35172
   328
lemma division_of_trivial[simp]: "s division_of {} \<longleftrightarrow> s = {}" unfolding division_of_def by auto 
himmelma@35172
   329
hoelzl@37489
   330
lemma division_of_sing[simp]: "s division_of {a..a::'a::ordered_euclidean_space} \<longleftrightarrow> s = {{a..a}}" (is "?l = ?r") proof
himmelma@35172
   331
  assume ?r moreover { assume "s = {{a}}" moreover fix k assume "k\<in>s" 
hoelzl@37489
   332
    ultimately have"\<exists>x y. k = {x..y}" apply(rule_tac x=a in exI)+ unfolding interval_sing by auto }
hoelzl@37489
   333
  ultimately show ?l unfolding division_of_def interval_sing by auto next
hoelzl@37489
   334
  assume ?l note as=conjunctD4[OF this[unfolded division_of_def interval_sing]]
himmelma@35172
   335
  { fix x assume x:"x\<in>s" have "x={a}" using as(2)[rule_format,OF x] by auto }
hoelzl@37489
   336
  moreover have "s \<noteq> {}" using as(4) by auto ultimately show ?r unfolding interval_sing by auto qed
himmelma@35172
   337
himmelma@35172
   338
lemma elementary_empty: obtains p where "p division_of {}"
himmelma@35172
   339
  unfolding division_of_trivial by auto
himmelma@35172
   340
himmelma@35172
   341
lemma elementary_interval: obtains p where  "p division_of {a..b}"
himmelma@35172
   342
  by(metis division_of_trivial division_of_self)
himmelma@35172
   343
himmelma@35172
   344
lemma division_contains: "s division_of i \<Longrightarrow> \<forall>x\<in>i. \<exists>k\<in>s. x \<in> k"
himmelma@35172
   345
  unfolding division_of_def by auto
himmelma@35172
   346
himmelma@35172
   347
lemma forall_in_division:
himmelma@35172
   348
 "d division_of i \<Longrightarrow> ((\<forall>x\<in>d. P x) \<longleftrightarrow> (\<forall>a b. {a..b} \<in> d \<longrightarrow> P {a..b}))"
himmelma@35172
   349
  unfolding division_of_def by fastsimp
himmelma@35172
   350
himmelma@35172
   351
lemma division_of_subset: assumes "p division_of (\<Union>p)" "q \<subseteq> p" shows "q division_of (\<Union>q)"
himmelma@35172
   352
  apply(rule division_ofI) proof- note as=division_ofD[OF assms(1)]
himmelma@35172
   353
  show "finite q" apply(rule finite_subset) using as(1) assms(2) by auto
himmelma@35172
   354
  { fix k assume "k \<in> q" hence kp:"k\<in>p" using assms(2) by auto show "k\<subseteq>\<Union>q" using `k \<in> q` by auto
himmelma@35172
   355
  show "\<exists>a b. k = {a..b}" using as(4)[OF kp] by auto show "k \<noteq> {}" using as(3)[OF kp] by auto }
himmelma@35172
   356
  fix k1 k2 assume "k1 \<in> q" "k2 \<in> q" "k1 \<noteq> k2" hence *:"k1\<in>p" "k2\<in>p" "k1\<noteq>k2" using assms(2) by auto
himmelma@35172
   357
  show "interior k1 \<inter> interior k2 = {}" using as(5)[OF *] by auto qed auto
himmelma@35172
   358
himmelma@35172
   359
lemma division_of_union_self[intro]: "p division_of s \<Longrightarrow> p division_of (\<Union>p)" unfolding division_of_def by auto
himmelma@35172
   360
himmelma@35172
   361
lemma division_of_content_0: assumes "content {a..b} = 0" "d division_of {a..b}" shows "\<forall>k\<in>d. content k = 0"
himmelma@35172
   362
  unfolding forall_in_division[OF assms(2)] apply(rule,rule,rule) apply(drule division_ofD(2)[OF assms(2)])
himmelma@35172
   363
  apply(drule content_subset) unfolding assms(1) proof- case goal1 thus ?case using content_pos_le[of a b] by auto qed
himmelma@35172
   364
hoelzl@37489
   365
lemma division_inter: assumes "p1 division_of s1" "p2 division_of (s2::('a::ordered_euclidean_space) set)"
himmelma@35172
   366
  shows "{k1 \<inter> k2 | k1 k2 .k1 \<in> p1 \<and> k2 \<in> p2 \<and> k1 \<inter> k2 \<noteq> {}} division_of (s1 \<inter> s2)" (is "?A' division_of _") proof-
himmelma@35172
   367
let ?A = "{s. s \<in>  (\<lambda>(k1,k2). k1 \<inter> k2) ` (p1 \<times> p2) \<and> s \<noteq> {}}" have *:"?A' = ?A" by auto
himmelma@35172
   368
show ?thesis unfolding * proof(rule division_ofI) have "?A \<subseteq> (\<lambda>(x, y). x \<inter> y) ` (p1 \<times> p2)" by auto
himmelma@35172
   369
  moreover have "finite (p1 \<times> p2)" using assms unfolding division_of_def by auto ultimately show "finite ?A" by auto
himmelma@35172
   370
  have *:"\<And>s. \<Union>{x\<in>s. x \<noteq> {}} = \<Union>s" by auto show "\<Union>?A = s1 \<inter> s2" apply(rule set_ext) unfolding * and Union_image_eq UN_iff
himmelma@35172
   371
    using division_ofD(6)[OF assms(1)] and division_ofD(6)[OF assms(2)] by auto
himmelma@35172
   372
  { fix k assume "k\<in>?A" then obtain k1 k2 where k:"k = k1 \<inter> k2" "k1\<in>p1" "k2\<in>p2" "k\<noteq>{}" by auto thus "k \<noteq> {}" by auto
himmelma@35172
   373
  show "k \<subseteq> s1 \<inter> s2" using division_ofD(2)[OF assms(1) k(2)] and division_ofD(2)[OF assms(2) k(3)] unfolding k by auto
himmelma@35172
   374
  guess a1 using division_ofD(4)[OF assms(1) k(2)] .. then guess b1 .. note ab1=this
himmelma@35172
   375
  guess a2 using division_ofD(4)[OF assms(2) k(3)] .. then guess b2 .. note ab2=this
himmelma@35172
   376
  show "\<exists>a b. k = {a..b}" unfolding k ab1 ab2 unfolding inter_interval by auto } fix k1 k2
himmelma@35172
   377
  assume "k1\<in>?A" then obtain x1 y1 where k1:"k1 = x1 \<inter> y1" "x1\<in>p1" "y1\<in>p2" "k1\<noteq>{}" by auto
himmelma@35172
   378
  assume "k2\<in>?A" then obtain x2 y2 where k2:"k2 = x2 \<inter> y2" "x2\<in>p1" "y2\<in>p2" "k2\<noteq>{}" by auto
himmelma@35172
   379
  assume "k1 \<noteq> k2" hence th:"x1\<noteq>x2 \<or> y1\<noteq>y2" unfolding k1 k2 by auto
himmelma@35172
   380
  have *:"(interior x1 \<inter> interior x2 = {} \<or> interior y1 \<inter> interior y2 = {}) \<Longrightarrow>
himmelma@35172
   381
      interior(x1 \<inter> y1) \<subseteq> interior(x1) \<Longrightarrow> interior(x1 \<inter> y1) \<subseteq> interior(y1) \<Longrightarrow>
himmelma@35172
   382
      interior(x2 \<inter> y2) \<subseteq> interior(x2) \<Longrightarrow> interior(x2 \<inter> y2) \<subseteq> interior(y2)
himmelma@35172
   383
      \<Longrightarrow> interior(x1 \<inter> y1) \<inter> interior(x2 \<inter> y2) = {}" by auto
himmelma@35172
   384
  show "interior k1 \<inter> interior k2 = {}" unfolding k1 k2 apply(rule *) defer apply(rule_tac[1-4] subset_interior)
himmelma@35172
   385
    using division_ofD(5)[OF assms(1) k1(2) k2(2)]
himmelma@35172
   386
    using division_ofD(5)[OF assms(2) k1(3) k2(3)] using th by auto qed qed
himmelma@35172
   387
hoelzl@37489
   388
lemma division_inter_1: assumes "d division_of i" "{a..b::'a::ordered_euclidean_space} \<subseteq> i"
himmelma@35172
   389
  shows "{ {a..b} \<inter> k |k. k \<in> d \<and> {a..b} \<inter> k \<noteq> {} } division_of {a..b}" proof(cases "{a..b} = {}")
himmelma@35172
   390
  case True show ?thesis unfolding True and division_of_trivial by auto next
himmelma@35172
   391
  have *:"{a..b} \<inter> i = {a..b}" using assms(2) by auto 
himmelma@35172
   392
  case False show ?thesis using division_inter[OF division_of_self[OF False] assms(1)] unfolding * by auto qed
himmelma@35172
   393
hoelzl@37489
   394
lemma elementary_inter: assumes "p1 division_of s" "p2 division_of (t::('a::ordered_euclidean_space) set)"
himmelma@35172
   395
  shows "\<exists>p. p division_of (s \<inter> t)"
himmelma@35172
   396
  by(rule,rule division_inter[OF assms])
himmelma@35172
   397
hoelzl@37489
   398
lemma elementary_inters: assumes "finite f" "f\<noteq>{}" "\<forall>s\<in>f. \<exists>p. p division_of (s::('a::ordered_euclidean_space) set)"
himmelma@35172
   399
  shows "\<exists>p. p division_of (\<Inter> f)" using assms apply-proof(induct f rule:finite_induct)
himmelma@35172
   400
case (insert x f) show ?case proof(cases "f={}")
himmelma@35172
   401
  case True thus ?thesis unfolding True using insert by auto next
himmelma@35172
   402
  case False guess p using insert(3)[OF False insert(5)[unfolded ball_simps,THEN conjunct2]] ..
himmelma@35172
   403
  moreover guess px using insert(5)[rule_format,OF insertI1] .. ultimately
himmelma@35172
   404
  show ?thesis unfolding Inter_insert apply(rule_tac elementary_inter) by assumption+ qed qed auto
himmelma@35172
   405
himmelma@35172
   406
lemma division_disjoint_union:
himmelma@35172
   407
  assumes "p1 division_of s1" "p2 division_of s2" "interior s1 \<inter> interior s2 = {}"
himmelma@35172
   408
  shows "(p1 \<union> p2) division_of (s1 \<union> s2)" proof(rule division_ofI) 
himmelma@35172
   409
  note d1 = division_ofD[OF assms(1)] and d2 = division_ofD[OF assms(2)]
himmelma@35172
   410
  show "finite (p1 \<union> p2)" using d1(1) d2(1) by auto
himmelma@35172
   411
  show "\<Union>(p1 \<union> p2) = s1 \<union> s2" using d1(6) d2(6) by auto
himmelma@35172
   412
  { fix k1 k2 assume as:"k1 \<in> p1 \<union> p2" "k2 \<in> p1 \<union> p2" "k1 \<noteq> k2" moreover let ?g="interior k1 \<inter> interior k2 = {}"
himmelma@35172
   413
  { assume as:"k1\<in>p1" "k2\<in>p2" have ?g using subset_interior[OF d1(2)[OF as(1)]] subset_interior[OF d2(2)[OF as(2)]]
himmelma@35172
   414
      using assms(3) by blast } moreover
himmelma@35172
   415
  { assume as:"k1\<in>p2" "k2\<in>p1" have ?g using subset_interior[OF d1(2)[OF as(2)]] subset_interior[OF d2(2)[OF as(1)]]
himmelma@35172
   416
      using assms(3) by blast} ultimately
himmelma@35172
   417
  show ?g using d1(5)[OF _ _ as(3)] and d2(5)[OF _ _ as(3)] by auto }
himmelma@35172
   418
  fix k assume k:"k \<in> p1 \<union> p2"  show "k \<subseteq> s1 \<union> s2" using k d1(2) d2(2) by auto
himmelma@35172
   419
  show "k \<noteq> {}" using k d1(3) d2(3) by auto show "\<exists>a b. k = {a..b}" using k d1(4) d2(4) by auto qed
himmelma@35172
   420
hoelzl@37489
   421
(* move *)
hoelzl@37489
   422
lemma Eucl_nth_inverse[simp]: fixes x::"'a::euclidean_space" shows "(\<chi>\<chi> i. x $$ i) = x"
hoelzl@37489
   423
  apply(subst euclidean_eq) by auto
hoelzl@37489
   424
himmelma@35172
   425
lemma partial_division_extend_1:
hoelzl@37489
   426
  assumes "{c..d} \<subseteq> {a..b::'a::ordered_euclidean_space}" "{c..d} \<noteq> {}"
himmelma@35172
   427
  obtains p where "p division_of {a..b}" "{c..d} \<in> p"
hoelzl@37489
   428
proof- def n \<equiv> "DIM('a)" have n:"1 \<le> n" "0 < n" "n \<noteq> 0" unfolding n_def using DIM_positive[where 'a='a] by auto
hoelzl@37489
   429
  guess \<pi> using ex_bij_betw_nat_finite_1[OF finite_lessThan[of "DIM('a)"]] .. note \<pi>=this
himmelma@35172
   430
  def \<pi>' \<equiv> "inv_into {1..n} \<pi>"
hoelzl@37489
   431
  have \<pi>':"bij_betw \<pi>' {..<DIM('a)} {1..n}" using bij_betw_inv_into[OF \<pi>] unfolding \<pi>'_def n_def by auto
hoelzl@37489
   432
  hence \<pi>'i:"\<And>i. i<DIM('a) \<Longrightarrow> \<pi>' i \<in> {1..n}" unfolding bij_betw_def by auto 
hoelzl@37489
   433
  have \<pi>i:"\<And>i. i\<in>{1..n} \<Longrightarrow> \<pi> i <DIM('a)" using \<pi> unfolding bij_betw_def n_def by auto 
hoelzl@37489
   434
  have \<pi>\<pi>'[simp]:"\<And>i. i<DIM('a) \<Longrightarrow> \<pi> (\<pi>' i) = i" unfolding \<pi>'_def
hoelzl@37489
   435
    apply(rule f_inv_into_f) unfolding n_def using \<pi> unfolding bij_betw_def by auto
hoelzl@37489
   436
  have \<pi>'\<pi>[simp]:"\<And>i. i\<in>{1..n} \<Longrightarrow> \<pi>' (\<pi> i) = i" unfolding \<pi>'_def apply(rule inv_into_f_eq)
hoelzl@37489
   437
    using \<pi> unfolding n_def bij_betw_def by auto
himmelma@35172
   438
  have "{c..d} \<noteq> {}" using assms by auto
hoelzl@37489
   439
  let ?p1 = "\<lambda>l. {(\<chi>\<chi> i. if \<pi>' i < l then c$$i else a$$i)::'a .. (\<chi>\<chi> i. if \<pi>' i < l then d$$i else if \<pi>' i = l then c$$\<pi> l else b$$i)}"
hoelzl@37489
   440
  let ?p2 = "\<lambda>l. {(\<chi>\<chi> i. if \<pi>' i < l then c$$i else if \<pi>' i = l then d$$\<pi> l else a$$i)::'a .. (\<chi>\<chi> i. if \<pi>' i < l then d$$i else b$$i)}"
himmelma@35172
   441
  let ?p =  "{?p1 l |l. l \<in> {1..n+1}} \<union> {?p2 l |l. l \<in> {1..n+1}}"
hoelzl@37489
   442
  have abcd:"\<And>i. i<DIM('a) \<Longrightarrow> a $$ i \<le> c $$ i \<and> c$$i \<le> d$$i \<and> d $$ i \<le> b $$ i" using assms
hoelzl@37489
   443
    unfolding subset_interval interval_eq_empty by auto
himmelma@35172
   444
  show ?thesis apply(rule that[of ?p]) apply(rule division_ofI)
hoelzl@37489
   445
  proof- have "\<And>i. i<DIM('a) \<Longrightarrow> \<pi>' i < Suc n"
hoelzl@37489
   446
    proof(rule ccontr,unfold not_less) fix i assume i:"i<DIM('a)" and "Suc n \<le> \<pi>' i"
hoelzl@37489
   447
      hence "\<pi>' i \<notin> {1..n}" by auto thus False using \<pi>' i unfolding bij_betw_def by auto
hoelzl@37489
   448
    qed hence "c = (\<chi>\<chi> i. if \<pi>' i < Suc n then c $$ i else a $$ i)"
hoelzl@37489
   449
        "d = (\<chi>\<chi> i. if \<pi>' i < Suc n then d $$ i else if \<pi>' i = n + 1 then c $$ \<pi> (n + 1) else b $$ i)"
hoelzl@37489
   450
      unfolding euclidean_eq[where 'a='a] using \<pi>' unfolding bij_betw_def by auto
himmelma@35172
   451
    thus cdp:"{c..d} \<in> ?p" apply-apply(rule UnI1) unfolding mem_Collect_eq apply(rule_tac x="n + 1" in exI) by auto
himmelma@35172
   452
    have "\<And>l. l\<in>{1..n+1} \<Longrightarrow> ?p1 l \<subseteq> {a..b}"  "\<And>l. l\<in>{1..n+1} \<Longrightarrow> ?p2 l \<subseteq> {a..b}"
himmelma@35172
   453
      unfolding subset_eq apply(rule_tac[!] ballI,rule_tac[!] ccontr)
himmelma@35172
   454
    proof- fix l assume l:"l\<in>{1..n+1}" fix x assume "x\<notin>{a..b}"
hoelzl@37489
   455
      then guess i unfolding mem_interval not_all not_imp .. note i=conjunctD2[OF this]
himmelma@35172
   456
      show "x \<in> ?p1 l \<Longrightarrow> False" "x \<in> ?p2 l \<Longrightarrow> False" unfolding mem_interval apply(erule_tac[!] x=i in allE)
himmelma@35172
   457
        apply(case_tac[!] "\<pi>' i < l", case_tac[!] "\<pi>' i = l") using abcd[of i] i by auto 
himmelma@35172
   458
    qed moreover have "\<And>x. x \<in> {a..b} \<Longrightarrow> x \<in> \<Union>?p"
himmelma@35172
   459
    proof- fix x assume x:"x\<in>{a..b}"
himmelma@35172
   460
      { presume "x\<notin>{c..d} \<Longrightarrow> x \<in> \<Union>?p" thus "x \<in> \<Union>?p" using cdp by blast }
hoelzl@37489
   461
      let ?M = "{i. i\<in>{1..n+1} \<and> \<not> (c $$ \<pi> i \<le> x $$ \<pi> i \<and> x $$ \<pi> i \<le> d $$ \<pi> i)}"
hoelzl@37489
   462
      assume "x\<notin>{c..d}" then guess i0 unfolding mem_interval not_all not_imp ..
himmelma@35172
   463
      hence "\<pi>' i0 \<in> ?M" using \<pi>' unfolding bij_betw_def by(auto intro!:le_SucI)
himmelma@35172
   464
      hence M:"finite ?M" "?M \<noteq> {}" by auto
himmelma@35172
   465
      def l \<equiv> "Min ?M" note l = Min_less_iff[OF M,unfolded l_def[symmetric]] Min_in[OF M,unfolded mem_Collect_eq l_def[symmetric]]
himmelma@35172
   466
        Min_gr_iff[OF M,unfolded l_def[symmetric]]
himmelma@35172
   467
      have "x\<in>?p1 l \<or> x\<in>?p2 l" using l(2)[THEN conjunct2] unfolding de_Morgan_conj not_le
himmelma@35172
   468
        apply- apply(erule disjE) apply(rule disjI1) defer apply(rule disjI2)
hoelzl@37489
   469
      proof- assume as:"x $$ \<pi> l < c $$ \<pi> l"
hoelzl@37489
   470
        show "x \<in> ?p1 l" unfolding mem_interval apply safe unfolding euclidean_lambda_beta'
hoelzl@37489
   471
        proof- case goal1 have "\<pi>' i \<in> {1..n}" using \<pi>' unfolding bij_betw_def not_le using goal1 by auto
himmelma@35172
   472
          thus ?case using as x[unfolded mem_interval,rule_format,of i]
hoelzl@37489
   473
            apply auto using l(3)[of "\<pi>' i"] using goal1 by(auto elim!:ballE[where x="\<pi>' i"])
hoelzl@37489
   474
        next case goal2 have "\<pi>' i \<in> {1..n}" using \<pi>' unfolding bij_betw_def not_le using goal2 by auto
hoelzl@37489
   475
          thus ?case using as x[unfolded mem_interval,rule_format,of i]
hoelzl@37489
   476
            apply auto using l(3)[of "\<pi>' i"] using goal2 by(auto elim!:ballE[where x="\<pi>' i"])
himmelma@35172
   477
        qed
hoelzl@37489
   478
      next assume as:"x $$ \<pi> l > d $$ \<pi> l"
hoelzl@37489
   479
        show "x \<in> ?p2 l" unfolding mem_interval apply safe unfolding euclidean_lambda_beta'
hoelzl@37489
   480
        proof- fix i assume i:"i<DIM('a)"
hoelzl@37489
   481
          have "\<pi>' i \<in> {1..n}" using \<pi>' unfolding bij_betw_def not_le using i by auto
hoelzl@37489
   482
          thus "(if \<pi>' i < l then c $$ i else if \<pi>' i = l then d $$ \<pi> l else a $$ i) \<le> x $$ i"
hoelzl@37489
   483
            "x $$ i \<le> (if \<pi>' i < l then d $$ i else b $$ i)"
hoelzl@37489
   484
            using as x[unfolded mem_interval,rule_format,of i]
hoelzl@37489
   485
            apply auto using l(3)[of "\<pi>' i"] i by(auto elim!:ballE[where x="\<pi>' i"])
himmelma@35172
   486
        qed qed
himmelma@35172
   487
      thus "x \<in> \<Union>?p" using l(2) by blast 
himmelma@35172
   488
    qed ultimately show "\<Union>?p = {a..b}" apply-apply(rule) defer apply(rule) by(assumption,blast)
himmelma@35172
   489
    
himmelma@35172
   490
    show "finite ?p" by auto
himmelma@35172
   491
    fix k assume k:"k\<in>?p" then obtain l where l:"k = ?p1 l \<or> k = ?p2 l" "l \<in> {1..n + 1}" by auto
himmelma@35172
   492
    show "k\<subseteq>{a..b}" apply(rule,unfold mem_interval,rule,rule) 
hoelzl@37489
   493
    proof fix i x assume i:"i<DIM('a)" assume "x \<in> k" moreover have "\<pi>' i < l \<or> \<pi>' i = l \<or> \<pi>' i > l" by auto
hoelzl@37489
   494
      ultimately show "a$$i \<le> x$$i" "x$$i \<le> b$$i" using abcd[of i] using l using i
hoelzl@37489
   495
        by(auto elim:disjE elim!:allE[where x=i] simp add:eucl_le[where 'a='a])
himmelma@35172
   496
    qed have "\<And>l. ?p1 l \<noteq> {}" "\<And>l. ?p2 l \<noteq> {}" unfolding interval_eq_empty not_ex apply(rule_tac[!] allI)
himmelma@35172
   497
    proof- case goal1 thus ?case using abcd[of x] by auto
himmelma@35172
   498
    next   case goal2 thus ?case using abcd[of x] by auto
himmelma@35172
   499
    qed thus "k \<noteq> {}" using k by auto
himmelma@35172
   500
    show "\<exists>a b. k = {a..b}" using k by auto
himmelma@35172
   501
    fix k' assume k':"k' \<in> ?p" "k \<noteq> k'" then obtain l' where l':"k' = ?p1 l' \<or> k' = ?p2 l'" "l' \<in> {1..n + 1}" by auto
himmelma@35172
   502
    { fix k k' l l'
himmelma@35172
   503
      assume k:"k\<in>?p" and l:"k = ?p1 l \<or> k = ?p2 l" "l \<in> {1..n + 1}" 
himmelma@35172
   504
      assume k':"k' \<in> ?p" "k \<noteq> k'" and  l':"k' = ?p1 l' \<or> k' = ?p2 l'" "l' \<in> {1..n + 1}" 
himmelma@35172
   505
      assume "l \<le> l'" fix x
himmelma@35172
   506
      have "x \<notin> interior k \<inter> interior k'" 
himmelma@35172
   507
      proof(rule,cases "l' = n+1") assume x:"x \<in> interior k \<inter> interior k'"
hoelzl@37489
   508
        case True hence "\<And>i. i<DIM('a) \<Longrightarrow> \<pi>' i < l'" using \<pi>'i using l' by(auto simp add:less_Suc_eq_le)
hoelzl@37489
   509
        hence *:"\<And> P Q. (\<chi>\<chi> i. if \<pi>' i < l' then P i else Q i) = ((\<chi>\<chi> i. P i)::'a)" apply-apply(subst euclidean_eq) by auto
hoelzl@37489
   510
        hence k':"k' = {c..d}" using l'(1) unfolding * by auto
himmelma@35172
   511
        have ln:"l < n + 1" 
himmelma@35172
   512
        proof(rule ccontr) case goal1 hence l2:"l = n+1" using l by auto
hoelzl@37489
   513
          hence "\<And>i. i<DIM('a) \<Longrightarrow> \<pi>' i < l" using \<pi>'i by(auto simp add:less_Suc_eq_le)
hoelzl@37489
   514
          hence *:"\<And> P Q. (\<chi>\<chi> i. if \<pi>' i < l then P i else Q i) = ((\<chi>\<chi> i. P i)::'a)" apply-apply(subst euclidean_eq) by auto
hoelzl@37489
   515
          hence "k = {c..d}" using l(1) \<pi>'i unfolding * by(auto)
himmelma@35172
   516
          thus False using `k\<noteq>k'` k' by auto
himmelma@35172
   517
        qed have **:"\<pi>' (\<pi> l) = l" using \<pi>'\<pi>[of l] using l ln by auto
hoelzl@37489
   518
        have "x $$ \<pi> l < c $$ \<pi> l \<or> d $$ \<pi> l < x $$ \<pi> l" using l(1) apply-
himmelma@35172
   519
        proof(erule disjE)
himmelma@35172
   520
          assume as:"k = ?p1 l" note * = conjunct1[OF x[unfolded as Int_iff interior_closed_interval mem_interval],rule_format]
hoelzl@37489
   521
          show ?thesis using *[of "\<pi> l"] using ln l(2) using \<pi>i[of l] by(auto simp add:** not_less)
himmelma@35172
   522
        next assume as:"k = ?p2 l" note * = conjunct1[OF x[unfolded as Int_iff interior_closed_interval mem_interval],rule_format]
hoelzl@37489
   523
          show ?thesis using *[of "\<pi> l"] using ln l(2) using \<pi>i[of l] unfolding ** by auto
himmelma@35172
   524
        qed thus False using x unfolding k' unfolding Int_iff interior_closed_interval mem_interval
himmelma@35172
   525
          by(auto elim!:allE[where x="\<pi> l"])
himmelma@35172
   526
      next case False hence "l < n + 1" using l'(2) using `l\<le>l'` by auto
himmelma@35172
   527
        hence ln:"l \<in> {1..n}" "l' \<in> {1..n}" using l l' False by auto
himmelma@35172
   528
        note \<pi>l = \<pi>'\<pi>[OF ln(1)] \<pi>'\<pi>[OF ln(2)]
himmelma@35172
   529
        assume x:"x \<in> interior k \<inter> interior k'"
himmelma@35172
   530
        show False using l(1) l'(1) apply-
himmelma@35172
   531
        proof(erule_tac[!] disjE)+
himmelma@35172
   532
          assume as:"k = ?p1 l" "k' = ?p1 l'"
hoelzl@37489
   533
          note * = conjunctD2[OF x[unfolded as Int_iff interior_closed_interval mem_interval],rule_format]
himmelma@35172
   534
          have "l \<noteq> l'" using k'(2)[unfolded as] by auto
hoelzl@37489
   535
          thus False using *[of "\<pi> l'"] *[of "\<pi> l"] ln using \<pi>i[OF ln(1)] \<pi>i[OF ln(2)] apply(cases "l<l'")
hoelzl@37489
   536
            by(auto simp add:euclidean_lambda_beta' \<pi>l \<pi>i n_def)
himmelma@35172
   537
        next assume as:"k = ?p2 l" "k' = ?p2 l'"
himmelma@35172
   538
          note * = conjunctD2[OF x[unfolded as Int_iff interior_closed_interval mem_interval],rule_format]
himmelma@35172
   539
          have "l \<noteq> l'" apply(rule) using k'(2)[unfolded as] by auto
hoelzl@37489
   540
          thus False using *[of "\<pi> l"] *[of "\<pi> l'"]  `l \<le> l'` ln by(auto simp add:euclidean_lambda_beta' \<pi>l \<pi>i n_def)
himmelma@35172
   541
        next assume as:"k = ?p1 l" "k' = ?p2 l'"
himmelma@35172
   542
          note * = conjunctD2[OF x[unfolded as Int_iff interior_closed_interval mem_interval],rule_format]
hoelzl@37489
   543
          show False using abcd[of "\<pi> l'"] using *[of "\<pi> l"] *[of "\<pi> l'"]  `l \<le> l'` ln apply(cases "l=l'")
hoelzl@37489
   544
            by(auto simp add:euclidean_lambda_beta' \<pi>l \<pi>i n_def)
himmelma@35172
   545
        next assume as:"k = ?p2 l" "k' = ?p1 l'"
himmelma@35172
   546
          note * = conjunctD2[OF x[unfolded as Int_iff interior_closed_interval mem_interval],rule_format]
hoelzl@37489
   547
          show False using *[of "\<pi> l"] *[of "\<pi> l'"] ln `l \<le> l'` apply(cases "l=l'") using abcd[of "\<pi> l'"] 
hoelzl@37489
   548
            by(auto simp add:euclidean_lambda_beta' \<pi>l \<pi>i n_def)
himmelma@35172
   549
        qed qed } 
himmelma@35172
   550
    from this[OF k l k' l'] this[OF k'(1) l' k _ l] have "\<And>x. x \<notin> interior k \<inter> interior k'"
himmelma@35172
   551
      apply - apply(cases "l' \<le> l") using k'(2) by auto            
himmelma@35172
   552
    thus "interior k \<inter> interior k' = {}" by auto        
himmelma@35172
   553
qed qed
himmelma@35172
   554
himmelma@35172
   555
lemma partial_division_extend_interval: assumes "p division_of (\<Union>p)" "(\<Union>p) \<subseteq> {a..b}"
hoelzl@37489
   556
  obtains q where "p \<subseteq> q" "q division_of {a..b::'a::ordered_euclidean_space}" proof(cases "p = {}")
himmelma@35172
   557
  case True guess q apply(rule elementary_interval[of a b]) .
himmelma@35172
   558
  thus ?thesis apply- apply(rule that[of q]) unfolding True by auto next
himmelma@35172
   559
  case False note p = division_ofD[OF assms(1)]
himmelma@35172
   560
  have *:"\<forall>k\<in>p. \<exists>q. q division_of {a..b} \<and> k\<in>q" proof case goal1
himmelma@35172
   561
    guess c using p(4)[OF goal1] .. then guess d .. note cd_ = this
himmelma@35172
   562
    have *:"{c..d} \<subseteq> {a..b}" "{c..d} \<noteq> {}" using p(2,3)[OF goal1, unfolded cd_] using assms(2) by auto
himmelma@35172
   563
    guess q apply(rule partial_division_extend_1[OF *]) . thus ?case unfolding cd_ by auto qed
himmelma@35172
   564
  guess q using bchoice[OF *] .. note q = conjunctD2[OF this[rule_format]]
himmelma@35172
   565
  have "\<And>x. x\<in>p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x - {x})" apply(rule,rule_tac p="q x" in division_of_subset) proof-
himmelma@35172
   566
    fix x assume x:"x\<in>p" show "q x division_of \<Union>q x" apply-apply(rule division_ofI)
himmelma@35172
   567
      using division_ofD[OF q(1)[OF x]] by auto show "q x - {x} \<subseteq> q x" by auto qed
himmelma@35172
   568
  hence "\<exists>d. d division_of \<Inter> ((\<lambda>i. \<Union>(q i - {i})) ` p)" apply- apply(rule elementary_inters)
himmelma@35172
   569
    apply(rule finite_imageI[OF p(1)]) unfolding image_is_empty apply(rule False) by auto
himmelma@35172
   570
  then guess d .. note d = this
himmelma@35172
   571
  show ?thesis apply(rule that[of "d \<union> p"]) proof-
himmelma@35172
   572
    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
himmelma@35172
   573
    have *:"{a..b} = \<Inter> (\<lambda>i. \<Union>(q i - {i})) ` p \<union> \<Union>p" apply(rule *[OF False]) proof fix i assume i:"i\<in>p"
himmelma@35172
   574
      show "\<Union>(q i - {i}) \<union> i = {a..b}" using division_ofD(6)[OF q(1)[OF i]] using q(2)[OF i] by auto qed
himmelma@35172
   575
    show "d \<union> p division_of {a..b}" unfolding * apply(rule division_disjoint_union[OF d assms(1)])
himmelma@35172
   576
      apply(rule inter_interior_unions_intervals) apply(rule p open_interior ballI)+ proof(assumption,rule)
himmelma@35172
   577
      fix k assume k:"k\<in>p" have *:"\<And>u t s. u \<subseteq> s \<Longrightarrow> s \<inter> t = {} \<Longrightarrow> u \<inter> t = {}" by auto
himmelma@35172
   578
      show "interior (\<Inter>(\<lambda>i. \<Union>(q i - {i})) ` p) \<inter> interior k = {}" apply(rule *[of _ "interior (\<Union>(q k - {k}))"])
himmelma@35172
   579
	defer apply(subst Int_commute) apply(rule inter_interior_unions_intervals) proof- note qk=division_ofD[OF q(1)[OF k]]
himmelma@35172
   580
	show "finite (q k - {k})" "open (interior k)"  "\<forall>t\<in>q k - {k}. \<exists>a b. t = {a..b}" using qk by auto
himmelma@35172
   581
	show "\<forall>t\<in>q k - {k}. interior k \<inter> interior t = {}" using qk(5) using q(2)[OF k] by auto
himmelma@35172
   582
	have *:"\<And>x s. x \<in> s \<Longrightarrow> \<Inter>s \<subseteq> x" by auto show "interior (\<Inter>(\<lambda>i. \<Union>(q i - {i})) ` p) \<subseteq> interior (\<Union>(q k - {k}))"
himmelma@35172
   583
	  apply(rule subset_interior *)+ using k by auto qed qed qed auto qed
himmelma@35172
   584
hoelzl@37489
   585
lemma elementary_bounded[dest]: "p division_of s \<Longrightarrow> bounded (s::('a::ordered_euclidean_space) set)"
himmelma@35172
   586
  unfolding division_of_def by(metis bounded_Union bounded_interval) 
himmelma@35172
   587
hoelzl@37489
   588
lemma elementary_subset_interval: "p division_of s \<Longrightarrow> \<exists>a b. s \<subseteq> {a..b::'a::ordered_euclidean_space}"
himmelma@35172
   589
  by(meson elementary_bounded bounded_subset_closed_interval)
himmelma@35172
   590
hoelzl@37489
   591
lemma division_union_intervals_exists: assumes "{a..b::'a::ordered_euclidean_space} \<noteq> {}"
himmelma@35172
   592
  obtains p where "(insert {a..b} p) division_of ({a..b} \<union> {c..d})" proof(cases "{c..d} = {}")
himmelma@35172
   593
  case True show ?thesis apply(rule that[of "{}"]) unfolding True using assms by auto next
himmelma@35172
   594
  case False note false=this show ?thesis proof(cases "{a..b} \<inter> {c..d} = {}")
himmelma@35172
   595
  have *:"\<And>a b. {a,b} = {a} \<union> {b}" by auto
himmelma@35172
   596
  case True show ?thesis apply(rule that[of "{{c..d}}"]) unfolding * apply(rule division_disjoint_union)
himmelma@35172
   597
    using false True assms using interior_subset by auto next
himmelma@35172
   598
  case False obtain u v where uv:"{a..b} \<inter> {c..d} = {u..v}" unfolding inter_interval by auto
himmelma@35172
   599
  have *:"{u..v} \<subseteq> {c..d}" using uv by auto
himmelma@35172
   600
  guess p apply(rule partial_division_extend_1[OF * False[unfolded uv]]) . note p=this division_ofD[OF this(1)]
himmelma@35172
   601
  have *:"{a..b} \<union> {c..d} = {a..b} \<union> \<Union>(p - {{u..v}})" "\<And>x s. insert x s = {x} \<union> s" using p(8) unfolding uv[THEN sym] by auto
himmelma@35172
   602
  show thesis apply(rule that[of "p - {{u..v}}"]) unfolding *(1) apply(subst *(2)) apply(rule division_disjoint_union)
himmelma@35172
   603
    apply(rule,rule assms) apply(rule division_of_subset[of p]) apply(rule division_of_union_self[OF p(1)]) defer
himmelma@35172
   604
    unfolding interior_inter[THEN sym] proof-
himmelma@35172
   605
    have *:"\<And>cd p uv ab. p \<subseteq> cd \<Longrightarrow> ab \<inter> cd = uv \<Longrightarrow> ab \<inter> p = uv \<inter> p" by auto
himmelma@35172
   606
    have "interior ({a..b} \<inter> \<Union>(p - {{u..v}})) = interior({u..v} \<inter> \<Union>(p - {{u..v}}))" 
himmelma@35172
   607
      apply(rule arg_cong[of _ _ interior]) apply(rule *[OF _ uv]) using p(8) by auto
himmelma@35172
   608
    also have "\<dots> = {}" unfolding interior_inter apply(rule inter_interior_unions_intervals) using p(6) p(7)[OF p(2)] p(3) by auto
himmelma@35172
   609
    finally show "interior ({a..b} \<inter> \<Union>(p - {{u..v}})) = {}" by assumption qed auto qed qed
himmelma@35172
   610
himmelma@35172
   611
lemma division_of_unions: assumes "finite f"  "\<And>p. p\<in>f \<Longrightarrow> p division_of (\<Union>p)"
himmelma@35172
   612
  "\<And>k1 k2. \<lbrakk>k1 \<in> \<Union>f; k2 \<in> \<Union>f; k1 \<noteq> k2\<rbrakk> \<Longrightarrow> interior k1 \<inter> interior k2 = {}"
himmelma@35172
   613
  shows "\<Union>f division_of \<Union>\<Union>f" apply(rule division_ofI) prefer 5 apply(rule assms(3)|assumption)+
himmelma@35172
   614
  apply(rule finite_Union assms(1))+ prefer 3 apply(erule UnionE) apply(rule_tac s=X in division_ofD(3)[OF assms(2)])
himmelma@35172
   615
  using division_ofD[OF assms(2)] by auto
himmelma@35172
   616
  
himmelma@35172
   617
lemma elementary_union_interval: assumes "p division_of \<Union>p"
hoelzl@37489
   618
  obtains q where "q division_of ({a..b::'a::ordered_euclidean_space} \<union> \<Union>p)" proof-
himmelma@35172
   619
  note assm=division_ofD[OF assms]
himmelma@35172
   620
  have lem1:"\<And>f s. \<Union>\<Union> (f ` s) = \<Union>(\<lambda>x.\<Union>(f x)) ` s" by auto
himmelma@35172
   621
  have lem2:"\<And>f s. f \<noteq> {} \<Longrightarrow> \<Union>{s \<union> t |t. t \<in> f} = s \<union> \<Union>f" by auto
himmelma@35172
   622
{ presume "p={} \<Longrightarrow> thesis" "{a..b} = {} \<Longrightarrow> thesis" "{a..b} \<noteq> {} \<Longrightarrow> interior {a..b} = {} \<Longrightarrow> thesis"
himmelma@35172
   623
    "p\<noteq>{} \<Longrightarrow> interior {a..b}\<noteq>{} \<Longrightarrow> {a..b} \<noteq> {} \<Longrightarrow> thesis"
himmelma@35172
   624
  thus thesis by auto
himmelma@35172
   625
next assume as:"p={}" guess p apply(rule elementary_interval[of a b]) .
himmelma@35172
   626
  thus thesis apply(rule_tac that[of p]) unfolding as by auto 
himmelma@35172
   627
next assume as:"{a..b}={}" show thesis apply(rule that) unfolding as using assms by auto
himmelma@35172
   628
next assume as:"interior {a..b} = {}" "{a..b} \<noteq> {}"
himmelma@35172
   629
  show thesis apply(rule that[of "insert {a..b} p"],rule division_ofI)
himmelma@35172
   630
    unfolding finite_insert apply(rule assm(1)) unfolding Union_insert  
himmelma@35172
   631
    using assm(2-4) as apply- by(fastsimp dest: assm(5))+
himmelma@35172
   632
next assume as:"p \<noteq> {}" "interior {a..b} \<noteq> {}" "{a..b}\<noteq>{}"
himmelma@35172
   633
  have "\<forall>k\<in>p. \<exists>q. (insert {a..b} q) division_of ({a..b} \<union> k)" proof case goal1
himmelma@35172
   634
    from assm(4)[OF this] guess c .. then guess d ..
himmelma@35172
   635
    thus ?case apply-apply(rule division_union_intervals_exists[OF as(3),of c d]) by auto
himmelma@35172
   636
  qed from bchoice[OF this] guess q .. note q=division_ofD[OF this[rule_format]]
himmelma@35172
   637
  let ?D = "\<Union>{insert {a..b} (q k) | k. k \<in> p}"
himmelma@35172
   638
  show thesis apply(rule that[of "?D"]) proof(rule division_ofI)
himmelma@35172
   639
    have *:"{insert {a..b} (q k) |k. k \<in> p} = (\<lambda>k. insert {a..b} (q k)) ` p" by auto
himmelma@35172
   640
    show "finite ?D" apply(rule finite_Union) unfolding * apply(rule finite_imageI) using assm(1) q(1) by auto
himmelma@35172
   641
    show "\<Union>?D = {a..b} \<union> \<Union>p" unfolding * lem1 unfolding lem2[OF as(1), of "{a..b}",THEN sym]
himmelma@35172
   642
      using q(6) by auto
himmelma@35172
   643
    fix k assume k:"k\<in>?D" thus " k \<subseteq> {a..b} \<union> \<Union>p" using q(2) by auto
himmelma@35172
   644
    show "k \<noteq> {}" using q(3) k by auto show "\<exists>a b. k = {a..b}" using q(4) k by auto
himmelma@35172
   645
    fix k' assume k':"k'\<in>?D" "k\<noteq>k'"
himmelma@35172
   646
    obtain x  where x: "k \<in>insert {a..b} (q x)"  "x\<in>p"  using k  by auto
himmelma@35172
   647
    obtain x' where x':"k'\<in>insert {a..b} (q x')" "x'\<in>p" using k' by auto
himmelma@35172
   648
    show "interior k \<inter> interior k' = {}" proof(cases "x=x'")
himmelma@35172
   649
      case True show ?thesis apply(rule q(5)) using x x' k' unfolding True by auto
himmelma@35172
   650
    next case False 
himmelma@35172
   651
      { presume "k = {a..b} \<Longrightarrow> ?thesis" "k' = {a..b} \<Longrightarrow> ?thesis" 
himmelma@35172
   652
        "k \<noteq> {a..b} \<Longrightarrow> k' \<noteq> {a..b} \<Longrightarrow> ?thesis"
himmelma@35172
   653
        thus ?thesis by auto }
himmelma@35172
   654
      { assume as':"k  = {a..b}" show ?thesis apply(rule q(5)) using x' k'(2) unfolding as' by auto }
himmelma@35172
   655
      { assume as':"k' = {a..b}" show ?thesis apply(rule q(5)) using x  k'(2) unfolding as' by auto }
himmelma@35172
   656
      assume as':"k \<noteq> {a..b}" "k' \<noteq> {a..b}"
himmelma@35172
   657
      guess c using q(4)[OF x(2,1)] .. then guess d .. note c_d=this
himmelma@35172
   658
      have "interior k  \<inter> interior {a..b} = {}" apply(rule q(5)) using x  k'(2) using as' by auto
himmelma@35172
   659
      hence "interior k \<subseteq> interior x" apply-
himmelma@35172
   660
        apply(rule interior_subset_union_intervals[OF c_d _ as(2) q(2)[OF x(2,1)]]) by auto moreover
himmelma@35172
   661
      guess c using q(4)[OF x'(2,1)] .. then guess d .. note c_d=this
himmelma@35172
   662
      have "interior k' \<inter> interior {a..b} = {}" apply(rule q(5)) using x' k'(2) using as' by auto
himmelma@35172
   663
      hence "interior k' \<subseteq> interior x'" apply-
himmelma@35172
   664
        apply(rule interior_subset_union_intervals[OF c_d _ as(2) q(2)[OF x'(2,1)]]) by auto
himmelma@35172
   665
      ultimately show ?thesis using assm(5)[OF x(2) x'(2) False] by auto
himmelma@35172
   666
    qed qed } qed
himmelma@35172
   667
himmelma@35172
   668
lemma elementary_unions_intervals:
hoelzl@37489
   669
  assumes "finite f" "\<And>s. s \<in> f \<Longrightarrow> \<exists>a b. s = {a..b::'a::ordered_euclidean_space}"
himmelma@35172
   670
  obtains p where "p division_of (\<Union>f)" proof-
himmelma@35172
   671
  have "\<exists>p. p division_of (\<Union>f)" proof(induct_tac f rule:finite_subset_induct) 
himmelma@35172
   672
    show "\<exists>p. p division_of \<Union>{}" using elementary_empty by auto
himmelma@35172
   673
    fix x F assume as:"finite F" "x \<notin> F" "\<exists>p. p division_of \<Union>F" "x\<in>f"
himmelma@35172
   674
    from this(3) guess p .. note p=this
himmelma@35172
   675
    from assms(2)[OF as(4)] guess a .. then guess b .. note ab=this
himmelma@35172
   676
    have *:"\<Union>F = \<Union>p" using division_ofD[OF p] by auto
himmelma@35172
   677
    show "\<exists>p. p division_of \<Union>insert x F" using elementary_union_interval[OF p[unfolded *], of a b]
himmelma@35172
   678
      unfolding Union_insert ab * by auto
himmelma@35172
   679
  qed(insert assms,auto) thus ?thesis apply-apply(erule exE,rule that) by auto qed
himmelma@35172
   680
hoelzl@37489
   681
lemma elementary_union: assumes "ps division_of s" "pt division_of (t::('a::ordered_euclidean_space) set)"
himmelma@35172
   682
  obtains p where "p division_of (s \<union> t)"
himmelma@35172
   683
proof- have "s \<union> t = \<Union>ps \<union> \<Union>pt" using assms unfolding division_of_def by auto
himmelma@35172
   684
  hence *:"\<Union>(ps \<union> pt) = s \<union> t" by auto
himmelma@35172
   685
  show ?thesis apply-apply(rule elementary_unions_intervals[of "ps\<union>pt"])
himmelma@35172
   686
    unfolding * prefer 3 apply(rule_tac p=p in that)
himmelma@35172
   687
    using assms[unfolded division_of_def] by auto qed
himmelma@35172
   688
hoelzl@37489
   689
lemma partial_division_extend: fixes t::"('a::ordered_euclidean_space) set"
himmelma@35172
   690
  assumes "p division_of s" "q division_of t" "s \<subseteq> t"
himmelma@35172
   691
  obtains r where "p \<subseteq> r" "r division_of t" proof-
himmelma@35172
   692
  note divp = division_ofD[OF assms(1)] and divq = division_ofD[OF assms(2)]
himmelma@35172
   693
  obtain a b where ab:"t\<subseteq>{a..b}" using elementary_subset_interval[OF assms(2)] by auto
himmelma@35172
   694
  guess r1 apply(rule partial_division_extend_interval) apply(rule assms(1)[unfolded divp(6)[THEN sym]])
himmelma@35172
   695
    apply(rule subset_trans) by(rule ab assms[unfolded divp(6)[THEN sym]])+  note r1 = this division_ofD[OF this(2)]
himmelma@35172
   696
  guess p' apply(rule elementary_unions_intervals[of "r1 - p"]) using r1(3,6) by auto 
himmelma@35172
   697
  then obtain r2 where r2:"r2 division_of (\<Union>(r1 - p)) \<inter> (\<Union>q)" 
himmelma@35172
   698
    apply- apply(drule elementary_inter[OF _ assms(2)[unfolded divq(6)[THEN sym]]]) by auto
himmelma@35172
   699
  { fix x assume x:"x\<in>t" "x\<notin>s"
himmelma@35172
   700
    hence "x\<in>\<Union>r1" unfolding r1 using ab by auto
himmelma@35172
   701
    then guess r unfolding Union_iff .. note r=this moreover
himmelma@35172
   702
    have "r \<notin> p" proof assume "r\<in>p" hence "x\<in>s" using divp(2) r by auto
himmelma@35172
   703
      thus False using x by auto qed
himmelma@35172
   704
    ultimately have "x\<in>\<Union>(r1 - p)" by auto }
himmelma@35172
   705
  hence *:"t = \<Union>p \<union> (\<Union>(r1 - p) \<inter> \<Union>q)" unfolding divp divq using assms(3) by auto
himmelma@35172
   706
  show ?thesis apply(rule that[of "p \<union> r2"]) unfolding * defer apply(rule division_disjoint_union)
himmelma@35172
   707
    unfolding divp(6) apply(rule assms r2)+
himmelma@35172
   708
  proof- have "interior s \<inter> interior (\<Union>(r1-p)) = {}"
himmelma@35172
   709
    proof(rule inter_interior_unions_intervals)
himmelma@35172
   710
      show "finite (r1 - p)" "open (interior s)" "\<forall>t\<in>r1-p. \<exists>a b. t = {a..b}" using r1 by auto
himmelma@35172
   711
      have *:"\<And>s. (\<And>x. x \<in> s \<Longrightarrow> False) \<Longrightarrow> s = {}" by auto
himmelma@35172
   712
      show "\<forall>t\<in>r1-p. interior s \<inter> interior t = {}" proof(rule)
himmelma@35172
   713
        fix m x assume as:"m\<in>r1-p"
himmelma@35172
   714
        have "interior m \<inter> interior (\<Union>p) = {}" proof(rule inter_interior_unions_intervals)
himmelma@35172
   715
          show "finite p" "open (interior m)" "\<forall>t\<in>p. \<exists>a b. t = {a..b}" using divp by auto
himmelma@35172
   716
          show "\<forall>t\<in>p. interior m \<inter> interior t = {}" apply(rule, rule r1(7)) using as using r1 by auto
himmelma@35172
   717
        qed thus "interior s \<inter> interior m = {}" unfolding divp by auto
himmelma@35172
   718
      qed qed        
himmelma@35172
   719
    thus "interior s \<inter> interior (\<Union>(r1-p) \<inter> (\<Union>q)) = {}" using interior_subset by auto
himmelma@35172
   720
  qed auto qed
himmelma@35172
   721
himmelma@35172
   722
subsection {* Tagged (partial) divisions. *}
himmelma@35172
   723
himmelma@35172
   724
definition tagged_partial_division_of (infixr "tagged'_partial'_division'_of" 40) where
himmelma@35172
   725
  "(s tagged_partial_division_of i) \<equiv>
himmelma@35172
   726
        finite s \<and>
himmelma@35172
   727
        (\<forall>x k. (x,k) \<in> s \<longrightarrow> x \<in> k \<and> k \<subseteq> i \<and> (\<exists>a b. k = {a..b})) \<and>
himmelma@35172
   728
        (\<forall>x1 k1 x2 k2. (x1,k1) \<in> s \<and> (x2,k2) \<in> s \<and> ((x1,k1) \<noteq> (x2,k2))
himmelma@35172
   729
                       \<longrightarrow> (interior(k1) \<inter> interior(k2) = {}))"
himmelma@35172
   730
himmelma@35172
   731
lemma tagged_partial_division_ofD[dest]: assumes "s tagged_partial_division_of i"
himmelma@35172
   732
  shows "finite s" "\<And>x k. (x,k) \<in> s \<Longrightarrow> x \<in> k" "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> i"
himmelma@35172
   733
  "\<And>x k. (x,k) \<in> s \<Longrightarrow> \<exists>a b. k = {a..b}"
himmelma@35172
   734
  "\<And>x1 k1 x2 k2. (x1,k1) \<in> s \<Longrightarrow> (x2,k2) \<in> s \<Longrightarrow> (x1,k1) \<noteq> (x2,k2) \<Longrightarrow> interior(k1) \<inter> interior(k2) = {}"
himmelma@35172
   735
  using assms unfolding tagged_partial_division_of_def  apply- by blast+ 
himmelma@35172
   736
himmelma@35172
   737
definition tagged_division_of (infixr "tagged'_division'_of" 40) where
himmelma@35172
   738
  "(s tagged_division_of i) \<equiv>
himmelma@35172
   739
        (s tagged_partial_division_of i) \<and> (\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
himmelma@35172
   740
himmelma@35172
   741
lemma tagged_division_of_finite[dest]: "s tagged_division_of i \<Longrightarrow> finite s"
himmelma@35172
   742
  unfolding tagged_division_of_def tagged_partial_division_of_def by auto
himmelma@35172
   743
himmelma@35172
   744
lemma tagged_division_of:
himmelma@35172
   745
 "(s tagged_division_of i) \<longleftrightarrow>
himmelma@35172
   746
        finite s \<and>
himmelma@35172
   747
        (\<forall>x k. (x,k) \<in> s
himmelma@35172
   748
               \<longrightarrow> x \<in> k \<and> k \<subseteq> i \<and> (\<exists>a b. k = {a..b})) \<and>
himmelma@35172
   749
        (\<forall>x1 k1 x2 k2. (x1,k1) \<in> s \<and> (x2,k2) \<in> s \<and> ~((x1,k1) = (x2,k2))
himmelma@35172
   750
                       \<longrightarrow> (interior(k1) \<inter> interior(k2) = {})) \<and>
himmelma@35172
   751
        (\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
himmelma@35172
   752
  unfolding tagged_division_of_def tagged_partial_division_of_def by auto
himmelma@35172
   753
himmelma@35172
   754
lemma tagged_division_ofI: assumes
himmelma@35172
   755
  "finite s" "\<And>x k. (x,k) \<in> s \<Longrightarrow> x \<in> k" "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> i"  "\<And>x k. (x,k) \<in> s \<Longrightarrow> \<exists>a b. k = {a..b}"
himmelma@35172
   756
  "\<And>x1 k1 x2 k2. (x1,k1) \<in> s \<Longrightarrow> (x2,k2) \<in> s \<Longrightarrow> ~((x1,k1) = (x2,k2)) \<Longrightarrow> (interior(k1) \<inter> interior(k2) = {})"
himmelma@35172
   757
  "(\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
himmelma@35172
   758
  shows "s tagged_division_of i"
himmelma@35172
   759
  unfolding tagged_division_of apply(rule) defer apply rule
himmelma@35172
   760
  apply(rule allI impI conjI assms)+ apply assumption
himmelma@35172
   761
  apply(rule, rule assms, assumption) apply(rule assms, assumption)
himmelma@35172
   762
  using assms(1,5-) apply- by blast+
himmelma@35172
   763
himmelma@35172
   764
lemma tagged_division_ofD[dest]: assumes "s tagged_division_of i"
himmelma@35172
   765
  shows "finite s" "\<And>x k. (x,k) \<in> s \<Longrightarrow> x \<in> k" "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> i"  "\<And>x k. (x,k) \<in> s \<Longrightarrow> \<exists>a b. k = {a..b}"
himmelma@35172
   766
  "\<And>x1 k1 x2 k2. (x1,k1) \<in> s \<Longrightarrow> (x2,k2) \<in> s \<Longrightarrow> ~((x1,k1) = (x2,k2)) \<Longrightarrow> (interior(k1) \<inter> interior(k2) = {})"
himmelma@35172
   767
  "(\<Union>{k. \<exists>x. (x,k) \<in> s} = i)" using assms unfolding tagged_division_of apply- by blast+
himmelma@35172
   768
himmelma@35172
   769
lemma division_of_tagged_division: assumes"s tagged_division_of i"  shows "(snd ` s) division_of i"
himmelma@35172
   770
proof(rule division_ofI) note assm=tagged_division_ofD[OF assms]
himmelma@35172
   771
  show "\<Union>snd ` s = i" "finite (snd ` s)" using assm by auto
himmelma@35172
   772
  fix k assume k:"k \<in> snd ` s" then obtain xk where xk:"(xk, k) \<in> s" by auto
himmelma@35172
   773
  thus  "k \<subseteq> i" "k \<noteq> {}" "\<exists>a b. k = {a..b}" using assm apply- by fastsimp+
himmelma@35172
   774
  fix k' assume k':"k' \<in> snd ` s" "k \<noteq> k'" from this(1) obtain xk' where xk':"(xk', k') \<in> s" by auto
himmelma@35172
   775
  thus "interior k \<inter> interior k' = {}" apply-apply(rule assm(5)) apply(rule xk xk')+ using k' by auto
himmelma@35172
   776
qed
himmelma@35172
   777
himmelma@35172
   778
lemma partial_division_of_tagged_division: assumes "s tagged_partial_division_of i"
himmelma@35172
   779
  shows "(snd ` s) division_of \<Union>(snd ` s)"
himmelma@35172
   780
proof(rule division_ofI) note assm=tagged_partial_division_ofD[OF assms]
himmelma@35172
   781
  show "finite (snd ` s)" "\<Union>snd ` s = \<Union>snd ` s" using assm by auto
himmelma@35172
   782
  fix k assume k:"k \<in> snd ` s" then obtain xk where xk:"(xk, k) \<in> s" by auto
himmelma@35172
   783
  thus "k\<noteq>{}" "\<exists>a b. k = {a..b}" "k \<subseteq> \<Union>snd ` s" using assm by auto
himmelma@35172
   784
  fix k' assume k':"k' \<in> snd ` s" "k \<noteq> k'" from this(1) obtain xk' where xk':"(xk', k') \<in> s" by auto
himmelma@35172
   785
  thus "interior k \<inter> interior k' = {}" apply-apply(rule assm(5)) apply(rule xk xk')+ using k' by auto
himmelma@35172
   786
qed
himmelma@35172
   787
himmelma@35172
   788
lemma tagged_partial_division_subset: assumes "s tagged_partial_division_of i" "t \<subseteq> s"
himmelma@35172
   789
  shows "t tagged_partial_division_of i"
himmelma@35172
   790
  using assms unfolding tagged_partial_division_of_def using finite_subset[OF assms(2)] by blast
himmelma@35172
   791
hoelzl@37489
   792
lemma setsum_over_tagged_division_lemma: fixes d::"('m::ordered_euclidean_space) set \<Rightarrow> 'a::real_normed_vector"
himmelma@35172
   793
  assumes "p tagged_division_of i" "\<And>u v. {u..v} \<noteq> {} \<Longrightarrow> content {u..v} = 0 \<Longrightarrow> d {u..v} = 0"
himmelma@35172
   794
  shows "setsum (\<lambda>(x,k). d k) p = setsum d (snd ` p)"
himmelma@35172
   795
proof- note assm=tagged_division_ofD[OF assms(1)]
himmelma@35172
   796
  have *:"(\<lambda>(x,k). d k) = d \<circ> snd" unfolding o_def apply(rule ext) by auto
himmelma@35172
   797
  show ?thesis unfolding * apply(subst eq_commute) proof(rule setsum_reindex_nonzero)
himmelma@35172
   798
    show "finite p" using assm by auto
himmelma@35172
   799
    fix x y assume as:"x\<in>p" "y\<in>p" "x\<noteq>y" "snd x = snd y" 
himmelma@35172
   800
    obtain a b where ab:"snd x = {a..b}" using assm(4)[of "fst x" "snd x"] as(1) by auto
himmelma@35172
   801
    have "(fst x, snd y) \<in> p" "(fst x, snd y) \<noteq> y" unfolding as(4)[THEN sym] using as(1-3) by auto
himmelma@35172
   802
    hence "interior (snd x) \<inter> interior (snd y) = {}" apply-apply(rule assm(5)[of "fst x" _ "fst y"]) using as by auto 
himmelma@35172
   803
    hence "content {a..b} = 0" unfolding as(4)[THEN sym] ab content_eq_0_interior by auto
himmelma@35172
   804
    hence "d {a..b} = 0" apply-apply(rule assms(2)) using assm(2)[of "fst x" "snd x"] as(1) unfolding ab[THEN sym] by auto
himmelma@35172
   805
    thus "d (snd x) = 0" unfolding ab by auto qed qed
himmelma@35172
   806
himmelma@35172
   807
lemma tag_in_interval: "p tagged_division_of i \<Longrightarrow> (x,k) \<in> p \<Longrightarrow> x \<in> i" by auto
himmelma@35172
   808
himmelma@35172
   809
lemma tagged_division_of_empty: "{} tagged_division_of {}"
himmelma@35172
   810
  unfolding tagged_division_of by auto
himmelma@35172
   811
himmelma@35172
   812
lemma tagged_partial_division_of_trivial[simp]:
himmelma@35172
   813
 "p tagged_partial_division_of {} \<longleftrightarrow> p = {}"
himmelma@35172
   814
  unfolding tagged_partial_division_of_def by auto
himmelma@35172
   815
himmelma@35172
   816
lemma tagged_division_of_trivial[simp]:
himmelma@35172
   817
 "p tagged_division_of {} \<longleftrightarrow> p = {}"
himmelma@35172
   818
  unfolding tagged_division_of by auto
himmelma@35172
   819
himmelma@35172
   820
lemma tagged_division_of_self:
himmelma@35172
   821
 "x \<in> {a..b} \<Longrightarrow> {(x,{a..b})} tagged_division_of {a..b}"
himmelma@35172
   822
  apply(rule tagged_division_ofI) by auto
himmelma@35172
   823
himmelma@35172
   824
lemma tagged_division_union:
himmelma@35172
   825
  assumes "p1 tagged_division_of s1"  "p2 tagged_division_of s2" "interior s1 \<inter> interior s2 = {}"
himmelma@35172
   826
  shows "(p1 \<union> p2) tagged_division_of (s1 \<union> s2)"
himmelma@35172
   827
proof(rule tagged_division_ofI) note p1=tagged_division_ofD[OF assms(1)] and p2=tagged_division_ofD[OF assms(2)]
himmelma@35172
   828
  show "finite (p1 \<union> p2)" using p1(1) p2(1) by auto
himmelma@35172
   829
  show "\<Union>{k. \<exists>x. (x, k) \<in> p1 \<union> p2} = s1 \<union> s2" using p1(6) p2(6) by blast
himmelma@35172
   830
  fix x k assume xk:"(x,k)\<in>p1\<union>p2" show "x\<in>k" "\<exists>a b. k = {a..b}" using xk p1(2,4) p2(2,4) by auto
himmelma@35172
   831
  show "k\<subseteq>s1\<union>s2" using xk p1(3) p2(3) by blast
himmelma@35172
   832
  fix x' k' assume xk':"(x',k')\<in>p1\<union>p2" "(x,k) \<noteq> (x',k')"
himmelma@35172
   833
  have *:"\<And>a b. a\<subseteq> s1 \<Longrightarrow> b\<subseteq> s2 \<Longrightarrow> interior a \<inter> interior b = {}" using assms(3) subset_interior by blast
himmelma@35172
   834
  show "interior k \<inter> interior k' = {}" apply(cases "(x,k)\<in>p1", case_tac[!] "(x',k')\<in>p1")
himmelma@35172
   835
    apply(rule p1(5)) prefer 4 apply(rule *) prefer 6 apply(subst Int_commute,rule *) prefer 8 apply(rule p2(5))
himmelma@35172
   836
    using p1(3) p2(3) using xk xk' by auto qed 
himmelma@35172
   837
himmelma@35172
   838
lemma tagged_division_unions:
himmelma@35172
   839
  assumes "finite iset" "\<forall>i\<in>iset. (pfn(i) tagged_division_of i)"
himmelma@35172
   840
  "\<forall>i1 \<in> iset. \<forall>i2 \<in> iset. ~(i1 = i2) \<longrightarrow> (interior(i1) \<inter> interior(i2) = {})"
himmelma@35172
   841
  shows "\<Union>(pfn ` iset) tagged_division_of (\<Union>iset)"
himmelma@35172
   842
proof(rule tagged_division_ofI)
himmelma@35172
   843
  note assm = tagged_division_ofD[OF assms(2)[rule_format]]
himmelma@35172
   844
  show "finite (\<Union>pfn ` iset)" apply(rule finite_Union) using assms by auto
himmelma@35172
   845
  have "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>pfn ` iset} = \<Union>(\<lambda>i. \<Union>{k. \<exists>x. (x, k) \<in> pfn i}) ` iset" by blast 
himmelma@35172
   846
  also have "\<dots> = \<Union>iset" using assm(6) by auto
himmelma@35172
   847
  finally show "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>pfn ` iset} = \<Union>iset" . 
himmelma@35172
   848
  fix x k assume xk:"(x,k)\<in>\<Union>pfn ` iset" then obtain i where i:"i \<in> iset" "(x, k) \<in> pfn i" by auto
himmelma@35172
   849
  show "x\<in>k" "\<exists>a b. k = {a..b}" "k \<subseteq> \<Union>iset" using assm(2-4)[OF i] using i(1) by auto
himmelma@35172
   850
  fix x' k' assume xk':"(x',k')\<in>\<Union>pfn ` iset" "(x, k) \<noteq> (x', k')" then obtain i' where i':"i' \<in> iset" "(x', k') \<in> pfn i'" by auto
himmelma@35172
   851
  have *:"\<And>a b. i\<noteq>i' \<Longrightarrow> a\<subseteq> i \<Longrightarrow> b\<subseteq> i' \<Longrightarrow> interior a \<inter> interior b = {}" using i(1) i'(1)
himmelma@35172
   852
    using assms(3)[rule_format] subset_interior by blast
himmelma@35172
   853
  show "interior k \<inter> interior k' = {}" apply(cases "i=i'")
himmelma@35172
   854
    using assm(5)[OF i _ xk'(2)]  i'(2) using assm(3)[OF i] assm(3)[OF i'] defer apply-apply(rule *) by auto
himmelma@35172
   855
qed
himmelma@35172
   856
himmelma@35172
   857
lemma tagged_partial_division_of_union_self:
himmelma@35172
   858
  assumes "p tagged_partial_division_of s" shows "p tagged_division_of (\<Union>(snd ` p))"
himmelma@35172
   859
  apply(rule tagged_division_ofI) using tagged_partial_division_ofD[OF assms] by auto
himmelma@35172
   860
himmelma@35172
   861
lemma tagged_division_of_union_self: assumes "p tagged_division_of s"
himmelma@35172
   862
  shows "p tagged_division_of (\<Union>(snd ` p))"
himmelma@35172
   863
  apply(rule tagged_division_ofI) using tagged_division_ofD[OF assms] by auto
himmelma@35172
   864
himmelma@35172
   865
subsection {* Fine-ness of a partition w.r.t. a gauge. *}
himmelma@35172
   866
himmelma@35172
   867
definition fine (infixr "fine" 46) where
himmelma@35172
   868
  "d fine s \<longleftrightarrow> (\<forall>(x,k) \<in> s. k \<subseteq> d(x))"
himmelma@35172
   869
himmelma@35172
   870
lemma fineI: assumes "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> d x"
himmelma@35172
   871
  shows "d fine s" using assms unfolding fine_def by auto
himmelma@35172
   872
himmelma@35172
   873
lemma fineD[dest]: assumes "d fine s"
himmelma@35172
   874
  shows "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> d x" using assms unfolding fine_def by auto
himmelma@35172
   875
himmelma@35172
   876
lemma fine_inter: "(\<lambda>x. d1 x \<inter> d2 x) fine p \<longleftrightarrow> d1 fine p \<and> d2 fine p"
himmelma@35172
   877
  unfolding fine_def by auto
himmelma@35172
   878
himmelma@35172
   879
lemma fine_inters:
himmelma@35172
   880
 "(\<lambda>x. \<Inter> {f d x | d.  d \<in> s}) fine p \<longleftrightarrow> (\<forall>d\<in>s. (f d) fine p)"
himmelma@35172
   881
  unfolding fine_def by blast
himmelma@35172
   882
himmelma@35172
   883
lemma fine_union:
himmelma@35172
   884
  "d fine p1 \<Longrightarrow> d fine p2 \<Longrightarrow> d fine (p1 \<union> p2)"
himmelma@35172
   885
  unfolding fine_def by blast
himmelma@35172
   886
himmelma@35172
   887
lemma fine_unions:"(\<And>p. p \<in> ps \<Longrightarrow> d fine p) \<Longrightarrow> d fine (\<Union>ps)"
himmelma@35172
   888
  unfolding fine_def by auto
himmelma@35172
   889
himmelma@35172
   890
lemma fine_subset:  "p \<subseteq> q \<Longrightarrow> d fine q \<Longrightarrow> d fine p"
himmelma@35172
   891
  unfolding fine_def by blast
himmelma@35172
   892
himmelma@35172
   893
subsection {* Gauge integral. Define on compact intervals first, then use a limit. *}
himmelma@35172
   894
himmelma@35172
   895
definition has_integral_compact_interval (infixr "has'_integral'_compact'_interval" 46) where
himmelma@35172
   896
  "(f has_integral_compact_interval y) i \<equiv>
himmelma@35172
   897
        (\<forall>e>0. \<exists>d. gauge d \<and>
himmelma@35172
   898
          (\<forall>p. p tagged_division_of i \<and> d fine p
himmelma@35172
   899
                        \<longrightarrow> norm(setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - y) < e))"
himmelma@35172
   900
himmelma@35172
   901
definition has_integral (infixr "has'_integral" 46) where 
hoelzl@37489
   902
"((f::('n::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector)) has_integral y) i \<equiv>
himmelma@35172
   903
        if (\<exists>a b. i = {a..b}) then (f has_integral_compact_interval y) i
himmelma@35172
   904
        else (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> {a..b}
himmelma@35172
   905
              \<longrightarrow> (\<exists>z. ((\<lambda>x. if x \<in> i then f x else 0) has_integral_compact_interval z) {a..b} \<and>
himmelma@35172
   906
                                       norm(z - y) < e))"
himmelma@35172
   907
himmelma@35172
   908
lemma has_integral:
himmelma@35172
   909
 "(f has_integral y) ({a..b}) \<longleftrightarrow>
himmelma@35172
   910
        (\<forall>e>0. \<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {a..b} \<and> d fine p
himmelma@35172
   911
                        \<longrightarrow> norm(setsum (\<lambda>(x,k). content(k) *\<^sub>R f x) p - y) < e))"
himmelma@35172
   912
  unfolding has_integral_def has_integral_compact_interval_def by auto
himmelma@35172
   913
himmelma@35172
   914
lemma has_integralD[dest]: assumes
himmelma@35172
   915
 "(f has_integral y) ({a..b})" "e>0"
himmelma@35172
   916
  obtains d where "gauge d" "\<And>p. p tagged_division_of {a..b} \<Longrightarrow> d fine p
himmelma@35172
   917
                        \<Longrightarrow> norm(setsum (\<lambda>(x,k). content(k) *\<^sub>R f(x)) p - y) < e"
himmelma@35172
   918
  using assms unfolding has_integral by auto
himmelma@35172
   919
himmelma@35172
   920
lemma has_integral_alt:
himmelma@35172
   921
 "(f has_integral y) i \<longleftrightarrow>
himmelma@35172
   922
      (if (\<exists>a b. i = {a..b}) then (f has_integral y) i
himmelma@35172
   923
       else (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> {a..b}
himmelma@35172
   924
                               \<longrightarrow> (\<exists>z. ((\<lambda>x. if x \<in> i then f(x) else 0)
himmelma@35172
   925
                                        has_integral z) ({a..b}) \<and>
himmelma@35172
   926
                                       norm(z - y) < e)))"
himmelma@35172
   927
  unfolding has_integral unfolding has_integral_compact_interval_def has_integral_def by auto
himmelma@35172
   928
himmelma@35172
   929
lemma has_integral_altD:
himmelma@35172
   930
  assumes "(f has_integral y) i" "\<not> (\<exists>a b. i = {a..b})" "e>0"
himmelma@35172
   931
  obtains B where "B>0" "\<forall>a b. ball 0 B \<subseteq> {a..b}\<longrightarrow> (\<exists>z. ((\<lambda>x. if x \<in> i then f(x) else 0) has_integral z) ({a..b}) \<and> norm(z - y) < e)"
himmelma@35172
   932
  using assms unfolding has_integral unfolding has_integral_compact_interval_def has_integral_def by auto
himmelma@35172
   933
himmelma@35172
   934
definition integrable_on (infixr "integrable'_on" 46) where
himmelma@35172
   935
  "(f integrable_on i) \<equiv> \<exists>y. (f has_integral y) i"
himmelma@35172
   936
himmelma@35172
   937
definition "integral i f \<equiv> SOME y. (f has_integral y) i"
himmelma@35172
   938
himmelma@35172
   939
lemma integrable_integral[dest]:
himmelma@35172
   940
 "f integrable_on i \<Longrightarrow> (f has_integral (integral i f)) i"
himmelma@35172
   941
  unfolding integrable_on_def integral_def by(rule someI_ex)
himmelma@35172
   942
himmelma@35172
   943
lemma has_integral_integrable[intro]: "(f has_integral i) s \<Longrightarrow> f integrable_on s"
himmelma@35172
   944
  unfolding integrable_on_def by auto
himmelma@35172
   945
himmelma@35172
   946
lemma has_integral_integral:"f integrable_on s \<longleftrightarrow> (f has_integral (integral s f)) s"
himmelma@35172
   947
  by auto
himmelma@35172
   948
himmelma@35172
   949
lemma setsum_content_null:
himmelma@35172
   950
  assumes "content({a..b}) = 0" "p tagged_division_of {a..b}"
himmelma@35172
   951
  shows "setsum (\<lambda>(x,k). content k *\<^sub>R f x) p = (0::'a::real_normed_vector)"
himmelma@35172
   952
proof(rule setsum_0',rule) fix y assume y:"y\<in>p"
himmelma@35172
   953
  obtain x k where xk:"y = (x,k)" using surj_pair[of y] by blast
himmelma@35172
   954
  note assm = tagged_division_ofD(3-4)[OF assms(2) y[unfolded xk]]
himmelma@35172
   955
  from this(2) guess c .. then guess d .. note c_d=this
himmelma@35172
   956
  have "(\<lambda>(x, k). content k *\<^sub>R f x) y = content k *\<^sub>R f x" unfolding xk by auto
himmelma@35172
   957
  also have "\<dots> = 0" using content_subset[OF assm(1)[unfolded c_d]] content_pos_le[of c d]
himmelma@35172
   958
    unfolding assms(1) c_d by auto
himmelma@35172
   959
  finally show "(\<lambda>(x, k). content k *\<^sub>R f x) y = 0" .
himmelma@35172
   960
qed
himmelma@35172
   961
himmelma@35172
   962
subsection {* Some basic combining lemmas. *}
himmelma@35172
   963
himmelma@35172
   964
lemma tagged_division_unions_exists:
himmelma@35172
   965
  assumes "finite iset" "\<forall>i \<in> iset. \<exists>p. p tagged_division_of i \<and> d fine p"
himmelma@35172
   966
  "\<forall>i1\<in>iset. \<forall>i2\<in>iset. ~(i1 = i2) \<longrightarrow> (interior(i1) \<inter> interior(i2) = {})" "(\<Union>iset = i)"
himmelma@35172
   967
   obtains p where "p tagged_division_of i" "d fine p"
himmelma@35172
   968
proof- guess pfn using bchoice[OF assms(2)] .. note pfn = conjunctD2[OF this[rule_format]]
himmelma@35172
   969
  show thesis apply(rule_tac p="\<Union>(pfn ` iset)" in that) unfolding assms(4)[THEN sym]
himmelma@35172
   970
    apply(rule tagged_division_unions[OF assms(1) _ assms(3)]) defer 
himmelma@35172
   971
    apply(rule fine_unions) using pfn by auto
himmelma@35172
   972
qed
himmelma@35172
   973
himmelma@35172
   974
subsection {* The set we're concerned with must be closed. *}
himmelma@35172
   975
hoelzl@37489
   976
lemma division_of_closed: "s division_of i \<Longrightarrow> closed (i::('n::ordered_euclidean_space) set)"
himmelma@35172
   977
  unfolding division_of_def by(fastsimp intro!: closed_Union closed_interval)
himmelma@35172
   978
himmelma@35172
   979
subsection {* General bisection principle for intervals; might be useful elsewhere. *}
himmelma@35172
   980
hoelzl@37489
   981
lemma interval_bisection_step:  fixes type::"'a::ordered_euclidean_space"
hoelzl@37489
   982
  assumes "P {}" "(\<forall>s t. P s \<and> P t \<and> interior(s) \<inter> interior(t) = {} \<longrightarrow> P(s \<union> t))" "~(P {a..b::'a})"
himmelma@35172
   983
  obtains c d where "~(P{c..d})"
hoelzl@37489
   984
  "\<forall>i<DIM('a). a$$i \<le> c$$i \<and> c$$i \<le> d$$i \<and> d$$i \<le> b$$i \<and> 2 * (d$$i - c$$i) \<le> b$$i - a$$i"
himmelma@35172
   985
proof- have "{a..b} \<noteq> {}" using assms(1,3) by auto
himmelma@35172
   986
  note ab=this[unfolded interval_eq_empty not_ex not_less]
himmelma@35172
   987
  { fix f have "finite f \<Longrightarrow>
himmelma@35172
   988
        (\<forall>s\<in>f. P s) \<Longrightarrow>
himmelma@35172
   989
        (\<forall>s\<in>f. \<exists>a b. s = {a..b}) \<Longrightarrow>
himmelma@35172
   990
        (\<forall>s\<in>f.\<forall>t\<in>f. ~(s = t) \<longrightarrow> interior(s) \<inter> interior(t) = {}) \<Longrightarrow> P(\<Union>f)"
himmelma@35172
   991
    proof(induct f rule:finite_induct)
himmelma@35172
   992
      case empty show ?case using assms(1) by auto
himmelma@35172
   993
    next case (insert x f) show ?case unfolding Union_insert apply(rule assms(2)[rule_format])
himmelma@35172
   994
        apply rule defer apply rule defer apply(rule inter_interior_unions_intervals)
himmelma@35172
   995
        using insert by auto
himmelma@35172
   996
    qed } note * = this
hoelzl@37489
   997
  let ?A = "{{c..d} | c d::'a. \<forall>i<DIM('a). (c$$i = a$$i) \<and> (d$$i = (a$$i + b$$i) / 2) \<or> (c$$i = (a$$i + b$$i) / 2) \<and> (d$$i = b$$i)}"
hoelzl@37489
   998
  let ?PP = "\<lambda>c d. \<forall>i<DIM('a). a$$i \<le> c$$i \<and> c$$i \<le> d$$i \<and> d$$i \<le> b$$i \<and> 2 * (d$$i - c$$i) \<le> b$$i - a$$i"
himmelma@35172
   999
  { presume "\<forall>c d. ?PP c d \<longrightarrow> P {c..d} \<Longrightarrow> False"
himmelma@35172
  1000
    thus thesis unfolding atomize_not not_all apply-apply(erule exE)+ apply(rule_tac c=x and d=xa in that) by auto }
himmelma@35172
  1001
  assume as:"\<forall>c d. ?PP c d \<longrightarrow> P {c..d}"
himmelma@35172
  1002
  have "P (\<Union> ?A)" proof(rule *, rule_tac[2-] ballI, rule_tac[4] ballI, rule_tac[4] impI) 
hoelzl@37489
  1003
    let ?B = "(\<lambda>s.{(\<chi>\<chi> i. if i \<in> s then a$$i else (a$$i + b$$i) / 2)::'a ..
hoelzl@37489
  1004
      (\<chi>\<chi> i. if i \<in> s then (a$$i + b$$i) / 2 else b$$i)}) ` {s. s \<subseteq> {..<DIM('a)}}"
himmelma@35172
  1005
    have "?A \<subseteq> ?B" proof case goal1
himmelma@35172
  1006
      then guess c unfolding mem_Collect_eq .. then guess d apply- by(erule exE,(erule conjE)+) note c_d=this[rule_format]
himmelma@35172
  1007
      have *:"\<And>a b c d. a = c \<Longrightarrow> b = d \<Longrightarrow> {a..b} = {c..d}" by auto
hoelzl@37489
  1008
      show "x\<in>?B" unfolding image_iff apply(rule_tac x="{i. i<DIM('a) \<and> c$$i = a$$i}" in bexI)
hoelzl@37489
  1009
        unfolding c_d apply(rule * ) unfolding euclidean_eq[where 'a='a] apply safe unfolding euclidean_lambda_beta' mem_Collect_eq
hoelzl@37489
  1010
      proof- fix i assume "i<DIM('a)" thus " c $$ i = (if i < DIM('a) \<and> c $$ i = a $$ i then a $$ i else (a $$ i + b $$ i) / 2)"
hoelzl@37489
  1011
          "d $$ i = (if i < DIM('a) \<and> c $$ i = a $$ i then (a $$ i + b $$ i) / 2 else b $$ i)"
himmelma@35172
  1012
          using c_d(2)[of i] ab[THEN spec[where x=i]] by(auto simp add:field_simps)
hoelzl@37489
  1013
      qed qed
hoelzl@37489
  1014
    thus "finite ?A" apply(rule finite_subset) by auto
himmelma@35172
  1015
    fix s assume "s\<in>?A" then guess c unfolding mem_Collect_eq .. then guess d apply- by(erule exE,(erule conjE)+)
himmelma@35172
  1016
    note c_d=this[rule_format]
hoelzl@37489
  1017
    show "P s" unfolding c_d apply(rule as[rule_format]) proof- case goal1 thus ?case 
himmelma@35172
  1018
        using c_d(2)[of i] using ab[THEN spec[where x=i]] by auto qed
himmelma@35172
  1019
    show "\<exists>a b. s = {a..b}" unfolding c_d by auto
himmelma@35172
  1020
    fix t assume "t\<in>?A" then guess e unfolding mem_Collect_eq .. then guess f apply- by(erule exE,(erule conjE)+)
himmelma@35172
  1021
    note e_f=this[rule_format]
himmelma@35172
  1022
    assume "s \<noteq> t" hence "\<not> (c = e \<and> d = f)" unfolding c_d e_f by auto
hoelzl@37489
  1023
    then obtain i where "c$$i \<noteq> e$$i \<or> d$$i \<noteq> f$$i" and i':"i<DIM('a)" unfolding de_Morgan_conj euclidean_eq[where 'a='a] by auto
hoelzl@37489
  1024
    hence i:"c$$i \<noteq> e$$i" "d$$i \<noteq> f$$i" apply- apply(erule_tac[!] disjE)
hoelzl@37489
  1025
    proof- assume "c$$i \<noteq> e$$i" thus "d$$i \<noteq> f$$i" using c_d(2)[of i] e_f(2)[of i] by fastsimp
hoelzl@37489
  1026
    next   assume "d$$i \<noteq> f$$i" thus "c$$i \<noteq> e$$i" using c_d(2)[of i] e_f(2)[of i] by fastsimp
himmelma@35172
  1027
    qed have *:"\<And>s t. (\<And>a. a\<in>s \<Longrightarrow> a\<in>t \<Longrightarrow> False) \<Longrightarrow> s \<inter> t = {}" by auto
himmelma@35172
  1028
    show "interior s \<inter> interior t = {}" unfolding e_f c_d interior_closed_interval proof(rule *)
himmelma@35172
  1029
      fix x assume "x\<in>{c<..<d}" "x\<in>{e<..<f}"
hoelzl@37489
  1030
      hence x:"c$$i < d$$i" "e$$i < f$$i" "c$$i < f$$i" "e$$i < d$$i" unfolding mem_interval using i'
hoelzl@37489
  1031
        apply-apply(erule_tac[!] x=i in allE)+ by auto
hoelzl@37489
  1032
      show False using c_d(2)[OF i'] apply- apply(erule_tac disjE)
hoelzl@37489
  1033
      proof(erule_tac[!] conjE) assume as:"c $$ i = a $$ i" "d $$ i = (a $$ i + b $$ i) / 2"
himmelma@35172
  1034
        show False using e_f(2)[of i] and i x unfolding as by(fastsimp simp add:field_simps)
hoelzl@37489
  1035
      next assume as:"c $$ i = (a $$ i + b $$ i) / 2" "d $$ i = b $$ i"
himmelma@35172
  1036
        show False using e_f(2)[of i] and i x unfolding as by(fastsimp simp add:field_simps)
himmelma@35172
  1037
      qed qed qed
himmelma@35172
  1038
  also have "\<Union> ?A = {a..b}" proof(rule set_ext,rule)
himmelma@35172
  1039
    fix x assume "x\<in>\<Union>?A" then guess Y unfolding Union_iff ..
himmelma@35172
  1040
    from this(1) guess c unfolding mem_Collect_eq .. then guess d ..
himmelma@35172
  1041
    note c_d = this[THEN conjunct2,rule_format] `x\<in>Y`[unfolded this[THEN conjunct1]]
hoelzl@37489
  1042
    show "x\<in>{a..b}" unfolding mem_interval proof safe
hoelzl@37489
  1043
      fix i assume "i<DIM('a)" thus "a $$ i \<le> x $$ i" "x $$ i \<le> b $$ i"
himmelma@35172
  1044
        using c_d(1)[of i] c_d(2)[unfolded mem_interval,THEN spec[where x=i]] by auto qed
himmelma@35172
  1045
  next fix x assume x:"x\<in>{a..b}"
hoelzl@37489
  1046
    have "\<forall>i<DIM('a). \<exists>c d. (c = a$$i \<and> d = (a$$i + b$$i) / 2 \<or> c = (a$$i + b$$i) / 2 \<and> d = b$$i) \<and> c\<le>x$$i \<and> x$$i \<le> d"
hoelzl@37489
  1047
      (is "\<forall>i<DIM('a). \<exists>c d. ?P i c d") unfolding mem_interval proof(rule,rule) fix i
hoelzl@37489
  1048
      have "?P i (a$$i) ((a $$ i + b $$ i) / 2) \<or> ?P i ((a $$ i + b $$ i) / 2) (b$$i)"
himmelma@35172
  1049
        using x[unfolded mem_interval,THEN spec[where x=i]] by auto thus "\<exists>c d. ?P i c d" by blast
hoelzl@37489
  1050
    qed thus "x\<in>\<Union>?A" unfolding Union_iff unfolding lambda_skolem' unfolding Bex_def mem_Collect_eq
himmelma@35172
  1051
      apply-apply(erule exE)+ apply(rule_tac x="{xa..xaa}" in exI) unfolding mem_interval by auto
himmelma@35172
  1052
  qed finally show False using assms by auto qed
himmelma@35172
  1053
hoelzl@37489
  1054
lemma interval_bisection: fixes type::"'a::ordered_euclidean_space"
hoelzl@37489
  1055
  assumes "P {}" "(\<forall>s t. P s \<and> P t \<and> interior(s) \<inter> interior(t) = {} \<longrightarrow> P(s \<union> t))" "\<not> P {a..b::'a}"
himmelma@35172
  1056
  obtains x where "x \<in> {a..b}" "\<forall>e>0. \<exists>c d. x \<in> {c..d} \<and> {c..d} \<subseteq> ball x e \<and> {c..d} \<subseteq> {a..b} \<and> ~P({c..d})"
himmelma@35172
  1057
proof-
hoelzl@37489
  1058
  have "\<forall>x. \<exists>y. \<not> P {fst x..snd x} \<longrightarrow> (\<not> P {fst y..snd y} \<and>
hoelzl@37489
  1059
    (\<forall>i<DIM('a). fst x$$i \<le> fst y$$i \<and> fst y$$i \<le> snd y$$i \<and> snd y$$i \<le> snd x$$i \<and>
hoelzl@37489
  1060
                           2 * (snd y$$i - fst y$$i) \<le> snd x$$i - fst x$$i))" proof case goal1 thus ?case proof-
himmelma@35172
  1061
      presume "\<not> P {fst x..snd x} \<Longrightarrow> ?thesis"
himmelma@35172
  1062
      thus ?thesis apply(cases "P {fst x..snd x}") by auto
himmelma@35172
  1063
    next assume as:"\<not> P {fst x..snd x}" from interval_bisection_step[of P, OF assms(1-2) as] guess c d . 
himmelma@35172
  1064
      thus ?thesis apply- apply(rule_tac x="(c,d)" in exI) by auto
himmelma@35172
  1065
    qed qed then guess f apply-apply(drule choice) by(erule exE) note f=this
himmelma@35172
  1066
  def AB \<equiv> "\<lambda>n. (f ^^ n) (a,b)" def A \<equiv> "\<lambda>n. fst(AB n)" and B \<equiv> "\<lambda>n. snd(AB n)" note ab_def = this AB_def
himmelma@35172
  1067
  have "A 0 = a" "B 0 = b" "\<And>n. \<not> P {A(Suc n)..B(Suc n)} \<and>
hoelzl@37489
  1068
    (\<forall>i<DIM('a). A(n)$$i \<le> A(Suc n)$$i \<and> A(Suc n)$$i \<le> B(Suc n)$$i \<and> B(Suc n)$$i \<le> B(n)$$i \<and> 
hoelzl@37489
  1069
    2 * (B(Suc n)$$i - A(Suc n)$$i) \<le> B(n)$$i - A(n)$$i)" (is "\<And>n. ?P n")
himmelma@35172
  1070
  proof- show "A 0 = a" "B 0 = b" unfolding ab_def by auto
himmelma@35172
  1071
    case goal3 note S = ab_def funpow.simps o_def id_apply show ?case
himmelma@35172
  1072
    proof(induct n) case 0 thus ?case unfolding S apply(rule f[rule_format]) using assms(3) by auto
himmelma@35172
  1073
    next case (Suc n) show ?case unfolding S apply(rule f[rule_format]) using Suc unfolding S by auto
himmelma@35172
  1074
    qed qed note AB = this(1-2) conjunctD2[OF this(3),rule_format]
himmelma@35172
  1075
himmelma@35172
  1076
  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"
hoelzl@37489
  1077
  proof- case goal1 guess n using real_arch_pow2[of "(setsum (\<lambda>i. b$$i - a$$i) {..<DIM('a)}) / e"] .. note n=this
himmelma@35172
  1078
    show ?case apply(rule_tac x=n in exI) proof(rule,rule)
himmelma@35172
  1079
      fix x y assume xy:"x\<in>{A n..B n}" "y\<in>{A n..B n}"
hoelzl@37489
  1080
      have "dist x y \<le> setsum (\<lambda>i. abs((x - y)$$i)) {..<DIM('a)}" unfolding dist_norm by(rule norm_le_l1)
hoelzl@37489
  1081
      also have "\<dots> \<le> setsum (\<lambda>i. B n$$i - A n$$i) {..<DIM('a)}"
hoelzl@37489
  1082
      proof(rule setsum_mono) fix i show "\<bar>(x - y) $$ i\<bar> \<le> B n $$ i - A n $$ i"
hoelzl@37489
  1083
          using xy[unfolded mem_interval,THEN spec[where x=i]] by auto qed
hoelzl@37489
  1084
      also have "\<dots> \<le> setsum (\<lambda>i. b$$i - a$$i) {..<DIM('a)} / 2^n" unfolding setsum_divide_distrib
himmelma@35172
  1085
      proof(rule setsum_mono) case goal1 thus ?case
himmelma@35172
  1086
        proof(induct n) case 0 thus ?case unfolding AB by auto
hoelzl@37489
  1087
        next case (Suc n) have "B (Suc n) $$ i - A (Suc n) $$ i \<le> (B n $$ i - A n $$ i) / 2"
hoelzl@37489
  1088
            using AB(4)[of i n] using goal1 by auto
hoelzl@37489
  1089
          also have "\<dots> \<le> (b $$ i - a $$ i) / 2 ^ Suc n" using Suc by(auto simp add:field_simps) finally show ?case .
himmelma@35172
  1090
        qed qed
himmelma@35172
  1091
      also have "\<dots> < e" using n using goal1 by(auto simp add:field_simps) finally show "dist x y < e" .
himmelma@35172
  1092
    qed qed
himmelma@35172
  1093
  { fix n m ::nat assume "m \<le> n" then guess d unfolding le_Suc_ex_iff .. note d=this
himmelma@35172
  1094
    have "{A n..B n} \<subseteq> {A m..B m}" unfolding d 
himmelma@35172
  1095
    proof(induct d) case 0 thus ?case by auto
himmelma@35172
  1096
    next case (Suc d) show ?case apply(rule subset_trans[OF _ Suc])
himmelma@35172
  1097
        apply(rule) unfolding mem_interval apply(rule,erule_tac x=i in allE)
hoelzl@37489
  1098
      proof- case goal1 thus ?case using AB(4)[of i "m + d"] by(auto simp add:field_simps)
himmelma@35172
  1099
      qed qed } note ABsubset = this 
himmelma@35172
  1100
  have "\<exists>a. \<forall>n. a\<in>{A n..B n}" apply(rule decreasing_closed_nest[rule_format,OF closed_interval _ ABsubset interv])
himmelma@35172
  1101
  proof- fix n show "{A n..B n} \<noteq> {}" apply(cases "0<n") using AB(3)[of "n - 1"] assms(1,3) AB(1-2) by auto qed auto
himmelma@35172
  1102
  then guess x0 .. note x0=this[rule_format]
himmelma@35172
  1103
  show thesis proof(rule that[rule_format,of x0])
himmelma@35172
  1104
    show "x0\<in>{a..b}" using x0[of 0] unfolding AB .
himmelma@35172
  1105
    fix e assume "0 < (e::real)" from interv[OF this] guess n .. note n=this
himmelma@35172
  1106
    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}"
himmelma@35172
  1107
      apply(rule_tac x="A n" in exI,rule_tac x="B n" in exI) apply(rule,rule x0) apply rule defer 
himmelma@35172
  1108
    proof show "\<not> P {A n..B n}" apply(cases "0<n") using AB(3)[of "n - 1"] assms(3) AB(1-2) by auto
himmelma@35172
  1109
      show "{A n..B n} \<subseteq> ball x0 e" using n using x0[of n] by auto
himmelma@35172
  1110
      show "{A n..B n} \<subseteq> {a..b}" unfolding AB(1-2)[symmetric] apply(rule ABsubset) by auto
himmelma@35172
  1111
    qed qed qed 
himmelma@35172
  1112
himmelma@35172
  1113
subsection {* Cousin's lemma. *}
himmelma@35172
  1114
himmelma@35172
  1115
lemma fine_division_exists: assumes "gauge g" 
hoelzl@37489
  1116
  obtains p where "p tagged_division_of {a..b::'a::ordered_euclidean_space}" "g fine p"
himmelma@35172
  1117
proof- presume "\<not> (\<exists>p. p tagged_division_of {a..b} \<and> g fine p) \<Longrightarrow> False"
himmelma@35172
  1118
  then guess p unfolding atomize_not not_not .. thus thesis apply-apply(rule that[of p]) by auto
himmelma@35172
  1119
next assume as:"\<not> (\<exists>p. p tagged_division_of {a..b} \<and> g fine p)"
himmelma@35172
  1120
  guess x apply(rule interval_bisection[of "\<lambda>s. \<exists>p. p tagged_division_of s \<and> g fine p",rule_format,OF _ _ as])
himmelma@35172
  1121
    apply(rule_tac x="{}" in exI) defer apply(erule conjE exE)+
himmelma@35172
  1122
  proof- show "{} tagged_division_of {} \<and> g fine {}" unfolding fine_def by auto
himmelma@35172
  1123
    fix s t p p' assume "p tagged_division_of s" "g fine p" "p' tagged_division_of t" "g fine p'" "interior s \<inter> interior t = {}"
himmelma@35172
  1124
    thus "\<exists>p. p tagged_division_of s \<union> t \<and> g fine p" apply-apply(rule_tac x="p \<union> p'" in exI) apply rule
himmelma@35172
  1125
      apply(rule tagged_division_union) prefer 4 apply(rule fine_union) by auto
himmelma@35172
  1126
  qed note x=this
himmelma@35172
  1127
  obtain e where e:"e>0" "ball x e \<subseteq> g x" using gaugeD[OF assms, of x] unfolding open_contains_ball by auto
himmelma@35172
  1128
  from x(2)[OF e(1)] guess c d apply-apply(erule exE conjE)+ . note c_d = this
himmelma@35172
  1129
  have "g fine {(x, {c..d})}" unfolding fine_def using e using c_d(2) by auto
himmelma@35172
  1130
  thus False using tagged_division_of_self[OF c_d(1)] using c_d by auto qed
himmelma@35172
  1131
himmelma@35172
  1132
subsection {* Basic theorems about integrals. *}
himmelma@35172
  1133
hoelzl@37489
  1134
lemma has_integral_unique: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::real_normed_vector"
himmelma@35172
  1135
  assumes "(f has_integral k1) i" "(f has_integral k2) i" shows "k1 = k2"
himmelma@35172
  1136
proof(rule ccontr) let ?e = "norm(k1 - k2) / 2" assume as:"k1 \<noteq> k2" hence e:"?e > 0" by auto
hoelzl@37489
  1137
  have lem:"\<And>f::'n \<Rightarrow> 'a.  \<And> a b k1 k2.
himmelma@35172
  1138
    (f has_integral k1) ({a..b}) \<Longrightarrow> (f has_integral k2) ({a..b}) \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> False"
himmelma@35172
  1139
  proof- case goal1 let ?e = "norm(k1 - k2) / 2" from goal1(3) have e:"?e > 0" by auto
himmelma@35172
  1140
    guess d1 by(rule has_integralD[OF goal1(1) e]) note d1=this
himmelma@35172
  1141
    guess d2 by(rule has_integralD[OF goal1(2) e]) note d2=this
himmelma@35172
  1142
    guess p by(rule fine_division_exists[OF gauge_inter[OF d1(1) d2(1)],of a b]) note p=this
himmelma@35172
  1143
    let ?c = "(\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)" have "norm (k1 - k2) \<le> norm (?c - k2) + norm (?c - k1)"
haftmann@36350
  1144
      using norm_triangle_ineq4[of "k1 - ?c" "k2 - ?c"] by(auto simp add:algebra_simps norm_minus_commute)
himmelma@35172
  1145
    also have "\<dots> < norm (k1 - k2) / 2 + norm (k1 - k2) / 2"
himmelma@35172
  1146
      apply(rule add_strict_mono) apply(rule_tac[!] d2(2) d1(2)) using p unfolding fine_def by auto
himmelma@35172
  1147
    finally show False by auto
himmelma@35172
  1148
  qed { presume "\<not> (\<exists>a b. i = {a..b}) \<Longrightarrow> False"
himmelma@35172
  1149
    thus False apply-apply(cases "\<exists>a b. i = {a..b}")
himmelma@35172
  1150
      using assms by(auto simp add:has_integral intro:lem[OF _ _ as]) }
himmelma@35172
  1151
  assume as:"\<not> (\<exists>a b. i = {a..b})"
himmelma@35172
  1152
  guess B1 by(rule has_integral_altD[OF assms(1) as,OF e]) note B1=this[rule_format]
himmelma@35172
  1153
  guess B2 by(rule has_integral_altD[OF assms(2) as,OF e]) note B2=this[rule_format]
hoelzl@37489
  1154
  have "\<exists>a b::'n. ball 0 B1 \<union> ball 0 B2 \<subseteq> {a..b}" apply(rule bounded_subset_closed_interval)
himmelma@35172
  1155
    using bounded_Un bounded_ball by auto then guess a b apply-by(erule exE)+
himmelma@35172
  1156
  note ab=conjunctD2[OF this[unfolded Un_subset_iff]]
himmelma@35172
  1157
  guess w using B1(2)[OF ab(1)] .. note w=conjunctD2[OF this]
himmelma@35172
  1158
  guess z using B2(2)[OF ab(2)] .. note z=conjunctD2[OF this]
himmelma@35172
  1159
  have "z = w" using lem[OF w(1) z(1)] by auto
himmelma@35172
  1160
  hence "norm (k1 - k2) \<le> norm (z - k2) + norm (w - k1)"
himmelma@35172
  1161
    using norm_triangle_ineq4[of "k1 - w" "k2 - z"] by(auto simp add: norm_minus_commute) 
himmelma@35172
  1162
  also have "\<dots> < norm (k1 - k2) / 2 + norm (k1 - k2) / 2" apply(rule add_strict_mono) by(rule_tac[!] z(2) w(2))
himmelma@35172
  1163
  finally show False by auto qed
himmelma@35172
  1164
himmelma@35172
  1165
lemma integral_unique[intro]:
himmelma@35172
  1166
  "(f has_integral y) k \<Longrightarrow> integral k f = y"
himmelma@35172
  1167
  unfolding integral_def apply(rule some_equality) by(auto intro: has_integral_unique) 
himmelma@35172
  1168
hoelzl@37489
  1169
lemma has_integral_is_0: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::real_normed_vector" 
himmelma@35172
  1170
  assumes "\<forall>x\<in>s. f x = 0" shows "(f has_integral 0) s"
hoelzl@37489
  1171
proof- have lem:"\<And>a b. \<And>f::'n \<Rightarrow> 'a.
himmelma@35172
  1172
    (\<forall>x\<in>{a..b}. f(x) = 0) \<Longrightarrow> (f has_integral 0) ({a..b})" unfolding has_integral
hoelzl@37489
  1173
  proof(rule,rule) fix a b e and f::"'n \<Rightarrow> 'a"
himmelma@35172
  1174
    assume as:"\<forall>x\<in>{a..b}. f x = 0" "0 < (e::real)"
himmelma@35172
  1175
    show "\<exists>d. gauge d \<and> (\<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)"
himmelma@35172
  1176
      apply(rule_tac x="\<lambda>x. ball x 1" in exI)  apply(rule,rule gaugeI) unfolding centre_in_ball defer apply(rule open_ball)
himmelma@35172
  1177
    proof(rule,rule,erule conjE) case goal1
himmelma@35172
  1178
      have "(\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) = 0" proof(rule setsum_0',rule)
himmelma@35172
  1179
        fix x assume x:"x\<in>p" have "f (fst x) = 0" using tagged_division_ofD(2-3)[OF goal1(1), of "fst x" "snd x"] using as x by auto
himmelma@35172
  1180
        thus "(\<lambda>(x, k). content k *\<^sub>R f x) x = 0" apply(subst surjective_pairing[of x]) unfolding split_conv by auto
himmelma@35172
  1181
      qed thus ?case using as by auto
himmelma@35172
  1182
    qed auto qed  { presume "\<not> (\<exists>a b. s = {a..b}) \<Longrightarrow> ?thesis"
himmelma@35172
  1183
    thus ?thesis apply-apply(cases "\<exists>a b. s = {a..b}")
himmelma@35172
  1184
      using assms by(auto simp add:has_integral intro:lem) }
himmelma@35172
  1185
  have *:"(\<lambda>x. if x \<in> s then f x else 0) = (\<lambda>x. 0)" apply(rule ext) using assms by auto
himmelma@35172
  1186
  assume "\<not> (\<exists>a b. s = {a..b})" thus ?thesis apply(subst has_integral_alt) unfolding if_not_P *
himmelma@35172
  1187
  apply(rule,rule,rule_tac x=1 in exI,rule) defer apply(rule,rule,rule)
himmelma@35172
  1188
  proof- fix e::real and a b assume "e>0"
hoelzl@37489
  1189
    thus "\<exists>z. ((\<lambda>x::'n. 0::'a) has_integral z) {a..b} \<and> norm (z - 0) < e"
himmelma@35172
  1190
      apply(rule_tac x=0 in exI) apply(rule,rule lem) by auto
himmelma@35172
  1191
  qed auto qed
himmelma@35172
  1192
hoelzl@37489
  1193
lemma has_integral_0[simp]: "((\<lambda>x::'n::ordered_euclidean_space. 0) has_integral 0) s"
himmelma@35172
  1194
  apply(rule has_integral_is_0) by auto 
himmelma@35172
  1195
himmelma@35172
  1196
lemma has_integral_0_eq[simp]: "((\<lambda>x. 0) has_integral i) s \<longleftrightarrow> i = 0"
himmelma@35172
  1197
  using has_integral_unique[OF has_integral_0] by auto
himmelma@35172
  1198
hoelzl@37489
  1199
lemma has_integral_linear: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::real_normed_vector"
himmelma@35172
  1200
  assumes "(f has_integral y) s" "bounded_linear h" shows "((h o f) has_integral ((h y))) s"
himmelma@35172
  1201
proof- interpret bounded_linear h using assms(2) . from pos_bounded guess B .. note B=conjunctD2[OF this,rule_format]
hoelzl@37489
  1202
  have lem:"\<And>f::'n \<Rightarrow> 'a. \<And> y a b.
himmelma@35172
  1203
    (f has_integral y) ({a..b}) \<Longrightarrow> ((h o f) has_integral h(y)) ({a..b})"
himmelma@35172
  1204
  proof(subst has_integral,rule,rule) case goal1
himmelma@35172
  1205
    from pos_bounded guess B .. note B=conjunctD2[OF this,rule_format]
himmelma@35172
  1206
    have *:"e / B > 0" apply(rule divide_pos_pos) using goal1(2) B by auto
himmelma@35172
  1207
    guess g using has_integralD[OF goal1(1) *] . note g=this
himmelma@35172
  1208
    show ?case apply(rule_tac x=g in exI) apply(rule,rule g(1))
himmelma@35172
  1209
    proof(rule,rule,erule conjE) fix p assume as:"p tagged_division_of {a..b}" "g fine p" 
himmelma@35172
  1210
      have *:"\<And>x k. h ((\<lambda>(x, k). content k *\<^sub>R f x) x) = (\<lambda>(x, k). h (content k *\<^sub>R f x)) x" by auto
himmelma@35172
  1211
      have "(\<Sum>(x, k)\<in>p. content k *\<^sub>R (h \<circ> f) x) = setsum (h \<circ> (\<lambda>(x, k). content k *\<^sub>R f x)) p"
himmelma@35172
  1212
        unfolding o_def unfolding scaleR[THEN sym] * by simp
himmelma@35172
  1213
      also have "\<dots> = h (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)" using setsum[of "\<lambda>(x,k). content k *\<^sub>R f x" p] using as by auto
himmelma@35172
  1214
      finally have *:"(\<Sum>(x, k)\<in>p. content k *\<^sub>R (h \<circ> f) x) = h (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)" .
himmelma@35172
  1215
      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (h \<circ> f) x) - h y) < e" unfolding * diff[THEN sym]
himmelma@35172
  1216
        apply(rule le_less_trans[OF B(2)]) using g(2)[OF as] B(1) by(auto simp add:field_simps)
himmelma@35172
  1217
    qed qed { presume "\<not> (\<exists>a b. s = {a..b}) \<Longrightarrow> ?thesis"
himmelma@35172
  1218
    thus ?thesis apply-apply(cases "\<exists>a b. s = {a..b}") using assms by(auto simp add:has_integral intro!:lem) }
himmelma@35172
  1219
  assume as:"\<not> (\<exists>a b. s = {a..b})" thus ?thesis apply(subst has_integral_alt) unfolding if_not_P
himmelma@35172
  1220
  proof(rule,rule) fix e::real  assume e:"0<e"
himmelma@35172
  1221
    have *:"0 < e/B" by(rule divide_pos_pos,rule e,rule B(1))
himmelma@35172
  1222
    guess M using has_integral_altD[OF assms(1) as *,rule_format] . note M=this
himmelma@35172
  1223
    show "\<exists>B>0. \<forall>a b. ball 0 B \<subseteq> {a..b} \<longrightarrow> (\<exists>z. ((\<lambda>x. if x \<in> s then (h \<circ> f) x else 0) has_integral z) {a..b} \<and> norm (z - h y) < e)"
himmelma@35172
  1224
      apply(rule_tac x=M in exI) apply(rule,rule M(1))
himmelma@35172
  1225
    proof(rule,rule,rule) case goal1 guess z using M(2)[OF goal1(1)] .. note z=conjunctD2[OF this]
himmelma@35172
  1226
      have *:"(\<lambda>x. if x \<in> s then (h \<circ> f) x else 0) = h \<circ> (\<lambda>x. if x \<in> s then f x else 0)"
himmelma@35172
  1227
        unfolding o_def apply(rule ext) using zero by auto
himmelma@35172
  1228
      show ?case apply(rule_tac x="h z" in exI,rule) unfolding * apply(rule lem[OF z(1)]) unfolding diff[THEN sym]
himmelma@35172
  1229
        apply(rule le_less_trans[OF B(2)]) using B(1) z(2) by(auto simp add:field_simps)
himmelma@35172
  1230
    qed qed qed
himmelma@35172
  1231
himmelma@35172
  1232
lemma has_integral_cmul:
himmelma@35172
  1233
  shows "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_integral (c *\<^sub>R k)) s"
himmelma@35172
  1234
  unfolding o_def[THEN sym] apply(rule has_integral_linear,assumption)
himmelma@35172
  1235
  by(rule scaleR.bounded_linear_right)
himmelma@35172
  1236
himmelma@35172
  1237
lemma has_integral_neg:
himmelma@35172
  1238
  shows "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. -(f x)) has_integral (-k)) s"
himmelma@35172
  1239
  apply(drule_tac c="-1" in has_integral_cmul) by auto
himmelma@35172
  1240
hoelzl@37489
  1241
lemma has_integral_add: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::real_normed_vector" 
himmelma@35172
  1242
  assumes "(f has_integral k) s" "(g has_integral l) s"
himmelma@35172
  1243
  shows "((\<lambda>x. f x + g x) has_integral (k + l)) s"
hoelzl@37489
  1244
proof- have lem:"\<And>f g::'n \<Rightarrow> 'a. \<And>a b k l.
himmelma@35172
  1245
    (f has_integral k) ({a..b}) \<Longrightarrow> (g has_integral l) ({a..b}) \<Longrightarrow>
himmelma@35172
  1246
     ((\<lambda>x. f(x) + g(x)) has_integral (k + l)) ({a..b})" proof- case goal1
himmelma@35172
  1247
    show ?case unfolding has_integral proof(rule,rule) fix e::real assume e:"e>0" hence *:"e/2>0" by auto
himmelma@35172
  1248
      guess d1 using has_integralD[OF goal1(1) *] . note d1=this
himmelma@35172
  1249
      guess d2 using has_integralD[OF goal1(2) *] . note d2=this
himmelma@35172
  1250
      show "\<exists>d. gauge d \<and> (\<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 + g x)) - (k + l)) < e)"
himmelma@35172
  1251
        apply(rule_tac x="\<lambda>x. (d1 x) \<inter> (d2 x)" in exI) apply(rule,rule gauge_inter[OF d1(1) d2(1)])
himmelma@35172
  1252
      proof(rule,rule,erule conjE) fix p assume as:"p tagged_division_of {a..b}" "(\<lambda>x. d1 x \<inter> d2 x) fine p"
himmelma@35172
  1253
        have *:"(\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) = (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p. content k *\<^sub>R g x)"
himmelma@35172
  1254
          unfolding scaleR_right_distrib setsum_addf[of "\<lambda>(x,k). content k *\<^sub>R f x" "\<lambda>(x,k). content k *\<^sub>R g x" p,THEN sym]
himmelma@35172
  1255
          by(rule setsum_cong2,auto)
himmelma@35172
  1256
        have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) - (k + l)) = norm (((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k) + ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - l))"
haftmann@36350
  1257
          unfolding * by(auto simp add:algebra_simps) also let ?res = "\<dots>"
himmelma@35172
  1258
        from as have *:"d1 fine p" "d2 fine p" unfolding fine_inter by auto
himmelma@35172
  1259
        have "?res < e/2 + e/2" apply(rule le_less_trans[OF norm_triangle_ineq])
himmelma@35172
  1260
          apply(rule add_strict_mono) using d1(2)[OF as(1) *(1)] and d2(2)[OF as(1) *(2)] by auto
himmelma@35172
  1261
        finally show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) - (k + l)) < e" by auto
himmelma@35172
  1262
      qed qed qed { presume "\<not> (\<exists>a b. s = {a..b}) \<Longrightarrow> ?thesis"
himmelma@35172
  1263
    thus ?thesis apply-apply(cases "\<exists>a b. s = {a..b}") using assms by(auto simp add:has_integral intro!:lem) }
himmelma@35172
  1264
  assume as:"\<not> (\<exists>a b. s = {a..b})" thus ?thesis apply(subst has_integral_alt) unfolding if_not_P
himmelma@35172
  1265
  proof(rule,rule) case goal1 hence *:"e/2 > 0" by auto
himmelma@35172
  1266
    from has_integral_altD[OF assms(1) as *] guess B1 . note B1=this[rule_format]
himmelma@35172
  1267
    from has_integral_altD[OF assms(2) as *] guess B2 . note B2=this[rule_format]
himmelma@35172
  1268
    show ?case apply(rule_tac x="max B1 B2" in exI) apply(rule,rule min_max.less_supI1,rule B1)
hoelzl@37489
  1269
    proof(rule,rule,rule) fix a b assume "ball 0 (max B1 B2) \<subseteq> {a..b::'n}"
hoelzl@37489
  1270
      hence *:"ball 0 B1 \<subseteq> {a..b::'n}" "ball 0 B2 \<subseteq> {a..b::'n}" by auto
himmelma@35172
  1271
      guess w using B1(2)[OF *(1)] .. note w=conjunctD2[OF this]
himmelma@35172
  1272
      guess z using B2(2)[OF *(2)] .. note z=conjunctD2[OF this]
himmelma@35172
  1273
      have *:"\<And>x. (if x \<in> s then f x + g x else 0) = (if x \<in> s then f x else 0) + (if x \<in> s then g x else 0)" by auto
himmelma@35172
  1274
      show "\<exists>z. ((\<lambda>x. if x \<in> s then f x + g x else 0) has_integral z) {a..b} \<and> norm (z - (k + l)) < e"
himmelma@35172
  1275
        apply(rule_tac x="w + z" in exI) apply(rule,rule lem[OF w(1) z(1), unfolded *[THEN sym]])
himmelma@35172
  1276
        using norm_triangle_ineq[of "w - k" "z - l"] w(2) z(2) by(auto simp add:field_simps)
himmelma@35172
  1277
    qed qed qed
himmelma@35172
  1278
himmelma@35172
  1279
lemma has_integral_sub:
himmelma@35172
  1280
  shows "(f has_integral k) s \<Longrightarrow> (g has_integral l) s \<Longrightarrow> ((\<lambda>x. f(x) - g(x)) has_integral (k - l)) s"
haftmann@36350
  1281
  using has_integral_add[OF _ has_integral_neg,of f k s g l] unfolding algebra_simps by auto
himmelma@35172
  1282
hoelzl@37489
  1283
lemma integral_0: "integral s (\<lambda>x::'n::ordered_euclidean_space. 0::'m::real_normed_vector) = 0"
himmelma@35172
  1284
  by(rule integral_unique has_integral_0)+
himmelma@35172
  1285
himmelma@35172
  1286
lemma integral_add:
himmelma@35172
  1287
  shows "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow>
himmelma@35172
  1288
   integral s (\<lambda>x. f x + g x) = integral s f + integral s g"
himmelma@35172
  1289
  apply(rule integral_unique) apply(drule integrable_integral)+
himmelma@35172
  1290
  apply(rule has_integral_add) by assumption+
himmelma@35172
  1291
himmelma@35172
  1292
lemma integral_cmul:
himmelma@35172
  1293
  shows "f integrable_on s \<Longrightarrow> integral s (\<lambda>x. c *\<^sub>R f x) = c *\<^sub>R integral s f"
himmelma@35172
  1294
  apply(rule integral_unique) apply(drule integrable_integral)+
himmelma@35172
  1295
  apply(rule has_integral_cmul) by assumption+
himmelma@35172
  1296
himmelma@35172
  1297
lemma integral_neg:
himmelma@35172
  1298
  shows "f integrable_on s \<Longrightarrow> integral s (\<lambda>x. - f x) = - integral s f"
himmelma@35172
  1299
  apply(rule integral_unique) apply(drule integrable_integral)+
himmelma@35172
  1300
  apply(rule has_integral_neg) by assumption+
himmelma@35172
  1301
himmelma@35172
  1302
lemma integral_sub:
himmelma@35172
  1303
  shows "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow> integral s (\<lambda>x. f x - g x) = integral s f - integral s g"
himmelma@35172
  1304
  apply(rule integral_unique) apply(drule integrable_integral)+
himmelma@35172
  1305
  apply(rule has_integral_sub) by assumption+
himmelma@35172
  1306
himmelma@35172
  1307
lemma integrable_0: "(\<lambda>x. 0) integrable_on s"
himmelma@35172
  1308
  unfolding integrable_on_def using has_integral_0 by auto
himmelma@35172
  1309
himmelma@35172
  1310
lemma integrable_add:
himmelma@35172
  1311
  shows "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow> (\<lambda>x. f x + g x) integrable_on s"
himmelma@35172
  1312
  unfolding integrable_on_def by(auto intro: has_integral_add)
himmelma@35172
  1313
himmelma@35172
  1314
lemma integrable_cmul:
himmelma@35172
  1315
  shows "f integrable_on s \<Longrightarrow> (\<lambda>x. c *\<^sub>R f(x)) integrable_on s"
himmelma@35172
  1316
  unfolding integrable_on_def by(auto intro: has_integral_cmul)
himmelma@35172
  1317
himmelma@35172
  1318
lemma integrable_neg:
himmelma@35172
  1319
  shows "f integrable_on s \<Longrightarrow> (\<lambda>x. -f(x)) integrable_on s"
himmelma@35172
  1320
  unfolding integrable_on_def by(auto intro: has_integral_neg)
himmelma@35172
  1321
himmelma@35172
  1322
lemma integrable_sub:
himmelma@35172
  1323
  shows "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow> (\<lambda>x. f x - g x) integrable_on s"
himmelma@35172
  1324
  unfolding integrable_on_def by(auto intro: has_integral_sub)
himmelma@35172
  1325
himmelma@35172
  1326
lemma integrable_linear:
himmelma@35172
  1327
  shows "f integrable_on s \<Longrightarrow> bounded_linear h \<Longrightarrow> (h o f) integrable_on s"
himmelma@35172
  1328
  unfolding integrable_on_def by(auto intro: has_integral_linear)
himmelma@35172
  1329
himmelma@35172
  1330
lemma integral_linear:
himmelma@35172
  1331
  shows "f integrable_on s \<Longrightarrow> bounded_linear h \<Longrightarrow> integral s (h o f) = h(integral s f)"
himmelma@35172
  1332
  apply(rule has_integral_unique) defer unfolding has_integral_integral 
himmelma@35172
  1333
  apply(drule has_integral_linear,assumption,assumption) unfolding has_integral_integral[THEN sym]
himmelma@35172
  1334
  apply(rule integrable_linear) by assumption+
himmelma@35172
  1335
hoelzl@37489
  1336
lemma integral_component_eq[simp]: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'm::ordered_euclidean_space"
hoelzl@37489
  1337
  assumes "f integrable_on s" shows "integral s (\<lambda>x. f x $$ k) = integral s f $$ k"
hoelzl@37489
  1338
  unfolding integral_linear[OF assms(1) bounded_linear_component,unfolded o_def] ..
himmelma@36243
  1339
himmelma@35172
  1340
lemma has_integral_setsum:
himmelma@35172
  1341
  assumes "finite t" "\<forall>a\<in>t. ((f a) has_integral (i a)) s"
himmelma@35172
  1342
  shows "((\<lambda>x. setsum (\<lambda>a. f a x) t) has_integral (setsum i t)) s"
himmelma@35172
  1343
proof(insert assms(1) subset_refl[of t],induct rule:finite_subset_induct)
himmelma@35172
  1344
  case (insert x F) show ?case unfolding setsum_insert[OF insert(1,3)]
himmelma@35172
  1345
    apply(rule has_integral_add) using insert assms by auto
himmelma@35172
  1346
qed auto
himmelma@35172
  1347
himmelma@35172
  1348
lemma integral_setsum:
himmelma@35172
  1349
  shows "finite t \<Longrightarrow> \<forall>a\<in>t. (f a) integrable_on s \<Longrightarrow>
himmelma@35172
  1350
  integral s (\<lambda>x. setsum (\<lambda>a. f a x) t) = setsum (\<lambda>a. integral s (f a)) t"
himmelma@35172
  1351
  apply(rule integral_unique) apply(rule has_integral_setsum)
himmelma@35172
  1352
  using integrable_integral by auto
himmelma@35172
  1353
himmelma@35172
  1354
lemma integrable_setsum:
himmelma@35172
  1355
  shows "finite t \<Longrightarrow> \<forall>a \<in> t.(f a) integrable_on s \<Longrightarrow> (\<lambda>x. setsum (\<lambda>a. f a x) t) integrable_on s"
himmelma@35172
  1356
  unfolding integrable_on_def apply(drule bchoice) using has_integral_setsum[of t] by auto
himmelma@35172
  1357
himmelma@35172
  1358
lemma has_integral_eq:
himmelma@35172
  1359
  assumes "\<forall>x\<in>s. f x = g x" "(f has_integral k) s" shows "(g has_integral k) s"
himmelma@35172
  1360
  using has_integral_sub[OF assms(2), of "\<lambda>x. f x - g x" 0]
himmelma@35172
  1361
  using has_integral_is_0[of s "\<lambda>x. f x - g x"] using assms(1) by auto
himmelma@35172
  1362
himmelma@35172
  1363
lemma integrable_eq:
himmelma@35172
  1364
  shows "\<forall>x\<in>s. f x = g x \<Longrightarrow> f integrable_on s \<Longrightarrow> g integrable_on s"
himmelma@35172
  1365
  unfolding integrable_on_def using has_integral_eq[of s f g] by auto
himmelma@35172
  1366
himmelma@35172
  1367
lemma has_integral_eq_eq:
himmelma@35172
  1368
  shows "\<forall>x\<in>s. f x = g x \<Longrightarrow> ((f has_integral k) s \<longleftrightarrow> (g has_integral k) s)"
huffman@36362
  1369
  using has_integral_eq[of s f g] has_integral_eq[of s g f] by rule auto
himmelma@35172
  1370
himmelma@35172
  1371
lemma has_integral_null[dest]:
himmelma@35172
  1372
  assumes "content({a..b}) = 0" shows  "(f has_integral 0) ({a..b})"
himmelma@35172
  1373
  unfolding has_integral apply(rule,rule,rule_tac x="\<lambda>x. ball x 1" in exI,rule) defer
himmelma@35172
  1374
proof(rule,rule,erule conjE) fix e::real assume e:"e>0" thus "gauge (\<lambda>x. ball x 1)" by auto
himmelma@35172
  1375
  fix p assume p:"p tagged_division_of {a..b}" (*"(\<lambda>x. ball x 1) fine p"*)
himmelma@35172
  1376
  have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) = 0" unfolding norm_eq_zero diff_0_right
himmelma@35172
  1377
    using setsum_content_null[OF assms(1) p, of f] . 
himmelma@35172
  1378
  thus "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) < e" using e by auto qed
himmelma@35172
  1379
himmelma@35172
  1380
lemma has_integral_null_eq[simp]:
himmelma@35172
  1381
  shows "content({a..b}) = 0 \<Longrightarrow> ((f has_integral i) ({a..b}) \<longleftrightarrow> i = 0)"
himmelma@35172
  1382
  apply rule apply(rule has_integral_unique,assumption) 
himmelma@35172
  1383
  apply(drule has_integral_null,assumption)
himmelma@35172
  1384
  apply(drule has_integral_null) by auto
himmelma@35172
  1385
himmelma@35172
  1386
lemma integral_null[dest]: shows "content({a..b}) = 0 \<Longrightarrow> integral({a..b}) f = 0"
himmelma@35172
  1387
  by(rule integral_unique,drule has_integral_null)
himmelma@35172
  1388
himmelma@35172
  1389
lemma integrable_on_null[dest]: shows "content({a..b}) = 0 \<Longrightarrow> f integrable_on {a..b}"
himmelma@35172
  1390
  unfolding integrable_on_def apply(drule has_integral_null) by auto
himmelma@35172
  1391
himmelma@35172
  1392
lemma has_integral_empty[intro]: shows "(f has_integral 0) {}"
himmelma@35172
  1393
  unfolding empty_as_interval apply(rule has_integral_null) 
himmelma@35172
  1394
  using content_empty unfolding empty_as_interval .
himmelma@35172
  1395
himmelma@35172
  1396
lemma has_integral_empty_eq[simp]: shows "(f has_integral i) {} \<longleftrightarrow> i = 0"
himmelma@35172
  1397
  apply(rule,rule has_integral_unique,assumption) by auto
himmelma@35172
  1398
himmelma@35172
  1399
lemma integrable_on_empty[intro]: shows "f integrable_on {}" unfolding integrable_on_def by auto
himmelma@35172
  1400
himmelma@35172
  1401
lemma integral_empty[simp]: shows "integral {} f = 0"
himmelma@35172
  1402
  apply(rule integral_unique) using has_integral_empty .
himmelma@35172
  1403
hoelzl@37489
  1404
lemma has_integral_refl[intro]: shows "(f has_integral 0) {a..a}" "(f has_integral 0) {a::'a::ordered_euclidean_space}"
hoelzl@37489
  1405
proof- have *:"{a} = {a..a}" apply(rule set_ext) unfolding mem_interval singleton_iff euclidean_eq[where 'a='a]
himmelma@35540
  1406
    apply safe prefer 3 apply(erule_tac x=i in allE) by(auto simp add: field_simps)
himmelma@35540
  1407
  show "(f has_integral 0) {a..a}" "(f has_integral 0) {a}" unfolding *
himmelma@35540
  1408
    apply(rule_tac[!] has_integral_null) unfolding content_eq_0_interior
himmelma@35540
  1409
    unfolding interior_closed_interval using interval_sing by auto qed
himmelma@35172
  1410
himmelma@35172
  1411
lemma integrable_on_refl[intro]: shows "f integrable_on {a..a}" unfolding integrable_on_def by auto
himmelma@35172
  1412
himmelma@35172
  1413
lemma integral_refl: shows "integral {a..a} f = 0" apply(rule integral_unique) by auto
himmelma@35172
  1414
himmelma@35172
  1415
subsection {* Cauchy-type criterion for integrability. *}
himmelma@35172
  1416
hoelzl@37489
  1417
(* XXXXXXX *)
hoelzl@37489
  1418
lemma integrable_cauchy: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::{real_normed_vector,complete_space}" 
himmelma@35172
  1419
  shows "f integrable_on {a..b} \<longleftrightarrow>
himmelma@35172
  1420
  (\<forall>e>0.\<exists>d. gauge d \<and> (\<forall>p1 p2. p1 tagged_division_of {a..b} \<and> d fine p1 \<and>
himmelma@35172
  1421
                            p2 tagged_division_of {a..b} \<and> d fine p2
himmelma@35172
  1422
                            \<longrightarrow> norm(setsum (\<lambda>(x,k). content k *\<^sub>R f x) p1 -
himmelma@35172
  1423
                                     setsum (\<lambda>(x,k). content k *\<^sub>R f x) p2) < e))" (is "?l = (\<forall>e>0. \<exists>d. ?P e d)")
himmelma@35172
  1424
proof assume ?l
himmelma@35172
  1425
  then guess y unfolding integrable_on_def has_integral .. note y=this
himmelma@35172
  1426
  show "\<forall>e>0. \<exists>d. ?P e d" proof(rule,rule) case goal1 hence "e/2 > 0" by auto
himmelma@35172
  1427
    then guess d apply- apply(drule y[rule_format]) by(erule exE,erule conjE) note d=this[rule_format]
himmelma@35172
  1428
    show ?case apply(rule_tac x=d in exI,rule,rule d) apply(rule,rule,rule,(erule conjE)+)
himmelma@35172
  1429
    proof- fix p1 p2 assume as:"p1 tagged_division_of {a..b}" "d fine p1" "p2 tagged_division_of {a..b}" "d fine p2"
himmelma@35172
  1430
      show "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x)) < e"
huffman@36587
  1431
        apply(rule dist_triangle_half_l[where y=y,unfolded dist_norm])
himmelma@35172
  1432
        using d(2)[OF conjI[OF as(1-2)]] d(2)[OF conjI[OF as(3-4)]] .
himmelma@35172
  1433
    qed qed
himmelma@35172
  1434
next assume "\<forall>e>0. \<exists>d. ?P e d" hence "\<forall>n::nat. \<exists>d. ?P (inverse(real (n + 1))) d" by auto
himmelma@35172
  1435
  from choice[OF this] guess d .. note d=conjunctD2[OF this[rule_format],rule_format]
himmelma@35172
  1436
  have "\<And>n. gauge (\<lambda>x. \<Inter>{d i x |i. i \<in> {0..n}})" apply(rule gauge_inters) using d(1) by auto
himmelma@35172
  1437
  hence "\<forall>n. \<exists>p. p tagged_division_of {a..b} \<and> (\<lambda>x. \<Inter>{d i x |i. i \<in> {0..n}}) fine p" apply-
himmelma@35172
  1438
  proof case goal1 from this[of n] show ?case apply(drule_tac fine_division_exists) by auto qed
himmelma@35172
  1439
  from choice[OF this] guess p .. note p = conjunctD2[OF this[rule_format]]
himmelma@35172
  1440
  have dp:"\<And>i n. i\<le>n \<Longrightarrow> d i fine p n" using p(2) unfolding fine_inters by auto
himmelma@35172
  1441
  have "Cauchy (\<lambda>n. setsum (\<lambda>(x,k). content k *\<^sub>R (f x)) (p n))"
himmelma@35172
  1442
  proof(rule CauchyI) case goal1 then guess N unfolding real_arch_inv[of e] .. note N=this
himmelma@35172
  1443
    show ?case apply(rule_tac x=N in exI)
himmelma@35172
  1444
    proof(rule,rule,rule,rule) fix m n assume mn:"N \<le> m" "N \<le> n" have *:"N = (N - 1) + 1" using N by auto
himmelma@35172
  1445
      show "norm ((\<Sum>(x, k)\<in>p m. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p n. content k *\<^sub>R f x)) < e"
himmelma@35172
  1446
        apply(rule less_trans[OF _ N[THEN conjunct2,THEN conjunct2]]) apply(subst *) apply(rule d(2))
himmelma@35172
  1447
        using dp p(1) using mn by auto 
himmelma@35172
  1448
    qed qed
himmelma@35172
  1449
  then guess y unfolding convergent_eq_cauchy[THEN sym] .. note y=this[unfolded Lim_sequentially,rule_format]
himmelma@35172
  1450
  show ?l unfolding integrable_on_def has_integral apply(rule_tac x=y in exI)
himmelma@35172
  1451
  proof(rule,rule) fix e::real assume "e>0" hence *:"e/2 > 0" by auto
himmelma@35172
  1452
    then guess N1 unfolding real_arch_inv[of "e/2"] .. note N1=this hence N1':"N1 = N1 - 1 + 1" by auto
himmelma@35172
  1453
    guess N2 using y[OF *] .. note N2=this
himmelma@35172
  1454
    show "\<exists>d. gauge d \<and> (\<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) - y) < e)"
himmelma@35172
  1455
      apply(rule_tac x="d (N1 + N2)" in exI) apply rule defer 
himmelma@35172
  1456
    proof(rule,rule,erule conjE) show "gauge (d (N1 + N2))" using d by auto
himmelma@35172
  1457
      fix q assume as:"q tagged_division_of {a..b}" "d (N1 + N2) fine q"
himmelma@35172
  1458
      have *:"inverse (real (N1 + N2 + 1)) < e / 2" apply(rule less_trans) using N1 by auto
himmelma@35172
  1459
      show "norm ((\<Sum>(x, k)\<in>q. content k *\<^sub>R f x) - y) < e" apply(rule norm_triangle_half_r)
himmelma@35172
  1460
        apply(rule less_trans[OF _ *]) apply(subst N1', rule d(2)[of "p (N1+N2)"]) defer
huffman@36587
  1461
        using N2[rule_format,unfolded dist_norm,of "N1+N2"]
himmelma@35172
  1462
        using as dp[of "N1 - 1 + 1 + N2" "N1 + N2"] using p(1)[of "N1 + N2"] using N1 by auto qed qed qed
himmelma@35172
  1463
himmelma@35172
  1464
subsection {* Additivity of integral on abutting intervals. *}
himmelma@35172
  1465
hoelzl@37489
  1466
lemma interval_split: fixes a::"'a::ordered_euclidean_space" assumes "k<DIM('a)" shows
hoelzl@37489
  1467
  "{a..b} \<inter> {x. x$$k \<le> c} = {a .. (\<chi>\<chi> i. if i = k then min (b$$k) c else b$$i)}"
hoelzl@37489
  1468
  "{a..b} \<inter> {x. x$$k \<ge> c} = {(\<chi>\<chi> i. if i = k then max (a$$k) c else a$$i) .. b}"
hoelzl@37489
  1469
  apply(rule_tac[!] set_ext) unfolding Int_iff mem_interval mem_Collect_eq using assms by auto
hoelzl@37489
  1470
hoelzl@37489
  1471
lemma content_split: fixes a::"'a::ordered_euclidean_space" assumes "k<DIM('a)" shows
hoelzl@37489
  1472
  "content {a..b} = content({a..b} \<inter> {x. x$$k \<le> c}) + content({a..b} \<inter> {x. x$$k >= c})"
hoelzl@37489
  1473
proof- note simps = interval_split[OF assms] content_closed_interval_cases eucl_le[where 'a='a]
hoelzl@37489
  1474
  { presume "a\<le>b \<Longrightarrow> ?thesis" thus ?thesis apply(cases "a\<le>b") unfolding simps using assms by auto }
hoelzl@37489
  1475
  have *:"{..<DIM('a)} = insert k ({..<DIM('a)} - {k})" "\<And>x. finite ({..<DIM('a)}-{x})" "\<And>x. x\<notin>{..<DIM('a)}-{x}"
hoelzl@37489
  1476
    using assms by auto
hoelzl@37489
  1477
  have *:"\<And>X Y Z. (\<Prod>i\<in>{..<DIM('a)}. Z i (if i = k then X else Y i)) = Z k X * (\<Prod>i\<in>{..<DIM('a)}-{k}. Z i (Y i))"
hoelzl@37489
  1478
    "(\<Prod>i\<in>{..<DIM('a)}. b$$i - a$$i) = (\<Prod>i\<in>{..<DIM('a)}-{k}. b$$i - a$$i) * (b$$k - a$$k)" 
himmelma@35172
  1479
    apply(subst *(1)) defer apply(subst *(1)) unfolding setprod_insert[OF *(2-)] by auto
hoelzl@37489
  1480
  assume as:"a\<le>b" moreover have "\<And>x. min (b $$ k) c = max (a $$ k) c
hoelzl@37489
  1481
    \<Longrightarrow> x* (b$$k - a$$k) = x*(max (a $$ k) c - a $$ k) + x*(b $$ k - max (a $$ k) c)"
himmelma@35172
  1482
    by  (auto simp add:field_simps)
hoelzl@37489
  1483
  moreover have **:"(\<Prod>i<DIM('a). ((\<chi>\<chi> i. if i = k then min (b $$ k) c else b $$ i)::'a) $$ i - a $$ i) = 
hoelzl@37489
  1484
    (\<Prod>i<DIM('a). (if i = k then min (b $$ k) c else b $$ i) - a $$ i)"
hoelzl@37489
  1485
    "(\<Prod>i<DIM('a). b $$ i - ((\<chi>\<chi> i. if i = k then max (a $$ k) c else a $$ i)::'a) $$ i) =
hoelzl@37489
  1486
    (\<Prod>i<DIM('a). b $$ i - (if i = k then max (a $$ k) c else a $$ i))"
hoelzl@37489
  1487
    apply(rule_tac[!] setprod.cong) by auto
hoelzl@37489
  1488
  have "\<not> a $$ k \<le> c \<Longrightarrow> \<not> c \<le> b $$ k \<Longrightarrow> False"
hoelzl@37489
  1489
    unfolding not_le using as[unfolded eucl_le[where 'a='a],rule_format,of k] assms by auto
hoelzl@37489
  1490
  ultimately show ?thesis using assms unfolding simps **
hoelzl@37489
  1491
    unfolding *(1)[of "\<lambda>i x. b$$i - x"] *(1)[of "\<lambda>i x. x - a$$i"] unfolding  *(2) 
hoelzl@37489
  1492
    apply(subst(2) euclidean_lambda_beta''[where 'a='a])
hoelzl@37489
  1493
    apply(subst(3) euclidean_lambda_beta''[where 'a='a]) by auto
himmelma@35172
  1494
qed
himmelma@35172
  1495
hoelzl@37489
  1496
lemma division_split_left_inj: fixes type::"'a::ordered_euclidean_space"
hoelzl@37489
  1497
  assumes "d division_of i" "k1 \<in> d" "k2 \<in> d"  "k1 \<noteq> k2" 
hoelzl@37489
  1498
  "k1 \<inter> {x::'a. x$$k \<le> c} = k2 \<inter> {x. x$$k \<le> c}"and k:"k<DIM('a)"
hoelzl@37489
  1499
  shows "content(k1 \<inter> {x. x$$k \<le> c}) = 0"
himmelma@35172
  1500
proof- note d=division_ofD[OF assms(1)]
hoelzl@37489
  1501
  have *:"\<And>a b::'a. \<And> c. (content({a..b} \<inter> {x. x$$k \<le> c}) = 0 \<longleftrightarrow> interior({a..b} \<inter> {x. x$$k \<le> c}) = {})"
hoelzl@37489
  1502
    unfolding  interval_split[OF k] content_eq_0_interior by auto
himmelma@35172
  1503
  guess u1 v1 using d(4)[OF assms(2)] apply-by(erule exE)+ note uv1=this
himmelma@35172
  1504
  guess u2 v2 using d(4)[OF assms(3)] apply-by(erule exE)+ note uv2=this
himmelma@35172
  1505
  have **:"\<And>s t u. s \<inter> t = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<subseteq> t \<Longrightarrow> u = {}" by auto
himmelma@35172
  1506
  show ?thesis unfolding uv1 uv2 * apply(rule **[OF d(5)[OF assms(2-4)]])
himmelma@35172
  1507
    defer apply(subst assms(5)[unfolded uv1 uv2]) unfolding uv1 uv2 by auto qed
hoelzl@37489
  1508
 
hoelzl@37489
  1509
lemma division_split_right_inj: fixes type::"'a::ordered_euclidean_space"
himmelma@35172
  1510
  assumes "d division_of i" "k1 \<in> d" "k2 \<in> d"  "k1 \<noteq> k2"
hoelzl@37489
  1511
  "k1 \<inter> {x::'a. x$$k \<ge> c} = k2 \<inter> {x. x$$k \<ge> c}" and k:"k<DIM('a)"
hoelzl@37489
  1512
  shows "content(k1 \<inter> {x. x$$k \<ge> c}) = 0"
himmelma@35172
  1513
proof- note d=division_ofD[OF assms(1)]
hoelzl@37489
  1514
  have *:"\<And>a b::'a. \<And> c. (content({a..b} \<inter> {x. x$$k >= c}) = 0 \<longleftrightarrow> interior({a..b} \<inter> {x. x$$k >= c}) = {})"
hoelzl@37489
  1515
    unfolding interval_split[OF k] content_eq_0_interior by auto
himmelma@35172
  1516
  guess u1 v1 using d(4)[OF assms(2)] apply-by(erule exE)+ note uv1=this
himmelma@35172
  1517
  guess u2 v2 using d(4)[OF assms(3)] apply-by(erule exE)+ note uv2=this
himmelma@35172
  1518
  have **:"\<And>s t u. s \<inter> t = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<subseteq> t \<Longrightarrow> u = {}" by auto
himmelma@35172
  1519
  show ?thesis unfolding uv1 uv2 * apply(rule **[OF d(5)[OF assms(2-4)]])
himmelma@35172
  1520
    defer apply(subst assms(5)[unfolded uv1 uv2]) unfolding uv1 uv2 by auto qed
himmelma@35172
  1521
hoelzl@37489
  1522
lemma tagged_division_split_left_inj: fixes x1::"'a::ordered_euclidean_space"
hoelzl@37489
  1523
  assumes "d tagged_division_of i" "(x1,k1) \<in> d" "(x2,k2) \<in> d" "k1 \<noteq> k2"  "k1 \<inter> {x. x$$k \<le> c} = k2 \<inter> {x. x$$k \<le> c}" 
hoelzl@37489
  1524
  and k:"k<DIM('a)"
hoelzl@37489
  1525
  shows "content(k1 \<inter> {x. x$$k \<le> c}) = 0"
himmelma@35172
  1526
proof- have *:"\<And>a b c. (a,b) \<in> c \<Longrightarrow> b \<in> snd ` c" unfolding image_iff apply(rule_tac x="(a,b)" in bexI) by auto
himmelma@35172
  1527
  show ?thesis apply(rule division_split_left_inj[OF division_of_tagged_division[OF assms(1)]])
himmelma@35172
  1528
    apply(rule_tac[1-2] *) using assms(2-) by auto qed
himmelma@35172
  1529
hoelzl@37489
  1530
lemma tagged_division_split_right_inj: fixes x1::"'a::ordered_euclidean_space"
hoelzl@37489
  1531
  assumes "d tagged_division_of i" "(x1,k1) \<in> d" "(x2,k2) \<in> d" "k1 \<noteq> k2"  "k1 \<inter> {x. x$$k \<ge> c} = k2 \<inter> {x. x$$k \<ge> c}" 
hoelzl@37489
  1532
  and k:"k<DIM('a)"
hoelzl@37489
  1533
  shows "content(k1 \<inter> {x. x$$k \<ge> c}) = 0"
himmelma@35172
  1534
proof- have *:"\<And>a b c. (a,b) \<in> c \<Longrightarrow> b \<in> snd ` c" unfolding image_iff apply(rule_tac x="(a,b)" in bexI) by auto
himmelma@35172
  1535
  show ?thesis apply(rule division_split_right_inj[OF division_of_tagged_division[OF assms(1)]])
himmelma@35172
  1536
    apply(rule_tac[1-2] *) using assms(2-) by auto qed
himmelma@35172
  1537
hoelzl@37489
  1538
lemma division_split: fixes a::"'a::ordered_euclidean_space"
hoelzl@37489
  1539
  assumes "p division_of {a..b}" and k:"k<DIM('a)"
hoelzl@37489
  1540
  shows "{l \<inter> {x. x$$k \<le> c} | l. l \<in> p \<and> ~(l \<inter> {x. x$$k \<le> c} = {})} division_of({a..b} \<inter> {x. x$$k \<le> c})" (is "?p1 division_of ?I1") and 
hoelzl@37489
  1541
        "{l \<inter> {x. x$$k \<ge> c} | l. l \<in> p \<and> ~(l \<inter> {x. x$$k \<ge> c} = {})} division_of ({a..b} \<inter> {x. x$$k \<ge> c})" (is "?p2 division_of ?I2")
hoelzl@37489
  1542
proof(rule_tac[!] division_ofI) note p=division_ofD[OF assms(1)]
himmelma@35172
  1543
  show "finite ?p1" "finite ?p2" using p(1) by auto show "\<Union>?p1 = ?I1" "\<Union>?p2 = ?I2" unfolding p(6)[THEN sym] by auto
himmelma@35172
  1544
  { fix k assume "k\<in>?p1" then guess l unfolding mem_Collect_eq apply-by(erule exE,(erule conjE)+) note l=this
himmelma@35172
  1545
    guess u v using p(4)[OF l(2)] apply-by(erule exE)+ note uv=this
himmelma@35172
  1546
    show "k\<subseteq>?I1" "k \<noteq> {}" "\<exists>a b. k = {a..b}" unfolding l
hoelzl@37489
  1547
      using p(2-3)[OF l(2)] l(3) unfolding uv apply- prefer 3 apply(subst interval_split[OF k]) by auto
himmelma@35172
  1548
    fix k' assume "k'\<in>?p1" then guess l' unfolding mem_Collect_eq apply-by(erule exE,(erule conjE)+) note l'=this
himmelma@35172
  1549
    assume "k\<noteq>k'" thus "interior k \<inter> interior k' = {}" unfolding l l' using p(5)[OF l(2) l'(2)] by auto }
himmelma@35172
  1550
  { fix k assume "k\<in>?p2" then guess l unfolding mem_Collect_eq apply-by(erule exE,(erule conjE)+) note l=this
himmelma@35172
  1551
    guess u v using p(4)[OF l(2)] apply-by(erule exE)+ note uv=this
himmelma@35172
  1552
    show "k\<subseteq>?I2" "k \<noteq> {}" "\<exists>a b. k = {a..b}" unfolding l
hoelzl@37489
  1553
      using p(2-3)[OF l(2)] l(3) unfolding uv apply- prefer 3 apply(subst interval_split[OF k]) by auto
himmelma@35172
  1554
    fix k' assume "k'\<in>?p2" then guess l' unfolding mem_Collect_eq apply-by(erule exE,(erule conjE)+) note l'=this
himmelma@35172
  1555
    assume "k\<noteq>k'" thus "interior k \<inter> interior k' = {}" unfolding l l' using p(5)[OF l(2) l'(2)] by auto }
himmelma@35172
  1556
qed
himmelma@35172
  1557
hoelzl@37489
  1558
lemma has_integral_split: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
hoelzl@37489
  1559
  assumes "(f has_integral i) ({a..b} \<inter> {x. x$$k \<le> c})"  "(f has_integral j) ({a..b} \<inter> {x. x$$k \<ge> c})" and k:"k<DIM('a)"
himmelma@35172
  1560
  shows "(f has_integral (i + j)) ({a..b})"
himmelma@35172
  1561
proof(unfold has_integral,rule,rule) case goal1 hence e:"e/2>0" by auto
hoelzl@37489
  1562
  guess d1 using has_integralD[OF assms(1)[unfolded interval_split[OF k]] e] . note d1=this[unfolded interval_split[THEN sym,OF k]]
hoelzl@37489
  1563
  guess d2 using has_integralD[OF assms(2)[unfolded interval_split[OF k]] e] . note d2=this[unfolded interval_split[THEN sym,OF k]]
hoelzl@37489
  1564
  let ?d = "\<lambda>x. if x$$k = c then (d1 x \<inter> d2 x) else ball x (abs(x$$k - c)) \<inter> d1 x \<inter> d2 x"
himmelma@35172
  1565
  show ?case apply(rule_tac x="?d" in exI,rule) defer apply(rule,rule,(erule conjE)+)
himmelma@35172
  1566
  proof- show "gauge ?d" using d1(1) d2(1) unfolding gauge_def by auto
himmelma@35172
  1567
    fix p assume "p tagged_division_of {a..b}" "?d fine p" note p = this tagged_division_ofD[OF this(1)]
hoelzl@37489
  1568
    have lem0:"\<And>x kk. (x,kk) \<in> p \<Longrightarrow> ~(kk \<inter> {x. x$$k \<le> c} = {}) \<Longrightarrow> x$$k \<le> c"
hoelzl@37489
  1569
         "\<And>x kk. (x,kk) \<in> p \<Longrightarrow> ~(kk \<inter> {x. x$$k \<ge> c} = {}) \<Longrightarrow> x$$k \<ge> c"
himmelma@35172
  1570
    proof- fix x kk assume as:"(x,kk)\<in>p"
hoelzl@37489
  1571
      show "~(kk \<inter> {x. x$$k \<le> c} = {}) \<Longrightarrow> x$$k \<le> c"
himmelma@35172
  1572
      proof(rule ccontr) case goal1
hoelzl@37489
  1573
        from this(2)[unfolded not_le] have "kk \<subseteq> ball x \<bar>x $$ k - c\<bar>"
himmelma@35172
  1574
          using p(2)[unfolded fine_def,rule_format,OF as,unfolded split_conv] by auto
hoelzl@37489
  1575
        hence "\<exists>y. y \<in> ball x \<bar>x $$ k - c\<bar> \<inter> {x. x $$ k \<le> c}" using goal1(1) by blast 
hoelzl@37489
  1576
        then guess y .. hence "\<bar>x $$ k - y $$ k\<bar> < \<bar>x $$ k - c\<bar>" "y$$k \<le> c" apply-apply(rule le_less_trans)
hoelzl@37489
  1577
          using component_le_norm[of "x - y" k] by(auto simp add:dist_norm)
himmelma@35172
  1578
        thus False using goal1(2)[unfolded not_le] by(auto simp add:field_simps)
himmelma@35172
  1579
      qed
hoelzl@37489
  1580
      show "~(kk \<inter> {x. x$$k \<ge> c} = {}) \<Longrightarrow> x$$k \<ge> c"
himmelma@35172
  1581
      proof(rule ccontr) case goal1
hoelzl@37489
  1582
        from this(2)[unfolded not_le] have "kk \<subseteq> ball x \<bar>x $$ k - c\<bar>"
himmelma@35172
  1583
          using p(2)[unfolded fine_def,rule_format,OF as,unfolded split_conv] by auto
hoelzl@37489
  1584
        hence "\<exists>y. y \<in> ball x \<bar>x $$ k - c\<bar> \<inter> {x. x $$ k \<ge> c}" using goal1(1) by blast 
hoelzl@37489
  1585
        then guess y .. hence "\<bar>x $$ k - y $$ k\<bar> < \<bar>x $$ k - c\<bar>" "y$$k \<ge> c" apply-apply(rule le_less_trans)
hoelzl@37489
  1586
          using component_le_norm[of "x - y" k] by(auto simp add:dist_norm)
himmelma@35172
  1587
        thus False using goal1(2)[unfolded not_le] by(auto simp add:field_simps)
himmelma@35172
  1588
      qed
himmelma@35172
  1589
    qed
himmelma@35172
  1590
himmelma@35172
  1591
    have lem1: "\<And>f P Q. (\<forall>x k. (x,k) \<in> {(x,f k) | x k. P x k} \<longrightarrow> Q x k) \<longleftrightarrow> (\<forall>x k. P x k \<longrightarrow> Q x (f k))" by auto
himmelma@35172
  1592
    have lem2: "\<And>f s P f. finite s \<Longrightarrow> finite {(x,f k) | x k. (x,k) \<in> s \<and> P x k}"
himmelma@35172
  1593
    proof- case goal1 thus ?case apply-apply(rule finite_subset[of _ "(\<lambda>(x,k). (x,f k)) ` s"]) by auto qed
hoelzl@37489
  1594
    have lem3: "\<And>g::('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool. finite p \<Longrightarrow>
himmelma@35172
  1595
      setsum (\<lambda>(x,k). content k *\<^sub>R f x) {(x,g k) |x k. (x,k) \<in> p \<and> ~(g k = {})}
himmelma@35172
  1596
               = setsum (\<lambda>(x,k). content k *\<^sub>R f x) ((\<lambda>(x,k). (x,g k)) ` p)"
himmelma@35172
  1597
      apply(rule setsum_mono_zero_left) prefer 3
hoelzl@37489
  1598
    proof fix g::"('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" and i::"('a) \<times> (('a) set)"
himmelma@35172
  1599
      assume "i \<in> (\<lambda>(x, k). (x, g k)) ` p - {(x, g k) |x k. (x, k) \<in> p \<and> g k \<noteq> {}}"
himmelma@35172
  1600
      then obtain x k where xk:"i=(x,g k)" "(x,k)\<in>p" "(x,g k) \<notin> {(x, g k) |x k. (x, k) \<in> p \<and> g k \<noteq> {}}" by auto
himmelma@35172
  1601
      have "content (g k) = 0" using xk using content_empty by auto
himmelma@35172
  1602
      thus "(\<lambda>(x, k). content k *\<^sub>R f x) i = 0" unfolding xk split_conv by auto
himmelma@35172
  1603
    qed auto
himmelma@35172
  1604
    have lem4:"\<And>g. (\<lambda>(x,l). content (g l) *\<^sub>R f x) = (\<lambda>(x,l). content l *\<^sub>R f x) o (\<lambda>(x,l). (x,g l))" apply(rule ext) by auto
himmelma@35172
  1605
hoelzl@37489
  1606
    let ?M1 = "{(x,kk \<inter> {x. x$$k \<le> c}) |x kk. (x,kk) \<in> p \<and> kk \<inter> {x. x$$k \<le> c} \<noteq> {}}"
himmelma@35172
  1607
    have "norm ((\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) - i) < e/2" apply(rule d1(2),rule tagged_division_ofI)
himmelma@35172
  1608
      apply(rule lem2 p(3))+ prefer 6 apply(rule fineI)
hoelzl@37489
  1609
    proof- show "\<Union>{k. \<exists>x. (x, k) \<in> ?M1} = {a..b} \<inter> {x. x$$k \<le> c}" unfolding p(8)[THEN sym] by auto
himmelma@35172
  1610
      fix x l assume xl:"(x,l)\<in>?M1"
himmelma@35172
  1611
      then guess x' l' unfolding mem_Collect_eq apply- unfolding Pair_eq apply((erule exE)+,(erule conjE)+) .  note xl'=this
himmelma@35172
  1612
      have "l' \<subseteq> d1 x'" apply(rule order_trans[OF fineD[OF p(2) xl'(3)]]) by auto
himmelma@35172
  1613
      thus "l \<subseteq> d1 x" unfolding xl' by auto
hoelzl@37489
  1614
      show "x\<in>l" "l \<subseteq> {a..b} \<inter> {x. x $$ k \<le> c}" unfolding xl' using p(4-6)[OF xl'(3)] using xl'(4)
himmelma@35172
  1615
        using lem0(1)[OF xl'(3-4)] by auto
hoelzl@37489
  1616
      show  "\<exists>a b. l = {a..b}" unfolding xl' using p(6)[OF xl'(3)] by(fastsimp simp add: interval_split[OF k,where c=c])
himmelma@35172
  1617
      fix y r let ?goal = "interior l \<inter> interior r = {}" assume yr:"(y,r)\<in>?M1"
himmelma@35172
  1618
      then guess y' r' unfolding mem_Collect_eq apply- unfolding Pair_eq apply((erule exE)+,(erule conjE)+) .  note yr'=this
himmelma@35172
  1619
      assume as:"(x,l) \<noteq> (y,r)" show "interior l \<inter> interior r = {}"
himmelma@35172
  1620
      proof(cases "l' = r' \<longrightarrow> x' = y'")
himmelma@35172
  1621
        case False thus ?thesis using p(7)[OF xl'(3) yr'(3)] using as unfolding xl' yr' by auto
himmelma@35172
  1622
      next case True hence "l' \<noteq> r'" using as unfolding xl' yr' by auto
himmelma@35172
  1623
        thus ?thesis using p(7)[OF xl'(3) yr'(3)] using as unfolding xl' yr' by auto
himmelma@35172
  1624
      qed qed moreover
himmelma@35172
  1625
hoelzl@37489
  1626
    let ?M2 = "{(x,kk \<inter> {x. x$$k \<ge> c}) |x kk. (x,kk) \<in> p \<and> kk \<inter> {x. x$$k \<ge> c} \<noteq> {}}" 
himmelma@35172
  1627
    have "norm ((\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - j) < e/2" apply(rule d2(2),rule tagged_division_ofI)
himmelma@35172
  1628
      apply(rule lem2 p(3))+ prefer 6 apply(rule fineI)
hoelzl@37489
  1629
    proof- show "\<Union>{k. \<exists>x. (x, k) \<in> ?M2} = {a..b} \<inter> {x. x$$k \<ge> c}" unfolding p(8)[THEN sym] by auto
himmelma@35172
  1630
      fix x l assume xl:"(x,l)\<in>?M2"
himmelma@35172
  1631
      then guess x' l' unfolding mem_Collect_eq apply- unfolding Pair_eq apply((erule exE)+,(erule conjE)+) .  note xl'=this
himmelma@35172
  1632
      have "l' \<subseteq> d2 x'" apply(rule order_trans[OF fineD[OF p(2) xl'(3)]]) by auto
himmelma@35172
  1633
      thus "l \<subseteq> d2 x" unfolding xl' by auto
hoelzl@37489
  1634
      show "x\<in>l" "l \<subseteq> {a..b} \<inter> {x. x $$ k \<ge> c}" unfolding xl' using p(4-6)[OF xl'(3)] using xl'(4)
himmelma@35172
  1635
        using lem0(2)[OF xl'(3-4)] by auto
hoelzl@37489
  1636
      show  "\<exists>a b. l = {a..b}" unfolding xl' using p(6)[OF xl'(3)] by(fastsimp simp add: interval_split[OF k, where c=c])
himmelma@35172
  1637
      fix y r let ?goal = "interior l \<inter> interior r = {}" assume yr:"(y,r)\<in>?M2"
himmelma@35172
  1638
      then guess y' r' unfolding mem_Collect_eq apply- unfolding Pair_eq apply((erule exE)+,(erule conjE)+) .  note yr'=this
himmelma@35172
  1639
      assume as:"(x,l) \<noteq> (y,r)" show "interior l \<inter> interior r = {}"
himmelma@35172
  1640
      proof(cases "l' = r' \<longrightarrow> x' = y'")
himmelma@35172
  1641
        case False thus ?thesis using p(7)[OF xl'(3) yr'(3)] using as unfolding xl' yr' by auto
himmelma@35172
  1642
      next case True hence "l' \<noteq> r'" using as unfolding xl' yr' by auto
himmelma@35172
  1643
        thus ?thesis using p(7)[OF xl'(3) yr'(3)] using as unfolding xl' yr' by auto
himmelma@35172
  1644
      qed qed ultimately
himmelma@35172
  1645
himmelma@35172
  1646
    have "norm (((\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) - i) + ((\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - j)) < e/2 + e/2"
himmelma@35172
  1647
      apply- apply(rule norm_triangle_lt) by auto
hoelzl@37489
  1648
    also { have *:"\<And>x y. x = (0::real) \<Longrightarrow> x *\<^sub>R (y::'b) = 0" using scaleR_zero_left by auto
himmelma@35172
  1649
      have "((\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) - i) + ((\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - j)
himmelma@35172
  1650
       = (\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - (i + j)" by auto
hoelzl@37489
  1651
      also have "\<dots> = (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. x $$ k \<le> c}) *\<^sub>R f x) +
hoelzl@37489
  1652
        (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. c \<le> x $$ k}) *\<^sub>R f x) - (i + j)"
himmelma@35172
  1653
        unfolding lem3[OF p(3)] apply(subst setsum_reindex_nonzero[OF p(3)]) defer apply(subst setsum_reindex_nonzero[OF p(3)])
himmelma@35172
  1654
        defer unfolding lem4[THEN sym] apply(rule refl) unfolding split_paired_all split_conv apply(rule_tac[!] *)
hoelzl@37489
  1655
      proof- case goal1 thus ?case apply- apply(rule tagged_division_split_left_inj [OF p(1), of a b aa ba]) using k by auto
hoelzl@37489
  1656
      next case   goal2 thus ?case apply- apply(rule tagged_division_split_right_inj[OF p(1), of a b aa ba]) using k by auto
himmelma@35172
  1657
      qed also note setsum_addf[THEN sym]
hoelzl@37489
  1658
      also have *:"\<And>x. x\<in>p \<Longrightarrow> (\<lambda>(x, ka). content (ka \<inter> {x. x $$ k \<le> c}) *\<^sub>R f x) x + (\<lambda>(x, ka). content (ka \<inter> {x. c \<le> x $$ k}) *\<^sub>R f x) x
himmelma@35172
  1659
        = (\<lambda>(x,ka). content ka *\<^sub>R f x) x" unfolding split_paired_all split_conv
himmelma@35172
  1660
      proof- fix a b assume "(a,b) \<in> p" from p(6)[OF this] guess u v apply-by(erule exE)+ note uv=this
hoelzl@37489
  1661
        thus "content (b \<inter> {x. x $$ k \<le> c}) *\<^sub>R f a + content (b \<inter> {x. c \<le> x $$ k}) *\<^sub>R f a = content b *\<^sub>R f a"
hoelzl@37489
  1662
          unfolding scaleR_left_distrib[THEN sym] unfolding uv content_split[OF k,of u v c] by auto
himmelma@35172
  1663
      qed note setsum_cong2[OF this]
hoelzl@37489
  1664
      finally have "(\<Sum>(x, k)\<in>{(x, kk \<inter> {x. x $$ k \<le> c}) |x kk. (x, kk) \<in> p \<and> kk \<inter> {x. x $$ k \<le> c} \<noteq> {}}. content k *\<^sub>R f x) - i +
hoelzl@37489
  1665
        ((\<Sum>(x, k)\<in>{(x, kk \<inter> {x. c \<le> x $$ k}) |x kk. (x, kk) \<in> p \<and> kk \<inter> {x. c \<le> x $$ k} \<noteq> {}}. content k *\<^sub>R f x) - j) =
himmelma@35172
  1666
        (\<Sum>(x, ka)\<in>p. content ka *\<^sub>R f x) - (i + j)" by auto }
himmelma@35172
  1667
    finally show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - (i + j)) < e" by auto qed qed
himmelma@35172
  1668
hoelzl@37489
  1669
(*lemma has_integral_split_cart: fixes f::"real^'n \<Rightarrow> 'a::real_normed_vector"
hoelzl@37489
  1670
  assumes "(f has_integral i) ({a..b} \<inter> {x. x$k \<le> c})"  "(f has_integral j) ({a..b} \<inter> {x. x$k \<ge> c})"
hoelzl@37489
  1671
  shows "(f has_integral (i + j)) ({a..b})" *)
hoelzl@37489
  1672
himmelma@35172
  1673
subsection {* A sort of converse, integrability on subintervals. *}
himmelma@35172
  1674
hoelzl@37489
  1675
lemma tagged_division_union_interval: fixes a::"'a::ordered_euclidean_space"
hoelzl@37489
  1676
  assumes "p1 tagged_division_of ({a..b} \<inter> {x. x$$k \<le> (c::real)})"  "p2 tagged_division_of ({a..b} \<inter> {x. x$$k \<ge> c})"
hoelzl@37489
  1677
  and k:"k<DIM('a)"
himmelma@35172
  1678
  shows "(p1 \<union> p2) tagged_division_of ({a..b})"
hoelzl@37489
  1679
proof- have *:"{a..b} = ({a..b} \<inter> {x. x$$k \<le> c}) \<union> ({a..b} \<inter> {x. x$$k \<ge> c})" by auto
hoelzl@37489
  1680
  show ?thesis apply(subst *) apply(rule tagged_division_union[OF assms(1-2)])
hoelzl@37489
  1681
    unfolding interval_split[OF k] interior_closed_interval using k
hoelzl@37489
  1682
    by(auto simp add: eucl_less[where 'a='a] elim!:allE[where x=k]) qed
hoelzl@37489
  1683
hoelzl@37489
  1684
lemma has_integral_separate_sides: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
hoelzl@37489
  1685
  assumes "(f has_integral i) ({a..b})" "e>0" and k:"k<DIM('a)"
hoelzl@37489
  1686
  obtains d where "gauge d" "(\<forall>p1 p2. p1 tagged_division_of ({a..b} \<inter> {x. x$$k \<le> c}) \<and> d fine p1 \<and>
hoelzl@37489
  1687
                                p2 tagged_division_of ({a..b} \<inter> {x. x$$k \<ge> c}) \<and> d fine p2
himmelma@35172
  1688
                                \<longrightarrow> norm((setsum (\<lambda>(x,k). content k *\<^sub>R f x) p1 +
himmelma@35172
  1689
                                          setsum (\<lambda>(x,k). content k *\<^sub>R f x) p2) - i) < e)"
hoelzl@37489
  1690
proof- guess d using has_integralD[OF assms(1-2)] . note d=this
himmelma@35172
  1691
  show ?thesis apply(rule that[of d]) apply(rule d) apply(rule,rule,rule,(erule conjE)+)
hoelzl@37489
  1692
  proof- fix p1 p2 assume "p1 tagged_division_of {a..b} \<inter> {x. x $$ k \<le> c}" "d fine p1" note p1=tagged_division_ofD[OF this(1)] this
hoelzl@37489
  1693
                   assume "p2 tagged_division_of {a..b} \<inter> {x. c \<le> x $$ k}" "d fine p2" note p2=tagged_division_ofD[OF this(1)] this
himmelma@35172
  1694
    note tagged_division_union_interval[OF p1(7) p2(7)] note p12 = tagged_division_ofD[OF this] this
himmelma@35172
  1695
    have "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - i) = norm ((\<Sum>(x, k)\<in>p1 \<union> p2. content k *\<^sub>R f x) - i)"
himmelma@35172
  1696
      apply(subst setsum_Un_zero) apply(rule p1 p2)+ apply(rule) unfolding split_paired_all split_conv
himmelma@35172
  1697
    proof- fix a b assume ab:"(a,b) \<in> p1 \<inter> p2"
himmelma@35172
  1698
      have "(a,b) \<in> p1" using ab by auto from p1(4)[OF this] guess u v apply-by(erule exE)+ note uv =this
hoelzl@37489
  1699
      have "b \<subseteq> {x. x$$k = c}" using ab p1(3)[of a b] p2(3)[of a b] by fastsimp
hoelzl@37489
  1700
      moreover have "interior {x::'a. x $$ k = c} = {}" 
hoelzl@37489
  1701
      proof(rule ccontr) case goal1 then obtain x where x:"x\<in>interior {x::'a. x$$k = c}" by auto
himmelma@35172
  1702
        then guess e unfolding mem_interior .. note e=this
hoelzl@37489
  1703
        have x:"x$$k = c" using x interior_subset by fastsimp
hoelzl@37489
  1704
        have *:"\<And>i. i<DIM('a) \<Longrightarrow> \<bar>(x - (x + (\<chi>\<chi> i. if i = k then e / 2 else 0))) $$ i\<bar>
hoelzl@37489
  1705
          = (if i = k then e/2 else 0)" using e by auto
hoelzl@37489
  1706
        have "(\<Sum>i<DIM('a). \<bar>(x - (x + (\<chi>\<chi> i. if i = k then e / 2 else 0))) $$ i\<bar>) =
hoelzl@37489
  1707
          (\<Sum>i<DIM('a). (if i = k then e / 2 else 0))" apply(rule setsum_cong2) apply(subst *) by auto
hoelzl@37489
  1708
        also have "... < e" apply(subst setsum_delta) using e by auto 
hoelzl@37489
  1709
        finally have "x + (\<chi>\<chi> i. if i = k then e/2 else 0) \<in> ball x e" unfolding mem_ball dist_norm
hoelzl@37489
  1710
          by(rule le_less_trans[OF norm_le_l1])
hoelzl@37489
  1711
        hence "x + (\<chi>\<chi> i. if i = k then e/2 else 0) \<in> {x. x$$k = c}" using e by auto
hoelzl@37489
  1712
        thus False unfolding mem_Collect_eq using e x k by auto
himmelma@35172
  1713
      qed ultimately have "content b = 0" unfolding uv content_eq_0_interior apply-apply(drule subset_interior) by auto
himmelma@35172
  1714
      thus "content b *\<^sub>R f a = 0" by auto
himmelma@35172
  1715
    qed auto
hoelzl@37489
  1716
    also have "\<dots> < e" by(rule k d(2) p12 fine_union p1 p2)+
himmelma@35172
  1717
    finally show "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - i) < e" . qed qed
himmelma@35172
  1718
hoelzl@37489
  1719
lemma integrable_split[intro]: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::{real_normed_vector,complete_space}"
hoelzl@37489
  1720
  assumes "f integrable_on {a..b}" and k:"k<DIM('a)"
hoelzl@37489
  1721
  shows "f integrable_on ({a..b} \<inter> {x. x$$k \<le> c})" (is ?t1) and "f integrable_on ({a..b} \<inter> {x. x$$k \<ge> c})" (is ?t2) 
hoelzl@37489
  1722
proof- guess y using assms(1) unfolding integrable_on_def .. note y=this
hoelzl@37489
  1723
  def b' \<equiv> "(\<chi>\<chi> i. if i = k then min (b$$k) c else b$$i)::'a"
hoelzl@37489
  1724
  and a' \<equiv> "(\<chi>\<chi> i. if i = k then max (a$$k) c else a$$i)::'a"
hoelzl@37489
  1725
  show ?t1 ?t2 unfolding interval_split[OF k] integrable_cauchy unfolding interval_split[THEN sym,OF k]
himmelma@35172
  1726
  proof(rule_tac[!] allI impI)+ fix e::real assume "e>0" hence "e/2>0" by auto
hoelzl@37489
  1727
    from has_integral_separate_sides[OF y this k,of c] guess d . note d=this[rule_format]
hoelzl@37489
  1728
    let ?P = "\<lambda>A. \<exists>d. gauge d \<and> (\<forall>p1 p2. p1 tagged_division_of {a..b} \<inter> A \<and> d fine p1
hoelzl@37489
  1729
      \<and> p2 tagged_division_of {a..b} \<inter> A \<and> d fine p2 \<longrightarrow>
hoelzl@37489
  1730
      norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x)) < e)"
hoelzl@37489
  1731
    show "?P {x. x $$ k \<le> c}" apply(rule_tac x=d in exI) apply(rule,rule d) apply(rule,rule,rule)
hoelzl@37489
  1732
    proof- fix p1 p2 assume as:"p1 tagged_division_of {a..b} \<inter> {x. x $$ k \<le> c} \<and> d fine p1
hoelzl@37489
  1733
        \<and> p2 tagged_division_of {a..b} \<inter> {x. x $$ k \<le> c} \<and> d fine p2"
himmelma@35172
  1734
      show "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x)) < e"
himmelma@35172
  1735
      proof- guess p using fine_division_exists[OF d(1), of a' b] . note p=this
himmelma@35172
  1736
        show ?thesis using norm_triangle_half_l[OF d(2)[of p1 p] d(2)[of p2 p]]
hoelzl@37489
  1737
          using as unfolding interval_split[OF k] b'_def[symmetric] a'_def[symmetric]
haftmann@36350
  1738
          using p using assms by(auto simp add:algebra_simps)
himmelma@35172
  1739
      qed qed  
hoelzl@37489
  1740
    show "?P {x. x $$ k \<ge> c}" apply(rule_tac x=d in exI) apply(rule,rule d) apply(rule,rule,rule)
hoelzl@37489
  1741
    proof- fix p1 p2 assume as:"p1 tagged_division_of {a..b} \<inter> {x. x $$ k \<ge> c} \<and> d fine p1
hoelzl@37489
  1742
        \<and> p2 tagged_division_of {a..b} \<inter> {x. x $$ k \<ge> c} \<and> d fine p2"
himmelma@35172
  1743
      show "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x)) < e"
himmelma@35172
  1744
      proof- guess p using fine_division_exists[OF d(1), of a b'] . note p=this
himmelma@35172
  1745
        show ?thesis using norm_triangle_half_l[OF d(2)[of p p1] d(2)[of p p2]]
hoelzl@37489
  1746
          using as unfolding interval_split[OF k] b'_def[symmetric] a'_def[symmetric]
haftmann@36350
  1747
          using p using assms by(auto simp add:algebra_simps) qed qed qed qed
himmelma@35172
  1748
himmelma@35172
  1749
subsection {* Generalized notion of additivity. *}
himmelma@35172
  1750
himmelma@35172
  1751
definition "neutral opp = (SOME x. \<forall>y. opp x y = y \<and> opp y x = y)"
himmelma@35172
  1752
hoelzl@37489
  1753
definition operative :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (('b::ordered_euclidean_space) set \<Rightarrow> 'a) \<Rightarrow> bool" where
himmelma@35172
  1754
  "operative opp f \<equiv> 
himmelma@35172
  1755
    (\<forall>a b. content {a..b} = 0 \<longrightarrow> f {a..b} = neutral(opp)) \<and>
hoelzl@37489
  1756
    (\<forall>a b c. \<forall>k<DIM('b). f({a..b}) =
hoelzl@37489
  1757
                   opp (f({a..b} \<inter> {x. x$$k \<le> c}))
hoelzl@37489
  1758
                       (f({a..b} \<inter> {x. x$$k \<ge> c})))"
hoelzl@37489
  1759
hoelzl@37489
  1760
lemma operativeD[dest]: fixes type::"'a::ordered_euclidean_space"  assumes "operative opp f"
hoelzl@37489
  1761
  shows "\<And>a b. content {a..b} = 0 \<Longrightarrow> f {a..b::'a} = neutral(opp)"
hoelzl@37489
  1762
  "\<And>a b c k. k<DIM('a) \<Longrightarrow> f({a..b}) = opp (f({a..b} \<inter> {x. x$$k \<le> c})) (f({a..b} \<inter> {x. x$$k \<ge> c}))"
himmelma@35172
  1763
  using assms unfolding operative_def by auto
himmelma@35172
  1764
himmelma@35172
  1765
lemma operative_trivial:
himmelma@35172
  1766
 "operative opp f \<Longrightarrow> content({a..b}) = 0 \<Longrightarrow> f({a..b}) = neutral opp"
himmelma@35172
  1767
  unfolding operative_def by auto
himmelma@35172
  1768
himmelma@35172
  1769
lemma property_empty_interval:
himmelma@35172
  1770
 "(\<forall>a b. content({a..b}) = 0 \<longrightarrow> P({a..b})) \<Longrightarrow> P {}" 
himmelma@35172
  1771
  using content_empty unfolding empty_as_interval by auto
himmelma@35172
  1772
himmelma@35172
  1773
lemma operative_empty: "operative opp f \<Longrightarrow> f {} = neutral opp"
himmelma@35172
  1774
  unfolding operative_def apply(rule property_empty_interval) by auto
himmelma@35172
  1775
himmelma@35172
  1776
subsection {* Using additivity of lifted function to encode definedness. *}
himmelma@35172
  1777
himmelma@35172
  1778
lemma forall_option: "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>x. P(Some x))"
huffman@36362
  1779
  by (metis option.nchotomy)
himmelma@35172
  1780
himmelma@35172
  1781
lemma exists_option:
himmelma@35172
  1782
 "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P(Some x))" 
huffman@36362
  1783
  by (metis option.nchotomy)
himmelma@35172
  1784
himmelma@35172
  1785
fun lifted where 
himmelma@35172
  1786
  "lifted (opp::'a\<Rightarrow>'a\<Rightarrow>'b) (Some x) (Some y) = Some(opp x y)" |
himmelma@35172
  1787
  "lifted opp None _ = (None::'b option)" |
himmelma@35172
  1788
  "lifted opp _ None = None"
himmelma@35172
  1789
himmelma@35172
  1790
lemma lifted_simp_1[simp]: "lifted opp v None = None"
himmelma@35172
  1791
  apply(induct v) by auto
himmelma@35172
  1792
himmelma@35172
  1793
definition "monoidal opp \<equiv>  (\<forall>x y. opp x y = opp y x) \<and>
himmelma@35172
  1794
                   (\<forall>x y z. opp x (opp y z) = opp (opp x y) z) \<and>
himmelma@35172
  1795
                   (\<forall>x. opp (neutral opp) x = x)"
himmelma@35172
  1796
himmelma@35172
  1797
lemma monoidalI: assumes "\<And>x y. opp x y = opp y x"
himmelma@35172
  1798
  "\<And>x y z. opp x (opp y z) = opp (opp x y) z"
himmelma@35172
  1799
  "\<And>x. opp (neutral opp) x = x" shows "monoidal opp"
himmelma@35172
  1800
  unfolding monoidal_def using assms by fastsimp
himmelma@35172
  1801
himmelma@35172
  1802
lemma monoidal_ac: assumes "monoidal opp"
himmelma@35172
  1803
  shows "opp (neutral opp) a = a" "opp a (neutral opp) = a" "opp a b = opp b a"
himmelma@35172
  1804
  "opp (opp a b) c = opp a (opp b c)"  "opp a (opp b c) = opp b (opp a c)"
himmelma@35172
  1805
  using assms unfolding monoidal_def apply- by metis+
himmelma@35172
  1806
himmelma@35172
  1807
lemma monoidal_simps[simp]: assumes "monoidal opp"
himmelma@35172
  1808
  shows "opp (neutral opp) a = a" "opp a (neutral opp) = a"
himmelma@35172
  1809
  using monoidal_ac[OF assms] by auto
himmelma@35172
  1810
himmelma@35172
  1811
lemma neutral_lifted[cong]: assumes "monoidal opp"
himmelma@35172
  1812
  shows "neutral (lifted opp) = Some(neutral opp)"
himmelma@35172
  1813
  apply(subst neutral_def) apply(rule some_equality) apply(rule,induct_tac y) prefer 3
himmelma@35172
  1814
proof- fix x assume "\<forall>y. lifted opp x y = y \<and> lifted opp y x = y"
himmelma@35172
  1815
  thus "x = Some (neutral opp)" apply(induct x) defer
himmelma@35172
  1816
    apply rule apply(subst neutral_def) apply(subst eq_commute,rule some_equality)
himmelma@35172
  1817
    apply(rule,erule_tac x="Some y" in allE) defer apply(erule_tac x="Some x" in allE) by auto
himmelma@35172
  1818
qed(auto simp add:monoidal_ac[OF assms])
himmelma@35172
  1819
himmelma@35172
  1820
lemma monoidal_lifted[intro]: assumes "monoidal opp" shows "monoidal(lifted opp)"
himmelma@35172
  1821
  unfolding monoidal_def forall_option neutral_lifted[OF assms] using monoidal_ac[OF assms] by auto
himmelma@35172
  1822
himmelma@35172
  1823
definition "support opp f s = {x. x\<in>s \<and> f x \<noteq> neutral opp}"
himmelma@35172
  1824
definition "fold' opp e s \<equiv> (if finite s then fold opp e s else e)"
himmelma@35172
  1825
definition "iterate opp s f \<equiv> fold' (\<lambda>x a. opp (f x) a) (neutral opp) (support opp f s)"
himmelma@35172
  1826
himmelma@35172
  1827
lemma support_subset[intro]:"support opp f s \<subseteq> s" unfolding support_def by auto
himmelma@35172
  1828
lemma support_empty[simp]:"support opp f {} = {}" using support_subset[of opp f "{}"] by auto
himmelma@35172
  1829
himmelma@35172
  1830
lemma fun_left_comm_monoidal[intro]: assumes "monoidal opp" shows "fun_left_comm opp"
himmelma@35172
  1831
  unfolding fun_left_comm_def using monoidal_ac[OF assms] by auto
himmelma@35172
  1832
himmelma@35172
  1833
lemma support_clauses:
himmelma@35172
  1834
  "\<And>f g s. support opp f {} = {}"
himmelma@35172
  1835
  "\<And>f g s. support opp f (insert x s) = (if f(x) = neutral opp then support opp f s else insert x (support opp f s))"
himmelma@35172
  1836
  "\<And>f g s. support opp f (s - {x}) = (support opp f s) - {x}"
himmelma@35172
  1837
  "\<And>f g s. support opp f (s \<union> t) = (support opp f s) \<union> (support opp f t)"
himmelma@35172
  1838
  "\<And>f g s. support opp f (s \<inter> t) = (support opp f s) \<inter> (support opp f t)"
himmelma@35172
  1839
  "\<And>f g s. support opp f (s - t) = (support opp f s) - (support opp f t)"
himmelma@35172
  1840
  "\<And>f g s. support opp g (f ` s) = f ` (support opp (g o f) s)"
himmelma@35172
  1841
unfolding support_def by auto
himmelma@35172
  1842
himmelma@35172
  1843
lemma finite_support[intro]:"finite s \<Longrightarrow> finite (support opp f s)"
himmelma@35172
  1844
  unfolding support_def by auto
himmelma@35172
  1845
himmelma@35172
  1846
lemma iterate_empty[simp]:"iterate opp {} f = neutral opp"
himmelma@35172
  1847
  unfolding iterate_def fold'_def by auto 
himmelma@35172
  1848
himmelma@35172
  1849
lemma iterate_insert[simp]: assumes "monoidal opp" "finite s"
himmelma@35172
  1850
  shows "iterate opp (insert x s) f = (if x \<in> s then iterate opp s f else opp (f x) (iterate opp s f))" 
himmelma@35172
  1851
proof(cases "x\<in>s") case True hence *:"insert x s = s" by auto
himmelma@35172
  1852
  show ?thesis unfolding iterate_def if_P[OF True] * by auto
himmelma@35172
  1853
next case False note x=this
himmelma@35172
  1854
  note * = fun_left_comm.fun_left_comm_apply[OF fun_left_comm_monoidal[OF assms(1)]]
himmelma@35172
  1855
  show ?thesis proof(cases "f x = neutral opp")
himmelma@35172
  1856
    case True show ?thesis unfolding iterate_def if_not_P[OF x] support_clauses if_P[OF True]
himmelma@35172
  1857
      unfolding True monoidal_simps[OF assms(1)] by auto
himmelma@35172
  1858
  next case False show ?thesis unfolding iterate_def fold'_def  if_not_P[OF x] support_clauses if_not_P[OF False]
himmelma@35172
  1859
      apply(subst fun_left_comm.fold_insert[OF * finite_support])
himmelma@35172
  1860
      using `finite s` unfolding support_def using False x by auto qed qed 
himmelma@35172
  1861
himmelma@35172
  1862
lemma iterate_some:
himmelma@35172
  1863
  assumes "monoidal opp"  "finite s"
himmelma@35172
  1864
  shows "iterate (lifted opp) s (\<lambda>x. Some(f x)) = Some (iterate opp s f)" using assms(2)
himmelma@35172
  1865
proof(induct s) case empty thus ?case using assms by auto
himmelma@35172
  1866
next case (insert x F) show ?case apply(subst iterate_insert) prefer 3 apply(subst if_not_P)
himmelma@35172
  1867
    defer unfolding insert(3) lifted.simps apply rule using assms insert by auto qed
himmelma@35172
  1868
subsection {* Two key instances of additivity. *}
himmelma@35172
  1869
himmelma@35172
  1870
lemma neutral_add[simp]:
himmelma@35172
  1871
  "neutral op + = (0::_::comm_monoid_add)" unfolding neutral_def 
himmelma@35172
  1872
  apply(rule some_equality) defer apply(erule_tac x=0 in allE) by auto
himmelma@35172
  1873
hoelzl@37489
  1874
lemma operative_content[intro]: "operative (op +) content" 
hoelzl@37489
  1875
  unfolding operative_def neutral_add apply safe 
hoelzl@37489
  1876
  unfolding content_split[THEN sym] ..
himmelma@35172
  1877
huffman@36362
  1878
lemma neutral_monoid: "neutral ((op +)::('a::comm_monoid_add) \<Rightarrow> 'a \<Rightarrow> 'a) = 0"
huffman@36362
  1879
  by (rule neutral_add) (* FIXME: duplicate *)
himmelma@35172
  1880
himmelma@35172
  1881
lemma monoidal_monoid[intro]:
himmelma@35172
  1882
  shows "monoidal ((op +)::('a::comm_monoid_add) \<Rightarrow> 'a \<Rightarrow> 'a)"
haftmann@36350
  1883
  unfolding monoidal_def neutral_monoid by(auto simp add: algebra_simps) 
himmelma@35172
  1884
hoelzl@37489
  1885
lemma operative_integral: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::banach"
himmelma@35172
  1886
  shows "operative (lifted(op +)) (\<lambda>i. if f integrable_on i then Some(integral i f) else None)"
himmelma@35172
  1887
  unfolding operative_def unfolding neutral_lifted[OF monoidal_monoid] neutral_add
hoelzl@37489
  1888
  apply(rule,rule,rule,rule) defer apply(rule allI impI)+
hoelzl@37489
  1889
proof- fix a b c k assume k:"k<DIM('a)" show "(if f integrable_on {a..b} then Some (integral {a..b} f) else None) =
hoelzl@37489
  1890
    lifted op + (if f integrable_on {a..b} \<inter> {x. x $$ k \<le> c} then Some (integral ({a..b} \<inter> {x. x $$ k \<le> c}) f) else None)
hoelzl@37489
  1891
    (if f integrable_on {a..b} \<inter> {x. c \<le> x $$ k} then Some (integral ({a..b} \<inter> {x. c \<le> x $$ k}) f) else None)"
himmelma@35172
  1892
  proof(cases "f integrable_on {a..b}") 
hoelzl@37489
  1893
    case True show ?thesis unfolding if_P[OF True] using k apply-
hoelzl@37489
  1894
      unfolding if_P[OF integrable_split(1)[OF True]] unfolding if_P[OF integrable_split(2)[OF True]]
hoelzl@37489
  1895
      unfolding lifted.simps option.inject apply(rule integral_unique) apply(rule has_integral_split[OF _ _ k]) 
hoelzl@37489
  1896
      apply(rule_tac[!] integrable_integral integrable_split)+ using True k by auto
hoelzl@37489
  1897
  next case False have "(\<not> (f integrable_on {a..b} \<inter> {x. x $$ k \<le> c})) \<or> (\<not> ( f integrable_on {a..b} \<inter> {x. c \<le> x $$ k}))"
himmelma@35172
  1898
    proof(rule ccontr) case goal1 hence "f integrable_on {a..b}" apply- unfolding integrable_on_def
hoelzl@37489
  1899
        apply(rule_tac x="integral ({a..b} \<inter> {x. x $$ k \<le> c}) f + integral ({a..b} \<inter> {x. x $$ k \<ge> c}) f" in exI)
hoelzl@37489
  1900
        apply(rule has_integral_split[OF _ _ k]) apply(rule_tac[!] integrable_integral) by auto
himmelma@35172
  1901
      thus False using False by auto
himmelma@35172
  1902
    qed thus ?thesis using False by auto 
himmelma@35172
  1903
  qed next 
hoelzl@37489
  1904
  fix a b assume as:"content {a..b::'a} = 0"
himmelma@35172
  1905
  thus "(if f integrable_on {a..b} then Some (integral {a..b} f) else None) = Some 0"
himmelma@35172
  1906
    unfolding if_P[OF integrable_on_null[OF as]] using has_integral_null_eq[OF as] by auto qed
himmelma@35172
  1907
himmelma@35172
  1908
subsection {* Points of division of a partition. *}
himmelma@35172
  1909
hoelzl@37489
  1910
definition "division_points (k::('a::ordered_euclidean_space) set) d = 
hoelzl@37489
  1911
    {(j,x). j<DIM('a) \<and> (interval_lowerbound k)$$j < x \<and> x < (interval_upperbound k)$$j \<and>
hoelzl@37489
  1912
           (\<exists>i\<in>d. (interval_lowerbound i)$$j = x \<or> (interval_upperbound i)$$j = x)}"
hoelzl@37489
  1913
hoelzl@37489
  1914
lemma division_points_finite: fixes i::"('a::ordered_euclidean_space) set"
hoelzl@37489
  1915
  assumes "d division_of i" shows "finite (division_points i d)"
himmelma@35172
  1916
proof- note assm = division_ofD[OF assms]
hoelzl@37489
  1917
  let ?M = "\<lambda>j. {(j,x)|x. (interval_lowerbound i)$$j < x \<and> x < (interval_upperbound i)$$j \<and>
hoelzl@37489
  1918
           (\<exists>i\<in>d. (interval_lowerbound i)$$j = x \<or> (interval_upperbound i)$$j = x)}"
hoelzl@37489
  1919
  have *:"division_points i d = \<Union>(?M ` {..<DIM('a)})"
himmelma@35172
  1920
    unfolding division_points_def by auto
himmelma@35172
  1921
  show ?thesis unfolding * using assm by auto qed
himmelma@35172
  1922
hoelzl@37489
  1923
lemma division_points_subset: fixes a::"'a::ordered_euclidean_space"
hoelzl@37489
  1924
  assumes "d division_of {a..b}" "\<forall>i<DIM('a). a$$i < b$$i"  "a$$k < c" "c < b$$k" and k:"k<DIM('a)"
hoelzl@37489
  1925
  shows "division_points ({a..b} \<inter> {x. x$$k \<le> c}) {l \<inter> {x. x$$k \<le> c} | l . l \<in> d \<and> ~(l \<inter> {x. x$$k \<le> c} = {})}
himmelma@35172
  1926
                  \<subseteq> division_points ({a..b}) d" (is ?t1) and
hoelzl@37489
  1927
        "division_points ({a..b} \<inter> {x. x$$k \<ge> c}) {l \<inter> {x. x$$k \<ge> c} | l . l \<in> d \<and> ~(l \<inter> {x. x$$k \<ge> c} = {})}
himmelma@35172
  1928
                  \<subseteq> division_points ({a..b}) d" (is ?t2)
himmelma@35172
  1929
proof- note assm = division_ofD[OF assms(1)]
hoelzl@37489
  1930
  have *:"\<forall>i<DIM('a). a$$i \<le> b$$i"   "\<forall>i<DIM('a). a$$i \<le> ((\<chi>\<chi> i. if i = k then min (b $$ k) c else b $$ i)::'a) $$ i"
hoelzl@37489
  1931
    "\<forall>i<DIM('a). ((\<chi>\<chi> i. if i = k then max (a $$ k) c else a $$ i)::'a) $$ i \<le> b$$i"  "min (b $$ k) c = c" "max (a $$ k) c = c"
himmelma@35172
  1932
    using assms using less_imp_le by auto
hoelzl@37489
  1933
  show ?t1 unfolding division_points_def interval_split[OF k, of a b]
hoelzl@37489
  1934
    unfolding interval_bounds[OF *(1)] interval_bounds[OF *(2)] interval_bounds[OF *(3)] unfolding *
hoelzl@37489
  1935
    unfolding subset_eq apply(rule) unfolding mem_Collect_eq split_beta apply(erule bexE conjE)+
hoelzl@37489
  1936
    unfolding mem_Collect_eq apply(erule exE conjE)+ unfolding euclidean_lambda_beta'
hoelzl@37489
  1937
  proof- fix i l x assume as:"a $$ fst x < snd x" "snd x < (if fst x = k then c else b $$ fst x)"
hoelzl@37489
  1938
      "interval_lowerbound i $$ fst x = snd x \<or> interval_upperbound i $$ fst x = snd x"
hoelzl@37489
  1939
      "i = l \<inter> {x. x $$ k \<le> c}" "l \<in> d" "l \<inter> {x. x $$ k \<le> c} \<noteq> {}" and fstx:"fst x <DIM('a)"
himmelma@35172
  1940
    from assm(4)[OF this(5)] guess u v apply-by(erule exE)+ note l=this
hoelzl@37489
  1941
    have *:"\<forall>i<DIM('a). u $$ i \<le> ((\<chi>\<chi> i. if i = k then min (v $$ k) c else v $$ i)::'a) $$ i"
hoelzl@37489
  1942
      using as(6) unfolding l interval_split[OF k] interval_ne_empty as .
hoelzl@37489
  1943
    have **:"\<forall>i<DIM('a). u$$i \<le> v$$i" using l using as(6) unfolding interval_ne_empty[THEN sym] by auto
hoelzl@37489
  1944
    show "fst x <DIM('a) \<and> a $$ fst x < snd x \<and> snd x < b $$ fst x \<and> (\<exists>i\<in>d. interval_lowerbound i $$ fst x = snd x
hoelzl@37489
  1945
      \<or> interval_upperbound i $$ fst x = snd x)" apply(rule,rule fstx)
hoelzl@37489
  1946
      using as(1-3,5) unfolding l interval_split[OF k] interval_ne_empty as interval_bounds[OF *] apply-
himmelma@35172
  1947
      apply(rule,assumption,rule) defer apply(rule_tac x="{u..v}" in bexI) unfolding interval_bounds[OF **]
hoelzl@37489
  1948
      apply(case_tac[!] "fst x = k") using assms fstx apply- unfolding euclidean_lambda_beta by auto
himmelma@35172
  1949
  qed
hoelzl@37489
  1950
  show ?t2 unfolding division_points_def interval_split[OF k, of a b]
hoelzl@37489
  1951
    unfolding interval_bounds[OF *(1)] interval_bounds[OF *(2)] interval_bounds[OF *(3)] unfolding *
hoelzl@37489
  1952
    unfolding subset_eq apply(rule) unfolding mem_Collect_eq split_beta apply(erule bexE conjE)+
hoelzl@37489
  1953
    unfolding mem_Collect_eq apply(erule exE conjE)+ unfolding euclidean_lambda_beta' apply(rule,assumption)
hoelzl@37489
  1954
  proof- fix i l x assume as:"(if fst x = k then c else a $$ fst x) < snd x" "snd x < b $$ fst x"
hoelzl@37489
  1955
      "interval_lowerbound i $$ fst x = snd x \<or> interval_upperbound i $$ fst x = snd x" 
hoelzl@37489
  1956
      "i = l \<inter> {x. c \<le> x $$ k}" "l \<in> d" "l \<inter> {x. c \<le> x $$ k} \<noteq> {}" and fstx:"fst x < DIM('a)"
himmelma@35172
  1957
    from assm(4)[OF this(5)] guess u v apply-by(erule exE)+ note l=this
hoelzl@37489
  1958
    have *:"\<forall>i<DIM('a). ((\<chi>\<chi> i. if i = k then max (u $$ k) c else u $$ i)::'a) $$ i \<le> v $$ i"
hoelzl@37489
  1959
      using as(6) unfolding l interval_split[OF k] interval_ne_empty as .
hoelzl@37489
  1960
    have **:"\<forall>i<DIM('a). u$$i \<le> v$$i" using l using as(6) unfolding interval_ne_empty[THEN sym] by auto
hoelzl@37489
  1961
    show "a $$ fst x < snd x \<and> snd x < b $$ fst x \<and> (\<exists>i\<in>d. interval_lowerbound i $$ fst x = snd x \<or>
hoelzl@37489
  1962
      interval_upperbound i $$ fst x = snd x)"
hoelzl@37489
  1963
      using as(1-3,5) unfolding l interval_split[OF k] interval_ne_empty as interval_bounds[OF *] apply-
himmelma@35172
  1964
      apply rule defer apply(rule,assumption) apply(rule_tac x="{u..v}" in bexI) unfolding interval_bounds[OF **]
hoelzl@37489
  1965
      apply(case_tac[!] "fst x = k") using assms fstx apply-  by(auto simp add:euclidean_lambda_beta'[OF k]) qed qed
hoelzl@37489
  1966
hoelzl@37489
  1967
lemma division_points_psubset: fixes a::"'a::ordered_euclidean_space"
hoelzl@37489
  1968
  assumes "d division_of {a..b}"  "\<forall>i<DIM('a). a$$i < b$$i"  "a$$k < c" "c < b$$k"
hoelzl@37489
  1969
  "l \<in> d" "interval_lowerbound l$$k = c \<or> interval_upperbound l$$k = c" and k:"k<DIM('a)"
hoelzl@37489
  1970
  shows "division_points ({a..b} \<inter> {x. x$$k \<le> c}) {l \<inter> {x. x$$k \<le> c} | l. l\<in>d \<and> l \<inter> {x. x$$k \<le> c} \<noteq> {}}
hoelzl@37489
  1971
              \<subset> division_points ({a..b}) d" (is "?D1 \<subset> ?D") 
hoelzl@37489
  1972
        "division_points ({a..b} \<inter> {x. x$$k \<ge> c}) {l \<inter> {x. x$$k \<ge> c} | l. l\<in>d \<and> l \<inter> {x. x$$k \<ge> c} \<noteq> {}}
hoelzl@37489
  1973
              \<subset> division_points ({a..b}) d" (is "?D2 \<subset> ?D") 
hoelzl@37489
  1974
proof- have ab:"\<forall>i<DIM('a). a$$i \<le> b$$i" using assms(2) by(auto intro!:less_imp_le)
himmelma@35172
  1975
  guess u v using division_ofD(4)[OF assms(1,5)] apply-by(erule exE)+ note l=this
hoelzl@37489
  1976
  have uv:"\<forall>i<DIM('a). u$$i \<le> v$$i" "\<forall>i<DIM('a). a$$i \<le> u$$i \<and> v$$i \<le> b$$i"
hoelzl@37489
  1977
    using division_ofD(2,2,3)[OF assms(1,5)] unfolding l interval_ne_empty
himmelma@35172
  1978
    unfolding subset_eq apply- defer apply(erule_tac x=u in ballE, erule_tac x=v in ballE) unfolding mem_interval by auto
hoelzl@37489
  1979
  have *:"interval_upperbound ({a..b} \<inter> {x. x $$ k \<le> interval_upperbound l $$ k}) $$ k = interval_upperbound l $$ k"
hoelzl@37489
  1980
         "interval_upperbound ({a..b} \<inter> {x. x $$ k \<le> interval_lowerbound l $$ k}) $$ k = interval_lowerbound l $$ k"
hoelzl@37489
  1981
    unfolding interval_split[OF k] apply(subst interval_bounds) prefer 3 apply(subst interval_bounds)
hoelzl@37489
  1982
    unfolding l interval_bounds[OF uv(1)] using uv[rule_format,of k] ab k by auto
himmelma@35172
  1983
  have "\<exists>x. x \<in> ?D - ?D1" using assms(2-) apply-apply(erule disjE)
hoelzl@37489
  1984
    apply(rule_tac x="(k,(interval_lowerbound l)$$k)" in exI) defer
hoelzl@37489
  1985
    apply(rule_tac x="(k,(interval_upperbound l)$$k)" in exI)
hoelzl@37489
  1986
    unfolding division_points_def unfolding interval_bounds[OF ab] by(auto simp add:*) 
hoelzl@37489
  1987
  thus "?D1 \<subset> ?D" apply-apply(rule,rule division_points_subset[OF assms(1-4)]) using k by auto
hoelzl@37489
  1988
hoelzl@37489
  1989
  have *:"interval_lowerbound ({a..b} \<inter> {x. x $$ k \<ge> interval_lowerbound l $$ k}) $$ k = interval_lowerbound l $$ k"
hoelzl@37489
  1990
         "interval_lowerbound ({a..b} \<inter> {x. x $$ k \<ge> interval_upperbound l $$ k}) $$ k = interval_upperbound l $$ k"
hoelzl@37489
  1991
    unfolding interval_split[OF k] apply(subst interval_bounds) prefer 3 apply(subst interval_bounds)
hoelzl@37489
  1992
    unfolding l interval_bounds[OF uv(1)] using uv[rule_format,of k] ab k by auto
himmelma@35172
  1993
  have "\<exists>x. x \<in> ?D - ?D2" using assms(2-) apply-apply(erule disjE)
hoelzl@37489
  1994
    apply(rule_tac x="(k,(interval_lowerbound l)$$k)" in exI) defer
hoelzl@37489
  1995
    apply(rule_tac x="(k,(interval_upperbound l)$$k)" in exI)
hoelzl@37489
  1996
    unfolding division_points_def unfolding interval_bounds[OF ab] by(auto simp add:*) 
hoelzl@37489
  1997
  thus "?D2 \<subset> ?D" apply-apply(rule,rule division_points_subset[OF assms(1-4) k]) by auto qed
himmelma@35172
  1998
himmelma@35172
  1999
subsection {* Preservation by divisions and tagged divisions. *}
himmelma@35172
  2000
himmelma@35172
  2001
lemma support_support[simp]:"support opp f (support opp f s) = support opp f s"
himmelma@35172
  2002
  unfolding support_def by auto
himmelma@35172
  2003
himmelma@35172
  2004
lemma iterate_support[simp]: "iterate opp (support opp f s) f = iterate opp s f"
himmelma@35172
  2005
  unfolding iterate_def support_support by auto
himmelma@35172
  2006
himmelma@35172
  2007
lemma iterate_expand_cases:
himmelma@35172
  2008
  "iterate opp s f = (if finite(support opp f s) then iterate opp (support opp f s) f else neutral opp)"
himmelma@35172
  2009
  apply(cases) apply(subst if_P,assumption) unfolding iterate_def support_support fold'_def by auto 
himmelma@35172
  2010
himmelma@35172
  2011
lemma iterate_image: assumes "monoidal opp"  "inj_on f s"
himmelma@35172
  2012
  shows "iterate opp (f ` s) g = iterate opp s (g \<circ> f)"
himmelma@35172
  2013
proof- have *:"\<And>s. finite s \<Longrightarrow>  \<forall>x\<in>s. \<forall>y\<in>s. f x = f y \<longrightarrow> x = y \<Longrightarrow>
himmelma@35172
  2014
     iterate opp (f ` s) g = iterate opp s (g \<circ> f)"
himmelma@35172
  2015
  proof- case goal1 show ?case using goal1
himmelma@35172
  2016
    proof(induct s) case empty thus ?case using assms(1) by auto
himmelma@35172
  2017
    next case (insert x s) show ?case unfolding iterate_insert[OF assms(1) insert(1)]
himmelma@35172
  2018
        unfolding if_not_P[OF insert(2)] apply(subst insert(3)[THEN sym])
himmelma@35172
  2019
        unfolding image_insert defer apply(subst iterate_insert[OF assms(1)])
himmelma@35172
  2020
        apply(rule finite_imageI insert)+ apply(subst if_not_P)
himmelma@35172
  2021
        unfolding image_iff o_def using insert(2,4) by auto
himmelma@35172
  2022
    qed qed
himmelma@35172
  2023
  show ?thesis 
himmelma@35172
  2024
    apply(cases "finite (support opp g (f ` s))")
himmelma@35172
  2025
    apply(subst (1) iterate_support[THEN sym],subst (2) iterate_support[THEN sym])
himmelma@35172
  2026
    unfolding support_clauses apply(rule *)apply(rule finite_imageD,assumption) unfolding inj_on_def[symmetric]
himmelma@35172
  2027
    apply(rule subset_inj_on[OF assms(2) support_subset])+
himmelma@35172
  2028
    apply(subst iterate_expand_cases) unfolding support_clauses apply(simp only: if_False)
himmelma@35172
  2029
    apply(subst iterate_expand_cases) apply(subst if_not_P) by auto qed
himmelma@35172
  2030
himmelma@35172
  2031
himmelma@35172
  2032
(* This lemma about iterations comes up in a few places.                     *)
himmelma@35172
  2033
lemma iterate_nonzero_image_lemma:
himmelma@35172
  2034
  assumes "monoidal opp" "finite s" "g(a) = neutral opp"
himmelma@35172
  2035
  "\<forall>x\<in>s. \<forall>y\<in>s. f x = f y \<and> x \<noteq> y \<longrightarrow> g(f x) = neutral opp"
himmelma@35172
  2036
  shows "iterate opp {f x | x. x \<in> s \<and> f x \<noteq> a} g = iterate opp s (g \<circ> f)"
himmelma@35172
  2037
proof- have *:"{f x |x. x \<in> s \<and> ~(f x = a)} = f ` {x. x \<in> s \<and> ~(f x = a)}" by auto
himmelma@35172
  2038
  have **:"support opp (g \<circ> f) {x \<in> s. f x \<noteq> a} = support opp (g \<circ> f) s"
himmelma@35172
  2039
    unfolding support_def using assms(3) by auto
himmelma@35172
  2040
  show ?thesis unfolding *
himmelma@35172
  2041
    apply(subst iterate_support[THEN sym]) unfolding support_clauses
himmelma@35172
  2042
    apply(subst iterate_image[OF assms(1)]) defer
himmelma@35172
  2043
    apply(subst(2) iterate_support[THEN sym]) apply(subst **)
himmelma@35172
  2044
    unfolding inj_on_def using assms(3,4) unfolding support_def by auto qed
himmelma@35172
  2045
himmelma@35172
  2046
lemma iterate_eq_neutral:
himmelma@35172
  2047
  assumes "monoidal opp"  "\<forall>x \<in> s. (f(x) = neutral opp)"
himmelma@35172
  2048
  shows "(iterate opp s f = neutral opp)"
himmelma@35172
  2049
proof- have *:"support opp f s = {}" unfolding support_def using assms(2) by auto
himmelma@35172
  2050
  show ?thesis apply(subst iterate_support[THEN sym]) 
himmelma@35172
  2051
    unfolding * using assms(1) by auto qed
himmelma@35172
  2052
himmelma@35172
  2053
lemma iterate_op: assumes "monoidal opp" "finite s"
himmelma@35172
  2054
  shows "iterate opp s (\<lambda>x. opp (f x) (g x)) = opp (iterate opp s f) (iterate opp s g)" using assms(2)
himmelma@35172
  2055
proof(induct s) case empty thus ?case unfolding iterate_insert[OF assms(1)] using assms(1) by auto
himmelma@35172
  2056
next case (insert x F) show ?case unfolding iterate_insert[OF assms(1) insert(1)] if_not_P[OF insert(2)] insert(3)
himmelma@35172
  2057
    unfolding monoidal_ac[OF assms(1)] by(rule refl) qed
himmelma@35172
  2058
himmelma@35172
  2059
lemma iterate_eq: assumes "monoidal opp" "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
himmelma@35172
  2060
  shows "iterate opp s f = iterate opp s g"
himmelma@35172
  2061
proof- have *:"support opp g s = support opp f s"
himmelma@35172
  2062
    unfolding support_def using assms(2) by auto
himmelma@35172
  2063
  show ?thesis
himmelma@35172
  2064
  proof(cases "finite (support opp f s)")
himmelma@35172
  2065
    case False thus ?thesis apply(subst iterate_expand_cases,subst(2) iterate_expand_cases)
himmelma@35172
  2066
      unfolding * by auto
himmelma@35172
  2067
  next def su \<equiv> "support opp f s"
himmelma@35172
  2068
    case True note support_subset[of opp f s] 
himmelma@35172
  2069
    thus ?thesis apply- apply(subst iterate_support[THEN sym],subst(2) iterate_support[THEN sym]) unfolding * using True
himmelma@35172
  2070
      unfolding su_def[symmetric]
himmelma@35172
  2071
    proof(induct su) case empty show ?case by auto
himmelma@35172
  2072
    next case (insert x s) show ?case unfolding iterate_insert[OF assms(1) insert(1)] 
himmelma@35172
  2073
        unfolding if_not_P[OF insert(2)] apply(subst insert(3))
himmelma@35172
  2074
        defer apply(subst assms(2)[of x]) using insert by auto qed qed qed
himmelma@35172
  2075
himmelma@35172
  2076
lemma nonempty_witness: assumes "s \<noteq> {}" obtains x where "x \<in> s" using assms by auto
himmelma@35172
  2077
hoelzl@37489
  2078
lemma operative_division: fixes f::"('a::ordered_euclidean_space) set \<Rightarrow> 'b"
himmelma@35172
  2079
  assumes "monoidal opp" "operative opp f" "d division_of {a..b}"
himmelma@35172
  2080
  shows "iterate opp d f = f {a..b}"
himmelma@35172
  2081
proof- def C \<equiv> "card (division_points {a..b} d)" thus ?thesis using assms
himmelma@35172
  2082
  proof(induct C arbitrary:a b d rule:full_nat_induct)
himmelma@35172
  2083
    case goal1
himmelma@35172
  2084
    { presume *:"content {a..b} \<noteq> 0 \<Longrightarrow> ?case"
himmelma@35172
  2085
      thus ?case apply-apply(cases) defer apply assumption
himmelma@35172
  2086
      proof- assume as:"content {a..b} = 0"
himmelma@35172
  2087
        show ?case unfolding operativeD(1)[OF assms(2) as] apply(rule iterate_eq_neutral[OF goal1(2)])
himmelma@35172
  2088
        proof fix x assume x:"x\<in>d"
himmelma@35172
  2089
          then guess u v apply(drule_tac division_ofD(4)[OF goal1(4)]) by(erule exE)+
himmelma@35172
  2090
          thus "f x = neutral opp" using division_of_content_0[OF as goal1(4)] 
himmelma@35172
  2091
            using operativeD(1)[OF assms(2)] x by auto
himmelma@35172
  2092
        qed qed }
himmelma@35172
  2093
    assume "content {a..b} \<noteq> 0" note ab = this[unfolded content_lt_nz[THEN sym] content_pos_lt_eq]
hoelzl@37489
  2094
    hence ab':"\<forall>i<DIM('a). a$$i \<le> b$$i" by (auto intro!: less_imp_le) show ?case 
himmelma@35172
  2095
    proof(cases "division_points {a..b} d = {}")
himmelma@35172
  2096
      case True have d':"\<forall>i\<in>d. \<exists>u v. i = {u..v} \<and>
hoelzl@37489
  2097
        (\<forall>j<DIM('a). u$$j = a$$j \<and> v$$j = a$$j \<or> u$$j = b$$j \<and> v$$j = b$$j \<or> u$$j = a$$j \<and> v$$j = b$$j)"
himmelma@35172
  2098
        unfolding forall_in_division[OF goal1(4)] apply(rule,rule,rule)
hoelzl@37489
  2099
        apply(rule_tac x=a in exI,rule_tac x=b in exI) apply(rule,rule refl) apply(rule,rule)
hoelzl@37489
  2100
      proof- fix u v j assume j:"j<DIM('a)" assume as:"{u..v} \<in> d" note division_ofD(3)[OF goal1(4) this]
hoelzl@37489
  2101
        hence uv:"\<forall>i<DIM('a). u$$i \<le> v$$i" "u$$j \<le> v$$j" using j unfolding interval_ne_empty by auto
hoelzl@37489
  2102
        have *:"\<And>p r Q. \<not> j<DIM('a) \<or> p \<or> r \<or> (\<forall>x\<in>d. Q x) \<Longrightarrow> p \<or> r \<or> (Q {u..v})" using as j by auto
hoelzl@37489
  2103
        have "(j, u$$j) \<notin> division_points {a..b} d"
hoelzl@37489
  2104
          "(j, v$$j) \<notin> division_points {a..b} d" using True by auto
himmelma@35172
  2105
        note this[unfolded de_Morgan_conj division_points_def mem_Collect_eq split_conv interval_bounds[OF ab'] bex_simps]
himmelma@35172
  2106
        note *[OF this(1)] *[OF this(2)] note this[unfolded interval_bounds[OF uv(1)]]
hoelzl@37489