author | hoelzl |
Wed, 27 Jul 2011 19:35:00 +0200 | |
changeset 44863 | c38c65a1bf9c |
parent 44862 | f4a7697011c5 |
child 44864 | b141d7a3d4e3 |
1.1 --- a/src/HOL/Library/Countable.thy Wed Jul 27 19:34:30 2011 +0200 1.2 +++ b/src/HOL/Library/Countable.thy Wed Jul 27 19:35:00 2011 +0200 1.3 @@ -35,6 +35,9 @@ 1.4 lemma inj_to_nat [simp]: "inj to_nat" 1.5 by (rule exE_some [OF ex_inj]) (simp add: to_nat_def) 1.6 1.7 +lemma inj_on_to_nat[simp, intro]: "inj_on to_nat S" 1.8 + using inj_to_nat by (auto simp: inj_on_def) 1.9 + 1.10 lemma surj_from_nat [simp]: "surj from_nat" 1.11 unfolding from_nat_def by (simp add: inj_imp_surj_inv) 1.12