equal
deleted
inserted
replaced
47 |
47 |
48 instance nat :: countable |
48 instance nat :: countable |
49 by (rule countable_classI [of "id"]) simp |
49 by (rule countable_classI [of "id"]) simp |
50 |
50 |
51 subclass (in finite) countable |
51 subclass (in finite) countable |
52 proof unfold_locales |
52 proof |
53 have "finite (UNIV\<Colon>'a set)" by (rule finite_UNIV) |
53 have "finite (UNIV\<Colon>'a set)" by (rule finite_UNIV) |
54 with finite_conv_nat_seg_image [of UNIV] |
54 with finite_conv_nat_seg_image [of UNIV] |
55 obtain n and f :: "nat \<Rightarrow> 'a" |
55 obtain n and f :: "nat \<Rightarrow> 'a" |
56 where "UNIV = f ` {i. i < n}" by auto |
56 where "UNIV = f ` {i. i < n}" by auto |
57 then have "surj f" unfolding surj_def by auto |
57 then have "surj f" unfolding surj_def by auto |