1280

1 
(* Title: FOL/FOL.ML

0

2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


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 


12 
(*** Classical introduction rules for  and EX ***)


13 

779

14 
qed_goal "disjCI" FOL.thy

0

15 
"(~Q ==> P) ==> PQ"


16 
(fn prems=>


17 
[ (resolve_tac [classical] 1),


18 
(REPEAT (ares_tac (prems@[disjI1,notI]) 1)),


19 
(REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);


20 


21 
(*introduction rule involving only EX*)

779

22 
qed_goal "ex_classical" FOL.thy

0

23 
"( ~(EX x. P(x)) ==> P(a)) ==> EX x.P(x)"


24 
(fn prems=>


25 
[ (resolve_tac [classical] 1),


26 
(eresolve_tac (prems RL [exI]) 1) ]);


27 


28 
(*version of above, simplifying ~EX to ALL~ *)

779

29 
qed_goal "exCI" FOL.thy

0

30 
"(ALL x. ~P(x) ==> P(a)) ==> EX x.P(x)"


31 
(fn [prem]=>


32 
[ (resolve_tac [ex_classical] 1),


33 
(resolve_tac [notI RS allI RS prem] 1),


34 
(eresolve_tac [notE] 1),


35 
(eresolve_tac [exI] 1) ]);


36 

779

37 
qed_goal "excluded_middle" FOL.thy "~P  P"

0

38 
(fn _=> [ rtac disjCI 1, assume_tac 1 ]);


39 

440

40 
(*For disjunctive case analysis*)


41 
fun excluded_middle_tac sP =


42 
res_inst_tac [("Q",sP)] (excluded_middle RS disjE);

0

43 


44 
(*** Special elimination rules *)


45 


46 


47 
(*Classical implies (>) elimination. *)

779

48 
qed_goal "impCE" FOL.thy

0

49 
"[ P>Q; ~P ==> R; Q ==> R ] ==> R"


50 
(fn major::prems=>


51 
[ (resolve_tac [excluded_middle RS disjE] 1),


52 
(DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);


53 


54 
(*Double negation law*)

779

55 
qed_goal "notnotD" FOL.thy "~~P ==> P"

0

56 
(fn [major]=>


57 
[ (resolve_tac [classical] 1), (eresolve_tac [major RS notE] 1) ]);


58 


59 


60 
(*** Tactics for implication and contradiction ***)


61 


62 
(*Classical <> elimination. Proof substitutes P=Q in


63 
~P ==> ~Q and P ==> Q *)

779

64 
qed_goalw "iffCE" FOL.thy [iff_def]

0

65 
"[ P<>Q; [ P; Q ] ==> R; [ ~P; ~Q ] ==> R ] ==> R"


66 
(fn prems =>


67 
[ (resolve_tac [conjE] 1),


68 
(REPEAT (DEPTH_SOLVE_1


69 
(etac impCE 1 ORELSE mp_tac 1 ORELSE ares_tac prems 1))) ]);
