moved finite lemmas to Finite_Set.thy
authorhaftmann
Tue Jul 10 17:30:43 2007 +0200 (2007-07-10)
changeset 23705315c638d5856
parent 23704 18d6ee425689
child 23706 b7abba3c230e
moved finite lemmas to Finite_Set.thy
src/HOL/Equiv_Relations.thy
src/HOL/IntDef.thy
     1.1 --- a/src/HOL/Equiv_Relations.thy	Tue Jul 10 16:46:37 2007 +0200
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Tue Jul 10 17:30:43 2007 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Equivalence Relations in Higher-Order Set Theory *}
     1.5  
     1.6  theory Equiv_Relations
     1.7 -imports Relation Finite_Set
     1.8 +imports Relation
     1.9  begin
    1.10  
    1.11  subsection {* Equivalence relations *}
    1.12 @@ -292,83 +292,4 @@
    1.13           erule equivA [THEN equiv_type, THEN subsetD, THEN SigmaE2])+
    1.14    done
    1.15  
    1.16 -
    1.17 -subsection {* Cardinality results *}
    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 -ML
    1.58 -{*
    1.59 -val UN_UN_split_split_eq = thm "UN_UN_split_split_eq";
    1.60 -val UN_constant_eq = thm "UN_constant_eq";
    1.61 -val UN_equiv_class = thm "UN_equiv_class";
    1.62 -val UN_equiv_class2 = thm "UN_equiv_class2";
    1.63 -val UN_equiv_class_inject = thm "UN_equiv_class_inject";
    1.64 -val UN_equiv_class_type = thm "UN_equiv_class_type";
    1.65 -val UN_equiv_class_type2 = thm "UN_equiv_class_type2";
    1.66 -val Union_quotient = thm "Union_quotient";
    1.67 -val comp_equivI = thm "comp_equivI";
    1.68 -val congruent2I = thm "congruent2I";
    1.69 -val congruent2_commuteI = thm "congruent2_commuteI";
    1.70 -val congruent2_def = thm "congruent2_def";
    1.71 -val congruent2_implies_congruent = thm "congruent2_implies_congruent";
    1.72 -val congruent2_implies_congruent_UN = thm "congruent2_implies_congruent_UN";
    1.73 -val congruent_def = thm "congruent_def";
    1.74 -val eq_equiv_class = thm "eq_equiv_class";
    1.75 -val eq_equiv_class_iff = thm "eq_equiv_class_iff";
    1.76 -val equiv_class_eq = thm "equiv_class_eq";
    1.77 -val equiv_class_eq_iff = thm "equiv_class_eq_iff";
    1.78 -val equiv_class_nondisjoint = thm "equiv_class_nondisjoint";
    1.79 -val equiv_class_self = thm "equiv_class_self";
    1.80 -val equiv_comp_eq = thm "equiv_comp_eq";
    1.81 -val equiv_def = thm "equiv_def";
    1.82 -val equiv_imp_dvd_card = thm "equiv_imp_dvd_card";
    1.83 -val equiv_type = thm "equiv_type";
    1.84 -val finite_equiv_class = thm "finite_equiv_class";
    1.85 -val finite_quotient = thm "finite_quotient";
    1.86 -val quotientE = thm "quotientE";
    1.87 -val quotientI = thm "quotientI";
    1.88 -val quotient_def = thm "quotient_def";
    1.89 -val quotient_disj = thm "quotient_disj";
    1.90 -val refl_comp_subset = thm "refl_comp_subset";
    1.91 -val subset_equiv_class = thm "subset_equiv_class";
    1.92 -val sym_trans_comp_subset = thm "sym_trans_comp_subset";
    1.93 -*}
    1.94 -*)
    1.95  end
     2.1 --- a/src/HOL/IntDef.thy	Tue Jul 10 16:46:37 2007 +0200
     2.2 +++ b/src/HOL/IntDef.thy	Tue Jul 10 17:30:43 2007 +0200
     2.3 @@ -11,6 +11,7 @@
     2.4  imports Equiv_Relations Nat
     2.5  begin
     2.6  
     2.7 +
     2.8  text {* the equivalence relation underlying the integers *}
     2.9  
    2.10  definition
    2.11 @@ -622,52 +623,6 @@
    2.12    by (rule Ints_cases) auto
    2.13  
    2.14  
    2.15 -(* int (Suc n) = 1 + int n *)
    2.16 -
    2.17 -
    2.18 -
    2.19 -subsection{*More Properties of @{term setsum} and  @{term setprod}*}
    2.20 -
    2.21 -text{*By Jeremy Avigad*}
    2.22 -
    2.23 -
    2.24 -lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
    2.25 -  apply (cases "finite A")
    2.26 -  apply (erule finite_induct, auto)
    2.27 -  done
    2.28 -
    2.29 -lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
    2.30 -  apply (cases "finite A")
    2.31 -  apply (erule finite_induct, auto)
    2.32 -  done
    2.33 -
    2.34 -lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
    2.35 -  apply (cases "finite A")
    2.36 -  apply (erule finite_induct, auto simp add: of_nat_mult)
    2.37 -  done
    2.38 -
    2.39 -lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
    2.40 -  apply (cases "finite A")
    2.41 -  apply (erule finite_induct, auto)
    2.42 -  done
    2.43 -
    2.44 -lemma setprod_nonzero_nat:
    2.45 -    "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0"
    2.46 -  by (rule setprod_nonzero, auto)
    2.47 -
    2.48 -lemma setprod_zero_eq_nat:
    2.49 -    "finite A ==> (setprod f A = (0::nat)) = (\<exists>x \<in> A. f x = 0)"
    2.50 -  by (rule setprod_zero_eq, auto)
    2.51 -
    2.52 -lemma setprod_nonzero_int:
    2.53 -    "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::int)) ==> setprod f A \<noteq> 0"
    2.54 -  by (rule setprod_nonzero, auto)
    2.55 -
    2.56 -lemma setprod_zero_eq_int:
    2.57 -    "finite A ==> (setprod f A = (0::int)) = (\<exists>x \<in> A. f x = 0)"
    2.58 -  by (rule setprod_zero_eq, auto)
    2.59 -
    2.60 -
    2.61  subsection {* Further properties *}
    2.62  
    2.63  text{*Now we replace the case analysis rule by a more conventional one:
    2.64 @@ -766,8 +721,6 @@
    2.65  lemmas int_Suc = of_nat_Suc [where ?'a_1.0=int]
    2.66  lemmas abs_int_eq = abs_of_nat [where 'a=int and n="?m"]
    2.67  lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
    2.68 -lemmas int_setsum = of_nat_setsum [where 'a=int]
    2.69 -lemmas int_setprod = of_nat_setprod [where 'a=int]
    2.70  lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
    2.71  lemmas zless_le = less_int_def [THEN meta_eq_to_obj_eq]
    2.72  lemmas int_eq_of_nat = TrueI