Theory Binary_Code_Morphisms
theory Binary_Code_Morphisms
imports CoWBasic Submonoids Morphisms
begin
chapter "Binary alphabet and binary morphisms"
section "Datatype of a binary alphabet"
text‹Basic elements for construction of binary words.›
type_notation Enum.finite_2 ("binA")
notation finite_2.a⇩1 ("bina")
notation finite_2.a⇩2 ("binb")
lemmas bin_distinct = Enum.finite_2.distinct
lemmas bin_exhaust = Enum.finite_2.exhaust
lemmas bin_induct = Enum.finite_2.induct
lemmas bin_UNIV = Enum.UNIV_finite_2
lemmas bin_eq_neq_iff = Enum.neq_finite_2_a⇩2_iff
lemmas bin_eq_neq_iff' = Enum.neq_finite_2_a⇩1_iff
abbreviation bin_word_a :: "binA list" ("𝔞") where
"bin_word_a ≡ [bina]"
abbreviation bin_word_b :: "binA list" ("𝔟") where
"bin_word_b ≡ [binb]"
abbreviation binUNIV :: "binA set" where "binUNIV ≡ UNIV"
lemma binUNIV_I [simp, intro]: "bina ∈ A ⟹ binb ∈ A ⟹ A = UNIV"
unfolding UNIV_finite_2 by auto
lemma bin_basis_code: "code {𝔞,𝔟}"
by (rule bin_code_code) blast
lemma bin_num: "bina = 0" "binb = 1"
by simp_all
lemma binA_simps [simp]: "bina - binb = binb" "binb - bina = binb" "1 - bina = binb" "1 - binb = bina" "a - a = bina" "1 - (1 - a) = a"
by simp_all
definition bin_swap :: "binA ⇒ binA" where "bin_swap x ≡ 1 - x"
lemma bin_swap_if_then: "1-x = (if x = bina then binb else bina)"
by fastforce
definition bin_swap_morph where "bin_swap_morph ≡ map bin_swap"
lemma alphabet_or[simp]: "a = bina ∨ a = binb"
by auto
lemma bin_im_or: "f [a] = f 𝔞 ∨ f [a] = f 𝔟"
by (rule bin_exhaust[of a], simp_all)
thm triv_forall_equality
lemma binUNIV_card: "card binUNIV = 2"
unfolding bin_UNIV card_2_iff by auto
lemma other_letter: obtains b where "b ≠ (a :: binA)"
using finite_2.distinct(1) by metis
lemma alphabet_or_neq: "x ≠ y ⟹ x = (a :: binA) ∨ y = a"
using alphabet_or[of x] alphabet_or[of y] alphabet_or[of a] by argo
lemma binA_neq_cases: assumes neq: "a ≠ b"
obtains "a = bina" and "b = binb" | "a = binb" and "b = bina"
using alphabet_or_neq assms by auto
lemma bin_neq_sym_pred: assumes "a ≠ b" and "P bina binb" and "P binb bina" shows "P a b"
using assms(2-3) binA_neq_cases[OF ‹a ≠ b›, of "P a b"] by blast
lemma no_third: "(c :: binA) ≠ a ⟹ b ≠ a ⟹ b = c"
using alphabet_or[of a] by fastforce
lemma two_in_bin_UNIV: assumes "a ≠ b" and "a ∈ S" and "b ∈ S" shows "S = binUNIV"
using ‹a ∈ S› ‹b ∈ S› alphabet_or_neq[OF ‹a ≠ b›] by fast
lemmas two_in_bin_set = two_in_bin_UNIV[unfolded bin_UNIV]
lemma bin_not_comp_set_UNIV: assumes "¬ u ⨝ v" shows "set (u ⋅ v) = binUNIV"
proof-
have uv: "u ⋅ v = ((u ∧⇩p v) ⋅ ([hd ((u ∧⇩p v)¯⇧>u)] ⋅ tl ((u ∧⇩p v)¯⇧>u))) ⋅ (u ∧⇩p v) ⋅ ([hd ((u ∧⇩p v)¯⇧>v)] ⋅ tl ((u ∧⇩p v)¯⇧>v))"
unfolding hd_tl[OF lcp_mismatch_lq(1)[OF assms]] hd_tl[OF lcp_mismatch_lq(2)[OF assms]] lcp_lq..
from this[unfolded rassoc]
have "hd ((u ∧⇩p v)¯⇧>u) ∈ set (u ⋅ v)" and "hd ((u ∧⇩p v)¯⇧>v) ∈ set (u ⋅ v)"
unfolding uv by simp_all
with lcp_mismatch_lq(3)[OF assms]
show ?thesis
using two_in_bin_UNIV by blast
qed
lemma bin_basis_singletons: "{[q] |q. q ∈ {bina, binb}} = {𝔞,𝔟}"
by blast
lemma bin_basis_generates: "⟨{𝔞,𝔟}⟩ = UNIV"
using sings_gen_lists[of binUNIV, unfolded lists_UNIV bin_UNIV bin_basis_singletons, folded bin_UNIV, unfolded lists_UNIV].
lemma a_in_bin_basis: "[a] ∈ {𝔞,𝔟}"
using Set.UNIV_I by auto
lemma lcp_zero_one_emp: "𝔞 ∧⇩p 𝔟 = ε" and lcp_one_zero_emp: "𝔟 ∧⇩p 𝔞 = ε"
by simp+
lemma bin_neq_induct: "(a::binA) ≠ b ⟹ P a ⟹ P b ⟹ P c"
proof (elim binA_neq_cases)
show " P a ⟹ P b ⟹ a = bina ⟹ b = binb ⟹ P c"
using finite_2.induct by blast
show " P a ⟹ P b ⟹ a = binb ⟹ b = bina ⟹ P c"
using finite_2.induct by blast
qed
lemma bin_neq_induct': assumes"(a::binA) ≠ b" and "P a" and "P b" shows "⋀ c. P c"
using bin_neq_induct[OF assms] by blast
lemma neq_exhaust: assumes "(a::binA) ≠ b" obtains "c = a" | "c = b"
using assms by (elim binA_neq_cases) (hypsubst, elim finite_2.exhaust, assumption)+
lemma bin_swap_neq [simp]: "1-(a :: binA) ≠ a"
by simp
lemmas bin_swap_neq'[simp] = bin_swap_neq[symmetric]
lemmas bin_swap_induct = bin_neq_induct[OF bin_swap_neq']
and bin_swap_exhaust = neq_exhaust[OF bin_swap_neq']
lemma bin_swap_induct': "P (a :: binA) ⟹ P (1-a) ⟹ (⋀ c. P c)"
using bin_swap_induct by auto
lemma swap_UNIV: "{a, 1-a} = binUNIV" (is "?P a")
using bin_swap_induct[of ?P bina, unfolded binA_simps] by fastforce
lemma bin_neq_swap'[intro]: "a ≠ b ⟹ 1 - b = (a :: binA)"
by (rule bin_swap_exhaust[of a b]) blast+
lemma bin_neq_swap[intro]: "a ≠ b ⟹ 1 - a = (b :: binA)"
using bin_neq_swap' by auto
lemma bin_neq_swap''[intro]: "a ≠ b ⟹ b = 1-(a:: binA)"
using bin_neq_swap by blast
lemma bin_neq_swap'''[intro]: "a ≠ b ⟹ a = 1-(b:: binA)"
using bin_neq_swap by blast
lemma bin_neq_iff: "c ≠ d ⟷ 1 - d = (c :: binA)"
using bin_neq_swap[of d c] bin_swap_neq[of d] by argo
lemma bin_neq_iff': "c ≠ d ⟷ 1 - c = (d :: binA)"
unfolding bin_neq_iff by force
lemma binA_neq_cases_swap: assumes neq: "a ≠ (b :: binA)"
obtains "a = c" and "b = 1 - c" | "a = 1 - c" and "b = c"
using assms bin_neq_swap bin_swap_exhaust[of a c] by metis
lemma im_swap_neq: "f a = f b ⟹ f bina ≠ f binb ⟹ a = b"
using binA_neq_cases_swap[of a b bina False, unfolded binA_simps] by fastforce
lemma bin_without_letter: assumes "(a1 :: binA) ∉ set w"
obtains k where "w = [1-a1]⇧@k"
proof-
have "∀ c. c ∈ set w ⟶ c = 1-a1"
using assms bin_swap_exhaust by blast
from that unique_letter_wordE'[OF this]
show thesis by blast
qed
lemma bin_empty_iff: "S = {} ⟷ (a :: binA) ∉ S ∧ 1-a ∉ S"
using bin_swap_induct[of "λa. a ∉ S"] by blast
lemma bin_UNIV_iff: "S = binUNIV ⟷ a ∈ S ∧ 1-a ∈ S"
using two_in_bin_UNIV[OF bin_swap_neq'] by blast
lemma bin_UNIV_I: "a ∈ S ⟹ 1-a ∈ S ⟹ S = binUNIV"
using bin_UNIV_iff by blast
lemma bin_sing_iff: "A = {a :: binA} ⟷ a ∈ A ∧ 1-a ∉ A"
proof (rule sym, intro iffI conjI, elim conjE)
assume "a ∈ A" and "1-a ∉ A"
have "b ∈ A ⟷ b = a" for b
using ‹a ∈ A› ‹1-a ∉ A› bin_swap_neq
by (intro bin_swap_induct[of "λc. (c ∈ A) = (c = a)" a b]) blast+
then show "A = {a}" by blast
qed simp_all
lemma bin_set_cases: obtains "S = {}" | "S = {bina}" | "S = {binb}" | "S = binUNIV"
unfolding bin_empty_iff[of _ "bina"] bin_UNIV_iff[of _ "bina"] bin_sing_iff
by fastforce
lemma not_UNIV_E: assumes "A ≠ binUNIV" obtains a where "A ⊆ {a}"
using assms by (cases rule: bin_set_cases[of A]) auto
lemma not_UNIV_nempE: assumes "A ≠ binUNIV" and "A ≠ {}" obtains a where "A = {a}"
using assms by (cases rule: bin_set_cases[of A]) auto
lemma bin_sing_gen_iff: "x ∈ ⟨{[a]}⟩ ⟷ 1-(a :: binA) ∉ set x"
unfolding sing_gen_lists[symmetric] in_lists_conv_set using bin_empty_iff bin_sing_iff by metis
lemma set_hd_pow_conv: "w ∈ [hd w]* ⟷ set w ≠ binUNIV"
unfolding root_sing_set_iff
proof
assume "set w ⊆ {hd w}"
thus "set w ≠ binUNIV"
unfolding bin_UNIV using bin_distinct(1) by force
next
assume "set w ≠ binUNIV"
thus "set w ⊆ {hd w}"
proof (cases "w = ε")
assume "set w ≠ binUNIV" and "w ≠ ε"
from hd_tl[OF this(2)] this(2)
have "hd w ∈ set w" by simp
hence "1-hd w ∉ set w"
using ‹set w ≠ binUNIV› unfolding bin_UNIV_iff[of "set w" "hd w"] by blast
thus "set w ⊆ {hd w}"
using bin_sing_iff by auto
qed simp
qed
lemma not_swap_eq: "P a b ⟹ (⋀ (c :: binA). ¬ P c (1-c)) ⟹ a = b"
using bin_neq_iff by metis
lemma bin_distinct_letter: assumes "set w = binUNIV"
obtains k w' where "[hd w]⇧@Suc k ⋅ [1-hd w] ⋅ w' = w"
proof-
from distinct_letter_in_hd'[of w, unfolded set_hd_pow_conv[of w] bool_simps(1), OF assms]
obtain m b q where "[hd w] ⇧@ Suc m ⋅ [b] ⋅ q = w" "b ≠ hd w".
with that bin_neq_swap'[OF this(2)]
show thesis
by blast
qed
lemma "P a ⟷ P (1-a) ⟹ P a ⟹ (⋀ (b :: binA). P b)"
using bin_swap_induct' by blast
lemma bin_sym_all: "P (a :: binA) ⟷ P (1-a) ⟹ P a ⟹ P x"
using bin_swap_induct[of "λ a. P a" a, unfolded binA_simps] by blast
lemma bin_sym_all_comm:
"f [a] ⋅ f [1-a] ≠ f [1-a] ⋅ f [a] ⟹ f [b] ⋅ f [1-b] ≠ f [1-b] ⋅ f [(b :: binA)]" (is "?P a ⟹ ?P b")
using bin_sym_all[of ?P a, unfolded binA_simps, OF neq_commute].
lemma bin_sym_all_neq:
"f [(a :: binA)] ≠ f [1-a] ⟹ f [b] ≠ f [1-b]" (is "?P a ⟹ ?P b")
using bin_sym_all[of ?P a, unfolded binA_simps, OF neq_commute].
lemma bin_len_count:
fixes w :: "binA list"
shows "❙|w❙| = count_list w a + count_list w (1-a)"
using sum_count_set[of w "{a,1-a}"] swap_UNIV by force
lemma bin_len_count':
fixes w :: "binA list"
shows "❙|w❙| = count_list w bina + count_list w binb"
using bin_len_count[of w bina] by force
section ‹Binary morphisms›
lemma bin_map_core_lists: "(map f⇧𝒞 w) ∈ lists {f 𝔞, f 𝔟}"
unfolding core_def by (induct w, simp, unfold map_hd)
(rule append_in_lists, simp_all add: bin_im_or)
lemma bin_range: "range f = {f bina, f binb}"
unfolding bin_UNIV by simp
lemma bin_core_range: "range f⇧𝒞 = {f 𝔞, f 𝔟}"
unfolding core_def bin_range..
lemma bin_core_range_swap: "range f⇧𝒞 = {f [(a :: binA)], f [1-a]}" (is "?P a")
by (rule bin_induct[of ?P, unfolded binA_simps], unfold bin_core_range, simp, force)
lemma bin_map_core_lists_swap: "(map f⇧𝒞 w) ∈ lists {f [(a :: binA)], f [1-a]}"
using map_core_lists[of f, unfolded bin_core_range_swap[of f a]].
locale binary_morphism = morphism f
for f :: "binA list ⇒ 'a list"
begin
lemma bin_len_count_im:
fixes a :: binA
shows "❙|f w❙| = count_list w a * ❙|f [a]❙| + count_list w (1-a) * ❙|f [1-a]❙|"
proof (induct w)
case (Cons b w)
show ?case
unfolding hd_word[of b w] morph lenmorph Cons.hyps count_list_append
by (induct a) simp_all
qed simp
lemma bin_len_count_im':
shows "❙|f w❙| = count_list w bina * ❙|f 𝔞❙| + count_list w binb * ❙|f 𝔟❙|"
proof (induct w)
case (Cons a w)
show ?case
unfolding hd_word[of a w] morph lenmorph Cons.hyps count_list_append
by (induct a) simp_all
qed simp
lemma bin_neq_inj_core: assumes "f [a] ≠ f [1-a]" shows "inj f⇧𝒞"
proof
show "f⇧𝒞 x = f⇧𝒞 y ⟹ x = y" for x y
proof (rule ccontr)
assume "x ≠ y"
from bin_sym_all_neq[OF assms]
have "f⇧𝒞 x ≠ f⇧𝒞 y"
unfolding core_def bin_neq_swap''[OF ‹x ≠ y›].
thus "f⇧𝒞 x = f⇧𝒞 y ⟹ False"
by blast
qed
qed
lemma bin_code_morphism_inj: assumes "f [a] ⋅ f [1-a] ≠ f [1-a] ⋅ f [a]"
shows "inj f"
unfolding inj_on_def
proof (rule ballI, rule ballI, rule impI)
have "f [b] ≠ f [1-b]" for b
using bin_sym_all_comm[OF assms, of b] by force
from bin_neq_inj_core[OF this]
have "inj f⇧𝒞".
fix xs ys assume "f xs = f ys"
hence "concat (map f⇧𝒞 xs) = concat (map f⇧𝒞 ys)"
unfolding morph_concat_map.
from bin_code_code[unfolded code_def, rule_format,
OF ‹f [a] ⋅ f [1-a] ≠ f [1-a] ⋅ f [a]› bin_map_core_lists_swap bin_map_core_lists_swap this]
show "xs = ys"
using ‹inj f⇧𝒞› by simp
qed
lemma bin_code_morphismI: "f [a] ⋅ f [1-a] ≠ f [1-a] ⋅ f [a] ⟹ code_morphism f"
using code_morphismI[OF bin_code_morphism_inj].
end
subsection ‹Binary periodic morphisms›
locale binary_periodic_morphism = periodic_morphism f
for f :: "binA list ⇒ 'a list"
begin
sublocale binary_morphism
by unfold_locales
definition fn0 where "fn0 ≡ (SOME n. f 𝔞 = mroot⇧@n)"
definition fn1 where "fn1 ≡ (SOME n. f 𝔟 = mroot⇧@n)"
lemma bin0_im: "f 𝔞 = mroot⇧@fn0"
using per_morph_rootI[rule_format, of 𝔞] someI[of "λ n. f 𝔞 = mroot⇧@n"] unfolding fn0_def by blast
lemma bin1_im: "f 𝔟 = mroot⇧@fn1"
using per_morph_rootI[rule_format, of 𝔟] someI[of "λ n. f 𝔟 = mroot⇧@n"] unfolding fn1_def by blast
lemma sorted_image : "f w = (f [a])⇧@(count_list w a) ⋅ (f [1-a])⇧@(count_list w (1-a))"
proof-
obtain k where "f w = mroot⇧@k"
using per_morph_rootI by blast
have len: "❙|f w❙| = ❙|(f [a])⇧@(count_list w a) ⋅ (f [1-a])⇧@(count_list w (1-a))❙|"
using bin_len_count_im unfolding lenmorph pow_len.
have *: "(f [a])⇧@(count_list w a) ⋅ (f [1-a])⇧@(count_list w (1-a)) = mroot⇧@(fn0 * (count_list w bina) + fn1 * (count_list w binb))"
by (induct a) (unfold binA_simps bin0_im bin1_im, unfold pow_mult[symmetric] add_exps[symmetric], simp_all add: add.commute)
show ?thesis
using len nemp_len[OF prim_nemp[OF per_morph_root_prim]]
unfolding * ‹f w = mroot⇧@k› pow_len by force
qed
lemma bin_per_morph_expI: "f u = mroot⇧@((mexp bina) * (count_list u bina) + (mexp binb) * (count_list u binb))"
using sorted_image[of u bina, unfolded binA_simps]
by (simp add: add_exps per_morph_expI' pow_mult)
end
section ‹From two words to a binary morphism›
definition bin_morph_of' :: "'a list ⇒ 'a list ⇒ binA list ⇒ 'a list" where "bin_morph_of' x y u = concat (map (λ a. (case a of bina ⇒ x | binb ⇒ y)) u)"
definition bin_morph_of :: "'a list ⇒ 'a list ⇒ binA list ⇒ 'a list" where "bin_morph_of x y u = concat (map (λ a. if a = bina then x else y) u)"
lemma case_finite_2_if_else: "case_finite_2 x y = (λ a. if a = bina then x else y)"
by (standard, simp split: finite_2.split)
lemma bin_morph_of_case_def: "bin_morph_of x y u = concat (map (λ a. (case a of bina ⇒ x | binb ⇒ y)) u)"
unfolding bin_morph_of_def case_finite_2_if_else..
lemma case_finiteD: "case_finite_2 (f 𝔞) (f 𝔟) = f⇧𝒞"
proof
show "(case x of bina ⇒ f 𝔞 | binb ⇒ f 𝔟) = f⇧𝒞 x" for x
unfolding core_def by (cases rule: finite_2.exhaust[of x]) auto
qed
lemma case_finiteD': "case_finite_2 (f 𝔞) (f 𝔟) u = f⇧𝒞 u"
using case_finiteD by metis
lemma bin_morph_of_maps: "bin_morph_of x y = List.maps (case_finite_2 x y)"
unfolding bin_morph_of_def maps_def unfolding case_finite_2_if_else by simp
lemma bin_morph_ofD: "(bin_morph_of x y) 𝔞 = x" "(bin_morph_of x y) 𝔟 = y"
unfolding bin_morph_of_def by simp_all
lemma bin_range_swap: "range f = {f (a::binA), f (1-a)}" (is "?P a")
using bin_swap_induct[of ?P bina] unfolding binA_simps bin_UNIV by auto
lemma bin_morph_of_core_range: "range (bin_morph_of x y)⇧𝒞 = {x,y}"
unfolding bin_core_range bin_morph_ofD..
lemma bin_morph_of_morph: "morphism (bin_morph_of x y)"
unfolding bin_morph_of_def by (simp add: morphism.intro)
lemma bin_morph_of_bin_morph: "binary_morphism (bin_morph_of x y)"
unfolding binary_morphism_def using bin_morph_of_morph.
lemma bin_morph_of_range: "range (bin_morph_of x y) = ⟨{x,y}⟩"
using morphism.range_hull[of "bin_morph_of x y", unfolded bin_morph_of_core_range, OF bin_morph_of_morph].
context binary_code
begin
lemma code_morph_of: "code_morphism (bin_morph_of u⇩0 u⇩1)"
using binary_morphism.bin_code_morphismI[OF bin_morph_of_bin_morph, of u⇩0 u⇩1 bina]
unfolding binA_simps bin_morph_ofD using non_comm.
lemma inj_morph_of: "inj (bin_morph_of u⇩0 u⇩1)"
using code_morphism.code_morph[OF code_morph_of].
end
section ‹Two binary morphism›
locale two_binary_morphisms = two_morphisms g h
for g h :: "binA list ⇒ 'a list"
begin
lemma eq_on_letters_eq: "g 𝔞 = h 𝔞 ⟹ g 𝔟 = h 𝔟 ⟹ g = h"
by (rule def_on_sings_eq, rule bin_induct) blast+
sublocale g: binary_morphism g
by unfold_locales
sublocale h: binary_morphism h
by unfold_locales
lemma rev_morphs: "two_binary_morphisms (rev_map g) (rev_map h)"
using rev_maps by (intro two_binary_morphisms.intro)
lemma solution_UNIV:
assumes "s ≠ ε" and "g s = h s" and "⋀a. g [a] ≠ h [a]"
shows "set s = UNIV"
proof (rule ccontr, elim not_UNIV_E unique_letter_wordE'')
fix a k assume *: "s = [a] ⇧@ k"
then have "0 < k" using ‹s ≠ ε› by blast
have "g [a] = h [a]" using ‹g s = h s› unfolding * g.pow_morph h.pow_morph
by (fact pow_eq_eq[OF _ ‹0 < k›])
then show False using ‹g [a] ≠ h [a]› by contradiction
qed
lemma solution_len_im_sing_less:
assumes sol: "g s = h s" and set: "a ∈ set s" and less: "❙|g [a]❙| < ❙|h [a]❙|"
shows "❙|h [1-a]❙| < ❙|g [1-a]❙|"
proof (intro not_le_imp_less notI)
assume "❙|g [1-a]❙| ≤ ❙|h [1-a]❙|"
with less_imp_le[OF less] have "❙|g [b]❙| ≤ ❙|h [b]❙|" for b
by (fact bin_swap_induct)
from this set less
have "❙|g s❙| < ❙|h s❙|" by (rule len_im_less[of s])
then show False using lenarg[OF sol] by simp
qed
lemma solution_len_im_sing_le:
assumes sol: "g s = h s" and set: "set s = UNIV" and less: "❙|g [a]❙| ≤ ❙|h [a]❙|"
shows "❙|h [1-a]❙| ≤ ❙|g [1-a]❙|"
proof (intro leI notI)
assume "❙|g [1-a]❙| < ❙|h [1-a]❙|"
from solution_len_im_sing_less[OF sol _ this]
have "❙|h [a]❙| < ❙|g [a]❙|" unfolding set binA_simps by blast
then show False using ‹❙|g [a]❙| ≤ ❙|h [a]❙|› by simp
qed
lemma solution_sing_len_cases:
assumes set: "set s = UNIV" and sol: "g s = h s" and "g ≠ h"
obtains a where "❙|g [a]❙| < ❙|h [a]❙|" and "❙|h [1-a]❙| < ❙|g [1-a]❙|"
proof (cases rule: linorder_cases)
show "❙|g [hd s]❙| < ❙|h [hd s]❙| ⟹ thesis"
using solution_len_im_sing_less[OF sol] that unfolding set by blast
interpret swap: two_binary_morphisms h g by unfold_locales
show "❙|h [hd s]❙| < ❙|g [hd s]❙| ⟹ thesis"
using swap.solution_len_im_sing_less[OF sol[symmetric]]
solution_len_im_sing_less[OF sol] that unfolding set by blast
have "s ≠ ε" using set by auto
assume *: "❙|g [hd s]❙| = ❙|h [hd s]❙|"
moreover have "❙|g [1 - (hd s)]❙| = ❙|h [1 - (hd s)]❙|"
proof (rule ccontr, elim linorder_neqE)
show "❙|g [1 - (hd s)]❙| < ❙|h [1 - (hd s)]❙| ⟹ False"
using solution_len_im_sing_less[OF sol, of "1 - (hd s)"]
unfolding set binA_simps * by blast
next
show "❙|h [1-(hd s)]❙| < ❙|g [1-(hd s)]❙| ⟹ False"
using swap.solution_len_im_sing_less[OF sol[symmetric], of "1 - (hd s)"]
unfolding set binA_simps * by blast
qed
ultimately have "❙|g [a]❙| = ❙|h [a]❙|" for a by (fact bin_swap_induct)
from def_on_sings[OF solution_eq_len_eq[OF sol this]]
show thesis unfolding set using ‹g ≠ h› by blast
qed
lemma len_ims_sing_neq:
assumes "g s = h s" "g ≠ h" "set s = binUNIV"
shows "❙|g [c]❙| ≠ ❙|h [c]❙|"
proof(rule solution_sing_len_cases[OF ‹set s = binUNIV› ‹g s = h s› ‹g ≠ h›])
fix a assume less: "❙|g [a]❙| < ❙|h [a]❙|" "❙|h [1 - a]❙| < ❙|g [1 - a]❙|"
show "❙|g [c]❙| ≠ ❙|h [c]❙|"
by (rule bin_swap_exhaust[of c a]) (use less in force)+
qed
end
lemma two_binary_morphismsI: "binary_morphism g ⟹ binary_morphism h ⟹ two_binary_morphisms g h"
unfolding binary_morphism_def two_binary_morphisms_def using two_morphisms.intro.
section ‹Binary code morphism›
subsection ‹Locale - binary code morphism›
locale binary_code_morphism = code_morphism "f :: binA list ⇒ 'a list" for f
begin
lemma morph_bin_morph_of: "f = bin_morph_of (f 𝔞) (f 𝔟)"
using morph_concat_map unfolding bin_morph_of_def case_finiteD
case_finite_2_if_else[symmetric] by simp
lemma non_comm_morph [simp]: "f [a] ⋅ f [1-a] ≠ f [1-a] ⋅ f [a]"
unfolding morph[symmetric] using code_morph_code bin_swap_neq by blast
lemma non_comp_morph: "¬ f [a] ⋅ f [1-a] ⨝ f [1-a] ⋅ f [a]"
using comm_comp_eq non_comm_morph by blast
lemma swap_non_comm_morph [simp, intro]: "a ≠ b ⟹ f [a] ⋅ f [b] ≠ f [b] ⋅ f [a]"
using bin_neq_swap non_comm_morph by blast
thm bin_core_range[of f]
lemma bin_code_morph_rev_map: "binary_code_morphism (rev_map f)"
unfolding binary_code_morphism_def using code_morphism_rev_map.
sublocale swap: binary_code "f 𝔟" "f 𝔞"
using non_comm_morph[of binb] unfolding binA_simps by unfold_locales
sublocale binary_code "f 𝔞" "f 𝔟"
using swap.bin_code_swap.
notation bin_code_lcp ("α") and
bin_code_lcs ("β") and
bin_code_mismatch_fst ("c⇩0") and
bin_code_mismatch_snd ("c⇩1")
term "bin_lcp (f 𝔞) (f 𝔟)"
abbreviation bin_morph_mismatch ("𝔠")
where "bin_morph_mismatch a ≡ bin_mismatch (f[a]) (f[1-a])"
abbreviation bin_morph_mismatch_suf ("𝔡")
where "bin_morph_mismatch_suf a ≡ bin_mismatch_suf (f[1-a]) (f[a])"
lemma bin_lcp_def': "α = f ([a] ⋅ [1-a]) ∧⇩p f ([1-a] ⋅ [a])"
by (rule bin_exhaust[of a "α = f ([a] ⋅ [1-a]) ∧⇩p f ([1-a] ⋅ [a])"],
unfold morph, use binA_simps(3-4) bin_lcp_def in force)
(unfold bin_lcp_def lcp_sym[of "f[a] ⋅ f[1-a]" "f[1-a] ⋅ f[a]"],
use binA_simps(3-4) in auto)
lemma bin_lcp_neq: "a ≠ b ⟹ α = f ([a] ⋅ [b]) ∧⇩p f ([b] ⋅ [a])"
using bin_neq_swap[of a b] unfolding bin_lcp_def'[of a] by blast
lemma sing_im: "f [a] ∈ {f 𝔞, f 𝔟}"
using finite_2.exhaust[of a ?thesis] by fastforce
lemma bin_mismatch_inj: "inj 𝔠"
unfolding inj_on_def
using non_comm_morph[folded bin_mismatch_comm] bin_neq_swap by force
lemma map_in_lists: "map (λx. f [x]) w ∈ lists {f 𝔞, f 𝔟}"
proof (induct w)
case (Cons a w)
then show ?case
unfolding list.map(2) using sing_im by simp
qed simp
lemma bin_morph_lcp_short: "❙|α❙| < ❙|f [a]❙| + ❙|f[1-a]❙|"
using finite_2.exhaust[of a ?thesis] bin_lcp_short by force
lemma swap_not_pref_bin_lcp: "¬ f([a] ⋅ [1-a]) ≤p α"
using pref_len[of "f [a] ⋅ f [1-a]" α] unfolding morph lenmorph using bin_morph_lcp_short[of a] by force
thm local.bin_mismatch_inj
lemma bin_mismatch_suf_inj: "inj 𝔡"
using binary_code_morphism.bin_mismatch_inj[OF bin_code_morph_rev_map, reversed].
lemma bin_lcp_sing: "bin_lcp (f [a]) (f [1-a]) = α"
unfolding bin_lcp_def
by (rule finite_2.exhaust[of a], simp_all add: lcp_sym)
lemma bin_lcs_sing: "bin_lcs (f [a]) (f [1-a]) = β"
unfolding bin_lcs_def
by (rule finite_2.exhaust[of a], simp_all add: lcs_sym)
lemma bin_code_morph_sing: "binary_code (f [a]) (f [1-a])"
unfolding binary_code_def
by (cases rule: binA_neq_cases[OF bin_swap_neq', of a]) simp_all
lemma bin_mismatch_swap_neq: "𝔠 a ≠ 𝔠 (1-a)"
using bin_code_morph_sing binary_code.bin_mismatch_neq by auto
lemma long_bin_lcp_hd: assumes "❙|f w❙| ≤ ❙|α❙|"
shows "w ∈ [hd w]*"
proof (rule ccontr)
assume "¬ w ∈ [hd w]*"
from distinct_letter_in_hd[OF this]
obtain m b suf where w: "[hd w]⇧@m ⋅ [b]⋅ suf = w" and "b ≠ hd w" and "m ≠ 0".
have ineq: "❙|f [b]❙| + ❙|f [hd w]❙| ≤ ❙|f w❙|"
using quotient_smaller[OF ‹m ≠ 0›, of "❙|f [hd w]❙|"]
unfolding arg_cong[OF w, of "λ x. ❙|f(x)❙|", unfolded morph lenmorph pow_morph pow_len, symmetric]
by linarith
hence "❙|f 𝔞❙| + ❙|f 𝔟❙| ≤ ❙|f w❙|"
using ‹b ≠ hd w› alphabet_or[of b] alphabet_or[of "hd w"] add.commute by fastforce
thus False
using bin_lcp_short ‹❙|f w❙| ≤ ❙|α❙|› by linarith
qed
thm nonerasing
nonerasing_morphism.nonerasing
lemmas nonerasing = nonerasing
thm nonerasing_morphism.nonerasing
binary_code_morphism.nonerasing
lemma bin_morph_lcp_mismatch_pref:
"α ⋅ [𝔠 a] ≤p f [a] ⋅ α"
using binary_code.bin_fst_mismatch[OF bin_code_morph_sing] unfolding bin_lcp_sing.
lemma "[𝔡 a] ⋅ β ≤s β ⋅ f [a]" using binary_code_morphism.bin_morph_lcp_mismatch_pref[OF bin_code_morph_rev_map, reversed].
lemma bin_lcp_pref_all: "α ≤p f w ⋅ α"
proof(induct w rule: rev_induct)
case (snoc x xs)
from pref_prolong[OF this, of "f[x]⋅α", unfolded lassoc]
show ?case
unfolding morph[of xs "[x]"] using bin_lcp_fst_lcp bin_lcp_snd_lcp alphabet_or[of x] by blast
qed simp
lemma bin_lcp_spref_all: "w ≠ ε ⟹ α <p f w ⋅ α"
using per_rootI[OF bin_lcp_pref_all] nemp_to_nemp by presburger
lemma pref_mono_lcp: assumes "w ≤p w'" shows "f w ⋅ α ≤p f w' ⋅ α"
proof-
from ‹w ≤p w'›
obtain z where "w' = w ⋅ z"
unfolding prefix_def by fast
show ?thesis
unfolding ‹w' = w ⋅ z› morph rassoc pref_cancel_conv using bin_lcp_pref_all.
qed
lemma long_bin_lcp: assumes "w ≠ ε" and "❙|f w❙| ≤ ❙|α❙|"
shows "w ∈ [hd w]*"
proof(rule ccontr)
assume "w ∉ [hd w]*"
obtain m b q where "[hd w]⇧@m ⋅ [b] ⋅ q = w" and "b ≠ hd w" and "m ≠ 0"
using distinct_letter_in_hd[OF ‹w ∉ [hd w]*›].
have ineq: "❙|f ([hd w]⇧@m ⋅ [b])❙| ≤ ❙|f w❙|"
using arg_cong[OF ‹[hd w] ⇧@ m ⋅ [b] ⋅ q = w›, of "λ x. ❙|f x❙|"]
unfolding morph lenmorph by force
have eq: "m*❙|f [hd w]❙| + ❙|f [b]❙| = ❙|f ([hd w]⇧@m ⋅ [b])❙|"
by (simp add: morph pow_len pow_morph)
have "❙|f [hd w]❙| + ❙|f [b]❙| ≤ m*❙|f [hd w]❙| + ❙|f [b]❙|"
using ineq ‹m ≠ 0› by simp
hence "❙|f [hd w]❙| + ❙|f [b]❙| ≤ ❙|f w❙|"
using eq ineq by linarith
hence "❙|f 𝔞❙| + ❙|f 𝔟❙| ≤ ❙|f w❙|"
using binA_neq_cases [OF ‹b ≠ hd w›] by fastforce
thus False
using bin_lcp_short ‹❙|f w❙| ≤ ❙|α❙|› by linarith
qed
thm sing_to_nemp
nonerasing
lemma bin_mismatch_code_morph: "c⇩0 = 𝔠 0" "c⇩1 = 𝔠 1"
unfolding bin_mismatch_def bin_lcp_def by simp_all
lemma bin_lcp_mismatch_pref_all: "α ⋅ [𝔠 a] ≤p f [a] ⋅ f w ⋅ α"
using pref_prolong[OF bin_fst_mismatch bin_lcp_pref_all[of w]]
pref_prolong[OF bin_snd_mismatch bin_lcp_pref_all[of w]]
unfolding bin_mismatch_code_morph
by (cases rule: finite_2.exhaust[of a]) simp_all
lemma bin_fst_mismatch_all: "α ⋅ [c⇩0] ≤p f 𝔞 ⋅ f w ⋅ α"
using pref_prolong[OF bin_fst_mismatch bin_lcp_pref_all[of w]].
lemma bin_snd_mismatch_all: "α ⋅ [c⇩1] ≤p f 𝔟 ⋅ f w ⋅ α"
using pref_prolong[OF bin_snd_mismatch bin_lcp_pref_all[of w]] by simp
lemma bin_long_mismatch: assumes "❙|α❙| < ❙|f w❙|" shows "α ⋅ [𝔠 (hd w)] ≤p f w"
proof-
have "w ≠ ε"
using assms emp_to_emp emp_len by force
have "f w = f[hd w] ⋅ f (tl w)"
unfolding pop_hd[symmetric] unfolding hd_word[of "hd w" "tl w"]
hd_tl[OF ‹w ≠ ε›]..
have "α ⋅ [𝔠 (hd w)] ≤p f w ⋅ α"
using bin_lcp_mismatch_pref_all[of "hd w" "tl w"]
unfolding lassoc ‹f w = f[hd w] ⋅ f (tl w)›[symmetric].
moreover have "❙|α ⋅ [𝔠 (hd w)]❙| ≤ ❙|f w❙|"
unfolding lenmorph sing_len using assms by linarith
ultimately show ?thesis by blast
qed
lemma sing_pow_mismatch: assumes "f [a] = [b]⇧@Suc n" shows "𝔠 a = b"
proof-
have aritm: "Suc n * Suc ❙|α❙| = Suc (n*❙|α❙| + n + ❙|α❙|)"
by auto
have set: "set ([b] ⇧@ (Suc n * Suc ❙|α❙|)) = {b}"
unfolding aritm using sing_pow_set_Suc.
have elem: "𝔠 a ∈ set (α ⋅ [𝔠 a])"
by simp
have hd: "hd ([a] ⇧@ Suc ❙|α❙|) = a"
by fastforce
let ?w = "[a]⇧@Suc ❙|α❙|"
have fw: "f ?w = [b]⇧@(Suc n*Suc ❙|α❙|)"
unfolding pow_mult assms[symmetric] pow_morph..
have "❙|α❙| < ❙|f ?w❙|"
unfolding fw pow_len sing_len by force
from set_mono_prefix[OF bin_long_mismatch[OF this, unfolded fw]]
show "𝔠 a = b"
unfolding hd set using elem by blast
qed
lemma sing_pow_mismatch_suf: "f [a] = [b]⇧@Suc n ⟹ 𝔡 a = b"
using binary_code_morphism.sing_pow_mismatch[OF bin_code_morph_rev_map, reversed].
lemma bin_lcp_swap_hd: "f [a] ⋅ f w ⋅ α ∧⇩p f [1-a] ⋅ f w' ⋅ α = α"
using lcp_first_mismatch[OF bin_mismatch_swap_neq, of α a]
bin_lcp_mismatch_pref_all[of a w] bin_lcp_mismatch_pref_all[of "1-a" w']
unfolding prefix_def rassoc by force
lemma bin_lcp_neq_hd: "a ≠ b ⟹ f [a] ⋅ f w ⋅ α ∧⇩p f [b] ⋅ f w' ⋅ α = α"
using bin_lcp_swap_hd bin_neq_swap by blast
lemma bin_mismatch_swap_not_comp: "¬ f [a] ⋅ f w ⋅ α ⨝ f [1-a] ⋅ f w' ⋅ α"
unfolding prefix_comparable_def lcp_pref_conv[symmetric] bin_lcp_swap_hd
bin_lcp_swap_hd[of "1-a", unfolded binA_simps] using sing_to_nemp by auto
lemma bin_lcp_root: "α <p f [a] ⋅ α"
using alphabet_or[of a] per_rootI[OF bin_lcp_pref_all[of 𝔟] bin_snd_nemp] per_rootI[OF bin_lcp_pref_all[of 𝔞] bin_fst_nemp] by blast
lemma bin_lcp_pref: assumes "w ∉ 𝔟*" and "w ∉ 𝔞*"
shows "α ≤p (f w)"
proof-
have "w ≠ ε"
using ‹¬ (w ∈ 𝔟*)› emp_all_roots by blast
have "w ∉ [hd w]*"
using assms alphabet_or[of "hd w"] by presburger
hence "❙|α❙| ≤ ❙|f w❙|"
using long_bin_lcp[OF ‹w ≠ ε›] nat_le_linear[of "❙|f w❙|" "❙|α❙|" ] by blast
show ?thesis
using pref_prod_le[OF bin_lcp_pref_all ‹❙|α❙| ≤ ❙|f w❙|›].
qed
lemma bin_lcp_pref'': "[a] ≤f w ⟹ [1-a] ≤f w ⟹ α ≤p (f w)"
using bin_lcp_pref[of w] sing_pow_fac'[OF bin_distinct(1),of w] sing_pow_fac'[OF bin_distinct(2), of w]
by (cases rule: finite_2.exhaust[of a]) force+
lemma bin_lcp_pref': "𝔞 ≤f w ⟹ 𝔟 ≤f w ⟹ α ≤p (f w)"
using bin_lcp_pref''[of bina, unfolded binA_simps].
lemma bin_lcp_mismatch_pref_all_set: assumes "1-a ∈ set w"
shows "α ⋅ [𝔠 a] ≤p f [a] ⋅ f w"
proof-
have "❙|f[1-a]❙| ≤ ❙|f w❙|"
using fac_len' morph split_list'[OF assms] by metis
hence "❙|α ⋅ [𝔠 a]❙| ≤ ❙|f [a] ⋅ f w❙|"
using bin_lcp_short unfolding lenmorph sing_len
by (cases rule: finite_2.exhaust[of a]) fastforce+
from bin_lcp_mismatch_pref_all[unfolded lassoc, THEN pref_prod_le, OF this]
show ?thesis.
qed
lemma bin_lcp_comp_hd: "α ⨝ f (𝔞 ⋅ w0) ∧⇩p f (𝔟 ⋅ w1)"
using ruler[OF bin_lcp_pref_all[of "𝔞 ⋅ w0"]
pref_trans[OF lcp_pref[of "f (𝔞 ⋅ w0)" "f (𝔟 ⋅ w1)"], of "f (𝔞 ⋅ w0) ⋅ α", OF triv_pref]]
unfolding prefix_comparable_def.
lemma sing_mismatch: assumes "f 𝔞 ∈ [a]*" shows "c⇩0 = a"
proof-
have "α ∈ [a]*"
using per_one[OF per_root_trans[OF bin_lcp_root assms]].
hence "f 𝔞 ⋅ α ∈ [a]*"
using ‹f 𝔞 ∈ [a]*› add_roots by blast
from sing_pow_fac'[OF _ this, of "c⇩0"]
show "c⇩0 = a"
using facI'[OF lq_pref[OF bin_fst_mismatch, unfolded rassoc]] by blast
qed
lemma sing_mismatch': assumes "f 𝔟 ∈ [a]*" shows "c⇩1 = a"
proof-
have "α ∈ [a]*"
using per_one[OF per_root_trans[OF bin_lcp_root assms]].
hence "f 𝔟 ⋅ α ∈ [a]*"
using ‹f 𝔟 ∈ [a]*› add_roots by blast
from sing_pow_fac'[OF _ this, of "c⇩1"]
show ?thesis
using facI'[OF lq_pref[OF bin_snd_mismatch, unfolded rassoc]] by blast
qed
lemma bin_lcp_comp_all: "α ⨝ (f w)"
unfolding prefix_comparable_def using ruler[OF bin_lcp_pref_all triv_pref].
lemma not_comp_bin_swap: "¬ f [a] ⋅ α ⨝ f [1-a] ⋅ α"
using not_comp_bin_fst_snd bin_exhaust[of a ?thesis]
unfolding prefix_comparable_def
by simp
lemma mismatch_pref:
assumes "α ≤p f ([a] ⋅ w0)" and "α ≤p f ([1-a] ⋅ w1)"
shows "α = f ([a] ⋅ w0) ∧⇩p f ([1-a] ⋅ w1)"
proof-
have "f ([a] ⋅ w0) ⋅ α ∧⇩p f ([1-a] ⋅ w1) ⋅ α = α"
unfolding morph using bin_lcp_swap_hd[unfolded lassoc].
hence "f ([a] ⋅ w0) ∧⇩p f ([1-a] ⋅ w1) ≤p α"
using lcp.mono[OF triv_pref[of "f ([a] ⋅ w0)" α] triv_pref[of "f ([1-a] ⋅ w1)" α]]
by presburger
moreover have "α ≤p f ([a] ⋅ w0) ∧⇩p f ([1-a] ⋅ w1)"
using assms pref_pref_lcp by blast
ultimately show ?thesis
using pref_antisym by blast
qed
lemma bin_set_UNIV_length: assumes "set w = UNIV" shows "❙|f [a]❙| + ❙|f [1-a]❙| ≤ ❙|f w❙|"
proof-
have "w ≠ ε"
using ‹set w = UNIV› by force
from set_ConsD[of "1- hd w" "hd w" "tl w", unfolded list.collapse[OF this] assms[folded swap_UNIV[of "hd w"]]]
have "1 - (hd w) ∈ set (tl w)"
using bin_swap_neq[of "hd w"] by blast
from in_set_morph_len[OF this]
have "❙|f [1-hd w]❙| ≤ ❙|f (tl w)❙|".
with lenarg[OF arg_cong[of _ _ f, OF hd_tl[OF ‹w ≠ ε›]]]
have "❙|f [hd w]❙| + ❙|f [1-hd w]❙| ≤ ❙|f w❙|"
unfolding morph lenmorph by linarith
thus ?thesis
using bin_swap_exhaust[of a "hd w" ?thesis] by force
qed
lemma set_UNIV_bin_lcp_pref: assumes "set w = UNIV" shows "α ⋅ [𝔠 (hd w)] ≤p f w"
using bin_long_mismatch[OF less_le_trans[OF bin_morph_lcp_short bin_set_UNIV_length[OF assms]]].
lemmas not_comp_bin_lcp_pref = bin_not_comp_set_UNIV[THEN set_UNIV_bin_lcp_pref]
lemma marked_lcp_conv: "marked_morphism f ⟷ α = ε"
proof
assume "marked_morphism f"
then interpret marked_morphism f by blast
from marked_core[unfolded core_def] core_nemp[unfolded core_def]
have "hd (f 𝔞 ⋅ f 𝔟) ≠ hd (f 𝔟 ⋅ f 𝔞)"
using hd_append finite_2.distinct by auto
thus "α = ε"
unfolding bin_lcp_def using lcp_distinct_hd by blast
next
assume "α = ε"
have "hd (f 𝔞) ≠ hd (f 𝔟)"
by (rule nemp_lcp_distinct_hd[OF sing_to_nemp sing_to_nemp])
(use lcp_append_monotone[of "f 𝔞" "f 𝔟" "f 𝔟" "f 𝔞", unfolded ‹α = ε›[unfolded bin_lcp_def]]
in simp)
show "marked_morphism f"
proof
fix a b :: binA assume "hd (f⇧𝒞 a) = hd (f⇧𝒞 b)"
from im_swap_neq[OF this[unfolded core_def] ‹hd (f 𝔞) ≠ hd (f 𝔟)›]
show "a = b".
qed
qed
lemma im_comm_lcp: "f w ⋅ α = α ⋅ f w ⟹ (∀ a. a ∈ set w ⟶ f [a] ⋅ α = α ⋅ f [a])"
proof (induct w)
case (Cons a w)
then show ?case
proof (cases "w = ε")
assume "w = ε"
show ?thesis
using Cons.prems(1) unfolding ‹w = ε› by force
next
assume "w ≠ ε"
have eq: "f [a] ⋅ f w ⋅ α = α ⋅ f [a] ⋅ f w"
unfolding morph[symmetric]
unfolding lassoc morph[symmetric] hd_tl[OF ‹w ≠ ε›]
using ‹f (a # w) ⋅ α = α ⋅ f (a # w)› by force
have "f [a] ⋅ α ≤p f [a] ⋅ f w ⋅ α"
unfolding pref_cancel_conv using bin_lcp_pref_all.
hence "f [a] ⋅ α = α ⋅ f [a]"
using eqd_eq[of "α ⋅ f [a]", OF _swap_len] unfolding prefix_def eq rassoc by metis
from eq[unfolded lassoc, folded this, unfolded rassoc cancel]
have "f w ⋅ α = α ⋅ f w".
from Cons.hyps[OF this] ‹f [a] ⋅ α = α ⋅ f [a]›
show ?thesis by fastforce
qed
qed simp
lemma im_comm_lcp_nemp: assumes "f w ⋅ α = α ⋅ f w" and "w ≠ ε" and "α ≠ ε"
obtains k where "w = [hd w]⇧@Suc k"
proof-
have "set w = {hd w}"
proof-
have "hd w ∈ set w" using ‹w ≠ ε› by force
have "a = hd w" if "a ∈ set w" for a
proof-
have "f [a] ⋅ α = α ⋅ f [a]" and "f [hd w] ⋅ α = α ⋅ f [hd w]"
using that im_comm_lcp[OF ‹f w ⋅ α = α ⋅ f w›] ‹hd w ∈ set w› by presburger+
from comm_trans[OF this ‹α ≠ ε›]
show "a = hd w"
using swap_non_comm_morph by blast
qed
thus "set w = {hd w}"
using ‹hd w ∈ set w› by blast
qed
from unique_letter_wordE[OF this]
show thesis
using that by blast
qed
lemma bin_lcp_ims_im_lcp: "f w ⋅ α ∧⇩p f w' ⋅ α = f (w ∧⇩p w') ⋅ α"
proof (cases "w ⨝ w'")
assume "w ⨝ w'"
from disjE[OF this[unfolded prefix_comparable_def]]
consider "w ≤p w'" | "w' ≤p w" by blast
thus ?thesis
proof (cases)
assume "w ≤p w'"
hence "f w ⋅ α ≤p f w' ⋅ α"
using pref_mono_lcp by blast
from this[folded lcp_pref_conv]
show ?thesis
unfolding ‹w ≤p w'›[folded lcp_pref_conv].
next
assume "w' ≤p w"
hence "f w' ⋅ α ≤p f w ⋅ α"
using pref_mono_lcp by blast
from this[folded lcp_pref_conv]
show ?thesis
unfolding lcp_sym[of "f w ⋅ α"] ‹w' ≤p w›[folded lcp_pref_conv, unfolded lcp_sym[of w']].
qed
next
assume "¬ w ⨝ w'"
from lcp_mismatchE[OF this]
obtain ws ws' where "(w ∧⇩p w') ⋅ ws = w" "(w ∧⇩p w') ⋅ ws' = w'"
"ws ≠ ε" "ws' ≠ ε" "hd ws ≠ hd ws'".
note hd_tl[OF ‹ws ≠ ε›] hd_tl[OF ‹ws' ≠ ε›]
have w: "(w ∧⇩p w') ⋅ [hd ws] ⋅ tl ws = w"
using ‹(w ∧⇩p w') ⋅ ws = w› ‹[hd ws] ⋅ tl ws = ws› by auto
have w': "(w ∧⇩p w') ⋅ [hd ws'] ⋅ tl ws' = w'"
using ‹(w ∧⇩p w') ⋅ ws' = w'› ‹[hd ws'] ⋅ tl ws' = ws'› by auto
have "f((w ∧⇩p w') ⋅ [hd ws] ⋅ tl ws) ⋅ α ∧⇩p f((w ∧⇩p w') ⋅ [hd ws'] ⋅ tl ws') ⋅ α =
f(w ∧⇩p w') ⋅ (f ([hd ws] ⋅ tl ws) ⋅ α ∧⇩p f([hd ws'] ⋅ tl ws') ⋅ α)"
unfolding morph using lcp_ext_left by auto
thus ?thesis
unfolding w w' bin_lcp_neq_hd[OF ‹hd ws ≠ hd ws'›, folded rassoc morph].
qed
lemma per_comp:
assumes "r <p f w ⋅ r"
shows "r ⨝ f w ⋅ α"
using assms
proof-
obtain n where "r <p f w⇧@n" "0 < n"
using per_root_powE[OF assms].
have "f w ⋅ α ≤p f w ⋅ f w ⇧@ (n - 1) ⋅ α"
using bin_lcp_pref_all[of "w⇧@(n-1)"]
unfolding pref_cancel_conv pow_morph.
with ruler[OF pref_ext[OF sprefD1[OF ‹r <p f w⇧@n›], of α], of "f w ⋅ α"]
show ?thesis
unfolding prefix_comparable_def pow_pos[OF ‹0 < n›] rassoc.
qed
end
subsection ‹More translations›
lemma bin_code_morph_iff': "binary_code_morphism f ⟷ morphism f ∧ f [a] ⋅ f [1-a] ≠ f [1-a] ⋅ f [a]"
proof
assume "binary_code_morphism f"
hence "morphism f"
by (simp add: binary_code_morphism_def code_morphism_def)
have "f [a] ⋅ f [1-a] ≠ f [1-a] ⋅ f [a]"
using ‹binary_code_morphism f› binary_code_morphism.non_comm_morph by auto
thus "morphism f ∧ f [a] ⋅ f [1-a] ≠ f [1-a] ⋅ f [a]"
using ‹morphism f› by blast
next
assume "morphism f ∧ f [a] ⋅ f [1-a] ≠ f [1-a] ⋅ f [a]"
hence "morphism f" and "f [a] ⋅ f [1-a] ≠ f [1-a] ⋅ f [a]" by force+
from binary_code_morphism.intro[OF binary_morphism.bin_code_morphismI[OF binary_morphism.intro], OF this]
show "binary_code_morphism f".
qed
lemma bin_code_morph_iff: "binary_code_morphism (bin_morph_of x y) ⟷ x ⋅ y ≠ y ⋅ x"
unfolding bin_code_morph_iff'[of "bin_morph_of x y" bina, unfolded binA_simps bin_morph_ofD]
using bin_morph_of_morph by blast
lemma bin_noner_morph_iff: "nonerasing_morphism (bin_morph_of x y) ⟷ x ≠ ε ∧ y ≠ ε"
proof
show "x ≠ ε ∧ y ≠ ε ⟹ nonerasing_morphism (bin_morph_of x y)"
by (rule morphism.nonerI[OF bin_morph_of_morph, of x y], unfold core_def bin_morph_of_def)
(simp split: finite_2.split)
show "nonerasing_morphism (bin_morph_of x y) ⟹ x ≠ ε ∧ y ≠ ε"
using nonerasing_morphism.nemp_to_nemp[of "bin_morph_of x y", of "[bina]"]
nonerasing_morphism.nemp_to_nemp[of "bin_morph_of x y", of "[binb]"]
unfolding bin_morph_of_def by simp_all
qed
lemma morph_bin_morph_of: "morphism f ⟷ bin_morph_of (f 𝔞) (f 𝔟) = f"
proof
show "morphism f ⟹ bin_morph_of (f 𝔞) (f 𝔟) = f"
using morphism.morph_concat_map'[of f]
unfolding bin_morph_of_def case_finiteD[symmetric, of f] case_finite_2_if_else by blast
qed (use bin_morph_of_morph in metis)
lemma two_bin_code_morphs_nonerasing_morphs: "binary_code_morphism g ⟹ binary_code_morphism h ⟹ two_nonerasing_morphisms g h"
by (simp add: binary_code_morphism.nonerasing binary_code_morphism_def code_morphism.axioms(1) nonerasing_morphism.intro nonerasing_morphism_axioms.intro two_morphisms_def two_nonerasing_morphisms.intro)
section "Marked binary morphism"
lemma marked_binary_morphI: assumes "morphism f" and "f [a :: binA] ≠ ε" and "f [1-a] ≠ ε" and "hd (f [a]) ≠ hd (f [1-a])"
shows "marked_morphism f"
proof (unfold_locales)
have "f [b] ≠ ε" for b
by (rule bin_swap_exhaust[of b a]) (use assms in force)+
thus "w = ε" if "f w = ε" for w
using morphism.noner_sings_conv[OF ‹morphism f›] that by blast
show "c = b" if "hd (f⇧𝒞 c) = hd (f⇧𝒞 b)" for c b
proof (rule ccontr)
assume "c ≠ b"
have "hd (f [c]) ≠ hd (f [b])"
by (rule binA_neq_cases_swap[OF ‹c ≠ b›, of a])
(use ‹hd (f [a]) ≠ hd (f [1-a])› in fastforce)+
thus False
using that[unfolded core_def] by contradiction
qed
qed (simp add: morphism.morph[OF assms(1)])
locale marked_binary_morphism = marked_morphism "f :: binA list ⇒ 'a list" for f
begin
lemma bin_marked: "hd (f 𝔞) ≠ hd (f 𝔟)"
using marked_morph[of bina binb] by blast
lemma bin_marked_sing: "hd (f [a]) ≠ hd (f [1-a])"
by (cases rule: finite_2.exhaust[of a]) (simp_all add: bin_marked bin_marked[symmetric])
sublocale binary_code_morphism
using binary_code_morphism_def code_morphism_axioms by blast
lemma marked_lcp_emp: "α = ε"
unfolding bin_lcp_def
proof (rule lcp_distinct_hd)
show "hd (f 𝔞 ⋅ f 𝔟) ≠ hd (f 𝔟 ⋅ f 𝔞)"
unfolding hd_append if_not_P[OF sing_to_nemp]
using bin_marked.
qed
lemma bin_marked': "(f 𝔞)!0 ≠ (f 𝔟)!0"
using bin_marked unfolding hd_conv_nth[OF bin_snd_nemp] hd_conv_nth[OF bin_fst_nemp].
lemma marked_bin_morph_pref_code: "r ⨝ s ∨ f (r ⋅ z1) ∧⇩p f (s ⋅ z2) = f (r ∧⇩p s)"
using lcp_ext_right marked_morph_lcp[of "r ⋅ z1" "s ⋅ z2"] by metis
end
lemma bin_marked_preimg_hd:
assumes "marked_binary_morphism (f :: binA list ⇒ binA list)"
obtains c where "hd (f [c]) = a"
proof-
interpret marked_binary_morphism f
using assms.
from that alphabet_or_neq[OF bin_marked]
show thesis
by blast
qed
section "Marked version"
context binary_code_morphism
begin
definition marked_version ("f⇩m") where "f⇩m = (λ w. α¯⇧>(f w ⋅ α))"
lemma marked_version_conjugates: "α ⋅ f⇩m w = f w ⋅ α"
unfolding marked_version_def using lq_pref[OF bin_lcp_pref_all, of w].
lemma marked_eq_conv: "f w = f w' ⟷ f⇩m w = f⇩m w'"
using cancel[of α "f⇩m w" "f⇩m w'"] unfolding marked_version_conjugates cancel_right.
lemma marked_marked: assumes "marked_morphism f" shows "f⇩m = f"
using marked_version_conjugates[unfolded emp_simps ‹marked_morphism f›[unfolded marked_lcp_conv]]
by blast
lemma marked_version_all_nemp: "w ≠ ε ⟹ f⇩m w ≠ ε"
unfolding marked_version_def using bin_lcp_pref_all nonerasing conjug_emp_emp marked_version_def by blast
lemma marked_version_binary_code_morph: "binary_code_morphism f⇩m"
unfolding bin_code_morph_iff' morphism_def
proof (unfold_locales)
have "f (u⋅v) ⋅ α = (f u ⋅ α) ⋅ α¯⇧>(f v ⋅ α)" for u v
unfolding rassoc morph cancel lq_pref[OF bin_lcp_pref_all[of v]]..
thus "⋀u v. f⇩m (u ⋅ v) = f⇩m u ⋅ f⇩m v"
unfolding marked_version_def lq_reassoc[OF bin_lcp_pref_all] by presburger
from code_morph
show "inj f⇩m"
unfolding inj_def marked_eq_conv.
qed
interpretation mv_bcm: binary_code_morphism f⇩m
using marked_version_binary_code_morph .
lemma marked_lcs: "bin_lcs (f⇩m 𝔞) (f⇩m 𝔟) = β ⋅ α"
unfolding bin_lcs_def morph[symmetric] lcs_ext_right[symmetric] marked_version_conjugates[symmetric] mv_bcm.morph[symmetric]
by (rule lcs_ext_left[of "f⇩m (𝔞 ⋅ 𝔟)" "f⇩m (𝔟 ⋅ 𝔞)" "f⇩m (𝔞 ⋅ 𝔟) ∧⇩s f⇩m (𝔟 ⋅ 𝔞) = α ⋅ f⇩m (𝔞 ⋅ 𝔟) ∧⇩s α ⋅ f⇩m (𝔟 ⋅ 𝔞)" α α], unfold mv_bcm.morph)
(use mv_bcm.bin_not_comp_suf in argo, simp)
lemma bin_lcp_shift: assumes "❙|α❙| < ❙|f w❙|" shows "(f w)!❙|α❙| = hd (f⇩m w)"
proof-
have "w ≠ ε"
using assms emp_to_emp by fastforce
hence "f⇩m w ≠ ε"
using marked_version_all_nemp by blast
show ?thesis
using pref_index[of "f w" "α⋅ f⇩m w" "❙|α❙|", OF prefI[of "f w" α " α ⋅ f⇩m w", OF marked_version_conjugates[of w, symmetric]], OF assms]
unfolding nth_append_length_plus[of α "f⇩m w" 0, unfolded add_0_right] hd_conv_nth[of "f⇩m w", symmetric, OF ‹f⇩m w ≠ ε›].
qed
lemma mismatch_fst: "hd (f⇩m 𝔞) = c⇩0"
proof-
have "(f [bina,binb])!❙|α❙| = hd (f⇩m [bina,binb])"
using bin_lcp_shift[of "[bina,binb]", unfolded pop_hd[of bina 𝔟] lenmorph, OF bin_lcp_short]
unfolding pop_hd[of bina 𝔟].
from this[unfolded mv_bcm.pop_hd[of bina 𝔟, unfolded not_Cons_self2[of bina ε]] hd_append2[OF mv_bcm.bin_fst_nemp, of "f⇩m 𝔟"], symmetric]
show ?thesis
unfolding bin_mismatch_def hd_word[of bina 𝔟] morph.
qed
lemma mismatch_snd: "hd (f⇩m 𝔟) = c⇩1"
proof-
have "(f [binb,bina])!❙|α❙| = hd (f⇩m [binb,bina])"
using bin_lcp_shift[of "[binb,bina]", unfolded pop_hd[of binb 𝔞] lenmorph, OF bin_lcp_short[unfolded add.commute[of "❙|f 𝔞❙|" "❙|f 𝔟❙|"]]]
unfolding pop_hd[of binb 𝔞].
from this[unfolded mv_bcm.pop_hd[of binb 𝔞, unfolded not_Cons_self2[of binb ε]] hd_append2[OF mv_bcm.bin_snd_nemp, of "f⇩m 𝔞"],symmetric]
show ?thesis
unfolding bin_mismatch_def hd_word[of binb 𝔞] morph bin_lcp_sym[of "f 𝔞"].
qed
lemma marked_hd_neq: "hd (f⇩m [a]) ≠ hd (f⇩m [1-a])" (is "?P (a :: binA)")
by (rule bin_induct[of ?P, unfolded binA_simps])
(use mismatch_fst mismatch_snd bin_mismatch_neq in presburger)+
lemma marked_version_marked_morph: "marked_morphism f⇩m"
by (standard, unfold core_def)
(use not_swap_eq[of "λ a b. hd (f⇩m [a]) = hd (f⇩m [b])", OF _ marked_hd_neq] in force)
interpretation mv_mbm: marked_binary_morphism f⇩m
using marked_version_marked_morph
by (simp add: marked_binary_morphism_def)
lemma bin_code_pref_morph: "f u ⋅ α ≤p f w ⋅ α ⟹ u ≤p w"
unfolding marked_version_conjugates[symmetric] pref_cancel_conv
using mv_mbm.pref_free_morph.
lemma mismatch_pref0: "[c⇩0] ≤p f⇩m 𝔞"
using mv_bcm.sing_to_nemp[THEN hd_pref, of bina] unfolding mismatch_fst.
lemma mismatch_pref1: "[c⇩1] ≤p f⇩m 𝔟"
using mv_bcm.bin_snd_nemp[THEN hd_pref] unfolding mismatch_snd.
lemma marked_version_len: "❙|f⇩m w❙| = ❙|f w❙|"
using add_left_imp_eq[OF
lenmorph[of α "f⇩m w", unfolded lenmorph[of "f w" α, folded marked_version_conjugates[of w]],symmetric,
unfolded add.commute[of "❙|f w❙|" "❙|α❙|"]]].
lemma bin_code_lcp: "(f r ⋅ α) ∧⇩p (f s ⋅ α) = f (r ∧⇩p s) ⋅ α"
by (metis lcp_ext_left marked_version_conjugates mv_mbm.marked_morph_lcp)
lemma not_comp_lcp: assumes "¬ r ⨝ s"
shows "f (r ∧⇩p s) ⋅ α = f r ⋅ f (r ⋅ s) ∧⇩p f s ⋅ f (r ⋅ s)"
proof-
let ?r' = "(r ∧⇩p s)¯⇧>r"
let ?s' = "(r ∧⇩p s)¯⇧>s"
from lcp_mismatch_lq[OF ‹¬ r ⨝ s›]
have "?r' ≠ ε" and "?s' ≠ ε" and "hd ?r' ≠ hd ?s'".
have "¬ f ((r ∧⇩p s) ⋅ [hd ?r'] ⋅ tl ?r') ⋅ α ⨝ f ((r ∧⇩p s) ⋅ [hd ?s'] ⋅ tl ?s') ⋅ α"
using bin_mismatch_swap_not_comp
unfolding morph prefix_comparable_def rassoc pref_cancel_conv
‹hd ?r' ≠ hd ?s'›[symmetric, unfolded bin_neq_iff, symmetric].
hence "¬ f r ⋅ α ⨝ f s ⋅ α"
unfolding hd_tl[OF ‹?r' ≠ ε›] hd_tl[OF ‹?s' ≠ ε›] lcp_lq.
have pref: "f w ⋅ α ≤p f w ⋅ f (r ⋅ s)" for w
unfolding pref_cancel_conv
using append_prefixD[OF not_comp_bin_lcp_pref, OF ‹¬ r ⨝ s›] by blast
from prefE[OF pref[of r], unfolded rassoc]
obtain gr' where gr': "f r ⋅ f (r ⋅ s) = f r ⋅ α ⋅ gr'".
from prefE[OF pref[of s], unfolded rassoc]
obtain gs' where gs': "f s ⋅ f (r ⋅ s) = f s ⋅ α ⋅ gs'".
thus "f (r ∧⇩p s) ⋅ α = f r ⋅ f (r ⋅ s) ∧⇩p f s ⋅ f (r ⋅ s)"
unfolding bin_code_lcp[symmetric, of r s] prefix_def using ‹¬ f r ⋅ α ⨝ f s ⋅ α›
lcp_ext_right[of "f r ⋅ α" "f s ⋅ α" _ gr' gs', unfolded rassoc, folded gr' gs'] by argo
qed
lemma bin_morph_pref_conv: "f u ⋅ α ≤p f v ⋅ α ⟷ u ≤p v"
proof
assume "u ≤p v"
from this[unfolded prefix_def]
obtain z where "v = u ⋅ z" by blast
show "f u ⋅ α ≤p f v ⋅ α"
unfolding arg_cong[OF ‹v = u ⋅ z›, of f, unfolded morph] rassoc pref_cancel_conv using bin_lcp_pref_all.
next
assume "f u ⋅ α ≤p f v ⋅ α"
then show "u ≤p v"
unfolding marked_version_conjugates[symmetric] prefix_comparable_def pref_cancel_conv
using mv_mbm.pref_free_morph by meson
qed
lemma bin_morph_compare_conv: "f u ⋅ α ⨝ f v ⋅ α ⟷ u ⨝ v"
using bin_morph_pref_conv unfolding prefix_comparable_def by auto
lemma code_lcp': "¬ r ⨝ s ⟹ α ≤p f z ⟹ α ≤p f z' ⟹ f (r ⋅ z) ∧⇩p f (s ⋅ z') = f (r ∧⇩p s) ⋅ α"
proof-
assume "α ≤p f z" "α ≤p f z'" "¬ r ⨝ s"
hence eqs: "f (r ⋅ z) = (f r ⋅ α) ⋅ (α¯⇧>f z)" "f (s ⋅ z') = (f s ⋅ α) ⋅ (α¯⇧>f z')"
unfolding rassoc by (metis lq_pref morph)+
show ?thesis
using bin_morph_compare_conv ‹¬ r ⨝ s› bin_code_lcp lcp_ext_right unfolding eqs
by metis
qed
lemma non_comm_im_lcp: assumes "u ⋅ v ≠ v ⋅ u"
shows "f (u ⋅ v) ∧⇩p f (v ⋅ u) = f (u ⋅ v ∧⇩p v ⋅ u) ⋅ α"
proof-
have "¬ f (u ⋅ v) ⨝ f (v ⋅ u)"
using assms comm_comp_eq[of "f u" "f v", folded morph, THEN code_morph_code] by blast
from lcp_ext_right_conv[OF this, of α α, unfolded bin_code_lcp, symmetric]
show ?thesis.
qed
end
locale binary_code_morphism_shift = binary_code_morphism +
fixes α'
assumes shift_pref: "α' ≤p α"
begin
definition shifted_f where "shifted_f = (λ w. α'¯⇧>(f w ⋅ α'))"
lemma shift_pref_all: "α' ≤p f w ⋅ α'"
proof-
have "α' ⋅ α'¯⇧>α ≤p f w ⋅ α' ⋅ α'¯⇧>α"
unfolding lq_pref[OF shift_pref] rassoc using bin_lcp_pref_all.
thus ?thesis
using pref_keeps_per_root by blast
qed
sublocale shifted: binary_code_morphism shifted_f
proof-
have morph: "f (u⋅v) ⋅ α' = (f u ⋅ α') ⋅ α'¯⇧>(f v ⋅ α')" for u v
unfolding rassoc morph cancel lq_pref[OF shift_pref_all]..
then interpret morphism shifted_f
unfolding shifted_f_def morphism_def
using lq_reassoc[OF shift_pref_all] by presburger
have "inj shifted_f"
unfolding inj_on_def shifted_f_def using lq_pref[OF shift_pref_all]
using cancel_right code_morph_code by metis
then show "binary_code_morphism shifted_f"
by unfold_locales
qed
lemma shifted_lcp: "α' ⋅ shifted.bin_code_lcp = α"
unfolding bin_lcp_def shifted_f_def lcp_ext_left[symmetric]
unfolding lassoc lq_pref[OF shift_pref_all]
unfolding rassoc lq_pref[OF shift_pref_all]
using lcp_ext_right_conv[OF bin_not_comp, unfolded rassoc].
lemma "α' = α ⟹ shifted_f = f⇩m"
unfolding shifted_f_def marked_version_def by fast
end
section "Two binary code morphisms"
locale two_binary_code_morphisms =
g: binary_code_morphism g +
h: binary_code_morphism h
for g h :: "binA list ⇒ 'a list"
begin
notation h.bin_code_lcp ("α⇩h")
notation g.bin_code_lcp ("α⇩g")
notation "g.marked_version" ("g⇩m")
notation "h.marked_version" ("h⇩m")
sublocale gm: marked_binary_morphism g⇩m
by (simp add: g.marked_version_marked_morph marked_binary_morphism.intro)
sublocale hm: marked_binary_morphism h⇩m
by (simp add: h.marked_version_marked_morph marked_binary_morphism.intro)
sublocale two_binary_morphisms g h..
sublocale marked: two_marked_morphisms g⇩m h⇩m..
sublocale code: two_code_morphisms g h
by unfold_locales
lemma marked_two_binary_code_morphisms: "two_binary_code_morphisms g⇩m h⇩m"
using g.marked_version_binary_code_morph h.marked_version_binary_code_morph
by unfold_locales
lemma revs_two_binary_code_morphisms: "two_binary_code_morphisms (rev_map g) (rev_map h)"
using code.revs_two_code_morphisms rev_morphs
by (simp add: g.bin_code_morph_rev_map h.bin_code_morph_rev_map rev_morphs two_binary_code_morphisms_def)
lemma swap_two_binary_code_morphisms: "two_binary_code_morphisms h g"
by unfold_locales
text‹Each successful overflow has a unique minimal successful continuation›
lemma min_completionE:
assumes "z ⋅ g⇩m r = z' ⋅ h⇩m s"
obtains p q where "z ⋅ g⇩m p = z' ⋅ h⇩m q" and
"⋀ r s. z ⋅ g⇩m r = z' ⋅ h⇩m s ⟹ p ≤p r ∧ q ≤p s"
proof-
interpret swap: two_binary_code_morphisms h g
by unfold_locales
define P where "P = (λ m. ∃ p q. z ⋅ g⇩m p = z' ⋅ h⇩m q ∧ ❙|p❙| = m)"
have "P ❙|r❙|" using assms P_def
by blast
obtain n where ndef: "n = (LEAST m. P m)"
by simp
then obtain p q where "z ⋅ g⇩m p = z' ⋅ h⇩m q" "❙|p❙| = n" using ‹P ❙|r❙|›
using LeastI P_def by metis
have "p ≤p r' ∧ q ≤p s'" if "z ⋅ g⇩m r' = z' ⋅ h⇩m s'" for r' s'
proof
have "z ⋅ g⇩m (p ∧⇩p r') = z' ⋅ h⇩m (q ∧⇩p s')"
using ‹z ⋅ g⇩m p = z' ⋅ h⇩m q› ‹z ⋅ g⇩m r' = z' ⋅ h⇩m s'›
marked.unique_continuation by blast
thus "p ≤p r'"
using P_def le_antisym ‹❙|p❙| = n› lcp_len' ndef not_less_Least
by metis
from this[folded lcp_pref_conv]
have "h⇩m q = h⇩m (q ∧⇩p s')"
using ‹z ⋅ g⇩m (p ∧⇩p r') = z' ⋅ h⇩m (q ∧⇩p s')› ‹z ⋅ g⇩m p = z' ⋅ h⇩m q›
by force
thus "q ≤p s'"
using hm.code_morph_code lcp_pref_conv by metis
qed
thus thesis
using ‹z ⋅ g⇩m p = z' ⋅ h⇩m q› that by blast
qed
lemma two_equals:
assumes "g r = h r" and "g s = h s" and "¬ r ⨝ s"
shows "g (r ∧⇩p s) ⋅ α⇩g = h (r ∧⇩p s) ⋅ α⇩h"
unfolding g.not_comp_lcp[OF ‹¬ r ⨝ s›] h.not_comp_lcp[OF ‹¬ r ⨝ s›] g.morph h.morph assms..
lemma solution_sing_len_diff: assumes "g ≠ h" and "g s = h s" and "set s = binUNIV"
shows "❙|g [c]❙| ≠ ❙|h [c]❙|"
proof (rule solution_sing_len_cases[OF ‹set s = binUNIV› ‹g s = h s› ‹g ≠ h›])
fix a assume less: "❙|g [a]❙| < ❙|h [a]❙|" "❙|h [1 - a]❙| < ❙|g [1 - a]❙|"
show "❙|g [c]❙| ≠ ❙|h [c]❙|"
by (rule bin_swap_exhaust[of c a]) (use less in force)+
qed
lemma alphas_pref: assumes "❙|α⇩h❙| ≤ ❙|α⇩g❙|" and "g r =⇩m h s" shows "α⇩h ≤p α⇩g"
proof-
have "s ≠ ε" and "r ≠ ε"
using min_coinD'[OF ‹g r =⇩m h s›] by force+
from
root_ruler[OF h.bin_lcp_spref_all[OF ‹s ≠ ε›] g.bin_lcp_spref_all[OF ‹r ≠ ε›, unfolded min_coinD[OF ‹g r =⇩m h s›]]]
show "α⇩h ≤p α⇩g"
unfolding prefix_comparable_def using ruler_le[OF self_pref _ assms(1)] by blast
qed
end
locale binary_codes_coincidence = two_binary_code_morphisms +
assumes alphas_len: "❙|α⇩h❙| ≤ ❙|α⇩g❙|" and
coin_ex: "∃ r s. g r =⇩m h s"
begin
lemma alphas_pref: "α⇩h ≤p α⇩g"
using alphas_pref[OF alphas_len] coin_ex by force
definition α where "α ≡ α⇩h¯⇧>α⇩g"
definition critical_overflow ("𝖼") where "critical_overflow ≡ α⇩g⇧<¯α⇩h"
lemma lcp_diff: "α⇩h ⋅ α = α⇩g"
unfolding α_def lq_pref using lq_pref[OF alphas_pref].
lemma solution_marked_version_conv: "g r = h s ⟷ α ⋅ g⇩m r = h⇩m s ⋅ α "
unfolding cancel[of α⇩h "α ⋅ g⇩m r" "h⇩m s ⋅ α", symmetric]
unfolding lassoc lcp_diff h.marked_version_conjugates g.marked_version_conjugates
unfolding rassoc lcp_diff cancel_right..
end
locale binary_code_coincidence_sym = two_binary_code_morphisms
+ assumes
coin_ex: "∃ r s. g r =⇩m h s"
begin
lemma coinE: obtains u v where "g u =⇩m h v" and "h v =⇩m g u"
using coin_ex code.min_coin_prefE[OF min_solD[of _ g h]] min_coin_sym by metis
definition α' where "α' = (if ❙|α⇩g❙| ≤ ❙|α⇩h❙| then α⇩g else α⇩h)"
definition g' where "g' = (if ❙|α⇩g❙| ≤ ❙|α⇩h❙| then (λ w. α'¯⇧>(g w ⋅ α')) else (λ w. α'¯⇧>(h w ⋅ α')))"
definition h' where "h' = (if ❙|α⇩g❙| ≤ ❙|α⇩h❙| then (λ w. α'¯⇧>(h w ⋅ α')) else (λ w. α'¯⇧>(g w ⋅ α')))"
lemma shift_pref_fst: "α' ≤p α⇩g"
unfolding α'_def
proof (cases "❙|α⇩g❙| ≤ ❙|α⇩h❙|", simp)
show "¬ ❙|α⇩g❙| ≤ ❙|α⇩h❙| ⟹ (if ❙|α⇩g❙| ≤ ❙|α⇩h❙| then α⇩g else α⇩h) ≤p α⇩g"
using alphas_pref coinE by fastforce
qed
interpretation gshift: binary_code_morphism_shift g α'
using shift_pref_fst by unfold_locales
interpretation swap: two_binary_code_morphisms h g
by (simp add: swap_two_binary_code_morphisms)
lemma shift_pref_snd: "α' ≤p α⇩h"
unfolding α'_def
proof (cases "¬ ❙|α⇩g❙| ≤ ❙|α⇩h❙|", simp_all)
show "❙|α⇩g❙| ≤ ❙|α⇩h❙| ⟹ α⇩g ≤p α⇩h"
using swap.alphas_pref[OF _ coinE] by blast
qed
interpretation hshift: binary_code_morphism_shift h α'
using shift_pref_snd by unfold_locales
lemma shifted_eq_conv:"g r = h s ⟷ g' r = h' s"
oops
lemma shifted_eq_conv:"g r = h r ⟷ g' r = h' r"
proof-
have "g r = h r ⟷ α'¯⇧>(g r ⋅ α') = α'¯⇧>(h r ⋅ α')"
using cancel_right lq_pref gshift.shift_pref_all hshift.shift_pref_all by metis
thus "g r = h r ⟷ g' r = h' r"
unfolding g'_def h'_def
by (cases "❙|α⇩g❙| ≤ ❙|α⇩h❙|", presburger)
fastforce
qed
lemma shifted_eq_conv':"g = h ⟷ g' = h'"
using shifted_eq_conv by fastforce
interpretation shifted_g: binary_code_morphism "(λ w. α'¯⇧>(g w ⋅ α'))"
using gshift.shifted.binary_code_morphism_axioms[unfolded gshift.shifted_f_def].
interpretation shifted_h: binary_code_morphism "(λ w. α'¯⇧>(h w ⋅ α'))"
using hshift.shifted.binary_code_morphism_axioms[unfolded hshift.shifted_f_def].
lemma shifted_min_sol_conv: "r ∈ g =⇩M h ⟷ r ∈ g' =⇩M h'"
unfolding min_sol_def using shifted_eq_conv by blast
lemma shifted_not_triv: "g = h ⟷ g' = h'"
using shifted_eq_conv by fastforce
sublocale shifted: two_binary_code_morphisms g' h'
proof-
interpret g': binary_code_morphism g'
unfolding g'_def using shifted_g.binary_code_morphism_axioms shifted_h.binary_code_morphism_axioms by presburger
interpret h': binary_code_morphism h'
unfolding h'_def using shifted_g.binary_code_morphism_axioms shifted_h.binary_code_morphism_axioms by presburger
show "two_binary_code_morphisms g' h'"..
qed
lemma shifted_fst_lcp_emp: "shifted.g.bin_code_lcp = ε"
unfolding bin_lcp_def
proof (cases "❙|α⇩g❙| ≤ ❙|α⇩h❙|")
assume "❙|α⇩g❙| ≤ ❙|α⇩h❙|"
hence *: "α' = α⇩g" "g' = (λ w. α'¯⇧>(g w ⋅ α'))"
unfolding α'_def g'_def by simp_all
have "g⇩m 𝔞 ⋅ g⇩m 𝔟 ∧⇩p g⇩m 𝔟 ⋅ g⇩m 𝔞 = ε"
using gm.marked_lcp_emp unfolding bin_lcp_def.
thus "g' 𝔞 ⋅ g' 𝔟 ∧⇩p g' 𝔟 ⋅ g' 𝔞 = ε"
unfolding * g.marked_version_def.
next
assume "¬ ❙|α⇩g❙| ≤ ❙|α⇩h❙|"
hence c: "α' = α⇩h" "g' = (λ w. α'¯⇧>(h w ⋅ α'))"
unfolding α'_def g'_def by simp_all
have "h⇩m 𝔞 ⋅ h⇩m 𝔟 ∧⇩p h⇩m 𝔟 ⋅ h⇩m 𝔞 = ε"
using hm.marked_lcp_emp unfolding bin_lcp_def.
thus "g' 𝔞 ⋅ g' 𝔟 ∧⇩p g' 𝔟 ⋅ g' 𝔞 = ε"
unfolding c h.marked_version_def.
qed
lemma shifted_alphas: assumes le: "❙|α⇩g❙| ≤ ❙|α⇩h❙|"
shows "α' ⋅ shifted.g.bin_code_lcp = α⇩g" and "α' ⋅ shifted.h.bin_code_lcp = α⇩h"
proof-
have c: "α' = α⇩g" "g' = (λ w. α'¯⇧>(g w ⋅ α'))" "h' = (λ w. α'¯⇧>(h w ⋅ α'))"
using le unfolding α'_def g'_def h'_def by simp_all
interpret binary_codes_coincidence h g
proof
show "∃r s. h r =⇩m g s"
using coin_ex[unfolded min_coin_sym_iff[of g]] by blast
qed fact
show "α' ⋅ shifted.g.bin_code_lcp = α⇩g"
unfolding c
unfolding bin_lcp_def[of "g' 𝔞", unfolded c] lcp_ext_left[symmetric]
unfolding lassoc lq_pref[OF g.bin_lcp_pref_all]
unfolding rassoc lq_pref[OF g.bin_lcp_pref_all]
unfolding lcp_ext_right_conv[OF g.non_comp_morph[of bina], unfolded binA_simps rassoc]
unfolding bin_lcp_def..
from pref_prod_pref[OF pref_trans[OF alphas_pref h.bin_lcp_pref_all] alphas_pref]
have pref_all: "α⇩g ≤p h w ⋅ α⇩g" for w.
show "α' ⋅ shifted.h.bin_code_lcp = α⇩h"
unfolding c
unfolding bin_lcp_def[of "h' 𝔞", unfolded c] lcp_ext_left[symmetric]
unfolding lassoc lq_pref[OF pref_all]
unfolding rassoc lq_pref[OF pref_all]
unfolding lcp_ext_right_conv[OF h.non_comp_morph[of bina], unfolded binA_simps rassoc]
unfolding bin_lcp_def..
qed
interpretation swapped: binary_code_coincidence_sym h g
proof
show "∃r s. h r =⇩m g s"
using coin_ex[unfolded min_coin_sym_iff[of g]] by blast
qed
lemma eq_len_eq_conv: "α⇩g = α⇩h ⟷ ❙|α⇩g❙| = ❙|α⇩h❙|"
proof
show "α⇩g = α⇩h" if "❙|α⇩g❙| = ❙|α⇩h❙|"
using swap.alphas_pref[OF eq_imp_le[OF that]] alphas_pref[OF eq_imp_le[OF that[symmetric]]]
using coinE[of "α⇩g = α⇩h"] by fastforce
qed simp
lemma shift_swapped: "swapped.α' = α'"
unfolding α'_def swapped.α'_def using eq_len_eq_conv by fastforce
lemma morphs_swapped: assumes "❙|α⇩g❙| ≠ ❙|α⇩h❙|" shows "swapped.g' = g'" "swapped.h' = h'"
unfolding g'_def swapped.g'_def h'_def swapped.h'_def shift_swapped using assms by fastforce+
lemma morphs_swapped': assumes "❙|α⇩g❙| = ❙|α⇩h❙|" shows "swapped.g' = h'" "swapped.h' = g'"
unfolding g'_def swapped.g'_def h'_def swapped.h'_def shift_swapped using assms by fastforce+
lemma shifted_lcp_len_eq: "❙|shifted.g.bin_code_lcp❙| = ❙|shifted.h.bin_code_lcp❙| ⟷ ❙|α⇩g❙| = ❙|α⇩h❙|" and
shifted_lcp_len_le: "❙|shifted.g.bin_code_lcp❙| ≤ ❙|shifted.h.bin_code_lcp❙|"
unfolding atomize_conj
proof (cases)
assume le: "❙|α⇩g❙| ≤ ❙|α⇩h❙|"
note shifted_alphas[OF this]
from lenarg[OF this(1)] lenarg[OF this(2)]
show "(❙|shifted.g.bin_code_lcp❙| = ❙|shifted.h.bin_code_lcp❙| ⟷ ❙|α⇩g❙| = ❙|α⇩h❙|) ∧ ❙|shifted.g.bin_code_lcp❙| ≤ ❙|shifted.h.bin_code_lcp❙|"
unfolding lenmorph using le by fastforce+
next
assume "¬ ❙|α⇩g❙| ≤ ❙|α⇩h❙|"
hence le: "❙|α⇩h❙| ≤ ❙|α⇩g❙|" by fastforce
note swapped.shifted_alphas[OF this]
note lens = lenarg[OF this(1)] lenarg[OF this(2)]
show "(❙|shifted.g.bin_code_lcp❙| = ❙|shifted.h.bin_code_lcp❙| ⟷ ❙|α⇩g❙| = ❙|α⇩h❙|) ∧ ❙|shifted.g.bin_code_lcp❙| ≤ ❙|shifted.h.bin_code_lcp❙|"
proof (cases)
assume eq: "❙|α⇩g❙| = ❙|α⇩h❙|"
show "(❙|shifted.g.bin_code_lcp❙| = ❙|shifted.h.bin_code_lcp❙| ⟷ ❙|α⇩g❙| = ❙|α⇩h❙|) ∧ ❙|shifted.g.bin_code_lcp❙| ≤ ❙|shifted.h.bin_code_lcp❙|"
using lens eq unfolding shift_swapped lenmorph bin_lcp_def morphs_swapped'[OF eq] by linarith+
next
assume neq: "❙|α⇩g❙| ≠ ❙|α⇩h❙|"
from lens
show "(❙|shifted.g.bin_code_lcp❙| = ❙|shifted.h.bin_code_lcp❙| ⟷ ❙|α⇩g❙| = ❙|α⇩h❙|) ∧ ❙|shifted.g.bin_code_lcp❙| ≤ ❙|shifted.h.bin_code_lcp❙|"
using le unfolding shift_swapped lenmorph bin_lcp_def morphs_swapped[OF neq] by fastforce+
qed
qed
end
locale two_marked_binary_morphisms = two_marked_morphisms g h
for g h :: "binA list ⇒ 'a list"
begin
sublocale two_binary_code_morphisms g h ..
lemma not_comm_im: assumes "g ≠ h" and "g s = h s" and "s ≠ ε"
and "hd s = a" and "set s = binUNIV"
shows "g[a] ⋅ h [a] ≠ h[a] ⋅ g[a]"
proof (rule notI)
assume comm: "g[a] ⋅ h [a] = h[a] ⋅ g[a]"
from hd_im_comm_eq[OF ‹g s = h s› ‹s ≠ ε›] comm
have "g [a] = h [a]"
unfolding core_def ‹hd s = a› by blast
thus False
using len_ims_sing_neq[OF ‹g s = h s› ‹g ≠ h› ‹set s = binUNIV›] by metis
qed
lemma sol_set_not_com_hd:
assumes
morphs_neq: "g ≠ h" and
sol: "g s = h s" and
sol_set: "set s = binUNIV"
shows "g ([hd s]) ⋅ h ([hd s]) ≠ h ([hd s]) ⋅ g ([hd s])"
proof
assume comm: "g [hd s] ⋅ h [hd s] = h [hd s] ⋅ g [hd s]"
obtain n s' where s: "[hd s]⇧@Suc n ⋅ [1 - hd s] ⋅ s' = s"
using bin_distinct_letter[OF sol_set].
have "[hd s] ⇧@ Suc n ⋅ [1 - hd s] ⋅ s' ≠ ε" by blast
from hd_im_comm_eq[OF _ this]
have "g [hd s] = h [hd s]"
unfolding core_def s comm using sol by blast
thus False
using len_ims_sing_neq[OF sol ‹g ≠ h› sol_set, of "hd s"] by argo
qed
sublocale g: marked_binary_morphism g
using g.marked_marked g.marked_morphism_axioms gm.marked_binary_morphism_axioms by auto
sublocale h: marked_binary_morphism h
using h.marked_marked h.marked_morphism_axioms hm.marked_binary_morphism_axioms by auto
sublocale revs: two_binary_code_morphisms "rev_map g" "rev_map h"
using revs_two_binary_code_morphisms.
end
section ‹Two marked binary morphisms with blocks›
locale two_binary_marked_blocks = two_marked_binary_morphisms +
assumes both_blocks: "⋀ a. blockP a"
begin
sublocale sucs: two_marked_binary_morphisms suc_fst suc_snd
using sucs_marked_morphs[OF both_blocks, folded two_marked_binary_morphisms_def].
sublocale sucs_enc: two_marked_binary_morphisms suc_fst' suc_snd'
using encoded_sucs[OF both_blocks, folded two_marked_binary_morphisms_def].
lemma bin_blocks_swap: "two_binary_marked_blocks h g"
proof (unfold_locales)
fix a
obtain c where "hd (suc_snd [c]) = a"
using bin_marked_preimg_hd[of suc_snd]
marked_binary_morphism_def sucs.h.marked_morphism_axioms by blast
show "two_marked_morphisms.blockP h g a"
proof (rule two_marked_morphisms.blockI, unfold_locales)
show "hd (suc_snd [c]) = a" by fact
show "h (suc_snd [c]) =⇩m g (suc_fst [c])"
using min_coin_sym[OF blockP_D[OF both_blocks]].
qed
qed
lemma blocks_all_letters_fst: "[b] ≤f suc_fst ([a] ⋅ [1-a])"
proof-
have *: "suc_fst ([a] ⋅ [1 - a]) = [a] ⋅ tl (suc_fst [a]) ⋅ [1-a] ⋅ tl (suc_fst [1 - a])"
unfolding sucs.g.morph lassoc hd_tl[OF sucs.g.sing_to_nemp, unfolded blockP_D_hd[OF both_blocks]]..
show ?thesis
by (cases rule: neq_exhaust[OF bin_swap_neq, of b a], unfold *)
(blast+)
qed
lemma blocks_all_letters_snd: "[b] ≤f suc_snd ([a] ⋅ [1-a])"
proof-
have *: "suc_snd ([a] ⋅ [1 - a]) = [hd (suc_snd [a])] ⋅ tl (suc_snd [a]) ⋅ [hd (suc_snd [1-a])] ⋅ tl (suc_snd [1-a])"
unfolding sucs.h.morph rassoc hd_tl[OF sucs.h.sing_to_nemp, unfolded blockP_D_hd[OF both_blocks]]
unfolding lassoc hd_tl[OF sucs.h.sing_to_nemp, unfolded blockP_D_hd[OF both_blocks]]..
show ?thesis
proof (cases rule: neq_exhaust[OF sucs.h.bin_marked_sing, of b a])
assume b: "b = hd (suc_snd [a])"
show ?thesis
unfolding b * by blast
next
assume b: "b = hd (suc_snd [1-a])"
show ?thesis
unfolding b * by blast
qed
qed
lemma lcs_suf_blocks_fst: "g.bin_code_lcs ≤s g (suc_fst ([a] ⋅ [1-a]))"
using revs.g.bin_lcp_pref''[reversed] g.bin_lcp_pref'' blocks_all_letters_fst by simp
lemma lcs_suf_blocks_snd: "h.bin_code_lcs ≤s h (suc_snd ([a] ⋅ [1-a]))"
using revs.h.bin_lcp_pref''[reversed] h.bin_lcp_pref'' blocks_all_letters_snd by simp
lemma lcs_fst_suf_snd: "g.bin_code_lcs ≤s h.bin_code_lcs ⋅ h sucs.h.bin_code_lcs"
proof-
have "g.bin_code_lcs ≤s g (suc_fst [a] ⋅ suc_fst [1-a])" for a
using lcs_suf_blocks_fst[of a]
unfolding binA_simps sucs.g.morph.
have "g.bin_code_lcs ≤s g (suc_fst 𝔞 ⋅ suc_fst 𝔟)" and "g.bin_code_lcs ≤s g (suc_fst 𝔟 ⋅ suc_fst 𝔞)"
using lcs_suf_blocks_fst[of bina] lcs_suf_blocks_fst[of binb]
unfolding binA_simps sucs.g.morph.
hence "g.bin_code_lcs ≤s h (suc_snd 𝔞 ⋅ suc_snd 𝔟)" and "g.bin_code_lcs ≤s h (suc_snd 𝔟 ⋅ suc_snd 𝔞)"
unfolding g.morph h.morph block_eq[OF both_blocks].
from suf_ext[OF this(1)] suf_ext[OF this(2)]
have "g.bin_code_lcs ≤s h.bin_code_lcs ⋅ h (suc_snd 𝔞 ⋅ suc_snd 𝔟)" and "g.bin_code_lcs ≤s h.bin_code_lcs ⋅ h (suc_snd 𝔟 ⋅ suc_snd 𝔞)".
hence "g.bin_code_lcs ≤s h.bin_code_lcs ⋅ h (suc_snd 𝔞 ⋅ suc_snd 𝔟) ∧⇩s h.bin_code_lcs ⋅ h (suc_snd 𝔟 ⋅ suc_snd 𝔞)"
using suf_lcs_iff by blast
thus "g.bin_code_lcs ≤s h.bin_code_lcs ⋅ h sucs.h.bin_code_lcs"
unfolding revs.h.bin_code_lcp[reversed] bin_lcs_def[symmetric].
qed
lemma suf_comp_lcs: "g.bin_code_lcs ⨝⇩s h.bin_code_lcs"
using lcs_suf_blocks_fst lcs_suf_blocks_snd
unfolding g.morph h.morph sucs.g.morph sucs.h.morph block_eq[OF both_blocks] suf_comp_or using ruler[reversed] by blast
end
section ‹Binary primitivity preserving morphism given by a pair of words›
definition bin_prim :: "'a list ⇒ 'a list ⇒ bool"
where "bin_prim x y ⟷ primitivity_preserving_morphism (bin_morph_of x y)"
lemma bin_prim_code:
assumes "bin_prim x y"
shows "x ⋅ y ≠ y ⋅ x"
proof -
have "inj (bin_morph_of x y)"
using ‹bin_prim x y› primitivity_preserving_morphism.code_morph
by (simp add: bin_prim_def)
then have "(bin_morph_of x y) (𝔞 ⋅ 𝔟) ≠ (bin_morph_of x y) (𝔟 ⋅ 𝔞)"
by (blast dest: injD)
then show "x ⋅ y ≠ y ⋅ x"
by (simp add: bin_morph_of_def)
qed
subsection ‹Translating to to list concatenation›
lemma bin_concat_prim_pres_noner1:
assumes "x ≠ y"
and prim_pres: "⋀ ws. ws ∈ lists {x,y} ⟹ 2 ≤ ❙|ws❙| ⟹ primitive ws ⟹ primitive (concat ws)"
shows "x ≠ ε"
proof
assume "x = ε"
with ‹x ≠ y› have "y ≠ ε"
by blast
have "primitive [x, y, y]"
using prim_abk[OF ‹x ≠ y›, of 2] by simp
with ‹x ≠ y› have "primitive (concat [x, y, y])"
by (intro prim_pres) simp_all
then show False
by (simp add: ‹x = ε› eq_append_not_prim)
qed
lemma bin_concat_prim_pres_noner:
assumes "x ≠ y"
and prim_pres: "⋀ ws. ws ∈ lists {x,y} ⟹ 2 ≤ ❙|ws❙| ⟹ primitive ws ⟹ primitive (concat ws)"
shows "nonerasing_morphism (bin_morph_of x y)"
proof (intro morphism.nonerI bin_morph_of_morph)
fix a
have "x ≠ ε" and "y ≠ ε"
using ‹x ≠ y› prim_pres
by (fact bin_concat_prim_pres_noner1, intro bin_concat_prim_pres_noner1)
(unfold insert_commute[of x y] eq_commute[of x y])
then show "(bin_morph_of x y)⇧𝒞 a ≠ ε"
by (simp add: bin_morph_of_def core_def)
qed
lemma bin_prim_concat_prim_pres_conv:
assumes "x ≠ y"
shows "bin_prim x y ⟷ (∀ws ∈ lists {x,y}. 2 ≤ ❙|ws❙| ⟶ primitive ws ⟶ primitive (concat ws))"
(is "_ ⟷ ?condition")
proof -
define f where "f = (λa. (if a = bina then x else y))"
have "inj f"
using ‹x ≠ y›
by (intro linorder_injI) (simp add: less_finite_2_def f_def)
moreover have "f ` UNIV = {x, y}"
by (simp add: f_def insert_commute)
ultimately have "bij_betw f UNIV {x, y}"
unfolding bij_betw_def..
then have bij: "bij_betw (map f) (lists UNIV) (lists {x, y})"
by (fact bij_lists)
have concat_map_f: "concat (map f w) = bin_morph_of x y w" for w
by (simp add: bin_morph_of_def f_def)
have "?condition ⟹ nonerasing_morphism (bin_morph_of x y)"
by (simp add: ‹x ≠ y› bin_concat_prim_pres_noner)
then show "bin_prim x y ⟷ ?condition"
unfolding bin_prim_def primitivity_preserving_morphism_def primitivity_preserving_morphism_axioms_def
unfolding bij_betw_ball[OF bij] prim_map_iff[OF ‹inj f›] concat_map_f
by auto
qed
lemma bin_prim_concat_prim_pres:
assumes "bin_prim x y"
shows "ws ∈ lists {x, y} ⟹ 2 ≤ ❙|ws❙| ⟹ primitive ws ⟹ primitive (concat ws)"
using bin_prim_code[OF ‹bin_prim x y›] ‹bin_prim x y› bin_prim_concat_prim_pres_conv[of x y]
by (cases "x = y") blast+
lemma bin_prim_altdef1:
"bin_prim x y ⟷
(x ≠ y) ∧ (∀ws ∈ lists {x,y}. 2 ≤ ❙|ws❙| ⟶ primitive ws ⟶ primitive (concat ws))"
using bin_prim_code[of x y] bin_prim_concat_prim_pres_conv[of x y]
by blast
lemma bin_prim_altdef2:
"bin_prim x y ⟷
(x ⋅ y ≠ y ⋅ x) ∧ (∀ws ∈ lists {x,y}. 2 ≤ ❙|ws❙| ⟶ primitive ws ⟶ primitive (concat ws))"
using bin_prim_code[of x y] bin_prim_concat_prim_pres_conv[of x y]
by blast
subsection ‹Basic properties of @{term bin_prim}›
lemma bin_prim_irrefl: "¬ bin_prim x x"
using bin_prim_code by blast
lemma bin_prim_symm [sym]: "bin_prim x y ⟹ bin_prim y x"
using bin_prim_concat_prim_pres_conv[of x y] bin_prim_concat_prim_pres_conv[of y x]
unfolding eq_commute[of y x] insert_commute[of y x]
by blast
lemma bin_prim_commutes: "bin_prim x y ⟷ bin_prim y x"
by (blast intro: bin_prim_symm)
end