# HG changeset patch
# User hoelzl
# Date 1358180944 -3600
# Node ID ae630bab13dae6ab71cf510e46b44346a11c9374
# Parent  b22ecedde1c7e665dcd102c154b9ade9be8bf6c1
renamed countable_basis_space to second_countable_topology

diff -r b22ecedde1c7 -r ae630bab13da src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jan 14 17:16:59 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jan 14 17:29:04 2013 +0100
@@ -220,11 +220,11 @@
 
 end
 
-class countable_basis_space = topological_space +
+class second_countable_topology = topological_space +
   assumes ex_countable_basis:
     "\<exists>B::'a::topological_space set set. countable B \<and> topological_basis B"
 
-sublocale countable_basis_space < countable_basis "SOME B. countable B \<and> topological_basis B"
+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
 
 subsection {* Polish spaces *}
@@ -232,7 +232,7 @@
 text {* Textbooks define Polish spaces as completely metrizable.
   We assume the topology to be complete for a given metric. *}
 
-class polish_space = complete_space + countable_basis_space
+class polish_space = complete_space + second_countable_topology
 
 subsection {* General notion of a topology as a value *}
 
@@ -5411,7 +5411,7 @@
   finally show ?thesis .
 qed
 
-instance euclidean_space \<subseteq> countable_basis_space
+instance euclidean_space \<subseteq> second_countable_topology
 proof
   def a \<equiv> "\<lambda>f :: 'a \<Rightarrow> (real \<times> real). \<Sum>i\<in>Basis. fst (f i) *\<^sub>R i"
   then have a: "\<And>f. (\<Sum>i\<in>Basis. fst (f i) *\<^sub>R i) = a f" by simp
diff -r b22ecedde1c7 -r ae630bab13da src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Mon Jan 14 17:16:59 2013 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Mon Jan 14 17:29:04 2013 +0100
@@ -172,7 +172,7 @@
   qed auto
 qed (metis A B topological_basis_open open_Times)
 
-instance prod :: (countable_basis_space, countable_basis_space) countable_basis_space
+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
@@ -184,7 +184,7 @@
 qed
 
 lemma borel_measurable_Pair[measurable (raw)]:
-  fixes f :: "'a \<Rightarrow> 'b::countable_basis_space" and g :: "'a \<Rightarrow> 'c::countable_basis_space"
+  fixes f :: "'a \<Rightarrow> 'b::second_countable_topology" and g :: "'a \<Rightarrow> 'c::second_countable_topology"
   assumes f[measurable]: "f \<in> borel_measurable M"
   assumes g[measurable]: "g \<in> borel_measurable M"
   shows "(\<lambda>x. (f x, g x)) \<in> borel_measurable M"
@@ -257,7 +257,7 @@
 qed
 
 lemma borel_measurable_continuous_Pair:
-  fixes f :: "'a \<Rightarrow> 'b::countable_basis_space" and g :: "'a \<Rightarrow> 'c::countable_basis_space"
+  fixes f :: "'a \<Rightarrow> 'b::second_countable_topology" and g :: "'a \<Rightarrow> 'c::second_countable_topology"
   assumes [measurable]: "f \<in> borel_measurable M"
   assumes [measurable]: "g \<in> borel_measurable M"
   assumes H: "continuous_on UNIV (\<lambda>x. H (fst x) (snd x))"
@@ -271,7 +271,7 @@
 section "Borel spaces on euclidean spaces"
 
 lemma borel_measurable_inner[measurable (raw)]:
-  fixes f g :: "'a \<Rightarrow> 'b::{countable_basis_space, real_inner}"
+  fixes f g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_inner}"
   assumes "f \<in> borel_measurable M"
   assumes "g \<in> borel_measurable M"
   shows "(\<lambda>x. f x \<bullet> g x) \<in> borel_measurable M"
diff -r b22ecedde1c7 -r ae630bab13da src/HOL/Probability/Discrete_Topology.thy
--- a/src/HOL/Probability/Discrete_Topology.thy	Mon Jan 14 17:16:59 2013 +0100
+++ b/src/HOL/Probability/Discrete_Topology.thy	Mon Jan 14 17:29:04 2013 +0100
@@ -48,7 +48,7 @@
   thus "\<exists>f::'a discrete \<Rightarrow> nat. inj f" by blast
 qed
 
-instance discrete :: (countable) countable_basis_space
+instance discrete :: (countable) second_countable_topology
 proof
   let ?B = "(range (\<lambda>n::nat. {from_nat n::'a discrete}))"
   have "topological_basis ?B"
diff -r b22ecedde1c7 -r ae630bab13da src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Mon Jan 14 17:16:59 2013 +0100
+++ b/src/HOL/Probability/Fin_Map.thy	Mon Jan 14 17:29:04 2013 +0100
@@ -1045,7 +1045,7 @@
 lemma product_open_generates_sets_PiF_single:
   assumes "I \<noteq> {}"
   assumes [simp]: "finite I"
-  shows "sets (PiF {I} (\<lambda>_. borel::'b::countable_basis_space measure)) =
+  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
@@ -1064,7 +1064,7 @@
 lemma product_open_generates_sets_PiM:
   assumes "I \<noteq> {}"
   assumes [simp]: "finite I"
-  shows "sets (PiM I (\<lambda>_. borel::'b::countable_basis_space measure)) =
+  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
diff -r b22ecedde1c7 -r ae630bab13da src/HOL/Probability/Regularity.thy
--- a/src/HOL/Probability/Regularity.thy	Mon Jan 14 17:16:59 2013 +0100
+++ b/src/HOL/Probability/Regularity.thy	Mon Jan 14 17:29:04 2013 +0100
@@ -104,7 +104,7 @@
 qed
 
 lemma
-  fixes M::"'a::{countable_basis_space, complete_space} measure"
+  fixes M::"'a::{second_countable_topology, complete_space} measure"
   assumes sb: "sets M = sets borel"
   assumes "emeasure M (space M) \<noteq> \<infinity>"
   assumes "B \<in> sets borel"