54 %----------------------------------------------------------------------------------------

    59 Ausaf and Urban cleverly defined an auxiliary function called $\flex$,

    55 %	SECTION corretness proof

    60 defined as

    56 %----------------------------------------------------------------------------------------

    61 \[

    57 \section{Proof Technique of Correctness of Bit-coded Algorithm with Simplification}

    62 \flex \; r \; f \; [] \; v \; = \; f\; v

    58 The non-trivial part of proving the correctness of the algorithm with simplification

    63 \flex \; r \; f \; c :: s \; v =  \flex r \; \lambda v. \, f (\inj \; r\; c\; v)\; s \; v

    59 compared with not having simplification is that we can no longer use the argument 

    64 \]

    60 in \cref{flex_retrieve}.

    65 which accumulates the characters that needs to be injected back, 

    61 The function \retrieve needs the structure of the annotated regular expression to 

    66 and does the injection in a stack-like manner (last taken derivative first injected).

    62 agree with the structure of the value, but simplification will always mess with the 

    67 $\flex$ is connected to the $\lexer$:

    63 structure:

    68 \begin{lemma}

    64 %TODO: after simp does not agree with each other: (a + 0) --> a v.s. Left(Char(a))

    69 $\flex \; r \; \textit{id}\; s \; \mkeps (r\backslash s) = \lexer \; r \; s$

    70 \end{lemma}

    71 $\flex$ provides us a bridge between $\lexer$ and $\blexer$.

    72 What is even better about $\flex$ is that it allows us to 

    73 directly operate on the value $\mkeps (r\backslash v)$,

    74 which is pivotal in the definition of  $\lexer $ and $\blexer$, but not visible as an argument.

    75 When the value created by $\mkeps$ becomes available, one can 

    76 prove some stepwise properties of lexing nicely:

    77 \begin{lemma}\label{flexStepwise}

    78 $\textit{flex} \; r \; f \; s@[c] \; v= \flex \; r \; f\; s \; (\inj \; (r\backslash s) \; c \; v) $

    79 \end{lemma}

    80 

    81 And for $\blexer$ we have a function with stepwise properties like $\flex$ as well,

    82 called $\retrieve$\ref{retrieveDef}.

    83 $\retrieve$ takes bit-codes from annotated regular expressions

    84 guided by a value.

    85 $\retrieve$ is connected to the $\blexer$ in the following way:

    86 \begin{lemma}\label{blexer_retrieve}

    87 $\blexer \; r \; s = \decode  \; (\retrieve \; (\internalise \; r) \; (\mkeps \; (r \backslash s) )) \; r$

    88 \end{lemma}

    89 If you take derivative of an annotated regular expression, 

    90 you can $\retrieve$ the same bit-codes as before the derivative took place,

    91 provided that you use the corresponding value:

    92 

    93 \begin{lemma}\label{retrieveStepwise}

    94 $\retrieve \; (r \backslash c)  \;  v= \retrieve \; r \; (\inj \; r\; c\; v)$

    95 \end{lemma}

    96 The other good thing about $\retrieve$ is that it can be connected to $\flex$:

    97 %centralLemma1

    98 \begin{lemma}\label{flex_retrieve}

    99 $\flex \; r \; \textit{id}\; s\; v = \decode \; (\retrieve \; (r\backslash s )\; v) \; r$

   100 \end{lemma}

   101 \begin{proof}

   102 By induction on $s$. The induction tactic is reverse induction on strings.

   103 $v$ is allowed to be arbitrary.

   104 The crucial point is to rewrite 

   105 \[

   106 \retrieve \; (r \backslash s@[c]) \; \mkeps (r \backslash s@[c]) 

   107 \]

   108 as

   109 \[

   110 \retrieve \; (r \backslash s) \; (\inj \; (r \backslash s) \; c\;  \mkeps (r \backslash s@[c]))

   111 \].

   112 This enables us to equate 

   113 \[

   114 \retrieve \; (r \backslash s@[c]) \; \mkeps (r \backslash s@[c]) 

   115 \] 

   116 with 

   117 \[

   118 \flex \; r \; \textit{id} \; s \; (\inj \; (r\backslash s) \; c\; (\mkeps (r\backslash s@[c])))

   119 \],

   120 which in turn can be rewritten as

   121 \[

   122 \flex \; r \; \textit{id} \; s@[c] \;  (\mkeps (r\backslash s@[c]))

   123 \].

   124 \end{proof}

   125 

   126 With the above lemma we can now link $\flex$ and $\blexer$.

   127 

   128 \begin{lemma}\label{flex_blexer}

   129 $\textit{flex} \; r \; \textit{id} \; s \; \mkeps(r \backslash s)  = \blexer \; r \; s$

   130 \end{lemma}

   131 \begin{proof}

   132 Using two of the above lemmas: \ref{flex_retrieve} and \ref{blexer_retrieve}.

   133 \end{proof}

   134 Finally 

   135 

   136