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-- |
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: |