# Theory Algebra

```section ‹Algebra›

text ‹
In this section, we develop the necessary algebra for developing the theory of Coxeter systems,
including groups, quotient groups, free groups, group presentations, and words in a group over a
set of generators.
›

theory Algebra
imports Prelim

begin

subsection ‹Miscellaneous algebra facts›

lemma times2_conv_add: "(j::nat) + j = 2*j"
by (induct j) auto

lemma (in comm_semiring_1) odd_n0: "odd m ⟹ m≠0"
using dvd_0_right by fast

lemma (in semigroup_add) add_assoc4: "a + b + c + d = a + (b + c + d)"

arg_cong[OF map_cong, OF refl, of _ _ _ sum_list]

begin

lemma map_uminus_order2:
"∀s∈set ss. s+s=0 ⟹ map (uminus) ss = ss"
by (induct ss) (auto simp add: minus_unique)

lemma uminus_sum_list: "- sum_list as = sum_list (map uminus (rev as))"

lemma uminus_sum_list_order2:
"∀s∈set ss. s+s=0 ⟹ - sum_list ss = sum_list (rev ss)"
using uminus_sum_list map_uminus_order2 by simp

subsection ‹The type of permutations of a type›

text ‹
Here we construct a type consisting of all bijective functions on a type. This is the
prototypical example of a group, where the group operation is composition, and every group can
be embedded into such a type. It is for this purpose that we construct this type, so that we may
confer upon suitable subsets of types that are not of class @{class group_add} the properties of
that class, via a suitable injective correspondence to this permutation type.
›

typedef 'a permutation = "{f::'a⇒'a. bij f}"
morphisms permutation Abs_permutation
by fast

setup_lifting type_definition_permutation

abbreviation permutation_apply :: "'a permutation ⇒ 'a ⇒ 'a " (infixr "→" 90)
where "p → a ≡ permutation p a"
abbreviation permutation_image :: "'a permutation ⇒ 'a set ⇒ 'a set"
(infixr "`→" 90)
where "p `→ A ≡ permutation p ` A"

lemma permutation_eq_image: "a `→ A = a `→ B ⟹ A=B"
using permutation[of a] inj_eq_image[OF bij_is_inj] by auto

instantiation permutation :: (type) zero
begin
lift_definition zero_permutation :: "'a permutation" is "id::'a⇒'a" by simp
instance ..
end

instantiation permutation :: (type) plus
begin
lift_definition plus_permutation :: "'a permutation ⇒ 'a permutation ⇒ 'a permutation"
is    "comp"
using bij_comp
by    fast
instance ..
end

lemma plus_permutation_abs_eq:
"bij f ⟹ bij g ⟹
Abs_permutation f + Abs_permutation g = Abs_permutation (f∘g)"

proof
fix a b c :: "'a permutation" show "a + b + c = a + (b + c)"
using comp_assoc[of "permutation a" "permutation b" "permutation c"]
by    transfer simp
qed

proof
fix a :: "'a permutation"
show "0 + a = a" by transfer simp
show "a + 0 = a" by transfer simp
qed

instantiation permutation :: (type) uminus
begin
lift_definition uminus_permutation :: "'a permutation ⇒ 'a permutation"
is    "λf. the_inv f"
using bij_betw_the_inv_into
by    fast
instance ..
end

instantiation permutation :: (type) minus
begin
lift_definition minus_permutation :: "'a permutation ⇒ 'a permutation ⇒ 'a permutation"
is    "λf g. f ∘ (the_inv g)"
using bij_betw_the_inv_into bij_comp
by    fast
instance ..
end

lemma minus_permutation_abs_eq:
"bij f ⟹ bij g ⟹
Abs_permutation f - Abs_permutation g = Abs_permutation (f ∘ the_inv g)"

proof
fix a b :: "'a permutation"
show "- a + a = 0" using the_inv_leftinv[of "permutation a"] by transfer simp
show "a + - b = a - b" by transfer simp
qed

subsection ‹Natural action of @{typ nat} on types of class @{class monoid_add}›

subsubsection ‹Translation from class @{class power}.›

text ‹
Here we translate the @{class power} class to apply to types of class @{class monoid_add}.
›

begin

sublocale nataction: power 0 plus .

abbreviation nataction :: "'a ⇒ nat ⇒ 'a" (infix "+^" 80)
where "a+^n  ≡ nataction.power a n"

lemma alternating_sum_list_conv_nataction:
"sum_list (alternating_list (2*n) s t) = (s+t)+^n"
by (induct n) (auto simp add: nataction_Suc2[THEN sym])

lemma nataction_add_flip: "(a+b)+^(Suc n) = a + (b+a)+^n + b"
using nataction_Suc2 add.assoc by (induct n arbitrary: a b) auto

assumes "(a+b)+^n = 0"
shows   "(b+a)+^n = 0"
proof (cases n)
case (Suc k) with assms show ?thesis
qed simp

subsubsection ‹Additive order of an element›

begin

definition add_order :: "'a ⇒ nat"
where "add_order a ≡ if (∃n>0. a+^n = 0) then
(LEAST n. n>0 ∧ a+^n = 0) else 0"

using LeastI_ex[of "λn. n>0 ∧ a+^n = 0"] add_order_def by simp

lemma add_order_least: "n>0 ⟹ a+^n = 0 ⟹ add_order a ≤ n"
using Least_le[of "λn. n>0 ∧ a+^n = 0"] add_order_def by simp

"⟦ n>0; a+^n = 0; (⋀m. m>0 ⟹ a+^m = 0 ⟹ n≤m) ⟧ ⟹
using Least_equality[of "λn. n>0 ∧ a+^n = 0"] add_order_def by auto

using LeastI_ex[of "λn. n>0 ∧ a+^n = 0"] add_order_def by simp

lemma add_order_eq0: "add_order a = 0 ⟹ n>0 ⟹ a+^n ≠ 0"

assumes "a+^k = 0" "k < add_order a"
shows   "k = 0"
proof (cases "k=0")
case False
moreover with assms(1) have "∃n>0. a+^n = 0" by fast
ultimately show ?thesis
using assms add_order_def not_less_Least[of k "λn. n>0 ∧ a+^n = 0"]
by    auto
qed simp

lemma less_add_order_eq_0_contra: "k>0 ⟹ k < add_order a ⟹ a+^k ≠ 0"

abbreviation pair_relator_list :: "'a ⇒ 'a ⇒ 'a list"
where "pair_relator_list s t ≡ alternating_list (2*add_order (s+t)) s t"
abbreviation pair_relator_halflist :: "'a ⇒ 'a ⇒ 'a list"
where "pair_relator_halflist s t ≡ alternating_list (add_order (s+t)) s t"
abbreviation pair_relator_halflist2 :: "'a ⇒ 'a ⇒ 'a list"
where "pair_relator_halflist2 s t ≡
(if even (add_order (s+t)) then pair_relator_halflist s t else
pair_relator_halflist t s)"

lemma sum_list_pair_relator_list: "sum_list (pair_relator_list s t) = 0"

begin

proof (cases "add_order (t+s) = 0" "add_order (s+t) = 0" rule: two_cases)
case one thus ?thesis
next
case other thus ?thesis
next
case neither thus ?thesis
by fastforce
qed simp

lemma pair_relator_halflist_append:
"pair_relator_halflist s t @ pair_relator_halflist2 s t = pair_relator_list s t"

lemma rev_pair_relator_list: "rev (pair_relator_list s t) = pair_relator_list t s"

lemma pair_relator_halflist2_conv_rev_pair_relator_halflist:
"pair_relator_halflist2 s t = rev (pair_relator_halflist t s)"

subsection ‹Partial sums of a list›

text ‹
Here we construct a list that collects the results of adding the elements of a given list
together one-by-one.
›

begin

primrec sums :: "'a list ⇒ 'a list"
where
"sums [] = [0]"
| "sums (x#xs) = 0 # map ((+) x) (sums xs)"

lemma length_sums: "length (sums xs) = Suc (length xs)"
by (induct xs) auto

lemma sums_snoc: "sums (xs@[x]) = sums xs @ [sum_list (xs@[x])]"

