src/FOL/FOL.ML
author wenzelm
Mon Nov 03 12:28:45 1997 +0100 (1997-11-03)
changeset 4096 8cdf672a83e8
parent 3835 9a5a4e123859
child 4186 e39f28f94cf8
permissions -rw-r--r--
moved cladata.ML, simpdata.ML to ROOT.ML;
clasohm@1459
     1
(*  Title:      FOL/FOL.ML
clasohm@0
     2
    ID:         $Id$
clasohm@1459
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1991  University of Cambridge
clasohm@0
     5
clasohm@1280
     6
Tactics and lemmas for FOL.thy (classical First-Order Logic)
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
open FOL;
clasohm@0
    10
clasohm@0
    11
paulson@2576
    12
val ccontr = FalseE RS classical;
paulson@2576
    13
clasohm@0
    14
(*** Classical introduction rules for | and EX ***)
clasohm@0
    15
clasohm@779
    16
qed_goal "disjCI" FOL.thy 
clasohm@0
    17
   "(~Q ==> P) ==> P|Q"
clasohm@0
    18
 (fn prems=>
clasohm@1459
    19
  [ (rtac classical 1),
clasohm@0
    20
    (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
clasohm@0
    21
    (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);
clasohm@0
    22
clasohm@0
    23
(*introduction rule involving only EX*)
clasohm@779
    24
qed_goal "ex_classical" FOL.thy 
wenzelm@3835
    25
   "( ~(EX x. P(x)) ==> P(a)) ==> EX x. P(x)"
clasohm@0
    26
 (fn prems=>
clasohm@1459
    27
  [ (rtac classical 1),
clasohm@0
    28
    (eresolve_tac (prems RL [exI]) 1) ]);
clasohm@0
    29
clasohm@0
    30
(*version of above, simplifying ~EX to ALL~ *)
clasohm@779
    31
qed_goal "exCI" FOL.thy 
wenzelm@3835
    32
   "(ALL x. ~P(x) ==> P(a)) ==> EX x. P(x)"
clasohm@0
    33
 (fn [prem]=>
clasohm@1459
    34
  [ (rtac ex_classical 1),
clasohm@0
    35
    (resolve_tac [notI RS allI RS prem] 1),
clasohm@1459
    36
    (etac notE 1),
clasohm@1459
    37
    (etac exI 1) ]);
clasohm@0
    38
clasohm@779
    39
qed_goal "excluded_middle" FOL.thy "~P | P"
clasohm@0
    40
 (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
clasohm@0
    41
lcp@440
    42
(*For disjunctive case analysis*)
lcp@440
    43
fun excluded_middle_tac sP =
lcp@440
    44
    res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
clasohm@0
    45
clasohm@0
    46
(*** Special elimination rules *)
clasohm@0
    47
clasohm@0
    48
clasohm@0
    49
(*Classical implies (-->) elimination. *)
clasohm@779
    50
qed_goal "impCE" FOL.thy 
clasohm@0
    51
    "[| P-->Q;  ~P ==> R;  Q ==> R |] ==> R"
clasohm@0
    52
 (fn major::prems=>
clasohm@0
    53
  [ (resolve_tac [excluded_middle RS disjE] 1),
clasohm@0
    54
    (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
clasohm@0
    55
clasohm@0
    56
(*Double negation law*)
clasohm@779
    57
qed_goal "notnotD" FOL.thy "~~P ==> P"
clasohm@0
    58
 (fn [major]=>
clasohm@1459
    59
  [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]);
clasohm@0
    60
clasohm@0
    61
clasohm@0
    62
(*** Tactics for implication and contradiction ***)
clasohm@0
    63
clasohm@0
    64
(*Classical <-> elimination.  Proof substitutes P=Q in 
clasohm@0
    65
    ~P ==> ~Q    and    P ==> Q  *)
clasohm@779
    66
qed_goalw "iffCE" FOL.thy [iff_def]
clasohm@0
    67
    "[| P<->Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R"
clasohm@0
    68
 (fn prems =>
clasohm@1459
    69
  [ (rtac conjE 1),
clasohm@0
    70
    (REPEAT (DEPTH_SOLVE_1 
clasohm@1459
    71
        (etac impCE 1  ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ]);
paulson@2469
    72