src/FOLP/FOLP.ML
author paulson
Mon Apr 26 13:25:49 1999 +0200 (1999-04-26)
changeset 6509 9f7f4fd05b1f
parent 3836 f1a1817659e6
child 9263 53e09e592278
permissions -rw-r--r--
fixed a bug many years old in rule plusEC
     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 Tactics and lemmas for FOLP (Classical First-Order Logic with Proofs)
     7 *)
     8 
     9 open FOLP;
    10 
    11 signature FOLP_LEMMAS = 
    12   sig
    13   val disjCI : thm
    14   val excluded_middle : thm
    15   val exCI : thm
    16   val ex_classical : thm
    17   val iffCE : thm
    18   val impCE : thm
    19   val notnotD : thm
    20   val swap : thm
    21   end;
    22 
    23 
    24 structure FOLP_Lemmas : FOLP_LEMMAS = 
    25 struct
    26 
    27 (*** Classical introduction rules for | and EX ***)
    28 
    29 val disjCI = prove_goal FOLP.thy 
    30    "(!!x. x:~Q ==> f(x):P) ==> ?p : P|Q"
    31  (fn prems=>
    32   [ (rtac classical 1),
    33     (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
    34     (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);
    35 
    36 (*introduction rule involving only EX*)
    37 val ex_classical = prove_goal FOLP.thy 
    38    "( !!u. u:~(EX x. P(x)) ==> f(u):P(a)) ==> ?p : EX x. P(x)"
    39  (fn prems=>
    40   [ (rtac classical 1),
    41     (eresolve_tac (prems RL [exI]) 1) ]);
    42 
    43 (*version of above, simplifying ~EX to ALL~ *)
    44 val exCI = prove_goal FOLP.thy 
    45    "(!!u. u:ALL x. ~P(x) ==> f(u):P(a)) ==> ?p : EX x. P(x)"
    46  (fn [prem]=>
    47   [ (rtac ex_classical 1),
    48     (resolve_tac [notI RS allI RS prem] 1),
    49     (etac notE 1),
    50     (etac exI 1) ]);
    51 
    52 val excluded_middle = prove_goal FOLP.thy "?p : ~P | P"
    53  (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
    54 
    55 
    56 (*** Special elimination rules *)
    57 
    58 
    59 (*Classical implies (-->) elimination. *)
    60 val impCE = prove_goal FOLP.thy 
    61     "[| p:P-->Q;  !!x. x:~P ==> f(x):R;  !!y. y:Q ==> g(y):R |] ==> ?p : R"
    62  (fn major::prems=>
    63   [ (resolve_tac [excluded_middle RS disjE] 1),
    64     (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
    65 
    66 (*Double negation law*)
    67 val notnotD = prove_goal FOLP.thy "p:~~P ==> ?p : P"
    68  (fn [major]=>
    69   [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]);
    70 
    71 
    72 (*** Tactics for implication and contradiction ***)
    73 
    74 (*Classical <-> elimination.  Proof substitutes P=Q in 
    75     ~P ==> ~Q    and    P ==> Q  *)
    76 val iffCE = prove_goalw FOLP.thy [iff_def]
    77     "[| p:P<->Q; !!x y.[| x:P; y:Q |] ==> f(x,y):R;  \
    78 \                !!x y.[| x:~P; y:~Q |] ==> g(x,y):R |] ==> ?p : R"
    79  (fn prems =>
    80   [ (rtac conjE 1),
    81     (REPEAT (DEPTH_SOLVE_1 
    82         (etac impCE 1  ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ]);
    83 
    84 
    85 (*Should be used as swap since ~P becomes redundant*)
    86 val swap = prove_goal FOLP.thy 
    87    "p:~P ==> (!!x. x:~Q ==> f(x):P) ==> ?p : Q"
    88  (fn major::prems=>
    89   [ (rtac classical 1),
    90     (rtac (major RS notE) 1),
    91     (REPEAT (ares_tac prems 1)) ]);
    92 
    93 end;
    94 
    95 open FOLP_Lemmas;