# HG changeset patch
# User paulson
# Date 1084546233 -7200
# Node ID 2eaff69d3d10a59d5445bb08e68d7d27d08fa4bb
# Parent  9f7b31cf74d8d39a054a83e1942a739e006e48b9
removal of locale coset

diff -r 9f7b31cf74d8 -r 2eaff69d3d10 src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Fri May 14 16:50:13 2004 +0200
+++ b/src/HOL/Algebra/Coset.thy	Fri May 14 16:50:33 2004 +0200
@@ -3,24 +3,24 @@
     Author:     Florian Kammueller, with new proofs by L C Paulson
 *)
 
-header{*Theory of Cosets*}
+header{*Cosets and Quotient Groups*}
 
 theory Coset = Group + Exponent:
 
 declare (in group) l_inv [simp] and r_inv [simp]
 
 constdefs (structure G)
-  r_coset    :: "[_,'a set, 'a] => 'a set"
-  "r_coset G H a == (% x. x \<otimes> a) ` H"
+  r_coset    :: "[_, 'a set, 'a] => 'a set"    (infixl "#>\<index>" 60)
+  "H #> a == (% x. x \<otimes> a) ` H"
 
-  l_coset    :: "[_, 'a, 'a set] => 'a set"
-  "l_coset G a H == (% x. a \<otimes> x) ` H"
+  l_coset    :: "[_, 'a, 'a set] => 'a set"    (infixl "<#\<index>" 60)
+  "a <# H == (% x. a \<otimes> x) ` H"
 
   rcosets  :: "[_, 'a set] => ('a set)set"
   "rcosets G H == r_coset G H ` (carrier G)"
 
-  set_mult  :: "[_, 'a set ,'a set] => 'a set"
-  "set_mult G H K == (%(x,y). x \<otimes> y) ` (H \<times> K)"
+  set_mult  :: "[_, 'a set ,'a set] => 'a set" (infixl "<#>\<index>" 60)
+  "H <#> K == (%(x,y). x \<otimes> y) ` (H \<times> K)"
 
   set_inv   :: "[_,'a set] => 'a set"
   "set_inv G H == m_inv G ` H"
@@ -30,120 +30,89 @@
                   (\<forall>x \<in> carrier G. r_coset G H x = l_coset G x H)"
 
 syntax (xsymbols)
-  normal  :: "['a set, ('a,'b) monoid_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 {*
-  Locale @{term coset} provides only syntax.
-  Logically, groups are cosets.
-*}
-lemma (in group) is_coset:
-  "coset G"
-  by (rule coset.intro)
-
-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)
+  normal :: "['a set, ('a,'b) monoid_scheme] => bool"  (infixl "\<lhd>" 60)
 
 
-subsection {*Lemmas Using *}
+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 group) r_coset_eq: "H #> a = {b . \<exists>h\<in>H. h \<otimes> a = b}"
+by (auto simp add: 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 group) l_coset_eq: "a <# H = {b . \<exists>h\<in>H. a \<otimes> h = b}"
+by (auto simp add: 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 group) setrcos_eq: "rcosets G H = {C . \<exists>a\<in>carrier G. C = H #> a}"
+by (auto simp add: rcosets_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 group) set_mult_eq: "H <#> K = {c . \<exists>h\<in>H. \<exists>k\<in>K. c = h \<otimes> k}"
+by (simp add: set_mult_def image_def)
 
-lemma (in coset) coset_mult_assoc:
-     "[| M <= carrier G; g \<in> carrier G; h \<in> carrier G |]
+lemma (in group) coset_mult_assoc:
+     "[| M \<subseteq> 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)
+by (force simp add: r_coset_def m_assoc)
 
-lemma (in coset) coset_mult_one [simp]: "M <= carrier G ==> M #> \<one> = M"
-by (force simp add: r_coset_eq)
+lemma (in group) coset_mult_one [simp]: "M \<subseteq> carrier G ==> M #> \<one> = M"
+by (force simp add: r_coset_def)
 
-lemma (in coset) coset_mult_inv1:
+lemma (in group) coset_mult_inv1:
      "[| M #> (x \<otimes> (inv y)) = M;  x \<in> carrier G ; y \<in> carrier G;
