# HG changeset patch
# User huffman
# Date 1333108818 -7200
# Node ID 7205eb4a0a054f5396f50c68cd9343f38d78a343
# Parent  52426c62b5d0a1eb8ee0f4a0f2680759636d0a65
rephrase lemma card_Pow using '2' instead of 'Suc (Suc 0)'

diff -r 52426c62b5d0 -r 7205eb4a0a05 src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Fri Mar 30 12:32:35 2012 +0200
+++ b/src/HOL/Enum.thy	Fri Mar 30 14:00:18 2012 +0200
@@ -465,7 +465,7 @@
   | "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"
+  "length (sublists xs) = 2 ^ length xs"
   by (induct xs) (simp_all add: Let_def)
 
 lemma sublists_powset:
@@ -484,9 +484,9 @@
   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)
+  then have "card (Pow (set xs)) = 2 ^ 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
+    have "card (Pow (set xs)) = 2 ^ 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
diff -r 52426c62b5d0 -r 7205eb4a0a05 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Mar 30 12:32:35 2012 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Mar 30 14:00:18 2012 +0200
@@ -2212,12 +2212,13 @@
 
 subsubsection {* Cardinality of the Powerset *}
 
-lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
+lemma card_Pow: "finite A ==> card (Pow A) = 2 ^ card A"
 apply (induct rule: finite_induct)
  apply (simp_all add: Pow_insert)
 apply (subst card_Un_disjoint, blast)
   apply (blast, blast)
 apply (subgoal_tac "inj_on (insert x) (Pow F)")
+ apply (subst mult_2)
  apply (simp add: card_image Pow_insert)
 apply (unfold inj_on_def)
 apply (blast elim!: equalityE)
diff -r 52426c62b5d0 -r 7205eb4a0a05 src/HOL/Library/Cardinality.thy
--- a/src/HOL/Library/Cardinality.thy	Fri Mar 30 12:32:35 2012 +0200
+++ b/src/HOL/Library/Cardinality.thy	Fri Mar 30 14:00:18 2012 +0200
@@ -59,7 +59,7 @@
 
 lemma card_set [simp]: "CARD('a set) = 2 ^ CARD('a::finite)"
   unfolding Pow_UNIV [symmetric]
-  by (simp only: card_Pow finite numeral_2_eq_2)
+  by (simp only: card_Pow finite)
 
 lemma card_nat [simp]: "CARD(nat) = 0"
   by (simp add: card_eq_0_iff)