header {* Funktionen auf Listen *};

(*<*) theory Aufgabe = Main: (*>*)

text{*
Definieren Sie eine Funktion @{term occurs}, so dass @{term"occurs x xs"}
die Anzahl der Vorkommen von @{term x} in der Liste @{term xs} ist.
*}
(*<*) consts (*>*)
  occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat"

text {*
Beweisen oder widerlegen Sie (mit Gegenbeispiel) nun folgende Theoreme.
Eventuell m\"ussen Sie dazu erst einige Lemmas beweisen. Im Fall von Widerlegungen, suchen Sie einige sinnvolle Vorbedingungen damit die Theoreme gelten. 
*};
theorem [simp]:"occurs a (xs @ ys) = occurs a xs + occurs a ys "
oops
theorem "occurs a xs = occurs a (rev xs)"
oops
theorem "occurs a xs <= length xs"
oops
theorem "occurs a (replicate n a) = n"
oops
text{*
Definieren Sie eine Funktion @{term areAll}, so dass @{term"areAll xs x"} gilt,
genau dann wenn alle Elemente von @{term xs} gleich @{term x} sind.
*}
(*<*) consts (*>*)
  areAll :: "'a list \<Rightarrow> 'a \<Rightarrow> bool"

theorem "areAll xs a \<longrightarrow> occurs a xs = length xs"
oops
theorem "occurs a xs = length xs \<longrightarrow> areAll xs a"
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"} soll alle Vorkommen von @{term x} in
@{term xs} entfernen.
*}
(*<*) consts (*>*)
  delall :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
  del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"

theorem "occurs a (delall a xs) = 0"
oops
theorem "Suc (occurs a (del1 a xs)) = occurs a xs"
oops
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"

theorem "occurs a xs = occurs b (replace a b xs)"
oops
text{* Mit Hilfe von @{term occurs}, definieren Sie eine Funktion @{term remDups}, die alle doppelten Vorkommen aus der gegebenen Liste entfernt.*}
(*<*) consts (*>*)
  remDups :: "'a list \<Rightarrow> 'a list"
text{* Formulieren und beweisen Sie ein Lemma, das besagt, dass @{term remDups} keine neuen Elemente in eine Liste einf\"ugt. *}
text{* Formulieren und beweisen Sie ein Lemma, das besagt, dass @{term remDups} immer eine Liste mit paarweise verschiedenen Elementen erzeugt (d.h. die Korrektheit von @{term remDups}).*}
text{* Mit Hilfe von @{term occurs}, definieren Sie jetzt eine Funktion @{term unique}, so dass @{term"unique xs"} gilt, genau dann wenn jedes Element in @{term xs} genau einmal vorkommt.
*}
(*<*) consts (*>*)
  unique :: "'a list \<Rightarrow> bool"

text{* Mit Hilfe von @{term unique}, formulieren und beweisen Sie die Korrektheit von @{term remDups}.*}
(*<*) end (*>*)