equal
deleted
inserted
replaced
1 (*<*) |
|
2 theory a5 = Main: |
|
3 (*>*) |
|
4 |
|
5 subsection {* Merge sort *} |
|
6 |
|
7 text {* Implement \emph{merge sort}: a list is sorted by splitting it |
|
8 into two lists, sorting them separately, and merging the results. |
|
9 |
|
10 With the help of @{text recdef} define two functions |
|
11 *} |
|
12 |
|
13 consts merge :: "nat list \<times> nat list \<Rightarrow> nat list" |
|
14 msort :: "nat list \<Rightarrow> nat list" |
|
15 |
|
16 text {* and show *} |
|
17 |
|
18 theorem "sorted (msort xs)" |
|
19 (*<*)oops(*>*) |
|
20 |
|
21 theorem "count (msort xs) x = count xs x" |
|
22 (*<*)oops(*>*) |
|
23 |
|
24 text {* where @{term sorted} and @{term count} are defined as in |
|
25 section~\ref{psv2002a2}. |
|
26 |
|
27 Hints: |
|
28 \begin{itemize} |
|
29 \item For @{text recdef} see section~3.5 of \cite{isabelle-tutorial}. |
|
30 |
|
31 \item To split a list into two halves of almost equal length you can |
|
32 use the functions \mbox{@{text "n div 2"}}, @{term take} und @{term drop}, |
|
33 where @{term "take n xs"} returns the first @{text n} elements of |
|
34 @{text xs} and @{text "drop n xs"} the remainder. |
|
35 |
|
36 \item Here are some potentially useful lemmas:\\ |
|
37 @{text "linorder_not_le:"} @{thm linorder_not_le [no_vars]}\\ |
|
38 @{text "order_less_le:"} @{thm order_less_le [no_vars]}\\ |
|
39 @{text "min_def:"} @{thm min_def [no_vars]} |
|
40 \end{itemize} |
|
41 *} |
|
42 |
|
43 (*<*) |
|
44 end |
|
45 (*>*) |
|