1 # POSIX Lexing with Bitcoded Regular Expressions

     2 

     3 Run the code with

     4 

     5 ```isabelle build -c -v -d . Posix```

     6 

     7 Tested with Isabelle2021-1.

     8 

     9 

    10 * RegLangs.thy (contains basic definitions for Regular Languages)

    11 

    12 * PosixSpec.thy (contains values and POSIX definitions)

    13 

    14 * Positions.thy (shows the equivalence of our POSIX spec and the definition by Okui & Suzuki)

    15 

    16 * PDerivs.thy (Partial Derivatives according to Antimirov, size bounds of pderivs)

    17 

    18 * Lexer.thy (first algorithm by Sulzmann & Lu without simplification)

    19 

    20 * LexerSimp.thy (correctness for simple-minded simplification rules)

    21 

    22 * Blexer.thy (second algorithm by Sulzmann & Lu without simplification)

    23 

    24 * BlexerSimp.thy (correctness for aggressive simplification rules)

    25 

    26 * Finite Bound Result: BasicIdentidies.thy, ClosedForms.thy, GeneralRegexBound, ClosedFormBounds.thy (Section 5 in the paper)