Bws bzgl. Fkt. über allg. Datentypen
------------------------------------
Strukturelle Induktion
Beweistechnik: Wenn A ein alg. Datentyp mit Kontstruktoren K_1 K_T ist, dann kann eine Aussage P
zu Elementen des Datentyp A bewiesen werden, indem eine Fallunterscheidung vorgenommen wird.
Zeige P für ELemente der Form K_1...,
zeige P für ELemente der Form K_o
wobei für rek. Konstruktoren die Eigenschaft P für allg. Ag. Des Types A vorrausgesetzt werden kann.
-- fallunterscheidung mit cases
-- case ausdruck = true, dann gleichung einsetzen, alle anderen cases als false
Binärbäume: Bws.:
data Tree a = Nil | Node a (Tree a) (Tree a)
collapse Nil = []
collapse (Node x t1 t2) = collapse t1 ++ [x] ++ collapse t2
mapTree f Nil = Nil
mapTree f (Node x t1 t2) = Node (f x) (mapTree f t1) (mapTree f t2)
map f [] = []
map f (x:xs) = fx:(map f xs)
Satz: collapse (mapTree f t) = map f (collapse t) für alle
f :: a -> b und t :: Tree a
Bws: -- strukt. Ind über aufbau von t
Nil - Fall: collapse (mapTree f Nil)