lemma sums_append2:
"sums (xs@ys) = butlast (sums xs) @ map ((+) (sum_list xs)) (sums ys)"
proof (induct ys rule: rev_induct)
case Nil show ?case by (cases xs rule: rev_cases) (auto simp add: sums_snoc)
next
case (snoc y ys) thus ?case using sums_snoc[of "xs@ys"] by (simp add: sums_snoc)
qed

lemma sums_Cons_conv_append_tl:
"sums (x#xs) = 0 # x # map ((+) x) (tl (sums xs))"
by (cases xs) auto

lemma pullback_sums_map_middle2:
"map F (sums xs) = ds@[d,e]@es ⟹
∃as a bs. xs = as@[a]@bs ∧ map F (sums as) = ds@[d] ∧
d = F (sum_list as) ∧ e = F (sum_list (as@[a]))"
proof (induct xs es rule: list_induct2_snoc)
case (Nil2 xs)
show ?case
proof (cases xs rule: rev_cases)
case Nil with Nil2 show ?thesis by simp
next
case (snoc ys y) have ys: "xs = ys@[y]" by fact
with Nil2(1) have y: "map F (sums ys) = ds@[d]" "e = F (sum_list (ys@[y]))"
show ?thesis
proof (cases ys rule: rev_cases)
case Nil
with ys y have
"xs = []@[y]@[]" "map F (sums []) = ds@[d]"
"d = F (sum_list [])" "e = F (sum_list ([]@[y]))"
by auto
thus ?thesis by fast
next
case (snoc zs z)
with y(1) have z: "map F (sums zs) = ds" "d = F (sum_list (zs@[z]))"
from z(1) ys y snoc have
"xs = (zs@[z])@[y]@[]" "map F (sums (zs@[z])) = ds@[d]"
"e = F (sum_list ((zs@[z])@[y]))"
by auto
with z(2) show ?thesis by fast
qed
qed
next
case snoc thus ?case by (fastforce simp add: sums_snoc)
qed simp

lemma pullback_sums_map_middle3:
"map F (sums xs) = ds@[d,e,f]@fs ⟹
∃as a b bs. xs = as@[a,b]@bs ∧ d = F (sum_list as) ∧
e = F (sum_list (as@[a])) ∧ f = F (sum_list (as@[a,b]))"
proof (induct xs fs rule: list_induct2_snoc)
case (Nil2 xs)
show ?case
proof (cases xs rule: rev_cases)
case Nil with Nil2 show ?thesis by simp
next
case (snoc ys y)
with Nil2 have y: "map F (sums ys) = ds@[d,e]" "f = F (sum_list (ys@[y]))"
from y(1) obtain as a bs where asabs:
"ys = as@[a]@bs" "map F (sums as) = ds@[d]"
"d = F (sum_list as)" "e = F (sum_list (as@[a]))"
using pullback_sums_map_middle2[of F ys ds]
by    fastforce
have "bs = []"
proof-
from y(1) asabs(1,2) have "Suc (length bs) = Suc 0"
by (auto simp add: sums_append2 map_butlast length_sums[THEN sym])
thus ?thesis by fast
qed
with snoc asabs(1) y(2) have "xs = as@[a,y]@[]" "f = F (sum_list (as@[a,y]))"
by auto
with asabs(3,4) show ?thesis by fast
qed
next
case snoc thus ?case by (fastforce simp add: sums_snoc)
qed simp

lemma pullback_sums_map_double_middle2:
assumes "map F (sums xs) = ds@[d,e]@es@[f,g]@gs"
shows   "∃as a bs b cs. xs = as@[a]@bs@[b]@cs ∧ d = F (sum_list as) ∧
e = F (sum_list (as@[a])) ∧ f = F (sum_list (as@[a]@bs)) ∧
g = F (sum_list (as@[a]@bs@[b]))"
proof-
from assms obtain As b cs where Asbcs:
"xs = As@[b]@cs" "map F (sums As) = ds@[d,e]@es@[f]"
"f = F (sum_list As)" "g = F (sum_list (As@[b]))"
using pullback_sums_map_middle2[of F xs "ds@[d,e]@es"]
by    fastforce
from Asbcs show ?thesis
using pullback_sums_map_middle2[of F As ds d e "es@[f]"] by fastforce
qed

subsection ‹Sums of alternating lists›

"s+s=0 ⟹ t+t=0 ⟹ - sum_list (alternating_list n s t) =
sum_list (if even n then alternating_list n t s else alternating_list n s t)"
using uminus_sum_list_order2 set_alternating_list[of n] rev_alternating_list[of n s]
by    fastforce

begin

