src/HOL/Library/Countable.thy
author bulwahn
Tue Apr 05 09:38:28 2011 +0200 (2011-04-05)
changeset 42231 bc1891226d00
parent 40702 cf26dd7395e4
child 43534 15df7bc8e93f
permissions -rw-r--r--
removing bounded_forall code equation for characters when loading Code_Char
     1 (*  Title:      HOL/Library/Countable.thy
     2     Author:     Alexander Krauss, TU Muenchen
     3 *)
     4 
     5 header {* Encoding (almost) everything into natural numbers *}
     6 
     7 theory Countable
     8 imports Main Rat Nat_Bijection
     9 begin
    10 
    11 subsection {* The class of countable types *}
    12 
    13 class countable =
    14   assumes ex_inj: "\<exists>to_nat \<Colon> 'a \<Rightarrow> nat. inj to_nat"
    15 
    16 lemma countable_classI:
    17   fixes f :: "'a \<Rightarrow> nat"
    18   assumes "\<And>x y. f x = f y \<Longrightarrow> x = y"
    19   shows "OFCLASS('a, countable_class)"
    20 proof (intro_classes, rule exI)
    21   show "inj f"
    22     by (rule injI [OF assms]) assumption
    23 qed
    24 
    25 
    26 subsection {* Conversion functions *}
    27 
    28 definition to_nat :: "'a\<Colon>countable \<Rightarrow> nat" where
    29   "to_nat = (SOME f. inj f)"
    30 
    31 definition from_nat :: "nat \<Rightarrow> 'a\<Colon>countable" where
    32   "from_nat = inv (to_nat \<Colon> 'a \<Rightarrow> nat)"
    33 
    34 lemma inj_to_nat [simp]: "inj to_nat"
    35   by (rule exE_some [OF ex_inj]) (simp add: to_nat_def)
    36 
    37 lemma surj_from_nat [simp]: "surj from_nat"
    38   unfolding from_nat_def by (simp add: inj_imp_surj_inv)
    39 
    40 lemma to_nat_split [simp]: "to_nat x = to_nat y \<longleftrightarrow> x = y"
    41   using injD [OF inj_to_nat] by auto
    42 
    43 lemma from_nat_to_nat [simp]:
    44   "from_nat (to_nat x) = x"
    45   by (simp add: from_nat_def)
    46 
    47 
    48 subsection {* Countable types *}
    49 
    50 instance nat :: countable
    51   by (rule countable_classI [of "id"]) simp
    52 
    53 subclass (in finite) countable
    54 proof
    55   have "finite (UNIV\<Colon>'a set)" by (rule finite_UNIV)
    56   with finite_conv_nat_seg_image [of "UNIV::'a set"]
    57   obtain n and f :: "nat \<Rightarrow> 'a" 
    58     where "UNIV = f ` {i. i < n}" by auto
    59   then have "surj f" unfolding surj_def by auto
    60   then have "inj (inv f)" by (rule surj_imp_inj_inv)
    61   then show "\<exists>to_nat \<Colon> 'a \<Rightarrow> nat. inj to_nat" by (rule exI[of inj])
    62 qed
    63 
    64 text {* Pairs *}
    65 
    66 instance prod :: (countable, countable) countable
    67   by (rule countable_classI [of "\<lambda>(x, y). prod_encode (to_nat x, to_nat y)"])
    68     (auto simp add: prod_encode_eq)
    69 
    70 
    71 text {* Sums *}
    72 
    73 instance sum :: (countable, countable) countable
    74   by (rule countable_classI [of "(\<lambda>x. case x of Inl a \<Rightarrow> to_nat (False, to_nat a)
    75                                      | Inr b \<Rightarrow> to_nat (True, to_nat b))"])
    76     (simp split: sum.split_asm)
    77 
    78 
    79 text {* Integers *}
    80 
    81 instance int :: countable
    82   by (rule countable_classI [of "int_encode"])
    83     (simp add: int_encode_eq)
    84 
    85 
    86 text {* Options *}
    87 
    88 instance option :: (countable) countable
    89   by (rule countable_classI [of "option_case 0 (Suc \<circ> to_nat)"])
    90     (simp split: option.split_asm)
    91 
    92 
    93 text {* Lists *}
    94 
    95 instance list :: (countable) countable
    96   by (rule countable_classI [of "list_encode \<circ> map to_nat"])
    97     (simp add: list_encode_eq)
    98 
    99 
   100 text {* Further *}
   101 
   102 instance String.literal :: countable
   103   by (rule countable_classI [of "to_nat o explode"])
   104     (auto simp add: explode_inject)
   105 
   106 instantiation typerep :: countable
   107 begin
   108 
   109 fun to_nat_typerep :: "typerep \<Rightarrow> nat" where
   110   "to_nat_typerep (Typerep.Typerep c ts) = to_nat (to_nat c, to_nat (map to_nat_typerep ts))"
   111 
   112 instance proof (rule countable_classI)
   113   fix t t' :: typerep and ts ts' :: "typerep list"
   114   assume "to_nat_typerep t = to_nat_typerep t'"
   115   moreover have "to_nat_typerep t = to_nat_typerep t' \<Longrightarrow> t = t'"
   116     and "map to_nat_typerep ts = map to_nat_typerep ts' \<Longrightarrow> ts = ts'"
   117   proof (induct t and ts arbitrary: t' and ts' rule: typerep.inducts)
   118     case (Typerep c ts t')
   119     then obtain c' ts' where t': "t' = Typerep.Typerep c' ts'" by (cases t') auto
   120     with Typerep have "c = c'" and "ts = ts'" by simp_all
   121     with t' show "Typerep.Typerep c ts = t'" by simp
   122   next
   123     case Nil_typerep then show ?case by simp
   124   next
   125     case (Cons_typerep t ts) then show ?case by auto
   126   qed
   127   ultimately show "t = t'" by simp
   128 qed
   129 
   130 end
   131 
   132 
   133 text {* Functions *}
   134 
   135 instance "fun" :: (finite, countable) countable
   136 proof
   137   obtain xs :: "'a list" where xs: "set xs = UNIV"
   138     using finite_list [OF finite_UNIV] ..
   139   show "\<exists>to_nat::('a \<Rightarrow> 'b) \<Rightarrow> nat. inj to_nat"
   140   proof
   141     show "inj (\<lambda>f. to_nat (map f xs))"
   142       by (rule injI, simp add: xs fun_eq_iff)
   143   qed
   144 qed
   145 
   146 
   147 subsection {* The Rationals are Countably Infinite *}
   148 
   149 definition nat_to_rat_surj :: "nat \<Rightarrow> rat" where
   150 "nat_to_rat_surj n = (let (a,b) = prod_decode n
   151                       in Fract (int_decode a) (int_decode b))"
   152 
   153 lemma surj_nat_to_rat_surj: "surj nat_to_rat_surj"
   154 unfolding surj_def
   155 proof
   156   fix r::rat
   157   show "\<exists>n. r = nat_to_rat_surj n"
   158   proof (cases r)
   159     fix i j assume [simp]: "r = Fract i j" and "j > 0"
   160     have "r = (let m = int_encode i; n = int_encode j
   161                in nat_to_rat_surj(prod_encode (m,n)))"
   162       by (simp add: Let_def nat_to_rat_surj_def)
   163     thus "\<exists>n. r = nat_to_rat_surj n" by(auto simp:Let_def)
   164   qed
   165 qed
   166 
   167 lemma Rats_eq_range_nat_to_rat_surj: "\<rat> = range nat_to_rat_surj"
   168 by (simp add: Rats_def surj_nat_to_rat_surj)
   169 
   170 context field_char_0
   171 begin
   172 
   173 lemma Rats_eq_range_of_rat_o_nat_to_rat_surj:
   174   "\<rat> = range (of_rat o nat_to_rat_surj)"
   175 using surj_nat_to_rat_surj
   176 by (auto simp: Rats_def image_def surj_def)
   177    (blast intro: arg_cong[where f = of_rat])
   178 
   179 lemma surj_of_rat_nat_to_rat_surj:
   180   "r\<in>\<rat> \<Longrightarrow> \<exists>n. r = of_rat(nat_to_rat_surj n)"
   181 by(simp add: Rats_eq_range_of_rat_o_nat_to_rat_surj image_def)
   182 
   183 end
   184 
   185 instance rat :: countable
   186 proof
   187   show "\<exists>to_nat::rat \<Rightarrow> nat. inj to_nat"
   188   proof
   189     have "surj nat_to_rat_surj"
   190       by (rule surj_nat_to_rat_surj)
   191     then show "inj (inv nat_to_rat_surj)"
   192       by (rule surj_imp_inj_inv)
   193   qed
   194 qed
   195 
   196 end