-         M <= carrier G |] ==> M #> x = M #> y"
+         M \<subseteq> 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 |]
+lemma (in group) coset_mult_inv2:
+     "[| M #> x = M #> y;  x \<in> carrier G;  y \<in> carrier G;  M \<subseteq> 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"
+lemma (in group) 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:
+lemma (in group) 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:
+lemma (in group) 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 group) r_coset_subset_G:
+     "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> H #> x \<subseteq> carrier G"
+by (auto simp add: r_coset_def)
 
-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 group) rcosI:
+     "[| h \<in> H; H \<subseteq> carrier G; x \<in> carrier G|] ==> h \<otimes> x \<in> H #> x"
+by (auto simp add: r_coset_def)
 
-lemma (in coset) setrcosI:
-     "[| H <= carrier G; x \<in> carrier G |] ==> H #> x \<in> rcosets G H"
+lemma (in group) setrcosI:
+     "[| H \<subseteq> 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:
+lemma (in group) 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:
+lemma (in group) 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"
+lemma (in group) 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)
@@ -152,60 +121,85 @@
 
 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:
+lemma (in group) 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 (auto simp add: l_coset_def r_coset_def normal_def)
 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:
+lemma (in group) 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)
+text{*Alternative characterization of normal subgroups*}
+lemma (in group) normal_inv_iff:
+     "(N \<lhd> G) = 
+      (subgroup N G & (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<otimes> h \<otimes> (inv x) \<in> N))"
+      (is "_ = ?rhs")
+proof
+  assume N: "N \<lhd> G"
+  show ?rhs
+    by (blast intro: N normal_imp_subgroup normal_inv_op_closed2) 
+next
+  assume ?rhs
+  hence sg: "subgroup N G" 
+    and closed: "!!x. x\<in>carrier G ==> \<forall>h\<in>N. x \<otimes> h \<otimes> inv x \<in> N" by auto
+  hence sb: "N \<subseteq> carrier G" by (simp add: subgroup.subset) 
+  show "N \<lhd> G"
+  proof (simp add: sg normal_def l_coset_def r_coset_def, clarify)
+    fix x
+    assume x: "x \<in> carrier G"
+    show "(\<lambda>n. n \<otimes> x) ` N = op \<otimes> x ` N"
+    proof
+      show "(\<lambda>n. n \<otimes> x) ` N \<subseteq> op \<otimes> x ` N"
+      proof clarify
+        fix n
+        assume n: "n \<in> N" 
+        show "n \<otimes> x \<in> op \<otimes> x ` N"
+        proof 
+          show "n \<otimes> x = x \<otimes> (inv x \<otimes> n \<otimes> x)"
+            by (simp add: x n m_assoc [symmetric] sb [THEN subsetD])
+          with closed [of "inv x"]
+          show "inv x \<otimes> n \<otimes> x \<in> N" by (simp add: x n)
+        qed
+      qed
+    next
+      show "op \<otimes> x ` N \<subseteq> (\<lambda>n. n \<otimes> x) ` N" 
+      proof clarify
+        fix n
+        assume n: "n \<in> N" 
+        show "x \<otimes> n \<in> (\<lambda>n. n \<otimes> x) ` N"
+        proof 
+          show "x \<otimes> n = (x \<otimes> n \<otimes> inv x) \<otimes> x"
+            by (simp add: x n m_assoc sb [THEN subsetD])
+          show "x \<otimes> n \<otimes> inv x \<in> N" by (simp add: x n closed)
+        qed
+      qed
+    qed
+  qed
+qed
 
-lemma (in coset) lcos_mult_one: "M <= carrier G ==> \<one> <# M = M"
-by (force simp add: l_coset_eq)
+lemma (in group) lcos_m_assoc:
+     "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
+      ==> g <# (h <# M) = (g \<otimes> h) <# M"
+by (force simp add: l_coset_def m_assoc)
 
-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 group) lcos_mult_one: "M \<subseteq> carrier G ==> \<one> <# M = M"
+by (force simp add: l_coset_def)
 
