(* Title: HOL/Algebra/Sym_Groups.thy
Author: Paulo EmÃlio de Vilhena
*)
theory Sym_Groups
imports Cycles Solvable_Groups
begin
section \<open>Symmetric Groups\<close>
subsection \<open>Definitions\<close>
abbreviation inv' :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"
where "inv' f \<equiv> Hilbert_Choice.inv f"
definition sym_group :: "nat \<Rightarrow> (nat \<Rightarrow> nat) monoid"
where "sym_group n = \<lparr> carrier = { p. p permutes {1..n} }, mult = (\<circ>), one = id \<rparr>"
definition alt_group :: "nat \<Rightarrow> (nat \<Rightarrow> nat) monoid"
where "alt_group n = (sym_group n) \<lparr> carrier := { p. p permutes {1..n} \<and> evenperm p } \<rparr>"
definition sign_img :: "int monoid"
where "sign_img = \<lparr> carrier = { -1, 1 }, mult = (*), one = 1 \<rparr>"
subsection \<open>Basic Properties\<close>
lemma sym_group_carrier: "p \<in> carrier (sym_group n) \<longleftrightarrow> p permutes {1..n}"
unfolding sym_group_def by simp
lemma sym_group_mult: "mult (sym_group n) = (\<circ>)"
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 \<in> carrier (sym_group n) \<Longrightarrow> permutation p"
unfolding sym_group_carrier permutation_permutes by auto
lemma alt_group_carrier: "p \<in> carrier (alt_group n) \<longleftrightarrow> p permutes {1..n} \<and> evenperm p"
unfolding alt_group_def by auto
lemma alt_group_mult: "mult (alt_group n) = (\<circ>)"
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 \<in> carrier (alt_group n) \<Longrightarrow> 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 \<in> carrier (sym_group n)" shows "inv' p \<in> carrier (sym_group n)"
using assms permutes_inv sym_group_def by auto
lemma alt_group_inv_closed:
assumes "p \<in> carrier (alt_group n)" shows "inv' p \<in> 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 \<in> carrier (sym_group n)" shows "inv\<^bsub>(sym_group n)\<^esub> p = inv' p"
proof -
have "inv' p \<circ> p = id"
using assms permutes_inv_o(2) sym_group_def by auto
hence "(inv' p) \<otimes>\<^bsub>(sym_group n)\<^esub> 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 \<in> 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 \<ge> 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 \<in> carrier (sym_group n)" and "id \<in> 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 \<subseteq> sign ` (carrier (sym_group n))"
using sign_id mk_disjoint_insert unfolding sign_img_def by fastforce
moreover have "sign ` (carrier (sym_group n)) \<subseteq> 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 \<ge> 2" shows "(sym_group n) Mod (carrier (alt_group n)) \<cong> 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 \<in> carrier (alt_group n)" shows "inv\<^bsub>(alt_group n)\<^esub> p = inv' p"
proof -
have "inv' p \<circ> p = id"
using assms permutes_inv_o(2) alt_group_def by auto
hence "(inv' p) \<otimes>\<^bsub>(alt_group n)\<^esub> 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 \<ge> 2" shows "2 * card (carrier (alt_group n)) = fact n"
proof -
have "card (rcosets\<^bsub>sym_group n\<^esub> (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 \<open>Transposition Sequences\<close>
text \<open>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. \<close>
inductive swapidseq_ext :: "'a set \<Rightarrow> nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool"
where
empty: "swapidseq_ext {} 0 id"
| single: "\<lbrakk> swapidseq_ext S n p; a \<notin> S \<rbrakk> \<Longrightarrow> swapidseq_ext (insert a S) n p"
| comp: "\<lbrakk> swapidseq_ext S n p; a \<noteq> b \<rbrakk> \<Longrightarrow>
swapidseq_ext (insert a (insert b S)) (Suc n) ((Fun.swap a b id) \<circ> 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:
assumes "swapidseq_ext S n p" shows "swapidseq n p"
using assms by (induction, simp, simp, meson comp_Suc)
lemma swapidseq_ext_zero_imp_id:
assumes "swapidseq_ext S 0 p" shows "p = id"
proof -
have "\<lbrakk> swapidseq_ext S n p; n = 0 \<rbrakk> \<Longrightarrow> 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 \<union> 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 "\<exists>a b A' p'. a \<noteq> b \<and> A = (insert a (insert b A')) \<and>
swapidseq_ext A' n p' \<and> p = (Fun.swap a b id) \<circ> p'"
proof -
{ fix A n k and p :: "'a \<Rightarrow> 'a"
assume "swapidseq_ext A n p" "n = Suc k"
hence "\<exists>a b A' p'. a \<noteq> b \<and> A = (insert a (insert b A')) \<and>
swapidseq_ext A' k p' \<and> p = (Fun.swap a b id) \<circ> p'"
proof (induction, simp)
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 "\<exists>a b A' p'. a \<in> A \<and> b \<in> A \<and> a \<noteq> b \<and> swapidseq_ext A n p' \<and> p = (Fun.swap a b id) \<circ> 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 \<noteq> b"
shows "swapidseq_ext (insert a (insert b S)) (Suc n) (p \<circ> (Fun.swap a b id))"
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 \<Rightarrow> 'a"
where cd: "c \<noteq> d" and S: "S = (insert c (insert d S'))" "swapidseq_ext S' n p'"
and p: "p = (Fun.swap c d id) \<circ> p'"
using swapidseq_ext_backwards[OF Suc(2)] by blast
hence "swapidseq_ext (insert a (insert b S')) (Suc n) (p' \<circ> (Fun.swap a b id))"
by (simp add: Suc.IH Suc.prems(2))
hence "swapidseq_ext (insert c (insert d (insert a (insert b S')))) (Suc (Suc n))
((Fun.swap c d id) \<circ> p' \<circ> (Fun.swap a b id))"
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 \<inter> B = {}"
shows "swapidseq_ext (A \<union> B) (n + m) (p \<circ> 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 "\<exists>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 "\<exists>n. swapidseq_ext S n p"
using cycle_decomp_imp_swapidseq_ext[OF cycle_decomposition[OF assms]] .
lemma split_swapidseq_ext:
assumes "k \<le> 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 \<circ> r" and "U \<union> V = S"
proof -
from assms
have "\<exists>q r U V. swapidseq_ext U (n - k) q \<and> swapidseq_ext V k r \<and> p = q \<circ> r \<and> U \<union> V = S"
(is "\<exists>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 \<circ> r" and S: "U \<union> V = S"
by blast
obtain a b r' V'
where "a \<noteq> b" and r': "V = (insert a (insert b V'))" "swapidseq_ext V' m r'" "r = (Fun.swap a b id) \<circ> r'"
using swapidseq_ext_backwards[OF r] by blast
have "swapidseq_ext (insert a (insert b U)) (n - m) (q \<circ> (Fun.swap a b id))"
using swapidseq_ext_endswap[OF q \<open>a \<noteq> b\<close>] step(2) by (metis Suc_diff_Suc)
hence "?split m (q \<circ> (Fun.swap a b id)) 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 \<open>Unsolvability of Symmetric Groups\<close>
text \<open>We show that symmetric groups (\<^term>\<open>sym_group n\<close>) are unsolvable for \<^term>\<open>n \<ge> 5\<close>.\<close>
abbreviation three_cycles :: "nat \<Rightarrow> (nat \<Rightarrow> nat) set"
where "three_cycles n \<equiv>
{ cycle_of_list cs | cs. cycle cs \<and> length cs = 3 \<and> set cs \<subseteq> {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 \<subseteq> carrier (alt_group n)"
proof
fix p assume "p \<in> three_cycles n"
then obtain cs where cs: "p = cycle_of_list cs" "cycle cs" "length cs = 3" "set cs \<subseteq> {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)) ((Fun.swap a b id) \<circ> (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 \<in> 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) \<subseteq> carrier (alt_group n)"
using A.generate_subgroup_incl[OF three_cycles_incl A.subgroup_self] .
next
show "carrier (alt_group n) \<subseteq> generate (alt_group n) (three_cycles n)"
proof
{ fix q :: "nat \<Rightarrow> nat" and a b c
assume "a \<noteq> b" "b \<noteq> c" "{ a, b, c } \<subseteq> {1..n}"
have "cycle_of_list [a, b, c] \<in> generate (alt_group n) (three_cycles n)"
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 ] \<in> generate (alt_group n) (three_cycles n)"
using one[of "alt_group n"] unfolding alt_group_one by simp
next
assume "c \<noteq> a"
have "distinct [a, b, c]"
using \<open>a \<noteq> b\<close> and \<open>b \<noteq> c\<close> and \<open>c \<noteq> a\<close> by auto
with \<open>{ a, b, c } \<subseteq> {1..n}\<close>
show "cycle_of_list [ a, b, c ] \<in> generate (alt_group n) (three_cycles n)"
by (intro incl, fastforce)
qed } note aux_lemma1 = this
{ fix S :: "nat set" and q :: "nat \<Rightarrow> nat"
assume seq: "swapidseq_ext S (Suc (Suc 0)) q" and S: "S \<subseteq> {1..n}"
have "q \<in> generate (alt_group n) (three_cycles n)"
proof -
obtain a b q' where ab: "a \<noteq> b" "a \<in> S" "b \<in> S"
and q': "swapidseq_ext S (Suc 0) q'" "q = (Fun.swap a b id) \<circ> q'"
using swapidseq_ext_backwards'[OF seq] by auto
obtain c d where cd: "c \<noteq> d" "c \<in> S" "d \<in> S"
and q: "q = (Fun.swap a b id) \<circ> (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 \<noteq> 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 } \<subseteq> {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 ] \<circ> cycle_of_list [ b, c, d ]"
unfolding q by (simp add: comp_swap)
moreover have "{ a, b, c } \<subseteq> {1..n}" and "{ b, c, d } \<subseteq> {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 } note aux_lemma2 = this
fix p assume "p \<in> 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 \<in> 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 \<open>p = id\<close> .
next
case (Suc m)
have arith: "2 * (Suc m) - (Suc (Suc 0)) = 2 * m" and "Suc (Suc 0) \<le> 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 \<circ> r" and UV: "U \<union> 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 \<ge> 5" shows "derived (alt_group n) (carrier (alt_group n)) = carrier (alt_group n)"
proof
show "derived (alt_group n) (carrier (alt_group n)) \<subseteq> carrier (alt_group n)"
using group.derived_in_carrier[OF alt_group_is_group] by simp
next
{ fix p assume "p \<in> three_cycles n" have "p \<in> derived (alt_group n) (carrier (alt_group n))"
proof -
obtain cs where cs: "p = cycle_of_list cs" "cycle cs" "length cs = 3" "set cs \<subseteq> {1..n}"
using \<open>p \<in> three_cycles n\<close> 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 \<noteq> {1..n}"
using assms cs(3) unfolding sym[OF distinct_card[OF cs(2)]] by auto
then obtain d where d: "d \<notin> set cs" "d \<in> {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) \<noteq> {1..n}"
using assms unfolding sym[OF distinct_card[OF \<open>cycle (d # cs)\<close>]]
by (metis Suc_n_not_le_n eval_nat_numeral(3))
then obtain e where e: "e \<notin> set (d # cs)" "e \<in> {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) \<circ> (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 \<circ> p \<circ> (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 \<circ> p"
using cs(2) unfolding cs(1) cs_def
by (auto, metis comp_id comp_swap swap_commute swap_triple)
finally have "q \<circ> p \<circ> (inv' q) = p \<circ> p" .
moreover have "bij p"
unfolding cs(1) cs_def by (simp add: bij_comp)
ultimately have p: "q \<circ> p \<circ> (inv' q) \<circ> (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 \<in> carrier (alt_group n)"
unfolding alt_group_carrier by simp
moreover have "p \<in> carrier (alt_group n)"
using \<open>p \<in> three_cycles n\<close> three_cycles_incl by blast
ultimately have "p \<in> 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 \<in> derived (alt_group n) (carrier (alt_group n))"
unfolding derived_def by (rule incl)
qed } note aux_lemma = this
interpret A: group "alt_group n"
using alt_group_is_group .
have "generate (alt_group n) (three_cycles n) \<subseteq> 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) \<subseteq> 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 \<ge> 5" shows "\<not> solvable (alt_group n)"
proof (rule ccontr)
assume "\<not> \<not> 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 \<ge> 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 \<ge> 5" shows "\<not> 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