src/FOL/FOL.ML
author clasohm
Mon Jan 29 13:58:15 1996 +0100 (1996-01-29)
changeset 1459 d12da312eff4
parent 1280 909079af97b7
child 2469 b50b8c0eec01
permissions -rw-r--r--
expanded tabs
     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 
    12 (*** Classical introduction rules for | and EX ***)
    13 
    14 qed_goal "disjCI" FOL.thy 
    15    "(~Q ==> P) ==> P|Q"
    16  (fn prems=>
    17   [ (rtac classical 1),
    18     (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
    19     (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);
    20 
    21 (*introduction rule involving only EX*)
    22 qed_goal "ex_classical" FOL.thy 
    23    "( ~(EX x. P(x)) ==> P(a)) ==> EX x.P(x)"
    24  (fn prems=>
    25   [ (rtac classical 1),
    26     (eresolve_tac (prems RL [exI]) 1) ]);
    27 
    28 (*version of above, simplifying ~EX to ALL~ *)
    29 qed_goal "exCI" FOL.thy 
    30    "(ALL x. ~P(x) ==> P(a)) ==> EX x.P(x)"
    31  (fn [prem]=>
    32   [ (rtac ex_classical 1),
    33     (resolve_tac [notI RS allI RS prem] 1),
    34     (etac notE 1),
    35     (etac exI 1) ]);
    36 
    37 qed_goal "excluded_middle" FOL.thy "~P | P"
    38  (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
    39 
    40 (*For disjunctive case analysis*)
    41 fun excluded_middle_tac sP =
    42     res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
    43 
    44 (*** Special elimination rules *)
    45 
    46 
    47 (*Classical implies (-->) elimination. *)
    48 qed_goal "impCE" FOL.thy 
    49     "[| P-->Q;  ~P ==> R;  Q ==> R |] ==> R"
    50  (fn major::prems=>
    51   [ (resolve_tac [excluded_middle RS disjE] 1),
    52     (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
    53 
    54 (*Double negation law*)
    55 qed_goal "notnotD" FOL.thy "~~P ==> P"
    56  (fn [major]=>
    57   [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]);
    58 
    59 
    60 (*** Tactics for implication and contradiction ***)
    61 
    62 (*Classical <-> elimination.  Proof substitutes P=Q in 
    63     ~P ==> ~Q    and    P ==> Q  *)
    64 qed_goalw "iffCE" FOL.thy [iff_def]
    65     "[| P<->Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R"
    66  (fn prems =>
    67   [ (rtac conjE 1),
    68     (REPEAT (DEPTH_SOLVE_1 
    69         (etac impCE 1  ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ]);