# 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 \<Rightarrow> '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\<Colon>nat)) ^ length xs"
-  by (induct xs) (simp_all add: Let_def)
-
-lemma sublists_powset:
-  "set ` set (sublists xs) = Pow (set xs)"
-proof -
-  have aux: "\<And>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 \<Rightarrow> '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\<Colon>nat)) ^ length xs"
+  by (induct xs) (simp_all add: Let_def)
+
+lemma sublists_powset:
+  "set ` set (sublists xs) = Pow (set xs)"
+proof -
+  have aux: "\<And>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