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