[isabelle] Proof Pearl: Regular Expression Equivalence and Relation Algebra



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.