(* Title: HOL/GroupTheory/Coset
ID: $Id$
Author: Florian Kammueller, with new proofs by L C Paulson
Copyright 1998-2001 University of Cambridge
Theory of cosets, using locales
*)
(** these versions are useful for Sylow's Theorem **)
Goal "[|finite A; finite B; \\<exists>f \\<in> A\\<rightarrow>B. inj_on f A|] ==> card(A) <= card(B)";
by (Clarify_tac 1);
by (rtac card_inj_on_le 1);
by (auto_tac (claset(), simpset() addsimps [Pi_def]));
qed "card_inj";
Goal "[| finite A; finite B; \\<exists>f \\<in> A\\<rightarrow>B. inj_on f A; \
\ \\<exists>g \\<in> B\\<rightarrow>A. inj_on g B |] ==> card(A) = card(B)";
by (Clarify_tac 1);
by (rtac card_bij_eq 1);
by (auto_tac (claset(), simpset() addsimps [Pi_def]));
qed "card_bij";
Open_locale "coset";
Addsimps [Group_G, simp_G];
val rcos_def = thm "rcos_def";
val lcos_def = thm "lcos_def";
val setprod_def = thm "setprod_def";
val setinv_def = thm "setinv_def";
val setrcos_def = thm "setrcos_def";
val group_defs = [thm "binop_def", thm "inv_def", thm "e_def"];
val coset_defs = [thm "rcos_def", thm "lcos_def", thm "setprod_def"];
(** Alternative definitions, reducing to locale constants **)
Goal "H #> a = {b . \\<exists>h\\<in>H. h ## a = b}";
by (auto_tac (claset(),
simpset() addsimps [rcos_def, r_coset_def, binop_def]));
qed "r_coset_eq";
Goal "a <# H = {b . \\<exists>h\\<in>H. a ## h = b}";
by (auto_tac (claset(),
simpset() addsimps [lcos_def, l_coset_def, binop_def]));
qed "l_coset_eq";
Goal "{*H*} = {C . \\<exists>a\\<in>carrier G. C = H #> a}";
by (auto_tac (claset(),
simpset() addsimps [set_r_cos_def, setrcos_def, rcos_def, binop_def]));
qed "setrcos_eq";
Goal "H <#> K = {c . \\<exists>h\\<in>H. \\<exists>k\\<in>K. c = h ## k}";
by (simp_tac
(simpset() addsimps [setprod_def, set_prod_def, binop_def, image_def]) 1);
qed "set_prod_eq";
Goal "[| M <= carrier G; g\\<in>carrier G; h\\<in>carrier G |] \
\ ==> (M #> g) #> h = M #> (g ## h)";
by (force_tac (claset(), simpset() addsimps [r_coset_eq, binop_assoc]) 1);
qed "coset_mul_assoc";
Goal "[| M <= carrier G |] ==> M #> e = M";
by (force_tac (claset(), simpset() addsimps [r_coset_eq]) 1);
qed "coset_mul_e";
Goal "[| M #> (x ## (i y)) = M; x \\<in> carrier G ; y \\<in> carrier G;\
\ M <= carrier G |] ==> M #> x = M #> y";
by (eres_inst_tac [("P","%z. M #> x = z #> y")] subst 1);
by (asm_simp_tac (simpset() addsimps [coset_mul_assoc, binop_assoc]) 1);
qed "coset_mul_inv1";
Goal "[| M #> x = M #> y; x \\<in> carrier G; y \\<in> carrier G; M <= carrier G |] \
\ ==> M #> (x ## (i y)) = M ";
by (afs [coset_mul_assoc RS sym] 1);
by (afs [coset_mul_assoc, coset_mul_e] 1);
qed "coset_mul_invers2";
Goal "[| H #> x = H; x \\<in> carrier G; H <<= G |] ==> x\\<in>H";
by (etac subst 1);
by (simp_tac (simpset() addsimps [r_coset_eq]) 1);
by (blast_tac (claset() addIs [e_ax1, subgroup_e_closed]) 1);
qed "coset_join1";
Goal "[| x\\<in>carrier G; H <<= G; x\\<in>H |] ==> H #> x = H";
by (auto_tac (claset(), simpset() addsimps [r_coset_eq]));
by (res_inst_tac [("x","xa ## (i x)")] bexI 2);
by (auto_tac (claset(),
simpset() addsimps [subgroup_f_closed, subgroup_inv_closed,
binop_assoc, subgroup_imp_subset RS subsetD]));
qed "coset_join2";
Goal "[| H <= carrier G; x\\<in>carrier G |] ==> H #> x <= carrier G";
by (auto_tac (claset(), simpset() addsimps [r_coset_eq]));
qed "r_coset_subset_G";
Goal "[| h \\<in> H; H <= carrier G; x \\<in> carrier G|] ==> h ## x \\<in> H #> x";
by (auto_tac (claset(), simpset() addsimps [r_coset_eq]));
qed "rcosI";
Goal "[| H <= carrier G; x \\<in> carrier G |] ==> H #> x \\<in> {*H*}";
by (auto_tac (claset(), simpset() addsimps [setrcos_eq]));
qed "setrcosI";
Goal "[| x ## y = z; x \\<in> carrier G; y \\<in> carrier G; z\\<in>carrier G |] \
\ ==> (i x) ## z = y";
by (Clarify_tac 1);
by (asm_simp_tac (simpset() addsimps [binop_assoc RS sym]) 1);
qed "transpose_inv";
Goal "[| y \\<in> H #> x; x \\<in> carrier G; H <<= G |] ==> H #> x = H #> y";
by (auto_tac (claset(),
simpset() addsimps [r_coset_eq, binop_assoc RS sym,
right_cancellation_iff, subgroup_imp_subset RS subsetD,
subgroup_f_closed]));
by (res_inst_tac [("x","ha ## i h")] bexI 1);
by (auto_tac (claset(),
simpset() addsimps [binop_assoc, subgroup_imp_subset RS subsetD,
subgroup_inv_closed, subgroup_f_closed]));
qed "repr_independence";
Goal "[| x \\<in> carrier G; H <<= G |] ==> x \\<in> H #> x";
by (simp_tac (simpset() addsimps [r_coset_eq]) 1);
by (blast_tac (claset() addIs [e_ax1, subgroup_imp_subset RS subsetD,
subgroup_e_closed]) 1);
qed "rcos_self";
Goal "setinv H = INV`H";
by (simp_tac
(simpset() addsimps [image_def, setinv_def, set_inv_def, inv_def]) 1);
qed "setinv_eq_image_inv";
(*** normal subgroups ***)
Goal "(H <| G) = (H <<= G & (\\<forall>x \\<in> carrier G. H #> x = x <# H))";
by (afs [thm "lcos_def", thm "rcos_def", normal_def] 1);
qed "normal_iff";
Goal "H <| G ==> H <<= G";
by (afs [normal_def] 1);
qed "normal_imp_subgroup";
Goal "[| H <| G; x \\<in> carrier G |] ==> H #> x = x <# H";
by (afs [thm "lcos_def", thm "rcos_def", normal_def] 1);
qed "normal_imp_rcos_eq_lcos";
Goal "\\<lbrakk>H \\<lhd> G; x \\<in> (G .<cr>); h \\<in> H\\<rbrakk> \\<Longrightarrow> i x ## h ## x \\<in> H";
by (auto_tac (claset(),
simpset() addsimps [l_coset_eq, r_coset_eq, normal_iff]));
by (ball_tac 1);
by (dtac (equalityD1 RS subsetD) 1);
by (Blast_tac 1);
by (Clarify_tac 1);
by (etac subst 1);
by (asm_simp_tac
(simpset() addsimps [binop_assoc RS sym, subgroup_imp_subset RS subsetD]) 1);
qed "normal_inv_op_closed1";
Goal "\\<lbrakk>H \\<lhd> G; x \\<in> (G .<cr>); h \\<in> H\\<rbrakk> \\<Longrightarrow> x ## h ## i x \\<in> H";
by (dres_inst_tac [("x","i x")] normal_inv_op_closed1 1);
by Auto_tac;
qed "normal_inv_op_closed2";
Goal "[| M <= carrier G; g\\<in>carrier G; h\\<in>carrier G |] \
\ ==> g <# (h <# M) = (g ## h) <# M";
by (force_tac (claset(), simpset() addsimps [l_coset_eq, binop_assoc]) 1);
qed "lcos_mul_assoc";
Goal "M <= carrier G ==> e <# M = M";
by (force_tac (claset(), simpset() addsimps [l_coset_eq]) 1);
qed "lcos_mul_e";
Goal "[| H <= carrier G; x\\<in>carrier G |]\
\ ==> x <# H <= carrier G";
by (auto_tac (claset(), simpset() addsimps [l_coset_eq, subsetD]));
qed "lcosetGaH_subset_G";
Goal "[| y \\<in> x <# H; x \\<in> carrier G; H <<= G |] ==> x <# H = y <# H";
by (auto_tac (claset(),
simpset() addsimps [l_coset_eq, binop_assoc,
left_cancellation_iff, subgroup_imp_subset RS subsetD,
subgroup_f_closed]));
by (res_inst_tac [("x","i h ## ha")] bexI 1);
by (auto_tac (claset(),
simpset() addsimps [binop_assoc RS sym, subgroup_imp_subset RS subsetD,
subgroup_inv_closed, subgroup_f_closed]));
qed "l_repr_independence";
Goal "[| H1 <= carrier G; H2 <= carrier G |] ==> H1 <#> H2 <= carrier G";
by (auto_tac (claset(), simpset() addsimps [set_prod_eq, subsetD]));
qed "setprod_subset_G";
val set_prod_subset_G = export setprod_subset_G;
Goal "H <<= G ==> H <#> H = H";
by (auto_tac (claset(),
simpset() addsimps [set_prod_eq, Sigma_def,image_def]));
by (res_inst_tac [("x","x")] bexI 2);
by (res_inst_tac [("x","e")] bexI 2);
by (auto_tac (claset(),
simpset() addsimps [subgroup_f_closed, subgroup_e_closed, e_ax2,
subgroup_imp_subset RS subsetD]));
qed "subgroup_prod_id";
val Subgroup_prod_id = export subgroup_prod_id;
(* set of inverses of an r_coset *)
Goal "[| H <| G; x \\<in> carrier G |] ==> I(H #> x) = H #>(i x)";
by (ftac normal_imp_subgroup 1);
by (auto_tac (claset(),
simpset() addsimps [r_coset_eq, setinv_eq_image_inv, image_def]));
by (res_inst_tac [("x","i x ## i h ## x")] bexI 1);
by (asm_simp_tac (simpset() addsimps [binop_assoc, inv_prod,
subgroup_imp_subset RS subsetD]) 1);
by (res_inst_tac [("x","i(h ## i x)")] exI 2);
by (asm_simp_tac (simpset() addsimps [inv_inv, inv_prod,
subgroup_imp_subset RS subsetD]) 2);
by (res_inst_tac [("x","x ## i h ## i x")] bexI 2);
by (auto_tac (claset(),
simpset() addsimps [normal_inv_op_closed1, normal_inv_op_closed2,
binop_assoc, subgroup_imp_subset RS subsetD,
subgroup_inv_closed]));
qed "rcos_inv";
val r_coset_inv = export rcos_inv;
Goal "[| H <| G; H1\\<in>{*H*}; x \\<in> H1 |] ==> I(H1) = H #> (i x)";
by (afs [setrcos_eq] 1);
by (Clarify_tac 1);
by (subgoal_tac "x : carrier G" 1);
by (rtac subsetD 2);
by (assume_tac 3);
by (asm_full_simp_tac (simpset() addsimps [r_coset_subset_G,
subgroup_imp_subset,normal_imp_subgroup]) 2);
by (dtac repr_independence 1);
by (assume_tac 1);
by (etac normal_imp_subgroup 1);
by (asm_simp_tac (simpset() addsimps [rcos_inv]) 1);
qed "rcos_inv2";
val r_coset_inv2 = export rcos_inv2;
(* some rules for <#> with #> or <# *)
Goal "[| H1 <= carrier G; H2 <= carrier G; x \\<in> carrier G |]\
\ ==> H1 <#> (H2 #> x) = (H1 <#> H2) #> x";
by (auto_tac (claset(),
simpset() addsimps [rcos_def, r_coset_def,
setprod_def, set_prod_def, Sigma_def,image_def]));
by (auto_tac (claset() addSIs [bexI,exI],
simpset() addsimps [binop_assoc, subsetD]));
qed "setprod_rcos_assoc";
val set_prod_r_coset_assoc = export setprod_rcos_assoc;
Goal "[| H1 <= carrier G; H2 <= carrier G; x \\<in> carrier G |]\
\ ==> (H1 #> x) <#> H2 = H1 <#> (x <# H2)";
by (asm_simp_tac
(simpset() addsimps [rcos_def, r_coset_def, lcos_def, l_coset_def,
setprod_def, set_prod_def, Sigma_def,image_def]) 1);
by (force_tac (claset() addSIs [bexI,exI],
simpset() addsimps [binop_assoc, subsetD]) 1);
qed "rcos_prod_assoc_lcos";
val rcoset_prod_assoc_lcoset = export rcos_prod_assoc_lcos;
(* product of rcosets *)
(* To show H x H y = H x y. which is done by
H x H y =1= H (x H) y =2= H (H x) y =3= H H x y =4= H x y *)
Goal "[| H <| G; x \\<in> carrier G; y \\<in> carrier G |]\
\ ==> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y";
by (afs [setprod_rcos_assoc, normal_imp_subgroup RS subgroup_imp_subset, r_coset_subset_G,
lcosetGaH_subset_G, rcos_prod_assoc_lcos] 1);
qed "rcos_prod_step1";
Goal "[| H <| G; x \\<in> carrier G; y \\<in> carrier G |]\
\ ==> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y";
by (afs [normal_imp_rcos_eq_lcos] 1);
qed "rcos_prod_step2";
Goal "[| H <| G; x \\<in> carrier G; y \\<in> carrier G |]\
\ ==> (H <#> (H #> x)) #> y = H #> (x ## y)";
by (afs [setprod_rcos_assoc,normal_imp_subgroup RS subgroup_imp_subset,
r_coset_subset_G, coset_mul_assoc, setprod_subset_G,
normal_imp_subgroup RS subgroup_imp_subset,subgroup_prod_id,
normal_imp_subgroup] 1);
qed "rcos_prod_step3";
Goal "[| H <| G; x \\<in> carrier G; y \\<in> carrier G |]\
\ ==> (H #> x) <#> (H #> y) = H #> (x ## y)";
by (afs [rcos_prod_step1,rcos_prod_step2,rcos_prod_step3] 1);
qed "rcos_prod";
val rcoset_prod = export rcos_prod;
(* operations on cosets *)
Goal "[| H <| G; H1 \\<in> {*H*}; H2 \\<in> {*H*} |] ==> H1 <#> H2 \\<in> {*H*}";
by (auto_tac (claset(),
simpset() addsimps [normal_imp_subgroup RS subgroup_imp_subset,
rcos_prod, setrcos_eq]));
qed "setprod_closed";
Goal "[| H <| G; H1 \\<in> {*H*} |] ==> I(H1) \\<in> {*H*}";
by (auto_tac (claset(),
simpset() addsimps [normal_imp_subgroup RS subgroup_imp_subset,
rcos_inv, setrcos_eq]));
qed "setinv_closed";
Goal "H <<= G ==> H \\<in> {*H*}";
by (simp_tac (simpset() addsimps [setrcos_eq]) 1);
by (blast_tac (claset() delrules [equalityI]
addSIs [subgroup_e_closed, e_closed, coset_join2 RS sym]) 1);
qed "setrcos_unit_closed";
Goal "[|H <| G; M \\<in> {*H*}|] ==> I M <#> M = H";
by (asm_full_simp_tac (simpset() addsimps [setrcos_eq]) 1);
by (Clarify_tac 1);
by (asm_simp_tac
(simpset() addsimps [rcos_inv, rcos_prod, normal_imp_subgroup,
subgroup_imp_subset, coset_mul_e]) 1);
qed "setrcos_inv_prod_eq";
(*generalizes subgroup_prod_id*)
Goal "[|H <| G; M \\<in> {*H*}|] ==> H <#> M = M";
by (asm_full_simp_tac (simpset() addsimps [setrcos_eq]) 1);
by (Clarify_tac 1);
by (asm_simp_tac
(simpset() addsimps [normal_imp_subgroup, subgroup_imp_subset,
setprod_rcos_assoc, subgroup_prod_id]) 1);
qed "setrcos_prod_eq";
Goal "[|H <| G; M1 \\<in> {*H*}; M2 \\<in> {*H*}; M3 \\<in> {*H*}|] \
\ ==> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)";
by (asm_full_simp_tac (simpset() addsimps [setrcos_eq]) 1);
by (Clarify_tac 1);
by (asm_simp_tac
(simpset() addsimps [rcos_prod, normal_imp_subgroup,
subgroup_imp_subset, binop_assoc]) 1);
qed "setrcos_prod_assoc";
(**** back to Sylow again, i.e. direction Lagrange ****)
(* Theorems necessary for Lagrange *)
Goal "H <<= G ==> \\<Union> {*H*} = carrier G";
by (rtac equalityI 1);
by (force_tac (claset(),
simpset() addsimps [subgroup_imp_subset RS subsetD, setrcos_eq, r_coset_eq]) 1);
by (auto_tac (claset(),
simpset() addsimps [setrcos_eq, subgroup_imp_subset, rcos_self]));
qed "setrcos_part_G";
Goal "[| c \\<in> {*H*}; H <= carrier G; finite (carrier G) |] ==> finite c";
by (auto_tac (claset(), simpset() addsimps [setrcos_eq]));
by (asm_simp_tac (simpset() addsimps [r_coset_subset_G RS finite_subset]) 1);
qed "cosets_finite";
Goal "[| c \\<in> {*H*}; H <= carrier G; finite(carrier G) |] ==> card c = card H";
by (auto_tac (claset(), simpset() addsimps [setrcos_eq]));
by (res_inst_tac [("f", "%y. y ## i a"), ("g","%y. y ## a")] card_bij_eq 1);
by (afs [r_coset_subset_G RS finite_subset] 1);
by (blast_tac (claset() addIs [finite_subset]) 1);
(* injective maps *)
by (blast_tac (claset() addIs [restrictI, rcosI]) 3);
by (force_tac (claset(),
simpset() addsimps [inj_on_def, right_cancellation_iff, subsetD]) 3);
(*now for f*)
by (force_tac (claset(),
simpset() addsimps [binop_assoc, subsetD, r_coset_eq]) 1);
(* injective *)
by (rtac inj_onI 1);
by (subgoal_tac "x \\<in> carrier G & y \\<in> carrier G" 1);
by (blast_tac (claset() addIs [r_coset_subset_G RS subsetD]) 2);
by (rotate_tac ~1 1);
by (asm_full_simp_tac
(simpset() addsimps [right_cancellation_iff, subsetD]) 1);
qed "card_cosets_equal";
(** Two distinct right cosets are disjoint **)
Goal "[|H <<= G; a \\<in> (G .<cr>); b \\<in> (G .<cr>); ha ## a = h ## b; \
\ h \\<in> H; ha \\<in> H; hb \\<in> H|] \
\ ==> \\<exists>h\\<in>H. h ## b = hb ## a";
by (res_inst_tac [("x","hb ## ((i ha) ## h)")] bexI 1);
by (afs [subgroup_f_closed, subgroup_inv_closed] 2);
by (asm_simp_tac (simpset() addsimps [binop_assoc, left_cancellation_iff,
transpose_inv, subgroup_imp_subset RS subsetD]) 1);
qed "rcos_equation";
Goal "[|H <<= G; c1 \\<in> {*H*}; c2 \\<in> {*H*}; c1 \\<noteq> c2|] ==> c1 \\<inter> c2 = {}";
by (asm_full_simp_tac (simpset() addsimps [setrcos_eq, r_coset_eq]) 1);
by (blast_tac (claset() addIs [rcos_equation, sym]) 1);
qed "rcos_disjoint";
Goal "H <<= G ==> {*H*} <= Pow(carrier G)";
by (simp_tac (simpset() addsimps [setrcos_eq]) 1);
by (blast_tac (claset() addDs [r_coset_subset_G,subgroup_imp_subset]) 1);
qed "setrcos_subset_PowG";
Goal "[| finite(carrier G); H <<= G |]\
\ ==> card({*H*}) * card(H) = order(G)";
by (asm_simp_tac (simpset() addsimps [order_def, setrcos_part_G RS sym]) 1);
by (stac mult_commute 1);
by (rtac card_partition 1);
by (asm_full_simp_tac
(simpset() addsimps [setrcos_subset_PowG RS finite_subset]) 1);
by (asm_full_simp_tac (simpset() addsimps [setrcos_part_G]) 1);
by (asm_full_simp_tac
(simpset() addsimps [card_cosets_equal, subgroup_def]) 1);
by (asm_full_simp_tac (simpset() addsimps [rcos_disjoint, subgroup_def]) 1);
qed "lagrange";
val Lagrange = export lagrange;
Close_locale "coset";
Close_locale "group";