# HG changeset patch
# User immler
# Date 1352972998 -3600
# Node ID 635d73673b5ee21d0e5348743631cb30bdcb1177
# Parent  ecffea78d381365764a07c96c852814ed330773c
regularity of measures, therefore:
characterization of closure with infimum distance;
characterize of compact sets as totally bounded;
added Diagonal_Subsequence to Library;
introduced (enumerable) topological basis;
rational boxes as basis of ordered euclidean space;
moved some lemmas upwards

diff -r ecffea78d381 -r 635d73673b5e src/HOL/Library/Diagonal_Subsequence.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Diagonal_Subsequence.thy	Thu Nov 15 10:49:58 2012 +0100
@@ -0,0 +1,111 @@
+(* Author: Fabian Immler, TUM *)
+
+header {* Sequence of Properties on Subsequences *}
+
+theory Diagonal_Subsequence
+imports SEQ
+begin
+
+locale subseqs =
+  fixes P::"nat\<Rightarrow>(nat\<Rightarrow>nat)\<Rightarrow>bool"
+  assumes ex_subseq: "\<And>n s. subseq s \<Longrightarrow> \<exists>r'. subseq r' \<and> P n (s o r')"
+begin
+
+primrec seqseq where
+  "seqseq 0 = id"
+| "seqseq (Suc n) = seqseq n o (SOME r'. subseq r' \<and> P n (seqseq n o r'))"
+
+lemma seqseq_ex:
+  shows "subseq (seqseq n) \<and>
+  (\<exists>r'. seqseq (Suc n) = seqseq n o r' \<and> subseq r' \<and> P n (seqseq n o r'))"
+proof (induct n)
+  case 0
+  let ?P = "\<lambda>r'. subseq r' \<and> P 0 r'"
+  let ?r = "Eps ?P"
+  have "?P ?r" using ex_subseq[of id 0] by (intro someI_ex[of ?P]) (auto simp: subseq_def)
+  thus ?case by (auto simp: subseq_def)
+next
+  case (Suc n)
+  then obtain r' where
+    Suc': "seqseq (Suc n) = seqseq n \<circ> r'" "subseq (seqseq n)" "subseq r'"
+      "P n (seqseq n o r')"
+    by blast
+  let ?P = "\<lambda>r'a. subseq (r'a ) \<and> P (Suc n) (seqseq n o r' o r'a)"
+  let ?r = "Eps ?P"
+  have "?P ?r" using ex_subseq[of "seqseq n o r'" "Suc n"] Suc'
+    by (intro someI_ex[of ?P]) (auto intro: subseq_o simp: o_assoc)
+  moreover have "seqseq (Suc (Suc n)) = seqseq n \<circ> r' \<circ> ?r"
+    by (subst seqseq.simps) (simp only: Suc' o_assoc)
+  moreover note subseq_o[OF `subseq (seqseq n)` `subseq r'`]
+  ultimately show ?case unfolding Suc' by (auto simp: o_def)
+qed
+
+lemma subseq_seqseq:
+  shows "subseq (seqseq n)" using seqseq_ex[OF assms] by auto
+
+definition reducer where "reducer n = (SOME r'. subseq r' \<and> P n (seqseq n o r'))"
+
+lemma subseq_reducer: "subseq (reducer n)" and reducer_reduces: "P n (seqseq n o reducer n)"
+  unfolding atomize_conj unfolding reducer_def using subseq_seqseq
+  by (rule someI_ex[OF ex_subseq])
+
+lemma seqseq_reducer[simp]:
+  "seqseq (Suc n) = seqseq n o reducer n"
+  by (simp add: reducer_def)
+
+declare seqseq.simps(2)[simp del]
+
+definition diagseq where "diagseq i = seqseq i i"
+
+lemma diagseq_mono: "diagseq n < diagseq (Suc n)"
+  unfolding diagseq_def seqseq_reducer o_def
+  by (metis subseq_mono[OF subseq_seqseq] less_le_trans lessI seq_suble subseq_reducer)
+
+lemma subseq_diagseq: "subseq diagseq"
+  using diagseq_mono by (simp add: subseq_Suc_iff diagseq_def)
+
+primrec fold_reduce where
+  "fold_reduce n 0 = id"
+| "fold_reduce n (Suc k) = fold_reduce n k o reducer (n + k)"
+
+lemma subseq_fold_reduce: "subseq (fold_reduce n k)"
+proof (induct k)
+  case (Suc k) from subseq_o[OF this subseq_reducer] show ?case by (simp add: o_def)
+qed (simp add: subseq_def)
+
+lemma ex_subseq_reduce_index: "seqseq (n + k) = seqseq n o fold_reduce n k"
+  by (induct k) simp_all
+
+lemma seqseq_fold_reduce: "seqseq n = fold_reduce 0 n"
+  by (induct n) (simp_all)
+
+lemma diagseq_fold_reduce: "diagseq n = fold_reduce 0 n n"
+  using seqseq_fold_reduce by (simp add: diagseq_def)
+
+lemma fold_reduce_add: "fold_reduce 0 (m + n) = fold_reduce 0 m o fold_reduce m n"
+  by (induct n) simp_all
+
+lemma diagseq_add: "diagseq (k + n) = (seqseq k o (fold_reduce k n)) (k + n)"
+proof -
+  have "diagseq (k + n) = fold_reduce 0 (k + n) (k + n)"
+    by (simp add: diagseq_fold_reduce)
+  also have "\<dots> = (seqseq k o fold_reduce k n) (k + n)"
+    unfolding fold_reduce_add seqseq_fold_reduce ..
+  finally show ?thesis .
+qed
+
+lemma diagseq_sub:
+  assumes "m \<le> n" shows "diagseq n = (seqseq m o (fold_reduce m (n - m))) n"
+  using diagseq_add[of m "n - m"] assms by simp
+
+lemma subseq_diagonal_rest: "subseq (\<lambda>x. fold_reduce k x (k + x))"
+  unfolding subseq_Suc_iff fold_reduce.simps o_def
+  by (metis subseq_mono[OF subseq_fold_reduce] less_le_trans lessI add_Suc_right seq_suble
+      subseq_reducer)
+
+lemma diagseq_seqseq: "diagseq o (op + k) = (seqseq k o (\<lambda>x. fold_reduce k x (k + x)))"
+  by (auto simp: o_def diagseq_add)
+
+end
+
+end
diff -r ecffea78d381 -r 635d73673b5e src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Thu Nov 15 14:04:23 2012 +0100
+++ b/src/HOL/Library/Library.thy	Thu Nov 15 10:49:58 2012 +0100
@@ -13,6 +13,7 @@
   Convex
   Countable
   Debug
+  Diagonal_Subsequence
   Dlist
   Eval_Witness
   Extended_Nat
diff -r ecffea78d381 -r 635d73673b5e src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Nov 15 14:04:23 2012 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Nov 15 10:49:58 2012 +0100
@@ -7,9 +7,210 @@
 header {* Elementary topology in Euclidean space. *}
 
 theory Topology_Euclidean_Space
-imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs" Norm_Arith
+imports
+  SEQ
+  "~~/src/HOL/Library/Diagonal_Subsequence"
+  "~~/src/HOL/Library/Countable"
+  Linear_Algebra
+  "~~/src/HOL/Library/Glbs"
+  Norm_Arith
+begin
+
+subsection {* Topological Basis *}
+
+context topological_space
+begin
+
+definition "topological_basis B =
+  ((\<forall>b\<in>B. open b) \<and> (\<forall>x. open x \<longrightarrow> (\<exists>B'. B' \<subseteq> B \<and> Union B' = x)))"
+
+lemma topological_basis_iff:
+  assumes "\<And>B'. B' \<in> B \<Longrightarrow> open B'"
+  shows "topological_basis B \<longleftrightarrow> (\<forall>O'. open O' \<longrightarrow> (\<forall>x\<in>O'. \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'))"
+    (is "_ \<longleftrightarrow> ?rhs")
+proof safe
+  fix O' and x::'a
+  assume H: "topological_basis B" "open O'" "x \<in> O'"
+  hence "(\<exists>B'\<subseteq>B. \<Union>B' = O')" by (simp add: topological_basis_def)
+  then obtain B' where "B' \<subseteq> B" "O' = \<Union>B'" by auto
+  thus "\<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'" using H by auto
+next
+  assume H: ?rhs
+  show "topological_basis B" using assms unfolding topological_basis_def
+  proof safe
+    fix O'::"'a set" assume "open O'"
+    with H obtain f where "\<forall>x\<in>O'. f x \<in> B \<and> x \<in> f x \<and> f x \<subseteq> O'"
+      by (force intro: bchoice simp: Bex_def)
+    thus "\<exists>B'\<subseteq>B. \<Union>B' = O'"
+      by (auto intro: exI[where x="{f x |x. x \<in> O'}"])
+  qed
+qed
+
+lemma topological_basisI:
+  assumes "\<And>B'. B' \<in> B \<Longrightarrow> open B'"
+  assumes "\<And>O' x. open O' \<Longrightarrow> x \<in> O' \<Longrightarrow> \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'"
+  shows "topological_basis B"
+  using assms by (subst topological_basis_iff) auto
+
+lemma topological_basisE:
+  fixes O'
+  assumes "topological_basis B"
+  assumes "open O'"
+  assumes "x \<in> O'"
+  obtains B' where "B' \<in> B" "x \<in> B'" "B' \<subseteq> O'"
+proof atomize_elim
+  from assms have "\<And>B'. B'\<in>B \<Longrightarrow> open B'" by (simp add: topological_basis_def)
+  with topological_basis_iff assms
+  show  "\<exists>B'. B' \<in> B \<and> x \<in> B' \<and> B' \<subseteq> O'" using assms by (simp add: Bex_def)
+qed
+
+end
+
+subsection {* Enumerable Basis *}
+
+class enumerable_basis = topological_space +
+  assumes ex_enum_basis: "\<exists>f::nat \<Rightarrow> 'a set. topological_basis (range f)"
 begin
 
+definition enum_basis'::"nat \<Rightarrow> 'a set"
+  where "enum_basis' = Eps (topological_basis o range)"
+
+lemma enumerable_basis': "topological_basis (range enum_basis')"
+  using ex_enum_basis
+  unfolding enum_basis'_def o_def
+  by (rule someI_ex)
+
+lemmas enumerable_basisE' = topological_basisE[OF enumerable_basis']
+
+text {* Extend enumeration of basis, such that it is closed under (finite) Union *}
+
+definition enum_basis::"nat \<Rightarrow> 'a set"
+  where "enum_basis n = \<Union>(set (map enum_basis' (from_nat n)))"
+
+lemma
+  open_enum_basis:
+  assumes "B \<in> range enum_basis"
+  shows "open B"
+  using assms enumerable_basis'
+  by (force simp add: topological_basis_def enum_basis_def)
+
+lemma enumerable_basis: "topological_basis (range enum_basis)"
+proof (rule topological_basisI[OF open_enum_basis])
+  fix O' x assume "open O'" "x \<in> O'"
+  from topological_basisE[OF enumerable_basis' this] guess B' . note B' = this
+  moreover then obtain n where "B' = enum_basis' n" by auto
+  moreover hence "B' = enum_basis (to_nat [n])" by (auto simp: enum_basis_def)
+  ultimately show "\<exists>B'\<in>range enum_basis. x \<in> B' \<and> B' \<subseteq> O'" by blast
+qed
+
+lemmas enumerable_basisE = topological_basisE[OF enumerable_basis]
+
+lemma open_enumerable_basis_ex:
+  assumes "open X"
+  shows "\<exists>N. X = (\<Union>n\<in>N. enum_basis n)"
+proof -
+  from enumerable_basis assms obtain B' where "B' \<subseteq> range enum_basis" "X = Union B'"
+    unfolding topological_basis_def by blast
+  hence "Union B' = (\<Union>n\<in>{n. enum_basis n \<in> B'}. enum_basis n)" by auto
+  with `X = Union B'` show ?thesis by blast
+qed
+
+lemma open_enumerable_basisE:
+  assumes "open X"
+  obtains N where "X = (\<Union>n\<in>N. enum_basis n)"
+  using assms open_enumerable_basis_ex by (atomize_elim) simp
+
+lemma countable_dense_set:
+  shows "\<exists>x::nat \<Rightarrow> _. \<forall>y. open y \<longrightarrow> y \<noteq> {} \<longrightarrow> (\<exists>n. x n \<in> y)"
+proof -
+  def x \<equiv> "\<lambda>n. (SOME x::'a. x \<in> enum_basis n)"
+  have x: "\<And>n. enum_basis n \<noteq> ({}::'a set) \<Longrightarrow> x n \<in> enum_basis n" unfolding x_def
+    by (rule someI_ex) auto
+  have "\<forall>y. open y \<longrightarrow> y \<noteq> {} \<longrightarrow> (\<exists>n. x n \<in> y)"
+  proof (intro allI impI)
+    fix y::"'a set" assume "open y" "y \<noteq> {}"
+    from open_enumerable_basisE[OF `open y`] guess N . note N = this
+    obtain n where n: "n \<in> N" "enum_basis n \<noteq> ({}::'a set)"
+    proof (atomize_elim, rule ccontr, clarsimp)
+      assume "\<forall>n. n \<in> N \<longrightarrow> enum_basis n = ({}::'a set)"
+      hence "(\<Union>n\<in>N. enum_basis n) = (\<Union>n\<in>N. {}::'a set)"
+        by (intro UN_cong) auto
+      hence "y = {}" unfolding N by simp
+      with `y \<noteq> {}` show False by auto
+    qed
+    with x N n have "x n \<in> y" by auto
+    thus "\<exists>n. x n \<in> y" ..
+  qed
+  thus ?thesis by blast
+qed
+
+lemma countable_dense_setE:
+  obtains x :: "nat \<Rightarrow> _"
+  where "\<And>y. open y \<Longrightarrow> y \<noteq> {} \<Longrightarrow> \<exists>n. x n \<in> y"
+  using countable_dense_set by blast
+
+text {* Construction of an Increasing Sequence Approximating Open Sets *}
+
+lemma empty_basisI[intro]: "{} \<in> range enum_basis"
+proof
+  show "{} = enum_basis (to_nat ([]::nat list))" by (simp add: enum_basis_def)
+qed rule
+
+lemma union_basisI[intro]:
+  assumes "A \<in> range enum_basis" "B \<in> range enum_basis"
+  shows "A \<union> B \<in> range enum_basis"
+proof -
+  from assms obtain a b where "A \<union> B = enum_basis a \<union> enum_basis b" by auto
+  also have "\<dots> = enum_basis (to_nat (from_nat a @ from_nat b::nat list))"
+    by (simp add: enum_basis_def)
+  finally show ?thesis by simp
+qed
+
+lemma open_imp_Union_of_incseq:
+  assumes "open X"
+  shows "\<exists>S. incseq S \<and> (\<Union>j. S j) = X \<and> range S \<subseteq> range enum_basis"
+proof -
+  from open_enumerable_basis_ex[OF `open X`] obtain N where N: "X = (\<Union>n\<in>N. enum_basis n)" by auto
+  hence X: "X = (\<Union>n. if n \<in> N then enum_basis n else {})" by (auto split: split_if_asm)
+  def S \<equiv> "nat_rec (if 0 \<in> N then enum_basis 0 else {})
+    (\<lambda>n S. if (Suc n) \<in> N then S \<union> enum_basis (Suc n) else S)"
+  have S_simps[simp]:
+    "S 0 = (if 0 \<in> N then enum_basis 0 else {})"
+    "\<And>n. S (Suc n) = (if (Suc n) \<in> N then S n \<union> enum_basis (Suc n) else S n)"
+    by (simp_all add: S_def)
+  have "incseq S" by (rule incseq_SucI) auto
+  moreover
+  have "(\<Union>j. S j) = X" unfolding N
+  proof safe
+    fix x n assume "n \<in> N" "x \<in> enum_basis n"
+    hence "x \<in> S n" by (cases n) auto
+    thus "x \<in> (\<Union>j. S j)" by auto
+  next
+    fix x j
+    assume "x \<in> S j"
+    thus "x \<in> UNION N enum_basis" by (induct j) (auto split: split_if_asm)
+  qed
+  moreover have "range S \<subseteq> range enum_basis"
+  proof safe
+    fix j show "S j \<in> range enum_basis" by (induct j) auto
+  qed
+  ultimately show ?thesis by auto
+qed
+
+lemma open_incseqE:
+  assumes "open X"
+  obtains S where "incseq S" "(\<Union>j. S j) = X" "range S \<subseteq> range enum_basis"
+  using open_imp_Union_of_incseq assms by atomize_elim
+
+end
+
+subsection {* Polish spaces *}
+
+text {* Textbooks define Polish spaces as completely metrizable.
+  We assume the topology to be complete for a given metric. *}
+
+class polish_space = complete_space + enumerable_basis
+
 subsection {* General notion of a topology as a value *}
 
 definition "istopology L \<longleftrightarrow> L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union> K))"
@@ -377,6 +578,86 @@
 
 lemma ball_empty[intro]: "e \<le> 0 ==> ball x e = {}" by simp
 
+lemma rational_boxes:
+  fixes x :: "'a\<Colon>ordered_euclidean_space"
+  assumes "0 < e"
+  shows "\<exists>a b. (\<forall>i. a $$ i \<in> \<rat>) \<and> (\<forall>i. b $$ i \<in> \<rat>) \<and> x \<in> {a <..< b} \<and> {a <..< b} \<subseteq> ball x e"
+proof -
+  def e' \<equiv> "e / (2 * sqrt (real (DIM ('a))))"
+  then have e: "0 < e'" using assms by (auto intro!: divide_pos_pos)
+  have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x $$ i \<and> x $$ i - y < e'" (is "\<forall>i. ?th i")
+  proof
+    fix i from Rats_dense_in_real[of "x $$ i - e'" "x $$ i"] e
+    show "?th i" by auto
+  qed
+  from choice[OF this] guess a .. note a = this
+  have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x $$ i < y \<and> y - x $$ i < e'" (is "\<forall>i. ?th i")
+  proof
+    fix i from Rats_dense_in_real[of "x $$ i" "x $$ i + e'"] e
+    show "?th i" by auto
+  qed
+  from choice[OF this] guess b .. note b = this
+  { fix y :: 'a assume *: "Chi a < y" "y < Chi b"
+    have "dist x y = sqrt (\<Sum>i<DIM('a). (dist (x $$ i) (y $$ i))\<twosuperior>)"
+      unfolding setL2_def[symmetric] by (rule euclidean_dist_l2)
+    also have "\<dots> < sqrt (\<Sum>i<DIM('a). e^2 / real (DIM('a)))"
+    proof (rule real_sqrt_less_mono, rule setsum_strict_mono)
+      fix i assume i: "i \<in> {..<DIM('a)}"
+      have "a i < y$$i \<and> y$$i < b i" using * i eucl_less[where 'a='a] by auto
+      moreover have "a i < x$$i" "x$$i - a i < e'" using a by auto
+      moreover have "x$$i < b i" "b i - x$$i < e'" using b by auto
+      ultimately have "\<bar>x$$i - y$$i\<bar> < 2 * e'" by auto
+      then have "dist (x $$ i) (y $$ i) < e/sqrt (real (DIM('a)))"
+        unfolding e'_def by (auto simp: dist_real_def)
+      then have "(dist (x $$ i) (y $$ i))\<twosuperior> < (e/sqrt (real (DIM('a))))\<twosuperior>"
+        by (rule power_strict_mono) auto
+      then show "(dist (x $$ i) (y $$ i))\<twosuperior> < e\<twosuperior> / real DIM('a)"
+        by (simp add: power_divide)
+    qed auto
+    also have "\<dots> = e" using `0 < e` by (simp add: real_eq_of_nat DIM_positive)
+    finally have "dist x y < e" . }
+  with a b show ?thesis
+    apply (rule_tac exI[of _ "Chi a"])
+    apply (rule_tac exI[of _ "Chi b"])
+    using eucl_less[where 'a='a] by auto
+qed
+
+lemma ex_rat_list:
+  fixes x :: "'a\<Colon>ordered_euclidean_space"
+  assumes "\<And> i. x $$ i \<in> \<rat>"
+  shows "\<exists> r. length r = DIM('a) \<and> (\<forall> i < DIM('a). of_rat (r ! i) = x $$ i)"
+proof -
+  have "\<forall>i. \<exists>r. x $$ i = of_rat r" using assms unfolding Rats_def by blast
+  from choice[OF this] guess r ..
+  then show ?thesis by (auto intro!: exI[of _ "map r [0 ..< DIM('a)]"])
+qed
+
+lemma open_UNION:
+  fixes M :: "'a\<Colon>ordered_euclidean_space set"
+  assumes "open M"
+  shows "M = UNION {(a, b) | a b. {Chi (of_rat \<circ> op ! a) <..< Chi (of_rat \<circ> op ! b)} \<subseteq> M}
+                   (\<lambda> (a, b). {Chi (of_rat \<circ> op ! a) <..< Chi (of_rat \<circ> op ! b)})"
+    (is "M = UNION ?idx ?box")
+proof safe
+  fix x assume "x \<in> M"
+  obtain e where e: "e > 0" "ball x e \<subseteq> M"
+    using openE[OF assms `x \<in> M`] by auto
+  then obtain a b where ab: "x \<in> {a <..< b}" "\<And>i. a $$ i \<in> \<rat>" "\<And>i. b $$ i \<in> \<rat>" "{a <..< b} \<subseteq> ball x e"
+    using rational_boxes[OF e(1)] by blast
+  then obtain p q where pq: "length p = DIM ('a)"
+                            "length q = DIM ('a)"
+                            "\<forall> i < DIM ('a). of_rat (p ! i) = a $$ i \<and> of_rat (q ! i) = b $$ i"
+    using ex_rat_list[OF ab(2)] ex_rat_list[OF ab(3)] by blast
+  hence p: "Chi (of_rat \<circ> op ! p) = a"
+    using euclidean_eq[of "Chi (of_rat \<circ> op ! p)" a]
+    unfolding o_def by auto
+  from pq have q: "Chi (of_rat \<circ> op ! q) = b"
+    using euclidean_eq[of "Chi (of_rat \<circ> op ! q)" b]
+    unfolding o_def by auto
+  have "x \<in> ?box (p, q)"
+    using p q ab by auto
+  thus "x \<in> UNION ?idx ?box" using ab e p q exI[of _ p] exI[of _ q] by auto
+qed auto
 
 subsection{* Connectedness *}
 
