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

section {* Aussagenlogik *}

text {*
F\"ur die Beweise auf diesem Übungsblatt gelten die folgenden Spielregeln: 
\begin{itemize}
\item 
Es d\"urfen nur diese Regeln verwendet werden: \\
@{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 "ccontr:"}~@{thm ccontr[of A,no_vars]}
\item
Es d\"urfen nur die 
Methoden @{term rule}, @{term erule} und @{term assumption} verwendet werden. 
\end{itemize}


Finden Sie Beweise im apply-Stil für die folgenden Aussagen:
*}

lemma "(A & B) & C --> A & (B & C)" (*<*)sorry(*>*)

lemma "(A | B) | C --> A | (B | C)"  (*<*)sorry(*>*)

lemma "(A --> B) --> (~B --> ~A)" (*<*)sorry(*>*)

text {*
  \emph{Hinweis:} Die Aufgaben kamen schonmal als Papier-Beweise auf Blatt 2.
*}
section {* Strukturierte Beweise *}

text {*
  Finden Sie strukturierte Isar-Beweise für die folgenden Aussagen:
*}

lemma "(A --> B --> C) --> (A --> B) --> (A --> C)" (*<*)sorry(*>*)

lemma "A & (B | C) <-> (A & B) | (A & C)" (*<*)sorry(*>*)


section {* Klassische Logik *}

text {* 
  Beweise, die die nicht-intuitionistische Regel 
  @{text "ccontr"} (classical contradiction) benötigen sind meist schwieriger.
  Zeigen Sie:
*}

lemma "A | ~ A" (*<*)sorry(*>*)
(*<*)
end
(*>*)