author  paulson 
Fri, 17 Jul 1998 11:24:09 +0200  
changeset 5159  8fc4fb20d70f 
parent 4308  9abce31cc764 
child 7355  4c43090659ca 
permissions  rwrr 
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 FirstOrder 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) ==> PQ" 
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 