Theory Binary_Square_Interpretation
theory Binary_Square_Interpretation
imports
Combinatorics_Words.Submonoids
Combinatorics_Words.Equations_Basic
begin
section ‹Lemmas for covered x square›
text ‹This section explores various variants of the situation when @{term "x ⋅ x"} is covered with
@{term "x⋅y⇧@k⋅u ⋅ v⋅y⇧@l⋅x"}, with @{term "y = u⋅v"}, and the displayed dots being synchronized.
›
subsection ‹Two particular cases›
lemma pref_suf_pers_short: assumes "x ≤p v ⋅ x" and "❙|v ⋅ u❙| < ❙|x❙|" and "x ≤s r ⋅ u ⋅ v ⋅ u" and "r ∈ ⟨{u,v}⟩"
shows "u⋅v = v⋅u"
proof (rule nemp_comm)
have "v ⋅ u <s x"
using suf_prod_long_less[OF _ ‹❙|v ⋅ u❙| < ❙|x❙|›, of "r ⋅ u", unfolded rassoc, OF ‹x ≤s r ⋅ u ⋅ v ⋅ u›].
assume "u ≠ ε" and "v ≠ ε"
obtain q where "x = q ⋅ v ⋅ u" and "q ≠ ε"
using ‹v ⋅ u <s x› by (auto simp add: suffix_def)
hence "q ≤s r ⋅ u"
using ‹x ≤s r ⋅ u ⋅ v ⋅ u› by (auto simp add: suffix_def)
from suf_trans[OF primroot_suf this]
have "ρ q ≤s r ⋅ u".
have "q ⋅ v = v ⋅ q"
using pref_marker[OF ‹x ≤p v⋅x›, of q ] ‹x = q ⋅ v ⋅ u› by simp
from suf_marker_per_root[OF ‹x ≤p v ⋅ x›, of q u, unfolded rassoc ‹x = q ⋅ v ⋅ u›]
have "u <p v ⋅ u"
using ‹v ≠ ε› by blast
from per_root_primroot[OF this]
comm_primroots'[OF ‹q ≠ ε› ‹v ≠ ε› ‹q ⋅ v = v ⋅ q›]
have "u ≤p ρ q ⋅ u"
by force
from gen_prim[OF ‹r ∈ ⟨{u, v}⟩›, unfolded ]
have "r ∈ ⟨{u, ρ q}⟩"
unfolding ‹ρ q = ρ v›.
from two_elem_root_suf_comm[OF ‹u ≤p ρ q ⋅ u› ‹ρ q ≤s r ⋅ u› this]
show "u ⋅ v = v ⋅ u"
using comm_primroot_conv[of _ v, folded ‹ρ q = ρ v›] by blast
qed
lemma pref_suf_pers_large_overlap:
assumes
"p ≤p x" and "s ≤s x" and "p ≤p r ⋅ p" and "s ≤s s ⋅ r" and "❙|x❙| + ❙|r❙| ≤ ❙|p❙| + ❙|s❙|"
shows "x ⋅ r = r ⋅ x"
using assms
proof (cases "r = ε")
assume "r ≠ ε" hence "r ≠ ε" by blast
have "❙|s❙| ≤ ❙|x❙|"
using ‹s ≤s x› unfolding suffix_def by force
have "❙|p❙| ≤ ❙|x❙|"
using ‹p ≤p x› by (force simp add: prefix_def)
have "❙|r❙| ≤ ❙|p❙|"
using ‹❙|x❙| + ❙|r❙| ≤ ❙|p❙| + ❙|s❙|› ‹❙|s❙| ≤ ❙|x❙|› unfolding lenmorph by linarith
have "❙|r❙| ≤ ❙|s❙|"
using ‹❙|x❙| + ❙|r❙| ≤ ❙|p❙| + ❙|s❙|› ‹❙|p❙| ≤ ❙|x❙|› unfolding lenmorph by linarith
obtain p1 ov s1 where "p1 ⋅ ov ⋅ s1 = x" and "p1 ⋅ ov = p" and "ov ⋅ s1 = s"
using pref_suf_overlapE[OF ‹p ≤p x› ‹s ≤s x›] using ‹❙|x❙| + ❙|r❙| ≤ ❙|p❙| + ❙|s❙|› by auto
have "❙|r❙| ≤ ❙|ov❙|"
using ‹❙|x❙| + ❙|r❙| ≤ ❙|p❙| + ❙|s❙|›[folded ‹p1 ⋅ ov ⋅ s1 = x› ‹p1 ⋅ ov = p› ‹ov ⋅ s1 = s›]
unfolding lenmorph by force
have "r ≤p p"
using ‹❙|r❙| ≤ ❙|p❙|›[unfolded swap_len] pref_prod_long[OF ‹p ≤p r ⋅ p›] by blast
hence "r ≤p x"
using ‹p ≤p x› by auto
have "r ≤s s"
using ‹❙|r❙| ≤ ❙|s❙|›[unfolded swap_len] pref_prod_long[reversed, OF ‹s ≤s s ⋅ r›] by blast
hence "r ≤s x"
using ‹s ≤s x› by auto
obtain k where "p ≤p r⇧@k" "0 < k"
using per_root_powE[OF per_rootI[OF ‹p ≤p r ⋅ p› ‹r ≠ ε›]] sprefD1 by metis
hence "p1 ⋅ ov ≤f r⇧@k"
unfolding ‹p1 ⋅ ov = p› by blast
obtain l where "s ≤s r⇧@ l" ‹0 < l›
using per_root_powE[reversed, OF per_rootI[reversed, OF ‹s ≤s s ⋅ r› ‹r ≠ ε›]] ssufD1 by metis
hence "ov ⋅ s1 ≤f r⇧@ l"
unfolding ‹ov ⋅ s1 = s› by blast
from per_glue_facs[OF ‹p1 ⋅ ov ≤f r⇧@ k› ‹ov ⋅ s1 ≤f r⇧@ l› ‹❙|r❙| ≤ ❙|ov❙|›, unfolded ‹p1 ⋅ ov ⋅ s1 = x›]
obtain m where "x ≤f r ⇧@ m".
show "x ⋅ r = r ⋅ x"
using root_suf_comm[OF
pref_prod_root[OF marker_fac_pref[OF ‹x ≤f r ⇧@ m› ‹r ≤p x›]]
suffix_appendI[OF ‹r ≤s x›]]..
qed simp
subsection ‹Main cases›
locale pref_suf_pers =
fixes x u v k m
assumes
x_pref: "x ≤p (v ⋅ (u ⋅ v)⇧@k) ⋅ x"
and
x_suf: "x ≤s x ⋅ (u ⋅ v)⇧@m ⋅ u"
and k_pos: "0 < k" and m_pos: "0 < m"
begin
lemma pref_suf_commute_all_commutes:
assumes "❙|u ⋅ v❙| ≤ ❙|x❙|" and "u ⋅ v = v ⋅ u"
shows "commutes {u,v,x}"
using assms
proof (cases "u ⋅ v = ε")
let ?p = "(v ⋅ (u ⋅ v)⇧@k)"
let ?s = "(u ⋅ v)⇧@m ⋅ u"
note x_pref x_suf
assume "u ⋅ v ≠ ε"
have "?p ≠ ε" and "?s ≠ ε" and "v ⋅ u ≠ ε"
using ‹u ⋅ v ≠ ε› m_pos k_pos by auto
obtain r where "u ∈ r*" and "v ∈ r*" and "primitive r"
using ‹u ⋅ v = v ⋅ u› comm_primrootE by metis
hence "r ≠ ε"
by force
have "?p ∈ r*" and "?s ∈ r*" and "v ⋅ u ∈ r*" and "u ⋅ v ∈ r*"
using ‹u ∈ r*› ‹v ∈ r*›
by (simp_all add: add_roots root_pow_root)
have "x ≤p r ⋅ x"
using ‹?p ∈ r*› ‹x ≤p ?p ⋅ x› ‹?p ≠ ε› by blast
have "v ⋅ u ≤s x"
using ruler_le[reversed, OF _ _ ‹❙|u ⋅ v❙| ≤ ❙|x❙|›[unfolded swap_len[of u]],
of "(x ⋅ (u ⋅ v) ⇧@ (m-1) ⋅ u) ⋅ v ⋅ u", OF triv_suf, unfolded rassoc, OF ‹x ≤s x ⋅ ?s›[unfolded pow_pos'[OF m_pos] rassoc]].
have "r ≤s v ⋅ u"
using ‹v ⋅ u ≠ ε› ‹v ⋅ u ∈ r*› per_root_suf by blast
have "r ≤s r ⋅ x"
using suf_trans[OF ‹r ≤s v ⋅ u› ‹v ⋅ u ≤s x›, THEN suffix_appendI] by blast
have "x ⋅ r = r ⋅ x"
using root_suf_comm[OF ‹x ≤p r ⋅ x› ‹r ≤s r ⋅ x›, symmetric].
hence "x ∈ r*"
by (simp add: ‹primitive r› prim_comm_root)
thus "commutes {u,v,x}"
using ‹u ∈ r*› ‹v ∈ r*› commutesI_root[of "{u,v,x}"] by blast
qed simp
lemma no_overlap:
assumes
len: "❙|v ⋅ (u ⋅ v)⇧@k❙| + ❙|(u ⋅ v)⇧@m ⋅ u❙| ≤ ❙|x❙|" (is "❙|?p❙| + ❙|?s❙| ≤ ❙|x❙|") and
"0 < k" "0 < m"
shows "commutes {u,v,x}"
using assms
proof (cases "u ⋅ v = ε")
note x_pref x_suf
assume "u ⋅ v ≠ ε"
have "?p ≠ ε" and "?s ≠ ε"
using ‹u ⋅ v ≠ ε› m_pos k_pos by force+
from per_lemma_pref_suf[OF per_rootI[OF ‹x ≤p ?p ⋅ x› ‹?p ≠ ε›] per_rootI[reversed, OF ‹x ≤s x ⋅ ?s› ‹?s ≠ ε›] ‹❙|?p❙| + ❙|?s❙| ≤ ❙|x❙|›]
obtain r s kp ks mw where "?p = (r ⋅ s)⇧@kp" and "?s = (s ⋅ r)⇧@ks" and "x = (r ⋅ s)⇧@mw ⋅ r" and "primitive (r ⋅ s)".
hence "ρ ?p = r ⋅ s"
using ‹v ⋅ (u ⋅ v) ⇧@k ≠ ε› comm_primroots nemp_pow_nemp pow_comm prim_self_root by metis
moreover have "ρ ?s = s ⋅ r"
using primroot_unique[OF ‹?s ≠ ε› _ ‹?s = (s ⋅ r)⇧@ks›] prim_conjug[OF ‹primitive (r ⋅ s)›] by blast
ultimately have "ρ ?p ∼ ρ ?s"
by force
from conj_pers_conj_comm[OF this k_pos m_pos]
have "u ⋅ v = v ⋅ u".
from pref_suf_commute_all_commutes[OF _ this]
show "commutes {u,v,x}"
using len by auto
qed simp
lemma no_overlap':
assumes
len: "❙|v ⋅ (u ⋅ v)⇧@k❙| + ❙|(u ⋅ v)⇧@m ⋅ u❙| ≤ ❙|x❙|" (is "❙|?p❙| + ❙|?s❙| ≤ ❙|x❙|")
and "0 < k" "0 < m"
shows "u ⋅ v = v ⋅ u"
by (rule commutesE[of "{u,v,x}"], simp_all add: no_overlap[OF assms])
lemma short_overlap:
assumes
len1: "❙|x❙| < ❙|v ⋅ (u ⋅ v)⇧@k❙| + ❙|(u ⋅ v)⇧@m ⋅ u❙|" (is "❙|x❙| < ❙|?p❙| + ❙|?s❙|") and
len2: "❙|v ⋅ (u ⋅ v)⇧@k❙| + ❙|(u ⋅ v)⇧@m ⋅ u❙| ≤ ❙|x❙| + ❙|u❙|" (is "❙|?p❙| + ❙|?s❙| ≤ ❙|x❙| + ❙|u❙|")
shows "commutes {u,v,x}"
proof (rule pref_suf_commute_all_commutes)
show "❙|u ⋅ v❙| ≤ ❙|x❙|"
using len2 unfolding pow_pos[OF k_pos] lenmorph by simp
next
note x_pref x_suf
have "❙|?p❙| ≤ ❙|x❙|"
using len2 unfolding lenmorph by linarith
hence "?p ≤p x"
using ‹x ≤p ?p ⋅ x› pref_prod_long by blast
have "❙|?s❙| ≤ ❙|x❙|"
using len2 unfolding pow_pos[OF k_pos] pow_len lenmorph by auto
hence "?s ≤s x"
using suf_prod_long[OF ‹x ≤s x ⋅ ?s›] by blast
from pref_suf_overlapE[OF ‹?p ≤p x› ‹?s ≤s x› less_imp_le[OF len1]]
obtain p1 ov s1 where "p1 ⋅ ov ⋅ s1 = x" and "p1 ⋅ ov = ?p" and "ov ⋅ s1 = ?s".
from len1[folded this]
have "ov ≠ ε"
by fastforce
have "❙|ov❙| ≤ ❙|u❙|"
using len2[folded ‹p1 ⋅ ov ⋅ s1 = x› ‹p1 ⋅ ov = ?p› ‹ov ⋅ s1 = ?s›] unfolding lenmorph by auto
then obtain s' where "ov ⋅ s' = u" and "s' ⋅ v ⋅ (u ⋅ v) ⇧@ (m -1) ⋅ u = s1"
using eqdE[OF ‹ov ⋅ s1 = ?s›[unfolded pow_pos[OF m_pos] rassoc]] by auto
from eqdE[reversed, of p1 ov "v ⋅ (u ⋅ v)⇧@(k-1)" "u ⋅ v", unfolded rassoc,
OF ‹p1 ⋅ ov = ?p›[unfolded pow_pos'[OF k_pos]] ] ‹❙|ov❙| ≤ ❙|u❙|›
have "v ⋅ (u ⋅ v) ⇧@ (k -1) ≤p p1"
unfolding lenmorph by (auto simp add: prefix_def)
then obtain q where "v ⋅ (u ⋅ v)⇧@(k-1) ⋅ q = p1"
by (force simp add: prefix_def)
show "u ⋅ v = v ⋅ u"
proof (rule sym, rule uvu_suf_uvvu)
show "s' ≤s u"
using ‹ov ⋅ s' = u› ‹ov ≠ ε› by blast
show "u ⋅ v ⋅ v ⋅ u ⋅ s' = q ⋅ u ⋅ v ⋅ u"
proof-
have "u ⋅ v ⋅ u ≤p ?s"
unfolding pow_pos[OF m_pos] rassoc pref_cancel_conv shift_pow by blast
hence "p1 ⋅ u ⋅ v ⋅ u ≤p x"
unfolding ‹p1 ⋅ ov ⋅ s1 = x›[symmetric] ‹ov ⋅ s1 = ?s› pref_cancel_conv.
hence "v ⋅ (u ⋅ v)⇧@(k-1) ⋅ q ⋅ u ⋅ v ⋅ ov ≤p x"
using ‹v ⋅ (u ⋅ v)⇧@(k-1) ⋅ q = p1› ‹ov ⋅ s' = u› by (force simp add: prefix_def)
have "v ⋅ u ≤p x"
using ‹?p ≤p x›[unfolded pow_pos[OF k_pos]] by (auto simp add: prefix_def)
have "❙|?p ⋅ v ⋅ u❙| ≤ ❙|x❙|"
using len2 unfolding pow_pos[OF m_pos] lenmorph by force
hence "?p ⋅ v ⋅ u ≤p x"
using ‹x ≤p ?p ⋅ x› ‹v ⋅ u ≤p x› pref_prod_longer by blast
hence "v ⋅ (u ⋅ v)⇧@(k-1) ⋅ u ⋅ v ⋅ v ⋅ u ≤p x"
unfolding pow_pos'[OF k_pos] rassoc.
have "❙|v ⋅ (u ⋅ v)⇧@(k-1) ⋅ u ⋅ v ⋅ v ⋅ u❙| = ❙|v ⋅ (u ⋅ v)⇧@(k-1) ⋅ q ⋅ u ⋅ v ⋅ ov❙|"
using lenarg[OF ‹p1 ⋅ ov = ?p›[folded ‹v ⋅ (u ⋅ v)⇧@(k-1) ⋅ q = p1›, unfolded pow_pos[OF k_pos] rassoc cancel]]
by force
from ruler_eq_len[OF ‹v ⋅ (u ⋅ v)⇧@(k-1) ⋅ u ⋅ v ⋅ v ⋅ u ≤p x› ‹v ⋅ (u ⋅ v)⇧@(k-1) ⋅ q ⋅ u ⋅ v ⋅ ov ≤p x› this, unfolded cancel]
have "u ⋅ v ⋅ v ⋅ u = q ⋅ u ⋅ v ⋅ ov".
thus "u ⋅ v ⋅ v ⋅ u ⋅ s' = q ⋅ u ⋅ v ⋅ u"
using ‹ov ⋅ s' = u› by auto
qed
show "q ≤s v ⋅ u"
proof (rule ruler_le[reversed])
show "q ≤s x"
proof (rule suf_trans)
show "p1 ≤s x"
using ‹p1 ⋅ ov ⋅ s1 = x›[unfolded ‹ov ⋅ s1 = ?s›] ‹x ≤s x ⋅ ?s› same_suffix_suffix by blast
show "q ≤s p1"
using ‹v ⋅ (u ⋅ v) ⇧@ (k-1) ⋅ q = p1› by auto
qed
show "v ⋅ u ≤s x"
using ‹?s ≤s x›[unfolded pow_pos'[OF m_pos] rassoc] suf_extD by metis
show "❙|q❙| ≤ ❙|v ⋅ u❙|"
using lenarg[OF ‹u ⋅ v ⋅ v ⋅ u ⋅ s' = q ⋅ u ⋅ v ⋅ u›] lenarg[OF ‹ov ⋅ s' = u›] by force
qed
qed auto
qed
lemma medium_overlap:
assumes
len1: "❙|x❙| + ❙|u❙| < ❙|v ⋅ (u ⋅ v)⇧@k❙| + ❙|(u ⋅ v)⇧@m ⋅ u❙|" (is "❙|x❙| + ❙|u❙| < ❙|?p❙| + ❙|?s❙|") and
len2: "❙|v ⋅ (u ⋅ v)⇧@k❙| + ❙|(u ⋅ v)⇧@m ⋅ u❙| < ❙|x❙| + ❙|u ⋅ v❙|" (is "❙|?p❙| + ❙|?s❙| < ❙|x❙| + ❙|u ⋅ v❙|")
shows "commutes {u,v,x}"
proof (rule pref_suf_commute_all_commutes)
show "❙|u ⋅ v❙| ≤ ❙|x❙|"
using len2 unfolding pow_pos[OF k_pos] by force
next
note x_pref x_suf
have "❙|?p❙| ≤ ❙|x❙|"
using len2 unfolding pow_pos[OF m_pos] by auto
hence "?p ≤p x"
using ‹x ≤p ?p ⋅ x› pref_prod_long by blast
hence "v ⋅ (u ⋅ v)⇧@(k-1) ⋅ u ⋅ v ⋅ v ≤p ?p ⋅ x"
using ‹x ≤p ?p ⋅ x› unfolding pow_pos'[OF k_pos] rassoc by (auto simp add: prefix_def)
have "❙|?s❙| ≤ ❙|x❙|"
using len2 unfolding pow_pos[OF k_pos] pow_len lenmorph by auto
hence "?s ≤s x"
using suf_prod_long[OF ‹x ≤s x ⋅ ?s›] by blast
then obtain p' where "p' ⋅ u ⋅ v ≤p x" and "p' ⋅ ?s = x"
unfolding pow_pos[OF m_pos] by (auto simp add: suffix_def)
have "❙|p' ⋅ u ⋅ v❙| ≤ ❙|?p ⋅ v❙|"
using len1[folded ‹p' ⋅ ?s = x›] by force
have "❙|v ⋅ (u ⋅ v)⇧@(k-1)❙| < ❙|p'❙|"
using len2[folded ‹p' ⋅ ?s = x›] unfolding pow_pos'[OF k_pos] by force
from less_imp_le[OF this]
obtain p where "v ⋅ (u ⋅ v)⇧@(k-1) ⋅ p = p'"
using ruler_le[OF ‹?p ≤p x› ‹p' ⋅ u ⋅ v ≤p x›,
unfolded pow_pos'[OF k_pos] lassoc, THEN pref_cancel_right, THEN pref_cancel_right]
unfolding lenmorph by (auto simp add: prefix_def)
have "❙|p❙| ≤ ❙|v❙|"
using ‹v ⋅ (u ⋅ v)⇧@(k-1) ⋅ p = p'› ‹❙|p' ⋅ u ⋅ v❙| ≤ ❙|?p ⋅ v❙|› unfolding pow_pos'[OF k_pos] by force
show "u ⋅ v = v ⋅ u"
proof (rule uv_fac_uvv)
show "p ⋅ u ⋅ v ≤p u ⋅ v ⋅ v"
proof (rule pref_cancel[of "v ⋅ (u ⋅ v)⇧@(k-1)"], rule ruler_le)
show "(v ⋅ (u ⋅ v) ⇧@ (k-1)) ⋅ p ⋅ u ⋅ v ≤p ?p ⋅ x"
unfolding lassoc ‹v ⋅ (u ⋅ v)⇧@(k-1) ⋅ p = p'›[unfolded lassoc]
using ‹p' ⋅ u ⋅ v ≤p x› ‹x ≤p ?p ⋅ x› unfolding pow_pos'[OF k_pos] by force
show "(v ⋅ (u ⋅ v) ⇧@ (k-1)) ⋅ u ⋅ v ⋅ v ≤p (v ⋅ (u ⋅ v) ⇧@ k) ⋅ x"
unfolding pow_pos'[OF k_pos] rassoc
using ‹v ⋅ (u ⋅ v) ⇧@ k ≤p x› by (auto simp add: prefix_def)
show "❙|(v ⋅ (u ⋅ v) ⇧@ (k-1)) ⋅ p ⋅ u ⋅ v❙| ≤ ❙|(v ⋅ (u ⋅ v) ⇧@ (k-1)) ⋅ u ⋅ v ⋅ v❙|"
using ‹v ⋅ (u ⋅ v)⇧@(k-1) ⋅ p = p'› ‹❙|p' ⋅ u ⋅ v❙| ≤ ❙|?p ⋅ v❙|› unfolding pow_pos'[OF k_pos] by force
qed
have "p ≤s x"
using ‹p' ⋅ ?s = x›[folded ‹v ⋅ (u ⋅ v)⇧@(k-1) ⋅ p = p'›] ‹x ≤s x ⋅ ?s› suf_cancel suf_extD by metis
from ruler_le[reversed, OF this ‹?s ≤s x›, unfolded pow_pos'[OF m_pos] rassoc]
show "p ≤s (u ⋅ v) ⇧@ (m-1) ⋅ u ⋅ v ⋅ u"
using ‹❙|p❙| ≤ ❙|v❙|› unfolding lenmorph by auto
show "(u ⋅ v) ⇧@ (m-1) ⋅ u ⋅ v ⋅ u ∈ ⟨{u, v}⟩"
by (simp add: gen_in hull_closed power_in)
show "p ≠ ε"
using ‹❙|v ⋅ (u ⋅ v)⇧@(k-1)❙| < ❙|p'❙|› ‹v ⋅ (u ⋅ v)⇧@(k-1) ⋅ p = p'› by force
qed
qed
thm
no_overlap
short_overlap
medium_overlap
end
thm
pref_suf_pers.no_overlap
pref_suf_pers.short_overlap
pref_suf_pers.medium_overlap
pref_suf_pers_large_overlap
section ‹Square interpretation›
text ‹In this section fundamental description is given of (the only)
possible @{term "{x,y}"}-interpretation of the square @{term "x⋅x"}, where @{term "❙|y❙| ≤ ❙|x❙|"}.
The proof is divided into several locales.
›
lemma cover_not_disjoint:
shows "primitive (𝔞⋅𝔟⋅𝔞⋅𝔟⋅𝔞⋅𝔟⋅𝔞)" (is "primitive ?x") and
"primitive (𝔞⋅𝔟)" (is "primitive ?y") and
"(𝔞⋅𝔟⋅𝔞⋅𝔟⋅𝔞⋅𝔟⋅𝔞) ⋅ (𝔞⋅𝔟) ≠ (𝔞⋅𝔟) ⋅ (𝔞⋅𝔟⋅𝔞⋅𝔟⋅𝔞⋅𝔟⋅𝔞)"
(is "?x ⋅ ?y ≠ ?y ⋅ ?x") and
"ε (𝔞⋅𝔟⋅𝔞⋅𝔟⋅𝔞⋅𝔟⋅𝔞) ⋅ (𝔞⋅𝔟⋅𝔞⋅𝔟⋅𝔞⋅𝔟⋅𝔞) (𝔟⋅𝔞⋅𝔟⋅𝔞) ∼⇩ℐ [(𝔞⋅𝔟⋅𝔞⋅𝔟⋅𝔞⋅𝔟⋅𝔞),(𝔞⋅𝔟),(𝔞⋅𝔟),(𝔞⋅𝔟⋅𝔞⋅𝔟⋅𝔞⋅𝔟⋅𝔞)]"
(is "ε ?x ⋅ ?x ?s ∼⇩ℐ [?x,?y,?y,?x]")
unfolding factor_interpretation_def
by primitivity_inspection+ force
subsection ‹Locale: interpretation›
locale square_interp =
fixes x y p s ws
assumes
non_comm: "x ⋅ y ≠ y ⋅ x" and
prim_x: "primitive x" and
y_le_x: "❙|y❙| ≤ ❙|x❙|" and
ws_lists: "ws ∈ lists {x,y}" and
nconjug: "¬ x ∼ y" and
disj_interp: "p [x,x] s ∼⇩𝒟 ws"
begin
lemma interp: "p (x⋅x) s ∼⇩ℐ ws"
using disj_interpD[OF disj_interp] by force
lemma disjoint: "p1 ≤p [x,x] ⟹ p2 ≤p ws ⟹ p ⋅ concat p1 ≠ concat p2"
using disj_interpD1[OF disj_interp].
interpretation binary_code x y
using non_comm by unfold_locales
lemmas interpret_concat = fac_interpD(3)[OF interp]
lemma p_nemp: "p ≠ ε"
using disjoint[of ε ε] by auto
lemma s_nemp: "s ≠ ε"
using disjoint[of "[x,x]" ws] interpret_concat by force
lemma x_root: "ρ x = x"
using prim_x by blast
lemma ws_nemp: "ws ≠ ε"
using bin_fst_nemp fac_interp_nemp interp by blast
lemma hd_ws_lists: "hd ws ∈ {x, y}"
using lists_hd_in_set ws_lists ws_nemp by auto
lemma last_ws_lists: "last ws ∈ {x, y}"
using lists_hd_in_set[reversed, OF ws_nemp ws_lists].
lemma kE: obtains k where "[hd ws] ⋅ [y]⇧@k ⋅ [last ws] = ws"
proof-
from list.collapse[OF ws_nemp] hd_word
obtain ws' where "ws = [hd ws] ⋅ ws'"
by metis
hence "❙|hd ws❙| ≤ ❙|x❙|"
using two_elem_cases[OF lists_hd_in_set[OF ws_nemp ws_lists]] y_le_x by blast
hence "❙|x❙| ≤ ❙|concat ws'❙|"
using lenarg[OF interpret_concat, unfolded lenmorph]
unfolding concat.simps emp_simps arg_cong[OF ‹ws = [hd ws] ⋅ ws'›, of "λ x. ❙|concat x❙|", unfolded concat_morph lenmorph]
by linarith
hence "ws' ≠ ε"
using nemp_len[OF bin_fst_nemp] by fastforce
then obtain mid_ws where "ws' = mid_ws ⋅ [last ws]"
using ‹ws = [hd ws] ⋅ ws'› append_butlast_last_id last_appendR by metis
note ‹ws = [hd ws] ⋅ ws'›[unfolded this]
fac_interpD[OF interp]
obtain p' where [symmetric]:"p ⋅ p' = hd ws" and "p' ≠ ε"
using spref_exE[OF ‹p <p hd ws›].
obtain s' where [symmetric]: "s'⋅ s = last ws" and "s' ≠ ε"
using spref_exE[reversed, OF ‹s <s last ws›].
have "p' ⋅ concat mid_ws ⋅ s' = x ⋅ x"
using ‹ws = [hd ws] ⋅ mid_ws ⋅ [last ws]›[unfolded ‹hd ws = p ⋅ p'› ‹last ws = s'⋅ s›]
‹p ⋅ (x ⋅ x) ⋅ s = concat ws› by simp
note over = prim_overlap_sqE[OF prim_x, folded this]
have "mid_ws ∈ lists {x,y}"
using ‹ws = [hd ws] ⋅ ws'› ‹ws' = mid_ws ⋅ [last ws]› append_in_lists_conv ws_lists by metis
have "x ∉ set mid_ws"
proof
assume "x ∈ set mid_ws"
then obtain r q where "concat mid_ws = r ⋅ x ⋅ q"
using concat.simps(2) concat_morph in_set_conv_decomp_first by metis
have "(p' ⋅ r) ⋅ x ⋅ (q ⋅ s') = x ⋅ x"
using ‹p' ⋅ concat mid_ws ⋅ s' = x ⋅ x›[unfolded ‹concat mid_ws = r ⋅ x ⋅ q›]
unfolding rassoc.
from prim_overlap_sqE[OF prim_x this]
show False
using ‹p' ≠ ε› ‹s' ≠ ε› by blast
qed
hence "mid_ws ∈ lists {y}"
using ‹mid_ws ∈ lists {x,y}› by force
from that sing_lists_exp[OF this]
show thesis
using ‹ws = [hd ws] ⋅ mid_ws ⋅ [last ws]› by metis
qed
lemma l_mE: obtains m u v l where "(hd ws)⋅y⇧@m⋅u = p⋅x" and "v ⋅ y⇧@l ⋅ (last ws) = x ⋅ s" and
"u⋅v = y" "u ≠ ε" "v ≠ ε" and "x ⋅ (v ⋅ u) ≠ (v ⋅ u) ⋅ x"
proof-
note fac_interpD[OF interp]
obtain k where "[hd ws] ⋅ [y]⇧@k ⋅ [last ws] = ws"
using kE.
from arg_cong[OF this, of concat, folded interpret_concat, unfolded concat_morph rassoc concat_sing' concat_sing_pow]
have "hd ws ⋅ y⇧@k ⋅ last ws = p ⋅ x ⋅ x ⋅ s".
have "❙|hd ws❙| ≤ ❙|p ⋅ x❙|"
unfolding lenmorph by (rule two_elem_cases[OF hd_ws_lists])
(use dual_order.trans[OF le_add2 y_le_x] le_add2[of "❙|x❙|"] in fast)+
from eqd[OF _ this]
obtain ya where "hd ws ⋅ ya = p ⋅ x"
using ‹hd ws ⋅ y⇧@k ⋅ last ws = p ⋅ x ⋅ x ⋅ s› by auto
have "❙|last ws❙| ≤ ❙|x❙|"
unfolding lenmorph using dual_order.trans last_ws_lists y_le_x by auto
hence "❙|last ws❙| < ❙|x ⋅ s❙|"
unfolding lenmorph using nemp_len[OF s_nemp] by linarith
from eqd[reversed, OF _ less_imp_le[OF this]]
obtain yb where "yb ⋅ (last ws) = x ⋅ s"
using ‹(hd ws) ⋅ y⇧@k ⋅ (last ws) = p ⋅ x ⋅ x ⋅ s› rassoc by metis
hence "yb ≠ ε"
using s_nemp ‹❙|last ws❙| < ❙|x ⋅ s❙|› by force
have "ya ⋅ yb = y⇧@k"
using ‹(hd ws) ⋅ y⇧@k ⋅ (last ws) = p ⋅ x ⋅ x ⋅ s›[folded ‹yb ⋅ (last ws) = x ⋅ s›, unfolded lassoc cancel_right, folded ‹(hd ws) ⋅ ya = p ⋅ x›, unfolded rassoc cancel, symmetric].
from pref_mod_pow'[OF sprefI[OF prefI[OF this]], folded this]
obtain m u where "m < k" and "u <p y" and "y⇧@m ⋅ u = ya"
using ‹yb ≠ ε› by blast
have "y⇧@m ⋅ u ⋅ (u¯⇧>y) ⋅ y⇧@(k - m - 1) = y⇧@m ⋅ y ⋅ y⇧@(k - m - 1)"
using ‹u <p y› by (auto simp add: prefix_def)
also have "... = y⇧@(m + 1 + (k-m-1))"
using rassoc add_exps pow_1 by metis
also have "... = y⇧@k"
using ‹m < k› by auto
finally obtain l v where "u⋅v = y" and "y⇧@m ⋅ u ⋅ v ⋅ y⇧@l = y⇧@k"
using ‹u <p y› lq_pref by blast
have "concat ([hd ws]⋅[y] ⇧@ m) = hd ws ⋅ y ⇧@ m"
by simp
have "v ≠ ε"
using ‹u <p y› ‹u⋅v = y› by force
have "[hd ws] ⋅ [y] ⇧@ m ≤p ws"
using ‹[hd ws] ⋅ [y]⇧@k ⋅ [last ws] = ws›[folded pop_pow[OF less_imp_le[OF ‹m < k›]]] by fastforce
from disjoint[OF _ this, of "[x]", unfolded ‹concat ([hd ws] ⋅ [y] ⇧@ m) = hd ws ⋅ y ⇧@ m›]
have "u ≠ ε"
using ‹(hd ws) ⋅ ya = p ⋅ x›[folded ‹y⇧@m ⋅ u = ya›] s_nemp by force
have "x ⋅ (v ⋅ u) ≠ (v ⋅ u) ⋅ x"
proof
assume "x ⋅ v ⋅ u = (v ⋅ u) ⋅ x"
from comm_primroots'[OF bin_fst_nemp suf_nemp[OF ‹u ≠ ε›] this, unfolded x_root]
have "x = ρ (v ⋅ u)".
thus False
using ‹u ⋅ v = y› nconjug y_le_x
using conjugI' nle_le pref_same_len primroot_emp primroot_len_le primroot_pref swap_len by metis
qed
with that[of m u "u¯⇧>y" l, OF ‹hd ws ⋅ ya = p ⋅ x›[folded ‹y ⇧@ m ⋅ u = ya›], folded ‹yb ⋅ last ws = x ⋅ s› ‹u ⋅ v = y›,
unfolded lq_triv lassoc cancel_right, OF _ _ ‹u ≠ ε› ‹v ≠ ε› this[unfolded lassoc]]
show thesis
using ‹y ⇧@ m ⋅ u ⋅ v ⋅ y ⇧@ l = y ⇧@ k›[folded ‹ya ⋅ yb = y ⇧@ k› ‹y ⇧@ m ⋅ u = ya›, unfolded rassoc cancel, folded ‹u ⋅ v = y›] by blast
qed
lemma last_ws: "last ws = x"
proof(rule ccontr)
assume "last ws ≠ x"
hence "last ws = y"
using last_ws_lists by blast
obtain l m u v where "(hd ws)⋅y⇧@m⋅u = p⋅x" and "v ⋅ y⇧@l ⋅ (last ws) = x ⋅ s" and
"u⋅v = y" and "u ≠ ε" and "v ≠ ε" and "x ⋅ v ⋅ u ≠ (v ⋅ u) ⋅ x"
using l_mE by metis
note y_le_x[folded ‹u ⋅ v = y›,unfolded swap_len[of u]]
from ‹v ⋅ y⇧@l ⋅ (last ws) = x ⋅ s›[unfolded ‹last ws = y›, folded ‹u ⋅ v = y›]
have "x ≤p (v ⋅ u)⇧@Suc l ⋅ v"
unfolding pow_Suc' rassoc using append_eq_appendI prefix_def shift_pow by metis
moreover have "(v ⋅ u) ⇧@ Suc l ⋅ v ≤p (v ⋅ u) ⋅ (v ⋅ u) ⇧@ Suc l ⋅ v"
unfolding lassoc pow_comm[symmetric] using rassoc by blast
ultimately have "x ≤p (v ⋅ u) ⋅ x"
using pref_keeps_per_root by blast
thus False
proof (cases "m = 0")
assume "m ≠ 0"
have "v ⋅ u ≤s x"
using ‹(hd ws)⋅y⇧@m⋅u = p⋅x›[folded ‹u ⋅ v = y›, unfolded pow_pos'[OF ‹m ≠ 0›[unfolded neq0_conv]] rassoc]
suf_extD[THEN suf_prod_long[OF _ ‹❙|v ⋅ u❙| ≤ ❙|x❙|›], of p "hd ws ⋅ (u ⋅ v) ⇧@ (m-1) ⋅ u", unfolded rassoc] by simp
have [symmetric]: "(v ⋅ u) ⋅ x = x ⋅ (v ⋅ u)"
using root_suf_comm'[OF ‹x ≤p (v ⋅ u) ⋅ x› ‹(v ⋅ u) ≤s x›].
thus False
using ‹x ⋅ v ⋅ u ≠ (v ⋅ u) ⋅ x› by blast
next
assume "m = 0"
thus False
proof (cases "hd ws = y")
assume "hd ws = y"
have "p ⋅ (x ⋅ x) ⋅ s = y⇧@Suc (Suc (Suc (m+l)))"
unfolding rassoc ‹v ⋅ y⇧@l ⋅ (last ws) = x ⋅ s›[unfolded ‹last ws = y›, symmetric] power_Suc2
unfolding lassoc ‹(hd ws)⋅y⇧@m⋅u = p⋅x›[unfolded ‹hd ws = y›, symmetric]
‹u ⋅ v = y›[symmetric]
by comparison
have "ρ x ∼ ρ y"
proof (rule fac_two_conjug_primroot')
show "x ≠ ε" and "y ≠ ε" using bin_fst_nemp bin_snd_nemp.
show "x ⋅ x ≤f y⇧@Suc (Suc (Suc (m+l)))"
using facI[of "x⋅x" p s,unfolded ‹p ⋅ (x ⋅ x) ⋅ s = y⇧@Suc (Suc (Suc (m+l)))›].
show "x ⋅ x ≤f x⇧@2"
unfolding pow_two by blast
show "❙|x❙| + ❙|y❙| ≤ ❙|x ⋅ x❙|"
using y_le_x unfolding lenmorph by auto
qed
thus False
unfolding x_root using nconjug y_le_x
by (metis conjug_len long_pref primroot_pref)
next
assume "hd ws ≠ y"
hence "hd ws = x"
using hd_ws_lists by auto
have "x ≤s x ⋅ u"
using ‹(hd ws)⋅y⇧@m⋅u = p⋅x›[unfolded ‹m = 0› ‹hd ws = x› pow_zero emp_simps]
by (simp add: suffix_def)
have "v ⋅ u ≤p x"
using ‹x ≤p (v ⋅ u) ⋅ x› y_le_x[folded ‹u ⋅ v = y›,unfolded swap_len[of u]]
pref_prod_long by blast
hence "❙|v ⋅ u❙| < ❙|x❙|"
using nconjug conjugI[OF _ ‹u ⋅ v = y›, of x] ‹❙|v ⋅ u❙| ≤ ❙|x❙|›
le_neq_implies_less pref_same_len by blast
have "u ⋅ v = v ⋅ u"
proof (rule pref_suf_pers_short[reversed])
from ‹x ≤p (v ⋅ u)⇧@Suc l ⋅ v›
show "x ≤p ((v ⋅ u) ⋅ v) ⋅ (u ⋅ v)⇧@l"
by comparison
show "(u ⋅ v) ⇧@ l ∈ ⟨{v, u}⟩"
by blast
qed fact+
from pref_extD[OF ‹v ⋅ u ≤p x›[folded ‹u ⋅ v = v ⋅ u›]]
have "x ⋅ u = u ⋅ x"
using ‹x ≤s x ⋅ u› suf_root_pref_comm by blast
with comm_trans[OF this ‹u ⋅ v = v ⋅ u›[symmetric] ‹u ≠ ε›]
have "x ⋅ (v ⋅ u) = (v ⋅ u) ⋅ x"
using comm_prod by blast
thus False
using ‹x ⋅ v ⋅ u ≠ (v ⋅ u) ⋅ x› by blast
qed
qed
qed
lemma rev_square_interp:
"square_interp (rev x) (rev y) (rev s) (rev p) (rev (map rev ws))"
proof (unfold_locales)
show "rev (map rev ws) ∈ lists {rev x, rev y}"
using ws_lists by force
show "❙|rev y❙| ≤ ❙|rev x❙|"
using y_le_x by simp
show "¬ (rev x) ∼ (rev y)"
by (simp add: conjug_rev_conv nconjug)
show "primitive (rev x)"
using prim_x
by (simp_all add: prim_rev_iff)
show "(rev s) [rev x, rev x] (rev p) ∼⇩𝒟 (rev (map rev ws))"
proof
show "(rev s) (concat [rev x, rev x]) (rev p) ∼⇩ℐ rev (map rev ws)"
using interp rev_fac_interp by fastforce
show "⋀p1 p2. p1 ≤p [rev x, rev x] ⟹ p2 ≤p rev (map rev ws) ⟹ rev s ⋅ concat p1 ≠ concat p2"
proof
fix p1' p2' assume "p1' ≤p [rev x, rev x]" and "p2' ≤p rev (map rev ws)" and "rev s ⋅ concat p1' = concat p2'"
obtain p1 p2 where "p1' ⋅ p1 = [rev x, rev x]" and "p2'⋅p2 = rev (map rev ws)"
using ‹p1' ≤p [rev x, rev x]› ‹p2' ≤p rev (map rev ws)› by (auto simp add: prefix_def)
hence "rev s ⋅ (concat p1' ⋅ concat p1) ⋅ rev p = concat p2' ⋅ concat p2"
unfolding concat_morph[symmetric] using ‹(rev s) (concat[rev x,rev x]) (rev p) ∼⇩ℐ rev (map rev ws)›
fac_interpD(3) by force
from this[unfolded lassoc, folded ‹rev s ⋅ concat p1' = concat p2'›, unfolded rassoc cancel]
have "concat p1 ⋅ rev p = concat p2".
hence "p ⋅ (concat (rev (map rev p1))) = concat (rev (map rev p2))"
using rev_append rev_concat rev_map rev_rev_ident by metis
have "rev (map rev p1) ≤p [x,x]"
using arg_cong[OF ‹p1' ⋅ p1 = [rev x, rev x]›, of "λ x. rev (map rev x)", unfolded map_append rev_append]
by fastforce
have "rev (map rev p2) ≤p ws"
using arg_cong[OF ‹p2'⋅p2 = rev (map rev ws)›, of "λ x. rev (map rev x)", unfolded map_append rev_append rev_map
rev_rev_ident map_rev_involution, folded rev_map] by blast
from disjoint[OF ‹rev (map rev p1) ≤p [x,x]› ‹rev (map rev p2) ≤p ws›]
show False
using ‹p ⋅ (concat (rev (map rev p1))) = concat (rev (map rev p2))› by blast
qed
qed
show "rev x ⋅ rev y ≠ rev y ⋅ rev x"
using non_comm unfolding comm_rev_iff.
qed
lemma hd_ws: "hd ws = x"
using square_interp.last_ws[reversed, OF rev_square_interp]
unfolding hd_map[OF ws_nemp]
by simp
lemma p_pref: "p <p x"
using fac_interpD(1) hd_ws interp by auto
lemma s_suf: "s <s x"
using fac_interpD(2) last_ws interp by auto
end
subsection ‹Locale with additional parameters›
locale square_interp_plus = square_interp +
fixes l m u v
assumes fst_x: "x ⋅ y⇧@m ⋅ u = p ⋅ x" and
snd_x: "v ⋅ y⇧@l ⋅ x = x ⋅ s" and
uv_y: "u ⋅ v = y" and
u_nemp: "u ≠ ε" and v_nemp: "v ≠ ε" and
vu_x_non_comm: "x ⋅ (v ⋅ u) ≠ (v ⋅ u) ⋅ x"
begin
interpretation binary_code x y
using non_comm by unfold_locales
lemma rev_square_interp_plus: "square_interp_plus (rev x) (rev y) (rev s) (rev p) (rev (map rev ws)) m l (rev v) (rev u)"
proof-
note fac_interpD[OF interp, unfolded hd_ws last_ws]
note ‹s <s x›[unfolded strict_suffix_to_prefix]
note ‹p <p x›[unfolded spref_rev_suf_iff]
interpret i: square_interp "(rev x)" "(rev y)" "(rev s)" "(rev p)" "(rev (map rev ws))"
using rev_square_interp.
show ?thesis
by standard
(simp_all del: rev_append add: rev_pow[symmetric] rev_append[symmetric],
simp_all add: fst_x snd_x uv_y v_nemp u_nemp vu_x_non_comm[symmetric, unfolded rassoc])
qed
subsubsection ‹Exactly one of the exponents is zero: impossible.›
text ‹Uses lemma @{thm pref_suf_pers_short} and exploits the symmetric interpretation.›
lemma fst_exp_zero: assumes "m = 0" and "0 < l" shows "False"
proof (rule notE[OF vu_x_non_comm])
note y_le_x[folded uv_y, unfolded swap_len[of u]]
have "x ≤p (v ⋅ (u ⋅ v) ⇧@ l) ⋅ x"
unfolding rassoc using snd_x[folded uv_y] by blast
have "v ⋅ (u ⋅ v) ⇧@ l ≠ ε"
using v_nemp by force
obtain exp where "x ≤p (v ⋅ (u ⋅ v) ⇧@ l)⇧@exp" "0 < exp"
using per_root_powE[OF per_rootI[OF ‹x ≤p (v ⋅ (u ⋅ v) ⇧@ l) ⋅ x› ‹v ⋅ (u ⋅ v) ⇧@ l ≠ ε›], of thesis] by blast
have "x ≤s x ⋅ u"
using fst_x[unfolded ‹m = 0› pow_zero emp_simps] by (simp add: suffix_def)
have "((v ⋅ u) ⋅ v) ⋅ ((u ⋅ v)⇧@(l-1)) ⋅ (v ⋅ (u ⋅ v) ⇧@ l)⇧@(exp-1) = (v ⋅ (u ⋅ v) ⇧@ l)⇧@exp"
(is "((v ⋅ u) ⋅ v) ⋅ ?suf = (v ⋅ (u ⋅ v) ⇧@ l)⇧@exp")
using ‹0 < l› ‹0 < exp› by comparison
have "v ⋅ u ≤p x"
using pref_prod_longer[OF ‹x ≤p (v ⋅ (u ⋅ v) ⇧@ l) ⋅ x›[unfolded rassoc] _ ‹❙|v ⋅ u❙| ≤ ❙|x❙|›]
unfolding pow_pos[OF ‹0 < l›] rassoc by blast
hence "❙|v ⋅ u❙| < ❙|x❙|"
using nconjug conjugI[OF _ uv_y, of x] ‹❙|v ⋅ u❙| ≤ ❙|x❙|›
le_neq_implies_less pref_same_len by blast
have "u ⋅ v = v ⋅ u"
proof (rule pref_suf_pers_short[reversed])
show "x ≤p ((v ⋅ u) ⋅ v) ⋅ ?suf"
unfolding ‹((v ⋅ u) ⋅ v) ⋅ ?suf = (v ⋅ (u ⋅ v) ⇧@ l)⇧@exp› by fact
show "((u ⋅ v)⇧@(l-1)) ⋅ (v ⋅ (u ⋅ v) ⇧@ l)⇧@(exp-1) ∈ ⟨{v,u}⟩"
by (simp add: gen_in hull_closed power_in)
qed fact+
show "x ⋅ v ⋅ u = (v ⋅ u) ⋅ x"
using root_suf_comm[OF _ ‹x ≤s x ⋅ u›] pref_keeps_per_root comm_trans[OF ‹u ⋅ v = v ⋅ u›[symmetric] _ u_nemp, symmetric] ‹v ⋅ u ≤p x› comm_prod prefI
by metis
qed
lemma snd_exp_zero: assumes "0 < m" and "l = 0" shows "False"
using square_interp_plus.fst_exp_zero[OF rev_square_interp_plus, reversed,
rotated, OF assms].
subsubsection ‹Both exponents positive: impossible›
lemma both_exps_pos: assumes "0 < m" and "0 < l" shows "False"
proof-
note fac_interpD[OF interp, unfolded hd_ws last_ws]
have "❙|p❙| ≤ ❙|x❙|" and "❙|s❙| ≤ ❙|x❙|"
using pref_len[OF sprefD1[OF ‹p <p x›]] suf_len[OF ssufD1[OF ‹s <s x›]].
have "x ≤p (v ⋅ (u ⋅ v)⇧@l) ⋅ x"
(is "x ≤p ?pref ⋅ x")
using snd_x[folded uv_y] by force
moreover have "x ≤s x ⋅ ((u ⋅ v)⇧@m ⋅ u)"
(is "x ≤s x ⋅ ?suf")
using fst_x[folded uv_y] by force
ultimately interpret pref_suf_pers x u v l m
using ‹0 < l› ‹0 < m› by unfold_locales
have "?pref ≤p x"
using snd_x[folded uv_y rassoc, symmetric] eqd[reversed, OF _ ‹❙|s❙| ≤ ❙|x❙|›] by blast
have "?suf ≤s x"
using fst_x[folded uv_y, symmetric] eqd[OF _ ‹❙|p❙| ≤ ❙|x❙|›] by blast
have in_particular: "commutes {u,v,x} ⟹ x ⋅ (v⋅u) = (v⋅u) ⋅ x"
unfolding commutes_def by (rule comm_prod) blast+
note no_overlap_comm = no_overlap[THEN in_particular] and
short_overlap_comm = short_overlap[THEN in_particular] and
medium_overlap_comm = medium_overlap[THEN in_particular] and
large_overlap_conjug = pref_suf_pers_large_overlap[OF ‹?pref ≤p x› ‹?suf ≤s x›, of "v⋅u"]
consider
(no_overlap) "❙|?pref❙| + ❙|?suf❙| ≤ ❙|x❙|" |
(short_overlap) "❙|x❙| < ❙|?pref❙| + ❙|?suf❙| ∧ ❙|?pref❙| + ❙|?suf❙| ≤ ❙|x❙| + ❙|u❙|" |
(medium_overlap) "❙|x❙| + ❙|u❙| < ❙|?pref❙| + ❙|?suf❙| ∧ ❙|?pref❙| + ❙|?suf❙| < ❙|x❙| + ❙|u ⋅ v❙|" |
(large_overlap) "❙|x❙| + ❙|v ⋅ u❙| ≤ ❙|?pref❙| + ❙|?suf❙|"
unfolding swap_len[of v] by linarith
thus False
proof (cases)
case no_overlap
then show False
using no_overlap_comm vu_x_non_comm ‹0 < l› ‹0 < m› by blast
next
case short_overlap
then show False
using short_overlap_comm vu_x_non_comm by blast
next
case medium_overlap
then show False
using medium_overlap_comm vu_x_non_comm by blast
next
case large_overlap
show False
thm large_overlap_conjug nconjug
proof (rule notE[OF vu_x_non_comm], rule large_overlap_conjug[OF _ _ large_overlap])
have "(u ⋅ v) ⇧@ (l-1) ≤p (u ⋅ v) ⇧@ Suc (l-1)"
using pref_pow_ext by blast
thus "v ⋅ (u ⋅ v) ⇧@ l ≤p (v ⋅ u) ⋅ v ⋅ (u ⋅ v) ⇧@ l"
unfolding pow_pos[OF ‹0 < l›] pow_Suc rassoc pref_cancel_conv.
show "(u ⋅ v) ⇧@ m ⋅ u ≤s ((u ⋅ v) ⇧@ m ⋅ u) ⋅ v ⋅ u"
by comparison
qed
qed
qed
thm suf_cancel_conv
end
subsection ‹Back to the main locale›
context square_interp
begin
definition u where "u = x¯⇧>(p ⋅ x)"
definition v where "v = (x ⋅ s)⇧<¯x"
lemma cover_xyx: "ws = [x,y,x]" and vu_x_non_comm: "x ⋅ (v ⋅ u) ≠ (v ⋅ u) ⋅ x" and uv_y: "u ⋅ v = y" and
px_xu: "p ⋅ x = x ⋅ u" and vx_xs: "v ⋅ x = x ⋅ s" and u_nemp: "u ≠ ε" and v_nemp: "v ≠ ε"
proof-
obtain k where ws: "[x] ⋅ [y]⇧@k ⋅ [x] = ws"
using kE[unfolded hd_ws last_ws].
obtain m u' v' l where "x ⋅ y ⇧@ m ⋅ u' = p ⋅ x" and "v' ⋅ y ⇧@ l ⋅ x = x ⋅ s" and "u' ⋅ v' = y"
and "u' ≠ ε" and "v' ≠ ε" and "x ⋅ v' ⋅ u' ≠ (v' ⋅ u') ⋅ x"
using l_mE[unfolded hd_ws last_ws].
then interpret square_interp_plus x y p s ws l m u' v'
by (unfold_locales)
have "m = 0" and "l = 0" and "y ≠ ε"
using both_exps_pos snd_exp_zero fst_exp_zero ‹u' ⋅ v' = y› ‹u' ≠ ε› by blast+
have "u' = u"
unfolding u_def
using conjug_lq[OF fst_x[unfolded ‹m = 0› pow_zero emp_simps, symmetric]].
have "v' = v"
unfolding v_def
using conjug_lq[reversed, OF snd_x[unfolded ‹l = 0› pow_zero emp_simps, symmetric]].
have "x ⋅ y ⇧@ m ⋅ (u' ⋅ v') ⋅ y⇧@l ⋅ x = concat ws"
unfolding interpret_concat[symmetric] using fst_x snd_x by force
from this[folded ws, unfolded ‹u' ⋅ v' = y› ‹m = 0› ‹l = 0› pow_zero emp_simps]
have "k = 1"
unfolding eq_pow_exp[OF ‹y ≠ ε›, of k 1, symmetric] pow_1 concat_morph concat_pow
by simp
from ws[unfolded this pow_1]
show "ws = [x,y,x]" by simp
show "u ⋅ v = y"
unfolding ‹u' = u›[symmetric] ‹v' = v›[symmetric] by fact+
show "p ⋅ x = x ⋅ u"
using ‹x ⋅ y ⇧@ m ⋅ u' = p ⋅ x›[unfolded ‹m = 0› ‹u' = u› pow_zero emp_simps, symmetric].
show " v ⋅ x = x ⋅ s"
using ‹v' ⋅ y ⇧@ l ⋅ x = x ⋅ s›[unfolded ‹l = 0› ‹v' = v› pow_zero emp_simps].
show "x ⋅ (v ⋅ u) ≠ (v ⋅ u) ⋅ x"
using ‹x ⋅ v' ⋅ u' ≠ (v' ⋅ u') ⋅ x›[unfolded ‹u' = u› ‹v' = v›].
show "u ≠ ε" and "v ≠ ε"
using ‹u' ≠ ε› ‹v' ≠ ε› unfolding ‹u' = u› ‹v' = v›.
qed
lemma cover: "x ⋅ y ⋅ x = p ⋅ x ⋅ x ⋅ s"
using interpret_concat cover_xyx by auto
lemma conjug_facs: "ρ u ∼ ρ v"
proof-
note sufI[OF px_xu]
have "u ≠ ε"
using p_nemp px_xu by force
obtain expu where "x <s u⇧@ expu" "0 < expu"
using per_root_powE[reversed, OF per_rootI[reversed, OF ‹ x ≤s x ⋅ u› ‹u ≠ ε›]].
hence "x ≤f u⇧@ expu"
using ssufD1 by blast
note prefI[OF vx_xs[symmetric]]
have "v ≠ ε"
using s_nemp vx_xs by force
obtain expv where "x <p v⇧@expv" "0 < expv"
using per_root_powE[OF per_rootI[OF ‹x ≤p v ⋅ x› ‹v ≠ ε›]].
hence "x ≤f v⇧@expv" by blast
show "ρ u ∼ ρ v"
proof(rule fac_two_conjug_primroot'[OF ‹x ≤f u⇧@expu› ‹x ≤f v⇧@expv› ‹u ≠ ε› ‹v ≠ ε›])
show "❙|u❙| + ❙|v❙| ≤ ❙|x❙|"
using y_le_x[folded uv_y, unfolded lenmorph] by fastforce
qed
qed
term square_interp.v
lemma bin_sq_interpE: obtains r t m k l
where "(t ⋅ r)⇧@k = u" and "(r ⋅ t)⇧@l = v" and
"(r ⋅ t)⇧@m ⋅ r = x" and "(t ⋅ r)⇧@k ⋅ (r ⋅ t)⇧@ l = y"
and "(r ⋅ t)⇧@k = p" and "(t ⋅ r)⇧@ l = s" and "r ⋅ t ≠ t ⋅ r" and
"0 < k" and "0 < m" and "0 < l"
proof-
obtain r t k m where "(r ⋅ t)⇧@ k = p" and "(t ⋅ r)⇧@ k = u" and "(r ⋅ t)⇧@m ⋅ r = x" and
"t ≠ ε" and "0 < k" and "primitive (r ⋅ t)"
using conjug_eq_primrootE[OF px_xu p_nemp].
have "t ⋅ r = ρ u"
using prim_conjug[OF ‹primitive (r ⋅ t)›, THEN primroot_unique[OF u_nemp], OF conjugI' ‹(t ⋅ r)⇧@k = u›[symmetric]]..
have "0 < m"
proof (rule ccontr)
assume "¬ 0 < m"
hence "x = r" using ‹(r ⋅ t)⇧@m ⋅ r = x› by simp
show False
using ‹0 < k› ‹(r ⋅ t) ⇧@ k = p› ‹x = r› comp_pows_pref_zero p_pref by blast
qed
from ‹(r ⋅ t)⇧@m ⋅ r = x›[unfolded pow_pos[OF ‹0 < m›]]
have "r ⋅ t ≤p x"
by auto
have "r ⋅ t = ρ v"
proof (rule ruler_eq_len[of "ρ v" "x" "r ⋅ t", symmetric])
have "❙|ρ v❙| ≤ ❙|x❙|"
unfolding conjug_len[OF conjug_facs, symmetric] ‹t ⋅ r = ρ u›[symmetric]
unfolding ‹(r ⋅ t)⇧@m ⋅ r = x›[symmetric] pow_pos[OF ‹0 < m›]
lenmorph pow_len by auto
from ruler_le[OF _ _ this, of "v ⋅ x"]
show "ρ v ≤p x"
using vx_xs prefI prefix_prefix primroot_pref v_nemp by metis
show "r ⋅ t ≤p x" by fact
show "❙|ρ v❙| = ❙|r ⋅ t❙|"
unfolding conjug_len[OF conjug_facs, symmetric, folded ‹t ⋅ r = ρ u›] lenmorph by simp
qed
then obtain l where "(r ⋅ t)⇧@ l = v" and "0 < l"
using primroot_expE v_nemp by metis
have "(t ⋅ r)⇧@ l = s"
using vx_xs[folded ‹(r ⋅ t)⇧@m ⋅ r = x› ‹(r ⋅ t)⇧@ l = v›, unfolded lassoc pows_comm[of _ _ m],
unfolded rassoc cancel, unfolded shift_pow cancel].
have "r ⋅ t ≠ t ⋅ r"
proof
assume "r ⋅ t = t ⋅ r"
hence aux: "r ⋅ (t ⋅ r) ⇧@ e = (t ⋅ r) ⇧@ e ⋅ r" for e
by comparison
have "x ⋅ (v ⋅ u) = (v ⋅ u) ⋅ x"
unfolding ‹(t ⋅ r) ⇧@ k = u›[symmetric] ‹(r ⋅ t) ⇧@ l = v›[symmetric]
unfolding ‹(r ⋅ t)⇧@m ⋅ r = x›[symmetric] add_exps[symmetric] ‹r ⋅ t = t ⋅ r› aux rassoc
unfolding lassoc cancel_right add_exps[symmetric]
by (simp add: add.commute)
thus False
using vu_x_non_comm by blast
qed
show thesis
using that[OF ‹(t ⋅r)⇧@ k = u› ‹(r ⋅ t) ⇧@ l = v› ‹(r ⋅ t)⇧@m ⋅ r = x›
uv_y[folded ‹(t ⋅r)⇧@ k = u› ‹(r ⋅ t) ⇧@ l = v›] ‹(r ⋅ t) ⇧@ k = p› ‹(t ⋅ r) ⇧@ l = s› ‹r ⋅ t ≠ t ⋅ r›
‹0 < k› ‹0 < m› ‹0 < l›].
qed
end
subsection ‹Locale: Extendable interpretation›
text ‹Further specification follows from the assumption that the interpretation is extendable,
that is, the covered @{term "x⋅x"} is a factor of a word composed of @{term "{x,y}"}. Namely, @{term u} and @{term v} are then conjugate by @{term x}.›
locale square_interp_ext = square_interp +
assumes p_extend: "∃ pe. pe ∈ ⟨{x,y}⟩ ∧ p ≤s pe" and
s_extend: "∃ se. se ∈ ⟨{x,y}⟩ ∧ s ≤p se"
begin
lemma s_pref_y: "s ≤p y"
proof-
obtain sy ry eu ev ex
where "(ry ⋅ sy)⇧@eu = u" and "(sy ⋅ ry)⇧@ ev = v" and
"(sy ⋅ ry)⇧@ eu = p" and "(ry ⋅ sy)⇧@ ev = s" and
"(sy ⋅ ry)⇧@ ex ⋅ sy = x" and "sy ⋅ ry ≠ ry ⋅ sy" and
"0 < eu" and "0 < ev" and "0 < ex"
using bin_sq_interpE.
obtain se where "se ∈ ⟨{x,y}⟩" and "s ≤p se"
using s_extend by blast
hence "se ≠ ε" using s_nemp by force
from ‹(sy ⋅ ry)⇧@ ex ⋅ sy = x›
have "sy ⋅ ry ≤p x"
unfolding pow_pos[OF ‹0 < ex›] rassoc by force
have "x ≤p se ∨ y ≤p se"
using ‹se ≠ ε› hull.cases[OF ‹se ∈ ⟨{x,y}⟩›, of "x ≤p se ∨ y ≤p se"]
prefix_append triv_pref two_elem_cases by blast
moreover have "¬ x ≤p se"
proof
assume "x ≤p se"
from ruler_eq_len[of "sy ⋅ ry" se "ry ⋅ sy", OF pref_trans[OF ‹sy ⋅ ry ≤p x› this]]
show False
using ‹s ≤p se›[folded ‹(ry ⋅ sy)⇧@ ev = s›[unfolded pow_pos[OF ‹0 < ev›]]] ‹sy ⋅ ry ≠ ry ⋅ sy› by (force simp add: prefix_def)
qed
ultimately have y_pref_se: "y ≤p se" by blast
from ruler_le[OF ‹s ≤p se› this]
show "s ≤p y"
using lenarg[OF vx_xs] unfolding uv_y[symmetric] lenmorph by linarith
qed
lemma rev_square_interp_ext: "square_interp_ext (rev x) (rev y) (rev s) (rev p) (rev (map rev ws))"
proof-
interpret i: square_interp "(rev x)" "(rev y)" "(rev s)" "(rev p)" "(rev (map rev ws))"
using rev_square_interp.
show ?thesis
proof
show "∃pe. pe ∈ ⟨{rev x, rev y}⟩ ∧ rev s ≤s pe"
using s_pref_y unfolding pref_rev_suf_iff by blast
obtain pe where "pe ∈ ⟨{x, y}⟩" and "p ≤s pe"
using p_extend by blast
hence "rev pe ∈ ⟨{rev x, rev y}⟩"
by (simp add: rev_hull rev_in_conv)
thus "∃se. se ∈ ⟨{rev x, rev y}⟩ ∧ rev p ≤p se"
using ‹p ≤s pe›[unfolded suf_rev_pref_iff prefix_def] rev_rev_ident by blast
qed
qed
lemma p_suf_y: "p ≤s y"
proof-
interpret i: square_interp_ext "(rev x)" "(rev y)" "(rev s)" "(rev p)" "(rev (map rev ws))"
using rev_square_interp_ext.
from i.s_pref_y[reversed]
show "p ≤s y".
qed
theorem bin_sq_interp_extE: obtains r t k m where "(r ⋅ t)⇧@m ⋅ r = x" and "(t ⋅ r)⇧@k ⋅ (r ⋅ t)⇧@ k = y"
"(r ⋅ t)⇧@ k = p" and "(t ⋅ r)⇧@ k = s" and "r ⋅ t ≠ t ⋅ r" and "u = s" and "v = p" and "❙|p❙| = ❙|s❙|" and
"0 < k" and "0 < m"
proof-
obtain r t k k' m
where u: "(t ⋅ r)⇧@ k = u" and v: "(r ⋅ t)⇧@ k' = v" and
p: "(r ⋅ t)⇧@ k = p" and s: "(t ⋅ r)⇧@ k' = s" and
x: "(r ⋅ t)⇧@ m ⋅ r = x" and code: "r ⋅ t ≠ t ⋅ r" and
"0 < k'" "0 < m" "0 < k"
using bin_sq_interpE.
have "❙|u ⋅ v❙| = ❙|s ⋅ p❙|"
using lenarg[OF px_xu, unfolded lenmorph] lenarg[OF vx_xs, unfolded lenmorph] by simp
hence "u ⋅ v = s ⋅ p"
unfolding uv_y using s_pref_y p_suf_y by (auto simp add: prefix_def suffix_def)
note eq = ‹u ⋅ v = s ⋅ p›[unfolded ‹(t ⋅ r)⇧@ k = u›[symmetric] ‹(r ⋅ t)⇧@ k' = v›[symmetric],
unfolded ‹(t ⋅ r)⇧@ k' = s›[symmetric] ‹(r ⋅ t)⇧@ k = p›[symmetric]]
from pows_comm_comm[OF this]
have "k = k'"
using ‹r ⋅ t ≠ t ⋅ r› eqd_eq(1)[OF _ swap_len, of t r] by fastforce
have "❙|p❙| = ❙|s❙|"
using lenarg[OF p] lenarg[OF s] unfolding ‹k = k'› pow_len lenmorph add.commute[of "❙|r❙|"] by fastforce
thus thesis
using that[OF x uv_y[folded u v ‹k = k'›] p s[folded ‹k = k'›] code _ _ _ ‹0 < k› ‹0 < m›] u v p s unfolding ‹k = k'› by argo
qed
lemma ps_len: "❙|p❙| = ❙|s❙|" and p_eq_v: "p = v" and s_eq_u: "s = u"
using bin_sq_interp_extE by blast+
lemma v_x_x_u: "v ⋅ x = x ⋅ u"
using vx_xs unfolding s_eq_u.
lemma sp_y: "s ⋅ p = y"
using p_eq_v s_eq_u uv_y by auto
lemma p_x_x_s: "p ⋅ x = x ⋅ s"
by (simp add: px_xu s_eq_u)
lemma xxy_root: "x ⋅ x ⋅ y = (x ⋅ p) ⋅ (x ⋅ p)"
using p_x_x_s sp_y by force
theorem sq_ext_interp: "ws = [x, y, x]" "s ⋅ p = y" "p ⋅ x = x ⋅ s"
using cover_xyx sp_y p_x_x_s.
end
theorem bin_sq_interpE:
assumes "x ⋅ y ≠ y ⋅ x" and "primitive x" and "❙|y❙| ≤ ❙|x❙|" and "ws ∈ lists {x, y}" and "¬ x ∼ y" and
"p [x,x] s ∼⇩𝒟 ws"
obtains r t m k l where "(r ⋅ t)⇧@ m ⋅ r = x" and "(t ⋅ r)⇧@ k ⋅ (r ⋅ t)⇧@l = y"
"(r ⋅ t)⇧@ k = p" and "(t ⋅ r)⇧@ l = s" and "r ⋅ t ≠ t ⋅ r" and "0 < k" "0 < m" "0 < l"
using square_interp.bin_sq_interpE[OF square_interp.intro, OF assms, of thesis].
theorem bin_sq_interp:
assumes "x ⋅ y ≠ y ⋅ x" and "primitive x" and "❙|y❙| ≤ ❙|x❙|" and "ws ∈ lists {x, y}" and "¬ x ∼ y" and
"p [x,x] s ∼⇩𝒟 ws"
shows "ws = [x,y,x]"
using square_interp.cover_xyx[OF square_interp.intro, OF assms].
theorem bin_sq_interp_extE:
assumes "x ⋅ y ≠ y ⋅ x" and "primitive x" and "❙|y❙| ≤ ❙|x❙|" and "ws ∈ lists {x, y}" and "¬ x ∼ y" and
"p [x,x] s ∼⇩𝒟 ws" and
p_extend: "∃ pe. pe ∈ ⟨{x,y}⟩ ∧ p ≤s pe" and
s_extend: "∃ se. se ∈ ⟨{x,y}⟩ ∧ s ≤p se"
obtains r t m k where "(r ⋅ t)⇧@ m ⋅ r = x" and "(t ⋅ r)⇧@ k ⋅ (r ⋅ t)⇧@ k = y"
"(r ⋅ t)⇧@ k = p" and "(t ⋅ r)⇧@ k = s" and "r ⋅ t ≠ t ⋅ r" and "0 < k" and "0 < m"
using square_interp_ext.bin_sq_interp_extE[OF square_interp_ext.intro, OF square_interp.intro square_interp_ext_axioms.intro, OF assms, of thesis].
end