# HG changeset patch
# User paulson
# Date 933678498 -7200
# Node ID 7845a5cafbc68838aaf7c527347347bca10936a2
# Parent  1135f3f8782c7d4a3243c93f687c3a82311091fd
new examples file for SVC

diff -r 1135f3f8782c -r 7845a5cafbc6 src/HOL/IsaMakefile
--- 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
diff -r 1135f3f8782c -r 7845a5cafbc6 src/HOL/ex/svc_test.ML
--- /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 ();