-lemma (in coset) l_coset_swap:
+lemma (in group) l_coset_subset_G:
+     "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> x <# H \<subseteq> carrier G"
+by (auto simp add: l_coset_def subsetD)
+
+lemma (in group) l_coset_swap:
      "[| y \<in> x <# H;  x \<in> carrier G;  subgroup H G |] ==> x \<in> y <# H"
 proof (simp add: l_coset_eq)
   assume "\<exists>h\<in>H. x \<otimes> h = y"
@@ -221,23 +215,23 @@
   qed
 qed
 
-lemma (in coset) l_coset_carrier:
+lemma (in group) l_coset_carrier:
      "[| y \<in> x <# H;  x \<in> carrier G;  subgroup H G |] ==> y \<in> carrier G"
-by (auto simp add: l_coset_eq m_assoc
+by (auto simp add: l_coset_def m_assoc
                    subgroup.subset [THEN subsetD] subgroup.m_closed)
 
-lemma (in coset) l_repr_imp_subset:
+lemma (in group) l_repr_imp_subset:
   assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
   shows "y <# H \<subseteq> x <# H"
 proof -
   from y
-  obtain h' where "h' \<in> H" "x \<otimes> h' = y" by (auto simp add: l_coset_eq)
+  obtain h' where "h' \<in> H" "x \<otimes> h' = y" by (auto simp add: l_coset_def)
   thus ?thesis using x sb
-    by (auto simp add: l_coset_eq m_assoc
+    by (auto simp add: l_coset_def m_assoc
                        subgroup.subset [THEN subsetD] subgroup.m_closed)
 qed
 
-lemma (in coset) l_repr_independence:
+lemma (in group) l_repr_independence:
   assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
   shows "x <# H = y <# H"
 proof
@@ -247,11 +241,11 @@
   show "y <# H \<subseteq> x <# H" by (rule l_repr_imp_subset [OF y x sb])
 qed
 
-lemma (in coset) setmult_subset_G:
-     "[| H <= carrier G; K <= carrier G |] ==> H <#> K <= carrier G"
+lemma (in group) setmult_subset_G:
+     "[| H \<subseteq> carrier G; K \<subseteq> carrier G |] ==> H <#> K \<subseteq> carrier G"
 by (auto simp add: set_mult_eq subsetD)
 
-lemma (in coset) subgroup_mult_id: "subgroup H G ==> H <#> H = H"
+lemma (in group) 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>"])
@@ -260,21 +254,21 @@
 done
 
 
-text {* Set of inverses of an @{text r_coset}. *}
+subsubsection {* Set of inverses of an @{text r_coset}. *}
 
-lemma (in coset) rcos_inv:
+lemma (in group) rcos_inv:
   assumes normalHG: "H <| G"
-      and xinG:     "x \<in> carrier G"
+      and x:     "x \<in> carrier G"
   shows "set_inv G (H #> x) = H #> (inv x)"
 proof -
-  have H_subset: "H <= carrier G"
+  have H_subset: "H \<subseteq> 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])
+        by (simp add: x 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
@@ -283,7 +277,7 @@
     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])
+        by (simp add: x 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],
@@ -293,24 +287,7 @@
   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:
+lemma (in group) 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")
@@ -323,47 +300,46 @@
 done
 
 
-text {* Some rules for @{text "<#>"} with @{text "#>"} or @{text "<#"}. *}
+subsubsection {* Some rules for @{text "<#>"} with @{text "#>"} or @{text "<#"}. *}
 
-lemma (in coset) setmult_rcos_assoc:
-     "[| H <= carrier G; K <= carrier G; x \<in> carrier G |]
+lemma (in group) setmult_rcos_assoc:
+     "[| H \<subseteq> carrier G; K \<subseteq> 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 (auto simp add: r_coset_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 |]
+lemma (in group) rcos_assoc_lcos:
+     "[| H \<subseteq> carrier G; K \<subseteq> 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 (auto simp add: r_coset_def l_coset_def set_mult_def Sigma_def image_def)
 apply (force intro!: exI bexI simp add: m_assoc)+
 done
 
-lemma (in coset) rcos_mult_step1:
+lemma (in group) 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:
+lemma (in group) 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)
+by (simp add: normal_def)
 
-lemma (in coset) rcos_mult_step3:
+lemma (in group) 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:
+lemma (in group) 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)
 
