author hoelzl Wed Sep 28 16:15:51 2016 +0200 (2016-09-28) changeset 63956 b235e845c8e8 parent 63955 51a3d38d2281 child 63957 c3da799b1b45
HOL-Analysis: add cover lemma ported by L. C. Paulson
```     1.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Sep 29 12:58:55 2016 +0100
1.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Sep 28 16:15:51 2016 +0200
1.3 @@ -16,6 +16,28 @@
1.4
1.5  subsection \<open>Sundries\<close>
1.6
1.7 +
1.8 +text\<open>A transitive relation is well-founded if all initial segments are finite.\<close>
1.9 +lemma wf_finite_segments:
1.10 +  assumes "irrefl r" and "trans r" and "\<And>x. finite {y. (y, x) \<in> r}"
1.11 +  shows "wf (r)"
1.12 +  apply (simp add: trans_wf_iff wf_iff_acyclic_if_finite converse_def assms)
1.13 +  using acyclic_def assms irrefl_def trans_Restr by fastforce
1.14 +
1.15 +text\<open>For creating values between @{term u} and @{term v}.\<close>
1.16 +lemma scaling_mono:
1.17 +  fixes u::"'a::linordered_field"
1.18 +  assumes "u \<le> v" "0 \<le> r" "r \<le> s"
1.19 +    shows "u + r * (v - u) / s \<le> v"
1.20 +proof -
1.21 +  have "r/s \<le> 1" using assms
1.22 +    using divide_le_eq_1 by fastforce
1.23 +  then have "(r/s) * (v - u) \<le> 1 * (v - u)"
1.24 +    by (meson diff_ge_0_iff_ge mult_right_mono \<open>u \<le> v\<close>)
1.25 +  then show ?thesis
1.26 +    by (simp add: field_simps)
1.27 +qed
1.28 +
1.29  lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
1.30  lemma conjunctD3: assumes "a \<and> b \<and> c" shows a b c using assms by auto
1.31  lemma conjunctD4: assumes "a \<and> b \<and> c \<and> d" shows a b c d using assms by auto
1.32 @@ -4767,7 +4789,7 @@
1.33  qed
1.34
1.35  lemma negligible_Un_eq[simp]: "negligible (s \<union> t) \<longleftrightarrow> negligible s \<and> negligible t"
1.36 -  using negligible_Un negligible_subset by blast
1.37 +  using negligible_Un negligible_subset by blast
1.38
1.39  lemma negligible_sing[intro]: "negligible {a::'a::euclidean_space}"
1.40    using negligible_standard_hyperplane[OF SOME_Basis, of "a \<bullet> (SOME i. i \<in> Basis)"] negligible_subset by blast
1.41 @@ -10709,6 +10731,277 @@
1.42         (insert assms, simp_all add: powr_minus powr_realpow divide_simps)
1.43  qed
1.44
1.45 +subsubsection \<open>Covering lemma\<close>
1.46 +
1.47 +
1.48 +text\<open> Some technical lemmas used in the approximation results that follow. Proof of the covering
1.49 +  lemma is an obvious multidimensional generalization of Lemma 3, p65 of Swartz's
1.50 +  "Introduction to Gauge Integrals". \<close>
1.51 +
1.52 +proposition covering_lemma:
1.53 +  assumes "S \<subseteq> cbox a b" "box a b \<noteq> {}" "gauge g"
1.54 +  obtains \<D> where
1.55 +    "countable \<D>"  "\<Union>\<D> \<subseteq> cbox a b"
1.56 +    "\<And>K. K \<in> \<D> \<Longrightarrow> interior K \<noteq> {} \<and> (\<exists>c d. K = cbox c d)"
1.57 +    "pairwise (\<lambda>A B. interior A \<inter> interior B = {}) \<D>"
1.58 +    "\<And>K. K \<in> \<D> \<Longrightarrow> \<exists>x \<in> S \<inter> K. K \<subseteq> g x"
1.59 +    "\<And>u v. cbox u v \<in> \<D> \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
1.60 +    "S \<subseteq> \<Union>\<D>"
1.61 +proof -
1.62 +  have aibi: "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i" and normab: "0 < norm(b - a)"
1.63 +    using \<open>box a b \<noteq> {}\<close> box_eq_empty box_sing by fastforce+
1.64 +  let ?K0 = "\<lambda>(n, f::'a\<Rightarrow>nat).
1.65 +                    cbox (\<Sum>i \<in> Basis. (a \<bullet> i + (f i / 2^n) * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i)
1.66 +                         (\<Sum>i \<in> Basis. (a \<bullet> i + ((f i + 1) / 2^n) * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i)"
1.67 +  let ?D0 = "?K0 ` (SIGMA n:UNIV. PiE Basis (\<lambda>i::'a. lessThan (2^n)))"
1.68 +  obtain \<D>0 where count: "countable \<D>0"
1.69 +             and sub: "\<Union>\<D>0 \<subseteq> cbox a b"
1.70 +             and int:  "\<And>K. K \<in> \<D>0 \<Longrightarrow> (interior K \<noteq> {}) \<and> (\<exists>c d. K = cbox c d)"
1.71 +             and intdj: "\<And>A B. \<lbrakk>A \<in> \<D>0; B \<in> \<D>0\<rbrakk> \<Longrightarrow> A \<subseteq> B \<or> B \<subseteq> A \<or> interior A \<inter> interior B = {}"
1.72 +             and SK: "\<And>x. x \<in> S \<Longrightarrow> \<exists>K \<in> \<D>0. x \<in> K \<and> K \<subseteq> g x"
1.73 +             and cbox: "\<And>u v. cbox u v \<in> \<D>0 \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
1.74 +             and fin: "\<And>K. K \<in> \<D>0 \<Longrightarrow> finite {L \<in> \<D>0. K \<subseteq> L}"
1.75 +  proof
1.76 +    show "countable ?D0"
1.77 +      by (simp add: countable_PiE)
1.78 +  next
1.79 +    show "\<Union>?D0 \<subseteq> cbox a b"
1.80 +      apply (simp add: UN_subset_iff)
1.81 +      apply (intro conjI allI ballI subset_box_imp)
1.82 +       apply (simp add: divide_simps zero_le_mult_iff aibi)
1.83 +      apply (force simp: aibi scaling_mono nat_less_real_le dest: PiE_mem)
1.84 +      done
1.85 +  next
1.86 +    show "\<And>K. K \<in> ?D0 \<Longrightarrow> interior K \<noteq> {} \<and> (\<exists>c d. K = cbox c d)"
1.87 +      using \<open>box a b \<noteq> {}\<close>
1.88 +      by (clarsimp simp: box_eq_empty) (fastforce simp add: divide_simps dest: PiE_mem)
1.89 +  next
1.90 +    have realff: "(real w) * 2^m < (real v) * 2^n \<longleftrightarrow> w * 2^m < v * 2^n" for m n v w
1.91 +      using of_nat_less_iff less_imp_of_nat_less by fastforce
1.92 +    have *: "\<forall>v w. ?K0(m,v) \<subseteq> ?K0(n,w) \<or> ?K0(n,w) \<subseteq> ?K0(m,v) \<or> interior(?K0(m,v)) \<inter> interior(?K0(n,w)) = {}"
1.93 +      for m n --\<open>The symmetry argument requires a single HOL formula\<close>
1.94 +    proof (rule linorder_wlog [where a=m and b=n], intro allI impI)
1.95 +      fix v w m and n::nat
1.96 +      assume "m \<le> n" --\<open>WLOG we can assume @{term"m \<le> n"}, when the first disjunct becomes impossible\<close>
1.97 +      have "?K0(n,w) \<subseteq> ?K0(m,v) \<or> interior(?K0(m,v)) \<inter> interior(?K0(n,w)) = {}"
1.98 +        apply (simp add: subset_box disjoint_interval)
1.99 +        apply (rule ccontr)
1.100 +        apply (clarsimp simp add: aibi mult_le_cancel_right divide_le_cancel not_less not_le)
1.101 +        apply (drule_tac x=i in bspec, assumption)
1.102 +        using \<open>m\<le>n\<close> realff [of _ _ "1+_"] realff [of "1+_"_ "1+_"]
1.104 +        apply (simp add: power_add, metis (no_types, hide_lams) mult_Suc mult_less_cancel2 not_less_eq mult.assoc)+
1.105 +        done
1.106 +      then show "?K0(m,v) \<subseteq> ?K0(n,w) \<or> ?K0(n,w) \<subseteq> ?K0(m,v) \<or> interior(?K0(m,v)) \<inter> interior(?K0(n,w)) = {}"
1.107 +        by meson
1.108 +    qed auto
1.109 +    show "\<And>A B. \<lbrakk>A \<in> ?D0; B \<in> ?D0\<rbrakk> \<Longrightarrow> A \<subseteq> B \<or> B \<subseteq> A \<or> interior A \<inter> interior B = {}"
1.110 +      apply (erule imageE SigmaE)+
1.111 +      using * by simp
1.112 +  next
1.113 +    show "\<exists>K \<in> ?D0. x \<in> K \<and> K \<subseteq> g x" if "x \<in> S" for x
1.114 +    proof (simp only: bex_simps split_paired_Bex_Sigma)
1.115 +      show "\<exists>n. \<exists>f \<in> Basis \<rightarrow>\<^sub>E {..<2 ^ n}. x \<in> ?K0(n,f) \<and> ?K0(n,f) \<subseteq> g x"
1.116 +      proof -
1.117 +        obtain e where "0 < e"
1.118 +                   and e: "\<And>y. (\<And>i. i \<in> Basis \<Longrightarrow> \<bar>x \<bullet> i - y \<bullet> i\<bar> \<le> e) \<Longrightarrow> y \<in> g x"
1.119 +        proof -
1.120 +          have "x \<in> g x" "open (g x)"
1.121 +            using \<open>gauge g\<close> by (auto simp: gauge_def)
1.122 +          then obtain \<epsilon> where "0 < \<epsilon>" and \<epsilon>: "ball x \<epsilon> \<subseteq> g x"
1.123 +            using openE by blast
1.124 +          have "norm (x - y) < \<epsilon>"
1.125 +               if "(\<And>i. i \<in> Basis \<Longrightarrow> \<bar>x \<bullet> i - y \<bullet> i\<bar> \<le> \<epsilon> / (2 * real DIM('a)))" for y
1.126 +          proof -
1.127 +            have "norm (x - y) \<le> (\<Sum>i\<in>Basis. \<bar>x \<bullet> i - y \<bullet> i\<bar>)"
1.128 +              by (metis (no_types, lifting) inner_diff_left norm_le_l1 setsum.cong)
1.129 +            also have "... \<le> DIM('a) * (\<epsilon> / (2 * real DIM('a)))"
1.130 +              by (meson setsum_bounded_above that)
1.131 +            also have "... = \<epsilon> / 2"
1.132 +              by (simp add: divide_simps)
1.133 +            also have "... < \<epsilon>"
1.134 +              by (simp add: \<open>0 < \<epsilon>\<close>)
1.135 +            finally show ?thesis .
1.136 +          qed
1.137 +          then show ?thesis
1.138 +            by (rule_tac e = "\<epsilon> / 2 / DIM('a)" in that) (simp_all add:  \<open>0 < \<epsilon>\<close> dist_norm subsetD [OF \<epsilon>])
1.139 +        qed
1.140 +        have xab: "x \<in> cbox a b"
1.141 +          using \<open>x \<in> S\<close> \<open>S \<subseteq> cbox a b\<close> by blast
1.142 +        obtain n where n: "norm (b - a) / 2^n < e"
1.143 +          using real_arch_pow_inv [of "e / norm(b - a)" "1/2"] normab \<open>0 < e\<close>
1.144 +          by (auto simp: divide_simps)
1.145 +        then have "norm (b - a) < e * 2^n"
1.146 +          by (auto simp: divide_simps)
1.147 +        then have bai: "b \<bullet> i - a \<bullet> i < e * 2 ^ n" if "i \<in> Basis" for i
1.148 +        proof -
1.149 +          have "b \<bullet> i - a \<bullet> i \<le> norm (b - a)"
1.150 +            by (metis abs_of_nonneg dual_order.trans inner_diff_left linear norm_ge_zero Basis_le_norm that)
1.151 +          also have "... < e * 2 ^ n"
1.152 +            using \<open>norm (b - a) < e * 2 ^ n\<close> by blast
1.153 +          finally show ?thesis .
1.154 +        qed
1.155 +        have D: "(a + n \<le> x \<and> x \<le> a + m) \<Longrightarrow> (a + n \<le> y \<and> y \<le> a + m) \<Longrightarrow> abs(x - y) \<le> m - n"
1.156 +                 for a m n x and y::real
1.157 +          by auto
1.158 +        have "\<forall>i\<in>Basis. \<exists>k<2 ^ n. (a \<bullet> i + real k * (b \<bullet> i - a \<bullet> i) / 2 ^ n \<le> x \<bullet> i \<and>
1.159 +               x \<bullet> i \<le> a \<bullet> i + (real k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n)"
1.160 +        proof
1.161 +          fix i::'a assume "i \<in> Basis"
1.162 +          consider "x \<bullet> i = b \<bullet> i" | "x \<bullet> i < b \<bullet> i"
1.163 +            using \<open>i \<in> Basis\<close> mem_box(2) xab by force
1.164 +          then show "\<exists>k<2 ^ n. (a \<bullet> i + real k * (b \<bullet> i - a \<bullet> i) / 2 ^ n \<le> x \<bullet> i \<and>
1.165 +                          x \<bullet> i \<le> a \<bullet> i + (real k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n)"
1.166 +          proof cases
1.167 +            case 1 then show ?thesis
1.168 +              by (rule_tac x = "2^n - 1" in exI) (auto simp: algebra_simps divide_simps of_nat_diff \<open>i \<in> Basis\<close> aibi)
1.169 +          next
1.170 +            case 2
1.171 +            then have abi_less: "a \<bullet> i < b \<bullet> i"
1.172 +              using \<open>i \<in> Basis\<close> xab by (auto simp: mem_box)
1.173 +            let ?k = "nat \<lfloor>2 ^ n * (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)\<rfloor>"
1.174 +            show ?thesis
1.175 +            proof (intro exI conjI)
1.176 +              show "?k < 2 ^ n"
1.177 +                using aibi xab \<open>i \<in> Basis\<close>
1.178 +                by (force simp: nat_less_iff floor_less_iff divide_simps 2 mem_box)
1.179 +            next
1.180 +              have "a \<bullet> i + real ?k * (b \<bullet> i - a \<bullet> i) / 2 ^ n \<le>
1.181 +                    a \<bullet> i + (2 ^ n * (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)) * (b \<bullet> i - a \<bullet> i) / 2 ^ n"
1.182 +                apply (intro add_left_mono mult_right_mono divide_right_mono of_nat_floor)
1.183 +                using aibi [OF \<open>i \<in> Basis\<close>] xab 2
1.184 +                  apply (simp_all add: \<open>i \<in> Basis\<close> mem_box divide_simps)
1.185 +                done
1.186 +              also have "... = x \<bullet> i"
1.187 +                using abi_less by (simp add: divide_simps)
1.188 +              finally show "a \<bullet> i + real ?k * (b \<bullet> i - a \<bullet> i) / 2 ^ n \<le> x \<bullet> i" .
1.189 +            next
1.190 +              have "x \<bullet> i \<le> a \<bullet> i + (2 ^ n * (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)) * (b \<bullet> i - a \<bullet> i) / 2 ^ n"
1.191 +                using abi_less by (simp add: divide_simps algebra_simps)
1.192 +              also have "... \<le> a \<bullet> i + (real ?k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n"
1.193 +                apply (intro add_left_mono mult_right_mono divide_right_mono of_nat_floor)
1.194 +                using aibi [OF \<open>i \<in> Basis\<close>] xab
1.195 +                  apply (auto simp: \<open>i \<in> Basis\<close> mem_box divide_simps)
1.196 +                done
1.197 +              finally show "x \<bullet> i \<le> a \<bullet> i + (real ?k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n" .
1.198 +            qed
1.199 +          qed
1.200 +        qed
1.201 +        then have "\<exists>f\<in>Basis \<rightarrow>\<^sub>E {..<2 ^ n}. x \<in> ?K0(n,f)"
1.202 +          apply (simp add: mem_box Bex_def)
1.203 +          apply (clarify dest!: bchoice)
1.204 +          apply (rule_tac x="restrict f Basis" in exI, simp)
1.205 +          done
1.206 +        moreover have "\<And>f. x \<in> ?K0(n,f) \<Longrightarrow> ?K0(n,f) \<subseteq> g x"
1.207 +          apply (clarsimp simp add: mem_box)
1.208 +          apply (rule e)
1.209 +          apply (drule bspec D, assumption)+
1.210 +          apply (erule order_trans)
1.211 +          apply (simp add: divide_simps)
1.212 +          using bai by (force simp: algebra_simps)
1.213 +        ultimately show ?thesis by auto
1.214 +      qed
1.215 +    qed
1.216 +  next
1.217 +    show "\<And>u v. cbox u v \<in> ?D0 \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
1.218 +      by (force simp: eq_cbox box_eq_empty field_simps dest!: aibi)
1.219 +  next
1.220 +    obtain j::'a where "j \<in> Basis"
1.221 +      using nonempty_Basis by blast
1.222 +    have "finite {L \<in> ?D0. ?K0(n,f) \<subseteq> L}" if "f \<in> Basis \<rightarrow>\<^sub>E {..<2 ^ n}" for n f
1.223 +    proof (rule finite_subset)
1.224 +      let ?B = "(\<lambda>(n, f::'a\<Rightarrow>nat). cbox (\<Sum>i\<in>Basis. (a \<bullet> i + (f i) / 2^n * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i)
1.225 +                                        (\<Sum>i\<in>Basis. (a \<bullet> i + ((f i) + 1) / 2^n * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i))
1.226 +                ` (SIGMA m:atMost n. PiE Basis (\<lambda>i::'a. lessThan (2^m)))"
1.227 +      have "?K0(m,g) \<in> ?B" if "g \<in> Basis \<rightarrow>\<^sub>E {..<2 ^ m}" "?K0(n,f) \<subseteq> ?K0(m,g)" for m g
1.228 +      proof -
1.229 +        have dd: "w / m \<le> v / n \<and> (v+1) / n \<le> (w+1) / m
1.230 +                  \<Longrightarrow> inverse n \<le> inverse m" for w m v n::real
1.231 +          by (auto simp: divide_simps algebra_simps)
1.232 +        have bjaj: "b \<bullet> j - a \<bullet> j > 0"
1.233 +          using \<open>j \<in> Basis\<close> \<open>box a b \<noteq> {}\<close> box_eq_empty(1) by fastforce
1.234 +        have "((g j) / 2 ^ m) * (b \<bullet> j - a \<bullet> j) \<le> ((f j) / 2 ^ n) * (b \<bullet> j - a \<bullet> j) \<and>
1.235 +              (((f j) + 1) / 2 ^ n) * (b \<bullet> j - a \<bullet> j) \<le> (((g j) + 1) / 2 ^ m) * (b \<bullet> j - a \<bullet> j)"
1.236 +          using that \<open>j \<in> Basis\<close> by (simp add: subset_box algebra_simps divide_simps aibi)
1.237 +        then have "((g j) / 2 ^ m) \<le> ((f j) / 2 ^ n) \<and>
1.238 +          ((real(f j) + 1) / 2 ^ n) \<le> ((real(g j) + 1) / 2 ^ m)"
1.239 +          by (metis bjaj mult.commute of_nat_1 of_nat_add real_mult_le_cancel_iff2)
1.240 +        then have "inverse (2^n) \<le> (inverse (2^m) :: real)"
1.241 +          by (rule dd)
1.242 +        then have "m \<le> n"
1.243 +          by auto
1.244 +        show ?thesis
1.245 +          by (rule imageI) (simp add: \<open>m \<le> n\<close> that)
1.246 +      qed
1.247 +      then show "{L \<in> ?D0. ?K0(n,f) \<subseteq> L} \<subseteq> ?B"
1.248 +        by auto
1.249 +      show "finite ?B"
1.250 +        by (intro finite_imageI finite_SigmaI finite_atMost finite_lessThan finite_PiE finite_Basis)
1.251 +    qed
1.252 +    then show "finite {L \<in> ?D0. K \<subseteq> L}" if "K \<in> ?D0" for K
1.253 +      using that by auto
1.254 +  qed
1.255 +  let ?D1 = "{K \<in> \<D>0. \<exists>x \<in> S \<inter> K. K \<subseteq> g x}"
1.256 +  obtain \<D> where count: "countable \<D>"
1.257 +             and sub: "\<Union>\<D> \<subseteq> cbox a b"  "S \<subseteq> \<Union>\<D>"
1.258 +             and int:  "\<And>K. K \<in> \<D> \<Longrightarrow> (interior K \<noteq> {}) \<and> (\<exists>c d. K = cbox c d)"
1.259 +             and intdj: "\<And>A B. \<lbrakk>A \<in> \<D>; B \<in> \<D>\<rbrakk> \<Longrightarrow> A \<subseteq> B \<or> B \<subseteq> A \<or> interior A \<inter> interior B = {}"
1.260 +             and SK: "\<And>K. K \<in> \<D> \<Longrightarrow> \<exists>x. x \<in> S \<inter> K \<and> K \<subseteq> g x"
1.261 +             and cbox: "\<And>u v. cbox u v \<in> \<D> \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
1.262 +             and fin: "\<And>K. K \<in> \<D> \<Longrightarrow> finite {L. L \<in> \<D> \<and> K \<subseteq> L}"
1.263 +  proof
1.264 +    show "countable ?D1" using count countable_subset
1.265 +      by (simp add: count countable_subset)
1.266 +    show "\<Union>?D1 \<subseteq> cbox a b"
1.267 +      using sub by blast
1.268 +    show "S \<subseteq> \<Union>?D1"
1.269 +      using SK by (force simp:)
1.270 +    show "\<And>K. K \<in> ?D1 \<Longrightarrow> (interior K \<noteq> {}) \<and> (\<exists>c d. K = cbox c d)"
1.271 +      using int by blast
1.272 +    show "\<And>A B. \<lbrakk>A \<in> ?D1; B \<in> ?D1\<rbrakk> \<Longrightarrow> A \<subseteq> B \<or> B \<subseteq> A \<or> interior A \<inter> interior B = {}"
1.273 +      using intdj by blast
1.274 +    show "\<And>K. K \<in> ?D1 \<Longrightarrow> \<exists>x. x \<in> S \<inter> K \<and> K \<subseteq> g x"
1.275 +      by auto
1.276 +    show "\<And>u v. cbox u v \<in> ?D1 \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
1.277 +      using cbox by blast
1.278 +    show "\<And>K. K \<in> ?D1 \<Longrightarrow> finite {L. L \<in> ?D1 \<and> K \<subseteq> L}"
1.279 +      using fin by simp (metis (mono_tags, lifting) Collect_mono rev_finite_subset)
1.280 +  qed
1.281 +  let ?\<D> = "{K \<in> \<D>. \<forall>K'. K' \<in> \<D> \<and> K \<noteq> K' \<longrightarrow> ~(K \<subseteq> K')}"
1.282 +  show ?thesis
1.283 +  proof (rule that)
1.284 +    show "countable ?\<D>"
1.285 +      by (blast intro: countable_subset [OF _ count])
1.286 +    show "\<Union>?\<D> \<subseteq> cbox a b"
1.287 +      using sub by blast
1.288 +    show "S \<subseteq> \<Union>?\<D>"
1.289 +    proof clarsimp
1.290 +      fix x
1.291 +      assume "x \<in> S"
1.292 +      then obtain X where "x \<in> X" "X \<in> \<D>" using \<open>S \<subseteq> \<Union>\<D>\<close> by blast
1.293 +      let ?R = "{(K,L). K \<in> \<D> \<and> L \<in> \<D> \<and> L \<subset> K}"
1.294 +      have irrR: "irrefl ?R" by (force simp: irrefl_def)
1.295 +      have traR: "trans ?R" by (force simp: trans_def)
1.296 +      have finR: "\<And>x. finite {y. (y, x) \<in> ?R}"
1.297 +        by simp (metis (mono_tags, lifting) fin \<open>X \<in> \<D>\<close> finite_subset mem_Collect_eq psubset_imp_subset subsetI)
1.298 +      have "{X \<in> \<D>. x \<in> X} \<noteq> {}"
1.299 +        using \<open>X \<in> \<D>\<close> \<open>x \<in> X\<close> by blast
1.300 +      then obtain Y where "Y \<in> {X \<in> \<D>. x \<in> X}" "\<And>Y'. (Y', Y) \<in> ?R \<Longrightarrow> Y' \<notin> {X \<in> \<D>. x \<in> X}"
1.301 +        by (rule wfE_min' [OF wf_finite_segments [OF irrR traR finR]]) blast
1.302 +      then show "\<exists>Y. Y \<in> \<D> \<and> (\<forall>K'. K' \<in> \<D> \<and> Y \<noteq> K' \<longrightarrow> \<not> Y \<subseteq> K') \<and> x \<in> Y"
1.303 +        by blast
1.304 +    qed
1.305 +    show "\<And>K. K \<in> ?\<D> \<Longrightarrow> interior K \<noteq> {} \<and> (\<exists>c d. K = cbox c d)"
1.306 +      by (blast intro: dest: int)
1.307 +    show "pairwise (\<lambda>A B. interior A \<inter> interior B = {}) ?\<D>"
1.308 +      using intdj by (simp add: pairwise_def) metis
1.309 +    show "\<And>K. K \<in> ?\<D> \<Longrightarrow> \<exists>x \<in> S \<inter> K. K \<subseteq> g x"
1.310 +      using SK by force
1.311 +    show "\<And>u v. cbox u v \<in> ?\<D> \<Longrightarrow> \<exists>n. \<forall>i\<in>Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
1.312 +      using cbox by force
1.313 +    qed
1.314 +qed
1.315 +
1.316  subsubsection \<open>Adaption to ordered Euclidean spaces and the Cartesian Euclidean space\<close>
1.317
1.318  lemma integral_component_eq_cart[simp]:
```