isabelle: src/HOL/Probability/Discrete_Topology.thy@f8fb4384180e (annotated)

50089 1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	1	(* Title: HOL/Probability/Discrete_Topology.thy
1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	2	Author: Fabian Immler, TU München
1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	3	*)
1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	4
1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	5	theory Discrete_Topology
66453 cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a; wenzelm parents: 63627 diff changeset	6	imports "HOL-Analysis.Analysis"
50089 1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	7	begin
1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	8
61808 fc1556774cfe isabelle update_cartouches -c -t; wenzelm parents: 51343 diff changeset	9	text \<open>Copy of discrete types with discrete topology. This space is polish.\<close>
50089 1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	10
1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	11	typedef 'a discrete = "UNIV::'a set"
1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	12	morphisms of_discrete discrete
1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	13	..
1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	14
1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	15	instantiation discrete :: (type) metric_space
1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	16	begin
1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	17
62101 26c0a70f78a3 add uniform spaces hoelzl parents: 61808 diff changeset	18	definition dist_discrete :: "'a discrete \<Rightarrow> 'a discrete \<Rightarrow> real"
50089 1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	19	where "dist_discrete n m = (if n = m then 0 else 1)"
1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	20
62101 26c0a70f78a3 add uniform spaces hoelzl parents: 61808 diff changeset	21	definition uniformity_discrete :: "('a discrete \<times> 'a discrete) filter" where
69260 0a9688695a1b removed relics of ASCII syntax for indexed big operators haftmann parents: 66453 diff changeset	22	"(uniformity::('a discrete \<times> 'a discrete) filter) = (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
62101 26c0a70f78a3 add uniform spaces hoelzl parents: 61808 diff changeset	23
26c0a70f78a3 add uniform spaces hoelzl parents: 61808 diff changeset	24	definition "open_discrete" :: "'a discrete set \<Rightarrow> bool" where
26c0a70f78a3 add uniform spaces hoelzl parents: 61808 diff changeset	25	"(open::'a discrete set \<Rightarrow> bool) U \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
26c0a70f78a3 add uniform spaces hoelzl parents: 61808 diff changeset	26
26c0a70f78a3 add uniform spaces hoelzl parents: 61808 diff changeset	27	instance proof qed (auto simp: uniformity_discrete_def open_discrete_def dist_discrete_def intro: exI[where x=1])
50089 1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	28	end
1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	29
62101 26c0a70f78a3 add uniform spaces hoelzl parents: 61808 diff changeset	30	lemma open_discrete: "open (S :: 'a discrete set)"
26c0a70f78a3 add uniform spaces hoelzl parents: 61808 diff changeset	31	unfolding open_dist dist_discrete_def by (auto intro!: exI[of _ "1 / 2"])
26c0a70f78a3 add uniform spaces hoelzl parents: 61808 diff changeset	32
50089 1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	33	instance discrete :: (type) complete_space
1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	34	proof
74362 0135a0c77b64 tuned proofs --- avoid 'guess'; wenzelm parents: 69260 diff changeset	35	fix X::"nat\<Rightarrow>'a discrete"
0135a0c77b64 tuned proofs --- avoid 'guess'; wenzelm parents: 69260 diff changeset	36	assume "Cauchy X"
0135a0c77b64 tuned proofs --- avoid 'guess'; wenzelm parents: 69260 diff changeset	37	then obtain n where "\<forall>m\<ge>n. X n = X m"
62390 842917225d56 more canonical names nipkow parents: 62101 diff changeset	38	by (force simp: dist_discrete_def Cauchy_def split: if_split_asm dest:spec[where x=1])
50089 1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	39	thus "convergent X"
1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	40	by (intro convergentI[where L="X n"] tendstoI eventually_sequentiallyI[of n])
1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	41	(simp add: dist_discrete_def)
1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	42	qed
1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	43
1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	44	instance discrete :: (countable) countable
1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	45	proof
1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	46	have "inj (\<lambda>c::'a discrete. to_nat (of_discrete c))"
1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	47	by (simp add: inj_on_def of_discrete_inject)
1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	48	thus "\<exists>f::'a discrete \<Rightarrow> nat. inj f" by blast
1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	49	qed
1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	50
50881 ae630bab13da renamed countable_basis_space to second_countable_topology hoelzl parents: 50245 diff changeset	51	instance discrete :: (countable) second_countable_topology
50089 1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	52	proof
51343 b61b32f62c78 use generate_topology for second countable topologies, does not require intersection stable basis hoelzl parents: 51000 diff changeset	53	let ?B = "range (\<lambda>n::'a discrete. {n})"
b61b32f62c78 use generate_topology for second countable topologies, does not require intersection stable basis hoelzl parents: 51000 diff changeset	54	have "\<And>S. generate_topology ?B (\<Union>x\<in>S. {x})"
b61b32f62c78 use generate_topology for second countable topologies, does not require intersection stable basis hoelzl parents: 51000 diff changeset	55	by (intro generate_topology_Union) (auto intro: generate_topology.intros)
b61b32f62c78 use generate_topology for second countable topologies, does not require intersection stable basis hoelzl parents: 51000 diff changeset	56	then have "open = generate_topology ?B"
62101 26c0a70f78a3 add uniform spaces hoelzl parents: 61808 diff changeset	57	by (auto intro!: ext simp: open_discrete)
50245 dea9363887a6 based countable topological basis on Countable_Set immler parents: 50089 diff changeset	58	moreover have "countable ?B" by simp
51343 b61b32f62c78 use generate_topology for second countable topologies, does not require intersection stable basis hoelzl parents: 51000 diff changeset	59	ultimately show "\<exists>B::'a discrete set set. countable B \<and> open = generate_topology B" by blast
50089 1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	60	qed
1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	61
1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	62	instance discrete :: (countable) polish_space ..
1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	63
1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: diff changeset	64	end

author	wenzelm
	Thu, 29 Feb 2024 22:52:45 +0100
changeset 79750	f8fb4384180e
parent 74362	0135a0c77b64
permissions	-rw-r--r--