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)"
  using add.assoc by simp

lemmas (in monoid_add) sum_list_map_cong =
  arg_cong[OF map_cong, OF refl, of _ _ _ sum_list]

context group_add
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))"
  by (induct as) (auto simp add: minus_add)

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

end (* context group_add *)

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)"
  by (simp add: plus_permutation.abs_eq eq_onp_same_args)

instance permutation :: (type) semigroup_add
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

instance permutation :: (type) monoid_add
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)"
  by (simp add: minus_permutation.abs_eq eq_onp_same_args)

instance permutation :: (type) group_add
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}.
›

context monoid_add
begin

sublocale nataction: power 0 plus .
sublocale add_mult_translate: monoid_mult 0 plus
  by unfold_locales (auto simp add: add.assoc)

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

lemmas nataction_2    = add_mult_translate.power2_eq_square
lemmas nataction_Suc2 = add_mult_translate.power_Suc2

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

end (* context monoid_add *)

lemma (in group_add) nataction_add_eq0_flip:
  assumes "(a+b)+^n = 0"
  shows   "(b+a)+^n = 0"
proof (cases n)
  case (Suc k) with assms show ?thesis
    using nataction_add_flip add.assoc[of "-a" "a+b" "(a+b)+^k"] by simp
qed simp

subsubsection ‹Additive order of an element›

context monoid_add
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"

lemma add_order: "a+^(add_order a) = 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

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

lemma add_order0: "add_order 0 = 1"
  using add_order_equality by simp

lemma add_order_gt0: "(add_order a > 0) = (∃n>0. a+^n = 0)"
  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"
  using add_order_gt0 by force

lemma less_add_order_eq_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"
  using less_add_order_eq_0 by fast

lemma add_order_relator: "add_order (a+^(add_order a)) = 1"
  using add_order by (auto intro: add_order_equality)

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"
  by (auto simp add: add_order alternating_sum_list_conv_nataction)

end (* context monoid_add *)

context group_add
begin

lemma add_order_add_eq1: "add_order (s+t) = 1 ⟹ t = -s"
  using add_order[of "s+t"] by (simp add: minus_unique)

lemma add_order_add_sym: "add_order (t+s) = add_order (s+t)"
proof (cases "add_order (t+s) = 0" "add_order (s+t) = 0" rule: two_cases)
  case one thus ?thesis
    using add_order nataction_add_eq0_flip[of s t] add_order_eq0 by auto
next
  case other thus ?thesis
    using add_order nataction_add_eq0_flip[of t s] add_order_eq0 by auto
next
  case neither thus ?thesis
    using add_order[of "s+t"] add_order[of "t+s"]
          nataction_add_eq0_flip[of s t] nataction_add_eq0_flip[of t s]
          add_order_least[of "add_order (s+t)"] add_order_least[of "add_order (t+s)"]
    by fastforce
qed simp

lemma pair_relator_halflist_append:
  "pair_relator_halflist s t @ pair_relator_halflist2 s t = pair_relator_list s t"
  using alternating_list_split[of "add_order (s+t)" "add_order (s+t)" s t]
  by    (auto simp add: times2_conv_add add_order_add_sym)

lemma rev_pair_relator_list: "rev (pair_relator_list s t) = pair_relator_list t s"
  by (simp add:rev_alternating_list add_order_add_sym)

lemma pair_relator_halflist2_conv_rev_pair_relator_halflist:
  "pair_relator_halflist2 s t = rev (pair_relator_halflist t s)"
  by (auto simp add: add_order_add_sym rev_alternating_list)
 
end (* context group_add *)

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.
›

context monoid_add
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])]"
  by (induct xs) (auto simp add: add.assoc)

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]))"
      by (auto simp add: sums_snoc)
    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]))"
        by (auto simp add: sums_snoc)
      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]))"
      by (auto simp add: sums_snoc)
    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

end (* context monoid_add *)

subsection ‹Sums of alternating lists›

lemma (in group_add) uminus_sum_list_alternating_order2:
  "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

context monoid_add
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

end (* context monoid_add *)

subsection ‹Conjugation in @{class group_add}›

subsubsection ‹Abbreviations and basic facts›

context group_add
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)"
  by (auto simp add: algebra_simps)

lemma rconjby_add: "rconjby (x+y) z = rconjby y (rconjby x z)"
  by (simp add: minus_add add.assoc[THEN sym])

lemma add_rconjby: "rconjby x y + rconjby x z = rconjby x (y+z)"
  by (simp add: add.assoc)

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"
  by (simp add: algebra_simps)

lemma rconjby_lconjby: "rconjby x (lconjby x y) = y"
  by (simp add: algebra_simps)

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"
  by (simp add: add_rconjby)

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]
    by    (simp add: algebra_simps)
  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]"]
    by    (simp add: algebra_simps)
  finally show ?case by fast
qed (auto simp add: assms(1) algebra_simps)

end (* context group_add *)

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.
›

context group_add
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]"
  by (induct xs) (auto simp add: lconjby_add)

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
    using lconjseq_snoc[of "xs@ys"] lconjseq_snoc[of ys] by (simp add: lconjby_add)
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))]"
    by    (auto simp add: lconjseq_snoc lconjby_add)
  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")
          (auto simp add: alternating_list_append[of k])
  finally show ?case using altst st
    by    (auto simp add:
            alternating_list_append(1)[THEN sym]
            alternating_sum_list_conv_nataction
            lconjby_alternating_list_order2 lconjseq_snoc
          )
qed (simp add: altst altts)

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]
    by    (auto simp add: times2_conv_add lconjseq_append)
  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)"
    by (simp add: times2_conv_add)
  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"]
      by    (simp add: algebra_simps)
    ultimately have "sum_list (s#ts@[t]) = sum_list (ts@[])"
      by (simp add: algebra_simps)
    thus ?thesis by fast
  qed
qed simp

end (* context group_add *)

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}›

context group_add
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 (simp add: surj_signed_lconjaction)
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)"
      by    (simp add: signed_lconjactionD)
    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"
      by (simp add: signed_list_lconjaction_fst)
    with Cons(2)
      have  "count_list (lconjseq (rev (s#ss))) (fst x) =
              count_list (lconjseq (rev ss)) (fst x)"
      by    (simp add:
              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)"
      by (simp add: signed_lconjactionD)
    ultimately show ?thesis by simp
  qed
qed simp

end (* context group_add *)

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
@{class comm_monoid_add}; here is a version in @{class monoid_add}.›
  by (auto simp add: elt_set_plus_def)

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

lemma lcoset_inj_on: "inj ((+o) (a::'a::group_add))"
  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"
  by (auto simp add: elt_set_plus_def)

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"
          ]
  by      (fastforce simp add: set_plus_rearrange2)

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 =
  fixes   G :: "'g::group_add set"
  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"
  using uminus_closed add_closed by fast

lemma lconjby_closed: "g∈G ⟹ x∈G ⟹ lconjby g x ∈ G"
  using add_closed diff_closed by fast

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
    by (fastforce simp add: zero_permutation.abs_eq)
  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
  with assms show "x∈G" by (simp add: add_closed)
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"
    using add.assoc[of g "-y" z] add_closed lcoset_rel_def[of G] by auto
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_add_closed                = Group.add_closed        [OF genby_Group]
lemmas genby_uminus_add_closed         = Group.uminus_add_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))"
    by (simp add: diff_conv_add_uminus uminus_sum_list)
  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
          genby_add_closed[of s S "sum_list ss"]
    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⟩"
    using add_closed genby_genset_closed[of _ S] by (force simp add: lconjby_add)
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')"
    by (simp add: algebra_simps)
  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
  for   G :: "'g::group_add set"
+ 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)"
  using add_closed by (simp add: im_diff hom)

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"

lemma uminus_add_in_Ker_eq_eq_im:
  "g∈G ⟹ h∈G ⟹ (-g + h ∈ Ker) = (T g = T h)"
  using neg_equal_iff_equal
  by    (simp add: uminus_add_closed ker_def im_uminus_add eq_neg_iff_add_eq_0)

end (* context GroupHom *)

locale UGroupHom = GroupHom UNIV T
  for T :: "'g::group_add ⇒ 'h::group_add"
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'"
    using Group.add_closed[OF assms]
    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
  for   G :: "'g::group_add set"
  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"
    using Group.add_closed[OF Group] inv_correspondence_into
    by    (simp add: homs(2)[THEN sym])
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"
    by   (fastforce simp add: algebra_simps)
    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"
      by (fastforce simp add: algebra_simps minus_add)
    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"
        by (simp add: algebra_simps)
      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'))"
        by (simp add: algebra_simps)
      also from h(2) h'(2) have "… = h + x + (-(h' + x) + x)"
        by (simp add: algebra_simps)
      also have "… = h + x + (-x + -h') + x"
        by (simp add: minus_add add.assoc)
      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"
        by (simp add: algebra_simps)
      also have "… = x + (-x + g + a + -g + x)" by (simp add: add.assoc)
      finally have "s + x = x + lconjby (-x+g) a"
        by (simp add: algebra_simps lconjby_add)
      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" 
        using minus_add[of w' x] minus_add[of x h'] by simp
      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

lemma normal_quotient_add_well_defined:
  assumes "Subgroup H" "normal H" "g∈G" "g'∈G"
  shows   "LCoset_rel H `` {g} + LCoset_rel H `` {g'} = LCoset_rel H `` {g+g'}"