-lemma (in coset) setrcos_mult_eq: "[|H <| G; M \<in> rcosets G H|] ==> H <#> M = M"
+lemma (in group) setrcos_mult_eq: "[|H <| G; M \<in> rcosets G H|] ==> H <#> M = M"
   -- {* generalizes @{text subgroup_mult_id} *}
   by (auto simp add: setrcos_eq normal_imp_subgroup subgroup.subset
     setmult_rcos_assoc subgroup_mult_id)
@@ -371,23 +347,21 @@
 
 subsection {*Lemmas Leading to Lagrange's Theorem *}
 
-lemma (in coset) setrcos_part_G: "subgroup H G ==> \<Union>rcosets G H = carrier G"
+lemma (in group) 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)
+                       setrcos_eq r_coset_def)
 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"
+lemma (in group) cosets_finite:
+     "[| c \<in> rcosets G H;  H \<subseteq> 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:
+text{*The next two lemmas support the proof of @{text card_cosets_equal}.*}
+lemma (in group) 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")
@@ -395,27 +369,28 @@
 apply (simp add: subsetD)
 done
 
-lemma (in coset) inj_on_g:
+lemma (in group) 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) |]
+lemma (in group) card_cosets_equal:
+     "[| c \<in> rcosets G H;  H \<subseteq> 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 (force simp add: m_assoc subsetD r_coset_def)
    apply (rule inj_on_g, assumption+)
-  apply (force simp add: m_assoc subsetD r_coset_eq)
+  apply (force simp add: m_assoc subsetD r_coset_def)
  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:
+lemma (in group) 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"
@@ -424,30 +399,31 @@
 apply (simp add: subgroup.m_closed subgroup.m_inv_closed)
 done
 
-lemma (in coset) rcos_disjoint:
+lemma (in group) 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)"
+lemma (in group) setrcos_subset_PowG:
+     "subgroup H G  ==> rcosets G H \<subseteq> Pow(carrier G)"
 apply (simp add: setrcos_eq)
 apply (blast dest: r_coset_subset_G subgroup.subset)
 done
 
-subsection {*Factorization of a Group*}
+subsection {*Quotient Groups: Factorization of a Group*}
 
 constdefs
   FactGroup :: "[('a,'b) monoid_scheme, 'a set] => ('a set) monoid"
      (infixl "Mod" 60)
+    --{*Actually defined for groups rather than monoids*}
   "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) *) |)"
+       one = H |)"
 
-lemma (in coset) setmult_closed:
+
+lemma (in group) 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]
@@ -455,9 +431,9 @@
 
 lemma (in group) 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 [OF is_coset]
-                 coset.setrcos_eq [OF is_coset])
+by (auto simp add: normal_imp_subgroup
+                   subgroup.subset rcos_inv
+                   setrcos_eq)
 
 (*
 The old version is no longer valid: "group G" has to be an explicit premise.
@@ -468,7 +444,7 @@
                    subgroup.subset coset.rcos_inv coset.setrcos_eq)
 *)
 
-lemma (in coset) setrcos_assoc:
+lemma (in group) 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
@@ -479,10 +455,10 @@
 proof -
   assume sub: "subgroup H G"
   have "r_coset G H \<one> = H"
-    by (rule coset.coset_join2)
-      (auto intro: sub subgroup.one_closed is_coset)
+    by (rule coset_join2)
+       (auto intro: sub subgroup.one_closed)
   then show ?thesis
-    by (auto simp add: coset.setrcos_eq [OF is_coset])
+    by (auto simp add: setrcos_eq)
 qed
 
 (*
@@ -497,7 +473,7 @@
 done
 *)
 
-lemma (in coset) setrcos_inv_mult_group_eq:
+lemma (in group) 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)
@@ -513,15 +489,29 @@
 *)
 theorem (in group) factorgroup_is_group:
   "H <| G ==> group (G Mod H)"
-apply (insert is_coset)
 apply (simp add: FactGroup_def)
 apply (rule groupI)
-    apply (simp add: coset.setmult_closed)
+    apply (simp add: setmult_closed)
    apply (simp add: normal_imp_subgroup subgroup_in_rcosets)
