theory Predicate_Logic_Exercises imports Main begin (*use rule, erule, and so on combined with basic elimination and introduction rules. do not use any automation...*) lemma shows "(\x. (P \ Q x)) \ (P \ (\x. Q x))" sorry (*prove contrapos_np first, then use it to prove the next lemma below:*) lemma contrapos_np: assumes "\ Q" and "\ P \ Q" shows "P" sorry lemma shows "\ (\x. P x \ Q x) \ (\x. \ P x \ \ Q x)" sorry lemma shows "\P. \Q. \x. ((P x \ Q x) \ P x) \ P x" sorry lemma assumes "Q \ (\x. S x)" and "S False \ Q" and "S True \ Q" shows "Q \ (\x. S x)" sorry lemma shows "(\P Q. \!x. P x \ Q x) \ False" sorry lemma shows "\P. \x. \ P x" sorry lemma shows "(\x. P x \ Q x) \ (\x. \ P x \ Q x)" sorry end