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 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 ***)


28 


29 
val disjCI = prove_goal FOLP.thy


30 
"(!!x.x:~Q ==> f(x):P) ==> ?p : PQ"


31 
(fn prems=>


32 
[ (resolve_tac [classical] 1),


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


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


35 


36 
(*introduction rule involving only EX*)


37 
val ex_classical = prove_goal FOLP.thy


38 
"( !!u.u:~(EX x. P(x)) ==> f(u):P(a)) ==> ?p : EX x.P(x)"


39 
(fn prems=>


40 
[ (resolve_tac [classical] 1),


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


42 


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


44 
val exCI = prove_goal FOLP.thy


45 
"(!!u.u:ALL x. ~P(x) ==> f(u):P(a)) ==> ?p : EX x.P(x)"


46 
(fn [prem]=>


47 
[ (resolve_tac [ex_classical] 1),


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


49 
(eresolve_tac [notE] 1),


50 
(eresolve_tac [exI] 1) ]);


51 


52 
val excluded_middle = prove_goal FOLP.thy "?p : ~P  P"


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


54 


55 


56 
(*** Special elimination rules *)


57 


58 


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


60 
val impCE = prove_goal FOLP.thy


61 
"[ p:P>Q; !!x.x:~P ==> f(x):R; !!y.y:Q ==> g(y):R ] ==> ?p : R"


62 
(fn major::prems=>


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


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


65 


66 
(*Double negation law*)


67 
val notnotD = prove_goal FOLP.thy "p:~~P ==> ?p : P"


68 
(fn [major]=>


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


70 


71 


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


73 


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


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


76 
val iffCE = prove_goalw FOLP.thy [iff_def]


77 
"[ 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"


79 
(fn prems =>


80 
[ (resolve_tac [conjE] 1),


81 
(REPEAT (DEPTH_SOLVE_1


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


83 


84 


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


86 
val swap = prove_goal FOLP.thy


87 
"p:~P ==> (!!x.x:~Q ==> f(x):P) ==> ?p : Q"


88 
(fn major::prems=>


89 
[ (resolve_tac [classical] 1),


90 
(rtac (major RS notE) 1),


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


92 


93 
end;


94 


95 
open FOLP_Lemmas;
