# HG changeset patch # User huffman # Date 1308848836 25200 # Node ID 15df7bc8e93fa8b76328e783b08c7f971a7d8ab2 # Parent d32d72ea3215075b24445353a3bacf20d900c55c add countable_datatype method for proving countable class instances diff -r d32d72ea3215 -r 15df7bc8e93f src/HOL/Library/Countable.thy --- a/src/HOL/Library/Countable.thy Thu Jun 23 09:16:48 2011 -0700 +++ b/src/HOL/Library/Countable.thy Thu Jun 23 10:07:16 2011 -0700 @@ -1,5 +1,6 @@ (* Title: HOL/Library/Countable.thy Author: Alexander Krauss, TU Muenchen + Author: Brian Huffman, Portland State University *) header {* Encoding (almost) everything into natural numbers *} @@ -103,33 +104,6 @@ by (rule countable_classI [of "to_nat o explode"]) (auto simp add: explode_inject) -instantiation typerep :: countable -begin - -fun to_nat_typerep :: "typerep \ nat" where - "to_nat_typerep (Typerep.Typerep c ts) = to_nat (to_nat c, to_nat (map to_nat_typerep ts))" - -instance proof (rule countable_classI) - fix t t' :: typerep and ts ts' :: "typerep list" - assume "to_nat_typerep t = to_nat_typerep t'" - moreover have "to_nat_typerep t = to_nat_typerep t' \ t = t'" - and "map to_nat_typerep ts = map to_nat_typerep ts' \ ts = ts'" - proof (induct t and ts arbitrary: t' and ts' rule: typerep.inducts) - case (Typerep c ts t') - then obtain c' ts' where t': "t' = Typerep.Typerep c' ts'" by (cases t') auto - with Typerep have "c = c'" and "ts = ts'" by simp_all - with t' show "Typerep.Typerep c ts = t'" by simp - next - case Nil_typerep then show ?case by simp - next - case (Cons_typerep t ts) then show ?case by auto - qed - ultimately show "t = t'" by simp -qed - -end - - text {* Functions *} instance "fun" :: (finite, countable) countable @@ -193,4 +167,144 @@ qed qed + +subsection {* Automatically proving countability of datatypes *} + +inductive finite_item :: "'a Datatype.item \ bool" where + undefined: "finite_item undefined" +| In0: "finite_item x \ finite_item (Datatype.In0 x)" +| In1: "finite_item x \ finite_item (Datatype.In1 x)" +| Leaf: "finite_item (Datatype.Leaf a)" +| Scons: "\finite_item x; finite_item y\ \ finite_item (Datatype.Scons x y)" + +function + nth_item :: "nat \ ('a::countable) Datatype.item" +where + "nth_item 0 = undefined" +| "nth_item (Suc n) = + (case sum_decode n of + Inl i \ + (case sum_decode i of + Inl j \ Datatype.In0 (nth_item j) + | Inr j \ Datatype.In1 (nth_item j)) + | Inr i \ + (case sum_decode i of + Inl j \ Datatype.Leaf (from_nat j) + | Inr j \ + (case prod_decode j of + (a, b) \ Datatype.Scons (nth_item a) (nth_item b))))" +by pat_completeness auto + +lemma le_sum_encode_Inl: "x \ y \ x \ sum_encode (Inl y)" +unfolding sum_encode_def by simp + +lemma le_sum_encode_Inr: "x \ y \ x \ sum_encode (Inr y)" +unfolding sum_encode_def by simp + +termination +by (relation "measure id") + (auto simp add: sum_encode_eq [symmetric] prod_encode_eq [symmetric] + le_imp_less_Suc le_sum_encode_Inl le_sum_encode_Inr + le_prod_encode_1 le_prod_encode_2) + +lemma nth_item_covers: "finite_item x \ \n. nth_item n = x" +proof (induct set: finite_item) + case undefined + have "nth_item 0 = undefined" by simp + thus ?case .. +next + case (In0 x) + then obtain n where "nth_item n = x" by fast + hence "nth_item (Suc (sum_encode (Inl (sum_encode (Inl n))))) + = Datatype.In0 x" by simp + thus ?case .. +next + case (In1 x) + then obtain n where "nth_item n = x" by fast + hence "nth_item (Suc (sum_encode (Inl (sum_encode (Inr n))))) + = Datatype.In1 x" by simp + thus ?case .. +next + case (Leaf a) + have "nth_item (Suc (sum_encode (Inr (sum_encode (Inl (to_nat a)))))) + = Datatype.Leaf a" by simp + thus ?case .. +next + case (Scons x y) + then obtain i j where "nth_item i = x" and "nth_item j = y" by fast + hence "nth_item + (Suc (sum_encode (Inr (sum_encode (Inr (prod_encode (i, j))))))) + = Datatype.Scons x y" by simp + thus ?case .. +qed + +theorem countable_datatype: + fixes Rep :: "'b \ ('a::countable) Datatype.item" + fixes Abs :: "('a::countable) Datatype.item \ 'b" + fixes rep_set :: "('a::countable) Datatype.item \ bool" + assumes type: "type_definition Rep Abs (Collect rep_set)" + assumes finite_item: "\x. rep_set x \ finite_item x" + shows "OFCLASS('b, countable_class)" +proof + def f \ "\y. LEAST n. nth_item n = Rep y" + { + fix y :: 'b + have "rep_set (Rep y)" + using type_definition.Rep [OF type] by simp + hence "finite_item (Rep y)" + by (rule finite_item) + hence "\n. nth_item n = Rep y" + by (rule nth_item_covers) + hence "nth_item (f y) = Rep y" + unfolding f_def by (rule LeastI_ex) + hence "Abs (nth_item (f y)) = y" + using type_definition.Rep_inverse [OF type] by simp + } + hence "inj f" + by (rule inj_on_inverseI) + thus "\f::'b \ nat. inj f" + by - (rule exI) +qed + +method_setup countable_datatype = {* +let + fun countable_tac ctxt = + SUBGOAL (fn (goal, i) => + let + val ty_name = + (case goal of + (_ $ Const ("TYPE", Type ("itself", [Type (n, _)]))) => n + | _ => raise Match) + val typedef_info = hd (Typedef.get_info ctxt ty_name) + val typedef_thm = #type_definition (snd typedef_info) + val pred_name = + (case HOLogic.dest_Trueprop (concl_of typedef_thm) of + (typedef $ rep $ abs $ (collect $ Const (n, _))) => n + | _ => raise Match) + val induct_info = Inductive.the_inductive ctxt pred_name + val pred_names = #names (fst induct_info) + val induct_thms = #inducts (snd induct_info) + val alist = pred_names ~~ induct_thms + val induct_thm = the (AList.lookup (op =) alist pred_name) + val rules = @{thms finite_item.intros} + in + SOLVED' (fn i => EVERY + [rtac @{thm countable_datatype} i, + rtac typedef_thm i, + etac induct_thm i, + REPEAT (resolve_tac rules i ORELSE atac i)]) 1 + end) +in + Scan.succeed (fn ctxt => SIMPLE_METHOD' (countable_tac ctxt)) end +*} "prove countable class instances for datatypes" + +hide_const (open) finite_item nth_item + + +subsection {* Countable datatypes *} + +instance typerep :: countable + by countable_datatype + +end