@@ -803,7 +1084,6 @@
   using frontier_complement frontier_subset_eq[of "- S"]
   unfolding open_closed by auto
 
-
 subsection {* Filters and the ``eventually true'' quantifier *}
 
 definition
@@ -1361,6 +1641,121 @@
   shows "closed S ==> (\<forall>e>0. \<exists>y\<in>S. dist y x < e) \<longleftrightarrow> x \<in> S"
   by (metis closure_closed closure_approachable)
 
+subsection {* Infimum Distance *}
+
+definition "infdist x A = (if A = {} then 0 else Inf {dist x a|a. a \<in> A})"
+
+lemma infdist_notempty: "A \<noteq> {} \<Longrightarrow> infdist x A = Inf {dist x a|a. a \<in> A}"
+  by (simp add: infdist_def)
+
+lemma infdist_nonneg:
+  shows "0 \<le> infdist x A"
+  using assms by (auto simp add: infdist_def)
+
+lemma infdist_le:
+  assumes "a \<in> A"
+  assumes "d = dist x a"
+  shows "infdist x A \<le> d"
+  using assms by (auto intro!: SupInf.Inf_lower[where z=0] simp add: infdist_def)
+
+lemma infdist_zero[simp]:
+  assumes "a \<in> A" shows "infdist a A = 0"
+proof -
+  from infdist_le[OF assms, of "dist a a"] have "infdist a A \<le> 0" by auto
+  with infdist_nonneg[of a A] assms show "infdist a A = 0" by auto
+qed
+
+lemma infdist_triangle:
+  shows "infdist x A \<le> infdist y A + dist x y"
+proof cases
+  assume "A = {}" thus ?thesis by (simp add: infdist_def)
+next
+  assume "A \<noteq> {}" then obtain a where "a \<in> A" by auto
+  have "infdist x A \<le> Inf {dist x y + dist y a |a. a \<in> A}"
+  proof
+    from `A \<noteq> {}` show "{dist x y + dist y a |a. a \<in> A} \<noteq> {}" by simp
+    fix d assume "d \<in> {dist x y + dist y a |a. a \<in> A}"
+    then obtain a where d: "d = dist x y + dist y a" "a \<in> A" by auto
+    show "infdist x A \<le> d"
+      unfolding infdist_notempty[OF `A \<noteq> {}`]
+    proof (rule Inf_lower2)
+      show "dist x a \<in> {dist x a |a. a \<in> A}" using `a \<in> A` by auto
+      show "dist x a \<le> d" unfolding d by (rule dist_triangle)
+      fix d assume "d \<in> {dist x a |a. a \<in> A}"
+      then obtain a where "a \<in> A" "d = dist x a" by auto
+      thus "infdist x A \<le> d" by (rule infdist_le)
+    qed
+  qed
+  also have "\<dots> = dist x y + infdist y A"
+  proof (rule Inf_eq, safe)
+    fix a assume "a \<in> A"
+    thus "dist x y + infdist y A \<le> dist x y + dist y a" by (auto intro: infdist_le)
+  next
+    fix i assume inf: "\<And>d. d \<in> {dist x y + dist y a |a. a \<in> A} \<Longrightarrow> i \<le> d"
+    hence "i - dist x y \<le> infdist y A" unfolding infdist_notempty[OF `A \<noteq> {}`] using `a \<in> A`
+      by (intro Inf_greatest) (auto simp: field_simps)
+    thus "i \<le> dist x y + infdist y A" by simp
+  qed
+  finally show ?thesis by simp
+qed
+
+lemma
+  in_closure_iff_infdist_zero:
+  assumes "A \<noteq> {}"
+  shows "x \<in> closure A \<longleftrightarrow> infdist x A = 0"
+proof
+  assume "x \<in> closure A"
+  show "infdist x A = 0"
+  proof (rule ccontr)
+    assume "infdist x A \<noteq> 0"
+    with infdist_nonneg[of x A] have "infdist x A > 0" by auto
+    hence "ball x (infdist x A) \<inter> closure A = {}" apply auto
+      by (metis `0 < infdist x A` `x \<in> closure A` closure_approachable dist_commute
+        eucl_less_not_refl euclidean_trans(2) infdist_le)
+    hence "x \<notin> closure A" by (metis `0 < infdist x A` centre_in_ball disjoint_iff_not_equal)
+    thus False using `x \<in> closure A` by simp
+  qed
+next
+  assume x: "infdist x A = 0"
+  then obtain a where "a \<in> A" by atomize_elim (metis all_not_in_conv assms)
+  show "x \<in> closure A" unfolding closure_approachable
+  proof (safe, rule ccontr)
+    fix e::real assume "0 < e"
+    assume "\<not> (\<exists>y\<in>A. dist y x < e)"
+    hence "infdist x A \<ge> e" using `a \<in> A`
+      unfolding infdist_def
+      by (force intro: Inf_greatest simp: dist_commute)
+    with x `0 < e` show False by auto
+  qed
+qed
+
+lemma
+  in_closed_iff_infdist_zero:
+  assumes "closed A" "A \<noteq> {}"
+  shows "x \<in> A \<longleftrightarrow> infdist x A = 0"
+proof -
+  have "x \<in> closure A \<longleftrightarrow> infdist x A = 0"
+    by (rule in_closure_iff_infdist_zero) fact
+  with assms show ?thesis by simp
+qed
+
+lemma tendsto_infdist [tendsto_intros]:
+  assumes f: "(f ---> l) F"
+  shows "((\<lambda>x. infdist (f x) A) ---> infdist l A) F"
+proof (rule tendstoI)
+  fix e ::real assume "0 < e"
+  from tendstoD[OF f this]
+  show "eventually (\<lambda>x. dist (infdist (f x) A) (infdist l A) < e) F"
+  proof (eventually_elim)
+    fix x
+    from infdist_triangle[of l A "f x"] infdist_triangle[of "f x" A l]
+    have "dist (infdist (f x) A) (infdist l A) \<le> dist (f x) l"
+      by (simp add: dist_commute dist_real_def)
+    also assume "dist (f x) l < e"
+    finally show "dist (infdist (f x) A) (infdist l A) < e" .
+  qed
+qed
+
 text{* Some other lemmas about sequences. *}
 
 lemma sequentially_offset:
