--- a/doc-src/Exercises/2002/a5/l2.thy Fri Apr 29 18:13:28 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,307 +0,0 @@
-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