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 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_pows_comm 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 pow_add pow_list_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_pows_comm[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)"
by simp
from eq[unfolded conjunct1[OF one_one] conjunct2[OF one_one] pow_list_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_pows_comm[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
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_pos2[OF ‹0 < m›, symmetric] ‹p' = ρ v⇧@m›[symmetric] ‹u ⋅ p' = p ⋅ u› suffix_def by force
thus "u ⋅ v = v ⋅ u"
using ‹w ∈ ⟨{u, v}⟩› by mismatch
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 force
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 pow_add ‹(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_in sing_gen_primroot
unfolding commutes_def
by metis
lemma commutes_primroot: assumes "commutes A"
obtains r where "⋀x. x ∈ A ⟹ x ∈ ⟨{r}⟩" and "primitive r"
by (cases "∀ x ∈ A. x = ε", fast)
(use assms[unfolded commutes_def] comm_primroots emp_in sing_gen_primroot
primroot_prim in 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. x ∈ A ⟹ x ∈ ⟨{t}⟩) ⟹ commutes A"
by (meson comm_rootI commutesI)
lemma commutesI_ex_root: "∃ t. ∀ x ∈ A. x ∈ ⟨{t}⟩ ⟹ commutes A"
by fast
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}⟩"
by force
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 sing_gen_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 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
from prod_cl[OF singletonI this]
show "ws ∈ ⟨{[a,b]}⟩"
unfolding *[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 pow_add rassoc spref_cancel_conv unfolding pow_list_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
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_pos2[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 eq_conjug_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 eq_conjug_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_primroot[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_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_pos2[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 pow_add[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_not0[OF ‹r' ≠ ε›]] trans_le_add1 in blast)
hence "(p ⋅ q)⇧@e ≤p r'"
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[OF nemp_len_not0[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_Suc2[of "e-1" "q ⋅ p", 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 e "(q ⋅ p)" l] by blast
have "❙|(q ⋅ p) ⇧@ e❙| ≤ ❙|t'❙|"
using gcd_le2_nat[OF nemp_len_not0[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› pow_add
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] pow_add 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] pow_add
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_generator :: "binA list ⇒ bool" where
"binary_equality_generator w ≡ (set w = UNIV) ∧ (∃ (g :: binA list ⇒ nat list) h. binary_code_morphism g ∧ binary_code_morphism h ∧ g ≠ h ∧ w ∈ g =⇩M h)"
definition canonical_binary_equality_generator :: "binA list ⇒ bool" where
"canonical_binary_equality_generator w = (∃ (g :: binA list ⇒ nat list) h. binary_code_morphism g ∧ binary_code_morphism h ∧ w ∈ g =⇩M h ∧ ❙|h 𝔞❙| < ❙|g 𝔞❙| ∧ ❙|g 𝔟❙| < ❙|h 𝔟❙| ∧ ❙|g 𝔞❙| ≤ ❙|h 𝔟❙|)"
lemma begE: assumes "binary_equality_generator w"
obtains g h where "binary_code_morphism (g :: binA list ⇒ nat list)" and "binary_code_morphism h" and "g ≠ h" and "w ∈ g =⇩M h" and "set w = UNIV"
using assms binary_equality_generator_def by auto
lemma cbegE: assumes "canonical_binary_equality_generator w"
obtains g h where "binary_code_morphism (g :: binA list ⇒ nat list)" and "binary_code_morphism h" and "w ∈ g =⇩M h" and "❙|h 𝔞❙| < ❙|g 𝔞❙|" and "❙|g 𝔟❙| < ❙|h 𝔟❙|" and "❙|g 𝔞❙| ≤ ❙|h 𝔟❙|"
using assms canonical_binary_equality_generator_def by auto
lemma cbeg_is_beg: assumes "canonical_binary_equality_generator w" shows "binary_equality_generator w"
proof-
from cbegE[OF assms]
obtain g h where gh: "binary_code_morphism (g :: binA list ⇒ nat list)" "binary_code_morphism h" "w ∈ g =⇩M h" and "❙|h 𝔞❙| < ❙|g 𝔞❙|" "❙|g 𝔟❙| < ❙|h 𝔟❙|" "❙|g 𝔞❙| ≤ ❙|h 𝔟❙|".
interpret g: binary_code_morphism g
by fact
interpret h: binary_code_morphism h
by fact
interpret two_binary_morphisms g h
using two_binary_morphisms_def two_morphisms_def g.morphism_axioms h.morphism_axioms by blast
have "g ≠ h"
using ‹❙|h 𝔞❙| < ❙|g 𝔞❙|› by blast
have "set w = UNIV"
using ‹❙|h 𝔞❙| < ❙|g 𝔞❙|› ‹❙|g 𝔟❙| < ❙|h 𝔟❙|› solution_UNIV[OF min_solD'[OF ‹w ∈ g =⇩M h›] min_solD[OF ‹w ∈ g =⇩M h›] bin_induct[of "λ c. g[c] ≠ h[c]"]] by force
then show "binary_equality_generator w"
unfolding binary_equality_generator_def using gh ‹g ≠ h› by blast
qed
lemma beg_productE: assumes "binary_equality_generator (u⋅v)" and "u ≠ ε" and "v ≠ ε"
obtains g h where "binary_code_morphism (g :: binA list ⇒ nat list)" and "binary_code_morphism h" and "g ≠ h" and " (u⋅v) ∈ g =⇩M h" and "❙|g u❙| < ❙|h u❙|" and "❙|h v❙| < ❙|g v❙|"
proof-
from begE[OF assms(1)]
obtain g h where gh: "binary_code_morphism (g :: binA list ⇒ nat list)" "binary_code_morphism h" "g ≠ h" "(u ⋅ v) ∈ g =⇩M h".
interpret g: binary_code_morphism g
by fact
interpret h: binary_code_morphism h
by fact
have "❙|g u❙| ≠ ❙|h u❙|"
using min_solD_min[OF ‹(u ⋅ v) ∈ g =⇩M h› ‹u ≠ ε› triv_pref] ‹v ≠ ε› eqd_eq(1)[OF min_solD[OF ‹(u ⋅ v) ∈ g =⇩M h›, unfolded g.morph h.morph]] by blast
let ?g = "if ❙|g u❙| ≤ ❙|h u❙| then g else h"
let ?h = "if ❙|g u❙| ≤ ❙|h u❙| then h else g"
have "?g ≠ ?h" "binary_code_morphism ?g" "binary_code_morphism ?h" "(u⋅v) ∈ ?g =⇩M ?h"
using gh by (simp_all add: min_sol_sym)
interpret g': binary_code_morphism ?g
by fact
interpret h': binary_code_morphism ?h
by fact
have "❙|?g u❙| < ❙|?h u❙|"
using ‹❙|g u❙| ≠ ❙|h u❙|› by simp
with lenarg[OF min_solD[OF ‹(u ⋅ v) ∈ ?g =⇩M ?h›, unfolded g'.morph h'.morph]]
have "❙|?h v❙| < ❙|?g v❙|"
unfolding lenmorph by linarith
show thesis
by (rule that[of ?g ?h]) fact+
qed
lemma bew_baiba_eq': 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_pos2[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_pos2[OF ‹0 < q›] suffix_append by blast
from root_suf_comm[OF _ suf_ext[OF this]]
have "x⋅p = p⋅x"
using pref_pow_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_Suc2 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]
by (intro gr_zeroI) force
have "y = w'⇧@t"
using y_def ‹w = ε› by force
hence "y∈ ⟨{w'}⟩"
by blast
have "s ∈ ⟨{w'}⟩"
using s_def ‹w = ε› by blast
hence "v ∈ ⟨{w'}⟩"
using ‹s ⋅ y = v› ‹y ∈ ⟨{w'}⟩› 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› unfolding y_def[unfolded ‹w = ε› ‹t = Suc t'› emp_simps]
using suf_prod_root[THEN suf_root_pref_comm] by meson
from prim_comm_exp[OF ‹primitive w'› this]
have "x ∈ ⟨{w'}⟩"
unfolding sing_gen_pow_ex_conv by blast
have "p ∈ ⟨{w'}⟩"
using ‹s ∈ ⟨{w'}⟩› ‹y ∈ ⟨{w'}⟩› ‹s ⋅ y = v›[folded ‹y ⋅ p = v›] ‹w ⋅ w' = w' ⋅ w›
unfolding p_def s_def by argo
have "v ⋅ u⇧@k ⋅ v ∈ ⟨{w'}⟩"
unfolding ‹y ⋅ x ⇧@ k ⋅ y = v ⋅ u ⇧@ k ⋅ v›[symmetric]
using ‹y ∈ ⟨{w'}⟩› ‹v ∈ ⟨{w'}⟩› hull_closed power_in[OF ‹x ∈ ⟨{w'}⟩›] by meson
have "u⇧@k ∈ ⟨{w'}⟩"
using sing_gen_pref_cancel[OF ‹v ⋅ u⇧@k ⋅ v ∈ ⟨{w'}⟩› ‹v ∈ ⟨{w'}⟩›] sing_gen_suf_cancel[OF _ ‹v ∈ ⟨{w'}⟩›] by blast
from prim_root_drop_exp[OF this ‹0 < k› ‹primitive w'›]
have "u ∈ ⟨{w'}⟩".
have "∀x∈{x,y,u,v}. x ∈ ⟨{w'}⟩"
using ‹x ∈ ⟨{w'}⟩› ‹y ∈ ⟨{w'}⟩› ‹u ∈ ⟨{w'}⟩› ‹v ∈ ⟨{w'}⟩› by blast
then show "commutes {x,y,u,v}"
using commutesI_ex_root by auto
qed
lemma bew_baiba_eq: assumes "y ⋅ x ≠ v ⋅ u" and
"y ⋅ x ⇧@ (k+1) ⋅ y ⋅ x = v ⋅ u ⇧@ (k+1) ⋅ v ⋅ u"
shows "commutes {x,y,u,v}"
proof-
have eq':"(y ⋅ x) ⋅ x ⇧@ k ⋅ y ⋅ x = (v ⋅ u)⋅ u ⇧@ k ⋅ v ⋅ u" and
eq: "(y ⋅ x ⇧@ (k+1)) ⋅ y ⋅ x = (v ⋅ u ⇧@ (k+1)) ⋅ v ⋅ u" and
perm: "{u, v ⋅ u, x, y ⋅ x} = {x, y ⋅ x, u, v ⋅ u}"
using assms(2) unfolding rassoc by (simp_all add: insert_commute)
from eqd_eq(1)[reversed,OF eq]
have "❙|y ⋅ x❙| ≠ ❙|v ⋅ u❙|"
using assms(1) by blast
hence "commutes {x, y ⋅ x, u, v ⋅ u}"
using bew_baiba_eq'[OF _ triv_suf triv_suf eq']
bew_baiba_eq'[OF _ triv_suf triv_suf eq'[symmetric], unfolded perm] by linarith
from commutes_root[OF this]
obtain t where roots: "⋀ z. z ∈{x, y ⋅ x, u, v ⋅ u} ⟹ z ∈ ⟨{t}⟩"
by blast
have "y ∈ ⟨{t}⟩"
using roots[of x] roots[of "y⋅x"] by force
have "v ∈ ⟨{t}⟩"
using roots[of u] roots[of "v⋅u"] by force
have "∀ z ∈ {x, y, u, v}. z ∈ ⟨{t}⟩"
using roots[of u] roots[of x] ‹v ∈ ⟨{t}⟩› ‹y ∈ ⟨{t}⟩› by blast
thus "commutes {x,y,u,v}"
using commutesI_ex_root[of "{x, y ⋅ x, u, v ⋅ u}"] by auto
qed
lemmas less_mult_le [intro] = mult_le_mono1[OF Suc_leI, unfolded mult_Suc]
lemma less_mult_le' [intro]: "m < (k::nat) ⟹ m*r + r ≤ k*r"
by (simp add: add.commute less_mult_le)
lemma bew_baibaib_eq_aux: assumes "❙|x❙| < ❙|u❙|" and "1 < i" and
eq: "x ⋅ y⇧@i⋅ x ⋅ y⇧@i ⋅ x = u ⋅ v⇧@i⋅ u ⋅ v⇧@i ⋅ u"
shows "commutes {x,y,u,v}"
proof-
from lenarg[OF ‹x ⋅ y⇧@i⋅ x ⋅ y⇧@i ⋅ x = u ⋅ v⇧@i⋅ u ⋅ v⇧@i ⋅ u›]
have "❙|u ⋅ v⇧@i❙| < ❙|x ⋅ y⇧@i❙|"
using ‹❙|x❙| < ❙|u❙|› by fastforce
have "0 < i"
using ‹1 < i› by force
have "(x⋅y⇧@i) ⋅ (u⋅v⇧@i) = (u⋅v⇧@i) ⋅ (x⋅y⇧@i)"
proof (rule two_pers)
show "x ⋅ y⇧@i⋅ x ⋅ y⇧@i ⋅ x ≤p (u ⋅ v ⇧@ i) ⋅ (x ⋅ y⇧@i⋅ x ⋅ y⇧@i ⋅ x)"
unfolding eq rassoc pref_cancel_conv by blast
show "x ⋅ y⇧@i⋅ x ⋅ y⇧@i ⋅ x ≤p (x ⋅ y ⇧@ i) ⋅ x ⋅ y⇧@i⋅ x ⋅ y⇧@i ⋅ x"
unfolding rassoc pref_cancel_conv by blast
show "❙|x ⋅ y ⇧@ i❙| + ❙|u ⋅ v ⇧@ i❙| ≤ ❙|x ⋅ y ⇧@ i ⋅ x ⋅ y ⇧@ i ⋅ x❙|"
using ‹❙|u ⋅ v⇧@i❙| < ❙|x ⋅ y⇧@i❙|› unfolding lenmorph by auto
qed
from comm_primrootE'[OF this]
obtain r m k where "x⋅y⇧@i = r⇧@k" "u⋅v⇧@i = r⇧@m" "primitive r".
note prim_nemp[OF ‹primitive r›]
have "❙|y❙| + ❙|r❙| ≤ ❙|y ⇧@ i❙|"
proof-
have "❙|u ⋅ v ⇧@ i ⋅ u ⋅ v ⇧@ i❙| ≤ ❙|x ⋅ y ⇧@ i ⋅ x ⋅ y ⇧@ i❙|" "❙|v ⇧@ i ⋅ u❙| ≤ ❙|y ⇧@ i ⋅ x❙|"
using ‹❙|u ⋅ v ⇧@ i❙| < ❙|x ⋅ y ⇧@ i❙|› unfolding lenmorph by linarith+
from eqdE[of "u ⋅ v⇧@i ⋅ u ⋅ v⇧@i" u "x ⋅ y⇧@i ⋅ x ⋅ y⇧@i" "x",
unfolded rassoc, OF eq[symmetric] this(1)]
obtain t' where t': "u ⋅ v ⇧@ i ⋅ u ⋅ v ⇧@ i ⋅ t' = x ⋅ y ⇧@ i ⋅ x ⋅ y ⇧@ i" "t' ⋅ x = u".
from eqdE[reversed, of "u ⋅ v⇧@i ⋅ u" "v⇧@i ⋅ u" "x ⋅ y⇧@i ⋅ x" "y⇧@i⋅x",
unfolded rassoc, OF eq[symmetric] ‹❙|v ⇧@ i ⋅ u❙| ≤ ❙|y ⇧@ i ⋅ x❙|›]
obtain t where t: "t ⋅ v ⇧@ i ⋅ u = y ⇧@ i ⋅ x" "x ⋅ y ⇧@ i ⋅ x ⋅ t = u ⋅ v ⇧@ i ⋅ u".
have "(x ⋅ y ⇧@ i ⋅ x ⋅ t) ⋅ (v ⇧@ i ⋅ t' ⋅ x) = x ⋅ y ⇧@ i ⋅ x ⋅ y ⇧@ i ⋅ x"
unfolding t' t rassoc eq..
hence "y⇧@i = t⋅v⇧@i⋅t'"
by force
have "m < k"
using ‹❙|u ⋅ v ⇧@ i❙| < ❙|x ⋅ y ⇧@ i❙|›
unfolding ‹u ⋅ v ⇧@ i = r ⇧@ m› ‹x ⋅ y ⇧@ i = r ⇧@ k› pow_len
by simp
hence "❙|u ⋅ v ⇧@ i❙| + ❙|r❙| ≤ ❙|x ⋅ y ⇧@ i❙|"
unfolding ‹u ⋅ v ⇧@ i = r ⇧@ m› ‹x ⋅ y ⇧@ i = r ⇧@ k› pow_len by blast
hence "2*❙|r❙| ≤ ❙|y⇧@i❙|"
using ‹❙|u ⋅ v ⇧@ i❙| + ❙|r❙| ≤ ❙|x ⋅ y ⇧@ i❙|› lenarg[OF t'(1)]
unfolding lenarg[OF ‹y⇧@i = t⋅v⇧@i⋅t'›] lenmorph by force
thus ?thesis
using mult_le_mono1[OF Suc_leI[OF ‹1 < i›], of "❙|y❙|"]
unfolding pow_len mult_Suc by force
qed
have "r ⋅ y = y ⋅ r"
proof (rule two_pers[reversed])
show "y⇧@i ≤s y⇧@i⋅r"
using triv_suf[of "y ⇧@ i" x, unfolded ‹x ⋅ y ⇧@ i = r ⇧@ k›, THEN suf_prod_root].
show "y⇧@i ≤s y⇧@i⋅y"
by (simp add: suf_pow_ext')
qed fact
note comm_pow_comm[OF this[symmetric], of i, symmetric]
have "r ⋅ x = x ⋅ r"
proof (rule comm_cancel_suf)
show "r ⋅ x ⋅ y⇧@i = x ⋅ y⇧@i ⋅ r"
using ‹x⋅y⇧@i = r⇧@k›
by (simp add: lassoc pow_comm)
show "r ⋅ y ⇧@ i = y ⇧@ i ⋅ r"
by fact
qed
have "r ⋅ u = u ⋅ r"
proof (rule comm_cancel_pref)
show "r ⋅ ((u ⋅ v⇧@i) ⋅ (u ⋅ v⇧@i)) = ((u ⋅ v⇧@i) ⋅ (u ⋅ v⇧@i)) ⋅ r"
unfolding ‹u⋅v⇧@i = r⇧@m› by comparison
have comm_aux: "r ⋅ (u ⋅ v ⇧@ i ⋅ u ⋅ v ⇧@ i ⋅ u) = (u ⋅ v ⇧@ i ⋅ u ⋅ v ⇧@ i ⋅ u) ⋅ r"
unfolding eq[symmetric]
using ‹x⋅y⇧@i = r⇧@k› ‹r ⋅ x = x ⋅ r› ‹r ⋅ y ⇧@ i = y ⇧@ i ⋅ r› rassoc by metis
show "r ⋅ ((u ⋅ v ⇧@ i) ⋅ u ⋅ v ⇧@ i) ⋅ u = ((u ⋅ v ⇧@ i) ⋅ u ⋅ v ⇧@ i) ⋅ u ⋅ r"
using comm_aux unfolding rassoc.
qed
have "r ⋅ v = v ⋅ r"
proof(rule comm_drop_exp[OF ‹0 < i›, symmetric])
show "r ⋅ v⇧@i = v⇧@i ⋅ r"
proof (rule comm_cancel_pref)
show "r ⋅ u ⋅ v⇧@i = u ⋅ v⇧@i ⋅ r"
using ‹u⋅v⇧@i = r⇧@m› pow_comm rassoc by metis
qed fact
qed
show "commutes {x,y,u,v}"
by (rule commutesI'[OF ‹r ≠ ε›])
(auto simp: ‹r ⋅ u = u ⋅ r› ‹r ⋅ v = v ⋅ r› ‹r ⋅ x = x ⋅ r› ‹r ⋅ y = y ⋅ r›)
qed
lemma bew_baibaib_eq: assumes "1 < i" and "x ≠ u" and
eq: "x ⋅ y⇧@i⋅ x ⋅ y⇧@i ⋅ x = u ⋅ v⇧@i⋅ u ⋅ v⇧@i ⋅ u"
shows "commutes {x,y,u,v}"
proof (rule linorder_cases[of "❙|x❙|" "❙|u❙|"])
assume "❙|x❙| < ❙|u❙|"
from bew_baibaib_eq_aux[OF this assms(1,3)]
show "commutes {x,y,u,v}".
next
assume "❙|u❙| < ❙|x❙|"
from bew_baibaib_eq_aux[OF this ‹1 < i› eq[symmetric]]
show "commutes {x,y,u,v}"
by (simp add: insert_commute)
qed (use eqd_eq(1)[OF eq] ‹x ≠ u› in blast)
theorem not_beg_abiab: "¬ binary_equality_generator (𝔞 ⋅ 𝔟⇧@(i+1) ⋅ 𝔞 ⋅ 𝔟)"
proof
have nemp: "𝔞 ⋅ 𝔟 ⇧@ (i + 1) ≠ ε" "𝔞 ⋅ 𝔟 ≠ ε"
by simp_all
assume "binary_equality_generator (𝔞 ⋅ 𝔟 ⇧@ (i+1) ⋅ 𝔞 ⋅ 𝔟)"
from beg_productE[of "𝔞 ⋅ 𝔟⇧@(i+1)" "𝔞 ⋅ 𝔟", unfolded rassoc, OF this nemp]
obtain g h where "binary_code_morphism (g :: binA list ⇒ nat list)" "binary_code_morphism h" "g ≠ h" "(𝔞 ⋅ 𝔟 ⇧@ (i + 1) ⋅ 𝔞 ⋅ 𝔟) ∈ g =⇩M h" "❙|g (𝔞 ⋅ 𝔟 ⇧@ (i + 1))❙| < ❙|h (𝔞 ⋅ 𝔟 ⇧@ (i + 1))❙|" "❙|h (𝔞 ⋅ 𝔟)❙| < ❙|g (𝔞 ⋅ 𝔟)❙|".
interpret g: binary_code_morphism g
by fact
interpret h: binary_code_morphism h
by fact
have " g 𝔞 ⋅ g 𝔟 ≠ h 𝔞 ⋅ h 𝔟"
using ‹❙|h (𝔞 ⋅ 𝔟)❙| < ❙|g (𝔞 ⋅ 𝔟)❙|› unfolding g.morph h.morph by fastforce
from bew_baiba_eq[OF this] min_solD[OF ‹(𝔞 ⋅ 𝔟 ⇧@ (i + 1) ⋅ 𝔞 ⋅ 𝔟) ∈ g =⇩M h›]
have "commutes {g 𝔟, g 𝔞, h 𝔟, h 𝔞}"
unfolding g.morph h.morph g.pow_morph h.pow_morph by blast
from commutesE[OF this, of "g 𝔞" "g 𝔟"]
show False
using g.non_comm_morph[of bina] by simp
qed
theorem not_beg_baibaib: assumes "1 < i"
shows "¬ binary_equality_generator (𝔟 ⋅ 𝔞⇧@i ⋅ 𝔟 ⋅ 𝔞⇧@i ⋅ 𝔟)"
proof
have nemp: "𝔟 ⋅ 𝔞⇧@i ⋅ 𝔟 ⋅ 𝔞⇧@i ≠ ε" "𝔟 ≠ ε"
by simp_all
assume "binary_equality_generator (𝔟 ⋅ 𝔞⇧@i ⋅ 𝔟 ⋅ 𝔞⇧@i ⋅ 𝔟)"
from beg_productE[of "𝔟 ⋅ 𝔞⇧@i ⋅ 𝔟 ⋅ 𝔞⇧@i" "𝔟", unfolded rassoc, OF this nemp]
obtain g h where "binary_code_morphism (g :: binA list ⇒ nat list)" "binary_code_morphism h" "g ≠ h" "(𝔟 ⋅ 𝔞 ⇧@ i ⋅ 𝔟 ⋅ 𝔞 ⇧@ i ⋅ 𝔟) ∈ g =⇩M h" "❙|g (𝔟 ⋅ 𝔞 ⇧@ i ⋅ 𝔟 ⋅ 𝔞 ⇧@ i)❙| < ❙|h (𝔟 ⋅ 𝔞 ⇧@ i ⋅ 𝔟 ⋅ 𝔞 ⇧@ i)❙|" "❙|h 𝔟❙| < ❙|g 𝔟❙|".
interpret g: binary_code_morphism g
by fact
interpret h: binary_code_morphism h
by fact
have "g 𝔟 ≠ h 𝔟"
using ‹❙|h 𝔟❙| < ❙|g 𝔟❙|› by fastforce
from bew_baibaib_eq[OF assms this] min_solD[OF ‹(𝔟 ⋅ 𝔞 ⇧@ i ⋅ 𝔟 ⋅ 𝔞 ⇧@ i ⋅ 𝔟) ∈ g =⇩M h›]
have "commutes {g 𝔟, g 𝔞, h 𝔟, h 𝔞}"
unfolding g.morph h.morph g.pow_morph h.pow_morph by blast
from commutesE[OF this, of "g 𝔞" "g 𝔟"]
show False
using g.non_comm_morph[of bina] by simp
qed
end