@@ -2696,6 +3091,157 @@
   assume ?rhs thus ?lhs by (rule bolzano_weierstrass_imp_compact)
 qed
 
+lemma bchoice_iff: "(\<forall>a\<in>A. \<exists>b. P a b) \<longleftrightarrow> (\<exists>f. \<forall>a\<in>A. P a (f a))"
+  by metis
+
+lemma nat_approx_posE:
+  fixes e::real
+  assumes "0 < e"
+  obtains n::nat where "1 / (Suc n) < e"
+proof atomize_elim
+  have " 1 / real (Suc (nat (ceiling (1/e)))) < 1 / (ceiling (1/e))"
+    by (rule divide_strict_left_mono) (auto intro!: mult_pos_pos simp: `0 < e`)
+  also have "1 / (ceiling (1/e)) \<le> 1 / (1/e)"
+    by (rule divide_left_mono) (auto intro!: divide_pos_pos simp: `0 < e`)
+  also have "\<dots> = e" by simp
+  finally show  "\<exists>n. 1 / real (Suc n) < e" ..
+qed
+
+lemma compact_eq_totally_bounded:
+  shows "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k)))"
+proof (safe intro!: compact_imp_complete)
+  fix e::real
+  def f \<equiv> "(\<lambda>x::'a. ball x e) ` UNIV"
+  assume "0 < e" "compact s"
+  hence "(\<forall>t\<in>f. open t) \<and> s \<subseteq> \<Union>f \<longrightarrow> (\<exists>f'\<subseteq>f. finite f' \<and> s \<subseteq> \<Union>f')"
+    by (simp add: compact_eq_heine_borel)
+  moreover
+  have d0: "\<And>x::'a. dist x x < e" using `0 < e` by simp
+  hence "(\<forall>t\<in>f. open t) \<and> s \<subseteq> \<Union>f" by (auto simp: f_def intro!: d0)
+  ultimately have "(\<exists>f'\<subseteq>f. finite f' \<and> s \<subseteq> \<Union>f')" ..
+  then guess K .. note K = this
+  have "\<forall>K'\<in>K. \<exists>k. K' = ball k e" using K by (auto simp: f_def)
+  then obtain k where "\<And>K'. K' \<in> K \<Longrightarrow> K' = ball (k K') e" unfolding bchoice_iff by blast
+  thus "\<exists>k. finite k \<and> s \<subseteq> \<Union>(\<lambda>x. ball x e) ` k" using K
+    by (intro exI[where x="k ` K"]) (auto simp: f_def)
+next
+  assume assms: "complete s" "\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> \<Union>(\<lambda>x. ball x e) ` k"
+  show "compact s"
+  proof cases
+    assume "s = {}" thus "compact s" by (simp add: compact_def)
+  next
+    assume "s \<noteq> {}"
+    show ?thesis
+      unfolding compact_def
+    proof safe
+      fix f::"nat \<Rightarrow> _" assume "\<forall>n. f n \<in> s" hence f: "\<And>n. f n \<in> s" by simp
+      from assms have "\<forall>e. \<exists>k. e>0 \<longrightarrow> finite k \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k))" by simp
+      then obtain K where
+        K: "\<And>e. e > 0 \<Longrightarrow> finite (K e) \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` (K e)))"
+        unfolding choice_iff by blast
+      {
+        fix e::real and f' have f': "\<And>n::nat. (f o f') n \<in> s" using f by auto
+        assume "e > 0"
+        from K[OF this] have K: "finite (K e)" "s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` (K e)))"
+          by simp_all
+        have "\<exists>k\<in>(K e). \<exists>r. subseq r \<and> (\<forall>i. (f o f' o r) i \<in> ball k e)"
+        proof (rule ccontr)
+          from K have "finite (K e)" "K e \<noteq> {}" "s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` (K e)))"
+            using `s \<noteq> {}`
+            by auto
+          moreover
+          assume "\<not> (\<exists>k\<in>K e. \<exists>r. subseq r \<and> (\<forall>i. (f \<circ> f' o r) i \<in> ball k e))"
+          hence "\<And>r k. k \<in> K e \<Longrightarrow> subseq r \<Longrightarrow> (\<exists>i. (f o f' o r) i \<notin> ball k e)" by simp
+          ultimately
+          show False using f'
+          proof (induct arbitrary: s f f' rule: finite_ne_induct)
+            case (singleton x)
+            have "\<exists>i. (f \<circ> f' o id) i \<notin> ball x e" by (rule singleton) (auto simp: subseq_def)
+            thus ?case using singleton by (auto simp: ball_def)
+          next
+            case (insert x A)
+            show ?case
+            proof cases
+              have inf_ms: "infinite ((f o f') -` s)" using insert by (simp add: vimage_def)
+              have "infinite ((f o f') -` \<Union>((\<lambda>x. ball x e) ` (insert x A)))"
+                using insert by (intro infinite_super[OF _ inf_ms]) auto
+              also have "((f o f') -` \<Union>((\<lambda>x. ball x e) ` (insert x A))) =
+                {m. (f o f') m \<in> ball x e} \<union> {m. (f o f') m \<in> \<Union>((\<lambda>x. ball x e) ` A)}" by auto
+              finally have "infinite \<dots>" .
+              moreover assume "finite {m. (f o f') m \<in> ball x e}"
+              ultimately have inf: "infinite {m. (f o f') m \<in> \<Union>((\<lambda>x. ball x e) ` A)}" by blast
+              hence "A \<noteq> {}" by auto then obtain k where "k \<in> A" by auto
+              def r \<equiv> "enumerate {m. (f o f') m \<in> \<Union>((\<lambda>x. ball x e) ` A)}"
+              have r_mono: "\<And>n m. n < m \<Longrightarrow> r n < r m"
+                using enumerate_mono[OF _ inf] by (simp add: r_def)
+              hence "subseq r" by (simp add: subseq_def)
+              have r_in_set: "\<And>n. r n \<in> {m. (f o f') m \<in> \<Union>((\<lambda>x. ball x e) ` A)}"
+                using enumerate_in_set[OF inf] by (simp add: r_def)
+              show False
+              proof (rule insert)
+                show "\<Union>(\<lambda>x. ball x e) ` A \<subseteq> \<Union>(\<lambda>x. ball x e) ` A" by simp
+                fix k s assume "k \<in> A" "subseq s"
+                thus "\<exists>i. (f o f' o r o s) i \<notin> ball k e" using `subseq r`
+                  by (subst (2) o_assoc[symmetric]) (intro insert(6) subseq_o, simp_all)
+              next
+                fix n show "(f \<circ> f' o r) n \<in> \<Union>(\<lambda>x. ball x e) ` A" using r_in_set by auto
+              qed
+            next
+              assume inf: "infinite {m. (f o f') m \<in> ball x e}"
+              def r \<equiv> "enumerate {m. (f o f') m \<in> ball x e}"
+              have r_mono: "\<And>n m. n < m \<Longrightarrow> r n < r m"
+                using enumerate_mono[OF _ inf] by (simp add: r_def)
+              hence "subseq r" by (simp add: subseq_def)
+              from insert(6)[OF insertI1 this] obtain i where "(f o f') (r i) \<notin> ball x e" by auto
+              moreover
+              have r_in_set: "\<And>n. r n \<in> {m. (f o f') m \<in> ball x e}"
+                using enumerate_in_set[OF inf] by (simp add: r_def)
+              hence "(f o f') (r i) \<in> ball x e" by simp
+              ultimately show False by simp
+            qed
+          qed
+        qed
+      }
+      hence ex: "\<forall>f'. \<forall>e > 0. (\<exists>k\<in>K e. \<exists>r. subseq r \<and> (\<forall>i. (f o f' \<circ> r) i \<in> ball k e))" by simp
+      let ?e = "\<lambda>n. 1 / real (Suc n)"
+      let ?P = "\<lambda>n s. \<exists>k\<in>K (?e n). (\<forall>i. (f o s) i \<in> ball k (?e n))"
+      interpret subseqs ?P using ex by unfold_locales force
+      from `complete s` have limI: "\<And>f. (\<And>n. f n \<in> s) \<Longrightarrow> Cauchy f \<Longrightarrow> (\<exists>l\<in>s. f ----> l)"
+        by (simp add: complete_def)
+      have "\<exists>l\<in>s. (f o diagseq) ----> l"
+      proof (intro limI metric_CauchyI)
+        fix e::real assume "0 < e" hence "0 < e / 2" by auto
+        from nat_approx_posE[OF this] guess n . note n = this
+        show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist ((f \<circ> diagseq) m) ((f \<circ> diagseq) n) < e"
+        proof (rule exI[where x="Suc n"], safe)
+          fix m mm assume "Suc n \<le> m" "Suc n \<le> mm"
+          let ?e = "1 / real (Suc n)"
+          from reducer_reduces[of n] obtain k where
+            "k\<in>K ?e"  "\<And>i. (f o seqseq (Suc n)) i \<in> ball k ?e"
+            unfolding seqseq_reducer by auto
+          moreover
+          note diagseq_sub[OF `Suc n \<le> m`] diagseq_sub[OF `Suc n \<le> mm`]
+          ultimately have "{(f o diagseq) m, (f o diagseq) mm} \<subseteq> ball k ?e" by auto
+          also have "\<dots> \<subseteq> ball k (e / 2)" using n by (intro subset_ball) simp
+          finally
+          have "dist k ((f \<circ> diagseq) m) + dist k ((f \<circ> diagseq) mm) < e / 2 + e /2"
+            by (intro add_strict_mono) auto
+          hence "dist ((f \<circ> diagseq) m) k + dist ((f \<circ> diagseq) mm) k < e"
+            by (simp add: dist_commute)
+          moreover have "dist ((f \<circ> diagseq) m) ((f \<circ> diagseq) mm) \<le>
+            dist ((f \<circ> diagseq) m) k + dist ((f \<circ> diagseq) mm) k"
+            by (rule dist_triangle2)
+          ultimately show "dist ((f \<circ> diagseq) m) ((f \<circ> diagseq) mm) < e"
+            by simp
+        qed
+      next
+        fix n show "(f o diagseq) n \<in> s" using f by simp
+      qed
+      thus "\<exists>l\<in>s. \<exists>r. subseq r \<and> (f \<circ> r) ----> l" using subseq_diagseq by auto
+    qed
+  qed
+qed
+
 lemma compact_eq_bounded_closed:
   fixes s :: "'a::heine_borel set"
   shows "compact s \<longleftrightarrow> bounded s \<and> closed s"  (is "?lhs = ?rhs")
@@ -2738,9 +3284,6 @@
   unfolding compact_def
   by simp
 
-lemma subseq_o: "subseq r \<Longrightarrow> subseq s \<Longrightarrow> subseq (r \<circ> s)"
-  unfolding subseq_def by simp (* TODO: move somewhere else *)
-
 lemma compact_union [intro]:
   assumes "compact s" and "compact t"
   shows "compact (s \<union> t)"
@@ -2771,6 +3314,13 @@
   qed
 qed
 
+lemma compact_Union [intro]: "finite S \<Longrightarrow> (\<And>T. T \<in> S \<Longrightarrow> compact T) \<Longrightarrow> compact (\<Union>S)"
+  by (induct set: finite) auto
+
+lemma compact_UN [intro]:
+  "finite A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> compact (B x)) \<Longrightarrow> compact (\<Union>x\<in>A. B x)"
+  unfolding SUP_def by (rule compact_Union) auto
+
 lemma compact_inter_closed [intro]:
   assumes "compact s" and "closed t"
   shows "compact (s \<inter> t)"
@@ -3294,6 +3844,11 @@
   shows "continuous F (\<lambda>x. dist (f x) (g x))"
   using assms unfolding continuous_def by (rule tendsto_dist)
 
+lemma continuous_infdist:
+  assumes "continuous F f"
+  shows "continuous F (\<lambda>x. infdist (f x) A)"
+  using assms unfolding continuous_def by (rule tendsto_infdist)
+
 lemma continuous_norm:
   shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. norm (f x))"
   unfolding continuous_def by (rule tendsto_norm)
