Theory CompositionSeries

(*  Title:      Composition Series
    Author:     Jakob von Raumer, Karlsruhe Institute of Technology
    Maintainer: Jakob von Raumer <jakob.raumer@student.kit.edu>
*)

theory CompositionSeries
imports
  MaximalNormalSubgroups Secondary_Sylow.SndSylow
begin

hide_const (open) Divisibility.prime

section ‹Normal series and Composition series›

subsection ‹Preliminaries›

text ‹A subgroup which is unique in cardinality is normal:›

lemma (in group) unique_sizes_subgrp_normal:
  assumes fin: "finite (carrier G)"
  assumes "∃!Q. Q ∈ subgroups_of_size q"
  shows "(THE Q. Q ∈ subgroups_of_size q) ⊲ G"
proof -
  from assms obtain Q where "Q ∈ subgroups_of_size q" by auto
  define Q where "Q = (THE Q. Q ∈ subgroups_of_size q)"
  with assms have Qsize: "Q ∈ subgroups_of_size q" using theI by metis
  hence QG: "subgroup Q G" and cardQ: "card Q = q" unfolding subgroups_of_size_def by auto
  from QG have "Q ⊲ G" apply(rule normalI)
  proof
    fix g
    assume g: "g ∈ carrier G"
    hence invg: "inv g ∈ carrier G" by (metis inv_closed)
    with fin Qsize have "conjugation_action q (inv g) Q ∈ subgroups_of_size q" by (metis conjugation_is_size_invariant)
    with g Qsize have "(inv g) <# (Q #> inv (inv g)) ∈ subgroups_of_size q" unfolding conjugation_action_def by auto
    with invg g have "inv g <# (Q #> g) = Q" by (metis Qsize assms(2) inv_inv)
    with QG QG g show "Q #> g = g <# Q" by (rule conj_wo_inv)
  qed
  with Q_def show ?thesis by simp
qed

text ‹A group whose order is the product of two distinct
primes $p$ and $q$ where $p < q$ has a unique subgroup of size $q$:›

lemma (in group) pq_order_unique_subgrp:
  assumes finite: "finite (carrier G)"
  assumes orderG: "order G = q * p"
  assumes primep: "prime p" and primeq: "prime q" and pq: "p < q"
  shows "∃!Q. Q ∈ (subgroups_of_size q)"
proof -
  from primep primeq pq have nqdvdp: "¬ (q dvd p)" by (metis less_not_refl3 prime_nat_iff)
  define calM where "calM = {s. s ⊆ carrier G ∧ card s = q ^ 1}"
  define RelM where "RelM = {(N1, N2). N1 ∈ calM ∧ N2 ∈ calM ∧ (∃g∈carrier G. N1 = N2 #> g)}"
  interpret syl: snd_sylow G q 1 p calM RelM
    unfolding snd_sylow_def sylow_def snd_sylow_axioms_def sylow_axioms_def
    using is_group primeq orderG finite nqdvdp calM_def RelM_def by auto
  obtain Q where Q: "Q ∈ subgroups_of_size q" by (metis (lifting, mono_tags) mem_Collect_eq power_one_right subgroups_of_size_def syl.sylow_thm)
  thus ?thesis 
  proof (rule ex1I)
     fix P
     assume P: "P ∈ subgroups_of_size q"
     have "card (subgroups_of_size q) mod q = 1" by (metis power_one_right syl.p_sylow_mod_p)     
     moreover have "card (subgroups_of_size q) dvd p" by (metis power_one_right syl.num_sylow_dvd_remainder)
     then have "card (subgroups_of_size q) = p ∨ card (subgroups_of_size q) = 1"
       using primep by (auto simp add: prime_nat_iff)
     ultimately have "card (subgroups_of_size q) = 1" using pq
       by auto
     with Q P show "P = Q" by (auto simp:card_Suc_eq)
  qed
qed

text ‹... And this unique subgroup is normal.›

corollary (in group) pq_order_subgrp_normal:
  assumes finite: "finite (carrier G)"
  assumes orderG: "order G = q * p"
  assumes primep: "prime p" and primeq: "prime q" and pq: "p < q"
  shows "(THE Q. Q ∈ subgroups_of_size q) ⊲ G"
using assms by (metis pq_order_unique_subgrp unique_sizes_subgrp_normal)

text ‹The trivial subgroup is normal in every group.›

lemma (in group) trivial_subgroup_is_normal:
  shows "{𝟭} ⊲ G"
unfolding normal_def normal_axioms_def r_coset_def l_coset_def by (auto intro: normalI subgroupI simp: is_group)

subsection ‹Normal Series›

text ‹We define a normal series as a locale which fixes one group
@{term G} and a list @{term 𝔊} of subsets of @{term G}'s carrier. This list
must begin with the trivial subgroup, end with the carrier of the group itself
and each of the list items must be a normal subgroup of its successor.›

locale normal_series = group +
  fixes 𝔊
  assumes notempty: "𝔊 ≠ []"
  assumes hd: "hd 𝔊 = {𝟭}"
  assumes last: "last 𝔊 = carrier G"
  assumes normal: "⋀i. i + 1 < length 𝔊 ⟹ (𝔊 ! i) ⊲ G⦇carrier := 𝔊 ! (i + 1)⦈"

lemma (in normal_series) is_normal_series: "normal_series G 𝔊" by (rule normal_series_axioms)

text ‹For every group there is a "trivial" normal series consisting
only of the group itself and its trivial subgroup.›

lemma (in group) trivial_normal_series:
  shows "normal_series G [{𝟭}, carrier G]"
unfolding normal_series_def normal_series_axioms_def
using is_group trivial_subgroup_is_normal by auto

text ‹We can also show that the normal series presented above is the only such with
a length of two:›

lemma (in normal_series) length_two_unique:
  assumes "length 𝔊 = 2"
  shows "𝔊 = [{𝟭}, carrier G]"
proof(rule nth_equalityI)
  from assms show "length 𝔊 = length [{𝟭}, carrier G]" by auto
next
  show "𝔊 ! i = [{𝟭}, carrier G] ! i" if i: "i < length 𝔊" for i
  proof -
    have "i = 0 ∨ i = 1" using that assms by auto
    thus "𝔊 ! i = [{𝟭}, carrier G] ! i"
    proof(rule disjE)
      assume i: "i = 0"
      hence "𝔊 ! i = hd 𝔊" by (metis hd_conv_nth notempty)
      thus "𝔊 ! i = [{𝟭}, carrier G] ! i" using hd i by simp
    next
      assume i: "i = 1"
      with assms have "𝔊 ! i = last 𝔊" by (metis diff_add_inverse last_conv_nth nat_1_add_1 notempty)
      thus "𝔊 ! i = [{𝟭}, carrier G] ! i" using last i by simp
    qed
  qed
qed

text ‹We can construct new normal series by expanding existing ones: If we
append the carrier of a group @{term G} to a normal series for a normal subgroup
@{term "H ⊲ G"} we receive a normal series for @{term G}.›

lemma (in group) normal_series_extend:
  assumes normal: "normal_series (G⦇carrier := H⦈) ℌ"
  assumes HG: "H ⊲ G"
  shows "normal_series G (ℌ @ [carrier G])"
proof -
  from normal interpret normalH: normal_series "(G⦇carrier := H⦈)" ℌ.
  from normalH.hd have "hd ℌ = {𝟭}" by simp
  with normalH.notempty have hdTriv: "hd (ℌ @ [carrier G]) = {𝟭}" by (metis hd_append2)
  show ?thesis unfolding normal_series_def normal_series_axioms_def using is_group
  proof auto
    fix x
    assume "x ∈ hd (ℌ @ [carrier G])"
    with hdTriv show "x = 𝟭" by simp
  next
    from hdTriv show  "𝟭 ∈ hd (ℌ @ [carrier G])" by simp
  next
    fix i
    assume i: "i < length ℌ"
    show "(ℌ @ [carrier G]) ! i ⊲ G⦇carrier := (ℌ @ [carrier G]) ! Suc i⦈"
    proof (cases "i + 1 < length ℌ")
      case True
      with normalH.normal have "ℌ ! i ⊲ G⦇carrier := ℌ ! (i + 1)⦈" by auto
      with i have "(ℌ @ [carrier G]) ! i ⊲ G⦇carrier := ℌ ! (i + 1)⦈" using nth_append by metis
      with True show "(ℌ @ [carrier G]) ! i ⊲ G⦇carrier := (ℌ @ [carrier G]) ! (Suc i)⦈" using nth_append Suc_eq_plus1 by metis
    next
      case False
      with i have i2: "i + 1 = length ℌ" by simp
      from i have "(ℌ @ [carrier G]) ! i = ℌ ! i" by (metis nth_append)
      also from i2 normalH.notempty have "... = last ℌ" by (metis add_diff_cancel_right' last_conv_nth)
      also from normalH.last have "... = H" by simp
      finally have "(ℌ @ [carrier G]) ! i = H".
      moreover from i2 have "(ℌ @ [carrier G]) ! (i + 1) = carrier G" by (metis nth_append_length)
      ultimately show ?thesis using HG by auto
    qed
  qed
qed

text ‹All entries of a normal series for $G$ are subgroups of $G$.›

lemma (in normal_series) normal_series_subgroups:
  shows "i < length 𝔊 ⟹ subgroup (𝔊 ! i) G"
proof -
  have "i + 1 < length 𝔊 ⟹ subgroup (𝔊 ! i) G"
  proof (induction "length 𝔊 - (i + 2)" arbitrary: i)
    case 0
    hence i: "i + 2 = length 𝔊" by simp
    hence ii: "i + 1 = length 𝔊 - 1" by force
    from i normal have "𝔊 ! i ⊲ G⦇carrier := 𝔊 ! (i + 1)⦈" by auto
    with ii last notempty show "subgroup (𝔊 ! i) G" using last_conv_nth normal_imp_subgroup by fastforce
  next
    case (Suc k)
    from Suc(3)  normal have i: "subgroup (𝔊 ! i) (G⦇carrier := 𝔊 ! (i + 1)⦈)" using normal_imp_subgroup by auto
    from Suc(2) have k: "k = length 𝔊 - ((i + 1) + 2)" by arith
    with Suc have "subgroup (𝔊 ! (i + 1)) G" by simp
    with i show "subgroup (𝔊 ! i) G"
      using incl_subgroup by blast
  qed
  moreover have "i + 1 = length 𝔊 ⟹ subgroup (𝔊 ! i) G"
    using last notempty last_conv_nth by (metis add_diff_cancel_right' subgroup_self)
  ultimately show "i < length 𝔊 ⟹ subgroup (𝔊 ! i) G" by force
qed

text ‹The second to last entry of a normal series is a normal subgroup of G.›

lemma (in normal_series) normal_series_snd_to_last:
  shows "𝔊 ! (length 𝔊 - 2) ⊲ G"
proof (cases "2 ≤ length 𝔊")
  case False
  with notempty have length: "length 𝔊 = 1" by (metis Suc_eq_plus1 leI length_0_conv less_2_cases plus_nat.add_0)
  with hd have "𝔊 ! (length 𝔊 - 2) = {𝟭}" using hd_conv_nth notempty by auto
  with length show ?thesis by (metis trivial_subgroup_is_normal)
next
  case True
  hence "(length 𝔊 - 2) + 1 < length 𝔊" by arith
  with normal last have "𝔊 ! (length 𝔊 - 2) ⊲ G⦇carrier := 𝔊 ! ((length 𝔊 - 2) + 1)⦈" by auto
  have "1 + (1 + (length 𝔊 - (1 + 1))) = length 𝔊"
    using True le_add_diff_inverse by presburger
  then have "𝔊 ! (length 𝔊 - 2) ⊲ G⦇carrier :=  𝔊 ! (length 𝔊 - 1)⦈"
    by (metis ‹𝔊 ! (length 𝔊 - 2) ⊲ G ⦇carrier := 𝔊 ! (length 𝔊 - 2 + 1)⦈› add.commute add_diff_cancel_left' one_add_one)
  with notempty last show ?thesis using last_conv_nth by force
qed

text ‹Just like the expansion of normal series, every prefix of a normal series is again a normal series.›

lemma (in normal_series) normal_series_prefix_closed:
  assumes "i ≤ length 𝔊" and "0 < i"
  shows "normal_series (G⦇carrier := 𝔊 ! (i - 1)⦈) (take i 𝔊)"
unfolding normal_series_def normal_series_axioms_def
using assms
apply (auto simp: hd del:equalityI)
  apply (simp add: is_group normal_series_subgroups subgroup.subgroup_is_group)
 apply (simp add: last_conv_nth min.absorb2 notempty)
using assms(1) normal apply simp
done

text ‹If a group's order is the product of two distinct primes @{term p} and @{term q}, where
@{term "p < q"}, we can construct a normal series using the only subgroup of size  @{term q}.›

lemma (in group) pq_order_normal_series:
  assumes finite: "finite (carrier G)"
  assumes orderG: "order G = q * p"
  assumes primep: "prime p" and primeq: "prime q" and pq: "p < q"
  shows "normal_series G [{𝟭}, (THE H. H ∈ subgroups_of_size q), carrier G]"
proof -
  define H where "H = (THE H. H ∈ subgroups_of_size q)"
  with assms have HG: "H ⊲ G" by (metis pq_order_subgrp_normal)
  then interpret groupH: group "G⦇carrier := H⦈" unfolding normal_def by (metis subgroup_imp_group)
  have "normal_series (G⦇carrier := H⦈) [{𝟭}, H]"  using groupH.trivial_normal_series by auto
  with HG show ?thesis unfolding H_def by (metis append_Cons append_Nil normal_series_extend)
qed

text ‹The following defines the list of all quotient groups of the normal series:›

definition (in normal_series) quotients
  where "quotients = map (λi. G⦇carrier := 𝔊 ! (i + 1)⦈ Mod 𝔊 ! i) [0..<((length 𝔊) - 1)]"

text ‹The list of quotient groups has one less entry than the series itself:›

lemma (in normal_series) quotients_length:
  shows "length quotients + 1 = length 𝔊"
proof -
  have "length quotients + 1 = length [0..<((length 𝔊) - 1)] + 1" unfolding quotients_def by simp
  also have "... = (length 𝔊 - 1) + 1" by (metis diff_zero length_upt)
  also with notempty have "... = length 𝔊"
    by (simp add: ac_simps)
  finally show ?thesis .
qed

lemma (in normal_series) last_quotient:
  assumes "length 𝔊 > 1"
  shows "last quotients = G Mod 𝔊 ! (length 𝔊 - 1 - 1)"
proof -
  from assms have lsimp: "length 𝔊 - 1 - 1 + 1 = length 𝔊 - 1" by auto
  from assms have "quotients ≠ []" unfolding quotients_def by auto
  hence "last quotients = quotients ! (length quotients - 1)" by (metis last_conv_nth)
  also have "… = quotients ! (length 𝔊 - 1 - 1)" by (metis add_diff_cancel_left' quotients_length add.commute)
  also have "… = G⦇carrier := 𝔊 ! ((length 𝔊 - 1 - 1) + 1)⦈ Mod 𝔊 ! (length 𝔊 - 1 - 1)"
    unfolding quotients_def using assms by auto
  also have "… = G⦇carrier := 𝔊 ! (length 𝔊 - 1)⦈ Mod 𝔊 ! (length 𝔊 - 1 - 1)" using lsimp by simp
  also have "… = G Mod 𝔊 ! (length 𝔊 - 1 - 1)" using last last_conv_nth notempty by force
  finally show ?thesis .
qed

text ‹The next lemma transports the constituting properties of a normal series
along an isomorphism of groups.›

lemma (in normal_series) normal_series_iso:
  assumes H: "group H"
  assumes iso: "Ψ ∈ iso G H"
  shows "normal_series H (map (image Ψ) 𝔊)"
apply (simp add: normal_series_def normal_series_axioms_def)
using H notempty apply simp
proof (rule conjI)
  from H is_group iso have group_hom: "group_hom G H Ψ" unfolding group_hom_def group_hom_axioms_def iso_def by auto
  have "hd (map (image Ψ) 𝔊) = Ψ ` {𝟭}" by (metis hd_map hd notempty)
  also have "… = {Ψ 𝟭}" by (metis image_empty image_insert)
  also have "… = {𝟭⇘H⇙}" using group_hom group_hom.hom_one by auto
  finally show "hd (map ((`) Ψ) 𝔊) = {𝟭⇘H⇙}".
next
  show "last (map ((`) Ψ) 𝔊) = carrier H ∧ (∀i. Suc i < length 𝔊 ⟶ Ψ ` 𝔊 ! i ⊲ H⦇carrier := Ψ ` 𝔊 ! Suc i⦈)"
  proof (auto del: equalityI)
    have "last (map ((`) Ψ) 𝔊) = Ψ ` (carrier G)" using last last_map notempty by metis
    also have "… = carrier H" using iso unfolding iso_def bij_betw_def by simp
    finally show "last (map ((`) Ψ) 𝔊) = carrier H".
  next
    fix i
    assume i: "Suc i < length 𝔊"
    hence norm: "𝔊 ! i ⊲ G⦇carrier := 𝔊 ! Suc i⦈" using normal by simp
    moreover have "restrict Ψ (𝔊 ! Suc i) ∈ iso (G⦇carrier := 𝔊 ! Suc i⦈) (H⦇carrier := Ψ ` 𝔊 ! Suc i⦈)"
      by (metis H i is_group iso iso_restrict normal_series_subgroups)
    moreover have "group (G⦇carrier := 𝔊 ! Suc i⦈)" by (metis i normal_series_subgroups subgroup_imp_group)
    moreover hence "subgroup (𝔊 ! Suc i) G" by (metis i normal_series_subgroups)
    hence "subgroup (Ψ ` 𝔊 ! Suc i) H"
      by (simp add: H iso subgroup.iso_subgroup)
    hence "group (H⦇carrier := Ψ ` 𝔊 ! Suc i⦈)" by (metis H subgroup.subgroup_is_group)
    ultimately have "restrict Ψ (𝔊 ! Suc i) ` 𝔊 ! i ⊲ H⦇carrier := Ψ ` 𝔊 ! Suc i⦈"
      using is_group H iso_normal_subgroup by (auto cong del: image_cong_simp)
    moreover from norm have "𝔊 ! i ⊆ 𝔊 ! Suc i" unfolding normal_def subgroup_def by auto
    hence "{y. ∃x∈𝔊 ! i. y = (if x ∈ 𝔊 ! Suc i then Ψ x else undefined)} = {y. ∃x∈𝔊 ! i. y = Ψ x}" by auto
    ultimately show "Ψ ` 𝔊 ! i ⊲ H⦇carrier := Ψ ` 𝔊 ! Suc i⦈" unfolding restrict_def image_def by auto
  qed
qed

subsection ‹Composition Series›

text ‹A composition series is a normal series where all consecutive factor groups are simple:›

locale composition_series = normal_series +
  assumes simplefact: "⋀i. i + 1 <  length 𝔊 ⟹ simple_group (G⦇carrier := 𝔊 ! (i + 1)⦈ Mod 𝔊 ! i)"

lemma (in composition_series) is_composition_series:
  shows "composition_series G 𝔊"
by (rule composition_series_axioms)

text ‹A composition series for a group $G$ has length one if and only if $G$ is the trivial group.›

lemma (in composition_series) composition_series_length_one:
  shows "(length 𝔊 = 1) = (𝔊 = [{𝟭}])"
proof
  assume "length 𝔊 = 1"
  with hd have "length 𝔊 = length [{𝟭}] ∧ (∀i < length 𝔊. 𝔊 ! i = [{𝟭}] ! i)" using hd_conv_nth notempty by force
  thus "𝔊 = [{𝟭}]" using list_eq_iff_nth_eq by blast
next
  assume "𝔊 = [{𝟭}]"
  thus "length 𝔊 = 1" by simp
qed

lemma (in composition_series) composition_series_triv_group:
  shows "(carrier G = {𝟭}) = (𝔊 = [{𝟭}])"
proof
  assume G: "carrier G = {𝟭}"
  have "length 𝔊 = 1"
  proof (rule ccontr)
    assume "length 𝔊 ≠ 1"
    with notempty have length: "length 𝔊 ≥ 2" by (metis Suc_eq_plus1 length_0_conv less_2_cases not_less plus_nat.add_0)
    with simplefact hd hd_conv_nth notempty have "simple_group (G⦇carrier := 𝔊 ! 1⦈ Mod {𝟭})" by force
    moreover have SG: "subgroup (𝔊 ! 1) G" using length normal_series_subgroups by auto
    hence "group (G⦇carrier := 𝔊 ! 1⦈)" by (metis subgroup_imp_group)
    ultimately have  "simple_group (G⦇carrier := 𝔊 ! 1⦈)" using group.trivial_factor_iso simple_group.iso_simple by fastforce
    moreover from SG G have "carrier (G⦇carrier := 𝔊 ! 1⦈) = {𝟭}" unfolding subgroup_def by auto
    ultimately show False using simple_group.simple_not_triv by force
  qed
  thus "𝔊 = [{𝟭}]" by (metis composition_series_length_one)
next
  assume "𝔊 = [{𝟭}]"
  with last show "carrier G = {𝟭}" by auto
qed

text ‹The inner elements of a composition series may not consist of the trivial subgroup or the
group itself.›

lemma (in composition_series) inner_elements_not_triv:
  assumes "i + 1 < length 𝔊"
  assumes "i > 0"
  shows "𝔊 ! i ≠ {𝟭}"
proof
  from assms have "(i - 1) + 1 < length 𝔊" by simp
  hence simple: "simple_group (G⦇carrier := 𝔊 ! ((i - 1) + 1)⦈ Mod 𝔊 ! (i - 1))" using simplefact by auto
  assume i: "𝔊 ! i = {𝟭}"
  moreover from assms have "(i - 1) + 1 = i" by auto
  ultimately have "G⦇carrier := 𝔊 ! ((i - 1) + 1)⦈ Mod 𝔊 ! (i - 1) = G⦇carrier := {𝟭}⦈ Mod 𝔊 ! (i - 1)" using i by auto
  hence "order (G⦇carrier := 𝔊 ! ((i - 1) + 1)⦈ Mod 𝔊 ! (i - 1)) = 1" unfolding FactGroup_def order_def RCOSETS_def by force
  thus "False" using i simple unfolding simple_group_def simple_group_axioms_def by auto
qed

text ‹A composition series of a simple group always is its trivial one.›

lemma (in composition_series) composition_series_simple_group:
  shows "(simple_group G) = (𝔊 = [{𝟭}, carrier G])"
proof
  assume "𝔊 = [{𝟭}, carrier G]"
  with simplefact have "simple_group (G Mod {𝟭})" by auto
  moreover have "the_elem ∈ iso (G Mod {𝟭}) G" by (rule trivial_factor_iso)
  ultimately show "simple_group G" by (metis is_group simple_group.iso_simple)
next
  assume simple: "simple_group G"
  have "length 𝔊 > 1"
  proof (rule ccontr)
    assume "¬ 1 < length 𝔊"
    hence "length 𝔊 = 1" by (simp add: Suc_leI antisym notempty)
    hence "carrier G = {𝟭}" using hd last by (metis composition_series_length_one composition_series_triv_group)
    hence "order G = 1" unfolding order_def by auto
    with simple show "False" unfolding simple_group_def simple_group_axioms_def by auto
  qed
  moreover have "length 𝔊 ≤ 2"
  proof (rule ccontr)
    define k where "k = length 𝔊 - 2"
    assume "¬ (length 𝔊 ≤ 2)"
    hence gt2: "length 𝔊 > 2" by simp
    hence ksmall: "k + 1 < length 𝔊" unfolding k_def by auto
    from gt2 have carrier: "𝔊 ! (k + 1) = carrier G" using notempty last last_conv_nth k_def
      by (metis Nat.add_diff_assoc Nat.diff_cancel ‹¬ length 𝔊 ≤ 2› add.commute nat_le_linear one_add_one)
    from normal ksmall have "𝔊 ! k ⊲ G⦇ carrier := 𝔊 ! (k + 1)⦈" by simp
    from simplefact ksmall have simplek: "simple_group (G⦇carrier := 𝔊 ! (k + 1)⦈ Mod 𝔊 ! k)" by simp
    from simplefact ksmall have simplek': "simple_group (G⦇carrier := 𝔊 ! ((k - 1) + 1)⦈ Mod 𝔊 ! (k - 1))" by auto
    have "𝔊 ! k ⊲ G" using carrier k_def gt2 normal ksmall by force
    with simple have "(𝔊 ! k) = carrier G ∨ (𝔊 ! k) = {𝟭}" unfolding simple_group_def simple_group_axioms_def by simp
    thus "False"
    proof (rule disjE)
      assume "𝔊 ! k = carrier G"
      hence "G⦇carrier := 𝔊 ! (k + 1)⦈ Mod 𝔊 ! k = G Mod (carrier G)" using carrier by auto
      with simplek self_factor_not_simple show "False" by auto
    next
      assume "𝔊 ! k = {𝟭}"
      with ksmall k_def gt2 show "False" using inner_elements_not_triv by auto
    qed
  qed
  ultimately have "length 𝔊 = 2" by simp
  thus "𝔊 = [{𝟭}, carrier G]" by (rule length_two_unique)
qed

text ‹Two consecutive elements in a composition series are distinct.›

lemma (in composition_series) entries_distinct:
  assumes finite: "finite (carrier G)"
  assumes i: "i + 1 < length 𝔊"
  shows "𝔊 ! i ≠ 𝔊 ! (i + 1)"
proof
  from finite have "finite  (𝔊 ! (i + 1))" 
    using i normal_series_subgroups subgroup.subset rev_finite_subset by metis
  hence fin: "finite (carrier (G⦇carrier := 𝔊 ! (i + 1)⦈))" by auto
  from i have norm: "𝔊 ! i ⊲ (G⦇carrier := 𝔊 ! (i + 1)⦈)" by (rule normal)
  assume "𝔊 ! i = 𝔊 ! (i + 1)"
  hence "𝔊 ! i = carrier (G⦇carrier := 𝔊 ! (i + 1)⦈)" by auto
  hence "carrier ((G⦇carrier := (𝔊 ! (i + 1))⦈) Mod (𝔊 ! i)) = {𝟭⇘(G⦇carrier := 𝔊 ! (i + 1)⦈) Mod 𝔊 ! i⇙}"
    using norm fin normal.fact_group_trivial_iff by metis
  hence "¬ simple_group ((G⦇carrier := (𝔊 ! (i + 1))⦈) Mod (𝔊 ! i))" by (metis simple_group.simple_not_triv)
  thus False by (metis i simplefact)
qed

text ‹The normal series for groups of order @{term "p * q"} is even a composition series:›

lemma (in group) pq_order_composition_series:
  assumes finite: "finite (carrier G)"
  assumes orderG: "order G = q * p"
  assumes primep: "prime p" and primeq: "prime q" and pq: "p < q"
  shows "composition_series G [{𝟭}, (THE H. H ∈ subgroups_of_size q), carrier G]"
unfolding composition_series_def composition_series_axioms_def
apply(auto)
using assms apply(rule pq_order_normal_series)
proof -
  define H where "H = (THE H. H ∈ subgroups_of_size q)"
  from assms have exi: "∃!Q. Q ∈ (subgroups_of_size q)" by (auto simp: pq_order_unique_subgrp)
  hence Hsize: "H ∈ subgroups_of_size q" unfolding H_def using theI' by metis
  hence HsubG: "subgroup H G" unfolding subgroups_of_size_def by auto
  then interpret Hgroup: group "G⦇carrier := H⦈" by (metis subgroup_imp_group)
  fix i
  assume "i < Suc (Suc 0)"
  hence "i = 0 ∨ i = 1" by auto
  thus "simple_group (G⦇carrier := [H, carrier G] ! i⦈ Mod [{𝟭}, H, carrier G] ! i)"
  proof
    assume i: "i = 0"
    from Hsize have orderH: "order (G⦇carrier := H⦈) = q" unfolding subgroups_of_size_def order_def by simp
    hence order_eq_q: "order (G⦇carrier := H⦈ Mod {𝟭}) = q"
      using Hgroup.trivial_factor_iso iso_same_order by auto
    have "normal {𝟭} (G⦇carrier := H⦈)"
      by (simp add: HsubG group.normal_restrict_supergroup subgroup.one_closed trivial_subgroup_is_normal)
    hence "group (G⦇carrier := H⦈ Mod {𝟭})" by (metis normal.factorgroup_is_group)
    with orderH primeq have "simple_group (G⦇carrier := H⦈ Mod {𝟭})" 
      by (metis order_eq_q group.prime_order_simple)
    with i show ?thesis by simp
  next
    assume i: "i = 1"
    from assms exi have "H ⊲ G" unfolding H_def by (metis pq_order_subgrp_normal)
    hence groupGH: "group (G Mod H)" by (metis normal.factorgroup_is_group)
    from primeq have "q ≠ 0" by (metis not_prime_0)
    from HsubG finite orderG have "card (rcosets H) * card H = q * p" unfolding subgroups_of_size_def using lagrange by simp
    with Hsize have "card (rcosets H) * q = q * p" unfolding subgroups_of_size_def by simp
    with ‹q ≠ 0› have "card (rcosets H) = p" by auto
    hence "order (G Mod H) = p" unfolding order_def FactGroup_def by auto
    with groupGH primep have "simple_group (G Mod H)" by (metis group.prime_order_simple)
    with i show ?thesis by auto
  qed
qed

text ‹Prefixes of composition series are also composition series.›

lemma (in composition_series) composition_series_prefix_closed:
  assumes "i ≤ length 𝔊" and "0 < i"
  shows "composition_series (G⦇carrier := 𝔊 ! (i - 1)⦈) (take i 𝔊)"
unfolding composition_series_def composition_series_axioms_def
proof auto
  from assms show "normal_series (G⦇carrier := 𝔊 ! (i - Suc 0)⦈) (take i 𝔊)" by (metis One_nat_def normal_series_prefix_closed)
next
  fix j
  assume j: "Suc j < length 𝔊" "Suc j < i"
  with simplefact show "simple_group (G⦇carrier := 𝔊 ! Suc j⦈ Mod 𝔊 ! j)" by (metis Suc_eq_plus1)
qed

text ‹The second element in a composition series is simple group.›

lemma (in composition_series) composition_series_snd_simple:
  assumes "2 ≤ length 𝔊"
  shows "simple_group (G⦇carrier := 𝔊 ! 1⦈)"
proof -
  from assms interpret compTake: composition_series "G⦇carrier := 𝔊 ! 1⦈" "take 2 𝔊" by (metis add_diff_cancel_right' composition_series_prefix_closed one_add_one zero_less_numeral)
  from assms have "length (take 2 𝔊) = 2" by (metis add_diff_cancel_right' append_take_drop_id diff_diff_cancel length_append length_drop)
  hence "(take 2 𝔊) = [{𝟭⇘(G⦇carrier := 𝔊 ! 1⦈)⇙}, carrier (G⦇carrier := 𝔊 ! 1⦈)]" by (rule compTake.length_two_unique)
  thus ?thesis by (metis compTake.composition_series_simple_group)
qed

text ‹As a stronger way to state the previous lemma: An entry of a composition series is 
  simple if and only if it is the second one.›

lemma (in composition_series) composition_snd_simple_iff:
  assumes "i < length 𝔊"
  shows "(simple_group (G⦇carrier :=  𝔊 ! i⦈)) = (i = 1)"
proof
  assume simpi: "simple_group (G⦇carrier := 𝔊 ! i⦈)"
  hence "𝔊 ! i ≠ {𝟭}" using simple_group.simple_not_triv by force
  hence "i ≠ 0" using hd hd_conv_nth notempty by auto
  then interpret compTake: composition_series "G⦇carrier := 𝔊 ! i⦈" "take (Suc i) 𝔊"
    using assms composition_series_prefix_closed by (metis diff_Suc_1 less_eq_Suc_le zero_less_Suc)
  from simpi have "(take (Suc i) 𝔊) = [{𝟭⇘G⦇carrier := 𝔊 ! i⦈⇙}, carrier (G⦇carrier := 𝔊 ! i⦈)]"
    by (metis compTake.composition_series_simple_group)
  hence "length (take (Suc i) 𝔊) = 2" by auto
  hence "min (length 𝔊) (Suc i) = 2" by (metis length_take)
  with assms have "Suc i = 2" by force
  thus "i = 1" by simp
next
  assume i: "i = 1"
  with assms have "2 ≤ length 𝔊" by simp
  with i show "simple_group (G⦇carrier := 𝔊 ! i⦈)" by (metis composition_series_snd_simple)
qed

text ‹The second to last entry of a normal series is not only a normal subgroup but
  actually even a \emph{maximal} normal subgroup.›

lemma (in composition_series) snd_to_last_max_normal:
  assumes finite: "finite (carrier G)"
  assumes length: "length 𝔊 > 1"
  shows "max_normal_subgroup (𝔊 ! (length 𝔊 - 2)) G"
unfolding max_normal_subgroup_def max_normal_subgroup_axioms_def
proof (auto del: equalityI)
  show "𝔊 ! (length 𝔊 - 2) ⊲ G" by (rule normal_series_snd_to_last)
next 
  define G' where "G' = 𝔊 ! (length 𝔊 - 2)"
  from length have length21: "length 𝔊 - 2 + 1 = length 𝔊 - 1" by arith
  from length have "length 𝔊 - 2 + 1 < length 𝔊" by arith
  with simplefact have "simple_group (G⦇carrier := 𝔊 ! ((length 𝔊 - 2) + 1)⦈ Mod G')" unfolding G'_def by auto
  with length21 have simple_last: "simple_group (G Mod G')" using last notempty last_conv_nth by fastforce
  {
    assume snd_to_last_eq: "G' = carrier G"
    hence "carrier (G Mod G') = {𝟭⇘G Mod G'⇙}"
    using normal_series_snd_to_last finite normal.fact_group_trivial_iff unfolding G'_def by metis
    with snd_to_last_eq have "¬ simple_group (G Mod G')" by (metis self_factor_not_simple)
    with simple_last show False unfolding G'_def by auto
  }
  {
    have G'G: "G' ⊲ G" unfolding G'_def by (rule normal_series_snd_to_last)
    fix J
    assume J: "J ⊲ G" "J ≠ G'" "J ≠ carrier G" "G' ⊆ J"
    hence JG'GG': "rcosets⇘(G⦇carrier := J⦈)⇙ G' ⊲ G Mod G'"  using normality_factorization normal_series_snd_to_last unfolding G'_def by auto
    from G'G J(1,4) have G'J: "G' ⊲ (G⦇carrier := J⦈)" by (metis normal_imp_subgroup normal_restrict_supergroup)
    from finite J(1) have finJ: "finite J" by (auto simp: normal_imp_subgroup subgroup_finite)
    from JG'GG' simple_last have "rcosets⇘G⦇carrier := J⦈⇙ G' = {𝟭⇘G Mod G'⇙} ∨ rcosets⇘G⦇carrier := J⦈⇙ G' = carrier (G Mod G')"
      unfolding simple_group_def simple_group_axioms_def by auto
    thus False 
    proof
      assume "rcosets⇘G⦇carrier := J⦈⇙ G' = {𝟭⇘G Mod G'⇙}"
      hence "rcosets⇘G⦇carrier := J⦈⇙ G' = {𝟭⇘(G⦇carrier := J⦈) Mod G'⇙}" unfolding FactGroup_def by simp
      hence "G' = J" using G'J finJ normal.fact_group_trivial_iff unfolding FactGroup_def by fastforce
      with J(2) show False by simp
    next
      assume facts_eq: "rcosets⇘G⦇carrier := J⦈⇙ G' = carrier (G Mod G')"
      have "J = carrier G"
      proof
        show "J ⊆ carrier G" using J(1) normal_imp_subgroup subgroup.subset by force
      next
        show "carrier G ⊆ J"
        proof
          fix x
          assume x: "x ∈ carrier G"
          hence "G' #> x ∈ carrier (G Mod G')" unfolding FactGroup_def RCOSETS_def by auto
          hence "G' #> x ∈ rcosets⇘G⦇carrier := J⦈⇙ G'" using facts_eq by auto
          then obtain j where j: "j ∈ J" "G' #> x = G' #> j" unfolding RCOSETS_def r_coset_def by force
          hence "x ∈ G' #> j" using G'G normal_imp_subgroup x repr_independenceD by fastforce
          then obtain g' where g': "g' ∈ G'" "x = g' ⊗ j" unfolding r_coset_def by auto
          hence "g' ∈ J" using G'J normal_imp_subgroup subgroup.subset by force
          with g'(2) j(1) show  "x ∈ J" using J(1) normal_imp_subgroup subgroup.m_closed by fastforce
        qed
      qed
      with J(3) show False by simp
    qed
  }
qed

text ‹For the next lemma we need a few facts about removing adjacent duplicates.›

lemma remdups_adj_obtain_adjacency:
  assumes "i + 1 < length (remdups_adj xs)" "length xs > 0"
  obtains j where "j + 1 < length xs"
    "(remdups_adj xs) ! i = xs ! j" "(remdups_adj xs) ! (i + 1) = xs ! (j + 1)"
using assms proof (induction xs arbitrary: i thesis)
  case Nil
  hence False by (metis length_greater_0_conv)
  thus thesis..
next
  case (Cons x xs)
  then have "xs ≠ []"
    by auto
  then obtain y xs' where xs: "xs = y # xs'"
    by (cases xs) blast
  from ‹xs ≠ []› have lenxs: "length xs > 0" by simp
  from xs have rem: "remdups_adj (x # xs) = (if x = y then remdups_adj (y # xs') else x # remdups_adj (y # xs'))" using remdups_adj.simps(3) by auto
  show thesis
  proof (cases "x = y")
    case True
    with rem xs have rem2: "remdups_adj (x # xs) = remdups_adj xs" by auto
    with Cons(3) have "i + 1 < length (remdups_adj xs)" by simp
    with Cons.IH lenxs obtain k where j: "k + 1 < length xs" "remdups_adj xs ! i = xs ! k"
        "remdups_adj xs ! (i + 1) = xs ! (k + 1)" by auto
    thus thesis using Cons(2) rem2 by auto
  next
    case False
    with rem xs have rem2: "remdups_adj (x # xs) = x # remdups_adj xs" by auto
    show thesis
    proof (cases i)
      case 0
      have "0 + 1 < length (x # xs)" using lenxs by auto
      moreover have "remdups_adj (x # xs) ! i = (x # xs) ! 0"
      proof -
        have "remdups_adj (x # xs) ! i = (x # remdups_adj (y # xs')) ! 0" using xs rem2 0 by simp
        also have "… = x" by simp
        also have "… = (x # xs) ! 0" by simp
        finally show ?thesis.
      qed
      moreover have "remdups_adj (x # xs) ! (i + 1) = (x # xs) ! (0 + 1)"
      proof -
        have "remdups_adj (x # xs) ! (i + 1) = (x # remdups_adj (y # xs')) ! 1" using xs rem2 0 by simp
        also have "… = remdups_adj (y # xs') ! 0" by simp
        also have "… = (y # (remdups (y # xs'))) ! 0" by (metis nth_Cons' remdups_adj_Cons_alt)
        also have "… = y" by simp
        also have "… = (x # xs) ! (0 + 1)" unfolding xs by simp
        finally show ?thesis.
      qed
      ultimately show thesis by (rule Cons.prems(1))
    next
      case (Suc k)
      with Cons(3) have "k + 1 < length (remdups_adj (x # xs)) - 1" by auto
      also have "… ≤ length (remdups_adj xs) + 1 - 1" by (metis One_nat_def le_refl list.size(4) rem2)
      also have "… = length (remdups_adj xs)" by simp
      finally have "k + 1 < length (remdups_adj xs)".
      with Cons.IH lenxs obtain j where j: "j + 1 < length xs" "remdups_adj xs ! k = xs ! j"
        "remdups_adj xs ! (k + 1) = xs ! (j + 1)" by auto
      from j(1) have "Suc j + 1 < length (x # xs)" by simp
      moreover have "remdups_adj (x # xs) ! i = (x # xs) ! (Suc j)"
      proof -
        have "remdups_adj (x # xs) ! i = (x # remdups_adj xs) ! i" using rem2 by simp
        also have "… = (remdups_adj xs) ! k" using Suc by simp
        also have "… = xs ! j" using j(2) .
        also have "… = (x # xs) ! (Suc j)" by simp
        finally show ?thesis .
      qed
      moreover have "remdups_adj (x # xs) ! (i + 1) = (x # xs) ! (Suc j + 1)"
      proof -
        have "remdups_adj (x # xs) ! (i + 1) = (x # remdups_adj xs) ! (i + 1)" using rem2 by simp
        also have "… = (remdups_adj xs) ! (k + 1)" using Suc by simp
        also have "… = xs ! (j + 1)" using j(3).
        also have "… = (x # xs) ! (Suc j + 1)" by simp
        finally show ?thesis.
      qed
      ultimately show thesis by (rule Cons.prems(1))
    qed
  qed
qed

lemma hd_remdups_adj[simp]: "hd (remdups_adj xs) = hd xs"
  by (induction xs rule: remdups_adj.induct) simp_all

lemma remdups_adj_adjacent:
  "Suc i < length (remdups_adj xs) ⟹ remdups_adj xs ! i ≠ remdups_adj xs ! Suc i"
proof (induction xs arbitrary: i rule: remdups_adj.induct)
  case (3 x y xs i)
  thus ?case by (cases i, cases "x = y") (simp, auto simp: hd_conv_nth[symmetric])
qed simp_all

text ‹Intersecting each entry of a composition series with a normal subgroup of $G$ and removing
  all adjacent duplicates yields another composition series.›

lemma (in composition_series) intersect_normal:
  assumes finite: "finite (carrier G)"
  assumes KG: "K ⊲ G"
  shows "composition_series (G⦇carrier := K⦈) (remdups_adj (map (λH. K ∩ H) 𝔊))"
unfolding composition_series_def composition_series_axioms_def normal_series_def normal_series_axioms_def
apply (auto simp only: conjI del: equalityI)
proof -
  show "group (G⦇carrier := K⦈)" using KG normal_imp_subgroup subgroup_imp_group by auto
next
  ― ‹Show, that removing adjacent duplicates doesn't result in an empty list.›
  assume "remdups_adj (map ((∩) K) 𝔊) = []"
  hence "map ((∩) K) 𝔊 = []" by (metis remdups_adj_Nil_iff)
  hence "𝔊 = []" by (metis Nil_is_map_conv)
  with notempty show False..
next
  ― ‹Show, that the head of the reduced list is still the trivial group›
  have "𝔊 = {𝟭} # tl 𝔊" using notempty hd by (metis list.sel(1,3) neq_Nil_conv)
  hence "map ((∩) K) 𝔊 = map ((∩) K) ({𝟭} # tl 𝔊)" by simp
  hence "remdups_adj (map ((∩) K) 𝔊) = remdups_adj ((K ∩ {𝟭}) # (map ((∩) K) (tl 𝔊)))" by simp
  also have "… = (K ∩ {𝟭}) # tl (remdups_adj ((K ∩ {𝟭}) # (map ((∩) K) (tl 𝔊))))" by simp
  finally have "hd (remdups_adj (map ((∩) K) 𝔊)) = K ∩ {𝟭}" using list.sel(1) by metis
  thus "hd (remdups_adj (map ((∩) K) 𝔊)) = {𝟭⇘G⦇carrier := K⦈⇙}" 
    using KG normal_imp_subgroup subgroup.one_closed by force
next
  ― ‹Show that the last entry is really @{text "K ∩ G"}. Since we don't have a lemma ready to talk about the
    last entry of a reduced list, we reverse the list twice.›
  have "rev 𝔊 = (carrier G) # tl (rev 𝔊)" by (metis list.sel(1,3) last last_rev neq_Nil_conv notempty rev_is_Nil_conv rev_rev_ident)
  hence "rev (map ((∩) K) 𝔊) = map ((∩) K) ((carrier G) # tl (rev 𝔊))" by (metis rev_map)
  hence rev: "rev (map ((∩) K) 𝔊) = (K ∩ (carrier G)) # (map ((∩) K) (tl (rev 𝔊)))" by simp
  have "last (remdups_adj (map ((∩) K) 𝔊)) = hd (rev (remdups_adj (map ((∩) K) 𝔊)))"
    by (metis hd_rev map_is_Nil_conv notempty remdups_adj_Nil_iff)
  also have "… = hd (remdups_adj (rev (map ((∩) K) 𝔊)))" by (metis remdups_adj_rev)
  also have "… = hd (remdups_adj ((K ∩ (carrier G)) # (map ((∩) K) (tl (rev 𝔊)))))" by (metis rev)
  also have "… = hd ((K ∩ (carrier G)) # (remdups_adj ((K ∩ (carrier G)) # (map ((∩) K) (tl (rev 𝔊))))))" by (metis list.sel(1) remdups_adj_Cons_alt)
  also have "… = K" using KG normal_imp_subgroup subgroup.subset by force
  finally show "last (remdups_adj (map ((∩) K) 𝔊)) = carrier (G⦇carrier := K⦈)" by auto
next
  ― ‹The induction step, using the second isomorphism theorem for groups.›
  fix j
  assume j: "j + 1 < length (remdups_adj (map ((∩) K) 𝔊))"
  have KGnotempty: "(map ((∩) K) 𝔊) ≠ []" using notempty by (metis Nil_is_map_conv)
  with j obtain i where i: "i + 1 < length (map ((∩) K) 𝔊)"
    "(remdups_adj (map ((∩) K) 𝔊)) ! j = (map ((∩) K) 𝔊) ! i"
    "(remdups_adj (map ((∩) K) 𝔊)) ! (j + 1) = (map ((∩) K) 𝔊) ! (i + 1)"
    using remdups_adj_obtain_adjacency by force
  from i(1) have i': "i + 1 < length 𝔊" by (metis length_map)
  hence GiSi: "𝔊 ! i ⊲ G⦇carrier := 𝔊 ! (i + 1)⦈" by (metis normal)
  hence GiSi': "𝔊 ! i ⊆ 𝔊 ! (i + 1)" using normal_imp_subgroup subgroup.subset by force
  from i' have finGSi: "finite (𝔊 ! (i + 1))" using  normal_series_subgroups finite by (metis subgroup_finite)
  from GiSi KG i' normal_series_subgroups have GSiKnormGSi: "𝔊 ! (i + 1) ∩ K ⊲ G⦇carrier := 𝔊 ! (i + 1)⦈"
    using second_isomorphism_grp.normal_subgrp_intersection_normal
    unfolding second_isomorphism_grp_def second_isomorphism_grp_axioms_def by auto
  with GiSi have "𝔊 ! i ∩ (𝔊 ! (i + 1) ∩ K) ⊲ G⦇carrier := 𝔊 ! (i + 1)⦈"
    by (metis group.normal_subgroup_intersect group.subgroup_imp_group i' is_group is_normal_series normal_series.normal_series_subgroups)
  hence "K ∩ (𝔊 ! i ∩ 𝔊 ! (i + 1)) ⊲ G⦇carrier := 𝔊 ! (i + 1)⦈" by (metis inf_commute inf_left_commute)
  hence KGinormGSi: "K ∩ 𝔊 ! i ⊲ G⦇carrier := 𝔊 ! (i + 1)⦈" using GiSi' by (metis le_iff_inf)
  moreover have "K ∩ 𝔊 ! i ⊆ K ∩ 𝔊 ! (i + 1)" using GiSi' by auto
  moreover have groupGSi: "group (G⦇carrier := 𝔊 ! (i + 1)⦈)" using i normal_series_subgroups subgroup_imp_group by auto
  moreover have subKGSiGSi: "subgroup (K ∩ 𝔊 ! (i + 1)) (G⦇carrier := 𝔊 ! (i + 1)⦈)" by (metis GSiKnormGSi inf_sup_aci(1) normal_imp_subgroup)
  ultimately have fstgoal: "K ∩ 𝔊 ! i ⊲ G⦇carrier := 𝔊 ! (i + 1), carrier := K ∩ 𝔊 ! (i + 1)⦈"
    using group.normal_restrict_supergroup by force
  thus "remdups_adj (map ((∩) K) 𝔊) ! j ⊲ G⦇carrier := K, carrier := remdups_adj (map ((∩) K) 𝔊) ! (j + 1)⦈"
    using i by auto
  from simplefact have Gisimple: "simple_group (G⦇carrier := 𝔊 ! (i + 1)⦈ Mod 𝔊 ! i)" using i' by simp
  hence Gimax: "max_normal_subgroup (𝔊 ! i) (G⦇carrier := 𝔊 ! (i + 1)⦈)"
    using normal.max_normal_simple_quotient GiSi finGSi by force
  from GSiKnormGSi GiSi have "𝔊 ! i <#>⇘G⦇carrier := 𝔊 ! (i + 1)⦈⇙ 𝔊 ! (i + 1) ∩ K ⊲ (G⦇carrier := 𝔊 ! (i + 1)⦈)"
    using groupGSi group.normal_subgroup_set_mult_closed set_mult_consistent by fastforce
  hence "𝔊 ! i <#> 𝔊 ! (i + 1) ∩ K ⊲ G⦇carrier := 𝔊 ! (i + 1)⦈" unfolding set_mult_def by auto
  hence "𝔊 ! i <#> K ∩ 𝔊 ! (i + 1) ⊲ G⦇carrier := 𝔊 ! (i + 1)⦈" using inf_commute by metis
  moreover have "𝔊 ! i ⊆ 𝔊 ! i <#>⇘G⦇carrier := 𝔊 ! (i + 1)⦈⇙ K ∩ 𝔊 ! (i + 1)"
    using second_isomorphism_grp.H_contained_in_set_mult
    unfolding second_isomorphism_grp_def second_isomorphism_grp_axioms_def
    using subKGSiGSi GiSi normal_imp_subgroup by fastforce
  hence "𝔊 ! i ⊆ 𝔊 ! i <#> K ∩ 𝔊 ! (i + 1)" unfolding set_mult_def by auto
  ultimately have KGdisj: "𝔊 ! i <#> K ∩ 𝔊 ! (i + 1) = 𝔊 ! i ∨ 𝔊 ! i <#> K ∩ 𝔊 ! (i + 1) = 𝔊 ! (i + 1)"
    using Gimax unfolding max_normal_subgroup_def max_normal_subgroup_axioms_def
    by auto
  obtain φ where "φ ∈ iso  (G⦇carrier := K ∩ 𝔊 ! (i + 1)⦈ Mod (𝔊 ! i ∩ (K ∩ 𝔊 ! (i + 1))))
             (G⦇carrier := 𝔊 ! i <#>⇘G⦇carrier := 𝔊 ! (i + 1)⦈⇙ K ∩ 𝔊 ! (i + 1)⦈ Mod 𝔊 ! i)"
    using second_isomorphism_grp.normal_intersection_quotient_isom
    unfolding second_isomorphism_grp_def second_isomorphism_grp_axioms_def
    using GiSi subKGSiGSi normal_imp_subgroup  by fastforce
  hence "φ ∈ iso  (G⦇carrier := K ∩ 𝔊 ! (i + 1)⦈ Mod (K ∩ 𝔊 ! (i + 1) ∩ 𝔊 ! i))
                  (G⦇carrier := 𝔊 ! i <#>⇘G⦇carrier := 𝔊 ! (i + 1)⦈⇙ K ∩ 𝔊 ! (i + 1)⦈ Mod 𝔊 ! i)" 
    by (metis inf_commute)
  hence "φ ∈ iso (G⦇carrier := K ∩ 𝔊 ! (i + 1)⦈ Mod (K ∩ (𝔊 ! (i + 1) ∩ 𝔊 ! i)))
                 (G⦇carrier := 𝔊 ! i <#>⇘G⦇carrier := 𝔊 ! (i + 1)⦈⇙ K ∩ 𝔊 ! (i + 1)⦈ Mod 𝔊 ! i)"
    by (metis Int_assoc)
  hence "φ ∈ iso (G⦇carrier := K ∩ 𝔊 ! (i + 1)⦈ Mod (K ∩ 𝔊 ! i))
                 (G⦇carrier := 𝔊 ! i <#>⇘G⦇carrier := 𝔊 ! (i + 1)⦈⇙ K ∩ 𝔊 ! (i + 1)⦈ Mod 𝔊 ! i)" 
    by (metis GiSi' Int_absorb2 Int_commute)
  hence φ: "φ ∈ iso (G⦇carrier := K ∩ 𝔊 ! (i + 1)⦈ Mod (K ∩ 𝔊 ! i))
                   (G⦇carrier := 𝔊 ! i <#> K ∩ 𝔊 ! (i + 1)⦈ Mod 𝔊 ! i)"
    unfolding set_mult_def by auto
  from fstgoal have KGsiKGigroup: "group (G⦇carrier := K ∩ 𝔊 ! (i + 1)⦈ Mod (K ∩ 𝔊 ! i))" using normal.factorgroup_is_group by auto
  from KGdisj show "simple_group (G⦇carrier := K, carrier := remdups_adj (map ((∩) K) 𝔊) ! (j + 1)⦈ Mod remdups_adj (map ((∩) K) 𝔊) ! j)"
  proof auto
    have groupGi: "group (G⦇carrier := 𝔊 ! i⦈)" using i' normal_series_subgroups subgroup_imp_group by auto
    assume "𝔊 ! i <#> K ∩ 𝔊 ! Suc i = 𝔊 ! i"
    with φ have "φ ∈ iso (G⦇carrier := K ∩ 𝔊 ! (i + 1)⦈ Mod (K ∩ 𝔊 ! i)) (G⦇carrier := 𝔊 ! i⦈ Mod 𝔊 ! i)" by auto
    moreover obtain ψ where "ψ ∈ iso (G⦇carrier := 𝔊 ! i⦈ Mod (carrier (G⦇carrier := 𝔊 ! i⦈))) (G⦇carrier := {𝟭⇘G⦇carrier := 𝔊 ! i⦈⇙}⦈)"
      using group.self_factor_iso groupGi by force
    ultimately obtain π where "π ∈ iso (G⦇carrier := K ∩ 𝔊 ! (i + 1)⦈ Mod (K ∩ 𝔊 ! i)) (G⦇carrier := {𝟭}⦈)"
      using iso_set_trans by fastforce
    hence "order (G⦇carrier := K ∩ 𝔊 ! (i + 1)⦈ Mod (K ∩ 𝔊 ! i)) = order (G⦇carrier := {𝟭}⦈)"
      by (meson iso_same_order)
    hence "order (G⦇carrier := K ∩ 𝔊 ! (i + 1)⦈ Mod (K ∩ 𝔊 ! i)) = 1" unfolding order_def by auto
    hence "carrier (G⦇carrier := K ∩ 𝔊 ! (i + 1)⦈ Mod (K ∩ 𝔊 ! i)) = {𝟭⇘G⦇carrier := K ∩ 𝔊 ! (i + 1)⦈ Mod (K ∩ 𝔊 ! i)⇙}"
      using group.order_one_triv_iff KGsiKGigroup by blast
    moreover from fstgoal have "K ∩ 𝔊 ! i ⊲ G⦇carrier := K ∩ 𝔊 ! (i + 1)⦈" by auto
    moreover from finGSi have "finite (carrier (G⦇carrier := K ∩ 𝔊 ! (i + 1)⦈))" by auto
    ultimately have "K ∩ 𝔊 ! i = carrier (G⦇carrier := K ∩ 𝔊 ! (i + 1)⦈)" by (metis normal.fact_group_trivial_iff)
    hence "(remdups_adj (map ((∩) K) 𝔊)) ! j = (remdups_adj (map ((∩) K) 𝔊)) ! (j + 1)" using i by auto
    with j have False using remdups_adj_adjacent KGnotempty Suc_eq_plus1 by metis
    thus "simple_group (G⦇carrier := remdups_adj (map ((∩) K) 𝔊) ! Suc j⦈ Mod remdups_adj (map ((∩) K) 𝔊) ! j)"..
  next
    assume "𝔊 ! i <#> K ∩ 𝔊 ! Suc i = 𝔊 ! Suc i"
    with φ have "φ ∈ iso (G⦇carrier := K ∩ 𝔊 ! (i + 1)⦈ Mod (K ∩ 𝔊 ! i)) (G⦇carrier := 𝔊 ! (i + 1)⦈ Mod 𝔊 ! i)"
      by auto
    then obtain φ' where "φ' ∈ iso (G⦇carrier := 𝔊 ! (i + 1)⦈ Mod 𝔊 ! i) (G⦇carrier := K ∩ 𝔊 ! (i + 1)⦈ Mod (K ∩ 𝔊 ! i))"
      using KGsiKGigroup group.iso_set_sym by auto
    with Gisimple KGsiKGigroup have "simple_group (G⦇carrier := K ∩ 𝔊 ! (i + 1)⦈ Mod (K ∩ 𝔊 ! i))" by (metis simple_group.iso_simple)
    with i show "simple_group (G⦇carrier := remdups_adj (map ((∩) K) 𝔊) ! Suc j⦈ Mod remdups_adj (map ((∩) K) 𝔊) ! j)"
      by auto
  qed
qed

lemma (in group) composition_series_extend:
  assumes "composition_series (G⦇carrier := H⦈) ℌ"
  assumes "simple_group (G Mod H)" "H ⊲ G"
  shows "composition_series G (ℌ @ [carrier G])"
unfolding composition_series_def composition_series_axioms_def
proof auto
  from assms(1) interpret compℌ: composition_series "G⦇carrier := H⦈" ℌ .
  show "normal_series G (ℌ @ [carrier G])" using  assms(3) compℌ.is_normal_series by (metis normal_series_extend)
  fix i
  assume i: "i < length ℌ"
  show "simple_group (G⦇carrier := (ℌ @ [carrier G]) ! Suc i⦈ Mod (ℌ @ [carrier G]) ! i)"
  proof (cases "i = length ℌ - 1")
    case True
    hence "(ℌ @ [carrier G]) ! Suc i = carrier G" by (metis i diff_Suc_1 lessE nth_append_length)
    moreover have "(ℌ @ [carrier G]) ! i = ℌ ! i"by (metis butlast_snoc i nth_butlast)
    hence "(ℌ @ [carrier G]) ! i = H" using True last_conv_nth compℌ.notempty compℌ.last by auto
    ultimately show ?thesis using assms(2) by auto
  next
    case False
    hence "Suc i < length ℌ" using i by auto
    hence "(ℌ @ [carrier G]) ! Suc i = ℌ ! Suc i" using nth_append by metis
    moreover from i have "(ℌ @ [carrier G]) ! i = ℌ ! i" using nth_append by metis
    ultimately show ?thesis using ‹Suc i < length ℌ› compℌ.simplefact by auto
  qed
qed

lemma (in composition_series) entries_mono:
  assumes "i ≤ j" "j < length 𝔊"
  shows "𝔊 ! i ⊆ 𝔊 ! j"
using assms proof (induction "j - i" arbitrary: i j)
  case 0
  hence "i = j" by auto
  thus "𝔊 ! i ⊆ 𝔊 ! j" by auto
next
  case (Suc k i j)
  hence i': "i + (Suc k) = j" "i + 1 < length 𝔊" by auto
  hence ij: "i + 1 ≤ j" by auto
  have "𝔊 ! i ⊆ 𝔊 ! (i + 1)" using i' normal normal_imp_subgroup subgroup.subset by force
  moreover have "j - (i + 1) = k" "j < length 𝔊" using Suc assms by auto
  hence "𝔊 ! (i + 1) ⊆ 𝔊 ! j" using Suc(1) ij by auto
  ultimately show "𝔊 ! i ⊆ 𝔊 ! j" by simp
qed

end