### Abstract

There are many proofs of the Myhill-Nerode theorem using automata. In this library we give a proof entirely based on regular expressions, since regularity of languages can be conveniently defined using regular expressions (it is more painful in HOL to define regularity in terms of automata). We prove the first direction of the Myhill-Nerode theorem by solving equational systems that involve regular expressions. For the second direction we give two proofs: one using tagging-functions and another using partial derivatives. We also establish various closure properties of regular languages. Most details of the theories are described in our ITP 2011 paper.

### License

BSD License

### Topics

- Computer science/Automata and formal languages

### Session Myhill-Nerode

- Folds
- Myhill_1
- Myhill_2
- Myhill
- Closures
- Closures2
- Non_Regular_Languages

### Depends on

- Abstract Rewriting
- Open Induction
- Regular Sets and Expressions
- Well-Quasi-Orders

### Auto-related entries

- Myhill-Nerode Theorem for Nominal G-Automata
- Finite Automata in Hereditarily Finite Set Theory
- Regular Tree Relations
- Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
- Tree Automata

## Cite

×

Myhill-Nerode-AFP

    @article{Myhill-Nerode-AFP,
      author  = {Chunhan Wu and Xingyuan Zhang and Christian Urban},
      title   = {The Myhill-Nerode Theorem Based on Regular Expressions},
      journal = {Archive of Formal Proofs},
      month   = {August},
      year    = {2011},
      note    = {\url{https://isa-afp.org/entries/Myhill-Nerode.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Mar 2, 2013 : Isabelle2013
- Feb 16, 2013 : Isabelle2013
- May 24, 2012 : Isabelle2012
- Oct 11, 2011 : Isabelle2011-1