src/FOL/fol.ML
author wenzelm
Sun, 15 Oct 2000 19:50:35 +0200
changeset 10220 2a726de6e124
parent 0 a5a9c433f639
permissions -rw-r--r--
proper symbol markup with \isamath, \isatext; support sub/super scripts:
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	FOL/fol.ML
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Tactics and lemmas for fol.thy (classical First-Order Logic)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
open FOL;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
signature FOL_LEMMAS = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
  sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
  val disjCI : thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
  val excluded_middle : thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
  val exCI : thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
  val ex_classical : thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
  val iffCE : thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
  val impCE : thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
  val notnotD : thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
  val swap : thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
structure FOL_Lemmas : FOL_LEMMAS = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
(*** Classical introduction rules for | and EX ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
val disjCI = prove_goal FOL.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
   "(~Q ==> P) ==> P|Q"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
  [ (resolve_tac [classical] 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
    (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
    (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
(*introduction rule involving only EX*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
val ex_classical = prove_goal FOL.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
   "( ~(EX x. P(x)) ==> P(a)) ==> EX x.P(x)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
  [ (resolve_tac [classical] 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
    (eresolve_tac (prems RL [exI]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
(*version of above, simplifying ~EX to ALL~ *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
val exCI = prove_goal FOL.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
   "(ALL x. ~P(x) ==> P(a)) ==> EX x.P(x)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
 (fn [prem]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
  [ (resolve_tac [ex_classical] 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
    (resolve_tac [notI RS allI RS prem] 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
    (eresolve_tac [notE] 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
    (eresolve_tac [exI] 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
val excluded_middle = prove_goal FOL.thy "~P | P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
 (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
(*** Special elimination rules *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
(*Classical implies (-->) elimination. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
val impCE = prove_goal FOL.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
    "[| P-->Q;  ~P ==> R;  Q ==> R |] ==> R"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
  [ (resolve_tac [excluded_middle RS disjE] 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
    (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
(*Double negation law*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
val notnotD = prove_goal FOL.thy "~~P ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
 (fn [major]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
  [ (resolve_tac [classical] 1), (eresolve_tac [major RS notE] 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
(*** Tactics for implication and contradiction ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
(*Classical <-> elimination.  Proof substitutes P=Q in 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
    ~P ==> ~Q    and    P ==> Q  *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
val iffCE = prove_goalw FOL.thy [iff_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
    "[| P<->Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
 (fn prems =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
  [ (resolve_tac [conjE] 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
    (REPEAT (DEPTH_SOLVE_1 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
	(etac impCE 1  ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
(*Should be used as swap since ~P becomes redundant*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
val swap = prove_goal FOL.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
   "~P ==> (~Q ==> P) ==> Q"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
  [ (resolve_tac [classical] 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
    (rtac (major RS notE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
    (REPEAT (ares_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
open FOL_Lemmas;