--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2002/a5/l2.thy Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,307 @@
+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