Theory FreeGroups

section ‹The Free Group›

theory "FreeGroups"
imports
   "HOL-Algebra.Group"
   Cancelation
   Generators
begin

text ‹
Based on the work in @{theory "Free-Groups.Cancelation"}, the free group is now easily defined
over the set of fully canceled words with the corresponding operations.
›

subsection ‹Inversion›

text ‹
To define the inverse of a word, we first create a helper function that inverts
a single generator, and show that it is self-inverse.
›

definition inv1 :: "'a g_i ⇒ 'a g_i"
 where "inv1 = apfst Not"

lemma inv1_inv1: "inv1 ∘ inv1 = id"
  by (simp add: fun_eq_iff comp_def inv1_def)

lemmas inv1_inv1_simp [simp] = inv1_inv1[unfolded id_def]

lemma snd_inv1: "snd ∘ inv1 = snd"
  by(simp add: fun_eq_iff comp_def inv1_def)

text ‹
The inverse of a word is obtained by reversing the order of the generators and
inverting each generator using @{term inv1}. Some properties of @{term inv_fg}
are noted.
›

definition inv_fg :: "'a word_g_i ⇒ 'a word_g_i"
 where "inv_fg l = rev (map inv1 l)"

lemma cancelling_inf[simp]: "canceling (inv1 a) (inv1 b) = canceling a b"
  by(simp add: canceling_def inv1_def)

lemma inv_idemp: "inv_fg (inv_fg l) = l"
  by (auto simp add:inv_fg_def rev_map)

lemma inv_fg_cancel: "normalize (l @ inv_fg l) = []"
proof(induct l rule:rev_induct)
  case Nil thus ?case
    by (auto simp add: inv_fg_def)
next
  case (snoc x xs)
  have "canceling x (inv1 x)" by (simp add:inv1_def canceling_def)
  moreover
  let ?i = "length xs"
  have "Suc ?i < length xs + 1 + 1 + length xs"
    by auto
  moreover
  have "inv_fg (xs @ [x]) = [inv1 x] @ inv_fg xs"
    by (auto simp add:inv_fg_def)
  ultimately
  have "cancels_to_1_at ?i (xs @ [x] @ (inv_fg (xs @ [x]))) (xs @ inv_fg xs)"
    by (auto simp add:cancels_to_1_at_def cancel_at_def nth_append)
  hence "cancels_to_1 (xs @ [x] @ (inv_fg (xs @ [x]))) (xs @ inv_fg xs)"
    by (auto simp add: cancels_to_1_def)
  hence "cancels_to (xs @ [x] @ (inv_fg (xs @ [x]))) (xs @ inv_fg xs)"
    by (auto simp add:cancels_to_def)
  with ‹normalize (xs @ (inv_fg xs)) = []›
  show "normalize ((xs @ [x]) @ (inv_fg (xs @ [x]))) = []"
    by auto
qed

lemma inv_fg_cancel2: "normalize (inv_fg l @ l) = []"
proof-
  have "normalize (inv_fg l @ inv_fg (inv_fg l)) = []" by (rule inv_fg_cancel)
  thus "normalize (inv_fg l @ l) = []" by (simp add: inv_idemp)
qed

lemma canceled_rev:
  assumes "canceled l"
  shows "canceled (rev l)"
proof(rule ccontr)
  assume "¬canceled (rev l)"
  hence "Domainp cancels_to_1 (rev l)" by (simp add: canceled_def)
  then obtain l' where "cancels_to_1 (rev l) l'" by auto
  then obtain i where "cancels_to_1_at i (rev l) l'" by (auto simp add:cancels_to_1_def)
  hence "Suc i < length (rev l)"
    and "canceling (rev l ! i) (rev l ! Suc i)"
    by (auto simp add:cancels_to_1_at_def)
  let ?x = "length l - i - 2"
  from ‹Suc i < length (rev l)›
  have "Suc ?x < length l" by auto
  moreover
  from ‹Suc i < length (rev l)›
  have "i < length l" and "length l - Suc i = Suc(length l - Suc (Suc i))" by auto
  hence "rev l ! i = l ! Suc ?x" and "rev l ! Suc i = l ! ?x"
    by (auto simp add: rev_nth map_nth)
  with ‹canceling (rev l ! i) (rev l ! Suc i)›
  have "canceling (l ! Suc ?x) (l ! ?x)" by auto
  hence "canceling (l ! ?x) (l ! Suc ?x)" by (rule cancel_sym)
  hence "canceling (l ! ?x) (l ! Suc ?x)" by simp
  ultimately
  have "cancels_to_1_at ?x l (cancel_at ?x l)" 
    by (auto simp add:cancels_to_1_at_def)
  hence "cancels_to_1 l (cancel_at ?x l)"
    by (auto simp add:cancels_to_1_def)
  hence "¬canceled l"
    by (auto simp add:canceled_def)
  with ‹canceled l› show False by contradiction
