# Theory Group_Extras

```text ‹Authors: Anthony Bordg and Lawrence Paulson›

theory Group_Extras
imports Main
"Jacobson_Basic_Algebra.Group_Theory"
"Set_Extras"

begin

section ‹Fold operator with a subdomain›

inductive_set
foldSetD :: "['a set, 'b ⇒ 'a ⇒ 'a, 'a] ⇒ ('b set * 'a) set"
for D :: "'a set" and f :: "'b ⇒ 'a ⇒ 'a" and e :: 'a
where
emptyI [intro]: "e ∈ D ⟹ ({}, e) ∈ foldSetD D f e"
| insertI [intro]: "⟦x ∉ A; f x y ∈ D; (A, y) ∈ foldSetD D f e⟧ ⟹
(insert x A, f x y) ∈ foldSetD D f e"

inductive_cases empty_foldSetDE [elim!]: "({}, x) ∈ foldSetD D f e"

definition
foldD :: "['a set, 'b ⇒ 'a ⇒ 'a, 'a, 'b set] ⇒ 'a"
where "foldD D f e A = (THE x. (A, x) ∈ foldSetD D f e)"

lemma foldSetD_closed: "(A, z) ∈ foldSetD D f e ⟹ z ∈ D"
by (erule foldSetD.cases) auto

lemma Diff1_foldSetD:
"⟦(A - {x}, y) ∈ foldSetD D f e; x ∈ A; f x y ∈ D⟧ ⟹
(A, f x y) ∈ foldSetD D f e"
by (metis Diff_insert_absorb foldSetD.insertI mk_disjoint_insert)

lemma foldSetD_imp_finite [simp]: "(A, x) ∈ foldSetD D f e ⟹ finite A"
by (induct set: foldSetD) auto

lemma finite_imp_foldSetD:
"⟦finite A; e ∈ D; ⋀x y. ⟦x ∈ A; y ∈ D⟧ ⟹ f x y ∈ D⟧
⟹ ∃x. (A, x) ∈ foldSetD D f e"
proof (induct set: finite)
case empty then show ?case by auto
next
case (insert x F)
then obtain y where y: "(F, y) ∈ foldSetD D f e" by auto
with insert have "y ∈ D" by (auto dest: foldSetD_closed)
with y and insert have "(insert x F, f x y) ∈ foldSetD D f e"
by (intro foldSetD.intros) auto
then show ?case ..
qed

lemma foldSetD_backwards:
assumes "A ≠ {}" "(A, z) ∈ foldSetD D f e"
shows "∃x y. x ∈ A ∧ (A - { x }, y) ∈ foldSetD D f e ∧ z = f x y"
using assms(2) by (cases) (simp add: assms(1), metis Diff_insert_absorb insertI1)

subsection ‹Left-Commutative Operations›

locale LCD =
fixes B :: "'b set"
and D :: "'a set"
and f :: "'b ⇒ 'a ⇒ 'a"    (infixl "⋅" 70)
assumes left_commute:
"⟦x ∈ B; y ∈ B; z ∈ D⟧ ⟹ x ⋅ (y ⋅ z) = y ⋅ (x ⋅ z)"
and f_closed [simp, intro!]: "!!x y. ⟦x ∈ B; y ∈ D⟧ ⟹ f x y ∈ D"

lemma (in LCD) foldSetD_closed [dest]: "(A, z) ∈ foldSetD D f e ⟹ z ∈ D"
by (erule foldSetD.cases) auto

lemma (in LCD) Diff1_foldSetD:
"⟦(A - {x}, y) ∈ foldSetD D f e; x ∈ A; A ⊆ B⟧ ⟹
(A, f x y) ∈ foldSetD D f e"
by (meson Diff1_foldSetD f_closed local.foldSetD_closed subsetCE)

lemma (in LCD) finite_imp_foldSetD:
"⟦finite A; A ⊆ B; e ∈ D⟧ ⟹ ∃x. (A, x) ∈ foldSetD D f e"
proof (induct set: finite)
case empty then show ?case by auto
next
case (insert x F)
then obtain y where y: "(F, y) ∈ foldSetD D f e" by auto
with insert have "y ∈ D" by auto
with y and insert have "(insert x F, f x y) ∈ foldSetD D f e"
by (intro foldSetD.intros) auto
then show ?case ..
qed

lemma (in LCD) foldSetD_determ_aux:
assumes "e ∈ D" and A: "card A < n" "A ⊆ B" "(A, x) ∈ foldSetD D f e" "(A, y) ∈ foldSetD D f e"
shows "y = x"
using A
proof (induction n arbitrary: A x y)
case 0
then show ?case
by auto
next
case (Suc n)
then consider "card A = n" | "card A < n"
by linarith
then show ?case
proof cases
case 1
show ?thesis
using foldSetD.cases [OF ‹(A,x) ∈ foldSetD D (⋅) e›]
proof cases
case 1
then show ?thesis
using ‹(A,y) ∈ foldSetD D (⋅) e› by auto
next
case (2 x' A' y')
note A' = this
show ?thesis
using foldSetD.cases [OF ‹(A,y) ∈ foldSetD D (⋅) e›]
proof cases
case 1
then show ?thesis
using ‹(A,x) ∈ foldSetD D (⋅) e› by auto
next
case (2 x'' A'' y'')
note A'' = this
show ?thesis
proof (cases "x' = x''")
case True
show ?thesis
proof (cases "y' = y''")
case True
then show ?thesis
using A' A'' ‹x' = x''› by (blast elim!: equalityE)
next
case False
then show ?thesis
using A' A'' ‹x' = x''›
by (metis ‹card A = n› Suc.IH Suc.prems(2) card_insert_disjoint foldSetD_imp_finite insert_eq_iff insert_subset lessI)
qed
next
case False
then have *: "A' - {x''} = A'' - {x'}" "x'' ∈ A'" "x' ∈ A''"
using A' A'' by fastforce+
then have "A' = insert x'' A'' - {x'}"
using ‹x' ∉ A'› by blast
then have card: "card A' ≤ card A''"
using A' A'' * by (metis card_Suc_Diff1 eq_refl foldSetD_imp_finite)
obtain u where u: "(A' - {x''}, u) ∈ foldSetD D (⋅) e"
using finite_imp_foldSetD [of "A' - {x''}"] A' Diff_insert ‹A ⊆ B› ‹e ∈ D› by fastforce
have "y' = f x'' u"
using Diff1_foldSetD [OF u] ‹x'' ∈ A'› ‹card A = n› A' Suc.IH ‹A ⊆ B› by auto
then have "(A'' - {x'}, u) ∈ foldSetD D f e"
using "*"(1) u by auto
then have "y'' = f x' u"
using A'' by (metis * ‹card A = n› A'(1) Diff1_foldSetD Suc.IH ‹A ⊆ B›
card card_Suc_Diff1 card_insert_disjoint foldSetD_imp_finite insert_subset le_imp_less_Suc)
then show ?thesis
using A' A''
by (metis ‹A ⊆ B› ‹y' = x'' ⋅ u› insert_subset left_commute local.foldSetD_closed u)
qed
qed
qed
next
case 2 with Suc show ?thesis by blast
qed
qed

lemma (in LCD) foldSetD_determ:
"⟦(A, x) ∈ foldSetD D f e; (A, y) ∈ foldSetD D f e; e ∈ D; A ⊆ B⟧
⟹ y = x"
by (blast intro: foldSetD_determ_aux [rule_format])

lemma (in LCD) foldD_equality:
"⟦(A, y) ∈ foldSetD D f e; e ∈ D; A ⊆ B⟧ ⟹ foldD D f e A = y"
by (unfold foldD_def) (blast intro: foldSetD_determ)

lemma foldD_empty [simp]:
"e ∈ D ⟹ foldD D f e {} = e"
by (unfold foldD_def) blast

lemma (in LCD) foldD_insert_aux:
"⟦x ∉ A; x ∈ B; e ∈ D; A ⊆ B⟧
⟹ ((insert x A, v) ∈ foldSetD D f e) ⟷ (∃y. (A, y) ∈ foldSetD D f e ∧ v = f x y)"
apply auto
by (metis Diff_insert_absorb f_closed finite_Diff foldSetD.insertI foldSetD_determ foldSetD_imp_finite insert_subset local.finite_imp_foldSetD local.foldSetD_closed)

lemma (in LCD) foldD_insert:
assumes "finite A" "x ∉ A" "x ∈ B" "e ∈ D" "A ⊆ B"
shows "foldD D f e (insert x A) = f x (foldD D f e A)"
proof -
have "(THE v. ∃y. (A, y) ∈ foldSetD D (⋅) e ∧ v = x ⋅ y) = x ⋅ (THE y. (A, y) ∈ foldSetD D (⋅) e)"
by (rule the_equality) (use assms foldD_def foldD_equality foldD_def finite_imp_foldSetD in ‹metis+›)
then show ?thesis
unfolding foldD_def using assms by (simp add: foldD_insert_aux)
qed

lemma (in LCD) foldD_closed [simp]:
"⟦finite A; e ∈ D; A ⊆ B⟧ ⟹ foldD D f e A ∈ D"
proof (induct set: finite)
case empty then show ?case by simp
next
case insert then show ?case by (simp add: foldD_insert)
qed

lemma (in LCD) foldD_commute:
"⟦finite A; x ∈ B; e ∈ D; A ⊆ B⟧ ⟹
f x (foldD D f e A) = foldD D f (f x e) A"
by (induct set: finite) (auto simp add: left_commute foldD_insert)

lemma Int_mono2:
"⟦A ⊆ C; B ⊆ C⟧ ⟹ A Int B ⊆ C"
by blast

lemma (in LCD) foldD_nest_Un_Int:
"⟦finite A; finite C; e ∈ D; A ⊆ B; C ⊆ B⟧ ⟹
foldD D f (foldD D f e C) A = foldD D f (foldD D f e (A Int C)) (A Un C)"
proof (induction set: finite)
case (insert x F)
then show ?case
by (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb Int_mono2)
qed simp

lemma (in LCD) foldD_nest_Un_disjoint:
"⟦finite A; finite B; A Int B = {}; e ∈ D; A ⊆ B; C ⊆ B⟧
⟹ foldD D f e (A Un B) = foldD D f (foldD D f e B) A"

― ‹Delete rules to do with ‹foldSetD› relation.›

declare foldSetD_imp_finite [simp del]
empty_foldSetDE [rule del]
foldSetD.intros [rule del]
declare (in LCD)
foldSetD_closed [rule del]

section ‹Monoids›

lemma comp_monoid_morphisms:
assumes "monoid_homomorphism η A multA oneA B multB oneB" and
"monoid_homomorphism θ B multB oneB C multC oneC"
shows "monoid_homomorphism (θ ∘ η ↓ A) A multA oneA C multC oneC"
proof-
have "map (θ ∘ η ↓ A) A C" using assms comp_maps by (metis monoid_homomorphism.axioms(1))
moreover have "(θ ∘ η ↓ A) oneA = oneC"
using assms
by (metis compose_eq monoid.unit_closed monoid_homomorphism.axioms(2) monoid_homomorphism.commutes_with_unit)
moreover have "(θ ∘ η ↓ A) (multA x y) = multC ((θ ∘ η ↓ A) x) ((θ ∘ η ↓ A) y)"
if "x ∈ A" "y ∈ A" for x y
using that assms monoid_homomorphism.commutes_with_composition
by (smt compose_eq map.map_closed monoid.composition_closed monoid_homomorphism.axioms)
ultimately show ?thesis
using monoid_homomorphism_def assms comp_maps by (smt monoid_homomorphism_axioms.intro)
qed

text ‹Commutative Monoids›

text ‹
We enter a more restrictive context, with ‹f :: 'a ⇒ 'a ⇒ 'a›
instead of ‹'b ⇒ 'a ⇒ 'a›.
›

locale ACeD =
fixes D :: "'a set"
and f :: "'a ⇒ 'a ⇒ 'a"    (infixl "⋅" 70)
and e :: 'a
assumes ident [simp]: "x ∈ D ⟹ x ⋅ e = x"
and commute: "⟦x ∈ D; y ∈ D⟧ ⟹ x ⋅ y = y ⋅ x"
and assoc: "⟦x ∈ D; y ∈ D; z ∈ D⟧ ⟹ (x ⋅ y) ⋅ z = x ⋅ (y ⋅ z)"
and e_closed [simp]: "e ∈ D"
and f_closed [simp]: "⟦x ∈ D; y ∈ D⟧ ⟹ x ⋅ y ∈ D"

lemma (in ACeD) left_commute:
"⟦x ∈ D; y ∈ D; z ∈ D⟧ ⟹ x ⋅ (y ⋅ z) = y ⋅ (x ⋅ z)"
proof -
assume D: "x ∈ D" "y ∈ D" "z ∈ D"
then have "x ⋅ (y ⋅ z) = (y ⋅ z) ⋅ x" by (simp add: commute)
also from D have "... = y ⋅ (z ⋅ x)" by (simp add: assoc)
also from D have "z ⋅ x = x ⋅ z" by (simp add: commute)
finally show ?thesis .
qed

lemmas (in ACeD) AC = assoc commute left_commute

lemma (in ACeD) left_ident [simp]: "x ∈ D ⟹ e ⋅ x = x"
proof -
assume "x ∈ D"
then have "x ⋅ e = x" by (rule ident)
with ‹x ∈ D› show ?thesis by (simp add: commute)
qed

lemma (in ACeD) foldD_Un_Int:
"⟦finite A; finite B; A ⊆ D; B ⊆ D⟧ ⟹
foldD D f e A ⋅ foldD D f e B =
foldD D f e (A Un B) ⋅ foldD D f e (A Int B)"
proof (induction set: finite)
case empty
then show ?case
by(simp add: left_commute LCD.foldD_closed [OF LCD.intro [of D]])
next
case (insert x F)
then show ?case
by(simp add: AC insert_absorb Int_insert_left Int_mono2
LCD.foldD_insert [OF LCD.intro [of D]]
LCD.foldD_closed [OF LCD.intro [of D]])
qed

lemma (in ACeD) foldD_Un_disjoint:
"⟦finite A; finite B; A Int B = {}; A ⊆ D; B ⊆ D⟧ ⟹
foldD D f e (A Un B) = foldD D f e A ⋅ foldD D f e B"
left_commute LCD.foldD_closed [OF LCD.intro [of D]])

subsection ‹Finite Products›

context monoid
begin

definition finprod:: "'b set => ('b => 'a) ⇒ 'a"
where "finprod I f ≡ if finite I then foldD M (composition ∘ f) 𝟭 I else 𝟭"

end (* monoid *)

section ‹Groups›

lemma comp_group_morphisms:
assumes "group_homomorphism η A multA oneA B multB oneB" and
"group_homomorphism θ B multB oneB C multC oneC"
shows "group_homomorphism (θ ∘ η ↓ A) A multA oneA C multC oneC"
using assms group_homomorphism_def comp_monoid_morphisms by metis

subsection ‹Subgroup Generated by a Subset›

context group
begin

inductive_set generate :: "'a set ⇒ 'a set"
for H where
unit:  "𝟭 ∈ generate H"
| incl: "a ∈ H ⟹ a ∈ generate H"
| inv:  "a ∈ H ⟹ inverse a ∈ generate H"
| mult:  "a ∈ generate H ⟹ b ∈ generate H ⟹ a ⋅ b ∈ generate H"

lemma generate_into_G: "a ∈ generate (G ∩ H) ⟹ a ∈ G"
by (induction rule: generate.induct) auto

definition subgroup_generated :: "'a set ⇒ 'a set"
where "subgroup_generated S = generate (G ∩ S)"

lemma inverse_in_subgroup_generated: "a ∈ subgroup_generated H ⟹ inverse a ∈ subgroup_generated H"
unfolding subgroup_generated_def
proof (induction rule: generate.induct)
case (mult a b)
then show ?case
by (simp add: generate.mult generate_into_G inverse_composition_commute)
qed (auto simp add: generate.unit generate.incl generate.inv)

lemma subgroup_generated_is_monoid:
fixes H
shows "Group_Theory.monoid (subgroup_generated H) (⋅) 𝟭"
unfolding subgroup_generated_def
proof qed (auto simp: generate.unit generate.mult associative generate_into_G)

lemma subgroup_generated_is_subset:
fixes H
shows "subgroup_generated H ⊆ G"
using generate_into_G subgroup_generated_def by blast

lemma subgroup_generated_is_subgroup:
fixes H
shows "subgroup (subgroup_generated H) G (⋅) 𝟭"
proof
show "subgroup_generated H ⊆ G"
show "a ⋅ b ∈ subgroup_generated H"
if "a ∈ subgroup_generated H" "b ∈ subgroup_generated H" for a b
using that by (meson monoid.composition_closed subgroup_generated_is_monoid)
show "a ⋅ b ⋅ c = a ⋅ (b ⋅ c)"
if "a ∈ subgroup_generated H" "b ∈ subgroup_generated H" "c ∈ subgroup_generated H"
for a b c
using that by (meson monoid.associative subgroup_generated_is_monoid)
show "monoid.invertible (subgroup_generated H) (⋅) 𝟭 u"
if "u ∈ subgroup_generated H" for u
proof (rule monoid.invertibleI )
show "Group_Theory.monoid (subgroup_generated H) (⋅) 𝟭"
show "u ⋅ local.inverse u = 𝟭" "local.inverse u ⋅ u = 𝟭" "u ∈ subgroup_generated H"
using ‹subgroup_generated H ⊆ G› that by auto
show "local.inverse u ∈ subgroup_generated H"
using inverse_in_subgroup_generated that by blast
qed
qed (auto simp: generate_into_G generate.unit subgroup_generated_def)

end (* group *)

section ‹Abelian Groups›

context abelian_group
begin

definition minus:: "'a ⇒ 'a ⇒ 'a" (infixl "‐" 70)
where "x ‐ y ≡ x ⋅ inverse y "

definition finsum:: "'b set ⇒ ('b ⇒ 'a) ⇒ 'a"
where "finsum I f ≡ finprod I f"

(* A notation "∑i∈I. f i" should be introduced for a sum of a family of elements of an abelian group *)

end (* abelian_group*)

end
```