coursework/cw05.tex
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Thu, 09 Apr 2015 07:42:23 +0100
changeset 322 698ed1c96cd0
parent 317 a61b50c5d57f
child 328 bc03ff3d347c
permissions -rw-r--r--
updated
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
253
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     1
\documentclass{article}
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     2
\usepackage{../style}
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     3
\usepackage{../langs}
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     4
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     5
\begin{document}
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     6
260
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
     7
\section*{Coursework (Strand 2)}
253
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     8
260
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
     9
\noindent This coursework is worth 25\% and is due on 12
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    10
December at 16:00. You are asked to prove the correctness of a
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    11
regular expression matcher from the lectures using the
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    12
Isabelle theorem prover. You need to submit a theory file
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    13
containing this proof. The Isabelle theorem prover is
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    14
available from 
253
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    15
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    16
\begin{center}
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    17
\url{http://isabelle.in.tum.de}
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    18
\end{center}
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    19
260
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    20
\noindent This is an interactive theorem prover, meaning that
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    21
you can make definitions and state properties, and then help
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    22
the system with proving these properties. Sometimes the proofs
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    23
are also automatic. There is a shortish user guide for
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    24
Isabelle, called ``Programming and Proving in Isabelle/HOL''
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    25
at
253
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    26
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    27
\begin{center}
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    28
\url{http://isabelle.in.tum.de/documentation.html}
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    29
\end{center}
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    30
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    31
\noindent
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    32
and also a longer (free) book at
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    33
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    34
\begin{center}
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    35
\url{http://www.concrete-semantics.org}
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    36
\end{center}
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    37
260
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    38
\noindent The Isabelle theorem prover is operated through the
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    39
jEdit IDE, which might not be an editor that is widely known.
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    40
JEdit is documented in
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    41
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    42
\begin{center}
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    43
\url{http://isabelle.in.tum.de/dist/Isabelle2014/doc/jedit.pdf}
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    44
\end{center}
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    45
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    46
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    47
\noindent If you need more help or you are stuck somewhere,
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    48
please feel free to contact me (christian.urban@kcl.ac.uk). I
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    49
am a main developer of Isabelle and have used it for
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    50
approximately the 14 years. One of the success stories of
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    51
Isabelle is the recent verification of a microkernel operating
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    52
system by an Australian group, see \url{http://sel4.systems}.
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    53
Their operating system is the only one that has been proved
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    54
correct according to its specification and is used for
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    55
application where high assurance, security and reliability is
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    56
needed. 
253
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    57
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    58
260
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    59
\subsection*{The Task}
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    60
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    61
In this coursework you are asked to prove the correctness of
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    62
the regular expression matcher from the lectures in Isabelle.
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    63
For this you need to first specify what the matcher is
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    64
supposed to do and then to implement the algorithm. Finally
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    65
you need to prove that the algorithm meets the specification.
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    66
The first two parts are relatively easy, because the
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    67
definitions in Isabelle will look very similar to the
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    68
mathematical definitions from the lectures or the Scala code
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    69
that is supplied at KEATS. For example very similar to Scala,
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    70
regular expressions are defined in Isabelle as an inductive
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    71
datatype:
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    72
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    73
\begin{lstlisting}[language={},numbers=none]
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    74
datatype rexp =
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    75
  NULL
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    76
| EMPTY
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    77
| CHAR char
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    78
| SEQ rexp rexp
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    79
| ALT rexp rexp
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    80
| STAR rexp
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    81
\end{lstlisting}
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    82
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    83
\noindent The meaning of regular expressions is given as 
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    84
usual:
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    85
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    86
\begin{center}
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    87
\begin{tabular}{rcl@{\hspace{10mm}}l}
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    88
$L(\varnothing)$  & $\dn$ & $\varnothing$   & \pcode{NULL}\\
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    89
$L(\epsilon)$     & $\dn$ & $\{[]\}$        & \pcode{EMPTY}\\ 
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    90
$L(c)$            & $\dn$ & $\{[c]\}$       & \pcode{CHAR}\\
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    91
$L(r_1 + r_2)$     & $\dn$ & $L(r_1) \cup L(r_2)$ & \pcode{ALT}\\
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    92
$L(r_1 \cdot r_2)$ & $\dn$ & $L(r_1) \,@\, L(r_2)$ & \pcode{SEQ}\\
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    93
$L(r^*)$           & $\dn$ & $(L(r))^*$ & \pcode{STAR}\\
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    94
\end{tabular}
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    95
\end{center}
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    96
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    97
\noindent You would need to implement this function in order
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    98
to state the theorem about the correctness of the algorithm.
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
    99
The function $L$ should in Isabelle take a \pcode{rexp} as
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   100
input and return a set of strings. Its type is
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   101
therefore 
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   102
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   103
\begin{center}
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   104
\pcode{L} \pcode{::} \pcode{rexp} $\Rightarrow$ \pcode{string set}
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   105
\end{center}
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   106
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   107
\noindent Isabelle treats strings as an abbreviation for lists
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   108
of characters. This means you can pattern-match strings like
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   109
lists. The union operation on sets (for the \pcode{ALT}-case)
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   110
is a standard definition in Isabelle, but not the
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   111
concatenation operation on sets and also not the
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   112
star-operation. You would have to supply these definitions.
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   113
The concatenation operation can be defined in terms of the
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   114
append function, written \code{_ @ _} in Isabelle, for lists.
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   115
The star-operation can be defined as a ``big-union'' of 
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   116
powers, like in the lectures, or directly as an inductive set.
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   117
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   118
The functions for the matcher are shown in
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   119
Figure~\ref{matcher}. The theorem that needs to be proved is
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   120
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   121
\begin{lstlisting}[numbers=none,language={},keywordstyle=\color{black}\ttfamily,mathescape]
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   122
theorem 
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   123
  "matches r s $\longleftrightarrow$ s $\in$ L r"
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   124
\end{lstlisting}
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   125
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   126
\noindent which states that the function \emph{matches} is
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   127
true if and only if the string is in the language of the
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   128
regular expression. A proof for this lemma will need
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   129
side-lemmas about \pcode{nullable} and \pcode{der}. An example
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   130
proof in Isabelle that will not be relevant for the theorem
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   131
above is given in Figure~\ref{proof}.
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   132
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   133
\begin{figure}[p]
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   134
\begin{lstlisting}[language={},keywordstyle=\color{black}\ttfamily,mathescape]
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   135
fun 
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   136
  nullable :: "rexp $\Rightarrow$ bool"
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   137
where
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   138
  "nullable NULL = False"
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   139
| "nullable EMPTY = True"
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   140
| "nullable (CHAR _) = False"
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   141
| "nullable (ALT r1 r2) = (nullable(r1) $\vee$ nullable(r2))"
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   142
| "nullable (SEQ r1 r2) = (nullable(r1) $\wedge$ nullable(r2))"
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   143
| "nullable (STAR _) = True"
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   144
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   145
fun 
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   146
  der :: "char $\Rightarrow$ rexp $\Rightarrow$ rexp"
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   147
where
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   148
  "der c NULL = NULL"
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   149
| "der c EMPTY = NULL"
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   150
| "der c (CHAR d) = (if c = d then EMPTY else NULL)"
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   151
| "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   152
| "der c (SEQ r1 r2) = 
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   153
     (if (nullable r1) then ALT (SEQ (der c r1) r2) (der c r2)
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   154
                       else SEQ (der c r1) r2)"
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   155
| "der c (STAR r) = SEQ (der c r) (STAR r)"
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   156
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   157
fun 
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   158
  ders :: "rexp $\Rightarrow$ string $\Rightarrow$ rexp"
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   159
where
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   160
  "ders r [] = r"
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   161
| "ders r (c # s) = ders (der c r) s"
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   162
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   163
fun 
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   164
  matches :: "rexp $\Rightarrow$ string $\Rightarrow$ bool"
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   165
where
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   166
  "matches r s = nullable (ders r s)" 
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   167
\end{lstlisting}
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   168
\caption{The definition of the matcher algorithm in 
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   169
Isabelle.\label{matcher}}
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   170
\end{figure}
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   171
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   172
\begin{figure}[p]
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   173
\begin{lstlisting}[language={},keywordstyle=\color{black}\ttfamily,mathescape]
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   174
fun 
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   175
  zeroable :: "rexp $\Rightarrow$ bool"
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   176
where
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   177
  "zeroable NULL = True"
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   178
| "zeroable EMPTY = False"
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   179
| "zeroable (CHAR _) = False"
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   180
| "zeroable (ALT r1 r2) = (zeroable(r1) $\wedge$ zeroable(r2))"
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   181
| "zeroable (SEQ r1 r2) = (zeroable(r1) $\vee$ zeroable(r2))"
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   182
| "zeroable (STAR _) = False"
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   183
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   184
lemma
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   185
  "zeroable r $\longleftrightarrow$ L r = {}"
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   186
proof (induct)
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   187
  case (NULL)
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   188
  have "zeroable NULL" "L NULL = {}" by simp_all
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   189
  then show "zeroable NULL $\longleftrightarrow$ (L NULL = {})" by simp
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   190
next
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   191
  case (EMPTY)
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   192
  have "$\neg$ zeroable EMPTY" "L EMPTY = {[]}" by simp_all
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   193
  then show "zeroable EMPTY $\longleftrightarrow$ (L EMPTY = {})" by simp
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   194
next
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   195
  case (CHAR c)
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   196
  have "$\neg$ zeroable (CHAR c)" "L (CHAR c) = {[c]}" by simp_all
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   197
  then show "zeroable (CHAR c) $\longleftrightarrow$ (L (CHAR c) = {})" by simp
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   198
next 
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   199
  case (ALT r1 r2)
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   200
  have ih1: "zeroable r1 $\longleftrightarrow$ L r1 = {}" by fact
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   201
  have ih2: "zeroable r2 $\longleftrightarrow$ L r2 = {}" by fact
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   202
  show "zeroable (ALT r1 r2) $\longleftrightarrow$ (L (ALT r1 r2) = {})" 
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   203
    using ih1 ih2 by simp
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   204
next
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   205
  case (SEQ r1 r2)
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   206
  have ih1: "zeroable r1 $\longleftrightarrow$ L r1 = {}" by fact
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   207
  have ih2: "zeroable r2 $\longleftrightarrow$ L r2 = {}" by fact
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   208
  show "zeroable (SEQ r1 r2) $\longleftrightarrow$ (L (SEQ r1 r2) = {})" 
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   209
    using ih1 ih2 by (auto simp add: Conc_def)
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   210
next
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   211
  case (STAR r)
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   212
  have "$\neg$ zeroable (STAR r)" "[] $\in$ L (r) ^ 0" by simp_all
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   213
  then show "zeroable (STAR r) $\longleftrightarrow$ (L (STAR r) = {})" 
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   214
    by (simp (no_asm) add: Star_def) blast
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   215
qed
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   216
\end{lstlisting}
317
a61b50c5d57f updated all
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 298
diff changeset
   217
\caption{An Isabelle proof about the function \texttt{zeroable}.\label{proof}}
260
65d1ea0e989f updated cws
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 253
diff changeset
   218
\end{figure}
253
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   219
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   220
\end{document}
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   221
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   222
%%% Local Variables: 
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   223
%%% mode: latex
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   224
%%% TeX-master: t
75c469893514 added coursework
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   225
%%% End: