header {* Funktionen auf Listen *};

theory Aufgabe1 = Main:

text{*
Definieren Sie eine Funktion @{term replace}, so dass @{term"replace x y zs"}
bedeutet ``ersetze \"uberall @{term x} durch @{term y} in @{term zs}''.
*}

consts replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"

text {*
Beweisen oder widerlegen Sie (mit Gegenbeispiel) nun folgende Theoreme.
Eventuell m\"ussen Sie dazu erst einige Lemmas beweisen.
*};

theorem "rev(replace x y zs) = replace x y (rev zs)"
oops

theorem "replace x y (replace u v zs) = replace u v (replace x y zs)"
oops

theorem "replace y z (replace x y zs) = replace x z zs"
oops

text{*
Definieren Sie zwei Funktion zum Entfernen von Elementen aus Listen:
@{term"del1 x xs"} soll das erste Vorkommen (von links) von @{term x} in
@{term xs} entfernen, @{term"delall x xs"} alle.
*}

consts del1   :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
       delall :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"


text {*
Beweisen oder widerlegen Sie (mit Gegenbeispiel) nun folgende Theoreme.
*};

theorem "del1 x (delall x xs) = delall x xs"
oops

theorem "delall x (delall x xs) = delall x xs"
oops

theorem "delall x (del1 x xs) = delall x xs"
oops

theorem "del1 x (del1 y zs) = del1 y (del1 x zs)"
oops

theorem "delall x (del1 y zs) = del1 y (delall x zs)"
oops

theorem "delall x (delall y zs) = delall y (delall x zs)"
oops

theorem "del1 y (replace x y xs) = del1 x xs"
oops

theorem "delall y (replace x y xs) = delall x xs"
oops

theorem "replace x y (delall x zs) = delall x zs"
oops

theorem "replace x y (delall z zs) = delall z (replace x y zs)"
oops

theorem "rev(del1 x xs) = del1 x (rev xs)"
oops

theorem "rev(delall x xs) = delall x (rev xs)"
oops

end;