--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOLP/FOLP_lemmas.ML Sun Sep 18 14:25:48 2005 +0200
@@ -0,0 +1,73 @@
+(* Title: FOLP/FOLP.ML
+ ID: $Id$
+ Author: Martin D Coen, Cambridge University Computer Laboratory
+ Copyright 1991 University of Cambridge
+*)
+
+(*** Classical introduction rules for | and EX ***)
+
+val prems= goal (the_context ())
+ "(!!x. x:~Q ==> f(x):P) ==> ?p : P|Q";
+by (rtac classical 1);
+by (REPEAT (ares_tac (prems@[disjI1,notI]) 1));
+by (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ;
+qed "disjCI";
+
+(*introduction rule involving only EX*)
+val prems= goal (the_context ())
+ "( !!u. u:~(EX x. P(x)) ==> f(u):P(a)) ==> ?p : EX x. P(x)";
+by (rtac classical 1);
+by (eresolve_tac (prems RL [exI]) 1) ;
+qed "ex_classical";
+
+(*version of above, simplifying ~EX to ALL~ *)
+val [prem]= goal (the_context ())
+ "(!!u. u:ALL x. ~P(x) ==> f(u):P(a)) ==> ?p : EX x. P(x)";
+by (rtac ex_classical 1);
+by (resolve_tac [notI RS allI RS prem] 1);
+by (etac notE 1);
+by (etac exI 1) ;
+qed "exCI";
+
+val excluded_middle = prove_goal (the_context ()) "?p : ~P | P"
+ (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
+
+
+(*** Special elimination rules *)
+
+
+(*Classical implies (-->) elimination. *)
+val major::prems= goal (the_context ())
+ "[| p:P-->Q; !!x. x:~P ==> f(x):R; !!y. y:Q ==> g(y):R |] ==> ?p : R";
+by (resolve_tac [excluded_middle RS disjE] 1);
+by (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ;
+qed "impCE";
+
+(*Double negation law*)
+Goal "p:~~P ==> ?p : P";
+by (rtac classical 1);
+by (etac notE 1);
+by (assume_tac 1);
+qed "notnotD";
+
+
+(*** Tactics for implication and contradiction ***)
+
+(*Classical <-> elimination. Proof substitutes P=Q in
+ ~P ==> ~Q and P ==> Q *)
+val prems = goalw (the_context ()) [iff_def]
+ "[| p:P<->Q; !!x y.[| x:P; y:Q |] ==> f(x,y):R; \
+\ !!x y.[| x:~P; y:~Q |] ==> g(x,y):R |] ==> ?p : R";
+by (rtac conjE 1);
+by (REPEAT (DEPTH_SOLVE_1 (etac impCE 1
+ ORELSE mp_tac 1 ORELSE ares_tac prems 1))) ;
+qed "iffCE";
+
+
+(*Should be used as swap since ~P becomes redundant*)
+val major::prems= goal (the_context ())
+ "p:~P ==> (!!x. x:~Q ==> f(x):P) ==> ?p : Q";
+by (rtac classical 1);
+by (rtac (major RS notE) 1);
+by (REPEAT (ares_tac prems 1)) ;
+qed "swap";