Theory Free_Group_F2
theory Free_Group_F2
imports
BT_Prelim
"Free-Groups.FreeGroups"
begin
section ‹Two-element generator type›
text ‹
We pick a concrete two-element type for the generators of ‹F⇩2›.
›
datatype gen2 = A | B
abbreviation Gen2 :: "gen2 set" where
"Gen2 ≡ {A, B}"
lemma Gen2_finite [simp]: "finite Gen2"
by simp
lemma Gen2_card [simp]: "card Gen2 = 2"
by simp
lemma Gen2_UNIV: "Gen2 = (UNIV :: gen2 set)"
using gen2.exhaust by auto
section ‹The free group ‹F⇩2› and its carrier›
abbreviation F2 :: "(bool × gen2) list monoid" where
"F2 ≡ ℱ⇘Gen2⇙"
text ‹The carrier of ‹F⇩2› consists of cancelled words over the alphabet
‹UNIV × Gen2 = UNIV × UNIV›.›
lemma F2_is_group: "group F2"
by (rule free_group_is_group)
lemma F2_carrier_iff:
"w ∈ carrier F2 ⟷ w ∈ lists (UNIV × Gen2) ∧ canceled w"
by (auto simp: free_group_def)
lemma F2_carrier_alt:
"carrier F2 = {w. canceled w}"
proof -
have "lists (UNIV × Gen2) = (UNIV :: (bool × gen2) list set)"
using Gen2_UNIV by auto
thus ?thesis by (auto simp: free_group_def)
qed
lemma in_F2_canceled [dest]:
assumes "w ∈ carrier F2"
shows "canceled w"
using assms by (simp add: F2_carrier_alt)
lemma canceled_in_F2 [intro]:
assumes "canceled w"
shows "w ∈ carrier F2"
using assms by (simp add: F2_carrier_alt)
lemma canceled_iff_no_adjacent_canceling:
"canceled w ⟷ (∀i. Suc i < length w ⟶ ¬ canceling (w ! i) (w ! Suc i))"
proof
assume c: "canceled w"
show "∀i. Suc i < length w ⟶ ¬ canceling (w ! i) (w ! Suc i)"
proof (intro allI impI notI)
fix i
assume len: "Suc i < length w" and can: "canceling (w ! i) (w ! Suc i)"
have "cancels_to_1_at i w (cancel_at i w)"
using len can by (auto simp: cancels_to_1_at_def)
hence "cancels_to_1 w (cancel_at i w)"
unfolding cancels_to_1_def by blast
hence "Domainp cancels_to_1 w"
by auto
with c show False
by (simp add: canceled_def)
qed
next
assume no_adj: "∀i. Suc i < length w ⟶ ¬ canceling (w ! i) (w ! Suc i)"
show "canceled w"
proof (simp add: canceled_def, intro notI)
assume "Domainp cancels_to_1 w"
then obtain w' where "cancels_to_1 w w'"
by auto
then obtain i where "cancels_to_1_at i w w'"
unfolding cancels_to_1_def by auto
hence "Suc i < length w" and "canceling (w ! i) (w ! Suc i)"
by (auto simp: cancels_to_1_at_def)
with no_adj show False
by blast
qed
qed
lemma canceled_Cons_iff:
"canceled (p # w) ⟷ canceled w ∧ (w = [] ∨ ¬ canceling p (hd w))"
unfolding canceled_iff_no_adjacent_canceling
by (cases w)
(auto simp: nth_Cons split: nat.splits)
lemma F2_ConsD:
assumes "p # w ∈ carrier F2"
shows "w ∈ carrier F2" and "w = [] ∨ ¬ canceling p (hd w)"
using assms by (simp_all add: F2_carrier_alt canceled_Cons_iff)
lemma F2_ConsI:
assumes "w ∈ carrier F2" and "w = [] ∨ ¬ canceling p (hd w)"
shows "p # w ∈ carrier F2"
using assms by (simp add: F2_carrier_alt canceled_Cons_iff)
lemma F2_one [simp]: "𝟭⇘F2⇙ = []"
by (simp add: free_group_def)
lemma F2_mult: "x ⊗⇘F2⇙ y = normalize (x @ y)"
by (simp add: free_group_def)
section ‹The four ``starts-with'' classes of ‹F⇩2››
text ‹
A non-empty reduced word in ‹F⇩2› begins with one of four
letters: ‹a›, ‹a⇧-⇧1›, ‹b›, or
‹b⇧-⇧1›. The corresponding ``starts-with'' classes
partition ‹F⇩2 \\ {1}›.
›
definition starts_with :: "bool ⇒ gen2 ⇒ (bool × gen2) list set" where
"starts_with b x = {w ∈ carrier F2. w ≠ [] ∧ hd w = (b, x)}"
abbreviation S_a :: "(bool × gen2) list set" where "S_a ≡ starts_with False A"
abbreviation S_aI :: "(bool × gen2) list set" where "S_aI ≡ starts_with True A"
abbreviation S_b :: "(bool × gen2) list set" where "S_b ≡ starts_with False B"
abbreviation S_bI :: "(bool × gen2) list set" where "S_bI ≡ starts_with True B"
lemma starts_with_subset: "starts_with b x ⊆ carrier F2"
by (auto simp: starts_with_def)
lemma starts_with_disjoint:
assumes "(b1, x1) ≠ (b2, x2)"
shows "starts_with b1 x1 ∩ starts_with b2 x2 = {}"
using assms by (auto simp: starts_with_def)
lemma starts_with_pairwise_disjoint:
shows "S_a ∩ S_aI = {}" "S_a ∩ S_b = {}" "S_a ∩ S_bI = {}"
"S_aI ∩ S_b = {}" "S_aI ∩ S_bI = {}" "S_b ∩ S_bI = {}"
"[] ∉ S_a" "[] ∉ S_aI" "[] ∉ S_b" "[] ∉ S_bI"
by (auto simp: starts_with_def)
text ‹
The four classes together with the singleton ‹{1}› partition the
carrier of ‹F⇩2›. The proof is a case analysis on the head
of a reduced word.
›
lemma F2_decomposition:
"carrier F2 = {[]} ∪ S_a ∪ S_aI ∪ S_b ∪ S_bI"
proof
show "{[]} ∪ S_a ∪ S_aI ∪ S_b ∪ S_bI ⊆ carrier F2"
using starts_with_subset
by (auto simp: F2_carrier_alt empty_canceled)
next
show "carrier F2 ⊆ {[]} ∪ S_a ∪ S_aI ∪ S_b ∪ S_bI"
proof
fix w assume w: "w ∈ carrier F2"
show "w ∈ {[]} ∪ S_a ∪ S_aI ∪ S_b ∪ S_bI"
proof (cases w)
case Nil thus ?thesis by simp
next
case (Cons a u)
obtain b x where head: "a = (b, x)" by (cases a) auto
from w have "x ∈ Gen2" using Cons head
by (auto simp: F2_carrier_iff)
hence "x = A ∨ x = B" by auto
with Cons head w show ?thesis
unfolding starts_with_def by auto
qed
qed
qed
section ‹The two distinguished generators ‹a› and ‹b››
abbreviation a_elt :: "(bool × gen2) list" where "a_elt ≡ [(False, A)]"
abbreviation aI_elt :: "(bool × gen2) list" where "aI_elt ≡ [(True, A)]"
abbreviation b_elt :: "(bool × gen2) list" where "b_elt ≡ [(False, B)]"
abbreviation bI_elt :: "(bool × gen2) list" where "bI_elt ≡ [(True, B)]"
lemma single_letter_canceled:
"canceled [(b, x)]"
by simp
lemma a_elt_in_F2 [simp]: "a_elt ∈ carrier F2"
by (intro canceled_in_F2 single_letter_canceled)
lemma aI_elt_in_F2 [simp]: "aI_elt ∈ carrier F2"
by (intro canceled_in_F2 single_letter_canceled)
lemma b_elt_in_F2 [simp]: "b_elt ∈ carrier F2"
by (intro canceled_in_F2 single_letter_canceled)
lemma bI_elt_in_F2 [simp]: "bI_elt ∈ carrier F2"
by (intro canceled_in_F2 single_letter_canceled)
lemma inv_a_eq_aI: "inv⇘F2⇙ a_elt = aI_elt"
by (simp add: inv_fg_def inv1_def)
lemma inv_b_eq_bI: "inv⇘F2⇙ b_elt = bI_elt"
by (simp add: inv_fg_def inv1_def)
lemma inv_aI_eq_a: "inv⇘F2⇙ aI_elt = a_elt"
by (simp add: inv_fg_def inv1_def)
lemma inv_bI_eq_b: "inv⇘F2⇙ bI_elt = b_elt"
by (simp add: inv_fg_def inv1_def)
end