312 

   312 

   313 While a formalised correctness proof for Sulzmann and Lu's algorithm already exists, this proof does not include any of the crucial simplification rules. These simplification rules are however necessary in order to have an acceptable runtime for this algorithm. Our version of the simplification rules includes a number of fixes and improvements: one problem we fix has to do with their use of the nub function that does not remove non-trivial duplicates. We improve the simplification rules by formulating them as simple recursive function and also by simplifying more instances of regular expressions.  As a result we can establish a bound on the size of derivatives. Our proofs are formalised in Isabelle/HOL.

   313 While a formalised correctness proof for Sulzmann and Lu's algorithm already exists, this proof does not include any of the crucial simplification rules. These simplification rules are however necessary in order to have an acceptable runtime for this algorithm. Our version of the simplification rules includes a number of fixes and improvements: one problem we fix has to do with their use of the nub function that does not remove non-trivial duplicates. We improve the simplification rules by formulating them as simple recursive function and also by simplifying more instances of regular expressions.  As a result we can establish a bound on the size of derivatives. Our proofs are formalised in Isabelle/HOL.

   314 

   314 

   315 

   315 

   316 

   316 

   318 %This thesis is about regular expressions and derivatives. It combines functional algorithms and their formal verification in the Isabelle/HOL theorem prover. 

   318 %This thesis is about regular expressions and derivatives. It combines functional algorithms and their formal verification in the Isabelle/HOL theorem prover. 

   319 %Classic results say that regular expression matching should be 

   319 %Classic results say that regular expression matching should be 

   320 %linear with respect to the input. The size of the regular expressions

   320 %linear with respect to the input. The size of the regular expressions

   321 %are often treated as a constant factor.

   321 %are often treated as a constant factor.

   322 %However with some regular expressions and inputs, existing implementations 

   322 %However with some regular expressions and inputs, existing implementations