# HG changeset patch
# User paulson
# Date 837090038 -7200
# Node ID 763f08fb194fea7b09d1d943198dee767e0b200b
# Parent  afa622bc829d1fc9fd24dc34a8f683ee4097988e
Documentation of oracles and their syntax

diff -r afa622bc829d -r 763f08fb194f doc-src/Ref/theories.tex
--- a/doc-src/Ref/theories.tex	Fri Jul 05 14:22:59 1996 +0200
+++ b/doc-src/Ref/theories.tex	Thu Jul 11 15:00:38 1996 +0200
@@ -124,6 +124,10 @@
 \item[$constdefs$] combines the declaration of constants and their
   definition. The first $string$ is the type, the second the definition.
 
+\item[$oracle$] links the theory to a trusted external reasoner.  It is
+  allowed to create theorems, but each theorem carries a proof object
+  describing the oracle invocation.  See \S\ref{sec:oracles} for details.
+
 \item[$ml$] \index{*ML section}
   consists of \ML\ code, typically for parse and print translation functions.
 \end{description}
@@ -916,4 +920,102 @@
 decomposes $cT$ as a record containing the type itself and its signature.
 \end{ttdescription}
 
+
+\section{Oracles: calling external reasoners }
+\label{sec:oracles}
+\index{oracles|(}
+
+Oracles allow Isabelle to take advantage of external reasoners such as
+arithmetic decision procedures, model checkers, fast tautology checkers or
+computer algebra systems.  Invoked as an oracle, an external reasoner can
+create arbitrary Isabelle theorems.  It is your responsibility to ensure that
+the external reasoner is as trustworthy as your application requires.
+Isabelle's proof objects~(\S\ref{sec:proofObjects}) record how each theorem
+depends upon oracle calls.
+
+\begin{ttbox}
+     invoke_oracle : theory * Sign.sg * exn -> thm
+     set_oracle    : Sign.sg -> typ -> string
+\end{ttbox}
+\begin{ttdescription}
+\item[\ttindexbold{invoke_oracle} ($thy$, $sign$, $exn$)] invokes the oracle
+  of theory $thy$ passing the information contained in the exception value
+  $exn$ and creating a theorem having signature $sign$.  Errors arise if $thy$
+  does not have an oracle, if the oracle rejects its arguments or if its
+  result is ill-typed.
+
+\item[\ttindexbold{set_oracle} $fn$ $thy$] sets the oracle of theory $thy$ to
+  be $fn$.  It is seldom called explicitly, as there is syntax for oracles in
+  theory files.  A theory can have at most one oracle.
+\end{ttdescription}
+
+A curious feature of {\ML} exceptions is that they are ordinary constructors.
+The {\ML} type {\tt exn} is a datatype that can be extended at any time.  (See
+my {\em {ML} for the Working Programmer}~\cite{paulson-ml2}, especially
+page~136.)  The oracle mechanism takes advantage of this to allow an oracle to
+take any information whatever.
+
+There must be some way of invoking the external reasoner from \ML, either
+because it is coded in {\ML} or via an operating system interface.  Isabelle
+expects the {\ML} function to take two arguments: a signature and an
+exception.
+\begin{itemize}
+\item The signature will typically be that of a desendant of the theory
+  declaring the oracle.  The oracle will use it to distinguish constants from
+  variables, etc., and it will be attached to the generated theorems.
+
+\item The exception is used to pass arbitrary information to the oracle.  This
+  information must contain a full description of the problem to be solved by
+  the external reasoner, including any additional information that might be
+  required.  The oracle may raise the exception to indicate that it cannot
+  solve the specified problem.
+\end{itemize}
+
+A trivial example is provided on directory {\tt FOL/ex}.  This oracle
+generates tautologies of the form $P\bimp\cdots\bimp P$, with an even number
+of $P$s. 
+
+File {\tt declIffOracle.ML} begins by declaring a new exception constructor
+for the oracle the information it requires: here, just an integer.  It
+contains some code (suppressed below) for creating the tautologies, and
+finally declares the oracle function itself:
+\begin{ttbox}
+exception IffOracleExn of int;
+\(\vdots\)
+fun mk_iff_oracle (sign, IffOracleExn n) = 
+    if n>0 andalso n mod 2 = 0 
+    then Trueprop $ mk_iff n
+    else raise IffOracleExn n;
+\end{ttbox}
+Observe the function two arguments, the signature {\tt sign} and the exception
+given as a pattern.  The function checks its argument for validity.  If $n$ is
+positive and even then it creates a tautology containing $n$ occurrences
+of~$P$.  Otherwise it signals error by raising its own exception.  Errors may
+be signalled by other means, such as returning the theorem {\tt True}.
+Please ensure that the oracle's result is correctly typed; Isabelle will
+reject ill-typed theorems by raising a cryptic exception at top level.
+
+The theory file {\tt IffOracle.thy} packages up the function above as an
+oracle.  The first line indicates that the new theory depends upon the file
+{\tt declIffOracle.ML} (which declares the {\ML} code) as well as on \FOL.
+The second line informs Isabelle that this theory has an oracle given by the
+function {\tt mk_iff_oracle}.
+\begin{ttbox}
+IffOracle = "declIffOracle" + FOL +
+oracle mk_iff_oracle
+end
+\end{ttbox}
+Because a theory can have at most one oracle, the theory itself serves to
+identify the oracle.
+
+Here are some examples of invoking the oracle.  An argument of 10 is allowed,
+but one of 5 is forbidden:
+\begin{ttbox}
+invoke_oracle (IffOracle.thy, sign_of IffOracle.thy, IffOracleExn 10);
+{\out  "P <-> P <-> P <-> P <-> P <-> P <-> P <-> P <-> P <-> P" : thm}
+invoke_oracle (IffOracle.thy, sign_of IffOracle.thy, IffOracleExn 5); 
+{\out Exception- IffOracleExn 5 raised}
+\end{ttbox}
+
+\index{oracles|)}
 \index{theories|)}
diff -r afa622bc829d -r 763f08fb194f doc-src/Ref/theory-syntax.tex
--- a/doc-src/Ref/theory-syntax.tex	Fri Jul 05 14:22:59 1996 +0200
+++ b/doc-src/Ref/theory-syntax.tex	Thu Jul 11 15:00:38 1996 +0200
@@ -36,6 +36,7 @@
         | trans
         | defs
         | rules
+        | oracle
         ;
 
 classes : 'classes' ( ( id (  ()
@@ -100,6 +101,9 @@
 defs : 'defs' (( id string ) + )
      ;
 
+oracle : 'oracle' name
+       ;
+
 ml : 'ML' text
    ;
 
diff -r afa622bc829d -r 763f08fb194f doc-src/Ref/thm.tex
--- a/doc-src/Ref/thm.tex	Fri Jul 05 14:22:59 1996 +0200
+++ b/doc-src/Ref/thm.tex	Thu Jul 11 15:00:38 1996 +0200
@@ -652,7 +652,7 @@
 \index{meta-rules|)}
 
 
-\section{Proof objects}
+\section{Proof objects}\label{sec:proofObjects}
 \index{proof objects|(} Isabelle can record the full meta-level proof of each
 theorem.  The proof object contains all logical inferences in detail, while
 omitting bookkeeping steps that have no logical meaning to an outside