# HG changeset patch # User paulson # Date 994166904 -7200 # Node ID e88c2c89f98ed5d79f76e4b95a245110ae1a1e30 # Parent ee3d40b5ac237f04cc133f9bfc74cc8e1185e41e Locale-based group theory proofs diff -r ee3d40b5ac23 -r e88c2c89f98e src/HOL/GroupTheory/Coset.ML --- /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; \\f \\ A\\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; \\f \\ A\\B. inj_on f A; \ +\ \\g \\ B\\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 . \\h\\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 . \\h\\H. a ## h = b}"; +by (auto_tac (claset(), + simpset() addsimps [lcos_def, l_coset_def, binop_def])); +qed "l_coset_eq"; + +Goal "{*H*} = {C . \\a\\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 . \\h\\H. \\k\\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\\carrier G; h\\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 \\ carrier G ; y \\ 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 \\ carrier G; y \\ 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 \\ carrier G; H <<= G |] ==> x\\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\\carrier G; H <<= G; x\\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\\carrier G |] ==> H #> x <= carrier G"; +by (auto_tac (claset(), simpset() addsimps [r_coset_eq])); +qed "r_coset_subset_G"; + +Goal "[| h \\ H; H <= carrier G; x \\ carrier G|] ==> h ## x \\ H #> x"; +by (auto_tac (claset(), simpset() addsimps [r_coset_eq])); +qed "rcosI"; + +Goal "[| H <= carrier G; x \\ carrier G |] ==> H #> x \\ {*H*}"; +by (auto_tac (claset(), simpset() addsimps [setrcos_eq])); +qed "setrcosI"; + + +Goal "[| x ## y = z; x \\ carrier G; y \\ carrier G; z\\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 \\ H #> x; x \\ 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 \\ carrier G; H <<= G |] ==> x \\ 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 & (\\x \\ 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 \\ carrier G |] ==> H #> x = x <# H"; +by (afs [thm "lcos_def", thm "rcos_def", normal_def] 1); +qed "normal_imp_rcos_eq_lcos"; + +Goal "\\H \\ G; x \\ (G .); h \\ H\\ \\ i x ## h ## x \\ 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 "\\H \\ G; x \\ (G .); h \\ H\\ \\ x ## h ## i x \\ 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\\carrier G; h\\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\\carrier G |]\ +\ ==> x <# H <= carrier G"; +by (auto_tac (claset(), simpset() addsimps [l_coset_eq, subsetD])); +qed "lcosetGaH_subset_G"; + +Goal "[| y \\ x <# H; x \\ 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 \\ 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\\{*H*}; x \\ 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 \\ 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 \\ 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 \\ carrier G; y \\ 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 \\ carrier G; y \\ 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 \\ carrier G; y \\ 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 \\ carrier G; y \\ 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 \\ {*H*}; H2 \\ {*H*} |] ==> H1 <#> H2 \\ {*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 \\ {*H*} |] ==> I(H1) \\ {*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 \\ {*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 ==> \\ {*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 \\ {*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 \\ {*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 \\ carrier G & y \\ 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 \\ (G .); b \\ (G .); ha ## a = h ## b; \ +\ h \\ H; ha \\ H; hb \\ H|] \ +\ ==> \\h\\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 \\ {*H*}; c2 \\ {*H*}; c1 \\ c2|] ==> c1 \\ 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"; + + + diff -r ee3d40b5ac23 -r e88c2c89f98e src/HOL/GroupTheory/Coset.thy --- /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 \\ 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 == \\G \\ Group. {H. H <<= G & + (\\x \\ 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" ("_ \\ _" [60,61]60) + +translations + "N <| G" == "(G,N) \\ 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 + + diff -r ee3d40b5ac23 -r e88c2c89f98e src/HOL/GroupTheory/DirProd.ML --- /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.) = ((G.) \\ (G'.))"; +by (afs [ProdGroup_def] 1); +qed "P_carrier"; + +Goal "(P.) = \ +\ (lam (x, x'): (P.). lam (y, y'): (P.). ( x ## y, x' ##' y'))"; +by (afs [ProdGroup_def, binop_def, binop'_def] 1); +qed "P_bin_op"; + +Goal "(P.) = (lam (x, y): (P.). (i x, i' y))"; +by (afs [ProdGroup_def, inv_def, inv'_def] 1); +qed "P_inverse"; + +Goal "(P.) = (G., G'.)"; +by (afs [ProdGroup_def, e_def, e'_def] 1); +qed "P_unit"; + +Goal "P = (| carrier = P., \ +\ bin_op = (lam (x, x'): (P.). lam (y, y'): (P.).\ +\ (x ## y, x' ##' y')), \ +\ inverse = (lam (x, y): (P.). (i x, i' y)), \ +\ unit = P. |)"; +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.) : (P.) \\ (P.) \\ (P.)"; +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.) : (P.) \\ (P.)"; +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 \\ Group \\ Group"; +by (REPEAT (ares_tac [funcsetI, ProdGroup_is_Group] 1)); +by (auto_tac (claset(), simpset() addsimps [ProdGroup_def])); +qed "ProdGroup_arity"; diff -r ee3d40b5ac23 -r e88c2c89f98e src/HOL/GroupTheory/DirProd.thy --- /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.) \\ (G'.)), + bin_op = (lam (x, x'): ((G.) \\ (G'.)). + lam (y, y'): ((G.) \\ (G'.)). + ((G.) x y,(G'.) x' y')), + inverse = (lam (x, y): ((G.) \\ (G'.)). ((G.) x, (G'.) y)), + unit = ((G.),(G'.)) |)" + +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 diff -r ee3d40b5ac23 -r e88c2c89f98e src/HOL/GroupTheory/Exponent.ML --- 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*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 (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 \\ {}"; by (force_tac (claset(), simpset() addsimps [card_empty]) 1); qed "card_nonempty"; -Goal "[| finite(A); finite(B); f \\ 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 \\ F; \ \ \\c1\\insert x F. \\c2 \\ insert x F. c1 \\ c2 --> c1 \\ c2 = {}|]\ \ ==> x \\ \\ F = {}"; diff -r ee3d40b5ac23 -r e88c2c89f98e src/HOL/GroupTheory/Exponent.thy --- 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. \\x \\ A. f(x) \\ B}" - exponent :: "[nat, nat] => nat" - "exponent p s == if p \\ prime then (GREATEST r. p ^ r dvd s) else 0" + "exponent p s == if p \\ prime then (GREATEST r. p^r dvd s) else 0" end diff -r ee3d40b5ac23 -r e88c2c89f98e src/HOL/GroupTheory/Group.ML --- 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\\A -> B ==> \\x\\A. f x\\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()) "\\x\\A. f x\\B ==> f\\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\\A -> B -> C ==> \\x\\A. \\ y\\B. f x y\\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()) "\\x\\A. \\ y\\B. f x y\\C ==> f\\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; \ -\ \\f \\ A -> B. inj_on f A; \\g \\ 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 \\ carrier G"; +by (afs [e_def] 1); +qed "e_closed"; +val unit_closed = export e_closed; +Addsimps [e_closed]; -goal (the_context()) "G\\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 ## \\ carrier G \\ carrier G \\ carrier G"; +by (simp_tac (simpset() addsimps [binop_def]) 1); +qed "binop_funcset"; -(* Derivations of the Group definitions *) -val [q1] = goal (the_context()) "G\\Group ==> unity G\\carrier G"; -by (rtac (q1 RSN(2,mp)) 1); -by (res_inst_tac [("P","%x. x\\Group --> unity 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 "unity_closed"; +Goal "[| x \\ carrier G; y \\ carrier G |] ==> x ## y \\ 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\\Group; a\\carrier G; b\\carrier G |] ==> bin_op G a b\\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\\Group --> bin_op G\\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 \\ carrier G \\ carrier G"; +by (simp_tac (simpset() addsimps [inv_def]) 1); +qed "inv_funcset"; -val [q1,q2] = goal (the_context()) "[| G\\Group; a\\carrier G |] ==> invers G a\\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\\Group --> invers 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 "invers_closed"; +Goal "x \\ carrier G ==> i(x) \\ 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\\Group; a\\carrier G |] ==> bin_op G (unity G) a = a"; -by (rtac (q1 RSN(2,mp)) 1); -by (res_inst_tac [("P","%x. x\\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 \\ 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\\Group; a\\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\\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 \\ carrier G ==> i(x) ## x = e"; +by (afs [binop_def, inv_def, e_def] 1); +qed "inv_ax2"; +Addsimps [inv_ax2]; + +Goal "[| x \\ carrier G; y \\ carrier G; z \\ 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\\Group; a\\carrier G; b\\carrier G; c\\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\\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 \\ A \\ A \\ A; i1 \\ A \\ A; e1 \\ A;\ +\ \\x \\ A. (f (i1 x) x = e1); \\x \\ A. (f e1 x = x);\ +\ \\x \\ A. \\y \\ A. \\z \\ A. (f (f x y) z = f (x) (f y z)) |] \ +\ ==> (| carrier = A, bin_op = f, inverse = i1, unit = e1 |) \\ Group"; +by (afs [Group_def] 1); +qed "groupI"; +val GroupI = export groupI; -val [p1,p2,p3,p4,p5] = goal (the_context()) "[| G\\Group; x\\carrier G; y\\carrier G;\ -\ z\\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\\carrier G ; y\\carrier G; z\\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\\Group; a\\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 \\ Group; a\\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\\Group; a\\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\\Group; M <= carrier G; g\\carrier G; h\\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 \\ 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 \\ carrier G; y \\ carrier G; z \\ 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 \\ Group; x\\carrier G; H <<= G;\ -\ x\\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 \\ 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 \\ Group; x\\carrier G; y\\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 \\ 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 \\ Group; x\\carrier G; y\\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 \\ 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\\Group; H <<= G|] ==> unity G\\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 \\ carrier G; y \\ 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 \\ Group; x\\carrier G; H <<= G;\ -\ r_coset G H x = H |] ==> x\\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 \\ 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 \\ 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\\Group; H <= carrier G; H \\ {}; \\ a \\ H. invers G a\\H;\ -\ \\ a\\H. \\ b\\H. bin_op G a b\\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 \\ carrier G; y \\ 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\\Group; x\\carrier G; y\\carrier G;\ -\ z\\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 \\ carrier G; y \\ carrier G; z \\ 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 \\ Group; H <<= G|]\ -\ ==> \\ (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 \\ carrier G; y \\ carrier G; z \\ 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 \\ Group; H <= carrier G; a\\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 \\ {}; \\a \\ H. i(a)\\H; \\a\\H. \\b\\H. a ## b\\H|] \ +\ ==> e \\ H"; +by (Force_tac 1); +qed "e_in_H"; -val [p1,p2,p3] = goal (the_context()) "[|G\\Group; H <= carrier G; finite(carrier G) |]\ -\ ==> \\ c \\ 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 \\ {}; \\a \\ H. i(a)\\H;\ +\ \\a\\H. \\b\\H. a ## b\\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 \\ Group; x \\ carrier G; y \\ carrier G;\ -\ z\\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|)\\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 \\ Group; H <<= G; h1 \\ H; h2 \\ H|]\ -\ ==> bin_op G h1 h2\\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 \\ Group; H <<= G; h1 \\ H|]\ -\ ==> invers G h1\\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 \\ Group; H <<= G |]\ -\ ==> \\ c1 \\ set_r_cos G H. \\ c2 \\ set_r_cos G H. c1 \\ c2 --> c1 \\ 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 \\ H; y \\ H |] ==> x ## y \\ H"; +by (dtac subgroupE2 1); +by (dtac bin_op_closed 1); +by (Asm_full_simp_tac 1); +by (thin_tac "x\\H" 1); +by Auto_tac; +qed "subgroup_f_closed"; + +Goal "[| H <<= G; x \\ H |] ==> i x \\ 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\\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 \\ 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 \\ 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' \\ AbelianGroup; x: carrier G'; y: carrier G'|] \ +\ ==> (G'.) x y = (G'.) y x"; +by (auto_tac (claset(), simpset() addsimps [AbelianGroup_def])); +qed "Group_commute"; - (*version using "Goal" but no locales... - Goal "[| G \\ 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"; diff -r ee3d40b5ac23 -r e88c2c89f98e src/HOL/GroupTheory/Group.thy --- 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 \\ *) +syntax (symbols) + "op funcset" :: "['a set, 'b set] => ('a => 'b) set" (infixr "\\" 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" ("_ ." [10] 10) + "@bin_op" :: "'a semigrouptype => (['a, 'a] => 'a)" ("_ ." [10] 10) + "@inverse" :: "'a grouptype => ('a => 'a)" ("_ ." [10] 10) + "@unit" :: "'a grouptype => 'a" ("_ ." [10] 10) -Group = Exponent + +translations + "G." => "carrier G" + "G." => "bin_op G" + "G." => "inverse G" + "G." => "unit G" + +constdefs + Semigroup :: "('a semigrouptype)set" + "Semigroup == {G. (bin_op G): carrier G \\ carrier G \\ 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 \\ carrier G \\ carrier G & inverse G : carrier G \\ 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.). ! y:(G.). ((G.) x y = (G.) 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 diff -r ee3d40b5ac23 -r e88c2c89f98e src/HOL/GroupTheory/ROOT.ML --- 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"; diff -r ee3d40b5ac23 -r e88c2c89f98e src/HOL/GroupTheory/Sylow.ML --- 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\\carrier G; h\\