src/HOL/Library/Countable.thy
changeset 58112 8081087096ad
parent 57437 0baf08c075b9
child 58155 14dda84afbb3
equal deleted inserted replaced
58111:82db9ad610b9 58112:8081087096ad
   171 qed
   171 qed
   172 
   172 
   173 
   173 
   174 subsection {* Automatically proving countability of datatypes *}
   174 subsection {* Automatically proving countability of datatypes *}
   175 
   175 
   176 inductive finite_item :: "'a Datatype.item \<Rightarrow> bool" where
   176 inductive finite_item :: "'a Old_Datatype.item \<Rightarrow> bool" where
   177   undefined: "finite_item undefined"
   177   undefined: "finite_item undefined"
   178 | In0: "finite_item x \<Longrightarrow> finite_item (Datatype.In0 x)"
   178 | In0: "finite_item x \<Longrightarrow> finite_item (Old_Datatype.In0 x)"
   179 | In1: "finite_item x \<Longrightarrow> finite_item (Datatype.In1 x)"
   179 | In1: "finite_item x \<Longrightarrow> finite_item (Old_Datatype.In1 x)"
   180 | Leaf: "finite_item (Datatype.Leaf a)"
   180 | Leaf: "finite_item (Old_Datatype.Leaf a)"
   181 | Scons: "\<lbrakk>finite_item x; finite_item y\<rbrakk> \<Longrightarrow> finite_item (Datatype.Scons x y)"
   181 | Scons: "\<lbrakk>finite_item x; finite_item y\<rbrakk> \<Longrightarrow> finite_item (Old_Datatype.Scons x y)"
   182 
   182 
   183 function
   183 function
   184   nth_item :: "nat \<Rightarrow> ('a::countable) Datatype.item"
   184   nth_item :: "nat \<Rightarrow> ('a::countable) Old_Datatype.item"
   185 where
   185 where
   186   "nth_item 0 = undefined"
   186   "nth_item 0 = undefined"
   187 | "nth_item (Suc n) =
   187 | "nth_item (Suc n) =
   188   (case sum_decode n of
   188   (case sum_decode n of
   189     Inl i \<Rightarrow>
   189     Inl i \<Rightarrow>
   190     (case sum_decode i of
   190     (case sum_decode i of
   191       Inl j \<Rightarrow> Datatype.In0 (nth_item j)
   191       Inl j \<Rightarrow> Old_Datatype.In0 (nth_item j)
   192     | Inr j \<Rightarrow> Datatype.In1 (nth_item j))
   192     | Inr j \<Rightarrow> Old_Datatype.In1 (nth_item j))
   193   | Inr i \<Rightarrow>
   193   | Inr i \<Rightarrow>
   194     (case sum_decode i of
   194     (case sum_decode i of
   195       Inl j \<Rightarrow> Datatype.Leaf (from_nat j)
   195       Inl j \<Rightarrow> Old_Datatype.Leaf (from_nat j)
   196     | Inr j \<Rightarrow>
   196     | Inr j \<Rightarrow>
   197       (case prod_decode j of
   197       (case prod_decode j of
   198         (a, b) \<Rightarrow> Datatype.Scons (nth_item a) (nth_item b))))"
   198         (a, b) \<Rightarrow> Old_Datatype.Scons (nth_item a) (nth_item b))))"
   199 by pat_completeness auto
   199 by pat_completeness auto
   200 
   200 
   201 lemma le_sum_encode_Inl: "x \<le> y \<Longrightarrow> x \<le> sum_encode (Inl y)"
   201 lemma le_sum_encode_Inl: "x \<le> y \<Longrightarrow> x \<le> sum_encode (Inl y)"
   202 unfolding sum_encode_def by simp
   202 unfolding sum_encode_def by simp
   203 
   203 
   216   have "nth_item 0 = undefined" by simp
   216   have "nth_item 0 = undefined" by simp
   217   thus ?case ..
   217   thus ?case ..
   218 next
   218 next
   219   case (In0 x)
   219   case (In0 x)
   220   then obtain n where "nth_item n = x" by fast
   220   then obtain n where "nth_item n = x" by fast
   221   hence "nth_item (Suc (sum_encode (Inl (sum_encode (Inl n)))))
   221   hence "nth_item (Suc (sum_encode (Inl (sum_encode (Inl n))))) = Old_Datatype.In0 x" by simp
   222     = Datatype.In0 x" by simp
       
   223   thus ?case ..
   222   thus ?case ..
   224 next
   223 next
   225   case (In1 x)
   224   case (In1 x)
   226   then obtain n where "nth_item n = x" by fast
   225   then obtain n where "nth_item n = x" by fast
   227   hence "nth_item (Suc (sum_encode (Inl (sum_encode (Inr n)))))
   226   hence "nth_item (Suc (sum_encode (Inl (sum_encode (Inr n))))) = Old_Datatype.In1 x" by simp
   228     = Datatype.In1 x" by simp
       
   229   thus ?case ..
   227   thus ?case ..
   230 next
   228 next
   231   case (Leaf a)
   229   case (Leaf a)
   232   have "nth_item (Suc (sum_encode (Inr (sum_encode (Inl (to_nat a))))))
   230   have "nth_item (Suc (sum_encode (Inr (sum_encode (Inl (to_nat a)))))) = Old_Datatype.Leaf a"
   233     = Datatype.Leaf a" by simp
   231     by simp
   234   thus ?case ..
   232   thus ?case ..
   235 next
   233 next
   236   case (Scons x y)
   234   case (Scons x y)
   237   then obtain i j where "nth_item i = x" and "nth_item j = y" by fast
   235   then obtain i j where "nth_item i = x" and "nth_item j = y" by fast
   238   hence "nth_item
   236   hence "nth_item
   239     (Suc (sum_encode (Inr (sum_encode (Inr (prod_encode (i, j)))))))
   237     (Suc (sum_encode (Inr (sum_encode (Inr (prod_encode (i, j))))))) = Old_Datatype.Scons x y"
   240       = Datatype.Scons x y" by simp
   238     by simp
   241   thus ?case ..
   239   thus ?case ..
   242 qed
   240 qed
   243 
   241 
   244 theorem countable_datatype:
   242 theorem countable_datatype:
   245   fixes Rep :: "'b \<Rightarrow> ('a::countable) Datatype.item"
   243   fixes Rep :: "'b \<Rightarrow> ('a::countable) Old_Datatype.item"
   246   fixes Abs :: "('a::countable) Datatype.item \<Rightarrow> 'b"
   244   fixes Abs :: "('a::countable) Old_Datatype.item \<Rightarrow> 'b"
   247   fixes rep_set :: "('a::countable) Datatype.item \<Rightarrow> bool"
   245   fixes rep_set :: "('a::countable) Old_Datatype.item \<Rightarrow> bool"
   248   assumes type: "type_definition Rep Abs (Collect rep_set)"
   246   assumes type: "type_definition Rep Abs (Collect rep_set)"
   249   assumes finite_item: "\<And>x. rep_set x \<Longrightarrow> finite_item x"
   247   assumes finite_item: "\<And>x. rep_set x \<Longrightarrow> finite_item x"
   250   shows "OFCLASS('b, countable_class)"
   248   shows "OFCLASS('b, countable_class)"
   251 proof
   249 proof
   252   def f \<equiv> "\<lambda>y. LEAST n. nth_item n = Rep y"
   250   def f \<equiv> "\<lambda>y. LEAST n. nth_item n = Rep y"