src/FOLP/FOLP_lemmas.ML
author haftmann
Tue Sep 20 08:21:49 2005 +0200 (2005-09-20)
changeset 17496 26535df536ae
parent 17480 fd19f77dcf60
child 24584 01e83ffa6c54
permissions -rw-r--r--
slight adaptions to library changes
wenzelm@17480
     1
(*  Title:      FOLP/FOLP.ML
wenzelm@17480
     2
    ID:         $Id$
wenzelm@17480
     3
    Author:     Martin D Coen, Cambridge University Computer Laboratory
wenzelm@17480
     4
    Copyright   1991  University of Cambridge
wenzelm@17480
     5
*)
wenzelm@17480
     6
wenzelm@17480
     7
(*** Classical introduction rules for | and EX ***)
wenzelm@17480
     8
wenzelm@17480
     9
val prems= goal (the_context ())
wenzelm@17480
    10
   "(!!x. x:~Q ==> f(x):P) ==> ?p : P|Q";
wenzelm@17480
    11
by (rtac classical 1);
wenzelm@17480
    12
by (REPEAT (ares_tac (prems@[disjI1,notI]) 1));
wenzelm@17480
    13
by (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ;
wenzelm@17480
    14
qed "disjCI";
wenzelm@17480
    15
wenzelm@17480
    16
(*introduction rule involving only EX*)
wenzelm@17480
    17
val prems= goal (the_context ())
wenzelm@17480
    18
   "( !!u. u:~(EX x. P(x)) ==> f(u):P(a)) ==> ?p : EX x. P(x)";
wenzelm@17480
    19
by (rtac classical 1);
wenzelm@17480
    20
by (eresolve_tac (prems RL [exI]) 1) ;
wenzelm@17480
    21
qed "ex_classical";
wenzelm@17480
    22
wenzelm@17480
    23
(*version of above, simplifying ~EX to ALL~ *)
wenzelm@17480
    24
val [prem]= goal (the_context ())
wenzelm@17480
    25
   "(!!u. u:ALL x. ~P(x) ==> f(u):P(a)) ==> ?p : EX x. P(x)";
wenzelm@17480
    26
by (rtac ex_classical 1);
wenzelm@17480
    27
by (resolve_tac [notI RS allI RS prem] 1);
wenzelm@17480
    28
by (etac notE 1);
wenzelm@17480
    29
by (etac exI 1) ;
wenzelm@17480
    30
qed "exCI";
wenzelm@17480
    31
wenzelm@17480
    32
val excluded_middle = prove_goal (the_context ()) "?p : ~P | P"
wenzelm@17480
    33
 (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
wenzelm@17480
    34
wenzelm@17480
    35
wenzelm@17480
    36
(*** Special elimination rules *)
wenzelm@17480
    37
wenzelm@17480
    38
wenzelm@17480
    39
(*Classical implies (-->) elimination. *)
wenzelm@17480
    40
val major::prems= goal (the_context ())
wenzelm@17480
    41
    "[| p:P-->Q;  !!x. x:~P ==> f(x):R;  !!y. y:Q ==> g(y):R |] ==> ?p : R";
wenzelm@17480
    42
by (resolve_tac [excluded_middle RS disjE] 1);
wenzelm@17480
    43
by (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ;
wenzelm@17480
    44
qed "impCE";
wenzelm@17480
    45
wenzelm@17480
    46
(*Double negation law*)
wenzelm@17480
    47
Goal "p:~~P ==> ?p : P";
wenzelm@17480
    48
by (rtac classical 1);
wenzelm@17480
    49
by (etac notE 1);
wenzelm@17480
    50
by (assume_tac 1);
wenzelm@17480
    51
qed "notnotD";
wenzelm@17480
    52
wenzelm@17480
    53
wenzelm@17480
    54
(*** Tactics for implication and contradiction ***)
wenzelm@17480
    55
wenzelm@17480
    56
(*Classical <-> elimination.  Proof substitutes P=Q in
wenzelm@17480
    57
    ~P ==> ~Q    and    P ==> Q  *)
wenzelm@17480
    58
val prems = goalw (the_context ()) [iff_def]
wenzelm@17480
    59
    "[| p:P<->Q; !!x y.[| x:P; y:Q |] ==> f(x,y):R;  \
wenzelm@17480
    60
\                !!x y.[| x:~P; y:~Q |] ==> g(x,y):R |] ==> ?p : R";
wenzelm@17480
    61
by (rtac conjE 1);
wenzelm@17480
    62
by (REPEAT (DEPTH_SOLVE_1 (etac impCE 1
wenzelm@17480
    63
               ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ;
wenzelm@17480
    64
qed "iffCE";
wenzelm@17480
    65
wenzelm@17480
    66
wenzelm@17480
    67
(*Should be used as swap since ~P becomes redundant*)
wenzelm@17480
    68
val major::prems= goal (the_context ())
wenzelm@17480
    69
   "p:~P ==> (!!x. x:~Q ==> f(x):P) ==> ?p : Q";
wenzelm@17480
    70
by (rtac classical 1);
wenzelm@17480
    71
by (rtac (major RS notE) 1);
wenzelm@17480
    72
by (REPEAT (ares_tac prems 1)) ;
wenzelm@17480
    73
qed "swap";