lemma alternating_order2_cancel_1left:
"s+s=0 ⟹
sum_list (s # (alternating_list (Suc n) s t)) = sum_list (alternating_list n t s)"
using add.assoc[of s s] alternating_list_Suc_Cons[of n s] by simp

lemma alternating_order2_cancel_2left:
"s+s=0 ⟹ t+t=0 ⟹
sum_list (t # s # (alternating_list (Suc (Suc n)) s t)) =
sum_list (alternating_list n s t)"
using alternating_order2_cancel_1left[of s "Suc n"]
alternating_order2_cancel_1left[of t n]
by    simp

lemma alternating_order2_even_cancel_right:
assumes st    : "s+s=0" "t+t=0"
and     even_n: "even n"
shows   "m ≤ n ⟹ sum_list (alternating_list n s t @ alternating_list m t s) =
sum_list (alternating_list (n-m) s t)"
proof (induct n arbitrary: m rule: nat_even_induct, rule even_n)
case (SucSuc k) with st show ?case
using alternating_order2_cancel_2left[of t s]
by    (cases m rule: nat_cases_2Suc) auto
qed simp

subsubsection ‹Abbreviations and basic facts›

begin

abbreviation lconjby :: "'a⇒'a⇒'a"
where "lconjby x y ≡ x+y-x"

abbreviation rconjby :: "'a⇒'a⇒'a"
where "rconjby x y ≡ -x+y+x"

lemma lconjby_add: "lconjby (x+y) z = lconjby x (lconjby y z)"

lemma rconjby_add: "rconjby (x+y) z = rconjby y (rconjby x z)"

lemma add_rconjby: "rconjby x y + rconjby x z = rconjby x (y+z)"

lemma lconjby_uminus: "lconjby x (-y) = - lconjby x y"
using minus_unique[of "lconjby x y", THEN sym] by (simp add: algebra_simps)

lemma rconjby_uminus: "rconjby x (-y) = - rconjby x y"
using minus_unique[of "rconjby x y"] add_assoc4[of "rconjby x y" "-x" "-y" x] by simp

lemma lconjby_rconjby: "lconjby x (rconjby x y) = y"

lemma rconjby_lconjby: "rconjby x (lconjby x y) = y"

lemma lconjby_inj: "inj (lconjby x)"
using rconjby_lconjby by (fast intro: inj_on_inverseI)

lemma rconjby_inj: "inj (rconjby x)"
using lconjby_rconjby by (fast intro: inj_on_inverseI)

lemma lconjby_surj: "surj (lconjby x)"
using lconjby_rconjby surjI[of "lconjby x"] by fast

lemma lconjby_bij: "bij (lconjby x)"
unfolding bij_def using lconjby_inj lconjby_surj by fast

lemma the_inv_lconjby: "the_inv (lconjby x) = (rconjby x)"
using bij_betw_f_the_inv_into_f[OF lconjby_bij, of _ x] lconjby_rconjby
by    (force intro: inj_onD[OF lconjby_inj, of x])

lemma lconjby_eq_conv_rconjby_eq: "w = lconjby x y ⟹ y = rconjby x w"
using the_inv_lconjby the_inv_into_f_f[OF lconjby_inj] by force

lemma rconjby_order2: "s+s = 0 ⟹ rconjby x s + rconjby x s = 0"

lemma rconjby_order2_eq_lconjby:
assumes "s+s=0"
shows   "rconjby s = lconjby s"
proof-
have "rconjby s = lconjby (-s)" by simp
with assms show ?thesis using minus_unique by simp
qed

lemma lconjby_alternating_list_order2:
assumes "s+s=0" "t+t=0"
shows   "lconjby (sum_list (alternating_list k s t)) (if even k then s else t) =
sum_list (alternating_list (Suc (2*k)) s t)"
proof (induct k rule: nat_induct_step2)
case (SucSuc m)
have "lconjby (sum_list (alternating_list (Suc (Suc m)) s t))
(if even (Suc (Suc m)) then s else t) = s + t +
lconjby (sum_list (alternating_list m s t)) (if even m then s else t) - t - s"
using alternating_list_SucSuc_ConsCons[of m s t]
also from assms SucSuc
have  "… = sum_list (alternating_list (Suc (2*Suc (Suc m))) s t)"
using alternating_list_SucSuc_ConsCons[of "Suc (2*m)" s t]
sum_list.append[of "alternating_list (Suc (2*Suc m)) s t" "[t]"]
finally show ?case by fast
qed (auto simp add: assms(1) algebra_simps)

subsubsection ‹The conjugation sequence›

text ‹
Given a list in @{class group_add}, we create a new list by conjugating each term by all the
previous terms. This sequence arises in Coxeter systems.
›

begin

primrec lconjseq :: "'a list ⇒ 'a list"
where
"lconjseq []     = []"
| "lconjseq (x#xs) = x # (map (lconjby x) (lconjseq xs))"

lemma length_lconjseq: "length (lconjseq xs) = length xs"
by (induct xs) auto

lemma lconjseq_snoc: "lconjseq (xs@[x]) = lconjseq xs @ [lconjby (sum_list xs) x]"

lemma lconjseq_append:
"lconjseq (xs@ys) = lconjseq xs @ (map (lconjby (sum_list xs)) (lconjseq ys))"
proof (induct ys rule: rev_induct)
case (snoc y ys) thus ?case
qed simp

lemma lconjseq_alternating_order2_repeats':
fixes   s t :: 'a
defines altst: "altst ≡ λn. alternating_list n s t"
and     altts: "altts ≡ λn. alternating_list n t s"
assumes st   : "s+s=0" "t+t=0" "(s+t)+^k = 0"
shows   "map (lconjby (sum_list (altst k)))
(lconjseq (if even k then altst m else altts m)) = lconjseq (altst m)"
proof (induct m)
case (Suc j)
with altst altts
have  "map (lconjby (sum_list (altst k)))
(lconjseq (if even k then altst (Suc j) else altts (Suc j))) =
lconjseq (altst j) @
[lconjby (sum_list (altst k @ (if even k then altst j else altts j)))
(if even k then (if even j then s else t) else (if even j then t else s))]"
also from altst altts st(1,2)
have  "… = lconjseq (altst j) @ [sum_list (altst (Suc (2*(k+j))))]"
using lconjby_alternating_list_order2[of s t "k+j"]
by    (cases "even k")
finally show ?case using altst st
alternating_list_append(1)[THEN sym]
alternating_sum_list_conv_nataction
lconjby_alternating_list_order2 lconjseq_snoc
)

lemma lconjseq_alternating_order2_repeats:
fixes   s t :: 'a and k :: nat
defines altst: "altst ≡ λn. alternating_list n s t"
and     altts: "altts ≡ λn. alternating_list n t s"
assumes st: "s+s=0" "t+t=0" "(s+t)+^k = 0"
shows   "lconjseq (altst (2*k)) = lconjseq (altst k) @ lconjseq (altst k)"
proof-
from altst altts
have "lconjseq (altst (2*k)) = lconjseq (altst k) @
map (lconjby (sum_list (altst k)))
(lconjseq (if even k then altst k else altts k))"
using alternating_list_append[THEN sym, of k k s t]
with altst altts st show ?thesis
using lconjseq_alternating_order2_repeats'[of s t k k] by auto
qed

lemma even_count_lconjseq_alternating_order2:
fixes   s t :: 'a
assumes "s+s=0" "t+t=0" "(s+t)+^k = 0"
shows   "even (count_list (lconjseq (alternating_list (2*k) s t)) x)"
proof-
define xs where xs: "xs ≡ lconjseq (alternating_list (2*k) s t)"
with assms obtain as where "xs = as@as"
using lconjseq_alternating_order2_repeats by fast
hence "count_list xs x = 2 * (count_list as x)"
with xs show ?thesis by simp
qed

lemma order2_hd_in_lconjseq_deletion:
shows "s+s=0 ⟹ s ∈ set (lconjseq ss)
⟹ ∃as b bs. ss = as@[b]@bs ∧ sum_list (s#ss) = sum_list (as@bs)"
proof (induct ss arbitrary: s rule: rev_induct)
case (snoc t ts) show ?case
proof (cases "s ∈ set (lconjseq ts)")
case True
with snoc(1,2) obtain as b bs
where   asbbs: "ts = as @[b]@bs" "sum_list (s#ts) = sum_list (as@bs)"
by      fastforce
from asbbs(2) have "sum_list (s#ts@[t]) = sum_list (as@(bs@[t]))"
using sum_list.append[of "s#ts" "[t]"] sum_list.append[of "as@bs" "[t]"] by simp
with asbbs(1) show ?thesis by fastforce
next
case False
with snoc(3) have s: "s = lconjby (sum_list ts) t" by (simp add: lconjseq_snoc)
with snoc(2) have "t+t=0"
using lconjby_eq_conv_rconjby_eq[of s "sum_list ts" t]
rconjby_order2[of s "sum_list ts"]
by    simp
moreover from s have "sum_list (s#ts@[t]) = sum_list ts + t + t"
using add.assoc[of "sum_list ts + t - sum_list ts" "sum_list ts"]
ultimately have "sum_list (s#ts@[t]) = sum_list (ts@[])"
thus ?thesis by fast
qed
qed simp

subsubsection ‹The action on signed @{class group_add} elements›

text ‹
Here we construct an action of a group on itself by conjugation, where group elements are
endowed with an auxiliary sign by pairing with a boolean element. In multiple applications of
this action, the auxiliary sign helps keep track of how many times the elements conjugating and
being conjugated are the same. This action arises in exploring reduced expressions of group
elements as words in a set of generators of order two (in particular, in a Coxeter group).
›

type_synonym 'a signed = "'a×bool"

definition signed_funaction :: "('a⇒'a⇒'a) ⇒ 'a ⇒ 'a signed ⇒ 'a signed"
where "signed_funaction f s x ≡ map_prod (f s) (λb. b ≠ (fst x = s)) x"
― ‹so the sign of @{term x} is flipped precisely when its first component is equal to
@{term s}›

begin

abbreviation "signed_lconjaction ≡ signed_funaction lconjby"
abbreviation "signed_rconjaction ≡ signed_funaction rconjby"

lemmas signed_lconjactionD = signed_funaction_def[of lconjby]
lemmas signed_rconjactionD = signed_funaction_def[of rconjby]

abbreviation signed_lconjpermutation :: "'a ⇒ 'a signed permutation"
where "signed_lconjpermutation s ≡ Abs_permutation (signed_lconjaction s)"

abbreviation signed_list_lconjaction :: "'a list ⇒ 'a signed ⇒ 'a signed"
where "signed_list_lconjaction ss ≡ foldr signed_lconjaction ss"

lemma signed_lconjaction_fst: "fst (signed_lconjaction s x) = lconjby s (fst x)"
using signed_lconjactionD by simp

lemma signed_lconjaction_rconjaction:
"signed_lconjaction s (signed_rconjaction s x) = x"
proof-
obtain a::'a and b::bool where "x = (a,b)" by fastforce
thus ?thesis
using signed_lconjactionD signed_rconjactionD injD[OF rconjby_inj, of s a]
lconjby_rconjby[of s a]
by    auto
qed

lemma signed_rconjaction_by_order2_eq_lconjaction:
"s+s=0 ⟹ signed_rconjaction s = signed_lconjaction s"
using signed_funaction_def[of lconjby s] signed_funaction_def[of rconjby s]
rconjby_order2_eq_lconjby[of s]
by    auto

lemma inj_signed_lconjaction: "inj (signed_lconjaction s)"
proof (rule injI)
fix x y assume 1: "signed_lconjaction s x = signed_lconjaction s y"
moreover obtain a1 a2 :: 'a and b1 b2 :: bool
where xy: "x = (a1,b1)" "y = (a2,b2)"
by    fastforce
ultimately show "x=y"
using injD[OF lconjby_inj, of s a1 a2] signed_lconjactionD
by    (cases "a1=s" "a2=s" rule: two_cases) auto
qed

lemma surj_signed_lconjaction: "surj (signed_lconjaction s)"
using signed_lconjaction_rconjaction[THEN sym] by fast

lemma bij_signed_lconjaction: "bij (signed_lconjaction s)"
using inj_signed_lconjaction surj_signed_lconjaction by (fast intro: bijI)

lemma the_inv_signed_lconjaction:
"the_inv (signed_lconjaction s) = signed_rconjaction s"
proof
fix x
show "the_inv (signed_lconjaction s) x = signed_rconjaction s x"
proof (rule the_inv_into_f_eq, rule inj_signed_lconjaction)
show "signed_lconjaction s (signed_rconjaction s x) = x"
using signed_lconjaction_rconjaction by fast
qed

lemma the_inv_signed_lconjaction_by_order2:
"s+s=0 ⟹ the_inv (signed_lconjaction s) = signed_lconjaction s"
using the_inv_signed_lconjaction signed_rconjaction_by_order2_eq_lconjaction
by    simp

lemma signed_list_lconjaction_fst:
"fst (signed_list_lconjaction ss x) = lconjby (sum_list ss) (fst x)"
using signed_lconjaction_fst lconjby_add by (induct ss) auto

lemma signed_list_lconjaction_snd:
shows "∀s∈set ss. s+s=0 ⟹ snd (signed_list_lconjaction ss x)
= (if even (count_list (lconjseq (rev ss)) (fst x)) then snd x else ¬snd x)"
proof (induct ss)
case (Cons s ss) hence prevcase:
"snd (signed_list_lconjaction ss x) =
(if even (count_list (lconjseq (rev ss)) (fst x)) then snd x else ¬ snd x)"
by simp
have 1: "snd (signed_list_lconjaction (s # ss) x) =
snd (signed_lconjaction s (signed_list_lconjaction ss x))"
by simp
show ?case
proof (cases "fst (signed_list_lconjaction ss x) = s")
case True
with 1 prevcase
have  "snd (signed_list_lconjaction (s # ss) x) =
(if even (count_list (lconjseq (rev ss)) (fst x)) then ¬ snd x else snd x)"
with True Cons(2) rconjby_lconjby show ?thesis
by    (auto simp add: signed_list_lconjaction_fst lconjseq_snoc
simp flip: uminus_sum_list_order2
)
next
case False
hence "rconjby (sum_list ss) (lconjby (sum_list ss) (fst x)) ≠
rconjby (sum_list ss) s"
with Cons(2)
have  "count_list (lconjseq (rev (s#ss))) (fst x) =
count_list (lconjseq (rev ss)) (fst x)"
rconjby_lconjby uminus_sum_list_order2[THEN sym]
lconjseq_snoc
)
moreover from False 1 prevcase
have "snd (signed_list_lconjaction (s # ss) x) =
(if even (count_list (lconjseq (rev ss)) (fst x)) then snd x else ¬ snd x)"
ultimately show ?thesis by simp
qed
qed simp

subsection ‹Cosets›

subsubsection ‹Basic facts›

lemma set_zero_plus' [simp]: "(0::'a::monoid_add) +o C = C"
― ‹lemma @{text "Set_Algebras.set_zero_plus"} is restricted to types of class

