src/FOLP/FOLP_lemmas.ML
changeset 17480 fd19f77dcf60
child 24584 01e83ffa6c54
equal deleted inserted replaced
17479:68a7acb5f22e 17480:fd19f77dcf60
       
     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 : P|Q";
       
    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";