# HG changeset patch
# User immler
# Date 1360773687 -3600
# Node ID fa66ed645b7f2256f431a034539cd134bb227527
# Parent  3f9dbd2cc4751ae75ccc0d5ed2a8fa0f8b523e72# Parent  66d0298fc554afb54eac93656ae34e9bd4d1093f
merged

diff -r 66d0298fc554 -r fa66ed645b7f src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Wed Feb 13 16:30:34 2013 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Wed Feb 13 17:41:27 2013 +0100
@@ -3368,4 +3368,80 @@
   foldr (%c r. (k c + of_nat n) * r) cs (g c0 a $ n)"
   by (induct cs arbitrary: c0) (auto simp add: algebra_simps f)
 
+lemma dist_less_imp_nth_equal:
+  assumes "dist f g < inverse (2 ^ i)"
+  assumes "j \<le> i"
+  shows "f $ j = g $ j"
+proof cases
+  assume "f \<noteq> g"
+  hence "\<exists>n. f $ n \<noteq> g $ n" by (simp add: fps_eq_iff)
+  with assms have "i < The (leastP (\<lambda>n. f $ n \<noteq> g $ n))"
+    by (simp add: split_if_asm dist_fps_def)
+  moreover
+  from fps_eq_least_unique[OF `f \<noteq> g`]
+  obtain n where "leastP (\<lambda>n. f$n \<noteq> g$n) n" "The (leastP (\<lambda>n. f $ n \<noteq> g $ n)) = n" by blast
+  moreover hence "\<And>m. m < n \<Longrightarrow> f$m = g$m" "f$n \<noteq> g$n"
+    by (auto simp add: leastP_def setge_def)
+  ultimately show ?thesis using `j \<le> i` by simp
+qed simp
+
+lemma nth_equal_imp_dist_less:
+  assumes "\<And>j. j \<le> i \<Longrightarrow> f $ j = g $ j"
+  shows "dist f g < inverse (2 ^ i)"
+proof cases
+  assume "f \<noteq> g"
+  hence "\<exists>n. f $ n \<noteq> g $ n" by (simp add: fps_eq_iff)
+  with assms have "dist f g = inverse (2 ^ (The (leastP (\<lambda>n. f $ n \<noteq> g $ n))))"
+    by (simp add: split_if_asm dist_fps_def)
+  moreover
+  from fps_eq_least_unique[OF `f \<noteq> g`]
+  obtain n where "leastP (\<lambda>n. f$n \<noteq> g$n) n" "The (leastP (\<lambda>n. f $ n \<noteq> g $ n)) = n" by blast
+  with assms have "i < The (leastP (\<lambda>n. f $ n \<noteq> g $ n))"
+    by (metis (full_types) leastPD1 not_le)
+  ultimately show ?thesis by simp
+qed simp
+
+lemma dist_less_eq_nth_equal:
+  shows "dist f g < inverse (2 ^ i) \<longleftrightarrow> (\<forall>j \<le> i. f $ j = g $ j)"
+  using dist_less_imp_nth_equal nth_equal_imp_dist_less by blast
+
+instance fps :: (comm_ring_1) complete_space
+proof
+  fix X::"nat \<Rightarrow> 'a fps"
+  assume "Cauchy X"
+  {
+    fix i
+    have "0 < inverse ((2::real)^i)" by simp
+    from metric_CauchyD[OF `Cauchy X` this] dist_less_imp_nth_equal
+    have "\<exists>M. \<forall>m \<ge> M. \<forall>j\<le>i. X M $ j = X m $ j" by blast
+  }
+  then obtain M where M: "\<forall>i. \<forall>m \<ge> M i. \<forall>j \<le> i. X (M i) $ j = X m $ j" by metis
+  hence "\<forall>i. \<forall>m \<ge> M i. \<forall>j \<le> i. X (M i) $ j = X m $ j" by metis
+  show "convergent X"
+  proof (rule convergentI)
+    show "X ----> Abs_fps (\<lambda>i. X (M i) $ i)"
+      unfolding tendsto_iff
+    proof safe
+      fix e::real assume "0 < e"
+      with LIMSEQ_inverse_realpow_zero[of 2, simplified, simplified filterlim_iff,
+        THEN spec, of "\<lambda>x. x < e"]
+      have "eventually (\<lambda>i. inverse (2 ^ i) < e) sequentially"
+        by safe (auto simp: eventually_nhds)
+      then obtain i where "inverse (2 ^ i) < e" by (auto simp: eventually_sequentially)
+      have "eventually (\<lambda>x. M i \<le> x) sequentially" by (auto simp: eventually_sequentially)
+      thus "eventually (\<lambda>x. dist (X x) (Abs_fps (\<lambda>i. X (M i) $ i)) < e) sequentially"
+      proof eventually_elim
+        fix x assume "M i \<le> x"
+        moreover
+        have "\<And>j. j \<le> i \<Longrightarrow> X (M i) $ j = X (M j) $ j"
+          using M by (metis nat_le_linear)
+        ultimately have "dist (X x) (Abs_fps (\<lambda>j. X (M j) $ j)) < inverse (2 ^ i)"
+          using M by (force simp: dist_less_eq_nth_equal)
+        also note `inverse (2 ^ i) < e`
+        finally show "dist (X x) (Abs_fps (\<lambda>j. X (M j) $ j)) < e" .
+      qed
+    qed
+  qed
+qed
+
 end
diff -r 66d0298fc554 -r fa66ed645b7f src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Feb 13 16:30:34 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Feb 13 17:41:27 2013 +0100
@@ -170,99 +170,6 @@
   where "countable D" "\<And>X. open X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> \<exists>d \<in> D. d \<in> X"
   using countable_dense_exists by blast
 