proof (rule seteqI)
  fix x assume "x ∈ LCoset_rel H `` {g} + LCoset_rel H `` {g'}"
  from this obtain y z
    where     "y ∈ LCoset_rel H `` {g}" "z ∈ LCoset_rel H `` {g'}" "x = y+z"
    unfolding set_plus_def
    by        fast
  with assms show "x ∈ LCoset_rel H `` {g + g'}"
    using lcoset_rel_def[of H] normal_lconjby_closed[of H g' "-g'+z"]
          Group.add_closed
          normal_rconjby_closed[of H g' "-g + y + (z - g')"]
          add.assoc[of "-g'" "-g"]
          add_closed lcoset_relI[of "g+g'" "y+z"]
    by    (fastforce simp add: add.assoc minus_add)
next
  fix x assume "x ∈ LCoset_rel H `` {g + g'}"
  moreover define h where "h ≡ -(g+g') + x"
  moreover hence "x = g + (g' + h)"
    using add.assoc[of "-g'" "-g" x] by (simp add: add.assoc minus_add)
  ultimately show "x ∈ LCoset_rel H `` {g} + LCoset_rel H `` {g'}"
    using assms(1,3,4) lcoset_rel_def[of H] add_closed
          refl_onD[OF subgroup_refl_on_LCoset_rel, of H]
    by    force
qed

abbreviation "quotient_set H ≡ G // LCoset_rel H"

lemma BinOpSetGroup_normal_quotient:
  assumes "Subgroup H" "normal H"
  shows   "BinOpSetGroup (quotient_set H) (+) H"
proof
  from assms(1) have H0: "H = LCoset_rel H `` {0}"
    using trivial_LCoset by auto

  from assms(1) show "H ∈ quotient_set H"
    using H0 zero_closed LCoset_rel_quotientI[of 0 H] by simp

  fix x assume "x ∈ quotient_set H"
  from this obtain gx where gx: "gx∈G" "x = LCoset_rel H `` {gx}"
    by (fast elim: LCoset_rel_quotientE)
  with assms(1,2) show "x+H = x" "H+x = x"
    using normal_quotient_add_well_defined[of H gx 0]
          normal_quotient_add_well_defined[of H 0 gx]
          H0 zero_closed
    by    auto

  from gx(1) have "LCoset_rel H `` {-gx} ∈ quotient_set H"
    using uminus_closed by (fast intro: LCoset_rel_quotientI)
  moreover from assms(1,2) gx
    have  "x + LCoset_rel H `` {-gx} = H" "LCoset_rel H `` {-gx} + x = H"
    using H0 uminus_closed normal_quotient_add_well_defined
    by    auto
  ultimately show "∃x'∈quotient_set H. x + x' = H ∧ x' + x = H" by fast

  fix y assume "y ∈ quotient_set H"
  from this obtain gy where gy: "gy∈G" "y = LCoset_rel H `` {gy}"
    by (fast elim: LCoset_rel_quotientE)
  with assms gx show "x+y ∈ quotient_set H"
    using add_closed normal_quotient_add_well_defined
    by    (auto intro: LCoset_rel_quotientI)

qed (rule add.assoc)

abbreviation "abs_lcoset_perm H ≡
                BinOpSetGroup.Abs_G_perm (quotient_set H) (+)"
abbreviation "abs_lcoset_perm_lift H g ≡ abs_lcoset_perm H (LCoset_rel H `` {g})"
abbreviation "abs_lcoset_perm_lift_arg_permutation g H ≡ abs_lcoset_perm_lift H g"

notation abs_lcoset_perm_lift_arg_permutation ("⌈_|_⌉" [51,51] 50)

end (* context Group *)

abbreviation "Group_abs_lcoset_perm_lift_arg_permutation G' g H ≡
  Group.abs_lcoset_perm_lift_arg_permutation G' g H"
notation Group_abs_lcoset_perm_lift_arg_permutation ("⌈_|_|_⌉" [51,51,51] 50)

context Group
begin

lemmas lcoset_perm_def =
  BinOpSetGroup.Abs_G_perm_def[OF BinOpSetGroup_normal_quotient]
lemmas lcoset_perm_comp =
  BinOpSetGroup.G_perm_comp[OF BinOpSetGroup_normal_quotient]
lemmas bij_lcoset_perm =
  BinOpSetGroup.bij_G_perm[OF BinOpSetGroup_normal_quotient]

lemma trivial_lcoset_perm:
  assumes "Subgroup H" "normal H" "h∈H"
  shows   "restrict1 ((+) (LCoset_rel H `` {h})) (quotient_set H) = id"
proof (rule ext, simp, rule impI)
  fix x assume x: "x ∈ quotient_set H"
  then obtain k where k: "k∈G" "x = LCoset_rel H `` {k}"
    by (blast elim: LCoset_rel_quotientE)
  with x have "LCoset_rel H `` {h} + x = LCoset_rel H `` {h+k}"
    using assms normal_quotient_add_well_defined by auto
  with assms k show "LCoset_rel H `` {h} + x = x"
    using add_closed[of h k] lcoset_relI[of k "h+k" H]
          normal_rconjby_closed[of H k h]
          eq_equiv_class_iff[OF lcoset_subgroup_rel_equiv, of H]
    by    (auto simp add: add.assoc)
qed

definition quotient_group :: "'g set ⇒ 'g set permutation set" where
  "quotient_group H ≡ BinOpSetGroup.pG (quotient_set H) (+)"

abbreviation "natural_quotient_hom H ≡ restrict0 (λg. ⌈g|H⌉) G"

theorem quotient_group:
  "Subgroup H ⟹ normal H ⟹ Group (quotient_group H)"
  unfolding quotient_group_def
  using     BinOpSetGroup.Group[OF BinOpSetGroup_normal_quotient]
  by        auto

lemma natural_quotient_hom:
  "Subgroup H ⟹ normal H ⟹ GroupHom G (natural_quotient_hom H)"
  using add_closed bij_lcoset_perm lcoset_perm_def supp_restrict0
        normal_quotient_add_well_defined[THEN sym]
        LCoset_rel_quotientI[of _ H]
  by    unfold_locales
        (force simp add: lcoset_perm_comp plus_permutation_abs_eq)

lemma natural_quotient_hom_image:
  "natural_quotient_hom H ` G = quotient_group H"
  unfolding quotient_group_def
  by        (force elim: LCoset_rel_quotientE intro: LCoset_rel_quotientI) 

lemma quotient_group_UN: "quotient_group H = (λg. ⌈g|H⌉) ` G"
  using natural_quotient_hom_image by auto

lemma quotient_identity_rule: "⟦ Subgroup H; normal H; h∈H ⟧ ⟹ ⌈h|H⌉ = 0"
  using lcoset_perm_def
  by    (simp add: trivial_lcoset_perm zero_permutation.abs_eq)
  
lemma quotient_group_lift_to_quotient_set:
  "⟦ Subgroup H; normal H; g∈G ⟧ ⟹ (⌈g|H⌉) → H = LCoset_rel H `` {g}"
  using LCoset_rel_quotientI
        BinOpSetGroup.G_perm_apply_identity[
          OF BinOpSetGroup_normal_quotient
        ]
  by    simp

end (* context Group *)

subsubsection ‹The induced homomorphism on a quotient group›

text ‹
  A normal subgroup contained in the kernel of a homomorphism gives rise to a homomorphism on the
  quotient group by that subgroup. When the subgroup is the kernel itself (which is always normal),
  we obtain an isomorphism on the quotient.
›

context GroupHom
begin

lemma respects_Ker_lcosets: "H ⊆ Ker ⟹ T respects (LCoset_rel H)"
  using     uminus_add_in_Ker_eq_eq_im
  unfolding lcoset_rel_def
  by        (blast intro: congruentI)

abbreviation "quotient_hom H ≡
  BinOpSetGroup.lift_hom (quotient_set H) (+) (quotientfun T)"

lemmas normal_subgroup_quotientfun_classrep_equality =
  quotientfun_classrep_equality[
    OF subgroup_refl_on_LCoset_rel, OF _ respects_Ker_lcosets
  ]

lemma quotient_hom_im:
  "⟦ Subgroup H; normal H; H ⊆ Ker; g∈G ⟧ ⟹ quotient_hom H (⌈g|H⌉) = T g"
  using quotient_group_def quotient_group_UN quotient_group_lift_to_quotient_set
        BinOpSetGroup.inv_correspondence_conv_apply[
          OF BinOpSetGroup_normal_quotient
        ]
        normal_subgroup_quotientfun_classrep_equality
  by    auto

lemma quotient_hom:
  assumes "Subgroup H" "normal H" "H ⊆ Ker"
  shows   "GroupHom (quotient_group H) (quotient_hom H)"
  unfolding quotient_group_def
proof (
  rule BinOpSetGroup.lift_hom, rule BinOpSetGroup_normal_quotient, rule assms(1),
  rule assms(2)
)
  from assms
    show  "∀x ∈ quotient_set H. ∀y ∈ quotient_set H.
            quotientfun T (x + y) = quotientfun T x + quotientfun T y"
    using normal_quotient_add_well_defined normal_subgroup_quotientfun_classrep_equality
          add_closed hom
    by    (fastforce elim: LCoset_rel_quotientE)
qed

end (* context GroupHom *)


subsection ‹Free groups›

subsubsection ‹Words in letters of @{type signed} type›

paragraph ‹Definitions and basic fact›

text ‹
  We pair elements of some type with type @{typ bool}, where the @{typ bool} part of the pair
  indicates inversion.
›

abbreviation "pairtrue  ≡ λs. (s,True)"
abbreviation "pairfalse ≡ λs. (s,False)"

abbreviation flip_signed :: "'a signed ⇒ 'a signed"
  where "flip_signed ≡ apsnd (λb. ¬b)"

abbreviation nflipped_signed :: "'a signed ⇒ 'a signed ⇒ bool"
  where "nflipped_signed x y ≡ y ≠ flip_signed x"

lemma flip_signed_order2: "flip_signed (flip_signed x) = x"
  using apsnd_conv[of "λb. ¬b" "fst x" "snd x"] by simp

abbreviation charpair :: "'a::uminus set ⇒ 'a ⇒ 'a signed"
  where "charpair S s ≡ if s∈S then (s,True) else (-s,False)"

lemma map_charpair_uniform:
  "ss∈lists S ⟹ map (charpair S) ss = map pairtrue ss"
  by (induct ss) auto

lemma fst_set_map_charpair_un_uminus:
  fixes ss :: "'a::group_add list"
  shows "ss∈lists (S ∪ uminus ` S) ⟹ fst ` set (map (charpair S) ss) ⊆ S"
  by (induct ss) auto

abbreviation apply_sign :: "('a⇒'b::uminus) ⇒ 'a signed ⇒ 'b"
  where "apply_sign f x ≡ (if snd x then f (fst x) else - f (fst x))"

text ‹
  A word in such pairs will be considered proper if it does not contain consecutive letters that
  have opposite signs (and so are considered inverse), since such consecutive letters would be
  cancelled in a group.
›

abbreviation proper_signed_list :: "'a signed list ⇒ bool"
  where "proper_signed_list ≡ binrelchain nflipped_signed"

lemma proper_map_flip_signed:
  "proper_signed_list xs ⟹ proper_signed_list (map flip_signed xs)"
  by (induct xs rule: list_induct_CCons) auto

lemma proper_rev_map_flip_signed:
  "proper_signed_list xs ⟹ proper_signed_list (rev (map flip_signed xs))"
  using proper_map_flip_signed binrelchain_sym_rev[of nflipped_signed] by fastforce

lemma uniform_snd_imp_proper_signed_list:
  "snd ` set xs ⊆ {b} ⟹ proper_signed_list xs"
proof (induct xs rule: list_induct_CCons)
  case CCons thus ?case by force
qed auto

lemma proper_signed_list_map_uniform_snd:
  "proper_signed_list (map (λs. (s,b)) as)"
  using uniform_snd_imp_proper_signed_list[of _ b] by force

paragraph ‹Algebra›

text ‹
  Addition is performed by appending words and recursively removing any newly created adjacent
  pairs of inverse letters. Since we will only ever be adding proper words, we only need to care
  about newly created adjacent inverse pairs in the middle.
›

function prappend_signed_list :: "'a signed list ⇒ 'a signed list ⇒ 'a signed list"
  where "prappend_signed_list xs [] = xs"
      | "prappend_signed_list [] ys = ys"
      | "prappend_signed_list (xs@[x]) (y#ys) = (
          if y = flip_signed x then prappend_signed_list xs ys else xs @ x # y # ys
        )"
  by (auto) (rule two_prod_lists_cases_snoc_Cons)
  termination by (relation "measure (λ(xs,ys). length xs + length ys)") auto

