Email Gateway (Aug 18 2022 at 16:06): Email Gateway (Aug 18 2022 at 16:06):From: Alexander Krauss <krauss@in.tum.de>
Dear all,
We are happy to announce the companion paper for the AFP entry Regular-Sets:
A. Krauss and T. Nipkow
Proof Pearl: Regular Expression Equivalence and Relation Algebra
http://www4.informatik.tu-muenchen.de/~krauss/papers/rexp.pdf
Abstract:
We describe and verify an elegant equivalence checker for regular
expressions. It works by constructing a bisimulation relation between
(derivatives of) regular expressions. By mapping regular expressions
to binary relations, an automatic and complete proof method for
(in)equalities of binary relations over union, composition and
(reflexive) transitive closure is obtained.
In other words:
lemma example:
fixes R S :: "('a * 'a) set"
shows "S O (S O S^* O R^* Un R^*) <= S O S^* O R^*"
by regexp
Enjoy!
Alex and Tobias
Last updated: Apr 19 2024 at 01:05 UTC