# HG changeset patch # User paulson # Date 1554459713 -3600 # Node ID adaa0a6ea4fe4c6ba3df04069e6fd7694e3b5c42 # Parent 7b6add80e3a575310c354874aceca6b1a886b801 fixes for Free_Abelian_Groups diff -r 7b6add80e3a5 -r adaa0a6ea4fe src/HOL/Algebra/Algebra.thy --- a/src/HOL/Algebra/Algebra.thy Thu Apr 04 16:38:45 2019 +0100 +++ b/src/HOL/Algebra/Algebra.thy Fri Apr 05 11:21:53 2019 +0100 @@ -1,7 +1,7 @@ (* Title: HOL/Algebra/Algebra.thy *) theory Algebra - imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields Product_Groups + imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields Free_Abelian_Groups Divisibility Embedded_Algebras IntRing Sym_Groups Exact_Sequence Polynomials begin end diff -r 7b6add80e3a5 -r adaa0a6ea4fe src/HOL/Algebra/Free_Abelian_Groups.thy --- a/src/HOL/Algebra/Free_Abelian_Groups.thy Thu Apr 04 16:38:45 2019 +0100 +++ b/src/HOL/Algebra/Free_Abelian_Groups.thy Fri Apr 05 11:21:53 2019 +0100 @@ -2,7 +2,7 @@ theory Free_Abelian_Groups imports - Product_Groups "HOL-Cardinals.Cardinal_Arithmetic" + Product_Groups "../Cardinals/Cardinal_Arithmetic" "HOL-Library.Countable_Set" "HOL-Library.Poly_Mapping" "HOL-Library.Equipollence" begin @@ -594,7 +594,6 @@ by (auto simp: hom_def free_Abelian_group_def Pi_def) qed - proposition iso_free_Abelian_group_sum: assumes "pairwise (\i j. disjnt (S i) (S j)) I" shows "(\f. sum' f I) \ iso (sum_group I (\i. free_Abelian_group(S i))) (free_Abelian_group (\(S ` I)))" @@ -610,8 +609,7 @@ done show "?h (x \\<^bsub>?G\<^esub> y) = ?h x \\<^bsub>?H\<^esub> ?h y" if "x \ carrier ?G" "y \ carrier ?G" for x y - using that apply (simp add: sum.finite_Collect_op carrier_sum_group sum.distrib') - sorry + using that by (simp add: sum.finite_Collect_op carrier_sum_group sum.distrib') qed interpret GH: group_hom "?G" "?H" "?h" using hom by (simp add: group_hom_def group_hom_axioms_def) diff -r 7b6add80e3a5 -r adaa0a6ea4fe src/HOL/Library/FuncSet.thy --- a/src/HOL/Library/FuncSet.thy Thu Apr 04 16:38:45 2019 +0100 +++ b/src/HOL/Library/FuncSet.thy Fri Apr 05 11:21:53 2019 +0100 @@ -220,6 +220,12 @@ lemma restrict_Pi_cancel: "restrict x I \ Pi I A \ x \ Pi I A" by (auto simp: restrict_def Pi_def) +lemma sum_restrict' [simp]: "sum' (\i\I. g i) I = sum' (\i. g i) I" + by (simp add: sum.G_def conj_commute cong: conj_cong) + +lemma prod_restrict' [simp]: "prod' (\i\I. g i) I = prod' (\i. g i) I" + by (simp add: prod.G_def conj_commute cong: conj_cong) + subsection \Bijections Between Sets\