--- a/NEWS Fri Oct 14 22:42:56 2011 +0200
+++ b/NEWS Sat Oct 15 00:18:00 2011 +0200
@@ -12,6 +12,10 @@
*** HOL ***
+* 'Transitive_Closure.ntrancl': bounded transitive closure on relations.
+
+* 'sublists' moved to More_List.thy; INCOMPATIBILITY.
+
* Theory Int: Discontinued many legacy theorems specific to type int.
INCOMPATIBILITY, use the corresponding generic theorems instead.
--- a/src/HOL/Enum.thy Fri Oct 14 22:42:56 2011 +0200
+++ b/src/HOL/Enum.thy Sat Oct 15 00:18:00 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
--- a/src/HOL/Library/More_List.thy Fri Oct 14 22:42:56 2011 +0200
+++ b/src/HOL/Library/More_List.thy Sat Oct 15 00:18:00 2011 +0200
@@ -299,6 +299,40 @@
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
+
+
text {* monad operation *}
definition bind :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where