header "Funktionen auf Listen"

(*<*)
theory a1 = Main:
(*>*)
text {*
  Definieren Sie den All- und den Existenz-Quantor für Listen.
  Die Funktion @{term "alls P xs"} soll genau dann wahr sein, wenn @{term "P x"}
  für jedes Element @{term x} der Liste @{term xs} wahr ist; analog soll 
  \mbox{@{term "exs P xs"}} wahr sein, wenn @{term P} für mindestens ein Element wahr ist.
*}
consts 
  alls :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
  exs  :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
text_raw {*
  \isamarkuptrue\isanewline
  \isacommand{primrec}\isanewline
  \ \ \isacommand{oops}\isanewline
  \isamarkupfalse
*}
text {* 
  Zeigen oder widerlegen Sie (mit Gegenbeispiel) folgende Lemmas. 
  Sie benötigen unter Umständen zusätzliche Lemmas, damit der Beweis funktioniert.
  Benutzen Sie das @{text "[simp]"}-Attribut nur, wenn die Gleichung, die Sie zeigen, 
  eine wirkliche Vereinfachung ist, oder Sie die Aussage als Lemma für
  einen späteren Beweis brauchen.
*}

lemma [simp]: "alls (\<lambda>x. P x \<and> Q x) xs = (alls P xs \<and> alls Q xs)"
  oops

lemma "alls P (rev xs) = alls P xs"
  oops

lemma "exs (\<lambda>x. P x \<and> Q x) xs = (exs P xs \<and> exs Q xs)"
  oops 

lemma "exs P (map f xs) = exs (P o f) xs"
  oops

lemma "exs P (rev xs) = exs P xs"
  oops

text {*
  Finden Sie ein @{text Z}, so dass folgende Gleichung gilt:
*}
lemma "exs (\<lambda>x. P x \<or> Q x) xs = Z"
  oops

text {*
  Drücken Sie den Existenzquantor durch den Allquantor aus (auf der
  rechten Seite soll kein @{text exs} mehr vorkommen).
*}
lemma "exs P xs = Z"
  oops

text {*
  Definieren Sie eine Funktion @{term "is_in x xs"}, die testet ob
  @{term x} in der Liste @{term xs} vorkommt. *}
text_raw {*
  \isamarkuptrue
  \isacommand{consts}\isanewline
  \ \ \isacommand{oops}\isamarkupfalse
*}
text {*
  Drücken Sie dann die Funktion @{text is_in} mit Hilfe des Existenzquantors
  auf Listen aus, und beweisen Sie, das ihre Gleichung stimmt.
*}
lemma "is_in a xs = Z"
  oops

text {*
  Schreiben Sie eine Funktion @{term "nodups xs"}, die genau dann wahr
  ist, wenn jedes Element von @{term xs} nur einmal in der Liste vorkommt.
  Definieren Sie zusätzlich eine Funktion @{term "deldups xs"}, die Duplikate
  aus Listen entfernt.

  Zeigen oder widerlegen Sie dann (mit Gegenbeispiel) folgende Lemmas.
*}
lemma "length (deldups xs) <= length xs"
  oops

lemma "nodups (deldups xs)"
  oops

lemma "deldups (rev xs) = rev (deldups xs)"
  oops

(*<*)
end
(*>*)