(* Title: HOL/Algebra/Coset.thy
Author: Florian Kammueller, with new proofs by L C Paulson, and
Stephan Hohe
*)
theory Coset imports Group begin
section {*Cosets and Quotient Groups*}
constdefs (structure G)
r_coset :: "[_, 'a set, 'a] \ 'a set" (infixl "#>\" 60)
"H #> a \ \h\H. {h \ a}"
l_coset :: "[_, 'a, 'a set] \ 'a set" (infixl "<#\" 60)
"a <# H \ \h\H. {a \ h}"
RCOSETS :: "[_, 'a set] \ ('a set)set" ("rcosets\ _" [81] 80)
"rcosets H \ \a\carrier G. {H #> a}"
set_mult :: "[_, 'a set ,'a set] \ 'a set" (infixl "<#>\" 60)
"H <#> K \ \h\H. \k\K. {h \ k}"
SET_INV :: "[_,'a set] \ 'a set" ("set'_inv\ _" [81] 80)
"set_inv H \ \h\H. {inv h}"
locale normal = subgroup + group +
assumes coset_eq: "(\x \ carrier G. H #> x = x <# H)"
abbreviation
normal_rel :: "['a set, ('a, 'b) monoid_scheme] \ bool" (infixl "\" 60) where
"H \ G \ normal H G"
subsection {*Basic Properties of Cosets*}
lemma (in group) coset_mult_assoc:
"[| M \ carrier G; g \ carrier G; h \ carrier G |]
==> (M #> g) #> h = M #> (g \ h)"
by (force simp add: r_coset_def m_assoc)
lemma (in group) coset_mult_one [simp]: "M \ carrier G ==> M #> \ = M"
by (force simp add: r_coset_def)
lemma (in group) coset_mult_inv1:
"[| M #> (x \ (inv y)) = M; x \ carrier G ; y \ carrier G;
M \ carrier G |] ==> M #> x = M #> y"
apply (erule subst [of concl: "%z. M #> x = z #> y"])
apply (simp add: coset_mult_assoc m_assoc)
done
lemma (in group) coset_mult_inv2:
"[| M #> x = M #> y; x \ carrier G; y \ carrier G; M \ carrier G |]
==> M #> (x \ (inv y)) = M "
apply (simp add: coset_mult_assoc [symmetric])
apply (simp add: coset_mult_assoc)
done
lemma (in group) coset_join1:
"[| H #> x = H; x \ carrier G; subgroup H G |] ==> x \ H"
apply (erule subst)
apply (simp add: r_coset_def)
apply (blast intro: l_one subgroup.one_closed sym)
done
lemma (in group) solve_equation:
"\subgroup H G; x \ H; y \ H\ \ \h\H. y = h \ x"
apply (rule bexI [of _ "y \ (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:
"\y \ H #> x; x \ carrier G; subgroup H G\ \ 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 \ carrier G; subgroup H G; x\H\ \ H #> x = H"
--{*Alternative proof is to put @{term "x=\"} in @{text repr_independence}.*}
by (force simp add: subgroup.m_closed r_coset_def solve_equation)
lemma (in monoid) r_coset_subset_G:
"[| H \ carrier G; x \ carrier G |] ==> H #> x \ carrier G"
by (auto simp add: r_coset_def)
lemma (in group) rcosI:
"[| h \ H; H \ carrier G; x \ carrier G|] ==> h \ x \ H #> x"
by (auto simp add: r_coset_def)
lemma (in group) rcosetsI:
"\H \ carrier G; x \ carrier G\ \ H #> x \ rcosets H"
by (auto simp add: RCOSETS_def)
text{*Really needed?*}
lemma (in group) transpose_inv:
"[| x \ y = z; x \ carrier G; y \ carrier G; z \ carrier G |]
==> (inv x) \ z = y"
by (force simp add: m_assoc [symmetric])
lemma (in group) rcos_self: "[| x \ carrier G; subgroup H G |] ==> x \ H #> x"
apply (simp add: r_coset_def)
apply (blast intro: sym l_one subgroup.subset [THEN subsetD]
subgroup.one_closed)
done
text (in group) {* Opposite of @{thm [source] "repr_independence"} *}
lemma (in group) repr_independenceD:
assumes "subgroup H G"
assumes ycarr: "y \ carrier G"
and repr: "H #> x = H #> y"
shows "y \ H #> x"
proof -
interpret subgroup H G by fact
show ?thesis apply (subst repr)
apply (intro rcos_self)
apply (rule ycarr)
apply (rule is_subgroup)
done
qed
text {* Elements of a right coset are in the carrier *}
lemma (in subgroup) elemrcos_carrier:
assumes "group G"
assumes acarr: "a \ carrier G"
and a': "a' \ H #> a"
shows "a' \ carrier G"
proof -
interpret group G by fact
from subset and acarr
have "H #> a \ carrier G" by (rule r_coset_subset_G)
from this and a'
show "a' \ carrier G"
by fast
qed
lemma (in subgroup) rcos_const:
assumes "group G"
assumes hH: "h \ H"
shows "H #> h = H"
proof -
interpret group G by fact
show ?thesis apply (unfold r_coset_def)
apply rule
apply rule
apply clarsimp
apply (intro subgroup.m_closed)
apply (rule is_subgroup)
apply assumption
apply (rule hH)
apply rule
apply simp
proof -
fix h'
assume h'H: "h' \ H"
note carr = hH[THEN mem_carrier] h'H[THEN mem_carrier]
from carr
have a: "h' = (h' \ inv h) \ h" by (simp add: m_assoc)
from h'H hH
have "h' \ inv h \ H" by simp
from this and a
show "\x\H. h' = x \ h" by fast
qed
qed
text {* Step one for lemma @{text "rcos_module"} *}
lemma (in subgroup) rcos_module_imp:
assumes "group G"
assumes xcarr: "x \ carrier G"
and x'cos: "x' \ H #> x"
shows "(x' \ inv x) \ H"
proof -
interpret group G by fact
from xcarr x'cos
have x'carr: "x' \ carrier G"
by (rule elemrcos_carrier[OF is_group])
from xcarr
have ixcarr: "inv x \ carrier G"
by simp
from x'cos
have "\h\H. x' = h \ x"
unfolding r_coset_def
by fast
from this
obtain h
where hH: "h \ H"
and x': "x' = h \ x"
by auto
from hH and subset
have hcarr: "h \ carrier G" by fast
note carr = xcarr x'carr hcarr
from x' and carr
have "x' \ (inv x) = (h \ x) \ (inv x)" by fast
also from carr
have "\ = h \ (x \ inv x)" by (simp add: m_assoc)
also from carr
have "\ = h \ \" by simp
also from carr
have "\ = h" by simp
finally
have "x' \ (inv x) = h" by simp
from hH this
show "x' \ (inv x) \ H" by simp
qed
text {* Step two for lemma @{text "rcos_module"} *}
lemma (in subgroup) rcos_module_rev:
assumes "group G"
assumes carr: "x \ carrier G" "x' \ carrier G"
and xixH: "(x' \ inv x) \ H"
shows "x' \ H #> x"
proof -
interpret group G by fact
from xixH
have "\h\H. x' \ (inv x) = h" by fast
from this
obtain h
where hH: "h \ H"
and hsym: "x' \ (inv x) = h"
by fast
from hH subset have hcarr: "h \ carrier G" by simp
note carr = carr hcarr
from hsym[symmetric] have "h \ x = x' \ (inv x) \ x" by fast
also from carr
have "\ = x' \ ((inv x) \ x)" by (simp add: m_assoc)
also from carr
have "\ = x' \ \" by (simp add: l_inv)
also from carr
have "\ = x'" by simp
finally
have "h \ x = x'" by simp
from this[symmetric] and hH
show "x' \ H #> x"
unfolding r_coset_def
by fast
qed
text {* Module property of right cosets *}
lemma (in subgroup) rcos_module:
assumes "group G"
assumes carr: "x \ carrier G" "x' \ carrier G"
shows "(x' \ H #> x) = (x' \ inv x \ H)"
proof -
interpret group G by fact
show ?thesis proof assume "x' \ H #> x"
from this and carr
show "x' \ inv x \ H"
by (intro rcos_module_imp[OF is_group])
next
assume "x' \ inv x \ H"
from this and carr
show "x' \ H #> x"
by (intro rcos_module_rev[OF is_group])
qed
qed
text {* Right cosets are subsets of the carrier. *}
lemma (in subgroup) rcosets_carrier:
assumes "group G"
assumes XH: "X \ rcosets H"
shows "X \ carrier G"
proof -
interpret group G by fact
from XH have "\x\ carrier G. X = H #> x"
unfolding RCOSETS_def
by fast
from this
obtain x
where xcarr: "x\ carrier G"
and X: "X = H #> x"
by fast
from subset and xcarr
show "X \ carrier G"
unfolding X
by (rule r_coset_subset_G)
qed
text {* Multiplication of general subsets *}
lemma (in monoid) set_mult_closed:
assumes Acarr: "A \ carrier G"
and Bcarr: "B \ carrier G"
shows "A <#> B \ carrier G"
apply rule apply (simp add: set_mult_def, clarsimp)
proof -
fix a b
assume "a \ A"
from this and Acarr
have acarr: "a \ carrier G" by fast
assume "b \ B"
from this and Bcarr
have bcarr: "b \ carrier G" by fast
from acarr bcarr
show "a \ b \ carrier G" by (rule m_closed)
qed
lemma (in comm_group) mult_subgroups:
assumes subH: "subgroup H G"
and subK: "subgroup K G"
shows "subgroup (H <#> K) G"
apply (rule subgroup.intro)
apply (intro set_mult_closed subgroup.subset[OF subH] subgroup.subset[OF subK])
apply (simp add: set_mult_def) apply clarsimp defer 1
apply (simp add: set_mult_def) defer 1
apply (simp add: set_mult_def, clarsimp) defer 1
proof -
fix ha hb ka kb
assume haH: "ha \ H" and hbH: "hb \ H" and kaK: "ka \ K" and kbK: "kb \ K"
note carr = haH[THEN subgroup.mem_carrier[OF subH]] hbH[THEN subgroup.mem_carrier[OF subH]]
kaK[THEN subgroup.mem_carrier[OF subK]] kbK[THEN subgroup.mem_carrier[OF subK]]
from carr
have "(ha \ ka) \ (hb \ kb) = ha \ (ka \ hb) \ kb" by (simp add: m_assoc)
also from carr
have "\ = ha \ (hb \ ka) \ kb" by (simp add: m_comm)
also from carr
have "\ = (ha \ hb) \ (ka \ kb)" by (simp add: m_assoc)
finally
have eq: "(ha \ ka) \ (hb \ kb) = (ha \ hb) \ (ka \ kb)" .
from haH hbH have hH: "ha \ hb \ H" by (simp add: subgroup.m_closed[OF subH])
from kaK kbK have kK: "ka \ kb \ K" by (simp add: subgroup.m_closed[OF subK])
from hH and kK and eq
show "\h'\H. \k'\K. (ha \ ka) \ (hb \ kb) = h' \ k'" by fast
next
have "\ = \ \ \" by simp
from subgroup.one_closed[OF subH] subgroup.one_closed[OF subK] this
show "\h\H. \k\K. \ = h \ k" by fast
next
fix h k
assume hH: "h \ H"
and kK: "k \ K"
from hH[THEN subgroup.mem_carrier[OF subH]] kK[THEN subgroup.mem_carrier[OF subK]]
have "inv (h \ k) = inv h \ inv k" by (simp add: inv_mult_group m_comm)
from subgroup.m_inv_closed[OF subH hH] and subgroup.m_inv_closed[OF subK kK] and this
show "\ha\H. \ka\K. inv (h \ k) = ha \ ka" by fast
qed
lemma (in subgroup) lcos_module_rev:
assumes "group G"
assumes carr: "x \ carrier G" "x' \ carrier G"
and xixH: "(inv x \ x') \ H"
shows "x' \ x <# H"
proof -
interpret group G by fact
from xixH
have "\h\H. (inv x) \ x' = h" by fast
from this
obtain h
where hH: "h \ H"
and hsym: "(inv x) \ x' = h"
by fast
from hH subset have hcarr: "h \ carrier G" by simp
note carr = carr hcarr
from hsym[symmetric] have "x \ h = x \ ((inv x) \ x')" by fast
also from carr
have "\ = (x \ (inv x)) \