# HG changeset patch
# User paulson
# Date 1033029613 -7200
# Node ID 5fcc8bf538ee5308d8e0c2c2668f21d30fb047b1
# Parent  a246a0a52dfb49831e9609d758616a577aaffd11
converted to Isar and using new "implicit structures" instead of Sigma, etc

diff -r a246a0a52dfb -r 5fcc8bf538ee src/HOL/GroupTheory/Bij.ML
--- 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";
-
diff -r a246a0a52dfb -r 5fcc8bf538ee src/HOL/GroupTheory/Bij.thy
--- 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
 
diff -r a246a0a52dfb -r 5fcc8bf538ee src/HOL/GroupTheory/Coset.ML
--- 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";
-
-
-
diff -r a246a0a52dfb -r 5fcc8bf538ee src/HOL/GroupTheory/Coset.thy
--- 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
-
-
diff -r a246a0a52dfb -r 5fcc8bf538ee src/HOL/GroupTheory/DirProd.ML
--- 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";
diff -r a246a0a52dfb -r 5fcc8bf538ee src/HOL/GroupTheory/DirProd.thy
--- 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
diff -r a246a0a52dfb -r 5fcc8bf538ee src/HOL/GroupTheory/Exponent.ML
--- 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";  
diff -r a246a0a52dfb -r 5fcc8bf538ee src/HOL/GroupTheory/Exponent.thy
--- 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
diff -r a246a0a52dfb -r 5fcc8bf538ee src/HOL/GroupTheory/FactGroup.ML
--- 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";
diff -r a246a0a52dfb -r 5fcc8bf538ee src/HOL/GroupTheory/FactGroup.thy
--- 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
diff -r a246a0a52dfb -r 5fcc8bf538ee src/HOL/GroupTheory/Group.ML
--- 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";
-
diff -r a246a0a52dfb -r 5fcc8bf538ee src/HOL/GroupTheory/Group.thy
--- 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
-
+ 
diff -r a246a0a52dfb -r 5fcc8bf538ee src/HOL/GroupTheory/Homomorphism.ML
--- 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" *)
diff -r a246a0a52dfb -r 5fcc8bf538ee src/HOL/GroupTheory/Homomorphism.thy
--- 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
diff -r a246a0a52dfb -r 5fcc8bf538ee src/HOL/GroupTheory/PiSets.ML
--- 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";
diff -r a246a0a52dfb -r 5fcc8bf538ee src/HOL/GroupTheory/PiSets.thy
--- 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
diff -r a246a0a52dfb -r 5fcc8bf538ee src/HOL/GroupTheory/README.html
--- 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>
diff -r a246a0a52dfb -r 5fcc8bf538ee src/HOL/GroupTheory/ROOT.ML
--- 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";
diff -r a246a0a52dfb -r 5fcc8bf538ee src/HOL/GroupTheory/Ring.ML
--- 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";
diff -r a246a0a52dfb -r 5fcc8bf538ee src/HOL/GroupTheory/Ring.thy
--- 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
-
-
diff -r a246a0a52dfb -r 5fcc8bf538ee src/HOL/GroupTheory/RingConstr.ML
--- 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;
-
-
diff -r a246a0a52dfb -r 5fcc8bf538ee src/HOL/GroupTheory/RingConstr.thy
--- 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
-
diff -r a246a0a52dfb -r 5fcc8bf538ee src/HOL/GroupTheory/Sylow.ML
--- 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";
diff -r a246a0a52dfb -r 5fcc8bf538ee src/HOL/GroupTheory/Sylow.thy
--- 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