-text {* Construction of an increasing sequence approximating open sets,
-  therefore basis which is closed under union. *}
-
-definition union_closed_basis::"'a set set" where
-  "union_closed_basis = (\<lambda>l. \<Union>set l) ` lists B"
-
-lemma basis_union_closed_basis: "topological_basis union_closed_basis"
-proof (rule topological_basisI)
-  fix O' and x::'a assume "open O'" "x \<in> O'"
-  from topological_basisE[OF is_basis this] guess B' . note B' = this
-  thus "\<exists>B'\<in>union_closed_basis. x \<in> B' \<and> B' \<subseteq> O'" unfolding union_closed_basis_def
-    by (auto intro!: bexI[where x="[B']"])
-next
-  fix B' assume "B' \<in> union_closed_basis"
-  thus "open B'"
-    using topological_basis_open[OF is_basis]
-    by (auto simp: union_closed_basis_def)
-qed
-
-lemma countable_union_closed_basis: "countable union_closed_basis"
-  unfolding union_closed_basis_def using countable_basis by simp
-
-lemmas open_union_closed_basis = topological_basis_open[OF basis_union_closed_basis]
-
-lemma union_closed_basis_ex:
- assumes X: "X \<in> union_closed_basis"
- shows "\<exists>B'. finite B' \<and> X = \<Union>B' \<and> B' \<subseteq> B"
-proof -
-  from X obtain l where "\<And>x. x\<in>set l \<Longrightarrow> x\<in>B" "X = \<Union>set l" by (auto simp: union_closed_basis_def)
-  thus ?thesis by auto
-qed
-
-lemma union_closed_basisE:
-  assumes "X \<in> union_closed_basis"
-  obtains B' where "finite B'" "X = \<Union>B'" "B' \<subseteq> B" using union_closed_basis_ex[OF assms] by blast
-
-lemma union_closed_basisI:
-  assumes "finite B'" "X = \<Union>B'" "B' \<subseteq> B"
-  shows "X \<in> union_closed_basis"
-proof -
-  from finite_list[OF `finite B'`] guess l ..
-  thus ?thesis using assms unfolding union_closed_basis_def by (auto intro!: image_eqI[where x=l])
-qed
-
-lemma empty_basisI[intro]: "{} \<in> union_closed_basis"
-  by (rule union_closed_basisI[of "{}"]) auto
-
-lemma union_basisI[intro]:
-  assumes "X \<in> union_closed_basis" "Y \<in> union_closed_basis"
-  shows "X \<union> Y \<in> union_closed_basis"
-  using assms by (auto intro: union_closed_basisI elim!:union_closed_basisE)
-
-lemma open_imp_Union_of_incseq:
-  assumes "open X"
-  shows "\<exists>S. incseq S \<and> (\<Union>j. S j) = X \<and> range S \<subseteq> union_closed_basis"
-proof -
-  from open_countable_basis_ex[OF `open X`]
-  obtain B' where B': "B'\<subseteq>B" "X = \<Union>B'" by auto
-  from this(1) countable_basis have "countable B'" by (rule countable_subset)
-  show ?thesis
-  proof cases
-    assume "B' \<noteq> {}"
-    def S \<equiv> "\<lambda>n. \<Union>i\<in>{0..n}. from_nat_into B' i"
-    have S:"\<And>n. S n = \<Union>{from_nat_into B' i|i. i\<in>{0..n}}" unfolding S_def by force
-    have "incseq S" by (force simp: S_def incseq_Suc_iff)
-    moreover
-    have "(\<Union>j. S j) = X" unfolding B'
-    proof safe
-      fix x X assume "X \<in> B'" "x \<in> X"
-      then obtain n where "X = from_nat_into B' n"
-        by (metis `countable B'` from_nat_into_surj)
-      also have "\<dots> \<subseteq> S n" by (auto simp: S_def)
-      finally show "x \<in> (\<Union>j. S j)" using `x \<in> X` by auto
-    next
-      fix x n
-      assume "x \<in> S n"
-      also have "\<dots> = (\<Union>i\<in>{0..n}. from_nat_into B' i)"
-        by (simp add: S_def)
-      also have "\<dots> \<subseteq> (\<Union>i. from_nat_into B' i)" by auto
-      also have "\<dots> \<subseteq> \<Union>B'" using `B' \<noteq> {}` by (auto intro: from_nat_into)
-      finally show "x \<in> \<Union>B'" .
-    qed
-    moreover have "range S \<subseteq> union_closed_basis" using B'
-      by (auto intro!: union_closed_basisI[OF _ S] simp: from_nat_into `B' \<noteq> {}`)
-    ultimately show ?thesis by auto
-  qed (auto simp: B')
-qed
-
-lemma open_incseqE:
-  assumes "open X"
-  obtains S where "incseq S" "(\<Union>j. S j) = X" "range S \<subseteq> union_closed_basis"
-  using open_imp_Union_of_incseq assms by atomize_elim
-
 end
 
 class first_countable_topology = topological_space +
@@ -304,6 +211,31 @@
   using first_countable_basis[of x]
   by atomize_elim auto
 
+lemma (in first_countable_topology) first_countable_basis_Int_stableE:
+  obtains A where "countable A" "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a"
+    "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)"
+    "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<inter> b \<in> A"
+proof atomize_elim
+  from first_countable_basisE[of x] guess A' . note A' = this
+  def A \<equiv> "(\<lambda>N. \<Inter>((\<lambda>n. from_nat_into A' n) ` N)) ` (Collect finite::nat set set)"
+  thus "\<exists>A. countable A \<and> (\<forall>a. a \<in> A \<longrightarrow> x \<in> a) \<and> (\<forall>a. a \<in> A \<longrightarrow> open a) \<and>
+        (\<forall>S. open S \<longrightarrow> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)) \<and> (\<forall>a b. a \<in> A \<longrightarrow> b \<in> A \<longrightarrow> a \<inter> b \<in> A)"
+  proof (safe intro!: exI[where x=A])
+    show "countable A" unfolding A_def by (intro countable_image countable_Collect_finite)
+    fix a assume "a \<in> A"
+    thus "x \<in> a" "open a" using A'(4)[OF open_UNIV] by (auto simp: A_def intro: A' from_nat_into)
+  next
+    let ?int = "\<lambda>N. \<Inter>from_nat_into A' ` N"
+    fix a b assume "a \<in> A" "b \<in> A"
+    then obtain N M where "a = ?int N" "b = ?int M" "finite (N \<union> M)" by (auto simp: A_def)
+    thus "a \<inter> b \<in> A" by (auto simp: A_def intro!: image_eqI[where x="N \<union> M"])
+  next
+    fix S assume "open S" "x \<in> S" then obtain a where a: "a\<in>A'" "a \<subseteq> S" using A' by blast
+    thus "\<exists>a\<in>A. a \<subseteq> S" using a A'
+      by (intro bexI[where x=a]) (auto simp: A_def intro: image_eqI[where x="{to_nat_on A' a}"])
+  qed
+qed
+
 instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology
 proof
   fix x :: "'a \<times> 'b"
@@ -794,7 +726,7 @@
     finally show "y \<in> ball x e" by (auto simp: ball_def)
   qed (insert a b, auto simp: box_def)
 qed
- 
+
 lemma open_UNION_box:
   fixes M :: "'a\<Colon>euclidean_space set"
   assumes "open M" 
@@ -3704,7 +3636,7 @@
 
 text{* Cauchy-type criteria for uniform convergence. *}
 
-lemma uniformly_convergent_eq_cauchy: fixes s::"nat \<Rightarrow> 'b \<Rightarrow> 'a::heine_borel" shows
+lemma uniformly_convergent_eq_cauchy: fixes s::"nat \<Rightarrow> 'b \<Rightarrow> 'a::complete_space" shows
  "(\<exists>l. \<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x --> dist(s n x)(l x) < e) \<longleftrightarrow>
   (\<forall>e>0. \<exists>N. \<forall>m n x. N \<le> m \<and> N \<le> n \<and> P x  --> dist (s m x) (s n x) < e)" (is "?lhs = ?rhs")
 proof(rule)
@@ -3738,7 +3670,7 @@
 qed
 
 lemma uniformly_cauchy_imp_uniformly_convergent:
-  fixes s :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::heine_borel"
+  fixes s :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::complete_space"
   assumes "\<forall>e>0.\<exists>N. \<forall>m (n::nat) x. N \<le> m \<and> N \<le> n \<and> P x --> dist(s m x)(s n x) < e"
           "\<forall>x. P x --> (\<forall>e>0. \<exists>N. \<forall>n. N \<le> n --> dist(s n x)(l x) < e)"
   shows "\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x --> dist(s n x)(l x) < e"
@@ -5796,7 +5728,7 @@
   show "\<exists>B::'a set set. countable B \<and> topological_basis B" unfolding topological_basis_def by blast
 qed
 
-instance ordered_euclidean_space \<subseteq> polish_space ..
+instance euclidean_space \<subseteq> polish_space ..
 
 text {* Intervals in general, including infinite and mixtures of open and closed. *}
 
diff -r 66d0298fc554 -r fa66ed645b7f src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Wed Feb 13 16:30:34 2013 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Wed Feb 13 17:41:27 2013 +0100
@@ -149,10 +149,6 @@
   thus "b \<in> sigma_sets UNIV (Collect open)" by auto
 qed simp_all
 
-lemma borel_eq_union_closed_basis:
-  "borel = sigma UNIV union_closed_basis"
-  by (rule borel_eq_countable_basis[OF countable_union_closed_basis basis_union_closed_basis])
-
 lemma borel_measurable_Pair[measurable (raw)]:
   fixes f :: "'a \<Rightarrow> 'b::second_countable_topology" and g :: "'a \<Rightarrow> 'c::second_countable_topology"
   assumes f[measurable]: "f \<in> borel_measurable M"
diff -r 66d0298fc554 -r fa66ed645b7f src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Wed Feb 13 16:30:34 2013 +0100
+++ b/src/HOL/Probability/Fin_Map.thy	Wed Feb 13 17:41:27 2013 +0100
@@ -76,9 +76,8 @@
 
 lemma finmap_of_eq_iff[simp]:
   assumes "finite i" "finite j"
-  shows "finmap_of i m = finmap_of j n \<longleftrightarrow> i = j \<and> restrict m i = restrict n i"
-  using assms
-  apply (auto simp: finmap_eq_iff restrict_def) by metis
+  shows "finmap_of i m = finmap_of j n \<longleftrightarrow> i = j \<and> (\<forall>k\<in>i. m k= n k)"
+  using assms by (auto simp: finmap_eq_iff)
 
 lemma finmap_of_inj_on_extensional_finite:
   assumes "finite K"
