--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/GroupTheory/Coset.ML Tue Jul 03 15:28:24 2001 +0200
@@ -0,0 +1,394 @@
+(* 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";
+
+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";
+
+
+(**** 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";
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/GroupTheory/Coset.thy Tue Jul 03 15:28:24 2001 +0200
@@ -0,0 +1,58 @@
+(* 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
+*)
+
+Coset = Group + Exponent +
+
+constdefs
+ r_coset :: "['a grouptype,'a set, 'a] => 'a set"
+ "r_coset G H a == (% x. (bin_op G) x a) ` H"
+
+ l_coset :: "['a grouptype, 'a, 'a set] => 'a set"
+ "l_coset G a H == (% x. (bin_op G) a x) ` H"
+
+ set_r_cos :: "['a grouptype,'a set] => ('a set)set"
+ "set_r_cos G H == r_coset G H ` (carrier G)"
+
+ set_prod :: "['a grouptype,'a set,'a set] => 'a set"
+ "set_prod G H1 H2 == (%x. (bin_op G) (fst x)(snd x)) ` (H1 \\<times> H2)"
+ set_inv :: "['a grouptype,'a set] => 'a set"
+ "set_inv G H == (%x. (inverse G) x) ` H"
+
+ normal :: "('a grouptype * 'a set)set"
+ "normal == \\<Sigma>G \\<in> Group. {H. H <<= G &
+ (\\<forall>x \\<in> carrier G. r_coset G H x = l_coset G x H)}"
+
+
+syntax
+ "@NS" :: "['a set, 'a grouptype] => bool" ("_ <| _" [60,61]60)
+
+syntax (xsymbols)
+ "@NS" :: "['a set, 'a grouptype] => bool" ("_ \\<lhd> _" [60,61]60)
+
+translations
+ "N <| G" == "(G,N) \\<in> normal"
+
+locale coset = group +
+ fixes
+ rcos :: "['a set, 'a] => 'a set" ("_ #> _" [60,61]60)
+ lcos :: "['a, 'a set] => 'a set" ("_ <# _" [60,61]60)
+ setprod :: "['a set, 'a set] => 'a set" ("_ <#> _" [60,61]60)
+ setinv :: "'a set => 'a set" ("I (_)" [90]91)
+ setrcos :: "'a set => 'a set set" ("{*_*}" [90]91)
+ assumes
+
+ defines
+ rcos_def "H #> x == r_coset G H x"
+ lcos_def "x <# H == l_coset G x H"
+ setprod_def "H1 <#> H2 == set_prod G H1 H2"
+ setinv_def "I(H) == set_inv G H"
+ setrcos_def "{*H*} == set_r_cos G H"
+
+end
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/GroupTheory/DirProd.ML Tue Jul 03 15:28:24 2001 +0200
@@ -0,0 +1,94 @@
+(* Title: HOL/GroupTheory/DirProd
+ ID: $Id$
+ Author: Florian Kammueller, with new proofs by L C Paulson
+ Copyright 1998-2001 University of Cambridge
+
+Direct product of two groups
+*)
+
+Open_locale "prodgroup";
+
+val e'_def = thm "e'_def";
+val binop'_def = thm "binop'_def";
+val inv'_def = thm "inv'_def";
+val P_def = thm "P_def";
+val Group_G' = thm "Group_G'";
+
+
+Addsimps [P_def, Group_G', Group_G];
+
+Goal "(P.<cr>) = ((G.<cr>) \\<times> (G'.<cr>))";
+by (afs [ProdGroup_def] 1);
+qed "P_carrier";
+
+Goal "(P.<f>) = \
+\ (lam (x, x'): (P.<cr>). lam (y, y'): (P.<cr>). ( x ## y, x' ##' y'))";
+by (afs [ProdGroup_def, binop_def, binop'_def] 1);
+qed "P_bin_op";
+
+Goal "(P.<inv>) = (lam (x, y): (P.<cr>). (i x, i' y))";
+by (afs [ProdGroup_def, inv_def, inv'_def] 1);
+qed "P_inverse";
+
+Goal "(P.<e>) = (G.<e>, G'.<e>)";
+by (afs [ProdGroup_def, e_def, e'_def] 1);
+qed "P_unit";
+
+Goal "P = (| carrier = P.<cr>, \
+\ bin_op = (lam (x, x'): (P.<cr>). lam (y, y'): (P.<cr>).\
+\ (x ## y, x' ##' y')), \
+\ inverse = (lam (x, y): (P.<cr>). (i x, i' y)), \
+\ unit = P.<e> |)";
+by (afs [ProdGroup_def, P_carrier, P_bin_op, P_inverse, P_unit] 1);
+by (afs [binop_def, binop'_def, inv_def, inv'_def] 1);
+qed "P_defI";
+val P_DefI = export P_defI;
+
+Delsimps [P_def];
+
+Goal "(P.<f>) : (P.<cr>) \\<rightarrow> (P.<cr>) \\<rightarrow> (P.<cr>)";
+by (auto_tac (claset() addSIs [restrictI],
+ simpset() addsimps [P_bin_op, P_carrier, binop'_def,
+ bin_op_closed]));
+qed "bin_op_prod_closed";
+
+Goal "(P.<inv>) : (P.<cr>) \\<rightarrow> (P.<cr>)";
+by (auto_tac (claset() addSIs [restrictI],
+ simpset() addsimps [P_inverse, P_carrier, inv_closed,
+ inv'_def, inverse_closed]));
+qed "inverse_prod_closed";
+
+(* MAIN PROOF *)
+Goal "P : Group";
+by (stac P_defI 1);
+by (rtac GroupI 1);
+by (auto_tac (claset(),
+ simpset() addsimps ([P_carrier,P_bin_op,P_inverse,P_unit] RL [sym])));
+(* 1. *)
+by (rtac bin_op_prod_closed 1);
+(* 2. *)
+by (rtac inverse_prod_closed 1);
+(* 3. *)
+by (afs [P_carrier, P_unit, export e_closed] 1);
+(* 4. *)
+by (afs [P_carrier, P_bin_op, P_inverse, P_unit, Group_G' RS inverse_closed,
+ inv'_def, e_def, binop'_def, Group_G' RS (export inv_ax2)] 1);
+(* 5 *)
+by (afs [P_carrier,P_bin_op,P_unit, Group_G' RS unit_closed, export e_ax1,
+ binop_def, binop'_def] 1);
+(* 6 *)
+by (afs [P_carrier,P_bin_op, Group_G' RS bin_op_closed,
+ binop'_def, binop_assoc,export binop_assoc] 1);
+qed "prodgroup_is_group";
+val ProdGroup_is_Group = export prodgroup_is_group;
+
+Delsimps [Group_G', Group_G];
+
+Close_locale "prodgroup";
+Close_locale "r_group";
+Close_locale "group";
+
+Goal "ProdGroup : Group \\<rightarrow> Group \\<rightarrow> Group";
+by (REPEAT (ares_tac [funcsetI, ProdGroup_is_Group] 1));
+by (auto_tac (claset(), simpset() addsimps [ProdGroup_def]));
+qed "ProdGroup_arity";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/GroupTheory/DirProd.thy Tue Jul 03 15:28:24 2001 +0200
@@ -0,0 +1,47 @@
+(* Title: HOL/GroupTheory/DirProd
+ ID: $Id$
+ Author: Florian Kammueller, with new proofs by L C Paulson
+ Copyright 1998-2001 University of Cambridge
+
+Direct product of two groups
+*)
+
+DirProd = Coset +
+
+consts
+ ProdGroup :: "(['a grouptype, 'b grouptype] => ('a * 'b) grouptype)"
+
+defs
+ ProdGroup_def "ProdGroup == lam G: Group. lam G': Group.
+ (| carrier = ((G.<cr>) \\<times> (G'.<cr>)),
+ bin_op = (lam (x, x'): ((G.<cr>) \\<times> (G'.<cr>)).
+ lam (y, y'): ((G.<cr>) \\<times> (G'.<cr>)).
+ ((G.<f>) x y,(G'.<f>) x' y')),
+ inverse = (lam (x, y): ((G.<cr>) \\<times> (G'.<cr>)). ((G.<inv>) x, (G'.<inv>) y)),
+ unit = ((G.<e>),(G'.<e>)) |)"
+
+syntax
+ "@Pro" :: "['a grouptype, 'b grouptype] => ('a * 'b) grouptype" ("<|_,_|>" [60,61]60)
+
+translations
+ "<| G , G' |>" == "ProdGroup G G'"
+
+locale r_group = group +
+ fixes
+ G' :: "'b grouptype"
+ e' :: "'b"
+ binop' :: "'b => 'b => 'b" ("(_ ##' _)" [80,81]80 )
+ INV' :: "'b => 'b" ("i' (_)" [90]91)
+ assumes
+ Group_G' "G' : Group"
+ defines
+ e'_def "e' == unit G'"
+ binop'_def "x ##' y == bin_op G' x y"
+ inv'_def "i'(x) == inverse G' x"
+
+locale prodgroup = r_group +
+ fixes
+ P :: "('a * 'b) grouptype"
+ defines
+ P_def "P == <| G, G' |>"
+end
--- a/src/HOL/GroupTheory/Exponent.ML Mon Jul 02 21:53:11 2001 +0200
+++ b/src/HOL/GroupTheory/Exponent.ML Tue Jul 03 15:28:24 2001 +0200
@@ -4,20 +4,6 @@
Copyright 2001 University of Cambridge
*)
-(*??Two more for Divides.ML *)
-Goal "0<m ==> (m*n dvd m) = (n=1)";
-by Auto_tac;
-by (subgoal_tac "m*n dvd m*1" 1);
-by (dtac dvd_mult_cancel 1);
-by Auto_tac;
-qed "dvd_mult_cancel1";
-
-Goal "0<m ==> (n*m dvd m) = (n=1)";
-by (stac mult_commute 1);
-by (etac dvd_mult_cancel1 1);
-qed "dvd_mult_cancel2";
-
-
(*** prime theorems ***)
val prime_def = thm "prime_def";
@@ -126,24 +112,10 @@
qed "le_extend_mult";
-(* card_inj lemma: F. Kammueller, 4.9. 96
-
-The sequel contains a proof of the lemma "card_inj" used in the
-plus preparations. The provable form here differs from the
-one used in Group in that it contains the additional neccessary assumptions
-"finite A" and "finite B" *)
-
Goal "0 < card(S) ==> S \\<noteq> {}";
by (force_tac (claset(), simpset() addsimps [card_empty]) 1);
qed "card_nonempty";
-Goal "[| finite(A); finite(B); f \\<in> A -> B; inj_on f A |] ==> card A <= card B";
-bw funcset_def;
-by (rtac card_inj_on_le 1);
-by (assume_tac 4);
-by Auto_tac;
-qed "card_inj";
-
Goal "[| x \\<notin> F; \
\ \\<forall>c1\\<in>insert x F. \\<forall>c2 \\<in> insert x F. c1 \\<noteq> c2 --> c1 \\<inter> c2 = {}|]\
\ ==> x \\<inter> \\<Union> F = {}";
--- a/src/HOL/GroupTheory/Exponent.thy Mon Jul 02 21:53:11 2001 +0200
+++ b/src/HOL/GroupTheory/Exponent.thy Tue Jul 03 15:28:24 2001 +0200
@@ -1,18 +1,18 @@
(* Title: HOL/GroupTheory/Exponent
ID: $Id$
Author: Florian Kammueller, with new proofs by L C Paulson
- Copyright 2001 University of Cambridge
+ Copyright 1998-2001 University of Cambridge
+
+The combinatorial argument underlying the first Sylow theorem
+
+ exponent p s yields the greatest power of p that divides s.
*)
Exponent = Main + Primes +
constdefs
- (*??use the one in Fun.thy?*)
- funcset :: "['a set, 'b set] => ('a => 'b) set" ("_ -> _" [91,90]90)
- "A -> B == {f. \\<forall>x \\<in> A. f(x) \\<in> B}"
-
exponent :: "[nat, nat] => nat"
- "exponent p s == if p \\<in> prime then (GREATEST r. p ^ r dvd s) else 0"
+ "exponent p s == if p \\<in> prime then (GREATEST r. p^r dvd s) else 0"
end
--- a/src/HOL/GroupTheory/Group.ML Mon Jul 02 21:53:11 2001 +0200
+++ b/src/HOL/GroupTheory/Group.ML Tue Jul 03 15:28:24 2001 +0200
@@ -1,849 +1,207 @@
(* Title: HOL/GroupTheory/Group
ID: $Id$
Author: Florian Kammueller, with new proofs by L C Paulson
- Copyright 2001 University of Cambridge
-*)
-
-(* Proof of the first theorem of Sylow, building on Group.thy
-F. Kammueller 4.9.96.
-The proofs are not using any simplification tacticals or alike, they are very
-basic stepwise derivations. Thus, they are very long.
-The reason for doing it that way is that I wanted to learn about reasoning in
-HOL and Group.thy.*)
+ Copyright 1998-2001 University of Cambridge
-(* general *)
-val [p1] = goal (the_context()) "f\\<in>A -> B ==> \\<forall>x\\<in>A. f x\\<in>B";
-by (res_inst_tac [("a","f")] CollectD 1);
-by (fold_goals_tac [funcset_def]);
-by (rtac p1 1);
-qed "funcsetE";
-
-val [p1] = goal (the_context()) "\\<forall>x\\<in>A. f x\\<in>B ==> f\\<in>A -> B";
-by (rewtac funcset_def);
-by (rtac CollectI 1);
-by (rtac p1 1);
-qed "funcsetI";
+Group theory using locales
+*)
-val [p1] = goal (the_context()) "f\\<in>A -> B -> C ==> \\<forall>x\\<in>A. \\<forall> y\\<in>B. f x y\\<in>C";
-by (rtac ballI 1);
-by (res_inst_tac [("a","f x")] CollectD 1);
-by (res_inst_tac [("A","A")] bspec 1);
-by (assume_tac 2);
-by (res_inst_tac [("a","f")] CollectD 1);
-by (fold_goals_tac [funcset_def]);
-by (rtac p1 1);
-qed "funcsetE2";
-
-val [p1] = goal (the_context()) "\\<forall>x\\<in>A. \\<forall> y\\<in>B. f x y\\<in>C ==> f\\<in>A -> B -> C";
-by (rewtac funcset_def);
-by (rtac CollectI 1);
-by (rtac ballI 1);
-by (rtac CollectI 1);
-by (res_inst_tac [("A","A")] bspec 1);
-by (assume_tac 2);
-by (rtac p1 1);
-qed "funcsetI2";
+fun afs thms = (asm_full_simp_tac (simpset() addsimps thms));
-val [p1,p2,p3,p4] = goal (the_context())
- "[| finite A; finite B; \
-\ \\<exists>f \\<in> A -> B. inj_on f A; \\<exists>g \\<in> B -> A. inj_on g B |] ==> card(A) = card(B)";
-by (rtac le_anti_sym 1);
-by (rtac bexE 1);
-by (rtac p3 1);
-by (rtac (p2 RS (p1 RS card_inj)) 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (rtac bexE 1);
-by (rtac p4 1);
-by (rtac (p1 RS (p2 RS card_inj)) 1);
-by (assume_tac 1);
-by (assume_tac 1);
-qed "card_bij";
+(* Proof of group theory theorems necessary for Sylow's theorem *)
+Open_locale "group";
-Goal "order(G) = card(carrier G)";
-by (simp_tac (simpset() addsimps [order_def,carrier_def]) 1);
-qed "order_eq";
+val e_def = thm "e_def";
+val binop_def = thm "binop_def";
+val inv_def = thm "inv_def";
+val Group_G = thm "Group_G";
-(* Basic group properties *)
-goal (the_context()) "bin_op (H, bin_op G, invers G, unity G) = bin_op G";
-by (rewtac bin_op_def);
-by (rewrite_goals_tac [snd_conv RS eq_reflection]);
-by (rewrite_goals_tac [fst_conv RS eq_reflection]);
-by (rtac refl 1);
-qed "bin_op_conv";
-
-goal (the_context()) "carrier (H, bin_op G, invers G, unity G) = H";
-by (rewtac carrier_def);
-by (rewrite_goals_tac [fst_conv RS eq_reflection]);
-by (rtac refl 1);
-qed "carrier_conv";
+val simp_G = simplify (simpset() addsimps [Group_def]) (Group_G);
+Addsimps [simp_G, Group_G];
-goal (the_context()) "invers (H, bin_op G, invers G, unity G) = invers G";
-by (rewtac invers_def);
-by (rewrite_goals_tac [snd_conv RS eq_reflection]);
-by (rewrite_goals_tac [fst_conv RS eq_reflection]);
-by (rtac refl 1);
-qed "invers_conv";
+Goal "e \\<in> carrier G";
+by (afs [e_def] 1);
+qed "e_closed";
+val unit_closed = export e_closed;
+Addsimps [e_closed];
-goal (the_context()) "G\\<in>Group ==> (carrier G, bin_op G, invers G, unity G) = G";
-by (rewrite_goals_tac [carrier_def,invers_def,unity_def,bin_op_def]);
-by (rtac (surjective_pairing RS subst) 1);
-by (rtac (surjective_pairing RS subst) 1);
-by (rtac (surjective_pairing RS subst) 1);
-by (rtac refl 1);
-qed "G_conv";
+Goal "op ## \\<in> carrier G \\<rightarrow> carrier G \\<rightarrow> carrier G";
+by (simp_tac (simpset() addsimps [binop_def]) 1);
+qed "binop_funcset";
-(* Derivations of the Group definitions *)
-val [q1] = goal (the_context()) "G\\<in>Group ==> unity G\\<in>carrier G";
-by (rtac (q1 RSN(2,mp)) 1);
-by (res_inst_tac [("P","%x. x\\<in>Group --> unity G\\<in>carrier G")] subst 1);
-by (rtac (q1 RS G_conv) 1);
-by (rtac impI 1);
-by (rewtac Group_def);
-by (dtac CollectD_prod4 1);
-by (Fast_tac 1);
-qed "unity_closed";
+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];
-(* second part is identical to previous proof *)
-val [q1,q2,q3] = goal (the_context()) "[| G\\<in>Group; a\\<in>carrier G; b\\<in>carrier G |] ==> bin_op G a b\\<in>carrier G";
-by (res_inst_tac [("x","b")] bspec 1);
-by (rtac q3 2);
-by (res_inst_tac [("x","a")] bspec 1);
-by (rtac q2 2);
-by (rtac funcsetE2 1);
-by (rtac (q1 RSN(2,mp)) 1);
-by (res_inst_tac [("P","%x. x\\<in>Group --> bin_op G\\<in>carrier G -> carrier G -> carrier G")] subst 1);
-by (rtac (q1 RS G_conv) 1);
-by (rtac impI 1);
-by (rewtac Group_def);
-by (dtac CollectD_prod4 1);
-by (Fast_tac 1);
-qed "bin_op_closed";
+Goal "INV \\<in> carrier G \\<rightarrow> carrier G";
+by (simp_tac (simpset() addsimps [inv_def]) 1);
+qed "inv_funcset";
-val [q1,q2] = goal (the_context()) "[| G\\<in>Group; a\\<in>carrier G |] ==> invers G a\\<in>carrier G";
-by (res_inst_tac [("x","a")] bspec 1);
-by (rtac q2 2);
-by (rtac funcsetE 1);
-by (rtac (q1 RSN(2,mp)) 1);
-by (res_inst_tac [("P","%x. x\\<in>Group --> invers G\\<in>carrier G -> carrier G")] subst 1);
-by (rtac (q1 RS G_conv) 1);
-by (rtac impI 1);
-by (rewtac Group_def);
-by (dtac CollectD_prod4 1);
-by (Fast_tac 1);
-qed "invers_closed";
+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];
-val [q1,q2] = goal (the_context()) "[| G\\<in>Group; a\\<in>carrier G |] ==> bin_op G (unity G) a = a";
-by (rtac (q1 RSN(2,mp)) 1);
-by (res_inst_tac [("P","%x. x\\<in>Group --> bin_op G (unity G) a = a")] subst 1);
-by (rtac (q1 RS G_conv) 1);
-by (rtac impI 1);
-by (rewtac Group_def);
-by (dtac CollectD_prod4 1);
-by (dtac conjunct2 1);
-by (dtac conjunct2 1);
-by (dtac conjunct2 1);
-by (dtac bspec 1);
-by (rtac q2 1);
-by (dtac bspec 1);
-by (rtac q2 1);
-by (dtac bspec 1);
-by (rtac q2 1);
-by (Fast_tac 1);
-qed "unity_ax1";
+Goal "x \\<in> carrier G ==> e ## x = x";
+by (afs [e_def, binop_def] 1);
+qed "e_ax1";
+Addsimps [e_ax1];
-(* Apart from the instantiation in third line identical to last proof ! *)
-val [q1,q2] = goal (the_context()) "[| G\\<in>Group; a\\<in>carrier G |] ==> bin_op G (invers G a) a = unity G";
-by (rtac (q1 RSN(2,mp)) 1);
-by (res_inst_tac [("P","%x. x\\<in>Group --> bin_op G (invers G a) a = unity G")] subst 1);
-by (rtac (q1 RS G_conv) 1);
-by (rtac impI 1);
-by (rewtac Group_def);
-by (dtac CollectD_prod4 1);
-by (dtac conjunct2 1);
-by (dtac conjunct2 1);
-by (dtac conjunct2 1);
-by (dtac bspec 1);
-by (rtac q2 1);
-by (dtac bspec 1);
-by (rtac q2 1);
-by (dtac bspec 1);
-by (rtac q2 1);
-by (Fast_tac 1);
-qed "invers_ax2";
+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";
-(* again similar, different instantiation also in bspec's later *)
-val [q1,q2,q3,q4] = goal (the_context()) "[| G\\<in>Group; a\\<in>carrier G; b\\<in>carrier G; c\\<in>carrier G |] \
-\ ==> bin_op G (bin_op G a b) c = bin_op G a (bin_op G b c)";
-by (rtac (q1 RSN(2,mp)) 1);
-by (res_inst_tac [("P","%x. x\\<in>Group --> bin_op G (bin_op G a b) c = bin_op G a (bin_op G b c)")] subst 1);
-by (rtac (q1 RS G_conv) 1);
-by (rtac impI 1);
-by (rewtac Group_def);
-by (dtac CollectD_prod4 1);
-by (dtac conjunct2 1);
-by (dtac conjunct2 1);
-by (dtac conjunct2 1);
-by (dtac bspec 1);
-by (rtac q2 1);
-by (dtac bspec 1);
-by (rtac q3 1);
-by (dtac bspec 1);
-by (rtac q4 1);
-by (Fast_tac 1);
-qed "bin_op_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;
-val [p1,p2,p3,p4,p5] = goal (the_context()) "[| G\\<in>Group; x\\<in>carrier G; y\\<in>carrier G;\
-\ z\\<in>carrier G; bin_op G x y = bin_op G x z |] ==> y = z";
-by (res_inst_tac [("P","%r. r = z")] (unity_ax1 RS subst) 1);
-by (rtac p1 1);
-by (rtac p3 1);
-by (res_inst_tac [("P","%r. bin_op G r y = z")] subst 1);
-by (res_inst_tac [("a","x")] invers_ax2 1);
-by (rtac p1 1);
-by (rtac p2 1);
-by (stac bin_op_assoc 1);
-by (rtac p1 1);
-by (rtac invers_closed 1);
-by (rtac p1 1);
-by (rtac p2 1);
-by (rtac p2 1);
-by (rtac p3 1);
-by (stac p5 1);
-by (rtac (bin_op_assoc RS subst) 1);
-by (rtac p1 1);
-by (rtac invers_closed 1);
-by (rtac p1 1);
-by (rtac p2 1);
-by (rtac p2 1);
-by (rtac p4 1);
-by (stac invers_ax2 1);
-by (rtac p1 1);
-by (rtac p2 1);
-by (stac unity_ax1 1);
-by (rtac p1 1);
-by (rtac p4 1);
-by (rtac refl 1);
+(*****)
+(* 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";
-(* here all other directions of basic lemmas, they need a cancellation *)
-(* to be able to show the other directions of inverse and unity axiom we need:*)
-val [q1,q2] = goal (the_context()) "[| G\\<in>Group; a\\<in>carrier G |] ==> bin_op G a (unity G) = a";
-by (res_inst_tac [("x","invers G a")] left_cancellation 1);
-by (rtac q1 1);
-by (rtac (q2 RS (q1 RS invers_closed)) 1);
-by (rtac (q2 RS (q1 RS bin_op_closed)) 1);
-by (rtac (q1 RS unity_closed) 1);
-by (rtac q2 1);
-by (rtac (q1 RS bin_op_assoc RS subst) 1);
-by (rtac (q2 RS (q1 RS invers_closed)) 1);
-by (rtac q2 1);
-by (rtac (q1 RS unity_closed) 1);
-by (rtac (q1 RS invers_ax2 RS ssubst) 1);
-by (rtac q2 1);
-by (rtac (q1 RS unity_ax1 RS ssubst) 1);
-by (rtac (q1 RS unity_closed) 1);
-by (rtac refl 1);
-qed "unity_ax2";
-
-val [q1,q2,q3] = goal (the_context()) "[| G \\<in> Group; a\\<in>carrier G; bin_op G a a = a |] ==> a = unity G";
-by (rtac (q3 RSN(2,mp)) 1);
-by (res_inst_tac [("P","%x. bin_op G a a = x --> a = unity G")] subst 1);
-by (rtac (q2 RS (q1 RS unity_ax2)) 1);
-by (rtac impI 1);
-by (res_inst_tac [("x","a")] left_cancellation 1);
-by (assume_tac 5);
-by (rtac q1 1);
-by (rtac q2 1);
-by (rtac q2 1);
-by (rtac (q1 RS unity_closed) 1);
-qed "idempotent_e";
-
-val [q1,q2] = goal (the_context()) "[| G\\<in>Group; a\\<in>carrier G |] ==> bin_op G a (invers G a) = unity G";
-by (rtac (q1 RS idempotent_e) 1);
-by (rtac (q1 RS bin_op_closed) 1);
-by (rtac q2 1);
-by (rtac (q2 RS (q1 RS invers_closed)) 1);
-by (rtac (q1 RS bin_op_assoc RS ssubst) 1);
-by (rtac q2 1);
-by (rtac (q2 RS (q1 RS invers_closed)) 1);
-by (rtac (q2 RS (q1 RS bin_op_closed)) 1);
-by (rtac (q2 RS (q1 RS invers_closed)) 1);
-by (res_inst_tac [("t","bin_op G (invers G a) (bin_op G a (invers G a))")] subst 1);
-by (rtac (q1 RS bin_op_assoc) 1);
-by (rtac (q2 RS (q1 RS invers_closed)) 1);
-by (rtac q2 1);
-by (rtac (q2 RS (q1 RS invers_closed)) 1);
-by (rtac (q2 RS (q1 RS invers_ax2) RS ssubst) 1);
-by (rtac (q1 RS unity_ax1 RS ssubst) 1);
-by (rtac (q2 RS (q1 RS invers_closed)) 1);
-by (rtac refl 1);
-qed "invers_ax1";
-
-val [p1,p2,p3] = goal (the_context()) "[|(P==>Q); (Q==>R); P |] ==> R";
-by (rtac p2 1);
-by (rtac p1 1);
-by (rtac p3 1);
-qed "trans_meta";
-
-val [p1,p2,p3,p4] = goal (the_context()) "[| G\\<in>Group; M <= carrier G; g\\<in>carrier G; h\\<in>carrier G |] \
-\ ==> r_coset G (r_coset G M g) h = r_coset G M (bin_op G g h)";
-by (rewtac r_coset_def);
-by (rtac equalityI 1);
-by (rtac subsetI 1);
-by (rtac CollectI 1);
-by (rtac trans_meta 1);
-by (assume_tac 3);
-by (etac CollectD 1);
-by (rtac bexE 1);
-by (assume_tac 1);
-by (etac subst 1);
-by (rtac trans_meta 1);
-by (assume_tac 3);
-by (res_inst_tac [("a","xa")] CollectD 1);
-by (assume_tac 1);
-by (res_inst_tac [("A","M")] bexE 1);
-by (assume_tac 1);
-by (etac subst 1);
-by (res_inst_tac [("x","xb")] bexI 1);
-by (rtac (bin_op_assoc RS subst) 1);
-by (rtac refl 5);
-by (assume_tac 5);
-by (rtac p4 4);
-by (rtac p3 3);
-by (rtac p1 1);
-by (rtac subsetD 1);
-by (assume_tac 2);
-by (rtac p2 1);
-(* end of first <= obligation *)
-by (rtac subsetI 1);
-by (rtac CollectI 1);
-by (rtac trans_meta 1);
-by (assume_tac 3);
-by (etac CollectD 1);
-by (rtac bexE 1);
-by (assume_tac 1);
-by (etac subst 1);
-by (res_inst_tac [("x","bin_op G xa g")] bexI 1);
-by (rtac CollectI 2);
-by (res_inst_tac [("x","xa")] bexI 2);
-by (assume_tac 3);
-by (rtac refl 2);
-by (rtac (bin_op_assoc RS subst) 1);
-by (rtac p1 1);
-by (rtac subsetD 1);
-by (assume_tac 2);
-by (rtac p2 1);
-by (rtac p3 1);
-by (rtac p4 1);
-by (rtac refl 1);
-qed "coset_mul_assoc";
-
-val [q1,q2] = goal (the_context()) "[| G \\<in> Group; M <= carrier G |] ==> r_coset G M (unity G) = M";
-by (rewtac r_coset_def);
-by (rtac equalityI 1);
-by (rtac subsetI 1);
-by (dtac CollectD 1);
-by (etac bexE 1);
-by (etac subst 1);
-by (stac unity_ax2 1);
-by (rtac q1 1);
-by (assume_tac 2);
-by (etac (q2 RS subsetD) 1);
-(* one direction <= finished *)
-by (rtac subsetI 1);
-by (rtac CollectI 1);
-by (rtac bexI 1);
-by (assume_tac 2);
-by (rtac unity_ax2 1);
-by (rtac q1 1);
-by (etac (q2 RS subsetD) 1);
-qed "coset_mul_unity";
+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";
-val [q1,q2,q3,q4] = goal (the_context()) "[| G \\<in> Group; x\\<in>carrier G; H <<= G;\
-\ x\\<in>H |] ==> r_coset G H x = H";
-by (rewtac r_coset_def);
-by (rtac equalityI 1);
-by (rtac subsetI 1);
-by (dtac CollectD 1);
-by (etac bexE 1);
-by (etac subst 1);
-by (rtac (bin_op_conv RS subst) 1);
-by (rtac (carrier_conv RS subst) 1);
-val l1 = q3 RS (subgroup_def RS apply_def) RS conjunct2;
-by (rtac (l1 RS bin_op_closed) 1);
-by (stac carrier_conv 1);
-by (assume_tac 1);
-by (stac carrier_conv 1);
-by (rtac q4 1);
-(* first <= finished *)
-by (rtac subsetI 1);
-by (rtac CollectI 1);
-by (res_inst_tac [("x","bin_op G xa (invers G x)")] bexI 1);
-by (stac bin_op_assoc 1);
-by (rtac q1 1);
-by (rtac q2 3);
-val l3 = q3 RS (subgroup_def RS apply_def) RS conjunct1;
-by (rtac subsetD 1);
-by (rtac l3 1);
-by (assume_tac 1);
-by (rtac invers_closed 1);
-by (rtac q1 1);
-by (rtac q2 1);
-by (stac invers_ax2 1);
-by (rtac q1 1);
-by (rtac q2 1);
-by (rtac unity_ax2 1);
-by (rtac q1 1);
-by (rtac subsetD 1);
-by (rtac l3 1);
-by (assume_tac 1);
-by (rtac (bin_op_conv RS subst) 1);
-by (rtac (carrier_conv RS subst) 1);
-by (rtac (l1 RS bin_op_closed) 1);
-by (rewrite_goals_tac [carrier_conv RS eq_reflection]);
-by (assume_tac 1);
-by (rtac (invers_conv RS subst) 1);
-by (rtac (carrier_conv RS subst) 1);
-by (rtac (l1 RS invers_closed) 1);
-by (stac carrier_conv 1);
-by (rtac q4 1);
-qed "coset_join2";
+(* 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];
-val [q1,q2,q3,q4,q5] = goal (the_context()) "[| G \\<in> Group; x\\<in>carrier G; y\\<in>carrier G;\
-\ M <= carrier G; r_coset G M (bin_op G x (invers G y)) = M |] ==> r_coset G M x = r_coset G M y";
-by (res_inst_tac [("P","%z. r_coset G M x = r_coset G z y")] (q5 RS subst) 1);
-by (stac coset_mul_assoc 1);
-by (rtac q1 1);
-by (rtac q4 1);
-by (rtac bin_op_closed 1);
-by (rtac q1 1);
-by (rtac q2 1);
-by (rtac (q3 RS (q1 RS invers_closed)) 1);
-by (rtac q3 1);
-by (rtac (q1 RS bin_op_assoc RS ssubst) 1);
-by (rtac q2 1);
-by (rtac (q3 RS (q1 RS invers_closed)) 1);
-by (rtac q3 1);
-by (rtac (q1 RS invers_ax2 RS ssubst) 1);
-by (rtac q3 1);
-by (rtac (q1 RS unity_ax2 RS ssubst) 1);
-by (rtac q2 1);
-by (rtac refl 1);
-qed "coset_mul_invers1";
+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";
-val [q1,q2,q3,q4,q5] = goal (the_context()) "[| G \\<in> Group; x\\<in>carrier G; y\\<in>carrier G;\
-\ M <= carrier G; r_coset G M x = r_coset G M y|] ==> r_coset G M (bin_op G x (invers G y)) = M ";
-by (rtac (coset_mul_assoc RS subst) 1);
-by (rtac q1 1);
-by (rtac q4 1);
-by (rtac q2 1);
-by (rtac (q3 RS (q1 RS invers_closed)) 1);
-by (stac q5 1);
-by (rtac (q1 RS coset_mul_assoc RS ssubst) 1);
-by (rtac q4 1);
-by (rtac q3 1);
-by (rtac (q3 RS (q1 RS invers_closed)) 1);
-by (stac invers_ax1 1);
-by (rtac q1 1);
-by (rtac q3 1);
-by (rtac (q4 RS (q1 RS coset_mul_unity)) 1);
-qed "coset_mul_invers2";
-
+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];
-val [q1,q2] = goal (the_context()) "[|G\\<in>Group; H <<= G|] ==> unity G\\<in>H";
-by (rtac (q2 RSN(2,mp)) 1);
-by (rtac impI 1);
-by (dtac (subgroup_def RS apply_def RS conjunct2) 1);
-by (rewtac Group_def);
-by (dtac CollectD_prod4 1);
-by (Fast_tac 1);
-qed "SG_unity";
-
+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";
-val [q1,q2,q3,q4] = goal (the_context()) "[| G \\<in> Group; x\\<in>carrier G; H <<= G;\
-\ r_coset G H x = H |] ==> x\\<in>H";
-by (rtac (q4 RS subst) 1);
-by (rewtac r_coset_def);
-by (rtac CollectI 1);
-by (res_inst_tac [("x", "unity G")] bexI 1);
-by (rtac unity_ax1 1);
-by (rtac q1 1);
-by (rtac q2 1);
-by (rtac SG_unity 1);
-by (rtac q1 1);
-by (rtac q3 1);
-qed "coset_join1";
-
-
-val [q1,q2,q3] = goal (the_context()) "[| G \\<in> Group; finite(carrier G); H <<= G |] ==> 0 < card(H)";
-by (rtac zero_less_card_empty 1);
-by (rtac ExEl_NotEmpty 2);
-by (res_inst_tac [("x","unity G")] exI 2);
-by (rtac finite_subset 1);
-by (rtac (q3 RS (subgroup_def RS apply_def) RS conjunct1) 1);
-by (rtac q2 1);
-by (rtac SG_unity 1);
-by (rtac q1 1);
-by (rtac q3 1);
-qed "SG_card1";
-
+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];
-(* subgroupI: a characterization of subgroups *)
-val [p1,p2,p3,p4,p5] = goal (the_context()) "[|G\\<in>Group; H <= carrier G; H \\<noteq> {}; \\<forall> a \\<in> H. invers G a\\<in>H;\
-\ \\<forall> a\\<in>H. \\<forall> b\\<in>H. bin_op G a b\\<in>H|] ==> H <<= G";
-by (rewtac subgroup_def);
-by (rtac conjI 1);
-by (rtac p2 1);
-by (rewtac Group_def);
-by (rtac CollectI_prod4 1);
-by (rtac conjI 1);
-by (rtac conjI 2);
-by (rtac conjI 3);
-by (rtac funcsetI2 1);
-by (rtac p5 1);
-by (rtac funcsetI 1);
-by (rtac p4 1);
-by (rtac exE 1);
-by (rtac (p3 RS NotEmpty_ExEl) 1);
-by (rtac (invers_ax1 RS subst) 1);
-by (etac (p2 RS subsetD) 2);
-by (rtac p1 1);
-by (rtac (p5 RS bspec RS bspec) 1);
-by (assume_tac 1);
-by (etac (p4 RS bspec) 1);
-by (REPEAT (rtac ballI 1));
-by (rtac conjI 1);
-by (rtac conjI 2);
-by (rtac (p1 RS bin_op_assoc) 3);
-by (REPEAT (etac (p2 RS subsetD) 3));
-by (rtac (p1 RS unity_ax1) 2);
-by (etac (p2 RS subsetD) 2);
-by (rtac (p1 RS invers_ax2) 1);
-by (etac (p2 RS subsetD) 1);
-qed "subgroupI";
+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";
-
-val [p1,p2,p3,p4,p5] = goal (the_context()) "[| G\\<in>Group; x\\<in>carrier G; y\\<in>carrier G;\
-\ z\\<in>carrier G; bin_op G y x = bin_op G z x|] ==> y = z";
-by (res_inst_tac [("P","%r. r = z")] (unity_ax2 RS subst) 1);
-by (rtac p1 1);
-by (rtac p3 1);
-by (res_inst_tac [("P","%r. bin_op G y r = z")] subst 1);
-by (res_inst_tac [("a","x")] invers_ax1 1);
-by (rtac p1 1);
-by (rtac p2 1);
-by (rtac (bin_op_assoc RS subst) 1);
-by (rtac p1 1);
-by (rtac p3 1);
-by (rtac p2 1);
-by (rtac invers_closed 1);
-by (rtac p1 1);
-by (rtac p2 1);
-by (stac p5 1);
-by (stac bin_op_assoc 1);
-by (rtac p1 1);
-by (rtac p4 1);
-by (rtac p2 1);
-by (rtac invers_closed 1);
-by (rtac p1 1);
-by (rtac p2 1);
-by (stac invers_ax1 1);
-by (rtac p1 1);
-by (rtac p2 1);
-by (stac unity_ax2 1);
-by (rtac p1 1);
-by (rtac p4 1);
-by (rtac refl 1);
+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";
-
-(* further general theorems necessary for Lagrange *)
-val [p1,p2] = goal (the_context()) "[| G \\<in> Group; H <<= G|]\
-\ ==> \\<Union> (set_r_cos G H) = carrier G";
-by (rtac equalityI 1);
-by (rtac subsetI 1);
-by (etac UnionE 1);
-by (SELECT_GOAL (rewtac set_r_cos_def) 1);
-by (dtac CollectD 1);
-by (etac bexE 1);
-by (SELECT_GOAL (rewtac r_coset_def) 1);
-by (rtac subsetD 1);
-by (assume_tac 2);
-by (etac ssubst 1);
-by (rtac subsetI 1);
-by (dtac CollectD 1);
-by (etac bexE 1);
-by (etac subst 1);
-by (rtac (p1 RS bin_op_closed) 1);
-by (assume_tac 2);
-by (rtac subsetD 1);
-by (assume_tac 2);
-by (rtac (p2 RS (subgroup_def RS apply_def) RS conjunct1) 1);
-by (rtac subsetI 1);
-by (res_inst_tac [("X","r_coset G H x")] UnionI 1);
-by (rewtac set_r_cos_def);
-by (rtac CollectI 1);
-by (rtac bexI 1);
-by (assume_tac 2);
-by (rtac refl 1);
-by (rewtac r_coset_def);
-by (rtac CollectI 1);
-by (rtac bexI 1);
-by (etac (p1 RS unity_ax1) 1);
-by (rtac (p2 RS (p1 RS SG_unity)) 1);
-qed "set_r_cos_part_G";
+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";
-val [p1,p2,p3] = goal (the_context()) "[| G \\<in> Group; H <= carrier G; a\\<in>carrier G |]\
-\ ==> r_coset G H a <= carrier G";
-by (rtac subsetI 1);
-by (rewtac r_coset_def);
-by (dtac CollectD 1);
-by (etac bexE 1);
-by (etac subst 1);
-by (rtac (p1 RS bin_op_closed) 1);
-by (etac (p2 RS subsetD) 1);
-by (rtac p3 1);
-qed "rcosetGHa_subset_G";
+(* 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";
-val [p1,p2,p3] = goal (the_context()) "[|G\\<in>Group; H <= carrier G; finite(carrier G) |]\
-\ ==> \\<forall> c \\<in> set_r_cos G H. card c = card H";
-by (rtac ballI 1);
-by (rewtac set_r_cos_def);
-by (dtac CollectD 1);
-by (etac bexE 1);
-by (etac ssubst 1);
-by (rtac card_bij 1); (*use card_bij_eq??*)
-by (rtac finite_subset 1);
-by (rtac p3 2);
-by (etac (p2 RS (p1 RS rcosetGHa_subset_G)) 1);
-by (rtac (p3 RS (p2 RS finite_subset)) 1);
-(* injective maps *)
-by (res_inst_tac [("x","%y. bin_op G y (invers G a)")] bexI 1);
-by (SELECT_GOAL (rewtac funcset_def) 2);
-by (rtac CollectI 2);
-by (rtac ballI 2);
-by (SELECT_GOAL (rewtac r_coset_def) 2);
-by (dtac CollectD 2);
-by (etac bexE 2);
-by (etac subst 2);
-by (rtac (p1 RS bin_op_assoc RS ssubst) 2);
-by (etac (p2 RS subsetD) 2);
-by (assume_tac 2);
-by (etac (p1 RS invers_closed) 2);
-by (etac (p1 RS invers_ax1 RS ssubst) 2);
-by (rtac (p1 RS unity_ax2 RS ssubst) 2);
-by (assume_tac 3);
-by (etac (p2 RS subsetD) 2);
-by (rtac inj_onI 1);
-by (rtac (p1 RS right_cancellation) 1);
-by (rtac (p1 RS invers_closed) 1);
-by (assume_tac 1);
-by (rtac (rcosetGHa_subset_G RS subsetD) 1);
-by (rtac p1 1);
-by (rtac p2 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (rtac (rcosetGHa_subset_G RS subsetD) 1);
-by (rtac p1 1);
-by (rtac p2 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (assume_tac 1);
-(* f finished *)
-by (res_inst_tac [("x","%y. bin_op G y a")] bexI 1);
-by (SELECT_GOAL (rewtac funcset_def) 2);
-by (rtac CollectI 2);
-by (rtac ballI 2);
-by (SELECT_GOAL (rewtac r_coset_def) 2);
-by (rtac CollectI 2);
-by (rtac bexI 2);
-by (rtac refl 2);
-by (assume_tac 2);
-by (rtac inj_onI 1);
-by (rtac (p1 RS right_cancellation) 1);
-by (assume_tac 1);
-by (etac (p2 RS subsetD) 1);
-by (etac (p2 RS subsetD) 1);
-by (assume_tac 1);
-qed "card_cosets_equal";
+(* 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;
-
-val prems = goal (the_context()) "[| G \\<in> Group; x \\<in> carrier G; y \\<in> carrier G;\
-\ z\\<in>carrier G; bin_op G x y = z|] ==> y = bin_op G (invers G x) z";
-by (res_inst_tac [("x","x")] left_cancellation 1);
-by (REPEAT (ares_tac prems 1));
-by (rtac bin_op_closed 1);
-by (rtac invers_closed 2);
-by (REPEAT (ares_tac prems 1));
-by (rtac (bin_op_assoc RS subst) 1);
-by (rtac invers_closed 3);
-by (REPEAT (ares_tac prems 1));
-by (stac invers_ax1 1);
-by (stac unity_ax1 3);
-by (REPEAT (ares_tac prems 1));
-qed "transpose_invers";
+Goal "H <<= G ==> \
+\ (|carrier = H, bin_op = lam x:H. lam y:H. x ## y, \
+\ inverse = lam 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;
-val [p1,p2,p3,p4] = goal (the_context()) "[| G \\<in> Group; H <<= G; h1 \\<in> H; h2 \\<in> H|]\
-\ ==> bin_op G h1 h2\\<in>H";
-by (rtac (bin_op_conv RS subst) 1);
-val l1 = (p2 RS (subgroup_def RS apply_def) RS conjunct2);
-by (rtac (carrier_conv RS subst) 1);
-by (rtac (l1 RS bin_op_closed) 1);
-by (rewrite_goals_tac [carrier_conv RS eq_reflection]);
-by (rtac p3 1);
-by (rtac p4 1);
-qed "SG_bin_op_closed";
-
-
-val [p1,p2,p3] = goal (the_context()) "[| G \\<in> Group; H <<= G; h1 \\<in> H|]\
-\ ==> invers G h1\\<in>H";
-by (rtac (invers_conv RS subst) 1);
-by (rtac (carrier_conv RS subst) 1);
-val l1 = (p2 RS (subgroup_def RS apply_def) RS conjunct2);
-by (rtac (l1 RS invers_closed) 1);
-by (stac carrier_conv 1);
-by (rtac p3 1);
-qed "SG_invers_closed";
-
-val [p1] = goal (the_context()) "x = y ==> bin_op G z x = bin_op G z y";
-by (res_inst_tac [("t","y")] subst 1);
-by (rtac refl 2);
-by (rtac p1 1);
-qed "left_extend";
+Goal "H <<= G ==> H <= carrier G";
+by (afs [subgroup_def, binop_def, inv_def, e_def] 1);
+qed "subgroup_imp_subset";
-val [p1,p2] = goal (the_context()) "[| G \\<in> Group; H <<= G |]\
-\ ==> \\<forall> c1 \\<in> set_r_cos G H. \\<forall> c2 \\<in> set_r_cos G H. c1 \\<noteq> c2 --> c1 \\<inter> c2 = {}";
-val l1 = (p2 RS (subgroup_def RS apply_def) RS conjunct1);
-val l2 = l1 RS (p1 RS rcosetGHa_subset_G) RS subsetD;
-by (rtac ballI 1);
-by (rtac ballI 1);
-by (rtac impI 1);
-by (rtac notnotD 1);
-by (etac contrapos_nn 1);
-by (dtac NotEmpty_ExEl 1);
-by (etac exE 1);
-by (ftac IntD1 1);
-by (dtac IntD2 1);
-by (rewtac set_r_cos_def);
-by (dtac CollectD 1);
-by (dtac CollectD 1);
-by (etac bexE 1);
-by (etac bexE 1);
-by (hyp_subst_tac 1);
-by (hyp_subst_tac 1);
-by (rewtac r_coset_def);
-(* Level 17 *)
-by (rtac equalityI 1);
-by (rtac subsetI 1);
-by (rtac subsetI 2);
-by (rtac CollectI 1);
-by (rtac CollectI 2);
-by (dtac CollectD 1);
-by (dtac CollectD 2);
-by (ftac CollectD 1);
-by (ftac CollectD 2);
-by (dres_inst_tac [("a","xa")] CollectD 1);
-by (dres_inst_tac [("a","xa")] CollectD 2);
-by (fold_goals_tac [r_coset_def]);
-by (REPEAT (etac bexE 1));
-by (REPEAT (etac bexE 2));
-(* first solve 1 *)
-by (res_inst_tac [("x","bin_op G hb (bin_op G (invers G h) ha)")] bexI 1);
-by (stac bin_op_assoc 1);
-val G_closed_rules = [(p1 RS invers_closed),(p1 RS bin_op_closed),(p2 RS (p1 RS SG_invers_closed))
- ,(p2 RS (p1 RS SG_bin_op_closed)),(l1 RS subsetD)];
-by (rtac p1 1);
-by (REPEAT (ares_tac G_closed_rules 1));
-by (REPEAT (ares_tac G_closed_rules 2));
-by (eres_inst_tac [("t","xa")] subst 1);
-by (rtac left_extend 1);
-by (stac bin_op_assoc 1);
-by (rtac p1 1);
-by (REPEAT (ares_tac G_closed_rules 1));
-by (eres_inst_tac [("t","bin_op G ha aa")] ssubst 1);
-by (rtac (p1 RS transpose_invers RS ssubst) 1);
-by (rtac refl 5);
-by (rtac l2 3);
-by (assume_tac 4);
-by (REPEAT (ares_tac G_closed_rules 1));
-(* second thing, level 47 *)
-by (res_inst_tac [("x","bin_op G hb (bin_op G (invers G ha) h)")] bexI 1);
-by (REPEAT (ares_tac G_closed_rules 2));
-by (stac bin_op_assoc 1);
-by (rtac p1 1);
-by (REPEAT (ares_tac G_closed_rules 1));
-by (eres_inst_tac [("t","xa")] subst 1);
-by (rtac left_extend 1);
-by (stac bin_op_assoc 1);
-by (rtac p1 1);
-by (REPEAT (ares_tac G_closed_rules 1));
-by (etac ssubst 1);
-by (rtac (p1 RS transpose_invers RS ssubst) 1);
-by (rtac refl 5);
-by (rtac l2 3);
-by (assume_tac 4);
-by (REPEAT (ares_tac G_closed_rules 1));
-qed "r_coset_disjunct";
+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";
-
-val [p1,p2] = goal (the_context()) "[| G \\<in> Group; H <<= G |]\
-\ ==> set_r_cos G H <= Pow( carrier G)";
-by (rewtac set_r_cos_def);
-by (rtac subsetI 1);
-by (dtac CollectD 1);
-by (etac bexE 1);
-by (etac ssubst 1);
-by (rtac PowI 1);
-by (rtac subsetI 1);
-by (rewtac r_coset_def);
-by (dtac CollectD 1);
-by (etac bexE 1);
-by (etac subst 1);
-by (rtac bin_op_closed 1);
-by (rtac p1 1);
-by (assume_tac 2);
-by (etac (p2 RS (subgroup_def RS apply_def) RS conjunct1 RS subsetD) 1);
-qed "set_r_cos_subset_PowG";
+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";
-val [p1,p2,p3] = goal (the_context()) "[| G \\<in> Group; finite(carrier G); H <<= G |]\
-\ ==> card(set_r_cos G H) * card(H) = order(G)";
-by (simp_tac (simpset() addsimps [order_eq]) 1);
-by (rtac (p3 RS (p1 RS set_r_cos_part_G) RS subst) 1);
-by (rtac (mult_commute RS subst) 1);
-by (rtac card_partition 1);
-by (rtac finite_subset 1);
-by (rtac (p3 RS (p1 RS set_r_cos_subset_PowG)) 1);
-by (simp_tac (simpset() addsimps [finite_Pow_iff]) 1);
-by (rtac p2 1);
-by (rtac (p3 RS (p1 RS set_r_cos_part_G) RS ssubst) 1);
-by (rtac p2 1);
-val l1 = (p3 RS (subgroup_def RS apply_def) RS conjunct1);
-by (rtac (l1 RS (p1 RS card_cosets_equal)) 1);
-by (rtac p2 1);
-by (rtac (p3 RS (p1 RS r_coset_disjunct)) 1);
-qed "Lagrange"; (*original version: closer to locales??*)
+(* 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";
- (*version using "Goal" but no locales...
- Goal "[| G \\<in> Group; finite(carrier G); H <<= G |] \
- \ ==> card(set_r_cos G H) * card(H) = order(G)";
- by (asm_simp_tac (simpset() addsimps [order_eq, set_r_cos_part_G RS sym]) 1);
- by (stac mult_commute 1);
- by (rtac card_partition 1);
- by (rtac finite_subset 1);
- by (rtac set_r_cos_subset_PowG 1);
- by (assume_tac 1); by (assume_tac 1);
- by (simp_tac (simpset() addsimps [finite_Pow_iff]) 1);
- by (asm_full_simp_tac (simpset() addsimps [set_r_cos_part_G]) 1);
- by (rtac card_cosets_equal 1);
- by (rtac r_coset_disjunct 4);
- by Auto_tac;
- by (asm_full_simp_tac (simpset() addsimps [subgroup_def]) 1);
- by (blast_tac (claset() addIs []) 1);
- qed "Lagrange";
- *)
+Goal "AbelianGroup <= Group";
+by (auto_tac (claset(), simpset() addsimps [AbelianGroup_def]));
+qed "Abel_subset_Group";
+
+val Abel_imp_Group = Abel_subset_Group RS subsetD;
+
+Close_locale "group";
--- a/src/HOL/GroupTheory/Group.thy Mon Jul 02 21:53:11 2001 +0200
+++ b/src/HOL/GroupTheory/Group.thy Tue Jul 03 15:28:24 2001 +0200
@@ -1,60 +1,85 @@
(* Title: HOL/GroupTheory/Group
ID: $Id$
Author: Florian Kammueller, with new proofs by L C Paulson
- Copyright 2001 University of Cambridge
+ Copyright 1998-2001 University of Cambridge
+
+Group theory using locales
*)
-(* Theory of Groups, for Sylow's theorem. F. Kammueller, 11.10.96
-Step 1: Use two separate .thy files for groups and Sylow's thm, respectively:
+Group = Main +
+
+ (*Giving funcset the nice arrow syntax \\<rightarrow> *)
+syntax (symbols)
+ "op funcset" :: "['a set, 'b set] => ('a => 'b) set" (infixr "\\<rightarrow>" 60)
+
+
+record 'a semigrouptype =
+ carrier :: "'a set"
+ bin_op :: "['a, 'a] => 'a"
+
-Besides the formalization of groups as polymorphic sets of quadruples this
-theory file contains a bunch of declarations and axioms of number theory
-because it is meant to be the basis for a proof experiment of the theorem of
-Sylow. This theorem uses various kinds of theoretical domains. To improve the
-syntactical form I have deleted here in contrast to the first almost complete
-version of the proof (8exp/Group.* or presently results/AllgGroup/Group.* )
-all definitions which are specific for Sylow's theorem. They are now contained
-in the file Sylow.thy.
-*)
+record 'a grouptype = 'a semigrouptype +
+ inverse :: "'a => 'a"
+ unit :: "'a"
+(* This should be obsolete, if records will allow the promised syntax *)
+syntax
+ "@carrier" :: "'a semigrouptype => 'a set" ("_ .<cr>" [10] 10)
+ "@bin_op" :: "'a semigrouptype => (['a, 'a] => 'a)" ("_ .<f>" [10] 10)
+ "@inverse" :: "'a grouptype => ('a => 'a)" ("_ .<inv>" [10] 10)
+ "@unit" :: "'a grouptype => 'a" ("_ .<e>" [10] 10)
-Group = Exponent +
+translations
+ "G.<cr>" => "carrier G"
+ "G.<f>" => "bin_op G"
+ "G.<inv>" => "inverse G"
+ "G.<e>" => "unit G"
+
+constdefs
+ Semigroup :: "('a semigrouptype)set"
+ "Semigroup == {G. (bin_op G): carrier G \\<rightarrow> carrier G \\<rightarrow> carrier G &
+ (! x: carrier G. ! y: carrier G. !z: carrier G.
+ (bin_op G (bin_op G x y) z = bin_op G (x) (bin_op G y z)))}"
constdefs
+ Group :: "('a grouptype)set"
+ "Group == {G. (bin_op G): carrier G \\<rightarrow> carrier G \\<rightarrow> carrier G & inverse G : carrier G \\<rightarrow> carrier G
+ & unit G : carrier G &
+ (! x: carrier G. ! y: carrier G. !z: carrier G.
+ (bin_op G (inverse G x) x = unit G)
+ & (bin_op G (unit G) x = x)
+ & (bin_op G (bin_op G x y) z = bin_op G (x) (bin_op G y z)))}"
- carrier :: "('a set * (['a, 'a] => 'a) * ('a => 'a) * 'a) => 'a set"
- "carrier(G) == fst(G)"
-
- bin_op :: "('a set * (['a, 'a] => 'a) * ('a => 'a) * 'a) => (['a, 'a] => 'a)"
- "bin_op(G) == fst(snd(G))"
+ order :: "'a grouptype => nat" "order(G) == card(carrier G)"
- invers :: "('a set * (['a, 'a] => 'a) * ('a => 'a) * 'a) => ('a => 'a)"
-"invers(G) == fst(snd(snd(G)))"
-
- unity :: "('a set * (['a, 'a] => 'a) * ('a => 'a) * 'a) => 'a"
- "unity(G) == snd(snd(snd(G)))"
-
- order :: "('a set * (['a, 'a] => 'a) * ('a => 'a) * 'a) => nat"
- "order(G) == card(fst(G))"
+ AbelianGroup :: "('a grouptype) set"
+ "AbelianGroup == {G. G : Group &
+ (! x:(G.<cr>). ! y:(G.<cr>). ((G.<f>) x y = (G.<f>) y x))}"
+consts
+ subgroup :: "('a grouptype * 'a set)set"
- r_coset :: "[('a set * (['a, 'a] => 'a) * ('a => 'a) * 'a), 'a set, 'a] => 'a set"
- "r_coset G H a == {b . ? h : H. bin_op G h a = b}"
-
- set_r_cos :: "[('a set * (['a, 'a] => 'a) * ('a => 'a) * 'a), 'a set] => 'a set set"
+defs
+ subgroup_def "subgroup == SIGMA G: Group. {H. H <= carrier G &
+ ((| carrier = H, bin_op = lam x: H. lam y: H. (bin_op G) x y,
+ inverse = lam x: H. (inverse G) x, unit = unit G |) : Group)}"
- "set_r_cos G H == {C . ? a : carrier G. C = r_coset G H a}"
+syntax
+ "@SG" :: "['a set, 'a grouptype] => bool" ("_ <<= _" [51,50]50)
- subgroup :: "['a set,('a set * (['a, 'a] => 'a) * ('a => 'a) * 'a)] => bool"
- ("_ <<= _" [51,50]50)
+translations
+ "H <<= G" == "(G,H) : subgroup"
- "H <<= G == H <= carrier(G) & (H,bin_op(G),invers(G),unity(G)) : Group"
-
- Group :: "'a set"
-
- "Group == {(G,f,inv,e). f : G -> G -> G & inv : G -> G & e : G &\
-\ (! x: G. ! y: G. !z: G.\
-\ (f (inv x) x = e) & (f e x = x) &
- (f (f x y) z = f (x) (f y z)))}"
-
+locale group =
+ fixes
+ G ::"'a grouptype"
+ e :: "'a"
+ binop :: "'a => 'a => 'a" (infixr "##" 80)
+ INV :: "'a => 'a" ("i (_)" [90]91)
+ assumes
+ Group_G "G: Group"
+ defines
+ e_def "e == unit G"
+ binop_def "op ## == bin_op G"
+ inv_def "INV == inverse G"
end
--- a/src/HOL/GroupTheory/ROOT.ML Mon Jul 02 21:53:11 2001 +0200
+++ b/src/HOL/GroupTheory/ROOT.ML Tue Jul 03 15:28:24 2001 +0200
@@ -1,4 +1,5 @@
no_document use_thy "Primes";
+use_thy "DirProd";
use_thy "Sylow";
--- a/src/HOL/GroupTheory/Sylow.ML Mon Jul 02 21:53:11 2001 +0200
+++ b/src/HOL/GroupTheory/Sylow.ML Tue Jul 03 15:28:24 2001 +0200
@@ -1,720 +1,342 @@
-(* Title: HOL/GroupTheory/Group
+(* Title: HOL/GroupTheory/Sylow
ID: $Id$
Author: Florian Kammueller, with new proofs by L C Paulson
- Copyright 2001 University of Cambridge
+ Copyright 1998-2001 University of Cambridge
+
+Sylow's theorem using locales (combinatorial argument in Exponent.thy)
*)
-(* The clean version, no comments, more tacticals*)
-
-AddIffs [p1 RS prime_imp_one_less];
-
-val [q1,q2,q3] = goal Sylow.thy "[|M <= carrier G; g\\<in>carrier G; h\\<in>carrier G |]\
-\ ==> (M #> g) #> h = M #> (g ## h)";
-by (rewrite_goals_tac [r_coset_abbr, bin_op_abbr]);
-by (rtac coset_mul_assoc 1);
-by (rtac p2 1);
-by (rtac q1 1);
-by (rtac q2 1);
-by (rtac q3 1);
-qed "Icoset_mul_assoc";
-
-val [q1] = goal Sylow.thy "[| M <= carrier G |] ==> M #> e = M";
-by (rewrite_goals_tac [r_coset_abbr,e_def]);
-by (rtac coset_mul_unity 1);
-by (rtac p2 1);
-by (rtac q1 1);
-qed "Icoset_mul_unity";
+Open_locale "sylow";
-val [q1,q2,q3,q4] = goal Sylow.thy "[| x\\<in>carrier G; y\\<in>carrier G;\
-\ M <= carrier G; M #> (x ## inv y) = M |] ==> M #> x = M #> y";
-by (rewtac r_coset_abbr);
-by (rtac coset_mul_invers1 1);
-by (rtac p2 1);
-by (rtac q1 1);
-by (rtac q2 1);
-by (rtac q3 1);
-by (fold_goals_tac [r_coset_abbr, bin_op_abbr,inv_def]);
-by (rtac q4 1);
-qed "Icoset_mul_invers1";
-
-val [q1,q2,q3,q4] = goal Sylow.thy "[| x\\<in>carrier G; y\\<in>carrier G;\
-\ M <= carrier G; M #> x = M #> y|] ==> M #> (x ## inv y) = M ";
-by (rewrite_goals_tac [r_coset_abbr,inv_def,bin_op_abbr]);
-by (rtac coset_mul_invers2 1);
-by (rtac p2 1);
-by (rtac q1 1);
-by (rtac q2 1);
-by (rtac q3 1);
-by (fold_goals_tac [r_coset_abbr]);
-by (rtac q4 1);
-qed "Icoset_mul_invers2";
+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";
-val [q1,q2,q3] = goal Sylow.thy "[| x\\<in>carrier G; H <<= G;\
-\ H #> x = H |] ==> x\\<in>H";
-by (rtac coset_join1 1);
-by (rtac p2 1);
-by (rtac q1 1);
-by (rtac q2 1);
-by (fold_goals_tac [r_coset_abbr]);
-by (rtac q3 1);
-qed "Icoset_join1";
-
-val [q1,q2,q3] = goal Sylow.thy "[| x\\<in>carrier G; H <<= G;\
-\ x\\<in>H |] ==> H #> x = H";
-by (rewtac r_coset_abbr);
-by (rtac coset_join2 1);
-by (rtac p2 1);
-by (rtac q1 1);
-by (rtac q2 1);
-by (rtac q3 1);
-qed "Icoset_join2";
+AddIffs [finite_G];
+Addsimps [coset_mul_e];
-val [q1,q2,q3,q4] = goal Sylow.thy "[| x\\<in>carrier G; y\\<in>carrier G;\
-\ z\\<in>carrier G; x ## y = x ## z |] ==> y = z";
-by (rtac left_cancellation 1);
-by (rtac p2 1);
-by (fold_goals_tac [bin_op_abbr]);
-by (rtac q1 1);
-by (rtac q2 1);
-by (rtac q3 1);
-by (rtac q4 1);
-qed "Ileft_cancellation";
-
-val [q1,q2,q3,q4] = goal Sylow.thy "[| x\\<in>carrier G; y\\<in>carrier G;\
-\ z\\<in>carrier G; y ## x = z ## x |] ==> y = z";
-by (rtac right_cancellation 1);
-by (rtac p2 1);
-by (fold_goals_tac [bin_op_abbr]);
-by (rtac q1 1);
-by (rtac q2 1);
-by (rtac q3 1);
-by (rtac q4 1);
-qed "Iright_cancellation";
-
-goal Sylow.thy "e\\<in>carrier G";
-by (rewtac e_def);
-by (rtac (p2 RS unity_closed) 1);
-qed "Iunity_closed";
+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";
-val [q1,q2] = goal Sylow.thy "[|x\\<in>carrier G; y\\<in>carrier G |]\
-\ ==> x ## y\\<in>carrier G";
-by (rewtac bin_op_abbr);
-by (rtac bin_op_closed 1);
-by (rtac p2 1);
-by (rtac q1 1);
-by (rtac q2 1);
-qed "Ibin_op_closed";
-
-val [q1] = goal Sylow.thy "[|x\\<in>carrier G |] ==> inv x\\<in>carrier G";
-by (rewtac inv_def);
-by (rtac invers_closed 1);
-by (rtac p2 1);
-by (rtac q1 1);
-qed "Iinvers_closed";
-
-val [q1] = goal Sylow.thy "[| x\\<in>carrier G |] ==> e ## x = x";
-by (rewrite_goals_tac [e_def,bin_op_abbr]);
-by (rtac unity_ax1 1);
-by (rtac p2 1);
-by (rtac q1 1);
-qed "Iunity_ax1";
-
-val [q1] = goal Sylow.thy "[| x\\<in>carrier G |] ==> x ## e = x";
-by (rewrite_goals_tac [e_def,bin_op_abbr]);
-by (rtac unity_ax2 1);
-by (rtac p2 1);
-by (rtac q1 1);
-qed "Iunity_ax2";
-
-val [q1] = goal Sylow.thy "[| x\\<in>carrier G |] ==> x ## inv x = e";
-by (rewrite_goals_tac [e_def,inv_def,bin_op_abbr]);
-by (rtac invers_ax1 1);
-by (rtac p2 1);
-by (rtac q1 1);
-qed "Iinvers_ax1";
-
-val [q1] = goal Sylow.thy "[| x\\<in>carrier G |] ==> inv x ## x = e";
-by (rewrite_goals_tac [e_def,inv_def,bin_op_abbr]);
-by (rtac invers_ax2 1);
-by (rtac p2 1);
-by (rtac q1 1);
-qed "Iinvers_ax2";
+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";
-val [q1,q2,q3] = goal Sylow.thy "[| x\\<in>carrier G; y\\<in>carrier G; z\\<in>carrier G |] \
-\ ==> (x ## y)## z = x ##(y ## z)";
-by (rewtac bin_op_abbr);
-by (rtac bin_op_assoc 1);
-by (rtac p2 1);
-by (rtac q1 1);
-by (rtac q2 1);
-by (rtac q3 1);
-qed "Ibin_op_assoc";
-
-val [q1] = goal Sylow.thy "H <<= G ==> e\\<in>H";
-by (rewtac e_def);
-by (rtac SG_unity 1);
-by (rtac p2 1);
-by (rtac q1 1);
-qed "ISG_unity";
-
-val prems = goal Sylow.thy "[| H <= carrier G; H \\<noteq> {};\
-\ \\<forall> x \\<in> H. inv x \\<in> H; \\<forall> x \\<in> H. \\<forall> y \\<in> H. x ## y \\<in> H |] ==> H <<= G";
-by (rtac subgroupI 1);
-by (fold_goals_tac [bin_op_abbr, inv_def]);
-by (REPEAT (ares_tac (p2 :: prems) 1));
-qed "IsubgroupI";
+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";
-goal Sylow.thy "equiv calM RelM";
-by (rewtac equiv_def);
-by (Step_tac 1);
-by (rewrite_goals_tac [refl_def,RelM_def]);
-by (rtac conjI 1);
-by (Step_tac 1);
-by (res_inst_tac [("x","e")] bexI 1);
-by (rtac Iunity_closed 2);
-by (rtac (Icoset_mul_unity RS sym) 1);
-by (SELECT_GOAL (rewtac calM_def) 1);
-by (Fast_tac 1);
-by (rewtac sym_def);
-by (Step_tac 1);
-by (res_inst_tac [("x","inv g")] bexI 1);
-by (etac Iinvers_closed 2);
-by (stac Icoset_mul_assoc 1);
-by (etac Iinvers_closed 3);
-by (assume_tac 2);
-by (SELECT_GOAL (rewtac calM_def) 1);
-by (Fast_tac 1);
-by (etac (Iinvers_ax1 RS ssubst) 1);
-by (stac Icoset_mul_unity 1);
-by (SELECT_GOAL (rewtac calM_def) 1);
-by (Fast_tac 1);
-by (rtac refl 1);
-by (rewtac trans_def);
-by (Step_tac 1);
-by (res_inst_tac [("x","ga ## g")] bexI 1);
-by (rtac Icoset_mul_assoc 1);
-by (rewtac calM_def);
-by (rotate_tac 4 1);
-by (Fast_tac 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (etac Ibin_op_closed 1);
-by (assume_tac 1);
+Goalw [equiv_def] "equiv calM RelM";
+by (blast_tac (claset() addIs [RelM_refl, RelM_sym, RelM_trans]) 1);
qed "RelM_equiv";
-
-val [q1] = goal Sylow.thy
-" M\\<in>calM // RelM ==> M <= calM";
-by (rtac quotientE 1);
-by (rtac q1 1);
-by (etac ssubst 1);
-by (rewrite_goals_tac [Image_def, RelM_def,subset_def]);
-by (rtac ballI 1);
-by (dtac CollectD 1);
-(* change *)
-by (etac bexE 1);
-by (dtac CollectD_prod 1);
-by (dtac conjunct1 1);
-by (etac SigmaD2 1);
+Goalw [RelM_def] "M \\<in> calM // RelM ==> M <= calM";
+by (blast_tac (claset() addSEs [quotientE]) 1);
qed "M_subset_calM_prep";
-val [q1] = goal Sylow.thy
-" M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M)) ==> M <= calM";
-by (rtac M_subset_calM_prep 1);
-by (rtac (q1 RS conjunct1) 1);
+(*** 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";
-val [q1,q2] = goal Sylow.thy "[|M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
-\ M1\\<in>M|] ==> card(M1) = p ^ a";
-by (res_inst_tac [("P", "M1 <= carrier G")] conjunct2 1);
-by (res_inst_tac [("a","M1")] CollectD 1);
-by (fold_goals_tac [calM_def]);
-by (rtac (q2 RSN(2, subsetD)) 1);
-by (rtac (q1 RS M_subset_calM) 1);
+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";
-val [q1,q2] = goal Sylow.thy
- "[|M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
-\ M1\\<in>M|] ==> \\<exists>x. x\\<in>M1";
-by (rtac NotEmpty_ExEl 1);
-by (rtac card_nonempty 1);
-by (rtac (q2 RS (q1 RS card_M1) RS ssubst) 1);
-by (rtac zero_less_prime_power 1);
-by (rtac p1 1);
+Goal "\\<exists>x. x\\<in>M1";
+by (rtac (card_nonempty RS NotEmpty_ExEl) 1);
+by (simp_tac (simpset() addsimps [card_M1, zero_less_prime_power, prime_p]) 1);
qed "exists_x_in_M1";
-val [q1,q2] = goal Sylow.thy "[| M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
-\ M1\\<in>M|] ==> M1 <= carrier G";
-by (rtac PowD 1);
-by (rtac subsetD 1);
-by (rtac q2 2);
-by (rtac subset_trans 1);
-by (rtac (q1 RS M_subset_calM) 1);
-by (rewtac calM_def);
-by (rtac subsetI 1);
-by (rtac PowI 1);
-by (rtac conjunct1 1);
-by (etac CollectD 1);
+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";
-val [q1,q2] = goal Sylow.thy
-"[| M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M)); M1\\<in>M|] ==> \
-\ \\<exists>f \\<in> {g. g\\<in>carrier G & M1 #> g = M1} -> M1. inj_on f {g. g\\<in>carrier G & M1 #> g = M1}";
-by (rtac exE 1);
-by (rtac (q2 RS (q1 RS exists_x_in_M1)) 1);
-by (res_inst_tac [("x", "% z. x ## z")] bexI 1);
-by (rewtac funcset_def);
-by (rtac CollectI 2);
-by (rtac ballI 2);
-by (dtac CollectD 2);
-by (ftac conjunct2 2);
-by (SELECT_GOAL (rewrite_goals_tac [r_coset_abbr, r_coset_def]) 2);
-by (dtac equalityD1 2);
-by (rewtac subset_def);
-by (fold_goals_tac [bin_op_abbr]);
-by (res_inst_tac [("P","%z. z\\<in>M1")] bspec 2);
-by (assume_tac 2);
-by (rtac CollectI 2);
-by (rtac bexI 2);
-by (assume_tac 3);
-by (rtac refl 2);
+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", "lam 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 Ileft_cancellation 1);
-by (assume_tac 4);
-by (dres_inst_tac [("a","y")] CollectD 3);
-by (etac conjunct1 3);
-by (dtac CollectD 2);
-by (etac conjunct1 2);
-by (etac (q2 RS (q1 RS M1_subset_G) RS subsetD) 1);
-val M1_inj_H = result();
+by (rtac left_cancellation 1);
+by (auto_tac (claset(), simpset() addsimps [H_def, M1_subset_G RS subsetD]));
+qed "M1_inj_H";
-val [q1,q2] = goal Sylow.thy "[| {} = RelM `` {x}; x\\<in>calM |] ==> False";
-by (res_inst_tac [("a","x")] emptyE 1);
-by (stac q1 1);
-by (rtac (q2 RS(RelM_equiv RS equiv_class_self)) 1);
-qed "RangeNotEmpty";
-
-goal Sylow.thy "{} \\<notin> calM // RelM";
-by (rtac notI 1);
-by (rtac (RangeNotEmpty RSN (2, quotientE)) 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (assume_tac 1);
+Goal "{} \\<notin> calM // RelM";
+by (blast_tac (claset() addSEs [quotientE]
+ addDs [RelM_equiv RS equiv_class_self]) 1);
qed "EmptyNotInEquivSet";
-val [q1] = goal Sylow.thy
-"M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M))==> \\<exists>M1. M1\\<in>M";
-by (rtac NotEmpty_ExEl 1);
-by (rtac (q1 RS conjunct1 RSN (2, MnotEqempty)) 1);
-by (rtac EmptyNotInEquivSet 1);
+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;
-goal Sylow.thy "0 < order(G)";
-by (rewtac order_def);
-by (fold_goals_tac [carrier_def]);
-by (rtac zero_less_card_empty 1);
-by (rtac p4 1);
-by (rtac ExEl_NotEmpty 1);
-by (res_inst_tac [("x","e")] exI 1);
-by (rtac Iunity_closed 1);
+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 Sylow.thy "0 < m";
-by (res_inst_tac [("P","0 < p ^ a")] conjunct2 1);
-by (rtac (zero_less_mult_iff RS subst) 1);
-by (rtac (p3 RS subst) 1);
-by (rtac zero_less_o_G 1);
+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 Sylow.thy "card(calM) = ((p ^ a) * m choose p ^ a)";
-by (simp_tac
- (simpset() addsimps [calM_def, p3 RS sym, order_eq, n_subsets, p4]) 1);
+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 (asm_full_simp_tac (simpset() addsimps [card_calM]) 1);
-by (rtac zero_less_binomial 1);
-by (rtac le_extend_mult 1);
-by (rtac le_refl 2);
-by (rtac zero_less_m 1);
+by (simp_tac (simpset() addsimps [card_calM, zero_less_binomial,
+ le_extend_mult, zero_less_m]) 1);
qed "zero_less_card_calM";
-Goal "~ (p ^ ((exponent p m)+ 1) dvd card(calM))";
+Goal "~(p ^ (exponent p m+ 1) 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, p1] 1);
+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";
-goal Sylow.thy "finite calM";
-by (rtac finite_subset 1);
-by (rtac (finite_Pow_iff RS iffD2) 2);
-by (rtac p4 2);
+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 ^ ((exponent p m)+ 1) 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 (rtac PowI 1);
-by (SELECT_GOAL (rewtac calM_def) 1);
-by (dtac CollectD 1);
-by (etac conjunct1 1);
-qed "finite_calM";
+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";
-Goal "~(\\<forall> x\\<in>M. P x) ==> \\<exists>x\\<in>M. ~P x";
-by (blast_tac (claset() addIs []) 1);
-qed "Set_NotAll_ExNot";
+(*** 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 "(lam 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";
-goal Sylow.thy "\\<exists>M. M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M))";
-by (fold_goals_tac [Bex_def]);
-by (rtac Set_NotAll_ExNot 1);
-by (rtac contrapos_nn 1);
-by (rtac max_p_div_calM 1);
-by (rtac (RelM_equiv RSN(2, equiv_imp_dvd_card)) 1);
-by (rtac finite_calM 1);
-by (assume_tac 1);
-qed "lemma_A1";
-
-val [q1,q2,q3,q4] = goal Sylow.thy "[| M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
-\ M1\\<in>M; x\\<in>{g. g\\<in>carrier G & M1 #> g = M1}; xa\\<in>{g. g\\<in>carrier G & M1 #> g = M1}|]\
-\ ==> x ## xa\\<in>{g. g\\<in>carrier G & M1 #> g = M1}";
-val l1 = q3 RS CollectD RS conjunct2;
-val l2 = q4 RS CollectD RS conjunct2;
-val l3 = q3 RS CollectD RS conjunct1;
-val l4 = q4 RS CollectD RS conjunct1;
-by (rtac CollectI 1);
-by (rtac conjI 1);
-by (rtac Ibin_op_closed 1);
-by (rtac l3 1);
-by (rtac l4 1);
-by (rtac (Icoset_mul_assoc RS subst) 1);
-by (rtac l3 2);
-by (rtac l4 2);
-by (rtac (q2 RS (q1 RS M1_subset_G)) 1);
-by (stac l1 1);
-by (stac l2 1);
-by (rtac refl 1);
-qed "bin_op_closed_lemma";
+(** the opposite injection **)
-val [q1,q2] = goal Sylow.thy "[|M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
-\ M1\\<in>M |] ==> {g. g\\<in>carrier G & M1 #> g = M1} <<= G";
-by (rtac IsubgroupI 1);
-by (rtac subsetI 1);
-by (etac subset_lemma1 1);
-by (rtac ExEl_NotEmpty 1);
-by (res_inst_tac [("x","e")] exI 1);
-by (rtac CollectI 1);
-by (rtac conjI 1);
-by (rtac Iunity_closed 1);
-by (rtac Icoset_mul_unity 1);
-by (rtac (q2 RS (q1 RS M1_subset_G)) 1);
-by (rtac ballI 1);
-by (rtac CollectI 1);
-by (dtac CollectD 1);
-by (rtac conjI 1);
-by (rtac Iinvers_closed 1);
-by (etac conjunct1 1);
-by (ftac conjunct2 1);
-by (eres_inst_tac [("P","%z. z #> inv x = M1")] subst 1);
-by (stac Icoset_mul_assoc 1);
-by (rtac (q2 RS (q1 RS M1_subset_G)) 1);
-by (etac conjunct1 1);
-by (rtac Iinvers_closed 1);
-by (etac conjunct1 1);
-by (stac Iinvers_ax1 1);
-by (etac conjunct1 1);
-by (rtac Icoset_mul_unity 1);
-by (rtac (q2 RS (q1 RS M1_subset_G)) 1);
-by (rtac ballI 1);
-by (rtac ballI 1);
-by (rtac (q2 RS( q1 RS bin_op_closed_lemma)) 1);
-by (assume_tac 1);
-by (assume_tac 1);
-qed "H_is_SG";
-
-val [q1,q2,q3] = goal Sylow.thy "[| M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
-\ M1 \\<in> M; M2 \\<in> M|] ==> \\<exists>g \\<in> carrier G. M1 #> g = M2";
-val l1 = (q1 RS conjunct1) RS (RelM_equiv RS ElemClassEquiv);
-val l2 = q2 RS ((q3 RS (l1 RS bspec)) RS bspec);
-by (rtac bex_sym 1);
-by (res_inst_tac [("P","(M2, M1)\\<in>calM <*> calM")] conjunct2 1);
-by (res_inst_tac [("x","M2"),("y","M1")] CollectD_prod 1);
-by (fold_goals_tac [RelM_def]);
-by (rtac l2 1);
-qed "M_elem_map";
-
-val [q1,q2,q3] = goal Sylow.thy "[|M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
-\ M1 \\<in> M; H\\<in>set_r_cos G {g. g\\<in>carrier G & M1 #> g = M1} |] ==>\
-\ \\<exists>g \\<in> carrier G. {g. g\\<in>carrier G & M1 #> g = M1} #> g = H";
-by (rtac bex_sym 1);
-by (res_inst_tac [("a","H")] CollectD 1);
-by (rewtac r_coset_abbr);
-by (fold_goals_tac [set_r_cos_def]);
-by (fold_goals_tac [r_coset_abbr]);
-by (rtac q3 1);
+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 [q1,q2,q3,q4] = goal Sylow.thy "[| M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
-\ M1 \\<in> M; g\\<in>carrier G; x\\<in>M1 #> g |] ==> x\\<in>carrier G";
-by (rtac (q4 RSN(2, mp)) 1);
-by (rtac impI 1);
-by (rewrite_goals_tac [r_coset_abbr,r_coset_def]);
-by (fold_goals_tac [bin_op_abbr]);
-by (dtac CollectD 1);
-by (etac bexE 1);
-by (etac subst 1);
-by (rtac Ibin_op_closed 1);
-by (rtac q3 2);
-by (etac (q2 RS( q1 RS M1_subset_G) RS subsetD) 1);
-qed "rcosetGM1g_subset_G";
-
-val [q1,q2] = goal Sylow.thy "[|M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
-\ M1 \\<in> M|] ==> finite M1";
-by (rtac finite_subset 1);
-by (rtac (q2 RS (q1 RS M1_subset_G)) 1);
-by (rtac p4 1);
-qed "finite_M1";
-
-val [q1,q2,q3] = goal Sylow.thy "[|M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
-\ M1 \\<in> M; g\\<in>carrier G|] ==> finite (M1 #> g)";
-by (rtac finite_subset 1);
-by (rtac subsetI 1);
-by (etac (q3 RS( q2 RS (q1 RS rcosetGM1g_subset_G))) 1);
-by (rtac p4 1);
-qed "finite_rcosetGM1g";
+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;
-val [q1,q2,q3] = goal Sylow.thy "[| M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
-\ M1 \\<in> M; g\\<in>carrier G|] ==> card(M1) = card(M1 #> g)";
-by (rewtac r_coset_abbr);
-by (rtac sym 1);
-by (rtac (p2 RS card_cosets_equal RS bspec) 1);
-by (rtac (q2 RS (q1 RS M1_subset_G)) 1);
-by (rtac p4 1);
-by (rewtac set_r_cos_def);
-by (Step_tac 1);
-by (rtac bexI 1);
-by (rtac refl 1);
-by (rtac q3 1);
-qed "M1_cardeq_rcosetGM1g";
-
-val [q1,q2,q3] = goal Sylow.thy "[| M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
-\ M1 \\<in> M; g\\<in>carrier G|] ==> (M1, M1 #> g)\\<in>RelM";
-val l1 = (q2 RS (q1 RS M1_subset_G));
-val l2 = q3 RS (q2 RS (q1 RS rcosetGM1g_subset_G));
-by (rewtac RelM_def);
-by (rtac CollectI_prod 1);
-by (rtac conjI 1);
-by (rtac SigmaI 1);
-by (SELECT_GOAL (rewtac calM_def) 1);
-by (rtac CollectI 1);
-by (rtac conjI 1);
-by (rtac (q2 RS (q1 RS card_M1)) 2);
-by (rtac l1 1);
-
-by (rewtac calM_def);
-by (rtac CollectI 1);
-by (rtac conjI 1);
-by (rtac (q3 RS (q2 RS (q1 RS M1_cardeq_rcosetGM1g)) RS subst) 2);
-by (rtac (q2 RS (q1 RS card_M1)) 2);
-by (rtac subsetI 1);
-by (etac l2 1);
-by (res_inst_tac [("x","inv g")] bexI 1);
-by (stac Icoset_mul_assoc 1);
-by (rtac l1 1);
-by (rtac q3 1);
-by (rtac (q3 RS Iinvers_closed) 1);
-by (stac Iinvers_ax1 1);
-by (rtac q3 1);
-by (rtac (Icoset_mul_unity RS sym) 1);
-by (rtac l1 1);
-by (rtac (q3 RS Iinvers_closed) 1);
-qed "M1_RelM_rcosetGM1g";
+Goal "(lam 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";
-val [q1,q2] = goal Sylow.thy "[| M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
-\ M1\\<in>M|] ==> (\\<exists>f \\<in> M -> set_r_cos G {g. g\\<in>carrier G & M1 #> g = M1}. inj_on f M )\
-\ & (\\<exists>g \\<in> (set_r_cos G {g. g\\<in>carrier G & M1 #> g = M1}) -> M. \
-\ inj_on g (set_r_cos G {g. g\\<in>carrier G & M1 #> g = M1}))";
-by (rtac conjI 1);
-by (res_inst_tac
-[("x","% M. {g. g\\<in>carrier G & M1 #> g = M1} #> (@ g. g\\<in>carrier G & M1 #> g = M)")]
-bexI 1);
-by (SELECT_GOAL (rewtac funcset_def) 2);
-by (rtac CollectI 2);
-by (rtac ballI 2);
-by (SELECT_GOAL (rewtac set_r_cos_def) 2);
-by (fold_goals_tac [r_coset_abbr]);
-by (rtac CollectI 2);
-by (rtac bexI 2);
-by (rtac refl 2);
-val l1 = (q2 RS(q1 RS M_elem_map)) RS (Bex_def RS apply_def) RS (Ex_def RS apply_def);
-by (rtac (l1 RS conjunct1) 2);
-by (assume_tac 2);
+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 (rtac ((l1 RS conjunct2) RS subst) 1);
-by (assume_tac 1);
-by (res_inst_tac [("P","% z. z = M1 #> (@ x. x\\<in>carrier G & M1 #> x = y)")] subst 1);
-by (rtac (l1 RS conjunct2) 1);
-by (assume_tac 1);
-by (rtac Icoset_mul_invers1 1);
-by (etac (l1 RS conjunct1) 1);
-by (etac (l1 RS conjunct1) 1);
-by (rtac (q2 RS (q1 RS M1_subset_G)) 1);
-by (res_inst_tac
-[("P","(@ xa. xa\\<in>carrier G & M1 #> xa = x) ## (inv (@ x. x\\<in>carrier G & M1 #> x = y))\\<in>carrier G")]
-conjunct2 1);
-by (res_inst_tac
-[("a","(@ xa. xa\\<in>carrier G & M1 #> xa = x) ## (inv (@ x. x\\<in>carrier G & M1 #> x = y))")]
-CollectD 1);
-by (rtac (H_is_SG RSN(2, Icoset_join1)) 1);
-by (rtac Ibin_op_closed 1);
-by (etac (l1 RS conjunct1) 1);
-by (rtac Iinvers_closed 1);
-by (etac (l1 RS conjunct1) 1);
-by (rtac q1 1);
-by (rtac q2 1);
-by (rtac Icoset_mul_invers2 1);
-by (etac (l1 RS conjunct1) 1);
-by (etac (l1 RS conjunct1) 1);
-by (rtac subsetI 1);
-by (dtac CollectD 1);
-by (etac conjunct1 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 (res_inst_tac [("x","% C. M1 #> (@g. g\\<in>carrier G &\
-\ {g. g \\<in> carrier G & M1 #> g = M1} #> g = C)")] bexI 1);
-by (rewtac funcset_def);
-by (rtac CollectI 2);
-by (rtac ballI 2);
-by (rtac ((q2 RS (q1 RS M1_RelM_rcosetGM1g)) RSN (4, EquivElemClass)) 2);
-by (rtac RelM_equiv 2);
-by (rtac (q1 RS conjunct1) 2);
-by (rtac q2 2);
-by (SELECT_GOAL (rewtac set_r_cos_def) 2);
-by (dtac CollectD 2);
-by (dtac bex_sym 2);
-by (fold_goals_tac [r_coset_abbr]);
-by (rewrite_goals_tac [Bex_def,Ex_def]);
-by (etac conjunct1 2);
-by (rtac inj_onI 1);
-val l1 = (q2 RS (q1 RS H_elem_map)) RS (Bex_def RS apply_def) RS (Ex_def RS apply_def);
-by (rtac (l1 RS conjunct2 RS subst) 1);
-by (assume_tac 1);
-by (res_inst_tac [("t","x")] (l1 RS conjunct2 RS subst) 1);
-by (assume_tac 1);
-by (rtac Icoset_mul_invers1 1);
-by (etac (l1 RS conjunct1) 1);
-by (etac (l1 RS conjunct1) 1);
-val l2 = (q2 RS (q1 RS H_is_SG));
-by (rtac (l2 RS (subgroup_def RS apply_def) RS conjunct1) 1);
-by (rtac Icoset_join2 1);
-by (rtac Ibin_op_closed 1);
-by (etac (l1 RS conjunct1) 1);
-by (rtac Iinvers_closed 1);
-by (etac (l1 RS conjunct1) 1);
-by (rtac l2 1);
-by (rtac CollectI 1);
-by (rtac conjI 1);
-by (rtac Ibin_op_closed 1);
-by (etac (l1 RS conjunct1) 1);
-by (rtac Iinvers_closed 1);
-by (etac (l1 RS conjunct1) 1);
-by (rtac Icoset_mul_invers2 1);
-by (assume_tac 4);
-by (etac (l1 RS conjunct1) 1);
-by (etac (l1 RS conjunct1) 1);
-by (rtac (q2 RS (q1 RS M1_subset_G)) 1);
-qed "bij_M_GmodH";
+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 Sylow.thy "calM <= Pow(carrier G)";
-by (rtac subsetI 1);
-by (rtac PowI 1);
-by (rewtac calM_def);
-by (dtac CollectD 1);
-by (etac conjunct1 1);
+Goal "calM <= Pow(carrier G)";
+by (auto_tac (claset(), simpset() addsimps [calM_def]));
qed "calM_subset_PowG";
-val [q1] = goal Sylow.thy "M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M)) ==> finite M";
+
+Goal "finite M";
by (rtac finite_subset 1);
-by (rtac (q1 RS M_subset_calM RS subset_trans) 1);
+by (rtac (M_subset_calM RS subset_trans) 1);
by (rtac calM_subset_PowG 1);
-by (rtac (p4 RS (finite_Pow_iff RS iffD2)) 1);
+by (Blast_tac 1);
qed "finite_M";
-val [q1,q2] = goal Sylow.thy "[| M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
-\ M1\\<in>M|] ==> card(M) = card(set_r_cos G {g. g\\<in>carrier G & M1 #> g = M1})";
-by (rtac card_bij 1);
-by (rtac (q1 RS finite_M) 1);
-by (rtac finite_subset 1);
-by (rtac (p2 RS set_r_cos_subset_PowG) 1);
-by (rtac (q2 RS( q1 RS H_is_SG)) 1);
-by (rtac (p4 RS (finite_Pow_iff RS iffD2)) 1);
-val l1 = (q2 RS (q1 RS bij_M_GmodH));
-by (rtac (l1 RS conjunct1) 1);
-by (rtac (l1 RS conjunct2) 1);
+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";
-val [q1,q2] = goal Sylow.thy "[| M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
-\ M1\\<in>M|] ==> (card(M) * card({g. g\\<in>carrier G & M1 #> g = M1})) = order(G)";
-by (rtac ((q2 RS( q1 RS cardMeqIndexH)) RS ssubst) 1);
-by (rtac Lagrange 1);
-by (rtac p2 1);
-by (rtac p4 1);
-by (rtac (q2 RS (q1 RS H_is_SG)) 1);
+Goal "card(M) * card(H) = order(G)";
+by (simp_tac (simpset() addsimps [cardMeqIndexH,lagrange, H_is_SG]) 1);
qed "index_lem";
-val [q1,q2] = goal Sylow.thy
- "[| M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
-\ M1\\<in>M |] \
-\ ==> p ^ a <= card({g. g\\<in>carrier G & M1 #> g = M1})";
-by (rtac dvd_imp_le 1);
-by (res_inst_tac [("r","exponent p m"),("n", "card(M)")] div_combine 1);
-by (rtac p1 1);
-by (rtac SG_card1 3);
-by (rtac p2 3);
-by (rtac p4 3);
-by (rtac (q2 RS (q1 RS H_is_SG)) 3);
-by (rtac (q1 RS conjunct2) 1);
-by (rtac (q2 RS (q1 RS index_lem) RS ssubst) 1);
-by (stac p3 1);
-by (stac power_add 1);
-by (rtac mult_dvd_mono 1);
-by (rtac dvd_refl 1);
-by (rtac power_exponent_dvd 1);
-by (rtac zero_less_m 1);
+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";
-val [q1,q2] = goal Sylow.thy "[| M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
-\ M1\\<in>M |] ==> card({g. g\\<in>carrier G & M1 #> g = M1}) <= p ^ a";
-by (rtac (q2 RS (q1 RS card_M1) RS subst) 1);
-by (rtac bexE 1);
-by (rtac (q2 RS (q1 RS M1_inj_H)) 1);
-by (rtac card_inj 1);
-by (assume_tac 3);
-by (assume_tac 3);
-by (rtac finite_subset 2);
-by (rtac p4 3);
-by (rtac (q2 RS (q1 RS M1_subset_G)) 2);
-by (rtac finite_subset 1);
-by (rtac p4 2);
-by (rtac subsetI 1);
-by (etac subset_lemma1 1);
+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";
-val [q1,q2] = goal Sylow.thy "[| M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
-\ M1\\<in>M|] ==> {g. g\\<in>carrier G & M1 #> g = M1} <<= G & \
-\ card({g. g\\<in>carrier G & M1 #> g = M1}) = p ^ a";
-by (rtac conjI 1);
-by (rtac le_anti_sym 2);
-by (rtac (q2 RS( q1 RS H_is_SG)) 1);
-by (rtac (q2 RS( q1 RS lemma_leq2)) 1);
-by (rtac (q2 RS( q1 RS lemma_leq1)) 1);
-qed "main_proof";
+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 Sylow.thy "\\<exists>H. H <<= G & card(H) = p ^ a";
-by (rtac exE 1);
-by (rtac lemma_A1 1);
-by (rtac exE 1);
-by (etac existsM1inM 1);
-by (dtac main_proof 1);
-by (assume_tac 1);
-by (etac exI 1);
-qed "Sylow1";
+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";
--- a/src/HOL/GroupTheory/Sylow.thy Mon Jul 02 21:53:11 2001 +0200
+++ b/src/HOL/GroupTheory/Sylow.thy Tue Jul 03 15:28:24 2001 +0200
@@ -1,45 +1,39 @@
-(* Title: HOL/GroupTheory/Group
+(* Title: HOL/GroupTheory/Sylow
ID: $Id$
Author: Florian Kammueller, with new proofs by L C Paulson
- Copyright 2001 University of Cambridge
-*)
+ Copyright 1998-2001 University of Cambridge
-(* Theory file for the proof of Sylow's theorem. F. Kammueller 11.10.96
-Step 1: Use two separate .thy files for groups and Sylow's thm, respectively:
-
-I.e. here are the definitions which are specific for Sylow's theorem.
+Sylow's theorem using locales (combinatorial argument in Exponent.thy)
*)
-Sylow = Group +
-
-types i
-arities i::term
-
-consts
- G :: "i set * ([i, i] => i) * (i => i) * i"
-(* overloading for the carrier of G does not work because "duplicate declaration" : G :: "i set" *)
- p, a, m :: "nat"
- r_cos :: "[i set, i] => i set" ("_ #> _" [60,61]60)
- "##" :: "[i, i] => i" (infixl 60)
+Sylow = Coset +
- (* coset and bin_op short forms *)
-defs
- r_coset_abbr "H #> x == r_coset G H x"
- bin_op_abbr "x ## y == bin_op G x y"
+locale sylow = coset +
+ fixes
+ p :: "nat"
+ a :: "nat"
+ m :: "nat"
+ calM :: "'a set set"
+ RelM :: "('a set * 'a set)set"
+ assumes
+ prime_p "p\\<in>prime"
+ order_G "order(G) = (p^a) * m"
+ finite_G "finite (carrier G)"
+ defines
+ calM_def "calM == {s. s <= carrier(G) & card(s) = p^a}"
+ RelM_def "RelM == {(N1,N2). (N1,N2) \\<in> calM \\<times> calM &
+ (\\<exists>g \\<in> carrier(G). N1 = (N2 #> g) )}"
-constdefs
- e :: "i" "e == unity G"
- inv :: "i => i" "inv == invers G"
- calM :: "i set set"
- "calM == {s. s <= carrier(G) & card(s) = (p ^ a)}"
- RelM :: "(i set * i set)set"
- "RelM == {(N1,N2).(N1,N2): calM <*> calM & (? g: carrier(G). N1 = (N2 #> g) )}"
-
-rules
-(* specific rules modeling the section mechanism *)
-p1 "p : prime"
-p2 "G : Group"
-p3 "order(G) = (p ^ a) * m"
-p4 "finite (carrier G)"
+locale sylow_central = sylow +
+ fixes
+ H :: "'a set"
+ M :: "'a set set"
+ M1 :: "'a set"
+ assumes
+ M_in_quot "M \\<in> calM // RelM"
+ not_dvd_M "~(p ^ (exponent p m + 1) dvd card(M))"
+ M1_in_M "M1 \\<in> M"
+ defines
+ H_def "H == {g. g\\<in>carrier G & M1 #> g = M1}"
end
--- a/src/HOL/IsaMakefile Mon Jul 02 21:53:11 2001 +0200
+++ b/src/HOL/IsaMakefile Tue Jul 03 15:28:24 2001 +0200
@@ -259,8 +259,11 @@
$(LOG)/HOL-GroupTheory.gz: $(OUT)/HOL \
Library/Primes.thy \
- GroupTheory/Exponent.thy GroupTheory/Exponent.ML GroupTheory/Group.thy\
- GroupTheory/Group.ML GroupTheory/Sylow.thy GroupTheory/Sylow.ML\
+ GroupTheory/Exponent.thy GroupTheory/Exponent.ML\
+ GroupTheory/Coset.thy GroupTheory/Coset.ML\
+ GroupTheory/DirProd.thy GroupTheory/DirProd.ML\
+ GroupTheory/Group.thy GroupTheory/Group.ML\
+ GroupTheory/Sylow.thy GroupTheory/Sylow.ML\
GroupTheory/ROOT.ML
@$(ISATOOL) usedir $(OUT)/HOL GroupTheory