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  m0"
  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:
  "sset 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:
  "sset 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 (fg)"
  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  nm)  
    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 "sset 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: "gG  -gG"
  using zero_closed diff_closed[of 0 g] by simp

lemma add_closed: "gG  hG  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: "gG  xG  lconjby g x  G"
  using add_closed diff_closed by fast

lemma lconjby_set_closed: "gG  AG  lconjby g ` A  G"
  using lconjby_closed by fast

lemma set_lconjby_subset_closed:
  "HG  AG  (hH. lconjby h ` A)  G"
  using lconjby_set_closed[of _ A] by fast

lemma sum_list_map_closed: "set (map f as)  G  (aas. 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  : "gG  hG  binop g h  G"
  and     assoc   :
    " gG; hG; kG   binop (binop g h) k = binop g (binop h k)"
  and     identity: "eG" "gG  binop g e = g" "gG  binop e g = g"
  and     inverses: "gG  hG. binop g h = e  binop h g = e"
begin

lemma unique_identity1: "gG  xG. binop g x = x  g = e"
  using identity(1,2) by auto

lemma unique_inverse:
  assumes "gG"
  shows   "∃!h. hG  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 "hG  binop g h = e  binop h g = e" "kG 
            binop g k = e  binop k g = e"
  hence h: "hG" "binop g h = e" "binop h g = e"
    and k: "kG" "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:
  "gG  hG  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. hG  binop g h = e  binop h g = e)"

abbreviation "𝔦  the_inverse"

lemma the_inverseD:
  assumes   "gG"
  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: "gG  xG  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   "gG"
  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: "hG" "kG" "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 "gG" "xG"
  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:
  "gG  restrict1 (the_inv_into G (binop g)) G = G_perm (𝔦 g)"
  using the_inv_into_G_binop_G by auto

lemma bij_G_perm: "gG  bij (G_perm g)"
  using set_permutation_bij_restrict1 bij_betw_binop_G by fast

lemma G_perm_apply: "gG  xG  𝔭 g  x = binop g x"
  using Abs_G_perm_def Abs_permutation_inverse bij_G_perm by fastforce

lemma G_perm_apply_identity: "gG  𝔭 g  e = g"
  using G_perm_apply identity(1,2) by simp

lemma the_inv_G_perm:
  "gG  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:
  "gG  hG  𝔭 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: "xG" "yG" "𝔭 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 "zG. binop (binop x (𝔦 y)) z = z"
  proof
    fix z assume "zG"
    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. gG  hG  𝔭 (binop g h) = 𝔭 g + 𝔭 h"
  "x y. xpG  ypG  binop (𝔦𝔭 x) (𝔦𝔭 y) = 𝔦𝔭 (x+y)"
proof-
  show 1: "g h. gG  hG  𝔭 (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. xpG  ypG  binop (𝔦𝔭 x) (𝔦𝔭 y) = 𝔦𝔭 (x+y)"
  proof-
    fix x y assume "xpG" "ypG"
    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 = xe"
  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 "gG" "x = a+g" using elt_set_plus_def[of a] by auto
  with assms show "xG" by (simp add: add_closed)
next
  fix x assume "xG"
  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: "aG  AG  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 "gG" "-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: "0H  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: "HG  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     : "0S"  ― ‹just in case @{term S} is empty›
    | genby_genset_closed: "sS  sS"
    | genby_diff_closed  : "wS  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  (sslists (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 "sS"
  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 = (sslists (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. sS  sG" by fast
    show "w w'. wG  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 = (sslists 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  (gG. lconjby g ` A)"
  assumes "gG"
  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  (gG. lconjby g ` A)"
  assumes "gG" "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 (aas. f a) = (aas. 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:
  "gG  hG  (-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. kG  T k = 0  k=0"
  shows   "GroupIso G T"
proof (unfold_locales, rule inj_onI)
  fix x y from assms show " xG; yG; 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 "gG. hG. 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. xpG  ypG 
            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  (gG. LCoset_rel H `` {g} = RCoset_rel H `` {g})"

lemma normalI:
  assumes   "Group H" "gG. hH. h'H. g+h = h'+g"
            "gG. hH. h'H. h+g = g+h'"
  shows     "normal H"
  unfolding normal_def
proof
  fix g assume g: "gG"
  show "LCoset_rel H `` {g} = RCoset_rel H `` {g}"
  proof (rule seteqI)
    fix x assume "x  LCoset_rel H `` {g}"
    with g have x: "xG" "-g+x  H" unfolding lcoset_rel_def by auto
    from g x(2) assms(2) obtain h where h: "hH" "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: "xG" "g-x  H" unfolding rcoset_rel_def by auto
    with assms(3) obtain h where h: "hH" "-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; gG; hH   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; gG; hH   rconjby g h  H"
  using normal_lconjby_closed[of H "-g" h] uminus_closed[of g] by auto

abbreviation "normal_closure A  gG. lconjby g ` A"

lemma (in Group) normal_closure:
  assumes "AG"
  shows   "normal (normal_closure A)"
proof (rule normalI, rule genby_Group)
  show "xG. hgG. lconjby g ` A.
        h'gG. lconjby g ` A. x + h = h' + x"
  proof
    fix x assume x: "xG"
    show "hgG. lconjby g ` A.
          h'gG. lconjby g ` A. x + h = h' + x"
    proof (rule ballI, erule genby.induct)
      show "hgG. lconjby g ` A. x + 0 = h + x"
        using genby_0_closed by force
    next
      fix s assume "s  (gG. lconjby g ` A)"
      from this obtain g a where ga: "gG" "aA" "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 "hgG. lconjby g ` A. x + s = h + x"
        using add_closed by (blast intro: genby_genset_closed)
    next
      fix w w'
      assume w :  "w  gG. lconjby g ` A"
                  "h gG. lconjby g ` A. x + w  = h + x"
        and  w':  "w' gG. lconjby g ` A"
                  "h'gG. lconjby g ` A. x + w' = h'+ x"
      from w(2) w'(2) obtain h h'
        where h : "h  gG. lconjby g ` A" "x + w  = h + x"
        and   h': "h' gG. 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  "hgG. lconjby g ` A. x + (w - w') = h + x"
        using genby_diff_closed
        by    fast
    qed
  qed
  show "xG. hgG. lconjby g ` A.
        h'gG. lconjby g ` A. h + x = x + h'"
  proof
    fix x assume x: "xG"
    show "hgG. lconjby g ` A.
            h'gG. lconjby g ` A. h + x = x + h'"
    proof (rule ballI, erule genby.induct)
      show "hgG. lconjby g ` A. 0 + x = x + h"
        using genby_0_closed by force
    next
      fix s assume "s  (gG. lconjby g ` A)"
      from this obtain g a where ga: "gG" "aA" "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 "hgG. lconjby g ` A. s + x = x + h"
        using uminus_add_closed by (blast intro: genby_genset_closed)
    next
      fix w w'
      assume w :  "w  gG. lconjby g ` A"
                  "h gG. lconjby g ` A. w  + x = x + h"
        and  w':  "w' gG. lconjby g ` A"
                  "h'gG. lconjby g ` A. w' + x = x + h'"
      from w(2) w'(2) obtain h h'
        where h : "h  gG. lconjby g ` A" "w + x = x + h"
        and   h': "h' gG. 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 "hgG. 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" "gG" "g'G"
  shows   "LCoset_rel H `` {g} + LCoset_rel H `` {g'} = LCoset_rel H `` {g