# HG changeset patch # User haftmann # Date 1318611359 -7200 # Node ID 3f4742ce4629b697c91592973fd4e5fb786666d3 # Parent aed8f14bf562369f375834c685493998454823fe moved sublists to More_List.thy diff -r aed8f14bf562 -r 3f4742ce4629 src/HOL/Enum.thy --- a/src/HOL/Enum.thy Fri Oct 14 18:55:29 2011 +0200 +++ b/src/HOL/Enum.thy Fri Oct 14 18:55:59 2011 +0200 @@ -370,37 +370,6 @@ end -primrec sublists :: "'a list \ 'a list list" where - "sublists [] = [[]]" - | "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)" - -lemma length_sublists: - "length (sublists xs) = Suc (Suc (0\nat)) ^ length xs" - by (induct xs) (simp_all add: Let_def) - -lemma sublists_powset: - "set ` set (sublists xs) = Pow (set xs)" -proof - - have aux: "\x A. set ` Cons x ` A = insert x ` set ` A" - by (auto simp add: image_def) - have "set (map set (sublists xs)) = Pow (set xs)" - by (induct xs) - (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map) - then show ?thesis by simp -qed - -lemma distinct_set_sublists: - assumes "distinct xs" - shows "distinct (map set (sublists xs))" -proof (rule card_distinct) - have "finite (set xs)" by rule - then have "card (Pow (set xs)) = Suc (Suc 0) ^ card (set xs)" by (rule card_Pow) - with assms distinct_card [of xs] - have "card (Pow (set xs)) = Suc (Suc 0) ^ length xs" by simp - then show "card (set (map set (sublists xs))) = length (map set (sublists xs))" - by (simp add: sublists_powset length_sublists) -qed - instantiation nibble :: enum begin diff -r aed8f14bf562 -r 3f4742ce4629 src/HOL/Library/More_List.thy --- a/src/HOL/Library/More_List.thy Fri Oct 14 18:55:29 2011 +0200 +++ b/src/HOL/Library/More_List.thy Fri Oct 14 18:55:59 2011 +0200 @@ -295,4 +295,37 @@ "nth_map (Suc n) f (x # xs) = x # nth_map n f xs" by (simp add: nth_map_def) +text {* Enumeration of all sublists of a list *} + +primrec sublists :: "'a list \ 'a list list" where + "sublists [] = [[]]" + | "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)" + +lemma length_sublists: + "length (sublists xs) = Suc (Suc (0\nat)) ^ length xs" + by (induct xs) (simp_all add: Let_def) + +lemma sublists_powset: + "set ` set (sublists xs) = Pow (set xs)" +proof - + have aux: "\x A. set ` Cons x ` A = insert x ` set ` A" + by (auto simp add: image_def) + have "set (map set (sublists xs)) = Pow (set xs)" + by (induct xs) + (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map) + then show ?thesis by simp +qed + +lemma distinct_set_sublists: + assumes "distinct xs" + shows "distinct (map set (sublists xs))" +proof (rule card_distinct) + have "finite (set xs)" by rule + then have "card (Pow (set xs)) = Suc (Suc 0) ^ card (set xs)" by (rule card_Pow) + with assms distinct_card [of xs] + have "card (Pow (set xs)) = Suc (Suc 0) ^ length xs" by simp + then show "card (set (map set (sublists xs))) = length (map set (sublists xs))" + by (simp add: sublists_powset length_sublists) +qed + end