equal
deleted
inserted
replaced
114 also have "\<dots> = length xs ^ n" by (simp add: card_length) |
114 also have "\<dots> = length xs ^ n" by (simp add: card_length) |
115 finally show "card (set (n_lists n xs)) = length (n_lists n xs)" |
115 finally show "card (set (n_lists n xs)) = length (n_lists n xs)" |
116 by (simp add: length_n_lists) |
116 by (simp add: length_n_lists) |
117 qed |
117 qed |
118 |
118 |
119 lemma map_of_zip_map: |
119 lemma map_of_zip_map: (*FIXME move to Map.thy*) |
120 fixes f :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>enum" |
120 "map_of (zip xs (map f xs)) = (\<lambda>x. if x \<in> set xs then Some (f x) else None)" |
121 shows "map_of (zip xs (map f xs)) = (\<lambda>x. if x \<in> set xs then Some (f x) else None)" |
|
122 by (induct xs) (simp_all add: expand_fun_eq) |
121 by (induct xs) (simp_all add: expand_fun_eq) |
123 |
122 |
124 lemma map_of_zip_enum_is_Some: |
123 lemma map_of_zip_enum_is_Some: |
125 assumes "length ys = length (enum \<Colon> 'a\<Colon>enum list)" |
124 assumes "length ys = length (enum \<Colon> 'a\<Colon>enum list)" |
126 shows "\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y" |
125 shows "\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y" |