13841
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
|
3 |
\def\isabellecontext{Aufgabe{\isadigit{5}}}%
|
|
4 |
\isamarkupfalse%
|
|
5 |
%
|
|
6 |
\isamarkupsubsection{Interval lists%
|
|
7 |
}
|
|
8 |
\isamarkuptrue%
|
|
9 |
%
|
|
10 |
\begin{isamarkuptext}%
|
|
11 |
Sets of natural numbers can be implemented as lists of
|
|
12 |
intervals, where an interval is simply a pair of numbers. For example
|
|
13 |
the set \isa{{\isacharbraceleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{5}}{\isacharcomma}\ {\isadigit{7}}{\isacharcomma}\ {\isadigit{8}}{\isacharcomma}\ {\isadigit{9}}{\isacharbraceright}} can be represented by the
|
|
14 |
list \isa{{\isacharbrackleft}{\isacharparenleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}{\isadigit{5}}{\isacharcomma}\ {\isadigit{5}}{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}{\isadigit{7}}{\isacharcomma}\ {\isadigit{9}}{\isacharparenright}{\isacharbrackright}}. A typical application
|
|
15 |
is the list of free blocks of dynamically allocated memory.%
|
|
16 |
\end{isamarkuptext}%
|
|
17 |
\isamarkuptrue%
|
|
18 |
%
|
|
19 |
\isamarkupsubsubsection{Definitions%
|
|
20 |
}
|
|
21 |
\isamarkuptrue%
|
|
22 |
%
|
|
23 |
\begin{isamarkuptext}%
|
|
24 |
We introduce the type%
|
|
25 |
\end{isamarkuptext}%
|
|
26 |
\isamarkuptrue%
|
|
27 |
\isacommand{types}\ intervals\ {\isacharequal}\ {\isachardoublequote}{\isacharparenleft}nat{\isacharasterisk}nat{\isacharparenright}\ list{\isachardoublequote}\isamarkupfalse%
|
|
28 |
%
|
|
29 |
\begin{isamarkuptext}%
|
|
30 |
This type contains all possible lists of pairs of natural
|
|
31 |
numbers, even those that we may not recognize as meaningful
|
|
32 |
representations of sets. Thus you should introduce an \emph{invariant}%
|
|
33 |
\end{isamarkuptext}%
|
|
34 |
\isamarkuptrue%
|
|
35 |
\isacommand{consts}\ inv\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}intervals\ {\isacharequal}{\isachargreater}\ bool{\isachardoublequote}\isamarkupfalse%
|
|
36 |
%
|
|
37 |
\begin{isamarkuptext}%
|
|
38 |
that characterizes exactly those interval lists representing
|
|
39 |
sets. (The reason why we call this an invariant will become clear
|
|
40 |
below.) For efficiency reasons intervals should be sorted in
|
|
41 |
ascending order, the lower bound of each interval should be less or
|
|
42 |
equal the upper bound, and the intervals should be chosen as large as
|
|
43 |
possible, i.e.\ no two adjecent intervals should overlap or even touch
|
|
44 |
each other. It turns out to be convenient to define \isa{Aufgabe{\isadigit{5}}{\isachardot}inv} in
|
|
45 |
terms of a more general function%
|
|
46 |
\end{isamarkuptext}%
|
|
47 |
\isamarkuptrue%
|
|
48 |
\isacommand{consts}\ inv{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isacharequal}{\isachargreater}\ intervals\ {\isacharequal}{\isachargreater}\ bool{\isachardoublequote}\isamarkupfalse%
|
|
49 |
%
|
|
50 |
\begin{isamarkuptext}%
|
|
51 |
such that the additional argument is a lower bound for the
|
|
52 |
intervals in the list.
|
|
53 |
|
|
54 |
To relate intervals back to sets define an \emph{abstraktion funktion}%
|
|
55 |
\end{isamarkuptext}%
|
|
56 |
\isamarkuptrue%
|
|
57 |
\isacommand{consts}\ set{\isacharunderscore}of\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}intervals\ {\isacharequal}{\isachargreater}\ nat\ set{\isachardoublequote}\isamarkupfalse%
|
|
58 |
%
|
|
59 |
\begin{isamarkuptext}%
|
|
60 |
that yields the set corresponding to an interval list (that
|
|
61 |
satisfies the invariant).
|
|
62 |
|
|
63 |
Finally, define two primitive recursive functions%
|
|
64 |
\end{isamarkuptext}%
|
|
65 |
\isamarkuptrue%
|
|
66 |
\isacommand{consts}\ add\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}nat{\isacharasterisk}nat{\isacharparenright}\ {\isacharequal}{\isachargreater}\ intervals\ {\isacharequal}{\isachargreater}\ intervals{\isachardoublequote}\isanewline
|
|
67 |
\ \ \ \ \ \ \ rem\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}nat{\isacharasterisk}nat{\isacharparenright}\ {\isacharequal}{\isachargreater}\ intervals\ {\isacharequal}{\isachargreater}\ intervals{\isachardoublequote}\isamarkupfalse%
|
|
68 |
%
|
|
69 |
\begin{isamarkuptext}%
|
|
70 |
for inserting and deleting an interval from an interval
|
|
71 |
list. The result should again satisfies the invariant. Hence the name:
|
|
72 |
\isa{inv} is invariant under the application of the operations
|
|
73 |
\isa{add} and \isa{rem} --- if \isa{inv} holds for the input, it
|
|
74 |
must also hold for the output.%
|
|
75 |
\end{isamarkuptext}%
|
|
76 |
\isamarkuptrue%
|
|
77 |
%
|
|
78 |
\isamarkupsubsubsection{Proving the invariant%
|
|
79 |
}
|
|
80 |
\isamarkuptrue%
|
|
81 |
\isacommand{declare}\ Let{\isacharunderscore}def\ {\isacharbrackleft}simp{\isacharbrackright}\isanewline
|
|
82 |
\isamarkupfalse%
|
|
83 |
\isacommand{declare}\ split{\isacharunderscore}split\ {\isacharbrackleft}split{\isacharbrackright}\isamarkupfalse%
|
|
84 |
%
|
|
85 |
\begin{isamarkuptext}%
|
|
86 |
Start off by proving the monotonicity of \isa{inv{\isadigit{2}}}:%
|
|
87 |
\end{isamarkuptext}%
|
|
88 |
\isamarkuptrue%
|
|
89 |
\isacommand{lemma}\ inv{\isadigit{2}}{\isacharunderscore}monotone{\isacharcolon}\ {\isachardoublequote}inv{\isadigit{2}}\ m\ ins\ {\isasymLongrightarrow}\ n{\isasymle}m\ {\isasymLongrightarrow}\ inv{\isadigit{2}}\ n\ ins{\isachardoublequote}\isamarkupfalse%
|
|
90 |
\isamarkupfalse%
|
|
91 |
%
|
|
92 |
\begin{isamarkuptext}%
|
|
93 |
Now show that \isa{add} and \isa{rem} preserve the invariant:%
|
|
94 |
\end{isamarkuptext}%
|
|
95 |
\isamarkuptrue%
|
|
96 |
\isacommand{theorem}\ inv{\isacharunderscore}add{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ i{\isasymle}j{\isacharsemicolon}\ inv\ ins\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ inv\ {\isacharparenleft}add\ {\isacharparenleft}i{\isacharcomma}j{\isacharparenright}\ ins{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
|
|
97 |
\isanewline
|
|
98 |
\isamarkupfalse%
|
|
99 |
\isacommand{theorem}\ inv{\isacharunderscore}rem{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ i{\isasymle}j{\isacharsemicolon}\ inv\ ins\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ inv\ {\isacharparenleft}rem\ {\isacharparenleft}i{\isacharcomma}j{\isacharparenright}\ ins{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
|
|
100 |
\isamarkupfalse%
|
|
101 |
%
|
|
102 |
\begin{isamarkuptext}%
|
|
103 |
Hint: you should first prove a more general statement
|
|
104 |
(involving \isa{inv{\isadigit{2}}}). This will probably involve some advanced
|
|
105 |
forms of induction discussed in section~9.3.1 of
|
|
106 |
\cite{isabelle-tutorial}.%
|
|
107 |
\end{isamarkuptext}%
|
|
108 |
\isamarkuptrue%
|
|
109 |
%
|
|
110 |
\isamarkupsubsubsection{Proving correctness of the implementation%
|
|
111 |
}
|
|
112 |
\isamarkuptrue%
|
|
113 |
%
|
|
114 |
\begin{isamarkuptext}%
|
|
115 |
Show the correctness of \isa{add} and \isa{rem} wrt.\
|
|
116 |
their counterparts \isa{{\isasymunion}} and \isa{{\isacharminus}} on sets:%
|
|
117 |
\end{isamarkuptext}%
|
|
118 |
\isamarkuptrue%
|
|
119 |
\isacommand{theorem}\ set{\isacharunderscore}of{\isacharunderscore}add{\isacharcolon}\ \isanewline
|
|
120 |
\ \ {\isachardoublequote}{\isasymlbrakk}\ i{\isasymle}j{\isacharsemicolon}\ inv\ ins\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ set{\isacharunderscore}of\ {\isacharparenleft}add\ {\isacharparenleft}i{\isacharcomma}j{\isacharparenright}\ ins{\isacharparenright}\ {\isacharequal}\ set{\isacharunderscore}of\ {\isacharbrackleft}{\isacharparenleft}i{\isacharcomma}j{\isacharparenright}{\isacharbrackright}\ {\isasymunion}\ set{\isacharunderscore}of\ ins{\isachardoublequote}\isamarkupfalse%
|
|
121 |
\isanewline
|
|
122 |
\isamarkupfalse%
|
|
123 |
\isacommand{theorem}\ set{\isacharunderscore}of{\isacharunderscore}rem{\isacharcolon}\isanewline
|
|
124 |
\ \ {\isachardoublequote}{\isasymlbrakk}\ i\ {\isasymle}\ j{\isacharsemicolon}\ inv\ ins\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ set{\isacharunderscore}of\ {\isacharparenleft}rem\ {\isacharparenleft}i{\isacharcomma}j{\isacharparenright}\ ins{\isacharparenright}\ {\isacharequal}\ set{\isacharunderscore}of\ ins\ {\isacharminus}\ set{\isacharunderscore}of\ {\isacharbrackleft}{\isacharparenleft}i{\isacharcomma}j{\isacharparenright}{\isacharbrackright}{\isachardoublequote}\isamarkupfalse%
|
|
125 |
\isamarkupfalse%
|
|
126 |
%
|
|
127 |
\begin{isamarkuptext}%
|
|
128 |
Hints: in addition to the hints above, you may also find it
|
|
129 |
useful to prove some relationship between \isa{inv{\isadigit{2}}} and \isa{set{\isacharunderscore}of} as a lemma.%
|
|
130 |
\end{isamarkuptext}%
|
|
131 |
\isamarkuptrue%
|
|
132 |
%
|
|
133 |
\isamarkupsubsubsection{General hints%
|
|
134 |
}
|
|
135 |
\isamarkuptrue%
|
|
136 |
%
|
|
137 |
\begin{isamarkuptext}%
|
|
138 |
\begin{itemize}
|
|
139 |
|
|
140 |
\item You should be familiar both with simplification and predicate
|
|
141 |
calculus reasoning. Automatic tactics like \isa{blast} and \isa{force} can simplify the proof.
|
|
142 |
|
|
143 |
\item
|
|
144 |
Equality of two sets can often be proved via the rule \isa{set{\isacharunderscore}ext}:
|
|
145 |
\begin{isabelle}%
|
|
146 |
{\isacharparenleft}{\isasymAnd}x{\isachardot}\ {\isacharparenleft}x\ {\isasymin}\ A{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymin}\ B{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ A\ {\isacharequal}\ B%
|
|
147 |
\end{isabelle}
|
|
148 |
|
|
149 |
\item
|
|
150 |
Potentially useful theorems for the simplification of sets include \\
|
|
151 |
\isa{Un{\isacharunderscore}Diff{\isacharcolon}}~\isa{A\ {\isasymunion}\ B\ {\isacharminus}\ C\ {\isacharequal}\ A\ {\isacharminus}\ C\ {\isasymunion}\ {\isacharparenleft}B\ {\isacharminus}\ C{\isacharparenright}} \\
|
|
152 |
\isa{Diff{\isacharunderscore}triv{\isacharcolon}}~\isa{A\ {\isasyminter}\ B\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}\ {\isasymLongrightarrow}\ A\ {\isacharminus}\ B\ {\isacharequal}\ A}.
|
|
153 |
|
|
154 |
\item
|
|
155 |
Theorems can be instantiated and simplified via \isa{of} and
|
|
156 |
\isa{{\isacharbrackleft}simplified{\isacharbrackright}} (see \cite{isabelle-tutorial}).
|
|
157 |
\end{itemize}%
|
|
158 |
\end{isamarkuptext}%
|
|
159 |
\isamarkuptrue%
|
|
160 |
\isamarkupfalse%
|
|
161 |
\end{isabellebody}%
|
|
162 |
%%% Local Variables:
|
|
163 |
%%% mode: latex
|
|
164 |
%%% TeX-master: "root"
|
|
165 |
%%% End:
|