lemma lcoset_0: "(w::'a::monoid_add) +o 0 = {w}"
using elt_set_plus_def[of w] by simp

lemma lcoset_refl: "(0::'a::monoid_add) ∈ A ⟹ a ∈ a +o A"
using elt_set_plus_def by force

lemma lcoset_eq_reps_subset:
"(a::'a::group_add) +o A ⊆ a +o B ⟹ A ⊆ B"
using elt_set_plus_def[of a] by auto

lemma lcoset_eq_reps: "(a::'a::group_add) +o A = a +o B ⟹ A = B"
using lcoset_eq_reps_subset[of a A B] lcoset_eq_reps_subset[of a B A] by auto

using lcoset_eq_reps inj_onI[of UNIV "(+o) a"] by auto

lemma lcoset_conv_set: "(a::'g::group_add) ∈ b +o A ⟹ -b + a ∈ A"

subsubsection ‹The supset order on cosets›

lemma supset_lbound_lcoset_shift:
"supset_lbound_of X Y B ⟹
ordering.lbound_of (⊇) (a +o X) (a +o Y) (a +o B)"
using ordering.lbound_of_def[OF supset_poset, of X Y B]
by    (fast intro: ordering.lbound_ofI supset_poset)

lemma supset_glbound_in_of_lcoset_shift:
fixes   P :: "'a::group_add set set"
assumes "supset_glbound_in_of P X Y B"
shows   "supset_glbound_in_of ((+o) a ` P) (a +o X) (a +o Y) (a +o B)"
using   ordering.glbound_in_ofD_in[OF supset_poset, OF assms]
ordering.glbound_in_ofD_lbound[OF supset_poset, OF assms]
supset_lbound_lcoset_shift[of X Y B a]
supset_lbound_lcoset_shift[of "a +o X" "a +o Y" _ "-a"]
ordering.glbound_in_ofD_glbound[OF supset_poset, OF assms]
ordering.glbound_in_ofI[
OF supset_poset, of "a +o B" "(+o) a ` P" "a +o X" "a +o Y"
]

subsubsection ‹The afforded partition›

definition lcoset_rel :: "'a::{uminus,plus} set ⇒ ('a×'a) set"
where "lcoset_rel A ≡ {(x,y). -x + y ∈ A}"

lemma lcoset_relI: "-x+y ∈ A ⟹ (x,y) ∈ lcoset_rel A"
using lcoset_rel_def by fast

subsection ‹Groups›

text ‹We consider groups as closed sets in a type of class @{class group_add}.›

subsubsection ‹Locale definition and basic facts›

locale    Group =
assumes nonempty   : "G ≠ {}"
and     diff_closed: "⋀g h. g ∈ G ⟹ h ∈ G ⟹ g - h ∈ G"
begin

abbreviation Subgroup :: "'g set ⇒ bool"
where "Subgroup H ≡ Group H ∧ H ⊆ G"

lemma SubgroupD1: "Subgroup H ⟹ Group H" by fast

lemma zero_closed : "0 ∈ G"
proof-
from nonempty obtain g where "g ∈ G" by fast
hence "g - g ∈ G" using diff_closed by fast
thus ?thesis by simp
qed

lemma uminus_closed: "g∈G ⟹ -g∈G"
using zero_closed diff_closed[of 0 g] by simp

lemma add_closed: "g∈G ⟹ h∈G ⟹ g+h ∈ G"
using uminus_closed[of h] diff_closed[of g "-h"] by simp

lemma uminus_add_closed: "g ∈ G ⟹ h ∈ G ⟹ -g + h ∈ G"

lemma lconjby_closed: "g∈G ⟹ x∈G ⟹ lconjby g x ∈ G"

lemma lconjby_set_closed: "g∈G ⟹ A⊆G ⟹ lconjby g ` A ⊆ G"
using lconjby_closed by fast

lemma set_lconjby_subset_closed:
"H⊆G ⟹ A⊆G ⟹ (⋃h∈H. lconjby h ` A) ⊆ G"
using lconjby_set_closed[of _ A] by fast

lemma sum_list_map_closed: "set (map f as) ⊆ G ⟹ (∑a←as. f a) ∈ G"
using zero_closed add_closed by (induct as) auto

lemma sum_list_closed: "set as ⊆ G ⟹ sum_list as ∈ G"
using sum_list_map_closed by force

end (* context Group *)

subsubsection ‹Sets with a suitable binary operation›

text ‹
We have chosen to only consider groups in types of class @{class group_add} so that we can take
advantage of all the algebra lemmas already proven in @{theory HOL.Groups}, as well as
constructs like @{const sum_list}. The following locale builds a bridge between this restricted
view of groups and the usual notion of a binary operation on a set satisfying the group axioms,
by constructing an injective map into type @{type permutation} (which is of class
@{class group_add} with respect to the composition operation) that respects the group operation.
This bridge will be necessary to define quotient groups, in particular.
›

