(* $Id: ex.thy,v 1.2 2004/11/23 15:14:35 webertj Exp$ *) header {* Propositional Logic *} (*<*) theory ex imports Main begin (*>*) text {* In this exercise, we will prove some lemmas of propositional logic with the aid of a calculus of natural deduction. For the proofs, you may only use \begin{itemize} \item the following 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]}\\ @{text "classical:"}~@{thm classical[of A,no_vars]} \item the proof methods @{term rule}, @{term erule} and @{term assumption}. \end{itemize} Prove: *} lemma I: "A \ A" (*<*) oops (*>*) lemma "A \ B \ B \ A" (*<*) oops (*>*) lemma "(A \ B) \ (A \ B)" (*<*) oops (*>*) lemma "((A \ B) \ C) \ A \ (B \ C)" (*<*) oops (*>*) lemma K: "A \ B \ A" (*<*) oops (*>*) lemma "(A \ A) = (A \ A)" (*<*) oops (*>*) lemma S: "(A \ B \ C) \ (A \ B) \ A \ C" (*<*) oops (*>*) lemma "(A \ B) \ (B \ C) \ A \ C" (*<*) oops (*>*) lemma "\ \ A \ A" (*<*) oops (*>*) lemma "A \ \ \ A" (*<*) oops (*>*) lemma "(\ A \ B) \ (\ B \ A)" (*<*) oops (*>*) lemma "((A \ B) \ A) \ A" (*<*) oops (*>*) lemma "A \ \ A" (*<*) oops (*>*) lemma "(\ (A \ B)) = (\ A \ \ B)" (*<*) oops (*>*) (*<*) end (*>*)