src/HOL/Algebra/Coset.thy

--- a/src/HOL/Algebra/Coset.thy	Tue Apr 29 12:36:49 2003 +0200
+++ b/src/HOL/Algebra/Coset.thy	Wed Apr 30 10:01:35 2003 +0200
@@ -10,27 +10,27 @@
 declare (in group) l_inv [simp]  r_inv [simp] 
 
 constdefs
-  r_coset    :: "[('a,'b) group_scheme,'a set, 'a] => 'a set"    
+  r_coset    :: "[('a,'b) monoid_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    :: "[('a,'b) monoid_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  :: "[('a,'b) monoid_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  :: "[('a,'b) monoid_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   :: "[('a,'b) monoid_scheme,'a set] => 'a set"
    "set_inv G H == (m_inv G) ` H"
 
-  normal     :: "['a set, ('a,'b) group_scheme] => bool"       (infixl "<|" 60)
+  normal     :: "['a set, ('a,'b) monoid_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)
+  normal  :: "['a set, ('a,'b) monoid_scheme] => bool" (infixl "\<lhd>" 60)
 
 locale coset = group G +
   fixes rcos      :: "['a set, 'a] => 'a set"     (infixl "#>" 60)
@@ -153,7 +153,7 @@
 subsection{*normal subgroups*}
 
 (*????????????????
-text{*Allows use of theorems proved in the locale coset*}
+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)  
@@ -406,13 +406,13 @@
 subsection {*Factorization of a Group*}
 
 constdefs
-  FactGroup :: "[('a,'b) group_scheme, 'a set] => ('a set) group"
+  FactGroup :: "[('a,'b) monoid_scheme, 'a set] => ('a set) monoid"
      (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) |)"
+	 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 |] 
@@ -482,18 +482,13 @@
   "H <| G ==> group (G Mod H)"
 apply (insert is_coset) 
 apply (simp add: FactGroup_def) 
-apply (rule group.intro)
-   apply (rule magma.intro) 
-   apply (simp add: coset.setmult_closed)
-  apply (rule semigroup_axioms.intro)
+apply (rule groupI)
+    apply (simp add: coset.setmult_closed)
+   apply (simp add: normal_imp_subgroup subgroup_in_rcosets)
   apply (simp add: restrictI coset.setmult_closed coset.setrcos_assoc)
- apply (rule l_one.intro)
-  apply (simp add: normal_imp_subgroup subgroup_in_rcosets)
  apply (simp add: normal_imp_subgroup
    subgroup_in_rcosets coset.setrcos_mult_eq)
-apply (rule group_axioms.intro)
- apply (simp add: restrictI setinv_closed)
-apply (simp add: setinv_closed coset.setrcos_inv_mult_group_eq)
+apply (auto dest: coset.setrcos_inv_mult_group_eq simp add: setinv_closed)
 done
 
 (*????????????????