locale BinOpSetGroup =
fixes G     :: "'a set"
and   binop :: "'a⇒'a⇒'a"
and   e     :: "'a"
assumes closed  : "g∈G ⟹ h∈G ⟹ binop g h ∈ G"
and     assoc   :
"⟦ g∈G; h∈G; k∈G ⟧ ⟹ binop (binop g h) k = binop g (binop h k)"
and     identity: "e∈G" "g∈G ⟹ binop g e = g" "g∈G ⟹ binop e g = g"
and     inverses: "g∈G ⟹ ∃h∈G. binop g h = e ∧ binop h g = e"
begin

lemma unique_identity1: "g∈G ⟹ ∀x∈G. binop g x = x ⟹ g = e"
using identity(1,2) by auto

lemma unique_inverse:
assumes "g∈G"
shows   "∃!h. h∈G ∧ binop g h = e ∧ binop h g = e"
proof (rule ex_ex1I)
from assms show "∃h. h ∈ G ∧ binop g h = e ∧ binop h g = e"
using inverses by fast
next
fix h k
assume "h∈G ∧ binop g h = e ∧ binop h g = e" "k∈G ∧
binop g k = e ∧ binop k g = e"
hence h: "h∈G" "binop g h = e" "binop h g = e"
and k: "k∈G" "binop g k = e" "binop k g = e"
by  auto
from assms h(1,3) k(1,2) show "h=k" using identity(2,3) assoc by force
qed

abbreviation "G_perm g ≡ restrict1 (binop g) G"

definition Abs_G_perm :: "'a ⇒ 'a permutation"
where "Abs_G_perm g ≡ Abs_permutation (G_perm g)"

abbreviation "𝔭 ≡ Abs_G_perm" ― ‹the injection into type @{type permutation}›
abbreviation "𝔦𝔭 ≡ the_inv_into G 𝔭" ― ‹the reverse correspondence›
abbreviation "pG ≡ 𝔭`G" ― ‹the resulting @{const Group} of type @{type permutation}›

lemma G_perm_comp:
"g∈G ⟹ h∈G ⟹ G_perm g ∘ G_perm h = G_perm (binop g h)"
using closed by (auto simp add: assoc)

definition the_inverse :: "'a ⇒ 'a"
where "the_inverse g ≡ (THE h. h∈G ∧ binop g h = e ∧ binop h g = e)"

abbreviation "𝔦 ≡ the_inverse"

lemma the_inverseD:
assumes   "g∈G"
shows     "𝔦 g ∈ G" "binop g (𝔦 g) = e" "binop (𝔦 g) g = e"
using     assms theI'[OF unique_inverse]
unfolding the_inverse_def
by        auto

lemma binop_G_comp_binop_𝔦G: "g∈G ⟹ x∈G ⟹ binop g (binop (𝔦 g) x) = x"
using the_inverseD(1) assoc[of g "𝔦 g" x] by (simp add: identity(3) the_inverseD(2))

lemma bij_betw_binop_G:
assumes   "g∈G"
shows     "bij_betw (binop g) G G"
unfolding bij_betw_def
proof
show "inj_on (binop g) G"
proof (rule inj_onI)
fix h k assume hk: "h∈G" "k∈G" "binop g h = binop g k"
with assms have "binop (binop (𝔦 g) g) h = binop (binop (𝔦 g) g) k"
using the_inverseD(1) by (simp add: assoc)
with assms hk(1,2) show "h=k" using the_inverseD(3) identity by simp
qed
show "binop g ` G = G"
proof
from assms show "binop g ` G ⊆ G" using closed by fast
from assms show "binop g ` G ⊇ G"
using binop_G_comp_binop_𝔦G[THEN sym] the_inverseD(1) closed by fast
qed
qed

lemma the_inv_into_G_binop_G:
assumes "g∈G" "x∈G"
shows   "the_inv_into G (binop g) x = binop (𝔦 g) x"
proof (rule the_inv_into_f_eq)
from assms(1) show "inj_on (binop g) G"
using bij_betw_imp_inj_on[OF bij_betw_binop_G] by fast
from assms show "binop g (binop (𝔦 g) x) = x"
using binop_G_comp_binop_𝔦G by fast
from assms show "binop (𝔦 g) x ∈ G" using closed the_inverseD(1) by fast
qed

lemma restrict1_the_inv_into_G_binop_G:
"g∈G ⟹ restrict1 (the_inv_into G (binop g)) G = G_perm (𝔦 g)"
using the_inv_into_G_binop_G by auto

lemma bij_G_perm: "g∈G ⟹ bij (G_perm g)"
using set_permutation_bij_restrict1 bij_betw_binop_G by fast

lemma G_perm_apply: "g∈G ⟹ x∈G ⟹ 𝔭 g → x = binop g x"
using Abs_G_perm_def Abs_permutation_inverse bij_G_perm by fastforce

lemma G_perm_apply_identity: "g∈G ⟹ 𝔭 g → e = g"
using G_perm_apply identity(1,2) by simp

lemma the_inv_G_perm:
"g∈G ⟹ the_inv (G_perm g) = G_perm (𝔦 g)"
using set_permutation_the_inv_restrict1 bij_betw_binop_G
restrict1_the_inv_into_G_binop_G
by    fastforce

lemma Abs_G_perm_diff:
"g∈G ⟹ h∈G ⟹ 𝔭 g - 𝔭 h = 𝔭 (binop g (𝔦 h))"
using Abs_G_perm_def minus_permutation_abs_eq[OF bij_G_perm bij_G_perm]
the_inv_G_perm G_perm_comp the_inverseD(1)
by    simp

lemma Group: "Group pG"
using identity(1) Abs_G_perm_diff the_inverseD(1) closed by unfold_locales auto

lemma inj_on_𝔭_G: "inj_on 𝔭 G"
proof (rule inj_onI)
fix x y assume xy: "x∈G" "y∈G" "𝔭 x = 𝔭 y"
hence "Abs_permutation (G_perm (binop x (𝔦 y))) = Abs_permutation id"
using Abs_G_perm_diff Abs_G_perm_def
moreover from xy(1,2) have 1: "binop x (𝔦 y) ∈ G"
using bij_id closed the_inverseD(1) by fast
ultimately have 2: "G_perm (binop x (𝔦 y)) = id"
using Abs_permutation_inject[of "G_perm (binop x (𝔦 y))"] bij_G_perm bij_id
by    simp
have "∀z∈G. binop (binop x (𝔦 y)) z = z"
proof
fix z assume "z∈G"
thus "binop (binop x (𝔦 y)) z = z" using fun_cong[OF 2, of z] by simp
qed
with xy(1,2) have "binop x (binop (𝔦 y) y) = y"
using unique_identity1[OF 1] the_inverseD(1) by (simp add: assoc)
with xy(1,2) show "x = y" using the_inverseD(3) identity(2) by simp
qed

lemma homs:
"⋀g h. g∈G ⟹ h∈G ⟹ 𝔭 (binop g h) = 𝔭 g + 𝔭 h"
"⋀x y. x∈pG ⟹ y∈pG ⟹ binop (𝔦𝔭 x) (𝔦𝔭 y) = 𝔦𝔭 (x+y)"
proof-
show 1: "⋀g h. g∈G ⟹ h∈G ⟹ 𝔭 (binop g h) = 𝔭 g + 𝔭 h"
using Abs_G_perm_def G_perm_comp
plus_permutation_abs_eq[OF bij_G_perm bij_G_perm]
by    simp
show "⋀x y. x∈pG ⟹ y∈pG ⟹ binop (𝔦𝔭 x) (𝔦𝔭 y) = 𝔦𝔭 (x+y)"
proof-
fix x y assume "x∈pG" "y∈pG"
moreover hence "𝔦𝔭 (𝔭 (binop (𝔦𝔭 x) (𝔦𝔭 y))) = 𝔦𝔭 (x + y)"
using 1 the_inv_into_into[OF inj_on_𝔭_G] f_the_inv_into_f[OF inj_on_𝔭_G]
by    simp
ultimately show "binop (𝔦𝔭 x) (𝔦𝔭 y) = 𝔦𝔭 (x+y)"
using the_inv_into_into[OF inj_on_𝔭_G] closed the_inv_into_f_f[OF inj_on_𝔭_G]
by    simp
qed
qed

