src/FOL/fol.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 0 a5a9c433f639
permissions -rw-r--r--
made tutorial first;
     1 (*  Title: 	FOL/fol.ML
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     5 
     6 Tactics and lemmas for fol.thy (classical First-Order Logic)
     7 *)
     8 
     9 open FOL;
    10 
    11 signature FOL_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 FOL_Lemmas : FOL_LEMMAS = 
    25 struct
    26 
    27 (*** Classical introduction rules for | and EX ***)
    28 
    29 val disjCI = prove_goal FOL.thy 
    30    "(~Q ==> P) ==> P|Q"
    31  (fn prems=>
    32   [ (resolve_tac [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 FOL.thy 
    38    "( ~(EX x. P(x)) ==> P(a)) ==> EX x.P(x)"
    39  (fn prems=>
    40   [ (resolve_tac [classical] 1),
    41     (eresolve_tac (prems RL [exI]) 1) ]);
    42 
    43 (*version of above, simplifying ~EX to ALL~ *)
    44 val exCI = prove_goal FOL.thy 
    45    "(ALL x. ~P(x) ==> P(a)) ==> EX x.P(x)"
    46  (fn [prem]=>
    47   [ (resolve_tac [ex_classical] 1),
    48     (resolve_tac [notI RS allI RS prem] 1),
    49     (eresolve_tac [notE] 1),
    50     (eresolve_tac [exI] 1) ]);
    51 
    52 val excluded_middle = prove_goal FOL.thy "~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 FOL.thy 
    61     "[| P-->Q;  ~P ==> R;  Q ==> R |] ==> 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 FOL.thy "~~P ==> P"
    68  (fn [major]=>
    69   [ (resolve_tac [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 FOL.thy [iff_def]
    77     "[| P<->Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R"
    78  (fn prems =>
    79   [ (resolve_tac [conjE] 1),
    80     (REPEAT (DEPTH_SOLVE_1 
    81 	(etac impCE 1  ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ]);
    82 
    83 
    84 (*Should be used as swap since ~P becomes redundant*)
    85 val swap = prove_goal FOL.thy 
    86    "~P ==> (~Q ==> P) ==> Q"
    87  (fn major::prems=>
    88   [ (resolve_tac [classical] 1),
    89     (rtac (major RS notE) 1),
    90     (REPEAT (ares_tac prems 1)) ]);
    91 
    92 end;
    93 
    94 open FOL_Lemmas;