# HG changeset patch
# User paulson
# Date 1048007226 -3600
# Node ID cf947d1ec5ffbfb61b3d1c8a09b87cadd2b9f54a
# Parent  18112403c80936340325e73509c64ec4af99cda9
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
to the new Group setup.

Deleted Ring, Module from GroupTheory

Minor UNITY changes

diff -r 18112403c809 -r cf947d1ec5ff src/HOL/Algebra/Coset.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/Coset.thy	Tue Mar 18 18:07:06 2003 +0100
@@ -0,0 +1,464 @@
+(*  Title:      HOL/GroupTheory/Coset
+    ID:         $Id$
+    Author:     Florian Kammueller, with new proofs by L C Paulson
+*)
+
+header{*Theory of Cosets*}
+
+theory Coset = Group + Exponent:
+
+declare (in group) l_inv [simp]  r_inv [simp] 
+
+constdefs
+  r_coset    :: "[('a,'b) group_scheme,'a set, 'a] => 'a set"    
+   "r_coset G H a == (% x. (mult G) x a) ` H"
+
+  l_coset    :: "[('a,'b) group_scheme, 'a, 'a set] => 'a set"
+   "l_coset G a H == (% x. (mult G) a x) ` H"
+
+  rcosets  :: "[('a,'b) group_scheme,'a set] => ('a set)set"
+   "rcosets G H == r_coset G H ` (carrier G)"
+
+  set_mult  :: "[('a,'b) group_scheme,'a set,'a set] => 'a set"
+   "set_mult G H K == (%(x,y). (mult G) x y) ` (H \<times> K)"
+
+  set_inv   :: "[('a,'b) group_scheme,'a set] => 'a set"
+   "set_inv G H == (m_inv 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 setmult   :: "['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 setmult_def: "H <#> K == set_mult 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 \<otimes> a = b}"
+by (auto simp add: rcos_def r_coset_def)
+
+lemma (in coset) l_coset_eq: "a <# H = {b . \<exists>h\<in>H. a \<otimes> h = b}"
+by (auto simp add: lcos_def l_coset_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)
+
+lemma (in coset) set_mult_eq: "H <#> K = {c . \<exists>h\<in>H. \<exists>k\<in>K. c = h \<otimes> k}"
+by (simp add: setmult_def set_mult_def image_def)
+
+lemma (in coset) coset_mult_assoc:
+     "[| M <= carrier G; g \<in> carrier G; h \<in> carrier G |]  
+      ==> (M #> g) #> h = M #> (g \<otimes> h)"
+by (force simp add: r_coset_eq m_assoc)
+
+lemma (in coset) coset_mult_one [simp]: "M <= carrier G ==> M #> \<one> = M"
+by (force simp add: r_coset_eq)
+
+lemma (in coset) coset_mult_inv1:
+     "[| M #> (x \<otimes> (inv 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_mult_assoc m_assoc)
+done
+
+lemma (in coset) coset_mult_inv2:
+     "[| M #> x = M #> y;  x \<in> carrier G;  y \<in> carrier G;  M <= carrier G |]  
+      ==> M #> (x \<otimes> (inv y)) = M "
+apply (simp add: coset_mult_assoc [symmetric])
+apply (simp add: coset_mult_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: l_one subgroup.one_closed)
+done
+
+text{*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 \<otimes> x = y"
+apply (rule bexI [of _ "y \<otimes> (inv x)"])
+apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc 
+                      subgroup.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.m_closed r_coset_eq solve_equation)
+
+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 \<otimes> 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_inv:
+     "[| x \<otimes> y = z;  x \<in> carrier G;  y \<in> carrier G;  z \<in> carrier G |]  
+      ==> (inv x) \<otimes> z = y"
+by (force simp add: m_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 m_assoc [symmetric] 
+                   subgroup.subset [THEN subsetD]
+                   subgroup.m_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: l_one subgroup.subset [THEN subsetD] 
+                    subgroup.one_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)
+
+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_inv_op_closed1:
+     "\<lbrakk>H \<lhd> G; x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<otimes> h \<otimes> 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: m_assoc subgroup.subset [THEN subsetD])
+apply (erule subst)
+apply (simp add: m_assoc [symmetric] subgroup.subset [THEN subsetD])
+done
+
+lemma (in coset) normal_inv_op_closed2:
+     "\<lbrakk>H \<lhd> G; x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> (inv x) \<in> H"
+apply (drule normal_inv_op_closed1 [of H "(inv x)"]) 
+apply auto
+done
+
+lemma (in coset) lcos_m_assoc:
+     "[| M <= carrier G; g \<in> carrier G; h \<in> carrier G |]  
+      ==> g <# (h <# M) = (g \<otimes> h) <# M"
+by (force simp add: l_coset_eq m_assoc)
+
+lemma (in coset) lcos_mult_one: "M <= carrier G ==> \<one> <# 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 m_assoc 
+                      subgroup.subset [THEN subsetD] subgroup.m_closed)
+apply (rule_tac x = "mult G (m_inv G h) ha" in bexI)
+  --{*FIXME: locales don't currently work with @{text rule_tac},
+      want @{term "(inv h) \<otimes> ha"}*}
+apply (auto simp add: m_assoc [symmetric] subgroup.subset [THEN subsetD] 
+                      subgroup.m_inv_closed subgroup.m_closed)
+done
+
+lemma (in coset) setmult_subset_G:
+     "[| H <= carrier G; K <= carrier G |] ==> H <#> K <= carrier G"
+by (auto simp add: set_mult_eq subsetD)
+
+lemma (in coset) subgroup_mult_id: "subgroup H G ==> H <#> H = H"
+apply (auto simp add: subgroup.m_closed set_mult_eq Sigma_def image_def)
+apply (rule_tac x = x in bexI)
+apply (rule bexI [of _ "\<one>"])
+apply (auto simp add: subgroup.m_closed subgroup.one_closed 
+                      r_one subgroup.subset [THEN subsetD])
+done
+
+
+(* set of inverses of an r_coset *)
+lemma (in coset) rcos_inv:
+  assumes normalHG: "H <| G"
+      and xinG:     "x \<in> carrier G"
+  shows "set_inv G (H #> x) = H #> (inv x)"
+proof -
+  have H_subset: "H <= carrier G" 
+    by (rule subgroup.subset [OF normal_imp_subgroup, OF normalHG])
+  show ?thesis
+  proof (auto simp add: r_coset_eq image_def set_inv_def)
+    fix h
+    assume "h \<in> H"
+      hence "((inv x) \<otimes> (inv h) \<otimes> x) \<otimes> inv x = inv (h \<otimes> x)"
+	by (simp add: xinG m_assoc inv_mult_group H_subset [THEN subsetD])
+      thus "\<exists>j\<in>H. j \<otimes> inv x = inv (h \<otimes> x)" 
+       using prems
+	by (blast intro: normal_inv_op_closed1 normal_imp_subgroup 
+			 subgroup.m_inv_closed)
+  next
+    fix h
+    assume "h \<in> H"
+      hence eq: "(x \<otimes> (inv h) \<otimes> (inv x)) \<otimes> x = x \<otimes> inv h"
+        by (simp add: xinG m_assoc H_subset [THEN subsetD])
+      hence "(\<exists>j\<in>H. j \<otimes> x = inv  (h \<otimes> (inv x))) \<and> h \<otimes> inv x = inv (inv (h \<otimes> (inv x)))"
+       using prems
+	by (simp add: m_assoc inv_mult_group H_subset [THEN subsetD],
+            blast intro: eq normal_inv_op_closed2 normal_imp_subgroup 
+			 subgroup.m_inv_closed)
+      thus "\<exists>y. (\<exists>h\<in>H. h \<otimes> x = y) \<and> h \<otimes> inv x = inv y" ..
+  qed
+qed
+
+(*The old proof is something like this, but the rule_tac calls make
+illegal references to implicit structures.
+lemma (in coset) rcos_inv:
+     "[| H <| G; x \<in> carrier G |] ==> set_inv G (H #> x) = H #> (inv x)"
+apply (frule normal_imp_subgroup)
+apply (auto simp add: r_coset_eq image_def set_inv_def)
+apply (rule_tac x = "(inv x) \<otimes> (inv h) \<otimes> x" in bexI)
+apply (simp add: m_assoc inv_mult_group subgroup.subset [THEN subsetD])
+apply (simp add: subgroup.m_inv_closed, assumption+)
+apply (rule_tac x = "inv  (h \<otimes> (inv x)) " in exI)
+apply (simp add: inv_mult_group subgroup.subset [THEN subsetD])
+apply (rule_tac x = "x \<otimes> (inv h) \<otimes> (inv x)" in bexI)
+apply (simp add: m_assoc subgroup.subset [THEN subsetD])
+apply (simp add: normal_inv_op_closed2 subgroup.m_inv_closed)
+done
+*)
+
+lemma (in coset) rcos_inv2:
+     "[| H <| G; K \<in> rcosets G H; x \<in> K |] ==> set_inv G K = H #> (inv x)"
+apply (simp add: setrcos_eq, clarify)
+apply (subgoal_tac "x : carrier G")
+ prefer 2
+ apply (blast dest: r_coset_subset_G subgroup.subset normal_imp_subgroup) 
+apply (drule repr_independence)
+  apply assumption
+ apply (erule normal_imp_subgroup)
+apply (simp add: rcos_inv)
+done
+
+
+(* some rules for <#> with #> or <# *)
+lemma (in coset) setmult_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 setmult_def set_mult_def)
+apply (force simp add: m_assoc)+
+done
+
+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 
+                      setmult_def set_mult_def Sigma_def image_def)
+apply (force intro!: exI bexI simp add: m_assoc)+
+done
+
+lemma (in coset) rcos_mult_step1:
+     "[| H <| G; x \<in> carrier G; y \<in> carrier G |] 
+      ==> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
+by (simp add: setmult_rcos_assoc normal_imp_subgroup [THEN subgroup.subset]
+              r_coset_subset_G l_coset_subset_G rcos_assoc_lcos)
+
+lemma (in coset) rcos_mult_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)
+
+lemma (in coset) rcos_mult_step3:
+     "[| H <| G; x \<in> carrier G; y \<in> carrier G |] 
+      ==> (H <#> (H #> x)) #> y = H #> (x \<otimes> y)"
+by (simp add: setmult_rcos_assoc r_coset_subset_G coset_mult_assoc
+              setmult_subset_G  subgroup_mult_id
+              subgroup.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 \<otimes> y)"
+by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)
+
+(*generalizes subgroup_mult_id*)
+lemma (in coset) setrcos_mult_eq: "[|H <| G; M \<in> rcosets G H|] ==> H <#> M = M"
+by (auto simp add: setrcos_eq normal_imp_subgroup subgroup.subset
+                   setmult_rcos_assoc subgroup_mult_id)
+
+
+subsection{*Lemmas Leading to Lagrange's Theorem*}
+
+lemma (in coset) setrcos_part_G: "subgroup H G ==> \<Union> rcosets G H = carrier G"
+apply (rule equalityI)
+apply (force simp add: subgroup.subset [THEN subsetD] 
+                       setrcos_eq r_coset_eq)
+apply (auto simp add: setrcos_eq subgroup.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
+
+text{*The next two lemmas support the proof of @{text card_cosets_equal},
+since we can't use @{text rule_tac} with explicit terms for @{term f} and
+@{term g}.*}
+lemma (in coset) inj_on_f:
+    "[|H \<subseteq> carrier G;  a \<in> carrier G|] ==> inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
+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 (simp add: subsetD)
+done
+
+lemma (in coset) inj_on_g:
+    "[|H \<subseteq> carrier G;  a \<in> carrier G|] ==> inj_on (\<lambda>y. y \<otimes> a) H"
+by (force simp add: inj_on_def subsetD)
+
+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)
+apply (rule card_bij_eq)
+     apply (rule inj_on_f, assumption+) 
+    apply (force simp add: m_assoc subsetD r_coset_eq)
+   apply (rule inj_on_g, assumption+) 
+  apply (force simp add: m_assoc subsetD r_coset_eq)
+ txt{*The sets @{term "H #> a"} and @{term "H"} are finite.*}
+ apply (simp add: r_coset_subset_G [THEN finite_subset])
+apply (blast intro: finite_subset)
+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 \<otimes> a = h \<otimes> b;   
+        h \<in> H;  ha \<in> H;  hb \<in> H|]  
+      ==> \<exists>h\<in>H. h \<otimes> b = hb \<otimes> a"
+apply (rule bexI [of _"hb \<otimes> ((inv ha) \<otimes> h)"])
+apply (simp  add: m_assoc transpose_inv subgroup.subset [THEN subsetD])
+apply (simp add: subgroup.m_closed subgroup.m_inv_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.subset)
+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,
+	 mult = (%X: rcosets G H. %Y: rcosets G H. set_mult G X Y),
+	 one = H,
+	 m_inv = (%X: rcosets G H. set_inv G X) |)"
+
+lemma (in coset) setmult_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.subset] 
+                   rcos_sum setrcos_eq)
+
+(*
+lemma setinv_closed:
+     "[| H <| G; K \<in> rcosets G H |] ==> set_inv G K \<in> rcosets G H"
+by (auto simp add:  normal_imp_subgroup
+                   subgroup.subset coset.rcos_inv 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.subset m_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.one_closed group.one_closed
+                     coset.coset_join2 [symmetric])
+done
+*)
+
+lemma (in coset) setrcos_inv_mult_group_eq:
+     "[|H <| G; M \<in> rcosets G H|] ==> set_inv G M <#> M = H"
+by (auto simp add: setrcos_eq rcos_inv rcos_sum normal_imp_subgroup 
+                   subgroup.subset)
+
+(*????????????????
+theorem factorgroup_is_group: "H <| G ==> group (G Mod H)"
+apply (frule normal_imp_coset) 
+apply (simp add: FactGroup_def) 
+apply (rule group.intro)
+apply (rule magma.intro) 
+apply (simp add: ); 
+  apply (simp add: restrictI coset.setmult_closed) 
+ apply (rule semigroup.intro) 
+  apply (simp add: restrictI coset.setmult_closed) 
+ apply (simp add: coset.setmult_closed coset.setrcos_assoc)  
+apply (rule group_axioms.intro) 
+   apply (simp add: restrictI setinv_closed) 
+  apply (simp add: normal_imp_subgroup subgroup_in_rcosets) 
+ apply (simp add: setinv_closed coset.setrcos_inv_mult_group_eq) 
+apply (simp add: normal_imp_subgroup subgroup_in_rcosets coset.setrcos_mult_eq)
+done
+*)
+
+end
diff -r 18112403c809 -r cf947d1ec5ff src/HOL/Algebra/Exponent.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/Exponent.thy	Tue Mar 18 18:07:06 2003 +0100
@@ -0,0 +1,351 @@
+(*  Title:      HOL/GroupTheory/Exponent
+    ID:         $Id$
+    Author:     Florian Kammueller, with new proofs by L C Paulson
+
+    exponent p s   yields the greatest power of p that divides s.
+*)
+
+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"
+
+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 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 18112403c809 -r cf947d1ec5ff src/HOL/Algebra/ROOT.ML
--- a/src/HOL/Algebra/ROOT.ML	Tue Mar 18 17:55:54 2003 +0100
+++ b/src/HOL/Algebra/ROOT.ML	Tue Mar 18 18:07:06 2003 +0100
@@ -6,3 +6,4 @@
 
 with_path "abstract" time_use_thy "Abstract";        (*The ring theory*)
 with_path "poly"     time_use_thy "Polynomial";      (*The full theory*)
