src/HOL/Library/Enum.thy
changeset 28245 9767dd8e1e54
parent 27487 c8a6ce181805
child 28562 4e74209f113e
equal deleted inserted replaced
28244:f433e544a855 28245:9767dd8e1e54
   175       distinct_map distinct_n_lists enum_distinct set_n_lists enum_all)
   175       distinct_map distinct_n_lists enum_distinct set_n_lists enum_all)
   176 qed
   176 qed
   177 
   177 
   178 end
   178 end
   179 
   179 
   180 lemma [code func]:
   180 lemma enum_fun_code [code func]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, eq} list)
   181   "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>('a\<Colon>{enum, eq}) list) ys)) (n_lists (length (enum\<Colon>'a\<Colon>{enum, eq} list)) enum)"
   181   in map (\<lambda>ys. the o map_of (zip enum_a ys)) (n_lists (length enum_a) enum))"
   182   unfolding enum_fun_def ..
   182   by (simp add: enum_fun_def Let_def)
   183 
   183 
   184 instantiation unit :: enum
   184 instantiation unit :: enum
   185 begin
   185 begin
   186 
   186 
   187 definition
   187 definition