author  wenzelm 
Thu, 18 Apr 2013 17:07:01 +0200  
changeset 51717  9e7d1c139569 
parent 51343  b61b32f62c78 
child 61808  fc1556774cfe 
permissions  rwrr 
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 
51000  6 
imports "~~/src/HOL/Multivariate_Analysis/Multivariate_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 

1badf63e5d97
generalized to copy of countable types instead of instantiation of nat for discrete topology
immler
parents:
diff
changeset

9 
text {* Copy of discrete types with discrete topology. This space is polish. *} 
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) topological_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 

1badf63e5d97
generalized to copy of countable types instead of instantiation of nat for discrete topology
immler
parents:
diff
changeset

18 
definition open_discrete::"'a discrete set \<Rightarrow> bool" 
1badf63e5d97
generalized to copy of countable types instead of instantiation of nat for discrete topology
immler
parents:
diff
changeset

19 
where "open_discrete s = True" 
1badf63e5d97
generalized to copy of countable types instead of instantiation of nat for discrete topology
immler
parents:
diff
changeset

20 

1badf63e5d97
generalized to copy of countable types instead of instantiation of nat for discrete topology
immler
parents:
diff
changeset

21 
instance proof qed (auto simp: open_discrete_def) 
1badf63e5d97
generalized to copy of countable types instead of instantiation of nat for discrete topology
immler
parents:
diff
changeset

22 
end 
1badf63e5d97
generalized to copy of countable types instead of instantiation of nat for discrete topology
immler
parents:
diff
changeset

23 

1badf63e5d97
generalized to copy of countable types instead of instantiation of nat for discrete topology
immler
parents:
diff
changeset

24 
instantiation discrete :: (type) metric_space 
1badf63e5d97
generalized to copy of countable types instead of instantiation of nat for discrete topology
immler
parents:
diff
changeset

25 
begin 
1badf63e5d97
generalized to copy of countable types instead of instantiation of nat for discrete topology
immler
parents:
diff
changeset

26 

1badf63e5d97
generalized to copy of countable types instead of instantiation of nat for discrete topology
immler
parents:
diff
changeset

27 
definition dist_discrete::"'a discrete \<Rightarrow> 'a discrete \<Rightarrow> real" 
1badf63e5d97
generalized to copy of countable types instead of instantiation of nat for discrete topology
immler
parents:
diff
changeset

28 
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

29 

1badf63e5d97
generalized to copy of countable types instead of instantiation of nat for discrete topology
immler
parents:
diff
changeset

30 
instance proof qed (auto simp: open_discrete_def dist_discrete_def intro: exI[where x=1]) 
1badf63e5d97
generalized to copy of countable types instead of instantiation of nat for discrete topology
immler
parents:
diff
changeset

31 
end 
1badf63e5d97
generalized to copy of countable types instead of instantiation of nat for discrete topology
immler
parents:
diff
changeset

32 

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 
1badf63e5d97
generalized to copy of countable types instead of instantiation of nat for discrete topology
immler
parents:
diff
changeset

35 
fix X::"nat\<Rightarrow>'a discrete" assume "Cauchy X" 
1badf63e5d97
generalized to copy of countable types instead of instantiation of nat for discrete topology
immler
parents:
diff
changeset

36 
hence "\<exists>n. \<forall>m\<ge>n. X n = X m" 
1badf63e5d97
generalized to copy of countable types instead of instantiation of nat for discrete topology
immler
parents:
diff
changeset

37 
by (force simp: dist_discrete_def Cauchy_def split: split_if_asm dest:spec[where x=1]) 
1badf63e5d97
generalized to copy of countable types instead of instantiation of nat for discrete topology
immler
parents:
diff
changeset

38 
then guess n .. 
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" 
b61b32f62c78
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl
parents:
51000
diff
changeset

57 
by (auto intro!: ext simp: open_discrete_def) 
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 