@@ -4886,6 +5441,39 @@
   thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
 qed
 
+instance ordered_euclidean_space \<subseteq> enumerable_basis
+proof
+  def to_cube \<equiv> "\<lambda>(a, b). {Chi (real_of_rat \<circ> op ! a)<..<Chi (real_of_rat \<circ> op ! b)}::'a set"
+  def enum \<equiv> "\<lambda>n. (to_cube (from_nat n)::'a set)"
+  have "Ball (range enum) open" unfolding enum_def
+  proof safe
+    fix n show "open (to_cube (from_nat n))"
+      by (cases "from_nat n::rat list \<times> rat list")
+         (simp add: open_interval to_cube_def)
+  qed
+  moreover have "(\<forall>x. open x \<longrightarrow> (\<exists>B'\<subseteq>range enum. \<Union>B' = x))"
+  proof safe
+    fix x::"'a set" assume "open x"
+    def lists \<equiv> "{(a, b) |a b. to_cube (a, b) \<subseteq> x}"
+    from open_UNION[OF `open x`]
+    have "\<Union>(to_cube ` lists) = x" unfolding lists_def to_cube_def
+     by simp
+    moreover have "to_cube ` lists \<subseteq> range enum"
+    proof
+      fix x assume "x \<in> to_cube ` lists"
+      then obtain l where "l \<in> lists" "x = to_cube l" by auto
+      hence "x = enum (to_nat l)" by (simp add: to_cube_def enum_def)
+      thus "x \<in> range enum" by simp
+    qed
+    ultimately
+    show "\<exists>B'\<subseteq>range enum. \<Union>B' = x" by blast
+  qed
+  ultimately
+  show "\<exists>f::nat\<Rightarrow>'a set. topological_basis (range f)" unfolding topological_basis_def by blast
+qed
+
+instance ordered_euclidean_space \<subseteq> polish_space ..
+
 text {* Intervals in general, including infinite and mixtures of open and closed. *}
 
 definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
diff -r ecffea78d381 -r 635d73673b5e src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Thu Nov 15 14:04:23 2012 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Thu Nov 15 10:49:58 2012 +0100
@@ -173,87 +173,6 @@
 
 subsection "Borel space equals sigma algebras over intervals"
 
-lemma rational_boxes:
-  fixes x :: "'a\<Colon>ordered_euclidean_space"
-  assumes "0 < e"
-  shows "\<exists>a b. (\<forall>i. a $$ i \<in> \<rat>) \<and> (\<forall>i. b $$ i \<in> \<rat>) \<and> x \<in> {a <..< b} \<and> {a <..< b} \<subseteq> ball x e"
-proof -
-  def e' \<equiv> "e / (2 * sqrt (real (DIM ('a))))"
-  then have e: "0 < e'" using assms by (auto intro!: divide_pos_pos)
-  have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x $$ i \<and> x $$ i - y < e'" (is "\<forall>i. ?th i")
-  proof
-    fix i from Rats_dense_in_real[of "x $$ i - e'" "x $$ i"] e
-    show "?th i" by auto
-  qed
-  from choice[OF this] guess a .. note a = this
-  have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x $$ i < y \<and> y - x $$ i < e'" (is "\<forall>i. ?th i")
-  proof
-    fix i from Rats_dense_in_real[of "x $$ i" "x $$ i + e'"] e
-    show "?th i" by auto
-  qed
-  from choice[OF this] guess b .. note b = this
-  { fix y :: 'a assume *: "Chi a < y" "y < Chi b"
-    have "dist x y = sqrt (\<Sum>i<DIM('a). (dist (x $$ i) (y $$ i))\<twosuperior>)"
-      unfolding setL2_def[symmetric] by (rule euclidean_dist_l2)
-    also have "\<dots> < sqrt (\<Sum>i<DIM('a). e^2 / real (DIM('a)))"
-    proof (rule real_sqrt_less_mono, rule setsum_strict_mono)
-      fix i assume i: "i \<in> {..<DIM('a)}"
-      have "a i < y$$i \<and> y$$i < b i" using * i eucl_less[where 'a='a] by auto
-      moreover have "a i < x$$i" "x$$i - a i < e'" using a by auto
-      moreover have "x$$i < b i" "b i - x$$i < e'" using b by auto
-      ultimately have "\<bar>x$$i - y$$i\<bar> < 2 * e'" by auto
-      then have "dist (x $$ i) (y $$ i) < e/sqrt (real (DIM('a)))"
-        unfolding e'_def by (auto simp: dist_real_def)
-      then have "(dist (x $$ i) (y $$ i))\<twosuperior> < (e/sqrt (real (DIM('a))))\<twosuperior>"
-        by (rule power_strict_mono) auto
-      then show "(dist (x $$ i) (y $$ i))\<twosuperior> < e\<twosuperior> / real DIM('a)"
-        by (simp add: power_divide)
-    qed auto
-    also have "\<dots> = e" using `0 < e` by (simp add: real_eq_of_nat DIM_positive)
-    finally have "dist x y < e" . }
-  with a b show ?thesis
-    apply (rule_tac exI[of _ "Chi a"])
-    apply (rule_tac exI[of _ "Chi b"])
-    using eucl_less[where 'a='a] by auto
-qed
-
-lemma ex_rat_list:
-  fixes x :: "'a\<Colon>ordered_euclidean_space"
-  assumes "\<And> i. x $$ i \<in> \<rat>"
-  shows "\<exists> r. length r = DIM('a) \<and> (\<forall> i < DIM('a). of_rat (r ! i) = x $$ i)"
-proof -
-  have "\<forall>i. \<exists>r. x $$ i = of_rat r" using assms unfolding Rats_def by blast
-  from choice[OF this] guess r ..
-  then show ?thesis by (auto intro!: exI[of _ "map r [0 ..< DIM('a)]"])
-qed
-
-lemma open_UNION:
-  fixes M :: "'a\<Colon>ordered_euclidean_space set"
-  assumes "open M"
-  shows "M = UNION {(a, b) | a b. {Chi (of_rat \<circ> op ! a) <..< Chi (of_rat \<circ> op ! b)} \<subseteq> M}
-                   (\<lambda> (a, b). {Chi (of_rat \<circ> op ! a) <..< Chi (of_rat \<circ> op ! b)})"
-    (is "M = UNION ?idx ?box")
-proof safe
-  fix x assume "x \<in> M"
-  obtain e where e: "e > 0" "ball x e \<subseteq> M"
-    using openE[OF assms `x \<in> M`] by auto
-  then obtain a b where ab: "x \<in> {a <..< b}" "\<And>i. a $$ i \<in> \<rat>" "\<And>i. b $$ i \<in> \<rat>" "{a <..< b} \<subseteq> ball x e"
-    using rational_boxes[OF e(1)] by blast
-  then obtain p q where pq: "length p = DIM ('a)"
-                            "length q = DIM ('a)"
-                            "\<forall> i < DIM ('a). of_rat (p ! i) = a $$ i \<and> of_rat (q ! i) = b $$ i"
-    using ex_rat_list[OF ab(2)] ex_rat_list[OF ab(3)] by blast
-  hence p: "Chi (of_rat \<circ> op ! p) = a"
-    using euclidean_eq[of "Chi (of_rat \<circ> op ! p)" a]
-    unfolding o_def by auto
-  from pq have q: "Chi (of_rat \<circ> op ! q) = b"
-    using euclidean_eq[of "Chi (of_rat \<circ> op ! q)" b]
-    unfolding o_def by auto
-  have "x \<in> ?box (p, q)"
-    using p q ab by auto
-  thus "x \<in> UNION ?idx ?box" using ab e p q exI[of _ p] exI[of _ q] by auto
-qed auto
-
 lemma borel_sigma_sets_subset:
   "A \<subseteq> sets borel \<Longrightarrow> sigma_sets UNIV A \<subseteq> sets borel"
   using sigma_sets_subset[of A borel] by simp
@@ -519,6 +438,39 @@
     by (auto intro: sigma_sets.intros)
 qed auto
 
+lemma borel_eq_closed: "borel = sigma UNIV (Collect closed)"
+  unfolding borel_def
+proof (intro sigma_eqI sigma_sets_eqI, safe)
+  fix x :: "'a set" assume "open x"
+  hence "x = UNIV - (UNIV - x)" by auto
+  also have "\<dots> \<in> sigma_sets UNIV (Collect closed)"
+    by (rule sigma_sets.Compl)
+       (auto intro!: sigma_sets.Basic simp: `open x`)
+  finally show "x \<in> sigma_sets UNIV (Collect closed)" by simp
+next
+  fix x :: "'a set" assume "closed x"
+  hence "x = UNIV - (UNIV - x)" by auto
+  also have "\<dots> \<in> sigma_sets UNIV (Collect open)"
+    by (rule sigma_sets.Compl)
+       (auto intro!: sigma_sets.Basic simp: `closed x`)
+  finally show "x \<in> sigma_sets UNIV (Collect open)" by simp
+qed simp_all
+
+lemma borel_eq_enum_basis:
+  "borel = sigma UNIV (range enum_basis)"
+  unfolding borel_def
+proof (intro sigma_eqI sigma_sets_eqI, safe)
+  fix x::"'a set" assume "open x"
+  from open_enumerable_basisE[OF this] guess N .
+  hence x: "x = (\<Union>n. if n \<in> N then enum_basis n else {})" by (auto split: split_if_asm)
+  also have "\<dots> \<in> sigma_sets UNIV (range enum_basis)" by (rule Union) auto
+  finally show "x \<in> sigma_sets UNIV (range enum_basis)" .
+next
+  fix n
+  have "open (enum_basis n)" by (rule open_enum_basis) simp
+  thus "enum_basis n \<in> sigma_sets UNIV (Collect open)" by auto
+qed simp_all
+
 lemma borel_measurable_halfspacesI:
   fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space"
   assumes F: "borel = sigma UNIV (range F)"
diff -r ecffea78d381 -r 635d73673b5e src/HOL/Probability/Finite_Product_Measure.thy
--- a/src/HOL/Probability/Finite_Product_Measure.thy	Thu Nov 15 14:04:23 2012 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Thu Nov 15 10:49:58 2012 +0100
@@ -1161,9 +1161,6 @@
     by (intro sigma_sets_subset) (auto simp: E_generates sets_Collect_single)
 qed
 
