src/FOL/FOL.ML
author paulson
Wed Nov 26 17:35:46 1997 +0100 (1997-11-26)
changeset 4308 9abce31cc764
parent 4186 e39f28f94cf8
child 5159 8fc4fb20d70f
permissions -rw-r--r--
Added rule impCE'
     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 val ccontr = FalseE RS classical;
    13 
    14 (*** Classical introduction rules for | and EX ***)
    15 
    16 qed_goal "disjCI" FOL.thy 
    17    "(~Q ==> P) ==> P|Q"
    18  (fn prems=>
    19   [ (rtac classical 1),
    20     (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
    21     (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);
    22 
    23 (*introduction rule involving only EX*)
    24 qed_goal "ex_classical" FOL.thy 
    25    "( ~(EX x. P(x)) ==> P(a)) ==> EX x. P(x)"
    26  (fn prems=>
    27   [ (rtac classical 1),
    28     (eresolve_tac (prems RL [exI]) 1) ]);
    29 
    30 (*version of above, simplifying ~EX to ALL~ *)
    31 qed_goal "exCI" FOL.thy 
    32    "(ALL x. ~P(x) ==> P(a)) ==> EX x. P(x)"
    33  (fn [prem]=>
    34   [ (rtac ex_classical 1),
    35     (resolve_tac [notI RS allI RS prem] 1),
    36     (etac notE 1),
    37     (etac exI 1) ]);
    38 
    39 qed_goal "excluded_middle" FOL.thy "~P | P"
    40  (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
    41 
    42 (*For disjunctive case analysis*)
    43 fun excluded_middle_tac sP =
    44     res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
    45 
    46 (*** Special elimination rules *)
    47 
    48 
    49 (*Classical implies (-->) elimination. *)
    50 qed_goal "impCE" FOL.thy 
    51     "[| P-->Q;  ~P ==> R;  Q ==> R |] ==> R"
    52  (fn major::prems=>
    53   [ (resolve_tac [excluded_middle RS disjE] 1),
    54     (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
    55 
    56 (*This version of --> elimination works on Q before P.  It works best for
    57   those cases in which P holds "almost everywhere".  Can't install as
    58   default: would break old proofs.*)
    59 qed_goal "impCE'" thy 
    60     "[| P-->Q;  Q ==> R;  ~P ==> R |] ==> R"
    61  (fn major::prems=>
    62   [ (resolve_tac [excluded_middle RS disjE] 1),
    63     (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
    64 
    65 (*Double negation law*)
    66 qed_goal "notnotD" FOL.thy "~~P ==> P"
    67  (fn [major]=>
    68   [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]);
    69 
    70 qed_goal "contrapos2" FOL.thy "[| Q; ~ P ==> ~ Q |] ==> P" (fn [p1,p2] => [
    71         rtac classical 1,
    72         dtac p2 1,
    73         etac notE 1,
    74         rtac p1 1]);
    75 
    76 (*** Tactics for implication and contradiction ***)
    77 
    78 (*Classical <-> elimination.  Proof substitutes P=Q in 
    79     ~P ==> ~Q    and    P ==> Q  *)
    80 qed_goalw "iffCE" FOL.thy [iff_def]
    81     "[| P<->Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R"
    82  (fn prems =>
    83   [ (rtac conjE 1),
    84     (REPEAT (DEPTH_SOLVE_1 
    85         (etac impCE 1  ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ]);
    86