Theory Submonoids
theory Submonoids
imports CoWBasic
begin
chapter ‹Submonoids of a free monoid›
text‹This chapter deals with properties of submonoids of a free monoid, that is, with monoids of words.
See more in Chapter 1 of @{cite Lo83}.
›
section ‹Hull›
text‹First, we define the hull of a set of words, that is, the monoid generated by them.›
inductive_set hull :: "'a list set ⇒ 'a list set" (‹⟨_⟩›)
for G where
emp_in[simp]: "ε ∈ ⟨G⟩" |
prod_cl: "w1 ∈ G ⟹ w2 ∈ ⟨G⟩ ⟹ w1 ⋅ w2 ∈ ⟨G⟩"
lemmas [intro] = hull.intros
lemma hull_closed[intro]: "w1 ∈ ⟨G⟩ ⟹ w2 ∈ ⟨G⟩ ⟹ w1 ⋅ w2 ∈ ⟨G⟩"
by (rule hull.induct[of w1 G "λ x. (x⋅w2)∈⟨G⟩"]) auto+
lemma gen_in [intro]: "w ∈ G ⟹ w ∈ ⟨G⟩"
using hull.prod_cl by force
lemma hull_induct: assumes "x ∈ ⟨G⟩" "P ε" "⋀w. w ∈ G ⟹ P w"
"⋀w1 w2. w1 ∈ ⟨G⟩ ⟹ P w1 ⟹ w2 ∈ ⟨G⟩ ⟹ P w2 ⟹ P (w1 ⋅ w2)" shows "P x"
using hull.induct[of _ _ P, OF ‹x ∈ ⟨G⟩› ‹P ε›]
assms by (simp add: gen_in)
lemma genset_sub[simp]: "G ⊆ ⟨G⟩"
using gen_in ..
lemma genset_sub_lists: "ws ∈ lists G ⟹ ws ∈ lists ⟨G⟩"
using sub_lists_mono[OF genset_sub].
lemma in_lists_conv_set_subset: "set ws ⊆ G ⟷ ws ∈ lists G"
by blast
lemma concat_in_hull [intro]:
assumes "set ws ⊆ G"
shows "concat ws ∈ ⟨G⟩"
using assms by (induction ws) auto
lemma concat_in_hull' [intro]:
assumes "ws ∈ lists G"
shows "concat ws ∈ ⟨G⟩"
using assms by (induction ws) auto
lemma hull_concat_lists0: "w ∈ ⟨G⟩ ⟹ (∃ ws ∈ lists G. concat ws = w)"
proof(rule hull.induct[of _ G])
show "∃ws∈lists G. concat ws = ε"
using concat.simps(1) lists.Nil[of G] exI[of "λ x. concat x = ε", OF concat.simps(1)] by blast
show " ⋀w1 w2. w1 ∈ G ⟹ w2 ∈ ⟨G⟩ ⟹ ∃ws∈lists G. concat ws = w2 ⟹ ∃ws∈lists G. concat ws = w1 ⋅ w2"
using Cons_in_lists_iff concat.simps(2) by metis
qed simp
lemma hull_concat_listsE: assumes "w ∈ ⟨G⟩"
obtains ws where "ws ∈ lists G" and "concat ws = w"
using assms hull_concat_lists0 by blast
lemma hull_concat_lists: "⟨G⟩ = concat ` lists G"
using hull_concat_lists0 by blast
lemma concat_tl: "x # xs ∈ lists G ⟹ concat xs ∈ ⟨G⟩"
by (simp add: hull_concat_lists)
lemma nemp_concat_hull: assumes "us ≠ ε" and "us ∈ lists (G - {ε})"
shows "concat us ∈ ⟨G⟩" and "concat us ≠ ε"
using assms by fastforce+
lemma hull_mono: "A ⊆ B ⟹ ⟨A⟩ ⊆ ⟨B⟩"
proof
fix x assume "A ⊆ B" "x ∈ ⟨A⟩"
thus "x ∈ ⟨B⟩"
unfolding image_def hull_concat_lists using sub_lists_mono[OF ‹A ⊆ B›]
by blast
qed
lemma emp_gen_set: "⟨{}⟩ = {ε}"
unfolding hull_concat_lists by auto
lemma concat_lists_minus[simp]: "concat ` lists (G - {ε}) = concat ` lists G"
proof
show "concat ` lists G ⊆ concat ` lists (G - {ε})"
proof
fix x assume "x ∈ concat ` lists G"
from imageE[OF this]
obtain y where "x = concat y" "y ∈ lists G".
from lists_minus'[OF ‹y ∈ lists G›] del_emp_concat[of y, folded ‹x = concat y›]
show "x ∈ concat ` lists (G - {ε})"
by blast
qed
qed (simp add: image_mono lists_mono)
lemma hull_drop_one: "⟨G - {ε}⟩ = ⟨G⟩"
proof (intro equalityI subsetI)
fix x assume "x ∈ ⟨G⟩" thus "x ∈ ⟨G - {ε}⟩"
unfolding hull_concat_lists by simp
next
fix x assume "x ∈ ⟨G - {ε}⟩" thus "x ∈ ⟨G⟩"
unfolding hull_concat_lists image_iff by auto
qed
lemma sing_gen_power: "u ∈ ⟨{x}⟩ ⟹ ∃k. u = x⇧@k"
unfolding hull_concat_lists using one_generated_list_power by auto
lemma sing_gen[intro]: "w ∈ ⟨{z}⟩ ⟹ w ∈ z*"
using rootI sing_gen_power by blast
lemma pow_sing_gen[simp]: "x⇧@k ∈ ⟨{x}⟩"
using concat_in_hull[OF sing_pow_set_sub, unfolded concat_sing_pow].
lemma root_sing_gen: "w ∈ z* ⟹ w ∈ ⟨{z}⟩"
by (elim rootE) force
lemma sing_genE[elim]:
assumes "u ∈ ⟨{x}⟩"
obtains k where "x⇧@k = u"
using assms using sing_gen_power by blast
lemma sing_gen_root_conv: "w ∈ ⟨{z}⟩ ⟷ w ∈ z*"
using root_sing_gen by blast
lemma lists_gen_to_hull: "us ∈ lists (G - {ε}) ⟹ us ∈ lists (⟨G⟩ - {ε})"
using lists_mono genset_sub by force
lemma rev_hull: "rev`⟨G⟩ = ⟨rev`G⟩"
proof
show "rev ` ⟨G⟩ ⊆ ⟨rev ` G⟩"
proof
fix x assume "x ∈ rev ` ⟨G⟩"
then obtain xs where "x = rev (concat xs)" and "xs ∈ lists G"
unfolding hull_concat_lists by auto
from rev_in_lists[OF ‹xs ∈ lists G›]
have "(map rev (rev xs)) ∈ lists (rev ` G)"
by fastforce
thus "x ∈ ⟨rev ` G⟩"
unfolding image_iff hull_concat_lists
using ‹x = rev (concat xs)›[unfolded rev_concat] by blast
qed
show "⟨rev ` G⟩ ⊆ rev ` ⟨G⟩"
proof
fix x assume "x ∈ ⟨rev ` G⟩"
then obtain xs where "x = concat xs" and "xs ∈ lists (rev ` G)"
unfolding hull_concat_lists by blast
from rev_in_lists[OF ‹xs ∈ lists ((rev ` G))›]
have "map rev (rev xs) ∈ lists G"
by fastforce
hence "rev x ∈ ⟨G⟩"
unfolding ‹x = concat xs› rev_concat
by fast
thus "x ∈ rev ` ⟨G⟩"
unfolding rev_in_conv.
qed
qed
lemma power_in[intro]: "x ∈ ⟨G⟩ ⟹ x⇧@k ∈ ⟨G⟩"
by (induction k, auto)
lemma hull_closed_lists: "us ∈ lists ⟨G⟩ ⟹ concat us ∈ ⟨G⟩"
by (induct us, auto)
lemma hull_I [intro]:
"ε ∈ H ⟹ (⋀ x y. x ∈ H ⟹ y ∈ H ⟹ x ⋅ y ∈ H) ⟹ ⟨H⟩ = H"
by (standard, use hull.induct[of _ H "λ x. x ∈ H"] in force) (simp only: genset_sub)
lemma self_gen: "⟨⟨G⟩⟩ = ⟨G⟩"
using image_subsetI[of "lists ⟨G⟩" concat "⟨G⟩", unfolded hull_concat_lists[of "⟨G⟩", symmetric],
THEN subset_antisym[OF _ genset_sub[of "⟨G⟩"]]] hull_closed_lists[of _ G] by blast
lemma hull_mono'[intro]: "A ⊆ ⟨B⟩ ⟹ ⟨A⟩ ⊆ ⟨B⟩"
using hull_mono self_gen by blast
lemma hull_conjug [elim]: "w ∈ ⟨{r⋅s,s⋅r}⟩ ⟹ w ∈ ⟨{r,s}⟩"
using hull_mono[of "{r⋅s,s⋅r}" "⟨{r,s}⟩", unfolded self_gen] by blast
text‹Intersection of hulls is a hull.›
lemma hulls_inter: "⟨⋂ {⟨G⟩ | G. G ∈ S}⟩ = ⋂ {⟨G⟩ | G. G ∈ S}"
proof
{fix G assume "G ∈ S"
hence "⟨⋂ {⟨G⟩ |G. G ∈ S}⟩ ⊆ ⟨G⟩"
using Inter_lower[of "⟨G⟩" "{⟨G⟩ |G. G ∈ S}"] mem_Collect_eq[of "⟨G⟩" "λ A. ∃ G. G ∈ S ∧ A = ⟨G⟩"]
hull_mono[of "⋂ {⟨G⟩ |G. G ∈ S}" "⟨G⟩"] unfolding self_gen by auto}
thus "⟨⋂ {⟨G⟩ |G. G ∈ S}⟩ ⊆ ⋂ {⟨G⟩ |G. G ∈ S}" by blast
next
show "⋂ {⟨G⟩ |G. G ∈ S} ⊆ ⟨⋂ {⟨G⟩ |G. G ∈ S}⟩"
by simp
qed
lemma hull_keeps_root: "∀ u ∈ A. u ∈ r* ⟹ w ∈ ⟨A⟩ ⟹ w ∈ r*"
by (rule hull.induct[of _ _ "λ x. x ∈ r*"], auto)
lemma bin_hull_keeps_root [intro]: "u ∈ r* ⟹ v ∈ r* ⟹ w ∈ ⟨{u,v}⟩ ⟹ w ∈ r*"
by (rule hull.induct[of _ _ "λ x. x ∈ r*"], auto)
lemma bin_comm_hull_comm: "x ⋅ y = y ⋅ x ⟹ u ∈ ⟨{x,y}⟩ ⟹ v ∈ ⟨{x,y}⟩ ⟹ u ⋅ v = v ⋅ u"
unfolding comm_root using bin_hull_keeps_root by blast
lemma[reversal_rule]: "rev ` ⟨{rev u, rev v}⟩ = ⟨{u,v}⟩"
by (simp add: rev_hull)
lemma[reversal_rule]: "rev w ∈ ⟨rev ` G⟩ ≡ w ∈ ⟨G⟩"
unfolding rev_in_conv rev_hull rev_rev_image_eq.
section "Factorization into generators"
text‹We define a decomposition (or a factorization) of a into elements of a given generating set. Such a decomposition is well defined only
if the decomposed word is an element of the hull. Even int that case, however, the decomposition need not be unique.›
definition decompose :: "'a list set ⇒ 'a list ⇒ 'a list list" (‹Dec _ _› [55,55] 56) where
"decompose G u = (SOME us. us ∈ lists (G - {ε}) ∧ concat us = u)"
lemma dec_ex: assumes "u ∈ ⟨G⟩" shows "∃ us. (us ∈ lists (G - {ε}) ∧ concat us = u)"
using assms unfolding image_def hull_concat_lists[of G] mem_Collect_eq
using del_emp_concat lists_minus' by metis
lemma dec_in_lists': "u ∈ ⟨G⟩ ⟹ (Dec G u) ∈ lists (G - {ε})"
unfolding decompose_def using someI_ex[OF dec_ex] by blast
lemma concat_dec[simp, intro] : "u ∈ ⟨G⟩ ⟹ concat (Dec G u) = u"
unfolding decompose_def using someI_ex[OF dec_ex] by blast
lemma dec_emp [simp]: "Dec G ε = ε"
proof-
have ex: "ε ∈ lists (G - {ε}) ∧ concat ε = ε"
by simp
have all: "(us ∈ lists (G - {ε}) ∧ concat us = ε) ⟹ us = ε" for us
using emp_concat_emp by auto
show ?thesis
unfolding decompose_def
using all[OF someI[of "λ x. x ∈ lists (G - {ε}) ∧ concat x = ε", OF ex]].
qed
lemma dec_nemp: "u ∈ ⟨G⟩ - {ε} ⟹ Dec G u ≠ ε"
using concat_dec[of u G] by force
lemma dec_nemp'[simp, intro]: "u ≠ ε ⟹ u ∈ ⟨G⟩ ⟹ Dec G u ≠ ε"
using dec_nemp by blast
lemma dec_eq_emp_iff [simp]: assumes "u ∈ ⟨G⟩" shows "Dec G u = ε ⟷ u = ε"
using dec_nemp'[OF _ ‹u ∈ ⟨G⟩›] by auto
lemma dec_in_lists[simp]: "u ∈ ⟨G⟩ ⟹ Dec G u ∈ lists G"
using dec_in_lists' by auto
lemma set_dec_sub: "x ∈ ⟨G⟩ ⟹ set (Dec G x) ⊆ G"
using dec_in_lists by blast
lemma dec_hd: "u ≠ ε ⟹ u ∈ ⟨G⟩ ⟹ hd (Dec G u) ∈ G"
by simp
lemma non_gen_dec: assumes "u ∈ ⟨G⟩" "u ∉ G" shows "Dec G u ≠ [u]"
using dec_in_lists[OF ‹u ∈ ⟨G⟩›] Cons_in_lists_iff[of u ε G] ‹u ∉ G› by argo
subsection ‹Refinement into a specific decomposition›
text‹We extend the decomposition to lists of words. This can be seen as a refinement of a previous decomposition of some word.›
definition refine :: "'a list set ⇒ 'a list list ⇒ 'a list list" (‹Ref _ _› [51,51] 65) where
"refine G us = concat(map (decompose G) us)"
lemma ref_morph: "us ∈ lists ⟨G⟩ ⟹ vs ∈ lists ⟨G⟩ ⟹ refine G (us ⋅ vs) = refine G us ⋅ refine G vs"
unfolding refine_def by simp
lemma ref_conjug:
"u ∼ v ⟹ (Ref G u) ∼ Ref G v"
unfolding refine_def by (intro conjug_concat_conjug map_conjug)
lemma ref_morph_plus: "us ∈ lists (⟨G⟩ - {ε}) ⟹ vs ∈ lists (⟨G⟩ - {ε}) ⟹ refine G (us ⋅ vs) = refine G us ⋅ refine G vs"
unfolding refine_def by simp
lemma ref_pref_mono: "ws ∈ lists ⟨G⟩ ⟹ us ≤p ws ⟹ Ref G us ≤p Ref G ws"
unfolding prefix_def using ref_morph append_in_lists_dest' append_in_lists_dest by metis
lemma ref_suf_mono: "ws ∈ lists ⟨G⟩ ⟹ us ≤s ws ⟹ (Ref G us) ≤s Ref G ws"
unfolding suffix_def using ref_morph append_in_lists_dest' append_in_lists_dest by metis
lemma ref_fac_mono: "ws ∈ lists ⟨G⟩ ⟹ us ≤f ws ⟹ (Ref G us) ≤f Ref G ws"
unfolding sublist_altdef' using ref_pref_mono ref_suf_mono suf_in_lists by metis
lemma ref_pop_hd: "us ≠ ε ⟹ us ∈ lists ⟨G⟩ ⟹ refine G us = decompose G (hd us) ⋅ refine G (tl us)"
unfolding refine_def using list.simps(9)[of "decompose G" "hd us" "tl us"] by simp
lemma ref_in: "us ∈ lists ⟨G⟩ ⟹ (Ref G us) ∈ lists (G - {ε})"
proof (induction us)
case (Cons a us)
then show ?case
using Cons.IH Cons.prems dec_in_lists' by (auto simp add: refine_def)
qed (simp add: refine_def)
lemma ref_in'[intro]: "us ∈ lists ⟨G⟩ ⟹ (Ref G us) ∈ lists G"
using ref_in by auto
lemma concat_ref: "us ∈ lists ⟨G⟩ ⟹ concat (Ref G us) = concat us"
proof (induction us)
case (Cons a us)
then show ?case
using Cons.IH Cons.prems concat_dec refine_def by (auto simp add: refine_def)
qed (simp add: refine_def)
lemma ref_gen: "us ∈ lists B ⟹ B ⊆ ⟨G⟩ ⟹ Ref G us ∈ ⟨decompose G ` B⟩"
by (induct us, auto simp add: refine_def)
lemma ref_set: "ws ∈ lists ⟨G⟩ ⟹ set (Ref G ws) = ⋃ (set`(decompose G)`set ws)"
by (simp add: refine_def)
lemma emp_ref: assumes "us ∈ lists (⟨G⟩ - {ε})" and "Ref G us = ε" shows "us = ε"
using emp_concat_emp[OF ‹us ∈ lists (⟨G⟩ - {ε})›]
concat_ref [OF lists_minus[OF assms(1)], unfolded ‹Ref G us = ε› concat.simps(1),symmetric] by blast
lemma sing_ref_sing:
assumes "us ∈ lists (⟨G⟩ - {ε})" and "refine G us = [b]"
shows "us = [b]"
proof-
have "us ≠ ε"
using ‹refine G us = [b]› by (auto simp add: refine_def)
have "tl us ∈ lists (⟨G⟩ - {ε})" and "hd us ∈ ⟨G⟩ - {ε}"
using list.collapse[OF ‹us ≠ ε›] ‹us ∈ lists (⟨G⟩ - {ε})› Cons_in_lists_iff[of "hd us" "tl us" "⟨G⟩ - {ε}"]
by auto
have "Dec G (hd us) ≠ ε"
using dec_nemp[OF ‹hd us ∈ ⟨G⟩ - {ε}›].
have "us ∈ lists ⟨G⟩"
using ‹us ∈ lists (⟨G⟩ - {ε})› lists_minus by auto
have "concat us = b"
using ‹us ∈ lists ⟨G⟩› assms(2) concat_ref by force
have "refine G (tl us) = ε"
using ref_pop_hd[OF ‹us ≠ ε› ‹us ∈ lists ⟨G⟩›] unfolding ‹refine G us = [b]›
using ‹Dec G (hd us) ≠ ε› Cons_eq_append_conv[of b ε "(Dec G (hd us))" "(Ref G (tl us))"]
Cons_eq_append_conv[of b ε "(Dec G (hd us))" "(Ref G (tl us))"] append_is_Nil_conv[of _ "(Ref G (tl us))"]
by blast
from emp_ref[OF ‹tl us ∈ lists (⟨G⟩ - {ε})› this, symmetric]
have "ε = tl us".
from this[unfolded Nil_tl]
show ?thesis
using ‹us ≠ ε› ‹concat us = b› by auto
qed
lemma ref_ex: assumes "Q ⊆ ⟨G⟩" and "us ∈ lists Q"
shows "Ref G us ∈ lists (G - {ε})" and "concat (Ref G us) = concat us"
using ref_in[OF sub_lists_mono[OF assms]] concat_ref[OF sub_lists_mono[OF assms]].
section "Basis"
text‹An important property of monoids of words is that they have a unique minimal generating set. Which is the set consisting of indecomposable elements.›
text‹The simple element is defined as a word which has only trivial decomposition into generators: a singleton.›
definition simple_element :: "'a list ⇒ 'a list set ⇒ bool" (‹ _ ∈B _ › [51,51] 50) where
"simple_element b G = (b ∈ G ∧ (∀ us. us ∈ lists (G - {ε}) ∧ concat us = b ⟶ ❙|us❙| = 1))"
lemma simp_el_el: "b ∈B G ⟹ b ∈ G"
unfolding simple_element_def by blast
lemma simp_elD: "b ∈B G ⟹ us ∈ lists (G - {ε}) ⟹ concat us = b ⟹ ❙|us❙| = 1"
unfolding simple_element_def by blast
lemma simp_el_sing: assumes "b ∈B G" "us ∈ lists (G - {ε})" "concat us = b" shows "us = [b]"
using ‹concat us = b› concat_len_one[OF simp_elD[OF assms]] sing_word[OF simp_elD[OF assms]] by simp
lemma nonsimp: "us ∈ lists (G - {ε}) ⟹ concat us ∈B G ⟹ us = [concat us]"
using simp_el_sing[of "concat us" G us] unfolding simple_element_def
by blast
lemma emp_nonsimp: assumes "b ∈B G" shows "b ≠ ε"
using simp_elD[OF assms, of ε] by force
lemma basis_no_fact: assumes "u ∈ ⟨G⟩" and "v ∈ ⟨G⟩" and "u ⋅ v ∈B G" shows "u = ε ∨ v = ε"
proof-
have eq1: "concat ((Dec G u) ⋅ (Dec G v)) = u ⋅ v"
using concat_morph[of "Dec G u" "Dec G v"]
unfolding concat_dec[OF ‹u ∈ ⟨G⟩›] concat_dec[OF ‹v ∈ ⟨G⟩›].
have eq2: "(Dec G u) ⋅ (Dec G v) = [u ⋅ v]"
using ‹u ⋅ v ∈B G› nonsimp[of "(Dec G u) ⋅ (Dec G v)"]
unfolding eq1 append_in_lists_conv[of "(Dec G u)" "(Dec G v)" "G - {ε}"]
using dec_in_lists'[OF ‹u ∈ ⟨G⟩›] dec_in_lists'[OF ‹v ∈ ⟨G⟩›]
by (meson append_in_lists_conv)
have "Dec G u = ε ∨ Dec G v = ε"
using butlast_append[of "Dec G u" "Dec G v"] unfolding eq2 butlast.simps(2)[of "u⋅v" ε]
using Nil_is_append_conv[of "Dec G u" "butlast (Dec G v)"] by auto
thus ?thesis
using concat_dec[OF ‹u ∈ ⟨G⟩›] concat_dec[OF ‹v ∈ ⟨G⟩›]
concat.simps(1)
by auto
qed
lemma simp_elI:
assumes "b ∈ G" and "b ≠ ε" and all: "∀ u v. u ≠ ε ∧ u ∈ ⟨G⟩ ∧ v ≠ ε ∧ v ∈ ⟨G⟩ ⟶ u ⋅ v ≠ b"
shows "b ∈B G"
unfolding simple_element_def
proof(rule conjI)
show "∀us. us ∈ lists (G - {ε}) ∧ concat us = b ⟶ ❙|us❙| = 1"
proof (rule allI, rule impI, elim conjE)
fix us assume "us ∈ lists (G - {ε})" "concat us = b"
hence "us ≠ ε" using ‹b ≠ ε› concat.simps(1) by blast
hence "hd us ∈ ⟨G⟩" and "hd us ≠ ε"
using ‹us ∈ lists (G - {ε})› lists_hd_in_set gen_in by auto
have "tl us = ε"
proof(rule ccontr)
assume "tl us ≠ ε"
from nemp_concat_hull[of "tl us", OF this tl_in_lists[OF ‹us ∈ lists (G - {ε})›]]
show False
using all ‹hd us ≠ ε› ‹hd us ∈ ⟨G⟩› concat.simps(2)[of "hd us" "tl us", symmetric]
unfolding list.collapse[OF ‹us ≠ ε›] ‹concat us = b›
by blast
qed
thus "❙|us❙| = 1"
using long_list_tl[of us] Nitpick.size_list_simp(2)[of us] ‹us ≠ ε› by fastforce
qed
qed (simp add: ‹b ∈ G›)
lemma simp_el_indecomp:
assumes "b ∈B G" "u ≠ ε" "u ∈ ⟨G⟩" "v ≠ ε" "v ∈ ⟨G⟩"
shows "u ⋅ v ≠ b"
using basis_no_fact[OF ‹u ∈ ⟨G⟩› ‹v ∈ ⟨G⟩›] ‹u ≠ ε› ‹v ≠ ε› ‹b ∈B G› by blast
text‹We are ready to define the \emph{basis} as the set of all simple elements.›
definition basis :: "'a list set ⇒ 'a list set" (‹𝔅 _› [51] ) where
"basis G = {x. x ∈B G}"
lemma basis_inI: "x ∈B G ⟹ x ∈ 𝔅 G"
unfolding basis_def by simp
lemma basisD: "x ∈ 𝔅 G ⟹ x ∈B G"
unfolding basis_def by simp
lemma emp_not_basis: "x ∈ 𝔅 G ⟹ x ≠ ε"
using basisD emp_nonsimp by blast
lemma basis_sub: "𝔅 G ⊆ G"
unfolding basis_def simple_element_def by simp
lemma basis_drop_emp: "(𝔅 G) - {ε} = 𝔅 G"
using emp_not_basis by blast
lemma simp_el_hull': assumes "b ∈B ⟨G⟩" shows "b ∈B G"
proof-
have all: "∀us. us ∈ lists (G - {ε}) ∧ concat us = b ⟶ ❙|us❙| = 1"
using assms lists_gen_to_hull unfolding simple_element_def by metis
have "b ∈ ⟨G⟩"
using assms simp_elD unfolding simple_element_def by blast
obtain bs where "bs ∈ lists (G - {ε})" and "concat bs = b"
using dec_ex[OF ‹b ∈ ⟨G⟩›] by blast
have "b ∈ G"
using
lists_minus[OF ‹bs ∈ lists (G - {ε})›]
lists_gen_to_hull[OF ‹bs ∈ lists (G - {ε})›, THEN nonsimp[of bs "⟨G⟩"],
unfolded ‹concat bs = b›, OF ‹b ∈B ⟨G⟩›] by force
thus "b ∈B G"
by (simp add: all simple_element_def)
qed
lemma simp_el_hull: assumes "b ∈B G" shows "b ∈B ⟨G⟩"
using simp_elI[of b "⟨G⟩", OF _ emp_nonsimp[OF assms]] unfolding self_gen
using simp_el_indecomp[OF ‹b ∈B G›] gen_in[OF simp_el_el[OF assms]] by presburger
lemma concat_tl_basis: "x # xs ∈ lists 𝔅 G ⟹ concat xs ∈ ⟨G⟩"
unfolding hull_concat_lists basis_def simple_element_def by auto
text‹The basis generates the hull›
lemma set_concat_len: assumes "us ∈ lists (G - {ε})" "1 < ❙|us❙|" "u ∈ set us" shows "❙|u❙| < ❙|concat us❙|"
proof-
obtain x y where "us = x ⋅ [u] ⋅ y" and "x ⋅ y ≠ ε"
using split_list_long[OF ‹1 < ❙|us❙|› ‹u ∈ set us›].
hence "x ⋅ y ∈ lists (G - {ε})"
using ‹us ∈ lists (G - {ε})› by auto
hence "❙|concat (x ⋅ y)❙| ≠ 0"
using ‹x ⋅ y ≠ ε› in_lists_conv_set by force
hence "❙|concat us❙| = ❙|u❙| + ❙|concat x❙| + ❙|concat y❙|"
using lenmorph ‹us = x ⋅ [u] ⋅ y› by simp
thus ?thesis
using ‹❙|concat (x ⋅ y)❙| ≠ 0› by auto
qed
lemma non_simp_dec: assumes "w ∉ 𝔅 G" "w ≠ ε" "w ∈ G"
obtains us where "us ∈ lists (G - {ε})" "1 < ❙|us❙|" "concat us = w"
using ‹w ≠ ε› ‹w ∈ G› ‹w ∉ 𝔅 G› basis_inI[of w G, unfolded simple_element_def]
using concat.simps(1) nemp_le_len nless_le by metis
lemma basis_gen: "w ∈ G ⟹ w ∈ ⟨𝔅 G⟩"
proof (induct "length w" arbitrary: w rule: less_induct)
case less
show ?case
proof (cases "w ∈ 𝔅 G ∨ w = ε", blast)
assume "¬ (w ∈ 𝔅 G ∨ w = ε)"
with ‹w ∈ G›
obtain us where "us ∈ lists (G - {ε})" "1 < ❙|us❙|" "concat us = w"
using non_simp_dec by blast
have "u ∈ set us ⟹ u ∈ ⟨𝔅 G⟩" for u
using lists_minus[OF ‹us ∈ lists (G - {ε})›] less(1)[OF set_concat_len[OF ‹us ∈ lists (G - {ε})› ‹1 < ❙|us❙|›, unfolded ‹concat us = w›], of u]
by blast
thus "w ∈ ⟨𝔅 G⟩ "
unfolding ‹concat us = w›[symmetric]
using hull_closed_lists[OF in_listsI] by blast
qed
qed
lemmas basis_concat_listsE = hull_concat_listsE[OF basis_gen]
theorem basis_gen_hull: "⟨𝔅 G⟩ = ⟨G⟩"
proof
show "⟨𝔅 G⟩ ⊆ ⟨G⟩"
unfolding hull_concat_lists basis_def simple_element_def by auto
show "⟨G⟩ ⊆ ⟨𝔅 G⟩"
proof
fix x show "x ∈ ⟨G⟩ ⟹ x ∈ ⟨𝔅 G⟩"
proof (induct rule: hull.induct)
show "⋀w1 w2. w1 ∈ G ⟹ w2 ∈ ⟨𝔅 G⟩ ⟹ w1 ⋅ w2 ∈ ⟨𝔅 G⟩"
using hull_closed[of _ "𝔅 G"] basis_gen[of _ G] by blast
qed auto
qed
qed
lemma basis_gen_hull': "⟨𝔅 ⟨G⟩⟩ = ⟨G⟩"
using basis_gen_hull self_gen by blast
theorem basis_of_hull: "𝔅 ⟨G⟩ = 𝔅 G"
proof
show "𝔅 G ⊆ 𝔅 ⟨G⟩"
using basisD basis_inI simp_el_hull by blast
show "𝔅 ⟨G⟩ ⊆ 𝔅 G"
using basisD basis_inI simp_el_hull' by blast
qed
lemma basis_hull_sub: "𝔅 ⟨G⟩ ⊆ G"
using basis_of_hull basis_sub by blast
text‹The basis is the smallest generating set.›
theorem basis_sub_gen: "⟨S⟩ = ⟨G⟩ ⟹ 𝔅 G ⊆ S"
using basis_of_hull basis_sub by metis
lemma basis_min_gen: "S ⊆ 𝔅 G ⟹ ⟨S⟩ = G ⟹ S = 𝔅 G"
using basis_of_hull basis_sub by blast
lemma basisI: "(⋀ B. ⟨B⟩ = ⟨C⟩ ⟹ C ⊆ B) ⟹ 𝔅 ⟨C⟩ = C"
using basis_gen_hull basis_min_gen basis_of_hull by metis
thm basis_inI
text‹An arbitrary set between basis and the hull is generating...›
lemma gen_sets: assumes "𝔅 G ⊆ S" and "S ⊆ ⟨G⟩" shows "⟨S⟩ = ⟨G⟩"
using image_mono[OF lists_mono[of S "⟨G⟩"], of concat, OF ‹S ⊆ ⟨G⟩›] image_mono[OF lists_mono[of "𝔅 G" S], of concat, OF ‹𝔅 G ⊆ S›]
unfolding sym[OF hull_concat_lists] basis_gen_hull
using subset_antisym[of "⟨S⟩" "⟨G⟩"] self_gen by metis
text‹... and has the same basis›
lemma basis_sets: "𝔅 G ⊆ S ⟹ S ⊆ ⟨G⟩ ⟹ 𝔅 G = 𝔅 S"
by (metis basis_of_hull gen_sets)
text‹Any nonempty composed element has a decomposition into basis elements with many useful properties›
lemma non_simp_fac: assumes "w ≠ ε" and "w ∈ ⟨G⟩" and "w ∉ 𝔅 G"
obtains us where "1 < ❙|us❙|" and "us ≠ ε" and "us ∈ lists 𝔅 G" and
"hd us ≠ ε" and "hd us ∈ ⟨G⟩" and
"concat(tl us) ≠ ε" and "concat(tl us) ∈ ⟨G⟩" and
"w = hd us ⋅ concat(tl us)"
proof-
obtain us where "us ∈ lists 𝔅 G" and "concat us = w"
using ‹w ∈ ⟨G⟩› dec_in_lists[of w "𝔅 G"] concat_dec[of w "𝔅 G"]
unfolding basis_gen_hull
by blast
hence "us ≠ ε"
using ‹w ≠ ε› concat.simps(1)
by blast
from lists_hd_in_set[OF this ‹us ∈ lists 𝔅 G›, THEN emp_not_basis]
lists_hd_in_set[OF this ‹us ∈ lists 𝔅 G›, THEN gen_in[of "hd us" "𝔅 G", unfolded basis_gen_hull]]
have "hd us ≠ ε" and "hd us ∈ ⟨G⟩".
have "1 < ❙|us❙|"
using ‹w ∉ 𝔅 G› lists_hd_in_set[OF ‹us ≠ ε› ‹us ∈ lists 𝔅 G›] ‹w ≠ ε› ‹w ∈ ⟨G⟩›
concat_len_one[of us, unfolded ‹concat us = w›]
‹us ≠ ε› leI nemp_le_len order_antisym_conv by metis
from nemp_concat_hull[OF long_list_tl[OF this], of "𝔅 G", unfolded basis_drop_emp basis_gen_hull, OF tl_in_lists[OF ‹us ∈ lists 𝔅 G›]]
have "concat (tl us) ∈ ⟨G⟩" and "concat(tl us) ≠ ε".
have "w = hd us ⋅ concat(tl us)"
using ‹us ≠ ε› ‹us ∈ lists 𝔅 G› ‹concat us = w› concat.simps(2)[of "hd us" "tl us"] list.collapse[of us]
by argo
from that[OF ‹1 < ❙|us❙|› ‹us ≠ ε› ‹us ∈ lists 𝔅 G› ‹hd us ≠ ε› ‹hd us ∈ ⟨G⟩› ‹concat (tl us) ≠ ε› ‹concat (tl us) ∈ ⟨G⟩› this]
show thesis.
qed
lemma basis_dec: "p ∈ ⟨G⟩ ⟹ s ∈ ⟨G⟩ ⟹ p ⋅ s ∈ 𝔅 G ⟹ p = ε ∨ s = ε"
using basis_no_fact[of p G s] unfolding basis_def by simp
lemma non_simp_fac': "w ∉ 𝔅 G ⟹ w ≠ ε ⟹ w ∈ ⟨G⟩ ⟹ ∃us. us ∈ lists (G - {ε}) ∧ w = concat us ∧ ❙|us❙| ≠ 1"
by (metis basis_inI concat_len_one dec_in_lists' dec_in_lists concat_dec dec_nemp lists_hd_in_set nemp_elem_setI simple_element_def)
lemma emp_gen_iff: "(G - {ε}) = {} ⟷ ⟨G⟩ = {ε}"
proof
assume "G - {ε} = {}" show "⟨G⟩ = {ε}"
using hull_drop_one[of G, unfolded ‹G - {ε} = {}› emp_gen_set] by simp
next
assume "⟨G⟩ = {ε}" thus"G - {ε} = {}" by blast
qed
lemma emp_basis_iff: "𝔅 G = {} ⟷ G - {ε} = {}"
using emp_gen_iff[of "𝔅 G", unfolded basis_gen_hull basis_drop_emp, folded emp_gen_iff].
section "Code"
locale nemp_words =
fixes G
assumes emp_not_in: "ε ∉ G"
begin
lemma drop_empD: "G - {ε} = G"
using emp_not_in by simp
lemmas emp_concat_emp' = emp_concat_emp[of _ G, unfolded drop_empD]
thm disjE[OF ruler[OF take_is_prefix take_is_prefix]]
lemma concat_take_mono: assumes "ws ∈ lists G" and "concat (take i ws) ≤p concat (take j ws)"
shows "take i ws ≤p take j ws"
proof (rule disjE[OF ruler[OF take_is_prefix take_is_prefix]])
assume "take j ws ≤p take i ws"
from prefixE[OF this]
obtain us where "take i ws = take j ws ⋅ us".
hence "us ∈ lists G" using ‹ws ∈ lists G›
using append_in_lists_conv take_in_lists by metis
have "concat (take j ws) = concat (take i ws)"
using pref_concat_pref[OF ‹take j ws ≤p take i ws›] assms(2) by simp
from arg_cong[OF ‹take i ws = take j ws ⋅ us›, of concat, unfolded concat_morph, unfolded this]
have "us = ε"
using ‹us ∈ lists G› emp_concat_emp' by blast
thus "take i ws ≤p take j ws"
using ‹take i ws = take j ws ⋅ us› by force
qed
lemma nemp: "x ∈ G ⟹ x ≠ ε"
using emp_not_in by blast
lemma code_concat_eq_emp_iff [simp]: "us ∈ lists G ⟹ concat us = ε ⟷ us = ε"
unfolding in_lists_conv_set concat_eq_Nil_conv
by (simp add: nemp)
lemma root_dec_inj_on: "inj_on (λ x. [ρ x]⇧@(e⇩ρ x)) G"
unfolding inj_on_def using primroot_exp_eq
unfolding concat_sing_pow[of "ρ _", symmetric] by metis
lemma concat_root_dec_eq_concat:
assumes "ws ∈ lists G"
shows "concat (concat (map (λ x. [ρ x]⇧@(e⇩ρ x)) ws)) = concat ws"
(is "concat(concat (map ?R ws)) = concat ws")
using assms
by (induction ws, simp_all add: nemp)
end
text‹A basis freely generating its hull is called a \emph{code}. By definition,
this means that generated elements have unique factorizations into the elements of the code.›
locale code =
fixes 𝒞
assumes is_code: "xs ∈ lists 𝒞 ⟹ ys ∈ lists 𝒞 ⟹ concat xs = concat ys ⟹ xs = ys"
begin
lemma code_not_comm: "x ∈ 𝒞 ⟹ y ∈ 𝒞 ⟹ x ≠ y ⟹ x ⋅ y ≠ y ⋅ x"
using is_code[of "[x,y]" "[y,x]"] by auto
lemma emp_not_in: "ε ∉ 𝒞"
proof
assume "ε ∈ 𝒞"
hence "[] ∈ lists 𝒞" and "[ε] ∈ lists 𝒞" and "concat [] = concat [ε]" and "[] ≠ [ε]"
by simp+
thus False
using is_code by blast
qed
lemma nemp: "u ∈ 𝒞 ⟹ u ≠ ε"
using emp_not_in by force
sublocale nemp_words 𝒞
using emp_not_in by unfold_locales
lemma code_simple: "c ∈ 𝒞 ⟹ c ∈B 𝒞"
unfolding simple_element_def
proof
fix c assume "c ∈ 𝒞"
hence "[c] ∈ lists 𝒞"
by simp
show "∀us. us ∈ lists (𝒞 - {ε}) ∧ concat us = c ⟶ ❙|us❙| = 1"
proof
fix us
{assume "us ∈ lists (𝒞 - {ε})" "concat us = c"
hence "us ∈ lists 𝒞" by blast
hence "us = [c]"
using ‹concat us = c› ‹c ∈ 𝒞› is_code[of "[c]", OF ‹[c] ∈ lists 𝒞› ‹us ∈ lists 𝒞›] emp_not_in by auto}
thus "us ∈ lists (𝒞 - {ε}) ∧ concat us = c ⟶ ❙|us❙| = 1"
using sing_len[of c] by fastforce
qed
qed
lemma code_is_basis: "𝔅 𝒞 = 𝒞"
using code_simple basis_def[of 𝒞] basis_sub by blast
lemma code_unique_dec': "us ∈ lists 𝒞 ⟹ Dec 𝒞 (concat us) = us"
using dec_in_lists[of "concat us" 𝒞, THEN is_code, of us]
concat_dec[of "concat us" 𝒞] hull_concat_lists[of 𝒞] image_eqI[of "concat us" concat us "lists 𝒞"]
by argo
lemma code_unique_dec [intro!]: "us ∈ lists 𝒞 ⟹ concat us = u ⟹ Dec 𝒞 u = us"
using code_unique_dec' by blast
lemma triv_refine[intro!] : "us ∈ lists 𝒞 ⟹ concat us = u ⟹ Ref 𝒞 [u] = us"
using code_unique_dec' by (auto simp add: refine_def)
lemma code_unique_ref: "us ∈ lists ⟨𝒞⟩ ⟹ refine 𝒞 us = decompose 𝒞 (concat us)"
proof-
assume "us ∈ lists ⟨𝒞⟩"
hence "concat (refine 𝒞 us) = concat us"
using concat_ref by blast
hence eq: "concat (refine 𝒞 us) = concat (decompose 𝒞 (concat us))"
using concat_dec[OF hull_closed_lists[OF ‹us ∈ lists ⟨𝒞⟩›]] by auto
have dec: "Dec 𝒞 (concat us) ∈ lists 𝒞"
using ‹us ∈ lists ⟨𝒞⟩› dec_in_lists hull_closed_lists
by metis
have "Ref 𝒞 us ∈ lists 𝒞"
using lists_minus[OF ref_in[OF ‹us ∈ lists ⟨𝒞⟩›]].
from is_code[OF this dec eq]
show ?thesis.
qed
lemma refI [intro]: "us ∈ lists ⟨𝒞⟩ ⟹ vs ∈ lists 𝒞 ⟹ concat vs = concat us ⟹ Ref 𝒞 us = vs"
unfolding code_unique_ref code_unique_dec..
lemma code_dec_morph: assumes "x ∈ ⟨𝒞⟩" "y ∈ ⟨𝒞⟩"
shows "(Dec 𝒞 x) ⋅ (Dec 𝒞 y) = Dec 𝒞 (x⋅y)"
proof-
have eq: "(Dec 𝒞 x) ⋅ (Dec 𝒞 y) = Dec 𝒞 (concat ((Dec 𝒞 x) ⋅ (Dec 𝒞 y)))"
using dec_in_lists[OF ‹x ∈ ⟨𝒞⟩›] dec_in_lists[OF ‹y ∈ ⟨𝒞⟩›]
code.code_unique_dec[OF code_axioms, of "(Dec 𝒞 x) ⋅ (Dec 𝒞 y)", unfolded append_in_lists_conv, symmetric]
by presburger
moreover have "concat ((Dec 𝒞 x) ⋅ (Dec 𝒞 y)) = (x ⋅ y)"
using concat_morph[of "Dec 𝒞 x" "Dec 𝒞 y"]
unfolding concat_dec[OF ‹x ∈ ⟨𝒞⟩›] concat_dec[OF ‹y ∈ ⟨𝒞⟩›].
ultimately show "(Dec 𝒞 x) ⋅ (Dec 𝒞 y) = Dec 𝒞 (x⋅y)"
by argo
qed
lemma dec_pow: "rs ∈ ⟨𝒞⟩ ⟹ Dec 𝒞 (rs⇧@k) = (Dec 𝒞 rs)⇧@k"
proof(induction k arbitrary: rs, fastforce)
case (Suc k)
then show ?case
using code_dec_morph pow_Suc power_in by metis
qed
lemma code_el_dec: "c ∈ 𝒞 ⟹ decompose 𝒞 c = [c]"
by fastforce
lemma code_ref_list: "us ∈ lists 𝒞 ⟹ refine 𝒞 us = us"
proof (induct us)
case (Cons a us)
then show ?case using code_el_dec
unfolding refine_def by simp
qed (simp add: refine_def)
lemma code_ref_gen: assumes "G ⊆ ⟨𝒞⟩" "u ∈ ⟨G⟩"
shows "Dec 𝒞 u ∈ ⟨decompose 𝒞 ` G⟩"
proof-
have "refine 𝒞 (Dec G u) = Dec 𝒞 u"
using dec_in_lists[OF ‹u ∈ ⟨G⟩›] ‹G ⊆ ⟨𝒞⟩› code_unique_ref[of "Dec G u", unfolded concat_dec[OF ‹u ∈ ⟨G⟩›]] by blast
from ref_gen[of "Dec G u" G, OF dec_in_lists[OF ‹u ∈ ⟨G⟩›], of 𝒞, unfolded this, OF ‹G ⊆ ⟨𝒞⟩›]
show ?thesis.
qed
find_theorems "ρ ?x ⇧@ ?k = ?x" "0 < ?k"
lemma code_rev_code: "code (rev ` 𝒞)"
proof
fix xs ys assume "xs ∈ lists (rev ` 𝒞)" "ys ∈ lists (rev ` 𝒞)" "concat xs = concat ys"
have "map rev (rev xs) ∈ lists 𝒞" and "map rev (rev ys) ∈ lists 𝒞"
using rev_in_lists[OF ‹xs ∈ lists (rev ` 𝒞)›] rev_in_lists[OF ‹ys ∈ lists (rev ` 𝒞)›] map_rev_lists_rev
by (metis imageI)+
moreover have "concat (map rev (rev xs)) = concat (map rev (rev ys))"
unfolding rev_concat[symmetric] using ‹concat xs = concat ys› by blast
ultimately have "map rev (rev xs) = map rev (rev ys)"
using is_code by blast
thus "xs = ys"
using ‹concat xs = concat ys› by simp
qed
lemma dec_rev [simp, reversal_rule]:
"u ∈ ⟨𝒞⟩ ⟹ Dec rev ` 𝒞 (rev u) = rev (map rev (Dec 𝒞 u))"
by (auto simp only: rev_map lists_image rev_in_lists rev_concat[symmetric] dec_in_lists
intro!: code_rev_code code.code_unique_dec imageI del: in_listsI)
lemma elem_comm_sing_set: assumes "ws ∈ lists 𝒞" and "ws ≠ ε" and "u ∈ 𝒞" and "concat ws ⋅ u = u ⋅ concat ws"
shows "set ws = {u}"
using assms
proof-
have "concat (ws ⋅ [u]) = concat ([u] ⋅ ws)"
using assms by simp
have "ws ⋅ [u] = [u] ⋅ ws"
using ‹u ∈ 𝒞› ‹ws ∈ lists 𝒞› is_code[OF _ _ ‹concat (ws ⋅ [u]) = concat ([u] ⋅ ws)›]
by simp
from comm_nemp_pows_posE[OF this ‹ws ≠ ε› not_Cons_self2[of u ε]]
obtain t k m where "ws = t⇧@k" "[u] = t⇧@m" "0 < k" "0 < m" "primitive t".
hence "t = [u]"
by force
show "set ws = {u}"
using sing_pow_set[OF ‹0 < k›] unfolding ‹ws = t⇧@k› ‹t = [u]›.
qed
lemma pure_code_pres_prim: assumes pure: "∀u ∈ ⟨𝒞⟩. ρ u ∈ ⟨𝒞⟩" and
"w ∈ ⟨𝒞⟩" and "primitive (Dec 𝒞 w)"
shows "primitive w"
proof-
obtain k where "(ρ w)⇧@k = w"
using primroot_expE by blast
have "ρ w ∈ ⟨𝒞⟩"
using assms(2) pure by auto
have "(Dec 𝒞 (ρ w))⇧@k ∈ lists 𝒞"
by (metis ‹ρ w ∈ ⟨𝒞⟩› concat_sing_pow dec_in_lists flatten_lists order_refl sing_pow_lists)
have "(Dec 𝒞 (ρ w))⇧@k = Dec 𝒞 w"
using ‹(Dec 𝒞 (ρ w)) ⇧@ k ∈ lists 𝒞› code.code_unique_dec code_axioms concat_morph_power ‹(ρ w) ⇧@ k = w› concat_dec[OF ‹ρ w ∈ ⟨𝒞⟩›] by metis
hence "k = 1"
using ‹primitive (Dec 𝒞 w)› unfolding primitive_def by blast
thus "primitive w"
by (metis pow_1 ‹ρ w ⇧@ k = w› assms(3) dec_emp prim_nemp primroot_prim)
qed
lemma inj_on_dec: "inj_on (decompose 𝒞) ⟨𝒞⟩"
by (rule inj_onI) (use concat_dec in force)
end
lemma emp_is_code: "code {}"
using code.intro empty_iff insert_iff lists_empty by metis
lemma code_induct_hd: assumes "ε ∉ C" and
"⋀ xs ys. xs ∈ lists C ⟹ ys ∈ lists C ⟹ concat xs = concat ys ⟹ hd xs = hd ys"
shows "code C"
proof
show "xs ∈ lists C ⟹ ys ∈ lists C ⟹ concat xs = concat ys ⟹ xs = ys" for xs ys
proof (induct xs ys rule: list_induct2')
case (4 x xs y ys)
from assms(2)[OF "4.prems"]
have "x = y" by force
from "4.prems"[unfolded this]
have "xs ∈ lists C" and "ys ∈ lists C" and "concat xs = concat ys"
by simp_all
from "4.hyps"[OF this] ‹x = y›
show ?case
by simp
qed (auto simp add: ‹ε ∉ C›)
qed
lemma ref_set_primroot: assumes "ws ∈ lists (G - {ε})" and "code (ρ`G)"
shows "set (Ref ρ`G ws) = ρ`(set ws)"
proof-
have "G ⊆ ⟨ρ`G⟩"
proof
fix x
assume "x ∈ G"
show "x ∈ ⟨ρ ` G⟩"
by (metis ‹x ∈ G› genset_sub image_subset_iff power_in primroot_expE)
qed
hence "ws ∈ lists ⟨ρ`G⟩"
using assms by blast
have "set (decompose (ρ`G) a) = {ρ a}" if "a ∈ set ws" for a
proof-
have "ρ a ∈ ρ`G"
using ‹a ∈ set ws› ‹ws ∈ lists (G - {ε})› by blast
have "(Dec (ρ`G) a) ∈ [ρ a]*"
using code.code_unique_dec[OF ‹code (ρ ` G)› sing_pow_lists concat_sing_pow, OF ‹ρ a ∈ ρ ` G›]
primroot_expE rootI by metis
from sing_pow_set'[OF this dec_nemp']
show "set (decompose (ρ`G) a) = {ρ a}"
using ‹a ∈ set ws› ‹ws ∈ lists ⟨ρ ` G⟩› ‹ws ∈ lists (G - {ε})› by blast
qed
have "(set`(decompose (ρ`G))`set ws) = {{ρ a} |a. a ∈ set ws}" (is "?L = ?R")
proof
show "?L ⊆ ?R"
using ‹⋀a. a ∈ set ws ⟹ set (Dec ρ ` G a) = {ρ a}› by blast
show "?R ⊆ ?L"
using ‹⋀a. a ∈ set ws ⟹ set (Dec ρ ` G a) = {ρ a}› by blast
qed
show ?thesis
using ref_set[OF ‹ws ∈ lists ⟨ρ`G⟩›]
Setcompr_eq_image ‹set ` decompose (ρ ` G) ` set ws = {{ρ a} |a. a ∈ set ws}› by (auto simp add: refine_def)
qed
section ‹Prefix code›
locale pref_code =
fixes 𝒞
assumes
emp_not_in: "ε ∉ 𝒞" and
pref_free: "u ∈ 𝒞 ⟹ v ∈ 𝒞 ⟹ u ≤p v ⟹ u = v"
begin
lemma nemp: "u ∈ 𝒞 ⟹ u ≠ ε"
using emp_not_in by force
lemma concat_pref_concat:
assumes "us ∈ lists 𝒞" "vs ∈ lists 𝒞" "concat us ≤p concat vs"
shows "us ≤p vs"
using assms proof (induction us vs rule: list_induct2')
case (4 x xs y ys)
from "4.prems"
have "x = y"
by (auto elim!: ruler_prefE intro: pref_free sym del: in_listsD)
with "4" show "x # xs ≤p y # ys"
by simp
qed (simp_all add: nemp)
lemma concat_pref_concat_conv:
assumes "us ∈ lists 𝒞" "vs ∈ lists 𝒞"
shows "concat us ≤p concat vs ⟷ us ≤p vs"
using concat_pref_concat[OF assms] pref_concat_pref..
sublocale code
by standard (simp_all add: pref_antisym concat_pref_concat)
lemmas is_code = is_code and
code = code_axioms
lemma dec_pref_unique:
"w ∈ ⟨𝒞⟩ ⟹ p ∈ ⟨𝒞⟩ ⟹ p ≤p w ⟹ Dec 𝒞 p ≤p Dec 𝒞 w"
using concat_pref_concat_conv[of "Dec 𝒞 p" "Dec 𝒞 w", THEN iffD1]
by simp
end
subsection ‹Suffix code›
locale suf_code = pref_code "(rev ` 𝒞)" for 𝒞
begin
thm dec_rev
code
sublocale code
using code_rev_code unfolding rev_rev_image_eq.
lemmas concat_suf_concat = concat_pref_concat[reversed] and
concat_suf_concat_conv = concat_pref_concat_conv[reversed] and
nemp = nemp[reversed] and
suf_free = pref_free[reversed] and
dec_suf_unique = dec_pref_unique[reversed]
thm is_code
code_axioms
code
end
section ‹Marked code›
locale marked_code =
fixes 𝒞
assumes
emp_not_in: "ε ∉ 𝒞" and
marked: "u ∈ 𝒞 ⟹ v ∈ 𝒞 ⟹ hd u = hd v ⟹ u = v"
begin
lemma nemp: "u ∈ 𝒞 ⟹ u ≠ ε"
using emp_not_in by blast
sublocale pref_code
by (unfold_locales) (simp_all add: emp_not_in marked nemp pref_hd_eq)
lemma marked_concat_lcp: "us ∈ lists 𝒞 ⟹ vs ∈ lists 𝒞 ⟹ concat (us ∧⇩p vs) = (concat us) ∧⇩p (concat vs)"
proof (induct us vs rule: list_induct2')
case (4 x xs y ys)
hence "x ∈ 𝒞" and "y ∈ 𝒞" and "xs ∈ lists 𝒞" and "ys ∈ lists 𝒞"
by simp_all
show ?case
proof (cases)
assume "x = y"
thus "concat (x # xs ∧⇩p y # ys) = concat (x # xs) ∧⇩p concat (y # ys)"
using "4.hyps"[OF ‹xs ∈ lists 𝒞› ‹ys ∈ lists 𝒞›] by (simp add: lcp_ext_left)
next
assume "x ≠ y"
with marked[OF ‹x ∈ 𝒞› ‹y ∈ 𝒞›] have "hd x ≠ hd y" by blast
hence "concat (x # xs) ∧⇩p concat (y # ys) = ε"
by (simp add: ‹x ∈ 𝒞› ‹y ∈ 𝒞› nemp lcp_distinct_hd)
moreover have "concat (x # xs ∧⇩p y # ys) = ε"
using ‹x ≠ y› by simp
ultimately show ?thesis by presburger
qed
qed simp_all
lemma hd_concat_hd: assumes "xs ∈ lists 𝒞" and "ys ∈ lists 𝒞" and "xs ≠ ε" and "ys ≠ ε" and
"hd (concat xs) = hd (concat ys)"
shows "hd xs = hd ys"
proof-
have "hd (hd xs) = hd (hd ys)"
using assms hd_concat[OF ‹xs ≠ ε› lists_hd_in_set[THEN nemp]] hd_concat[OF ‹ys ≠ ε› lists_hd_in_set[THEN nemp]]
by presburger
from marked[OF lists_hd_in_set lists_hd_in_set this] assms(1-4)
show "hd xs = hd ys"
by simp
qed
end
section "Non-overlapping code"
locale non_overlapping =
fixes 𝒞
assumes
emp_not_in: "ε ∉ 𝒞" and
no_overlap: "u ∈ 𝒞 ⟹ v ∈ 𝒞 ⟹ z ≤p u ⟹ z ≤s v ⟹ z ≠ ε ⟹ u = v" and
no_fac: "u ∈ 𝒞 ⟹ v ∈ 𝒞 ⟹ u ≤f v ⟹ u = v"
begin
lemma nemp: "u ∈ 𝒞 ⟹ u ≠ ε"
using emp_not_in by force
sublocale pref_code
using nemp non_overlapping.no_fac non_overlapping_axioms pref_code.intro by fastforce
lemma rev_non_overlapping: "non_overlapping (rev ` 𝒞)"
proof
show "ε ∉ rev ` 𝒞"
using nemp by force
show "u ∈ rev ` 𝒞 ⟹ v ∈ rev ` 𝒞 ⟹ z ≤p u ⟹ z ≤s v ⟹ z ≠ ε ⟹ u = v" for u v z
using no_overlap[reversed] unfolding rev_in_conv..
show "u ∈ rev ` 𝒞 ⟹ v ∈ rev ` 𝒞 ⟹ u ≤f v ⟹ u = v" for u v
using no_fac[reversed] unfolding rev_in_conv by presburger
qed
sublocale suf: suf_code 𝒞
proof-
interpret i: non_overlapping "rev ` 𝒞"
using rev_non_overlapping.
from i.pref_code_axioms
show "suf_code 𝒞"
by unfold_locales
qed
lemma overlap_concat_last: assumes "u ∈ 𝒞" and "vs ∈ lists 𝒞" and "vs ≠ ε" and
"r ≠ ε" and "r ≤p u" and "r ≤s p ⋅ concat vs"
shows "u = last vs"
proof-
from suffix_same_cases[OF suf_ext[OF concat_last_suf[OF ‹vs ≠ ε›]] ‹r ≤s p ⋅ concat vs›]
show "u = last vs"
proof (rule disjE)
assume "r ≤s last vs"
from no_overlap[OF ‹u ∈ 𝒞› _ ‹r ≤p u› this ‹r ≠ ε›]
show "u = last vs"
using ‹vs ∈ lists 𝒞› ‹vs ≠ ε› by force
next
assume "last vs ≤s r"
from no_fac[OF _ ‹u ∈ 𝒞› pref_suf_fac, OF _ ‹r ≤p u› this]
show "u = last vs"
using ‹vs ∈ lists 𝒞› ‹vs ≠ ε› by force
qed
qed
lemma overlap_concat_hd: assumes "u ∈ 𝒞" and "vs ∈ lists 𝒞" and "vs ≠ ε" and "r ≠ ε" and "r ≤s u" and "r ≤p concat vs ⋅ s"
shows "u = hd vs"
proof-
interpret c: non_overlapping "rev ` 𝒞" by (simp add: rev_non_overlapping)
from c.overlap_concat_last[reversed, OF assms]
show ?thesis.
qed
lemma fac_concat_fac:
assumes "us ∈ lists 𝒞" "vs ∈ lists 𝒞"
and "1 < card (set us)"
and "concat vs = p ⋅ concat us ⋅ s"
obtains ps ss where "concat ps = p" and "concat ss = s" and "ps ⋅ us ⋅ ss = vs"
proof-
define us1 where "us1 = takeWhile (λ a. a = hd us) us"
define us2 where "us2 = dropWhile (λ a. a = hd us) us"
from card_set_decompose[OF ‹1 < card (set us)›]
have "us = us1 ⋅ us2" "us1 ≠ ε" "us2 ≠ ε" "set us1 = {hd us}" "last us1 ≠ hd us2"
unfolding us1_def us2_def by simp_all
have "us2 ∈ lists 𝒞" "us1 ∈ lists 𝒞"
using ‹us = us1 ⋅ us2› ‹us ∈ lists 𝒞› by simp_all
hence "concat us2 ≠ ε"
using ‹us2 ≠ ε› nemp by force
hence "p ⋅ concat us1 <p concat vs"
using ‹us = us1 ⋅ us2› unfolding ‹concat vs = p ⋅ concat us ⋅ s› by simp
from pref_mod_list[OF this]
obtain j r where "j < ❙|vs❙|" "r <p vs ! j" "concat (take j vs) ⋅ r = p ⋅ concat us1".
have "r = ε"
proof (rule ccontr)
assume "r ≠ ε"
from spref_exE[OF ‹r <p vs ! j›]
obtain z where "r ⋅ z = vs ! j" "z ≠ ε".
from overlap_concat_last[OF _ ‹us1 ∈ lists 𝒞› ‹us1 ≠ ε› ‹r ≠ ε› sprefD1[OF ‹r <p vs ! j›] sufI[OF ‹concat (take j vs) ⋅ r = p ⋅ concat us1›]]
have "vs ! j = last us1"
using nth_in_lists[OF ‹j < ❙|vs❙|› ‹vs ∈ lists 𝒞›].
have concat_vs: "concat vs = concat (take j vs) ⋅ vs!j ⋅ concat (drop (Suc j) vs)"
unfolding lassoc concat_take_Suc[OF ‹j < ❙|vs❙|›] concat_morph[symmetric] by force
from this[folded ‹r ⋅ z = vs ! j›]
have "z ⋅ concat (drop (Suc j) vs) = concat us2 ⋅ s"
unfolding ‹concat vs = p ⋅ concat us ⋅ s› lassoc ‹concat (take j vs) ⋅ r = p ⋅ concat us1› ‹us = us1 ⋅ us2› concat_morph
unfolding rassoc cancel by simp
from overlap_concat_hd[OF _ ‹us2 ∈ lists 𝒞› ‹us2 ≠ ε› ‹z ≠ ε› sufI[OF ‹r ⋅ z = vs ! j›] prefI[OF this]]
have "vs ! j = hd us2"
using nth_in_lists[OF ‹j < ❙|vs❙|› ‹vs ∈ lists 𝒞›].
thus False
unfolding ‹vs ! j = last us1› using ‹last us1 ≠ hd us2› by contradiction
qed
have "drop j vs ∈ lists 𝒞" and "take j vs ∈ lists 𝒞"
using ‹vs ∈ lists 𝒞› by inlists
have "concat us2 ⋅ s = concat (drop j vs)"
using arg_cong[OF takedrop[of j vs], of concat] ‹concat (take j vs) ⋅ r = p ⋅ concat us1›
unfolding ‹concat vs = p ⋅ concat us ⋅ s› concat_morph ‹r = ε› emp_simps ‹us = us1 ⋅ us2› by auto
from prefI[OF this]
have "us2 ≤p drop j vs"
using concat_pref_concat_conv[OF ‹us2 ∈ lists 𝒞› ‹drop j vs ∈ lists 𝒞›] by blast
hence s: "concat (us2¯⇧>drop j vs) = s"
using ‹concat us2 ⋅ s = concat (drop j vs)› concat_morph_lq lqI by blast
from ‹concat (take j vs) ⋅ r = p ⋅ concat us1›[unfolded ‹r = ε› emp_simps]
have "concat us1 ≤s concat (take j vs)"
by fastforce
hence "us1 ≤s take j vs"
using suf.concat_pref_concat_conv[reversed, OF ‹us1 ∈ lists 𝒞› ‹take j vs ∈ lists 𝒞›] by blast
from arg_cong[OF rq_suf[OF this], of concat, unfolded concat_morph]
have p: "concat (take j vs⇧<¯us1 ) = p"
using rqI[OF ‹concat (take j vs) = p ⋅ concat us1›[symmetric]]
rq_triv by metis
have "take j vs⇧<¯us1 ⋅ us ⋅ us2¯⇧>drop j vs = vs"
unfolding ‹us = us1 ⋅ us2› rassoc lq_pref[OF ‹us2 ≤p drop j vs›]
unfolding lassoc rq_suf[OF ‹us1 ≤s take j vs›] by simp
from that[OF p s this]
show thesis.
qed
theorem prim_morph:
assumes "ws ∈ lists 𝒞"
and "❙|ws❙| ≠ 1"
and "primitive ws"
shows "primitive (concat ws)"
proof (rule ccontr)
have "ws ∈ lists 𝒞" and "ws ⋅ ws ∈ lists 𝒞"
using ‹ws ∈ lists 𝒞› by simp_all
moreover have "1 < card (set ws)" using ‹primitive ws› ‹❙|ws❙| ≠ 1›
by (rule prim_card_set)
moreover assume "¬ primitive (concat ws)"
then obtain k z where "2 ≤ k" and "z ⇧@ k = concat ws" by (elim not_prim_primroot_expE)
have "concat (ws ⋅ ws) = z ⋅ concat ws ⋅ z⇧@(k-1)"
unfolding concat_morph ‹z ⇧@ k = concat ws›[symmetric] add_exps[symmetric] pow_Suc[symmetric]
using ‹2 ≤ k› by simp
ultimately obtain ps ss where "concat ps = z" and "concat ss = z⇧@(k-1)" and "ps ⋅ ws ⋅ ss = ws ⋅ ws"
by (rule fac_concat_fac)
have "ps ⇧@ k ∈ lists 𝒞"
using ‹ps ⋅ ws ⋅ ss = ws ⋅ ws› ‹ws ⋅ ws ∈ lists 𝒞› by inlists
moreover have "concat (ps ⇧@ k) = concat ws"
unfolding concat_pow ‹concat ps = z› ‹z ⇧@ k = concat ws›..
ultimately have "ps ⇧@ k = ws" using ‹ws ∈ lists 𝒞› by (intro is_code)
show False
using prim_exp_one[OF ‹primitive ws› ‹ps ⇧@ k = ws›] ‹2 ≤ k› by presburger
qed
lemma prim_concat_conv:
assumes "ws ∈ lists 𝒞"
and "❙|ws❙| ≠ 1"
shows "primitive (concat ws) ⟷ primitive ws"
using prim_concat_prim prim_morph[OF assms]..
end
lemma (in code) code_roots_non_overlapping: "non_overlapping ((λ x. [ρ x]⇧@(e⇩ρ x)) ` 𝒞)"
proof
show "ε ∉ (λx. [ρ x] ⇧@ e⇩ρ x) ` 𝒞"
proof
assume "ε ∈ (λx. [ρ x] ⇧@ e⇩ρ x) ` 𝒞 "
from this[unfolded image_iff]
obtain u where "u ∈ 𝒞" and "ε = [ρ u] ⇧@ e⇩ρ u"
by blast
from arg_cong[OF this(2), of concat]
show False
unfolding concat.simps(1) concat_sing_pow primroot_exp_eq
using emp_not_in ‹u ∈ 𝒞› by blast
qed
fix us vs
assume us': "us ∈ (λx. [ρ x] ⇧@ e⇩ρ x) ` 𝒞" and vs': "vs ∈ (λx. [ρ x] ⇧@ e⇩ρ x) ` 𝒞"
from us'[unfolded image_iff]
obtain u where "u ∈ 𝒞" and us: "us = [ρ u] ⇧@ e⇩ρ u"
by blast
from vs'[unfolded image_iff]
obtain v where "v ∈ 𝒞" and vs: "vs = [ρ v] ⇧@ e⇩ρ v"
by blast
note sing_set = sing_pow_set[OF primroot_exp_nemp[OF nemp]]
show "us = vs" if "zs ≤p us" and "zs ≤s vs" and "zs ≠ ε" for zs
proof-
from set_mono_prefix[OF ‹zs ≤p us›] ‹zs ≠ ε›[folded set_empty2]
have "set zs = {ρ u}"
using subset_singletonD unfolding ‹us = [ρ u] ⇧@ e⇩ρ u› sing_set[OF ‹u ∈ 𝒞›]
by metis
from set_mono_suffix[OF ‹zs ≤s vs›] ‹zs ≠ ε›[folded set_empty2]
have "set zs = {ρ v}"
using subset_singletonD unfolding ‹vs = [ρ v] ⇧@ e⇩ρ v› sing_set[OF ‹v ∈ 𝒞›]
by metis
hence "ρ u = ρ v"
unfolding ‹set zs = {ρ u}› by simp
from same_primroots_comm[OF this]
have "u = v"
using code_not_comm [OF ‹u ∈ 𝒞› ‹v ∈ 𝒞›] by blast
thus "us = vs"
unfolding ‹us = [ρ u] ⇧@ e⇩ρ u› ‹vs = [ρ v] ⇧@ e⇩ρ v› by blast
qed
show "us = vs" if "us ≤f vs"
proof-
from sing_set[OF ‹u ∈ 𝒞›, of "ρ u"] sing_set[OF ‹v ∈ 𝒞›, of "ρ v"]
have "ρ u = ρ v"
unfolding us[symmetric] vs[symmetric] using set_mono_sublist[OF ‹us ≤f vs›]
by force
from same_primroots_comm[OF this]
have "u = v"
using code_not_comm [OF ‹u ∈ 𝒞› ‹v ∈ 𝒞›] by blast
thus "us = vs"
unfolding ‹us = [ρ u] ⇧@ e⇩ρ u› ‹vs = [ρ v] ⇧@ e⇩ρ v› by blast
qed
qed
theorem (in code) roots_prim_morph:
assumes "ws ∈ lists 𝒞"
and "❙|ws❙| ≠ 1"
and "primitive ws"
shows "primitive (concat (map (λ x. [ρ x]⇧@(e⇩ρ x)) ws))"
(is "primitive (concat (map ?R ws))")
proof-
interpret rc: non_overlapping "?R ` 𝒞"
using code_roots_non_overlapping.
show ?thesis
proof (rule rc.prim_morph)
show "primitive (map ?R ws)"
using inj_map_prim[OF root_dec_inj_on
‹ws ∈ lists 𝒞› ‹primitive ws›].
show "map ?R ws ∈ lists (?R ` 𝒞)"
using ‹ws ∈ lists 𝒞› lists_image[of ?R 𝒞] by force
show "❙|map (λx. [ρ x] ⇧@ e⇩ρ x) ws❙| ≠ 1"
using ‹❙|ws❙| ≠ 1› by simp
qed
qed
section ‹Binary code›
text‹We pay a special attention to two element codes.
In particular, we show that two words form a code if and only if they do not commute. This means that two
words either commute, or do not satisfy any nontrivial relation.
›
definition bin_lcp where "bin_lcp x y = x⋅y ∧⇩p y⋅x"
definition bin_lcs where "bin_lcs x y = x⋅y ∧⇩s y⋅x"
definition bin_mismatch where "bin_mismatch x y = (x⋅y)!❙|bin_lcp x y❙|"
definition bin_mismatch_suf where " bin_mismatch_suf x y = bin_mismatch (rev y) (rev x)"
value[nbe] "[0::nat,1,0]!3"
lemma bin_lcs_rev: "bin_lcs x y = rev (bin_lcp (rev x) (rev y))"
unfolding bin_lcp_def bin_lcs_def longest_common_suffix_def rev_append using lcp_sym by fastforce
lemma bin_lcp_sym: "bin_lcp x y = bin_lcp y x"
unfolding bin_lcp_def using lcp_sym.
lemma bin_mismatch_comm: "(bin_mismatch x y = bin_mismatch y x) ⟷ (x ⋅ y = y ⋅ x)"
unfolding bin_mismatch_def bin_lcp_def lcp_sym[of "y ⋅ x"]
using lcp_mismatch'[of "x ⋅ y" "y ⋅ x", unfolded comm_comp_eq_conv[of x y]] by fastforce
lemma bin_lcp_pref_fst_snd: "bin_lcp x y ≤p x ⋅ y"
unfolding bin_lcp_def using lcp_pref.
lemma bin_lcp_pref_snd_fst: "bin_lcp x y ≤p y ⋅ x"
using bin_lcp_pref_fst_snd[of y x, unfolded bin_lcp_sym[of y x]].
lemma bin_lcp_bin_lcs [reversal_rule]: "bin_lcp (rev x) (rev y) = rev (bin_lcs x y)"
unfolding bin_lcp_def bin_lcs_def rev_append[symmetric] lcs_lcp
lcs_sym[of "x ⋅ y"]..
lemmas bin_lcs_sym = bin_lcp_sym[reversed]
lemma bin_lcp_len: "x ⋅ y ≠ y ⋅ x ⟹ ❙|bin_lcp x y❙| < ❙|x ⋅ y❙|"
unfolding bin_lcp_def
using lcp_len' pref_comm_eq by blast
lemmas bin_lcs_len = bin_lcp_len[reversed]
lemma bin_mismatch_pref_suf'[reversal_rule]:
"bin_mismatch (rev y) (rev x) = bin_mismatch_suf x y"
unfolding bin_mismatch_suf_def..
subsection ‹Binary code locale›
locale binary_code =
fixes u⇩0 u⇩1
assumes non_comm: "u⇩0 ⋅ u⇩1 ≠ u⇩1 ⋅ u⇩0"
begin
text‹A crucial property of two element codes is the constant decoding delay given by the word $\alpha$,
which is a prefix of any generating word (sufficiently long), while the letter
immediately after this common prefix indicates the first element of the decomposition.
›
definition uu where "uu a = (if a then u⇩0 else u⇩1)"
lemma bin_code_set_bool: "{uu a,uu (¬ a)} = {u⇩0,u⇩1}"
by (induct a, unfold uu_def, simp_all add: insert_commute)
lemma bin_code_set_bool': "{uu a,uu (¬ a)} = {u⇩1,u⇩0}"
by (induct a, unfold uu_def, simp_all add: insert_commute)
lemma bin_code_swap: "binary_code u⇩1 u⇩0"
using binary_code.intro[OF non_comm[symmetric]].
lemma bin_code_bool: "binary_code (uu a) (uu (¬ a))"
unfolding uu_def by (induct a, simp_all add: bin_code_swap binary_code_axioms)
lemma bin_code_neq: "u⇩0 ≠ u⇩1"
using non_comm by auto
lemma bin_code_neq_bool: "uu a ≠ uu (¬ a)"
unfolding uu_def by (induct a) (use bin_code_neq in fastforce)+
lemma bin_fst_nemp: "u⇩0 ≠ ε" and bin_snd_nemp: "u⇩1 ≠ ε" and bin_nemp_bool: "uu a ≠ ε"
using non_comm uu_def by auto
lemma bin_not_comp: "¬ u⇩0 ⋅ u⇩1 ⨝ u⇩1 ⋅ u⇩0"
using comm_comp_eq_conv non_comm by blast
lemma bin_not_comp_bool: "¬ (uu a ⋅ uu (¬ a) ⨝ uu (¬ a) ⋅ uu a)"
unfolding uu_def by (induct a, use bin_not_comp pref_comp_sym in auto)
lemma bin_not_comp_suf: "¬ u⇩0 ⋅ u⇩1 ⨝⇩s u⇩1 ⋅ u⇩0"
using comm_comp_eq_conv_suf non_comm[reversed] by blast
lemma bin_not_comp_suf_bool: "¬ (uu a ⋅ uu (¬ a) ⨝⇩s uu (¬ a) ⋅ uu a)"
unfolding uu_def by (induct a, use bin_not_comp_suf suf_comp_sym in auto)
lemma bin_mismatch_neq: "bin_mismatch u⇩0 u⇩1 ≠ bin_mismatch u⇩1 u⇩0"
using non_comm[folded bin_mismatch_comm].
abbreviation bin_code_lcp (‹α›) where "bin_code_lcp ≡ bin_lcp u⇩0 u⇩1"
abbreviation bin_code_lcs where "bin_code_lcs ≡ bin_lcs u⇩0 u⇩1"
abbreviation bin_code_mismatch_fst (‹c⇩0›) where "bin_code_mismatch_fst ≡ bin_mismatch u⇩0 u⇩1"
abbreviation bin_code_mismatch_snd (‹c⇩1›) where "bin_code_mismatch_snd ≡ bin_mismatch u⇩1 u⇩0"
definition cc where "cc a = (if a then c⇩0 else c⇩1)"
lemmas bin_lcp_swap = bin_lcp_sym[of u⇩0 u⇩1, symmetric] and
bin_lcp_pref = bin_lcp_pref_fst_snd[of u⇩0 u⇩1] and
bin_lcp_pref' = bin_lcp_pref_snd_fst[of u⇩0 u⇩1] and
bin_lcp_short = bin_lcp_len[OF non_comm, unfolded lenmorph]
lemmas bin_code_simps = cc_def uu_def if_True if_False bool_simps
lemma bin_lcp_bool: "bin_lcp (uu a) (uu (¬ a)) = bin_code_lcp"
unfolding uu_def by (induct a, simp_all add: bin_lcp_swap)
lemma bin_lcp_spref: "α <p u⇩0 ⋅ u⇩1"
using bin_lcp_pref bin_lcp_pref' bin_not_comp by fastforce
lemma bin_lcp_spref': "α <p u⇩1 ⋅ u⇩0"
using bin_lcp_pref bin_lcp_pref' bin_not_comp by fastforce
lemma bin_lcp_spref_bool: "α <p uu a ⋅ uu (¬ a)"
unfolding uu_def by (induct a, use bin_lcp_spref bin_lcp_spref' in auto)
lemma bin_mismatch_bool': "α ⋅ [cc a] ≤p uu a ⋅ uu (¬ a)"
using add_nth_pref[OF bin_lcp_spref_bool, of a]
unfolding uu_def cc_def bin_mismatch_def bin_lcp_bool bin_lcp_swap
by (induct a) simp_all
lemma bin_mismatch_bool: "α ⋅ [cc a] ≤p uu a ⋅ α"
proof-
from bin_mismatch_bool'
have "α ⋅ [cc a] ≤p uu a ⋅ (uu (¬ a) ⋅ uu a)"
using pref_prolong by blast
from pref_prod_pref_short[OF this bin_lcp_pref_snd_fst, unfolded bin_lcp_bool lenmorph sing_len]
show ?thesis
using nemp_len[OF bin_nemp_bool, of a] by linarith
qed
lemmas bin_fst_mismatch = bin_mismatch_bool[of True, unfolded bin_code_simps] and
bin_fst_mismatch' = bin_mismatch_bool'[of True, unfolded bin_code_simps] and
bin_snd_mismatch = bin_mismatch_bool[of False, unfolded bin_code_simps] and
bin_snd_mismatch' = bin_mismatch_bool'[of False, unfolded bin_code_simps]
lemma bin_lcp_pref_all: "xs ∈ lists {u⇩0,u⇩1} ⟹ α ≤p concat xs ⋅ α"
proof (induct xs)
case (Cons a xs)
have "a ∈ {u⇩0,u⇩1}" and "xs ∈ lists {u⇩0, u⇩1}"
using ‹a # xs ∈ lists {u⇩0, u⇩1}› by simp_all
show ?case
proof (rule two_elemP[OF ‹a ∈ {u⇩0,u⇩1}›], simp_all)
show "α ≤p u⇩0 ⋅ concat xs ⋅ α"
using pref_extD[OF bin_fst_mismatch] Cons.hyps[OF ‹xs ∈ lists {u⇩0, u⇩1}›] pref_prolong by blast
next
show "α ≤p u⇩1 ⋅ concat xs ⋅ α"
using pref_extD[OF bin_snd_mismatch] Cons.hyps[OF ‹xs ∈ lists {u⇩0, u⇩1}›] pref_prolong by blast
qed
qed simp
lemma bin_lcp_pref_all_hull: "w ∈ ⟨{u⇩0,u⇩1}⟩ ⟹ α ≤p w ⋅ α"
using bin_lcp_pref_all using hull_concat_listsE by metis
lemma bin_lcp_mismatch_pref_all_bool: assumes "q ≤p w" and "w ∈ ⟨{uu b,uu (¬ b)}⟩" and "❙|α❙| < ❙|uu a ⋅ q❙|"
shows "α ⋅ [cc a] ≤p uu a ⋅ q"
proof-
have aux: "uu a ⋅ w ⋅ α = (uu a ⋅ q) ⋅ (q¯⇧>w ⋅ α)" "{uu b,uu (¬ b)} = {u⇩0,u⇩1}"
using lq_pref[OF ‹q ≤p w›] bin_code_set_bool by force+
have "❙|α ⋅ [cc a]❙| ≤ ❙|uu a ⋅ q❙|"
using ‹❙|α❙| < ❙|uu a ⋅ q❙|› by auto
thus ?thesis
using pref_prolong[OF bin_mismatch_bool bin_lcp_pref_all_hull[OF ‹w ∈ ⟨{uu b,uu (¬ b)}⟩›[unfolded aux]], of a]
unfolding aux by blast
qed
lemmas bin_lcp_mismatch_pref_all_fst = bin_lcp_mismatch_pref_all_bool[of _ _ True True, unfolded bin_code_simps] and
bin_lcp_mismatch_pref_all_snd = bin_lcp_mismatch_pref_all_bool[of _ _ True False, unfolded bin_code_simps]
lemma bin_lcp_pref_all_len: assumes "q ≤p w" and "w ∈ ⟨{u⇩0,u⇩1}⟩" and "❙|α❙| ≤ ❙|q❙|"
shows "α ≤p q"
using bin_lcp_pref_all_hull[OF ‹w ∈ ⟨{u⇩0,u⇩1}⟩›] pref_ext[OF ‹q ≤p w›] prefix_length_prefix[OF _ _ ‹❙|bin_code_lcp❙| ≤ ❙|q❙|›] by blast
lemma bin_mismatch_all_bool: assumes "xs ∈ lists {uu b, uu (¬ b)}" shows "α ⋅ [cc a] ≤p (uu a) ⋅ concat xs ⋅ α"
using pref_prolong[OF bin_mismatch_bool bin_lcp_pref_all, of xs a] assms unfolding bin_code_set_bool[of b].
lemmas bin_fst_mismatch_all = bin_mismatch_all_bool[of _ True True, unfolded bin_code_simps] and
bin_snd_mismatch_all = bin_mismatch_all_bool[of _ True False, unfolded bin_code_simps]
lemma bin_mismatch_all_hull_bool: assumes "w ∈ ⟨{uu b,uu (¬ b)}⟩" shows "α ⋅ [cc a] ≤p uu a ⋅ w ⋅ α"
using bin_mismatch_all_bool hull_concat_listsE[OF assms] by metis
lemmas bin_fst_mismatch_all_hull = bin_mismatch_all_hull_bool[of _ True True, unfolded bin_code_simps] and
bin_snd_mismatch_all_hull = bin_mismatch_all_hull_bool[of _ True False, unfolded bin_code_simps]
lemma bin_mismatch_all_len_bool: assumes "q ≤p uu a ⋅ w" and "w ∈ ⟨{uu b,uu (¬ b)}⟩" and "❙|α❙| < ❙|q❙|"
shows "α ⋅ [cc a] ≤p q"
proof-
have "❙|α ⋅ [cc a]❙| ≤ ❙|uu a ⋅ w❙|" "❙|α ⋅ [cc a]❙| ≤ ❙|q❙|"
using less_le_trans[OF ‹❙|α❙| < ❙|q❙|› pref_len[OF ‹q ≤p uu a ⋅ w›]] ‹❙|α❙| < ❙|q❙|› by force+
from pref_prod_le[OF bin_mismatch_all_hull_bool[OF assms(2), unfolded lassoc], OF this(1)]
show ?thesis
by (rule prefix_length_prefix) fact+
qed
lemmas bin_fst_mismatch_all_len = bin_mismatch_all_len_bool[of _ True _ True, unfolded bin_code_simps] and
bin_snd_mismatch_all_len = bin_mismatch_all_len_bool[of _ False _ True, unfolded bin_code_simps]
lemma bin_code_delay: assumes "❙|α❙| ≤ ❙|q⇩0❙|" and "❙|α❙| ≤ ❙|q⇩1❙|" and
"q⇩0 ≤p u⇩0 ⋅ w⇩0" and "q⇩1 ≤p u⇩1 ⋅ w⇩1" and
"w⇩0 ∈ ⟨{u⇩0, u⇩1}⟩" and "w⇩1 ∈ ⟨{u⇩0, u⇩1}⟩"
shows "q⇩0 ∧⇩p q⇩1 = α"
proof-
have p1: "α ⋅ [c⇩0] ≤p u⇩0 ⋅ w⇩0 ⋅ α"
using assms(5) using bin_fst_mismatch_all_hull by auto
have p2: "α ⋅ [c⇩1] ≤p u⇩1 ⋅ w⇩1 ⋅ α"
using assms(6) using bin_snd_mismatch_all_hull by auto
have lcp: "u⇩0 ⋅ w⇩0 ⋅ α ∧⇩p u⇩1 ⋅ w⇩1 ⋅ α = α"
using lcp_first_mismatch_pref[OF p1 p2 bin_mismatch_neq].
from lcp_extend_eq[of "q⇩0" "u⇩0 ⋅ w⇩0 ⋅ α" "q⇩1" "u⇩1 ⋅ w⇩1 ⋅ α",
unfolded this,OF _ _ assms(1-2)]
show ?thesis
using pref_ext[OF ‹q⇩0 ≤p u⇩0 ⋅ w⇩0›] pref_ext[OF ‹q⇩1 ≤p u⇩1 ⋅ w⇩1›] by force
qed
lemma hd_lq_mismatch_fst: "hd (α¯⇧>(u⇩0 ⋅ α)) = c⇩0"
using hd_lq_conv_nth[OF prefix_snocD[OF bin_fst_mismatch]] bin_fst_mismatch
by (auto simp add: prefix_def)
lemma hd_lq_mismatch_snd: "hd (α¯⇧>(u⇩1 ⋅ α)) = c⇩1"
using hd_lq_conv_nth[OF prefix_snocD[OF bin_snd_mismatch]] bin_snd_mismatch
by (auto simp add: prefix_def)
lemma hds_bin_mismatch_neq: "hd (α¯⇧>(u⇩0 ⋅ α)) ≠ hd (α¯⇧>(u⇩1 ⋅ α))"
unfolding hd_lq_mismatch_fst hd_lq_mismatch_snd
using bin_mismatch_neq.
lemma bin_lcp_fst_pow_pref: assumes "0 < k" shows "α ⋅ [c⇩0] ≤p u⇩0⇧@k ⋅ u⇩1 ⋅ z"
using assms
proof (induct k rule: nat_induct_non_zero)
case 1
then show ?case
unfolding pow_1 using pref_prolong[OF bin_fst_mismatch' triv_pref].
next
case (Suc n)
show ?case
unfolding pow_Suc rassoc
by (rule pref_prolong[OF bin_fst_mismatch])
(use append_prefixD[OF Suc.hyps(2)] in blast)
qed
lemmas bin_lcp_snd_pow_pref = binary_code.bin_lcp_fst_pow_pref[OF bin_code_swap, unfolded bin_lcp_swap]
lemma bin_lcp_fst_lcp: "α ≤p u⇩0 ⋅ α" and bin_lcp_snd_lcp: "α ≤p u⇩1 ⋅ α"
using pref_extD[OF bin_fst_mismatch] pref_extD[OF bin_snd_mismatch].
lemma bin_lcp_pref_all_set: assumes "set ws = {u⇩0,u⇩1}"
shows "α ≤p concat ws"
proof-
have "ws ∈ lists {u⇩0, u⇩1}"
using assms by blast
have "❙|u⇩0❙| + ❙|u⇩1❙| ≤ ❙|concat ws❙|"
using assms two_in_set_concat_len[OF bin_code_neq] by simp
with pref_prod_le[OF bin_lcp_pref_all[OF ‹ws ∈ lists {u⇩0, u⇩1}›]] bin_lcp_short
show ?thesis
by simp
qed
lemma bin_lcp_conjug_morph:
assumes "u ∈ ⟨{u⇩0,u⇩1}⟩" and "v ∈ ⟨{u⇩0,u⇩1}⟩"
shows "α¯⇧>(u ⋅ α) ⋅ α¯⇧>(v ⋅ α) = α¯⇧>((u ⋅ v) ⋅ α)"
unfolding lq_reassoc[OF bin_lcp_pref_all_hull[OF ‹u ∈ ⟨{u⇩0,u⇩1}⟩›]] rassoc
lq_pref[OF bin_lcp_pref_all_hull[OF ‹v ∈ ⟨{u⇩0,u⇩1}⟩›]]..
lemma lcp_bin_conjug_prim_iff:
"set ws = {u⇩0,u⇩1} ⟹ primitive (α¯⇧>(concat ws) ⋅ α) ⟷ primitive (concat ws)"
using conjug_prim_iff[OF root_conjug[OF pref_ext[OF bin_lcp_pref_all_set]], symmetric]
unfolding lq_reassoc[OF bin_lcp_pref_all_set] by simp
lemma bin_lcp_conjug_inj_on: "inj_on (λu. α¯⇧>(u ⋅ α)) ⟨{u⇩0,u⇩1}⟩"
unfolding inj_on_def using bin_lcp_pref_all_hull cancel_right lq_pref
by metis
lemma bin_code_lcp_marked: assumes "us ∈ lists {u⇩0,u⇩1}" and "vs ∈ lists {u⇩0,u⇩1}" and "hd us ≠ hd vs"
shows "concat us ⋅ α ∧⇩p concat vs ⋅ α = α"
proof (cases "us = ε ∨ vs = ε")
assume "us = ε ∨ vs = ε"
thus ?thesis
using append_self_conv2 assms(1) assms(2) bin_lcp_pref_all concat.simps(1) lcp_pref_conv lcp_sym by metis
next
assume "¬ (us = ε ∨ vs = ε)" hence "us ≠ ε" and "vs ≠ ε" by blast+
have spec_case: "concat us ⋅ α ∧⇩p concat vs ⋅ α = α" if "us ∈ lists {u⇩0,u⇩1}" and "vs ∈ lists {u⇩0,u⇩1}" and "hd us = u⇩0" and "hd vs = u⇩1" and "us ≠ ε" and "vs ≠ ε" for us vs
proof-
have "concat us = u⇩0 ⋅ concat (tl us)"
unfolding hd_concat_tl[OF ‹us ≠ ε›, symmetric] ‹hd us = u⇩0›..
from bin_fst_mismatch_all[OF tl_in_lists[OF ‹us ∈ lists {u⇩0,u⇩1}›], folded rassoc this]
have pref1: "α ⋅ [c⇩0] ≤p concat us ⋅ α".
have "concat vs = u⇩1 ⋅ concat (tl vs)"
unfolding hd_concat_tl[OF ‹vs ≠ ε›, symmetric] ‹hd vs = u⇩1›..
from bin_snd_mismatch_all[OF tl_in_lists[OF ‹vs ∈ lists {u⇩0,u⇩1}›], folded rassoc this]
have pref2: "α ⋅ [c⇩1] ≤p concat vs ⋅ α".
show ?thesis
using lcp_first_mismatch_pref[OF pref1 pref2 bin_mismatch_neq].
qed
have "hd us ∈ {u⇩0,u⇩1}" and "hd vs ∈ {u⇩0,u⇩1}" using
lists_hd_in_set[OF ‹us ≠ ε› ‹us ∈ lists {u⇩0, u⇩1}›] lists_hd_in_set[OF ‹vs ≠ ε› ‹vs ∈ lists {u⇩0, u⇩1}›].
then consider "hd us = u⇩0 ∧ hd vs = u⇩1" | "hd us = u⇩1 ∧ hd vs = u⇩0"
using ‹hd us ≠ hd vs› by fastforce
then show ?thesis
using spec_case[rule_format] ‹us ≠ ε› ‹vs ≠ ε› assms lcp_sym by metis
qed
lemma assumes "us ∈ lists {u⇩0,u⇩1}" and "vs ∈ lists {u⇩0,u⇩1}" and "hd us ≠ hd vs"
shows "concat us ⋅ α ∧⇩p concat vs ⋅ α = α"
using assms
proof (induct us vs rule: list_induct2')
case (2 x xs)
show ?case
using bin_lcp_pref_all[OF ‹x # xs ∈ lists {u⇩0, u⇩1}›, folded lcp_pref_conv, unfolded lcp_sym[of α]] by simp
next
case (3 y ys)
show ?case
using bin_lcp_pref_all[OF ‹y # ys ∈ lists {u⇩0, u⇩1}›, folded lcp_pref_conv] by simp
next
case (4 x xs y ys)
interpret i: binary_code x y
using "4.prems"(1) "4.prems"(2) "4.prems"(3) non_comm binary_code.intro by auto
have alph: "{u⇩0,u⇩1} = {x,y}"
using "4.prems"(1) "4.prems"(2) "4.prems"(3) by auto
from disjE[OF this[unfolded doubleton_eq_iff]]
have "i.bin_code_lcp = α"
using i.bin_lcp_swap[symmetric] by blast
have c0: "i.bin_code_lcp ⋅ [i.bin_code_mismatch_fst] ≤p x ⋅ concat xs ⋅ i.bin_code_lcp"
using i.bin_lcp_pref_all[of xs] ‹x # xs ∈ lists {u⇩0, u⇩1}›[unfolded Cons_in_lists_iff alph]
pref_prolong[OF i.bin_fst_mismatch] by blast
have c1: "i.bin_code_lcp ⋅ [i.bin_code_mismatch_snd] ≤p y ⋅ concat ys ⋅ i.bin_code_lcp"
using pref_prolong[OF conjunct2[OF ‹y # ys ∈ lists {u⇩0, u⇩1}›[unfolded Cons_in_lists_iff alph],
THEN i.bin_snd_mismatch_all[of ys]], OF self_pref].
have "i.bin_code_lcp⋅[i.bin_code_mismatch_fst] ∧⇩p i.bin_code_lcp⋅[i.bin_code_mismatch_snd] = i.bin_code_lcp"
by (simp add: i.bin_mismatch_neq lcp_first_mismatch')
from lcp_rulers[OF c0 c1, unfolded this, unfolded bin_lcp_swap]
show ?case
unfolding concat.simps(2) rassoc using i.bin_mismatch_neq
‹i.bin_code_lcp = α› by force
qed simp
lemma bin_code_lcp_concat: assumes "us ∈ lists {u⇩0,u⇩1}" and "vs ∈ lists {u⇩0,u⇩1}" and "¬ us ⨝ vs"
shows "concat us ⋅ α ∧⇩p concat vs ⋅ α = concat (us ∧⇩p vs) ⋅ α"
proof-
obtain us' vs' where us: "(us ∧⇩p vs) ⋅ us' = us" and vs: "(us ∧⇩p vs) ⋅ vs' = vs" and "us' ≠ ε" and "vs' ≠ ε" and "hd us' ≠ hd vs'"
using lcp_mismatchE[OF ‹¬ us ⨝ vs›].
have cu: "concat us ⋅ α = concat (us ∧⇩p vs) ⋅ concat us' ⋅ α"
unfolding lassoc concat_morph[symmetric] us..
have cv: "concat vs ⋅ α = concat (us ∧⇩p vs) ⋅ concat vs' ⋅ α"
unfolding lassoc concat_morph[symmetric] vs..
have "us' ∈ lists {u⇩0,u⇩1}"
using ‹us ∈ lists {u⇩0,u⇩1}› us by inlists
have "vs' ∈ lists {u⇩0,u⇩1}"
using ‹vs ∈ lists {u⇩0,u⇩1}› vs by inlists
show "concat us ⋅ α ∧⇩p concat vs ⋅ α = concat (us ∧⇩p vs) ⋅ α"
unfolding cu cv
using bin_code_lcp_marked[OF ‹us' ∈ lists {u⇩0,u⇩1}› ‹vs' ∈ lists {u⇩0,u⇩1}› ‹hd us' ≠ hd vs'›]
unfolding lcp_ext_left by fast
qed
lemma bin_code_lcp_concat': assumes "us ∈ lists {u⇩0,u⇩1}" and "vs ∈ lists {u⇩0,u⇩1}" and "¬ concat us ⨝ concat vs"
shows "concat us ∧⇩p concat vs = concat (us ∧⇩p vs) ⋅ α"
using bin_code_lcp_concat[OF assms(1-2)] assms(3) lcp_ext_right_conv pref_concat_pref prefix_comparable_def by metis
lemma bin_lcp_pows: "0 < k ⟹ 0 < l ⟹ u⇩0⇧@k ⋅ u⇩1 ⋅ z ∧⇩p u⇩1⇧@l ⋅ u⇩0 ⋅ z' = α"
using lcp_first_mismatch_pref[OF bin_lcp_fst_pow_pref bin_lcp_snd_pow_pref bin_mismatch_neq].
theorem bin_code: assumes "us ∈ lists {u⇩0,u⇩1}" and "vs ∈ lists {u⇩0,u⇩1}" and "concat us = concat vs"
shows "us = vs"
using assms
proof (induct us vs rule: list_induct2')
case (4 x xs y ys)
then show ?case
proof-
have "x =y"
using bin_code_lcp_marked[OF ‹x # xs ∈ lists {u⇩0, u⇩1}› ‹y # ys ∈ lists {u⇩0, u⇩1}›] ‹y # ys ∈ lists {u⇩0, u⇩1}› non_comm
unfolding ‹concat (x # xs) = concat (y # ys)› unfolding concat.simps(2) lcp_self list.sel(1)
by auto
thus "x # xs = y # ys"
using "4.hyps" ‹concat (x # xs) = concat (y # ys)›[unfolded concat.simps(2) ‹x = y›, unfolded cancel]
‹y # ys ∈ lists {u⇩0, u⇩1}›[unfolded Cons_in_lists_iff] ‹x # xs ∈ lists {u⇩0, u⇩1}›[unfolded Cons_in_lists_iff]
by simp
qed
qed (auto simp: bin_fst_nemp bin_snd_nemp)
lemma code_bin_roots: "binary_code (ρ u⇩0) (ρ u⇩1)"
using non_comm comp_primroot_conv' by unfold_locales blast
sublocale code "{u⇩0,u⇩1}"
using bin_code by unfold_locales
lemma primroot_dec: "(Dec {ρ u⇩0, ρ u⇩1} u⇩0) = [ρ u⇩0]⇧@e⇩ρ u⇩0" "(Dec {ρ u⇩0, ρ u⇩1} u⇩1) = [ρ u⇩1]⇧@e⇩ρ u⇩1"
proof-
interpret rs: binary_code "ρ u⇩0" "ρ u⇩1"
by (simp add: code_bin_roots)
from primroot_exp_eq
have "concat ([ρ u⇩0]⇧@e⇩ρ u⇩0) = u⇩0" "concat ([ρ u⇩1]⇧@e⇩ρ u⇩1) = u⇩1"
by force+
from rs.code_unique_dec[OF _ this(1)] rs.code_unique_dec[OF _ this(2)]
show "(Dec {ρ u⇩0, ρ u⇩1} u⇩0) = [ρ u⇩0]⇧@e⇩ρ u⇩0" "(Dec {ρ u⇩0, ρ u⇩1} u⇩1) = [ρ u⇩1]⇧@e⇩ρ u⇩1"
by (simp_all add: sing_pow_lists)
qed
lemma bin_code_prefs: assumes "w ∈ ⟨{u⇩0,u⇩1}⟩" and "p ≤p w" "w' ∈ ⟨{u⇩0,u⇩1}⟩" and "❙|u⇩1❙| ≤ ❙|p❙|"
shows " ¬ u⇩0 ⋅ p ≤p u⇩1 ⋅ w'"
proof
assume contr: "u⇩0 ⋅ p ≤p u⇩1 ⋅ w'"
have "❙|α❙| < ❙|u⇩0 ⋅ p❙|"
using ‹❙|u⇩1❙| ≤ ❙|p❙|› bin_lcp_short by auto
hence "α ⋅ [c⇩0] ≤p u⇩0 ⋅ p"
using ‹p ≤p w› ‹w ∈ ⟨{u⇩0,u⇩1}⟩› bin_lcp_mismatch_pref_all_fst by auto
from pref_ext[OF pref_trans[OF this contr], unfolded rassoc]
have "α ⋅ [c⇩0] ≤p u⇩1 ⋅ w' ⋅ α".
from bin_mismatch_neq same_sing_pref[OF bin_snd_mismatch_all_hull[OF ‹w' ∈ ⟨{u⇩0,u⇩1}⟩›] this]
show False
by simp
qed
lemma bin_code_rev: "binary_code (rev u⇩0) (rev u⇩1)"
by (unfold_locales, unfold comm_rev_iff, simp add: non_comm)
lemma bin_mismatch_pows: "¬ u⇩0⇧@Suc k ⋅ u⇩1 ⋅ z = u⇩1⇧@Suc l ⋅ u⇩0 ⋅ z'"
proof (rule notI)
assume eq: "u⇩0 ⇧@ Suc k ⋅ u⇩1 ⋅ z = u⇩1 ⇧@ Suc l ⋅ u⇩0 ⋅ z'"
have pref1: "α ⋅ [c⇩0] ≤p u⇩0⇧@Suc k ⋅ u⇩1" and pref2: "α ⋅ [c⇩1] ≤p u⇩1⇧@Suc l ⋅ u⇩0"
using bin_lcp_fst_pow_pref[of "Suc k" ε, unfolded emp_simps] bin_lcp_snd_pow_pref[of "Suc l" ε, unfolded emp_simps] by blast+
from ruler[OF pref_ext[OF pref1, unfolded rassoc, of z, unfolded eq] pref_ext[OF pref2, unfolded rassoc, of z', unfolded eq]] bin_mismatch_neq
show False by simp
qed
lemma bin_lcp_pows_lcp: "0 < k ⟹ 0 < l ⟹ u⇩0⇧@k ⋅ u⇩1⇧@l ∧⇩p u⇩1⇧@l ⋅ u⇩0⇧@k = u⇩0 ⋅ u⇩1 ∧⇩p u⇩1 ⋅ u⇩0"
using bin_lcp_pows unfolding bin_lcp_def using pow_pos by metis
lemma bin_mismatch: "u⇩0 ⋅ α ∧⇩p u⇩1 ⋅ α = α"
using lcp_first_mismatch_pref[OF bin_fst_mismatch bin_snd_mismatch bin_mismatch_neq].
lemma not_comp_bin_fst_snd: "¬ u⇩0 ⋅ α ⨝ u⇩1 ⋅ α"
using ruler_comp[OF bin_fst_mismatch bin_snd_mismatch] bin_mismatch_neq
unfolding prefix_comparable_def pref_cancel_conv by force
theorem bin_bounded_delay: assumes "z ≤p u⇩0 ⋅ w⇩0" and "z ≤p u⇩1 ⋅ w⇩1"
and "w⇩0 ∈ ⟨{u⇩0,u⇩1}⟩" and "w⇩1 ∈ ⟨{u⇩0,u⇩1}⟩"
shows "❙|z❙| ≤ ❙|α❙|"
proof (rule leI, rule notI)
assume "❙|α❙| < ❙|z❙|"
hence "❙|α ⋅ [a]❙| ≤ ❙|z❙|" for a
unfolding lenmorph sing_len by simp
have "z ≤p u⇩0 ⋅ w⇩0 ⋅ α" and "z ≤p u⇩1 ⋅ w⇩1 ⋅ α"
using pref_prolong[OF ‹z ≤p u⇩0 ⋅ w⇩0› triv_pref] pref_prolong[OF ‹z ≤p u⇩1 ⋅ w⇩1› triv_pref].
have "α ⋅ [c⇩0] ≤p u⇩0 ⋅ w⇩0 ⋅ α" and "α ⋅ [c⇩1] ≤p u⇩1 ⋅ w⇩1 ⋅ α"
using bin_fst_mismatch_all_hull[OF ‹w⇩0 ∈ ⟨{u⇩0,u⇩1}⟩›] bin_snd_mismatch_all_hull[OF ‹w⇩1 ∈ ⟨{u⇩0,u⇩1}⟩›].
from ‹z ≤p u⇩0 ⋅ w⇩0 ⋅ α› ‹α ⋅ [c⇩0] ≤p u⇩0 ⋅ w⇩0 ⋅ α› ‹❙|α ⋅ [c⇩0]❙| ≤ ❙|z❙|›
have "α ⋅ [c⇩0] ≤p z"
using prefix_length_prefix by blast
from ‹z ≤p u⇩1 ⋅ w⇩1 ⋅ α› ‹α ⋅ [c⇩1] ≤p u⇩1 ⋅ w⇩1 ⋅ α› ‹❙|α ⋅ [c⇩1]❙| ≤ ❙|z❙|›
have "α ⋅ [c⇩1] ≤p z"
using prefix_length_prefix by blast
from ‹α ⋅ [c⇩1] ≤p z› ‹α ⋅ [c⇩0] ≤p z› bin_mismatch_neq
show False
unfolding prefix_def by force
qed
thm binary_code.bin_lcp_pows_lcp
lemma prim_roots_lcp: "ρ u⇩0 ⋅ ρ u⇩1 ∧⇩p ρ u⇩1 ⋅ ρ u⇩0 = α"
proof-
obtain k where "ρ u⇩0⇧@k = u⇩0" "0 < k"
using primroot_expE.
obtain m where "ρ u⇩1⇧@m = u⇩1" "0 < m"
using primroot_expE.
have "ρ u⇩0 ⋅ ρ u⇩1 ≠ ρ u⇩1 ⋅ ρ u⇩0"
using non_comm[unfolded comp_primroot_conv'[of u⇩0]].
then interpret r: binary_code "ρ u⇩0" "ρ u⇩1" by unfold_locales
from r.bin_lcp_pows_lcp[OF ‹0 < k› ‹0 < m›, unfolded ‹ρ u⇩1⇧@m = u⇩1› ‹ρ u⇩0⇧@k = u⇩0›, symmetric]
show ?thesis
unfolding bin_lcp_def.
qed
subsubsection ‹Maximal r-prefixes›
lemma bin_lcp_per_root_max_pref_short: assumes "α <p u⇩0 ⋅ u⇩1 ∧⇩p r ⋅ u⇩0 ⋅ u⇩1" and "r ≠ ε" and "q ≤p w" and "w ∈ ⟨{u⇩0, u⇩1}⟩"
shows "u⇩1 ⋅ q ∧⇩p r ⋅ u⇩1 ⋅ q = take ❙|u⇩1 ⋅ q❙| α"
proof-
have "q ⨝ α"
using bin_lcp_pref_all_hull[OF ‹w ∈ ⟨{u⇩0, u⇩1}⟩›] ruler_comp[OF ‹q ≤p w›, of α "w ⋅ α"] by blast
hence comp1: "u⇩1 ⋅ q ⨝ α ⋅ [c⇩1]"
using ruler_comp[OF self_pref bin_snd_mismatch, of "u⇩1 ⋅ q"] unfolding comp_cancel by blast
from add_nth_pref[OF assms(1), THEN pref_lcp_pref] bin_fst_mismatch'
have "(u⇩0 ⋅ u⇩1 ∧⇩p r ⋅ u⇩0 ⋅ u⇩1) ! ❙|α❙| = c⇩0"
using same_sing_pref by fast
from add_nth_pref[OF assms(1), unfolded this]
have "α ⋅ [c⇩0] ≤p r ⋅ u⇩0 ⋅ u⇩1"
by force
have len: "❙|α ⋅ [c⇩0]❙| ≤ ❙|r ⋅ α❙|"
using nemp_pos_len[OF ‹r ≠ ε›] unfolding lenmorph sing_len by linarith
have comp2: "r ⋅ u⇩1 ⋅ q ⨝ α ⋅ [c⇩0]"
proof(rule ruler_comp[OF _ _ comp_refl])
show "r ⋅ u⇩1 ⋅ q ≤p r ⋅ u⇩1 ⋅ w ⋅ α"
using ‹q ≤p w› by fastforce
show "α ⋅ [c⇩0] ≤p r ⋅ u⇩1 ⋅ w ⋅ α"
proof(rule pref_prolong)
show "α ⋅ [c⇩0] ≤p r ⋅ α"
using ‹α ⋅ [c⇩0] ≤p r ⋅ u⇩0 ⋅ u⇩1› bin_lcp_pref len pref_prod_pref_short by blast
show "α ≤p u⇩1 ⋅ w ⋅ α"
using ‹w ∈ ⟨{u⇩0, u⇩1}⟩› bin_lcp_pref_all_hull[of "u⇩1 ⋅ w"] by auto
qed
qed
have min: "(min ❙|u⇩1 ⋅ q❙| ❙|r ⋅ u⇩1 ⋅ q❙|) = ❙|u⇩1 ⋅ q❙|"
unfolding lenmorph by simp
show ?thesis
using bin_mismatch_neq double_ruler[OF comp1 comp2,unfolded min]
by (simp add: lcp_mismatch_eq_len mismatch_incopm)
qed
lemma bin_per_root_max_pref_short: assumes "(u⇩0 ⋅ u⇩1) <p r ⋅ u⇩0 ⋅ u⇩1" and "q ≤p w" and "w ∈ ⟨{u⇩0, u⇩1}⟩"
shows "u⇩1 ⋅ q ∧⇩p r ⋅ u⇩1 ⋅ q = take ❙|u⇩1 ⋅ q❙| α"
proof (rule bin_lcp_per_root_max_pref_short[OF _ _ assms(2-3)])
show "α <p u⇩0 ⋅ u⇩1 ∧⇩p r ⋅ u⇩0 ⋅ u⇩1"
unfolding lcp.absorb3[OF assms(1)] using bin_fst_mismatch'[THEN prefix_snocD].
qed (use assms(1) in blast)
lemma bin_root_max_pref_long: assumes "r ⋅ u⇩0 ⋅ u⇩1 = u⇩0 ⋅ u⇩1 ⋅ r" and "q ≤p w" and "w ∈ ⟨{u⇩0, u⇩1}⟩" and "❙|α❙| ≤ ❙|q❙|"
shows "u⇩0 ⋅ α ≤p u⇩0 ⋅ q ∧⇩p r ⋅ u⇩0 ⋅ q"
proof (rule pref_pref_lcp)
have len: " ❙|u⇩0 ⋅ α❙| ≤ ❙|r ⋅ u⇩0 ⋅ α❙|"
by simp
from bin_lcp_pref_all_len[OF assms(2-4)]
show "u⇩0 ⋅ α ≤p u⇩0 ⋅ q"
unfolding pref_cancel_conv.
have "u⇩0 ⋅ α ≤p r ⋅ u⇩0 ⋅ α"
proof(rule ruler_le[OF _ _ len])
show "u⇩0 ⋅ α ≤p (r ⋅ u⇩0 ⋅ u⇩1) ⋅ u⇩0 ⋅ u⇩1"
unfolding assms(1) unfolding rassoc pref_cancel_conv assms(1)
using pref_ext[OF pref_ext[OF bin_lcp_pref'], unfolded rassoc].
show "r ⋅ u⇩0 ⋅ α ≤p (r ⋅ u⇩0 ⋅ u⇩1) ⋅ u⇩0 ⋅ u⇩1"
unfolding rassoc pref_cancel_conv using pref_ext[OF bin_lcp_pref', unfolded rassoc].
qed
from pref_prolong[OF this[unfolded lassoc], OF ‹α ≤p q›, unfolded rassoc]
show "u⇩0 ⋅ α ≤p r ⋅ u⇩0 ⋅ q".
qed
lemma per_root_lcp_per_root: "u⇩0 ⋅ u⇩1 <p r ⋅ u⇩0 ⋅ u⇩1 ⟹ α ⋅ [c⇩0] ≤p r ⋅ α"
using per_root_pref_sing[OF _ bin_fst_mismatch'].
lemma per_root_bin_fst_snd_lcp: assumes "u⇩0 ⋅ u⇩1 <p r ⋅ u⇩0 ⋅ u⇩1" and
"q ≤p w" and "w ∈ ⟨{u⇩0,u⇩1}⟩" and "❙|α❙| < ❙|u⇩1 ⋅ q❙|"
"q' ≤p w'" and "w' ∈ ⟨{u⇩0,u⇩1}⟩" and "❙|α❙| ≤ ❙|q'❙|"
shows "u⇩1 ⋅ q ∧⇩p r ⋅ q' = α"
proof-
have pref1: "α ⋅ [c⇩1] ≤p u⇩1 ⋅ q"
using ‹❙|α❙| < ❙|u⇩1 ⋅ q❙|› ‹q ≤p w› bin_snd_mismatch_all_len[of "u⇩1 ⋅ q", OF _ ‹w ∈ ⟨{u⇩0,u⇩1}⟩›]
unfolding pref_cancel_conv by blast
have "α ≤p q'"
using ‹❙|α❙| ≤ ❙|q'❙|› ‹q' ≤p w'› ‹w' ∈ ⟨{u⇩0,u⇩1}⟩› bin_lcp_pref_all_len by blast
have pref2: "α ⋅ [c⇩0] ≤p r ⋅ α"
using assms(1) per_root_lcp_per_root by auto
hence pref2: "α ⋅ [c⇩0] ≤p r ⋅ q'"
using ‹α ≤p q'› pref_prolong by blast
show ?thesis
using lcp_first_mismatch_pref[OF pref1 pref2 bin_mismatch_neq[symmetric]].
qed
end
lemmas no_comm_bin_code = binary_code.bin_code[unfolded binary_code_def]
theorem bin_code_code: assumes "u ⋅ v ≠ v ⋅ u" shows "code {u, v}"
unfolding code_def using no_comm_bin_code[OF assms] by blast
lemma code_bin_code: "u ≠ v ⟹ code {u,v} ⟹ u ⋅ v ≠ v ⋅ u"
by (elim code.code_not_comm) simp_all
lemma lcp_roots_lcp: "x ⋅ y ≠ y ⋅ x ⟹ x ⋅ y ∧⇩p y ⋅ x = ρ x ⋅ ρ y ∧⇩p ρ y ⋅ ρ x"
using binary_code.prim_roots_lcp[unfolded binary_code_def bin_lcp_def, symmetric].
subsection ‹Binary Mismatch tools›
thm binary_code.bin_mismatch_pows[unfolded binary_code_def]
lemma bin_mismatch: "u⇧@Suc k ⋅ v ⋅ z = v⇧@Suc l ⋅ u ⋅ z' ⟹ u ⋅ v = v ⋅ u"
using binary_code.bin_mismatch_pows[unfolded binary_code_def] by blast
definition bin_mismatch_pref :: "'a list ⇒ 'a list ⇒ 'a list ⇒ bool" where
"bin_mismatch_pref x y w ≡ ∃ k. x⇧@k ⋅ y ≤p w"
lemma bm_pref_letter: assumes "x ⋅ y ≠ y ⋅ x" and "bin_mismatch_pref x y (w1 ⋅ y)"
shows "bin_lcp x y ⋅ [bin_mismatch x y] ≤p x ⋅ w1 ⋅ bin_lcp x y"
proof-
interpret binary_code x y
using assms(1) by unfold_locales
from assms[unfolded bin_mismatch_pref_def prefix_def rassoc]
obtain k1 z1 where eq1: "w1 ⋅ y = x⇧@k1 ⋅ y ⋅ z1"
by blast
have "bin_lcp x y ⋅ [bin_mismatch x y] ≤p x ⋅ w1 ⋅ y ⋅ bin_lcp x y"
unfolding lassoc ‹w1 ⋅ y = x⇧@k1 ⋅ y ⋅ z1› pow_Suc[symmetric] unfolding rassoc using bin_lcp_fst_pow_pref by blast
have "❙|bin_lcp x y ⋅ [bin_mismatch x y]❙| ≤ ❙|(x ⋅ w1) ⋅ bin_lcp x y❙|"
unfolding lenmorph sing_len using nemp_len[OF bin_fst_nemp] by linarith
from ruler_le[OF ‹bin_lcp x y ⋅ [bin_mismatch x y] ≤p x ⋅ w1 ⋅ y ⋅ bin_lcp x y› _ this]
show "bin_code_lcp ⋅ [bin_mismatch x y] ≤p x ⋅ w1 ⋅ bin_code_lcp"
unfolding shifts using bin_lcp_snd_lcp.
qed
lemma bm_eq_hard: assumes "x ⋅ w1 = y ⋅ w2" and "bin_mismatch_pref x y (w1 ⋅ y)" and "bin_mismatch_pref y x (w2 ⋅ x)"
shows "x ⋅ y = y ⋅ x"
proof(rule classical)
assume "x ⋅ y ≠ y ⋅ x"
note bm_pref_letter[OF this assms(2)] bm_pref_letter[OF this[symmetric] assms(3)]
from ruler_eq_len[OF this[unfolded lassoc ‹x⋅w1 = y⋅w2› bin_lcp_sym[of y]]]
have "bin_mismatch x y = bin_mismatch y x"
unfolding lenmorph sing_len cancel by blast
thus "x ⋅ y = y ⋅ x"
unfolding bin_mismatch_comm.
qed
lemma bm_hard_lcp: assumes "x ⋅ y ≠ y ⋅ x" and "bin_mismatch_pref x y w1" and "bin_mismatch_pref y x w2"
shows "x ⋅ w1 ∧⇩p y ⋅ w2 = x ⋅ y ∧⇩p y ⋅ x"
proof-
interpret binary_code x y
using ‹x ⋅ y ≠ y ⋅ x› by unfold_locales
write bin_code_lcp (‹α›)
from assms[unfolded bin_mismatch_pref_def]
obtain k m where "x⇧@k ⋅ y ≤p w1" "y⇧@m ⋅ x ≤p w2"
by blast
hence prefs: "x ⋅ x⇧@k ⋅ y ≤p x ⋅ w1" "y ⋅ y⇧@m ⋅ x ≤p y ⋅ w2"
unfolding pref_cancel_conv.
have l_less: "❙|α❙| < ❙|x ⋅ x⇧@k ⋅ y❙|" "❙|α❙| < ❙|y ⋅ y⇧@m ⋅ x❙|"
using bin_lcp_short unfolding lenmorph by simp_all
from bin_code_delay[OF less_imp_le less_imp_le, OF this self_pref self_pref]
have aux: "x ⋅ x⇧@k ⋅ y ∧⇩p y ⋅ y⇧@ m ⋅ x = α"
by blast+
have "¬ x ⋅ x ⇧@ k ⋅ y ⨝ y ⋅ y ⇧@ m ⋅ x"
unfolding prefix_comparable_def lcp_pref_conv'[symmetric] aux aux[unfolded lcp_sym[of "x ⋅ _"]]
using l_less by fastforce
thus ?thesis
using lcp_rulers[OF prefs] unfolding bin_lcp_def aux by blast
qed
lemma bm_pref_hard: assumes "x ⋅ w1 ≤p y ⋅ w2" and "bin_mismatch_pref x y w1"
and "bin_mismatch_pref y x (w2 ⋅ x)"
shows "x ⋅ y = y ⋅ x"
proof(rule classical)
assume "x ⋅ y ≠ y ⋅ x"
then interpret binary_code x y
by unfold_locales
from assms[unfolded bin_mismatch_pref_def prefix_def rassoc]
obtain k1 z1 where eq1: "w1 = x⇧@k1 ⋅ y ⋅ z1"
by blast
have "bin_lcp x y ⋅ [bin_mismatch x y] ≤p x ⋅ w1"
unfolding lassoc ‹w1 = x⇧@k1 ⋅ y ⋅ z1› pow_Suc[symmetric] unfolding rassoc using bin_lcp_fst_pow_pref by blast
note pref_ext[OF pref_trans[OF this assms(1)], unfolded rassoc] bm_pref_letter[OF ‹x ⋅ y ≠ y ⋅ x›[symmetric] assms(3), unfolded bin_lcp_sym[of y]]
from ruler_eq_len[OF this]
have "bin_mismatch x y = bin_mismatch y x"
unfolding lenmorph sing_len cancel by blast
thus "x ⋅ y = y ⋅ x"
unfolding bin_mismatch_comm.
qed
named_theorems bm_elims
lemmas [bm_elims] = bm_eq_hard bm_eq_hard[symmetric] bm_pref_hard bm_pref_hard[symmetric]
bm_hard_lcp bm_hard_lcp[symmetric]
arg_cong2[of _ _ _ _ "λ x y. x ∧⇩p y"]
named_theorems bm_elims_rev
lemmas [bm_elims_rev] = bm_elims[reversed]
named_theorems bm_simps
lemma [bm_simps]: " bin_mismatch_pref x y (y ⋅ v)"
unfolding bin_mismatch_pref_def using append_Nil pow_zero[of x] by blast
lemma [bm_simps]: " bin_mismatch_pref x y y"
unfolding bin_mismatch_pref_def using append_Nil pow_zero[of x] self_pref by metis
lemma [bm_simps]:
"w1 ∈ ⟨{x,y}⟩ ⟹ bin_mismatch_pref x y w ⟹ bin_mismatch_pref x y (w1 ⋅ w)"
unfolding bin_mismatch_pref_def
proof (induct w1 arbitrary: w rule: hull.induct)
case (prod_cl w1 w2)
from prod_cl.hyps(3)[OF prod_cl.prems]
obtain k s where "w2 ⋅ w = x ⇧@ k ⋅ y ⋅ s" by (auto simp add: prefix_def)
consider "w1 = x" | "w1 = y" using ‹w1 ∈ {x,y}› by blast
then show ?case
proof (cases)
assume "w1 = x"
show ?thesis
unfolding rassoc ‹w2 ⋅ w = x ⇧@ k ⋅ y ⋅ s› ‹w1 = x›
unfolding lassoc pow_Suc[symmetric] unfolding rassoc
using same_prefix_prefix by blast
next
assume "w1 = y"
have "x⇧@0 ⋅ y ≤p y ⋅ w2 ⋅ w" by auto
thus ?thesis
unfolding rassoc ‹w1 = y› by blast
qed
qed simp
lemmas [bm_simps] = lcp_ext_left
named_theorems bm_simps_rev
lemmas [bm_simps_rev] = bm_simps[reversed]
named_theorems bin_hull_in
lemma[bin_hull_in]: "x ∈ ⟨{x,y}⟩"
by blast
lemma[bin_hull_in]: "y ∈ ⟨{x,y}⟩"
by blast
lemma[bin_hull_in]: "w ∈ ⟨{x,y}⟩ ⟷ w ∈ ⟨{y,x}⟩"
by (simp add: insert_commute)
lemmas[bin_hull_in] = hull_closed power_in rassoc
named_theorems bin_hull_in_rev
lemmas [bin_hull_in_rev] = bin_hull_in[reversed]
method mismatch0 =
((simp only: shifts bm_simps)?,
(elim bm_elims)?;
(simp_all only: bm_simps bin_hull_in))
method mismatch_rev =
((simp only: shifts_rev bm_simps_rev)?,
(elim bm_elims_rev)?;
(simp_all only: bm_simps_rev bin_hull_in_rev))
method mismatch =
(insert method_facts, use nothing in
‹(mismatch0;fail)|(mismatch_rev)›
)
thm bm_elims
subsubsection "Mismatch method demonstrations"
lemma "y ⋅ x ≤p x⇧@k ⋅ x ⋅ y ⋅ w ⟹ x ⋅ y = y ⋅ x"
by mismatch
lemma "w1 ∈ ⟨{x,y}⟩ ⟹ w2 ∈ ⟨{x,y}⟩ ⟹ x ⋅ w2 ⋅ y ⋅ z = y ⋅ w1 ⋅ x ⋅ v ⟹ x ⋅ y = y ⋅ x"
by mismatch
lemma "w1 ∈ ⟨{x,y}⟩ ⟹ y ⋅ x ⋅ w2 ⋅ z = x ⋅ w1 ⟹ x ⋅ y = y ⋅ x"
by mismatch
lemma "w1 ∈ ⟨{x,y}⟩ ⟹ w2 ∈ ⟨{x,y}⟩ ⟹ x ⋅ y ⋅ w2 ⋅ x ≤s x ⋅ w1 ⋅ y ⟹ x ⋅ y = y ⋅ x"
by mismatch
lemma assumes "x ⋅ y ⋅ z = y ⋅ y ⋅ x ⋅ v" shows "x ⋅ y = y ⋅ x"
using assms by mismatch
lemma assumes "y ⋅ x ⋅ x ⋅ y ⋅ z = y ⋅ x ⋅ y ⋅ y ⋅ x ⋅ v" shows "x ⋅ y = y ⋅ x"
using assms by mismatch
lemma "y ⋅ y ⋅ x ⋅ v = x ⋅ x ⋅ y ⋅ z ⟹ x ⋅ y = y ⋅ x"
by mismatch
lemma "x ⋅ x ⋅ y ⋅ z = y ⋅ y ⋅ x ⋅ z' ⟹ x ⋅ y = y ⋅ x"
by mismatch
lemma "z ⋅ x ⋅ y ⋅ x ⋅ x = v ⋅ x ⋅ y ⋅ y ⟹ y ⋅ x = x ⋅ y"
by mismatch
lemma "x ⋅ y ≤p y ⋅ y ⋅ x ⟹ x ⋅ y = y ⋅ x"
by mismatch
lemma "y ⋅ x ⋅ x ⋅ x ⋅ y ≤p y ⋅ x ⋅ x ⋅ y ⋅ y ⋅ x ⟹ x ⋅ y = y ⋅ x"
by mismatch
lemma "x ⋅ y ≤p y ⋅ y ⋅ x ⋅ z ⟹ y ⋅ x = x ⋅ y"
by mismatch
lemma "x ⋅ x ⋅ y ⋅ y ⋅ y ≤s z⋅ y ⋅ y ⋅ x ⋅ x ⟹ x ⋅ y = y ⋅ x"
by mismatch
lemma assumes "x ⋅ x ⋅ y ⋅ y ⋅ y ⋅ y ≤s z⋅ y ⋅ y ⋅ x ⋅ x" shows "x ⋅ y = y ⋅ x"
using assms by mismatch
lemma "k ≠ 0 ⟹ j ≠ 0 ⟹ (x ⇧@ j ⋅ y ⇧@ ka) ⋅ y = y⇧@k ⋅ x ⇧@ j ⋅ y ⇧@ (k - 1) ⟹ x ⋅ y = y ⋅ x"
by mismatch
lemma "dif ≠ 0 ⟹ j ≠ 0 ⟹ (x ⇧@ j ⋅ y ⇧@ ka) ⋅ y ⇧@ dif = y ⇧@ dif ⋅ x ⇧@ j ⋅ y ⇧@ ka ⟹ x ⋅ y = y ⋅ x"
by mismatch
lemma assumes "x ⋅ y ≠ y ⋅ x"
shows "x ⋅ x ⋅ y ∧⇩p y ⋅ y ⋅ x = (x ⋅ y ∧⇩p y ⋅ x)"
using assms by mismatch
lemma assumes "x ⋅ y ≠ y ⋅ x"
shows "w ⋅ z ⋅ x ⋅ x ⋅ y ∧⇩p w ⋅ z ⋅ y ⋅ y ⋅ x = (w ⋅ z) ⋅ (x ⋅ y ∧⇩p y ⋅ x)"
using assms by mismatch
subsection ‹Applied mismatch›
lemma pows_comm_comm: assumes "u⇧@k ⋅ v⇧@m = u⇧@l ⋅ v⇧@n" "k ≠ l" shows "u ⋅ v = v ⋅ u"
proof-
have aux: "u⇧@k ⋅ v⇧@m ⋅ v ⋅ u = u⇧@l ⋅ v⇧@n ⋅ v ⋅ u ⟹ k ≠ l ⟹ u ⋅ v = v ⋅ u"
by (induct k l rule: diff_induct) mismatch+
from this[unfolded lassoc cancel_right, OF assms]
show "u ⋅ v = v ⋅ u".
qed
section ‹Two words hull (not necessarily a code)›
lemma bin_lists_len_count: assumes "x ≠ y" and "ws ∈ lists {x,y}" shows
"count_list ws x + count_list ws y = ❙|ws❙|"
proof-
have "finite {x,y}" by simp
have "set ws ⊆ {x,y}" using ‹ws ∈ lists{x,y}› by blast
show ?thesis
using sum_count_set[OF ‹set ws ⊆ {x,y}› ‹finite {x,y}›] ‹x ≠ y› by simp
qed
lemma two_elem_first_block: assumes "w ∈ ⟨{u,v}⟩"
obtains m where "u⇧@m ⋅ v ⨝ w"
using assms
proof-
obtain ws where "concat ws = w" and "ws ∈ lists {u,v}"
using concat_dec[OF ‹w ∈ ⟨{u,v}⟩›] dec_in_lists[OF ‹w ∈ ⟨{u,v}⟩›] by simp
consider (only_u) "takeWhile (λ x. x = u) ws = ws" | (some_v) "takeWhile (λ x. x = u) ws ≠ ws ∧ hd (dropWhile (λ x. x = u) ws) ≠ u"
using hd_dropWhile[of "(λ x. x = u)" ws] by auto
then show thesis
proof (cases)
case only_u
hence "ws = [u]⇧@❙|ws❙|"
unfolding takeWhile_sing_pow by metis
hence "w = u⇧@❙|ws❙|"
using ‹concat ws = w› concat_sing_pow by metis
then show thesis
using that by blast
next
case some_v
note some_v = conjunct1[OF this] conjunct2[OF this]
hence "dropWhile (λ x. x = u) ws ≠ ε" by force
from lists_hd_in_set[OF this]
have "hd (dropWhile (λx. x = u) ws) ∈ {u,v}"
using ‹ws ∈ lists {u,v}› append_in_lists_conv takeWhile_dropWhile_id by metis
hence "hd (dropWhile (λx. x = u) ws) = v"
using some_v(2) by simp
from dropWhile_distinct[of ws u, unfolded this] some_v(1)
have "(takeWhile (λx. x = u) ws)⋅[v] ≤p ws"
unfolding takeWhile_letter_pref_exp by simp
from pref_concat_pref[OF this, unfolded concat_morph, unfolded ‹concat ws = w› concat_takeWhile_sing[unfolded this]]
have "u⇧@❙|takeWhile (λx. x = u) ws❙|⋅ v ≤p w"
by simp
with that
show thesis
by blast
qed
qed
lemmas two_elem_last_block = two_elem_first_block[reversed]
lemma two_elem_pref: assumes "v ≤p u ⋅ p" and "p ∈ ⟨{u,v}⟩"
shows "v ≤p u ⋅ v"
proof-
obtain m where "u⇧@m ⋅ v ⨝ p"
using two_elem_first_block[OF ‹p ∈ ⟨{u,v}⟩›].
have "v ≤p u⇧@(Suc m) ⋅ v"
using pref_prolong_comp[OF ‹v ≤p u ⋅ p› ‹u⇧@m ⋅ v ⨝ p›, unfolded lassoc, folded pow_Suc].
thus "v ≤p u ⋅ v"
using per_drop_exp' by blast
qed
lemmas two_elem_suf = two_elem_pref[reversed]
lemma gen_drop_exp: assumes "p ∈ ⟨{u,v⇧@(Suc k)}⟩" shows "p ∈ ⟨{u,v}⟩"
by (rule hull.induct[OF assms], simp, blast)
lemma gen_drop_exp_pos: assumes "p ∈ ⟨{u,v⇧@k}⟩" "0 < k" shows "p ∈ ⟨{u,v}⟩"
using gen_drop_exp[of _ _ _ "k-1", unfolded Suc_minus_pos[OF ‹0 < k›], OF ‹p ∈ ⟨{u,v⇧@k}⟩›].
lemma gen_prim: "p ∈ ⟨{u,v}⟩ ⟹ p ∈ ⟨{u,ρ v}⟩"
using gen_drop_exp_pos primroot_expE by metis
lemma roots_hull: assumes "w ∈ ⟨{u⇧@k,v⇧@m}⟩" shows "w ∈ ⟨{u,v}⟩"
proof-
have "u⇧@k ∈ ⟨{u,v}⟩" and "v⇧@m ∈ ⟨{u,v}⟩"
by (simp_all add: gen_in power_in)
hence "{u⇧@k,v⇧@m} ⊆ ⟨{u,v}⟩"
by blast
from hull_mono'[OF this]
show "w ∈ ⟨{u,v}⟩"
using ‹w ∈ ⟨{u⇧@k,v⇧@m}⟩› by blast
qed
lemma roots_hull_sub: "⟨{u⇧@k,v⇧@m}⟩ ⊆ ⟨{u,v}⟩"
using roots_hull by blast
lemma primroot_gen[intro]: "v ∈ ⟨{u, ρ v}⟩"
using power_in[of "ρ v" "{u,ρ v}"]
by (cases "v = ε", simp) (metis primroot_expE gen_in insert_iff)
lemma primroot_gen'[intro]: "u ∈ ⟨{ρ u, v}⟩"
using primroot_gen insert_commute by metis
lemma set_lists_primroot: "set ws ⊆ {x,y} ⟹ ws ∈ lists ⟨{ρ x, ρ y}⟩"
by blast
section ‹Free hull›
text‹While not every set $G$ of generators is a code, there is a unique minimal
free monoid containing it, called the \emph{free hull} of $G$.
It can be defined inductively using the property known as the \emph{stability condition}.
›
inductive_set free_hull :: "'a list set ⇒ 'a list set" (‹⟨_⟩⇩F›)
for G where
"ε ∈ ⟨G⟩⇩F"
| free_gen_in: "w ∈ G ⟹ w ∈ ⟨G⟩⇩F"
| "w1 ∈ ⟨G⟩⇩F ⟹ w2 ∈ ⟨G⟩⇩F ⟹ w1 ⋅ w2 ∈ ⟨G⟩⇩F"
| "p ∈ ⟨G⟩⇩F ⟹ q ∈ ⟨G⟩⇩F ⟹ p ⋅ w ∈ ⟨G⟩⇩F ⟹ w ⋅ q ∈ ⟨G⟩⇩F ⟹ w ∈ ⟨G⟩⇩F"
lemmas [intro] = free_hull.intros
text‹The defined set indeed is a hull.›
lemma free_hull_hull[simp]: "⟨⟨G⟩⇩F⟩ = ⟨G⟩⇩F"
by (intro antisym subsetI, rule hull.induct) blast+
text‹The free hull is always (non-strictly) larger than the hull.›
lemma hull_sub_free_hull: "⟨G⟩ ⊆ ⟨G⟩⇩F"
proof
fix x assume "x ∈ ⟨G⟩"
then show "x ∈ ⟨G⟩⇩F"
using free_hull.intros(3)
hull_induct[of x G "λ x. x ∈ ⟨G⟩⇩F", OF ‹x ∈ ⟨G⟩› free_hull.intros(1)[of G] free_hull.intros(2)]
by auto
qed
text‹On the other hand, it can be proved that the \emph{free basis}, defined as the basis of the free hull, has a (non-strictly) smaller cardinality than the ordinary basis.›
definition free_basis :: "'a list set ⇒ 'a list set" (‹𝔅⇩F _› [54] 55)
where "free_basis G ≡ 𝔅 ⟨G⟩⇩F"
lemma basis_gen_hull_free: "⟨𝔅⇩F G⟩ = ⟨G⟩⇩F"
unfolding free_basis_def using basis_gen_hull free_hull_hull by blast
lemma genset_sub_free: "G ⊆ ⟨G⟩⇩F"
by (simp add: free_hull.free_gen_in subsetI)
text
‹We have developed two points of view on freeness:
▪ being a free hull, that is, to satisfy the stability condition;
▪ being generated by a code.›
text‹We now show their equivalence›
text‹First, basis of a free hull is a code.›
lemma free_basis_code[simp]: "code (𝔅⇩F G)"
proof
fix xs ys
show "xs ∈ lists (𝔅⇩F G) ⟹ ys ∈ lists (𝔅⇩F G) ⟹ concat xs = concat ys ⟹ xs = ys"
proof(induction xs ys rule: list_induct2')
case (2 x xs)
show ?case
using listsE[OF ‹x # xs ∈ lists (𝔅⇩F G)›, of "x ∈ 𝔅⇩F G", unfolded free_basis_def, THEN emp_not_basis]
concat.simps(2)[of x xs, unfolded ‹concat (x # xs) = concat ε›[unfolded concat.simps(1)], symmetric, unfolded append_is_Nil_conv[of x "concat xs"]]
by blast
next
case (3 y ys)
show ?case
using listsE[OF ‹y # ys ∈ lists (𝔅⇩F G)›, of "y ∈ 𝔅⇩F G", unfolded free_basis_def, THEN emp_not_basis]
concat.simps(2)[of y ys, unfolded ‹concat ε = concat (y # ys)›[unfolded concat.simps(1),symmetric],symmetric, unfolded append_is_Nil_conv[of y "concat ys"]]
by blast
next
case (4 x xs y ys)
have "❙|x❙| = ❙|y❙|"
proof(rule ccontr)
assume "❙|x❙| ≠ ❙|y❙|"
have "x ⋅ concat xs = y ⋅ concat ys"
using ‹concat (x # xs) = concat (y # ys)› by simp
then obtain t where or: "x = y ⋅ t ∧ t ⋅ concat xs = concat ys ∨ x ⋅ t = y ∧ concat xs = t ⋅ concat ys"
using append_eq_append_conv2[of x "concat xs" y "concat ys"] by blast
hence "t ≠ ε"
using ‹❙|x❙| ≠ ❙|y❙|› by auto
have "x ∈ 𝔅⇩F G" and "y ∈ 𝔅⇩F G"
using listsE[OF ‹x # xs ∈ lists (𝔅⇩F G)›, of "x ∈ 𝔅⇩F G" ] listsE[OF ‹y # ys ∈ lists (𝔅⇩F G)›, of "y ∈ 𝔅⇩F G" ] by blast+
hence "x ≠ ε" and "y ≠ ε"
unfolding free_basis_def using emp_not_basis by blast+
have "x ∈ ⟨G⟩⇩F" and "y ∈ ⟨G⟩⇩F"
using basis_sub[of "⟨G⟩⇩F", unfolded free_basis_def[symmetric] ] ‹x # xs ∈ lists (𝔅⇩F G)›
‹y # ys ∈ lists (𝔅⇩F G)› by auto
have "concat xs ∈ ⟨G⟩⇩F" and "concat ys ∈ ⟨G⟩⇩F"
using concat_tl_basis[OF ‹x # xs ∈ lists (𝔅⇩F G)›[unfolded free_basis_def]]
concat_tl_basis[OF ‹y # ys ∈ lists (𝔅⇩F G)›[unfolded free_basis_def]] unfolding free_hull_hull.
have "t ∈ ⟨G⟩⇩F"
using or free_hull.intros(4) ‹x ∈ ⟨G⟩⇩F› ‹y ∈ ⟨G⟩⇩F› ‹concat xs ∈ ⟨G⟩⇩F› ‹concat ys ∈ ⟨G⟩⇩F› by metis
thus False
using or basis_dec[of x "⟨G⟩⇩F" t, unfolded free_hull_hull, OF ‹x ∈ ⟨G⟩⇩F› ‹t ∈ ⟨G⟩⇩F›]
basis_dec[of y "⟨G⟩⇩F" t, unfolded free_hull_hull, OF ‹y ∈ ⟨G⟩⇩F› ‹t ∈ ⟨G⟩⇩F›]
using ‹t ≠ ε› ‹x ≠ ε› ‹y ≠ ε› ‹x ∈ 𝔅⇩F G› ‹y ∈ 𝔅⇩F G› unfolding free_basis_def
by auto
qed
thus "x # xs = y # ys"
using "4.IH" ‹x # xs ∈ lists (𝔅⇩F G)› ‹y # ys ∈ lists (𝔅⇩F G)› ‹concat (x # xs) = concat (y # ys)›
by auto
next
qed simp
qed
lemma gen_in_free_hull: "x ∈ G ⟹ x ∈ ⟨𝔅⇩F G⟩"
using free_hull.free_gen_in[folded basis_gen_hull_free].
text‹Second, a code generates its free hull.›
lemma (in code) code_gen_free_hull: "⟨𝒞⟩⇩F = ⟨𝒞⟩"
proof
show "⟨𝒞⟩ ⊆ ⟨𝒞⟩⇩F"
using hull_mono[of 𝒞 "⟨𝒞⟩⇩F"]
free_gen_in[of _ 𝒞] subsetI[of 𝒞 "⟨𝒞⟩⇩F"]
unfolding free_hull_hull by auto
show "⟨𝒞⟩⇩F ⊆ ⟨𝒞⟩"
proof
fix x assume "x ∈ ⟨𝒞⟩⇩F"
have "ε ∈ ⟨𝒞⟩"
by simp
show "x ∈ ⟨𝒞⟩"
proof(rule free_hull.induct[of x 𝒞])
fix p q w assume "p ∈ ⟨𝒞⟩" "q ∈ ⟨𝒞⟩" "p ⋅ w ∈ ⟨𝒞⟩" "w ⋅ q ∈ ⟨𝒞⟩"
have eq: "(Dec 𝒞 p) ⋅ (Dec 𝒞 w ⋅ q) = (Dec 𝒞 p ⋅ w) ⋅ (Dec 𝒞 q)"
using code_dec_morph[OF ‹p ∈ ⟨𝒞⟩› ‹w ⋅ q ∈ ⟨𝒞⟩›, unfolded lassoc]
unfolding code_dec_morph[OF ‹p ⋅ w ∈ ⟨𝒞⟩› ‹q ∈ ⟨𝒞⟩›, symmetric].
have "Dec 𝒞 p ⨝ Dec 𝒞 p ⋅ w"
using eqd_comp[OF eq].
hence "Dec 𝒞 p ≤p Dec 𝒞 p ⋅ w"
using ‹p ⋅ w ∈ ⟨𝒞⟩› ‹p ∈ ⟨𝒞⟩› concat_morph concat_dec prefD pref_antisym triv_pref
unfolding prefix_comparable_def
by metis
then obtain ts where "(Dec 𝒞 p) ⋅ ts = Dec 𝒞 p ⋅ w"
using lq_pref by blast
hence "ts ∈ lists 𝒞"
using ‹p ⋅ w ∈ ⟨𝒞⟩› by inlists
hence "concat ts = w"
using concat_morph[of "Dec 𝒞 p" ts]
unfolding ‹(Dec 𝒞 p) ⋅ ts = Dec 𝒞 p ⋅ w› concat_dec[OF ‹p ⋅ w ∈ ⟨𝒞⟩›] concat_dec[OF ‹p ∈ ⟨𝒞⟩›] by auto
thus "w ∈ ⟨𝒞⟩"
using ‹ts ∈ lists 𝒞› by auto
qed (simp_all add: ‹x ∈ ⟨𝒞⟩⇩F› hull_closed gen_in)
qed
qed
text‹That is, a code is its own free basis›
lemma (in code) code_free_basis: "𝒞 = 𝔅⇩F 𝒞"
using basis_of_hull[of 𝒞, unfolded code_gen_free_hull[symmetric]
code_is_basis, symmetric] unfolding free_basis_def.
text‹This allows to use the introduction rules of the free hull to prove one of the basic characterizations
of the code, called the stability condition›
lemma (in code) stability: "p ∈ ⟨𝒞⟩ ⟹ q ∈ ⟨𝒞⟩ ⟹ p ⋅ w ∈ ⟨𝒞⟩ ⟹ w ⋅ q ∈ ⟨𝒞⟩ ⟹ w ∈ ⟨𝒞⟩"
unfolding code_gen_free_hull[symmetric] using free_hull.intros(4) by auto
text‹Moreover, the free hull of G is the smallest code-generated hull containing G.
In other words, the term free hull is appropriate.›
text‹First, several intuitive monotonicity and closure results.›
lemma free_hull_mono: "G ⊆ H ⟹ ⟨G⟩⇩F ⊆ ⟨H⟩⇩F"
proof
assume "G ⊆ H"
fix x assume "x ∈ ⟨G⟩⇩F"
have el: "⋀ w. w ∈ G ⟹ w ∈ ⟨H⟩⇩F"
using ‹G ⊆ H› free_hull.free_gen_in by auto
show "x ∈ ⟨H⟩⇩F"
by (rule free_hull.induct[of x G]) (auto simp add: ‹x ∈ ⟨G⟩⇩F› el)
qed
lemma free_hull_idem: "⟨⟨G⟩⇩F⟩⇩F = ⟨G⟩⇩F"
proof
show "⟨⟨G⟩⇩F⟩⇩F ⊆ ⟨G⟩⇩F"
proof
fix x assume "x ∈ ⟨⟨G⟩⇩F⟩⇩F"
show "x ∈ ⟨G⟩⇩F"
proof (rule free_hull.induct[of x "⟨G⟩⇩F"])
show "⋀p q w. p ∈ ⟨G⟩⇩F ⟹ q ∈ ⟨G⟩⇩F ⟹ p ⋅ w ∈ ⟨G⟩⇩F ⟹ w ⋅ q ∈ ⟨G⟩⇩F ⟹ w ∈ ⟨G⟩⇩F"
using free_hull.intros(4) by auto
qed (simp_all add: ‹x ∈ ⟨⟨G⟩⇩F⟩⇩F› free_hull.intros(1), simp add: free_hull.intros(2), simp add: free_hull.intros(3))
qed
next
show "⟨G⟩⇩F ⊆ ⟨⟨G⟩⇩F⟩⇩F"
using free_hull_hull hull_sub_free_hull by auto
qed
lemma hull_gen_free_hull: "⟨⟨G⟩⟩⇩F = ⟨G⟩⇩F"
proof
show " ⟨⟨G⟩⟩⇩F ⊆ ⟨G⟩⇩F"
using free_hull_idem free_hull_mono hull_sub_free_hull by metis
next
show "⟨G⟩⇩F ⊆ ⟨⟨G⟩⟩⇩F"
by (simp add: free_hull_mono)
qed
text ‹Code is also the free basis of its hull.›
lemma (in code) code_free_basis_hull: "𝒞 = 𝔅⇩F ⟨𝒞⟩"
unfolding free_basis_def using code_free_basis[unfolded free_basis_def]
unfolding hull_gen_free_hull.
text‹The minimality of the free hull easily follows.›
theorem (in code) free_hull_min: assumes "G ⊆ ⟨𝒞⟩" shows "⟨G⟩⇩F ⊆ ⟨𝒞⟩"
using free_hull_mono[OF ‹G ⊆ ⟨𝒞⟩›] unfolding hull_gen_free_hull
unfolding code_gen_free_hull.
theorem free_hull_inter: "⟨G⟩⇩F = ⋂ {M. G ⊆ M ∧ M = ⟨M⟩⇩F}"
proof
have "X ∈ {M. G ⊆ M ∧ M = ⟨M⟩⇩F} ⟹ ⟨G⟩⇩F ⊆ X" for X
unfolding mem_Collect_eq[of _ "λ M. G ⊆ M ∧ M = ⟨M⟩⇩F"]
using free_hull_mono[of G X] by simp
from Inter_greatest[of "{M. G ⊆ M ∧ M = ⟨M⟩⇩F}", OF this]
show "⟨G⟩⇩F ⊆ ⋂ {M. G ⊆ M ∧ M = ⟨M⟩⇩F}"
by blast
next
show " ⋂ {M. G ⊆ M ∧ M = ⟨M⟩⇩F} ⊆ ⟨G⟩⇩F"
by (simp add: Inter_lower free_hull_idem genset_sub_free)
qed
text‹Decomposition into the free basis is a morphism.›
lemma free_basis_dec_morph: "u ∈ ⟨G⟩⇩F ⟹ v ∈ ⟨G⟩⇩F ⟹
Dec (𝔅⇩F G) (u ⋅ v) = (Dec (𝔅⇩F G) u) ⋅ (Dec (𝔅⇩F G) v)"
using code.code_dec_morph[OF free_basis_code, of u G v, symmetric,
unfolded basis_gen_hull_free[of G]].
section ‹Reversing hulls and decompositions›
lemma basis_rev_commute[reversal_rule]: "𝔅 (rev ` G) = rev ` (𝔅 G)"
proof
have "⟨rev ` 𝔅 G⟩ = ⟨rev ` G⟩" and *: "⟨rev ` 𝔅 (rev ` G)⟩ = ⟨rev ` rev `G⟩"
unfolding rev_hull[symmetric] basis_gen_hull by blast+
from basis_sub_gen[OF this(1)]
show "𝔅 (rev ` G) ⊆ rev ` 𝔅 G".
from image_mono[OF basis_sub_gen[OF *], of rev]
show "rev ` (𝔅 G) ⊆ 𝔅 (rev ` G)"
unfolding rev_rev_image_eq.
qed
lemma rev_free_hull_comm: "⟨rev ` X⟩⇩F = rev ` ⟨X⟩⇩F"
proof-
have "rev ` ⟨X⟩⇩F ⊆ ⟨rev ` X⟩⇩F" for X :: "'a list set"
proof
fix x assume "x ∈ rev ` ⟨X⟩⇩F"
hence "rev x ∈ ⟨X⟩⇩F"
by (simp add: rev_in_conv)
have "rev x ∈ rev ` ⟨rev ` X⟩⇩F"
by (induct rule: free_hull.induct[OF ‹rev x ∈ ⟨X⟩⇩F›])
(auto simp add: rev_in_conv[symmetric])
then show "x ∈ ⟨rev ` X⟩⇩F"
by blast
qed
from this
image_mono[OF this[of "rev ` X", unfolded rev_rev_image_eq], of rev, unfolded rev_rev_image_eq]
show "⟨rev ` X⟩⇩F = rev ` ⟨X⟩⇩F"
by blast
qed
lemma free_basis_rev_commute [reversal_rule]: "𝔅⇩F rev ` X = rev ` (𝔅⇩F X)"
unfolding free_basis_def basis_rev_commute free_basis_def rev_free_hull_comm..
lemma rev_dec[reversal_rule]: assumes "x ∈ ⟨X⟩⇩F" shows "Dec rev ` (𝔅⇩F X) (rev x) = map rev (rev (Dec (𝔅⇩F X) x))"
proof-
have "x ∈ ⟨𝔅⇩F X⟩"
using ‹x ∈ ⟨X⟩⇩F› by (simp add: basis_gen_hull_free)
from concat_dec[OF this]
have "concat (map rev (rev (Dec 𝔅⇩F X x))) = rev x"
unfolding rev_concat[symmetric] by blast
from rev_image_eqI[OF rev_in_lists[OF dec_in_lists[OF ‹x ∈ ⟨𝔅⇩F X⟩›]], of _ "map rev"]
have "map rev (rev (Dec 𝔅⇩F X x)) ∈ lists (rev ` (𝔅⇩F X))"
unfolding lists_image by blast
from code.code_unique_dec'[OF code.code_rev_code[OF free_basis_code] this]
show ?thesis
unfolding ‹concat (map rev (rev (Dec 𝔅⇩F X x))) = rev x›.
qed
lemma rev_hd_dec_last_eq[reversal_rule]: assumes "x ∈ X" and "x ≠ ε" shows
"rev (hd (Dec (rev ` (𝔅⇩F X)) (rev x))) = last (Dec 𝔅⇩F X x)"
proof-
have "rev (Dec 𝔅⇩F X x) ≠ ε"
using ‹x ∈ X› basis_gen_hull_free dec_nemp'[OF ‹x ≠ ε›] by blast
show ?thesis
unfolding hd_rev rev_dec[OF free_gen_in[OF ‹x ∈ X›]] hd_map[OF ‹rev (Dec 𝔅⇩F X x) ≠ ε›]
by simp
qed
lemma rev_hd_dec_last_eq'[reversal_rule]: assumes "x ∈ X" and "x ≠ ε" shows
"(hd (Dec (rev ` (𝔅⇩F X)) (rev x))) = rev (last (Dec 𝔅⇩F X x))"
using assms(1) assms(2) rev_hd_dec_last_eq rev_swap by blast
section ‹Lists as the free hull of singletons›
text‹A crucial property of free monoids of words is that they can be seen as lists over the free basis,
instead as lists over the original alphabet.›
abbreviation sings where "sings B ≡ {[b] | b. b ∈ B}"
term "Set.filter P A"
lemma sings_image: "sings B = (λ x. [x]) ` B"
using Setcompr_eq_image.
lemma lists_sing_map_concat_ident: "xs ∈ lists (sings B) ⟹ xs = map (λ x. [x]) (concat xs)"
by (induct xs, simp, auto)
lemma code_sings: "code (sings B)"
proof
fix xs ys assume xs: "xs ∈ lists (sings B)" and ys: "ys ∈ lists (sings B)"
and eq: "concat xs = concat ys"
from lists_sing_map_concat_ident[OF xs, unfolded eq]
show "xs = ys" unfolding lists_sing_map_concat_ident[OF ys, symmetric].
qed
lemma sings_gen_lists: "⟨sings B⟩ = lists B"
unfolding hull_concat_lists
proof(intro equalityI subsetI, standard)
fix xs
show "xs ∈ concat ` lists (sings B) ⟹ ∀x∈set xs. x ∈ B"
by force
assume "xs ∈ lists B"
hence "map (λx. x # ε) xs ∈ lists (sings B)"
by force
from imageI[OF this, of concat]
show "xs ∈ concat ` lists (sings B)"
unfolding concat_map_sing_ident[of xs].
qed
lemma sing_gen_lists: "lists {x} = ⟨{[x]}⟩"
using sings_gen_lists[of "{x}"] by simp
lemma bin_gen_lists: "lists {x, y} = ⟨{[x],[y]}⟩"
using sings_gen_lists[of "{x,y}"] unfolding Setcompr_eq_image by simp
lemma "sings B = 𝔅⇩F (lists B)"
using code.code_free_basis_hull[OF code_sings, of B, unfolded sings_gen_lists].
lemma map_sings: "xs ∈ lists B ⟹ map (λx. x # ε) xs ∈ lists (sings B)"
by (induct xs) auto
lemma dec_sings: "xs ∈ lists B ⟹ Dec (sings B) xs = map (λ x. [x]) xs"
using code.code_unique_dec'[OF code_sings, of "map (λ x. [x]) xs" B, OF map_sings]
unfolding concat_map_sing_ident.
lemma sing_lists_exp: assumes "ws ∈ lists {x}"
obtains k where "ws = [x]⇧@k"
using unique_letter_wordE''[OF assms[folded in_lists_conv_set_subset]].
lemma sing_lists_exp_len: "ws ∈ lists {x} ⟹ [x]⇧@❙|ws❙| = ws"
by (induct ws, auto)
lemma sing_lists_exp_count: "ws ∈ lists {x} ⟹ [x]⇧@(count_list ws x) = ws"
by (induct ws, auto)
lemma sing_set_pow_count_list: "set ws ⊆ {a} ⟹ [a]⇧@(count_list ws a) = ws"
unfolding in_lists_conv_set_subset using sing_lists_exp_count.
lemma sing_set_pow: "set ws ⊆ {a} ⟹ [a]⇧@❙|ws❙| = ws"
by auto
lemma count_sing_exp[simp]: "count_list ([a]⇧@k) a = k"
by (induct k, simp_all)
lemma count_sing_exp'[simp]: "count_list ([a]) a = 1"
by simp
lemma count_sing_distinct[simp]: "a ≠ b ⟹ count_list ([a]⇧@k) b = 0"
by (induct k, simp, auto)
lemma count_sing_distinct'[simp]: "a ≠ b ⟹ count_list ([a]) b = 0"
by simp
lemma sing_letter_imp_prim: assumes "count_list w a = 1" shows "primitive w"
proof
fix r k
assume "r ⇧@ k = w"
have "count_list w a = k * count_list r a"
by (simp only: count_list_pow flip: ‹r ⇧@ k = w›)
then show "k = 1"
unfolding ‹count_list w a = 1› by simp
qed
lemma prim_abk: "a ≠ b ⟹ primitive ([a] ⋅ [b] ⇧@ k)"
by (intro sing_letter_imp_prim[of _ a]) simp
lemma sing_code: "x ≠ ε ⟹ code {x}"
proof (rule code.intro)
fix xs ys
assume "x ≠ ε" "xs ∈ lists {x}" "ys ∈ lists {x}" "concat xs = concat ys"
show "xs = ys"
using ‹concat xs = concat ys›
[unfolded concat_sing_list_pow'[OF ‹xs ∈ lists {x}›]
concat_sing_list_pow'[OF ‹ys ∈ lists {x}›]
eq_pow_exp[OF ‹x ≠ ε›]]
sing_lists_exp_len[OF ‹xs ∈ lists {x}›]
sing_lists_exp_len[OF ‹ys ∈ lists {x}›] by argo
qed
lemma sings_card: "card A = card (sings A)"
by(rule bij_betw_same_card, rule bij_betwI'[of _ "λx. [x]"], auto)
lemma sings_finite: "finite A = finite (sings A)"
by(rule bij_betw_finite, rule bij_betwI'[of _ "λx. [x]"], auto)
lemma sings_conv: "A = B ⟷ sings A = sings B"
proof(standard, simp)
have "⋀x A B. sings A = sings B ⟹ x ∈ A ⟹ x ∈ B"
proof-
fix x :: "'b" and A B
assume "sings A = sings B" "x ∈ A"
hence "[x] ∈ sings B"
using ‹sings A = sings B› by blast
thus "x ∈ B"
by blast
qed
from this[of A B] this[of B A, OF sym]
show "sings A = sings B ⟹ A = B"
by blast
qed
section ‹Various additional lemmas›
subsection ‹Roots of binary set›
lemma two_roots_code: assumes "x ≠ ε" and "y ≠ ε" shows "code {ρ x, ρ y}"
using assms
proof (cases "ρ x = ρ y")
assume "ρ x = ρ y"
thus "code {ρ x, ρ y}" using sing_code[OF primroot_nemp[OF ‹x ≠ ε›]] by simp
next
assume "ρ x ≠ ρ y"
hence "ρ x ⋅ ρ y ≠ ρ y ⋅ ρ x"
using comm_prim[OF primroot_prim[OF ‹x ≠ ε›] primroot_prim[OF ‹y ≠ ε›]] by blast
thus "code {ρ x, ρ y}"
by (simp add: bin_code_code)
qed
lemma primroot_in_set_dec: assumes "x ≠ ε" and "y ≠ ε" shows "ρ x ∈ set (Dec {ρ x, ρ y} x)"
proof-
obtain k where "concat ([ρ x]⇧@k) = x" "0 < k"
using primroot_expE
concat_sing_pow[symmetric, of "ρ x"] by metis
from code.code_unique_dec'[OF two_roots_code[OF assms], of "[ρ x]⇧@k", unfolded ‹concat ([ρ x]⇧@k) = x›]
have "Dec {ρ x, ρ y} x = [ρ x]⇧@k"
using insertI1 sing_pow_lists by metis
show ?thesis
unfolding ‹Dec {ρ x, ρ y} x = [ρ x]⇧@k› using ‹0 < k› by simp
qed
lemma primroot_dec: assumes "x ⋅ y ≠ y ⋅ x"
shows "(Dec {ρ x, ρ y} x) = [ρ x]⇧@e⇩ρ x" "(Dec {ρ x, ρ y} y) = [ρ y]⇧@e⇩ρ y"
by (simp_all add: binary_code.intro[OF assms] binary_code.primroot_dec)
lemma (in binary_code) bin_roots_sings_code: "non_overlapping {Dec {ρ u⇩0, ρ u⇩1} u⇩0, Dec {ρ u⇩0, ρ u⇩1} u⇩1}"
using code_roots_non_overlapping unfolding primroot_dec by force
subsection Other
lemma bin_count_one_decompose: assumes "ws ∈ lists {x,y}" and "x ≠ y" and "count_list ws y = 1"
obtains k m where "[x]⇧@k ⋅ [y] ⋅ [x]⇧@m = ws"
proof-
have "ws ∉ [x]*"
using count_sing_distinct[OF ‹x ≠ y›] ‹count_list ws y = 1› unfolding root_def by force
from distinct_letter_in[OF this]
obtain ws' k b where "[x]⇧@k ⋅ [b] ⋅ ws' = ws" and "b ≠ x" by blast
hence "b = y"
using ‹ws ∈ lists {x,y}› by force
have "ws' ∈ lists {x,y}"
using ‹ws ∈ lists {x,y}›[folded ‹[x]⇧@k ⋅ [b] ⋅ ws' = ws›] by simp
have "count_list ws' y = 0"
using arg_cong[OF ‹[x]⇧@k ⋅ [b] ⋅ ws' = ws›, of "λ x. count_list x y"]
unfolding count_list_append ‹count_list ws y = 1› ‹b = y› by force
from sing_lists_exp[OF bin_lists_count_zero'[OF ‹ws' ∈ lists {x,y}› this]]
obtain m where "ws' = [x]⇧@m".
from that[OF ‹[x]⇧@k ⋅ [b] ⋅ ws' = ws›[unfolded this ‹b = y›]]
show thesis.
qed
lemma bin_count_one_conjug: assumes "ws ∈ lists {x,y}" and "x ≠ y" and "count_list ws y = 1"
shows "ws ∼ [x]⇧@(count_list ws x) ⋅ [y]"
proof-
obtain e1 e2 where "[x]⇧@e1 ⋅ [y] ⋅ [x]⇧@e2 = ws"
using bin_count_one_decompose[OF assms].
from conjugI'[of "[x] ⇧@ e1 ⋅ [y]" "[x]⇧@e2", unfolded rassoc this]
have "ws ∼ [x]⇧@(e2 + e1) ⋅ [y]"
unfolding add_exps rassoc.
moreover have "count_list ([x]⇧@(e2 + e1) ⋅ [y]) x = e2 + e1"
using ‹x ≠ y› by simp
ultimately show ?thesis
by (simp add: count_list_conjug)
qed
lemma bin_prim_long_set: assumes "ws ∈ lists {x,y}" and "primitive ws" and "2 ≤ ❙|ws❙|"
shows "set ws = {x,y}"
proof-
have "¬ set ws ⊆ {c}" for c
using ‹primitive ws› pow_nemp_imprim ‹2 ≤ ❙|ws❙|›
sing_lists_exp_len[folded in_lists_conv_set_subset] by metis
then show "set ws = {x,y}"
unfolding subset_singleton_iff using ‹ws ∈ lists {x,y}›[folded in_lists_conv_set_subset] doubleton_subset_cases by metis
qed
lemma bin_prim_long_pref: assumes "ws ∈ lists {x,y}" and "primitive ws" and "2 ≤ ❙|ws❙|"
obtains ws' where "ws ∼ ws'" and "[x,y] ≤p ws'"
proof-
from pow_nemp_imprim[OF ‹2 ≤ ❙|ws❙|›, of "[x]"] sing_lists_exp_len[of ws x]
have "¬ ws ∈ lists {x}"
using ‹primitive ws› ‹2 ≤ ❙|ws❙|› by fastforce
hence "x ≠ y"
using ‹ws ∈ lists {x,y}› by fastforce
from switch_fac[OF ‹x ≠ y› bin_prim_long_set[OF assms]]
show thesis
using ‹2 ≤ ❙|ws❙|› rotate_into_pos_sq[of ε "[x,y]" ws thesis, unfolded emp_simps, OF ‹[x, y] ≤f ws ⋅ ws› _ _ that, of id]
by force
qed
end