src/HOL/Library/Countable.thy
changeset 58158 d2cb7cbb3aaa
parent 58155 14dda84afbb3
child 58160 e4965b677ba9
equal deleted inserted replaced
58157:c376c43c346c 58158:d2cb7cbb3aaa
   306 *} "prove countable class instances for datatypes"
   306 *} "prove countable class instances for datatypes"
   307 
   307 
   308 hide_const (open) finite_item nth_item
   308 hide_const (open) finite_item nth_item
   309 
   309 
   310 
   310 
   311 (* FIXME
       
   312 subsection {* Countable datatypes *}
   311 subsection {* Countable datatypes *}
   313 
   312 
       
   313 (* TODO: automate *)
       
   314 
       
   315 primrec encode_typerep :: "typerep \<Rightarrow> nat" where
       
   316   "encode_typerep (Typerep.Typerep s ts) = prod_encode (to_nat s, to_nat (map encode_typerep ts))"
       
   317 
       
   318 lemma encode_typerep_injective: "\<forall>u. encode_typerep t = encode_typerep u \<longrightarrow> t = u"
       
   319   apply (induct t)
       
   320   apply (rule allI)
       
   321   apply (case_tac u)
       
   322   apply (auto simp: sum_encode_eq prod_encode_eq elim: list.inj_map_strong[rotated 1])
       
   323   done
       
   324 
   314 instance typerep :: countable
   325 instance typerep :: countable
   315   by countable_datatype
   326   apply default
   316 *)
   327   apply (unfold inj_on_def ball_UNIV)
       
   328   apply (rule exI)
       
   329   apply (rule allI)
       
   330   apply (rule encode_typerep_injective)
       
   331   done
   317 
   332 
   318 end
   333 end