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