header "Funktionen auf Listen (Lösungsvorschlag)"

theory l1 = 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"

primrec 
  "alls P [] = True"
  "alls P (x#xs) = (if \<not>P x then False else alls P xs)"

primrec
  "exs P [] = False"
  "exs P (x#xs) = (if P x then True else exs P xs)"
  
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)"
  apply (induct_tac xs)
  apply auto
  done

lemma [simp]: "alls P (a@b) = (alls P a \<and> alls P b)"
  apply (induct_tac a)
  apply auto
  done

lemma "alls P (rev xs) = alls P xs"
  apply (induct_tac xs)
  apply auto
  done

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

lemma "a\<noteq>b \<Longrightarrow> 
  exs (\<lambda>x. x=a \<and> x=b) [a,b] \<noteq> (exs (\<lambda>x. x=a) [a,b] \<and> exs (\<lambda>x. x=b) [a,b])"
  apply auto
  done

lemma "exs P (map f xs) = exs (P o f) xs"
  apply (induct_tac xs)
  apply auto
  done

lemma [simp]: "exs P (a@b) = (exs P a \<or> exs P b)"
  apply (induct_tac a)
  apply auto
  done

lemma "exs P (rev xs) = exs P xs"
  apply (induct_tac xs)
  apply auto
  done

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

text {*
  Drücken Sie den Existenzquantor durch den Allquantor aus (auf der
  rechten Seite soll kein @{text exs} mehr vorkommen).
*}
lemma "exs P xs = (\<not>alls (\<lambda>x. \<not>P x) xs)"
  apply (induct_tac xs)
  apply auto
  done


text {*
  Definieren Sie eine Funktion @{term "is_in x xs"}, die testet ob
  @{term x} in der Liste @{term xs} vorkommt. *}
consts
  is_in :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
primrec
  "is_in y [] = False"
  "is_in y (x#xs) = (if x = y then True else is_in y xs)"

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 =  exs (\<lambda>x. a = x) xs"
  apply (induct_tac xs)
  apply auto
  done

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.
*}
consts
  nodups :: "'a list \<Rightarrow> bool"
  deldups :: "'a list \<Rightarrow> 'a list"

primrec
  "nodups [] = True"
  "nodups (x#xs) = (if is_in x xs then False else nodups xs)"

primrec
  "deldups [] = []"
  "deldups (x#xs) = (if is_in x xs then deldups xs else x#deldups xs)"


lemma "length (deldups xs) <= length xs"
  apply (induct_tac xs)
  apply auto
  done

lemma [simp]: "is_in a (deldups xs) = is_in a xs"
  apply (induct_tac xs)
  apply auto
  done

lemma "nodups (deldups xs)"
  apply (induct_tac xs)
  apply auto
  done
  
lemma "deldups (rev xs) = rev (deldups xs)"
  apply (induct_tac xs)
  apply auto
  oops

lemma 
  "a\<noteq>c \<Longrightarrow> deldups (rev [a,a,c,a]) \<noteq> rev (deldups [a,a,c,a])"
  apply auto
  done


(*<*)
end
(*>*)