Commit 03541962 authored by MARCHE Claude's avatar MARCHE Claude

completed doc on ITPs and Isabelle

parent 4e4f7272
......@@ -3,22 +3,48 @@
\index{Isabelle proof assistant}
When using Isabelle from Why3, files generated from Why3 theories and
goals are stored in a dedicated XML format. Those files should not be
edited. Instead, the proofs must be completed in a file with the same
name and extension \texttt{.thy}. This is the file that is opened when
using ``Edit'' action in \texttt{why3ide}.
\subsection{Installation}
You need version Isabelle2013-2.
You need version Isabelle2013-2. Former versions are not supported.
\todo{put ... in ... etc/components}
Isabelle must be installed before compiling Why3. After compilation
and installation of Why3, you must manually add the path
\begin{verbatim}
<Why3 lib dir>/isabelle
\end{verbatim}
into either the user file
\begin{verbatim}
.isabelle/Isabelle2013-2/etc/components
\end{verbatim}
or the system-wide file
\begin{verbatim}
<Isabelle install dir>/etc/components
\end{verbatim}
\subsection{Usage}
\todo{Explain Isabelle/jedit server interaction}
When using Isabelle, files generated from Why3 theories are stored in
a dedicated XML format. Those files should not be edited. Instead,
realizations must be designed in some \texttt{.thy} as follows.
The most convenient way to call Isabelle for discharging a Why3 goal
is to start the Isabelle/jedit interface in server mode. In this mode,
one must start the server once, before launching \texttt{why3ide},
using
\begin{verbatim}
isabelle why3_jedit
\end{verbatim}
Then, inside a \texttt{why3ide} session, any use of ``Edit'' will
transfer the file to the already opened instance of jEdit. When the
proof is completed, the user must send back the edited proof to
\texttt{why3ide} by closing the opened buffer, typically by hitting
\texttt{Ctrl-w}.
\subsection{Realizations}
Realizations must be designed in some \texttt{.thy} as follows.
The realization file corresponding to some Why3 file \url{f.why}
should have the following form.
\begin{verbatim}
......@@ -40,7 +66,6 @@ why3_vc <some other lemma> by proof
why3_end
\end{verbatim}
See directory \url{lib/isabelle} for examples.
......
\chapter{Interactive Proof Assistants}
\section{Using an Interactive Proof Assistant from \why}
\todo{expliquer les principes}
% ... We then provide specific information about some ITPs.
... We then provide specific information about some ITPs.
\section{Using an Interactive Proof Assistant to Discharge Goals}
Instead of calling an automated theorem prover to discharge a goal,
\why offers the possibility to call an interactive theorem prover
instead. In that case, the interaction is decomposed into two distinct
phases:
\begin{itemize}
\item Edition of a proof script for the goal, typically inside a proof editor
provided by the external interactive theorem prover;
\item Replay of an existing proof script.
\end{itemize}
An example of such an interaction is given in the tutorial
section~\ref{sec:gui}.
Some proof assistants offer more than one possible editor, e.g. a
choice between the use of a dedicated editor and the use of the Emacs
editor and the ProofGeneral mode. Selection of the preferred mode can
be made in \texttt{why3ide} preferences, under the ``Editors'' tab.
\section{Theory Realizations}
\label{sec:realizations}
......@@ -16,7 +32,7 @@ some of its uninterpreted symbols and proofs for some of its
axioms. This way, one can show the consistency of an axiomatized
theory and/or make a connection to an existing library (of the proof
assistant) to ease some proofs.
Currently, realizations are supported for the proof assistants Coq and PVS.
%Currently, realizations are supported for the proof assistants Coq and PVS.
\subsection{Generating a realization}
......
\newcommand{\todo}[1]{{\Huge\bfseries TODO: #1}}
%\newcommand{\todo}[1]{{\Huge\bfseries TODO: #1}}
\newcommand{\why}{\textsf{Why3}\xspace}
\newcommand{\whyml}{\textsf{WhyML}\xspace}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment