Quelle  Sym_Groups.thy

(*  Title:      HOL/Algebra/Sym_Groups.thy
  Author: Paulo Emílio de Vilhena
*)

theory Sym_Groups
  imports
    "HOL-Combinatorics.Cycles"
    Solvable_Groups
begin

section ‹Symmetric Groups›

subsection ‹Definitions›

abbreviation inv' :: "('a ==> 'b) ==> ('b ==> 'a)"
  where "inv' f ≡ Hilbert_Choice.inv f"
  
definition sym_group :: "nat ==> (nat ==> nat) monoid"
  where "sym_group n = ( carrier = { p. p permutes {1..n} }, mult = (∘), one = id )"

definition alt_group :: "nat ==> (nat ==> nat) monoid"
  where "alt_group n = (sym_group n) ( carrier := { p. p permutes {1..n} ∧ evenperm p } )"

definition sign_img :: "int monoid"
  where "sign_img = ( carrier = { -1, 1 }, mult = (*), one = 1 )"


subsection ‹Basic Properties›

lemma sym_group_carrier: "p ∈ carrier (sym_group n) ⟷ p permutes {1..n}"
  unfolding sym_group_def by simp

lemma sym_group_mult: "mult (sym_group n) = (∘)"
  unfolding sym_group_def by simp

lemma sym_group_one: "one (sym_group n) = id"
  unfolding sym_group_def by simp

lemma sym_group_carrier': "p ∈ carrier (sym_group n) ==> permutation p"
  unfolding sym_group_carrier permutation_permutes by auto

lemma alt_group_carrier: "p ∈ carrier (alt_group n) ⟷ p permutes {1..n} ∧ evenperm p"
  unfolding alt_group_def by auto

lemma alt_group_mult: "mult (alt_group n) = (∘)"
  unfolding alt_group_def using sym_group_mult by simp

lemma alt_group_one: "one (alt_group n) = id"
  unfolding alt_group_def using sym_group_one by simp

lemma alt_group_carrier': "p ∈ carrier (alt_group n) ==> permutation p"
  unfolding alt_group_carrier permutation_permutes by auto

lemma sym_group_is_group: "group (sym_group n)"
  using permutes_inv permutes_inv_o(2)
  by (auto intro!: groupI
         simp add: sym_group_def permutes_compose
                   permutes_id comp_assoc, blast)

lemma sign_img_is_group: "group sign_img"
  unfolding sign_img_def by (unfold_locales, auto simp add: Units_def)

lemma sym_group_inv_closed:
  assumes "p ∈ carrier (sym_group n)" shows "inv' p ∈ carrier (sym_group n)"
  using assms permutes_inv sym_group_def by auto

lemma alt_group_inv_closed:
  assumes "p ∈ carrier (alt_group n)" shows "inv' p ∈ carrier (alt_group n)"
  using evenperm_inv[OF alt_group_carrier'] permutes_inv assms alt_group_carrier by auto

lemma sym_group_inv_equality [simp]:
  assumes "p ∈ carrier (sym_group n)" shows "inv🪙(sym_group n)🪙 p = inv' p"
proof -
  have "inv' p ∘ p = id"
    using assms permutes_inv_o(2) sym_group_def by auto
  hence "(inv' p) ⊗🪙(sym_group n)🪙 p = one (sym_group n)"
    by (simp add: sym_group_def)
  thus ?thesis  using group.inv_equality[OF sym_group_is_group]
    by (simp add: assms sym_group_inv_closed)
qed

lemma sign_is_hom: "sign ∈ hom (sym_group n) sign_img"
  unfolding hom_def sign_img_def sym_group_mult using sym_group_carrier'[of _ n]
  by (auto simp add: sign_compose, meson sign_def)

lemma sign_group_hom: "group_hom (sym_group n) sign_img sign"
  using group_hom.intro[OF sym_group_is_group sign_img_is_group] sign_is_hom
  by (simp add: group_hom_axioms_def)

lemma sign_is_surj:
  assumes "n ≥ 2" shows "sign ` (carrier (sym_group n)) = carrier sign_img"
proof -
  have "swapidseq (Suc 0) (Fun.swap (1 :: nat) 2 id)"
    using comp_Suc[OF id, of "1 :: nat" "2"] by auto
  hence "sign (Fun.swap (1 :: nat) 2 id) = (-1 :: int)"
    by (simp add: sign_swap_id)
  moreover have "Fun.swap (1 :: nat) 2 id ∈ carrier (sym_group n)" and "id ∈ carrier (sym_group n)"
    using assms permutes_swap_id[of "1 :: nat" "{1..n}" 2] permutes_id
    unfolding sym_group_carrier by auto
  ultimately have "carrier sign_img ⊆ sign ` (carrier (sym_group n))"
    using sign_id mk_disjoint_insert unfolding sign_img_def by fastforce
  moreover have "sign ` (carrier (sym_group n)) ⊆ carrier sign_img"
    using sign_is_hom unfolding hom_def by auto
  ultimately show ?thesis
    by blast
qed 

lemma alt_group_is_sign_kernel:
  "carrier (alt_group n) = kernel (sym_group n) sign_img sign"
  unfolding alt_group_def sym_group_def sign_img_def kernel_def sign_def by auto

lemma alt_group_is_subgroup: "subgroup (carrier (alt_group n)) (sym_group n)"
  using group_hom.subgroup_kernel[OF sign_group_hom]
  unfolding alt_group_is_sign_kernel by blast

lemma alt_group_is_group: "group (alt_group n)"
  using group.subgroup_imp_group[OF sym_group_is_group alt_group_is_subgroup]
  by (simp add: alt_group_def)

lemma sign_iso:
  assumes "n ≥ 2" shows "(sym_group n) Mod (carrier (alt_group n)) ≅ sign_img"
  using group_hom.FactGroup_iso[OF sign_group_hom sign_is_surj[OF assms]]
  unfolding alt_group_is_sign_kernel .

lemma alt_group_inv_equality:
  assumes "p ∈ carrier (alt_group n)" shows "inv🪙(alt_group n)🪙 p = inv' p"
proof -
  have "inv' p ∘ p = id"
    using assms permutes_inv_o(2) alt_group_def by auto
  hence "(inv' p) ⊗🪙(alt_group n)🪙 p = one (alt_group n)"
    by (simp add: alt_group_def sym_group_def)
  thus ?thesis  using group.inv_equality[OF alt_group_is_group]
    by (simp add: assms alt_group_inv_closed)
qed

lemma sym_group_card_carrier: "card (carrier (sym_group n)) = fact n"
  using card_permutations[of "{1..n}" n] unfolding sym_group_def by simp

lemma alt_group_card_carrier:
  assumes "n ≥ 2" shows "2 * card (carrier (alt_group n)) = fact n"
proof -
  have "card (rcosets🪙sym_group n🪙 (carrier (alt_group n))) = 2"
    using iso_same_card[OF sign_iso[OF assms]] unfolding FactGroup_def sign_img_def by auto
  thus ?thesis
    using group.lagrange[OF sym_group_is_group alt_group_is_subgroup, of n]
    unfolding order_def sym_group_card_carrier by simp
qed


subsection ‹Transposition Sequences›

text ‹In order to prove that the Alternating Group can be generated by 3-cycles, we need
  a stronger decomposition of permutations as transposition sequences than the one
  proposed at Permutations.thy. ›

inductive swapidseq_ext :: "'a set ==> nat ==> ('a ==> 'a) ==> bool"
  where
    empty:  "swapidseq_ext {} 0 id"
  | single: "[ swapidseq_ext S n p; a ∉ S ] ==> swapidseq_ext (insert a S) n p"
  | comp:   "[ swapidseq_ext S n p; a ≠ b ] ==>
               swapidseq_ext (insert a (insert b S)) (Suc n) ((transpose a b) ∘ p)"


lemma swapidseq_ext_finite:
  assumes "swapidseq_ext S n p" shows "finite S"
  using assms by (induction) (auto)

lemma swapidseq_ext_zero:
  assumes "finite S" shows "swapidseq_ext S 0 id"
  using assms empty by (induct set: "finite", fastforce, simp add: single)

lemma swapidseq_ext_imp_swapidseq:
  ‹swapidseq n p› if ‹swapidseq_ext S n p›
using that proof induction
  case empty
  then show ?case
    by (simp add: fun_eq_iff)
next
  case (single S n p a)
  then show ?case by simp
next
  case (comp S n p a b)
  then have ‹swapidseq (Suc n) (transpose a b ∘ p)›
    by (simp add: comp_Suc)
  then show ?case by (simp add: comp_def)
qed

lemma swapidseq_ext_zero_imp_id:
  assumes "swapidseq_ext S 0 p" shows "p = id"
proof -
  have "[ swapidseq_ext S n p; n = 0 ] ==> p = id" for n
    by (induction rule: swapidseq_ext.induct, auto)
  thus ?thesis
    using assms by simp
qed

lemma swapidseq_ext_finite_expansion:
  assumes "finite B" and "swapidseq_ext A n p" shows "swapidseq_ext (A ∪ B) n p"
  using assms
proof (induct set: "finite", simp)
  case (insert b B) show ?case
    using insert single[OF insert(3), of b] by (metis Un_insert_right insert_absorb)
qed

lemma swapidseq_ext_backwards:
  assumes "swapidseq_ext A (Suc n) p"
  shows "∃a b A' p'. a ≠ b ∧ A = (insert a (insert b A')) ∧
                     swapidseq_ext A' n p' ∧ p = (transpose a b) ∘ p'"
proof -
  have "∃a b A' p'. a ≠ b ∧ A = (insert a (insert b A')) ∧
                     swapidseq_ext A' k p' ∧ p = (transpose a b) ∘ p'"
    if "swapidseq_ext A n p" "n = Suc k"
    for A n k and p :: "'a ==> 'a"
    using that
  proof (induction)
    case empty
    thus ?case by simp
  next
    case single
    thus ?case by (metis Un_insert_right insert_iff insert_is_Un swapidseq_ext.single)
  next
    case comp
    thus ?case by blast 
  qed
  thus ?thesis using assms by simp
qed

lemma swapidseq_ext_backwards':
  assumes "swapidseq_ext A (Suc n) p"
  shows "∃a b A' p'. a ∈ A ∧ b ∈ A ∧ a ≠ b ∧ swapidseq_ext A n p' ∧ p = (transpose a b) ∘ p'"
  using swapidseq_ext_backwards[OF assms] swapidseq_ext_finite_expansion
  by (metis Un_insert_left assms insertI1 sup.idem sup_commute swapidseq_ext_finite)

lemma swapidseq_ext_endswap:
  assumes "swapidseq_ext S n p" "a ≠ b"
  shows "swapidseq_ext (insert a (insert b S)) (Suc n) (p ∘ (transpose a b))"
  using assms
proof (induction n arbitrary: S p a b)
  case 0 hence "p = id"
    using swapidseq_ext_zero_imp_id by blast
  thus ?case
    using 0 by (metis comp_id id_comp swapidseq_ext.comp) 
next
  case (Suc n)
  then obtain c d S' and p' :: "'a ==> 'a"
    where cd: "c ≠ d" and S: "S = (insert c (insert d S'))" "swapidseq_ext S' n p'"
      and p: "p = transpose c d ∘ p'"
    using swapidseq_ext_backwards[OF Suc(2)] by blast
  hence "swapidseq_ext (insert a (insert b S')) (Suc n) (p' ∘ (transpose a b))"
    by (simp add: Suc.IH Suc.prems(2))
  hence "swapidseq_ext (insert c (insert d (insert a (insert b S')))) (Suc (Suc n))
                 (transpose c d ∘ p' ∘ (transpose a b))"
    by (metis cd fun.map_comp swapidseq_ext.comp)
  thus ?case
    by (metis S(1) p insert_commute) 
qed

lemma swapidseq_ext_extension:
  assumes "swapidseq_ext A n p" and "swapidseq_ext B m q" and "A ∩ B = {}"
  shows "swapidseq_ext (A ∪ B) (n + m) (p ∘ q)"
  using assms(1,3)
proof (induction, simp add: assms(2))
  case single show ?case
    using swapidseq_ext.single[OF single(3)] single(2,4) by auto
next
  case comp show ?case
    using swapidseq_ext.comp[OF comp(3,2)] comp(4)
    by (metis Un_insert_left add_Suc insert_disjoint(1) o_assoc)
qed

lemma swapidseq_ext_of_cycles:
  assumes "cycle cs" shows "swapidseq_ext (set cs) (length cs - 1) (cycle_of_list cs)"
  using assms
proof (induct cs rule: cycle_of_list.induct)
  case (1 i j cs) show ?case
    using comp[OF 1(1), of i j] 1(2) by (simp add: o_def)  
next
  case "2_1" show ?case
    by (simp, metis eq_id_iff empty)
next
  case ("2_2" v) show ?case
    using single[OF empty, of v] by (simp, metis eq_id_iff)
qed

lemma cycle_decomp_imp_swapidseq_ext:
  assumes "cycle_decomp S p" shows "∃n. swapidseq_ext S n p"
  using assms
proof (induction)
  case empty show ?case
    using swapidseq_ext.empty by blast
next
  case (comp I p cs)
  then obtain m where m: "swapidseq_ext I m p" by blast
  hence "swapidseq_ext (set cs) (length cs - 1) (cycle_of_list cs)"
    using comp.hyps(2) swapidseq_ext_of_cycles by blast
  thus ?case using swapidseq_ext_extension m
    using comp.hyps(3) by blast
qed

lemma swapidseq_ext_of_permutation:
  assumes "p permutes S" and "finite S" shows "∃n. swapidseq_ext S n p"
  using cycle_decomp_imp_swapidseq_ext[OF cycle_decomposition[OF assms]] .

lemma split_swapidseq_ext:
  assumes "k ≤ n" and "swapidseq_ext S n p"
  obtains q r U V where "swapidseq_ext U (n - k) q" and "swapidseq_ext V k r" and "p = q ∘ r" and "U ∪ V = S"
proof -
  from assms
  have "∃q r U V. swapidseq_ext U (n - k) q ∧ swapidseq_ext V k r ∧ p = q ∘ r ∧ U ∪ V = S"
   (is "∃q r U V. ?split k q r U V")
  proof (induct k rule: inc_induct)
    case base thus ?case
      by (metis diff_self_eq_0 id_o sup_bot.left_neutral empty)
  next
    case (step m)
    then obtain q r U V
      where q: "swapidseq_ext U (n - Suc m) q" and r: "swapidseq_ext V (Suc m) r"
        and p: "p = q ∘ r" and S: "U ∪ V = S"
      by blast
    obtain a b r' V' 
      where "a ≠ b" and r': "V = (insert a (insert b V'))" "swapidseq_ext V' m r'" "r = (transpose a b) ∘ r'"
      using swapidseq_ext_backwards[OF r] by blast
    have "swapidseq_ext (insert a (insert b U)) (n - m) (q ∘ (transpose a b))"
      using swapidseq_ext_endswap[OF q ‹a ≠ b›] step(2) by (metis Suc_diff_Suc)
    hence "?split m (q ∘ (transpose a b)) r' (insert a (insert b U)) V'"
      using r' S unfolding p by fastforce 
    thus ?case by blast
  qed
  thus ?thesis
    using that by blast
qed


subsection ‹Unsolvability of Symmetric Groups›

text ‹We show that symmetric groups (🍋‹sym_group n›) are unsolvable for 🍋‹n ≥ 5›.›

abbreviation three_cycles :: "nat ==> (nat ==> nat) set"
  where "three_cycles n ≡
           { cycle_of_list cs | cs. cycle cs ∧ length cs = 3 ∧ set cs ⊆ {1..n} }"


lemma stupid_lemma:
  assumes "length cs = 3" shows "cs = [ (cs ! 0), (cs ! 1), (cs ! 2) ]"
  using assms by (auto intro!: nth_equalityI)
    (metis Suc_lessI less_2_cases not_less_eq nth_Cons_0
           nth_Cons_Suc numeral_2_eq_2 numeral_3_eq_3)

lemma three_cycles_incl: "three_cycles n ⊆ carrier (alt_group n)"
proof
  fix p assume "p ∈ three_cycles n"
  then obtain cs where cs: "p = cycle_of_list cs" "cycle cs" "length cs = 3" "set cs ⊆ {1..n}"
    by auto
  obtain a b c where cs_def: "cs = [ a, b, c ]"
    using stupid_lemma[OF cs(3)] by auto
  have "swapidseq (Suc (Suc 0)) ((transpose a b) ∘ (Fun.swap b c id))"
    using comp_Suc[OF comp_Suc[OF id], of b c a b] cs(2) unfolding cs_def by simp
  hence "evenperm p"
    using cs(1) unfolding cs_def by (simp add: evenperm_unique)
  thus "p ∈ carrier (alt_group n)"
    using permutes_subset[OF cycle_permutes cs(4)]
    unfolding alt_group_carrier cs(1) by simp