@@ -94,17 +93,6 @@
   show "x = y" using assms by (simp add: extensional_restrict)
 qed
 
-lemma finmap_choice:
-  assumes *: "\<And>i. i \<in> I \<Longrightarrow> \<exists>x. P i x" and I: "finite I"
-  shows "\<exists>fm. domain fm = I \<and> (\<forall>i\<in>I. P i (fm i))"
-proof -
-  have "\<exists>f. \<forall>i\<in>I. P i (f i)"
-    unfolding bchoice_iff[symmetric] using * by auto
-  then guess f ..
-  with I show ?thesis
-    by (intro exI[of _ "finmap_of I f"]) auto
-qed
-
 subsection {* Product set of Finite Maps *}
 
 text {* This is @{term Pi} for Finite Maps, most of this is copied *}
@@ -163,128 +151,19 @@
   apply auto
   done
 
-subsection {* Metric Space of Finite Maps *}
-
-instantiation finmap :: (type, metric_space) metric_space
-begin
+subsection {* Topological Space of Finite Maps *}
 
-definition dist_finmap where
-  "dist P Q = (\<Sum>i\<in>domain P \<union> domain Q. dist ((P)\<^isub>F i) ((Q)\<^isub>F i)) +
-    card ((domain P - domain Q) \<union> (domain Q - domain P))"
-
-lemma dist_finmap_extend:
-  assumes "finite X"
-  shows "dist P Q = (\<Sum>i\<in>domain P \<union> domain Q \<union> X. dist ((P)\<^isub>F i) ((Q)\<^isub>F i)) +
-    card ((domain P - domain Q) \<union> (domain Q - domain P))"
-    unfolding dist_finmap_def add_right_cancel
-    using assms extensional_arb[of "(P)\<^isub>F"] extensional_arb[of "(Q)\<^isub>F" "domain Q"]
-    by (intro setsum_mono_zero_cong_left) auto
+instantiation finmap :: (type, topological_space) topological_space
+begin
 
 definition open_finmap :: "('a \<Rightarrow>\<^isub>F 'b) set \<Rightarrow> bool" where
-  "open_finmap S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
-
-lemma add_eq_zero_iff[simp]:
-  fixes a b::real
-  assumes "a \<ge> 0" "b \<ge> 0"
-  shows "a + b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
-using assms by auto
-
-lemma dist_le_1_imp_domain_eq:
-  assumes "dist P Q < 1"
-  shows "domain P = domain Q"
-proof -
-  have "0 \<le> (\<Sum>i\<in>domain P \<union> domain Q. dist (P i) (Q i))"
-    by (simp add: setsum_nonneg)
-  with assms have "card (domain P - domain Q \<union> (domain Q - domain P)) = 0"
-    unfolding dist_finmap_def by arith
-  thus "domain P = domain Q" by auto
-qed
-
-lemma dist_proj:
-  shows "dist ((x)\<^isub>F i) ((y)\<^isub>F i) \<le> dist x y"
-proof -
-  have "dist (x i) (y i) = (\<Sum>i\<in>{i}. dist (x i) (y i))" by simp
-  also have "\<dots> \<le> (\<Sum>i\<in>domain x \<union> domain y \<union> {i}. dist (x i) (y i))"
-    by (intro setsum_mono2) auto
-  also have "\<dots> \<le> dist x y" by (simp add: dist_finmap_extend[of "{i}"])
-  finally show ?thesis by simp
-qed
+  "open_finmap = generate_topology {Pi' a b|a b. \<forall>i\<in>a. open (b i)}"
 
