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


text {*

\section{ Nat\"urliches Schlie{\ss}en }

In dieser Aufgabe geht es um den Kalk\"ul des nat\"urlichen Schlie{\ss}ens, 
mit dessen Hilfe einige Lemmas der Aussagen-Logik bewiesen werden sollen
(n\"achste Seite).

F\"ur die Beweise gelten die folgenden Spielregeln: 
\begin{itemize}
\item 
Es d\"urfen nur diese Lemmas verwendet werden: \\
(Anzeigen der Lemmas mittel \texttt{thm} \emph{lemma-Name})\\
@{text "notI:"}~@{thm notI[of A,no_vars]},\\
@{text "notE:"}~@{thm notE[of A B,no_vars]},\\
@{text "conjI:"}~@{thm conjI[of A B,no_vars]},\\ 
@{text "conjE:"}~@{thm conjE[of A B C,no_vars]},\\
@{text "disjI1:"}~@{thm disjI1[of A B,no_vars]},\\
@{text "disjI2:"}~@{thm disjI2[of A B,no_vars]},\\
@{text "disjE:"}~@{thm disjE[of A B C,no_vars]},\\
@{text "impI:"}~@{thm impI[of A B,no_vars]},\\
@{text "impE:"}~@{thm impE[of A B C,no_vars]},\\
@{text "mp:"}~@{thm mp[of A B,no_vars]}\\
@{text "iffI:"}~@{thm iffI[of A B,no_vars]}, \\
@{text "iffE:"}~@{thm iffE[of A B C,no_vars]}\\
@{text "classical:"}~@{thm classical[of A,no_vars]}
\item
Es d\"urfen nur die 
Methoden @{term rule}, @{term erule} und @{term assumption} verwendet werden. 
\end{itemize}

Beispiel:
*}
lemma imp_uncurry: "(P \<longrightarrow> (Q \<longrightarrow> R)) \<longrightarrow> P \<and> Q \<longrightarrow> R"
apply(rule impI)
apply(rule impI)
apply(erule conjE)
apply(erule impE)
 apply assumption
apply(erule mp)
apply assumption
done

text {* \eject *}

lemma I: "A \<longrightarrow> A" 
oops

lemma "A \<and> B \<longrightarrow> B \<and> A" 
oops

lemma "(A \<and> B) \<longrightarrow> (A \<or> B)"
oops

lemma "((A \<or> B) \<or> C) \<longrightarrow> A \<or> (B \<or> C)"
oops

lemma K: "A \<longrightarrow> B \<longrightarrow> A" 
oops

lemma "(A \<or> A) = (A \<and> A)" 
oops

lemma S: "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> B) \<longrightarrow> A \<longrightarrow> C" 
oops

lemma "(A \<longrightarrow> B) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> A \<longrightarrow> C" 
oops

lemma "\<not> \<not> A \<longrightarrow> A" 
oops

lemma "A \<longrightarrow> \<not> \<not> A" 
oops

lemma "(\<not> A \<longrightarrow> B) \<longrightarrow> (\<not> B \<longrightarrow> A)" 
oops

lemma "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A" 
oops

lemma "A \<or> \<not> A"
oops

lemma deMorgan1:"(\<not> (A \<or> B)) = (\<not> A \<and> \<not> B)"
oops

lemma deMorgan2:"(\<not> (A \<and> B)) = (\<not> A \<or> \<not> B)"
oops

text {* Anmerkung: Ist Ihnen bei den Beweisen der De Morgan-Regeln etwas aufgefallen? *} 



(*<*) end (*>*)