src/FOL/FOL.ML
author lcp
Fri Jun 24 13:01:53 1994 +0200 (1994-06-24)
changeset 440 1577cbcd0936
parent 0 a5a9c433f639
child 677 dbb8431184f9
permissions -rw-r--r--
FOL/FOL.ML/excluded_middle_tac: new
     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 excluded_middle_tac : string -> int -> tactic
    16   val exCI : thm
    17   val ex_classical : thm
    18   val iffCE : thm
    19   val impCE : thm
    20   val notnotD : thm
    21   val swap : thm
    22   end;
    23 
    24 
    25 structure FOL_Lemmas : FOL_LEMMAS = 
    26 struct
    27 
    28 (*** Classical introduction rules for | and EX ***)
    29 
    30 val disjCI = prove_goal FOL.thy 
    31    "(~Q ==> P) ==> P|Q"
    32  (fn prems=>
    33   [ (resolve_tac [classical] 1),
    34     (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
    35     (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);
    36 
    37 (*introduction rule involving only EX*)
    38 val ex_classical = prove_goal FOL.thy 
    39    "( ~(EX x. P(x)) ==> P(a)) ==> EX x.P(x)"
    40  (fn prems=>
    41   [ (resolve_tac [classical] 1),
    42     (eresolve_tac (prems RL [exI]) 1) ]);
    43 
    44 (*version of above, simplifying ~EX to ALL~ *)
    45 val exCI = prove_goal FOL.thy 
    46    "(ALL x. ~P(x) ==> P(a)) ==> EX x.P(x)"
    47  (fn [prem]=>
    48   [ (resolve_tac [ex_classical] 1),
    49     (resolve_tac [notI RS allI RS prem] 1),
    50     (eresolve_tac [notE] 1),
    51     (eresolve_tac [exI] 1) ]);
    52 
    53 val excluded_middle = prove_goal FOL.thy "~P | P"
    54  (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
    55 
    56 (*For disjunctive case analysis*)
    57 fun excluded_middle_tac sP =
    58     res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
    59 
    60 (*** Special elimination rules *)
    61 
    62 
    63 (*Classical implies (-->) elimination. *)
    64 val impCE = prove_goal FOL.thy 
    65     "[| P-->Q;  ~P ==> R;  Q ==> R |] ==> R"
    66  (fn major::prems=>
    67   [ (resolve_tac [excluded_middle RS disjE] 1),
    68     (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
    69 
    70 (*Double negation law*)
    71 val notnotD = prove_goal FOL.thy "~~P ==> P"
    72  (fn [major]=>
    73   [ (resolve_tac [classical] 1), (eresolve_tac [major RS notE] 1) ]);
    74 
    75 
    76 (*** Tactics for implication and contradiction ***)
    77 
    78 (*Classical <-> elimination.  Proof substitutes P=Q in 
    79     ~P ==> ~Q    and    P ==> Q  *)
    80 val iffCE = prove_goalw FOL.thy [iff_def]
    81     "[| P<->Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R"
    82  (fn prems =>
    83   [ (resolve_tac [conjE] 1),
    84     (REPEAT (DEPTH_SOLVE_1 
    85 	(etac impCE 1  ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ]);
    86 
    87 
    88 (*Should be used as swap since ~P becomes redundant*)
    89 val swap = prove_goal FOL.thy 
    90    "~P ==> (~Q ==> P) ==> Q"
    91  (fn major::prems=>
    92   [ (resolve_tac [classical] 1),
    93     (rtac (major RS notE) 1),
    94     (REPEAT (ares_tac prems 1)) ]);
    95 
    96 end;
    97 
    98 open FOL_Lemmas;