src/HOL/Enum.thy
 changeset 45144 3f4742ce4629 parent 45141 b2eb87bd541b child 45963 1c7e6454883e
```     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
```