-lemma bchoice_iff: "(\<forall>a\<in>A. \<exists>b. P a b) \<longleftrightarrow> (\<exists>f. \<forall>a\<in>A. P a (f a))"
-  by metis
-
 lemma sigma_prod_algebra_sigma_eq:
   fixes E :: "'i \<Rightarrow> 'a set set" and S :: "'i \<Rightarrow> nat \<Rightarrow> 'a set"
   assumes "finite I"
diff -r ecffea78d381 -r 635d73673b5e src/HOL/Probability/Independent_Family.thy
--- a/src/HOL/Probability/Independent_Family.thy	Thu Nov 15 14:04:23 2012 +0100
+++ b/src/HOL/Probability/Independent_Family.thy	Thu Nov 15 10:49:58 2012 +0100
@@ -8,20 +8,6 @@
   imports Probability_Measure Infinite_Product_Measure
 begin
 
-lemma INT_decseq_offset:
-  assumes "decseq F"
-  shows "(\<Inter>i. F i) = (\<Inter>i\<in>{n..}. F i)"
-proof safe
-  fix x i assume x: "x \<in> (\<Inter>i\<in>{n..}. F i)"
-  show "x \<in> F i"
-  proof cases
-    from x have "x \<in> F n" by auto
-    also assume "i \<le> n" with `decseq F` have "F n \<subseteq> F i"
-      unfolding decseq_def by simp
-    finally show ?thesis .
-  qed (insert x, simp)
-qed auto
-
 definition (in prob_space)
   "indep_sets F I \<longleftrightarrow> (\<forall>i\<in>I. F i \<subseteq> events) \<and>
     (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> (\<forall>A\<in>Pi J F. prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))))"
diff -r ecffea78d381 -r 635d73673b5e src/HOL/Probability/Infinite_Product_Measure.thy
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Thu Nov 15 14:04:23 2012 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Thu Nov 15 10:49:58 2012 +0100
@@ -8,69 +8,6 @@
   imports Probability_Measure Caratheodory Projective_Family
 begin
 
-lemma (in product_prob_space) distr_restrict:
-  assumes "J \<noteq> {}" "J \<subseteq> K" "finite K"
-  shows "(\<Pi>\<^isub>M i\<in>J. M i) = distr (\<Pi>\<^isub>M i\<in>K. M i) (\<Pi>\<^isub>M i\<in>J. M i) (\<lambda>f. restrict f J)" (is "?P = ?D")
-proof (rule measure_eqI_generator_eq)
-  have "finite J" using `J \<subseteq> K` `finite K` by (auto simp add: finite_subset)
-  interpret J: finite_product_prob_space M J proof qed fact
-  interpret K: finite_product_prob_space M K proof qed fact
-
-  let ?J = "{Pi\<^isub>E J E | E. \<forall>i\<in>J. E i \<in> sets (M i)}"
-  let ?F = "\<lambda>i. \<Pi>\<^isub>E k\<in>J. space (M k)"
-  let ?\<Omega> = "(\<Pi>\<^isub>E k\<in>J. space (M k))"
-  show "Int_stable ?J"
-    by (rule Int_stable_PiE)
-  show "range ?F \<subseteq> ?J" "(\<Union>i. ?F i) = ?\<Omega>"
-    using `finite J` by (auto intro!: prod_algebraI_finite)
-  { fix i show "emeasure ?P (?F i) \<noteq> \<infinity>" by simp }
-  show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets_into_space)
-  show "sets (\<Pi>\<^isub>M i\<in>J. M i) = sigma_sets ?\<Omega> ?J" "sets ?D = sigma_sets ?\<Omega> ?J"
-    using `finite J` by (simp_all add: sets_PiM prod_algebra_eq_finite Pi_iff)
-  
-  fix X assume "X \<in> ?J"
-  then obtain E where [simp]: "X = Pi\<^isub>E J E" and E: "\<forall>i\<in>J. E i \<in> sets (M i)" by auto
-  with `finite J` have X: "X \<in> sets (Pi\<^isub>M J M)"
-    by simp
-
-  have "emeasure ?P X = (\<Prod> i\<in>J. emeasure (M i) (E i))"
-    using E by (simp add: J.measure_times)
-  also have "\<dots> = (\<Prod> i\<in>J. emeasure (M i) (if i \<in> J then E i else space (M i)))"
-    by simp
-  also have "\<dots> = (\<Prod> i\<in>K. emeasure (M i) (if i \<in> J then E i else space (M i)))"
-    using `finite K` `J \<subseteq> K`
-    by (intro setprod_mono_one_left) (auto simp: M.emeasure_space_1)
-  also have "\<dots> = emeasure (Pi\<^isub>M K M) (\<Pi>\<^isub>E i\<in>K. if i \<in> J then E i else space (M i))"
-    using E by (simp add: K.measure_times)
-  also have "(\<Pi>\<^isub>E i\<in>K. if i \<in> J then E i else space (M i)) = (\<lambda>f. restrict f J) -` Pi\<^isub>E J E \<inter> (\<Pi>\<^isub>E i\<in>K. space (M i))"
-    using `J \<subseteq> K` sets_into_space E by (force simp:  Pi_iff split: split_if_asm)
-  finally show "emeasure (Pi\<^isub>M J M) X = emeasure ?D X"
-    using X `J \<subseteq> K` apply (subst emeasure_distr)
-    by (auto intro!: measurable_restrict_subset simp: space_PiM)
-qed
-
-lemma (in product_prob_space) emeasure_prod_emb[simp]:
-  assumes L: "J \<noteq> {}" "J \<subseteq> L" "finite L" and X: "X \<in> sets (Pi\<^isub>M J M)"
-  shows "emeasure (Pi\<^isub>M L M) (prod_emb L M J X) = emeasure (Pi\<^isub>M J M) X"
-  by (subst distr_restrict[OF L])
-     (simp add: prod_emb_def space_PiM emeasure_distr measurable_restrict_subset L X)
-
-sublocale product_prob_space \<subseteq> projective_family I "\<lambda>J. PiM J M" M
-proof
-  fix J::"'i set" assume "finite J"
-  interpret f: finite_product_prob_space M J proof qed fact
-  show "emeasure (Pi\<^isub>M J M) (space (Pi\<^isub>M J M)) \<noteq> \<infinity>" by simp
-  show "\<exists>A. range A \<subseteq> sets (Pi\<^isub>M J M) \<and>
-            (\<Union>i. A i) = space (Pi\<^isub>M J M) \<and>
-            (\<forall>i. emeasure (Pi\<^isub>M J M) (A i) \<noteq> \<infinity>)" using sigma_finite[OF `finite J`]
-    by (auto simp add: sigma_finite_measure_def)
-  show "emeasure (Pi\<^isub>M J M) (space (Pi\<^isub>M J M)) = 1" by (rule f.emeasure_space_1)
-qed simp_all
-
-lemma (in product_prob_space) PiP_PiM_finite[simp]:
-  assumes "J \<noteq> {}" "finite J" "J \<subseteq> I" shows "PiP J M (\<lambda>J. PiM J M) = PiM J M"
-  using assms by (simp add: PiP_finite)
-
 lemma (in product_prob_space) emeasure_PiM_emb_not_empty:
   assumes X: "J \<noteq> {}" "J \<subseteq> I" "finite J" "\<forall>i\<in>J. X i \<in> sets (M i)"
   shows "emeasure (Pi\<^isub>M I M) (emb I J (Pi\<^isub>E J X)) = emeasure (Pi\<^isub>M J M) (Pi\<^isub>E J X)"
diff -r ecffea78d381 -r 635d73673b5e src/HOL/Probability/Measure_Space.thy
--- a/src/HOL/Probability/Measure_Space.thy	Thu Nov 15 14:04:23 2012 +0100
+++ b/src/HOL/Probability/Measure_Space.thy	Thu Nov 15 10:49:58 2012 +0100
@@ -169,6 +169,27 @@
   finally show "f x \<le> f y" by simp
 qed
 
+lemma (in ring_of_sets) subadditive:
+  assumes f: "positive M f" "additive M f" and A: "range A \<subseteq> M" and S: "finite S"
+  shows "f (\<Union>i\<in>S. A i) \<le> (\<Sum>i\<in>S. f (A i))"
+using S
+proof (induct S)
+  case empty thus ?case using f by (auto simp: positive_def)
+next
+  case (insert x F)
+  hence in_M: "A x \<in> M" "(\<Union> i\<in>F. A i) \<in> M" "(\<Union> i\<in>F. A i) - A x \<in> M" using A by force+
+  have subs: "(\<Union> i\<in>F. A i) - A x \<subseteq> (\<Union> i\<in>F. A i)" by auto
+  have "(\<Union> i\<in>(insert x F). A i) = A x \<union> ((\<Union> i\<in>F. A i) - A x)" by auto
+  hence "f (\<Union> i\<in>(insert x F). A i) = f (A x \<union> ((\<Union> i\<in>F. A i) - A x))"
+    by simp
+  also have "\<dots> = f (A x) + f ((\<Union> i\<in>F. A i) - A x)"
+    using f(2) by (rule additiveD) (insert in_M, auto)
+  also have "\<dots> \<le> f (A x) + f (\<Union> i\<in>F. A i)"
+    using additive_increasing[OF f] in_M subs by (auto simp: increasing_def intro: add_left_mono)
+  also have "\<dots> \<le> f (A x) + (\<Sum>i\<in>F. f (A i))" using insert by (auto intro: add_left_mono)
+  finally show "f (\<Union> i\<in>(insert x F). A i) \<le> (\<Sum>i\<in>(insert x F). f (A i))" using insert by simp
+qed
+
 lemma (in ring_of_sets) countably_additive_additive:
   assumes posf: "positive M f" and ca: "countably_additive M f"
   shows "additive M f"
diff -r ecffea78d381 -r 635d73673b5e src/HOL/Probability/Probability.thy
--- a/src/HOL/Probability/Probability.thy	Thu Nov 15 14:04:23 2012 +0100
+++ b/src/HOL/Probability/Probability.thy	Thu Nov 15 10:49:58 2012 +0100
@@ -3,6 +3,7 @@
   Complete_Measure
   Probability_Measure
   Infinite_Product_Measure
+  Regularity
   Independent_Family
   Information
 begin
diff -r ecffea78d381 -r 635d73673b5e src/HOL/Probability/Projective_Family.thy
--- a/src/HOL/Probability/Projective_Family.thy	Thu Nov 15 14:04:23 2012 +0100
+++ b/src/HOL/Probability/Projective_Family.thy	Thu Nov 15 10:49:58 2012 +0100
@@ -9,6 +9,53 @@
 imports Finite_Product_Measure Probability_Measure
 begin
 
+lemma (in product_prob_space) distr_restrict:
+  assumes "J \<noteq> {}" "J \<subseteq> K" "finite K"
+  shows "(\<Pi>\<^isub>M i\<in>J. M i) = distr (\<Pi>\<^isub>M i\<in>K. M i) (\<Pi>\<^isub>M i\<in>J. M i) (\<lambda>f. restrict f J)" (is "?P = ?D")
+proof (rule measure_eqI_generator_eq)
+  have "finite J" using `J \<subseteq> K` `finite K` by (auto simp add: finite_subset)
+  interpret J: finite_product_prob_space M J proof qed fact
+  interpret K: finite_product_prob_space M K proof qed fact
+
+  let ?J = "{Pi\<^isub>E J E | E. \<forall>i\<in>J. E i \<in> sets (M i)}"
+  let ?F = "\<lambda>i. \<Pi>\<^isub>E k\<in>J. space (M k)"
+  let ?\<Omega> = "(\<Pi>\<^isub>E k\<in>J. space (M k))"
+  show "Int_stable ?J"
+    by (rule Int_stable_PiE)
+  show "range ?F \<subseteq> ?J" "(\<Union>i. ?F i) = ?\<Omega>"
+    using `finite J` by (auto intro!: prod_algebraI_finite)
+  { fix i show "emeasure ?P (?F i) \<noteq> \<infinity>" by simp }
+  show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets_into_space)
+  show "sets (\<Pi>\<^isub>M i\<in>J. M i) = sigma_sets ?\<Omega> ?J" "sets ?D = sigma_sets ?\<Omega> ?J"
+    using `finite J` by (simp_all add: sets_PiM prod_algebra_eq_finite Pi_iff)
+
+  fix X assume "X \<in> ?J"
+  then obtain E where [simp]: "X = Pi\<^isub>E J E" and E: "\<forall>i\<in>J. E i \<in> sets (M i)" by auto
+  with `finite J` have X: "X \<in> sets (Pi\<^isub>M J M)"
+    by simp
+
+  have "emeasure ?P X = (\<Prod> i\<in>J. emeasure (M i) (E i))"
+    using E by (simp add: J.measure_times)
+  also have "\<dots> = (\<Prod> i\<in>J. emeasure (M i) (if i \<in> J then E i else space (M i)))"
+    by simp
+  also have "\<dots> = (\<Prod> i\<in>K. emeasure (M i) (if i \<in> J then E i else space (M i)))"
+    using `finite K` `J \<subseteq> K`
+    by (intro setprod_mono_one_left) (auto simp: M.emeasure_space_1)
+  also have "\<dots> = emeasure (Pi\<^isub>M K M) (\<Pi>\<^isub>E i\<in>K. if i \<in> J then E i else space (M i))"
+    using E by (simp add: K.measure_times)
+  also have "(\<Pi>\<^isub>E i\<in>K. if i \<in> J then E i else space (M i)) = (\<lambda>f. restrict f J) -` Pi\<^isub>E J E \<inter> (\<Pi>\<^isub>E i\<in>K. space (M i))"
+    using `J \<subseteq> K` sets_into_space E by (force simp:  Pi_iff split: split_if_asm)
+  finally show "emeasure (Pi\<^isub>M J M) X = emeasure ?D X"
+    using X `J \<subseteq> K` apply (subst emeasure_distr)
+    by (auto intro!: measurable_restrict_subset simp: space_PiM)
+qed
+
+lemma (in product_prob_space) emeasure_prod_emb[simp]:
+  assumes L: "J \<noteq> {}" "J \<subseteq> L" "finite L" and X: "X \<in> sets (Pi\<^isub>M J M)"
+  shows "emeasure (Pi\<^isub>M L M) (prod_emb L M J X) = emeasure (Pi\<^isub>M J M) X"
+  by (subst distr_restrict[OF L])
+     (simp add: prod_emb_def space_PiM emeasure_distr measurable_restrict_subset L X)
+
 definition
   PiP :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i set \<Rightarrow> ('i \<Rightarrow> 'a) measure) \<Rightarrow> ('i \<Rightarrow> 'a) measure" where
   "PiP I M P = extend_measure (\<Pi>\<^isub>E i\<in>I. space (M i))
