diff --git a/metadata/entries/Combinatorics_Words.toml b/metadata/entries/Combinatorics_Words.toml
--- a/metadata/entries/Combinatorics_Words.toml
+++ b/metadata/entries/Combinatorics_Words.toml
@@ -1,42 +1,46 @@
title = "Combinatorics on Words Basics"
date = 2021-05-24
topics = [
"Computer science/Automata and formal languages",
]
abstract = """
We formalize basics of Combinatorics on Words. This is an extension of
existing theories on lists. We provide additional properties related
to prefix, suffix, factor, length and rotation. The topics include
prefix and suffix comparability, mismatch, word power, total and
reversed morphisms, border, periods, primitivity and roots. We also
formalize basic, mostly folklore results related to word equations:
equidivisibility, commutation and conjugation. Slightly advanced
properties include the Periodicity lemma (often cited as the Fine and
Wilf theorem) and the variant of the Lyndon-Schützenberger theorem for
-words. We support the algebraic point of view which sees words as
-generators of submonoids of a free monoid. This leads to the concepts
-of the (free) hull, the (free) basis (or code)."""
+words, including its full parametric solution. We support the algebraic point of view which sees words as generators of submonoids of a free monoid. This leads to the concepts of the (free) hull, the (free) basis (or code). We also provide relevant proof methods and a tool to generate reverse-symmetric claims."""
license = "bsd"
note = ""
[authors]
[authors.holub]
homepage = "holub_homepage"
[authors.raska]
[authors.starosta]
homepage = "starosta_homepage"
[contributors]
[notify]
holub = "holub_email"
starosta = "starosta_email"
[history]
+2022-08-24 = """
+Many updates and additions. New theories: Border_Array, Morphisms, Equations_Basic, and Binary_Code_Morphisms.
+"""
[extra]
[related]
+dois = ["10.4230/LIPIcs.ITP.2021.22"]
+pubs = ["Producing symmetrical facts for lists induced by the list reversal mapping in Isabelle/HOL", "Development repository"]
+
diff --git a/metadata/entries/Combinatorics_Words_Graph_Lemma.toml b/metadata/entries/Combinatorics_Words_Graph_Lemma.toml
--- a/metadata/entries/Combinatorics_Words_Graph_Lemma.toml
+++ b/metadata/entries/Combinatorics_Words_Graph_Lemma.toml
@@ -1,33 +1,37 @@
title = "Graph Lemma"
date = 2021-05-24
topics = [
"Computer science/Automata and formal languages",
]
abstract = """
Graph lemma quantifies the defect effect of a system of word
equations. That is, it provides an upper bound on the rank of the
system. We formalize the proof based on the decomposition of a
solution into its free basis. A direct application is an alternative
proof of the fact that two noncommuting words form a code."""
license = "bsd"
note = ""
[authors]
[authors.holub]
homepage = "holub_homepage"
[authors.starosta]
homepage = "starosta_homepage"
[contributors]
[notify]
holub = "holub_email"
starosta = "starosta_email"
[history]
+2022-08-24 = """
+Reworked version. Added theory Glued_Codes.
+"""
[extra]
[related]
+pubs = ["Development repository"]
diff --git a/metadata/entries/Combinatorics_Words_Lyndon.toml b/metadata/entries/Combinatorics_Words_Lyndon.toml
--- a/metadata/entries/Combinatorics_Words_Lyndon.toml
+++ b/metadata/entries/Combinatorics_Words_Lyndon.toml
@@ -1,34 +1,36 @@
title = "Lyndon words"
date = 2021-05-24
topics = [
"Computer science/Automata and formal languages",
]
abstract = """
Lyndon words are words lexicographically minimal in their conjugacy
class. We formalize their basic properties and characterizations, in
particular the concepts of the longest Lyndon suffix and the Lyndon
factorization. Most of the work assumes a fixed lexicographical order.
Nevertheless we also define the smallest relation guaranteeing
lexicographical minimality of a given word (in its conjugacy class)."""
license = "bsd"
note = ""
[authors]
[authors.holub]
homepage = "holub_homepage"
[authors.starosta]
homepage = "starosta_homepage"
[contributors]
[notify]
holub = "holub_email"
starosta = "starosta_email"
[history]
[extra]
[related]
+dois = ["10.1007/978-3-030-81508-0_18"]
+pubs = ["Development repository"]
diff --git a/thys/Combinatorics_Words/Arithmetical_Hints.thy b/thys/Combinatorics_Words/Arithmetical_Hints.thy
--- a/thys/Combinatorics_Words/Arithmetical_Hints.thy
+++ b/thys/Combinatorics_Words/Arithmetical_Hints.thy
@@ -1,60 +1,136 @@
(* Title: CoW/Arithmetical_Hints.thy
Author: Štěpán Holub, Charles University
Author: Martin Raška, Charles University
Author: Štěpán Starosta, CTU in Prague
+
+Part of Combinatorics on Words Formalized. See https://gitlab.com/formalcow/combinatorics-on-words-formalized/
*)
theory Arithmetical_Hints
imports Main
begin
section "Arithmetical hints"
-text\In this section we give some specific auxiliary lemmas on natural integers.\
+text\In this section we give some specific auxiliary lemmas on natural numbers.\
lemma zero_diff_eq: "i \ j \ (0::nat) = j - i \ j = i"
by simp
lemma zero_less_diff': "i < j \ j - i \ (0::nat)"
by simp
lemma nat_prod_le: "m \ (0 :: nat) \ m*n \ k \ n \ k"
using le_trans[of n "m*n" k] by auto
lemma get_div: "(p :: nat) < a \ m = (m * a + p) div a"
by simp
lemma get_mod: "(p :: nat) < a \ p = (m * a + p) mod a"
by simp
lemma plus_one_between: "(a :: nat) < b \ \ b < a + 1"
by auto
-lemma quotient_smaller: "a \ 0 \ a = k * b \ b \ (a::nat)"
+lemma quotient_smaller: "k \ (0 :: nat) \ b \ k * b"
by simp
lemma mult_cancel_le: "b \ 0 \ a*b \ c*b \ a \ (c::nat)"
by simp
-lemma add_lessD2: assumes "k + m < (n::nat)" shows "m < n"
- using add_lessD1[OF assms[unfolded add.commute[of k m]]].
+lemma add_lessD2: "k + m < (n::nat) \ m < n"
+unfolding add.commute[of k] using add_lessD1.
lemma mod_offset: assumes "M \ (0 :: nat)"
obtains k where "n mod M = (l + k) mod M"
proof-
have "(l + (M - l mod M)) mod M = 0"
using mod_add_left_eq[of l M "(M - l mod M)", unfolded le_add_diff_inverse[OF mod_le_divisor[OF assms[unfolded neq0_conv]], of l] mod_self, symmetric].
from mod_add_left_eq[of "(l + (M - l mod M))" M n, symmetric, unfolded this add.commute[of 0] add.comm_neutral]
have "((l + (M - l mod M)) + n) mod M = n mod M".
from that[OF this[unfolded add.assoc, symmetric]]
show thesis.
qed
lemma assumes "q \ (0::nat)" shows "p \ p + q - gcd p q"
using gcd_le2_nat[OF \q \ 0\, of p]
by linarith
lemma less_mult_one: assumes "(m-1)*k < k" obtains "m = 0" | "m = (1::nat)"
using assms by fastforce
+lemma per_lemma_len_le: assumes le: "p + q - gcd p q \ (n :: nat)" and "q \ 0" shows "p \ n"
+ using le unfolding add_diff_assoc[OF gcd_le2_nat[OF \q \ 0\], symmetric] by (rule add_leD1)
+
+lemma predE: assumes "k \ 0" obtains pred where "k = Suc pred"
+ using assms not0_implies_Suc by auto
+
+lemma Suc_less_iff_Suc_le: "Suc n < k \ Suc n \ k - 1"
+ by auto
+
+lemma nat_induct_pair: "P 0 0 \ (\ m n. P m n \ P m (Suc n)) \ (\ m n. P m n \ P (Suc m) n) \ P m n"
+ by (induction m arbitrary: n) (metis nat_induct, simp)
+
+lemma One_less_Two_le_iff: "1 < k \ 2 \ (k :: nat)"
+ by fastforce
+
+lemma at_least2_Suc: assumes "2 \ k"
+ obtains k' where "k = Suc(Suc k')"
+ using Suc3_eq_add_3 less_eqE[OF assms] by auto
+
+lemma at_least3_Suc: assumes "3 \ k"
+ obtains k' where "k = Suc(Suc(Suc k'))"
+ using Suc3_eq_add_3 less_eqE[OF assms] by auto
+
+lemma two_three_add_le_mult: assumes "2 \ (l::nat)" and "3 \ k" shows "l + k + 1 \ l*k"
+proof-
+ obtain l' where l: "l = Suc (Suc l')"
+ using \2 \ l\ at_least2_Suc[OF \2 \ l\] by blast
+ obtain k' where k: "k = Suc (Suc (Suc k'))"
+ using \3 \ k\ at_least3_Suc[OF \3 \ k\] by blast
+ show "l + k + 1 \ l*k"
+ unfolding l k
+ by (induct l' k' rule: nat_induct_pair, simp, simp add: add.commute[of "Suc (Suc l')"] mult.commute[of "Suc (Suc l')"], simp_all)
+qed
+
+lemmas not0_SucE = not0_implies_Suc[THEN exE]
+
+lemma le1_SucE: assumes "1 \ n"
+ obtains k where "n = Suc k" using Suc_le_D[OF assms[unfolded One_nat_def]] by blast
+
+lemma Suc_minus: "k \ 0 \ Suc (k - 1) = k"
+ by simp
+
+lemma Suc_minus': "1 \ k \ Suc(k - 1) = k"
+ by simp
+
+lemmas Suc_minus'' = Suc_diff_1
+
+lemma Suc_minus2: "2 \ k \ Suc (Suc(k - 2)) = k"
+ by auto
+
+lemma almost_equal_equal: assumes "(a:: nat) \ 0" and "b \ 0" and eq: "k*(a+b) + a = m*(a+b) + b"
+ shows "k = m" and "a = b"
+proof-
+ show "k = m"
+ proof (rule linorder_cases[of k m])
+ assume "k < m"
+ from add_le_mono1[OF mult_le_mono1[OF Suc_leI[OF this]]]
+ have "(Suc k)*(a + b) + b \ m*(a+b) + b".
+ hence False
+ using \b \ 0\ unfolding mult_Suc eq[symmetric] by force
+ thus ?thesis by blast
+ next
+ assume "m < k"
+ from add_le_mono1[OF mult_le_mono1[OF Suc_leI[OF this]]]
+ have "(Suc m)*(a + b) + a \ k*(a+b) + a".
+ hence False
+ using \a \ 0\ unfolding mult_Suc eq by force
+ thus ?thesis by blast
+ qed (simp)
+ thus "a = b"
+ using eq by auto
+qed
+
+
end
\ No newline at end of file
diff --git a/thys/Combinatorics_Words/Binary_Code_Morphisms.thy b/thys/Combinatorics_Words/Binary_Code_Morphisms.thy
new file mode 100644
--- /dev/null
+++ b/thys/Combinatorics_Words/Binary_Code_Morphisms.thy
@@ -0,0 +1,1354 @@
+(* Title: Binary Code Morphisms
+ File: CoW.Binary_Code_Morphisms
+ Author: Štěpán Holub, Charles University
+
+Part of Combinatorics on Words Formalized. See https://gitlab.com/formalcow/combinatorics-on-words-formalized/
+*)
+
+theory Binary_Code_Morphisms
+ imports CoWBasic Submonoids Morphisms
+
+begin
+
+chapter "Binary alphabet and binary morphisms"
+
+section "Datatype of a binary alphabet"
+
+text\Basic elements for construction of binary words.\
+
+type_notation Enum.finite_2 ("binA")
+notation finite_2.a\<^sub>1 ("bin0")
+notation finite_2.a\<^sub>2 ("bin1")
+
+lemmas bin_distinct = Enum.finite_2.distinct
+lemmas bin_exhaust = Enum.finite_2.exhaust
+lemmas bin_induct = Enum.finite_2.induct
+lemmas bin_UNIV = Enum.UNIV_finite_2
+lemmas bin_eq_neq_iff = Enum.neq_finite_2_a\<^sub>2_iff
+lemmas bin_eq_neq_iff' = Enum.neq_finite_2_a\<^sub>1_iff
+
+abbreviation bin_word_0 :: "binA list" ("\") where
+ "bin_word_0 \ [bin0]"
+
+abbreviation bin_word_1 :: "binA list" ("\") where
+ "bin_word_1 \ [bin1]"
+
+abbreviation binUNIV :: "binA set" where "binUNIV \ UNIV"
+
+lemma bin_basis_code: "code {\,\}"
+ by (rule bin_code_code) blast
+
+lemma bin_num: "bin0 = 0" "bin1 = 1"
+ by simp_all
+
+lemma binsimp[simp]: "bin0 - bin1 = bin1" "bin1 - bin0 = bin1" "1 - bin0 = bin1" "1 - bin1 = bin0" "a - a = bin0" "1 - (1 - a) = a"
+ by simp_all
+
+definition bin_swap :: "binA \ binA" where "bin_swap x \ 1 - x"
+
+lemma bin_swap_if_then: "1-x = (if x = bin0 then bin1 else bin0)"
+ by fastforce
+
+definition bin_swap_morph where "bin_swap_morph \ map bin_swap"
+
+lemma alphabet_or[simp]: "a = bin0 \ a = bin1"
+ by auto
+
+lemma bin_im_or: "f [a] = f \ \ f [a] = f \"
+ by (rule bin_exhaust[of a], simp_all)
+
+thm triv_forall_equality
+
+lemma binUNIV_card: "card binUNIV = 2"
+ unfolding bin_UNIV card_2_iff by auto
+
+lemma other_letter: obtains b where "b \ (a :: binA)"
+ using finite_2.distinct(1) by metis
+
+lemma alphabet_or_neq: "x \ y \ x = (a :: binA) \ y = a"
+ using alphabet_or[of x] alphabet_or[of y] alphabet_or[of a] by argo
+
+lemma binA_neq_cases: assumes neq: "a \ b"
+ obtains "a = bin0" and "b = bin1" | "a = bin1" and "b = bin0"
+ using alphabet_or_neq assms by auto
+
+lemma bin_neq_sym_pred: assumes "a \ b" and "P bin0 bin1" and "P bin1 bin0" shows "P a b"
+ using assms(2-3) binA_neq_cases[OF \a \ b\, of "P a b"] by blast
+
+lemma no_third: "(c :: binA) \ a \ b \ a \ b = c"
+ using alphabet_or[of a] by fastforce
+
+lemma two_in_bin_UNIV: assumes "a \ b" and "a \ S" and "b \ S" shows "S = binUNIV"
+ using \a \ S\ \b \ S\ alphabet_or_neq[OF \a \ b\] by fast
+
+lemmas two_in_bin_set = two_in_bin_UNIV[unfolded bin_UNIV]
+
+lemma bin_not_comp_set_UNIV: assumes "\ u \ v" shows "set (u \ v) = binUNIV"
+proof-
+ have uv: "u \ v = ((u \\<^sub>p v) \ ([hd ((u \\<^sub>p v)\\<^sup>>u)] \ tl ((u \\<^sub>p v)\\<^sup>>u))) \ (u \\<^sub>p v) \ ([hd ((u \\<^sub>p v)\\<^sup>>v)] \ tl ((u \\<^sub>p v)\\<^sup>>v))"
+ unfolding hd_tl[OF lcp_mismatch_lq(1)[OF assms]] hd_tl[OF lcp_mismatch_lq(2)[OF assms]] lcp_lq..
+ from this[unfolded rassoc]
+ have "hd ((u \\<^sub>p v)\\<^sup>>u) \ set (u \ v)" and "hd ((u \\<^sub>p v)\\<^sup>>v) \ set (u \ v)"
+ unfolding uv by simp_all
+ with lcp_mismatch_lq(3)[OF assms]
+ show ?thesis
+ using two_in_bin_UNIV by blast
+qed
+
+lemma bin_basis_singletons: "{[q] |q. q \ {bin0, bin1}} = {\,\}"
+ by blast
+
+lemma bin_basis_generates: "\{\,\}\ = UNIV"
+ using sings_gen_lists[of binUNIV, unfolded lists_UNIV bin_UNIV bin_basis_singletons, folded bin_UNIV, unfolded lists_UNIV].
+
+lemma a_in_bin_basis: "[a] \ {\,\}"
+ using Set.UNIV_I by auto
+
+lemma lcp_zero_one_emp: "\ \\<^sub>p \ = \" and lcp_one_zero_emp: "\ \\<^sub>p \ = \"
+ by simp+
+
+lemma neq_induct: "(a::binA) \ b \ P a \ P b \ P c"
+ by (elim binA_neq_cases) (hypsubst, rule finite_2.induct, assumption+)+
+
+lemma neq_exhaust: assumes "(a::binA) \ b" obtains "c = a" | "c = b"
+ using assms by (elim binA_neq_cases) (hypsubst, elim finite_2.exhaust, assumption)+
+
+lemma bin_swap_neq [simp]: "1-(a :: binA) \ a"
+ by simp
+lemmas bin_swap_neq'[simp] = bin_swap_neq[symmetric]
+
+lemmas bin_swap_induct = neq_induct[OF bin_swap_neq']
+ and bin_swap_exhaust = neq_exhaust[OF bin_swap_neq']
+
+lemma bin_swap_induct': "P (a :: binA) \ P (1-a) \ (\ c. P c)"
+ using bin_swap_induct by auto
+
+lemma bin_UNIV_swap: "{a, 1-a} = binUNIV" (is "?P a")
+ using bin_swap_induct[of ?P bin0, unfolded binsimp] by fastforce
+
+lemma neq_bin_swap: "c \ d \ d = 1-(c :: binA)"
+ by (rule bin_swap_exhaust[of d c]) blast+
+
+lemma neq_bin_swap': "c \ d \ c = 1-(d :: binA)"
+ using neq_bin_swap by presburger
+
+lemma bin_neq_iff: "c \ d \ d = 1-(c :: binA)"
+ using neq_bin_swap[of c d] bin_swap_neq[of c] by argo
+
+lemma bin_neq_iff': "c \ d \ c = 1-(d :: binA)"
+ unfolding bin_neq_iff by force
+
+lemma bin_neq_swap': "a \ b \ b = 1-(a:: binA)"
+ by (simp add: bin_neq_iff')
+
+lemma binA_neq_cases_swap: assumes neq: "a \ (b :: binA)"
+ obtains "a = c" and "b = 1 - c" | "a = 1 - c" and "b = c"
+ using bin_neq_swap'[OF assms] bin_swap_exhaust by auto
+
+lemma bin_without_letter: assumes "(a1 :: binA) \ set w"
+ obtains k where "w = [1-a1]\<^sup>@k"
+proof-
+ have "\ c. c \ set w \ c = 1-a1"
+ using assms bin_swap_exhaust by blast
+ from that unique_letter_wordE'[OF this]
+ show thesis by blast
+qed
+
+lemma bin_neq_swap[intro]: "a \ b \ a = 1-(b:: binA)"
+ by (simp add: bin_neq_iff')
+
+lemma bin_empty_iff: "S = {} \ (a :: binA) \ S \ 1-a \ S"
+ using bin_swap_induct[of "\a. a \ S"] by blast
+
+lemma bin_UNIV_iff: "S = binUNIV \ a \ S \ 1-a \ S"
+ using two_in_bin_UNIV[OF bin_swap_neq'] by blast
+
+lemma bin_UNIV_I: "a \ S \ 1-a \ S \ S = binUNIV"
+ using bin_UNIV_iff by blast
+
+lemma swap_UNIV: "{a,1-a} = binUNIV"
+ unfolding bin_UNIV_iff[of "{a,1-a}" a] by fast
+
+lemma bin_sing_iff: "A = {a :: binA} \ a \ A \ 1-a \ A"
+proof (rule sym, intro iffI conjI, elim conjE)
+ assume "a \ A" and "1-a \ A"
+ have "b \ A \ b = a" for b
+ using \a \ A\ \1-a \ A\ bin_swap_neq
+ by (intro bin_swap_induct[of "\c. (c \ A) = (c = a)" a b]) blast+
+ then show "A = {a}" by blast
+qed simp_all
+
+lemma bin_set_cases: obtains "S = {}" | "S = {bin0}" | "S = {bin1}" | "S = binUNIV"
+ unfolding bin_empty_iff[of _ "bin0"] bin_UNIV_iff[of _ "bin0"] bin_sing_iff
+ by fastforce
+
+lemma not_UNIV_E: assumes "A \ binUNIV" obtains a where "A \ {a}"
+ using assms by (cases rule: bin_set_cases[of A]) auto
+
+lemma not_UNIV_nempE: assumes "A \ binUNIV" and "A \ {}" obtains a where "A = {a}"
+ using assms by (cases rule: bin_set_cases[of A]) auto
+
+lemma bin_sing_gen_iff: "x \ \{[a]}\ \ 1-(a :: binA) \ set x"
+ unfolding sing_gen_lists[symmetric] in_lists_conv_set using bin_empty_iff bin_sing_iff by metis
+
+lemma set_hd_pow_conv: "w \ [hd w]* \ set w \ binUNIV"
+ unfolding root_sing_set_iff
+proof
+ assume "set w \ {hd w}"
+ thus "set w \ binUNIV"
+ unfolding bin_UNIV using bin_distinct(1) by force
+next
+ assume "set w \ binUNIV"
+ thus "set w \ {hd w}"
+ proof (cases "w = \", simp)
+ assume "set w \ binUNIV" and "w \ \"
+ from hd_tl[OF this(2)] this(2)
+ have "hd w \ set w" by simp
+ hence "1-hd w \ set w"
+ using \