(*
$Id: ex.thy,v 1.2 2004/11/23 15:14:34 webertj Exp $
Author: Gerwin Klein
*)
header {* Merge Sort *}
(*<*) theory ex imports Main begin (*>*)
subsection {* Sorting with lists *}
text {*
For simplicity we sort natural numbers.
Define a predicate @{term sorted} that checks if each element in the list is
less or equal to the following ones; @{term "le n xs"} should be true iff
@{term n} is less or equal to all elements of @{text xs}.
*}
consts
le :: "nat \ nat list \ bool"
sorted :: "nat list \ bool"
text {*
Define a function @{term "count xs x"} that counts how often @{term x} occurs
in @{term xs}.
*}
consts
count :: "nat list => nat => nat"
subsection {* Merge sort *}
text {*
Implement \emph{merge sort}: a list is sorted by splitting it into two lists,
sorting them separately, and merging the results.
With the help of @{text recdef} define two functions
*}
consts merge :: "nat list \ nat list \ nat list"
msort :: "nat list \ nat list"
text {* and show *}
theorem "sorted (msort xs)"
(*<*)oops(*>*)
theorem "count (msort xs) x = count xs x"
(*<*)oops(*>*)
text {*
You may have to prove lemmas about @{term sorted} and @{term count}.
Hints:
\begin{itemize}
\item For @{text recdef} see Section~3.5 of the Isabelle/HOL tutorial.
\item To split a list into two halves of almost equal length you can use the
functions \mbox{@{text "n div 2"}}, @{term take} und @{term drop}, where
@{term "take n xs"} returns the first @{text n} elements of @{text xs} and
@{text "drop n xs"} the remainder.
\item Here are some potentially useful lemmas:\\
@{text "linorder_not_le:"} @{thm linorder_not_le [no_vars]}\\
@{text "order_less_le:"} @{thm order_less_le [no_vars]}\\
@{text "min_def:"} @{thm min_def [no_vars]}
\end{itemize}
*}
(*<*) end (*>*)