theory l2 = Main:
text {*
\section*{Sortieren auf Listen}
Der erste Teil des Blattes beschäftigt sich mit einem
einfachen Sortieralgorithmus auf Listen von natürlichen Zahlen.
Ihre Aufgabe ist es, den Sortieralgorithmus in Isabelle zu
programmieren und zu zeigen, dass Ihre Implementierung korrekt ist.
Der Algorithmus lässt sich in folgende Funktionen zerlegen:
*}
consts
insort :: "nat \<Rightarrow> nat list \<Rightarrow> nat list"
sort :: "nat list \<Rightarrow> nat list"
le :: "nat \<Rightarrow> nat list \<Rightarrow> bool"
sorted :: "nat list \<Rightarrow> bool"
text {*
Hierbei soll @{term "insort x xs"} eine Zahl @{term x} in eine
sortierte Liste @{text xs} einfügen, und die Funktion @{term "sort ys"}
(aufbauend auf @{text insort}) die sortierte Version von @{text ys}
liefern.
Um zu zeigen, dass die resultierende Liste tatsächlich sortiert
ist, benötigen sie das Prädikat @{term "sorted xs"}, das überprüft
ob jedes Element der Liste kleiner ist als alle folgenden Elemente
der Liste. Die Funktion @{term "le n xs"} soll genau dann wahr sein,
wenn @{term n} kleiner oder gleich allen Elementen von @{text xs}
ist.
*}
primrec
"le a [] = True"
"le a (x#xs) = (a <= x & le a xs)"
primrec
"sorted [] = True"
"sorted (x#xs) = (le x xs & sorted xs)"
primrec
"insort a [] = [a]"
"insort a (x#xs) = (if a <= x then a#x#xs else x # insort a xs)"
primrec
"sort [] = []"
"sort (x#xs) = insort x (sort xs)"
lemma "le 3 [7,10,3]" by auto
lemma "\<not> le 3 [7,10,2]" by auto
lemma "sorted [1,2,3,4]" by auto
lemma "\<not> sorted [3,1,4,2]" by auto
lemma "sort [3,1,4,2] = [1,2,3,4]" by auto
text {*
Zeigen Sie zu Beginn folgendes Monotonie-Lemma über @{term le}. Die
Formulierung des Lemmas ist aus technischen Gründen (über die sie
später mehr erfahren werden) etwas ungewohnt:
*}
lemma [simp]: "x \<le> y \<Longrightarrow> le y xs \<longrightarrow> le x xs"
apply (induct_tac xs)
apply auto
done
lemma [simp]:
"le x (insort a xs) = (x <= a & le x xs)"
apply (induct_tac xs)
apply auto
done
lemma [simp]:
"sorted (insort a xs) = sorted xs"
apply (induct_tac xs)
apply auto
done
theorem "sorted (sort xs)"
apply (induct_tac xs)
apply auto
done
text {*
Das Theorem sagt zwar aus, dass Ihr Algorithmus eine sortierte
Liste zurückgibt, es gibt Ihnen aber nicht die Sicherheit, dass die sortierte
Liste auch die gleichen Elemente wie das Original enthält. Formulieren Sie deswegen
eine Funktion @{term "count xs x"}, die zählt, wie oft die Zahl
@{term x} in @{term xs} vorkommt.
*}
consts
count :: "nat list => nat => nat"
primrec
"count [] y = 0"
"count (x#xs) y = (if x=y then Suc(count xs y) else count xs y)"
lemma "count [2,3,1,3] 3 = 2" by auto
lemma "count [2,3,1,3] 7 = 0" by auto
lemma "count [2,3,1,3] 2 = 1" by auto
lemma [simp]:
"count (insort x xs) y =
(if x=y then Suc (count xs y) else count xs y)"
apply (induct_tac xs)
apply auto
done
theorem "count (sort xs) x = count xs x"
apply (induct_tac xs)
apply auto
done
text {*
\section*{Sortieren mit Bäumen}
Der zweite Teil des Blattes beschäftigt sich mit einem
Sortieralgorithmus, der Bäume verwendet.
Definieren Sie dazu zuerst den Datentyp @{text bintree} der
Binärbäume. Für diese Aufgabe sind Binärbäume entweder leer, oder
bestehen aus einem
Knoten mit einer natürlichen Zahl und zwei Unterbäumen.
Schreiben Sie dann eine Funktion @{text tsorted}, die feststellt, ob
ein Binärbaum geordnet ist. Sie werden dazu zwei Hilfsfunktionen
@{text tge} und @{text tle} benötigen, die überprüfen ob eine Zahl
grössergleich/kleinergleich als alle Elemente eines Baumes sind.
Formulieren Sie schliesslich eine Funktion @{text tree_of}, die zu einer
(unsortierten) Liste den geordneten Binärbaum zurückgibt. Stützen Sie
sich dabei auf eine Funktion @{term "ins n b"}, die eine Zahl @{term
n} in einen geordneten Binärbaum @{term b} einfügt.
*}
datatype bintree = Empty | Node nat bintree bintree
consts
tsorted :: "bintree \<Rightarrow> bool"
tge :: "nat \<Rightarrow> bintree \<Rightarrow> bool"
tle :: "nat \<Rightarrow> bintree \<Rightarrow> bool"
ins :: "nat \<Rightarrow> bintree \<Rightarrow> bintree"
tree_of :: "nat list \<Rightarrow> bintree"
primrec
"tsorted Empty = True"
"tsorted (Node n t1 t2) = (tsorted t1 \<and> tsorted t2 \<and> tge n t1 \<and> tle n t2)"
primrec
"tge x Empty = True"
"tge x (Node n t1 t2) = (n \<le> x \<and> tge x t1 \<and> tge x t2)"
primrec
"tle x Empty = True"
"tle x (Node n t1 t2) = (x \<le> n \<and> tle x t1 \<and> tle x t2)"
primrec
"ins x Empty = Node x Empty Empty"
"ins x (Node n t1 t2) = (if x \<le> n then Node n (ins x t1) t2 else Node n t1 (ins x t2))"
primrec
"tree_of [] = Empty"
"tree_of (x#xs) = ins x (tree_of xs)"
lemma "tge 5 (Node 3 (Node 2 Empty Empty) Empty)" by auto
lemma "\<not> tge 5 (Node 3 Empty (Node 7 Empty Empty))" by auto
lemma "\<not> tle 5 (Node 3 (Node 2 Empty Empty) Empty)" by auto
lemma "\<not> tle 5 (Node 3 Empty (Node 7 Empty Empty))" by auto
lemma "tle 3 (Node 3 Empty (Node 7 Empty Empty))" by auto
lemma "tsorted (Node 3 Empty (Node 7 Empty Empty))" by auto
lemma "tree_of [3,2] = Node 2 Empty (Node 3 Empty Empty)" by auto
lemma [simp]:
"tge a (ins x t) = (x \<le> a \<and> tge a t)"
apply (induct_tac t)
apply auto
done
lemma [simp]:
"tle a (ins x t) = (a \<le> x \<and> tle a t)"
apply (induct_tac t)
apply auto
done
lemma [simp]:
"tsorted (ins x t) = tsorted t"
apply (induct_tac t)
apply auto
done
theorem [simp]: "tsorted (tree_of xs)"
apply (induct_tac xs)
apply auto
done
text {*
Auch bei diesem Algorithmus müssen wir noch zeigen, dass keine
Elemente beim Sortieren verloren gehen (oder erfunden werden). Formulieren
Sie analog zu den Listen eine Funktion @{term "tcount x b"}, die zählt, wie
oft die Zahl @{term x} im Baum @{term b} vorkommt.
*}
consts
tcount :: "bintree => nat => nat"
primrec
"tcount Empty y = 0"
"tcount (Node x t1 t2) y =
(if x=y
then Suc (tcount t1 y + tcount t2 y)
else tcount t1 y + tcount t2 y)"
lemma [simp]:
"tcount (ins x t) y =
(if x=y then Suc (tcount t y) else tcount t y)"
apply(induct_tac t)
apply auto
done
theorem "tcount (tree_of xs) x = count xs x"
apply (induct_tac xs)
apply auto
done
text {*
Die eigentliche Aufgabe war es, Listen zu sortieren. Bis jetzt haben
wir lediglich einen Algorithmus, der Listen in geordnete Bäume
transformiert. Definieren Sie deswegen eine Funktion @{text
list_of}, die zu einen (geordneten) Baum eine (geordnete) Liste liefert.
*}
consts
ge :: "nat \<Rightarrow> nat list \<Rightarrow> bool"
list_of :: "bintree \<Rightarrow> nat list"
primrec
"ge a [] = True"
"ge a (x#xs) = (x \<le> a \<and> ge a xs)"
primrec
"list_of Empty = []"
"list_of (Node n t1 t2) = list_of t1 @ [n] @ list_of t2"
lemma [simp]:
"le x (a@b) = (le x a \<and> le x b)"
apply (induct_tac a)
apply auto
done
lemma [simp]:
"ge x (a@b) = (ge x a \<and> ge x b)"
apply (induct_tac a)
apply auto
done
lemma [simp]:
"sorted (a@x#b) = (sorted a \<and> sorted b \<and> ge x a \<and> le x b)"
apply (induct_tac a)
apply auto
done
lemma [simp]:
"ge n (list_of t) = tge n t"
apply (induct_tac t)
apply auto
done
lemma [simp]:
"le n (list_of t) = tle n t"
apply (induct_tac t)
apply auto
done
lemma [simp]:
"sorted (list_of t) = tsorted t"
apply (induct_tac t)
apply auto
done
theorem "sorted (list_of (tree_of xs))"
apply auto
done
lemma count_append [simp]:
"count (a@b) n = count a n + count b n"
apply (induct a)
apply auto
done
lemma [simp]:
"count (list_of b) n = tcount b n"
apply (induct b)
apply auto
done
theorem "count (list_of (tree_of xs)) n = count xs n"
apply (induct xs)
apply auto
done
end