haftmann@26169
|
1 |
(* Title: HOL/Library/Countable.thy
|
haftmann@26350
|
2 |
Author: Alexander Krauss, TU Muenchen
|
huffman@44405
|
3 |
Author: Brian Huffman, Portland State University
|
haftmann@26169
|
4 |
*)
|
haftmann@26169
|
5 |
|
haftmann@26169
|
6 |
header {* Encoding (almost) everything into natural numbers *}
|
haftmann@26169
|
7 |
|
haftmann@26169
|
8 |
theory Countable
|
huffman@35700
|
9 |
imports Main Rat Nat_Bijection
|
haftmann@26169
|
10 |
begin
|
haftmann@26169
|
11 |
|
haftmann@26169
|
12 |
subsection {* The class of countable types *}
|
haftmann@26169
|
13 |
|
haftmann@29734
|
14 |
class countable =
|
haftmann@26169
|
15 |
assumes ex_inj: "\<exists>to_nat \<Colon> 'a \<Rightarrow> nat. inj to_nat"
|
haftmann@26169
|
16 |
|
haftmann@26169
|
17 |
lemma countable_classI:
|
haftmann@26169
|
18 |
fixes f :: "'a \<Rightarrow> nat"
|
haftmann@26169
|
19 |
assumes "\<And>x y. f x = f y \<Longrightarrow> x = y"
|
haftmann@26169
|
20 |
shows "OFCLASS('a, countable_class)"
|
haftmann@26169
|
21 |
proof (intro_classes, rule exI)
|
haftmann@26169
|
22 |
show "inj f"
|
haftmann@26169
|
23 |
by (rule injI [OF assms]) assumption
|
haftmann@26169
|
24 |
qed
|
haftmann@26169
|
25 |
|
haftmann@26169
|
26 |
|
huffman@26585
|
27 |
subsection {* Conversion functions *}
|
haftmann@26169
|
28 |
|
haftmann@26169
|
29 |
definition to_nat :: "'a\<Colon>countable \<Rightarrow> nat" where
|
haftmann@26169
|
30 |
"to_nat = (SOME f. inj f)"
|
haftmann@26169
|
31 |
|
haftmann@26169
|
32 |
definition from_nat :: "nat \<Rightarrow> 'a\<Colon>countable" where
|
haftmann@26169
|
33 |
"from_nat = inv (to_nat \<Colon> 'a \<Rightarrow> nat)"
|
haftmann@26169
|
34 |
|
haftmann@26169
|
35 |
lemma inj_to_nat [simp]: "inj to_nat"
|
haftmann@26169
|
36 |
by (rule exE_some [OF ex_inj]) (simp add: to_nat_def)
|
haftmann@26169
|
37 |
|
hoelzl@44863
|
38 |
lemma inj_on_to_nat[simp, intro]: "inj_on to_nat S"
|
hoelzl@44863
|
39 |
using inj_to_nat by (auto simp: inj_on_def)
|
hoelzl@44863
|
40 |
|
huffman@29847
|
41 |
lemma surj_from_nat [simp]: "surj from_nat"
|
huffman@29847
|
42 |
unfolding from_nat_def by (simp add: inj_imp_surj_inv)
|
huffman@29847
|
43 |
|
haftmann@26169
|
44 |
lemma to_nat_split [simp]: "to_nat x = to_nat y \<longleftrightarrow> x = y"
|
haftmann@26169
|
45 |
using injD [OF inj_to_nat] by auto
|
haftmann@26169
|
46 |
|
haftmann@26169
|
47 |
lemma from_nat_to_nat [simp]:
|
haftmann@26169
|
48 |
"from_nat (to_nat x) = x"
|
haftmann@26169
|
49 |
by (simp add: from_nat_def)
|
haftmann@26169
|
50 |
|
haftmann@26169
|
51 |
|
haftmann@26169
|
52 |
subsection {* Countable types *}
|
haftmann@26169
|
53 |
|
haftmann@26169
|
54 |
instance nat :: countable
|
huffman@35700
|
55 |
by (rule countable_classI [of "id"]) simp
|
haftmann@26169
|
56 |
|
haftmann@26169
|
57 |
subclass (in finite) countable
|
haftmann@28823
|
58 |
proof
|
haftmann@26169
|
59 |
have "finite (UNIV\<Colon>'a set)" by (rule finite_UNIV)
|
nipkow@31992
|
60 |
with finite_conv_nat_seg_image [of "UNIV::'a set"]
|
haftmann@26169
|
61 |
obtain n and f :: "nat \<Rightarrow> 'a"
|
haftmann@26169
|
62 |
where "UNIV = f ` {i. i < n}" by auto
|
haftmann@26169
|
63 |
then have "surj f" unfolding surj_def by auto
|
haftmann@26169
|
64 |
then have "inj (inv f)" by (rule surj_imp_inj_inv)
|
haftmann@26169
|
65 |
then show "\<exists>to_nat \<Colon> 'a \<Rightarrow> nat. inj to_nat" by (rule exI[of inj])
|
haftmann@26169
|
66 |
qed
|
haftmann@26169
|
67 |
|
haftmann@26169
|
68 |
text {* Pairs *}
|
haftmann@26169
|
69 |
|
haftmann@37678
|
70 |
instance prod :: (countable, countable) countable
|
huffman@35700
|
71 |
by (rule countable_classI [of "\<lambda>(x, y). prod_encode (to_nat x, to_nat y)"])
|
huffman@35700
|
72 |
(auto simp add: prod_encode_eq)
|
haftmann@26169
|
73 |
|
haftmann@26169
|
74 |
|
haftmann@26169
|
75 |
text {* Sums *}
|
haftmann@26169
|
76 |
|
haftmann@37678
|
77 |
instance sum :: (countable, countable) countable
|
haftmann@26169
|
78 |
by (rule countable_classI [of "(\<lambda>x. case x of Inl a \<Rightarrow> to_nat (False, to_nat a)
|
haftmann@26169
|
79 |
| Inr b \<Rightarrow> to_nat (True, to_nat b))"])
|
huffman@35700
|
80 |
(simp split: sum.split_asm)
|
haftmann@26169
|
81 |
|
haftmann@26169
|
82 |
|
haftmann@26169
|
83 |
text {* Integers *}
|
haftmann@26169
|
84 |
|
haftmann@26169
|
85 |
instance int :: countable
|
huffman@35700
|
86 |
by (rule countable_classI [of "int_encode"])
|
huffman@35700
|
87 |
(simp add: int_encode_eq)
|
haftmann@26169
|
88 |
|
haftmann@26169
|
89 |
|
haftmann@26169
|
90 |
text {* Options *}
|
haftmann@26169
|
91 |
|
haftmann@26169
|
92 |
instance option :: (countable) countable
|
huffman@35700
|
93 |
by (rule countable_classI [of "option_case 0 (Suc \<circ> to_nat)"])
|
huffman@35700
|
94 |
(simp split: option.split_asm)
|
haftmann@26169
|
95 |
|
haftmann@26169
|
96 |
|
haftmann@26169
|
97 |
text {* Lists *}
|
haftmann@26169
|
98 |
|
haftmann@26169
|
99 |
instance list :: (countable) countable
|
huffman@35700
|
100 |
by (rule countable_classI [of "list_encode \<circ> map to_nat"])
|
huffman@35700
|
101 |
(simp add: list_encode_eq)
|
haftmann@26169
|
102 |
|
huffman@26243
|
103 |
|
haftmann@37652
|
104 |
text {* Further *}
|
haftmann@37652
|
105 |
|
haftmann@37652
|
106 |
instance String.literal :: countable
|
bulwahn@39477
|
107 |
by (rule countable_classI [of "to_nat o explode"])
|
bulwahn@39477
|
108 |
(auto simp add: explode_inject)
|
haftmann@37652
|
109 |
|
huffman@26243
|
110 |
text {* Functions *}
|
huffman@26243
|
111 |
|
huffman@26243
|
112 |
instance "fun" :: (finite, countable) countable
|
huffman@26243
|
113 |
proof
|
huffman@26243
|
114 |
obtain xs :: "'a list" where xs: "set xs = UNIV"
|
huffman@26243
|
115 |
using finite_list [OF finite_UNIV] ..
|
huffman@26243
|
116 |
show "\<exists>to_nat::('a \<Rightarrow> 'b) \<Rightarrow> nat. inj to_nat"
|
huffman@26243
|
117 |
proof
|
huffman@26243
|
118 |
show "inj (\<lambda>f. to_nat (map f xs))"
|
nipkow@39535
|
119 |
by (rule injI, simp add: xs fun_eq_iff)
|
huffman@26243
|
120 |
qed
|
huffman@26243
|
121 |
qed
|
huffman@26243
|
122 |
|
huffman@29817
|
123 |
|
huffman@29817
|
124 |
subsection {* The Rationals are Countably Infinite *}
|
huffman@29817
|
125 |
|
huffman@29817
|
126 |
definition nat_to_rat_surj :: "nat \<Rightarrow> rat" where
|
huffman@35700
|
127 |
"nat_to_rat_surj n = (let (a,b) = prod_decode n
|
huffman@35700
|
128 |
in Fract (int_decode a) (int_decode b))"
|
huffman@29817
|
129 |
|
huffman@29817
|
130 |
lemma surj_nat_to_rat_surj: "surj nat_to_rat_surj"
|
huffman@29817
|
131 |
unfolding surj_def
|
huffman@29817
|
132 |
proof
|
huffman@29817
|
133 |
fix r::rat
|
huffman@29817
|
134 |
show "\<exists>n. r = nat_to_rat_surj n"
|
haftmann@35374
|
135 |
proof (cases r)
|
haftmann@35374
|
136 |
fix i j assume [simp]: "r = Fract i j" and "j > 0"
|
huffman@35700
|
137 |
have "r = (let m = int_encode i; n = int_encode j
|
huffman@35700
|
138 |
in nat_to_rat_surj(prod_encode (m,n)))"
|
huffman@35700
|
139 |
by (simp add: Let_def nat_to_rat_surj_def)
|
huffman@29817
|
140 |
thus "\<exists>n. r = nat_to_rat_surj n" by(auto simp:Let_def)
|
huffman@29817
|
141 |
qed
|
huffman@29817
|
142 |
qed
|
huffman@29817
|
143 |
|
huffman@29817
|
144 |
lemma Rats_eq_range_nat_to_rat_surj: "\<rat> = range nat_to_rat_surj"
|
hoelzl@40950
|
145 |
by (simp add: Rats_def surj_nat_to_rat_surj)
|
huffman@29817
|
146 |
|
huffman@29817
|
147 |
context field_char_0
|
huffman@29817
|
148 |
begin
|
huffman@29817
|
149 |
|
huffman@29817
|
150 |
lemma Rats_eq_range_of_rat_o_nat_to_rat_surj:
|
huffman@29817
|
151 |
"\<rat> = range (of_rat o nat_to_rat_surj)"
|
huffman@29817
|
152 |
using surj_nat_to_rat_surj
|
huffman@29817
|
153 |
by (auto simp: Rats_def image_def surj_def)
|
huffman@29817
|
154 |
(blast intro: arg_cong[where f = of_rat])
|
huffman@29817
|
155 |
|
huffman@29817
|
156 |
lemma surj_of_rat_nat_to_rat_surj:
|
huffman@29817
|
157 |
"r\<in>\<rat> \<Longrightarrow> \<exists>n. r = of_rat(nat_to_rat_surj n)"
|
huffman@29817
|
158 |
by(simp add: Rats_eq_range_of_rat_o_nat_to_rat_surj image_def)
|
huffman@29817
|
159 |
|
haftmann@26169
|
160 |
end
|
huffman@29817
|
161 |
|
huffman@29817
|
162 |
instance rat :: countable
|
huffman@29817
|
163 |
proof
|
huffman@29817
|
164 |
show "\<exists>to_nat::rat \<Rightarrow> nat. inj to_nat"
|
huffman@29817
|
165 |
proof
|
huffman@29817
|
166 |
have "surj nat_to_rat_surj"
|
huffman@29817
|
167 |
by (rule surj_nat_to_rat_surj)
|
huffman@29817
|
168 |
then show "inj (inv nat_to_rat_surj)"
|
huffman@29817
|
169 |
by (rule surj_imp_inj_inv)
|
huffman@29817
|
170 |
qed
|
huffman@29817
|
171 |
qed
|
huffman@29817
|
172 |
|
huffman@44405
|
173 |
|
huffman@44405
|
174 |
subsection {* Automatically proving countability of datatypes *}
|
huffman@44405
|
175 |
|
huffman@44405
|
176 |
inductive finite_item :: "'a Datatype.item \<Rightarrow> bool" where
|
huffman@44405
|
177 |
undefined: "finite_item undefined"
|
huffman@44405
|
178 |
| In0: "finite_item x \<Longrightarrow> finite_item (Datatype.In0 x)"
|
huffman@44405
|
179 |
| In1: "finite_item x \<Longrightarrow> finite_item (Datatype.In1 x)"
|
huffman@44405
|
180 |
| Leaf: "finite_item (Datatype.Leaf a)"
|
huffman@44405
|
181 |
| Scons: "\<lbrakk>finite_item x; finite_item y\<rbrakk> \<Longrightarrow> finite_item (Datatype.Scons x y)"
|
huffman@44405
|
182 |
|
huffman@44405
|
183 |
function
|
huffman@44405
|
184 |
nth_item :: "nat \<Rightarrow> ('a::countable) Datatype.item"
|
huffman@44405
|
185 |
where
|
huffman@44405
|
186 |
"nth_item 0 = undefined"
|
huffman@44405
|
187 |
| "nth_item (Suc n) =
|
huffman@44405
|
188 |
(case sum_decode n of
|
huffman@44405
|
189 |
Inl i \<Rightarrow>
|
huffman@44405
|
190 |
(case sum_decode i of
|
huffman@44405
|
191 |
Inl j \<Rightarrow> Datatype.In0 (nth_item j)
|
huffman@44405
|
192 |
| Inr j \<Rightarrow> Datatype.In1 (nth_item j))
|
huffman@44405
|
193 |
| Inr i \<Rightarrow>
|
huffman@44405
|
194 |
(case sum_decode i of
|
huffman@44405
|
195 |
Inl j \<Rightarrow> Datatype.Leaf (from_nat j)
|
huffman@44405
|
196 |
| Inr j \<Rightarrow>
|
huffman@44405
|
197 |
(case prod_decode j of
|
huffman@44405
|
198 |
(a, b) \<Rightarrow> Datatype.Scons (nth_item a) (nth_item b))))"
|
huffman@44405
|
199 |
by pat_completeness auto
|
huffman@44405
|
200 |
|
huffman@44405
|
201 |
lemma le_sum_encode_Inl: "x \<le> y \<Longrightarrow> x \<le> sum_encode (Inl y)"
|
huffman@44405
|
202 |
unfolding sum_encode_def by simp
|
huffman@44405
|
203 |
|
huffman@44405
|
204 |
lemma le_sum_encode_Inr: "x \<le> y \<Longrightarrow> x \<le> sum_encode (Inr y)"
|
huffman@44405
|
205 |
unfolding sum_encode_def by simp
|
huffman@44405
|
206 |
|
huffman@44405
|
207 |
termination
|
huffman@44405
|
208 |
by (relation "measure id")
|
huffman@44405
|
209 |
(auto simp add: sum_encode_eq [symmetric] prod_encode_eq [symmetric]
|
huffman@44405
|
210 |
le_imp_less_Suc le_sum_encode_Inl le_sum_encode_Inr
|
huffman@44405
|
211 |
le_prod_encode_1 le_prod_encode_2)
|
huffman@44405
|
212 |
|
huffman@44405
|
213 |
lemma nth_item_covers: "finite_item x \<Longrightarrow> \<exists>n. nth_item n = x"
|
huffman@44405
|
214 |
proof (induct set: finite_item)
|
huffman@44405
|
215 |
case undefined
|
huffman@44405
|
216 |
have "nth_item 0 = undefined" by simp
|
huffman@44405
|
217 |
thus ?case ..
|
huffman@44405
|
218 |
next
|
huffman@44405
|
219 |
case (In0 x)
|
huffman@44405
|
220 |
then obtain n where "nth_item n = x" by fast
|
huffman@44405
|
221 |
hence "nth_item (Suc (sum_encode (Inl (sum_encode (Inl n)))))
|
huffman@44405
|
222 |
= Datatype.In0 x" by simp
|
huffman@44405
|
223 |
thus ?case ..
|
huffman@44405
|
224 |
next
|
huffman@44405
|
225 |
case (In1 x)
|
huffman@44405
|
226 |
then obtain n where "nth_item n = x" by fast
|
huffman@44405
|
227 |
hence "nth_item (Suc (sum_encode (Inl (sum_encode (Inr n)))))
|
huffman@44405
|
228 |
= Datatype.In1 x" by simp
|
huffman@44405
|
229 |
thus ?case ..
|
huffman@44405
|
230 |
next
|
huffman@44405
|
231 |
case (Leaf a)
|
huffman@44405
|
232 |
have "nth_item (Suc (sum_encode (Inr (sum_encode (Inl (to_nat a))))))
|
huffman@44405
|
233 |
= Datatype.Leaf a" by simp
|
huffman@44405
|
234 |
thus ?case ..
|
huffman@44405
|
235 |
next
|
huffman@44405
|
236 |
case (Scons x y)
|
huffman@44405
|
237 |
then obtain i j where "nth_item i = x" and "nth_item j = y" by fast
|
huffman@44405
|
238 |
hence "nth_item
|
huffman@44405
|
239 |
(Suc (sum_encode (Inr (sum_encode (Inr (prod_encode (i, j)))))))
|
huffman@44405
|
240 |
= Datatype.Scons x y" by simp
|
huffman@44405
|
241 |
thus ?case ..
|
huffman@44405
|
242 |
qed
|
huffman@44405
|
243 |
|
huffman@44405
|
244 |
theorem countable_datatype:
|
huffman@44405
|
245 |
fixes Rep :: "'b \<Rightarrow> ('a::countable) Datatype.item"
|
huffman@44405
|
246 |
fixes Abs :: "('a::countable) Datatype.item \<Rightarrow> 'b"
|
huffman@44405
|
247 |
fixes rep_set :: "('a::countable) Datatype.item \<Rightarrow> bool"
|
huffman@44405
|
248 |
assumes type: "type_definition Rep Abs (Collect rep_set)"
|
huffman@44405
|
249 |
assumes finite_item: "\<And>x. rep_set x \<Longrightarrow> finite_item x"
|
huffman@44405
|
250 |
shows "OFCLASS('b, countable_class)"
|
huffman@44405
|
251 |
proof
|
huffman@44405
|
252 |
def f \<equiv> "\<lambda>y. LEAST n. nth_item n = Rep y"
|
huffman@44405
|
253 |
{
|
huffman@44405
|
254 |
fix y :: 'b
|
huffman@44405
|
255 |
have "rep_set (Rep y)"
|
huffman@44405
|
256 |
using type_definition.Rep [OF type] by simp
|
huffman@44405
|
257 |
hence "finite_item (Rep y)"
|
huffman@44405
|
258 |
by (rule finite_item)
|
huffman@44405
|
259 |
hence "\<exists>n. nth_item n = Rep y"
|
huffman@44405
|
260 |
by (rule nth_item_covers)
|
huffman@44405
|
261 |
hence "nth_item (f y) = Rep y"
|
huffman@44405
|
262 |
unfolding f_def by (rule LeastI_ex)
|
huffman@44405
|
263 |
hence "Abs (nth_item (f y)) = y"
|
huffman@44405
|
264 |
using type_definition.Rep_inverse [OF type] by simp
|
huffman@44405
|
265 |
}
|
huffman@44405
|
266 |
hence "inj f"
|
huffman@44405
|
267 |
by (rule inj_on_inverseI)
|
huffman@44405
|
268 |
thus "\<exists>f::'b \<Rightarrow> nat. inj f"
|
huffman@44405
|
269 |
by - (rule exI)
|
huffman@44405
|
270 |
qed
|
huffman@44405
|
271 |
|
huffman@44405
|
272 |
method_setup countable_datatype = {*
|
huffman@44405
|
273 |
let
|
huffman@44405
|
274 |
fun countable_tac ctxt =
|
huffman@44405
|
275 |
SUBGOAL (fn (goal, i) =>
|
huffman@44405
|
276 |
let
|
huffman@44405
|
277 |
val ty_name =
|
huffman@44405
|
278 |
(case goal of
|
huffman@44405
|
279 |
(_ $ Const ("TYPE", Type ("itself", [Type (n, _)]))) => n
|
huffman@44405
|
280 |
| _ => raise Match)
|
huffman@44405
|
281 |
val typedef_info = hd (Typedef.get_info ctxt ty_name)
|
huffman@44405
|
282 |
val typedef_thm = #type_definition (snd typedef_info)
|
huffman@44405
|
283 |
val pred_name =
|
huffman@44405
|
284 |
(case HOLogic.dest_Trueprop (concl_of typedef_thm) of
|
huffman@44405
|
285 |
(typedef $ rep $ abs $ (collect $ Const (n, _))) => n
|
huffman@44405
|
286 |
| _ => raise Match)
|
huffman@44405
|
287 |
val induct_info = Inductive.the_inductive ctxt pred_name
|
huffman@44405
|
288 |
val pred_names = #names (fst induct_info)
|
huffman@44405
|
289 |
val induct_thms = #inducts (snd induct_info)
|
huffman@44405
|
290 |
val alist = pred_names ~~ induct_thms
|
huffman@44405
|
291 |
val induct_thm = the (AList.lookup (op =) alist pred_name)
|
huffman@44405
|
292 |
val rules = @{thms finite_item.intros}
|
huffman@44405
|
293 |
in
|
huffman@44405
|
294 |
SOLVED' (fn i => EVERY
|
huffman@44405
|
295 |
[rtac @{thm countable_datatype} i,
|
huffman@44405
|
296 |
rtac typedef_thm i,
|
huffman@44405
|
297 |
etac induct_thm i,
|
huffman@44405
|
298 |
REPEAT (resolve_tac rules i ORELSE atac i)]) 1
|
huffman@44405
|
299 |
end)
|
huffman@44405
|
300 |
in
|
huffman@44405
|
301 |
Scan.succeed (fn ctxt => SIMPLE_METHOD' (countable_tac ctxt))
|
huffman@29817
|
302 |
end
|
huffman@44405
|
303 |
*} "prove countable class instances for datatypes"
|
huffman@44405
|
304 |
|
huffman@44405
|
305 |
hide_const (open) finite_item nth_item
|
huffman@44405
|
306 |
|
huffman@44405
|
307 |
|
huffman@44405
|
308 |
subsection {* Countable datatypes *}
|
huffman@44405
|
309 |
|
huffman@44405
|
310 |
instance typerep :: countable
|
huffman@44405
|
311 |
by countable_datatype
|
huffman@44405
|
312 |
|
huffman@44405
|
313 |
end
|