# HG changeset patch
# User haftmann
# Date 1277908093 -7200
# Node ID 6aa09d2a6cf9b8bffc46084db111b2abaeb0493e
# Parent  62fc163419229c06785aed8c42efd7a0a8bfa075
added literal and typerep instances

diff -r 62fc16341922 -r 6aa09d2a6cf9 src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Wed Jun 30 12:20:45 2010 +0200
+++ b/src/HOL/Library/Countable.thy	Wed Jun 30 16:28:13 2010 +0200
@@ -97,6 +97,45 @@
     (simp add: list_encode_eq)
 
 
+text {* Further *}
+
+instance String.literal :: countable
+  by (rule countable_classI [of "String.literal_case to_nat"])
+   (auto split: String.literal.splits)
+
+instantiation typerep :: countable
+begin
+
+fun to_nat_typerep :: "typerep \<Rightarrow> nat" where
+  "to_nat_typerep (Typerep.Typerep c ts) = to_nat (to_nat c, to_nat (map to_nat_typerep ts))"
+
+instance proof (rule countable_classI)
+  fix t t' :: typerep and ts
+  have "(\<forall>t'. to_nat_typerep t = to_nat_typerep t' \<longrightarrow> t = t')
+    \<and> (\<forall>ts'. map to_nat_typerep ts = map to_nat_typerep ts' \<longrightarrow> ts = ts')"
+  proof (induct rule: typerep.induct)
+    case (Typerep c ts) show ?case
+    proof (rule allI, rule impI)
+      fix t'
+      assume hyp: "to_nat_typerep (Typerep.Typerep c ts) = to_nat_typerep t'"
+      then obtain c' ts' where t': "t' = (Typerep.Typerep c' ts')"
+        by (cases t') auto
+      with Typerep hyp have "c = c'" and "ts = ts'" by simp_all
+      with t' show "Typerep.Typerep c ts = t'" by simp
+    qed
+  next
+    case Nil_typerep then show ?case by simp
+  next
+    case (Cons_typerep t ts) then show ?case by auto
+  qed
+  then have "to_nat_typerep t = to_nat_typerep t' \<Longrightarrow> t = t'" by auto
+  moreover assume "to_nat_typerep t = to_nat_typerep t'"
+  ultimately show "t = t'" by simp
+qed
+
+end
+
+
 text {* Functions *}
 
 instance "fun" :: (finite, countable) countable