qed

lemma alt_group_carrier_as_three_cycles:
  "carrier (alt_group n) = generate (alt_group n) (three_cycles n)"
proof -
  interpret A: group "alt_group n"
    using alt_group_is_group by simp

  show ?thesis
  proof
    show "generate (alt_group n) (three_cycles n) ⊆ carrier (alt_group n)"
      using A.generate_subgroup_incl[OF three_cycles_incl A.subgroup_self] .
    show "carrier (alt_group n) ⊆ generate (alt_group n) (three_cycles n)"
    proof
      have aux_lemma1: "cycle_of_list [a, b, c] ∈ generate (alt_group n) (three_cycles n)"
        if "a ≠ b" "b ≠ c" "{ a, b, c } ⊆ {1..n}"
        for q :: "nat ==> nat" and a b c
      proof (cases)
        assume "c = a"
        hence "cycle_of_list [ a, b, c ] = id"
          by (simp add: swap_commute)
        thus "cycle_of_list [ a, b, c ] ∈ generate (alt_group n) (three_cycles n)"
          using one[of "alt_group n"] unfolding alt_group_one by simp
      next
        assume "c ≠ a"
        have "distinct [a, b, c]"
          using ‹a ≠ b› and ‹b ≠ c› and ‹c ≠ a› by auto
        with ‹{ a, b, c } ⊆ {1..n}›
        show "cycle_of_list [ a, b, c ] ∈ generate (alt_group n) (three_cycles n)"
          by (intro incl) fastforce
      qed
    
      have aux_lemma2: "q ∈ generate (alt_group n) (three_cycles n)"
        if seq: "swapidseq_ext S (Suc (Suc 0)) q" and S: "S ⊆ {1..n}"
        for S :: "nat set" and q :: "nat ==> nat"
      proof -
        obtain a b q' where ab: "a ≠ b" "a ∈ S" "b ∈ S"
          and q': "swapidseq_ext S (Suc 0) q'" "q = (transpose a b) ∘ q'"
          using swapidseq_ext_backwards'[OF seq] by auto 
        obtain c d where cd: "c ≠ d" "c ∈ S" "d ∈ S"
          and q: "q = (transpose a b) ∘ (Fun.swap c d id)"
          using swapidseq_ext_backwards'[OF q'(1)]
            swapidseq_ext_zero_imp_id
          unfolding q'(2)
          by fastforce

        consider (eq) "b = c" | (ineq) "b ≠ c" by auto
        thus ?thesis
        proof cases
          case eq
          then have "q = cycle_of_list [ a, b, d ]"
            unfolding q by simp
          moreover have "{ a, b, d } ⊆ {1..n}"
            using ab cd S by blast
          ultimately show ?thesis
            using aux_lemma1[OF ab(1)] cd(1) eq by simp
        next
          case ineq
          hence "q = cycle_of_list [ a, b, c ] ∘ cycle_of_list [ b, c, d ]"
            unfolding q by (simp add: swap_nilpotent o_assoc)
          moreover have "{ a, b, c } ⊆ {1..n}" and "{ b, c, d } ⊆ {1..n}"
            using ab cd S by blast+
          ultimately show ?thesis
            using eng[OF aux_lemma1[OF ab(1) ineq] aux_lemma1[OF ineq cd(1)]]
            unfolding alt_group_mult by simp
        qed
      qed
      
      fix p assume "p ∈ carrier (alt_group n)" then have p: "p permutes {1..n}" "evenperm p"
        unfolding alt_group_carrier by auto
      obtain m where m: "swapidseq_ext {1..n} m p"
        using swapidseq_ext_of_permutation[OF p(1)] by auto
      have "even m"
        using swapidseq_ext_imp_swapidseq[OF m] p(2) evenperm_unique by blast
      then obtain k where k: "m = 2 * k"
        by auto
      show "p ∈ generate (alt_group n) (three_cycles n)"
        using m unfolding k
      proof (induct k arbitrary: p)
        case 0 then have "p = id"
          using swapidseq_ext_zero_imp_id by simp
        show ?case
          using generate.one[of "alt_group n" "three_cycles n"]
          unfolding alt_group_one ‹p = id› .
      next
        case (Suc m)
        have arith: "2 * (Suc m) - (Suc (Suc 0)) = 2 * m" and "Suc (Suc 0) ≤ 2 * Suc m"
          by auto
        then obtain q r U V
          where q: "swapidseq_ext U (2 * m) q" and r: "swapidseq_ext V (Suc (Suc 0)) r"
            and p: "p = q ∘ r" and UV: "U ∪ V = {1..n}"
          using split_swapidseq_ext[OF _ Suc(2), of "Suc (Suc 0)"] unfolding arith by metis
        have "swapidseq_ext {1..n} (2 * m) q"
          using UV q swapidseq_ext_finite_expansion[OF swapidseq_ext_finite[OF r] q] by simp
        thus ?case
          using eng[OF Suc(1) aux_lemma2[OF r], of q] UV unfolding alt_group_mult p by blast
      qed
    qed
  qed
