# HG changeset patch
# User paulson
# Date 935068272 -7200
# Node ID 5cfe2944910a88a22cd44530e52babf0053315db
# Parent  69d601df351c957cfbdfc53fcbfac65ebe532211
documented svc_tac

diff -r 69d601df351c -r 5cfe2944910a doc-src/HOL/HOL.tex
--- a/doc-src/HOL/HOL.tex	Thu Aug 19 13:56:02 1999 +0200
+++ b/doc-src/HOL/HOL.tex	Thu Aug 19 15:11:12 1999 +0200
@@ -901,6 +901,7 @@
 There is also a large collection of monotonicity theorems for constructions
 on sets in the file \texttt{HOL/mono.ML}.
 
+
 \section{Generic packages}
 \label{sec:HOL:generic-packages}
 
@@ -1008,15 +1009,109 @@
 well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
 rule; recall Fig.\ts\ref{hol-lemmas2} above.
 
-The classical reasoner is installed.  Tactics such as \texttt{Blast_tac} and {\tt
-Best_tac} refer to the default claset (\texttt{claset()}), which works for most
-purposes.  Named clasets include \ttindexbold{prop_cs}, which includes the
-propositional rules, and \ttindexbold{HOL_cs}, which also includes quantifier
-rules.  See the file \texttt{HOL/cladata.ML} for lists of the classical rules,
+The classical reasoner is installed.  Tactics such as \texttt{Blast_tac} and
+{\tt Best_tac} refer to the default claset (\texttt{claset()}), which works
+for most purposes.  Named clasets include \ttindexbold{prop_cs}, which
+includes the propositional rules, and \ttindexbold{HOL_cs}, which also
+includes quantifier rules.  See the file \texttt{HOL/cladata.ML} for lists of
+the classical rules,
 and \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
 {Chap.\ts\ref{chap:classical}} for more discussion of classical proof methods.
 
 
+\section{Calling the decision procedure SVC}\label{sec:HOL:SVC}
+
+\index{SVC decision procedure|(}
+
+The Stanford Validity Checker (SVC) is a tool that can check the validity of
+certain types of formulae.  If it is installed on your machine, then
+Isabelle/HOL can be configured to call it through the tactic
+\ttindex{svc_tac}.  It is ideal for large tautologies and complex problems in
+linear arithmetic.  Subexpressions that SVC cannot handle are automatically
+replaced by variables, so you can call the tactic on any subgoal.  See the
+file \texttt{HOL/ex/svc_test.ML} for examples.
+\begin{ttbox} 
+svc_tac   : int -> tactic
+Svc.trace : bool ref      \hfill{\bf initially false}
+\end{ttbox}
+
+\begin{ttdescription}
+\item[\ttindexbold{svc_tac} $i$] attempts to prove subgoal~$i$ by translating
+  it into a formula recognized by~SVC\@.  If it succeeds then the subgoal is
+  removed.  It fails if SVC is unable to prove the subgoal.  It crashes with
+  an error message if SVC appears not to be installed.  Numeric variables may
+  have types \texttt{nat}, \texttt{int} or \texttt{real}.
+
+\item[\ttindexbold{Svc.trace}] is a flag that, if set, causes \texttt{svc_tac}
+  to trace its operations: abstraction of the subgoal, translation to SVC
+  syntax, SVC's response.
+\end{ttdescription}
+
+Here is an example, with tracing turned on:
+\begin{ttbox}
+set Svc.trace;
+{\out val it : bool = true}
+Goal "(#3::nat)*a <= #2 + #4*b + #6*c  & #11 <= #2*a + b + #2*c & \ttback
+\ttback     a + #3*b <= #5 + #2*c  --> #2 + #3*b <= #2*a + #6*c";
+
+by (svc_tac 1);
+{\out Subgoal abstracted to}
+{\out #3 * a <= #2 + #4 * b + #6 * c &}
+{\out #11 <= #2 * a + b + #2 * c & a + #3 * b <= #5 + #2 * c -->}
+{\out #2 + #3 * b <= #2 * a + #6 * c}
+{\out Calling SVC:}
+{\out (=> (<= 0  (F_c) )  (=> (<= 0  (F_b) )  (=> (<= 0  (F_a) )}
+{\out   (=> (AND (<= {* 3  (F_a) }  {+ {+ 2  {* 4  (F_b) } }  }
+{\out {* 6  (F_c) } } )  (AND (<= 11  {+ {+ {* 2  (F_a) }  (F_b) }}
+{\out   {* 2  (F_c) } } )  (<= {+ (F_a)  {* 3  (F_b) } }  {+ 5  }
+{\out {* 2  (F_c) } } ) ) )  (< {+ 2  {* 3  (F_b) } }  {+ 1  {+ }
+{\out {* 2  (F_a) }  {* 6  (F_c) } } } ) ) ) ) ) }
+{\out SVC Returns:}
+{\out VALID}
+{\out Level 1}
+{\out #3 * a <= #2 + #4 * b + #6 * c &}
+{\out #11 <= #2 * a + b + #2 * c & a + #3 * b <= #5 + #2 * c -->}
+{\out #2 + #3 * b <= #2 * a + #6 * c}
+{\out No subgoals!}
+\end{ttbox}
+
+
+\begin{warn}
+Calling \ttindex{svc_tac} entails an above-average risk of
+unsoundness.  Isabelle does not check SVC's result independently.  Moreover,
+the tactic translates the submitted formula using code that lies outside
+Isabelle's inference core.  Theorems that depend upon results proved using SVC
+(and other oracles) are displayed with the annotation \texttt{[!]} attached.
+You can also use \texttt{\#der (rep_thm $th$)} to examine the proof object of
+theorem~$th$, as described in the \emph{Reference Manual}.  
+\end{warn}
+
+To start, first download SVC from the Internet at URL
+\begin{ttbox}
+http://agamemnon.stanford.edu/~levitt/vc/index.html
+\end{ttbox}
+and install it using the instructions supplied.  SVC requires two environment
+variables:
+\begin{ttdescription}
+\item[\ttindexbold{SVC_HOME}] is an absolute pathname to the SVC
+    distribution directory. 
+    
+  \item[\ttindexbold{SVC_MACHINE}] identifies the type of computer and
+    operating system.  
+\end{ttdescription}
+You can set these environment variables either using the Unix shell or through
+an Isabelle \texttt{settings} file.  Isabelle assumes SVC to be installed if
+\texttt{SVC_HOME} is defined.
+
+\paragraph*{Acknowledgement.}  This interface uses code supplied by S{\o}ren
+Heilmann.
+
+
+\index{SVC decision procedure|)}
+
+
+
+
 \section{Types}\label{sec:HOL:Types}
 This section describes \HOL's basic predefined types ($\alpha \times
 \beta$, $\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for