author | wenzelm |
Mon, 16 Nov 1998 11:33:42 +0100 | |
changeset 5896 | 4a75d89e2818 |
parent 5159 | 8fc4fb20d70f |
child 7355 | 4c43090659ca |
permissions | -rw-r--r-- |
1459 | 1 |
(* Title: FOL/FOL.ML |
0 | 2 |
ID: $Id$ |
1459 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1991 University of Cambridge |
5 |
||
1280 | 6 |
Tactics and lemmas for FOL.thy (classical First-Order Logic) |
0 | 7 |
*) |
8 |
||
9 |
open FOL; |
|
10 |
||
11 |
||
2576
390c9fb786b5
Declaration of ccontr (classical contradiction) for HOL compatibility
paulson
parents:
2469
diff
changeset
|
12 |
val ccontr = FalseE RS classical; |
390c9fb786b5
Declaration of ccontr (classical contradiction) for HOL compatibility
paulson
parents:
2469
diff
changeset
|
13 |
|
0 | 14 |
(*** Classical introduction rules for | and EX ***) |
15 |
||
779 | 16 |
qed_goal "disjCI" FOL.thy |
0 | 17 |
"(~Q ==> P) ==> P|Q" |
18 |
(fn prems=> |
|
1459 | 19 |
[ (rtac classical 1), |
0 | 20 |
(REPEAT (ares_tac (prems@[disjI1,notI]) 1)), |
21 |
(REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]); |
|
22 |
||
23 |
(*introduction rule involving only EX*) |
|
779 | 24 |
qed_goal "ex_classical" FOL.thy |
3835 | 25 |
"( ~(EX x. P(x)) ==> P(a)) ==> EX x. P(x)" |
0 | 26 |
(fn prems=> |
1459 | 27 |
[ (rtac classical 1), |
0 | 28 |
(eresolve_tac (prems RL [exI]) 1) ]); |
29 |
||
30 |
(*version of above, simplifying ~EX to ALL~ *) |
|
779 | 31 |
qed_goal "exCI" FOL.thy |
3835 | 32 |
"(ALL x. ~P(x) ==> P(a)) ==> EX x. P(x)" |
0 | 33 |
(fn [prem]=> |
1459 | 34 |
[ (rtac ex_classical 1), |
0 | 35 |
(resolve_tac [notI RS allI RS prem] 1), |
1459 | 36 |
(etac notE 1), |
37 |
(etac exI 1) ]); |
|
0 | 38 |
|
779 | 39 |
qed_goal "excluded_middle" FOL.thy "~P | P" |
0 | 40 |
(fn _=> [ rtac disjCI 1, assume_tac 1 ]); |
41 |
||
440 | 42 |
(*For disjunctive case analysis*) |
43 |
fun excluded_middle_tac sP = |
|
44 |
res_inst_tac [("Q",sP)] (excluded_middle RS disjE); |
|
0 | 45 |
|
5159 | 46 |
qed_goal "case_split_thm" FOL.thy "[| P ==> Q; ~P ==> Q |] ==> Q" |
47 |
(fn [p1,p2] => [rtac (excluded_middle RS disjE) 1, |
|
48 |
etac p2 1, etac p1 1]); |
|
49 |
||
50 |
(*HOL's more natural case analysis tactic*) |
|
51 |
fun case_tac a = res_inst_tac [("P",a)] case_split_thm; |
|
52 |
||
53 |
||
0 | 54 |
(*** Special elimination rules *) |
55 |
||
56 |
||
57 |
(*Classical implies (-->) elimination. *) |
|
779 | 58 |
qed_goal "impCE" FOL.thy |
0 | 59 |
"[| P-->Q; ~P ==> R; Q ==> R |] ==> R" |
60 |
(fn major::prems=> |
|
61 |
[ (resolve_tac [excluded_middle RS disjE] 1), |
|
62 |
(DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]); |
|
63 |
||
4308 | 64 |
(*This version of --> elimination works on Q before P. It works best for |
65 |
those cases in which P holds "almost everywhere". Can't install as |
|
66 |
default: would break old proofs.*) |
|
67 |
qed_goal "impCE'" thy |
|
68 |
"[| P-->Q; Q ==> R; ~P ==> R |] ==> R" |
|
69 |
(fn major::prems=> |
|
70 |
[ (resolve_tac [excluded_middle RS disjE] 1), |
|
71 |
(DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]); |
|
72 |
||
0 | 73 |
(*Double negation law*) |
779 | 74 |
qed_goal "notnotD" FOL.thy "~~P ==> P" |
0 | 75 |
(fn [major]=> |
1459 | 76 |
[ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]); |
0 | 77 |
|
4186 | 78 |
qed_goal "contrapos2" FOL.thy "[| Q; ~ P ==> ~ Q |] ==> P" (fn [p1,p2] => [ |
79 |
rtac classical 1, |
|
80 |
dtac p2 1, |
|
81 |
etac notE 1, |
|
82 |
rtac p1 1]); |
|
0 | 83 |
|
84 |
(*** Tactics for implication and contradiction ***) |
|
85 |
||
86 |
(*Classical <-> elimination. Proof substitutes P=Q in |
|
87 |
~P ==> ~Q and P ==> Q *) |
|
779 | 88 |
qed_goalw "iffCE" FOL.thy [iff_def] |
0 | 89 |
"[| P<->Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R" |
90 |
(fn prems => |
|
1459 | 91 |
[ (rtac conjE 1), |
0 | 92 |
(REPEAT (DEPTH_SOLVE_1 |
1459 | 93 |
(etac impCE 1 ORELSE mp_tac 1 ORELSE ares_tac prems 1))) ]); |
2469 | 94 |