--- a/src/HOL/GroupTheory/Bij.ML Wed Sep 25 11:23:26 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,171 +0,0 @@
-(* Title: HOL/GroupTheory/Bij
- ID: $Id$
- Author: Florian Kammueller, with new proofs by L C Paulson
- Copyright 1998-2001 University of Cambridge
-
-Bijections of a set and the group of bijections
- Sigma version with locales
-*)
-
-Addsimps [Id_compose, compose_Id];
-
-(*Inv_f_f should suffice, only here A=B=S so the equality remains.*)
-Goalw [Inv_def]
- "[| f`A = B; x : B |] ==> Inv A f x : A";
-by (Clarify_tac 1);
-by (fast_tac (claset() addIs [restrict_in_funcset, someI2]) 1);
-qed "Inv_mem";
-
-Open_locale "bij";
-
-val B_def = thm "B_def";
-val o'_def = thm "o'_def";
-val inv'_def = thm "inv'_def";
-val e'_def = thm "e'_def";
-
-Addsimps [B_def, o'_def, inv'_def];
-
-Goal "f \\<in> B ==> f \\<in> S \\<rightarrow> S";
-by (afs [Bij_def] 1);
-qed "BijE1";
-
-Goal "f \\<in> B ==> f ` S = S";
-by (afs [Bij_def] 1);
-qed "BijE2";
-
-Goal "f \\<in> B ==> inj_on f S";
-by (afs [Bij_def] 1);
-qed "BijE3";
-
-Goal "[| f \\<in> S \\<rightarrow> S; f ` S = S; inj_on f S |] ==> f \\<in> B";
-by (afs [Bij_def] 1);
-qed "BijI";
-
-Delsimps [B_def];
-Addsimps [BijE1,BijE2,BijE3];
-
-
-(* restrict (Inv S f) S *)
-Goal "f \\<in> B ==> (%x:S. (inv' f) x) \\<in> B";
-by (rtac BijI 1);
-(* 1. (%x:S. (inv' f) x): S \\<rightarrow> S *)
-by (afs [Inv_funcset] 1);
-(* 2. (%x:S. (inv' f) x) ` S = S *)
-by (asm_full_simp_tac (simpset() addsimps [inv_def]) 1);
-by (rtac equalityI 1);
-(* 2. <= *)
-by (Clarify_tac 1);
-by (afs [Inv_mem, BijE2] 1);
-(* 2. => *)
-by (rtac subsetI 1);
-by (res_inst_tac [("x","f x")] image_eqI 1);
-by (asm_simp_tac (simpset() addsimps [Inv_f_f, BijE1 RS funcset_mem]) 1);
-by (asm_simp_tac (simpset() addsimps [BijE1 RS funcset_mem]) 1);
-(* 3. *)
-by (rtac inj_onI 1);
-by (auto_tac (claset() addEs [Inv_injective], simpset()));
-qed "restrict_Inv_Bij";
-
-Addsimps [e'_def];
-
-Goal "e'\\<in>B ";
-by (rtac BijI 1);
-by (auto_tac (claset(), simpset() addsimps [funcsetI, inj_on_def]));
-qed "restrict_id_Bij";
-
-Goal "f \\<in> B ==> (%g:B. %x:S. (inv' g) x) f = (%x:S. (inv' f) x)";
-by (Asm_full_simp_tac 1);
-qed "eval_restrict_Inv";
-
-Goal "[| x \\<in> B; y \\<in> B|] ==> x o' y \\<in> B";
-by (simp_tac (simpset() addsimps [o'_def]) 1);
-by (rtac BijI 1);
-by (blast_tac (claset() addIs [funcset_compose] addDs [BijE1,BijE2,BijE3]) 1);
-by (blast_tac (claset() delrules [equalityI]
- addIs [surj_compose] addDs [BijE1,BijE2,BijE3]) 1);
-by (blast_tac (claset() addIs [inj_on_compose] addDs [BijE1,BijE2,BijE3]) 1);
-qed "compose_Bij";
-
-
-
-(**** Bijections form a group ****)
-
-
-Open_locale "bijgroup";
-
-val BG_def = thm "BG_def";
-
-Goal "[| x\\<in>B; y\\<in>B |] ==> (%g:B. %f:B. g o' f) x y = x o' y";
-by (Asm_full_simp_tac 1);
-qed "eval_restrict_comp2";
-
-
-Addsimps [BG_def, B_def, o'_def, inv'_def,e'_def];
-
-Goal "carrier BG == B";
-by (afs [BijGroup_def] 1);
-qed "BG_carrier";
-
-Goal "bin_op BG == %g:B. %f:B. g o' f";
-by (afs [BijGroup_def] 1);
-qed "BG_bin_op";
-
-Goal "inverse BG == %f:B. %x:S. (inv' f) x";
-by (afs [BijGroup_def] 1);
-qed "BG_inverse";
-
-Goal "unit BG == e'";
-by (afs [BijGroup_def] 1);
-qed "BG_unit";
-
-Goal "BG = (| carrier = BG.<cr>, bin_op = BG.<f>,\
-\ inverse = BG.<inv>, unit = BG.<e> |)";
-by (afs [BijGroup_def,BG_carrier, BG_bin_op, BG_inverse, BG_unit] 1);
-qed "BG_defI";
-
-Delsimps [B_def, BG_def, o'_def, inv'_def, e'_def];
-
-
-Goal "(%g:B. %f:B. g o' f) \\<in> B \\<rightarrow> B \\<rightarrow> B";
-by (simp_tac (simpset() addsimps [funcsetI, compose_Bij]) 1);
-qed "restrict_compose_Bij";
-
-
-Goal "BG \\<in> Group";
-by (stac BG_defI 1);
-by (rtac GroupI 1);
-(* 1. (BG .<f>)\\<in>(BG .<cr>) \\<rightarrow> (BG .<cr>) \\<rightarrow> (BG .<cr>) *)
-by (afs [BG_bin_op, BG_carrier, restrict_compose_Bij] 1);
-(* 2: (BG .<inv>)\\<in>(BG .<cr>) \\<rightarrow> (BG .<cr>) *)
-by (simp_tac (simpset() addsimps [BG_inverse, BG_carrier, restrict_Inv_Bij,
- funcsetI]) 1);
-by (afs [BG_inverse, BG_carrier,eval_restrict_Inv, restrict_Inv_Bij] 1);
-(* 3. *)
-by (afs [BG_carrier, BG_unit, restrict_id_Bij] 1);
-(* Now the equalities *)
-(* 4. ! x:BG .<cr>. (BG .<f>) ((BG .<inv>) x) x = (BG .<e>) *)
-by (simp_tac
- (simpset() addsimps [BG_carrier, BG_unit, BG_inverse, BG_bin_op,
- e'_def, compose_Inv_id, inv'_def, o'_def]) 1);
-by (simp_tac
- (simpset() addsimps [symmetric (inv'_def), restrict_Inv_Bij]) 1);
-(* 5: ! x:BG .<cr>. (BG .<f>) (BG .<e>) x = x *)
-by (simp_tac
- (simpset() addsimps [BG_carrier, BG_unit, BG_bin_op,
- e'_def, o'_def]) 1);
-by (simp_tac
- (simpset() addsimps [symmetric (e'_def), restrict_id_Bij]) 1);
-(* 6. ! x:BG .<cr>.
- ! y:BG .<cr>.
- ! z:BG .<cr>.
- (BG .<f>) ((BG .<f>) x y) z = (BG .<f>) x ((BG .<f>) y z) *)
-by (simp_tac
- (simpset() addsimps [BG_carrier, BG_unit, BG_inverse, BG_bin_op,
- compose_Bij]) 1);
-by (simp_tac (simpset() addsimps [o'_def]) 1);
-by (blast_tac (claset() addIs [compose_assoc RS sym, BijE1]) 1);
-qed "Bij_are_Group";
-
-Close_locale "bijgroup";
-Close_locale "bij";
-
--- a/src/HOL/GroupTheory/Bij.thy Wed Sep 25 11:23:26 2002 +0200
+++ b/src/HOL/GroupTheory/Bij.thy Thu Sep 26 10:40:13 2002 +0200
@@ -1,42 +1,131 @@
(* Title: HOL/GroupTheory/Bij
ID: $Id$
Author: Florian Kammueller, with new proofs by L C Paulson
- Copyright 1998-2001 University of Cambridge
-
-Bijections of a set and the group of bijections
- Sigma version with locales
*)
-Bij = Group +
+
+header{*Bijections of a Set, Permutation Groups, Automorphism Groups*}
+
+theory Bij = Group:
constdefs
Bij :: "'a set => (('a => 'a)set)"
- "Bij S == {f. f \\<in> S \\<rightarrow> S & f`S = S & inj_on f S}"
+ --{*Only extensional functions, since otherwise we get too many.*}
+ "Bij S == extensional S \<inter> {f. f`S = S & inj_on f S}"
+
+ BijGroup :: "'a set => (('a => 'a) group)"
+ "BijGroup S == (| carrier = Bij S,
+ sum = %g: Bij S. %f: Bij S. compose S g f,
+ gminus = %f: Bij S. %x: S. (Inv S f) x,
+ zero = %x: S. x |)"
+
+
+declare Id_compose [simp] compose_Id [simp]
+
+lemma Bij_imp_extensional: "f \<in> Bij S ==> f \<in> extensional S"
+by (simp add: Bij_def)
+
+lemma Bij_imp_funcset: "f \<in> Bij S ==> f \<in> S -> S"
+by (auto simp add: Bij_def Pi_def)
+
+lemma Bij_imp_apply: "f \<in> Bij S ==> f ` S = S"
+by (simp add: Bij_def)
+
+lemma Bij_imp_inj_on: "f \<in> Bij S ==> inj_on f S"
+by (simp add: Bij_def)
+
+lemma BijI: "[| f \<in> extensional(S); f`S = S; inj_on f S |] ==> f \<in> Bij S"
+by (simp add: Bij_def)
+
-constdefs
-BijGroup :: "'a set => (('a => 'a) grouptype)"
-"BijGroup S == (| carrier = Bij S,
- bin_op = %g: Bij S. %f: Bij S. compose S g f,
- inverse = %f: Bij S. %x: S. (Inv S f) x,
- unit = %x: S. x |)"
+subsection{*Bijections Form a Group*}
+
+lemma restrict_Inv_Bij: "f \<in> Bij S ==> (%x:S. (Inv S f) x) \<in> Bij S"
+apply (simp add: Bij_def)
+apply (intro conjI)
+txt{*Proving @{term "restrict (Inv S f) S ` S = S"}*}
+ apply (rule equalityI)
+ apply (force simp add: Inv_mem) --{*first inclusion*}
+ apply (rule subsetI) --{*second inclusion*}
+ apply (rule_tac x = "f x" in image_eqI)
+ apply (force intro: simp add: Inv_f_f)
+ apply blast
+txt{*Remaining goal: @{term "inj_on (restrict (Inv S f) S) S"}*}
+apply (rule inj_onI)
+apply (auto elim: Inv_injective)
+done
+
+lemma id_Bij: "(\<lambda>x\<in>S. x) \<in> Bij S "
+apply (rule BijI)
+apply (auto simp add: inj_on_def)
+done
+
+lemma compose_Bij: "[| x \<in> Bij S; y \<in> Bij S|] ==> compose S x y \<in> Bij S"
+apply (rule BijI)
+ apply (simp add: compose_extensional)
+ apply (blast del: equalityI
+ intro: surj_compose dest: Bij_imp_apply Bij_imp_inj_on)
+apply (blast intro: inj_on_compose dest: Bij_imp_apply Bij_imp_inj_on)
+done
-locale bij =
- fixes
- S :: "'a set"
- B :: "('a => 'a)set"
- comp :: "[('a => 'a),('a => 'a)]=>('a => 'a)" (infixr "o''" 80)
- inv' :: "('a => 'a)=>('a => 'a)"
- e' :: "('a => 'a)"
- defines
- B_def "B == Bij S"
- o'_def "g o' f == compose S g f"
- inv'_def "inv' f == Inv S f"
- e'_def "e' == (%x: S. x)"
+theorem group_BijGroup: "group (BijGroup S)"
+apply (simp add: group_def semigroup_def group_axioms_def
+ BijGroup_def restrictI compose_Bij restrict_Inv_Bij id_Bij)
+apply (auto intro!: compose_Bij)
+ apply (blast intro: compose_assoc [symmetric] Bij_imp_funcset)
+ apply (simp add: Bij_def compose_Inv_id)
+apply (simp add: Id_compose Bij_imp_funcset Bij_imp_extensional)
+done
+
+
+subsection{*Automorphisms Form a Group*}
+
+lemma Bij_Inv_mem: "[| f \<in> Bij S; x : S |] ==> Inv S f x : S"
+by (simp add: Bij_def Inv_mem)
+
+lemma Bij_Inv_lemma:
+ assumes eq: "!!x y. [|x \<in> S; y \<in> S|] ==> h(g x y) = g (h x) (h y)"
+ shows "[| h \<in> Bij S; g \<in> S \<rightarrow> S \<rightarrow> S; x \<in> S; y \<in> S |]
+ ==> Inv S h (g x y) = g (Inv S h x) (Inv S h y)"
+apply (simp add: Bij_def)
+apply (subgoal_tac "EX x':S. EX y':S. x = h x' & y = h y'")
+ apply clarify
+ apply (simp add: eq [symmetric] Inv_f_f funcset_mem [THEN funcset_mem], blast)
+done
+
+constdefs
+ auto :: "('a,'b)group_scheme => ('a => 'a)set"
+ "auto G == hom G G Int Bij (carrier G)"
-locale bijgroup = bij +
- fixes
- BG :: "('a => 'a) grouptype"
- defines
- BG_def "BG == BijGroup S"
+ AutoGroup :: "[('a,'c) group_scheme] => ('a=>'a) group"
+ "AutoGroup G == BijGroup (carrier G) (|carrier := auto G |)"
+
+lemma id_in_auto: "group G ==> (%x: carrier G. x) \<in> auto G"
+by (simp add: auto_def hom_def restrictI semigroup.sum_closed
+ group.axioms id_Bij)
+
+lemma restrict_Inv_hom:
+ "[|group G; h \<in> hom G G; h \<in> Bij (carrier G)|]
+ ==> restrict (Inv (carrier G) h) (carrier G) \<in> hom G G"
+by (simp add: hom_def Bij_Inv_mem restrictI semigroup.sum_closed
+ semigroup.sum_funcset group.axioms Bij_Inv_lemma)
+
+lemma subgroup_auto:
+ "group G ==> subgroup (auto G) (BijGroup (carrier G))"
+apply (rule group.subgroupI)
+ apply (rule group_BijGroup)
+ apply (force simp add: auto_def BijGroup_def)
+ apply (blast intro: dest: id_in_auto)
+ apply (simp add: auto_def BijGroup_def restrict_Inv_Bij
+ restrict_Inv_hom)
+apply (simp add: auto_def BijGroup_def compose_Bij)
+apply (simp add: hom_def compose_def Pi_def group.axioms)
+done
+
+theorem AutoGroup: "group G ==> group (AutoGroup G)"
+apply (drule subgroup_auto)
+apply (simp add: subgroup_def AutoGroup_def)
+done
+
end
--- a/src/HOL/GroupTheory/Coset.ML Wed Sep 25 11:23:26 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,422 +0,0 @@
-(* Title: HOL/GroupTheory/Coset
- ID: $Id$
- Author: Florian Kammueller, with new proofs by L C Paulson
- Copyright 1998-2001 University of Cambridge
-
-Theory of cosets, using locales
-*)
-
-(** these versions are useful for Sylow's Theorem **)
-
-Goal "[|finite A; finite B; \\<exists>f \\<in> A\\<rightarrow>B. inj_on f A|] ==> card(A) <= card(B)";
-by (Clarify_tac 1);
-by (rtac card_inj_on_le 1);
-by (auto_tac (claset(), simpset() addsimps [Pi_def]));
-qed "card_inj";
-
-Goal "[| finite A; finite B; \\<exists>f \\<in> A\\<rightarrow>B. inj_on f A; \
-\ \\<exists>g \\<in> B\\<rightarrow>A. inj_on g B |] ==> card(A) = card(B)";
-by (Clarify_tac 1);
-by (rtac card_bij_eq 1);
-by (auto_tac (claset(), simpset() addsimps [Pi_def]));
-qed "card_bij";
-
-
-
-Open_locale "coset";
-Addsimps [Group_G, simp_G];
-
-val rcos_def = thm "rcos_def";
-val lcos_def = thm "lcos_def";
-val setprod_def = thm "setprod_def";
-val setinv_def = thm "setinv_def";
-val setrcos_def = thm "setrcos_def";
-
-val group_defs = [thm "binop_def", thm "inv_def", thm "e_def"];
-val coset_defs = [thm "rcos_def", thm "lcos_def", thm "setprod_def"];
-
-(** Alternative definitions, reducing to locale constants **)
-
-Goal "H #> a = {b . \\<exists>h\\<in>H. h ## a = b}";
-by (auto_tac (claset(),
- simpset() addsimps [rcos_def, r_coset_def, binop_def]));
-qed "r_coset_eq";
-
-Goal "a <# H = {b . \\<exists>h\\<in>H. a ## h = b}";
-by (auto_tac (claset(),
- simpset() addsimps [lcos_def, l_coset_def, binop_def]));
-qed "l_coset_eq";
-
-Goal "{*H*} = {C . \\<exists>a\\<in>carrier G. C = H #> a}";
-by (auto_tac (claset(),
- simpset() addsimps [set_r_cos_def, setrcos_def, rcos_def, binop_def]));
-qed "setrcos_eq";
-
-Goal "H <#> K = {c . \\<exists>h\\<in>H. \\<exists>k\\<in>K. c = h ## k}";
-by (simp_tac
- (simpset() addsimps [setprod_def, set_prod_def, binop_def, image_def]) 1);
-qed "set_prod_eq";
-
-Goal "[| M <= carrier G; g\\<in>carrier G; h\\<in>carrier G |] \
-\ ==> (M #> g) #> h = M #> (g ## h)";
-by (force_tac (claset(), simpset() addsimps [r_coset_eq, binop_assoc]) 1);
-qed "coset_mul_assoc";
-
-Goal "[| M <= carrier G |] ==> M #> e = M";
-by (force_tac (claset(), simpset() addsimps [r_coset_eq]) 1);
-qed "coset_mul_e";
-
-Goal "[| M #> (x ## (i y)) = M; x \\<in> carrier G ; y \\<in> carrier G;\
-\ M <= carrier G |] ==> M #> x = M #> y";
-by (eres_inst_tac [("P","%z. M #> x = z #> y")] subst 1);
-by (asm_simp_tac (simpset() addsimps [coset_mul_assoc, binop_assoc]) 1);
-qed "coset_mul_inv1";
-
-Goal "[| M #> x = M #> y; x \\<in> carrier G; y \\<in> carrier G; M <= carrier G |] \
-\ ==> M #> (x ## (i y)) = M ";
-by (afs [coset_mul_assoc RS sym] 1);
-by (afs [coset_mul_assoc, coset_mul_e] 1);
-qed "coset_mul_invers2";
-
-Goal "[| H #> x = H; x \\<in> carrier G; H <<= G |] ==> x\\<in>H";
-by (etac subst 1);
-by (simp_tac (simpset() addsimps [r_coset_eq]) 1);
-by (blast_tac (claset() addIs [e_ax1, subgroup_e_closed]) 1);
-qed "coset_join1";
-
-Goal "[| x\\<in>carrier G; H <<= G; x\\<in>H |] ==> H #> x = H";
-by (auto_tac (claset(), simpset() addsimps [r_coset_eq]));
-by (res_inst_tac [("x","xa ## (i x)")] bexI 2);
-by (auto_tac (claset(),
- simpset() addsimps [subgroup_f_closed, subgroup_inv_closed,
- binop_assoc, subgroup_imp_subset RS subsetD]));
-qed "coset_join2";
-
-Goal "[| H <= carrier G; x\\<in>carrier G |] ==> H #> x <= carrier G";
-by (auto_tac (claset(), simpset() addsimps [r_coset_eq]));
-qed "r_coset_subset_G";
-
-Goal "[| h \\<in> H; H <= carrier G; x \\<in> carrier G|] ==> h ## x \\<in> H #> x";
-by (auto_tac (claset(), simpset() addsimps [r_coset_eq]));
-qed "rcosI";
-
-Goal "[| H <= carrier G; x \\<in> carrier G |] ==> H #> x \\<in> {*H*}";
-by (auto_tac (claset(), simpset() addsimps [setrcos_eq]));
-qed "setrcosI";
-
-
-Goal "[| x ## y = z; x \\<in> carrier G; y \\<in> carrier G; z\\<in>carrier G |] \
-\ ==> (i x) ## z = y";
-by (Clarify_tac 1);
-by (asm_simp_tac (simpset() addsimps [binop_assoc RS sym]) 1);
-qed "transpose_inv";
-
-
-Goal "[| y \\<in> H #> x; x \\<in> carrier G; H <<= G |] ==> H #> x = H #> y";
-by (auto_tac (claset(),
- simpset() addsimps [r_coset_eq, binop_assoc RS sym,
- right_cancellation_iff, subgroup_imp_subset RS subsetD,
- subgroup_f_closed]));
-by (res_inst_tac [("x","ha ## i h")] bexI 1);
-by (auto_tac (claset(),
- simpset() addsimps [binop_assoc, subgroup_imp_subset RS subsetD,
- subgroup_inv_closed, subgroup_f_closed]));
-qed "repr_independence";
-
-Goal "[| x \\<in> carrier G; H <<= G |] ==> x \\<in> H #> x";
-by (simp_tac (simpset() addsimps [r_coset_eq]) 1);
-by (blast_tac (claset() addIs [e_ax1, subgroup_imp_subset RS subsetD,
- subgroup_e_closed]) 1);
-qed "rcos_self";
-
-Goal "setinv H = INV`H";
-by (simp_tac
- (simpset() addsimps [image_def, setinv_def, set_inv_def, inv_def]) 1);
-qed "setinv_eq_image_inv";
-
-
-(*** normal subgroups ***)
-
-Goal "(H <| G) = (H <<= G & (\\<forall>x \\<in> carrier G. H #> x = x <# H))";
-by (afs [thm "lcos_def", thm "rcos_def", normal_def] 1);
-qed "normal_iff";
-
-Goal "H <| G ==> H <<= G";
-by (afs [normal_def] 1);
-qed "normal_imp_subgroup";
-
-Goal "[| H <| G; x \\<in> carrier G |] ==> H #> x = x <# H";
-by (afs [thm "lcos_def", thm "rcos_def", normal_def] 1);
-qed "normal_imp_rcos_eq_lcos";
-
-Goal "\\<lbrakk>H \\<lhd> G; x \\<in> (G .<cr>); h \\<in> H\\<rbrakk> \\<Longrightarrow> i x ## h ## x \\<in> H";
-by (auto_tac (claset(),
- simpset() addsimps [l_coset_eq, r_coset_eq, normal_iff]));
-by (ball_tac 1);
-by (dtac (equalityD1 RS subsetD) 1);
-by (Blast_tac 1);
-by (Clarify_tac 1);
-by (etac subst 1);
-by (asm_simp_tac
- (simpset() addsimps [binop_assoc RS sym, subgroup_imp_subset RS subsetD]) 1);
-qed "normal_inv_op_closed1";
-
-Goal "\\<lbrakk>H \\<lhd> G; x \\<in> (G .<cr>); h \\<in> H\\<rbrakk> \\<Longrightarrow> x ## h ## i x \\<in> H";
-by (dres_inst_tac [("x","i x")] normal_inv_op_closed1 1);
-by Auto_tac;
-qed "normal_inv_op_closed2";
-
-Goal "[| M <= carrier G; g\\<in>carrier G; h\\<in>carrier G |] \
-\ ==> g <# (h <# M) = (g ## h) <# M";
-by (force_tac (claset(), simpset() addsimps [l_coset_eq, binop_assoc]) 1);
-qed "lcos_mul_assoc";
-
-Goal "M <= carrier G ==> e <# M = M";
-by (force_tac (claset(), simpset() addsimps [l_coset_eq]) 1);
-qed "lcos_mul_e";
-
-Goal "[| H <= carrier G; x\\<in>carrier G |]\
-\ ==> x <# H <= carrier G";
-by (auto_tac (claset(), simpset() addsimps [l_coset_eq, subsetD]));
-qed "lcosetGaH_subset_G";
-
-Goal "[| y \\<in> x <# H; x \\<in> carrier G; H <<= G |] ==> x <# H = y <# H";
-by (auto_tac (claset(),
- simpset() addsimps [l_coset_eq, binop_assoc,
- left_cancellation_iff, subgroup_imp_subset RS subsetD,
- subgroup_f_closed]));
-by (res_inst_tac [("x","i h ## ha")] bexI 1);
-by (auto_tac (claset(),
- simpset() addsimps [binop_assoc RS sym, subgroup_imp_subset RS subsetD,
- subgroup_inv_closed, subgroup_f_closed]));
-qed "l_repr_independence";
-
-Goal "[| H1 <= carrier G; H2 <= carrier G |] ==> H1 <#> H2 <= carrier G";
-by (auto_tac (claset(), simpset() addsimps [set_prod_eq, subsetD]));
-qed "setprod_subset_G";
-val set_prod_subset_G = export setprod_subset_G;
-
-Goal "H <<= G ==> H <#> H = H";
-by (auto_tac (claset(),
- simpset() addsimps [set_prod_eq, Sigma_def,image_def]));
-by (res_inst_tac [("x","x")] bexI 2);
-by (res_inst_tac [("x","e")] bexI 2);
-by (auto_tac (claset(),
- simpset() addsimps [subgroup_f_closed, subgroup_e_closed, e_ax2,
- subgroup_imp_subset RS subsetD]));
-qed "subgroup_prod_id";
-val Subgroup_prod_id = export subgroup_prod_id;
-
-
-(* set of inverses of an r_coset *)
-Goal "[| H <| G; x \\<in> carrier G |] ==> I(H #> x) = H #>(i x)";
-by (ftac normal_imp_subgroup 1);
-by (auto_tac (claset(),
- simpset() addsimps [r_coset_eq, setinv_eq_image_inv, image_def]));
-by (res_inst_tac [("x","i x ## i h ## x")] bexI 1);
-by (asm_simp_tac (simpset() addsimps [binop_assoc, inv_prod,
- subgroup_imp_subset RS subsetD]) 1);
-by (res_inst_tac [("x","i(h ## i x)")] exI 2);
-by (asm_simp_tac (simpset() addsimps [inv_inv, inv_prod,
- subgroup_imp_subset RS subsetD]) 2);
-by (res_inst_tac [("x","x ## i h ## i x")] bexI 2);
-by (auto_tac (claset(),
- simpset() addsimps [normal_inv_op_closed1, normal_inv_op_closed2,
- binop_assoc, subgroup_imp_subset RS subsetD,
- subgroup_inv_closed]));
-qed "rcos_inv";
-val r_coset_inv = export rcos_inv;
-
-Goal "[| H <| G; H1\\<in>{*H*}; x \\<in> H1 |] ==> I(H1) = H #> (i x)";
-by (afs [setrcos_eq] 1);
-by (Clarify_tac 1);
-by (subgoal_tac "x : carrier G" 1);
- by (rtac subsetD 2);
- by (assume_tac 3);
- by (asm_full_simp_tac (simpset() addsimps [r_coset_subset_G,
- subgroup_imp_subset,normal_imp_subgroup]) 2);
-by (dtac repr_independence 1);
- by (assume_tac 1);
- by (etac normal_imp_subgroup 1);
-by (asm_simp_tac (simpset() addsimps [rcos_inv]) 1);
-qed "rcos_inv2";
-val r_coset_inv2 = export rcos_inv2;
-
-
-
-(* some rules for <#> with #> or <# *)
-Goal "[| H1 <= carrier G; H2 <= carrier G; x \\<in> carrier G |]\
-\ ==> H1 <#> (H2 #> x) = (H1 <#> H2) #> x";
-by (auto_tac (claset(),
- simpset() addsimps [rcos_def, r_coset_def,
- setprod_def, set_prod_def, Sigma_def,image_def]));
-by (auto_tac (claset() addSIs [bexI,exI],
- simpset() addsimps [binop_assoc, subsetD]));
-qed "setprod_rcos_assoc";
-val set_prod_r_coset_assoc = export setprod_rcos_assoc;
-
-Goal "[| H1 <= carrier G; H2 <= carrier G; x \\<in> carrier G |]\
-\ ==> (H1 #> x) <#> H2 = H1 <#> (x <# H2)";
-by (asm_simp_tac
- (simpset() addsimps [rcos_def, r_coset_def, lcos_def, l_coset_def,
- setprod_def, set_prod_def, Sigma_def,image_def]) 1);
-by (force_tac (claset() addSIs [bexI,exI],
- simpset() addsimps [binop_assoc, subsetD]) 1);
-qed "rcos_prod_assoc_lcos";
-val rcoset_prod_assoc_lcoset = export rcos_prod_assoc_lcos;
-
-
-(* product of rcosets *)
-(* To show H x H y = H x y. which is done by
- H x H y =1= H (x H) y =2= H (H x) y =3= H H x y =4= H x y *)
-
-Goal "[| H <| G; x \\<in> carrier G; y \\<in> carrier G |]\
-\ ==> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y";
-by (afs [setprod_rcos_assoc, normal_imp_subgroup RS subgroup_imp_subset, r_coset_subset_G,
- lcosetGaH_subset_G, rcos_prod_assoc_lcos] 1);
-qed "rcos_prod_step1";
-
-Goal "[| H <| G; x \\<in> carrier G; y \\<in> carrier G |]\
-\ ==> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y";
-by (afs [normal_imp_rcos_eq_lcos] 1);
-qed "rcos_prod_step2";
-
-Goal "[| H <| G; x \\<in> carrier G; y \\<in> carrier G |]\
-\ ==> (H <#> (H #> x)) #> y = H #> (x ## y)";
-by (afs [setprod_rcos_assoc,normal_imp_subgroup RS subgroup_imp_subset,
- r_coset_subset_G, coset_mul_assoc, setprod_subset_G,
- normal_imp_subgroup RS subgroup_imp_subset,subgroup_prod_id,
- normal_imp_subgroup] 1);
-qed "rcos_prod_step3";
-
-Goal "[| H <| G; x \\<in> carrier G; y \\<in> carrier G |]\
-\ ==> (H #> x) <#> (H #> y) = H #> (x ## y)";
-by (afs [rcos_prod_step1,rcos_prod_step2,rcos_prod_step3] 1);
-qed "rcos_prod";
-val rcoset_prod = export rcos_prod;
-
-(* operations on cosets *)
-Goal "[| H <| G; H1 \\<in> {*H*}; H2 \\<in> {*H*} |] ==> H1 <#> H2 \\<in> {*H*}";
-by (auto_tac (claset(),
- simpset() addsimps [normal_imp_subgroup RS subgroup_imp_subset,
- rcos_prod, setrcos_eq]));
-qed "setprod_closed";
-
-Goal "[| H <| G; H1 \\<in> {*H*} |] ==> I(H1) \\<in> {*H*}";
-by (auto_tac (claset(),
- simpset() addsimps [normal_imp_subgroup RS subgroup_imp_subset,
- rcos_inv, setrcos_eq]));
-qed "setinv_closed";
-
-Goal "H <<= G ==> H \\<in> {*H*}";
-by (simp_tac (simpset() addsimps [setrcos_eq]) 1);
-by (blast_tac (claset() delrules [equalityI]
- addSIs [subgroup_e_closed, e_closed, coset_join2 RS sym]) 1);
-qed "setrcos_unit_closed";
-
-Goal "[|H <| G; M \\<in> {*H*}|] ==> I M <#> M = H";
-by (asm_full_simp_tac (simpset() addsimps [setrcos_eq]) 1);
-by (Clarify_tac 1);
-by (asm_simp_tac
- (simpset() addsimps [rcos_inv, rcos_prod, normal_imp_subgroup,
- subgroup_imp_subset, coset_mul_e]) 1);
-qed "setrcos_inv_prod_eq";
-
-(*generalizes subgroup_prod_id*)
-Goal "[|H <| G; M \\<in> {*H*}|] ==> H <#> M = M";
-by (asm_full_simp_tac (simpset() addsimps [setrcos_eq]) 1);
-by (Clarify_tac 1);
-by (asm_simp_tac
- (simpset() addsimps [normal_imp_subgroup, subgroup_imp_subset,
- setprod_rcos_assoc, subgroup_prod_id]) 1);
-qed "setrcos_prod_eq";
-
-Goal "[|H <| G; M1 \\<in> {*H*}; M2 \\<in> {*H*}; M3 \\<in> {*H*}|] \
-\ ==> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)";
-by (asm_full_simp_tac (simpset() addsimps [setrcos_eq]) 1);
-by (Clarify_tac 1);
-by (asm_simp_tac
- (simpset() addsimps [rcos_prod, normal_imp_subgroup,
- subgroup_imp_subset, binop_assoc]) 1);
-qed "setrcos_prod_assoc";
-
-
-(**** back to Sylow again, i.e. direction Lagrange ****)
-
-(* Theorems necessary for Lagrange *)
-
-Goal "H <<= G ==> \\<Union> {*H*} = carrier G";
-by (rtac equalityI 1);
-by (force_tac (claset(),
- simpset() addsimps [subgroup_imp_subset RS subsetD, setrcos_eq, r_coset_eq]) 1);
-by (auto_tac (claset(),
- simpset() addsimps [setrcos_eq, subgroup_imp_subset, rcos_self]));
-qed "setrcos_part_G";
-
-Goal "[| c \\<in> {*H*}; H <= carrier G; finite (carrier G) |] ==> finite c";
-by (auto_tac (claset(), simpset() addsimps [setrcos_eq]));
-by (asm_simp_tac (simpset() addsimps [r_coset_subset_G RS finite_subset]) 1);
-qed "cosets_finite";
-
-Goal "[| c \\<in> {*H*}; H <= carrier G; finite(carrier G) |] ==> card c = card H";
-by (auto_tac (claset(), simpset() addsimps [setrcos_eq]));
-by (res_inst_tac [("f", "%y. y ## i a"), ("g","%y. y ## a")] card_bij_eq 1);
-by (afs [r_coset_subset_G RS finite_subset] 1);
-by (blast_tac (claset() addIs [finite_subset]) 1);
-(* injective maps *)
- by (blast_tac (claset() addIs [restrictI, rcosI]) 3);
- by (force_tac (claset(),
- simpset() addsimps [inj_on_def, right_cancellation_iff, subsetD]) 3);
-(*now for f*)
- by (force_tac (claset(),
- simpset() addsimps [binop_assoc, subsetD, r_coset_eq]) 1);
-(* injective *)
-by (rtac inj_onI 1);
-by (subgoal_tac "x \\<in> carrier G & y \\<in> carrier G" 1);
- by (blast_tac (claset() addIs [r_coset_subset_G RS subsetD]) 2);
-by (rotate_tac ~1 1);
-by (asm_full_simp_tac
- (simpset() addsimps [right_cancellation_iff, subsetD]) 1);
-qed "card_cosets_equal";
-
-
-(** Two distinct right cosets are disjoint **)
-
-Goal "[|H <<= G; a \\<in> (G .<cr>); b \\<in> (G .<cr>); ha ## a = h ## b; \
-\ h \\<in> H; ha \\<in> H; hb \\<in> H|] \
-\ ==> \\<exists>h\\<in>H. h ## b = hb ## a";
-by (res_inst_tac [("x","hb ## ((i ha) ## h)")] bexI 1);
-by (afs [subgroup_f_closed, subgroup_inv_closed] 2);
-by (asm_simp_tac (simpset() addsimps [binop_assoc, left_cancellation_iff,
- transpose_inv, subgroup_imp_subset RS subsetD]) 1);
-qed "rcos_equation";
-
-Goal "[|H <<= G; c1 \\<in> {*H*}; c2 \\<in> {*H*}; c1 \\<noteq> c2|] ==> c1 \\<inter> c2 = {}";
-by (asm_full_simp_tac (simpset() addsimps [setrcos_eq, r_coset_eq]) 1);
-by (blast_tac (claset() addIs [rcos_equation, sym]) 1);
-qed "rcos_disjoint";
-
-Goal "H <<= G ==> {*H*} <= Pow(carrier G)";
-by (simp_tac (simpset() addsimps [setrcos_eq]) 1);
-by (blast_tac (claset() addDs [r_coset_subset_G,subgroup_imp_subset]) 1);
-qed "setrcos_subset_PowG";
-
-Goal "[| finite(carrier G); H <<= G |]\
-\ ==> card({*H*}) * card(H) = order(G)";
-by (asm_simp_tac (simpset() addsimps [order_def, setrcos_part_G RS sym]) 1);
-by (stac mult_commute 1);
-by (rtac card_partition 1);
-by (asm_full_simp_tac
- (simpset() addsimps [setrcos_subset_PowG RS finite_subset]) 1);
-by (asm_full_simp_tac (simpset() addsimps [setrcos_part_G]) 1);
-by (asm_full_simp_tac
- (simpset() addsimps [card_cosets_equal, subgroup_def]) 1);
-by (asm_full_simp_tac (simpset() addsimps [rcos_disjoint, subgroup_def]) 1);
-qed "lagrange";
-val Lagrange = export lagrange;
-
-Close_locale "coset";
-Close_locale "group";
-
-
-
--- a/src/HOL/GroupTheory/Coset.thy Wed Sep 25 11:23:26 2002 +0200
+++ b/src/HOL/GroupTheory/Coset.thy Thu Sep 26 10:40:13 2002 +0200
@@ -1,58 +1,436 @@
(* 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 +
+header{*Theory of Cosets*}
+
+theory 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"
+ r_coset :: "[('a,'b) group_scheme,'a set, 'a] => 'a set"
+ "r_coset G H a == (% x. (sum G) x a) ` H"
+
+ l_coset :: "[('a,'b) group_scheme, 'a, 'a set] => 'a set"
+ "l_coset G a H == (% x. (sum G) a x) ` H"
+
+ rcosets :: "[('a,'b) group_scheme,'a set] => ('a set)set"
+ "rcosets G H == r_coset G H ` (carrier G)"
+
+ set_sum :: "[('a,'b) group_scheme,'a set,'a set] => 'a set"
+ "set_sum G H K == (%(x,y). (sum G) x y) ` (H \<times> K)"
+
+ set_minus :: "[('a,'b) group_scheme,'a set] => 'a set"
+ "set_minus G H == (gminus G) ` H"
+
+ normal :: "['a set, ('a,'b) group_scheme] => bool" (infixl "<|" 60)
+ "normal H G == subgroup H G &
+ (\<forall>x \<in> carrier G. r_coset G H x = l_coset G x H)"
+
+syntax (xsymbols)
+ normal :: "['a set, ('a,'b) group_scheme] => bool" (infixl "\<lhd>" 60)
+
+locale coset = group G +
+ fixes rcos :: "['a set, 'a] => 'a set" (infixl "#>" 60)
+ and lcos :: "['a, 'a set] => 'a set" (infixl "<#" 60)
+ and setsum :: "['a set, 'a set] => 'a set" (infixl "<#>" 60)
+ defines rcos_def: "H #> x == r_coset G H x"
+ and lcos_def: "x <# H == l_coset G x H"
+ and setsum_def: "H <#> K == set_sum G H K"
+
+
+text{*Lemmas useful for Sylow's Theorem*}
+
+lemma card_inj:
+ "[|f \<in> A\<rightarrow>B; inj_on f A; finite A; finite B|] ==> card(A) <= card(B)"
+apply (rule card_inj_on_le)
+apply (auto simp add: Pi_def)
+done
+
+lemma card_bij:
+ "[|f \<in> A\<rightarrow>B; inj_on f A;
+ g \<in> B\<rightarrow>A; inj_on g B; finite A; finite B|] ==> card(A) = card(B)"
+by (blast intro: card_inj order_antisym)
+
+
+subsection{*Lemmas Using Locale Constants*}
+
+lemma (in coset) r_coset_eq: "H #> a = {b . \<exists>h\<in>H. h \<oplus> a = b}"
+by (auto simp add: rcos_def r_coset_def sum_def)
- l_coset :: "['a grouptype, 'a, 'a set] => 'a set"
- "l_coset G a H == (% x. (bin_op G) a x) ` H"
+lemma (in coset) l_coset_eq: "a <# H = {b . \<exists>h\<in>H. a \<oplus> h = b}"
+by (auto simp add: lcos_def l_coset_def sum_def)
+
+lemma (in coset) setrcos_eq: "rcosets G H = {C . \<exists>a\<in>carrier G. C = H #> a}"
+by (auto simp add: rcosets_def rcos_def sum_def)
+
+lemma (in coset) set_sum_eq: "H <#> K = {c . \<exists>h\<in>H. \<exists>k\<in>K. c = h \<oplus> k}"
+by (simp add: setsum_def set_sum_def sum_def image_def)
+
+lemma (in coset) coset_sum_assoc:
+ "[| M <= carrier G; g \<in> carrier G; h \<in> carrier G |]
+ ==> (M #> g) #> h = M #> (g \<oplus> h)"
+by (force simp add: r_coset_eq sum_assoc)
+
+lemma (in coset) coset_sum_zero [simp]: "M <= carrier G ==> M #> \<zero> = M"
+by (force simp add: r_coset_eq)
+
+lemma (in coset) coset_sum_minus1:
+ "[| M #> (x \<oplus> (\<ominus>y)) = M; x \<in> carrier G ; y \<in> carrier G;
+ M <= carrier G |] ==> M #> x = M #> y"
+apply (erule subst [of concl: "%z. M #> x = z #> y"])
+apply (simp add: coset_sum_assoc sum_assoc)
+done
- set_r_cos :: "['a grouptype,'a set] => ('a set)set"
- "set_r_cos G H == r_coset G H ` (carrier G)"
+lemma (in coset) coset_sum_minus2:
+ "[| M #> x = M #> y; x \<in> carrier G; y \<in> carrier G; M <= carrier G |]
+ ==> M #> (x \<oplus> (\<ominus>y)) = M "
+apply (simp add: coset_sum_assoc [symmetric])
+apply (simp add: coset_sum_assoc)
+done
+
+lemma (in coset) coset_join1:
+ "[| H #> x = H; x \<in> carrier G; subgroup H G |] ==> x\<in>H"
+apply (erule subst)
+apply (simp add: r_coset_eq)
+apply (blast intro: left_zero subgroup_zero_closed)
+done
+
+text{*FIXME: locales don't currently work with @{text rule_tac}, so we
+must prove this lemma separately.*}
+lemma (in coset) solve_equation:
+ "\<lbrakk>subgroup H G; x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. h \<oplus> x = y"
+apply (rule bexI [of _ "y \<oplus> (\<ominus>x)"])
+apply (auto simp add: subgroup_sum_closed subgroup_minus_closed sum_assoc
+ subgroup_imp_subset [THEN subsetD])
+done
+
+lemma (in coset) coset_join2:
+ "[| x \<in> carrier G; subgroup H G; x\<in>H |] ==> H #> x = H"
+by (force simp add: subgroup_sum_closed r_coset_eq solve_equation)
- 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"
+lemma (in coset) r_coset_subset_G:
+ "[| H <= carrier G; x \<in> carrier G |] ==> H #> x <= carrier G"
+by (auto simp add: r_coset_eq)
+
+lemma (in coset) rcosI:
+ "[| h \<in> H; H <= carrier G; x \<in> carrier G|] ==> h \<oplus> x \<in> H #> x"
+by (auto simp add: r_coset_eq)
+
+lemma (in coset) setrcosI:
+ "[| H <= carrier G; x \<in> carrier G |] ==> H #> x \<in> rcosets G H"
+by (auto simp add: setrcos_eq)
+
+
+text{*Really needed?*}
+lemma (in coset) transpose_minus:
+ "[| x \<oplus> y = z; x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |]
+ ==> (\<ominus>x) \<oplus> z = y"
+by (force simp add: sum_assoc [symmetric])
+
+lemma (in coset) repr_independence:
+ "[| y \<in> H #> x; x \<in> carrier G; subgroup H G |] ==> H #> x = H #> y"
+by (auto simp add: r_coset_eq sum_assoc [symmetric] right_cancellation_iff
+ subgroup_imp_subset [THEN subsetD]
+ subgroup_sum_closed solve_equation)
+
+lemma (in coset) rcos_self: "[| x \<in> carrier G; subgroup H G |] ==> x \<in> H #> x"
+apply (simp add: r_coset_eq)
+apply (blast intro: left_zero subgroup_imp_subset [THEN subsetD]
+ subgroup_zero_closed)
+done
+
+
+subsection{*normal subgroups*}
+
+text{*Allows use of theorems proved in the locale coset*}
+lemma subgroup_imp_coset: "subgroup H G ==> coset G"
+apply (drule subgroup_imp_group)
+apply (simp add: group_def coset_def)
+done
+
+lemma normal_imp_subgroup: "H <| G ==> subgroup H G"
+by (simp add: normal_def)
+
+lemmas normal_imp_group = normal_imp_subgroup [THEN subgroup_imp_group]
+lemmas normal_imp_coset = normal_imp_subgroup [THEN subgroup_imp_coset]
+
+lemma (in coset) normal_iff:
+ "(H <| G) = (subgroup H G & (\<forall>x \<in> carrier G. H #> x = x <# H))"
+by (simp add: lcos_def rcos_def normal_def)
- 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)}"
+lemma (in coset) normal_imp_rcos_eq_lcos:
+ "[| H <| G; x \<in> carrier G |] ==> H #> x = x <# H"
+by (simp add: lcos_def rcos_def normal_def)
+
+lemma (in coset) normal_minus_op_closed1:
+ "\<lbrakk>H \<lhd> G; x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (\<ominus>x) \<oplus> h \<oplus> x \<in> H"
+apply (auto simp add: l_coset_eq r_coset_eq normal_iff)
+apply (drule bspec, assumption)
+apply (drule equalityD1 [THEN subsetD], blast, clarify)
+apply (simp add: sum_assoc subgroup_imp_subset [THEN subsetD])
+apply (erule subst)
+apply (simp add: sum_assoc [symmetric] subgroup_imp_subset [THEN subsetD])
+done
+
+lemma (in coset) normal_minus_op_closed2:
+ "\<lbrakk>H \<lhd> G; x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> x \<oplus> h \<oplus> (\<ominus>x) \<in> H"
+apply (drule normal_minus_op_closed1 [of H "(\<ominus>x)"])
+apply auto
+done
+
+lemma (in coset) lcos_sum_assoc:
+ "[| M <= carrier G; g \<in> carrier G; h \<in> carrier G |]
+ ==> g <# (h <# M) = (g \<oplus> h) <# M"
+by (force simp add: l_coset_eq sum_assoc)
+
+lemma (in coset) lcos_sum_zero: "M <= carrier G ==> \<zero> <# M = M"
+by (force simp add: l_coset_eq)
+
+lemma (in coset) l_coset_subset_G:
+ "[| H <= carrier G; x \<in> carrier G |] ==> x <# H <= carrier G"
+by (auto simp add: l_coset_eq subsetD)
+
+lemma (in coset) l_repr_independence:
+ "[| y \<in> x <# H; x \<in> carrier G; subgroup H G |] ==> x <# H = y <# H"
+apply (auto simp add: l_coset_eq sum_assoc left_cancellation_iff
+ subgroup_imp_subset [THEN subsetD] subgroup_sum_closed)
+apply (rule_tac x = "sum G (gminus G h) ha" in bexI)
+ --{*FIXME: locales don't currently work with @{text rule_tac},
+ want @{term "(\<ominus>h) \<oplus> ha"}*}
+apply (auto simp add: sum_assoc [symmetric] subgroup_imp_subset [THEN subsetD]
+ subgroup_minus_closed subgroup_sum_closed)
+done
+
+lemma (in coset) setsum_subset_G:
+ "[| H <= carrier G; K <= carrier G |] ==> H <#> K <= carrier G"
+by (auto simp add: set_sum_eq subsetD)
+
+lemma (in coset) subgroup_sum_id: "subgroup H G ==> H <#> H = H"
+apply (auto simp add: subgroup_sum_closed set_sum_eq Sigma_def image_def)
+apply (rule_tac x = x in bexI)
+apply (rule bexI [of _ "\<zero>"])
+apply (auto simp add: subgroup_sum_closed subgroup_zero_closed
+ right_zero subgroup_imp_subset [THEN subsetD])
+done
-syntax
- "@NS" :: "['a set, 'a grouptype] => bool" ("_ <| _" [60,61]60)
+(* set of inverses of an r_coset *)
+lemma (in coset) rcos_minus:
+ "[| H <| G; x \<in> carrier G |] ==> set_minus G (H #> x) = H #> (\<ominus>x)"
+apply (frule normal_imp_subgroup)
+apply (auto simp add: r_coset_eq image_def set_minus_def)
+(*FIXME: I can't say
+apply (rule_tac x = "(\<ominus>x) \<oplus> (\<ominus>h) \<oplus> x" in bexI)
+*)
+apply (rule rev_bexI [OF normal_minus_op_closed1 [of concl: x]])
+apply (rule_tac [3] subgroup_minus_closed, assumption+)
+apply (simp add: sum_assoc minus_sum subgroup_imp_subset [THEN subsetD])
+(*FIXME: I can't say
+apply (rule_tac x = "\<ominus> (h \<oplus> (\<ominus>x)) " in exI)
+*)
+apply (rule_tac x = "gminus G (sum G h (gminus G x))" in exI)
+apply (simp add: minus_sum subgroup_imp_subset [THEN subsetD])
+(*FIXME: I can't say
+apply (rule_tac x = "x \<oplus> (\<ominus>h) \<oplus> (\<ominus>x)" in bexI)
+*)
+apply (rule_tac x = "sum G (sum G x (gminus G h)) (gminus G x)" in bexI)
+apply (simp add: sum_assoc subgroup_imp_subset [THEN subsetD])
+apply (simp add: normal_minus_op_closed2 subgroup_minus_closed)
+done
+
+lemma (in coset) rcos_minus2:
+ "[| H <| G; K \<in> rcosets G H; x \<in> K |] ==> set_minus G K = H #> (\<ominus>x)"
+apply (simp add: setrcos_eq, clarify)
+apply (subgoal_tac "x : carrier G")
+ prefer 2
+ apply (blast dest: r_coset_subset_G subgroup_imp_subset normal_imp_subgroup)
+apply (drule repr_independence)
+ apply assumption
+ apply (erule normal_imp_subgroup)
+apply (simp add: rcos_minus)
+done
+
+
+(* some rules for <#> with #> or <# *)
+lemma (in coset) setsum_rcos_assoc:
+ "[| H <= carrier G; K <= carrier G; x \<in> carrier G |]
+ ==> H <#> (K #> x) = (H <#> K) #> x"
+apply (auto simp add: rcos_def r_coset_def setsum_def set_sum_def)
+apply (force simp add: sum_assoc)+
+done
-syntax (xsymbols)
- "@NS" :: "['a set, 'a grouptype] => bool" ("_ \\<lhd> _" [60,61]60)
+lemma (in coset) rcos_assoc_lcos:
+ "[| H <= carrier G; K <= carrier G; x \<in> carrier G |]
+ ==> (H #> x) <#> K = H <#> (x <# K)"
+apply (auto simp add: rcos_def r_coset_def lcos_def l_coset_def
+ setsum_def set_sum_def Sigma_def image_def)
+apply (force simp add: sum_assoc)+
+done
+
+
+(* sumuct 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 *)
+
+lemma (in coset) rcos_sum_step1:
+ "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
+ ==> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
+by (simp add: setsum_rcos_assoc normal_imp_subgroup [THEN subgroup_imp_subset]
+ r_coset_subset_G l_coset_subset_G rcos_assoc_lcos)
+
+lemma (in coset) rcos_sum_step2:
+ "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
+ ==> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"
+by (simp add: normal_imp_rcos_eq_lcos)
-translations
- "N <| G" == "(G,N) \\<in> normal"
+lemma (in coset) rcos_sum_step3:
+ "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
+ ==> (H <#> (H #> x)) #> y = H #> (x \<oplus> y)"
+by (simp add: setsum_rcos_assoc r_coset_subset_G coset_sum_assoc
+ setsum_subset_G subgroup_sum_id
+ subgroup_imp_subset normal_imp_subgroup)
+
+lemma (in coset) rcos_sum:
+ "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
+ ==> (H #> x) <#> (H #> y) = H #> (x \<oplus> y)"
+by (simp add: rcos_sum_step1 rcos_sum_step2 rcos_sum_step3)
+
+(*generalizes subgroup_sum_id*)
+lemma (in coset) setrcos_sum_eq: "[|H <| G; M \<in> rcosets G H|] ==> H <#> M = M"
+by (auto simp add: setrcos_eq normal_imp_subgroup subgroup_imp_subset
+ setsum_rcos_assoc subgroup_sum_id)
+
+
+subsection{*Theorems Necessary for Lagrange*}
+
+lemma (in coset) setrcos_part_G: "subgroup H G ==> \<Union> rcosets G H = carrier G"
+apply (rule equalityI)
+apply (force simp add: subgroup_imp_subset [THEN subsetD] setrcos_eq r_coset_eq)
+apply (auto simp add: setrcos_eq subgroup_imp_subset rcos_self)
+done
+
+lemma (in coset) cosets_finite:
+ "[| c \<in> rcosets G H; H <= carrier G; finite (carrier G) |] ==> finite c"
+apply (auto simp add: setrcos_eq)
+apply (simp (no_asm_simp) add: r_coset_subset_G [THEN finite_subset])
+done
-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
+lemma (in coset) card_cosets_equal:
+ "[| c \<in> rcosets G H; H <= carrier G; finite(carrier G) |] ==> card c = card H"
+apply (auto simp add: setrcos_eq)
+(*FIXME: I can't say
+apply (rule_tac f = "%y. y \<oplus> (\<ominus>a)" and g = "%y. y \<oplus> a" in card_bij_eq)
+*)
+apply (rule_tac f = "%y. sum G y (gminus G a)"
+ and g = "%y. sum G y a" in card_bij_eq)
+ apply (simp add: r_coset_subset_G [THEN finite_subset])
+ apply (blast intro: finite_subset)
+ txt{*inclusion in @{term H}*}
+ apply (force simp add: sum_assoc subsetD r_coset_eq)
+ defer 1
+ txt{*inclusion in @{term "H #> a"}*}
+ apply (blast intro: rcosI)
+ apply (force simp add: inj_on_def right_cancellation_iff subsetD)
+apply (rule inj_onI)
+apply (subgoal_tac "x \<in> carrier G & y \<in> carrier G")
+ prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])
+apply (rotate_tac -1)
+apply (simp add: right_cancellation_iff subsetD)
+done
+
+
+subsection{*Two distinct right cosets are disjoint*}
+
+lemma (in coset) rcos_equation:
+ "[|subgroup H G; a \<in> carrier G; b \<in> carrier G; ha \<oplus> a = h \<oplus> b;
+ h \<in> H; ha \<in> H; hb \<in> H|]
+ ==> \<exists>h\<in>H. h \<oplus> b = hb \<oplus> a"
+apply (rule bexI [of _"hb \<oplus> ((\<ominus>ha) \<oplus> h)"])
+apply (simp add: sum_assoc transpose_minus subgroup_imp_subset [THEN subsetD])
+apply (simp add: subgroup_sum_closed subgroup_minus_closed)
+done
+
+lemma (in coset) rcos_disjoint:
+ "[|subgroup H G; a \<in> rcosets G H; b \<in> rcosets G H; a\<noteq>b|] ==> a \<inter> b = {}"
+apply (simp add: setrcos_eq r_coset_eq)
+apply (blast intro: rcos_equation sym)
+done
+
+lemma (in coset) setrcos_subset_PowG:
+ "subgroup H G ==> rcosets G H <= Pow(carrier G)"
+apply (simp add: setrcos_eq)
+apply (blast dest: r_coset_subset_G subgroup_imp_subset)
+done
- 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"
+theorem (in coset) lagrange:
+ "[| finite(carrier G); subgroup H G |]
+ ==> card(rcosets G H) * card(H) = order(G)"
+apply (simp (no_asm_simp) add: order_def setrcos_part_G [symmetric])
+apply (subst mult_commute)
+apply (rule card_partition)
+ apply (simp add: setrcos_subset_PowG [THEN finite_subset])
+ apply (simp add: setrcos_part_G)
+ apply (simp add: card_cosets_equal subgroup_def)
+apply (simp add: rcos_disjoint)
+done
+
+
+subsection {*Factorization of a Group*}
+
+constdefs
+ FactGroup :: "[('a,'b) group_scheme, 'a set] => ('a set) group"
+ (infixl "Mod" 60)
+ "FactGroup G H ==
+ (| carrier = rcosets G H,
+ sum = (%X: rcosets G H. %Y: rcosets G H. set_sum G X Y),
+ gminus = (%X: rcosets G H. set_minus G X),
+ zero = H |)"
+
+lemma (in coset) setsum_closed:
+ "[| H <| G; K1 \<in> rcosets G H; K2 \<in> rcosets G H |]
+ ==> K1 <#> K2 \<in> rcosets G H"
+by (auto simp add: normal_imp_subgroup [THEN subgroup_imp_subset]
+ rcos_sum setrcos_eq)
+
+lemma setminus_closed:
+ "[| H <| G; K \<in> rcosets G H |] ==> set_minus G K \<in> rcosets G H"
+by (auto simp add: normal_imp_coset normal_imp_group normal_imp_subgroup
+ subgroup_imp_subset coset.rcos_minus coset.setrcos_eq)
+
+lemma (in coset) setrcos_assoc:
+ "[|H <| G; M1 \<in> rcosets G H; M2 \<in> rcosets G H; M3 \<in> rcosets G H|]
+ ==> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
+by (auto simp add: setrcos_eq rcos_sum normal_imp_subgroup
+ subgroup_imp_subset sum_assoc)
+
+lemma subgroup_in_rcosets: "subgroup H G ==> H \<in> rcosets G H"
+apply (frule subgroup_imp_coset)
+apply (frule subgroup_imp_group)
+apply (simp add: coset.setrcos_eq)
+apply (blast del: equalityI
+ intro!: group.subgroup_zero_closed group.zero_closed
+ coset.coset_join2 [symmetric])
+done
+
+lemma (in coset) setrcos_minus_sum_eq:
+ "[|H <| G; M \<in> rcosets G H|] ==> set_minus G M <#> M = H"
+by (auto simp add: setrcos_eq rcos_minus rcos_sum normal_imp_subgroup
+ subgroup_imp_subset)
+
+theorem factorgroup_is_group: "H <| G ==> (G Mod H) \<in> Group"
+apply (frule normal_imp_coset)
+apply (simp add: FactGroup_def)
+apply (rule group.intro)
+ apply (rule semigroup.intro)
+ apply (simp add: restrictI coset.setsum_closed)
+ apply (simp add: coset.setsum_closed coset.setrcos_assoc)
+apply (rule group_axioms.intro)
+ apply (simp add: restrictI setminus_closed)
+ apply (simp add: normal_imp_subgroup subgroup_in_rcosets)
+ apply (simp add: setminus_closed coset.setrcos_minus_sum_eq)
+apply (simp add: normal_imp_subgroup subgroup_in_rcosets coset.setrcos_sum_eq)
+done
+
end
-
-
--- a/src/HOL/GroupTheory/DirProd.ML Wed Sep 25 11:23:26 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,94 +0,0 @@
-(* 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>) = \
-\ (%(x, x'): (P.<cr>). %(y, y'): (P.<cr>). ( x ## y, x' ##' y'))";
-by (afs [ProdGroup_def, binop_def, binop'_def] 1);
-qed "P_bin_op";
-
-Goal "(P.<inv>) = (%(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 = (%(x, x'): (P.<cr>). %(y, y'): (P.<cr>).\
-\ (x ## y, x' ##' y')), \
-\ inverse = (%(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 [P_def, 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";
--- a/src/HOL/GroupTheory/DirProd.thy Wed Sep 25 11:23:26 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-(* 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 == %G: Group. %G': Group.
- (| carrier = ((G.<cr>) \\<times> (G'.<cr>)),
- bin_op = (%(x, x'): ((G.<cr>) \\<times> (G'.<cr>)).
- %(y, y'): ((G.<cr>) \\<times> (G'.<cr>)).
- ((G.<f>) x y,(G'.<f>) x' y')),
- inverse = (%(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 Wed Sep 25 11:23:26 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,464 +0,0 @@
-(* Title: HOL/GroupTheory/Exponent
- ID: $Id$
- Author: Florian Kammueller, with new proofs by L C Paulson
- Copyright 2001 University of Cambridge
-*)
-
-(*** prime theorems ***)
-
-val prime_def = thm "prime_def";
-
-Goalw [prime_def] "p\\<in>prime ==> Suc 0 < p";
-by (force_tac (claset(), simpset() addsimps []) 1);
-qed "prime_imp_one_less";
-
-Goal "(p\\<in>prime) = (Suc 0 < p & (\\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))";
-by (auto_tac (claset(), simpset() addsimps [prime_imp_one_less]));
-by (blast_tac (claset() addSDs [thm "prime_dvd_mult"]) 1);
-by (auto_tac (claset(), simpset() addsimps [prime_def]));
-by (etac dvdE 1);
-by (case_tac "k=0" 1);
-by (Asm_full_simp_tac 1);
-by (dres_inst_tac [("x","m")] spec 1);
-by (dres_inst_tac [("x","k")] spec 1);
-by (asm_full_simp_tac
- (simpset() addsimps [dvd_mult_cancel1, dvd_mult_cancel2]) 1);
-by Auto_tac;
-qed "prime_iff";
-
-Goal "p\\<in>prime ==> 0 < p^a";
-by (force_tac (claset(), simpset() addsimps [prime_iff]) 1);
-qed "zero_less_prime_power";
-
-
-(*First some things about HOL and sets *)
-val [p1] = goal (the_context()) "(P x y) ==> ( (x, y)\\<in>{(a,b). P a b})";
-by (rtac CollectI 1);
-by (rewrite_goals_tac [split RS eq_reflection]);
-by (rtac p1 1);
-qed "CollectI_prod";
-
-val [p1] = goal (the_context()) "( (x, y)\\<in>{(a,b). P a b}) ==> (P x y)";
-by (res_inst_tac [("c1","P")] (split RS subst) 1);
-by (res_inst_tac [("a","(x,y)")] CollectD 1);
-by (rtac p1 1);
-qed "CollectD_prod";
-
-val [p1] = goal (the_context()) "(P x y z v) ==> ( (x, y, z, v)\\<in>{(a,b,c,d). P a b c d})";
-by (rtac CollectI_prod 1);
-by (rewrite_goals_tac [split RS eq_reflection]);
-by (rtac p1 1);
-qed "CollectI_prod4";
-
-Goal "( (x, y, z, v)\\<in>{(a,b,c,d). P a b c d}) ==> (P x y z v)";
-by Auto_tac;
-qed "CollectD_prod4";
-
-
-
-val [p1] = goal (the_context()) "x\\<in>{y. P(y) & Q(y)} ==> P(x)";
-by (res_inst_tac [("Q","Q x"),("P", "P x")] conjE 1);
-by (assume_tac 2);
-by (res_inst_tac [("a", "x")] CollectD 1);
-by (rtac p1 1);
-qed "subset_lemma1";
-
-val [p1,p2] = goal (the_context()) "[|P == Q; P|] ==> Q";
-by (fold_goals_tac [p1]);
-by (rtac p2 1);
-qed "apply_def";
-
-Goal "S \\<noteq> {} ==> \\<exists>x. x\\<in>S";
-by Auto_tac;
-qed "NotEmpty_ExEl";
-
-Goal "\\<exists>x. x: S ==> S \\<noteq> {}";
-by Auto_tac;
-qed "ExEl_NotEmpty";
-
-
-(* The following lemmas are needed for existsM1inM *)
-
-Goal "[| {} \\<notin> A; M\\<in>A |] ==> M \\<noteq> {}";
-by Auto_tac;
-qed "MnotEqempty";
-
-val [p1] = goal (the_context()) "\\<exists>g \\<in> A. x = P(g) ==> \\<exists>g \\<in> A. P(g) = x";
-by (rtac bexE 1);
-by (rtac p1 1);
-by (rtac bexI 1);
-by (rtac sym 1);
-by (assume_tac 1);
-by (assume_tac 1);
-qed "bex_sym";
-
-Goalw [equiv_def,quotient_def,sym_def,trans_def]
- "[| equiv A r; C\\<in>A // r |] ==> \\<forall>x \\<in> C. \\<forall>y \\<in> C. (x,y)\\<in>r";
-by (Blast_tac 1);
-qed "ElemClassEquiv";
-
-Goalw [equiv_def,quotient_def,sym_def,trans_def]
- "[|equiv A r; M\\<in>A // r; M1\\<in>M; (M1, M2)\\<in>r |] ==> M2\\<in>M";
-by (Blast_tac 1);
-qed "EquivElemClass";
-
-Goal "[| 0 < c; a <= b |] ==> a <= b * (c::nat)";
-by (res_inst_tac [("P","%x. x <= b * c")] subst 1);
-by (rtac mult_1_right 1);
-by (rtac mult_le_mono 1);
-by Auto_tac;
-qed "le_extend_mult";
-
-
-Goal "0 < card(S) ==> S \\<noteq> {}";
-by (force_tac (claset(), simpset() addsimps [card_empty]) 1);
-qed "card_nonempty";
-
-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 = {}";
-by Auto_tac;
-qed "insert_partition";
-
-(* main cardinality theorem *)
-Goal "finite C ==> \
-\ finite (\\<Union> C) --> \
-\ (\\<forall>c\\<in>C. card c = k) --> \
-\ (\\<forall>c1 \\<in> C. \\<forall>c2 \\<in> C. c1 \\<noteq> c2 --> c1 \\<inter> c2 = {}) --> \
-\ k * card(C) = card (\\<Union> C)";
-by (etac finite_induct 1);
-by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac
- (simpset() addsimps [card_insert_disjoint, card_Un_disjoint,
- insert_partition, inst "B" "\\<Union>(insert x F)" finite_subset]) 1);
-qed_spec_mp "card_partition";
-
-Goal "[| finite S; S \\<noteq> {} |] ==> 0 < card(S)";
-by (swap_res_tac [card_0_eq RS iffD1] 1);
-by Auto_tac;
-qed "zero_less_card_empty";
-
-
-Goal "[| p*k dvd m*n; p\\<in>prime |] \
-\ ==> (\\<exists>x. k dvd x*n & m = p*x) | (\\<exists>y. k dvd m*y & n = p*y)";
-by (asm_full_simp_tac (simpset() addsimps [prime_iff]) 1);
-by (ftac dvd_mult_left 1);
-by (subgoal_tac "p dvd m | p dvd n" 1);
-by (Blast_tac 2);
-by (etac disjE 1);
-by (rtac disjI1 1);
-by (rtac disjI2 2);
-by (eres_inst_tac [("n","m")] dvdE 1);
-by (eres_inst_tac [("n","n")] dvdE 2);
-by Auto_tac;
-by (res_inst_tac [("k","p")] dvd_mult_cancel 2);
-by (res_inst_tac [("k","p")] dvd_mult_cancel 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps mult_ac)));
-qed "prime_dvd_cases";
-
-
-Goal "p\\<in>prime \
-\ ==> \\<forall>m n. p^c dvd m*n --> \
-\ (\\<forall>a b. a+b = Suc c --> p^a dvd m | p^b dvd n)";
-by (induct_tac "c" 1);
- by (Clarify_tac 1);
- by (case_tac "a" 1);
- by (Asm_full_simp_tac 1);
- by (Asm_full_simp_tac 1);
-(*inductive step*)
-by (Asm_full_simp_tac 1);
-by (Clarify_tac 1);
-by (etac (prime_dvd_cases RS disjE) 1);
-by (assume_tac 1);
-by Auto_tac;
-(*case 1: p dvd m*)
- by (case_tac "a" 1);
- by (Asm_full_simp_tac 1);
- by (Clarify_tac 1);
- by (dtac spec 1 THEN dtac spec 1 THEN mp_tac 1);
- by (dres_inst_tac [("x","nat")] spec 1);
- by (dres_inst_tac [("x","b")] spec 1);
- by (Asm_full_simp_tac 1);
- by (blast_tac (claset() addIs [dvd_refl, mult_dvd_mono]) 1);
-(*case 2: p dvd n*)
-by (case_tac "b" 1);
- by (Asm_full_simp_tac 1);
-by (Clarify_tac 1);
-by (dtac spec 1 THEN dtac spec 1 THEN mp_tac 1);
-by (dres_inst_tac [("x","a")] spec 1);
-by (dres_inst_tac [("x","nat")] spec 1);
-by (Asm_full_simp_tac 1);
-by (blast_tac (claset() addIs [dvd_refl, mult_dvd_mono]) 1);
-qed_spec_mp "prime_power_dvd_cases";
-
-(*needed in this form in Sylow.ML*)
-Goal "[| p \\<in> prime; ~ (p ^ (Suc r) dvd n); p^(a+r) dvd n*k |] \
-\ ==> p ^ a dvd k";
-by (dres_inst_tac [("a","Suc r"), ("b","a")] prime_power_dvd_cases 1);
-by (assume_tac 1);
-by Auto_tac;
-qed "div_combine";
-
-(*Lemma for power_dvd_bound*)
-Goal "Suc 0 < p ==> Suc n <= p^n";
-by (induct_tac "n" 1);
-by (Asm_simp_tac 1);
-by (Asm_full_simp_tac 1);
-by (subgoal_tac "2 * n + 2 <= p * p^n" 1);
-by (Asm_full_simp_tac 1);
-by (subgoal_tac "2 * p^n <= p * p^n" 1);
-(*?arith_tac should handle all of this!*)
-by (rtac order_trans 1);
-by (assume_tac 2);
-by (dres_inst_tac [("k","2")] mult_le_mono2 1);
-by (Asm_full_simp_tac 1);
-by (rtac mult_le_mono1 1);
-by (Asm_full_simp_tac 1);
-qed "Suc_le_power";
-
-(*An upper bound for the n such that p^n dvd a: needed for GREATEST to exist*)
-Goal "[|p^n dvd a; Suc 0 < p; 0 < a|] ==> n < a";
-by (dtac dvd_imp_le 1);
-by (dres_inst_tac [("n","n")] Suc_le_power 2);
-by Auto_tac;
-qed "power_dvd_bound";
-
-
-(*** exponent theorems ***)
-
-Goal "[|p^k dvd n; p\\<in>prime; 0<n|] ==> k <= exponent p n";
-by (asm_full_simp_tac (simpset() addsimps [exponent_def]) 1);
-by (etac (thm "Greatest_le") 1);
-by (blast_tac (claset() addDs [prime_imp_one_less, power_dvd_bound]) 1);
-qed_spec_mp "exponent_ge";
-
-Goal "0<s ==> (p ^ exponent p s) dvd s";
-by (simp_tac (simpset() addsimps [exponent_def]) 1);
-by (Clarify_tac 1);
-by (res_inst_tac [("k","0")] (thm "GreatestI") 1);
-by (blast_tac (claset() addDs [prime_imp_one_less, power_dvd_bound]) 2);
-by (Asm_full_simp_tac 1);
-qed "power_exponent_dvd";
-
-Goal "[|(p * p ^ exponent p s) dvd s; p\\<in>prime |] ==> s=0";
-by (subgoal_tac "p ^ Suc(exponent p s) dvd s" 1);
-by (Asm_full_simp_tac 2);
-by (rtac ccontr 1);
-by (dtac exponent_ge 1);
-by Auto_tac;
-qed "power_Suc_exponent_Not_dvd";
-
-Goal "p\\<in>prime ==> exponent p (p^a) = a";
-by (asm_simp_tac (simpset() addsimps [exponent_def]) 1);
-by (rtac (thm "Greatest_equality") 1);
-by (Asm_full_simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [prime_imp_one_less, power_dvd_imp_le]) 1);
-qed "exponent_power_eq";
-Addsimps [exponent_power_eq];
-
-Goal "!r::nat. (p^r dvd a) = (p^r dvd b) ==> exponent p a = exponent p b";
-by (asm_simp_tac (simpset() addsimps [exponent_def]) 1);
-qed "exponent_equalityI";
-
-Goal "p \\<notin> prime ==> exponent p s = 0";
-by (asm_simp_tac (simpset() addsimps [exponent_def]) 1);
-qed "exponent_eq_0";
-Addsimps [exponent_eq_0];
-
-
-(* exponent_mult_add, easy inclusion. Could weaken p\\<in>prime to Suc 0 < p *)
-Goal "[| 0 < a; 0 < b |] \
-\ ==> (exponent p a) + (exponent p b) <= exponent p (a * b)";
-by (case_tac "p \\<in> prime" 1);
-by (rtac exponent_ge 1);
-by (auto_tac (claset(), simpset() addsimps [power_add]));
-by (blast_tac (claset() addIs [prime_imp_one_less, power_exponent_dvd,
- mult_dvd_mono]) 1);
-qed "exponent_mult_add1";
-
-(* exponent_mult_add, opposite inclusion *)
-Goal "[| 0 < a; 0 < b |] \
-\ ==> exponent p (a * b) <= (exponent p a) + (exponent p b)";
-by (case_tac "p\\<in>prime" 1);
-by (rtac leI 1);
-by (Clarify_tac 1);
-by (cut_inst_tac [("p","p"),("s","a*b")] power_exponent_dvd 1);
-by Auto_tac;
-by (subgoal_tac "p ^ (Suc (exponent p a + exponent p b)) dvd a * b" 1);
-by (rtac (le_imp_power_dvd RS dvd_trans) 2);
- by (assume_tac 3);
- by (Asm_full_simp_tac 2);
-by (forw_inst_tac [("a","Suc (exponent p a)"), ("b","Suc (exponent p b)")]
- prime_power_dvd_cases 1);
- by (assume_tac 1 THEN Force_tac 1);
-by (Asm_full_simp_tac 1);
-by (blast_tac (claset() addDs [power_Suc_exponent_Not_dvd]) 1);
-qed "exponent_mult_add2";
-
-Goal "[| 0 < a; 0 < b |] \
-\ ==> exponent p (a * b) = (exponent p a) + (exponent p b)";
-by (blast_tac (claset() addIs [exponent_mult_add1, exponent_mult_add2,
- order_antisym]) 1);
-qed "exponent_mult_add";
-
-
-Goal "~ (p dvd n) ==> exponent p n = 0";
-by (case_tac "exponent p n" 1);
-by (Asm_full_simp_tac 1);
-by (case_tac "n" 1);
-by (Asm_full_simp_tac 1);
-by (cut_inst_tac [("s","n"),("p","p")] power_exponent_dvd 1);
-by (auto_tac (claset() addDs [dvd_mult_left], simpset()));
-qed "not_divides_exponent_0";
-
-Goal "exponent p (Suc 0) = 0";
-by (case_tac "p \\<in> prime" 1);
-by (auto_tac (claset(),
- simpset() addsimps [prime_iff, not_divides_exponent_0]));
-qed "exponent_1_eq_0";
-Addsimps [exponent_1_eq_0];
-
-
-(*** Lemmas for the main combinatorial argument ***)
-
-Goal "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |] ==> r <= a";
-by (rtac notnotD 1);
-by (rtac notI 1);
-by (dtac (leI RSN (2, contrapos_nn) RS notnotD) 1);
-by (assume_tac 1);
-by (dres_inst_tac [("m","a")] less_imp_le 1);
-by (dtac le_imp_power_dvd 1);
-by (dres_inst_tac [("n","p ^ r")] dvd_trans 1);
-by (assume_tac 1);
-by (forw_inst_tac [("m","k")] less_imp_le 1);
-by (dres_inst_tac [("c","m")] le_extend_mult 1);
-by (assume_tac 1);
-by (dres_inst_tac [("k","p ^ a"),("m","(p ^ a) * m")] dvd_diffD1 1);
-by (assume_tac 2);
-by (rtac (dvd_refl RS dvd_mult2) 1);
-by (dres_inst_tac [("n","k")] dvd_imp_le 1);
-by Auto_tac;
-qed "p_fac_forw_lemma";
-
-Goal "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |] \
-\ ==> (p^r) dvd (p^a) - k";
-by (forw_inst_tac [("k1","k"),("i","p")]
- (p_fac_forw_lemma RS le_imp_power_dvd) 1);
-by Auto_tac;
-by (subgoal_tac "p^r dvd p^a*m" 1);
- by (blast_tac (claset() addIs [dvd_mult2]) 2);
-by (dtac dvd_diffD1 1);
- by (assume_tac 1);
- by (blast_tac (claset() addIs [dvd_diff]) 2);
-by (dtac less_imp_Suc_add 1);
-by Auto_tac;
-qed "p_fac_forw";
-
-
-Goal "[| 0 < (k::nat); k < p^a; 0 < p; (p^r) dvd (p^a) - k |] ==> r <= a";
-by (res_inst_tac [("m","Suc 0")] p_fac_forw_lemma 1);
-by Auto_tac;
-qed "r_le_a_forw";
-
-Goal "[| 0<m; 0<k; 0 < (p::nat); k < p^a; (p^r) dvd p^a - k |] \
-\ ==> (p^r) dvd (p^a)*m - k";
-by (forw_inst_tac [("k1","k"),("i","p")] (r_le_a_forw RS le_imp_power_dvd) 1);
-by Auto_tac;
-by (subgoal_tac "p^r dvd p^a*m" 1);
- by (blast_tac (claset() addIs [dvd_mult2]) 2);
-by (dtac dvd_diffD1 1);
- by (assume_tac 1);
- by (blast_tac (claset() addIs [dvd_diff]) 2);
-by (dtac less_imp_Suc_add 1);
-by Auto_tac;
-qed "p_fac_backw";
-
-Goal "[| 0<m; 0<k; 0 < (p::nat); k < p^a |] \
-\ ==> exponent p (p^a * m - k) = exponent p (p^a - k)";
-by (blast_tac (claset() addIs [exponent_equalityI, p_fac_forw,
- p_fac_backw]) 1);
-qed "exponent_p_a_m_k_equation";
-
-(*Suc rules that we have to delete from the simpset*)
-val bad_Sucs = [binomial_Suc_Suc, mult_Suc, mult_Suc_right];
-
-(*The bound K is needed; otherwise it's too weak to be used.*)
-Goal "[| \\<forall>i. Suc i < K --> exponent p (Suc i) = exponent p (Suc(j+i))|] \
-\ ==> k<K --> exponent p ((j+k) choose k) = 0";
-by (case_tac "p \\<in> prime" 1);
-by (Asm_simp_tac 2);
-by (induct_tac "k" 1);
-by (Simp_tac 1);
-(*induction step*)
-by (subgoal_tac "0 < (Suc(j+n) choose Suc n)" 1);
- by (simp_tac (simpset() addsimps [zero_less_binomial_iff]) 2);
-by (Clarify_tac 1);
-by (subgoal_tac
- "exponent p ((Suc(j+n) choose Suc n) * Suc n) = exponent p (Suc n)" 1);
-(*First, use the assumed equation. We simplify the LHS to
- exponent p (Suc (j + n) choose Suc n) + exponent p (Suc n);
- the common terms cancel, proving the conclusion.*)
- by (asm_full_simp_tac (simpset() delsimps bad_Sucs
- addsimps [exponent_mult_add]) 1);
-(*Establishing the equation requires first applying Suc_times_binomial_eq...*)
-by (asm_full_simp_tac (simpset() delsimps bad_Sucs
- addsimps [Suc_times_binomial_eq RS sym]) 1);
-(*...then exponent_mult_add and the quantified premise.*)
-by (asm_full_simp_tac (simpset() delsimps bad_Sucs
- addsimps [zero_less_binomial_iff, exponent_mult_add]) 1);
-qed_spec_mp "p_not_div_choose_lemma";
-
-(*The lemma above, with two changes of variables*)
-Goal "[| k<K; k<=n; \
-\ \\<forall>j. 0<j & j<K --> exponent p (n - k + (K - j)) = exponent p (K - j)|] \
-\ ==> exponent p (n choose k) = 0";
-by (cut_inst_tac [("j","n-k"),("k","k"),("p","p")] p_not_div_choose_lemma 1);
-by (assume_tac 2);
-by (Asm_full_simp_tac 2);
-by (Clarify_tac 1);
-by (dres_inst_tac [("x","K - Suc i")] spec 1);
-by (asm_full_simp_tac (simpset() addsimps [Suc_diff_le]) 1);
-qed "p_not_div_choose";
-
-
-Goal "0 < m ==> exponent p ((p^a * m - Suc 0) choose (p^a - Suc 0)) = 0";
-by (case_tac "p \\<in> prime" 1);
-by (Asm_simp_tac 2);
-by (forw_inst_tac [("a","a")] zero_less_prime_power 1);
-by (res_inst_tac [("K","p^a")] p_not_div_choose 1);
- by (Asm_full_simp_tac 1);
- by (Asm_full_simp_tac 1);
- by (case_tac "m" 1);
- by (case_tac "p^a" 2);
- by Auto_tac;
-(*now the hard case, simplified to
- exponent p (Suc (p ^ a * m + i - p ^ a)) = exponent p (Suc i) *)
-by (subgoal_tac "0<p" 1);
- by (force_tac (claset() addSDs [prime_imp_one_less], simpset()) 2);
-by (stac exponent_p_a_m_k_equation 1);
-by Auto_tac;
-qed "const_p_fac_right";
-
-Goal "0 < m ==> exponent p (((p^a) * m) choose p^a) = exponent p m";
-by (case_tac "p \\<in> prime" 1);
-by (Asm_simp_tac 2);
-by (subgoal_tac "0 < p^a * m & p^a <= p^a * m" 1);
-by (force_tac (claset(), simpset() addsimps [prime_iff]) 2);
-(*A similar trick to the one used in p_not_div_choose_lemma:
- insert an equation; use exponent_mult_add on the LHS; on the RHS, first
- transform the binomial coefficient, then use exponent_mult_add.*)
-by (subgoal_tac
- "exponent p ((((p^a) * m) choose p^a) * p^a) = a + exponent p m" 1);
-by (asm_full_simp_tac (simpset() delsimps bad_Sucs
- addsimps [zero_less_binomial_iff, exponent_mult_add, prime_iff]) 1);
-(*one subgoal left!*)
-by (stac times_binomial_minus1_eq 1);
-by (Asm_full_simp_tac 1);
-by (Asm_full_simp_tac 1);
-by (stac exponent_mult_add 1);
-by (Asm_full_simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [zero_less_binomial_iff]) 1);
-by (arith_tac 1);
-by (asm_full_simp_tac (simpset() delsimps bad_Sucs
- addsimps [exponent_mult_add, const_p_fac_right]) 1);
-qed "const_p_fac";
--- a/src/HOL/GroupTheory/Exponent.thy Wed Sep 25 11:23:26 2002 +0200
+++ b/src/HOL/GroupTheory/Exponent.thy Thu Sep 26 10:40:13 2002 +0200
@@ -1,18 +1,354 @@
(* Title: HOL/GroupTheory/Exponent
ID: $Id$
Author: Florian Kammueller, with new proofs by L C Paulson
- 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 +
+header{*The Combinatorial Argument Underlying the First Sylow Theorem*}
+
+theory Exponent = Main + Primes:
constdefs
+ exponent :: "[nat, nat] => nat"
+ "exponent p s == if p \<in> prime then (GREATEST r. p^r dvd s) else 0"
- exponent :: "[nat, nat] => nat"
- "exponent p s == if p \\<in> prime then (GREATEST r. p^r dvd s) else 0"
+subsection{*Prime Theorems*}
+
+lemma prime_imp_one_less: "p \<in> prime ==> Suc 0 < p"
+by (unfold prime_def, force)
+
+lemma prime_iff:
+ "(p \<in> prime) = (Suc 0 < p & (\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))"
+apply (auto simp add: prime_imp_one_less)
+apply (blast dest!: prime_dvd_mult)
+apply (auto simp add: prime_def)
+apply (erule dvdE)
+apply (case_tac "k=0", simp)
+apply (drule_tac x = m in spec)
+apply (drule_tac x = k in spec)
+apply (simp add: dvd_mult_cancel1 dvd_mult_cancel2, auto)
+done
+
+lemma zero_less_prime_power: "p \<in> prime ==> 0 < p^a"
+by (force simp add: prime_iff)
+
+
+lemma le_extend_mult: "[| 0 < c; a <= b |] ==> a <= b * (c::nat)"
+apply (rule_tac P = "%x. x <= b * c" in subst)
+apply (rule mult_1_right)
+apply (rule mult_le_mono, auto)
+done
+
+lemma card_nonempty: "0 < card(S) ==> S \<noteq> {}"
+by (force simp add: card_empty)
+
+lemma insert_partition:
+ "[| 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 = {}"
+by auto
+
+(* main cardinality theorem *)
+lemma card_partition [rule_format]:
+ "finite C ==>
+ finite (\<Union> C) -->
+ (\<forall>c\<in>C. card c = k) -->
+ (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->
+ k * card(C) = card (\<Union> C)"
+apply (erule finite_induct, simp)
+apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition
+ finite_subset [of _ "\<Union> (insert x F)"])
+done
+
+lemma zero_less_card_empty: "[| finite S; S \<noteq> {} |] ==> 0 < card(S)"
+by (rule ccontr, simp)
+
+
+lemma prime_dvd_cases:
+ "[| p*k dvd m*n; p \<in> prime |]
+ ==> (\<exists>x. k dvd x*n & m = p*x) | (\<exists>y. k dvd m*y & n = p*y)"
+apply (simp add: prime_iff)
+apply (frule dvd_mult_left)
+apply (subgoal_tac "p dvd m | p dvd n")
+ prefer 2 apply blast
+apply (erule disjE)
+apply (rule disjI1)
+apply (rule_tac [2] disjI2)
+apply (erule_tac n = m in dvdE)
+apply (erule_tac [2] n = n in dvdE, auto)
+apply (rule_tac [2] k = p in dvd_mult_cancel)
+apply (rule_tac k = p in dvd_mult_cancel)
+apply (simp_all add: mult_ac)
+done
+
+
+lemma prime_power_dvd_cases [rule_format (no_asm)]: "p \<in> prime
+ ==> \<forall>m n. p^c dvd m*n -->
+ (\<forall>a b. a+b = Suc c --> p^a dvd m | p^b dvd n)"
+apply (induct_tac "c")
+ apply clarify
+ apply (case_tac "a")
+ apply simp
+ apply simp
+(*inductive step*)
+apply simp
+apply clarify
+apply (erule prime_dvd_cases [THEN disjE], assumption, auto)
+(*case 1: p dvd m*)
+ apply (case_tac "a")
+ apply simp
+ apply clarify
+ apply (drule spec, drule spec, erule (1) notE impE)
+ apply (drule_tac x = nat in spec)
+ apply (drule_tac x = b in spec)
+ apply simp
+ apply (blast intro: dvd_refl mult_dvd_mono)
+(*case 2: p dvd n*)
+apply (case_tac "b")
+ apply simp
+apply clarify
+apply (drule spec, drule spec, erule (1) notE impE)
+apply (drule_tac x = a in spec)
+apply (drule_tac x = nat in spec, simp)
+apply (blast intro: dvd_refl mult_dvd_mono)
+done
+
+(*needed in this form in Sylow.ML*)
+lemma div_combine:
+ "[| p \<in> prime; ~ (p ^ (Suc r) dvd n); p^(a+r) dvd n*k |]
+ ==> p ^ a dvd k"
+by (drule_tac a = "Suc r" and b = a in prime_power_dvd_cases, assumption, auto)
+
+(*Lemma for power_dvd_bound*)
+lemma Suc_le_power: "Suc 0 < p ==> Suc n <= p^n"
+apply (induct_tac "n")
+apply (simp (no_asm_simp))
+apply simp
+apply (subgoal_tac "2 * n + 2 <= p * p^n", simp)
+apply (subgoal_tac "2 * p^n <= p * p^n")
+(*?arith_tac should handle all of this!*)
+apply (rule order_trans)
+prefer 2 apply assumption
+apply (drule_tac k = 2 in mult_le_mono2, simp)
+apply (rule mult_le_mono1, simp)
+done
+
+(*An upper bound for the n such that p^n dvd a: needed for GREATEST to exist*)
+lemma power_dvd_bound: "[|p^n dvd a; Suc 0 < p; 0 < a|] ==> n < a"
+apply (drule dvd_imp_le)
+apply (drule_tac [2] n = n in Suc_le_power, auto)
+done
+
+
+subsection{*Exponent Theorems*}
+
+lemma exponent_ge [rule_format]:
+ "[|p^k dvd n; p \<in> prime; 0<n|] ==> k <= exponent p n"
+apply (simp add: exponent_def)
+apply (erule Greatest_le)
+apply (blast dest: prime_imp_one_less power_dvd_bound)
+done
+
+lemma power_exponent_dvd: "0<s ==> (p ^ exponent p s) dvd s"
+apply (simp add: exponent_def)
+apply clarify
+apply (rule_tac k = 0 in GreatestI)
+prefer 2 apply (blast dest: prime_imp_one_less power_dvd_bound, simp)
+done
+
+lemma power_Suc_exponent_Not_dvd:
+ "[|(p * p ^ exponent p s) dvd s; p \<in> prime |] ==> s=0"
+apply (subgoal_tac "p ^ Suc (exponent p s) dvd s")
+ prefer 2 apply simp
+apply (rule ccontr)
+apply (drule exponent_ge, auto)
+done
+
+lemma exponent_power_eq [simp]: "p \<in> prime ==> exponent p (p^a) = a"
+apply (simp (no_asm_simp) add: exponent_def)
+apply (rule Greatest_equality, simp)
+apply (simp (no_asm_simp) add: prime_imp_one_less power_dvd_imp_le)
+done
+
+lemma exponent_equalityI:
+ "!r::nat. (p^r dvd a) = (p^r dvd b) ==> exponent p a = exponent p b"
+by (simp (no_asm_simp) add: exponent_def)
+
+lemma exponent_eq_0 [simp]: "p \<notin> prime ==> exponent p s = 0"
+by (simp (no_asm_simp) add: exponent_def)
+
+
+(* exponent_mult_add, easy inclusion. Could weaken p \<in> prime to Suc 0 < p *)
+lemma exponent_mult_add1:
+ "[| 0 < a; 0 < b |]
+ ==> (exponent p a) + (exponent p b) <= exponent p (a * b)"
+apply (case_tac "p \<in> prime")
+apply (rule exponent_ge)
+apply (auto simp add: power_add)
+apply (blast intro: prime_imp_one_less power_exponent_dvd mult_dvd_mono)
+done
+
+(* exponent_mult_add, opposite inclusion *)
+lemma exponent_mult_add2: "[| 0 < a; 0 < b |]
+ ==> exponent p (a * b) <= (exponent p a) + (exponent p b)"
+apply (case_tac "p \<in> prime")
+apply (rule leI, clarify)
+apply (cut_tac p = p and s = "a*b" in power_exponent_dvd, auto)
+apply (subgoal_tac "p ^ (Suc (exponent p a + exponent p b)) dvd a * b")
+apply (rule_tac [2] le_imp_power_dvd [THEN dvd_trans])
+ prefer 3 apply assumption
+ prefer 2 apply simp
+apply (frule_tac a = "Suc (exponent p a) " and b = "Suc (exponent p b) " in prime_power_dvd_cases)
+ apply (assumption, force, simp)
+apply (blast dest: power_Suc_exponent_Not_dvd)
+done
+
+lemma exponent_mult_add:
+ "[| 0 < a; 0 < b |]
+ ==> exponent p (a * b) = (exponent p a) + (exponent p b)"
+by (blast intro: exponent_mult_add1 exponent_mult_add2 order_antisym)
+
+
+lemma not_divides_exponent_0: "~ (p dvd n) ==> exponent p n = 0"
+apply (case_tac "exponent p n", simp)
+apply (case_tac "n", simp)
+apply (cut_tac s = n and p = p in power_exponent_dvd)
+apply (auto dest: dvd_mult_left)
+done
+
+lemma exponent_1_eq_0 [simp]: "exponent p (Suc 0) = 0"
+apply (case_tac "p \<in> prime")
+apply (auto simp add: prime_iff not_divides_exponent_0)
+done
+
+
+subsection{*Lemmas for the Main Combinatorial Argument*}
+
+lemma p_fac_forw_lemma:
+ "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |] ==> r <= a"
+apply (rule notnotD)
+apply (rule notI)
+apply (drule contrapos_nn [OF _ leI, THEN notnotD], assumption)
+apply (drule_tac m = a in less_imp_le)
+apply (drule le_imp_power_dvd)
+apply (drule_tac n = "p ^ r" in dvd_trans, assumption)
+apply (frule_tac m = k in less_imp_le)
+apply (drule_tac c = m in le_extend_mult, assumption)
+apply (drule_tac k = "p ^ a" and m = " (p ^ a) * m" in dvd_diffD1)
+prefer 2 apply assumption
+apply (rule dvd_refl [THEN dvd_mult2])
+apply (drule_tac n = k in dvd_imp_le, auto)
+done
+
+lemma p_fac_forw: "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |]
+ ==> (p^r) dvd (p^a) - k"
+apply (frule_tac k1 = k and i = p in p_fac_forw_lemma [THEN le_imp_power_dvd], auto)
+apply (subgoal_tac "p^r dvd p^a*m")
+ prefer 2 apply (blast intro: dvd_mult2)
+apply (drule dvd_diffD1)
+ apply assumption
+ prefer 2 apply (blast intro: dvd_diff)
+apply (drule less_imp_Suc_add, auto)
+done
+
+
+lemma r_le_a_forw: "[| 0 < (k::nat); k < p^a; 0 < p; (p^r) dvd (p^a) - k |] ==> r <= a"
+by (rule_tac m = "Suc 0" in p_fac_forw_lemma, auto)
+
+lemma p_fac_backw: "[| 0<m; 0<k; 0 < (p::nat); k < p^a; (p^r) dvd p^a - k |]
+ ==> (p^r) dvd (p^a)*m - k"
+apply (frule_tac k1 = k and i = p in r_le_a_forw [THEN le_imp_power_dvd], auto)
+apply (subgoal_tac "p^r dvd p^a*m")
+ prefer 2 apply (blast intro: dvd_mult2)
+apply (drule dvd_diffD1)
+ apply assumption
+ prefer 2 apply (blast intro: dvd_diff)
+apply (drule less_imp_Suc_add, auto)
+done
+
+lemma exponent_p_a_m_k_equation: "[| 0<m; 0<k; 0 < (p::nat); k < p^a |]
+ ==> exponent p (p^a * m - k) = exponent p (p^a - k)"
+apply (blast intro: exponent_equalityI p_fac_forw p_fac_backw)
+done
+
+text{*Suc rules that we have to delete from the simpset*}
+lemmas bad_Sucs = binomial_Suc_Suc mult_Suc mult_Suc_right
+
+(*The bound K is needed; otherwise it's too weak to be used.*)
+lemma p_not_div_choose_lemma [rule_format]:
+ "[| \<forall>i. Suc i < K --> exponent p (Suc i) = exponent p (Suc(j+i))|]
+ ==> k<K --> exponent p ((j+k) choose k) = 0"
+apply (case_tac "p \<in> prime")
+ prefer 2 apply simp
+apply (induct_tac "k")
+apply (simp (no_asm))
+(*induction step*)
+apply (subgoal_tac "0 < (Suc (j+n) choose Suc n) ")
+ prefer 2 apply (simp add: zero_less_binomial_iff, clarify)
+apply (subgoal_tac "exponent p ((Suc (j+n) choose Suc n) * Suc n) =
+ exponent p (Suc n)")
+ txt{*First, use the assumed equation. We simplify the LHS to
+ @{term "exponent p (Suc (j + n) choose Suc n) + exponent p (Suc n)"}
+ the common terms cancel, proving the conclusion.*}
+ apply (simp del: bad_Sucs add: exponent_mult_add)
+txt{*Establishing the equation requires first applying
+ @{text Suc_times_binomial_eq} ...*}
+apply (simp del: bad_Sucs add: Suc_times_binomial_eq [symmetric])
+txt{*...then @{text exponent_mult_add} and the quantified premise.*}
+apply (simp del: bad_Sucs add: zero_less_binomial_iff exponent_mult_add)
+done
+
+(*The lemma above, with two changes of variables*)
+lemma p_not_div_choose:
+ "[| k<K; k<=n;
+ \<forall>j. 0<j & j<K --> exponent p (n - k + (K - j)) = exponent p (K - j)|]
+ ==> exponent p (n choose k) = 0"
+apply (cut_tac j = "n-k" and k = k and p = p in p_not_div_choose_lemma)
+ prefer 3 apply simp
+ prefer 2 apply assumption
+apply (drule_tac x = "K - Suc i" in spec)
+apply (simp add: Suc_diff_le)
+done
+
+
+lemma const_p_fac_right:
+ "0 < m ==> exponent p ((p^a * m - Suc 0) choose (p^a - Suc 0)) = 0"
+apply (case_tac "p \<in> prime")
+ prefer 2 apply simp
+apply (frule_tac a = a in zero_less_prime_power)
+apply (rule_tac K = "p^a" in p_not_div_choose)
+ apply simp
+ apply simp
+ apply (case_tac "m")
+ apply (case_tac [2] "p^a")
+ apply auto
+(*now the hard case, simplified to
+ exponent p (Suc (p ^ a * m + i - p ^ a)) = exponent p (Suc i) *)
+apply (subgoal_tac "0<p")
+ prefer 2 apply (force dest!: prime_imp_one_less)
+apply (subst exponent_p_a_m_k_equation, auto)
+done
+
+lemma const_p_fac:
+ "0 < m ==> exponent p (((p^a) * m) choose p^a) = exponent p m"
+apply (case_tac "p \<in> prime")
+ prefer 2 apply simp
+apply (subgoal_tac "0 < p^a * m & p^a <= p^a * m")
+ prefer 2 apply (force simp add: prime_iff)
+txt{*A similar trick to the one used in @{text p_not_div_choose_lemma}:
+ insert an equation; use @{text exponent_mult_add} on the LHS; on the RHS,
+ first
+ transform the binomial coefficient, then use @{text exponent_mult_add}.*}
+apply (subgoal_tac "exponent p ((( (p^a) * m) choose p^a) * p^a) =
+ a + exponent p m")
+ apply (simp del: bad_Sucs add: zero_less_binomial_iff exponent_mult_add prime_iff)
+txt{*one subgoal left!*}
+apply (subst times_binomial_minus1_eq, simp, simp)
+apply (subst exponent_mult_add, simp)
+apply (simp (no_asm_simp) add: zero_less_binomial_iff)
+apply arith
+apply (simp del: bad_Sucs add: exponent_mult_add const_p_fac_right)
+done
+
end
--- a/src/HOL/GroupTheory/FactGroup.ML Wed Sep 25 11:23:26 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,80 +0,0 @@
-(* Title: HOL/GroupTheory/FactGroup
- ID: $Id$
- Author: Florian Kammueller, with new proofs by L C Paulson
- Copyright 1998-2001 University of Cambridge
-
-Factorization of a group
-*)
-
-
-Open_locale "factgroup";
-
-val H_normal = thm "H_normal";
-val F_def = thm "F_def";
-
-Addsimps [H_normal, F_def,setrcos_def];
-
-Goal "carrier F = {* H *}";
-by (afs [FactGroup_def] 1);
-qed "F_carrier";
-
-Goal "bin_op F = (%X: {* H *}. %Y: {* H *}. X <#> Y) ";
-by (afs [FactGroup_def, setprod_def] 1);
-qed "F_bin_op";
-
-Goal "inverse F = (%X: {* H *}. I(X))";
-by (afs [FactGroup_def, setinv_def] 1);
-qed "F_inverse";
-
-Goal "unit F = H";
-by (afs [FactGroup_def] 1);
-qed "F_unit";
-
-Goal "F = (| carrier = {* H *}, \
-\ bin_op = (%X: {* H *}. %Y: {* H *}. X <#> Y), \
-\ inverse = (%X: {* H *}. I(X)), unit = H |)";
-by (afs [FactGroup_def, F_carrier, F_bin_op, F_inverse, F_unit] 1);
-by (auto_tac (claset() addSIs [restrict_ext],
- simpset() addsimps [set_prod_def, setprod_def, setinv_def]));
-qed "F_defI";
-val F_DefI = export F_defI;
-
-Delsimps [setrcos_def];
-
-(* MAIN PROOF *)
-Goal "F \\<in> Group";
-val l1 = H_normal RS normal_imp_subgroup ;
-val l2 = l1 RS subgroup_imp_subset;
-by (stac F_defI 1);
-by (rtac GroupI 1);
-(* 1. *)
-by (afs [restrictI, setprod_closed] 1);
-(* 2. *)
-by (afs [restrictI, setinv_closed] 1);
-(* 3. H\\<in>{* H *} *)
-by (rtac (l1 RS setrcos_unit_closed) 1);
-(* 4. inverse property *)
-by (simp_tac (simpset() addsimps [setinv_closed, setrcos_inv_prod_eq]) 1);
-(* 5. unit property *)
-by (simp_tac (simpset() addsimps [normal_imp_subgroup,
- setrcos_unit_closed, setrcos_prod_eq]) 1);
-(* 6. associativity *)
-by (asm_simp_tac
- (simpset() addsimps [setprod_closed, H_normal RS setrcos_prod_assoc]) 1);
-qed "factorgroup_is_group";
-val FactorGroup_is_Group = export factorgroup_is_group;
-
-
-Delsimps [H_normal, F_def];
-Close_locale "factgroup";
-
-
-Goalw [FactGroup_def] "FactGroup \\<in> (PI G: Group. {H. H <| G} \\<rightarrow> Group)";
-by (rtac restrictI 1);
-by (rtac restrictI 1);
-by (asm_full_simp_tac
- (simpset() addsimps [F_DefI RS sym, FactorGroup_is_Group]) 1);
-qed "FactGroup_arity";
-
-Close_locale "coset";
-Close_locale "group";
--- a/src/HOL/GroupTheory/FactGroup.thy Wed Sep 25 11:23:26 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-(* Title: HOL/GroupTheory/FactGroup
- ID: $Id$
- Author: Florian Kammueller, with new proofs by L C Paulson
- Copyright 1998-2001 University of Cambridge
-
-Factorization of a group
-*)
-
-FactGroup = Coset +
-
-constdefs
- FactGroup :: "(['a grouptype, 'a set] => ('a set) grouptype)"
-
- "FactGroup ==
- %G: Group. %H: {H. H <| G}.
- (| carrier = set_r_cos G H,
- bin_op = (%X: set_r_cos G H. %Y: set_r_cos G H. set_prod G X Y),
- inverse = (%X: set_r_cos G H. set_inv G X),
- unit = H |)"
-
-syntax
- "@Fact" :: "['a grouptype, 'a set] => ('a set) grouptype"
- ("_ Mod _" [60,61]60)
-
-translations
- "G Mod H" == "FactGroup G H"
-
-locale factgroup = coset +
-fixes
- F :: "('a set) grouptype"
- H :: "('a set)"
-assumes
- H_normal "H <| G"
-defines
- F_def "F == FactGroup G H"
-
-end
-
\ No newline at end of file
--- a/src/HOL/GroupTheory/Group.ML Wed Sep 25 11:23:26 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,223 +0,0 @@
-(* Title: HOL/GroupTheory/Group
- ID: $Id$
- Author: Florian Kammueller, with new proofs by L C Paulson
- Copyright 1998-2001 University of Cambridge
-
-Group theory using locales
-*)
-
-
-fun afs thms = (asm_full_simp_tac (simpset() addsimps thms));
-
-
-(* Proof of group theory theorems necessary for Sylow's theorem *)
-Open_locale "group";
-
-val e_def = thm "e_def";
-val binop_def = thm "binop_def";
-val inv_def = thm "inv_def";
-val Group_G = thm "Group_G";
-
-
-val simp_G = simplify (simpset() addsimps [Group_def]) (Group_G);
-Addsimps [simp_G, Group_G];
-
-Goal "e \\<in> carrier G";
-by (afs [e_def] 1);
-qed "e_closed";
-val unit_closed = export e_closed;
-Addsimps [e_closed];
-
-Goal "op ## \\<in> carrier G \\<rightarrow> carrier G \\<rightarrow> carrier G";
-by (simp_tac (simpset() addsimps [binop_def]) 1);
-qed "binop_funcset";
-
-Goal "[| x \\<in> carrier G; y \\<in> carrier G |] ==> x ## y \\<in> carrier G";
-by (afs [binop_funcset RS (funcset_mem RS funcset_mem)] 1);
-qed "binop_closed";
-val bin_op_closed = export binop_closed;
-Addsimps [binop_closed];
-
-Goal "INV \\<in> carrier G \\<rightarrow> carrier G";
-by (simp_tac (simpset() addsimps [inv_def]) 1);
-qed "inv_funcset";
-
-Goal "x \\<in> carrier G ==> i(x) \\<in> carrier G";
-by (afs [inv_funcset RS funcset_mem] 1);
-qed "inv_closed";
-val inverse_closed = export inv_closed;
-Addsimps [inv_closed];
-
-Goal "x \\<in> carrier G ==> e ## x = x";
-by (afs [e_def, binop_def] 1);
-qed "e_ax1";
-Addsimps [e_ax1];
-
-Goal "x \\<in> carrier G ==> i(x) ## x = e";
-by (afs [binop_def, inv_def, e_def] 1);
-qed "inv_ax2";
-Addsimps [inv_ax2];
-
-Goal "[| x \\<in> carrier G; y \\<in> carrier G; z \\<in> carrier G |] \
-\ ==> (x ## y) ## z = x ## (y ## z)";
-by (afs [binop_def] 1);
-qed "binop_assoc";
-
-Goal "[|f \\<in> A \\<rightarrow> A \\<rightarrow> A; i1 \\<in> A \\<rightarrow> A; e1 \\<in> A;\
-\ \\<forall>x \\<in> A. (f (i1 x) x = e1); \\<forall>x \\<in> A. (f e1 x = x);\
-\ \\<forall>x \\<in> A. \\<forall>y \\<in> A. \\<forall>z \\<in> A. (f (f x y) z = f (x) (f y z)) |] \
-\ ==> (| carrier = A, bin_op = f, inverse = i1, unit = e1 |) \\<in> Group";
-by (afs [Group_def] 1);
-qed "groupI";
-val GroupI = export groupI;
-
-(*****)
-(* Now the real derivations *)
-
-Goal "[| x\\<in>carrier G ; y\\<in>carrier G; z\\<in>carrier G; x ## y = x ## z |] \
-\ ==> y = z";
-by (dres_inst_tac [("f","%z. i x ## z")] arg_cong 1);
-by (asm_full_simp_tac (simpset() addsimps [binop_assoc RS sym]) 1);
-qed "left_cancellation";
-
-Goal "[| x \\<in> carrier G; y \\<in> carrier G; z \\<in> carrier G |] \
-\ ==> (x ## y = x ## z) = (y = z)";
-by (blast_tac (claset() addIs [left_cancellation]) 1);
-qed "left_cancellation_iff";
-
-
-(* Now the other directions of basic lemmas; they need a left cancellation*)
-
-Goal "x \\<in> carrier G ==> x ## e = x";
-by (res_inst_tac [("x","i x")] left_cancellation 1);
-by (auto_tac (claset(), simpset() addsimps [binop_assoc RS sym]));
-qed "e_ax2";
-Addsimps [e_ax2];
-
-Goal "[| x \\<in> carrier G; x ## x = x |] ==> x = e";
-by (res_inst_tac [("x","x")] left_cancellation 1);
-by Auto_tac;
-qed "idempotent_e";
-
-Goal "x \\<in> carrier G ==> x ## i(x) = e";
-by (rtac idempotent_e 1);
-by (auto_tac (claset(), simpset() addsimps [binop_assoc RS sym]));
-by (asm_simp_tac (simpset() addsimps [inst "x" "x" binop_assoc]) 1);
-qed "inv_ax1";
-Addsimps [inv_ax1];
-
-Goal "[| x \\<in> carrier G; y \\<in> carrier G; x ## y = e |] ==> y = i(x)";
-by (res_inst_tac [("x","x")] left_cancellation 1);
-by Auto_tac;
-qed "inv_unique";
-
-Goal "x \\<in> carrier G ==> i(i(x)) = x";
-by (res_inst_tac [("x","i x")] left_cancellation 1);
-by Auto_tac;
-qed "inv_inv";
-Addsimps [inv_inv];
-
-Goal "[| x \\<in> carrier G; y \\<in> carrier G |] ==> i(x ## y) = i(y) ## i(x)";
-by (rtac (inv_unique RS sym) 1);
-by (auto_tac (claset(), simpset() addsimps [binop_assoc RS sym]));
-by (asm_simp_tac (simpset() addsimps [inst "x" "x" binop_assoc]) 1);
-qed "inv_prod";
-
-Goal "[| y ## x = z ## x; \
-\ x \\<in> carrier G; y \\<in> carrier G; z \\<in> carrier G|] ==> y = z";
-by (dres_inst_tac [("f","%z. z ## i x")] arg_cong 1);
-by (asm_full_simp_tac (simpset() addsimps [binop_assoc]) 1);
-qed "right_cancellation";
-
-Goal "[| x \\<in> carrier G; y \\<in> carrier G; z \\<in> carrier G |] \
-\ ==> (y ## x = z ## x) = (y = z)";
-by (blast_tac (claset() addIs [right_cancellation]) 1);
-qed "right_cancellation_iff";
-
-
-(* subgroup *)
-Goal "[| H <= carrier G; H \\<noteq> {}; \\<forall>a \\<in> H. i(a)\\<in>H; \\<forall>a\\<in>H. \\<forall>b\\<in>H. a ## b\\<in>H|] \
-\ ==> e \\<in> H";
-by (Force_tac 1);
-qed "e_in_H";
-
-(* subgroupI: a characterization of subgroups *)
-Goal "[| H <= carrier G; H \\<noteq> {}; \\<forall>a \\<in> H. i(a)\\<in>H;\
-\ \\<forall>a\\<in>H. \\<forall>b\\<in>H. a ## b\\<in>H |] ==> H <<= G";
-by (asm_full_simp_tac (simpset() addsimps [subgroup_def]) 1);
-(* Fold the locale definitions: the top level definition of subgroup gives
- the verbose form, which does not immediately match rules like inv_ax1 *)
-by (rtac groupI 1);
-by (ALLGOALS (asm_full_simp_tac
- (simpset() addsimps [subsetD, restrictI, e_in_H, binop_assoc] @
- (map symmetric [binop_def, inv_def, e_def]))));
-qed "subgroupI";
-val SubgroupI = export subgroupI;
-
-Goal "H <<= G ==> \
-\ (|carrier = H, bin_op = %x:H. %y:H. x ## y, \
-\ inverse = %x:H. i(x), unit = e|)\\<in>Group";
-by (afs [subgroup_def, binop_def, inv_def, e_def] 1);
-qed "subgroupE2";
-val SubgroupE2 = export subgroupE2;
-
-Goal "H <<= G ==> H <= carrier G";
-by (afs [subgroup_def, binop_def, inv_def, e_def] 1);
-qed "subgroup_imp_subset";
-
-Goal "[| H <<= G; x \\<in> H; y \\<in> H |] ==> x ## y \\<in> H";
-by (dtac subgroupE2 1);
-by (dtac bin_op_closed 1);
-by (Asm_full_simp_tac 1);
-by (thin_tac "x\\<in>H" 1);
-by Auto_tac;
-qed "subgroup_f_closed";
-
-Goal "[| H <<= G; x \\<in> H |] ==> i x \\<in> H";
-by (dtac (subgroupE2 RS inverse_closed) 1);
-by Auto_tac;
-qed "subgroup_inv_closed";
-val Subgroup_inverse_closed = export subgroup_inv_closed;
-
-Goal "H <<= G ==> e\\<in>H";
-by (dtac (subgroupE2 RS unit_closed) 1);
-by (Asm_full_simp_tac 1);
-qed "subgroup_e_closed";
-
-Goal "[| finite(carrier G); H <<= G |] ==> 0 < card(H)";
-by (subgoal_tac "finite H" 1);
- by (blast_tac (claset() addIs [finite_subset] addDs [subgroup_imp_subset]) 2);
-by (rtac ccontr 1);
-by (asm_full_simp_tac (simpset() addsimps [card_0_eq]) 1);
-by (blast_tac (claset() addDs [subgroup_e_closed]) 1);
-qed "SG_card1";
-
-(* Abelian Groups *)
-Goal "[|G' \\<in> AbelianGroup; x: carrier G'; y: carrier G'|] \
-\ ==> (G'.<f>) x y = (G'.<f>) y x";
-by (auto_tac (claset(), simpset() addsimps [AbelianGroup_def]));
-qed "Group_commute";
-
-Goal "AbelianGroup <= Group";
-by (auto_tac (claset(), simpset() addsimps [AbelianGroup_def]));
-qed "Abel_subset_Group";
-
-val Abel_imp_Group = Abel_subset_Group RS subsetD;
-
-Delsimps [simp_G, Group_G];
-Close_locale "group";
-
-Goal "G \\<in> Group ==> (| carrier = G .<cr>, bin_op = G .<f>, inverse = G .<inv>,\
-\ unit = G .<e> |) \\<in> Group";
-by (blast_tac
- (claset() addIs [GroupI, export binop_funcset, export inv_funcset, export e_closed, export inv_ax2, export e_ax1, export binop_assoc]) 1);
-qed "Group_Group";
-
-Goal "G \\<in> AbelianGroup \
-\ ==> (| carrier = G .<cr>, bin_op = G .<f>, inverse = G .<inv>,\
-\ unit = G .<e> |) \\<in> AbelianGroup";
-by (asm_full_simp_tac (simpset() addsimps [AbelianGroup_def]) 1);
-by (rtac Group_Group 1);
-by Auto_tac;
-qed "Abel_Abel";
-
--- a/src/HOL/GroupTheory/Group.thy Wed Sep 25 11:23:26 2002 +0200
+++ b/src/HOL/GroupTheory/Group.thy Thu Sep 26 10:40:13 2002 +0200
@@ -1,85 +1,376 @@
(* Title: HOL/GroupTheory/Group
ID: $Id$
Author: Florian Kammueller, with new proofs by L C Paulson
- Copyright 1998-2001 University of Cambridge
-
-Group theory using locales
*)
-Group = Main +
+header{*Group Theory Using Locales*}
+
+theory Group = FuncSet:
+
+subsection{*Semigroups*}
+
+record 'a semigroup =
+ carrier :: "'a set"
+ sum :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<oplus>\<index>" 65)
- (*Giving funcset the nice arrow syntax \\<rightarrow> *)
-syntax (xsymbols)
- "op funcset" :: "['a set, 'b set] => ('a => 'b) set" (infixr "\\<rightarrow>" 60)
+locale semigroup =
+ fixes S (structure)
+ assumes sum_funcset: "sum S \<in> carrier S \<rightarrow> carrier S \<rightarrow> carrier S"
+ and sum_assoc:
+ "[|x \<in> carrier S; y \<in> carrier S; z \<in> carrier S|]
+ ==> (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
-
-record 'a semigrouptype =
- carrier :: "'a set"
- bin_op :: "['a, 'a] => 'a"
+constdefs
+ order :: "(('a,'b) semigroup_scheme) => nat"
+ "order(S) == card(carrier S)"
-record 'a grouptype = 'a semigrouptype +
- inverse :: "'a => 'a"
- unit :: "'a"
-
-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)
+(*Overloading is impossible because of the way record types are represented*)
+constdefs
+ subsemigroup :: "['a set, ('a,'b) semigroup_scheme] => bool"
+ "subsemigroup H G ==
+ H <= carrier G &
+ semigroup G &
+ semigroup (G(|carrier:=H|))"
-translations
- "G.<cr>" => "carrier G"
- "G.<f>" => "bin_op G"
- "G.<inv>" => "inverse G"
- "G.<e>" => "unit G"
+(*a characterization of subsemigroups *)
+lemma (in semigroup) subsemigroupI:
+ "[| H <= carrier S;
+ !!a b. [|a \<in> H; b \<in> H|] ==> a \<oplus> b \<in> H |]
+ ==> subsemigroup H S"
+apply (insert prems)
+apply (simp add: semigroup_def subsemigroup_def, clarify)
+apply (blast intro: funcsetI)
+done
+
+
+subsection{*Groups*}
-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)))}"
+record 'a group = "'a semigroup" +
+ gminus :: "'a \<Rightarrow> 'a" ("(\<ominus>\<index>_)" [81] 80)
+ zero :: 'a ("\<zero>\<index>")
+
+locale group = semigroup G +
+ assumes minus_funcset: "gminus G \<in> carrier G \<rightarrow> carrier G"
+ and zero_closed [iff]:
+ "zero G \<in> carrier G"
+ and left_minus [simp]:
+ "x \<in> carrier G ==> (\<ominus>x) \<oplus> x = \<zero>"
+ and left_zero [simp]:
+ "x \<in> carrier G ==> \<zero> \<oplus> x = x"
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)))}"
+ Group :: "('a,'b) group_scheme set"
+ "Group == Collect group"
+
+lemma [simp]: "(G \<in> Group) = (group G)"
+by (simp add: Group_def)
+
+lemma "group G ==> semigroup G"
+by (simp add: group_def semigroup_def)
+
+
+locale abelian_group = group +
+ assumes sum_commute: "[|x \<in> carrier G; y \<in> carrier G|] ==> x \<oplus> y = y \<oplus> x"
+
+
+subsection{*Basic Group Theory Theorems*}
+
+lemma (in semigroup) sum_closed [simp]:
+ "[|x \<in> carrier S; y \<in> carrier S|] ==> (x \<oplus> y) \<in> carrier S"
+apply (insert sum_funcset)
+apply (blast dest: funcset_mem)
+done
+
+lemma (in group) minus_closed [simp]:
+ "x \<in> carrier G ==> (\<ominus>x) \<in> carrier G"
+apply (insert minus_funcset)
+apply (blast dest: funcset_mem)
+done
+
+lemma (in group) left_cancellation:
+ "[| x \<oplus> y = x \<oplus> z;
+ x \<in> carrier G ; y \<in> carrier G; z \<in> carrier G |]
+ ==> y = z"
+apply (drule arg_cong [of concl: "%z. (\<ominus>x) \<oplus> z"])
+apply (simp add: sum_assoc [symmetric])
+done
+
+(*Isar version??
+lemma (in group) left_cancellation:
+ assumes eq: "x \<oplus> y = x \<oplus> z"
+ shows "[| x \<in> carrier G ; y \<in> carrier G; z \<in> carrier G |]
+ ==> y = z"
+proof -
+ have "(\<ominus>x) \<oplus> (x \<oplus> y) = (\<ominus>x) \<oplus> (x \<oplus> z)" by (simp only: eq)
+ assume ?this
+ have "((\<ominus>x) \<oplus> x) \<oplus> y = ((\<ominus>x) \<oplus> x) \<oplus> z" by (simp only: sum_assoc)
+*)
+
+lemma (in group) left_cancellation_iff [simp]:
+ "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |]
+ ==> (x \<oplus> y = x \<oplus> z) = (y = z)"
+by (blast intro: left_cancellation)
+
+
+subsection{*The Other Directions of Basic Lemmas*}
+
+lemma (in group) right_zero [simp]: "x \<in> carrier G ==> x \<oplus> \<zero> = x"
+apply (rule left_cancellation [of "(\<ominus>x)"])
+apply (auto simp add: sum_assoc [symmetric])
+done
+
+lemma (in group) idempotent_imp_zero: "[| x \<in> carrier G; x \<oplus> x = x |] ==> x=\<zero>"
+by (rule left_cancellation [of x], auto)
+
+lemma (in group) right_minus [simp]: "x \<in> carrier G ==> x \<oplus> (\<ominus>x) = \<zero>"
+apply (rule idempotent_imp_zero)
+apply (simp_all add: sum_assoc [symmetric])
+apply (simp add: sum_assoc)
+done
+
+lemma (in group) minus_unique:
+ "[| x \<in> carrier G; y \<in> carrier G; x \<oplus> y = \<zero> |] ==> y = (\<ominus>x)"
+apply (rule left_cancellation [of x], auto)
+done
- order :: "'a grouptype => nat" "order(G) == card(carrier 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"
+lemma (in group) minus_minus [simp]:
+ "x \<in> carrier G ==> \<ominus>(\<ominus>x) = x"
+apply (rule left_cancellation [of "(\<ominus>x)"])
+apply auto
+done
+
+lemma (in group) minus_sum:
+ "[| x \<in> carrier G; y \<in> carrier G |] ==> \<ominus>(x \<oplus> y) = (\<ominus>y) \<oplus> (\<ominus>x)"
+apply (rule minus_unique [symmetric])
+apply (simp_all add: sum_assoc [symmetric])
+apply (simp add: sum_assoc)
+done
+
+lemma (in group) right_cancellation:
+ "[| y \<oplus> x = z \<oplus> x;
+ x \<in> carrier G; y \<in> carrier G; z \<in> carrier G|] ==> y = z"
+apply (drule arg_cong [of concl: "%z. z \<oplus> (\<ominus>x)"])
+apply (simp add: sum_assoc)
+done
+
+lemma (in group) right_cancellation_iff [simp]:
+ "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |]
+ ==> (y \<oplus> x = z \<oplus> x) = (y = z)"
+by (blast intro: right_cancellation)
+
+
+subsection{*The Subgroup Relation*}
+
+constdefs
+ subgroup :: "['a set, ('a,'b) group_scheme] => bool"
+ "subgroup H G ==
+ H <= carrier G &
+ group G &
+ group (G(|carrier:=H|))";
+
-defs
- subgroup_def "subgroup == SIGMA G: Group. {H. H <= carrier G &
- ((| carrier = H, bin_op = %x: H. %y: H. (bin_op G) x y,
- inverse = %x: H. (inverse G) x, unit = unit G |) : Group)}"
+text{*Since @{term H} is nonempty, it contains some element @{term x}. Since
+it's closed under inverse, it contains @{text "(\<ominus>x)"}. Since
+it's closed under sum, it contains @{text "x \<oplus> (\<ominus>x) = \<zero>"}.
+How impressive that the proof is automatic!*}
+lemma (in group) zero_in_subset:
+ "[| H <= carrier G; H \<noteq> {}; \<forall>a \<in> H. (\<ominus>a) \<in> H; \<forall>a\<in>H. \<forall>b\<in>H. a \<oplus> b \<in> H|]
+ ==> \<zero> \<in> H"
+by force
+
+text{*A characterization of subgroups*}
+lemma (in group) subgroupI:
+ "[| H <= carrier G; H \<noteq> {};
+ !!a. a \<in> H ==> (\<ominus>a) \<in> H;
+ !!a b. [|a \<in> H; b \<in> H|] ==> a \<oplus> b \<in> H |]
+ ==> subgroup H G"
+apply (insert prems)
+apply (simp add: group_def subgroup_def)
+apply (simp add: semigroup_def group_axioms_def, clarify)
+apply (intro conjI ballI)
+apply (simp_all add: funcsetI subsetD [of H "carrier G"])
+apply (blast intro: zero_in_subset)
+done
+
+
+lemma subgroup_imp_subset: "subgroup H G ==> H <= carrier G"
+by (simp add: subgroup_def)
+
+lemma (in group) subgroup_sum_closed:
+ "[| subgroup H G; x \<in> H; y \<in> H |] ==> x \<oplus> y \<in> H"
+by (simp add: subgroup_def group_def semigroup_def Pi_def)
+
+lemma (in group) subgroup_minus_closed:
+ "[| subgroup H G; x \<in> H |] ==> (\<ominus>x) \<in> H"
+by (simp add: subgroup_def group_def group_axioms_def Pi_def)
+
+lemma (in group) subgroup_zero_closed: "subgroup H G ==> \<zero> \<in> H"
+by (simp add: subgroup_def group_def group_axioms_def)
+
+text{*Global declarations, in force outside the locale*}
+declare semigroup.sum_closed [simp]
-syntax
- "@SG" :: "['a set, 'a grouptype] => bool" ("_ <<= _" [51,50]50)
+declare group.zero_closed [iff]
+ and group.minus_closed [simp]
+ and group.left_minus [simp]
+ and group.left_zero [simp]
+ and group.right_minus [simp]
+ and group.right_zero [simp]
+ and group.minus_minus [simp]
+
+
+lemma subgroup_imp_group: "subgroup H G ==> group G"
+by (simp add: subgroup_def)
+
+lemma subgroup_nonempty: "~ subgroup {} G"
+by (blast dest: subgroup_imp_group group.subgroup_zero_closed)
+
+lemma subgroup_card_positive:
+ "[| finite(carrier G); subgroup H G |] ==> 0 < card(H)"
+apply (subgoal_tac "finite H")
+ prefer 2 apply (blast intro: finite_subset dest: subgroup_imp_subset)
+apply (rule ccontr)
+apply (simp add: card_0_eq subgroup_nonempty)
+done
+
+subsection{*Direct Product of Two Groups*}
+
+text{*We want to overload product for all algebraic structures. But it is not
+easy. All of them are instances of the same type, namely @{text
+carrier_field_type}, which the record declaration generates automatically.
+Overloading requires distinct types.*}
+
+constdefs
+ ProdGroup :: "[('a,'c) group_scheme, ('b,'d) group_scheme] => ('a*'b) group"
+ (infixr "'(*')" 80)
+ "G (*) G' ==
+ (| carrier = carrier G \<times> carrier G',
+ sum = (%(x, x') (y, y'). (sum G x y, sum G' x' y')),
+ gminus = (%(x, y). (gminus G x, gminus G' y)),
+ zero = (zero G, zero G') |)"
-translations
- "H <<= G" == "(G,H) : subgroup"
+syntax (xsymbols)
+ ProdGroup :: "[('a,'c) group_scheme, ('b,'d) group_scheme] => ('a*'b) group"
+ (infixr "\<otimes>" 80)
+
+
+lemma P_carrier: "(carrier (G\<otimes>G')) = ((carrier G) \<times> (carrier G'))"
+by (simp add: ProdGroup_def)
+
+lemma P_sum: "sum (G\<otimes>G') = (%(x, x') (y, y'). (sum G x y, sum G' x' y'))"
+by (simp add: ProdGroup_def)
+
+lemma P_minus: "(gminus (G\<otimes>G')) = (%(x, y). (gminus G x, gminus G' y))"
+by (simp add: ProdGroup_def)
+
+lemma P_zero: "zero (G\<otimes>G') = (zero G, zero G')"
+by (simp add: ProdGroup_def)
+
+lemma P_sum_funcset:
+ "[|semigroup G; semigroup G'|] ==>
+ sum(G\<otimes>G') : carrier(G\<otimes>G') \<rightarrow> carrier(G\<otimes>G') \<rightarrow> carrier(G\<otimes>G')"
+by (auto intro!: funcsetI
+ simp add: semigroup.sum_closed P_sum P_carrier)
+
+lemma P_minus_funcset:
+ "[|group G; group G'|] ==>
+ gminus(G\<otimes>G') : carrier(G\<otimes>G') \<rightarrow> carrier(G\<otimes>G')"
+by (auto intro!: funcsetI
+ simp add: group_def group.minus_closed P_minus P_carrier)
+
+theorem ProdGroup_is_group: "[|group G; group G'|] ==> group (G\<otimes>G')"
+apply (rule group.intro)
+ apply (simp add: group_def)
+ apply (rule semigroup.intro)
+ apply (simp add: group_def P_sum_funcset)
+ apply (force simp add: ProdGroup_def semigroup.sum_assoc)
+apply (rule group_axioms.intro)
+ apply (simp add: P_minus_funcset)
+ apply (simp add: ProdGroup_def group.zero_closed)
+ apply (force simp add: ProdGroup_def group.left_minus)
+apply (force simp add: ProdGroup_def group.left_zero)
+done
-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"
+lemma ProdGroup_arity: "ProdGroup : Group \<rightarrow> Group \<rightarrow> Group"
+by (auto intro!: funcsetI ProdGroup_is_group)
+
+subsection{*Homomorphisms on Groups and Semigroups*}
+
+constdefs
+ hom :: "[('a,'c)semigroup_scheme, ('b,'d)semigroup_scheme] => ('a => 'b)set"
+ "hom S S' ==
+ {h. h \<in> carrier S -> carrier S' &
+ (\<forall>x \<in> carrier S. \<forall>y \<in> carrier S. h(sum S x y) = sum S' (h x) (h y))}"
+
+lemma hom_semigroup:
+ "semigroup S ==> semigroup (|carrier = hom S S, sum = (%h g. h o g) |)"
+apply (simp add: semigroup_def o_assoc)
+apply (simp add: Pi_def hom_def)
+done
+
+lemma hom_sum:
+ "[|h \<in> hom S S'; x \<in> carrier S; y \<in> carrier S|]
+ ==> h(sum S x y) = sum S' (h x) (h y)"
+by (simp add: hom_def)
+
+lemma hom_closed:
+ "[|h \<in> hom G G'; x \<in> carrier G|] ==> h x \<in> carrier G'"
+by (auto simp add: hom_def funcset_mem)
+
+lemma hom_zero_closed [simp]:
+ "[|h \<in> hom G G'; group G|] ==> h (zero G) \<in> carrier G'"
+by (auto simp add: hom_closed)
+
+text{*Or just @{text "group_hom.hom_zero [OF group_homI]"}*}
+lemma hom_zero [simp]:
+ "[|h \<in> hom G G'; group G; group G'|] ==> h (zero G) = zero G'"
+by (simp add: group.idempotent_imp_zero hom_sum [of h, symmetric])
+
+lemma hom_minus_closed [simp]:
+ "[|h \<in> hom G G'; x \<in> carrier G; group G|]
+ ==> h (gminus G x) \<in> carrier G'"
+by (simp add: hom_closed)
+
+text{*Or just @{text "group_hom.hom_minus [OF group_homI]"}*}
+lemma hom_minus [simp]:
+ "[|h \<in> hom G G'; x \<in> carrier G; group G; group G'|]
+ ==> h (gminus G x) = gminus G' (h x)"
+by (simp add: group.minus_unique hom_closed hom_sum [of h, symmetric])
+
+
+text{*This locale uses the subscript notation mentioned by Wenzel in
+@{text "HOL/ex/Locales.thy"}. We fix two groups and a homomorphism between
+them. Then we prove theorems similar to those just above.*}
+
+locale group_homomorphism = group G + group G' +
+ fixes h
+ assumes homh: "h \<in> hom G G'"
+
+lemma (in group_homomorphism) hom_sum [simp]:
+ "[|x \<in> carrier G; y \<in> carrier G|] ==> h (x \<oplus>\<^sub>1 y) = (h x) \<oplus>\<^sub>2 (h y)"
+by (simp add: hom_sum [OF homh])
+
+lemma (in group_homomorphism) hom_zero_closed [simp]: "h \<zero>\<^sub>1 \<in> carrier G'"
+by (simp add: hom_closed [OF homh])
+
+lemma (in group_homomorphism) hom_zero [simp]: "h \<zero>\<^sub>1 = \<zero>\<^sub>2"
+by (simp add: idempotent_imp_zero hom_sum [symmetric])
+
+lemma (in group_homomorphism) hom_minus_closed [simp]:
+ "x \<in> carrier G ==> h (\<ominus>x) \<in> carrier G'"
+by (simp add: hom_closed [OF homh])
+
+lemma (in group_homomorphism) hom_minus [simp]:
+ "x \<in> carrier G ==> h (\<ominus>\<^sub>1 x) = \<ominus>\<^sub>2 (h x)"
+by (simp add: minus_unique hom_closed [OF homh] hom_sum [symmetric])
+
+text{*Necessary because the standard theorem
+ @{text "group_homomorphism.intro"} is unnatural.*}
+lemma group_homomorphismI:
+ "[|group G; group G'; h \<in> hom G G'|] ==> group_homomorphism G G' h"
+by (simp add: group_def group_homomorphism_def group_homomorphism_axioms_def)
+
end
-
+
--- a/src/HOL/GroupTheory/Homomorphism.ML Wed Sep 25 11:23:26 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,267 +0,0 @@
-(* Title: HOL/GroupTheory/Homomorphism
- ID: $Id$
- Author: Florian Kammueller, with new proofs by L C Paulson
- Copyright 1998-2001 University of Cambridge
-
-Homomorphisms of groups, rings, and automorphisms.
-Sigma version with Locales
-*)
-
-Open_locale "bij";
-
-Addsimps [B_def, o'_def, inv'_def];
-
-Goal "[|x \\<in> S; f \\<in> B|] ==> EX x'. x = f x'";
-by (dtac BijE2 1);
-by Auto_tac;
-
-
-Goal "[| f \\<in> B; g \\<in> S \\<rightarrow> S \\<rightarrow> S; x \\<in> S; y \\<in> S;\
-\ \\<forall>x \\<in> S. \\<forall>y \\<in> S. f(g x y) = g (f x) (f y) |] \
-\ ==> inv' f (g x y) = g (inv' f x) (inv' f y)";
-by (subgoal_tac "EX x':S. EX y':S. x = f x' & y = f y'" 1);
-by (blast_tac (claset() addDs [BijE2]) 2);
-by (Clarify_tac 1);
-(*the next step could be avoided if we could re-orient the quanitifed
- assumption, to rewrite g (f x') (f y') ...*)
-by (rtac inj_onD 1);
-by (etac BijE3 1);
-by (asm_full_simp_tac (simpset() addsimps [f_Inv_f, Inv_f_f, BijE2, BijE3,
- funcset_mem RS funcset_mem]) 1);
-by (ALLGOALS
- (asm_full_simp_tac
- (simpset() addsimps [funcset_mem RS funcset_mem, BijE2, Inv_mem])));
-qed "Bij_op_lemma";
-
-Goal "[| a \\<in> B; b \\<in> B; g \\<in> S \\<rightarrow> S \\<rightarrow> S; x \\<in> S; y \\<in> S; \
-\ \\<forall>x \\<in> S. \\<forall>y \\<in> S. a (b (g x y)) = g (a (b x)) (a (b y)) |] \
-\ ==> (a o' b) (g x y) = g ((a o' b) x) ((a o' b) y)";
-by (afs [o'_def, compose_eq, B_def,
- funcset_mem RS funcset_mem] 1);
-qed "Bij_comp_lemma";
-
-
-Goal "[| R1 \\<in> Ring; R2 \\<in> Ring |] \
-\ ==> RingHom `` {R1} `` {R2} = \
-\ {Phi. Phi \\<in> (R1.<cr>) \\<rightarrow> (R2.<cr>) & \
-\ (\\<forall>x \\<in> (R1.<cr>). \\<forall>y \\<in> (R1.<cr>). \
-\ (Phi((R1.<f>) x y) = (R2.<f>) (Phi x) (Phi y))) &\
-\ (\\<forall>x \\<in> (R1.<cr>). \\<forall>y \\<in> (R1.<cr>). \
-\ (Phi((R1.<m>) x y) = (R2.<m>) (Phi x) (Phi y)))}";
-by (afs [Image_def,RingHom_def] 1);
-qed "RingHom_apply";
-
-(* derive the defining properties as single lemmas *)
-Goal "(R1,R2,Phi) \\<in> RingHom ==> Phi \\<in> (R1.<cr>) \\<rightarrow> (R2.<cr>)";
-by (afs [RingHom_def] 1);
-qed "RingHom_imp_funcset";
-
-Goal "[| (R1,R2,Phi) \\<in> RingHom; x \\<in> (R1.<cr>); y \\<in> (R1.<cr>) |] \
-\ ==> Phi((R1.<f>) x y) = (R2.<f>) (Phi x) (Phi y)";
-by (afs [RingHom_def] 1);
-qed "RingHom_preserves_rplus";
-
-Goal "[| (R1,R2,Phi) \\<in> RingHom; x \\<in> (R1.<cr>); y \\<in> (R1.<cr>) |] \
-\ ==> Phi((R1.<m>) x y) = (R2.<m>) (Phi x) (Phi y)";
-by (afs [RingHom_def] 1);
-qed "RingHom_preserves_rmult";
-
-Goal "[| R1 \\<in> Ring; R2 \\<in> Ring; Phi \\<in> (R1.<cr>) \\<rightarrow> (R2.<cr>); \
-\ \\<forall>x \\<in> (R1.<cr>). \\<forall>y \\<in> (R1.<cr>). \
-\ Phi((R1.<f>) x y) = (R2.<f>) (Phi x) (Phi y);\
-\ \\<forall>x \\<in> (R1.<cr>). \\<forall>y \\<in> (R1.<cr>). \
-\ Phi((R1.<m>) x y) = (R2.<m>) (Phi x) (Phi y)|]\
-\ ==> (R1,R2,Phi) \\<in> RingHom";
-by (afs [RingHom_def] 1);
-qed "RingHomI";
-
-Open_locale "ring";
-
-val Ring_R = thm "Ring_R";
-val rmult_def = thm "rmult_def";
-
-Addsimps [simp_R, Ring_R];
-
-
-
-(* RingAutomorphisms *)
-Goal "RingAuto `` {R} = \
-\ {Phi. (R,R,Phi) \\<in> RingHom & inj_on Phi (R.<cr>) & Phi ` (R.<cr>) = (R.<cr>)}";
-by (rewtac RingAuto_def);
-by (afs [Image_def] 1);
-qed "RingAuto_apply";
-
-Goal "(R,Phi) \\<in> RingAuto ==> (R, R, Phi) \\<in> RingHom";
-by (afs [RingAuto_def] 1);
-qed "RingAuto_imp_RingHom";
-
-Goal "(R,Phi) \\<in> RingAuto ==> inj_on Phi (R.<cr>)";
-by (afs [RingAuto_def] 1);
-qed "RingAuto_imp_inj_on";
-
-Goal "(R,Phi) \\<in> RingAuto ==> Phi ` (R.<cr>) = (R.<cr>)";
-by (afs [RingAuto_def] 1);
-qed "RingAuto_imp_preserves_R";
-
-Goal "(R,Phi) \\<in> RingAuto ==> Phi \\<in> (R.<cr>) \\<rightarrow> (R.<cr>)";
-by (etac (RingAuto_imp_RingHom RS RingHom_imp_funcset) 1);
-qed "RingAuto_imp_funcset";
-
-Goal "[| (R,R,Phi) \\<in> RingHom; \
-\ inj_on Phi (R.<cr>); \
-\ Phi ` (R.<cr>) = (R.<cr>) |]\
-\ ==> (R,Phi) \\<in> RingAuto";
-by (afs [RingAuto_def] 1);
-qed "RingAutoI";
-
-
-(* major result: RingAutomorphism builds a group *)
-(* We prove that they are a subgroup of the bijection group.
- Note!!! Here we need "RingAuto `` {R} ~= {}", (as a result from the
- resolution with subgroupI). That is, this is an example where one might say
- the discipline of Pi types pays off, because there we have the proof basically
- already there (compare the Pi-version).
- Here in the Sigma version, we have to redo now the proofs (or slightly
- adapted verisions) of promoteRingHom and promoteRingAuto *)
-
-Goal "RingAuto `` {R} ~= {}";
-by (stac RingAuto_apply 1);
-by Auto_tac;
-by (res_inst_tac [("x","%y: (R.<cr>). y")] exI 1);
-by (auto_tac (claset(), simpset() addsimps [inj_on_def]));
-by (asm_full_simp_tac (simpset() addsimps [RingHom_def, restrictI,
- R_binop_def, symmetric (rmult_def), rplus_closed, rmult_closed]) 1);
-qed "RingAutoEx";
-
-Goal "(R,f) \\<in> RingAuto ==> f \\<in> Bij (R.<cr>)";
-by (afs [RingAuto_imp_RingHom RS RingHom_imp_funcset, RingAuto_imp_inj_on,
- RingAuto_imp_preserves_R, export BijI] 1);
-qed "RingAuto_Bij";
-Addsimps [RingAuto_Bij];
-
-Goal "[| (R,a) \\<in> RingAuto; (R,b) \\<in> RingAuto; \
-\ g \\<in> (R.<cr>) \\<rightarrow> (R.<cr>) \\<rightarrow> (R.<cr>); x \\<in> carrier R; y \\<in> carrier R; \
-\ \\<forall>Phi. (R,Phi) \\<in> RingAuto --> \
-\ (\\<forall>x \\<in> (R.<cr>). \\<forall>y \\<in> (R.<cr>). Phi(g x y) = g(Phi x) (Phi y)) |] \
-\ ==> compose (R.<cr>) a b (g x y) = \
-\ g (compose (R.<cr>) a b x) (compose (R.<cr>) a b y)";
-by (asm_simp_tac (simpset() addsimps [export Bij_comp_lemma,
- RingAuto_imp_funcset RS funcset_mem]) 1);
-qed "Auto_comp_lemma";
-
-Goal "[|(R, a) \\<in> RingAuto; x \\<in> carrier R; y \\<in> carrier R|] \
-\ ==> Inv (carrier R) a (x ## y) = \
-\ Inv (carrier R) a x ## Inv (carrier R) a y";
-by (rtac (export Bij_op_lemma) 1);
-by (etac RingAuto_Bij 1);
-by (rtac rplus_funcset 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [R_binop_def RS sym,
- RingAuto_imp_RingHom RS RingHom_preserves_rplus]) 1);
-qed "Inv_rplus_lemma";
-
-Goal "(R,a) \\<in> RingAuto \
-\ ==> (R, grouptype.inverse (BijGroup (carrier R)) a) \\<in> RingAuto";
-by (rtac RingAutoI 1);
-by (afs [BijGroup_def, export (restrict_Inv_Bij RS BijE3)] 2);
-by (afs [BijGroup_def, export (restrict_Inv_Bij RS BijE2)] 2);
-by (rtac RingHomI 1);
-by (rtac (Ring_R) 1);
-by (rtac (Ring_R) 1);
-(* ... ==> (BijGroup (R .<R>) .<inv>) a \\<in> (R .<R>) \\<rightarrow> (R .<R>) *)
-by (asm_simp_tac (simpset() addsimps [BijGroup_def,
- export restrict_Inv_Bij RS export BijE1]) 1);
-by (asm_simp_tac (simpset() addsimps [BijGroup_def, R_binop_def, rplus_closed, Inv_rplus_lemma]) 1);
-by (afs [BijGroup_def, symmetric (rmult_def), rmult_closed] 1);
-by (afs [export Bij_op_lemma, rmult_funcset, rmult_def,
- RingAuto_imp_RingHom RS RingHom_preserves_rmult] 1);
-qed "inverse_BijGroup_lemma";
-
-Goal "[|(R, a) \\<in> RingAuto; (R, b) \\<in> RingAuto|] \
-\ ==> (R, bin_op (BijGroup (carrier R)) a b) \\<in> RingAuto";
-by (afs [BijGroup_def] 1);
-by (rtac RingAutoI 1);
-by (rtac RingHomI 1);
-by (rtac (Ring_R) 1);
-by (rtac (Ring_R) 1);
-by (afs [RingAuto_Bij,export compose_Bij,export BijE1] 1);
-by (Clarify_tac 1);
-by (rtac Auto_comp_lemma 1);
-by (ALLGOALS Asm_full_simp_tac);
-by (asm_full_simp_tac (simpset() addsimps [R_binop_def, rplus_funcset]) 1);
-by (blast_tac (claset() addIs [RingAuto_imp_RingHom RS RingHom_preserves_rplus]) 1);
-by (Clarify_tac 1);
-by (rtac Auto_comp_lemma 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [rmult_funcset]) 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (blast_tac (claset() addIs [RingAuto_imp_RingHom RS RingHom_preserves_rmult]) 1);
-(* ==> inj_on (compose (R .<R>) a b) (R .<R>) *)
-by (blast_tac (claset() delrules [equalityI]
- addIs [inj_on_compose, RingAuto_imp_inj_on,
- RingAuto_imp_funcset, RingAuto_imp_preserves_R]) 1);
-(* ==> compose (R .<R>) a b ` (R .<R>) = (R .<R>) *)
-by (blast_tac (claset() delrules [equalityI]
- addIs [surj_compose, RingAuto_imp_funcset, RingAuto_imp_preserves_R]) 1);
-qed "binop_BijGroup_lemma";
-
-
-(* Ring automorphisms are a subgroup of the group of bijections over the
- ring's carrier, and thus a group *)
-Goal "RingAuto `` {R} <<= BijGroup (R.<cr>)";
-by (rtac SubgroupI 1);
-by (rtac (export Bij_are_Group) 1);
-(* 1. RingAuto `` {R} <= (BijGroup (R .<R>) .<cr>) *)
-by (afs [subset_def, BijGroup_def, Bij_def,
- RingAuto_imp_RingHom RS RingHom_imp_funcset, RingAuto_imp_inj_on,
- RingAuto_imp_preserves_R, Image_def] 1);
-(* 1. !!R. R \\<in> Ring ==> RingAuto `` {R} ~= {} *)
-by (rtac RingAutoEx 1);
-by (auto_tac (claset(),
- simpset() addsimps [inverse_BijGroup_lemma, binop_BijGroup_lemma]));
-qed "RingAuto_SG_BijGroup";
-
-Delsimps [simp_R, Ring_R];
-
-Close_locale "ring";
-Close_locale "group";
-
-val RingAuto_are_Group = (export RingAuto_SG_BijGroup) RS (export Bij_are_Group RS SubgroupE2);
-(* So far:
-"[| ?R2 \\<in> Ring; group_of ?R2 \\<in> Group |]
- ==> (| carrier = RingAuto `` {?R2},
- bin_op =
- %x:RingAuto `` {?R2}.
- restrict ((BijGroup (?R2 .<cr>) .<f>) x) (RingAuto `` {?R2}),
- inverse = restrict (BijGroup (?R2 .<cr>) .<inv>) (RingAuto `` {?R2}),
- unit = BijGroup (?R2 .<cr>) .<e> |) \\<in> Group" *)
-
-(* Unfortunately we have to eliminate the extra assumptions
-Now only group_of R \\<in> Group *)
-
-Goal "R \\<in> Ring ==> group_of R \\<in> Group";
-by (asm_full_simp_tac (simpset() addsimps [group_of_def]) 1);
-by (rtac Abel_imp_Group 1);
-by (etac (export R_Abel) 1);
-qed "R_Group";
-
-Goal "R \\<in> Ring ==> (| carrier = RingAuto `` {R},\
-\ bin_op = %x:RingAuto `` {R}. %y: RingAuto `` {R}.\
-\ (BijGroup (R.<cr>) .<f>) x y ,\
-\ inverse = %x: RingAuto `` {R}. (BijGroup (R.<cr>) .<inv>) x,\
-\ unit = BijGroup (R.<cr>) .<e> |) \\<in> Group";
-by (rtac (R_Group RSN (2, RingAuto_are_Group)) 1);
-by (assume_tac 1);
-by (assume_tac 1);
-qed "RingAuto_are_Groupf";
-
-(* "?R \\<in> Ring
- ==> (| carrier = RingAuto `` {?R},
- bin_op =
- %x:RingAuto `` {?R}.
- restrict ((BijGroup (?R .<cr>) .<f>) x) (RingAuto `` {?R}),
- inverse = restrict (BijGroup (?R .<cr>) .<inv>) (RingAuto `` {?R}),
- unit = BijGroup (?R .<cr>) .<e> |) \\<in> Group" *)
--- a/src/HOL/GroupTheory/Homomorphism.thy Wed Sep 25 11:23:26 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-(* Title: HOL/GroupTheory/Homomorphism
- ID: $Id$
- Author: Florian Kammueller, with new proofs by L C Paulson
- Copyright 1998-2001 University of Cambridge
-
-Homomorphisms of groups, rings, and automorphisms.
-Sigma version with Locales
-*)
-
-Homomorphism = Ring + Bij +
-
-consts
- Hom :: "('a grouptype * 'b grouptype * ('a => 'b)) set"
-
-defs
- Hom_def "Hom == \\<Sigma>G \\<in> Group. \\<Sigma>H \\<in> Group. {Phi. Phi \\<in> (G.<cr>) \\<rightarrow> (H.<cr>) &
- (\\<forall>x \\<in> (G.<cr>) . \\<forall>y \\<in> (G.<cr>) . (Phi((G.<f>) x y) = (H.<f>) (Phi x)(Phi y)))}"
-
-consts
- RingHom :: "(('a ringtype) * ('b ringtype) * ('a => 'b))set"
-defs
- RingHom_def "RingHom == \\<Sigma>R1 \\<in> Ring. \\<Sigma>R2 \\<in> Ring. {Phi. Phi \\<in> (R1.<cr>) \\<rightarrow> (R2.<cr>) &
- (\\<forall>x \\<in> (R1.<cr>). \\<forall>y \\<in> (R1.<cr>). (Phi((R1.<f>) x y) = (R2.<f>) (Phi x) (Phi y))) &
- (\\<forall>x \\<in> (R1.<cr>). \\<forall>y \\<in> (R1.<cr>). (Phi((R1.<m>) x y) = (R2.<m>) (Phi x) (Phi y)))}"
-
-consts
- GroupAuto :: "('a grouptype * ('a => 'a)) set"
-
-defs
- GroupAuto_def "GroupAuto == \\<Sigma>G \\<in> Group. {Phi. (G,G,Phi)\\<in>Hom &
- inj_on Phi (G.<cr>) & Phi ` (G.<cr>) = (G.<cr>)}"
-
-consts
- RingAuto :: "(('a ringtype) * ('a => 'a))set"
-
-defs
- RingAuto_def "RingAuto == \\<Sigma>R \\<in> Ring. {Phi. (R,R,Phi)\\<in>RingHom &
- inj_on Phi (R.<cr>) & Phi ` (R.<cr>) = (R.<cr>)}"
-
-end
\ No newline at end of file
--- a/src/HOL/GroupTheory/PiSets.ML Wed Sep 25 11:23:26 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,66 +0,0 @@
-(* Title: HOL/ex/PiSets.ML
- ID: $Id$
- Author: Florian Kammueller, University of Cambridge
-
-Pi sets and their application.
-*)
-
-(*** Bijection between Pi in terms of => and Pi in terms of Sigma ***)
-Goal "f \\<in> Pi A B ==> PiBij A B f <= Sigma A B";
-by (auto_tac (claset(), simpset() addsimps [PiBij_def,Pi_def]));
-qed "PiBij_subset_Sigma";
-
-Goal "f \\<in> Pi A B ==> \\<forall>x \\<in> A. \\<exists>!y. (x, y) \\<in> (PiBij A B f)";
-by (auto_tac (claset(), simpset() addsimps [PiBij_def]));
-qed "PiBij_unique";
-
-Goal "f \\<in> Pi A B ==> PiBij A B f \\<in> Graph A B";
-by (asm_simp_tac (simpset() addsimps [Graph_def,PiBij_unique,
- PiBij_subset_Sigma]) 1);
-qed "PiBij_in_Graph";
-
-Goalw [PiBij_def, Graph_def] "PiBij A B \\<in> Pi A B \\<rightarrow> Graph A B";
-by (rtac restrictI 1);
-by (auto_tac (claset(), simpset() addsimps [Pi_def]));
-qed "PiBij_func";
-
-Goal "inj_on (PiBij A B) (Pi A B)";
-by (rtac inj_onI 1);
-by (rtac Pi_extensionality 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [PiBij_def]) 1);
-by (Blast_tac 1);
-qed "inj_PiBij";
-
-
-Goal "x \\<in> Graph A B \\<Longrightarrow> (%a:A. SOME y. (a, y) \\<in> x) \\<in> Pi A B";
-by (rtac restrictI 1);
-by (res_inst_tac [("P", "%xa. (a, xa)\\<in>x")] ex1E 1);
- by (force_tac (claset(), simpset() addsimps [Graph_def]) 1);
-by (full_simp_tac (simpset() addsimps [Graph_def]) 1);
-by (stac some_equality 1);
- by (assume_tac 1);
- by (Blast_tac 1);
-by (Blast_tac 1);
-qed "in_Graph_imp_in_Pi";
-
-Goal "PiBij A B ` (Pi A B) = Graph A B";
-by (rtac equalityI 1);
-by (force_tac (claset(), simpset() addsimps [PiBij_in_Graph]) 1);
-by (rtac subsetI 1);
-by (rtac image_eqI 1);
-by (etac in_Graph_imp_in_Pi 2);
-(* x = PiBij A B (%a:A. @ y. (a, y)\\<in>x) *)
-by (asm_simp_tac (simpset() addsimps [in_Graph_imp_in_Pi, PiBij_def]) 1);
-by (auto_tac (claset(), simpset() addsimps [some1_equality, Graph_def]));
-by (fast_tac (claset() addIs [someI2]) 1);
-qed "surj_PiBij";
-
-Goal "f \\<in> Pi A B ==> Inv (Pi A B) (PiBij A B) (PiBij A B f) = f";
-by (asm_simp_tac (simpset() addsimps [Inv_f_f, inj_PiBij]) 1);
-qed "PiBij_bij1";
-
-Goal "f \\<in> Graph A B ==> PiBij A B (Inv (Pi A B) (PiBij A B) f) = f";
-by (asm_simp_tac (simpset() addsimps [f_Inv_f, surj_PiBij]) 1);
-qed "PiBij_bij2";
--- a/src/HOL/GroupTheory/PiSets.thy Wed Sep 25 11:23:26 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-(* Title: HOL/ex/PiSets.thy
- ID: $Id$
- Author: Florian Kammueller, University of Cambridge
-
-The bijection between elements of the Pi set and functional graphs
-*)
-
-PiSets = Group +
-
-constdefs
-(* bijection between Pi_sig and Pi_=> *)
- PiBij :: "['a set, 'a => 'b set, 'a => 'b] => ('a * 'b) set"
- "PiBij A B == %f: Pi A B. {(x, y). x: A & y = f x}"
-
- Graph :: "['a set, 'a => 'b set] => ('a * 'b) set set"
- "Graph A B == {f. f \\<in> Pow(Sigma A B) & (\\<forall>x\\<in>A. \\<exists>!y. (x, y) \\<in> f)}"
-
-end
--- a/src/HOL/GroupTheory/README.html Wed Sep 25 11:23:26 2002 +0200
+++ b/src/HOL/GroupTheory/README.html Thu Sep 26 10:40:13 2002 +0200
@@ -11,32 +11,20 @@
Here is an outline of the directory's contents:
-<UL>
+<UL> <LI>Theory <A HREF="Group.html"><CODE>Group</CODE></A> defines
+semigroups, groups, homomorphisms and the subgroup relation. It also defines
+the product of two groups. It defines the factorization of a group and shows
+that the factorization a normal subgroup is a group.
+
<LI>Theory <A HREF="Bij.html"><CODE>Bij</CODE></A>
defines bijections over sets and operations on them and shows that they
-are a group.
-
-<LI>Theory <A HREF="DirProd.html"><CODE>DirProd</CODE></A>
-defines the product of two groups and proves that it is a group again.
-
-<LI>Theory <A HREF="FactGroup.html"><CODE>FactGroup</CODE></A>
-defines the factorization of a group and shows that the factorization a
-normal subgroup is a group.
+are a group. It shows that automorphisms form a group.
-<LI>Theory <A HREF="Homomorphism.html"><CODE>Homomorphism</CODE></A>
-defines homomorphims and automorphisms for groups and rings and shows that
-ring automorphisms are a group by using the previous result for
-bijections.
-
-<LI>Theory <A HREF="Ring.html"><CODE>Ring</CODE></A>
-and <A HREF="RingConstr.html"><CODE>RingConstr</CODE></A>
-defines rings, proves a few basic theorems and constructs a lambda
-function to extract the group that is part of the ring showing that it is
-an abelian group.
+<LI>Theory <A HREF="Ring.html"><CODE>Ring</CODE></A> defines rings and proves
+a few basic theorems. Ring automorphisms are shown to form a group.
<LI>Theory <A HREF="Sylow.html"><CODE>Sylow</CODE></A>
contains a proof of the first Sylow theorem.
-
</UL>
<HR>
--- a/src/HOL/GroupTheory/ROOT.ML Wed Sep 25 11:23:26 2002 +0200
+++ b/src/HOL/GroupTheory/ROOT.ML Thu Sep 26 10:40:13 2002 +0200
@@ -1,7 +1,5 @@
-
no_document use_thy "Primes";
+no_document use_thy "FuncSet";
-use_thy "DirProd";
use_thy "Sylow";
-use_thy "RingConstr";
-use_thy "PiSets";
+use_thy "Ring";
--- a/src/HOL/GroupTheory/Ring.ML Wed Sep 25 11:23:26 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,138 +0,0 @@
-(* Title: HOL/GroupTheory/Ring
- ID: $Id$
- Author: Florian Kammueller, with new proofs by L C Paulson
- Copyright 1998-2001 University of Cambridge
-
-Ring theory. Sigma version
-*)
-
-Goal
-"[| (| carrier = carrier R, bin_op = R .<f>, \
-\ inverse = R .<inv>, unit = R .<e> |) \\<in> AbelianGroup;\
-\ (R.<m>) \\<in> (carrier R) \\<rightarrow> (carrier R) \\<rightarrow> (carrier R); \
-\ \\<forall>x \\<in> carrier R. \\<forall>y \\<in> carrier R. \\<forall>z \\<in> carrier R. (R.<m>) x ((R.<m>) y z) = (R.<m>) ((R.<m>) x y) z;\
-\ distr_l (carrier R)(R.<m>)(R.<f>); distr_r (carrier R)(R.<m>)(R.<f>) |]\
-\ ==> R \\<in> Ring";
-by (afs [Ring_def] 1);
-qed "RingI";
-
-Open_locale "ring";
-
-val simp_R = simplify (simpset() addsimps [Ring_def]) (thm "Ring_R");
-
-Addsimps [simp_R, thm "Ring_R", thm "rmult_def",thm "R_id_G"];
-
-Goal "(| carrier = (carrier R), bin_op = (R.<f>), inverse = (R.<inv>), \
-\ unit = (R.<e>) |) \\<in> AbelianGroup";
-by (Asm_full_simp_tac 1);
-qed "R_Abel";
-
-Goal "group_of R \\<in> AbelianGroup";
-by (afs [group_of_def] 1);
-qed "R_forget";
-
-Goal "((group_of R).<cr>) = (carrier R)";
-by (afs [group_of_def] 1);
-qed "FR_carrier";
-
-Goal "(G.<cr>) = (carrier R)";
-by (simp_tac (simpset() addsimps [FR_carrier RS sym]) 1);
-qed "R_carrier_def";
-
-Goal "((group_of R).<f>) = op ##";
-by (afs [binop_def, thm "R_id_G"] 1);
-qed "FR_bin_op";
-
-Goal "(R.<f>) = op ##";
-by (afs [FR_bin_op RS sym, group_of_def] 1);
-qed "R_binop_def";
-
-Goal "((group_of R).<inv>) = INV";
-by (afs [thm "inv_def"] 1);
-qed "FR_inverse";
-
-Goal "(R.<inv>) = INV";
-by (afs [FR_inverse RS sym, group_of_def] 1);
-qed "R_inv_def";
-
-Goal "((group_of R).<e>) = e";
-by (afs [thm "e_def"] 1);
-qed "FR_unit";
-
-Goal "(R.<e>) = e";
-by (afs [FR_unit RS sym, group_of_def] 1);
-qed "R_unit_def";
-
-Goal "G \\<in> AbelianGroup";
-by (afs [group_of_def] 1);
-qed "G_abelian";
-
-
-Delsimps [thm "R_id_G"]; (*needed below?*)
-
-Goal "[| x \\<in> (G.<cr>); y \\<in> (G.<cr>) |] ==> x ## y = y ## x";
-by (afs [thm "binop_def", G_abelian RS Group_commute] 1);
-qed "binop_commute";
-
-Goal "op ** \\<in> (carrier R) \\<rightarrow> (carrier R) \\<rightarrow> (carrier R)";
-by (simp_tac (simpset() addsimps [thm "rmult_def"]) 1);
-qed "rmult_funcset";
-
-Goal "[| x \\<in> (carrier R); y \\<in> (carrier R) |] ==> x ** y \\<in> (carrier R)";
-by (blast_tac
- (claset() addIs [rmult_funcset RS funcset_mem RS funcset_mem]) 1);
-qed "rmult_closed";
-
-Goal "[|x \\<in> (carrier R); y \\<in> (carrier R); z \\<in> (carrier R)|] \
-\ ==> x **(y ** z) = (x ** y)** z";
-by (Asm_full_simp_tac 1);
-qed "rmult_assoc";
-
-Goal "[|x \\<in> (carrier R); y \\<in> (carrier R); z \\<in> (carrier R)|] \
-\ ==> x **(y ## z) = (x ** y) ## (x ** z)";
-by (cut_facts_tac [thm "Ring_R"] 1);
-by (asm_full_simp_tac (simpset() delsimps [thm "Ring_R", simp_R]
- addsimps [Ring_def, distr_l_def, R_binop_def]) 1);
-qed "R_distrib1";
-
-
-(* The following have been in the earlier version without locales and the
-record extension proofs in which we needed to use conversion functions to
-establish these facts. We can transfer all facts that are
-derived for groups to rings now. The subsequent proofs are not really hard
-proofs, they are just instantiations of the known facts to rings. This is
-because the elements of the ring and the group are now identified!! Before, in
-the older version we could do something similar, but we always had to go the
-longer way, via the implication R \\<in> Ring ==> R \\<in> Abelian group and then
-conversion functions for the operators *)
-
-Goal "e \\<in> carrier R";
-by (afs [R_carrier_def RS sym,e_closed] 1);
-qed "R_e_closed";
-
-Goal "\\<forall>x \\<in> carrier R. e ## x = x";
-by (afs [R_carrier_def RS sym,e_ax1] 1);
-qed "R_e_ax1";
-
-Goal "op ## \\<in> carrier R \\<rightarrow> carrier R \\<rightarrow> carrier R";
-by (afs [R_carrier_def RS sym, binop_funcset] 1);
-qed "rplus_funcset";
-
-Goal "[| x \\<in> carrier R; y \\<in> carrier R |] ==> x ## y \\<in> carrier R";
-by (afs [rplus_funcset RS funcset_mem RS funcset_mem] 1);
-qed "rplus_closed";
-
-Goal "[| a \\<in> carrier R; a ## a = a |] ==> a = e";
-by (afs [ R_carrier_def RS sym, idempotent_e] 1);
-qed "R_idempotent_e";
-
-Delsimps [simp_R, thm "Ring_R", thm "rmult_def", thm "R_id_G"];
-
-Goal "e ** e = e";
-by (rtac R_idempotent_e 1);
-by (blast_tac (claset() addIs [rmult_closed, R_e_closed]) 1);
-by (simp_tac (simpset() addsimps [R_distrib1 RS sym, R_e_closed]) 1);
-qed "R_e_mult_base";
-
-Close_locale "ring";
-Close_locale "group";
--- a/src/HOL/GroupTheory/Ring.thy Wed Sep 25 11:23:26 2002 +0200
+++ b/src/HOL/GroupTheory/Ring.thy Thu Sep 26 10:40:13 2002 +0200
@@ -1,60 +1,204 @@
(* Title: HOL/GroupTheory/Ring
ID: $Id$
Author: Florian Kammueller, with new proofs by L C Paulson
- Copyright 1998-2001 University of Cambridge
-Ring theory. Sigma version
*)
-Ring = Coset +
+header{*Ring Theory*}
+
+theory Ring = Bij + Coset:
+
+
+subsection{*Definition of a Ring*}
+
+record 'a ring = "'a group" +
+ prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<cdot>\<index>" 70)
+
+record 'a unit_ring = "'a ring" +
+ one :: 'a ("\<one>\<index>")
+
+
+text{*Abbrevations for the left and right distributive laws*}
+constdefs
+ distrib_l :: "['a set, ['a, 'a] => 'a, ['a, 'a] => 'a] => bool"
+ "distrib_l A f g ==
+ (\<forall>x \<in> A. \<forall>y \<in> A. \<forall>z \<in> A. (f x (g y z) = g (f x y) (f x z)))"
-record 'a ringtype = 'a grouptype +
- Rmult :: "['a, 'a] => 'a"
+ distrib_r :: "['a set, ['a, 'a] => 'a, ['a, 'a] => 'a] => bool"
+ "distrib_r A f g ==
+ (\<forall>x \<in> A. \<forall>y \<in> A. \<forall>z \<in> A. (f (g y z) x = g (f y x) (f z x)))"
+
+
+locale ring = abelian_group R +
+ assumes prod_funcset: "prod R \<in> carrier R \<rightarrow> carrier R \<rightarrow> carrier R"
+ and prod_assoc:
+ "[|x \<in> carrier R; y \<in> carrier R; z \<in> carrier R|]
+ ==> (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
+ and left: "distrib_l (carrier R) (prod R) (sum R)"
+ and right: "distrib_r (carrier R) (prod R) (sum R)"
+
+constdefs (*????FIXME needed?*)
+ Ring :: "('a,'b) ring_scheme set"
+ "Ring == Collect ring"
+
+
+lemma ring_is_abelian_group: "ring(R) ==> abelian_group(R)"
+by (simp add: ring_def abelian_group_def)
-syntax
- "@Rmult" :: "('a ringtype) => (['a, 'a] => 'a)" ("_ .<m>" [10] 10)
+text{*Construction of a ring from a semigroup and an Abelian group*}
+lemma "[|abelian_group R;
+ semigroup(|carrier = carrier R, sum = prod R|);
+ distrib_l (carrier R) (prod R) (sum R);
+ distrib_r (carrier R) (prod R) (sum R)|] ==> ring R"
+by (simp add: abelian_group_def ring_def ring_axioms_def semigroup_def)
+
+lemma (in ring) prod_closed [simp]:
+ "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<cdot> y \<in> carrier R"
+apply (insert prod_funcset)
+apply (blast dest: funcset_mem)
+done
+
+declare ring.prod_closed [simp]
+
+lemma (in ring) sum_closed:
+ "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<oplus> y \<in> carrier R"
+by simp
+
+declare ring.sum_closed [simp]
-translations
- "R.<m>" == "Rmult R"
+lemma (in ring) distrib_left:
+ "[|x \<in> carrier R; y \<in> carrier R; z \<in> carrier R|]
+ ==> x \<cdot> (y \<oplus> z) = (x \<cdot> y) \<oplus> (x \<cdot> z)"
+apply (insert left)
+apply (simp add: distrib_l_def)
+done
+
+lemma (in ring) distrib_right:
+ "[|x \<in> carrier R; y \<in> carrier R; z \<in> carrier R|]
+ ==> (y \<oplus> z) \<cdot> x = (y \<cdot> x) \<oplus> (z \<cdot> x)"
+apply (insert right)
+apply (simp add: distrib_r_def)
+done
+
+lemma (in ring) prod_zero_left: "x \<in> carrier R ==> \<zero> \<cdot> x = \<zero>"
+by (simp add: idempotent_imp_zero distrib_right [symmetric])
+
+lemma (in ring) prod_zero_right: "x \<in> carrier R ==> x \<cdot> \<zero> = \<zero>"
+by (simp add: idempotent_imp_zero distrib_left [symmetric])
+
+lemma (in ring) prod_minus_left:
+ "[|x \<in> carrier R; y \<in> carrier R|]
+ ==> (\<ominus>x) \<cdot> y = \<ominus> (x \<cdot> y)"
+by (simp add: minus_unique prod_zero_left distrib_right [symmetric])
+
+lemma (in ring) prod_minus_right:
+ "[|x \<in> carrier R; y \<in> carrier R|]
+ ==> x \<cdot> (\<ominus>y) = \<ominus> (x \<cdot> y)"
+by (simp add: minus_unique prod_zero_right distrib_left [symmetric])
+
+
+subsection {*Ring Homomorphisms*}
constdefs
- distr_l :: "['a set, ['a, 'a] => 'a, ['a, 'a] => 'a] => bool"
- "distr_l S f1 f2 == (\\<forall>x \\<in> S. \\<forall>y \\<in> S. \\<forall>z \\<in> S.
- (f1 x (f2 y z) = f2 (f1 x y) (f1 x z)))"
- distr_r :: "['a set, ['a, 'a] => 'a, ['a, 'a] => 'a] => bool"
- "distr_r S f1 f2 == (\\<forall>x \\<in> S. \\<forall>y \\<in> S. \\<forall>z \\<in> S.
- (f1 (f2 y z) x = f2 (f1 y x) (f1 z x)))"
+ ring_hom :: "[('a,'c)ring_scheme, ('b,'d)ring_scheme] => ('a => 'b)set"
+ "ring_hom R R' ==
+ {h. h \<in> carrier R -> carrier R' &
+ (\<forall>x \<in> carrier R. \<forall>y \<in> carrier R. h(sum R x y) = sum R' (h x) (h y)) &
+ (\<forall>x \<in> carrier R. \<forall>y \<in> carrier R. h(prod R x y) = prod R' (h x) (h y))}"
+
+ ring_auto :: "('a,'b)ring_scheme => ('a => 'a)set"
+ "ring_auto R == ring_hom R R \<inter> Bij(carrier R)"
-consts
- Ring :: "('a ringtype) set"
+ RingAutoGroup :: "[('a,'c) ring_scheme] => ('a=>'a) group"
+ "RingAutoGroup R == BijGroup (carrier R) (|carrier := ring_auto R |)"
+
+
+lemma ring_hom_subset_hom: "ring_hom R R' <= hom R R'"
+by (force simp add: ring_hom_def hom_def)
+
+subsection{*The Ring Automorphisms From a Group*}
+
+lemma id_in_ring_auto: "ring R ==> (%x: carrier R. x) \<in> ring_auto R"
+by (simp add: ring_auto_def ring_hom_def restrictI ring.axioms id_Bij)
-defs
- Ring_def
- "Ring ==
- {R. (| carrier = (R.<cr>), bin_op = (R.<f>),
- inverse = (R.<inv>), unit = (R.<e>) |) \\<in> AbelianGroup &
- (R.<m>) \\<in> (R.<cr>) \\<rightarrow> (R.<cr>) \\<rightarrow> (R.<cr>) &
- (\\<forall>x \\<in> (R.<cr>). \\<forall>y \\<in> (R.<cr>). \\<forall>z \\<in> (R.<cr>).
- ((R.<m>) x ((R.<m>) y z) = (R.<m>) ((R.<m>) x y) z)) &
- distr_l (R.<cr>)(R.<m>)(R.<f>) &
- distr_r (R.<cr>)(R.<m>)(R.<f>) }"
+lemma restrict_Inv_ring_hom:
+ "[|ring R; h \<in> ring_hom R R; h \<in> Bij (carrier R)|]
+ ==> restrict (Inv (carrier R) h) (carrier R) \<in> ring_hom R R"
+by (simp add: ring.axioms group.axioms
+ ring_hom_def Bij_Inv_mem restrictI ring.sum_closed
+ semigroup.sum_funcset ring.prod_funcset Bij_Inv_lemma)
+
+text{*Ring automorphisms are a subgroup of the group of bijections over the
+ ring's carrier, and thus a group*}
+lemma subgroup_ring_auto:
+ "ring R ==> subgroup (ring_auto R) (BijGroup (carrier R))"
+apply (rule group.subgroupI)
+ apply (rule group_BijGroup)
+ apply (force simp add: ring_auto_def BijGroup_def)
+ apply (blast intro: dest: id_in_ring_auto)
+ apply (simp add: ring_auto_def BijGroup_def restrict_Inv_Bij
+ restrict_Inv_ring_hom)
+apply (simp add: ring_auto_def BijGroup_def compose_Bij)
+apply (simp add: ring_hom_def compose_def Pi_def)
+done
+
+lemma ring_auto: "ring R ==> group (RingAutoGroup R)"
+apply (drule subgroup_ring_auto)
+apply (simp add: subgroup_def RingAutoGroup_def)
+done
-constdefs
- group_of :: "'a ringtype => 'a grouptype"
- "group_of == %R: Ring. (| carrier = (R.<cr>), bin_op = (R.<f>),
- inverse = (R.<inv>), unit = (R.<e>) |)"
+subsection{*A Locale for a Pair of Rings and a Homomorphism*}
+
+locale ring_homomorphism = ring R + ring R' +
+ fixes h
+ assumes homh: "h \<in> ring_hom R R'"
+
+lemma ring_hom_sum:
+ "[|h \<in> ring_hom R R'; x \<in> carrier R; y \<in> carrier R|]
+ ==> h(sum R x y) = sum R' (h x) (h y)"
+by (simp add: ring_hom_def)
+
+lemma ring_hom_prod:
+ "[|h \<in> ring_hom R R'; x \<in> carrier R; y \<in> carrier R|]
+ ==> h(prod R x y) = prod R' (h x) (h y)"
+by (simp add: ring_hom_def)
+
+lemma ring_hom_closed:
+ "[|h \<in> ring_hom G G'; x \<in> carrier G|] ==> h x \<in> carrier G'"
+by (auto simp add: ring_hom_def funcset_mem)
+
+lemma (in ring_homomorphism) ring_hom_sum [simp]:
+ "[|x \<in> carrier R; y \<in> carrier R|] ==> h (x \<oplus>\<^sub>1 y) = (h x) \<oplus>\<^sub>2 (h y)"
+by (simp add: ring_hom_sum [OF homh])
-locale ring = group +
- fixes
- R :: "'a ringtype"
- rmult :: "['a, 'a] => 'a" (infixr "**" 80)
- assumes
- Ring_R "R \\<in> Ring"
- defines
- rmult_def "op ** == (R.<m>)"
- R_id_G "G == group_of R"
+lemma (in ring_homomorphism) ring_hom_prod [simp]:
+ "[|x \<in> carrier R; y \<in> carrier R|] ==> h (x \<cdot>\<^sub>1 y) = (h x) \<cdot>\<^sub>2 (h y)"
+by (simp add: ring_hom_prod [OF homh])
+
+lemma (in ring_homomorphism) group_homomorphism: "group_homomorphism R R' h"
+by (simp add: group_homomorphism_def group_homomorphism_axioms_def
+ prems homh ring_hom_subset_hom [THEN subsetD])
+
+lemma (in ring_homomorphism) hom_zero_closed [simp]: "h \<zero>\<^sub>1 \<in> carrier R'"
+by (simp add: ring_hom_closed [OF homh])
+
+lemma (in ring_homomorphism) hom_zero [simp]: "h \<zero>\<^sub>1 = \<zero>\<^sub>2"
+by (rule group_homomorphism.hom_zero [OF group_homomorphism])
+
+lemma (in ring_homomorphism) hom_minus_closed [simp]:
+ "x \<in> carrier R ==> h (\<ominus>x) \<in> carrier R'"
+by (rule group_homomorphism.hom_minus_closed [OF group_homomorphism])
+
+lemma (in ring_homomorphism) hom_minus [simp]:
+ "x \<in> carrier R ==> h (\<ominus>\<^sub>1 x) = \<ominus>\<^sub>2 (h x)"
+by (rule group_homomorphism.hom_minus [OF group_homomorphism])
+
+
+text{*Needed because the standard theorem @{text "ring_homomorphism.intro"}
+is unnatural.*}
+lemma ring_homomorphismI:
+ "[|ring R; ring R'; h \<in> ring_hom R R'|] ==> ring_homomorphism R R' h"
+by (simp add: ring_def ring_homomorphism_def ring_homomorphism_axioms_def)
end
-
-
--- a/src/HOL/GroupTheory/RingConstr.ML Wed Sep 25 11:23:26 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,67 +0,0 @@
-(* Title: HOL/GroupTheory/RingConstr
- ID: $Id$
- Author: Florian Kammueller, with new proofs by L C Paulson
- Copyright 1998-2001 University of Cambridge
-
-Construction of a ring from a semigroup and an Abelian group
-*)
-
-Goal "[| G \\<in> AbelianGroup; S \\<in> Semigroup; (S.<cr>) = (G.<cr>); \
-\ R \\<in> ring_constr `` {G} `` {S} |] \
-\ ==> R \\<in> Ring";
-by (force_tac (claset(),
- simpset() addsimps [Ring_def, ring_constr_def, Abel_Abel,
- Semigroup_def]@[distr_l_def, distr_r_def]) 1);
-qed "RingC_Ring";
-
-Goal "R = (| carrier = R .<cr>, bin_op = R .<f>, inverse = R .<inv>,\
-\ unit = R .<e>, Rmult = R .<m> |)";
-by Auto_tac;
-qed "surjective_Ring";
-
-Goal "R \\<in> Ring \
-\ ==> \\<exists>G \\<in> AbelianGroup. \\<exists>S \\<in> Semigroup. R \\<in> ring_constr `` {G} `` {S}";
-by (res_inst_tac [("x","group_of R")] bexI 1);
-by (afs [Ring_def, group_of_def] 2);
-by (res_inst_tac [("x","(| carrier = (R.<cr>), bin_op = (R.<m>) |)")] bexI 1);
-by (afs [Ring_def, AbelianGroup_def, Semigroup_def] 2);
-(* Now the main conjecture:
- R\\<in>Ring
- ==> R\\<in>ring_constr `` {group_of R} ``
- {(| carrier = R .<cr>, bin_op = R .<m> |)} *)
-by (afs [ring_constr_def, Ring_def, group_of_def, AbelianGroup_def,
- Semigroup_def,distr_l_def,distr_r_def] 1);
-qed "Ring_RingC";
-
-
-Goal "[| G \\<in> AbelianGroup; S \\<in> Semigroup; (S.<cr>) = (G.<cr>); \
-\ distr_l (G .<cr>) (S .<f>) (G .<f>); \
-\ distr_r (G .<cr>) (S .<f>) (G .<f>) |] \
-\ ==> ring_from G S \\<in> Ring";
-by (rtac RingI 1);
-by (ALLGOALS
- (asm_full_simp_tac (simpset() addsimps [ring_from_def, Abel_Abel,
- Semigroup_def])));
-qed "RingFrom_is_Ring";
-
-
-Goal "ring_from \\<in> (PI G : AbelianGroup. {M. M \\<in> Semigroup & (M.<cr>) = (G.<cr>) \
-\ & distr_l (G.<cr>) (M.<f>) (G.<f>) & distr_r (G.<cr>) (M.<f>) (G.<f>)} \\<rightarrow> Ring)";
-by (rtac Pi_I 1);
-by (afs [ring_from_def] 2);
-by (rtac funcsetI 1);
-by (asm_full_simp_tac (simpset() addsimps [ring_from_def]) 2);
-by (Force_tac 2);
-by (afs [RingFrom_is_Ring] 1);
-qed "RingFrom_arity";
-
-(* group_of, i.e. the group in a ring *)
-
-Goal "R \\<in> Ring ==> group_of R \\<in> AbelianGroup";
-by (afs [group_of_def] 1);
-by (etac (export R_Abel) 1);
-qed "group_of_in_AbelianGroup";
-
-val R_Group = group_of_in_AbelianGroup RS Abel_imp_Group;
-
-
--- a/src/HOL/GroupTheory/RingConstr.thy Wed Sep 25 11:23:26 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-(* Title: HOL/GroupTheory/RingConstr
- ID: $Id$
- Author: Florian Kammueller, with new proofs by L C Paulson
- Copyright 1998-2001 University of Cambridge
-
-Construction of a ring from a semigroup and an Abelian group
-*)
-
-RingConstr = Homomorphism +
-
-constdefs
- ring_of :: "['a grouptype, 'a semigrouptype] => 'a ringtype"
- "ring_of ==
- %G: AbelianGroup. %S: {M. M \\<in> Semigroup & (M.<cr>) = (G.<cr>)}.
- (| carrier = (G.<cr>), bin_op = (G.<f>),
- inverse = (G.<inv>), unit = (G.<e>), Rmult = (S.<f>) |)"
-
- ring_constr :: "('a grouptype * 'a semigrouptype *'a ringtype) set"
- "ring_constr ==
- \\<Sigma>G \\<in> AbelianGroup. \\<Sigma>S \\<in> {M. M \\<in> Semigroup & (M.<cr>) = (G.<cr>)}.
- {R. R = (| carrier = (G.<cr>), bin_op = (G.<f>),
- inverse = (G.<inv>), unit = (G.<e>),
- Rmult = (S.<f>) |) &
- (\\<forall>x \\<in> (R.<cr>). \\<forall>y \\<in> (R.<cr>). \\<forall>z \\<in> (R.<cr>).
- ((R.<m>) x ((R.<f>) y z) = (R.<f>) ((R.<m>) x y) ((R.<m>) x z))) &
-(\\<forall>x \\<in> (R.<cr>). \\<forall>y \\<in> (R.<cr>). \\<forall>z \\<in> (R.<cr>).
- ((R.<m>) ((R.<f>) y z) x = (R.<f>) ((R.<m>) y x) ((R.<m>) z x)))}"
-
- ring_from :: "['a grouptype, 'a semigrouptype] => 'a ringtype"
- "ring_from == %G: AbelianGroup.
- %S: {M. M \\<in> Semigroup & (M.<cr>) = (G.<cr>) &
- distr_l (G.<cr>) (M.<f>) (G.<f>) &
- distr_r (G.<cr>) (M.<f>) (G.<f>)}.
- (| carrier = (G.<cr>), bin_op = (G.<f>),
- inverse = (G.<inv>), unit = (G.<e>), Rmult = (S.<f>) |)"
-
-end
-
--- a/src/HOL/GroupTheory/Sylow.ML Wed Sep 25 11:23:26 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,348 +0,0 @@
-(* Title: HOL/GroupTheory/Sylow
- ID: $Id$
- Author: Florian Kammueller, with new proofs by L C Paulson
- Copyright 1998-2001 University of Cambridge
-
-Sylow's theorem using locales (combinatorial argument in Exponent.thy)
-
-See Florian Kamm\"uller and L. C. Paulson,
- A Formal Proof of Sylow's theorem:
- An Experiment in Abstract Algebra with Isabelle HOL
- J. Automated Reasoning 23 (1999), 235-264
-*)
-
-Open_locale "sylow";
-
-val prime_p = thm "prime_p";
-val order_G = thm "order_G";
-val finite_G = thm "finite_G";
-val calM_def = thm "calM_def";
-val RelM_def = thm "RelM_def";
-
-AddIffs [finite_G];
-Addsimps [coset_mul_e];
-
-Goalw [refl_def, RelM_def] "refl calM RelM";
-by Auto_tac;
-by (asm_full_simp_tac (simpset() addsimps [calM_def]) 1);
-by (res_inst_tac [("x","e")] bexI 1);
-by (auto_tac (claset(), simpset() addsimps [e_closed]));
-qed "RelM_refl";
-
-Goalw [sym_def, RelM_def] "sym RelM";
-by Auto_tac;
-by (res_inst_tac [("x","i g")] bexI 1);
-by (etac inv_closed 2);
-by (asm_full_simp_tac
- (simpset() addsimps [coset_mul_assoc, calM_def, inv_closed]) 1);
-qed "RelM_sym";
-
-Goalw [trans_def, RelM_def] "trans RelM";
-by Auto_tac;
-by (res_inst_tac [("x","ga ## g")] bexI 1);
-by (ALLGOALS (asm_full_simp_tac
- (simpset() addsimps [coset_mul_assoc, calM_def, binop_closed])));
-qed "RelM_trans";
-
-Goalw [equiv_def] "equiv calM RelM";
-by (blast_tac (claset() addIs [RelM_refl, RelM_sym, RelM_trans]) 1);
-qed "RelM_equiv";
-
-Goalw [RelM_def] "M \\<in> calM // RelM ==> M <= calM";
-by (blast_tac (claset() addSEs [quotientE]) 1);
-qed "M_subset_calM_prep";
-
-(*** Central Part of the Proof ***)
-
-Open_locale "sylow_central";
-
-val M_in_quot = thm "M_in_quot";
-val not_dvd_M = thm "not_dvd_M";
-val M1_in_M = thm "M1_in_M";
-val H_def = thm "H_def";
-
-Goal "M <= calM";
-by (rtac (M_in_quot RS M_subset_calM_prep) 1);
-qed "M_subset_calM";
-
-Goal "card(M1) = p^a";
-by (cut_facts_tac [M_subset_calM, M1_in_M] 1);
-by (asm_full_simp_tac (simpset() addsimps [calM_def]) 1);
-by (Blast_tac 1);
-qed "card_M1";
-
-Goal "\\<exists>x. x\\<in>M1";
-by (rtac (card_nonempty RS NotEmpty_ExEl) 1);
-by (cut_facts_tac [prime_p RS prime_imp_one_less] 1);
-by (asm_simp_tac (simpset() addsimps [card_M1]) 1);
-qed "exists_x_in_M1";
-
-Goal "M1 <= carrier G";
-by (rtac (subsetD RS PowD) 1);
-by (rtac M1_in_M 2);
-by (rtac (M_subset_calM RS subset_trans) 1);
-by (auto_tac (claset(), simpset() addsimps [calM_def]));
-qed "M1_subset_G";
-
-Goal "\\<exists>f \\<in> H\\<rightarrow>M1. inj_on f H";
-by (rtac (exists_x_in_M1 RS exE) 1);
-by (res_inst_tac [("x", "%z: H. x ## z")] bexI 1);
-by (rtac restrictI 2);
-by (asm_full_simp_tac (simpset() addsimps [H_def]) 2);
-by (Clarify_tac 2);
-by (etac subst 2);
-by (asm_full_simp_tac (simpset() addsimps [rcosI, M1_subset_G]) 2);
-by (rtac inj_onI 1);
-by (rtac left_cancellation 1);
-by (auto_tac (claset(), simpset() addsimps [H_def, M1_subset_G RS subsetD]));
-qed "M1_inj_H";
-
-Goal "{} \\<notin> calM // RelM";
-by (blast_tac (claset() addSEs [quotientE]
- addDs [RelM_equiv RS equiv_class_self]) 1);
-qed "EmptyNotInEquivSet";
-
-Goal "\\<exists>M1. M1\\<in>M";
-by (cut_facts_tac [M_in_quot, EmptyNotInEquivSet] 1);
-by (blast_tac (claset() addIs [NotEmpty_ExEl]) 1);
-qed "existsM1inM";
-val ExistsM1inM = Export existsM1inM;
-
-Goalw [order_def] "0 < order(G)";
-by (cut_facts_tac [e_closed] 1);
-by (blast_tac (claset() addIs [zero_less_card_empty]) 1);
-qed "zero_less_o_G";
-
-Goal "0 < m";
-by (cut_facts_tac [zero_less_o_G] 1);
-by (asm_full_simp_tac (simpset() addsimps [order_G]) 1);
-qed "zero_less_m";
-
-Goal "card(calM) = (p^a) * m choose p^a";
-by (simp_tac (simpset() addsimps [calM_def, n_subsets,
- order_G RS sym, order_def]) 1);
-qed "card_calM";
-
-Goal "0 < card calM";
-by (simp_tac (simpset() addsimps [card_calM, zero_less_binomial,
- le_extend_mult, zero_less_m]) 1);
-qed "zero_less_card_calM";
-
-Goal "~ (p ^ Suc(exponent p m) dvd card(calM))";
-by (subgoal_tac "exponent p m = exponent p (card calM)" 1);
- by (asm_full_simp_tac (simpset() addsimps [card_calM,
- zero_less_m RS const_p_fac]) 2);
-by (cut_facts_tac [zero_less_card_calM, prime_p] 1);
-by (force_tac (claset() addDs [power_Suc_exponent_Not_dvd], simpset()) 1);
-qed "max_p_div_calM";
-
-Goalw [calM_def] "finite calM";
-by (res_inst_tac [("B", "Pow (carrier G)")] finite_subset 1);
-by Auto_tac;
-qed "finite_calM";
-
-Goal "\\<exists>M \\<in> calM // RelM. ~ (p ^ Suc(exponent p m) dvd card(M))";
-by (rtac (max_p_div_calM RS contrapos_np) 1);
-by (asm_full_simp_tac (simpset() addsimps [finite_calM,
- RelM_equiv RSN(2, equiv_imp_dvd_card)]) 1);
-qed "lemma_A1";
-val Lemma_A1 = Export lemma_A1;
-
-Goal "x \\<in> H ==> x \\<in> carrier G";
-by (afs [H_def] 1);
-qed "H_into_carrier_G";
-
-Goal "g : H ==> M1 #> g = M1";
-by (asm_full_simp_tac (simpset() addsimps [H_def]) 1);
-qed "in_H_imp_eq";
-
-Goalw [H_def] "[| x\\<in>H; xa\\<in>H|] ==> x ## xa\\<in>H";
-by (asm_full_simp_tac (simpset() addsimps [coset_mul_assoc RS sym,
- binop_closed, M1_subset_G]) 1);
-qed "bin_op_closed_lemma";
-
-Goal "H \\<noteq> {}";
-by (asm_full_simp_tac (simpset() addsimps [H_def]) 1);
-by (res_inst_tac [("x","e")] exI 1);
-by (asm_full_simp_tac (simpset() addsimps [e_closed, M1_subset_G]) 1);
-qed "H_not_empty";
-
-Goal "H <<= G";
-by (rtac subgroupI 1);
-by (rtac subsetI 1);
-by (etac H_into_carrier_G 1);
-by (rtac H_not_empty 1);
-by (afs [H_def, inv_closed] 1);
-by (Clarify_tac 1);
-by (eres_inst_tac [("P","%z. z #> i a = M1")] subst 1);
-by (asm_simp_tac (simpset() addsimps [coset_mul_assoc, inv_closed,
- inv_ax1, coset_mul_e, M1_subset_G]) 1);
-by (blast_tac (claset() addIs [bin_op_closed_lemma]) 1);
-qed "H_is_SG";
-val H_is_subgroup = Export H_is_SG;
-
-Goal "[| g\\<in>carrier G; x\\<in>M1 #> g |] ==> x\\<in>carrier G";
-by (rtac (r_coset_subset_G RS subsetD) 1);
-by (assume_tac 3);
-by (assume_tac 2);
-by (rtac M1_subset_G 1);
-qed "rcosetGM1g_subset_G";
-
-Goal "finite M1";
-by (rtac ([ M1_subset_G, finite_G] MRS finite_subset) 1);
-qed "finite_M1";
-
-Goal "g\\<in>carrier G ==> finite (M1 #> g)";
-by (rtac finite_subset 1);
-by (rtac subsetI 1);
-by (etac rcosetGM1g_subset_G 1);
-by (assume_tac 1);
-by (rtac finite_G 1);
-qed "finite_rcosetGM1g";
-
-Goal "g\\<in>carrier G ==> card(M1 #> g) = card(M1)";
-by (asm_simp_tac
- (simpset() addsimps [M1_subset_G, card_cosets_equal, setrcosI]) 1);
-qed "M1_cardeq_rcosetGM1g";
-
-Goal "g \\<in> carrier G ==> (M1, M1 #> g) \\<in> RelM";
-by (simp_tac (simpset() addsimps [RelM_def,calM_def,card_M1,M1_subset_G]) 1);
-by (rtac conjI 1);
- by (blast_tac (claset() addIs [rcosetGM1g_subset_G]) 1);
-by (asm_simp_tac (simpset() addsimps [card_M1, M1_cardeq_rcosetGM1g]) 1);
-by (res_inst_tac [("x","i g")] bexI 1);
-by (asm_full_simp_tac (simpset() addsimps [coset_mul_assoc, M1_subset_G,
- inv_closed, inv_ax1]) 1);
-by (asm_simp_tac (simpset() addsimps [inv_closed]) 1);
-qed "M1_RelM_rcosetGM1g";
-
-
-
-(*** A pair of injections between M and {*H*} shows their cardinalities are
- equal ***)
-
-Goal "M2 \\<in> M ==> \\<exists>g. g \\<in> carrier G & M1 #> g = M2";
-by (cut_facts_tac [M1_in_M, M_in_quot RS (RelM_equiv RS ElemClassEquiv)] 1);
-by (asm_full_simp_tac (simpset() addsimps [RelM_def]) 1);
-by (blast_tac (claset() addSDs [bspec]) 1);
-qed "M_elem_map";
-
-val M_elem_map_carrier = M_elem_map RS someI_ex RS conjunct1;
-val M_elem_map_eq = M_elem_map RS someI_ex RS conjunct2;
-
-Goal "(%x:M. H #> (SOME g. g \\<in> carrier G & M1 #> g = x)) \\<in> M \\<rightarrow> {* H *}";
-by (rtac (setrcosI RS restrictI) 1);
-by (rtac (H_is_SG RS subgroup_imp_subset) 1);
-by (etac M_elem_map_carrier 1);
-qed "M_funcset_setrcos_H";
-
-Goal "\\<exists>f \\<in> M\\<rightarrow>{* H *}. inj_on f M";
-by (rtac bexI 1);
-by (rtac M_funcset_setrcos_H 2);
-by (rtac inj_onI 1);
-by (Asm_full_simp_tac 1);
-by (rtac ([asm_rl,M_elem_map_eq] MRS trans) 1);
-by (assume_tac 2);
-by (rtac ((M_elem_map_eq RS sym) RS trans) 1);
-by (assume_tac 1);
-by (rtac coset_mul_inv1 1);
-by (REPEAT (etac M_elem_map_carrier 2));
-by (rtac M1_subset_G 2);
-by (rtac (coset_join1 RS in_H_imp_eq) 1);
-by (rtac H_is_SG 3);
-by (blast_tac (claset() addIs [binop_closed,M_elem_map_carrier,inv_closed]) 2);
-by (asm_full_simp_tac (simpset() addsimps [coset_mul_invers2, H_def,
- M_elem_map_carrier, subset_def]) 1);
-qed "inj_M_GmodH";
-
-
-(** the opposite injection **)
-
-Goal "H1\\<in>{* H *} ==> \\<exists>g. g \\<in> carrier G & H #> g = H1";
-by (auto_tac (claset(), simpset() addsimps [setrcos_eq]));
-qed "H_elem_map";
-
-val H_elem_map_carrier = H_elem_map RS someI_ex RS conjunct1;
-val H_elem_map_eq = H_elem_map RS someI_ex RS conjunct2;
-
-Goal "(%C:{*H*}. M1 #> (@g. g \\<in> (G .<cr>) \\<and> H #> g = C)) \\<in> {* H *} \\<rightarrow> M";
-by (simp_tac (simpset() addsimps [setrcos_eq]) 1);
-by (fast_tac (claset() addIs [someI2]
- addSIs [restrictI, RelM_equiv, M_in_quot,
- [RelM_equiv,M_in_quot,asm_rl,M1_RelM_rcosetGM1g] MRS EquivElemClass, M1_in_M]) 1);
-qed "setrcos_H_funcset_M";
-
-Goal "\\<exists>g \\<in> {* H *}\\<rightarrow>M. inj_on g ({* H *})";
-by (rtac bexI 1);
-by (rtac setrcos_H_funcset_M 2);
-by (rtac inj_onI 1);
-by (rotate_tac ~2 1);
-by (Asm_full_simp_tac 1);
-by (rtac ([asm_rl,H_elem_map_eq] MRS trans) 1);
-by (assume_tac 2);
-by (rtac ((H_elem_map_eq RS sym) RS trans) 1);
-by (assume_tac 1);
-by (rtac coset_mul_inv1 1);
-by (REPEAT (etac H_elem_map_carrier 2));
-by (rtac (H_is_SG RS subgroup_imp_subset) 2);
-by (rtac coset_join2 1);
-by (blast_tac (claset() addIs [binop_closed,inv_closed,H_elem_map_carrier]) 1);
-by (rtac H_is_SG 1);
-by (asm_full_simp_tac (simpset() addsimps [H_def, coset_mul_invers2,
- M1_subset_G, H_elem_map_carrier]) 1);
-qed "inj_GmodH_M";
-
-Goal "calM <= Pow(carrier G)";
-by (auto_tac (claset(), simpset() addsimps [calM_def]));
-qed "calM_subset_PowG";
-
-
-Goal "finite M";
-by (rtac finite_subset 1);
-by (rtac (M_subset_calM RS subset_trans) 1);
-by (rtac calM_subset_PowG 1);
-by (Blast_tac 1);
-qed "finite_M";
-
-Goal "card(M) = card({* H *})";
-by (blast_tac (claset() addSIs [inj_M_GmodH,inj_GmodH_M]
- addIs [card_bij, finite_M, H_is_SG,
- setrcos_subset_PowG RS finite_subset,
- finite_Pow_iff RS iffD2]) 1);
-qed "cardMeqIndexH";
-
-Goal "card(M) * card(H) = order(G)";
-by (simp_tac (simpset() addsimps [cardMeqIndexH,lagrange, H_is_SG]) 1);
-qed "index_lem";
-
-Goal "p^a <= card(H)";
-by (rtac ([prime_p,not_dvd_M] MRS div_combine RS dvd_imp_le) 1);
-by (blast_tac (claset() addIs [SG_card1,H_is_SG]) 2);
-by (simp_tac (simpset() addsimps [index_lem,order_G,power_add,mult_dvd_mono,
- power_exponent_dvd,zero_less_m]) 1);
-qed "lemma_leq1";
-
-Goal "card(H) <= p^a";
-by (stac (card_M1 RS sym) 1);
-by (cut_facts_tac [M1_inj_H] 1);
-by (blast_tac (claset() addSIs [M1_subset_G]
- addIs [card_inj, H_into_carrier_G,
- finite_G RSN(2, finite_subset)]) 1);
-qed "lemma_leq2";
-
-Goal "card(H) = p^a";
-by (blast_tac (claset() addIs [le_anti_sym, lemma_leq1, lemma_leq2]) 1);
-qed "card_H_eq";
-val Card_H_eq = Export card_H_eq;
-
-Close_locale "sylow_central";
-
-Goal "\\<exists>H. H <<= G & card(H) = p^a";
-by (cut_facts_tac [Lemma_A1] 1);
-by (blast_tac (claset() addDs [ExistsM1inM, H_is_subgroup, Card_H_eq]) 1);
-qed "sylow1";
-val Sylow1 = export sylow1;
-
-Close_locale "sylow";
-Close_locale "coset";
-Close_locale "group";
--- a/src/HOL/GroupTheory/Sylow.thy Wed Sep 25 11:23:26 2002 +0200
+++ b/src/HOL/GroupTheory/Sylow.thy Thu Sep 26 10:40:13 2002 +0200
@@ -1,9 +1,6 @@
(* Title: HOL/GroupTheory/Sylow
ID: $Id$
Author: Florian Kammueller, with new proofs by L C Paulson
- Copyright 1998-2001 University of Cambridge
-
-Sylow's theorem using locales (combinatorial argument in Exponent.thy)
See Florian Kamm\"uller and L. C. Paulson,
A Formal Proof of Sylow's theorem:
@@ -11,34 +8,357 @@
J. Automated Reasoning 23 (1999), 235-264
*)
-Sylow = Coset +
+header{*Sylow's theorem using locales*}
+
+theory Sylow = Coset:
+
+text{*The combinatorial argument is in theory Exponent*}
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) )}"
+ fixes p and a and m and calM and RelM
+ assumes prime_p: "p \<in> prime"
+ and order_G: "order(G) = (p^a) * m"
+ and finite_G [iff]: "finite (carrier G)"
+ defines "calM == {s. s <= carrier(G) & card(s) = p^a}"
+ and "RelM == {(N1,N2). N1 \<in> calM & N2 \<in> calM &
+ (\<exists>g \<in> carrier(G). N1 = (N2 #> g) )}"
+
+lemma (in sylow) RelM_refl: "refl calM RelM"
+apply (unfold refl_def RelM_def, auto)
+apply (simp add: calM_def)
+apply (rule bexI [of _ \<zero>])
+apply (auto simp add: zero_closed)
+done
+
+lemma (in sylow) RelM_sym: "sym RelM"
+apply (unfold sym_def RelM_def, auto)
+apply (rule_tac x = "gminus G g" in bexI)
+apply (erule_tac [2] minus_closed)
+apply (simp add: coset_sum_assoc calM_def)
+done
+
+lemma (in sylow) RelM_trans: "trans RelM"
+apply (unfold trans_def RelM_def, auto)
+apply (rule_tac x = "sum G ga g" in bexI)
+apply (simp_all add: coset_sum_assoc calM_def)
+done
+
+lemma (in sylow) RelM_equiv: "equiv calM RelM"
+apply (unfold equiv_def)
+apply (blast intro: RelM_refl RelM_sym RelM_trans)
+done
+
+lemma (in sylow) M_subset_calM_prep: "M' \<in> calM // RelM ==> M' <= calM"
+apply (unfold RelM_def)
+apply (blast elim!: quotientE)
+done
+
+subsection{*Main Part of the Proof*}
+
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 ^ Suc(exponent p m) dvd card(M))"
- M1_in_M "M1 \\<in> M"
- defines
- H_def "H == {g. g\\<in>carrier G & M1 #> g = M1}"
+ fixes H and M1 and M
+ assumes M_in_quot: "M \<in> calM // RelM"
+ and not_dvd_M: "~(p ^ Suc(exponent p m) dvd card(M))"
+ and M1_in_M: "M1 \<in> M"
+ defines "H == {g. g\<in>carrier G & M1 #> g = M1}"
+
+lemma (in sylow_central) M_subset_calM: "M <= calM"
+by (rule M_in_quot [THEN M_subset_calM_prep])
+
+lemma (in sylow_central) card_M1: "card(M1) = p^a"
+apply (cut_tac M_subset_calM M1_in_M)
+apply (simp add: calM_def, blast)
+done
+
+lemma (in sylow_central) exists_x_in_M1: "\<exists>x. x\<in>M1"
+apply (subgoal_tac "0 < card M1")
+ apply (blast dest: card_nonempty)
+apply (cut_tac prime_p [THEN prime_imp_one_less])
+apply (simp (no_asm_simp) add: card_M1)
+done
+
+lemma (in sylow_central) M1_subset_G [simp]: "M1 <= carrier G"
+apply (rule subsetD [THEN PowD])
+apply (rule_tac [2] M1_in_M)
+apply (rule M_subset_calM [THEN subset_trans])
+apply (auto simp add: calM_def)
+done
+
+lemma (in sylow_central) M1_inj_H: "\<exists>f \<in> H\<rightarrow>M1. inj_on f H"
+apply (rule exists_x_in_M1 [THEN exE])
+apply (rule_tac x = "%z: H. sum G x z" in bexI)
+ apply (rule inj_onI)
+ apply (rule left_cancellation)
+ apply (auto simp add: H_def M1_subset_G [THEN subsetD])
+apply (rule restrictI)
+apply (simp add: H_def, clarify)
+apply (erule subst)
+apply (simp add: rcosI)
+done
+
+subsection{*Discharging the Assumptions of @{text sylow_central}*}
+
+lemma (in sylow) EmptyNotInEquivSet: "{} \<notin> calM // RelM"
+by (blast elim!: quotientE dest: RelM_equiv [THEN equiv_class_self])
+
+lemma (in sylow) existsM1inM: "M \<in> calM // RelM ==> \<exists>M1. M1 \<in> M"
+apply (subgoal_tac "M \<noteq> {}")
+ apply blast
+apply (cut_tac EmptyNotInEquivSet, blast)
+done
+
+lemma (in sylow) zero_less_o_G: "0 < order(G)"
+apply (unfold order_def)
+apply (cut_tac zero_closed)
+apply (blast intro: zero_less_card_empty)
+done
+
+lemma (in sylow) zero_less_m: "0 < m"
+apply (cut_tac zero_less_o_G)
+apply (simp add: order_G)
+done
+
+lemma (in sylow) card_calM: "card(calM) = (p^a) * m choose p^a"
+by (simp add: calM_def n_subsets order_G [symmetric] order_def)
+
+lemma (in sylow) zero_less_card_calM: "0 < card calM"
+by (simp add: card_calM zero_less_binomial le_extend_mult zero_less_m)
+
+lemma (in sylow) max_p_div_calM:
+ "~ (p ^ Suc(exponent p m) dvd card(calM))"
+apply (subgoal_tac "exponent p m = exponent p (card calM) ")
+ apply (cut_tac zero_less_card_calM prime_p)
+ apply (force dest: power_Suc_exponent_Not_dvd)
+apply (simp add: card_calM zero_less_m [THEN const_p_fac])
+done
+
+lemma (in sylow) finite_calM: "finite calM"
+apply (unfold calM_def)
+apply (rule_tac B = "Pow (carrier G) " in finite_subset)
+apply auto
+done
+
+lemma (in sylow) lemma_A1:
+ "\<exists>M \<in> calM // RelM. ~ (p ^ Suc(exponent p m) dvd card(M))"
+apply (rule max_p_div_calM [THEN contrapos_np])
+apply (simp add: finite_calM equiv_imp_dvd_card [OF _ RelM_equiv])
+done
+
+
+subsubsection{*Introduction and Destruct Rules for @{term H}*}
+
+lemma (in sylow_central) H_I: "[|g \<in> carrier G; M1 #> g = M1|] ==> g \<in> H"
+by (simp add: H_def)
+
+lemma (in sylow_central) H_into_carrier_G: "x \<in> H ==> x \<in> carrier G"
+by (simp add: H_def)
+
+lemma (in sylow_central) in_H_imp_eq: "g : H ==> M1 #> g = M1"
+by (simp add: H_def)
+
+lemma (in sylow_central) H_sum_closed: "[| x\<in>H; y\<in>H|] ==> x \<oplus> y \<in> H"
+apply (unfold H_def)
+apply (simp add: coset_sum_assoc [symmetric] sum_closed)
+done
+
+lemma (in sylow_central) H_not_empty: "H \<noteq> {}"
+apply (simp add: H_def)
+apply (rule exI [of _ \<zero>], simp)
+done
+
+lemma (in sylow_central) H_is_subgroup: "subgroup H G"
+apply (rule subgroupI)
+apply (rule subsetI)
+apply (erule H_into_carrier_G)
+apply (rule H_not_empty)
+apply (simp add: H_def, clarify)
+apply (erule_tac P = "%z. ?lhs(z) = M1" in subst)
+apply (simp add: coset_sum_assoc )
+apply (blast intro: H_sum_closed)
+done
+
+
+lemma (in sylow_central) rcosetGM1g_subset_G:
+ "[| g \<in> carrier G; x \<in> M1 #> g |] ==> x \<in> carrier G"
+by (blast intro: M1_subset_G [THEN r_coset_subset_G, THEN subsetD])
+
+lemma (in sylow_central) finite_M1: "finite M1"
+by (rule finite_subset [OF M1_subset_G finite_G])
+
+lemma (in sylow_central) finite_rcosetGM1g: "g\<in>carrier G ==> finite (M1 #> g)"
+apply (rule finite_subset)
+apply (rule subsetI)
+apply (erule rcosetGM1g_subset_G, assumption)
+apply (rule finite_G)
+done
+
+lemma (in sylow_central) M1_cardeq_rcosetGM1g:
+ "g \<in> carrier G ==> card(M1 #> g) = card(M1)"
+by (simp (no_asm_simp) add: M1_subset_G card_cosets_equal setrcosI)
+
+lemma (in sylow_central) M1_RelM_rcosetGM1g:
+ "g \<in> carrier G ==> (M1, M1 #> g) \<in> RelM"
+apply (simp (no_asm) add: RelM_def calM_def card_M1 M1_subset_G)
+apply (rule conjI)
+ apply (blast intro: rcosetGM1g_subset_G)
+apply (simp (no_asm_simp) add: card_M1 M1_cardeq_rcosetGM1g)
+apply (rule bexI [of _ "\<ominus>g"])
+apply (simp_all add: coset_sum_assoc M1_subset_G)
+done
+
+
+
+subsection{*Equal Cardinalities of @{term M} and @{term "rcosets G H"}*}
+
+text{*Injections between @{term M} and @{term "rcosets G H"} show that
+ their cardinalities are equal.*}
+
+lemma ElemClassEquiv:
+ "[| equiv A r; C\<in>A // r |] ==> \<forall>x \<in> C. \<forall>y \<in> C. (x,y)\<in>r"
+apply (unfold equiv_def quotient_def sym_def trans_def, blast)
+done
+
+lemma (in sylow_central) M_elem_map:
+ "M2 \<in> M ==> \<exists>g. g \<in> carrier G & M1 #> g = M2"
+apply (cut_tac M1_in_M M_in_quot [THEN RelM_equiv [THEN ElemClassEquiv]])
+apply (simp add: RelM_def)
+apply (blast dest!: bspec)
+done
+
+lemmas (in sylow_central) M_elem_map_carrier =
+ M_elem_map [THEN someI_ex, THEN conjunct1]
+
+lemmas (in sylow_central) M_elem_map_eq =
+ M_elem_map [THEN someI_ex, THEN conjunct2]
+
+lemma (in sylow_central) M_funcset_setrcos_H:
+ "(%x:M. H #> (SOME g. g \<in> carrier G & M1 #> g = x)) \<in> M \<rightarrow> rcosets G H"
+apply (rule setrcosI [THEN restrictI])
+apply (rule H_is_subgroup [THEN subgroup_imp_subset])
+apply (erule M_elem_map_carrier)
+done
+
+lemma (in sylow_central) inj_M_GmodH: "\<exists>f \<in> M\<rightarrow>rcosets G H. inj_on f M"
+apply (rule bexI)
+apply (rule_tac [2] M_funcset_setrcos_H)
+apply (rule inj_onI, simp)
+apply (rule trans [OF _ M_elem_map_eq])
+prefer 2 apply assumption
+apply (rule M_elem_map_eq [symmetric, THEN trans], assumption)
+apply (rule coset_sum_minus1)
+apply (erule_tac [2] M_elem_map_carrier)+
+apply (rule_tac [2] M1_subset_G)
+apply (rule coset_join1 [THEN in_H_imp_eq])
+apply (rule_tac [3] H_is_subgroup)
+prefer 2 apply (blast intro: sum_closed M_elem_map_carrier minus_closed)
+apply (simp add: coset_sum_minus2 H_def M_elem_map_carrier subset_def)
+done
+
+
+(** the opposite injection **)
+
+lemma (in sylow_central) H_elem_map:
+ "H1\<in>rcosets G H ==> \<exists>g. g \<in> carrier G & H #> g = H1"
+by (auto simp add: setrcos_eq)
+
+lemmas (in sylow_central) H_elem_map_carrier =
+ H_elem_map [THEN someI_ex, THEN conjunct1]
+
+lemmas (in sylow_central) H_elem_map_eq =
+ H_elem_map [THEN someI_ex, THEN conjunct2]
+
+
+lemma EquivElemClass:
+ "[|equiv A r; M\<in>A // r; M1\<in>M; (M1, M2)\<in>r |] ==> M2\<in>M"
+apply (unfold equiv_def quotient_def sym_def trans_def, blast)
+done
+
+lemma (in sylow_central) setrcos_H_funcset_M:
+ "(\<lambda>C \<in> rcosets G H. M1 #> (@g. g \<in> carrier G \<and> H #> g = C))
+ \<in> rcosets G H \<rightarrow> M"
+apply (simp add: setrcos_eq)
+apply (fast intro: someI2
+ intro!: restrictI M1_in_M
+ EquivElemClass [OF RelM_equiv M_in_quot _ M1_RelM_rcosetGM1g])
+done
+
+text{*close to a duplicate of @{text inj_M_GmodH}*}
+lemma (in sylow_central) inj_GmodH_M:
+ "\<exists>g \<in> rcosets G H\<rightarrow>M. inj_on g (rcosets G H)"
+apply (rule bexI)
+apply (rule_tac [2] setrcos_H_funcset_M)
+apply (rule inj_onI)
+apply (rotate_tac -2, simp)
+apply (rule trans [OF _ H_elem_map_eq])
+prefer 2 apply assumption
+apply (rule H_elem_map_eq [symmetric, THEN trans], assumption)
+apply (rule coset_sum_minus1)
+apply (erule_tac [2] H_elem_map_carrier)+
+apply (rule_tac [2] H_is_subgroup [THEN subgroup_imp_subset])
+apply (rule coset_join2)
+apply (blast intro: sum_closed minus_closed H_elem_map_carrier)
+apply (rule H_is_subgroup)
+apply (simp add: H_I coset_sum_minus2 M1_subset_G H_elem_map_carrier)
+done
+
+lemma (in sylow_central) calM_subset_PowG: "calM <= Pow(carrier G)"
+by (auto simp add: calM_def)
+
+
+lemma (in sylow_central) finite_M: "finite M"
+apply (rule finite_subset)
+apply (rule M_subset_calM [THEN subset_trans])
+apply (rule calM_subset_PowG, blast)
+done
+
+lemma (in sylow_central) cardMeqIndexH: "card(M) = card(rcosets G H)"
+apply (insert inj_M_GmodH inj_GmodH_M)
+apply (blast intro: card_bij finite_M H_is_subgroup
+ setrcos_subset_PowG [THEN finite_subset]
+ finite_Pow_iff [THEN iffD2])
+done
+
+lemma (in sylow_central) index_lem: "card(M) * card(H) = order(G)"
+by (simp add: cardMeqIndexH lagrange H_is_subgroup)
+
+lemma (in sylow_central) lemma_leq1: "p^a <= card(H)"
+apply (rule dvd_imp_le)
+ apply (rule div_combine [OF prime_p not_dvd_M])
+ prefer 2 apply (blast intro: subgroup_card_positive H_is_subgroup)
+apply (simp add: index_lem order_G power_add mult_dvd_mono power_exponent_dvd
+ zero_less_m)
+done
+
+lemma (in sylow_central) lemma_leq2: "card(H) <= p^a"
+apply (subst card_M1 [symmetric])
+apply (cut_tac M1_inj_H)
+apply (blast intro!: M1_subset_G intro:
+ card_inj H_into_carrier_G finite_subset [OF _ finite_G])
+done
+
+lemma (in sylow_central) card_H_eq: "card(H) = p^a"
+by (blast intro: le_anti_sym lemma_leq1 lemma_leq2)
+
+lemma (in sylow) sylow_thm: "\<exists>H. subgroup H G & card(H) = p^a"
+apply (cut_tac lemma_A1, clarify)
+apply (frule existsM1inM, clarify)
+apply (subgoal_tac "sylow_central G p a m M1 M")
+ apply (blast dest: sylow_central.H_is_subgroup sylow_central.card_H_eq)
+apply (simp add: sylow_central_def sylow_central_axioms_def prems)
+done
+
+text{*Needed because the locale's automatic definition refers to
+ @{term "semigroup G"} and @{term "group_axioms G"} rather than
+ simply to @{term "group G"}.*}
+lemma sylow_eq: "sylow G p a m = (group G & sylow_axioms G p a m)"
+by (simp add: sylow_def group_def)
+
+theorem sylow_thm:
+ "[|p \<in> prime; group(G); order(G) = (p^a) * m; finite (carrier G)|]
+ ==> \<exists>H. subgroup H G & card(H) = p^a"
+apply (rule sylow.sylow_thm [of G p a m])
+apply (simp add: sylow_eq sylow_axioms_def)
+done
end