--- a/src/HOL/IsaMakefile Tue Aug 03 13:06:16 1999 +0200
+++ b/src/HOL/IsaMakefile Tue Aug 03 13:08:18 1999 +0200
@@ -326,7 +326,7 @@
ex/IntRing.thy ex/IntRingDefs.ML ex/IntRingDefs.thy ex/Lagrange.ML \
ex/Lagrange.thy ex/Ring.ML ex/Ring.thy ex/StringEx.ML \
ex/StringEx.thy ex/Tarski.ML ex/Tarski.thy \
- ex/BinEx.ML ex/BinEx.thy ex/MonoidGroup.thy \
+ ex/BinEx.ML ex/BinEx.thy ex/svc_test.ML ex/MonoidGroup.thy \
ex/PiSets.thy ex/PiSets.ML ex/LocaleGroup.thy ex/LocaleGroup.ML \
ex/Antiquote.thy ex/Antiquote.ML ex/Points.thy
@$(ISATOOL) usedir $(OUT)/HOL ex
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/svc_test.ML Tue Aug 03 13:08:18 1999 +0200
@@ -0,0 +1,54 @@
+(* Title: HOL/ex/svc_test.ML
+ ID: $Id$
+ Author: Lawrence C Paulson
+ Copyright 1999 University of Cambridge
+
+Demonstrating svc_tac: the interface to the Stanford Validity Checker
+
+SVC is assumed to be present if the environment variable SVC_HOME is non-empty.
+
+set Svc.trace;
+*)
+
+val svc_enabled = getenv "SVC_HOME" <> "";
+
+if svc_enabled then
+ (
+ (** Propositional Logic **)
+ Goal "((P & (Q-->R))-->S) = ((~P | Q | S) & (~P | ~R | S))";
+ by (svc_tac 1);
+ result();
+
+ (*Blast_tac's runtime for this type of problem appears to be exponential
+ in its length*)
+ Goal "P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P";
+ by (svc_tac 1);
+ result();
+
+ (** Linear arithmetic **)
+
+ Goal "x ~= #14 & x ~= #13 & x ~= #12 & x ~= #11 & x ~= #10 & x ~= #9 & \
+ \ x ~= #8 & x ~= #7 & x ~= #6 & x ~= #5 & x ~= #4 & x ~= #3 & \
+ \ x ~= #2 & x ~= #1 & #0 < x & x < #16 --> #15 = (x::int)";
+ by (svc_tac 1);
+ result();
+
+ (*merely to test polarity handling in the presence of biconditionals*)
+ Goal "(x < (y::int)) = (x+#1 <= y)";
+ by (svc_tac 1);
+ result();
+
+ (** Natural number examples requiring implicit "non-negative" assumptions*)
+
+ Goal "(#3::nat)*a <= #2 + #4*b + #6*c & #11 <= #2*a + b + #2*c & \
+ \ a + #3*b <= #5 + #2*c --> #2 + #3*b <= #2*a + #6*c";
+ by (svc_tac 1);
+ result();
+
+ Goal "(n::nat) < #2 ==> (n = #0) | (n = #1)";
+ by (svc_tac 1);
+ result();
+
+ ()
+)
+else ();