author paulson Thu, 11 Jul 1996 15:00:38 +0200 changeset 1846 763f08fb194f parent 1845 afa622bc829d child 1847 58ab3b74a344
Documentation of oracles and their syntax
 doc-src/Ref/theories.tex file | annotate | diff | comparison | revisions doc-src/Ref/theory-syntax.tex file | annotate | diff | comparison | revisions doc-src/Ref/thm.tex file | annotate | diff | comparison | revisions
--- 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|)}
--- 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
;

--- 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