Theory Binary_Code_Imprimitive
theory Binary_Code_Imprimitive
imports
Combinatorics_Words_Graph_Lemma.Glued_Codes
Binary_Square_Interpretation
begin
text ‹This theory focuses on the characterization of imprimitive words which are concatenations
of copies of two words (forming a binary code).
We follow the article \cite{ lerest} (mainly Th\'eor\`eme 2.1 and Lemme 3.1),
while substantially optimizing the proof. See also \cite{ spehner} for an earlier result on this question,
and \cite{ Manuch} for another proof.›
section ‹General primitivity not preserving codes›
context code
begin
text ‹
Two nontrivially conjugate elements generated by a code induce a disjoint interpretation.›
lemma shift_disjoint:
assumes "ws ∈ lists 𝒞" and "ws' ∈ lists 𝒞" and "z ∉ ⟨𝒞⟩" and "z ⋅ concat ws = concat ws' ⋅ z"
"us ≤p ws⇧@n" and "vs ≤p ws'⇧@n"
shows "z ⋅ concat us ≠ concat vs"
using ‹z ∉ ⟨𝒞⟩›
proof (elim contrapos_nn)
assume "z ⋅ concat us = concat vs"
have "z ≠ ε"
using ‹z ∉ ⟨𝒞⟩› by blast
obtain us' where "ws⇧@n = us ⋅ us'"
using prefixE[OF ‹us ≤p ws⇧@n›].
obtain vs' where "ws'⇧@n = vs ⋅ vs'"
using prefixE[OF ‹vs ≤p ws'⇧@n›].
from conjug_pow[OF ‹z ⋅ concat ws = concat ws' ⋅ z›[symmetric], symmetric]
have "z ⋅ concat (ws⇧@n) = concat (ws'⇧@n) ⋅ z"
unfolding concat_pow_list.
from this[ unfolded ‹ws⇧@n = us ⋅ us'› ‹ws'⇧@n = vs ⋅ vs'› concat_morph rassoc
‹z ⋅ concat us = concat vs›[symmetric] cancel]
have "concat vs' ⋅ z = concat us'"..
show "z ∈ ⟨𝒞⟩"
proof (rule stability)
have "us ∈ lists 𝒞" and "us' ∈ lists 𝒞" and "vs ∈ lists 𝒞" and "vs' ∈ lists 𝒞"
using ‹ws ∈ lists 𝒞› ‹ws' ∈ lists 𝒞› ‹ws'⇧@n = vs ⋅ vs'› ‹ws⇧@n = us ⋅ us'›
by inlists
thus "z ⋅ concat us ∈ ⟨𝒞⟩" and "concat vs' ∈ ⟨𝒞⟩" and "concat us ∈ ⟨𝒞⟩" and "concat vs' ⋅ z ∈ ⟨𝒞⟩"
unfolding ‹concat vs' ⋅ z = concat us'› ‹z ⋅ concat us = concat vs›
by (simp_all add: concat_in_hull')
qed
qed
text‹This in particular yields a disjoint extendable interpretation of any prefix›
lemma shift_interp:
assumes "ws ∈ lists 𝒞" and "ws' ∈ lists 𝒞" and "z ∉ ⟨𝒞⟩" and
conjug: "z ⋅ concat ws = concat ws' ⋅ z" and "❙|z❙| ≤ ❙|concat ws'❙|"
and "us ≤p ws" and "us ≠ ε"
obtains p s vs ps where
"p us s ∼⇩𝒟 vs" and "vs ∈ lists 𝒞"
and "s ≤p concat (us¯⇧>(ws ⋅ ws))" and "p ≤s concat ws"
and "ps ⋅ vs ≤p ws' ⋅ ws'" and "concat ps ⋅ p = z"
proof-
have "ws' ⋅ ws' ∈ lists 𝒞"
using ‹ws' ∈ lists 𝒞› by inlists
have "concat us ≠ ε"
using ‹us ≠ ε› unfolding concat_eq_emp_conv[OF pref_in_lists[OF ‹us ≤p ws› ‹ws ∈ lists 𝒞›]].
have "❙|concat ws'❙| = ❙|concat ws❙|"
using lenarg[OF conjug, unfolded lenmorph] by linarith
have "z ⋅ concat(ws ⋅ ws) = concat (ws' ⋅ ws') ⋅ z"
unfolding rassoc concat_morph conjug[symmetric] unfolding lassoc cancel_right
using conjug.
hence "concat (ws' ⋅ ws') ≤p z ⋅ concat (ws ⋅ ws)"
by blast
have "z ⋅ concat ws ≤p concat (ws' ⋅ ws')"
unfolding concat_morph conjug pref_cancel_conv using eq_le_pref[OF conjug ‹❙|z❙| ≤ ❙|concat ws'❙|›].
from prefixE[OF pref_shorten[OF pref_concat_pref[OF ‹us ≤p ws›] this], unfolded rassoc]
obtain su where fac_u[symmetric]: "concat (ws' ⋅ ws') = z ⋅ concat us ⋅ su".
from fac_fac_interpE[OF fac_u ‹concat us ≠ ε›]
obtain ps ss' p s vs where "p (concat us) s ∼⇩ℐ vs" and
"ps ⋅ vs ⋅ ss' = ws' ⋅ ws'" and "concat ps ⋅ p = z" and "s ⋅ concat ss' = su".
note fac_interpD[OF ‹p (concat us) s ∼⇩ℐ vs›]
let ?ss = "us¯⇧>(ws ⋅ ws)"
have "us ⋅ ?ss = ws ⋅ ws"
using ‹us ≤p ws› by auto
have "ps ⋅ vs ≤p ws' ⋅ ws'"
unfolding ‹ps ⋅ vs ⋅ ss' = ws' ⋅ ws'›[symmetric] lassoc using triv_pref.
hence "vs ∈ lists 𝒞"
using ‹ws'∈ lists 𝒞›
by inlists
have "s ≤p concat ?ss"
using ‹concat (ws' ⋅ ws') ≤p z ⋅ concat (ws ⋅ ws)›
unfolding arg_cong[OF ‹ps ⋅ vs ⋅ ss' = ws' ⋅ ws'›, of concat, symmetric] ‹concat ps ⋅ p = z›[symmetric]
arg_cong[OF ‹us ⋅ ?ss = ws ⋅ ws›, of concat, symmetric]
unfolding concat_morph rassoc pref_cancel_conv
‹p ⋅ concat us ⋅ s = concat vs›[symmetric]
using append_prefixD by auto
have "❙|p❙| ≤ ❙|concat ws❙|"
using ‹❙|z❙| ≤ ❙|concat ws'❙|›[folded lenarg[OF ‹concat ps ⋅ p = z›], unfolded ‹❙|concat ws'❙| = ❙|concat ws❙|›]
by simp
with eqd[reversed, OF conjug[folded ‹concat ps ⋅ p = z›, unfolded lassoc, symmetric] this]
have "p ≤s concat ws"
by blast
have disjoint: "p ⋅ concat us' ≠ concat vs'" if "us' ≤p us" "vs' ≤p vs" for us' vs'
proof
have "us' ≤p ws ⋅ ws"
using ‹us ≤p ws› ‹us' ≤p us› by auto
have "ps ⋅ vs' ≤p ws' ⋅ ws'"
using ‹vs' ≤p vs› ‹ps ⋅ vs ≤p ws' ⋅ ws'› pref_trans same_prefix_prefix by metis
assume "p ⋅ concat us' = concat vs'"
hence "z ⋅ concat us' = concat (ps ⋅ vs')"
unfolding concat_morph ‹concat ps ⋅ p = z›[symmetric] rassoc cancel.
thus False
using shift_disjoint[OF ‹ws ∈ lists 𝒞› ‹ws' ∈ lists 𝒞› ‹z ∉ ⟨𝒞⟩›
‹z ⋅ concat ws = concat ws' ⋅ z› ‹us' ≤p ws ⋅ ws›[folded pow_list_2] ‹ps ⋅ vs' ≤p ws' ⋅ ws'›[folded pow_list_2]] by fast
qed
from disjoint[of ε ε]
have "p ≠ ε" by blast
have "s ≠ ε"
using ‹p ⋅ concat us ⋅ s = concat vs› disjoint by auto
from disj_interpI[OF ‹p (concat us) s ∼⇩ℐ vs›] disjoint
have "p us s ∼⇩𝒟 vs"
by blast
from that[OF this ‹vs ∈ lists 𝒞›
‹s ≤p concat ?ss› ‹p ≤s concat ws› ‹ps ⋅ vs ≤p ws' ⋅ ws'› ‹concat ps ⋅ p = z› ]
show thesis.
qed
text‹The conditions are in particular met by imprimitivity witnesses›
lemma imprim_witness_shift:
assumes "ws ∈ lists 𝒞" and "primitive ws" and "¬ primitive (concat ws)"
obtains z n where "concat ws = z⇧@n" "z ∉ ⟨𝒞⟩" and
"z ⋅ concat ws = concat ws ⋅ z" and "❙|z❙| < ❙|concat ws❙|" and "2 ≤ n"
proof-
have "concat ws ≠ ε"
using ‹primitive ws› emp_concat_emp'[OF ‹ws ∈ lists 𝒞›] emp_not_prim by blast
obtain z n where [symmetric]: "z⇧@n = concat ws" and "2 ≤ n"
using not_prim_primroot_expE[OF ‹¬ primitive (concat ws)›] by metis
hence "z ≠ ε"
using ‹concat ws ≠ ε› by force
have "z ∉ ⟨𝒞⟩"
proof
assume "z ∈ ⟨𝒞⟩"
then obtain zs where "zs ∈ lists 𝒞" and "concat zs = z"
using hull_concat_lists0 by blast
from is_code[OF ‹ws ∈ lists 𝒞› pow_in_lists[OF ‹zs ∈ lists 𝒞›],
unfolded concat_pow_list ‹concat ws = z⇧@n› ‹concat zs = z›, of n]
show False
using ‹primitive ws› ‹2 ≤ n› pow_nemp_imprim by blast
qed
have "❙|z❙| < ❙|concat ws❙|"
unfolding lenarg[OF ‹concat ws = z⇧@n›, unfolded lenmorph pow_len]
using nemp_len[OF ‹z ≠ ε›] ‹2 ≤ n› by simp
from that[OF ‹concat ws = z⇧@n› ‹z ∉ ⟨𝒞⟩› _ this ‹2 ≤ n›]
show thesis
unfolding ‹concat ws = z⇧@n› pow_comm by blast
qed
end
section ‹Covered uniform square›
lemma cover_xy_xxx: assumes "❙|x❙| = ❙|y❙|" and "p ⋅ x ⋅ y ⋅ s = x ⋅ x ⋅ x"
shows "x = y"
using append_assoc assms(1) assms(2) eq_le_pref le_refl long_pref lq_triv prefI pref_comm_eq' by metis
lemma cover_xy_yyy: assumes "❙|x❙| = ❙|y❙|" and eq: "p ⋅ x ⋅ y ⋅ s = y ⋅ y ⋅ y"
shows "x = y"
using cover_xy_xxx[reversed, unfolded rassoc, OF ‹❙|x❙| = ❙|y❙|›[symmetric] eq, symmetric].
lemma cover_xy_xxy: assumes "❙|x❙| = ❙|y❙|" and "s ≠ ε" and eq: "p ⋅ x ⋅ y ⋅ s = x ⋅ x ⋅ y"
shows "x = y"
proof-
have "❙|p❙| < ❙|x❙|"
using lenarg[OF eq] nemp_len[OF ‹s ≠ ε›] unfolding lenmorph by linarith
then obtain t where x: "x = p ⋅ t" and "t ≠ ε"
using eqd[OF eq] by force
from eq[unfolded this rassoc cancel]
have "p ⋅ t = t ⋅ p"
by mismatch
hence "x ≤p t ⋅ x"
unfolding x by auto
from eq[unfolded x]
have "y ≤p t ⋅ y"
using ‹p ⋅ t = t ⋅ p› ‹p ⋅ t ⋅ y ⋅ s = t ⋅ p ⋅ t ⋅ y› pref_cancel' suf_marker_per_root triv_pref by metis
show "x = y"
using same_len_nemp_root_eq[OF ‹x ≤p t ⋅ x›
‹y ≤p t ⋅ y› ‹t ≠ ε› _ ‹❙|x❙| = ❙|y❙|›] ‹❙|x❙| = ❙|y❙|› by force
qed
lemma cover_xy_xyy: assumes "❙|x❙| = ❙|y❙|" and "p ≠ ε" and eq: "p ⋅ x ⋅ y ⋅ s = x ⋅ y ⋅ y"
shows "x = y"
using cover_xy_xxy[reversed, unfolded rassoc, OF assms(1)[symmetric] assms(2) eq]..
lemma cover_xy_yyx: assumes "❙|x❙| = ❙|y❙|" and eq: "p ⋅ x ⋅ y ⋅ s = y ⋅ y ⋅ x"
shows "x = y"
proof-
have "❙|p❙| ≤ ❙|y❙|"
using lenarg[OF eq] unfolding lenmorph by linarith
then obtain t where y: "y = p ⋅ t"
using eqd[OF eq] by force
from eqd_eq[OF _ ‹❙|x❙| = ❙|y❙|›[unfolded y swap_len[of p]], unfolded rassoc] eq[unfolded this rassoc cancel]
have x: "x = t ⋅ p" by blast
from eq[unfolded x y rassoc cancel]
have "p ⋅ t = t ⋅ p"
by mismatch
thus "x = y"
unfolding x y..
qed
lemma cover_xy_yxx: assumes "❙|x❙| = ❙|y❙|" and eq: "p ⋅ x ⋅ y ⋅ s = y ⋅ x ⋅ x"
shows "x = y"
using cover_xy_yyx[reversed, unfolded rassoc, OF assms(1)[symmetric] eq]..
lemma cover_xy_xyx: assumes "❙|x❙| = ❙|y❙|" and "p ≠ ε" and "s ≠ ε" and eq: "p ⋅ x ⋅ y ⋅ s = x ⋅ y ⋅ x"
shows "¬ primitive (x ⋅ y)"
proof
assume "primitive (x ⋅ y)"
have "p ⋅ (x ⋅ y) ⋅ (s ⋅ y) = (x ⋅ y) ⋅ (x ⋅ y)"
unfolding lassoc eq[unfolded lassoc]..
from prim_overlap_sqE[OF ‹primitive (x ⋅ y)› this]
show False
using ‹p ≠ ε› ‹s ≠ ε› by blast
qed
lemma cover_xy_yxy: assumes "❙|x❙| = ❙|y❙|" and "p ≠ ε" and ‹s ≠ ε› and eq: "p ⋅ x ⋅ y ⋅ s = y ⋅ x ⋅ y"
shows "¬ primitive (x ⋅ y)"
using cover_xy_xyx[reversed, unfolded rassoc, OF assms(1)[symmetric] assms(3) assms(2) eq].
lemma cover_xy_three: assumes "❙|ws❙| = 3" "ws ∈ lists {x,y}" "❙|x❙| = ❙|y❙|"
"p ⋅ (x ⋅ y) ⋅ s = concat ws" "p ≠ ε" "s ≠ ε"
shows "¬ primitive (x⋅y) ∧ (ws = [x,y,x] ∨ ws = [y,x,y])"
proof (cases "x = y")
assume "x = y"
hence "~ primitive (x ⋅ y)"
using eq_append_not_prim by blast
moreover have "ws = [x,y,x] ∨ ws = [y,x,y]"
using ‹ws ∈ lists {x,y}› sing_pow_exp[of ws x, unfolded ‹❙|ws❙| = 3›]
unfolding ‹x = y› pow_list_3 by auto
ultimately show ?thesis
by blast
next
assume "x ≠ y"
with assms
show "¬ primitive (x⋅y) ∧ (ws = [x,y,x] ∨ ws = [y,x,y])"
proof(list_inspection, simp_all)
assume "p ⋅ x ⋅ y ⋅ s = x ⋅ x ⋅ x"
from cover_xy_xxx[OF ‹❙|x❙| = ❙|y❙|› this]
show False
using ‹x ≠ y› by blast
next
assume "p ⋅ x ⋅ y ⋅ s = x ⋅ x ⋅ y"
from cover_xy_xxy[OF ‹❙|x❙| = ❙|y❙|› ‹s ≠ ε› this]
show False
using ‹x ≠ y› by blast
next
assume "p ⋅ x ⋅ y ⋅ s = x ⋅ y ⋅ x"
from cover_xy_xyx[OF ‹❙|x❙| = ❙|y❙|› ‹p ≠ ε› ‹s ≠ ε› this]
show "¬ primitive (x ⋅ y)"
by blast
next
assume "p ⋅ x ⋅ y ⋅ s = x ⋅ y ⋅ y"
from cover_xy_xyy[OF ‹❙|x❙| = ❙|y❙|› ‹p ≠ ε› this]
show False
using ‹x ≠ y› by blast
next
assume "p ⋅ x ⋅ y ⋅ s = y ⋅ x ⋅ x"
from cover_xy_yxx[OF ‹❙|x❙| = ❙|y❙|› this]
show False
using ‹x ≠ y› by blast
next
assume "p ⋅ x ⋅ y ⋅ s = y ⋅ x ⋅ y"
from cover_xy_yxy[OF ‹❙|x❙| = ❙|y❙|› ‹p ≠ ε› ‹s ≠ ε› this]
show "¬ primitive (x ⋅ y)"
using ‹x ≠ y› by blast
next
assume "p ⋅ x ⋅ y ⋅ s = y ⋅ y ⋅ x"
from cover_xy_yyx[OF ‹❙|x❙| = ❙|y❙|› this]
show False
using ‹x ≠ y› by blast
next
assume "p ⋅ x ⋅ y ⋅ s = y ⋅ y ⋅ y"
from cover_xy_yyy[OF ‹❙|x❙| = ❙|y❙|› this]
show False
using ‹x ≠ y› by blast
qed
qed
lemma bin_uniform_len: assumes "ws ∈ lists {x,y}" "❙|x❙| = ❙|y❙|"
shows "❙|concat ws❙| = ❙|ws❙| * ❙|x❙|"
using assms by (induct ws, simp_all) blast
theorem uniform_square_interp: assumes "x⋅y ≠ y⋅x" and "❙|x❙| = ❙|y❙|" and "vs ∈ lists {x,y}"
and "p (x ⋅ y) s ∼⇩ℐ vs" and "p ≠ ε"
shows "¬ primitive (x⋅y)" and "vs = [x,y,x] ∨ vs = [y,x,y]"
proof-
note fac_interpD[OF ‹p (x ⋅ y) s ∼⇩ℐ vs›]
have "vs ≠ ε"
using ‹p ⋅ (x ⋅ y) ⋅ s = concat vs› assms(5) by force
have "❙|p❙| < ❙|x❙|"
using prefix_length_less[OF ‹p <p hd vs›] lists_hd_in_set[OF ‹vs ≠ ε› ‹vs ∈ lists {x,y}›]
‹❙|x❙| = ❙|y❙|›
by fastforce
have "❙|s❙| < ❙|x❙|"
using suffix_length_less[OF ‹s <s last vs›] ‹❙|x❙| = ❙|y❙|› lists_hd_in_set[reversed, OF ‹vs ≠ ε› ‹vs ∈ lists {x,y}›]
by fastforce
have "❙|concat vs❙| = ❙|x❙| * ❙|vs❙|"
using bin_uniform_len[OF assms(3,2)] by simp
note leneq = lenarg[OF ‹p ⋅ (x ⋅ y) ⋅ s = concat vs›, unfolded this lenmorph ‹❙|x❙| = ❙|y❙|›[symmetric]]
hence "2 * ❙|x❙| < ❙|x❙| * ❙|vs❙|" and "❙|x❙| * ❙|vs❙| < ❙|x❙| * 4"
using ‹❙|p❙| < ❙|x❙|› ‹❙|s❙| < ❙|x❙|› nemp_len[OF ‹p ≠ ε›] by linarith+
hence "❙|vs❙| = 3"
by force
hence "s ≠ ε"
using leneq ‹❙|p❙| < ❙|x❙|› by force
show "¬ primitive (x⋅y)" "vs = [x,y,x] ∨ vs = [y,x,y]"
using cover_xy_three[OF ‹❙|vs❙| = 3› ‹vs ∈ lists {x,y}› ‹❙|x❙| = ❙|y❙|› ‹p ⋅ (x ⋅ y) ⋅ s = concat vs› ‹p ≠ ε› ‹s ≠ ε› ]
by blast+
qed
subsection ‹Primitivity (non)preserving uniform binary codes›
theorem bin_uniform_prim_morph:
assumes "x ⋅ y ≠ y ⋅ x" and "❙|x❙| = ❙|y❙|" and "primitive (x ⋅ y)"
and "ws ∈ lists {x,y}" and "2 ≤ ❙|ws❙|"
shows "primitive ws ⟷ primitive (concat ws)"
proof (standard, rule ccontr)
assume ‹primitive ws› and ‹¬ primitive (concat ws)›
from bin_prim_long_pref[OF ‹ws ∈ lists {x,y}› ‹primitive ws› ‹2 ≤ ❙|ws❙|›]
obtain ws' where "ws ∼ ws'" "[x, y] ≤p ws'".
have "ws' ∈ lists {x,y}"
using conjug_in_lists'[OF ‹ws ∼ ws'› ‹ws ∈ lists {x,y}›].
have "primitive ws'"
using prim_conjug[OF ‹primitive ws› ‹ws ∼ ws'›].
have "¬ primitive (concat ws')"
using conjug_concat_prim_iff ‹¬ primitive (concat ws)› ‹ws ∼ ws'› by auto
interpret code "{x,y}"
using bin_code_code[OF ‹x ⋅ y ≠ y ⋅ x›].
have "[x,y] ≠ ε" by blast
from imprim_witness_shift[OF ‹ws' ∈ lists {x,y}› ‹primitive ws'› ‹¬ primitive (concat ws')›]
obtain z n where "concat ws' = z ⇧@ n" "z ∉ ⟨{x, y}⟩" "z ⋅ concat ws' = concat ws' ⋅ z" "❙|z❙| < ❙|concat ws'❙|".
from shift_interp[OF ‹ws' ∈ lists {x,y}› ‹ws' ∈ lists {x,y}› this(2-3) less_imp_le[OF this(4)] ‹[x,y] ≤p ws'› ‹[x,y] ≠ ε›]
obtain p s vs ps where "p [x, y] s ∼⇩𝒟 vs" "vs ∈ lists {x, y}" "s ≤p concat ([x, y]¯⇧>(ws' ⋅ ws'))"
"p ≤s concat ws'" "ps ⋅ vs ≤p ws' ⋅ ws'" "concat ps ⋅ p = z".
from uniform_square_interp(1)[OF ‹x ⋅ y ≠ y ⋅ x› ‹❙|x❙| = ❙|y❙|› ‹vs ∈ lists {x,y}› _ _]
‹primitive (x ⋅ y)› disj_interpD0[OF this(1), simplified] disj_interp_nemp(1)[OF this(1)]
show False
by blast
qed (simp add: prim_concat_prim)
lemma bin_uniform_imprim: assumes "x ⋅ y ≠ y ⋅ x" and "❙|x❙| = ❙|y❙|" and "¬ primitive (x ⋅ y)"
shows "primitive x"
proof-
have "x ⋅ y ≠ ε" and "x ≠ ε" and "y ≠ ε"
using ‹x ⋅ y ≠ y ⋅ x› by blast+
from not_prim_expE[OF ‹¬ primitive (x ⋅ y)› ‹x ⋅ y ≠ ε›]
obtain z k where "primitive z" and "2 ≤ k" and "z⇧@k = x ⋅ y".
hence "0 < k"
by simp
from split_pow[OF ‹z⇧@k = x ⋅ y›[symmetric] ‹0 < k› ‹y ≠ ε›]
obtain u v l m where [symmetric]: "z = u ⋅ v" and "v ≠ ε" "x = (u⋅v) ⇧@ l ⋅ u" "y = (v ⋅ u) ⇧@ m ⋅ v" "k = l + m + 1".
have "u ⋅ v ≠ v ⋅ u"
using ‹x ⋅ y ≠ y ⋅ x› unfolding ‹x = (u⋅v) ⇧@ l ⋅ u› ‹y = (v ⋅ u) ⇧@ m ⋅ v›
shifts unfolding pow_add[symmetric] add.commute[of m] by force
have "u ≠ ε" and "v ≠ ε" and "u ≠ v"
using ‹u ⋅ v ≠ v ⋅ u› by blast+
have "m = l" and "❙|u❙| = ❙|v❙|"
using almost_equal_equal[OF nemp_len_not0[OF ‹u ≠ ε›] nemp_len_not0[OF ‹v ≠ ε›], of l m] lenarg[OF ‹x = (u⋅v)⇧@l ⋅ u›, unfolded ‹❙|x❙| =❙|y❙|›, unfolded lenarg[OF ‹y = (v ⋅ u) ⇧@ m ⋅ v›]]
unfolding lenmorph pow_len lenarg[OF ‹u ⋅ v = z›, symmetric] by algebra+
from ‹k = l + m + 1›[folded Suc_eq_plus1, symmetric]
have "l ≠ 0"
using ‹2 ≤ k›[folded ‹Suc(l+m) = k›, unfolded ‹m = l›] by force
let ?w = "[u,v]⇧@l ⋅ [u]"
have "?w ∈ lists {u,v}"
by (induct l, simp_all)
have "2 ≤ ❙|?w❙|"
using ‹l ≠ 0› unfolding lenmorph pow_len by fastforce
have "concat ?w = x"
using ‹x = (u ⋅ v) ⇧@ l ⋅ u› by (simp add: concat_pow_list)
from bin_uniform_prim_morph[OF ‹u ⋅ v ≠ v ⋅ u› ‹❙|u❙| = ❙|v❙|› ‹primitive z›[folded ‹u ⋅ v = z›] ‹?w ∈ lists {u,v}› ‹2 ≤ ❙|?w❙|›]
show "primitive x"
unfolding ‹concat ?w = x› using alternate_prim[OF ‹u ≠ v›] by blast
qed
theorem bin_uniform_prim_morph':
assumes "x ⋅ y ≠ y ⋅ x" and "❙|x❙| = ❙|y❙|" and "primitive (x ⋅ y) ∨ ¬ primitive x ∨ ¬ primitive y"
and "ws ∈ lists {x,y}" and "2 ≤ ❙|ws❙|"
shows "primitive ws ⟷ primitive (concat ws)"
using bin_uniform_prim_morph[OF assms(1-2) _ assms(4-5)] bin_uniform_imprim[OF assms(1-2)]
bin_uniform_imprim[OF assms(1-2)[symmetric], unfolded conjug_prim_iff'[of y]]
assms(3) by blast
section ‹The main theorem›
subsection ‹Imprimitive words with single y›
text ‹If the shorter word occurs only once, the result is straightforward from the parametric solution of the Lyndon-Schutzenberger
equation.›
lemma bin_imprim_single_y:
assumes non_comm: "x ⋅ y ≠ y ⋅ x" and
"ws ∈ lists {x,y}" and
"❙|y❙| ≤ ❙|x❙|" and
"2 ≤ count_list ws x" and
"count_list ws y < 2" and
"primitive ws" and
"¬ primitive (concat ws)"
shows "ws ∼ [x,x,y]" and "primitive x" and "primitive y"
proof-
have "x ≠ y"
using non_comm by blast
have "count_list ws y ≠ 0"
proof
assume "count_list ws y = 0"
with ‹ws ∈ lists {x,y}›
have "ws ∈ lists {x}"
unfolding count_list_0_iff by blast
from prim_exp_one[OF ‹primitive ws› this[unfolded sing_lists_exp_count]]
show False
using ‹2 ≤ count_list ws x› by simp
qed
hence "count_list ws y = 1"
using ‹count_list ws y < 2› by linarith
from this bin_count_one_conjug[OF ‹ws ∈ lists {x,y}› _ this]
have "ws ∼ [x]⇧@count_list ws x ⋅ [y]"
using non_comm (1) by metis
from conjug_concat_prim_iff[OF this]
have "¬ primitive (x⇧@(count_list ws x) ⋅ y)"
using ‹¬ primitive (concat ws)› by simp
from not_prim_primroot_expE[OF this]
obtain z l where [symmetric]: "z⇧@l = x⇧@(count_list ws x) ⋅ y⇧@1" and "2 ≤ l"
unfolding pow_list_1.
interpret LS_len_le x y "count_list ws x" 1 l z
by (unfold_locales)
(use ‹2 ≤ count_list ws x› ‹x ⋅ y ≠ y ⋅ x› ‹ ❙|y❙| ≤ ❙|x❙|›
‹x ⇧@ count_list ws x ⋅ y ⇧@ 1 = z ⇧@ l› ‹2 ≤ l› in force)+
from case_j2k1[OF ‹2 ≤ count_list ws x› refl]
have "primitive x" and "primitive y" and "count_list ws x = 2" by blast+
with ‹ws ∼ [x]⇧@count_list ws x ⋅ [y]›[unfolded this(3) pow_list_2 append_Cons append_Nil]
show "primitive x" and "primitive y" and "ws ∼ [x,x,y]"
by simp_all
qed
subsection ‹Conjugate words›
lemma bin_imprim_not_conjug:
assumes "ws ∈ lists {x,y}" and
"x ⋅ y ≠ y ⋅ x" and
"2 ≤ ❙|ws❙|" and
"primitive ws" and
"¬ primitive (concat ws)"
shows "¬ x ∼ y"
proof
assume "x ∼ y"
hence "❙|x❙| = ❙|y❙|" by force
from bin_uniform_prim_morph[OF ‹x ⋅ y ≠ y ⋅ x› this _ ‹ws ∈ lists {x,y}› ‹2 ≤ ❙|ws❙|›]
have "¬ primitive (x⋅y)"
using ‹primitive ws› ‹¬ primitive (concat ws)› by blast
from Lyndon_Schutzenberger_conjug[OF ‹x ∼ y› this]
show False
using ‹x ⋅ y ≠ y ⋅ x› by blast
qed
subsection ‹Square factor of the longer word and both words primitive (was all\_assms)›
text‹The main idea of the proof is as follows: Imprimitivity of the concatenation yields
(at least) two overlapping factorizations into @{term "{x,y}"}.
Due to the presence of the square @{term "x ⋅ x"}, these two can be synchronized, which yields that the
situation coincides with the canonical form.
›
lemma bin_imprim_primitive:
assumes "x ⋅ y ≠ y ⋅ x"
and "primitive x" and "primitive y"
and "❙|y❙| ≤ ❙|x❙|"
and "ws ∈ lists {x, y}"
and "primitive ws" and "¬ primitive (concat ws)"
and "[x, x] ≤f ws ⋅ ws"
shows "ws ∼ [x, x, y]"
proof-
have "x ≠ y"
using assms(1) by blast
have "❙|ws❙| ≠ 1"
using len_one_concat_in[OF ‹ws ∈ lists {x, y}›] ‹¬ primitive (concat ws)› ‹primitive x› ‹primitive y›
by blast
with prim_nemp[OF ‹primitive ws›, THEN nemp_le_len]
have "2 ≤ ❙|ws❙|"
by auto
hence "❙|[x, x]❙| ≤ ❙|ws❙|"
by force
have "¬ x ∼ y"
by (rule bin_imprim_not_conjug) fact+
have "primitive [x,x,y]"
using ‹x ≠ y› by primitivity_inspection
have "concat [x,x] = x ⋅ x"
by simp
interpret xy: binary_code x y
using ‹x ⋅ y ≠ y ⋅ x› by (unfold_locales)
obtain ws' where "ws ∼ ws'" "[x,x] ≤p ws'"
using rotate_into_pos_sq[of ε "[x,x]" _ thesis, unfolded emp_simps, OF ‹[x, x] ≤f ws ⋅ ws›
le0 ‹❙|[x, x]❙| ≤ ❙|ws❙|›] by blast
have "ws' ∈ lists {x,y}" and "primitive ws'" and "¬ primitive (concat ws')"
using conjug_in_lists'[OF ‹ws ∼ ws'› ‹ws ∈ lists {x, y}›]
prim_conjug[OF ‹primitive ws› ‹ws ∼ ws'›]
‹¬ primitive (concat ws)›[unfolded conjug_concat_prim_iff[OF ‹ws ∼ ws'›]].
have "2 ≤ ❙|ws'❙|" and "[x,x] ≠ ε" and "ws' ≠ ε"
using ‹[x,x] ≤p ws'› unfolding prefix_def by auto
have "concat ws' ≠ ε"
using ‹primitive x› ‹[x,x] ≤p ws'› by (fastforce simp add: prefix_def)
have "ws' ⋅ ws' ⋅ ws' ∈ lists {x, y}" and "ws' ⋅ ws' ∈ lists {x, y}"
using ‹ws' ∈ lists {x,y}› by inlists
have "ws' = [x,x,y]"
proof(rule ccontr)
assume "ws' ≠ [x,x,y]"
from xy.imprim_witness_shift[OF ‹ws' ∈ lists {x,y}› ‹primitive ws'› ‹¬ primitive (concat ws')›]
obtain z n where con_ws: "concat ws' = z ⇧@ n" and "z ∉ ⟨{x, y}⟩" and "z ⋅ concat ws' = concat ws' ⋅ z"
and "❙|z❙| < ❙|concat ws'❙|" and "2 ≤ n".
have "0 < n"
using ‹2 ≤ n› by simp
from xy.shift_interp[OF ‹ws' ∈ lists {x,y}› ‹ws' ∈ lists {x,y}› ‹z ∉ ⟨{x, y}⟩› ‹z ⋅ concat ws' = concat ws' ⋅ z›
less_imp_le[OF ‹❙|z❙| < ❙|concat ws'❙|›] ‹[x,x] ≤p ws'› ‹[x,x] ≠ ε›]
obtain p s vs ps where dis: "p [x,x] s ∼⇩𝒟 vs" and ‹vs ∈ lists {x, y}› and
"s ≤p concat ([x,x]¯⇧>(ws'⋅ws'))" and "p ≤s concat ws'" and "ps ⋅ vs ≤p ws' ⋅ ws'" and "concat ps ⋅ p = z".
from disj_interp_nemp(1)[OF this(1)]
have "p ≠ ε" by simp
have "p ⋅ concat p1 ≠ concat p2" if "p1 ≤p [x, x]" and "p2 ≤p vs" for p1 p2
using ‹p [x,x] s ∼⇩𝒟 vs› disj_interpD1 that by blast
have "ps ∈ lists {x,y}"
using ‹ps ⋅ vs ≤p ws' ⋅ ws'› ‹ws' ∈ lists {x,y}› ‹ws' ⋅ ws' ∈ lists {x, y}› append_prefixD pref_in_lists by metis
have "vs ∈ lists {x,y}"
using ‹ws' ∈ lists {x,y}› pref_in_lists[OF ‹ps ⋅ vs ≤p ws' ⋅ ws'›] by inlists
have "[x,x]¯⇧>(ws'⋅ws') ∈ lists {x,y}"
using ‹ws' ∈ lists {x,y}› by inlists
have "p x ⋅ x s ∼⇩ℐ vs"
using disj_interpD0[OF ‹p [x,x] s ∼⇩𝒟 vs›] by simp
interpret square_interp_ext x y p s vs
proof (rule square_interp_ext.intro[OF square_interp.intro, unfolded square_interp_ext_axioms_def])
show "(∃pe. pe ∈ ⟨{x, y}⟩ ∧ p ≤s pe) ∧ (∃se. se ∈ ⟨{x, y}⟩ ∧ s ≤p se)"
using ‹s ≤p concat ([x,x]¯⇧>(ws'⋅ws'))› ‹p ≤s concat ws'›
‹[x, x]¯⇧>(ws' ⋅ ws') ∈ lists {x, y}› ‹ws' ∈ lists {x, y}› concat_in_hull' by meson
show "¬ ρ x ∼ ρ y"
using ‹¬ x ∼ y› unfolding prim_primroot[OF ‹primitive y›] prim_primroot[OF ‹primitive x›].
show "p Ref {ρ x, y} [x, x] s ∼⇩𝒟 vs"
unfolding prim_primroot[OF ‹primitive x›] using dis xy.code_ref_list[of "[x,x]"] by force
qed fact+
define xp where "xp = x ⋅ p"
have "concat [x,x,y] = xp ⋅ xp"
by (simp add: xxy_root xp_def)
hence "ws' ⋅ [x,x,y] ≠ [x,x,y] ⋅ ws'"
using comm_prim[OF ‹primitive ws'› ‹primitive [x,x,y]›] ‹ws' ≠ [x,x,y] ›by force
have "z ⋅ xp ≠ xp ⋅ z"
proof
assume "z ⋅ xp = xp ⋅ z"
from comm_pow_comm[symmetric, OF this[symmetric], of 2,
THEN comm_pow_comm, of n, unfolded pow_list_2]
have "z⇧@n ⋅ xp ⋅ xp = xp ⋅ xp ⋅ z⇧@n"
unfolding rassoc.
hence "concat ws' ⋅ concat [x,x,y] = concat [x,x,y] ⋅ concat ws'"
unfolding con_ws ‹concat [x,x,y] = xp ⋅ xp› rassoc by simp
from xy.is_code[OF _ _ this[folded concat_morph]]
have "ws' ⋅ [x, x, y] = [x,x,y] ⋅ ws'"
using append_in_lists ‹ws' ∈ lists {x,y}› by simp
thus False
using ‹ws' ⋅ [x, x, y] ≠ [x,x,y] ⋅ ws'› by fastforce
qed
then interpret binary_code z xp
by (unfold_locales)
have "¬ concat (ws' ⋅ [x, x, y]) ⨝ concat ([x, x, y] ⋅ ws')"
proof (rule notI)
assume "concat (ws' ⋅ [x, x, y]) ⨝ concat ([x, x, y] ⋅ ws')"
from comm_comp_eq[OF this[unfolded concat_morph], unfolded ‹concat [x,x,y] = xp ⋅ xp› con_ws]
have "z ⇧@ n ⋅ xp⇧@Suc(Suc 0) = xp⇧@Suc(Suc 0) ⋅ z ⇧@ n"
unfolding pow_Suc pow_zero emp_simps rassoc.
from comm_drop_exps[OF _ _ this]
show False
using ‹z ⋅ xp ≠ xp ⋅ z› ‹2 ≤ n› by force
qed
define lcp_ws where "lcp_ws = ws' ⋅ [x,x,y] ∧⇩p [x,x,y] ⋅ ws'"
have "lcp_ws ∈ lists {x,y}"
unfolding lcp_ws_def by inlists
have lcp_xp_z: "concat (ws' ⋅ [x,x,y]) ∧⇩p concat ([x,x,y] ⋅ ws') = bin_lcp z (x ⋅ p)"
unfolding concat_morph con_ws ‹concat [x,x,y] = xp ⋅ xp› pow_add[symmetric]
using bin_lcp_pows[OF ‹0 < n›, of 2]
unfolding pow_list_2 pow_pos[OF ‹0 < n›] rassoc xp_def by force
have "(concat lcp_ws) ⋅ bin_lcp x y = bin_lcp z (x ⋅ p)"
proof (rule xy.bin_code_lcp_concat'[OF _ _ ‹¬ concat (ws' ⋅ [x, x, y]) ⨝ concat ([x, x, y] ⋅ ws')›, folded lcp_ws_def, unfolded lcp_xp_z, symmetric])
show "ws' ⋅ [x, x, y] ∈ lists {x, y}" and "[x, x, y] ⋅ ws' ∈ lists {x, y}"
by inlists
qed
define ws'' where "ws'' = ps ⋅ [x,y]"
define lcp_ws' where "lcp_ws' = ws' ⋅ ws'' ∧⇩p ws'' ⋅ ws'"
have "lcp_ws' ∈ lists {x,y}"
unfolding lcp_ws'_def
using ‹ps ∈ lists {x, y}› ‹ws' ∈ lists {x, y}› ws''_def by inlists
have "concat ws'' = z ⋅ xp"
unfolding ws''_def xp_def using ‹concat ps ⋅ p = z› xxy_root by fastforce
have "ws' ⋅ ws'' ≠ ws'' ⋅ ws'"
proof
assume "ws' ⋅ ws'' = ws'' ⋅ ws'"
from arg_cong[OF this, of concat, unfolded concat_morph con_ws
‹concat ws'' = z ⋅ xp›,
unfolded lassoc pow_comm, unfolded rassoc cancel]
show False
using ‹z ⋅ xp ≠ xp ⋅ z› comm_drop_exp'[OF _ ‹0 < n›] by blast
qed
have
lcp_xp_z': "concat (ws' ⋅ ws'') ∧⇩p concat (ws'' ⋅ ws') = z ⋅ bin_lcp z (x ⋅ p)"
unfolding concat_morph con_ws ‹concat ws'' = z ⋅ xp› pow_Suc
unfolding lcp_ext_left[symmetric] bin_lcp_def shifts
unfolding rassoc lcp_ext_left cancel
using bin_lcp_pows[OF ‹0 < n›, of 1 ε "z⇧@(n-1)", unfolded pow_list_1, folded pow_pos[OF ‹0 < n›]]
unfolding bin_lcp_def xp_def rassoc emp_simps by linarith
have "z ⋅ bin_lcp z (x ⋅ p) = concat (lcp_ws') ⋅ bin_lcp x y"
unfolding lcp_xp_z'[symmetric] lcp_ws'_def
proof (rule xy.bin_code_lcp_concat')
show "ws' ⋅ ws'' ∈ lists {x, y}"
unfolding ws''_def using ‹ws' ⋅ ws' ⋅ ws' ∈ lists {x, y}› ‹ps ∈ lists {x,y}› by inlists
thus "ws'' ⋅ ws' ∈ lists {x, y}"
by inlists
show "¬ concat (ws' ⋅ ws'') ⨝ concat (ws'' ⋅ ws')"
unfolding concat_morph con_ws ‹concat ws'' = z ⋅ xp› pow_pos[OF ‹0 < n›]
unfolding rassoc comp_cancel
unfolding lassoc pow_pos[OF ‹0 < n›, symmetric] pow_pos2[OF ‹0 < n›, symmetric]
comm_comp_eq_conv
using comm_drop_exp'[OF _ ‹0 < n›, of n z xp] non_comm by argo
qed
have "concat lcp_ws' = z ⋅ concat lcp_ws"
unfolding cancel_right[of "concat lcp_ws'" "bin_lcp x y" "z ⋅ concat lcp_ws", symmetric]
unfolding rassoc[of z] ‹concat (lcp_ws) ⋅ bin_lcp x y = bin_lcp z (x ⋅ p)› ‹z ⋅ bin_lcp z (x ⋅ p) = concat (lcp_ws') ⋅ bin_lcp x y›..
have "lcp_ws ≤p ws' ⋅ [x,x,y]"
unfolding lcp_ws_def using longest_common_prefix_prefix1.
have "lcp_ws ≠ ws' ⋅ [x,x,y]"
unfolding lcp_ws_def lcp_pref_conv
using ‹ws' ⋅ [x, x, y] ≠ [x, x, y] ⋅ ws'› pref_comm_eq by blast
have "lcp_ws ≤p ws' ⋅ [x,x]"
using spref_butlast_pref[OF ‹lcp_ws ≤p ws' ⋅ [x,x,y]› ‹lcp_ws ≠ ws' ⋅ [x,x,y]›]
unfolding butlast_append by simp
from prefixE[OF pref_prolong[OF this ‹[x,x] ≤p ws'›]]
obtain ws''⇩1 where "ws' ⋅ ws' ⋅ ws' = lcp_ws ⋅ ws''⇩1" using rassoc by metis
have "ws' ⋅ ps ⋅ [x,y] ≤p ws' ⋅ ps ⋅ [x,y,x]"
by simp
from pref_trans[OF pref_trans[OF longest_common_prefix_prefix1 this]]
have "lcp_ws' ≤p ws' ⋅ ws' ⋅ ws'"
unfolding lcp_ws'_def ws''_def using ‹ps ⋅ vs ≤p ws' ⋅ ws'›[unfolded cover_xyx, unfolded pref_cancel_conv]
unfolding pref_cancel_conv[symmetric, of "ps ⋅ [x,y,x]" "ws' ⋅ ws'" ws'] by blast
from prefixE[OF this]
obtain ws''⇩2 where "ws' ⋅ ws' ⋅ ws' = lcp_ws' ⋅ ws''⇩2".
have "concat lcp_ws'⋅ concat ws''⇩1 = z ⋅ concat(lcp_ws) ⋅ concat ws''⇩1"
unfolding lassoc ‹concat lcp_ws' = z ⋅ concat lcp_ws›..
also have "... = z ⋅ concat (ws' ⋅ ws' ⋅ ws')"
unfolding rassoc ‹ws' ⋅ ws' ⋅ ws' = lcp_ws ⋅ ws''⇩1› concat_morph..
also have "... = concat (ws' ⋅ ws' ⋅ ws') ⋅ z"
unfolding concat_morph con_ws pow_add[symmetric]
pow_Suc[symmetric] pow_Suc2[symmetric]..
also have "... = concat lcp_ws'⋅ concat ws''⇩2 ⋅ z"
unfolding ‹ws' ⋅ ws' ⋅ ws' = lcp_ws' ⋅ ws''⇩2› concat_morph rassoc..
finally have "concat ws''⇩1 = concat ws''⇩2 ⋅ z"
unfolding cancel.
from xy.stability[of "concat ws''⇩2" "concat lcp_ws" z,
folded ‹concat ws''⇩1 = concat ws''⇩2 ⋅ z› ‹concat lcp_ws' = z ⋅ concat lcp_ws›]
have "z ∈ ⟨{x, y}⟩"
using ‹ws' ⋅ ws' ⋅ ws' = lcp_ws ⋅ ws''⇩1› ‹ws' ⋅ ws' ⋅ ws' = lcp_ws' ⋅ ws''⇩2› ‹ws' ⋅ ws' ⋅ ws' ∈ lists {x, y}›
append_in_lists_dest append_in_lists_dest' concat_in_hull' by metis
thus False
using ‹z ∉ ⟨{x,y}⟩› by blast
qed
thus "ws ∼ [x, x, y]"
using ‹ws ∼ ws'› by blast
qed
subsection ‹Obtaining primitivity with two squares (refining)›
lemma bin_imprim_both_squares_prim:
assumes "x ⋅ y ≠ y ⋅ x"
and "ws ∈ lists {x, y}"
and "primitive ws" and "¬ primitive (concat ws)"
and "[x, x] ≤f ws ⋅ ws"
and "[y, y] ≤f ws ⋅ ws"
and "primitive x" and "primitive y"
shows False
proof-
have "x ≠ y" using ‹x ⋅ y ≠ y ⋅ x›
by blast
from bin_imprim_primitive[OF ‹x ⋅ y ≠ y ⋅ x› ‹primitive x› ‹primitive y›
_ ‹ws ∈ lists {x,y}› ‹primitive ws› ‹¬ primitive (concat ws)› ‹[x, x] ≤f ws ⋅ ws›]
bin_imprim_primitive[OF ‹x ⋅ y ≠ y ⋅ x›[symmetric] ‹primitive y› ‹primitive x›
_ ‹ws ∈ lists {x,y}›[unfolded insert_commute[of x]] ‹primitive ws› ‹¬ primitive (concat ws)›
‹[y, y] ≤f ws ⋅ ws›]
have "ws ∼ [x, x, y] ∨ ws ∼ [y, y, x]"
using ‹x ⋅ y ≠ y ⋅ x›
by force
hence "❙|ws❙| = 3"
using conjug_len by force
note[simp] = sublist_code(3)
from ‹❙|ws❙| = 3› ‹ws ∈ lists {x,y}› ‹x ≠ y›
‹[x, x] ≤f ws ⋅ ws› ‹[y, y] ≤f ws ⋅ ws›
show False
by list_inspection simp_all
qed
lemma bin_imprim_both_squares:
assumes "x ⋅ y ≠ y ⋅ x"
and "ws ∈ lists {x, y}"
and "primitive ws" and "¬ primitive (concat ws)"
and "[x, x] ≤f ws ⋅ ws"
and "[y, y] ≤f ws ⋅ ws"
shows False
proof (rule bin_imprim_both_squares_prim)
have "x ≠ ε" and "y ≠ ε" and "x ≠ y"
using ‹x ⋅ y ≠ y ⋅ x› by blast+
let ?R = "λ x. [ρ x]⇧@(e⇩ρ x)"
define ws' where "ws' = Ref⇩ρ ws"
show "ρ x ⋅ ρ y ≠ ρ y ⋅ ρ x"
using ‹x ⋅ y ≠ y ⋅ x›[unfolded comm_primroot_conv'[of x y]].
have [simp]: "a = x ∨ a = y ⟹ [ρ a] ⇧@ e⇩ρ a ∈ lists {ρ x, ρ y}" for a
using insert_iff sing_pow_lists[of _ "{ρ x, ρ y}"] by metis
show "ws' ∈ lists {ρ x, ρ y}"
unfolding ws'_def root_ref_def using ‹ws ∈ lists {x,y}›
by (induction ws, simp_all)
interpret binary_code x y
using ‹x ⋅ y ≠ y ⋅ x› by unfold_locales
note[simp] = sublist_code(3)
have "❙|ws❙| ≤ 3 ⟹ ws ∈ lists {x,y} ⟹ x ≠ y ⟹ [x, x] ≤f ws ⋅ ws ⟹ [y, y] ≤f ws ⋅ ws ⟹ False"
by list_inspection simp_all
from this[OF _ ‹ ws ∈ lists {x,y}› ‹x ≠ y› ‹[x, x] ≤f ws ⋅ ws› ‹[y, y] ≤f ws ⋅ ws›]
roots_prim_morph[OF ‹ws ∈ lists {x,y}› _ ‹primitive ws›]
show "primitive ws'"
unfolding ws'_def root_ref_def by fastforce
show "¬ primitive (concat ws')"
unfolding ws'_def root_ref_refines by fact
have "Ref⇩ρ [x,x] ≤f ws' ⋅ ws'" and "Ref⇩ρ [y,y] ≤f ws' ⋅ ws'"
unfolding ws'_def root_ref_def
using concat_mono_fac[OF map_mono_sublist[OF ‹[x,x] ≤f ws ⋅ ws›]]
concat_mono_fac[OF map_mono_sublist[OF ‹[y,y] ≤f ws ⋅ ws›]]
unfolding concat_morph map_append.
have "Suc (Suc (e⇩ρ x + e⇩ρ x - 2)) = e⇩ρ x + e⇩ρ x"
using Suc_minus2 primroot_exp_nemp[OF ‹x ≠ ε›] by simp
have "Ref⇩ρ [x,x] = [ρ x] ⇧@ (Suc (e⇩ρ x -1) + Suc (e⇩ρ x - 1))"
unfolding Suc_minus_pos[OF primroot_exp_nemp[OF ‹x ≠ ε›]]
root_ref_def by (simp add: pow_add)
hence "[ρ x, ρ x] ≤f Ref⇩ρ [x,x]"
by auto
thus "[ρ x, ρ x] ≤f ws' ⋅ ws'"
using fac_trans[OF _ ‹Ref⇩ρ [x,x] ≤f ws' ⋅ ws'›] by blast
have "Suc (Suc (e⇩ρ y + e⇩ρ y - 2)) = e⇩ρ y + e⇩ρ y"
using Suc_minus2 primroot_exp_nemp[OF ‹y ≠ ε›] by simp
have "Ref⇩ρ [y,y] = [ρ y] ⇧@ (Suc (e⇩ρ y -1) + Suc (e⇩ρ y - 1))"
unfolding Suc_minus_pos[OF primroot_exp_nemp[OF ‹y ≠ ε›]] root_ref_def
by (simp add: pow_add)
hence "[ρ y, ρ y] ≤f Ref⇩ρ [y,y]"
by auto
thus "[ρ y, ρ y] ≤f ws' ⋅ ws'"
using fac_trans[OF _ ‹Ref⇩ρ [y,y] ≤f ws' ⋅ ws'›] by blast
show "primitive (ρ x)" and "primitive (ρ y)"
using primroot_prim ‹x ≠ ε› ‹y ≠ ε› by blast+
qed
subsection ‹Obtaining the square of the longer word (gluing)›
lemma bin_imprim_longer_twice:
assumes "x ⋅ y ≠ y ⋅ x"
and "ws ∈ lists {x, y}"
and "❙|y❙| ≤ ❙|x❙|"
and "count_list ws x ≥ 2"
and "primitive ws" and "¬ primitive (concat ws)"
shows "ws ∼ [x,x,y] ∧ primitive x ∧ primitive y"
using assms proof (induction "❙|ws❙|" arbitrary: x y ws rule: less_induct)
case less
then show ?case
proof (cases)
assume "[x, x] ≤f ws ⋅ ws ∧ [y, y] ≤f ws ⋅ ws"
with bin_imprim_both_squares[OF ‹x ⋅ y ≠ y ⋅ x› ‹ws ∈ lists {x,y}› ‹primitive ws› ‹ ¬ primitive (concat ws)›]
have False by blast
thus ?case by blast
next
assume missing_sq: "¬ ([x, x] ≤f ws ⋅ ws ∧ [y, y] ≤f ws ⋅ ws)"
then show ?case
proof (cases)
assume "count_list ws y < 2"
with bin_imprim_single_y[OF less.prems(1-4) this less.prems(5-6)]
show "ws ∼ [x,x,y] ∧ primitive x ∧ primitive y"
by blast
next
assume "¬ count_list ws y < 2" hence "2 ≤ count_list ws y" by simp
define x' where "x' = (if ¬ [x, x] ≤f ws ⋅ ws then x else y)"
define y' where "y' = (if ¬ [x, x] ≤f ws ⋅ ws then y else x)"
have "{x', y'} = {x, y}"
by (simp add: doubleton_eq_iff x'_def y'_def)
note cases = disjE[OF this[unfolded doubleton_eq_iff]]
have "¬ [x', x'] ≤f ws ⋅ ws"
using missing_sq x'_def by presburger
have "count_list ws x' ≥ 2" and "count_list ws y' ≥ 2"
unfolding x'_def y'_def using ‹2 ≤ count_list ws x› ‹2 ≤ count_list ws y› by presburger+
have "x' ⋅ y' ≠ y' ⋅ x'"
by (rule cases, simp_all add: ‹x ⋅ y ≠ y ⋅ x› ‹x ⋅ y ≠ y ⋅ x›[symmetric])
have "x' ≠ ε" and "x' ≠ y'" and "x' ⋅ y' ≠ y'"
using ‹x' ⋅ y' ≠ y' ⋅ x'› by auto
note prim_nemp[OF ‹primitive ws›]
hence rot: "last ws = x' ⟹ hd ws = x' ⟹ butlast ws ⋅ [x',x'] ⋅ tl ws = ws ⋅ ws"
using append_butlast_last_id hd_tl hd_word rassoc by metis
from this[THEN facI']
have "last ws = x' ⟹ hd ws ≠ x'"
using ‹¬ [x', x'] ≤f ws ⋅ ws› by blast
define ws' where "ws' = (if last ws ≠ x' then ws else tl ws ⋅ [hd ws])"
have cond: "ws' = ε ∨ last ws' ≠ x'"
unfolding ws'_def using ‹last ws = x' ⟹ hd ws ≠ x'› by simp
have "ws' ∼ ws"
unfolding ws'_def using ‹ws ≠ ε› by fastforce
hence counts': "count_list ws' x' ≥ 2" "count_list ws' y' ≥ 2"
by (simp_all add: ‹2 ≤ count_list ws x'› ‹2 ≤ count_list ws y'› count_list_conjug)
let ?ws = "glue x' ws'"
have c1: "❙|?ws❙| < ❙|ws❙|"
using len_glue[OF cond] conjug_len[OF ‹ws' ∼ ws›] ‹count_list ws' x' ≥ 2› by linarith
hence c2: "(x' ⋅ y') ⋅ y' ≠ y' ⋅ x' ⋅ y'"
using ‹x' ⋅ y' ≠ y' ⋅ x'› by force
have "ws' ≤f ws ⋅ ws"
using conjugE[OF ‹ws' ∼ ws›] rassoc sublist_appendI by metis
hence "¬ [x', x'] ≤f ws'"
using ‹¬ [x',x'] ≤f ws ⋅ ws› by blast
have "ws' ∈ lists {x',y'}"
using conjug_in_lists[OF ‹ws' ∼ ws› ‹ws ∈ lists {x,y}›[folded ‹{x',y'} = {x,y}›]].
have c3: "?ws ∈ lists {x' ⋅ y', y'}"
using single_bin_glue_in_lists[OF cond ‹¬ [x', x'] ≤f ws'› ‹ws' ∈ lists {x',y'}›].
have c4: "2 ≤ count_list (glue x' ws') (x' ⋅ y')"
using ‹2 ≤ count_list ws' x'›
unfolding count_list_single_bin_glue(1)[OF ‹x' ≠ ε› ‹x' ≠ y'› cond ‹ws' ∈ lists {x',y'}› ‹¬ [x',x'] ≤f ws'›].
from ‹primitive ws›[folded conjug_prim_iff[OF ‹ws' ∼ ws›]]
have c5: "primitive (glue x' ws')"
using prim_bin_glue [OF ‹ws' ∈ lists {x',y'}› ‹x' ≠ ε› cond] by blast
have "count_list ws' x' ≥ 2"
using ‹count_list ws x ≥ 2› ‹count_list ws y ≥ 2› ‹{x', y'} = {x, y}›
count_list_conjug[OF ‹ws' ∼ ws›] x'_def by metis
have "concat (glue x' ws') = concat ws'"
by (simp add: cond)
have c6: "¬ primitive (concat (glue x' ws'))"
unfolding ‹concat (glue x' ws') = concat ws'› using ‹¬ primitive (concat ws)› ‹ws' ∼ ws›
conjug_concat_conjug prim_conjug by metis
from less.hyps[OF c1 c2 c3 _ c4 c5 c6]
have "glue x' ws' ∼ [x' ⋅ y', x' ⋅ y', y']" by simp
from prim_xyxyy[OF ‹x' ⋅ y' ≠ y' ⋅ x'›] conjug_prim_iff[OF conjug_concat_conjug[OF this]]
have False
using ‹¬ primitive (concat (glue x' ws'))› by simp
thus ?case by blast
qed
qed
qed
lemma bin_imprim_both_twice:
assumes "x ⋅ y ≠ y ⋅ x"
and "ws ∈ lists {x, y}"
and "count_list ws x ≥ 2"
and "count_list ws y ≥ 2"
and "primitive ws" and "¬ primitive (concat ws)"
shows False
proof-
have "x ≠ y"
using ‹x ⋅ y ≠ y ⋅ x› by blast
from bin_imprim_longer_twice[OF assms(1-2) _ assms(3) assms(5-6)]
bin_imprim_longer_twice[OF assms(1)[symmetric] assms(2)[unfolded insert_commute[of x]] _ assms(4) assms(5-6)]
have or: "ws ∼ [x, x, y] ∨ ws ∼ [y, y, x]" by linarith
thus False
proof (rule disjE)
assume "ws ∼ [x, x, y]"
from ‹count_list ws y ≥ 2›[unfolded count_list_conjug[OF this]]
show False
using ‹x ≠ y› by force
next
assume "ws ∼ [y, y, x]"
from ‹count_list ws x ≥ 2›[unfolded count_list_conjug[OF this]]
show False
using ‹x ≠ y› by force
qed
qed
section ‹Examples›
lemma "x ≠ ε ⟹ ε (x⋅x) ε ∼⇩ℐ [x,x]"
unfolding factor_interpretation_def
by simp
lemma assumes "x = [(0::nat),1,0,1,0]" and "y = [1,0,0,1]"
shows "[0,1] (x⋅x) [1,0] ∼⇩ℐ [x,y,x]"
unfolding factor_interpretation_def assms by (simp add: suffix_def)
section "Primitivity non-preserving binary code"
text‹In this section, we give the final form of imprimitive words over a given
binary code @{term "{x,y}"}.
We start with a lemma, then we show that the only possibility is that such
word is conjugate with @{term "x⇧@j ⋅ y⇧@k"}.›
lemma bin_imprim_expsE_y: assumes "x ⋅ y ≠ y ⋅ x" and
"ws ∈ lists {x,y}" and
"2 ≤ ❙|ws❙|" and
"primitive ws" and
"¬ primitive (concat ws)" and
"count_list ws y = 1"
obtains j k where "1 ≤ j" "1 ≤ k" "j = 1 ∨ k = 1"
"ws ∼ [x]⇧@j ⋅ [y]⇧@k"
proof-
have "x ≠ y" using ‹x ⋅ y ≠ y ⋅ x› by blast
obtain j1 j2 where "[x]⇧@j1⋅[y]⋅[x]⇧@j2 = ws"
using bin_count_one_decompose[OF ‹ws ∈ lists {x,y}› ‹x ≠ y› ‹count_list ws y = 1›].
have "1 ≤ j2 + j1"
using ‹[x] ⇧@ j1 ⋅ [y] ⋅ [x] ⇧@ j2 = ws› ‹2 ≤ ❙|ws❙|› not_less_eq_eq by fastforce
have "ws ∼ [x]⇧@(j2+j1)⋅[y]⇧@1"
using conjugI'[of "[x] ⇧@ j1 ⋅ [y]" "[x] ⇧@ j2"]
unfolding ‹[x] ⇧@ j1 ⋅ [y] ⋅ [x] ⇧@ j2 = ws›[symmetric] pow_add rassoc pow_list_1.
from that[OF ‹1 ≤ j2 + j1› _ _ this]
show ?thesis
by blast
qed
lemma bin_imprim_expsE: assumes "x ⋅ y ≠ y ⋅ x" and
"ws ∈ lists {x,y}" and
"2 ≤ ❙|ws❙|" and
"primitive ws" and
"¬ primitive (concat ws)"
obtains j k where "1 ≤ j" "1 ≤ k" "j = 1 ∨ k = 1"
"ws ∼ [x]⇧@j ⋅ [y]⇧@k"
proof-
note ‹ws ∈ lists {x,y}›[unfolded insert_commute[of x]]
from ‹ws ∈ lists {x,y}›
sing_lists_exp_len[of ws y]
prim_exp_one[OF ‹primitive ws›, of "❙|ws❙|" "[y]"]
have "count_list ws x ≠ 0"
using ‹2 ≤ ❙|ws❙|› unfolding count_list_0_iff by force
from ‹ws ∈ lists {y,x}›
sing_lists_exp_len[of ws x]
prim_exp_one[OF ‹primitive ws›, of "❙|ws❙|" "[x]"]
have "count_list ws y ≠ 0"
using ‹2 ≤ ❙|ws❙|› unfolding count_list_0_iff by fastforce
consider "count_list ws x = 1" | "count_list ws y = 1"
using bin_imprim_both_twice[OF ‹x ⋅ y ≠ y ⋅ x› ‹ws ∈ lists {x,y}› _ _
‹primitive ws› ‹¬ primitive (concat ws)›]
‹count_list ws x ≠ 0› ‹count_list ws y ≠ 0›
unfolding One_less_Two_le_iff[symmetric] less_one[symmetric] by fastforce
thus thesis
proof(cases)
assume ‹count_list ws x = 1›
from bin_imprim_expsE_y[reversed, OF ‹x ⋅ y ≠ y ⋅ x› ‹ws ∈ lists {y, x}› ‹2 ≤ ❙|ws❙|›
‹primitive ws› ‹¬ primitive (concat ws)› ‹count_list ws x = 1›]
show thesis
using that by metis
next
assume ‹count_list ws y = 1›
from bin_imprim_expsE_y[OF ‹x ⋅ y ≠ y ⋅ x› ‹ws ∈ lists {x, y}› ‹2 ≤ ❙|ws❙|›
‹primitive ws› ‹¬ primitive (concat ws)› ‹count_list ws y = 1›]
show ?thesis
using that.
qed
qed
subsection ‹The target theorem›
text‹Given a binary code @{term "{x,y}"} such that there is a primitive factorisation
@{term ws} over it whose concatenation is imprimitive, we finally show that there are
integers @{term j} and @{term k} (depending only on @{term "{x,y}"}) such that
any other such factorisation @{term ws'} is conjugate to @{term "[x]⇧@j ⋅ [y]⇧@k"}.›
theorem bin_imprim_code: assumes "x ⋅ y ≠ y ⋅ x" and "ws ∈ lists {x,y}" and
"2 ≤ ❙|ws❙|" and "primitive ws" and "¬ primitive (concat ws)"
obtains j k where "1 ≤ j" and "1 ≤ k" and "j = 1 ∨ k = 1"
"⋀ws. ws ∈ lists {x,y} ⟹ 2 ≤ ❙|ws❙| ⟹
(primitive ws ∧ ¬ primitive (concat ws) ⟷ ws ∼ [x]⇧@j ⋅ [y]⇧@k)" and
"❙|y❙| ≤ ❙|x❙| ⟹ 2 ≤ j ⟹ j = 2 ∧ primitive x ∧ primitive y" and
"❙|y❙| ≤ ❙|x❙| ⟹ 2 ≤ k ⟹ j = 1 ∧ primitive x"
proof-
obtain j k where "1 ≤ j" "1 ≤ k" "j = 1 ∨ k = 1"
"ws ∼ [x]⇧@j ⋅ [y]⇧@k"
using bin_imprim_expsE[OF ‹x ⋅ y ≠ y ⋅ x›]
using assms by metis
have "¬ primitive (x⇧@j ⋅ y⇧@k)"
using ‹¬ primitive (concat ws)›
unfolding concat_morph concat_pow_list_single
conjug_prim_iff[OF conjug_concat_conjug[OF ‹ws ∼ [x] ⇧@ j ⋅ [y] ⇧@ k›]].
from not_prim_primroot_expE[OF this]
obtain z l where [symmetric]: "z⇧@l = x⇧@j ⋅ y⇧@k" and "2 ≤ l".
show thesis
proof (rule that[of j k ])
show "1 ≤ j" "1 ≤ k" "j = 1 ∨ k = 1" by fact+
fix ws'
assume hyps: "ws' ∈ lists {x,y}" "2 ≤ ❙|ws'❙|"
show "primitive ws' ∧ ¬ primitive (concat ws') ⟷ ws' ∼ [x]⇧@j ⋅ [y]⇧@k"
proof
assume " primitive ws' ∧ ¬ primitive (concat ws')"
hence prems: "primitive ws'" "¬ primitive (concat ws')" by blast+
obtain j' k' where "1 ≤ j'" "1 ≤ k'" "j' = 1 ∨ k' = 1"
"ws' ∼ [x]⇧@j' ⋅ [y]⇧@k'"
using bin_imprim_expsE[OF ‹x ⋅ y ≠ y ⋅ x› hyps prems].
have "¬ primitive (x ⇧@ j'⋅ y ⇧@ k')"
using ‹¬ primitive (concat ws')›
unfolding concat_morph concat_pow_list_single
conjug_prim_iff[OF conjug_concat_conjug[OF ‹ws' ∼ [x] ⇧@ j' ⋅ [y] ⇧@ k'›]].
have "j = j'" "k = k'"
using LS_unique[OF ‹x ⋅ y ≠ y ⋅ x›
_ _ ‹¬ primitive (x ⇧@ j ⋅ y ⇧@ k)›
_ _ ‹¬ primitive (x ⇧@ j'⋅ y ⇧@ k')›] ‹1 ≤ j› ‹1 ≤ k› ‹1 ≤ j'› ‹1 ≤ k'› by force+
show "ws' ∼ [x] ⇧@ j ⋅ [y] ⇧@ k"
unfolding ‹j = j'› ‹k = k'› by fact
next
assume "ws' ∼ [x]⇧@j ⋅ [y]⇧@k"
note conjug_trans[OF ‹ws ∼ [x]⇧@j ⋅ [y]⇧@k› conjug_sym[OF this]]
from prim_conjug[OF ‹primitive ws› this]
‹¬ primitive (concat ws)›[unfolded conjug_concat_prim_iff[OF ‹ws ∼ ws'›]]
show "primitive ws' ∧ ¬ primitive (concat ws')" by blast
qed
next
assume "❙|y❙| ≤ ❙|x❙|"
interpret LS_len_le x y j k l z
by unfold_locales fact+
assume "2 ≤ j"
with jk_small
have "k = 1" by fastforce
from case_j2k1[OF ‹2 ≤ j› this]
show "j = 2 ∧ primitive x ∧ primitive y"
by blast
next
assume "❙|y❙| ≤ ❙|x❙|"
interpret LS_len_le x y j k l z
by unfold_locales fact+
assume "2 ≤ k"
show "j = 1 ∧ primitive x"
using ‹2 ≤ k› ‹j = 1 ∨ k = 1› case_j1k2_primitive by auto
qed
qed
definition bin_imprim_code where "bin_imprim_code x y ≡ x ⋅ y ≠ y ⋅ x ∧ (¬ bin_prim x y)"
theorem bin_imprim_code': assumes "bin_imprim_code x y"
obtains j k where "1 ≤ j" and "1 ≤ k" and "j = 1 ∨ k = 1"
"⋀ws. ws ∈ lists {x,y} ⟹ 2 ≤ ❙|ws❙| ⟹
(primitive ws ∧ ¬ primitive (concat ws) ⟷ ws ∼ [x]⇧@j ⋅ [y]⇧@k)" and
"❙|y❙| ≤ ❙|x❙| ⟹ 2 ≤ j ⟹ j = 2 ∧ primitive x ∧ primitive y" and
"❙|y❙| ≤ ❙|x❙| ⟹ 2 ≤ k ⟹ j = 1 ∧ primitive x"
proof-
thm bin_imprim_code
obtain ws where "x ⋅ y ≠ y ⋅ x"
and "ws ∈ lists {x,y}" and "2 ≤ ❙|ws❙|" and "primitive ws" and "¬ primitive (concat ws)"
using assms unfolding bin_imprim_code_def bin_prim_altdef2 by metis
from bin_imprim_code[OF this] that
show thesis
by blast
qed
end