qed

lemma inv_fg_closure1:
  assumes "canceled l"
  shows "canceled (inv_fg l)"
unfolding inv_fg_def and inv1_def and apfst_def
proof-
  have "inj Not" by (auto intro:injI)
  moreover
  have "inj_on id (snd ` set l)" by auto
  ultimately
  have "canceled (map (map_prod Not id) l)" 
    using ‹canceled l› 
    by -(rule rename_gens_canceled)
  thus "canceled (rev (map (map_prod Not id) l))" by (rule canceled_rev)
qed

lemma inv_fg_closure2:
  "l ∈ lists (UNIV × gens) ⟹ inv_fg l ∈ lists (UNIV × gens)"
  by (auto iff:lists_eq_set simp add:inv1_def inv_fg_def)

subsection ‹The definition›

text ‹
Finally, we can define the Free Group over a set of generators, and show that it
is indeed a group.
›

definition free_group :: "'a set => ((bool * 'a) list) monoid" (‹ℱı›)
where 
  "ℱ⇘gens⇙ ≡ ⦇
     carrier = {l∈lists (UNIV × gens). canceled l },
     mult = λ x y. normalize (x @ y),
     one = []
  ⦈"


lemma occuring_gens_in_element:
  "x ∈ carrier ℱ⇘gens⇙ ⟹ x ∈ lists (UNIV × gens)"
by(auto simp add:free_group_def)

theorem free_group_is_group: "group ℱ⇘gens⇙"
proof
  fix x y
  assume "x ∈ carrier ℱ⇘gens⇙" hence x: "x ∈ lists (UNIV × gens)" by
    (rule occuring_gens_in_element)
  assume "y ∈ carrier ℱ⇘gens⇙" hence y: "y ∈ lists (UNIV × gens)" by
    (rule occuring_gens_in_element)
  from x and y
  have "x ⊗⇘ℱ⇘gens⇙⇙ y ∈ lists (UNIV × gens)"
    by (auto intro!: normalize_preserves_generators simp add:free_group_def append_in_lists_conv)
  thus "x ⊗⇘ℱ⇘gens⇙⇙ y ∈ carrier ℱ⇘gens⇙"
    by (auto simp add:free_group_def)
next
  fix x y z
  have "cancels_to (x @ y) (normalize (x @ (y::'a word_g_i)))"
   and "cancels_to z (z::'a word_g_i)"
    by auto
  hence "normalize (normalize (x @ y) @ z) = normalize ((x @ y) @ z)"
    by (rule normalize_append_cancel_to[THEN sym])
  also
  have "… = normalize (x @ (y @ z))" by auto
  also
  have "cancels_to (y @ z) (normalize (y @ (z::'a word_g_i)))"
   and "cancels_to x (x::'a word_g_i)"
    by auto
  hence "normalize (x @ (y @ z)) = normalize (x @ normalize (y @ z))"
    by -(rule normalize_append_cancel_to)
  finally
  show "x ⊗⇘ℱ⇘gens⇙⇙ y ⊗⇘ℱ⇘gens⇙⇙ z =
        x ⊗⇘ℱ⇘gens⇙⇙ (y ⊗⇘ℱ⇘gens⇙⇙ z)"
    by (auto simp add:free_group_def)
next
  show "𝟭⇘ℱ⇘gens⇙⇙ ∈ carrier ℱ⇘gens⇙"
    by (auto simp add:free_group_def)
next
  fix x
  assume "x ∈ carrier ℱ⇘gens⇙"
  thus "𝟭⇘ℱ⇘gens⇙⇙ ⊗⇘ℱ⇘gens⇙⇙ x = x"
    by (auto simp add:free_group_def)
