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