equal
deleted
inserted
replaced
306 *} "prove countable class instances for datatypes" |
306 *} "prove countable class instances for datatypes" |
307 |
307 |
308 hide_const (open) finite_item nth_item |
308 hide_const (open) finite_item nth_item |
309 |
309 |
310 |
310 |
311 (* FIXME |
|
312 subsection {* Countable datatypes *} |
311 subsection {* Countable datatypes *} |
313 |
312 |
|
313 (* TODO: automate *) |
|
314 |
|
315 primrec encode_typerep :: "typerep \<Rightarrow> nat" where |
|
316 "encode_typerep (Typerep.Typerep s ts) = prod_encode (to_nat s, to_nat (map encode_typerep ts))" |
|
317 |
|
318 lemma encode_typerep_injective: "\<forall>u. encode_typerep t = encode_typerep u \<longrightarrow> t = u" |
|
319 apply (induct t) |
|
320 apply (rule allI) |
|
321 apply (case_tac u) |
|
322 apply (auto simp: sum_encode_eq prod_encode_eq elim: list.inj_map_strong[rotated 1]) |
|
323 done |
|
324 |
314 instance typerep :: countable |
325 instance typerep :: countable |
315 by countable_datatype |
326 apply default |
316 *) |
327 apply (unfold inj_on_def ball_UNIV) |
|
328 apply (rule exI) |
|
329 apply (rule allI) |
|
330 apply (rule encode_typerep_injective) |
|
331 done |
317 |
332 |
318 end |
333 end |