(* CSMR WS10/11 - Sheet 2 *) use "sheet1.ML"; (* *) (* Exercise 1 -------------------- *) (* *) (* 1.1 *) (* Solution thanks to ideas by Maria Vassileva *) goal thy "P \\ \\P"; br classical 1; br disjI2 1; by (rewrite_goals_tac [not_def]); br impI 1; br mp 1; ba 1; br disjI1 1; ba 1; qed "ex1_1"; qed "excl_middle"; (* 1.2 *) (* The problem is that to apply peirce_aux we would need to rewrite the *) (* first occurrence of ~P only. The solution is to prove the *) (* following auxiliary statement *) goal thy "(A \\ (A \\ False)) \\ ((A \\ B) \\ A) \\ A"; by (fold_goals_tac [not_def]); br peirce_aux 1; (* From Sheet 1 *) qed "ex1_2_aux"; goal thy "P \\ \\P \\ ((\\P \\ P) \\ P)"; by (rewrite_goals_tac [not_def]); br ex1_2_aux 1; qed "ex1_2"; (* *) (* Exercise 2 -------------------- *) (* *) (* Peirce's law: *) goal thy "((A \\ B) \\ A) \\ A"; br mp 1; br peirce_aux 1; br excl_middle 1; qed "ex2"; (*Derived Rules*) (*let's see what the type of goal is*) goal; (*The following is not very useful:*) goal thy "P&Q \\ Q&P"; (*Note that the problem could be avoided here by using Goal, but in other situations that would not work.*) (*Exception due to non-matching binding attempt val [prem1,prem2] = goal thy "P&Q \\ Q&P"; *) (*deriving commutativity of &*) val [prem] = goal thy "P&Q \\ Q&P"; prem; br conjI 1; br conjunct2 1; br prem 1; br conjunct1 1; br prem 1; qed "conjComm"; (* *) (* Exercise 3 -------------------- *) (* *) val [prem1,prem2,prem3] = goal thy "[| P-->Q; P; Q ==> R |] ==> R"; br prem3 1; br mp 1; br prem1 1; br prem2 1; qed "impE"; (* *) (* Exercise 4 -------------------- *) (* *) (* 4.1 *) (* a "dual" to classical*) val [prem] = goal thy "(A \\ (A\\B))\\ (A\\ B)"; br impI 1; br mp 1; br prem 1; ba 1; ba 1; qed "ex4_1"; (* 4.2 *) val [prem] = goal thy "(A \\ (~A))\\ (~A)"; bw not_def; (*The above is an abbreviation for by (rewrite_goals_tac [not_def]) See 2.2.3 in the Isabelle reference manual*) br ex4_1 1; by (fold_goals_tac [not_def]); br prem 1; ba 1; qed "classical_dual"; (*Same using etac, but this will be introduced later*) (*I use Goal here since it saves typing*) (* 4.1' *) val [prem] = Goal "(A \\ (A\\B))\\ (A\\ B)"; br impI 1; br mp 1; be prem 1; ba 1; qed; (* 4.2' *) val [prem] = Goal "(A \\ (~A))\\ (~A)"; bw not_def; br ex4_1 1; by (fold_goals_tac [not_def]); be prem 1; qed; (* 4.2" *) (*Alternative*) val [prems] = Goal "(A \\ ~A) \\ ~A"; br notI 1; br notE 1; br prems 1; ba 1; ba 1; qed; (*Elimination tactic*) Goal "A & B \\ A"; br impI 1; by (etac conjunct1 1); qed; (* *) (* Exercise 5 -------------------- *) (* *) (* 5.1 *) Goal "A \\ (B \\ C) \\ (A \\ B) \\ C"; br impI 1; be conjE 1; be conjE 1; br conjI 1; br conjI 1; ba 1; ba 1; ba 1; qed "ex5_1"; (*For comparison, ex5_2 without using etac*) (*without conjE*) Goal "A \\ (B \\ C) \\ (A \\ B) \\ C"; br impI 1; br conjI 1; br conjI 1; br conjunct1 1; ba 1; br conjunct1 1; br conjunct2 1; ba 1; br conjunct2 1; br conjunct2 1; ba 1; qed; (*with conjE but without etac*) Goal "A \\ (B \\ C) \\ (A \\ B) \\ C"; br impI 1; br conjE 1; ba 1; by (rotate_tac 1 1); br conjE 1; ba 1; br conjI 1; br conjI 1; ba 1; ba 1; ba 1; qed; (* 5.2 *) Goal "(A \\ C) \\ (B \\ C) \\ (A \\ B) \\ C"; br impI 1; be conjE 1; be disjE 1; be disjE 1; br disjI1 1; br conjI 1; ba 1; ba 1; br disjI2 1; ba 1; br disjI2 1; ba 1; qed "ex5_2";