equal
deleted
inserted
replaced
32 definition from_nat :: "nat \<Rightarrow> 'a\<Colon>countable" where |
32 definition from_nat :: "nat \<Rightarrow> 'a\<Colon>countable" where |
33 "from_nat = inv (to_nat \<Colon> 'a \<Rightarrow> nat)" |
33 "from_nat = inv (to_nat \<Colon> 'a \<Rightarrow> nat)" |
34 |
34 |
35 lemma inj_to_nat [simp]: "inj to_nat" |
35 lemma inj_to_nat [simp]: "inj to_nat" |
36 by (rule exE_some [OF ex_inj]) (simp add: to_nat_def) |
36 by (rule exE_some [OF ex_inj]) (simp add: to_nat_def) |
|
37 |
|
38 lemma inj_on_to_nat[simp, intro]: "inj_on to_nat S" |
|
39 using inj_to_nat by (auto simp: inj_on_def) |
37 |
40 |
38 lemma surj_from_nat [simp]: "surj from_nat" |
41 lemma surj_from_nat [simp]: "surj from_nat" |
39 unfolding from_nat_def by (simp add: inj_imp_surj_inv) |
42 unfolding from_nat_def by (simp add: inj_imp_surj_inv) |
40 |
43 |
41 lemma to_nat_split [simp]: "to_nat x = to_nat y \<longleftrightarrow> x = y" |
44 lemma to_nat_split [simp]: "to_nat x = to_nat y \<longleftrightarrow> x = y" |