Theory Submonoids

(*  Title:      CoW/Submonoids.thy
    Author:     Štěpán Holub, Charles University
    Author:     Martin Raška, 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 Submonoids
  imports CoWBasic "HOL.Hull"
begin

chapter ‹Submonoids of a free monoid›

text‹This chapter deals with properties of submonoids of a free monoid, that is, with monoids of words.
See more in Chapter 1 of \cite{ Lo83}.
›

section ‹Generated monoid (also called hull)›

text‹First, we define the hull of a set of words, that is, the monoid generated by them.›

definition word_monoid where
  "word_monoid M ≡ (∀ w1 w2. w1 ∈ M ⟶ w2 ∈ M ⟶ w1 ⋅ w2 ∈ M) ∧ ε ∈ M"

lemma word_monoidI[intro]: assumes "⋀ w1 w2. w1 ∈ M ⟹ w2 ∈ M ⟹ w1 ⋅ w2 ∈ M" "ε ∈ M"
  shows "word_monoid M"
  by (simp add: assms word_monoid_def)

inductive_set hull :: "'a list set ⇒ 'a list set" ("⟨_⟩")
  for G where
    emp_in[simp]:  "ε ∈ ⟨G⟩" |
    prod_cl:  "w1 ∈ G ⟹ w2 ∈ ⟨G⟩ ⟹ w1 ⋅ w2 ∈ ⟨G⟩"

lemmas [intro] = hull.intros

lemma hull_closed[intro]: "w1 ∈ ⟨G⟩ ⟹ w2 ∈ ⟨G⟩ ⟹ w1 ⋅ w2 ∈ ⟨G⟩"
  by (rule hull.induct[of w1 G "λ x. (x⋅w2)∈⟨G⟩"]) auto+

lemma gen_in [intro]: "w ∈ G ⟹ w ∈ ⟨G⟩"
  using hull.prod_cl by force

lemma gen_monoid_monoid: "word_monoid ⟨G⟩"
  unfolding word_monoid_def using hull_closed emp_in by blast

lemma gen_monoid_hull: "word_monoid hull G = ⟨G⟩"
proof (rule hull_unique, blast, use gen_monoid_monoid in blast,rule subsetI)
  fix M x
  assume "G ⊆ M" and "word_monoid M" "x ∈ ⟨G⟩"
  show "x ∈ M"
  by (induction rule: hull.induct[OF ‹x ∈ ⟨G⟩›])
  (use ‹word_monoid M›[unfolded word_monoid_def] ‹G ⊆ M› in blast)+
qed

lemma gen_monoid_induct: assumes "x ∈ ⟨G⟩" "P ε" "⋀w. w ∈ G ⟹ P w"
  "⋀w1 w2. w1 ∈ ⟨G⟩ ⟹ P w1 ⟹ w2 ∈ ⟨G⟩ ⟹ P w2 ⟹ P (w1 ⋅ w2)" shows  "P x"
  using hull.induct[of _ _ P, OF ‹x ∈ ⟨G⟩›  ‹P ε›]
    assms by (simp add: gen_in)

lemma genset_sub[simp]: "G ⊆ ⟨G⟩"
  using gen_in ..

lemma lists_sub: "ws ∈ lists G ⟹ ws ∈ lists ⟨G⟩"
  using sub_lists_mono[OF genset_sub].

lemma in_lists_conv_set_subset: "set ws ⊆ G ⟷ ws ∈ lists G"
  unfolding in_lists_conv_set subset_code(1)..

lemma concat_in_hull [intro]:
  assumes "set ws ⊆ G"
  shows   "concat ws ∈ ⟨G⟩"
  using assms by (induction ws) auto

lemma concat_in_hull' [intro]:
  assumes "ws ∈ lists G"
  shows   "concat ws ∈ ⟨G⟩"
  using assms by (induction ws) auto

lemma hull_concat_lists0:
   "w ∈ ⟨G⟩ ⟹ ∃ ws ∈ lists G. concat ws = w" (is "w ∈ ⟨G⟩ ⟹ ?P w")
proof(rule hull.induct[of _ G])
  show "∃ws∈lists G. concat ws = w1 ⋅ w2" if "w1 ∈ G" "w2 ∈ ⟨G⟩"
 "∃ws∈lists G. concat ws = w2"  for w1 w2
    using that Cons_in_lists_iff concat.simps(2) by metis
qed (use concat_nemp in blast)+

lemma hull_concat_listsE[elim]: assumes "w ∈ ⟨G⟩"
  obtains ws where "ws ∈ lists G" and "concat ws = w"
  using assms hull_concat_lists0 by blast

lemma hull_concat_lists: "⟨G⟩ = concat ` lists G"
  using hull_concat_lists0 by blast

lemma hull_concat_lists': "⟨G⟩ = {concat xs | xs. xs ∈ lists G}"
  using Setcompr_eq_image hull_concat_lists by blast

lemma hull_mono: "A ⊆ B ⟹ ⟨A⟩ ⊆ ⟨B⟩"
  using gen_monoid_hull hull_mono by blast

lemma hull_concat_lists_nempE[elim]: assumes "w ∈ ⟨G⟩"
  obtains ws where "ws ∈ lists (G - {ε})" and "concat ws = w"
proof-
  obtain ws where "ws ∈ lists G" "concat ws = w"
    using assms by blast
  with that[of "filter (λ x. x ≠ ε) ws"]
  show thesis
    by force
qed

lemma hull_nemp_eq_hull[simp]: "⟨G - {ε}⟩ = ⟨G⟩"
  by (rule equalityI, use hull_mono in fast, rule subsetI, blast)



lemma emp_gen_set: "⟨{}⟩ = {ε}"
  unfolding hull_concat_lists by auto

lemma concat_lists_minus[simp]: "concat ` lists (G - {ε}) = concat ` lists G"
proof
  show "concat ` lists G ⊆ concat ` lists (G - {ε})"
  proof
    fix x assume "x ∈ concat ` lists G"
    from imageE[OF this]
    obtain y where "x = concat y" "y ∈ lists G".
    from lists_minus'[OF ‹y ∈ lists G›] del_emp_concat[of y, folded ‹x = concat y›]
    show "x ∈ concat ` lists (G - {ε})"
      by blast
  qed
qed (simp add: image_mono lists_mono)

lemma hull_drop_one: "⟨G - {ε}⟩ = ⟨G⟩"
proof (intro equalityI subsetI)
  fix x assume "x ∈ ⟨G⟩" thus "x ∈ ⟨G - {ε}⟩"
    unfolding  hull_concat_lists by simp
next
  fix x assume "x ∈ ⟨G - {ε}⟩" thus "x ∈ ⟨G⟩"
    unfolding  hull_concat_lists image_iff by auto
qed

lemma sing_gen_power: "u ∈ ⟨{x}⟩ ⟹ ∃k. u = x⇧^@k"
  unfolding hull_concat_lists  using one_generated_list_power by auto


lemma pow_sing_gen[simp]: "x⇧^@k ∈ ⟨{x}⟩"
  using concat_in_hull[OF sing_pow_set_sub, of _  k x] concat_pow_list_single by simp

lemma sing_gen_pow_ex_conv: "u ∈ ⟨{x}⟩ ⟷ (∃k. u = x⇧^@k)"
  using sing_gen_power pow_sing_gen by blast

lemma sing_gen_primroot_gen:  assumes "w ∈ ⟨{x}⟩"
  shows "w ∈ ⟨{ρ x}⟩"
  using sing_gen_power[OF assms] pow_sing_gen
  by (subst (asm) (1) primroot_exp_eq[of x, symmetric],
  unfold pow_mult[symmetric]) blast

lemma sing_gen_primroot_eq:
  assumes "w ∈ ⟨{x}⟩" "w ≠ ε"
  shows "ρ w = ρ x"
proof-
  have "ρ x ≠ ε"
    using assms concat.simps(1) by fastforce
  from sing_gen_primroot_gen[OF ‹w ∈ ⟨{x}⟩›]
  show "ρ w = ρ x"
    using primroot_unique[OF ‹w ≠ ε› primroot_prim[OF ‹ρ x ≠ ε›, unfolded primroot_idemp]]  sing_gen_power[OF ‹w ∈ ⟨{ρ x}⟩›] by blast
qed

lemma sing_gen_pow_conv: "w ∈ ⟨{ρ x}⟩ ⟷ w = ρ x⇧^@e⇩_ρ w"
proof (rule iffI, cases "w = ε", force)
  assume "w ∈ ⟨{ρ x}⟩" "w ≠ ε"
  have "ρ w = ρ x"
    using sing_gen_primroot_eq[OF ‹w ∈ ⟨{ρ x}⟩› ‹w ≠ ε›, unfolded primroot_idemp].
  show "w = ρ x ⇧^@ e⇩_ρ w"
    using primroot_exp_eq[of w, unfolded ‹ρ w = ρ x›, symmetric].
qed (metis pow_sing_gen)

lemma two_primroots_comm: assumes "w ≠ ε" and  "w ∈ ⟨{ρ x}⟩" and "w ∈ ⟨{ρ y}⟩"
  shows "x ⋅ y = y ⋅ x"
proof (rule comm_primrootI)
  from assms[unfolded sing_gen_pow_conv]
  show "ρ x ⋅ ρ y = ρ y ⋅ ρ x"
    using comm_drop_exps primroot_exp_nemp by metis
qed

lemma comm_rootI: "x ∈ ⟨{r}⟩ ⟹ y ∈ ⟨{r}⟩ ⟹ x ⋅ y = y ⋅ x"
  unfolding comm sing_gen_pow_ex_conv by blast


lemma sing_genE[elim]:
  assumes "u ∈ ⟨{x}⟩"
  obtains k where "x⇧^@k = u"
  using assms using sing_gen_power by blast


lemma lists_gen_to_hull: "us ∈ lists (G - {ε}) ⟹ us ∈ lists (⟨G⟩ - {ε})"
  using lists_mono genset_sub  by blast

lemma rev_hull: "rev`⟨G⟩ = ⟨rev`G⟩"
proof
  show "rev ` ⟨G⟩ ⊆ ⟨rev ` G⟩"
  proof
    fix x assume "x ∈ rev ` ⟨G⟩"
    then obtain xs where "x = rev (concat xs)" and "xs ∈ lists G"
      unfolding hull_concat_lists by auto
    from rev_in_lists[OF ‹xs ∈ lists G›]
    have "(map rev (rev xs)) ∈ lists (rev ` G)"
      by fastforce
    thus "x ∈ ⟨rev ` G⟩"
      unfolding image_iff hull_concat_lists
      using ‹x = rev (concat xs)›[unfolded rev_concat] by blast
  qed
  show "⟨rev ` G⟩ ⊆ rev ` ⟨G⟩"
  proof
    fix x assume  "x ∈  ⟨rev ` G⟩"
    then obtain xs where "x = concat xs" and "xs ∈ lists (rev ` G)"
      unfolding hull_concat_lists by blast
    from rev_in_lists[OF ‹xs ∈ lists ((rev ` G))›]
    have "map rev (rev xs) ∈ lists G"
      by fastforce
    hence "rev x ∈ ⟨G⟩"
      unfolding ‹x = concat xs› rev_concat
      by fast
    thus "x ∈ rev ` ⟨G⟩"
      unfolding rev_in_conv.
  qed
qed

lemma power_in[intro]: "x ∈ ⟨G⟩ ⟹ x⇧^@k ∈ ⟨G⟩"
  by (induction k, auto)

lemma hull_closed_lists:  "us ∈ lists ⟨G⟩ ⟹ concat us ∈ ⟨G⟩"
  by (induct us, auto)

lemma hull_I [intro]:
  "ε ∈ H ⟹ (⋀ x y. x ∈ H ⟹ y ∈ H ⟹ x ⋅ y ∈ H) ⟹ ⟨H⟩ = H"
  by (standard, use hull.induct[of _ H "λ x. x ∈ H"] in force) (simp only: genset_sub)

lemma gen_idemp: "⟨⟨G⟩⟩ = ⟨G⟩"
  using image_subsetI[of "lists ⟨G⟩" concat "⟨G⟩", unfolded hull_concat_lists[of "⟨G⟩", symmetric],
      THEN subset_antisym[OF _ genset_sub[of "⟨G⟩"]]] hull_closed_lists[of _ G] by blast

lemma hull_mono'[intro]: "A ⊆ ⟨B⟩ ⟹ ⟨A⟩ ⊆ ⟨B⟩"
  using hull_mono[of A "⟨B⟩"] unfolding gen_idemp.

lemma hull_conjug [elim]: "w ∈ ⟨{r⋅s,s⋅r}⟩ ⟹ w ∈ ⟨{r,s}⟩"
  using hull_mono[of "{r⋅s,s⋅r}" "⟨{r,s}⟩", unfolded gen_idemp] by blast

lemma root_divisor: assumes "period w k" and  "k dvd ❙|w❙|" shows "w ∈ ⟨{take k w}⟩"
  using pow_sing_gen[of "(❙|w❙| div k)" "take k w"] unfolding
    take_several_pers[OF ‹period w k›, of "❙|w❙| div k", unfolded dvd_div_mult_self[OF ‹k dvd ❙|w❙|›] take_self, OF , OF order_refl].

text‹Intersection of hulls is a hull.›

lemma hulls_inter: "⟨⋂ {⟨G⟩ | G. G ∈ S}⟩ = ⋂ {⟨G⟩ | G. G ∈ S}"
proof
  {fix G assume "G ∈ S"
    hence "⟨⋂ {⟨G⟩ |G. G ∈ S}⟩ ⊆ ⟨G⟩"
      using Inter_lower[of "⟨G⟩" "{⟨G⟩ |G. G ∈ S}"] mem_Collect_eq[of "⟨G⟩" "λ A. ∃ G. G ∈ S ∧ A = ⟨G⟩"]
        hull_mono[of "⋂ {⟨G⟩ |G. G ∈ S}" "⟨G⟩"] unfolding gen_idemp by auto}
  thus "⟨⋂ {⟨G⟩ |G. G ∈ S}⟩ ⊆ ⋂ {⟨G⟩ |G. G ∈ S}"  by blast
next
  show "⋂ {⟨G⟩ |G. G ∈ S} ⊆ ⟨⋂ {⟨G⟩ |G. G ∈ S}⟩"
    by simp
qed

theorem hull_minimal: "⟨G⟩ = ⋂ {S . G ⊆ S ∧ ⟨S⟩ = S}"
proof
  show " ⟨G⟩ ⊆ ⋂ {S. G ⊆ S ∧ ⟨S⟩ = S}"
    by (rule Inter_greatest, unfold mem_Collect_eq) (use hull_mono'[of G] in blast)
  show " ⋂ {S. G ⊆ S ∧ ⟨S⟩ = S} ⊆ ⟨G⟩"
    by (rule Inter_lower, unfold mem_Collect_eq gen_idemp) (use genset_sub in blast)
qed



lemma all_gen_comm_hull_comm: assumes "⋀ x y. x ∈ G ⟹ y ∈ G  ⟹ x ⋅ y = y ⋅ x"
      "u ∈ ⟨G⟩" "v ∈ ⟨G⟩"
    shows "u ⋅ v = v ⋅ u"
proof (rule hull.induct[OF ‹u ∈ ⟨G⟩›], blast)
  fix w1 w2
  assume "w1 ∈ G" "w2 ∈ ⟨G⟩" "w2 ⋅ v = v ⋅ w2"
  show "(w1 ⋅ w2) ⋅ v = v ⋅ w1 ⋅ w2"
    unfolding rassoc ‹w2 ⋅ v = v ⋅ w2› unfolding lassoc cancel_right
  proof (rule hull.induct[OF ‹v ∈ ⟨G⟩›], blast)
    fix w1' w2'
    assume "w1' ∈ G" "w2' ∈ ⟨G⟩" "w1 ⋅ w2' = w2' ⋅ w1"
    show "w1 ⋅ w1' ⋅ w2' = (w1' ⋅ w2') ⋅ w1"
      unfolding rassoc ‹w1 ⋅ w2' = w2' ⋅ w1›[symmetric] unfolding lassoc cancel_right
      using ‹w1' ∈ G› ‹w1 ∈ G› assms(1) by force
  qed
qed

lemma bin_comm_hull_comm: assumes "x ⋅ y = y ⋅ x" "u ∈ ⟨{x,y}⟩" "v ∈ ⟨{x,y}⟩"
  shows "u ⋅ v = v ⋅ u"
  by (rule all_gen_comm_hull_comm[OF _ assms(2-3)]) (use assms(1) in fastforce)

lemma[reversal_rule]: "rev ` ⟨{rev u, rev v}⟩ = ⟨{u,v}⟩"
  by (simp add: rev_hull)

lemma[reversal_rule]: "rev w ∈  ⟨rev ` G⟩ ≡ w ∈ ⟨G⟩"
  unfolding rev_in_conv rev_hull rev_rev_image_eq.


section "Factorization into generators"

text‹We define a decomposition (or a factorization) of a into elements of a given generating set. Such a decomposition is well defined only
if the decomposed word is an element of the hull. Even int that case, however, the decomposition need not be unique.›

definition decompose :: "'a list set  ⇒ 'a list ⇒ 'a list list" ("Dec _ _" [55,55] 56) where
  "decompose G u = (SOME us. us ∈ lists (G - {ε}) ∧ concat us = u)"

lemma dec_ex:  assumes "u ∈ ⟨G⟩" shows "∃ us. (us ∈ lists (G - {ε}) ∧ concat us = u)"
  using assms unfolding image_def  hull_concat_lists[of G] mem_Collect_eq
  using del_emp_concat lists_minus' by metis

lemma dec_in_lists': "u ∈ ⟨G⟩ ⟹ (Dec G u) ∈ lists (G - {ε})"
  unfolding decompose_def using someI_ex[OF dec_ex] by blast

lemma concat_dec[simp, intro] : "u ∈ ⟨G⟩ ⟹ concat (Dec G u) = u"
  unfolding decompose_def using someI_ex[OF dec_ex] by blast

lemma dec_emp [simp]: "Dec G ε = ε"
proof-
  have ex:  "ε ∈ lists (G - {ε}) ∧ concat ε = ε"
    by simp
  have all: "(us ∈ lists (G - {ε}) ∧ concat us = ε) ⟹ us = ε" for us
    using emp_concat_emp by auto
  show  ?thesis
    unfolding decompose_def
    using all[OF someI[of "λ x. x ∈ lists (G - {ε}) ∧ concat x = ε", OF ex]].
qed

lemma dec_nemp: "u ∈ ⟨G⟩ - {ε} ⟹  Dec G u ≠ ε"
  using concat_dec[of u G] by force

lemma dec_nemp'[simp, intro]: "u ≠ ε ⟹ u ∈ ⟨G⟩ ⟹ Dec G u ≠ ε"
  using dec_nemp by blast

lemma dec_eq_emp_iff [simp]: assumes "u ∈ ⟨G⟩" shows "Dec G u = ε ⟷ u = ε"
  using dec_nemp'[OF _ ‹u ∈ ⟨G⟩›] by auto

lemma dec_in_lists[simp]: "u ∈ ⟨G⟩ ⟹ Dec G u ∈ lists G"
  using dec_in_lists' by auto

lemma set_dec_sub: "x ∈ ⟨G⟩ ⟹ set (Dec G x) ⊆ G"
  using dec_in_lists by blast

lemma dec_hd: "u ≠ ε ⟹ u ∈ ⟨G⟩ ⟹ hd (Dec G u) ∈ G"
  by simp

lemma non_gen_dec: assumes  "u ∈ ⟨G⟩" "u ∉ G" shows "Dec G u  ≠ [u]"
  using dec_in_lists[OF ‹u ∈ ⟨G⟩›] Cons_in_lists_iff[of u ε G] ‹u ∉ G› by argo

lemma fac_fac_interpE_dec: assumes  "w ∈ ⟨G⟩"  "u ≤f w" "u ≠ ε"
  obtains p s ws where "ws ∈ lists (G - {ε})" "p u s ∼⇩_ℐ ws" "ws ≤f Dec G w"
proof-
  from fac_fac_interpE'[OF  _  ‹u ≠ ε›, of "Dec G w", unfolded concat_dec[OF ‹w ∈ ⟨G⟩›], OF ‹u ≤f w›]
  obtain p s ws where *: "p u s ∼⇩_ℐ ws" "ws ≤f Dec G w".
  have "ws ∈ lists (G - {ε})"
    using  fac_in_lists[OF dec_in_lists'[OF ‹w ∈ ⟨G⟩›] ‹ws ≤f Dec G w›].
  from that[OF this *]
  show thesis.
qed

lemma set_len_mod_concat: assumes "∀ x ∈ set us. ❙|x❙| mod n = 0" "0 < n"
  shows "❙|concat us❙| mod n = 0"
  using ‹∀ x ∈ set us. ❙|x❙| mod n = 0›
  by (induct us, force, unfold concat_simps lenmorph, force)

lemma hull_len_mod_concat: assumes "∀ x ∈ G. ❙|x❙| mod n = 0" "0 < n" "w ∈ ⟨G⟩"
  shows "❙|w❙| mod n = 0"
  by (rule set_len_mod_concat[of "Dec G w", OF _ ‹0 < n›, unfolded concat_dec[OF ‹w ∈ ⟨G⟩›]] concat_dec[OF ‹w ∈ ⟨G⟩›])
  (use ‹∀ x ∈ G. ❙|x❙| mod n = 0› ‹w ∈ ⟨G⟩› set_dec_sub in blast)

subsection ‹Refinement into a specific decomposition›

text‹We extend the decomposition to lists of words. This can be seen as a refinement of a previous decomposition of some word.›

definition refine :: "'a list set ⇒ 'a list list ⇒ 'a list list" ("Ref _ _" [55,56] 56) where
  "refine G us = concat(map (decompose G) us)"

lemma ref_morph: "us ∈ lists ⟨G⟩ ⟹ vs ∈ lists ⟨G⟩ ⟹ refine G (us ⋅ vs) = refine G us ⋅ refine G vs"
  unfolding refine_def by simp

lemma ref_morph_plus: "us ∈ lists (⟨G⟩ - {ε}) ⟹ vs ∈ lists (⟨G⟩ - {ε}) ⟹ refine G (us ⋅ vs) = refine G us ⋅ refine G vs"
  unfolding refine_def by simp

lemma ref_pref_mono: "ws ∈ lists ⟨G⟩ ⟹ us ≤p ws ⟹ Ref G us ≤p Ref G ws"
  unfolding prefix_def using ref_morph append_in_lists_dest' append_in_lists_dest by metis

lemma ref_suf_mono: "ws ∈ lists ⟨G⟩ ⟹ us ≤s ws ⟹ (Ref G us) ≤s Ref G ws"
  unfolding suffix_def using ref_morph append_in_lists_dest' append_in_lists_dest by metis

lemma ref_fac_mono: "ws ∈ lists ⟨G⟩ ⟹ us ≤f ws ⟹ (Ref G us) ≤f Ref G ws"
  unfolding sublist_altdef' using ref_pref_mono ref_suf_mono  suf_in_lists by metis

lemma ref_pop_hd: "us ≠ ε ⟹ us ∈ lists ⟨G⟩ ⟹ refine G us = decompose G (hd us) ⋅ refine G (tl us)"
  unfolding  refine_def  using list.simps(9)[of "decompose G" "hd us" "tl us"] by simp

lemma ref_in: "us ∈ lists ⟨G⟩ ⟹ (Ref G us) ∈ lists (G - {ε})"
proof (induction us)
  case (Cons a us)
  then show ?case
    using Cons.IH Cons.prems dec_in_lists' by (auto simp add: refine_def)
qed (simp add: refine_def)

lemma ref_in'[intro]: "us ∈ lists ⟨G⟩ ⟹ (Ref G us) ∈ lists G"
  using ref_in by auto

lemma concat_ref: "us ∈ lists ⟨G⟩ ⟹ concat (Ref G us) = concat us"
proof (induction us)
  case (Cons a us)
  then show ?case
    using Cons.IH Cons.prems concat_dec refine_def by (auto simp add: refine_def)
qed (simp add: refine_def)

lemma ref_gen: "us ∈ lists B ⟹ B ⊆ ⟨G⟩ ⟹ Ref G us ∈ ⟨decompose G ` B⟩"
  by (induct us, auto simp add: refine_def)

lemma ref_set: "ws ∈ lists ⟨G⟩ ⟹ set (Ref G ws) = ⋃ (set`(decompose G)`set ws)"
  by (simp add: refine_def)

lemma emp_ref: assumes "us ∈ lists (⟨G⟩ - {ε})" and  "Ref G us = ε" shows "us = ε"
  using emp_concat_emp[OF ‹us ∈ lists (⟨G⟩ - {ε})›]
    concat_ref [OF lists_minus[OF assms(1)], unfolded ‹Ref G us = ε› concat.simps(1),symmetric] by blast

lemma sing_ref_sing:
  assumes "us ∈ lists (⟨G⟩ - {ε})" and "refine G us = [b]"
  shows "us = [b]"
proof-
  have "us ≠ ε"
    using ‹refine G us = [b]› by (auto simp add: refine_def)
  have "tl us ∈ lists (⟨G⟩ - {ε})" and "hd us ∈ ⟨G⟩ - {ε}"
    using list.collapse[OF ‹us ≠ ε›]  ‹us ∈ lists (⟨G⟩ - {ε})› Cons_in_lists_iff[of "hd us" "tl us" "⟨G⟩ - {ε}"]
    by auto
  have "Dec G (hd us) ≠ ε"
    using dec_nemp[OF ‹hd us ∈ ⟨G⟩ - {ε}›].
  have "us ∈ lists ⟨G⟩"
    using ‹us ∈ lists (⟨G⟩ - {ε})› lists_minus by auto
  have "concat us = b"
    using ‹us ∈ lists ⟨G⟩› assms(2) concat_ref by force
  have "refine G (tl us) = ε"
    using ref_pop_hd[OF ‹us ≠ ε› ‹us ∈ lists ⟨G⟩›]  unfolding  ‹refine G us = [b]›
    using ‹Dec G (hd us) ≠ ε› Cons_eq_append_conv[of b ε "(Dec G (hd us))" "(Ref G (tl us))"]
      Cons_eq_append_conv[of b ε "(Dec G (hd us))" "(Ref G (tl us))"]  append_is_Nil_conv[of _ "(Ref G (tl us))"]
    by blast
  from  emp_ref[OF ‹tl us ∈ lists (⟨G⟩ - {ε})› this, symmetric]
  have "ε = tl us".
  from this[unfolded Nil_tl]
  show ?thesis
    using ‹us ≠ ε› ‹concat us = b› by auto
qed

lemma ref_ex: assumes "Q ⊆ ⟨G⟩" and "us ∈ lists Q"
  shows "Ref G us ∈ lists (G - {ε})" and "concat (Ref G us) = concat us"
  using ref_in[OF sub_lists_mono[OF assms]] concat_ref[OF sub_lists_mono[OF assms]].

lemma ref_emp [simp]: "Ref G ε = ε"
  unfolding refine_def by force

section "Basis"

text‹An important property of monoids of words is that they have a unique minimal generating set. Which is the set consisting of indecomposable elements.›

text‹Indecomposable element is an element that is not generated by other ones.›

definition ungenerated :: "'a list ⇒ 'a list set  ⇒ bool" (" _ ∈U _ " [51,51] 50) where
  "ungenerated b G ≡ b ∈ G ∧ b ∉ ⟨G - {b}⟩"

lemma ungen_nemp[simp]: "b ∈U G ⟹ b ≠ ε"
  unfolding ungenerated_def by blast

lemma ungen_in[intro]: "ungenerated b G ⟹ b ∈ G" and
      ungenD[intro]: "ungenerated b G ⟹ b ∉ ⟨G - {b}⟩"
  unfolding ungenerated_def by blast+

text ‹An ungenerated element has no nontrivial decomposition›

lemma ungen_dec_triv: assumes "u ∈ ⟨G⟩" "v ∈ ⟨G⟩" "u ⋅ v ∈U ⟨G⟩" shows " u = ε ∨ v = ε"
proof (rule ccontr)
  assume "¬ (u = ε ∨ v = ε)"
  hence "u ⋅ v ≠ u" "u ⋅ v ≠ v"
    by blast+
  hence "u ∈ ⟨⟨G⟩ - {u ⋅ v}⟩" "v ∈ ⟨⟨G⟩ - {u ⋅ v}⟩"
    using assms(1-2) by blast+
  from hull_closed[OF this]
  show False
    using ‹u ⋅ v ∈U ⟨G⟩› unfolding ungenerated_def by blast
qed

lemma ungen_dec_triv': assumes "us ∈ lists (⟨G⟩ - {ε})" "concat us ∈U ⟨G⟩" shows "❙|us❙| = 1"
proof-
  have "us ≠ ε"
    using ‹concat us ∈U ⟨G⟩› ungen_nemp by force
  hence "hd us ≠ ε" "hd us ∈ ⟨G⟩"
    using  ‹us ∈ lists (⟨G⟩ - {ε})› by force+
  have "concat (tl us) ∈ ⟨G⟩"
    using  concat_in_hull'[OF tl_in_lists, OF ‹us ∈ lists (⟨G⟩ - {ε})›, unfolded gen_idemp]
    by (simp add: gen_idemp)
  have "hd us ⋅  concat (tl us) ∈U ⟨G⟩"
    using ‹concat us ∈U ⟨G⟩›  by (subst (asm) (1) hd_tl[OF ‹us ≠ ε›, symmetric], simp)
  from ungen_dec_triv[of "hd us" _ "concat (tl us)", OF ‹hd us ∈ ⟨G⟩› ‹concat (tl us) ∈ ⟨G⟩›  this]
  have "tl us = ε"
    using tl_in_lists[OF ‹us ∈ lists (⟨G⟩ - {ε})›] ‹hd us ≠ ε› by force
  then show "❙|us❙| = 1"
    using nemp_le_len[OF ‹us ≠ ε›] long_list_tl by force
qed

text ‹Conversely, any nonempty  element that is not ungenerated is a product of at least two shorter elements›

lemma gen_elem_list: assumes "u ∈ ⟨G - {u}⟩" "u ≠ ε"
  obtains us where "us ∈ lists (G - {u} - {ε})" "concat us = u" "1 < ❙|us❙|"
    "⋀ c. c ∈ set us ⟹ ❙|c❙| < ❙|u❙|"
proof-
  from  hull_concat_lists_nempE[OF ‹u ∈ ⟨G - {u}⟩›]
  obtain ws where cond:  "ws ∈ lists (G - {u} - {ε})" "concat ws = u".
  have "1 < ❙|ws❙|"
  proof (rule ccontr)
    assume "¬ 1 < ❙|ws❙| "
    hence "❙|ws❙| = 1"
      using nemp_len[of ws] ‹u ≠ ε›[folded ‹concat ws = u›]
      by (metis concat_nemp less_one linorder_neqE_nat nemp_len_not0)
    hence "ws = [u]"
      using ‹concat ws = u› sing_word_concat by fastforce
    thus False
      using ‹ws ∈ lists (G - {u} - {ε})› by force
  qed
  have "❙|c❙| < ❙|u❙|" if "c ∈ set ws" for c
  proof-
    obtain ws1 ws2 where "ws = ws1 ⋅ [c] ⋅ ws2"
      using ‹c ∈ set ws› split_listE by meson
    hence ws_lists: "ws1 ∈ lists (G - {u} - {ε})" "ws2 ∈ lists (G - {u} - {ε})"
      using ‹ws ∈ lists (G - {u} - {ε})› by simp_all
    have "ws1 ⋅  ws2 ≠ ε"
      using ‹1 < ❙|ws❙|›[unfolded ‹ws = ws1 ⋅ [c] ⋅ ws2›] by force
    hence "❙|concat ws1❙| + ❙|concat ws2❙| ≠ 0"
      using ws_lists by force
    thus "❙|c❙| < ❙|u❙|"
      using lenarg[OF arg_cong[OF ‹ws = ws1 ⋅ [c] ⋅ ws2›, of concat]]
      unfolding concat_morph lenmorph concat_sing' ‹concat ws = u› by linarith
  qed
  from that[OF cond ‹1 < ❙|ws❙|› this]
  show thesis.
qed

lemma gen_elem_dec: assumes "b ∈ ⟨G - {b}⟩" "b ≠ ε"
  obtains u v where "u ∈ ⟨G⟩" "u ≠ ε" "v ∈ ⟨G⟩" "v ≠ ε" "u ⋅ v = b"
proof-
  from gen_elem_list[OF assms]
  obtain us where "us ∈ lists (G - {b} - {ε})" "concat us = b" "1 < ❙|us❙|".
  have "us ≠ ε" "tl us ≠ ε" "[hd us] ≠ ε"
    using long_list_tl[OF ‹1 < ❙|us❙|›] by fastforce+
  note b =  arg_cong[OF hd_tl[OF ‹us ≠ ε›], of concat, unfolded ‹concat us = b› concat_morph]
  have "concat (tl us) ≠ ε"
    using ‹tl us ≠ ε› ‹us ∈ lists (G - {b} - {ε})› emp_concat_emp tl_in_lists by meson
  have "concat (tl us) ∈ ⟨G⟩"
    using ‹us ∈ lists (G - {b} - {ε})› concat_in_hull' lists_minus tl_in_lists by meson
  have "concat [hd us] ≠ ε"
    using ‹us ∈ lists (G - {b} - {ε})› ‹us ≠ ε› by fastforce
  have "concat [hd us] ∈ ⟨G⟩"
    using ‹us ∈ lists (G - {b} - {ε})› Diff_iff ‹us ≠ ε› concat_sing' gen_in lists_hd_in_set by metis
  show thesis
    by (rule that[OF _ _ _ _ b]) fact+
qed

text ‹This yields several criteria for being ungenerated›

lemma ungeneratedI:
  assumes "b ∈ G" and "b ≠ ε"
  and all: "⋀ u v. u ≠ ε ⟹  u ∈ ⟨G⟩ ⟹  v ≠ ε ⟹ v ∈ ⟨G⟩ ⟹ u ⋅ v ≠ b"
  shows "b ∈U G"
  unfolding ungenerated_def
proof
  show "b ∉ ⟨G - {b}⟩"
  proof
    assume "b ∈ ⟨G - {b}⟩"
    from gen_elem_dec[OF this ‹b ≠ ε›]
    show False
      using all by metis
  qed
qed fact

lemma ungeneratedI':
  assumes "b ∈ G" and "b ≠ ε"
  and all: "⋀ us. us ∈ lists (G - {b} - {ε})  ⟹ concat us = b  ⟹ ❙|us❙| ≤ 1"
  shows "b ∈U G"
  unfolding ungenerated_def
proof
  show "b ∉ ⟨G - {b}⟩"
  proof
    assume "b ∈ ⟨G - {b}⟩"
    from gen_elem_list[OF this ‹b ≠ ε›]
    show False
      using all le_antisym nless_le by metis
  qed
qed fact

lemma ungenerated_shortest:
  assumes "b ∈ G" and "b ≠ ε"
  and all: "⋀ c. c ∈ G - {ε}  ⟹ ❙|b❙| ≤ ❙|c❙|"
  shows "b ∈U G"
  unfolding ungenerated_def
proof
  show "b ∉ ⟨G - {b}⟩"
  proof
    assume "b ∈ ⟨G - {b}⟩"
    from gen_elem_list[OF this ‹b ≠ ε›]
    obtain us where "us ∈ lists (G - {b} - {ε})" "concat us = b" and all': "(⋀c. c ∈ set us ⟹ ❙|c❙| < ❙|b❙|)"
      by metis
    have "c ∈ set us ⟹ ❙|b❙| ≤ ❙|c❙|" for c
      using all ‹us ∈ lists (G - {b} - {ε})› by blast
    then show False
      using all' ‹b ≠ ε› ‹concat us = b› unfolding linorder_not_less[symmetric]
      by fastforce
  qed
qed fact

lemma ungenerated_sing:
  assumes "[a] ∈ G"
  shows "[a] ∈U G"
  using ungenerated_shortest[OF assms] nemp_le_len unfolding sing_len
   by blast

― ‹Ungeneretad element is ungenerated by the whole monoid›

lemma ungen_hull_ungen:  "b ∈U ⟨G⟩ ⟷ b ∈U G"
proof
  assume "b ∈U G"
  show " b ∈U ⟨G⟩"
    unfolding ungenerated_def
  proof
    show "b ∉ ⟨⟨G⟩ - {b}⟩"
    proof
      assume "b ∈ ⟨⟨G⟩ - {b}⟩"
    from gen_elem_list[OF this ungen_nemp[OF ‹b ∈U G›]]
    obtain us where "us ∈ lists (⟨G⟩ - {b} - {ε})" and "concat us = b"
      and "1 < ❙|us❙|" and short: "⋀c. c ∈ set us ⟹ ❙|c❙| < ❙|b❙|"
      by blast
    have no_b: "b ∉ set (Dec G u)" if  "u ∈ set us" for u
    proof
      assume "b ∈ set (Dec G u)"
      have "concat (Dec G u) = u"
        using ‹us ∈ lists (⟨G⟩ - {b} - {ε})› ‹u ∈ set us› by blast
      hence "❙|b❙| ≤ ❙|u❙|"
        using split_list_first[OF ‹b ∈ set (Dec G u)›] by force
      thus False
        using short[OF ‹u ∈ set us›] by force
    qed
    define vs where "vs = refine G us"
    have  "concat vs = b" "vs ∈ lists (G - {ε})"
      using ref_ex[OF _ ‹us ∈ lists (⟨G⟩ - {b} - {ε})›, of G]
      unfolding vs_def ‹concat us = b› by blast+
    have "b ∉ set vs"
      using no_b unfolding vs_def refine_def by simp
    hence "vs ∈ lists (G - {b})"
      using ‹vs ∈ lists (G - {ε})› by blast
    with ungenD[OF ‹b ∈U G›]
    show False
      unfolding ungenerated_def using ‹concat vs = b› by blast
  qed
  show "b ∈ ⟨G⟩"
    using ungen_in[OF ‹b ∈U G›] by blast
qed
next
  assume "b ∈U ⟨G⟩ "
  show "b ∈U G"
    unfolding ungenerated_def
  proof
    have "G - {b} ⊆ ⟨G⟩ - {b}"
      by blast
    from hull_mono[OF this]
    show "b ∉ ⟨G - {b}⟩"
      using ungenD[OF ‹b ∈U ⟨G⟩›] by blast
    then show "b ∈ G"
      using ungen_in[OF ‹b ∈U ⟨G⟩›] by auto
  qed
qed

text‹The \emph{basis} is the set of all ungenerated elements.›

definition basis :: "'a list set  ⇒ 'a list set" ("𝔅 _" [51] ) where
  "basis G = {x. x ∈U G}"

lemma basisD: "x ∈ 𝔅 G ⟹ x ∈U G"
  unfolding basis_def by simp

lemma basis_in: "x ∈ 𝔅 G ⟹ x ∈ G"
  unfolding basis_def ungenerated_def by simp

lemma emp_not_basis: "x ∈ 𝔅 G ⟹ x ≠ ε"
  unfolding basis_def ungenerated_def by blast

lemma basis_sub_gen: "𝔅 G ⊆ G"
  unfolding  basis_def ungenerated_def by simp

text‹The basis generates the generating set and therefore also the whole monoid›

lemma gen_sub_basis: "G ⊆ ⟨𝔅 G⟩"
proof
  fix w show "w ∈ G ⟹ w ∈ ⟨𝔅 G⟩"
  proof (induct "length w" arbitrary: w rule: less_induct)
    case less
    show ?case
    proof (cases "w ∈ 𝔅 G ∨ w = ε", blast)
      assume "¬ (w ∈ 𝔅 G ∨ w = ε)"
      hence "w ∈ ⟨G - {w}⟩" "w ≠ ε"
        using ‹w ∈ G› unfolding basis_def ungenerated_def  by blast+
      from gen_elem_list[OF this[unfolded ungenerated_def]]
      obtain us where "us ∈ lists (G - {w} - {ε})" "concat us = w" "1 < ❙|us❙|" and
        small: "(⋀c. c ∈ set us ⟹ ❙|c❙| < ❙|w❙|)"
        by blast
      have "c ∈ ⟨𝔅 G⟩" if "c ∈ set us" for c
        using  less.hyps[of c, OF small, OF that] ‹c ∈ set us› ‹us ∈ lists (G - {w} - {ε})› by blast
      thus "w ∈ ⟨𝔅 G⟩ "
        unfolding ‹concat us = w›[symmetric]
        using hull_closed_lists[OF in_listsI] by blast
    qed
  qed
qed

lemma basis_concat_listsE:
  assumes "w ∈ G"
  obtains ws where "ws ∈ lists 𝔅 G"  and "concat ws = w"
  using assms by (rule hull_concat_listsE[OF subsetD, OF  gen_sub_basis])

theorem basis_gen_hull: "⟨𝔅 G⟩ = ⟨G⟩"
  by (rule equalityI; simp only: hull_mono[OF basis_sub_gen] hull_mono[OF gen_sub_basis, unfolded gen_idemp])

theorem basis_of_hull: "𝔅 ⟨G⟩ = 𝔅 G"
unfolding basis_def ungen_hull_ungen..

lemma basis_gen_hull': "⟨𝔅 ⟨G⟩⟩ = ⟨G⟩"
  unfolding basis_of_hull using basis_gen_hull.

lemma basis_hull_sub: "𝔅 ⟨G⟩ ⊆ G"
  unfolding basis_of_hull using basis_sub_gen.

text‹The basis is the smallest generating set.›
theorem gen_basis_sub:  "⟨S⟩ = ⟨G⟩ ⟹ 𝔅 G ⊆ S"
  using basis_hull_sub[of S] basis_of_hull[of G] by simp

lemma basis_min_gen: "S ⊆ 𝔅 G ⟹ ⟨S⟩ = G ⟹ S = 𝔅 G"
  using basis_of_hull basis_sub_gen by blast

lemma basisI: "(⋀ B. ⟨B⟩ = ⟨C⟩ ⟹ C ⊆ B) ⟹ 𝔅 ⟨C⟩ = C"
  using basis_gen_hull basis_min_gen basis_of_hull by metis

text‹An arbitrary set between basis and the hull is generating...›
lemma gen_sets: assumes "𝔅 G ⊆ S" and "S ⊆ ⟨G⟩" shows "⟨S⟩ = ⟨G⟩"
  using hull_mono[OF ‹S ⊆ ⟨G⟩›, unfolded gen_idemp] hull_mono[OF ‹𝔅 G ⊆ S›, unfolded basis_gen_hull] by blast

text‹... and has the same basis›
lemma basis_sets: "𝔅 G ⊆ S ⟹ S ⊆ ⟨G⟩ ⟹ 𝔅 G = 𝔅 S"
  by (metis basis_of_hull  gen_sets)

section "Code"

locale nemp_words =
  fixes G
  assumes emp_not_in: "ε ∉ G"

begin
lemma drop_empD: "G - {ε} = G"
  using emp_not_in by simp

lemmas emp_concat_emp' = emp_concat_emp[of _ G, unfolded drop_empD]

thm disjE[OF ruler[OF take_is_prefix take_is_prefix]]


lemma nemp: "x ∈ G ⟹ x ≠ ε"
  using emp_not_in by blast

lemma concat_eq_emp_conv [simp]: "us ∈ lists G ⟹ concat us = ε ⟷ us = ε"
  unfolding in_lists_conv_set concat_eq_Nil_conv
  by (simp add: nemp)

lemma root_dec_inj_on: "inj_on (λ x. [ρ x]⇧^@(e⇩_ρ x)) G"
  unfolding inj_on_def using primroot_exp_eq
  unfolding concat_pow_list_single[of _ "ρ _", symmetric] by metis

lemma concat_len_ruler: assumes "ws ∈ lists G" "us ≤p ws" "vs ≤p ws" "❙|concat us❙| ≤ ❙|concat vs❙|"
  shows "us ≤p vs"
proof (rule ccontr)
  assume "¬ us ≤p vs"
  with ruler[OF assms(2-3)]
  have "vs <p us"
    by blast
  from arg_cong[OF lq_spref[OF this], of "λ x. ❙|concat x❙|", unfolded concat_morph lenmorph]
  have "❙|concat (vs¯⇧^>us)❙| = 0"
    using assms(4) by linarith
  hence "vs¯⇧^>us = ε"
    using emp_concat_emp'[OF lq_in_lists[OF pref_in_lists[OF ‹us ≤p ws› ‹ws ∈ lists G›]]] by blast
  thus False
    using lq_spref_nemp[OF ‹vs <p us›] by contradiction
qed


end

lemma concat_emp:
   "ε ∉ G ⟹ us ∈ lists G ⟹ concat us = ε ⟹ us = ε"
 using nemp_words.concat_eq_emp_conv[OF nemp_words.intro] by blast

text‹A basis freely generating its hull is called a \emph{code}. By definition,
this means that generated elements have unique factorizations into the elements of the code.›

locale code =
  fixes 𝒞
  assumes is_code: "xs ∈ lists 𝒞 ⟹ ys ∈ lists 𝒞 ⟹ concat xs = concat ys ⟹ xs = ys"
begin

lemma code_comm_eq: "x ∈ 𝒞 ⟹ y ∈ 𝒞 ⟹ x ⋅ y = y ⋅ x ⟹ x = y"
  using is_code[of "[x,y]" "[y,x]", THEN arg_cong[of _ _ hd]] by simp

lemma emp_not_in: "ε ∉ 𝒞"
proof
  assume "ε ∈ 𝒞"
  hence "[] ∈ lists 𝒞" and "[ε] ∈ lists 𝒞" and "concat [] = concat [ε]" and "[] ≠ [ε]"
    by simp+
  thus False
    using is_code by blast
qed

lemma nemp: "u ∈ 𝒞 ⟹ u ≠ ε"
  using emp_not_in by force

sublocale nemp_words 𝒞
  using emp_not_in by unfold_locales

lemma code_elem_dec: "us ∈ lists 𝒞 ⟹ concat us = c ⟹ c ∈ 𝒞 ⟹ us = [c]"
  using is_code[of us "[c]"] by simp

lemma code_ungen: assumes "c ∈ 𝒞" shows "c ∈U 𝒞"
  unfolding ungenerated_def
proof
  show "c ∉ ⟨𝒞 - {c}⟩"
  proof
    assume ‹c ∈ ⟨𝒞 - {c}⟩›
    from gen_elem_list[OF this nemp[OF ‹c ∈ 𝒞›]]
    obtain us where "us ∈ lists (𝒞 - {c} - {ε})" "concat us = c" "1 < ❙|us❙|".
    show False
      using code_elem_dec[OF _ ‹concat us = c› ‹c ∈ 𝒞›]
        ‹1 < ❙|us❙|› sing_len[of c] ‹us ∈ lists (𝒞 - {c} - {ε})› by fastforce
  qed
qed fact

lemma code_is_basis: "𝔅 𝒞 = 𝒞"
  using code_ungen basis_def[of 𝒞] basis_sub_gen by blast

lemma code_unique_dec': "us ∈ lists 𝒞 ⟹ Dec 𝒞 (concat us) = us"
  using dec_in_lists[of "concat us" 𝒞, THEN is_code, of us]
    concat_dec[of "concat us" 𝒞] hull_concat_lists[of 𝒞] image_eqI[of "concat us" concat us "lists 𝒞"]
  by argo

lemma code_unique_dec [intro!]: "us ∈ lists 𝒞 ⟹ concat us = u ⟹  Dec 𝒞 u = us"
  using code_unique_dec' by blast

lemma triv_refine[intro!] : "us ∈ lists 𝒞 ⟹ concat us = u ⟹  Ref 𝒞 [u] = us"
  using code_unique_dec' by (auto simp add: refine_def)

lemma code_unique_ref: "us ∈ lists ⟨𝒞⟩ ⟹ refine 𝒞 us = decompose 𝒞 (concat us)"
proof-
  assume "us ∈ lists ⟨𝒞⟩"
  hence "concat (refine 𝒞 us) = concat us"
    using concat_ref by blast
  hence eq: "concat (refine 𝒞 us) = concat (decompose 𝒞 (concat us))"
    using  concat_dec[OF hull_closed_lists[OF ‹us ∈ lists ⟨𝒞⟩›]] by auto
  have dec: "Dec 𝒞 (concat us) ∈ lists 𝒞"
    using ‹us ∈ lists ⟨𝒞⟩› dec_in_lists hull_closed_lists
    by metis
  have "Ref 𝒞 us ∈ lists 𝒞"
    using lists_minus[OF ref_in[OF ‹us ∈ lists ⟨𝒞⟩›]].
  from  is_code[OF this dec eq]
  show ?thesis.
qed

lemma refI [intro]: "us ∈ lists ⟨𝒞⟩ ⟹ vs ∈ lists 𝒞 ⟹ concat vs = concat us ⟹ Ref 𝒞 us = vs"
  unfolding code_unique_ref code_unique_dec..

lemma code_dec_morph: assumes "x ∈ ⟨𝒞⟩" "y ∈ ⟨𝒞⟩"
  shows "(Dec 𝒞 x) ⋅ (Dec 𝒞 y) = Dec 𝒞 (x⋅y)"
proof-
  have eq: "(Dec 𝒞 x) ⋅ (Dec 𝒞 y) = Dec 𝒞 (concat ((Dec 𝒞 x) ⋅ (Dec 𝒞 y)))"
    using dec_in_lists[OF ‹x ∈ ⟨𝒞⟩›] dec_in_lists[OF ‹y ∈ ⟨𝒞⟩›]
      code.code_unique_dec[OF code_axioms, of "(Dec 𝒞 x) ⋅ (Dec 𝒞 y)", unfolded append_in_lists_conv, symmetric]
    by presburger
  moreover have "concat ((Dec 𝒞 x) ⋅ (Dec 𝒞 y)) = (x ⋅ y)"
    using concat_morph[of "Dec 𝒞 x" "Dec 𝒞 y"]
    unfolding concat_dec[OF ‹x ∈ ⟨𝒞⟩›] concat_dec[OF ‹y ∈ ⟨𝒞⟩›].
  ultimately show "(Dec 𝒞 x) ⋅ (Dec 𝒞 y) = Dec 𝒞 (x⋅y)"
    by argo
qed

lemma dec_pow: "rs ∈ ⟨𝒞⟩ ⟹ Dec 𝒞 (rs⇧^@k) = (Dec 𝒞 rs)⇧^@k"
proof(induction k arbitrary: rs, fastforce)
  case (Suc k)
  then show ?case
    using code_dec_morph pow_Suc power_in by metis
qed

lemma code_el_dec: "c ∈ 𝒞 ⟹ decompose 𝒞 c = [c]"
  by fastforce

lemma code_ref_list: "us ∈ lists 𝒞 ⟹ refine 𝒞 us = us"
proof (induct us)
  case (Cons a us)
  then show ?case using code_el_dec
    unfolding refine_def by simp
qed (simp add: refine_def)

lemma code_ref_gen: assumes "G ⊆ ⟨𝒞⟩" "u ∈ ⟨G⟩"
  shows "Dec 𝒞 u ∈ ⟨decompose 𝒞 ` G⟩"
proof-
  have "refine 𝒞 (Dec G u) = Dec 𝒞 u"
    using  dec_in_lists[OF ‹u ∈ ⟨G⟩›]  ‹G ⊆ ⟨𝒞⟩› code_unique_ref[of "Dec G u", unfolded concat_dec[OF ‹u ∈ ⟨G⟩›]] by blast
  from ref_gen[of "Dec G u" G, OF dec_in_lists[OF ‹u ∈ ⟨G⟩›], of 𝒞, unfolded this, OF ‹G ⊆ ⟨𝒞⟩›]
  show ?thesis.
qed

find_theorems "ρ ?x ⇧^@ ?k = ?x" "0 < ?k"

lemma code_rev_code: "code (rev ` 𝒞)"
proof
  fix xs ys assume "xs ∈ lists (rev ` 𝒞)" "ys ∈ lists (rev ` 𝒞)" "concat xs = concat ys"
  have "map rev (rev xs) ∈ lists 𝒞" and "map rev (rev ys) ∈ lists 𝒞"
    using rev_in_lists[OF ‹xs ∈ lists (rev ` 𝒞)›] rev_in_lists[OF ‹ys ∈ lists (rev ` 𝒞)›] map_rev_lists_rev
    by (metis imageI)+
  moreover have "concat (map rev (rev xs)) = concat (map rev (rev ys))"
    unfolding rev_concat[symmetric] using ‹concat xs = concat ys› by blast
  ultimately have "map rev (rev xs) = map rev (rev ys)"
    using is_code by blast
  thus "xs = ys"
     using ‹concat xs = concat ys› by simp
qed

lemma dec_rev [simp, reversal_rule]:
  "u ∈ ⟨𝒞⟩ ⟹ Dec rev ` 𝒞 (rev u) = rev (map rev (Dec 𝒞 u))"
  by (auto simp only: rev_map lists_image rev_in_lists rev_concat[symmetric] dec_in_lists
      intro!: code_rev_code code.code_unique_dec imageI del: in_listsI)

lemma elem_comm_sing_set: assumes "ws ∈ lists 𝒞" and "ws ≠ ε" and "u ∈ 𝒞" and "concat ws ⋅ u = u ⋅ concat ws"
  shows  "set ws = {u}"
  using assms
proof-
  have "concat (ws ⋅ [u]) = concat ([u] ⋅ ws)"
    using assms by simp
  have "ws ⋅ [u] = [u] ⋅ ws"
    using  ‹u ∈ 𝒞› ‹ws ∈ lists 𝒞› is_code[OF _ _  ‹concat (ws ⋅ [u]) = concat ([u] ⋅ ws)›]
    by simp
  from comm_nemp_pows_posE[OF this ‹ws ≠ ε› not_Cons_self2[of u ε]]
  obtain t k m where "ws = t⇧^@k" "[u] = t⇧^@m" "0 < k" "0 < m" "primitive t".
  hence "t = [u]"
    by force
  show "set ws = {u}"
    using  ‹ws = t⇧^@k›[unfolded ‹t = [u]›]  set_sing_nemp_eq[OF  sing_pow_set_sub  ‹ws ≠ ε›] by blast
qed

lemma  pure_code_pres_prim:  assumes pure: "∀u ∈ ⟨𝒞⟩. ρ u ∈ ⟨𝒞⟩" and
  "w ∈ ⟨𝒞⟩" and "primitive (Dec 𝒞 w)"
shows "primitive w"
proof-
  obtain k where "(ρ w)⇧^@k = w"
    using primroot_expE by blast

  have "ρ w ∈ ⟨𝒞⟩"
    using assms(2) pure by auto

  have "(Dec 𝒞 (ρ w))⇧^@k ∈ lists 𝒞"
    by (metis ‹ρ w ∈ ⟨𝒞⟩› concat_pow_list_single dec_in_lists flatten_lists order_refl sing_pow_lists)

  have "(Dec 𝒞 (ρ w))⇧^@k = Dec 𝒞 w"
    using ‹(Dec 𝒞 (ρ w)) ⇧^@ k ∈ lists 𝒞›  code.code_unique_dec code_axioms concat_morph_power ‹(ρ w) ⇧^@ k = w› concat_dec[OF ‹ρ w ∈ ⟨𝒞⟩›] by metis
  hence "k = 1"
    using ‹primitive (Dec 𝒞 w)› unfolding primitive_def by blast
  thus "primitive w"
    by (metis pow_list_1 ‹ρ w ⇧^@ k = w› assms(3) dec_emp prim_nemp primroot_prim)
qed

lemma inj_on_dec: "inj_on (decompose 𝒞) ⟨𝒞⟩"
  by (rule inj_on_inverseI[of _ concat]) simp

lemma ref_disj_interp: assumes "vs ∈ lists ⟨𝒞⟩" "p Ref 𝒞 vs s ∼⇩_𝒟 ws"
  shows "p vs s ∼⇩_𝒟 ws"
proof(rule disj_interpI)
  show "p (concat vs) s ∼⇩_ℐ ws"
    using disj_interpD0[OF ‹p Ref 𝒞 vs s ∼⇩_𝒟 ws›]
    unfolding concat_ref[OF ‹vs ∈ lists ⟨𝒞⟩›].
  show "∀u v. u ≤p vs ∧ v ≤p ws ⟶ p ⋅ concat u ≠ concat v"
  proof (rule allI, rule allI, rule impI, elim conjE)
    fix u v assume "u ≤p vs" "v ≤p ws"
    have "Ref 𝒞 u ≤p Ref 𝒞 vs"
      using ref_pref_mono[OF ‹vs ∈ lists ⟨𝒞⟩› ‹u ≤p vs›].
    have "concat (Ref 𝒞 u) = concat u"
      using  concat_ref[OF pref_in_lists[OF ‹u ≤p vs› ‹vs ∈ lists ⟨𝒞⟩›]].
    then show "p ⋅ concat u ≠ concat v"
      using disj_interpD1[OF ‹p Ref 𝒞 vs s ∼⇩_𝒟 ws› ‹Ref 𝒞 u ≤p Ref 𝒞 vs› ‹v ≤p ws›]
      by simp
  qed
qed

end ― ‹end context code›

lemma emp_is_code: "code {}"
  using code.intro empty_iff insert_iff lists_empty by metis

lemma code_rev_code_iff [reversal_rule]: "code (rev ` C) ⟷ code C"
  by (rule iffI[OF code.code_rev_code[of "rev ` C", unfolded rev_rev_image_eq] code.code_rev_code])

lemma code_induct_hd: assumes "ε ∉ C" and
  "⋀ xs ys. xs ∈ lists C ⟹ ys ∈ lists C ⟹ concat xs = concat ys ⟹ hd xs = hd ys"
shows "code C"
proof
  show "xs ∈ lists C ⟹ ys ∈ lists C ⟹ concat xs = concat ys ⟹ xs = ys" for xs ys
  proof (induct xs ys rule: list_induct2')
    case (4 x xs y ys)
    from assms(2)[OF "4.prems"]
    have "x = y" by force
    from "4.prems"[unfolded this]
    have "xs ∈ lists C" and "ys ∈ lists C" and "concat xs = concat ys"
      by simp_all
    from "4.hyps"[OF this] ‹x = y›
    show ?case
      by simp
  qed (auto simp add: ‹ε ∉ C›)
qed

lemma ref_set_primroot: assumes "ws ∈ lists (G - {ε})" and "code (ρ`G)"
  shows "set (Ref ρ`G ws) = ρ`(set ws)"
proof-
  have "G ⊆ ⟨ρ`G⟩"
  proof
    fix x
    assume "x ∈ G"
    show "x ∈ ⟨ρ ` G⟩"
      by (metis ‹x ∈ G› genset_sub image_subset_iff power_in primroot_expE)
  qed
  hence "ws ∈ lists ⟨ρ`G⟩"
    using assms by blast

  have "set (decompose (ρ`G) a) = {ρ a}" if "a ∈ set ws" for a
  proof-
    have "ρ a ∈ ρ`G" "a ≠ ε"
      using ‹a ∈ set ws› ‹ws ∈ lists (G - {ε})› by force+
    obtain k where "(Dec (ρ`G) a) = [ρ a]⇧^@k" "0 < k"
      using code.code_unique_dec[OF ‹code (ρ ` G)› sing_pow_lists concat_pow_list_single, OF ‹ρ a ∈ ρ ` G›]
        primroot_expE by metis
    hence "Dec (ρ`G) a ≠ ε"
      by simp
    from set_sing_nemp_eq[OF _ this]
    show "set (decompose (ρ`G) a) = {ρ a}"
      unfolding ‹Dec ρ ` G a = [ρ a] ⇧^@ k› using sing_pow_set' by metis
  qed

  have "(set`(decompose (ρ`G))`set ws) = {{ρ a} |a. a ∈ set ws}" (is "?L = ?R")
  proof
    show "?L ⊆ ?R"
      using ‹⋀a. a ∈ set ws ⟹ set (Dec ρ ` G a) = {ρ a}› by blast
    show "?R ⊆ ?L"
      using ‹⋀a. a ∈ set ws ⟹ set (Dec ρ ` G a) = {ρ a}› by blast
  qed

  show ?thesis
    using ref_set[OF ‹ws ∈ lists ⟨ρ`G⟩›]
      Setcompr_eq_image ‹set ` decompose (ρ ` G) ` set ws = {{ρ a} |a. a ∈ set ws}› by (auto simp add: refine_def)
qed

section ‹Prefix code›

locale prefix_code =
  fixes 𝒞
  assumes
    emp_not_in: "ε ∉ 𝒞" and
    pref_free: "u ∈ 𝒞 ⟹ v ∈ 𝒞 ⟹ u ≤p v ⟹ u = v"

begin

lemma nemp: "u ∈ 𝒞 ⟹ u ≠ ε"
  using emp_not_in by force

lemma concat_pref_concat:
  assumes "us ∈ lists 𝒞" "vs ∈ lists 𝒞" "concat us ≤p concat vs"
  shows "us ≤p vs"
using assms proof (induction us vs rule: list_induct2')
  case (4 x xs y ys)
  from "4.prems"
  have "x = y"
    by (auto elim!: ruler_prefE intro: pref_free sym del: in_listsD)
  with "4" show "x # xs ≤p y # ys"
  by simp
qed (simp_all add: nemp)

lemma concat_pref_concat_conv:
  assumes "us ∈ lists 𝒞" "vs ∈ lists 𝒞"
  shows "concat us ≤p concat vs ⟷ us ≤p vs"
using concat_pref_concat[OF assms] pref_concat_pref..

sublocale code
  by standard (simp_all add: pref_antisym concat_pref_concat)

lemmas is_code = is_code and
  code = code_axioms

lemma dec_pref_unique:
  "w ∈ ⟨𝒞⟩ ⟹ p ∈ ⟨𝒞⟩ ⟹ p ≤p w ⟹ Dec 𝒞 p ≤p Dec 𝒞 w"
  using concat_pref_concat_conv[of "Dec 𝒞 p" "Dec 𝒞 w", THEN iffD1]
  by simp

lemma concat_suf_eq: assumes
  "us ∈ lists 𝒞" "ws ∈ lists 𝒞" and
  "concat us ⋅ s = concat ws" and "s <s last ws"
shows "us = ws" and "s = ε"
proof-
  from concat_pref_concat_conv[OF assms(1,2), folded ‹concat us ⋅ s = concat ws›]
  have "us ≤p ws"
    by blast
  hence "concat (us¯⇧^>ws) = s"
    using assms(3) concat_morph_lq lq_triv by metis
  from concat_butlast_last[of "us¯⇧^>ws", unfolded this]
  show "us = ws"
    using empty_lq_eq[OF ‹us ≤p ws›] assms(4)  last_appendR lq_pref[OF ‹us ≤p ws›]
    ssuf_extD suffix_order.strict_iff_not by metis
  show "s = ε"
    using ‹concat us ⋅ s = concat ws›[unfolded ‹us = ws›] by blast
qed

end

thm prefix_code.concat_suf_eq[reversed]

subsection ‹Suffix code›

locale suffix_code = prefix_code "(rev ` 𝒞)" for 𝒞
begin

thm dec_rev
    code

sublocale code
  using code_rev_code unfolding rev_rev_image_eq.

lemmas concat_suf_concat = concat_pref_concat[reversed] and
       concat_suf_concat_conv = concat_pref_concat_conv[reversed] and
       nemp = nemp[reversed] and
       suf_free = pref_free[reversed] and
       dec_suf_unique = dec_pref_unique[reversed]

lemma concat_pref_eq: assumes
  "us ∈ lists 𝒞" "ws ∈ lists 𝒞" and
  "p ⋅ concat us = concat ws" and "p <p hd ws"
shows "us = ws" and "p = ε"
proof (atomize(full))
  show "us = ws ∧ p = ε"
  proof (cases "ws = ε")
    assume "ws = ε"
    hence "p ⋅ concat us = ε"
      unfolding ‹p ⋅ concat us = concat ws› by simp
    thus "us = ws ∧ p = ε"
      unfolding ‹ws = ε› using ‹us ∈ lists 𝒞›
      using concat_emp[OF emp_not_in ‹us ∈ lists 𝒞›] by blast
  next
    assume "ws ≠ ε"
    from  concat_suf_eq[reversed, OF assms(1-3)]
    show "us = ws ∧ p = ε"
      unfolding hd_map[OF ‹ws ≠ ε›] spref_rev_suf_iff[symmetric]
      using ‹p <p hd ws› by blast
  qed
qed

thm is_code
    code_axioms
    code

end

subsection ‹Bifix code›

locale bifix_code = prefix_code + suf: suffix_code
begin

lemma joint_interp_triv: assumes
  "us ∈ lists 𝒞" "ws ∈ lists 𝒞" and
  interp: "p (concat us) s ∼⇩_ℐ ws" and
  joint: "¬ p us s ∼⇩_𝒟 ws"
shows "p = ε" and "s = ε" and "us = ws"
proof-
  from non_disjoint_interpE[OF interp joint]
  obtain ws1 ws2 us1 us2 where "us1 ⋅ us2 = us" "ws1 ⋅ ws2 = ws"
    "p ⋅ concat us1 = concat ws1" "concat us2 ⋅ s = concat ws2".
  hence "ws1 ∈ lists 𝒞" "ws2 ∈ lists 𝒞" "us1 ∈ lists 𝒞" "us2 ∈ lists 𝒞"
    using ‹us ∈ lists 𝒞› ‹ws ∈ lists 𝒞› by inlists
  have eq1: "us2 = ws2 ∧ s = ε"
  proof (cases "ws2 = ε")
    assume "ws2 = ε"
    show ?thesis
      thm emp_concat_emp'
      using ‹concat us2 ⋅ s = concat ws2› emp_concat_emp'[OF ‹us2 ∈ lists 𝒞›] unfolding ‹ws2 = ε›
      concat.simps by blast
  next
    assume "ws2 ≠ ε"
    with concat_suf_eq[OF ‹us2 ∈ lists 𝒞› ‹ws2 ∈ lists 𝒞› ‹concat us2 ⋅ s = concat ws2›]
    show ?thesis
      using fac_interpD(2)[OF interp, folded ‹ws1 ⋅ ws2 = ws›] by force
  qed
  have eq2: "us1 = ws1 ∧ p = ε"
  proof (cases "ws1 = ε")
    assume "ws1 = ε"
    show ?thesis
      using ‹p ⋅ concat us1 = concat ws1› emp_concat_emp'[OF ‹us1 ∈ lists 𝒞›] unfolding ‹ws1 = ε›
      concat.simps by blast
  next
    assume "ws1 ≠ ε"
    with suf.concat_pref_eq[OF ‹us1 ∈ lists 𝒞› ‹ws1 ∈ lists 𝒞› ‹p ⋅ concat us1 = concat ws1›]
    show ?thesis
      using fac_interpD(1)[OF interp, folded ‹ws1 ⋅ ws2 = ws›] by force
  qed
  show "p = ε" and "s = ε" and "us = ws"
    using eq1 eq2 ‹us1 ⋅ us2 = us› ‹ws1 ⋅ ws2 = ws› by blast+
qed

end

section ‹Marked code›

locale marked_code =
  fixes 𝒞
  assumes
    emp_not_in: "ε ∉ 𝒞" and
    marked: "u ∈ 𝒞 ⟹ v ∈ 𝒞 ⟹ hd u = hd v ⟹ u = v"

begin

lemma nemp: "u ∈ 𝒞 ⟹ u ≠ ε"
  using emp_not_in by blast

sublocale prefix_code
  by (unfold_locales) (simp_all add: emp_not_in marked nemp pref_hd_eq)


lemma marked_concat_lcp: "us ∈ lists 𝒞 ⟹ vs ∈ lists 𝒞 ⟹ concat (us ∧⇩_p vs) = (concat us) ∧⇩_p (concat vs)"
proof (induct us vs rule: list_induct2')
  case (4 x xs y ys)
  hence "x ∈ 𝒞" and "y ∈ 𝒞" and "xs ∈ lists 𝒞" and "ys ∈ lists 𝒞"
    by simp_all
  show ?case
  proof (cases)
    assume "x = y"
    thus "concat (x # xs ∧⇩_p y # ys) = concat (x # xs) ∧⇩_p concat (y # ys)"
      using "4.hyps"[OF ‹xs ∈ lists 𝒞› ‹ys ∈ lists 𝒞›] by (simp add: lcp_ext_left)
  next
    assume "x ≠ y"
    with marked[OF ‹x ∈ 𝒞› ‹y ∈ 𝒞›] have "hd x ≠ hd y" by blast
    hence "concat (x # xs) ∧⇩_p concat (y # ys) = ε"
      by (simp add: ‹x ∈ 𝒞› ‹y ∈ 𝒞› nemp lcp_distinct_hd)
    moreover have "concat (x # xs ∧⇩_p y # ys) = ε"
      using ‹x ≠ y› by simp
    ultimately show ?thesis by presburger
  qed
qed simp_all

lemma hd_concat_hd: assumes "xs ∈ lists 𝒞" and "ys ∈ lists 𝒞" and "xs ≠ ε" and "ys ≠ ε" and
  "hd (concat xs) = hd (concat ys)"
shows "hd xs = hd ys"
proof-
  have "hd (hd xs) = hd (hd ys)"
    using assms  hd_concat[OF ‹xs ≠ ε› lists_hd_in_set[THEN nemp]] hd_concat[OF ‹ys ≠ ε› lists_hd_in_set[THEN nemp]]
    by presburger

  from marked[OF lists_hd_in_set lists_hd_in_set this] assms(1-4)
  show "hd xs = hd ys"
    by simp
qed

end

section "Non-overlapping code"

locale non_overlapping =
  fixes 𝒞
  assumes
    emp_not_in: "ε ∉ 𝒞" and
    no_overlap: "u ∈ 𝒞 ⟹ v ∈ 𝒞 ⟹ z ≤p u ⟹ z ≤s v ⟹ z ≠ ε ⟹ u = v" and
    no_fac: "u ∈ 𝒞 ⟹ v ∈ 𝒞 ⟹ u ≤f v ⟹  u = v"
begin

lemma nemp: "u ∈ 𝒞  ⟹ u ≠ ε"
  using emp_not_in by force

sublocale prefix_code
  using nemp non_overlapping.no_fac non_overlapping_axioms prefix_code.intro
   prefix_imp_sublist by metis

lemma rev_non_overlapping: "non_overlapping (rev ` 𝒞)"
proof
  show "ε ∉ rev ` 𝒞"
    using nemp by force
  show "u ∈ rev ` 𝒞 ⟹ v ∈ rev ` 𝒞 ⟹ z ≤p u ⟹ z ≤s v ⟹ z ≠ ε ⟹ u = v" for u v z
    using no_overlap[reversed] unfolding rev_in_conv..
  show "u ∈ rev ` 𝒞 ⟹ v ∈ rev ` 𝒞 ⟹ u ≤f v ⟹ u = v" for u v
    using no_fac[reversed] unfolding rev_in_conv by presburger
qed

sublocale suf: suffix_code 𝒞
proof-
  interpret i: non_overlapping "rev ` 𝒞"
    using rev_non_overlapping.
  from i.prefix_code_axioms
  show "suffix_code 𝒞"
    by unfold_locales
qed

lemma overlap_concat_last: assumes  "u ∈ 𝒞" and "vs ∈ lists 𝒞" and "vs ≠ ε" and
      "r ≠ ε" and "r ≤p u" and  "r ≤s p ⋅ concat vs"
  shows  "u = last vs"
proof-
  from suffix_same_cases[OF suf_ext[OF concat_last_suf[OF ‹vs ≠ ε›]] ‹r ≤s p ⋅ concat vs›]
  show "u = last vs"
  proof (rule disjE)
    assume "r ≤s last vs"
    from no_overlap[OF ‹u ∈ 𝒞› _ ‹r ≤p u› this ‹r ≠ ε›]
    show "u = last vs"
      using ‹vs ∈ lists 𝒞› ‹vs ≠ ε› by force
  next
    assume "last vs ≤s r"
    from no_fac[OF _ ‹u ∈ 𝒞› pref_suf_fac, OF _ ‹r ≤p u›  this]
    show "u = last vs"
      using ‹vs ∈ lists 𝒞› ‹vs ≠ ε› by force
  qed
qed

lemma overlap_concat_hd: assumes  "u ∈ 𝒞" and "vs ∈ lists 𝒞" and "vs ≠ ε" and "r ≠ ε" and "r ≤s u" and  "r ≤p concat vs ⋅ s"
  shows  "u = hd vs"
proof-
  interpret c: non_overlapping "rev ` 𝒞" by (simp add: rev_non_overlapping)
  from c.overlap_concat_last[reversed, OF assms]
  show ?thesis.
qed

lemma fac_concat_fac:
  assumes "us ∈ lists 𝒞" "vs ∈ lists 𝒞"
    and "1 < card (set us)"
    and "concat vs = p ⋅ concat us ⋅ s"
  obtains ps ss where  "concat ps = p" and "concat ss = s" and "ps ⋅ us ⋅ ss = vs"
proof-
  have "us ≠ ε"
    using ‹1 < card (set us)› by fastforce
  let ?a = "hd us"
  define us1 where "us1 = takeWhile (λ b. b = ?a) us"
  define us2 where "us2 = dropWhile (λ b. b = ?a) us"
  define k where "k = ❙|us1❙|"
  have "us1 ≠ ε"
    unfolding us1_def takeWhile_eq_Nil_iff using ‹us ≠ ε› by blast
  note nemp_len[OF this, folded k_def]
  have "us = us1 ⋅ us2"
    unfolding us1_def us2_def by simp
  have "set us1 = {?a}"
    using set_sing_nemp_eq takeWhile_subset ‹us1 ≠ ε› unfolding us1_def by metis
  hence "us1 = [?a]⇧^@k"
    using sing_pow_exp unfolding k_def by fastforce
  have "last us1 = ?a"
    unfolding ‹us1 = [?a]⇧^@k›[unfolded  pow_pos2[OF ‹0 < k›]] using last_snoc.
  have "us2 ≠ ε"
    using ‹1 < card (set us)›[unfolded ‹us = us1 ⋅ us2›] ‹set us1 = {?a}› by force
  have "hd us2 ≠ ?a"
    using  hd_dropWhile[OF ‹us2 ≠ ε›[unfolded us2_def]] unfolding us2_def.
  note this[symmetric, folded ‹last us1 = ?a›]

  have "us2 ∈ lists 𝒞" "us1 ∈ lists 𝒞"
    using ‹us = us1 ⋅ us2› ‹us ∈ lists 𝒞› by simp_all
  hence "concat us2 ≠ ε"
    using ‹us2 ≠ ε› nemp by force
  hence "p ⋅ concat us1 <p concat vs"
    using ‹us = us1 ⋅ us2› unfolding ‹concat vs = p ⋅ concat us ⋅ s› by simp
  from pref_mod_list'[OF this]
  obtain j r where "j < ❙|vs❙|" "r <p vs ! j" "concat (take j vs) ⋅ r = p ⋅ concat us1".
  have "r = ε"
  proof (rule ccontr)
    assume "r ≠ ε"
    from spref_exE[OF ‹r <p vs ! j›]
    obtain z where "r ⋅ z = vs ! j" "z ≠ ε".
    from overlap_concat_last[OF _ ‹us1 ∈ lists 𝒞› ‹us1 ≠ ε› ‹r ≠ ε› sprefD1[OF ‹r <p vs ! j›] sufI[OF ‹concat (take j vs) ⋅ r = p ⋅ concat us1›]]
    have "vs ! j = last us1"
      using  nth_in_lists[OF ‹j < ❙|vs❙|› ‹vs ∈ lists 𝒞›].

    have concat_vs: "concat vs = concat (take j vs) ⋅ vs!j ⋅ concat (drop (Suc j) vs)"
      unfolding lassoc concat_take_Suc[OF ‹j < ❙|vs❙|›] concat_morph[symmetric] by force
    from this[folded ‹r ⋅ z = vs ! j›]
    have "z ⋅ concat (drop (Suc j) vs) = concat us2 ⋅ s"
      unfolding ‹concat vs = p ⋅ concat us ⋅ s› lassoc ‹concat (take j vs) ⋅ r = p ⋅ concat us1›            ‹us = us1 ⋅ us2› concat_morph
      unfolding rassoc cancel by simp
    from overlap_concat_hd[OF _ ‹us2 ∈ lists 𝒞› ‹us2 ≠ ε› ‹z ≠ ε› sufI[OF ‹r ⋅ z = vs ! j›]  prefI[OF this]]
    have "vs ! j = hd us2"
      using  nth_in_lists[OF ‹j < ❙|vs❙|› ‹vs ∈ lists 𝒞›].

    thus False
      unfolding ‹vs ! j = last us1› using  ‹last us1 ≠ hd us2› by contradiction
  qed

  have "drop j vs ∈ lists 𝒞" and "take j vs ∈ lists 𝒞"
    using ‹vs ∈ lists 𝒞› by inlists
  have "concat us2 ⋅ s = concat (drop j vs)"
    using arg_cong[OF takedrop[of j vs], of concat] ‹concat (take j vs) ⋅ r = p ⋅ concat us1›
    unfolding ‹concat vs = p ⋅ concat us ⋅ s› concat_morph ‹r = ε› emp_simps ‹us = us1 ⋅ us2› by auto
  from prefI[OF this]
  have "us2 ≤p drop j vs"
    using concat_pref_concat_conv[OF ‹us2 ∈ lists 𝒞› ‹drop j vs ∈ lists 𝒞›] by blast
  hence s: "concat (us2¯⇧^>drop j vs) = s"
    using ‹concat us2 ⋅ s = concat (drop j vs)› concat_morph_lq lqI by blast

  from ‹concat (take j vs) ⋅ r = p ⋅ concat us1›[unfolded ‹r = ε› emp_simps]
  have "concat us1 ≤s concat (take j vs)"
    by fastforce
  hence "us1 ≤s take j vs"
    using suf.concat_pref_concat_conv[reversed, OF ‹us1 ∈ lists 𝒞› ‹take j vs ∈ lists 𝒞›] by blast
  from arg_cong[OF rq_suf[OF this], of concat, unfolded concat_morph]
  have p: "concat (take j vs⇧^<¯us1 ) = p"
    using rqI[OF ‹concat (take j vs) = p ⋅ concat us1›[symmetric]]
    rq_triv by metis

  have "take j vs⇧^<¯us1  ⋅ us ⋅ us2¯⇧^>drop j vs = vs"
    unfolding ‹us = us1 ⋅ us2› rassoc lq_pref[OF ‹us2 ≤p drop j vs›]
    unfolding lassoc  rq_suf[OF ‹us1 ≤s take j vs›] by simp

  from that[OF p s this]
  show thesis.
qed

theorem prim_morph:
  assumes "ws ∈ lists 𝒞"
    and "❙|ws❙| ≠ 1"
    and "primitive ws"
  shows "primitive (concat ws)"
proof (rule ccontr)
  have "ws ∈ lists 𝒞" and "ws ⋅ ws ∈ lists 𝒞"
    using ‹ws ∈ lists 𝒞› by simp_all
  moreover have "1 < card (set ws)" using ‹primitive ws› ‹❙|ws❙| ≠ 1›
    by (rule prim_card_set)
  moreover assume "¬ primitive (concat ws)"
  then obtain k z where "2 ≤ k" and "z ⇧^@ k = concat ws"
    by (elim not_prim_primroot_expE)
  have "concat (ws ⋅ ws) = z ⋅ concat ws ⋅ z⇧^@(k-1)"
    unfolding concat_morph ‹z ⇧^@ k = concat ws›[symmetric] pow_add[symmetric] pow_Suc[symmetric]
    using ‹2 ≤ k› by simp
  ultimately obtain ps ss where "concat ps = z" and "concat ss = z⇧^@(k-1)" and  "ps ⋅ ws ⋅ ss = ws ⋅ ws"
    by (rule fac_concat_fac)
  have "ps ⇧^@ k ∈ lists 𝒞"
    using ‹ps ⋅ ws ⋅ ss = ws ⋅ ws› ‹ws ⋅ ws ∈ lists 𝒞› by inlists
  moreover have "concat (ps ⇧^@ k) = concat ws"
    unfolding concat_pow_list ‹concat ps = z› ‹z ⇧^@ k = concat ws›..
  ultimately have "ps ⇧^@ k = ws" using ‹ws ∈ lists 𝒞› by (intro is_code)
  show False
    using prim_exp_one[OF ‹primitive ws› ‹ps ⇧^@ k = ws›] ‹2 ≤ k› by presburger
qed

lemma prim_concat_conv:
  assumes "ws ∈ lists 𝒞"
    and "❙|ws❙| ≠ 1"
  shows "primitive (concat ws) ⟷ primitive ws"
  using prim_concat_prim prim_morph[OF assms]..

end

section ‹Binary code›

text‹We pay a special attention to two element codes.
In particular, we show that two words form a code if and only if they do not commute. This means that two
words either commute, or do not satisfy any nontrivial relation.
›

definition  bin_lcp  where "bin_lcp x y  =  x⋅y ∧⇩_p y⋅x"
definition  bin_lcs  where "bin_lcs x y  =  x⋅y ∧⇩_s y⋅x"

definition  bin_mismatch where "bin_mismatch x y =  (x⋅y)!❙|bin_lcp x y❙|"
definition  bin_mismatch_suf where " bin_mismatch_suf x y = bin_mismatch (rev y) (rev x)"

value[nbe] "[0::nat,1,0]!3"

lemma bin_lcs_rev: "bin_lcs x y = rev (bin_lcp (rev x) (rev y))"
  unfolding bin_lcp_def bin_lcs_def  longest_common_suffix_def rev_append using lcp_sym by fastforce

lemma bin_lcp_sym: "bin_lcp x y = bin_lcp y x"
  unfolding bin_lcp_def using lcp_sym.

lemma bin_mismatch_comm: "(bin_mismatch x y = bin_mismatch y x) ⟷ (x ⋅ y = y ⋅ x)"
  unfolding bin_mismatch_def bin_lcp_def lcp_sym[of "y ⋅ x"]
  using  lcp_mismatch'[of "x ⋅ y" "y ⋅ x", unfolded comm_comp_eq_conv[of x y]]   by fastforce

lemma bin_lcp_pref_fst_snd: "bin_lcp x y ≤p x ⋅ y"
  unfolding bin_lcp_def using lcp_pref.

lemma bin_lcp_pref_snd_fst: "bin_lcp x y ≤p y ⋅ x"
  using bin_lcp_pref_fst_snd[of y x, unfolded bin_lcp_sym[of y x]].

lemma bin_lcp_bin_lcs [reversal_rule]:  "bin_lcp (rev x) (rev y) = rev (bin_lcs x y)"
  unfolding bin_lcp_def bin_lcs_def rev_append[symmetric] lcs_lcp
    lcs_sym[of "x ⋅ y"]..

lemmas bin_lcs_sym = bin_lcp_sym[reversed]

lemma bin_lcp_len: "x ⋅ y ≠ y ⋅ x ⟹ ❙|bin_lcp x y❙| < ❙|x ⋅ y❙|"
  unfolding bin_lcp_def
  using lcp_len' pref_comm_eq by blast

lemmas bin_lcs_len = bin_lcp_len[reversed]

lemma bin_mismatch_pref_suf'[reversal_rule]:
  "bin_mismatch (rev y) (rev x) =  bin_mismatch_suf x y"
  unfolding bin_mismatch_suf_def..

subsection ‹Binary code locale›

locale binary_code =
  fixes u⇩₀ u⇩₁
  assumes non_comm: "u⇩₀ ⋅ u⇩₁ ≠ u⇩₁ ⋅ u⇩₀"

begin

text‹A crucial property of two element codes is the constant decoding delay given by the word $\alpha$,
which is a prefix of any generating word (sufficiently long), while the letter
immediately after this common prefix indicates the first element of the decomposition.
›

definition uu where "uu a = (if a then u⇩₀ else u⇩₁)"

lemma bin_code_set_bool: "{uu a,uu (¬ a)} = {u⇩₀,u⇩₁}"
  by (induct a, unfold uu_def, simp_all add: insert_commute)

lemma bin_code_set_bool': "{uu a,uu (¬ a)} = {u⇩₁,u⇩₀}"
  by (induct a, unfold uu_def, simp_all add: insert_commute)

lemma bin_code_swap: "binary_code u⇩₁ u⇩₀"
  using binary_code.intro[OF non_comm[symmetric]].

lemma bin_code_bool: "binary_code (uu a)  (uu (¬ a))"
  unfolding uu_def by (induct a, simp_all add: bin_code_swap binary_code_axioms)

lemma bin_code_neq: "u⇩₀ ≠ u⇩₁"
  using non_comm by auto

lemma bin_code_neq_bool: "uu a ≠ uu (¬ a)"
  unfolding uu_def by (induct a) (use bin_code_neq in fastforce)+

lemma bin_fst_nemp: "u⇩₀ ≠ ε" and bin_snd_nemp: "u⇩₁ ≠ ε" and bin_nemp_bool: "uu a ≠ ε"
  using non_comm uu_def by auto

lemma bin_not_comp: "¬ u⇩₀ ⋅ u⇩₁ ⨝ u⇩₁ ⋅ u⇩₀"
  using comm_comp_eq_conv non_comm by blast

lemma bin_not_comp_bool: "¬ (uu a ⋅ uu (¬ a) ⨝ uu (¬ a) ⋅ uu a)"
  unfolding uu_def by (induct a, use bin_not_comp pref_comp_sym in auto)

lemma bin_not_comp_suf: "¬ u⇩₀ ⋅ u⇩₁ ⨝⇩_s u⇩₁ ⋅ u⇩₀"
  using comm_comp_eq_conv_suf non_comm[reversed] by blast

lemma bin_not_comp_suf_bool: "¬ (uu a ⋅ uu (¬ a) ⨝⇩_s uu (¬ a) ⋅ uu a)"
  unfolding uu_def by (induct a, use bin_not_comp_suf suf_comp_sym in auto)

lemma bin_mismatch_neq: "bin_mismatch u⇩₀ u⇩₁ ≠ bin_mismatch u⇩₁ u⇩₀"
  using non_comm[folded bin_mismatch_comm].

abbreviation bin_code_lcp ("α") where  "bin_code_lcp ≡ bin_lcp u⇩₀ u⇩₁"
abbreviation bin_code_lcs where "bin_code_lcs ≡ bin_lcs u⇩₀ u⇩₁"
abbreviation bin_code_mismatch_fst ("c⇩₀") where "bin_code_mismatch_fst ≡ bin_mismatch u⇩₀ u⇩₁"
abbreviation bin_code_mismatch_snd ("c⇩₁") where "bin_code_mismatch_snd ≡ bin_mismatch u⇩₁ u⇩₀"

definition cc where "cc a = (if a then c⇩₀ else c⇩₁)"


lemmas bin_lcp_swap = bin_lcp_sym[of u⇩₀ u⇩₁, symmetric] and
       bin_lcp_pref = bin_lcp_pref_fst_snd[of u⇩₀ u⇩₁] and
       bin_lcp_pref' = bin_lcp_pref_snd_fst[of u⇩₀ u⇩₁] and
       bin_lcp_short = bin_lcp_len[OF non_comm, unfolded lenmorph]

lemmas bin_code_simps = cc_def uu_def if_True if_False bool_simps

lemma bin_lcp_bool: "bin_lcp (uu a) (uu (¬ a)) = bin_code_lcp"
  unfolding uu_def by (induct a, simp_all add: bin_lcp_swap)

lemma bin_lcp_spref: "α <p u⇩₀ ⋅ u⇩₁"
  using bin_lcp_pref bin_lcp_pref' bin_not_comp by fastforce

lemma bin_lcp_spref': "α <p u⇩₁ ⋅ u⇩₀"
  using bin_lcp_pref bin_lcp_pref' bin_not_comp by fastforce

lemma bin_lcp_spref_bool: "α <p uu a ⋅ uu (¬ a)"
  unfolding uu_def by (induct a, use  bin_lcp_spref bin_lcp_spref' in auto)

lemma bin_mismatch_bool': "α ⋅ [cc a] ≤p uu a ⋅ uu (¬ a)"
  using add_nth_pref[OF bin_lcp_spref_bool, of a]
  unfolding uu_def cc_def bin_mismatch_def bin_lcp_bool bin_lcp_swap
  by (induct a) simp_all

lemma bin_mismatch_bool: "α ⋅ [cc a] ≤p uu a ⋅ α"
proof-
  from pref_prolong[OF bin_mismatch_bool', OF triv_pref]
  have "α ⋅ [cc a] ≤p uu a ⋅ (uu (¬ a) ⋅ uu a)"
    by blast
  from pref_prod_pref_short[OF this bin_lcp_pref_snd_fst, unfolded bin_lcp_bool lenmorph sing_len]
  show ?thesis
    using nemp_len[OF bin_nemp_bool, of a] by linarith
qed

lemmas bin_fst_mismatch = bin_mismatch_bool[of True, unfolded bin_code_simps] and
       bin_fst_mismatch' = bin_mismatch_bool'[of True, unfolded bin_code_simps] and
       bin_snd_mismatch = bin_mismatch_bool[of False, unfolded bin_code_simps] and
       bin_snd_mismatch' = bin_mismatch_bool'[of False, unfolded bin_code_simps]

lemma bin_lcp_pref_all: "xs ∈ lists {u⇩₀,u⇩₁} ⟹ α ≤p concat xs ⋅ α"
proof (induct xs)
  case (Cons a xs)
  have "a ∈ {u⇩₀,u⇩₁}" and "xs ∈ lists {u⇩₀, u⇩₁}"
    using ‹a # xs ∈ lists {u⇩₀, u⇩₁}› by simp_all
  show ?case
  proof (rule two_elemP[OF ‹a ∈ {u⇩₀,u⇩₁}›], simp_all)
    show "α ≤p u⇩₀ ⋅ concat xs ⋅ α"
      using pref_extD[OF bin_fst_mismatch] Cons.hyps[OF ‹xs ∈ lists {u⇩₀, u⇩₁}›] pref_prolong by blast
  next
    show "α ≤p u⇩₁ ⋅ concat xs ⋅ α"
      using pref_extD[OF bin_snd_mismatch] Cons.hyps[OF ‹xs ∈ lists {u⇩₀, u⇩₁}›] pref_prolong by blast
  qed
qed simp

lemma bin_lcp_pref_all_hull: "w ∈ ⟨{u⇩₀,u⇩₁}⟩ ⟹ α ≤p w ⋅ α"
  using bin_lcp_pref_all using hull_concat_listsE by metis

lemma bin_lcp_mismatch_pref_all_bool: assumes "q ≤p w" and "w ∈ ⟨{uu b,uu (¬ b)}⟩" and "❙|α❙| < ❙|uu a ⋅ q❙|"
  shows "α ⋅ [cc a] ≤p uu a ⋅ q"
proof-
  have aux: "uu a ⋅ w ⋅ α = (uu a ⋅ q) ⋅ (q¯⇧^>w ⋅ α)" "{uu b,uu (¬ b)} = {u⇩₀,u⇩₁}"
    using lq_pref[OF ‹q ≤p w›] bin_code_set_bool by force+
  have "❙|α ⋅ [cc a]❙| ≤ ❙|uu a ⋅ q❙|"
    using ‹❙|α❙| < ❙|uu a ⋅ q❙|› by auto
  thus ?thesis
    using pref_prolong[OF bin_mismatch_bool  bin_lcp_pref_all_hull[OF ‹w ∈ ⟨{uu b,uu (¬ b)}⟩›[unfolded aux]], of a]
    unfolding aux by blast
qed

lemmas bin_lcp_mismatch_pref_all_fst = bin_lcp_mismatch_pref_all_bool[of _ _ True True, unfolded bin_code_simps] and
       bin_lcp_mismatch_pref_all_snd = bin_lcp_mismatch_pref_all_bool[of _ _ True False, unfolded bin_code_simps]

lemma bin_lcp_pref_all_len: assumes "q ≤p w" and "w ∈ ⟨{u⇩₀,u⇩₁}⟩" and "❙|α❙| ≤ ❙|q❙|"
  shows "α ≤p q"
  using bin_lcp_pref_all_hull[OF ‹w ∈ ⟨{u⇩₀,u⇩₁}⟩›] pref_ext[OF ‹q ≤p w›] prefix_length_prefix[OF _ _ ‹❙|bin_code_lcp❙| ≤ ❙|q❙|›] by blast

lemma bin_mismatch_all_bool: assumes "xs ∈ lists {uu b, uu (¬ b)}" shows "α ⋅ [cc a] ≤p (uu a) ⋅ concat xs ⋅ α"
  using pref_prolong[OF bin_mismatch_bool bin_lcp_pref_all, of xs a] assms unfolding  bin_code_set_bool[of b].

lemmas bin_fst_mismatch_all = bin_mismatch_all_bool[of _ True True, unfolded bin_code_simps] and
       bin_snd_mismatch_all = bin_mismatch_all_bool[of _ True False, unfolded bin_code_simps]

lemma bin_mismatch_all_hull_bool: assumes "w ∈ ⟨{uu b,uu (¬ b)}⟩" shows "α ⋅ [cc a] ≤p uu a ⋅ w ⋅ α"
  using bin_mismatch_all_bool hull_concat_listsE[OF assms] by metis

lemmas bin_fst_mismatch_all_hull = bin_mismatch_all_hull_bool[of _ True True, unfolded bin_code_simps] and
       bin_snd_mismatch_all_hull = bin_mismatch_all_hull_bool[of _ True False, unfolded bin_code_simps]

lemma bin_mismatch_all_len_bool: assumes "q ≤p uu a ⋅ w" and "w ∈ ⟨{uu b,uu (¬ b)}⟩" and "❙|α❙| < ❙|q❙|"
  shows "α ⋅ [cc a] ≤p q"
proof-
  have "❙|α ⋅ [cc a]❙| ≤ ❙|uu a ⋅ w❙|" "❙|α ⋅ [cc a]❙| ≤ ❙|q❙|"
    using less_le_trans[OF ‹❙|α❙| < ❙|q❙|› pref_len[OF ‹q ≤p uu a ⋅ w›]] ‹❙|α❙| < ❙|q❙|› by force+
  from pref_prod_le[OF bin_mismatch_all_hull_bool[OF assms(2), unfolded lassoc], OF this(1)]
  show ?thesis
    by (rule prefix_length_prefix) fact+
qed

lemmas bin_fst_mismatch_all_len = bin_mismatch_all_len_bool[of _ True _ True, unfolded bin_code_simps] and
       bin_snd_mismatch_all_len = bin_mismatch_all_len_bool[of _ False _ True, unfolded bin_code_simps]

lemma bin_code_delay: assumes "❙|α❙| ≤ ❙|q⇩₀❙|" and "❙|α❙| ≤ ❙|q⇩₁❙|" and
      "q⇩₀ ≤p u⇩₀ ⋅ w⇩₀" and "q⇩₁ ≤p u⇩₁ ⋅ w⇩₁" and
      "w⇩₀ ∈ ⟨{u⇩₀, u⇩₁}⟩" and "w⇩₁ ∈ ⟨{u⇩₀, u⇩₁}⟩"
  shows "q⇩₀ ∧⇩_p q⇩₁ = α"
proof-
  have p1: "α ⋅ [c⇩₀] ≤p u⇩₀ ⋅ w⇩₀ ⋅ α"
    using assms(5) using bin_fst_mismatch_all_hull by auto
  have p2: "α ⋅ [c⇩₁] ≤p u⇩₁ ⋅ w⇩₁ ⋅ α"
    using assms(6) using bin_snd_mismatch_all_hull by auto
  have lcp: "u⇩₀ ⋅ w⇩₀ ⋅ α ∧⇩_p u⇩₁ ⋅ w⇩₁ ⋅ α = α"
    using lcp_first_mismatch_pref[OF p1 p2 bin_mismatch_neq].
  from lcp_extend_eq[of "q⇩₀" "u⇩₀ ⋅ w⇩₀ ⋅ α" "q⇩₁" "u⇩₁ ⋅ w⇩₁ ⋅ α",
       unfolded this,OF _ _ assms(1-2)]
  show ?thesis
    using pref_ext[OF ‹q⇩₀ ≤p u⇩₀ ⋅ w⇩₀›] pref_ext[OF ‹q⇩₁ ≤p u⇩₁ ⋅ w⇩₁›] by force
qed

lemma hd_lq_mismatch_fst: "hd (α¯⇧^>(u⇩₀ ⋅ α)) = c⇩₀"
  using hd_lq_conv_nth[OF prefix_snocD[OF bin_fst_mismatch]] bin_fst_mismatch
  by (auto simp add: prefix_def)

lemma hd_lq_mismatch_snd: "hd (α¯⇧^>(u⇩₁ ⋅ α)) = c⇩₁"
  using hd_lq_conv_nth[OF prefix_snocD[OF bin_snd_mismatch]] bin_snd_mismatch
  by (auto simp add: prefix_def)

lemma hds_bin_mismatch_neq: "hd (α¯⇧^>(u⇩₀ ⋅ α)) ≠ hd (α¯⇧^>(u⇩₁ ⋅ α))"
  unfolding hd_lq_mismatch_fst hd_lq_mismatch_snd
  using bin_mismatch_neq.

lemma bin_lcp_fst_pow_pref: assumes "0 < k" shows "α ⋅ [c⇩₀] ≤p u⇩₀⇧^@k ⋅ u⇩₁ ⋅ z"
  using assms
proof (induct k rule: nat_induct_non_zero)
  case 1
  then show ?case
    unfolding pow_list_1 using  pref_prolong[OF bin_fst_mismatch' triv_pref].
next
  case (Suc n)
  show ?case
    unfolding pow_Suc rassoc
    by (rule pref_prolong[OF bin_fst_mismatch])
    (use append_prefixD[OF Suc.hyps(2)] in blast)
qed

lemmas bin_lcp_snd_pow_pref = binary_code.bin_lcp_fst_pow_pref[OF bin_code_swap, unfolded bin_lcp_swap]

lemma bin_lcp_fst_lcp: "α ≤p u⇩₀ ⋅ α" and bin_lcp_snd_lcp: "α ≤p u⇩₁ ⋅ α"
  using pref_extD[OF bin_fst_mismatch]  pref_extD[OF bin_snd_mismatch].

lemma bin_lcp_pref_all_set: assumes "set ws = {u⇩₀,u⇩₁}"
  shows "α ≤p concat ws"
proof-
  have "ws ∈ lists {u⇩₀, u⇩₁}"
    using assms by blast
  have "❙|u⇩₀❙| + ❙|u⇩₁❙| ≤ ❙|concat ws❙|"
    using assms two_in_set_concat_len[OF bin_code_neq] by simp
  with pref_prod_le[OF bin_lcp_pref_all[OF ‹ws ∈ lists {u⇩₀, u⇩₁}›]] bin_lcp_short
  show ?thesis
    by simp
qed

lemma bin_lcp_conjug_morph:
  assumes "u ∈ ⟨{u⇩₀,u⇩₁}⟩" and "v ∈ ⟨{u⇩₀,u⇩₁}⟩"
  shows "α¯⇧^>(u ⋅ α) ⋅ α¯⇧^>(v ⋅ α) = α¯⇧^>((u ⋅ v) ⋅ α)"
  unfolding lq_reassoc[OF bin_lcp_pref_all_hull[OF ‹u ∈ ⟨{u⇩₀,u⇩₁}⟩›]] rassoc
    lq_pref[OF bin_lcp_pref_all_hull[OF ‹v ∈ ⟨{u⇩₀,u⇩₁}⟩›]]..

lemma lcp_bin_conjug_prim_iff:
  "set ws = {u⇩₀,u⇩₁} ⟹ primitive (α¯⇧^>(concat ws) ⋅ α) ⟷ primitive (concat ws)"
  using conjug_prim_iff[OF root_conjug[OF pref_ext[OF bin_lcp_pref_all_set]], symmetric]
  unfolding lq_reassoc[OF bin_lcp_pref_all_set] by simp

lemma bin_lcp_conjug_inj_on: "inj_on (λu. α¯⇧^>(u ⋅ α)) ⟨{u⇩₀,u⇩₁}⟩"
  unfolding inj_on_def using bin_lcp_pref_all_hull cancel_right lq_pref
  by metis

lemma bin_code_lcp_marked: assumes "us ∈ lists {u⇩₀,u⇩₁}" and "vs ∈ lists {u⇩₀,u⇩₁}" and "hd us ≠ hd vs"
  shows "concat us ⋅ α ∧⇩_p concat vs ⋅ α = α"
proof (cases "us = ε ∨ vs = ε")
  assume "us = ε ∨ vs = ε"
  thus ?thesis
    using append_self_conv2 assms(1) assms(2) bin_lcp_pref_all concat.simps(1) lcp_pref_conv lcp_sym by metis
next
  assume "¬ (us = ε ∨ vs = ε)" hence "us ≠ ε" and "vs ≠ ε" by blast+
  have spec_case: "concat us ⋅ α ∧⇩_p concat vs ⋅ α = α" if "us ∈ lists {u⇩₀,u⇩₁}" and "vs ∈ lists {u⇩₀,u⇩₁}" and "hd us = u⇩₀" and "hd vs = u⇩₁" and "us ≠ ε" and "vs ≠ ε" for us vs
  proof-
    have "concat us = u⇩₀ ⋅ concat (tl us)"
      unfolding hd_concat_tl[OF ‹us ≠ ε›, symmetric] ‹hd us = u⇩₀›..
    from bin_fst_mismatch_all[OF tl_in_lists[OF ‹us ∈ lists {u⇩₀,u⇩₁}›], folded rassoc this]
    have pref1: "α ⋅ [c⇩₀] ≤p concat us ⋅ α".
    have "concat vs = u⇩₁ ⋅ concat (tl vs)"
      unfolding hd_concat_tl[OF ‹vs ≠ ε›, symmetric] ‹hd vs = u⇩₁›..
    from bin_snd_mismatch_all[OF tl_in_lists[OF ‹vs ∈ lists {u⇩₀,u⇩₁}›], folded rassoc this]
    have pref2: "α ⋅ [c⇩₁] ≤p concat vs ⋅ α".
    show ?thesis
      using  lcp_first_mismatch_pref[OF pref1 pref2 bin_mismatch_neq].
  qed
  have "hd us ∈  {u⇩₀,u⇩₁}" and "hd vs ∈  {u⇩₀,u⇩₁}" using
      lists_hd_in_set[OF ‹us ≠ ε› ‹us ∈ lists {u⇩₀, u⇩₁}›] lists_hd_in_set[OF ‹vs ≠ ε› ‹vs ∈ lists {u⇩₀, u⇩₁}›].
  then consider "hd us = u⇩₀ ∧ hd vs = u⇩₁" | "hd us = u⇩₁ ∧ hd vs = u⇩₀"
    using ‹hd us ≠ hd vs› by fastforce
  then show ?thesis
    using spec_case[rule_format] ‹us ≠ ε› ‹vs ≠ ε› assms lcp_sym by metis
qed

― ‹ALT PROOF›
lemma  assumes "us ∈ lists {u⇩₀,u⇩₁}" and "vs ∈ lists {u⇩₀,u⇩₁}" and "hd us ≠ hd vs"
  shows "concat us ⋅ α ∧⇩_p concat vs ⋅ α = α"
  using assms
proof (induct us vs rule: list_induct2')
  case (2 x xs)
  show ?case
    using bin_lcp_pref_all[OF ‹x # xs ∈ lists {u⇩₀, u⇩₁}›, folded lcp_pref_conv, unfolded lcp_sym[of α]] by simp
next
  case (3 y ys)
  show ?case
    using bin_lcp_pref_all[OF ‹y # ys ∈ lists {u⇩₀, u⇩₁}›, folded lcp_pref_conv] by simp
next
  case (4 x xs y ys)
  interpret i: binary_code x y
    using "4.prems"(1) "4.prems"(2) "4.prems"(3) non_comm binary_code.intro by auto
  have alph: "{u⇩₀,u⇩₁} = {x,y}"
    using "4.prems"(1) "4.prems"(2) "4.prems"(3) by auto
  from disjE[OF this[unfolded doubleton_eq_iff]]
  have "i.bin_code_lcp = α"
    using i.bin_lcp_swap[symmetric] by blast
  have c0: "i.bin_code_lcp ⋅ [i.bin_code_mismatch_fst] ≤p x ⋅ concat xs ⋅ i.bin_code_lcp"
    using  i.bin_lcp_pref_all[of xs] ‹x # xs ∈ lists {u⇩₀, u⇩₁}›[unfolded Cons_in_lists_iff alph]
      pref_prolong[OF i.bin_fst_mismatch] by blast
  have c1: "i.bin_code_lcp ⋅ [i.bin_code_mismatch_snd] ≤p y ⋅ concat ys ⋅ i.bin_code_lcp"
    using pref_prolong[OF conjunct2[OF ‹y # ys ∈ lists {u⇩₀, u⇩₁}›[unfolded      Cons_in_lists_iff alph],
          THEN i.bin_snd_mismatch_all[of ys]], OF self_pref].
  have "i.bin_code_lcp⋅[i.bin_code_mismatch_fst] ∧⇩_p i.bin_code_lcp⋅[i.bin_code_mismatch_snd] = i.bin_code_lcp"
    by (simp add: i.bin_mismatch_neq lcp_first_mismatch')
  from lcp_rulers[OF c0 c1, unfolded this, unfolded bin_lcp_swap]
  show ?case
    unfolding concat.simps(2) rassoc using i.bin_mismatch_neq
      ‹i.bin_code_lcp = α› by force
qed simp

lemma bin_code_lcp_concat: assumes "us ∈ lists {u⇩₀,u⇩₁}" and "vs ∈ lists {u⇩₀,u⇩₁}" and "¬ us ⨝ vs"
  shows "concat us ⋅ α ∧⇩_p concat vs ⋅ α = concat (us ∧⇩_p vs) ⋅ α"
proof-
  obtain us' vs' where us: "(us ∧⇩_p vs) ⋅ us' = us" and vs: "(us ∧⇩_p vs) ⋅ vs' = vs" and "us' ≠ ε" and "vs' ≠ ε" and "hd us' ≠ hd vs'"
    using lcp_mismatchE[OF ‹¬ us ⨝ vs›].
  have cu: "concat us ⋅ α = concat (us ∧⇩_p vs) ⋅ concat us' ⋅ α"
    unfolding lassoc concat_morph[symmetric] us..
  have cv: "concat vs ⋅ α = concat (us ∧⇩_p vs) ⋅ concat vs' ⋅ α"
    unfolding lassoc concat_morph[symmetric] vs..
  have "us' ∈ lists {u⇩₀,u⇩₁}"
    using ‹us ∈ lists {u⇩₀,u⇩₁}› us by inlists
  have "vs' ∈ lists {u⇩₀,u⇩₁}"
    using ‹vs ∈ lists {u⇩₀,u⇩₁}› vs by inlists
  show "concat us ⋅ α ∧⇩_p concat vs ⋅ α = concat (us ∧⇩_p vs) ⋅ α"
    unfolding cu cv
    using bin_code_lcp_marked[OF ‹us' ∈ lists {u⇩₀,u⇩₁}› ‹vs' ∈ lists {u⇩₀,u⇩₁}› ‹hd us' ≠ hd vs'›]
    unfolding lcp_ext_left by fast
qed

lemma bin_code_lcp_concat': assumes "us ∈ lists {u⇩₀,u⇩₁}" and "vs ∈ lists {u⇩₀,u⇩₁}" and "¬ concat us ⨝ concat vs"
  shows "concat us ∧⇩_p concat vs = concat (us ∧⇩_p vs) ⋅ α"
  using bin_code_lcp_concat[OF assms(1-2)] assms(3) lcp_ext_right_conv pref_concat_pref prefix_comparable_def by metis

lemma bin_lcp_pows:  "0 < k ⟹ 0 < l ⟹ u⇩₀⇧^@k ⋅ u⇩₁ ⋅ z ∧⇩_p u⇩₁⇧^@l ⋅ u⇩₀ ⋅ z' = α"
  using lcp_first_mismatch_pref[OF bin_lcp_fst_pow_pref bin_lcp_snd_pow_pref bin_mismatch_neq].

theorem bin_code: assumes "us ∈ lists {u⇩₀,u⇩₁}" and "vs ∈ lists {u⇩₀,u⇩₁}" and "concat us = concat vs"
  shows "us = vs"
  using assms
proof (induct us vs rule: list_induct2')
  case (4 x xs y ys)
  then show ?case
  proof-
    have "x =y"
      using bin_code_lcp_marked[OF ‹x # xs ∈ lists {u⇩₀, u⇩₁}› ‹y # ys ∈ lists {u⇩₀, u⇩₁}›] ‹y # ys ∈ lists {u⇩₀, u⇩₁}› non_comm
      unfolding ‹concat (x # xs) = concat (y # ys)› unfolding concat.simps(2) lcp_self list.sel(1)
      by auto
     thus "x # xs = y # ys"
      using "4.hyps" ‹concat (x # xs) = concat (y # ys)›[unfolded  concat.simps(2) ‹x = y›, unfolded cancel]
        ‹y # ys ∈ lists {u⇩₀, u⇩₁}›[unfolded Cons_in_lists_iff] ‹x # xs ∈ lists {u⇩₀, u⇩₁}›[unfolded Cons_in_lists_iff]
      by simp
  qed
qed (auto simp: bin_fst_nemp bin_snd_nemp)

lemma code_bin_roots: "binary_code (ρ u⇩₀) (ρ u⇩₁)"
  using non_comm comm_primroot_conv'  by (unfold_locales) blast

sublocale code "{u⇩₀,u⇩₁}"
  using bin_code by unfold_locales

lemma primroot_dec: "(Dec {ρ u⇩₀, ρ u⇩₁} u⇩₀) = [ρ u⇩₀]⇧^@e⇩_ρ u⇩₀" "(Dec {ρ u⇩₀, ρ u⇩₁} u⇩₁) = [ρ u⇩₁]⇧^@e⇩_ρ u⇩₁"
proof-
  interpret rs: binary_code "ρ u⇩₀" "ρ u⇩₁"
    by (simp add: code_bin_roots)
  from primroot_exp_eq
  have "concat ([ρ u⇩₀]⇧^@e⇩_ρ u⇩₀) = u⇩₀" "concat ([ρ u⇩₁]⇧^@e⇩_ρ u⇩₁) = u⇩₁"
    by force+
  from rs.code_unique_dec[OF _ this(1)] rs.code_unique_dec[OF _ this(2)]
  show "(Dec {ρ u⇩₀, ρ u⇩₁} u⇩₀) = [ρ u⇩₀]⇧^@e⇩_ρ u⇩₀" "(Dec {ρ u⇩₀, ρ u⇩₁} u⇩₁) = [ρ u⇩₁]⇧^@e⇩_ρ u⇩₁"
    by (simp_all add: sing_pow_lists)
qed

lemma bin_code_prefs: assumes "w ∈ ⟨{u⇩₀,u⇩₁}⟩" and "p ≤p w" "w' ∈ ⟨{u⇩₀,u⇩₁}⟩" and "❙|u⇩₁❙| ≤ ❙|p❙|"
  shows " ¬ u⇩₀ ⋅  p ≤p u⇩₁ ⋅ w'"
proof
  assume contr: "u⇩₀ ⋅ p  ≤p u⇩₁ ⋅ w'"
  have "❙|α❙| < ❙|u⇩₀ ⋅ p❙|"
    using ‹❙|u⇩₁❙| ≤ ❙|p❙|› bin_lcp_short by auto
  hence "α ⋅ [c⇩₀] ≤p u⇩₀ ⋅ p"
    using ‹p ≤p w›  ‹w ∈ ⟨{u⇩₀,u⇩₁}⟩› bin_lcp_mismatch_pref_all_fst by auto
  from pref_ext[OF pref_trans[OF this contr], unfolded rassoc]
  have "α ⋅ [c⇩₀] ≤p u⇩₁ ⋅ w' ⋅ α".
  from bin_mismatch_neq same_sing_pref[OF bin_snd_mismatch_all_hull[OF ‹w' ∈ ⟨{u⇩₀,u⇩₁}⟩›] this]
  show False
    by simp
qed

lemma bin_code_rev: "binary_code (rev u⇩₀) (rev u⇩₁)"
  by (unfold_locales, unfold comm_rev_iff, simp add: non_comm)


lemma bin_lcp_pows_lcp:  "0 < k ⟹ 0 < l ⟹ u⇩₀⇧^@k ⋅ u⇩₁⇧^@l ∧⇩_p u⇩₁⇧^@l ⋅ u⇩₀⇧^@k = u⇩₀ ⋅ u⇩₁ ∧⇩_p u⇩₁ ⋅ u⇩₀"
   using bin_lcp_pows unfolding bin_lcp_def using pow_pos by metis

lemma bin_mismatch: "u⇩₀ ⋅ α ∧⇩_p u⇩₁ ⋅ α = α"
  using lcp_first_mismatch_pref[OF bin_fst_mismatch bin_snd_mismatch bin_mismatch_neq].

lemma not_comp_bin_fst_snd: "¬ u⇩₀ ⋅ α ⨝ u⇩₁ ⋅  α"
  using ruler_comp[OF bin_fst_mismatch bin_snd_mismatch] bin_mismatch_neq
  unfolding prefix_comparable_def pref_cancel_conv by force

theorem bin_bounded_delay: assumes "z ≤p u⇩₀ ⋅ w⇩₀" and "z ≤p u⇩₁ ⋅ w⇩₁"
  and "w⇩₀ ∈ ⟨{u⇩₀,u⇩₁}⟩" and "w⇩₁ ∈ ⟨{u⇩₀,u⇩₁}⟩"
shows "❙|z❙| ≤ ❙|α❙|"
proof (rule leI, rule notI)
  assume "❙|α❙| < ❙|z❙|"
  hence "❙|α ⋅ [a]❙| ≤ ❙|z❙|" for a
    unfolding lenmorph sing_len by simp
  have "z ≤p u⇩₀ ⋅ w⇩₀ ⋅ α" and "z ≤p u⇩₁ ⋅ w⇩₁ ⋅ α"
    using  pref_prolong[OF ‹z ≤p u⇩₀ ⋅ w⇩₀› triv_pref] pref_prolong[OF ‹z ≤p u⇩₁ ⋅ w⇩₁› triv_pref].
  have "α ⋅ [c⇩₀] ≤p u⇩₀ ⋅ w⇩₀ ⋅ α" and "α ⋅ [c⇩₁] ≤p u⇩₁ ⋅ w⇩₁ ⋅ α"
    using bin_fst_mismatch_all_hull[OF ‹w⇩₀ ∈ ⟨{u⇩₀,u⇩₁}⟩›] bin_snd_mismatch_all_hull[OF ‹w⇩₁ ∈ ⟨{u⇩₀,u⇩₁}⟩›].
  from ‹z ≤p u⇩₀ ⋅ w⇩₀ ⋅ α› ‹α ⋅ [c⇩₀] ≤p u⇩₀ ⋅ w⇩₀ ⋅ α› ‹❙|α ⋅ [c⇩₀]❙| ≤ ❙|z❙|›
  have "α ⋅ [c⇩₀] ≤p z"
    using prefix_length_prefix by blast
  from ‹z ≤p u⇩₁ ⋅ w⇩₁ ⋅ α› ‹α ⋅ [c⇩₁] ≤p u⇩₁ ⋅ w⇩₁ ⋅ α› ‹❙|α ⋅ [c⇩₁]❙| ≤ ❙|z❙|›
  have "α ⋅ [c⇩₁] ≤p z"
    using prefix_length_prefix by blast
  from ‹α ⋅ [c⇩₁] ≤p z› ‹α ⋅ [c⇩₀] ≤p z› bin_mismatch_neq
  show False
    unfolding prefix_def by force
qed

thm binary_code.bin_lcp_pows_lcp

lemma prim_roots_lcp: "bin_lcp  (ρ u⇩₀)  (ρ u⇩₁)  = α"
proof-
  obtain k where "ρ u⇩₀⇧^@k = u⇩₀" "0 < k"
    using primroot_expE.
  obtain m where "ρ u⇩₁⇧^@m = u⇩₁" "0 < m"
    using primroot_expE.
  have "ρ u⇩₀ ⋅ ρ u⇩₁ ≠ ρ u⇩₁ ⋅ ρ u⇩₀"
    using non_comm[unfolded comm_primroot_conv'[of u⇩₀]].
  then interpret r: binary_code "ρ u⇩₀" "ρ u⇩₁" by unfold_locales
  from r.bin_lcp_pows_lcp[OF ‹0 < k› ‹0 < m›, unfolded ‹ρ u⇩₁⇧^@m = u⇩₁› ‹ρ u⇩₀⇧^@k = u⇩₀›, symmetric]
  show ?thesis
     unfolding bin_lcp_def.
qed

lemma bin_roots_decompose:
        "Dec {ρ u⇩₀, u⇩₁} u⇩₀ = [ρ u⇩₀]⇧^@e⇩_ρ u⇩₀"
        "Dec {ρ u⇩₀, u⇩₁} u⇩₁ = [u⇩₁]"
        "Dec {u⇩₀, ρ u⇩₁} u⇩₁ = [ρ u⇩₁]⇧^@e⇩_ρ u⇩₁"
        "Dec {u⇩₀, ρ u⇩₁} u⇩₀ = [u⇩₀]"
        "Dec {u⇩₀,u⇩₁} u⇩₀ = [u⇩₀]"
        "Dec {u⇩₀,u⇩₁} u⇩₁ = [u⇩₁]"
proof-
  show "Dec {u⇩₀,u⇩₁} u⇩₀ = [u⇩₀]" "Dec {u⇩₀,u⇩₁} u⇩₁ = [u⇩₁]"
    using code_el_dec by simp_all
  interpret r: binary_code "ρ u⇩₀" u⇩₁
    using non_comm unfolding binary_code_def using comm_primroot_conv[of u⇩₁ u⇩₀]
    by presburger
  interpret r': binary_code u⇩₀ "ρ u⇩₁"
    using non_comm unfolding binary_code_def using comm_primroot_conv[of u⇩₀ u⇩₁]
    by presburger
  from r.code_el_dec
  show "Dec {ρ u⇩₀, u⇩₁} u⇩₁ = [u⇩₁]"
    by force
  from r'.code_el_dec
  show "Dec {u⇩₀, ρ u⇩₁} u⇩₀ = [u⇩₀]"
    by force
  show "Dec {ρ u⇩₀, u⇩₁} u⇩₀ = [ρ u⇩₀]⇧^@e⇩_ρ u⇩₀"
    using r.code_unique_dec'[OF sing_pow_lists[of "ρ u⇩₀" "{ρ u⇩₀, u⇩₁}" "e⇩_ρ u⇩₀"]]
    unfolding concat_pow_list concat_sing' primroot_exp_eq by simp
  show "Dec {u⇩₀, ρ u⇩₁} u⇩₁ = [ρ u⇩₁] ⇧^@ e⇩_ρ u⇩₁"
    using r'.code_unique_dec'[OF sing_pow_lists[of "ρ u⇩₁" "{u⇩₀, ρ u⇩₁}" "e⇩_ρ u⇩₁"]]
    unfolding concat_pow_list concat_sing' primroot_exp_eq by simp
qed

lemma ref_fst_sq: "Ref {ρ u⇩₀, u⇩₁}[u⇩₀,u⇩₀] = [ρ u⇩₀]⇧^@(e⇩_ρ u⇩₀ * 2)"
  unfolding refine_def pow_mult pow_list_2
  using bin_roots_decompose by simp

lemma ref_fst_pow: "Ref {ρ u⇩₀, u⇩₁}[u⇩₀]⇧^@k = [ρ u⇩₀]⇧^@(e⇩_ρ u⇩₀ * k)"
  unfolding refine_def pow_mult pow_list_2
  using bin_roots_decompose by simp

lemma bin_code_concat_len: assumes "ws ∈ lists {u⇩₀,u⇩₁}"
  shows "❙|concat ws❙| = count_list ws u⇩₀ * ❙|u⇩₀❙| + count_list ws u⇩₁ * ❙|u⇩₁❙|"
  using bin_len_concat[OF bin_code_neq assms].

subsubsection ‹Maximal r-prefixes›

lemma bin_lcp_per_root_max_pref_short:  assumes "α <p u⇩₀ ⋅ u⇩₁ ∧⇩_p r ⋅ u⇩₀ ⋅ u⇩₁" and "r ≠ ε" and "q ≤p w" and "w ∈ ⟨{u⇩₀, u⇩₁}⟩"
  shows "u⇩₁ ⋅ q ∧⇩_p r ⋅ u⇩₁ ⋅ q = take ❙|u⇩₁ ⋅ q❙| α"
proof-
  have "q ⨝ α"
    using bin_lcp_pref_all_hull[OF ‹w ∈ ⟨{u⇩₀, u⇩₁}⟩›] ruler_comp[OF ‹q ≤p w›, of α "w ⋅ α"] by blast
  hence comp1: "u⇩₁ ⋅ q ⨝ α ⋅ [c⇩₁]"
    using  ruler_comp[OF self_pref bin_snd_mismatch, of "u⇩₁ ⋅ q"] unfolding comp_cancel by blast

  from add_nth_pref[OF assms(1), THEN pref_lcp_pref] bin_fst_mismatch'
  have "(u⇩₀ ⋅ u⇩₁ ∧⇩_p r ⋅ u⇩₀ ⋅ u⇩₁) ! ❙|α❙| = c⇩₀"
    using same_sing_pref by fast

  from add_nth_pref[OF assms(1), unfolded this]
  have "α ⋅ [c⇩₀] ≤p r ⋅ u⇩₀ ⋅ u⇩₁"
    by force

  have len: "❙|α ⋅ [c⇩₀]❙| ≤ ❙|r ⋅ α❙|"
    using nemp_len[OF ‹r ≠ ε›] unfolding lenmorph sing_len by linarith

  have comp2: "r ⋅ u⇩₁ ⋅ q ⨝ α ⋅ [c⇩₀]"
  proof(rule ruler_comp[OF _ _ comp_refl])
    show "r ⋅ u⇩₁ ⋅ q ≤p r ⋅ u⇩₁ ⋅ w ⋅ α"
      using ‹q ≤p w› by fastforce
    show "α ⋅ [c⇩₀] ≤p r ⋅ u⇩₁ ⋅ w ⋅ α"
    proof(rule pref_prolong)
      show "α ⋅ [c⇩₀] ≤p r ⋅ α"
        using ‹α ⋅ [c⇩₀] ≤p r ⋅ u⇩₀ ⋅ u⇩₁› bin_lcp_pref len pref_prod_pref_short by blast
      show "α ≤p u⇩₁ ⋅ w ⋅ α"
        using ‹w ∈ ⟨{u⇩₀, u⇩₁}⟩› bin_lcp_pref_all_hull[of "u⇩₁ ⋅ w"] by auto
    qed
  qed

  have min: "(min ❙|u⇩₁ ⋅ q❙| ❙|r ⋅ u⇩₁ ⋅ q❙|) = ❙|u⇩₁ ⋅ q❙|"
    unfolding lenmorph by simp

  show ?thesis
    using  bin_mismatch_neq double_ruler[OF comp1 comp2,unfolded min]
    by (simp add: lcp_mismatch_eq_len mismatch_incopm)
qed

lemma bin_per_root_max_pref_short:  assumes "(u⇩₀ ⋅ u⇩₁) <p r ⋅ u⇩₀ ⋅ u⇩₁" and "q ≤p w" and "w ∈ ⟨{u⇩₀, u⇩₁}⟩"
  shows "u⇩₁ ⋅ q ∧⇩_p r ⋅ u⇩₁ ⋅ q = take ❙|u⇩₁ ⋅ q❙| α"
proof (rule bin_lcp_per_root_max_pref_short[OF _ _ assms(2-3)])
  show "α <p u⇩₀ ⋅ u⇩₁ ∧⇩_p r ⋅ u⇩₀ ⋅ u⇩₁"
    unfolding lcp.absorb3[OF assms(1)] using bin_fst_mismatch'[THEN prefix_snocD].
qed (use assms(1) in blast)

lemma bin_root_max_pref_long:  assumes "r ⋅ u⇩₀ ⋅ u⇩₁ =  u⇩₀ ⋅ u⇩₁ ⋅ r" and "q ≤p w" and "w ∈ ⟨{u⇩₀, u⇩₁}⟩" and "❙|α❙| ≤ ❙|q❙|"
  shows "u⇩₀ ⋅ α  ≤p u⇩₀ ⋅ q ∧⇩_p r ⋅ u⇩₀ ⋅ q"
proof (rule pref_pref_lcp)
  have len: " ❙|u⇩₀ ⋅ α❙| ≤ ❙|r ⋅ u⇩₀ ⋅ α❙|"
    by simp
  from bin_lcp_pref_all_len[OF assms(2-4)]
  show "u⇩₀ ⋅ α ≤p u⇩₀ ⋅ q"
    unfolding pref_cancel_conv.
  have "u⇩₀ ⋅ α ≤p r ⋅ u⇩₀ ⋅ α"
  proof(rule ruler_le[OF _ _ len])
    show "u⇩₀ ⋅ α ≤p (r ⋅ u⇩₀ ⋅ u⇩₁) ⋅ u⇩₀ ⋅ u⇩₁"
      unfolding assms(1) unfolding rassoc pref_cancel_conv assms(1)
      using pref_ext[OF pref_ext[OF bin_lcp_pref'], unfolded rassoc].
    show "r ⋅ u⇩₀ ⋅ α ≤p (r ⋅ u⇩₀ ⋅ u⇩₁) ⋅ u⇩₀ ⋅ u⇩₁"
      unfolding rassoc pref_cancel_conv using pref_ext[OF bin_lcp_pref', unfolded rassoc].
  qed
  from pref_prolong[OF this[unfolded lassoc], OF ‹α ≤p q›, unfolded rassoc]
  show "u⇩₀ ⋅ α ≤p r ⋅ u⇩₀ ⋅ q".
qed

lemma per_root_lcp_per_root: "u⇩₀ ⋅ u⇩₁ <p r ⋅ u⇩₀ ⋅ u⇩₁ ⟹ α ⋅ [c⇩₀] ≤p r ⋅ α"
  using per_root_pref_sing[OF _ bin_fst_mismatch'].

lemma per_root_bin_fst_snd_lcp:  assumes "u⇩₀ ⋅ u⇩₁ <p r ⋅ u⇩₀ ⋅ u⇩₁" and
                   "q ≤p w" and "w ∈ ⟨{u⇩₀,u⇩₁}⟩" and "❙|α❙| < ❙|u⇩₁ ⋅ q❙|"
                   "q' ≤p w'" and "w' ∈ ⟨{u⇩₀,u⇩₁}⟩" and "❙|α❙| ≤ ❙|q'❙|"
  shows "u⇩₁ ⋅ q ∧⇩_p r ⋅ q' = α"
proof-
  have pref1: "α ⋅ [c⇩₁] ≤p u⇩₁ ⋅ q"
    using ‹❙|α❙| < ❙|u⇩₁ ⋅ q❙|› ‹q ≤p w› bin_snd_mismatch_all_len[of "u⇩₁ ⋅ q", OF _ ‹w ∈ ⟨{u⇩₀,u⇩₁}⟩›]
    unfolding pref_cancel_conv by blast

  have "α ≤p q'"
    using ‹❙|α❙| ≤ ❙|q'❙|› ‹q' ≤p w'› ‹w' ∈ ⟨{u⇩₀,u⇩₁}⟩› bin_lcp_pref_all_len by blast
  have pref2: "α ⋅ [c⇩₀] ≤p r ⋅ α"
    using assms(1) per_root_lcp_per_root by auto
  hence pref2: "α ⋅ [c⇩₀] ≤p r ⋅ q'"
    using ‹α ≤p q'› pref_prolong by blast

  show ?thesis
    using lcp_first_mismatch_pref[OF pref1 pref2 bin_mismatch_neq[symmetric]].

qed






end
text ‹lemmas allowing to translate properties of binary code to its roots›

named_theorems bin_code_primroots
lemma bin_lcp_eq_primroots [bin_code_primroots]: assumes "x ⋅ y ≠ y ⋅ x"
  shows "bin_lcp (ρ x) (ρ y) = bin_lcp x y"
using binary_code.prim_roots_lcp[OF binary_code.intro[OF assms]].

lemma bin_lcs_eq_primroots [bin_code_primroots]: assumes "x ⋅ y ≠ y ⋅ x"
  shows "bin_lcs (ρ x) (ρ y) = bin_lcs x y"
  using bin_lcp_eq_primroots[reversed, OF assms[symmetric]].

lemma bin_mismatch_fst_eq_primroots [bin_code_primroots]: assumes "x ⋅ y ≠ y ⋅ x"
  shows "bin_mismatch (ρ x) (ρ y) = bin_mismatch x y"
proof-
  interpret binary_code x y
    using assms by unfold_locales
  interpret r: binary_code "ρ x" "ρ y"
    using assms  by unfold_locales (simp add: comm_primroot_conv'[of x])
  have "r.bin_code_lcp = bin_code_lcp"
    using prim_roots_lcp.
  have "bin_lcp (ρ x) (ρ y) ⋅ [bin_mismatch (ρ x) (ρ y)] = bin_lcp x y ⋅ [bin_mismatch x y]"
  proof (rule ruler_eq_len[OF _ bin_fst_mismatch], unfold prim_roots_lcp[symmetric])
    show " r.bin_code_lcp ⋅ [r.bin_code_mismatch_fst] ≤p x ⋅ r.bin_code_lcp"
      by (subst (3) pop_primroot[of x], unfold rassoc, rule r.bin_fst_mismatch_all_hull, blast)
  qed force
  then show ?thesis
  unfolding bin_lcp_eq_primroots[OF assms] cancel by blast
qed

lemmas bin_mismatch_snd_eq_primroots[bin_code_primroots] = bin_mismatch_fst_eq_primroots[OF not_sym] and
       bin_mismatch_suf_fst_eq_primroots[bin_code_primroots] = bin_mismatch_fst_eq_primroots[reversed] and
       bin_mismatch_suf_snd_primroots[bin_code_primroots] = bin_mismatch_fst_eq_primroots[reversed, OF not_sym]

lemma bin_lcp_eq_primroots' [bin_code_primroots]: "x ⋅ y ≠ y ⋅ x ⟹ ρ x ⋅ ρ y ∧⇩_p ρ y ⋅ ρ x = x ⋅ y ∧⇩_p y ⋅ x"
  using bin_lcp_eq_primroots unfolding bin_lcp_def.

lemmas no_comm_bin_code = binary_code.bin_code[unfolded binary_code_def]

theorem bin_code_code[intro]: assumes "u ⋅ v ≠ v ⋅ u" shows "code {u, v}"
  unfolding code_def using no_comm_bin_code[OF assms] by blast

lemma code_bin_code: "u ≠ v ⟹ code {u,v} ⟹ u ⋅ v ≠ v ⋅ u"
  using code.code_comm_eq[of "{u,v}" u v] by blast

lemma lcp_roots_lcp: "x ⋅ y ≠ y ⋅ x ⟹ x ⋅ y ∧⇩_p y ⋅ x = ρ x ⋅ ρ y ∧⇩_p ρ y ⋅ ρ x"
  using binary_code.prim_roots_lcp[unfolded binary_code_def bin_lcp_def, symmetric].

lemma sing_gen_primroot [simp]: "u ∈ ⟨{ρ u}⟩"
  unfolding sing_gen_pow_conv by simp

lemma sing_gen_pref_cancel [elim]: " u ⋅ v ∈ ⟨{r}⟩ ⟹  u ∈ ⟨{r}⟩ ⟹ v ∈ ⟨{r}⟩"
  using exp_pref_cancel[of _ r v] unfolding sing_gen_pow_ex_conv by blast

lemma sing_gen_suf_cancel [elim]: " u ⋅ v ∈ ⟨{r}⟩ ⟹  v ∈ ⟨{r}⟩ ⟹ u ∈ ⟨{r}⟩"
  using exp_suf_cancel[of u _ r] unfolding sing_gen_pow_ex_conv by blast

lemma prim_comm_root[elim]: assumes "primitive r" and "u ⋅ r = r ⋅ u" shows "u ∈ ⟨{r}⟩"
  using ‹u⋅r = r⋅u›[unfolded comm] prim_exp_eq[OF ‹primitive r›] pow_sing_gen  by metis

lemma prim_root_drop_exp[elim]: assumes "u⇧^@k ∈ ⟨{r}⟩" and "0 < k" and  "primitive r"
  shows "u ∈ ⟨{r}⟩"
  using pow_list_comm_comm[of k u _ r, OF ‹0 < k›, THEN prim_comm_root[OF ‹primitive r›]]
    ‹u⇧^@k ∈ ⟨{r}⟩› sing_gen_power by blast

lemma per_root_trans[intro]: assumes "w <p u ⋅ w" and "u ∈ ⟨{t}⟩" shows "w <p t ⋅ w"
   by (rule  sing_genE[OF ‹u ∈ ⟨{t}⟩› per_root_drop_exp]) (use ‹w <p u ⋅ w› in blast)

lemma per_root_trans'[intro]: "w ≤p u ⋅ w ⟹ u ∈ ⟨{r}⟩ ⟹ u ≠ ε ⟹ w ≤p r ⋅ w"
  using per_root_trans sprefD1 per_rootI by metis

lemmas per_root_trans_suf'[intro] = per_root_trans'[reversed]

lemma per_root_pref: "w ≠ ε ⟹ w ∈ ⟨{r}⟩ ⟹ r ≤p w"
  by (rule hull.cases) blast+

lemmas per_root_suf = per_root_pref[reversed]

lemma comm_primrootE: assumes  "x ⋅ y = y ⋅ x"
  obtains t where "x ∈ ⟨{t}⟩" and "y ∈ ⟨{t}⟩" and "primitive t"
  using comm_primroots assms prim_sing  primroot_prim
   emp_in sing_gen_primroot by metis

lemma root_trans[trans]: "⟦v ∈ ⟨{u}⟩; u ∈⟨{t}⟩⟧ ⟹ v ∈ ⟨{t}⟩"
  by (metis sing_gen_pow_ex_conv pow_mult)


lemma root_rev_iff[reversal_rule]: "((rev u) ∈ ⟨{rev t}⟩) ⟷ (u ∈ ⟨{t}⟩)"
  unfolding sing_gen_pow_ex_conv rev_pow[symmetric] by blast

section ‹Two words hull (not necessarily a code)›

lemma bin_lists_len_count: assumes "x ≠ y" and "ws ∈ lists {x,y}" shows
  "count_list ws x + count_list ws y = ❙|ws❙|"
proof-
  have "finite {x,y}" by simp
  have "set ws ⊆ {x,y}" using ‹ws ∈ lists{x,y}› by blast
  show ?thesis
    using sum_count_set[OF ‹set ws ⊆ {x,y}› ‹finite {x,y}›] ‹x ≠ y› by simp
qed

lemma two_elem_first_block: assumes "w ∈ ⟨{u,v}⟩"
  obtains m where "u⇧^@m ⋅ v ≤p w ∨ w = u⇧^@m"
  using assms
proof (induction rule: hull.induct)
  case (prod_cl w1 w2)
  show ?case
  proof (rule two_elem_cases[OF ‹w1 ∈ {u,v}›])
    assume "w1 = u"
    from  prod_cl.IH[OF prod_cl.prems, of Suc, unfolded this pow_Suc]
    show thesis
      by simp
  next
    assume "w1 = v"
    from  prod_cl.IH[OF prod_cl.prems, of "λ _.0", unfolded pow_zero this]
    show thesis
      by simp
  qed
qed force

lemmas two_elem_last_block = two_elem_first_block[reversed]

lemma two_elem_pref: assumes  "v ≤p u ⋅ p" and "p ∈ ⟨{u,v}⟩"
  shows "v ≤p u ⋅ v"
proof (rule two_elem_first_block[OF ‹p ∈ ⟨{u,v}⟩›], erule disjE)
  show "v ≤p u ⋅ v" if "u ⇧^@ m ⋅ v ≤p p" for m
  proof-
    have "u⇧^@(Suc m) ⋅ v ≤p u ⋅ p"
     unfolding pow_Suc rassoc  pref_cancel_conv by fact
  from ruler_le[OF ‹v ≤p u ⋅ p› this]
  have "v ≤p u ⇧^@ Suc m ⋅ v"
    unfolding lenmorph by linarith
  from per_drop_exp[OF zero_less_Suc this]
  show "v ≤p u ⋅ v".
   qed
  show "v ≤p u ⋅ v" if "p = u ⇧^@ m" for m
    using ‹v ≤p u ⋅ p›[unfolded that, folded pow_Suc]
    by (rule pref_pow_root)
qed

lemmas two_elem_suf = two_elem_pref[reversed]

lemma gen_drop_exp: assumes "p ∈ ⟨{u,v⇧^@(Suc k)}⟩" shows "p ∈ ⟨{u,v}⟩"
  by (rule hull.induct[OF assms], simp, blast)

lemma gen_drop_exp_pos: assumes "p ∈ ⟨{u,v⇧^@k}⟩" "0 < k" shows "p ∈ ⟨{u,v}⟩"
  using gen_drop_exp[of _ _ "k-1", unfolded Suc_minus_pos[OF ‹0 < k›], OF ‹p ∈ ⟨{u,v⇧^@k}⟩›].

lemma gen_prim: "p ∈ ⟨{u,v}⟩ ⟹ p ∈ ⟨{u,ρ v}⟩"
  using gen_drop_exp_pos primroot_expE by metis

lemma roots_hull: assumes "w ∈ ⟨{u⇧^@k,v⇧^@m}⟩" shows "w ∈ ⟨{u,v}⟩"
proof-
  have "u⇧^@k ∈ ⟨{u,v}⟩" and "v⇧^@m ∈ ⟨{u,v}⟩"
    by (simp_all add: gen_in power_in)
  hence "{u⇧^@k,v⇧^@m} ⊆ ⟨{u,v}⟩"
    by blast
  from hull_mono'[OF this]
  show "w ∈ ⟨{u,v}⟩"
    using ‹w ∈ ⟨{u⇧^@k,v⇧^@m}⟩› by blast
qed

lemma in_hull_primroots: "w ∈ ⟨{x, y}⟩ ⟹ w ∈ ⟨{ρ x, ρ y}⟩"
  using roots_hull[of w "e⇩_ρ x" "ρ x"  "e⇩_ρ y" "ρ y"] unfolding primroot_exp_eq.

lemma roots_hull_sub: "⟨{u⇧^@k,v⇧^@m}⟩ ⊆ ⟨{u,v}⟩"
  by (rule subsetI; rule roots_hull)

lemma primroot_gen[simp,intro]: "v ∈ ⟨{u, ρ v}⟩"
  using power_in[of "ρ v" "{u,ρ v}"]
  by (cases "v = ε", simp) (metis primroot_expE gen_in insert_iff)

lemma primroot_gen'[simp, intro]: "u ∈ ⟨{ρ u, v}⟩"
  using primroot_gen insert_commute by metis

lemma lists_lists_gen_primroots [intro]: "u ∈ lists {x, y} ⟹ u ∈ lists ⟨{ρ x, ρ y}⟩"
  using lists_mono[OF genset_sub] by fast

lemma dec_primroot_bin_sing [intro]: assumes "a ∈ {x,y}" "x ⋅ y ≠ y ⋅ x"
  shows "Dec {ρ x, ρ y} a = [ρ a]⇧^@e⇩_ρ a"
  using assms by (auto intro: binary_code.primroot_dec[OF binary_code.intro[OF ‹x ⋅ y ≠ y ⋅ x›]])

lemma ref_primroot_bin_sing: assumes "a ∈ {x,y}" "x ⋅ y ≠ y ⋅ x"
  shows "Ref {ρ x, ρ y} [a] = [ρ a]⇧^@e⇩_ρ a"
  by (rule code.code_unique_ref[of "{ρ x, ρ y}" "[a]", unfolded dec_primroot_bin_sing[OF assms] concat_simps])
  (use assms in blast, use assms in force)

lemma lists_sub_mono_gen: "ws ∈ lists S ⟹ S ⊆ ⟨G⟩ ⟹ ws ∈ lists ⟨G⟩"
  using sub_lists_mono.

subsection ‹Binary Mismatch tools›

definition bin_mismatch_hard :: "'a list ⇒ 'a list ⇒ 'a list  ⇒ bool" where
  "bin_mismatch_hard x y w ≡ ∃ k. ρ x ⋅ (ρ x)⇧^@k ⋅ ρ y ≤p w"

lemma bin_mismatch_hard_def':  assumes "x ⋅ y ≠ y ⋅ x" "bin_mismatch_hard x y w"
  shows "bin_lcp x y ⋅ [bin_mismatch x y] ≤p w"
proof-
  from ‹x ⋅ y ≠ y ⋅ x›
  interpret binary_code "ρ x" "ρ y"
    by unfold_locales blast
  find_theorems "bin_lcp ?x ?y ⋅ [bin_mismatch ?x ?y]"
  from bin_lcp_fst_pow_pref[OF zero_less_Suc, of _ ε, unfolded emp_simps] ‹bin_mismatch_hard x y w›[unfolded bin_mismatch_hard_def lassoc pow_Suc[symmetric]]
  show ?thesis
    unfolding bin_code_primroots[OF ‹x ⋅ y ≠ y ⋅ x›] using pref_trans by blast
qed

definition bin_mismatch_pref :: "'a list ⇒ 'a list ⇒ 'a list  ⇒ bool" where
  "bin_mismatch_pref x y w ≡ ∃ k.  ρ x⇧^@k ⋅ ρ y ≤p w"

lemma bm_pref_letter:  assumes "x ⋅ y ≠ y ⋅ x" and "bin_mismatch_pref x y (w ⋅ ρ y)"
  shows "bin_lcp x y ⋅ [bin_mismatch x y] ≤p x ⋅ w ⋅ bin_lcp x y" (is "?α ⋅ [?c] ≤p x ⋅ w ⋅ ?α")
proof-
  from binary_code.code_bin_roots[OF binary_code.intro, OF ‹x ⋅ y ≠ y ⋅ x›]
  interpret binary_code "ρ x" "ρ y".
  write bin_code_lcp ("α") and bin_code_mismatch_fst ("c⇩_x") and bin_code_mismatch_snd ("c⇩_y")
  have "x ≠ ε"
    using ‹x ⋅ y ≠ y ⋅ x› by blast
  from exE[OF assms(2)[unfolded bin_mismatch_pref_def]]
  obtain k where pref_x: "ρ x ⇧^@ (e⇩_ρ x + k) ⋅ ρ y ≤p x ⋅ w ⋅ ρ y"
    unfolding pow_add primroot_exp_eq rassoc pref_cancel_conv.
  have mismatch_x: "α ⋅ [c⇩_x] ≤p ρ x ⇧^@ (e⇩_ρ x + k) ⋅ ρ y"
    using bin_lcp_fst_pow_pref[of "e⇩_ρ x + k" ε, unfolded emp_simps]
    ‹x ≠ ε›[folded primroot_exp_zero_conv] by blast
  have "α ⋅ [c⇩_x] ≤p x ⋅ w ⋅ α"
    by (rule ruler_le[OF pref_trans[OF mismatch_x pref_ext[OF pref_x, unfolded rassoc]]],
       unfold pref_cancel_conv, rule bin_lcp_pref')
    (unfold pref_cancel_conv lenmorph sing_len, use nemp_len[OF ‹x ≠ ε›] in linarith)
  then show ?thesis
    unfolding bin_code_primroots[OF ‹x ⋅ y ≠ y ⋅ x›].
qed

― ‹Binary mismatch elims›
named_theorems bm_elims

lemma bm_eq1 [bm_elims]: assumes "x ⋅ w1 = y ⋅ w2" and  "bin_mismatch_pref x y (w1 ⋅ ρ y)" and "bin_mismatch_pref y x (w2 ⋅ ρ x)"
  shows "x ⋅ y = y ⋅ x"
proof(rule nemp_comm, rule ccontr)
  assume a: "x ⋅ y ≠ y ⋅ x"
  from binary_code.code_bin_roots[OF binary_code.intro, OF ‹x ⋅ y ≠ y ⋅ x›]
  interpret binary_code "ρ x" "ρ y".
  from bm_pref_letter[OF a assms(2), unfolded lassoc  ‹x ⋅ w1 = y ⋅ w2›]
    bm_pref_letter[OF a[symmetric] assms(3), unfolded lassoc]
  show False
    unfolding bin_lcp_sym[of y x] bin_code_primroots[OF a, symmetric]
    using  same_sing_pref bin_mismatch_neq by fast
qed

lemma bm_eq2 [bm_elims]: assumes "ρ x ⋅ w1 = y ⋅ w2" and  "bin_mismatch_pref x y (w1 ⋅ ρ y)" and "bin_mismatch_pref y x (w2 ⋅ ρ x)"
  shows "x ⋅ y = y ⋅ x"
  using bm_eq1[OF ‹ρ x ⋅ w1 = y ⋅ w2›] assms(2-3) unfolding bin_mismatch_pref_def primroot_idemp
  comm_primroot_conv[of "ρ x" y] using comm_primroot_conv'[of x y, symmetric] by argo

lemma bm_eq3 [bm_elims]: assumes "x ⋅ w1 = ρ y ⋅ w2" and  "bin_mismatch_pref x y (w1 ⋅  ρ y)" and "bin_mismatch_pref y x (w2 ⋅ ρ x)"
  shows "x ⋅ y = y ⋅ x"
  using bm_eq1[OF ‹x ⋅ w1 = ρ y ⋅ w2›] assms(2-3) unfolding bin_mismatch_pref_def primroot_idemp
  comm_primroot_conv[of "ρ x" y] using comm_primroot_conv[of x y, symmetric] by blast

lemma bm_eq4 [bm_elims]: assumes "ρ x ⋅ w1 = ρ y ⋅ w2" and  "bin_mismatch_pref x y (w1 ⋅ ρ y) " and "bin_mismatch_pref y x (w2 ⋅ ρ x)"
  shows "x ⋅ y = y ⋅ x"
  using bm_eq3[OF ‹ρ x ⋅ w1 = ρ y ⋅ w2›, symmetric] assms(2-3) unfolding bin_mismatch_pref_def primroot_idemp comm_primroot_conv'[of x y, symmetric] using comm_primroot_conv[of y x] by presburger

lemma bm_hard_lcp [bm_elims]: assumes "x ⋅ y ≠ y ⋅ x" and "bin_mismatch_hard x y w1" and "bin_mismatch_hard y x w2"
  shows "w1 ∧⇩_p w2 = x ⋅ y ∧⇩_p y ⋅ x"
proof-
  interpret binary_code "ρ x" "ρ y"
    using ‹x ⋅ y ≠ y ⋅ x› by unfold_locales blast
  show ?thesis
    using  bin_mismatch_hard_def'[OF assms(1-2)] bin_mismatch_hard_def'[OF assms(1)[symmetric] assms(3)]
    unfolding bin_code_primroots[OF assms(1), symmetric] bin_lcp_def[symmetric] bin_lcp_sym[of y]
    prefix_def rassoc bin_mismatch_hard_def
    using lcp_first_mismatch[OF bin_mismatch_neq] by blast
qed

lemma bin_mismatch_pref_ext: "bin_mismatch_pref x y w1 ⟹ bin_mismatch_pref x y (w1 ⋅ z)"
  unfolding bin_mismatch_pref_def using pref_ext by blast

lemma bm_pref1 [bm_elims]: assumes "x ⋅ w1 ≤p y ⋅ w2" and  "bin_mismatch_pref x y w1"
  and "bin_mismatch_pref  y x (w2 ⋅ ρ x)"
shows "x ⋅ y = y ⋅ x"
  using bm_eq1[OF lq_pref[OF ‹x ⋅ w1 ≤p y ⋅ w2›, unfolded rassoc]]
  bin_mismatch_pref_ext[OF assms(2)]  assms(3) unfolding rassoc  by presburger

lemma bm_pref2 [bm_elims]: assumes "ρ x ⋅ w1 ≤p  y ⋅ w2" and "bin_mismatch_pref x y w1"
  and "bin_mismatch_pref y x (w2 ⋅ ρ x)"
shows "x ⋅ y = y ⋅ x"
  using bm_eq2[OF lq_pref[OF ‹ρ x ⋅ w1 ≤p y ⋅ w2›, unfolded rassoc]] bin_mismatch_pref_ext[OF assms(2)]
  assms(3) unfolding rassoc  by presburger

lemma bm_pref3 [bm_elims]: assumes "x ⋅ w1 ≤p  ρ y ⋅ w2" and "bin_mismatch_pref x y w1"
  and "bin_mismatch_pref y x (w2 ⋅ ρ x)"
shows "x ⋅ y = y ⋅ x"
  using bm_eq3[OF lq_pref[OF ‹x ⋅ w1 ≤p ρ y ⋅ w2›, unfolded rassoc]] bin_mismatch_pref_ext[OF assms(2)]
    assms(3) unfolding rassoc  by presburger

lemma bm_pref4 [bm_elims]: assumes "ρ x ⋅ w1 ≤p  ρ y ⋅ w2" and "bin_mismatch_pref x y w1"
  and "bin_mismatch_pref y x (w2 ⋅ ρ x)"
shows "x ⋅ y = y ⋅ x"
  using bm_eq4[OF lq_pref[OF ‹ρ x ⋅ w1 ≤p ρ y ⋅ w2›, unfolded rassoc]] bin_mismatch_pref_ext[OF assms(2)]  assms(3) unfolding rassoc by presburger

lemmas [bm_elims] = bm_elims[symmetric]

― ‹Binary mismatch predicate evaluation›

named_theorems bm_simps
lemma bm_mismatch_rhoI1 [bm_simps]: assumes "bin_mismatch_pref x y w" shows  "bin_mismatch_hard x y (ρ x ⋅ w)"
  using assms  unfolding bin_mismatch_pref_def bin_mismatch_hard_def
  by blast

lemma bm_mismatchI1 [bm_simps]: assumes "bin_mismatch_pref x y w" shows  "bin_mismatch_hard x y (x ⋅ w)"
proof-
  from assms[unfolded bin_mismatch_pref_def]
  obtain k where "ρ x ⇧^@ k ⋅ ρ y ≤p w"
    by blast
  have "ρ x ⋅ ρ x ⇧^@ (e⇩_ρ x - 1 + k) ⋅ ρ y ≤p x ⋅ w"
    by (subst (4) pop_primroot[of x], unfold pow_add rassoc pref_cancel_conv) fact
  then show ?thesis
    unfolding bin_mismatch_hard_def by blast
qed

lemma bm_mismatch_rhoI2' [bm_simps]: assumes "bin_mismatch_pref x y w" shows  "bin_mismatch_pref x y (ρ x⇧^@k ⋅ w)"
 unfolding bin_mismatch_pref_def
proof (rule exE[OF assms[unfolded bin_mismatch_pref_def]])
  fix m
  assume "ρ x ⇧^@ m ⋅ ρ y ≤p w"
  show "∃ka. ρ x ⇧^@ ka ⋅ ρ y ≤p ρ x ⇧^@ k ⋅ w"
    by (rule exI[of _ "k+m"], unfold pow_add rassoc pref_cancel_conv) fact
qed

lemma bm_mismatch_rhoI2 [bm_simps]: assumes "bin_mismatch_pref x y w" shows  "bin_mismatch_pref x y (ρ x ⋅ w)"
  using bm_mismatch_rhoI2'[OF assms, of 1, unfolded pow_list_1].

lemma bm_mismatchI2 [bm_simps]: assumes "bin_mismatch_pref x y w" shows  "bin_mismatch_pref x y (x ⋅ w)"
  using bm_mismatch_rhoI2'[OF assms, of "e⇩_ρ x", unfolded primroot_exp_eq].

lemma bm_mismatchI2' [bm_simps]: assumes "bin_mismatch_pref x y w" shows  "bin_mismatch_pref x y (x⇧^@k ⋅ w)"
  using bm_mismatch_rhoI2'[OF assms, of "e⇩_ρ x * k", unfolded pow_mult primroot_exp_eq].

lemma [bm_simps]: " bin_mismatch_pref x y (y ⋅ v)"
  unfolding bin_mismatch_pref_def using append_Nil[of "ρ y", folded pow_zero[of "ρ  x"]]
   pref_ext[OF primroot_pref[of y]] by metis

lemma [bm_simps]: " bin_mismatch_pref x y y"
  unfolding bin_mismatch_pref_def using  append_Nil[of "ρ y", folded pow_zero[of "ρ  x"]] primroot_pref[of y] by metis

lemma [bm_simps]:  assumes  "w1 ∈ ⟨{x,y}⟩" "bin_mismatch_pref x y w"
  shows "bin_mismatch_pref x y (w1 ⋅ w)"
proof-
  obtain k where "ρ x⇧^@k ⋅ ρ y ≤p w "
    using ‹bin_mismatch_pref x y w›[unfolded bin_mismatch_pref_def] by blast
  obtain m where or: "x ⇧^@ m ⋅ y ≤p w1 ∨ w1 = x ⇧^@ m"
    using two_elem_first_block[OF ‹w1 ∈ ⟨{x,y}⟩›] by blast
  show "bin_mismatch_pref x y (w1 ⋅ w)"
    unfolding bin_mismatch_pref_def
  proof (rule disjE[OF or])
    assume "x ⇧^@ m ⋅ y ≤p w1"
    from pref_shorten[OF primroot_pref this]
    have "ρ x⇧^@(e⇩_ρ x * m) ⋅ ρ  y ≤p w1"
      unfolding pow_mult primroot_exp_eq.
    from pref_ext[OF this]
    show "∃k. ρ x ⇧^@ k ⋅ ρ y ≤p w1 ⋅ w"
      by blast
  next
    assume "w1 = x ⇧^@ m"
    have "ρ x⇧^@(e⇩_ρ x * m + k) ⋅ ρ y ≤p w1 ⋅ w"
      unfolding pow_add pow_mult primroot_exp_eq ‹w1 = x ⇧^@ m› pref_cancel_conv
      using ‹ρ x⇧^@k ⋅ ρ y ≤p w› by fastforce
    then show "∃k. ρ x ⇧^@ k ⋅ ρ y ≤p w1 ⋅ w"
      by blast
  qed
qed

lemma bm_pref_triv_rho [bm_simps]: "bin_mismatch_pref x y (ρ y ⋅ w)"
  unfolding bin_mismatch_pref_def using  append_Nil[of "ρ y",folded pow_zero[of "ρ x"]] by blast

lemma bm_pref_fst_rho [bm_simps]: "bin_mismatch_pref x y (ρ y)"
  unfolding bin_mismatch_pref_def using  append_Nil[of "ρ y",folded pow_zero[of "ρ x"]] self_pref[of "ρ y"] by metis

― ‹Binary hull membership evaluation›

lemma[bm_simps]: "x ∈ ⟨{x,y}⟩"
  by blast
lemma[bm_simps]: "y ∈ ⟨{x,y}⟩"
  by blast
lemma[bm_simps]: "w ∈ ⟨{x,y}⟩ ⟷ w ∈ ⟨{y,x}⟩"
  by (simp add: insert_commute)

lemmas[bm_simps] = hull_closed power_in
lemmas [bm_simps] = lcp_ext_left

― ‹the method setup›

method mismatch0 =
  (insert method_facts, use nothing in
    ‹(
      ((simp  only: shifts bm_simps)?,
      (elim bm_elims);(simp_all only: shifts bm_simps))
      )›
  )

lemmas bm_simps_rev =  bm_simps[reversed]
lemmas bm_elims_rev = bm_elims[reversed]

method mismatch_rev =
  (insert method_facts, use nothing in
    ‹(
      ((simp  only: shifts_rev bm_simps_rev)?,
      (elim bm_elims_rev);(simp_all only: shifts_rev bm_simps_rev))
      )›
  )

method mismatch =
  (insert method_facts, use nothing in
    ‹(mismatch0;fail|mismatch_rev)›
  )

find_theorems name: bm_elims "?x ∧⇩_p ?y"

subsubsection "Mismatch method demonstrations"

― ‹equalitites›

lemma assumes "x ⋅ y ⋅ z = y ⋅ y ⋅ x ⋅ v" shows "x ⋅ y = y ⋅ x"
  using assms by mismatch

lemma assumes "y ⋅ x ⋅ x ⋅ y ⋅ z = (y ⋅ x ⋅ y) ⋅ y ⋅ x ⋅ v" shows "x ⋅ y = y ⋅ x" ― ‹cancel›
  using assms by mismatch

lemma "y ⋅ y ⋅ x ⋅ v = x ⋅ x ⋅ y ⋅ z ⟹ x ⋅ y = y ⋅ x" ― ‹swap›
  by mismatch

lemma "ρ x ⋅ ρ x⇧^@k ⋅ y = y ⋅ w ⋅ ρ x ⟹ w ∈ ⟨{x,y}⟩ ⟹ x ⋅ y = y ⋅ x" ― ‹primitive root and hull›
  by mismatch

lemma "(r ⋅ q) ⋅ (r ⋅ q) ⇧^@ t ⋅ r ⋅ (q ⋅ r ⋅ r ⋅ q) ⇧^@ k = ((r ⋅ q) ⇧^@ t ⋅ r ⋅ (q ⋅ r ⋅ r ⋅ q) ⇧^@ k) ⋅ r ⋅ q ⟹
    0 < k ⟹ r ⋅ q = q ⋅ r" ― ‹power›
  by mismatch

lemma "((u ⋅ v) ⇧^@ m ⋅ u) ⋅ v ⋅ (u ⋅ v) ⇧^@ k =  (v ⋅ (u ⋅ v) ⇧^@ k) ⋅ (u ⋅ v) ⇧^@ m ⋅ u ⟹ u ⋅ v = v ⋅ u"
  by mismatch

lemma "w1 ∈ ⟨{x,y}⟩ ⟹ y ⋅ x ⋅ w2 ⋅ z = x ⋅ w1 ⟹ x ⋅ y = y ⋅ x"
  by mismatch

lemma "x ⋅ y ⋅ u ⋅ x ⋅ y = y ⋅ v ⋅ y ⋅ x ⟹ x ⋅ y = y ⋅ x" ― ‹reverse mismatch›
  apply mismatch_rev.

lemma "z ⋅ x ⋅ y ⋅ x ⋅ x  = v ⋅ x ⋅ y ⋅ y ⟹ y ⋅ x = x ⋅ y" ― ‹reverse mismatch›
  by mismatch

lemma "k ≠ 0 ⟹ j ≠ 0 ⟹ (x ⇧^@ j ⋅ y ⇧^@ k) ⋅ y = y⇧^@k ⋅ x ⇧^@ j ⋅ y ⇧^@ (k - 1) ⟹ x ⋅ y = y ⋅ x"
  by mismatch


― ‹prefixes›
lemma "ρ x ⋅ ρ x⇧^@k ⋅ y ≤p y ⋅ w ⋅ ρ x ⟹ w ∈ ⟨{x,y}⟩ ⟹ x ⋅ y = y ⋅ x"
  by mismatch

lemma "y ⋅ x ≤p x⇧^@k ⋅ x ⋅ y ⋅ w ⟹ x ⋅ y = y ⋅ x"
  by mismatch

lemma "0 < k ⟹ y ⋅ x ≤p x⇧^@k ⋅ y ⋅ w ⟹ x ⋅ y = y ⋅ x"
  by mismatch

lemma "0 < k ⟹ 0 < l ⟹ y⇧^@l ⋅ x ≤p x⇧^@k ⋅ y ⋅ w ⟹ x ⋅ y = y ⋅ x"
  by mismatch

lemma "0 < k ⟹ 1 < l ⟹ y⇧^@l ⋅ x ≤p y ⋅ x⇧^@k ⋅ y ⋅ w ⟹ x ⋅ y = y ⋅ x"
  by mismatch

lemma "0 < k ⟹ m < l ⟹ y⇧^@l ⋅ x ≤p y⇧^@m ⋅ x⇧^@k ⋅ y ⋅ w ⟹ x ⋅ y = y ⋅ x"
  by mismatch

lemma assumes "0 < k" "m < l" "y⇧^@l ⋅ x ≤p y⇧^@m ⋅ x⇧^@k ⋅ y ⋅ w" shows "x ⋅ y = y ⋅ x"
  using assms  by mismatch

lemma "w1 ∈ ⟨{x,y}⟩ ⟹ w2 ∈ ⟨{x,y}⟩ ⟹ x ⋅ w2 ⋅ y ⋅ z = y ⋅ w1 ⋅ x ⋅ v ⟹ x ⋅ y = y ⋅ x"
  by mismatch

― ‹suffixes›

lemma assumes "x ⋅ x ⋅ y ⋅ y ⋅ y ⋅ y ≤s z⋅ y ⋅ y ⋅ x ⋅ x" shows "x ⋅ y = y ⋅ x"
  using assms by mismatch

lemma  "u ⋅ v ⇧^@ k ⋅ v ≤s v ⋅ w ⋅ u ⟹ w ∈ ⟨{u, v}⟩ ⟹ u ⋅ v = v ⋅ u"
  by mismatch

lemma  "u ⋅ ρ v ⇧^@ k ⋅ ρ v ≤s ρ v ⋅ w ⋅ u ⟹ w ∈ ⟨{u, v}⟩ ⟹ u ⋅ v = v ⋅ u"
  by mismatch

lemma  "u ⋅ v ⇧^@ k ⋅ ρ v ≤s ρ v ⋅ w ⋅ u ⟹ w ∈ ⟨{u, v}⟩ ⟹ u ⋅ v = v ⋅ u"
  by mismatch

lemma "2 ≤ j ⟹ q ⋅ p ⋅ q ≤s (q ⋅ p) ⇧^@ et' ⋅ q ⇧^@ j ⟹ p ⋅ q = q ⋅ p"
  by mismatch

lemma "w1 ∈ ⟨{x,y}⟩ ⟹ w2 ∈ ⟨{x,y}⟩ ⟹ x ⋅ y ⋅ w2 ⋅ x ≤s x ⋅ w1 ⋅ y ⟹ x ⋅ y = y ⋅ x"
  by mismatch

lemma "w ∈ ⟨{x,y}⟩ ⟹ w' ∈ ⟨{x,y}⟩ ⟹ bin_mismatch_pref x  y (w ⋅ w ⋅ y)"
  by (simp add: bm_simps)

― ‹Known issue: In he next example, the method fails because the assumption simplifies the goal;
   on the other hand, avoiding simplification would fail to use the positivity of ‹k››
lemma "x ⋅ y = y⇧^@k ⟹ 0 < k ⟹ x ⋅ y = y ⋅ x"
      oops

― ‹least common prefix›

lemma assumes "x ⋅ y ≠ y ⋅ x"
  shows "x ⋅ x ⋅ y ∧⇩_p y ⋅ y ⋅ x = (x ⋅ y ∧⇩_p y ⋅ x)"
  using assms by mismatch

lemma assumes "x ⋅ y ≠ y ⋅ x"
  shows "w ⋅ z ⋅ x ⋅ x ⋅ y ∧⇩_p w ⋅ z ⋅ y ⋅ y ⋅ x = (w ⋅ z) ⋅ (x ⋅ y ∧⇩_p y ⋅ x)"
  using assms by mismatch

lemma assumes "x ⋅ y ≠ y ⋅ x"
  shows "y ⋅ y ⋅ x ∧⇩_p x ⋅ x ⋅ y = (x ⋅ y ∧⇩_p y ⋅ x)"
  using assms[symmetric] unfolding lcp_sym[of "x ⋅ y"] ― ‹lcp mismatch is order sensitive›
  by mismatch

― ‹least common suffix›

lemma assumes "x ⋅ y ≠ y ⋅ x"
  shows "x ⋅ x ⋅ y ∧⇩_s y ⋅ y ⋅ x = (x ⋅ y ∧⇩_s y ⋅ x)"
  using assms  by mismatch

lemma assumes "x ⋅ y ≠ y ⋅ x"
  shows "x ⋅ x ⋅ y ⋅ z ⋅ y ∧⇩_s y ⋅ y ⋅ x ⋅ z ⋅ y = (x ⋅ y ∧⇩_s y ⋅ x) ⋅ (z ⋅ y)"
  using assms by mismatch

subsection ‹Applied mismatch›

 ― ‹An alternative proof of @{thm pow_list_comm_comm}. Note the artificial introduction of the "mismatch"›
lemma assumes "x⇧^@j = y⇧^@k" "0 < j" shows "x ⋅ y = y ⋅ x"
  using arg_cong[OF assms(1), of "λ z. z ⋅ y"] ‹0 < j›
  by mismatch

lemma pows_comm_comm:  assumes  "u⇧^@k ⋅ v⇧^@m = u⇧^@l ⋅ v⇧^@n" "k ≠ l" shows "u ⋅ v = v ⋅ u"
proof-
  have aux: "u⇧^@k ⋅ v⇧^@m ⋅ v ⋅ u = u⇧^@l ⋅ v⇧^@n ⋅ v ⋅ u ⟹ k ≠ l ⟹ u ⋅ v = v ⋅ u"
  proof (induct k l rule: diff_induct) qed (mismatch, mismatch, fastforce)
  ― ‹the third goal has nothing to do with mismatch,
  therefore trying to make mismatch+ succeed is misleading›
  from this[unfolded lassoc cancel_right, OF assms]
  show "u ⋅ v = v ⋅ u".
qed

― ‹The following is needed in binary interpretations›
lemma sq_not_pref_mesosome_cover: assumes eq:  "x ⋅ x ⋅ concat ws = p ⋅ x ⋅ y⇧^@k ⋅ x ⋅ s"  and "ws ∈ lists {x,y}" "p <p x" "p ≠ ε" ‹1 < k›
  shows "x ⋅ y = y  ⋅ x"
proof-
  define z where "z = (p ⋅ x) ¯⇧^> (x ⋅ x)"
  have "p ⋅ x <p x ⋅ x"
    by (rule ruler_less[of _ ‹x ⋅ x ⋅ concat ws›], simp add: eq, simp_all add: spref_len[OF ‹p <p x›])
  from mid_sq_primroot[OF this, folded z_def]
  have "(ρ x)⇧^@e⇩_ρ z  ⋅ concat ws = y⇧^@k ⋅ x ⋅ s"
    using eq unfolding lassoc ‹x ⋅ x = p ⋅ x ⋅ ρ x ⇧^@ e⇩_ρ z›  unfolding rassoc cancel by blast
  thus "x ⋅ y = y  ⋅ x"
    using concat_in_hull'[OF ‹ws ∈ lists {x,y}›]
    unfolding pow_pos[OF ‹0 < e⇩_ρ z›] pop_pow_2[OF ‹1 < k›, symmetric] rassoc
    by mismatch
qed

lemma (in binary_code) bin_mismatch_pows: "u⇩₀⇧^@Suc k ⋅ u⇩₁ ⋅ z ≠ u⇩₁⇧^@Suc l ⋅ u⇩₀ ⋅ z'"
proof
  assume "u⇩₀ ⇧^@ Suc k ⋅ u⇩₁ ⋅ z = u⇩₁ ⇧^@ Suc l ⋅ u⇩₀ ⋅ z'"
  then have "u⇩₀ ⋅ u⇩₁ = u⇩₁ ⋅ u⇩₀"
    by mismatch
  then show False
    using non_comm by contradiction
qed

section ‹Free hull›

text‹While not every set $G$ of generators is a code, there is a unique minimal
 free monoid containing it, called the \emph{free hull} of $G$.
It can be defined inductively using the property known as the \emph{stability condition}.
›

inductive_set free_hull :: "'a list set ⇒ 'a list set" ("⟨_⟩⇩_F")
  for G where
    "ε ∈ ⟨G⟩⇩_F"
  | free_gen_in: "w ∈ G ⟹ w ∈ ⟨G⟩⇩_F"
  | "w1 ∈ ⟨G⟩⇩_F ⟹ w2 ∈ ⟨G⟩⇩_F ⟹ w1 ⋅ w2 ∈ ⟨G⟩⇩_F"
  | stability: "p ∈ ⟨G⟩⇩_F ⟹ q ∈ ⟨G⟩⇩_F ⟹ p ⋅ w ∈ ⟨G⟩⇩_F ⟹ w ⋅ q ∈ ⟨G⟩⇩_F ⟹ w ∈ ⟨G⟩⇩_F" ― ‹the stability condition›

lemmas [intro] = free_hull.intros

text‹The defined set indeed is a hull.›

lemma free_hull_hull[simp]: "⟨⟨G⟩⇩_F⟩ = ⟨G⟩⇩_F"
  by (intro antisym subsetI, rule hull.induct) blast+

text‹The free hull is always (non-strictly) larger than the hull.›

lemma hull_sub_free_hull: "⟨G⟩ ⊆ ⟨G⟩⇩_F"
proof
  fix x assume "x ∈ ⟨G⟩"
  then show "x ∈ ⟨G⟩⇩_F"
    using free_hull.intros(3)
      gen_monoid_induct[of x G "λ x. x ∈ ⟨G⟩⇩_F", OF ‹x ∈ ⟨G⟩› free_hull.intros(1)[of G] free_hull.intros(2)]
    by auto
qed

text‹On the other hand, it can be proved that the \emph{free basis}, defined as the basis of the free hull,  has a (non-strictly) smaller cardinality than the ordinary basis. (See the AFP theory Combinatorics-Words-Graph-Lemma.Graph-Lemma)›

definition free_basis ::  "'a list set ⇒ 'a list set" ("𝔅⇩_F _" [54] 55)
  where  "free_basis G ≡ 𝔅 ⟨G⟩⇩_F"

lemma basis_gen_hull_free: "⟨𝔅⇩_F G⟩ = ⟨G⟩⇩_F"
  unfolding free_basis_def  basis_gen_hull free_hull_hull..

lemma genset_sub_free: "G ⊆ ⟨G⟩⇩_F"
  by (simp add: free_hull.free_gen_in subsetI)

text
  ‹We have developed two points of view on freeness:
▪ inductive point of view: to satisfy the stability condition;
▪ being generated by a code.
›

text‹We now show their equivalence›

text‹First, basis of a free hull is a code.›

lemma free_basis_code[simp]: "code (𝔅⇩_F G)"
proof (rule code.intro)
  fix xs ys
  show "xs ∈ lists (𝔅⇩_F G) ⟹ ys ∈ lists (𝔅⇩_F G) ⟹ concat xs = concat ys ⟹ xs = ys"
  proof(induction xs ys rule: list_induct2')
    case (2 x xs)
    have "x = ε"
      using ‹concat (x # xs) = concat ε› by force
    have "x ∈ 𝔅 ⟨G⟩⇩_F"
      using  ‹x # xs ∈ lists (𝔅⇩_F G)› unfolding free_basis_def by force
    from emp_not_basis[OF this]
    have "x ≠ ε".
    then show ?case
      using ‹x = ε› by contradiction
  next
    case (3 y ys)
    have "y = ε"
      using ‹concat ε = concat (y # ys)› by force
    have "y ∈ 𝔅 ⟨G⟩⇩_F"
      using  ‹y # ys ∈ lists (𝔅⇩_F G)› unfolding free_basis_def by force
    from emp_not_basis[OF this]
    have "y ≠ ε".
    then show ?case
      using ‹y = ε› by contradiction
  next
    case (4 x xs y ys)
    show ?case
    proof (unfold list.inject, rule conjI)
      have in_free_hull:  "x ∈ ⟨G⟩⇩_F" "y ∈ ⟨G⟩⇩_F" "concat xs ∈ ⟨G⟩⇩_F" "concat ys ∈ ⟨G⟩⇩_F" and
           simple: "x ∈U ⟨G⟩⇩_F" "y ∈U ⟨G⟩⇩_F" and
           in_hull: "x ∈ ⟨⟨G⟩⇩_F⟩" "y ∈ ⟨⟨G⟩⇩_F⟩" and
           nemp: "x ≠ ε" "y ≠ ε"
        using ‹x # xs ∈ lists (𝔅⇩_F G)› ‹y # ys ∈ lists (𝔅⇩_F G)› free_basis_def
        emp_not_basis unfolding basis_def basis_gen_hull_free[symmetric] by auto
      have "x ⋅ concat xs = y ⋅ concat ys"
        using ‹concat (x # xs) = concat (y # ys)› by simp
      from eqd_or[OF this]
       obtain t where or: "x ⋅ t = y ∧ t ⋅ concat ys = concat xs ∨ y ⋅ t = x ∧ t ⋅ concat xs = concat ys"
        by blast
      have "t ∈ ⟨G⟩⇩_F"
        by (rule disjE[OF or])
        (use stability[of x G "concat ys" t] stability[of y G "concat xs" t] in_free_hull
        in fastforce)+
      hence "t = ε"
        using or simple free_hull_hull in_hull nemp ungen_dec_triv by metis
      thus "x = y"
        using or by blast
      then show "xs = ys"
      using "4.IH" ‹x # xs ∈ lists (𝔅⇩_F G)› ‹y # ys ∈ lists (𝔅⇩_F G)› ‹concat (x # xs) = concat (y # ys)›
      by auto
  qed
qed simp
qed

lemma gen_in_free_hull: "x ∈ G ⟹ x ∈ ⟨𝔅⇩_F G⟩"
  using free_hull.free_gen_in[folded basis_gen_hull_free].

text‹Second, a code generates its free hull.›

lemma (in code) code_gen_free_hull: "⟨𝒞⟩⇩_F = ⟨𝒞⟩"
proof
  show "⟨𝒞⟩ ⊆ ⟨𝒞⟩⇩_F"
    using hull_mono[of 𝒞 "⟨𝒞⟩⇩_F"] free_gen_in[of _ 𝒞]  subsetI[of 𝒞 "⟨𝒞⟩⇩_F"]
    unfolding free_hull_hull by fast
  show "⟨𝒞⟩⇩_F ⊆ ⟨𝒞⟩"
  proof
    fix x assume "x ∈ ⟨𝒞⟩⇩_F"
    thm emp_in
    show "x ∈ ⟨𝒞⟩"
    proof(rule free_hull.induct[OF ‹x ∈ ⟨𝒞⟩⇩_F›])
      show "w ∈ ⟨𝒞⟩" if elems: "p ∈ ⟨𝒞⟩" "q ∈ ⟨𝒞⟩" "p ⋅ w ∈ ⟨𝒞⟩" "w ⋅ q ∈ ⟨𝒞⟩" for p q w
      proof-
        have eq: "(Dec 𝒞 p) ⋅ (Dec 𝒞 w ⋅ q) = (Dec 𝒞 p ⋅ w) ⋅ (Dec 𝒞 q)"
          using code_dec_morph[OF ‹p ∈ ⟨𝒞⟩› ‹w ⋅ q ∈ ⟨𝒞⟩›, unfolded lassoc]
          unfolding code_dec_morph[OF ‹p ⋅ w ∈ ⟨𝒞⟩› ‹q ∈ ⟨𝒞⟩›, symmetric].
        from eqd_or[OF this]
        obtain ts where or': "(Dec 𝒞 p) ⋅ ts = Dec 𝒞 p ⋅ w ∨ (Dec 𝒞 p ⋅ w) ⋅ ts = Dec 𝒞 p "
          by blast
        hence "concat ((Dec 𝒞 p) ⋅ ts)  = concat (Dec 𝒞 p ⋅ w) ∨
              concat((Dec 𝒞 p ⋅ w) ⋅ ts) = concat (Dec 𝒞 p)"
          by presburger
        hence "concat ts = w"
          unfolding concat_dec[OF ‹p ⋅ w ∈ ⟨𝒞⟩›] concat_dec[OF ‹p ∈ ⟨𝒞⟩›] concat_morph
          rassoc by blast
        have "ts ∈ lists 𝒞"
          using dec_in_lists[OF ‹p ⋅ w ∈ ⟨𝒞⟩›] dec_in_lists[OF ‹p ∈ ⟨𝒞⟩›]
          or' append_in_lists_conv[of _ ts 𝒞] by metis
        thus "w ∈ ⟨𝒞⟩"
          using ‹concat ts = w› by blast
      qed
    qed (simp_all add: ‹x ∈ ⟨𝒞⟩⇩_F› hull_closed gen_in)
  qed
qed


text‹That is, a code is its own free basis›

lemma (in code) code_free_basis: "𝒞 = 𝔅⇩_F 𝒞"
  using basis_of_hull[of 𝒞, unfolded code_gen_free_hull[symmetric]
      code_is_basis, symmetric] unfolding free_basis_def.

text‹This allows to use the introduction rules of the free hull to prove one of the basic characterizations
 of the code, called the stability condition›

lemma (in code) stability: "p ∈ ⟨𝒞⟩ ⟹ q ∈ ⟨𝒞⟩ ⟹ p ⋅ w ∈ ⟨𝒞⟩ ⟹ w ⋅ q ∈ ⟨𝒞⟩ ⟹ w ∈ ⟨𝒞⟩"
  unfolding code_gen_free_hull[symmetric] using free_hull.intros(4) by auto

text‹Moreover, the free hull of G is the smallest code-generated hull containing G.
In other words, the term free hull is appropriate.›



text‹First, several intuitive monotonicity and closure results.›

lemma free_hull_mono: assumes "G ⊆ H" shows "⟨G⟩⇩_F ⊆ ⟨H⟩⇩_F"
proof
  fix x assume "x ∈ ⟨G⟩⇩_F"
  have el: "⋀ w. w ∈ G ⟹ w ∈ ⟨H⟩⇩_F"
    using ‹G ⊆ H› free_hull.free_gen_in by auto
  show "x ∈ ⟨H⟩⇩_F"
    by (rule free_hull.induct[of x G]) (auto simp add: ‹x ∈ ⟨G⟩⇩_F› el)
qed

lemma free_hull_idem: "⟨⟨G⟩⇩_F⟩⇩_F = ⟨G⟩⇩_F"
proof
  show "⟨⟨G⟩⇩_F⟩⇩_F ⊆ ⟨G⟩⇩_F"
  proof
    fix x assume "x ∈ ⟨⟨G⟩⇩_F⟩⇩_F"
    show "x ∈ ⟨G⟩⇩_F"
    proof (rule free_hull.induct[of x "⟨G⟩⇩_F"])
      show "⋀p q w. p ∈ ⟨G⟩⇩_F ⟹  q ∈ ⟨G⟩⇩_F ⟹  p ⋅ w ∈ ⟨G⟩⇩_F ⟹  w ⋅ q ∈ ⟨G⟩⇩_F ⟹ w ∈ ⟨G⟩⇩_F"
        using free_hull.intros(4) by auto
    qed (simp_all add: ‹x ∈ ⟨⟨G⟩⇩_F⟩⇩_F› free_hull.intros(1), simp add: free_hull.intros(2), simp add: free_hull.intros(3))
  qed
next
  show "⟨G⟩⇩_F ⊆ ⟨⟨G⟩⇩_F⟩⇩_F"
    using free_hull_hull hull_sub_free_hull by auto
qed

lemma hull_gen_free_hull: "⟨⟨G⟩⟩⇩_F = ⟨G⟩⇩_F"
proof
  show " ⟨⟨G⟩⟩⇩_F ⊆ ⟨G⟩⇩_F"
    using free_hull_idem free_hull_mono hull_sub_free_hull by metis
next
  show "⟨G⟩⇩_F ⊆ ⟨⟨G⟩⟩⇩_F"
    by (simp add: free_hull_mono)
qed

text ‹Code is also the free basis of its hull.›

lemma (in code) code_free_basis_hull: "𝒞 = 𝔅⇩_F ⟨𝒞⟩"
  unfolding free_basis_def using code_free_basis[unfolded free_basis_def]
  unfolding  hull_gen_free_hull.

text‹The minimality of the free hull easily follows.›

theorem (in code) free_hull_min: assumes "G ⊆ ⟨𝒞⟩" shows "⟨G⟩⇩_F ⊆ ⟨𝒞⟩"
  using free_hull_mono[OF ‹G ⊆ ⟨𝒞⟩›] unfolding hull_gen_free_hull
  unfolding code_gen_free_hull.

theorem free_hull_inter: "⟨G⟩⇩_F = ⋂ {M. G ⊆ M ∧ M = ⟨M⟩⇩_F}"
proof
  have "X ∈ {M. G ⊆ M ∧ M = ⟨M⟩⇩_F} ⟹ ⟨G⟩⇩_F ⊆ X" for X
    unfolding mem_Collect_eq[of _ "λ M. G ⊆ M ∧ M = ⟨M⟩⇩_F"]
    using free_hull_mono[of G X] by simp
  from Inter_greatest[of "{M. G ⊆ M ∧ M = ⟨M⟩⇩_F}", OF this]
  show "⟨G⟩⇩_F ⊆ ⋂ {M. G ⊆ M ∧ M = ⟨M⟩⇩_F}"
    by blast
next
  show " ⋂ {M. G ⊆ M ∧ M = ⟨M⟩⇩_F} ⊆ ⟨G⟩⇩_F"
    by (simp add: Inter_lower free_hull_idem genset_sub_free)
qed

text‹Decomposition into the free basis is a morphism.›

lemma free_basis_dec_morph: "u ∈ ⟨G⟩⇩_F ⟹ v ∈ ⟨G⟩⇩_F ⟹
    Dec (𝔅⇩_F G) (u ⋅ v) = (Dec (𝔅⇩_F G) u) ⋅ (Dec (𝔅⇩_F G) v)"
  using code.code_dec_morph[OF free_basis_code, of u G v, symmetric,
      unfolded  basis_gen_hull_free[of G]].

section ‹Reversing hulls and decompositions›

lemma basis_rev_commute[reversal_rule]: "𝔅 (rev ` G) = rev ` (𝔅 G)"
proof
  have "⟨rev ` 𝔅 G⟩ = ⟨rev ` G⟩" and *: "⟨rev ` 𝔅 (rev ` G)⟩ = ⟨rev ` rev `G⟩"
    unfolding rev_hull[symmetric] basis_gen_hull by blast+
  from gen_basis_sub[OF this(1)]
  show "𝔅 (rev ` G) ⊆ rev ` 𝔅 G".
  from image_mono[OF gen_basis_sub[OF *], of rev]
  show "rev ` (𝔅 G) ⊆ 𝔅 (rev ` G)"
    unfolding rev_rev_image_eq.
qed

lemma rev_free_hull_comm: "⟨rev ` X⟩⇩_F = rev ` ⟨X⟩⇩_F"
proof-
  have "rev ` ⟨X⟩⇩_F ⊆ ⟨rev ` X⟩⇩_F" for X :: "'a list set"
  proof
    fix x assume "x ∈ rev ` ⟨X⟩⇩_F"
    hence  "rev x ∈ ⟨X⟩⇩_F"
      by (simp add: rev_in_conv)
    have "rev x ∈ rev ` ⟨rev ` X⟩⇩_F"
      by (induct rule: free_hull.induct[OF ‹rev x ∈ ⟨X⟩⇩_F›])
        (auto simp add: rev_in_conv[symmetric])
    then show "x ∈ ⟨rev ` X⟩⇩_F"
      by blast
  qed
  from this
    image_mono[OF this[of "rev ` X", unfolded rev_rev_image_eq], of rev, unfolded rev_rev_image_eq]
  show  "⟨rev ` X⟩⇩_F = rev ` ⟨X⟩⇩_F"
    by blast
qed

lemma free_basis_rev_commute [reversal_rule]: "𝔅⇩_F rev ` X =  rev ` (𝔅⇩_F X)"
  unfolding free_basis_def basis_rev_commute free_basis_def rev_free_hull_comm..

lemma rev_dec[reversal_rule]: assumes "x ∈ ⟨X⟩⇩_F" shows "Dec rev ` (𝔅⇩_F X) (rev x) = map rev (rev (Dec (𝔅⇩_F X) x))"
proof-
  have "x ∈ ⟨𝔅⇩_F X⟩"
    using ‹x ∈ ⟨X⟩⇩_F› by (simp add: basis_gen_hull_free)
  from concat_dec[OF this]
  have "concat (map rev (rev (Dec 𝔅⇩_F X x))) = rev x"
    unfolding rev_concat[symmetric] by blast
  from  rev_image_eqI[OF rev_in_lists[OF dec_in_lists[OF ‹x ∈ ⟨𝔅⇩_F X⟩›]], of _ "map rev"]
  have "map rev (rev (Dec 𝔅⇩_F X x)) ∈ lists (rev ` (𝔅⇩_F X))"
    unfolding lists_image by blast
  from code.code_unique_dec'[OF code.code_rev_code[OF free_basis_code] this]
  show ?thesis
    unfolding ‹concat (map rev (rev (Dec 𝔅⇩_F X x))) = rev x›.
qed

lemma rev_hd_dec_last_eq[reversal_rule]: assumes "x ∈ X" and  "x ≠ ε" shows
  "rev (hd (Dec (rev ` (𝔅⇩_F X)) (rev x))) = last (Dec 𝔅⇩_F X x)"
proof-
  have "rev (Dec 𝔅⇩_F X x) ≠ ε"
    using ‹x ∈ X› basis_gen_hull_free dec_nemp'[OF ‹x ≠ ε›] by blast
  show ?thesis
    unfolding hd_rev rev_dec[OF free_gen_in[OF ‹x ∈ X›]] hd_map[OF ‹rev (Dec 𝔅⇩_F X x) ≠ ε›]
    by simp
qed

lemma rev_hd_dec_last_eq'[reversal_rule]: assumes "x ∈ X" and  "x ≠ ε" shows
  "(hd (Dec (rev ` (𝔅⇩_F X)) (rev x))) = rev (last (Dec 𝔅⇩_F X x))"
  using assms(1) assms(2) rev_hd_dec_last_eq rev_swap by blast

section ‹Lists as the free hull of singletons›

text‹A crucial property of free monoids of words is that they can be seen as lists over the free basis,
instead as lists over the original alphabet.›

abbreviation sings where "sings B ≡ {[b] | b. b ∈ B}"

term "Set.filter P A"

lemma sings_image: "sings B =  (λ x. [x]) ` B"
  using Setcompr_eq_image.

lemma lists_sing_map_concat_ident: "xs ∈ lists (sings B) ⟹ xs = map (λ x. [x]) (concat xs)"
  by (induct xs, simp, auto)

lemma code_sings: "code (sings B)"
proof
  fix xs ys assume xs: "xs ∈ lists (sings B)" and ys: "ys ∈ lists (sings B)"
    and eq: "concat xs = concat ys"
  from lists_sing_map_concat_ident[OF xs, unfolded eq]
  show "xs = ys" unfolding  lists_sing_map_concat_ident[OF ys, symmetric].
qed

lemma sings_gen_lists: "⟨sings B⟩ = lists B"
  unfolding hull_concat_lists
proof(intro equalityI subsetI, standard)
  fix xs
  show "xs ∈ concat ` lists (sings B) ⟹ ∀x∈set xs. x ∈ B"
    by force
  assume "xs ∈ lists B"
  hence "map (λx. x # ε) xs ∈ lists (sings B)"
    by force
  from imageI[OF this, of concat]
  show "xs ∈ concat ` lists (sings B)"
    unfolding concat_map_sing_ident[of xs].
qed

lemma sing_gen_lists: "lists {x} = ⟨{[x]}⟩"
  using sings_gen_lists[of "{x}"] by simp

lemma bin_gen_lists: "lists {x, y} = ⟨{[x],[y]}⟩"
  using sings_gen_lists[of "{x,y}"] unfolding Setcompr_eq_image by simp

lemma "sings B = 𝔅⇩_F (lists B)"
  using code.code_free_basis_hull[OF code_sings, of B, unfolded sings_gen_lists].

lemma map_sings: "xs ∈ lists B ⟹ map (λx. x # ε) xs ∈ lists (sings B)"
  by (induct xs) auto

lemma dec_sings: "xs ∈ lists B ⟹ Dec (sings B) xs = map (λ x. [x]) xs"
  using code.code_unique_dec'[OF code_sings, of "map (λ x. [x]) xs" B, OF map_sings]
  unfolding concat_map_sing_ident.

lemma sing_lists_exp: assumes "ws ∈ lists {a}"
  obtains k where "ws = [a]⇧^@k"
  using  sing_set_wordE[OF assms[folded in_lists_conv_set_subset]].

lemma sing_lists_exp_len: "ws ∈ lists {a} ⟷ [a]⇧^@❙|ws❙| = ws"
  by  (induct ws, auto)

lemma sing_lists_exp_count: "ws ∈ lists {a} ⟷ [a]⇧^@(count_list ws a) = ws"
  by  (standard, induct ws, force, simp)
  (use sing_pow_lists[OF singletonI, of "count_list ws a" a] in argo)

lemma sing_set_pow_count_list: "set ws ⊆ {a} ⟷ [a]⇧^@(count_list ws a) = ws"
  unfolding in_lists_conv_set_subset using  sing_lists_exp_count.

lemma count_le_length_iff: "set ws ⊆ {a} ⟷ count_list ws a = ❙|ws❙|"
proof
  show "set ws ⊆ {a} ⟹ count_list ws a = ❙|ws❙|"
  unfolding sing_set_pow_count_list using
  lenarg[of "[a] ⇧^@ count_list ws a" ws, unfolded pow_len sing_len] by force
next
  assume "count_list ws a = ❙|ws❙|"
  then show "set ws ⊆ {a}"
  proof (induct ws, force)
    case (Cons b ws)
    have "b = a"
      using Cons.prems count_le_length[of ws a] impossible_Cons[of "b#ws"]
      unfolding count_list.simps(2) by metis
    have "count_list ws a = ❙|ws❙|"
      using Cons.prems unfolding ‹b = a› by force
    from Cons.hyps[OF this]
    show "set (b # ws) ⊆ {a}"
      unfolding ‹b = a› by simp
  qed
qed

lemma sing_set_pow: "set ws ⊆ {a} ⟷ [a]⇧^@❙|ws❙| = ws"
  using sing_lists_exp_len[unfolded sing_lists_exp_count]
  using sing_set_pow_count_list[unfolded count_le_length_iff]
  unfolding count_le_length_iff  by fast

lemma count_sing_exp[simp]: "count_list ([a]⇧^@k) a = k"
  by (induct k, simp_all)

lemma count_sing_exp'[simp]: "count_list ([a]) a = 1"
  by simp

lemma count_sing_distinct[simp]: "a ≠ b ⟹ count_list ([a]⇧^@k) b = 0"
  by (induct k, simp, auto)

lemma count_sing_distinct'[simp]: "a ≠ b ⟹ count_list ([a]) b = 0"
  by simp

lemma sing_letter_imp_prim: assumes "count_list w a = 1" shows "primitive w"
proof
  fix r k
  assume "r ⇧^@ k = w"
  have "count_list w a = k * count_list r a"
    by (simp only: count_list_pow_list flip: ‹r ⇧^@ k = w›)
  then show "k = 1"
    unfolding ‹count_list w a = 1› by simp
qed

lemma prim_abk: "a ≠ b ⟹ primitive ([a] ⋅ [b] ⇧^@ k)"
  by (intro sing_letter_imp_prim[of _ a]) simp

lemma sing_code: "x ≠ ε ⟹ code {x}"
proof (rule code.intro)
  fix xs ys
  assume "x ≠ ε" "xs ∈ lists {x}" "ys ∈ lists {x}" "concat xs = concat ys"
  from ‹xs ∈ lists {x}›[unfolded sing_lists_exp_len, symmetric]
       ‹ys ∈ lists {x}›[unfolded sing_lists_exp_len, symmetric]
  have "❙|xs❙| = ❙|ys❙|"
    using ‹concat xs = concat ys› concat_pow_list_single eq_pow_exp[OF ‹x ≠ ε›] by metis
  then show "xs = ys"
    using ‹xs = [x] ⇧^@ ❙|xs❙|› ‹ys = [x] ⇧^@ ❙|ys❙|› by argo
qed

lemma sings_card: "card A = card (sings A)"
  by(rule bij_betw_same_card, rule bij_betwI'[of _ "λx. [x]"], auto)

lemma sings_finite: "finite A = finite (sings A)"
  by(rule bij_betw_finite, rule bij_betwI'[of _ "λx. [x]"], auto)

lemma sings_conv: "A = B ⟷ sings A = sings B"
proof(standard, simp)
  have "⋀x A B. sings A = sings B ⟹ x ∈ A ⟹ x ∈ B"
  proof-
    fix x :: "'b" and A B
    assume "sings A = sings B" "x ∈ A"
    hence "[x] ∈ sings B"
      using ‹sings A = sings B› by blast
    thus "x ∈ B"
      by blast
  qed
  from this[of A B] this[of B A, OF sym]
  show "sings A = sings B ⟹ A = B"
    by blast
qed

section ‹Various additional lemmas›

subsection ‹Roots of binary set›

lemma two_roots_code: assumes "x ≠ ε" and  "y ≠ ε" shows "code {ρ x, ρ y}"
  using assms
proof (cases "ρ x = ρ y")
  assume "ρ x = ρ y"
  thus "code {ρ x, ρ y}" using sing_code[OF primroot_nemp[OF ‹x ≠ ε›]] by simp
next
  assume "ρ x ≠ ρ y"
  hence "ρ x ⋅ ρ y ≠ ρ y ⋅ ρ x"
    using comm_prim[OF primroot_prim[OF ‹x ≠ ε›] primroot_prim[OF ‹y ≠ ε›]] by blast
  thus "code {ρ x, ρ y}"
    by (simp add: bin_code_code)
qed

lemma primroot_in_set_dec: assumes "x ≠ ε" and  "y ≠ ε" shows "ρ x ∈ set (Dec {ρ x, ρ y} x)"
proof-
  obtain k where "concat ([ρ x]⇧^@k) = x" "0 < k"
    using primroot_expE
      concat_pow_list_single[symmetric, of _ "ρ x"] by metis
  from code.code_unique_dec'[OF two_roots_code[OF assms], of "[ρ x]⇧^@k", unfolded ‹concat ([ρ x]⇧^@k) = x›]
  have "Dec {ρ x, ρ y} x = [ρ x]⇧^@k"
    using insertI1 sing_pow_lists by metis
  show ?thesis
    unfolding ‹Dec {ρ x, ρ y} x = [ρ x]⇧^@k› using ‹0 < k› by simp
qed

lemma primroot_dec: assumes "x ⋅ y ≠ y ⋅ x"
  shows "(Dec {ρ x, ρ y} x) = [ρ x]⇧^@e⇩_ρ x" "(Dec {ρ x, ρ y} y) = [ρ y]⇧^@e⇩_ρ y"
  by (simp_all add: binary_code.intro[OF assms] binary_code.primroot_dec)


subsection Other

lemma bin_count_one_decompose: assumes "ws ∈ lists {x,y}" and "x ≠ y" and  "count_list ws y = 1"
  obtains k m where "[x]⇧^@k ⋅ [y] ⋅ [x]⇧^@m = ws"
proof-
  have "¬ set ws ⊆ {x}"
    using count_sing_distinct[OF ‹x ≠ y›] ‹count_list ws y = 1› by auto
  from distinct_letter_in[OF this]
  obtain ws' k  b where "[x]⇧^@k ⋅ [b] ⋅ ws' = ws" and "b ≠ x" by blast
  hence "b = y"
    using ‹ws ∈ lists {x,y}›  by force
  have "ws' ∈ lists {x,y}"
    using ‹ws ∈ lists {x,y}›[folded ‹[x]⇧^@k ⋅ [b] ⋅ ws' = ws›] by simp
  have "count_list ws' y = 0"
    using arg_cong[OF ‹[x]⇧^@k ⋅ [b] ⋅ ws' = ws›, of "λ x. count_list x y"]
    unfolding count_list_append ‹count_list ws y = 1› ‹b = y›  by force
     hence "set ws' ⊆ {x}"
     unfolding count_list_0_iff using  ‹ws' ∈ lists {x,y}› by blast
  then obtain m where "ws' = [x]⇧^@m"
     by blast
  from that[OF ‹[x]⇧^@k ⋅ [b] ⋅ ws' = ws›[unfolded this ‹b = y›]]
  show thesis.
qed

lemma bin_count_one_conjug: assumes "ws ∈ lists {x,y}" and "x ≠ y" and "count_list ws y = 1"
  shows "ws ∼ [x]⇧^@(count_list ws x) ⋅ [y]"
proof-
  obtain e1 e2 where "[x]⇧^@e1 ⋅ [y] ⋅ [x]⇧^@e2 = ws"
    using bin_count_one_decompose[OF assms].
  from conjugI'[of "[x] ⇧^@ e1 ⋅ [y]" "[x]⇧^@e2", unfolded rassoc this]
  have "ws ∼ [x]⇧^@(e2 + e1) ⋅ [y]"
    unfolding pow_add rassoc.
  moreover have "count_list ([x]⇧^@(e2 + e1) ⋅ [y]) x = e2 + e1"
    using ‹x ≠ y› by simp
  ultimately show ?thesis
    by (simp add: count_list_conjug)
qed

lemma bin_prim_long_set: assumes "ws ∈ lists {x,y}" and "primitive ws" and  "2 ≤ ❙|ws❙|"
  shows "set ws = {x,y}"
proof-
  have "¬ set ws ⊆ {c}" for c
    using ‹primitive ws› pow_nemp_imprim ‹2 ≤ ❙|ws❙|›
      sing_lists_exp_len[folded in_lists_conv_set_subset] by metis
  then show "set ws = {x,y}"
    unfolding subset_singleton_iff using ‹ws ∈ lists {x,y}›[folded in_lists_conv_set_subset] doubleton_subset_cases by metis
qed

lemma bin_prim_long_pref: assumes "ws ∈ lists {x,y}" and "primitive ws" and  "2 ≤ ❙|ws❙|"
  obtains ws' where "ws ∼ ws'" and "[x,y] ≤p ws'"
proof-
  from pow_nemp_imprim[OF ‹2 ≤ ❙|ws❙|›, of "[x]"] sing_lists_exp_len[of ws x]
  have "¬ ws ∈ lists {x}"
    using ‹primitive ws› ‹2 ≤ ❙|ws❙|› by fastforce
  hence "x ≠ y"
    using ‹ws ∈ lists {x,y}› by fastforce
  from switch_fac[OF ‹x ≠ y› bin_prim_long_set[OF assms]]
  show thesis
    using ‹2 ≤ ❙|ws❙|› rotate_into_pos_sq[of ε "[x,y]" ws thesis, unfolded emp_simps, OF ‹[x, y] ≤f ws ⋅ ws› _ _ that, of id]
    by force
qed

end