src/FOLP/FOLP.ML
changeset 17480 fd19f77dcf60
parent 17479 68a7acb5f22e
child 17481 75166ebb619b
     1.1 --- a/src/FOLP/FOLP.ML	Sat Sep 17 20:49:14 2005 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,76 +0,0 @@
     1.4 -(*  Title:      FOLP/FOLP.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Martin D Coen, Cambridge University Computer Laboratory
     1.7 -    Copyright   1991  University of Cambridge
     1.8 -
     1.9 -Tactics and lemmas for FOLP (Classical First-Order Logic with Proofs)
    1.10 -*)
    1.11 -
    1.12 -(*** Classical introduction rules for | and EX ***)
    1.13 -
    1.14 -val prems= goal FOLP.thy 
    1.15 -   "(!!x. x:~Q ==> f(x):P) ==> ?p : P|Q";
    1.16 -by (rtac classical 1);
    1.17 -by (REPEAT (ares_tac (prems@[disjI1,notI]) 1));
    1.18 -by (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ;
    1.19 -qed "disjCI";
    1.20 -
    1.21 -(*introduction rule involving only EX*)
    1.22 -val prems= goal FOLP.thy 
    1.23 -   "( !!u. u:~(EX x. P(x)) ==> f(u):P(a)) ==> ?p : EX x. P(x)";
    1.24 -by (rtac classical 1);
    1.25 -by (eresolve_tac (prems RL [exI]) 1) ;
    1.26 -qed "ex_classical";
    1.27 -
    1.28 -(*version of above, simplifying ~EX to ALL~ *)
    1.29 -val [prem]= goal FOLP.thy 
    1.30 -   "(!!u. u:ALL x. ~P(x) ==> f(u):P(a)) ==> ?p : EX x. P(x)";
    1.31 -by (rtac ex_classical 1);
    1.32 -by (resolve_tac [notI RS allI RS prem] 1);
    1.33 -by (etac notE 1);
    1.34 -by (etac exI 1) ;
    1.35 -qed "exCI";
    1.36 -
    1.37 -val excluded_middle = prove_goal FOLP.thy "?p : ~P | P"
    1.38 - (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
    1.39 -
    1.40 -
    1.41 -(*** Special elimination rules *)
    1.42 -
    1.43 -
    1.44 -(*Classical implies (-->) elimination. *)
    1.45 -val major::prems= goal FOLP.thy 
    1.46 -    "[| p:P-->Q;  !!x. x:~P ==> f(x):R;  !!y. y:Q ==> g(y):R |] ==> ?p : R";
    1.47 -by (resolve_tac [excluded_middle RS disjE] 1);
    1.48 -by (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ;
    1.49 -qed "impCE";
    1.50 -
    1.51 -(*Double negation law*)
    1.52 -Goal "p:~~P ==> ?p : P";
    1.53 -by (rtac classical 1);
    1.54 -by (etac notE 1);
    1.55 -by (assume_tac 1);
    1.56 -qed "notnotD";
    1.57 -
    1.58 -
    1.59 -(*** Tactics for implication and contradiction ***)
    1.60 -
    1.61 -(*Classical <-> elimination.  Proof substitutes P=Q in 
    1.62 -    ~P ==> ~Q    and    P ==> Q  *)
    1.63 -val prems = goalw FOLP.thy [iff_def]
    1.64 -    "[| p:P<->Q; !!x y.[| x:P; y:Q |] ==> f(x,y):R;  \
    1.65 -\                !!x y.[| x:~P; y:~Q |] ==> g(x,y):R |] ==> ?p : R";
    1.66 -by (rtac conjE 1);
    1.67 -by (REPEAT (DEPTH_SOLVE_1 (etac impCE 1
    1.68 -               ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ;
    1.69 -qed "iffCE";
    1.70 -
    1.71 -
    1.72 -(*Should be used as swap since ~P becomes redundant*)
    1.73 -val major::prems= goal FOLP.thy 
    1.74 -   "p:~P ==> (!!x. x:~Q ==> f(x):P) ==> ?p : Q";
    1.75 -by (rtac classical 1);
    1.76 -by (rtac (major RS notE) 1);
    1.77 -by (REPEAT (ares_tac prems 1)) ;
    1.78 -qed "swap";
    1.79 -