lemmas inv_correspondence_into =
the_inv_into_into[OF inj_on_𝔭_G, of _ G, simplified]

lemma inv_correspondence_conv_apply: "x ∈ pG ⟹ 𝔦𝔭 x = x→e"
using G_perm_apply_identity inj_on_𝔭_G by (auto intro: the_inv_into_f_eq)

end (* context BinOpSetGroup *)

subsubsection ‹Cosets of a @{const Group}›

context Group
begin

lemma lcoset_refl: "a ∈ a +o G"
using lcoset_refl zero_closed by fast

lemma lcoset_el_reduce:
assumes "a ∈ G"
shows "a +o G = G"
proof (rule seteqI)
fix x assume "x ∈ a +o G"
from this obtain g where "g∈G" "x = a+g" using elt_set_plus_def[of a] by auto
next
fix x assume "x∈G"
with assms have "-a + x ∈ G" by (simp add: uminus_add_closed)
thus "x ∈ a +o G" using elt_set_plus_def by force
qed

lemma lcoset_el_reduce0: "0 ∈ a +o G ⟹ a +o G = G"
using elt_set_plus_def[of a G] minus_unique uminus_closed[of "-a"]
lcoset_el_reduce
by    fastforce

lemma lcoset_subgroup_imp_eq_reps:
"Group H ⟹ w +o H ⊆ w' +o G ⟹ w' +o G = w +o G"
using Group.lcoset_refl[of H w] lcoset_conv_set[of w] lcoset_el_reduce
set_plus_rearrange2[of w' "-w'+w" G]
by    force

lemma lcoset_closed: "a∈G ⟹ A⊆G ⟹ a +o A ⊆ G"
using elt_set_plus_def[of a] add_closed by auto

lemma lcoset_rel_sym: "sym (lcoset_rel G)"
proof (rule symI)
fix a b show "(a,b) ∈ lcoset_rel G ⟹ (b,a) ∈ lcoset_rel G"
using uminus_closed minus_add[of "-a" b] lcoset_rel_def[of G] by fastforce
qed

lemma lcoset_rel_trans: "trans (lcoset_rel G)"
proof (rule transI)
fix x y z assume xy: "(x,y) ∈ lcoset_rel G" and yz: "(y,z) ∈ lcoset_rel G"
from this obtain g g' where "g∈G" "-x+y = g" "g'∈G" "-y+z = g'"
using lcoset_rel_def[of G] by fast
thus "(x, z) ∈ lcoset_rel G"
qed

abbreviation LCoset_rel :: "'g set ⇒ ('g×'g) set"
where "LCoset_rel H ≡ lcoset_rel H ∩ (G×G)"

lemma refl_on_LCoset_rel: "0∈H ⟹ refl_on G (LCoset_rel H)"
using lcoset_rel_def by (fastforce intro: refl_onI)

lemmas subgroup_refl_on_LCoset_rel =
refl_on_LCoset_rel[OF Group.zero_closed, OF SubgroupD1]
lemmas LCoset_rel_quotientI        = quotientI[of _ G "LCoset_rel _"]
lemmas LCoset_rel_quotientE        = quotientE[of _ G "LCoset_rel _"]

lemma lcoset_subgroup_rel_equiv:
"Subgroup H ⟹ equiv G (LCoset_rel H)"
using Group.lcoset_rel_sym sym_sym sym_Int Group.lcoset_rel_trans trans_sym
trans_Int subgroup_refl_on_LCoset_rel
by    (blast intro: equivI)

lemma trivial_LCoset: "H⊆G ⟹ H = LCoset_rel H `` {0}"
using zero_closed unfolding lcoset_rel_def by auto

end (* context Group *)

subsubsection ‹The @{const Group} generated by a set›

inductive_set genby :: "'a::group_add set ⇒ 'a set" ("⟨_⟩")
for S :: "'a set"
where
genby_0_closed     : "0∈⟨S⟩"  ― ‹just in case @{term S} is empty›
| genby_genset_closed: "s∈S ⟹ s∈⟨S⟩"
| genby_diff_closed  : "w∈⟨S⟩ ⟹ w'∈⟨S⟩ ⟹ w - w' ∈ ⟨S⟩"

lemma genby_Group: "Group ⟨S⟩"
using genby_0_closed genby_diff_closed by unfold_locales fast

lemmas genby_uminus_closed             = Group.uminus_closed     [OF genby_Group]
lemmas genby_lcoset_refl               = Group.lcoset_refl       [OF genby_Group]
lemmas genby_lcoset_el_reduce          = Group.lcoset_el_reduce  [OF genby_Group]
lemmas genby_lcoset_el_reduce0         = Group.lcoset_el_reduce0 [OF genby_Group]
lemmas genby_lcoset_closed             = Group.lcoset_closed     [OF genby_Group]

lemmas genby_lcoset_subgroup_imp_eq_reps =
Group.lcoset_subgroup_imp_eq_reps[OF genby_Group, OF genby_Group]

lemma genby_genset_subset: "S ⊆ ⟨S⟩"
using genby_genset_closed by fast

lemma genby_uminus_genset_subset: "uminus ` S ⊆ ⟨S⟩"
using genby_genset_subset genby_uminus_closed by auto

lemma genby_in_sum_list_lists:
fixes   S
defines S_sum_lists: "S_sum_lists ≡ (⋃ss∈lists (S ∪ uminus ` S). {sum_list ss})"
shows   "w ∈ ⟨S⟩ ⟹ w ∈ S_sum_lists"
proof (erule genby.induct)
have "0 = sum_list []" by simp
with S_sum_lists show "0 ∈ S_sum_lists" by blast
next
fix s assume "s∈S"
hence "[s] ∈ lists (S ∪ uminus ` S)" by simp
moreover have "s = sum_list [s]" by simp
ultimately show "s ∈ S_sum_lists" using S_sum_lists by blast
next
fix w w' assume ww': "w ∈ S_sum_lists" "w' ∈ S_sum_lists"
with S_sum_lists obtain ss ts
where ss: "ss ∈ lists (S ∪ uminus ` S)" "w = sum_list ss"
and   ts: "ts ∈ lists (S ∪ uminus ` S)" "w' = sum_list ts"
by fastforce
from ss(2) ts(2) have "w-w' = sum_list (ss @ map uminus (rev ts))"
moreover from ss(1) ts(1)
have  "ss @ map uminus (rev ts) ∈ lists (S ∪ uminus ` S)"
by    fastforce
ultimately show "w - w' ∈ S_sum_lists" using S_sum_lists by fast
qed

lemma sum_list_lists_in_genby: "ss ∈ lists (S ∪ uminus ` S) ⟹ sum_list ss ∈ ⟨S⟩"
proof (induct ss)
case Nil show ?case using genby_0_closed by simp
next
case (Cons s ss) thus ?case
using genby_genset_subset[of S] genby_uminus_genset_subset
by    auto
qed

lemma sum_list_lists_in_genby_sym:
"uminus ` S ⊆ S ⟹ ss ∈ lists S ⟹ sum_list ss ∈ ⟨S⟩"
using sum_list_lists_in_genby by fast

lemma genby_eq_sum_lists: "⟨S⟩ = (⋃ss∈lists (S ∪ uminus ` S). {sum_list ss})"
using genby_in_sum_list_lists sum_list_lists_in_genby by fast

lemma genby_mono: "T ⊆ S ⟹ ⟨T⟩ ⊆ ⟨S⟩"
using genby_eq_sum_lists[of T] genby_eq_sum_lists[of S] by force

lemma (in Group) genby_closed:
assumes "S ⊆ G"
shows "⟨S⟩ ⊆ G"
proof
fix x show "x ∈ ⟨S⟩ ⟹ x ∈ G"
proof (erule genby.induct, rule zero_closed)
from assms show "⋀s. s∈S ⟹ s∈G" by fast
show "⋀w w'. w∈G ⟹ w'∈G ⟹ w-w' ∈ G" using diff_closed by fast
qed
qed

lemma (in Group) genby_subgroup: "S ⊆ G ⟹ Subgroup ⟨S⟩"
using genby_closed genby_Group by simp

lemma genby_sym_eq_sum_lists:
"uminus ` S ⊆ S ⟹ ⟨S⟩ = (⋃ss∈lists S. {sum_list ss})"
using lists_mono genby_eq_sum_lists[of S] by force

lemma genby_empty': "w ∈ ⟨{}⟩ ⟹ w = 0"
proof (erule genby.induct) qed auto

lemma genby_order2':
assumes "s+s=0"
shows   "w ∈ ⟨{s}⟩ ⟹ w = 0 ∨ w = s"
proof (erule genby.induct)
fix w w' assume "w = 0 ∨ w = s" "w' = 0 ∨ w' = s"
with assms show "w - w' = 0 ∨ w - w' = s"
by (cases "w'=0") (auto simp add: minus_unique)
qed auto

lemma genby_order2: "s+s=0 ⟹ ⟨{s}⟩ = {0,s}"
using genby_order2'[of s] genby_0_closed genby_genset_closed by auto

lemma genby_empty: "⟨{}⟩ = 0"
using genby_empty' genby_0_closed by auto

lemma genby_lcoset_order2: "s+s=0 ⟹ w +o ⟨{s}⟩ = {w,w+s}"
using elt_set_plus_def[of w] by (auto simp add: genby_order2)

lemma genby_lcoset_empty: "(w::'a::group_add) +o ⟨{}⟩ = {w}"
proof-
have "⟨{}::'a set⟩ = (0::'a set)" using genby_empty by fast
thus ?thesis using lcoset_0 by simp
qed

lemma (in Group) genby_set_lconjby_set_lconjby_closed:
fixes   A :: "'g set"
defines "S ≡ (⋃g∈G. lconjby g ` A)"
assumes "g∈G"
shows   "x ∈ ⟨S⟩ ⟹ lconjby g x ∈ ⟨S⟩"
proof (erule genby.induct)
show "lconjby g 0 ∈ ⟨S⟩" using genby_0_closed by simp
from assms show "⋀s. s ∈ S ⟹ lconjby g s ∈ ⟨S⟩"
next
fix w w'
assume ww': "lconjby g w ∈ ⟨S⟩" "lconjby g w' ∈ ⟨S⟩"
have "lconjby g (w - w') = lconjby g w + lconjby g (-w')"
with ww' show "lconjby g (w - w') ∈ ⟨S⟩"
using lconjby_uminus[of g] diff_conv_add_uminus[of _ "lconjby g w'"]
genby_diff_closed
by    fastforce
qed

