src/HOL/Library/Countable.thy
author blanchet
Wed Sep 03 00:06:27 2014 +0200 (2014-09-03)
changeset 58155 14dda84afbb3
parent 58112 8081087096ad
child 58158 d2cb7cbb3aaa
permissions -rw-r--r--
commented out failing tactic (now that 'typerep' is defined using the new package
     1 (*  Title:      HOL/Library/Countable.thy
     2     Author:     Alexander Krauss, TU Muenchen
     3     Author:     Brian Huffman, Portland State University
     4 *)
     5 
     6 header {* Encoding (almost) everything into natural numbers *}
     7 
     8 theory Countable
     9 imports Main Rat Nat_Bijection
    10 begin
    11 
    12 subsection {* The class of countable types *}
    13 
    14 class countable =
    15   assumes ex_inj: "\<exists>to_nat \<Colon> 'a \<Rightarrow> nat. inj to_nat"
    16 
    17 lemma countable_classI:
    18   fixes f :: "'a \<Rightarrow> nat"
    19   assumes "\<And>x y. f x = f y \<Longrightarrow> x = y"
    20   shows "OFCLASS('a, countable_class)"
    21 proof (intro_classes, rule exI)
    22   show "inj f"
    23     by (rule injI [OF assms]) assumption
    24 qed
    25 
    26 
    27 subsection {* Conversion functions *}
    28 
    29 definition to_nat :: "'a\<Colon>countable \<Rightarrow> nat" where
    30   "to_nat = (SOME f. inj f)"
    31 
    32 definition from_nat :: "nat \<Rightarrow> 'a\<Colon>countable" where
    33   "from_nat = inv (to_nat \<Colon> 'a \<Rightarrow> nat)"
    34 
    35 lemma inj_to_nat [simp]: "inj to_nat"
    36   by (rule exE_some [OF ex_inj]) (simp add: to_nat_def)
    37 
    38 lemma inj_on_to_nat[simp, intro]: "inj_on to_nat S"
    39   using inj_to_nat by (auto simp: inj_on_def)
    40 
    41 lemma surj_from_nat [simp]: "surj from_nat"
    42   unfolding from_nat_def by (simp add: inj_imp_surj_inv)
    43 
    44 lemma to_nat_split [simp]: "to_nat x = to_nat y \<longleftrightarrow> x = y"
    45   using injD [OF inj_to_nat] by auto
    46 
    47 lemma from_nat_to_nat [simp]:
    48   "from_nat (to_nat x) = x"
    49   by (simp add: from_nat_def)
    50 
    51 
    52 subsection {* Countable types *}
    53 
    54 instance nat :: countable
    55   by (rule countable_classI [of "id"]) simp
    56 
    57 subclass (in finite) countable
    58 proof
    59   have "finite (UNIV\<Colon>'a set)" by (rule finite_UNIV)
    60   with finite_conv_nat_seg_image [of "UNIV::'a set"]
    61   obtain n and f :: "nat \<Rightarrow> 'a" 
    62     where "UNIV = f ` {i. i < n}" by auto
    63   then have "surj f" unfolding surj_def by auto
    64   then have "inj (inv f)" by (rule surj_imp_inj_inv)
    65   then show "\<exists>to_nat \<Colon> 'a \<Rightarrow> nat. inj to_nat" by (rule exI[of inj])
    66 qed
    67 
    68 text {* Pairs *}
    69 
    70 instance prod :: (countable, countable) countable
    71   by (rule countable_classI [of "\<lambda>(x, y). prod_encode (to_nat x, to_nat y)"])
    72     (auto simp add: prod_encode_eq)
    73 
    74 
    75 text {* Sums *}
    76 
    77 instance sum :: (countable, countable) countable
    78   by (rule countable_classI [of "(\<lambda>x. case x of Inl a \<Rightarrow> to_nat (False, to_nat a)
    79                                      | Inr b \<Rightarrow> to_nat (True, to_nat b))"])
    80     (simp split: sum.split_asm)
    81 
    82 
    83 text {* Integers *}
    84 
    85 instance int :: countable
    86   by (rule countable_classI [of "int_encode"])
    87     (simp add: int_encode_eq)
    88 
    89 
    90 text {* Options *}
    91 
    92 instance option :: (countable) countable
    93   by (rule countable_classI [of "case_option 0 (Suc \<circ> to_nat)"])
    94     (simp split: option.split_asm)
    95 
    96 
    97 text {* Lists *}
    98 
    99 instance list :: (countable) countable
   100   by (rule countable_classI [of "list_encode \<circ> map to_nat"])
   101     (simp add: list_encode_eq)
   102 
   103 
   104 text {* Further *}
   105 
   106 instance String.literal :: countable
   107   by (rule countable_classI [of "to_nat o String.explode"])
   108     (auto simp add: explode_inject)
   109 
   110 text {* Functions *}
   111 
   112 instance "fun" :: (finite, countable) countable
   113 proof
   114   obtain xs :: "'a list" where xs: "set xs = UNIV"
   115     using finite_list [OF finite_UNIV] ..
   116   show "\<exists>to_nat::('a \<Rightarrow> 'b) \<Rightarrow> nat. inj to_nat"
   117   proof
   118     show "inj (\<lambda>f. to_nat (map f xs))"
   119       by (rule injI, simp add: xs fun_eq_iff)
   120   qed
   121 qed
   122 
   123 
   124 subsection {* The Rationals are Countably Infinite *}
   125 
   126 definition nat_to_rat_surj :: "nat \<Rightarrow> rat" where
   127 "nat_to_rat_surj n = (let (a,b) = prod_decode n
   128                       in Fract (int_decode a) (int_decode b))"
   129 
   130 lemma surj_nat_to_rat_surj: "surj nat_to_rat_surj"
   131 unfolding surj_def
   132 proof
   133   fix r::rat
   134   show "\<exists>n. r = nat_to_rat_surj n"
   135   proof (cases r)
   136     fix i j assume [simp]: "r = Fract i j" and "j > 0"
   137     have "r = (let m = int_encode i; n = int_encode j
   138                in nat_to_rat_surj(prod_encode (m,n)))"
   139       by (simp add: Let_def nat_to_rat_surj_def)
   140     thus "\<exists>n. r = nat_to_rat_surj n" by(auto simp:Let_def)
   141   qed
   142 qed
   143 
   144 lemma Rats_eq_range_nat_to_rat_surj: "\<rat> = range nat_to_rat_surj"
   145 by (simp add: Rats_def surj_nat_to_rat_surj)
   146 
   147 context field_char_0
   148 begin
   149 
   150 lemma Rats_eq_range_of_rat_o_nat_to_rat_surj:
   151   "\<rat> = range (of_rat o nat_to_rat_surj)"
   152 using surj_nat_to_rat_surj
   153 by (auto simp: Rats_def image_def surj_def)
   154    (blast intro: arg_cong[where f = of_rat])
   155 
   156 lemma surj_of_rat_nat_to_rat_surj:
   157   "r\<in>\<rat> \<Longrightarrow> \<exists>n. r = of_rat(nat_to_rat_surj n)"
   158 by(simp add: Rats_eq_range_of_rat_o_nat_to_rat_surj image_def)
   159 
   160 end
   161 
   162 instance rat :: countable
   163 proof
   164   show "\<exists>to_nat::rat \<Rightarrow> nat. inj to_nat"
   165   proof
   166     have "surj nat_to_rat_surj"
   167       by (rule surj_nat_to_rat_surj)
   168     then show "inj (inv nat_to_rat_surj)"
   169       by (rule surj_imp_inj_inv)
   170   qed
   171 qed
   172 
   173 
   174 subsection {* Automatically proving countability of datatypes *}
   175 
   176 inductive finite_item :: "'a Old_Datatype.item \<Rightarrow> bool" where
   177   undefined: "finite_item undefined"
   178 | In0: "finite_item x \<Longrightarrow> finite_item (Old_Datatype.In0 x)"
   179 | In1: "finite_item x \<Longrightarrow> finite_item (Old_Datatype.In1 x)"
   180 | Leaf: "finite_item (Old_Datatype.Leaf a)"
   181 | Scons: "\<lbrakk>finite_item x; finite_item y\<rbrakk> \<Longrightarrow> finite_item (Old_Datatype.Scons x y)"
   182 
   183 function
   184   nth_item :: "nat \<Rightarrow> ('a::countable) Old_Datatype.item"
   185 where
   186   "nth_item 0 = undefined"
   187 | "nth_item (Suc n) =
   188   (case sum_decode n of
   189     Inl i \<Rightarrow>
   190     (case sum_decode i of
   191       Inl j \<Rightarrow> Old_Datatype.In0 (nth_item j)
   192     | Inr j \<Rightarrow> Old_Datatype.In1 (nth_item j))
   193   | Inr i \<Rightarrow>
   194     (case sum_decode i of
   195       Inl j \<Rightarrow> Old_Datatype.Leaf (from_nat j)
   196     | Inr j \<Rightarrow>
   197       (case prod_decode j of
   198         (a, b) \<Rightarrow> Old_Datatype.Scons (nth_item a) (nth_item b))))"
   199 by pat_completeness auto
   200 
   201 lemma le_sum_encode_Inl: "x \<le> y \<Longrightarrow> x \<le> sum_encode (Inl y)"
   202 unfolding sum_encode_def by simp
   203 
   204 lemma le_sum_encode_Inr: "x \<le> y \<Longrightarrow> x \<le> sum_encode (Inr y)"
   205 unfolding sum_encode_def by simp
   206 
   207 termination
   208 by (relation "measure id")
   209   (auto simp add: sum_encode_eq [symmetric] prod_encode_eq [symmetric]
   210     le_imp_less_Suc le_sum_encode_Inl le_sum_encode_Inr
   211     le_prod_encode_1 le_prod_encode_2)
   212 
   213 lemma nth_item_covers: "finite_item x \<Longrightarrow> \<exists>n. nth_item n = x"
   214 proof (induct set: finite_item)
   215   case undefined
   216   have "nth_item 0 = undefined" by simp
   217   thus ?case ..
   218 next
   219   case (In0 x)
   220   then obtain n where "nth_item n = x" by fast
   221   hence "nth_item (Suc (sum_encode (Inl (sum_encode (Inl n))))) = Old_Datatype.In0 x" by simp
   222   thus ?case ..
   223 next
   224   case (In1 x)
   225   then obtain n where "nth_item n = x" by fast
   226   hence "nth_item (Suc (sum_encode (Inl (sum_encode (Inr n))))) = Old_Datatype.In1 x" by simp
   227   thus ?case ..
   228 next
   229   case (Leaf a)
   230   have "nth_item (Suc (sum_encode (Inr (sum_encode (Inl (to_nat a)))))) = Old_Datatype.Leaf a"
   231     by simp
   232   thus ?case ..
   233 next
   234   case (Scons x y)
   235   then obtain i j where "nth_item i = x" and "nth_item j = y" by fast
   236   hence "nth_item
   237     (Suc (sum_encode (Inr (sum_encode (Inr (prod_encode (i, j))))))) = Old_Datatype.Scons x y"
   238     by simp
   239   thus ?case ..
   240 qed
   241 
   242 theorem countable_datatype:
   243   fixes Rep :: "'b \<Rightarrow> ('a::countable) Old_Datatype.item"
   244   fixes Abs :: "('a::countable) Old_Datatype.item \<Rightarrow> 'b"
   245   fixes rep_set :: "('a::countable) Old_Datatype.item \<Rightarrow> bool"
   246   assumes type: "type_definition Rep Abs (Collect rep_set)"
   247   assumes finite_item: "\<And>x. rep_set x \<Longrightarrow> finite_item x"
   248   shows "OFCLASS('b, countable_class)"
   249 proof
   250   def f \<equiv> "\<lambda>y. LEAST n. nth_item n = Rep y"
   251   {
   252     fix y :: 'b
   253     have "rep_set (Rep y)"
   254       using type_definition.Rep [OF type] by simp
   255     hence "finite_item (Rep y)"
   256       by (rule finite_item)
   257     hence "\<exists>n. nth_item n = Rep y"
   258       by (rule nth_item_covers)
   259     hence "nth_item (f y) = Rep y"
   260       unfolding f_def by (rule LeastI_ex)
   261     hence "Abs (nth_item (f y)) = y"
   262       using type_definition.Rep_inverse [OF type] by simp
   263   }
   264   hence "inj f"
   265     by (rule inj_on_inverseI)
   266   thus "\<exists>f::'b \<Rightarrow> nat. inj f"
   267     by - (rule exI)
   268 qed
   269 
   270 ML {*
   271   fun countable_tac ctxt =
   272     SUBGOAL (fn (goal, i) =>
   273       let
   274         val ty_name =
   275           (case goal of
   276             (_ $ Const (@{const_name Pure.type}, Type (@{type_name itself}, [Type (n, _)]))) => n
   277           | _ => raise Match)
   278         val typedef_info = hd (Typedef.get_info ctxt ty_name)
   279         val typedef_thm = #type_definition (snd typedef_info)
   280         val pred_name =
   281           (case HOLogic.dest_Trueprop (concl_of typedef_thm) of
   282             (typedef $ rep $ abs $ (collect $ Const (n, _))) => n
   283           | _ => raise Match)
   284         val induct_info = Inductive.the_inductive ctxt pred_name
   285         val pred_names = #names (fst induct_info)
   286         val induct_thms = #inducts (snd induct_info)
   287         val alist = pred_names ~~ induct_thms
   288         val induct_thm = the (AList.lookup (op =) alist pred_name)
   289         val vars = rev (Term.add_vars (Thm.prop_of induct_thm) [])
   290         val thy = Proof_Context.theory_of ctxt
   291         val insts = vars |> map (fn (_, T) => try (Thm.cterm_of thy)
   292           (Const (@{const_name Countable.finite_item}, T)))
   293         val induct_thm' = Drule.instantiate' [] insts induct_thm
   294         val rules = @{thms finite_item.intros}
   295       in
   296         SOLVED' (fn i => EVERY
   297           [rtac @{thm countable_datatype} i,
   298            rtac typedef_thm i,
   299            etac induct_thm' i,
   300            REPEAT (resolve_tac rules i ORELSE atac i)]) 1
   301       end)
   302 *}
   303 
   304 method_setup countable_datatype = {*
   305   Scan.succeed (fn ctxt => SIMPLE_METHOD' (countable_tac ctxt))
   306 *} "prove countable class instances for datatypes"
   307 
   308 hide_const (open) finite_item nth_item
   309 
   310 
   311 (* FIXME
   312 subsection {* Countable datatypes *}
   313 
   314 instance typerep :: countable
   315   by countable_datatype
   316 *)
   317 
   318 end