(* Original Author of Riddle: Tjark Weber Updates and additions by Jacques Fleuriot *) theory sol imports Main begin (* Note that most of these can be proved in more than one way *) lemma "(P \(Q\R))\((P\Q)\(P\R))" proof (rule impI)+ assume "P" "P \ Q \ R" then have qr: "Q \ R" by fast assume "P" "P \ Q" then have "Q" by blast then show "R" using qr by blast qed lemma "(\x. P x \ Q)\(\x. P x\Q)" proof assume "\x. P x \ Q" then have "P a \ Q" .. then show "\x. P x\Q" .. qed lemma assumes ex: "\(\x. P x)" shows all: "\x. \P x" proof (safe) fix x assume "P x" then have "\x. P x" .. then show False using ex by simp qed (* A proof showing the use of a raw proof block. More elegant proofs are possible. *) lemma assumes n_all: "\(\x. P x)" shows "\x. \P x" proof (rule ccontr) assume n_ex: "\x. \ P x" have "\x. P x" proof - {fix x have "P x" proof (rule ccontr) assume "\ P x" then have "\x. \ P x" .. then show False using n_ex by simp qed} then show ?thesis .. qed then show False using n_all by simp qed (* Shorter proof of same theorem as above *) lemma assumes n_all: "\(\x. P x)" shows "\x. \P x" proof (rule ccontr) assume n_ex: "\x. \ P x" {fix x have "P x" proof (rule ccontr) assume "\ P x" then have "\x. \ P x" .. then show False using n_ex by simp qed} then have "\x. P x" .. then show False using n_all by simp qed (* A possible proof, without named assumptions and goals. Other proofs are possible *) lemma "(R\P)\(((\R \ P)\(Q\S))\(Q\S))" proof (rule impI)+ assume "R \ P" "Q" "\ R \ P \ Q \ S" show "S" proof (cases) assume "R" then have "P" using \R \ P\ by blast then have "\R \ P" .. then have "Q \ S" using \\ R \ P \ Q \ S\ by blast then show "S" using \Q\ by simp next assume notr: "\R" then have "\R \ P" .. then have "Q \ S" using \\ R \ P \ Q \ S\ by blast then show "S" using \Q\ by simp qed qed (* Another proof of the above, without explicit use of cases *) lemma "(R \ P) \ (((\R \ P) \ (Q \ S)) \ (Q \ S))" proof (rule impI, rule impI) assume a: "R \ P" "\ R \ P \ Q \ S" { assume R hence P using a(1) by (rule_tac mp) hence "\ R \ P" by (rule disjI2) } moreover { assume "\R" hence "\ R \ P" by (rule disjI1) } ultimately have "\ R \ P" by (rule_tac disjE, rule_tac excluded_middle) from this a(2) show "Q \ S" by (rule_tac mp) qed text {* A Riddle: Rich Grandfather *} text {* First prove the following formula, which is valid in classical predicate logic, informally with pen and paper. Use case distinctions and/or proof by contradiction. "If every poor man has a rich father, then there is a rich man who has a rich grandfather" *} text {* Proof (1) We first show: "\x. rich x". Proof by contradiction. Assume "\ (\x. rich x)" Then "\x. \ rich x" We consider an arbitrary "y" with "\ rich y" Then "rich (father y)" (2) Now we show the theorem. Proof by cases. Case 1: "rich (father (father x))" We are done. Case 2: "\ rich (father (father x))" Then "rich (father (father (father x))) Also "rich (father x)" because otherwise "rich (father (father x))" qed *} text {* Now prove the formula in Isabelle using a sequence of rule applications (i.e.\ only using the methods rule, erule and assumption). *} theorem "\x. \ rich x \ rich (father x) \ \x. rich (father (father x)) \ rich x" apply (rule classical) apply (rule exI) apply (rule conjI) apply (rule classical) apply (rule allE) apply assumption apply (erule impE) apply assumption apply (erule notE) apply (rule exI) apply (rule conjI) apply assumption apply (rule classical) apply (erule allE) apply (erule notE) apply (erule impE) apply assumption apply assumption apply (rule classical) apply (rule allE) apply assumption apply (erule impE) apply assumption apply (erule notE) apply (rule exI) apply (rule conjI) apply assumption apply (rule classical) apply (erule allE) apply (erule notE) apply (erule impE) apply assumption apply assumption done text{* An alternative proof of the above that does not rely on meta variables and uses additional tactics/methods such as drule and cut_tac .Note the use of rule exCI too. Note also that the order in which the subgoals are tackled are dictated by Isabelle but there are ways of doing the proof in a way closer to the informal one e.g. using "prefer" to change the order of the goals (although this makes the proof potentially more "brittle" to changes in future versions of Isabelle *} theorem "\x. \ rich x \ rich (father x) \ \x. rich (father (father x)) \ rich x" apply (subgoal_tac "\x. rich x") apply (erule exE) (* Tackling (2) first *) apply (cut_tac P="rich (father(father x))" in excluded_middle) apply (erule disjE) (* Case 2 *) apply (subgoal_tac "rich(father x)") apply (drule_tac x="father(father x)" in spec) apply (drule mp, assumption) apply (rule_tac x="father x" in exI) apply (rule conjI) apply assumption apply assumption apply (rule ccontr) apply (drule_tac x="father x" in spec) apply (drule mp, assumption) apply (erule notE, assumption) (* Case 1*) apply (rule_tac x=x in exI) apply (rule conjI) apply assumption apply assumption (* Tackling (1) now *) apply (rule_tac a="father x" in exCI) apply (drule_tac x=x in spec) apply (drule_tac x=x in spec) apply (drule mp, assumption) apply assumption done text {* Here is a proof in Isar that resembles the informal reasoning above: *} theorem rich_grandfather: "\x. \ rich x \ rich (father x) \ \x. rich x \ rich (father (father x))" proof - assume a: "\x. \ rich x \ rich (father x)" have "\x. rich x" proof (rule classical) fix y assume "\ (\x. rich x)" then have "\x. \ rich x" by simp then have "\ rich y" by simp with a have "rich (father y)" by simp then show ?thesis by rule qed then obtain x where x: "rich x" by auto show ?thesis proof cases assume "rich (father (father x))" with x show ?thesis by auto next assume b: "\ rich (father (father x))" with a have "rich (father (father (father x)))" by simp moreover have "rich (father x)" proof (rule classical) assume "\ rich (father x)" with a have "rich (father (father x))" by simp with b show ?thesis by contradiction qed ultimately show ?thesis by auto qed qed text {* An slightly modified proof of the above, with a named assumption right from the beginning: *} theorem rich_grandfather2: assumes a: "\x. \ rich x \ rich (father x)" shows "\x. rich x \ rich (father (father x))" proof - have "\x. rich x" proof (rule classical) fix y assume "\ (\x. rich x)" then have "\x. \ rich x" by simp then have "\ rich y" by simp with a have "rich (father y)" by simp then show ?thesis by rule qed then obtain x where x: "rich x" by auto show ?thesis proof cases assume "rich (father (father x))" with x show ?thesis by auto next assume b: "\ rich (father (father x))" with a have "rich (father (father (father x)))" by simp moreover have "rich (father x)" proof (rule classical) assume "\ rich (father x)" with a have "rich (father (father x))" by simp with b show ?thesis by contradiction qed ultimately show ?thesis by auto qed qed end