moved some finite lemmas here
authorhaftmann
Tue Jul 10 17:30:45 2007 +0200 (2007-07-10)
changeset 23706b7abba3c230e
parent 23705 315c638d5856
child 23707 745799215e02
moved some finite lemmas here
src/HOL/Finite_Set.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Tue Jul 10 17:30:43 2007 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Jul 10 17:30:45 2007 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  header {* Finite sets *}
     1.5  
     1.6  theory Finite_Set
     1.7 -imports Divides
     1.8 +imports Divides Equiv_Relations IntDef
     1.9  begin
    1.10  
    1.11  subsection {* Definition and basic properties *}
    1.12 @@ -2272,6 +2272,92 @@
    1.13  apply(simp add: neq_commute less_le)
    1.14  done
    1.15  
    1.16 +
    1.17 +subsection {* Finiteness and quotients *}
    1.18 +
    1.19 +text {*Suggested by Florian Kammüller*}
    1.20 +
    1.21 +lemma finite_quotient: "finite A ==> r \<subseteq> A \<times> A ==> finite (A//r)"
    1.22 +  -- {* recall @{thm equiv_type} *}
    1.23 +  apply (rule finite_subset)
    1.24 +   apply (erule_tac [2] finite_Pow_iff [THEN iffD2])
    1.25 +  apply (unfold quotient_def)
    1.26 +  apply blast
    1.27 +  done
    1.28 +
    1.29 +lemma finite_equiv_class:
    1.30 +  "finite A ==> r \<subseteq> A \<times> A ==> X \<in> A//r ==> finite X"
    1.31 +  apply (unfold quotient_def)
    1.32 +  apply (rule finite_subset)
    1.33 +   prefer 2 apply assumption
    1.34 +  apply blast
    1.35 +  done
    1.36 +
    1.37 +lemma equiv_imp_dvd_card:
    1.38 +  "finite A ==> equiv A r ==> \<forall>X \<in> A//r. k dvd card X
    1.39 +    ==> k dvd card A"
    1.40 +  apply (rule Union_quotient [THEN subst])
    1.41 +   apply assumption
    1.42 +  apply (rule dvd_partition)
    1.43 +     prefer 3 apply (blast dest: quotient_disj)
    1.44 +    apply (simp_all add: Union_quotient equiv_type)
    1.45 +  done
    1.46 +
    1.47 +lemma card_quotient_disjoint:
    1.48 + "\<lbrakk> finite A; inj_on (\<lambda>x. {x} // r) A \<rbrakk> \<Longrightarrow> card(A//r) = card A"
    1.49 +apply(simp add:quotient_def)
    1.50 +apply(subst card_UN_disjoint)
    1.51 +   apply assumption
    1.52 +  apply simp
    1.53 + apply(fastsimp simp add:inj_on_def)
    1.54 +apply (simp add:setsum_constant)
    1.55 +done
    1.56 +
    1.57 +
    1.58 +subsection {* @{term setsum} and @{term setprod} on integers *}
    1.59 +
    1.60 +text {*By Jeremy Avigad*}
    1.61 +
    1.62 +lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
    1.63 +  apply (cases "finite A")
    1.64 +  apply (erule finite_induct, auto)
    1.65 +  done
    1.66 +
    1.67 +lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
    1.68 +  apply (cases "finite A")
    1.69 +  apply (erule finite_induct, auto)
    1.70 +  done
    1.71 +
    1.72 +lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
    1.73 +  apply (cases "finite A")
    1.74 +  apply (erule finite_induct, auto simp add: of_nat_mult)
    1.75 +  done
    1.76 +
    1.77 +lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
    1.78 +  apply (cases "finite A")
    1.79 +  apply (erule finite_induct, auto)
    1.80 +  done
    1.81 +
    1.82 +lemma setprod_nonzero_nat:
    1.83 +    "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0"
    1.84 +  by (rule setprod_nonzero, auto)
    1.85 +
    1.86 +lemma setprod_zero_eq_nat:
    1.87 +    "finite A ==> (setprod f A = (0::nat)) = (\<exists>x \<in> A. f x = 0)"
    1.88 +  by (rule setprod_zero_eq, auto)
    1.89 +
    1.90 +lemma setprod_nonzero_int:
    1.91 +    "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::int)) ==> setprod f A \<noteq> 0"
    1.92 +  by (rule setprod_nonzero, auto)
    1.93 +
    1.94 +lemma setprod_zero_eq_int:
    1.95 +    "finite A ==> (setprod f A = (0::int)) = (\<exists>x \<in> A. f x = 0)"
    1.96 +  by (rule setprod_zero_eq, auto)
    1.97 +
    1.98 +lemmas int_setsum = of_nat_setsum [where 'a=int]
    1.99 +lemmas int_setprod = of_nat_setprod [where 'a=int]
   1.100 +
   1.101 +
   1.102  locale Lattice = lattice -- {* we do not pollute the @{text lattice} clas *}
   1.103  begin
   1.104