header {* Generators *}
theory "Generators"
imports
"~~/src/HOL/Algebra/Group"
"~~/src/HOL/Algebra/Lattice"
begin
text {* This theory is not specific to Free Groups and could be moved to a more
general place. It defines the subgroup generated by a set of generators and
that homomorphisms agree on the generated subgroup if they agree on the
generators. *}
notation subgroup (infix "\" 80)
subsection {* The subgroup generated by a set *}
text {* The span of a set of subgroup generators, i.e. the generated subgroup, can
be defined inductively or as the intersection of all subgroups containing the
generators. Here, we define it inductively and proof the equivalence *}
inductive_set gen_span :: "('a,'b) monoid_scheme \ 'a set \ 'a set" ("\_\\")
for G and gens
where gen_one [intro!, simp]: "\\<^bsub>G\<^esub> \ \gens\\<^bsub>G\<^esub>"
| gen_gens: "x \ gens \ x \ \gens\\<^bsub>G\<^esub>"
| gen_inv: "x \ \gens\\<^bsub>G\<^esub> \ inv\<^bsub>G\<^esub> x \ \gens\\<^bsub>G\<^esub>"
| gen_mult: "\ x \ \gens\\<^bsub>G\<^esub>; y \ \gens\\<^bsub>G\<^esub> \ \ x \\<^bsub>G\<^esub> y \ \gens\\<^bsub>G\<^esub>"
lemma (in group) gen_span_closed:
assumes "gens \ carrier G"
shows "\gens\\<^bsub>G\<^esub> \ carrier G"
proof (* How can I do this in one "by" line? *)
fix x
from assms show "x \ \gens\\<^bsub>G\<^esub> \ x \ carrier G"
by -(induct rule:gen_span.induct, auto)
qed
lemma (in group) gen_subgroup_is_subgroup:
"gens \ carrier G \ \gens\\<^bsub>G\<^esub> \ G"
by(rule subgroupI)(auto intro:gen_span.intros simp add:gen_span_closed)
lemma (in group) gen_subgroup_is_smallest_containing:
assumes "gens \ carrier G"
shows "\{H. H \ G \ gens \ H} = \gens\\<^bsub>G\<^esub>"
proof
show "\gens\\<^bsub>G\<^esub> \ \{H. H \ G \ gens \ H}"
proof(rule Inf_greatest)
fix H
assume "H \ {H. H \ G \ gens \ H}"
hence "H \ G" and "gens \ H" by auto
show "\gens\\<^bsub>G\<^esub> \ H"
proof
fix x
from `H \ G` and `gens \ H`
show "x \ \gens\\<^bsub>G\<^esub> \ x \ H"
unfolding subgroup_def
by -(induct rule:gen_span.induct, auto)
qed
qed
next
from `gens \ carrier G`
have "\gens\\<^bsub>G\<^esub> \ G" by (rule gen_subgroup_is_subgroup)
moreover
have "gens \ \gens\\<^bsub>G\<^esub>" by (auto intro:gen_span.intros)
ultimately
show "\{H. H \ G \ gens \ H} \ \gens\\<^bsub>G\<^esub>"
by(auto intro:Inter_lower)
qed
subsection {* Generators and homomorphisms *}
text {* Two homorphisms agreeing on some elements agree on the span of those elements.*}
lemma hom_unique_on_span:
assumes "group G"
and "group H"
and "gens \ carrier G"
and "h \ hom G H"
and "h' \ hom G H"
and "\g \ gens. h g = h' g"
shows "\x \ \gens\\<^bsub>G\<^esub>. h x = h' x"
proof
interpret G: group G by fact
interpret H: group H by fact
interpret h: group_hom G H h by unfold_locales fact
interpret h': group_hom G H h' by unfold_locales fact
fix x
from `gens \ carrier G` have "\gens\\<^bsub>G\<^esub> \ carrier G" by (rule G.gen_span_closed)
with assms show "x \ \gens\\<^bsub>G\<^esub> \ h x = h' x" apply -
proof(induct rule:gen_span.induct)
case (gen_mult x y)
hence x: "x \ carrier G" and y: "y \ carrier G" and
hx: "h x = h' x" and hy: "h y = h' y" by auto
thus "h (x \\<^bsub>G\<^esub> y) = h' (x \\<^bsub>G\<^esub> y)" by simp
qed auto
qed
subsection {* Sets of generators *}
text {* There is no definition for @{text gens} is a generating set of
@{text G}. This is easily expressed by @{text "\gens\ = carrier G"}. *}
text {* The following is application of @{text hom_unique_on_span} on a generating
set of the whole group. *}
lemma (in group) hom_unique_by_gens:
assumes "group H"
and gens: "\gens\\<^bsub>G\<^esub> = carrier G"
and "h \ hom G H"
and "h' \ hom G H"
and "\g \ gens. h g = h' g"
shows "\x \ carrier G. h x = h' x"
proof
fix x
from gens have "gens \ carrier G" by (auto intro:gen_span.gen_gens)
with assms and group_axioms have r: "\x \ \gens\\<^bsub>G\<^esub>. h x = h' x"
by -(erule hom_unique_on_span, auto)
with gens show "x \ carrier G \ h x = h' x" by auto
qed
lemma (in group_hom) hom_span:
assumes "gens \ carrier G"
shows "h ` (\gens\\<^bsub>G\<^esub>) = \h ` gens\\<^bsub>H\<^esub>"
proof(rule set_ext, rule iffI)
from `gens \ carrier G`
have "\gens\\<^bsub>G\<^esub> \ carrier G" by (rule G.gen_span_closed)
fix y
assume "y \ h ` \gens\\<^bsub>G\<^esub>"
then obtain x where "x \ \gens\\<^bsub>G\<^esub>" and "y = h x" by auto
from `x \ \gens\\<^bsub>G\<^esub>`
have "h x \ \h ` gens\\<^bsub>H\<^esub>"
proof(induct x)
print_cases
case (gen_inv x)
hence "x \ carrier G" and "h x \ \h ` gens\\<^bsub>H\<^esub>"
using `\gens\\<^bsub>G\<^esub> \ carrier G`
by auto
thus ?case by (auto intro:gen_span.intros)
next
case (gen_mult x y)
hence "x \ carrier G" and "h x \ \h ` gens\\<^bsub>H\<^esub>"
and "y \ carrier G" and "h y \ \h ` gens\\<^bsub>H\<^esub>"
using `\gens\\<^bsub>G\<^esub> \ carrier G`
by auto
thus ?case by (auto intro:gen_span.intros)
qed(auto intro: gen_span.intros)
with `y = h x`
show "y \ \h ` gens\\<^bsub>H\<^esub>" by simp
next
fix x
show "x \ \h ` gens\\<^bsub>H\<^esub> \ x \ h ` \gens\"
proof(induct x rule:gen_span.induct)
print_cases
case (gen_inv y)
then obtain x where "y = h x" and "x \ \gens\" by auto
moreover
hence "x \ carrier G" using `gens \ carrier G`
by (auto dest:G.gen_span_closed)
ultimately show ?case
by (auto intro:hom_inv[THEN sym] rev_image_eqI gen_span.gen_inv simp del:group_hom.hom_inv hom_inv)
next
case (gen_mult y y')
then obtain x and x'
where "y = h x" and "x \ \gens\"
and "y' = h x'" and "x' \ \gens\" by auto
moreover
hence "x \ carrier G" and "x' \ carrier G" using `gens \ carrier G`
by (auto dest:G.gen_span_closed)
ultimately show ?case
by (auto intro:hom_mult[THEN sym] rev_image_eqI gen_span.gen_mult simp del:group_hom.hom_mult hom_mult)
qed(auto intro:rev_image_eqI intro:gen_span.intros)
qed
subsection {* Product of a list of group elements *}
text {* Not strictly related to generators of groups, this is still a general
group concept and not related to FreeGroups. *}
abbreviation (in monoid) m_concat
where "m_concat l \ foldr (op \) l \"
lemma (in monoid) m_concat_closed[simp]:
"set l \ carrier G \ m_concat l \ carrier G"
by (induct l, auto)
lemma (in monoid) m_concat_append[simp]:
assumes "set a \ carrier G"
and "set b \ carrier G"
shows "m_concat (a@b) = m_concat a \ m_concat b"
using assms
by(induct a)(auto simp add: m_assoc)
lemma (in monoid) m_concat_cons[simp]:
"\ x \ carrier G ; set xs \ carrier G \ \ m_concat (x#xs) = x \ m_concat xs"
by(induct xs)(auto simp add: m_assoc)
lemma (in monoid) nat_pow_mult1l:
assumes x: "x \ carrier G"
shows "x \ x (^) n = x (^) Suc n"
proof-
have "x \ x (^) n = x (^) (1::nat) \ x (^) n " using x by auto
also have "\ = x (^) (1 + n)" using x
by (auto dest:nat_pow_mult simp del:One_nat_def)
also have "\ = x (^) Suc n" by simp
finally show "x \ x (^) n = x (^) Suc n" .
qed
lemma (in monoid) m_concat_power[simp]: "x \ carrier G \ m_concat (replicate n x) = x (^) n"
by(induct n, auto simp add:nat_pow_mult1l)
subsection {* Isomorphisms *}
text {* Nicer way of proving that something is a group homomorphism or isomorphism *}
lemma group_homI[intro]:
assumes range: "h ` (carrier g1) \ carrier g2"
and hom: "\x\carrier g1. \y\carrier g1. h (x \\<^bsub>g1\<^esub> y) = h x \\<^bsub>g2\<^esub> h y"
shows "h \ hom g1 g2"
proof-
have "h \ carrier g1 \ carrier g2" using range by auto
thus "h \ hom g1 g2" using hom unfolding hom_def by auto
qed
lemma (in group_hom) hom_injI:
assumes "\x\carrier G. h x = \\<^bsub>H\<^esub> \ x = \\<^bsub>G\<^esub>"
shows "inj_on h (carrier G)"
unfolding inj_on_def
proof(rule ballI, rule ballI, rule impI)
fix x
fix y
assume x: "x\carrier G"
and y: "y\carrier G"
and "h x = h y"
hence "h (x \ inv y) = \\<^bsub>H\<^esub>" and "x \ inv y \ carrier G"
by auto
with assms
have "x \ inv y = \" by auto
thus "x = y" using x and y
by(auto dest: G.inv_equality)
qed
lemma group_isoI[intro]:
assumes G: "group G"
and H: "group H"
and inj1: "\x\carrier G. h x = \\<^bsub>H\<^esub> \ x = \\<^bsub>G\<^esub>"
and surj: "h ` (carrier G) = carrier H"
and hom: "\x\carrier G. \y\carrier G. h (x \\<^bsub>G\<^esub> y) = h x \\<^bsub>H\<^esub> h y"
shows "h \ G \ H"
proof-
from surj
have "h \