13739
|
1 |
theory l2 = Main:
|
|
2 |
|
|
3 |
text {*
|
|
4 |
\section*{Sortieren auf Listen}
|
|
5 |
|
|
6 |
Der erste Teil des Blattes beschäftigt sich mit einem
|
|
7 |
einfachen Sortieralgorithmus auf Listen von natürlichen Zahlen.
|
|
8 |
Ihre Aufgabe ist es, den Sortieralgorithmus in Isabelle zu
|
|
9 |
programmieren und zu zeigen, dass Ihre Implementierung korrekt ist.
|
|
10 |
|
|
11 |
Der Algorithmus lässt sich in folgende Funktionen zerlegen:
|
|
12 |
*}
|
|
13 |
consts
|
|
14 |
insort :: "nat \<Rightarrow> nat list \<Rightarrow> nat list"
|
|
15 |
sort :: "nat list \<Rightarrow> nat list"
|
|
16 |
le :: "nat \<Rightarrow> nat list \<Rightarrow> bool"
|
|
17 |
sorted :: "nat list \<Rightarrow> bool"
|
|
18 |
text {*
|
|
19 |
Hierbei soll @{term "insort x xs"} eine Zahl @{term x} in eine
|
|
20 |
sortierte Liste @{text xs} einfügen, und die Funktion @{term "sort ys"}
|
|
21 |
(aufbauend auf @{text insort}) die sortierte Version von @{text ys}
|
|
22 |
liefern.
|
|
23 |
|
|
24 |
Um zu zeigen, dass die resultierende Liste tatsächlich sortiert
|
|
25 |
ist, benötigen sie das Prädikat @{term "sorted xs"}, das überprüft
|
|
26 |
ob jedes Element der Liste kleiner ist als alle folgenden Elemente
|
|
27 |
der Liste. Die Funktion @{term "le n xs"} soll genau dann wahr sein,
|
|
28 |
wenn @{term n} kleiner oder gleich allen Elementen von @{text xs}
|
|
29 |
ist.
|
|
30 |
*}
|
|
31 |
primrec
|
|
32 |
"le a [] = True"
|
|
33 |
"le a (x#xs) = (a <= x & le a xs)"
|
|
34 |
|
|
35 |
primrec
|
|
36 |
"sorted [] = True"
|
|
37 |
"sorted (x#xs) = (le x xs & sorted xs)"
|
|
38 |
|
|
39 |
primrec
|
|
40 |
"insort a [] = [a]"
|
|
41 |
"insort a (x#xs) = (if a <= x then a#x#xs else x # insort a xs)"
|
|
42 |
|
|
43 |
primrec
|
|
44 |
"sort [] = []"
|
|
45 |
"sort (x#xs) = insort x (sort xs)"
|
|
46 |
|
|
47 |
lemma "le 3 [7,10,3]" by auto
|
|
48 |
|
|
49 |
lemma "\<not> le 3 [7,10,2]" by auto
|
|
50 |
|
|
51 |
lemma "sorted [1,2,3,4]" by auto
|
|
52 |
|
|
53 |
lemma "\<not> sorted [3,1,4,2]" by auto
|
|
54 |
|
|
55 |
lemma "sort [3,1,4,2] = [1,2,3,4]" by auto
|
|
56 |
|
|
57 |
text {*
|
|
58 |
Zeigen Sie zu Beginn folgendes Monotonie-Lemma über @{term le}. Die
|
|
59 |
Formulierung des Lemmas ist aus technischen Gründen (über die sie
|
|
60 |
später mehr erfahren werden) etwas ungewohnt:
|
|
61 |
*}
|
|
62 |
lemma [simp]: "x \<le> y \<Longrightarrow> le y xs \<longrightarrow> le x xs"
|
|
63 |
apply (induct_tac xs)
|
|
64 |
apply auto
|
|
65 |
done
|
|
66 |
|
|
67 |
lemma [simp]:
|
|
68 |
"le x (insort a xs) = (x <= a & le x xs)"
|
|
69 |
apply (induct_tac xs)
|
|
70 |
apply auto
|
|
71 |
done
|
|
72 |
|
|
73 |
lemma [simp]:
|
|
74 |
"sorted (insort a xs) = sorted xs"
|
|
75 |
apply (induct_tac xs)
|
|
76 |
apply auto
|
|
77 |
done
|
|
78 |
|
|
79 |
theorem "sorted (sort xs)"
|
|
80 |
apply (induct_tac xs)
|
|
81 |
apply auto
|
|
82 |
done
|
|
83 |
|
|
84 |
text {*
|
|
85 |
Das Theorem sagt zwar aus, dass Ihr Algorithmus eine sortierte
|
|
86 |
Liste zurückgibt, es gibt Ihnen aber nicht die Sicherheit, dass die sortierte
|
|
87 |
Liste auch die gleichen Elemente wie das Original enthält. Formulieren Sie deswegen
|
|
88 |
eine Funktion @{term "count xs x"}, die zählt, wie oft die Zahl
|
|
89 |
@{term x} in @{term xs} vorkommt.
|
|
90 |
*}
|
|
91 |
consts
|
|
92 |
count :: "nat list => nat => nat"
|
|
93 |
primrec
|
|
94 |
"count [] y = 0"
|
|
95 |
"count (x#xs) y = (if x=y then Suc(count xs y) else count xs y)"
|
|
96 |
|
|
97 |
lemma "count [2,3,1,3] 3 = 2" by auto
|
|
98 |
|
|
99 |
lemma "count [2,3,1,3] 7 = 0" by auto
|
|
100 |
|
|
101 |
lemma "count [2,3,1,3] 2 = 1" by auto
|
|
102 |
|
|
103 |
lemma [simp]:
|
|
104 |
"count (insort x xs) y =
|
|
105 |
(if x=y then Suc (count xs y) else count xs y)"
|
|
106 |
apply (induct_tac xs)
|
|
107 |
apply auto
|
|
108 |
done
|
|
109 |
|
|
110 |
theorem "count (sort xs) x = count xs x"
|
|
111 |
apply (induct_tac xs)
|
|
112 |
apply auto
|
|
113 |
done
|
|
114 |
|
|
115 |
text {*
|
|
116 |
\section*{Sortieren mit Bäumen}
|
|
117 |
|
|
118 |
Der zweite Teil des Blattes beschäftigt sich mit einem
|
|
119 |
Sortieralgorithmus, der Bäume verwendet.
|
|
120 |
Definieren Sie dazu zuerst den Datentyp @{text bintree} der
|
|
121 |
Binärbäume. Für diese Aufgabe sind Binärbäume entweder leer, oder
|
|
122 |
bestehen aus einem
|
|
123 |
Knoten mit einer natürlichen Zahl und zwei Unterbäumen.
|
|
124 |
|
|
125 |
Schreiben Sie dann eine Funktion @{text tsorted}, die feststellt, ob
|
|
126 |
ein Binärbaum geordnet ist. Sie werden dazu zwei Hilfsfunktionen
|
|
127 |
@{text tge} und @{text tle} benötigen, die überprüfen ob eine Zahl
|
|
128 |
grössergleich/kleinergleich als alle Elemente eines Baumes sind.
|
|
129 |
|
|
130 |
Formulieren Sie schliesslich eine Funktion @{text tree_of}, die zu einer
|
|
131 |
(unsortierten) Liste den geordneten Binärbaum zurückgibt. Stützen Sie
|
|
132 |
sich dabei auf eine Funktion @{term "ins n b"}, die eine Zahl @{term
|
|
133 |
n} in einen geordneten Binärbaum @{term b} einfügt.
|
|
134 |
*}
|
|
135 |
|
|
136 |
datatype bintree = Empty | Node nat bintree bintree
|
|
137 |
|
|
138 |
consts
|
|
139 |
tsorted :: "bintree \<Rightarrow> bool"
|
|
140 |
tge :: "nat \<Rightarrow> bintree \<Rightarrow> bool"
|
|
141 |
tle :: "nat \<Rightarrow> bintree \<Rightarrow> bool"
|
|
142 |
ins :: "nat \<Rightarrow> bintree \<Rightarrow> bintree"
|
|
143 |
tree_of :: "nat list \<Rightarrow> bintree"
|
|
144 |
|
|
145 |
primrec
|
|
146 |
"tsorted Empty = True"
|
|
147 |
"tsorted (Node n t1 t2) = (tsorted t1 \<and> tsorted t2 \<and> tge n t1 \<and> tle n t2)"
|
|
148 |
|
|
149 |
primrec
|
|
150 |
"tge x Empty = True"
|
|
151 |
"tge x (Node n t1 t2) = (n \<le> x \<and> tge x t1 \<and> tge x t2)"
|
|
152 |
|
|
153 |
primrec
|
|
154 |
"tle x Empty = True"
|
|
155 |
"tle x (Node n t1 t2) = (x \<le> n \<and> tle x t1 \<and> tle x t2)"
|
|
156 |
|
|
157 |
primrec
|
|
158 |
"ins x Empty = Node x Empty Empty"
|
|
159 |
"ins x (Node n t1 t2) = (if x \<le> n then Node n (ins x t1) t2 else Node n t1 (ins x t2))"
|
|
160 |
|
|
161 |
primrec
|
|
162 |
"tree_of [] = Empty"
|
|
163 |
"tree_of (x#xs) = ins x (tree_of xs)"
|
|
164 |
|
|
165 |
|
|
166 |
lemma "tge 5 (Node 3 (Node 2 Empty Empty) Empty)" by auto
|
|
167 |
|
|
168 |
lemma "\<not> tge 5 (Node 3 Empty (Node 7 Empty Empty))" by auto
|
|
169 |
|
|
170 |
lemma "\<not> tle 5 (Node 3 (Node 2 Empty Empty) Empty)" by auto
|
|
171 |
|
|
172 |
lemma "\<not> tle 5 (Node 3 Empty (Node 7 Empty Empty))" by auto
|
|
173 |
|
|
174 |
lemma "tle 3 (Node 3 Empty (Node 7 Empty Empty))" by auto
|
|
175 |
|
|
176 |
lemma "tsorted (Node 3 Empty (Node 7 Empty Empty))" by auto
|
|
177 |
|
|
178 |
lemma "tree_of [3,2] = Node 2 Empty (Node 3 Empty Empty)" by auto
|
|
179 |
|
|
180 |
lemma [simp]:
|
|
181 |
"tge a (ins x t) = (x \<le> a \<and> tge a t)"
|
|
182 |
apply (induct_tac t)
|
|
183 |
apply auto
|
|
184 |
done
|
|
185 |
|
|
186 |
lemma [simp]:
|
|
187 |
"tle a (ins x t) = (a \<le> x \<and> tle a t)"
|
|
188 |
apply (induct_tac t)
|
|
189 |
apply auto
|
|
190 |
done
|
|
191 |
|
|
192 |
lemma [simp]:
|
|
193 |
"tsorted (ins x t) = tsorted t"
|
|
194 |
apply (induct_tac t)
|
|
195 |
apply auto
|
|
196 |
done
|
|
197 |
|
|
198 |
theorem [simp]: "tsorted (tree_of xs)"
|
|
199 |
apply (induct_tac xs)
|
|
200 |
apply auto
|
|
201 |
done
|
|
202 |
|
|
203 |
text {*
|
|
204 |
Auch bei diesem Algorithmus müssen wir noch zeigen, dass keine
|
|
205 |
Elemente beim Sortieren verloren gehen (oder erfunden werden). Formulieren
|
|
206 |
Sie analog zu den Listen eine Funktion @{term "tcount x b"}, die zählt, wie
|
|
207 |
oft die Zahl @{term x} im Baum @{term b} vorkommt.
|
|
208 |
*}
|
|
209 |
consts
|
|
210 |
tcount :: "bintree => nat => nat"
|
|
211 |
primrec
|
|
212 |
"tcount Empty y = 0"
|
|
213 |
"tcount (Node x t1 t2) y =
|
|
214 |
(if x=y
|
|
215 |
then Suc (tcount t1 y + tcount t2 y)
|
|
216 |
else tcount t1 y + tcount t2 y)"
|
|
217 |
|
|
218 |
lemma [simp]:
|
|
219 |
"tcount (ins x t) y =
|
|
220 |
(if x=y then Suc (tcount t y) else tcount t y)"
|
|
221 |
apply(induct_tac t)
|
|
222 |
apply auto
|
|
223 |
done
|
|
224 |
|
|
225 |
theorem "tcount (tree_of xs) x = count xs x"
|
|
226 |
apply (induct_tac xs)
|
|
227 |
apply auto
|
|
228 |
done
|
|
229 |
|
|
230 |
text {*
|
|
231 |
Die eigentliche Aufgabe war es, Listen zu sortieren. Bis jetzt haben
|
|
232 |
wir lediglich einen Algorithmus, der Listen in geordnete Bäume
|
|
233 |
transformiert. Definieren Sie deswegen eine Funktion @{text
|
|
234 |
list_of}, die zu einen (geordneten) Baum eine (geordnete) Liste liefert.
|
|
235 |
*}
|
|
236 |
|
|
237 |
consts
|
|
238 |
ge :: "nat \<Rightarrow> nat list \<Rightarrow> bool"
|
|
239 |
list_of :: "bintree \<Rightarrow> nat list"
|
|
240 |
|
|
241 |
primrec
|
|
242 |
"ge a [] = True"
|
|
243 |
"ge a (x#xs) = (x \<le> a \<and> ge a xs)"
|
|
244 |
|
|
245 |
primrec
|
|
246 |
"list_of Empty = []"
|
|
247 |
"list_of (Node n t1 t2) = list_of t1 @ [n] @ list_of t2"
|
|
248 |
|
|
249 |
|
|
250 |
lemma [simp]:
|
|
251 |
"le x (a@b) = (le x a \<and> le x b)"
|
|
252 |
apply (induct_tac a)
|
|
253 |
apply auto
|
|
254 |
done
|
|
255 |
|
|
256 |
lemma [simp]:
|
|
257 |
"ge x (a@b) = (ge x a \<and> ge x b)"
|
|
258 |
apply (induct_tac a)
|
|
259 |
apply auto
|
|
260 |
done
|
|
261 |
|
|
262 |
lemma [simp]:
|
|
263 |
"sorted (a@x#b) = (sorted a \<and> sorted b \<and> ge x a \<and> le x b)"
|
|
264 |
apply (induct_tac a)
|
|
265 |
apply auto
|
|
266 |
done
|
|
267 |
|
|
268 |
lemma [simp]:
|
|
269 |
"ge n (list_of t) = tge n t"
|
|
270 |
apply (induct_tac t)
|
|
271 |
apply auto
|
|
272 |
done
|
|
273 |
|
|
274 |
lemma [simp]:
|
|
275 |
"le n (list_of t) = tle n t"
|
|
276 |
apply (induct_tac t)
|
|
277 |
apply auto
|
|
278 |
done
|
|
279 |
|
|
280 |
lemma [simp]:
|
|
281 |
"sorted (list_of t) = tsorted t"
|
|
282 |
apply (induct_tac t)
|
|
283 |
apply auto
|
|
284 |
done
|
|
285 |
|
|
286 |
theorem "sorted (list_of (tree_of xs))"
|
|
287 |
apply auto
|
|
288 |
done
|
|
289 |
|
|
290 |
lemma count_append [simp]:
|
|
291 |
"count (a@b) n = count a n + count b n"
|
|
292 |
apply (induct a)
|
|
293 |
apply auto
|
|
294 |
done
|
|
295 |
|
|
296 |
lemma [simp]:
|
|
297 |
"count (list_of b) n = tcount b n"
|
|
298 |
apply (induct b)
|
|
299 |
apply auto
|
|
300 |
done
|
|
301 |
|
|
302 |
theorem "count (list_of (tree_of xs)) n = count xs n"
|
|
303 |
apply (induct xs)
|
|
304 |
apply auto
|
|
305 |
done
|
|
306 |
|
|
307 |
end
|