generalized to copy of countable types instead of instantiation of nat for discrete topology
1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Probability/Discrete_Topology.thy Thu Nov 15 15:50:01 2012 +0100
1.3 @@ -0,0 +1,64 @@
1.4 +(* Title: HOL/Probability/Discrete_Topology.thy
1.5 + Author: Fabian Immler, TU München
1.6 +*)
1.7 +
1.8 +theory Discrete_Topology
1.9 +imports Multivariate_Analysis
1.10 +begin
1.11 +
1.12 +text {* Copy of discrete types with discrete topology. This space is polish. *}
1.13 +
1.14 +typedef 'a discrete = "UNIV::'a set"
1.15 +morphisms of_discrete discrete
1.16 +..
1.17 +
1.18 +instantiation discrete :: (type) topological_space
1.19 +begin
1.20 +
1.21 +definition open_discrete::"'a discrete set \<Rightarrow> bool"
1.22 + where "open_discrete s = True"
1.23 +
1.24 +instance proof qed (auto simp: open_discrete_def)
1.25 +end
1.26 +
1.27 +instantiation discrete :: (type) metric_space
1.28 +begin
1.29 +
1.30 +definition dist_discrete::"'a discrete \<Rightarrow> 'a discrete \<Rightarrow> real"
1.31 + where "dist_discrete n m = (if n = m then 0 else 1)"
1.32 +
1.33 +instance proof qed (auto simp: open_discrete_def dist_discrete_def intro: exI[where x=1])
1.34 +end
1.35 +
1.36 +instance discrete :: (type) complete_space
1.37 +proof
1.38 + fix X::"nat\<Rightarrow>'a discrete" assume "Cauchy X"
1.39 + hence "\<exists>n. \<forall>m\<ge>n. X n = X m"
1.40 + by (force simp: dist_discrete_def Cauchy_def split: split_if_asm dest:spec[where x=1])
1.41 + then guess n ..
1.42 + thus "convergent X"
1.43 + by (intro convergentI[where L="X n"] tendstoI eventually_sequentiallyI[of n])
1.44 + (simp add: dist_discrete_def)
1.45 +qed
1.46 +
1.47 +instance discrete :: (countable) countable
1.48 +proof
1.49 + have "inj (\<lambda>c::'a discrete. to_nat (of_discrete c))"
1.50 + by (simp add: inj_on_def of_discrete_inject)
1.51 + thus "\<exists>f::'a discrete \<Rightarrow> nat. inj f" by blast
1.52 +qed
1.53 +
1.54 +instance discrete :: (countable) enumerable_basis
1.55 +proof
1.56 + have "topological_basis (range (\<lambda>n::nat. {from_nat n::'a discrete}))"
1.57 + proof (intro topological_basisI)
1.58 + fix x::"'a discrete" and O' assume "open O'" "x \<in> O'"
1.59 + thus "\<exists>B'\<in>range (\<lambda>n. {from_nat n}). x \<in> B' \<and> B' \<subseteq> O'"
1.60 + by (auto intro: exI[where x="to_nat x"])
1.61 + qed (simp add: open_discrete_def)
1.62 + thus "\<exists>f::nat\<Rightarrow>'a discrete set. topological_basis (range f)" by blast
1.63 +qed
1.64 +
1.65 +instance discrete :: (countable) polish_space ..
1.66 +
1.67 +end
2.1 --- a/src/HOL/Probability/Probability.thy Thu Nov 15 11:16:58 2012 +0100
2.2 +++ b/src/HOL/Probability/Probability.thy Thu Nov 15 15:50:01 2012 +0100
2.3 @@ -1,5 +1,6 @@
2.4 theory Probability
2.5 imports
2.6 + Discrete_Topology
2.7 Complete_Measure
2.8 Probability_Measure
2.9 Infinite_Product_Measure
3.1 --- a/src/HOL/Probability/Regularity.thy Thu Nov 15 11:16:58 2012 +0100
3.2 +++ b/src/HOL/Probability/Regularity.thy Thu Nov 15 15:50:01 2012 +0100
3.3 @@ -2,53 +2,12 @@
3.4 Author: Fabian Immler, TU München
3.5 *)
3.6
3.7 +header {* Regularity of Measures *}
3.8 +
3.9 theory Regularity
3.10 imports Measure_Space Borel_Space
3.11 begin
3.12
3.13 -instantiation nat::topological_space
3.14 -begin
3.15 -
3.16 -definition open_nat::"nat set \<Rightarrow> bool"
3.17 - where "open_nat s = True"
3.18 -
3.19 -instance proof qed (auto simp: open_nat_def)
3.20 -end
3.21 -
3.22 -instantiation nat::metric_space
3.23 -begin
3.24 -
3.25 -definition dist_nat::"nat \<Rightarrow> nat \<Rightarrow> real"
3.26 - where "dist_nat n m = (if n = m then 0 else 1)"
3.27 -
3.28 -instance proof qed (auto simp: open_nat_def dist_nat_def intro: exI[where x=1])
3.29 -end
3.30 -
3.31 -instance nat::complete_space
3.32 -proof
3.33 - fix X::"nat\<Rightarrow>nat" assume "Cauchy X"
3.34 - hence "\<exists>n. \<forall>m\<ge>n. X m = X n"
3.35 - by (force simp: dist_nat_def Cauchy_def split: split_if_asm dest:spec[where x=1])
3.36 - then guess n ..
3.37 - thus "convergent X"
3.38 - apply (intro convergentI[where L="X n"] tendstoI)
3.39 - unfolding eventually_sequentially dist_nat_def
3.40 - apply (intro exI[where x=n])
3.41 - apply (intro allI)
3.42 - apply (drule_tac x=na in spec)
3.43 - apply simp
3.44 - done
3.45 -qed
3.46 -
3.47 -instance nat::enumerable_basis
3.48 -proof
3.49 - have "topological_basis (range (\<lambda>n::nat. {n}))"
3.50 - by (intro topological_basisI) (auto simp: open_nat_def)
3.51 - thus "\<exists>f::nat\<Rightarrow>nat set. topological_basis (range f)" by blast
3.52 -qed
3.53 -
3.54 -subsection {* Regularity of Measures *}
3.55 -
3.56 lemma ereal_approx_SUP:
3.57 fixes x::ereal
3.58 assumes A_notempty: "A \<noteq> {}"