# HG changeset patch # User traytel # Date 1390306915 -3600 # Node ID 916b2ac758f4418750ffa20aa0d5626de6b2886d # Parent 149ccaf4ae5c70a44e59010c338cb93cc6124e44 removed theory dependency of BNF_LFP on Datatype diff -r 149ccaf4ae5c -r 916b2ac758f4 src/HOL/Finite_Set.thy --- 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 \ 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 \ 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: diff -r 149ccaf4ae5c -r 916b2ac758f4 src/HOL/Groups_Big.thy --- 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 ==> (\x\ 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 (\k. if k=a then b k else c) S = (if a \ S then (b a ::'a::comm_monoid_mult) * c^ (card S - 1) else c^ card S)" -proof- - let ?f = "(\k. if k=a then b k else c)" - {assume a: "a \ S" - hence "\ k\ S. ?f k = c" by simp - hence ?thesis using a setprod_constant[OF fS, of c] by simp } - moreover - {assume a: "a \ S" - let ?A = "S - {a}" - let ?B = "{a}" - have eq: "S = ?A \ ?B" using a by blast - have dj: "?A \ ?B = {}" by simp - from fS have fAB: "finite ?A" "finite ?B" by auto - have fA0:"setprod ?f ?A = setprod (\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 \ (ALL a:F. f a = (1::nat))" by (induct set: finite) auto diff -r 149ccaf4ae5c -r 916b2ac758f4 src/HOL/Int.thy --- 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 *} diff -r 149ccaf4ae5c -r 916b2ac758f4 src/HOL/Power.thy --- 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 \ 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 ==> (\x\ 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 (\k. if k=a then b k else c) S = (if a \ S then (b a ::'a::comm_monoid_mult) * c^ (card S - 1) else c^ card S)" +proof- + let ?f = "(\k. if k=a then b k else c)" + {assume a: "a \ S" + hence "\ k\ S. ?f k = c" by simp + hence ?thesis using a setprod_constant[OF fS, of c] by simp } + moreover + {assume a: "a \ S" + let ?A = "S - {a}" + let ?B = "{a}" + have eq: "S = ?A \ ?B" using a by blast + have dj: "?A \ ?B = {}" by simp + from fS have fAB: "finite ?A" "finite ?B" by auto + have fA0:"setprod ?f ?A = setprod (\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 *} diff -r 149ccaf4ae5c -r 916b2ac758f4 src/HOL/Relation.thy --- 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. \y. (x, y) \ 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 *}