src/FOLP/FOLP_lemmas.ML
changeset 17480 fd19f77dcf60
child 24584 01e83ffa6c54
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/FOLP/FOLP_lemmas.ML	Sun Sep 18 14:25:48 2005 +0200
     1.3 @@ -0,0 +1,73 @@
     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 +
    1.10 +(*** Classical introduction rules for | and EX ***)
    1.11 +
    1.12 +val prems= goal (the_context ())
    1.13 +   "(!!x. x:~Q ==> f(x):P) ==> ?p : P|Q";
    1.14 +by (rtac classical 1);
    1.15 +by (REPEAT (ares_tac (prems@[disjI1,notI]) 1));
    1.16 +by (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ;
    1.17 +qed "disjCI";
    1.18 +
    1.19 +(*introduction rule involving only EX*)
    1.20 +val prems= goal (the_context ())
    1.21 +   "( !!u. u:~(EX x. P(x)) ==> f(u):P(a)) ==> ?p : EX x. P(x)";
    1.22 +by (rtac classical 1);
    1.23 +by (eresolve_tac (prems RL [exI]) 1) ;
    1.24 +qed "ex_classical";
    1.25 +
    1.26 +(*version of above, simplifying ~EX to ALL~ *)
    1.27 +val [prem]= goal (the_context ())
    1.28 +   "(!!u. u:ALL x. ~P(x) ==> f(u):P(a)) ==> ?p : EX x. P(x)";
    1.29 +by (rtac ex_classical 1);
    1.30 +by (resolve_tac [notI RS allI RS prem] 1);
    1.31 +by (etac notE 1);
    1.32 +by (etac exI 1) ;
    1.33 +qed "exCI";
    1.34 +
    1.35 +val excluded_middle = prove_goal (the_context ()) "?p : ~P | P"
    1.36 + (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
    1.37 +
    1.38 +
    1.39 +(*** Special elimination rules *)
    1.40 +
    1.41 +
    1.42 +(*Classical implies (-->) elimination. *)
    1.43 +val major::prems= goal (the_context ())
    1.44 +    "[| p:P-->Q;  !!x. x:~P ==> f(x):R;  !!y. y:Q ==> g(y):R |] ==> ?p : R";
    1.45 +by (resolve_tac [excluded_middle RS disjE] 1);
    1.46 +by (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ;
    1.47 +qed "impCE";
    1.48 +
    1.49 +(*Double negation law*)
    1.50 +Goal "p:~~P ==> ?p : P";
    1.51 +by (rtac classical 1);
    1.52 +by (etac notE 1);
    1.53 +by (assume_tac 1);
    1.54 +qed "notnotD";
    1.55 +
    1.56 +
    1.57 +(*** Tactics for implication and contradiction ***)
    1.58 +
    1.59 +(*Classical <-> elimination.  Proof substitutes P=Q in
    1.60 +    ~P ==> ~Q    and    P ==> Q  *)
    1.61 +val prems = goalw (the_context ()) [iff_def]
    1.62 +    "[| p:P<->Q; !!x y.[| x:P; y:Q |] ==> f(x,y):R;  \
    1.63 +\                !!x y.[| x:~P; y:~Q |] ==> g(x,y):R |] ==> ?p : R";
    1.64 +by (rtac conjE 1);
    1.65 +by (REPEAT (DEPTH_SOLVE_1 (etac impCE 1
    1.66 +               ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ;
    1.67 +qed "iffCE";
    1.68 +
    1.69 +
    1.70 +(*Should be used as swap since ~P becomes redundant*)
    1.71 +val major::prems= goal (the_context ())
    1.72 +   "p:~P ==> (!!x. x:~Q ==> f(x):P) ==> ?p : Q";
    1.73 +by (rtac classical 1);
    1.74 +by (rtac (major RS notE) 1);
    1.75 +by (REPEAT (ares_tac prems 1)) ;
    1.76 +qed "swap";