# POSIX Lexing with Bitcoded Regular Expressions+
−
+
−
Run the code with+
−
+
−
```isabelle build -c -v -d . Posix```+
−
+
−
Generate the paper with+
−
+
−
```isabelle build -c -v -d . Paper```+
−
+
−
Tested with Isabelle2021-1.+
−
+
−
+
−
* RegLangs.thy (contains basic definitions for Regular Languages)+
−
+
−
* PosixSpec.thy (contains values and POSIX definitions)+
−
+
−
* Positions.thy (shows the equivalence of our POSIX spec and the definition by Okui & Suzuki)+
−
+
−
* PDerivs.thy (Partial Derivatives according to Antimirov, size bounds of pderivs)+
−
+
−
* Lexer.thy (first algorithm by Sulzmann & Lu without simplification)+
−
+
−
* LexerSimp.thy (correctness for simple-minded simplification rules)+
−
+
−
* Blexer.thy (second algorithm by Sulzmann & Lu without simplification)+
−
+
−
* BlexerSimp.thy (correctness for aggressive simplification rules)+
−
+
−
* Finite Bound Result: BasicIdentidies.thy, ClosedForms.thy, GeneralRegexBound, ClosedFormBounds.thy (Section 5 in the paper)+
−