summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Library/Countable.thy

changeset 26243 | 69592314f977 |

parent 26169 | 73027318f9ba |

child 26350 | a170a190c5d3 |

--- 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