(*<*)
theory a5 = Main + l2:
(*>*)
text {*
\section*{Prädikatenlogik}

  Beweisen Sie die folgenden Formeln der Pr\"adikatenlogik mit den
  Regeln des nat\"urlichen Schlie{\ss}ens wie auf Blatt 4.

  Zus\"atzlich k\"onnen Sie die folgenden Regeln verwenden:\\
  @{text "exI:"}~@{thm exI[no_vars]}\\
  @{text "exE:"}~@{thm exE[no_vars]}\\
  @{text "allI:"}~@{thm allI[no_vars]}\\
  @{text "allE:"}~@{thm allE[no_vars]}\\
  \vspace*{0,5cm}
*}

lemma "\<exists>x. (P x \<longrightarrow> (\<forall>x. P x))"
oops

lemma "(\<exists>x. \<forall>y. P x y) \<longrightarrow> (\<forall>y. \<exists>x. P x y)" 
oops

lemma "(\<forall>x. P x \<longrightarrow> Q) = ((\<exists>x. P x) \<longrightarrow> Q)" 
oops


text {*
  \vspace*{0,5cm}

  Das folgende Lemma (Cantor's Theorem) besagt, dass
  keine Funktion vom Typ \mbox{@{typ "'a \<Rightarrow> 'a set"}} surjektiv ist.
  Um es etwas einfacher zu machen, stellen wir
  \mbox{@{typ "'a set"}} als @{typ "'a \<Rightarrow> bool"} dar. Sie dürfen für
  diese Aufgabe @{text "case_tac"} und das Lemma 
  \mbox{@{text "fun_cong:"} @{thm fun_cong [no_vars]}} zusammen mit
  @{text drule_tac} benutzen 
*}

lemma "\<forall>f :: 'a \<Rightarrow> 'a \<Rightarrow> bool. \<not>(\<forall>y. \<exists>x. f x = y)"
oops

text {*
  \newpage
  \section*{Merge-Sort}

  Implementieren Sie den Algorithmus Merge-Sort:
  Eine Liste wird sortiert, indem sie in der Mitte geteilt wird, die
  Teillisten sortiert werden, und danach zur geordneten Liste gemerged
  werden. 

  Definieren Sie dazu mit @{text recdef} zwei Funktion
*}
consts merge :: "nat list \<times> nat list \<Rightarrow> nat list"
consts msort :: "nat list \<Rightarrow> nat list"
text {*
  und zeigen Sie   
*}
theorem "sorted (msort xs)"
  oops

theorem "count (msort xs) x = count xs x"
  oops

text {*
  \note{Hinweise}
  \begin{itemize}
  \item Informationen zu @{text recdef} finden Sie im Tutorial,
  Abschnitt 3.5.
  \item Um die Liste in zwei ungefähr gleich große Hälften zu 
  teilen, können Sie die Funktionen @{text "x div 2"}, @{text "take n
  xs"} und @{text "drop n xs"} benutzen. Die Funktion @{text take} gibt
  die ersten @{text n} Elemente von @{text xs} zurück, die Funktion @{text drop} 
  liefert die Liste @{text xs} bis auf die ersten @{text n} Elemente.
  \item Sie können die folgenden Lemmas benutzen:\\
  @{text "linorder_not_le:"} @{thm linorder_not_le [no_vars]}\\
  @{text "order_less_le:"} @{thm order_less_le [no_vars]}\\
  @{text "div_if:"} @{thm div_if [no_vars]}\\
  @{text "min_def:"} @{thm min_def [no_vars]}
  \end{itemize}
*}

(*<*)
end 
(*>*)