1 (*<*) |
|
2 theory a2 = Main: |
|
3 (*>*) |
|
4 subsection {* Sorting \label{psv2002a2} *} |
|
5 |
|
6 text{* For simplicity we sort natural numbers. *} |
|
7 |
|
8 subsubsection{* Sorting with lists*} |
|
9 |
|
10 text {* |
|
11 The task is to define insertion sort and prove its correctness. |
|
12 The following functions are required: |
|
13 *} |
|
14 |
|
15 consts |
|
16 insort :: "nat \<Rightarrow> nat list \<Rightarrow> nat list" |
|
17 sort :: "nat list \<Rightarrow> nat list" |
|
18 le :: "nat \<Rightarrow> nat list \<Rightarrow> bool" |
|
19 sorted :: "nat list \<Rightarrow> bool" |
|
20 |
|
21 text {* In your definition, @{term "insort x xs"} should insert a |
|
22 number @{term x} into an already sorted list @{text xs}, and @{term |
|
23 "sort ys"} should build on @{text insort} to produce the sorted |
|
24 version of @{text ys}. |
|
25 |
|
26 To show that the resulting list is indeed sorted we need a predicate |
|
27 @{term sorted} that checks if each element in the list is less or equal |
|
28 to the following ones; @{term "le n xs"} should be true iff |
|
29 @{term n} is less or equal to all elements of @{text xs}. |
|
30 |
|
31 Start out by showing a monotonicity property of @{term le}. |
|
32 For technical reasons the lemma should be phrased as follows: |
|
33 *} |
|
34 lemma [simp]: "x \<le> y \<Longrightarrow> le y xs \<longrightarrow> le x xs" |
|
35 (*<*)oops(*>*) |
|
36 |
|
37 text {* Now show the following correctness theorem: *} |
|
38 theorem "sorted (sort xs)" |
|
39 (*<*)oops(*>*) |
|
40 |
|
41 text {* This theorem alone is too weak. It does not guarantee that the |
|
42 sorted list contains the same elements as the input. In the worst |
|
43 case, @{term sort} might always return @{term"[]"} --- surely an |
|
44 undesirable implementation of sorting. |
|
45 |
|
46 Define a function @{term "count xs x"} that counts how often @{term x} |
|
47 occurs in @{term xs}. Show that |
|
48 *} |
|
49 |
|
50 theorem "count (sort xs) x = count xs x" |
|
51 (*<*)oops(*>*) |
|
52 |
|
53 subsubsection {* Sorting with trees *} |
|
54 |
|
55 text {* Our second sorting algorithm uses trees. Thus you should first |
|
56 define a data type @{text bintree} of binary trees that are either |
|
57 empty or consist of a node carrying a natural number and two subtrees. |
|
58 |
|
59 Define a function @{text tsorted} that checks if a binary tree is |
|
60 sorted. It is convenien to employ two auxiliary functions @{text |
|
61 tge}/@{text tle} that test whether a number is |
|
62 greater-or-equal/less-or-equal to all elements of a tree. |
|
63 |
|
64 Finally define a function @{text tree_of} that turns a list into a |
|
65 sorted tree. It is helpful to base @{text tree_of} on a function |
|
66 @{term "ins n b"} that inserts a number @{term n} into a sorted tree |
|
67 @{term b}. |
|
68 |
|
69 Show |
|
70 *} |
|
71 theorem [simp]: "tsorted (tree_of xs)" |
|
72 (*<*)oops(*>*) |
|
73 |
|
74 text {* Again we have to show that no elements are lost (or added). |
|
75 As for lists, define a function @{term "tcount x b"} that counts the |
|
76 number of occurrences of the number @{term x} in the tree @{term b}. |
|
77 Show |
|
78 *} |
|
79 |
|
80 theorem "tcount (tree_of xs) x = count xs x" |
|
81 (*<*)oops(*>*) |
|
82 |
|
83 text {* Now we are ready to sort lists. We know how to produce an |
|
84 ordered tree from a list. Thus we merely need a function @{text |
|
85 list_of} that turns an (ordered) tree into an (ordered) list. |
|
86 Define this function and prove |
|
87 *} |
|
88 |
|
89 theorem "sorted (list_of (tree_of xs))" |
|
90 (*<*)oops(*>*) |
|
91 |
|
92 theorem "count (list_of (tree_of xs)) n = count xs n" |
|
93 (*<*)oops(*>*) |
|
94 |
|
95 text {* |
|
96 Hints: |
|
97 \begin{itemize} |
|
98 \item |
|
99 Try to formulate all your lemmas as equations rather than implications |
|
100 because that often simplifies their proof. |
|
101 Make sure that the right-hand side is (in some sense) |
|
102 simpler than the left-hand side. |
|
103 \item |
|
104 Eventually you need to relate @{text sorted} and @{text tsorted}. |
|
105 This is facilitated by a function @{text ge} on lists (analogously to |
|
106 @{text tge} on trees) and the following lemma (that you will need to prove): |
|
107 @{term[display] "sorted (a@x#b) = (sorted a \<and> sorted b \<and> ge x a \<and> le x b)"} |
|
108 \end{itemize} |
|
109 *} |
|
110 |
|
111 (*<*) |
|
112 end |
|
113 (*>*) |
|