summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/More_List.thy

changeset 45973 | 204f34a99ceb |

parent 45146 | 5465824c1c8d |

1.1 --- a/src/HOL/Library/More_List.thy Sat Dec 24 15:53:11 2011 +0100 1.2 +++ b/src/HOL/Library/More_List.thy Sat Dec 24 15:53:11 2011 +0100 1.3 @@ -1,4 +1,4 @@ 1.4 -(* Author: Florian Haftmann, TU Muenchen *) 1.5 +(* Author: Florian Haftmann, TU Muenchen *) 1.6 1.7 header {* Operations on lists beyond the standard List theory *} 1.8 1.9 @@ -299,40 +299,6 @@ 1.10 by (simp add: nth_map_def) 1.11 1.12 1.13 -text {* Enumeration of all sublists of a list *} 1.14 - 1.15 -primrec sublists :: "'a list \<Rightarrow> 'a list list" where 1.16 - "sublists [] = [[]]" 1.17 - | "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)" 1.18 - 1.19 -lemma length_sublists: 1.20 - "length (sublists xs) = Suc (Suc (0\<Colon>nat)) ^ length xs" 1.21 - by (induct xs) (simp_all add: Let_def) 1.22 - 1.23 -lemma sublists_powset: 1.24 - "set ` set (sublists xs) = Pow (set xs)" 1.25 -proof - 1.26 - have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A" 1.27 - by (auto simp add: image_def) 1.28 - have "set (map set (sublists xs)) = Pow (set xs)" 1.29 - by (induct xs) 1.30 - (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map) 1.31 - then show ?thesis by simp 1.32 -qed 1.33 - 1.34 -lemma distinct_set_sublists: 1.35 - assumes "distinct xs" 1.36 - shows "distinct (map set (sublists xs))" 1.37 -proof (rule card_distinct) 1.38 - have "finite (set xs)" by rule 1.39 - then have "card (Pow (set xs)) = Suc (Suc 0) ^ card (set xs)" by (rule card_Pow) 1.40 - with assms distinct_card [of xs] 1.41 - have "card (Pow (set xs)) = Suc (Suc 0) ^ length xs" by simp 1.42 - then show "card (set (map set (sublists xs))) = length (map set (sublists xs))" 1.43 - by (simp add: sublists_powset length_sublists) 1.44 -qed 1.45 - 1.46 - 1.47 text {* monad operation *} 1.48 1.49 definition bind :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where