# HG changeset patch
# User huffman
# Date 1205171060 -3600
# Node ID 69592314f9773bdd320e24e7b22004c8a37708e3
# Parent  d64510d3c7b7336f1d68f2476b65bce3c7471d32
instance fun :: (finite, countable) countable

diff -r d64510d3c7b7 -r 69592314f977 src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Sun Mar 09 07:57:30 2008 +0100
+++ b/src/HOL/Library/Countable.thy	Mon Mar 10 18:44:20 2008 +0100
@@ -180,4 +180,18 @@
   qed
 qed
 
+
+text {* Functions *}
+
+instance "fun" :: (finite, countable) countable
+proof
+  obtain xs :: "'a list" where xs: "set xs = UNIV"
+    using finite_list [OF finite_UNIV] ..
+  show "\<exists>to_nat::('a \<Rightarrow> 'b) \<Rightarrow> nat. inj to_nat"
+  proof
+    show "inj (\<lambda>f. to_nat (map f xs))"
+      by (rule injI, simp add: xs expand_fun_eq)
+  qed
+qed
+
 end