author traytel Tue Jan 21 13:21:55 2014 +0100 (2014-01-21) changeset 55096 916b2ac758f4 parent 55094 149ccaf4ae5c child 55097 81dac5c1a5bb
removed theory dependency of BNF_LFP on Datatype
 src/HOL/Finite_Set.thy file | annotate | diff | revisions src/HOL/Groups_Big.thy file | annotate | diff | revisions src/HOL/Int.thy file | annotate | diff | revisions src/HOL/Power.thy file | annotate | diff | revisions src/HOL/Relation.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Finite_Set.thy	Tue Jan 21 13:05:22 2014 +0100
1.2 +++ b/src/HOL/Finite_Set.thy	Tue Jan 21 13:21:55 2014 +0100
1.3 @@ -6,7 +6,7 @@
1.4  header {* Finite sets *}
1.5
1.6  theory Finite_Set
1.7 -imports Power
1.8 +imports Product_Type Sum_Type Nat
1.9  begin
1.10
1.11  subsection {* Predicate for finite sets *}
1.12 @@ -1509,9 +1509,6 @@
1.13  lemma card_UNIV_unit [simp]: "card (UNIV :: unit set) = 1"
1.14    unfolding UNIV_unit by simp
1.15
1.16 -lemma card_UNIV_bool [simp]: "card (UNIV :: bool set) = 2"
1.17 -  unfolding UNIV_bool by simp
1.18 -
1.19
1.20  subsubsection {* Cardinality of image *}
1.21
1.22 @@ -1639,25 +1636,6 @@
1.23    "card (A <+> B) = (if finite A \<and> finite B then card A + card B else 0)"
1.24    by (auto simp add: card_Plus)
1.25
1.26 -
1.27 -subsubsection {* Cardinality of the Powerset *}
1.28 -
1.29 -lemma card_Pow: "finite A \<Longrightarrow> card (Pow A) = 2 ^ card A"
1.30 -proof (induct rule: finite_induct)
1.31 -  case empty
1.32 -    show ?case by auto
1.33 -next
1.34 -  case (insert x A)
1.35 -  then have "inj_on (insert x) (Pow A)"
1.36 -    unfolding inj_on_def by (blast elim!: equalityE)
1.37 -  then have "card (Pow A) + card (insert x ` Pow A) = 2 * 2 ^ card A"
1.38 -    by (simp add: mult_2 card_image Pow_insert insert.hyps)
1.39 -  then show ?case using insert
1.40 -    apply (simp add: Pow_insert)
1.41 -    apply (subst card_Un_disjoint, auto)
1.42 -    done
1.43 -qed
1.44 -
1.45  text {* Relates to equivalence classes.  Based on a theorem of F. Kamm\"uller.  *}
1.46
1.47  lemma dvd_partition:
```
```     2.1 --- a/src/HOL/Groups_Big.thy	Tue Jan 21 13:05:22 2014 +0100
2.2 +++ b/src/HOL/Groups_Big.thy	Tue Jan 21 13:21:55 2014 +0100
2.3 @@ -1332,38 +1332,6 @@
2.4      by induct (auto simp add: field_simps abs_mult)
2.5  qed auto
2.6
2.7 -lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
2.8 -apply (erule finite_induct)
2.9 -apply auto
2.10 -done
2.11 -
2.12 -lemma setprod_gen_delta:
2.13 -  assumes fS: "finite S"
2.14 -  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)"
2.15 -proof-
2.16 -  let ?f = "(\<lambda>k. if k=a then b k else c)"
2.17 -  {assume a: "a \<notin> S"
2.18 -    hence "\<forall> k\<in> S. ?f k = c" by simp
2.19 -    hence ?thesis  using a setprod_constant[OF fS, of c] by simp }
2.20 -  moreover
2.21 -  {assume a: "a \<in> S"
2.22 -    let ?A = "S - {a}"
2.23 -    let ?B = "{a}"
2.24 -    have eq: "S = ?A \<union> ?B" using a by blast
2.25 -    have dj: "?A \<inter> ?B = {}" by simp
2.26 -    from fS have fAB: "finite ?A" "finite ?B" by auto
2.27 -    have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
2.28 -      apply (rule setprod_cong) by auto
2.29 -    have cA: "card ?A = card S - 1" using fS a by auto
2.30 -    have fA1: "setprod ?f ?A = c ^ card ?A"  unfolding fA0 apply (rule setprod_constant) using fS by auto
2.31 -    have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
2.32 -      using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
2.33 -      by simp
2.34 -    then have ?thesis using a cA
2.35 -      by (simp add: fA1 field_simps cong add: setprod_cong cong del: if_weak_cong)}
2.36 -  ultimately show ?thesis by blast
2.37 -qed
2.38 -
2.39  lemma setprod_eq_1_iff [simp]:
2.40    "finite F ==> setprod f F = 1 \<longleftrightarrow> (ALL a:F. f a = (1::nat))"
2.41    by (induct set: finite) auto
```
```     3.1 --- a/src/HOL/Int.thy	Tue Jan 21 13:05:22 2014 +0100
3.2 +++ b/src/HOL/Int.thy	Tue Jan 21 13:21:55 2014 +0100
3.3 @@ -6,7 +6,7 @@
3.4  header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *}
3.5
3.6  theory Int
3.7 -imports Equiv_Relations Wellfounded Quotient Fun_Def
3.8 +imports Equiv_Relations Wellfounded Power Quotient Fun_Def
3.9  begin
3.10
3.11  subsection {* Definition of integers as a quotient type *}
```
```     4.1 --- a/src/HOL/Power.thy	Tue Jan 21 13:05:22 2014 +0100
4.2 +++ b/src/HOL/Power.thy	Tue Jan 21 13:21:55 2014 +0100
4.3 @@ -6,7 +6,7 @@
4.5
4.6  theory Power
4.7 -imports Num
4.8 +imports Num Equiv_Relations
4.9  begin
4.10
4.11  subsection {* Powers for Arbitrary Monoids *}
4.12 @@ -735,6 +735,66 @@
4.13    qed
4.14  qed
4.15
4.16 +subsubsection {* Cardinality of the Powerset *}
4.17 +
4.18 +lemma card_UNIV_bool [simp]: "card (UNIV :: bool set) = 2"
4.19 +  unfolding UNIV_bool by simp
4.20 +
4.21 +lemma card_Pow: "finite A \<Longrightarrow> card (Pow A) = 2 ^ card A"
4.22 +proof (induct rule: finite_induct)
4.23 +  case empty
4.24 +    show ?case by auto
4.25 +next
4.26 +  case (insert x A)
4.27 +  then have "inj_on (insert x) (Pow A)"
4.28 +    unfolding inj_on_def by (blast elim!: equalityE)
4.29 +  then have "card (Pow A) + card (insert x ` Pow A) = 2 * 2 ^ card A"
4.30 +    by (simp add: mult_2 card_image Pow_insert insert.hyps)
4.31 +  then show ?case using insert
4.32 +    apply (simp add: Pow_insert)
4.33 +    apply (subst card_Un_disjoint, auto)
4.34 +    done
4.35 +qed
4.36 +
4.37 +subsubsection {* Generalized product over a set *}
4.38 +
4.39 +lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
4.40 +apply (erule finite_induct)
4.41 +apply auto
4.42 +done
4.43 +
4.44 +lemma setprod_gen_delta:
4.45 +  assumes fS: "finite S"
4.46 +  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)"
4.47 +proof-
4.48 +  let ?f = "(\<lambda>k. if k=a then b k else c)"
4.49 +  {assume a: "a \<notin> S"
4.50 +    hence "\<forall> k\<in> S. ?f k = c" by simp
4.51 +    hence ?thesis  using a setprod_constant[OF fS, of c] by simp }
4.52 +  moreover
4.53 +  {assume a: "a \<in> S"
4.54 +    let ?A = "S - {a}"
4.55 +    let ?B = "{a}"
4.56 +    have eq: "S = ?A \<union> ?B" using a by blast
4.57 +    have dj: "?A \<inter> ?B = {}" by simp
4.58 +    from fS have fAB: "finite ?A" "finite ?B" by auto
4.59 +    have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
4.60 +      apply (rule setprod_cong) by auto
4.61 +    have cA: "card ?A = card S - 1" using fS a by auto
4.62 +    have fA1: "setprod ?f ?A = c ^ card ?A"  unfolding fA0 apply (rule setprod_constant) using fS by auto
4.63 +    have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
4.64 +      using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
4.65 +      by simp
4.66 +    then have ?thesis using a cA
4.67 +      by (simp add: fA1 field_simps cong add: setprod_cong cong del: if_weak_cong)}
4.68 +  ultimately show ?thesis by blast
4.69 +qed
4.70 +
4.71 +lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
4.72 +  by auto
4.73 +
4.74 +lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
4.75 +  by auto
4.76
4.77  subsection {* Code generator tweak *}
4.78
```
```     5.1 --- a/src/HOL/Relation.thy	Tue Jan 21 13:05:22 2014 +0100
5.2 +++ b/src/HOL/Relation.thy	Tue Jan 21 13:21:55 2014 +0100
5.3 @@ -930,12 +930,6 @@
5.4    "Domain r = {x. \<exists>y. (x, y) \<in> r}"
5.5    by blast
5.6
5.7 -lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
5.8 -  by auto
5.9 -
5.10 -lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
5.11 -  by auto
5.12 -
5.13
5.14  subsubsection {* Image of a set under a relation *}
5.15
```