author | haftmann |
Fri, 02 Jul 2010 14:23:17 +0200 | |
changeset 37693 | b10444eb9c98 |
parent 37678 | 0040bafffdef |
child 37715 | 44b27ea94a16 |
permissions | -rw-r--r-- |
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 |