(*
$Id: ex.thy,v 1.2 2004/11/23 15:14:34 webertj Exp $
Author: Gerwin Klein
*)
header {* Sorting with Lists and Trees *}
(*<*) theory ex imports Main begin (*>*)
text {*
For simplicity we sort natural numbers.
*}
subsubsection {* Sorting with lists *}
text {*
The task is to define insertion sort and prove its correctness. The
following functions are required:
*}
consts
insort :: "nat \ nat list \ nat list"
sort :: "nat list \ nat list"
le :: "nat \ nat list \ bool"
sorted :: "nat list \ bool"
text {*
In your definition, @{term "insort x xs"} should insert a number @{term x}
into an already sorted list @{text xs}, and @{term "sort ys"} should build on
@{text insort} to produce the sorted version of @{text ys}.
To show that the resulting list is indeed sorted we need 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}.
*}
text {*
Start out by showing a monotonicity property of @{term le}. For technical
reasons the lemma should be phrased as follows:
*}
lemma [simp]: "x \ y \ le y xs \ le x xs"
(*<*) oops (*>*)
text {*
Now show the following correctness theorem:
*}
theorem "sorted (sort xs)"
(*<*) oops (*>*)
text {*
This theorem alone is too weak. It does not guarantee that the sorted list
contains the same elements as the input. In the worst case, @{term sort}
might always return @{term"[]"}~-- surely an undesirable implementation of
sorting.
Define a function @{term "count xs x"} that counts how often @{term x} occurs
in @{term xs}.
*}
text {*
Show that
*}
theorem "count (sort xs) x = count xs x"
(*<*) oops (*>*)
subsubsection {* Sorting with trees *}
text {*
Our second sorting algorithm uses trees. Thus you should first define a data
type @{text bintree} of binary trees that are either empty or consist of a
node carrying a natural number and two subtrees.
*}
text {*
Define a function @{text tsorted} that checks if a binary tree is sorted. It
is convenient to employ two auxiliary functions @{text tge}/@{text tle} that
test whether a number is greater-or-equal/less-or-equal to all elements of a
tree.
Finally define a function @{text tree_of} that turns a list into a sorted
tree. It is helpful to base @{text tree_of} on a function @{term "ins n b"}
that inserts a number @{term n} into a sorted tree @{term b}.
*}
text {*
Show
*}
theorem [simp]: "tsorted (tree_of xs)"
(*<*) oops (*>*)
text {*
Again we have to show that no elements are lost (or added). As for lists,
define a function @{term "tcount x b"} that counts the number of occurrences
of the number @{term x} in the tree @{term b}.
*}
text {*
Show
*}
theorem "tcount (tree_of xs) x = count xs x"
(*<*) oops (*>*)
text {*
Now we are ready to sort lists. We know how to produce an ordered tree from
a list. Thus we merely need a function @{text list_of} that turns an
(ordered) tree into an (ordered) list. Define this function and prove
*}
theorem "sorted (list_of (tree_of xs))"
(*<*) oops (*>*)
theorem "count (list_of (tree_of xs)) n = count xs n"
(*<*) oops (*>*)
text {*
Hints:
\begin{itemize}
\item
Try to formulate all your lemmas as equations rather than implications
because that often simplifies their proof. Make sure that the right-hand
side is (in some sense) simpler than the left-hand side.
\item
Eventually you need to relate @{text sorted} and @{text tsorted}. This is
facilitated by a function @{text ge} on lists (analogously to @{text tge} on
trees) and the following lemma (that you will need to prove):\\
@{term[display] "sorted (a@x#b) = (sorted a \ sorted b \ ge x a
\ le x b)"}
\end{itemize}
*}
(*<*) end (*>*)