(*<*)theory Quantification imports Main begin(*>*)



text {*

\section*{Pr\"adikatenlogik}

Es geht wiederum um Beweise mit den Regeln des Kalk\"uls des nat\"urlichen
Schlie{\ss}ens. Zus\"atzlich zu den Regeln von Blatt~1 k\"onnen Sie nun auch
folgende Regeln verwenden:

@{text "allI:"}~@{thm allI[no_vars]}\\
@{text "allE:"}~@{thm allE[no_vars]}\\
@{text "exI:"}~@{thm exI[no_vars]}\\
@{text "exE:"}~@{thm exE[no_vars]}

Es d\"urfen wiederum nur die 
Methoden @{term rule}, @{term erule} und @{term assumption} verwendet werden. 

Achten Sie darauf, f\"ur @{text exI} und @{text allE} nur @{text rule_tac} 
bzw. @{text erule_tac} mit gleichzeitiger Instantiierung der Variablen zu verwenden, 
ansonsten erhalten sie beliebige Variablen, die den Beweis erschweren k\"onnen!

Beispiel:
*}
lemma "\<forall>x. P x \<longrightarrow> (\<exists>x. P x)"
apply(rule allI)
apply(rule impI)
apply(rule_tac x="x" in exI)
apply assumption
done

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

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

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

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

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

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

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

(*<*) end (*>*)