src/FOL/fol.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/fol.ML	Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,94 @@
+(*  Title: 	FOL/fol.ML
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1991  University of Cambridge
+
+Tactics and lemmas for fol.thy (classical First-Order Logic)
+*)
+
+open FOL;
+
+signature FOL_LEMMAS = 
+  sig
+  val disjCI : thm
+  val excluded_middle : thm
+  val exCI : thm
+  val ex_classical : thm
+  val iffCE : thm
+  val impCE : thm
+  val notnotD : thm
+  val swap : thm
+  end;
+
+
+structure FOL_Lemmas : FOL_LEMMAS = 
+struct
+
+(*** Classical introduction rules for | and EX ***)
+
+val disjCI = prove_goal FOL.thy 
+   "(~Q ==> P) ==> P|Q"
+ (fn prems=>
+  [ (resolve_tac [classical] 1),
+    (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
+    (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);
+
+(*introduction rule involving only EX*)
+val ex_classical = prove_goal FOL.thy 
+   "( ~(EX x. P(x)) ==> P(a)) ==> EX x.P(x)"
+ (fn prems=>
+  [ (resolve_tac [classical] 1),
+    (eresolve_tac (prems RL [exI]) 1) ]);
+
+(*version of above, simplifying ~EX to ALL~ *)
+val exCI = prove_goal FOL.thy 
+   "(ALL x. ~P(x) ==> P(a)) ==> EX x.P(x)"
+ (fn [prem]=>
+  [ (resolve_tac [ex_classical] 1),
+    (resolve_tac [notI RS allI RS prem] 1),
+    (eresolve_tac [notE] 1),
+    (eresolve_tac [exI] 1) ]);
+
+val excluded_middle = prove_goal FOL.thy "~P | P"
+ (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
+
+
+(*** Special elimination rules *)
+
+
+(*Classical implies (-->) elimination. *)
+val impCE = prove_goal FOL.thy 
+    "[| P-->Q;  ~P ==> R;  Q ==> R |] ==> R"
+ (fn major::prems=>
+  [ (resolve_tac [excluded_middle RS disjE] 1),
+    (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
+
+(*Double negation law*)
+val notnotD = prove_goal FOL.thy "~~P ==> P"
+ (fn [major]=>
+  [ (resolve_tac [classical] 1), (eresolve_tac [major RS notE] 1) ]);
+
+
+(*** Tactics for implication and contradiction ***)
+
+(*Classical <-> elimination.  Proof substitutes P=Q in 
+    ~P ==> ~Q    and    P ==> Q  *)
+val iffCE = prove_goalw FOL.thy [iff_def]
+    "[| P<->Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R"
+ (fn prems =>
+  [ (resolve_tac [conjE] 1),
+    (REPEAT (DEPTH_SOLVE_1 
+	(etac impCE 1  ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ]);
+
+
+(*Should be used as swap since ~P becomes redundant*)
+val swap = prove_goal FOL.thy 
+   "~P ==> (~Q ==> P) ==> Q"
+ (fn major::prems=>
+  [ (resolve_tac [classical] 1),
+    (rtac (major RS notE) 1),
+    (REPEAT (ares_tac prems 1)) ]);
+
+end;
+
+open FOL_Lemmas;