summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Algebra/Group.thy

author | nipkow |

Fri, 13 Nov 2009 14:14:04 +0100 | |

changeset 33657 | a4179bf442d1 |

parent 33057 | 764547b68538 |

child 35416 | d8d7d1b785af |

permissions | -rw-r--r-- |

renamed lemmas "anti_sym" -> "antisym"

(* Title: HOL/Algebra/Group.thy Author: Clemens Ballarin, started 4 February 2003 Based on work by Florian Kammueller, L C Paulson and Markus Wenzel. *) theory Group imports Lattice FuncSet begin section {* Monoids and Groups *} subsection {* Definitions *} text {* Definitions follow \cite{Jacobson:1985}. *} 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) "inv x == (THE y. y \<in> carrier G & x \<otimes> y = \<one> & y \<otimes> x = \<one>)" Units :: "_ => 'a set" --{*The set of invertible elements*} "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) defs (overloaded) nat_pow_def: "pow G a n == nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) n" int_pow_def: "pow G a z == 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 monoid = fixes G (structure) assumes m_closed [intro, simp]: "\<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: fixes G (structure) assumes m_closed: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G" and one_closed: "\<one> \<in> carrier G" and m_assoc: "!!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: "!!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 intro: assms) lemma (in monoid) Units_closed [dest]: "x \<in> Units G ==> x \<in> carrier G" by (unfold Units_def) fast lemma (in monoid) inv_unique: assumes eq: "y \<otimes> x = \<one>" "x \<otimes> y' = \<one>" and G: "x \<in> carrier G" "y \<in> carrier G" "y' \<in> carrier G" shows "y = y'" proof - from G eq have "y = y \<otimes> (x \<otimes> y')" by simp also from G have "... = (y \<otimes> x) \<otimes> y'" by (simp add: m_assoc) also from G eq have "... = y'" by simp finally show ?thesis . qed lemma (in monoid) Units_m_closed [intro, simp]: assumes x: "x \<in> Units G" and y: "y \<in> Units G" shows "x \<otimes> y \<in> Units G" proof - from x obtain x' where x: "x \<in> carrier G" "x' \<in> carrier G" and xinv: "x \<otimes> x' = \<one>" "x' \<otimes> x = \<one>" unfolding Units_def by fast from y obtain y' where y: "y \<in> carrier G" "y' \<in> carrier G" and yinv: "y \<otimes> y' = \<one>" "y' \<otimes> y = \<one>" unfolding Units_def by fast from x y xinv yinv have "y' \<otimes> (x' \<otimes> x) \<otimes> y = \<one>" by simp moreover from x y xinv yinv have "x \<otimes> (y \<otimes> y') \<otimes> x' = \<one>" by simp moreover note x y ultimately show ?thesis unfolding Units_def -- "Must avoid premature use of @{text hyp_subst_tac}." apply (rule_tac CollectI) apply (rule) apply (fast) apply (rule bexI [where x = "y' \<otimes> x'"]) apply (auto simp: m_assoc) done qed lemma (in monoid) Units_one_closed [intro, simp]: "\<one> \<in> Units G" by (unfold Units_def) auto lemma (in monoid) Units_inv_closed [intro, simp]: "x \<in> Units G ==> inv x \<in> carrier G" apply (unfold Units_def m_inv_def, auto) apply (rule theI2, fast) apply (fast intro: inv_unique, fast) done lemma (in monoid) Units_l_inv_ex: "x \<in> Units G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>" by (unfold Units_def) auto lemma (in monoid) Units_r_inv_ex: "x \<in> Units G ==> \<exists>y \<in> carrier G. x \<otimes> y = \<one>" by (unfold Units_def) auto lemma (in monoid) Units_l_inv [simp]: "x \<in> Units G ==> inv x \<otimes> x = \<one>" apply (unfold Units_def m_inv_def, auto) apply (rule theI2, fast) apply (fast intro: inv_unique, fast) done lemma (in monoid) Units_r_inv [simp]: "x \<in> Units G ==> x \<otimes> inv x = \<one>" apply (unfold Units_def m_inv_def, auto) apply (rule theI2, fast) apply (fast intro: inv_unique, fast) done lemma (in monoid) Units_inv_Units [intro, simp]: "x \<in> Units G ==> inv x \<in> Units G" proof - assume x: "x \<in> Units G" show "inv x \<in> Units G" by (auto simp add: Units_def intro: Units_l_inv Units_r_inv x Units_closed [OF x]) qed lemma (in monoid) Units_l_cancel [simp]: "[| x \<in> Units G; y \<in> carrier G; z \<in> carrier G |] ==> (x \<otimes> y = x \<otimes> z) = (y = z)" proof assume eq: "x \<otimes> y = x \<otimes> z" and G: "x \<in> Units G" "y \<in> carrier G" "z \<in> carrier G" then have "(inv x \<otimes> x) \<otimes> y = (inv x \<otimes> x) \<otimes> z" by (simp add: m_assoc Units_closed del: Units_l_inv) with G show "y = z" by (simp add: Units_l_inv) next assume eq: "y = z" and G: "x \<in> Units G" "y \<in> carrier G" "z \<in> carrier G" then show "x \<otimes> y = x \<otimes> z" by simp qed lemma (in monoid) Units_inv_inv [simp]: "x \<in> Units G ==> inv (inv x) = x" proof - assume x: "x \<in> Units G" then have "inv x \<otimes> inv (inv x) = inv x \<otimes> x" by simp with x show ?thesis by (simp add: Units_closed del: Units_l_inv Units_r_inv) qed lemma (in monoid) inv_inj_on_Units: "inj_on (m_inv G) (Units G)" proof (rule inj_onI) fix x y assume G: "x \<in> Units G" "y \<in> Units G" and eq: "inv x = inv y" then have "inv (inv x) = inv (inv y)" by simp with G show "x = y" by simp qed lemma (in monoid) Units_inv_comm: assumes inv: "x \<otimes> y = \<one>" and G: "x \<in> Units G" "y \<in> Units G" shows "y \<otimes> x = \<one>" proof - from G have "x \<otimes> y \<otimes> x = x \<otimes> \<one>" by (auto simp add: inv Units_closed) with G show ?thesis by (simp del: r_one add: m_assoc Units_closed) qed text {* Power *} lemma (in monoid) nat_pow_closed [intro, simp]: "x \<in> carrier G ==> x (^) (n::nat) \<in> carrier G" by (induct n) (simp_all add: nat_pow_def) lemma (in monoid) nat_pow_0 [simp]: "x (^) (0::nat) = \<one>" by (simp add: nat_pow_def) lemma (in monoid) nat_pow_Suc [simp]: "x (^) (Suc n) = x (^) n \<otimes> x" by (simp add: nat_pow_def) lemma (in monoid) nat_pow_one [simp]: "\<one> (^) (n::nat) = \<one>" by (induct n) simp_all lemma (in monoid) nat_pow_mult: "x \<in> carrier G ==> x (^) (n::nat) \<otimes> x (^) m = x (^) (n + m)" by (induct m) (simp_all add: m_assoc [THEN sym]) lemma (in monoid) nat_pow_pow: "x \<in> carrier G ==> (x (^) n) (^) m = x (^) (n * m::nat)" by (induct m) (simp, simp add: nat_pow_mult add_commute) (* Jacobson defines submonoid here. *) (* Jacobson defines the order of a monoid here. *) subsection {* Groups *} text {* A group is a monoid all of whose elements are invertible. *} locale group = monoid + assumes Units: "carrier G <= Units G" lemma (in group) is_group: "group G" by (rule group_axioms) theorem groupI: fixes G (structure) assumes m_closed [simp]: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G" and one_closed [simp]: "\<one> \<in> carrier G" and m_assoc: "!!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 ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>" shows "group G" proof - have l_cancel [simp]: "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==> (x \<otimes> y = x \<otimes> z) = (y = z)" proof fix x y z assume eq: "x \<otimes> y = x \<otimes> z" and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G" with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier G" and l_inv: "x_inv \<otimes> x = \<one>" by fast from G eq xG have "(x_inv \<otimes> x) \<otimes> y = (x_inv \<otimes> x) \<otimes> z" by (simp add: m_assoc) with G show "y = z" by (simp add: l_inv) next fix x y z assume eq: "y = z" and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G" then show "x \<otimes> y = x \<otimes> z" by simp qed have r_one: "!!x. x \<in> carrier G ==> x \<otimes> \<one> = x" proof - fix x assume x: "x \<in> carrier G" with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier G" and l_inv: "x_inv \<otimes> x = \<one>" by fast from x xG have "x_inv \<otimes> (x \<otimes> \<one>) = x_inv \<otimes> x" by (simp add: m_assoc [symmetric] l_inv) with x xG show "x \<otimes> \<one> = x" by simp qed have inv_ex: "!!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" with l_inv_ex obtain y where y: "y \<in> carrier G" and l_inv: "y \<otimes> x = \<one>" by fast from x y have "y \<otimes> (x \<otimes> y) = y \<otimes> \<one>" 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 "\<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 proof qed (auto simp: r_one m_assoc carrier_subset_Units) qed lemma (in monoid) group_l_invI: assumes l_inv_ex: "!!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) lemma (in group) Units_eq [simp]: "Units G = carrier G" proof show "Units G <= carrier G" by fast next show "carrier G <= Units G" by (rule Units) qed lemma (in group) inv_closed [intro, simp]: "x \<in> carrier G ==> inv x \<in> carrier G" using Units_inv_closed by simp lemma (in group) l_inv_ex [simp]: "x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>" using Units_l_inv_ex by simp lemma (in group) r_inv_ex [simp]: "x \<in> carrier G ==> \<exists>y \<in> carrier G. x \<otimes> y = \<one>" using Units_r_inv_ex by simp lemma (in group) l_inv [simp]: "x \<in> carrier G ==> inv x \<otimes> x = \<one>" using Units_l_inv by simp subsection {* Cancellation Laws and Basic Properties *} lemma (in group) l_cancel [simp]: "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==> (x \<otimes> y = x \<otimes> z) = (y = z)" using Units_l_inv by simp lemma (in group) r_inv [simp]: "x \<in> carrier G ==> x \<otimes> inv x = \<one>" proof - assume x: "x \<in> carrier G" then have "inv x \<otimes> (x \<otimes> inv x) = inv x \<otimes> \<one>" by (simp add: m_assoc [symmetric] l_inv) with x show ?thesis by (simp del: r_one) qed lemma (in group) r_cancel [simp]: "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==> (y \<otimes> x = z \<otimes> x) = (y = z)" proof 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] del: r_inv Units_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" then show "y \<otimes> x = z \<otimes> x" by simp qed lemma (in group) inv_one [simp]: "inv \<one> = \<one>" proof - have "inv \<one> = \<one> \<otimes> (inv \<one>)" by (simp del: r_inv Units_r_inv) moreover have "... = \<one>" by simp finally show ?thesis . qed lemma (in group) inv_inv [simp]: "x \<in> carrier G ==> inv (inv x) = x" using Units_inv_inv by simp lemma (in group) inv_inj: "inj_on (m_inv G) (carrier G)" using inv_inj_on_Units by simp lemma (in group) inv_mult_group: "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv y \<otimes> inv x" 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]) with G show ?thesis by (simp del: l_inv Units_l_inv) qed lemma (in group) inv_comm: "[| x \<otimes> y = \<one>; x \<in> carrier G; y \<in> carrier G |] ==> y \<otimes> x = \<one>" by (rule Units_inv_comm) auto lemma (in group) inv_equality: "[|y \<otimes> x = \<one>; x \<in> carrier G; y \<in> carrier G|] ==> inv x = y" apply (simp add: m_inv_def) apply (rule the_equality) apply (simp add: inv_comm [of y x]) apply (rule r_cancel [THEN iffD1], auto) done text {* Power *} lemma (in group) int_pow_def2: "a (^) (z::int) = (if neg z then inv (a (^) (nat (-z))) else a (^) (nat z))" by (simp add: int_pow_def nat_pow_def Let_def) lemma (in group) int_pow_0 [simp]: "x (^) (0::int) = \<one>" by (simp add: int_pow_def2) lemma (in group) int_pow_one [simp]: "\<one> (^) (z::int) = \<one>" by (simp add: int_pow_def2) subsection {* Subgroups *} locale subgroup = fixes H and G (structure) 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" lemma (in subgroup) is_subgroup: "subgroup H G" by (rule subgroup_axioms) declare (in subgroup) group.intro [intro] lemma (in subgroup) mem_carrier [simp]: "x \<in> H \<Longrightarrow> x \<in> carrier G" using subset by blast lemma subgroup_imp_subset: "subgroup H G \<Longrightarrow> H \<subseteq> carrier G" by (rule subgroup.subset) lemma (in subgroup) subgroup_is_group [intro]: assumes "group G" shows "group (G\<lparr>carrier := H\<rparr>)" proof - interpret group G by fact show ?thesis apply (rule monoid.group_l_invI) apply (unfold_locales) [1] apply (auto intro: m_assoc l_inv mem_carrier) done qed text {* Since @{term H} is nonempty, it contains some element @{term x}. Since it is closed under inverse, it contains @{text "inv x"}. Since it is closed under product, it contains @{text "x \<otimes> inv x = \<one>"}. *} lemma (in group) one_in_subset: "[| H \<subseteq> carrier G; H \<noteq> {}; \<forall>a \<in> H. inv a \<in> H; \<forall>a\<in>H. \<forall>b\<in>H. a \<otimes> b \<in> H |] ==> \<one> \<in> H" by (force simp add: l_inv) text {* A characterization of subgroups: closed, non-empty subset. *} lemma (in group) subgroupI: assumes subset: "H \<subseteq> carrier G" and non_empty: "H \<noteq> {}" 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 (simp add: subgroup_def assms) show "\<one> \<in> H" by (rule one_in_subset) (auto simp only: assms) qed declare monoid.one_closed [iff] group.inv_closed [simp] monoid.l_one [simp] monoid.r_one [simp] group.inv_inv [simp] lemma subgroup_nonempty: "~ subgroup {} G" by (blast dest: subgroup.one_closed) lemma (in subgroup) finite_imp_card_positive: "finite (carrier G) ==> 0 < card H" proof (rule classical) 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 (* lemma (in monoid) Units_subgroup: "subgroup (Units G) G" *) subsection {* Direct Products *} 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 DirProd_monoid: assumes "monoid G" and "monoid H" shows "monoid (G \<times>\<times> H)" proof - interpret G: monoid G by fact interpret H: monoid H by fact from assms show ?thesis by (unfold monoid_def DirProd_def, auto) qed text{*Does not use the previous result because it's easier just to use auto.*} lemma DirProd_group: assumes "group G" and "group H" shows "group (G \<times>\<times> H)" proof - interpret G: group G by fact interpret H: group H by fact show ?thesis by (rule groupI) (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv simp add: DirProd_def) qed lemma carrier_DirProd [simp]: "carrier (G \<times>\<times> H) = carrier G \<times> carrier H" by (simp add: DirProd_def) 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_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_DirProd [simp]: assumes "group G" and "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 - interpret G: group G by fact interpret H: group H by fact interpret Prod: group "G \<times>\<times> H" by (auto intro: DirProd_group group.intro group.axioms assms) show ?thesis by (simp add: Prod.inv_equality g h) qed subsection {* Homomorphisms and Isomorphisms *} constdefs (structure G and H) hom :: "_ => _ => ('a => 'b) set" "hom G H == {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 group) hom_compose: "[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I" by (fastsimp simp add: hom_def compose_def) constdefs iso :: "_ => _ => ('a => 'b) set" (infixr "\<cong>" 60) "G \<cong> H == {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}" lemma iso_refl: "(%x. x) \<in> G \<cong> G" by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def) lemma (in group) iso_sym: "h \<in> G \<cong> H \<Longrightarrow> inv_into (carrier G) h \<in> H \<cong> G" apply (simp add: iso_def bij_betw_inv_into) apply (subgoal_tac "inv_into (carrier G) h \<in> carrier H \<rightarrow> carrier G") prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_inv_into]) apply (simp add: hom_def bij_betw_def inv_into_f_eq f_inv_into_f Pi_def) done lemma (in group) iso_trans: "[|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 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) 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) text{*Basis for homomorphism proofs: we assume two groups @{term G} and @{term H}, with a homomorphism @{term h} between them*} locale group_hom = G: group G + H: group H for G (structure) and H (structure) + fixes h assumes homh: "h \<in> hom G H" lemma (in group_hom) hom_mult [simp]: "[| x \<in> carrier G; y \<in> carrier G |] ==> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y" proof - assume "x \<in> carrier G" "y \<in> carrier G" with homh [unfolded hom_def] show ?thesis by simp qed lemma (in group_hom) hom_closed [simp]: "x \<in> carrier G ==> h x \<in> carrier H" proof - assume "x \<in> carrier G" with homh [unfolded hom_def] show ?thesis by auto qed lemma (in group_hom) one_closed [simp]: "h \<one> \<in> carrier H" by simp lemma (in group_hom) hom_one [simp]: "h \<one> = \<one>\<^bsub>H\<^esub>" proof - have "h \<one> \<otimes>\<^bsub>H\<^esub> \<one>\<^bsub>H\<^esub> = h \<one> \<otimes>\<^bsub>H\<^esub> h \<one>" by (simp add: hom_mult [symmetric] del: hom_mult) then show ?thesis by (simp del: r_one) qed lemma (in group_hom) inv_closed [simp]: "x \<in> carrier G ==> h (inv x) \<in> carrier H" by simp lemma (in group_hom) hom_inv [simp]: "x \<in> carrier G ==> h (inv x) = inv\<^bsub>H\<^esub> (h x)" 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] 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] 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 del: H.r_inv H.Units_r_inv) qed subsection {* Commutative Structures *} text {* Naming convention: multiplicative structures that are commutative are called \emph{commutative}, additive structures are called \emph{Abelian}. *} 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_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" from xyz have "x \<otimes> (y \<otimes> z) = (x \<otimes> y) \<otimes> z" by (simp add: m_assoc) also from xyz have "... = (y \<otimes> x) \<otimes> z" by (simp add: m_comm) also from xyz have "... = y \<otimes> (x \<otimes> z)" by (simp add: m_assoc) finally show ?thesis . qed lemmas (in comm_monoid) m_ac = m_assoc m_comm m_lcomm lemma comm_monoidI: fixes G (structure) assumes m_closed: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G" and one_closed: "\<one> \<in> carrier G" and m_assoc: "!!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: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x" and m_comm: "!!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 comm_monoid_axioms.intro monoid.intro intro: assms 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 - assume G: "x \<in> carrier G" then have "x \<otimes> \<one> = \<one> \<otimes> x" by (simp add: m_comm) 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" by (induct n) (simp, simp add: m_ac) locale comm_group = comm_monoid + group lemma (in group) group_comm_groupI: assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x" shows "comm_group G" proof qed (simp_all add: m_comm) lemma comm_groupI: fixes G (structure) assumes m_closed: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G" and one_closed: "\<one> \<in> carrier G" and m_assoc: "!!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 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 ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>" shows "comm_group G" by (fast intro: group.group_comm_groupI groupI assms) lemma (in comm_group) inv_mult: "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv x \<otimes> inv y" by (simp add: m_ac inv_mult_group) subsection {* The Lattice of Subgroups of a Group *} text_raw {* \label{sec:subgroup-lattice} *} theorem (in group) subgroups_partial_order: "partial_order (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)" proof qed simp_all lemma (in group) subgroup_self: "subgroup (carrier G) G" by (rule subgroupI) auto lemma (in group) subgroup_imp_group: "subgroup H G ==> group (G(| carrier := H |))" by (erule subgroup.subgroup_is_group) (rule group_axioms) lemma (in group) is_monoid [intro, simp]: "monoid G" 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" apply (rule_tac inv_equality [THEN sym]) apply (rule group.l_inv [OF subgroup_imp_group, simplified], assumption+) apply (rule subsetD [OF subgroup.subset], assumption+) apply (rule subsetD [OF subgroup.subset], assumption) apply (rule_tac group.inv_closed [OF subgroup_imp_group, simplified], assumption+) done theorem (in group) subgroups_Inter: assumes subgr: "(!!H. H \<in> A ==> subgroup H G)" and not_empty: "A ~= {}" shows "subgroup (\<Inter>A) G" proof (rule subgroupI) from subgr [THEN subgroup.subset] and not_empty show "\<Inter>A \<subseteq> carrier G" by blast next from subgr [THEN subgroup.one_closed] show "\<Inter>A ~= {}" by blast next fix x assume "x \<in> \<Inter>A" with subgr [THEN subgroup.m_inv_closed] show "inv x \<in> \<Inter>A" by blast next fix x y assume "x \<in> \<Inter>A" "y \<in> \<Inter>A" with subgr [THEN subgroup.m_closed] show "x \<otimes> y \<in> \<Inter>A" by blast qed theorem (in group) subgroups_complete_lattice: "complete_lattice (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)" (is "complete_lattice ?L") proof (rule partial_order.complete_lattice_criterion1) show "partial_order ?L" by (rule subgroups_partial_order) next show "\<exists>G. greatest ?L G (carrier ?L)" proof show "greatest ?L (carrier G) (carrier ?L)" by (unfold greatest_def) (simp add: subgroup.subset subgroup_self) qed next fix A assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}" then have Int_subgroup: "subgroup (\<Inter>A) G" by (fastsimp intro: subgroups_Inter) show "\<exists>I. greatest ?L I (Lower ?L A)" proof show "greatest ?L (\<Inter>A) (Lower ?L A)" (is "greatest _ ?Int _") proof (rule greatest_LowerI) fix H assume H: "H \<in> A" with L have subgroupH: "subgroup H G" by auto from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H") by (rule subgroup_imp_group) from groupH have monoidH: "monoid ?H" by (rule group.is_monoid) from H have Int_subset: "?Int \<subseteq> H" by fastsimp then show "le ?L ?Int H" by simp next fix H assume H: "H \<in> Lower ?L A" with L Int_subgroup show "le ?L H ?Int" by (fastsimp simp: Lower_def intro: Inter_greatest) next show "A \<subseteq> carrier ?L" by (rule L) next show "?Int \<in> carrier ?L" by simp (rule Int_subgroup) qed qed qed end