Theory Lyndon_Addition

(*  Title:      Combinatorics_Words_Lyndon.Lyndon_Addition
    Author:     Štěpán Holub, Charles University
    Author:     Štěpán Starosta, CTU in Prague

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

theory Lyndon_Addition
  imports Lyndon Szpilrajn.Szpilrajn

begin

subsection "The minimal relation"

text ‹We define the minimal relation which guarantees the lexicographic minimality of w compared to its
nontrivial conjugates.›

inductive_set rotate_rel :: "'a list ⇒ 'a rel" for w
  where  "0 < n ⟹ n < ❙|w❙| ⟹ (mismatch_pair w (rotate n w)) ∈ rotate_rel w"

text‹A word is Lyndon iff the corresponding order of letters is compatible with  @{term "rotate_rel w"}.›

lemma (in linorder) rotate_rel_iff: assumes "w ≠ ε"
  shows  "Lyndon w ⟷ rotate_rel w ⊆ {(x,y). x < y}" (is "?L ⟷ ?R")
proof
  assume "Lyndon w" show "rotate_rel w ⊆ {(x,y). x < y}"
  proof
    fix  x assume "x ∈ rotate_rel w"
    then obtain n where "x = mismatch_pair w (rotate n w)" and "0 < n" and "n < ❙|w❙|"
      using rotate_rel.cases by blast
    have "w <lex rotate n w"
      using LyndonD[OF ‹Lyndon w› ‹0 < n› ‹n < ❙|w❙|›].
    from this[unfolded lexordp_conv_lexord]
      prim_no_rotate[OF Lyndon_prim[OF ‹Lyndon w›] ‹0 < n›  ‹n < ❙|w❙|›]
    show "x ∈ {(a, b). a < b}"
      using lexord_mismatch[of w "rotate n w" "{(a,b). a < b}", folded ‹x = mismatch_pair w (rotate n w)›]
        ‹rotate n w ≠ w› rotate_comp_eq[of w n]
      unfolding irrefl_def by blast
  qed
next
  assume "?R"
  show "?L"
    unfolding Lyndon.simps
  proof(simp add: assms)
    have "w <lex rotate n w" if "0 < n"  "n < ❙|w❙|" for n
    proof-
      have "¬ w ⨝ rotate n w"
        using rotate_comp_eq[of w n] subsetD[OF ‹?R›, OF rotate_rel.intros[OF ‹0 < n› ‹n < ❙|w❙|›]]
          mismatch_pair_lcp[of w "rotate n w"] by fastforce
      from mismatch_lexord_linorder[OF this subsetD[OF ‹?R›, OF rotate_rel.intros[OF ‹0 < n› ‹n < ❙|w❙|›]]]
      show "w <lex rotate n w".
    qed
    thus "∀n. 0 < n ∧ n < ❙|w❙| ⟶ w <lex rotate n w"  by blast
  qed
qed

text‹It is well known that an acyclic order can be extended to a total strict linear order. This means that
a word is Lyndon with respect to some order iff its @{term "rotate_rel w"} is acyclic.
›
lemma Lyndon_rotate_rel_iff:
  "acyclic (rotate_rel w) ⟷ (∃ r. strict_linear_order r ∧ rotate_rel w ⊆ r)" (is "?L ⟷ ?R")
proof
  assume "?R" thus "?L"
    unfolding strict_linear_order_on_def acyclic_def irrefl_def
    using trancl_id trancl_mono by metis
next
  assume "?L" thus "?R"
    using acyclic_order_extension by auto
qed

lemma slo_linorder: "strict_linear_order r ⟹ class.linorder (λ a b. (a,b) ∈ r⇧=) (λ a b. (a,b) ∈ r)"
    unfolding strict_linear_order_on_def strict_partial_order_def irrefl_def trans_def total_on_def
    by unfold_locales blast+

text‹Application examples›

lemma assumes "w ≠ ε" and "acyclic (rotate_rel w)" shows "primitive w"
proof-
  obtain r where "strict_linear_order r" and "rotate_rel w ⊆ r"
    using Lyndon_rotate_rel_iff assms by blast

  interpret r: linorder "λ a b. (a,b) ∈ r⇧=" "λ a b. (a,b) ∈ r"
    using slo_linorder[OF ‹strict_linear_order r›].

  have "r.Lyndon w"
    using r.rotate_rel_iff[OF ‹w ≠ ε›] ‹rotate_rel w ⊆ r› by blast

  from r.Lyndon_prim[OF this]
  show "primitive w".

qed

lemma assumes "w ≠ ε" and "acyclic (rotate_rel w)" shows "¬ bordered w"
proof-
  obtain r where "strict_linear_order r" and "rotate_rel w ⊆ r"
    using Lyndon_rotate_rel_iff assms by blast

  interpret r: linorder "λ a b. (a,b) ∈ r⇧=" "λ a b. (a,b) ∈ r"
    using slo_linorder[OF ‹strict_linear_order r›].

  have "r.Lyndon w"
    using r.rotate_rel_iff[OF ‹w ≠ ε›] ‹rotate_rel w ⊆ r› by blast

  from r.Lyndon_unbordered[OF this]
  show "¬ bordered w".
qed

end