(* Title: HOL/GroupTheory/Sylow
ID: $Id$
Author: Florian Kammueller, with new proofs by L C Paulson
Copyright 1998-2001 University of Cambridge
Sylow's theorem using locales (combinatorial argument in Exponent.thy)
See Florian Kamm\"uller and L. C. Paulson,
A Formal Proof of Sylow's theorem:
An Experiment in Abstract Algebra with Isabelle HOL
J. Automated Reasoning 23 (1999), 235-264
*)
Open_locale "sylow";
val prime_p = thm "prime_p";
val order_G = thm "order_G";
val finite_G = thm "finite_G";
val calM_def = thm "calM_def";
val RelM_def = thm "RelM_def";
AddIffs [finite_G];
Addsimps [coset_mul_e];
Goalw [refl_def, RelM_def] "refl calM RelM";
by Auto_tac;
by (asm_full_simp_tac (simpset() addsimps [calM_def]) 1);
by (res_inst_tac [("x","e")] bexI 1);
by (auto_tac (claset(), simpset() addsimps [e_closed]));
qed "RelM_refl";
Goalw [sym_def, RelM_def] "sym RelM";
by Auto_tac;
by (res_inst_tac [("x","i g")] bexI 1);
by (etac inv_closed 2);
by (asm_full_simp_tac
(simpset() addsimps [coset_mul_assoc, calM_def, inv_closed]) 1);
qed "RelM_sym";
Goalw [trans_def, RelM_def] "trans RelM";
by Auto_tac;
by (res_inst_tac [("x","ga ## g")] bexI 1);
by (ALLGOALS (asm_full_simp_tac
(simpset() addsimps [coset_mul_assoc, calM_def, binop_closed])));
qed "RelM_trans";
Goalw [equiv_def] "equiv calM RelM";
by (blast_tac (claset() addIs [RelM_refl, RelM_sym, RelM_trans]) 1);
qed "RelM_equiv";
Goalw [RelM_def] "M \\<in> calM // RelM ==> M <= calM";
by (blast_tac (claset() addSEs [quotientE]) 1);
qed "M_subset_calM_prep";
(*** Central Part of the Proof ***)
Open_locale "sylow_central";
val M_in_quot = thm "M_in_quot";
val not_dvd_M = thm "not_dvd_M";
val M1_in_M = thm "M1_in_M";
val H_def = thm "H_def";
Goal "M <= calM";
by (rtac (M_in_quot RS M_subset_calM_prep) 1);
qed "M_subset_calM";
Goal "card(M1) = p^a";
by (cut_facts_tac [M_subset_calM, M1_in_M] 1);
by (asm_full_simp_tac (simpset() addsimps [calM_def]) 1);
by (Blast_tac 1);
qed "card_M1";
Goal "\\<exists>x. x\\<in>M1";
by (rtac (card_nonempty RS NotEmpty_ExEl) 1);
by (cut_facts_tac [prime_p RS prime_imp_one_less] 1);
by (asm_simp_tac (simpset() addsimps [card_M1]) 1);
qed "exists_x_in_M1";
Goal "M1 <= carrier G";
by (rtac (subsetD RS PowD) 1);
by (rtac M1_in_M 2);
by (rtac (M_subset_calM RS subset_trans) 1);
by (auto_tac (claset(), simpset() addsimps [calM_def]));
qed "M1_subset_G";
Goal "\\<exists>f \\<in> H\\<rightarrow>M1. inj_on f H";
by (rtac (exists_x_in_M1 RS exE) 1);
by (res_inst_tac [("x", "%z: H. x ## z")] bexI 1);
by (rtac restrictI 2);
by (asm_full_simp_tac (simpset() addsimps [H_def]) 2);
by (Clarify_tac 2);
by (etac subst 2);
by (asm_full_simp_tac (simpset() addsimps [rcosI, M1_subset_G]) 2);
by (rtac inj_onI 1);
by (rtac left_cancellation 1);
by (auto_tac (claset(), simpset() addsimps [H_def, M1_subset_G RS subsetD]));
qed "M1_inj_H";
Goal "{} \\<notin> calM // RelM";
by (blast_tac (claset() addSEs [quotientE]
addDs [RelM_equiv RS equiv_class_self]) 1);
qed "EmptyNotInEquivSet";
Goal "\\<exists>M1. M1\\<in>M";
by (cut_facts_tac [M_in_quot, EmptyNotInEquivSet] 1);
by (blast_tac (claset() addIs [NotEmpty_ExEl]) 1);
qed "existsM1inM";
val ExistsM1inM = Export existsM1inM;
Goalw [order_def] "0 < order(G)";
by (cut_facts_tac [e_closed] 1);
by (blast_tac (claset() addIs [zero_less_card_empty]) 1);
qed "zero_less_o_G";
Goal "0 < m";
by (cut_facts_tac [zero_less_o_G] 1);
by (asm_full_simp_tac (simpset() addsimps [order_G]) 1);
qed "zero_less_m";
Goal "card(calM) = (p^a) * m choose p^a";
by (simp_tac (simpset() addsimps [calM_def, n_subsets,
order_G RS sym, order_def]) 1);
qed "card_calM";
Goal "0 < card calM";
by (simp_tac (simpset() addsimps [card_calM, zero_less_binomial,
le_extend_mult, zero_less_m]) 1);
qed "zero_less_card_calM";
Goal "~ (p ^ Suc(exponent p m) dvd card(calM))";
by (subgoal_tac "exponent p m = exponent p (card calM)" 1);
by (asm_full_simp_tac (simpset() addsimps [card_calM,
zero_less_m RS const_p_fac]) 2);
by (cut_facts_tac [zero_less_card_calM, prime_p] 1);
by (force_tac (claset() addDs [power_Suc_exponent_Not_dvd], simpset()) 1);
qed "max_p_div_calM";
Goalw [calM_def] "finite calM";
by (res_inst_tac [("B", "Pow (carrier G)")] finite_subset 1);
by Auto_tac;
qed "finite_calM";
Goal "\\<exists>M \\<in> calM // RelM. ~ (p ^ Suc(exponent p m) dvd card(M))";
by (rtac (max_p_div_calM RS contrapos_np) 1);
by (asm_full_simp_tac (simpset() addsimps [finite_calM,
RelM_equiv RSN(2, equiv_imp_dvd_card)]) 1);
qed "lemma_A1";
val Lemma_A1 = Export lemma_A1;
Goal "x \\<in> H ==> x \\<in> carrier G";
by (afs [H_def] 1);
qed "H_into_carrier_G";
Goal "g : H ==> M1 #> g = M1";
by (asm_full_simp_tac (simpset() addsimps [H_def]) 1);
qed "in_H_imp_eq";
Goalw [H_def] "[| x\\<in>H; xa\\<in>H|] ==> x ## xa\\<in>H";
by (asm_full_simp_tac (simpset() addsimps [coset_mul_assoc RS sym,
binop_closed, M1_subset_G]) 1);
qed "bin_op_closed_lemma";
Goal "H \\<noteq> {}";
by (asm_full_simp_tac (simpset() addsimps [H_def]) 1);
by (res_inst_tac [("x","e")] exI 1);
by (asm_full_simp_tac (simpset() addsimps [e_closed, M1_subset_G]) 1);
qed "H_not_empty";
Goal "H <<= G";
by (rtac subgroupI 1);
by (rtac subsetI 1);
by (etac H_into_carrier_G 1);
by (rtac H_not_empty 1);
by (afs [H_def, inv_closed] 1);
by (Clarify_tac 1);
by (eres_inst_tac [("P","%z. z #> i a = M1")] subst 1);
by (asm_simp_tac (simpset() addsimps [coset_mul_assoc, inv_closed,
inv_ax1, coset_mul_e, M1_subset_G]) 1);
by (blast_tac (claset() addIs [bin_op_closed_lemma]) 1);
qed "H_is_SG";
val H_is_subgroup = Export H_is_SG;
Goal "[| g\\<in>carrier G; x\\<in>M1 #> g |] ==> x\\<in>carrier G";
by (rtac (r_coset_subset_G RS subsetD) 1);
by (assume_tac 3);
by (assume_tac 2);
by (rtac M1_subset_G 1);
qed "rcosetGM1g_subset_G";
Goal "finite M1";
by (rtac ([ M1_subset_G, finite_G] MRS finite_subset) 1);
qed "finite_M1";
Goal "g\\<in>carrier G ==> finite (M1 #> g)";
by (rtac finite_subset 1);
by (rtac subsetI 1);
by (etac rcosetGM1g_subset_G 1);
by (assume_tac 1);
by (rtac finite_G 1);
qed "finite_rcosetGM1g";
Goal "g\\<in>carrier G ==> card(M1 #> g) = card(M1)";
by (asm_simp_tac
(simpset() addsimps [M1_subset_G, card_cosets_equal, setrcosI]) 1);
qed "M1_cardeq_rcosetGM1g";
Goal "g \\<in> carrier G ==> (M1, M1 #> g) \\<in> RelM";
by (simp_tac (simpset() addsimps [RelM_def,calM_def,card_M1,M1_subset_G]) 1);
by (rtac conjI 1);
by (blast_tac (claset() addIs [rcosetGM1g_subset_G]) 1);
by (asm_simp_tac (simpset() addsimps [card_M1, M1_cardeq_rcosetGM1g]) 1);
by (res_inst_tac [("x","i g")] bexI 1);
by (asm_full_simp_tac (simpset() addsimps [coset_mul_assoc, M1_subset_G,
inv_closed, inv_ax1]) 1);
by (asm_simp_tac (simpset() addsimps [inv_closed]) 1);
qed "M1_RelM_rcosetGM1g";
(*** A pair of injections between M and {*H*} shows their cardinalities are
equal ***)
Goal "M2 \\<in> M ==> \\<exists>g. g \\<in> carrier G & M1 #> g = M2";
by (cut_facts_tac [M1_in_M, M_in_quot RS (RelM_equiv RS ElemClassEquiv)] 1);
by (asm_full_simp_tac (simpset() addsimps [RelM_def]) 1);
by (blast_tac (claset() addSDs [bspec]) 1);
qed "M_elem_map";
val M_elem_map_carrier = M_elem_map RS someI_ex RS conjunct1;
val M_elem_map_eq = M_elem_map RS someI_ex RS conjunct2;
Goal "(%x:M. H #> (SOME g. g \\<in> carrier G & M1 #> g = x)) \\<in> M \\<rightarrow> {* H *}";
by (rtac (setrcosI RS restrictI) 1);
by (rtac (H_is_SG RS subgroup_imp_subset) 1);
by (etac M_elem_map_carrier 1);
qed "M_funcset_setrcos_H";
Goal "\\<exists>f \\<in> M\\<rightarrow>{* H *}. inj_on f M";
by (rtac bexI 1);
by (rtac M_funcset_setrcos_H 2);
by (rtac inj_onI 1);
by (Asm_full_simp_tac 1);
by (rtac ([asm_rl,M_elem_map_eq] MRS trans) 1);
by (assume_tac 2);
by (rtac ((M_elem_map_eq RS sym) RS trans) 1);
by (assume_tac 1);
by (rtac coset_mul_inv1 1);
by (REPEAT (etac M_elem_map_carrier 2));
by (rtac M1_subset_G 2);
by (rtac (coset_join1 RS in_H_imp_eq) 1);
by (rtac H_is_SG 3);
by (blast_tac (claset() addIs [binop_closed,M_elem_map_carrier,inv_closed]) 2);
by (asm_full_simp_tac (simpset() addsimps [coset_mul_invers2, H_def,
M_elem_map_carrier, subset_def]) 1);
qed "inj_M_GmodH";
(** the opposite injection **)
Goal "H1\\<in>{* H *} ==> \\<exists>g. g \\<in> carrier G & H #> g = H1";
by (auto_tac (claset(), simpset() addsimps [setrcos_eq]));
qed "H_elem_map";
val H_elem_map_carrier = H_elem_map RS someI_ex RS conjunct1;
val H_elem_map_eq = H_elem_map RS someI_ex RS conjunct2;
Goal "(%C:{*H*}. M1 #> (@g. g \\<in> (G .<cr>) \\<and> H #> g = C)) \\<in> {* H *} \\<rightarrow> M";
by (simp_tac (simpset() addsimps [setrcos_eq]) 1);
by (deepen_tac (claset() addIs [someI2]
addSIs [restrictI, RelM_equiv, M_in_quot,
M1_RelM_rcosetGM1g RSN (4, EquivElemClass),M1_in_M]) 0 1);
qed "setrcos_H_funcset_M";
Goal "\\<exists>g \\<in> {* H *}\\<rightarrow>M. inj_on g ({* H *})";
by (rtac bexI 1);
by (rtac setrcos_H_funcset_M 2);
by (rtac inj_onI 1);
by (rotate_tac ~2 1);
by (Asm_full_simp_tac 1);
by (rtac ([asm_rl,H_elem_map_eq] MRS trans) 1);
by (assume_tac 2);
by (rtac ((H_elem_map_eq RS sym) RS trans) 1);
by (assume_tac 1);
by (rtac coset_mul_inv1 1);
by (REPEAT (etac H_elem_map_carrier 2));
by (rtac (H_is_SG RS subgroup_imp_subset) 2);
by (rtac coset_join2 1);
by (blast_tac (claset() addIs [binop_closed,inv_closed,H_elem_map_carrier]) 1);
by (rtac H_is_SG 1);
by (asm_full_simp_tac (simpset() addsimps [H_def, coset_mul_invers2,
M1_subset_G, H_elem_map_carrier]) 1);
qed "inj_GmodH_M";
Goal "calM <= Pow(carrier G)";
by (auto_tac (claset(), simpset() addsimps [calM_def]));
qed "calM_subset_PowG";
Goal "finite M";
by (rtac finite_subset 1);
by (rtac (M_subset_calM RS subset_trans) 1);
by (rtac calM_subset_PowG 1);
by (Blast_tac 1);
qed "finite_M";
Goal "card(M) = card({* H *})";
by (blast_tac (claset() addSIs [inj_M_GmodH,inj_GmodH_M]
addIs [card_bij, finite_M, H_is_SG,
setrcos_subset_PowG RS finite_subset,
finite_Pow_iff RS iffD2]) 1);
qed "cardMeqIndexH";
Goal "card(M) * card(H) = order(G)";
by (simp_tac (simpset() addsimps [cardMeqIndexH,lagrange, H_is_SG]) 1);
qed "index_lem";
Goal "p^a <= card(H)";
by (rtac ([prime_p,not_dvd_M] MRS div_combine RS dvd_imp_le) 1);
by (blast_tac (claset() addIs [SG_card1,H_is_SG]) 2);
by (simp_tac (simpset() addsimps [index_lem,order_G,power_add,mult_dvd_mono,
power_exponent_dvd,zero_less_m]) 1);
qed "lemma_leq1";
Goal "card(H) <= p^a";
by (stac (card_M1 RS sym) 1);
by (cut_facts_tac [M1_inj_H] 1);
by (blast_tac (claset() addSIs [M1_subset_G]
addIs [card_inj, H_into_carrier_G,
finite_G RSN(2, finite_subset)]) 1);
qed "lemma_leq2";
Goal "card(H) = p^a";
by (blast_tac (claset() addIs [le_anti_sym, lemma_leq1, lemma_leq2]) 1);
qed "card_H_eq";
val Card_H_eq = Export card_H_eq;
Close_locale "sylow_central";
Goal "\\<exists>H. H <<= G & card(H) = p^a";
by (cut_facts_tac [Lemma_A1] 1);
by (blast_tac (claset() addDs [ExistsM1inM, H_is_subgroup, Card_H_eq]) 1);
qed "sylow1";
val Sylow1 = export sylow1;
Close_locale "sylow";
Close_locale "coset";
Close_locale "group";