author  haftmann 
Mon, 05 Jul 2010 15:12:20 +0200  
changeset 37715  44b27ea94a16 
parent 37678  0040bafffdef 
child 39198  f967a16dfcdd 
permissions  rwrr 
26169  1 
(* Title: HOL/Library/Countable.thy 
26350  2 
Author: Alexander Krauss, TU Muenchen 
26169  3 
*) 
4 

5 
header {* Encoding (almost) everything into natural numbers *} 

6 

7 
theory Countable 

35700  8 
imports Main Rat Nat_Bijection 
26169  9 
begin 
10 

11 
subsection {* The class of countable types *} 

12 

29797  13 
class countable = 
26169  14 
assumes ex_inj: "\<exists>to_nat \<Colon> 'a \<Rightarrow> nat. inj to_nat" 
15 

16 
lemma countable_classI: 

17 
fixes f :: "'a \<Rightarrow> nat" 

18 
assumes "\<And>x y. f x = f y \<Longrightarrow> x = y" 

19 
shows "OFCLASS('a, countable_class)" 

20 
proof (intro_classes, rule exI) 

21 
show "inj f" 

22 
by (rule injI [OF assms]) assumption 

23 
qed 

24 

25 

26585  26 
subsection {* Conversion functions *} 
26169  27 

28 
definition to_nat :: "'a\<Colon>countable \<Rightarrow> nat" where 

29 
"to_nat = (SOME f. inj f)" 

30 

31 
definition from_nat :: "nat \<Rightarrow> 'a\<Colon>countable" where 

32 
"from_nat = inv (to_nat \<Colon> 'a \<Rightarrow> nat)" 

33 

34 
lemma inj_to_nat [simp]: "inj to_nat" 

35 
by (rule exE_some [OF ex_inj]) (simp add: to_nat_def) 

36 

29910  37 
lemma surj_from_nat [simp]: "surj from_nat" 
38 
unfolding from_nat_def by (simp add: inj_imp_surj_inv) 

39 

26169  40 
lemma to_nat_split [simp]: "to_nat x = to_nat y \<longleftrightarrow> x = y" 
41 
using injD [OF inj_to_nat] by auto 

42 

43 
lemma from_nat_to_nat [simp]: 

44 
"from_nat (to_nat x) = x" 

45 
by (simp add: from_nat_def) 

46 

47 

48 
subsection {* Countable types *} 

49 

50 
instance nat :: countable 

35700  51 
by (rule countable_classI [of "id"]) simp 
26169  52 

53 
subclass (in finite) countable 

28823  54 
proof 
26169  55 
have "finite (UNIV\<Colon>'a set)" by (rule finite_UNIV) 
31992  56 
with finite_conv_nat_seg_image [of "UNIV::'a set"] 
26169  57 
obtain n and f :: "nat \<Rightarrow> 'a" 
58 
where "UNIV = f ` {i. i < n}" by auto 

59 
then have "surj f" unfolding surj_def by auto 

60 
then have "inj (inv f)" by (rule surj_imp_inj_inv) 

61 
then show "\<exists>to_nat \<Colon> 'a \<Rightarrow> nat. inj to_nat" by (rule exI[of inj]) 

62 
qed 

63 

64 
text {* Pairs *} 

65 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37652
diff
changeset

66 
instance prod :: (countable, countable) countable 
35700  67 
by (rule countable_classI [of "\<lambda>(x, y). prod_encode (to_nat x, to_nat y)"]) 
68 
(auto simp add: prod_encode_eq) 

26169  69 

70 

71 
text {* Sums *} 

72 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37652
diff
changeset

