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