# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# 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 (\<lambda>i j. disjnt (S i) (S j)) I"
   shows "(\<lambda>f. sum' f I) \<in> iso (sum_group I (\<lambda>i. free_Abelian_group(S i))) (free_Abelian_group (\<Union>(S ` I)))"
@@ -610,8 +609,7 @@
       done
     show "?h (x \<otimes>\<^bsub>?G\<^esub> y) = ?h x \<otimes>\<^bsub>?H\<^esub> ?h y"
       if "x \<in> carrier ?G" "y \<in> 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 \<in> Pi I A \<longleftrightarrow> x \<in> Pi I A"
   by (auto simp: restrict_def Pi_def)
 
+lemma sum_restrict' [simp]: "sum' (\<lambda>i\<in>I. g i) I = sum' (\<lambda>i. g i) I"
+  by (simp add: sum.G_def conj_commute cong: conj_cong)
+
+lemma prod_restrict' [simp]: "prod' (\<lambda>i\<in>I. g i) I = prod' (\<lambda>i. g i) I"
+  by (simp add: prod.G_def conj_commute cong: conj_cong)
+
 
 subsection \<open>Bijections Between Sets\<close>