Theory Equations_Basic
theory Equations_Basic
imports
Periodicity_Lemma
Lyndon_Schutzenberger
Submonoids
Binary_Code_Morphisms
begin
chapter "Equations on words - basics"
text
‹Contains various nontrivial auxiliary or rudimentary facts related to equations. Often moderately advanced or even fairly advanced.
May change significantly in the future.›
section ‹Factor interpretation›
definition factor_interpretation :: "'a list ⇒ 'a list ⇒ 'a list ⇒ 'a list list ⇒ bool" ("_ _ _ ∼⇩ℐ _" [51,51,51,51] 60)
where "factor_interpretation p u s ws = (p <p hd ws ∧ s <s last ws ∧ p ⋅ u ⋅ s = concat ws)"
lemma fac_interp_nemp: "u ≠ ε ⟹ p u s ∼⇩ℐ ws ⟹ ws ≠ ε"
unfolding factor_interpretation_def by auto
lemma fac_interpD: assumes "p u s ∼⇩ℐ ws"
shows "p <p hd ws" and "s <s last ws" and "p ⋅ u ⋅ s = concat ws"
using assms unfolding factor_interpretation_def by blast+
lemma fac_interpI:
"p <p hd ws ⟹ s <s last ws ⟹ p ⋅ u ⋅ s = concat ws ⟹ p u s ∼⇩ℐ ws"
unfolding factor_interpretation_def by blast
lemma obtain_fac_interp: assumes "pu ⋅ u ⋅ su = concat ws" and "u ≠ ε"
obtains ps ss p s vs where "p u s ∼⇩ℐ vs" and "ps ⋅ vs ⋅ ss = ws" and "concat ps ⋅ p = pu" and
"s ⋅ concat ss = su"
using assms
proof (induction "❙|ws❙|" arbitrary: ws pu su thesis rule: less_induct)
case less
then show ?case
proof-
have "ws ≠ ε"
using ‹u ≠ ε› ‹pu ⋅ u ⋅ su = concat ws› by force
have "❙|tl ws❙| < ❙|ws❙|" and "❙|butlast ws❙| < ❙|ws❙|"
using ‹ws ≠ ε› by force+
show thesis
proof (cases)
assume "hd ws ≤p pu ∨ last ws ≤s su"
then show thesis
proof
assume "hd ws ≤p pu"
from prefixE[OF this]
obtain pu' where "pu = hd ws ⋅ pu'".
from ‹pu ⋅ u ⋅ su = concat ws›[unfolded this, folded arg_cong[OF hd_tl[OF ‹ws ≠ ε›], of concat]]
have "pu' ⋅ u ⋅ su = concat (tl ws)"
by force
from less.hyps[OF ‹❙|tl ws❙| < ❙|ws❙|› _ ‹pu' ⋅ u ⋅ su = concat (tl ws)› ‹u ≠ ε›]
obtain p s vs ps' ss where "p u s ∼⇩ℐ vs" and "ps' ⋅ vs ⋅ ss = tl ws" and "concat ps' ⋅ p = pu'"
and "s ⋅ concat ss = su".
have "(hd ws # ps') ⋅ vs ⋅ ss = ws"
using ‹ws ≠ ε› ‹ps' ⋅ vs ⋅ ss = tl ws› by auto
have "concat (hd ws # ps') ⋅ p = pu"
using ‹concat ps' ⋅ p = pu'› unfolding ‹pu = hd ws ⋅ pu'› by fastforce
from less.prems(1)[OF ‹p u s ∼⇩ℐ vs› ‹(hd ws # ps') ⋅ vs ⋅ ss = ws› ‹concat (hd ws # ps') ⋅ p = pu› ‹s ⋅ concat ss = su›]
show thesis.
next
assume "last ws ≤s su"
from suffixE[OF this]
obtain su' where "su = su' ⋅ last ws".
from ‹pu ⋅ u ⋅ su = concat ws›[unfolded this, folded arg_cong[OF hd_tl[reversed, OF ‹ws ≠ ε›], of concat]]
have "pu ⋅ u ⋅ su' = concat (butlast ws)"
by force
from less.hyps[OF ‹❙|butlast ws❙| < ❙|ws❙|› _ ‹pu ⋅ u ⋅ su' = concat (butlast ws)› ‹u ≠ ε›]
obtain p s vs ps ss' where "p u s ∼⇩ℐ vs" and "ps ⋅ vs ⋅ ss' = butlast ws" and "concat ps ⋅ p = pu" and "s ⋅ concat ss' = su'".
have "ps ⋅ vs ⋅ (ss' ⋅ [last ws]) = ws"
using append_butlast_last_id[OF ‹ws ≠ ε›, folded ‹ps ⋅ vs ⋅ ss' = butlast ws›] unfolding rassoc.
have "s ⋅ concat (ss' ⋅ [last ws]) = su"
using ‹s ⋅ concat ss' = su'› ‹su = su' ⋅ last ws› by fastforce
from less.prems(1)[OF ‹p u s ∼⇩ℐ vs› ‹ps ⋅ vs ⋅ (ss' ⋅ [last ws]) = ws› ‹concat ps ⋅ p = pu› ‹s ⋅ concat (ss' ⋅ [last ws]) = su›]
show thesis.
qed
next
assume not_or: "¬ (hd ws ≤p pu ∨ last ws ≤s su)"
hence "pu <p hd ws" and "su <s last ws"
using ruler[OF concat_hd_pref[OF ‹ws ≠ ε›] prefI'[OF ‹pu ⋅ u ⋅ su = concat ws›[symmetric]]]
ruler[reversed, OF concat_hd_pref[reversed, OF ‹ws ≠ ε›] prefI'[reversed, OF ‹pu ⋅ u ⋅ su = concat ws›[symmetric, unfolded lassoc]]] by auto
from fac_interpI[OF this ‹pu ⋅ u ⋅ su = concat ws›]
have "pu u su ∼⇩ℐ ws".
from less.prems(1)[OF this, of ε ε]
show thesis by simp
qed
qed
qed
lemma obtain_fac_interp': assumes "u ≤f concat ws" and "u ≠ ε"
obtains p s vs where "p u s ∼⇩ℐ vs" and "vs ≤f ws"
proof-
from facE[OF ‹u ≤f concat ws›]
obtain pu su where "concat ws = pu ⋅ u ⋅ su".
from obtain_fac_interp[OF this[symmetric] ‹u ≠ ε›] that
show thesis
using facI' by metis
qed
lemma fac_pow_longE: assumes "w ≤f v⇧@k" and "❙|v❙| ≤ ❙|w❙|"
obtains m v1 v2 where "v1 ≤s v" "v2 ≤p v" "w = v1 ⋅ v⇧@m ⋅ v2"
using assms
proof (cases "w = ε ∨ w = v")
assume "w = ε ∨ w = v"
then show thesis
by (rule disjE) (use that[of ε ε 0] in fastforce, use that[of ε ε 1] in auto)
next
assume "¬ (w = ε ∨ w = v)"
hence "w ≠ ε" and "w ≠ v" by blast+
have "v⇧@k = concat ([v]⇧@k)"
by auto
from obtain_fac_interp'[OF ‹w ≤f v⇧@k›[unfolded this] ‹w ≠ ε›]
obtain p vs s where "p w s ∼⇩ℐ vs" "vs ≤f [v] ⇧@ k".
note fac_interpD[OF this(1)]
obtain m where "vs = [v]⇧@m"
using ‹vs ≤f [v] ⇧@ k› unique_letter_fac_expE by meson
hence "concat vs = v⇧@m"
by simp
from lenarg[OF ‹p ⋅ w ⋅ s = concat vs›, unfolded this lenmorph pow_len]
have "0 < m"
using ‹❙|v❙| ≤ ❙|w❙|› ‹¬ (w = ε ∨ w = v)› by force
hence "hd vs = v" and "last vs = v"
using ‹vs = [v]⇧@m›
by (simp_all add: hd_pow hd_pow[reversed])
obtain v1 where "v = p ⋅ v1"
using ‹p <p hd vs› unfolding ‹hd vs = v› strict_prefix_def prefix_def by force
obtain v2 where "v = v2 ⋅ s"
using ‹s <s last vs› unfolding ‹last vs = v› strict_suffix_def suffix_def by force
have "m ≠ 1"
using ‹p ⋅ w ⋅ s = concat vs› unfolding ‹concat vs = v⇧@m›
using ‹w ≠ v› ‹❙|v❙| ≤ ❙|w❙|› by force
hence "2 ≤ m"
using ‹0 < m› by linarith
from Suc_minus2[OF this]
have "concat vs = v ⋅ v⇧@(m-2) ⋅ v"
unfolding pow_Suc'[symmetric] pow_Suc[symmetric] ‹concat vs = v⇧@m› by argo
hence "w = v1 ⋅ v⇧@(m-2) ⋅ v2"
by (subst(asm) ‹v = p ⋅ v1›, subst(asm) (2) ‹v = v2 ⋅ s›)
(simp add: ‹p ⋅ w ⋅ s = concat vs›[symmetric])
from that[OF _ _ this]
show thesis
using ‹v = p ⋅ v1› ‹v = v2 ⋅ s› by blast
qed
lemma obtain_fac_interp_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 obtain_fac_interp'[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 fac_interp_inner: assumes "u ≠ ε" and "p u s ∼⇩ℐ ws" and "1 < ❙|ws❙|"
shows "p¯⇧>(hd ws)⋅concat(butlast (tl ws))⋅(last ws)⇧<¯s = u"
proof-
have "p <p hd ws" and "s <s last ws" and "p ⋅ u ⋅ s = concat ws"
using assms[unfolded factor_interpretation_def] by blast+
have "last (tl ws) = last ws"
using last_tl long_list_tl[OF ‹1 < ❙|ws❙|›] by blast
have ws_eq: "[hd ws] ⋅ butlast (tl ws) ⋅ [last ws] = ws"
using hd_tl[OF fac_interp_nemp[OF ‹u ≠ ε› ‹p u s ∼⇩ℐ ws›]] append_butlast_last_id[OF long_list_tl[OF ‹1 < ❙|ws❙|›], unfolded ‹last (tl ws) = last ws›] by simp
from arg_cong[OF this, of concat, unfolded concat_morph, unfolded concat_sing', folded ‹p ⋅ u ⋅ s = concat ws›]
have "(hd ws)⋅concat(butlast (tl ws))⋅(last ws) = p ⋅ u ⋅ s".
thus "p¯⇧>(hd ws)⋅concat(butlast (tl ws))⋅(last ws)⇧<¯s = u"
unfolding cancel_right[of "p¯⇧>(hd ws)⋅concat (butlast (tl ws)) ⋅ last ws⇧<¯s" s u, symmetric]
unfolding rassoc rq_suf[OF ssufD1[OF ‹s <s last ws›]]
unfolding cancel[of p "p¯⇧>hd ws ⋅ concat (butlast (tl ws)) ⋅ last ws" "u⋅s", symmetric]
unfolding lassoc lq_pref[OF sprefD1[OF ‹p <p hd ws›]].
qed
lemma fac_interp_inner_len: assumes "u ≠ ε" and "p u s ∼⇩ℐ ws"
shows "❙|concat(butlast (tl ws))❙| < ❙|u❙|"
proof (cases "❙|ws❙| ≤ 1")
assume "❙|ws❙| ≤ 1"
hence "tl ws = ε"
using nemp_le_len by fastforce
thus ?thesis
using ‹u ≠ ε› by simp
next
assume neg: "¬ ❙|ws❙| ≤ 1" hence "1 < ❙|ws❙|" by auto
from lenarg[OF fac_interp_inner[OF ‹u ≠ ε› ‹p u s ∼⇩ℐ ws› this]] ‹p u s ∼⇩ℐ ws›
show ?thesis
unfolding factor_interpretation_def lenmorph
using rq_ssuf[of s "last ws", folded length_greater_0_conv]
by linarith
qed
lemma rev_in_set_map_rev_conv: "rev u ∈ set (map rev ws) ⟷ u ∈ set ws"
by auto
lemma rev_fac_interp: assumes "p u s ∼⇩ℐ ws" shows "(rev s) (rev u) (rev p) ∼⇩ℐ rev (map rev ws)"
proof (rule fac_interpI)
note fac_interpD[OF assms]
show ‹rev s <p hd (rev (map rev ws))›
using ‹s <s last ws›
by (metis ‹p <p hd ws› ‹p ⋅ u ⋅ s = concat ws› append_is_Nil_conv concat.simps(1) hd_rev last_map list.simps(8) rev_is_Nil_conv strict_suffix_to_prefix)
show "rev p <s last (rev (map rev ws))"
using ‹ p <p hd ws›
by (metis ‹p ⋅ u ⋅ s = concat ws› ‹s <s last ws› append_is_Nil_conv concat.simps(1) last_rev list.map_sel(1) list.simps(8) rev_is_Nil_conv spref_rev_suf_iff)
show "rev s ⋅ rev u ⋅ rev p = concat (rev (map rev ws))"
using ‹p ⋅ u ⋅ s = concat ws›
by (metis append_assoc rev_append rev_concat rev_map)
qed
lemma rev_fac_interp_iff [reversal_rule]: "(rev s) (rev u) (rev p) ∼⇩ℐ rev (map rev ws) ⟷ p u s ∼⇩ℐ ws"
using rev_fac_interp
by (metis (no_types, lifting) map_rev_involution rev_map rev_rev_ident)
lemma fac_interp_mid_fac: assumes "p u s ∼⇩ℐ ws"
shows "concat (butlast (tl ws)) ≤f u"
proof(rule le_cases)
assume "2 ≤ ❙|ws❙|"
note fac_interpD[OF ‹p u s ∼⇩ℐ ws›]
mid_fac_ex[OF ‹2 ≤ ❙|ws❙|›]
note ex = sprefD1[OF this(1)] sprefE[reversed, OF this(2)]
obtain p' where "hd ws = p ⋅ p'"
using ex(1) prefixE
by blast
obtain s' where "last ws = s' ⋅ s"
using ‹s <s last ws› by (blast elim: ssufE sufE)
show ?thesis
using ‹p ⋅ u ⋅ s = concat ws›
unfolding arg_cong[OF ‹ws = [hd ws] ⋅ butlast (tl ws) ⋅ [last ws]›, of concat]
unfolding concat_morph concat_sing'
unfolding ‹hd ws = p ⋅ p'› ‹last ws = s' ⋅ s›
by simp
next
assume "❙|ws❙| ≤ 2"
hence "butlast (tl ws) = ε"
using nemp_le_len by fastforce
thus ?thesis
by simp
qed
definition disjoint_interpretation :: "'a list ⇒ 'a list list ⇒ 'a list ⇒ 'a list list ⇒ bool" ("_ _ _ ∼⇩𝒟 _" [51,51,51,51] 60)
where "p us s ∼⇩𝒟 ws ≡ p (concat us) s ∼⇩ℐ ws ∧
(∀ u v. u ≤p us ∧ v ≤p ws ⟶ p ⋅ concat u ≠ concat v)"
lemma disjoint_interpI: "p (concat us) s ∼⇩ℐ ws ⟹
(∀ u v. u ≤p us ∧ v ≤p ws ⟶ p ⋅ concat u ≠ concat v) ⟹ p us s ∼⇩𝒟 ws"
unfolding disjoint_interpretation_def by blast
lemma disjoint_interpI'[intro]: "p (concat us) s ∼⇩ℐ ws ⟹
(⋀ u v. u ≤p us ⟹ v ≤p ws ⟹ p ⋅ concat u ≠ concat v) ⟹ p us s ∼⇩𝒟 ws"
unfolding disjoint_interpretation_def by blast
lemma disj_interpD: "p us s ∼⇩𝒟 ws ⟹ p (concat us) s ∼⇩ℐ ws"
unfolding disjoint_interpretation_def by blast
lemma disj_interpD1: assumes "p us s ∼⇩𝒟 ws" and "us' ≤p us" and "ws' ≤p ws"
shows "p ⋅ concat us' ≠ concat ws'"
using assms unfolding disjoint_interpretation_def by blast
lemma disj_interp_nemp: assumes "p us s ∼⇩𝒟 ws"
shows "p ≠ ε" and "s ≠ ε"
using disj_interpD1[OF assms emp_pref emp_pref]
disj_interpD1[OF assms self_pref self_pref, folded
fac_interpD(3)[OF disj_interpD, OF assms], unfolded cancel] by blast+
subsection "Factor intepretation of morphic images"
context morphism
begin
lemma image_fac_interp': assumes "w ≤f f z" "w ≠ ε"
obtains p w_pred s where "w_pred ≤f z" "p w s ∼⇩ℐ (map f⇧𝒞 w_pred)"
proof-
let ?fzs = "map f⇧𝒞 z"
have "w ≤f concat (map f⇧𝒞 z)"
by (simp add: assms(1) morph_concat_map)
from obtain_fac_interp'[OF ‹w ≤f concat (map f⇧𝒞 z)› ‹w ≠ ε›]
obtain p s ws where "p w s ∼⇩ℐ ws" "ws ≤f ?fzs"
by blast
obtain w_pred where "ws = map f⇧𝒞 w_pred" "w_pred ≤f z"
using ‹ws ≤f map f⇧𝒞 z› sublist_map_rightE by blast
show ?thesis
using ‹p w s ∼⇩ℐ ws› ‹w_pred ≤f z› ‹ws = map f⇧𝒞 w_pred› that by blast
qed
lemma image_fac_interp: assumes "u⋅w⋅v = f z" "w ≠ ε"
obtains p w_pred s u_pred v_pred where
"u_pred⋅w_pred⋅v_pred = z" "p w s ∼⇩ℐ (map f⇧𝒞 w_pred)"
"u = (f u_pred)⋅p" "v = s⋅(f v_pred)"
proof-
let ?fzs = "map f⇧𝒞 z"
have "u⋅w⋅v = concat (map f⇧𝒞 z)"
by (simp add: assms(1) morph_concat_map)
from obtain_fac_interp[OF ‹u⋅w⋅v = concat (map f⇧𝒞 z)› ‹w ≠ ε›]
obtain ps ss p s ws where "p w s ∼⇩ℐ ws" "ps⋅ws⋅ss = ?fzs" "concat ps ⋅ p = u" "s ⋅ concat ss = v"
by metis
obtain w_pred u_pred v_pred where "ws = map f⇧𝒞 w_pred" "ps = map f⇧𝒞 u_pred"
"ss = map f⇧𝒞 v_pred" "u_pred⋅w_pred⋅v_pred = z"
using ‹ps ⋅ ws ⋅ ss = map f⇧𝒞 z›[unfolded append_eq_map_conv]
by blast
show ?thesis
using ‹concat ps ⋅ p = u› ‹p w s ∼⇩ℐ ws› ‹ps = map f⇧𝒞 u_pred› ‹s ⋅ concat ss = v› ‹ss = map f⇧𝒞 v_pred› ‹u_pred ⋅ w_pred ⋅ v_pred = z› ‹ws = map f⇧𝒞 w_pred› morph_concat_map that by blast
qed
lemma image_fac_interp_mid: assumes "p w s ∼⇩ℐ map f⇧𝒞 w_pred" "2 ≤ ❙|w_pred❙|"
obtains pw sw where
"w = pw ⋅ (f (butlast (tl w_pred))) ⋅ sw" "p⋅pw = f [hd w_pred]" "sw⋅s = f [last w_pred]"
proof-
note fac_interpD[OF ‹p w s ∼⇩ℐ map f⇧𝒞 w_pred›, unfolded morph_concat_map]
note butl = mid_fac_ex[OF ‹2 ≤ ❙|w_pred❙|›]
have "w_pred ≠ ε"
using assms(2) by force
obtain pw' where
"p ⋅ pw' = hd (map f⇧𝒞 w_pred)"
using sprefE[OF ‹p <p hd (map f⇧𝒞 w_pred)›] prefixE by metis
hence pw': "p ⋅ pw' = f [hd w_pred]"
unfolding core_def
unfolding hd_map[OF ‹w_pred ≠ ε›, of "f⇧𝒞", unfolded core_def].
obtain sw' where
"sw' ⋅ s = last (map f⇧𝒞 (w_pred))"
using sprefE[reversed, OF ‹s <s last (map f⇧𝒞 w_pred)›] suffix_def by metis
hence sw' : "sw' ⋅ s = f [last (w_pred)]"
unfolding core_def
unfolding last_map[OF ‹w_pred ≠ ε›, of "f⇧𝒞", unfolded core_def].
have "w = pw' ⋅ f (butlast (tl w_pred)) ⋅ sw'"
using ‹p ⋅ w ⋅ s = f w_pred›[unfolded arg_cong[OF butl, of f]]
unfolding morph
unfolding pw'[symmetric] sw'[symmetric]
by simp
thus ?thesis
using pw' sw' that by blast
qed
end
section Miscellanea
subsection ‹Mismatch additions›
lemma mismatch_pref_comm_len: assumes "w1 ∈ ⟨{u,v}⟩" and "w2 ∈ ⟨{u,v}⟩" and "p ≤p w1"
"u ⋅ p ≤p v ⋅ w2" and "❙|v❙| ≤ ❙|p❙|"
shows "u ⋅ v = v ⋅ u"
proof (rule ccontr)
assume "u ⋅ v ≠ v ⋅ u"
then interpret binary_code u v
by unfold_locales
show False
using bin_code_prefs[OF ‹w1 ∈ ⟨{u,v}⟩› ‹p ≤p w1› ‹w2 ∈ ⟨{u,v}⟩› ‹❙|v❙| ≤ ❙|p❙|›]
‹u ⋅ p ≤p v ⋅ w2›
by blast
qed
lemma mismatch_pref_comm: assumes "w1 ∈ ⟨{u,v}⟩" and "w2 ∈ ⟨{u,v}⟩" and
"u ⋅ w1 ⋅ v ≤p v ⋅ w2 ⋅ u"
shows "u ⋅ v = v ⋅ u"
using assms by mismatch
lemma mismatch_eq_comm: assumes "w1 ∈ ⟨{u,v}⟩" and "w2 ∈ ⟨{u,v}⟩" and
"u ⋅ w1 = v ⋅ w2"
shows "u ⋅ v = v ⋅ u"
using assms by mismatch
lemmas mismatch_suf_comm = mismatch_pref_comm[reversed] and
mismatch_suf_comm_len = mismatch_pref_comm_len[reversed, unfolded rassoc]
subsection ‹Conjugate words with conjugate periods›
lemma conj_pers_conj_comm_aux:
assumes "(u ⋅ v)⇧@k ⋅ u = r ⋅ s" and "(v ⋅ u)⇧@l ⋅ v = (s ⋅ r)⇧@m" and "0 < k" "0 < l" and "2 ≤ m"
shows "u ⋅ v = v ⋅ u"
proof (rule nemp_comm)
assume "u ≠ ε" and "v ≠ ε" hence "u ⋅ v ≠ ε" and "v ⋅ u ≠ ε" by blast+
have "l ≠ 1"
proof (rule notI)
assume "l = 1"
hence "v ⋅ u ⋅ v = (s ⋅ r)⇧@m"
using assms(2) by simp
have "❙|v ⋅ u❙| + ❙|u❙| ≤ ❙|r ⋅ s❙|"
unfolding lenmorph add.commute[of "❙|u❙|"]
lenarg[OF assms(1), unfolded lenmorph pow_len, symmetric]
using ‹0 < k› by simp
hence "❙|v ⋅ u ⋅ v ⋅ u❙| ≤ 2*❙|r ⋅ s❙|"
unfolding lenmorph pow_len by simp
hence "❙|v ⋅ u ⋅ v❙| < 2*❙|r ⋅ s❙|"
unfolding lenmorph pow_len using nemp_len[OF ‹u ≠ ε›] by linarith
from this[unfolded ‹v ⋅ u ⋅ v = (s ⋅ r)⇧@m›]
show False
using mult_le_mono1[OF ‹2 ≤ m›, of "❙|r❙| + ❙|s❙|"]
unfolding lenmorph pow_len add.commute[of "❙|s❙|"] by force
qed
hence "2 ≤ l"
using ‹0 < l› by force
let ?w = "(v ⋅ u)⇧@l ⋅ v"
have per1: "?w ≤p (v ⋅ u) ⋅ ?w"
unfolding lassoc pow_comm[symmetric] by force
have per2: "?w ≤p (s ⋅ r) ⋅ ?w"
unfolding assms(2) using pref_pow_ext' by blast
have len: "❙|v ⋅ u❙| + ❙|s ⋅ r❙| ≤ ❙|?w❙|"
proof-
have len1: "2*❙|s ⋅ r❙| ≤ ❙|?w❙|"
using mult_le_mono1[OF ‹2 ≤ m›, of "❙|s❙| + ❙|r❙|"]
unfolding ‹(v ⋅ u)⇧@l ⋅ v = (s ⋅ r)⇧@m› lenmorph pow_len.
moreover have len2: "2*❙|v ⋅ u❙| ≤ ❙|?w❙|"
using mult_le_mono1[OF ‹2 ≤ l›, of "❙|v❙| + ❙|u❙|"]
unfolding lenmorph pow_len by linarith
ultimately show ?thesis
using len1 len2 by linarith
qed
from two_pers[OF per1 per2 len]
have "(v ⋅ u) ⋅ (s ⋅ r) = (s ⋅ r) ⋅ (v ⋅ u)".
hence "(v ⋅ u)⇧@l ⋅ (s ⋅ r)⇧@m = (s ⋅ r)⇧@m ⋅ (v ⋅ u)⇧@l"
using comm_add_exps by blast
from comm_drop_exp'[OF this[folded assms(2), unfolded rassoc cancel] ‹0 < l›]
show "u ⋅ v = v ⋅ u"
unfolding rassoc cancel by blast
qed
lemma conj_pers_conj_comm: assumes "ρ (v ⋅ (u ⋅ v)⇧@k) ∼ ρ ((u ⋅ v)⇧@m ⋅ u)" and "0 < k" and "0 < m"
shows "u ⋅ v = v ⋅ u"
proof (rule nemp_comm)
let ?v = "v ⋅ (u ⋅ v)⇧@k" and ?u = "(u ⋅ v)⇧@m ⋅ u"
assume "u ≠ ε" and "v ≠ ε"
hence "u ⋅ v ≠ ε" and "?v ≠ ε" and "?u ≠ ε" by simp_all
obtain r s where "r ⋅ s = ρ ?v" and "s ⋅ r = ρ ?u"
using conjugE[OF assms(1)].
then obtain k1 k2 where "?v = (r ⋅ s)⇧@k1" and "?u = (s ⋅ r)⇧@k2" and "0 < k1" and "0 < k2"
using primroot_expE[of ?u] primroot_expE[of ?v] unfolding shift_pow by metis
hence eq: "(s ⋅ r)⇧@k2 ⋅ (r ⋅ s)⇧@k1 = (u ⋅ v)⇧@(m + 1 + k)"
unfolding add_exps pow_one rassoc by simp
have ineq: "2 ≤ m + 1 + k"
using ‹0 < k› by simp
consider (two_two) "2 ≤ k1 ∧ 2 ≤ k2"|
(one_one) "k1 = 1 ∧ k2 = 1" |
(two_one) "2 ≤ k1 ∧ k2 = 1" |
(one_two) "k1 = 1 ∧ 2 ≤ k2"
using ‹0 < k1› ‹0 < k2› by linarith
then show "u ⋅ v = v ⋅ u"
proof (cases)
case (two_two)
with Lyndon_Schutzenberger(1)[OF eq _ _ ineq]
have "(s ⋅ r) ⋅ (r ⋅ s) = (r ⋅ s) ⋅ (s ⋅ r)"
using eqd_eq[of "s ⋅ r" "r ⋅ s" "r ⋅ s" "s ⋅ r"] by fastforce
from comm_add_exps[OF this, of k2 k1, folded ‹?v = (r ⋅ s)⇧@k1› ‹?u = (s ⋅ r)⇧@k2›]
show "u ⋅ v = v ⋅ u"
by mismatch
next
case (one_one)
hence "(s ⋅ r) ⇧@ k2 ⋅ (r ⋅ s) ⇧@ k1 = (s ⋅ r) ⋅ (r ⋅ s)"
using pow_one by simp
from eq[unfolded conjunct1[OF one_one] conjunct2[OF one_one] pow_1]
pow_nemp_imprim[OF ineq, folded eq[unfolded this]]
Lyndon_Schutzenberger_conjug[of "s ⋅ r" "r ⋅ s", OF conjugI']
have "(s ⋅ r) ⋅ (r ⋅ s) = (r ⋅ s) ⋅ (s ⋅ r)" by metis
from comm_add_exps[OF this, of k2 k1, folded ‹?v = (r ⋅ s)⇧@k1› ‹?u = (s ⋅ r)⇧@k2›, folded shift_pow]
show "u ⋅ v = v ⋅ u"
by mismatch
next
case (two_one)
hence "?u = s ⋅ r"
using ‹?u = (s ⋅ r)⇧@k2›
by simp
from ‹?v = (r ⋅ s)⇧@k1›[folded shift_pow, unfolded this]
have "(v ⋅ u) ⇧@ k ⋅ v = (r ⋅ s)⇧@k1".
from conj_pers_conj_comm_aux[OF ‹?u = s ⋅ r› this ‹0 < m› ‹0 < k› ]
show "u ⋅ v = v ⋅ u"
using two_one by auto
next
case (one_two)
hence "?v = r ⋅ s"
using ‹?v = (r ⋅ s)⇧@k1› by simp
from ‹?u = (s ⋅ r)⇧@k2›[unfolded this]
have "(u ⋅ v) ⇧@ m ⋅ u = (s ⋅ r) ⇧@ k2".
from conj_pers_conj_comm_aux[OF ‹?v = r ⋅ s›[folded shift_pow] this ‹0 < k› ‹0 < m›]
show "u ⋅ v = v ⋅ u"
using one_two by argo
qed
qed
hide_fact conj_pers_conj_comm_aux
subsection ‹Covering uvvu›
lemma uv_fac_uvv: assumes "p ⋅ u ⋅ v ≤p u ⋅ v ⋅ v" and "p ≠ ε" and "p ≤s w" and "w ∈ ⟨{u,v}⟩"
shows "u ⋅ v = v ⋅ u"
proof (rule nemp_comm)
assume "u ≠ ε" and "v ≠ ε"
obtain s where "u ⋅ v ⋅ v = p ⋅ u ⋅ v ⋅ s"
using ‹p ⋅ u ⋅ v ≤p u ⋅ v ⋅ v› by (auto simp add: prefix_def)
obtain p' where "u ⋅ p' = p ⋅ u" and "p' ⋅ v ⋅ s = v ⋅ v"
using eqdE[of u "v ⋅ v" "p ⋅ u" "v ⋅ s", unfolded rassoc, OF ‹u ⋅ v ⋅ v = p ⋅ u ⋅ v ⋅ s› suf_len'].
hence "p' ≠ ε"
using ‹p ≠ ε› by force
have "p' ⋅ v ⋅ s = v ⋅ v"
using ‹u ⋅ v ⋅ v = p ⋅ u ⋅ v ⋅ s› ‹u ⋅ p' = p ⋅ u› cancel rassoc by metis
from mid_sq[OF this]
have "v ⋅ p' = p' ⋅ v" by simp
from this comm_primroots[OF ‹v ≠ ε› ‹p' ≠ ε›]
have "ρ v = ρ p'"
by simp
have "w ∈ ⟨{u, ρ v}⟩"
using gen_prim[OF ‹w ∈ ⟨{u, v}⟩›].
obtain m where "p' = ρ v⇧@m" "0 < m"
using primroot_expE unfolding ‹ρ v = ρ p'› by metis
have "(u ⋅ ρ v⇧@(m-1)) ⋅ ρ v ≤s (ρ v ⋅ w) ⋅ u"
using ‹p ≤s w›
unfolding rassoc pow_pos'[OF ‹0 < m›, symmetric] ‹p' = ρ v⇧@m›[symmetric] ‹u ⋅ p' = p ⋅ u› suffix_def by force
hence "u ⋅ ρ v = ρ v ⋅ u"
using ‹w ∈ ⟨{u, ρ v}⟩› by mismatch
thus "u ⋅ v = v ⋅ u"
unfolding comm_primroot_conv[symmetric].
qed
lemmas uv_fac_uvv_suf = uv_fac_uvv[reversed, unfolded rassoc]
lemma "u ≤p v ⟹ u' ≤p v' ⟹ u ∧⇩p u' ≠ u ⟹ u ∧⇩p u' ≠ u' ⟹ u ∧⇩p u' = v ∧⇩p v'"
using lcp.absorb2 lcp.orderE lcp_rulers pref_compE by metis
lemma comm_puv_pvs_eq_uq: assumes "p ⋅ u ⋅ v = u ⋅ v ⋅ p" and "p ⋅ v ⋅ s = u ⋅ q" and
"p ≤p u" "q ≤p w" and "s ≤p w'" and
"w ∈ ⟨{u,v}⟩" and "w' ∈ ⟨{u,v}⟩" and "❙|u❙| ≤ ❙|s❙|"
shows "u ⋅ v = v ⋅ u"
proof (rule ccontr)
assume "u ⋅ v ≠ v ⋅ u"
then interpret binary_code u v
by unfold_locales
write bin_code_lcp ("α") and
bin_code_mismatch_fst ("c⇩0") and
bin_code_mismatch_snd ("c⇩1")
have "❙|α❙| < ❙|v ⋅ s❙|"
using ‹❙|u❙| ≤ ❙|s❙|› bin_lcp_short by force
show False
proof (cases)
assume "p = ε"
hence "v ⋅ s = u ⋅ q"
using ‹p ⋅ v ⋅ s = u ⋅ q› by fastforce
with ‹❙|α❙| < ❙|v ⋅ s❙|› ‹❙|α❙| < ❙|v ⋅ s❙|›[unfolded this]
have "α ⋅ [c⇩1] ≤p v ⋅ s" and "α ⋅ [c⇩0] ≤p u ⋅ q"
using ‹s ≤p w'› ‹w' ∈ ⟨{u,v}⟩› ‹q ≤p w› ‹w ∈ ⟨{u,v}⟩›
bin_lcp_mismatch_pref_all_snd bin_lcp_mismatch_pref_all_fst ‹v ⋅ s = u ⋅ q›
by blast+
thus False
unfolding ‹v ⋅ s = u ⋅ q› using bin_mismatch_neq
by (simp add: same_sing_pref)
next
assume "p ≠ ε"
show False
proof-
have "u ≠ ε" and "v ≠ ε" and "u ⋅ v ≠ v ⋅ u"
by (simp_all add: bin_fst_nemp bin_snd_nemp non_comm)
have "w ⋅ u ⋅ v ∈ ⟨{u, v}⟩"
using ‹w ∈ ⟨{u, v}⟩› by blast
have "❙|w ⋅ u ⋅ v❙| ≥ ❙|α❙|"
using bin_lcp_short by auto
have p_pref1: "p ⋅ v ⋅ s ∧⇩p p ⋅ p ⋅ v ⋅ s = p ⋅ α"
using bin_per_root_max_pref_short[of p s w', OF _ ‹s ≤p w'› ‹w' ∈ ⟨{u, v}⟩›]
‹p ≠ ε› ‹p ⋅ u ⋅ v = u ⋅ v ⋅ p› unfolding lcp_ext_left cancel take_all[OF less_imp_le[OF‹❙|α❙| <❙|v ⋅ s❙|›]] by force
have p_pref2: "u ⋅ α ≤p u ⋅ (w ⋅ u ⋅ v) ∧⇩p p ⋅ u ⋅ (w ⋅ u ⋅ v)"
using bin_root_max_pref_long[OF ‹p ⋅ u ⋅ v = u ⋅ v ⋅ p› self_pref ‹w ⋅ u ⋅ v ∈ ⟨{u, v}⟩› ‹❙|α❙| ≤ ❙|w ⋅ u ⋅ v❙| ›].
have "u ⋅ w ⋅ u ⋅ v ∧⇩p p ⋅ u ⋅ w ⋅ u ⋅ v = p ⋅ v ⋅ s ∧⇩p p ⋅ p ⋅ v ⋅ s"
proof(rule lcp_rulers')
show "¬ p ⋅ v ⋅ s ⨝ p ⋅ p ⋅ v ⋅ s"
proof (rule notI)
assume "p ⋅ v ⋅ s ⨝ p ⋅ p ⋅ v ⋅ s"
hence "p ⋅ v ⋅ s ∧⇩p p ⋅ p ⋅ v ⋅ s = p ⋅ v ⋅ s"
using ‹p ≠ ε› lcp.absorb1 pref_compE same_sufix_nil by meson
from this[unfolded p_pref1 cancel]
show False
using bin_lcp_short ‹❙|u❙| ≤ ❙|s❙|› by force
qed
show "p ⋅ v ⋅ s ≤p u ⋅ (w ⋅ u ⋅ v)" "p ⋅ p ⋅ v ⋅ s ≤p p ⋅ u ⋅ w ⋅ u ⋅ v"
by (simp_all add: assms(2) assms(4))
qed
from p_pref2[unfolded rassoc this p_pref1]
have "p = u"
using ‹p ≤p u› pref_cancel_right by force
thus False
using ‹p ⋅ u ⋅ v = u ⋅ v ⋅ p› non_comm by blast
qed
qed
qed
lemma assumes "u ⋅ v ⋅ v ⋅ u = p ⋅ u ⋅ v ⋅ u ⋅ q" and "p ≠ ε" and "q ≠ ε"
shows "u ⋅ v = v ⋅ u"
oops
lemma uvu_pref_uvv: assumes "p ⋅ u ⋅ v ⋅ v ⋅ s = u ⋅ v ⋅ u ⋅ q" and
"p ≤p u" and "q ≤p w" and "s ≤p w'" and
"w ∈ ⟨{u,v}⟩" and "w' ∈ ⟨{u,v}⟩" and "❙|u❙| ≤ ❙|s❙|"
shows "u ⋅ v = v ⋅ u"
proof(rule nemp_comm)
have "❙|p ⋅ u ⋅ v❙| ≤ ❙|u ⋅ v ⋅ u❙|"
using ‹p ≤p u› unfolding lenmorph
by (simp add: prefix_length_le)
have "p ⋅ (u ⋅ v) = (u ⋅ v) ⋅ p"
by (rule pref_marker[of "u ⋅ v ⋅ u"], force)
(rule eq_le_pref, use assms in force, fact)
have "p ⋅ v ⋅ s = u ⋅ q"
proof-
have "((u ⋅ v) ⋅ p) ⋅ v ⋅ s = (u ⋅ v) ⋅ u ⋅ q"
unfolding ‹p ⋅ u ⋅ v = (u ⋅ v) ⋅ p›[symmetric] unfolding rassoc by fact
from this[unfolded rassoc cancel]
show ?thesis.
qed
from comm_puv_pvs_eq_uq[OF ‹p ⋅ (u ⋅ v) = (u ⋅ v) ⋅ p›[unfolded rassoc] this assms(2-)]
show "u ⋅ v = v ⋅ u".
qed
lemma uvu_pref_uvvu: assumes "p ⋅ u ⋅ v ⋅ v ⋅ u = u ⋅ v ⋅ u ⋅ q" and
"p ≤p u" and "q ≤p w" and " w ∈ ⟨{u,v}⟩"
shows "u ⋅ v = v ⋅ u"
using uvu_pref_uvv[OF ‹p ⋅ u ⋅ v ⋅ v ⋅ u = u ⋅ v ⋅ u ⋅ q› ‹p ≤p u› ‹q ≤p w› _ ‹w ∈ ⟨{u,v}⟩›, of u]
by blast
lemma uvu_pref_uvvu_interp: assumes interp: "p u ⋅ v ⋅ v ⋅ u s ∼⇩ℐ ws" and
"[u, v, u] ≤p ws" and "ws ∈ lists {u,v}"
shows "u ⋅ v = v ⋅ u"
proof-
note fac_interpD[OF interp]
obtain ws' where "[u,v,u] ⋅ ws' = ws" and "ws' ∈ lists {u,v}"
using ‹[u, v, u] ≤p ws› ‹ws ∈ lists {u,v}› by (force simp add: prefix_def)
have "p ⋅ u ⋅ v ⋅ v ⋅ u ⋅ s = u ⋅ v ⋅ u ⋅ concat ws'"
using ‹p ⋅ (u ⋅ v ⋅ v ⋅ u) ⋅ s = concat ws›[folded ‹[u,v,u] ⋅ ws' = ws›, unfolded concat_morph rassoc]
by simp
from lenarg[OF this, unfolded lenmorph]
have "❙|s❙| ≤ ❙|concat ws'❙|"
by auto
hence "s ≤s concat ws'"
using eqd[reversed, OF ‹p ⋅ u ⋅ v ⋅ v ⋅ u ⋅ s = u ⋅ v ⋅ u ⋅ concat ws'›[unfolded lassoc]]
by blast
note local_rule = uvu_pref_uvv[of p u v u "concat ws'⇧<¯s" "concat ws'" u]
show "u ⋅ v = v ⋅ u"
proof (rule local_rule)
show "p ≤p u"
using ‹p <p hd ws› pref_hd_eq[OF ‹[u, v, u] ≤p ws› list.distinct(1)[of u "[v,u]", symmetric]]
by force
have "p ⋅ u ⋅ v ⋅ v ⋅ u ⋅ s = u ⋅ v ⋅ u ⋅ (concat ws'⇧<¯s) ⋅ s"
using ‹p ⋅ u ⋅ v ⋅ v ⋅ u ⋅ s = u ⋅ v ⋅ u ⋅ concat ws'› unfolding rq_suf[OF ‹s ≤s concat ws'›].
thus "p ⋅ u ⋅ v ⋅ v ⋅ u = u ⋅ v ⋅ u ⋅ concat ws'⇧<¯s"
by simp
show "concat ws' ∈ ⟨{u,v}⟩"
using ‹ws' ∈ lists {u,v}› by blast
show "concat ws'⇧<¯s ≤p concat ws'"
using rq_suf[OF ‹s ≤s concat ws'›] by fast
qed auto
qed
lemmas uvu_suf_uvvu = uvu_pref_uvvu[reversed, unfolded rassoc] and
uvu_suf_uvv = uvu_pref_uvv[reversed, unfolded rassoc]
lemma uvu_suf_uvvu_interp: "p u ⋅ v ⋅ v ⋅ u s ∼⇩ℐ ws ⟹ [u, v, u] ≤s ws
⟹ ws ∈ lists {u,v} ⟹ u ⋅ v = v ⋅ u"
by (rule uvu_pref_uvvu_interp[reversed, unfolded rassoc emp_simps, symmetric, of p u v s ws],
simp, force, simp add: image_iff rev_in_lists rev_map)
subsection ‹Conjugate words›
lemma conjug_pref_suf_mismatch: assumes "w1 ∈ ⟨{r⋅s,s⋅r}⟩" and "w2 ∈ ⟨{r⋅s,s⋅r}⟩" and "r ⋅ w1 = w2 ⋅ s"
shows "r = s ∨ r = ε ∨ s = ε"
proof (rule ccontr)
assume "¬ (r = s ∨ r = ε ∨ s = ε)"
hence "r ≠ s" and "r ≠ ε" and "s ≠ ε" by simp_all
from assms
show False
proof (induct "❙|w1❙|" arbitrary: w1 w2 rule: less_induct)
case less
have "w1 ∈ ⟨{r,s}⟩"
using ‹w1 ∈ ⟨{r⋅s,s⋅r}⟩› by force
obtain w1' where "(w1 = ε ∨ w1 = r ⋅ s ⋅ w1' ∨ w1 = s ⋅ r ⋅ w1') ∧ w1' ∈ ⟨{r⋅s,s⋅r}⟩"
using hull.cases[OF ‹w1 ∈ ⟨{r⋅s,s⋅r}⟩›] empty_iff insert_iff rassoc ‹w1 ∈ ⟨{r ⋅ s, s ⋅ r}⟩› by metis
hence "w1' ∈ ⟨{r⋅s,s⋅r}⟩" and cases1: "(w1 = ε ∨ w1 = r ⋅ s ⋅ w1' ∨ w1 = s ⋅ r ⋅ w1')" by blast+
hence "w1' ∈ ⟨{r,s}⟩" by force
obtain w2' where "(w2 = ε ∨ w2 = r ⋅ s ⋅ w2' ∨ w2 = s ⋅ r ⋅ w2') ∧ w2' ∈ ⟨{r⋅s,s⋅r}⟩"
using hull.cases[OF ‹w2 ∈ ⟨{r⋅s,s⋅r}⟩›] empty_iff insert_iff rassoc ‹w1 ∈ ⟨{r ⋅ s, s ⋅ r}⟩› by metis
hence "w2' ∈ ⟨{r⋅s,s⋅r}⟩" and cases2: "(w2 = ε ∨ w2 = r ⋅ s ⋅ w2' ∨ w2 = s ⋅ r ⋅ w2')" by blast+
hence "w2' ∈ ⟨{r,s}⟩" by force
consider (empty2) "w2 = ε" | (sr2) "w2 = s ⋅ r ⋅ w2'" | (rs2) "w2 = r ⋅ s ⋅ w2'"using cases2 by blast
thus False
proof (cases)
case empty2
consider (empty1) "w1 = ε" | (sr1) "w1 = s ⋅ r ⋅ w1'" | (rs1) "w1 = r ⋅ s ⋅ w1'"
using cases1 by blast
thus False
proof (cases)
case empty1
show False
using ‹r ⋅ w1 = w2 ⋅ s›[unfolded empty1 empty2 rassoc] ‹r ≠ s› by simp
next
case sr1
show False
using ‹r ⋅ w1 = w2 ⋅ s›[unfolded sr1 empty2 rassoc] ‹r ≠ ε› fac_triv by auto
next
case rs1
show False
using ‹r ⋅ w1 = w2 ⋅ s›[unfolded rs1 empty2 rassoc emp_simps] ‹r ≠ ε›
fac_triv[of "r ⋅ r" s w1', unfolded rassoc] by force
qed
next
case sr2
have "r ⋅ s = s ⋅ r"
using ‹w2' ∈ ⟨{r,s}⟩› ‹w1 ∈ ⟨{r,s}⟩› ‹r ⋅ w1 = w2 ⋅ s›[unfolded sr2 rassoc]
by (mismatch)
consider (empty1) "w1 = ε" | (sr1) "w1 = s ⋅ r ⋅ w1'" | (rs1) "w1 = r ⋅ s ⋅ w1'" using cases1 by blast
thus False
proof (cases)
case empty1
then show False
using ‹r ⋅ w1 = w2 ⋅ s›[unfolded sr2 empty1 rassoc cancel emp_simps, symmetric] ‹s ≠ ε› fac_triv by blast
next
case rs1
then have "r ⋅ s = s ⋅ r"
using ‹w2' ∈ ⟨{r,s}⟩› ‹w1' ∈ ⟨{r,s}⟩› ‹r ⋅ w1 = w2 ⋅ s›[unfolded rs1 sr2 rassoc cancel]
by mismatch
hence "r ⋅ w1' = w2' ⋅ s"
using ‹r ⋅ w1 = w2 ⋅ s›[unfolded rs1 sr2] rassoc cancel by metis
from less.hyps[OF _ ‹w1' ∈ ⟨{r ⋅ s, s ⋅ r}⟩› ‹w2' ∈ ⟨{r ⋅ s, s ⋅ r}⟩› this]
show False
using lenarg[OF ‹w1 = r ⋅ s ⋅ w1'›, unfolded lenmorph] nemp_len[OF ‹s ≠ ε›] by linarith
next
case sr1
then have "r ⋅ s = s ⋅ r"
using ‹w2' ∈ ⟨{r,s}⟩› ‹w1' ∈ ⟨{r,s}⟩› ‹r ⋅ w1 = w2 ⋅ s›[unfolded sr1 sr2 rassoc cancel]
by mismatch
hence "r ⋅ w1' = w2' ⋅ s"
using ‹r ⋅ w1 = w2 ⋅ s›[unfolded sr1 sr2] rassoc cancel by metis
from less.hyps[OF _ ‹w1' ∈ ⟨{r ⋅ s, s ⋅ r}⟩› ‹w2' ∈ ⟨{r ⋅ s, s ⋅ r}⟩› this]
show False
using less.hyps[OF _ ‹w1' ∈ ⟨{r ⋅ s, s ⋅ r}⟩› ‹w2' ∈ ⟨{r ⋅ s, s ⋅ r}⟩› ‹r ⋅ w1' = w2' ⋅ s›]
lenarg[OF ‹w1 = s ⋅ r ⋅ w1'›, unfolded lenmorph] nemp_len[OF ‹s ≠ ε›] by linarith
qed
next
case rs2
consider (empty1) "w1 = ε" | (sr1) "w1 = s ⋅ r ⋅ w1'" | (rs1) "w1 = r ⋅ s ⋅ w1'" using cases1 by blast
thus False
proof (cases)
case empty1
then show False
using ‹r ⋅ w1 = w2 ⋅ s›[unfolded rs2 empty1 rassoc cancel] ‹s ≠ ε› by blast
next
case rs1
then have "r ⋅ s = s ⋅ r"
using ‹w2' ∈ ⟨{r,s}⟩› ‹w1' ∈ ⟨{r,s}⟩› ‹r ⋅ w1 = w2 ⋅ s›[unfolded rs2 rs1 rassoc cancel]
by mismatch
hence "r ⋅ w1' = w2' ⋅ s"
using ‹r ⋅ w1 = w2 ⋅ s›[unfolded rs1 rs2] rassoc cancel by metis
from less.hyps[OF _ ‹w1' ∈ ⟨{r ⋅ s, s ⋅ r}⟩› ‹w2' ∈ ⟨{r ⋅ s, s ⋅ r}⟩› this]
show False
using less.hyps[OF _ ‹w1' ∈ ⟨{r ⋅ s, s ⋅ r}⟩› ‹w2' ∈ ⟨{r ⋅ s, s ⋅ r}⟩› ‹r ⋅ w1' = w2' ⋅ s›]
lenarg[OF ‹w1 = r ⋅ s ⋅ w1'›, unfolded lenmorph] nemp_len[OF ‹s ≠ ε›] by linarith
next
case sr1
then show False
using less.hyps[OF _ ‹w1' ∈ ⟨{r ⋅ s, s ⋅ r}⟩› ‹w2' ∈ ⟨{r ⋅ s, s ⋅ r}⟩› ‹r ⋅ w1 = w2 ⋅ s›[unfolded rs2 sr1 rassoc cancel]]
lenarg[OF ‹w1 = s ⋅ r ⋅ w1'›, unfolded lenmorph] nemp_len[OF ‹s ≠ ε›] by linarith
qed
qed
qed
qed
lemma conjug_conjug_primroots: assumes "u ≠ ε" and "r ≠ ε" and "ρ (u ⋅ v) = r ⋅ s" and "ρ (v ⋅ u) = s ⋅ r"
obtains k m where "(r ⋅ s)⇧@k ⋅ r = u" and "(s ⋅ r)⇧@m ⋅ s = v"
proof-
have "v ⋅ u ≠ ε" and "u ⋅ v ≠ ε"
using ‹u ≠ ε› by blast+
have "ρ (s ⋅ r) = s ⋅ r"
using primroot_idemp[of "v ⋅ u", unfolded ‹ρ (v ⋅ u) = s ⋅ r›].
obtain n where "(r ⋅ s)⇧@n = u ⋅ v" "0 < n"
using primroot_expE[unfolded ‹ρ (u ⋅ v) = r ⋅ s›]
using assms(3) by metis
obtain n' where "(s ⋅ r)⇧@ n' = v ⋅ u" "0 < n'"
using primroot_expE[of "v ⋅ u",unfolded ‹ρ (v ⋅ u) = s ⋅ r›].
have "(s ⋅ u) ⋅ (s ⋅ r) = (s ⋅ r) ⋅ (s ⋅ u)"
proof (rule pref_marker)
show "(s ⋅ u) ⋅ s ⋅ r ≤p s ⋅ (r ⋅ s)⇧@(n+ n)"
unfolding rassoc add_exps ‹(r ⋅ s)⇧@n = u ⋅ v›
unfolding lassoc ‹(s ⋅ r)⇧@n' = v ⋅ u›[symmetric] using ‹0 < n'› by comparison
show "s ⋅ (r ⋅ s) ⇧@ (n + n) ≤p (s ⋅ r) ⋅ s ⋅ (r ⋅ s) ⇧@ (n + n)"
by comparison
qed
from comm_primroot_exp[OF primroot_nemp[OF ‹v ⋅ u ≠ ε›, unfolded ‹ρ (v ⋅ u) = s ⋅ r›] this]
obtain k where "(s ⋅ r)⇧@k = s ⋅ u"
unfolding ‹ρ (s ⋅ r) = s ⋅ r›.
from suf_nemp[OF ‹u ≠ ε›, of s, folded this]
have "0 < k"
by blast
have u: "(r ⋅ s)⇧@(k-1) ⋅ r = u"
using ‹(s ⋅ r)⇧@k = s ⋅ u› unfolding pow_pos[OF ‹0 < k›] rassoc cancel shift_pow by fast
from exp_pref_cancel[OF ‹(r ⋅ s)⇧@n = u ⋅ v›[folded this, unfolded rassoc, symmetric]]
have "r ⋅ v = (r ⋅ s) ⇧@ (n + 1 - k)"
using ‹0 < k› by fastforce
from pref_nemp[OF ‹r ≠ ε›, of v, unfolded this]
have "0 < n + 1 - k"
by blast
from ‹r ⋅ v = (r ⋅ s) ⇧@ (n + 1 - k)›[unfolded pow_pos[OF ‹0 < n + 1 - k›] rassoc cancel shift_pow[symmetric], symmetric]
have v: "(s ⋅ r)⇧@(n + 1 - k - 1) ⋅ s = v".
show thesis
using that[OF u v].
qed
subsection ‹Predicate ``commutes''›
definition commutes :: "'a list set ⇒ bool"
where "commutes A = (∀x y. x ∈ A ⟶ y ∈ A ⟶ x⋅y = y⋅x)"
lemma commutesE: "commutes A ⟹ x ∈ A ⟹ y ∈ A ⟹ x⋅y = y⋅x"
using commutes_def by blast
lemma commutes_root: assumes "commutes A"
obtains r where "⋀x. x ∈ A ⟹ x ∈ r*"
using assms comm_primroots emp_all_roots primroot_is_root
unfolding commutes_def
by metis
lemma commutes_primroot: assumes "commutes A"
obtains r where "⋀x. x ∈ A ⟹ x ∈ r*" and "primitive r"
using commutes_root[OF assms] emp_all_roots prim_sing
primroot_is_root primroot_prim root_trans
by metis
lemma commutesI [intro]: "(⋀x y. x ∈ A ⟹ y ∈ A ⟹ x⋅y = y⋅x) ⟹ commutes A"
unfolding commutes_def
by blast
lemma commutesI': assumes "x ≠ ε" and "⋀y. y ∈ A ⟹ x⋅y = y⋅x"
shows "commutes A"
proof-
have "⋀x' y'. x' ∈ A ⟹ y' ∈ A ⟹ x'⋅y' = y'⋅x'"
proof-
fix x' y'
assume "x' ∈ A" "y' ∈ A"
hence "x'⋅x = x⋅x'" and "y'⋅x = x⋅y'"
using assms(2) by auto+
from comm_trans[OF this assms(1)]
show "x'⋅y' = y'⋅x'".
qed
thus ?thesis
by (simp add: commutesI)
qed
lemma commutesI_root[intro]: "∀x ∈ A. x ∈ t* ⟹ commutes A"
by (meson comm_root commutesI)
lemma commutes_sub: "commutes A ⟹ B ⊆ A ⟹ commutes B"
by (simp add: commutes_def subsetD)
lemma commutes_insert: "commutes A ⟹ x ∈ A ⟹ x ≠ ε ⟹ x⋅y = y⋅x ⟹ commutes (insert y A)"
using commutesE[of A x] commutesI'[of x "insert y A"] insertE
by blast
lemma commutes_emp [simp]: "commutes {ε, w}"
by (simp add: commutes_def)
lemma commutes_emp'[simp]: "commutes {w, ε}"
by (simp add: commutes_def)
lemma commutes_cancel: assumes "y ∈ A" and "x ⋅ y ∈ A" and "commutes A"
shows "commutes (insert x A)"
proof-
from commutes_root[OF ‹commutes A›]
obtain r where "(⋀x. x ∈ A ⟹ x ∈ r*)"
by metis
hence "y ∈ r*" and "x ⋅ y ∈ r*"
using ‹y ∈ A› ‹x ⋅ y ∈ A› by blast+
hence "x ∈ r*"
using root_suf_cancel by auto
thus "commutes (insert x A)"
using ‹⋀x. x ∈ A ⟹ x ∈ r*› by blast
qed
lemma commutes_cancel': assumes "x ∈ A" and "x ⋅ y ∈ A" and "commutes A"
shows "commutes (insert y A)"
proof-
from commutes_root[OF ‹commutes A›]
obtain r where "(⋀x. x ∈ A ⟹ x ∈ r*)"
by metis
hence "x ∈ r*" and "x ⋅ y ∈ r*"
using ‹x ∈ A› ‹x ⋅ y ∈ A› by blast+
hence "y ∈ r*"
using root_pref_cancel by auto
thus "commutes (insert y A)"
using ‹⋀x. x ∈ A ⟹ x ∈ r*› by blast
qed
subsection ‹Strong elementary lemmas›
text‹Discovered by smt›
lemma xyx_per_comm: assumes "x⋅y⋅x ≤p q⋅x⋅y⋅x"
and "q ≠ ε" and "q ≤p y ⋅ q"
shows "x⋅y = y⋅x"
proof(cases)
assume "x ⋅ y ≤p q"
from pref_marker[OF ‹q ≤p y ⋅ q› this]
show "x ⋅ y = y ⋅ x".
next
have "(x ⋅ y) ⋅ x ≤p q ⋅ x ⋅ y ⋅ x" unfolding rassoc by fact
assume "¬ x ⋅ y ≤p q"
hence "q ≤p x ⋅ y"
using ruler_prefE[OF ‹(x ⋅ y) ⋅ x ≤p q ⋅ x ⋅ y ⋅ x›] by argo
from pref_prolong[OF ‹q ≤p y ⋅ q› this, unfolded lassoc]
have"q ≤p (y ⋅ x) ⋅ y".
from ruler_pref'[OF this, THEN disjE] ‹q ≤p x ⋅ y›
have "q ≤p y ⋅ x"
using pref_trans[OF _ ‹q ≤p x ⋅ y›, of "y ⋅ x", THEN pref_comm_eq] by metis
from pref_cancel'[OF this, of x]
have "x ⋅ q = q ⋅ x"
using pref_marker[OF ‹x ⋅ y ⋅ x ≤p q ⋅ x ⋅ y ⋅ x›, of x] by blast
hence "x ⋅ y ⋅ x ≤p x ⋅ x ⋅ y ⋅ x"
using root_comm_root[OF _ _ ‹q ≠ ε›, of "x ⋅ y ⋅ x" x] ‹x ⋅ y ⋅ x ≤p q ⋅ x ⋅ y ⋅ x› by fast
thus "x⋅y = y⋅x"
by mismatch
qed
lemma two_elem_root_suf_comm: assumes "u ≤p v ⋅ u" and "v ≤s p ⋅ u" and "p ∈ ⟨{u,v}⟩"
shows "u ⋅ v = v ⋅ u"
using root_suf_comm[OF ‹u ≤p v ⋅ u› two_elem_suf[OF ‹v ≤s p ⋅ u› ‹p ∈ ⟨{u,v}⟩›], symmetric].
subsection ‹Binary words without a letter square›
lemma no_repetition_list:
assumes "set ws ⊆ {a,b}"
and not_per: "¬ ws ≤p [a,b] ⋅ ws" "¬ ws ≤p [b,a] ⋅ ws"
and not_square: "¬ [a,a] ≤f ws" and "¬ [b,b] ≤f ws"
shows False
using assms
proof (induction ws)
case (Cons d ws)
show ?case
proof (rule "Cons.IH")
show "set ws ⊆ {a,b}"
using ‹set (d # ws) ⊆ {a, b}› by auto
have "ws ≠ ε"
using "Cons.IH" Cons.prems by force
from hd_tl[OF this]
have "hd ws ≠ d"
using Cons.prems(1,4-5) hd_pref[OF ‹ws ≠ ε›] by force
thus "¬ [a, a] ≤f ws" and "¬ [b, b] ≤f ws"
using Cons.prems(4-5) unfolding sublist_code(3) by blast+
show "¬ ws ≤p [a, b] ⋅ ws"
proof (rule notI)
assume "ws ≤p [a, b] ⋅ ws"
from pref_hd_eq[OF this ‹ws ≠ ε›]
have "hd ws = a" by simp
hence "d = b"
using ‹set (d # ws) ⊆ {a, b}› ‹hd ws ≠ d› by auto
show False
using ‹ws ≤p [a, b] ⋅ ws› ‹¬ d # ws ≤p [b, a] ⋅ d # ws›[unfolded ‹d = b›] by force
qed
show "¬ ws ≤p [b, a] ⋅ ws"
proof (rule notI)
assume "ws ≤p [b, a] ⋅ ws"
from pref_hd_eq[OF this ‹ws ≠ ε›]
have "hd ws = b" by simp
hence "d = a"
using ‹set (d # ws) ⊆ {a, b}› ‹hd ws ≠ d› by auto
show False
using ‹ws ≤p [b, a] ⋅ ws› ‹¬ d # ws ≤p [a, b] ⋅ d # ws›[unfolded ‹d = a›] by force
qed
qed
qed simp
lemma hd_Cons_append[intro,simp]: "hd ((a#v) ⋅ u) = a"
by simp
lemma no_repetition_list_bin:
fixes ws :: "binA list"
assumes not_square: "⋀ c. ¬ [c,c] ≤f ws"
shows "ws ≤p [hd ws, 1-(hd ws)] ⋅ ws"
proof (cases "ws = ε")
assume "ws ≠ ε"
have set: "set ws ⊆ {hd ws, 1-hd ws}"
using swap_UNIV by auto
have "¬ ws ≤p [1 - hd ws, hd ws] ⋅ ws"
using pref_hd_eq[OF _ ‹ws ≠ ε›, of "[1 - hd ws, hd ws] ⋅ ws"] bin_swap_neq'
unfolding hd_Cons_append by blast
from no_repetition_list[OF set _ this not_square not_square]
show "ws ≤p [hd ws, 1-(hd ws)] ⋅ ws" by blast
qed simp
lemma per_root_hd_last_root: assumes "ws ≤p [a,b] ⋅ ws" and "hd ws ≠ last ws"
shows "ws ∈ [a,b]*"
using assms
proof (induction "❙|ws❙|" arbitrary: ws rule: less_induct)
case less
then show ?case
proof (cases "ws = ε")
assume "ws ≠ ε"
with ‹hd ws ≠ last ws›
have *: "[hd ws, hd (tl ws)] ⋅ tl (tl ws) = ws"
using append_Cons last_ConsL[of "tl ws" "hd ws"] list.exhaust_sel[of ws] hd_tl by metis
have ind: "❙|tl (tl ws)❙| < ❙|ws❙|" using ‹ws ≠ ε› by auto
have "[hd ws, hd (tl ws)] ⋅ tl (tl ws) ≤p [a,b] ⋅ ws "
unfolding * using ‹ws ≤p [a, b] ⋅ ws›.
hence "[a,b] = [hd ws, hd (tl ws)]" by simp
hence "hd ws = a" by simp
have "tl (tl ws) ≤p [a,b] ⋅ tl (tl ws)"
unfolding pref_cancel_conv[of "[a,b]" "tl (tl ws)", symmetric] ‹[a,b] = [hd ws, hd (tl ws)]› *
using ‹ws ≤p [a, b] ⋅ ws›[unfolded ‹[a,b] = [hd ws, hd (tl ws)]›].
have "tl (tl ws) ∈ [a, b]*"
proof (cases "tl (tl ws) = ε")
assume "tl (tl ws) ≠ ε"
from pref_hd_eq[OF ‹tl (tl ws) ≤p [a, b] ⋅ tl (tl ws)› this]
have "hd (tl (tl ws)) = a" by simp
have "last (tl (tl ws)) = last ws"
using ‹tl (tl ws) ≠ ε› last_tl tl_Nil by metis
from ‹hd ws ≠ last ws›[unfolded ‹hd ws =a›, folded this ‹hd (tl (tl ws)) = a›]
have "hd (tl (tl ws)) ≠ last (tl (tl ws))".
from less.hyps[OF ind ‹tl (tl ws) ≤p [a,b] ⋅ tl (tl ws)› this]
show "tl (tl ws) ∈ [a, b]*".
qed simp
thus "ws ∈ [a,b]*"
unfolding add_root[of "[a,b]" "tl(tl ws)", symmetric]
*[folded ‹[a,b] = [hd ws, hd (tl ws)]› ].
qed simp
qed
lemma no_cyclic_repetition_list:
assumes "set ws ⊆ {a,b}" "ws ∉ [a,b]*" "ws ∉ [b,a]*" "hd ws ≠ last ws"
"¬ [a,a] ≤f ws" "¬ [b,b] ≤f ws"
shows False
using per_root_hd_last_root[OF _ ‹hd ws ≠ last ws›] ‹ws ∉ [a,b]*› ‹ws ∉ [b,a]*›
no_repetition_list[OF assms(1) _ _ assms(5-6)] by blast
subsection ‹Three covers›
lemma three_covers_example:
assumes
v: "v = 𝔞" and
t: "t = (𝔟 ⋅ 𝔞⇧@(j+1))⇧@(m + l + 1) ⋅ 𝔟 ⋅ 𝔞 " and
r: "r = 𝔞 ⋅ 𝔟 ⋅ (𝔞⇧@(j+1) ⋅ 𝔟)⇧@(m + l + 1)" and
t': "t' = (𝔟 ⋅ 𝔞⇧@(j + 1))⇧@m ⋅ 𝔟 ⋅ 𝔞 " and
r': "r' = 𝔞 ⋅ 𝔟 ⋅ (𝔞⇧@(j + 1) ⋅ 𝔟)⇧@l" and
w: "w = 𝔞 ⋅ (𝔟 ⋅ 𝔞⇧@(j + 1))⇧@(m + l + 1) ⋅ 𝔟 ⋅ 𝔞 "
shows "w = v ⋅ t" and "w = r ⋅ v" and "w = r' ⋅ v⇧@(j + 1) ⋅ t'" and "t' <p t" and "r' <s r"
proof-
show "w = v ⋅ t"
unfolding w v t..
show "w = r ⋅ v"
unfolding w r v by comparison
find_theorems "?u ⋅ ?u⇧@?j = ?u⇧@?j ⋅ ?u"
show "t' <p t"
unfolding t t' unfolding add.assoc unfolding add.commute[of l]
unfolding add_exps rassoc spref_cancel_conv unfolding pow_1
unfolding rassoc spref_cancel_conv
unfolding lassoc shifts(20)
unfolding rassoc by blast
have "r = 𝔞 ⋅ 𝔟 ⋅ (𝔞⇧@Suc j ⋅ 𝔟)⇧@ m ⋅ 𝔞⇧@j ⋅ r'"
unfolding r' r by comparison
thus "r' <s r"
by force
show "w = r' ⋅ v⇧@(j + 1) ⋅ t'"
unfolding w r' v t'
by comparison
qed
lemma three_covers_pers:
assumes "w = v ⋅ t" and "w = r' ⋅ v⇧@j ⋅ t'" and "w = r ⋅ v" and "0 < j" and
"r' <s r" and "t' <p t"
shows "period w (❙|t❙| - ❙|t'❙|)" and "period w (❙|r❙| - ❙|r'❙|)" and
"(❙|t❙| - ❙|t'❙|) + (❙|r❙| - ❙|r'❙|) = ❙|w❙| + j*❙|v❙| - 2*❙|v❙|"
proof-
let ?per_r = "❙|r❙| - ❙|r'❙|"
let ?per_t = "❙|t❙| - ❙|t'❙|"
let ?gcd = "gcd (❙|t❙| - ❙|t'❙|) (❙|r❙| - ❙|r'❙|)"
have "w ≠ ε"
using ‹w = v ⋅ t› ‹t' <p t› by auto
obtain "r''" where "r'' ⋅ r' = r" and "r'' ≠ ε"
using ssufD[OF ‹r' <s r›] sufD by blast
have "w <p r'' ⋅ w"
using per_rootI[OF _ ‹r'' ≠ ε›, of w] ‹w = r ⋅ v› ‹w = r' ⋅ v ⇧@ j ⋅ t'› ‹r'' ⋅ r' = r›
unfolding pow_pos[OF ‹0 < j›] using rassoc triv_pref by metis
thus "period w ?per_r"
using lenarg[OF ‹r'' ⋅ r' = r›] periodI[OF ‹w ≠ ε› ‹w <p r'' ⋅ w›]
unfolding lenmorph
by (metis add_diff_cancel_right')
have "❙|r'❙| < ❙|r❙|"
using suffix_length_less[OF ‹r' <s r›].
have "❙|t'❙| < ❙|t❙|"
using prefix_length_less[OF ‹t' <p t›].
obtain t'' where "t' ⋅ t'' = t" and "t'' ≠ ε"
using ‹t' <p t› by (blast elim: spref_exE)
have "w <s w ⋅ t''"
using per_rootI[reversed, OF _ ‹t'' ≠ ε›, of w]
‹w = v ⋅ t› ‹w = r' ⋅ v ⇧@ j ⋅ t'› ‹t' ⋅ t'' = t›
unfolding pow_pos'[OF ‹0 < j›] using rassoc triv_suf by metis
thus "period w ?per_t"
using lenarg[OF ‹t' ⋅ t'' = t›] periodI[reversed, OF ‹w ≠ ε› ‹w <s w ⋅ t''›]
unfolding lenmorph
by (metis add_diff_cancel_left')
show eq: "?per_t + ?per_r = ❙|w❙| + j*❙|v❙| - 2*❙|v❙|"
using lenarg[OF ‹w = r' ⋅ v⇧@ j ⋅ t'›]
lenarg[OF ‹w = v ⋅ t›] lenarg[OF ‹w = r ⋅ v›] ‹❙|t'❙| < ❙|t❙|› ‹❙|r'❙| < ❙|r❙|›
unfolding pow_len lenmorph by force
qed
lemma three_covers_per0: assumes "w = v ⋅ t" and "w = r' ⋅ v⇧@ j ⋅ t'" and "w = r ⋅ v" and "0 < j"
"r' <s r" and "t' <p t" and "❙|t'❙| ≤ ❙|r'❙|"
and "primitive v"
shows "period w (gcd (❙|t❙| - ❙|t'❙|) (❙|r❙| - ❙|r'❙|))"
using assms
proof (induct "❙|w❙|" arbitrary: w t r t' r' v rule: less_induct)
case less
then show ?case
proof-
let ?per_r = "❙|r❙| - ❙|r'❙|"
let ?per_t = "❙|t❙| - ❙|t'❙|"
let ?gcd = "gcd (❙|t❙| - ❙|t'❙|) (❙|r❙| - ❙|r'❙|)"
have "v ≠ ε" using prim_nemp[OF ‹primitive v›].
have "w ≠ ε"
using ‹w = v ⋅ t› ‹v ≠ ε› by blast
note prefix_length_less[OF ‹t' <p t›] prefix_length_less[reversed, OF ‹r' <s r›]
have "?gcd ≠ 0"
using gcd_eq_0_iff zero_less_diff'[OF ‹❙|t'❙| < ❙|t❙|›] by simp
have "period w ?per_t" and "period w ?per_r"
and eq: "?per_t + ?per_r = ❙|w❙| + j*❙|v❙| - 2*❙|v❙|"
using three_covers_pers[OF ‹w = v ⋅ t› ‹w = r' ⋅ v ⇧@ j ⋅ t'› ‹w = r ⋅ v› ‹0 < j› ‹r' <s r› ‹t' <p t›].
obtain "r''" where "r'' ⋅ r' = r" and "r'' ≠ ε"
using ssufD[OF ‹r' <s r›] sufD by blast
hence "w ≤p r'' ⋅ w"
using less.prems unfolding pow_pos[OF ‹0 < j›] using rassoc triv_pref by metis
obtain "t''" where "t' ⋅ t'' = t" and "t'' ≠ ε"
using sprefD[OF ‹t' <p t›] prefD by blast
show "period w ?gcd"
proof (cases)
have local_rule: "a - c ≤ b ⟹ k + a - c - b ≤ k" for a b c k :: nat
by simp
assume "j*❙|v❙| - 2*❙|v❙| ≤ ?gcd"
from local_rule[OF this]
have len: "?per_t + ?per_r - ?gcd ≤ ❙|w❙|"
unfolding eq.
show "period w ?gcd"
using per_lemma[OF ‹period w ?per_t› ‹period w ?per_r› len].
next
assume "¬ j*❙|v❙| - 2*❙|v❙| ≤ ?gcd"
hence "?gcd ≤ ❙|v⇧@j❙| - 2*❙|v❙|"
unfolding pow_len by linarith
hence "?gcd + ❙|v❙| ≤ ❙|v ⇧@ j❙|"
using ‹?gcd ≠ 0› by linarith
show "period w ?gcd"
proof (cases)
assume "❙|r'❙| = ❙|t'❙|"
hence "❙|t❙| - ❙|t'❙| = ❙|r❙| - ❙|r'❙|"
using conj_len[OF ‹w = v ⋅ t›[unfolded ‹w = r ⋅ v›]] by force
show "period w (gcd (❙|t❙| - ❙|t'❙|) (❙|r❙| - ❙|r'❙|))"
unfolding ‹❙|t❙| - ❙|t'❙| = ❙|r❙| - ❙|r'❙|› gcd_idem_nat using ‹period w (❙|r❙| - ❙|r'❙|)›.
next
assume "❙|r'❙| ≠ ❙|t'❙|"
hence "❙|t'❙| < ❙|r'❙|"
using ‹❙|t'❙| ≤ ❙|r'❙|› by force
have "r' ⋅ v <p w"
using ‹❙|r'❙| < ❙|r❙|› ‹r'' ⋅ r' = r› ‹w ≤p r'' ⋅ w› ‹w = r ⋅ v› by force
obtain p where "r' ⋅ v = v ⋅ p"
using ruler_le[OF triv_pref[of v t , folded ‹w = v ⋅ t›], of "r' ⋅ v"]
unfolding lenmorph ‹w = r' ⋅ v⇧@j ⋅ t'›[unfolded pow_pos[OF ‹0 < j›]] rassoc
by (force simp add: prefix_def)
from ‹w = r' ⋅ v⇧@j ⋅ t'›[unfolded pow_pos[OF ‹0 < j›] lassoc this ‹w = v ⋅ t›, unfolded rassoc cancel]
have "p ≤p t"
by blast
have "❙|v ⋅ p❙| < ❙|w❙|"
using prefix_length_less[OF ‹r' ⋅ v <p w›, unfolded ‹r' ⋅ v = v ⋅ p›].
have "v ⋅ p ≤s w"
using ‹r' ⋅ v = v ⋅ p› ‹w = r ⋅ v› ‹r' <s r› same_suffix_suffix ssufD by metis
have "❙|r'❙| = ❙|p❙|"
using conj_len[OF ‹r' ⋅ v = v ⋅ p›].
note ‹❙|t'❙| ≤ ❙|r'❙|›[unfolded ‹❙|r'❙| = ❙|p❙|›]
hence "t' <p p"
using ‹t = p ⋅ v ⇧@ (j - 1) ⋅ t'› ‹t' ⋅ t'' = t› ‹❙|r'❙| = ❙|p❙|› ‹❙|t'❙| < ❙|r'❙|› ‹p ≤p t› pref_prod_long_less by metis
hence "p ≠ ε"
by auto
show ?thesis
proof (cases)
assume "❙|v ⋅ p❙| ≤ ❙|v⇧@j ⋅ t'❙|"
have "ρ (rev v) = rev (ρ v)"
using ‹v ≠ ε› primroot_rev by auto
from pref_marker_ext[reversed, OF ‹❙|t'❙| ≤ ❙|p❙|› ‹v ≠ ε›]
suf_prod_le[OF ‹v ⋅ p ≤s w›[unfolded ‹w = r' ⋅ v⇧@j ⋅ t'›] ‹❙|v ⋅ p❙| ≤ ❙|v⇧@j ⋅ t'❙|›]
obtain k where "p = v⇧@k ⋅ t'"
unfolding prim_self_root[OF ‹primitive v›].
hence "p ≤p v⇧@k ⋅ p"
using ‹t' <p p› by simp
from root_comm_root[OF this pow_comm[symmetric]]
have "p ≤p v ⋅ p"
using ‹❙|r'❙| = ❙|p❙|› ‹❙|r'❙| ≠ ❙|t'❙|› ‹p = v ⇧@ k ⋅ t'› by force
hence "p = r'"
using ‹❙|r'❙| = ❙|p❙|› ‹r' ⋅ v = v ⋅ p› pref_prod_eq by metis
note ‹r' ⋅ v = v ⋅ p›[folded this] ‹r' ⋅ v = v ⋅ p›[unfolded this]
then obtain er' where "r' = v⇧@er'"
using ‹primitive v› by auto
from ‹p ⋅ v = v ⋅ p›[unfolded ‹p = v⇧@k ⋅ t'› lassoc pow_comm[symmetric], unfolded rassoc cancel]
have "t' ⋅ v = v ⋅ t'".
then obtain et' where "t' = v⇧@et'"
using ‹primitive v› by auto
have "t ⋅ v = v ⋅ t"
by (simp add: pow_comm ‹p = r'› ‹r' ⋅ v = v ⋅ r'› ‹t = p ⋅ v ⇧@ (j - 1) ⋅ t'› ‹t' ⋅ v = v ⋅ t'›)
then obtain et where "t = v⇧@et"
using ‹primitive v› by auto
have "r ⋅ v = v ⋅ r"
using ‹t ⋅ v = v ⋅ t› cancel_right ‹w = v ⋅ t› ‹w = r ⋅ v› by metis
then obtain er where "r = v⇧@er"
using ‹primitive v› by auto
have "w ⋅ v = v ⋅ w"
by (simp add: ‹r ⋅ v = v ⋅ r› ‹w = r ⋅ v›)
then obtain ew where "w = v⇧@ew"
using ‹primitive v› by auto
hence "period w ❙|v❙|"
using ‹v ≠ ε› ‹w ⋅ v = v ⋅ w› ‹w ≠ ε› by blast
have dift: "❙|t❙| - ❙|t'❙| = (et - et')*❙|v❙|"
using lenarg[OF ‹t = v⇧@et›] lenarg[OF ‹t' = v⇧@et'›] unfolding lenmorph pow_len
by (simp add: diff_mult_distrib)
have difr: "(❙|r❙| - ❙|r'❙|) = (er - er')*❙|v❙|"
using lenarg[OF ‹r = v⇧@er›] lenarg[OF ‹r' = v⇧@er'›] unfolding lenmorph pow_len
by (simp add: diff_mult_distrib)
obtain g where g: "g*❙|v❙| = ?gcd"
unfolding dift difr mult.commute[of _ "❙|v❙|"]
gcd_mult_distrib_nat[symmetric] by blast
hence "0 < g"
using nemp_len[OF ‹v ≠ ε›] per_not_zero[OF ‹period w (❙|r❙| - ❙|r'❙|)›]
gcd_nat.neutr_eq_iff[of "❙|t❙| - ❙|t'❙|" "❙|r❙| - ❙|r'❙|"] mult_is_0[of g "❙|v❙|"]
by force
from per_mult[OF ‹period w ❙|v❙|› this]
show ?thesis
unfolding g.
next
assume "¬ ❙|v ⋅ p❙| ≤ ❙|v ⇧@ j ⋅ t'❙|"
then obtain ri' where "v ⋅ p = ri'⋅ v⇧@j ⋅ t'" and "ri' ≤s r'"
using ‹v ⋅ p ≤s w› unfolding ‹w = r' ⋅ v⇧@j ⋅ t'›
using suffix_append suffix_length_le by blast
from len_less_neq[OF ‹❙|v ⋅ p❙| < ❙|w❙|›, unfolded this(1) ‹w = r' ⋅ v⇧@j ⋅ t'›] this(2)
have "ri' <s r'"
by blast
have gcd_eq: "gcd (❙|p❙| - ❙|t'❙|) (❙|r'❙| - ❙|ri'❙|) = ?gcd"
proof-
have "❙|r'❙| ≤ ❙|r❙|"
by (simp add: ‹❙|r'❙| < ❙|r❙|› dual_order.strict_implies_order)
have "❙|t❙| = ❙|r❙|"
using lenarg[OF ‹w = v ⋅ t›] unfolding lenarg[OF ‹w = r ⋅ v›] lenmorph by auto
have e1: "❙|r'❙| - ❙|ri'❙| = ❙|r❙| - ❙|r'❙|"
using lenarg[OF ‹v ⋅ p = ri'⋅v⇧@ j ⋅ t'›[folded ‹r' ⋅ v = v ⋅ p›]]
lenarg[OF ‹w = r ⋅ v›[unfolded ‹w = r' ⋅ v⇧@ j ⋅ t'›]]
unfolding lenmorph pow_len by (simp add: add.commute diff_add_inverse diff_diff_add)
have "❙|t❙| = ❙|p❙| + ❙|r'❙| - ❙|ri'❙|"
unfolding add_diff_assoc[OF suffix_length_le[OF ‹ri' ≤s r'›], unfolded e1, symmetric]
‹❙|t❙| = ❙|r❙|› unfolding ‹❙|r'❙| = ❙|p❙|›
using ‹❙|r'❙| < ❙|r❙|›[unfolded ‹❙|r'❙| = ❙|p❙|›] by linarith
hence e2: "❙|t❙| - ❙|t'❙| = (❙|p❙| - ❙|t'❙|) + (❙|r'❙| - ❙|ri'❙|)"
unfolding add_diff_assoc2[OF ‹❙|t'❙| ≤ ❙|p❙|›] ‹❙|t❙| = ❙|p❙| + ❙|r'❙| - ❙|ri'❙|›
using suf_len[OF ‹ri' ≤s r'›] by force
show ?thesis
unfolding e2 e1 gcd_add1..
qed
have per_vp: "period (v ⋅ p) ?gcd"
proof (cases)
assume "❙|t'❙| ≤ ❙|ri'❙|"
from less.hyps[OF ‹❙|v ⋅ p❙| < ❙|w❙|› refl ‹v ⋅ p = ri'⋅v⇧@ j ⋅ t'› ‹r' ⋅ v = v ⋅ p›[symmetric] ‹0 < j›
‹ri' <s r'› ‹t' <p p› this ‹primitive v›]
show "period (v ⋅ p) ?gcd"
unfolding gcd_eq by blast
next
assume "¬ ❙|t'❙| ≤ ❙|ri'❙|" hence "❙|ri'❙| ≤ ❙|t'❙|" by simp
have "period (rev p ⋅ rev v) (gcd (❙|rev r'❙| - ❙|rev ri'❙|) (❙|rev p❙| - ❙|rev t'❙|))"
proof (rule less.hyps[OF _ _ _ refl])
show "❙|rev p ⋅ rev v❙| < ❙|w❙|"
using ‹❙|v ⋅ p❙| < ❙|w❙|› by simp
show "rev p ⋅ rev v = rev v ⋅ rev r'"
using ‹r' ⋅ v = v ⋅ p› unfolding rev_append[symmetric] by simp
show "rev p ⋅ rev v = rev t' ⋅ rev v ⇧@ j ⋅ rev ri'"
using ‹v ⋅ p = ri'⋅v⇧@ j ⋅ t'› unfolding rev_append[symmetric] rev_pow[symmetric] rassoc by simp
show "rev t' <s rev p"
using ‹t' <p p› by (auto simp add: prefix_def)
show "rev ri' <p rev r'"
using ‹ri' <s r'› strict_suffix_to_prefix by blast
show "❙|rev ri'❙| ≤ ❙|rev t'❙|"
by (simp add: ‹❙|ri'❙| ≤ ❙|t'❙|›)
show "primitive (rev v)"
by (simp add: ‹primitive v› prim_rev_iff)
qed fact
thus ?thesis
unfolding length_rev rev_append[symmetric] period_rev_conv gcd.commute[of "❙|r'❙| - ❙|ri'❙|"] gcd_eq.
qed
have "period (v⇧@ j) (gcd ❙|v❙| ?gcd)"
proof (rule per_lemma)
show " ❙|v❙| + ?gcd - gcd ❙|v❙| (gcd (❙|t❙| - ❙|t'❙|) (❙|r❙| - ❙|r'❙|)) ≤ ❙|v ⇧@ j❙|"
using ‹?gcd + ❙|v❙| ≤ ❙|v ⇧@ j❙|› by linarith
show "period (v ⇧@ j) ❙|v❙|"
using ‹v ≠ ε› ‹0 < j›
by blast
find_theorems "?v⇧@?n" "?w = ε"
have "v ⇧@ j ≠ ε"
using ‹0 < j› ‹v ≠ ε› by blast
from period_fac[OF per_vp[unfolded ‹v ⋅ p = ri' ⋅ v ⇧@ j ⋅ t'›] this]
show "period (v ⇧@ j) ?gcd".
qed
have per_vp': "period (v ⋅ p) (gcd ❙|v❙| ?gcd)"
proof (rule refine_per)
show "gcd ❙|v❙| ?gcd dvd ?gcd" by blast
show "?gcd ≤ ❙|v⇧@j❙|"
using ‹?gcd + ❙|v❙| ≤ ❙|v ⇧@ j❙|› add_leE by blast
show "v ⇧@ j ≤f v ⋅ p"
using facI'[OF ‹v ⋅ p = ri' ⋅ v ⇧@ j ⋅ t'›[symmetric]].
qed fact+
have "period w (gcd ❙|v❙| ?gcd)"
proof (rule per_glue)
show "v ⋅ p ≤p w"
using ‹p ≤p t› ‹w = v ⋅ t› by auto
have "❙|v ⇧@ j❙| + ❙|t'❙| ≤ ❙|v❙| + ❙|p❙|"
using ‹¬ ❙|v ⋅ p❙| ≤ ❙|v ⇧@ j ⋅ t'❙|› by auto
moreover have "❙|r'❙| + gcd ❙|v❙| ?gcd ≤ ❙|v❙| + ❙|p❙|"
using lenarg[OF ‹r' ⋅ v = v ⋅ p›, unfolded lenmorph]
‹v ≠ ε› gcd_le1_nat length_0_conv nat_add_left_cancel_le by metis
ultimately show "❙|w❙| + gcd ❙|v❙| ?gcd ≤ ❙|v ⋅ p❙| + ❙|v ⋅ p❙|"
unfolding lenarg[OF ‹w = r' ⋅ v ⇧@ j ⋅ t'›] lenmorph add.commute[of "❙|r'❙|"] by linarith
qed fact+
obtain k where k: "?gcd = k*(gcd ❙|v❙| ?gcd)"
using gcd_dvd2 unfolding dvd_def mult.commute[of _ "gcd ❙|v❙| ?gcd"] by blast
hence "k ≠ 0"
using ‹?gcd ≠ 0› by algebra
from per_mult[OF ‹period w (gcd ❙|v❙| ?gcd)› this[unfolded neq0_conv], folded k]
show ?thesis.
qed
qed
qed
qed
qed
lemma three_covers_per: assumes "w = v ⋅ t" and "w = r' ⋅ v⇧@j ⋅ t'" and "w = r ⋅ v"
"r' <s r" and "t' <p t" and "0 < j"
shows "period w (gcd (❙|t❙| - ❙|t'❙|) (❙|r❙| - ❙|r'❙|))"
proof-
let ?per_r = "❙|r❙| - ❙|r'❙|"
let ?per_t = "❙|t❙| - ❙|t'❙|"
let ?gcd = "gcd (❙|t❙| - ❙|t'❙|) (❙|r❙| - ❙|r'❙|)"
have "period w ?per_t" and "period w ?per_r" and len: "(❙|t❙| - ❙|t'❙|) + (❙|r❙| - ❙|r'❙|) = ❙|w❙| + j*❙|v❙| - 2*❙|v❙|"
using three_covers_pers[OF ‹w = v ⋅ t› ‹w = r' ⋅ v ⇧@ j ⋅ t'› ‹w = r ⋅ v› ‹0 < j› ‹r' <s r› ‹t' <p t›] by blast+
show ?thesis
proof(cases)
assume "v = ε"
have "❙|t❙| - ❙|t'❙| + (❙|r❙| - ❙|r'❙|) = ❙|w❙|"
using ‹w = v ⋅ t› ‹w = r' ⋅ v⇧@j ⋅ t'› ‹w = r ⋅ v› unfolding ‹v = ε› emp_pow emp_simps by force
from per_lemma[OF ‹period w ?per_t› ‹period w ?per_r›, unfolded this]
show "period w ?gcd"
by fastforce
next
assume "v ≠ ε"
show ?thesis
proof (cases)
assume "j ≤ 1"
hence "(j = 0 ⟹ P) ⟹ (j = 1 ⟹ P) ⟹ P" for P by force
hence "❙|w❙| + j*❙|v❙| - 2*❙|v❙| - ?gcd ≤ ❙|w❙|"
by (cases, simp_all)
thus "period w ?gcd"
using per_lemma[OF ‹period w ?per_t› ‹period w ?per_r›] unfolding len by blast
next
assume "¬ j ≤ 1" hence "2 ≤ j" by simp
obtain e where "v = ρ v⇧@e" "0 < e"
using primroot_expE by metis
have "w = ρ v ⋅ ρ v⇧@(e -1) ⋅ t"
unfolding lassoc pow_pos[OF ‹0 < e›, symmetric] ‹v = ρ v⇧@e›[symmetric] by fact
have "w = (r ⋅ ρ v⇧@(e - 1)) ⋅ ρ v"
unfolding rassoc pow_pos'[OF ‹0 < e›, symmetric] ‹v = ρ v⇧@e›[symmetric] by fact
note aux = add_less_mono[OF diff_less[OF zero_less_one ‹0 < e›] diff_less[OF zero_less_one ‹0 < e›]]
have "(e-1) + (e-1) < j*e"
using less_le_trans[OF aux mult_le_mono1[OF ‹2 ≤ j›, unfolded mult_2]].
then obtain e' where "(e-1) + (e-1) + e' = j*e" "0 < e'"
using less_imp_add_positive by blast
hence aux_sum: "(e - 1) + e' + (e - 1) = j*e"
by presburger
have cover3: "w = (r' ⋅ (ρ v)⇧@(e-1)) ⋅ (ρ v) ⇧@e' ⋅ ((ρ v)⇧@(e-1) ⋅ t')"
unfolding ‹w = r' ⋅ v⇧@ j ⋅ t'› rassoc cancel unfolding lassoc cancel_right
unfolding add_exps[symmetric]
pow_mult unfolding aux_sum unfolding mult.commute[of j]
pow_mult ‹v = ρ v⇧@e›[symmetric]..
show ?thesis
proof(cases)
assume "❙|t'❙| ≤ ❙|r'❙|"
have dif1: "❙|ρ v ⇧@ (e -1) ⋅ t❙| - ❙|ρ v ⇧@ (e - 1) ⋅ t'❙| = ❙|t❙| - ❙|t'❙|"
unfolding lenmorph by simp
have dif2: "❙|r ⋅ ρ v ⇧@ (e-1)❙| - ❙|r' ⋅ ρ v ⇧@ (e-1)❙| = ❙|r❙| - ❙|r'❙|"
unfolding lenmorph by simp
show ?thesis
proof (rule three_covers_per0[OF ‹w = ρ v ⋅ (ρ v⇧@(e -1) ⋅ t)›
cover3 ‹w = (r ⋅ ρ v⇧@(e - 1)) ⋅ ρ v› ‹0 < e'› _ _ _ primroot_prim[OF ‹v ≠ ε›],
unfolded dif1 dif2])
show "r' ⋅ ρ v ⇧@ (e -1) <s r ⋅ ρ v ⇧@ (e -1)"
using ‹r' <s r› by auto
show "ρ v ⇧@ (e - 1) ⋅ t' <p ρ v ⇧@ (e - 1) ⋅ t"
using ‹t' <p t› by auto
show "❙|ρ v ⇧@ (e -1) ⋅ t'❙| ≤ ❙|r' ⋅ ρ v ⇧@ (e - 1)❙|"
unfolding lenmorph using ‹❙|t'❙| ≤ ❙|r'❙|› by auto
qed
next
let ?w = "rev w" and ?r = "rev t" and ?t = "rev r" and ?ρ = "rev (ρ v)" and ?r' = "rev t'" and ?t' = "rev r'"
assume "¬ ❙|t'❙| ≤ ❙|r'❙|"
hence "❙|?t'❙| ≤ ❙|?r'❙|" by auto
have "?w = (?r ⋅ ?ρ⇧@(e-1)) ⋅ ?ρ"
unfolding rev_pow[symmetric] rev_append[symmetric] ‹w = ρ v ⋅ (ρ v⇧@(e-1) ⋅ t)› rassoc..
have "?w = ?ρ ⋅ (?ρ⇧@(e-1) ⋅ ?t)"
unfolding rev_pow[symmetric] rev_append[symmetric] ‹w = (r ⋅ ρ v⇧@(e-1)) ⋅ ρ v›..
have "?w = (?r' ⋅ ?ρ⇧@(e-1)) ⋅ ?ρ⇧@e' ⋅ (?ρ⇧@(e-1) ⋅ ?t')"
unfolding rev_pow[symmetric] rev_append[symmetric] ‹w = (r' ⋅ ρ v⇧@(e-1)) ⋅ ρ v ⇧@e' ⋅ (ρ v⇧@(e-1) ⋅ t')› rassoc..
have dif1: "❙|?ρ ⇧@ (e-1) ⋅ ?t❙| - ❙|?ρ ⇧@ (e-1) ⋅ ?t'❙| = ❙|r❙| - ❙|r'❙|"
unfolding lenmorph by simp
have dif2: "❙|?r ⋅ ?ρ ⇧@ (e-1)❙| - ❙|?r' ⋅ ?ρ ⇧@ (e-1)❙| = ❙|t❙| - ❙|t'❙|"
unfolding lenmorph by simp
show ?thesis
proof(rule three_covers_per0[OF ‹?w = ?ρ ⋅ (?ρ⇧@(e-1) ⋅ ?t)›
‹?w = (?r' ⋅ ?ρ⇧@(e-1)) ⋅ ?ρ⇧@e' ⋅ (?ρ⇧@(e-1) ⋅ ?t')› ‹?w = (?r ⋅ ?ρ⇧@(e-1)) ⋅ ?ρ› ‹0 < e'›,
unfolded dif1 dif2 period_rev_conv gcd.commute[of "❙|r❙| - ❙|r'❙|"]])
show "?r' ⋅ ?ρ ⇧@ (e-1) <s ?r ⋅ ?ρ ⇧@ (e-1)"
using ‹t' <p t› by (auto simp add: prefix_def)
show "?ρ ⇧@ (e-1) ⋅ ?t' <p ?ρ ⇧@ (e-1) ⋅ ?t"
using ‹r' <s r› by (auto simp add: suffix_def)
show "❙|?ρ ⇧@ (e-1) ⋅ ?t'❙| ≤ ❙|?r' ⋅ ?ρ ⇧@ (e-1)❙|"
unfolding lenmorph using ‹❙|?t'❙| ≤ ❙|?r'❙|› by auto
show "primitive ?ρ"
using primroot_prim[OF ‹v ≠ ε›] by (simp add: prim_rev_iff)
qed
qed
qed
qed
qed
thm per_root_modE'
lemma assumes "w <p r ⋅ w"
obtains p q i where "w = (p ⋅ q)⇧@i ⋅ p" "p ⋅ q = r"
using assms by blast
lemma three_coversE: assumes "w = v ⋅ t" and "w = r' ⋅ v ⋅ t'" and "w = r ⋅ v" and
"r' <s r" and "t' <p t"
obtains p q i k m where "t = (q ⋅ p)⇧@(m+k)" and "r = (p ⋅ q)⇧@(m+k)" and
"t' = (q ⋅ p)⇧@k" and "r' = (p ⋅ q)⇧@m" and "v = (p ⋅ q)⇧@i ⋅ p" and
"w = (p ⋅ q)⇧@(m + i + k) ⋅ p" and "primitive (p ⋅ q)" and "q ≠ ε"
and "0 < m" and "0 < k"
proof-
let ?d = "gcd ❙|r'❙| ❙|t'❙|"
have "r' ≠ ε" "t' ≠ ε"
using assms by force+
have "0 < ?d"
using nemp_len[OF ‹r' ≠ ε›] by simp
have "❙|t❙| - ❙|t'❙| = ❙|r'❙|" "❙|r❙| - ❙|r'❙| = ❙|t'❙|"
using lenarg[OF ‹w = v ⋅ t›] lenarg[OF ‹w = r ⋅ v›]
unfolding lenarg[OF ‹w = r' ⋅ v ⋅ t'›] lenmorph by simp_all
note three_covers_per[of _ _ _ _1, unfolded cow_simps, OF assms order.refl, unfolded this period_def]
from per_root_mod_primE[OF ‹w <p take (gcd ❙|r'❙| ❙|t'❙|) w ⋅ w›]
obtain l p q where "p ⋅ q = ρ (take ?d w)" "(p ⋅ q)⇧@l ⋅ p = w" "q ≠ ε".
hence "primitive (p ⋅ q)" by auto
define e where "e = e⇩ρ (take ?d w)"
have "e ≠ 0"
unfolding e_def
using ‹w <p take (gcd ❙|r'❙| ❙|t'❙|) w ⋅ w› primroot_exp_nemp by blast
have "(p ⋅ q)⇧@e = take ?d w"
unfolding e_def ‹p ⋅ q = ρ (take ?d w)› by force
have "❙|(p ⋅ q)⇧@e❙| ≤ ❙|w❙|"
unfolding ‹(p ⋅ q)⇧@e = take ?d w›
using len_take2 by blast
have swap_e: "❙|(p ⋅ q)⇧@e❙| = ❙|(q ⋅ p)⇧@e❙|"
unfolding pow_len swap_len..
have "❙|(p ⋅ q)⇧@e❙| = ?d"
unfolding ‹(p ⋅ q)⇧@e = take ?d w›
by (rule take_len, unfold lenarg[OF ‹w = r' ⋅ v ⋅ t'›, unfolded lenmorph],
use gcd_le1_nat[OF nemp_len[OF ‹r' ≠ ε›]] trans_le_add1 in blast)
hence "(p ⋅ q)⇧@e ≤p r'"
using ‹❙|(p ⋅ q)⇧@e❙| = ?d›
unfolding pref_take_conv[of "(p ⋅ q)⇧@e" r', symmetric] using ‹w = r' ⋅ v ⋅ t'›
‹(p ⋅ q)⇧@e = take ?d w›[symmetric] gcd_le1_nat nemp_len[OF ‹r' ≠ ε›] short_take_append by metis
hence "(p ⋅ q)⇧@e = take ?d r'"
using pref_take_conv ‹❙|(p ⋅ q)⇧@e❙| = ?d› by metis
have "r' ≤p (p ⋅ q)⇧@e ⋅ r'"
using pref_keeps_per_root[OF sprefD1[OF ‹w <p take ?d w ⋅ w›]]
unfolding ‹(p ⋅ q)⇧@e = take (gcd ❙|r'❙| ❙|t'❙|) w›
using ‹w = r' ⋅ v ⋅ t'› by blast
then obtain m where "r' = (p ⋅ q)⇧@m"
using per_div[OF gcd_dvd1 period_I', OF ‹r' ≠ ε› ‹0 < ?d›, folded ‹(p ⋅ q)⇧@e = take ?d r'›]
unfolding pow_mult[symmetric] by metis
have "p ≤s (q ⋅ p) ⇧@ e"
unfolding pow_Suc'[of "q ⋅ p" "e-1", unfolded Suc_minus[OF ‹e ≠ 0›] lassoc] by blast
note ‹❙|(p ⋅ q)⇧@e❙| ≤ ❙|w❙|›[unfolded swap_e, folded ‹(p ⋅ q)⇧@l ⋅ p = w›, unfolded shift_pow]
have "(q ⋅ p)⇧@e ≤s (r' ⋅ v) ⋅ t'"
unfolding rassoc ‹w = r' ⋅ v ⋅ t'›[symmetric, folded ‹(p ⋅ q)⇧@l ⋅ p = w›, unfolded shift_pow]
using suf_prod_suf_short[OF _ ‹p ≤s (q ⋅ p) ⇧@ e› ‹ ❙|(q ⋅ p) ⇧@ e❙| ≤ ❙|p ⋅ (q ⋅ p) ⇧@ l❙|›]
unfolding pows_comm[of "(q ⋅ p)" e l] by blast
have "❙|(q ⋅ p) ⇧@ e❙| ≤ ❙|t'❙|"
using gcd_le2_nat[OF nemp_len[OF ‹t' ≠ ε›], of "❙|r'❙|", folded ‹❙|(p ⋅ q)⇧@e❙| = ?d›]
unfolding swap_len[of p q] pow_len.
have "(q ⋅ p)⇧@e ≤s t'"
unfolding ‹w = r' ⋅ v ⋅ t'›[unfolded lassoc]
using suf_prod_le[OF ‹(q ⋅ p)⇧@e ≤s (r' ⋅ v) ⋅ t'› ‹❙|(q ⋅ p) ⇧@ e❙| ≤ ❙|t'❙|›].
have "t' ≤s t' ⋅ (q ⋅ p)⇧@e"
proof (rule pref_keeps_per_root[reversed, of w])
show "w ≤s w ⋅ (q ⋅ p)⇧@e"
unfolding ‹(p ⋅ q)⇧@l ⋅ p = w›[symmetric, unfolded shift_pow] rassoc pows_comm
unfolding lassoc shift_pow[symmetric]
unfolding rassoc unfolding shift_pow by blast
show "t' ≤s w"
unfolding ‹w = r' ⋅ v ⋅ t'› lassoc by blast
qed
have t_drop: "(q ⋅ p)⇧@e = drop (❙|t'❙| - ?d) t'"
using ‹❙|(p ⋅ q)⇧@e❙| = ?d›[unfolded swap_e, symmetric] ‹(q ⋅ p)⇧@e ≤s t'›[unfolded suf_drop_conv, symmetric]
by argo
obtain k where "t' = (q ⋅ p)⇧@k"
using per_div[reversed, OF gcd_dvd2 period_I'[reversed], OF ‹t'≠ ε› ‹0 < ?d›,
folded t_drop, OF ‹t' ≤s t' ⋅ (q ⋅ p)⇧@e› ] pow_mult by metis
have "m + k ≤ l"
unfolding linorder_not_less[symmetric]
proof (rule notI)
assume "l < m + k"
hence "l + 1 ≤ m + k"
by force
from trans_le_add1[OF mult_le_mono1[OF this]]
have "(l + 1)* ❙|p ⋅ q❙| ≤ (m + k) * ❙|p⋅q❙| + ❙|v❙|".
with lenarg[OF ‹w = r' ⋅ v ⋅ t'›[folded ‹(p ⋅ q)⇧@l ⋅ p = w›, unfolded ‹t' = (q ⋅ p)⇧@k› ‹r' = (p ⋅ q)⇧@m›],
unfolded lenmorph, unfolded pow_len add.assoc[symmetric], symmetric]
show False
unfolding distrib_right add.commute[of _ "❙|v❙|"] lenmorph
unfolding distrib_left using nemp_len[OF ‹q ≠ ε›] by linarith
qed
then obtain i where "l = m + i + k"
by (metis add.assoc add.commute le_Suc_ex)
have "v = (p ⋅ q)⇧@i ⋅ p"
using ‹w = r' ⋅ v ⋅ t'›
unfolding ‹(p ⋅ q)⇧@l ⋅ p = w›[symmetric] ‹t' = (q ⋅ p)⇧@k› ‹r' = (p ⋅ q)⇧@m› ‹l = m + i + k› add_exps
rassoc cancel cancel_right
unfolding lassoc shift_pow cancel_right by simp
have "r = (p ⋅ q)⇧@(m + k)"
using ‹w = r ⋅ v› unfolding ‹(p ⋅ q)⇧@l ⋅ p = w›[symmetric] ‹v = (p ⋅ q)⇧@i ⋅ p› ‹l = m + i + k›
unfolding lassoc cancel_right add.commute[of _ k] add.assoc[symmetric] add_exps by simp
have "t = (q ⋅ p)⇧@(m + k)"
using ‹w = v ⋅ t› unfolding ‹(p ⋅ q)⇧@l ⋅ p = w›[symmetric] ‹v = (p ⋅ q)⇧@i ⋅ p› ‹l = m + i + k›
unfolding rassoc cancel add.commute[of m] add.assoc[symmetric] add_exps
unfolding shift_pow unfolding lassoc shift_pow unfolding rassoc cancel
unfolding pows_comm by simp
have "0 < m"
using ‹r' = (p ⋅ q)⇧@m› ‹r' ≠ ε› by blast
have "0 < k"
using ‹t' = (q ⋅ p)⇧@k› ‹t' ≠ ε› by blast
thm that
from that[OF ‹t = (q ⋅ p)⇧@(m + k)› ‹r = (p ⋅ q)⇧@(m + k)› ‹t' = (q ⋅ p)⇧@k› ‹r' = (p ⋅ q)⇧@m› ‹v = (p ⋅ q)⇧@i ⋅ p›
‹(p ⋅ q)⇧@l ⋅ p = w›[symmetric, unfolded ‹l = m + i + k›] ‹primitive (p ⋅ q)› ‹q ≠ ε› ‹0 < m› ‹0 < k›]
show thesis.
qed
lemma three_covers_pref_suf_pow: assumes "x ⋅ y ≤p w" and "y ⋅ x ≤s w" and "w ≤f y⇧@k" and "❙|y❙| ≤ ❙|x❙|"
shows "x ⋅ y = y ⋅ x"
using fac_marker_suf[OF fac_trans[OF pref_fac[OF ‹x ⋅ y ≤p w›] ‹w ≤f y⇧@k›]]
fac_marker_pref[OF fac_trans[OF suf_fac[OF ‹y ⋅ x ≤s w›] ‹w ≤f y⇧@k›]]
root_suf_comm'[OF _ suf_prod_long, OF _ _ ‹❙|y❙| ≤ ❙|x❙|›, of x] by presburger
subsection ‹Binary Equality Words›
definition binary_equality_word :: "binA list ⇒ bool" where
"binary_equality_word w = (∃ (g :: binA list ⇒ nat list) h. binary_code_morphism g ∧ binary_code_morphism h ∧ g ≠ h ∧ w ∈ g =⇩M h)"
lemma not_bew_baiba: assumes "❙|y❙| < ❙|v❙|" and "x ≤s y" and "u ≤s v" and
"y ⋅ x ⇧@ k ⋅ y = v ⋅ u ⇧@ k ⋅ v"
shows "commutes {x,y,u,v}"
proof-
obtain p where "y⋅p = v"
using eqdE[OF ‹y ⋅ x ⇧@ k ⋅ y = v ⋅ u ⇧@ k ⋅ v› less_imp_le[OF ‹❙|y❙| < ❙|v❙|›]] by blast
have "❙|u ⇧@ k ⋅ v❙| ≤ ❙|x ⇧@ k ⋅ y❙|"
using lenarg[OF ‹y ⋅ x ⇧@ k ⋅ y = v ⋅ u ⇧@ k ⋅ v›] ‹❙|y❙| < ❙|v❙|› unfolding lenmorph
by linarith
obtain s where "s⋅y = v"
using eqdE[reversed, OF ‹y ⋅ x ⇧@ k ⋅ y = v ⋅ u ⇧@ k ⋅ v›[unfolded lassoc] less_imp_le[OF ‹❙|y❙| < ❙|v❙|›]].
have "s ≠ ε"
using ‹❙|y❙| < ❙|v❙|› ‹s ⋅ y = v› by force
have "p ≠ ε"
using ‹❙|y❙| < ❙|v❙|› ‹y ⋅ p = v› by force
have "s ⋅ y = y ⋅ p"
by (simp add: ‹s ⋅ y = v› ‹y ⋅ p = v›)
obtain w w' q t where p_def: "p = (w'⋅w)⇧@q" and s_def: "s = (w⋅w')⇧@q"
and y_def: "y = (w⋅w')⇧@t⋅w" and "w' ≠ ε" and "primitive (w⋅w')" and ‹0 < q›
using conjug_eq_primrootE[OF ‹s ⋅ y = y ⋅ p› ‹s ≠ ε›, of thesis]
by blast
have "primitive (w'⋅w)"
using ‹primitive (w ⋅ w')› prim_conjug by auto
have "y ⋅ x ⇧@ k ⋅ y = y⋅ p ⋅ u ⇧@ k ⋅ s ⋅ y"
using ‹s ⋅ y = v› ‹y ⋅ p = v› ‹y ⋅ x ⇧@ k ⋅ y = v ⋅ u ⇧@ k ⋅ v› by auto
hence "x⇧@k = p⋅u⇧@k⋅s"
by auto
hence "x ≠ ε"
using ‹p ≠ ε› by force
have "w⋅w' ≤s x⇧@k"
using ‹x ⇧@ k = p ⋅ u ⇧@ k ⋅ s›[unfolded s_def]
unfolding pow_pos'[OF ‹0 < q›]
using sufI[of "p ⋅ u ⇧@ k ⋅ (w ⋅ w') ⇧@ (q - 1)" "w ⋅ w'" "x⇧@k", unfolded rassoc]
by argo
have "❙|w⋅w'❙| ≤ ❙|x❙|"
proof(intro leI notI)
assume "❙|x❙| < ❙|w ⋅ w'❙|"
have "x ≤s (w⋅w')⋅y"
using ‹x ≤s y› by (auto simp add: suffix_def)
have "(w'⋅w) ≤s (w⋅w')⋅y"
unfolding ‹y = (w⋅w')⇧@t⋅w› lassoc pow_comm[symmetric] suf_cancel_conv
by blast
from ruler_le[reversed, OF ‹x ≤s (w⋅w')⋅y› this
less_imp_le[OF ‹❙|x❙| < ❙|w ⋅ w'❙|›[unfolded swap_len]]]
have "x ≤s w'⋅ w".
hence "x ≤s p"
unfolding p_def pow_pos'[OF ‹0 < q›] suffix_append by blast
from root_suf_comm[OF _ suf_ext[OF this]]
have "x⋅p = p⋅x"
using pref_prod_root[OF prefI[OF ‹x ⇧@ k = p ⋅ u ⇧@ k ⋅ s›[symmetric]]] by blast
from comm_drop_exp[OF _ this[unfolded ‹p = (w' ⋅ w) ⇧@ q›]]
have "x ⋅ (w' ⋅ w) = (w' ⋅ w) ⋅ x"
using ‹0 < q› by force
from prim_comm_short_emp[OF ‹primitive (w'⋅w)› this ‹❙|x❙| < ❙|w⋅w'❙|›[unfolded swap_len]]
show False
using ‹x ≠ ε› by blast
qed
hence "w⋅w' ≤s x"
using suf_prod_le[OF suf_prod_root[OF ‹w ⋅ w' ≤s x ⇧@ k›]] by blast
from suffix_order.trans[OF this ‹x ≤s y›]
have "w ⋅ w' ≤s y".
hence "❙|w ⋅ w'❙| ≤ ❙|y❙|"
using suffix_length_le by blast
then obtain t' where "t = Suc t'"
unfolding y_def lenmorph pow_len ‹w' ≠ ε› add.commute[of _ "❙|w❙|"] nat_add_left_cancel_le
using ‹w' ≠ ε› mult_0[of "❙|w❙| + ❙|w'❙|"] npos_len[of w'] not0_implies_Suc[of t] by force
from ruler_eq_len[reversed, OF ‹w ⋅ w' ≤s y› _ swap_len, unfolded y_def this pow_Suc' rassoc]
have "w ⋅ w' = w'⋅ w"
unfolding lassoc suf_cancel_conv by blast
from comm_not_prim[OF _ ‹w' ≠ ε› this]
have "w = ε"
using ‹primitive (w ⋅ w')› by blast
hence "primitive w'"
using ‹primitive (w' ⋅ w)› by auto
have "0 < k"
using ‹❙|y❙| < ❙|v❙|› lenarg[OF ‹y ⋅ x ⇧@ k ⋅ y = v ⋅ u ⇧@ k ⋅ v›, unfolded lenmorph pow_len]
gr_zeroI by fastforce
have "y = w'⇧@t"
using y_def ‹w = ε› by force
hence "y ∈ w'*"
using rootI by blast
have "s ∈ w'*"
using s_def ‹w = ε› rootI by force
hence "v ∈ w'*"
using ‹s ⋅ y = v› ‹y ∈ w'*› add_roots by blast
have "w' ≤p x"
using ‹x⇧@k = p⋅u⇧@k⋅s›[symmetric] eq_le_pref[OF _ ‹❙|w⋅w'❙| ≤ ❙|x❙|›, of "w' ⇧@ (q -1) ⋅ u ⋅ u ⇧@ (k - 1) ⋅ s" "x ⇧@ (k - 1)"]
unfolding p_def ‹w = ε› emp_simps pow_pos[OF ‹0 < k›] pow_pos[OF ‹0 < q›] pow_pos rassoc by argo
have "x ⋅ w' = w' ⋅ x"
using ‹x ≤s y› ‹w' ≤p x› y_def[unfolded ‹w = ε› ‹t = Suc t'› emp_simps]
pref_suf_pows_comm[of w' x 0 0 0 t', unfolded pow_zero emp_simps, folded y_def[unfolded ‹w = ε› ‹t = Suc t'›, unfolded emp_simps]]
by force
hence "x ∈ w'*"
using prim_comm_exp[OF ‹primitive w'›, of x]
unfolding root_def
by metis
have "p ∈ w'*"
using ‹s ∈ w'*› ‹y ∈ w'*› ‹s ⋅ y = v›[folded ‹y ⋅ p = v›]
by (simp add: ‹s ⋅ y = y ⋅ p› ‹s ∈ w'*› ‹y ∈ w'*› ‹w ⋅ w' = w' ⋅ w› p_def s_def)
have "u⇧@k ∈ w'*"
using root_pow_root[OF ‹x ∈ w'*›, of k, unfolded ‹x⇧@k = p⋅u⇧@k⋅s›]
root_pref_cancel[OF _ ‹p ∈ w'*›] root_suf_cancel[OF _ ‹s ∈ w'*›] by blast
from prim_root_drop_exp[OF this ‹0 < k› ‹primitive w'›]
have "u ∈ w'*".
show "commutes {x,y,u,v}"
by (intro commutesI_root[of _ w'], unfold Set.ball_simps(7), simp add: ‹x ∈ w'*› ‹y ∈ w'*› ‹u ∈ w'*› ‹v ∈ w'*›)
qed
lemma not_bew_baibaib: assumes "❙|x❙| < ❙|u❙|" and "1 < i" and
"x ⋅ y⇧@i⋅ x ⋅ y⇧@i ⋅ x = u ⋅ v⇧@i⋅ u ⋅ v⇧@i ⋅ u"
shows "commutes {x,y,u,v}"
proof-
have "0 < i"
using assms(2) by auto
from lenarg[OF ‹x ⋅ y⇧@i⋅ x ⋅ y⇧@i ⋅ x = u ⋅ v⇧@i⋅ u ⋅ v⇧@i ⋅ u›]
have "2*❙|x ⋅ y⇧@i❙| + ❙|x❙| = 2*❙|u ⋅ v⇧@i❙| + ❙|u❙|"
by auto
hence "❙|u ⋅ v⇧@i❙| < ❙|x ⋅ y⇧@i❙|"
using ‹❙|x❙| < ❙|u❙|› by fastforce
hence "u ⋅ v⇧@i <p x ⋅ y⇧@i"
using assms(3) eq_le_pref less_or_eq_imp_le rassoc sprefI2 by metis
have "x⋅y⇧@i ≠ ε"
by (metis ‹u ⋅ v ⇧@ i <p x ⋅ y ⇧@ i› strict_prefix_simps(1))
have "u⋅v⇧@i ≠ ε"
using assms(1) gr_implies_not0 by blast
have "(u⋅v⇧@i) ⋅ (x⋅y⇧@i) = (x⋅y⇧@i) ⋅ (u⋅v⇧@i)"
proof(rule sq_short_per)
have eq: "(x ⋅ y ⇧@ i) ⋅ (x ⋅ y ⇧@ i) ⋅ x = (u ⋅ v ⇧@ i) ⋅ (u ⋅ v ⇧@ i) ⋅ u"
using assms(3) by auto
from lenarg[OF this]
have "❙|u ⋅ v⇧@i ⋅ u❙| < ❙|x ⋅ y⇧@i ⋅ x ⋅ y⇧@i❙|"
unfolding lenmorph using ‹❙|x❙| < ❙|u❙|› by linarith
from eq_le_pref[OF _ less_imp_le[OF this]]
have "(u ⋅ v⇧@i)⋅u ≤p (x ⋅ y⇧@i) ⋅ (x ⋅ y⇧@i)"
using eq[symmetric] unfolding rassoc by blast
hence "(u ⋅ v ⇧@ i) ⋅ (u ⋅ v⇧@i) ⋅ u ≤p (u ⋅ v ⇧@ i) ⋅ ((x ⋅ y⇧@i) ⋅ (x ⋅ y⇧@i))"
unfolding same_prefix_prefix.
from pref_trans[OF prefI[of "(x ⋅ y ⇧@ i) ⋅ (x ⋅ y ⇧@ i)" x "(x ⋅ y ⇧@ i) ⋅ (x ⋅ y ⇧@ i) ⋅ x"]
this[folded ‹(x ⋅ y ⇧@ i) ⋅ (x ⋅ y ⇧@ i) ⋅ x = (u ⋅ v ⇧@ i) ⋅ (u ⋅ v ⇧@ i) ⋅ u›],
unfolded rassoc, OF refl]
show "(x ⋅ y⇧@i)⋅(x ⋅ y⇧@i) ≤p (u ⋅ v⇧@i) ⋅ ((x ⋅ y⇧@i) ⋅ (x ⋅ y⇧@i))"
by fastforce
show "❙|u ⋅ v ⇧@ i❙| ≤ ❙|x ⋅ y ⇧@ i❙|"
using less_imp_le_nat[OF ‹❙|u ⋅ v ⇧@ i❙| < ❙|x ⋅ y ⇧@ i❙|›].
qed
obtain r m k where "x⋅y⇧@i = r⇧@k" "u⋅v⇧@i = r⇧@m" "primitive r"
using ‹(u ⋅ v ⇧@ i) ⋅ x ⋅ y ⇧@ i = (x ⋅ y ⇧@ i) ⋅ u ⋅ v ⇧@ i›[unfolded
comm_primroots[OF ‹u ⋅ v ⇧@ i ≠ ε› ‹x ⋅ y ⇧@ i ≠ ε›]]
‹u ⋅ v ⇧@ i ≠ ε› ‹x ⋅ y ⇧@ i ≠ ε› primroot_expE primroot_prim by metis
have "m < k"
using ‹❙|u ⋅ v ⇧@ i❙| < ❙|x ⋅ y ⇧@ i❙|›
unfolding strict_prefix_def ‹u ⋅ v ⇧@ i = r ⇧@ m› ‹x ⋅ y ⇧@ i = r ⇧@ k›
pow_len
by simp
have "x⋅y⇧@i = u⋅v⇧@i⋅r⇧@(k-m)"
by (simp add: ‹m < k› ‹u ⋅ v ⇧@ i = r ⇧@ m› ‹x ⋅ y ⇧@ i = r ⇧@ k› lassoc less_imp_le_nat pop_pow)
have "❙|y ⇧@ i❙| = ❙|v ⇧@ i❙| + 3 * ❙|r ⇧@ (k - m)❙|" and "❙|r❙| ≤ ❙|y⇧@(i-1)❙|"
proof-
have "❙|x ⋅ y⇧@i❙| = ❙|r⇧@(k-m)❙| + ❙|u ⋅ v⇧@i❙|"
using lenarg[OF ‹x⋅y⇧@i = u⋅v⇧@i⋅r⇧@(k-m)›]
by auto
have "❙|u❙| = 2 * ❙|r ⇧@ (k - m)❙| + ❙|x❙|"
using ‹2*❙|x ⋅ y⇧@i❙| + ❙|x❙| = 2*❙|u ⋅ v⇧@i❙| + ❙|u❙|›
unfolding ‹❙|x ⋅ y⇧@i❙| = ❙|r⇧@(k-m)❙| + ❙|u ⋅ v⇧@i❙|›
add_mult_distrib2
by simp
have "2*❙|y⇧@i❙| + 3*❙|x❙| = 2*❙|v⇧@i❙| + 3*❙|u❙|"
using lenarg[OF ‹x ⋅ y⇧@i⋅ x ⋅ y⇧@i ⋅ x = u ⋅ v⇧@i⋅ u ⋅ v⇧@i ⋅ u›]
unfolding lenmorph numeral_3_eq_3 numerals(2)
by linarith
have "2 * ❙|y ⇧@ i❙| = 2 * ❙|v ⇧@ i❙| + 3 * (2 * ❙|r ⇧@ (k - m)❙|)"
using ‹2*❙|y⇧@i❙| + 3*❙|x❙| = 2*❙|v⇧@i❙| + 3*❙|u❙|›
unfolding ‹❙|u❙| = 2 * ❙|r ⇧@ (k - m)❙| + ❙|x❙|› add_mult_distrib2
by simp
hence "2 * ❙|y ⇧@ i❙| = 2 * ❙|v ⇧@ i❙| + 2 * (3 * ❙|r ⇧@ (k - m)❙|)"
by presburger
hence "2 * ❙|y ⇧@ i❙| = 2 * (❙|v ⇧@ i❙| + (3 * ❙|r ⇧@ (k - m)❙|))"
by simp
thus "❙|y ⇧@ i❙| = ❙|v ⇧@ i❙| + 3 * ❙|r ⇧@ (k - m)❙|"
using nat_mult_eq_cancel1[of 2] zero_less_numeral
by force
hence "3 * ❙|r ⇧@ (k - m)❙| ≤ ❙|y ⇧@ i❙|"
using le_add2 by presburger
moreover have "❙|r❙| ≤ ❙|r ⇧@ (k - m)❙|"
by (metis pow_Suc pow_Suc' ‹primitive r› ‹u ⋅ v ⇧@ i <p x ⋅ y ⇧@ i›
‹x ⋅ y ⇧@ i = u ⋅ v ⇧@ i ⋅ r ⇧@ (k - m)› not_le prim_comm_short_emp
self_append_conv strict_prefix_def)
ultimately have "3 * ❙|r❙| ≤ ❙|y ⇧@ i❙|"
by (meson le_trans mult_le_mono2)
hence "3 * ❙|r❙| ≤ i*❙|y❙|"
by (simp add: pow_len)
moreover have "i ≤ 3*(i-1)"
using assms(2) by linarith
ultimately have "3*❙|r❙| ≤ 3*((i-1)*❙|y❙|)"
by (metis (no_types, lifting) le_trans mult.assoc mult_le_mono1)
hence "❙|r❙| ≤ (i-1)*❙|y❙|"
by (meson nat_mult_le_cancel1 zero_less_numeral)
thus "❙|r❙| ≤ ❙|y⇧@(i-1)❙|"
unfolding pow_len.
qed
have "❙|r❙| + ❙|y❙| ≤ ❙|y ⇧@ i❙|"
using ‹❙|r❙| ≤ ❙|y⇧@(i-1)❙|›
unfolding pow_len nat_add_left_cancel_le[of "❙|y❙|" "❙|r❙|", symmetric]
using add.commute ‹0 < i› mult_eq_if
by force
have "y⇧@i ≤s y⇧@i⋅r"
using triv_suf[of "y ⇧@ i" x, unfolded ‹x ⋅ y ⇧@ i = r ⇧@ k›,
THEN suf_prod_root].
have "y⇧@i ≤s y⇧@i⋅y"
by (simp add: suf_pow_ext')
from two_pers[reversed, OF ‹y⇧@i ≤s y⇧@i⋅r› ‹y⇧@i ≤s y⇧@i⋅y› ‹❙|r❙| + ❙|y❙| ≤ ❙|y ⇧@ i❙|›]
have "y ⋅ r = r ⋅ y".
have "x ⋅ y ⇧@ i ⋅ r = r ⋅ x ⋅ y ⇧@ i"
by (simp add: pow_comm ‹x ⋅ y ⇧@ i = r ⇧@ k› lassoc)
hence "x ⋅ r ⋅ y ⇧@ i = r ⋅ x ⋅ y ⇧@ i"
by (simp add: ‹y ⋅ r = r ⋅ y› comm_add_exp)
hence "x ⋅ r = r ⋅ x"
by auto
obtain n where "y = r⇧@n"
using ‹primitive r› ‹y ⋅ r = r ⋅ y› by blast
hence "❙|y⇧@i❙| = i*n*❙|r❙|"
by (simp add: pow_len)
hence "❙|v ⇧@ i❙| = i*n*❙|r❙| - 3 * ❙|r ⇧@ (k - m)❙|"
using ‹❙|y ⇧@ i❙| = ❙|v ⇧@ i❙| + 3 * ❙|r ⇧@ (k - m)❙|›
diff_add_inverse2 by presburger
hence "❙|v ⇧@ i❙| = (i*n - 3*(k-m))*❙|r❙|"
by (simp add: ‹❙|v ⇧@ i❙| = i * n * ❙|r❙| - 3 * ❙|r ⇧@ (k - m)❙|› ab_semigroup_mult_class.mult_ac(1) left_diff_distrib' pow_len)
have "v⇧@i ∈ r*"
using per_exp_eq[reversed, OF _ ‹❙|v ⇧@ i❙| = (i*n - 3*(k-m))*❙|r❙|›]
‹u ⋅ v ⇧@ i = r ⇧@ m› suf_prod_root triv_suf by metis
have "u ⋅ r = r ⋅ u"
using root_suf_cancel[OF rootI[of r m, folded ‹u ⋅ v ⇧@ i = r ⇧@ m›] ‹v ⇧@ i ∈ r*›]
self_root[of r] unfolding comm_root
by blast
have "v ⋅ r = r ⋅ v"
thm comm_drop_exp
using comm_drop_exp[OF ‹0 < i›,
OF comm_rootI[OF self_root ‹v⇧@i ∈ r*›]].
show ?thesis
using commutesI_root[of "{x, y, u, v}" r]
prim_comm_root[OF ‹primitive r› ‹u ⋅ r = r ⋅ u›]
prim_comm_root[OF ‹primitive r› ‹v ⋅ r = r ⋅ v›]
prim_comm_root[OF ‹primitive r› ‹x ⋅ r = r ⋅ x›]
prim_comm_root[OF ‹primitive r› ‹y ⋅ r = r ⋅ y›]
by auto
qed
theorem "¬ binary_equality_word (𝔞 ⋅ 𝔟⇧@Suc k ⋅ 𝔞 ⋅ 𝔟)"
proof
assume "binary_equality_word (𝔞 ⋅ 𝔟 ⇧@ Suc k ⋅ 𝔞 ⋅ 𝔟)"
then obtain g' h' where g'_morph: "binary_code_morphism (g' :: binA list ⇒ nat list)" and h'_morph: "binary_code_morphism h'" and "g' ≠ h'" and
msol': "(𝔞 ⋅ 𝔟 ⇧@ Suc k ⋅ 𝔞 ⋅ 𝔟) ∈ g' =⇩M h'"
using binary_equality_word_def by blast
interpret g': binary_code_morphism g'
by fact
interpret h': binary_code_morphism h'
by fact
interpret gh: two_morphisms g' h'
by (simp add: g'.morphism_axioms h'.morphism_axioms two_morphisms_def)
have "❙|g'(𝔞 ⋅ 𝔟)❙| ≠ ❙|h'(𝔞 ⋅ 𝔟)❙|"
proof
assume len: "❙|g'(𝔞 ⋅ 𝔟)❙| = ❙|h'(𝔞 ⋅ 𝔟)❙|"
hence eq1: "g'(𝔞 ⋅ 𝔟) = h'(𝔞 ⋅ 𝔟)" and eq2: "g' (𝔟⇧@k ⋅ 𝔞 ⋅ 𝔟) = h' (𝔟⇧@k ⋅ 𝔞 ⋅ 𝔟)"
using msol' eqd_eq[OF _ len, of "g' (𝔟⇧@k ⋅ 𝔞 ⋅ 𝔟)" "h' (𝔟⇧@k ⋅ 𝔞 ⋅ 𝔟) "]
unfolding min_sol_def pow_Suc pow_one g'.morph[symmetric] h'.morph[symmetric] rassoc
by blast+
hence "g' (𝔟⇧@k) = h' (𝔟⇧@k)"
by (simp add: g'.morph h'.morph)
show False
proof (cases "k = 0")
assume "k = 0"
from min_solD_min[OF msol' _ _ eq1, unfolded ‹k = 0› pow_one]
show False by simp
next
assume "k ≠ 0"
hence "g' (𝔟) = h' (𝔟)"
using ‹g' (𝔟⇧@k) = h' (𝔟⇧@k)›
unfolding g'.pow_morph h'.pow_morph using pow_eq_eq by blast
hence "g' (𝔞) = h' (𝔞)"
using ‹g'(𝔞 ⋅ 𝔟) = h'(𝔞 ⋅ 𝔟)› unfolding g'.morph h'.morph
by simp
show False
using gh.def_on_sings_eq[OF finite_2.induct[of "λ a. g'[a] = h'[a]", OF ‹g' (𝔞) = h' (𝔞)› ‹g' (𝔟) = h' (𝔟)›]]
‹g' ≠ h'› by blast
qed
qed
then have less': "❙|(if ❙|g' (𝔞 ⋅ 𝔟)❙| < ❙|h' (𝔞 ⋅ 𝔟)❙| then g' else h') (𝔞 ⋅ 𝔟)❙|
< ❙|(if ❙|g' (𝔞 ⋅ 𝔟)❙| < ❙|h' (𝔞 ⋅ 𝔟)❙| then h' else g') (𝔞 ⋅ 𝔟)❙|"
by simp
obtain g h where g_morph: "binary_code_morphism (g :: binA list ⇒ nat list)" and h_morph: "binary_code_morphism h"
and msol: "g (𝔞 ⋅ 𝔟 ⇧@ Suc k ⋅ 𝔞 ⋅ 𝔟) = h (𝔞 ⋅ 𝔟 ⇧@ Suc k ⋅ 𝔞 ⋅ 𝔟)" and less: "❙|g(𝔞 ⋅ 𝔟)❙| < ❙|h(𝔞 ⋅ 𝔟)❙|"
using that[of "(if ❙|g' (𝔞 ⋅ 𝔟)❙| < ❙|h' (𝔞 ⋅ 𝔟)❙| then g' else h')" "(if ❙|g' (𝔞 ⋅ 𝔟)❙| < ❙|h' (𝔞 ⋅ 𝔟)❙| then h' else g')", OF _ _ _ less']
g'_morph h'_morph min_solD[OF msol'] by presburger
interpret g: binary_code_morphism g
using g_morph by blast
interpret h: binary_code_morphism h
using h_morph by blast
have "g 𝔟 ≤s g (𝔞 ⋅ 𝔟)" and "h 𝔟 ≤s h (𝔞 ⋅ 𝔟)"
unfolding g.morph h.morph by blast+
from not_bew_baiba[OF less this, of k] msol
have "commutes {g 𝔟, g (𝔞 ⋅ 𝔟), h 𝔟, h (𝔞 ⋅ 𝔟)}"
unfolding g.morph h.morph g.pow_morph h.pow_morph pow_Suc rassoc by blast
hence "g 𝔟 ⋅ g (𝔞 ⋅ 𝔟) = g (𝔞 ⋅ 𝔟) ⋅ g 𝔟"
unfolding commutes_def by blast
from this[unfolded g.morph lassoc cancel_right]
show False
using g.non_comm_morph by simp
qed
end