removed theory dependency of BNF_LFP on Datatype
authortraytel
Tue Jan 21 13:21:55 2014 +0100 (2014-01-21)
changeset 55096916b2ac758f4
parent 55094 149ccaf4ae5c
child 55097 81dac5c1a5bb
removed theory dependency of BNF_LFP on Datatype
src/HOL/Finite_Set.thy
src/HOL/Groups_Big.thy
src/HOL/Int.thy
src/HOL/Power.thy
src/HOL/Relation.thy
     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.4  header {* Exponentiation *}
     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