summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | huffman |

Mon, 10 Mar 2008 18:44:20 +0100 | |

changeset 26243 | 69592314f977 |

parent 26242 | d64510d3c7b7 |

child 26244 | 0686a953b873 |

instance fun :: (finite, countable) countable

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