author  haftmann 
Thu, 01 Jul 2010 16:54:44 +0200  
changeset 37678  0040bafffdef 
parent 37652  6aa09d2a6cf9 
child 37715  44b27ea94a16 
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) 

113 
fix t t' :: typerep and ts 

114 
have "(\<forall>t'. to_nat_typerep t = to_nat_typerep t' \<longrightarrow> t = t') 

115 
\<and> (\<forall>ts'. map to_nat_typerep ts = map to_nat_typerep ts' \<longrightarrow> ts = ts')" 

116 
proof (induct rule: typerep.induct) 

117 
case (Typerep c ts) show ?case 

118 
proof (rule allI, rule impI) 

119 
fix t' 

120 
assume hyp: "to_nat_typerep (Typerep.Typerep c ts) = to_nat_typerep t'" 

121 
then obtain c' ts' where t': "t' = (Typerep.Typerep c' ts')" 

122 
by (cases t') auto 

123 
with Typerep hyp have "c = c'" and "ts = ts'" by simp_all 

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

125 
qed 

126 
next 

127 
case Nil_typerep then show ?case by simp 

128 
next 

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

130 
qed 

131 
then have "to_nat_typerep t = to_nat_typerep t' \<Longrightarrow> t = t'" by auto 

132 
moreover assume "to_nat_typerep t = to_nat_typerep t'" 

133 
ultimately show "t = t'" by simp 

134 
qed 

135 

136 
end 

137 

138 

26243  139 
text {* Functions *} 
140 

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

142 
proof 

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

144 
using finite_list [OF finite_UNIV] .. 

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

146 
proof 

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

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

149 
qed 

150 
qed 

151 

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 
subsection {* The Rationals are Countably Infinite *} 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

154 

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

155 
definition nat_to_rat_surj :: "nat \<Rightarrow> rat" where 
35700  156 
"nat_to_rat_surj n = (let (a,b) = prod_decode n 
157 
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

158 

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

159 
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

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

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

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

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

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

168 
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

169 
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

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

171 
qed 
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_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

174 
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

175 

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

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

177 
begin 
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 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

180 
"\<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

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

182 
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

183 
(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

184 

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

185 
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

186 
"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

187 
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

188 

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

190 

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

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

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

193 
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

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

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

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

197 
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

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

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

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

201 

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

202 
end 