(*<*)
theory Blatt6
imports Main Infinite_Set
begin
(*>*)

section {* Prädikatenlogik *}

text {*
  Zusätzlich zu den Regeln der Aussagenlogik kommen jetzt 
  die folgenden Regeln zum Einsatz:\\
@{text "exI:"}~@{thm exI[no_vars]},\\
@{text "exE:"}~@{thm exE[no_vars]},\\
@{text "allI:"}~@{thm allI[no_vars]},\\ 
@{text "allE:"}~@{thm allE[no_vars]}.\\

Zeigen Sie die folgenden prädikatenlogischen Aussagen: *}

lemma "(\<forall>x. (P x \<longrightarrow> Q x ) \<and> \<not> Q a ) \<longrightarrow> \<not> P a"
(*<*)sorry(*>*)

lemma "(\<exists>x. P x ) \<and> (\<forall>x. P x  \<longrightarrow> Q x) \<longrightarrow> (\<exists>x. Q x)"
(*<*)sorry(*>*)

lemma "\<not>(\<forall>x. P x ) \<Longrightarrow> (\<exists>x. \<not> P x )"
(*<*)sorry(*>*)

lemma drinkers_principle: "\<exists>x. D x  \<longrightarrow> (\<forall>y. D y)"
(*<*)sorry(*>*)


section {* Knobelaufgabe: Rich Grandfather *}

text {* 
Beweisen Sie die folgende in klassischer Pr"adikatenlogik
g"ultige Formel zun"achst informell mit Papier und Bleistift.
Verwenden Sie im Beweis Fallunterscheidung oder Widerspruch..

  \begin{quote}{\it  Wenn jeder Arme einen reichen Vater hat,\\
 dann gibt es einen Reichen mit einem reichen Grossvater.}\end{quote}
*}

theorem rich_grandfather:
  "\<forall>x. \<not> rich x \<longrightarrow> rich (father x) \<Longrightarrow> 
  \<exists>x. rich (father (father x)) \<and> rich x" 
(*<*)sorry(*>*)
  


section {* Mengen, Abbildungen und anderes *}

text {* 
  \emph{Ab hier und auch in Zukunft dürfen alle Methoden und Lemmas
  verwendet werden.}
*}

text {* 
  Im folgenden Lemma ist außerdem das Auswahlprinzip nützlich:\\
  @{text "choice:"}~@{thm choice[no_vars]}

  Weiterhin muss die Theorie @{text "Infinite_Set"} importiert werden,
  in der die Notation @{term "\<exists>\<^sub>\<infinity> x. P x"} (in ASCII: @{text "INFM x. P x"})
  definiert wird.
*}

lemma finite_range:
  fixes f :: "nat \<Rightarrow> 'a"
  assumes fin: "finite (range f)"
  shows "\<exists>x. \<exists>\<^sub>\<infinity>i. f i = x"
(*<*)sorry(*>*)


(*<*)
end
(*>*)