author  haftmann 
Tue, 08 Jun 2010 16:37:22 +0200  
changeset 37388  793618618f78 
parent 35700  951974ce903e 
child 37652  6aa09d2a6cf9 
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 

66 
instance "*" :: (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 

37388  73 
instance "+" :: (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 

100 
text {* Functions *} 

101 

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

103 
proof 

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

105 
using finite_list [OF finite_UNIV] .. 

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

107 
proof 

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

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

110 
qed 

111 
qed 

112 

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

113 

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

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

115 

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

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

119 

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

120 
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

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

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

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

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

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

129 
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

130 
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

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

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

133 

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

134 
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

135 
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

136 

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

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

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

139 

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

140 
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

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

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

143 
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

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

145 

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

146 
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

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

148 
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

149 

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

151 

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

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

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

154 
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

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

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

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

158 
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

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

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

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

162 

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

163 
end 