@@ -297,4 +344,20 @@
 
 end
 
+sublocale product_prob_space \<subseteq> projective_family I "\<lambda>J. PiM J M" M
+proof
+  fix J::"'i set" assume "finite J"
+  interpret f: finite_product_prob_space M J proof qed fact
+  show "emeasure (Pi\<^isub>M J M) (space (Pi\<^isub>M J M)) \<noteq> \<infinity>" by simp
+  show "\<exists>A. range A \<subseteq> sets (Pi\<^isub>M J M) \<and>
+            (\<Union>i. A i) = space (Pi\<^isub>M J M) \<and>
+            (\<forall>i. emeasure (Pi\<^isub>M J M) (A i) \<noteq> \<infinity>)" using sigma_finite[OF `finite J`]
+    by (auto simp add: sigma_finite_measure_def)
+  show "emeasure (Pi\<^isub>M J M) (space (Pi\<^isub>M J M)) = 1" by (rule f.emeasure_space_1)
+qed simp_all
+
+lemma (in product_prob_space) PiP_PiM_finite[simp]:
+  assumes "J \<noteq> {}" "finite J" "J \<subseteq> I" shows "PiP J M (\<lambda>J. PiM J M) = PiM J M"
+  using assms by (simp add: PiP_finite)
+
 end
