1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{a{\isadigit{5}}}% |
|
4 \isamarkupfalse% |
|
5 % |
|
6 \isamarkupsubsection{Merge sort% |
|
7 } |
|
8 \isamarkuptrue% |
|
9 % |
|
10 \begin{isamarkuptext}% |
|
11 Implement \emph{merge sort}: a list is sorted by splitting it |
|
12 into two lists, sorting them separately, and merging the results. |
|
13 |
|
14 With the help of \isa{recdef} define two functions% |
|
15 \end{isamarkuptext}% |
|
16 \isamarkuptrue% |
|
17 \isacommand{consts}\ merge\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ list\ {\isasymtimes}\ nat\ list\ {\isasymRightarrow}\ nat\ list{\isachardoublequote}\isanewline |
|
18 \ \ \ \ \ \ \ msort\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ list\ {\isasymRightarrow}\ nat\ list{\isachardoublequote}\isamarkupfalse% |
|
19 % |
|
20 \begin{isamarkuptext}% |
|
21 and show% |
|
22 \end{isamarkuptext}% |
|
23 \isamarkuptrue% |
|
24 \isacommand{theorem}\ {\isachardoublequote}sorted\ {\isacharparenleft}msort\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
25 \isanewline |
|
26 \isamarkupfalse% |
|
27 \isacommand{theorem}\ {\isachardoublequote}count\ {\isacharparenleft}msort\ xs{\isacharparenright}\ x\ {\isacharequal}\ count\ xs\ x{\isachardoublequote}\isamarkupfalse% |
|
28 \isamarkupfalse% |
|
29 % |
|
30 \begin{isamarkuptext}% |
|
31 where \isa{sorted} and \isa{count} are defined as in |
|
32 section~\ref{psv2002a2}. |
|
33 |
|
34 Hints: |
|
35 \begin{itemize} |
|
36 \item For \isa{recdef} see section~3.5 of \cite{isabelle-tutorial}. |
|
37 |
|
38 \item To split a list into two halves of almost equal length you can |
|
39 use the functions \mbox{\isa{n\ div\ {\isadigit{2}}}}, \isa{take} und \isa{drop}, |
|
40 where \isa{take\ n\ xs} returns the first \isa{n} elements of |
|
41 \isa{xs} and \isa{drop\ n\ xs} the remainder. |
|
42 |
|
43 \item Here are some potentially useful lemmas:\\ |
|
44 \isa{linorder{\isacharunderscore}not{\isacharunderscore}le{\isacharcolon}} \isa{{\isacharparenleft}{\isasymnot}\ x\ {\isasymle}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y\ {\isacharless}\ x{\isacharparenright}}\\ |
|
45 \isa{order{\isacharunderscore}less{\isacharunderscore}le{\isacharcolon}} \isa{{\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymle}\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}}\\ |
|
46 \isa{min{\isacharunderscore}def{\isacharcolon}} \isa{min\ a\ b\ {\isasymequiv}\ if\ a\ {\isasymle}\ b\ then\ a\ else\ b} |
|
47 \end{itemize}% |
|
48 \end{isamarkuptext}% |
|
49 \isamarkuptrue% |
|
50 \isamarkupfalse% |
|
51 \end{isabellebody}% |
|
52 %%% Local Variables: |
|
53 %%% mode: latex |
|
54 %%% TeX-master: "root" |
|
55 %%% End: |
|