|
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 FOLP; |
|
10 |
|
11 signature FOLP_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 FOLP_Lemmas : FOLP_LEMMAS = |
|
25 struct |
|
26 |
|
27 (*** Classical introduction rules for | and EX ***) |
|
28 |
|
29 val disjCI = prove_goal FOLP.thy |
|
30 "(!!x.x:~Q ==> f(x):P) ==> ?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 FOLP.thy |
|
38 "( !!u.u:~(EX x. P(x)) ==> f(u):P(a)) ==> ?p : 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 FOLP.thy |
|
45 "(!!u.u:ALL x. ~P(x) ==> f(u):P(a)) ==> ?p : 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 FOLP.thy "?p : ~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 FOLP.thy |
|
61 "[| p:P-->Q; !!x.x:~P ==> f(x):R; !!y.y:Q ==> g(y):R |] ==> ?p : 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 FOLP.thy "p:~~P ==> ?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 FOLP.thy [iff_def] |
|
77 "[| p:P<->Q; !!x y.[| x:P; y:Q |] ==> f(x,y):R; \ |
|
78 \ !!x y.[| x:~P; y:~Q |] ==> g(x,y):R |] ==> ?p : R" |
|
79 (fn prems => |
|
80 [ (resolve_tac [conjE] 1), |
|
81 (REPEAT (DEPTH_SOLVE_1 |
|
82 (etac impCE 1 ORELSE mp_tac 1 ORELSE ares_tac prems 1))) ]); |
|
83 |
|
84 |
|
85 (*Should be used as swap since ~P becomes redundant*) |
|
86 val swap = prove_goal FOLP.thy |
|
87 "p:~P ==> (!!x.x:~Q ==> f(x):P) ==> ?p : Q" |
|
88 (fn major::prems=> |
|
89 [ (resolve_tac [classical] 1), |
|
90 (rtac (major RS notE) 1), |
|
91 (REPEAT (ares_tac prems 1)) ]); |
|
92 |
|
93 end; |
|
94 |
|
95 open FOLP_Lemmas; |