src/HOL/Library/Countable.thy
author chaieb
Mon Feb 09 17:21:46 2009 +0000 (2009-02-09)
changeset 29847 af32126ee729
parent 29797 08ef36ed2f8a
child 29880 3dee8ff45d3d
permissions -rw-r--r--
added Determinants to Library
     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 Plain "~~/src/HOL/List" "~~/src/HOL/Hilbert_Choice"
     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 to_nat_split [simp]: "to_nat x = to_nat y \<longleftrightarrow> x = y"
    38   using injD [OF inj_to_nat] by auto
    39 
    40 lemma from_nat_to_nat [simp]:
    41   "from_nat (to_nat x) = x"
    42   by (simp add: from_nat_def)
    43 
    44 
    45 subsection {* Countable types *}
    46 
    47 instance nat :: countable
    48   by (rule countable_classI [of "id"]) simp 
    49 
    50 subclass (in finite) countable
    51 proof
    52   have "finite (UNIV\<Colon>'a set)" by (rule finite_UNIV)
    53   with finite_conv_nat_seg_image [of UNIV]
    54   obtain n and f :: "nat \<Rightarrow> 'a" 
    55     where "UNIV = f ` {i. i < n}" by auto
    56   then have "surj f" unfolding surj_def by auto
    57   then have "inj (inv f)" by (rule surj_imp_inj_inv)
    58   then show "\<exists>to_nat \<Colon> 'a \<Rightarrow> nat. inj to_nat" by (rule exI[of inj])
    59 qed
    60 
    61 text {* Pairs *}
    62 
    63 primrec sum :: "nat \<Rightarrow> nat"
    64 where
    65   "sum 0 = 0"
    66 | "sum (Suc n) = Suc n + sum n"
    67 
    68 lemma sum_arith: "sum n = n * Suc n div 2"
    69   by (induct n) auto
    70 
    71 lemma sum_mono: "n \<ge> m \<Longrightarrow> sum n \<ge> sum m"
    72   by (induct n m rule: diff_induct) auto
    73 
    74 definition
    75   "pair_encode = (\<lambda>(m, n). sum (m + n) + m)"
    76 
    77 lemma inj_pair_cencode: "inj pair_encode"
    78   unfolding pair_encode_def
    79 proof (rule injI, simp only: split_paired_all split_conv)
    80   fix a b c d
    81   assume eq: "sum (a + b) + a = sum (c + d) + c"
    82   have "a + b = c + d \<or> a + b \<ge> Suc (c + d) \<or> c + d \<ge> Suc (a + b)" by arith
    83   then
    84   show "(a, b) = (c, d)"
    85   proof (elim disjE)
    86     assume sumeq: "a + b = c + d"
    87     then have "a = c" using eq by auto
    88     moreover from sumeq this have "b = d" by auto
    89     ultimately show ?thesis by simp
    90   next
    91     assume "a + b \<ge> Suc (c + d)"
    92     from sum_mono[OF this] eq
    93     show ?thesis by auto
    94   next
    95     assume "c + d \<ge> Suc (a + b)"
    96     from sum_mono[OF this] eq
    97     show ?thesis by auto
    98   qed
    99 qed
   100 
   101 instance "*" :: (countable, countable) countable
   102 by (rule countable_classI [of "\<lambda>(x, y). pair_encode (to_nat x, to_nat y)"])
   103   (auto dest: injD [OF inj_pair_cencode] injD [OF inj_to_nat])
   104 
   105 
   106 text {* Sums *}
   107 
   108 instance "+":: (countable, countable) countable
   109   by (rule countable_classI [of "(\<lambda>x. case x of Inl a \<Rightarrow> to_nat (False, to_nat a)
   110                                      | Inr b \<Rightarrow> to_nat (True, to_nat b))"])
   111     (auto split:sum.splits)
   112 
   113 
   114 text {* Integers *}
   115 
   116 lemma int_cases: "(i::int) = 0 \<or> i < 0 \<or> i > 0"
   117 by presburger
   118 
   119 lemma int_pos_neg_zero:
   120   obtains (zero) "(z::int) = 0" "sgn z = 0" "abs z = 0"
   121   | (pos) n where "z = of_nat n" "sgn z = 1" "abs z = of_nat n"
   122   | (neg) n where "z = - (of_nat n)" "sgn z = -1" "abs z = of_nat n"
   123 apply atomize_elim
   124 apply (insert int_cases[of z])
   125 apply (auto simp:zsgn_def)
   126 apply (rule_tac x="nat (-z)" in exI, simp)
   127 apply (rule_tac x="nat z" in exI, simp)
   128 done
   129 
   130 instance int :: countable
   131 proof (rule countable_classI [of "(\<lambda>i. to_nat (nat (sgn i + 1), nat (abs i)))"], 
   132     auto dest: injD [OF inj_to_nat])
   133   fix x y 
   134   assume a: "nat (sgn x + 1) = nat (sgn y + 1)" "nat (abs x) = nat (abs y)"
   135   show "x = y"
   136   proof (cases rule: int_pos_neg_zero[of x])
   137     case zero 
   138     with a show "x = y" by (cases rule: int_pos_neg_zero[of y]) auto
   139   next
   140     case (pos n)
   141     with a show "x = y" by (cases rule: int_pos_neg_zero[of y]) auto
   142   next
   143     case (neg n)
   144     with a show "x = y" by (cases rule: int_pos_neg_zero[of y]) auto
   145   qed
   146 qed
   147 
   148 
   149 text {* Options *}
   150 
   151 instance option :: (countable) countable
   152 by (rule countable_classI[of "\<lambda>x. case x of None \<Rightarrow> 0
   153                                      | Some y \<Rightarrow> Suc (to_nat y)"])
   154  (auto split:option.splits)
   155 
   156 
   157 text {* Lists *}
   158 
   159 lemma from_nat_to_nat_map [simp]: "map from_nat (map to_nat xs) = xs"
   160   by (simp add: comp_def map_compose [symmetric])
   161 
   162 primrec
   163   list_encode :: "'a\<Colon>countable list \<Rightarrow> nat"
   164 where
   165   "list_encode [] = 0"
   166 | "list_encode (x#xs) = Suc (to_nat (x, list_encode xs))"
   167 
   168 instance list :: (countable) countable
   169 proof (rule countable_classI [of "list_encode"])
   170   fix xs ys :: "'a list"
   171   assume cenc: "list_encode xs = list_encode ys"
   172   then show "xs = ys"
   173   proof (induct xs arbitrary: ys)
   174     case (Nil ys)
   175     with cenc show ?case by (cases ys, auto)
   176   next
   177     case (Cons x xs' ys)
   178     thus ?case by (cases ys) auto
   179   qed
   180 qed
   181 
   182 
   183 text {* Functions *}
   184 
   185 instance "fun" :: (finite, countable) countable
   186 proof
   187   obtain xs :: "'a list" where xs: "set xs = UNIV"
   188     using finite_list [OF finite_UNIV] ..
   189   show "\<exists>to_nat::('a \<Rightarrow> 'b) \<Rightarrow> nat. inj to_nat"
   190   proof
   191     show "inj (\<lambda>f. to_nat (map f xs))"
   192       by (rule injI, simp add: xs expand_fun_eq)
   193   qed
   194 qed
   195 
   196 end