author huffman Fri, 30 Mar 2012 14:00:18 +0200 changeset 47221 7205eb4a0a05 parent 47220 52426c62b5d0 child 47222 1b7c909a6fad
rephrase lemma card_Pow using '2' instead of 'Suc (Suc 0)'
 src/HOL/Enum.thy file | annotate | diff | comparison | revisions src/HOL/Finite_Set.thy file | annotate | diff | comparison | revisions src/HOL/Library/Cardinality.thy file | annotate | diff | comparison | revisions
--- 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))"
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 (subst card_Un_disjoint, blast)
apply (blast, blast)
apply (subgoal_tac "inj_on (insert x) (Pow F)")
+ apply (subst mult_2)
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"