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.
- August 17, 2023
- Updated to version v1.10.1.
- August 24, 2022
- Many updates and additions. New theories: Border_Array, Morphisms, Equations_Basic, and Binary_Code_Morphisms.
- Holub, Š., & Starosta, Š. (2021). Formalization of Basic Combinatorics on Words. Schloss Dagstuhl - Leibniz-Zentrum Für Informatik. https://doi.org/10.4230/LIPICS.ITP.2021.22
- Producing symmetrical facts for lists induced by the list reversal mapping in Isabelle/HOL
- Development repository