--- a/src/HOL/Algebra/Bij.thy Thu Jun 17 14:27:01 2004 +0200
+++ b/src/HOL/Algebra/Bij.thy Thu Jun 17 17:18:30 2004 +0200
@@ -8,39 +8,39 @@
theory Bij = Group:
constdefs
- Bij :: "'a set => ('a => 'a) set"
+ Bij :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) set"
--{*Only extensional functions, since otherwise we get too many.*}
- "Bij S == extensional S \<inter> {f. bij_betw f S S}"
+ "Bij S \<equiv> extensional S \<inter> {f. bij_betw f S S}"
- BijGroup :: "'a set => ('a => 'a) monoid"
- "BijGroup S ==
- (| carrier = Bij S,
- mult = %g: Bij S. %f: Bij S. compose S g f,
- one = %x: S. x |)"
+ BijGroup :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) monoid"
+ "BijGroup S \<equiv>
+ \<lparr>carrier = Bij S,
+ mult = \<lambda>g \<in> Bij S. \<lambda>f \<in> Bij S. compose S g f,
+ one = \<lambda>x \<in> S. x\<rparr>"
declare Id_compose [simp] compose_Id [simp]
-lemma Bij_imp_extensional: "f \<in> Bij S ==> f \<in> extensional S"
+lemma Bij_imp_extensional: "f \<in> Bij S \<Longrightarrow> f \<in> extensional S"
by (simp add: Bij_def)
-lemma Bij_imp_funcset: "f \<in> Bij S ==> f \<in> S -> S"
+lemma Bij_imp_funcset: "f \<in> Bij S \<Longrightarrow> f \<in> S \<rightarrow> S"
by (auto simp add: Bij_def bij_betw_imp_funcset)
subsection {*Bijections Form a Group *}
-lemma restrict_Inv_Bij: "f \<in> Bij S ==> (%x:S. (Inv S f) x) \<in> Bij S"
+lemma restrict_Inv_Bij: "f \<in> Bij S \<Longrightarrow> (\<lambda>x \<in> S. (Inv S f) x) \<in> Bij S"
by (simp add: Bij_def bij_betw_Inv)
lemma id_Bij: "(\<lambda>x\<in>S. x) \<in> Bij S "
by (auto simp add: Bij_def bij_betw_def inj_on_def)
-lemma compose_Bij: "[| x \<in> Bij S; y \<in> Bij S|] ==> compose S x y \<in> Bij S"
+lemma compose_Bij: "\<lbrakk>x \<in> Bij S; y \<in> Bij S\<rbrakk> \<Longrightarrow> compose S x y \<in> Bij S"
by (auto simp add: Bij_def bij_betw_compose)
lemma Bij_compose_restrict_eq:
- "f \<in> Bij S ==> compose S (restrict (Inv S f) S) f = (\<lambda>x\<in>S. x)"
+ "f \<in> Bij S \<Longrightarrow> compose S (restrict (Inv S f) S) f = (\<lambda>x\<in>S. x)"
by (simp add: Bij_def compose_Inv_id)
theorem group_BijGroup: "group (BijGroup S)"
@@ -57,62 +57,68 @@
subsection{*Automorphisms Form a Group*}
-lemma Bij_Inv_mem: "[| f \<in> Bij S; x \<in> S |] ==> Inv S f x \<in> S"
+lemma Bij_Inv_mem: "\<lbrakk> f \<in> Bij S; x \<in> S\<rbrakk> \<Longrightarrow> Inv S f x \<in> S"
by (simp add: Bij_def bij_betw_def Inv_mem)
lemma Bij_Inv_lemma:
- assumes eq: "!!x y. [|x \<in> S; y \<in> S|] ==> h(g x y) = g (h x) (h y)"
- shows "[| h \<in> Bij S; g \<in> S \<rightarrow> S \<rightarrow> S; x \<in> S; y \<in> S |]
- ==> Inv S h (g x y) = g (Inv S h x) (Inv S h y)"
+ assumes eq: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> h(g x y) = g (h x) (h y)"
+ shows "\<lbrakk>h \<in> Bij S; g \<in> S \<rightarrow> S \<rightarrow> S; x \<in> S; y \<in> S\<rbrakk>
+ \<Longrightarrow> Inv S h (g x y) = g (Inv S h x) (Inv S h y)"
apply (simp add: Bij_def bij_betw_def)
apply (subgoal_tac "\<exists>x'\<in>S. \<exists>y'\<in>S. x = h x' & y = h y'", clarify)
- apply (simp add: eq [symmetric] Inv_f_f funcset_mem [THEN funcset_mem], blast )
+ apply (simp add: eq [symmetric] Inv_f_f funcset_mem [THEN funcset_mem], blast)
done
+
constdefs
- auto :: "('a, 'b) monoid_scheme => ('a => 'a) set"
- "auto G == hom G G \<inter> Bij (carrier G)"
+ auto :: "('a, 'b) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'a) set"
+ "auto G \<equiv> hom G G \<inter> Bij (carrier G)"
- AutoGroup :: "('a, 'c) monoid_scheme => ('a => 'a) monoid"
- "AutoGroup G == BijGroup (carrier G) (|carrier := auto G |)"
+ AutoGroup :: "('a, 'c) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'a) monoid"
+ "AutoGroup G \<equiv> BijGroup (carrier G) \<lparr>carrier := auto G\<rparr>"
-lemma id_in_auto: "group G ==> (%x: carrier G. x) \<in> auto G"
+lemma (in group) id_in_auto: "(\<lambda>x \<in> carrier G. x) \<in> auto G"
by (simp add: auto_def hom_def restrictI group.axioms id_Bij)
-lemma mult_funcset: "group G ==> mult G \<in> carrier G -> carrier G -> carrier G"
+lemma (in group) mult_funcset: "mult G \<in> carrier G \<rightarrow> carrier G \<rightarrow> carrier G"
by (simp add: Pi_I group.axioms)
-lemma restrict_Inv_hom:
- "[|group G; h \<in> hom G G; h \<in> Bij (carrier G)|]
- ==> restrict (Inv (carrier G) h) (carrier G) \<in> hom G G"
+lemma (in group) restrict_Inv_hom:
+ "\<lbrakk>h \<in> hom G G; h \<in> Bij (carrier G)\<rbrakk>
+ \<Longrightarrow> restrict (Inv (carrier G) h) (carrier G) \<in> hom G G"
by (simp add: hom_def Bij_Inv_mem restrictI mult_funcset
group.axioms Bij_Inv_lemma)
lemma inv_BijGroup:
- "f \<in> Bij S ==> m_inv (BijGroup S) f = (%x: S. (Inv S f) x)"
+ "f \<in> Bij S \<Longrightarrow> m_inv (BijGroup S) f = (\<lambda>x \<in> S. (Inv S f) x)"
apply (rule group.inv_equality)
apply (rule group_BijGroup)
apply (simp_all add: BijGroup_def restrict_Inv_Bij Bij_compose_restrict_eq)
done
-lemma subgroup_auto:
- "group G ==> subgroup (auto G) (BijGroup (carrier G))"
-apply (rule group.subgroupI)
- apply (rule group_BijGroup)
- apply (force simp add: auto_def BijGroup_def)
- apply (blast dest: id_in_auto)
- apply (simp del: restrict_apply
+lemma (in group) subgroup_auto:
+ "subgroup (auto G) (BijGroup (carrier G))"
+proof (rule subgroup.intro)
+ show "auto G \<subseteq> carrier (BijGroup (carrier G))"
+ by (force simp add: auto_def BijGroup_def)
+next
+ fix x y
+ assume "x \<in> auto G" "y \<in> auto G"
+ thus "x \<otimes>\<^bsub>BijGroup (carrier G)\<^esub> y \<in> auto G"
+ by (force simp add: BijGroup_def is_group auto_def Bij_imp_funcset
+ group.hom_compose compose_Bij)
+next
+ show "\<one>\<^bsub>BijGroup (carrier G)\<^esub> \<in> auto G" by (simp add: BijGroup_def id_in_auto)
+next
+ fix x
+ assume "x \<in> auto G"
+ thus "inv\<^bsub>BijGroup (carrier G)\<^esub> x \<in> auto G"
+ by (simp del: restrict_apply
add: inv_BijGroup auto_def restrict_Inv_Bij restrict_Inv_hom)
-apply (auto simp add: BijGroup_def auto_def Bij_imp_funcset group.hom_compose
- compose_Bij)
-done
+qed
-theorem AutoGroup: "group G ==> group (AutoGroup G)"
-apply (simp add: AutoGroup_def)
-apply (rule Group.subgroup.groupI)
-apply (erule subgroup_auto)
-apply (insert Bij.group_BijGroup [of "carrier G"])
-apply (simp_all add: group_def)
-done
+theorem (in group) AutoGroup: "group (AutoGroup G)"
+by (simp add: AutoGroup_def subgroup.subgroup_is_group subgroup_auto
+ group_BijGroup)
end
--- a/src/HOL/Algebra/CRing.thy Thu Jun 17 14:27:01 2004 +0200
+++ b/src/HOL/Algebra/CRing.thy Thu Jun 17 17:18:30 2004 +0200
@@ -24,16 +24,18 @@
"[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y == x \<oplus> (\<ominus> y)"
locale abelian_monoid = struct G +
- assumes a_comm_monoid: "comm_monoid (| carrier = carrier G,
- mult = add G, one = zero G |)"
+ assumes a_comm_monoid:
+ "comm_monoid (| carrier = carrier G, mult = add G, one = zero G |)"
+
text {*
The following definition is redundant but simple to use.
*}
locale abelian_group = abelian_monoid +
- assumes a_comm_group: "comm_group (| carrier = carrier G,
- mult = add G, one = zero G |)"
+ assumes a_comm_group:
+ "comm_group (| carrier = carrier G, mult = add G, one = zero G |)"
+
subsection {* Basic Properties *}
@@ -66,35 +68,19 @@
abelian_group_axioms.intro comm_monoidI comm_groupI
intro: prems)
-(* TODO: The following thms are probably unnecessary. *)
-
-lemma (in abelian_monoid) a_magma:
- "magma (| carrier = carrier G, mult = add G, one = zero G |)"
- by (rule comm_monoid.axioms) (rule a_comm_monoid)
-
-lemma (in abelian_monoid) a_semigroup:
- "semigroup (| carrier = carrier G, mult = add G, one = zero G |)"
- by (unfold semigroup_def) (fast intro: comm_monoid.axioms a_comm_monoid)
-
lemma (in abelian_monoid) a_monoid:
"monoid (| carrier = carrier G, mult = add G, one = zero G |)"
- by (unfold monoid_def) (fast intro: a_comm_monoid comm_monoid.axioms)
+by (rule comm_monoid.axioms, rule a_comm_monoid)
lemma (in abelian_group) a_group:
"group (| carrier = carrier G, mult = add G, one = zero G |)"
- by (unfold group_def semigroup_def)
- (fast intro: comm_group.axioms a_comm_group)
+by (simp add: group_def a_monoid comm_group.axioms a_comm_group)
-lemma (in abelian_monoid) a_comm_semigroup:
- "comm_semigroup (| carrier = carrier G, mult = add G, one = zero G |)"
- by (unfold comm_semigroup_def semigroup_def)
- (fast intro: comm_monoid.axioms a_comm_monoid)
-
-lemmas monoid_record_simps = partial_object.simps semigroup.simps monoid.simps
+lemmas monoid_record_simps = partial_object.simps monoid.simps
lemma (in abelian_monoid) a_closed [intro, simp]:
- "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus> y \<in> carrier G"
- by (rule magma.m_closed [OF a_magma, simplified monoid_record_simps])
+ "\<lbrakk> x \<in> carrier G; y \<in> carrier G \<rbrakk> \<Longrightarrow> x \<oplus> y \<in> carrier G"
+ by (rule monoid.m_closed [OF a_monoid, simplified monoid_record_simps])
lemma (in abelian_monoid) zero_closed [intro, simp]:
"\<zero> \<in> carrier G"
@@ -120,9 +106,9 @@
by (rule group.r_cancel [OF a_group, simplified monoid_record_simps])
lemma (in abelian_monoid) a_assoc:
- "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
+ "\<lbrakk>x \<in> carrier G; y \<in> carrier G; z \<in> carrier G\<rbrakk> \<Longrightarrow>
(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
- by (rule semigroup.m_assoc [OF a_semigroup, simplified monoid_record_simps])
+ by (rule monoid.m_assoc [OF a_monoid, simplified monoid_record_simps])
lemma (in abelian_monoid) l_zero [simp]:
"x \<in> carrier G ==> \<zero> \<oplus> x = x"
@@ -134,15 +120,15 @@
group.l_inv [OF a_group, simplified monoid_record_simps])
lemma (in abelian_monoid) a_comm:
- "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus> y = y \<oplus> x"
- by (rule comm_semigroup.m_comm [OF a_comm_semigroup,
+ "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> x \<oplus> y = y \<oplus> x"
+ by (rule comm_monoid.m_comm [OF a_comm_monoid,
simplified monoid_record_simps])
lemma (in abelian_monoid) a_lcomm:
- "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
+ "\<lbrakk>x \<in> carrier G; y \<in> carrier G; z \<in> carrier G\<rbrakk> \<Longrightarrow>
x \<oplus> (y \<oplus> z) = y \<oplus> (x \<oplus> z)"
- by (rule comm_semigroup.m_lcomm [OF a_comm_semigroup,
- simplified monoid_record_simps])
+ by (rule comm_monoid.m_lcomm [OF a_comm_monoid,
+ simplified monoid_record_simps])
lemma (in abelian_monoid) r_zero [simp]:
"x \<in> carrier G ==> x \<oplus> \<zero> = x"
@@ -329,7 +315,7 @@
==> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
shows "ring R"
by (auto intro: ring.intro
- abelian_group.axioms monoid.axioms ring_axioms.intro prems)
+ abelian_group.axioms ring_axioms.intro prems)
lemma (in ring) is_abelian_group:
"abelian_group R"
@@ -356,13 +342,12 @@
note [simp]= comm_monoid.axioms [OF comm_monoid]
abelian_group.axioms [OF abelian_group]
abelian_monoid.a_closed
- magma.m_closed
from R have "z \<otimes> (x \<oplus> y) = (x \<oplus> y) \<otimes> z"
- by (simp add: comm_semigroup.m_comm [OF comm_semigroup.intro])
+ by (simp add: comm_monoid.m_comm [OF comm_monoid.intro])
also from R have "... = x \<otimes> z \<oplus> y \<otimes> z" by (simp add: l_distr)
also from R have "... = z \<otimes> x \<oplus> z \<otimes> y"
- by (simp add: comm_semigroup.m_comm [OF comm_semigroup.intro])
+ by (simp add: comm_monoid.m_comm [OF comm_monoid.intro])
finally show "z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y" .
qed
qed (auto intro: cring.intro
--- a/src/HOL/Algebra/Coset.thy Thu Jun 17 14:27:01 2004 +0200
+++ b/src/HOL/Algebra/Coset.thy Thu Jun 17 17:18:30 2004 +0200
@@ -7,46 +7,36 @@
theory Coset = Group + Exponent:
-declare (in group) l_inv [simp] and r_inv [simp]
-
constdefs (structure G)
- r_coset :: "[_, 'a set, 'a] => 'a set" (infixl "#>\<index>" 60)
- "H #> a == (% x. x \<otimes> a) ` H"
+ r_coset :: "[_, 'a set, 'a] \<Rightarrow> 'a set" (infixl "#>\<index>" 60)
+ "H #> a \<equiv> \<Union>h\<in>H. {h \<otimes> a}"
- l_coset :: "[_, 'a, 'a set] => 'a set" (infixl "<#\<index>" 60)
- "a <# H == (% x. a \<otimes> x) ` H"
+ l_coset :: "[_, 'a, 'a set] \<Rightarrow> 'a set" (infixl "<#\<index>" 60)
+ "a <# H \<equiv> \<Union>h\<in>H. {a \<otimes> h}"
- rcosets :: "[_, 'a set] => ('a set)set"
- "rcosets G H == r_coset G H ` (carrier G)"
+ RCOSETS :: "[_, 'a set] \<Rightarrow> ('a set)set" ("rcosets\<index> _" [81] 80)
+ "rcosets H \<equiv> \<Union>a\<in>carrier G. {H #> a}"
+
+ set_mult :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<#>\<index>" 60)
+ "H <#> K \<equiv> \<Union>h\<in>H. \<Union>k\<in>K. {h \<otimes> k}"
- set_mult :: "[_, 'a set ,'a set] => 'a set" (infixl "<#>\<index>" 60)
- "H <#> K == (%(x,y). x \<otimes> y) ` (H \<times> K)"
+ SET_INV :: "[_,'a set] \<Rightarrow> 'a set" ("set'_inv\<index> _" [81] 80)
+ "set_inv H \<equiv> \<Union>h\<in>H. {inv h}"
- set_inv :: "[_,'a set] => 'a set"
- "set_inv G H == m_inv G ` H"
+
+locale normal = subgroup + group +
+ assumes coset_eq: "(\<forall>x \<in> carrier G. H #> x = x <# H)"
- normal :: "['a set, _] => bool" (infixl "<|" 60)
- "normal H G == subgroup H G &
- (\<forall>x \<in> carrier G. r_coset G H x = l_coset G x H)"
-syntax (xsymbols)
- normal :: "['a set, ('a,'b) monoid_scheme] => bool" (infixl "\<lhd>" 60)
+syntax
+ "@normal" :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool" (infixl "\<lhd>" 60)
+
+translations
+ "H \<lhd> G" == "normal H G"
subsection {*Basic Properties of Cosets*}
-lemma (in group) r_coset_eq: "H #> a = {b . \<exists>h\<in>H. h \<otimes> a = b}"
-by (auto simp add: r_coset_def)
-
-lemma (in group) l_coset_eq: "a <# H = {b . \<exists>h\<in>H. a \<otimes> h = b}"
-by (auto simp add: l_coset_def)
-
-lemma (in group) setrcos_eq: "rcosets G H = {C . \<exists>a\<in>carrier G. C = H #> a}"
-by (auto simp add: rcosets_def)
-
-lemma (in group) set_mult_eq: "H <#> K = {c . \<exists>h\<in>H. \<exists>k\<in>K. c = h \<otimes> k}"
-by (simp add: set_mult_def image_def)
-
lemma (in group) coset_mult_assoc:
"[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
==> (M #> g) #> h = M #> (g \<otimes> h)"
@@ -72,20 +62,27 @@
lemma (in group) coset_join1:
"[| H #> x = H; x \<in> carrier G; subgroup H G |] ==> x \<in> H"
apply (erule subst)
-apply (simp add: r_coset_eq)
-apply (blast intro: l_one subgroup.one_closed)
+apply (simp add: r_coset_def)
+apply (blast intro: l_one subgroup.one_closed sym)
done
lemma (in group) solve_equation:
- "\<lbrakk>subgroup H G; x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. h \<otimes> x = y"
+ "\<lbrakk>subgroup H G; x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. y = h \<otimes> x"
apply (rule bexI [of _ "y \<otimes> (inv x)"])
apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc
subgroup.subset [THEN subsetD])
done
+lemma (in group) repr_independence:
+ "\<lbrakk>y \<in> H #> x; x \<in> carrier G; subgroup H G\<rbrakk> \<Longrightarrow> H #> x = H #> y"
+by (auto simp add: r_coset_def m_assoc [symmetric]
+ subgroup.subset [THEN subsetD]
+ subgroup.m_closed solve_equation)
+
lemma (in group) coset_join2:
- "[| x \<in> carrier G; subgroup H G; x\<in>H |] ==> H #> x = H"
-by (force simp add: subgroup.m_closed r_coset_eq solve_equation)
+ "\<lbrakk>x \<in> carrier G; subgroup H G; x\<in>H\<rbrakk> \<Longrightarrow> H #> x = H"
+ --{*Alternative proof is to put @{term "x=\<one>"} in @{text repr_independence}.*}
+by (force simp add: subgroup.m_closed r_coset_def solve_equation)
lemma (in group) r_coset_subset_G:
"[| H \<subseteq> carrier G; x \<in> carrier G |] ==> H #> x \<subseteq> carrier G"
@@ -95,10 +92,9 @@
"[| h \<in> H; H \<subseteq> carrier G; x \<in> carrier G|] ==> h \<otimes> x \<in> H #> x"
by (auto simp add: r_coset_def)
-lemma (in group) setrcosI:
- "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> H #> x \<in> rcosets G H"
-by (auto simp add: setrcos_eq)
-
+lemma (in group) rcosetsI:
+ "\<lbrakk>H \<subseteq> carrier G; x \<in> carrier G\<rbrakk> \<Longrightarrow> H #> x \<in> rcosets H"
+by (auto simp add: RCOSETS_def)
text{*Really needed?*}
lemma (in group) transpose_inv:
@@ -106,37 +102,37 @@
==> (inv x) \<otimes> z = y"
by (force simp add: m_assoc [symmetric])
-lemma (in group) repr_independence:
- "[| y \<in> H #> x; x \<in> carrier G; subgroup H G |] ==> H #> x = H #> y"
-by (auto simp add: r_coset_eq m_assoc [symmetric]
- subgroup.subset [THEN subsetD]
- subgroup.m_closed solve_equation)
-
lemma (in group) rcos_self: "[| x \<in> carrier G; subgroup H G |] ==> x \<in> H #> x"
-apply (simp add: r_coset_eq)
-apply (blast intro: l_one subgroup.subset [THEN subsetD]
+apply (simp add: r_coset_def)
+apply (blast intro: sym l_one subgroup.subset [THEN subsetD]
subgroup.one_closed)
done
subsection {* Normal subgroups *}
-lemma normal_imp_subgroup: "H <| G ==> subgroup H G"
-by (simp add: normal_def)
+lemma normal_imp_subgroup: "H \<lhd> G \<Longrightarrow> subgroup H G"
+ by (simp add: normal_def subgroup_def)
-lemma (in group) normal_inv_op_closed1:
- "\<lbrakk>H \<lhd> G; x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<otimes> h \<otimes> x \<in> H"
-apply (auto simp add: l_coset_def r_coset_def normal_def)
+lemma (in group) normalI:
+ "subgroup H G \<Longrightarrow> (\<forall>x \<in> carrier G. H #> x = x <# H) \<Longrightarrow> H \<lhd> G";
+ by (simp add: normal_def normal_axioms_def prems)
+
+lemma (in normal) inv_op_closed1:
+ "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<otimes> h \<otimes> x \<in> H"
+apply (insert coset_eq)
+apply (auto simp add: l_coset_def r_coset_def)
apply (drule bspec, assumption)
apply (drule equalityD1 [THEN subsetD], blast, clarify)
-apply (simp add: m_assoc subgroup.subset [THEN subsetD])
-apply (simp add: m_assoc [symmetric] subgroup.subset [THEN subsetD])
+apply (simp add: m_assoc)
+apply (simp add: m_assoc [symmetric])
done
-lemma (in group) normal_inv_op_closed2:
- "\<lbrakk>H \<lhd> G; x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> (inv x) \<in> H"
-apply (drule normal_inv_op_closed1 [of H "(inv x)"])
-apply auto
+lemma (in normal) inv_op_closed2:
+ "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> (inv x) \<in> H"
+apply (subgoal_tac "inv (inv x) \<otimes> h \<otimes> (inv x) \<in> H")
+apply (simp add: );
+apply (blast intro: inv_op_closed1)
done
text{*Alternative characterization of normal subgroups*}
@@ -147,46 +143,47 @@
proof
assume N: "N \<lhd> G"
show ?rhs
- by (blast intro: N normal_imp_subgroup normal_inv_op_closed2)
+ by (blast intro: N normal.inv_op_closed2 normal_imp_subgroup)
next
assume ?rhs
hence sg: "subgroup N G"
- and closed: "!!x. x\<in>carrier G ==> \<forall>h\<in>N. x \<otimes> h \<otimes> inv x \<in> N" by auto
+ and closed: "\<And>x. x\<in>carrier G \<Longrightarrow> \<forall>h\<in>N. x \<otimes> h \<otimes> inv x \<in> N" by auto
hence sb: "N \<subseteq> carrier G" by (simp add: subgroup.subset)
show "N \<lhd> G"
- proof (simp add: sg normal_def l_coset_def r_coset_def, clarify)
+ proof (intro normalI [OF sg], simp add: l_coset_def r_coset_def, clarify)
fix x
assume x: "x \<in> carrier G"
- show "(\<lambda>n. n \<otimes> x) ` N = op \<otimes> x ` N"
+ show "(\<Union>\<^bsub>h\<in>N\<^esub> {h \<otimes> x}) = (\<Union>\<^bsub>h\<in>N\<^esub> {x \<otimes> h})"
proof
- show "(\<lambda>n. n \<otimes> x) ` N \<subseteq> op \<otimes> x ` N"
+ show "(\<Union>\<^bsub>h\<in>N\<^esub> {h \<otimes> x}) \<subseteq> (\<Union>\<^bsub>h\<in>N\<^esub> {x \<otimes> h})"
proof clarify
fix n
assume n: "n \<in> N"
- show "n \<otimes> x \<in> op \<otimes> x ` N"
+ show "n \<otimes> x \<in> (\<Union>\<^bsub>h\<in>N\<^esub> {x \<otimes> h})"
proof
- show "n \<otimes> x = x \<otimes> (inv x \<otimes> n \<otimes> x)"
+ from closed [of "inv x"]
+ show "inv x \<otimes> n \<otimes> x \<in> N" by (simp add: x n)
+ show "n \<otimes> x \<in> {x \<otimes> (inv x \<otimes> n \<otimes> x)}"
by (simp add: x n m_assoc [symmetric] sb [THEN subsetD])
- with closed [of "inv x"]
- show "inv x \<otimes> n \<otimes> x \<in> N" by (simp add: x n)
qed
qed
next
- show "op \<otimes> x ` N \<subseteq> (\<lambda>n. n \<otimes> x) ` N"
+ show "(\<Union>\<^bsub>h\<in>N\<^esub> {x \<otimes> h}) \<subseteq> (\<Union>\<^bsub>h\<in>N\<^esub> {h \<otimes> x})"
proof clarify
fix n
assume n: "n \<in> N"
- show "x \<otimes> n \<in> (\<lambda>n. n \<otimes> x) ` N"
+ show "x \<otimes> n \<in> (\<Union>\<^bsub>h\<in>N\<^esub> {h \<otimes> x})"
proof
- show "x \<otimes> n = (x \<otimes> n \<otimes> inv x) \<otimes> x"
+ show "x \<otimes> n \<otimes> inv x \<in> N" by (simp add: x n closed)
+ show "x \<otimes> n \<in> {x \<otimes> n \<otimes> inv x \<otimes> x}"
by (simp add: x n m_assoc sb [THEN subsetD])
- show "x \<otimes> n \<otimes> inv x \<in> N" by (simp add: x n closed)
qed
qed
qed
qed
qed
+
subsection{*More Properties of Cosets*}
lemma (in group) lcos_m_assoc:
@@ -202,15 +199,15 @@
by (auto simp add: l_coset_def subsetD)
lemma (in group) l_coset_swap:
- "[| y \<in> x <# H; x \<in> carrier G; subgroup H G |] ==> x \<in> y <# H"
-proof (simp add: l_coset_eq)
- assume "\<exists>h\<in>H. x \<otimes> h = y"
+ "\<lbrakk>y \<in> x <# H; x \<in> carrier G; subgroup H G\<rbrakk> \<Longrightarrow> x \<in> y <# H"
+proof (simp add: l_coset_def)
+ assume "\<exists>h\<in>H. y = x \<otimes> h"
and x: "x \<in> carrier G"
and sb: "subgroup H G"
then obtain h' where h': "h' \<in> H & x \<otimes> h' = y" by blast
- show "\<exists>h\<in>H. y \<otimes> h = x"
+ show "\<exists>h\<in>H. x = y \<otimes> h"
proof
- show "y \<otimes> inv h' = x" using h' x sb
+ show "x = y \<otimes> inv h'" using h' x sb
by (auto simp add: m_assoc subgroup.subset [THEN subsetD])
show "inv h' \<in> H" using h' sb
by (auto simp add: subgroup.subset [THEN subsetD] subgroup.m_inv_closed)
@@ -244,11 +241,11 @@
qed
lemma (in group) setmult_subset_G:
- "[| H \<subseteq> carrier G; K \<subseteq> carrier G |] ==> H <#> K \<subseteq> carrier G"
-by (auto simp add: set_mult_eq subsetD)
+ "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G\<rbrakk> \<Longrightarrow> H <#> K \<subseteq> carrier G"
+by (auto simp add: set_mult_def subsetD)
-lemma (in group) subgroup_mult_id: "subgroup H G ==> H <#> H = H"
-apply (auto simp add: subgroup.m_closed set_mult_eq Sigma_def image_def)
+lemma (in group) subgroup_mult_id: "subgroup H G \<Longrightarrow> H <#> H = H"
+apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def image_def)
apply (rule_tac x = x in bexI)
apply (rule bexI [of _ "\<one>"])
apply (auto simp add: subgroup.m_closed subgroup.one_closed
@@ -258,135 +255,180 @@
subsubsection {* Set of inverses of an @{text r_coset}. *}
-lemma (in group) rcos_inv:
- assumes normalHG: "H <| G"
- and x: "x \<in> carrier G"
- shows "set_inv G (H #> x) = H #> (inv x)"
-proof -
- have H_subset: "H \<subseteq> carrier G"
- by (rule subgroup.subset [OF normal_imp_subgroup, OF normalHG])
- show ?thesis
- proof (auto simp add: r_coset_eq image_def set_inv_def)
- fix h
- assume "h \<in> H"
- hence "((inv x) \<otimes> (inv h) \<otimes> x) \<otimes> inv x = inv (h \<otimes> x)"
- by (simp add: x m_assoc inv_mult_group H_subset [THEN subsetD])
- thus "\<exists>j\<in>H. j \<otimes> inv x = inv (h \<otimes> x)"
- using prems
- by (blast intro: normal_inv_op_closed1 normal_imp_subgroup
- subgroup.m_inv_closed)
- next
- fix h
- assume "h \<in> H"
- hence eq: "(x \<otimes> (inv h) \<otimes> (inv x)) \<otimes> x = x \<otimes> inv h"
- by (simp add: x m_assoc H_subset [THEN subsetD])
- hence "(\<exists>j\<in>H. j \<otimes> x = inv (h \<otimes> (inv x))) \<and> h \<otimes> inv x = inv (inv (h \<otimes> (inv x)))"
- using prems
- by (simp add: m_assoc inv_mult_group H_subset [THEN subsetD],
- blast intro: eq normal_inv_op_closed2 normal_imp_subgroup
- subgroup.m_inv_closed)
- thus "\<exists>y. (\<exists>h\<in>H. h \<otimes> x = y) \<and> h \<otimes> inv x = inv y" ..
+lemma (in normal) rcos_inv:
+ assumes x: "x \<in> carrier G"
+ shows "set_inv (H #> x) = H #> (inv x)"
+proof (simp add: r_coset_def SET_INV_def x inv_mult_group, safe)
+ fix h
+ assume "h \<in> H"
+ show "inv x \<otimes> inv h \<in> (\<Union>\<^bsub>j\<in>H\<^esub> {j \<otimes> inv x})"
+ proof
+ show "inv x \<otimes> inv h \<otimes> x \<in> H"
+ by (simp add: inv_op_closed1 prems)
+ show "inv x \<otimes> inv h \<in> {inv x \<otimes> inv h \<otimes> x \<otimes> inv x}"
+ by (simp add: prems m_assoc)
+ qed
+next
+ fix h
+ assume "h \<in> H"
+ show "h \<otimes> inv x \<in> (\<Union>\<^bsub>j\<in>H\<^esub> {inv x \<otimes> inv j})"
+ proof
+ show "x \<otimes> inv h \<otimes> inv x \<in> H"
+ by (simp add: inv_op_closed2 prems)
+ show "h \<otimes> inv x \<in> {inv x \<otimes> inv (x \<otimes> inv h \<otimes> inv x)}"
+ by (simp add: prems m_assoc [symmetric] inv_mult_group)
qed
qed
-lemma (in group) rcos_inv2:
- "[| H <| G; K \<in> rcosets G H; x \<in> K |] ==> set_inv G K = H #> (inv x)"
-apply (simp add: setrcos_eq, clarify)
-apply (subgoal_tac "x : carrier G")
- prefer 2
- apply (blast dest: r_coset_subset_G subgroup.subset normal_imp_subgroup)
-apply (drule repr_independence)
- apply assumption
- apply (erule normal_imp_subgroup)
-apply (simp add: rcos_inv)
-done
-
subsubsection {*Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.*}
lemma (in group) setmult_rcos_assoc:
- "[| H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G |]
- ==> H <#> (K #> x) = (H <#> K) #> x"
-apply (auto simp add: r_coset_def set_mult_def)
-apply (force simp add: m_assoc)+
-done
+ "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
+ \<Longrightarrow> H <#> (K #> x) = (H <#> K) #> x"
+by (force simp add: r_coset_def set_mult_def m_assoc)
lemma (in group) rcos_assoc_lcos:
- "[| H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G |]
- ==> (H #> x) <#> K = H <#> (x <# K)"
-apply (auto simp add: r_coset_def l_coset_def set_mult_def Sigma_def image_def)
-apply (force intro!: exI bexI simp add: m_assoc)+
-done
+ "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
+ \<Longrightarrow> (H #> x) <#> K = H <#> (x <# K)"
+by (force simp add: r_coset_def l_coset_def set_mult_def m_assoc)
-lemma (in group) rcos_mult_step1:
- "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
- ==> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
-by (simp add: setmult_rcos_assoc normal_imp_subgroup [THEN subgroup.subset]
+lemma (in normal) rcos_mult_step1:
+ "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
+ \<Longrightarrow> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
+by (simp add: setmult_rcos_assoc subset
r_coset_subset_G l_coset_subset_G rcos_assoc_lcos)
-lemma (in group) rcos_mult_step2:
- "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
- ==> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"
-by (simp add: normal_def)
+lemma (in normal) rcos_mult_step2:
+ "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
+ \<Longrightarrow> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"
+by (insert coset_eq, simp add: normal_def)
-lemma (in group) rcos_mult_step3:
- "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
- ==> (H <#> (H #> x)) #> y = H #> (x \<otimes> y)"
-by (simp add: setmult_rcos_assoc r_coset_subset_G coset_mult_assoc
- setmult_subset_G subgroup_mult_id
- subgroup.subset normal_imp_subgroup)
+lemma (in normal) rcos_mult_step3:
+ "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
+ \<Longrightarrow> (H <#> (H #> x)) #> y = H #> (x \<otimes> y)"
+by (simp add: setmult_rcos_assoc coset_mult_assoc
+ subgroup_mult_id subset prems)
-lemma (in group) rcos_sum:
- "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
- ==> (H #> x) <#> (H #> y) = H #> (x \<otimes> y)"
+lemma (in normal) rcos_sum:
+ "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
+ \<Longrightarrow> (H #> x) <#> (H #> y) = H #> (x \<otimes> y)"
by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)
-lemma (in group) setrcos_mult_eq: "[|H <| G; M \<in> rcosets G H|] ==> H <#> M = M"
+lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M"
-- {* generalizes @{text subgroup_mult_id} *}
- by (auto simp add: setrcos_eq normal_imp_subgroup subgroup.subset
- setmult_rcos_assoc subgroup_mult_id)
+ by (auto simp add: RCOSETS_def subset
+ setmult_rcos_assoc subgroup_mult_id prems)
+
+
+subsubsection{*An Equivalence Relation*}
+
+constdefs (structure G)
+ r_congruent :: "[('a,'b)monoid_scheme, 'a set] \<Rightarrow> ('a*'a)set"
+ ("rcong\<index> _")
+ "rcong H \<equiv> {(x,y). x \<in> carrier G & y \<in> carrier G & inv x \<otimes> y \<in> H}"
+
+
+lemma (in subgroup) equiv_rcong:
+ includes group G
+ shows "equiv (carrier G) (rcong H)"
+proof (intro equiv.intro)
+ show "refl (carrier G) (rcong H)"
+ by (auto simp add: r_congruent_def refl_def)
+next
+ show "sym (rcong H)"
+ proof (simp add: r_congruent_def sym_def, clarify)
+ fix x y
+ assume [simp]: "x \<in> carrier G" "y \<in> carrier G"
+ and "inv x \<otimes> y \<in> H"
+ hence "inv (inv x \<otimes> y) \<in> H" by (simp add: m_inv_closed)
+ thus "inv y \<otimes> x \<in> H" by (simp add: inv_mult_group)
+ qed
+next
+ show "trans (rcong H)"
+ proof (simp add: r_congruent_def trans_def, clarify)
+ fix x y z
+ assume [simp]: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
+ and "inv x \<otimes> y \<in> H" and "inv y \<otimes> z \<in> H"
+ hence "(inv x \<otimes> y) \<otimes> (inv y \<otimes> z) \<in> H" by simp
+ hence "inv x \<otimes> (y \<otimes> inv y) \<otimes> z \<in> H" by (simp add: m_assoc del: r_inv)
+ thus "inv x \<otimes> z \<in> H" by simp
+ qed
+qed
+
+text{*Equivalence classes of @{text rcong} correspond to left cosets.
+ Was there a mistake in the definitions? I'd have expected them to
+ correspond to right cosets.*}
+
+(* CB: This is correct, but subtle.
+ We call H #> a the right coset of a relative to H. According to
+ Jacobson, this is what the majority of group theory literature does.
+ He then defines the notion of congruence relation ~ over monoids as
+ equivalence relation with a ~ a' & b ~ b' \<Longrightarrow> a*b ~ a'*b'.
+ Our notion of right congruence induced by K: rcong K appears only in
+ the context where K is a normal subgroup. Jacobson doesn't name it.
+ But in this context left and right cosets are identical.
+*)
+
+lemma (in subgroup) l_coset_eq_rcong:
+ includes group G
+ assumes a: "a \<in> carrier G"
+ shows "a <# H = rcong H `` {a}"
+by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a )
subsubsection{*Two distinct right cosets are disjoint*}
lemma (in group) rcos_equation:
- "[|subgroup H G; a \<in> carrier G; b \<in> carrier G; ha \<otimes> a = h \<otimes> b;
- h \<in> H; ha \<in> H; hb \<in> H|]
- ==> \<exists>h\<in>H. h \<otimes> b = hb \<otimes> a"
-apply (rule bexI [of _"hb \<otimes> ((inv ha) \<otimes> h)"])
-apply (simp add: m_assoc transpose_inv subgroup.subset [THEN subsetD])
-apply (simp add: subgroup.m_closed subgroup.m_inv_closed)
+ includes subgroup H G
+ shows
+ "\<lbrakk>ha \<otimes> a = h \<otimes> b; a \<in> carrier G; b \<in> carrier G;
+ h \<in> H; ha \<in> H; hb \<in> H\<rbrakk>
+ \<Longrightarrow> hb \<otimes> a \<in> (\<Union>h\<in>H. {h \<otimes> b})"
+apply (rule UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"])
+apply (simp add: );
+apply (simp add: m_assoc transpose_inv)
done
lemma (in group) rcos_disjoint:
- "[|subgroup H G; a \<in> rcosets G H; b \<in> rcosets G H; a\<noteq>b|] ==> a \<inter> b = {}"
-apply (simp add: setrcos_eq r_coset_eq)
-apply (blast intro: rcos_equation sym)
+ includes subgroup H G
+ shows "\<lbrakk>a \<in> rcosets H; b \<in> rcosets H; a\<noteq>b\<rbrakk> \<Longrightarrow> a \<inter> b = {}"
+apply (simp add: RCOSETS_def r_coset_def)
+apply (blast intro: rcos_equation prems sym)
done
subsection {*Order of a Group and Lagrange's Theorem*}
constdefs
- order :: "('a, 'b) semigroup_scheme => nat"
- "order S == card (carrier S)"
+ order :: "('a, 'b) monoid_scheme \<Rightarrow> nat"
+ "order S \<equiv> card (carrier S)"
-lemma (in group) setrcos_part_G: "subgroup H G ==> \<Union>rcosets G H = carrier G"
+lemma (in group) rcos_self:
+ includes subgroup
+ shows "x \<in> carrier G \<Longrightarrow> x \<in> H #> x"
+apply (simp add: r_coset_def)
+apply (rule_tac x="\<one>" in bexI)
+apply (auto simp add: );
+done
+
+lemma (in group) rcosets_part_G:
+ includes subgroup
+ shows "\<Union>(rcosets H) = carrier G"
apply (rule equalityI)
-apply (force simp add: subgroup.subset [THEN subsetD]
- setrcos_eq r_coset_def)
-apply (auto simp add: setrcos_eq subgroup.subset rcos_self)
+ apply (force simp add: RCOSETS_def r_coset_def)
+apply (auto simp add: RCOSETS_def intro: rcos_self prems)
done
lemma (in group) cosets_finite:
- "[| c \<in> rcosets G H; H \<subseteq> carrier G; finite (carrier G) |] ==> finite c"
-apply (auto simp add: setrcos_eq)
-apply (simp (no_asm_simp) add: r_coset_subset_G [THEN finite_subset])
+ "\<lbrakk>c \<in> rcosets H; H \<subseteq> carrier G; finite (carrier G)\<rbrakk> \<Longrightarrow> finite c"
+apply (auto simp add: RCOSETS_def)
+apply (simp add: r_coset_subset_G [THEN finite_subset])
done
text{*The next two lemmas support the proof of @{text card_cosets_equal}.*}
lemma (in group) inj_on_f:
- "[|H \<subseteq> carrier G; a \<in> carrier G|] ==> inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
+ "\<lbrakk>H \<subseteq> carrier G; a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
apply (rule inj_onI)
apply (subgoal_tac "x \<in> carrier G & y \<in> carrier G")
prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])
@@ -394,13 +436,13 @@
done
lemma (in group) inj_on_g:
- "[|H \<subseteq> carrier G; a \<in> carrier G|] ==> inj_on (\<lambda>y. y \<otimes> a) H"
+ "\<lbrakk>H \<subseteq> carrier G; a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> a) H"
by (force simp add: inj_on_def subsetD)
lemma (in group) card_cosets_equal:
- "[| c \<in> rcosets G H; H \<subseteq> carrier G; finite(carrier G) |]
- ==> card c = card H"
-apply (auto simp add: setrcos_eq)
+ "\<lbrakk>c \<in> rcosets H; H \<subseteq> carrier G; finite(carrier G)\<rbrakk>
+ \<Longrightarrow> card c = card H"
+apply (auto simp add: RCOSETS_def)
apply (rule card_bij_eq)
apply (rule inj_on_f, assumption+)
apply (force simp add: m_assoc subsetD r_coset_def)
@@ -411,21 +453,21 @@
apply (blast intro: finite_subset)
done
-lemma (in group) setrcos_subset_PowG:
- "subgroup H G ==> rcosets G H \<subseteq> Pow(carrier G)"
-apply (simp add: setrcos_eq)
+lemma (in group) rcosets_subset_PowG:
+ "subgroup H G \<Longrightarrow> rcosets H \<subseteq> Pow(carrier G)"
+apply (simp add: RCOSETS_def)
apply (blast dest: r_coset_subset_G subgroup.subset)
done
theorem (in group) lagrange:
- "[| finite(carrier G); subgroup H G |]
- ==> card(rcosets G H) * card(H) = order(G)"
-apply (simp (no_asm_simp) add: order_def setrcos_part_G [symmetric])
+ "\<lbrakk>finite(carrier G); subgroup H G\<rbrakk>
+ \<Longrightarrow> card(rcosets H) * card(H) = order(G)"
+apply (simp (no_asm_simp) add: order_def rcosets_part_G [symmetric])
apply (subst mult_commute)
apply (rule card_partition)
- apply (simp add: setrcos_subset_PowG [THEN finite_subset])
- apply (simp add: setrcos_part_G)
+ apply (simp add: rcosets_subset_PowG [THEN finite_subset])
+ apply (simp add: rcosets_part_G)
apply (simp add: card_cosets_equal subgroup.subset)
apply (simp add: rcos_disjoint)
done
@@ -434,99 +476,85 @@
subsection {*Quotient Groups: Factorization of a Group*}
constdefs
- FactGroup :: "[('a,'b) monoid_scheme, 'a set] => ('a set) monoid"
+ FactGroup :: "[('a,'b) monoid_scheme, 'a set] \<Rightarrow> ('a set) monoid"
(infixl "Mod" 65)
--{*Actually defined for groups rather than monoids*}
- "FactGroup G H ==
- (| carrier = rcosets G H, mult = set_mult G, one = H |)"
+ "FactGroup G H \<equiv>
+ \<lparr>carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\<rparr>"
-lemma (in group) setmult_closed:
- "[| H <| G; K1 \<in> rcosets G H; K2 \<in> rcosets G H |]
- ==> K1 <#> K2 \<in> rcosets G H"
-by (auto simp add: normal_imp_subgroup [THEN subgroup.subset]
- rcos_sum setrcos_eq)
+lemma (in normal) setmult_closed:
+ "\<lbrakk>K1 \<in> rcosets H; K2 \<in> rcosets H\<rbrakk> \<Longrightarrow> K1 <#> K2 \<in> rcosets H"
+by (auto simp add: rcos_sum RCOSETS_def)
-lemma (in group) setinv_closed:
- "[| H <| G; K \<in> rcosets G H |] ==> set_inv G K \<in> rcosets G H"
-by (auto simp add: normal_imp_subgroup
- subgroup.subset rcos_inv
- setrcos_eq)
+lemma (in normal) setinv_closed:
+ "K \<in> rcosets H \<Longrightarrow> set_inv K \<in> rcosets H"
+by (auto simp add: rcos_inv RCOSETS_def)
-lemma (in group) setrcos_assoc:
- "[|H <| G; M1 \<in> rcosets G H; M2 \<in> rcosets G H; M3 \<in> rcosets G H|]
- ==> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
-by (auto simp add: setrcos_eq rcos_sum normal_imp_subgroup
- subgroup.subset m_assoc)
+lemma (in normal) rcosets_assoc:
+ "\<lbrakk>M1 \<in> rcosets H; M2 \<in> rcosets H; M3 \<in> rcosets H\<rbrakk>
+ \<Longrightarrow> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
+by (auto simp add: RCOSETS_def rcos_sum m_assoc)
-lemma (in group) subgroup_in_rcosets:
- "subgroup H G ==> H \<in> rcosets G H"
+lemma (in subgroup) subgroup_in_rcosets:
+ includes group G
+ shows "H \<in> rcosets H"
proof -
- assume sub: "subgroup H G"
- have "r_coset G H \<one> = H"
- by (rule coset_join2)
- (auto intro: sub subgroup.one_closed)
+ have "H #> \<one> = H"
+ by (rule coset_join2, auto)
then show ?thesis
- by (auto simp add: setrcos_eq)
+ by (auto simp add: RCOSETS_def)
qed
-lemma (in group) setrcos_inv_mult_group_eq:
- "[|H <| G; M \<in> rcosets G H|] ==> set_inv G M <#> M = H"
-by (auto simp add: setrcos_eq rcos_inv rcos_sum normal_imp_subgroup
- subgroup.subset)
-(*
-lemma (in group) factorgroup_is_magma:
- "H <| G ==> magma (G Mod H)"
- by rule (simp add: FactGroup_def coset.setmult_closed [OF is_coset])
+lemma (in normal) rcosets_inv_mult_group_eq:
+ "M \<in> rcosets H \<Longrightarrow> set_inv M <#> M = H"
+by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset prems)
-lemma (in group) factorgroup_semigroup_axioms:
- "H <| G ==> semigroup_axioms (G Mod H)"
- by rule (simp add: FactGroup_def coset.setrcos_assoc [OF is_coset]
- coset.setmult_closed [OF is_coset])
-*)
-theorem (in group) factorgroup_is_group:
- "H <| G ==> group (G Mod H)"
+theorem (in normal) factorgroup_is_group:
+ "group (G Mod H)"
apply (simp add: FactGroup_def)
apply (rule groupI)
apply (simp add: setmult_closed)
- apply (simp add: normal_imp_subgroup subgroup_in_rcosets)
- apply (simp add: restrictI setmult_closed setrcos_assoc)
+ apply (simp add: normal_imp_subgroup subgroup_in_rcosets [OF is_group])
+ apply (simp add: restrictI setmult_closed rcosets_assoc)
apply (simp add: normal_imp_subgroup
- subgroup_in_rcosets setrcos_mult_eq)
-apply (auto dest: setrcos_inv_mult_group_eq simp add: setinv_closed)
+ subgroup_in_rcosets rcosets_mult_eq)
+apply (auto dest: rcosets_inv_mult_group_eq simp add: setinv_closed)
done
lemma mult_FactGroup [simp]: "X \<otimes>\<^bsub>(G Mod H)\<^esub> X' = X <#>\<^bsub>G\<^esub> X'"
by (simp add: FactGroup_def)
-lemma (in group) inv_FactGroup:
- "N <| G ==> X \<in> carrier (G Mod N) ==> inv\<^bsub>G Mod N\<^esub> X = set_inv G X"
+lemma (in normal) inv_FactGroup:
+ "X \<in> carrier (G Mod H) \<Longrightarrow> inv\<^bsub>G Mod H\<^esub> X = set_inv X"
apply (rule group.inv_equality [OF factorgroup_is_group])
-apply (simp_all add: FactGroup_def setinv_closed setrcos_inv_mult_group_eq)
+apply (simp_all add: FactGroup_def setinv_closed rcosets_inv_mult_group_eq)
done
text{*The coset map is a homomorphism from @{term G} to the quotient group
- @{term "G Mod N"}*}
-lemma (in group) r_coset_hom_Mod:
- assumes N: "N <| G"
- shows "(r_coset G N) \<in> hom G (G Mod N)"
-by (simp add: FactGroup_def rcosets_def Pi_def hom_def rcos_sum N)
+ @{term "G Mod H"}*}
+lemma (in normal) r_coset_hom_Mod:
+ "(\<lambda>a. H #> a) \<in> hom G (G Mod H)"
+ by (auto simp add: FactGroup_def RCOSETS_def Pi_def hom_def rcos_sum)
+
+subsection{*The First Isomorphism Theorem*}
-subsection{*Quotienting by the Kernel of a Homomorphism*}
+text{*The quotient by the kernel of a homomorphism is isomorphic to the
+ range of that homomorphism.*}
constdefs
- kernel :: "('a, 'm) monoid_scheme => ('b, 'n) monoid_scheme =>
- ('a => 'b) => 'a set"
+ kernel :: "('a, 'm) monoid_scheme \<Rightarrow> ('b, 'n) monoid_scheme \<Rightarrow>
+ ('a \<Rightarrow> 'b) \<Rightarrow> 'a set"
--{*the kernel of a homomorphism*}
- "kernel G H h == {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}";
+ "kernel G H h \<equiv> {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}";
lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
-apply (rule group.subgroupI)
+apply (rule subgroup.intro)
apply (auto simp add: kernel_def group.intro prems)
done
text{*The kernel of a homomorphism is a normal subgroup*}
-lemma (in group_hom) normal_kernel: "(kernel G H h) <| G"
+lemma (in group_hom) normal_kernel: "(kernel G H h) \<lhd> G"
apply (simp add: group.normal_inv_iff subgroup_kernel group.intro prems)
apply (simp add: kernel_def)
done
@@ -538,9 +566,9 @@
from X
obtain g where "g \<in> carrier G"
and "X = kernel G H h #> g"
- by (auto simp add: FactGroup_def rcosets_def)
+ by (auto simp add: FactGroup_def RCOSETS_def)
thus ?thesis
- by (force simp add: kernel_def r_coset_def image_def intro: hom_one)
+ by (auto simp add: kernel_def r_coset_def image_def intro: hom_one)
qed
@@ -551,13 +579,14 @@
from X
obtain g where g: "g \<in> carrier G"
and "X = kernel G H h #> g"
- by (auto simp add: FactGroup_def rcosets_def)
- hence "h ` X = {h g}" by (force simp add: kernel_def r_coset_def image_def g)
+ by (auto simp add: FactGroup_def RCOSETS_def)
+ hence "h ` X = {h g}" by (auto simp add: kernel_def r_coset_def image_def g)
thus ?thesis by (auto simp add: g)
qed
lemma (in group_hom) FactGroup_hom:
- "(%X. contents (h`X)) \<in> hom (G Mod (kernel G H h)) H"
+ "(\<lambda>X. contents (h`X)) \<in> hom (G Mod (kernel G H h)) H"
+apply (simp add: hom_def FactGroup_contents_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
proof (simp add: hom_def funcsetI FactGroup_contents_mem, intro ballI)
fix X and X'
assume X: "X \<in> carrier (G Mod kernel G H h)"
@@ -566,7 +595,7 @@
obtain g and g'
where "g \<in> carrier G" and "g' \<in> carrier G"
and "X = kernel G H h #> g" and "X' = kernel G H h #> g'"
- by (auto simp add: FactGroup_def rcosets_def)
+ by (auto simp add: FactGroup_def RCOSETS_def)
hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'"
and Xsub: "X \<subseteq> carrier G" and X'sub: "X' \<subseteq> carrier G"
by (force simp add: kernel_def r_coset_def image_def)+
@@ -578,10 +607,11 @@
by (simp add: all image_eq_UN FactGroup_nonempty X X')
qed
+
text{*Lemma for the following injectivity result*}
lemma (in group_hom) FactGroup_subset:
- "[|g \<in> carrier G; g' \<in> carrier G; h g = h g'|]
- ==> kernel G H h #> g \<subseteq> kernel G H h #> g'"
+ "\<lbrakk>g \<in> carrier G; g' \<in> carrier G; h g = h g'\<rbrakk>
+ \<Longrightarrow> kernel G H h #> g \<subseteq> kernel G H h #> g'"
apply (clarsimp simp add: kernel_def r_coset_def image_def);
apply (rename_tac y)
apply (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI)
@@ -598,7 +628,7 @@
obtain g and g'
where gX: "g \<in> carrier G" "g' \<in> carrier G"
"X = kernel G H h #> g" "X' = kernel G H h #> g'"
- by (auto simp add: FactGroup_def rcosets_def)
+ by (auto simp add: FactGroup_def RCOSETS_def)
hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'"
by (force simp add: kernel_def r_coset_def image_def)+
assume "contents (h ` X) = contents (h ` X')"
@@ -624,7 +654,7 @@
hence "(\<Union>\<^bsub>x\<in>kernel G H h #> g\<^esub> {h x}) = {y}"
by (auto simp add: y kernel_def r_coset_def)
with g show "y \<in> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)"
- by (auto intro!: bexI simp add: FactGroup_def rcosets_def image_eq_UN)
+ by (auto intro!: bexI simp add: FactGroup_def RCOSETS_def image_eq_UN)
qed
qed
@@ -633,8 +663,9 @@
quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
theorem (in group_hom) FactGroup_iso:
"h ` carrier G = carrier H
- \<Longrightarrow> (%X. contents (h`X)) \<in> (G Mod (kernel G H h)) \<cong> H"
+ \<Longrightarrow> (\<lambda>X. contents (h`X)) \<in> (G Mod (kernel G H h)) \<cong> H"
by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def
FactGroup_onto)
+
end
--- a/src/HOL/Algebra/Group.thy Thu Jun 17 14:27:01 2004 +0200
+++ b/src/HOL/Algebra/Group.thy Thu Jun 17 17:18:30 2004 +0200
@@ -11,21 +11,17 @@
theory Group = FuncSet + Lattice:
-section {* From Magmas to Groups *}
+section {* Monoids and Groups *}
text {*
- Definitions follow \cite{Jacobson:1985}; with the exception of
- \emph{magma} which, following Bourbaki, is a set together with a
- binary, closed operation.
+ Definitions follow \cite{Jacobson:1985}.
*}
subsection {* Definitions *}
-record 'a semigroup = "'a partial_object" +
- mult :: "['a, 'a] => 'a" (infixl "\<otimes>\<index>" 70)
-
-record 'a monoid = "'a semigroup" +
- one :: 'a ("\<one>\<index>")
+record 'a monoid = "'a partial_object" +
+ mult :: "['a, 'a] \<Rightarrow> 'a" (infixl "\<otimes>\<index>" 70)
+ one :: 'a ("\<one>\<index>")
constdefs (structure G)
m_inv :: "('a, 'b) monoid_scheme => 'a => 'a" ("inv\<index> _" [81] 80)
@@ -33,7 +29,7 @@
Units :: "_ => 'a set"
--{*The set of invertible elements*}
- "Units G == {y. y \<in> carrier G & (EX x : carrier G. x \<otimes> y = \<one> & y \<otimes> x = \<one>)}"
+ "Units G == {y. y \<in> carrier G & (\<exists>x \<in> carrier G. x \<otimes> y = \<one> & y \<otimes> x = \<one>)}"
consts
pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75)
@@ -44,19 +40,15 @@
let p = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a)
in if neg z then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z)"
-locale magma = struct G +
+locale monoid = struct G +
assumes m_closed [intro, simp]:
- "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
-
-locale semigroup = magma +
- assumes m_assoc:
- "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
- (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
-
-locale monoid = semigroup +
- assumes one_closed [intro, simp]: "\<one> \<in> carrier G"
- and l_one [simp]: "x \<in> carrier G ==> \<one> \<otimes> x = x"
- and r_one [simp]: "x \<in> carrier G ==> x \<otimes> \<one> = x"
+ "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> carrier G"
+ and m_assoc:
+ "\<lbrakk>x \<in> carrier G; y \<in> carrier G; z \<in> carrier G\<rbrakk>
+ \<Longrightarrow> (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
+ and one_closed [intro, simp]: "\<one> \<in> carrier G"
+ and l_one [simp]: "x \<in> carrier G \<Longrightarrow> \<one> \<otimes> x = x"
+ and r_one [simp]: "x \<in> carrier G \<Longrightarrow> x \<otimes> \<one> = x"
lemma monoidI:
includes struct G
@@ -69,9 +61,7 @@
and l_one: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x"
and r_one: "!!x. x \<in> carrier G ==> x \<otimes> \<one> = x"
shows "monoid G"
- by (fast intro!: monoid.intro magma.intro semigroup_axioms.intro
- semigroup.intro monoid_axioms.intro
- intro: prems)
+ by (fast intro!: monoid.intro intro: prems)
lemma (in monoid) Units_closed [dest]:
"x \<in> Units G ==> x \<in> carrier G"
@@ -210,7 +200,7 @@
"!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
and l_one [simp]: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x"
- and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. y \<otimes> x = \<one>"
+ and l_inv_ex: "!!x. x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>"
shows "group G"
proof -
have l_cancel [simp]:
@@ -243,7 +233,7 @@
with x xG show "x \<otimes> \<one> = x" by simp
qed
have inv_ex:
- "!!x. x \<in> carrier G ==> EX y : carrier G. y \<otimes> x = \<one> & x \<otimes> y = \<one>"
+ "!!x. x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one> & x \<otimes> y = \<one>"
proof -
fix x
assume x: "x \<in> carrier G"
@@ -253,20 +243,19 @@
by (simp add: m_assoc [symmetric] l_inv r_one)
with x y have r_inv: "x \<otimes> y = \<one>"
by simp
- from x y show "EX y : carrier G. y \<otimes> x = \<one> & x \<otimes> y = \<one>"
+ from x y show "\<exists>y \<in> carrier G. y \<otimes> x = \<one> & x \<otimes> y = \<one>"
by (fast intro: l_inv r_inv)
qed
then have carrier_subset_Units: "carrier G <= Units G"
by (unfold Units_def) fast
show ?thesis
- by (fast intro!: group.intro magma.intro semigroup_axioms.intro
- semigroup.intro monoid_axioms.intro group_axioms.intro
+ by (fast intro!: group.intro monoid.intro group_axioms.intro
carrier_subset_Units intro: prems r_one)
qed
lemma (in monoid) monoid_groupI:
assumes l_inv_ex:
- "!!x. x \<in> carrier G ==> EX y : carrier G. y \<otimes> x = \<one>"
+ "!!x. x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>"
shows "group G"
by (rule groupI) (auto intro: m_assoc l_inv_ex)
@@ -282,7 +271,7 @@
"x \<in> carrier G ==> inv x \<in> carrier G"
using Units_inv_closed by simp
-lemma (in group) l_inv:
+lemma (in group) l_inv [simp]:
"x \<in> carrier G ==> inv x \<otimes> x = \<one>"
using Units_l_inv by simp
@@ -293,7 +282,7 @@
(x \<otimes> y = x \<otimes> z) = (y = z)"
using Units_l_inv by simp
-lemma (in group) r_inv:
+lemma (in group) r_inv [simp]:
"x \<in> carrier G ==> x \<otimes> inv x = \<one>"
proof -
assume x: "x \<in> carrier G"
@@ -309,8 +298,8 @@
assume eq: "y \<otimes> x = z \<otimes> x"
and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
then have "y \<otimes> (x \<otimes> inv x) = z \<otimes> (x \<otimes> inv x)"
- by (simp add: m_assoc [symmetric])
- with G show "y = z" by (simp add: r_inv)
+ by (simp add: m_assoc [symmetric] del: r_inv)
+ with G show "y = z" by simp
next
assume eq: "y = z"
and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
@@ -320,8 +309,8 @@
lemma (in group) inv_one [simp]:
"inv \<one> = \<one>"
proof -
- have "inv \<one> = \<one> \<otimes> (inv \<one>)" by simp
- moreover have "... = \<one>" by (simp add: r_inv)
+ have "inv \<one> = \<one> \<otimes> (inv \<one>)" by (simp del: r_inv)
+ moreover have "... = \<one>" by simp
finally show ?thesis .
qed
@@ -338,8 +327,8 @@
proof -
assume G: "x \<in> carrier G" "y \<in> carrier G"
then have "inv (x \<otimes> y) \<otimes> (x \<otimes> y) = (inv y \<otimes> inv x) \<otimes> (x \<otimes> y)"
- by (simp add: m_assoc l_inv) (simp add: m_assoc [symmetric] l_inv)
- with G show ?thesis by simp
+ by (simp add: m_assoc l_inv) (simp add: m_assoc [symmetric])
+ with G show ?thesis by (simp del: l_inv)
qed
lemma (in group) inv_comm:
@@ -368,54 +357,28 @@
"\<one> (^) (z::int) = \<one>"
by (simp add: int_pow_def2)
-subsection {* Substructures *}
-
-locale submagma = var H + struct G +
- assumes subset [intro, simp]: "H \<subseteq> carrier G"
- and m_closed [intro, simp]: "[| x \<in> H; y \<in> H |] ==> x \<otimes> y \<in> H"
-
-declare (in submagma) magma.intro [intro] semigroup.intro [intro]
- semigroup_axioms.intro [intro]
-
-lemma submagma_imp_subset:
- "submagma H G ==> H \<subseteq> carrier G"
- by (rule submagma.subset)
-
-lemma (in submagma) subsetD [dest, simp]:
- "x \<in> H ==> x \<in> carrier G"
- using subset by blast
+subsection {* Subgroups *}
-lemma (in submagma) magmaI [intro]:
- includes magma G
- shows "magma (G(| carrier := H |))"
- by rule simp
-
-lemma (in submagma) semigroup_axiomsI [intro]:
- includes semigroup G
- shows "semigroup_axioms (G(| carrier := H |))"
- by rule (simp add: m_assoc)
-
-lemma (in submagma) semigroupI [intro]:
- includes semigroup G
- shows "semigroup (G(| carrier := H |))"
- using prems by fast
-
-
-locale subgroup = submagma H G +
- assumes one_closed [intro, simp]: "\<one> \<in> H"
- and m_inv_closed [intro, simp]: "x \<in> H ==> inv x \<in> H"
+locale subgroup = var H + struct G +
+ assumes subset: "H \<subseteq> carrier G"
+ and m_closed [intro, simp]: "\<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> H"
+ and one_closed [simp]: "\<one> \<in> H"
+ and m_inv_closed [intro,simp]: "x \<in> H \<Longrightarrow> inv x \<in> H"
declare (in subgroup) group.intro [intro]
-lemma (in subgroup) group_axiomsI [intro]:
- includes group G
- shows "group_axioms (G(| carrier := H |))"
- by (rule group_axioms.intro) (auto intro: l_inv r_inv simp add: Units_def)
+lemma (in subgroup) mem_carrier [simp]:
+ "x \<in> H \<Longrightarrow> x \<in> carrier G"
+ using subset by blast
-lemma (in subgroup) groupI [intro]:
+lemma subgroup_imp_subset:
+ "subgroup H G \<Longrightarrow> H \<subseteq> carrier G"
+ by (rule subgroup.subset)
+
+lemma (in subgroup) subgroup_is_group [intro]:
includes group G
- shows "group (G(| carrier := H |))"
- by (rule groupI) (auto intro: m_assoc l_inv)
+ shows "group (G\<lparr>carrier := H\<rparr>)"
+ by (rule groupI) (auto intro: m_assoc l_inv mem_carrier)
text {*
Since @{term H} is nonempty, it contains some element @{term x}. Since
@@ -432,31 +395,13 @@
lemma (in group) subgroupI:
assumes subset: "H \<subseteq> carrier G" and non_empty: "H \<noteq> {}"
- and inv: "!!a. a \<in> H ==> inv a \<in> H"
- and mult: "!!a b. [|a \<in> H; b \<in> H|] ==> a \<otimes> b \<in> H"
+ and inv: "!!a. a \<in> H \<Longrightarrow> inv a \<in> H"
+ and mult: "!!a b. \<lbrakk>a \<in> H; b \<in> H\<rbrakk> \<Longrightarrow> a \<otimes> b \<in> H"
shows "subgroup H G"
-proof (rule subgroup.intro)
- from subset and mult show "submagma H G" by (rule submagma.intro)
-next
- have "\<one> \<in> H" by (rule one_in_subset) (auto simp only: prems)
- with inv show "subgroup_axioms H G"
- by (intro subgroup_axioms.intro) simp_all
+proof (simp add: subgroup_def prems)
+ show "\<one> \<in> H" by (rule one_in_subset) (auto simp only: prems)
qed
-text {*
- Repeat facts of submagmas for subgroups. Necessary???
-*}
-
-lemma (in subgroup) subset:
- "H \<subseteq> carrier G"
- ..
-
-lemma (in subgroup) m_closed:
- "[| x \<in> H; y \<in> H |] ==> x \<otimes> y \<in> H"
- ..
-
-declare magma.m_closed [simp]
-
declare monoid.one_closed [iff] group.inv_closed [simp]
monoid.l_one [simp] monoid.r_one [simp] group.inv_inv [simp]
@@ -467,11 +412,9 @@
lemma (in subgroup) finite_imp_card_positive:
"finite (carrier G) ==> 0 < card H"
proof (rule classical)
- have sub: "subgroup H G" using prems by (rule subgroup.intro)
- assume fin: "finite (carrier G)"
- and zero: "~ 0 < card H"
- then have "finite H" by (blast intro: finite_subset dest: subset)
- with zero sub have "subgroup {} G" by simp
+ assume "finite (carrier G)" "~ 0 < card H"
+ then have "finite H" by (blast intro: finite_subset [OF subset])
+ with prems have "subgroup {} G" by simp
with subgroup_nonempty show ?thesis by contradiction
qed
@@ -482,83 +425,67 @@
subsection {* Direct Products *}
-constdefs (structure G and H)
- DirProdSemigroup :: "_ => _ => ('a \<times> 'b) semigroup" (infixr "\<times>\<^sub>s" 80)
- "G \<times>\<^sub>s H == (| carrier = carrier G \<times> carrier H,
- mult = (%(g, h) (g', h'). (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')) |)"
-
- DirProdGroup :: "_ => _ => ('a \<times> 'b) monoid" (infixr "\<times>\<^sub>g" 80)
- "G \<times>\<^sub>g H == semigroup.extend (G \<times>\<^sub>s H) (| one = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>) |)"
-
-lemma DirProdSemigroup_magma:
- includes magma G + magma H
- shows "magma (G \<times>\<^sub>s H)"
- by (rule magma.intro) (auto simp add: DirProdSemigroup_def)
+constdefs
+ DirProd :: "_ \<Rightarrow> _ \<Rightarrow> ('a \<times> 'b) monoid" (infixr "\<times>\<times>" 80)
+ "G \<times>\<times> H \<equiv> \<lparr>carrier = carrier G \<times> carrier H,
+ mult = (\<lambda>(g, h) (g', h'). (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')),
+ one = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)\<rparr>"
-lemma DirProdSemigroup_semigroup_axioms:
- includes semigroup G + semigroup H
- shows "semigroup_axioms (G \<times>\<^sub>s H)"
- by (rule semigroup_axioms.intro)
- (auto simp add: DirProdSemigroup_def G.m_assoc H.m_assoc)
+lemma DirProd_monoid:
+ includes monoid G + monoid H
+ shows "monoid (G \<times>\<times> H)"
+proof -
+ from prems
+ show ?thesis by (unfold monoid_def DirProd_def, auto)
+qed
-lemma DirProdSemigroup_semigroup:
- includes semigroup G + semigroup H
- shows "semigroup (G \<times>\<^sub>s H)"
- using prems
- by (fast intro: semigroup.intro
- DirProdSemigroup_magma DirProdSemigroup_semigroup_axioms)
-
-lemma DirProdGroup_magma:
- includes magma G + magma H
- shows "magma (G \<times>\<^sub>g H)"
- by (rule magma.intro)
- (auto simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
-lemma DirProdGroup_semigroup_axioms:
- includes semigroup G + semigroup H
- shows "semigroup_axioms (G \<times>\<^sub>g H)"
- by (rule semigroup_axioms.intro)
- (auto simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs
- G.m_assoc H.m_assoc)
-
-lemma DirProdGroup_semigroup:
- includes semigroup G + semigroup H
- shows "semigroup (G \<times>\<^sub>g H)"
- using prems
- by (fast intro: semigroup.intro
- DirProdGroup_magma DirProdGroup_semigroup_axioms)
-
-text {* \dots\ and further lemmas for group \dots *}
-
-lemma DirProdGroup_group:
+text{*Does not use the previous result because it's easier just to use auto.*}
+lemma DirProd_group:
includes group G + group H
- shows "group (G \<times>\<^sub>g H)"
+ shows "group (G \<times>\<times> H)"
by (rule groupI)
- (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
- simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
+ (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
+ simp add: DirProd_def)
-lemma carrier_DirProdGroup [simp]:
- "carrier (G \<times>\<^sub>g H) = carrier G \<times> carrier H"
- by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
+lemma carrier_DirProd [simp]:
+ "carrier (G \<times>\<times> H) = carrier G \<times> carrier H"
+ by (simp add: DirProd_def)
-lemma one_DirProdGroup [simp]:
- "\<one>\<^bsub>(G \<times>\<^sub>g H)\<^esub> = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)"
- by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
+lemma one_DirProd [simp]:
+ "\<one>\<^bsub>G \<times>\<times> H\<^esub> = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)"
+ by (simp add: DirProd_def)
-lemma mult_DirProdGroup [simp]:
- "(g, h) \<otimes>\<^bsub>(G \<times>\<^sub>g H)\<^esub> (g', h') = (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')"
- by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
+lemma mult_DirProd [simp]:
+ "(g, h) \<otimes>\<^bsub>(G \<times>\<times> H)\<^esub> (g', h') = (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')"
+ by (simp add: DirProd_def)
-lemma inv_DirProdGroup [simp]:
+lemma inv_DirProd [simp]:
includes group G + group H
assumes g: "g \<in> carrier G"
and h: "h \<in> carrier H"
- shows "m_inv (G \<times>\<^sub>g H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
- apply (rule group.inv_equality [OF DirProdGroup_group])
+ shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
+ apply (rule group.inv_equality [OF DirProd_group])
apply (simp_all add: prems group_def group.l_inv)
done
-subsection {* Isomorphisms *}
+text{*This alternative proof of the previous result demonstrates instantiate.
+ It uses @{text Prod.inv_equality} (available after instantiation) instead of
+ @{text "group.inv_equality [OF DirProd_group]"}. *}
+lemma
+ includes group G + group H
+ assumes g: "g \<in> carrier G"
+ and h: "h \<in> carrier H"
+ shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
+proof -
+ have "group (G \<times>\<times> H)"
+ by (blast intro: DirProd_group group.intro prems)
+ then instantiate Prod: group
+ show ?thesis by (simp add: Prod.inv_equality g h)
+qed
+
+
+subsection {* Homomorphisms and Isomorphisms *}
constdefs (structure G and H)
hom :: "_ => _ => ('a => 'b) set"
@@ -566,16 +493,6 @@
{h. h \<in> carrier G -> carrier H &
(\<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)}"
-lemma (in semigroup) hom:
- "semigroup (| carrier = hom G G, mult = op o |)"
-proof (rule semigroup.intro)
- show "magma (| carrier = hom G G, mult = op o |)"
- by (rule magma.intro) (simp add: Pi_def hom_def)
-next
- show "semigroup_axioms (| carrier = hom G G, mult = op o |)"
- by (rule semigroup_axioms.intro) (simp add: o_assoc)
-qed
-
lemma hom_mult:
"[| h \<in> hom G H; x \<in> carrier G; y \<in> carrier G |]
==> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
@@ -613,15 +530,17 @@
"[|h \<in> G \<cong> H; i \<in> H \<cong> I|] ==> (compose (carrier G) i h) \<in> G \<cong> I"
by (auto simp add: iso_def hom_compose bij_betw_compose)
-lemma DirProdGroup_commute_iso:
- shows "(%(x,y). (y,x)) \<in> (G \<times>\<^sub>g H) \<cong> (H \<times>\<^sub>g G)"
+lemma DirProd_commute_iso:
+ shows "(\<lambda>(x,y). (y,x)) \<in> (G \<times>\<times> H) \<cong> (H \<times>\<times> G)"
by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
-lemma DirProdGroup_assoc_iso:
- 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))"
+lemma DirProd_assoc_iso:
+ shows "(\<lambda>(x,y,z). (x,(y,z))) \<in> (G \<times>\<times> H \<times>\<times> I) \<cong> (G \<times>\<times> (H \<times>\<times> I))"
by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
+text{*Basis for homomorphism proofs: we assume two groups @{term G} and
+ @term{H}, with a homomorphism @{term h} between them*}
locale group_hom = group G + group H + var h +
assumes homh: "h \<in> hom G H"
notes hom_mult [simp] = hom_mult [OF homh]
@@ -648,11 +567,11 @@
proof -
assume x: "x \<in> carrier G"
then have "h x \<otimes>\<^bsub>H\<^esub> h (inv x) = \<one>\<^bsub>H\<^esub>"
- by (simp add: hom_mult [symmetric] G.r_inv del: hom_mult)
+ by (simp add: hom_mult [symmetric] del: hom_mult)
also from x have "... = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)"
- by (simp add: hom_mult [symmetric] H.r_inv del: hom_mult)
+ by (simp add: hom_mult [symmetric] del: hom_mult)
finally have "h x \<otimes>\<^bsub>H\<^esub> h (inv x) = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)" .
- with x show ?thesis by simp
+ with x show ?thesis by (simp del: H.r_inv)
qed
subsection {* Commutative Structures *}
@@ -665,11 +584,11 @@
subsection {* Definition *}
-locale comm_semigroup = semigroup +
- assumes m_comm: "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
+locale comm_monoid = monoid +
+ assumes m_comm: "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> x \<otimes> y = y \<otimes> x"
-lemma (in comm_semigroup) m_lcomm:
- "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
+lemma (in comm_monoid) m_lcomm:
+ "\<lbrakk>x \<in> carrier G; y \<in> carrier G; z \<in> carrier G\<rbrakk> \<Longrightarrow>
x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)"
proof -
assume xyz: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
@@ -679,9 +598,7 @@
finally show ?thesis .
qed
-lemmas (in comm_semigroup) m_ac = m_assoc m_comm m_lcomm
-
-locale comm_monoid = comm_semigroup + monoid
+lemmas (in comm_monoid) m_ac = m_assoc m_comm m_lcomm
lemma comm_monoidI:
includes struct G
@@ -696,15 +613,15 @@
"!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
shows "comm_monoid G"
using l_one
- by (auto intro!: comm_monoid.intro magma.intro semigroup_axioms.intro
- comm_semigroup_axioms.intro monoid_axioms.intro
- intro: prems simp: m_closed one_closed m_comm)
+ by (auto intro!: comm_monoid.intro comm_monoid_axioms.intro monoid.intro
+ intro: prems simp: m_closed one_closed m_comm)
lemma (in monoid) monoid_comm_monoidI:
assumes m_comm:
"!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
shows "comm_monoid G"
by (rule comm_monoidI) (auto intro: m_assoc m_comm)
+
(*lemma (in comm_monoid) r_one [simp]:
"x \<in> carrier G ==> x \<otimes> \<one> = x"
proof -
@@ -713,6 +630,7 @@
also from G have "... = x" by simp
finally show ?thesis .
qed*)
+
lemma (in comm_monoid) nat_pow_distr:
"[| x \<in> carrier G; y \<in> carrier G |] ==>
(x \<otimes> y) (^) (n::nat) = x (^) n \<otimes> y (^) n"
@@ -724,7 +642,7 @@
assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
x \<otimes> y = y \<otimes> x"
shows "comm_group G"
- by (fast intro: comm_group.intro comm_semigroup_axioms.intro
+ by (fast intro: comm_group.intro comm_monoid_axioms.intro
is_group prems)
lemma comm_groupI:
@@ -738,7 +656,7 @@
and m_comm:
"!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
and l_one: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x"
- and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. y \<otimes> x = \<one>"
+ and l_inv_ex: "!!x. x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>"
shows "comm_group G"
by (fast intro: group.group_comm_groupI groupI prems)
@@ -760,11 +678,11 @@
lemma (in group) subgroup_imp_group:
"subgroup H G ==> group (G(| carrier := H |))"
- using subgroup.groupI [OF _ group.intro] .
+ using subgroup.subgroup_is_group [OF _ group.intro] .
lemma (in group) is_monoid [intro, simp]:
"monoid G"
- by (rule monoid.intro)
+ by (auto intro: monoid.intro m_assoc)
lemma (in group) subgroup_inv_equality:
"[| subgroup H G; x \<in> H |] ==> m_inv (G (| carrier := H |)) x = inv x"
@@ -803,7 +721,7 @@
next
have "greatest ?L (carrier G) (carrier ?L)"
by (unfold greatest_def) (simp add: subgroup.subset subgroup_self)
- then show "EX G. greatest ?L G (carrier ?L)" ..
+ then show "\<exists>G. greatest ?L G (carrier ?L)" ..
next
fix A
assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}"
@@ -815,7 +733,6 @@
fix H
assume H: "H \<in> A"
with L have subgroupH: "subgroup H G" by auto
- from subgroupH have submagmaH: "submagma H G" by (rule subgroup.axioms)
from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H")
by (rule subgroup_imp_group)
from groupH have monoidH: "monoid ?H"
@@ -831,7 +748,7 @@
next
show "?Int \<in> carrier ?L" by simp (rule Int_subgroup)
qed
- then show "EX I. greatest ?L I (Lower ?L A)" ..
+ then show "\<exists>I. greatest ?L I (Lower ?L A)" ..
qed
end
--- a/src/HOL/Algebra/Sylow.thy Thu Jun 17 14:27:01 2004 +0200
+++ b/src/HOL/Algebra/Sylow.thy Thu Jun 17 17:18:30 2004 +0200
@@ -206,7 +206,7 @@
lemma (in sylow_central) M1_cardeq_rcosetGM1g:
"g \<in> carrier G ==> card(M1 #> g) = card(M1)"
-by (simp (no_asm_simp) add: M1_subset_G card_cosets_equal setrcosI)
+by (simp (no_asm_simp) add: M1_subset_G card_cosets_equal rcosetsI)
lemma (in sylow_central) M1_RelM_rcosetGM1g:
"g \<in> carrier G ==> (M1, M1 #> g) \<in> RelM"
@@ -219,16 +219,14 @@
done
+subsection{*Equal Cardinalities of @{term M} and the Set of Cosets*}
-subsection{*Equal Cardinalities of @{term M} and @{term "rcosets G H"}*}
-
-text{*Injections between @{term M} and @{term "rcosets G H"} show that
+text{*Injections between @{term M} and @{term "rcosets\<^bsub>G\<^esub> H"} show that
their cardinalities are equal.*}
lemma ElemClassEquiv:
- "[| equiv A r; C\<in>A // r |] ==> \<forall>x \<in> C. \<forall>y \<in> C. (x,y)\<in>r"
-apply (unfold equiv_def quotient_def sym_def trans_def, blast)
-done
+ "[| equiv A r; C \<in> A // r |] ==> \<forall>x \<in> C. \<forall>y \<in> C. (x,y)\<in>r"
+by (unfold equiv_def quotient_def sym_def trans_def, blast)
lemma (in sylow_central) M_elem_map:
"M2 \<in> M ==> \<exists>g. g \<in> carrier G & M1 #> g = M2"
@@ -243,16 +241,16 @@
lemmas (in sylow_central) M_elem_map_eq =
M_elem_map [THEN someI_ex, THEN conjunct2]
-lemma (in sylow_central) M_funcset_setrcos_H:
- "(%x:M. H #> (SOME g. g \<in> carrier G & M1 #> g = x)) \<in> M \<rightarrow> rcosets G H"
-apply (rule setrcosI [THEN restrictI])
+lemma (in sylow_central) M_funcset_rcosets_H:
+ "(%x:M. H #> (SOME g. g \<in> carrier G & M1 #> g = x)) \<in> M \<rightarrow> rcosets H"
+apply (rule rcosetsI [THEN restrictI])
apply (rule H_is_subgroup [THEN subgroup.subset])
apply (erule M_elem_map_carrier)
done
-lemma (in sylow_central) inj_M_GmodH: "\<exists>f \<in> M\<rightarrow>rcosets G H. inj_on f M"
+lemma (in sylow_central) inj_M_GmodH: "\<exists>f \<in> M\<rightarrow>rcosets H. inj_on f M"
apply (rule bexI)
-apply (rule_tac [2] M_funcset_setrcos_H)
+apply (rule_tac [2] M_funcset_rcosets_H)
apply (rule inj_onI, simp)
apply (rule trans [OF _ M_elem_map_eq])
prefer 2 apply assumption
@@ -267,11 +265,11 @@
done
-(** the opposite injection **)
+subsubsection{*The opposite injection*}
lemma (in sylow_central) H_elem_map:
- "H1\<in>rcosets G H ==> \<exists>g. g \<in> carrier G & H #> g = H1"
-by (auto simp add: setrcos_eq)
+ "H1 \<in> rcosets H ==> \<exists>g. g \<in> carrier G & H #> g = H1"
+by (auto simp add: RCOSETS_def)
lemmas (in sylow_central) H_elem_map_carrier =
H_elem_map [THEN someI_ex, THEN conjunct1]
@@ -281,14 +279,13 @@
lemma EquivElemClass:
- "[|equiv A r; M\<in>A // r; M1\<in>M; (M1, M2)\<in>r |] ==> M2\<in>M"
-apply (unfold equiv_def quotient_def sym_def trans_def, blast)
-done
+ "[|equiv A r; M \<in> A//r; M1\<in>M; (M1,M2) \<in> r |] ==> M2 \<in> M"
+by (unfold equiv_def quotient_def sym_def trans_def, blast)
+
-lemma (in sylow_central) setrcos_H_funcset_M:
- "(\<lambda>C \<in> rcosets G H. M1 #> (@g. g \<in> carrier G \<and> H #> g = C))
- \<in> rcosets G H \<rightarrow> M"
-apply (simp add: setrcos_eq)
+lemma (in sylow_central) rcosets_H_funcset_M:
+ "(\<lambda>C \<in> rcosets H. M1 #> (@g. g \<in> carrier G \<and> H #> g = C)) \<in> rcosets H \<rightarrow> M"
+apply (simp add: RCOSETS_def)
apply (fast intro: someI2
intro!: restrictI M1_in_M
EquivElemClass [OF RelM_equiv M_in_quot _ M1_RelM_rcosetGM1g])
@@ -296,9 +293,9 @@
text{*close to a duplicate of @{text inj_M_GmodH}*}
lemma (in sylow_central) inj_GmodH_M:
- "\<exists>g \<in> rcosets G H\<rightarrow>M. inj_on g (rcosets G H)"
+ "\<exists>g \<in> rcosets H\<rightarrow>M. inj_on g (rcosets H)"
apply (rule bexI)
-apply (rule_tac [2] setrcos_H_funcset_M)
+apply (rule_tac [2] rcosets_H_funcset_M)
apply (rule inj_onI)
apply (simp)
apply (rule trans [OF _ H_elem_map_eq])
@@ -323,10 +320,10 @@
apply (rule calM_subset_PowG, blast)
done
-lemma (in sylow_central) cardMeqIndexH: "card(M) = card(rcosets G H)"
+lemma (in sylow_central) cardMeqIndexH: "card(M) = card(rcosets H)"
apply (insert inj_M_GmodH inj_GmodH_M)
apply (blast intro: card_bij finite_M H_is_subgroup
- setrcos_subset_PowG [THEN finite_subset]
+ rcosets_subset_PowG [THEN finite_subset]
finite_Pow_iff [THEN iffD2])
done
@@ -373,3 +370,4 @@
done
end
+
--- a/src/HOL/Algebra/UnivPoly.thy Thu Jun 17 14:27:01 2004 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Thu Jun 17 17:18:30 2004 +0200
@@ -402,11 +402,6 @@
UP_cring)
(* TODO: provide cring.is_monoid *)
-lemma (in UP_cring) UP_comm_semigroup:
- "comm_semigroup P"
- by (fast intro!: cring.is_comm_monoid comm_monoid.axioms comm_semigroup.intro
- UP_cring)
-
lemma (in UP_cring) UP_comm_monoid:
"comm_monoid P"
by (fast intro!: cring.is_comm_monoid UP_cring)
@@ -441,7 +436,7 @@
monoid.nat_pow_pow [OF UP_monoid]
lemmas (in UP_cring) UP_m_lcomm =
- comm_semigroup.m_lcomm [OF UP_comm_semigroup]
+ comm_monoid.m_lcomm [OF UP_comm_monoid]
lemmas (in UP_cring) UP_m_ac = UP_m_assoc UP_m_comm UP_m_lcomm
--- a/src/HOL/Algebra/ringsimp.ML Thu Jun 17 14:27:01 2004 +0200
+++ b/src/HOL/Algebra/ringsimp.ML Thu Jun 17 17:18:30 2004 +0200
@@ -57,7 +57,7 @@
fun ring_ord a =
find_index_eq a ["CRing.ring.zero", "CRing.ring.add", "CRing.a_inv",
- "CRing.minus", "Group.monoid.one", "Group.semigroup.mult"];
+ "CRing.minus", "Group.monoid.one", "Group.monoid.mult"];
fun termless_ring (a, b) = (term_lpo ring_ord (a, b) = LESS);
@@ -69,7 +69,7 @@
| _ => [])
handle TERM _ => [];
fun comm_filter t = (case HOLogic.dest_Trueprop t of
- Const ("Group.comm_semigroup_axioms", _) $ Free (s, _) => [s]
+ Const ("Group.comm_monoid_axioms", _) $ Free (s, _) => [s]
| _ => [])
handle TERM _ => [];