src/HOL/Library/Countable.thy
changeset 61076 bdc1e2f0a86a
parent 60801 7664e0916eec
child 61115 3a4400985780
     1.1 --- a/src/HOL/Library/Countable.thy	Tue Sep 01 17:25:36 2015 +0200
     1.2 +++ b/src/HOL/Library/Countable.thy	Tue Sep 01 22:32:58 2015 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  subsection \<open>The class of countable types\<close>
     1.5  
     1.6  class countable =
     1.7 -  assumes ex_inj: "\<exists>to_nat \<Colon> 'a \<Rightarrow> nat. inj to_nat"
     1.8 +  assumes ex_inj: "\<exists>to_nat :: 'a \<Rightarrow> nat. inj to_nat"
     1.9  
    1.10  lemma countable_classI:
    1.11    fixes f :: "'a \<Rightarrow> nat"
    1.12 @@ -27,11 +27,11 @@
    1.13  
    1.14  subsection \<open>Conversion functions\<close>
    1.15  
    1.16 -definition to_nat :: "'a\<Colon>countable \<Rightarrow> nat" where
    1.17 +definition to_nat :: "'a::countable \<Rightarrow> nat" where
    1.18    "to_nat = (SOME f. inj f)"
    1.19  
    1.20 -definition from_nat :: "nat \<Rightarrow> 'a\<Colon>countable" where
    1.21 -  "from_nat = inv (to_nat \<Colon> 'a \<Rightarrow> nat)"
    1.22 +definition from_nat :: "nat \<Rightarrow> 'a::countable" where
    1.23 +  "from_nat = inv (to_nat :: 'a \<Rightarrow> nat)"
    1.24  
    1.25  lemma inj_to_nat [simp]: "inj to_nat"
    1.26    by (rule exE_some [OF ex_inj]) (simp add: to_nat_def)
    1.27 @@ -54,13 +54,13 @@
    1.28  
    1.29  subclass (in finite) countable
    1.30  proof
    1.31 -  have "finite (UNIV\<Colon>'a set)" by (rule finite_UNIV)
    1.32 +  have "finite (UNIV::'a set)" by (rule finite_UNIV)
    1.33    with finite_conv_nat_seg_image [of "UNIV::'a set"]
    1.34    obtain n and f :: "nat \<Rightarrow> 'a" 
    1.35      where "UNIV = f ` {i. i < n}" by auto
    1.36    then have "surj f" unfolding surj_def by auto
    1.37    then have "inj (inv f)" by (rule surj_imp_inj_inv)
    1.38 -  then show "\<exists>to_nat \<Colon> 'a \<Rightarrow> nat. inj to_nat" by (rule exI[of inj])
    1.39 +  then show "\<exists>to_nat :: 'a \<Rightarrow> nat. inj to_nat" by (rule exI[of inj])
    1.40  qed
    1.41  
    1.42