added contrapos
authoroheimb
Fri, 07 Nov 1997 17:51:26 +0100
changeset 4187 2fafec5868fe
parent 4186 e39f28f94cf8
child 4188 1025a27b08f9
added contrapos
src/FOL/IFOL.ML
--- a/src/FOL/IFOL.ML	Fri Nov 07 17:51:10 1997 +0100
+++ b/src/FOL/IFOL.ML	Fri Nov 07 17:51:26 1997 +0100
@@ -61,6 +61,11 @@
 qed_goal "rev_mp" IFOL.thy "[| P;  P --> Q |] ==> Q"
  (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
 
+qed_goal "contrapos" IFOL.thy "[| ~Q;  P==>Q |] ==> ~P"
+ (fn [major,minor]=> 
+  [ (rtac (major RS notE RS notI) 1), 
+    (etac minor 1) ]);
+
 
 (*Contrapositive of an inference rule*)
 qed_goal "contrapos" IFOL.thy "[| ~Q;  P==>Q |] ==> ~P"