\Brz{} introduced the notion of derivatives for regular

expressions. They can be used for a very simple regular expression

matching algorithm.  Sulzmann and Lu cleverly extended this algorithm

in order to deal with POSIX matching, which is the underlying

disambiguation strategy for regular expressions needed in

lexers. Sulzmann and Lu have made available on-line what they call a

``rigorous proof'' of the correctness of their algorithm w.r.t.~their

specification; regrettably, it appears to us to have unfillable gaps.

In the first part of this paper we give our inductive definition of

what a POSIX value is and show $(i)$ that such a value is unique (for

given regular expression and string being matched) and $(ii)$ that

Sulzmann and Lu's algorithm always generates such a value (provided

that the regular expression matches the string).  We also prove the

correctness of an optimised version of the POSIX matching

algorithm. Our definitions and proof are much simpler than those by

Sulzmann and Lu and can be easily formalised in Isabelle/HOL.  In the

second part we analyse the correctness argument by Sulzmann and Lu in

more detail and explain why it seems hard to turn it into a proof

rigorous enough to be accepted by a system such as Isabelle/HOL.

{\bf Keywords:} POSIX matching, Derivatives of Regular Expressions,

Isabelle/HOL