lemma proper_prappend_signed_list:
  "proper_signed_list xs ⟹ proper_signed_list ys
    ⟹ proper_signed_list (prappend_signed_list xs ys)"
proof (induct xs ys rule: list_induct2_snoc_Cons)
  case (snoc_Cons xs x y ys)
  show ?case
  proof (cases "y = flip_signed x")
    case True with snoc_Cons show ?thesis
      using binrelchain_append_reduce1[of nflipped_signed]
            binrelchain_Cons_reduce[of nflipped_signed y]
      by    auto
  next
    case False with snoc_Cons(2,3) show ?thesis
      using binrelchain_join[of nflipped_signed] by simp
  qed
qed auto

lemma fully_prappend_signed_list:
  "prappend_signed_list (rev (map flip_signed xs)) xs = []"
  by (induct xs) auto

lemma prappend_signed_list_single_Cons:
  "prappend_signed_list [x] (y#ys) = (if y = flip_signed x then ys else x#y#ys)"
  using prappend_signed_list.simps(3)[of "[]" x] by simp

lemma prappend_signed_list_map_uniform_snd:
  "prappend_signed_list (map (λs. (s,b)) xs) (map (λs. (s,b)) ys) =
    map (λs. (s,b)) xs @ map (λs. (s,b)) ys"
  by (cases xs ys rule: two_lists_cases_snoc_Cons) auto

lemma prappend_signed_list_assoc_conv_snoc2Cons:
  assumes "proper_signed_list (xs@[y])" "proper_signed_list (y#ys)"
  shows   "prappend_signed_list (xs@[y]) ys = prappend_signed_list xs (y#ys)"
proof (cases xs ys rule: two_lists_cases_snoc_Cons')
  case Nil1 with assms(2) show ?thesis
    by (simp add: prappend_signed_list_single_Cons)
next
  case Nil2 with assms(1) show ?thesis
    using binrelchain_append_reduce2 by force
next
  case (snoc_Cons as a b bs)
  with assms show ?thesis 
    using prappend_signed_list.simps(3)[of "as@[a]"]
          binrelchain_append_reduce2[of nflipped_signed as "[a,y]"]
    by    simp
qed simp

lemma prappend_signed_list_assoc:
  "⟦ proper_signed_list xs; proper_signed_list ys; proper_signed_list zs ⟧ ⟹
    prappend_signed_list (prappend_signed_list xs ys) zs =
      prappend_signed_list xs (prappend_signed_list ys zs)"
proof (induct xs ys zs rule: list_induct3_snoc_Conssnoc_Cons_pairwise)
  case (snoc_single_Cons xs x y z zs)
  thus ?case
    using prappend_signed_list.simps(3)[of "[]" y]
          prappend_signed_list.simps(3)[of "xs@[x]"]
    by    (cases "y = flip_signed x" "z = flip_signed y" rule: two_cases)
          (auto simp add:
            flip_signed_order2 prappend_signed_list_assoc_conv_snoc2Cons
          )
next
  case (snoc_Conssnoc_Cons xs x y ys w z zs)
  thus ?case
    using binrelchain_Cons_reduce[of nflipped_signed y "ys@[w]"]
          binrelchain_Cons_reduce[of nflipped_signed z zs]
          binrelchain_append_reduce1[of nflipped_signed xs]
          binrelchain_append_reduce1[of nflipped_signed "y#ys"]
          binrelchain_Conssnoc_reduce[of nflipped_signed y ys]
          prappend_signed_list.simps(3)[of "y#ys"]
          prappend_signed_list.simps(3)[of "xs@x#y#ys"]
    by    (cases "y = flip_signed x" "z = flip_signed w" rule: two_cases) auto
qed auto

lemma fst_set_prappend_signed_list:
  "fst ` set (prappend_signed_list xs ys) ⊆ fst ` (set xs ∪ set ys)"
  by (induct xs ys rule: list_induct2_snoc_Cons) auto

lemma collapse_flipped_signed:
  "prappend_signed_list [(s,b)] [(s,¬b)] = []"
  using prappend_signed_list.simps(3)[of "[]" "(s,b)"] by simp



subsubsection ‹The collection of proper signed lists as a type›

text ‹
  Here we create a type out of the collection of proper signed lists. This type will be of class
  @{class group_add}, with the empty list as zero, the modified append operation
  @{const prappend_signed_list} as addition, and inversion performed by flipping the signs of the
  elements in the list and then reversing the order.
›

paragraph ‹Type definition, instantiations, and instances›

text ‹Here we define the type and instantiate it with respect to various type classes.›

typedef 'a freeword = "{as::'a signed list. proper_signed_list as}"
  morphisms freeword Abs_freeword
  using binrelchain.simps(1) by fast

text ‹
  These two functions act as the natural injections of letters and words in the letter type into
  the @{type freeword} type.
›

abbreviation Abs_freeletter :: "'a ⇒ 'a freeword"
  where "Abs_freeletter s ≡ Abs_freeword [pairtrue s]"

abbreviation Abs_freelist :: "'a list ⇒ 'a freeword"
  where "Abs_freelist as ≡ Abs_freeword (map pairtrue as)"

abbreviation Abs_freelistfst :: "'a signed list ⇒ 'a freeword"
  where "Abs_freelistfst xs ≡ Abs_freelist (map fst xs)"

setup_lifting type_definition_freeword

instantiation freeword :: (type) zero
begin
lift_definition zero_freeword :: "'a freeword" is "[]::'a signed list" by simp
instance ..
end

instantiation freeword :: (type) plus
begin
lift_definition plus_freeword :: "'a freeword ⇒ 'a freeword ⇒ 'a freeword"
  is    "prappend_signed_list"
  using proper_prappend_signed_list
  by    fast
instance ..
end

instantiation freeword :: (type) uminus
begin
lift_definition uminus_freeword :: "'a freeword ⇒ 'a freeword"
  is "λxs. rev (map flip_signed xs)"
  by (rule proper_rev_map_flip_signed)
instance ..
end

instantiation freeword :: (type) minus
begin
lift_definition minus_freeword :: "'a freeword ⇒ 'a freeword ⇒ 'a freeword"
  is "λxs ys. prappend_signed_list xs (rev (map flip_signed ys))"
  using proper_rev_map_flip_signed proper_prappend_signed_list by fast
instance ..
end

instance freeword :: (type) semigroup_add
proof
  fix a b c :: "'a freeword" show "a + b + c = a + (b + c)"
    using prappend_signed_list_assoc[of "freeword a" "freeword b" "freeword c"]
    by    transfer simp
qed

instance freeword :: (type) monoid_add
proof
  fix a b c :: "'a freeword"
  show "0 + a = a" by transfer simp
  show "a + 0 = a" by transfer simp
qed

instance freeword :: (type) group_add
proof
  fix a b :: "'a freeword"
  show "- a + a = 0"
    using fully_prappend_signed_list[of "freeword a"] by transfer simp
  show "a + - b = a - b" by transfer simp
qed

paragraph ‹Basic algebra and transfer facts in the @{type freeword} type›

text ‹
  Here we record basic algebraic manipulations for the @{type freeword} type as well as various
  transfer facts for dealing with representations of elements of @{type freeword} type as lists of
  signed letters.
›

abbreviation Abs_freeletter_add :: "'a ⇒ 'a ⇒ 'a freeword" (infixl "[+]" 65)
  where "s [+] t ≡ Abs_freeletter s + Abs_freeletter t"

lemma Abs_freeword_Cons:
  assumes "proper_signed_list (x#xs)"
  shows "Abs_freeword (x#xs) = Abs_freeword [x] + Abs_freeword xs"
proof (cases xs)
  case Nil thus ?thesis
    using add_0_right[of "Abs_freeword [x]"] by (simp add: zero_freeword.abs_eq)
next
  case (Cons y ys) 
  with assms
    have  "freeword (Abs_freeword (x#xs)) =
            freeword (Abs_freeword [x] + Abs_freeword xs)"
    by    (simp add:
            plus_freeword.rep_eq Abs_freeword_inverse
            prappend_signed_list_single_Cons
          )
  thus ?thesis using freeword_inject by fast
qed

