removal of magmas and semigroups
authorpaulson
Thu Jun 17 17:18:30 2004 +0200 (2004-06-17)
changeset 14963d584e32f7d46
parent 14962 3283b52ebcac
child 14964 2c1456d705e9
removal of magmas and semigroups
src/HOL/Algebra/Bij.thy
src/HOL/Algebra/CRing.thy
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Sylow.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/Algebra/ringsimp.ML
     1.1 --- a/src/HOL/Algebra/Bij.thy	Thu Jun 17 14:27:01 2004 +0200
     1.2 +++ b/src/HOL/Algebra/Bij.thy	Thu Jun 17 17:18:30 2004 +0200
     1.3 @@ -8,39 +8,39 @@
     1.4  theory Bij = Group:
     1.5  
     1.6  constdefs
     1.7 -  Bij :: "'a set => ('a => 'a) set"
     1.8 +  Bij :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) set"
     1.9      --{*Only extensional functions, since otherwise we get too many.*}
    1.10 -  "Bij S == extensional S \<inter> {f. bij_betw f S S}"
    1.11 +  "Bij S \<equiv> extensional S \<inter> {f. bij_betw f S S}"
    1.12  
    1.13 -  BijGroup :: "'a set => ('a => 'a) monoid"
    1.14 -  "BijGroup S ==
    1.15 -    (| carrier = Bij S,
    1.16 -      mult = %g: Bij S. %f: Bij S. compose S g f,
    1.17 -      one = %x: S. x |)"
    1.18 +  BijGroup :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) monoid"
    1.19 +  "BijGroup S \<equiv>
    1.20 +    \<lparr>carrier = Bij S,
    1.21 +     mult = \<lambda>g \<in> Bij S. \<lambda>f \<in> Bij S. compose S g f,
    1.22 +     one = \<lambda>x \<in> S. x\<rparr>"
    1.23  
    1.24  
    1.25  declare Id_compose [simp] compose_Id [simp]
    1.26  
    1.27 -lemma Bij_imp_extensional: "f \<in> Bij S ==> f \<in> extensional S"
    1.28 +lemma Bij_imp_extensional: "f \<in> Bij S \<Longrightarrow> f \<in> extensional S"
    1.29    by (simp add: Bij_def)
    1.30  
    1.31 -lemma Bij_imp_funcset: "f \<in> Bij S ==> f \<in> S -> S"
    1.32 +lemma Bij_imp_funcset: "f \<in> Bij S \<Longrightarrow> f \<in> S \<rightarrow> S"
    1.33    by (auto simp add: Bij_def bij_betw_imp_funcset)
    1.34  
    1.35  
    1.36  subsection {*Bijections Form a Group *}
    1.37  
    1.38 -lemma restrict_Inv_Bij: "f \<in> Bij S ==> (%x:S. (Inv S f) x) \<in> Bij S"
    1.39 +lemma restrict_Inv_Bij: "f \<in> Bij S \<Longrightarrow> (\<lambda>x \<in> S. (Inv S f) x) \<in> Bij S"
    1.40    by (simp add: Bij_def bij_betw_Inv)
    1.41  
    1.42  lemma id_Bij: "(\<lambda>x\<in>S. x) \<in> Bij S "
    1.43    by (auto simp add: Bij_def bij_betw_def inj_on_def)
    1.44  
    1.45 -lemma compose_Bij: "[| x \<in> Bij S; y \<in> Bij S|] ==> compose S x y \<in> Bij S"
    1.46 +lemma compose_Bij: "\<lbrakk>x \<in> Bij S; y \<in> Bij S\<rbrakk> \<Longrightarrow> compose S x y \<in> Bij S"
    1.47    by (auto simp add: Bij_def bij_betw_compose) 
    1.48  
    1.49  lemma Bij_compose_restrict_eq:
    1.50 -     "f \<in> Bij S ==> compose S (restrict (Inv S f) S) f = (\<lambda>x\<in>S. x)"
    1.51 +     "f \<in> Bij S \<Longrightarrow> compose S (restrict (Inv S f) S) f = (\<lambda>x\<in>S. x)"
    1.52    by (simp add: Bij_def compose_Inv_id)
    1.53  
    1.54  theorem group_BijGroup: "group (BijGroup S)"
    1.55 @@ -57,62 +57,68 @@
    1.56  
    1.57  subsection{*Automorphisms Form a Group*}
    1.58  
    1.59 -lemma Bij_Inv_mem: "[|  f \<in> Bij S;  x \<in> S |] ==> Inv S f x \<in> S"
    1.60 +lemma Bij_Inv_mem: "\<lbrakk> f \<in> Bij S;  x \<in> S\<rbrakk> \<Longrightarrow> Inv S f x \<in> S"
    1.61  by (simp add: Bij_def bij_betw_def Inv_mem)
    1.62  
    1.63  lemma Bij_Inv_lemma:
    1.64 - assumes eq: "!!x y. [|x \<in> S; y \<in> S|] ==> h(g x y) = g (h x) (h y)"
    1.65 - shows "[| h \<in> Bij S;  g \<in> S \<rightarrow> S \<rightarrow> S;  x \<in> S;  y \<in> S |]
    1.66 -        ==> Inv S h (g x y) = g (Inv S h x) (Inv S h y)"
    1.67 + assumes eq: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> h(g x y) = g (h x) (h y)"
    1.68 + shows "\<lbrakk>h \<in> Bij S;  g \<in> S \<rightarrow> S \<rightarrow> S;  x \<in> S;  y \<in> S\<rbrakk>
    1.69 +        \<Longrightarrow> Inv S h (g x y) = g (Inv S h x) (Inv S h y)"
    1.70  apply (simp add: Bij_def bij_betw_def)
    1.71  apply (subgoal_tac "\<exists>x'\<in>S. \<exists>y'\<in>S. x = h x' & y = h y'", clarify)
    1.72 - apply (simp add: eq [symmetric] Inv_f_f funcset_mem [THEN funcset_mem], blast )
    1.73 + apply (simp add: eq [symmetric] Inv_f_f funcset_mem [THEN funcset_mem], blast)
    1.74  done
    1.75  
    1.76 +
    1.77  constdefs
    1.78 -  auto :: "('a, 'b) monoid_scheme => ('a => 'a) set"
    1.79 -  "auto G == hom G G \<inter> Bij (carrier G)"
    1.80 +  auto :: "('a, 'b) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'a) set"
    1.81 +  "auto G \<equiv> hom G G \<inter> Bij (carrier G)"
    1.82  
    1.83 -  AutoGroup :: "('a, 'c) monoid_scheme => ('a => 'a) monoid"
    1.84 -  "AutoGroup G == BijGroup (carrier G) (|carrier := auto G |)"
    1.85 +  AutoGroup :: "('a, 'c) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'a) monoid"
    1.86 +  "AutoGroup G \<equiv> BijGroup (carrier G) \<lparr>carrier := auto G\<rparr>"
    1.87  
    1.88 -lemma id_in_auto: "group G ==> (%x: carrier G. x) \<in> auto G"
    1.89 +lemma (in group) id_in_auto: "(\<lambda>x \<in> carrier G. x) \<in> auto G"
    1.90    by (simp add: auto_def hom_def restrictI group.axioms id_Bij)
    1.91  
    1.92 -lemma mult_funcset: "group G ==> mult G \<in> carrier G -> carrier G -> carrier G"
    1.93 +lemma (in group) mult_funcset: "mult G \<in> carrier G \<rightarrow> carrier G \<rightarrow> carrier G"
    1.94    by (simp add:  Pi_I group.axioms)
    1.95  
    1.96 -lemma restrict_Inv_hom:
    1.97 -      "[|group G; h \<in> hom G G; h \<in> Bij (carrier G)|]
    1.98 -       ==> restrict (Inv (carrier G) h) (carrier G) \<in> hom G G"
    1.99 +lemma (in group) restrict_Inv_hom:
   1.100 +      "\<lbrakk>h \<in> hom G G; h \<in> Bij (carrier G)\<rbrakk>
   1.101 +       \<Longrightarrow> restrict (Inv (carrier G) h) (carrier G) \<in> hom G G"
   1.102    by (simp add: hom_def Bij_Inv_mem restrictI mult_funcset
   1.103                  group.axioms Bij_Inv_lemma)
   1.104  
   1.105  lemma inv_BijGroup:
   1.106 -     "f \<in> Bij S ==> m_inv (BijGroup S) f = (%x: S. (Inv S f) x)"
   1.107 +     "f \<in> Bij S \<Longrightarrow> m_inv (BijGroup S) f = (\<lambda>x \<in> S. (Inv S f) x)"
   1.108  apply (rule group.inv_equality)
   1.109  apply (rule group_BijGroup)
   1.110  apply (simp_all add: BijGroup_def restrict_Inv_Bij Bij_compose_restrict_eq)
   1.111  done
   1.112  
   1.113 -lemma subgroup_auto:
   1.114 -      "group G ==> subgroup (auto G) (BijGroup (carrier G))"
   1.115 -apply (rule group.subgroupI)
   1.116 -    apply (rule group_BijGroup)
   1.117 -   apply (force simp add: auto_def BijGroup_def)
   1.118 -  apply (blast dest: id_in_auto)
   1.119 - apply (simp del: restrict_apply
   1.120 +lemma (in group) subgroup_auto:
   1.121 +      "subgroup (auto G) (BijGroup (carrier G))"
   1.122 +proof (rule subgroup.intro)
   1.123 +  show "auto G \<subseteq> carrier (BijGroup (carrier G))"
   1.124 +    by (force simp add: auto_def BijGroup_def)
   1.125 +next
   1.126 +  fix x y
   1.127 +  assume "x \<in> auto G" "y \<in> auto G" 
   1.128 +  thus "x \<otimes>\<^bsub>BijGroup (carrier G)\<^esub> y \<in> auto G"
   1.129 +    by (force simp add: BijGroup_def is_group auto_def Bij_imp_funcset 
   1.130 +                        group.hom_compose compose_Bij)
   1.131 +next
   1.132 +  show "\<one>\<^bsub>BijGroup (carrier G)\<^esub> \<in> auto G" by (simp add:  BijGroup_def id_in_auto)
   1.133 +next
   1.134 +  fix x 
   1.135 +  assume "x \<in> auto G" 
   1.136 +  thus "inv\<^bsub>BijGroup (carrier G)\<^esub> x \<in> auto G"
   1.137 +    by (simp del: restrict_apply
   1.138               add: inv_BijGroup auto_def restrict_Inv_Bij restrict_Inv_hom)
   1.139 -apply (auto simp add: BijGroup_def auto_def Bij_imp_funcset group.hom_compose
   1.140 -                      compose_Bij)
   1.141 -done
   1.142 +qed
   1.143  
   1.144 -theorem AutoGroup: "group G ==> group (AutoGroup G)"
   1.145 -apply (simp add: AutoGroup_def)
   1.146 -apply (rule Group.subgroup.groupI)
   1.147 -apply (erule subgroup_auto)
   1.148 -apply (insert Bij.group_BijGroup [of "carrier G"])
   1.149 -apply (simp_all add: group_def)
   1.150 -done
   1.151 +theorem (in group) AutoGroup: "group (AutoGroup G)"
   1.152 +by (simp add: AutoGroup_def subgroup.subgroup_is_group subgroup_auto 
   1.153 +              group_BijGroup)
   1.154  
   1.155  end
     2.1 --- a/src/HOL/Algebra/CRing.thy	Thu Jun 17 14:27:01 2004 +0200
     2.2 +++ b/src/HOL/Algebra/CRing.thy	Thu Jun 17 17:18:30 2004 +0200
     2.3 @@ -24,16 +24,18 @@
     2.4    "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y == x \<oplus> (\<ominus> y)"
     2.5  
     2.6  locale abelian_monoid = struct G +
     2.7 -  assumes a_comm_monoid: "comm_monoid (| carrier = carrier G,
     2.8 -      mult = add G, one = zero G |)"
     2.9 +  assumes a_comm_monoid:
    2.10 +     "comm_monoid (| carrier = carrier G, mult = add G, one = zero G |)"
    2.11 +
    2.12  
    2.13  text {*
    2.14    The following definition is redundant but simple to use.
    2.15  *}
    2.16  
    2.17  locale abelian_group = abelian_monoid +
    2.18 -  assumes a_comm_group: "comm_group (| carrier = carrier G,
    2.19 -      mult = add G, one = zero G |)"
    2.20 +  assumes a_comm_group:
    2.21 +     "comm_group (| carrier = carrier G, mult = add G, one = zero G |)"
    2.22 +
    2.23  
    2.24  subsection {* Basic Properties *}
    2.25  
    2.26 @@ -66,35 +68,19 @@
    2.27        abelian_group_axioms.intro comm_monoidI comm_groupI
    2.28      intro: prems)
    2.29  
    2.30 -(* TODO: The following thms are probably unnecessary. *)
    2.31 -
    2.32 -lemma (in abelian_monoid) a_magma:
    2.33 -  "magma (| carrier = carrier G, mult = add G, one = zero G |)"
    2.34 -  by (rule comm_monoid.axioms) (rule a_comm_monoid)
    2.35 -
    2.36 -lemma (in abelian_monoid) a_semigroup:
    2.37 -  "semigroup (| carrier = carrier G, mult = add G, one = zero G |)"
    2.38 -  by (unfold semigroup_def) (fast intro: comm_monoid.axioms a_comm_monoid)
    2.39 -
    2.40  lemma (in abelian_monoid) a_monoid:
    2.41    "monoid (| carrier = carrier G, mult = add G, one = zero G |)"
    2.42 -  by (unfold monoid_def) (fast intro: a_comm_monoid comm_monoid.axioms)
    2.43 +by (rule comm_monoid.axioms, rule a_comm_monoid) 
    2.44  
    2.45  lemma (in abelian_group) a_group:
    2.46    "group (| carrier = carrier G, mult = add G, one = zero G |)"
    2.47 -  by (unfold group_def semigroup_def)
    2.48 -    (fast intro: comm_group.axioms a_comm_group)
    2.49 +by (simp add: group_def a_monoid comm_group.axioms a_comm_group) 
    2.50  
    2.51 -lemma (in abelian_monoid) a_comm_semigroup:
    2.52 -  "comm_semigroup (| carrier = carrier G, mult = add G, one = zero G |)"
    2.53 -  by (unfold comm_semigroup_def semigroup_def)
    2.54 -    (fast intro: comm_monoid.axioms a_comm_monoid)
    2.55 -
    2.56 -lemmas monoid_record_simps = partial_object.simps semigroup.simps monoid.simps
    2.57 +lemmas monoid_record_simps = partial_object.simps monoid.simps
    2.58  
    2.59  lemma (in abelian_monoid) a_closed [intro, simp]:
    2.60 -  "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus> y \<in> carrier G"
    2.61 -  by (rule magma.m_closed [OF a_magma, simplified monoid_record_simps]) 
    2.62 +  "\<lbrakk> x \<in> carrier G; y \<in> carrier G \<rbrakk> \<Longrightarrow> x \<oplus> y \<in> carrier G"
    2.63 +  by (rule monoid.m_closed [OF a_monoid, simplified monoid_record_simps]) 
    2.64  
    2.65  lemma (in abelian_monoid) zero_closed [intro, simp]:
    2.66    "\<zero> \<in> carrier G"
    2.67 @@ -120,9 +106,9 @@
    2.68    by (rule group.r_cancel [OF a_group, simplified monoid_record_simps])
    2.69  
    2.70  lemma (in abelian_monoid) a_assoc:
    2.71 -  "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    2.72 +  "\<lbrakk>x \<in> carrier G; y \<in> carrier G; z \<in> carrier G\<rbrakk> \<Longrightarrow>
    2.73    (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
    2.74 -  by (rule semigroup.m_assoc [OF a_semigroup, simplified monoid_record_simps])
    2.75 +  by (rule monoid.m_assoc [OF a_monoid, simplified monoid_record_simps])
    2.76  
    2.77  lemma (in abelian_monoid) l_zero [simp]:
    2.78    "x \<in> carrier G ==> \<zero> \<oplus> x = x"
    2.79 @@ -134,15 +120,15 @@
    2.80      group.l_inv [OF a_group, simplified monoid_record_simps])
    2.81  
    2.82  lemma (in abelian_monoid) a_comm:
    2.83 -  "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus> y = y \<oplus> x"
    2.84 -  by (rule comm_semigroup.m_comm [OF a_comm_semigroup,
    2.85 +  "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> x \<oplus> y = y \<oplus> x"
    2.86 +  by (rule comm_monoid.m_comm [OF a_comm_monoid,
    2.87      simplified monoid_record_simps])
    2.88  
    2.89  lemma (in abelian_monoid) a_lcomm:
    2.90 -  "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    2.91 +  "\<lbrakk>x \<in> carrier G; y \<in> carrier G; z \<in> carrier G\<rbrakk> \<Longrightarrow>
    2.92     x \<oplus> (y \<oplus> z) = y \<oplus> (x \<oplus> z)"
    2.93 -  by (rule comm_semigroup.m_lcomm [OF a_comm_semigroup,
    2.94 -    simplified monoid_record_simps])
    2.95 +  by (rule comm_monoid.m_lcomm [OF a_comm_monoid,
    2.96 +                                simplified monoid_record_simps])
    2.97  
    2.98  lemma (in abelian_monoid) r_zero [simp]:
    2.99    "x \<in> carrier G ==> x \<oplus> \<zero> = x"
   2.100 @@ -329,7 +315,7 @@
   2.101        ==> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
   2.102    shows "ring R"
   2.103    by (auto intro: ring.intro
   2.104 -    abelian_group.axioms monoid.axioms ring_axioms.intro prems)
   2.105 +    abelian_group.axioms ring_axioms.intro prems)
   2.106  
   2.107  lemma (in ring) is_abelian_group:
   2.108    "abelian_group R"
   2.109 @@ -356,13 +342,12 @@
   2.110        note [simp]= comm_monoid.axioms [OF comm_monoid]
   2.111          abelian_group.axioms [OF abelian_group]
   2.112          abelian_monoid.a_closed
   2.113 -        magma.m_closed
   2.114          
   2.115        from R have "z \<otimes> (x \<oplus> y) = (x \<oplus> y) \<otimes> z"
   2.116 -        by (simp add: comm_semigroup.m_comm [OF comm_semigroup.intro])
   2.117 +        by (simp add: comm_monoid.m_comm [OF comm_monoid.intro])
   2.118        also from R have "... = x \<otimes> z \<oplus> y \<otimes> z" by (simp add: l_distr)
   2.119        also from R have "... = z \<otimes> x \<oplus> z \<otimes> y"
   2.120 -        by (simp add: comm_semigroup.m_comm [OF comm_semigroup.intro])
   2.121 +        by (simp add: comm_monoid.m_comm [OF comm_monoid.intro])
   2.122        finally show "z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y" .
   2.123      qed
   2.124    qed (auto intro: cring.intro
     3.1 --- a/src/HOL/Algebra/Coset.thy	Thu Jun 17 14:27:01 2004 +0200
     3.2 +++ b/src/HOL/Algebra/Coset.thy	Thu Jun 17 17:18:30 2004 +0200
     3.3 @@ -7,46 +7,36 @@
     3.4  
     3.5  theory Coset = Group + Exponent:
     3.6  
     3.7 -declare (in group) l_inv [simp] and r_inv [simp]
     3.8 -
     3.9  constdefs (structure G)
    3.10 -  r_coset    :: "[_, 'a set, 'a] => 'a set"    (infixl "#>\<index>" 60)
    3.11 -  "H #> a == (% x. x \<otimes> a) ` H"
    3.12 +  r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "#>\<index>" 60)
    3.13 +  "H #> a \<equiv> \<Union>h\<in>H. {h \<otimes> a}"
    3.14  
    3.15 -  l_coset    :: "[_, 'a, 'a set] => 'a set"    (infixl "<#\<index>" 60)
    3.16 -  "a <# H == (% x. a \<otimes> x) ` H"
    3.17 +  l_coset    :: "[_, 'a, 'a set] \<Rightarrow> 'a set"    (infixl "<#\<index>" 60)
    3.18 +  "a <# H \<equiv> \<Union>h\<in>H. {a \<otimes> h}"
    3.19  
    3.20 -  rcosets  :: "[_, 'a set] => ('a set)set"
    3.21 -  "rcosets G H == r_coset G H ` (carrier G)"
    3.22 +  RCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"   ("rcosets\<index> _" [81] 80)
    3.23 +  "rcosets H \<equiv> \<Union>a\<in>carrier G. {H #> a}"
    3.24 +
    3.25 +  set_mult  :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<#>\<index>" 60)
    3.26 +  "H <#> K \<equiv> \<Union>h\<in>H. \<Union>k\<in>K. {h \<otimes> k}"
    3.27  
    3.28 -  set_mult  :: "[_, 'a set ,'a set] => 'a set" (infixl "<#>\<index>" 60)
    3.29 -  "H <#> K == (%(x,y). x \<otimes> y) ` (H \<times> K)"
    3.30 +  SET_INV :: "[_,'a set] \<Rightarrow> 'a set"  ("set'_inv\<index> _" [81] 80)
    3.31 +  "set_inv H \<equiv> \<Union>h\<in>H. {inv h}"
    3.32  
    3.33 -  set_inv   :: "[_,'a set] => 'a set"
    3.34 -  "set_inv G H == m_inv G ` H"
    3.35 +
    3.36 +locale normal = subgroup + group +
    3.37 +  assumes coset_eq: "(\<forall>x \<in> carrier G. H #> x = x <# H)"
    3.38  
    3.39 -  normal     :: "['a set, _] => bool"       (infixl "<|" 60)
    3.40 -  "normal H G == subgroup H G &
    3.41 -                  (\<forall>x \<in> carrier G. r_coset G H x = l_coset G x H)"
    3.42  
    3.43 -syntax (xsymbols)
    3.44 -  normal :: "['a set, ('a,'b) monoid_scheme] => bool"  (infixl "\<lhd>" 60)
    3.45 +syntax
    3.46 +  "@normal" :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool"  (infixl "\<lhd>" 60)
    3.47 +
    3.48 +translations
    3.49 +  "H \<lhd> G" == "normal H G"
    3.50  
    3.51  
    3.52  subsection {*Basic Properties of Cosets*}
    3.53  
    3.54 -lemma (in group) r_coset_eq: "H #> a = {b . \<exists>h\<in>H. h \<otimes> a = b}"
    3.55 -by (auto simp add: r_coset_def)
    3.56 -
    3.57 -lemma (in group) l_coset_eq: "a <# H = {b . \<exists>h\<in>H. a \<otimes> h = b}"
    3.58 -by (auto simp add: l_coset_def)
    3.59 -
    3.60 -lemma (in group) setrcos_eq: "rcosets G H = {C . \<exists>a\<in>carrier G. C = H #> a}"
    3.61 -by (auto simp add: rcosets_def)
    3.62 -
    3.63 -lemma (in group) set_mult_eq: "H <#> K = {c . \<exists>h\<in>H. \<exists>k\<in>K. c = h \<otimes> k}"
    3.64 -by (simp add: set_mult_def image_def)
    3.65 -
    3.66  lemma (in group) coset_mult_assoc:
    3.67       "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
    3.68        ==> (M #> g) #> h = M #> (g \<otimes> h)"
    3.69 @@ -72,20 +62,27 @@
    3.70  lemma (in group) coset_join1:
    3.71       "[| H #> x = H;  x \<in> carrier G;  subgroup H G |] ==> x \<in> H"
    3.72  apply (erule subst)
    3.73 -apply (simp add: r_coset_eq)
    3.74 -apply (blast intro: l_one subgroup.one_closed)
    3.75 +apply (simp add: r_coset_def)
    3.76 +apply (blast intro: l_one subgroup.one_closed sym)
    3.77  done
    3.78  
    3.79  lemma (in group) solve_equation:
    3.80 -    "\<lbrakk>subgroup H G; x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. h \<otimes> x = y"
    3.81 +    "\<lbrakk>subgroup H G; x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. y = h \<otimes> x"
    3.82  apply (rule bexI [of _ "y \<otimes> (inv x)"])
    3.83  apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc
    3.84                        subgroup.subset [THEN subsetD])
    3.85  done
    3.86  
    3.87 +lemma (in group) repr_independence:
    3.88 +     "\<lbrakk>y \<in> H #> x;  x \<in> carrier G; subgroup H G\<rbrakk> \<Longrightarrow> H #> x = H #> y"
    3.89 +by (auto simp add: r_coset_def m_assoc [symmetric]
    3.90 +                   subgroup.subset [THEN subsetD]
    3.91 +                   subgroup.m_closed solve_equation)
    3.92 +
    3.93  lemma (in group) coset_join2:
    3.94 -     "[| x \<in> carrier G;  subgroup H G;  x\<in>H |] ==> H #> x = H"
    3.95 -by (force simp add: subgroup.m_closed r_coset_eq solve_equation)
    3.96 +     "\<lbrakk>x \<in> carrier G;  subgroup H G;  x\<in>H\<rbrakk> \<Longrightarrow> H #> x = H"
    3.97 +  --{*Alternative proof is to put @{term "x=\<one>"} in @{text repr_independence}.*}
    3.98 +by (force simp add: subgroup.m_closed r_coset_def solve_equation)
    3.99  
   3.100  lemma (in group) r_coset_subset_G:
   3.101       "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> H #> x \<subseteq> carrier G"
   3.102 @@ -95,10 +92,9 @@
   3.103       "[| h \<in> H; H \<subseteq> carrier G; x \<in> carrier G|] ==> h \<otimes> x \<in> H #> x"
   3.104  by (auto simp add: r_coset_def)
   3.105  
   3.106 -lemma (in group) setrcosI:
   3.107 -     "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> H #> x \<in> rcosets G H"
   3.108 -by (auto simp add: setrcos_eq)
   3.109 -
   3.110 +lemma (in group) rcosetsI:
   3.111 +     "\<lbrakk>H \<subseteq> carrier G; x \<in> carrier G\<rbrakk> \<Longrightarrow> H #> x \<in> rcosets H"
   3.112 +by (auto simp add: RCOSETS_def)
   3.113  
   3.114  text{*Really needed?*}
   3.115  lemma (in group) transpose_inv:
   3.116 @@ -106,37 +102,37 @@
   3.117        ==> (inv x) \<otimes> z = y"
   3.118  by (force simp add: m_assoc [symmetric])
   3.119  
   3.120 -lemma (in group) repr_independence:
   3.121 -     "[| y \<in> H #> x;  x \<in> carrier G; subgroup H G |] ==> H #> x = H #> y"
   3.122 -by (auto simp add: r_coset_eq m_assoc [symmetric]
   3.123 -                   subgroup.subset [THEN subsetD]
   3.124 -                   subgroup.m_closed solve_equation)
   3.125 -
   3.126  lemma (in group) rcos_self: "[| x \<in> carrier G; subgroup H G |] ==> x \<in> H #> x"
   3.127 -apply (simp add: r_coset_eq)
   3.128 -apply (blast intro: l_one subgroup.subset [THEN subsetD]
   3.129 +apply (simp add: r_coset_def)
   3.130 +apply (blast intro: sym l_one subgroup.subset [THEN subsetD]
   3.131                      subgroup.one_closed)
   3.132  done
   3.133  
   3.134  
   3.135  subsection {* Normal subgroups *}
   3.136  
   3.137 -lemma normal_imp_subgroup: "H <| G ==> subgroup H G"
   3.138 -by (simp add: normal_def)
   3.139 +lemma normal_imp_subgroup: "H \<lhd> G \<Longrightarrow> subgroup H G"
   3.140 +  by (simp add: normal_def subgroup_def)
   3.141  
   3.142 -lemma (in group) normal_inv_op_closed1:
   3.143 -     "\<lbrakk>H \<lhd> G; x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<otimes> h \<otimes> x \<in> H"
   3.144 -apply (auto simp add: l_coset_def r_coset_def normal_def)
   3.145 +lemma (in group) normalI: 
   3.146 +  "subgroup H G \<Longrightarrow> (\<forall>x \<in> carrier G. H #> x = x <# H) \<Longrightarrow> H \<lhd> G";
   3.147 +  by (simp add: normal_def normal_axioms_def prems) 
   3.148 +
   3.149 +lemma (in normal) inv_op_closed1:
   3.150 +     "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<otimes> h \<otimes> x \<in> H"
   3.151 +apply (insert coset_eq) 
   3.152 +apply (auto simp add: l_coset_def r_coset_def)
   3.153  apply (drule bspec, assumption)
   3.154  apply (drule equalityD1 [THEN subsetD], blast, clarify)
   3.155 -apply (simp add: m_assoc subgroup.subset [THEN subsetD])
   3.156 -apply (simp add: m_assoc [symmetric] subgroup.subset [THEN subsetD])
   3.157 +apply (simp add: m_assoc)
   3.158 +apply (simp add: m_assoc [symmetric])
   3.159  done
   3.160  
   3.161 -lemma (in group) normal_inv_op_closed2:
   3.162 -     "\<lbrakk>H \<lhd> G; x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> (inv x) \<in> H"
   3.163 -apply (drule normal_inv_op_closed1 [of H "(inv x)"])
   3.164 -apply auto
   3.165 +lemma (in normal) inv_op_closed2:
   3.166 +     "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> (inv x) \<in> H"
   3.167 +apply (subgoal_tac "inv (inv x) \<otimes> h \<otimes> (inv x) \<in> H") 
   3.168 +apply (simp add: ); 
   3.169 +apply (blast intro: inv_op_closed1) 
   3.170  done
   3.171  
   3.172  text{*Alternative characterization of normal subgroups*}
   3.173 @@ -147,46 +143,47 @@
   3.174  proof
   3.175    assume N: "N \<lhd> G"
   3.176    show ?rhs
   3.177 -    by (blast intro: N normal_imp_subgroup normal_inv_op_closed2) 
   3.178 +    by (blast intro: N normal.inv_op_closed2 normal_imp_subgroup) 
   3.179  next
   3.180    assume ?rhs
   3.181    hence sg: "subgroup N G" 
   3.182 -    and closed: "!!x. x\<in>carrier G ==> \<forall>h\<in>N. x \<otimes> h \<otimes> inv x \<in> N" by auto
   3.183 +    and closed: "\<And>x. x\<in>carrier G \<Longrightarrow> \<forall>h\<in>N. x \<otimes> h \<otimes> inv x \<in> N" by auto
   3.184    hence sb: "N \<subseteq> carrier G" by (simp add: subgroup.subset) 
   3.185    show "N \<lhd> G"
   3.186 -  proof (simp add: sg normal_def l_coset_def r_coset_def, clarify)
   3.187 +  proof (intro normalI [OF sg], simp add: l_coset_def r_coset_def, clarify)
   3.188      fix x
   3.189      assume x: "x \<in> carrier G"
   3.190 -    show "(\<lambda>n. n \<otimes> x) ` N = op \<otimes> x ` N"
   3.191 +    show "(\<Union>\<^bsub>h\<in>N\<^esub> {h \<otimes> x}) = (\<Union>\<^bsub>h\<in>N\<^esub> {x \<otimes> h})"
   3.192      proof
   3.193 -      show "(\<lambda>n. n \<otimes> x) ` N \<subseteq> op \<otimes> x ` N"
   3.194 +      show "(\<Union>\<^bsub>h\<in>N\<^esub> {h \<otimes> x}) \<subseteq> (\<Union>\<^bsub>h\<in>N\<^esub> {x \<otimes> h})"
   3.195        proof clarify
   3.196          fix n
   3.197          assume n: "n \<in> N" 
   3.198 -        show "n \<otimes> x \<in> op \<otimes> x ` N"
   3.199 +        show "n \<otimes> x \<in> (\<Union>\<^bsub>h\<in>N\<^esub> {x \<otimes> h})"
   3.200          proof 
   3.201 -          show "n \<otimes> x = x \<otimes> (inv x \<otimes> n \<otimes> x)"
   3.202 +          from closed [of "inv x"]
   3.203 +          show "inv x \<otimes> n \<otimes> x \<in> N" by (simp add: x n)
   3.204 +          show "n \<otimes> x \<in> {x \<otimes> (inv x \<otimes> n \<otimes> x)}"
   3.205              by (simp add: x n m_assoc [symmetric] sb [THEN subsetD])
   3.206 -          with closed [of "inv x"]
   3.207 -          show "inv x \<otimes> n \<otimes> x \<in> N" by (simp add: x n)
   3.208          qed
   3.209        qed
   3.210      next
   3.211 -      show "op \<otimes> x ` N \<subseteq> (\<lambda>n. n \<otimes> x) ` N" 
   3.212 +      show "(\<Union>\<^bsub>h\<in>N\<^esub> {x \<otimes> h}) \<subseteq> (\<Union>\<^bsub>h\<in>N\<^esub> {h \<otimes> x})"
   3.213        proof clarify
   3.214          fix n
   3.215          assume n: "n \<in> N" 
   3.216 -        show "x \<otimes> n \<in> (\<lambda>n. n \<otimes> x) ` N"
   3.217 +        show "x \<otimes> n \<in> (\<Union>\<^bsub>h\<in>N\<^esub> {h \<otimes> x})"
   3.218          proof 
   3.219 -          show "x \<otimes> n = (x \<otimes> n \<otimes> inv x) \<otimes> x"
   3.220 +          show "x \<otimes> n \<otimes> inv x \<in> N" by (simp add: x n closed)
   3.221 +          show "x \<otimes> n \<in> {x \<otimes> n \<otimes> inv x \<otimes> x}"
   3.222              by (simp add: x n m_assoc sb [THEN subsetD])
   3.223 -          show "x \<otimes> n \<otimes> inv x \<in> N" by (simp add: x n closed)
   3.224          qed
   3.225        qed
   3.226      qed
   3.227    qed
   3.228  qed
   3.229  
   3.230 +
   3.231  subsection{*More Properties of Cosets*}
   3.232  
   3.233  lemma (in group) lcos_m_assoc:
   3.234 @@ -202,15 +199,15 @@
   3.235  by (auto simp add: l_coset_def subsetD)
   3.236  
   3.237  lemma (in group) l_coset_swap:
   3.238 -     "[| y \<in> x <# H;  x \<in> carrier G;  subgroup H G |] ==> x \<in> y <# H"
   3.239 -proof (simp add: l_coset_eq)
   3.240 -  assume "\<exists>h\<in>H. x \<otimes> h = y"
   3.241 +     "\<lbrakk>y \<in> x <# H;  x \<in> carrier G;  subgroup H G\<rbrakk> \<Longrightarrow> x \<in> y <# H"
   3.242 +proof (simp add: l_coset_def)
   3.243 +  assume "\<exists>h\<in>H. y = x \<otimes> h"
   3.244      and x: "x \<in> carrier G"
   3.245      and sb: "subgroup H G"
   3.246    then obtain h' where h': "h' \<in> H & x \<otimes> h' = y" by blast
   3.247 -  show "\<exists>h\<in>H. y \<otimes> h = x"
   3.248 +  show "\<exists>h\<in>H. x = y \<otimes> h"
   3.249    proof
   3.250 -    show "y \<otimes> inv h' = x" using h' x sb
   3.251 +    show "x = y \<otimes> inv h'" using h' x sb
   3.252        by (auto simp add: m_assoc subgroup.subset [THEN subsetD])
   3.253      show "inv h' \<in> H" using h' sb
   3.254        by (auto simp add: subgroup.subset [THEN subsetD] subgroup.m_inv_closed)
   3.255 @@ -244,11 +241,11 @@
   3.256  qed
   3.257  
   3.258  lemma (in group) setmult_subset_G:
   3.259 -     "[| H \<subseteq> carrier G; K \<subseteq> carrier G |] ==> H <#> K \<subseteq> carrier G"
   3.260 -by (auto simp add: set_mult_eq subsetD)
   3.261 +     "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G\<rbrakk> \<Longrightarrow> H <#> K \<subseteq> carrier G"
   3.262 +by (auto simp add: set_mult_def subsetD)
   3.263  
   3.264 -lemma (in group) subgroup_mult_id: "subgroup H G ==> H <#> H = H"
   3.265 -apply (auto simp add: subgroup.m_closed set_mult_eq Sigma_def image_def)
   3.266 +lemma (in group) subgroup_mult_id: "subgroup H G \<Longrightarrow> H <#> H = H"
   3.267 +apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def image_def)
   3.268  apply (rule_tac x = x in bexI)
   3.269  apply (rule bexI [of _ "\<one>"])
   3.270  apply (auto simp add: subgroup.m_closed subgroup.one_closed
   3.271 @@ -258,135 +255,180 @@
   3.272  
   3.273  subsubsection {* Set of inverses of an @{text r_coset}. *}
   3.274  
   3.275 -lemma (in group) rcos_inv:
   3.276 -  assumes normalHG: "H <| G"
   3.277 -      and x:     "x \<in> carrier G"
   3.278 -  shows "set_inv G (H #> x) = H #> (inv x)"
   3.279 -proof -
   3.280 -  have H_subset: "H \<subseteq> carrier G"
   3.281 -    by (rule subgroup.subset [OF normal_imp_subgroup, OF normalHG])
   3.282 -  show ?thesis
   3.283 -  proof (auto simp add: r_coset_eq image_def set_inv_def)
   3.284 -    fix h
   3.285 -    assume "h \<in> H"
   3.286 -      hence "((inv x) \<otimes> (inv h) \<otimes> x) \<otimes> inv x = inv (h \<otimes> x)"
   3.287 -        by (simp add: x m_assoc inv_mult_group H_subset [THEN subsetD])
   3.288 -      thus "\<exists>j\<in>H. j \<otimes> inv x = inv (h \<otimes> x)"
   3.289 -       using prems
   3.290 -        by (blast intro: normal_inv_op_closed1 normal_imp_subgroup
   3.291 -                         subgroup.m_inv_closed)
   3.292 -  next
   3.293 -    fix h
   3.294 -    assume "h \<in> H"
   3.295 -      hence eq: "(x \<otimes> (inv h) \<otimes> (inv x)) \<otimes> x = x \<otimes> inv h"
   3.296 -        by (simp add: x m_assoc H_subset [THEN subsetD])
   3.297 -      hence "(\<exists>j\<in>H. j \<otimes> x = inv  (h \<otimes> (inv x))) \<and> h \<otimes> inv x = inv (inv (h \<otimes> (inv x)))"
   3.298 -       using prems
   3.299 -        by (simp add: m_assoc inv_mult_group H_subset [THEN subsetD],
   3.300 -            blast intro: eq normal_inv_op_closed2 normal_imp_subgroup
   3.301 -                         subgroup.m_inv_closed)
   3.302 -      thus "\<exists>y. (\<exists>h\<in>H. h \<otimes> x = y) \<and> h \<otimes> inv x = inv y" ..
   3.303 +lemma (in normal) rcos_inv:
   3.304 +  assumes x:     "x \<in> carrier G"
   3.305 +  shows "set_inv (H #> x) = H #> (inv x)" 
   3.306 +proof (simp add: r_coset_def SET_INV_def x inv_mult_group, safe)
   3.307 +  fix h
   3.308 +  assume "h \<in> H"
   3.309 +  show "inv x \<otimes> inv h \<in> (\<Union>\<^bsub>j\<in>H\<^esub> {j \<otimes> inv x})"
   3.310 +  proof
   3.311 +    show "inv x \<otimes> inv h \<otimes> x \<in> H"
   3.312 +      by (simp add: inv_op_closed1 prems)
   3.313 +    show "inv x \<otimes> inv h \<in> {inv x \<otimes> inv h \<otimes> x \<otimes> inv x}"
   3.314 +      by (simp add: prems m_assoc)
   3.315 +  qed
   3.316 +next
   3.317 +  fix h
   3.318 +  assume "h \<in> H"
   3.319 +  show "h \<otimes> inv x \<in> (\<Union>\<^bsub>j\<in>H\<^esub> {inv x \<otimes> inv j})"
   3.320 +  proof
   3.321 +    show "x \<otimes> inv h \<otimes> inv x \<in> H"
   3.322 +      by (simp add: inv_op_closed2 prems)
   3.323 +    show "h \<otimes> inv x \<in> {inv x \<otimes> inv (x \<otimes> inv h \<otimes> inv x)}"
   3.324 +      by (simp add: prems m_assoc [symmetric] inv_mult_group)
   3.325    qed
   3.326  qed
   3.327  
   3.328 -lemma (in group) rcos_inv2:
   3.329 -     "[| H <| G; K \<in> rcosets G H; x \<in> K |] ==> set_inv G K = H #> (inv x)"
   3.330 -apply (simp add: setrcos_eq, clarify)
   3.331 -apply (subgoal_tac "x : carrier G")
   3.332 - prefer 2
   3.333 - apply (blast dest: r_coset_subset_G subgroup.subset normal_imp_subgroup)
   3.334 -apply (drule repr_independence)
   3.335 -  apply assumption
   3.336 - apply (erule normal_imp_subgroup)
   3.337 -apply (simp add: rcos_inv)
   3.338 -done
   3.339 -
   3.340  
   3.341  subsubsection {*Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.*}
   3.342  
   3.343  lemma (in group) setmult_rcos_assoc:
   3.344 -     "[| H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G |]
   3.345 -      ==> H <#> (K #> x) = (H <#> K) #> x"
   3.346 -apply (auto simp add: r_coset_def set_mult_def)
   3.347 -apply (force simp add: m_assoc)+
   3.348 -done
   3.349 +     "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
   3.350 +      \<Longrightarrow> H <#> (K #> x) = (H <#> K) #> x"
   3.351 +by (force simp add: r_coset_def set_mult_def m_assoc)
   3.352  
   3.353  lemma (in group) rcos_assoc_lcos:
   3.354 -     "[| H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G |]
   3.355 -      ==> (H #> x) <#> K = H <#> (x <# K)"
   3.356 -apply (auto simp add: r_coset_def l_coset_def set_mult_def Sigma_def image_def)
   3.357 -apply (force intro!: exI bexI simp add: m_assoc)+
   3.358 -done
   3.359 +     "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
   3.360 +      \<Longrightarrow> (H #> x) <#> K = H <#> (x <# K)"
   3.361 +by (force simp add: r_coset_def l_coset_def set_mult_def m_assoc)
   3.362  
   3.363 -lemma (in group) rcos_mult_step1:
   3.364 -     "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
   3.365 -      ==> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
   3.366 -by (simp add: setmult_rcos_assoc normal_imp_subgroup [THEN subgroup.subset]
   3.367 +lemma (in normal) rcos_mult_step1:
   3.368 +     "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
   3.369 +      \<Longrightarrow> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
   3.370 +by (simp add: setmult_rcos_assoc subset
   3.371                r_coset_subset_G l_coset_subset_G rcos_assoc_lcos)
   3.372  
   3.373 -lemma (in group) rcos_mult_step2:
   3.374 -     "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
   3.375 -      ==> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"
   3.376 -by (simp add: normal_def)
   3.377 +lemma (in normal) rcos_mult_step2:
   3.378 +     "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
   3.379 +      \<Longrightarrow> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"
   3.380 +by (insert coset_eq, simp add: normal_def)
   3.381  
   3.382 -lemma (in group) rcos_mult_step3:
   3.383 -     "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
   3.384 -      ==> (H <#> (H #> x)) #> y = H #> (x \<otimes> y)"
   3.385 -by (simp add: setmult_rcos_assoc r_coset_subset_G coset_mult_assoc
   3.386 -              setmult_subset_G  subgroup_mult_id
   3.387 -              subgroup.subset normal_imp_subgroup)
   3.388 +lemma (in normal) rcos_mult_step3:
   3.389 +     "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
   3.390 +      \<Longrightarrow> (H <#> (H #> x)) #> y = H #> (x \<otimes> y)"
   3.391 +by (simp add: setmult_rcos_assoc coset_mult_assoc
   3.392 +              subgroup_mult_id subset prems)
   3.393  
   3.394 -lemma (in group) rcos_sum:
   3.395 -     "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
   3.396 -      ==> (H #> x) <#> (H #> y) = H #> (x \<otimes> y)"
   3.397 +lemma (in normal) rcos_sum:
   3.398 +     "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
   3.399 +      \<Longrightarrow> (H #> x) <#> (H #> y) = H #> (x \<otimes> y)"
   3.400  by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)
   3.401  
   3.402 -lemma (in group) setrcos_mult_eq: "[|H <| G; M \<in> rcosets G H|] ==> H <#> M = M"
   3.403 +lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M"
   3.404    -- {* generalizes @{text subgroup_mult_id} *}
   3.405 -  by (auto simp add: setrcos_eq normal_imp_subgroup subgroup.subset
   3.406 -    setmult_rcos_assoc subgroup_mult_id)
   3.407 +  by (auto simp add: RCOSETS_def subset
   3.408 +        setmult_rcos_assoc subgroup_mult_id prems)
   3.409 +
   3.410 +
   3.411 +subsubsection{*An Equivalence Relation*}
   3.412 +
   3.413 +constdefs (structure G)
   3.414 +  r_congruent :: "[('a,'b)monoid_scheme, 'a set] \<Rightarrow> ('a*'a)set"
   3.415 +                  ("rcong\<index> _")
   3.416 +   "rcong H \<equiv> {(x,y). x \<in> carrier G & y \<in> carrier G & inv x \<otimes> y \<in> H}"
   3.417 +
   3.418 +
   3.419 +lemma (in subgroup) equiv_rcong:
   3.420 +   includes group G
   3.421 +   shows "equiv (carrier G) (rcong H)"
   3.422 +proof (intro equiv.intro)
   3.423 +  show "refl (carrier G) (rcong H)"
   3.424 +    by (auto simp add: r_congruent_def refl_def) 
   3.425 +next
   3.426 +  show "sym (rcong H)"
   3.427 +  proof (simp add: r_congruent_def sym_def, clarify)
   3.428 +    fix x y
   3.429 +    assume [simp]: "x \<in> carrier G" "y \<in> carrier G" 
   3.430 +       and "inv x \<otimes> y \<in> H"
   3.431 +    hence "inv (inv x \<otimes> y) \<in> H" by (simp add: m_inv_closed) 
   3.432 +    thus "inv y \<otimes> x \<in> H" by (simp add: inv_mult_group)
   3.433 +  qed
   3.434 +next
   3.435 +  show "trans (rcong H)"
   3.436 +  proof (simp add: r_congruent_def trans_def, clarify)
   3.437 +    fix x y z
   3.438 +    assume [simp]: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
   3.439 +       and "inv x \<otimes> y \<in> H" and "inv y \<otimes> z \<in> H"
   3.440 +    hence "(inv x \<otimes> y) \<otimes> (inv y \<otimes> z) \<in> H" by simp
   3.441 +    hence "inv x \<otimes> (y \<otimes> inv y) \<otimes> z \<in> H" by (simp add: m_assoc del: r_inv) 
   3.442 +    thus "inv x \<otimes> z \<in> H" by simp
   3.443 +  qed
   3.444 +qed
   3.445 +
   3.446 +text{*Equivalence classes of @{text rcong} correspond to left cosets.
   3.447 +  Was there a mistake in the definitions? I'd have expected them to
   3.448 +  correspond to right cosets.*}
   3.449 +
   3.450 +(* CB: This is correct, but subtle.
   3.451 +   We call H #> a the right coset of a relative to H.  According to
   3.452 +   Jacobson, this is what the majority of group theory literature does.
   3.453 +   He then defines the notion of congruence relation ~ over monoids as
   3.454 +   equivalence relation with a ~ a' & b ~ b' \<Longrightarrow> a*b ~ a'*b'.
   3.455 +   Our notion of right congruence induced by K: rcong K appears only in
   3.456 +   the context where K is a normal subgroup.  Jacobson doesn't name it.
   3.457 +   But in this context left and right cosets are identical.
   3.458 +*)
   3.459 +
   3.460 +lemma (in subgroup) l_coset_eq_rcong:
   3.461 +  includes group G
   3.462 +  assumes a: "a \<in> carrier G"
   3.463 +  shows "a <# H = rcong H `` {a}"
   3.464 +by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a ) 
   3.465  
   3.466  
   3.467  subsubsection{*Two distinct right cosets are disjoint*}
   3.468  
   3.469  lemma (in group) rcos_equation:
   3.470 -     "[|subgroup H G;  a \<in> carrier G;  b \<in> carrier G;  ha \<otimes> a = h \<otimes> b;
   3.471 -        h \<in> H;  ha \<in> H;  hb \<in> H|]
   3.472 -      ==> \<exists>h\<in>H. h \<otimes> b = hb \<otimes> a"
   3.473 -apply (rule bexI [of _"hb \<otimes> ((inv ha) \<otimes> h)"])
   3.474 -apply (simp  add: m_assoc transpose_inv subgroup.subset [THEN subsetD])
   3.475 -apply (simp add: subgroup.m_closed subgroup.m_inv_closed)
   3.476 +  includes subgroup H G
   3.477 +  shows
   3.478 +     "\<lbrakk>ha \<otimes> a = h \<otimes> b; a \<in> carrier G;  b \<in> carrier G;  
   3.479 +        h \<in> H;  ha \<in> H;  hb \<in> H\<rbrakk>
   3.480 +      \<Longrightarrow> hb \<otimes> a \<in> (\<Union>h\<in>H. {h \<otimes> b})"
   3.481 +apply (rule UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"])
   3.482 +apply (simp add: ); 
   3.483 +apply (simp add: m_assoc transpose_inv)
   3.484  done
   3.485  
   3.486  lemma (in group) rcos_disjoint:
   3.487 -     "[|subgroup H G; a \<in> rcosets G H; b \<in> rcosets G H; a\<noteq>b|] ==> a \<inter> b = {}"
   3.488 -apply (simp add: setrcos_eq r_coset_eq)
   3.489 -apply (blast intro: rcos_equation sym)
   3.490 +  includes subgroup H G
   3.491 +  shows "\<lbrakk>a \<in> rcosets H; b \<in> rcosets H; a\<noteq>b\<rbrakk> \<Longrightarrow> a \<inter> b = {}"
   3.492 +apply (simp add: RCOSETS_def r_coset_def)
   3.493 +apply (blast intro: rcos_equation prems sym)
   3.494  done
   3.495  
   3.496  
   3.497  subsection {*Order of a Group and Lagrange's Theorem*}
   3.498  
   3.499  constdefs
   3.500 -  order :: "('a, 'b) semigroup_scheme => nat"
   3.501 -  "order S == card (carrier S)"
   3.502 +  order :: "('a, 'b) monoid_scheme \<Rightarrow> nat"
   3.503 +  "order S \<equiv> card (carrier S)"
   3.504  
   3.505 -lemma (in group) setrcos_part_G: "subgroup H G ==> \<Union>rcosets G H = carrier G"
   3.506 +lemma (in group) rcos_self:
   3.507 +  includes subgroup
   3.508 +  shows "x \<in> carrier G \<Longrightarrow> x \<in> H #> x"
   3.509 +apply (simp add: r_coset_def)
   3.510 +apply (rule_tac x="\<one>" in bexI) 
   3.511 +apply (auto simp add: ); 
   3.512 +done
   3.513 +
   3.514 +lemma (in group) rcosets_part_G:
   3.515 +  includes subgroup
   3.516 +  shows "\<Union>(rcosets H) = carrier G"
   3.517  apply (rule equalityI)
   3.518 -apply (force simp add: subgroup.subset [THEN subsetD]
   3.519 -                       setrcos_eq r_coset_def)
   3.520 -apply (auto simp add: setrcos_eq subgroup.subset rcos_self)
   3.521 + apply (force simp add: RCOSETS_def r_coset_def)
   3.522 +apply (auto simp add: RCOSETS_def intro: rcos_self prems)
   3.523  done
   3.524  
   3.525  lemma (in group) cosets_finite:
   3.526 -     "[| c \<in> rcosets G H;  H \<subseteq> carrier G;  finite (carrier G) |] ==> finite c"
   3.527 -apply (auto simp add: setrcos_eq)
   3.528 -apply (simp (no_asm_simp) add: r_coset_subset_G [THEN finite_subset])
   3.529 +     "\<lbrakk>c \<in> rcosets H;  H \<subseteq> carrier G;  finite (carrier G)\<rbrakk> \<Longrightarrow> finite c"
   3.530 +apply (auto simp add: RCOSETS_def)
   3.531 +apply (simp add: r_coset_subset_G [THEN finite_subset])
   3.532  done
   3.533  
   3.534  text{*The next two lemmas support the proof of @{text card_cosets_equal}.*}
   3.535  lemma (in group) inj_on_f:
   3.536 -    "[|H \<subseteq> carrier G;  a \<in> carrier G|] ==> inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
   3.537 +    "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
   3.538  apply (rule inj_onI)
   3.539  apply (subgoal_tac "x \<in> carrier G & y \<in> carrier G")
   3.540   prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])
   3.541 @@ -394,13 +436,13 @@
   3.542  done
   3.543  
   3.544  lemma (in group) inj_on_g:
   3.545 -    "[|H \<subseteq> carrier G;  a \<in> carrier G|] ==> inj_on (\<lambda>y. y \<otimes> a) H"
   3.546 +    "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> a) H"
   3.547  by (force simp add: inj_on_def subsetD)
   3.548  
   3.549  lemma (in group) card_cosets_equal:
   3.550 -     "[| c \<in> rcosets G H;  H \<subseteq> carrier G; finite(carrier G) |]
   3.551 -      ==> card c = card H"
   3.552 -apply (auto simp add: setrcos_eq)
   3.553 +     "\<lbrakk>c \<in> rcosets H;  H \<subseteq> carrier G; finite(carrier G)\<rbrakk>
   3.554 +      \<Longrightarrow> card c = card H"
   3.555 +apply (auto simp add: RCOSETS_def)
   3.556  apply (rule card_bij_eq)
   3.557       apply (rule inj_on_f, assumption+)
   3.558      apply (force simp add: m_assoc subsetD r_coset_def)
   3.559 @@ -411,21 +453,21 @@
   3.560  apply (blast intro: finite_subset)
   3.561  done
   3.562  
   3.563 -lemma (in group) setrcos_subset_PowG:
   3.564 -     "subgroup H G  ==> rcosets G H \<subseteq> Pow(carrier G)"
   3.565 -apply (simp add: setrcos_eq)
   3.566 +lemma (in group) rcosets_subset_PowG:
   3.567 +     "subgroup H G  \<Longrightarrow> rcosets H \<subseteq> Pow(carrier G)"
   3.568 +apply (simp add: RCOSETS_def)
   3.569  apply (blast dest: r_coset_subset_G subgroup.subset)
   3.570  done
   3.571  
   3.572  
   3.573  theorem (in group) lagrange:
   3.574 -     "[| finite(carrier G); subgroup H G |]
   3.575 -      ==> card(rcosets G H) * card(H) = order(G)"
   3.576 -apply (simp (no_asm_simp) add: order_def setrcos_part_G [symmetric])
   3.577 +     "\<lbrakk>finite(carrier G); subgroup H G\<rbrakk>
   3.578 +      \<Longrightarrow> card(rcosets H) * card(H) = order(G)"
   3.579 +apply (simp (no_asm_simp) add: order_def rcosets_part_G [symmetric])
   3.580  apply (subst mult_commute)
   3.581  apply (rule card_partition)
   3.582 -   apply (simp add: setrcos_subset_PowG [THEN finite_subset])
   3.583 -  apply (simp add: setrcos_part_G)
   3.584 +   apply (simp add: rcosets_subset_PowG [THEN finite_subset])
   3.585 +  apply (simp add: rcosets_part_G)
   3.586   apply (simp add: card_cosets_equal subgroup.subset)
   3.587  apply (simp add: rcos_disjoint)
   3.588  done
   3.589 @@ -434,99 +476,85 @@
   3.590  subsection {*Quotient Groups: Factorization of a Group*}
   3.591  
   3.592  constdefs
   3.593 -  FactGroup :: "[('a,'b) monoid_scheme, 'a set] => ('a set) monoid"
   3.594 +  FactGroup :: "[('a,'b) monoid_scheme, 'a set] \<Rightarrow> ('a set) monoid"
   3.595       (infixl "Mod" 65)
   3.596      --{*Actually defined for groups rather than monoids*}
   3.597 -  "FactGroup G H ==
   3.598 -    (| carrier = rcosets G H, mult = set_mult G, one = H |)"
   3.599 +  "FactGroup G H \<equiv>
   3.600 +    \<lparr>carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\<rparr>"
   3.601  
   3.602 -lemma (in group) setmult_closed:
   3.603 -     "[| H <| G; K1 \<in> rcosets G H; K2 \<in> rcosets G H |]
   3.604 -      ==> K1 <#> K2 \<in> rcosets G H"
   3.605 -by (auto simp add: normal_imp_subgroup [THEN subgroup.subset]
   3.606 -                   rcos_sum setrcos_eq)
   3.607 +lemma (in normal) setmult_closed:
   3.608 +     "\<lbrakk>K1 \<in> rcosets H; K2 \<in> rcosets H\<rbrakk> \<Longrightarrow> K1 <#> K2 \<in> rcosets H"
   3.609 +by (auto simp add: rcos_sum RCOSETS_def)
   3.610  
   3.611 -lemma (in group) setinv_closed:
   3.612 -     "[| H <| G; K \<in> rcosets G H |] ==> set_inv G K \<in> rcosets G H"
   3.613 -by (auto simp add: normal_imp_subgroup
   3.614 -                   subgroup.subset rcos_inv
   3.615 -                   setrcos_eq)
   3.616 +lemma (in normal) setinv_closed:
   3.617 +     "K \<in> rcosets H \<Longrightarrow> set_inv K \<in> rcosets H"
   3.618 +by (auto simp add: rcos_inv RCOSETS_def)
   3.619  
   3.620 -lemma (in group) setrcos_assoc:
   3.621 -     "[|H <| G; M1 \<in> rcosets G H; M2 \<in> rcosets G H; M3 \<in> rcosets G H|]
   3.622 -      ==> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
   3.623 -by (auto simp add: setrcos_eq rcos_sum normal_imp_subgroup
   3.624 -                   subgroup.subset m_assoc)
   3.625 +lemma (in normal) rcosets_assoc:
   3.626 +     "\<lbrakk>M1 \<in> rcosets H; M2 \<in> rcosets H; M3 \<in> rcosets H\<rbrakk>
   3.627 +      \<Longrightarrow> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
   3.628 +by (auto simp add: RCOSETS_def rcos_sum m_assoc)
   3.629  
   3.630 -lemma (in group) subgroup_in_rcosets:
   3.631 -  "subgroup H G ==> H \<in> rcosets G H"
   3.632 +lemma (in subgroup) subgroup_in_rcosets:
   3.633 +  includes group G
   3.634 +  shows "H \<in> rcosets H"
   3.635  proof -
   3.636 -  assume sub: "subgroup H G"
   3.637 -  have "r_coset G H \<one> = H"
   3.638 -    by (rule coset_join2)
   3.639 -       (auto intro: sub subgroup.one_closed)
   3.640 +  have "H #> \<one> = H"
   3.641 +    by (rule coset_join2, auto)
   3.642    then show ?thesis
   3.643 -    by (auto simp add: setrcos_eq)
   3.644 +    by (auto simp add: RCOSETS_def)
   3.645  qed
   3.646  
   3.647 -lemma (in group) setrcos_inv_mult_group_eq:
   3.648 -     "[|H <| G; M \<in> rcosets G H|] ==> set_inv G M <#> M = H"
   3.649 -by (auto simp add: setrcos_eq rcos_inv rcos_sum normal_imp_subgroup
   3.650 -                   subgroup.subset)
   3.651 -(*
   3.652 -lemma (in group) factorgroup_is_magma:
   3.653 -  "H <| G ==> magma (G Mod H)"
   3.654 -  by rule (simp add: FactGroup_def coset.setmult_closed [OF is_coset])
   3.655 +lemma (in normal) rcosets_inv_mult_group_eq:
   3.656 +     "M \<in> rcosets H \<Longrightarrow> set_inv M <#> M = H"
   3.657 +by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset prems)
   3.658  
   3.659 -lemma (in group) factorgroup_semigroup_axioms:
   3.660 -  "H <| G ==> semigroup_axioms (G Mod H)"
   3.661 -  by rule (simp add: FactGroup_def coset.setrcos_assoc [OF is_coset]
   3.662 -    coset.setmult_closed [OF is_coset])
   3.663 -*)
   3.664 -theorem (in group) factorgroup_is_group:
   3.665 -  "H <| G ==> group (G Mod H)"
   3.666 +theorem (in normal) factorgroup_is_group:
   3.667 +  "group (G Mod H)"
   3.668  apply (simp add: FactGroup_def)
   3.669  apply (rule groupI)
   3.670      apply (simp add: setmult_closed)
   3.671 -   apply (simp add: normal_imp_subgroup subgroup_in_rcosets)
   3.672 -  apply (simp add: restrictI setmult_closed setrcos_assoc)
   3.673 +   apply (simp add: normal_imp_subgroup subgroup_in_rcosets [OF is_group])
   3.674 +  apply (simp add: restrictI setmult_closed rcosets_assoc)
   3.675   apply (simp add: normal_imp_subgroup
   3.676 -                  subgroup_in_rcosets setrcos_mult_eq)
   3.677 -apply (auto dest: setrcos_inv_mult_group_eq simp add: setinv_closed)
   3.678 +                  subgroup_in_rcosets rcosets_mult_eq)
   3.679 +apply (auto dest: rcosets_inv_mult_group_eq simp add: setinv_closed)
   3.680  done
   3.681  
   3.682  lemma mult_FactGroup [simp]: "X \<otimes>\<^bsub>(G Mod H)\<^esub> X' = X <#>\<^bsub>G\<^esub> X'"
   3.683    by (simp add: FactGroup_def) 
   3.684  
   3.685 -lemma (in group) inv_FactGroup:
   3.686 -     "N <| G ==> X \<in> carrier (G Mod N) ==> inv\<^bsub>G Mod N\<^esub> X = set_inv G X"
   3.687 +lemma (in normal) inv_FactGroup:
   3.688 +     "X \<in> carrier (G Mod H) \<Longrightarrow> inv\<^bsub>G Mod H\<^esub> X = set_inv X"
   3.689  apply (rule group.inv_equality [OF factorgroup_is_group]) 
   3.690 -apply (simp_all add: FactGroup_def setinv_closed setrcos_inv_mult_group_eq)
   3.691 +apply (simp_all add: FactGroup_def setinv_closed rcosets_inv_mult_group_eq)
   3.692  done
   3.693  
   3.694  text{*The coset map is a homomorphism from @{term G} to the quotient group
   3.695 -  @{term "G Mod N"}*}
   3.696 -lemma (in group) r_coset_hom_Mod:
   3.697 -  assumes N: "N <| G"
   3.698 -  shows "(r_coset G N) \<in> hom G (G Mod N)"
   3.699 -by (simp add: FactGroup_def rcosets_def Pi_def hom_def rcos_sum N) 
   3.700 +  @{term "G Mod H"}*}
   3.701 +lemma (in normal) r_coset_hom_Mod:
   3.702 +  "(\<lambda>a. H #> a) \<in> hom G (G Mod H)"
   3.703 +  by (auto simp add: FactGroup_def RCOSETS_def Pi_def hom_def rcos_sum)
   3.704  
   3.705 + 
   3.706 +subsection{*The First Isomorphism Theorem*}
   3.707  
   3.708 -subsection{*Quotienting by the Kernel of a Homomorphism*}
   3.709 +text{*The quotient by the kernel of a homomorphism is isomorphic to the 
   3.710 +  range of that homomorphism.*}
   3.711  
   3.712  constdefs
   3.713 -  kernel :: "('a, 'm) monoid_scheme => ('b, 'n) monoid_scheme => 
   3.714 -             ('a => 'b) => 'a set" 
   3.715 +  kernel :: "('a, 'm) monoid_scheme \<Rightarrow> ('b, 'n) monoid_scheme \<Rightarrow> 
   3.716 +             ('a \<Rightarrow> 'b) \<Rightarrow> 'a set" 
   3.717      --{*the kernel of a homomorphism*}
   3.718 -  "kernel G H h == {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}";
   3.719 +  "kernel G H h \<equiv> {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}";
   3.720  
   3.721  lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
   3.722 -apply (rule group.subgroupI) 
   3.723 +apply (rule subgroup.intro) 
   3.724  apply (auto simp add: kernel_def group.intro prems) 
   3.725  done
   3.726  
   3.727  text{*The kernel of a homomorphism is a normal subgroup*}
   3.728 -lemma (in group_hom) normal_kernel: "(kernel G H h) <| G"
   3.729 +lemma (in group_hom) normal_kernel: "(kernel G H h) \<lhd> G"
   3.730  apply (simp add: group.normal_inv_iff subgroup_kernel group.intro prems)
   3.731  apply (simp add: kernel_def)  
   3.732  done
   3.733 @@ -538,9 +566,9 @@
   3.734    from X
   3.735    obtain g where "g \<in> carrier G" 
   3.736               and "X = kernel G H h #> g"
   3.737 -    by (auto simp add: FactGroup_def rcosets_def)
   3.738 +    by (auto simp add: FactGroup_def RCOSETS_def)
   3.739    thus ?thesis 
   3.740 -   by (force simp add: kernel_def r_coset_def image_def intro: hom_one)
   3.741 +   by (auto simp add: kernel_def r_coset_def image_def intro: hom_one)
   3.742  qed
   3.743  
   3.744  
   3.745 @@ -551,13 +579,14 @@
   3.746    from X
   3.747    obtain g where g: "g \<in> carrier G" 
   3.748               and "X = kernel G H h #> g"
   3.749 -    by (auto simp add: FactGroup_def rcosets_def)
   3.750 -  hence "h ` X = {h g}" by (force simp add: kernel_def r_coset_def image_def g)
   3.751 +    by (auto simp add: FactGroup_def RCOSETS_def)
   3.752 +  hence "h ` X = {h g}" by (auto simp add: kernel_def r_coset_def image_def g)
   3.753    thus ?thesis by (auto simp add: g)
   3.754  qed
   3.755  
   3.756  lemma (in group_hom) FactGroup_hom:
   3.757 -     "(%X. contents (h`X)) \<in> hom (G Mod (kernel G H h)) H"
   3.758 +     "(\<lambda>X. contents (h`X)) \<in> hom (G Mod (kernel G H h)) H"
   3.759 +apply (simp add: hom_def FactGroup_contents_mem  normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)  
   3.760  proof (simp add: hom_def funcsetI FactGroup_contents_mem, intro ballI) 
   3.761    fix X and X'
   3.762    assume X:  "X  \<in> carrier (G Mod kernel G H h)"
   3.763 @@ -566,7 +595,7 @@
   3.764    obtain g and g'
   3.765             where "g \<in> carrier G" and "g' \<in> carrier G" 
   3.766               and "X = kernel G H h #> g" and "X' = kernel G H h #> g'"
   3.767 -    by (auto simp add: FactGroup_def rcosets_def)
   3.768 +    by (auto simp add: FactGroup_def RCOSETS_def)
   3.769    hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'" 
   3.770      and Xsub: "X \<subseteq> carrier G" and X'sub: "X' \<subseteq> carrier G"
   3.771      by (force simp add: kernel_def r_coset_def image_def)+
   3.772 @@ -578,10 +607,11 @@
   3.773      by (simp add: all image_eq_UN FactGroup_nonempty X X')  
   3.774  qed
   3.775  
   3.776 +
   3.777  text{*Lemma for the following injectivity result*}
   3.778  lemma (in group_hom) FactGroup_subset:
   3.779 -     "[|g \<in> carrier G; g' \<in> carrier G; h g = h g'|]
   3.780 -      ==>  kernel G H h #> g \<subseteq> kernel G H h #> g'"
   3.781 +     "\<lbrakk>g \<in> carrier G; g' \<in> carrier G; h g = h g'\<rbrakk>
   3.782 +      \<Longrightarrow>  kernel G H h #> g \<subseteq> kernel G H h #> g'"
   3.783  apply (clarsimp simp add: kernel_def r_coset_def image_def);
   3.784  apply (rename_tac y)  
   3.785  apply (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI) 
   3.786 @@ -598,7 +628,7 @@
   3.787    obtain g and g'
   3.788             where gX: "g \<in> carrier G"  "g' \<in> carrier G" 
   3.789                "X = kernel G H h #> g" "X' = kernel G H h #> g'"
   3.790 -    by (auto simp add: FactGroup_def rcosets_def)
   3.791 +    by (auto simp add: FactGroup_def RCOSETS_def)
   3.792    hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'" 
   3.793      by (force simp add: kernel_def r_coset_def image_def)+
   3.794    assume "contents (h ` X) = contents (h ` X')"
   3.795 @@ -624,7 +654,7 @@
   3.796      hence "(\<Union>\<^bsub>x\<in>kernel G H h #> g\<^esub> {h x}) = {y}" 
   3.797        by (auto simp add: y kernel_def r_coset_def) 
   3.798      with g show "y \<in> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)" 
   3.799 -      by (auto intro!: bexI simp add: FactGroup_def rcosets_def image_eq_UN)
   3.800 +      by (auto intro!: bexI simp add: FactGroup_def RCOSETS_def image_eq_UN)
   3.801    qed
   3.802  qed
   3.803  
   3.804 @@ -633,8 +663,9 @@
   3.805   quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
   3.806  theorem (in group_hom) FactGroup_iso:
   3.807    "h ` carrier G = carrier H
   3.808 -   \<Longrightarrow> (%X. contents (h`X)) \<in> (G Mod (kernel G H h)) \<cong> H"
   3.809 +   \<Longrightarrow> (\<lambda>X. contents (h`X)) \<in> (G Mod (kernel G H h)) \<cong> H"
   3.810  by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def 
   3.811                FactGroup_onto) 
   3.812  
   3.813 +
   3.814  end
     4.1 --- a/src/HOL/Algebra/Group.thy	Thu Jun 17 14:27:01 2004 +0200
     4.2 +++ b/src/HOL/Algebra/Group.thy	Thu Jun 17 17:18:30 2004 +0200
     4.3 @@ -11,21 +11,17 @@
     4.4  theory Group = FuncSet + Lattice:
     4.5  
     4.6  
     4.7 -section {* From Magmas to Groups *}
     4.8 +section {* Monoids and Groups *}
     4.9  
    4.10  text {*
    4.11 -  Definitions follow \cite{Jacobson:1985}; with the exception of
    4.12 -  \emph{magma} which, following Bourbaki, is a set together with a
    4.13 -  binary, closed operation.
    4.14 +  Definitions follow \cite{Jacobson:1985}.
    4.15  *}
    4.16  
    4.17  subsection {* Definitions *}
    4.18  
    4.19 -record 'a semigroup = "'a partial_object" +
    4.20 -  mult :: "['a, 'a] => 'a" (infixl "\<otimes>\<index>" 70)
    4.21 -
    4.22 -record 'a monoid = "'a semigroup" +
    4.23 -  one :: 'a ("\<one>\<index>")
    4.24 +record 'a monoid =  "'a partial_object" +
    4.25 +  mult    :: "['a, 'a] \<Rightarrow> 'a" (infixl "\<otimes>\<index>" 70)
    4.26 +  one     :: 'a ("\<one>\<index>")
    4.27  
    4.28  constdefs (structure G)
    4.29    m_inv :: "('a, 'b) monoid_scheme => 'a => 'a" ("inv\<index> _" [81] 80)
    4.30 @@ -33,7 +29,7 @@
    4.31  
    4.32    Units :: "_ => 'a set"
    4.33    --{*The set of invertible elements*}
    4.34 -  "Units G == {y. y \<in> carrier G & (EX x : carrier G. x \<otimes> y = \<one> & y \<otimes> x = \<one>)}"
    4.35 +  "Units G == {y. y \<in> carrier G & (\<exists>x \<in> carrier G. x \<otimes> y = \<one> & y \<otimes> x = \<one>)}"
    4.36  
    4.37  consts
    4.38    pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75)
    4.39 @@ -44,19 +40,15 @@
    4.40      let p = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a)
    4.41      in if neg z then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z)"
    4.42  
    4.43 -locale magma = struct G +
    4.44 +locale monoid = struct G +
    4.45    assumes m_closed [intro, simp]:
    4.46 -    "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
    4.47 -
    4.48 -locale semigroup = magma +
    4.49 -  assumes m_assoc:
    4.50 -    "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    4.51 -    (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
    4.52 -
    4.53 -locale monoid = semigroup +
    4.54 -  assumes one_closed [intro, simp]: "\<one> \<in> carrier G"
    4.55 -    and l_one [simp]: "x \<in> carrier G ==> \<one> \<otimes> x = x"
    4.56 -    and r_one [simp]: "x \<in> carrier G ==> x \<otimes> \<one> = x"
    4.57 +         "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> carrier G"
    4.58 +      and m_assoc:
    4.59 +         "\<lbrakk>x \<in> carrier G; y \<in> carrier G; z \<in> carrier G\<rbrakk> 
    4.60 +          \<Longrightarrow> (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
    4.61 +      and one_closed [intro, simp]: "\<one> \<in> carrier G"
    4.62 +      and l_one [simp]: "x \<in> carrier G \<Longrightarrow> \<one> \<otimes> x = x"
    4.63 +      and r_one [simp]: "x \<in> carrier G \<Longrightarrow> x \<otimes> \<one> = x"
    4.64  
    4.65  lemma monoidI:
    4.66    includes struct G
    4.67 @@ -69,9 +61,7 @@
    4.68      and l_one: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x"
    4.69      and r_one: "!!x. x \<in> carrier G ==> x \<otimes> \<one> = x"
    4.70    shows "monoid G"
    4.71 -  by (fast intro!: monoid.intro magma.intro semigroup_axioms.intro
    4.72 -    semigroup.intro monoid_axioms.intro
    4.73 -    intro: prems)
    4.74 +  by (fast intro!: monoid.intro intro: prems)
    4.75  
    4.76  lemma (in monoid) Units_closed [dest]:
    4.77    "x \<in> Units G ==> x \<in> carrier G"
    4.78 @@ -210,7 +200,7 @@
    4.79        "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    4.80        (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
    4.81      and l_one [simp]: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x"
    4.82 -    and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. y \<otimes> x = \<one>"
    4.83 +    and l_inv_ex: "!!x. x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>"
    4.84    shows "group G"
    4.85  proof -
    4.86    have l_cancel [simp]:
    4.87 @@ -243,7 +233,7 @@
    4.88      with x xG show "x \<otimes> \<one> = x" by simp
    4.89    qed
    4.90    have inv_ex:
    4.91 -    "!!x. x \<in> carrier G ==> EX y : carrier G. y \<otimes> x = \<one> & x \<otimes> y = \<one>"
    4.92 +    "!!x. x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one> & x \<otimes> y = \<one>"
    4.93    proof -
    4.94      fix x
    4.95      assume x: "x \<in> carrier G"
    4.96 @@ -253,20 +243,19 @@
    4.97        by (simp add: m_assoc [symmetric] l_inv r_one)
    4.98      with x y have r_inv: "x \<otimes> y = \<one>"
    4.99        by simp
   4.100 -    from x y show "EX y : carrier G. y \<otimes> x = \<one> & x \<otimes> y = \<one>"
   4.101 +    from x y show "\<exists>y \<in> carrier G. y \<otimes> x = \<one> & x \<otimes> y = \<one>"
   4.102        by (fast intro: l_inv r_inv)
   4.103    qed
   4.104    then have carrier_subset_Units: "carrier G <= Units G"
   4.105      by (unfold Units_def) fast
   4.106    show ?thesis
   4.107 -    by (fast intro!: group.intro magma.intro semigroup_axioms.intro
   4.108 -      semigroup.intro monoid_axioms.intro group_axioms.intro
   4.109 +    by (fast intro!: group.intro monoid.intro group_axioms.intro
   4.110        carrier_subset_Units intro: prems r_one)
   4.111  qed
   4.112  
   4.113  lemma (in monoid) monoid_groupI:
   4.114    assumes l_inv_ex:
   4.115 -    "!!x. x \<in> carrier G ==> EX y : carrier G. y \<otimes> x = \<one>"
   4.116 +    "!!x. x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>"
   4.117    shows "group G"
   4.118    by (rule groupI) (auto intro: m_assoc l_inv_ex)
   4.119  
   4.120 @@ -282,7 +271,7 @@
   4.121    "x \<in> carrier G ==> inv x \<in> carrier G"
   4.122    using Units_inv_closed by simp
   4.123  
   4.124 -lemma (in group) l_inv:
   4.125 +lemma (in group) l_inv [simp]:
   4.126    "x \<in> carrier G ==> inv x \<otimes> x = \<one>"
   4.127    using Units_l_inv by simp
   4.128  
   4.129 @@ -293,7 +282,7 @@
   4.130     (x \<otimes> y = x \<otimes> z) = (y = z)"
   4.131    using Units_l_inv by simp
   4.132  
   4.133 -lemma (in group) r_inv:
   4.134 +lemma (in group) r_inv [simp]:
   4.135    "x \<in> carrier G ==> x \<otimes> inv x = \<one>"
   4.136  proof -
   4.137    assume x: "x \<in> carrier G"
   4.138 @@ -309,8 +298,8 @@
   4.139    assume eq: "y \<otimes> x = z \<otimes> x"
   4.140      and G: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
   4.141    then have "y \<otimes> (x \<otimes> inv x) = z \<otimes> (x \<otimes> inv x)"
   4.142 -    by (simp add: m_assoc [symmetric])
   4.143 -  with G show "y = z" by (simp add: r_inv)
   4.144 +    by (simp add: m_assoc [symmetric] del: r_inv)
   4.145 +  with G show "y = z" by simp
   4.146  next
   4.147    assume eq: "y = z"
   4.148      and G: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
   4.149 @@ -320,8 +309,8 @@
   4.150  lemma (in group) inv_one [simp]:
   4.151    "inv \<one> = \<one>"
   4.152  proof -
   4.153 -  have "inv \<one> = \<one> \<otimes> (inv \<one>)" by simp
   4.154 -  moreover have "... = \<one>" by (simp add: r_inv)
   4.155 +  have "inv \<one> = \<one> \<otimes> (inv \<one>)" by (simp del: r_inv)
   4.156 +  moreover have "... = \<one>" by simp
   4.157    finally show ?thesis .
   4.158  qed
   4.159  
   4.160 @@ -338,8 +327,8 @@
   4.161  proof -
   4.162    assume G: "x \<in> carrier G"  "y \<in> carrier G"
   4.163    then have "inv (x \<otimes> y) \<otimes> (x \<otimes> y) = (inv y \<otimes> inv x) \<otimes> (x \<otimes> y)"
   4.164 -    by (simp add: m_assoc l_inv) (simp add: m_assoc [symmetric] l_inv)
   4.165 -  with G show ?thesis by simp
   4.166 +    by (simp add: m_assoc l_inv) (simp add: m_assoc [symmetric])
   4.167 +  with G show ?thesis by (simp del: l_inv)
   4.168  qed
   4.169  
   4.170  lemma (in group) inv_comm:
   4.171 @@ -368,54 +357,28 @@
   4.172    "\<one> (^) (z::int) = \<one>"
   4.173    by (simp add: int_pow_def2)
   4.174  
   4.175 -subsection {* Substructures *}
   4.176 -
   4.177 -locale submagma = var H + struct G +
   4.178 -  assumes subset [intro, simp]: "H \<subseteq> carrier G"
   4.179 -    and m_closed [intro, simp]: "[| x \<in> H; y \<in> H |] ==> x \<otimes> y \<in> H"
   4.180 -
   4.181 -declare (in submagma) magma.intro [intro] semigroup.intro [intro]
   4.182 -  semigroup_axioms.intro [intro]
   4.183 -
   4.184 -lemma submagma_imp_subset:
   4.185 -  "submagma H G ==> H \<subseteq> carrier G"
   4.186 -  by (rule submagma.subset)
   4.187 -
   4.188 -lemma (in submagma) subsetD [dest, simp]:
   4.189 -  "x \<in> H ==> x \<in> carrier G"
   4.190 -  using subset by blast
   4.191 +subsection {* Subgroups *}
   4.192  
   4.193 -lemma (in submagma) magmaI [intro]:
   4.194 -  includes magma G
   4.195 -  shows "magma (G(| carrier := H |))"
   4.196 -  by rule simp
   4.197 -
   4.198 -lemma (in submagma) semigroup_axiomsI [intro]:
   4.199 -  includes semigroup G
   4.200 -  shows "semigroup_axioms (G(| carrier := H |))"
   4.201 -    by rule (simp add: m_assoc)
   4.202 -
   4.203 -lemma (in submagma) semigroupI [intro]:
   4.204 -  includes semigroup G
   4.205 -  shows "semigroup (G(| carrier := H |))"
   4.206 -  using prems by fast
   4.207 -
   4.208 -
   4.209 -locale subgroup = submagma H G +
   4.210 -  assumes one_closed [intro, simp]: "\<one> \<in> H"
   4.211 -    and m_inv_closed [intro, simp]: "x \<in> H ==> inv x \<in> H"
   4.212 +locale subgroup = var H + struct G + 
   4.213 +  assumes subset: "H \<subseteq> carrier G"
   4.214 +    and m_closed [intro, simp]: "\<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> H"
   4.215 +    and  one_closed [simp]: "\<one> \<in> H"
   4.216 +    and m_inv_closed [intro,simp]: "x \<in> H \<Longrightarrow> inv x \<in> H"
   4.217  
   4.218  declare (in subgroup) group.intro [intro]
   4.219  
   4.220 -lemma (in subgroup) group_axiomsI [intro]:
   4.221 -  includes group G
   4.222 -  shows "group_axioms (G(| carrier := H |))"
   4.223 -  by (rule group_axioms.intro) (auto intro: l_inv r_inv simp add: Units_def)
   4.224 +lemma (in subgroup) mem_carrier [simp]:
   4.225 +  "x \<in> H \<Longrightarrow> x \<in> carrier G"
   4.226 +  using subset by blast
   4.227  
   4.228 -lemma (in subgroup) groupI [intro]:
   4.229 +lemma subgroup_imp_subset:
   4.230 +  "subgroup H G \<Longrightarrow> H \<subseteq> carrier G"
   4.231 +  by (rule subgroup.subset)
   4.232 +
   4.233 +lemma (in subgroup) subgroup_is_group [intro]:
   4.234    includes group G
   4.235 -  shows "group (G(| carrier := H |))"
   4.236 -  by (rule groupI) (auto intro: m_assoc l_inv)
   4.237 +  shows "group (G\<lparr>carrier := H\<rparr>)" 
   4.238 +  by (rule groupI) (auto intro: m_assoc l_inv mem_carrier)
   4.239  
   4.240  text {*
   4.241    Since @{term H} is nonempty, it contains some element @{term x}.  Since
   4.242 @@ -432,31 +395,13 @@
   4.243  
   4.244  lemma (in group) subgroupI:
   4.245    assumes subset: "H \<subseteq> carrier G" and non_empty: "H \<noteq> {}"
   4.246 -    and inv: "!!a. a \<in> H ==> inv a \<in> H"
   4.247 -    and mult: "!!a b. [|a \<in> H; b \<in> H|] ==> a \<otimes> b \<in> H"
   4.248 +    and inv: "!!a. a \<in> H \<Longrightarrow> inv a \<in> H"
   4.249 +    and mult: "!!a b. \<lbrakk>a \<in> H; b \<in> H\<rbrakk> \<Longrightarrow> a \<otimes> b \<in> H"
   4.250    shows "subgroup H G"
   4.251 -proof (rule subgroup.intro)
   4.252 -  from subset and mult show "submagma H G" by (rule submagma.intro)
   4.253 -next
   4.254 -  have "\<one> \<in> H" by (rule one_in_subset) (auto simp only: prems)
   4.255 -  with inv show "subgroup_axioms H G"
   4.256 -    by (intro subgroup_axioms.intro) simp_all
   4.257 +proof (simp add: subgroup_def prems)
   4.258 +  show "\<one> \<in> H" by (rule one_in_subset) (auto simp only: prems)
   4.259  qed
   4.260  
   4.261 -text {*
   4.262 -  Repeat facts of submagmas for subgroups.  Necessary???
   4.263 -*}
   4.264 -
   4.265 -lemma (in subgroup) subset:
   4.266 -  "H \<subseteq> carrier G"
   4.267 -  ..
   4.268 -
   4.269 -lemma (in subgroup) m_closed:
   4.270 -  "[| x \<in> H; y \<in> H |] ==> x \<otimes> y \<in> H"
   4.271 -  ..
   4.272 -
   4.273 -declare magma.m_closed [simp]
   4.274 -
   4.275  declare monoid.one_closed [iff] group.inv_closed [simp]
   4.276    monoid.l_one [simp] monoid.r_one [simp] group.inv_inv [simp]
   4.277  
   4.278 @@ -467,11 +412,9 @@
   4.279  lemma (in subgroup) finite_imp_card_positive:
   4.280    "finite (carrier G) ==> 0 < card H"
   4.281  proof (rule classical)
   4.282 -  have sub: "subgroup H G" using prems by (rule subgroup.intro)
   4.283 -  assume fin: "finite (carrier G)"
   4.284 -    and zero: "~ 0 < card H"
   4.285 -  then have "finite H" by (blast intro: finite_subset dest: subset)
   4.286 -  with zero sub have "subgroup {} G" by simp
   4.287 +  assume "finite (carrier G)" "~ 0 < card H"
   4.288 +  then have "finite H" by (blast intro: finite_subset [OF subset])
   4.289 +  with prems have "subgroup {} G" by simp
   4.290    with subgroup_nonempty show ?thesis by contradiction
   4.291  qed
   4.292  
   4.293 @@ -482,83 +425,67 @@
   4.294  
   4.295  subsection {* Direct Products *}
   4.296  
   4.297 -constdefs (structure G and H)
   4.298 -  DirProdSemigroup :: "_ => _ => ('a \<times> 'b) semigroup"  (infixr "\<times>\<^sub>s" 80)
   4.299 -  "G \<times>\<^sub>s H == (| carrier = carrier G \<times> carrier H,
   4.300 -    mult = (%(g, h) (g', h'). (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')) |)"
   4.301 -
   4.302 -  DirProdGroup :: "_ => _ => ('a \<times> 'b) monoid"  (infixr "\<times>\<^sub>g" 80)
   4.303 -  "G \<times>\<^sub>g H == semigroup.extend (G \<times>\<^sub>s H) (| one = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>) |)"
   4.304 -
   4.305 -lemma DirProdSemigroup_magma:
   4.306 -  includes magma G + magma H
   4.307 -  shows "magma (G \<times>\<^sub>s H)"
   4.308 -  by (rule magma.intro) (auto simp add: DirProdSemigroup_def)
   4.309 +constdefs
   4.310 +  DirProd :: "_ \<Rightarrow> _ \<Rightarrow> ('a \<times> 'b) monoid"  (infixr "\<times>\<times>" 80)
   4.311 +  "G \<times>\<times> H \<equiv> \<lparr>carrier = carrier G \<times> carrier H,
   4.312 +                mult = (\<lambda>(g, h) (g', h'). (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')),
   4.313 +                one = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)\<rparr>"
   4.314  
   4.315 -lemma DirProdSemigroup_semigroup_axioms:
   4.316 -  includes semigroup G + semigroup H
   4.317 -  shows "semigroup_axioms (G \<times>\<^sub>s H)"
   4.318 -  by (rule semigroup_axioms.intro)
   4.319 -    (auto simp add: DirProdSemigroup_def G.m_assoc H.m_assoc)
   4.320 +lemma DirProd_monoid:
   4.321 +  includes monoid G + monoid H
   4.322 +  shows "monoid (G \<times>\<times> H)"
   4.323 +proof -
   4.324 +  from prems
   4.325 +  show ?thesis by (unfold monoid_def DirProd_def, auto) 
   4.326 +qed
   4.327  
   4.328 -lemma DirProdSemigroup_semigroup:
   4.329 -  includes semigroup G + semigroup H
   4.330 -  shows "semigroup (G \<times>\<^sub>s H)"
   4.331 -  using prems
   4.332 -  by (fast intro: semigroup.intro
   4.333 -    DirProdSemigroup_magma DirProdSemigroup_semigroup_axioms)
   4.334 -
   4.335 -lemma DirProdGroup_magma:
   4.336 -  includes magma G + magma H
   4.337 -  shows "magma (G \<times>\<^sub>g H)"
   4.338 -  by (rule magma.intro)
   4.339 -    (auto simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
   4.340  
   4.341 -lemma DirProdGroup_semigroup_axioms:
   4.342 -  includes semigroup G + semigroup H
   4.343 -  shows "semigroup_axioms (G \<times>\<^sub>g H)"
   4.344 -  by (rule semigroup_axioms.intro)
   4.345 -    (auto simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs
   4.346 -      G.m_assoc H.m_assoc)
   4.347 -
   4.348 -lemma DirProdGroup_semigroup:
   4.349 -  includes semigroup G + semigroup H
   4.350 -  shows "semigroup (G \<times>\<^sub>g H)"
   4.351 -  using prems
   4.352 -  by (fast intro: semigroup.intro
   4.353 -    DirProdGroup_magma DirProdGroup_semigroup_axioms)
   4.354 -
   4.355 -text {* \dots\ and further lemmas for group \dots *}
   4.356 -
   4.357 -lemma DirProdGroup_group:
   4.358 +text{*Does not use the previous result because it's easier just to use auto.*}
   4.359 +lemma DirProd_group:
   4.360    includes group G + group H
   4.361 -  shows "group (G \<times>\<^sub>g H)"
   4.362 +  shows "group (G \<times>\<times> H)"
   4.363    by (rule groupI)
   4.364 -    (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
   4.365 -      simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
   4.366 +     (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
   4.367 +           simp add: DirProd_def)
   4.368  
   4.369 -lemma carrier_DirProdGroup [simp]:
   4.370 -     "carrier (G \<times>\<^sub>g H) = carrier G \<times> carrier H"
   4.371 -  by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
   4.372 +lemma carrier_DirProd [simp]:
   4.373 +     "carrier (G \<times>\<times> H) = carrier G \<times> carrier H"
   4.374 +  by (simp add: DirProd_def)
   4.375  
   4.376 -lemma one_DirProdGroup [simp]:
   4.377 -     "\<one>\<^bsub>(G \<times>\<^sub>g H)\<^esub> = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)"
   4.378 -  by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
   4.379 +lemma one_DirProd [simp]:
   4.380 +     "\<one>\<^bsub>G \<times>\<times> H\<^esub> = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)"
   4.381 +  by (simp add: DirProd_def)
   4.382  
   4.383 -lemma mult_DirProdGroup [simp]:
   4.384 -     "(g, h) \<otimes>\<^bsub>(G \<times>\<^sub>g H)\<^esub> (g', h') = (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')"
   4.385 -  by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
   4.386 +lemma mult_DirProd [simp]:
   4.387 +     "(g, h) \<otimes>\<^bsub>(G \<times>\<times> H)\<^esub> (g', h') = (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')"
   4.388 +  by (simp add: DirProd_def)
   4.389  
   4.390 -lemma inv_DirProdGroup [simp]:
   4.391 +lemma inv_DirProd [simp]:
   4.392    includes group G + group H
   4.393    assumes g: "g \<in> carrier G"
   4.394        and h: "h \<in> carrier H"
   4.395 -  shows "m_inv (G \<times>\<^sub>g H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
   4.396 -  apply (rule group.inv_equality [OF DirProdGroup_group])
   4.397 +  shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
   4.398 +  apply (rule group.inv_equality [OF DirProd_group])
   4.399    apply (simp_all add: prems group_def group.l_inv)
   4.400    done
   4.401  
   4.402 -subsection {* Isomorphisms *}
   4.403 +text{*This alternative proof of the previous result demonstrates instantiate.
   4.404 +   It uses @{text Prod.inv_equality} (available after instantiation) instead of
   4.405 +   @{text "group.inv_equality [OF DirProd_group]"}. *}
   4.406 +lemma
   4.407 +  includes group G + group H
   4.408 +  assumes g: "g \<in> carrier G"
   4.409 +      and h: "h \<in> carrier H"
   4.410 +  shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
   4.411 +proof -
   4.412 +  have "group (G \<times>\<times> H)"
   4.413 +    by (blast intro: DirProd_group group.intro prems)
   4.414 +  then instantiate Prod: group
   4.415 +  show ?thesis by (simp add: Prod.inv_equality g h)
   4.416 +qed
   4.417 +  
   4.418 +
   4.419 +subsection {* Homomorphisms and Isomorphisms *}
   4.420  
   4.421  constdefs (structure G and H)
   4.422    hom :: "_ => _ => ('a => 'b) set"
   4.423 @@ -566,16 +493,6 @@
   4.424      {h. h \<in> carrier G -> carrier H &
   4.425        (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y)}"
   4.426  
   4.427 -lemma (in semigroup) hom:
   4.428 -     "semigroup (| carrier = hom G G, mult = op o |)"
   4.429 -proof (rule semigroup.intro)
   4.430 -  show "magma (| carrier = hom G G, mult = op o |)"
   4.431 -    by (rule magma.intro) (simp add: Pi_def hom_def)
   4.432 -next
   4.433 -  show "semigroup_axioms (| carrier = hom G G, mult = op o |)"
   4.434 -    by (rule semigroup_axioms.intro) (simp add: o_assoc)
   4.435 -qed
   4.436 -
   4.437  lemma hom_mult:
   4.438    "[| h \<in> hom G H; x \<in> carrier G; y \<in> carrier G |]
   4.439     ==> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
   4.440 @@ -613,15 +530,17 @@
   4.441       "[|h \<in> G \<cong> H; i \<in> H \<cong> I|] ==> (compose (carrier G) i h) \<in> G \<cong> I"
   4.442  by (auto simp add: iso_def hom_compose bij_betw_compose)
   4.443  
   4.444 -lemma DirProdGroup_commute_iso:
   4.445 -  shows "(%(x,y). (y,x)) \<in> (G \<times>\<^sub>g H) \<cong> (H \<times>\<^sub>g G)"
   4.446 +lemma DirProd_commute_iso:
   4.447 +  shows "(\<lambda>(x,y). (y,x)) \<in> (G \<times>\<times> H) \<cong> (H \<times>\<times> G)"
   4.448  by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def) 
   4.449  
   4.450 -lemma DirProdGroup_assoc_iso:
   4.451 -  shows "(%(x,y,z). (x,(y,z))) \<in> (G \<times>\<^sub>g H \<times>\<^sub>g I) \<cong> (G \<times>\<^sub>g (H \<times>\<^sub>g I))"
   4.452 +lemma DirProd_assoc_iso:
   4.453 +  shows "(\<lambda>(x,y,z). (x,(y,z))) \<in> (G \<times>\<times> H \<times>\<times> I) \<cong> (G \<times>\<times> (H \<times>\<times> I))"
   4.454  by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def) 
   4.455  
   4.456  
   4.457 +text{*Basis for homomorphism proofs: we assume two groups @{term G} and
   4.458 +  @term{H}, with a homomorphism @{term h} between them*}
   4.459  locale group_hom = group G + group H + var h +
   4.460    assumes homh: "h \<in> hom G H"
   4.461    notes hom_mult [simp] = hom_mult [OF homh]
   4.462 @@ -648,11 +567,11 @@
   4.463  proof -
   4.464    assume x: "x \<in> carrier G"
   4.465    then have "h x \<otimes>\<^bsub>H\<^esub> h (inv x) = \<one>\<^bsub>H\<^esub>"
   4.466 -    by (simp add: hom_mult [symmetric] G.r_inv del: hom_mult)
   4.467 +    by (simp add: hom_mult [symmetric] del: hom_mult)
   4.468    also from x have "... = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)"
   4.469 -    by (simp add: hom_mult [symmetric] H.r_inv del: hom_mult)
   4.470 +    by (simp add: hom_mult [symmetric] del: hom_mult)
   4.471    finally have "h x \<otimes>\<^bsub>H\<^esub> h (inv x) = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)" .
   4.472 -  with x show ?thesis by simp
   4.473 +  with x show ?thesis by (simp del: H.r_inv)
   4.474  qed
   4.475  
   4.476  subsection {* Commutative Structures *}
   4.477 @@ -665,11 +584,11 @@
   4.478  
   4.479  subsection {* Definition *}
   4.480  
   4.481 -locale comm_semigroup = semigroup +
   4.482 -  assumes m_comm: "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
   4.483 +locale comm_monoid = monoid +
   4.484 +  assumes m_comm: "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> x \<otimes> y = y \<otimes> x"
   4.485  
   4.486 -lemma (in comm_semigroup) m_lcomm:
   4.487 -  "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   4.488 +lemma (in comm_monoid) m_lcomm:
   4.489 +  "\<lbrakk>x \<in> carrier G; y \<in> carrier G; z \<in> carrier G\<rbrakk> \<Longrightarrow>
   4.490     x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)"
   4.491  proof -
   4.492    assume xyz: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
   4.493 @@ -679,9 +598,7 @@
   4.494    finally show ?thesis .
   4.495  qed
   4.496  
   4.497 -lemmas (in comm_semigroup) m_ac = m_assoc m_comm m_lcomm
   4.498 -
   4.499 -locale comm_monoid = comm_semigroup + monoid
   4.500 +lemmas (in comm_monoid) m_ac = m_assoc m_comm m_lcomm
   4.501  
   4.502  lemma comm_monoidI:
   4.503    includes struct G
   4.504 @@ -696,15 +613,15 @@
   4.505        "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
   4.506    shows "comm_monoid G"
   4.507    using l_one
   4.508 -  by (auto intro!: comm_monoid.intro magma.intro semigroup_axioms.intro
   4.509 -    comm_semigroup_axioms.intro monoid_axioms.intro
   4.510 -    intro: prems simp: m_closed one_closed m_comm)
   4.511 +    by (auto intro!: comm_monoid.intro comm_monoid_axioms.intro monoid.intro 
   4.512 +             intro: prems simp: m_closed one_closed m_comm)
   4.513  
   4.514  lemma (in monoid) monoid_comm_monoidI:
   4.515    assumes m_comm:
   4.516        "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
   4.517    shows "comm_monoid G"
   4.518    by (rule comm_monoidI) (auto intro: m_assoc m_comm)
   4.519 +
   4.520  (*lemma (in comm_monoid) r_one [simp]:
   4.521    "x \<in> carrier G ==> x \<otimes> \<one> = x"
   4.522  proof -
   4.523 @@ -713,6 +630,7 @@
   4.524    also from G have "... = x" by simp
   4.525    finally show ?thesis .
   4.526  qed*)
   4.527 +
   4.528  lemma (in comm_monoid) nat_pow_distr:
   4.529    "[| x \<in> carrier G; y \<in> carrier G |] ==>
   4.530    (x \<otimes> y) (^) (n::nat) = x (^) n \<otimes> y (^) n"
   4.531 @@ -724,7 +642,7 @@
   4.532    assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
   4.533        x \<otimes> y = y \<otimes> x"
   4.534    shows "comm_group G"
   4.535 -  by (fast intro: comm_group.intro comm_semigroup_axioms.intro
   4.536 +  by (fast intro: comm_group.intro comm_monoid_axioms.intro
   4.537                    is_group prems)
   4.538  
   4.539  lemma comm_groupI:
   4.540 @@ -738,7 +656,7 @@
   4.541      and m_comm:
   4.542        "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
   4.543      and l_one: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x"
   4.544 -    and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. y \<otimes> x = \<one>"
   4.545 +    and l_inv_ex: "!!x. x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>"
   4.546    shows "comm_group G"
   4.547    by (fast intro: group.group_comm_groupI groupI prems)
   4.548  
   4.549 @@ -760,11 +678,11 @@
   4.550  
   4.551  lemma (in group) subgroup_imp_group:
   4.552    "subgroup H G ==> group (G(| carrier := H |))"
   4.553 -  using subgroup.groupI [OF _ group.intro] .
   4.554 +  using subgroup.subgroup_is_group [OF _ group.intro] .
   4.555  
   4.556  lemma (in group) is_monoid [intro, simp]:
   4.557    "monoid G"
   4.558 -  by (rule monoid.intro)
   4.559 +  by (auto intro: monoid.intro m_assoc) 
   4.560  
   4.561  lemma (in group) subgroup_inv_equality:
   4.562    "[| subgroup H G; x \<in> H |] ==> m_inv (G (| carrier := H |)) x = inv x"
   4.563 @@ -803,7 +721,7 @@
   4.564  next
   4.565    have "greatest ?L (carrier G) (carrier ?L)"
   4.566      by (unfold greatest_def) (simp add: subgroup.subset subgroup_self)
   4.567 -  then show "EX G. greatest ?L G (carrier ?L)" ..
   4.568 +  then show "\<exists>G. greatest ?L G (carrier ?L)" ..
   4.569  next
   4.570    fix A
   4.571    assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}"
   4.572 @@ -815,7 +733,6 @@
   4.573      fix H
   4.574      assume H: "H \<in> A"
   4.575      with L have subgroupH: "subgroup H G" by auto
   4.576 -    from subgroupH have submagmaH: "submagma H G" by (rule subgroup.axioms)
   4.577      from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H")
   4.578        by (rule subgroup_imp_group)
   4.579      from groupH have monoidH: "monoid ?H"
   4.580 @@ -831,7 +748,7 @@
   4.581    next
   4.582      show "?Int \<in> carrier ?L" by simp (rule Int_subgroup)
   4.583    qed
   4.584 -  then show "EX I. greatest ?L I (Lower ?L A)" ..
   4.585 +  then show "\<exists>I. greatest ?L I (Lower ?L A)" ..
   4.586  qed
   4.587  
   4.588  end
     5.1 --- a/src/HOL/Algebra/Sylow.thy	Thu Jun 17 14:27:01 2004 +0200
     5.2 +++ b/src/HOL/Algebra/Sylow.thy	Thu Jun 17 17:18:30 2004 +0200
     5.3 @@ -206,7 +206,7 @@
     5.4  
     5.5  lemma (in sylow_central) M1_cardeq_rcosetGM1g:
     5.6       "g \<in> carrier G ==> card(M1 #> g) = card(M1)"
     5.7 -by (simp (no_asm_simp) add: M1_subset_G card_cosets_equal setrcosI)
     5.8 +by (simp (no_asm_simp) add: M1_subset_G card_cosets_equal rcosetsI)
     5.9  
    5.10  lemma (in sylow_central) M1_RelM_rcosetGM1g:
    5.11       "g \<in> carrier G ==> (M1, M1 #> g) \<in> RelM"
    5.12 @@ -219,16 +219,14 @@
    5.13  done
    5.14  
    5.15  
    5.16 +subsection{*Equal Cardinalities of @{term M} and the Set of Cosets*}
    5.17  
    5.18 -subsection{*Equal Cardinalities of @{term M} and @{term "rcosets G H"}*}
    5.19 -
    5.20 -text{*Injections between @{term M} and @{term "rcosets G H"} show that
    5.21 +text{*Injections between @{term M} and @{term "rcosets\<^bsub>G\<^esub> H"} show that
    5.22   their cardinalities are equal.*}
    5.23  
    5.24  lemma ElemClassEquiv:
    5.25 -     "[| equiv A r; C\<in>A // r |] ==> \<forall>x \<in> C. \<forall>y \<in> C. (x,y)\<in>r"
    5.26 -apply (unfold equiv_def quotient_def sym_def trans_def, blast)
    5.27 -done
    5.28 +     "[| equiv A r; C \<in> A // r |] ==> \<forall>x \<in> C. \<forall>y \<in> C. (x,y)\<in>r"
    5.29 +by (unfold equiv_def quotient_def sym_def trans_def, blast)
    5.30  
    5.31  lemma (in sylow_central) M_elem_map:
    5.32       "M2 \<in> M ==> \<exists>g. g \<in> carrier G & M1 #> g = M2"
    5.33 @@ -243,16 +241,16 @@
    5.34  lemmas (in sylow_central) M_elem_map_eq =
    5.35          M_elem_map [THEN someI_ex, THEN conjunct2]
    5.36  
    5.37 -lemma (in sylow_central) M_funcset_setrcos_H:
    5.38 -     "(%x:M. H #> (SOME g. g \<in> carrier G & M1 #> g = x)) \<in> M \<rightarrow> rcosets G H"
    5.39 -apply (rule setrcosI [THEN restrictI])
    5.40 +lemma (in sylow_central) M_funcset_rcosets_H:
    5.41 +     "(%x:M. H #> (SOME g. g \<in> carrier G & M1 #> g = x)) \<in> M \<rightarrow> rcosets H"
    5.42 +apply (rule rcosetsI [THEN restrictI])
    5.43  apply (rule H_is_subgroup [THEN subgroup.subset])
    5.44  apply (erule M_elem_map_carrier)
    5.45  done
    5.46  
    5.47 -lemma (in sylow_central) inj_M_GmodH: "\<exists>f \<in> M\<rightarrow>rcosets G H. inj_on f M"
    5.48 +lemma (in sylow_central) inj_M_GmodH: "\<exists>f \<in> M\<rightarrow>rcosets H. inj_on f M"
    5.49  apply (rule bexI)
    5.50 -apply (rule_tac [2] M_funcset_setrcos_H)
    5.51 +apply (rule_tac [2] M_funcset_rcosets_H)
    5.52  apply (rule inj_onI, simp)
    5.53  apply (rule trans [OF _ M_elem_map_eq])
    5.54  prefer 2 apply assumption
    5.55 @@ -267,11 +265,11 @@
    5.56  done
    5.57  
    5.58  
    5.59 -(** the opposite injection **)
    5.60 +subsubsection{*The opposite injection*}
    5.61  
    5.62  lemma (in sylow_central) H_elem_map:
    5.63 -     "H1\<in>rcosets G H ==> \<exists>g. g \<in> carrier G & H #> g = H1"
    5.64 -by (auto simp add: setrcos_eq)
    5.65 +     "H1 \<in> rcosets H ==> \<exists>g. g \<in> carrier G & H #> g = H1"
    5.66 +by (auto simp add: RCOSETS_def)
    5.67  
    5.68  lemmas (in sylow_central) H_elem_map_carrier =
    5.69          H_elem_map [THEN someI_ex, THEN conjunct1]
    5.70 @@ -281,14 +279,13 @@
    5.71  
    5.72  
    5.73  lemma EquivElemClass:
    5.74 -     "[|equiv A r; M\<in>A // r; M1\<in>M; (M1, M2)\<in>r |] ==> M2\<in>M"
    5.75 -apply (unfold equiv_def quotient_def sym_def trans_def, blast)
    5.76 -done
    5.77 +     "[|equiv A r; M \<in> A//r; M1\<in>M; (M1,M2) \<in> r |] ==> M2 \<in> M"
    5.78 +by (unfold equiv_def quotient_def sym_def trans_def, blast)
    5.79 +
    5.80  
    5.81 -lemma (in sylow_central) setrcos_H_funcset_M:
    5.82 -     "(\<lambda>C \<in> rcosets G H. M1 #> (@g. g \<in> carrier G \<and> H #> g = C))
    5.83 -      \<in> rcosets G H \<rightarrow> M"
    5.84 -apply (simp add: setrcos_eq)
    5.85 +lemma (in sylow_central) rcosets_H_funcset_M:
    5.86 +  "(\<lambda>C \<in> rcosets H. M1 #> (@g. g \<in> carrier G \<and> H #> g = C)) \<in> rcosets H \<rightarrow> M"
    5.87 +apply (simp add: RCOSETS_def)
    5.88  apply (fast intro: someI2
    5.89              intro!: restrictI M1_in_M
    5.90                EquivElemClass [OF RelM_equiv M_in_quot _  M1_RelM_rcosetGM1g])
    5.91 @@ -296,9 +293,9 @@
    5.92  
    5.93  text{*close to a duplicate of @{text inj_M_GmodH}*}
    5.94  lemma (in sylow_central) inj_GmodH_M:
    5.95 -     "\<exists>g \<in> rcosets G H\<rightarrow>M. inj_on g (rcosets G H)"
    5.96 +     "\<exists>g \<in> rcosets H\<rightarrow>M. inj_on g (rcosets H)"
    5.97  apply (rule bexI)
    5.98 -apply (rule_tac [2] setrcos_H_funcset_M)
    5.99 +apply (rule_tac [2] rcosets_H_funcset_M)
   5.100  apply (rule inj_onI)
   5.101  apply (simp)
   5.102  apply (rule trans [OF _ H_elem_map_eq])
   5.103 @@ -323,10 +320,10 @@
   5.104  apply (rule calM_subset_PowG, blast)
   5.105  done
   5.106  
   5.107 -lemma (in sylow_central) cardMeqIndexH: "card(M) = card(rcosets G H)"
   5.108 +lemma (in sylow_central) cardMeqIndexH: "card(M) = card(rcosets H)"
   5.109  apply (insert inj_M_GmodH inj_GmodH_M)
   5.110  apply (blast intro: card_bij finite_M H_is_subgroup
   5.111 -             setrcos_subset_PowG [THEN finite_subset]
   5.112 +             rcosets_subset_PowG [THEN finite_subset]
   5.113               finite_Pow_iff [THEN iffD2])
   5.114  done
   5.115  
   5.116 @@ -373,3 +370,4 @@
   5.117  done
   5.118  
   5.119  end
   5.120 +
     6.1 --- a/src/HOL/Algebra/UnivPoly.thy	Thu Jun 17 14:27:01 2004 +0200
     6.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Thu Jun 17 17:18:30 2004 +0200
     6.3 @@ -402,11 +402,6 @@
     6.4      UP_cring)
     6.5  (* TODO: provide cring.is_monoid *)
     6.6  
     6.7 -lemma (in UP_cring) UP_comm_semigroup:
     6.8 -  "comm_semigroup P"
     6.9 -  by (fast intro!: cring.is_comm_monoid comm_monoid.axioms comm_semigroup.intro
    6.10 -    UP_cring)
    6.11 -
    6.12  lemma (in UP_cring) UP_comm_monoid:
    6.13    "comm_monoid P"
    6.14    by (fast intro!: cring.is_comm_monoid UP_cring)
    6.15 @@ -441,7 +436,7 @@
    6.16    monoid.nat_pow_pow [OF UP_monoid]
    6.17  
    6.18  lemmas (in UP_cring) UP_m_lcomm =
    6.19 -  comm_semigroup.m_lcomm [OF UP_comm_semigroup]
    6.20 +  comm_monoid.m_lcomm [OF UP_comm_monoid]
    6.21  
    6.22  lemmas (in UP_cring) UP_m_ac = UP_m_assoc UP_m_comm UP_m_lcomm
    6.23  
     7.1 --- a/src/HOL/Algebra/ringsimp.ML	Thu Jun 17 14:27:01 2004 +0200
     7.2 +++ b/src/HOL/Algebra/ringsimp.ML	Thu Jun 17 17:18:30 2004 +0200
     7.3 @@ -57,7 +57,7 @@
     7.4  
     7.5  fun ring_ord a =
     7.6    find_index_eq a ["CRing.ring.zero", "CRing.ring.add", "CRing.a_inv",
     7.7 -  "CRing.minus", "Group.monoid.one", "Group.semigroup.mult"];
     7.8 +  "CRing.minus", "Group.monoid.one", "Group.monoid.mult"];
     7.9  
    7.10  fun termless_ring (a, b) = (term_lpo ring_ord (a, b) = LESS);
    7.11  
    7.12 @@ -69,7 +69,7 @@
    7.13        | _ => [])
    7.14        handle TERM _ => [];
    7.15      fun comm_filter t = (case HOLogic.dest_Trueprop t of
    7.16 -        Const ("Group.comm_semigroup_axioms", _) $ Free (s, _) => [s]
    7.17 +        Const ("Group.comm_monoid_axioms", _) $ Free (s, _) => [s]
    7.18        | _ => [])
    7.19        handle TERM _ => [];
    7.20