qed

theorem derived_alt_group_const:
  assumes "n ≥ 5" shows "derived (alt_group n) (carrier (alt_group n)) = carrier (alt_group n)"
proof
  show "derived (alt_group n) (carrier (alt_group n)) ⊆ carrier (alt_group n)"
    using group.derived_in_carrier[OF alt_group_is_group] by simp
next
  have aux_lemma: "p ∈ derived (alt_group n) (carrier (alt_group n))"
    if "p ∈ three_cycles n" for p
  proof -
    obtain cs where cs: "p = cycle_of_list cs" "cycle cs" "length cs = 3" "set cs ⊆ {1..n}"
      using ‹p ∈ three_cycles n› by auto
    then obtain a b c where cs_def: "cs = [ a, b, c ]"
      using stupid_lemma[OF cs(3)] by blast
    have "card (set cs) = 3"
      using cs(2-3)
      by (simp add: distinct_card)

    have "set cs ≠ {1..n}"
      using assms cs(3) unfolding sym[OF distinct_card[OF cs(2)]] by auto
    then obtain d where d: "d ∉ set cs" "d ∈ {1..n}"
      using cs(4) by blast

    hence "cycle (d # cs)" and "length (d # cs) = 4" and "card {1..n} = n"
      using cs(2-3) by auto 
    hence "set (d # cs) ≠ {1..n}"
      using assms unfolding sym[OF distinct_card[OF ‹cycle (d # cs)›]]
      by (metis Suc_n_not_le_n eval_nat_numeral(3)) 
    then obtain e where e: "e ∉ set (d # cs)" "e ∈ {1..n}"
      using d cs(4) by (metis insert_subset list.simps(15) subsetI subset_antisym) 

    define q where "q = (Fun.swap d e id) ∘ (Fun.swap b c id)"
    hence "bij q"
      by (simp add: bij_comp)
    moreover have "q b = c" and "q c = b"
      using d(1) e(1) unfolding q_def cs_def by simp+
    moreover have "q a = a"
      using d(1) e(1) cs(2) unfolding q_def cs_def by auto
    ultimately have "q ∘ p ∘ (inv' q) = cycle_of_list [ a, c, b ]"
      using conjugation_of_cycle[OF cs(2), of q]
      unfolding sym[OF cs(1)] unfolding cs_def by simp
    also have " ... = p ∘ p"
      using cs(2) unfolding cs(1) cs_def
      by (simp add: comp_swap swap_commute transpose_comp_triple) 
    finally have "q ∘ p ∘ (inv' q) = p ∘ p" .
    moreover have "bij p"
      unfolding cs(1) cs_def by (simp add: bij_comp)
    ultimately have p: "q ∘ p ∘ (inv' q) ∘ (inv' p) = p"
      by (simp add: bijection.intro bijection.inv_comp_right comp_assoc)

    have "swapidseq (Suc (Suc 0)) q"
      using comp_Suc[OF comp_Suc[OF id], of b c d e] e(1) cs(2)  unfolding q_def cs_def by auto
    hence "evenperm q"
      using even_Suc_Suc_iff evenperm_unique by blast
    moreover have "q permutes { d, e, b, c }"
      unfolding q_def by (simp add: permutes_compose permutes_swap_id)
    hence "q permutes {1..n}"
      using cs(4) d(2) e(2) permutes_subset unfolding cs_def by fastforce
    ultimately have "q ∈ carrier (alt_group n)"
      unfolding alt_group_carrier by simp
    moreover have "p ∈ carrier (alt_group n)"
      using ‹p ∈ three_cycles n› three_cycles_incl by blast
    ultimately have "p ∈ derived_set (alt_group n) (carrier (alt_group n))"
      using p alt_group_inv_equality unfolding alt_group_mult
      by (metis (no_types, lifting) UN_iff singletonI)
    thus "p ∈ derived (alt_group n) (carrier (alt_group n))"
      unfolding derived_def by (rule incl)
  qed

  interpret A: group "alt_group n"
    using alt_group_is_group .

  have "generate (alt_group n) (three_cycles n) ⊆ derived (alt_group n) (carrier (alt_group n))"
    using A.generate_subgroup_incl[OF _ A.derived_is_subgroup] aux_lemma by (meson subsetI) 
  thus "carrier (alt_group n) ⊆ derived (alt_group n) (carrier (alt_group n))"
    using alt_group_carrier_as_three_cycles by simp
qed

corollary alt_group_is_unsolvable:
  assumes "n ≥ 5" shows "¬ solvable (alt_group n)"
proof (rule ccontr)
  assume "¬ ¬ solvable (alt_group n)"
  then obtain m where "(derived (alt_group n) ^^ m) (carrier (alt_group n)) = { id }"
    using group.solvable_iff_trivial_derived_seq[OF alt_group_is_group] unfolding alt_group_one by blast
  moreover have "(derived (alt_group n) ^^ m) (carrier (alt_group n)) = carrier (alt_group n)"
    using derived_alt_group_const[OF assms] by (induct m) (auto)
  ultimately have card_eq_1: "card (carrier (alt_group n)) = 1"
    by simp
  have ge_2: "n ≥ 2"
    using assms by simp
  moreover have "2 = fact n"
    using alt_group_card_carrier[OF ge_2] unfolding card_eq_1
    by (metis fact_2 mult.right_neutral of_nat_fact)
  ultimately have "n = 2"
      by (metis antisym_conv fact_ge_self)
  thus False
    using assms by simp
qed

corollary sym_group_is_unsolvable:
  assumes "n ≥ 5" shows "¬ solvable (sym_group n)"
proof -
  interpret Id: group_hom "alt_group n" "sym_group n" id
    using group.canonical_inj_is_hom[OF sym_group_is_group alt_group_is_subgroup] alt_group_def by simp
  show ?thesis
    using Id.inj_hom_imp_solvable alt_group_is_unsolvable[OF assms] by auto
qed

end