lemma Abs_freelist_Cons: "Abs_freelist (x#xs) = Abs_freeletter x + Abs_freelist xs"
  using proper_signed_list_map_uniform_snd[of True "x#xs"] Abs_freeword_Cons
  by    simp

lemma plus_freeword_abs_eq:
  "proper_signed_list xs ⟹ proper_signed_list ys ⟹
    Abs_freeword xs + Abs_freeword ys = Abs_freeword (prappend_signed_list xs ys)"
  using plus_freeword.abs_eq unfolding eq_onp_def by simp

lemma Abs_freeletter_add: "s [+] t = Abs_freelist [s,t]"
  using Abs_freelist_Cons[of s "[t]"] by simp

lemma uminus_freeword_Abs_eq:
  "proper_signed_list xs ⟹
    - Abs_freeword xs = Abs_freeword (rev (map flip_signed xs))"
  using uminus_freeword.abs_eq unfolding eq_onp_def by simp

lemma uminus_Abs_freeword_singleton:
  "- Abs_freeword [(s,b)] = Abs_freeword [(s,¬ b)]"
  using uminus_freeword_Abs_eq[of "[(s,b)]"] by simp

lemma Abs_freeword_append_uniform_snd:
  "Abs_freeword (map (λs. (s,b)) (xs@ys)) =
    Abs_freeword (map (λs. (s,b)) xs) + Abs_freeword (map (λs. (s,b)) ys)"
  using proper_signed_list_map_uniform_snd[of b xs]
        proper_signed_list_map_uniform_snd[of b ys]
        plus_freeword_abs_eq prappend_signed_list_map_uniform_snd[of b xs ys]
  by    force

lemmas Abs_freelist_append = Abs_freeword_append_uniform_snd[of True]

lemma Abs_freelist_append_append:
  "Abs_freelist (xs@ys@zs) = Abs_freelist xs + Abs_freelist ys + Abs_freelist zs"
  using Abs_freelist_append[of "xs@ys"] Abs_freelist_append by simp

lemma Abs_freelist_inverse: "freeword (Abs_freelist as) = map pairtrue as"
  using proper_signed_list_map_uniform_snd Abs_freeword_inverse by fast

lemma Abs_freeword_singleton_conv_apply_sign_freeletter:
  "Abs_freeword [x] = apply_sign Abs_freeletter x"
  by (cases x) (auto simp add: uminus_Abs_freeword_singleton)

lemma Abs_freeword_conv_freeletter_sum_list:
  "proper_signed_list xs ⟹
    Abs_freeword xs = (∑x←xs. apply_sign Abs_freeletter x)"
proof (induct xs)
  case (Cons x xs) thus ?case
    using Abs_freeword_Cons[of x] binrelchain_Cons_reduce[of _ x]
    by (simp add: Abs_freeword_singleton_conv_apply_sign_freeletter)
qed (simp add: zero_freeword.abs_eq)

lemma freeword_conv_freeletter_sum_list:
  "x = (∑s←freeword x. apply_sign Abs_freeletter s)"
  using Abs_freeword_conv_freeletter_sum_list[of "freeword x"] freeword
  by    (auto simp add: freeword_inverse)

lemma Abs_freeletter_prod_conv_Abs_freeword:
  "snd x ⟹ Abs_freeletter (fst x) = Abs_freeword [x]"
  using prod_eqI[of x "pairtrue (fst x)"] by simp


subsubsection ‹Lifts of functions on the letter type›

text ‹
  Here we lift functions on the letter type to type @{type freeword}. In particular, we are
  interested in the case where the function being lifted has codomain of class @{class group_add}.
›

paragraph ‹The universal property›

text ‹
  The universal property for free groups says that every function from the letter type to some
  @{class group_add} type gives rise to a unique homomorphism.
›

lemma extend_map_to_freeword_hom':
  fixes   f :: "'a ⇒ 'b::group_add"
  defines h: "h::'a signed ⇒ 'b ≡ λ(s,b). if b then f s else - (f s)"
  defines g: "g::'a signed list ⇒ 'b ≡ λxs. sum_list (map h xs)"
  shows   "g (prappend_signed_list xs ys) = g xs + g ys"
proof (induct xs ys rule: list_induct2_snoc_Cons)
  case (snoc_Cons xs x y ys)
  show ?case
  proof (cases "y = flip_signed x")
    case True
    with h have "h y = - h x"
      using split_beta'[of "λs b. if b then f s else - (f s)"] by simp
    with g have "g (xs @ [x]) + g (y # ys) = g xs + g ys"
      by (simp add: algebra_simps)
    with True snoc_Cons show ?thesis by simp
  next
    case False with g show ?thesis
      using sum_list.append[of "map h (xs@[x])" "map h (y#ys)"] by simp
  qed
qed (auto simp add: h g)

lemma extend_map_to_freeword_hom1:
  fixes   f :: "'a ⇒ 'b::group_add"
  defines "h::'a signed ⇒ 'b ≡ λ(s,b). if b then f s else - (f s)"
  defines "g::'a freeword ⇒ 'b ≡ λx. sum_list (map h (freeword x))"
  shows   "g (Abs_freeletter s) = f s"
  using   assms
  by      (simp add: Abs_freeword_inverse)

lemma extend_map_to_freeword_hom2:
  fixes   f :: "'a ⇒ 'b::group_add"
  defines "h::'a signed ⇒ 'b ≡ λ(s,b). if b then f s else - (f s)"
  defines "g::'a freeword ⇒ 'b ≡ λx. sum_list (map h (freeword x))"
  shows   "UGroupHom g"
  using   assms
  by      (
            auto intro: UGroupHomI
            simp add: plus_freeword.rep_eq extend_map_to_freeword_hom'
          )

lemma uniqueness_of_extended_map_to_freeword_hom':
  fixes   f :: "'a ⇒ 'b::group_add"
  defines h: "h::'a signed ⇒ 'b ≡ λ(s,b). if b then f s else - (f s)"
  defines g: "g::'a signed list ⇒ 'b ≡ λxs. sum_list (map h xs)"
  assumes singles: "⋀s. k [(s,True)] = f s"
  and     adds   : "⋀xs ys. proper_signed_list xs ⟹ proper_signed_list ys
            ⟹ k (prappend_signed_list xs ys) = k xs + k ys"
  shows   "proper_signed_list xs ⟹ k xs = g xs"
proof-
  have knil: "k [] = 0" using adds[of "[]" "[]"] add.assoc[of "k []" "k []" "- k []"] by simp
  have ksingle: "⋀x. k [x] = g [x]"
  proof-
    fix x :: "'a signed"
    obtain s b where x: "x = (s,b)" by fastforce
    show "k [x] = g [x]"
    proof (cases b)
      case False
      from adds x singles
        have  "k (prappend_signed_list [x] [(s,True)]) = k [x] + f s"
        by    simp
      moreover have "prappend_signed_list [(s,False)] [(s,True)] = []"
        using collapse_flipped_signed[of s False] by simp
      ultimately have "- f s = k [x] + f s + - f s" using x False knil by simp
      with x False g h show "k [x] = g [x]" by (simp add: algebra_simps)
    qed (simp add: x g h singles)
  qed
  show "proper_signed_list xs ⟹ k xs = g xs"
  proof (induct xs rule: list_induct_CCons)
    case (CCons x y xs)
    with g h show ?case
      using adds[of "[x]" "y#xs"]
      by    (simp add:
              prappend_signed_list_single_Cons
              ksingle extend_map_to_freeword_hom'
            )
  qed (auto simp add: g h knil ksingle)
qed

lemma uniqueness_of_extended_map_to_freeword_hom:
  fixes   f :: "'a ⇒ 'b::group_add"
  defines "h::'a signed ⇒ 'b ≡ λ(s,b). if b then f s else - (f s)"
  defines "g::'a freeword ⇒ 'b ≡ λx. sum_list (map h (freeword x))"
  assumes k: "k ∘ Abs_freeletter = f" "UGroupHom k"
  shows   "k = g"
