-
Notifications
You must be signed in to change notification settings - Fork 0
/
Sym_Groups.thy
554 lines (481 loc) · 23.1 KB
/
Sym_Groups.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
(* 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 symetric groups (sym_group n) are unsolvable for n \<ge> 5.\<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
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)
hence "n = 2"
by (smt fact_ge_self ge_2 le_antisym)
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