author | haftmann |
Thu, 20 May 2010 17:29:43 +0200 | |
changeset 37027 | 98bfff1d159d |
parent 35700 | 951974ce903e |
child 37388 | 793618618f78 |
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 |
||
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 |
||
73 |
instance "+":: (countable, countable) countable |
|
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 |