diff -r ecffea78d381 -r 635d73673b5e src/HOL/Probability/Regularity.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Regularity.thy	Thu Nov 15 10:49:58 2012 +0100
@@ -0,0 +1,516 @@
+(*  Title:      HOL/Probability/Projective_Family.thy
+    Author:     Fabian Immler, TU München
+*)
+
+theory Regularity
+imports Measure_Space Borel_Space
+begin
+
+instantiation nat::topological_space
+begin
+
+definition open_nat::"nat set \<Rightarrow> bool"
+  where "open_nat s = True"
+
+instance proof qed (auto simp: open_nat_def)
+end
+
+instantiation nat::metric_space
+begin
+
+definition dist_nat::"nat \<Rightarrow> nat \<Rightarrow> real"
+  where "dist_nat n m = (if n = m then 0 else 1)"
+
+instance proof qed (auto simp: open_nat_def dist_nat_def intro: exI[where x=1])
+end
+
+instance nat::complete_space
+proof
+  fix X::"nat\<Rightarrow>nat" assume "Cauchy X"
+  hence "\<exists>n. \<forall>m\<ge>n. X m = X n"
+    by (force simp: dist_nat_def Cauchy_def split: split_if_asm dest:spec[where x=1])
+  then guess n ..
+  thus "convergent X"
+    apply (intro convergentI[where L="X n"] tendstoI)
+    unfolding eventually_sequentially dist_nat_def
+    apply (intro exI[where x=n])
+    apply (intro allI)
+    apply (drule_tac x=na in spec)
+    apply simp
+    done
+qed
+
+instance nat::enumerable_basis
+proof
+  have "topological_basis (range (\<lambda>n::nat. {n}))"
+    by (intro topological_basisI) (auto simp: open_nat_def)
+  thus "\<exists>f::nat\<Rightarrow>nat set. topological_basis (range f)" by blast
+qed
+
+subsection {* Regularity of Measures *}
+
+lemma ereal_approx_SUP:
+  fixes x::ereal
+  assumes A_notempty: "A \<noteq> {}"
+  assumes f_bound: "\<And>i. i \<in> A \<Longrightarrow> f i \<le> x"
+  assumes f_fin: "\<And>i. i \<in> A \<Longrightarrow> f i \<noteq> \<infinity>"
+  assumes f_nonneg: "\<And>i. 0 \<le> f i"
+  assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. x \<le> f i + e"
+  shows "x = (SUP i : A. f i)"
+proof (subst eq_commute, rule ereal_SUPI)
+  show "\<And>i. i \<in> A \<Longrightarrow> f i \<le> x" using f_bound by simp
+next
+  fix y :: ereal assume f_le_y: "(\<And>i::'a. i \<in> A \<Longrightarrow> f i \<le> y)"
+  with A_notempty f_nonneg have "y \<ge> 0" by auto (metis order_trans)
+  show "x \<le> y"
+  proof (rule ccontr)
+    assume "\<not> x \<le> y" hence "x > y" by simp
+    hence y_fin: "\<bar>y\<bar> \<noteq> \<infinity>" using `y \<ge> 0` by auto
+    have x_fin: "\<bar>x\<bar> \<noteq> \<infinity>" using `x > y` f_fin approx[where e = 1] by auto
+    def e \<equiv> "real ((x - y) / 2)"
+    have e: "x > y + e" "e > 0" using `x > y` y_fin x_fin by (auto simp: e_def field_simps)
+    note e(1)
+    also from approx[OF `e > 0`] obtain i where i: "i \<in> A" "x \<le> f i + e" by blast
+    note i(2)
+    finally have "y < f i" using y_fin f_fin by (metis add_right_mono linorder_not_le)
+    moreover have "f i \<le> y" by (rule f_le_y) fact
+    ultimately show False by simp
+  qed
+qed
+
+lemma ereal_approx_INF:
+  fixes x::ereal
+  assumes A_notempty: "A \<noteq> {}"
+  assumes f_bound: "\<And>i. i \<in> A \<Longrightarrow> x \<le> f i"
+  assumes f_fin: "\<And>i. i \<in> A \<Longrightarrow> f i \<noteq> \<infinity>"
+  assumes f_nonneg: "\<And>i. 0 \<le> f i"
+  assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. f i \<le> x + e"
+  shows "x = (INF i : A. f i)"
+proof (subst eq_commute, rule ereal_INFI)
+  show "\<And>i. i \<in> A \<Longrightarrow> x \<le> f i" using f_bound by simp
+next
+  fix y :: ereal assume f_le_y: "(\<And>i::'a. i \<in> A \<Longrightarrow> y \<le> f i)"
+  with A_notempty f_fin have "y \<noteq> \<infinity>" by force
+  show "y \<le> x"
+  proof (rule ccontr)
+    assume "\<not> y \<le> x" hence "y > x" by simp hence "y \<noteq> - \<infinity>" by auto
+    hence y_fin: "\<bar>y\<bar> \<noteq> \<infinity>" using `y \<noteq> \<infinity>` by auto
+    have x_fin: "\<bar>x\<bar> \<noteq> \<infinity>" using `y > x` f_fin f_nonneg approx[where e = 1] A_notempty
+      apply auto by (metis ereal_infty_less_eq(2) f_le_y)
+    def e \<equiv> "real ((y - x) / 2)"
+    have e: "y > x + e" "e > 0" using `y > x` y_fin x_fin by (auto simp: e_def field_simps)
+    from approx[OF `e > 0`] obtain i where i: "i \<in> A" "x + e \<ge> f i" by blast
+    note i(2)
+    also note e(1)
+    finally have "y > f i" .
+    moreover have "y \<le> f i" by (rule f_le_y) fact
+    ultimately show False by simp
+  qed
+qed
+
+lemma INF_approx_ereal:
+  fixes x::ereal and e::real
+  assumes "e > 0"
+  assumes INF: "x = (INF i : A. f i)"
+  assumes "\<bar>x\<bar> \<noteq> \<infinity>"
+  shows "\<exists>i \<in> A. f i < x + e"
+proof (rule ccontr, clarsimp)
+  assume "\<forall>i\<in>A. \<not> f i < x + e"
+  moreover
+  from INF have "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> f i) \<Longrightarrow> y \<le> x" by (auto intro: INF_greatest)
+  ultimately
+  have "(INF i : A. f i) = x + e" using `e > 0`
+    by (intro ereal_INFI)
+      (force, metis add.comm_neutral add_left_mono ereal_less(1)
+        linorder_not_le not_less_iff_gr_or_eq)
+  thus False using assms by auto
+qed
+
+lemma SUP_approx_ereal:
+  fixes x::ereal and e::real
+  assumes "e > 0"
+  assumes SUP: "x = (SUP i : A. f i)"
+  assumes "\<bar>x\<bar> \<noteq> \<infinity>"
+  shows "\<exists>i \<in> A. x \<le> f i + e"
+proof (rule ccontr, clarsimp)
+  assume "\<forall>i\<in>A. \<not> x \<le> f i + e"
+  moreover
+  from SUP have "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<le> y) \<Longrightarrow> y \<ge> x" by (auto intro: SUP_least)
+  ultimately
+  have "(SUP i : A. f i) = x - e" using `e > 0` `\<bar>x\<bar> \<noteq> \<infinity>`
+    by (intro ereal_SUPI)
+       (metis PInfty_neq_ereal(2) abs_ereal.simps(1) ereal_minus_le linorder_linear,
+        metis ereal_between(1) ereal_less(2) less_eq_ereal_def order_trans)
+  thus False using assms by auto
+qed
+
+lemma
+  fixes M::"'a::{enumerable_basis, complete_space} measure"
+  assumes sb: "sets M = sets borel"
+  assumes "emeasure M (space M) \<noteq> \<infinity>"
+  assumes "B \<in> sets borel"
+  shows inner_regular: "emeasure M B =
+    (SUP K : {K. K \<subseteq> B \<and> compact K}. emeasure M K)" (is "?inner B")
+  and outer_regular: "emeasure M B =
+    (INF U : {U. B \<subseteq> U \<and> open U}. emeasure M U)" (is "?outer B")
+proof -
+  have Us: "UNIV = space M" by (metis assms(1) sets_eq_imp_space_eq space_borel)
+  hence sU: "space M = UNIV" by simp
+  interpret finite_measure M by rule fact
+  have approx_inner: "\<And>A. A \<in> sets M \<Longrightarrow>
+    (\<And>e. e > 0 \<Longrightarrow> \<exists>K. K \<subseteq> A \<and> compact K \<and> emeasure M A \<le> emeasure M K + ereal e) \<Longrightarrow> ?inner A"
+    by (rule ereal_approx_SUP)
+      (force intro!: emeasure_mono simp: compact_imp_closed emeasure_eq_measure)+
+  have approx_outer: "\<And>A. A \<in> sets M \<Longrightarrow>
+    (\<And>e. e > 0 \<Longrightarrow> \<exists>B. A \<subseteq> B \<and> open B \<and> emeasure M B \<le> emeasure M A + ereal e) \<Longrightarrow> ?outer A"
+    by (rule ereal_approx_INF)
+       (force intro!: emeasure_mono simp: emeasure_eq_measure sb)+
+  from countable_dense_setE guess x::"nat \<Rightarrow> 'a"  . note x = this
+  {
+    fix r::real assume "r > 0" hence "\<And>y. open (ball y r)" "\<And>y. ball y r \<noteq> {}" by auto
+    with x[OF this]
+    have x: "space M = (\<Union>n. cball (x n) r)"
+      by (auto simp add: sU) (metis dist_commute order_less_imp_le)
+    have "(\<lambda>k. emeasure M (\<Union>n\<in>{0..k}. cball (x n) r)) ----> M (\<Union>k. (\<Union>n\<in>{0..k}. cball (x n) r))"
+      by (rule Lim_emeasure_incseq)
+        (auto intro!: borel_closed bexI simp: closed_cball incseq_def Us sb)
+    also have "(\<Union>k. (\<Union>n\<in>{0..k}. cball (x n) r)) = space M"
+      unfolding x by force
+    finally have "(\<lambda>k. M (\<Union>n\<in>{0..k}. cball (x n) r)) ----> M (space M)" .
+  } note M_space = this
+  {
+    fix e ::real and n :: nat assume "e > 0" "n > 0"
+    hence "1/n > 0" "e * 2 powr - n > 0" by (auto intro: mult_pos_pos)
+    from M_space[OF `1/n>0`]
+    have "(\<lambda>k. measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n))) ----> measure M (space M)"
+      unfolding emeasure_eq_measure by simp
+    from metric_LIMSEQ_D[OF this `0 < e * 2 powr -n`]
+    obtain k where "dist (measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n))) (measure M (space M)) <
+      e * 2 powr -n"
+      by auto
+    hence "measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n)) \<ge>
+      measure M (space M) - e * 2 powr -real n"
+      by (auto simp: dist_real_def)
+    hence "\<exists>k. measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n)) \<ge>
+      measure M (space M) - e * 2 powr - real n" ..
+  } note k=this
+  hence "\<forall>e\<in>{0<..}. \<forall>(n::nat)\<in>{0<..}. \<exists>k.
+    measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n)) \<ge> measure M (space M) - e * 2 powr - real n"
+    by blast
+  then obtain k where k: "\<forall>e\<in>{0<..}. \<forall>n\<in>{0<..}. measure M (space M) - e * 2 powr - real (n::nat)
+    \<le> measure M (\<Union>i\<in>{0..k e n}. cball (x i) (1 / n))"
+    apply atomize_elim unfolding bchoice_iff .
+  hence k: "\<And>e n. e > 0 \<Longrightarrow> n > 0 \<Longrightarrow> measure M (space M) - e * 2 powr - n
+    \<le> measure M (\<Union>i\<in>{0..k e n}. cball (x i) (1 / n))"
+    unfolding Ball_def by blast
+  have approx_space:
+    "\<And>e. e > 0 \<Longrightarrow>
+      \<exists>K \<in> {K. K \<subseteq> space M \<and> compact K}. emeasure M (space M) \<le> emeasure M K + ereal e"
+      (is "\<And>e. _ \<Longrightarrow> ?thesis e")
+  proof -
+    fix e :: real assume "e > 0"
+    def B \<equiv> "\<lambda>n. \<Union>i\<in>{0..k e (Suc n)}. cball (x i) (1 / Suc n)"
+    have "\<And>n. closed (B n)" by (auto simp: B_def closed_cball)
+    hence [simp]: "\<And>n. B n \<in> sets M" by (simp add: sb)
+    from k[OF `e > 0` zero_less_Suc]
+    have "\<And>n. measure M (space M) - measure M (B n) \<le> e * 2 powr - real (Suc n)"
+      by (simp add: algebra_simps B_def finite_measure_compl)
+    hence B_compl_le: "\<And>n::nat. measure M (space M - B n) \<le> e * 2 powr - real (Suc n)"
+      by (simp add: finite_measure_compl)
+    def K \<equiv> "\<Inter>n. B n"
+    from `closed (B _)` have "closed K" by (auto simp: K_def)
+    hence [simp]: "K \<in> sets M" by (simp add: sb)
+    have "measure M (space M) - measure M K = measure M (space M - K)"
+      by (simp add: finite_measure_compl)
+    also have "\<dots> = emeasure M (\<Union>n. space M - B n)" by (auto simp: K_def emeasure_eq_measure)
+    also have "\<dots> \<le> (\<Sum>n. emeasure M (space M - B n))"
+      by (rule emeasure_subadditive_countably) (auto simp: summable_def)
+    also have "\<dots> \<le> (\<Sum>n. ereal (e*2 powr - real (Suc n)))"
+      using B_compl_le by (intro suminf_le_pos) (simp_all add: measure_nonneg emeasure_eq_measure)
+    also have "\<dots> \<le> (\<Sum>n. ereal (e * (1 / 2) ^ Suc n))"
+      by (simp add: powr_minus inverse_eq_divide powr_realpow field_simps power_divide)
+    also have "\<dots> = (\<Sum>n. ereal e * ((1 / 2) ^ Suc n))"
+      unfolding times_ereal.simps[symmetric] ereal_power[symmetric] one_ereal_def numeral_eq_ereal
+      by simp
+    also have "\<dots> = ereal e * (\<Sum>n. ((1 / 2) ^ Suc n))"
+      by (rule suminf_cmult_ereal) (auto simp: `0 < e` less_imp_le)
+    also have "\<dots> = e" unfolding suminf_half_series_ereal by simp
+    finally have "measure M (space M) \<le> measure M K + e" by simp
+    hence "emeasure M (space M) \<le> emeasure M K + e" by (simp add: emeasure_eq_measure)
+    moreover have "compact K"
+      unfolding compact_eq_totally_bounded
+    proof safe
+      show "complete K" using `closed K` by (simp add: complete_eq_closed)
+      fix e'::real assume "0 < e'"
+      from nat_approx_posE[OF this] guess n . note n = this
+      let ?k = "x ` {0..k e (Suc n)}"
+      have "finite ?k" by simp
+      moreover have "K \<subseteq> \<Union>(\<lambda>x. ball x e') ` ?k" unfolding K_def B_def using n by force
+      ultimately show "\<exists>k. finite k \<and> K \<subseteq> \<Union>(\<lambda>x. ball x e') ` k" by blast
+    qed
+    ultimately
+    show "?thesis e " by (auto simp: sU)
+  qed
+  have closed_in_D: "\<And>A. closed A \<Longrightarrow> ?inner A \<and> ?outer A"
+  proof
+    fix A::"'a set" assume "closed A" hence "A \<in> sets borel" by (simp add: compact_imp_closed)
+    hence [simp]: "A \<in> sets M" by (simp add: sb)
+    show "?inner A"
+    proof (rule approx_inner)
+      fix e::real assume "e > 0"
+      from approx_space[OF this] obtain K where
+        K: "K \<subseteq> space M" "compact K" "emeasure M (space M) \<le> emeasure M K + e"
+        by (auto simp: emeasure_eq_measure)
+      hence [simp]: "K \<in> sets M" by (simp add: sb compact_imp_closed)
+      have "M A - M (A \<inter> K) = measure M A - measure M (A \<inter> K)"
+        by (simp add: emeasure_eq_measure)
+      also have "\<dots> = measure M (A - A \<inter> K)"
+        by (subst finite_measure_Diff) auto
+      also have "A - A \<inter> K = A \<union> K - K" by auto
+      also have "measure M \<dots> = measure M (A \<union> K) - measure M K"
+        by (subst finite_measure_Diff) auto
+      also have "\<dots> \<le> measure M (space M) - measure M K"
+        by (simp add: emeasure_eq_measure sU sb finite_measure_mono)
+      also have "\<dots> \<le> e" using K by (simp add: emeasure_eq_measure)
+      finally have "emeasure M A \<le> emeasure M (A \<inter> K) + ereal e"
+        by (simp add: emeasure_eq_measure algebra_simps)
+      moreover have "A \<inter> K \<subseteq> A" "compact (A \<inter> K)" using `closed A` `compact K` by auto
+      ultimately show "\<exists>K \<subseteq> A. compact K \<and> emeasure M A \<le> emeasure M K + ereal e"
+        by blast
+    qed simp
+    show "?outer A"
+    proof cases
+      assume "A \<noteq> {}"
+      let ?G = "\<lambda>d. {x. infdist x A < d}"
+      {
+        fix d
+        have "?G d = (\<lambda>x. infdist x A) -` {..<d}" by auto
+        also have "open \<dots>"
+          by (intro continuous_open_vimage) (auto intro!: continuous_infdist continuous_at_id)
+        finally have "open (?G d)" .
+      } note open_G = this
+      from in_closed_iff_infdist_zero[OF `closed A` `A \<noteq> {}`]
+      have "A = {x. infdist x A = 0}" by auto
+      also have "\<dots> = (\<Inter>i. ?G (1/real (Suc i)))"
+      proof (auto, rule ccontr)
+        fix x
+        assume "infdist x A \<noteq> 0"
+        hence pos: "infdist x A > 0" using infdist_nonneg[of x A] by simp
+        from nat_approx_posE[OF this] guess n .
+        moreover
+        assume "\<forall>i. infdist x A < 1 / real (Suc i)"
+        hence "infdist x A < 1 / real (Suc n)" by auto
+        ultimately show False by simp
+      qed
+      also have "M \<dots> = (INF n. emeasure M (?G (1 / real (Suc n))))"
+      proof (rule INF_emeasure_decseq[symmetric], safe)
+        fix i::nat
+        from open_G[of "1 / real (Suc i)"]
+        show "?G (1 / real (Suc i)) \<in> sets M" by (simp add: sb borel_open)
+      next
+        show "decseq (\<lambda>i. {x. infdist x A < 1 / real (Suc i)})"
+          by (auto intro: less_trans intro!: divide_strict_left_mono mult_pos_pos
+            simp: decseq_def le_eq_less_or_eq)
+      qed simp
+      finally
+      have "emeasure M A = (INF n. emeasure M {x. infdist x A < 1 / real (Suc n)})" .
+      moreover
+      have "\<dots> \<ge> (INF U:{U. A \<subseteq> U \<and> open U}. emeasure M U)"
+      proof (intro INF_mono)
+        fix m
+        have "?G (1 / real (Suc m)) \<in> {U. A \<subseteq> U \<and> open U}" using open_G by auto
+        moreover have "M (?G (1 / real (Suc m))) \<le> M (?G (1 / real (Suc m)))" by simp
+        ultimately show "\<exists>U\<in>{U. A \<subseteq> U \<and> open U}.
+          emeasure M U \<le> emeasure M {x. infdist x A < 1 / real (Suc m)}"
+          by blast
+      qed
+      moreover
+      have "emeasure M A \<le> (INF U:{U. A \<subseteq> U \<and> open U}. emeasure M U)"
+        by (rule INF_greatest) (auto intro!: emeasure_mono simp: sb)
+      ultimately show ?thesis by simp
+    qed (auto intro!: ereal_INFI)
+  qed
+  let ?D = "{B \<in> sets M. ?inner B \<and> ?outer B}"
+  interpret dynkin: dynkin_system "space M" ?D
+  proof (rule dynkin_systemI)
+    have "{U::'a set. space M \<subseteq> U \<and> open U} = {space M}" by (auto simp add: sU)
+    hence "?outer (space M)" by (simp add: min_def INF_def)
+    moreover
+    have "?inner (space M)"
+    proof (rule ereal_approx_SUP)
+      fix e::real assume "0 < e"
+      thus "\<exists>K\<in>{K. K \<subseteq> space M \<and> compact K}. emeasure M (space M) \<le> emeasure M K + ereal e"
+        by (rule approx_space)
+    qed (auto intro: emeasure_mono simp: sU sb intro!: exI[where x="{}"])
+    ultimately show "space M \<in> ?D" by (simp add: sU sb)
+  next
+    fix B assume "B \<in> ?D" thus "B \<subseteq> space M" by (simp add: sU)
+    from `B \<in> ?D` have [simp]: "B \<in> sets M" and "?inner B" "?outer B" by auto
+    hence inner: "emeasure M B = (SUP K:{K. K \<subseteq> B \<and> compact K}. emeasure M K)"
+      and outer: "emeasure M B = (INF U:{U. B \<subseteq> U \<and> open U}. emeasure M U)" by auto
+    have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
+    also have "\<dots> = (INF K:{K. K \<subseteq> B \<and> compact K}. M (space M) -  M K)"
+      unfolding inner by (subst INFI_ereal_cminus) force+
+    also have "\<dots> = (INF U:{U. U \<subseteq> B \<and> compact U}. M (space M - U))"
+      by (rule INF_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
+    also have "\<dots> \<ge> (INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U))"
+      by (rule INF_superset_mono) (auto simp add: compact_imp_closed)
+    also have "(INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U)) =
+      (INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U)"
+      by (subst INF_image[of "\<lambda>u. space M - u", symmetric])
+         (rule INF_cong, auto simp add: sU intro!: INF_cong)
+    finally have
+      "(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<le> emeasure M (space M - B)" .
+    moreover have
+      "(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<ge> emeasure M (space M - B)"
+      by (auto simp: sb sU intro!: INF_greatest emeasure_mono)
+    ultimately have "?outer (space M - B)" by simp
+    moreover
+    {
+      have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
+      also have "\<dots> = (SUP U: {U. B \<subseteq> U \<and> open U}. M (space M) -  M U)"
+        unfolding outer by (subst SUPR_ereal_cminus) auto
+      also have "\<dots> = (SUP U:{U. B \<subseteq> U \<and> open U}. M (space M - U))"
+        by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
+      also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)"
+        by (subst SUP_image[of "\<lambda>u. space M - u", symmetric])
+           (rule SUP_cong, auto simp: sU)
+      also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
+      proof (safe intro!: antisym SUP_least)
+        fix K assume "closed K" "K \<subseteq> space M - B"
+        from closed_in_D[OF `closed K`]
+        have K_inner: "emeasure M K = (SUP K:{Ka. Ka \<subseteq> K \<and> compact Ka}. emeasure M K)" by simp
+        show "emeasure M K \<le> (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
+          unfolding K_inner using `K \<subseteq> space M - B`
+          by (auto intro!: SUP_upper SUP_least)
+      qed (fastforce intro!: SUP_least SUP_upper simp: compact_imp_closed)
+      finally have "?inner (space M - B)" .
+    } hence "?inner (space M - B)" .
+    ultimately show "space M - B \<in> ?D" by auto
+  next
+    fix D :: "nat \<Rightarrow> _"
+    assume "range D \<subseteq> ?D" hence "range D \<subseteq> sets M" by auto
+    moreover assume "disjoint_family D"
+    ultimately have M[symmetric]: "(\<Sum>i. M (D i)) = M (\<Union>i. D i)" by (rule suminf_emeasure)
+    also have "(\<lambda>n. \<Sum>i\<in>{0..<n}. M (D i)) ----> (\<Sum>i. M (D i))"
+      by (intro summable_sumr_LIMSEQ_suminf summable_ereal_pos emeasure_nonneg)
+    finally have measure_LIMSEQ: "(\<lambda>n. \<Sum>i = 0..<n. measure M (D i)) ----> measure M (\<Union>i. D i)"
+      by (simp add: emeasure_eq_measure)
+    have "(\<Union>i. D i) \<in> sets M" using `range D \<subseteq> sets M` by auto
+    moreover
+    hence "?inner (\<Union>i. D i)"
+    proof (rule approx_inner)
+      fix e::real assume "e > 0"
+      with measure_LIMSEQ
+      have "\<exists>no. \<forall>n\<ge>no. \<bar>(\<Sum>i = 0..<n. measure M (D i)) -measure M (\<Union>x. D x)\<bar> < e/2"
+        by (auto simp: LIMSEQ_def dist_real_def simp del: less_divide_eq_numeral1)
+      hence "\<exists>n0. \<bar>(\<Sum>i = 0..<n0. measure M (D i)) - measure M (\<Union>x. D x)\<bar> < e/2" by auto
+      then obtain n0 where n0: "\<bar>(\<Sum>i = 0..<n0. measure M (D i)) - measure M (\<Union>i. D i)\<bar> < e/2"
+        unfolding choice_iff by blast
+      have "ereal (\<Sum>i = 0..<n0. measure M (D i)) = (\<Sum>i = 0..<n0. M (D i))"
+        by (auto simp add: emeasure_eq_measure)
+      also have "\<dots> = (\<Sum>i<n0. M (D i))" by (rule setsum_cong) auto
+      also have "\<dots> \<le> (\<Sum>i. M (D i))" by (rule suminf_upper) (auto simp: emeasure_nonneg)
+      also have "\<dots> = M (\<Union>i. D i)" by (simp add: M)
+      also have "\<dots> = measure M (\<Union>i. D i)" by (simp add: emeasure_eq_measure)
+      finally have n0: "measure M (\<Union>i. D i) - (\<Sum>i = 0..<n0. measure M (D i)) < e/2"
+        using n0 by auto
+      have "\<forall>i. \<exists>K. K \<subseteq> D i \<and> compact K \<and> emeasure M (D i) \<le> emeasure M K + e/(2*Suc n0)"
+      proof
+        fix i
+        from `0 < e` have "0 < e/(2*Suc n0)" by (auto intro: divide_pos_pos)
+        have "emeasure M (D i) = (SUP K:{K. K \<subseteq> (D i) \<and> compact K}. emeasure M K)"
+          using `range D \<subseteq> ?D` by blast
+        from SUP_approx_ereal[OF `0 < e/(2*Suc n0)` this]
+        show "\<exists>K. K \<subseteq> D i \<and> compact K \<and> emeasure M (D i) \<le> emeasure M K + e/(2*Suc n0)"
+          by (auto simp: emeasure_eq_measure)
+      qed
+      then obtain K where K: "\<And>i. K i \<subseteq> D i" "\<And>i. compact (K i)"
+        "\<And>i. emeasure M (D i) \<le> emeasure M (K i) + e/(2*Suc n0)"
+        unfolding choice_iff by blast
+      let ?K = "\<Union>i\<in>{0..<n0}. K i"
+      have "disjoint_family_on K {0..<n0}" using K `disjoint_family D`
+        unfolding disjoint_family_on_def by blast
+      hence mK: "measure M ?K = (\<Sum>i = 0..<n0. measure M (K i))" using K
+        by (intro finite_measure_finite_Union) (auto simp: sb compact_imp_closed)
+      have "measure M (\<Union>i. D i) < (\<Sum>i = 0..<n0. measure M (D i)) + e/2" using n0 by simp
+      also have "(\<Sum>i = 0..<n0. measure M (D i)) \<le> (\<Sum>i = 0..<n0. measure M (K i) + e/(2*Suc n0))"
+        using K by (auto intro: setsum_mono simp: emeasure_eq_measure)
+      also have "\<dots> = (\<Sum>i = 0..<n0. measure M (K i)) + (\<Sum>i = 0..<n0. e/(2*Suc n0))"
+        by (simp add: setsum.distrib)
+      also have "\<dots> \<le> (\<Sum>i = 0..<n0. measure M (K i)) +  e / 2" using `0 < e`
+        by (auto simp: real_of_nat_def[symmetric] field_simps intro!: mult_left_mono)
+      finally
+      have "measure M (\<Union>i. D i) < (\<Sum>i = 0..<n0. measure M (K i)) + e / 2 + e / 2"
+        by auto
+      hence "M (\<Union>i. D i) < M ?K + e" by (auto simp: mK emeasure_eq_measure)
+      moreover
+      have "?K \<subseteq> (\<Union>i. D i)" using K by auto
+      moreover
+      have "compact ?K" using K by auto
+      ultimately
+      have "?K\<subseteq>(\<Union>i. D i) \<and> compact ?K \<and> emeasure M (\<Union>i. D i) \<le> emeasure M ?K + ereal e" by simp
+      thus "\<exists>K\<subseteq>\<Union>i. D i. compact K \<and> emeasure M (\<Union>i. D i) \<le> emeasure M K + ereal e" ..
+    qed
+    moreover have "?outer (\<Union>i. D i)"
+    proof (rule approx_outer[OF `(\<Union>i. D i) \<in> sets M`])
+      fix e::real assume "e > 0"
+      have "\<forall>i::nat. \<exists>U. D i \<subseteq> U \<and> open U \<and> e/(2 powr Suc i) > emeasure M U - emeasure M (D i)"
+      proof
+        fix i::nat
+        from `0 < e` have "0 < e/(2 powr Suc i)" by (auto intro: divide_pos_pos)
+        have "emeasure M (D i) = (INF U:{U. (D i) \<subseteq> U \<and> open U}. emeasure M U)"
+          using `range D \<subseteq> ?D` by blast
+        from INF_approx_ereal[OF `0 < e/(2 powr Suc i)` this]
+        show "\<exists>U. D i \<subseteq> U \<and> open U \<and> e/(2 powr Suc i) > emeasure M U - emeasure M (D i)"
+          by (auto simp: emeasure_eq_measure)
+      qed
+      then obtain U where U: "\<And>i. D i \<subseteq> U i" "\<And>i. open (U i)"
+        "\<And>i. e/(2 powr Suc i) > emeasure M (U i) - emeasure M (D i)"
+        unfolding choice_iff by blast
+      let ?U = "\<Union>i. U i"
+      have "M ?U - M (\<Union>i. D i) = M (?U - (\<Union>i. D i))" using U  `(\<Union>i. D i) \<in> sets M`
+        by (subst emeasure_Diff) (auto simp: sb)
+      also have "\<dots> \<le> M (\<Union>i. U i - D i)" using U  `range D \<subseteq> sets M`
+        by (intro emeasure_mono) (auto simp: sb intro!: countable_nat_UN Diff)
+      also have "\<dots> \<le> (\<Sum>i. M (U i - D i))" using U  `range D \<subseteq> sets M`
+        by (intro emeasure_subadditive_countably) (auto intro!: Diff simp: sb)
+      also have "\<dots> \<le> (\<Sum>i. ereal e/(2 powr Suc i))" using U `range D \<subseteq> sets M`
+        by (intro suminf_le_pos, subst emeasure_Diff)
+           (auto simp: emeasure_Diff emeasure_eq_measure sb measure_nonneg intro: less_imp_le)
+      also have "\<dots> \<le> (\<Sum>n. ereal (e * (1 / 2) ^ Suc n))"
+        by (simp add: powr_minus inverse_eq_divide powr_realpow field_simps power_divide)
+      also have "\<dots> = (\<Sum>n. ereal e * ((1 / 2) ^  Suc n))"
+        unfolding times_ereal.simps[symmetric] ereal_power[symmetric] one_ereal_def numeral_eq_ereal
+        by simp
+      also have "\<dots> = ereal e * (\<Sum>n. ((1 / 2) ^ Suc n))"
+        by (rule suminf_cmult_ereal) (auto simp: `0 < e` less_imp_le)
+      also have "\<dots> = e" unfolding suminf_half_series_ereal by simp
+      finally
+      have "emeasure M ?U \<le> emeasure M (\<Union>i. D i) + ereal e" by (simp add: emeasure_eq_measure)
+      moreover
+      have "(\<Union>i. D i) \<subseteq> ?U" using U by auto
+      moreover
+      have "open ?U" using U by auto
+      ultimately
+      have "(\<Union>i. D i) \<subseteq> ?U \<and> open ?U \<and> emeasure M ?U \<le> emeasure M (\<Union>i. D i) + ereal e" by simp
+      thus "\<exists>B. (\<Union>i. D i) \<subseteq> B \<and> open B \<and> emeasure M B \<le> emeasure M (\<Union>i. D i) + ereal e" ..
+    qed
+    ultimately show "(\<Union>i. D i) \<in> ?D" by safe
+  qed
+  have "sets borel = sigma_sets (space M) (Collect closed)" by (simp add: borel_eq_closed sU)
+  also have "\<dots> = dynkin (space M) (Collect closed)"
+  proof (rule sigma_eq_dynkin)
+    show "Collect closed \<subseteq> Pow (space M)" using Sigma_Algebra.sets_into_space by (auto simp: sU)
+    show "Int_stable (Collect closed)" by (auto simp: Int_stable_def)
+  qed
+  also have "\<dots> \<subseteq> ?D" using closed_in_D
+    by (intro dynkin.dynkin_subset) (auto simp add: compact_imp_closed sb)
+  finally have "sets borel \<subseteq> ?D" .
+  moreover have "?D \<subseteq> sets borel" by (auto simp: sb)
+  ultimately have "sets borel = ?D" by simp
+  with assms show "?inner B" and "?outer B" by auto
+qed
+
+end
+
diff -r ecffea78d381 -r 635d73673b5e src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Thu Nov 15 14:04:23 2012 +0100
+++ b/src/HOL/SEQ.thy	Thu Nov 15 10:49:58 2012 +0100
@@ -171,6 +171,12 @@
   thus ?case by arith
 qed
 
