0

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 FirstOrder Logic)


7 
*)


8 


9 
open FOL;


10 


11 
signature FOL_LEMMAS =


12 
sig


13 
val disjCI : thm


14 
val excluded_middle : thm

440

15 
val excluded_middle_tac : string > int > tactic

0

16 
val exCI : thm


17 
val ex_classical : thm


18 
val iffCE : thm


19 
val impCE : thm


20 
val notnotD : thm


21 
val swap : thm


22 
end;


23 


24 


25 
structure FOL_Lemmas : FOL_LEMMAS =


26 
struct


27 


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


29 


30 
val disjCI = prove_goal FOL.thy


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


32 
(fn prems=>


33 
[ (resolve_tac [classical] 1),


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


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


36 


37 
(*introduction rule involving only EX*)


38 
val ex_classical = prove_goal FOL.thy


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


40 
(fn prems=>


41 
[ (resolve_tac [classical] 1),


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


43 


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


45 
val exCI = prove_goal FOL.thy


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


47 
(fn [prem]=>


48 
[ (resolve_tac [ex_classical] 1),


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


50 
(eresolve_tac [notE] 1),


51 
(eresolve_tac [exI] 1) ]);


52 


53 
val excluded_middle = prove_goal FOL.thy "~P  P"


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


55 

440

56 
(*For disjunctive case analysis*)


57 
fun excluded_middle_tac sP =


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

0

59 


60 
(*** Special elimination rules *)


61 


62 


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


64 
val impCE = prove_goal FOL.thy


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


66 
(fn major::prems=>


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


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


69 


70 
(*Double negation law*)


71 
val notnotD = prove_goal FOL.thy "~~P ==> P"


72 
(fn [major]=>


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


74 


75 


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


77 


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


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


80 
val iffCE = prove_goalw FOL.thy [iff_def]


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


82 
(fn prems =>


83 
[ (resolve_tac [conjE] 1),


84 
(REPEAT (DEPTH_SOLVE_1


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


86 


87 


88 
(*Should be used as swap since ~P becomes redundant*)


89 
val swap = prove_goal FOL.thy


90 
"~P ==> (~Q ==> P) ==> Q"


91 
(fn major::prems=>


92 
[ (resolve_tac [classical] 1),


93 
(rtac (major RS notE) 1),


94 
(REPEAT (ares_tac prems 1)) ]);


95 


96 
end;


97 


98 
open FOL_Lemmas;