lemma (in Group) genby_set_lconjby_set_rconjby_closed:
fixes   A :: "'g set"
defines "S ≡ (⋃g∈G. lconjby g ` A)"
assumes "g∈G" "x ∈ ⟨S⟩"
shows   "rconjby g x ∈ ⟨S⟩"
using   assms uminus_closed genby_set_lconjby_set_lconjby_closed
by      fastforce

subsubsection ‹Homomorphisms and isomorphisms›

locale GroupHom = Group G
+ fixes T :: "'g ⇒ 'h::group_add"
assumes hom : "g ∈ G ⟹ g' ∈ G ⟹ T (g + g') = T g + T g'"
and     supp: "supp T ⊆ G"
begin

lemma im_zero: "T 0 = 0"
using zero_closed hom[of 0 0] add_diff_cancel[of "T 0" "T 0"] by simp

lemma im_uminus: "T (- g) = - T g"
using im_zero hom[of g "- g"] uminus_closed[of g] minus_unique[of "T g"]
uminus_closed[of "-g"] supp suppI_contra[of g T]
suppI_contra[of "-g" T]
by    fastforce

lemma im_uminus_add: "g ∈ G ⟹ g' ∈ G ⟹ T (-g + g') = - T g + T g'"
by (simp add: uminus_closed hom im_uminus)

lemma im_diff: "g ∈ G ⟹ g' ∈ G ⟹ T (g - g') = T g - T g'"
using hom uminus_closed hom[of g "-g'"] im_uminus by simp

lemma im_lconjby: "x ∈ G ⟹ g ∈ G ⟹ T (lconjby x g) = lconjby (T x) (T g)"

lemma im_sum_list_map:
"set (map f as) ⊆ G ⟹ T (∑a←as. f a) = (∑a←as. T (f a))"
using hom im_zero sum_list_closed by (induct as) auto

lemma comp:
assumes "GroupHom H S" "T`G ⊆ H"
shows   "GroupHom G (S ∘ T)"
proof
fix g g' assume "g ∈ G" "g' ∈ G"
with hom assms(2) show "(S ∘ T) (g + g') = (S ∘ T) g + (S ∘ T) g'"
using GroupHom.hom[OF assms(1)] by fastforce
next
from supp have "⋀g. g ∉ G ⟹ (S ∘ T) g = 0"
using suppI_contra GroupHom.im_zero[OF assms(1)] by fastforce
thus "supp (S ∘ T) ⊆ G" using suppD_contra by fast
qed

end (* context GroupHom *)

definition ker :: "('a⇒'b::zero) ⇒ 'a set"
where "ker f = {a. f a = 0}"

lemma ker_subset_ker_restrict0: "ker f ⊆ ker (restrict0 f A)"
unfolding ker_def by auto

context GroupHom
begin

abbreviation "Ker ≡ ker T ∩ G"

"g∈G ⟹ h∈G ⟹ (-g + h ∈ Ker) = (T g = T h)"
using neg_equal_iff_equal

end (* context GroupHom *)

locale UGroupHom = GroupHom UNIV T
begin

lemmas im_zero       = im_zero
lemmas im_uminus     = im_uminus

lemma hom: "T (g+g') = T g + T g'"
using hom by simp

lemma im_diff: "T (g - g') = T g - T g'"
using im_diff by simp

lemma im_lconjby: "T (lconjby x g) = lconjby (T x) (T g)"
using im_lconjby by simp

