theory Perlen3_WS1617_Blatt6 imports Main begin section \Trees\ text \ Wir betrachten folgenden einfachen Baumtyp und die Funktion @{term explode}: \ datatype tree = Tip | Node tree tree fun explode :: "nat \ tree \ tree" where "explode 0 t = t" | "explode (Suc n) t = explode n (Node t t)" text \ Schreiben Sie eine Funktion @{term "count :: tree \ nat"}, die die Knoten in einem Baum zählt, und beweisen Sie, wie sich die Operation @{term explode} auf die Größe des Baums auswirkt. Hinweis: Eine oft nützliche Sammlung algebraischer Umformungsregeln ist unter dem Namen @{thm algebra_simps} zusammengefasst. \ section \Polynome\ text \ Man kann Polynome in einer Variablen mit Integer-Koeffizienten durch folgenden Datentyp darstellen: \ datatype poly = Var | Const int | Add poly poly | Mul poly poly text \ Dabei wird z.B. $(4x - 2)x^2+5$ repräsentiert durch den term @{term "Add (Mul (Add (Mul (Const 4) Var) (Const (-2))) (Mul Var Var)) (Const 5)"}. Definieren Sie eine Funktion "eval", die ein Polynom an einer Stelle auswertet. \ text \ Eine alternative Darstellung von Polynomen ist eine Liste von Koeffizienten, beginnend mit dem niedrigsten. So steht z.B. die Liste $[4, 2, -1, 3]$ für das Polynom $3x^3 - x^2 + 2x + 4$. Definieren Sie eine Funktion @{term "evalc :: int list \ int \ int"}, die ein Polynom auswertet, das als Koeffizientenliste gegeben ist. Definieren Sie eine Funktion @{term "coeffs :: poly \ int list"}, die ein Polynom in eine Koeffizientenliste umwandelt. Dafür benötigen Sie ggf. Hilfsfunktionen. Zeigen Sie: \ lemma "evalc (coeffs p) x = eval p x" sorry end