+use_thy "Sylow";
diff -r 18112403c809 -r cf947d1ec5ff src/HOL/Algebra/Sylow.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/Sylow.thy	Tue Mar 18 18:07:06 2003 +0100
@@ -0,0 +1,395 @@
+(*  Title:      HOL/GroupTheory/Sylow
+    ID:         $Id$
+    Author:     Florian Kammueller, with new proofs by L C Paulson
+
+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
+*)
+
+header{*Sylow's theorem using locales*}
+
+theory Sylow = Coset:
+
+subsection {*Order of a Group and Lagrange's Theorem*}
+
+constdefs
+  order     :: "(('a,'b) semigroup_scheme) => nat"
+   "order(S) == card(carrier S)"
+
+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.subset)
+apply (simp add: rcos_disjoint)
+done
+
+
+text{*The combinatorial argument is in theory Exponent*}
+
+locale sylow = coset +
+  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 (auto simp add: refl_def RelM_def calM_def) 
+apply (blast intro!: coset_mult_one [symmetric]) 
+done
+
+lemma (in sylow) RelM_sym: "sym RelM"
+proof (unfold sym_def RelM_def, clarify)
+  fix y g
+  assume   "y \<in> calM"
+    and g: "g \<in> carrier G"
+  hence "y = y #> g #> (inv g)" by (simp add: coset_mult_assoc calM_def)
+  thus "\<exists>g'\<in>carrier G. y = y #> g #> g'"
+   by (blast intro: g inv_closed)
+qed
+
+lemma (in sylow) RelM_trans: "trans RelM"
+by (auto simp add: trans_def RelM_def calM_def coset_mult_assoc) 
+
+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 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 card_nonempty: "0 < card(S) ==> S \<noteq> {}"
+by force
+
+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"
+  proof -
+    from exists_x_in_M1 obtain m1 where m1M: "m1 \<in> M1"..
+    have m1G: "m1 \<in> carrier G" by (simp add: m1M M1_subset_G [THEN subsetD])
+    show ?thesis
+    proof
+      show "inj_on (\<lambda>z\<in>H. m1 \<otimes> z) H"
+	by (simp add: inj_on_def l_cancel [of m1 x y, THEN iffD1] H_def m1G)
+      show "restrict (op \<otimes> m1) H \<in> H \<rightarrow> M1"
+      proof (rule restrictI)
+	fix z assume zH: "z \<in> H"
+	show "m1 \<otimes> z \<in> M1"
+	proof -
+	  from zH
+	  have zG: "z \<in> carrier G" and M1zeq: "M1 #> z = M1" 
+	    by (auto simp add: H_def)
+	  show ?thesis
+	    by (rule subst [OF M1zeq], simp add: m1M zG rcosI)
+	qed
+      qed
+    qed
+  qed
+
+
+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 (blast intro: one_closed 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_m_closed: "[| x\<in>H; y\<in>H|] ==> x \<otimes> y \<in> H"
+apply (unfold H_def)
+apply (simp add: coset_mult_assoc [symmetric] m_closed)
+done
+
+lemma (in sylow_central) H_not_empty: "H \<noteq> {}"
+apply (simp add: H_def)
+apply (rule exI [of _ \<one>], 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_mult_assoc )
+apply (blast intro: H_m_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 _ "inv g"])
+apply (simp_all add: coset_mult_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.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_mult_inv1)
+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: m_closed M_elem_map_carrier inv_closed)
+apply (simp add: coset_mult_inv2 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 (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_mult_inv1)
+apply (erule_tac [2] H_elem_map_carrier)+
+apply (rule_tac [2] H_is_subgroup [THEN subgroup.subset])
+apply (rule coset_join2)
+apply (blast intro: m_closed inv_closed H_elem_map_carrier)
+apply (rule H_is_subgroup) 
+apply (simp add: H_I coset_mult_inv2 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.finite_imp_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
diff -r 18112403c809 -r cf947d1ec5ff src/HOL/GroupTheory/Coset.thy
--- a/src/HOL/GroupTheory/Coset.thy	Tue Mar 18 17:55:54 2003 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,462 +0,0 @@
-(*  Title:      HOL/GroupTheory/Coset
-    ID:         $Id$
-    Author:     Florian Kammueller, with new proofs by L C Paulson
-*)
-
-header{*Theory of Cosets*}
-
-theory Coset = Group + Exponent:
-
-constdefs
-  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)
-
-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
-
-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{*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)
-
-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)
-
-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 
-                      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
-
-
-(* set of inverses of an r_coset *)
-lemma (in coset) rcos_minus:
-  assumes normalHG: "H <| G"
-      and xinG:     "x \<in> carrier G"
-  shows "set_minus G (H #> x) = H #> (\<ominus>x)"
-proof -
-  have H_subset: "H <= carrier G" 
-    by (rule subgroup_imp_subset [OF normal_imp_subgroup, OF normalHG])
-  show ?thesis
-  proof (auto simp add: r_coset_eq image_def set_minus_def)
-    fix h
-    assume "h \<in> H"
-      hence "((\<ominus>x) \<oplus> (\<ominus>h) \<oplus> x) \<oplus> \<ominus>x = \<ominus>(h \<oplus> x)"
-	by (simp add: xinG sum_assoc minus_sum H_subset [THEN subsetD])
-      thus "\<exists>j\<in>H. j \<oplus> \<ominus>x = \<ominus>(h \<oplus> x)" 
-       using prems
-	by (blast intro: normal_minus_op_closed1 normal_imp_subgroup 
-			 subgroup_minus_closed)
-  next
-    fix h
-    assume "h \<in> H"
-      hence eq: "(x \<oplus> (\<ominus>h) \<oplus> (\<ominus>x)) \<oplus> x = x \<oplus> \<ominus>h"
-        by (simp add: xinG sum_assoc H_subset [THEN subsetD])
-      hence "(\<exists>j\<in>H. j \<oplus> x = \<ominus> (h \<oplus> (\<ominus>x))) \<and> h \<oplus> \<ominus>x = \<ominus>(\<ominus>(h \<oplus> (\<ominus>x)))"
-       using prems
-	by (simp add: sum_assoc minus_sum H_subset [THEN subsetD],
-            blast intro: eq normal_minus_op_closed2 normal_imp_subgroup 
-			 subgroup_minus_closed)
-      thus "\<exists>y. (\<exists>h\<in>H. h \<oplus> x = y) \<and> h \<oplus> \<ominus>x = \<ominus>y" ..
-  qed
-qed
-
-(*The old proof is something like this, but the rule_tac calls make
-illegal references to implicit structures.
-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)
-apply (rule_tac x = "(\<ominus>x) \<oplus> (\<ominus>h) \<oplus> x" in bexI)
-apply (simp add: sum_assoc minus_sum subgroup_imp_subset [THEN subsetD])
-apply (simp add: subgroup_minus_closed, assumption+)
-apply (rule_tac x = "\<ominus> (h \<oplus> (\<ominus>x)) " in exI)
-apply (simp add: minus_sum subgroup_imp_subset [THEN subsetD])
-apply (rule_tac x = "x \<oplus> (\<ominus>h) \<oplus> (\<ominus>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
-
-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 intro!: exI bexI simp add: sum_assoc)+
-done
-
-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)
-
-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{*Lemmas Leading to Lagrange's Theorem*}
-
-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
-
-text{*The next two lemmas support the proof of @{text card_cosets_equal},
-since we can't use @{text rule_tac} with explicit terms for @{term f} and
-@{term g}.*}
-lemma (in coset) inj_on_f:
-    "[|H \<subseteq> carrier G;  a \<in> carrier G|] ==> inj_on (\<lambda>y. y \<oplus> \<ominus>a) (H #> a)"
-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 (simp add: subsetD)
-done
-
-lemma (in coset) inj_on_g:
-    "[|H \<subseteq> carrier G;  a \<in> carrier G|] ==> inj_on (\<lambda>y. y \<oplus> a) H"
-by (force simp add: inj_on_def subsetD)
-
-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)
-apply (rule card_bij_eq)
-     apply (rule inj_on_f, assumption+) 
-    apply (force simp add: sum_assoc subsetD r_coset_eq)
-   apply (rule inj_on_g, assumption+) 
-  apply (force simp add: sum_assoc subsetD r_coset_eq)
- txt{*The sets @{term "H #> a"} and @{term "H"} are finite.*}
- apply (simp add: r_coset_subset_G [THEN finite_subset])
-apply (blast intro: finite_subset)
-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
-
-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 18112403c809 -r cf947d1ec5ff src/HOL/GroupTheory/Exponent.thy
--- a/src/HOL/GroupTheory/Exponent.thy	Tue Mar 18 17:55:54 2003 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,351 +0,0 @@
-(*  Title:      HOL/GroupTheory/Exponent
-    ID:         $Id$
-    Author:     Florian Kammueller, with new proofs by L C Paulson
-
-    exponent p s   yields the greatest power of p that divides s.
-*)
-
-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"
-
-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 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 18112403c809 -r cf947d1ec5ff src/HOL/GroupTheory/Module.thy
--- a/src/HOL/GroupTheory/Module.thy	Tue Mar 18 17:55:54 2003 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,62 +0,0 @@
-(*  Title:      HOL/GroupTheory/Module
-    ID:         $Id$
-    Author:     Lawrence C Paulson
-
-*)
-
-header{*Modules*}
-
-theory Module = Ring:
-
-text{*The record includes all the group components (carrier, sum, gminus,
-zero), adding the scalar product.*}
-record ('a,'b) module  = "'a group" + 
-  sprod :: "'b \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "\<star>\<index>" 70) 
-
-text{*The locale assumes all the properties of a ring and an Abelian group,
-adding laws relating them.*}
-locale module = ring R + abelian_group M +
-  assumes sprod_funcset: "sprod M \<in> carrier R \<rightarrow> carrier M \<rightarrow> carrier M"
-      and sprod_assoc:   
-            "[|r \<in> carrier R; s \<in> carrier R; a \<in> carrier M|] 
-             ==> (r \<cdot>\<^sub>1 s) \<star>\<^sub>2 a = r \<star>\<^sub>2 (s \<star>\<^sub>2 a)"
-      and sprod_distrib_left:
-            "[|r \<in> carrier R; a \<in> carrier M; b \<in> carrier M|] 
-             ==> r \<star>\<^sub>2 (a \<oplus>\<^sub>2 b) = (r \<star>\<^sub>2 a) \<oplus>\<^sub>2 (r \<star>\<^sub>2 b)"
-      and sprod_distrib_right:
-            "[|r \<in> carrier R; s \<in> carrier R; a \<in> carrier M|] 
-             ==> (r \<oplus>\<^sub>1 s) \<star>\<^sub>2 a = (r \<star>\<^sub>2 a) \<oplus>\<^sub>2 (s \<star>\<^sub>2 a)"
-
-lemma module_iff:
-     "module R M = (ring R & abelian_group M & module_axioms R M)"
-by (simp add: module_def ring_def abelian_group_def) 
-
-text{*The sum and product in @{text R} are @{text "r \<oplus>\<^sub>1 s"} and @{text
-"r \<cdot>\<^sub>1 s"}, respectively.  The sum in @{text M} is @{text "a \<oplus>\<^sub>2 b"}.*}
-
-
-text{*We have to write the ring product as @{text "\<cdot>\<^sub>2"}. But if we
-refer to the scalar product as @{text "\<cdot>\<^sub>1"} then syntactic ambiguities
-arise.  This presumably happens because the subscript merely determines which
-structure argument to insert, which happens after parsing.  Better to use a
-different symbol such as @{text "\<star>"}*}
-
-subsection {*Trivial Example: Every Ring is an R-Module Over Itself *}
-
-constdefs
- triv_mod :: "('a,'b) ring_scheme => ('a,'a) module"
-  "triv_mod R == (|carrier = carrier R,
-                 sum = sum R,
-                 gminus = gminus R,
-                 zero = zero R, 
-                 sprod = prod R|)"
-
-theorem module_triv_mod: "ring R ==> module R (triv_mod R)"
-apply (simp add: triv_mod_def module_iff module_axioms_def
-                 ring_def ring_axioms_def abelian_group_def
-                 distrib_l_def distrib_r_def semigroup_def group_axioms_def)
-apply (simp add: abelian_group_axioms_def)
-  --{*Combining the two simplifications causes looping!*}
-done
-
-end
diff -r 18112403c809 -r cf947d1ec5ff src/HOL/GroupTheory/ROOT.ML
--- a/src/HOL/GroupTheory/ROOT.ML	Tue Mar 18 17:55:54 2003 +0100
+++ b/src/HOL/GroupTheory/ROOT.ML	Tue Mar 18 18:07:06 2003 +0100
@@ -1,6 +1,4 @@
-no_document use_thy "Primes";
 no_document use_thy "FuncSet";
 
