Theory Morphisms
theory Morphisms
imports CoWBasic Submonoids
begin
chapter "Morphisms"
section ‹One morphism›
subsection ‹Morphism, core map and extension›
definition list_extension :: "('a ⇒ 'b list) ⇒ ('a list ⇒ 'b list)" ("_⇧ℒ" [1000] 1000)
where "t⇧ℒ ≡ (λ x. concat (map t x))"
definition morphism_core :: "('a list ⇒ 'b list) ⇒ ('a ⇒ 'b list)" ("_⇧𝒞" [1000] 1000)
where core_def: "f⇧𝒞 ≡ (λ x. f [x])"
lemma core_sing: "f⇧𝒞 a = f [a]"
unfolding core_def..
lemma range_map_core: "range (map f⇧𝒞) = lists (range f⇧𝒞)"
using lists_image[of "λx. f [x]" UNIV, folded core_def, symmetric]
unfolding lists_UNIV.
lemma map_core_lists: "(map f⇧𝒞 w) ∈ lists (range f⇧𝒞)"
by auto
lemma comp_core: "(f ∘ g)⇧𝒞 = f ∘ g⇧𝒞"
unfolding core_def
by auto
locale morphism_on =
fixes f :: "'a list ⇒ 'b list" and A :: "'a list set"
assumes morph_on: "u ∈ ⟨A⟩ ⟹ v ∈ ⟨A⟩ ⟹ f (u ⋅ v) = f u ⋅ f v"
begin
lemma emp_to_emp[simp]: "f ε = ε"
using morph_on[of ε ε] self_append_conv2[of "f ε" "f ε"] by simp
lemma emp_to_emp': "w = ε ⟹ f w = ε"
using morph_on[of ε ε] self_append_conv2[of "f ε" "f ε"] by simp
lemma morph_concat_concat_map: "ws ∈ lists ⟨A⟩ ⟹ f (concat ws) = concat (map f ws)"
by (induct ws, simp_all add: morph_on hull_closed_lists)
lemma hull_im_hull:
shows "⟨f ` A⟩ = f ` ⟨A⟩"
proof
show " ⟨f ` A⟩ ⊆ f ` ⟨A⟩"
proof (rule subsetI)
fix x
show "x ∈ ⟨f ` A⟩ ⟹ x ∈ f ` ⟨A⟩"
proof (induction rule: hull.induct)
show "ε ∈ f ` ⟨A⟩"
using hull.emp_in emp_to_emp by force
show "w1 ⋅ w2 ∈ f ` ⟨A⟩" if "w1 ∈ f ` A" and "w2 ∈ f ` ⟨A⟩" for w1 w2
proof-
from that
obtain pre1 pre2 where "pre1 ∈ ⟨A⟩" and "pre2 ∈ ⟨A⟩" and "f pre1 = w1" and "f pre2 = w2"
using imageE by blast+
from hull_closed[OF this(1-2)] morph_on[OF ‹pre1 ∈ ⟨A⟩› ‹pre2 ∈ ⟨A⟩›, unfolded this(3-4)]
show "w1 ⋅ w2 ∈ f ` ⟨A⟩"
by force
qed
qed
qed
show "f ` ⟨A⟩ ⊆ ⟨f ` A⟩"
proof
fix x
assume "x ∈ f ` ⟨A⟩"
then obtain xs where "f (concat xs) = x" and "xs ∈ lists A"
using hull_concat_lists0 by blast
from this[unfolded morph_concat_concat_map]
morph_concat_concat_map[OF genset_sub_lists[OF this(2)]]
show "x ∈ ⟨f ` A⟩"
by fastforce
qed
qed
lemma inj_basis_to_basis: assumes "inj_on f ⟨A⟩"
shows "f ` (𝔅 ⟨A⟩) = 𝔅 (f`⟨A⟩)"
proof
interpret basis: morphism_on f "𝔅 ⟨A⟩"
by (rule morph_on morphism_on.intro, unfold basis_gen_hull'[of A])
(simp only: morph_on)
show "𝔅 (f ` ⟨A⟩) ⊆ f ` 𝔅 ⟨A⟩"
using basis.hull_im_hull unfolding basis_gen_hull unfolding self_gen using basis_hull_sub[of "f ` 𝔅 ⟨A⟩"] by argo
show "f ` 𝔅 ⟨A⟩ ⊆ 𝔅 (f ` ⟨A⟩)"
proof
fix x
assume "x ∈ f ` 𝔅 ⟨A⟩"
then obtain y where "y ∈ 𝔅 ⟨A⟩" and "x = f y" by blast
hence "x ∈ f ` ⟨A⟩"
using basis_sub by blast
from basis_concat_listsE[OF this]
obtain xs where "xs ∈ lists 𝔅 (f `⟨A⟩)" and "concat xs = x".
hence "ε ∉ set xs"
using emp_not_basis by blast
have "xs ∈ lists (f `⟨A⟩)"
using ‹xs ∈ lists 𝔅 (f `⟨A⟩)› basis_sub by blast
then obtain ys where "map f ys = xs" and "ys ∈ lists ⟨A⟩"
unfolding lists_image by blast
have "ε ∉ set ys"
using emp_to_emp ‹ε ∉ set xs›
imageI[of ε "set ys" f] unfolding list.set_map[of f ys, unfolded ‹map f ys = xs›] by presburger
hence "ys ∈ lists (⟨A⟩ - {ε}) "
using ‹ys ∈ lists ⟨A⟩› by fast
have "f (concat ys) = x"
unfolding morph_concat_concat_map[OF ‹ys ∈ lists ⟨A⟩›] ‹map f ys = xs› by fact
from ‹inj_on f ⟨A⟩› this[unfolded ‹x = f y›]
have "concat ys = y"
unfolding inj_on_def using subsetD[OF basis_sub ‹y ∈ 𝔅 ⟨A⟩›] hull_closed_lists[OF ‹ys ∈ lists ⟨A⟩›] by blast
hence "❙|ys❙| = 1"
using ‹y ∈ 𝔅 ⟨A⟩› ‹ys ∈ lists (⟨A⟩ - {ε})› unfolding basis_def simple_element_def mem_Collect_eq by fast
hence "❙|xs❙| = 1"
using ‹map f ys = xs› by fastforce
with ‹concat xs = x› ‹xs ∈ lists 𝔅 (f `⟨A⟩)›
show "x ∈ 𝔅 (f ` ⟨A⟩)"
using len_one_concat_in by blast
qed
qed
lemma inj_code_to_code: assumes "inj_on f ⟨A⟩" and "code A"
shows "code (f ` A)"
proof
fix xs ys
assume "xs ∈ lists (f ` A)" and "ys ∈ lists (f ` A)"
then obtain xs' ys' where "xs' ∈ lists A" and "map f xs' = xs" and "ys' ∈ lists A" and "map f ys' = ys"
unfolding lists_image by blast
assume "concat xs = concat ys"
hence "f (concat xs') = f (concat ys')"
by (simp add: ‹map f xs' = xs› ‹map f ys' = ys› ‹xs' ∈ lists A› ‹ys' ∈ lists A› genset_sub_lists morph_concat_concat_map)
hence "concat xs' = concat ys'"
using ‹inj_on f ⟨A⟩›[unfolded inj_on_def] ‹xs' ∈ lists A› ‹ys' ∈ lists A› by auto
hence "xs' = ys'"
using ‹code A›[unfolded code_def] ‹xs' ∈ lists A› ‹ys' ∈ lists A› by simp
thus "xs = ys"
using ‹map f xs' = xs› ‹map f ys' = ys› by blast
qed
end
locale morphism =
fixes f :: "'a list ⇒ 'b list"
assumes morph: "f (u ⋅ v) = f u ⋅ f v"
begin
sublocale morphism_on f UNIV
by (simp add: morph morphism_on.intro)
lemma map_core_lists[simp]: "map f⇧𝒞 xs ∈ lists (range f⇧𝒞)"
by auto
lemma pow_morph: "f (x⇧@k) = (f x)⇧@k"
by (induction k) (simp add: morph)+
lemma rev_map_pow: "(rev_map f) (w⇧@n) = rev ((f (rev w))⇧@n)"
by (simp add: pow_morph rev_map_arg rev_pow)
lemma pop_hd: "f (a#u) = f [a] ⋅ f u"
unfolding hd_word[of a u] using morph.
lemma pop_hd_nemp: "u ≠ ε ⟹ f (u) = f [hd u] ⋅ f (tl u)"
using list.exhaust_sel pop_hd[of "hd u" "tl u"] by force
lemma pop_last_nemp: "u ≠ ε ⟹ f (u) = f (butlast u) ⋅ f [last u]"
unfolding morph[symmetric] append_butlast_last_id ..
lemma pref_mono: "u ≤p v ⟹ f u ≤p f v"
using morph by (auto simp add: prefix_def)
lemma suf_mono: "u ≤s v ⟹ f u ≤s f v"
using morph by (auto simp add: suffix_def)
lemma morph_concat_map: "concat (map f⇧𝒞 x) = f x"
unfolding core_def
proof (induction x)
case (Cons a x)
then show ?case
unfolding pop_hd[of a x] by auto
qed simp
lemma morph_concat_map': "(λ x. concat (map f⇧𝒞 x)) = f"
using morph_concat_map by simp
lemma morph_to_concat:
obtains xs where "xs ∈ lists (range f⇧𝒞)" and "f x = concat xs"
proof-
have "map f⇧𝒞 x ∈ lists (range f⇧𝒞)"
by fastforce
from that[OF this morph_concat_map[symmetric]]
show thesis.
qed
lemma range_hull: "range f = ⟨(range f⇧𝒞)⟩"
using arg_cong[OF range_map_core[of f], of "image concat", unfolded image_comp, folded hull_concat_lists] morph_concat_map by auto
lemma im_in_hull: "f w ∈ ⟨(range f⇧𝒞)⟩"
using range_hull by blast
lemma core_ext_id: "f⇧𝒞⇧ℒ = f"
using morph_concat_map unfolding list_extension_def core_def by simp
lemma rev_map_morph: "morphism (rev_map f)"
by (standard, auto simp add: rev_map_def morph)
lemma morph_rev_len: "❙|f (rev u)❙| = ❙|f u❙|"
proof (induction u)
case (Cons a u)
then show ?case
unfolding rev.simps(2) pop_hd[of a u] morph lenmorph by force
qed simp
lemma rev_map_len: "❙|rev_map f u❙| = ❙|f u❙|"
unfolding rev_map_def
by (simp add: morph_rev_len)
lemma in_set_morph_len: assumes "a ∈ set w" shows "❙|f [a]❙| ≤ ❙|f w❙|"
proof-
from split_listE[OF assms]
obtain p s where "w = p ⋅ [a] ⋅ s".
from lenarg[OF arg_cong[of _ _ f, OF this], unfolded morph lenmorph]
show ?thesis by linarith
qed
lemma morph_lq_comm: "u ≤p v ⟹ f (u¯⇧>v) = (f u)¯⇧>(f v)"
using morph by (auto simp add: prefix_def)
lemma morph_rq_comm: assumes "v ≤s u"
shows "f (u⇧<¯v) = (f u)⇧<¯(f v)"
using arg_cong[OF rq_suf[OF ‹v ≤s u›], of f, unfolded morph, THEN rqI, symmetric].
lemma code_set_morph: assumes c: "code (f⇧𝒞 `(set (u ⋅ v)))" and i: "inj_on f⇧𝒞 (set (u ⋅ v))"
and "f u = f v"
shows "u = v"
proof-
let ?C = "f⇧𝒞 `(set (u ⋅ v))"
interpret code ?C
using c by blast
have "(map f⇧𝒞 u) ∈ lists ?C" and "(map f⇧𝒞 v) ∈ lists ?C"
by (simp_all add: in_listsI)
from is_code[OF this ‹f u = f v›[folded morph_concat_map]]
show "u = v"
using inj_on_map_lists[OF i] unfolding inj_on_def
by (simp add: in_listsI)
qed
lemma morph_concat_concat_map: "f (concat ws) = concat (map f ws)"
by (induct ws, simp_all add: morph)
lemma morph_on: "morphism_on f A"
unfolding morphism_on_def using morph by blast
lemma noner_sings_conv: "(∀ w. w = ε ⟷ f w = ε) ⟷ (∀ a. f [a] ≠ ε)"
by (rule iffI, blast)
(metis Nil_is_append_conv emp_to_emp' hd_tlE pop_hd)
lemma fac_mono: "u ≤f w ⟹ f u ≤f f w"
using morph by fastforce
lemma set_core_set: "set (f w) = ⋃ (set ` f⇧𝒞 ` (set w))"
unfolding list.set_map[symmetric]
unfolding image_set[of set "(map f⇧𝒞 w)", symmetric]
unfolding morph_concat_map[symmetric, of w]
using set_concat.
end
lemma morph_map: "morphism (map f)"
by (simp add: morphism_def)
lemma list_ext_morph: "morphism t⇧ℒ"
unfolding list_extension_def by (simp add: morphism_def)
lemma ext_def_on_set: "(⋀ a. a ∈ set u ⟹ g a = f a) ⟹ g⇧ℒ u = f⇧ℒ u"
unfolding list_extension_def using map_ext by metis
lemma morph_def_on_set: "morphism f ⟹ morphism g ⟹ (⋀ a. a ∈ set u ⟹ g⇧𝒞 a = f⇧𝒞 a) ⟹ g u = f u"
using ext_def_on_set morphism.core_ext_id by metis
lemma morph_compose: "morphism f ⟹ morphism g ⟹ morphism (f ∘ g)"
by (simp add: morphism_def)
subsection ‹Periodic morphism›
locale periodic_morphism = morphism +
assumes ims_comm: "⋀ u v. f u ⋅ f v = f v ⋅ f u" and
not_triv_emp: "¬ (∀ c. f [c] = ε)"
begin
lemma per_morph_root_ex:
"∃ r. ∀ u. ∃ n. f u = r⇧@n ∧ primitive r"
proof-
obtain c root n where "f[c] = root⇧@n" and "root = ρ (f [c])" and "f [c] ≠ ε"
using primroot_expE not_triv_emp by metis
have "∃ n. f u = root⇧@n" for u
using comm_primroot_exp[OF ‹f [c] ≠ ε›, OF ims_comm, folded ‹root = ρ (f [c])›] by metis
thus ?thesis
using ‹root = ρ (f [c])› ‹f [c] ≠ ε› by auto
qed
definition mroot where "mroot ≡ (SOME r. (∀ u. ∃ n. f u = r⇧@n) ∧ primitive r)"
definition mexp :: "'a ⇒ nat" where "mexp c ≡ (SOME n. f [c] = mroot⇧@n)"
lemma per_morph_rootI: "∀ u. ∃ n. f u = mroot⇧@n" and
per_morph_root_prim: "primitive mroot"
using per_morph_root_ex exE_some[of "λ r. ∀u. ∃n. f u = r ⇧@ n ∧ primitive r", of mroot]
unfolding mroot_def by auto
lemma per_morph_expI': "f [c] = mroot⇧@(mexp c)"
using per_morph_rootI exE_some[of "λ n. f [c] = mroot ⇧@ n", of "mexp c"]
unfolding mexp_def by blast
lemma per_morph_expE:
obtains n where "f u = mroot⇧@n"
using per_morph_rootI by auto
interpretation mirror: periodic_morphism "rev_map f"
proof
show "rev_map f (u ⋅ v) = rev_map f u ⋅ rev_map f v" for u v
using morphism.morph[OF rev_map_morph].
show "rev_map f u ⋅ rev_map f v = rev_map f v ⋅ rev_map f u" for u v
unfolding comm_rev_iff ims_comm rev_map_arg..
show "¬ (∀c. rev_map f [c] = ε)"
using not_triv_emp unfolding rev_map_sing by blast
qed
lemma mroot_rev: "mirror.mroot = rev mroot"
proof-
have "primitive (rev mroot)"
using per_morph_root_prim prim_rev_iff by blast
obtain u where "f u ≠ ε"
using not_triv_emp by auto
obtain n where "f u = mroot⇧@n"
using per_morph_expE[of u].
hence "0 < n"
using ‹f u ≠ ε› by blast
obtain n' where "rev (f u) = mirror.mroot⇧@n'" "0 < n'"
using mirror.per_morph_expE rev_map_arg_rev
‹f u ≠ ε›[folded Nil_is_rev_conv, symmetric]
using bot_nat_0.not_eq_extremum zero_exp by metis
from this(1)[unfolded ‹f u = mroot⇧@ n›, unfolded rev_pow]
have *: "rev mroot ⇧@ n = mirror.mroot ⇧@ n'".
have "(rev mroot) ⋅ mirror.mroot = mirror.mroot ⋅ (rev mroot)"
by (rule comm_drop_exps[OF _ ‹0 < n› ‹0 < n'›]) (use * in blast)
thus ?thesis
using comm_prim[OF ‹primitive (rev mroot)› mirror.per_morph_root_prim] by force
qed
end
subsection ‹Non-erasing morphism›
locale nonerasing_morphism = morphism +
assumes nonerasing: "f w = ε ⟹ w = ε"
begin
lemma core_nemp: "f⇧𝒞 a ≠ ε"
unfolding core_def using nonerasing not_Cons_self2 by blast
lemma nemp_to_nemp: "w ≠ ε ⟹ f w ≠ ε"
using nonerasing by blast
lemma sing_to_nemp: "f [a] ≠ ε"
by (simp add: nemp_to_nemp)
lemma pref_morph_pref_eq: "u ≤p v ⟹ f v ≤p f u ⟹ u = v"
using nonerasing morph[of u "u¯⇧>v"] unfolding prefix_def by fastforce
lemma comm_eq_im_eq:
"u ⋅ v = v ⋅ u ⟹ f u = f v ⟹ u = v"
by (elim ruler_eqE)
(simp_all add: pref_morph_pref_eq pref_morph_pref_eq[symmetric])
lemma comm_eq_im_iff :
assumes "u ⋅ v = v ⋅ u"
shows "f u = f v ⟷ u = v"
using comm_eq_im_eq[OF ‹u ⋅ v = v ⋅ u›] by blast
lemma rev_map_nonerasing: "nonerasing_morphism (rev_map f)"
proof
show "rev_map f (u ⋅ v) = rev_map f u ⋅ rev_map f v" for u v
by (simp add: morphism.morph rev_map_morph)
show "rev_map f w = ε ⟹ w = ε" for w
unfolding rev_map_arg using rev_is_Nil_conv nonerasing by fast
qed
lemma first_of_first: "(f (a # ws))!0 = f [a]!0"
unfolding pop_hd[of a ws] using hd_prod[of "f[a]" "f ws", OF
nonerasing[of "[a]", THEN contrapos_nn[OF not_Cons_self2[of a ε], of ‹f (a # ε) = ε›]]].
lemma hd_im_hd_hd: assumes "u ≠ ε" shows "hd (f u) = hd (f [hd u])"
unfolding hd_append2[OF sing_to_nemp] pop_hd_nemp[OF ‹u ≠ ε›]..
lemma ssuf_mono: "u <s v ⟹ f u <s f v"
by (elim strict_suffixE')
(use morph sing_to_nemp ssufI1 suf_nemp in metis)
lemma im_len_le: "❙|u❙| ≤ ❙|f u❙|"
proof (induct u)
case (Cons a u)
show ?case
unfolding hd_word[of a u] morph lenmorph sing_len
by (rule add_mono[OF _ ‹❙|u❙| ≤ ❙|f u❙|›], use nemp_le_len[OF sing_to_nemp] in force)
qed simp
lemma im_len_eq_iff: "❙|u❙| = ❙|f u❙| ⟷ (∀ c. c ∈ set u ⟶ ❙|f [c]❙| = 1)"
proof (induct u)
case (Cons a u)
show ?case
proof
assume "❙|a # u❙| = ❙|f (a # u)❙|"
from this[unfolded hd_word[of a u] morph lenmorph sing_len]
have "❙|f [a]❙| = 1" and "❙|u❙| = ❙|f u❙|"
unfolding sing_len[of a, symmetric] using im_len_le[of "[a]"] im_len_le[of u] by auto
from this(2)[unfolded Cons.hyps] this(1)
show "∀c. c ∈ set (a # u) ⟶ ❙|f [c]❙| = 1" by auto
next
assume "∀c. c ∈ set (a # u) ⟶ ❙|f [c]❙| = 1"
hence all: "∀c. c ∈ set u ⟶ ❙|f [c]❙| = 1" and "❙|f [a]❙| = 1"
by simp_all
show "❙|a # u❙| = ❙|f (a # u)❙|"
unfolding hd_word[of a u] morph lenmorph sing_len ‹❙|f [a]❙| = 1› all[folded Cons.hyps]..
qed
qed simp
lemma im_len_less: "a ∈ set u ⟹ ❙|f [a]❙| ≠ 1 ⟹ ❙|u❙| < ❙|f u❙|"
using im_len_le im_len_eq_iff order_le_neq_trans by auto
end
lemma (in morphism) nonerI[intro]: assumes "(⋀ a. f⇧𝒞 a ≠ ε)"
shows "nonerasing_morphism f"
proof
from assms[unfolded core_def] noner_sings_conv
show "⋀w. f w = ε ⟹ w = ε" by presburger
qed
lemma (in morphism) prim_morph_noner:
assumes prim_morph: "⋀u. 2 ≤ ❙|u❙| ⟹ primitive u ⟹ primitive (f u)"
and non_single_dom: "∃a b :: 'a. a ≠ b"
shows "nonerasing_morphism f"
proof (intro nonerI notI)
fix a
assume "f⇧𝒞 a = ε"
obtain c d :: "'a" where "c ≠ d"
using non_single_dom by blast
then obtain b where "a ≠ b"
by (cases "a = c") simp_all
then have "¬ primitive (f ([a] ⋅ [b] ⋅ [b]))"
using ‹f⇧𝒞 a = ε› unfolding morph
by (simp add: core_def eq_append_not_prim)
have "primitive ([a] ⋅ [b] ⋅ [b])"
using prim_abk[OF ‹a ≠ b›, of 2] by simp
from prim_morph[OF _ this] ‹¬ primitive (f ([a] ⋅ [b] ⋅ [b]))›
show False
by simp
qed
subsection ‹Code morphism›
text ‹The term ``Code morphism'' is equivalent to ``injective morphism''.›
text ‹Note that this is not equivalent to @{term "code (range f⇧𝒞)"}, since the core can be not injective.›
lemma (in morphism) code_core_range_inj: "inj f ⟷ code (range f⇧𝒞) ∧ inj f⇧𝒞"
proof
assume "inj f"
show "code (range f⇧𝒞) ∧ inj f⇧𝒞"
proof
show "inj f⇧𝒞"
using ‹inj f› unfolding inj_on_def core_def by blast
show "code (range f⇧𝒞)"
proof
show
"xs ∈ lists (range f⇧𝒞) ⟹ ys ∈ lists (range f⇧𝒞) ⟹ concat xs = concat ys ⟹ xs = ys" for xs ys
unfolding range_map_core[symmetric] using ‹inj f›[unfolded inj_on_def core_def] morph_concat_map
by force
qed
qed
next
assume "code (range f⇧𝒞) ∧ inj f⇧𝒞" hence "code (range f⇧𝒞)" and "inj f⇧𝒞" by blast+
show "inj f"
proof
fix x y assume "f x = f y"
with code.is_code[OF ‹code (range f⇧𝒞)›, folded range_map_core, OF rangeI rangeI, unfolded morph_concat_map]
have "map f⇧𝒞 x = map f⇧𝒞 y" by blast
with ‹inj f⇧𝒞›
show "x = y" by simp
qed
qed
locale code_morphism = morphism f for f +
assumes code_morph: "inj f"
begin
lemma inj_core: "inj f⇧𝒞"
using code_morph unfolding core_def inj_on_def by blast
lemma sing_im_core: "f [a] ∈ (range f⇧𝒞)"
unfolding core_def by simp
lemma code_im: "code (range f⇧𝒞)"
using code_morph morph_concat_map unfolding inj_on_def code_def core_def
unfolding lists_image lists_UNIV by fastforce
sublocale code "range f⇧𝒞"
using code_im.
sublocale nonerasing_morphism
by (rule nonerI, simp add: nemp)
lemma code_morph_code: assumes "f r = f s" shows "r = s"
proof-
from code.is_code[OF code_im, of "map f⇧𝒞 r" "map f⇧𝒞 s"]
have "map f⇧𝒞 r = map f⇧𝒞 s"
unfolding morph_concat_map using range_map_core assms by blast
thus "r = s"
unfolding inj_map_eq_map[OF inj_core].
qed
lemma code_morph_bij: "bij_betw f UNIV ⟨(range f⇧𝒞)⟩"
unfolding bij_betw_def
by (rule disjE, simp_all add: range_hull)
(rule injI, simp add: code_morph_code)
lemma code_morphism_rev_map: "code_morphism (rev_map f)"
unfolding code_morphism_def code_morphism_axioms_def
proof (rule conjI)
show "inj (rev_map f)"
using code_morph
unfolding inj_def rev_map_arg rev_is_rev_conv
using rev_is_rev_conv by blast
qed (simp add: rev_map_morph)
lemma morph_on_inj_on:
"morphism_on f A" "inj_on f A"
using morph code_morph_code unfolding morphism_on_def inj_on_def
by blast+
end
lemma (in morphism) code_morphismI: "inj f ⟹ code_morphism f"
by unfold_locales
lemma (in nonerasing_morphism) code_morphismI' :
assumes comm: "⋀u v. f u = f v ⟹ u ⋅ v = v ⋅ u"
shows "code_morphism f"
proof (unfold_locales, intro injI)
fix u v
assume "f u = f v"
then have "u ⋅ v = v ⋅ u"
by (fact comm)
from comm_eq_im_eq[OF this ‹f u = f v›]
show "u = v".
qed
subsection ‹Prefix code morphism›
locale pref_code_morphism = nonerasing_morphism +
assumes
pref_free: "f⇧𝒞 a ≤p f⇧𝒞 b ⟹ a = b"
begin
interpretation prefrange: pref_code "(range f⇧𝒞)"
by (unfold_locales, unfold image_iff)
(use core_nemp in metis, use pref_free in fast)
lemma inj_core: "inj f⇧𝒞"
unfolding inj_on_def using pref_free by force
sublocale code_morphism
proof
show "inj f"
proof (rule injI)
fix x y
assume "f x = f y"
hence "map f⇧𝒞 x = map f⇧𝒞 y"
using prefrange.is_code[folded range_map_core, of "map f⇧𝒞 x" "map f⇧𝒞 y"]
unfolding morph_concat_map by fast
with inj_core[folded inj_map[of "f⇧𝒞"], unfolded inj_on_def]
show "x = y"
by fast
qed
qed
thm nonerasing
lemma pref_free_morph: assumes "f r ≤p f s" shows "r ≤p s"
using assms
proof (induction r s rule: list_induct2')
case (2 x xs)
then show ?case
using emp_to_emp nonerasing prefix_bot.extremum_unique by auto
next
case (3 y ys)
then show ?case
using emp_to_emp nonerasing prefix_bot.extremum_unique by blast
next
case (4 x xs y ys)
then show ?case
proof-
have "f⇧𝒞 x ≤p f⇧𝒞 y ⋅ f ys"
unfolding core_def using "4.prems"[unfolded pop_hd[of x xs] pop_hd[of y ys], THEN append_prefixD].
from ruler_pref'[OF this] prefrange.pref_free[OF rangeI rangeI] inj_core
have "x = y"
unfolding inj_on_def by fastforce
show ?case
using "4.IH" "4.prems" unfolding pop_hd[of x xs] pop_hd[of y ys]
unfolding ‹x = y› by fastforce
qed
qed simp
end
subsection ‹Marked morphism›
locale marked_morphism = nonerasing_morphism +
assumes
marked_core: "hd (f⇧𝒞 a) = hd (f⇧𝒞 b) ⟹ a = b"
begin
lemma marked_im: "marked_code (range f⇧𝒞)"
by (unfold_locales, unfold image_iff)
(use marked_core core_nemp in metis)+
interpretation marked_code "(range f⇧𝒞)"
using marked_im.
lemmas marked_morph = marked_core[unfolded core_sing]
sublocale pref_code_morphism
by (unfold_locales, simp_all add: core_nemp marked_core pref_hd_eq)
lemma hd_im_eq_hd_eq: assumes "u ≠ ε" and "v ≠ ε" and "hd (f u) = hd (f v)"
shows "hd u = hd v"
using marked_morph[OF ‹hd (f u) = hd (f v)›[unfolded hd_im_hd_hd[OF ‹u ≠ ε›] hd_im_hd_hd[OF ‹v ≠ ε›]]].
lemma marked_morph_lcp: "f (r ∧⇩p s) = f r ∧⇩p f s"
by (rule marked_concat_lcp[of "map f⇧𝒞 r" "map f⇧𝒞 s", unfolded map_lcp_conv[OF inj_core] morph_concat_map]) simp_all
lemma marked_inj_map: "inj e ⟹ marked_morphism ((map e) ∘ f)"
unfolding inj_on_def
by unfold_locales
(simp add: morph, simp add: code_morph_code, simp add: core_def core_nemp nemp_to_nemp marked_core list.map_sel(1) sing_to_nemp)
end
thm morphism.nonerI
lemma (in morphism) marked_morphismI:
"(⋀ a. f[a] ≠ ε) ⟹ (⋀ a b. a ≠ b) ⟹ hd (f[a]) ≠ hd (f[b]) ⟹ marked_morphism f"
by unfold_locales presburger+
subsection "Image length"
definition max_image_length:: "('a list ⇒ 'b list) ⇒ nat" ("⌈_⌉")
where "max_image_length f = Max (length`(range f⇧𝒞))"
definition min_image_length::"('a list ⇒ 'b list) ⇒ nat" ("⌊_⌋" )
where "min_image_length f = Min (length`(range f⇧𝒞))"
lemma max_im_len_id: "⌈id::('a list ⇒ 'a list)⌉ = 1" and min_im_len_id: "⌊id::('a list ⇒ 'a list)⌋ = 1"
proof-
have a1: "length ` range (λx. [x]) = {1}"
by force
show "⌈id::('a list ⇒ 'a list)⌉ = 1" and "⌊id::('a list ⇒ 'a list)⌋ = 1"
unfolding max_image_length_def min_image_length_def core_def id_apply a1
by force+
qed
context morphism
begin
lemma max_im_len_le: "finite (length`range f⇧𝒞) ⟹ ❙|f z❙| ≤ ❙|z❙|*⌈f⌉"
proof(induction z)
case (Cons a z)
have "❙|f [a]❙| ∈ length`(range f⇧𝒞)"
by (simp add: core_def)
hence "❙|f [a]❙| ≤ ⌈f⌉"
unfolding max_image_length_def
using Cons.prems Max.coboundedI by metis
thus ?case
unfolding hd_word[of a z] morph[of "[a]" z]
unfolding lenmorph
using Cons.IH[OF Cons.prems] by auto
qed simp
lemma max_im_len_le_sing: assumes "finite (length`range f⇧𝒞)"
shows "❙|f [a]❙| ≤ ⌈f⌉"
using max_im_len_le[OF assms, of "[a]"]
unfolding mult_1 sing_len.
lemma min_im_len_ge: "finite (length`range f⇧𝒞) ⟹ ❙|z❙| * ⌊f⌋ ≤ ❙|f z❙|"
proof(induction z)
case (Cons a z)
have "❙|f [a]❙| ∈ length`(range f⇧𝒞)"
by (simp add: core_def)
hence "⌊f⌋ ≤ ❙|f [a]❙|"
unfolding min_image_length_def
by (meson Cons.prems Min_le)
thus ?case
unfolding hd_word[of a z] morph[of "[a]" z]
unfolding lenmorph
using Cons.IH[OF Cons.prems] by auto
qed simp
lemma max_im_len_comp_le: assumes finite_f: "finite (length`range f⇧𝒞)" and
finite_g: "finite (length`range g⇧𝒞)" and "morphism g"
shows "finite (length ` range (g ∘ f)⇧𝒞)" "⌈g ∘ f⌉ ≤ ⌈f⌉*⌈g⌉"
proof-
interpret mg: morphism g
by (simp add: ‹morphism g›)
have "❙|g (f [x])❙| ≤ ⌈f⌉*⌈g⌉" for x
proof-
have "❙|f [x]❙| ≤ ⌈f⌉"
using finite_f max_im_len_le_sing by presburger
thus "❙|g (f [x])❙| ≤ ⌈f⌉*⌈g⌉"
by (meson finite_g le_trans mg.max_im_len_le mult_le_cancel2)
qed
hence "❙|(g o f)⇧𝒞 x❙| ≤ ⌈f⌉*⌈g⌉" for x
by (simp add: core_sing)
hence "l ∈ length ` range (g ∘ f)⇧𝒞 ⟹ l ≤ ⌈f⌉*⌈g⌉" for l
by blast
thus "finite (length ` range (g ∘ f)⇧𝒞)"
using finite_nat_set_iff_bounded_le by metis
from Max.boundedI[OF this]
show "⌈g o f⌉ ≤ ⌈f⌉*⌈g⌉"
using ‹⋀l. l ∈ length ` range (g ∘ f)⇧𝒞 ⟹ l ≤ ⌈f⌉ * ⌈g⌉›
unfolding max_image_length_def
by blast
qed
lemma max_im_len_emp: assumes "finite (length ` range f⇧𝒞)"
shows "⌈f⌉ = 0 ⟷ (f = (λw. ε))"
by (rule iffI, use max_im_len_le[OF assms] npos_len in force, simp add: core_def max_image_length_def)
lemmas max_im_len_le_dom = max_im_len_le[OF finite_imageI, OF finite_imageI] and
max_im_len_le_sing_dom = max_im_len_le_sing[OF finite_imageI, OF finite_imageI] and
min_im_len_ge_dom = min_im_len_ge[OF finite_imageI, OF finite_imageI] and
max_im_len_comp_le_dom = max_im_len_comp_le[OF finite_imageI, OF finite_imageI] and
max_im_len_emp_dom = max_im_len_emp[OF finite_imageI, OF finite_imageI]
end
subsection "Endomorphism"
locale endomorphism = morphism f for f:: "'a list ⇒ 'a list"
begin
lemma pow_endomorphism: "endomorphism (f^^k)"
by (unfold_locales, induction k) (simp_all add: power.power.power_0 morph)
interpretation pow_endm: endomorphism "(f^^k)"
using pow_endomorphism by blast
lemmas pow_morphism = pow_endm.morphism_axioms and
pow_morph = pow_endm.morph and
pow_emp_to_emp = pow_endm.emp_to_emp
lemma pow_sets_im: "set w = set v ⟹ set ((f^^k) w) = set ((f^^k) v)"
by(induct k, auto simp add: power.power.power_0 set_core_set)
lemma fin_len_ran_pow: "finite (length ` range f⇧𝒞) ⟹ finite (length ` range (f^^k)⇧𝒞)"
proof(induction k)
case 0
have "(w::'a list) ∈ range (λa. [a]) ⟹ ❙|w❙| = 1" for w
by force
thus ?case
unfolding funpow_0 core_def
using finite_nat_set_iff_bounded_le by auto
next
case (Suc k)
show ?case
using pow_endm.max_im_len_comp_le(1)[of _ f, folded funpow.simps(2), OF Suc.IH, OF Suc.prems Suc.prems morphism_axioms].
qed
lemma max_im_len_pow_le: assumes "finite (length ` range f⇧𝒞)" shows "⌈f^^k⌉ ≤ ⌈f⌉^k"
proof(induction k)
have funpow_1: "f^^1 = f" by simp
case (Suc k)
show ?case
using mult_le_mono2[OF Suc.IH[OF Suc.prems], of "⌈f ^^ 1⌉"] pow_endm.max_im_len_comp_le(2)[OF fin_len_ran_pow, OF ‹finite (length ` range f⇧𝒞)› ‹finite (length ` range f⇧𝒞)› morphism_axioms]
unfolding compow_Suc funpow_1 comp_apply
unfolding power_class.power.power_Suc
unfolding mult.commute[of "⌈f⌉"]
using dual_order.trans by blast
qed (simp add: max_im_len_id[unfolded id_def])
lemma max_im_len_pow_le': "finite (length ` range f⇧𝒞) ⟹ ❙|(f^^k) w❙| ≤ ❙|w❙| * ⌈f⌉^k"
using fin_len_ran_pow le_trans max_im_len_pow_le mult_le_mono2 pow_endm.max_im_len_le by meson
lemmas max_im_len_pow_le_dom = max_im_len_pow_le[OF finite_imageI, OF finite_imageI] and
max_im_len_pow_le'_dom = max_im_len_pow_le'[OF finite_imageI, OF finite_imageI]
lemma funpow_nonerasing_morphism: assumes "nonerasing_morphism f"
shows "nonerasing_morphism (f^^k)"
proof(unfold_locales, induction k)
case (Suc k)
then show ?case
using nonerasing_morphism.nonerasing[OF assms]
unfolding compow_Suc' by blast
qed simp
lemma im_len_pow_mono: assumes "nonerasing_morphism f" "i ≤ j"
shows "(❙|(f^^i) w❙| ≤ ❙|(f^^j) w❙|)"
using nonerasing_morphism.im_len_le[OF funpow_nonerasing_morphism[of "j-i"], OF ‹nonerasing_morphism f›, of "(f^^i) w"]
using funpow_add[unfolded comp_apply, of "j-i" i f]
unfolding diff_add[OF ‹i ≤ j›]
by simp
lemma fac_mono_pow: "u ≤f (f^^k) w ⟹ (f^^l) u ≤f (f^^(l+k)) w"
by (simp add: funpow_add pow_endm.fac_mono)
lemma rev_map_endomorph: "endomorphism (rev_map f)"
by (simp add: endomorphism.intro rev_map_morph)
end
section ‹Primitivity preserving morphisms›
locale primitivity_preserving_morphism = nonerasing_morphism +
assumes prim_morph : "2 ≤ ❙|u❙| ⟹ primitive u ⟹ primitive (f u)"
begin
sublocale code_morphism
proof (rule code_morphismI', rule nemp_comm)
fix u v
assume "u ≠ ε" and "v ≠ ε" and "f u = f v"
then have "2 ≤ ❙|u ⋅ v❙|" and "2 ≤ ❙|u ⋅ v ⋅ v❙|"
by (simp_all flip: len_nemp_conv)
moreover have "¬ primitive (f (u ⋅ v))" and "¬ primitive (f (u ⋅ v ⋅ v))"
using pow_nemp_imprim[of 2] pow_nemp_imprim[of 3] unfolding numeral_nat
by (simp_all add: morph ‹f u = f v›) assumption+
ultimately have "¬ primitive (u ⋅ v)" and "¬ primitive (u ⋅ v ⋅ v)"
by (intro notI; elim prim_morph[rotated, elim_format], blast+)+
then show "u ⋅ v = v ⋅ u"
by (fact imprim_ext_suf_comm)
qed
lemmas code_morph = code_morph
end
section ‹Two morphisms›
text ‹Solutions and the coincidence pairs are defined for any two mappings›
subsection ‹Solutions›
definition minimal_solution :: "'a list ⇒ ('a list ⇒ 'b list) ⇒ ('a list ⇒ 'b list) ⇒ bool"
("_ ∈ _ =⇩M _" [80,80,80] 51 )
where min_sol_def: "minimal_solution s g h ≡ s ≠ ε ∧ g s = h s
∧ (∀ s'. s' ≠ ε ∧ s' ≤p s ∧ g s' = h s' ⟶ s' = s)"
lemma min_solD: "s ∈ g =⇩M h ⟹ g s = h s"
using min_sol_def by blast
lemma min_solD': "s ∈ g =⇩M h ⟹ s ≠ ε"
using min_sol_def by blast
lemma min_solD_min: "s ∈ g =⇩M h ⟹ p ≠ ε ⟹ p ≤p s ⟹ g p = h p ⟹ p = s"
by (simp add: min_sol_def)
lemma min_solI[intro]: "s ≠ ε ⟹ g s = h s ⟹ (⋀ s'. s'≤p s ⟹ s' ≠ ε ⟹ g s' = h s' ⟹ s' = s) ⟹ s ∈ g =⇩M h"
using min_sol_def by metis
lemma min_sol_sym_iff: "s ∈ g =⇩M h ⟷ s ∈ h =⇩M g"
unfolding min_sol_def eq_commute[of "g _" "h _"] by blast
lemma min_sol_sym[sym]: "s ∈ g =⇩M h ⟹ s ∈ h =⇩M g"
unfolding min_sol_def eq_commute[of "g _"].
lemma min_sol_prefE:
assumes "g r = h r" and "r ≠ ε"
obtains e where "e ∈ g =⇩M h" and "e ≤p r"
proof-
let ?min = "λ n. take n r ≠ ε ∧ g (take n r) = h (take n r)"
have "?min ❙|r❙|"
using assms by force
define n where "n = (LEAST n. ?min n)"
define e where "e = take n r"
from Least_le[of ?min, folded n_def, OF ‹?min ❙|r❙|›]
have "n = ❙|e❙|"
unfolding e_def by simp
show thesis
proof (rule that)
show "e ≤p r"
unfolding e_def using take_is_prefix by blast
show "e ∈ g =⇩M h"
proof (rule min_solI)
from LeastI[of ?min, OF ‹?min ❙|r❙|›, folded n_def e_def]
show "e ≠ ε" and "g e = h e"
by blast+
show min: "s = e" if "s ≤p e" "s ≠ ε" "g s = h s" for s
proof-
have "❙|s❙| ≤ ❙|e❙|"
using pref_len[OF ‹s ≤p e›].
hence "take ❙|s❙| r = s"
using ‹s ≤p e› pref_take unfolding e_def by fastforce
from not_less_Least[of "❙|s❙|" ?min, folded e_def n_def, unfolded this]
show "s = e"
using that leI long_pref unfolding ‹n = ❙|e❙|› by fast
qed
qed
qed
qed
subsection ‹Coincidence pairs›
definition coincidence_set :: "('a list ⇒ 'b list) ⇒ ('a list ⇒ 'b list) ⇒ ('a list × 'a list) set" ("ℭ")
where "coincidence_set g h ≡ {(r,s). g r = h s}"
lemma coin_set_eq: "(g ∘ fst)`(ℭ g h) = (h ∘ snd)`(ℭ g h)"
unfolding coincidence_set_def comp_apply using Product_Type.Collect_case_prodD[of _ "λ x y. g x = h y"] image_cong by auto
lemma coin_setD: "pair ∈ ℭ g h ⟹ g (fst pair) = h (snd pair)"
unfolding coincidence_set_def by force
lemma coin_setD_iff: "pair ∈ ℭ g h ⟷ g (fst pair) = h (snd pair)"
unfolding coincidence_set_def by force
lemma coin_set_sym: "fst`(ℭ g h) = snd `(ℭ h g)"
unfolding coincidence_set_def
by (rule set_eqI) (auto simp add: image_iff, metis)
lemma coin_set_inter_fst: "(g ∘ fst)`(ℭ g h) = range g ∩ range h"
proof
show "(g ∘ fst) ` ℭ g h ⊆ range g ∩ range h"
proof
fix x assume "x ∈ (g ∘ fst) ` ℭ g h"
then obtain pair where "x = g (fst pair)" and "pair ∈ ℭ g h"
by force
from this(1)[unfolded coin_setD[OF this(2)]] this(1)
show "x ∈ range g ∩ range h" by blast
qed
next
show "range g ∩ range h ⊆ (g ∘ fst) ` ℭ g h"
proof
fix x assume "x ∈ range g ∩ range h"
then obtain r s where "g r = h s" and "x = g r" by blast
hence "(r,s) ∈ ℭ g h"
unfolding coincidence_set_def by blast
thus "x ∈ (g ∘ fst) ` ℭ g h"
unfolding ‹x = g r› by force
qed
qed
lemmas coin_set_inter_snd = coin_set_inter_fst[unfolded coin_set_eq]
definition minimal_coincidence :: "('a list ⇒ 'b list) ⇒ 'a list ⇒ ('a list ⇒ 'b list) ⇒ 'a list ⇒ bool" ("(_ _) =⇩m (_ _)" [80,81,80,81] 51 )
where min_coin_def: "minimal_coincidence g r h s ≡ r ≠ ε ∧ s ≠ ε ∧ g r = h s ∧ (∀ r' s'. r' ≤np r ∧ s' ≤np s ∧ g r' = h s' ⟶ r' = r ∧ s' = s)"
definition min_coincidence_set :: "('a list ⇒ 'b list) ⇒ ('a list ⇒ 'b list) ⇒ ('a list × 'a list) set" ("ℭ⇩m")
where "min_coincidence_set g h ≡ ({(r,s) . g r =⇩m h s})"
lemma min_coin_minD: "g r =⇩m h s ⟹ r' ≤np r ⟹ s' ≤np s ⟹ g r' = h s' ⟹ r' = r ∧ s' = s"
using min_coin_def by blast
lemma min_coin_setD: "p ∈ ℭ⇩m g h ⟹ g (fst p) =⇩m h (snd p)"
unfolding min_coincidence_set_def by force
lemma min_coinD: "g r =⇩m h s ⟹ g r = h s"
using min_coin_def by blast
lemma min_coinD': "g r =⇩m h s ⟹ r ≠ ε ∧ s ≠ ε"
using min_coin_def by blast
lemma min_coin_sub: "ℭ⇩m g h ⊆ ℭ g h"
unfolding coincidence_set_def min_coincidence_set_def
using min_coinD by blast
lemma min_coin_defI: assumes "r ≠ ε" and "s ≠ ε" and "g r = h s" and
"(⋀ r' s'. r' ≤np r ⟹ s' ≤np s ⟹ g r' = h s' ⟹ r' = r ∧ s' = s)"
shows "g r =⇩m h s"
unfolding min_coin_def[rule_format] using assms by blast
lemma min_coin_sym[sym]: "g r =⇩m h s ⟹ h s =⇩m g r"
unfolding min_coin_def eq_commute[of "g _" "h _"] by blast
lemma min_coin_sym_iff: "g r =⇩m h s ⟷ h s =⇩m g r"
using min_coin_sym by auto
lemma min_coin_set_sym: "fst`(ℭ⇩m g h) = snd `(ℭ⇩m h g)"
unfolding min_coincidence_set_def image_iff
by (rule set_eqI, rule iffI) (simp_all add: image_iff min_coin_sym_iff)
subsection ‹Basics›
locale two_morphisms = g: morphism g + h: morphism h for g h :: "'a list ⇒ 'b list"
begin
lemma def_on_sings:
assumes "⋀a. a ∈ set u ⟹ g [a] = h [a]"
shows "g u = h u"
using assms
proof (induct u)
next
case (Cons a u)
then show ?case
unfolding g.pop_hd[of a u] h.pop_hd[of a u] using assms by simp
qed simp
lemma def_on_sings_eq:
assumes "⋀a. g [a] = h [a]"
shows "g = h"
using def_on_sings[OF assms]
by (simp add: ext)
lemma ims_prefs_comp:
assumes "u ≤p u'" and "v ≤p v'" and "g u' ⨝ h v'" shows "g u ⨝ h v"
using ruler_comp[OF g.pref_mono h.pref_mono, OF assms].
lemma ims_sufs_comp:
assumes "u ≤s u'" and "v ≤s v'" and "g u' ⨝⇩s h v'" shows "g u ⨝⇩s h v"
using suf_ruler_comp[OF g.suf_mono h.suf_mono, OF assms].
lemma ims_hd_eq_comp:
assumes "u ≠ ε" and "g u = h u" shows "g [hd u] ⨝ h [hd u]"
using ims_prefs_comp[OF hd_pref[OF ‹u ≠ ε›] hd_pref[OF ‹u ≠ ε›]]
unfolding ‹g u = h u› by blast
lemma ims_last_eq_suf_comp:
assumes "u ≠ ε" and "g u = h u" shows "g [last u] ⨝⇩s h [last u]"
using ims_sufs_comp[OF hd_pref[reversed, OF ‹u ≠ ε›] hd_pref[reversed, OF ‹u ≠ ε›]]
unfolding ‹g u = h u› using comp_refl[reversed] by blast
lemma len_im_le:
assumes "(⋀a. a ∈ set s ⟹ ❙|g [a]❙| ≤ ❙|h [a]❙|)"
shows "❙|g s❙| ≤ ❙|h s❙|"
using assms proof (induction s)
case (Cons a s)
have IH_prem: "⋀a. a ∈ set s ⟹ ❙|g [a]❙| ≤ ❙|h [a]❙|" using Cons.prems by simp
show "❙|g (a # s)❙| ≤ ❙|h (a # s)❙|"
unfolding g.pop_hd[of _ s] h.pop_hd[of _ s] lenmorph
using Cons.prems[of a, simplified] Cons.IH[OF IH_prem]
by (rule add_le_mono)
qed simp
lemma len_im_less:
assumes "⋀a. a ∈ set s ⟹ ❙|g [a]❙| ≤ ❙|h [a]❙|" and
"b ∈ set s" and "❙|g [b]❙| < ❙|h [b]❙|"
shows "❙|g s❙| < ❙|h s❙|"
using assms proof (induction s arbitrary: b)
case (Cons a s)
have IH_prem: "⋀a. a ∈ set s ⟹ ❙|g [a]❙| ≤ ❙|h [a]❙|" using Cons.prems(1)[OF list.set_intros(2)].
note split = g.pop_hd[of _ s] h.pop_hd[of _ s] lenmorph
show "❙|g (a # s)❙| < ❙|h (a # s)❙|"
proof (cases)
assume "a = b" show "❙|g (a # s)❙| < ❙|h (a # s)❙|"
unfolding split ‹a = b› using ‹❙|g [b]❙| < ❙|h [b]❙|› len_im_le[OF IH_prem]
by (rule add_less_le_mono)
next
assume "a ≠ b"
then have "b ∈ set s" using ‹b ∈ set (a # s)› by simp
show "❙|g (a # s)❙| < ❙|h (a # s)❙|"
unfolding split using Cons.prems(1)[OF list.set_intros(1)]
Cons.IH[OF IH_prem ‹b ∈ set s› ‹❙|g [b]❙| < ❙|h [b]❙|›]
by (rule add_le_less_mono)
qed
qed simp
lemma solution_eq_len_eq:
assumes "g s = h s" and "⋀a. a ∈ set s ⟹ ❙|g [a]❙| = ❙|h [a]❙|"
shows "⋀a. a ∈ set s ⟹ g [a] = h [a]"
using assms proof (induction s)
case (Cons b s)
have nemp: "b # s ≠ ε" using list.distinct(2).
from ims_hd_eq_comp[OF nemp ‹g (b # s) = h (b # s)›] Cons.prems(3)[OF list.set_intros(1)]
have *: "g [b] = h [b]" unfolding list.sel(1) by (fact pref_comp_eq)
moreover have "g s = h s"
using ‹g (b # s) = h (b # s)›
unfolding g.pop_hd_nemp[OF nemp] h.pop_hd_nemp[OF nemp] list.sel * ..
from Cons.IH[OF _ this Cons.prems(3)[OF list.set_intros(2)]]
have "a ∈ set s ⟹ g [a] = h [a]" for a.
ultimately show "⋀a. a ∈ set (b # s) ⟹ g [a] = h [a]" by auto
qed auto
lemma rev_maps: "two_morphisms (rev_map g) (rev_map h)"
using g.rev_map_morph h.rev_map_morph by (intro two_morphisms.intro)
lemma min_solD_min_suf: assumes "sol ∈ g =⇩M h" and "s ≠ ε" "s ≤s sol" and "g s = h s"
shows "s = sol"
proof (rule ccontr)
assume "s ≠ sol"
from sufE[OF ‹s ≤s sol›]
obtain y where "sol = y ⋅ s".
hence "y ≠ ε"
using ‹s ≠ sol› by force
have "g y = h y"
using min_solD[OF ‹sol ∈ g =⇩M h›, unfolded ‹sol = y ⋅ s›]
unfolding g.morph h.morph ‹g s = h s› by blast
from min_solD_min[OF ‹sol ∈ g =⇩M h› ‹y ≠ ε› _ this]
have "y = sol"
using ‹sol = y ⋅ s› by blast
thus False
using ‹sol = y ⋅ s› ‹s ≠ ε› by fast
qed
lemma min_sol_rev[reversal_rule]:
assumes "s ∈ g =⇩M h"
shows "(rev s) ∈ (rev_map g) =⇩M (rev_map h)"
unfolding min_sol_def[of _ "rev_map g" "rev_map h", reversed]
using min_solD[OF assms] min_solD'[OF assms] min_solD_min_suf[OF assms] by blast
lemma coin_set_lists_concat: "ps ∈ lists (ℭ g h) ⟹ g (concat (map fst ps)) = h (concat (map snd ps))"
unfolding coincidence_set_def
by (induct ps, simp, auto simp add: g.morph h.morph)
lemma coin_set_hull: "⟨snd `(ℭ g h)⟩ = snd `(ℭ g h)"
proof (rule equalityI, rule subsetI)
fix x assume "x ∈ ⟨snd ` ℭ g h⟩"
then obtain xs where "xs ∈ lists (snd ` ℭ g h)" and "concat xs = x"
using hull_concat_lists0 by blast
then obtain ps where "ps ∈ lists (ℭ g h)" and "map snd ps = xs"
unfolding image_iff lists_image by blast
from coin_set_lists_concat[OF this(1), unfolded this(2) ‹concat xs = x›]
show "x ∈ snd ` ℭ g h"
unfolding coincidence_set_def by force
qed simp
lemma min_sol_sufE:
assumes "g r = h r" and "r ≠ ε"
obtains e where "e ∈ g =⇩M h" and "e ≤s r"
using assms
proof (induction "❙|r❙|" arbitrary: r thesis rule: less_induct)
case less
then show thesis
proof-
from min_sol_prefE[of g r h, OF ‹g r = h r› ‹r ≠ ε›]
obtain p where "p ∈ g =⇩M h" and "p ≤p r".
show thesis
proof (cases "p = r", (use less.prems(1)[OF ‹p ∈ g =⇩M h›] in fast))
assume "p ≠ r"
from prefE[OF ‹p ≤p r›]
obtain r' where "r = p ⋅ r'".
have "g r' = h r'"
using ‹g r = h r›[unfolded ‹r = p ⋅ r'› g.morph h.morph min_solD[OF ‹p ∈ g =⇩M h›] cancel].
from ‹p ≠ r› ‹r = p ⋅ r'›
have "r' ≠ ε" by fast
from min_solD'[OF ‹p ∈ g =⇩M h›] ‹r = p ⋅ r'›
have "❙|r'❙| < ❙|r❙|" by fastforce
from less.hyps[OF this _ ‹g r' = h r'› ‹r' ≠ ε›]
obtain e where "e ∈ g =⇩M h" "e ≤s r'".
from less.prems(1)[OF this(1), unfolded ‹r = p ⋅ r'›, OF suf_ext, OF this(2)]
show thesis.
qed
qed
qed
lemma min_sol_primitive: assumes "sol ∈ g =⇩M h" shows "primitive sol"
proof (rule ccontr)
have "sol ≠ ε"
using assms min_sol_def by auto
assume "¬ primitive sol"
from not_prim_primroot_expE[OF this]
obtain k where "(ρ sol)⇧@k = sol" "2 ≤ k".
hence "0 < k" by linarith
note min_solD[OF assms]
have "g (ρ sol) = h (ρ sol)"
by (rule pow_eq_eq[OF _ ‹0 < k›])
(unfold g.pow_morph[of "ρ sol" k, symmetric] h.pow_morph[of "ρ sol" k, symmetric] ‹(ρ sol)⇧@k = sol›, fact)
thus False
using ‹¬ primitive sol› min_solD_min[OF ‹sol ∈ g =⇩M h› primroot_nemp primroot_pref] ‹sol ≠ ε›
unfolding prim_primroot_conv[OF ‹sol ≠ ε›, symmetric] by blast
qed
lemma prim_sol_two_sols:
assumes "g u = h u" and "¬ u ∈ g =⇩M h" and "primitive u"
obtains s1 s2 where "s1 ∈ g =⇩M h" and "s2 ∈ g =⇩M h" and "s1 ≠ s2"
proof-
show thesis
using assms
proof (induction "❙|u❙|" arbitrary: u rule: less_induct)
case less
then show ?case
proof-
obtain s1 where "s1 ∈ g =⇩M h" and "s1 ≤p u"
using min_sol_prefE[of g u h, OF ‹g u = h u› prim_nemp[OF ‹primitive u›]].
obtain u' where "s1 ⋅ u' = u"
using ‹s1 ≤p u› unfolding prefix_def by blast
have "g u' = h u'"
using ‹g u = h u›[folded ‹s1 ⋅ u' = u›]
unfolding g.morph h.morph min_solD[OF ‹s1 ∈ g =⇩M h›] cancel.
have "u' ≠ ε"
using ‹s1 ∈ g =⇩M h› ‹¬ u ∈ g =⇩M h›[folded ‹s1 ⋅ u' = u›] by force
obtain exp where "(ρ u')⇧@exp = u'" "0 < exp"
using primroot_expE.
from pow_eq_eq[of "g (ρ u')" exp "h (ρ u')", folded g.pow_morph h.pow_morph, unfolded this(1), OF ‹g u' = h u'› ‹0 < exp›]
have "g (ρ u') = h (ρ u')".
have "❙|ρ u'❙| < ❙|u❙|"
using add_strict_increasing[OF nemp_pos_len [OF min_solD'[OF ‹s1 ∈ g =⇩M h›]] primroot_len_le[OF ‹u' ≠ ε›]]
unfolding lenarg[OF ‹s1 ⋅ u' = u›, unfolded lenmorph].
show thesis
proof (cases)
assume "ρ u' ∈ g =⇩M h"
have "ρ u' ≠ s1"
using ‹primitive u›[folded ‹s1 ⋅ u' = u›] comm_not_prim[OF primroot_nemp[OF ‹u' ≠ ε›] ‹u' ≠ ε› comm_primroot[symmetric]] by fast
from that[OF ‹ρ u' ∈ g =⇩M h› ‹s1 ∈ g =⇩M h› this]
show thesis.
next
assume "¬ ρ u' ∈ g =⇩M h"
from less.hyps[OF ‹❙|ρ u'❙| < ❙|u❙|› ‹g (ρ u') = h (ρ u')› this]
show thesis
using ‹u' ≠ ε› by blast
qed
qed
qed
qed
lemma prim_sols_two_sols:
assumes "g r = h r" and "g s = h s" and "primitive s" and "primitive r" and "r ≠ s"
obtains s1 s2 where "s1 ∈ g =⇩M h" and "s2 ∈ g =⇩M h" and "s1 ≠ s2"
using prim_sol_two_sols assms by blast
end
subsection ‹Two nonerasing morphisms›
text ‹Minimal coincidence pairs and minimal solutions make good sense for nonerasing morphisms only.›
locale two_nonerasing_morphisms = two_morphisms +
g: nonerasing_morphism g +
h: nonerasing_morphism h
begin
thm g.morph
thm g.emp_to_emp
lemma two_nonerasing_morphisms_swap: "two_nonerasing_morphisms h g"
by unfold_locales
lemma noner_eq_emp_iff: "g u = h v ⟹ u = ε ⟷ v = ε"
by (metis g.emp_to_emp g.nonerasing h.emp_to_emp h.nonerasing)
lemma min_coin_rev:
assumes "g r =⇩m h s"
shows "(rev_map g) (rev r) =⇩m (rev_map h) (rev s)"
proof (rule min_coin_defI)
show "rev r ≠ ε" and "rev s ≠ ε"
using min_coinD'[OF ‹g r =⇩m h s›] by simp_all
show "rev_map g (rev r) = rev_map h (rev s)"
unfolding rev_map_def using min_coinD[OF ‹g r =⇩m h s›] by auto
next
fix r' s' assume "r' ≤np rev r" "s' ≤np rev s" "rev_map g r' = rev_map h s'"
then obtain r'' s'' where "r''⋅ rev r' = r" and "s''⋅ rev s' = s"
using npD[OF ‹s' ≤np rev s›] npD[OF ‹r' ≤np rev r›]
unfolding pref_rev_suf_iff rev_rev_ident using sufD by (auto simp add: suffix_def)
have "g (rev r') = h (rev s')"
using ‹rev_map g r' = rev_map h s'›[unfolded rev_map_def rev_is_rev_conv] by simp
hence "g r'' = h s''"
using min_coinD[OF ‹g r =⇩m h s›, folded ‹r''⋅ rev r' = r› ‹s''⋅ rev s' = s›,
unfolded g.morph h.morph] by simp
have "r'' ≠ r"
using ‹r' ≤np rev r› ‹r'' ⋅ rev r' = r› by auto
hence "r'' = ε ∨ s'' = ε"
using ‹g r =⇩m h s›[unfolded min_coin_def nonempty_prefix_def]
‹r''⋅ rev r' = r› ‹s''⋅ rev s' = s› ‹g r'' = h s''›
by blast
hence "r'' = ε" and "s'' = ε"
using noner_eq_emp_iff[OF ‹g r'' = h s''›] by force+
thus "r' = rev r ∧ s' = rev s"
using ‹r''⋅ rev r' = r› ‹s''⋅ rev s' = s› by auto
qed
lemma min_coin_pref_eq:
assumes "g e =⇩m h f" and "g e' = h f'" and "e' ≤np e" and "f' ⨝ f"
shows "e' = e" and "f' = f"
proof-
note npD'[OF ‹e' ≤np e›] npD[OF ‹e' ≤np e›]
have "f ≠ ε" and "g e = h f"
using ‹g e =⇩m h f›[unfolded min_coin_def] by blast+
have "f' ≠ ε"
using ‹g e' = h f'› ‹e' ≠ ε› by (simp add: noner_eq_emp_iff)
from g.pref_mono[OF ‹e' ≤p e›, unfolded ‹g e = h f› ‹g e' = h f'›]
have "f' ≤p f"
using pref_compE[OF ‹f' ⨝ f›] ‹f' ≠ ε› h.pref_mono h.pref_morph_pref_eq by metis
hence "f' ≤np f"
using ‹f' ≠ ε› by blast
with ‹g e =⇩m h f›[unfolded min_coin_def]
show "e' = e" and "f' = f"
using ‹g e' = h f'› ‹e' ≤np e› by blast+
qed
lemma min_coin_prefE:
assumes "g r = h s" and "r ≠ ε"
obtains e f where "g e =⇩m h f" and "e ≤p r" and "f ≤p s" and "hd e = hd r"
proof-
define P where "P = (λ k. ∃ e f. g e = h f ∧ e ≠ ε ∧ e ≤p r ∧ f ≤p s ∧ ❙|e❙| = k)"
define d where "d = (LEAST k. P k)"
obtain e f where "g e = h f" and "e ≠ ε" and "e ≤p r" and "f ≤p s" and "❙|e❙| = d"
using ‹g r = h s› LeastI[of P "❙|r❙|"] P_def assms(2) d_def by blast
hence "f ≠ ε"
using noner_eq_emp_iff by blast
have "r' ≤np e ⟹ s' ≤np f ⟹ g r' = h s' ⟹ r' = e ∧ s' = f" for r' s'
proof-
assume "r' ≤np e" and "s' ≤np f" and "g r' = h s'"
hence "P ❙|r'❙|"
unfolding P_def using ‹e ≤p r› ‹f ≤p s› npD'[OF ‹r' ≤np e›]
pref_trans[OF npD[OF ‹r' ≤np e›] ‹e ≤p r›]
pref_trans[OF npD[OF ‹s' ≤np f›] ‹f ≤p s›] by blast
from Least_le[of P, OF this, folded ‹❙|e❙| = d› d_def]
have "r' = e"
using long_pref[OF npD[OF ‹r' ≤np e›]] by blast
from ‹g e = h f›[folded this, unfolded ‹g r' = h s'›] this
show ?thesis
using conjunct2[OF ‹s' ≤np f›[unfolded nonempty_prefix_def]] h.pref_morph_pref_eq
by simp
qed
hence "g e =⇩m h f"
unfolding min_coin_def using ‹e ≠ ε› ‹f ≠ ε› ‹g e = h f› by blast
from that[OF this ‹e ≤p r› ‹f ≤p s› pref_hd_eq[OF ‹e ≤p r› ‹e ≠ ε›]]
show thesis.
qed
lemma min_coin_dec: assumes "g e = h f"
obtains ps where "concat (map fst ps) = e" and "concat (map snd ps) = f" and
"⋀ p. p ∈ set ps ⟹ g (fst p) =⇩m h (snd p)"
using assms
proof (induct "❙|e❙|" arbitrary: e f thesis rule: less_induct)
case less
then show ?case
proof-
show thesis
proof (cases "e = ε")
assume "e = ε"
hence "f = ε" using ‹g e = h f›
using noner_eq_emp_iff by auto
from less.prems(1)[of ε] ‹e = ε› ‹f = ε›
show thesis by simp
next
assume "e ≠ ε"
from min_coin_prefE[OF ‹g e = h f› this]
obtain e⇩1 e⇩2 f⇩1 f⇩2 where "g e⇩1 =⇩m h f⇩1" and "e⇩1 ⋅ e⇩2 = e" and "f⇩1 ⋅ f⇩2 = f" and "e⇩1 ≠ ε" and "f⇩1 ≠ ε"
using min_coinD' prefD by metis
have "g e⇩2 = h f⇩2"
using ‹g e = h f›[folded ‹e⇩1 ⋅ e⇩2 = e› ‹f⇩1 ⋅ f⇩2 = f›, unfolded g.morph h.morph min_coinD[OF ‹g e⇩1 =⇩m h f⇩1›] cancel].
have "❙|e⇩2❙| < ❙|e❙|"
using lenarg[OF ‹e⇩1 ⋅ e⇩2 = e›] nemp_pos_len[OF ‹e⇩1 ≠ ε›] unfolding lenmorph by linarith
from less.hyps[OF ‹❙|e⇩2❙| < ❙|e❙|› _ ‹g e⇩2 = h f⇩2›]
obtain ps' where "concat (map fst ps') = e⇩2" and "concat (map snd ps') = f⇩2" and "⋀p. p ∈ set ps' ⟹ g (fst p) =⇩m h (snd p)"
by blast
show thesis
proof(rule less.prems(1)[of "(e⇩1,f⇩1)#ps'"])
show "concat (map fst ((e⇩1, f⇩1) # ps')) = e"
using ‹concat (map fst ps') = e⇩2› ‹e⇩1 ⋅ e⇩2 = e› by simp
show "concat (map snd ((e⇩1, f⇩1) # ps')) = f"
using ‹concat (map snd ps') = f⇩2› ‹f⇩1 ⋅ f⇩2 = f› by simp
show "⋀p. p ∈ set ((e⇩1, f⇩1) # ps') ⟹ g (fst p) =⇩m h (snd p)"
using ‹⋀p. p ∈ set ps' ⟹ g (fst p) =⇩m h (snd p)› ‹g e⇩1 =⇩m h f⇩1› by auto
qed
qed
qed
qed
lemma min_coin_code:
assumes "xs ∈ lists (ℭ⇩m g h)" and "ys ∈ lists (ℭ⇩m g h)" and
"concat (map fst xs) = concat (map fst ys)" and
"concat (map snd xs) = concat (map snd ys)"
shows "xs = ys"
using assms
proof (induction xs ys rule: list_induct2')
case (2 x xs)
then show ?case
using min_coin_setD[THEN min_coinD', of x g h] listsE[OF ‹x # xs ∈ lists (ℭ⇩m g h)›] by force
next
case (3 y ys)
then show ?case
using min_coin_setD[of y g h, THEN min_coinD'] listsE[OF ‹y # ys ∈ lists (ℭ⇩m g h)›] by auto
next
case (4 x xs y ys)
then show ?case
proof-
have "concat (map fst (x#xs)) = fst x ⋅ concat (map fst xs)"
"concat (map fst (y#ys)) = fst y ⋅ concat (map fst ys)"
"concat (map snd (x#xs)) = snd x ⋅ concat (map snd xs)"
"concat (map snd (y#ys)) = snd y ⋅ concat (map snd ys)"
by auto
from eqd_comp[OF ‹concat (map fst (x#xs)) = concat (map fst (y#ys))›[unfolded this]] eqd_comp[OF ‹concat (map snd (x#xs)) = concat (map snd (y#ys))›[unfolded this]]
have "fst x ⨝ fst y" and "snd x ⨝ snd y".
have "g (fst y) =⇩m h (snd y)" and "g (fst x) =⇩m h (snd x)"
by (use min_coin_setD listsE[OF ‹y # ys ∈ lists (ℭ⇩m g h)›] in blast)
(use min_coin_setD listsE[OF ‹x # xs ∈ lists (ℭ⇩m g h)›] in blast)
from min_coin_pref_eq[OF this(1) min_coinD[OF this(2)] _ ‹snd x ⨝ snd y›]
min_coin_pref_eq[OF this(2) min_coinD[OF this(1)] _ pref_comp_sym[OF ‹snd x ⨝ snd y›]] min_coinD'[OF this(1)] min_coinD'[OF this(2)]
have "fst x = fst y" and "snd x = snd y"
using npI pref_compE[OF ‹fst x ⨝ fst y›] by metis+
hence eq: "concat (map fst xs) = concat (map fst ys)"
"concat (map snd xs) = concat (map snd ys)"
using "4.prems"(3-4) by fastforce+
have "xs ∈ lists (ℭ⇩m g h)" "ys ∈ lists (ℭ⇩m g h)"
using "4.prems"(1-2) by fastforce+
from "4.IH"(1)[OF this eq] prod_eqI[OF ‹fst x = fst y› ‹snd x = snd y›]
show "x # xs = y # ys"
by blast
qed
qed simp
lemma coin_closed: "ps ∈ lists (ℭ g h) ⟹ (concat (map fst ps), concat (map snd ps)) ∈ ℭ g h"
unfolding coincidence_set_def
by (induct ps, simp, auto simp add: g.morph h.morph)
lemma min_coin_gen_snd: "⟨snd ` (ℭ⇩m g h)⟩ = snd `(ℭ g h)"
proof
show "⟨snd ` ℭ⇩m g h⟩ ⊆ snd ` ℭ g h"
proof
fix x assume "x ∈ ⟨snd ` ℭ⇩m g h⟩"
then obtain xs where "xs ∈ lists (snd ` ℭ⇩m g h)" and "x = concat xs"
using hull_concat_lists0 by blast
then obtain ps where "ps ∈ lists (ℭ⇩m g h)" and "xs = map snd ps"
unfolding lists_image image_iff by blast
from min_coin_sub coin_closed this(1)
have "(concat (map fst ps), x) ∈ ℭ g h"
unfolding ‹x = concat xs› ‹xs = map snd ps› by fast
thus "x ∈ snd ` ℭ g h" by force
qed
show "snd ` ℭ g h ⊆ ⟨snd ` ℭ⇩m g h⟩"
proof
fix x assume "x ∈ snd ` ℭ g h"
then obtain r where "g r = h x"
unfolding image_iff coincidence_set_def by force
from min_coin_dec[OF this]
obtain ps where "concat (map snd ps) = x" and "⋀p. p ∈ set ps ⟹ g (fst p) =⇩m h (snd p)" by metis
thus "x ∈ ⟨snd ` ℭ⇩m g h⟩"
unfolding min_coincidence_set_def image_def by fastforce
qed
qed
lemma min_coin_gen_fst: "⟨fst ` (ℭ⇩m g h)⟩ = fst `(ℭ g h)"
using two_nonerasing_morphisms.min_coin_gen_snd[folded coin_set_sym min_coin_set_sym, OF two_nonerasing_morphisms_swap].
lemma min_coin_code_snd:
assumes "code_morphism g" shows "code (snd ` (ℭ⇩m g h))"
proof
fix xs ys assume "xs ∈ lists (snd ` ℭ⇩m g h)" and "ys ∈ lists (snd ` ℭ⇩m g h)"
then obtain psx psy where "psx ∈ lists (ℭ⇩m g h)" and "xs = map snd psx" and
"psy ∈ lists (ℭ⇩m g h)" and "ys = map snd psy"
unfolding image_iff lists_image by blast+
have eq1: "g (concat (map fst psx)) = h (concat xs)"
using ‹psx ∈ lists (ℭ⇩m g h)› ‹xs = map snd psx› min_coin_sub[of g h]
coin_set_lists_concat by fastforce
have eq2: "g (concat (map fst psy)) = h (concat ys)"
using ‹psy ∈ lists (ℭ⇩m g h)› ‹ys = map snd psy› min_coin_sub[of g h]
coin_set_lists_concat by fastforce
assume "concat xs = concat ys"
from arg_cong[OF this, of h, folded eq1 eq2]
have "concat (map fst psx) = concat (map fst psy)"
using code_morphism.code_morph_code[OF ‹code_morphism g›] by auto
have "concat (map snd psx) = concat (map snd psy)"
using ‹concat xs = concat ys› ‹xs = map snd psx› ‹ys = map snd psy› by auto
from min_coin_code[OF ‹psx ∈ lists (ℭ⇩m g h)› ‹psy ∈ lists (ℭ⇩m g h)› ‹concat (map fst psx) = concat (map fst psy)› this]
show "xs = ys"
unfolding ‹xs = map snd psx› ‹ys = map snd psy› by blast
qed
lemma min_coin_code_fst:
"code_morphism h ⟹ code (fst ` (ℭ⇩m g h))"
using two_nonerasing_morphisms.min_coin_code_snd[OF two_nonerasing_morphisms_swap, folded min_coin_set_sym].
lemma min_coin_basis_snd:
assumes "code_morphism g"
shows "𝔅 (snd `(ℭ g h)) = snd ` (ℭ⇩m g h)"
unfolding min_coin_gen_snd[symmetric] basis_of_hull
using min_coin_code_snd[OF assms] code.code_is_basis by blast
lemma min_coin_basis_fst:
"code_morphism h ⟹ 𝔅 (fst `(ℭ g h)) = fst ` (ℭ⇩m g h)"
using two_nonerasing_morphisms.min_coin_basis_snd[folded coin_set_sym min_coin_set_sym, OF two_nonerasing_morphisms_swap].
lemma sol_im_len_less: assumes "g u = h u" and "g ≠ h" and "set u = UNIV"
shows "❙|u❙| < ❙|g u❙|"
proof (rule ccontr)
assume "¬ ❙|u❙| < ❙|g u❙|"
hence "❙|u❙| = ❙|g u❙|" and "❙|u❙| = ❙|h u❙|"
unfolding ‹g u = h u› using h.im_len_le le_neq_implies_less by blast+
from this(1)[unfolded g.im_len_eq_iff] this(2)[unfolded h.im_len_eq_iff] ‹set u = UNIV›
have "❙|g [c]❙| = 1" and "❙|h [c]❙| = 1" for c by blast+
hence "g = h"
using solution_eq_len_eq[OF ‹g u = h u›, THEN def_on_sings_eq, unfolded ‹set u = UNIV›, OF _ UNIV_I]
by force
thus False using ‹g ≠ h› by contradiction
qed
end
locale two_code_morphisms = g: code_morphism g + h: code_morphism h
for g h :: "'a list ⇒ 'b list"
begin
sublocale two_nonerasing_morphisms g h
by unfold_locales
lemmas code_morphs = g.code_morphism_axioms h.code_morphism_axioms
lemma revs_two_code_morphisms: "two_code_morphisms (rev_map g) (rev_map h)"
by (simp add: g.code_morphism_rev_map h.code_morphism_rev_map two_code_morphisms.intro)
lemma min_coin_im_basis:
"𝔅 (h` (snd `(ℭ g h))) = h ` snd ` (ℭ⇩m g h)"
"𝔅 (g` (fst `(ℭ g h))) = g ` fst ` (ℭ⇩m g h)"
proof-
thm morphism_on.inj_basis_to_basis
code_morphism.morph_on_inj_on
min_coin_basis_snd
note basis_morph_swap = morphism_on.inj_basis_to_basis[OF code_morphism.morph_on_inj_on, symmetric]
thm basis_morph_swap
coin_set_hull
basis_morph_swap[OF code_morphs(2) code_morphs(2), of "snd ` ℭ g h", unfolded coin_set_hull]
show "𝔅 (h ` snd ` ℭ g h) = h ` snd ` ℭ⇩m g h"
unfolding basis_morph_swap[OF code_morphs(2) code_morphs(2), of "snd ` ℭ g h", unfolded coin_set_hull]
unfolding min_coin_basis_snd[OF code_morphs(1)]..
interpret swap: two_code_morphisms h g
using two_code_morphisms_def code_morphs by blast
thm basis_morph_swap[OF code_morphs(1) code_morphs(1), of "fst ` ℭ g h"]
swap.coin_set_hull
coin_set_hull
coin_set_sym
swap.coin_set_hull[folded coin_set_sym]
basis_morph_swap[OF code_morphs(1) code_morphs(1), of "fst ` ℭ g h", unfolded swap.coin_set_hull[folded coin_set_sym]]
min_coin_basis_fst
show "𝔅 (g ` fst ` ℭ g h) = g ` fst ` ℭ⇩m g h"
unfolding basis_morph_swap[OF code_morphs(1) code_morphs(1), of "fst ` ℭ g h", unfolded swap.coin_set_hull[folded coin_set_sym]]
unfolding min_coin_basis_fst[OF code_morphs(2)]
unfolding min_coin_gen_fst..
qed
lemma range_inter_basis_snd:
shows "𝔅 (range g ∩ range h) = h ` (snd ` ℭ⇩m g h)"
"𝔅 (range g ∩ range h) = g ` (fst ` ℭ⇩m g h)"
proof-
show "𝔅 (range g ∩ range h) = h ` (snd ` ℭ⇩m g h)"
unfolding coin_set_inter_snd[folded image_comp, symmetric]
using min_coin_im_basis(1).
show "𝔅 (range g ∩ range h) = g ` (fst ` ℭ⇩m g h)"
unfolding coin_set_inter_fst[folded image_comp, symmetric]
using min_coin_im_basis(2).
qed
lemma range_inter_code:
shows "code 𝔅 (range g ∩ range h)"
unfolding range_inter_basis_snd
thm morphism_on.inj_code_to_code
by (rule morphism_on.inj_code_to_code)
(simp_all add: h.morph_on h.morph_on_inj_on(2) code_morphs(1) min_coin_code_snd)
end
subsection ‹Two marked morphisms›
locale two_marked_morphisms = two_nonerasing_morphisms +
g: marked_morphism g + h: marked_morphism h
begin
sublocale revs: two_code_morphisms g h
by (simp add: g.code_morphism_axioms h.code_morphism_axioms two_code_morphisms.intro)
lemmas ne_g = g.nonerasing and
ne_h = h.nonerasing
lemma unique_continuation:
"z ⋅ g r = z' ⋅ h s ⟹ z ⋅ g r' = z' ⋅ h s' ⟹ z ⋅ g (r ∧⇩p r') = z' ⋅ h (s ∧⇩p s')"
using lcp_ext_left g.marked_morph_lcp h.marked_morph_lcp by metis
lemmas empty_sol = noner_eq_emp_iff
lemma comparable_min_sol_eq: assumes "r ≤p r'" and "g r =⇩m h s" and "g r' =⇩m h s'"
shows "r = r'" and "s = s'"
proof-
have "s ≤p s'"
using g.pref_mono[OF ‹r ≤p r'›]
h.pref_free_morph
unfolding min_coinD[OF ‹g r =⇩m h s›] min_coinD[OF ‹g r' =⇩m h s'›] by simp
thus "r = r'"and "s = s'"
using ‹g r' =⇩m h s'›[unfolded min_coin_def] min_coinD[OF ‹g r =⇩m h s›] min_coinD'[OF ‹g r =⇩m h s›] ‹r ≤p r'›
by blast+
qed
lemma first_letter_determines:
assumes "g e =⇩m h f" and "g e' = h f'" and "hd e = hd e'" and "e' ≠ ε"
shows "e ≤p e'" and "f ≤p f'"
proof-
have "g (e ∧⇩p e') = h (f ∧⇩p f')"
using unique_continuation[of ε e ε f e' f', unfolded emp_simps, OF min_coinD[OF‹g e =⇩m h f›] ‹g e' = h f'›].
have "e ≠ ε"
using ‹g e =⇩m h f› min_coinD' by auto
hence eq1: "e = [hd e] ⋅ tl e" and eq2: "e' = [hd e'] ⋅ tl e'" using ‹e' ≠ ε› by simp+
from lcp_ext_left[of "[hd e]" "tl e" "tl e'", folded eq1 eq2[folded ‹hd e = hd e'›]]
have "e ∧⇩p e' ≠ ε" by force
from this
have "f ∧⇩p f' ≠ ε"
using ‹g (e ∧⇩p e') = h (f ∧⇩p f')› g.nonerasing h.emp_to_emp by force
from npI[OF ‹e ∧⇩p e' ≠ ε› lcp_pref] npI[OF ‹f ∧⇩p f' ≠ ε› lcp_pref]
show "e ≤p e'" and "f ≤p f'"
using min_coin_minD[OF assms(1) ‹e ∧⇩p e' ≤np e› ‹f ∧⇩p f' ≤np f› ‹g (e ∧⇩p e') = h (f ∧⇩p f')›,
unfolded lcp_sym[of e] lcp_sym[of f]] lcp_pref by metis+
qed
corollary first_letter_determines':
assumes "g e =⇩m h f" and "g e' =⇩m h f'" and "hd e = hd e'"
shows "e = e'" and "f = f'"
proof-
have "e ≠ ε" and "e' ≠ ε"
using ‹g e =⇩m h f› ‹g e' =⇩m h f'› min_coinD' by blast+
have "g e' = h f'" and "g e = h f"
using ‹g e =⇩m h f› ‹g e' =⇩m h f'› min_coinD by blast+
show "e = e'" and "f = f'"
using first_letter_determines[OF ‹g e =⇩m h f› ‹g e' = h f'› ‹hd e = hd e'› ‹e' ≠ ε›]
first_letter_determines[OF ‹g e' =⇩m h f'› ‹g e = h f› ‹hd e = hd e'›[symmetric] ‹e ≠ ε›]
by force+
qed
lemma first_letter_determines_sol: assumes "r ∈ g =⇩M h" and "s ∈ g =⇩M h" and "hd r = hd s"
shows "r = s"
proof-
have "r ∧⇩p s ≠ ε"
using nemp_lcp_distinct_hd[OF min_solD'[OF ‹r ∈ g =⇩M h›] min_solD'[OF ‹s ∈ g =⇩M h›]] ‹hd r = hd s›
by blast
have "g r = h r" and "g s = h s"
using min_solD[OF ‹r ∈ g =⇩M h›] min_solD[OF ‹s ∈ g =⇩M h›].
have "g (r ∧⇩p s) = h (r ∧⇩p s)"
unfolding ‹g r = h r› ‹g s = h s› g.marked_morph_lcp h.marked_morph_lcp..
from min_solD_min[OF ‹r ∈ g =⇩M h› ‹r ∧⇩p s ≠ ε› lcp_pref this] min_solD_min[OF ‹s ∈ g =⇩M h› ‹r ∧⇩p s ≠ ε› lcp_pref' this]
show "r = s" by force
qed
definition pre_block :: "'a ⇒ 'a list × 'a list"
where "pre_block a = (THE p. (g (fst p) =⇩m h (snd p)) ∧ hd (fst p) = a)"
definition blockP :: "'a ⇒ bool"
where "blockP a ≡ g (fst (pre_block a)) =⇩m h (snd (pre_block a)) ∧ hd (fst (pre_block a)) = a"
lemma pre_blockI: "g u =⇩m h v ⟹ pre_block (hd u) = (u,v)"
unfolding pre_block_def
proof (rule the_equality)
show "⋀p. g u =⇩m h v ⟹ g (fst p) =⇩m h (snd p) ∧ hd (fst p) = hd u ⟹ p = (u, v)"
using first_letter_determines' by force
qed simp
lemma blockI: assumes "g u =⇩m h v" and "hd u = a"
shows "blockP a"
proof-
from pre_blockI[OF ‹g u =⇩m h v›, unfolded ‹hd u = a›]
show "blockP a"
unfolding blockP_def using assms by simp
qed
lemma hd_im_comm_eq_aux:
assumes "g w = h w" and "w ≠ ε" and comm: "g⇧𝒞 (hd w) ⋅ h⇧𝒞(hd w) = h⇧𝒞 (hd w) ⋅ g⇧𝒞(hd w)" and len: "❙|g⇧𝒞 (hd w)❙| ≤ ❙|h⇧𝒞(hd w)❙|"
shows "g⇧𝒞 (hd w) = h⇧𝒞 (hd w)"
proof(cases "w ∈ [hd w]*")
assume "w ∈ [hd w]*"
then obtain l where "w = [hd w]⇧@l"
unfolding root_def by metis
from nemp_exp_pos[OF ‹w ≠ ε›, of "[hd w]" l, folded this]
have "l ≠ 0"
by fast
from ‹g w = h w›
have "(g [hd w])⇧@l = (h [hd w])⇧@l"
unfolding g.pow_morph[symmetric] h.pow_morph[symmetric] ‹w = [hd w]⇧@l›[symmetric].
with ‹l ≠ 0›
have "g [hd w] = h [hd w]"
using pow_eq_eq by blast
thus "g⇧𝒞 (hd w) = h⇧𝒞 (hd w)"
unfolding core_def.
next
assume "w ∉ [hd w]*"
from distinct_letter_in_hd[OF this]
obtain b l w' where "[hd w]⇧@l ⋅ [b] ⋅ w' = w" and "b ≠ hd w" and "l ≠ 0".
from commE[OF comm]
obtain t m k where "g⇧𝒞 (hd w) = t⇧@m" and "h⇧𝒞 (hd w) = t⇧@k".
have "❙|t❙| ≠ 0" and "t ≠ ε" and "m ≠ 0"
using ‹g⇧𝒞 (hd w) = t⇧@m› g.core_nemp pow_zero[of t] by (fastforce, fastforce, metis)
with lenarg[OF ‹g⇧𝒞 (hd w) = t⇧@m›] lenarg[OF ‹h⇧𝒞 (hd w) = t⇧@k›]
have "m ≤ k"
unfolding pow_len lenmorph using len by auto
have "m = k"
proof(rule ccontr)
assume "m ≠ k" hence "m < k" using ‹m ≤ k› by simp
have "0 < k*l-m*l"
using ‹m < k› ‹l ≠ 0› by force
have "g w = t⇧@(m*l) ⋅ g [b] ⋅ g w'"
unfolding arg_cong[OF ‹[hd w]⇧@l ⋅ [b] ⋅ w' = w›, of g, symmetric] g.morph
g.pow_morph ‹g⇧𝒞 (hd w) = t⇧@m›[unfolded core_def] pow_mult[symmetric]..
moreover have "h w = t⇧@(k*l) ⋅ h [b] ⋅ h w'"
unfolding arg_cong[OF ‹[hd w]⇧@l ⋅ [b] ⋅ w' = w›, of h, symmetric] h.morph
h.pow_morph ‹h⇧𝒞 (hd w) = t⇧@k›[unfolded core_def] pow_mult[symmetric]..
ultimately have *: "g [b] ⋅ g w' = t⇧@(k*l-m*l) ⋅ h [b] ⋅ h w'"
using ‹g w = h w› pop_pow_cancel[OF _ mult_le_mono1[OF ‹m ≤ k›]]
unfolding g.morph[symmetric] h.morph[symmetric] by metis
have "t⇧@(k*l-m*l) ≠ ε"
using gr_implies_not0[OF ‹0 < k * l - m * l›] unfolding nemp_emp_pow[OF ‹t ≠ ε›].
have "hd (t⇧@(k*l-m*l)) = hd t"
using hd_append2[OF ‹t ≠ ε›] unfolding pow_pos[OF ‹0 < k * l - m * l›].
have "hd t = hd (g [b])"
using hd_append2[OF g.sing_to_nemp[of b], of "g w'"]
unfolding hd_append2[of _ "h [b] ⋅ h w'", OF ‹t⇧@(k*l-m*l) ≠ ε›, folded *] ‹hd (t⇧@(k*l-m*l)) = hd t›.
have "hd t = hd (g [hd w])"
using g.hd_im_hd_hd[OF ‹w ≠ ε›, unfolded ‹g⇧𝒞 (hd w) = t ⇧@ m›[unfolded core_def]]
hd_append2[OF ‹t ≠ ε›, of "t⇧@(m-1)", unfolded pow_Suc, folded pow_Suc[of t "m-1", unfolded Suc_minus[OF ‹m ≠ 0›]]]
g.hd_im_hd_hd[OF ‹w ≠ ε›] by force
thus False
unfolding ‹hd t = hd (g [b])› using ‹b ≠ hd w› g.marked_morph by blast
qed
show "g⇧𝒞 (hd w) = h⇧𝒞 (hd w)"
unfolding ‹g⇧𝒞 (hd w) = t⇧@m› ‹h⇧𝒞 (hd w) = t⇧@k› ‹m = k›..
qed
lemma hd_im_comm_eq:
assumes "g w = h w" and "w ≠ ε" and comm: "g⇧𝒞 (hd w) ⋅ h⇧𝒞(hd w) = h⇧𝒞 (hd w) ⋅ g⇧𝒞(hd w)"
shows "g⇧𝒞 (hd w) = h⇧𝒞 (hd w)"
proof-
interpret swap: two_marked_morphisms h g by unfold_locales
show "g⇧𝒞 (hd w) = h⇧𝒞 (hd w)"
using hd_im_comm_eq_aux[OF assms] swap.hd_im_comm_eq_aux[OF assms(1)[symmetric] assms(2) assms(3)[symmetric], symmetric]
by force
qed
lemma block_ex: assumes "g u =⇩m h v" shows "blockP (hd u)"
unfolding blockP_def using pre_blockI[OF assms] assms by simp
lemma sol_block_ex: assumes "g u = h v" and "u ≠ ε" shows "blockP (hd u)"
using min_coin_prefE[OF assms] block_ex by metis
definition suc_fst where "suc_fst ≡ λ x. concat(map (λ y. fst (pre_block y)) x)"
definition suc_snd where "suc_snd ≡ λ x. concat(map (λ y. snd (pre_block y)) x)"
lemma blockP_D: "blockP a ⟹ g (suc_fst [a]) =⇩m h (suc_snd [a])"
unfolding blockP_def suc_fst_def suc_snd_def by simp
lemma blockP_D_hd: "blockP a ⟹ hd (suc_fst [a]) = a"
unfolding blockP_def suc_fst_def by simp
abbreviation "blocks τ ≡ (∀ a. a ∈ set τ ⟶ blockP a)"
sublocale sucs: two_morphisms suc_fst suc_snd
by (standard) (simp_all add: suc_fst_def suc_snd_def)
lemma blockP_D_hd_hd: assumes "blockP a"
shows "hd (h⇧𝒞 (hd (suc_snd [a]))) = hd (g⇧𝒞 a)"
proof-
from hd_tlE[OF conjunct2[OF min_coinD'[OF blockP_D[OF ‹blockP a›]]]]
obtain b where "hd (suc_snd [a]) = b" by blast
have "suc_fst [a] ≠ ε" and "suc_snd [a] ≠ ε"
using min_coinD'[OF blockP_D[OF ‹blockP a›]] by blast+
from g.hd_im_hd_hd[OF this(1)] h.hd_im_hd_hd[OF this(2)]
have "hd (h⇧𝒞 (hd (suc_snd [a]))) = hd (g⇧𝒞 (hd (suc_fst [a])))"
unfolding core_def min_coinD[OF blockP_D[OF ‹blockP a›]] by argo
thus ?thesis
unfolding blockP_D_hd[OF assms].
qed
lemma suc_morph_sings: assumes "g e =⇩m h f"
shows "suc_fst [hd e] = e" and "suc_snd [hd e] = f"
unfolding suc_fst_def suc_snd_def using pre_blockI[OF assms] by simp_all
lemma blocks_eq: "blocks τ ⟹ g (suc_fst τ) = h (suc_snd τ)"
proof (induct τ)
case (Cons a τ)
have "blocks τ" and "blockP a"
using ‹blocks (a # τ)› by simp_all
from Cons.hyps[OF this(1)]
show ?case
unfolding sucs.g.pop_hd[of a τ] sucs.h.pop_hd[of a τ] g.morph h.morph
using min_coinD[OF blockP_D, OF ‹blockP a›] by simp
qed simp
lemma suc_eq': assumes "⋀ a. blockP a" shows "g(suc_fst w) = h(suc_snd w)"
by (simp add: assms blocks_eq)
lemma suc_eq: assumes all_blocks: "⋀ a. blockP a" shows "g ∘ suc_fst = h ∘ suc_snd"
using suc_eq'[OF assms] by fastforce
lemma block_eq: "blockP a ⟹ g (suc_fst [a]) = h (suc_snd [a])"
using blockP_D min_coinD by blast
lemma blocks_inj_suc: assumes "blocks τ" shows "inj_on suc_fst⇧𝒞 (set τ)"
unfolding inj_on_def core_def using blockP_D_hd[OF ‹blocks τ›[rule_format]]
by metis
lemma blocks_inj_suc': assumes "blocks τ" shows "inj_on suc_snd⇧𝒞 (set τ)"
using g.marked_core blockP_D_hd_hd[OF ‹blocks τ›[rule_format]]
unfolding inj_on_def core_def by metis
lemma blocks_marked_code: assumes "blocks τ"
shows "marked_code (suc_fst⇧𝒞 `(set τ))"
proof
show "ε ∉ suc_fst⇧𝒞 ` set τ"
unfolding core_def image_iff using min_coinD'[OF blockP_D[OF ‹blocks τ›[rule_format]]] by fastforce
show "⋀u v. u ∈ suc_fst⇧𝒞 ` set τ ⟹
v ∈ suc_fst⇧𝒞 ` set τ ⟹ hd u = hd v ⟹ u = v"
using blockP_D_hd[OF ‹blocks τ›[rule_format]] unfolding core_def by fastforce
qed
lemma blocks_marked_code': assumes all_blocks: "⋀ a. a ∈ set τ ⟹ blockP a"
shows "marked_code (suc_snd⇧𝒞 `(set τ))"
proof
show "ε ∉ suc_snd⇧𝒞 ` set τ"
unfolding core_def image_iff using min_coinD'[OF all_blocks[THEN blockP_D]] by fastforce
show "u = v" if "u ∈ suc_snd⇧𝒞 ` set τ" and "v ∈ suc_snd⇧𝒞 ` set τ" and "hd u = hd v" for u v
proof-
obtain a b where "u = suc_snd [a]" and "v = suc_snd [b]" and "a ∈ set τ" and "b ∈ set τ"
using ‹v ∈ suc_snd⇧𝒞 ` set τ› ‹u ∈ suc_snd⇧𝒞 ` set τ› unfolding core_def by fast+
from g.marked_core[of a b,
folded blockP_D_hd_hd[OF all_blocks, OF ‹a ∈ set τ›] blockP_D_hd_hd[OF all_blocks, OF ‹b ∈ set τ›]
this(1-2) ‹hd u = hd v›,OF refl]
show "u = v"
unfolding ‹u = suc_snd [a]› ‹v = suc_snd [b]› by blast
qed
qed
lemma sucs_marked_morphs: assumes all_blocks: "⋀ a. blockP a"
shows "two_marked_morphisms suc_fst suc_snd"
proof
show "hd (suc_fst⇧𝒞 a) = hd (suc_fst⇧𝒞 b) ⟹ a = b" for a b
using blockP_D_hd[OF all_blocks] unfolding core_def by force
show "hd (suc_snd⇧𝒞 a) = hd (suc_snd⇧𝒞 b) ⟹ a = b" for a b
using blockP_D_hd_hd[OF all_blocks, folded core_sing] g.marked_core by metis
show "suc_fst w = ε ⟹ w = ε" for w
using assms blockP_D min_coinD' sucs.g.noner_sings_conv by blast
show "suc_snd w = ε ⟹ w = ε" for w
using blockP_D[OF assms(1), THEN min_coinD'] sucs.h.noner_sings_conv by blast
qed
lemma pre_blocks_range: "{(e,f). g e =⇩m h f } ⊆ range pre_block"
using pre_blockI case_prodE by blast
corollary card_blocks: assumes "finite (UNIV :: 'a set)" shows "card {(e,f). g e =⇩m h f } ≤ card (UNIV :: 'a set)"
using le_trans[OF card_mono[OF finite_imageI pre_blocks_range, OF assms] card_image_le[of _ pre_block, OF assms]].
lemma block_decomposition: assumes "g e = h f"
obtains τ where "suc_fst τ = e" and "suc_snd τ = f" and "blocks τ"
using assms
proof (induct "❙|e❙|" arbitrary: e f thesis rule: less_induct)
case less
show ?case
proof (cases "e = ε")
assume "e = ε"
hence "f = ε"
using less.hyps empty_sol[OF ‹g e = h f›] by blast
hence "suc_fst ε = e" and "suc_snd ε = f"
unfolding suc_fst_def suc_snd_def by (simp add: ‹e = ε›)+
from less.prems(1)[OF this]
show thesis
by simp
next
assume "e ≠ ε"
from min_coin_prefE[OF ‹g e = h f› this]
obtain e⇩1 e⇩2 f⇩1 f⇩2
where "g e⇩1 =⇩m h f⇩1" and "e⇩1⋅e⇩2 = e" and "f⇩1⋅f⇩2 = f" and "e⇩1 ≠ ε" and "f⇩1 ≠ ε"
by (metis min_coinD' prefD)
from ‹g e = h f›[folded ‹e⇩1⋅e⇩2 = e› ‹f⇩1⋅f⇩2 = f›, unfolded g.morph h.morph]
have "g e⇩2 = h f⇩2"
using min_coinD[OF ‹g e⇩1 =⇩m h f⇩1›] by simp
have "❙|e⇩2❙| < ❙|e❙|"
using ‹e⇩1⋅e⇩2 = e› ‹e⇩1 ≠ ε› by auto
from less.hyps[OF this _ ‹g e⇩2 = h f⇩2›]
obtain τ' where "suc_fst τ' = e⇩2" and "suc_snd τ' = f⇩2" and "blocks τ'".
have "suc_fst [hd e] = e⇩1" and "suc_snd [hd e] = f⇩1"
using suc_morph_sings ‹e⇩1 ⋅ e⇩2 = e› ‹g e⇩1 =⇩m h f⇩1› ‹e⇩1 ≠ ε› by auto
hence "suc_fst (hd e # τ') = e" and "suc_snd (hd e # τ') = f"
using ‹e⇩1 ⋅ e⇩2 = e› ‹f⇩1 ⋅ f⇩2 = f›
unfolding hd_word[of "hd e" τ'] sucs.g.morph sucs.h.morph ‹suc_fst τ' = e⇩2› ‹suc_snd τ' = f⇩2› ‹suc_fst [hd e] = e⇩1› ‹suc_snd [hd e] = f⇩1› by force+
have "blocks (hd e # τ')"
using ‹blocks τ'› ‹e⇩1 ⋅ e⇩2 = e› ‹e⇩1 ≠ ε› ‹g e⇩1 =⇩m h f⇩1› block_ex by force
from less.prems(1)[OF _ _ this]
show thesis
by (simp add: ‹suc_fst (hd e # τ') = e› ‹suc_snd (hd e # τ') = f›)
qed
qed
lemma block_decomposition_unique: assumes "g e = h f" and
"suc_fst τ = e" and "suc_fst τ' = e" and "blocks τ" and "blocks τ'" shows "τ = τ'"
proof-
let ?C = "suc_fst⇧𝒞`(set (τ ⋅ τ'))"
have "blocks (τ ⋅ τ')"
using ‹blocks τ› ‹blocks τ'› by auto
interpret marked_code ?C
by (rule blocks_marked_code) (simp add: ‹blocks (τ ⋅ τ')›)
have "inj_on suc_fst⇧𝒞 (set (τ ⋅ τ'))"
using ‹blocks (τ ⋅ τ')› blocks_inj_suc by blast
from sucs.g.code_set_morph[OF code_axioms this ‹suc_fst τ = e›[folded ‹suc_fst τ' = e›]]
show "τ = τ'".
qed
lemma block_decomposition_unique': assumes "g e = h f" and
"suc_snd τ = f" and "suc_snd τ' = f" and "blocks τ" and "blocks τ'"
shows "τ = τ'"
proof-
have "suc_fst τ = e" and "suc_fst τ' = e"
using assms blocks_eq g.code_morph_code by presburger+
from block_decomposition_unique[OF assms(1) this assms(4-5)]
show "τ = τ'".
qed
lemma comm_sings_block: assumes "g[a] ⋅ h[b] = h[b] ⋅ g[a]"
obtains m n where "suc_fst [a] = [a]⇧@Suc m" and "suc_snd [a] = [b]⇧@Suc n"
proof-
have "[a] ⇧@ ❙|h [b]❙| ≠ ε"
using nemp_len[OF h.sing_to_nemp, of b, folded sing_pow_empty[of a "❙|h [b]❙|"]].
obtain e f where "g e =⇩m h f" and "e ≤p [a] ⇧@ ❙|h [b]❙|" and "f ≤p [b] ⇧@ ❙|g [a]❙|"
using min_coin_prefE[OF comm_common_power[OF assms,folded g.pow_morph h.pow_morph] ‹[a] ⇧@ ❙|h [b]❙| ≠ ε›, of thesis] by blast
note e = pref_sing_pow[OF ‹e ≤p [a] ⇧@ ❙|h [b]❙|›]
note f = pref_sing_pow[OF ‹f ≤p [b] ⇧@ ❙|g [a]❙|›]
from min_coinD'[OF ‹g e =⇩m h f›]
have exps: "❙|e❙| = Suc (❙|e❙| - 1)" "❙|f❙| = Suc (❙|f❙| - 1)"
by auto
have "hd e = a"
using ‹e = [a] ⇧@ ❙|e❙|›[unfolded pow_Suc[of "[a]" "❙|e❙| - 1", folded ‹❙|e❙| = Suc (❙|e❙| - 1)›], folded hd_word[of a "[a] ⇧@ (❙|e❙| - 1)"]]
list.sel(1)[of a "[a] ⇧@ (❙|e❙| - 1)"] by argo
from that suc_morph_sings[OF ‹g e =⇩m h f›, unfolded this] e f exps
show thesis
by metis
qed
definition sucs_encoding where "sucs_encoding = (λ a. hd (g [a]))"
definition sucs_decoding where "sucs_decoding = (λ a. SOME c. hd (g[c]) = a)"
lemma sucs_encoding_inv: "sucs_decoding ∘ sucs_encoding = id"
by (rule ext)
(unfold sucs_encoding_def sucs_decoding_def comp_apply id_apply, use g.marked_core[unfolded core_def] in blast)
lemma encoding_inj: "inj sucs_encoding"
unfolding sucs_encoding_def inj_on_def using g.marked_core[unfolded core_def] by blast
lemma map_encoding_inj: "inj (map sucs_encoding)"
using encoding_inj by simp
definition suc_fst' where "suc_fst' = (map sucs_encoding) ∘ suc_fst"
definition suc_snd' where "suc_snd' = (map sucs_encoding) ∘ suc_snd"
lemma encoded_sucs_eq_conv: "suc_fst w = suc_snd w' ⟷ suc_fst' w = suc_snd' w'"
unfolding suc_fst'_def suc_snd'_def using encoding_inj by force
lemma encoded_sucs_eq_conv': "suc_fst = suc_snd ⟷ suc_fst' = suc_snd'"
unfolding suc_fst'_def suc_snd'_def using inj_comp_eq[OF map_encoding_inj] by blast
lemma encoded_sucs: assumes "⋀ c. blockP c" shows "two_marked_morphisms suc_fst' suc_snd'"
unfolding suc_fst'_def suc_snd'_def
proof-
from sucs_marked_morphs[OF assms]
interpret sucs: two_marked_morphisms suc_fst suc_snd
by force
interpret nonerasing_morphism "(map sucs_encoding) ∘ suc_fst"
unfolding comp_apply by (standard, simp add: sucs.g.morph, use sucs.g.nemp_to_nemp in fast)
interpret nonerasing_morphism "(map sucs_encoding) ∘ suc_snd"
unfolding comp_apply by (standard, simp add: sucs.h.morph, use sucs.h.nemp_to_nemp in fast)
interpret marked_morphism "(map sucs_encoding) ∘ suc_fst"
proof
show "hd ((map sucs_encoding ∘ suc_fst)⇧𝒞 a) = hd ((map sucs_encoding ∘ suc_fst)⇧𝒞 b) ⟹ a = b" for a b
unfolding comp_apply core_def sucs_encoding_def hd_map[OF sucs.g.sing_to_nemp]
unfolding blockP_D_hd[OF assms] using g.marked_morph.
qed
interpret marked_morphism "(map sucs_encoding) ∘ suc_snd"
proof
show "hd ((map sucs_encoding ∘ suc_snd)⇧𝒞 a) = hd ((map sucs_encoding ∘ suc_snd)⇧𝒞 b) ⟹ a = b" for a b
unfolding comp_apply core_def sucs_encoding_def hd_map[OF sucs.h.sing_to_nemp]
using g.marked_morph[THEN sucs.h.marked_morph].
qed
show "two_marked_morphisms ((map sucs_encoding) ∘ suc_fst) ((map sucs_encoding) ∘ suc_snd)"..
qed
lemma encoded_sucs_len: "❙|suc_fst w❙| = ❙|suc_fst' w❙|" and "❙|suc_snd w❙| = ❙|suc_snd' w❙|"
unfolding suc_fst'_def suc_snd'_def sucs_encoding_def comp_apply by force+
end
end