header {* My Logic *} theory My_Logic imports Main begin lemma "\P; P \ Q; P \ (Q \ R)\ \ R" apply (drule mp) apply assumption apply (drule mp) apply assumption apply (drule mp) apply assumption apply assumption done lemma "Q \ R \ P \ Q \ P \ R" apply (rule impI) apply (erule disjE) apply (rule disjI1) apply assumption apply (drule mp) apply assumption apply (rule disjI2) apply assumption done lemma "P \ Q \ \ Q \ \ P" apply (rule impI) apply (rule notI) apply (drule mp) apply assumption apply (erule notE) apply assumption done lemma "\ P \ \ Q \ Q \ P" apply (rule impI) apply (rule ccontr) apply (drule mp) apply assumption apply (erule notE) apply (erule notE) apply assumption done lemma peirce: "((P \ Q) \ P) \ P" apply (rule impI) apply (rule ccontr) apply (drule mp) apply (rule impI) apply (erule notE) apply assumption apply (erule notE) apply assumption done lemma "\x. P x \ \ (\x. \ P x)" apply (rule notI) apply (erule exE) apply (erule allE) apply (erule notE) apply assumption done lemma "\ (\x. \ P x) \ \x. P x" apply (rule allI) apply (rule ccontr) apply (drule notE) apply (rule exI) apply assumption apply assumption done (* exercises *) lemma "(P \ Q) \ R \ P \ (Q \ R)" apply (rule impI) apply (rule impI) apply (drule mp) apply (rule conjI) apply assumption apply assumption apply assumption done lemma "P \ (Q \ R) \ P \ Q \ R" apply (rule impI) apply (erule conjE) apply (drule mp) apply assumption apply (drule mp) apply assumption apply assumption done lemma "\x. \y. P x y \ \y. \x. P x y" apply (erule exE) apply (rule allI) apply (erule allE) apply (rule exI) apply assumption done lemma "\y. \x. P x y \ \x. \y. P x y" nitpick oops end