merged
authorpaulson
Fri, 05 Apr 2019 11:22:00 +0100
changeset 70246 1a85c1495d1f
parent 70243 5b75480f371a (current diff)
parent 70245 adaa0a6ea4fe (diff)
child 70247 cc89a395b5a3
merged
--- a/src/HOL/Algebra/Algebra.thy	Thu Apr 04 23:05:53 2019 +0200
+++ b/src/HOL/Algebra/Algebra.thy	Fri Apr 05 11:22:00 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
--- a/src/HOL/Algebra/Free_Abelian_Groups.thy	Thu Apr 04 23:05:53 2019 +0200
+++ b/src/HOL/Algebra/Free_Abelian_Groups.thy	Fri Apr 05 11:22:00 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)
--- a/src/HOL/Library/FuncSet.thy	Thu Apr 04 23:05:53 2019 +0200
+++ b/src/HOL/Library/FuncSet.thy	Fri Apr 05 11:22:00 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>