3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4 Copyright 1991 University of Cambridge
6 Tactics and lemmas for FOL.thy (classical First-Order Logic)
12 (*** Classical introduction rules for | and EX ***)
14 qed_goal "disjCI" FOL.thy
17 [ (resolve_tac [classical] 1),
18 (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
19 (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);
21 (*introduction rule involving only EX*)
22 qed_goal "ex_classical" FOL.thy
23 "( ~(EX x. P(x)) ==> P(a)) ==> EX x.P(x)"
25 [ (resolve_tac [classical] 1),
26 (eresolve_tac (prems RL [exI]) 1) ]);
28 (*version of above, simplifying ~EX to ALL~ *)
29 qed_goal "exCI" FOL.thy
30 "(ALL x. ~P(x) ==> P(a)) ==> EX x.P(x)"
32 [ (resolve_tac [ex_classical] 1),
33 (resolve_tac [notI RS allI RS prem] 1),
34 (eresolve_tac [notE] 1),
35 (eresolve_tac [exI] 1) ]);
37 qed_goal "excluded_middle" FOL.thy "~P | P"
38 (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
40 (*For disjunctive case analysis*)
41 fun excluded_middle_tac sP =
42 res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
44 (*** Special elimination rules *)
47 (*Classical implies (-->) elimination. *)
48 qed_goal "impCE" FOL.thy
49 "[| P-->Q; ~P ==> R; Q ==> R |] ==> R"
51 [ (resolve_tac [excluded_middle RS disjE] 1),
52 (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
54 (*Double negation law*)
55 qed_goal "notnotD" FOL.thy "~~P ==> P"
57 [ (resolve_tac [classical] 1), (eresolve_tac [major RS notE] 1) ]);
60 (*** Tactics for implication and contradiction ***)
62 (*Classical <-> elimination. Proof substitutes P=Q in
63 ~P ==> ~Q and P ==> Q *)
64 qed_goalw "iffCE" FOL.thy [iff_def]
65 "[| P<->Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R"
67 [ (resolve_tac [conjE] 1),
68 (REPEAT (DEPTH_SOLVE_1
69 (etac impCE 1 ORELSE mp_tac 1 ORELSE ares_tac prems 1))) ]);