src/HOL/Power.thy
changeset 55096 916b2ac758f4
parent 54489 03ff4d1e6784
child 55718 34618f031ba9
     1.1 --- a/src/HOL/Power.thy	Tue Jan 21 13:05:22 2014 +0100
     1.2 +++ b/src/HOL/Power.thy	Tue Jan 21 13:21:55 2014 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Exponentiation *}
     1.5  
     1.6  theory Power
     1.7 -imports Num
     1.8 +imports Num Equiv_Relations
     1.9  begin
    1.10  
    1.11  subsection {* Powers for Arbitrary Monoids *}
    1.12 @@ -735,6 +735,66 @@
    1.13    qed
    1.14  qed
    1.15  
    1.16 +subsubsection {* Cardinality of the Powerset *}
    1.17 +
    1.18 +lemma card_UNIV_bool [simp]: "card (UNIV :: bool set) = 2"
    1.19 +  unfolding UNIV_bool by simp
    1.20 +
    1.21 +lemma card_Pow: "finite A \<Longrightarrow> card (Pow A) = 2 ^ card A"
    1.22 +proof (induct rule: finite_induct)
    1.23 +  case empty 
    1.24 +    show ?case by auto
    1.25 +next
    1.26 +  case (insert x A)
    1.27 +  then have "inj_on (insert x) (Pow A)" 
    1.28 +    unfolding inj_on_def by (blast elim!: equalityE)
    1.29 +  then have "card (Pow A) + card (insert x ` Pow A) = 2 * 2 ^ card A" 
    1.30 +    by (simp add: mult_2 card_image Pow_insert insert.hyps)
    1.31 +  then show ?case using insert
    1.32 +    apply (simp add: Pow_insert)
    1.33 +    apply (subst card_Un_disjoint, auto)
    1.34 +    done
    1.35 +qed
    1.36 +
    1.37 +subsubsection {* Generalized product over a set *}
    1.38 +
    1.39 +lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
    1.40 +apply (erule finite_induct)
    1.41 +apply auto
    1.42 +done
    1.43 +
    1.44 +lemma setprod_gen_delta:
    1.45 +  assumes fS: "finite S"
    1.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)"
    1.47 +proof-
    1.48 +  let ?f = "(\<lambda>k. if k=a then b k else c)"
    1.49 +  {assume a: "a \<notin> S"
    1.50 +    hence "\<forall> k\<in> S. ?f k = c" by simp
    1.51 +    hence ?thesis  using a setprod_constant[OF fS, of c] by simp }
    1.52 +  moreover 
    1.53 +  {assume a: "a \<in> S"
    1.54 +    let ?A = "S - {a}"
    1.55 +    let ?B = "{a}"
    1.56 +    have eq: "S = ?A \<union> ?B" using a by blast 
    1.57 +    have dj: "?A \<inter> ?B = {}" by simp
    1.58 +    from fS have fAB: "finite ?A" "finite ?B" by auto  
    1.59 +    have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
    1.60 +      apply (rule setprod_cong) by auto
    1.61 +    have cA: "card ?A = card S - 1" using fS a by auto
    1.62 +    have fA1: "setprod ?f ?A = c ^ card ?A"  unfolding fA0 apply (rule setprod_constant) using fS by auto
    1.63 +    have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
    1.64 +      using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
    1.65 +      by simp
    1.66 +    then have ?thesis using a cA
    1.67 +      by (simp add: fA1 field_simps cong add: setprod_cong cong del: if_weak_cong)}
    1.68 +  ultimately show ?thesis by blast
    1.69 +qed
    1.70 +
    1.71 +lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
    1.72 +  by auto
    1.73 +
    1.74 +lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
    1.75 +  by auto
    1.76  
    1.77  subsection {* Code generator tweak *}
    1.78