(*<*)
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 "(ALL x. (P x --> Q x ) & ~ Q a ) --> ~ P a"
(*<*)sorry(*>*)

lemma "(EX x. P x ) & (ALL x. P x  --> Q x) --> (EX x. Q x)"
(*<*)sorry(*>*)

lemma "~(ALL x. P x ) ==> (EX x. ~ P x )"
(*<*)sorry(*>*)

lemma drinkers_principle: "EX x. D x  --> (ALL 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:
  "ALL x. ~ rich x --> rich (father x) ==> 
  EX x. rich (father (father x)) & 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 => 'a"
  assumes fin: "finite (range f)"
  shows "EX x. INFM i. f i = x"
(*<*)sorry(*>*)


(*<*)
end
(*>*)