next
  fix x
  assume "x ∈ carrier ℱ⇘gens⇙"
  thus "x ⊗⇘ℱ⇘gens⇙⇙ 𝟭⇘ℱ⇘gens⇙⇙ = x"
    by (auto simp add:free_group_def)
next
  show "carrier ℱ⇘gens⇙ ⊆ Units ℱ⇘gens⇙"
  proof (simp add:free_group_def Units_def, rule subsetI)
    fix x :: "'a word_g_i"
    let ?x' = "inv_fg x"
    assume "x ∈ {y∈lists(UNIV×gens). canceled y}"
    hence "?x' ∈ lists(UNIV×gens) ∧ canceled ?x'"
      by (auto elim:inv_fg_closure1 simp add:inv_fg_closure2)
    moreover
    have "normalize (?x' @ x) = []"
     and "normalize (x @ ?x') = []"
      by (auto simp add:inv_fg_cancel inv_fg_cancel2)
    ultimately
    have "∃y. y ∈ lists (UNIV × gens) ∧
                  canceled y ∧
                  normalize (y @ x) = [] ∧ normalize (x @ y) = []"
      by auto
    with ‹x ∈ {y∈lists(UNIV×gens). canceled y}›
    show "x ∈ {y ∈ lists (UNIV × gens).  canceled y  ∧
          (∃x. x ∈ lists (UNIV × gens) ∧
                  canceled x ∧
                  normalize (x @ y) = [] ∧ normalize (y @ x) = [])}"
      by auto
  qed
qed

lemma inv_is_inv_fg[simp]:
  "x ∈ carrier ℱ⇘gens⇙ ⟹ inv⇘ℱ⇘gens⇙⇙ x = inv_fg x"
by (rule group.inv_equality,auto simp add:free_group_is_group,auto simp add: free_group_def inv_fg_cancel inv_fg_cancel2 inv_fg_closure1 inv_fg_closure2)


subsection ‹The universal property›

text ‹Free Groups are important due to their universal property: Every map of
the set of generators to another group can be extended uniquely to an
homomorphism from the Free Group.›

definition insert (‹ι›)
  where "ι g = [(False, g)]"

lemma insert_closed:
  "g ∈ gens ⟹ ι g ∈ carrier ℱ⇘gens⇙"
  by (auto simp add:insert_def free_group_def)

definition (in group) lift_gi
  where "lift_gi f gi = (if fst gi then inv (f (snd gi)) else f (snd gi))"

lemma (in group) lift_gi_closed:
  assumes cl: "f ∈ gens → carrier G"
      and "snd gi ∈ gens"
  shows "lift_gi f gi ∈ carrier G"
using assms by (auto simp add:lift_gi_def)

definition (in group) lift
  where "lift f w = m_concat (map (lift_gi f) w)"

lemma (in group) lift_nil[simp]: "lift f [] = 𝟭"
 by (auto simp add:lift_def)

lemma (in group) lift_closed[simp]:
  assumes cl: "f ∈ gens → carrier G"
      and "x ∈ lists (UNIV × gens)"
  shows "lift f x ∈ carrier G"
proof-
  have "set (map (lift_gi f) x) ⊆ carrier G"
    using ‹x ∈ lists (UNIV × gens)›
    by (auto simp add:lift_gi_closed[OF cl])
  thus "lift f x ∈ carrier G"
    by (auto simp add:lift_def)
qed

lemma (in group) lift_append[simp]:
  assumes cl: "f ∈ gens → carrier G"
      and "x ∈ lists (UNIV × gens)"
      and "y ∈ lists (UNIV × gens)"
  shows "lift f (x @ y) = lift f x ⊗ lift f y"
proof-
  from ‹x ∈ lists (UNIV × gens)›
  have "set (map snd x) ⊆ gens" by auto
  hence "set (map (lift_gi f) x) ⊆ carrier G"
    by (induct x)(auto simp add:lift_gi_closed[OF cl])
  moreover
  from ‹y ∈ lists (UNIV × gens)›
  have "set (map snd y) ⊆ gens" by auto
  hence "set (map (lift_gi f) y) ⊆ carrier G"
    by (induct y)(auto simp add:lift_gi_closed[OF cl])
  ultimately
  show "lift f (x @ y) = lift f x ⊗ lift f y"
    by (auto simp add:lift_def m_assoc simp del:set_map foldr_append)
qed