+lemma subseq_o: "subseq r \<Longrightarrow> subseq s \<Longrightarrow> subseq (r \<circ> s)"
+  unfolding subseq_def by simp
+
+lemma subseq_mono: assumes "subseq r" "m < n" shows "r m < r n"
+  using assms by (auto simp: subseq_def)
+
 lemma incseq_imp_monoseq:  "incseq X \<Longrightarrow> monoseq X"
   by (simp add: incseq_def monoseq_def)
 
@@ -181,6 +187,20 @@
   fixes X :: "nat \<Rightarrow> 'a::ordered_ab_group_add" shows "decseq X = incseq (\<lambda>n. - X n)" 
   by (simp add: decseq_def incseq_def)
 
+lemma INT_decseq_offset:
+  assumes "decseq F"
+  shows "(\<Inter>i. F i) = (\<Inter>i\<in>{n..}. F i)"
+proof safe
+  fix x i assume x: "x \<in> (\<Inter>i\<in>{n..}. F i)"
+  show "x \<in> F i"
+  proof cases
+    from x have "x \<in> F n" by auto
+    also assume "i \<le> n" with `decseq F` have "F n \<subseteq> F i"
+      unfolding decseq_def by simp
+    finally show ?thesis .
+  qed (insert x, simp)
+qed auto
+
 subsection {* Defintions of limits *}
 
 abbreviation (in topological_space)