17480

1 
(* Title: FOLP/FOLP.ML


2 
ID: $Id$


3 
Author: Martin D Coen, Cambridge University Computer Laboratory


4 
Copyright 1991 University of Cambridge


5 
*)


6 


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


8 


9 
val prems= goal (the_context ())


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


11 
by (rtac classical 1);


12 
by (REPEAT (ares_tac (prems@[disjI1,notI]) 1));


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


14 
qed "disjCI";


15 


16 
(*introduction rule involving only EX*)


17 
val prems= goal (the_context ())


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


19 
by (rtac classical 1);


20 
by (eresolve_tac (prems RL [exI]) 1) ;


21 
qed "ex_classical";


22 


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


24 
val [prem]= goal (the_context ())


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


26 
by (rtac ex_classical 1);


27 
by (resolve_tac [notI RS allI RS prem] 1);


28 
by (etac notE 1);


29 
by (etac exI 1) ;


30 
qed "exCI";


31 


32 
val excluded_middle = prove_goal (the_context ()) "?p : ~P  P"


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


34 


35 


36 
(*** Special elimination rules *)


37 


38 


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


40 
val major::prems= goal (the_context ())


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


42 
by (resolve_tac [excluded_middle RS disjE] 1);


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


44 
qed "impCE";


45 


46 
(*Double negation law*)


47 
Goal "p:~~P ==> ?p : P";


48 
by (rtac classical 1);


49 
by (etac notE 1);


50 
by (assume_tac 1);


51 
qed "notnotD";


52 


53 


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


55 


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


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


58 
val prems = goalw (the_context ()) [iff_def]


59 
"[ p:P<>Q; !!x y.[ x:P; y:Q ] ==> f(x,y):R; \


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


61 
by (rtac conjE 1);


62 
by (REPEAT (DEPTH_SOLVE_1 (etac impCE 1


63 
ORELSE mp_tac 1 ORELSE ares_tac prems 1))) ;


64 
qed "iffCE";


65 


66 


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


68 
val major::prems= goal (the_context ())


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


70 
by (rtac classical 1);


71 
by (rtac (major RS notE) 1);


72 
by (REPEAT (ares_tac prems 1)) ;


73 
qed "swap";