lemma restrict0:
assumes "Group G"
shows   "GroupHom G (restrict0 T G)"
proof (intro_locales, rule assms, unfold_locales)
from hom
show  "⋀g g'. g ∈ G ⟹ g' ∈ G ⟹
restrict0 T G (g + g') = restrict0 T G g + restrict0 T G g'"
by    auto
show "supp (restrict0 T G) ⊆ G" using supp_restrict0[of G T] by fast
qed

end (* context UGroupHom *)

lemma UGroupHomI:
assumes "⋀g g'. T (g + g') = T g + T g'"
shows   "UGroupHom T"
using   assms
by      unfold_locales auto

locale GroupIso = GroupHom G T
and   T :: "'g ⇒ 'h::group_add"
+ assumes inj_on: "inj_on T G"

lemma (in GroupHom) isoI:
assumes "⋀k. k∈G ⟹ T k = 0 ⟹ k=0"
shows   "GroupIso G T"
proof (unfold_locales, rule inj_onI)
fix x y from assms show "⟦ x∈G; y∈G; T x = T y ⟧ ⟹ x = y"
using im_diff diff_closed by force
qed

text ‹
In a @{const BinOpSetGroup}, any map from the set into a type of class @{class group_add} that respects the
binary operation induces a @{const GroupHom}.
›

abbreviation (in BinOpSetGroup) "lift_hom T ≡ restrict0 (T ∘ 𝔦𝔭) pG"

lemma (in BinOpSetGroup) lift_hom:
fixes T :: "'a ⇒ 'b::group_add"
assumes "∀g∈G. ∀h∈G. T (binop g h) = T g + T h"
shows   "GroupHom pG (lift_hom T)"
proof (intro_locales, rule Group, unfold_locales)
from assms
show  "⋀x y. x∈pG ⟹ y∈pG ⟹
lift_hom T (x+y) = lift_hom T x + lift_hom T y"
qed (rule supp_restrict0)

subsubsection ‹Normal subgroups›

definition rcoset_rel :: "'a::{minus,plus} set ⇒ ('a×'a) set"
where "rcoset_rel A ≡ {(x,y). x-y ∈ A}"

context Group
begin

lemma rcoset_rel_conv_lcoset_rel:
"rcoset_rel G = map_prod uminus uminus ` (lcoset_rel G)"
proof (rule set_eqI)
fix x :: "'g×'g"
obtain a b where ab: "x=(a,b)" by fastforce
hence "(x ∈ rcoset_rel G) = (a-b ∈ G)"  using rcoset_rel_def by auto
also have "… = ( (-b,-a) ∈ lcoset_rel G )"
using uminus_closed lcoset_rel_def by fastforce
finally
show  "(x ∈ rcoset_rel G) = (x ∈ map_prod uminus uminus ` (lcoset_rel G))"
using ab symD[OF lcoset_rel_sym] map_prod_def
by    force
qed

lemma rcoset_rel_sym: "sym (rcoset_rel G)"
using rcoset_rel_conv_lcoset_rel map_prod_sym lcoset_rel_sym by simp

abbreviation RCoset_rel :: "'g set ⇒ ('g×'g) set"
where "RCoset_rel H ≡ rcoset_rel H ∩ (G×G)"

definition normal :: "'g set ⇒ bool"
where "normal H ≡ (∀g∈G. LCoset_rel H `` {g} = RCoset_rel H `` {g})"

lemma normalI:
assumes   "Group H" "∀g∈G. ∀h∈H. ∃h'∈H. g+h = h'+g"
"∀g∈G. ∀h∈H. ∃h'∈H. h+g = g+h'"
shows     "normal H"
unfolding normal_def
proof
fix g assume g: "g∈G"
show "LCoset_rel H `` {g} = RCoset_rel H `` {g}"
proof (rule seteqI)
fix x assume "x ∈ LCoset_rel H `` {g}"
with g have x: "x∈G" "-g+x ∈ H" unfolding lcoset_rel_def by auto
from g x(2) assms(2) obtain h where h: "h∈H" "g-x = -h"
with assms(1) g x(1) show "x ∈ RCoset_rel H `` {g}"
using Group.uminus_closed unfolding rcoset_rel_def by simp
next
fix x assume "x ∈ RCoset_rel H `` {g}"
with g have x: "x∈G" "g-x ∈ H" unfolding rcoset_rel_def by auto
with assms(3) obtain h where h: "h∈H" "-g+x = -h"
with assms(1) g x(1) show "x ∈ LCoset_rel H `` {g}"
using Group.uminus_closed unfolding lcoset_rel_def by simp
qed
qed

lemma normal_lconjby_closed:
"⟦ Subgroup H; normal H; g∈G; h∈H ⟧ ⟹ lconjby g h ∈ H"
using lcoset_relI[of g "g+h" H] add_closed[of g h] normal_def[of H]
symD[OF Group.rcoset_rel_sym, of H g "g+h"] rcoset_rel_def[of H]
by    auto

lemma normal_rconjby_closed:
"⟦ Subgroup H; normal H; g∈G; h∈H ⟧ ⟹ rconjby g h ∈ H"
using normal_lconjby_closed[of H "-g" h] uminus_closed[of g] by auto

abbreviation "normal_closure A ≡ ⟨⋃g∈G. lconjby g ` A⟩"

lemma (in Group) normal_closure:
assumes "A⊆G"
shows   "normal (normal_closure A)"
proof (rule normalI, rule genby_Group)
show "∀x∈G. ∀h∈⟨⋃g∈G. lconjby g ` A⟩.
∃h'∈⟨⋃g∈G. lconjby g ` A⟩. x + h = h' + x"
proof
fix x assume x: "x∈G"
show "∀h∈⟨⋃g∈G. lconjby g ` A⟩.
∃h'∈⟨⋃g∈G. lconjby g ` A⟩. x + h = h' + x"
proof (rule ballI, erule genby.induct)
show "∃h∈⟨⋃g∈G. lconjby g ` A⟩. x + 0 = h + x"
using genby_0_closed by force
next
fix s assume "s ∈ (⋃g∈G. lconjby g ` A)"
from this obtain g a where ga: "g∈G" "a∈A" "s = lconjby g a" by fast
from ga(3) have "x + s = lconjby x (lconjby g a) + x"
hence "x + s = lconjby (x+g) a + x" by (simp add: lconjby_add)
with x ga(1,2) show "∃h∈⟨⋃g∈G. lconjby g ` A⟩. x + s = h + x"
using add_closed by (blast intro: genby_genset_closed)
next
fix w w'
assume w :  "w ∈ ⟨⋃g∈G. lconjby g ` A⟩"
"∃h ∈⟨⋃g∈G. lconjby g ` A⟩. x + w  = h + x"
and  w':  "w'∈ ⟨⋃g∈G. lconjby g ` A⟩"
"∃h'∈⟨⋃g∈G. lconjby g ` A⟩. x + w' = h'+ x"
from w(2) w'(2) obtain h h'
where h : "h ∈ ⟨⋃g∈G. lconjby g ` A⟩" "x + w  = h + x"
and   h': "h'∈ ⟨⋃g∈G. lconjby g ` A⟩" "x + w' = h'+ x"
by    fast
have "x + (w - w') = x + w - (-x + (x + w'))"
also from h(2) h'(2) have "… = h + x + (-(h' + x) + x)"
also have "… = h + x + (-x + -h') + x"
finally have "x + (w-w') = h - h' + x"
using add.assoc[of "h+x" "-x" "-h'"] by simp
with h(1) h'(1)
show  "∃h∈⟨⋃g∈G. lconjby g ` A⟩. x + (w - w') = h + x"
using genby_diff_closed
by    fast
qed
qed
show "∀x∈G. ∀h∈⟨⋃g∈G. lconjby g ` A⟩.
∃h'∈⟨⋃g∈G. lconjby g ` A⟩. h + x = x + h'"
proof
fix x assume x: "x∈G"
show "∀h∈⟨⋃g∈G. lconjby g ` A⟩.
∃h'∈⟨⋃g∈G. lconjby g ` A⟩. h + x = x + h'"
proof (rule ballI, erule genby.induct)
show "∃h∈⟨⋃g∈G. lconjby g ` A⟩. 0 + x = x + h"
using genby_0_closed by force
next
fix s assume "s ∈ (⋃g∈G. lconjby g ` A)"
from this obtain g a where ga: "g∈G" "a∈A" "s = lconjby g a" by fast
from ga(3) have "s + x = x + (((-x + g) + a) + -g) + x"
also have "… = x + (-x + g + a + -g + x)" by (simp add: add.assoc)
finally have "s + x = x + lconjby (-x+g) a"
with x ga(1,2) show "∃h∈⟨⋃g∈G. lconjby g ` A⟩. s + x = x + h"
using uminus_add_closed by (blast intro: genby_genset_closed)
next
fix w w'
assume w :  "w ∈ ⟨⋃g∈G. lconjby g ` A⟩"
"∃h ∈⟨⋃g∈G. lconjby g ` A⟩. w  + x = x + h"
and  w':  "w'∈ ⟨⋃g∈G. lconjby g ` A⟩"
"∃h'∈⟨⋃g∈G. lconjby g ` A⟩. w' + x = x + h'"
from w(2) w'(2) obtain h h'
where h : "h ∈ ⟨⋃g∈G. lconjby g ` A⟩" "w + x = x + h"
and   h': "h'∈ ⟨⋃g∈G. lconjby g ` A⟩" "w' + x = x + h'"
by    fast
have "w - w' + x = w + x + (-x + -w') + x" by (simp add: algebra_simps)
also from h(2) h'(2) have "… = x + h + (-h'+-x) + x"
finally have "w - w' + x = x + (h - h')" by (simp add: algebra_simps)
with h(1) h'(1) show "∃h∈⟨⋃g∈G. lconjby g ` A⟩. w - w' + x = x + h"
using genby_diff_closed by fast
qed
qed
qed

end (* context Group *)

subsubsection ‹Quotient groups›

text ‹
Here we use the bridge built by @{const BinOpSetGroup} to make the quotient of a @{const Group}
by a normal subgroup into a @{const Group} itself.
›

context Group
begin