moved `sublists` to theory Enum
authorhaftmann
Sat Dec 24 15:53:11 2011 +0100 (2011-12-24)
changeset 45973204f34a99ceb
parent 45972 deda685ba210
child 45974 2b043ed911ac
moved `sublists` to theory Enum
src/HOL/Library/More_List.thy
     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