-use_thy "Sylow";
-use_thy "Module";
+use_thy "Bij";
 use_thy "Summation";
\ No newline at end of file
diff -r 18112403c809 -r cf947d1ec5ff src/HOL/GroupTheory/Ring.thy
--- a/src/HOL/GroupTheory/Ring.thy	Tue Mar 18 17:55:54 2003 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,222 +0,0 @@
-(*  Title:      HOL/GroupTheory/Ring
-    ID:         $Id$
-    Author:     Florian Kammueller, with new proofs by L C Paulson
-
-*)
-
-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)))"
-
-  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
-  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)
-
-text{*Construction of a ring from a semigroup and an Abelian group*}
-lemma ringI:
-     "[|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]
-
-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 {*Example: The Ring of Integers*}
-
-constdefs
- integers :: "int ring"
-  "integers == (|carrier = UNIV, 
-                 sum = op +,
-                 gminus = (%x. -x),
-                 zero = 0::int,
-                 prod = op *|)"
-
-theorem ring_integers: "ring (integers)"
-by (simp add: integers_def ring_def ring_axioms_def 
-              distrib_l_def distrib_r_def 
-              zadd_zmult_distrib zadd_zmult_distrib2 
-              abelian_group_axioms_def group_axioms_def semigroup_def) 
-
-
-subsection {*Ring Homomorphisms*}
-
-constdefs
- 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)"
-
-  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) 
-
-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 
-              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 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
-
-
-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])
-
-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 18112403c809 -r cf947d1ec5ff src/HOL/GroupTheory/Sylow.thy
--- a/src/HOL/GroupTheory/Sylow.thy	Tue Mar 18 17:55:54 2003 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,364 +0,0 @@
-(*  Title:      HOL/GroupTheory/Sylow
-    ID:         $Id$
-    Author:     Florian Kammueller, with new proofs by L C Paulson
-
-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
-*)
-
-header{*Sylow's theorem using locales*}
-
-theory Sylow = Coset:
-
-text{*The combinatorial argument is in theory Exponent*}
-
-locale sylow = coset +
-  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 (auto simp add: refl_def RelM_def calM_def) 
-apply (blast intro!: coset_sum_zero [symmetric]) 
-done
-
-lemma (in sylow) RelM_sym: "sym RelM"
-proof (unfold sym_def RelM_def, clarify)
-  fix y g
-  assume   "y \<in> calM"
-    and g: "g \<in> carrier G"
-  hence "y = y #> g #> (\<ominus>g)" by (simp add: coset_sum_assoc calM_def)
-  thus "\<exists>g'\<in>carrier G. y = y #> g #> g'"
-   by (blast intro: g minus_closed)
-qed
-
-lemma (in sylow) RelM_trans: "trans RelM"
-by (auto simp add: trans_def RelM_def calM_def coset_sum_assoc) 
-
-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 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 card_nonempty: "0 < card(S) ==> S \<noteq> {}"
-by force
-
-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 (blast intro: zero_closed 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 (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
diff -r 18112403c809 -r cf947d1ec5ff src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Mar 18 17:55:54 2003 +0100
+++ b/src/HOL/IsaMakefile	Tue Mar 18 18:07:06 2003 +0100
@@ -280,12 +280,8 @@
 $(LOG)/HOL-GroupTheory.gz: $(OUT)/HOL \
   Library/Primes.thy Library/FuncSet.thy \
   GroupTheory/Bij.thy \
-  GroupTheory/Coset.thy \
-  GroupTheory/Exponent.thy \
   GroupTheory/Group.thy \
-  GroupTheory/Module.thy GroupTheory/Ring.thy \
   GroupTheory/Summation.thy \
-  GroupTheory/Sylow.thy \
   GroupTheory/ROOT.ML \
   GroupTheory/document/root.tex
 	@$(ISATOOL) usedir -g true $(OUT)/HOL GroupTheory
@@ -340,6 +336,9 @@
 HOL-Algebra: HOL $(LOG)/HOL-Algebra.gz
 
 $(LOG)/HOL-Algebra.gz: $(OUT)/HOL Algebra/ROOT.ML \
+  Algebra/Coset.thy \
+  Algebra/Exponent.thy \
+  Algebra/Sylow.thy \
   Algebra/abstract/Abstract.thy \
   Algebra/abstract/Factor.ML Algebra/abstract/Factor.thy \
   Algebra/abstract/Field.thy \
diff -r 18112403c809 -r cf947d1ec5ff src/HOL/UNITY/ProgressSets.thy
--- a/src/HOL/UNITY/ProgressSets.thy	Tue Mar 18 17:55:54 2003 +0100
+++ b/src/HOL/UNITY/ProgressSets.thy	Tue Mar 18 18:07:06 2003 +0100
@@ -132,7 +132,7 @@
 
   progress_set :: "['a program, 'a set, 'a set] => 'a set set set"
    "progress_set F T B ==
-      {L. F \<in> stable T & lattice L & B \<in> L & T \<in> L & closed F T B L}"
+      {L. lattice L & B \<in> L & T \<in> L & closed F T B L}"
 
 lemma closedD:
    "[|closed F T B L; act \<in> Acts F; B\<subseteq>M; T\<inter>M \<in> L|] 
@@ -234,7 +234,7 @@
 
 text{*The Lemma proved on page 96*}
 lemma progress_set_lemma:
-     "[|C \<in> progress_set F T B; r \<in> wens_set F B|] ==> T\<inter>r \<in> C"
+     "[|C \<in> progress_set F T B; r \<in> wens_set F B; F \<in> stable T|] ==> T\<inter>r \<in> C"
 apply (simp add: progress_set_def, clarify) 
 apply (erule wens_set.induct) 
   txt{*Base*}
@@ -278,12 +278,13 @@
 
 theorem progress_set_Union:
   assumes prog: "C \<in> progress_set F T B"
+      and Fstable: "F \<in> stable T"
       and BB':  "B \<subseteq> B'"
       and B'C:  "B' \<in> C"
       and Gco: "!!X. X\<in>C ==> G \<in> X-B co X"
       and leadsTo: "F \<in> A leadsTo B'"
   shows "F\<squnion>G \<in> T\<inter>A leadsTo B'"
-apply (insert prog) 
+apply (insert prog Fstable) 
 apply (rule leadsTo_Join [OF leadsTo]) 
   apply (force simp add: progress_set_def awp_iff_stable [symmetric]) 
 apply (simp add: awp_iff_constrains)
@@ -292,4 +293,10 @@
                     BB' [THEN subsetD]) 
 done
 
+
+subsection {*Some Progress Sets*}
+
+lemma UNIV_in_progress_set: "UNIV \<in> progress_set F T B"
+by (simp add: progress_set_def lattice_def closed_def)
+
 end
diff -r 18112403c809 -r cf947d1ec5ff src/HOL/UNITY/UNITY.thy
--- a/src/HOL/UNITY/UNITY.thy	Tue Mar 18 17:55:54 2003 +0100
+++ b/src/HOL/UNITY/UNITY.thy	Tue Mar 18 18:07:06 2003 +0100
@@ -244,6 +244,10 @@
 apply (blast intro: constrains_UN)
 done
 
+lemma stable_Union: 
+    "(!!A. A \<in> X ==> F \<in> stable A) ==> F \<in> stable (\<Union>X)"
+by (unfold stable_def constrains_def, blast)
+
 (** Intersection **)
 
 lemma stable_Int: 
@@ -258,6 +262,10 @@
 apply (blast intro: constrains_INT)
 done
 
+lemma stable_Inter: 
+    "(!!A. A \<in> X ==> F \<in> stable A) ==> F \<in> stable (\<Inter>X)"
+by (unfold stable_def constrains_def, blast)
+
 lemma stable_constrains_Un: 
     "[| F \<in> stable C; F \<in> A co (C \<union> A') |] ==> F \<in> (C \<union> A) co (C \<union> A')"
 by (unfold stable_def constrains_def, blast)
@@ -267,7 +275,7 @@
 by (unfold stable_def constrains_def, blast)
 
 (*[| F \<in> stable C; F \<in>  (C \<inter> A) co A |] ==> F \<in> stable (C \<inter> A) *)
-lemmas stable_constrains_stable = stable_constrains_Int [THEN stableI, standard]
+lemmas stable_constrains_stable = stable_constrains_Int[THEN stableI, standard]
 
 
 (*** invariant ***)