header {* Nat\"urliches Schlie{\ss}en *}

(*<*)
theory Aufgabe4 = Main:
(*>*)

text {* 
In diesem Aufgabenblatt geht es um den Kalk\"ul des nat\"urlichen Schie{\ss}ens, 
mit dessen Hilfe einige Lemmas der reinen Aussagen-Logik bewiesen werden sollen.



F\"ur die Beweise gelten die folgenden Spielregeln: 
\begin{itemize}
\item 
Es d\"urfen nur die Lemmas \\
@{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]}\\
und f\"ur die klassischen Beweise zus\"atzlich\\
@{text "classical:"}~@{thm classical[of A,no_vars]}\\
verwendet werden.

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



subsection {* Einige konstruktive Lemmas *}

lemma I: "A --> A" oops

lemma "A & B --> A" oops

lemma "A & B --> B & A" oops

lemma "(A & B) --> (A | B)" oops

lemma K: "A --> B --> A" oops

lemma "(A | B) = (B | A)" oops

lemma "(A | A) = (A & A)" oops

lemma S: "(A --> B --> C) --> (A --> B) --> A --> C" oops

lemma "(A --> B) --> (A' --> B') --> A & A' --> B & B'" oops

lemma "(A --> B) --> (B --> C) --> A --> C" oops


subsection  {* Einige klassische lemmas *}

lemma "~ ~ A --> A" oops

lemma "(~ A --> B) --> (~ B --> A)" oops

lemma "((A --> B) --> A) --> A" oops

lemma "~(A --> ~B) --> A" oops

lemma "(~ (A & B)) = (~A | ~B)" oops

lemma "(A = B) = (B = (A::bool))" oops

lemma "~ (A = (~ A))" oops

lemma "A | ~ A" oops

(*<*)
end
(*>*)