293 |
293 |
294 lemma nth_map_Suc [simp]: |
294 lemma nth_map_Suc [simp]: |
295 "nth_map (Suc n) f (x # xs) = x # nth_map n f xs" |
295 "nth_map (Suc n) f (x # xs) = x # nth_map n f xs" |
296 by (simp add: nth_map_def) |
296 by (simp add: nth_map_def) |
297 |
297 |
|
298 text {* Enumeration of all sublists of a list *} |
|
299 |
|
300 primrec sublists :: "'a list \<Rightarrow> 'a list list" where |
|
301 "sublists [] = [[]]" |
|
302 | "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)" |
|
303 |
|
304 lemma length_sublists: |
|
305 "length (sublists xs) = Suc (Suc (0\<Colon>nat)) ^ length xs" |
|
306 by (induct xs) (simp_all add: Let_def) |
|
307 |
|
308 lemma sublists_powset: |
|
309 "set ` set (sublists xs) = Pow (set xs)" |
|
310 proof - |
|
311 have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A" |
|
312 by (auto simp add: image_def) |
|
313 have "set (map set (sublists xs)) = Pow (set xs)" |
|
314 by (induct xs) |
|
315 (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map) |
|
316 then show ?thesis by simp |
|
317 qed |
|
318 |
|
319 lemma distinct_set_sublists: |
|
320 assumes "distinct xs" |
|
321 shows "distinct (map set (sublists xs))" |
|
322 proof (rule card_distinct) |
|
323 have "finite (set xs)" by rule |
|
324 then have "card (Pow (set xs)) = Suc (Suc 0) ^ card (set xs)" by (rule card_Pow) |
|
325 with assms distinct_card [of xs] |
|
326 have "card (Pow (set xs)) = Suc (Suc 0) ^ length xs" by simp |
|
327 then show "card (set (map set (sublists xs))) = length (map set (sublists xs))" |
|
328 by (simp add: sublists_powset length_sublists) |
|
329 qed |
|
330 |
298 end |
331 end |