-lemma open_Pi'I:
-  assumes open_component: "\<And>i. i \<in> I \<Longrightarrow> open (A i)"
-  shows "open (Pi' I A)"
-proof (subst open_finmap_def, safe)
-  fix x assume x: "x \<in> Pi' I A"
-  hence dim_x: "domain x = I" by (simp add: Pi'_def)
-  hence [simp]: "finite I" unfolding dim_x[symmetric] by simp
-  have "\<exists>ei. \<forall>i\<in>I. 0 < ei i \<and> (\<forall>y. dist y (x i) < ei i \<longrightarrow> y \<in> A i)"
-  proof (safe intro!: bchoice)
-    fix i assume i: "i \<in> I"
-    moreover with open_component have "open (A i)" by simp
-    moreover have "x i \<in> A i" using x i
-      by (auto simp: proj_def)
-    ultimately show "\<exists>e>0. \<forall>y. dist y (x i) < e \<longrightarrow> y \<in> A i"
-      using x by (auto simp: open_dist Ball_def)
-  qed
-  then guess ei .. note ei = this
-  def es \<equiv> "ei ` I"
-  def e \<equiv> "if es = {} then 0.5 else min 0.5 (Min es)"
-  from ei have "e > 0" using x
-    by (auto simp add: e_def es_def Pi'_def Ball_def)
-  moreover have "\<forall>y. dist y x < e \<longrightarrow> y \<in> Pi' I A"
-  proof (intro allI impI)
-    fix y
-    assume "dist y x < e"
-    also have "\<dots> < 1" by (auto simp: e_def)
-    finally have "domain y = domain x" by (rule dist_le_1_imp_domain_eq)
-    with dim_x have dims: "domain y = domain x" "domain x = I" by auto
-    show "y \<in> Pi' I A"
-    proof
-      show "domain y = I" using dims by simp
-    next
-      fix i
-      assume "i \<in> I"
-      have "dist (y i) (x i) \<le> dist y x" using dims `i \<in> I`
-        by (auto intro: dist_proj)
-      also have "\<dots> < e" using `dist y x < e` dims
-        by (simp add: dist_finmap_def)
-      also have "e \<le> Min (ei ` I)" using dims `i \<in> I`
-        by (auto simp: e_def es_def)
-      also have "\<dots> \<le> ei i" using `i \<in> I` by (simp add: e_def)
-      finally have "dist (y i) (x i) < ei i" .
-      with ei `i \<in> I` show "y i \<in> A  i" by simp
-    qed
-  qed
-  ultimately
-  show "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> Pi' I A" by blast
-qed
+lemma open_Pi'I: "(\<And>i. i \<in> I \<Longrightarrow> open (A i)) \<Longrightarrow> open (Pi' I A)"
+  by (auto intro: generate_topology.Basis simp: open_finmap_def)
 
-instance
-proof
-  fix S::"('a \<Rightarrow>\<^isub>F 'b) set"
-  show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
-    unfolding open_finmap_def ..
-next
-  fix P Q::"'a \<Rightarrow>\<^isub>F 'b"
-  show "dist P Q = 0 \<longleftrightarrow> P = Q"
-    by (auto simp: finmap_eq_iff dist_finmap_def setsum_nonneg setsum_nonneg_eq_0_iff)
-next
-  fix P Q R::"'a \<Rightarrow>\<^isub>F 'b"
-  let ?symdiff = "\<lambda>a b. domain a - domain b \<union> (domain b - domain a)"
-  def E \<equiv> "domain P \<union> domain Q \<union> domain R"
-  hence "finite E" by (simp add: E_def)
-  have "card (?symdiff P Q) \<le> card (?symdiff P R \<union> ?symdiff Q R)"
-    by (auto intro: card_mono)
-  also have "\<dots> \<le> card (?symdiff P R) + card (?symdiff Q R)"
-    by (subst card_Un_Int) auto
-  finally have "dist P Q \<le> (\<Sum>i\<in>E. dist (P i) (R i) + dist (Q i) (R i)) +
-    real (card (?symdiff P R) + card (?symdiff Q R))"
-    unfolding dist_finmap_extend[OF `finite E`]
-    by (intro add_mono) (auto simp: E_def intro: setsum_mono dist_triangle_le)
-  also have "\<dots> \<le> dist P R + dist Q R"
-    unfolding dist_finmap_extend[OF `finite E`] by (simp add: ac_simps E_def setsum_addf[symmetric])
-  finally show "dist P Q \<le> dist P R + dist Q R" by simp
-qed
+instance using topological_space_generate_topology
+  by intro_classes (auto simp: open_finmap_def class.topological_space_def)
 
 end
 
@@ -310,69 +189,268 @@
 
 lemma closed_restricted_space:
   shows "closed {m. P (domain m)}"
-proof -
-  have "{m. P (domain m)} = - (\<Union>i \<in> - Collect P. {m. domain m = i})" by auto
-  also have "closed \<dots>"
-  proof (rule, rule, rule, cases)
-    fix i::"'a set"
-    assume "finite i"
-    hence "{m. domain m = i} = Pi' i (\<lambda>_. UNIV)" by (auto simp: Pi'_def)
-    also have "open \<dots>" by (auto intro: open_Pi'I simp: `finite i`)
-    finally show "open {m. domain m = i}" .
-  next
-    fix i::"'a set"
-    assume "\<not> finite i" hence "{m. domain m = i} = {}" by auto
-    also have "open \<dots>" by simp
-    finally show "open {m. domain m = i}" .
-  qed
-  finally show ?thesis .
+  using open_restricted_space[of "\<lambda>x. \<not> P x"]
+  unfolding closed_def by (rule back_subst) auto
+
+lemma tendsto_proj: "((\<lambda>x. x) ---> a) F \<Longrightarrow> ((\<lambda>x. (x)\<^isub>F i) ---> (a)\<^isub>F i) F"
+  unfolding tendsto_def
+proof safe
+  fix S::"'b set"
+  let ?S = "Pi' (domain a) (\<lambda>x. if x = i then S else UNIV)"
+  assume "open S" hence "open ?S" by (auto intro!: open_Pi'I)
+  moreover assume "\<forall>S. open S \<longrightarrow> a \<in> S \<longrightarrow> eventually (\<lambda>x. x \<in> S) F" "a i \<in> S"
+  ultimately have "eventually (\<lambda>x. x \<in> ?S) F" by auto
+  thus "eventually (\<lambda>x. (x)\<^isub>F i \<in> S) F"
+    by eventually_elim (insert `a i \<in> S`, force simp: Pi'_iff split: split_if_asm)
 qed
 
 lemma continuous_proj:
   shows "continuous_on s (\<lambda>x. (x)\<^isub>F i)"
-  unfolding continuous_on_topological
-proof safe
-  fix x B assume "x \<in> s" "open B" "x i \<in> B"
-  let ?A = "Pi' (domain x) (\<lambda>j. if i = j then B else UNIV)"
-  have "open ?A" using `open B` by (auto intro: open_Pi'I)
-  moreover have "x \<in> ?A" using `x i \<in> B` by auto
-  moreover have "(\<forall>y\<in>s. y \<in> ?A \<longrightarrow> y i \<in> B)"
-  proof (cases, safe)
-    fix y assume "y \<in> s"
-    assume "i \<notin> domain x" hence "undefined \<in> B" using `x i \<in> B`
-      by simp
-    moreover
-    assume "y \<in> ?A" hence "domain y = domain x" by (simp add: Pi'_def)
-    hence "y i = undefined" using `i \<notin> domain x` by simp
-    ultimately
-    show "y i \<in> B" by simp
-  qed force
-  ultimately
-  show "\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> y i \<in> B)" by blast
+  unfolding continuous_on_def
+  by (safe intro!: tendsto_proj tendsto_ident_at_within)
+
+instance finmap :: (type, first_countable_topology) first_countable_topology
+proof
+  fix x::"'a\<Rightarrow>\<^isub>F'b"
+  have "\<forall>i. \<exists>A. countable A \<and> (\<forall>a\<in>A. x i \<in> a) \<and> (\<forall>a\<in>A. open a) \<and>
+    (\<forall>S. open S \<and> x i \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)) \<and> (\<forall>a b. a \<in> A \<longrightarrow> b \<in> A \<longrightarrow> a \<inter> b \<in> A)" (is "\<forall>i. ?th i")
+  proof
+    fix i from first_countable_basis_Int_stableE[of "x i"] guess A .
+    thus "?th i" by (intro exI[where x=A]) simp
+  qed
+  then guess A unfolding choice_iff .. note A = this
+  hence open_sub: "\<And>i S. i\<in>domain x \<Longrightarrow> open (S i) \<Longrightarrow> x i\<in>(S i) \<Longrightarrow> (\<exists>a\<in>A i. a\<subseteq>(S i))" by auto
+  have A_notempty: "\<And>i. i \<in> domain x \<Longrightarrow> A i \<noteq> {}" using open_sub[of _ "\<lambda>_. UNIV"] by auto
+  let ?A = "(\<lambda>f. Pi' (domain x) f) ` (Pi\<^isub>E (domain x) A)"
+  show "\<exists>A. countable A \<and> (\<forall>a\<in>A. x \<in> a \<and> open a) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S))"
+  proof (rule exI[where x="?A"], safe)
+    show "countable ?A" using A by (simp add: countable_PiE)
+  next
+    fix S::"('a \<Rightarrow>\<^isub>F 'b) set" assume "open S" "x \<in> S"
+    thus "\<exists>a\<in>?A. a \<subseteq> S" unfolding open_finmap_def
+    proof (induct rule: generate_topology.induct)
+      case UNIV thus ?case by (auto simp add: ex_in_conv PiE_eq_empty_iff A_notempty)
+    next
+      case (Int a b)
+      then obtain f g where
+        "f \<in> Pi\<^isub>E (domain x) A" "Pi' (domain x) f \<subseteq> a" "g \<in> Pi\<^isub>E (domain x) A" "Pi' (domain x) g \<subseteq> b"
+        by auto
+      thus ?case using A
+        by (auto simp: Pi'_iff PiE_iff extensional_def Int_stable_def
+            intro!: bexI[where x="\<lambda>i. f i \<inter> g i"])
+    next
+      case (UN B)
+      then obtain b where "x \<in> b" "b \<in> B" by auto
+      hence "\<exists>a\<in>?A. a \<subseteq> b" using UN by simp
+      thus ?case using `b \<in> B` by blast
+    next
+      case (Basis s)
+      then obtain a b where xs: "x\<in> Pi' a b" "s = Pi' a b" "\<And>i. i\<in>a \<Longrightarrow> open (b i)" by auto
+      have "\<forall>i. \<exists>a. (i \<in> domain x \<and> open (b i) \<and> (x)\<^isub>F i \<in> b i) \<longrightarrow> (a\<in>A i \<and> a \<subseteq> b i)"
+        using open_sub[of _ b] by auto
+      then obtain b'
+        where "\<And>i. i \<in> domain x \<Longrightarrow> open (b i) \<Longrightarrow> (x)\<^isub>F i \<in> b i \<Longrightarrow> (b' i \<in>A i \<and> b' i \<subseteq> b i)"
+          unfolding choice_iff by auto
+      with xs have "\<And>i. i \<in> a \<Longrightarrow> (b' i \<in>A i \<and> b' i \<subseteq> b i)" "Pi' a b' \<subseteq> Pi' a b"
+        by (auto simp: Pi'_iff intro!: Pi'_mono)
+      thus ?case using xs
+        by (intro bexI[where x="Pi' a b'"])
+          (auto simp: Pi'_iff intro!: image_eqI[where x="restrict b' (domain x)"])
+    qed
+  qed (insert A,auto simp: PiE_iff intro!: open_Pi'I)
+qed
+
+subsection {* Metric Space of Finite Maps *}
+
+instantiation finmap :: (type, metric_space) metric_space
+begin
+
+definition dist_finmap where
+  "dist P Q = Max (range (\<lambda>i. dist ((P)\<^isub>F i) ((Q)\<^isub>F i))) + (if domain P = domain Q then 0 else 1)"
+
+lemma add_eq_zero_iff[simp]:
+  fixes a b::real
+  assumes "a \<ge> 0" "b \<ge> 0"
+  shows "a + b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
+using assms by auto
+
+lemma finite_proj_image': "x \<notin> domain P \<Longrightarrow> finite ((P)\<^isub>F ` S)"
+  by (rule finite_subset[of _ "proj P ` (domain P \<inter> S \<union> {x})"]) auto
+
+lemma finite_proj_image: "finite ((P)\<^isub>F ` S)"
+ by (cases "\<exists>x. x \<notin> domain P") (auto intro: finite_proj_image' finite_subset[where B="domain P"])
+
+lemma finite_proj_diag: "finite ((\<lambda>i. d ((P)\<^isub>F i) ((Q)\<^isub>F i)) ` S)"
+proof -
+  have "(\<lambda>i. d ((P)\<^isub>F i) ((Q)\<^isub>F i)) ` S = (\<lambda>(i, j). d i j) ` ((\<lambda>i. ((P)\<^isub>F i, (Q)\<^isub>F i)) ` S)" by auto
+  moreover have "((\<lambda>i. ((P)\<^isub>F i, (Q)\<^isub>F i)) ` S) \<subseteq> (\<lambda>i. (P)\<^isub>F i) ` S \<times> (\<lambda>i. (Q)\<^isub>F i) ` S" by auto
+  moreover have "finite \<dots>" using finite_proj_image[of P S] finite_proj_image[of Q S]
+    by (intro finite_cartesian_product) simp_all
+  ultimately show ?thesis by (simp add: finite_subset)
+qed
+
+lemma dist_le_1_imp_domain_eq:
+  shows "dist P Q < 1 \<Longrightarrow> domain P = domain Q"
+  by (simp add: dist_finmap_def finite_proj_diag split: split_if_asm)
+
+lemma dist_proj:
+  shows "dist ((x)\<^isub>F i) ((y)\<^isub>F i) \<le> dist x y"
+proof -
+  have "dist (x i) (y i) \<le> Max (range (\<lambda>i. dist (x i) (y i)))"
+    by (simp add: Max_ge_iff finite_proj_diag)
+  also have "\<dots> \<le> dist x y" by (simp add: dist_finmap_def)
+  finally show ?thesis .
 qed
 
-subsection {* Complete Space of Finite Maps *}
+lemma dist_finmap_lessI:
+  assumes "domain P = domain Q"
+  assumes "0 < e"
+  assumes "\<And>i. i \<in> domain P \<Longrightarrow> dist (P i) (Q i) < e"
+  shows "dist P Q < e"
+proof -
+  have "dist P Q = Max (range (\<lambda>i. dist (P i) (Q i)))"
+    using assms by (simp add: dist_finmap_def finite_proj_diag)
+  also have "\<dots> < e"
+  proof (subst Max_less_iff, safe)
+    fix i
+    show "dist ((P)\<^isub>F i) ((Q)\<^isub>F i) < e" using assms
+      by (cases "i \<in> domain P") simp_all
+  qed (simp add: finite_proj_diag)
+  finally show ?thesis .
+qed
 
-lemma tendsto_dist_zero:
-  assumes "(\<lambda>i. dist (f i) g) ----> 0"
-  shows "f ----> g"
-  using assms by (auto simp: tendsto_iff dist_real_def)
+instance
+proof
+  fix S::"('a \<Rightarrow>\<^isub>F 'b) set"
+  show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" (is "_ = ?od")
+  proof
+    assume "open S"
+    thus ?od
+      unfolding open_finmap_def
+    proof (induct rule: generate_topology.induct)
+      case UNIV thus ?case by (auto intro: zero_less_one)
+    next
+      case (Int a b)
+      show ?case
+      proof safe
+        fix x assume x: "x \<in> a" "x \<in> b"
+        with Int x obtain e1 e2 where
+          "e1>0" "\<forall>y. dist y x < e1 \<longrightarrow> y \<in> a" "e2>0" "\<forall>y. dist y x < e2 \<longrightarrow> y \<in> b" by force
+        thus "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> a \<inter> b"
+          by (auto intro!: exI[where x="min e1 e2"])
+      qed
+    next
+      case (UN K)
+      show ?case
+      proof safe
+        fix x X assume "x \<in> X" "X \<in> K"
+        moreover with UN obtain e where "e>0" "\<And>y. dist y x < e \<longrightarrow> y \<in> X" by force
+        ultimately show "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> \<Union>K" by auto
+      qed
+    next
+      case (Basis s) then obtain a b where s: "s = Pi' a b" and b: "\<And>i. i\<in>a \<Longrightarrow> open (b i)" by auto
+      show ?case
+      proof safe
+        fix x assume "x \<in> s"
+        hence [simp]: "finite a" and a_dom: "a = domain x" using s by (auto simp: Pi'_iff)
+        obtain es where es: "\<forall>i \<in> a. es i > 0 \<and> (\<forall>y. dist y (proj x i) < es i \<longrightarrow> y \<in> b i)"
+          using b `x \<in> s` by atomize_elim (intro bchoice, auto simp: open_dist s)
+        hence in_b: "\<And>i y. i \<in> a \<Longrightarrow> dist y (proj x i) < es i \<Longrightarrow> y \<in> b i" by auto
+        show "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> s"
+        proof (cases, rule, safe)
+          assume "a \<noteq> {}"
+          show "0 < min 1 (Min (es ` a))" using es by (auto simp: `a \<noteq> {}`)
+          fix y assume d: "dist y x < min 1 (Min (es ` a))"
+          show "y \<in> s" unfolding s
+          proof
+            show "domain y = a" using d s `a \<noteq> {}` by (auto simp: dist_le_1_imp_domain_eq a_dom)
+            fix i assume "i \<in> a"
+            moreover
+            hence "dist ((y)\<^isub>F i) ((x)\<^isub>F i) < es i" using d
+              by (auto simp: dist_finmap_def `a \<noteq> {}` intro!: le_less_trans[OF dist_proj])
+            ultimately
+            show "y i \<in> b i" by (rule in_b)
+          qed
+        next
+          assume "\<not>a \<noteq> {}"
+          thus "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> s"
+            using s `x \<in> s` by (auto simp: Pi'_def dist_le_1_imp_domain_eq intro!: exI[where x=1])
+        qed
+      qed
+    qed
+  next
+    assume "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S"
+    then obtain e where e_pos: "\<And>x. x \<in> S \<Longrightarrow> e x > 0" and
+      e_in:  "\<And>x y . x \<in> S \<Longrightarrow> dist y x < e x \<Longrightarrow> y \<in> S"
+      unfolding bchoice_iff
+      by auto
+    have S_eq: "S = \<Union>{Pi' a b| a b. \<exists>x\<in>S. domain x = a \<and> b = (\<lambda>i. ball (x i) (e x))}"
+    proof safe
+      fix x assume "x \<in> S"
+      thus "x \<in> \<Union>{Pi' a b| a b. \<exists>x\<in>S. domain x = a \<and> b = (\<lambda>i. ball (x i) (e x))}"
+        using e_pos by (auto intro!: exI[where x="Pi' (domain x) (\<lambda>i. ball (x i) (e x))"])
+    next
+      fix x y
+      assume "y \<in> S"
+      moreover
+      assume "x \<in> (\<Pi>' i\<in>domain y. ball (y i) (e y))"
+      hence "dist x y < e y" using e_pos `y \<in> S`
+        by (auto simp: dist_finmap_def Pi'_iff finite_proj_diag dist_commute)
+      ultimately show "x \<in> S" by (rule e_in)
+    qed
+    also have "open \<dots>"
+      unfolding open_finmap_def
+      by (intro generate_topology.UN) (auto intro: generate_topology.Basis)
+    finally show "open S" .
+  qed
+next
+  fix P Q::"'a \<Rightarrow>\<^isub>F 'b"
+  have Max_eq_iff: "\<And>A m. finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> (Max A = m) = (m \<in> A \<and> (\<forall>a\<in>A. a \<le> m))"
+    by (metis Max.in_idem Max_in max_def min_max.sup.commute order_refl)
+  show "dist P Q = 0 \<longleftrightarrow> P = Q"
+    by (auto simp: finmap_eq_iff dist_finmap_def Max_ge_iff finite_proj_diag Max_eq_iff
+      intro!: Max_eqI image_eqI[where x=undefined])
+next
+  fix P Q R::"'a \<Rightarrow>\<^isub>F 'b"
+  let ?dists = "\<lambda>P Q i. dist ((P)\<^isub>F i) ((Q)\<^isub>F i)"
+  let ?dpq = "?dists P Q" and ?dpr = "?dists P R" and ?dqr = "?dists Q R"
+  let ?dom = "\<lambda>P Q. (if domain P = domain Q then 0 else 1::real)"
+  have "dist P Q = Max (range ?dpq) + ?dom P Q"
+    by (simp add: dist_finmap_def)
+  also obtain t where "t \<in> range ?dpq" "t = Max (range ?dpq)" by (simp add: finite_proj_diag)
+  then obtain i where "Max (range ?dpq) = ?dpq i" by auto
+  also have "?dpq i \<le> ?dpr i + ?dqr i" by (rule dist_triangle2)
+  also have "?dpr i \<le> Max (range ?dpr)" by (simp add: finite_proj_diag)
+  also have "?dqr i \<le> Max (range ?dqr)" by (simp add: finite_proj_diag)
+  also have "?dom P Q \<le> ?dom P R + ?dom Q R" by simp
+  finally show "dist P Q \<le> dist P R + dist Q R" by (simp add: dist_finmap_def ac_simps)
+qed
 
-lemma tendsto_dist_zero':
-  assumes "(\<lambda>i. dist (f i) g) ----> x"
-  assumes "0 = x"
-  shows "f ----> g"
-  using assms tendsto_dist_zero by simp
+end
+
+subsection {* Complete Space of Finite Maps *}
 
 lemma tendsto_finmap:
   fixes f::"nat \<Rightarrow> ('i \<Rightarrow>\<^isub>F ('a::metric_space))"
   assumes ind_f:  "\<And>n. domain (f n) = domain g"
   assumes proj_g:  "\<And>i. i \<in> domain g \<Longrightarrow> (\<lambda>n. (f n) i) ----> g i"
   shows "f ----> g"
-  apply (rule tendsto_dist_zero')
-  unfolding dist_finmap_def assms
-  apply (rule tendsto_intros proj_g | simp)+
-  done
+  unfolding tendsto_iff
+proof safe
+  fix e::real assume "0 < e"
+  let ?dists = "\<lambda>x i. dist ((f x)\<^isub>F i) ((g)\<^isub>F i)"
+  have "eventually (\<lambda>x. \<forall>i\<in>domain g. ?dists x i < e) sequentially"
+    using finite_domain[of g] proj_g
+  proof induct
+    case (insert i G)
+    with `0 < e` have "eventually (\<lambda>x. ?dists x i < e) sequentially" by (auto simp add: tendsto_iff)
+    moreover
+    from insert have "eventually (\<lambda>x. \<forall>i\<in>G. dist ((f x)\<^isub>F i) ((g)\<^isub>F i) < e) sequentially" by simp
+    ultimately show ?case by eventually_elim auto
+  qed simp
+  thus "eventually (\<lambda>x. dist (f x) g < e) sequentially"
+    by eventually_elim (auto simp add: dist_finmap_def finite_proj_diag ind_f `0 < e`)
+qed
 
 instance finmap :: (type, complete_space) complete_space
 proof
@@ -412,123 +490,114 @@
   have "P ----> Q"
   proof (rule metric_LIMSEQ_I)
     fix e::real assume "0 < e"
-    def e' \<equiv> "min 1 (e / (card d + 1))"
-    hence "0 < e'" using `0 < e` by (auto simp: e'_def intro: divide_pos_pos)
-    have "\<exists>ni. \<forall>i\<in>d. \<forall>n\<ge>ni i. dist (p i n) (q i) < e'"
+    have "\<exists>ni. \<forall>i\<in>d. \<forall>n\<ge>ni i. dist (p i n) (q i) < e"
     proof (safe intro!: bchoice)
       fix i assume "i \<in> d"
-      from p[OF `i \<in> d`, THEN metric_LIMSEQ_D, OF `0 < e'`]
-      show "\<exists>no. \<forall>n\<ge>no. dist (p i n) (q i) < e'" .
+      from p[OF `i \<in> d`, THEN metric_LIMSEQ_D, OF `0 < e`]
+      show "\<exists>no. \<forall>n\<ge>no. dist (p i n) (q i) < e" .
     qed then guess ni .. note ni = this
     def N \<equiv> "max Nd (Max (ni ` d))"
     show "\<exists>N. \<forall>n\<ge>N. dist (P n) Q < e"
     proof (safe intro!: exI[where x="N"])
       fix n assume "N \<le> n"
-      hence "domain (P n) = d" "domain Q = d" "domain (P n) = domain Q"
+      hence dom: "domain (P n) = d" "domain Q = d" "domain (P n) = domain Q"
         using dim by (simp_all add: N_def Q_def dim_def Abs_finmap_inverse)
-      hence "dist (P n) Q = (\<Sum>i\<in>d. dist ((P n) i) (Q i))" by (simp add: dist_finmap_def)
-      also have "\<dots> \<le> (\<Sum>i\<in>d. e')"
-      proof (intro setsum_mono less_imp_le)
-        fix i assume "i \<in> d"
-        hence "ni i \<le> Max (ni ` d)" by simp
+      show "dist (P n) Q < e"
+      proof (rule dist_finmap_lessI[OF dom(3) `0 < e`])
+        fix i
+        assume "i \<in> domain (P n)"
+        hence "ni i \<le> Max (ni ` d)" using dom by simp
         also have "\<dots> \<le> N" by (simp add: N_def)
-        also have "\<dots> \<le> n" using `N \<le> n` .
-        finally
-        show "dist ((P n) i) (Q i) < e'"
-          using ni `i \<in> d` by (auto simp: p_def q N_def)
+        finally show "dist ((P n)\<^isub>F i) ((Q)\<^isub>F i) < e" using ni `i \<in> domain (P n)` `N \<le> n` dom
+          by (auto simp: p_def q N_def less_imp_le)
       qed
-      also have "\<dots> = card d * e'" by (simp add: real_eq_of_nat)
-      also have "\<dots> < e" using `0 < e` by (simp add: e'_def field_simps min_def)
-      finally show "dist (P n) Q < e" .
     qed
   qed
   thus "convergent P" by (auto simp: convergent_def)
 qed
 
-subsection {* Polish Space of Finite Maps *}
+subsection {* Second Countable Space of Finite Maps *}
 
-instantiation finmap :: (countable, polish_space) polish_space
+instantiation finmap :: (countable, second_countable_topology) second_countable_topology
 begin
 
+definition basis_proj::"'b set set"
+  where "basis_proj = (SOME B. countable B \<and> topological_basis B)"
+
+lemma countable_basis_proj: "countable basis_proj" and basis_proj: "topological_basis basis_proj"
+  unfolding basis_proj_def by (intro is_basis countable_basis)+
+
 definition basis_finmap::"('a \<Rightarrow>\<^isub>F 'b) set set"
-  where "basis_finmap = {Pi' I S|I S. finite I \<and> (\<forall>i \<in> I. S i \<in> union_closed_basis)}"
+  where "basis_finmap = {Pi' I S|I S. finite I \<and> (\<forall>i \<in> I. S i \<in> basis_proj)}"
 
 lemma in_basis_finmapI:
-  assumes "finite I" assumes "\<And>i. i \<in> I \<Longrightarrow> S i \<in> union_closed_basis"
+  assumes "finite I" assumes "\<And>i. i \<in> I \<Longrightarrow> S i \<in> basis_proj"
   shows "Pi' I S \<in> basis_finmap"
   using assms unfolding basis_finmap_def by auto
 
-lemma in_basis_finmapE:
-  assumes "x \<in> basis_finmap"
-  obtains I S where "x = Pi' I S" "finite I" "\<And>i. i \<in> I \<Longrightarrow> S i \<in> union_closed_basis"
-  using assms unfolding basis_finmap_def by auto
-
 lemma basis_finmap_eq:
-  "basis_finmap = (\<lambda>f. Pi' (domain f) (\<lambda>i. from_nat_into union_closed_basis ((f)\<^isub>F i))) `
+  assumes "basis_proj \<noteq> {}"
+  shows "basis_finmap = (\<lambda>f. Pi' (domain f) (\<lambda>i. from_nat_into basis_proj ((f)\<^isub>F i))) `
     (UNIV::('a \<Rightarrow>\<^isub>F nat) set)" (is "_ = ?f ` _")
   unfolding basis_finmap_def
 proof safe
   fix I::"'a set" and S::"'a \<Rightarrow> 'b set"
-  assume "finite I" "\<forall>i\<in>I. S i \<in> union_closed_basis"
-  hence "Pi' I S = ?f (finmap_of I (\<lambda>x. to_nat_on union_closed_basis (S x)))"
-    by (force simp: Pi'_def countable_union_closed_basis)
+  assume "finite I" "\<forall>i\<in>I. S i \<in> basis_proj"
+  hence "Pi' I S = ?f (finmap_of I (\<lambda>x. to_nat_on basis_proj (S x)))"
+    by (force simp: Pi'_def countable_basis_proj)
   thus "Pi' I S \<in> range ?f" by simp
-qed (metis (mono_tags) empty_basisI equals0D finite_domain from_nat_into)
+next
+  fix x and f::"'a \<Rightarrow>\<^isub>F nat"
+  show "\<exists>I S. (\<Pi>' i\<in>domain f. from_nat_into local.basis_proj ((f)\<^isub>F i)) = Pi' I S \<and>
+    finite I \<and> (\<forall>i\<in>I. S i \<in> local.basis_proj)"
+    using assms by (auto intro: from_nat_into)
+qed
+
+lemma basis_finmap_eq_empty: "basis_proj = {} \<Longrightarrow> basis_finmap = {Pi' {} undefined}"
+  by (auto simp: Pi'_iff basis_finmap_def)
 
 lemma countable_basis_finmap: "countable basis_finmap"
-  unfolding basis_finmap_eq by simp
+  by (cases "basis_proj = {}") (auto simp: basis_finmap_eq basis_finmap_eq_empty)
 
 lemma finmap_topological_basis:
   "topological_basis basis_finmap"
 proof (subst topological_basis_iff, safe)
   fix B' assume "B' \<in> basis_finmap"
   thus "open B'"
-    by (auto intro!: open_Pi'I topological_basis_open[OF basis_union_closed_basis]
+    by (auto intro!: open_Pi'I topological_basis_open[OF basis_proj]
       simp: topological_basis_def basis_finmap_def Let_def)
 next
   fix O'::"('a \<Rightarrow>\<^isub>F 'b) set" and x
-  assume "open O'" "x \<in> O'"
-  then obtain e where e: "e > 0" "\<And>y. dist y x < e \<Longrightarrow> y \<in> O'"  unfolding open_dist by blast
-  def e' \<equiv> "e / (card (domain x) + 1)"
-
+  assume O': "open O'" "x \<in> O'"
+  then obtain a where a:
+    "x \<in> Pi' (domain x) a" "Pi' (domain x) a \<subseteq> O'" "\<And>i. i\<in>domain x \<Longrightarrow> open (a i)"
+    unfolding open_finmap_def
+  proof (atomize_elim, induct rule: generate_topology.induct)
+    case (Int a b)
+    let ?p="\<lambda>a f. x \<in> Pi' (domain x) f \<and> Pi' (domain x) f \<subseteq> a \<and> (\<forall>i. i \<in> domain x \<longrightarrow> open (f i))"
+    from Int obtain f g where "?p a f" "?p b g" by auto
+    thus ?case by (force intro!: exI[where x="\<lambda>i. f i \<inter> g i"] simp: Pi'_def)
+  next
+    case (UN k)
+    then obtain kk a where "x \<in> kk" "kk \<in> k" "x \<in> Pi' (domain x) a" "Pi' (domain x) a \<subseteq> kk"
+      "\<And>i. i\<in>domain x \<Longrightarrow> open (a i)"
+      by force
+    thus ?case by blast
+  qed (auto simp: Pi'_def)
   have "\<exists>B.
-    (\<forall>i\<in>domain x. x i \<in> B i \<and> B i \<subseteq> ball (x i) e' \<and> B i \<in> union_closed_basis)"
+    (\<forall>i\<in>domain x. x i \<in> B i \<and> B i \<subseteq> a i \<and> B i \<in> basis_proj)"
   proof (rule bchoice, safe)
     fix i assume "i \<in> domain x"
-    have "open (ball (x i) e')" "x i \<in> ball (x i) e'" using e
-      by (auto simp add: e'_def intro!: divide_pos_pos)
-    from topological_basisE[OF basis_union_closed_basis this] guess b' .
-    thus "\<exists>y. x i \<in> y \<and> y \<subseteq> ball (x i) e' \<and> y \<in> union_closed_basis" by auto
+    hence "open (a i)" "x i \<in> a i" using a by auto
+    from topological_basisE[OF basis_proj this] guess b' .
+    thus "\<exists>y. x i \<in> y \<and> y \<subseteq> a i \<and> y \<in> basis_proj" by auto
   qed
   then guess B .. note B = this
   def B' \<equiv> "Pi' (domain x) (\<lambda>i. (B i)::'b set)"
-  hence "B' \<in> basis_finmap" unfolding B'_def using B
-    by (intro in_basis_finmapI) auto
-  moreover have "x \<in> B'" unfolding B'_def using B by auto
-  moreover have "B' \<subseteq> O'"
-  proof
-    fix y assume "y \<in> B'" with B have "domain y = domain x" unfolding B'_def
-      by (simp add: Pi'_def)
-    show "y \<in> O'"
-    proof (rule e)
-      have "dist y x = (\<Sum>i \<in> domain x. dist (y i) (x i))"
-        using `domain y = domain x` by (simp add: dist_finmap_def)
-      also have "\<dots> \<le> (\<Sum>i \<in> domain x. e')"
-      proof (rule setsum_mono)
-        fix i assume "i \<in> domain x"
-        with `y \<in> B'` B have "y i \<in> B i"
-          by (simp add: Pi'_def B'_def)
-        hence "y i \<in> ball (x i) e'" using B `domain y = domain x` `i \<in> domain x`
-          by force
-        thus "dist (y i) (x i) \<le> e'" by (simp add: dist_commute)
-      qed
-      also have "\<dots> = card (domain x) * e'" by (simp add: real_eq_of_nat)
-      also have "\<dots> < e" using e by (simp add: e'_def field_simps)
-      finally show "dist y x < e" .
-    qed
-  qed
-  ultimately
-  show "\<exists>B'\<in>basis_finmap. x \<in> B' \<and> B' \<subseteq> O'" by blast
+  have "B' \<subseteq> Pi' (domain x) a" using B by (auto intro!: Pi'_mono simp: B'_def)
+  also note `\<dots> \<subseteq> O'`
+  finally show "\<exists>B'\<in>basis_finmap. x \<in> B' \<and> B' \<subseteq> O'" using B
+    by (auto intro!: bexI[where x=B'] Pi'_mono in_basis_finmapI simp: B'_def)
 qed
 
 lemma range_enum_basis_finmap_imp_open:
@@ -540,6 +609,11 @@
 
 end
 
+subsection {* Polish Space of Finite Maps *}
+
+instance finmap :: (countable, polish_space) polish_space proof qed
+
+
 subsection {* Product Measurable Space of Finite Maps *}
 
 definition "PiF I M \<equiv>
@@ -942,9 +1016,8 @@
 text {* adapted from @{thm sigma_prod_algebra_sigma_eq} *}
 
 lemma sigma_fprod_algebra_sigma_eq:
-  fixes E :: "'i \<Rightarrow> 'a set set"
+  fixes E :: "'i \<Rightarrow> 'a set set" and S :: "'i \<Rightarrow> nat \<Rightarrow> 'a set"
   assumes [simp]: "finite I" "I \<noteq> {}"
-  assumes S_mono: "\<And>i. i \<in> I \<Longrightarrow> incseq (S i)"
     and S_union: "\<And>i. i \<in> I \<Longrightarrow> (\<Union>j. S i j) = space (M i)"
     and S_in_E: "\<And>i. i \<in> I \<Longrightarrow> range (S i) \<subseteq> E i"
   assumes E_closed: "\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> Pow (space (M i))"
@@ -953,6 +1026,9 @@
   shows "sets (PiF {I} M) = sigma_sets (space (PiF {I} M)) P"
 proof
   let ?P = "sigma (space (Pi\<^isub>F {I} M)) P"
+  from `finite I`[THEN ex_bij_betw_finite_nat] guess T ..
+  then have T: "\<And>i. i \<in> I \<Longrightarrow> T i < card I" "\<And>i. i\<in>I \<Longrightarrow> the_inv_into I T (T i) = i"
+    by (auto simp add: bij_betw_def set_eq_iff image_iff the_inv_into_f_f simp del: `finite I`)
   have P_closed: "P \<subseteq> Pow (space (Pi\<^isub>F {I} M))"
     using E_closed by (auto simp: space_PiF P_def Pi'_iff subset_eq)
   then have space_P: "space ?P = (\<Pi>' i\<in>I. space (M i))"
@@ -975,15 +1051,20 @@
           using E_closed `i \<in> I` by (auto simp: space_P Pi_iff subset_eq split: split_if_asm)
         also have "\<dots> = (\<Pi>' j\<in>I. \<Union>n. if i = j then A else S j n)"
           by (intro Pi'_cong) (simp_all add: S_union)
-        also have "\<dots> = (\<Union>n. \<Pi>' j\<in>I. if i = j then A else S j n)"
-          using S_mono
-          by (subst Pi'_UN[symmetric, OF `finite I`]) (auto simp: incseq_def)
+        also have "\<dots> = (\<Union>xs\<in>{xs. length xs = card I}. \<Pi>' j\<in>I. if i = j then A else S j (xs ! T j))"
+          using T
+          apply auto
+          apply (simp_all add: Pi'_iff bchoice_iff)
+          apply (erule conjE exE)+
+          apply (rule_tac x="map (\<lambda>n. f (the_inv_into I T n)) [0..<card I]" in exI)
+          apply (auto simp: bij_betw_def)
+          done
         also have "\<dots> \<in> sets ?P"
         proof (safe intro!: sets.countable_UN)
-          fix n show "(\<Pi>' j\<in>I. if i = j then A else S j n) \<in> sets ?P"
+          fix xs show "(\<Pi>' j\<in>I. if i = j then A else S j (xs ! T j)) \<in> sets ?P"
             using A S_in_E
             by (simp add: P_closed)
-               (auto simp: P_def subset_eq intro!: exI[of _ "\<lambda>j. if i = j then A else S j n"])
+               (auto simp: P_def subset_eq intro!: exI[of _ "\<lambda>j. if i = j then A else S j (xs ! T j)"])
         qed
         finally show "(\<lambda>x. (x)\<^isub>F i) -` A \<inter> space ?P \<in> sets ?P"
           using P_closed by simp
@@ -1003,76 +1084,28 @@
     by (auto intro!: sets.sigma_sets_subset product_in_sets_PiFI simp: E_generates P_def)
 qed
 
-lemma sets_PiF_eq_sigma_union_closed_basis_single:
-  assumes "I \<noteq> {}"
-  assumes [simp]: "finite I"
-  shows "sets (PiF {I} (\<lambda>_. borel)) = sigma_sets (space (PiF {I} (\<lambda>_. borel)))
-    {Pi' I F |F. (\<forall>i\<in>I. F i \<in> union_closed_basis)}"
-proof -
-  from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'b set" . note S = this
-  show ?thesis
-  proof (rule sigma_fprod_algebra_sigma_eq)
-    show "finite I" by simp
-    show "I \<noteq> {}" by fact
-    show "incseq S" "(\<Union>j. S j) = space borel" "range S \<subseteq> union_closed_basis"
-      using S by simp_all
-    show "union_closed_basis \<subseteq> Pow (space borel)" by simp
-    show "sets borel = sigma_sets (space borel) union_closed_basis"
-      by (simp add: borel_eq_union_closed_basis)
-  qed
-qed
-
-text {* adapted from @{thm sets_PiF_eq_sigma_union_closed_basis_single} *}
-
-lemma sets_PiM_eq_sigma_union_closed_basis:
-  assumes "I \<noteq> {}"
-  assumes [simp]: "finite I"
-  shows "sets (PiM I (\<lambda>_. borel)) = sigma_sets (space (PiM I (\<lambda>_. borel)))
-    {Pi\<^isub>E I F |F. \<forall>i\<in>I. F i \<in> union_closed_basis}"
-proof -
-  from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'b set" . note S = this
-  show ?thesis
-  proof (rule sigma_prod_algebra_sigma_eq)
-    show "finite I" by simp note[[show_types]]
-    fix i show "(\<Union>j. S j) = space borel" "range S \<subseteq> union_closed_basis"
-      using S by simp_all
-    show "union_closed_basis \<subseteq> Pow (space borel)" by simp
-    show "sets borel = sigma_sets (space borel) union_closed_basis"
-      by (simp add: borel_eq_union_closed_basis)
-  qed
-qed
-
 lemma product_open_generates_sets_PiF_single:
   assumes "I \<noteq> {}"
   assumes [simp]: "finite I"
   shows "sets (PiF {I} (\<lambda>_. borel::'b::second_countable_topology measure)) =
     sigma_sets (space (PiF {I} (\<lambda>_. borel))) {Pi' I F |F. (\<forall>i\<in>I. F i \<in> Collect open)}"
 proof -
-  from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'b set" . note S = this
+  from open_countable_basisE[OF open_UNIV] guess S::"'b set set" . note S = this
   show ?thesis
   proof (rule sigma_fprod_algebra_sigma_eq)
     show "finite I" by simp
     show "I \<noteq> {}" by fact
-    show "incseq S" "(\<Union>j. S j) = space borel" "range S \<subseteq> Collect open"
-      using S by (auto simp: open_union_closed_basis)
-    show "Collect open \<subseteq> Pow (space borel)" by simp
-    show "sets borel = sigma_sets (space borel) (Collect open)"
-      by (simp add: borel_def)
-  qed
-qed
-
-lemma product_open_generates_sets_PiM:
-  assumes "I \<noteq> {}"
-  assumes [simp]: "finite I"
-  shows "sets (PiM I (\<lambda>_. borel::'b::second_countable_topology measure)) =
-    sigma_sets (space (PiM I (\<lambda>_. borel))) {Pi\<^isub>E I F |F. \<forall>i\<in>I. F i \<in> Collect open}"
-proof -
-  from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'b set" . note S = this
-  show ?thesis
-  proof (rule sigma_prod_algebra_sigma_eq)
-    show "finite I" by simp note[[show_types]]
-    fix i show "(\<Union>j. S j) = space borel" "range S \<subseteq> Collect open"
-      using S by (auto simp: open_union_closed_basis)
+    def S'\<equiv>"from_nat_into S"
+    show "(\<Union>j. S' j) = space borel"
+      using S
+      apply (auto simp add: from_nat_into countable_basis_proj S'_def basis_proj_def)
+      apply (metis (lifting, mono_tags) UNIV_I UnionE basis_proj_def countable_basis_proj countable_subset from_nat_into_surj)
+      done
+    show "range S' \<subseteq> Collect open"
+      using S
+      apply (auto simp add: from_nat_into countable_basis_proj S'_def)
+      apply (metis UNIV_not_empty Union_empty from_nat_into set_mp topological_basis_open[OF basis_proj] basis_proj_def)
+      done
     show "Collect open \<subseteq> Pow (space borel)" by simp
     show "sets borel = sigma_sets (space borel) (Collect open)"
       by (simp add: borel_def)
@@ -1099,7 +1132,7 @@
     proof
       fix x assume "x \<in> B'" with B' have "x \<in> basis_finmap" by auto
       then obtain J X where "x = Pi' J X" "finite J" "X \<in> J \<rightarrow> sigma_sets UNIV (Collect open)"
-        by (auto simp: basis_finmap_def open_union_closed_basis)
+        by (auto simp: basis_finmap_def topological_basis_open[OF basis_proj])
       thus "x \<in> sets ?s" by auto
     qed
   qed