src/FOLP/FOLP_lemmas.ML

--- a/src/FOLP/FOLP_lemmas.ML	Tue Mar 18 21:57:36 2008 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,73 +0,0 @@
-(*  Title:      FOLP/FOLP_lemmas.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";