lemma (in group) lift_cancels_to:
  assumes "cancels_to x y"
      and "x ∈ lists (UNIV × gens)"
      and cl: "f ∈ gens → carrier G"
  shows "lift f x = lift f y"
using assms
unfolding cancels_to_def
proof(induct rule:rtranclp_induct)
  case (step y z)
    from ‹cancels_to_1⇧*⇧* x y›
    and ‹x ∈ lists (UNIV × gens)›
    have "y ∈ lists (UNIV × gens)"
      by -(rule cancels_to_preserves_generators, simp add:cancels_to_def)
    hence "lift f x = lift f y"
      using step by auto
    also
    from ‹cancels_to_1 y z›
    obtain ys1 y1 y2 ys2
      where y: "y = ys1 @ y1 # y2 # ys2"
      and "z = ys1 @ ys2"
      and "canceling y1 y2"
    by (rule cancels_to_1_unfold)
    have "lift f y  = lift f (ys1 @ [y1] @ [y2] @ ys2)"
      using y by simp
    also
    from y and cl and ‹y ∈ lists (UNIV × gens)›
    have "lift f (ys1 @ [y1] @ [y2] @ ys2)
        = lift f ys1 ⊗ (lift f [y1] ⊗ lift f [y2]) ⊗ lift f ys2"
      by (auto intro:lift_append[OF cl] simp del: append_Cons simp add:m_assoc iff:lists_eq_set)
    also
    from cl[THEN funcset_image]
     and y and ‹y ∈ lists (UNIV × gens)›
     and ‹canceling y1 y2›
    have "(lift f [y1] ⊗ lift f [y2]) = 𝟭"
      by (auto simp add:lift_def lift_gi_def canceling_def iff:lists_eq_set)
    hence "lift f ys1 ⊗ (lift f [y1] ⊗ lift f [y2]) ⊗ lift f ys2
           = lift f ys1 ⊗ 𝟭 ⊗ lift f ys2"
      by simp
    also
    from y and ‹y ∈ lists (UNIV × gens)›
     and cl
     have "lift f ys1 ⊗ 𝟭 ⊗ lift f ys2 = lift f (ys1 @ ys2)"
      by (auto intro:lift_append iff:lists_eq_set)
    also
    from ‹z = ys1 @ ys2›
    have "lift f (ys1 @ ys2) = lift f z" by simp
    finally show "lift f x = lift f z" .
qed auto

lemma (in group) lift_is_hom:
  assumes cl: "f ∈ gens → carrier G"
  shows "lift f ∈ hom ℱ⇘gens⇙ G"
proof-
  {
    fix x
    assume "x ∈ carrier ℱ⇘gens⇙"
    hence "x ∈ lists (UNIV × gens)"
      unfolding free_group_def by simp
    hence "lift f x ∈ carrier G"
     by (induct x, auto simp add:lift_def lift_gi_closed[OF cl])
  } 
  moreover
  { fix x
    assume "x ∈ carrier ℱ⇘gens⇙"
    fix y
    assume "y ∈ carrier ℱ⇘gens⇙"

    from ‹x ∈ carrier ℱ⇘gens⇙› and ‹y ∈ carrier ℱ⇘gens⇙›
    have "x ∈ lists (UNIV × gens)" and "y ∈ lists (UNIV × gens)"
      by (auto simp add:free_group_def)

    have "cancels_to (x @ y) (normalize (x @ y))" by simp
    from ‹x ∈ lists (UNIV × gens)› and ‹y ∈ lists (UNIV × gens)›
     and lift_cancels_to[THEN sym, OF ‹cancels_to (x @ y) (normalize (x @ y))›] and cl
    have "lift f (x ⊗⇘ℱ⇘gens⇙⇙ y) = lift f (x @ y)"
      by (auto simp add:free_group_def iff:lists_eq_set)
    also
    from ‹x ∈ lists (UNIV × gens)› and ‹y ∈ lists (UNIV × gens)› and cl
    have "lift f (x @ y) = lift f x ⊗ lift f y"
      by simp
    finally
    have "lift f (x ⊗⇘ℱ⇘gens⇙⇙ y) = lift f x ⊗ lift f y" .
  }
  ultimately
  show "lift f ∈ hom ℱ⇘gens⇙ G"
    by auto
qed

