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[simp]: "(map f⇧𝒞 w) ∈ lists (range f⇧𝒞)"
by auto
lemma comp_core: "(f ∘ g)⇧𝒞 = f ∘ g⇧𝒞"
unfolding core_def
by auto
lemma ext_core_id [simp]: "f⇧ℒ⇧𝒞 = f"
unfolding list_extension_def core_def by simp
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_on[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_on: "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⟩"
unfolding set_eq_iff
proof
have elem1: "x ∈ ⟨f ` A⟩ ⟷ (∃ ws. ws ∈ lists A ∧ x = concat (map f ws))" for x
unfolding hull_concat_lists unfolding lists_image
by blast
have elem2: "x ∈ f ` ⟨A⟩ ⟷ (∃ ws. ws ∈ lists A ∧ x = f (concat ws))" for x
by blast
show "x ∈ ⟨f ` A⟩ ⟷ x ∈ f ` ⟨A⟩" for x
unfolding elem1 elem2
using morph_concat_concat_map_on by force
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 gen_idemp 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_gen 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_gen 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_on ‹ε ∉ 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_on[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_gen ‹y ∈ 𝔅 ⟨A⟩›] hull_closed_lists[OF ‹ys ∈ lists ⟨A⟩›] by blast
hence "❙|ys❙| = 1"
using basisD[OF ‹y ∈ 𝔅 ⟨A⟩›] ungen_dec_triv'[OF ‹ys ∈ lists (⟨A⟩ - {ε})›] by simp
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 "xs = map f xs'" and "ys' ∈ lists A" and "ys = map f ys'"
unfolding lists_image by blast
assume "concat xs = concat ys"
hence "f (concat xs') = f (concat ys')"
using morph_concat_concat_map_on lists_mono[OF genset_sub]
‹xs' ∈ lists A› ‹ys' ∈ lists A›
unfolding ‹xs = map f xs'› ‹ys = map f ys'› subset_iff by metis
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 ‹xs = map f xs'› ‹ys = map f 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)
lemmas emp_to_emp = emp_to_emp_on
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_all: "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[intro]: "(⋀ 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 im_exp :: "'a list ⇒ nat" where "im_exp u ≡ (SOME n. f u = 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_im_exp:
"f u = mroot⇧@im_exp u"
unfolding im_exp_def
using per_morph_rootI tfl_some by meson
lemma mroot_primroot: assumes "f u ≠ ε"
shows "mroot = ρ (f u)"
using per_morph_rootI primroot_unique[OF ‹f u ≠ ε› per_morph_root_prim, symmetric] by blast
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 per_morph_rev_map: "rev_map f u = rev (f u)"
proof (induct u, simp)
case (Cons a u)
show ?case
unfolding hd_word[of a u] morph morphism.morph[OF rev_map_morph] rev_append Cons.hyps
ims_comm cancel_right rev_map_sing..
qed
lemma mroot_rev: "mirror.mroot = rev mroot"
proof-
obtain u where "f u ≠ ε"
using not_triv_emp by auto
hence "rev (f u) ≠ ε"
by blast
show ?thesis
unfolding per_morph_rev_map mirror.mroot_primroot[unfolded per_morph_rev_map, OF ‹rev (f u) ≠ ε›]
mroot_primroot[OF ‹f u ≠ ε›] primroot_rev..
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
using nonerasing[of "rev w"]
unfolding rev_map_arg rev_is_Nil_conv.
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 add: pow_list_2)
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 prefix_code_morphism = nonerasing_morphism +
assumes
pref_free: "f⇧𝒞 a ≤p f⇧𝒞 b ⟹ a = b"
begin
interpretation prefrange: prefix_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
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 (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_all
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 prefix_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. ε))"
proof
show "⌈f⌉ = 0 ⟹ f = (λw. ε)"
using max_im_len_le[OF assms] by fastforce
show "f = (λw. ε) ⟹ ⌈f⌉ = 0"
unfolding max_image_length_def core_def by force
qed
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]
lemma Cons_im: "f (x#xs) = f⇧𝒞 x ⋅ f xs"
unfolding core_sing using pop_hd.
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
subsection ‹Decomposition into primitive roots›
definition root_refine ("Ref⇩ρ _" [55] 56) where "root_refine = (λ x. [ρ x]⇧@e⇩ρ x)⇧ℒ"
lemma root_ref_morph: "morphism root_refine"
unfolding root_refine_def using list_ext_morph.
thm morphism.morph_concat_concat_map
interpretation rr_morph: morphism root_refine
using root_ref_morph by blast
lemma root_ref_def: "Ref⇩ρ us = concat (map (λ x. [ρ x]⇧@e⇩ρ x) us)"
unfolding root_refine_def list_extension_def..
lemma root_ref_refines: "concat (Ref⇩ρ ws) = concat ws"
proof (induct ws)
case (Cons a ws)
show ?case
unfolding rr_morph.Cons_im concat_morph concat.simps Cons.hyps
by (simp add: root_refine_def)
qed simp
lemmas root_ref_emp = rr_morph.emp_to_emp
lemma "Ref⇩ρ [ε,ε] = ε"
unfolding root_ref_def by force
lemma root_ref_empty_conv: "Ref⇩ρ us = ε ⟷ set us ⊆ {ε}"
proof
show "set us ⊆ {ε} ⟹ Ref⇩ρ us = ε"
unfolding root_ref_def by auto
show "Ref⇩ρ us = ε ⟹ set us ⊆ {ε}"
unfolding root_ref_def
proof (induction us, force)
case (Cons a us)
hence "[ρ a] ⇧@ e⇩ρ a = ε" and hyp: "concat (map (λx. [ρ x] ⇧@ e⇩ρ x) us) = ε"
unfolding list.simps concat.simps by fast+
hence "a = ε"
by blast
from Cons.IH[OF hyp]
obtain k where "[ε]⇧@k = us"
by blast
show ?case
using ‹a = ε› ‹set us ⊆ {ε}› by simp
qed
qed
lemma root_ref_hd: assumes "x ≠ ε"
shows "hd (Ref⇩ρ (x#xs)) = ρ x"
unfolding root_ref_def by (simp_all add: hd_append ‹x ≠ ε› hd_sing_pow)
lemma root_ref_injective:
assumes
emp_not_in: "ε ∉ 𝒞" and
comm_eq: "⋀ x y. x ∈ 𝒞 ⟹ y ∈ 𝒞 ⟹ x ⋅ y = y ⋅ x ⟹ x = y" and
"us ∈ lists 𝒞" "vs ∈ lists 𝒞"
shows "Ref⇩ρ us = Ref⇩ρ vs ⟹ us = vs"
using assms(3-4)
proof (induction rule: list_induct2')
case (4 x xs y ys)
show ?case
proof (rule arg_cong2[of x y xs ys])
have "x ≠ ε" "y ≠ ε" "x ∈ 𝒞" "y ∈ 𝒞" "xs ∈ lists 𝒞" "ys ∈ lists 𝒞"
using ‹x # xs ∈ lists 𝒞› ‹y # ys ∈ lists 𝒞› emp_not_in by auto
from root_ref_hd[OF ‹x ≠ ε›, of xs] root_ref_hd[OF ‹y ≠ ε›, of ys]
have "ρ x = ρ y"
unfolding "4.prems"(1) by presburger
from same_primroots_comm[OF this, THEN comm_eq[OF ‹x ∈ 𝒞› ‹y ∈ 𝒞›]]
show "x = y".
from "4.prems"(1)[unfolded this] "4.IH"[OF _ ‹xs ∈ lists 𝒞› ‹ys ∈ lists 𝒞›]
show "xs = ys"
unfolding rr_morph.Cons_im cancel by blast
qed
qed (simp_all add: root_ref_def emp_not_in)
lemma (in code) code_root_ref_injective:
assumes "us ∈ lists 𝒞" "vs ∈ lists 𝒞"
shows "Ref⇩ρ us = Ref⇩ρ vs ⟹ us = vs"
using root_ref_injective[OF emp_not_in code_comm_eq assms].
find_theorems "set ?w = {?a}"
lemma (in code) code_roots_non_overlapping: "non_overlapping ((λ x. [ρ x]⇧@(e⇩ρ x)) ` 𝒞)"
proof
show nemp_dec: "ε ∉ (λ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_pow_list_single 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) ` 𝒞"
have "us ≠ ε" "vs ≠ ε"
using us' vs' nemp_dec by blast+
from us'[unfolded image_iff]
obtain u where "u ∈ 𝒞" and us: "us = [ρ u] ⇧@ e⇩ρ u" and "0 < e⇩ρ u"
using ‹us ≠ ε› by fastforce
from vs'[unfolded image_iff]
obtain v where "v ∈ 𝒞" and vs: "vs = [ρ v] ⇧@ e⇩ρ v" and "0 < e⇩ρ v"
using ‹vs ≠ ε› by fastforce
have "set us = {ρ u}"
using us ‹0 < e⇩ρ u› ..
have "set vs = {ρ v}"
using vs ‹0 < e⇩ρ v› ..
show "us = vs" if "zs ≤p us" and "zs ≤s vs" and "zs ≠ ε" for zs
proof-
have "set zs = {ρ u}"
using set_mono_prefix[OF ‹zs ≤p us›] ‹zs ≠ ε› unfolding ‹set us = {ρ u}› by auto
have "set zs = {ρ v}"
using set_mono_suffix[OF ‹zs ≤s vs›] ‹zs ≠ ε› unfolding ‹set vs = {ρ v}› by auto
hence "ρ u = ρ v"
unfolding ‹set zs = {ρ u}› by simp
from same_primroots_comm[OF this]
have "u = v"
using code_comm_eq [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 ‹set us = {ρ u}› ‹set vs = {ρ v}›
have "ρ u = ρ v"
using set_mono_sublist[OF ‹us ≤f vs›] by force
from same_primroots_comm[OF this]
have "u = v"
using code_comm_eq [OF ‹u ∈ 𝒞› ‹v ∈ 𝒞›] by blast
thus "us = vs"
unfolding ‹us = [ρ u] ⇧@ e⇩ρ u› ‹vs = [ρ v] ⇧@ e⇩ρ v› by blast
qed
qed
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
theorem (in code) roots_prim_morph:
assumes "ws ∈ lists 𝒞"
and "❙|ws❙| ≠ 1"
and "primitive ws"
shows "primitive (Ref⇩ρ ws)"
proof-
let ?R = "λ x. [ρ x]⇧@(e⇩ρ x)"
interpret rc: non_overlapping "?R ` 𝒞"
using code_roots_non_overlapping.
show ?thesis
unfolding root_ref_def
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 ‹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' ≤p r ∧ r' ≠ ε ∧ s' ≤p s ∧ 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' ≤p r ⟹ r' ≠ ε ⟹ s' ≤p s ⟹ s' ≠ ε ⟹ g r' = h s' ⟹ r' = r ∧ s' = s"
unfolding 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' ≤p r ⟹ r' ≠ ε ⟹ s' ≤p s ⟹ s' ≠ ε ⟹ g r' = h s' ⟹ r' = r ∧ s' = s)"
shows "g r =⇩m h s"
unfolding min_coin_def[rule_format] using assms by auto
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 k "ρ sol", symmetric] h.pow_morph[of k "ρ sol", 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 exp "g (ρ u')" "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_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 "Factor intepretation of morphic images"
context morphism
begin
lemma image_fac_interp': assumes "w ≤f f z" "w ≠ ε"
obtains p w_pred s where "w_pred ≤f z" "p w s ∼⇩ℐ (map f⇧𝒞 w_pred)"
proof-
let ?fzs = "map f⇧𝒞 z"
have "w ≤f concat (map f⇧𝒞 z)"
by (simp add: assms(1) morph_concat_map)
from fac_fac_interpE'[OF ‹w ≤f concat (map f⇧𝒞 z)› ‹w ≠ ε›]
obtain p s ws where "p w s ∼⇩ℐ ws" "ws ≤f ?fzs"
by blast
obtain w_pred where "ws = map f⇧𝒞 w_pred" "w_pred ≤f z"
using ‹ws ≤f map f⇧𝒞 z› sublist_map_rightE by blast
show ?thesis
using ‹p w s ∼⇩ℐ ws› ‹w_pred ≤f z› ‹ws = map f⇧𝒞 w_pred› that by blast
qed
lemma image_fac_interp: assumes "u⋅w⋅v = f z" "w ≠ ε"
obtains p w_pred s u_pred v_pred where
"u_pred⋅w_pred⋅v_pred = z" "p w s ∼⇩ℐ (map f⇧𝒞 w_pred)"
"u = (f u_pred)⋅p" "v = s⋅(f v_pred)"
proof-
let ?fzs = "map f⇧𝒞 z"
have "u⋅w⋅v = concat (map f⇧𝒞 z)"
by (simp add: assms(1) morph_concat_map)
from fac_fac_interpE[OF ‹u⋅w⋅v = concat (map f⇧𝒞 z)› ‹w ≠ ε›]
obtain ps ss p s ws where "p w s ∼⇩ℐ ws" "ps⋅ws⋅ss = ?fzs" "concat ps ⋅ p = u" "s ⋅ concat ss = v"
by metis
obtain w_pred u_pred v_pred where "ws = map f⇧𝒞 w_pred" "ps = map f⇧𝒞 u_pred"
"ss = map f⇧𝒞 v_pred" "u_pred⋅w_pred⋅v_pred = z"
using ‹ps ⋅ ws ⋅ ss = map f⇧𝒞 z›[unfolded append_eq_map_conv]
by blast
show ?thesis
using ‹concat ps ⋅ p = u› ‹p w s ∼⇩ℐ ws› ‹ps = map f⇧𝒞 u_pred› ‹s ⋅ concat ss = v› ‹ss = map f⇧𝒞 v_pred› ‹u_pred ⋅ w_pred ⋅ v_pred = z› ‹ws = map f⇧𝒞 w_pred› morph_concat_map that by blast
qed
lemma image_fac_interp_mid: assumes "p w s ∼⇩ℐ map f⇧𝒞 w_pred" "2 ≤ ❙|w_pred❙|"
obtains pw sw where
"w = pw ⋅ (f (butlast (tl w_pred))) ⋅ sw" "p⋅pw = f [hd w_pred]" "sw⋅s = f [last w_pred]"
proof-
note fac_interpD[OF ‹p w s ∼⇩ℐ map f⇧𝒞 w_pred›, unfolded morph_concat_map]
note butl = hd_middle_last[OF ‹2 ≤ ❙|w_pred❙|›[folded One_less_Two_le_iff]]
have "w_pred ≠ ε"
using assms(2) by force
obtain pw' where
"p ⋅ pw' = hd (map f⇧𝒞 w_pred)"
using sprefE[OF ‹p <p hd (map f⇧𝒞 w_pred)›] prefixE by metis
hence pw': "p ⋅ pw' = f [hd w_pred]"
unfolding core_def
unfolding hd_map[OF ‹w_pred ≠ ε›, of "f⇧𝒞", unfolded core_def].
obtain sw' where
"sw' ⋅ s = last (map f⇧𝒞 (w_pred))"
using sprefE[reversed, OF ‹s <s last (map f⇧𝒞 w_pred)›] suffix_def by metis
hence sw' : "sw' ⋅ s = f [last (w_pred)]"
unfolding core_def
unfolding last_map[OF ‹w_pred ≠ ε›, of "f⇧𝒞", unfolded core_def].
have "w = pw' ⋅ f (butlast (tl w_pred)) ⋅ sw'"
using ‹p ⋅ w ⋅ s = f w_pred›[unfolded arg_cong[OF butl[symmetric], of f]]
unfolding morph
unfolding pw'[symmetric] sw'[symmetric]
by simp
thus ?thesis
using pw' sw' that by blast
qed
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' ≤p rev r" "r' ≠ ε" "s' ≤p rev s" "s' ≠ ε" "rev_map g r' = rev_map h s'"
then obtain r'' s'' where "r''⋅ rev r' = r" and "s''⋅ rev s' = s"
using ‹s' ≤p rev s› ‹r' ≤p 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' ≤p rev r› ‹r' ≠ ε› ‹r'' ⋅ rev r' = r› by auto
hence "r'' = ε ∨ s'' = ε"
using min_coin_minD[OF ‹g r =⇩m h s› _ _ _ _ ‹g r'' = h s''›, THEN conjunct1]
‹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' ≤p e" and "e' ≠ ε" and "f' ⨝ f"
shows "e' = e" and "f' = f"
proof-
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
with ‹g e =⇩m h f›[unfolded min_coin_def]
show "e' = e" and "f' = f"
using ‹g e' = h f'› ‹e' ≤p e› ‹e' ≠ ε› ‹f' ≠ ε› 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' ≤p e ⟹ r'≠ ε⟹ s' ≤p f ⟹ s' ≠ ε ⟹ g r' = h s' ⟹ r' = e ∧ s' = f" for r' s'
proof-
assume "r' ≤p e" and "r' ≠ ε" and "s' ≤p f" and "s' ≠ ε" and "g r' = h s'"
hence "P ❙|r'❙|"
unfolding P_def using ‹e ≤p r› ‹f ≤p s› ‹r' ≠ ε›
pref_trans[OF ‹r' ≤p e› ‹e ≤p r›]
pref_trans[OF ‹s' ≤p 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 ‹r' ≤p e›] by blast
from ‹g e = h f›[folded this, unfolded ‹g r' = h s'›] this
show ?thesis
using ‹s' ≤p f› 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_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 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_all 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 force+
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
show "e ≤p e'" and "f ≤p f'"
using min_coin_minD[OF assms(1) lcp_pref ‹e ∧⇩p e' ≠ ε› lcp_pref ‹f ∧⇩p 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 "set w ⊆ {hd w}")
assume "set w ⊆ {hd w}"
then obtain l where "w = [hd w]⇧@l"
by blast
from nemp_exp_pos[OF ‹w ≠ ε›, of l "[hd w]", folded this]
have "0 < l"
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 ‹0 < l›
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 "¬ set 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 "m-1" t, 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 blockP_D[OF assms, THEN 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 auto
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] by simp
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_pow_list_iff[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 "❙|e❙| - 1" "[a]", 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 unfold_locales
(use sucs.g.morph sucs.g.nemp_to_nemp in auto)
interpret nonerasing_morphism "(map sucs_encoding) ∘ suc_snd"
by unfold_locales
(use sucs.h.morph sucs.h.nemp_to_nemp in auto)
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