# HG changeset patch
# User huffman
# Date 1234638635 28800
# Node ID 623c9c20966b30917679976d1e4590656bda51eb
# Parent  9433df0998485b7a553c28afcf331baa6bd02c0b
add lemma surj_from_nat

diff -r 9433df099848 -r 623c9c20966b src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Sat Feb 14 06:53:28 2009 -0800
+++ b/src/HOL/Library/Countable.thy	Sat Feb 14 11:10:35 2009 -0800
@@ -39,6 +39,9 @@
 lemma inj_to_nat [simp]: "inj to_nat"
   by (rule exE_some [OF ex_inj]) (simp add: to_nat_def)
 
+lemma surj_from_nat [simp]: "surj from_nat"
+  unfolding from_nat_def by (simp add: inj_imp_surj_inv)
+
 lemma to_nat_split [simp]: "to_nat x = to_nat y \<longleftrightarrow> x = y"
   using injD [OF inj_to_nat] by auto