lemma gens_span_free_group:
shows "⟨ι ` gens⟩⇘ℱ⇘gens⇙⇙ = carrier ℱ⇘gens⇙"
proof
  interpret group "ℱ⇘gens⇙" by (rule free_group_is_group)
  show "⟨ι ` gens⟩⇘ℱ⇘gens⇙⇙ ⊆ carrier ℱ⇘gens⇙"
  by(rule gen_span_closed, auto simp add:insert_def free_group_def)

  show "carrier ℱ⇘gens⇙  ⊆ ⟨ι ` gens⟩⇘ℱ⇘gens⇙⇙"
  proof
    fix x
    show "x ∈ carrier ℱ⇘gens⇙ ⟹ x ∈ ⟨ι ` gens⟩⇘ℱ⇘gens⇙⇙"
    proof(induct x)
    case Nil
      have "one ℱ⇘gens⇙ ∈ ⟨ι ` gens⟩⇘ℱ⇘gens⇙⇙"
        by simp
      thus "[] ∈ ⟨ι ` gens⟩⇘ℱ⇘gens⇙⇙"
        by (simp add:free_group_def)
    next
    case (Cons a x)
      from ‹a # x ∈ carrier ℱ⇘gens⇙›
      have "x ∈ carrier ℱ⇘gens⇙"
        by (auto intro:cons_canceled simp add:free_group_def)
      hence "x ∈ ⟨ι ` gens⟩⇘ℱ⇘gens⇙⇙"
        using Cons by simp
      moreover

      from ‹a # x ∈ carrier ℱ⇘gens⇙›
      have "snd a ∈ gens"
        by (auto simp add:free_group_def)
      hence isa: "ι (snd a) ∈ ⟨ι ` gens⟩⇘ℱ⇘gens⇙⇙"
        by (auto simp add:insert_def intro:gen_gens)
      have "[a] ∈ ⟨ι ` gens⟩⇘ℱ⇘gens⇙⇙"
      proof(cases "fst a")
        case False
          hence "[a] = ι (snd a)" by (cases a, auto simp add:insert_def)
           with isa show "[a] ∈ ⟨ι ` gens⟩⇘ℱ⇘gens⇙⇙" by simp
       next
        case True
          from ‹snd a ∈ gens›
          have "ι (snd a) ∈ carrier ℱ⇘gens⇙" 
            by (auto simp add:free_group_def insert_def)
          with True
          have "[a] = inv⇘ℱ⇘gens⇙⇙ (ι (snd a))"
            by (cases a, auto simp add:insert_def inv_fg_def inv1_def)
          moreover
          from isa
          have "inv⇘ℱ⇘gens⇙⇙ (ι (snd a)) ∈ ⟨ι ` gens⟩⇘ℱ⇘gens⇙⇙"
            by (auto intro:gen_inv)
          ultimately
          show "[a] ∈ ⟨ι ` gens⟩⇘ℱ⇘gens⇙⇙"
            by simp
      qed
      ultimately 
      have "mult ℱ⇘gens⇙ [a] x ∈ ⟨ι ` gens⟩⇘ℱ⇘gens⇙⇙"
        by (auto intro:gen_mult)
      with
      ‹a # x ∈ carrier ℱ⇘gens⇙›
      show "a # x ∈ ⟨ι ` gens⟩⇘ℱ⇘gens⇙⇙" by (simp add:free_group_def)
    qed
  qed
qed

lemma (in group) lift_is_unique:
  assumes "group G"
  and cl: "f ∈ gens → carrier G"
  and "h ∈ hom ℱ⇘gens⇙ G"
  and "∀ g ∈ gens. h (ι g) = f g"
  shows "∀x ∈ carrier ℱ⇘gens⇙. h x = lift f x"
unfolding gens_span_free_group[THEN sym]
proof(rule hom_unique_on_span[of "ℱ⇘gens⇙" G])
  show "group ℱ⇘gens⇙" by (rule free_group_is_group)
next
  show "group G" by fact
next
  show "ι ` gens ⊆ carrier ℱ⇘gens⇙"
    by(auto intro:insert_closed)
next
  show "h ∈ hom ℱ⇘gens⇙ G" by fact
next
  show "lift f ∈ hom ℱ⇘gens⇙ G" by (rule lift_is_hom[OF cl])
next
  from ‹∀g∈ gens. h (ι g) = f g› and cl[THEN funcset_image]
  show "∀g∈ ι ` gens. h g = lift f g"
    by(auto simp add:insert_def lift_def lift_gi_def)
qed

end