2 Author: Alexander Krauss, TU Muenchen |
2 Author: Alexander Krauss, TU Muenchen |
3 Author: Brian Huffman, Portland State University |
3 Author: Brian Huffman, Portland State University |
4 Author: Jasmin Blanchette, TU Muenchen |
4 Author: Jasmin Blanchette, TU Muenchen |
5 *) |
5 *) |
6 |
6 |
7 section {* Encoding (almost) everything into natural numbers *} |
7 section \<open>Encoding (almost) everything into natural numbers\<close> |
8 |
8 |
9 theory Countable |
9 theory Countable |
10 imports Old_Datatype Rat Nat_Bijection |
10 imports Old_Datatype Rat Nat_Bijection |
11 begin |
11 begin |
12 |
12 |
13 subsection {* The class of countable types *} |
13 subsection \<open>The class of countable types\<close> |
14 |
14 |
15 class countable = |
15 class countable = |
16 assumes ex_inj: "\<exists>to_nat \<Colon> 'a \<Rightarrow> nat. inj to_nat" |
16 assumes ex_inj: "\<exists>to_nat \<Colon> 'a \<Rightarrow> nat. inj to_nat" |
17 |
17 |
18 lemma countable_classI: |
18 lemma countable_classI: |
189 [rtac @{thm countable_datatype} i, |
189 [rtac @{thm countable_datatype} i, |
190 rtac typedef_thm i, |
190 rtac typedef_thm i, |
191 etac induct_thm' i, |
191 etac induct_thm' i, |
192 REPEAT (resolve_tac ctxt rules i ORELSE atac i)]) 1 |
192 REPEAT (resolve_tac ctxt rules i ORELSE atac i)]) 1 |
193 end) |
193 end) |
194 *} |
194 \<close> |
195 |
195 |
196 hide_const (open) finite_item nth_item |
196 hide_const (open) finite_item nth_item |
197 |
197 |
198 |
198 |
199 subsection {* Automatically proving countability of datatypes *} |
199 subsection \<open>Automatically proving countability of datatypes\<close> |
200 |
200 |
201 ML_file "bnf_lfp_countable.ML" |
201 ML_file "bnf_lfp_countable.ML" |
202 |
202 |
203 ML {* |
203 ML \<open> |
204 fun countable_datatype_tac ctxt st = |
204 fun countable_datatype_tac ctxt st = |
205 (case try (fn () => HEADGOAL (old_countable_datatype_tac ctxt) st) () of |
205 (case try (fn () => HEADGOAL (old_countable_datatype_tac ctxt) st) () of |
206 SOME res => res |
206 SOME res => res |
207 | NONE => BNF_LFP_Countable.countable_datatype_tac ctxt st); |
207 | NONE => BNF_LFP_Countable.countable_datatype_tac ctxt st); |
208 |
208 |
209 (* compatibility *) |
209 (* compatibility *) |
210 fun countable_tac ctxt = |
210 fun countable_tac ctxt = |
211 SELECT_GOAL (countable_datatype_tac ctxt); |
211 SELECT_GOAL (countable_datatype_tac ctxt); |
212 *} |
212 \<close> |
213 |
213 |
214 method_setup countable_datatype = {* |
214 method_setup countable_datatype = \<open> |
215 Scan.succeed (SIMPLE_METHOD o countable_datatype_tac) |
215 Scan.succeed (SIMPLE_METHOD o countable_datatype_tac) |
216 *} "prove countable class instances for datatypes" |
216 \<close> "prove countable class instances for datatypes" |
217 |
217 |
218 |
218 |
219 subsection {* More Countable types *} |
219 subsection \<open>More Countable types\<close> |
220 |
220 |
221 text {* Naturals *} |
221 text \<open>Naturals\<close> |
222 |
222 |
223 instance nat :: countable |
223 instance nat :: countable |
224 by (rule countable_classI [of "id"]) simp |
224 by (rule countable_classI [of "id"]) simp |
225 |
225 |
226 text {* Pairs *} |
226 text \<open>Pairs\<close> |
227 |
227 |
228 instance prod :: (countable, countable) countable |
228 instance prod :: (countable, countable) countable |
229 by (rule countable_classI [of "\<lambda>(x, y). prod_encode (to_nat x, to_nat y)"]) |
229 by (rule countable_classI [of "\<lambda>(x, y). prod_encode (to_nat x, to_nat y)"]) |
230 (auto simp add: prod_encode_eq) |
230 (auto simp add: prod_encode_eq) |
231 |
231 |
232 text {* Sums *} |
232 text \<open>Sums\<close> |
233 |
233 |
234 instance sum :: (countable, countable) countable |
234 instance sum :: (countable, countable) countable |
235 by (rule countable_classI [of "(\<lambda>x. case x of Inl a \<Rightarrow> to_nat (False, to_nat a) |
235 by (rule countable_classI [of "(\<lambda>x. case x of Inl a \<Rightarrow> to_nat (False, to_nat a) |
236 | Inr b \<Rightarrow> to_nat (True, to_nat b))"]) |
236 | Inr b \<Rightarrow> to_nat (True, to_nat b))"]) |
237 (simp split: sum.split_asm) |
237 (simp split: sum.split_asm) |
238 |
238 |
239 text {* Integers *} |
239 text \<open>Integers\<close> |
240 |
240 |
241 instance int :: countable |
241 instance int :: countable |
242 by (rule countable_classI [of int_encode]) (simp add: int_encode_eq) |
242 by (rule countable_classI [of int_encode]) (simp add: int_encode_eq) |
243 |
243 |
244 text {* Options *} |
244 text \<open>Options\<close> |
245 |
245 |
246 instance option :: (countable) countable |
246 instance option :: (countable) countable |
247 by countable_datatype |
247 by countable_datatype |
248 |
248 |
249 text {* Lists *} |
249 text \<open>Lists\<close> |
250 |
250 |
251 instance list :: (countable) countable |
251 instance list :: (countable) countable |
252 by countable_datatype |
252 by countable_datatype |
253 |
253 |
254 text {* String literals *} |
254 text \<open>String literals\<close> |
255 |
255 |
256 instance String.literal :: countable |
256 instance String.literal :: countable |
257 by (rule countable_classI [of "to_nat \<circ> String.explode"]) (auto simp add: explode_inject) |
257 by (rule countable_classI [of "to_nat \<circ> String.explode"]) (auto simp add: explode_inject) |
258 |
258 |
259 text {* Functions *} |
259 text \<open>Functions\<close> |
260 |
260 |
261 instance "fun" :: (finite, countable) countable |
261 instance "fun" :: (finite, countable) countable |
262 proof |
262 proof |
263 obtain xs :: "'a list" where xs: "set xs = UNIV" |
263 obtain xs :: "'a list" where xs: "set xs = UNIV" |
264 using finite_list [OF finite_UNIV] .. |
264 using finite_list [OF finite_UNIV] .. |
267 show "inj (\<lambda>f. to_nat (map f xs))" |
267 show "inj (\<lambda>f. to_nat (map f xs))" |
268 by (rule injI, simp add: xs fun_eq_iff) |
268 by (rule injI, simp add: xs fun_eq_iff) |
269 qed |
269 qed |
270 qed |
270 qed |
271 |
271 |
272 text {* Typereps *} |
272 text \<open>Typereps\<close> |
273 |
273 |
274 instance typerep :: countable |
274 instance typerep :: countable |
275 by countable_datatype |
275 by countable_datatype |
276 |
276 |
277 |
277 |
278 subsection {* The rationals are countably infinite *} |
278 subsection \<open>The rationals are countably infinite\<close> |
279 |
279 |
280 definition nat_to_rat_surj :: "nat \<Rightarrow> rat" where |
280 definition nat_to_rat_surj :: "nat \<Rightarrow> rat" where |
281 "nat_to_rat_surj n = (let (a, b) = prod_decode n in Fract (int_decode a) (int_decode b))" |
281 "nat_to_rat_surj n = (let (a, b) = prod_decode n in Fract (int_decode a) (int_decode b))" |
282 |
282 |
283 lemma surj_nat_to_rat_surj: "surj nat_to_rat_surj" |
283 lemma surj_nat_to_rat_surj: "surj nat_to_rat_surj" |