-  apply (simp add: restrictI coset.setmult_closed coset.setrcos_assoc)
+  apply (simp add: restrictI setmult_closed setrcos_assoc)
  apply (simp add: normal_imp_subgroup
-   subgroup_in_rcosets coset.setrcos_mult_eq)
-apply (auto dest: coset.setrcos_inv_mult_group_eq simp add: setinv_closed)
+                  subgroup_in_rcosets setrcos_mult_eq)
+apply (auto dest: setrcos_inv_mult_group_eq simp add: setinv_closed)
 done
 
+lemma (in group) inv_FactGroup:
+     "N <| G ==> X \<in> carrier (G Mod N) ==> inv\<^bsub>G Mod N\<^esub> X = set_inv G X"
+apply (rule group.inv_equality [OF factorgroup_is_group]) 
+apply (simp_all add: FactGroup_def setinv_closed 
+    setrcos_inv_mult_group_eq group.intro [OF prems])
+done
+
+text{*The coset map is a homomorphism from @{term G} to the quotient group
+  @{term "G Mod N"}*}
+lemma (in group) r_coset_hom_Mod:
+  assumes N: "N <| G"
+  shows "(r_coset G N) \<in> hom G (G Mod N)"
+by (simp add: FactGroup_def rcosets_def Pi_def hom_def
+           rcos_sum group.intro prems) 
+
 end
diff -r 9f7b31cf74d8 -r 2eaff69d3d10 src/HOL/Algebra/Sylow.thy
--- a/src/HOL/Algebra/Sylow.thy	Fri May 14 16:50:13 2004 +0200
+++ b/src/HOL/Algebra/Sylow.thy	Fri May 14 16:50:33 2004 +0200
@@ -17,7 +17,7 @@
   order :: "('a, 'b) semigroup_scheme => nat"
   "order S == card (carrier S)"
 
-theorem (in coset) lagrange:
+theorem (in group) 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])
@@ -32,12 +32,12 @@
 
 text{*The combinatorial argument is in theory Exponent*}
 
-locale sylow = coset +
+locale sylow = group +
   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}"
+  defines "calM == {s. s \<subseteq> carrier(G) & card(s) = p^a}"
       and "RelM == {(N1,N2). N1 \<in> calM & N2 \<in> calM &
                              (\<exists>g \<in> carrier(G). N1 = (N2 #> g) )}"
 
@@ -64,7 +64,7 @@
 apply (blast intro: RelM_refl RelM_sym RelM_trans)
 done
 
-lemma (in sylow) M_subset_calM_prep: "M' \<in> calM // RelM  ==> M' <= calM"
+lemma (in sylow) M_subset_calM_prep: "M' \<in> calM // RelM  ==> M' \<subseteq> calM"
 apply (unfold RelM_def)
 apply (blast elim!: quotientE)
 done
@@ -79,7 +79,7 @@
       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"
+lemma (in sylow_central) M_subset_calM: "M \<subseteq> calM"
 by (rule M_in_quot [THEN M_subset_calM_prep])
 
 lemma (in sylow_central) card_M1: "card(M1) = p^a"
@@ -97,7 +97,7 @@
 apply (simp (no_asm_simp) add: card_M1)
 done
 
-lemma (in sylow_central) M1_subset_G [simp]: "M1 <= carrier G"
+lemma (in sylow_central) M1_subset_G [simp]: "M1 \<subseteq> carrier G"
 apply (rule subsetD [THEN PowD])
 apply (rule_tac [2] M1_in_M)
 apply (rule M_subset_calM [THEN subset_trans])
@@ -332,7 +332,7 @@
 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)"
+lemma (in sylow_central) calM_subset_PowG: "calM \<subseteq> Pow(carrier G)"
 by (auto simp add: calM_def)
 
 
@@ -352,7 +352,7 @@
 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)"
+lemma (in sylow_central) lemma_leq1: "p^a \<le> 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)
@@ -360,7 +360,7 @@
                  zero_less_m)
 done
 
-lemma (in sylow_central) lemma_leq2: "card(H) <= p^a"
+lemma (in sylow_central) lemma_leq2: "card(H) \<le> p^a"
 apply (subst card_M1 [symmetric])
 apply (cut_tac M1_inj_H)
 apply (blast intro!: M1_subset_G intro: