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 +constdefs (structure G)
3.9 + r_coset :: "[_, 'a set, 'a] \<Rightarrow> 'a set" (infixl "#>\<index>" 60)
3.10 + "H #> a \<equiv> \<Union>h\<in>H. {h \<otimes> a}"
3.11
3.12 -constdefs (structure G)
3.13 - r_coset :: "[_, 'a set, 'a] => 'a set" (infixl "#>\<index>" 60)
3.14 - "H #> a == (% x. x \<otimes> a) ` H"
3.15 + l_coset :: "[_, 'a, 'a set] \<Rightarrow> 'a set" (infixl "<#\<index>" 60)
3.16 + "a <# H \<equiv> \<Union>h\<in>H. {a \<otimes> h}"
3.17
3.18 - l_coset :: "[_, 'a, 'a set] => 'a set" (infixl "<#\<index>" 60)
3.19 - "a <# H == (% x. a \<otimes> x) ` H"
3.20 + RCOSETS :: "[_, 'a set] \<Rightarrow> ('a set)set" ("rcosets\<index> _" [81] 80)
3.21 + "rcosets H \<equiv> \<Union>a\<in>carrier G. {H #> a}"
3.22
3.23 - rcosets :: "[_, 'a set] => ('a set)set"
3.24 - "rcosets G H == r_coset G H ` (carrier G)"
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 - normal :: "['a set, _] => bool" (infixl "<|" 60)
3.37 - "normal H G == subgroup H G &
3.38 - (\<forall>x \<in> carrier G. r_coset G H x = l_coset G x H)"
3.39 +locale normal = subgroup + group +
3.40 + assumes coset_eq: "(\<forall>x \<in> carrier G. H #> x = x <# H)"
3.41
3.42 -syntax (xsymbols)
3.43 - normal :: "['a set, ('a,'b) monoid_scheme] => bool" (infixl "\<lhd>" 60)
3.44 +
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 +subsection {* Subgroups *}
4.177
4.178 -locale submagma = var H + struct G +
4.179 - assumes subset [intro, simp]: "H \<subseteq> carrier G"
4.180 - and m_closed [intro, simp]: "[| x \<in> H; y \<in> H |] ==> x \<otimes> y \<in> H"
4.181 -
4.182 -declare (in submagma) magma.intro [intro] semigroup.intro [intro]
4.183 - semigroup_axioms.intro [intro]
4.184 -
4.185 -lemma submagma_imp_subset:
4.186 - "submagma H G ==> H \<subseteq> carrier G"
4.187 - by (rule submagma.subset)
4.188 -
4.189 -lemma (in submagma) subsetD [dest, simp]:
4.190 - "x \<in> H ==> x \<in> carrier G"
4.191 - using subset by blast
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 +lemma (in subgroup) mem_carrier [simp]:
4.222 + "x \<in> H \<Longrightarrow> x \<in> carrier G"
4.223 + using subset by blast
4.224 +
4.225 +lemma subgroup_imp_subset:
4.226 + "subgroup H G \<Longrightarrow> H \<subseteq> carrier G"
4.227 + by (rule subgroup.subset)
4.228 +
4.229 +lemma (in subgroup) subgroup_is_group [intro]:
4.230 includes group G
4.231 - shows "group_axioms (G(| carrier := H |))"
4.232 - by (rule group_axioms.intro) (auto intro: l_inv r_inv simp add: Units_def)
4.233 -
4.234 -lemma (in subgroup) groupI [intro]:
4.235 - includes group G
4.236 - shows "group (G(| carrier := H |))"
4.237 - by (rule groupI) (auto intro: m_assoc l_inv)
4.238 + shows "group (G\<lparr>carrier := H\<rparr>)"
4.239 + by (rule groupI) (auto intro: m_assoc l_inv mem_carrier)
4.240
4.241 text {*
4.242 Since @{term H} is nonempty, it contains some element @{term x}. Since
4.243 @@ -432,31 +395,13 @@
4.244
4.245 lemma (in group) subgroupI:
4.246 assumes subset: "H \<subseteq> carrier G" and non_empty: "H \<noteq> {}"
4.247 - and inv: "!!a. a \<in> H ==> inv a \<in> H"
4.248 - and mult: "!!a b. [|a \<in> H; b \<in> H|] ==> a \<otimes> b \<in> H"
4.249 + and inv: "!!a. a \<in> H \<Longrightarrow> inv a \<in> H"
4.250 + and mult: "!!a b. \<lbrakk>a \<in> H; b \<in> H\<rbrakk> \<Longrightarrow> a \<otimes> b \<in> H"
4.251 shows "subgroup H G"
4.252 -proof (rule subgroup.intro)
4.253 - from subset and mult show "submagma H G" by (rule submagma.intro)
4.254 -next
4.255 - have "\<one> \<in> H" by (rule one_in_subset) (auto simp only: prems)
4.256 - with inv show "subgroup_axioms H G"
4.257 - by (intro subgroup_axioms.intro) simp_all
4.258 +proof (simp add: subgroup_def prems)
4.259 + show "\<one> \<in> H" by (rule one_in_subset) (auto simp only: prems)
4.260 qed
4.261
4.262 -text {*
4.263 - Repeat facts of submagmas for subgroups. Necessary???
4.264 -*}
4.265 -
4.266 -lemma (in subgroup) subset:
4.267 - "H \<subseteq> carrier G"
4.268 - ..
4.269 -
4.270 -lemma (in subgroup) m_closed:
4.271 - "[| x \<in> H; y \<in> H |] ==> x \<otimes> y \<in> H"
4.272 - ..
4.273 -
4.274 -declare magma.m_closed [simp]
4.275 -
4.276 declare monoid.one_closed [iff] group.inv_closed [simp]
4.277 monoid.l_one [simp] monoid.r_one [simp] group.inv_inv [simp]
4.278
4.279 @@ -467,11 +412,9 @@
4.280 lemma (in subgroup) finite_imp_card_positive:
4.281 "finite (carrier G) ==> 0 < card H"
4.282 proof (rule classical)
4.283 - have sub: "subgroup H G" using prems by (rule subgroup.intro)
4.284 - assume fin: "finite (carrier G)"
4.285 - and zero: "~ 0 < card H"
4.286 - then have "finite H" by (blast intro: finite_subset dest: subset)
4.287 - with zero sub have "subgroup {} G" by simp
4.288 + assume "finite (carrier G)" "~ 0 < card H"
4.289 + then have "finite H" by (blast intro: finite_subset [OF subset])
4.290 + with prems have "subgroup {} G" by simp
4.291 with subgroup_nonempty show ?thesis by contradiction
4.292 qed
4.293
4.294 @@ -482,83 +425,67 @@
4.295
4.296 subsection {* Direct Products *}
4.297
4.298 -constdefs (structure G and H)
4.299 - DirProdSemigroup :: "_ => _ => ('a \<times> 'b) semigroup" (infixr "\<times>\<^sub>s" 80)
4.300 - "G \<times>\<^sub>s H == (| carrier = carrier G \<times> carrier H,
4.301 - mult = (%(g, h) (g', h'). (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')) |)"
4.302 +constdefs
4.303 + DirProd :: "_ \<Rightarrow> _ \<Rightarrow> ('a \<times> 'b) monoid" (infixr "\<times>\<times>" 80)
4.304 + "G \<times>\<times> H \<equiv> \<lparr>carrier = carrier G \<times> carrier H,
4.305 + mult = (\<lambda>(g, h) (g', h'). (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')),
4.306 + one = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)\<rparr>"
4.307
4.308 - DirProdGroup :: "_ => _ => ('a \<times> 'b) monoid" (infixr "\<times>\<^sub>g" 80)
4.309 - "G \<times>\<^sub>g H == semigroup.extend (G \<times>\<^sub>s H) (| one = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>) |)"
4.310 +lemma DirProd_monoid:
4.311 + includes monoid G + monoid H
4.312 + shows "monoid (G \<times>\<times> H)"
4.313 +proof -
4.314 + from prems
4.315 + show ?thesis by (unfold monoid_def DirProd_def, auto)
4.316 +qed
4.317
4.318 -lemma DirProdSemigroup_magma:
4.319 - includes magma G + magma H
4.320 - shows "magma (G \<times>\<^sub>s H)"
4.321 - by (rule magma.intro) (auto simp add: DirProdSemigroup_def)
4.322
4.323 -lemma DirProdSemigroup_semigroup_axioms:
4.324 - includes semigroup G + semigroup H
4.325 - shows "semigroup_axioms (G \<times>\<^sub>s H)"
4.326 - by (rule semigroup_axioms.intro)
4.327 - (auto simp add: DirProdSemigroup_def G.m_assoc H.m_assoc)
4.328 +text{*Does not use the previous result because it's easier just to use auto.*}
4.329 +lemma DirProd_group:
4.330 + includes group G + group H
4.331 + shows "group (G \<times>\<times> H)"
4.332 + by (rule groupI)
4.333 + (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
4.334 + simp add: DirProd_def)
4.335
4.336 -lemma DirProdSemigroup_semigroup:
4.337 - includes semigroup G + semigroup H
4.338 - shows "semigroup (G \<times>\<^sub>s H)"
4.339 - using prems
4.340 - by (fast intro: semigroup.intro
4.341 - DirProdSemigroup_magma DirProdSemigroup_semigroup_axioms)
4.342 +lemma carrier_DirProd [simp]:
4.343 + "carrier (G \<times>\<times> H) = carrier G \<times> carrier H"
4.344 + by (simp add: DirProd_def)
4.345
4.346 -lemma DirProdGroup_magma:
4.347 - includes magma G + magma H
4.348 - shows "magma (G \<times>\<^sub>g H)"
4.349 - by (rule magma.intro)
4.350 - (auto simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
4.351 +lemma one_DirProd [simp]:
4.352 + "\<one>\<^bsub>G \<times>\<times> H\<^esub> = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)"
4.353 + by (simp add: DirProd_def)
4.354
4.355 -lemma DirProdGroup_semigroup_axioms:
4.356 - includes semigroup G + semigroup H
4.357 - shows "semigroup_axioms (G \<times>\<^sub>g H)"
4.358 - by (rule semigroup_axioms.intro)
4.359 - (auto simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs
4.360 - G.m_assoc H.m_assoc)
4.361 +lemma mult_DirProd [simp]:
4.362 + "(g, h) \<otimes>\<^bsub>(G \<times>\<times> H)\<^esub> (g', h') = (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')"
4.363 + by (simp add: DirProd_def)
4.364
4.365 -lemma DirProdGroup_semigroup:
4.366 - includes semigroup G + semigroup H
4.367 - shows "semigroup (G \<times>\<^sub>g H)"
4.368 - using prems
4.369 - by (fast intro: semigroup.intro
4.370 - DirProdGroup_magma DirProdGroup_semigroup_axioms)
4.371 -
4.372 -text {* \dots\ and further lemmas for group \dots *}
4.373 -
4.374 -lemma DirProdGroup_group:
4.375 - includes group G + group H
4.376 - shows "group (G \<times>\<^sub>g H)"
4.377 - by (rule groupI)
4.378 - (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
4.379 - simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
4.380 -
4.381 -lemma carrier_DirProdGroup [simp]:
4.382 - "carrier (G \<times>\<^sub>g H) = carrier G \<times> carrier H"
4.383 - by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
4.384 -
4.385 -lemma one_DirProdGroup [simp]:
4.386 - "\<one>\<^bsub>(G \<times>\<^sub>g H)\<^esub> = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)"
4.387 - by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
4.388 -
4.389 -lemma mult_DirProdGroup [simp]:
4.390 - "(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.391 - by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
4.392 -
4.393 -lemma inv_DirProdGroup [simp]:
4.394 +lemma inv_DirProd [simp]:
4.395 includes group G + group H
4.396 assumes g: "g \<in> carrier G"
4.397 and h: "h \<in> carrier H"
4.398 - shows "m_inv (G \<times>\<^sub>g H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
4.399 - apply (rule group.inv_equality [OF DirProdGroup_group])
4.400 + shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
4.401 + apply (rule group.inv_equality [OF DirProd_group])
4.402 apply (simp_all add: prems group_def group.l_inv)
4.403 done
4.404
4.405 -subsection {* Isomorphisms *}
4.406 +text{*This alternative proof of the previous result demonstrates instantiate.
4.407 + It uses @{text Prod.inv_equality} (available after instantiation) instead of
4.408 + @{text "group.inv_equality [OF DirProd_group]"}. *}
4.409 +lemma
4.410 + includes group G + group H
4.411 + assumes g: "g \<in> carrier G"
4.412 + and h: "h \<in> carrier H"
4.413 + shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
4.414 +proof -
4.415 + have "group (G \<times>\<times> H)"
4.416 + by (blast intro: DirProd_group group.intro prems)
4.417 + then instantiate Prod: group
4.418 + show ?thesis by (simp add: Prod.inv_equality g h)
4.419 +qed
4.420 +
4.421 +
4.422 +subsection {* Homomorphisms and Isomorphisms *}
4.423
4.424 constdefs (structure G and H)
4.425 hom :: "_ => _ => ('a => 'b) set"
4.426 @@ -566,16 +493,6 @@
4.427 {h. h \<in> carrier G -> carrier H &
4.428 (\<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.429
4.430 -lemma (in semigroup) hom:
4.431 - "semigroup (| carrier = hom G G, mult = op o |)"
4.432 -proof (rule semigroup.intro)
4.433 - show "magma (| carrier = hom G G, mult = op o |)"
4.434 - by (rule magma.intro) (simp add: Pi_def hom_def)
4.435 -next
4.436 - show "semigroup_axioms (| carrier = hom G G, mult = op o |)"
4.437 - by (rule semigroup_axioms.intro) (simp add: o_assoc)
4.438 -qed
4.439 -
4.440 lemma hom_mult:
4.441 "[| h \<in> hom G H; x \<in> carrier G; y \<in> carrier G |]
4.442 ==> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
4.443 @@ -613,15 +530,17 @@
4.444 "[|h \<in> G \<cong> H; i \<in> H \<cong> I|] ==> (compose (carrier G) i h) \<in> G \<cong> I"
4.445 by (auto simp add: iso_def hom_compose bij_betw_compose)
4.446
4.447 -lemma DirProdGroup_commute_iso:
4.448 - shows "(%(x,y). (y,x)) \<in> (G \<times>\<^sub>g H) \<cong> (H \<times>\<^sub>g G)"
4.449 +lemma DirProd_commute_iso:
4.450 + shows "(\<lambda>(x,y). (y,x)) \<in> (G \<times>\<times> H) \<cong> (H \<times>\<times> G)"
4.451 by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
4.452
4.453 -lemma DirProdGroup_assoc_iso:
4.454 - 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.455 +lemma DirProd_assoc_iso:
4.456 + 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.457 by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
4.458
4.459
4.460 +text{*Basis for homomorphism proofs: we assume two groups @{term G} and
4.461 + @term{H}, with a homomorphism @{term h} between them*}
4.462 locale group_hom = group G + group H + var h +
4.463 assumes homh: "h \<in> hom G H"
4.464 notes hom_mult [simp] = hom_mult [OF homh]
4.465 @@ -648,11 +567,11 @@
4.466 proof -
4.467 assume x: "x \<in> carrier G"
4.468 then have "h x \<otimes>\<^bsub>H\<^esub> h (inv x) = \<one>\<^bsub>H\<^esub>"
4.469 - by (simp add: hom_mult [symmetric] G.r_inv del: hom_mult)
4.470 + by (simp add: hom_mult [symmetric] del: hom_mult)
4.471 also from x have "... = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)"
4.472 - by (simp add: hom_mult [symmetric] H.r_inv del: hom_mult)
4.473 + by (simp add: hom_mult [symmetric] del: hom_mult)
4.474 finally have "h x \<otimes>\<^bsub>H\<^esub> h (inv x) = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)" .
4.475 - with x show ?thesis by simp
4.476 + with x show ?thesis by (simp del: H.r_inv)
4.477 qed
4.478
4.479 subsection {* Commutative Structures *}
4.480 @@ -665,11 +584,11 @@
4.481
4.482 subsection {* Definition *}
4.483
4.484 -locale comm_semigroup = semigroup +
4.485 - assumes m_comm: "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
4.486 +locale comm_monoid = monoid +
4.487 + assumes m_comm: "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> x \<otimes> y = y \<otimes> x"
4.488
4.489 -lemma (in comm_semigroup) m_lcomm:
4.490 - "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
4.491 +lemma (in comm_monoid) m_lcomm:
4.492 + "\<lbrakk>x \<in> carrier G; y \<in> carrier G; z \<in> carrier G\<rbrakk> \<Longrightarrow>
4.493 x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)"
4.494 proof -
4.495 assume xyz: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
4.496 @@ -679,9 +598,7 @@
4.497 finally show ?thesis .
4.498 qed
4.499
4.500 -lemmas (in comm_semigroup) m_ac = m_assoc m_comm m_lcomm
4.501 -
4.502 -locale comm_monoid = comm_semigroup + monoid
4.503 +lemmas (in comm_monoid) m_ac = m_assoc m_comm m_lcomm
4.504
4.505 lemma comm_monoidI:
4.506 includes struct G
4.507 @@ -696,15 +613,15 @@
4.508 "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
4.509 shows "comm_monoid G"
4.510 using l_one
4.511 - by (auto intro!: comm_monoid.intro magma.intro semigroup_axioms.intro
4.512 - comm_semigroup_axioms.intro monoid_axioms.intro
4.513 - intro: prems simp: m_closed one_closed m_comm)
4.514 + by (auto intro!: comm_monoid.intro comm_monoid_axioms.intro monoid.intro
4.515 + intro: prems simp: m_closed one_closed m_comm)
4.516
4.517 lemma (in monoid) monoid_comm_monoidI:
4.518 assumes m_comm:
4.519 "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
4.520 shows "comm_monoid G"
4.521 by (rule comm_monoidI) (auto intro: m_assoc m_comm)
4.522 +
4.523 (*lemma (in comm_monoid) r_one [simp]:
4.524 "x \<in> carrier G ==> x \<otimes> \<one> = x"
4.525 proof -
4.526 @@ -713,6 +630,7 @@
4.527 also from G have "... = x" by simp
4.528 finally show ?thesis .
4.529 qed*)
4.530 +
4.531 lemma (in comm_monoid) nat_pow_distr:
4.532 "[| x \<in> carrier G; y \<in> carrier G |] ==>
4.533 (x \<otimes> y) (^) (n::nat) = x (^) n \<otimes> y (^) n"
4.534 @@ -724,7 +642,7 @@
4.535 assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
4.536 x \<otimes> y = y \<otimes> x"
4.537 shows "comm_group G"
4.538 - by (fast intro: comm_group.intro comm_semigroup_axioms.intro
4.539 + by (fast intro: comm_group.intro comm_monoid_axioms.intro
4.540 is_group prems)
4.541
4.542 lemma comm_groupI:
4.543 @@ -738,7 +656,7 @@
4.544 and m_comm:
4.545 "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
4.546 and l_one: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x"
4.547 - and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. y \<otimes> x = \<one>"
4.548 + and l_inv_ex: "!!x. x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>"
4.549 shows "comm_group G"
4.550 by (fast intro: group.group_comm_groupI groupI prems)
4.551
4.552 @@ -760,11 +678,11 @@
4.553
4.554 lemma (in group) subgroup_imp_group:
4.555 "subgroup H G ==> group (G(| carrier := H |))"
4.556 - using subgroup.groupI [OF _ group.intro] .
4.557 + using subgroup.subgroup_is_group [OF _ group.intro] .
4.558
4.559 lemma (in group) is_monoid [intro, simp]:
4.560 "monoid G"
4.561 - by (rule monoid.intro)
4.562 + by (auto intro: monoid.intro m_assoc)
4.563
4.564 lemma (in group) subgroup_inv_equality:
4.565 "[| subgroup H G; x \<in> H |] ==> m_inv (G (| carrier := H |)) x = inv x"
4.566 @@ -803,7 +721,7 @@
4.567 next
4.568 have "greatest ?L (carrier G) (carrier ?L)"
4.569 by (unfold greatest_def) (simp add: subgroup.subset subgroup_self)
4.570 - then show "EX G. greatest ?L G (carrier ?L)" ..
4.571 + then show "\<exists>G. greatest ?L G (carrier ?L)" ..
4.572 next
4.573 fix A
4.574 assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}"
4.575 @@ -815,7 +733,6 @@
4.576 fix H
4.577 assume H: "H \<in> A"
4.578 with L have subgroupH: "subgroup H G" by auto
4.579 - from subgroupH have submagmaH: "submagma H G" by (rule subgroup.axioms)
4.580 from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H")
4.581 by (rule subgroup_imp_group)
4.582 from groupH have monoidH: "monoid ?H"
4.583 @@ -831,7 +748,7 @@
4.584 next
4.585 show "?Int \<in> carrier ?L" by simp (rule Int_subgroup)
4.586 qed
4.587 - then show "EX I. greatest ?L I (Lower ?L A)" ..
4.588 + then show "\<exists>I. greatest ?L I (Lower ?L A)" ..
4.589 qed
4.590
4.591 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 -lemma (in sylow_central) setrcos_H_funcset_M:
5.81 - "(\<lambda>C \<in> rcosets G H. M1 #> (@g. g \<in> carrier G \<and> H #> g = C))
5.82 - \<in> rcosets G H \<rightarrow> M"
5.83 -apply (simp add: setrcos_eq)
5.84 +
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