header {* Automated Reasoning, Exercise Sheet 3 *} theory ex3 imports Main begin text {* Prove the following lemmas in Isabelle *} text {* The following tautology is known as "modus tollens". According to Wikipedia, this is Latin for "the way that denies by denying" *} lemma one : "(P \ Q) \ \ Q \ \ P" oops text {* This lemma can be either be proved directly, or can be proved more quickly by using 'cut_tac' with the lemma above *} lemma two : "\ (P \ Q) \ \ P" oops text {* The following lemma is the symmetric version of 'two'. We will use both in the final lemma below. *} lemma three : "\ (P \ Q) \ \ Q" oops text {* The following lemma can now be proved by using the lemmas 'two' and 'three'. *} lemma four : "\ (P \ Q) \ (\ P \ \ Q)" oops end