(*
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] \ 'a" (infixl "\\" 70)
one :: 'a ("\\")
constdefs (structure G)
m_inv :: "('a, 'b) monoid_scheme => 'a => 'a" ("inv\ _" [81] 80)
"inv x == (THE y. y \ carrier G & x \ y = \ & y \ x = \)"
Units :: "_ => 'a set"
--{*The set of invertible elements*}
"Units G == {y. y \ carrier G & (\x \ carrier G. x \ y = \ & y \ x = \)}"
consts
pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\" 75)
defs (overloaded)
nat_pow_def: "pow G a n == nat_rec \\<^bsub>G\<^esub> (%u b. b \\<^bsub>G\<^esub> a) n"
int_pow_def: "pow G a z ==
let p = nat_rec \\<^bsub>G\<^esub> (%u b. b \\<^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]:
"\x \ carrier G; y \ carrier G\ \ x \ y \ carrier G"
and m_assoc:
"\x \ carrier G; y \ carrier G; z \ carrier G\
\ (x \ y) \ z = x \ (y \ z)"
and one_closed [intro, simp]: "\ \ carrier G"
and l_one [simp]: "x \ carrier G \ \ \ x = x"
and r_one [simp]: "x \ carrier G \ x \ \ = x"
lemma monoidI:
fixes G (structure)
assumes m_closed:
"!!x y. [| x \ carrier G; y \ carrier G |] ==> x \ y \ carrier G"
and one_closed: "\ \ carrier G"
and m_assoc:
"!!x y z. [| x \ carrier G; y \ carrier G; z \ carrier G |] ==>
(x \ y) \ z = x \ (y \ z)"
and l_one: "!!x. x \ carrier G ==> \ \ x = x"
and r_one: "!!x. x \ carrier G ==> x \ \ = x"
shows "monoid G"
by (fast intro!: monoid.intro intro: assms)
lemma (in monoid) Units_closed [dest]:
"x \ Units G ==> x \ carrier G"
by (unfold Units_def) fast
lemma (in monoid) inv_unique:
assumes eq: "y \ x = \" "x \ y' = \"
and G: "x \ carrier G" "y \ carrier G" "y' \ carrier G"
shows "y = y'"
proof -
from G eq have "y = y \ (x \ y')" by simp
also from G have "... = (y \ x) \ 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 \ Units G" and y: "y \ Units G"
shows "x \ y \ Units G"
proof -
from x obtain x' where x: "x \ carrier G" "x' \ carrier G" and xinv: "x \ x' = \" "x' \ x = \"
unfolding Units_def by fast
from y obtain y' where y: "y \ carrier G" "y' \ carrier G" and yinv: "y \ y' = \" "y' \ y = \"
unfolding Units_def by fast
from x y xinv yinv have "y' \ (x' \ x) \ y = \" by simp
moreover from x y xinv yinv have "x \ (y \ y') \ x' = \" 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' \ x'"])
apply (auto simp: m_assoc)
done
qed
lemma (in monoid) Units_one_closed [intro, simp]:
"\ \ Units G"
by (unfold Units_def) auto
lemma (in monoid) Units_inv_closed [intro, simp]:
"x \ Units G ==> inv x \ 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 \ Units G ==> \y \ carrier G. y \ x = \"
by (unfold Units_def) auto
lemma (in monoid) Units_r_inv_ex:
"x \ Units G ==> \y \ carrier G. x \ y = \"
by (unfold Units_def) auto
lemma (in monoid) Units_l_inv [simp]:
"x \ Units G ==> inv x \ x = \"
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 \ Units G ==> x \ inv x = \"
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 \ Units G ==> inv x \ Units G"
proof -
assume x: "x \ Units G"
show "inv x \ 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 \ Units G; y \ carrier G; z \ carrier G |] ==>
(x \ y = x \ z) = (y = z)"
proof
assume eq: "x \ y = x \ z"
and G: "x \ Units G" "y \ carrier G" "z \ carrier G"
then have "(inv x \ x) \ y = (inv x \ x) \ 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 \ Units G" "y \ carrier G" "z \ carrier G"
then show "x \ y = x \ z" by simp
qed
lemma (in monoid) Units_inv_inv [simp]:
"x \ Units G ==> inv (inv x) = x"
proof -
assume x: "x \ Units G"
then have "inv x \ inv (inv x) = inv x \ 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 \ Units G" "y \ 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 \ y = \"
and G: "x \ Units G" "y \ Units G"
shows "y \ x = \"
proof -
from G have "x \ y \ x = x \ \" 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 \ carrier G ==> x (^) (n::nat) \ carrier G"
by (induct n) (simp_all add: nat_pow_def)
lemma (in monoid) nat_pow_0 [simp]:
"x (^) (0::nat) = \"
by (simp add: nat_pow_def)
lemma (in monoid) nat_pow_Suc [simp]:
"x (^) (Suc n) = x (^) n \ x"
by (simp add: nat_pow_def)
lemma (in monoid) nat_pow_one [simp]:
"\ (^) (n::nat) = \"
by (induct n) simp_all
lemma (in monoid) nat_pow_mult:
"x \ carrier G ==> x (^) (n::nat) \ x (^) m = x (^) (n + m)"
by (induct m) (simp_all add: m_assoc [THEN sym])
lemma (in monoid) nat_pow_pow:
"x \ 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 \ carrier G; y \ carrier G |] ==> x \ y \ carrier G"
and one_closed [simp]: "\ \ carrier G"
and m_assoc:
"!!x y z. [| x \ carrier G; y \ carrier G; z \ carrier G |] ==>
(x \ y) \ z = x \ (y \ z)"
and l_one [simp]: "!!x. x \ carrier G ==> \ \ x = x"
and l_inv_ex: "!!x. x \ carrier G ==> \y \ carrier G. y \ x = \"
shows "group G"
proof -
have l_cancel [simp]:
"!!x y z. [| x \ carrier G; y \ carrier G; z \ carrier G |] ==>
(x \ y = x \ z) = (y = z)"
proof
fix x y z
assume eq: "x \ y = x \ z"
and G: "x \ carrier G" "y \ carrier G" "z \ carrier G"
with l_inv_ex obtain x_inv where xG: "x_inv \ carrier G"
and l_inv: "x_inv \ x = \" by fast
from G eq xG have "(x_inv \ x) \ y = (x_inv \ x) \ 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 \ carrier G" "y \ carrier G" "z \ carrier G"
then show "x \ y = x \ z" by simp
qed
have r_one:
"!!x. x \ carrier G ==> x \ \ = x"
proof -
fix x
assume x: "x \ carrier G"
with l_inv_ex obtain x_inv where xG: "x_inv \ carrier G"
and l_inv: "x_inv \ x = \" by fast
from x xG have "x_inv \ (x \ \) = x_inv \ x"
by (simp add: m_assoc [symmetric] l_inv)
with x xG show "x \ \ = x" by simp
qed
have inv_ex:
"!!x. x \ carrier G ==> \y \ carrier G. y \ x = \ & x \ y = \"
proof -
fix x
assume x: "x \ carrier G"
with l_inv_ex obtain y where y: "y \ carrier G"
and l_inv: "y \ x = \" by fast
from x y have "y \ (x \ y) = y \ \"
by (simp add: m_assoc [symmetric] l_inv r_one)
with x y have r_inv: "x \ y = \"
by simp
from x y show "\y \ carrier G. y \ x = \ & x \ y = \"
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 \ carrier G ==> \