Strange. The proof worked in the 2008 release. In order to make it work now, the last line of the proof must be moved up two places. In other words, the first proof step is now returning its subgoals in a different order from before.
(*
Title: HOL/Algebra/Group.thy
Id: $Id$
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 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"
by (simp add: hom_def)
lemma hom_closed:
"[| h \<in> hom G H; x \<in> carrier G |] ==> h x \<in> carrier H"
by (auto simp add: hom_def funcset_mem)
lemma (in group) hom_compose:
"[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
apply (auto simp add: hom_def funcset_compose)
apply (simp add: compose_def funcset_mem)
done
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 (carrier G) h \<in> H \<cong> G"
apply (simp add: iso_def bij_betw_Inv)
apply (subgoal_tac "Inv (carrier G) h \<in> carrier H \<rightarrow> carrier G")
prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_Inv])
apply (simp add: hom_def bij_betw_def Inv_f_eq funcset_mem f_Inv_f)
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 Pi_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 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]
and hom_closed [simp] = hom_closed [OF homh]
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