Theory Graph_Lemma

(*  Title:      Graph Lemma
    File:       Combinatorics_Words_Graph_Lemma.Graph_Lemma
    Author:     Štěpán Holub, Charles University
    Author:     Martin Raška, Charles University

Part of Combinatorics on Words Formalized. See https://gitlab.com/formalcow/combinatorics-on-words-formalized/
*)

theory Graph_Lemma
  imports Combinatorics_Words.Submonoids Glued_Codes

begin

chapter ‹Graph Lemma›

text‹The Graph Lemma is an important tool for gaining information about systems of word equations.
It yields an upper bound on the rank of the solution, that is, on the number of factors into all images of unknowns can be factorized.
The most straightforward application is showing that a system of equations admits periodic solutions only, which
in particular holds for any nontrivial equation over two words.

The name refers to a graph whose vertices are the unknowns of the system, and edges connect front letters of the left- and right-
hand sides of equations. The bound mentioned above is then the number of connected components of the graph.

We formalize the algebraic proof from @{cite Berstel1979}. Key ingredients of the proof are in the @{theory "Combinatorics_Words_Graph_Lemma.Glued_Codes"}.›

section ‹Graph lemma›

theorem graph_lemma_last: "𝔅F G = {last (Dec (𝔅F G) g) | g. g ∈ G ∧ g ≠ ε}"
proof
  interpret code "𝔅F G"
    using free_basis_code.
  ― ‹the core is to show that each element of the free basis must be a last of some word›
  show "𝔅F G ⊆ {last (Dec 𝔅F G g) |g. g ∈ G ∧ g ≠ ε}"
  proof (rule ccontr)
    ― ‹Assume the contrary.›
    assume "¬ 𝔅F G ⊆ {last (Dec 𝔅F G g) |g. g ∈ G ∧ g ≠ ε}"
    ― ‹And let w be the not-last›
    then obtain w
      where "w ∈ 𝔅F G"
        and hd_dec_neq: "⋀g. g ∈ G ⟹ g ≠ ε ⟹ last (Dec (𝔅F G) g) ≠ w"
      by blast
    ― ‹For contradiction: We have a free hull which does not contain w but contains G.›
    have "G ⊆ ⟨glued_gens w (𝔅F G)⟩"
      by (blast intro!: gen_in_free_hull hd_dec_neq del: notI)
    then have "⟨𝔅F G⟩ ⊆ ⟨glued_gens w (𝔅F G)⟩"
      unfolding basis_gen_hull_free
      by (intro code.free_hull_min glued_gens_code ‹w ∈ 𝔅F G›)
    then show False
      using ‹w ∈ 𝔅F G› glued_not_in_glued_hull by blast
  qed
  ― ‹The opposite inclusion is easy›
  show "{last (Dec 𝔅F G g) |g. g ∈ G ∧ g ≠ ε} ⊆ 𝔅F G"
    by (auto intro!: dec_in_lists lists_hd_in_set[reversed] gen_in_free_hull del: notI)
qed

theorem graph_lemma: "𝔅F G = {hd (Dec (𝔅F G) g) | g. g ∈ G ∧ g ≠ ε}"
proof -
  have *: "rev u = last (Dec rev ` (𝔅F G) (rev g)) ∧ g ∈ G ∧ g ≠ ε
           ⟷ u = hd (Dec (𝔅F G) g) ∧ g ∈ G ∧ g ≠ ε" for u g
    by (cases "g ∈ G ∧ g ≠ ε") (simp add: gen_in_free_hull last_rev hd_map code.dec_rev, blast)
  show ?thesis
    using graph_lemma_last[reversed, of G] unfolding *.
qed

section ‹Binary code›

text ‹We illustrate the use of the Graph Lemma in an alternative proof of the fact that two non-commuting words form a code.
See also @{thm no_comm_bin_code [no_vars]} in @{theory "Combinatorics_Words.CoWBasic"}.

First, we prove a lemma which is the core of the alternative proof.›

lemma non_comm_hds_neq: assumes "u ⋅ v ≠ v ⋅ u" shows "hd (Dec 𝔅F {u,v} u) ≠ hd (Dec 𝔅F {u,v} v)"
using assms proof (rule contrapos_nn)
  assume hds_eq: "hd (Dec 𝔅F {u,v} u) = hd (Dec 𝔅F {u,v} v)"
  have **: "𝔅F {u,v} = {hd (Dec 𝔅F {u,v} u)}"
    using graph_lemma by (rule trans) (use assms in ‹auto intro: hds_eq[symmetric]›)
  show "u ⋅ v = v ⋅ u"
    by (intro comm_rootI[of _ "hd (Dec 𝔅F {u,v} u)"] sing_gen)
       (simp_all add: **[symmetric] gen_in_free_hull)
qed

theorem assumes "u ⋅ v ≠ v ⋅ u" shows "code {u, v}"
proof
  have *: "w ∈ {u, v} ⟹ w ≠ ε" for w
    using ‹u ⋅ v ≠ v ⋅ u› by blast
  fix xs ys
  show "xs ∈ lists {u, v} ⟹ ys ∈ lists {u, v} ⟹ concat xs = concat ys ⟹ xs = ys"
  proof (induction xs ys rule: list_induct2')
    case (4 x xs y ys)
      have **: "hd (Dec 𝔅F {u,v} (concat (z # zs))) = hd (Dec 𝔅F {u,v} z)"
        if "z # zs ∈ lists {u, v}" for z zs
        using that by (elim listsE) (simp del: insert_iff
          add: concat_in_hull' gen_in set_mp[OF hull_sub_free_hull]
               free_basis_dec_morph * basis_gen_hull_free)
      have "hd (Dec 𝔅F {u,v} x) = hd (Dec 𝔅F {u,v} y)"
        using "4.prems" by (simp only: **[symmetric])
      then have "x = y"
        using "4.prems"(1-2) non_comm_hds_neq[OF ‹u ⋅ v ≠ v ⋅ u›]
        by (elim listsE insertE emptyE) simp_all
      with 4 show "x # xs = y # ys" by simp
  qed (simp_all add: *)
qed

end