--- a/src/HOL/Finite_Set.thy Tue Jan 21 13:05:22 2014 +0100
+++ b/src/HOL/Finite_Set.thy Tue Jan 21 13:21:55 2014 +0100
@@ -6,7 +6,7 @@
header {* Finite sets *}
theory Finite_Set
-imports Power
+imports Product_Type Sum_Type Nat
begin
subsection {* Predicate for finite sets *}
@@ -1509,9 +1509,6 @@
lemma card_UNIV_unit [simp]: "card (UNIV :: unit set) = 1"
unfolding UNIV_unit by simp
-lemma card_UNIV_bool [simp]: "card (UNIV :: bool set) = 2"
- unfolding UNIV_bool by simp
-
subsubsection {* Cardinality of image *}
@@ -1639,25 +1636,6 @@
"card (A <+> B) = (if finite A \<and> finite B then card A + card B else 0)"
by (auto simp add: card_Plus)
-
-subsubsection {* Cardinality of the Powerset *}
-
-lemma card_Pow: "finite A \<Longrightarrow> card (Pow A) = 2 ^ card A"
-proof (induct rule: finite_induct)
- case empty
- show ?case by auto
-next
- case (insert x A)
- then have "inj_on (insert x) (Pow A)"
- unfolding inj_on_def by (blast elim!: equalityE)
- then have "card (Pow A) + card (insert x ` Pow A) = 2 * 2 ^ card A"
- by (simp add: mult_2 card_image Pow_insert insert.hyps)
- then show ?case using insert
- apply (simp add: Pow_insert)
- apply (subst card_Un_disjoint, auto)
- done
-qed
-
text {* Relates to equivalence classes. Based on a theorem of F. Kamm\"uller. *}
lemma dvd_partition:
--- a/src/HOL/Groups_Big.thy Tue Jan 21 13:05:22 2014 +0100
+++ b/src/HOL/Groups_Big.thy Tue Jan 21 13:21:55 2014 +0100
@@ -1332,38 +1332,6 @@
by induct (auto simp add: field_simps abs_mult)
qed auto
-lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
-apply (erule finite_induct)
-apply auto
-done
-
-lemma setprod_gen_delta:
- assumes fS: "finite S"
- shows "setprod (\<lambda>k. if k=a then b k else c) S = (if a \<in> S then (b a ::'a::comm_monoid_mult) * c^ (card S - 1) else c^ card S)"
-proof-
- let ?f = "(\<lambda>k. if k=a then b k else c)"
- {assume a: "a \<notin> S"
- hence "\<forall> k\<in> S. ?f k = c" by simp
- hence ?thesis using a setprod_constant[OF fS, of c] by simp }
- moreover
- {assume a: "a \<in> S"
- let ?A = "S - {a}"
- let ?B = "{a}"
- have eq: "S = ?A \<union> ?B" using a by blast
- have dj: "?A \<inter> ?B = {}" by simp
- from fS have fAB: "finite ?A" "finite ?B" by auto
- have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
- apply (rule setprod_cong) by auto
- have cA: "card ?A = card S - 1" using fS a by auto
- have fA1: "setprod ?f ?A = c ^ card ?A" unfolding fA0 apply (rule setprod_constant) using fS by auto
- have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
- using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
- by simp
- then have ?thesis using a cA
- by (simp add: fA1 field_simps cong add: setprod_cong cong del: if_weak_cong)}
- ultimately show ?thesis by blast
-qed
-
lemma setprod_eq_1_iff [simp]:
"finite F ==> setprod f F = 1 \<longleftrightarrow> (ALL a:F. f a = (1::nat))"
by (induct set: finite) auto
--- a/src/HOL/Int.thy Tue Jan 21 13:05:22 2014 +0100
+++ b/src/HOL/Int.thy Tue Jan 21 13:21:55 2014 +0100
@@ -6,7 +6,7 @@
header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *}
theory Int
-imports Equiv_Relations Wellfounded Quotient Fun_Def
+imports Equiv_Relations Wellfounded Power Quotient Fun_Def
begin
subsection {* Definition of integers as a quotient type *}
--- a/src/HOL/Power.thy Tue Jan 21 13:05:22 2014 +0100
+++ b/src/HOL/Power.thy Tue Jan 21 13:21:55 2014 +0100
@@ -6,7 +6,7 @@
header {* Exponentiation *}
theory Power
-imports Num
+imports Num Equiv_Relations
begin
subsection {* Powers for Arbitrary Monoids *}
@@ -735,6 +735,66 @@
qed
qed
+subsubsection {* Cardinality of the Powerset *}
+
+lemma card_UNIV_bool [simp]: "card (UNIV :: bool set) = 2"
+ unfolding UNIV_bool by simp
+
+lemma card_Pow: "finite A \<Longrightarrow> card (Pow A) = 2 ^ card A"
+proof (induct rule: finite_induct)
+ case empty
+ show ?case by auto
+next
+ case (insert x A)
+ then have "inj_on (insert x) (Pow A)"
+ unfolding inj_on_def by (blast elim!: equalityE)
+ then have "card (Pow A) + card (insert x ` Pow A) = 2 * 2 ^ card A"
+ by (simp add: mult_2 card_image Pow_insert insert.hyps)
+ then show ?case using insert
+ apply (simp add: Pow_insert)
+ apply (subst card_Un_disjoint, auto)
+ done
+qed
+
+subsubsection {* Generalized product over a set *}
+
+lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
+apply (erule finite_induct)
+apply auto
+done
+
+lemma setprod_gen_delta:
+ assumes fS: "finite S"
+ shows "setprod (\<lambda>k. if k=a then b k else c) S = (if a \<in> S then (b a ::'a::comm_monoid_mult) * c^ (card S - 1) else c^ card S)"
+proof-
+ let ?f = "(\<lambda>k. if k=a then b k else c)"
+ {assume a: "a \<notin> S"
+ hence "\<forall> k\<in> S. ?f k = c" by simp
+ hence ?thesis using a setprod_constant[OF fS, of c] by simp }
+ moreover
+ {assume a: "a \<in> S"
+ let ?A = "S - {a}"
+ let ?B = "{a}"
+ have eq: "S = ?A \<union> ?B" using a by blast
+ have dj: "?A \<inter> ?B = {}" by simp
+ from fS have fAB: "finite ?A" "finite ?B" by auto
+ have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
+ apply (rule setprod_cong) by auto
+ have cA: "card ?A = card S - 1" using fS a by auto
+ have fA1: "setprod ?f ?A = c ^ card ?A" unfolding fA0 apply (rule setprod_constant) using fS by auto
+ have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
+ using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
+ by simp
+ then have ?thesis using a cA
+ by (simp add: fA1 field_simps cong add: setprod_cong cong del: if_weak_cong)}
+ ultimately show ?thesis by blast
+qed
+
+lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
+ by auto
+
+lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
+ by auto
subsection {* Code generator tweak *}
--- a/src/HOL/Relation.thy Tue Jan 21 13:05:22 2014 +0100
+++ b/src/HOL/Relation.thy Tue Jan 21 13:21:55 2014 +0100
@@ -930,12 +930,6 @@
"Domain r = {x. \<exists>y. (x, y) \<in> r}"
by blast
-lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
- by auto
-
-lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
- by auto
-
subsubsection {* Image of a set under a relation *}