moved sublists to More_List.thy
authorhaftmann
Fri Oct 14 18:55:59 2011 +0200 (2011-10-14 ago)
changeset 451443f4742ce4629
parent 45143 aed8f14bf562
child 45146 5465824c1c8d
moved sublists to More_List.thy
src/HOL/Enum.thy
src/HOL/Library/More_List.thy
     1.1 --- a/src/HOL/Enum.thy	Fri Oct 14 18:55:29 2011 +0200
     1.2 +++ b/src/HOL/Enum.thy	Fri Oct 14 18:55:59 2011 +0200
     1.3 @@ -370,37 +370,6 @@
     1.4  
     1.5  end
     1.6  
     1.7 -primrec sublists :: "'a list \<Rightarrow> 'a list list" where
     1.8 -  "sublists [] = [[]]"
     1.9 -  | "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
    1.10 -
    1.11 -lemma length_sublists:
    1.12 -  "length (sublists xs) = Suc (Suc (0\<Colon>nat)) ^ length xs"
    1.13 -  by (induct xs) (simp_all add: Let_def)
    1.14 -
    1.15 -lemma sublists_powset:
    1.16 -  "set ` set (sublists xs) = Pow (set xs)"
    1.17 -proof -
    1.18 -  have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A"
    1.19 -    by (auto simp add: image_def)
    1.20 -  have "set (map set (sublists xs)) = Pow (set xs)"
    1.21 -    by (induct xs)
    1.22 -      (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map)
    1.23 -  then show ?thesis by simp
    1.24 -qed
    1.25 -
    1.26 -lemma distinct_set_sublists:
    1.27 -  assumes "distinct xs"
    1.28 -  shows "distinct (map set (sublists xs))"
    1.29 -proof (rule card_distinct)
    1.30 -  have "finite (set xs)" by rule
    1.31 -  then have "card (Pow (set xs)) = Suc (Suc 0) ^ card (set xs)" by (rule card_Pow)
    1.32 -  with assms distinct_card [of xs]
    1.33 -    have "card (Pow (set xs)) = Suc (Suc 0) ^ length xs" by simp
    1.34 -  then show "card (set (map set (sublists xs))) = length (map set (sublists xs))"
    1.35 -    by (simp add: sublists_powset length_sublists)
    1.36 -qed
    1.37 -
    1.38  instantiation nibble :: enum
    1.39  begin
    1.40  
     2.1 --- a/src/HOL/Library/More_List.thy	Fri Oct 14 18:55:29 2011 +0200
     2.2 +++ b/src/HOL/Library/More_List.thy	Fri Oct 14 18:55:59 2011 +0200
     2.3 @@ -295,4 +295,37 @@
     2.4    "nth_map (Suc n) f (x # xs) = x # nth_map n f xs"
     2.5    by (simp add: nth_map_def)
     2.6  
     2.7 +text {* Enumeration of all sublists of a list *}
     2.8 +
     2.9 +primrec sublists :: "'a list \<Rightarrow> 'a list list" where
    2.10 +  "sublists [] = [[]]"
    2.11 +  | "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
    2.12 +
    2.13 +lemma length_sublists:
    2.14 +  "length (sublists xs) = Suc (Suc (0\<Colon>nat)) ^ length xs"
    2.15 +  by (induct xs) (simp_all add: Let_def)
    2.16 +
    2.17 +lemma sublists_powset:
    2.18 +  "set ` set (sublists xs) = Pow (set xs)"
    2.19 +proof -
    2.20 +  have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A"
    2.21 +    by (auto simp add: image_def)
    2.22 +  have "set (map set (sublists xs)) = Pow (set xs)"
    2.23 +    by (induct xs)
    2.24 +      (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map)
    2.25 +  then show ?thesis by simp
    2.26 +qed
    2.27 +
    2.28 +lemma distinct_set_sublists:
    2.29 +  assumes "distinct xs"
    2.30 +  shows "distinct (map set (sublists xs))"
    2.31 +proof (rule card_distinct)
    2.32 +  have "finite (set xs)" by rule
    2.33 +  then have "card (Pow (set xs)) = Suc (Suc 0) ^ card (set xs)" by (rule card_Pow)
    2.34 +  with assms distinct_card [of xs]
    2.35 +    have "card (Pow (set xs)) = Suc (Suc 0) ^ length xs" by simp
    2.36 +  then show "card (set (map set (sublists xs))) = length (map set (sublists xs))"
    2.37 +    by (simp add: sublists_powset length_sublists)
    2.38 +qed
    2.39 +
    2.40  end