theory ex2 imports Main begin lemma one: "(P \ (Q \ R)) \ ((P \ Q) \ (P \ R))" apply (rule impI) apply (rule impI) apply (rule impI) apply (erule impE) apply assumption apply (erule impE) apply assumption apply (erule impE) by assumption+ lemma two: "\\P \ P" apply (rule impI) apply (rule ccontr) apply (rule notE) apply assumption apply assumption done lemma three: "(P \ Q \ R) \ ((P \ Q) \ (P \ R))" apply (rule impI) apply (rule conjI) apply (rule impI) apply (rule conjunct1) apply (rule mp) apply assumption apply assumption apply (rule impI) apply (rule conjunct2) apply (rule mp) apply assumption apply assumption done lemma four: "(\P \ Q) \ (\Q \ P)" apply (rule impI) apply (rule impI) apply (rule ccontr) apply (rule notE) apply assumption apply (rule mp) apply assumption apply assumption done lemma five: "P \ \P" apply (rule disjE) apply (rule excluded_middle) apply (rule disjI2) apply assumption apply (rule disjI1) apply assumption done end