1 (* Title: FOL/fol.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1991 University of Cambridge |
|
5 |
|
6 Tactics and lemmas for fol.thy (classical First-Order Logic) |
|
7 *) |
|
8 |
|
9 open FOL; |
|
10 |
|
11 signature FOL_LEMMAS = |
|
12 sig |
|
13 val disjCI : thm |
|
14 val excluded_middle : thm |
|
15 val exCI : thm |
|
16 val ex_classical : thm |
|
17 val iffCE : thm |
|
18 val impCE : thm |
|
19 val notnotD : thm |
|
20 val swap : thm |
|
21 end; |
|
22 |
|
23 |
|
24 structure FOL_Lemmas : FOL_LEMMAS = |
|
25 struct |
|
26 |
|
27 (*** Classical introduction rules for | and EX ***) |
|
28 |
|
29 val disjCI = prove_goal FOL.thy |
|
30 "(~Q ==> P) ==> P|Q" |
|
31 (fn prems=> |
|
32 [ (resolve_tac [classical] 1), |
|
33 (REPEAT (ares_tac (prems@[disjI1,notI]) 1)), |
|
34 (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]); |
|
35 |
|
36 (*introduction rule involving only EX*) |
|
37 val ex_classical = prove_goal FOL.thy |
|
38 "( ~(EX x. P(x)) ==> P(a)) ==> EX x.P(x)" |
|
39 (fn prems=> |
|
40 [ (resolve_tac [classical] 1), |
|
41 (eresolve_tac (prems RL [exI]) 1) ]); |
|
42 |
|
43 (*version of above, simplifying ~EX to ALL~ *) |
|
44 val exCI = prove_goal FOL.thy |
|
45 "(ALL x. ~P(x) ==> P(a)) ==> EX x.P(x)" |
|
46 (fn [prem]=> |
|
47 [ (resolve_tac [ex_classical] 1), |
|
48 (resolve_tac [notI RS allI RS prem] 1), |
|
49 (eresolve_tac [notE] 1), |
|
50 (eresolve_tac [exI] 1) ]); |
|
51 |
|
52 val excluded_middle = prove_goal FOL.thy "~P | P" |
|
53 (fn _=> [ rtac disjCI 1, assume_tac 1 ]); |
|
54 |
|
55 |
|
56 (*** Special elimination rules *) |
|
57 |
|
58 |
|
59 (*Classical implies (-->) elimination. *) |
|
60 val impCE = prove_goal FOL.thy |
|
61 "[| P-->Q; ~P ==> R; Q ==> R |] ==> R" |
|
62 (fn major::prems=> |
|
63 [ (resolve_tac [excluded_middle RS disjE] 1), |
|
64 (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]); |
|
65 |
|
66 (*Double negation law*) |
|
67 val notnotD = prove_goal FOL.thy "~~P ==> P" |
|
68 (fn [major]=> |
|
69 [ (resolve_tac [classical] 1), (eresolve_tac [major RS notE] 1) ]); |
|
70 |
|
71 |
|
72 (*** Tactics for implication and contradiction ***) |
|
73 |
|
74 (*Classical <-> elimination. Proof substitutes P=Q in |
|
75 ~P ==> ~Q and P ==> Q *) |
|
76 val iffCE = prove_goalw FOL.thy [iff_def] |
|
77 "[| P<->Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R" |
|
78 (fn prems => |
|
79 [ (resolve_tac [conjE] 1), |
|
80 (REPEAT (DEPTH_SOLVE_1 |
|
81 (etac impCE 1 ORELSE mp_tac 1 ORELSE ares_tac prems 1))) ]); |
|
82 |
|
83 |
|
84 (*Should be used as swap since ~P becomes redundant*) |
|
85 val swap = prove_goal FOL.thy |
|
86 "~P ==> (~Q ==> P) ==> Q" |
|
87 (fn major::prems=> |
|
88 [ (resolve_tac [classical] 1), |
|
89 (rtac (major RS notE) 1), |
|
90 (REPEAT (ares_tac prems 1)) ]); |
|
91 |
|
92 end; |
|
93 |
|
94 open FOL_Lemmas; |
|