(* Title: HOL/GroupTheory/Group
ID: $Id$
Author: Florian Kammueller, with new proofs by L C Paulson
Copyright 1998-2001 University of Cambridge
Group theory using locales
*)
fun afs thms = (asm_full_simp_tac (simpset() addsimps thms));
(* Proof of group theory theorems necessary for Sylow's theorem *)
Open_locale "group";
val e_def = thm "e_def";
val binop_def = thm "binop_def";
val inv_def = thm "inv_def";
val Group_G = thm "Group_G";
val simp_G = simplify (simpset() addsimps [Group_def]) (Group_G);
Addsimps [simp_G, Group_G];
Goal "e \\<in> carrier G";
by (afs [e_def] 1);
qed "e_closed";
val unit_closed = export e_closed;
Addsimps [e_closed];
Goal "op ## \\<in> carrier G \\<rightarrow> carrier G \\<rightarrow> carrier G";
by (simp_tac (simpset() addsimps [binop_def]) 1);
qed "binop_funcset";
Goal "[| x \\<in> carrier G; y \\<in> carrier G |] ==> x ## y \\<in> carrier G";
by (afs [binop_funcset RS (funcset_mem RS funcset_mem)] 1);
qed "binop_closed";
val bin_op_closed = export binop_closed;
Addsimps [binop_closed];
Goal "INV \\<in> carrier G \\<rightarrow> carrier G";
by (simp_tac (simpset() addsimps [inv_def]) 1);
qed "inv_funcset";
Goal "x \\<in> carrier G ==> i(x) \\<in> carrier G";
by (afs [inv_funcset RS funcset_mem] 1);
qed "inv_closed";
val inverse_closed = export inv_closed;
Addsimps [inv_closed];
Goal "x \\<in> carrier G ==> e ## x = x";
by (afs [e_def, binop_def] 1);
qed "e_ax1";
Addsimps [e_ax1];
Goal "x \\<in> carrier G ==> i(x) ## x = e";
by (afs [binop_def, inv_def, e_def] 1);
qed "inv_ax2";
Addsimps [inv_ax2];
Goal "[| x \\<in> carrier G; y \\<in> carrier G; z \\<in> carrier G |] \
\ ==> (x ## y) ## z = x ## (y ## z)";
by (afs [binop_def] 1);
qed "binop_assoc";
Goal "[|f \\<in> A \\<rightarrow> A \\<rightarrow> A; i1 \\<in> A \\<rightarrow> A; e1 \\<in> A;\
\ \\<forall>x \\<in> A. (f (i1 x) x = e1); \\<forall>x \\<in> A. (f e1 x = x);\
\ \\<forall>x \\<in> A. \\<forall>y \\<in> A. \\<forall>z \\<in> A. (f (f x y) z = f (x) (f y z)) |] \
\ ==> (| carrier = A, bin_op = f, inverse = i1, unit = e1 |) \\<in> Group";
by (afs [Group_def] 1);
qed "groupI";
val GroupI = export groupI;
(*****)
(* Now the real derivations *)
Goal "[| x\\<in>carrier G ; y\\<in>carrier G; z\\<in>carrier G; x ## y = x ## z |] \
\ ==> y = z";
by (dres_inst_tac [("f","%z. i x ## z")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps [binop_assoc RS sym]) 1);
qed "left_cancellation";
Goal "[| x \\<in> carrier G; y \\<in> carrier G; z \\<in> carrier G |] \
\ ==> (x ## y = x ## z) = (y = z)";
by (blast_tac (claset() addIs [left_cancellation]) 1);
qed "left_cancellation_iff";
(* Now the other directions of basic lemmas; they need a left cancellation*)
Goal "x \\<in> carrier G ==> x ## e = x";
by (res_inst_tac [("x","i x")] left_cancellation 1);
by (auto_tac (claset(), simpset() addsimps [binop_assoc RS sym]));
qed "e_ax2";
Addsimps [e_ax2];
Goal "[| x \\<in> carrier G; x ## x = x |] ==> x = e";
by (res_inst_tac [("x","x")] left_cancellation 1);
by Auto_tac;
qed "idempotent_e";
Goal "x \\<in> carrier G ==> x ## i(x) = e";
by (rtac idempotent_e 1);
by (auto_tac (claset(), simpset() addsimps [binop_assoc RS sym]));
by (asm_simp_tac (simpset() addsimps [inst "x" "x" binop_assoc]) 1);
qed "inv_ax1";
Addsimps [inv_ax1];
Goal "[| x \\<in> carrier G; y \\<in> carrier G; x ## y = e |] ==> y = i(x)";
by (res_inst_tac [("x","x")] left_cancellation 1);
by Auto_tac;
qed "inv_unique";
Goal "x \\<in> carrier G ==> i(i(x)) = x";
by (res_inst_tac [("x","i x")] left_cancellation 1);
by Auto_tac;
qed "inv_inv";
Addsimps [inv_inv];
Goal "[| x \\<in> carrier G; y \\<in> carrier G |] ==> i(x ## y) = i(y) ## i(x)";
by (rtac (inv_unique RS sym) 1);
by (auto_tac (claset(), simpset() addsimps [binop_assoc RS sym]));
by (asm_simp_tac (simpset() addsimps [inst "x" "x" binop_assoc]) 1);
qed "inv_prod";
Goal "[| y ## x = z ## x; \
\ x \\<in> carrier G; y \\<in> carrier G; z \\<in> carrier G|] ==> y = z";
by (dres_inst_tac [("f","%z. z ## i x")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps [binop_assoc]) 1);
qed "right_cancellation";
Goal "[| x \\<in> carrier G; y \\<in> carrier G; z \\<in> carrier G |] \
\ ==> (y ## x = z ## x) = (y = z)";
by (blast_tac (claset() addIs [right_cancellation]) 1);
qed "right_cancellation_iff";
(* subgroup *)
Goal "[| H <= carrier G; H \\<noteq> {}; \\<forall>a \\<in> H. i(a)\\<in>H; \\<forall>a\\<in>H. \\<forall>b\\<in>H. a ## b\\<in>H|] \
\ ==> e \\<in> H";
by (Force_tac 1);
qed "e_in_H";
(* subgroupI: a characterization of subgroups *)
Goal "[| H <= carrier G; H \\<noteq> {}; \\<forall>a \\<in> H. i(a)\\<in>H;\
\ \\<forall>a\\<in>H. \\<forall>b\\<in>H. a ## b\\<in>H |] ==> H <<= G";
by (asm_full_simp_tac (simpset() addsimps [subgroup_def]) 1);
(* Fold the locale definitions: the top level definition of subgroup gives
the verbose form, which does not immediately match rules like inv_ax1 *)
by (rtac groupI 1);
by (ALLGOALS (asm_full_simp_tac
(simpset() addsimps [subsetD, restrictI, e_in_H, binop_assoc] @
(map symmetric [binop_def, inv_def, e_def]))));
qed "subgroupI";
val SubgroupI = export subgroupI;
Goal "H <<= G ==> \
\ (|carrier = H, bin_op = %x:H. %y:H. x ## y, \
\ inverse = %x:H. i(x), unit = e|)\\<in>Group";
by (afs [subgroup_def, binop_def, inv_def, e_def] 1);
qed "subgroupE2";
val SubgroupE2 = export subgroupE2;
Goal "H <<= G ==> H <= carrier G";
by (afs [subgroup_def, binop_def, inv_def, e_def] 1);
qed "subgroup_imp_subset";
Goal "[| H <<= G; x \\<in> H; y \\<in> H |] ==> x ## y \\<in> H";
by (dtac subgroupE2 1);
by (dtac bin_op_closed 1);
by (Asm_full_simp_tac 1);
by (thin_tac "x\\<in>H" 1);
by Auto_tac;
qed "subgroup_f_closed";
Goal "[| H <<= G; x \\<in> H |] ==> i x \\<in> H";
by (dtac (subgroupE2 RS inverse_closed) 1);
by Auto_tac;
qed "subgroup_inv_closed";
val Subgroup_inverse_closed = export subgroup_inv_closed;
Goal "H <<= G ==> e\\<in>H";
by (dtac (subgroupE2 RS unit_closed) 1);
by (Asm_full_simp_tac 1);
qed "subgroup_e_closed";
Goal "[| finite(carrier G); H <<= G |] ==> 0 < card(H)";
by (subgoal_tac "finite H" 1);
by (blast_tac (claset() addIs [finite_subset] addDs [subgroup_imp_subset]) 2);
by (rtac ccontr 1);
by (asm_full_simp_tac (simpset() addsimps [card_0_eq]) 1);
by (blast_tac (claset() addDs [subgroup_e_closed]) 1);
qed "SG_card1";
(* Abelian Groups *)
Goal "[|G' \\<in> AbelianGroup; x: carrier G'; y: carrier G'|] \
\ ==> (G'.<f>) x y = (G'.<f>) y x";
by (auto_tac (claset(), simpset() addsimps [AbelianGroup_def]));
qed "Group_commute";
Goal "AbelianGroup <= Group";
by (auto_tac (claset(), simpset() addsimps [AbelianGroup_def]));
qed "Abel_subset_Group";
val Abel_imp_Group = Abel_subset_Group RS subsetD;
Delsimps [simp_G, Group_G];
Close_locale "group";
Goal "G \\<in> Group ==> (| carrier = G .<cr>, bin_op = G .<f>, inverse = G .<inv>,\
\ unit = G .<e> |) \\<in> Group";
by (blast_tac
(claset() addIs [GroupI, export binop_funcset, export inv_funcset, export e_closed, export inv_ax2, export e_ax1, export binop_assoc]) 1);
qed "Group_Group";
Goal "G \\<in> AbelianGroup \
\ ==> (| carrier = G .<cr>, bin_op = G .<f>, inverse = G .<inv>,\
\ unit = G .<e> |) \\<in> AbelianGroup";
by (asm_full_simp_tac (simpset() addsimps [AbelianGroup_def]) 1);
by (rtac Group_Group 1);
by Auto_tac;
qed "Abel_Abel";