--- 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
--- 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)
--- 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)