POSIX Lexing with Bitcoded Regular Expressions

Run the code with

isabelle build -c -v -d . Posix

Tested with Isabelle2021-1.

RegLangs.thy (contains basic definitions for Regular Languages, chapter 2)
PosixSpec.thy (contains values and POSIX definitions, chapter 2)
Lexer.thy (first algorithm by Sulzmann & Lu without simplification, chapter 2)
LexerSimp.thy (correctness for simple-minded simplification rules, chapter 2)
Blexer.thy (second algorithm by Sulzmann & Lu without simplification, chapter 3)
BlexerSimp.thy (correctness for simplification rules with effective de-duplication, chapter 4)
Finite Bound Result: (chapter 5) BasicIdentidies.thy ClosedForms.thy GeneralRegexBound ClosedFormBounds.thy FBound.thy

Name		Name	Last commit message	Last commit date
Latest commit History 8 Commits
BasicIdentities.thy		BasicIdentities.thy
Blexer.thy		Blexer.thy
BlexerSimp.thy		BlexerSimp.thy
ClosedForms.thy		ClosedForms.thy
ClosedFormsBounds.thy		ClosedFormsBounds.thy
FBound.thy		FBound.thy
GeneralRegexBound.thy		GeneralRegexBound.thy
Lexer.thy		Lexer.thy
LexerSimp.thy		LexerSimp.thy
PosixSpec.thy		PosixSpec.thy
README.md		README.md
ROOT		ROOT
RegLangs.thy		RegLangs.thy
backRef.sc		backRef.sc

Provide feedback