src/FOL/FOL.ML
changeset 0 a5a9c433f639
child 440 1577cbcd0936
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/FOL/FOL.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,94 @@
     1.4 +(*  Title: 	FOL/fol.ML
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1991  University of Cambridge
     1.8 +
     1.9 +Tactics and lemmas for fol.thy (classical First-Order Logic)
    1.10 +*)
    1.11 +
    1.12 +open FOL;
    1.13 +
    1.14 +signature FOL_LEMMAS = 
    1.15 +  sig
    1.16 +  val disjCI : thm
    1.17 +  val excluded_middle : thm
    1.18 +  val exCI : thm
    1.19 +  val ex_classical : thm
    1.20 +  val iffCE : thm
    1.21 +  val impCE : thm
    1.22 +  val notnotD : thm
    1.23 +  val swap : thm
    1.24 +  end;
    1.25 +
    1.26 +
    1.27 +structure FOL_Lemmas : FOL_LEMMAS = 
    1.28 +struct
    1.29 +
    1.30 +(*** Classical introduction rules for | and EX ***)
    1.31 +
    1.32 +val disjCI = prove_goal FOL.thy 
    1.33 +   "(~Q ==> P) ==> P|Q"
    1.34 + (fn prems=>
    1.35 +  [ (resolve_tac [classical] 1),
    1.36 +    (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
    1.37 +    (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);
    1.38 +
    1.39 +(*introduction rule involving only EX*)
    1.40 +val ex_classical = prove_goal FOL.thy 
    1.41 +   "( ~(EX x. P(x)) ==> P(a)) ==> EX x.P(x)"
    1.42 + (fn prems=>
    1.43 +  [ (resolve_tac [classical] 1),
    1.44 +    (eresolve_tac (prems RL [exI]) 1) ]);
    1.45 +
    1.46 +(*version of above, simplifying ~EX to ALL~ *)
    1.47 +val exCI = prove_goal FOL.thy 
    1.48 +   "(ALL x. ~P(x) ==> P(a)) ==> EX x.P(x)"
    1.49 + (fn [prem]=>
    1.50 +  [ (resolve_tac [ex_classical] 1),
    1.51 +    (resolve_tac [notI RS allI RS prem] 1),
    1.52 +    (eresolve_tac [notE] 1),
    1.53 +    (eresolve_tac [exI] 1) ]);
    1.54 +
    1.55 +val excluded_middle = prove_goal FOL.thy "~P | P"
    1.56 + (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
    1.57 +
    1.58 +
    1.59 +(*** Special elimination rules *)
    1.60 +
    1.61 +
    1.62 +(*Classical implies (-->) elimination. *)
    1.63 +val impCE = prove_goal FOL.thy 
    1.64 +    "[| P-->Q;  ~P ==> R;  Q ==> R |] ==> R"
    1.65 + (fn major::prems=>
    1.66 +  [ (resolve_tac [excluded_middle RS disjE] 1),
    1.67 +    (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
    1.68 +
    1.69 +(*Double negation law*)
    1.70 +val notnotD = prove_goal FOL.thy "~~P ==> P"
    1.71 + (fn [major]=>
    1.72 +  [ (resolve_tac [classical] 1), (eresolve_tac [major RS notE] 1) ]);
    1.73 +
    1.74 +
    1.75 +(*** Tactics for implication and contradiction ***)
    1.76 +
    1.77 +(*Classical <-> elimination.  Proof substitutes P=Q in 
    1.78 +    ~P ==> ~Q    and    P ==> Q  *)
    1.79 +val iffCE = prove_goalw FOL.thy [iff_def]
    1.80 +    "[| P<->Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R"
    1.81 + (fn prems =>
    1.82 +  [ (resolve_tac [conjE] 1),
    1.83 +    (REPEAT (DEPTH_SOLVE_1 
    1.84 +	(etac impCE 1  ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ]);
    1.85 +
    1.86 +
    1.87 +(*Should be used as swap since ~P becomes redundant*)
    1.88 +val swap = prove_goal FOL.thy 
    1.89 +   "~P ==> (~Q ==> P) ==> Q"
    1.90 + (fn major::prems=>
    1.91 +  [ (resolve_tac [classical] 1),
    1.92 +    (rtac (major RS notE) 1),
    1.93 +    (REPEAT (ares_tac prems 1)) ]);
    1.94 +
    1.95 +end;
    1.96 +
    1.97 +open FOL_Lemmas;