### Abstract

This is a library of constructions on regular expressions and languages. It provides the operations of concatenation, Kleene star and derivative on languages. Regular expressions and their meaning are defined. An executable equivalence checker for regular expressions is verified; it does not need automata but works directly on regular expressions. By mapping regular expressions to binary relations, an automatic and complete proof method for (in)equalities of binary relations over union, concatenation and (reflexive) transitive closure is obtained.

Extended regular expressions with complement and intersection are also defined and an equivalence checker is provided.

### License

BSD License

### History

May 10, 2012
  Tobias Nipkow added equivalence checking with partial derivatives
August 26, 2011
  Christian Urban added a theory about derivatives and partial derivatives of regular expressions

### Topics

- Computer science/Automata and formal languages

### Related publications

- Krauss, A., & Nipkow, T. (2011). Proof Pearl: Regular Expression Equivalence and Relation Algebra. Journal of Automated Reasoning, 49(1), 95–106. https://doi.org/10.1007/s10817-011-9223-4
- author's copy

### Session Regular-Sets

- Regular_Set
- Regular_Exp
- NDerivative
- Equivalence_Checking
- Relation_Interpretation
- Regexp_Method
- Regexp_Constructions
- Derivatives
- pEquivalence_Checking
- Regular_Exp2
- Equivalence_Checking2

### Used by

- Isabelle/DOF
- The number of comparisons in QuickSort
- Formalization of Knuth–Bendix Orders for Lambda-Free Higher-Order Terms
- POSIX Lexing with Derivatives of Regular Expressions
- Analysis of List Update Algorithms
- Finite Automata in Hereditarily Finite Set Theory
- Unified Decision Procedures for Regular Expression Equivalence
- A Codatatype of Formal Languages
- Light-weight Containers
- Executable Transitive Closures
- The Myhill-Nerode Theorem Based on Regular Expressions
- Abstract Rewriting
- Functional Automata

## Cite

×

Regular-Sets-AFP

    @article{Regular-Sets-AFP,
      author  = {Alexander Krauss and Tobias Nipkow},
      title   = {Regular Sets and Expressions},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2010},
      note    = {\url{https://isa-afp.org/entries/Regular-Sets.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
- Feb 11, 2011 : Isabelle2011
- Jul 1, 2010 : Isabelle2009-2