# HG changeset patch
# User hoelzl
# Date 1311788100 -7200
# Node ID c38c65a1bf9c8d2d383786a2c33f949e580fed80
# Parent  f4a7697011c587ef27361c1e078d21c254fdf0bf
to_nat is injective on arbitrary domains

diff -r f4a7697011c5 -r c38c65a1bf9c src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Wed Jul 27 19:34:30 2011 +0200
+++ b/src/HOL/Library/Countable.thy	Wed Jul 27 19:35:00 2011 +0200
@@ -35,6 +35,9 @@
 lemma inj_to_nat [simp]: "inj to_nat"
   by (rule exE_some [OF ex_inj]) (simp add: to_nat_def)
 
+lemma inj_on_to_nat[simp, intro]: "inj_on to_nat S"
+  using inj_to_nat by (auto simp: inj_on_def)
+
 lemma surj_from_nat [simp]: "surj from_nat"
   unfolding from_nat_def by (simp add: inj_imp_surj_inv)