73 
instance sum :: (countable, countable) countable 
26169  74 
by (rule countable_classI [of "(\<lambda>x. case x of Inl a \<Rightarrow> to_nat (False, to_nat a) 
75 
 Inr b \<Rightarrow> to_nat (True, to_nat b))"]) 

35700  76 
(simp split: sum.split_asm) 
26169  77 

78 

79 
text {* Integers *} 

80 

81 
instance int :: countable 

35700  82 
by (rule countable_classI [of "int_encode"]) 
83 
(simp add: int_encode_eq) 

26169  84 

85 

86 
text {* Options *} 

87 

88 
instance option :: (countable) countable 

35700  89 
by (rule countable_classI [of "option_case 0 (Suc \<circ> to_nat)"]) 
90 
(simp split: option.split_asm) 

26169  91 

92 

93 
text {* Lists *} 

94 

95 
instance list :: (countable) countable 

35700  96 
by (rule countable_classI [of "list_encode \<circ> map to_nat"]) 
97 
(simp add: list_encode_eq) 

26169  98 

26243  99 

37652  100 
text {* Further *} 
101 

102 
instance String.literal :: countable 

103 
by (rule countable_classI [of "String.literal_case to_nat"]) 

104 
(auto split: String.literal.splits) 

105 

106 
instantiation typerep :: countable 

107 
begin 

108 

109 
fun to_nat_typerep :: "typerep \<Rightarrow> nat" where 

110 
"to_nat_typerep (Typerep.Typerep c ts) = to_nat (to_nat c, to_nat (map to_nat_typerep ts))" 

111 

112 
instance proof (rule countable_classI) 

37715  113 
fix t t' :: typerep and ts ts' :: "typerep list" 
114 
assume "to_nat_typerep t = to_nat_typerep t'" 

115 
moreover have "to_nat_typerep t = to_nat_typerep t' \<Longrightarrow> t = t'" 

116 
and "map to_nat_typerep ts = map to_nat_typerep ts' \<Longrightarrow> ts = ts'" 

117 
proof (induct t and ts arbitrary: t' and ts' rule: typerep.inducts) 

118 
case (Typerep c ts t') 

119 
then obtain c' ts' where t': "t' = Typerep.Typerep c' ts'" by (cases t') auto 

120 
with Typerep have "c = c'" and "ts = ts'" by simp_all 

121 
with t' show "Typerep.Typerep c ts = t'" by simp 

37652  122 
next 
123 
case Nil_typerep then show ?case by simp 

124 
next 

125 
case (Cons_typerep t ts) then show ?case by auto 

126 
qed 

127 
ultimately show "t = t'" by simp 

128 
qed 

129 

130 
end 

131 

132 

26243  133 
text {* Functions *} 
134 

135 
instance "fun" :: (finite, countable) countable 

136 
proof 

137 
obtain xs :: "'a list" where xs: "set xs = UNIV" 

138 
using finite_list [OF finite_UNIV] .. 

139 
show "\<exists>to_nat::('a \<Rightarrow> 'b) \<Rightarrow> nat. inj to_nat" 

140 
proof 

141 
show "inj (\<lambda>f. to_nat (map f xs))" 

142 
by (rule injI, simp add: xs expand_fun_eq) 

143 
qed 

144 
qed 

145 

29880
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

146 

3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

147 
subsection {* The Rationals are Countably Infinite *} 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

148 

3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

149 
definition nat_to_rat_surj :: "nat \<Rightarrow> rat" where 
35700  150 
"nat_to_rat_surj n = (let (a,b) = prod_decode n 
151 
in Fract (int_decode a) (int_decode b))" 

29880
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

152 

3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

153 
lemma surj_nat_to_rat_surj: "surj nat_to_rat_surj" 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

154 
unfolding surj_def 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

155 
proof 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

156 
fix r::rat 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

157 
show "\<exists>n. r = nat_to_rat_surj n" 
35374  158 
proof (cases r) 
159 
fix i j assume [simp]: "r = Fract i j" and "j > 0" 

35700  160 
have "r = (let m = int_encode i; n = int_encode j 
161 
in nat_to_rat_surj(prod_encode (m,n)))" 

162 
by (simp add: Let_def nat_to_rat_surj_def) 

29880
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

163 
thus "\<exists>n. r = nat_to_rat_surj n" by(auto simp:Let_def) 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

164 
qed 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

165 
qed 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

166 

3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

167 
lemma Rats_eq_range_nat_to_rat_surj: "\<rat> = range nat_to_rat_surj" 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

168 
by (simp add: Rats_def surj_nat_to_rat_surj surj_range) 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

169 

3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

170 
context field_char_0 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

171 
begin 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

172 

3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

173 
lemma Rats_eq_range_of_rat_o_nat_to_rat_surj: 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

174 
"\<rat> = range (of_rat o nat_to_rat_surj)" 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

175 
using surj_nat_to_rat_surj 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

176 
by (auto simp: Rats_def image_def surj_def) 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

177 
(blast intro: arg_cong[where f = of_rat]) 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

178 

3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

179 
lemma surj_of_rat_nat_to_rat_surj: 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

180 
"r\<in>\<rat> \<Longrightarrow> \<exists>n. r = of_rat(nat_to_rat_surj n)" 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

181 
by(simp add: Rats_eq_range_of_rat_o_nat_to_rat_surj image_def) 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

182 

26169  183 
end 
29880
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

184 

3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

185 
instance rat :: countable 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

186 
proof 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

187 
show "\<exists>to_nat::rat \<Rightarrow> nat. inj to_nat" 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

188 
proof 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

189 
have "surj nat_to_rat_surj" 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

190 
by (rule surj_nat_to_rat_surj) 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

191 
then show "inj (inv nat_to_rat_surj)" 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

192 
by (rule surj_imp_inj_inv) 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

193 
qed 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

194 
qed 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

195 

3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

196 
end 