1(* Title: HOL/Probability/Discrete_Topology.thy 2 Author: Fabian Immler, TU M��nchen 3*) 4 5theory Discrete_Topology 6imports "HOL-Analysis.Analysis" 7begin 8 9text \<open>Copy of discrete types with discrete topology. This space is polish.\<close> 10 11typedef 'a discrete = "UNIV::'a set" 12morphisms of_discrete discrete 13.. 14 15instantiation discrete :: (type) metric_space 16begin 17 18definition dist_discrete :: "'a discrete \<Rightarrow> 'a discrete \<Rightarrow> real" 19 where "dist_discrete n m = (if n = m then 0 else 1)" 20 21definition uniformity_discrete :: "('a discrete \<times> 'a discrete) filter" where 22 "(uniformity::('a discrete \<times> 'a discrete) filter) = (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})" 23 24definition "open_discrete" :: "'a discrete set \<Rightarrow> bool" where 25 "(open::'a discrete set \<Rightarrow> bool) U \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)" 26 27instance proof qed (auto simp: uniformity_discrete_def open_discrete_def dist_discrete_def intro: exI[where x=1]) 28end 29 30lemma open_discrete: "open (S :: 'a discrete set)" 31 unfolding open_dist dist_discrete_def by (auto intro!: exI[of _ "1 / 2"]) 32 33instance discrete :: (type) complete_space 34proof 35 fix X::"nat\<Rightarrow>'a discrete" assume "Cauchy X" 36 hence "\<exists>n. \<forall>m\<ge>n. X n = X m" 37 by (force simp: dist_discrete_def Cauchy_def split: if_split_asm dest:spec[where x=1]) 38 then guess n .. 39 thus "convergent X" 40 by (intro convergentI[where L="X n"] tendstoI eventually_sequentiallyI[of n]) 41 (simp add: dist_discrete_def) 42qed 43 44instance discrete :: (countable) countable 45proof 46 have "inj (\<lambda>c::'a discrete. to_nat (of_discrete c))" 47 by (simp add: inj_on_def of_discrete_inject) 48 thus "\<exists>f::'a discrete \<Rightarrow> nat. inj f" by blast 49qed 50 51instance discrete :: (countable) second_countable_topology 52proof 53 let ?B = "range (\<lambda>n::'a discrete. {n})" 54 have "\<And>S. generate_topology ?B (\<Union>x\<in>S. {x})" 55 by (intro generate_topology_Union) (auto intro: generate_topology.intros) 56 then have "open = generate_topology ?B" 57 by (auto intro!: ext simp: open_discrete) 58 moreover have "countable ?B" by simp 59 ultimately show "\<exists>B::'a discrete set set. countable B \<and> open = generate_topology B" by blast 60qed 61 62instance discrete :: (countable) polish_space .. 63 64end 65