diff --git a/metadata/entries/Binary_Code_Imprimitive.toml b/metadata/entries/Binary_Code_Imprimitive.toml
--- a/metadata/entries/Binary_Code_Imprimitive.toml
+++ b/metadata/entries/Binary_Code_Imprimitive.toml
@@ -1,38 +1,42 @@
title = "Binary codes that do not preserve primitivity"
date = 2023-01-03
topics = [
"Computer science/Automata and formal languages",
]
abstract = """
A code $X$ is not primitivity preserving if there is a primitive list $\\mathtt{ws} \\in \\mathtt{lists} \\ X$ whose concatenation is imprimitive. We formalize a full characterization of such codes in the binary case in the proof assistant Isabelle/HOL. Part of the formalization, interesting on its own, is a description of $\\{x,y\\}$-interpretations of the square $xx$ if $\\mathtt{length}\\ y \\leq \\mathtt{length} \\ x$. We also provide a formalized parametric solution of the related equation $x^jy^k = z^\\ell$.
The core of the theory is an investigation of imprimitive words which are concatenations of copies of two noncommuting words (such a pair of words is called a binary code). We follow the article [Barbin-Le Rest, Le Rest, 85] (mainly Théorème 2.1 and Lemme 3.1), while substantially optimizing the proof. See also [J.-C. Spehner. Quelques problèmes d’extension, de conjugaison et de présentation des sous-monoïdes d’un monoïde libre. PhD thesis, Université Paris VII, 1976] for an earlier result on this question, and [Maňuch, 01] for another proof."""
license = "bsd"
note = ""
[authors]
[authors.holub]
email = "holub_email"
[authors.raska]
[contributors]
[notify]
holub = "holub_email"
starosta = "starosta_email"
[history]
+2023-08-17 = """
+Updated to version v1.10.1.
+"""
[extra]
[related]
dois = [
+ "10.1007/s10817-023-09674-2",
"10.1016/0304-3975(85)90060-X",
"10.46298/dmtcs.279",
]
pubs = [
"J.-C. Spehner. Quelques problèmes d’extension, de conjugaison et de présentation des sous-monoïdes d’un monoïde libre. PhD thesis, Université Paris VII, 1976",
"Development repository",
]
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,46 +1,49 @@
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, 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]
+2023-08-17 = """
+Updated to version v1.10.1.
+"""
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,37 +1,42 @@
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.raska]
+
[authors.starosta]
homepage = "starosta_homepage"
[contributors]
[notify]
holub = "holub_email"
starosta = "starosta_email"
[history]
+2023-08-17 = """
+Updated to version v1.10.1.
+"""
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,36 +1,39 @@
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]
+2023-08-17 = """
+Updated to version v1.10.1.
+"""
[extra]
[related]
dois = ["10.1007/978-3-030-81508-0_18"]
pubs = ["Development repository"]
diff --git a/metadata/entries/Two_Generated_Word_Monoids_Intersection.toml b/metadata/entries/Two_Generated_Word_Monoids_Intersection.toml
--- a/metadata/entries/Two_Generated_Word_Monoids_Intersection.toml
+++ b/metadata/entries/Two_Generated_Word_Monoids_Intersection.toml
@@ -1,41 +1,44 @@
title = "Intersection of two monoids generated by two element codes"
date = 2023-01-03
topics = [
"Computer science/Automata and formal languages",
]
abstract = """
This article provides a formalization of the classification of intersection
\\( \\{x,y\\}^* \\cap \\{u,v\\}^*\\) of two monoids generated by two element codes.
Namely, the intersection has one of the following forms
\\( \\{\\beta,\\gamma\\}^* \\quad \\text{ or } \\quad \\left(\\beta_0 + \\beta(\\gamma(1+\\delta+ \\cdots + \\delta^t))^*\\epsilon\\right)^*.\\)
Note that it can be infinitely generated.
The result is due to [Karhumäki, 84]. Our proof uses the terminology of morphisms which allows us to formulate the result in a shorter and more transparent way."""
license = "bsd"
note = ""
[authors]
[authors.holub]
email = "holub_email"
[authors.starosta]
email = "starosta_email"
[contributors]
[notify]
holub = "holub_email"
starosta = "starosta_email"
[history]
+2023-08-17 = """
+Updated to version v1.10.1.
+"""
[extra]
[related]
dois = [
"10.1007/BFb0036924",
]
pubs = [
"Development repository",
]
diff --git a/thys/Binary_Code_Imprimitive/Binary_Code_Imprimitive.thy b/thys/Binary_Code_Imprimitive/Binary_Code_Imprimitive.thy
--- a/thys/Binary_Code_Imprimitive/Binary_Code_Imprimitive.thy
+++ b/thys/Binary_Code_Imprimitive/Binary_Code_Imprimitive.thy
@@ -1,1168 +1,1156 @@
(* Title: Binary Code Imprimitive
- File: Combinatorics_Words_Interpretations.Binary_Code_Imprimitive
+ File: Binary_Code_Imprimitive.Binary_Code_Imprimitive
Author: Štěpán Holub, Charles University
Author: Martin Raška, Charles University
Part of Combinatorics on Words Formalized. See https://gitlab.com/formalcow/combinatorics-on-words-formalized/
*)
-chapter "Binary codes that do not preserve primitivity"
-
theory Binary_Code_Imprimitive
- imports
- Combinatorics_Words_Graph_Lemma.Glued_Codes
+ imports
+ Combinatorics_Words_Graph_Lemma.Glued_Codes
Binary_Square_Interpretation
begin
text \This theory focuses on the characterization of imprimitive words which are concatenations
-of copies of two words (forming a binary code).
+of copies of two words (forming a binary code).
We follow the article @{cite lerest} (mainly Th\'eor\`eme 2.1 and Lemme 3.1),
while substantially optimizing the proof. See also @{cite spehner} for an earlier result on this question,
and @{cite Manuch} for another proof.\
section \General primitivity not preserving codes\
context code
begin
text \
Two nontrivially conjugate elements generated by a code induce a disjoint interpretation.\
lemma shift_disjoint:
- assumes "ws \ lists \" and "ws' \ lists \" and "z \ \\\" and "z \ concat ws = concat ws' \ z"
- "us \p ws\<^sup>@n" and "vs \p ws'\<^sup>@n"
+ assumes "ws \ lists \" and "ws' \ lists \" and "z \ \\\" and "z \ concat ws = concat ws' \ z"
+ "us \p ws\<^sup>@n" and "vs \p ws'\<^sup>@n"
shows "z \ concat us \ concat vs"
using \z \ \\\\
proof (elim contrapos_nn)
- assume "z \ concat us = concat vs"
+ assume "z \ concat us = concat vs"
have "z \ \"
- using \z \ \\\\ by blast
+ using \z \ \\\\ by blast
obtain us' where "ws\<^sup>@n = us \ us'"
- using prefixE[OF \us \p ws\<^sup>@n\].
+ using prefixE[OF \us \p ws\<^sup>@n\].
obtain vs' where "ws'\<^sup>@n = vs \ vs'"
- using prefixE[OF \vs \p ws'\<^sup>@n\].
+ using prefixE[OF \vs \p ws'\<^sup>@n\].
from conjug_pow[OF \z \ concat ws = concat ws' \ z\[symmetric], symmetric]
have "z \ concat (ws\<^sup>@n) = concat (ws'\<^sup>@n) \ z"
unfolding concat_pow.
from this[ unfolded \ws\<^sup>@n = us \ us'\ \ws'\<^sup>@n = vs \ vs'\ concat_morph rassoc
\z \ concat us = concat vs\[symmetric] cancel]
have "concat vs' \ z = concat us'"..
show "z \ \\\"
proof (rule stability)
have "us \ lists \" and "us' \ lists \" and "vs \ lists \" and "vs' \ lists \"
using \ws \ lists \\ \ws' \ lists \\ \ws'\<^sup>@n = vs \ vs'\ \ws\<^sup>@n = us \ us'\
by inlists
thus "z \ concat us \ \\\" and "concat vs' \ \\\" and "concat us \ \\\" and "concat vs' \ z \ \\\"
unfolding \concat vs' \ z = concat us'\ \z \ concat us = concat vs\
- by (simp_all add: concat_in_hull')
+ by (simp_all add: concat_in_hull')
qed
qed
text\This in particular yields a disjoint extendable interpretation of any prefix\
-lemma shift_interpret:
+lemma shift_interp:
assumes "ws \ lists \" and "ws' \ lists \" and "z \ \\\" and
- conjug: "z \ concat ws = concat ws' \ z" and "\<^bold>|z\<^bold>| < \<^bold>|concat ws'\<^bold>|"
+ conjug: "z \ concat ws = concat ws' \ z" and "\<^bold>|z\<^bold>| \ \<^bold>|concat ws'\<^bold>|"
and "us \p ws" and "us \ \"
- obtains p s vs ps ss where "p (concat us) s \\<^sub>\ vs" and "ps \ vs \p ws' \ ws'"
- and "us \ ss = ws \ ws" and
- "concat ps \ p = z" and "s \p concat ss" and "p \s concat ws" and "vs \ lists \"
- "\ us' vs'. us' \p us \ vs' \p vs \ p \ concat us' \ concat vs'" and "p \ \" and "s \ \"
+ obtains p s vs ps where
+ "p us s \\<^sub>\ vs" and "vs \ lists \"
+ and "s \p concat (us\\<^sup>>(ws \ ws))" and "p \s concat ws" \ \extendable\
+ and "ps \ vs \p ws' \ ws'" and "concat ps \ p = z"
proof-
have "ws' \ ws' \ lists \"
using \ws' \ lists \\ by inlists
have "concat us \ \"
using \us \ \\ unfolding code_concat_eq_emp_iff[OF pref_in_lists[OF \us \p ws\ \ws \ lists \\]].
have "\<^bold>|concat ws'\<^bold>| = \<^bold>|concat ws\<^bold>|"
using lenarg[OF conjug, unfolded lenmorph] by linarith
have "z \ concat(ws \ ws) = concat (ws' \ ws') \ z"
- unfolding rassoc concat_morph conjug[symmetric] unfolding lassoc cancel_right
+ unfolding rassoc concat_morph conjug[symmetric] unfolding lassoc cancel_right
using conjug.
- hence "concat (ws' \ ws') \p z \ concat (ws \ ws)"
+ hence "concat (ws' \ ws') \p z \ concat (ws \ ws)"
by blast
have "z \ concat ws \p concat (ws' \ ws')"
- unfolding concat_morph conjug pref_cancel_conv using eq_le_pref[OF conjug less_imp_le[OF \\<^bold>|z\<^bold>| < \<^bold>|concat ws'\<^bold>|\]].
+ unfolding concat_morph conjug pref_cancel_conv using eq_le_pref[OF conjug \\<^bold>|z\<^bold>| \ \<^bold>|concat ws'\<^bold>|\].
from prefixE[OF pref_shorten[OF pref_concat_pref[OF \us \p ws\] this], unfolded rassoc]
- obtain su where fac_u[symmetric]: "concat (ws' \ ws') = z \ concat us \ su".
+ obtain su where fac_u[symmetric]: "concat (ws' \ ws') = z \ concat us \ su".
- from obtain_fac_interpret[OF fac_u \concat us \ \\]
+ from obtain_fac_interp[OF fac_u \concat us \ \\]
obtain ps ss' p s vs where "p (concat us) s \\<^sub>\ vs" and
"ps \ vs \ ss' = ws' \ ws'" and "concat ps \ p = z" and "s \ concat ss' = su".
- note fac_interpretE[OF \