merged
authorwenzelm
Thu, 04 Apr 2019 22:21:09 +0200
changeset 70059 06edf32c6057
parent 70045 7b6add80e3a5 (diff)
parent 70058 43acf9a457f0 (current diff)
child 70060 3e9394adcccd
merged
--- a/src/HOL/Algebra/Algebra.thy	Thu Apr 04 22:18:32 2019 +0200
+++ b/src/HOL/Algebra/Algebra.thy	Thu Apr 04 22:21:09 2019 +0200
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Algebra/Algebra.thy *)
 
 theory Algebra
-  imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields Elementary_Groups
+  imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields Product_Groups
      Divisibility Embedded_Algebras IntRing Sym_Groups Exact_Sequence Polynomials
 begin
 end
--- a/src/HOL/Algebra/Coset.thy	Thu Apr 04 22:18:32 2019 +0200
+++ b/src/HOL/Algebra/Coset.thy	Thu Apr 04 22:21:09 2019 +0200
@@ -1061,6 +1061,26 @@
   apply (simp add: kernel_def)
   done
 
+lemma iso_kernel_image:
+  assumes "group G" "group H"
+  shows "f \<in> iso G H \<longleftrightarrow> f \<in> hom G H \<and> kernel G H f = {\<one>\<^bsub>G\<^esub>} \<and> f ` carrier G = carrier H"
+    (is "?lhs = ?rhs")
+proof (intro iffI conjI)
+  assume f: ?lhs
+  show "f \<in> hom G H"
+    using Group.iso_iff f by blast
+  show "kernel G H f = {\<one>\<^bsub>G\<^esub>}"
+    using assms f Group.group_def hom_one
+    by (fastforce simp add: kernel_def iso_iff_mon_epi mon_iff_hom_one set_eq_iff)
+  show "f ` carrier G = carrier H"
+    by (meson Group.iso_iff f)
+next
+  assume ?rhs
+  with assms show ?lhs
+    by (auto simp: kernel_def iso_def bij_betw_def inj_on_one_iff')
+qed
+
+
 lemma (in group_hom) FactGroup_nonempty:
   assumes X: "X \<in> carrier (G Mod kernel G H h)"
   shows "X \<noteq> {}"
@@ -1083,7 +1103,7 @@
   proof -
     have "x \<otimes>\<^bsub>G\<^esub> inv\<^bsub>G\<^esub> y \<in> N"
       using \<open>N \<lhd> G\<close> group.rcos_self normal.axioms(2) normal_imp_subgroup
-         subgroup.rcos_module_imp that by fastforce
+         subgroup.rcos_module_imp that by metis 
     with h have xy: "x \<otimes>\<^bsub>G\<^esub> inv\<^bsub>G\<^esub> y \<in> kernel G H h"
       by blast
     have "h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub>(h y) = h (x \<otimes>\<^bsub>G\<^esub> inv\<^bsub>G\<^esub> y)"
@@ -1221,7 +1241,6 @@
     using A G.inv_equality G.inv_inv by blast
 qed
 
-(* NEW ========================================================================== *)
 lemma (in group_hom) inj_iff_trivial_ker:
   shows "inj_on h (carrier G) \<longleftrightarrow> kernel G H h = { \<one> }"
 proof
@@ -1236,7 +1255,6 @@
     using trivial_ker_imp_inj by simp
 qed
 
-(* NEW ========================================================================== *)
 lemma (in group_hom) induced_group_hom':
   assumes "subgroup I G" shows "group_hom (G \<lparr> carrier := I \<rparr>) H h"
 proof -
@@ -1247,13 +1265,11 @@
     unfolding group_hom_def group_hom_axioms_def by auto
 qed
 
-(* NEW ========================================================================== *)
 lemma (in group_hom) inj_on_subgroup_iff_trivial_ker:
   assumes "subgroup I G"
   shows "inj_on h I \<longleftrightarrow> kernel (G \<lparr> carrier := I \<rparr>) H h = { \<one> }"
   using group_hom.inj_iff_trivial_ker[OF induced_group_hom'[OF assms]] by simp
 
-(* NEW ========================================================================== *)
 lemma set_mult_hom:
   assumes "h \<in> hom G H" "I \<subseteq> carrier G" and "J \<subseteq> carrier G"
   shows "h ` (I <#>\<^bsub>G\<^esub> J) = (h ` I) <#>\<^bsub>H\<^esub> (h ` J)"
@@ -1281,13 +1297,11 @@
   qed
 qed
 
-(* NEW ========================================================================== *)
 corollary coset_hom:
   assumes "h \<in> hom G H" "I \<subseteq> carrier G" "a \<in> carrier G"
   shows "h ` (a <#\<^bsub>G\<^esub> I) = h a <#\<^bsub>H\<^esub> (h ` I)" and "h ` (I #>\<^bsub>G\<^esub> a) = (h ` I) #>\<^bsub>H\<^esub> h a"
   unfolding l_coset_eq_set_mult r_coset_eq_set_mult using assms set_mult_hom[OF assms(1)] by auto
 
-(* NEW ========================================================================== *)
 corollary (in group_hom) set_mult_ker_hom:
   assumes "I \<subseteq> carrier G"
   shows "h ` (I <#> (kernel G H h)) = h ` I" and "h ` ((kernel G H h) <#> I) = h ` I"
@@ -1305,8 +1319,145 @@
     using set_mult_hom[OF homh assms ker_in_carrier] set_mult_hom[OF homh ker_in_carrier assms] by simp+
 qed
 
+subsubsection\<open>Trivial homomorphisms\<close>
 
-subsection \<open>Theorems about Factor Groups and Direct product\<close>
+definition trivial_homomorphism where
+ "trivial_homomorphism G H f \<equiv> f \<in> hom G H \<and> (\<forall>x \<in> carrier G. f x = one H)"
+
+lemma trivial_homomorphism_kernel:
+   "trivial_homomorphism G H f \<longleftrightarrow> f \<in> hom G H \<and> kernel G H f = carrier G"
+  by (auto simp: trivial_homomorphism_def kernel_def)
+
+lemma (in group) trivial_homomorphism_image:
+   "trivial_homomorphism G H f \<longleftrightarrow> f \<in> hom G H \<and> f ` carrier G = {one H}"
+  by (auto simp: trivial_homomorphism_def) (metis one_closed rev_image_eqI)
+
+
+subsection \<open>Image kernel theorems\<close>
+
+lemma group_Int_image_ker:
+  assumes f: "f \<in> hom G H" and g: "g \<in> hom H K" and "inj_on (g \<circ> f) (carrier G)" "group G" "group H" "group K"
+  shows "(f ` carrier G) \<inter> (kernel H K g) = {\<one>\<^bsub>H\<^esub>}"
+proof -
+  have "(f ` carrier G) \<inter> (kernel H K g) \<subseteq> {\<one>\<^bsub>H\<^esub>}"
+    using assms
+    apply (clarsimp simp: kernel_def o_def)
+    by (metis group.is_monoid hom_one inj_on_eq_iff monoid.one_closed)
+  moreover have "one H \<in> f ` carrier G"
+    by (metis f \<open>group G\<close> \<open>group H\<close> group.is_monoid hom_one image_iff monoid.one_closed)
+  moreover have "one H \<in> kernel H K g"
+    apply (simp add: kernel_def)
+    using g group.is_monoid hom_one \<open>group H\<close> \<open>group K\<close> by blast
+  ultimately show ?thesis
+    by blast
+qed
+
+
+lemma group_sum_image_ker:
+  assumes f: "f \<in> hom G H" and g: "g \<in> hom H K" and eq: "(g \<circ> f) ` (carrier G) = carrier K"
+     and "group G" "group H" "group K"
+  shows "set_mult H (f ` carrier G) (kernel H K g) = carrier H" (is "?lhs = ?rhs")
+proof
+  show "?lhs \<subseteq> ?rhs"
+    apply (auto simp: kernel_def set_mult_def)
+    by (meson Group.group_def assms(5) f hom_carrier image_eqI monoid.m_closed subset_iff)
+  have "\<exists>x\<in>carrier G. \<exists>z. z \<in> carrier H \<and> g z = \<one>\<^bsub>K\<^esub> \<and> y = f x \<otimes>\<^bsub>H\<^esub> z"
+    if y: "y \<in> carrier H" for y
+  proof -
+    have "g y \<in> carrier K"
+      using g hom_carrier that by blast
+    with assms obtain x where x: "x \<in> carrier G" "(g \<circ> f) x = g y"
+      by (metis image_iff)
+    with assms have "inv\<^bsub>H\<^esub> f x \<otimes>\<^bsub>H\<^esub> y \<in> carrier H"
+      by (metis group.subgroup_self hom_carrier image_subset_iff subgroup_def y)
+    moreover
+    have "g (inv\<^bsub>H\<^esub> f x \<otimes>\<^bsub>H\<^esub> y) = \<one>\<^bsub>K\<^esub>"
+    proof -
+      have "inv\<^bsub>H\<^esub> f x \<in> carrier H"
+        by (meson \<open>group H\<close> f group.inv_closed hom_carrier image_subset_iff x(1))
+      then have "g (inv\<^bsub>H\<^esub> f x \<otimes>\<^bsub>H\<^esub> y) = g (inv\<^bsub>H\<^esub> f x) \<otimes>\<^bsub>K\<^esub> g y"
+        by (simp add: hom_mult [OF g] y)
+      also have "\<dots> = inv\<^bsub>K\<^esub> (g (f x)) \<otimes>\<^bsub>K\<^esub> g y"
+        using assms x(1)
+        by (metis (mono_tags, lifting) group_hom.hom_inv group_hom.intro group_hom_axioms.intro hom_carrier image_subset_iff)
+      also have "\<dots> = \<one>\<^bsub>K\<^esub>"
+        using \<open>g y \<in> carrier K\<close> assms(6) group.l_inv x(2) by fastforce
+      finally show ?thesis .
+    qed
+    moreover
+    have "y = f x \<otimes>\<^bsub>H\<^esub> (inv\<^bsub>H\<^esub> f x \<otimes>\<^bsub>H\<^esub> y)"
+      using x y
+      by (metis (no_types, hide_lams) assms(5) f group.inv_solve_left group.subgroup_self hom_carrier image_subset_iff subgroup_def that)
+    ultimately
+    show ?thesis
+      using x y by force
+  qed
+  then show "?rhs \<subseteq> ?lhs"
+    by (auto simp: kernel_def set_mult_def)
+qed
+
+
+lemma group_sum_ker_image:
+  assumes f: "f \<in> hom G H" and g: "g \<in> hom H K" and eq: "(g \<circ> f) ` (carrier G) = carrier K"
+     and "group G" "group H" "group K"
+   shows "set_mult H (kernel H K g) (f ` carrier G) = carrier H" (is "?lhs = ?rhs")
+proof
+  show "?lhs \<subseteq> ?rhs"
+    apply (auto simp: kernel_def set_mult_def)
+    by (meson Group.group_def \<open>group H\<close> f hom_carrier image_eqI monoid.m_closed subset_iff)
+  have "\<exists>w\<in>carrier H. \<exists>x \<in> carrier G. g w = \<one>\<^bsub>K\<^esub> \<and> y = w \<otimes>\<^bsub>H\<^esub> f x"
+    if y: "y \<in> carrier H" for y
+  proof -
+    have "g y \<in> carrier K"
+      using g hom_carrier that by blast
+    with assms obtain x where x: "x \<in> carrier G" "(g \<circ> f) x = g y"
+      by (metis image_iff)
+    with assms have carr: "(y \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> f x) \<in> carrier H"
+      by (metis group.subgroup_self hom_carrier image_subset_iff subgroup_def y)
+    moreover
+    have "g (y \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> f x) = \<one>\<^bsub>K\<^esub>"
+    proof -
+      have "inv\<^bsub>H\<^esub> f x \<in> carrier H"
+        by (meson \<open>group H\<close> f group.inv_closed hom_carrier image_subset_iff x(1))
+      then have "g (y \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> f x) = g y \<otimes>\<^bsub>K\<^esub> g (inv\<^bsub>H\<^esub> f x)"
+        by (simp add: hom_mult [OF g] y)
+      also have "\<dots> = g y \<otimes>\<^bsub>K\<^esub> inv\<^bsub>K\<^esub> (g (f x))"
+        using assms x(1)
+        by (metis (mono_tags, lifting) group_hom.hom_inv group_hom.intro group_hom_axioms.intro hom_carrier image_subset_iff)
+      also have "\<dots> = \<one>\<^bsub>K\<^esub>"
+        using \<open>g y \<in> carrier K\<close> assms(6) group.l_inv x(2)
+        by (simp add: group.r_inv)
+      finally show ?thesis .
+    qed
+    moreover
+    have "y = (y \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> f x) \<otimes>\<^bsub>H\<^esub> f x"
+      using x y by (meson \<open>group H\<close> carr f group.inv_solve_right hom_carrier image_subset_iff)
+    ultimately
+    show ?thesis
+      using x y by force
+  qed
+  then show "?rhs \<subseteq> ?lhs"
+    by (force simp: kernel_def set_mult_def)
+qed
+
+lemma group_semidirect_sum_ker_image:
+  assumes "(g \<circ> f) \<in> iso G K" "f \<in> hom G H" "g \<in> hom H K" "group G" "group H" "group K"
+  shows "(kernel H K g) \<inter> (f ` carrier G) = {\<one>\<^bsub>H\<^esub>}"
+        "kernel H K g <#>\<^bsub>H\<^esub> (f ` carrier G) = carrier H"
+  using assms
+  by (simp_all add: iso_iff_mon_epi group_Int_image_ker group_sum_ker_image epi_def mon_def Int_commute [of "kernel H K g"])
+
+lemma group_semidirect_sum_image_ker:
+  assumes f: "f \<in> hom G H" and g: "g \<in> hom H K" and iso: "(g \<circ> f) \<in> iso G K"
+     and "group G" "group H" "group K"
+   shows "(f ` carrier G) \<inter> (kernel H K g) = {\<one>\<^bsub>H\<^esub>}"
+          "f ` carrier G <#>\<^bsub>H\<^esub> (kernel H K g) = carrier H"
+  using group_Int_image_ker [OF f g] group_sum_image_ker [OF f g] assms
+  by (simp_all add: iso_def bij_betw_def)
+
+
+
+subsection \<open>Factor Groups and Direct product\<close>
 
 lemma (in group) DirProd_normal : \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
   assumes "group K"
--- a/src/HOL/Algebra/Elementary_Groups.thy	Thu Apr 04 22:18:32 2019 +0200
+++ b/src/HOL/Algebra/Elementary_Groups.thy	Thu Apr 04 22:21:09 2019 +0200
@@ -5,7 +5,7 @@
 *)
 
 theory Elementary_Groups
-imports Generated_Groups
+imports Generated_Groups Multiplicative_Group "HOL-Library.Infinite_Set"
 begin
 
 subsection\<open>Direct sum/product lemmas\<close>
@@ -379,4 +379,289 @@
    "x \<in> carrier G \<Longrightarrow> pow G x \<in> hom integer_group G"
   by (rule homI) (auto simp: int_pow_mult)
 
+subsection\<open>Additive group of integers modulo n (n = 0 gives just the integers)\<close>
+
+definition integer_mod_group :: "nat \<Rightarrow> int monoid"
+  where
+  "integer_mod_group n \<equiv>
+     if n = 0 then integer_group
+     else \<lparr>carrier = {0..<int n}, monoid.mult = (\<lambda>x y. (x+y) mod int n), one = 0\<rparr>"
+
+lemma carrier_integer_mod_group:
+  "carrier(integer_mod_group n) = (if n=0 then UNIV else {0..<int n})"
+  by (simp add: integer_mod_group_def)
+
+lemma one_integer_mod_group[simp]: "one(integer_mod_group n) = 0"
+  by (simp add: integer_mod_group_def)
+
+lemma mult_integer_mod_group[simp]: "monoid.mult(integer_mod_group n) = (\<lambda>x y. (x + y) mod int n)"
+  by (simp add: integer_mod_group_def integer_group_def)
+
+lemma group_integer_mod_group [simp]: "group (integer_mod_group n)"
+proof -
+  have *: "\<exists>y\<ge>0. y < int n \<and> (y + x) mod int n = 0" if "x < int n" "0 \<le> x" for x
+  proof (cases "x=0")
+    case False
+    with that show ?thesis
+      by (rule_tac x="int n - x" in exI) auto
+  qed (use that in auto)
+  show ?thesis
+    apply (rule groupI)
+        apply (auto simp: integer_mod_group_def Bex_def *, presburger+)
+    done
+qed
+
+lemma inv_integer_mod_group[simp]:
+  "x \<in> carrier (integer_mod_group n) \<Longrightarrow> m_inv(integer_mod_group n) x = (-x) mod int n"
+  by (rule group.inv_equality [OF group_integer_mod_group]) (auto simp: integer_mod_group_def add.commute mod_add_right_eq)
+
+
+lemma pow_integer_mod_group [simp]:
+  fixes m::nat
+  shows "pow (integer_mod_group n) x m = (int m * x) mod int n"
+proof (cases "n=0")
+  case False
+  show ?thesis
+    by (induction m) (auto simp: add.commute mod_add_right_eq distrib_left mult.commute)
+qed (simp add: integer_mod_group_def)
+
+lemma int_pow_integer_mod_group:
+  "pow (integer_mod_group n) x m = (m * x) mod int n"
+proof -
+  have "inv\<^bsub>integer_mod_group n\<^esub> (- (m * x) mod int n) = m * x mod int n"
+    by (simp add: carrier_integer_mod_group mod_minus_eq)
+  then show ?thesis
+    by (simp add: int_pow_def2)
+qed
+
+lemma abelian_integer_mod_group [simp]: "comm_group(integer_mod_group n)"
+  by (simp add: add.commute group.group_comm_groupI)
+
+lemma integer_mod_group_0 [simp]: "0 \<in> carrier(integer_mod_group n)"
+  by (simp add: integer_mod_group_def)
+
+lemma integer_mod_group_1 [simp]: "1 \<in> carrier(integer_mod_group n) \<longleftrightarrow> (n \<noteq> 1)"
+  by (auto simp: integer_mod_group_def)
+
+lemma trivial_integer_mod_group: "trivial_group(integer_mod_group n) \<longleftrightarrow> n = 1"
+  (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+  by (simp add: trivial_group_def carrier_integer_mod_group set_eq_iff split: if_split_asm) (presburger+)
+next
+  assume ?rhs
+  then show ?lhs
+    by (force simp: trivial_group_def carrier_integer_mod_group)
+qed
+
+
+subsection\<open>Cyclic groups\<close>
+
+lemma (in group) subgroup_of_powers:
+  "x \<in> carrier G \<Longrightarrow> subgroup (range (\<lambda>n::int. x [^] n)) G"
+  apply (auto simp: subgroup_def image_iff simp flip: int_pow_mult int_pow_neg)
+  apply (metis group.int_pow_diff int_pow_closed is_group r_inv)
+  done
+
+lemma (in group) carrier_subgroup_generated_by_singleton:
+  assumes "x \<in> carrier G"
+  shows "carrier(subgroup_generated G {x}) = (range (\<lambda>n::int. x [^] n))"
+proof
+  show "carrier (subgroup_generated G {x}) \<subseteq> range (\<lambda>n::int. x [^] n)"
+  proof (rule subgroup_generated_minimal)
+    show "subgroup (range (\<lambda>n::int. x [^] n)) G"
+      using assms subgroup_of_powers by blast
+    show "{x} \<subseteq> range (\<lambda>n::int. x [^] n)"
+      by clarify (metis assms int_pow_1 range_eqI)
+  qed
+  have x: "x \<in> carrier (subgroup_generated G {x})"
+    using assms subgroup_generated_subset_carrier_subset by auto
+  show "range (\<lambda>n::int. x [^] n) \<subseteq> carrier (subgroup_generated G {x})"
+  proof clarify
+    fix n :: "int"
+    show "x [^] n \<in> carrier (subgroup_generated G {x})"
+        by (simp add: x subgroup_int_pow_closed subgroup_subgroup_generated)
+  qed
+qed
+
+
+definition cyclic_group
+  where "cyclic_group G \<equiv> \<exists>x \<in> carrier G. subgroup_generated G {x} = G"
+
+lemma (in group) cyclic_group:
+  "cyclic_group G \<longleftrightarrow> (\<exists>x \<in> carrier G. carrier G = range (\<lambda>n::int. x [^] n))"
+proof -
+  have "\<And>x. \<lbrakk>x \<in> carrier G; carrier G = range (\<lambda>n::int. x [^] n)\<rbrakk>
+         \<Longrightarrow> \<exists>x\<in>carrier G. subgroup_generated G {x} = G"
+    by (rule_tac x=x in bexI) (auto simp: generate_pow subgroup_generated_def intro!: monoid.equality)
+  then show ?thesis
+    unfolding cyclic_group_def
+    using carrier_subgroup_generated_by_singleton by fastforce
+qed
+
+lemma cyclic_integer_group [simp]: "cyclic_group integer_group"
+proof -
+  have *: "int n \<in> generate integer_group {1}" for n
+  proof (induction n)
+    case 0
+    then show ?case
+    using generate.simps by force
+  next
+    case (Suc n)
+    then show ?case
+    by simp (metis generate.simps insert_subset integer_group_def monoid.simps(1) subsetI)
+  qed
+  have **: "i \<in> generate integer_group {1}" for i
+  proof (cases i rule: int_cases)
+    case (nonneg n)
+    then show ?thesis
+      by (simp add: *)
+  next
+    case (neg n)
+    then have "-i \<in> generate integer_group {1}"
+      by (metis "*" add.inverse_inverse)
+    then have "- (-i) \<in> generate integer_group {1}"
+      by (metis UNIV_I group.generate_m_inv_closed group_integer_group integer_group_def inv_integer_group partial_object.select_convs(1) subsetI)
+    then show ?thesis
+      by simp
+  qed
+  show ?thesis
+    unfolding cyclic_group_def
+    by (rule_tac x=1 in bexI)
+       (auto simp: carrier_subgroup_generated ** intro: monoid.equality)
+qed
+
+lemma nontrivial_integer_group [simp]: "\<not> trivial_group integer_group"
+  using integer_mod_group_def trivial_integer_mod_group by presburger
+
+
+lemma (in group) cyclic_imp_abelian_group:
+  "cyclic_group G \<Longrightarrow> comm_group G"
+  apply (auto simp: cyclic_group comm_group_def is_group intro!: monoid_comm_monoidI)
+  apply (metis add.commute int_pow_mult rangeI)
+  done
+
+lemma trivial_imp_cyclic_group:
+   "trivial_group G \<Longrightarrow> cyclic_group G"
+  by (metis cyclic_group_def group.subgroup_generated_group_carrier insertI1 trivial_group_def)
+
+lemma (in group) cyclic_group_alt:
+   "cyclic_group G \<longleftrightarrow> (\<exists>x. subgroup_generated G {x} = G)"
+proof safe
+  fix x
+  assume *: "subgroup_generated G {x} = G"
+  show "cyclic_group G"
+  proof (cases "x \<in> carrier G")
+    case True
+    then show ?thesis
+      using \<open>subgroup_generated G {x} = G\<close> cyclic_group_def by blast
+  next
+    case False
+    then show ?thesis
+      by (metis "*" Int_empty_right Int_insert_right_if0 carrier_subgroup_generated generate_empty trivial_group trivial_imp_cyclic_group)
+  qed
+qed (auto simp: cyclic_group_def)
+
+lemma (in group) cyclic_group_generated:
+  "cyclic_group (subgroup_generated G {x})"
+  using group.cyclic_group_alt group_subgroup_generated subgroup_generated2 by blast
+
+lemma (in group) cyclic_group_epimorphic_image:
+  assumes "h \<in> epi G H" "cyclic_group G" "group H"
+  shows "cyclic_group H"
+proof -
+  interpret h: group_hom
+    using assms
+    by (simp add: group_hom_def group_hom_axioms_def is_group epi_def)
+  obtain x where "x \<in> carrier G" and x: "carrier G = range (\<lambda>n::int. x [^] n)" and eq: "carrier H = h ` carrier G"
+    using assms by (auto simp: cyclic_group epi_def)
+  have "h ` carrier G = range (\<lambda>n::int. h x [^]\<^bsub>H\<^esub> n)"
+    by (metis (no_types, lifting) \<open>x \<in> carrier G\<close> h.hom_int_pow image_cong image_image x)
+  then show ?thesis
+    using \<open>x \<in> carrier G\<close> eq h.cyclic_group by blast
+qed
+
+lemma isomorphic_group_cyclicity:
+   "\<lbrakk>G \<cong> H; group G; group H\<rbrakk> \<Longrightarrow> cyclic_group G \<longleftrightarrow> cyclic_group H"
+  by (meson ex_in_conv group.cyclic_group_epimorphic_image group.iso_sym is_iso_def iso_iff_mon_epi)
+
+
+lemma (in group)
+  assumes "x \<in> carrier G"
+  shows finite_cyclic_subgroup:
+        "finite(carrier(subgroup_generated G {x})) \<longleftrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> x [^] n = \<one>)" (is "?fin \<longleftrightarrow> ?nat1")
+    and infinite_cyclic_subgroup:
+        "infinite(carrier(subgroup_generated G {x})) \<longleftrightarrow> (\<forall>m n::nat. x [^] m = x [^] n \<longrightarrow> m = n)" (is "\<not> ?fin \<longleftrightarrow> ?nateq")
+    and finite_cyclic_subgroup_int:
+        "finite(carrier(subgroup_generated G {x})) \<longleftrightarrow> (\<exists>i::int. i \<noteq> 0 \<and> x [^] i = \<one>)" (is "?fin \<longleftrightarrow> ?int1")
+    and infinite_cyclic_subgroup_int:
+        "infinite(carrier(subgroup_generated G {x})) \<longleftrightarrow> (\<forall>i j::int. x [^] i = x [^] j \<longrightarrow> i = j)" (is "\<not> ?fin \<longleftrightarrow> ?inteq")
+proof -
+  have 1: "\<not> ?fin" if ?nateq
+  proof -
+    have "infinite (range (\<lambda>n::nat. x [^] n))"
+      using that range_inj_infinite [of "(\<lambda>n::nat. x [^] n)"] by (auto simp: inj_on_def)
+    moreover have "range (\<lambda>n::nat. x [^] n) \<subseteq> range (\<lambda>i::int. x [^] i)"
+      apply clarify
+      by (metis assms group.int_pow_neg int_pow_closed int_pow_neg_int is_group local.inv_equality nat_pow_closed r_inv rangeI)
+    ultimately show ?thesis
+      using carrier_subgroup_generated_by_singleton [OF assms] finite_subset by auto
+  qed
+  have 2: "m = n" if mn: "x [^] m = x [^] n" and eq [rule_format]: "?inteq" for m n::nat
+    using eq [of "int m" "int n"]
+    by (simp add: int_pow_int mn)
+  have 3: ?nat1 if non: "\<not> ?inteq"
+  proof -
+    obtain i j::int where eq: "x [^] i = x [^] j" and "i \<noteq> j"
+      using non by auto
+    show ?thesis
+    proof (cases i j rule: linorder_cases)
+      case less
+      then have [simp]: "x [^] (j - i) = \<one>"
+        by (simp add: eq assms int_pow_diff)
+      show ?thesis
+        using less by (rule_tac x="nat (j-i)" in exI) auto
+    next
+      case greater
+      then have [simp]: "x [^] (i - j) = \<one>"
+        by (simp add: eq assms int_pow_diff)
+      then show ?thesis
+        using greater by (rule_tac x="nat (i-j)" in exI) auto
+    qed (use \<open>i \<noteq> j\<close> in auto)
+  qed
+  have 4: "\<exists>i::int. (i \<noteq> 0) \<and> x [^] i = \<one>" if "n \<noteq> 0" "x [^] n = \<one>" for n::nat
+    apply (rule_tac x="int n" in exI)
+    by (simp add: int_pow_int that)
+  have 5: "finite (carrier (subgroup_generated G {x}))" if "i \<noteq> 0" and 1: "x [^] i = \<one>" for i::int
+  proof -
+    obtain n::nat where n: "n > 0" "x [^] n = \<one>"
+      using "1" "3" \<open>i \<noteq> 0\<close> by fastforce
+    have "x [^] a \<in> ([^]) x ` {0..<n}" for a::int
+    proof
+      show "x [^] a = x [^] nat (a mod int n)"
+        using n
+        by simp (metis (no_types, lifting) assms dvd_minus_mod dvd_trans int_pow_eq int_pow_eq_id int_pow_int)
+      show "nat (a mod int n) \<in> {0..<n}"
+        using n  apply (simp add:  split: split_nat)
+        using Euclidean_Division.pos_mod_bound by presburger
+    qed
+    then have "carrier (subgroup_generated G {x}) \<subseteq> ([^]) x ` {0..<n}"
+      using carrier_subgroup_generated_by_singleton [OF assms] by auto
+    then show ?thesis
+      using finite_surj by blast
+  qed
+  show "?fin \<longleftrightarrow> ?nat1" "\<not> ?fin \<longleftrightarrow> ?nateq" "?fin \<longleftrightarrow> ?int1" "\<not> ?fin \<longleftrightarrow> ?inteq"
+    using 1 2 3 4 5 by meson+
+qed
+
+lemma (in group) finite_cyclic_subgroup_order:
+   "x \<in> carrier G \<Longrightarrow> finite(carrier(subgroup_generated G {x})) \<longleftrightarrow> ord x \<noteq> 0"
+  by (simp add: finite_cyclic_subgroup ord_eq_0)
+
+lemma (in group) infinite_cyclic_subgroup_order:
+   "x \<in> carrier G \<Longrightarrow> infinite (carrier(subgroup_generated G {x})) \<longleftrightarrow> ord x = 0"
+  by (simp add: finite_cyclic_subgroup_order)
+
+
 end
--- a/src/HOL/Algebra/Exact_Sequence.thy	Thu Apr 04 22:18:32 2019 +0200
+++ b/src/HOL/Algebra/Exact_Sequence.thy	Thu Apr 04 22:21:09 2019 +0200
@@ -1,12 +1,13 @@
 (*  Title:      HOL/Algebra/Exact_Sequence.thy
-    Author:     Martin Baillon
+    Author:     Martin Baillon (first part) and LC Paulson (material ported from HOL Light)
 *)
 
+section \<open>Exact Sequences\<close>
+
 theory Exact_Sequence
-  imports Group Coset Solvable_Groups
+  imports Elementary_Groups Solvable_Groups
 begin
 
-section \<open>Exact Sequences\<close>
 
 
 subsection \<open>Definitions\<close>
@@ -16,6 +17,9 @@
 extension: "\<lbrakk> exact_seq ((G # K # l), (g # q)); group H ; h \<in> hom G H ;
               kernel G H h = image g (carrier K) \<rbrakk> \<Longrightarrow> exact_seq (H # G # K # l, h # g # q)"
 
+inductive_simps exact_seq_end_iff [simp]: "exact_seq ([G,H], (g # q))"
+inductive_simps exact_seq_cons_iff [simp]: "exact_seq ((G # K # H # l), (g # h # q))"
+
 abbreviation exact_seq_arrow ::
   "('a \<Rightarrow> 'a) \<Rightarrow> 'a monoid list \<times> ('a \<Rightarrow> 'a) list \<Rightarrow>  'a monoid \<Rightarrow> 'a monoid list \<times> ('a \<Rightarrow> 'a) list"
   ("(3_ / \<longlongrightarrow>\<index> _)" [1000, 60])
@@ -173,4 +177,295 @@
   shows "(solvable G1) \<and> (solvable G3) \<longleftrightarrow>  solvable G2"
   using exact_seq_solvable_recip exact_seq_solvable_imp assms by blast
 
+
+lemma exact_seq_eq_triviality:
+  assumes "exact_seq ([E,D,C,B,A], [k,h,g,f])"
+  shows "trivial_group C \<longleftrightarrow> f ` carrier A = carrier B \<and> inj_on k (carrier D)" (is "_ = ?rhs")
+proof
+  assume C: "trivial_group C"
+  with assms have "inj_on k (carrier D)"
+    apply (auto simp: group_hom.image_from_trivial_group trivial_group_def hom_one)
+    apply (simp add: group_hom_def group_hom_axioms_def group_hom.inj_iff_trivial_ker)
+    done
+  with assms C show ?rhs
+    apply (auto simp: group_hom.image_from_trivial_group trivial_group_def hom_one)
+     apply (auto simp: group_hom_def group_hom_axioms_def hom_def kernel_def)
+    done
+next
+  assume ?rhs
+  with assms show "trivial_group C"
+    apply (simp add: trivial_group_def)
+    by (metis group_hom.inj_iff_trivial_ker group_hom.trivial_hom_iff group_hom_axioms.intro group_hom_def)
+qed
+
+lemma exact_seq_imp_triviality:
+   "\<lbrakk>exact_seq ([E,D,C,B,A], [k,h,g,f]); f \<in> iso A B; k \<in> iso D E\<rbrakk> \<Longrightarrow> trivial_group C"
+  by (metis (no_types, lifting) Group.iso_def bij_betw_def exact_seq_eq_triviality mem_Collect_eq)
+
+lemma exact_seq_epi_eq_triviality:
+   "exact_seq ([D,C,B,A], [h,g,f]) \<Longrightarrow> (f ` carrier A = carrier B) \<longleftrightarrow> trivial_homomorphism B C g"
+  by (auto simp: trivial_homomorphism_def kernel_def)
+
+lemma exact_seq_mon_eq_triviality:
+   "exact_seq ([D,C,B,A], [h,g,f]) \<Longrightarrow> inj_on h (carrier C) \<longleftrightarrow> trivial_homomorphism B C g"
+  by (auto simp: trivial_homomorphism_def kernel_def group.is_monoid inj_on_one_iff' image_def) blast
+
+lemma exact_sequence_sum_lemma:
+  assumes "comm_group G" and h: "h \<in> iso A C" and k: "k \<in> iso B D"
+    and ex: "exact_seq ([D,G,A], [g,i])" "exact_seq ([C,G,B], [f,j])"
+    and fih: "\<And>x. x \<in> carrier A \<Longrightarrow> f(i x) = h x"
+    and gjk: "\<And>x. x \<in> carrier B \<Longrightarrow> g(j x) = k x"
+  shows "(\<lambda>(x, y). i x \<otimes>\<^bsub>G\<^esub> j y) \<in> Group.iso (A \<times>\<times> B) G \<and> (\<lambda>z. (f z, g z)) \<in> Group.iso G (C \<times>\<times> D)"
+    (is "?ij \<in> _ \<and> ?gf \<in> _")
+proof (rule epi_iso_compose_rev)
+  interpret comm_group G
+    by (rule assms)
+  interpret f: group_hom G C f
+    using ex by (simp add: group_hom_def group_hom_axioms_def)
+  interpret g: group_hom G D g
+    using ex by (simp add: group_hom_def group_hom_axioms_def)
+  interpret i: group_hom A G i
+    using ex by (simp add: group_hom_def group_hom_axioms_def)
+  interpret j: group_hom B G j
+    using ex by (simp add: group_hom_def group_hom_axioms_def)
+  have kerf: "kernel G C f = j ` carrier B" and "group A" "group B" "i \<in> hom A G"
+    using ex by (auto simp: group_hom_def group_hom_axioms_def)
+  then obtain h' where "h' \<in> hom C A" "(\<forall>x \<in> carrier A. h'(h x) = x)"
+    and hh': "(\<forall>y \<in> carrier C. h(h' y) = y)" and "group_isomorphisms A C h h'"
+    using h by (auto simp: group.iso_iff_group_isomorphisms group_isomorphisms_def)
+  have homij: "?ij \<in> hom (A \<times>\<times> B) G"
+    unfolding case_prod_unfold
+    apply (rule hom_group_mult)
+    using ex by (simp_all add: group_hom_def hom_of_fst [unfolded o_def] hom_of_snd [unfolded o_def])
+  show homgf: "?gf \<in> hom G (C \<times>\<times> D)"
+    using ex by (simp add: hom_paired)
+  show "?ij \<in> epi (A \<times>\<times> B) G"
+  proof (clarsimp simp add: epi_iff_subset homij)
+    fix x
+    assume x: "x \<in> carrier G"
+    with \<open>i \<in> hom A G\<close> \<open>h' \<in> hom C A\<close> have "x \<otimes>\<^bsub>G\<^esub> inv\<^bsub>G\<^esub>(i(h'(f x))) \<in> kernel G C f"
+      by (simp add: kernel_def hom_in_carrier hh' fih)
+    with kerf obtain y where y: "y \<in> carrier B" "j y = x \<otimes>\<^bsub>G\<^esub> inv\<^bsub>G\<^esub>(i(h'(f x)))"
+      by auto
+    have "i (h' (f x)) \<otimes>\<^bsub>G\<^esub> (x \<otimes>\<^bsub>G\<^esub> inv\<^bsub>G\<^esub> i (h' (f x))) = x \<otimes>\<^bsub>G\<^esub> (i (h' (f x)) \<otimes>\<^bsub>G\<^esub> inv\<^bsub>G\<^esub> i (h' (f x)))"
+      by (meson \<open>h' \<in> hom C A\<close> x f.hom_closed hom_in_carrier i.hom_closed inv_closed m_lcomm)
+    also have "\<dots> = x"
+      using \<open>h' \<in> hom C A\<close> hom_in_carrier x by fastforce
+    finally show "x \<in> (\<lambda>(x, y). i x \<otimes>\<^bsub>G\<^esub> j y) ` (carrier A \<times> carrier B)"
+      using x y apply (clarsimp simp: image_def)
+      apply (rule_tac x="h'(f x)" in bexI)
+       apply (rule_tac x=y in bexI, auto)
+      by (meson \<open>h' \<in> hom C A\<close> f.hom_closed hom_in_carrier)
+  qed
+  show "(\<lambda>z. (f z, g z)) \<circ> (\<lambda>(x, y). i x \<otimes>\<^bsub>G\<^esub> j y) \<in> Group.iso (A \<times>\<times> B) (C \<times>\<times> D)"
+    apply (rule group.iso_eq [where f = "\<lambda>(x,y). (h x,k y)"])
+    using ex
+    apply (auto simp: group_hom_def group_hom_axioms_def DirProd_group iso_paired2 h k fih gjk kernel_def set_eq_iff)
+     apply (metis f.hom_closed f.r_one fih imageI)
+    apply (metis g.hom_closed g.l_one gjk imageI)
+    done
+qed
+
+subsection \<open>Splitting lemmas and Short exact sequences\<close>
+text\<open>Ported from HOL Light by LCP\<close>
+
+definition short_exact_sequence
+  where "short_exact_sequence A B C f g \<equiv> \<exists>T1 T2 e1 e2. exact_seq ([T1,A,B,C,T2], [e1,f,g,e2]) \<and> trivial_group T1 \<and> trivial_group T2"
+
+lemma short_exact_sequenceD:
+  assumes "short_exact_sequence A B C f g" shows "exact_seq ([A,B,C], [f,g]) \<and> f \<in> epi B A \<and> g \<in> mon C B"
+  using assms
+  apply (auto simp: short_exact_sequence_def group_hom_def group_hom_axioms_def)
+  apply (simp add: epi_iff_subset group_hom.intro group_hom.kernel_to_trivial_group group_hom_axioms.intro)
+  by (metis (no_types, lifting) group_hom.inj_iff_trivial_ker group_hom.intro group_hom_axioms.intro
+      hom_one image_empty image_insert mem_Collect_eq mon_def trivial_group_def)
+
+lemma short_exact_sequence_iff:
+  "short_exact_sequence A B C f g \<longleftrightarrow> exact_seq ([A,B,C], [f,g]) \<and> f \<in> epi B A \<and> g \<in> mon C B"
+proof -
+  have "short_exact_sequence A B C f g"
+    if "exact_seq ([A, B, C], [f, g])" and "f \<in> epi B A" and "g \<in> mon C B"
+  proof -
+    show ?thesis
+      unfolding short_exact_sequence_def
+    proof (intro exI conjI)
+      have "kernel A (singleton_group \<one>\<^bsub>A\<^esub>) (\<lambda>x. \<one>\<^bsub>A\<^esub>) = f ` carrier B"
+        using that by (simp add: kernel_def singleton_group_def epi_def)
+      moreover have "kernel C B g = {\<one>\<^bsub>C\<^esub>}"
+        using that group_hom.inj_iff_trivial_ker mon_def by fastforce
+      ultimately show "exact_seq ([singleton_group (one A), A, B, C, singleton_group (one C)], [\<lambda>x. \<one>\<^bsub>A\<^esub>, f, g, id])"
+        using that
+        by (simp add: group_hom_def group_hom_axioms_def group.id_hom_singleton)
+    qed auto
+qed
+  then show ?thesis
+    using short_exact_sequenceD by blast
+qed
+
+lemma very_short_exact_sequence:
+  assumes "exact_seq ([D,C,B,A], [h,g,f])" "trivial_group A" "trivial_group D"
+  shows "g \<in> iso B C"
+  using assms
+  apply simp
+  by (metis (no_types, lifting) group_hom.image_from_trivial_group group_hom.iso_iff
+      group_hom.kernel_to_trivial_group group_hom.trivial_ker_imp_inj group_hom_axioms.intro group_hom_def hom_carrier inj_on_one_iff')
+
+lemma splitting_sublemma_gen:
+  assumes ex: "exact_seq ([C,B,A], [g,f])" and fim: "f ` carrier A = H"
+      and "subgroup K B" and 1: "H \<inter> K \<subseteq> {one B}" and eq: "set_mult B H K = carrier B"
+  shows "g \<in> iso (subgroup_generated B K) (subgroup_generated C(g ` carrier B))"
+proof -
+  interpret KB: subgroup K B
+    by (rule assms)
+  interpret fAB: group_hom A B f
+    using ex by simp
+  interpret gBC: group_hom B C g
+    using ex by (simp add: group_hom_def group_hom_axioms_def)
+  have "group A" "group B" "group C" and kerg: "kernel B C g = f ` carrier A"
+      using ex by (auto simp: group_hom_def group_hom_axioms_def)
+  have ker_eq: "kernel B C g = H"
+    using ex by (simp add: fim)
+  then have "subgroup H B"
+    using ex by (simp add: group_hom.img_is_subgroup)
+  show ?thesis
+    unfolding iso_iff
+  proof (intro conjI)
+    show "g \<in> hom (subgroup_generated B K) (subgroup_generated C(g ` carrier B))"
+      by (metis ker_eq \<open>subgroup K B\<close> eq gBC.hom_between_subgroups gBC.set_mult_ker_hom(2) order_refl subgroup.subset)
+    show "g ` carrier (subgroup_generated B K) = carrier (subgroup_generated C(g ` carrier B))"
+      by (metis assms(3) eq fAB.H.subgroupE(1) gBC.img_is_subgroup gBC.set_mult_ker_hom(2) ker_eq subgroup.carrier_subgroup_generated_subgroup)
+    interpret gKBC: group_hom "subgroup_generated B K" C g
+      apply (auto simp: group_hom_def group_hom_axioms_def \<open>group C\<close>)
+      by (simp add: fAB.H.hom_from_subgroup_generated gBC.homh)
+    have *: "x = \<one>\<^bsub>B\<^esub>"
+      if x: "x \<in> carrier (subgroup_generated B K)" and "g x = \<one>\<^bsub>C\<^esub>" for x
+    proof -
+      have x': "x \<in> carrier B"
+        using that fAB.H.carrier_subgroup_generated_subset by blast
+      moreover have "x \<in> H"
+        using kerg fim x' that by (auto simp: kernel_def set_eq_iff)
+      ultimately show ?thesis
+        by (metis "1" x Int_iff singletonD KB.carrier_subgroup_generated_subgroup subsetCE)
+    qed
+    show "inj_on g (carrier (subgroup_generated B K))"
+      using "*" gKBC.inj_on_one_iff by auto
+  qed
+qed
+
+lemma splitting_sublemma:
+  assumes ex: "short_exact_sequence C B A g f" and fim: "f ` carrier A = H"
+      and "subgroup K B" and 1: "H \<inter> K \<subseteq> {one B}" and eq: "set_mult B H K = carrier B"
+    shows "f \<in> iso A (subgroup_generated B H)" (is ?f)
+          "g \<in> iso (subgroup_generated B K) C" (is ?g)
+proof -
+  show ?f
+    using short_exact_sequenceD [OF ex]
+    apply (clarsimp simp add: group_hom_def group.iso_onto_image)
+    using fim group.iso_onto_image by blast
+  have "C = subgroup_generated C(g ` carrier B)"
+    using short_exact_sequenceD [OF ex]
+    apply simp
+    by (metis epi_iff_subset group.subgroup_generated_group_carrier hom_carrier subset_antisym)
+  then show ?g
+    using short_exact_sequenceD [OF ex]
+    by (metis "1" \<open>subgroup K B\<close> eq fim splitting_sublemma_gen)
+qed
+
+lemma splitting_lemma_left_gen:
+  assumes ex: "exact_seq ([C,B,A], [g,f])" and f': "f' \<in> hom B A" and iso: "(f' \<circ> f) \<in> iso A A"
+    and injf: "inj_on f (carrier A)" and surj: "g ` carrier B = carrier C"
+ obtains H K where "H \<lhd> B" "K \<lhd> B" "H \<inter> K \<subseteq> {one B}" "set_mult B H K = carrier B"
+                   "f \<in> iso A (subgroup_generated B H)" "g \<in> iso (subgroup_generated B K) C"
+proof -
+  interpret gBC: group_hom B C g
+    using ex by (simp add: group_hom_def group_hom_axioms_def)
+  have "group A" "group B" "group C" and kerg: "kernel B C g = f ` carrier A"
+    using ex by (auto simp: group_hom_def group_hom_axioms_def)
+  then have *: "f ` carrier A \<inter> kernel B A f' = {\<one>\<^bsub>B\<^esub>} \<and> f ` carrier A <#>\<^bsub>B\<^esub> kernel B A f' = carrier B"
+    using group_semidirect_sum_image_ker [of f A B f' A] assms by auto
+  interpret f'AB: group_hom B A f'
+    using assms by (auto simp: group_hom_def group_hom_axioms_def)
+  let ?H = "f ` carrier A"
+  let ?K = "kernel B A f'"
+  show thesis
+  proof
+    show "?H \<lhd> B"
+      by (simp add: gBC.normal_kernel flip: kerg)
+    show "?K \<lhd> B"
+      by (rule f'AB.normal_kernel)
+    show "?H \<inter> ?K \<subseteq> {\<one>\<^bsub>B\<^esub>}" "?H <#>\<^bsub>B\<^esub> ?K = carrier B"
+      using * by auto
+    show "f \<in> Group.iso A (subgroup_generated B ?H)"
+      using ex by (simp add: injf iso_onto_image group_hom_def group_hom_axioms_def)
+    have C: "C = subgroup_generated C(g ` carrier B)"
+      using surj by (simp add: gBC.subgroup_generated_group_carrier)
+    show "g \<in> Group.iso (subgroup_generated B ?K) C"
+      apply (subst C)
+      apply (rule splitting_sublemma_gen [OF ex refl])
+      using * by (auto simp: f'AB.subgroup_kernel)
+  qed
+qed
+
+lemma splitting_lemma_left:
+  assumes ex: "exact_seq ([C,B,A], [g,f])" and f': "f' \<in> hom B A"
+    and inv: "(\<And>x. x \<in> carrier A \<Longrightarrow> f'(f x) = x)"
+    and injf: "inj_on f (carrier A)" and surj: "g ` carrier B = carrier C"
+ obtains H K where "H \<lhd> B" "K \<lhd> B" "H \<inter> K \<subseteq> {one B}" "set_mult B H K = carrier B"
+                   "f \<in> iso A (subgroup_generated B H)" "g \<in> iso (subgroup_generated B K) C"
+proof -
+  interpret fAB: group_hom A B f
+    using ex by simp
+  interpret gBC: group_hom B C g
+    using ex by (simp add: group_hom_def group_hom_axioms_def)
+  have "group A" "group B" "group C" and kerg: "kernel B C g = f ` carrier A"
+      using ex by (auto simp: group_hom_def group_hom_axioms_def)
+  have iso: "f' \<circ> f \<in> Group.iso A A"
+    using ex by (auto simp: inv intro:  group.iso_eq [OF \<open>group A\<close> id_iso])
+  show thesis
+    by (metis that splitting_lemma_left_gen [OF ex f' iso injf surj])
+qed
+
+lemma splitting_lemma_right_gen:
+  assumes ex: "short_exact_sequence C B A g f" and g': "g' \<in> hom C B" and iso: "(g \<circ> g') \<in> iso C C"
+ obtains H K where "H \<lhd> B" "subgroup K B" "H \<inter> K \<subseteq> {one B}" "set_mult B H K = carrier B"
+                   "f \<in> iso A (subgroup_generated B H)" "g \<in> iso (subgroup_generated B K) C"
+proof
+  interpret fAB: group_hom A B f
+    using short_exact_sequenceD [OF ex] by (simp add: group_hom_def group_hom_axioms_def)
+  interpret gBC: group_hom B C g
+    using short_exact_sequenceD [OF ex] by (simp add: group_hom_def group_hom_axioms_def)
+  have *: "f ` carrier A \<inter> g' ` carrier C = {\<one>\<^bsub>B\<^esub>}"
+          "f ` carrier A <#>\<^bsub>B\<^esub> g' ` carrier C = carrier B"
+          "group A" "group B" "group C"
+          "kernel B C g = f ` carrier A"
+    using group_semidirect_sum_ker_image [of g g' C C B] short_exact_sequenceD [OF ex]
+    by (simp_all add: g' iso group_hom_def)
+  show "kernel B C g \<lhd> B"
+    by (simp add: gBC.normal_kernel)
+  show "(kernel B C g) \<inter> (g' ` carrier C) \<subseteq> {\<one>\<^bsub>B\<^esub>}" "(kernel B C g) <#>\<^bsub>B\<^esub> (g' ` carrier C) = carrier B"
+    by (auto simp: *)
+  show "f \<in> Group.iso A (subgroup_generated B (kernel B C g))"
+    by (metis "*"(6) fAB.group_hom_axioms group.iso_onto_image group_hom_def short_exact_sequenceD [OF ex])
+  show "subgroup (g' ` carrier C) B"
+    using splitting_sublemma
+    by (simp add: fAB.H.is_group g' gBC.is_group group_hom.img_is_subgroup group_hom_axioms_def group_hom_def)
+  then show "g \<in> Group.iso (subgroup_generated B (g' ` carrier C)) C"
+    by (metis (no_types, lifting) iso_iff fAB.H.hom_from_subgroup_generated gBC.homh image_comp inj_on_imageI iso subgroup.carrier_subgroup_generated_subgroup)
+qed
+
+lemma splitting_lemma_right:
+  assumes ex: "short_exact_sequence C B A g f" and g': "g' \<in> hom C B" and gg': "\<And>z. z \<in> carrier C \<Longrightarrow> g(g' z) = z"
+ obtains H K where "H \<lhd> B" "subgroup K B" "H \<inter> K \<subseteq> {one B}" "set_mult B H K = carrier B"
+                   "f \<in> iso A (subgroup_generated B H)" "g \<in> iso (subgroup_generated B K) C"
+proof -
+  have *: "group A" "group B" "group C"
+    using group_semidirect_sum_ker_image [of g g' C C B] short_exact_sequenceD [OF ex]
+    by (simp_all add: g'  group_hom_def)
+  show thesis
+    apply (rule splitting_lemma_right_gen [OF ex g' group.iso_eq [OF _ id_iso]])
+    using * apply (auto simp: gg' intro: that)
+    done
+qed
+
+
 end
--- a/src/HOL/Algebra/FiniteProduct.thy	Thu Apr 04 22:18:32 2019 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy	Thu Apr 04 22:21:09 2019 +0200
@@ -547,6 +547,61 @@
     finprod_cong [of "A - {i}" "A - {i}" "(\<lambda>j. if i = j then f j else \<one>)" "(\<lambda>i. \<one>)"]
   unfolding Pi_def simp_implies_def by (force simp add: insert_absorb)
 
+lemma finprod_singleton_swap:
+  assumes i_in_A: "i \<in> A" and fin_A: "finite A" and f_Pi: "f \<in> A \<rightarrow> carrier G"
+  shows "(\<Otimes>j\<in>A. if j = i then f j else \<one>) = f i"
+  using finprod_singleton [OF assms] by (simp add: eq_commute)
+
+lemma finprod_mono_neutral_cong_left:
+  assumes "finite B"
+    and "A \<subseteq> B"
+    and 1: "\<And>i. i \<in> B - A \<Longrightarrow> h i = \<one>"
+    and gh: "\<And>x. x \<in> A \<Longrightarrow> g x = h x"
+    and h: "h \<in> B \<rightarrow> carrier G"
+  shows "finprod G g A = finprod G h B"
+proof-
+  have eq: "A \<union> (B - A) = B" using \<open>A \<subseteq> B\<close> by blast
+  have d: "A \<inter> (B - A) = {}" using \<open>A \<subseteq> B\<close> by blast
+  from \<open>finite B\<close> \<open>A \<subseteq> B\<close> have f: "finite A" "finite (B - A)"
+    by (auto intro: finite_subset)
+  have "h \<in> A \<rightarrow> carrier G" "h \<in> B - A \<rightarrow> carrier G"
+    using assms by (auto simp: image_subset_iff_funcset)
+  moreover have "finprod G g A = finprod G h A \<otimes> finprod G h (B - A)"
+  proof -
+    have "finprod G h (B - A) = \<one>"
+      using "1" finprod_one_eqI by blast
+    moreover have "finprod G g A = finprod G h A"
+      using \<open>h \<in> A \<rightarrow> carrier G\<close> finprod_cong' gh by blast
+    ultimately show ?thesis
+      by (simp add: \<open>h \<in> A \<rightarrow> carrier G\<close>)
+  qed
+  ultimately show ?thesis
+    by (simp add: finprod_Un_disjoint [OF f d, unfolded eq])
+qed
+
+lemma finprod_mono_neutral_cong_right:
+  assumes "finite B"
+    and "A \<subseteq> B" "\<And>i. i \<in> B - A \<Longrightarrow> g i = \<one>" "\<And>x. x \<in> A \<Longrightarrow> g x = h x" "g \<in> B \<rightarrow> carrier G"
+  shows "finprod G g B = finprod G h A"
+  using assms  by (auto intro!: finprod_mono_neutral_cong_left [symmetric])
+
+lemma finprod_mono_neutral_cong:
+  assumes [simp]: "finite B" "finite A"
+    and *: "\<And>i. i \<in> B - A \<Longrightarrow> h i = \<one>" "\<And>i. i \<in> A - B \<Longrightarrow> g i = \<one>"
+    and gh: "\<And>x. x \<in> A \<inter> B \<Longrightarrow> g x = h x"
+    and g: "g \<in> A \<rightarrow> carrier G"
+    and h: "h \<in> B \<rightarrow> carrier G"
+ shows "finprod G g A = finprod G h B"
+proof-
+  have "finprod G g A = finprod G g (A \<inter> B)"
+    by (rule finprod_mono_neutral_cong_right) (use assms in auto)
+  also have "\<dots> = finprod G h (A \<inter> B)"
+    by (rule finprod_cong) (use assms in auto)
+  also have "\<dots> = finprod G h B"
+    by (rule finprod_mono_neutral_cong_left) (use assms in auto)
+  finally show ?thesis .
+qed
+
 end
 
 (* Jeremy Avigad. This should be generalized to arbitrary groups, not just commutative
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/Free_Abelian_Groups.thy	Thu Apr 04 22:21:09 2019 +0200
@@ -0,0 +1,758 @@
+section\<open>Free Abelian Groups\<close>
+
+theory Free_Abelian_Groups
+  imports
+    Product_Groups "HOL-Cardinals.Cardinal_Arithmetic"
+   "HOL-Library.Countable_Set" "HOL-Library.Poly_Mapping" "HOL-Library.Equipollence"
+
+begin
+
+(*Move? But where?*)
+lemma eqpoll_Fpow:
+  assumes "infinite A" shows "Fpow A \<approx> A"
+  unfolding eqpoll_iff_card_of_ordIso
+  by (metis assms card_of_Fpow_infinite)
+
+lemma infinite_iff_card_of_countable: "\<lbrakk>countable B; infinite B\<rbrakk> \<Longrightarrow> infinite A \<longleftrightarrow> ( |B| \<le>o |A| )"
+  unfolding infinite_iff_countable_subset card_of_ordLeq countable_def
+  by (force intro: card_of_ordLeqI ordLeq_transitive)
+
+lemma iso_imp_eqpoll_carrier: "G \<cong> H \<Longrightarrow> carrier G \<approx> carrier H"
+  by (auto simp: is_iso_def iso_def eqpoll_def)
+
+subsection\<open>Generalised finite product\<close>
+
+definition
+  gfinprod :: "[('b, 'm) monoid_scheme, 'a \<Rightarrow> 'b, 'a set] \<Rightarrow> 'b"
+  where "gfinprod G f A =
+   (if finite {x \<in> A. f x \<noteq> \<one>\<^bsub>G\<^esub>} then finprod G f {x \<in> A. f x \<noteq> \<one>\<^bsub>G\<^esub>} else \<one>\<^bsub>G\<^esub>)"
+
+context comm_monoid begin
+
+lemma gfinprod_closed [simp]:
+  "f \<in> A \<rightarrow> carrier G \<Longrightarrow> gfinprod G f A \<in> carrier G"
+  unfolding gfinprod_def
+  by (auto simp: image_subset_iff_funcset intro: finprod_closed)
+
+lemma gfinprod_cong:
+  "\<lbrakk>A = B; f \<in> B \<rightarrow> carrier G;
+    \<And>i. i \<in> B =simp=> f i = g i\<rbrakk> \<Longrightarrow> gfinprod G f A = gfinprod G g B"
+  unfolding gfinprod_def
+  by (auto simp: simp_implies_def cong: conj_cong intro: finprod_cong)
+
+lemma gfinprod_eq_finprod [simp]: "\<lbrakk>finite A; f \<in> A \<rightarrow> carrier G\<rbrakk> \<Longrightarrow> gfinprod G f A = finprod G f A"
+  by (auto simp: gfinprod_def intro: finprod_mono_neutral_cong_left)
+
+lemma gfinprod_insert [simp]:
+  assumes "finite {x \<in> A. f x \<noteq> \<one>\<^bsub>G\<^esub>}" "f \<in> A \<rightarrow> carrier G" "f i \<in> carrier G"
+  shows "gfinprod G f (insert i A) = (if i \<in> A then gfinprod G f A else f i \<otimes> gfinprod G f A)"
+proof -
+  have f: "f \<in> {x \<in> A. f x \<noteq> \<one>} \<rightarrow> carrier G"
+    using assms by (auto simp: image_subset_iff_funcset)
+  have "{x. x = i \<and> f x \<noteq> \<one> \<or> x \<in> A \<and> f x \<noteq> \<one>} = (if f i = \<one> then {x \<in> A. f x \<noteq> \<one>} else insert i {x \<in> A. f x \<noteq> \<one>})"
+    by auto
+  then show ?thesis
+    using assms
+    unfolding gfinprod_def by (simp add: conj_disj_distribR insert_absorb f split: if_split_asm)
+qed
+
+lemma gfinprod_distrib:
+  assumes fin: "finite {x \<in> A. f x \<noteq> \<one>\<^bsub>G\<^esub>}" "finite {x \<in> A. g x \<noteq> \<one>\<^bsub>G\<^esub>}"
+     and "f \<in> A \<rightarrow> carrier G" "g \<in> A \<rightarrow> carrier G"
+  shows "gfinprod G (\<lambda>i. f i \<otimes> g i) A = gfinprod G f A \<otimes> gfinprod G g A"
+proof -
+  have "finite {x \<in> A. f x \<otimes> g x \<noteq> \<one>}"
+    by (auto intro: finite_subset [OF _ finite_UnI [OF fin]])
+  then have "gfinprod G (\<lambda>i. f i \<otimes> g i) A = gfinprod G (\<lambda>i. f i \<otimes> g i) ({i \<in> A. f i \<noteq> \<one>\<^bsub>G\<^esub>} \<union> {i \<in> A. g i \<noteq> \<one>\<^bsub>G\<^esub>})"
+    unfolding gfinprod_def
+    using assms by (force intro: finprod_mono_neutral_cong)
+  also have "\<dots> = gfinprod G f A \<otimes> gfinprod G g A"
+  proof -
+    have "finprod G f ({i \<in> A. f i \<noteq> \<one>\<^bsub>G\<^esub>} \<union> {i \<in> A. g i \<noteq> \<one>\<^bsub>G\<^esub>}) = gfinprod G f A"
+      "finprod G g ({i \<in> A. f i \<noteq> \<one>\<^bsub>G\<^esub>} \<union> {i \<in> A. g i \<noteq> \<one>\<^bsub>G\<^esub>}) = gfinprod G g A"
+      using assms by (auto simp: gfinprod_def intro: finprod_mono_neutral_cong_right)
+    moreover have "(\<lambda>i. f i \<otimes> g i) \<in> {i \<in> A. f i \<noteq> \<one>} \<union> {i \<in> A. g i \<noteq> \<one>} \<rightarrow> carrier G"
+      using assms by (force simp: image_subset_iff_funcset)
+    ultimately show ?thesis
+      using assms
+      apply simp
+      apply (subst finprod_multf, auto)
+      done
+  qed
+  finally show ?thesis .
+qed
+
+lemma gfinprod_mono_neutral_cong_left:
+  assumes "A \<subseteq> B"
+    and 1: "\<And>i. i \<in> B - A \<Longrightarrow> h i = \<one>"
+    and gh: "\<And>x. x \<in> A \<Longrightarrow> g x = h x"
+    and h: "h \<in> B \<rightarrow> carrier G"
+  shows "gfinprod G g A = gfinprod G h B"
+proof (cases "finite {x \<in> B. h x \<noteq> \<one>}")
+  case True
+  then have "finite {x \<in> A. h x \<noteq> \<one>}"
+    apply (rule rev_finite_subset)
+    using \<open>A \<subseteq> B\<close> by auto
+  with True assms show ?thesis
+    apply (simp add: gfinprod_def cong: conj_cong)
+    apply (auto intro!: finprod_mono_neutral_cong_left)
+    done
+next
+  case False
+  have "{x \<in> B. h x \<noteq> \<one>} \<subseteq> {x \<in> A. h x \<noteq> \<one>}"
+    using 1 by auto
+  with False have "infinite {x \<in> A. h x \<noteq> \<one>}"
+    using infinite_super by blast
+  with False assms show ?thesis
+    by (simp add: gfinprod_def cong: conj_cong)
+qed
+
+lemma gfinprod_mono_neutral_cong_right:
+  assumes "A \<subseteq> B" "\<And>i. i \<in> B - A \<Longrightarrow> g i = \<one>" "\<And>x. x \<in> A \<Longrightarrow> g x = h x" "g \<in> B \<rightarrow> carrier G"
+  shows "gfinprod G g B = gfinprod G h A"
+  using assms  by (auto intro!: gfinprod_mono_neutral_cong_left [symmetric])
+
+lemma gfinprod_mono_neutral_cong:
+  assumes [simp]: "finite B" "finite A"
+    and *: "\<And>i. i \<in> B - A \<Longrightarrow> h i = \<one>" "\<And>i. i \<in> A - B \<Longrightarrow> g i = \<one>"
+    and gh: "\<And>x. x \<in> A \<inter> B \<Longrightarrow> g x = h x"
+    and g: "g \<in> A \<rightarrow> carrier G"
+    and h: "h \<in> B \<rightarrow> carrier G"
+ shows "gfinprod G g A = gfinprod G h B"
+proof-
+  have "gfinprod G g A = gfinprod G g (A \<inter> B)"
+    by (rule gfinprod_mono_neutral_cong_right) (use assms in auto)
+  also have "\<dots> = gfinprod G h (A \<inter> B)"
+    by (rule gfinprod_cong) (use assms in auto)
+  also have "\<dots> = gfinprod G h B"
+    by (rule gfinprod_mono_neutral_cong_left) (use assms in auto)
+  finally show ?thesis .
+qed
+
+end
+
+lemma (in comm_group) hom_group_sum:
+  assumes hom: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> hom (A i) G" and grp: "\<And>i. i \<in> I \<Longrightarrow> group (A i)"
+  shows "(\<lambda>x. gfinprod G (\<lambda>i. (f i) (x i)) I) \<in> hom (sum_group I A) G"
+  unfolding hom_def
+proof (intro CollectI conjI ballI)
+  show "(\<lambda>x. gfinprod G (\<lambda>i. f i (x i)) I) \<in> carrier (sum_group I A) \<rightarrow> carrier G"
+    using assms
+    by (force simp: hom_def carrier_sum_group intro: gfinprod_closed simp flip: image_subset_iff_funcset)
+next
+  fix x y
+  assume x: "x \<in> carrier (sum_group I A)" and y: "y \<in> carrier (sum_group I A)"
+  then have finx: "finite {i \<in> I. x i \<noteq> \<one>\<^bsub>A i\<^esub>}" and finy: "finite {i \<in> I. y i \<noteq> \<one>\<^bsub>A i\<^esub>}"
+    using assms by (auto simp: carrier_sum_group)
+  have finfx: "finite {i \<in> I. f i (x i) \<noteq> \<one>}"
+    using assms by (auto simp: is_group hom_one [OF hom] intro: finite_subset [OF _ finx])
+  have finfy: "finite {i \<in> I. f i (y i) \<noteq> \<one>}"
+    using assms by (auto simp: is_group hom_one [OF hom] intro: finite_subset [OF _ finy])
+  have carr: "f i (x i) \<in> carrier G"  "f i (y i) \<in> carrier G" if "i \<in> I" for i
+    using hom_carrier [OF hom] that x y assms
+    by (fastforce simp add: carrier_sum_group)+
+  have lam: "(\<lambda>i. f i ( x i \<otimes>\<^bsub>A i\<^esub> y i)) \<in> I \<rightarrow> carrier G"
+    using x y assms by (auto simp: hom_def carrier_sum_group PiE_def Pi_def)
+  have lam': "(\<lambda>i. f i (if i \<in> I then x i \<otimes>\<^bsub>A i\<^esub> y i else undefined)) \<in> I \<rightarrow> carrier G"
+    by (simp add: lam Pi_cong)
+  with lam x y assms
+  show "gfinprod G (\<lambda>i. f i ((x \<otimes>\<^bsub>sum_group I A\<^esub> y) i)) I
+      = gfinprod G (\<lambda>i. f i (x i)) I \<otimes> gfinprod G (\<lambda>i. f i (y i)) I"
+    by (simp add: carrier_sum_group PiE_def Pi_def hom_mult [OF hom]
+                  gfinprod_distrib finfx finfy carr cong: gfinprod_cong)
+qed
+
+subsection\<open>Free Abelian groups on a set, using the "frag" type constructor.          \<close>
+
+definition free_Abelian_group :: "'a set \<Rightarrow> ('a \<Rightarrow>\<^sub>0 int) monoid"
+  where "free_Abelian_group S = \<lparr>carrier = {c. Poly_Mapping.keys c \<subseteq> S}, monoid.mult = (+), one  = 0\<rparr>"
+
+lemma group_free_Abelian_group [simp]: "group (free_Abelian_group S)"
+proof -
+  have "\<And>x. Poly_Mapping.keys x \<subseteq> S \<Longrightarrow> x \<in> Units (free_Abelian_group S)"
+    unfolding free_Abelian_group_def Units_def
+    by clarsimp (metis eq_neg_iff_add_eq_0 neg_eq_iff_add_eq_0 keys_minus)
+  then show ?thesis
+    unfolding free_Abelian_group_def
+    by unfold_locales (auto simp: dest: subsetD [OF keys_add])
+qed
+
+lemma carrier_free_Abelian_group_iff [simp]:
+  shows "x \<in> carrier (free_Abelian_group S) \<longleftrightarrow> Poly_Mapping.keys x \<subseteq> S"
+  by (auto simp: free_Abelian_group_def)
+
+lemma one_free_Abelian_group [simp]: "\<one>\<^bsub>free_Abelian_group S\<^esub> = 0"
+  by (auto simp: free_Abelian_group_def)
+
+lemma mult_free_Abelian_group [simp]: "x \<otimes>\<^bsub>free_Abelian_group S\<^esub> y = x + y"
+  by (auto simp: free_Abelian_group_def)
+
+lemma inv_free_Abelian_group [simp]: "Poly_Mapping.keys x \<subseteq> S \<Longrightarrow> inv\<^bsub>free_Abelian_group S\<^esub> x = -x"
+  by (rule group.inv_equality [OF group_free_Abelian_group]) auto
+
+lemma abelian_free_Abelian_group: "comm_group(free_Abelian_group S)"
+  apply (rule group.group_comm_groupI [OF group_free_Abelian_group])
+  by (simp add: free_Abelian_group_def)
+
+lemma pow_free_Abelian_group [simp]:
+  fixes n::nat
+  shows "Group.pow (free_Abelian_group S) x n = frag_cmul (int n) x"
+  by (induction n) (auto simp: nat_pow_def free_Abelian_group_def frag_cmul_distrib)
+
+lemma int_pow_free_Abelian_group [simp]:
+  fixes n::int
+  assumes "Poly_Mapping.keys x \<subseteq> S"
+  shows "Group.pow (free_Abelian_group S) x n = frag_cmul n x"
+proof (induction n)
+  case (nonneg n)
+  then show ?case
+    by (simp add: int_pow_int)
+next
+  case (neg n)
+  have "x [^]\<^bsub>free_Abelian_group S\<^esub> - int (Suc n)
+     = inv\<^bsub>free_Abelian_group S\<^esub> (x [^]\<^bsub>free_Abelian_group S\<^esub> int (Suc n))"
+    by (rule group.int_pow_neg [OF group_free_Abelian_group]) (use assms in \<open>simp add: free_Abelian_group_def\<close>)
+  also have "\<dots> = frag_cmul (- int (Suc n)) x"
+    by (metis assms inv_free_Abelian_group pow_free_Abelian_group int_pow_int minus_frag_cmul
+              order_trans keys_cmul)
+  finally show ?case .
+qed
+
+lemma frag_of_in_free_Abelian_group [simp]:
+   "frag_of x \<in> carrier(free_Abelian_group S) \<longleftrightarrow> x \<in> S"
+  by simp
+
+lemma free_Abelian_group_induct:
+  assumes major: "Poly_Mapping.keys x \<subseteq> S"
+      and minor: "P(0)"
+           "\<And>x y. \<lbrakk>Poly_Mapping.keys x \<subseteq> S; Poly_Mapping.keys y \<subseteq> S; P x; P y\<rbrakk> \<Longrightarrow> P(x-y)"
+           "\<And>a. a \<in> S \<Longrightarrow> P(frag_of a)"
+         shows "P x"
+proof -
+  have "Poly_Mapping.keys x \<subseteq> S \<and> P x"
+    using major
+  proof (induction x rule: frag_induction)
+    case (diff a b)
+    then show ?case
+      by (meson Un_least minor(2) order.trans keys_diff)
+  qed (auto intro: minor)
+  then show ?thesis ..
+qed
+
+lemma sum_closed_free_Abelian_group:
+    "(\<And>i. i \<in> I \<Longrightarrow> x i \<in> carrier (free_Abelian_group S)) \<Longrightarrow> sum x I \<in> carrier (free_Abelian_group S)"
+  apply (induction I rule: infinite_finite_induct, auto)
+  by (metis (no_types, hide_lams) UnE subsetCE keys_add)
+
+
+lemma (in comm_group) free_Abelian_group_universal:
+  fixes f :: "'c \<Rightarrow> 'a"
+  assumes "f ` S \<subseteq> carrier G"
+  obtains h where "h \<in> hom (free_Abelian_group S) G" "\<And>x. x \<in> S \<Longrightarrow> h(frag_of x) = f x"
+proof
+  have fin: "Poly_Mapping.keys u \<subseteq> S \<Longrightarrow> finite {x \<in> S. f x [^] poly_mapping.lookup u x \<noteq> \<one>}" for u :: "'c \<Rightarrow>\<^sub>0 int"
+    apply (rule finite_subset [OF _ finite_keys [of u]])
+    unfolding keys.rep_eq by force
+  define h :: "('c \<Rightarrow>\<^sub>0 int) \<Rightarrow> 'a"
+    where "h \<equiv> \<lambda>x. gfinprod G (\<lambda>a. f a [^] poly_mapping.lookup x a) S"
+  show "h \<in> hom (free_Abelian_group S) G"
+  proof (rule homI)
+    fix x y
+    assume xy: "x \<in> carrier (free_Abelian_group S)" "y \<in> carrier (free_Abelian_group S)"
+    then show "h (x \<otimes>\<^bsub>free_Abelian_group S\<^esub> y) = h x \<otimes> h y"
+      using assms unfolding h_def free_Abelian_group_def
+      by (simp add: fin gfinprod_distrib image_subset_iff Poly_Mapping.lookup_add int_pow_mult cong: gfinprod_cong)
+  qed (use assms in \<open>force simp: free_Abelian_group_def h_def intro: gfinprod_closed\<close>)
+  show "h(frag_of x) = f x" if "x \<in> S" for x
+  proof -
+    have fin: "(\<lambda>a. f x [^] (1::int)) \<in> {x} \<rightarrow> carrier G" "f x [^] (1::int) \<in> carrier G"
+      using assms that by force+
+    show ?thesis
+      by (cases " f x [^] (1::int) = \<one>") (use assms that in \<open>auto simp: h_def gfinprod_def finprod_singleton\<close>)
+  qed
+qed
+
+lemma eqpoll_free_Abelian_group_infinite:
+  assumes "infinite A" shows "carrier(free_Abelian_group A) \<approx> A"
+proof (rule lepoll_antisym)
+  have "carrier (free_Abelian_group A) \<lesssim> {f::'a\<Rightarrow>int. f ` A \<subseteq> UNIV \<and> {x. f x \<noteq> 0} \<subseteq> A \<and> finite {x. f x \<noteq> 0}}"
+    unfolding lepoll_def
+    by (rule_tac x="Poly_Mapping.lookup" in exI) (auto simp: poly_mapping_eqI lookup_not_eq_zero_eq_in_keys inj_onI)
+  also have "\<dots> \<lesssim> Fpow (A \<times> (UNIV::int set))"
+    by (rule lepoll_restricted_funspace)
+  also have "\<dots> \<approx> A \<times> (UNIV::int set)"
+  proof (rule eqpoll_Fpow)
+    show "infinite (A \<times> (UNIV::int set))"
+      using assms finite_cartesian_productD1 by fastforce
+  qed
+  also have "\<dots> \<approx> A"
+    unfolding eqpoll_iff_card_of_ordIso
+  proof -
+    have "|A \<times> (UNIV::int set)| <=o |A|"
+      by (simp add: assms card_of_Times_ordLeq_infinite flip: infinite_iff_card_of_countable)
+    moreover have "|A| \<le>o |A \<times> (UNIV::int set)|"
+      by simp
+    ultimately have "|A| *c |(UNIV::int set)| =o |A|"
+      by (simp add: cprod_def ordIso_iff_ordLeq)
+    then show "|A \<times> (UNIV::int set)| =o |A|"
+      by (metis Times_cprod ordIso_transitive)
+  qed
+  finally show "carrier (free_Abelian_group A) \<lesssim> A" .
+  have "inj_on frag_of A"
+    by (simp add: frag_of_eq inj_on_def)
+  moreover have "frag_of ` A \<subseteq> carrier (free_Abelian_group A)"
+    by (simp add: image_subsetI)
+  ultimately show "A \<lesssim> carrier (free_Abelian_group A)"
+    by (force simp: lepoll_def)
+qed
+
+proposition (in comm_group) eqpoll_homomorphisms_from_free_Abelian_group:
+   "{f. f \<in> extensional (carrier(free_Abelian_group S)) \<and> f \<in> hom (free_Abelian_group S) G}
+    \<approx> (S \<rightarrow>\<^sub>E carrier G)"  (is "?lhs \<approx> ?rhs")
+  unfolding eqpoll_def bij_betw_def
+proof (intro exI conjI)
+  let ?f = "\<lambda>f. restrict (f \<circ> frag_of) S"
+  show "inj_on ?f ?lhs"
+  proof (clarsimp simp: inj_on_def)
+    fix g h
+    assume
+      g: "g \<in> extensional (carrier (free_Abelian_group S))" "g \<in> hom (free_Abelian_group S) G"
+      and h: "h \<in> extensional (carrier (free_Abelian_group S))" "h \<in> hom (free_Abelian_group S) G"
+      and eq: "restrict (g \<circ> frag_of) S = restrict (h \<circ> frag_of) S"
+    have 0: "0 \<in> carrier (free_Abelian_group S)"
+      by simp
+    interpret hom_g: group_hom "free_Abelian_group S" G g
+      using g by (auto simp: group_hom_def group_hom_axioms_def is_group)
+    interpret hom_h: group_hom "free_Abelian_group S" G h
+      using h by (auto simp: group_hom_def group_hom_axioms_def is_group)
+    have "Poly_Mapping.keys c \<subseteq> S \<Longrightarrow> Poly_Mapping.keys c \<subseteq> S \<and> g c = h c" for c
+    proof (induction c rule: frag_induction)
+      case zero
+      show ?case
+        using hom_g.hom_one hom_h.hom_one by auto
+    next
+      case (one x)
+      then show ?case
+        using eq by (simp add: fun_eq_iff) (metis comp_def)
+    next
+      case (diff a b)
+      then show ?case
+        using hom_g.hom_mult hom_h.hom_mult hom_g.hom_inv hom_h.hom_inv
+        apply (auto simp: dest: subsetD [OF keys_diff])
+        by (metis keys_minus uminus_add_conv_diff)
+    qed
+    then show "g = h"
+      by (meson g h carrier_free_Abelian_group_iff extensionalityI)
+  qed
+  have "f \<in> (\<lambda>f. restrict (f \<circ> frag_of) S) `
+            {f \<in> extensional (carrier (free_Abelian_group S)). f \<in> hom (free_Abelian_group S) G}"
+    if f: "f \<in> S \<rightarrow>\<^sub>E carrier G"
+    for f :: "'c \<Rightarrow> 'a"
+  proof -
+    obtain h where h: "h \<in> hom (free_Abelian_group S) G" "\<And>x. x \<in> S \<Longrightarrow> h(frag_of x) = f x"
+    proof (rule free_Abelian_group_universal)
+      show "f ` S \<subseteq> carrier G"
+        using f by blast
+    qed auto
+    let ?h = "restrict h (carrier (free_Abelian_group S))"
+    show ?thesis
+    proof
+      show "f = restrict (?h \<circ> frag_of) S"
+        using f by (force simp: h)
+      show "?h \<in> {f \<in> extensional (carrier (free_Abelian_group S)). f \<in> hom (free_Abelian_group S) G}"
+        using h by (auto simp: hom_def dest!: subsetD [OF keys_add])
+    qed
+  qed
+  then show "?f ` ?lhs = S \<rightarrow>\<^sub>E carrier G"
+    by (auto simp: hom_def Ball_def Pi_def)
+qed
+
+lemma hom_frag_minus:
+  assumes "h \<in> hom (free_Abelian_group S) (free_Abelian_group T)" "Poly_Mapping.keys a \<subseteq> S"
+  shows "h (-a) = - (h a)"
+proof -
+  have "Poly_Mapping.keys (h a) \<subseteq> T"
+    by (meson assms carrier_free_Abelian_group_iff hom_in_carrier)
+  then show ?thesis
+    by (metis (no_types) assms carrier_free_Abelian_group_iff group_free_Abelian_group group_hom.hom_inv group_hom_axioms_def group_hom_def inv_free_Abelian_group)
+qed
+
+lemma hom_frag_add:
+  assumes "h \<in> hom (free_Abelian_group S) (free_Abelian_group T)" "Poly_Mapping.keys a \<subseteq> S" "Poly_Mapping.keys b \<subseteq> S"
+  shows "h (a+b) = h a + h b"
+proof -
+  have "Poly_Mapping.keys (h a) \<subseteq> T"
+    by (meson assms carrier_free_Abelian_group_iff hom_in_carrier)
+  moreover
+  have "Poly_Mapping.keys (h b) \<subseteq> T"
+    by (meson assms carrier_free_Abelian_group_iff hom_in_carrier)
+  ultimately show ?thesis
+    using assms hom_mult by fastforce
+qed
+
+lemma hom_frag_diff:
+  assumes "h \<in> hom (free_Abelian_group S) (free_Abelian_group T)" "Poly_Mapping.keys a \<subseteq> S" "Poly_Mapping.keys b \<subseteq> S"
+  shows "h (a-b) = h a - h b"
+  by (metis (no_types, lifting) assms diff_conv_add_uminus hom_frag_add hom_frag_minus keys_minus)
+
+
+proposition isomorphic_free_Abelian_groups:
+   "free_Abelian_group S \<cong> free_Abelian_group T \<longleftrightarrow> S \<approx> T"  (is "(?FS \<cong> ?FT) = ?rhs")
+proof
+  interpret S: group "?FS"
+    by simp
+  interpret T: group "?FT"
+    by simp
+  interpret G2: comm_group "integer_mod_group 2"
+    by (rule abelian_integer_mod_group)
+  let ?Two = "{0..<2::int}"
+  have [simp]: "\<not> ?Two \<subseteq> {a}" for a
+    by (simp add: subset_iff) presburger
+  assume L: "?FS \<cong> ?FT"
+  let ?HS = "{h \<in> extensional (carrier ?FS). h \<in> hom ?FS (integer_mod_group 2)}"
+  let ?HT = "{h \<in> extensional (carrier ?FT). h \<in> hom ?FT (integer_mod_group 2)}"
+  have "S \<rightarrow>\<^sub>E ?Two \<approx> ?HS"
+    apply (rule eqpoll_sym)
+    using G2.eqpoll_homomorphisms_from_free_Abelian_group by (simp add: carrier_integer_mod_group)
+  also have "\<dots> \<approx> ?HT"
+  proof -
+    obtain f g where "group_isomorphisms ?FS ?FT f g"
+      using L S.iso_iff_group_isomorphisms by (force simp: is_iso_def)
+    then have f: "f \<in> hom ?FS ?FT"
+      and g: "g \<in> hom ?FT ?FS"
+      and gf: "\<forall>x \<in> carrier ?FS. g(f x) = x"
+      and fg: "\<forall>y \<in> carrier ?FT. f(g y) = y"
+      by (auto simp: group_isomorphisms_def)
+    let ?f = "\<lambda>h. restrict (h \<circ> g) (carrier ?FT)"
+    let ?g = "\<lambda>h. restrict (h \<circ> f) (carrier ?FS)"
+    show ?thesis
+    proof (rule lepoll_antisym)
+      show "?HS \<lesssim> ?HT"
+        unfolding lepoll_def
+      proof (intro exI conjI)
+        show "inj_on ?f ?HS"
+          apply (rule inj_on_inverseI [where g = ?g])
+          using hom_in_carrier [OF f]
+          by (auto simp: gf fun_eq_iff carrier_integer_mod_group Ball_def Pi_def extensional_def)
+        show "?f ` ?HS \<subseteq> ?HT"
+        proof clarsimp
+          fix h
+          assume h: "h \<in> hom ?FS (integer_mod_group 2)"
+          have "h \<circ> g \<in> hom ?FT (integer_mod_group 2)"
+            by (rule hom_compose [OF g h])
+          moreover have "restrict (h \<circ> g) (carrier ?FT) x = (h \<circ> g) x" if "x \<in> carrier ?FT" for x
+            using g that by (simp add: hom_def)
+          ultimately show "restrict (h \<circ> g) (carrier ?FT) \<in> hom ?FT (integer_mod_group 2)"
+            using T.hom_restrict by fastforce
+        qed
+      qed
+    next
+      show "?HT \<lesssim> ?HS"
+        unfolding lepoll_def
+      proof (intro exI conjI)
+        show "inj_on ?g ?HT"
+          apply (rule inj_on_inverseI [where g = ?f])
+          using hom_in_carrier [OF g]
+          by (auto simp: fg fun_eq_iff carrier_integer_mod_group Ball_def Pi_def extensional_def)
+        show "?g ` ?HT \<subseteq> ?HS"
+        proof clarsimp
+          fix k
+          assume k: "k \<in> hom ?FT (integer_mod_group 2)"
+          have "k \<circ> f \<in> hom ?FS (integer_mod_group 2)"
+            by (rule hom_compose [OF f k])
+          moreover have "restrict (k \<circ> f) (carrier ?FS) x = (k \<circ> f) x" if "x \<in> carrier ?FS" for x
+            using f that by (simp add: hom_def)
+          ultimately show "restrict (k \<circ> f) (carrier ?FS) \<in> hom ?FS (integer_mod_group 2)"
+            using S.hom_restrict by fastforce
+        qed
+      qed
+    qed
+  qed
+  also have "\<dots> \<approx> T \<rightarrow>\<^sub>E ?Two"
+    using G2.eqpoll_homomorphisms_from_free_Abelian_group by (simp add: carrier_integer_mod_group)
+  finally have *: "S \<rightarrow>\<^sub>E ?Two \<approx> T \<rightarrow>\<^sub>E ?Two" .
+  then have "finite (S \<rightarrow>\<^sub>E ?Two) \<longleftrightarrow> finite (T \<rightarrow>\<^sub>E ?Two)"
+    by (rule eqpoll_finite_iff)
+  then have "finite S \<longleftrightarrow> finite T"
+    by (auto simp: finite_funcset_iff)
+  then consider "finite S" "finite T" | "~ finite S" "~ finite T"
+    by blast
+  then show ?rhs
+  proof cases
+    case 1
+    with * have "2 ^ card S = (2::nat) ^ card T"
+      by (simp add: card_PiE finite_PiE eqpoll_iff_card)
+    then have "card S = card T"
+      by auto
+    then show ?thesis
+      using eqpoll_iff_card 1 by blast
+  next
+    case 2
+    have "carrier (free_Abelian_group S) \<approx> carrier (free_Abelian_group T)"
+      using L by (simp add: iso_imp_eqpoll_carrier)
+    then show ?thesis
+      using 2 eqpoll_free_Abelian_group_infinite eqpoll_sym eqpoll_trans by metis
+  qed
+next
+  assume ?rhs
+  then obtain f g where f: "\<And>x. x \<in> S \<Longrightarrow> f x \<in> T \<and> g(f x) = x"
+                    and g: "\<And>y. y \<in> T \<Longrightarrow> g y \<in> S \<and> f(g y) = y"
+    using eqpoll_iff_bijections by metis
+  interpret S: comm_group "?FS"
+    by (simp add: abelian_free_Abelian_group)
+  interpret T: comm_group "?FT"
+    by (simp add: abelian_free_Abelian_group)
+  have "(frag_of \<circ> f) ` S \<subseteq> carrier (free_Abelian_group T)"
+    using f by auto
+  then obtain h where h: "h \<in> hom (free_Abelian_group S) (free_Abelian_group T)"
+    and h_frag: "\<And>x. x \<in> S \<Longrightarrow> h (frag_of x) = (frag_of \<circ> f) x"
+    using T.free_Abelian_group_universal [of "frag_of \<circ> f" S] by blast
+  interpret hhom: group_hom "free_Abelian_group S" "free_Abelian_group T" h
+    by (simp add: h group_hom_axioms_def group_hom_def)
+  have "(frag_of \<circ> g) ` T \<subseteq> carrier (free_Abelian_group S)"
+    using g by auto
+  then obtain k where k: "k \<in> hom (free_Abelian_group T) (free_Abelian_group S)"
+    and k_frag: "\<And>x. x \<in> T \<Longrightarrow> k (frag_of x) = (frag_of \<circ> g) x"
+    using S.free_Abelian_group_universal [of "frag_of \<circ> g" T] by blast
+  interpret khom: group_hom "free_Abelian_group T" "free_Abelian_group S" k
+    by (simp add: k group_hom_axioms_def group_hom_def)
+  have kh: "Poly_Mapping.keys x \<subseteq> S \<Longrightarrow> Poly_Mapping.keys x \<subseteq> S \<and> k (h x) = x" for x
+  proof (induction rule: frag_induction)
+    case zero
+    then show ?case
+      apply auto
+      by (metis group_free_Abelian_group h hom_one k one_free_Abelian_group)
+  next
+    case (one x)
+    then show ?case
+      by (auto simp: h_frag k_frag f)
+  next
+    case (diff a b)
+    with keys_diff have "Poly_Mapping.keys (a - b) \<subseteq> S"
+      by (metis Un_least order_trans)
+    with diff hhom.hom_closed show ?case
+      by (simp add: hom_frag_diff [OF h] hom_frag_diff [OF k])
+  qed
+  have hk: "Poly_Mapping.keys y \<subseteq> T \<Longrightarrow> Poly_Mapping.keys y \<subseteq> T \<and> h (k y) = y" for y
+  proof (induction rule: frag_induction)
+    case zero
+    then show ?case
+      apply auto
+      by (metis group_free_Abelian_group h hom_one k one_free_Abelian_group)
+  next
+    case (one y)
+    then show ?case
+      by (auto simp: h_frag k_frag g)
+  next
+    case (diff a b)
+    with keys_diff have "Poly_Mapping.keys (a - b) \<subseteq> T"
+      by (metis Un_least order_trans)
+    with diff khom.hom_closed show ?case
+      by (simp add: hom_frag_diff [OF h] hom_frag_diff [OF k])
+  qed
+  have "h \<in> iso ?FS ?FT"
+    unfolding iso_def bij_betw_iff_bijections mem_Collect_eq
+  proof (intro conjI exI ballI h)
+    fix x
+    assume x: "x \<in> carrier (free_Abelian_group S)"
+    show "h x \<in> carrier (free_Abelian_group T)"
+      by (meson x h hom_in_carrier)
+    show "k (h x) = x"
+      using x by (simp add: kh)
+  next
+    fix y
+    assume y: "y \<in> carrier (free_Abelian_group T)"
+    show "k y \<in> carrier (free_Abelian_group S)"
+      by (meson y k hom_in_carrier)
+    show "h (k y) = y"
+      using y by (simp add: hk)
+  qed
+  then show "?FS \<cong> ?FT"
+    by (auto simp: is_iso_def)
+qed
+
+lemma isomorphic_group_integer_free_Abelian_group_singleton:
+  "integer_group \<cong> free_Abelian_group {x}"
+proof -
+  have "(\<lambda>n. frag_cmul n (frag_of x)) \<in> iso integer_group (free_Abelian_group {x})"
+  proof (rule isoI [OF homI])
+    show "bij_betw (\<lambda>n. frag_cmul n (frag_of x)) (carrier integer_group) (carrier (free_Abelian_group {x}))"
+      apply (rule bij_betwI [where g = "\<lambda>y. Poly_Mapping.lookup y x"])
+      by (auto simp: integer_group_def in_keys_iff intro!: poly_mapping_eqI)
+  qed (auto simp: frag_cmul_distrib)
+  then show ?thesis
+    unfolding is_iso_def
+    by blast
+qed
+
+lemma group_hom_free_Abelian_groups_id:
+  "id \<in> hom (free_Abelian_group S) (free_Abelian_group T) \<longleftrightarrow> S \<subseteq> T"
+proof -
+  have "x \<in> T" if ST: "\<And>c:: 'a \<Rightarrow>\<^sub>0 int. Poly_Mapping.keys c \<subseteq> S \<longrightarrow> Poly_Mapping.keys c \<subseteq> T" and "x \<in> S" for x
+    using ST [of "frag_of x"] \<open>x \<in> S\<close> by simp
+  then show ?thesis
+    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)))"
+    (is "?h \<in> iso ?G ?H")
+proof (rule isoI)
+  show hom: "?h \<in> hom ?G ?H"
+  proof (rule homI)
+    show "?h c \<in> carrier ?H" if "c \<in> carrier ?G" for c
+      using that
+      apply (simp add: sum.G_def carrier_sum_group)
+      apply (rule order_trans [OF keys_sum])
+      apply (auto simp: free_Abelian_group_def)
+      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
+  qed
+  interpret GH: group_hom "?G" "?H" "?h"
+    using hom by (simp add: group_hom_def group_hom_axioms_def)
+  show "bij_betw ?h (carrier ?G) (carrier ?H)"
+    unfolding bij_betw_def
+  proof (intro conjI subset_antisym)
+    show "?h ` carrier ?G \<subseteq> carrier ?H"
+      apply (clarsimp simp: sum.G_def carrier_sum_group simp del: carrier_free_Abelian_group_iff)
+      by (force simp: PiE_def Pi_iff intro!: sum_closed_free_Abelian_group)
+    have *: "poly_mapping.lookup (Abs_poly_mapping (\<lambda>j. if j \<in> S i then poly_mapping.lookup x j else 0)) k
+           = (if k \<in> S i then poly_mapping.lookup x k else 0)" if "i \<in> I" for i k and x :: "'b \<Rightarrow>\<^sub>0 int"
+      using that by (auto simp: conj_commute cong: conj_cong)
+    have eq: "Abs_poly_mapping (\<lambda>j. if j \<in> S i then poly_mapping.lookup x j else 0) = 0
+     \<longleftrightarrow> (\<forall>c \<in> S i. poly_mapping.lookup x c = 0)" if "i \<in> I" for i and x :: "'b \<Rightarrow>\<^sub>0 int"
+      apply (auto simp: poly_mapping_eq_iff fun_eq_iff)
+      apply (simp add: * Abs_poly_mapping_inverse conj_commute cong: conj_cong)
+      apply (force dest!: spec split: if_split_asm)
+      done
+    have "x \<in> ?h ` {x \<in> \<Pi>\<^sub>E i\<in>I. {c. Poly_Mapping.keys c \<subseteq> S i}. finite {i \<in> I. x i \<noteq> 0}}"
+      if x: "Poly_Mapping.keys x \<subseteq> \<Union> (S ` I)" for x :: "'b \<Rightarrow>\<^sub>0 int"
+    proof -
+      let ?f = "(\<lambda>i c. if c \<in> S i then Poly_Mapping.lookup x c else 0)"
+      define J where "J \<equiv> {i \<in> I. \<exists>c\<in>S i. c \<in> Poly_Mapping.keys x}"
+      have "J \<subseteq> (\<lambda>c. THE i. i \<in> I \<and> c \<in> S i) ` Poly_Mapping.keys x"
+      proof (clarsimp simp: J_def)
+        show "i \<in> (\<lambda>c. THE i. i \<in> I \<and> c \<in> S i) ` Poly_Mapping.keys x"
+          if "i \<in> I" "c \<in> S i" "c \<in> Poly_Mapping.keys x" for i c
+        proof
+          show "i = (THE i. i \<in> I \<and> c \<in> S i)"
+            using assms that by (auto simp: pairwise_def disjnt_def intro: the_equality [symmetric])
+        qed (simp add: that)
+      qed
+      then have fin: "finite J"
+        using finite_subset finite_keys by blast
+      have [simp]: "Poly_Mapping.keys (Abs_poly_mapping (?f i)) = {k. ?f i k \<noteq> 0}" if "i \<in> I" for i
+        by (simp add: eq_onp_def keys.abs_eq conj_commute cong: conj_cong)
+      have [simp]: "Poly_Mapping.lookup (Abs_poly_mapping (?f i)) c = ?f i c" if "i \<in> I" for i c
+        by (auto simp: Abs_poly_mapping_inverse conj_commute cong: conj_cong)
+      show ?thesis
+      proof
+        have "poly_mapping.lookup x c = poly_mapping.lookup (?h (\<lambda>i\<in>I. Abs_poly_mapping (?f i))) c"
+          for c
+        proof (cases "c \<in> Poly_Mapping.keys x")
+          case True
+          then obtain i where "i \<in> I" "c \<in> S i" "?f i c \<noteq> 0"
+            using x by (auto simp: in_keys_iff)
+          then have 1: "poly_mapping.lookup (sum' (\<lambda>j. Abs_poly_mapping (?f j)) (I - {i})) c = 0"
+            using assms
+            apply (simp add: sum.G_def Poly_Mapping.lookup_sum pairwise_def disjnt_def)
+            apply (force simp: eq split: if_split_asm intro!: comm_monoid_add_class.sum.neutral)
+            done
+          have 2: "poly_mapping.lookup x c = poly_mapping.lookup (Abs_poly_mapping (?f i)) c"
+            by (auto simp: \<open>c \<in> S i\<close> Abs_poly_mapping_inverse conj_commute cong: conj_cong)
+          have "finite {i \<in> I. Abs_poly_mapping (?f i) \<noteq> 0}"
+            by (rule finite_subset [OF _ fin]) (use \<open>i \<in> I\<close> J_def eq in \<open>auto simp: in_keys_iff\<close>)
+          with \<open>i \<in> I\<close> have "?h (\<lambda>j\<in>I. Abs_poly_mapping (?f j)) = Abs_poly_mapping (?f i) + sum' (\<lambda>j. Abs_poly_mapping (?f j)) (I - {i})"
+            apply (simp add: sum_diff1')
+            sorry
+          then show ?thesis
+            by (simp add: 1 2 Poly_Mapping.lookup_add)
+        next
+          case False
+          then have "poly_mapping.lookup x c = 0"
+            using keys.rep_eq by force
+          then show ?thesis
+            unfolding sum.G_def by (simp add: lookup_sum * comm_monoid_add_class.sum.neutral)
+        qed
+        then show "x = ?h (\<lambda>i\<in>I. Abs_poly_mapping (?f i))"
+          by (rule poly_mapping_eqI)
+        have "(\<lambda>i. Abs_poly_mapping (?f i)) \<in> (\<Pi> i\<in>I. {c. Poly_Mapping.keys c \<subseteq> S i})"
+          by (auto simp: PiE_def Pi_def in_keys_iff)
+        then show "(\<lambda>i\<in>I. Abs_poly_mapping (?f i))
+                 \<in> {x \<in> \<Pi>\<^sub>E i\<in>I. {c. Poly_Mapping.keys c \<subseteq> S i}. finite {i \<in> I. x i \<noteq> 0}}"
+          using fin unfolding J_def by (simp add: eq in_keys_iff cong: conj_cong)
+      qed
+    qed
+    then show "carrier ?H \<subseteq> ?h ` carrier ?G"
+      by (simp add: carrier_sum_group) (auto simp: free_Abelian_group_def)
+    show "inj_on ?h (carrier (sum_group I (\<lambda>i. free_Abelian_group (S i))))"
+      unfolding GH.inj_on_one_iff
+    proof clarify
+      fix x
+      assume "x \<in> carrier ?G" "?h x = \<one>\<^bsub>?H\<^esub>"
+      then have eq0: "sum' x I = 0"
+        and xs: "\<And>i. i \<in> I \<Longrightarrow> Poly_Mapping.keys (x i) \<subseteq> S i" and xext: "x \<in> extensional I"
+        and fin: "finite {i \<in> I. x i \<noteq> 0}"
+        by (simp_all add: carrier_sum_group PiE_def Pi_def)
+      have "x i = 0" if "i \<in> I" for i
+      proof -
+        have "sum' x (insert i (I - {i})) = 0"
+          using eq0 that by (simp add: insert_absorb)
+        moreover have "Poly_Mapping.keys (sum' x (I - {i})) = {}"
+        proof -
+          have "x i = - sum' x (I - {i})"
+            by (metis (mono_tags, lifting) diff_zero eq0 fin sum_diff1' minus_diff_eq that)
+          then have "Poly_Mapping.keys (x i) = Poly_Mapping.keys (sum' x (I - {i}))"
+            by simp
+          then have "Poly_Mapping.keys (sum' x (I - {i})) \<subseteq> S i"
+            using that xs by metis
+          moreover
+          have "Poly_Mapping.keys (sum' x (I - {i})) \<subseteq> (\<Union>j \<in> I - {i}. S j)"
+          proof -
+            have "Poly_Mapping.keys (sum' x (I - {i})) \<subseteq> (\<Union>i\<in>{j \<in> I. j \<noteq> i \<and> x j \<noteq> 0}. Poly_Mapping.keys (x i))"
+              using keys_sum [of x "{j \<in> I. j \<noteq> i \<and> x j \<noteq> 0}"] by (simp add: sum.G_def)
+            also have "\<dots> \<subseteq> \<Union> (S ` (I - {i}))"
+              using xs by force
+            finally show ?thesis .
+          qed
+          moreover have "A = {}" if "A \<subseteq> S i" "A \<subseteq> \<Union> (S ` (I - {i}))" for A
+            using assms that \<open>i \<in> I\<close>
+            by (force simp: pairwise_def disjnt_def image_def subset_iff)
+          ultimately show ?thesis
+            by metis
+        qed
+        then have [simp]: "sum' x (I - {i}) = 0"
+          by (auto simp: sum.G_def)
+        have "sum' x (insert i (I - {i})) = x i"
+          by (subst sum.insert' [OF finite_subset [OF _ fin]]) auto
+        ultimately show ?thesis
+          by metis
+      qed
+      with xext [unfolded extensional_def]
+      show "x = \<one>\<^bsub>sum_group I (\<lambda>i. free_Abelian_group (S i))\<^esub>"
+        by (force simp: free_Abelian_group_def)
+    qed
+  qed
+qed
+
+lemma isomorphic_free_Abelian_group_Union:
+  "pairwise disjnt I \<Longrightarrow> free_Abelian_group(\<Union> I) \<cong> sum_group I free_Abelian_group"
+  using iso_free_Abelian_group_sum [of "\<lambda>X. X" I]
+  by (metis SUP_identity_eq empty_iff group.iso_sym group_free_Abelian_group is_iso_def sum_group)
+
+lemma isomorphic_sum_integer_group:
+   "sum_group I (\<lambda>i. integer_group) \<cong> free_Abelian_group I"
+proof -
+  have "sum_group I (\<lambda>i. integer_group) \<cong> sum_group I (\<lambda>i. free_Abelian_group {i})"
+    by (rule iso_sum_groupI) (auto simp: isomorphic_group_integer_free_Abelian_group_singleton)
+  also have "\<dots> \<cong> free_Abelian_group I"
+    using iso_free_Abelian_group_sum [of "\<lambda>x. {x}" I] by (auto simp: is_iso_def)
+  finally show ?thesis .
+qed
+
+end
--- a/src/HOL/Algebra/Generated_Groups.thy	Thu Apr 04 22:18:32 2019 +0200
+++ b/src/HOL/Algebra/Generated_Groups.thy	Thu Apr 04 22:21:09 2019 +0200
@@ -2,12 +2,14 @@
     Author:     Paulo Emílio de Vilhena
 *)
 
+section \<open>Generated Groups\<close>
+
 theory Generated_Groups
   imports Group Coset
   
 begin
 
-section \<open>Generated Groups\<close>
+subsection \<open>Generated Groups\<close>
 
 inductive_set generate :: "('a, 'b) monoid_scheme \<Rightarrow> 'a set \<Rightarrow> 'a set"
   for G and H where
@@ -17,7 +19,7 @@
   | eng:  "h1 \<in> generate G H \<Longrightarrow> h2 \<in> generate G H \<Longrightarrow> h1 \<otimes>\<^bsub>G\<^esub> h2 \<in> generate G H"
 
 
-subsection \<open>Basic Properties\<close>
+subsubsection \<open>Basic Properties\<close>
 
 lemma (in group) generate_consistent:
   assumes "K \<subseteq> H" "subgroup H G" shows "generate (G \<lparr> carrier := H \<rparr>) K = generate G K"
@@ -195,9 +197,9 @@
 qed
 
 
-section \<open>Derived Subgroup\<close>
+subsection \<open>Derived Subgroup\<close>
 
-subsection \<open>Definitions\<close>
+subsubsection \<open>Definitions\<close>
 
 abbreviation derived_set :: "('a, 'b) monoid_scheme \<Rightarrow> 'a set \<Rightarrow> 'a set"
   where "derived_set G H \<equiv>
@@ -207,7 +209,7 @@
   "derived G H = generate G (derived_set G H)"
 
 
-subsection \<open>Basic Properties\<close>
+subsubsection \<open>Basic Properties\<close>
 
 lemma (in group) derived_set_incl:
   assumes "K \<subseteq> H" "subgroup H G" shows "derived_set G K \<subseteq> H"
@@ -444,7 +446,7 @@
   using derived_img[OF G.exp_of_derived_in_carrier[OF assms]] by (induct n) (auto)
 
 
-subsection \<open>Generated subgroup of a group\<close>
+subsubsection \<open>Generated subgroup of a group\<close>
 
 definition subgroup_generated :: "('a, 'b) monoid_scheme \<Rightarrow> 'a set \<Rightarrow> ('a, 'b) monoid_scheme"
   where "subgroup_generated G S = G\<lparr>carrier := generate G (carrier G \<inter> S)\<rparr>"
@@ -600,4 +602,114 @@
   "kernel G (subgroup_generated H S) f = kernel G H f"
   by (simp add: kernel_def)
 
+subsection \<open>And homomorphisms\<close>
+
+lemma (in group) hom_from_subgroup_generated:
+   "h \<in> hom G H \<Longrightarrow> h \<in> hom(subgroup_generated G A) H"
+  apply (simp add: hom_def carrier_subgroup_generated Pi_iff)
+  apply (metis group.generate_in_carrier inf_le1 is_group)
+  done
+
+lemma hom_into_subgroup:
+   "\<lbrakk>h \<in> hom G G'; h ` (carrier G) \<subseteq> H\<rbrakk> \<Longrightarrow> h \<in> hom G (subgroup_generated G' H)"
+  by (auto simp: hom_def carrier_subgroup_generated Pi_iff generate.incl image_subset_iff)
+
+lemma hom_into_subgroup_eq_gen:
+    "group G \<Longrightarrow>
+     h \<in> hom K (subgroup_generated G H)
+ \<longleftrightarrow> h \<in> hom K G \<and> h ` (carrier K) \<subseteq> carrier(subgroup_generated G H)"
+  using group.carrier_subgroup_generated_subset [of G H] by (auto simp: hom_def)
+
+lemma hom_into_subgroup_eq:
+   "\<lbrakk>subgroup H G; group G\<rbrakk>
+    \<Longrightarrow> (h \<in> hom K (subgroup_generated G H) \<longleftrightarrow> h \<in> hom K G \<and> h ` (carrier K) \<subseteq> H)"
+  by (simp add: hom_into_subgroup_eq_gen image_subset_iff subgroup.carrier_subgroup_generated_subgroup)
+
+lemma (in group_hom) hom_between_subgroups:
+  assumes "h ` A \<subseteq> B"
+  shows "h \<in> hom (subgroup_generated G A) (subgroup_generated H B)"
+proof -
+  have [simp]: "group G" "group H"
+    by (simp_all add: G.is_group H.is_group)
+  have "x \<in> generate G (carrier G \<inter> A) \<Longrightarrow> h x \<in> generate H (carrier H \<inter> B)" for x
+  proof (induction x rule: generate.induct)
+    case (incl h)
+    then show ?case
+      by (meson IntE IntI assms generate.incl hom_closed image_subset_iff)
+  next
+    case (inv h)
+    then show ?case
+      by (metis G.inv_closed G.inv_inv IntE IntI assms generate.simps hom_inv image_subset_iff local.inv_closed)
+  next
+    case (eng h1 h2)
+    then show ?case
+      by (metis G.generate_in_carrier generate.simps inf.cobounded1 local.hom_mult)
+  qed (auto simp: generate.intros)
+  then have "h ` carrier (subgroup_generated G A) \<subseteq> carrier (subgroup_generated H B)"
+    using group.carrier_subgroup_generated_subset [of G A]
+    by (auto simp: carrier_subgroup_generated)
+  then show ?thesis
+    by (simp add: hom_into_subgroup_eq_gen group.hom_from_subgroup_generated homh)
+qed
+
+lemma (in group_hom) subgroup_generated_by_image:
+  assumes "S \<subseteq> carrier G"
+  shows "carrier (subgroup_generated H (h ` S)) = h ` (carrier(subgroup_generated G S))"
+proof
+  have "x \<in> generate H (carrier H \<inter> h ` S) \<Longrightarrow> x \<in> h ` generate G (carrier G \<inter> S)" for x
+  proof (erule generate.induct)
+    show "\<one>\<^bsub>H\<^esub> \<in> h ` generate G (carrier G \<inter> S)"
+      using generate.one by force
+  next
+    fix f
+    assume "f \<in> carrier H \<inter> h ` S"
+    with assms show "f \<in> h ` generate G (carrier G \<inter> S)" "inv\<^bsub>H\<^esub> f \<in> h ` generate G (carrier G \<inter> S)"
+       apply (auto simp: Int_absorb1 generate.incl)
+      apply (metis generate.simps hom_inv imageI subsetCE)
+      done
+  next
+    fix h1 h2
+    assume
+      "h1 \<in> generate H (carrier H \<inter> h ` S)" "h1 \<in> h ` generate G (carrier G \<inter> S)"
+      "h2 \<in> generate H (carrier H \<inter> h ` S)" "h2 \<in> h ` generate G (carrier G \<inter> S)"
+    then show "h1 \<otimes>\<^bsub>H\<^esub> h2 \<in> h ` generate G (carrier G \<inter> S)"
+      using H.subgroupE(4) group.generate_is_subgroup subgroup_img_is_subgroup
+      by (simp add: G.generate_is_subgroup)
+  qed
+  then
+  show "carrier (subgroup_generated H (h ` S)) \<subseteq> h ` carrier (subgroup_generated G S)"
+    by (auto simp: carrier_subgroup_generated)
+next
+  have "h ` S \<subseteq> carrier H"
+    by (metis (no_types) assms hom_closed image_subset_iff subsetCE)
+  then show "h ` carrier (subgroup_generated G S) \<subseteq> carrier (subgroup_generated H (h ` S))"
+    apply (clarsimp simp: carrier_subgroup_generated)
+    by (metis Int_absorb1 assms generate_img imageI)
+qed
+
+lemma (in group_hom) iso_between_subgroups:
+  assumes "h \<in> iso G H" "S \<subseteq> carrier G" "h ` S = T"
+  shows "h \<in> iso (subgroup_generated G S) (subgroup_generated H T)"
+  using assms
+  by (metis G.carrier_subgroup_generated_subset Group.iso_iff hom_between_subgroups inj_on_subset subgroup_generated_by_image subsetI)
+
+lemma (in group) subgroup_generated_group_carrier:
+  "subgroup_generated G (carrier G) = G"
+proof (rule monoid.equality)
+  show "carrier (subgroup_generated G (carrier G)) = carrier G"
+    by (simp add: subgroup.carrier_subgroup_generated_subgroup subgroup_self)
+qed (auto simp: subgroup_generated_def)
+
+lemma iso_onto_image:
+  assumes "group G" "group H"
+  shows
+   "f \<in> iso G (subgroup_generated H (f ` carrier G)) \<longleftrightarrow> f \<in> hom G H \<and> inj_on f (carrier G)"
+  using assms
+  apply (auto simp: iso_def bij_betw_def hom_into_subgroup_eq_gen carrier_subgroup_generated hom_carrier generate.incl Int_absorb1 Int_absorb2)
+  by (metis group.generateI group.subgroupE(1) group.subgroup_self group_hom.generate_img group_hom.intro group_hom_axioms.intro)
+
+lemma (in group) iso_onto_image:
+   "group H \<Longrightarrow> f \<in> iso G (subgroup_generated H (f ` carrier G)) \<longleftrightarrow> f \<in> mon G H"
+  by (simp add: mon_def epi_def hom_into_subgroup_eq_gen iso_onto_image)
+
 end
\ No newline at end of file
--- a/src/HOL/Algebra/Group.thy	Thu Apr 04 22:18:32 2019 +0200
+++ b/src/HOL/Algebra/Group.thy	Thu Apr 04 22:21:09 2019 +0200
@@ -186,7 +186,10 @@
 locale group = monoid +
   assumes Units: "carrier G <= Units G"
 
-lemma (in group) is_group: "group G" by (rule group_axioms)
+lemma (in group) is_group [iff]: "group G" by (rule group_axioms)
+
+lemma (in group) is_monoid [iff]: "monoid G"
+  by (rule monoid_axioms)
 
 theorem groupI:
   fixes G (structure)
@@ -825,6 +828,9 @@
 lemma mult_DirProd [simp]: "(g, h) \<otimes>\<^bsub>(G \<times>\<times> H)\<^esub> (g', h') = (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')"
   by (simp add: DirProd_def)
 
+lemma mult_DirProd': "x \<otimes>\<^bsub>(G \<times>\<times> H)\<^esub> y = (fst x \<otimes>\<^bsub>G\<^esub> fst y, snd x \<otimes>\<^bsub>H\<^esub> snd y)"
+  by (subst mult_DirProd [symmetric]) simp
+
 lemma DirProd_assoc: "(G \<times>\<times> H \<times>\<times> I) = (G \<times>\<times> (H \<times>\<times> I))"
   by auto
 
@@ -858,7 +864,7 @@
   ultimately show "Group.group ((G \<times>\<times> K)\<lparr>carrier := H \<times> I\<rparr>)" by simp
 qed
 
-subsection \<open>Homomorphisms and Isomorphisms\<close>
+subsection \<open>Homomorphisms (mono and epi) and Isomorphisms\<close>
 
 definition
   hom :: "_ => _ => ('a => 'b) set" where
@@ -923,6 +929,14 @@
 corollary iso_refl [simp]: "G \<cong> G"
   using iso_set_refl unfolding is_iso_def by auto
 
+lemma iso_iff:
+   "h \<in> iso G H \<longleftrightarrow> h \<in> hom G H \<and> h ` (carrier G) = carrier H \<and> inj_on h (carrier G)"
+  by (auto simp: iso_def hom_def bij_betw_def)
+
+lemma iso_imp_homomorphism:
+   "h \<in> iso G H \<Longrightarrow> h \<in> hom G H"
+  by (simp add: iso_iff)
+
 lemma trivial_hom:
    "group H \<Longrightarrow> (\<lambda>x. one H) \<in> hom G H"
   by (auto simp: hom_def Group.group_def)
@@ -965,7 +979,6 @@
     by (simp add: Group.iso_def bij_betw_inv_into h)
 qed
 
-
 corollary (in group) iso_sym: "G \<cong> H \<Longrightarrow> H \<cong> G"
   using iso_set_sym unfolding is_iso_def by auto
 
@@ -979,6 +992,50 @@
 lemma iso_same_card: "G \<cong> H \<Longrightarrow> card (carrier G) = card (carrier H)"
   using bij_betw_same_card  unfolding is_iso_def iso_def by auto
 
+lemma iso_finite: "G \<cong> H \<Longrightarrow> finite(carrier G) \<longleftrightarrow> finite(carrier H)"
+  by (auto simp: is_iso_def iso_def bij_betw_finite)
+
+lemma mon_compose:
+   "\<lbrakk>f \<in> mon G H; g \<in> mon H K\<rbrakk> \<Longrightarrow> (g \<circ> f) \<in> mon G K"
+  by (auto simp: mon_def intro: hom_compose comp_inj_on inj_on_subset [OF _ hom_carrier])
+
+lemma mon_compose_rev:
+   "\<lbrakk>f \<in> hom G H; g \<in> hom H K; (g \<circ> f) \<in> mon G K\<rbrakk> \<Longrightarrow> f \<in> mon G H"
+  using inj_on_imageI2 by (auto simp: mon_def)
+
+lemma epi_compose:
+   "\<lbrakk>f \<in> epi G H; g \<in> epi H K\<rbrakk> \<Longrightarrow> (g \<circ> f) \<in> epi G K"
+  using hom_compose by (force simp: epi_def hom_compose simp flip: image_image)
+
+lemma epi_compose_rev:
+   "\<lbrakk>f \<in> hom G H; g \<in> hom H K; (g \<circ> f) \<in> epi G K\<rbrakk> \<Longrightarrow> g \<in> epi H K"
+  by (fastforce simp: epi_def hom_def Pi_iff image_def set_eq_iff)
+
+lemma iso_compose_rev:
+   "\<lbrakk>f \<in> hom G H; g \<in> hom H K; (g \<circ> f) \<in> iso G K\<rbrakk> \<Longrightarrow> f \<in> mon G H \<and> g \<in> epi H K"
+  unfolding iso_iff_mon_epi using mon_compose_rev epi_compose_rev by blast
+
+lemma epi_iso_compose_rev:
+  assumes "f \<in> epi G H" "g \<in> hom H K" "(g \<circ> f) \<in> iso G K"
+  shows "f \<in> iso G H \<and> g \<in> iso H K"
+proof
+  show "f \<in> iso G H"
+    by (metis (no_types, lifting) assms epi_def iso_compose_rev iso_iff_mon_epi mem_Collect_eq)
+  then have "f \<in> hom G H \<and> bij_betw f (carrier G) (carrier H)"
+    using Group.iso_def \<open>f \<in> Group.iso G H\<close> by blast
+  then have "bij_betw g (carrier H) (carrier K)"
+    using Group.iso_def assms(3) bij_betw_comp_iff by blast
+  then show "g \<in> iso H K"
+    using Group.iso_def assms(2) by blast
+qed
+
+lemma mon_left_invertible:
+   "\<lbrakk>f \<in> hom G H; \<And>x. x \<in> carrier G \<Longrightarrow> g(f x) = x\<rbrakk> \<Longrightarrow> f \<in> mon G H"
+  by (simp add: mon_def inj_on_def) metis
+
+lemma epi_right_invertible:
+   "\<lbrakk>g \<in> hom H G; f \<in> carrier G \<rightarrow> carrier H; \<And>x. x \<in> carrier G \<Longrightarrow> g(f x) = x\<rbrakk> \<Longrightarrow> g \<in> epi H G"
+  by (force simp: Pi_iff epi_iff_subset image_subset_iff_funcset subset_iff)
 
 lemma (in monoid) hom_imp_img_monoid: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "h \<in> hom G H"
@@ -1109,6 +1166,43 @@
   ultimately show ?thesis by simp
 qed
 
+subsubsection \<open>HOL Light's concept of an isomorphism pair\<close>
+
+definition group_isomorphisms
+  where
+ "group_isomorphisms G H f g \<equiv>
+        f \<in> hom G H \<and> g \<in> hom H G \<and>
+        (\<forall>x \<in> carrier G. g(f x) = x) \<and>
+        (\<forall>y \<in> carrier H. f(g y) = y)"
+
+lemma group_isomorphisms_sym: "group_isomorphisms G H f g \<Longrightarrow> group_isomorphisms H G g f"
+  by (auto simp: group_isomorphisms_def)
+
+lemma group_isomorphisms_imp_iso: "group_isomorphisms G H f g \<Longrightarrow> f \<in> iso G H"
+by (auto simp: iso_def inj_on_def image_def group_isomorphisms_def hom_def bij_betw_def Pi_iff, metis+)
+
+lemma (in group) iso_iff_group_isomorphisms:
+  "f \<in> iso G H \<longleftrightarrow> (\<exists>g. group_isomorphisms G H f g)"
+proof safe
+  show "\<exists>g. group_isomorphisms G H f g" if "f \<in> Group.iso G H"
+    unfolding group_isomorphisms_def
+  proof (intro exI conjI)
+    let ?g = "inv_into (carrier G) f"
+    show "\<forall>x\<in>carrier G. ?g (f x) = x"
+      by (metis (no_types, lifting) Group.iso_def bij_betw_inv_into_left mem_Collect_eq that)
+    show "\<forall>y\<in>carrier H. f (?g y) = y"
+      by (metis (no_types, lifting) Group.iso_def bij_betw_inv_into_right mem_Collect_eq that)
+  qed (use Group.iso_def iso_set_sym that in \<open>blast+\<close>)
+next
+  fix g
+  assume "group_isomorphisms G H f g"
+  then show "f \<in> Group.iso G H"
+    by (auto simp: iso_def group_isomorphisms_def hom_in_carrier intro: bij_betw_byWitness)
+qed
+
+
+subsubsection \<open>Involving direct products\<close>
+
 lemma DirProd_commute_iso_set:
   shows "(\<lambda>(x,y). (y,x)) \<in> iso (G \<times>\<times> H) (H \<times>\<times> G)"
   by (auto simp add: iso_def hom_def inj_on_def bij_betw_def)
@@ -1141,6 +1235,49 @@
   shows "G \<times>\<times> H \<cong> G2 \<times>\<times> I"
   using DirProd_iso_set_trans assms unfolding is_iso_def by blast
 
+lemma hom_pairwise: "f \<in> hom G (DirProd H K) \<longleftrightarrow> (fst \<circ> f) \<in> hom G H \<and> (snd \<circ> f) \<in> hom G K"
+  apply (auto simp: hom_def mult_DirProd' dest: Pi_mem)
+   apply (metis Product_Type.mem_Times_iff comp_eq_dest_lhs funcset_mem)
+  by (metis mult_DirProd prod.collapse)
+
+lemma hom_paired:
+   "(\<lambda>x. (f x,g x)) \<in> hom G (DirProd H K) \<longleftrightarrow> f \<in> hom G H \<and> g \<in> hom G K"
+  by (simp add: hom_pairwise o_def)
+
+lemma hom_paired2:
+  assumes "group G" "group H"
+  shows "(\<lambda>(x,y). (f x,g y)) \<in> hom (DirProd G H) (DirProd G' H') \<longleftrightarrow> f \<in> hom G G' \<and> g \<in> hom H H'"
+  using assms
+  by (fastforce simp: hom_def Pi_def dest!: group.is_monoid)
+
+lemma iso_paired2:
+  assumes "group G" "group H"
+  shows "(\<lambda>(x,y). (f x,g y)) \<in> iso (DirProd G H) (DirProd G' H') \<longleftrightarrow> f \<in> iso G G' \<and> g \<in> iso H H'"
+  using assms
+  by (fastforce simp add: iso_def inj_on_def bij_betw_def hom_paired2 image_paired_Times
+      times_eq_iff group_def monoid.carrier_not_empty)
+
+lemma hom_of_fst:
+  assumes "group H"
+  shows "(f \<circ> fst) \<in> hom (DirProd G H) K \<longleftrightarrow> f \<in> hom G K"
+proof -
+  interpret group H
+    by (rule assms)
+  show ?thesis
+    using one_closed by (auto simp: hom_def Pi_def)
+qed
+
+lemma hom_of_snd:
+  assumes "group G"
+  shows "(f \<circ> snd) \<in> hom (DirProd G H) K \<longleftrightarrow> f \<in> hom H K"
+proof -
+  interpret group G
+    by (rule assms)
+  show ?thesis
+    using one_closed by (auto simp: hom_def Pi_def)
+qed
+
+
 subsection\<open>The locale for a homomorphism between two groups\<close>
 
 text\<open>Basis for homomorphism proofs: we assume two groups \<^term>\<open>G\<close> and
@@ -1172,7 +1309,8 @@
 proof -
   have "h \<one> \<otimes>\<^bsub>H\<^esub> \<one>\<^bsub>H\<^esub> = h \<one> \<otimes>\<^bsub>H\<^esub> h \<one>"
     by (simp add: hom_mult [symmetric] del: hom_mult)
-  then show ?thesis by (simp del: r_one)
+  then show ?thesis
+    by (metis H.Units_eq H.Units_l_cancel H.one_closed local.one_closed)
 qed
 
 lemma hom_one:
@@ -1383,6 +1521,11 @@
   finally show "x \<otimes>\<^bsub>(?h_img)\<^esub> y = y \<otimes>\<^bsub>(?h_img)\<^esub> x" .
 qed
 
+lemma (in comm_group) hom_group_mult:
+  assumes "f \<in> hom H G" "g \<in> hom H G"
+ shows "(\<lambda>x. f x \<otimes>\<^bsub>G\<^esub> g x) \<in> hom H G"
+    using assms by (auto simp: hom_def Pi_def m_ac)
+
 lemma (in comm_group) hom_imp_img_comm_group: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "h \<in> hom G H"
   shows "comm_group (H \<lparr> carrier := h ` (carrier G), one := h \<one>\<^bsub>G\<^esub> \<rparr>)"
@@ -1465,10 +1608,6 @@
   "subgroup H G ==> group (G\<lparr>carrier := H\<rparr>)"
   by (erule subgroup.subgroup_is_group) (rule group_axioms)
 
-lemma (in group) is_monoid [intro, simp]:
-  "monoid G"
-  by (auto intro: monoid.intro m_assoc)
-
 lemma (in group) subgroup_mult_equality:
   "\<lbrakk> subgroup H G; h1 \<in> H; h2 \<in> H \<rbrakk> \<Longrightarrow>  h1 \<otimes>\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> h2 = h1 \<otimes> h2"
   unfolding subgroup_def by simp
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/Product_Groups.thy	Thu Apr 04 22:21:09 2019 +0200
@@ -0,0 +1,480 @@
+(*  Title:      HOL/Algebra/Product_Groups.thy
+    Author:     LC Paulson (ported from HOL Light)
+*)
+
+section \<open>Product and Sum Groups\<close>
+
+theory Product_Groups
+  imports Elementary_Groups "HOL-Library.Equipollence" 
+  
+begin
+
+subsection \<open>Product of a Family of Groups\<close>
+
+definition product_group:: "'a set \<Rightarrow> ('a \<Rightarrow> ('b, 'c) monoid_scheme) \<Rightarrow> ('a \<Rightarrow> 'b) monoid"
+  where "product_group I G \<equiv> \<lparr>carrier = (\<Pi>\<^sub>E i\<in>I. carrier (G i)),
+                              monoid.mult = (\<lambda>x y. (\<lambda>i\<in>I. x i \<otimes>\<^bsub>G i\<^esub> y i)),
+                              one = (\<lambda>i\<in>I. \<one>\<^bsub>G i\<^esub>)\<rparr>"
+
+lemma carrier_product_group [simp]: "carrier(product_group I G) = (\<Pi>\<^sub>E i\<in>I. carrier (G i))"
+  by (simp add: product_group_def)
+
+lemma one_product_group [simp]: "one(product_group I G) = (\<lambda>i\<in>I. one (G i))"
+  by (simp add: product_group_def)
+
+lemma mult_product_group [simp]: "(\<otimes>\<^bsub>product_group I G\<^esub>) = (\<lambda>x y. \<lambda>i\<in>I. x i \<otimes>\<^bsub>G i\<^esub> y i)"
+  by (simp add: product_group_def)
+
+lemma product_group [simp]:
+  assumes "\<And>i. i \<in> I \<Longrightarrow> group (G i)" shows "group (product_group I G)"
+proof (rule groupI; simp)
+  show "(\<lambda>i. x i \<otimes>\<^bsub>G i\<^esub> y i) \<in> (\<Pi> i\<in>I. carrier (G i))"
+    if "x \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" "y \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" for x y
+    using that assms group.subgroup_self subgroup.m_closed by fastforce
+  show "(\<lambda>i. \<one>\<^bsub>G i\<^esub>) \<in> (\<Pi> i\<in>I. carrier (G i))"
+    by (simp add: assms group.is_monoid)
+  show "(\<lambda>i\<in>I. (if i \<in> I then x i \<otimes>\<^bsub>G i\<^esub> y i else undefined) \<otimes>\<^bsub>G i\<^esub> z i) =
+        (\<lambda>i\<in>I. x i \<otimes>\<^bsub>G i\<^esub> (if i \<in> I then y i \<otimes>\<^bsub>G i\<^esub> z i else undefined))"
+    if "x \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" "y \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" "z \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" for x y z
+    using that  by (auto simp: PiE_iff assms group.is_monoid monoid.m_assoc intro: restrict_ext)
+  show "(\<lambda>i\<in>I. (if i \<in> I then \<one>\<^bsub>G i\<^esub> else undefined) \<otimes>\<^bsub>G i\<^esub> x i) = x"
+    if "x \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" for x
+    using assms that by (fastforce simp: Group.group_def PiE_iff)
+  show "\<exists>y\<in>\<Pi>\<^sub>E i\<in>I. carrier (G i). (\<lambda>i\<in>I. y i \<otimes>\<^bsub>G i\<^esub> x i) = (\<lambda>i\<in>I. \<one>\<^bsub>G i\<^esub>)"
+    if "x \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" for x
+    by (rule_tac x="\<lambda>i\<in>I. inv\<^bsub>G i\<^esub> x i" in bexI) (use assms that in \<open>auto simp: PiE_iff group.l_inv\<close>)
+qed
+
+lemma inv_product_group [simp]:
+  assumes "f \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" "\<And>i. i \<in> I \<Longrightarrow> group (G i)"
+  shows "inv\<^bsub>product_group I G\<^esub> f = (\<lambda>i\<in>I. inv\<^bsub>G i\<^esub> f i)"
+proof (rule group.inv_equality)
+  show "Group.group (product_group I G)"
+    by (simp add: assms)
+  show "(\<lambda>i\<in>I. inv\<^bsub>G i\<^esub> f i) \<otimes>\<^bsub>product_group I G\<^esub> f = \<one>\<^bsub>product_group I G\<^esub>"
+    using assms by (auto simp: PiE_iff group.l_inv)
+  show "f \<in> carrier (product_group I G)"
+    using assms by simp
+  show "(\<lambda>i\<in>I. inv\<^bsub>G i\<^esub> f i) \<in> carrier (product_group I G)"
+    using PiE_mem assms by fastforce
+qed
+
+
+lemma trivial_product_group: "trivial_group(product_group I G) \<longleftrightarrow> (\<forall>i \<in> I. trivial_group(G i))"
+ (is "?lhs = ?rhs")
+proof
+  assume L: ?lhs
+  then have "inv\<^bsub>product_group I G\<^esub> (\<lambda>a\<in>I. \<one>\<^bsub>G a\<^esub>) = \<one>\<^bsub>product_group I G\<^esub>"
+    by (metis group.is_monoid monoid.inv_one one_product_group trivial_group_def)
+  have [simp]: "\<one>\<^bsub>G i\<^esub> \<otimes>\<^bsub>G i\<^esub> \<one>\<^bsub>G i\<^esub> = \<one>\<^bsub>G i\<^esub>" if "i \<in> I" for i
+    unfolding trivial_group_def
+  proof -
+    have 1: "(\<lambda>a\<in>I. \<one>\<^bsub>G a\<^esub>) i = \<one>\<^bsub>G i\<^esub>"
+      by (simp add: that)
+    have "(\<lambda>a\<in>I. \<one>\<^bsub>G a\<^esub>) = (\<lambda>a\<in>I. \<one>\<^bsub>G a\<^esub>) \<otimes>\<^bsub>product_group I G\<^esub> (\<lambda>a\<in>I. \<one>\<^bsub>G a\<^esub>)"
+      by (metis (no_types) L group.is_monoid monoid.l_one one_product_group singletonI trivial_group_def)
+    then show ?thesis
+      using 1 by (simp add: that)
+  qed
+  show ?rhs
+    using L
+    by (auto simp: trivial_group_def product_group_def PiE_eq_singleton intro: groupI)
+next
+  assume ?rhs
+  then show ?lhs
+    by (simp add: PiE_eq_singleton trivial_group_def)
+qed
+
+
+lemma PiE_subgroup_product_group:
+  assumes "\<And>i. i \<in> I \<Longrightarrow> group (G i)"
+  shows "subgroup (PiE I H) (product_group I G) \<longleftrightarrow> (\<forall>i \<in> I. subgroup (H i) (G i))"
+    (is "?lhs = ?rhs")
+proof
+  assume L: ?lhs
+  then have [simp]: "PiE I H \<noteq> {}"
+    using subgroup_nonempty by force
+  show ?rhs
+  proof (clarify; unfold_locales)
+    show sub: "H i \<subseteq> carrier (G i)" if "i \<in> I" for i
+      using that L by (simp add: subgroup_def) (metis (no_types, lifting) L subgroup_nonempty subset_PiE)
+    show "x \<otimes>\<^bsub>G i\<^esub> y \<in> H i" if "i \<in> I" "x \<in> H i" "y \<in> H i" for i x y
+    proof -
+      have *: "\<And>x. x \<in> Pi\<^sub>E I H \<Longrightarrow> (\<forall>y \<in> Pi\<^sub>E I H. \<forall>i\<in>I. x i \<otimes>\<^bsub>G i\<^esub> y i \<in> H i)"
+        using L by (auto simp: subgroup_def Pi_iff)
+      have "\<forall>y\<in>H i. f i \<otimes>\<^bsub>G i\<^esub> y \<in> H i" if f: "f \<in> Pi\<^sub>E I H" and "i \<in> I" for i f
+        using * [OF f] \<open>i \<in> I\<close>
+        by (subst(asm) all_PiE_elements) auto
+      then have "\<forall>f \<in> Pi\<^sub>E I H. \<forall>i \<in> I. \<forall>y\<in>H i. f i \<otimes>\<^bsub>G i\<^esub> y \<in> H i"
+        by blast
+      with that show ?thesis
+        by (subst(asm) all_PiE_elements) auto
+    qed
+    show "\<one>\<^bsub>G i\<^esub> \<in> H i" if "i \<in> I" for i
+      using L subgroup.one_closed that by fastforce
+    show "inv\<^bsub>G i\<^esub> x \<in> H i" if "i \<in> I" and x: "x \<in> H i" for i x
+    proof -
+      have *: "\<forall>y \<in> Pi\<^sub>E I H. \<forall>i\<in>I. inv\<^bsub>G i\<^esub> y i \<in> H i"
+      proof
+        fix y
+        assume y: "y \<in> Pi\<^sub>E I H"
+        then have yc: "y \<in> carrier (product_group I G)"
+          by (metis (no_types) L subgroup_def subsetCE)
+        have "inv\<^bsub>product_group I G\<^esub> y \<in> Pi\<^sub>E I H"
+          by (simp add: y L subgroup.m_inv_closed)
+        moreover have "inv\<^bsub>product_group I G\<^esub> y = (\<lambda>i\<in>I. inv\<^bsub>G i\<^esub> y i)"
+          using yc by (simp add: assms)
+        ultimately show "\<forall>i\<in>I. inv\<^bsub>G i\<^esub> y i \<in> H i"
+          by auto
+      qed
+      then have "\<forall>i\<in>I. \<forall>x\<in>H i. inv\<^bsub>G i\<^esub> x \<in> H i"
+        by (subst(asm) all_PiE_elements) auto
+      then show ?thesis
+        using that(1) x by blast
+    qed
+  qed
+next
+  assume R: ?rhs
+  show ?lhs
+  proof
+    show "Pi\<^sub>E I H \<subseteq> carrier (product_group I G)"
+      using R by (force simp: subgroup_def)
+    show "x \<otimes>\<^bsub>product_group I G\<^esub> y \<in> Pi\<^sub>E I H" if "x \<in> Pi\<^sub>E I H" "y \<in> Pi\<^sub>E I H" for x y
+      using R that by (auto simp: PiE_iff subgroup_def)
+    show "\<one>\<^bsub>product_group I G\<^esub> \<in> Pi\<^sub>E I H"
+      using R by (force simp: subgroup_def)
+    show "inv\<^bsub>product_group I G\<^esub> x \<in> Pi\<^sub>E I H" if "x \<in> Pi\<^sub>E I H" for x
+    proof -
+      have x: "x \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))"
+        using R that by (force simp:  subgroup_def)
+      show ?thesis
+        using assms R that by (fastforce simp: x assms subgroup_def)
+    qed
+  qed
+qed
+
+lemma product_group_subgroup_generated:
+  assumes "\<And>i. i \<in> I \<Longrightarrow> subgroup (H i) (G i)" and gp: "\<And>i. i \<in> I \<Longrightarrow> group (G i)"
+  shows "product_group I (\<lambda>i. subgroup_generated (G i) (H i))
+       = subgroup_generated (product_group I G) (PiE I H)"
+proof (rule monoid.equality)
+  have [simp]: "\<And>i. i \<in> I \<Longrightarrow> carrier (G i) \<inter> H i = H i" "(\<Pi>\<^sub>E i\<in>I. carrier (G i)) \<inter> Pi\<^sub>E I H = Pi\<^sub>E I H"
+    using assms by (force simp: subgroup_def)+
+  have "(\<Pi>\<^sub>E i\<in>I. generate (G i) (H i)) = generate (product_group I G) (Pi\<^sub>E I H)"
+  proof (rule group.generateI)
+    show "Group.group (product_group I G)"
+      using assms by simp
+    show "subgroup (\<Pi>\<^sub>E i\<in>I. generate (G i) (H i)) (product_group I G)"
+      using assms by (simp add: PiE_subgroup_product_group group.generate_is_subgroup subgroup.subset)
+    show "Pi\<^sub>E I H \<subseteq> (\<Pi>\<^sub>E i\<in>I. generate (G i) (H i))"
+      using assms by (auto simp: PiE_iff generate.incl)
+    show "(\<Pi>\<^sub>E i\<in>I. generate (G i) (H i)) \<subseteq> K"
+      if "subgroup K (product_group I G)" "Pi\<^sub>E I H \<subseteq> K" for K
+      using assms that group.generate_subgroup_incl by fastforce
+  qed
+  with assms
+  show "carrier (product_group I (\<lambda>i. subgroup_generated (G i) (H i))) =
+        carrier (subgroup_generated (product_group I G) (Pi\<^sub>E I H))"
+    by (simp add: carrier_subgroup_generated cong: PiE_cong)
+qed auto
+
+lemma finite_product_group:
+  assumes "\<And>i. i \<in> I \<Longrightarrow> group (G i)"
+  shows
+   "finite (carrier (product_group I G)) \<longleftrightarrow>
+    finite {i. i \<in> I \<and> ~ trivial_group(G i)} \<and> (\<forall>i \<in> I. finite(carrier(G i)))"
+proof -
+  have [simp]: "\<And>i. i \<in> I \<Longrightarrow> carrier (G i) \<noteq> {}"
+    using assms group.is_monoid by blast
+  show ?thesis
+    by (auto simp: finite_PiE_iff PiE_eq_empty_iff group.trivial_group_alt [OF assms] cong: Collect_cong conj_cong)
+qed
+
+subsection \<open>Sum of a Family of Groups\<close>
+
+definition sum_group :: "'a set \<Rightarrow> ('a \<Rightarrow> ('b, 'c) monoid_scheme) \<Rightarrow> ('a \<Rightarrow> 'b) monoid"
+  where "sum_group I G \<equiv>
+        subgroup_generated
+         (product_group I G)
+         {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}"
+
+lemma subgroup_sum_group:
+  assumes "\<And>i. i \<in> I \<Longrightarrow> group (G i)"
+  shows "subgroup {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}
+                  (product_group I G)"
+proof unfold_locales
+  fix x y
+  have *: "{i. (i \<in> I \<longrightarrow> x i \<otimes>\<^bsub>G i\<^esub> y i \<noteq> \<one>\<^bsub>G i\<^esub>) \<and> i \<in> I}
+        \<subseteq> {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>} \<union> {i \<in> I. y i \<noteq> \<one>\<^bsub>G i\<^esub>}"
+    by (auto simp: Group.group_def dest: assms)
+  assume
+    "x \<in> {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}"
+    "y \<in> {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}"
+  then
+  show "x \<otimes>\<^bsub>product_group I G\<^esub> y \<in> {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}"
+    using assms
+    apply (auto simp: Group.group_def monoid.m_closed PiE_iff)
+    apply (rule finite_subset [OF *])
+    by blast
+next
+  fix x
+  assume "x \<in> {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}"
+  then show "inv\<^bsub>product_group I G\<^esub> x \<in> {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}"
+    using assms
+    by (auto simp: PiE_iff assms group.inv_eq_1_iff [OF assms] conj_commute cong: rev_conj_cong)
+qed (use assms [unfolded Group.group_def] in auto)
+
+lemma carrier_sum_group:
+  assumes "\<And>i. i \<in> I \<Longrightarrow> group (G i)"
+  shows "carrier(sum_group I G) = {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}"
+proof -
+  interpret SG: subgroup "{x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}" "(product_group I G)"
+    by (simp add: assms subgroup_sum_group)
+  show ?thesis
+    by (simp add: sum_group_def subgroup_sum_group carrier_subgroup_generated_alt)
+qed
+
+lemma one_sum_group [simp]: "\<one>\<^bsub>sum_group I G\<^esub> = (\<lambda>i\<in>I. \<one>\<^bsub>G i\<^esub>)"
+  by (simp add: sum_group_def)
+
+lemma mult_sum_group [simp]: "(\<otimes>\<^bsub>sum_group I G\<^esub>) = (\<lambda>x y. (\<lambda>i\<in>I. x i \<otimes>\<^bsub>G i\<^esub> y i))"
+  by (auto simp: sum_group_def)
+
+lemma sum_group [simp]:
+  assumes "\<And>i. i \<in> I \<Longrightarrow> group (G i)" shows "group (sum_group I G)"
+proof (rule groupI)
+  note group.is_monoid [OF assms, simp]
+  show "x \<otimes>\<^bsub>sum_group I G\<^esub> y \<in> carrier (sum_group I G)"
+    if "x \<in> carrier (sum_group I G)" and
+      "y \<in> carrier (sum_group I G)" for x y
+  proof -
+    have *: "{i \<in> I. x i \<otimes>\<^bsub>G i\<^esub> y i \<noteq> \<one>\<^bsub>G i\<^esub>} \<subseteq> {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>} \<union> {i \<in> I. y i \<noteq> \<one>\<^bsub>G i\<^esub>}"
+      by auto
+    show ?thesis
+      using that
+      apply (simp add: assms carrier_sum_group PiE_iff monoid.m_closed conj_commute cong: rev_conj_cong)
+      apply (blast intro: finite_subset [OF *])
+      done
+  qed
+  show "\<one>\<^bsub>sum_group I G\<^esub> \<otimes>\<^bsub>sum_group I G\<^esub> x = x"
+    if "x \<in> carrier (sum_group I G)" for x
+    using that by (auto simp: assms carrier_sum_group PiE_iff extensional_def)
+  show "\<exists>y\<in>carrier (sum_group I G). y \<otimes>\<^bsub>sum_group I G\<^esub> x = \<one>\<^bsub>sum_group I G\<^esub>"
+    if "x \<in> carrier (sum_group I G)" for x
+  proof
+    let ?y = "\<lambda>i\<in>I. m_inv (G i) (x i)"
+    show "?y \<otimes>\<^bsub>sum_group I G\<^esub> x = \<one>\<^bsub>sum_group I G\<^esub>"
+      using that assms
+      by (auto simp: carrier_sum_group PiE_iff group.l_inv)
+    show "?y \<in> carrier (sum_group I G)"
+      using that assms
+      by (auto simp: carrier_sum_group PiE_iff group.inv_eq_1_iff group.l_inv cong: conj_cong)
+  qed
+qed (auto simp: assms carrier_sum_group PiE_iff group.is_monoid monoid.m_assoc)
+
+lemma inv_sum_group [simp]:
+  assumes "\<And>i. i \<in> I \<Longrightarrow> group (G i)" and x: "x \<in> carrier (sum_group I G)"
+  shows "m_inv (sum_group I G) x = (\<lambda>i\<in>I. m_inv (G i) (x i))"
+proof (rule group.inv_equality)
+  show "(\<lambda>i\<in>I. inv\<^bsub>G i\<^esub> x i) \<otimes>\<^bsub>sum_group I G\<^esub> x = \<one>\<^bsub>sum_group I G\<^esub>"
+    using x by (auto simp: carrier_sum_group PiE_iff group.l_inv assms intro: restrict_ext)
+  show "(\<lambda>i\<in>I. inv\<^bsub>G i\<^esub> x i) \<in> carrier (sum_group I G)"
+    using x by (simp add: carrier_sum_group PiE_iff group.inv_eq_1_iff assms conj_commute cong: rev_conj_cong)
+qed (auto simp: assms)
+
+
+thm group.subgroups_Inter (*REPLACE*)
+theorem subgroup_Inter:
+  assumes subgr: "(\<And>H. H \<in> A \<Longrightarrow> subgroup H G)"
+    and not_empty: "A \<noteq> {}"
+  shows "subgroup (\<Inter>A) G"
+proof
+  show "\<Inter> A \<subseteq> carrier G"
+    by (simp add: Inf_less_eq not_empty subgr subgroup.subset)
+qed (auto simp: subgr subgroup.m_closed subgroup.one_closed subgroup.m_inv_closed)
+
+thm group.subgroups_Inter_pair (*REPLACE*)
+lemma subgroup_Int:
+  assumes "subgroup I G" "subgroup J G"
+  shows "subgroup (I \<inter> J) G" using subgroup_Inter[ where ?A = "{I,J}"] assms by auto
+
+
+lemma sum_group_subgroup_generated:
+  assumes "\<And>i. i \<in> I \<Longrightarrow> group (G i)" and sg: "\<And>i. i \<in> I \<Longrightarrow> subgroup (H i) (G i)"
+  shows "sum_group I (\<lambda>i. subgroup_generated (G i) (H i)) = subgroup_generated (sum_group I G) (PiE I H)"
+proof (rule monoid.equality)
+  have "subgroup (carrier (sum_group I G) \<inter> Pi\<^sub>E I H) (product_group I G)"
+    by (rule subgroup_Int) (auto simp: assms carrier_sum_group subgroup_sum_group PiE_subgroup_product_group)
+  moreover have "carrier (sum_group I G) \<inter> Pi\<^sub>E I H
+              \<subseteq> carrier (subgroup_generated (product_group I G)
+                    {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}})"
+    by (simp add: assms subgroup_sum_group subgroup.carrier_subgroup_generated_subgroup carrier_sum_group)
+  ultimately
+  have "subgroup (carrier (sum_group I G) \<inter> Pi\<^sub>E I H) (sum_group I G)"
+    by (simp add: assms sum_group_def group.subgroup_subgroup_generated_iff)
+  then have *: "{f \<in> \<Pi>\<^sub>E i\<in>I. carrier (subgroup_generated (G i) (H i)). finite {i \<in> I. f i \<noteq> \<one>\<^bsub>G i\<^esub>}}
+      = carrier (subgroup_generated (sum_group I G) (carrier (sum_group I G) \<inter> Pi\<^sub>E I H))"
+    apply (simp only: subgroup.carrier_subgroup_generated_subgroup)
+    using subgroup.subset [OF sg]
+    apply (auto simp: set_eq_iff PiE_def Pi_def assms carrier_sum_group subgroup.carrier_subgroup_generated_subgroup)
+    done
+  then show "carrier (sum_group I (\<lambda>i. subgroup_generated (G i) (H i))) =
+        carrier (subgroup_generated (sum_group I G) (Pi\<^sub>E I H))"
+    by simp (simp add: assms group.subgroupE(1) group.group_subgroup_generated carrier_sum_group)
+qed (auto simp: sum_group_def subgroup_generated_def)
+
+
+lemma iso_product_groupI:
+  assumes iso: "\<And>i. i \<in> I \<Longrightarrow> G i \<cong> H i"
+    and G: "\<And>i. i \<in> I \<Longrightarrow> group (G i)" and H: "\<And>i. i \<in> I \<Longrightarrow> group (H i)"
+  shows "product_group I G \<cong> product_group I H" (is "?IG \<cong> ?IH")
+proof -
+  have "\<And>i. i \<in> I \<Longrightarrow> \<exists>h. h \<in> iso (G i) (H i)"
+    using iso by (auto simp: is_iso_def)
+  then obtain f where f: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> iso (G i) (H i)"
+    by metis
+  define h where "h \<equiv> \<lambda>x. (\<lambda>i\<in>I. f i (x i))"
+  have hom: "h \<in> iso ?IG ?IH"
+  proof (rule isoI)
+    show hom: "h \<in> hom ?IG ?IH"
+    proof (rule homI)
+      fix x
+      assume "x \<in> carrier ?IG"
+      with f show "h x \<in> carrier ?IH"
+        using PiE by (fastforce simp add: h_def PiE_def iso_def hom_def)
+    next
+      fix x y
+      assume "x \<in> carrier ?IG" "y \<in> carrier ?IG"
+      with f show "h (x \<otimes>\<^bsub>?IG\<^esub> y) = h x \<otimes>\<^bsub>?IH\<^esub> h y"
+        apply (simp add: h_def PiE_def iso_def hom_def)
+        using PiE by (fastforce simp add: h_def PiE_def iso_def hom_def intro: restrict_ext)
+    qed
+    with G H interpret GH : group_hom "?IG" "?IH" h
+      by (simp add: group_hom_def group_hom_axioms_def)
+    show "bij_betw h (carrier ?IG) (carrier ?IH)"
+      unfolding bij_betw_def
+    proof (intro conjI subset_antisym)
+      have "\<gamma> i = \<one>\<^bsub>G i\<^esub>"
+        if \<gamma>: "\<gamma> \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" and eq: "(\<lambda>i\<in>I. f i (\<gamma> i)) = (\<lambda>i\<in>I. \<one>\<^bsub>H i\<^esub>)" and "i \<in> I"
+        for \<gamma> i
+      proof -
+        have "inj_on (f i) (carrier (G i))" "f i \<in> hom (G i) (H i)"
+          using \<open>i \<in> I\<close> f by (auto simp: iso_def bij_betw_def)
+        then have *: "\<And>x. \<lbrakk>f i x = \<one>\<^bsub>H i\<^esub>; x \<in> carrier (G i)\<rbrakk> \<Longrightarrow> x = \<one>\<^bsub>G i\<^esub>"
+          by (metis G Group.group_def H hom_one inj_onD monoid.one_closed \<open>i \<in> I\<close>)
+        show ?thesis
+          using eq \<open>i \<in> I\<close> * \<gamma> by (simp add: fun_eq_iff) (meson PiE_iff)
+      qed
+      then show "inj_on h (carrier ?IG)"
+        apply (simp add: iso_def bij_betw_def GH.inj_on_one_iff flip: carrier_product_group)
+        apply (force simp: h_def)
+        done
+    next
+      show "h ` carrier ?IG \<subseteq> carrier ?IH"
+        unfolding h_def using f
+        by (force simp: PiE_def Pi_def Group.iso_def dest!: bij_betwE)
+    next
+      show "carrier ?IH \<subseteq> h ` carrier ?IG"
+        unfolding h_def
+      proof (clarsimp simp: iso_def bij_betw_def)
+        fix x
+        assume "x \<in> (\<Pi>\<^sub>E i\<in>I. carrier (H i))"
+        with f have x: "x \<in> (\<Pi>\<^sub>E i\<in>I. f i ` carrier (G i))"
+          unfolding h_def by (auto simp: iso_def bij_betw_def)
+        have "\<And>i. i \<in> I \<Longrightarrow> inj_on (f i) (carrier (G i))"
+          using f by (auto simp: iso_def bij_betw_def)
+        let ?g = "\<lambda>i\<in>I. inv_into (carrier (G i)) (f i) (x i)"
+        show "x \<in> (\<lambda>g. \<lambda>i\<in>I. f i (g i)) ` (\<Pi>\<^sub>E i\<in>I. carrier (G i))"
+        proof
+          show "x = (\<lambda>i\<in>I. f i (?g i))"
+            using x by (auto simp: PiE_iff fun_eq_iff extensional_def f_inv_into_f)
+          show "?g \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))"
+            using x by (auto simp: PiE_iff inv_into_into)
+        qed
+      qed
+    qed
+  qed
+  then show ?thesis
+    using is_iso_def by auto
+qed
+
+lemma iso_sum_groupI:
+  assumes iso: "\<And>i. i \<in> I \<Longrightarrow> G i \<cong> H i"
+    and G: "\<And>i. i \<in> I \<Longrightarrow> group (G i)" and H: "\<And>i. i \<in> I \<Longrightarrow> group (H i)"
+  shows "sum_group I G \<cong> sum_group I H" (is "?IG \<cong> ?IH")
+proof -
+  have "\<And>i. i \<in> I \<Longrightarrow> \<exists>h. h \<in> iso (G i) (H i)"
+    using iso by (auto simp: is_iso_def)
+  then obtain f where f: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> iso (G i) (H i)"
+    by metis
+  then have injf: "inj_on (f i) (carrier (G i))"
+    and homf: "f i \<in> hom (G i) (H i)" if "i \<in> I" for i
+    using \<open>i \<in> I\<close> f by (auto simp: iso_def bij_betw_def)
+  then have one: "\<And>x. \<lbrakk>f i x = \<one>\<^bsub>H i\<^esub>; x \<in> carrier (G i)\<rbrakk> \<Longrightarrow> x = \<one>\<^bsub>G i\<^esub>" if "i \<in> I" for i
+    by (metis G H group.subgroup_self hom_one inj_on_eq_iff subgroup.one_closed that)
+  have fin1: "finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>} \<Longrightarrow> finite {i \<in> I. f i (x i) \<noteq> \<one>\<^bsub>H i\<^esub>}" for x
+    using homf by (auto simp: G H hom_one elim!: rev_finite_subset)
+  define h where "h \<equiv> \<lambda>x. (\<lambda>i\<in>I. f i (x i))"
+  have hom: "h \<in> iso ?IG ?IH"
+  proof (rule isoI)
+    show hom: "h \<in> hom ?IG ?IH"
+    proof (rule homI)
+      fix x
+      assume "x \<in> carrier ?IG"
+      with f fin1 show "h x \<in> carrier ?IH"
+        by (force simp: h_def PiE_def iso_def hom_def carrier_sum_group assms conj_commute cong: conj_cong)
+    next
+      fix x y
+      assume "x \<in> carrier ?IG" "y \<in> carrier ?IG"
+      with homf show "h (x \<otimes>\<^bsub>?IG\<^esub> y) = h x \<otimes>\<^bsub>?IH\<^esub> h y"
+        by (fastforce simp add: h_def PiE_def hom_def carrier_sum_group assms intro: restrict_ext)
+    qed
+    with G H interpret GH : group_hom "?IG" "?IH" h
+      by (simp add: group_hom_def group_hom_axioms_def)
+    show "bij_betw h (carrier ?IG) (carrier ?IH)"
+      unfolding bij_betw_def
+    proof (intro conjI subset_antisym)
+      have \<gamma>: "\<gamma> i = \<one>\<^bsub>G i\<^esub>"
+        if "\<gamma> \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" and eq: "(\<lambda>i\<in>I. f i (\<gamma> i)) = (\<lambda>i\<in>I. \<one>\<^bsub>H i\<^esub>)" and "i \<in> I"
+        for \<gamma> i
+        using \<open>i \<in> I\<close> one that by (simp add: fun_eq_iff) (meson PiE_iff)
+      show "inj_on h (carrier ?IG)"
+        apply (simp add: iso_def bij_betw_def GH.inj_on_one_iff assms one flip: carrier_sum_group)
+        apply (auto simp: h_def fun_eq_iff carrier_sum_group assms PiE_def Pi_def extensional_def one)
+        done
+    next
+      show "h ` carrier ?IG \<subseteq> carrier ?IH"
+        using homf GH.hom_closed
+        by (fastforce simp: h_def PiE_def Pi_def dest!: bij_betwE)
+    next
+      show "carrier ?IH \<subseteq> h ` carrier ?IG"
+        unfolding h_def
+      proof (clarsimp simp: iso_def bij_betw_def carrier_sum_group assms)
+        fix x
+        assume x: "x \<in> (\<Pi>\<^sub>E i\<in>I. carrier (H i))" and fin: "finite {i \<in> I. x i \<noteq> \<one>\<^bsub>H i\<^esub>}"
+        with f have xf: "x \<in> (\<Pi>\<^sub>E i\<in>I. f i ` carrier (G i))"
+          unfolding h_def
+          by (auto simp: iso_def bij_betw_def)
+        have "\<And>i. i \<in> I \<Longrightarrow> inj_on (f i) (carrier (G i))"
+          using f by (auto simp: iso_def bij_betw_def)
+        let ?g = "\<lambda>i\<in>I. inv_into (carrier (G i)) (f i) (x i)"
+        show "x \<in> (\<lambda>g. \<lambda>i\<in>I. f i (g i))
+                 ` {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}"
+        proof
+          show xeq: "x = (\<lambda>i\<in>I. f i (?g i))"
+            using x by (clarsimp simp: PiE_iff fun_eq_iff extensional_def) (metis iso_iff f_inv_into_f f)
+          have "finite {i \<in> I. inv_into (carrier (G i)) (f i) (x i) \<noteq> \<one>\<^bsub>G i\<^esub>}"
+            apply (rule finite_subset [OF _ fin])
+            using G H group.subgroup_self hom_one homf injf inv_into_f_eq subgroup.one_closed by fastforce
+          with x show "?g \<in> {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}"
+            apply (auto simp: PiE_iff inv_into_into conj_commute cong: conj_cong)
+            by (metis (no_types, hide_lams) iso_iff f inv_into_into)
+        qed
+      qed
+    qed
+  qed
+  then show ?thesis
+    using is_iso_def by auto
+qed
+
+end
--- a/src/HOL/Analysis/Abstract_Topology.thy	Thu Apr 04 22:18:32 2019 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Thu Apr 04 22:21:09 2019 +0200
@@ -4063,7 +4063,7 @@
   "openin (topology_generated_by S) s \<Longrightarrow> generate_topology_on S s"
 using openin_topology_generated_by_iff by auto
 
-lemma topology_generated_by_topspace:
+lemma topology_generated_by_topspace [simp]:
   "topspace (topology_generated_by S) = (\<Union>S)"
 proof
   {
--- a/src/HOL/Analysis/Elementary_Topology.thy	Thu Apr 04 22:18:32 2019 +0200
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Thu Apr 04 22:21:09 2019 +0200
@@ -1459,25 +1459,6 @@
   qed
 qed
 
-text\<open>Deducing things about the limit from the elements.\<close>
-
-lemma Lim_in_closed_set:
-  assumes "closed S"
-    and "eventually (\<lambda>x. f(x) \<in> S) net"
-    and "\<not> trivial_limit net" "(f \<longlongrightarrow> l) net"
-  shows "l \<in> S"
-proof (rule ccontr)
-  assume "l \<notin> S"
-  with \<open>closed S\<close> have "open (- S)" "l \<in> - S"
-    by (simp_all add: open_Compl)
-  with assms(4) have "eventually (\<lambda>x. f x \<in> - S) net"
-    by (rule topological_tendstoD)
-  with assms(2) have "eventually (\<lambda>x. False) net"
-    by (rule eventually_elim2) simp
-  with assms(3) show "False"
-    by (simp add: eventually_False)
-qed
-
 text\<open>These are special for limits out of the same topological space.\<close>
 
 lemma Lim_within_id: "(id \<longlongrightarrow> a) (at a within s)"
--- a/src/HOL/Groups_Big.thy	Thu Apr 04 22:18:32 2019 +0200
+++ b/src/HOL/Groups_Big.thy	Thu Apr 04 22:21:09 2019 +0200
@@ -16,6 +16,8 @@
 locale comm_monoid_set = comm_monoid
 begin
 
+subsubsection \<open>Standard sum or product indexed by a finite set\<close>
+
 interpretation comp_fun_commute f
   by standard (simp add: fun_eq_iff left_commute)
 
@@ -523,6 +525,92 @@
   shows "F \<phi> A = F \<gamma> B"
   by (rule eq_general [where h=h]) (force intro: dest: A B)+
 
+subsubsection \<open>HOL Light variant: sum/product indexed by the non-neutral subset\<close>
+text \<open>NB only a subset of the properties above are proved\<close>
+
+definition G :: "['b \<Rightarrow> 'a,'b set] \<Rightarrow> 'a"
+  where "G p I \<equiv> if finite {x \<in> I. p x \<noteq> \<^bold>1} then F p {x \<in> I. p x \<noteq> \<^bold>1} else \<^bold>1"
+
+lemma finite_Collect_op:
+  shows "\<lbrakk>finite {i \<in> I. x i \<noteq> \<^bold>1}; finite {i \<in> I. y i \<noteq> \<^bold>1}\<rbrakk> \<Longrightarrow> finite {i \<in> I. x i \<^bold>* y i \<noteq> \<^bold>1}"
+  apply (rule finite_subset [where B = "{i \<in> I. x i \<noteq> \<^bold>1} \<union> {i \<in> I. y i \<noteq> \<^bold>1}"]) 
+  using left_neutral by force+
+
+lemma empty' [simp]: "G p {} = \<^bold>1"
+  by (auto simp: G_def)
+
+lemma eq_sum [simp]: "finite I \<Longrightarrow> G p I = F p I"
+  by (auto simp: G_def intro: mono_neutral_cong_left)
+
+lemma insert' [simp]:
+  assumes "finite {x \<in> I. p x \<noteq> \<^bold>1}"
+  shows "G p (insert i I) = (if i \<in> I then G p I else p i \<^bold>* G p I)"
+proof -
+  have "{x. x = i \<and> p x \<noteq> \<^bold>1 \<or> x \<in> I \<and> p x \<noteq> \<^bold>1} = (if p i = \<^bold>1 then {x \<in> I. p x \<noteq> \<^bold>1} else insert i {x \<in> I. p x \<noteq> \<^bold>1})"
+    by auto
+  then show ?thesis
+    using assms by (simp add: G_def conj_disj_distribR insert_absorb)
+qed
+
+lemma distrib_triv':
+  assumes "finite I"
+  shows "G (\<lambda>i. g i \<^bold>* h i) I = G g I \<^bold>* G h I"
+  by (simp add: assms local.distrib)
+
+lemma non_neutral': "G g {x \<in> I. g x \<noteq> \<^bold>1} = G g I"
+  by (simp add: G_def)
+
+lemma distrib':
+  assumes "finite {x \<in> I. g x \<noteq> \<^bold>1}" "finite {x \<in> I. h x \<noteq> \<^bold>1}"
+  shows "G (\<lambda>i. g i \<^bold>* h i) I = G g I \<^bold>* G h I"
+proof -
+  have "a \<^bold>* a \<noteq> a \<Longrightarrow> a \<noteq> \<^bold>1" for a
+    by auto
+  then have "G (\<lambda>i. g i \<^bold>* h i) I = G (\<lambda>i. g i \<^bold>* h i) ({i \<in> I. g i \<noteq> \<^bold>1} \<union> {i \<in> I. h i \<noteq> \<^bold>1})"
+    using assms  by (force simp: G_def finite_Collect_op intro!: mono_neutral_cong)
+  also have "\<dots> = G g I \<^bold>* G h I"
+  proof -
+    have "F g ({i \<in> I. g i \<noteq> \<^bold>1} \<union> {i \<in> I. h i \<noteq> \<^bold>1}) = G g I"
+         "F h ({i \<in> I. g i \<noteq> \<^bold>1} \<union> {i \<in> I. h i \<noteq> \<^bold>1}) = G h I"
+      by (auto simp: G_def assms intro: mono_neutral_right)
+    then show ?thesis
+      using assms by (simp add: distrib)
+  qed
+  finally show ?thesis .
+qed
+
+lemma cong':
+  assumes "A = B"
+  assumes g_h: "\<And>x. x \<in> B \<Longrightarrow> g x = h x"
+  shows "G g A = G h B"
+  using assms by (auto simp: G_def cong: conj_cong intro: cong)
+
+
+lemma mono_neutral_cong_left':
+  assumes "S \<subseteq> T"
+    and "\<And>i. i \<in> T - S \<Longrightarrow> h i = \<^bold>1"
+    and "\<And>x. x \<in> S \<Longrightarrow> g x = h x"
+  shows "G g S = G h T"
+proof -
+  have *: "{x \<in> S. g x \<noteq> \<^bold>1} = {x \<in> T. h x \<noteq> \<^bold>1}"
+    using assms by (metis DiffI subset_eq) 
+  then have "finite {x \<in> S. g x \<noteq> \<^bold>1} = finite {x \<in> T. h x \<noteq> \<^bold>1}"
+    by simp
+  then show ?thesis
+    using assms by (auto simp add: G_def * intro: cong)
+qed
+
+lemma mono_neutral_cong_right':
+  "S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. g i = \<^bold>1 \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> g x = h x) \<Longrightarrow>
+    G g T = G h S"
+  by (auto intro!: mono_neutral_cong_left' [symmetric])
+
+lemma mono_neutral_left': "S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. g i = \<^bold>1 \<Longrightarrow> G g S = G g T"
+  by (blast intro: mono_neutral_cong_left')
+
+lemma mono_neutral_right': "S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. g i = \<^bold>1 \<Longrightarrow> G g T = G g S"
+  by (blast intro!: mono_neutral_left' [symmetric])
+
 end
 
 
@@ -532,7 +620,7 @@
 begin
 
 sublocale sum: comm_monoid_set plus 0
-  defines sum = sum.F ..
+  defines sum = sum.F and sum' = sum.G ..
 
 abbreviation Sum ("\<Sum>")
   where "\<Sum> \<equiv> sum (\<lambda>x. x)"
@@ -615,6 +703,31 @@
   qed
 qed
 
+lemma sum_diff1'_aux:
+  fixes f :: "'a \<Rightarrow> 'b::ab_group_add"
+  assumes "finite F" "{i \<in> I. f i \<noteq> 0} \<subseteq> F"
+  shows "sum' f (I - {i}) = (if i \<in> I then sum' f I - f i else sum' f I)"
+  using assms
+proof induct
+  case (insert x F)
+  have 1: "finite {x \<in> I. f x \<noteq> 0} \<Longrightarrow> finite {x \<in> I. x \<noteq> i \<and> f x \<noteq> 0}"
+    by (erule rev_finite_subset) auto
+  have 2: "finite {x \<in> I. x \<noteq> i \<and> f x \<noteq> 0} \<Longrightarrow> finite {x \<in> I. f x \<noteq> 0}"
+    apply (drule finite_insert [THEN iffD2])
+    by (erule rev_finite_subset) auto
+  have 3: "finite {i \<in> I. f i \<noteq> 0}"
+    using finite_subset insert by blast
+  show ?case
+    using insert sum_diff1 [of "{i \<in> I. f i \<noteq> 0}" f i]
+    by (auto simp: sum.G_def 1 2 3 set_diff_eq conj_ac)
+qed (simp add: sum.G_def)
+
+lemma sum_diff1':
+  fixes f :: "'a \<Rightarrow> 'b::ab_group_add"
+  assumes "finite {i \<in> I. f i \<noteq> 0}"
+  shows "sum' f (I - {i}) = (if i \<in> I then sum' f I - f i else sum' f I)"
+  by (rule sum_diff1'_aux [OF assms order_refl])
+
 lemma (in ordered_comm_monoid_add) sum_mono:
   "(\<And>i. i\<in>K \<Longrightarrow> f i \<le> g i) \<Longrightarrow> (\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
   by (induct K rule: infinite_finite_induct) (use add_mono in auto)
@@ -1134,7 +1247,7 @@
 begin
 
 sublocale prod: comm_monoid_set times 1
-  defines prod = prod.F ..
+  defines prod = prod.F and prod' = prod.G ..
 
 abbreviation Prod ("\<Prod>_" [1000] 999)
   where "\<Prod>A \<equiv> prod (\<lambda>x. x) A"
--- a/src/HOL/Library/Library.thy	Thu Apr 04 22:18:32 2019 +0200
+++ b/src/HOL/Library/Library.thy	Thu Apr 04 22:21:09 2019 +0200
@@ -64,6 +64,7 @@
   Perm
   Permutation
   Permutations
+  Poly_Mapping
   Power_By_Squaring
   Preorder
   Product_Plus
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Poly_Mapping.thy	Thu Apr 04 22:21:09 2019 +0200
@@ -0,0 +1,1878 @@
+(* Author: Andreas Lochbihler, ETH Zurich
+   Author: Florian Haftmann, TU Muenchen
+   with some material ported from HOL Light by LCP
+*)
+
+section \<open>Polynomial mapping: combination of almost everywhere zero functions with an algebraic view\<close>
+
+theory Poly_Mapping
+imports Groups_Big_Fun Fun_Lexorder More_List
+begin
+
+subsection \<open>Preliminary: auxiliary operations for \emph{almost everywhere zero}\<close>
+
+text \<open>
+  A central notion for polynomials are functions being \emph{almost everywhere zero}.
+  For these we provide some auxiliary definitions and lemmas.
+\<close>
+
+lemma finite_mult_not_eq_zero_leftI:
+  fixes f :: "'b \<Rightarrow> 'a :: mult_zero"
+  assumes "finite {a. f a \<noteq> 0}"
+  shows "finite {a. g a * f a \<noteq> 0}"
+proof -
+  have "{a. g a * f a \<noteq> 0} \<subseteq> {a. f a \<noteq> 0}" by auto
+  then show ?thesis using assms by (rule finite_subset)
+qed
+
+lemma finite_mult_not_eq_zero_rightI:
+  fixes f :: "'b \<Rightarrow> 'a :: mult_zero"
+  assumes "finite {a. f a \<noteq> 0}"
+  shows "finite {a. f a * g a \<noteq> 0}"
+proof -
+  have "{a. f a * g a \<noteq> 0} \<subseteq> {a. f a \<noteq> 0}" by auto
+  then show ?thesis using assms by (rule finite_subset)
+qed
+
+lemma finite_mult_not_eq_zero_prodI:
+  fixes f g :: "'a \<Rightarrow> 'b::semiring_0"
+  assumes "finite {a. f a \<noteq> 0}" (is "finite ?F")
+  assumes "finite {b. g b \<noteq> 0}" (is "finite ?G")
+  shows "finite {(a, b). f a * g b \<noteq> 0}"
+proof -
+  from assms have "finite (?F \<times> ?G)"
+    by blast
+  then have "finite {(a, b). f a \<noteq> 0 \<and> g b \<noteq> 0}"
+    by simp
+  then show ?thesis
+    by (rule rev_finite_subset) auto
+qed
+
+lemma finite_not_eq_zero_sumI:
+  fixes f g :: "'a::monoid_add \<Rightarrow> 'b::semiring_0"
+  assumes "finite {a. f a \<noteq> 0}" (is "finite ?F")
+  assumes "finite {b. g b \<noteq> 0}" (is "finite ?G")
+  shows "finite {a + b | a b. f a \<noteq> 0 \<and> g b \<noteq> 0}" (is "finite ?FG")
+proof -
+  from assms have "finite (?F \<times> ?G)"
+    by (simp add: finite_cartesian_product_iff)
+  then have "finite (case_prod plus ` (?F \<times> ?G))"
+    by (rule finite_imageI)
+  also have "case_prod plus ` (?F \<times> ?G) = ?FG"
+    by auto
+  finally show ?thesis
+    by simp
+qed
+
+lemma finite_mult_not_eq_zero_sumI:
+  fixes f g :: "'a::monoid_add \<Rightarrow> 'b::semiring_0"
+  assumes "finite {a. f a \<noteq> 0}"
+  assumes "finite {b. g b \<noteq> 0}"
+  shows "finite {a + b | a b. f a * g b \<noteq> 0}"
+proof -
+  from assms
+  have "finite {a + b | a b. f a \<noteq> 0 \<and> g b \<noteq> 0}"
+    by (rule finite_not_eq_zero_sumI)
+  then show ?thesis
+    by (rule rev_finite_subset) (auto dest: mult_not_zero)
+qed
+
+lemma finite_Sum_any_not_eq_zero_weakenI:
+  assumes "finite {a. \<exists>b. f a b \<noteq> 0}"
+  shows "finite {a. Sum_any (f a) \<noteq> 0}"
+proof -
+  have "{a. Sum_any (f a) \<noteq> 0} \<subseteq> {a. \<exists>b. f a b \<noteq> 0}"
+    by (auto elim: Sum_any.not_neutral_obtains_not_neutral)
+  then show ?thesis using assms by (rule finite_subset)
+qed
+
+context zero
+begin
+
+definition "when" :: "'a \<Rightarrow> bool \<Rightarrow> 'a" (infixl "when" 20)
+where
+  "(a when P) = (if P then a else 0)"
+
+text \<open>
+  Case distinctions always complicate matters, particularly when
+  nested.  The @{const "when"} operation allows to minimise these
+  if @{term 0} is the false-case value and makes proof obligations
+  much more readable.
+\<close>
+
+lemma "when" [simp]:
+  "P \<Longrightarrow> (a when P) = a"
+  "\<not> P \<Longrightarrow> (a when P) = 0"
+  by (simp_all add: when_def)
+
+lemma when_simps [simp]:
+  "(a when True) = a"
+  "(a when False) = 0"
+  by simp_all
+
+lemma when_cong:
+  assumes "P \<longleftrightarrow> Q"
+    and "Q \<Longrightarrow> a = b"
+  shows "(a when P) = (b when Q)"
+  using assms by (simp add: when_def)
+
+lemma zero_when [simp]:
+  "(0 when P) = 0"
+  by (simp add: when_def)
+
+lemma when_when:
+  "(a when P when Q) = (a when P \<and> Q)"
+  by (cases Q) simp_all
+
+lemma when_commute:
+  "(a when Q when P) = (a when P when Q)"
+  by (simp add: when_when conj_commute)
+
+lemma when_neq_zero [simp]:
+  "(a when P) \<noteq> 0 \<longleftrightarrow> P \<and> a \<noteq> 0"
+  by (cases P) simp_all
+
+end
+
+context monoid_add
+begin
+
+lemma when_add_distrib:
+  "(a + b when P) = (a when P) + (b when P)"
+  by (simp add: when_def)
+
+end
+
+context semiring_1
+begin
+
+lemma zero_power_eq:
+  "0 ^ n = (1 when n = 0)"
+  by (simp add: power_0_left)
+
+end
+
+context comm_monoid_add
+begin
+
+lemma Sum_any_when_equal [simp]:
+  "(\<Sum>a. (f a when a = b)) = f b"
+  by (simp add: when_def)
+
+lemma Sum_any_when_equal' [simp]:
+  "(\<Sum>a. (f a when b = a)) = f b"
+  by (simp add: when_def)
+
+lemma Sum_any_when_independent:
+  "(\<Sum>a. g a when P) = ((\<Sum>a. g a) when P)"
+  by (cases P) simp_all
+
+lemma Sum_any_when_dependent_prod_right:
+  "(\<Sum>(a, b). g a when b = h a) = (\<Sum>a. g a)"
+proof -
+  have "inj_on (\<lambda>a. (a, h a)) {a. g a \<noteq> 0}"
+    by (rule inj_onI) auto
+  then show ?thesis unfolding Sum_any.expand_set
+    by (rule sum.reindex_cong) auto
+qed
+
+lemma Sum_any_when_dependent_prod_left:
+  "(\<Sum>(a, b). g b when a = h b) = (\<Sum>b. g b)"
+proof -
+  have "(\<Sum>(a, b). g b when a = h b) = (\<Sum>(b, a). g b when a = h b)"
+    by (rule Sum_any.reindex_cong [of prod.swap]) (simp_all add: fun_eq_iff)
+  then show ?thesis by (simp add: Sum_any_when_dependent_prod_right)
+qed
+
+end
+
+context cancel_comm_monoid_add
+begin
+
+lemma when_diff_distrib:
+  "(a - b when P) = (a when P) - (b when P)"
+  by (simp add: when_def)
+
+end
+
+context group_add
+begin
+
+lemma when_uminus_distrib:
+  "(- a when P) = - (a when P)"
+  by (simp add: when_def)
+
+end
+
+context mult_zero
+begin
+
+lemma mult_when:
+  "a * (b when P) = (a * b when P)"
+  by (cases P) simp_all
+
+lemma when_mult:
+  "(a when P) * b = (a * b when P)"
+  by (cases P) simp_all
+
+end
+
+
+subsection \<open>Type definition\<close>
+
+text \<open>
+  The following type is of central importance:
+\<close>
+
+typedef (overloaded) ('a, 'b) poly_mapping ("(_ \<Rightarrow>\<^sub>0 /_)" [1, 0] 0) =
+  "{f :: 'a \<Rightarrow> 'b::zero. finite {x. f x \<noteq> 0}}"
+  morphisms lookup Abs_poly_mapping
+proof -
+  have "(\<lambda>_::'a. (0 :: 'b)) \<in> ?poly_mapping" by simp
+  then show ?thesis by (blast intro!: exI)
+qed
+
+declare lookup_inverse [simp]
+declare lookup_inject [simp]
+
+lemma lookup_Abs_poly_mapping [simp]:
+  "finite {x. f x \<noteq> 0} \<Longrightarrow> lookup (Abs_poly_mapping f) = f"
+  using Abs_poly_mapping_inverse [of f] by simp
+
+lemma finite_lookup [simp]:
+  "finite {k. lookup f k \<noteq> 0}"
+  using poly_mapping.lookup [of f] by simp
+
+lemma finite_lookup_nat [simp]:
+  fixes f :: "'a \<Rightarrow>\<^sub>0 nat"
+  shows "finite {k. 0 < lookup f k}"
+  using poly_mapping.lookup [of f] by simp
+
+lemma poly_mapping_eqI:
+  assumes "\<And>k. lookup f k = lookup g k"
+  shows "f = g"
+  using assms unfolding poly_mapping.lookup_inject [symmetric]
+  by blast
+
+lemma poly_mapping_eq_iff: "a = b \<longleftrightarrow> lookup a = lookup b"
+  by auto
+
+text \<open>
+  We model the universe of functions being \emph{almost everywhere zero}
+  by means of a separate type @{typ "('a, 'b) poly_mapping"}.
+  For convenience we provide a suggestive infix syntax which
+  is a variant of the usual function space syntax.  Conversion between both types
+  happens through the morphisms
+  \begin{quote}
+    @{term_type lookup}
+  \end{quote}
+  \begin{quote}
+    @{term_type Abs_poly_mapping}
+  \end{quote}
+  satisfying
+  \begin{quote}
+    @{thm lookup_inverse}
+  \end{quote}
+  \begin{quote}
+    @{thm lookup_Abs_poly_mapping}
+  \end{quote}
+  Luckily, we have rarely to deal with those low-level morphisms explicitly
+  but rely on Isabelle's \emph{lifting} package with its method \<open>transfer\<close>
+  and its specification tool \<open>lift_definition\<close>.
+\<close>
+
+setup_lifting type_definition_poly_mapping
+code_datatype Abs_poly_mapping\<comment>\<open>FIXME? workaround for preventing \<open>code_abstype\<close> setup\<close>
+
+text \<open>
+  @{typ "'a \<Rightarrow>\<^sub>0 'b"} serves distinctive purposes:
+  \begin{enumerate}
+    \item A clever nesting as @{typ "(nat \<Rightarrow>\<^sub>0 nat) \<Rightarrow>\<^sub>0 'a"}
+      later in theory \<open>MPoly\<close> gives a suitable
+      representation type for polynomials \emph{almost for free}:
+      Interpreting @{typ "nat \<Rightarrow>\<^sub>0 nat"} as a mapping from variable identifiers
+      to exponents yields monomials, and the whole type maps monomials
+      to coefficients.  Lets call this the \emph{ultimate interpretation}.
+    \item A further more specialised type isomorphic to @{typ "nat \<Rightarrow>\<^sub>0 'a"}
+      is apt to direct implementation using code generation
+      \cite{Haftmann-Nipkow:2010:code}.
+  \end{enumerate}
+  Note that despite the names \emph{mapping} and \emph{lookup} suggest something
+  implementation-near, it is best to keep @{typ "'a \<Rightarrow>\<^sub>0 'b"} as an abstract
+  \emph{algebraic} type
+  providing operations like \emph{addition}, \emph{multiplication} without any notion
+  of key-order, data structures etc.  This implementations-specific notions are
+  easily introduced later for particular implementations but do not provide any
+  gain for specifying logical properties of polynomials.
+\<close>
+
+subsection \<open>Additive structure\<close>
+
+text \<open>
+  The additive structure covers the usual operations \<open>0\<close>, \<open>+\<close> and
+  (unary and binary) \<open>-\<close>.  Recalling the ultimate interpretation, it
+  is obvious that these have just lift the corresponding operations on values
+  to mappings.
+
+  Isabelle has a rich hierarchy of algebraic type classes, and in such situations
+  of pointwise lifting a typical pattern is to have instantiations for a considerable
+  number of type classes.
+
+  The operations themselves are specified using \<open>lift_definition\<close>, where
+  the proofs of the \emph{almost everywhere zero} property can be significantly involved.
+
+  The @{const lookup} operation is supposed to be usable explicitly (unless in
+  other situations where the morphisms between types are somehow internal
+  to the \emph{lifting} package).  Hence it is good style to provide explicit rewrite
+  rules how @{const lookup} acts on operations immediately.
+\<close>
+
+instantiation poly_mapping :: (type, zero) zero
+begin
+
+lift_definition zero_poly_mapping :: "'a \<Rightarrow>\<^sub>0 'b"
+  is "\<lambda>k. 0"
+  by simp
+
+instance ..
+
+end
+
+lemma Abs_poly_mapping [simp]: "Abs_poly_mapping (\<lambda>k. 0) = 0"
+  by (simp add: zero_poly_mapping.abs_eq)
+
+lemma lookup_zero [simp]: "lookup 0 k = 0"
+  by transfer rule
+
+instantiation poly_mapping :: (type, monoid_add) monoid_add
+begin
+
+lift_definition plus_poly_mapping ::
+    "('a \<Rightarrow>\<^sub>0 'b) \<Rightarrow> ('a \<Rightarrow>\<^sub>0 'b) \<Rightarrow> 'a \<Rightarrow>\<^sub>0 'b"
+  is "\<lambda>f1 f2 k. f1 k + f2 k"
+proof -
+  fix f1 f2 :: "'a \<Rightarrow> 'b"
+  assume "finite {k. f1 k \<noteq> 0}"
+    and "finite {k. f2 k \<noteq> 0}"
+  then have "finite ({k. f1 k \<noteq> 0} \<union> {k. f2 k \<noteq> 0})" by auto
+  moreover have "{x. f1 x + f2 x \<noteq> 0} \<subseteq> {k. f1 k \<noteq> 0} \<union> {k. f2 k \<noteq> 0}"
+    by auto
+  ultimately show "finite {x. f1 x + f2 x \<noteq> 0}"
+    by (blast intro: finite_subset)
+qed
+
+instance
+  by intro_classes (transfer, simp add: fun_eq_iff ac_simps)+
+
+end
+
+lemma lookup_add:
+  "lookup (f + g) k = lookup f k + lookup g k"
+  by transfer rule
+
+instance poly_mapping :: (type, comm_monoid_add) comm_monoid_add
+  by intro_classes (transfer, simp add: fun_eq_iff ac_simps)+
+
+lemma lookup_sum: "lookup (sum pp X) i = sum (\<lambda>x. lookup (pp x) i) X"
+  by (induction rule: infinite_finite_induct) (auto simp: lookup_add)
+
+(*instance poly_mapping :: (type, "{monoid_add, cancel_semigroup_add}") cancel_semigroup_add
+  by intro_classes (transfer, simp add: fun_eq_iff)+*)
+
+instantiation poly_mapping :: (type, cancel_comm_monoid_add) cancel_comm_monoid_add
+begin
+
+lift_definition minus_poly_mapping :: "('a \<Rightarrow>\<^sub>0 'b) \<Rightarrow> ('a \<Rightarrow>\<^sub>0 'b) \<Rightarrow> 'a \<Rightarrow>\<^sub>0 'b"
+  is "\<lambda>f1 f2 k. f1 k - f2 k"
+proof -
+  fix f1 f2 :: "'a \<Rightarrow> 'b"
+  assume "finite {k. f1 k \<noteq> 0}"
+    and "finite {k. f2 k \<noteq> 0}"
+  then have "finite ({k. f1 k \<noteq> 0} \<union> {k. f2 k \<noteq> 0})" by auto
+  moreover have "{x. f1 x - f2 x \<noteq> 0} \<subseteq> {k. f1 k \<noteq> 0} \<union> {k. f2 k \<noteq> 0}"
+    by auto
+  ultimately show "finite {x. f1 x - f2 x \<noteq> 0}" by (blast intro: finite_subset)
+qed
+
+instance
+  by intro_classes (transfer, simp add: fun_eq_iff diff_diff_add)+
+
+end
+
+instantiation poly_mapping :: (type, ab_group_add) ab_group_add
+begin
+
+lift_definition uminus_poly_mapping :: "('a \<Rightarrow>\<^sub>0 'b) \<Rightarrow> 'a \<Rightarrow>\<^sub>0 'b"
+  is uminus
+  by simp
+
+
+instance
+  by intro_classes (transfer, simp add: fun_eq_iff ac_simps)+
+
+end
+
+lemma lookup_uminus [simp]:
+  "lookup (- f) k = - lookup f k"
+  by transfer simp
+
+lemma lookup_minus:
+  "lookup (f - g) k = lookup f k - lookup g k"
+  by transfer rule
+
+
+subsection \<open>Multiplicative structure\<close>
+
+instantiation poly_mapping :: (zero, zero_neq_one) zero_neq_one
+begin
+
+lift_definition one_poly_mapping :: "'a \<Rightarrow>\<^sub>0 'b"
+  is "\<lambda>k. 1 when k = 0"
+  by simp
+
+instance
+  by intro_classes (transfer, simp add: fun_eq_iff)
+
+end
+
+lemma lookup_one:
+  "lookup 1 k = (1 when k = 0)"
+  by transfer rule
+
+lemma lookup_one_zero [simp]:
+  "lookup 1 0 = 1"
+  by transfer simp
+
+definition prod_fun :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a::monoid_add \<Rightarrow> 'b::semiring_0"
+where
+  "prod_fun f1 f2 k = (\<Sum>l. f1 l * (\<Sum>q. (f2 q when k = l + q)))"
+
+lemma prod_fun_unfold_prod:
+  fixes f g :: "'a :: monoid_add \<Rightarrow> 'b::semiring_0"
+  assumes fin_f: "finite {a. f a \<noteq> 0}"
+  assumes fin_g: "finite {b. g b \<noteq> 0}"
+  shows "prod_fun f g k = (\<Sum>(a, b). f a * g b when k = a + b)"
+proof -
+  let ?C = "{a. f a \<noteq> 0} \<times> {b. g b \<noteq> 0}"
+  from fin_f fin_g have "finite ?C" by blast
+  moreover have "{a. \<exists>b. (f a * g b when k = a + b) \<noteq> 0} \<times>
+    {b. \<exists>a. (f a * g b when k = a + b) \<noteq> 0} \<subseteq> {a. f a \<noteq> 0} \<times> {b. g b \<noteq> 0}"
+    by auto
+  ultimately show ?thesis using fin_g
+    by (auto simp add: prod_fun_def
+      Sum_any.cartesian_product [of "{a. f a \<noteq> 0} \<times> {b. g b \<noteq> 0}"] Sum_any_right_distrib mult_when)
+qed
+
+lemma finite_prod_fun:
+  fixes f1 f2 :: "'a :: monoid_add \<Rightarrow> 'b :: semiring_0"
+  assumes fin1: "finite {l. f1 l \<noteq> 0}"
+  and fin2: "finite {q. f2 q \<noteq> 0}"
+  shows "finite {k. prod_fun f1 f2 k \<noteq> 0}"
+proof -
+  have *: "finite {k. (\<exists>l. f1 l \<noteq> 0 \<and> (\<exists>q. f2 q \<noteq> 0 \<and> k = l + q))}"
+    using assms by simp
+  { fix k l
+    have "{q. (f2 q when k = l + q) \<noteq> 0} \<subseteq> {q. f2 q \<noteq> 0 \<and> k = l + q}" by auto
+    with fin2 have "sum f2 {q. f2 q \<noteq> 0 \<and> k = l + q} = (\<Sum>q. (f2 q when k = l + q))"
+      by (simp add: Sum_any.expand_superset [of "{q. f2 q \<noteq> 0 \<and> k = l + q}"]) }
+  note aux = this
+  have "{k. (\<Sum>l. f1 l * sum f2 {q. f2 q \<noteq> 0 \<and> k = l + q}) \<noteq> 0}
+    \<subseteq> {k. (\<exists>l. f1 l * sum f2 {q. f2 q \<noteq> 0 \<and> k = l + q} \<noteq> 0)}"
+    by (auto elim!: Sum_any.not_neutral_obtains_not_neutral)
+  also have "\<dots> \<subseteq> {k. (\<exists>l. f1 l \<noteq> 0 \<and> sum f2 {q. f2 q \<noteq> 0 \<and> k = l + q} \<noteq> 0)}"
+    by (auto dest: mult_not_zero)
+  also have "\<dots> \<subseteq> {k. (\<exists>l. f1 l \<noteq> 0 \<and> (\<exists>q. f2 q \<noteq> 0 \<and> k = l + q))}"
+    by (auto elim!: sum.not_neutral_contains_not_neutral)
+  finally have "finite {k. (\<Sum>l. f1 l * sum f2 {q. f2 q \<noteq> 0 \<and> k = l + q}) \<noteq> 0}"
+    using * by (rule finite_subset)
+  with aux have "finite {k. (\<Sum>l. f1 l * (\<Sum>q. (f2 q when k = l + q))) \<noteq> 0}"
+    by simp
+  with fin2 show ?thesis
+   by (simp add: prod_fun_def)
+qed
+
+instantiation poly_mapping :: (monoid_add, semiring_0) semiring_0
+begin
+
+lift_definition times_poly_mapping :: "('a \<Rightarrow>\<^sub>0 'b) \<Rightarrow> ('a \<Rightarrow>\<^sub>0 'b) \<Rightarrow> 'a \<Rightarrow>\<^sub>0 'b"
+  is prod_fun
+by(rule finite_prod_fun)
+
+instance
+proof
+  fix a b c :: "'a \<Rightarrow>\<^sub>0 'b"
+  show "a * b * c = a * (b * c)"
+  proof transfer
+    fix f g h :: "'a \<Rightarrow> 'b"
+    assume fin_f: "finite {a. f a \<noteq> 0}" (is "finite ?F")
+    assume fin_g: "finite {b. g b \<noteq> 0}" (is "finite ?G")
+    assume fin_h: "finite {c. h c \<noteq> 0}" (is "finite ?H")
+    from fin_f fin_g have fin_fg: "finite {(a, b). f a * g b \<noteq> 0}" (is "finite ?FG")
+      by (rule finite_mult_not_eq_zero_prodI)
+    from fin_g fin_h have fin_gh: "finite {(b, c). g b * h c \<noteq> 0}" (is "finite ?GH")
+      by (rule finite_mult_not_eq_zero_prodI)
+    from fin_f fin_g have fin_fg': "finite {a + b | a b. f a * g b \<noteq> 0}" (is "finite ?FG'")
+      by (rule finite_mult_not_eq_zero_sumI)
+    then have fin_fg'': "finite {d. (\<Sum>(a, b). f a * g b when d = a + b) \<noteq> 0}"
+      by (auto intro: finite_Sum_any_not_eq_zero_weakenI)
+    from fin_g fin_h have fin_gh': "finite {b + c | b c. g b * h c \<noteq> 0}" (is "finite ?GH'")
+      by (rule finite_mult_not_eq_zero_sumI)
+    then have fin_gh'': "finite {d. (\<Sum>(b, c). g b * h c when d = b + c) \<noteq> 0}"
+      by (auto intro: finite_Sum_any_not_eq_zero_weakenI)
+    show "prod_fun (prod_fun f g) h = prod_fun f (prod_fun g h)" (is "?lhs = ?rhs")
+    proof
+      fix k
+      from fin_f fin_g fin_h fin_fg''
+      have "?lhs k = (\<Sum>(ab, c). (\<Sum>(a, b). f a * g b when ab = a + b) * h c when k = ab + c)"
+        by (simp add: prod_fun_unfold_prod)
+      also have "\<dots> = (\<Sum>(ab, c). (\<Sum>(a, b). f a * g b * h c when k = ab + c when ab = a + b))"
+        apply (subst Sum_any_left_distrib)
+        using fin_fg apply (simp add: split_def)
+        apply (subst Sum_any_when_independent [symmetric])
+        apply (simp add: when_when when_mult mult_when split_def conj_commute)
+        done
+      also have "\<dots> = (\<Sum>(ab, c, a, b). f a * g b * h c when k = ab + c when ab = a + b)"
+        apply (subst Sum_any.cartesian_product2 [of "(?FG' \<times> ?H) \<times> ?FG"])
+        apply (auto simp add: finite_cartesian_product_iff fin_fg fin_fg' fin_h dest: mult_not_zero)
+        done
+      also have "\<dots> = (\<Sum>(ab, c, a, b). f a * g b * h c when k = a + b + c when ab = a + b)"
+        by (rule Sum_any.cong) (simp add: split_def when_def)
+      also have "\<dots> = (\<Sum>(ab, cab). (case cab of (c, a, b) \<Rightarrow> f a * g b * h c when k = a + b + c)
+        when ab = (case cab of (c, a, b) \<Rightarrow> a + b))"
+        by (simp add: split_def)
+      also have "\<dots> = (\<Sum>(c, a, b). f a * g b * h c when k = a + b + c)"
+        by (simp add: Sum_any_when_dependent_prod_left)
+      also have "\<dots> = (\<Sum>(bc, cab). (case cab of (c, a, b) \<Rightarrow> f a * g b * h c when k = a + b + c)
+        when bc = (case cab of (c, a, b) \<Rightarrow> b + c))"
+        by (simp add: Sum_any_when_dependent_prod_left)
+      also have "\<dots> = (\<Sum>(bc, c, a, b). f a * g b * h c when k = a + b + c when bc = b + c)"
+        by (simp add: split_def)
+      also have "\<dots> = (\<Sum>(bc, c, a, b). f a * g b * h c when bc = b + c when k = a + bc)"
+        by (rule Sum_any.cong) (simp add: split_def when_def ac_simps)
+      also have "\<dots> = (\<Sum>(a, bc, b, c). f a * g b * h c when bc = b + c when k = a + bc)"
+      proof -
+        have "bij (\<lambda>(a, d, b, c). (d, c, a, b))"
+          by (auto intro!: bijI injI surjI [of _ "\<lambda>(d, c, a, b). (a, d, b, c)"] simp add: split_def)
+        then show ?thesis
+          by (rule Sum_any.reindex_cong) auto
+      qed
+      also have "\<dots> = (\<Sum>(a, bc). (\<Sum>(b, c). f a * g b * h c when bc = b + c when k = a + bc))"
+        apply (subst Sum_any.cartesian_product2 [of "(?F \<times> ?GH') \<times> ?GH"])
+        apply (auto simp add: finite_cartesian_product_iff fin_f fin_gh fin_gh' ac_simps dest: mult_not_zero)
+        done
+      also have "\<dots> = (\<Sum>(a, bc). f a * (\<Sum>(b, c). g b * h c when bc = b + c) when k = a + bc)"
+        apply (subst Sum_any_right_distrib)
+        using fin_gh apply (simp add: split_def)
+        apply (subst Sum_any_when_independent [symmetric])
+        apply (simp add: when_when when_mult mult_when split_def ac_simps)
+        done
+      also from fin_f fin_g fin_h fin_gh''
+      have "\<dots> = ?rhs k"
+        by (simp add: prod_fun_unfold_prod)
+      finally show "?lhs k = ?rhs k" .
+    qed
+  qed
+  show "(a + b) * c = a * c + b * c"
+  proof transfer
+    fix f g h :: "'a \<Rightarrow> 'b"
+    assume fin_f: "finite {k. f k \<noteq> 0}"
+    assume fin_g: "finite {k. g k \<noteq> 0}"
+    assume fin_h: "finite {k. h k \<noteq> 0}"
+    show "prod_fun (\<lambda>k. f k + g k) h = (\<lambda>k. prod_fun f h k + prod_fun g h k)"
+      apply (rule ext)
+      apply (auto simp add: prod_fun_def algebra_simps)
+      apply (subst Sum_any.distrib)
+      using fin_f fin_g apply (auto intro: finite_mult_not_eq_zero_rightI)
+      done
+  qed
+  show "a * (b + c) = a * b + a * c"
+  proof transfer
+    fix f g h :: "'a \<Rightarrow> 'b"
+    assume fin_f: "finite {k. f k \<noteq> 0}"
+    assume fin_g: "finite {k. g k \<noteq> 0}"
+    assume fin_h: "finite {k. h k \<noteq> 0}"
+    show "prod_fun f (\<lambda>k. g k + h k) = (\<lambda>k. prod_fun f g k + prod_fun f h k)"
+      apply (rule ext)
+      apply (auto simp add: prod_fun_def Sum_any.distrib algebra_simps when_add_distrib)
+      apply (subst Sum_any.distrib)
+      apply (simp_all add: algebra_simps)
+      apply (auto intro: fin_g fin_h)
+      apply (subst Sum_any.distrib)
+      apply (simp_all add: algebra_simps)
+      using fin_f apply (rule finite_mult_not_eq_zero_rightI)
+      using fin_f apply (rule finite_mult_not_eq_zero_rightI)
+      done
+  qed
+  show "0 * a = 0"
+    by transfer (simp add: prod_fun_def [abs_def])
+  show "a * 0 = 0"
+    by transfer (simp add: prod_fun_def [abs_def])
+qed
+
+end
+
+lemma lookup_mult:
+  "lookup (f * g) k = (\<Sum>l. lookup f l * (\<Sum>q. lookup g q when k = l + q))"
+  by transfer (simp add: prod_fun_def)
+
+instance poly_mapping :: (comm_monoid_add, comm_semiring_0) comm_semiring_0
+proof
+  fix a b c :: "'a \<Rightarrow>\<^sub>0 'b"
+  show "a * b = b * a"
+  proof transfer
+    fix f g :: "'a \<Rightarrow> 'b"
+    assume fin_f: "finite {a. f a \<noteq> 0}"
+    assume fin_g: "finite {b. g b \<noteq> 0}"
+    show "prod_fun f g = prod_fun g f"
+    proof
+      fix k
+      have fin1: "\<And>l. finite {a. (f a when k = l + a) \<noteq> 0}"
+        using fin_f by auto
+      have fin2: "\<And>l. finite {b. (g b when k = l + b) \<noteq> 0}"
+        using fin_g by auto
+      from fin_f fin_g have "finite {(a, b). f a \<noteq> 0 \<and> g b \<noteq> 0}" (is "finite ?AB")
+        by simp
+      show "prod_fun f g k = prod_fun g f k"
+        apply (simp add: prod_fun_def)
+        apply (subst Sum_any_right_distrib)
+        apply (rule fin2)
+        apply (subst Sum_any_right_distrib)
+         apply (rule fin1)
+        apply (subst Sum_any.swap [of ?AB])
+        apply (fact \<open>finite ?AB\<close>)
+        apply (auto simp add: mult_when ac_simps)
+        done
+    qed
+  qed
+  show "(a + b) * c = a * c + b * c"
+  proof transfer
+    fix f g h :: "'a \<Rightarrow> 'b"
+    assume fin_f: "finite {k. f k \<noteq> 0}"
+    assume fin_g: "finite {k. g k \<noteq> 0}"
+    assume fin_h: "finite {k. h k \<noteq> 0}"
+    show "prod_fun (\<lambda>k. f k + g k) h = (\<lambda>k. prod_fun f h k + prod_fun g h k)"
+      apply (auto simp add: prod_fun_def fun_eq_iff algebra_simps)
+      apply (subst Sum_any.distrib)
+      using fin_f apply (rule finite_mult_not_eq_zero_rightI)
+      using fin_g apply (rule finite_mult_not_eq_zero_rightI)
+      apply simp_all
+      done
+  qed
+qed
+
+instance poly_mapping :: (monoid_add, semiring_0_cancel) semiring_0_cancel
+  ..
+
+instance poly_mapping :: (comm_monoid_add, comm_semiring_0_cancel) comm_semiring_0_cancel
+  ..
+
+instance poly_mapping :: (monoid_add, semiring_1) semiring_1
+proof
+  fix a :: "'a \<Rightarrow>\<^sub>0 'b"
+  show "1 * a = a"
+    by transfer (simp add: prod_fun_def [abs_def] when_mult)
+  show "a * 1 = a"
+    apply transfer
+    apply (simp add: prod_fun_def [abs_def] Sum_any_right_distrib Sum_any_left_distrib mult_when)
+    apply (subst when_commute)
+    apply simp
+    done
+qed
+
+instance poly_mapping :: (comm_monoid_add, comm_semiring_1) comm_semiring_1
+proof
+  fix a :: "'a \<Rightarrow>\<^sub>0 'b"
+  show "1 * a = a"
+    by transfer (simp add: prod_fun_def [abs_def])
+qed
+
+instance poly_mapping :: (monoid_add, semiring_1_cancel) semiring_1_cancel
+  ..
+
+instance poly_mapping :: (monoid_add, ring) ring
+  ..
+
+instance poly_mapping :: (comm_monoid_add, comm_ring) comm_ring
+  ..
+
+instance poly_mapping :: (monoid_add, ring_1) ring_1
+  ..
+
+instance poly_mapping :: (comm_monoid_add, comm_ring_1) comm_ring_1
+  ..
+
+
+subsection \<open>Single-point mappings\<close>
+
+lift_definition single :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>0 'b::zero"
+  is "\<lambda>k v k'. (v when k = k')"
+  by simp
+
+lemma inj_single [iff]:
+  "inj (single k)"
+proof (rule injI, transfer)
+  fix k :: 'b and a b :: "'a::zero"
+  assume "(\<lambda>k'. a when k = k') = (\<lambda>k'. b when k = k')"
+  then have "(\<lambda>k'. a when k = k') k = (\<lambda>k'. b when k = k') k"
+    by (rule arg_cong)
+  then show "a = b" by simp
+qed
+
+lemma lookup_single:
+  "lookup (single k v) k' = (v when k = k')"
+  by transfer rule
+
+lemma lookup_single_eq [simp]:
+  "lookup (single k v) k = v"
+  by transfer simp
+
+lemma lookup_single_not_eq:
+  "k \<noteq> k' \<Longrightarrow> lookup (single k v) k' = 0"
+  by transfer simp
+
+lemma single_zero [simp]:
+  "single k 0 = 0"
+  by transfer simp
+
+lemma single_one [simp]:
+  "single 0 1 = 1"
+  by transfer simp
+
+lemma single_add:
+  "single k (a + b) = single k a + single k b"
+  by transfer (simp add: fun_eq_iff when_add_distrib)
+
+lemma single_uminus:
+  "single k (- a) = - single k a"
+  by transfer (simp add: fun_eq_iff when_uminus_distrib)
+
+lemma single_diff:
+  "single k (a - b) = single k a - single k b"
+  by transfer (simp add: fun_eq_iff when_diff_distrib)
+
+lemma single_numeral [simp]:
+  "single 0 (numeral n) = numeral n"
+  by (induct n) (simp_all only: numeral.simps numeral_add single_zero single_one single_add)
+
+lemma lookup_numeral:
+  "lookup (numeral n) k = (numeral n when k = 0)"
+proof -
+  have "lookup (numeral n) k = lookup (single 0 (numeral n)) k"
+    by simp
+  then show ?thesis unfolding lookup_single by simp
+qed
+
+lemma single_of_nat [simp]:
+  "single 0 (of_nat n) = of_nat n"
+  by (induct n) (simp_all add: single_add)
+
+lemma lookup_of_nat:
+  "lookup (of_nat n) k = (of_nat n when k = 0)"
+proof -
+  have "lookup (of_nat n) k = lookup (single 0 (of_nat n)) k"
+    by simp
+  then show ?thesis unfolding lookup_single by simp
+qed
+
+lemma of_nat_single:
+  "of_nat = single 0 \<circ> of_nat"
+  by (simp add: fun_eq_iff)
+
+lemma mult_single:
+  "single k a * single l b = single (k + l) (a * b)"
+proof transfer
+  fix k l :: 'a and a b :: 'b
+  show "prod_fun (\<lambda>k'. a when k = k') (\<lambda>k'. b when l = k') = (\<lambda>k'. a * b when k + l = k')"
+  proof
+    fix k'
+    have "prod_fun (\<lambda>k'. a when k = k') (\<lambda>k'. b when l = k') k' = (\<Sum>n. a * b when l = n when k' = k + n)"
+      by (simp add: prod_fun_def Sum_any_right_distrib mult_when when_mult)
+    also have "\<dots> = (\<Sum>n. a * b when k' = k + n when l = n)"
+      by (simp add: when_when conj_commute)
+    also have "\<dots> = (a * b when k' = k + l)"
+      by simp
+    also have "\<dots> = (a * b when k + l = k')"
+      by (simp add: when_def)
+    finally show "prod_fun (\<lambda>k'. a when k = k') (\<lambda>k'. b when l = k') k' =
+      (\<lambda>k'. a * b when k + l = k') k'" .
+  qed
+qed
+
+instance poly_mapping :: (monoid_add, semiring_char_0) semiring_char_0
+  by intro_classes (auto intro: inj_compose inj_of_nat simp add: of_nat_single)
+
+instance poly_mapping :: (monoid_add, ring_char_0) ring_char_0
+  ..
+
+lemma single_of_int [simp]:
+  "single 0 (of_int k) = of_int k"
+  by (cases k) (simp_all add: single_diff single_uminus)
+
+lemma lookup_of_int:
+  "lookup (of_int l) k = (of_int l when k = 0)"
+proof -
+  have "lookup (of_int l) k = lookup (single 0 (of_int l)) k"
+    by simp
+  then show ?thesis unfolding lookup_single by simp
+qed
+
+
+subsection \<open>Integral domains\<close>
+
+instance poly_mapping :: ("{ordered_cancel_comm_monoid_add, linorder}", semiring_no_zero_divisors) semiring_no_zero_divisors
+  text \<open>The @{class "linorder"} constraint is a pragmatic device for the proof --- maybe it can be dropped\<close>
+proof
+  fix f g :: "'a \<Rightarrow>\<^sub>0 'b"
+  assume "f \<noteq> 0" and "g \<noteq> 0"
+  then show "f * g \<noteq> 0"
+  proof transfer
+    fix f g :: "'a \<Rightarrow> 'b"
+    define F where "F = {a. f a \<noteq> 0}"
+    moreover define G where "G = {a. g a \<noteq> 0}"
+    ultimately have [simp]:
+      "\<And>a. f a \<noteq> 0 \<longleftrightarrow> a \<in> F"
+      "\<And>b. g b \<noteq> 0 \<longleftrightarrow> b \<in> G"
+      by simp_all
+    assume "finite {a. f a \<noteq> 0}"
+    then have [simp]: "finite F"
+      by simp
+    assume "finite {a. g a \<noteq> 0}"
+    then have [simp]: "finite G"
+      by simp
+    assume "f \<noteq> (\<lambda>a. 0)"
+    then obtain a where "f a \<noteq> 0"
+      by (auto simp add: fun_eq_iff)
+    assume "g \<noteq> (\<lambda>b. 0)"
+    then obtain b where "g b \<noteq> 0"
+      by (auto simp add: fun_eq_iff)
+    from \<open>f a \<noteq> 0\<close> and \<open>g b \<noteq> 0\<close> have "F \<noteq> {}" and "G \<noteq> {}"
+      by auto
+    note Max_F = \<open>finite F\<close> \<open>F \<noteq> {}\<close>
+    note Max_G = \<open>finite G\<close> \<open>G \<noteq> {}\<close>
+    from Max_F and Max_G have [simp]:
+      "Max F \<in> F"
+      "Max G \<in> G"
+      by auto
+    from Max_F Max_G have [dest!]:
+      "\<And>a. a \<in> F \<Longrightarrow> a \<le> Max F"
+      "\<And>b. b \<in> G \<Longrightarrow> b \<le> Max G"
+      by auto
+    define q where "q = Max F + Max G"
+    have "(\<Sum>(a, b). f a * g b when q = a + b) =
+      (\<Sum>(a, b). f a * g b when q = a + b when a \<in> F \<and> b \<in> G)"
+      by (rule Sum_any.cong) (auto simp add: split_def when_def q_def intro: ccontr)
+    also have "\<dots> =
+      (\<Sum>(a, b). f a * g b when (Max F, Max G) = (a, b))"
+    proof (rule Sum_any.cong)
+      fix ab :: "'a \<times> 'a"
+      obtain a b where [simp]: "ab = (a, b)"
+        by (cases ab) simp_all
+      have [dest!]:
+        "a \<le> Max F \<Longrightarrow> Max F \<noteq> a \<Longrightarrow> a < Max F"
+        "b \<le> Max G \<Longrightarrow> Max G \<noteq> b \<Longrightarrow> b < Max G"
+        by auto
+      show "(case ab of (a, b) \<Rightarrow> f a * g b when q = a + b when a \<in> F \<and> b \<in> G) =
+         (case ab of (a, b) \<Rightarrow> f a * g b when (Max F, Max G) = (a, b))"
+        by (auto simp add: split_def when_def q_def dest: add_strict_mono [of a "Max F" b "Max G"])
+    qed
+    also have "\<dots> = (\<Sum>ab. (case ab of (a, b) \<Rightarrow> f a * g b) when
+      (Max F, Max G) = ab)"
+      unfolding split_def when_def by auto
+    also have "\<dots> \<noteq> 0"
+      by simp
+    finally have "prod_fun f g q \<noteq> 0"
+      by (simp add: prod_fun_unfold_prod)
+    then show "prod_fun f g \<noteq> (\<lambda>k. 0)"
+      by (auto simp add: fun_eq_iff)
+  qed
+qed
+
+instance poly_mapping :: ("{ordered_cancel_comm_monoid_add, linorder}", ring_no_zero_divisors) ring_no_zero_divisors
+  ..
+
+instance poly_mapping :: ("{ordered_cancel_comm_monoid_add, linorder}", ring_1_no_zero_divisors) ring_1_no_zero_divisors
+  ..
+
+instance poly_mapping :: ("{ordered_cancel_comm_monoid_add, linorder}", idom) idom
+  ..
+
+
+subsection \<open>Mapping order\<close>
+
+instantiation poly_mapping :: (linorder, "{zero, linorder}") linorder
+begin
+
+lift_definition less_poly_mapping :: "('a \<Rightarrow>\<^sub>0 'b) \<Rightarrow> ('a \<Rightarrow>\<^sub>0 'b) \<Rightarrow> bool"
+  is less_fun
+  .
+
+lift_definition less_eq_poly_mapping :: "('a \<Rightarrow>\<^sub>0 'b) \<Rightarrow> ('a \<Rightarrow>\<^sub>0 'b) \<Rightarrow> bool"
+  is "\<lambda>f g. less_fun f g \<or> f = g"
+  .
+
+instance proof (rule class.Orderings.linorder.of_class.intro)
+  show "class.linorder (less_eq :: (_ \<Rightarrow>\<^sub>0 _) \<Rightarrow> _) less"
+  proof (rule linorder_strictI, rule order_strictI)
+    fix f g h :: "'a \<Rightarrow>\<^sub>0 'b"
+    show "f \<le> g \<longleftrightarrow> f < g \<or> f = g"
+      by transfer (rule refl)
+    show "\<not> f < f"
+      by transfer (rule less_fun_irrefl)
+    show "f < g \<or> f = g \<or> g < f"
+    proof transfer
+      fix f g :: "'a \<Rightarrow> 'b"
+      assume "finite {k. f k \<noteq> 0}" and "finite {k. g k \<noteq> 0}"
+      then have "finite ({k. f k \<noteq> 0} \<union> {k. g k \<noteq> 0})"
+        by simp
+      moreover have "{k. f k \<noteq> g k} \<subseteq> {k. f k \<noteq> 0} \<union> {k. g k \<noteq> 0}"
+        by auto
+      ultimately have "finite {k. f k \<noteq> g k}"
+        by (rule rev_finite_subset)
+      then show "less_fun f g \<or> f = g \<or> less_fun g f"
+        by (rule less_fun_trichotomy)
+    qed
+    assume "f < g" then show "\<not> g < f"
+      by transfer (rule less_fun_asym)
+    note \<open>f < g\<close> moreover assume "g < h"
+      ultimately show "f < h"
+      by transfer (rule less_fun_trans)
+  qed
+qed
+
+end
+
+instance poly_mapping :: (linorder, "{ordered_comm_monoid_add, ordered_ab_semigroup_add_imp_le, linorder}") ordered_ab_semigroup_add
+proof (intro_classes, transfer)
+  fix f g h :: "'a \<Rightarrow> 'b"
+  assume *: "less_fun f g \<or> f = g"
+  { assume "less_fun f g"
+    then obtain k where "f k < g k" "(\<And>k'. k' < k \<Longrightarrow> f k' = g k')"
+      by (blast elim!: less_funE)
+    then have "h k + f k < h k + g k" "(\<And>k'. k' < k \<Longrightarrow> h k' + f k' = h k' + g k')"
+      by simp_all
+    then have "less_fun (\<lambda>k. h k + f k) (\<lambda>k. h k + g k)"
+      by (blast intro: less_funI)
+  }
+  with * show "less_fun (\<lambda>k. h k + f k) (\<lambda>k. h k + g k) \<or> (\<lambda>k. h k + f k) = (\<lambda>k. h k + g k)"
+    by (auto simp add: fun_eq_iff)
+qed
+
+instance poly_mapping :: (linorder, "{ordered_comm_monoid_add, ordered_ab_semigroup_add_imp_le, cancel_comm_monoid_add, linorder}") linordered_cancel_ab_semigroup_add
+  ..
+
+instance poly_mapping :: (linorder, "{ordered_comm_monoid_add, ordered_ab_semigroup_add_imp_le, cancel_comm_monoid_add, linorder}") ordered_comm_monoid_add
+  ..
+
+instance poly_mapping :: (linorder, "{ordered_comm_monoid_add, ordered_ab_semigroup_add_imp_le, cancel_comm_monoid_add, linorder}") ordered_cancel_comm_monoid_add
+  ..
+
+instance poly_mapping :: (linorder, linordered_ab_group_add) linordered_ab_group_add
+  ..
+
+text \<open>
+  For pragmatism we leave out the final elements in the hierarchy:
+  @{class linordered_ring}, @{class linordered_ring_strict}, @{class linordered_idom};
+  remember that the order instance is a mere technical device, not a deeper algebraic
+  property.
+\<close>
+
+
+subsection \<open>Fundamental mapping notions\<close>
+
+lift_definition keys :: "('a \<Rightarrow>\<^sub>0 'b::zero) \<Rightarrow> 'a set"
+  is "\<lambda>f. {k. f k \<noteq> 0}" .
+
+lift_definition range :: "('a \<Rightarrow>\<^sub>0 'b::zero) \<Rightarrow> 'b set"
+  is "\<lambda>f :: 'a \<Rightarrow> 'b. Set.range f - {0}" .
+
+lemma finite_keys [simp]:
+  "finite (keys f)"
+  by transfer
+
+lemma not_in_keys_iff_lookup_eq_zero:
+  "k \<notin> keys f \<longleftrightarrow> lookup f k = 0"
+  by transfer simp
+
+lemma lookup_not_eq_zero_eq_in_keys:
+  "lookup f k \<noteq> 0 \<longleftrightarrow> k \<in> keys f"
+  by transfer simp
+
+lemma lookup_eq_zero_in_keys_contradict [dest]:
+  "lookup f k = 0 \<Longrightarrow> \<not> k \<in> keys f"
+  by (simp add: not_in_keys_iff_lookup_eq_zero)
+
+lemma finite_range [simp]: "finite (Poly_Mapping.range p)"
+proof transfer
+  fix f :: "'b \<Rightarrow> 'a"
+  assume *: "finite {x. f x \<noteq> 0}"
+  have "Set.range f - {0} \<subseteq> f ` {x. f x \<noteq> 0}"
+    by auto
+  thus "finite (Set.range f - {0})"
+    by(rule finite_subset)(rule finite_imageI[OF *])
+qed
+
+lemma in_keys_lookup_in_range [simp]:
+  "k \<in> keys f \<Longrightarrow> lookup f k \<in> range f"
+  by transfer simp
+
+lemma in_keys_iff: "x \<in> (keys s) = (lookup s x \<noteq> 0)"
+  by (transfer, simp)
+
+lemma keys_zero [simp]:
+  "keys 0 = {}"
+  by transfer simp
+
+lemma range_zero [simp]:
+  "range 0 = {}"
+  by transfer auto
+
+lemma keys_add:
+  "keys (f + g) \<subseteq> keys f \<union> keys g"
+  by transfer auto
+
+lemma keys_one [simp]:
+  "keys 1 = {0}"
+  by transfer simp
+
+lemma range_one [simp]:
+  "range 1 = {1}"
+  by transfer (auto simp add: when_def)
+
+lemma keys_single [simp]:
+  "keys (single k v) = (if v = 0 then {} else {k})"
+  by transfer simp
+
+lemma range_single [simp]:
+  "range (single k v) = (if v = 0 then {} else {v})"
+  by transfer (auto simp add: when_def)
+
+lemma keys_mult:
+  "keys (f * g) \<subseteq> {a + b | a b. a \<in> keys f \<and> b \<in> keys g}"
+  apply transfer
+  apply (auto simp add: prod_fun_def dest!: mult_not_zero elim!: Sum_any.not_neutral_obtains_not_neutral)
+  apply blast
+  done
+
+lemma setsum_keys_plus_distrib:
+  assumes hom_0: "\<And>k. f k 0 = 0"
+  and hom_plus: "\<And>k. k \<in> Poly_Mapping.keys p \<union> Poly_Mapping.keys q \<Longrightarrow> f k (Poly_Mapping.lookup p k + Poly_Mapping.lookup q k) = f k (Poly_Mapping.lookup p k) + f k (Poly_Mapping.lookup q k)"
+  shows
+  "(\<Sum>k\<in>Poly_Mapping.keys (p + q). f k (Poly_Mapping.lookup (p + q) k)) =
+   (\<Sum>k\<in>Poly_Mapping.keys p. f k (Poly_Mapping.lookup p k)) +
+   (\<Sum>k\<in>Poly_Mapping.keys q. f k (Poly_Mapping.lookup q k))"
+  (is "?lhs = ?p + ?q")
+proof -
+  let ?A = "Poly_Mapping.keys p \<union> Poly_Mapping.keys q"
+  have "?lhs = (\<Sum>k\<in>?A. f k (Poly_Mapping.lookup p k + Poly_Mapping.lookup q k))"
+    apply(rule sum.mono_neutral_cong_left)
+       apply(simp_all add: Poly_Mapping.keys_add)
+     apply(transfer fixing: f)
+     apply(auto simp add: hom_0)[1]
+    apply(transfer fixing: f)
+    apply(auto simp add: hom_0)[1]
+    done
+  also have "\<dots> = (\<Sum>k\<in>?A. f k (Poly_Mapping.lookup p k) + f k (Poly_Mapping.lookup q k))"
+    by(rule sum.cong)(simp_all add: hom_plus)
+  also have "\<dots> = (\<Sum>k\<in>?A. f k (Poly_Mapping.lookup p k)) + (\<Sum>k\<in>?A. f k (Poly_Mapping.lookup q k))"
+    (is "_ = ?p' + ?q'")
+    by(simp add: sum.distrib)
+  also have "?p' = ?p"
+    by (simp add: hom_0 in_keys_iff sum.mono_neutral_cong_right)
+  also have "?q' = ?q"
+    by (simp add: hom_0 in_keys_iff sum.mono_neutral_cong_right)
+  finally show ?thesis .
+qed
+
+subsection \<open>Degree\<close>
+
+definition degree :: "(nat \<Rightarrow>\<^sub>0 'a::zero) \<Rightarrow> nat"
+where
+  "degree f = Max (insert 0 (Suc ` keys f))"
+
+lemma degree_zero [simp]:
+  "degree 0 = 0"
+  unfolding degree_def by transfer simp
+
+lemma degree_one [simp]:
+  "degree 1 = 1"
+  unfolding degree_def by transfer simp
+
+lemma degree_single_zero [simp]:
+  "degree (single k 0) = 0"
+  unfolding degree_def by transfer simp
+
+lemma degree_single_not_zero [simp]:
+  "v \<noteq> 0 \<Longrightarrow> degree (single k v) = Suc k"
+  unfolding degree_def by transfer simp
+
+lemma degree_zero_iff [simp]:
+  "degree f = 0 \<longleftrightarrow> f = 0"
+unfolding degree_def proof transfer
+  fix f :: "nat \<Rightarrow> 'a"
+  assume "finite {n. f n \<noteq> 0}"
+  then have fin: "finite (insert 0 (Suc ` {n. f n \<noteq> 0}))" by auto
+  show "Max (insert 0 (Suc ` {n. f n \<noteq> 0})) = 0 \<longleftrightarrow> f = (\<lambda>n. 0)" (is "?P \<longleftrightarrow> ?Q")
+  proof
+    assume ?P
+    have "{n. f n \<noteq> 0} = {}"
+    proof (rule ccontr)
+      assume "{n. f n \<noteq> 0} \<noteq> {}"
+      then obtain n where "n \<in> {n. f n \<noteq> 0}" by blast
+      then have "{n. f n \<noteq> 0} = insert n {n. f n \<noteq> 0}" by auto
+      then have "Suc ` {n. f n \<noteq> 0} = insert (Suc n) (Suc ` {n. f n \<noteq> 0})" by auto
+      with \<open>?P\<close> have "Max (insert 0 (insert (Suc n) (Suc ` {n. f n \<noteq> 0}))) = 0" by simp
+      then have "Max (insert (Suc n) (insert 0 (Suc ` {n. f n \<noteq> 0}))) = 0"
+        by (simp add: insert_commute)
+      with fin have "max (Suc n) (Max (insert 0 (Suc ` {n. f n \<noteq> 0}))) = 0"
+        by simp
+      then show False by simp
+    qed
+    then show ?Q by (simp add: fun_eq_iff)
+  next
+    assume ?Q then show ?P by simp
+  qed
+qed
+
+lemma degree_greater_zero_in_keys:
+  assumes "0 < degree f"
+  shows "degree f - 1 \<in> keys f"
+proof -
+  from assms have "keys f \<noteq> {}"
+    by (auto simp add: degree_def)
+  then show ?thesis unfolding degree_def
+    by (simp add: mono_Max_commute [symmetric] mono_Suc)
+qed
+
+lemma in_keys_less_degree:
+  "n \<in> keys f \<Longrightarrow> n < degree f"
+unfolding degree_def by transfer (auto simp add: Max_gr_iff)
+
+lemma beyond_degree_lookup_zero:
+  "degree f \<le> n \<Longrightarrow> lookup f n = 0"
+  unfolding degree_def by transfer auto
+
+lemma degree_add:
+  "degree (f + g) \<le> max (degree f) (Poly_Mapping.degree g)"
+unfolding degree_def proof transfer
+  fix f g :: "nat \<Rightarrow> 'a"
+  assume f: "finite {x. f x \<noteq> 0}"
+  assume g: "finite {x. g x \<noteq> 0}"
+  let ?f = "Max (insert 0 (Suc ` {k. f k \<noteq> 0}))"
+  let ?g = "Max (insert 0 (Suc ` {k. g k \<noteq> 0}))"
+  have "Max (insert 0 (Suc ` {k. f k + g k \<noteq> 0})) \<le> Max (insert 0 (Suc ` ({k. f k \<noteq> 0} \<union> {k. g k \<noteq> 0})))"
+    by (rule Max.subset_imp) (insert f g, auto)
+  also have "\<dots> = max ?f ?g"
+    using f g by (simp_all add: image_Un Max_Un [symmetric])
+  finally show "Max (insert 0 (Suc ` {k. f k + g k \<noteq> 0}))
+    \<le> max (Max (insert 0 (Suc ` {k. f k \<noteq> 0}))) (Max (insert 0 (Suc ` {k. g k \<noteq> 0})))"
+    .
+qed
+
+lemma sorted_list_of_set_keys:
+  "sorted_list_of_set (keys f) = filter (\<lambda>k. k \<in> keys f) [0..<degree f]" (is "_ = ?r")
+proof -
+  have "keys f = set ?r"
+    by (auto dest: in_keys_less_degree)
+  moreover have "sorted_list_of_set (set ?r) = ?r"
+    unfolding sorted_list_of_set_sort_remdups
+    by (simp add: remdups_filter filter_sort [symmetric])
+  ultimately show ?thesis by simp
+qed
+
+
+subsection \<open>Inductive structure\<close>
+
+lift_definition update :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow>\<^sub>0 'b::zero) \<Rightarrow> 'a \<Rightarrow>\<^sub>0 'b"
+  is "\<lambda>k v f. f(k := v)"
+proof -
+  fix f :: "'a \<Rightarrow> 'b" and k' v
+  assume "finite {k. f k \<noteq> 0}"
+  then have "finite (insert k' {k. f k \<noteq> 0})"
+    by simp
+  then show "finite {k. (f(k' := v)) k \<noteq> 0}"
+    by (rule rev_finite_subset) auto
+qed
+
+lemma update_induct [case_names const update]:
+  assumes const': "P 0"
+  assumes update': "\<And>f a b. a \<notin> keys f \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> P f \<Longrightarrow> P (update a b f)"
+  shows "P f"
+proof -
+  obtain g where "f = Abs_poly_mapping g" and "finite {a. g a \<noteq> 0}"
+    by (cases f) simp_all
+  define Q where "Q g = P (Abs_poly_mapping g)" for g
+  from \<open>finite {a. g a \<noteq> 0}\<close> have "Q g"
+  proof (induct g rule: finite_update_induct)
+    case const with const' Q_def show ?case
+      by simp
+  next
+    case (update a b g)
+    from \<open>finite {a. g a \<noteq> 0}\<close> \<open>g a = 0\<close> have "a \<notin> keys (Abs_poly_mapping g)"
+      by (simp add: Abs_poly_mapping_inverse keys.rep_eq)
+    moreover note \<open>b \<noteq> 0\<close>
+    moreover from \<open>Q g\<close> have "P (Abs_poly_mapping g)"
+      by (simp add: Q_def)
+    ultimately have "P (update a b (Abs_poly_mapping g))"
+      by (rule update')
+    also from \<open>finite {a. g a \<noteq> 0}\<close>
+    have "update a b (Abs_poly_mapping g) = Abs_poly_mapping (g(a := b))"
+      by (simp add: update.abs_eq eq_onp_same_args)
+    finally show ?case
+      by (simp add: Q_def fun_upd_def)
+  qed
+  then show ?thesis by (simp add: Q_def \<open>f = Abs_poly_mapping g\<close>)
+qed
+
+lemma lookup_update:
+  "lookup (update k v f) k' = (if k = k' then v else lookup f k')"
+  by transfer simp
+
+lemma keys_update:
+  "keys (update k v f) = (if v = 0 then keys f - {k} else insert k (keys f))"
+  by transfer auto
+
+
+subsection \<open>Quasi-functorial structure\<close>
+
+lift_definition map :: "('b::zero \<Rightarrow> 'c::zero)
+  \<Rightarrow> ('a \<Rightarrow>\<^sub>0 'b) \<Rightarrow> ('a \<Rightarrow>\<^sub>0 'c::zero)"
+  is "\<lambda>g f k. g (f k) when f k \<noteq> 0"
+  by simp
+
+context
+  fixes f :: "'b \<Rightarrow> 'a"
+  assumes inj_f: "inj f"
+begin
+
+lift_definition map_key :: "('a \<Rightarrow>\<^sub>0 'c::zero) \<Rightarrow> 'b \<Rightarrow>\<^sub>0 'c"
+  is "\<lambda>p. p \<circ> f"
+proof -
+  fix g :: "'c \<Rightarrow> 'd" and p :: "'a \<Rightarrow> 'c"
+  assume "finite {x. p x \<noteq> 0}"
+  hence "finite (f ` {y. p (f y) \<noteq> 0})"
+    by(rule finite_subset[rotated]) auto
+  thus "finite {x. (p \<circ> f) x \<noteq> 0}" unfolding o_def
+    by(rule finite_imageD)(rule subset_inj_on[OF inj_f], simp)
+qed
+
+end
+
+lemma map_key_compose:
+  assumes [transfer_rule]: "inj f" "inj g"
+  shows "map_key f (map_key g p) = map_key (g \<circ> f) p"
+proof -
+  from assms have [transfer_rule]: "inj (g \<circ> f)"
+    by(simp add: inj_compose)
+  show ?thesis by transfer(simp add: o_assoc)
+qed
+
+lemma map_key_id:
+  "map_key (\<lambda>x. x) p = p"
+proof -
+  have [transfer_rule]: "inj (\<lambda>x. x)" by simp
+  show ?thesis by transfer(simp add: o_def)
+qed
+
+context
+  fixes f :: "'a \<Rightarrow> 'b"
+  assumes inj_f [transfer_rule]: "inj f"
+begin
+
+lemma map_key_map:
+  "map_key f (map g p) = map g (map_key f p)"
+  by transfer (simp add: fun_eq_iff)
+
+lemma map_key_plus:
+  "map_key f (p + q) = map_key f p + map_key f q"
+  by transfer (simp add: fun_eq_iff)
+
+lemma keys_map_key:
+  "keys (map_key f p) = f -` keys p"
+  by transfer auto
+
+lemma map_key_zero [simp]:
+  "map_key f 0 = 0"
+  by transfer (simp add: fun_eq_iff)
+
+lemma map_key_single [simp]:
+  "map_key f (single (f k) v) = single k v"
+  by transfer (simp add: fun_eq_iff inj_onD [OF inj_f] when_def)
+
+end
+
+lemma mult_map_scale_conv_mult: "map ((*) s) p = single 0 s * p"
+proof(transfer fixing: s)
+  fix p :: "'a \<Rightarrow> 'b"
+  assume *: "finite {x. p x \<noteq> 0}"
+  { fix x
+    have "prod_fun (\<lambda>k'. s when 0 = k') p x =
+          (\<Sum>l :: 'a. if l = 0 then s * (\<Sum>q. p q when x = q) else 0)"
+      by(auto simp add: prod_fun_def when_def intro: Sum_any.cong simp del: Sum_any.delta)
+    also have "\<dots> = (\<lambda>k. s * p k when p k \<noteq> 0) x" by(simp add: when_def)
+    also note calculation }
+  then show "(\<lambda>k. s * p k when p k \<noteq> 0) = prod_fun (\<lambda>k'. s when 0 = k') p"
+    by(simp add: fun_eq_iff)
+qed
+
+lemma map_single [simp]:
+  "(c = 0 \<Longrightarrow> f 0 = 0) \<Longrightarrow> map f (single x c) = single x (f c)"
+by transfer(auto simp add: fun_eq_iff when_def)
+
+lemma map_eq_zero_iff: "map f p = 0 \<longleftrightarrow> (\<forall>k \<in> keys p. f (lookup p k) = 0)"
+by transfer(auto simp add: fun_eq_iff when_def)
+
+subsection \<open>Canonical dense representation of @{typ "nat \<Rightarrow>\<^sub>0 'a"}\<close>
+
+abbreviation no_trailing_zeros :: "'a :: zero list \<Rightarrow> bool"
+where
+  "no_trailing_zeros \<equiv> no_trailing ((=) 0)"
+
+lift_definition "nth" :: "'a list \<Rightarrow> (nat \<Rightarrow>\<^sub>0 'a::zero)"
+  is "nth_default 0"
+  by (fact finite_nth_default_neq_default)
+
+text \<open>
+  The opposite direction is directly specified on (later)
+  type \<open>nat_mapping\<close>.
+\<close>
+
+lemma nth_Nil [simp]:
+  "nth [] = 0"
+  by transfer (simp add: fun_eq_iff)
+
+lemma nth_singleton [simp]:
+  "nth [v] = single 0 v"
+proof (transfer, rule ext)
+  fix n :: nat and v :: 'a
+  show "nth_default 0 [v] n = (v when 0 = n)"
+    by (auto simp add: nth_default_def nth_append)
+qed
+
+lemma nth_replicate [simp]:
+  "nth (replicate n 0 @ [v]) = single n v"
+proof (transfer, rule ext)
+  fix m n :: nat and v :: 'a
+  show "nth_default 0 (replicate n 0 @ [v]) m = (v when n = m)"
+    by (auto simp add: nth_default_def nth_append)
+qed
+
+lemma nth_strip_while [simp]:
+  "nth (strip_while ((=) 0) xs) = nth xs"
+  by transfer (fact nth_default_strip_while_dflt)
+
+lemma nth_strip_while' [simp]:
+  "nth (strip_while (\<lambda>k. k = 0) xs) = nth xs"
+  by (subst eq_commute) (fact nth_strip_while)
+
+lemma nth_eq_iff:
+  "nth xs = nth ys \<longleftrightarrow> strip_while (HOL.eq 0) xs = strip_while (HOL.eq 0) ys"
+  by transfer (simp add: nth_default_eq_iff)
+
+lemma lookup_nth [simp]:
+  "lookup (nth xs) = nth_default 0 xs"
+  by (fact nth.rep_eq)
+
+lemma keys_nth [simp]:
+  "keys (nth xs) =  fst ` {(n, v) \<in> set (enumerate 0 xs). v \<noteq> 0}"
+proof transfer
+  fix xs :: "'a list"
+  { fix n
+    assume "nth_default 0 xs n \<noteq> 0"
+    then have "n < length xs" and "xs ! n \<noteq> 0"
+      by (auto simp add: nth_default_def split: if_splits)
+    then have "(n, xs ! n) \<in> {(n, v). (n, v) \<in> set (enumerate 0 xs) \<and> v \<noteq> 0}" (is "?x \<in> ?A")
+      by (auto simp add: in_set_conv_nth enumerate_eq_zip)
+    then have "fst ?x \<in> fst ` ?A"
+      by blast
+    then have "n \<in> fst ` {(n, v). (n, v) \<in> set (enumerate 0 xs) \<and> v \<noteq> 0}"
+      by simp
+  }
+  then show "{k. nth_default 0 xs k \<noteq> 0} = fst ` {(n, v). (n, v) \<in> set (enumerate 0 xs) \<and> v \<noteq> 0}"
+    by (auto simp add: in_enumerate_iff_nth_default_eq)
+qed
+
+lemma range_nth [simp]:
+  "range (nth xs) = set xs - {0}"
+  by transfer simp
+
+lemma degree_nth:
+  "no_trailing_zeros xs \<Longrightarrow> degree (nth xs) = length xs"
+unfolding degree_def proof transfer
+  fix xs :: "'a list"
+  assume *: "no_trailing_zeros xs"
+  let ?A = "{n. nth_default 0 xs n \<noteq> 0}"
+  let ?f = "nth_default 0 xs"
+  let ?bound = "Max (insert 0 (Suc ` {n. ?f n \<noteq> 0}))"
+  show "?bound = length xs"
+  proof (cases "xs = []")
+    case False
+    with * obtain n where n: "n < length xs" "xs ! n \<noteq> 0"
+      by (fastforce simp add: no_trailing_unfold last_conv_nth neq_Nil_conv)
+    then have "?bound = Max (Suc ` {k. (k < length xs \<longrightarrow> xs ! k \<noteq> (0::'a)) \<and> k < length xs})"
+      by (subst Max_insert) (auto simp add: nth_default_def)
+    also let ?A = "{k. k < length xs \<and> xs ! k \<noteq> 0}"
+    have "{k. (k < length xs \<longrightarrow> xs ! k \<noteq> (0::'a)) \<and> k < length xs} = ?A" by auto
+    also have "Max (Suc ` ?A) = Suc (Max ?A)" using n
+      by (subst mono_Max_commute [where f = Suc, symmetric]) (auto simp add: mono_Suc)
+    also {
+      have "Max ?A \<in> ?A" using n Max_in [of ?A] by fastforce
+      hence "Suc (Max ?A) \<le> length xs" by simp
+      moreover from * False have "length xs - 1 \<in> ?A"
+        by(auto simp add: no_trailing_unfold last_conv_nth)
+      hence "length xs - 1 \<le> Max ?A" using Max_ge[of ?A "length xs - 1"] by auto
+      hence "length xs \<le> Suc (Max ?A)" by simp
+      ultimately have "Suc (Max ?A) = length xs" by simp }
+    finally show ?thesis .
+  qed simp
+qed
+
+lemma nth_trailing_zeros [simp]:
+  "nth (xs @ replicate n 0) = nth xs"
+  by transfer simp
+
+lemma nth_idem:
+  "nth (List.map (lookup f) [0..<degree f]) = f"
+  unfolding degree_def by transfer
+    (auto simp add: nth_default_def fun_eq_iff not_less)
+
+lemma nth_idem_bound:
+  assumes "degree f \<le> n"
+  shows "nth (List.map (lookup f) [0..<n]) = f"
+proof -
+  from assms obtain m where "n = degree f + m"
+    by (blast dest: le_Suc_ex)
+  then have "[0..<n] = [0..<degree f] @ [degree f..<degree f + m]"
+    by (simp add: upt_add_eq_append [of 0])
+  moreover have "List.map (lookup f) [degree f..<degree f + m] = replicate m 0"
+    by (rule replicate_eqI) (auto simp add: beyond_degree_lookup_zero)
+  ultimately show ?thesis by (simp add: nth_idem)
+qed
+
+
+subsection \<open>Canonical sparse representation of @{typ "'a \<Rightarrow>\<^sub>0 'b"}\<close>
+
+lift_definition the_value :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow>\<^sub>0 'b::zero"
+  is "\<lambda>xs k. case map_of xs k of None \<Rightarrow> 0 | Some v \<Rightarrow> v"
+proof -
+  fix xs :: "('a \<times> 'b) list"
+  have fin: "finite {k. \<exists>v. map_of xs k = Some v}"
+    using finite_dom_map_of [of xs] unfolding dom_def by auto
+  then show "finite {k. (case map_of xs k of None \<Rightarrow> 0 | Some v \<Rightarrow> v) \<noteq> 0}"
+    using fin by (simp split: option.split)
+qed
+
+definition items :: "('a::linorder \<Rightarrow>\<^sub>0 'b::zero) \<Rightarrow> ('a \<times> 'b) list"
+where
+  "items f = List.map (\<lambda>k. (k, lookup f k)) (sorted_list_of_set (keys f))"
+
+text \<open>
+  For the canonical sparse representation we provide both
+  directions of morphisms since the specification of
+  ordered association lists in theory \<open>OAList\<close>
+  will support arbitrary linear orders @{class linorder}
+  as keys, not just natural numbers @{typ nat}.
+\<close>
+
+lemma the_value_items [simp]:
+  "the_value (items f) = f"
+  unfolding items_def
+  by transfer (simp add: fun_eq_iff map_of_map_restrict restrict_map_def)
+
+lemma lookup_the_value:
+  "lookup (the_value xs) k = (case map_of xs k of None \<Rightarrow> 0 | Some v \<Rightarrow> v)"
+  by transfer rule
+
+lemma items_the_value:
+  assumes "sorted (List.map fst xs)" and "distinct (List.map fst xs)" and "0 \<notin> snd ` set xs"
+  shows "items (the_value xs) = xs"
+proof -
+  from assms have "sorted_list_of_set (set (List.map fst xs)) = List.map fst xs"
+    unfolding sorted_list_of_set_sort_remdups by (simp add: distinct_remdups_id sorted_sort_id)
+  moreover from assms have "keys (the_value xs) = fst ` set xs"
+    by transfer (auto simp add: image_def split: option.split dest: set_map_of_compr)
+  ultimately show ?thesis
+    unfolding items_def using assms
+    by (auto simp add: lookup_the_value intro: map_idI)
+qed
+
+lemma the_value_Nil [simp]:
+  "the_value [] = 0"
+  by transfer (simp add: fun_eq_iff)
+
+lemma the_value_Cons [simp]:
+  "the_value (x # xs) = update (fst x) (snd x) (the_value xs)"
+  by transfer (simp add: fun_eq_iff)
+
+lemma items_zero [simp]:
+  "items 0 = []"
+  unfolding items_def by simp
+
+lemma items_one [simp]:
+  "items 1 = [(0, 1)]"
+  unfolding items_def by transfer simp
+
+lemma items_single [simp]:
+  "items (single k v) = (if v = 0 then [] else [(k, v)])"
+  unfolding items_def by simp
+
+lemma in_set_items_iff [simp]:
+  "(k, v) \<in> set (items f) \<longleftrightarrow> k \<in> keys f \<and> lookup f k = v"
+  unfolding items_def by transfer auto
+
+
+subsection \<open>Size estimation\<close>
+
+context
+  fixes f :: "'a \<Rightarrow> nat"
+  and g :: "'b :: zero \<Rightarrow> nat"
+begin
+
+definition poly_mapping_size :: "('a \<Rightarrow>\<^sub>0 'b) \<Rightarrow> nat"
+where
+  "poly_mapping_size m = g 0 + (\<Sum>k \<in> keys m. Suc (f k + g (lookup m k)))"
+
+lemma poly_mapping_size_0 [simp]:
+  "poly_mapping_size 0 = g 0"
+  by (simp add: poly_mapping_size_def)
+
+lemma poly_mapping_size_single [simp]:
+  "poly_mapping_size (single k v) = (if v = 0 then g 0 else g 0 + f k + g v + 1)"
+  unfolding poly_mapping_size_def by transfer simp
+
+lemma keys_less_poly_mapping_size:
+  "k \<in> keys m \<Longrightarrow> f k + g (lookup m k) < poly_mapping_size m"
+unfolding poly_mapping_size_def
+proof transfer
+  fix k :: 'a and m :: "'a \<Rightarrow> 'b" and f :: "'a \<Rightarrow> nat" and g
+  let ?keys = "{k. m k \<noteq> 0}"
+  assume *: "finite ?keys" "k \<in> ?keys"
+  then have "f k + g (m k) = (\<Sum>k' \<in> ?keys. f k' + g (m k') when k' = k)"
+    by (simp add: sum.delta when_def)
+  also have "\<dots> < (\<Sum>k' \<in> ?keys. Suc (f k' + g (m k')))" using *
+    by (intro sum_strict_mono) (auto simp add: when_def)
+  also have "\<dots> \<le> g 0 + \<dots>" by simp
+  finally have "f k + g (m k) < \<dots>" .
+  then show "f k + g (m k) < g 0 + (\<Sum>k | m k \<noteq> 0. Suc (f k + g (m k)))"
+    by simp
+qed
+
+lemma lookup_le_poly_mapping_size:
+  "g (lookup m k) \<le> poly_mapping_size m"
+proof (cases "k \<in> keys m")
+  case True
+  with keys_less_poly_mapping_size [of k m]
+  show ?thesis by simp
+next
+  case False
+  then show ?thesis
+    by (simp add: Poly_Mapping.poly_mapping_size_def in_keys_iff)
+qed 
+
+lemma poly_mapping_size_estimation:
+  "k \<in> keys m \<Longrightarrow> y \<le> f k + g (lookup m k) \<Longrightarrow> y < poly_mapping_size m"
+  using keys_less_poly_mapping_size by (auto intro: le_less_trans)
+
+lemma poly_mapping_size_estimation2:
+  assumes "v \<in> range m" and "y \<le> g v"
+  shows "y < poly_mapping_size m"
+proof -
+  from assms obtain k where *: "lookup m k = v" "v \<noteq> 0"
+    by transfer blast
+  from * have "k \<in> keys m"
+    by (simp add: in_keys_iff)
+  then show ?thesis
+  proof (rule poly_mapping_size_estimation)
+    from assms * have "y \<le> g (lookup m k)"
+      by simp
+    then show "y \<le> f k + g (lookup m k)"
+      by simp
+  qed
+qed
+
+end
+
+lemma poly_mapping_size_one [simp]:
+  "poly_mapping_size f g 1 = g 0 + f 0 + g 1 + 1"
+  unfolding poly_mapping_size_def by transfer simp
+
+lemma poly_mapping_size_cong [fundef_cong]:
+  "m = m' \<Longrightarrow> g 0 = g' 0 \<Longrightarrow> (\<And>k. k \<in> keys m' \<Longrightarrow> f k = f' k)
+    \<Longrightarrow> (\<And>v. v \<in> range m' \<Longrightarrow> g v = g' v)
+    \<Longrightarrow> poly_mapping_size f g m = poly_mapping_size f' g' m'"
+  by (auto simp add: poly_mapping_size_def intro!: sum.cong)
+
+instantiation poly_mapping :: (type, zero) size
+begin
+
+definition "size = poly_mapping_size (\<lambda>_. 0) (\<lambda>_. 0)"
+
+instance ..
+
+end
+
+
+subsection \<open>Further mapping operations and properties\<close>
+
+text \<open>It is like in algebra: there are many definitions, some are also used\<close>
+
+lift_definition mapp ::
+  "('a \<Rightarrow> 'b :: zero \<Rightarrow> 'c :: zero) \<Rightarrow> ('a \<Rightarrow>\<^sub>0 'b) \<Rightarrow> ('a \<Rightarrow>\<^sub>0 'c)"
+  is "\<lambda>f p k. (if k \<in> keys p then f k (lookup p k) else 0)"
+  by simp
+
+lemma mapp_cong [fundef_cong]:
+  "\<lbrakk> m = m'; \<And>k. k \<in> keys m' \<Longrightarrow> f k (lookup m' k) = f' k (lookup m' k) \<rbrakk>
+  \<Longrightarrow> mapp f m = mapp f' m'"
+  by transfer (auto simp add: fun_eq_iff)
+
+lemma lookup_mapp:
+  "lookup (mapp f p) k = (f k (lookup p k) when k \<in> keys p)"
+  by (simp add: mapp.rep_eq)
+
+lemma keys_mapp_subset: "keys (mapp f p) \<subseteq> keys p"
+  by (meson in_keys_iff mapp.rep_eq subsetI)
+
+subsection\<open>Free Abelian Groups Over a Type\<close>
+
+abbreviation frag_of :: "'a \<Rightarrow> 'a \<Rightarrow>\<^sub>0 int"
+  where "frag_of c \<equiv> Poly_Mapping.single c (1::int)"
+
+lemma lookup_frag_of [simp]:
+   "Poly_Mapping.lookup(frag_of c) = (\<lambda>x. if x = c then 1 else 0)"
+  by (force simp add: lookup_single_not_eq)
+
+lemma frag_of_nonzero [simp]: "frag_of a \<noteq> 0"
+proof -
+  let ?f = "\<lambda>x. if x = a then 1 else (0::int)"
+  have "?f \<noteq> (\<lambda>x. 0::int)"
+    by (auto simp: fun_eq_iff)
+  then have "Poly_Mapping.lookup (Abs_poly_mapping ?f) \<noteq> Poly_Mapping.lookup (Abs_poly_mapping (\<lambda>x. 0))"
+    by fastforce
+  then show ?thesis
+    by (metis lookup_single_eq lookup_zero)
+qed
+
+definition frag_cmul :: "int \<Rightarrow> ('a \<Rightarrow>\<^sub>0 int) \<Rightarrow> ('a \<Rightarrow>\<^sub>0 int)"
+  where "frag_cmul c a = Abs_poly_mapping (\<lambda>x. c * Poly_Mapping.lookup a x)"
+
+lemma frag_cmul_zero [simp]: "frag_cmul 0 x = 0"
+  by (simp add: frag_cmul_def)
+
+lemma frag_cmul_zero2 [simp]: "frag_cmul c 0 = 0"
+  by (simp add: frag_cmul_def)
+
+lemma frag_cmul_one [simp]: "frag_cmul 1 x = x"
+  by (auto simp: frag_cmul_def Poly_Mapping.poly_mapping.lookup_inverse)
+
+lemma frag_cmul_minus_one [simp]: "frag_cmul (-1) x = -x"
+  by (simp add: frag_cmul_def uminus_poly_mapping_def poly_mapping_eqI)
+
+lemma frag_cmul_cmul [simp]: "frag_cmul c (frag_cmul d x) = frag_cmul (c*d) x"
+  by (simp add: frag_cmul_def mult_ac)
+
+lemma lookup_frag_cmul [simp]: "poly_mapping.lookup (frag_cmul c x) i = c * poly_mapping.lookup x i"
+  by (simp add: frag_cmul_def)
+
+lemma minus_frag_cmul [simp]: "- frag_cmul k x = frag_cmul (-k) x"
+  by (simp add: poly_mapping_eqI)
+
+lemma keys_frag_of: "Poly_Mapping.keys(frag_of a) = {a}"
+  by simp
+
+lemma finite_cmul_nonzero: "finite {x. c * Poly_Mapping.lookup a x \<noteq> (0::int)}"
+  by simp
+
+lemma keys_cmul: "Poly_Mapping.keys(frag_cmul c a) \<subseteq> Poly_Mapping.keys a"
+  using finite_cmul_nonzero [of c a]
+  by (metis lookup_frag_cmul mult_zero_right not_in_keys_iff_lookup_eq_zero subsetI)
+  
+
+lemma keys_cmul_iff [iff]: "i \<in> Poly_Mapping.keys (frag_cmul c x) \<longleftrightarrow> i \<in> Poly_Mapping.keys x \<and> c \<noteq> 0"
+  apply (auto simp: )
+  apply (meson subsetD keys_cmul)
+  by (metis in_keys_iff lookup_frag_cmul mult_eq_0_iff)
+
+lemma keys_minus [simp]: "Poly_Mapping.keys(-a) = Poly_Mapping.keys a"
+  by (metis (no_types, hide_lams) in_keys_iff lookup_uminus neg_equal_0_iff_equal subsetI subset_antisym)
+
+lemma keys_diff: 
+  "Poly_Mapping.keys(a - b) \<subseteq> Poly_Mapping.keys a \<union> Poly_Mapping.keys b"
+  by (auto simp add: in_keys_iff lookup_minus)
+
+lemma keys_eq_empty [simp]: "Poly_Mapping.keys c = {} \<longleftrightarrow> c = 0"
+  by (metis in_keys_iff keys_zero lookup_zero poly_mapping_eqI)
+
+lemma frag_cmul_eq_0_iff [simp]: "frag_cmul k c = 0 \<longleftrightarrow> k=0 \<or> c=0"
+  by auto (metis subsetI subset_antisym keys_cmul_iff keys_eq_empty)
+
+lemma frag_of_eq: "frag_of x = frag_of y \<longleftrightarrow> x = y"
+  by (metis lookup_single_eq lookup_single_not_eq zero_neq_one)
+
+lemma frag_cmul_distrib: "frag_cmul (c+d) a = frag_cmul c a + frag_cmul d a"
+  by (simp add: frag_cmul_def plus_poly_mapping_def int_distrib)
+
+lemma frag_cmul_distrib2: "frag_cmul c (a+b) = frag_cmul c a + frag_cmul c b"
+proof -
+  have "finite {x. poly_mapping.lookup a x + poly_mapping.lookup b x \<noteq> 0}"
+    using keys_add [of a b]
+    by (metis (no_types, lifting) finite_keys finite_subset keys.rep_eq lookup_add mem_Collect_eq subsetI)
+  then show ?thesis
+    by (simp add: frag_cmul_def plus_poly_mapping_def int_distrib)
+qed
+
+lemma frag_cmul_diff_distrib: "frag_cmul (a - b) c = frag_cmul a c - frag_cmul b c"
+  by (auto simp: left_diff_distrib lookup_minus poly_mapping_eqI)
+
+lemma frag_cmul_sum:
+     "frag_cmul a (sum b I) = (\<Sum>i\<in>I. frag_cmul a (b i))"
+proof (induction rule: infinite_finite_induct)
+  case (insert i I)
+  then show ?case
+    by (auto simp: algebra_simps frag_cmul_distrib2)
+qed auto
+
+lemma keys_sum: "Poly_Mapping.keys(sum b I) \<subseteq> (\<Union>i \<in>I. Poly_Mapping.keys(b i))"
+proof (induction I rule: infinite_finite_induct)
+  case (insert i I)
+  then show ?case
+    using keys_add [of "b i" "sum b I"] by auto
+qed auto
+
+
+definition frag_extend :: "('b \<Rightarrow> 'a \<Rightarrow>\<^sub>0 int) \<Rightarrow> ('b \<Rightarrow>\<^sub>0 int) \<Rightarrow> 'a \<Rightarrow>\<^sub>0 int"
+  where "frag_extend b x \<equiv> (\<Sum>i \<in> Poly_Mapping.keys x. frag_cmul (Poly_Mapping.lookup x i) (b i))"
+
+lemma frag_extend_0 [simp]: "frag_extend b 0 = 0"
+  by (simp add: frag_extend_def)
+
+lemma frag_extend_of [simp]: "frag_extend f (frag_of a) = f a"
+  by (simp add: frag_extend_def)
+
+lemma frag_extend_cmul:
+   "frag_extend f (frag_cmul c x) = frag_cmul c (frag_extend f x)"
+  by (auto simp: frag_extend_def frag_cmul_sum intro: sum.mono_neutral_cong_left)
+
+lemma frag_extend_minus:
+   "frag_extend f (- x) = - (frag_extend f x)"
+  using frag_extend_cmul [of f "-1"] by simp
+
+lemma frag_extend_add:
+  "frag_extend f (a+b) = (frag_extend f a) + (frag_extend f b)"
+proof -
+  have *: "(\<Sum>i\<in>Poly_Mapping.keys a. frag_cmul (poly_mapping.lookup a i) (f i)) 
+         = (\<Sum>i\<in>Poly_Mapping.keys a \<union> Poly_Mapping.keys b. frag_cmul (poly_mapping.lookup a i) (f i))"
+          "(\<Sum>i\<in>Poly_Mapping.keys b. frag_cmul (poly_mapping.lookup b i) (f i)) 
+         = (\<Sum>i\<in>Poly_Mapping.keys a \<union> Poly_Mapping.keys b. frag_cmul (poly_mapping.lookup b i) (f i))"
+    by (auto simp: in_keys_iff intro: sum.mono_neutral_cong_left)
+  have "frag_extend f (a+b) = (\<Sum>i\<in>Poly_Mapping.keys (a + b).
+       frag_cmul (poly_mapping.lookup a i) (f i) + frag_cmul (poly_mapping.lookup b i) (f i)) "
+    by (auto simp: frag_extend_def Poly_Mapping.lookup_add frag_cmul_distrib)
+  also have "... = (\<Sum>i \<in> Poly_Mapping.keys a \<union> Poly_Mapping.keys b. frag_cmul (poly_mapping.lookup a i) (f i) 
+                         + frag_cmul (poly_mapping.lookup b i) (f i))"
+    apply (rule sum.mono_neutral_cong_left)
+    using keys_add [of a b]
+     apply (auto simp add: in_keys_iff plus_poly_mapping.rep_eq frag_cmul_distrib [symmetric])
+    done
+  also have "... = (frag_extend f a) + (frag_extend f b)"
+    by (auto simp: * sum.distrib frag_extend_def)
+  finally show ?thesis .
+qed
+
+lemma frag_extend_diff:
+   "frag_extend f (a-b) = (frag_extend f a) - (frag_extend f b)"
+  by (metis (no_types, hide_lams) add_uminus_conv_diff frag_extend_add frag_extend_minus)
+
+lemma frag_extend_sum:
+   "finite I \<Longrightarrow> frag_extend f (\<Sum>i\<in>I. g i) = sum (frag_extend f o g) I"
+  by (induction I rule: finite_induct) (simp_all add: frag_extend_add)
+
+lemma frag_extend_eq:
+   "(\<And>f. f \<in> Poly_Mapping.keys c \<Longrightarrow> g f = h f) \<Longrightarrow> frag_extend g c = frag_extend h c"
+  by (simp add: frag_extend_def)
+
+lemma frag_extend_eq_0:
+   "(\<And>x. x \<in> Poly_Mapping.keys c \<Longrightarrow> f x = 0) \<Longrightarrow> frag_extend f c = 0"
+  by (simp add: frag_extend_def)
+
+lemma keys_frag_extend: "Poly_Mapping.keys(frag_extend f c) \<subseteq> (\<Union>x \<in> Poly_Mapping.keys c. Poly_Mapping.keys(f x))"
+  unfolding frag_extend_def
+  by (smt SUP_mono' keys_cmul keys_sum order_trans)
+
+lemma frag_expansion: "a = frag_extend frag_of a"
+proof -
+  have *: "finite I
+        \<Longrightarrow> Poly_Mapping.lookup (\<Sum>i\<in>I. frag_cmul (Poly_Mapping.lookup a i) (frag_of i)) j =
+            (if j \<in> I then Poly_Mapping.lookup a j else 0)" for I j
+    by (induction I rule: finite_induct) (auto simp: lookup_single lookup_add)
+  show ?thesis
+    unfolding frag_extend_def
+    by (rule poly_mapping_eqI) (fastforce simp add: in_keys_iff *)
+qed
+
+lemma frag_closure_minus_cmul:
+  assumes "P 0" and P: "\<And>x y. \<lbrakk>P x; P y\<rbrakk> \<Longrightarrow> P(x - y)" "P c"
+  shows "P(frag_cmul k c)"
+proof -
+  have "P (frag_cmul (int n) c)" for n
+    apply (induction n)
+     apply (simp_all add: assms frag_cmul_distrib)
+    by (metis add.left_neutral add_diff_cancel_right' add_uminus_conv_diff P)
+  then show ?thesis
+    by (metis (no_types, hide_lams) add_diff_eq assms(2) diff_add_cancel frag_cmul_distrib int_diff_cases)
+qed
+
+lemma frag_induction [consumes 1, case_names zero one diff]:
+  assumes supp: "Poly_Mapping.keys c \<subseteq> S"
+    and 0: "P 0" and sing: "\<And>x. x \<in> S \<Longrightarrow> P(frag_of x)"
+    and diff: "\<And>a b. \<lbrakk>P a; P b\<rbrakk> \<Longrightarrow> P(a - b)"
+  shows "P c"
+proof -
+  have "P (\<Sum>i\<in>I. frag_cmul (poly_mapping.lookup c i) (frag_of i))"
+    if "I \<subseteq> Poly_Mapping.keys c" for I
+    using finite_subset [OF that finite_keys [of c]] that supp
+  proof (induction I arbitrary: c rule: finite_induct)
+    case empty
+    then show ?case
+      by (auto simp: 0)
+  next
+    case (insert i I c)
+    have ab: "a+b = a - (0 - b)" for a b :: "'a \<Rightarrow>\<^sub>0 int"
+      by simp
+    have Pfrag: "P (frag_cmul (poly_mapping.lookup c i) (frag_of i))"
+      by (metis "0" diff frag_closure_minus_cmul insert.prems insert_subset sing subset_iff)
+    show ?case
+      apply (simp add: insert.hyps)
+      apply (subst ab)
+      using insert apply (blast intro: assms Pfrag)
+      done
+  qed
+  then show ?thesis
+    by (subst frag_expansion) (auto simp add: frag_extend_def)
+qed
+
+lemma frag_extend_compose:
+  "frag_extend f (frag_extend (frag_of o g) c) = frag_extend (f o g) c"
+  using subset_UNIV
+  by (induction c rule: frag_induction) (auto simp: frag_extend_diff)
+
+lemma frag_split:
+  fixes c :: "'a \<Rightarrow>\<^sub>0 int"
+  assumes "Poly_Mapping.keys c \<subseteq> S \<union> T"
+  obtains d e where "Poly_Mapping.keys d \<subseteq> S" "Poly_Mapping.keys e \<subseteq> T" "d + e = c"
+proof 
+  let ?d = "frag_extend (\<lambda>f. if f \<in> S then frag_of f else 0) c"
+  let ?e = "frag_extend (\<lambda>f. if f \<in> S then 0 else frag_of f) c"
+  show "Poly_Mapping.keys ?d \<subseteq> S" "Poly_Mapping.keys ?e \<subseteq> T"
+    using assms by (auto intro!: order_trans [OF keys_frag_extend] split: if_split_asm)
+  show "?d + ?e = c"
+    using assms
+  proof (induction c rule: frag_induction)
+    case (diff a b)
+    then show ?case
+      by (metis (no_types, lifting) frag_extend_diff add_diff_eq diff_add_eq diff_add_eq_diff_diff_swap)
+  qed auto
+qed
+
+hide_const (open) lookup single update keys range map map_key degree nth the_value items foldr mapp
+
+end
\ No newline at end of file
--- a/src/HOL/Product_Type.thy	Thu Apr 04 22:18:32 2019 +0200
+++ b/src/HOL/Product_Type.thy	Thu Apr 04 22:21:09 2019 +0200
@@ -1137,6 +1137,10 @@
 lemma Times_Int_Times: "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)"
   by auto
 
+lemma image_paired_Times:
+   "(\<lambda>(x,y). (f x, g y)) ` (A \<times> B) = (f ` A) \<times> (g ` B)"
+  by auto
+
 lemma product_swap: "prod.swap ` (A \<times> B) = B \<times> A"
   by (auto simp add: set_eq_iff)