rephrase lemma card_Pow using '2' instead of 'Suc (Suc 0)'
authorhuffman
Fri Mar 30 14:00:18 2012 +0200 (2012-03-30)
changeset 472217205eb4a0a05
parent 47220 52426c62b5d0
child 47222 1b7c909a6fad
rephrase lemma card_Pow using '2' instead of 'Suc (Suc 0)'
src/HOL/Enum.thy
src/HOL/Finite_Set.thy
src/HOL/Library/Cardinality.thy
     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
     2.1 --- a/src/HOL/Finite_Set.thy	Fri Mar 30 12:32:35 2012 +0200
     2.2 +++ b/src/HOL/Finite_Set.thy	Fri Mar 30 14:00:18 2012 +0200
     2.3 @@ -2212,12 +2212,13 @@
     2.4  
     2.5  subsubsection {* Cardinality of the Powerset *}
     2.6  
     2.7 -lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
     2.8 +lemma card_Pow: "finite A ==> card (Pow A) = 2 ^ card A"
     2.9  apply (induct rule: finite_induct)
    2.10   apply (simp_all add: Pow_insert)
    2.11  apply (subst card_Un_disjoint, blast)
    2.12    apply (blast, blast)
    2.13  apply (subgoal_tac "inj_on (insert x) (Pow F)")
    2.14 + apply (subst mult_2)
    2.15   apply (simp add: card_image Pow_insert)
    2.16  apply (unfold inj_on_def)
    2.17  apply (blast elim!: equalityE)
     3.1 --- a/src/HOL/Library/Cardinality.thy	Fri Mar 30 12:32:35 2012 +0200
     3.2 +++ b/src/HOL/Library/Cardinality.thy	Fri Mar 30 14:00:18 2012 +0200
     3.3 @@ -59,7 +59,7 @@
     3.4  
     3.5  lemma card_set [simp]: "CARD('a set) = 2 ^ CARD('a::finite)"
     3.6    unfolding Pow_UNIV [symmetric]
     3.7 -  by (simp only: card_Pow finite numeral_2_eq_2)
     3.8 +  by (simp only: card_Pow finite)
     3.9  
    3.10  lemma card_nat [simp]: "CARD(nat) = 0"
    3.11    by (simp add: card_eq_0_iff)