# HG changeset patch
# User blanchet
# Date 1409695592 -7200
# Node ID d2cb7cbb3aaaca8078d0d73f0ecc808baf148ca7
# Parent  c376c43c346cc9025224b7b7166b095139e8e342
registered 'typerep' as countable again

diff -r c376c43c346c -r d2cb7cbb3aaa src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Wed Sep 03 00:06:30 2014 +0200
+++ b/src/HOL/Library/Countable.thy	Wed Sep 03 00:06:32 2014 +0200
@@ -308,11 +308,26 @@
 hide_const (open) finite_item nth_item
 
 
-(* FIXME
 subsection {* Countable datatypes *}
 
+(* TODO: automate *)
+
+primrec encode_typerep :: "typerep \<Rightarrow> nat" where
+  "encode_typerep (Typerep.Typerep s ts) = prod_encode (to_nat s, to_nat (map encode_typerep ts))"
+
+lemma encode_typerep_injective: "\<forall>u. encode_typerep t = encode_typerep u \<longrightarrow> t = u"
+  apply (induct t)
+  apply (rule allI)
+  apply (case_tac u)
+  apply (auto simp: sum_encode_eq prod_encode_eq elim: list.inj_map_strong[rotated 1])
+  done
+
 instance typerep :: countable
-  by countable_datatype
-*)
+  apply default
+  apply (unfold inj_on_def ball_UNIV)
+  apply (rule exI)
+  apply (rule allI)
+  apply (rule encode_typerep_injective)
+  done
 
 end