# HG changeset patch
# User hoelzl
# Date 1358181036 -3600
# Node ID a382bf90867e4268064591487ce9f1289b96f866
# Parent  ae630bab13dae6ab71cf510e46b44346a11c9374
move prod instantiation of second_countable_topology to its definition

diff -r ae630bab13da -r a382bf90867e src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jan 14 17:29:04 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jan 14 17:30:36 2013 +0100
@@ -93,6 +93,25 @@
 
 end
 
+lemma topological_basis_prod:
+  assumes A: "topological_basis A" and B: "topological_basis B"
+  shows "topological_basis ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))"
+  unfolding topological_basis_def
+proof (safe, simp_all del: ex_simps add: subset_image_iff ex_simps(1)[symmetric])
+  fix S :: "('a \<times> 'b) set" assume "open S"
+  then show "\<exists>X\<subseteq>A \<times> B. (\<Union>(a,b)\<in>X. a \<times> b) = S"
+  proof (safe intro!: exI[of _ "{x\<in>A \<times> B. fst x \<times> snd x \<subseteq> S}"])
+    fix x y assume "(x, y) \<in> S"
+    from open_prod_elim[OF `open S` this]
+    obtain a b where a: "open a""x \<in> a" and b: "open b" "y \<in> b" and "a \<times> b \<subseteq> S"
+      by (metis mem_Sigma_iff)
+    moreover from topological_basisE[OF A a] guess A0 .
+    moreover from topological_basisE[OF B b] guess B0 .
+    ultimately show "(x, y) \<in> (\<Union>(a, b)\<in>{X \<in> A \<times> B. fst X \<times> snd X \<subseteq> S}. a \<times> b)"
+      by (intro UN_I[of "(A0, B0)"]) auto
+  qed auto
+qed (metis A B topological_basis_open open_Times)
+
 subsection {* Countable Basis *}
 
 locale countable_basis =
@@ -227,6 +246,17 @@
 sublocale second_countable_topology < countable_basis "SOME B. countable B \<and> topological_basis B"
   using someI_ex[OF ex_countable_basis] by unfold_locales safe
 
+instance prod :: (second_countable_topology, second_countable_topology) second_countable_topology
+proof
+  obtain A :: "'a set set" where "countable A" "topological_basis A"
+    using ex_countable_basis by auto
+  moreover
+  obtain B :: "'b set set" where "countable B" "topological_basis B"
+    using ex_countable_basis by auto
+  ultimately show "\<exists>B::('a \<times> 'b) set set. countable B \<and> topological_basis B"
+    by (auto intro!: exI[of _ "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"] topological_basis_prod)
+qed
+
 subsection {* Polish spaces *}
 
 text {* Textbooks define Polish spaces as completely metrizable.
diff -r ae630bab13da -r a382bf90867e src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Mon Jan 14 17:29:04 2013 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Mon Jan 14 17:30:36 2013 +0100
@@ -153,36 +153,6 @@
   "borel = sigma UNIV union_closed_basis"
   by (rule borel_eq_countable_basis[OF countable_union_closed_basis basis_union_closed_basis])
 
-lemma topological_basis_prod:
-  assumes A: "topological_basis A" and B: "topological_basis B"
-  shows "topological_basis ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))"
-  unfolding topological_basis_def
-proof (safe, simp_all del: ex_simps add: subset_image_iff ex_simps(1)[symmetric])
-  fix S :: "('a \<times> 'b) set" assume "open S"
-  then show "\<exists>X\<subseteq>A \<times> B. (\<Union>(a,b)\<in>X. a \<times> b) = S"
-  proof (safe intro!: exI[of _ "{x\<in>A \<times> B. fst x \<times> snd x \<subseteq> S}"])
-    fix x y assume "(x, y) \<in> S"
-    from open_prod_elim[OF `open S` this]
-    obtain a b where a: "open a""x \<in> a" and b: "open b" "y \<in> b" and "a \<times> b \<subseteq> S"
-      by (metis mem_Sigma_iff)
-    moreover from topological_basisE[OF A a] guess A0 .
-    moreover from topological_basisE[OF B b] guess B0 .
-    ultimately show "(x, y) \<in> (\<Union>(a, b)\<in>{X \<in> A \<times> B. fst X \<times> snd X \<subseteq> S}. a \<times> b)"
-      by (intro UN_I[of "(A0, B0)"]) auto
-  qed auto
-qed (metis A B topological_basis_open open_Times)
-
-instance prod :: (second_countable_topology, second_countable_topology) second_countable_topology
-proof
-  obtain A :: "'a set set" where "countable A" "topological_basis A"
-    using ex_countable_basis by auto
-  moreover
-  obtain B :: "'b set set" where "countable B" "topological_basis B"
-    using ex_countable_basis by auto
-  ultimately show "\<exists>B::('a \<times> 'b) set set. countable B \<and> topological_basis B"
-    by (auto intro!: exI[of _ "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"] topological_basis_prod)
-qed
-
 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"