proof
  fix x::"'a freeword"
  define k' where k': "k' ≡ k ∘ Abs_freeword"
  have "k' (freeword x) = g x" unfolding h_def g_def
  proof (rule uniqueness_of_extended_map_to_freeword_hom')
    from k' k(1) show "⋀s. k' [pairtrue s] = f s" by auto
    show "⋀xs ys. proper_signed_list xs ⟹ proper_signed_list ys
            ⟹ k' (prappend_signed_list xs ys) = k' xs + k' ys"
    proof-
      fix xs ys :: "'a signed list"
      assume xsys: "proper_signed_list xs" "proper_signed_list ys"
      with k'
        show  "k' (prappend_signed_list xs ys) = k' xs + k' ys"
        using UGroupHom.hom[OF k(2), of "Abs_freeword xs" "Abs_freeword ys"]
        by    (simp add: plus_freeword_abs_eq)      
    qed
    show "proper_signed_list (freeword x)" using freeword by fast
  qed
  with k' show "k x = g x" using freeword_inverse[of x] by simp
qed

theorem universal_property:
  fixes f :: "'a ⇒ 'b::group_add"
  shows "∃!g::'a freeword⇒'b. g ∘ Abs_freeletter = f ∧ UGroupHom g"
proof
  define h where h: "h ≡ λ(s,b). if b then f s else - (f s)"
  define g where g: "g ≡ λx. sum_list (map h (freeword x))"
  from g h show "g ∘ Abs_freeletter = f ∧ UGroupHom g"
    using extend_map_to_freeword_hom1[of f] extend_map_to_freeword_hom2
    by    auto
  from g h show "⋀k. k ∘ Abs_freeletter = f ∧ UGroupHom k ⟹ k = g"
    using uniqueness_of_extended_map_to_freeword_hom by auto
qed

paragraph ‹Properties of homomorphisms afforded by the universal property›

text ‹
  The lift of a function on the letter set is the unique additive function on @{type freeword}
  that agrees with the original function on letters.
›

definition freeword_funlift :: "('a ⇒ 'b::group_add) ⇒ ('a freeword⇒'b::group_add)"
  where "freeword_funlift f ≡ (THE g. g ∘ Abs_freeletter = f ∧ UGroupHom g)"

lemma additive_freeword_funlift: "UGroupHom (freeword_funlift f)"
  using theI'[OF universal_property, of f] unfolding freeword_funlift_def by simp

lemma freeword_funlift_Abs_freeletter: "freeword_funlift f (Abs_freeletter s) = f s"
  using     theI'[OF universal_property, of f]
            comp_apply[of "freeword_funlift f" Abs_freeletter]
  unfolding freeword_funlift_def
  by        fastforce

lemmas freeword_funlift_add         = UGroupHom.hom        [OF additive_freeword_funlift]
lemmas freeword_funlift_0           = UGroupHom.im_zero    [OF additive_freeword_funlift]
lemmas freeword_funlift_uminus      = UGroupHom.im_uminus  [OF additive_freeword_funlift]
lemmas freeword_funlift_diff        = UGroupHom.im_diff    [OF additive_freeword_funlift]
lemmas freeword_funlift_lconjby     = UGroupHom.im_lconjby [OF additive_freeword_funlift]

lemma freeword_funlift_uminus_Abs_freeletter:
  "freeword_funlift f (Abs_freeword [(s,False)]) = - f s"
  using freeword_funlift_uminus[of f "Abs_freeword [(s,False)]"]
        uminus_freeword_Abs_eq[of "[(s,False)]"]
        freeword_funlift_Abs_freeletter[of f]
  by    simp

lemma freeword_funlift_Abs_freeword_singleton:
  "freeword_funlift f (Abs_freeword [x]) = apply_sign f x"
proof-
  obtain s b where x: "x = (s,b)" by fastforce
  thus ?thesis
    using freeword_funlift_Abs_freeletter freeword_funlift_uminus_Abs_freeletter
    by    (cases b) auto
qed

lemma freeword_funlift_Abs_freeword_Cons:
  assumes "proper_signed_list (x#xs)"
  shows   "freeword_funlift f (Abs_freeword (x#xs)) =
            apply_sign f x + freeword_funlift f (Abs_freeword xs)"
proof-
  from assms
    have "freeword_funlift f (Abs_freeword (x#xs)) =
            freeword_funlift f (Abs_freeword [x]) +
            freeword_funlift f (Abs_freeword xs)"
    using Abs_freeword_Cons[of x xs] freeword_funlift_add by simp
  thus ?thesis
    using freeword_funlift_Abs_freeword_singleton[of f x] by simp
qed

lemma freeword_funlift_Abs_freeword:
  "proper_signed_list xs ⟹ freeword_funlift f (Abs_freeword xs) =
    (∑x←xs. apply_sign f x)"
proof (induct xs)
  case (Cons x xs) thus ?case
    using freeword_funlift_Abs_freeword_Cons[of _ _ f]
          binrelchain_Cons_reduce[of _ x xs]
    by    simp
qed (simp add: zero_freeword.abs_eq[THEN sym] freeword_funlift_0)

lemma freeword_funlift_Abs_freelist:
  "freeword_funlift f (Abs_freelist xs) = (∑x←xs. f x)"
proof (induct xs)
  case (Cons x xs) thus ?case
    using Abs_freelist_Cons[of x xs]
    by    (simp add: freeword_funlift_add freeword_funlift_Abs_freeletter)
qed (simp add: zero_freeword.abs_eq[THEN sym] freeword_funlift_0)

lemma freeword_funlift_im':
  "proper_signed_list xs ⟹ fst ` set xs ⊆ S ⟹
    freeword_funlift f (Abs_freeword xs) ∈ ⟨f`S⟩"
proof (induct xs)
  case Nil
  have "Abs_freeword ([]::'a signed list) = (0::'a freeword)"
    using zero_freeword.abs_eq[THEN sym] by simp
  thus "freeword_funlift f (Abs_freeword ([]::'a signed list)) ∈ ⟨f`S⟩"
    using freeword_funlift_0[of f] genby_0_closed by simp
next
  case (Cons x xs)
  define y where y: "y ≡ apply_sign f x"
  define z where z: "z ≡ freeword_funlift f (Abs_freeword xs)"
  from Cons(3) have "fst ` set xs ⊆ S" by simp
  with z Cons(1,2) have "z ∈ ⟨f`S⟩" using binrelchain_Cons_reduce by fast
  with y Cons(3) have "y + z ∈ ⟨f`S⟩"
    using genby_genset_closed[of _ "f`S"]
          genby_uminus_closed genby_add_closed[of y]
    by    fastforce
  with Cons(2) y z show ?case
    using freeword_funlift_Abs_freeword_Cons
          subst[
            OF  sym,
            of  "freeword_funlift f (Abs_freeword (x#xs))" "y+z"
                "λb. b∈⟨f`S⟩"
          ]
    by    fast
qed


subsubsection ‹Free groups on a set›

text ‹
  We now take the free group on a set to be the set in the @{type freeword} type with letters
  restricted to the given set.
›

paragraph ‹Definition and basic facts›

text ‹
  Here we define the set of elements of the free group over a set of letters, and record basic
  facts about that set.
›

definition FreeGroup :: "'a set ⇒ 'a freeword set"
  where "FreeGroup S ≡ {x. fst ` set (freeword x) ⊆ S}"

lemma FreeGroupI_transfer:
  "proper_signed_list xs ⟹ fst ` set xs ⊆ S ⟹ Abs_freeword xs ∈ FreeGroup S"
  using Abs_freeword_inverse unfolding FreeGroup_def by fastforce

lemma FreeGroupD: "x ∈ FreeGroup S ⟹ fst ` set (freeword x) ⊆ S"
  using FreeGroup_def by fast

lemma FreeGroupD_transfer:
  "proper_signed_list xs ⟹ Abs_freeword xs ∈ FreeGroup S ⟹ fst ` set xs ⊆ S"
  using Abs_freeword_inverse unfolding FreeGroup_def by fastforce

lemma FreeGroupD_transfer':
  "Abs_freelist xs ∈ FreeGroup S ⟹ xs ∈ lists S"
  using proper_signed_list_map_uniform_snd FreeGroupD_transfer by fastforce

lemma FreeGroup_0_closed: "0 ∈ FreeGroup S"
proof-
  have "(0::'a freeword) = Abs_freeword []" using zero_freeword.abs_eq by fast
  moreover have "Abs_freeword [] ∈ FreeGroup S"
    using FreeGroupI_transfer[of "[]"] by simp
  ultimately show ?thesis by simp
qed

lemma FreeGroup_diff_closed:
  assumes "x ∈ FreeGroup S" "y ∈ FreeGroup S"
  shows   "x-y ∈ FreeGroup S"
proof-
  define xs where xs: "xs ≡ freeword x"
  define ys where ys: "ys ≡ freeword y"
  have "freeword (x-y) =
        prappend_signed_list (freeword x) (rev (map flip_signed (freeword y)))"
    by transfer simp
  hence "fst ` set (freeword (x-y)) ⊆ fst ` (set (freeword x) ∪ set (freeword y))"
    using fst_set_prappend_signed_list by force
  with assms show ?thesis unfolding FreeGroup_def by fast
qed

lemma FreeGroup_Group: "Group (FreeGroup S)"
  using FreeGroup_0_closed FreeGroup_diff_closed by unfold_locales fast

lemmas FreeGroup_add_closed    = Group.add_closed    [OF FreeGroup_Group]
lemmas FreeGroup_uminus_closed = Group.uminus_closed [OF FreeGroup_Group]

lemmas FreeGroup_genby_set_lconjby_set_rconjby_closed =
  Group.genby_set_lconjby_set_rconjby_closed[OF FreeGroup_Group]

lemma Abs_freelist_in_FreeGroup: "ss ∈ lists S ⟹ Abs_freelist ss ∈ FreeGroup S"
  using proper_signed_list_map_uniform_snd by (fastforce intro: FreeGroupI_transfer)

lemma Abs_freeletter_in_FreeGroup_iff: "(Abs_freeletter s ∈ FreeGroup S) = (s∈S)"
  using Abs_freeword_inverse[of "[pairtrue s]"] unfolding FreeGroup_def by simp

paragraph ‹Lifts of functions from the letter set to some type of class @{class group_add}›

text ‹
  We again obtain a universal property for functions from the (restricted) letter set to some type
  of class @{class group_add}.
›

abbreviation "res_freeword_funlift f S ≡
                restrict0 (freeword_funlift f) (FreeGroup S)"

lemma freeword_funlift_im: "x ∈ FreeGroup S ⟹ freeword_funlift f x ∈ ⟨f ` S⟩"
  using     freeword[of x] freeword_funlift_im'[of "freeword x"]
            freeword_inverse[of x]
  unfolding FreeGroup_def
  by        auto

lemma freeword_funlift_surj':
  "ys ∈ lists (f`S ∪ uminus`f`S) ⟹ sum_list ys ∈ freeword_funlift f ` FreeGroup S"
proof (induct ys)
  case Nil thus ?case using FreeGroup_0_closed freeword_funlift_0 by fastforce
next
  case (Cons y ys)
  from this obtain x
    where x: "x ∈ FreeGroup S" "sum_list ys = freeword_funlift f x"
    by    auto
  show "sum_list (y#ys) ∈ freeword_funlift f ` FreeGroup S"
  proof (cases "y ∈ f`S")
    case True
    from this obtain s where s: "s∈S" "y = f s" by fast
    from s(1) x(1) have "Abs_freeletter s + x ∈ FreeGroup S"
      using FreeGroupI_transfer[of _ S] FreeGroup_add_closed[of _ S] by force
    moreover from s(2) x(2)
      have  "freeword_funlift f (Abs_freeletter s + x) = sum_list (y#ys)"
      using freeword_funlift_add[of f] freeword_funlift_Abs_freeletter
      by    simp
    ultimately show ?thesis by force
  next
    case False
    with Cons(2) obtain s where s: "s∈S" "y = - f s" by auto
    from s(1) x(1) have "Abs_freeword [(s,False)] + x ∈ FreeGroup S"
      using FreeGroupI_transfer[of _ S] FreeGroup_add_closed[of _ S] by force
    moreover from s(2) x(2)
      have  "freeword_funlift f (Abs_freeword [(s,False)] + x) = sum_list (y#ys)"
      using freeword_funlift_add[of f] freeword_funlift_uminus_Abs_freeletter
      by    simp
    ultimately show ?thesis by force
  qed
qed

lemma freeword_funlift_surj:
  fixes f :: "'a ⇒ 'b::group_add"
  shows "freeword_funlift f ` FreeGroup S = ⟨f`S⟩"
proof (rule seteqI)
  show "⋀a. a ∈ freeword_funlift f ` FreeGroup S ⟹ a ∈ ⟨f`S⟩"
    using freeword_funlift_im by auto
next
  fix w assume "w∈⟨f`S⟩"
  from this obtain ys where ys: "ys ∈ lists (f`S ∪ uminus`f`S)" "w = sum_list ys"
    using genby_eq_sum_lists[of "f`S"] by auto
  thus "w ∈ freeword_funlift f ` FreeGroup S" using freeword_funlift_surj' by simp
qed

lemma hom_restrict0_freeword_funlift:
  "GroupHom (FreeGroup S) (res_freeword_funlift f S)"
  using UGroupHom.restrict0 additive_freeword_funlift FreeGroup_Group
  by    auto

lemma uniqueness_of_restricted_lift:
  assumes "GroupHom (FreeGroup S) T" "∀s∈S. T (Abs_freeletter s) = f s"
  shows   "T = res_freeword_funlift f S"
proof
  fix x
  define F where "F ≡ res_freeword_funlift f S"
  define u_Abs where "u_Abs ≡ λa::'a signed. apply_sign Abs_freeletter a"
  show "T x = F x"
  proof (cases "x ∈ FreeGroup S")
    case True
    have 1: "set (map u_Abs (freeword x)) ⊆ FreeGroup S"
      using u_Abs_def FreeGroupD[OF True]
            Abs_freeletter_in_FreeGroup_iff[of _ S]
            FreeGroup_uminus_closed
      by    auto
    moreover from u_Abs_def have  "x = (∑a←freeword x. u_Abs a)"
      using freeword_conv_freeletter_sum_list by fast
    ultimately
      have  "T x = (∑a←freeword x. T (u_Abs a))"
            "F x = (∑a←freeword x. F (u_Abs a))"
      using F_def
            GroupHom.im_sum_list_map[OF assms(1), of u_Abs "freeword x"]
            GroupHom.im_sum_list_map[
              OF hom_restrict0_freeword_funlift,
              of u_Abs "freeword x" S f
            ]
      by auto
    moreover have "∀a∈set (freeword x). T (u_Abs a) = F (u_Abs a)"
    proof
      fix a assume "a ∈ set (freeword x)"
      moreover define b where "b ≡ Abs_freeletter (fst a)"
      ultimately show "T (u_Abs a) = F (u_Abs a)"
        using F_def u_Abs_def True assms(2) FreeGroupD[of x S]
              GroupHom.im_uminus[OF assms(1)] 
              Abs_freeletter_in_FreeGroup_iff[of "fst a" S]
              GroupHom.im_uminus[OF hom_restrict0_freeword_funlift, of b S f]
              freeword_funlift_Abs_freeletter[of f]
        by    auto
    qed
    ultimately show ?thesis
      using F_def
            sum_list_map_cong[of "freeword x" "λs. T (u_Abs s)" "λs. F (u_Abs s)"]
      by    simp
  next
    case False
    with assms(1) F_def show ?thesis
      using hom_restrict0_freeword_funlift GroupHom.supp suppI_contra[of x T]
            suppI_contra[of x F]
      by    fastforce
  qed
qed

theorem FreeGroup_universal_property:
  fixes f :: "'a ⇒ 'b::group_add"
  shows "∃!T::'a freeword⇒'b. (∀s∈S. T (Abs_freeletter s) = f s) ∧
          GroupHom (FreeGroup S) T"
proof (rule ex1I, rule conjI)
  show "∀s∈S. res_freeword_funlift f S (Abs_freeletter s) = f s"
    using Abs_freeletter_in_FreeGroup_iff[of _ S] freeword_funlift_Abs_freeletter
    by    auto
  show "⋀T. (∀s∈S. T (Abs_freeletter s) = f s) ∧
          GroupHom (FreeGroup S) T ⟹
          T = restrict0 (freeword_funlift f) (FreeGroup S)"
    using uniqueness_of_restricted_lift by auto
qed (rule hom_restrict0_freeword_funlift)


subsubsection ‹Group presentations›

text ‹
  We now define a group presentation to be the quotient of a free group by the subgroup generated by
  all conjugates of a set of relators. We are most concerned with lifting functions on the letter
  set to the free group and with the associated induced homomorphisms on the quotient.
›

paragraph ‹A first group presentation locale and basic facts›

text ‹
  Here we define a locale that provides a way to construct a group by providing sets of generators
  and relator words.
›

locale GroupByPresentation =
  fixes   S :: "'a set"  ― ‹the set of generators›
  and     P :: "'a signed list set" ― ‹the set of relator words›
  assumes P_S: "ps∈P ⟹ fst ` set ps ⊆ S"
  and     proper_P: "ps∈P ⟹ proper_signed_list ps"
begin

abbreviation "P' ≡ Abs_freeword ` P" ― ‹the set of relators›
abbreviation "Q ≡ Group.normal_closure (FreeGroup S) P'"
― ‹the normal subgroup generated by relators inside the free group›
abbreviation "G ≡ Group.quotient_group (FreeGroup S) Q"

lemmas G_UN = Group.quotient_group_UN[OF FreeGroup_Group, of S Q]

lemma P'_FreeS: "P' ⊆ FreeGroup S"
  using P_S proper_P by (blast intro: FreeGroupI_transfer)

lemma relators: "P' ⊆ Q"
  using FreeGroup_0_closed genby_genset_subset by fastforce

lemmas lconjby_P'_FreeS =
  Group.set_lconjby_subset_closed[
    OF FreeGroup_Group _ P'_FreeS, OF basic_monos(1)
  ]

lemmas Q_FreeS =
  Group.genby_closed[OF FreeGroup_Group lconjby_P'_FreeS]

lemmas Q_subgroup_FreeS =
  Group.genby_subgroup[OF FreeGroup_Group lconjby_P'_FreeS]

lemmas normal_Q = Group.normal_closure[OF FreeGroup_Group, OF P'_FreeS]

lemmas natural_hom =
  Group.natural_quotient_hom[
    OF FreeGroup_Group Q_subgroup_FreeS normal_Q
  ]

lemmas natural_hom_image =
  Group.natural_quotient_hom_image[OF FreeGroup_Group, of S Q]

end (* context GroupByPresentation *)

paragraph ‹Functions on the quotient induced from lifted functions›

text ‹
  A function on the generator set into a type of class @{class group_add} lifts to a unique
  homomorphism on the free group. If this lift is trivial on relators, then it factors to a
  homomorphism of the group described by the generators and relators.
›

locale GroupByPresentationInducedFun = GroupByPresentation S P
  for     S :: "'a set"
  and     P :: "'a signed list set" ― ‹the set of relator words›
+ fixes   f :: "'a ⇒ 'b::group_add"
  assumes lift_f_trivial_P:
    "ps∈P ⟹ freeword_funlift f (Abs_freeword ps) = 0"
begin

abbreviation "lift_f ≡ freeword_funlift f"

definition induced_hom :: "'a freeword set permutation ⇒ 'b"
  where "induced_hom ≡ GroupHom.quotient_hom (FreeGroup S)
          (restrict0 lift_f (FreeGroup S)) Q"
  ― ‹the @{const restrict0} operation is really only necessary to make
@{const GroupByPresentationInducedFun.induced_hom} a @{const GroupHom}›
abbreviation "F ≡ induced_hom"

lemma lift_f_trivial_P': "p∈P' ⟹ lift_f p = 0"
  using lift_f_trivial_P by fast

lemma lift_f_trivial_lconjby_P': "p∈P' ⟹ lift_f (lconjby w p) = 0"
  using freeword_funlift_lconjby[of f] lift_f_trivial_P' by simp

lemma lift_f_trivial_Q: "q∈Q ⟹ lift_f q = 0"
proof (erule genby.induct, rule freeword_funlift_0)
  show "⋀s. s ∈ (⋃w ∈ FreeGroup S. lconjby w ` P') ⟹ lift_f s = 0"
    using lift_f_trivial_lconjby_P' by fast
next
  fix w w' :: "'a freeword" assume ww': "lift_f w = 0" "lift_f w' = 0"
  have "lift_f (w - w') = lift_f w - lift_f w'"
    using freeword_funlift_diff[of f w] by simp
  with ww' show "lift_f (w-w') = 0" by simp
qed

lemma lift_f_ker_Q: "Q ⊆ ker lift_f"
  using lift_f_trivial_Q unfolding ker_def by auto

lemma lift_f_Ker_Q: "Q ⊆ GroupHom.Ker (FreeGroup S) lift_f"
  using lift_f_ker_Q Q_FreeS by fast

lemma restrict0_lift_f_Ker_Q:
  "Q ⊆ GroupHom.Ker (FreeGroup S) (restrict0 lift_f (FreeGroup S))"
  using lift_f_Ker_Q ker_subset_ker_restrict0 by fast

lemma induced_hom_equality:
  "w ∈ FreeGroup S ⟹ F (⌈FreeGroup S|w|Q⌉) = lift_f w"
― ‹algebraic properties of the induced homomorphism could be proved using its properties as a group
  homomorphism, but it's generally easier to prove them using the algebraic properties of the lift
  via this lemma›
  unfolding induced_hom_def
  using     GroupHom.quotient_hom_im hom_restrict0_freeword_funlift
            Q_subgroup_FreeS normal_Q restrict0_lift_f_Ker_Q
  by        fastforce

lemma hom_induced_hom: "GroupHom G F"
  unfolding induced_hom_def
  using     GroupHom.quotient_hom hom_restrict0_freeword_funlift
            Q_subgroup_FreeS normal_Q restrict0_lift_f_Ker_Q
  by        fast

lemma induced_hom_Abs_freeletter_equality:
  "s∈S ⟹ F (⌈FreeGroup S|Abs_freeletter s|Q⌉) = f s"
  using Abs_freeletter_in_FreeGroup_iff[of s S]        
  by    (simp add: induced_hom_equality freeword_funlift_Abs_freeletter)

lemma uniqueness_of_induced_hom':
  defines "q ≡ Group.natural_quotient_hom (FreeGroup S) Q"
  assumes "GroupHom G T" "∀s∈S. T (⌈FreeGroup S|Abs_freeletter s|Q⌉) = f s"
  shows   "T ∘ q = F ∘ q"
proof-
  from assms have "T∘q = res_freeword_funlift f S"
    using natural_hom natural_hom_image Abs_freeletter_in_FreeGroup_iff[of _ S]
    by    (force intro: uniqueness_of_restricted_lift GroupHom.comp)
  moreover from q_def have "F ∘ q = res_freeword_funlift f S"
    using induced_hom_equality GroupHom.im_zero[OF hom_induced_hom]
    by    auto
  ultimately show ?thesis by simp  
qed

lemma uniqueness_of_induced_hom:
  assumes "GroupHom G T" "∀s∈S. T (⌈FreeGroup S|Abs_freeletter s|Q⌉) = f s"
  shows   "T = F"
proof
  fix x
  show "T x = F x"
  proof (cases "x∈G")
    case True
    define q where "q ≡ Group.natural_quotient_hom (FreeGroup S) Q"
    from True obtain w where "w ∈ FreeGroup S" "x = (⌈FreeGroup S|w|Q⌉)"
      using G_UN by fast
    with q_def have "T x = (T∘q) w" "F x = (F∘q) w" by auto
    with assms q_def show ?thesis using uniqueness_of_induced_hom' by simp
  next
    case False
    with assms(1) show ?thesis
      using hom_induced_hom GroupHom.supp suppI_contra[of x T]
            suppI_contra[of x F]
      by    fastforce
  qed
qed

theorem induced_hom_universal_property:
  "∃!F. GroupHom G F ∧ (∀s∈S. F (⌈FreeGroup S|Abs_freeletter s|Q⌉) = f s)"
  using hom_induced_hom induced_hom_Abs_freeletter_equality
        uniqueness_of_induced_hom
  by    blast

lemma induced_hom_Abs_freelist_conv_sum_list:
  "ss∈lists S ⟹ F (⌈FreeGroup S|Abs_freelist ss|Q⌉) = (∑s←ss. f s)"
  by  (simp add:
        Abs_freelist_in_FreeGroup induced_hom_equality freeword_funlift_Abs_freelist
      )

lemma induced_hom_surj: "F`G = ⟨f`S⟩"
proof (rule seteqI)
  show "⋀x. x∈F`G ⟹ x∈⟨f`S⟩"
    using G_UN induced_hom_equality freeword_funlift_surj[of f S] by auto
next
  fix x assume "x∈⟨f`S⟩"
  hence "x ∈ lift_f ` FreeGroup S" using freeword_funlift_surj[of f S] by fast
  thus "x ∈ F`G" using induced_hom_equality G_UN by force
qed

end (* context GroupByPresentationInducedFun *)

paragraph ‹Groups affording a presentation›

text ‹
  The locale @{const GroupByPresentation} allows the construction of a @{const Group} out of any
  type from a set of generating letters and a set of relator words in (signed) letters. The
  following locale concerns the question of when the @{const Group} generated by a set in class
  @{class group_add} is isomorphic to a group presentation.
›

locale GroupWithGeneratorsRelators =
  fixes S :: "'g::group_add set" ― ‹the set of generators›
  and   R :: "'g list set" ― ‹the set of relator words›
  assumes relators: "rs∈R ⟹ rs ∈ lists (S ∪ uminus ` S)"
                    "rs∈R ⟹ sum_list rs = 0"
                    "rs∈R ⟹ proper_signed_list (map (charpair S) rs)"
begin

abbreviation "P ≡ map (charpair S) ` R"
abbreviation "P' ≡ GroupByPresentation.P' P"
abbreviation "Q ≡ GroupByPresentation.Q S P"
abbreviation "G ≡ GroupByPresentation.G S P"
abbreviation "relator_freeword rs ≡ Abs_freeword (map (charpair S) rs)"
― ‹this maps R onto P'›

abbreviation "freeliftid ≡ freeword_funlift id"

abbreviation induced_id :: "'g freeword set permutation ⇒ 'g"
  where "induced_id ≡ GroupByPresentationInducedFun.induced_hom S P id"

lemma GroupByPresentation_S_P: "GroupByPresentation S P"
proof
  show "⋀ps. ps ∈ P ⟹ fst ` set ps ⊆ S"
    using fst_set_map_charpair_un_uminus relators(1) by fast
  show "⋀ps. ps ∈ P ⟹ proper_signed_list ps" using relators(3) by fast
qed

lemmas G_UN     = GroupByPresentation.G_UN[OF GroupByPresentation_S_P]
lemmas P'_FreeS = GroupByPresentation.P'_FreeS[OF GroupByPresentation_S_P]

lemma freeliftid_trivial_relator_freeword_R:
  "rs∈R ⟹ freeliftid (relator_freeword rs) = 0"
  using relators(2,3) freeword_funlift_Abs_freeword[of "map (charpair S) rs" id]
        sum_list_map_cong[of rs "(apply_sign id) ∘ (charpair S)" id]
  by    simp

lemma freeliftid_trivial_P: "ps∈P ⟹ freeliftid (Abs_freeword ps) = 0"
  using freeliftid_trivial_relator_freeword_R by fast

lemma GroupByPresentationInducedFun_S_P_id:
  "GroupByPresentationInducedFun S P id"
  by  (
        intro_locales, rule GroupByPresentation_S_P,
        unfold_locales, rule freeliftid_trivial_P
      )

lemma induced_id_Abs_freelist_conv_sum_list:
  "ss∈lists S ⟹ induced_id (⌈FreeGroup S|Abs_freelist ss|Q⌉) = sum_list ss"
  by  (simp add:
        GroupByPresentationInducedFun.induced_hom_Abs_freelist_conv_sum_list[
          OF GroupByPresentationInducedFun_S_P_id
        ]
      )

lemma lconj_relator_freeword_R:
  "⟦ rs∈R; proper_signed_list xs; fst ` set xs ⊆ S ⟧ ⟹
    lconjby (Abs_freeword xs) (relator_freeword rs) ∈ Q"
  by (blast intro: genby_genset_closed FreeGroupI_transfer)

lemma rconj_relator_freeword:
  assumes "rs∈R" "proper_signed_list xs" "fst ` set xs ⊆ S"
  shows   "rconjby (Abs_freeword xs) (relator_freeword rs) ∈ Q"
proof (rule genby_genset_closed, rule UN_I)
  show "- Abs_freeword xs ∈ FreeGroup S"
    using FreeGroupI_transfer[OF assms(2,3)] FreeGroup_uminus_closed by fast
  from assms(1)
    show  "rconjby (Abs_freeword xs) (relator_freeword rs) ∈
            lconjby (- Abs_freeword xs) ` Abs_freeword ` P"
    by    simp
qed

lemma lconjby_Abs_freelist_relator_freeword:
  "⟦ rs∈R; xs∈lists S ⟧ ⟹ lconjby (Abs_freelist xs) (relator_freeword rs) ∈ Q"
  using proper_signed_list_map_uniform_snd by (force intro: lconj_relator_freeword_R)

text ‹
  Here we record that the lift of the identity map to the free group on @{term S} induces a
  homomorphic surjection onto the group generated by @{term S} from the group presentation on
  @{term S}, subject to the same relations as the elements of @{term S}.
›

theorem induced_id_hom_surj: "GroupHom G induced_id" "induced_id ` G = ⟨S⟩"
  using GroupByPresentationInducedFun.hom_induced_hom[
          OF GroupByPresentationInducedFun_S_P_id
        ]
        GroupByPresentationInducedFun.induced_hom_surj[
          OF GroupByPresentationInducedFun_S_P_id
        ]
  by    auto

end (* context GroupWithGeneratorsRelators *)

locale GroupPresentation = GroupWithGeneratorsRelators S R
  for S :: "'g::group_add set" ― ‹the set of generators›
  and R :: "'g list set" ― ‹the set of relator words›
+ assumes induced_id_inj: "inj_on induced_id G"
begin

abbreviation "inv_induced_id ≡ the_inv_into G induced_id"

lemma inv_induced_id_sum_list_S:
  "ss ∈ lists S ⟹ inv_induced_id (sum_list ss) = (⌈FreeGroup S|Abs_freelist ss|Q⌉)"
  using G_UN induced_id_inj induced_id_Abs_freelist_conv_sum_list
        Abs_freelist_in_FreeGroup
  by    (blast intro: the_inv_into_f_eq)

end (* GroupPresentation *)

subsection ‹Words over a generating set›

text ‹
  Here we gather the necessary constructions and facts for studying a group generated by some set
  in terms of words in the generators.
›

context monoid_add
begin

abbreviation "word_for A a as ≡ as ∈ lists A ∧ sum_list as = a"

definition reduced_word_for :: "'a set ⇒ 'a ⇒ 'a list ⇒ bool"
  where "reduced_word_for A a as ≡ is_arg_min length (word_for A a) as"

abbreviation "reduced_word A as ≡ reduced_word_for A (sum_list as) as"
abbreviation "reduced_words_for A a ≡ Collect (reduced_word_for A a)"

abbreviation reduced_letter_set :: "'a set ⇒ 'a ⇒ 'a set"
  where "reduced_letter_set A a ≡ ⋃( set ` (reduced_words_for A a) )"
  ― ‹will be empty if @{term a} is not in the set generated by @{term A}›

definition word_length :: "'a set ⇒ 'a ⇒ nat"
  where "word_length A a ≡ length (arg_min length (word_for A a))"

lemma reduced_word_forI:
  assumes   "as ∈ lists A" "sum_list as = a"
            "⋀bs. bs ∈ lists A ⟹ sum_list bs = a ⟹ length as ≤ length bs"
  shows     "reduced_word_for A a as"
  using     assms 
  unfolding reduced_word_for_def
  by        (force intro: is_arg_minI)

lemma reduced_word_forI_compare:
  "⟦ reduced_word_for A a as; bs ∈ lists A; sum_list bs = a; length bs = length as ⟧
    ⟹ reduced_word_for A a bs"
  using reduced_word_for_def is_arg_min_eq[of length] by fast

lemma reduced_word_for_lists: "reduced_word_for A a as ⟹ as ∈ lists A"
  using reduced_word_for_def is_arg_minD1 by fast

lemma reduced_word_for_sum_list: "reduced_word_for A a as ⟹ sum_list as = a"
  using reduced_word_for_def is_arg_minD1 by fast

lemma reduced_word_for_minimal:
  "⟦ reduced_word_for A a as; bs ∈ lists A; sum_list bs = a ⟧ ⟹
    length as ≤ length bs"
  using reduced_word_for_def is_arg_minD2[of length]
  by fastforce

lemma reduced_word_for_length:
  "reduced_word_for A a as ⟹ length as = word_length A a"
  unfolding word_length_def reduced_word_for_def is_arg_min_def
  by (fastforce intro: arg_min_equality[THEN sym])

lemma reduced_word_for_eq_length:
  "reduced_word_for A a as ⟹ reduced_word_for A a bs ⟹ length as = length bs"
  using reduced_word_for_length by simp

lemma reduced_word_for_arg_min:
  "as ∈ lists A ⟹ sum_list as = a ⟹
    reduced_word_for A a (arg_min length (word_for A a))"
  using     is_arg_min_arg_min_nat[of "word_for A a"]
  unfolding reduced_word_for_def
  by        fast

lemma nil_reduced_word_for_0: "reduced_word_for A 0 []"
  by (auto intro: reduced_word_forI)

lemma reduced_word_for_0_imp_nil: "reduced_word_for A 0 as ⟹ as = []"
  using     nil_reduced_word_for_0[of A] reduced_word_for_minimal[of A 0 as]
  unfolding reduced_word_for_def is_arg_min_def
  by (metis (mono_tags, opaque_lifting) length_0_conv length_greater_0_conv)

lemma not_reduced_word_for:
  "⟦ bs ∈ lists A; sum_list bs = a; length bs < length as ⟧ ⟹
    ¬ reduced_word_for A a as"
  using reduced_word_for_minimal by fastforce

lemma reduced_word_for_imp_reduced_word:
  "reduced_word_for A a as ⟹ reduced_word A as"
unfolding reduced_word_for_def is_arg_min_def
by (fast intro: reduced_word_forI)

lemma sum_list_zero_nreduced:
  "as ≠ [] ⟹ sum_list as = 0 ⟹ ¬ reduced_word A as"
  using not_reduced_word_for[of "[]"] by simp

lemma order2_nreduced: "a+a=0 ⟹ ¬ reduced_word A [a,a]"
  using sum_list_zero_nreduced by simp

lemma reduced_word_append_reduce_contra1:
  assumes "¬ reduced_word A as"
  shows   "¬ reduced_word A (as@bs)"
proof (cases "as ∈ lists A" "bs ∈ lists A" rule: two_cases)
  case both
  define cs where cs: "cs ≡ ARG_MIN length cs. cs ∈ lists A ∧ sum_list cs = sum_list as"
  with both(1) have "reduced_word_for A (sum_list as) cs"
    using reduced_word_for_def is_arg_min_arg_min_nat[of "word_for A (sum_list as)"]
    by    auto
  with assms both show ?thesis
    using reduced_word_for_lists reduced_word_for_sum_list
          reduced_word_for_minimal[of A "sum_list as" cs as]
          reduced_word_forI_compare[of A "sum_list as" cs as]
          not_reduced_word_for[of "cs@bs" A "sum_list (as@bs)"]
    by    fastforce
next
  case one thus ?thesis using reduced_word_for_lists by fastforce
next
  case other thus ?thesis using reduced_word_for_lists by fastforce
next
  case neither thus ?thesis using reduced_word_for_lists by fastforce
qed

lemma reduced_word_append_reduce_contra2:
  assumes "¬ reduced_word A bs"
  shows   "¬ reduced_word A (as@bs)"
proof (cases "as ∈ lists A" "bs ∈ lists A" rule: two_cases)
  case both
  define cs where cs: "cs ≡ ARG_MIN length cs. cs ∈ lists A ∧ sum_list cs = sum_list bs"
  with both(2) have "reduced_word_for A (sum_list bs) cs"
    using reduced_word_for_def is_arg_min_arg_min_nat[of "word_for A (sum_list bs)" ]
    by    auto
  with assms both show ?thesis
    using reduced_word_for_lists reduced_word_for_sum_list
          reduced_word_for_minimal[of A "sum_list bs" cs bs]
          reduced_word_forI_compare[of A "sum_list bs" cs bs]
          not_reduced_word_for[of "as@cs" A "sum_list (as@bs)"]
    by    fastforce
next
  case one thus ?thesis using reduced_word_for_lists by fastforce
next
  case other thus ?thesis using reduced_word_for_lists by fastforce
next
  case neither thus ?thesis using reduced_word_for_lists by fastforce
qed

lemma contains_nreduced_imp_nreduced:
  "¬ reduced_word A bs ⟹ ¬ reduced_word A (as@bs@cs)"
  using reduced_word_append_reduce_contra1 reduced_word_append_reduce_contra2
  by    fast

lemma contains_order2_nreduced: "a+a=0 ⟹ ¬ reduced_word A (as@[a,a]@bs)"
  using order2_nreduced contains_nreduced_imp_nreduced by fast

lemma reduced_word_Cons_reduce_contra:
  "¬ reduced_word A as ⟹ ¬ reduced_word A (a#as)"
  using reduced_word_append_reduce_contra2[of A as "[a]"] by simp

lemma reduced_word_Cons_reduce: "reduced_word A (a#as) ⟹ reduced_word A as"
  using reduced_word_Cons_reduce_contra by fast

lemma reduced_word_singleton:
  assumes "a∈A" "a≠0"
  shows   "reduced_word A [a]"
proof (rule reduced_word_forI)
  from assms(1) show "[a] ∈ lists A" by simp
next
  fix bs assume bs: "bs ∈ lists A" "sum_list bs = sum_list [a]"
  with assms(2) show "length [a] ≤ length bs" by (cases bs) auto
qed simp

lemma el_reduced:
  assumes "0 ∉ A" "as ∈ lists A" "sum_list as ∈ A" "reduced_word A as"
  shows "length as = 1"
proof-
  define n where n: "n ≡ length as"
  from assms(3) obtain a where "[a]∈lists A" "sum_list as = sum_list [a]" by auto
  with n assms(1,3,4) have "n≤1" "n>0"
    using reduced_word_for_minimal[of A _ as "[a]"] by auto
  hence "n = 1" by simp
  with n show ?thesis by fast
qed

lemma reduced_letter_set_0: "reduced_letter_set A 0 = {}"
  using reduced_word_for_0_imp_nil by simp

lemma reduced_letter_set_subset: "reduced_letter_set A a ⊆ A"
  using reduced_word_for_lists by fast

lemma reduced_word_forI_length:
  "⟦ as ∈ lists A; sum_list as = a; length as = word_length A a ⟧ ⟹
    reduced_word_for A a as"
  using reduced_word_for_arg_min reduced_word_for_length
        reduced_word_forI_compare[of A a _ as]
  by    fastforce

lemma word_length_le:
  "as ∈ lists A ⟹ sum_list as = a ⟹ word_length A a ≤ length as"
  using reduced_word_for_arg_min reduced_word_for_length
        reduced_word_for_minimal[of A]
  by    fastforce

lemma reduced_word_forI_length':
  "⟦ as ∈ lists A; sum_list as = a; length as ≤ word_length A a ⟧ ⟹
    reduced_word_for A a as"
  using word_length_le[of as A] reduced_word_forI_length[of as A] by fastforce

lemma word_length_lt:
  "as ∈ lists A ⟹ sum_list as = a ⟹ ¬ reduced_word_for A a as ⟹
    word_length A a < length as"
  using reduced_word_forI_length' by fastforce

end (* context monoid_add *)

lemma in_genby_reduced_letter_set:
  assumes "as ∈ lists A" "sum_list as = a"
  shows   "a ∈ ⟨reduced_letter_set A a⟩"
proof-
  define xs where xs: "xs ≡ arg_min length (word_for A a)"
  with assms have "xs ∈ lists (reduced_letter_set A a)" "sum_list xs = a"
    using reduced_word_for_arg_min[of as A] reduced_word_for_sum_list by auto
  thus ?thesis using genby_eq_sum_lists by force
qed

lemma reduced_word_for_genby_arg_min:
  fixes   A :: "'a::group_add set"
  defines "B ≡ A ∪ uminus ` A"
  assumes "a∈⟨A⟩"
  shows   "reduced_word_for B a (arg_min length (word_for B a))"
  using   assms genby_eq_sum_lists[of A] reduced_word_for_arg_min[of _ B a]
  by      auto

lemma reduced_word_for_genby_sym_arg_min:
  assumes "uminus ` A ⊆ A" "a∈⟨A⟩"
  shows   "reduced_word_for A a (arg_min length (word_for A a))"
proof-
  from assms(1) have "A = A ∪ uminus ` A" by auto
  with assms(2) show ?thesis
    using reduced_word_for_genby_arg_min[of a A] by simp
qed

lemma in_genby_imp_in_reduced_letter_set:
  fixes   A :: "'a::group_add set"
  defines "B ≡ A ∪ uminus ` A"
  assumes "a ∈ ⟨A⟩"
  shows   "a ∈ ⟨reduced_letter_set B a⟩"
  using   assms genby_eq_sum_lists[of A] in_genby_reduced_letter_set[of _ B]
  by      auto

lemma in_genby_sym_imp_in_reduced_letter_set:
  "uminus ` A ⊆ A ⟹ a ∈ ⟨A⟩ ⟹ a ∈ ⟨reduced_letter_set A a⟩"
  using in_genby_imp_in_reduced_letter_set by (fastforce simp add: Un_absorb2)

end (* theory *)