src/HOL/Enum.thy
changeset 47221 7205eb4a0a05
parent 46361 87d5d36a9005
child 47231 3ff8c79a9e2f
     1.1 --- a/src/HOL/Enum.thy	Fri Mar 30 12:32:35 2012 +0200
     1.2 +++ b/src/HOL/Enum.thy	Fri Mar 30 14:00:18 2012 +0200
     1.3 @@ -465,7 +465,7 @@
     1.4    | "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
     1.5  
     1.6  lemma length_sublists:
     1.7 -  "length (sublists xs) = Suc (Suc (0\<Colon>nat)) ^ length xs"
     1.8 +  "length (sublists xs) = 2 ^ length xs"
     1.9    by (induct xs) (simp_all add: Let_def)
    1.10  
    1.11  lemma sublists_powset:
    1.12 @@ -484,9 +484,9 @@
    1.13    shows "distinct (map set (sublists xs))"
    1.14  proof (rule card_distinct)
    1.15    have "finite (set xs)" by rule
    1.16 -  then have "card (Pow (set xs)) = Suc (Suc 0) ^ card (set xs)" by (rule card_Pow)
    1.17 +  then have "card (Pow (set xs)) = 2 ^ card (set xs)" by (rule card_Pow)
    1.18    with assms distinct_card [of xs]
    1.19 -    have "card (Pow (set xs)) = Suc (Suc 0) ^ length xs" by simp
    1.20 +    have "card (Pow (set xs)) = 2 ^ length xs" by simp
    1.21    then show "card (set (map set (sublists xs))) = length (map set (sublists xs))"
    1.22      by (simp add: sublists_powset length_sublists)
    1.23  qed