

% \documentstyle[12pt,fleqn,espcrc1,alltt]{article}
% \documentstyle[fleqn,wicsbook,alltt,fuzz]{article}
% \documentstyle[fleqn,wicsbook,alltt,zed]{article}

\documentstyle[fleqn,wicsbook,zed]{article}

% Last updated by Jonathan Bowen, 18 November 1993.

%%% Mike: please check lines starting with "%%%"


\title{\vspace{-3pc}\titlesize\bf Z and HOL}

\author{\footnotesize
% \hspace{-2mm}
\begin{tabular}[t]{@{}l}
{\large Jonathan Bowen} \\[1ex]
Oxford University\\
Computing Laboratory \\
%Programming Research Group \\
Wolfson Building \\
Parks Road \\
Oxford OX1 3QD \\
UK \\[1ex]
\footnotesize
Email: \verb"Jonathan.Bowen@comlab.ox.ac.uk"
\end{tabular}
% \hspace{-2mm}
\begin{tabular}[t]{l@{}}
{\large Mike Gordon} \\[1ex]
University of Cambridge \\
Computer Laboratory \\
New Museums Site \\
Pembroke Street \\
Cambridge CB2 3QG \\
UK \\[1ex]
\footnotesize
Email: \verb"Mike.Gordon@cl.cam.ac.uk"
\end{tabular}
\date{} }


% Definitions

\def\Z{{Z}}
\def\W{${\cal W}$}
\def\zedB{{\it zed}{\bf B}}
\def\HOL{{\rm\small HOL}}
\def\LCF{{\rm\small LCF}}
\def\ML{{\rm\small ML}}
\def\fuzz{{\large\it f\kern0.1em}{\normalsize\sc uzz}}

% ---------------------------------------------------------------------
% Macros for little HOL sessions displayed in boxes.
%
% Usage: (1) \setcounter{sessioncount}{1} resets the session counter
%
%        (2) \begin{session}\begin{verbatim}
%             .
%              < lines from hol session >
%             .
%            \end{verbatim}\end{session}
%
%            typesets the session in a numbered box.
% ---------------------------------------------------------------------

\newlength{\hsbw}
\setlength{\hsbw}{\textwidth}
\addtolength{\hsbw}{-\arrayrulewidth}
\addtolength{\hsbw}{-\tabcolsep}
\newcommand\HOLSpacing{9pt}

\newcounter{sessioncount}
\setcounter{sessioncount}{1}

\newenvironment{session}{\begin{flushleft}
 \vskip-1.5mm
 \begin{tabular}{@{}|c@{}|@{}}\hline
 \begin{minipage}[b]{\hsbw}
 \vspace*{-.5pt}
 \begin{flushright}
 \rule{0.01in}{.15in}\rule{0.3in}{0.01in}\hspace{-0.35in}
 \raisebox{0.04in}{\makebox[0.3in][c]{\small \thesessioncount}}
 \end{flushright}
 \vspace*{-.55in}
% Change the following from \small to make fit WICS style if necessary
 \begingroup\small\baselineskip\HOLSpacing}{\endgroup\end{minipage}\\
 \hline
 \end{tabular}
 \vskip-1.5mm
 \end{flushleft}
 \stepcounter{sessioncount}
 }

% ALLTT DOCUMENT-STYLE OPTION
% ` changed to be non-active

\makeatletter
\def\docspecials{\do\ \do\$\do\&%
  \do\#\do\^\do\^^K\do\_\do\^^A\do\%\do\~}

\def\alltt{\trivlist \item[]\if@minipage\else\vskip\parskip\fi
	\leftskip\@totalleftmargin\rightskip\z@
\parindent\z@\parfillskip\@flushglue\parskip\z@
\@tempswafalse \def\par{\if@tempswa\hbox{}\fi\@tempswatrue\@@par}
\obeylines \tt % \catcode``=13
% \@noligs
\let\do\@makeother \docspecials
 \frenchspacing\@vobeyspaces}

\let\endalltt=\endtrivlist
\makeatother



\begin{document}

\maketitle
\thispagestyle{empty}

% \tableofcontents


%%% New abstract - check you are happy with it.
%%% Tweaked by MJCG

\begin{abstract}

\noindent

\noindent A simple `shallow' semantic embedding of the \Z\ notation into the
\HOL\ logic is described. The \Z\ notation is based on set theory
and first order predicate logic.  The \HOL\ theorem proving system
supports higher order logic.  A well-known case study is used as a
running example. The presentation is intended to show people with some
knowledge of \Z\ how a tool such as \HOL\ can be used to provide
mechanical support for the notation, including mechanization of
proofs. No specialized knowledge of \HOL\ is assumed.

\end{abstract}


\section{Introduction}

\HOL\ \cite{HOL} is an `\LCF-style' theorem proving
environment \cite{EdinLCF,CamLCF} for classical higher order logic
\cite{Andrews,Church}. Proof tools for the formal specification
notation \Z\ \cite{Z:Brie92,Z:Spiv92} can be implemented by translating
\Z\ schemas into higher order logic and then programming schema
combining operations in \HOL's metalanguage \ML.\footnote{The ML
language was originally developed as part of LCF, but is now an
independent programming language in its own right \cite{StandardML}. It
is an eager-evaluation impure functional language with a polymorphic type
discipline.} This technique is known as {\it semantic embedding\/} (see
section~\ref{embed}) and has been pioneered by ICL for many years. They
have built their own `industrial strength' version of \HOL, called
ProofPower \cite{ProofPower}, and implemented sophisticated proof tools
for \Z\ on top of it (see section~\ref{other} for more on ProofPower and other
proof tools for \Z).

This paper is intended to be an accessible introduction to support for
\Z\ by semantic embedding. It is intended for readers familiar with \Z,
but not with \HOL. The techniques described here use ordinary \HOL\
and are simpler and less powerful than those found in ProofPower. In
the next section a familiar Z specification example, Spivey's `birthday
book', is used to illustrate how \HOL\ can support \Z. Subsequent
sections discuss how this support is achieved.


\section{The Birthday Book}\label{birthdaybook}

It is assumed that readers are reasonably familiar with the
birthday book example in Chapter~1 of Spivey's {\it The \Z\
Notation: A Reference Manual\/} \cite{Z:Spiv92} (also to be found in
\cite{Z:Spiv89b}), henceforth called ZRM. The schemas from
this specification are included here for comparison with their \HOL\
equivalents.

The numbered boxes that follow show a \HOL\ session in which the
birthday book is input and some simple facts are proved. The \HOL\
system prompts for input with {\verb"#"}, so all lines beginning with
this symbol are supplied by the user. All other lines are generated
by \HOL{}. The sessions have been edited to remove some output and to
suppress details of some user-supplied theorem proving tactics, which
will only be comprehensible to readers familiar with \HOL.\footnote{The
complete input to HOL for the Birthday Book and other examples is
available in the directory {\verb+contrib/Examples+} distributed with
HOL88, Version 2.02.  Details of HOL 
(including how to get it) are available from an
on-line networked hypertext documentation
service 
run by the Laboratory for Applied Logic at Brigham Young University.
To browse this documentation, first obtain the XMosaic
tool (connect to
{\verb+ftp.ncsa.uiuc.edu+} by anonymous FTP, then the directory
{\verb+/Mosaic/xmosaic-binaries+} contains compiled copies of the
latest version of XMosaic for a variety of architectures).
To connect to the HOL documentation server 
select {\tt OPEN} from the XMosaic menu and enter
{\verb+http://lal.cs.byu.edu/lal/hol-documentation.html+}.}
Before the session starts \HOL{} is run and the \Z{} support package loaded. This package
is a collection of \ML{} declarations together with a theory {\verb+Z+} containing definitions to
support \Z\ operators and its `Mathematical Tool-kit' (see
section~\ref{zops}). Details of this loading are omitted here.

The first interaction of the session is shown in box~1 below. A
new theory called {\verb"BirthdayBook"} is started. Theories contain
definitions and theorems that the user has proved. They are stored in
a hierarchical database on disk. The \ML\ command {\verb"new_theory"}
starts a new theory with a user-supplied name.


\begin{session}\begin{verbatim}

#new_theory `BirthdayBook`;;
\end{verbatim}\end{session}

This interaction initiates the specification of the Birthday Book by
starting a new \HOL\ theory called {\verb"BirthdayBook"}.  Note that
in the version of \ML\ (Classic~\ML) provided by \HOL 88 (which is the version
of \HOL{} used here) user input is terminated with {\verb+;;+} (in
Standard \ML\ the terminator is a single semi-colon).


The first definition in this theory introduces
two sets:

\begin{zed}
  [~ NAME, DATE ~]
\end{zed}

\noindent
The corresponding declaration in \HOL\ uses an \ML\ function
{\verb"sets"}.

\begin{session}\begin{verbatim}

#sets `NAME DATE`;;
\end{verbatim}\end{session}

With this second interaction the two sets {\tt NAME} and {\tt DATE} are declared.

The first schema in the Birthday Book defines the abstract state and an
`invariant' on that state:

\begin{schema}{BirthdayBook}
  known    : \power NAME \\
  birthday : NAME \pfun DATE
\where
  known = \dom birthday
\end{schema}

\noindent
The declaration of schemas in \HOL\ uses a notation that is
intended to make it clear what the corresponding \Z\ is. This is shown in
box~3 below.

\begin{session}\begin{verbatim}

#declare
# `BirthdayBook`
# "SCHEMA
#   [known :: (P NAME);
#    birthday :: (NAME -+> DATE)]
#   %---------------------------%
#   [known = dom birthday]";;
\end{verbatim}\end{session}

This third interaction illustrates the format (shown on lines
starting with {\verb"#"}) used to input \Z{} schemas to \HOL.  A preprocessor
converts the input format to a \HOL\ term that represents the
semantics of the corresponding schema. This preprocessor could in
principle be a complete parser for \Z\ notation,\footnote{HOL
libraries provide syntax processing utilities that enable custom
parsers and pretty-printers to be generated.} but in keeping with our
`lightweight' approach this has not been done (ICL's ProofPower tool
supports proper
\Z\ syntax). The aim has been to have an input format that is readable
as both \Z\ and \HOL.

The powerset operator {\tt P} and infix partial function operator
{\verb"-+>"} are defined in the theory {\tt Z}, which implements (part
of) the \Z\ mathematical tool-kit; see section~\ref{zops} for more
details.

The \ML\ function {\verb"declare"} converts the term
{\verb+"SCHEMA+}$~\cdots${\verb+"+} that follows it into the \HOL\
representation of the schema, remembers the declaration (and the types
of declared variables) in a global data structure and returns the
schema representation.

The \HOL\ representation of a schema of the form:

%%unchecked
\begin{schema}{~\ldots~}
  x_1 \hspace{1mm}   : S_1 \\
  x_2 \hspace{1mm}   : S_2 \\
\hspace{5.2mm}\vdots\\
  x_m    : S_m
\where
  P_1\\
  P_2\\
\hspace{1mm}\vdots\\
 P_n
\end{schema}

\noindent
is semantically equivalent to the formula:

\[
x_1 \in S_1 \wedge x_2 \in S_2 \wedge \ldots \wedge x_m \in S_m \wedge
  P_1 \wedge P_2 \wedge \ldots \wedge P_n
\]

\noindent
which in \HOL\ notation is written as:

\begin{alltt}
\(x\sb{1}\) IN \(S\sb{1}\) \verb"/\" \(x\sb{2}\) IN \(S\sb{2}\) \verb"/\" \(\ldots\) \verb"/\" \(x\sb{m}\) IN \(S\sb{m}\) \verb"/\" \(P\sb{1}\) \verb"/\" \(P\sb{2}\) \verb"/\" \(\ldots\) \verb"/\" \(P\sb{n}\)
\end{alltt}

\noindent
where $S_i$ is a \HOL\ term denoting a set and $P_1, \ldots, P_n$ are
Boolean terms constituting the schema's predicate. The infix
operators {\verb"IN"} and {\verb"::"} both denote the set membership
relation. The former is used for general set membership in predicates
(e.g.~to represent $\in$), the latter for type membership assertions
(e.g.~in the declaration part of schemas, where \Z\ would have a
colon). Note that schema operations can move type
membership assertions from the declaration part of schemas into the
predicate part, thus automatically generated assertions of the form
$x{\verb+::+}S$ may appear in the predicate parts of schemas.

The actual semantic representation is not the conjunction shown above,
but the logically equivalent term:

\begin{alltt}
   SCHEMA [\(x\sb{1}\) :: \(S\sb{1}\); \(x\sb{2}\) :: \(S\sb{2}\); \(\ldots\) ;\(x\sb{m}\) :: \(S\sb{m}\)]
          [\(P\sb{1}\); \(P\sb{2}\); \(\ldots\) ; \(P\sb{n}\)]
\end{alltt}

\noindent where {\tt SCHEMA} is defined (in the theory {\tt Z}) by:

\begin{alltt}
   SCHEMA [\(d\sb{1}\); \(\ldots\) ;\(d\sb{m}\)] [\(P\sb{1}\); \(\ldots\) ;\(P\sb{n}\)]  =
    \(d\sb{1}\) \verb"/\" \(\ldots\)  \verb"/\" \(d\sb{m}\) \verb"/\" \(P\sb{1}\) \verb"/\" \(\ldots\)  \verb"/\" \(P\sb{n}\)
\end{alltt}

\noindent This representation is more convenient as the conjuncts
corresponding to the declaration and predicate parts of the schema can
be easily extracted.

\HOL\ input will usually be laid out in the following `\Z-style'
format:

\begin{alltt}
   SCHEMA
    [\(x\sb{1}\) \hspace{1.3mm}:: \(S\sb{1}\);
     \(x\sb{2}\) \hspace{1.3mm}:: \(S\sb{2}\);
         \(\vdots\)
     \(x\sb{m}\) :: \(S\sb{m}\)]
    %---------%
    [\(P\sb{1}\);
     \(P\sb{2}\);
\hspace{1mm}     \(\vdots\)
     \(P\sb{n}\)]
\end{alltt}

\noindent where the line {\verb"%--"}$\cdots${\verb"--%"} is just a
comment to aid the eye (comments in \ML\ are enclosed between percent
symbols).

The next schema illustrates schema inclusion and the $\Delta$ change of
state schema convention. First the \Z:

\begin{schema}{AddBirthday}
  \Delta BirthdayBook \\
  name? : NAME \\
  date? : DATE
\where
  name? \notin known
\also
  birthday' = birthday \cup \{name? \mapsto date?\}
\end{schema}

\noindent The corresponding \HOL\ is:

\begin{session}\begin{verbatim}

#declare
# `AddBirthday`
# "SCHEMA
#   [DELTA BirthdayBook;
#    name? :: NAME;
#    date? :: DATE]
#   %--------------------------------------------%
#   [~(name? IN known);
#    birthday' = birthday UNION {name? |-> date?}]";;
\end{verbatim}\end{session}

The symbol {\verb"~"}
represents negation ($\neg$) in \HOL.  Normally schemas are printed out as
their name, but this default can be changed so that the semantic
representations of schemas are printed in full.  This mode is entered
by evaluating the \ML\ expression {\verb"show_schemas true"}.

\begin{session}\begin{verbatim}

#"BirthdayBook";;
"BirthdayBook" : term

#show_schemas true;;

#"BirthdayBook";;
"SCHEMA
 [known :: (P NAME);
  birthday :: (NAME -+> DATE)]
 [known = dom birthday]" : term

#"AddBirthday";;
"SCHEMA
 [known :: (P NAME);
  birthday :: (NAME -+> DATE);
  known' :: (P NAME);
  birthday' :: (NAME -+> DATE);
  name? :: NAME;date? :: DATE]
 [known = dom birthday;
  known' = dom birthday';
  ~name? IN known;
  birthday' = birthday UNION {name? |-> date?}]"

\end{verbatim}\end{session}


Note how the schema inclusion {\tt DELTA~BirthdayBook} (which represents
\Z's $\Delta BirthdayBook$) results in extra primed variables being
added to the declaration of {\tt AddBirthday}, and appropriate
instances of the predicate part of {\tt BirthdayBook} being included
in the predicate of {\tt AddBirthday}. More details of how {\tt
DELTA}-expansion is implemented can be found in section~\ref{io}.

As a check, the precondition of {\tt AddBirthday} can be computed and
simplified using a theorem proving tool called {\tt simp}.  The
precondition of an operation schema is the condition on the state that
must hold if the operation is to be applicable.  See page 77 of
\cite{Z:Spiv92}, page 151 of \cite{Z:Pott90} and page 141 of
\cite{Z:Dill90} for further discussions of this. For example, here is
the computation of the precondition of $AddBirthday$:

\begin{session}\begin{verbatim}

#show_schemas false;;

#simp "pre AddBirthday";;
known :: (P NAME), 
birthday :: (NAME -+> DATE), 
name? :: NAME, 
date? :: DATE, 
(dom(birthday UNION {name? |-> date?})) :: (P NAME), 
(birthday UNION {name? |-> date?}) :: (NAME -+> DATE) 
|- pre AddBirthday = (known = dom birthday) /\ ~name? IN (dom birthday)
\end{verbatim}\end{session}

\noindent
The evaluation of {\verb+simp "pre AddBirthday"+} results in a
theorem asserting that the precondition of $AddBirthday$ is 
$known = \dom birthday \land name? \notin \dom birthday$. 

Theorems are a special datatype in \ML,
values of which can only be created by applying sequences of inference
rules to axioms (or previously proved theorems) \cite{EdinLCF,HOL}.  A
theorem $t_1${\verb","}$\ldots${\verb","}$t_n${\verb" |- "}$t$ asserts
that the term $t$ follows from the conjunction of the terms $t_1$,
$\ldots$ , $t_n$.

In the example above, the terms before the turnstile {\verb"|-"} are
type inclusion assumptions used by {\verb"simp"} in simplifying
{\verb"pre AddBirthday"}. The function {\tt simp} uses some simple
heuristics (e.g.~the `One Point Rule' \cite{Z:Pott90}, which is
implemented in the {\verb"unwind"} library), to simplify the supplied
term. The heuristics are adequate here, but not for more complex
examples (see {\tt RAddBirthday} below).  Special purpose theorem
proving tools like {\tt simp} are easy for users to implement for
themselves in \ML.

Sets are regarded as primitive in \Z, but in \HOL\ they must be
defined. Fortunately, \HOL's {\tt sets} library defines a type of
sets and the usual operations of set theory. It also defines the set
comprehension notation:
$${\verb"{"}~E[x_1,\cdots,x_n]~{\verb"|"}~P[x_1,\cdots,x_n]~{\verb"}"}$$
which is equivalent to:
$${\verb"{"}~x~{\verb"|"}~\exists x_1\cdots x_n.~ x =
 E[x_1,\cdots,x_n] ~\wedge~ P[x_1,\cdots,x_n]~{\verb"}"}$$
Thus the \Z\ set comprehension notation $\{S\spot E\}$ is translated
into $\{E\mid S\}$ in \HOL. It would be possible to support \Z's
comprehension notation directly, but as the translation is so direct
this has not been done.

The theory {\tt Z} provides the definitions of some of the set
theoretic operators in \Z\ and its mathematical toolkit. For example,
\Z\ functions are a special case of relations:
\[
\begin{array}{@{}lll}
X \rel  Y & = & \power(X \cross Y)
\also
X \pfun Y & = & \{f : X \rel Y \mid (\forall x : X; y_1,y_2:Y\spot\\
&& \t2
(x\mapsto y_1)\in f \land (x\mapsto y_2)\in f \implies y_1 = y_2)\}
\end{array}
\]
The corresponding \HOL\ definitions are:

\begin{verbatim}
   X <-> Y  =  P(X >< Y)
   X -+> Y  =  {f | f IN (X <-> Y) /\ (!x y1 y2.
                (x|->y1) IN f /\ (x|->y2) IN f ==> (y1 = y2))}
\end{verbatim}

\noindent where {\verb"!"} is \HOL's notation for the universal
quantifier $\forall$. These definitions are `generic': {\verb"X"} and
{\verb"Y"} range over sets of arbitrary elements. In the \HOL\ logic
functions are a primitive concept and unlike in \Z\ are not regarded as
certain kinds of sets. The \HOL\ notation $f${\tt (}$x${\tt )}, which
can also be written without brackets as just $f~x$, denotes the
application of the logical function $f$ to argument $x$. If $f$ is a set
of ordered pairs, then this is not a well-formed \HOL\ term -- only
logical functions can be applied to arguments. To get around this
problem occurrences of $f${\tt (}$x${\tt )}, where $f$ has been
previously declared to be a function graph, are preprocessed to
$f${\verb"^^"}$x$, where {\verb"^^"} is an infix operator for `applying'
sets defined in the theory {\tt Z} (see section~\ref{zops}).

The specification presented so far can be further tested by proving 
the property discussed on page 5 of ZRM. In \Z\ notation this is:

\[
  AddBirthday \vdash known' = known \cup \{name?\}
\]

\noindent
In \HOL\ the proof proceeds as follows:

\begin{session}\begin{alltt}

#prove_theorem
# (`known_UNION`,
#  "[AddBirthday] |-? (known' = known UNION {name?})",
#  REWRITE_ALL_TAC[SCHEMA;CONJL;dom_UNION;dom_SING]);;

known_UNION = AddBirthday |- known' = known UNION {name?}

\end{alltt}\end{session}

The input has the form
\verb"prove_theorem("$name$\verb","$goal$\verb","$tactic$\verb")". This
instructs \HOL\ to try to prove $goal$ using $tactic$.  A goal of the
form {\verb"["}$t_1${\verb";"}$\ldots${\verb";"}$t_n${\verb"] |-? "}$t$
is solved if $tactic$ proves the theorem
$t_1${\verb","}$\ldots${\verb","}$t_n${\verb" |- "}$t$.  A goal just
consisting of a term $t$ has no assumptions and is solved if $tactic$
proves the theorem {\verb" |- "}$t$ (see the example in box~18 below).

The tactic used above rewrites the goal and assumptions with the
definitions of {\tt SCHEMA} and {\tt CONJL} (see section~\ref{zops}) and
also with the following two laws (which are pre-proved in the theory
{\tt Z}, see section~\ref{zops}).

\begin{verbatim}
   dom_UNION  |- dom(X UNION Y) = (dom X) UNION (dom Y)
   dom_SING   |- dom{x |-> y}   = {x}
\end{verbatim}

\noindent If the proof succeeds, as it does here, then the resulting
theorem value is bound to $name$ in the metalanguage \ML\ and may be
used subsequently.

\begin{session}\begin{verbatim}

#known_UNION;;
AddBirthday |- known' = known UNION {name?}

#show_schemas true;;

#known_UNION;;
SCHEMA
[known :: (P NAME);birthday :: (NAME -+> DATE);known' :: (P NAME);
 birthday' :: (NAME -+> DATE);name? :: NAME;date? :: DATE]
[known = dom birthday;
 known' = dom birthday';
 ~name? IN known;
 birthday' = birthday UNION {name? |-> date?}]
|- known' = known UNION {name?}

\end{verbatim}\end{session}

The next operation schema in the birthday book specification is:

\begin{schema}{FindBirthday}
  \Xi BirthdayBook \\
  name? : NAME \\
  date! : DATE
\where
  name? \in known
\also
  date! = birthday(name?)
\end{schema}

\noindent This uses the $\Xi$ (no change
of state) convention in the declaration.

\begin{session}\begin{verbatim}

#declare
# `FindBirthday`
# "SCHEMA
#   [XI BirthdayBook;
#    name? :: NAME;
#    date! :: DATE]
#   %-----------------------%
#   [name? :: known;
#    date! = birthday(name?)]";;

\end{verbatim}\end{session}

\noindent The schema {\tt FindBirthday} is expanded out 
to a term logically equivalent to:

\begin{verbatim}
   SCHEMA
    [known :: (P NAME);
     birthday :: (NAME -+> DATE);
     known' :: (P NAME);
     birthday' :: (NAME -+> DATE);
     name? :: NAME;
     date! :: DATE]
    [known = dom birthday;
     known' = known;
     birthday' = birthday;
     name? :: known;
     date! = birthday ^^ name?]" : term
\end{verbatim}

\noindent The actual expansion is described in section~\ref{io}.

A second lemma to check the specification can now be proved. In \Z\
notation it is:

\[
  (AddBirthday \semi FindBirthday) \vdash (date! = date?)
\]

\noindent
This checks that a subsequent $FindBirthday$ operation results in the
same date for a given name as that provided by a previous $AddBirthday$
operation.

The hypothesis is the sequential composition of two schemas. This
illustrates the shallowness of the embedding of \Z. The composition of
schemas is computed when they are input by the preprocessor: {\tt SEQ}
acts like a macro. With a {\em deep embedding} (see
section~\ref{embed}) the composition operator {\tt SEQ} would have to
be defined in the object logic.


\begin{session}\begin{alltt}

#prove_theorem
# (`SEQ_AddBirthday_FindBirthday`,
#  "[AddBirthday SEQ FindBirthday] |-? (date! = date?)",
#  REWRITE_ALL_TAC[SCHEMA;CONJL]
#   THEN POP_ASSUM STRIP_ASSUME_TAC
#   THEN SMART_ELIMINATE_TAC
#   THEN IMP_RES_TAC Ap_UNION2
#   THEN ASM_REWRITE_TAC[]);;

SEQ_AddBirthday_FindBirthday = 
SCHEMA
[known :: (P NAME);birthday :: (NAME -+> DATE);known' :: (P NAME);
 birthday' :: (NAME -+> DATE);name? :: NAME;
 date? :: DATE;date! :: DATE]
[?known'' birthday''.
  (known'' :: (P NAME) \verb"/\" birthday'' :: (NAME -+> DATE)) \verb"/\"
  (known = dom birthday) \verb"/\"
  (known'' = dom birthday'') \verb"/\"
  ~name? IN known \verb"/\"
  (birthday'' = birthday UNION {name? |-> date?}) \verb"/\"
  (known'' = dom birthday'') \verb"/\"
  (known' = dom birthday') \verb"/\"
  ((`birthday`,birthday'),`known`,known' =
   (`birthday`,birthday''),`known`,known'') \verb"/\"
  name? :: known'' \verb"/\"
  (date! = birthday'' ^^ name?)] 
|- date! = date?

\end{alltt}\end{session}

\noindent The symbol {\verb"?"} is \HOL's notation for the universal
quantifier $\exists$. Iterated quantifications of the form 
$Q~x_1\cdots x_n${\verb"."}$t$ and $Q~x_1\cdots x_n${\verb"::"}$S${\verb"."}$t$ 
are allowed (where $Q$ is either {\verb"!"} or {\verb"?"}).

The tactic above has the form $tac_1~{\tt THEN}~tac_2~{\tt
THEN}~tac_3~{\tt THEN}~tac_5~{\tt THEN}~tac_5$, which instructs
\HOL\ to apply $tac_1 \ldots tac_5$ in that order:

\begin{itemize}

\item$tac_1$ rewrites the goal with the definitions of {\tt SCHEMA} and
{\tt CONJL};

\item $tac_2$ simplifies and `explodes' the assumption; 

\item $tac_3$ is {\verb"SMART_ELIMINATE_TAC"} which removes redundant
assumptions (it was contributed \footnote{HOL is distributed with both
a library and a {\tt contrib} directory.  The former contains uniformly
documented material; the latter contains less formal contributions
including {\tt SMART\_ELIMINATE\_TAC}.} by Donald Syme of the
Australian National University);

\item $tac_4$ tries to combine the preproved law {\verb"Ap_UNION2"}
with assumptions using Modus Ponens, where {\verb"Ap_UNION2"} is:
\begin{verbatim}
   |-  ~x IN (dom X) ==> ((X UNION {x |-> v}) ^^ x = v)
\end{verbatim}

\item $tac_5$ rewrites with all the current assumptions (including any 
extra ones generated by $tac_4$).

\end{itemize}

Switching off schema printing causes the input form to be
reconstructed. (How this is done is explained in section~\ref{io}.)

\begin{session}\begin{verbatim}

#show_schemas false;;

#SEQ_AddBirthday_FindBirthday;;
AddBirthday SEQ FindBirthday |- date! = date?

\end{verbatim}\end{session}

The next two schemas given in ZRM ($Remind$ and $InitBirthdayBook$) do
not add anything new and are omitted.

The birthday book uses a `free set' called $REPORT$, defined in
\Z\ by:

\begin{zed}
  REPORT ::= ok \mid already\_known \mid not\_known
\end{zed}

\noindent Such definitions are supported in \HOL\ using a type
definition facility written by Tom Melham \cite{Melham} (which is
slightly repackaged for use with {\tt Z}).

\begin{session}\begin{verbatim}

#free_set `REPORT = ok | already_known | not_known`;;
\end{verbatim}\end{session}

\noindent Melham's package only supports a subset of \Z's free types.
A wider class is definable in Isabelle's ZF application using a
fixpoint method developed by Paulson \cite{paulson-fixedpt}. This
approach suggests a way of handling more of \Z's free types in \HOL;
see also \cite{Z:Smit92}.

Next a couple of routine schema declarations to handle success and error
conditions:

\begin{schema}{Success}
  result!: REPORT
\where
  result! = ok
\end{schema}

\begin{schema}{AlreadyKnown}
  \Xi BirthdayBook \\
  name? : NAME \\
  result! : REPORT
\where
  name? \in known
\also
  result! = already\_known
\end{schema}

\noindent These are input to \HOL\ by:

\begin{session}\begin{verbatim}

#declare
# `Success`
# "SCHEMA
#   [result! :: REPORT]
#   %-----------------%
#   [result! = ok]";;

\end{verbatim}\end{session}

\noindent and

\begin{session}\begin{verbatim}

#declare
# `AlreadyKnown`
# "SCHEMA
#   [XI BirthdayBook;
#    name? :: NAME;
#    result! :: REPORT]
#   %-----------------------%
#   [name? :: known;
#    result! = already_known]";;

\end{verbatim}\end{session}

The next schema in the birthday book uses schema conjunction and
disjunction:

\begin{zed}
  RAddBirthday \defs (AddBirthday \land Success) \lor AlreadyKnown
\end{zed}

The conjunction and disjunction of schemas is computed on input, just as
for the sequential composition {\tt SEQ}. {\tt AND} and {\tt OR} can be
regarded as macros.

\begin{session}\begin{verbatim}

#declare
# `RAddBirthday`
# "(AddBirthday AND Success) OR AlreadyKnown";;

"RAddBirthday" : term

#show_schemas true;;

#"RAddBirthday";;
"SCHEMA
 [known :: (P NAME);
  birthday :: (NAME -+> DATE);
  known' :: (P NAME);
  birthday' :: (NAME -+> DATE);
  name? :: NAME;
  date? :: DATE;
  result! :: REPORT]
 [(known = dom birthday) /\
  (known' = dom birthday') /\
  ~name? IN known /\
  (birthday' = birthday UNION {name? |-> date?}) /\
  (result! = ok) \/
  (known = dom birthday) /\
  (known' = known) /\
  (birthday' = birthday) /\
  name? :: known /\
  (result! = already_known)]" : term

\end{verbatim}\end{session}

\noindent
Note that in \HOL, {\verb"/\"} binds tighter than {\verb"\/"}, so the
body of this schema is a disjunction of conjunctions. It is easy to
prove it equivalent to:

\def\RAddBirthday{RAddBirthday}

\begin{schema}{\RAddBirthday}
  \Delta BirthdayBook \\
  name?   : NAME \\
  date?   : DATE \\
  result! : REPORT
\where
  (name? \notin known \land \\
\t1  birthday' = birthday \cup \{name? \mapsto date?\} \land \\
\t1  result! = ok) \lor\\
%\also
  (name? \in known \land \\
\t1  birthday' = birthday \land \\
\t1  result! = already\_known)
\end{schema}

\noindent
 From now on the tactics used to prove theorems will be omitted.

%%% I've made the following into a figure to help avoid bad page breaks.
%%% I think some tweaking may be necessary in the final version.
%%% MJCG has undone this!

%\begin{figure}

\begin{session}\begin{alltt}

#show_schemas false;;

#prove_theorem
# (`RAddBirthdayLemma`,
#  "(AddBirthday AND Success) OR AlreadyKnown =
#   SCHEMA
#    [DELTA BirthdayBook;
#     name? :: NAME;
#     date? :: DATE;
#     result! :: REPORT]
#    %-------------------------------------------------------%
#    [(~(name? IN known) \verb"/\"
#              (birthday' = birthday UNION {name? |-> date?}) \verb"/\"
#              (result! = ok)) \verb"\/"
#     (name? IN known \verb"/\"
#              (birthday' = birthday) \verb"/\"
#              (result! = already_known))]",
#  \(<omitted tactic>\) );;

RAddBirthdayLemma =
|- RAddBirthday =
   SCHEMA
   [known :: (P NAME);birthday :: (NAME -+> DATE);known' :: (P NAME);
    birthday' :: (NAME -+> DATE);name? :: NAME;date? :: DATE;
    result! :: REPORT]
   [known = dom birthday;known' = dom birthday';
    ~name? IN known \verb"/\"
    (birthday' = birthday UNION {name? |-> date?}) \verb"/\"
    (result! = ok) \/
    name? IN known \verb"/\"
    (birthday' = birthday) \verb"/\"
    (result! = already_known)]

\end{alltt}\end{session}

%\caption{Proof of logical equivalence in HOL.\label{lemma1}}
%\end{figure}

This proof confirms informal remarks made on page 9 of ZRM (page
10 in the first edition). Note that the left hand side of the
equation proved is printed as {\tt RAddBirthday} rather than as {\tt
(AddBirthday AND Success) OR AlreadyKnown}. This is because the former
is recognized as being defined equal to the latter. The right hand side
of the equation has not previously been given a name, so it is printed
out in full.

A further check on $RAddBirthday$ is to show that its precondition is
true. Unfortunately, {\tt simp} is not powerful enough:

\begin{session}\begin{verbatim}

#simp "pre RAddBirthday";;
known :: (P NAME), 
birthday :: (NAME -+> DATE), 
name? :: NAME, 
date? :: DATE 
|- pre RAddBirthday =
   (?known' birthday' result!.
     (known' :: (P NAME) /\
      birthday' :: (NAME -+> DATE) /\
      result! :: REPORT) /\
     ((known = dom birthday) /\
      (known' = dom birthday') /\
      ~name? IN known /\
      (birthday' = birthday UNION {name? |-> date?}) /\
      (result! = ok) \/
      (known = dom birthday) /\
      (known' = dom birthday') /\
      ((birthday' = birthday) /\ (known' = known)) /\
      name? :: known /\
      (result! = already_known)))

\end{verbatim}\end{session}

\noindent The heuristics employed by {\tt simp} cannot deal with the
existentially quantified disjunction. They could be improved to
work for this example, but sooner or later another example would crop
up that is not handled. What is required is user guided simplification.
This can be achieved in various ways, the approach illustrated here is
to prove that the precondition is true with a user-supplied tactic.

\begin{session}\begin{alltt}

#prove_theorem
# (`pre_RAddBirthday`,
#  "[BirthdayBook; sig RAddBirthday] |-? pre RAddBirthday",
#  \(<omitted tactic>\) );;

pre_RAddBirthday =  
BirthdayBook, sig RAddBirthday |- pre RAddBirthday

\end{alltt}\end{session}

\noindent The {\tt sig} of a schema consists of the type membership
statements of its variables.

\[
\verb"sig (SCHEMA ["x_1\verb"::"S_1\verb";"\ldots\verb";"x_n\verb"::"
  S_n\verb"] ["\cdots\verb"]) = "x_1\in S_1\land\ldots\land x_n\in S_n
\]

The last three schema definitions in the abstract specification of the
birthday book are $NotKnown$, $RFindBirthday$ and $RRemind$. These are
straightforward and are omitted here.

In section~1.5 of ZRM the operations and data structures of the
birthday book are implemented.  The concrete operation corresponding to
$BirthdayBook$ is $BirthdayBook1$, where:

\begin{schema}{BirthdayBook1}
  names : \nat_1 \fun NAME \\
  dates : \nat_1 \fun DATE \\
  hwm : \nat
\where
  \forall i, j : 1 \upto hwm \spot
    i \neq j \implies names(i) \neq names(j)
\end{schema}

The \HOL\ version of this uses the terms {\tt NN} and {\verb"NN_1"}
which denote the sets of natural numbers and strictly positive natural
numbers, respectively. The notation $m${\verb".."}$n$ denotes the set
of numbers in the closed interval $[m,n]$ (``{\verb".."}'' is a \HOL\
infix operator). \HOL{} allows restricted quantifications of the form
{\verb"!"}$x${\verb"::"}$S${\verb"."}$t$ 
and {\verb"?"}$x${\verb"::"}$S${\verb"."}$t$
(where $S$
is a term denoting a set), which are equivalent
to {\verb"!"}$x${\verb"."}$x~${\tt IN}$~S${\verb" ==> "}$t$ and
{\verb"?"}$x${\verb"."}$x~${\tt IN}$~S${\verb" /\ "}$t$, respectively.
The infix operator
{\verb"-->"} is defined in the theory {\tt Z} and constructs the set of
total functions.

Using these notations, the \Z\ schema above is input into \HOL\ as:

\begin{session}\begin{verbatim}

#declare
# `BirthdayBook1`
# "SCHEMA
#   [names :: (NN_1-->NAME);
#    dates :: (NN_1-->DATE);
#    hwm :: NN]
#   %---------------------------------------------------%
#   [!i j::(1..hwm). ~(i = j) ==> ~(names(i) = names(j))]";;

\end{verbatim}\end{session}

The relation between $BirthdayBook$ and its implementation
$BirthdayBook1$ is specified with the schema $Abs$:

\begin{schema}{Abs}
  BirthdayBook \\
  BirthdayBook1
\where
  known = \{~ i : 1 \upto hwm \spot names(i) ~\}
\also
  \forall i : 1 \upto hwm \spot
    birthday(names(i)) = dates(i)
\end{schema}

\noindent The \HOL\ version is:

\begin{session}\begin{verbatim}

#declare
# `Abs`
# "SCHEMA
#   [BirthdayBook;
#    BirthdayBook1]
#   %-------------------------------------------%
#   [known = {names(i) | i::(1..hwm)};
#    !i::(1..hwm). birthday(names(i)) = dates(i)]";;

\end{verbatim}\end{session}

The implementation of $AddBirthday$ is $AddBirthday1$, where:

\begin{schema}{AddBirthday1}
  \Delta BirthdayBook1 \\
  name? : NAME \\
  date? : DATE
\where
  \forall i: 1 \upto hwm \spot name? \neq names(i)
\also
  hwm' = hwm + 1 \\
  names' = names \oplus \{ hwm' \mapsto name? \} \\
  dates' = dates \oplus \{ hwm' \mapsto date? \}
\end{schema}

\noindent The \HOL\ version of this is:

\begin{session}\begin{verbatim}

#declare
# `AddBirthday1`
# "SCHEMA
#   [DELTA BirthdayBook1;
#    name? :: NAME;
#    date? :: DATE]
#   %-----------------------------------%
#   [!i::(1..hwm). ~(name? = names(i));
#    hwm' = hwm + 1;
#    names' = names (+) {hwm' |-> name?};
#    dates' = dates (+) {hwm' |-> date?}]";;

\end{verbatim}\end{session}

The final three schemas in the implementation of the birthday book are
$FindBirthday1$, $AbsCards$, $Remind1$ and $InitBirthdayBook1$. They
introduce nothing new and are omitted.

The specification of the implementation of the birthday book is now
complete. The soundness of the implementation can be verified by
proving that the rules for operation and data refinement are
met. These rules are described in sections 5.5 and 5.6 of ZRM. When
applied to the birthday book, they generate the following two
conditions:

%%% Old theorems:
% \[
%   1.~ \pre AddBirthday \land Abs \implies \pre AddBirthday1
% \also
%   2.~ \pre AddBirthday \land Abs \land AddBirthday1 \\
%      \phantom{2.~}
%      \implies \\
%      \phantom{2.~}
%      (\exists BirthdayBook' \spot Abs' \land AddBirthday)
% \]

%%% New theorems: (make HOL match)
%%% Add \vdash in front?

\begin{zed}
  \forall BirthdayBook; BirthdayBook1; name?:NAME; date?:DATE \spot \\
\t1    \pre AddBirthday \land Abs \implies \pre AddBirthday1
\also
  \forall BirthdayBook; BirthdayBook1; BirthdayBook1'; \\
\t1     name?:NAME; date?:DATE \spot \\
\t2     \pre AddBirthday \land Abs \land AddBirthday1 \\
\t2       \implies (\exists BirthdayBook' \spot Abs' \land AddBirthday)
\end{zed}

%%% A different paragraph should be sustituted for the following if
%%% required.

%%% \noindent The operator $\land$ here is schema conjunction, whereas
%%% the operator $\implies$ is logical implication\footnote{Z experts
%%% may like to ponder on why this is the case.}. The quantifier
%%% $\exists$ is schema quantification.

It is straightforward to verify these properties in \HOL. The proofs
are quite a bit more complex than previous ones, involving various
mathematical laws (see section~\ref{zops}) and extensive case
analysis. The details will not be given here, but are available in
the directory {\verb+contrib/Z/examples+} distributed with \HOL 88 Version 2.02.

The first theorem establishes that the precondition of $AddBirthday1$
is liberal enough.

%%% Update HOL to match theorems above.
%%% Also add example on p140 of ZRM2 (functional data refinement)
%%% if you have the time: (uncomment out and position the following
%%% suitably if so)

%%% \[
%%%   \forall BirthdayBook; BirthdayBook';
%%%       BirthdayBook1; BirthdayBook1'; \\
%%% \t1   name?:NAME; date?:DATE \spot \\
%%% \t2     \pre AddBirthday \land Abs \land AddBirthday1 \\
%%% \t2       \implies AddBirthday
%%% \]

\begin{session}\begin{alltt}

#prove_theorem
# (`AbsThm1`,
#  "FORALL [BirthdayBook; BirthdayBook1; (name?::NAME); (date?::DATE)]
#    ((pre AddBirthday \verb"/\" Abs) ==> (pre AddBirthday1))",
#  \(<omitted tactic>\) );;

AbsThm1 =
|- FORALL
   [BirthdayBook;BirthdayBook1;name? :: NAME;date? :: DATE]
   (pre AddBirthday \verb"/\" Abs ==> pre AddBirthday1)

\end{alltt}\end{session}

\noindent  
The schema operations {\tt pre} and {\tt FORALL} are expanded on
input.  Note that {\tt FORALL} is interpreted as yielding a predicate
not a schema (the quantifier {\verb"SCHEMA_FORALL"} returns a schema).

There is no standard way of formulating theorems about \Z\ schemas
(though a start is made in Annexe F of the {\em \Z\ Base Standard\/}
\cite{Z:Brie92}). For example, the two theorems in \Z\ notation above
admit a variety of formal interpretations. `$\pre AddBirthday \land
Abs$' could be interpreted as either a schema expression or as a
predicate; in the former case $\land$ is a schema operation
(represented by {\tt AND} in \HOL), in the latter case it is a logical
operation (\verb"/\" in \HOL). In this particular case the two
interpretations of conjunction result in logically equivalent terms in
\HOL, but in general it is unclear if this will always be the case
(particularly with implications and quantifications). The convention
for theorems adopted here is, wherever possible, to interpret \Z's
logical operators as operators that construct predicates rather than
schemas. Other choices are possible, for example
the following version of {\tt AbsThm1} is also provable:

\begin{verbatim}
   FORALL 
    [BirthdayBook; BirthdayBook1; (name?::NAME); (date?::DATE)]
    ((pre AddBirthday AND Abs) ==> (pre AddBirthday1))
\end{verbatim}

The second theorem establishes that $AddBirthday1$ produces
the right answer.

\begin{session}\begin{alltt}

#prove_theorem
# (`AbsThm2`,
#  "FORALL [BirthdayBook; BirthdayBook1; BirthdayBook1';
#           (name?::NAME); (date?::DATE)]
#    ((pre AddBirthday \verb"/\" Abs \verb"/\" AddBirthday1)
#     ==>
#     (EXISTS BirthdayBook' (Abs' \verb"/\" AddBirthday)))",
#  \(<omitted tactic>\) );;

AbsThm2 =
|- FORALL
   [BirthdayBook; BirthdayBook1; BirthdayBook1';
    name? :: NAME; date? :: DATE]
   (pre AddBirthday \verb"/\" Abs \verb"/\" AddBirthday1 ==>
    EXISTS BirthdayBook'(Abs' \verb"/\" AddBirthday))

\end{alltt}\end{session}

\noindent  
The schema operations {\tt pre}, {\tt FORALL} and {\tt EXISTS} are
expanded on input.  {\tt FORALL} and {\tt EXISTS} are interpreted as
yielding predicates not schemas (the quantifier {\verb"SCHEMA_EXISTS"}
returns a schema).  The priming conventions for schemas are also
handled on input.  For example,

\begin{session}\begin{verbatim}

#show_schemas true;;

#"BirthdayBook";;
"SCHEMA
 [known :: (P NAME);birthday :: (NAME -+> DATE)]
 [known = dom birthday]" : term

#"BirthdayBook'";;
"SCHEMA
 [known' :: (P NAME);birthday' :: (NAME -+> DATE)]
 [known' = dom birthday']" : term

\end{verbatim}\end{session}

It is a tribute to \Z's notational power using the schema notation that
complex theorems like $AbsThm1$ and $AbsThm2$ can be expressed
concisely. This complexity is revealed if the \Z\ printing is switched
off so that the semantic representations of schemas is output as
illustrated in box~25. This graphically illustrates why
the schema notation was invented to structure and hide the mass of
detailed mathematics which can be held in a \Z\ specification.

%%% I've made the following into a figure to help avoid bad page breaks.
%%% I think some tweaking may be necessary in the final version.
%%% Undone by MJCG!

%\begin{figure}
\begin{session}{\footnotesize\baselineskip=8pt\begin{verbatim}

#AbsThm2;;
|- !known birthday.
    known :: (P NAME) /\ birthday :: (NAME -+> DATE) ==>
    known :: (P NAME) /\ birthday :: (NAME -+> DATE) /\
    (known = dom birthday) ==>
    (!names dates hwm.
      names :: (NN_1 --> NAME) /\ dates :: (NN_1 --> DATE) /\ hwm :: NN ==>
      names :: (NN_1 --> NAME) /\ dates :: (NN_1 --> DATE) /\ hwm :: NN /\
      (!i j :: 1 .. hwm. ~(i = j) ==> ~(names ^^ i = names ^^ j)) ==>
      (!names' dates' hwm'.
        names' :: (NN_1 --> NAME) /\ dates' :: (NN_1 --> DATE) /\
        hwm' :: NN ==>
        names' :: (NN_1 --> NAME) /\ dates' :: (NN_1 --> DATE) /\
        hwm' :: NN /\
        (!i j :: 1 .. hwm'. ~(i = j) ==> ~(names' ^^ i = names' ^^ j)) ==>
        (!name?.
          name? :: NAME ==>
          (!date?.
            date? :: DATE ==>
            SCHEMA
            [known :: (P NAME);birthday :: (NAME -+> DATE);
             name? :: NAME;date? :: DATE]
            [?known' birthday'.
              (known' :: (P NAME) /\ birthday' :: (NAME -+> DATE)) /\
              (known = dom birthday) /\ (known' = dom birthday') /\
              ~name? IN known /\
              (birthday' = birthday UNION {name? |-> date?})] /\
            SCHEMA
            [known :: (P NAME);birthday :: (NAME -+> DATE);
             names :: (NN_1 --> NAME);dates :: (NN_1 --> DATE);
             hwm :: NN]
            [known = dom birthday;
             !i j :: 1 .. hwm. ~(i = j) ==> ~(names ^^ i = names ^^ j);
             known = {names ^^ i | i :: (1 .. hwm)};
             !i :: 1 .. hwm. birthday ^^ (names ^^ i) = dates ^^ i] /\
            SCHEMA
            [names :: (NN_1 --> NAME);dates :: (NN_1 --> DATE);
             hwm :: NN;names' :: (NN_1 --> NAME);
             dates' :: (NN_1 --> DATE);hwm' :: NN;name? :: NAME;
             date? :: DATE]
            [!i j :: 1 .. hwm. ~(i = j) ==> ~(names ^^ i = names ^^ j);
             !i j :: 1 .. hwm'. ~(i = j) ==> ~(names' ^^ i = names' ^^ j);
             !i :: 1 .. hwm. ~(name? = names ^^ i);hwm' = hwm + 1;
             names' = names (+) {hwm' |-> name?};
             dates' = dates (+) {hwm' |-> date?}] ==>
            (?known' birthday'.
              (known' :: (P NAME) /\ birthday' :: (NAME -+> DATE)) /\
              known' :: (P NAME) /\ birthday' :: (NAME -+> DATE) /\
              (known' = dom birthday') /\
              SCHEMA
              [known' :: (P NAME);birthday' :: (NAME -+> DATE);
               names' :: (NN_1 --> NAME);dates' :: (NN_1 --> DATE);
               hwm' :: NN]
              [known' = dom birthday';
               !i j :: 1 .. hwm'. ~(i = j) ==> ~(names' ^^ i = names' ^^ j);
               known' = {names' ^^ i | i :: (1 .. hwm')};
               !i :: 1 .. hwm'. birthday' ^^ (names' ^^ i) = dates' ^^ i] /\
              SCHEMA
              [known :: (P NAME);birthday :: (NAME -+> DATE);
               known' :: (P NAME);birthday' :: (NAME -+> DATE);
               name? :: NAME;date? :: DATE]
              [known = dom birthday;known' = dom birthday';
               ~name? IN known;
               birthday' = birthday UNION {name? |-> date?}])))))

\end{verbatim}}\end{session}

%\caption{An example of expanding a theorem.\label{AbsThm2}}
%\end{figure}

\bigskip

As a final example, here is the ``sufficient condition'' for the
correct implementation of the sequential composition 
of {\verb+AddBirthday+} and {\verb+FindBirthday+} that is
described in general terms
on page 134 of
ZRM.
This is much easier to prove than either {\verb"AbsThm1"}
or {\verb"AbsThm2"}. 
The sufficient condition for the composition
of {\verb+AddBirthday1+} and {\verb+FindBirthday1+}
is also easy to prove.
Note that {\verb"show_schema true"} is still in force.

\begin{session}{\footnotesize\begin{alltt}

#prove_theorem
# (`AddFindSeq`,
#  "FORALL 
#    [BirthdayBook'']
#    ((EXISTS[AddBirthday](theta BirthdayBook' = theta BirthdayBook''))
#     ==>
#     (EXISTS[FindBirthday](theta BirthdayBook = theta BirthdayBook'')))",
#  \(<omitted tactic>\) );;

AddFindSeq = 
|- !known'' birthday''.
    known'' :: (P NAME) \verb"/\" birthday'' :: (NAME -+> DATE) ==>
    known'' :: (P NAME) \verb"/\"
    birthday'' :: (NAME -+> DATE) \verb"/\"
    (known'' = dom birthday'') ==>
    (?known birthday known' birthday' name? date?.
      (known :: (P NAME) \verb"/\" birthday :: (NAME -+> DATE) \verb"/\"
       known' :: (P NAME) \verb"/\" birthday' :: (NAME -+> DATE) \verb"/\"
       name? :: NAME \verb"/\" date? :: DATE) \verb"/\" known :: (P NAME) \verb"/\"
      birthday :: (NAME -+> DATE) \verb"/\" known' :: (P NAME) \verb"/\"
      birthday' :: (NAME -+> DATE) \verb"/\" name? :: NAME \verb"/\"
      date? :: DATE \verb"/\" (known = dom birthday) \verb"/\"
      (known' = dom birthday') \verb"/\" ~name? IN known \verb"/\"
      (birthday' = birthday UNION {name? |-> date?}) \verb"/\"
      ((`birthday`,birthday'),`known`,known' =
       (`birthday`,birthday''),`known`,known'')) ==>
    (?known birthday known' birthday' name? date!.
      (known :: (P NAME) \verb"/\" birthday :: (NAME -+> DATE) \verb"/\"
       known' :: (P NAME) \verb"/\" birthday' :: (NAME -+> DATE) \verb"/\"
       name? :: NAME \verb"/\" date! :: DATE) \verb"/\" known :: (P NAME) \verb"/\"
      birthday :: (NAME -+> DATE) \verb"/\" known' :: (P NAME) \verb"/\"
      birthday' :: (NAME -+> DATE) \verb"/\" name? :: NAME \verb"/\"
      date! :: DATE \verb"/\" (known = dom birthday) \verb"/\"
      (known' = dom birthday') \verb"/\"
      ((`birthday`,birthday'),`known`,known' =
       (`birthday`,birthday),`known`,known) \verb"/\"
      name? :: known \verb"/\"
      (date! = birthday ^^ name?) \verb"/\"
      ((`birthday`,birthday),`known`,known =
       (`birthday`,birthday''),`known`,known''))

\end{alltt}}\end{session}

The implementation of bindings
and their extraction (i.e.~$\theta$ in \Z{} and {\verb"theta"} in \HOL) is
discussed in section~\ref{io}.

\section{How Z is supported in HOL}\label{support}

The support for \Z\ illustrated in the previous section has two
parts: (i) input and output procedures to handle the various schema
operations and to manage schema and variable names, and (ii) the
\HOL\ theory {\tt Z} that implements the \Z\ operators and
mathematical toolkit.

\subsection{Inputting and outputting schemas}\label{io}

When a \HOL\ quotation of the form {\verb+"+}$\cdots${\verb+"+} is read
a number of transformations are performed. The most important of these
are listed below.

\begin{enumerate}

\item
Variables that have previously been declared as schema names
with the \ML\ function {\tt declare} are replaced by their semantic
representation, which is a term of the form
{\verb"SCHEMA ["}$\cdots${\verb"] ["}$\cdots${\verb"]"}.

Decorated (e.g.~dashed) schema names are expanded to the appropriately
decorated semantic representations (see box~24).

\item
Applications $s~x$, where $s$ has previously been declared in a
schema as a set representing a \Z\ function, are expanded to
$s${\verb"^^"}$x$.

\item
Terms of the form:

\begin{enumerate}

\item
{\tt pre}~{\verb"(SCHEMA ["}$\cdots${\verb"] ["}$\cdots${\verb"])"}

\item
{\verb"(SCHEMA ["}$\cdots${\verb"] ["}%
$\cdots${\verb"])"}~{\tt SEQ}~{\verb"(SCHEMA ["}$\cdots${\verb"] ["}%
$\cdots${\verb"])"}

\item
{\verb"(SCHEMA ["}$\cdots${\verb"] ["}%
$\cdots${\verb"])"}~{\tt AND}~{\verb"(SCHEMA ["}$\cdots${\verb"] ["}%
$\cdots${\verb"])"}

\item
{\verb"(SCHEMA ["}$\cdots${\verb"] ["}%
$\cdots${\verb"])"}~{\tt OR}~{\verb"(SCHEMA ["}$\cdots${\verb"] ["}%
$\cdots${\verb"])"}

\item
{\verb"(SCHEMA ["}$\cdots${\verb"] ["}%
$\cdots${\verb"])"}~{\tt IMPLIES}~{\verb"(SCHEMA ["}%
$\cdots${\verb"] ["}$\cdots${\verb"])"}

\item
{\verb"(SCHEMA ["}$\cdots${\verb"] ["}%
$\cdots${\verb"])"}~{\tt HIDE}~{\verb"("}$x_1,\cdots,x_n${\verb")"}

\item
{\verb"SCHEMA_FORALL "}{\verb"(SCHEMA ["}$\cdots${\verb"] ["}%
$\cdots${\verb"])"}~{\verb"(SCHEMA ["}%
$\cdots${\verb"] ["}$\cdots${\verb"])"}

\item
{\verb"SCHEMA_EXISTS "}{\verb"(SCHEMA ["}$\cdots${\verb"] ["}%
$\cdots${\verb"])"}~{\verb"(SCHEMA ["}%
$\cdots${\verb"] ["}$\cdots${\verb"])"}

\end{enumerate}

\noindent
are expanded out to the appropriate semantic representation
of the form {\verb"SCHEMA ["}$\cdots${\verb"] ["}$\cdots${\verb"]"}.

The input and result of the expansion is saved in a global
data structure, so that it can be inverted when schemas are printed.

\item
Terms of the form:

\begin{enumerate}

\item
{\verb"FORALL "}{\verb"(SCHEMA ["}$\cdots${\verb"] ["}%
$\cdots${\verb"])"}~$P$

\item
{\verb"FORALL "}{\verb"("}$x${\verb"::"}$S${\verb")"}~$P$

\item
{\verb"EXISTS "}{\verb"(SCHEMA ["}$\cdots${\verb"] ["}%
$\cdots${\verb"])"}~$P$

\item
{\verb"EXISTS "}{\verb"("}$x${\verb"::"}$S${\verb")"}~$P$

\end{enumerate}

\noindent
are expanded out to terms representing the appropriate quantifications
of the predicate $P$.  The input and result of the expansion is saved
in a global data structure, so it that can be inverted when schemas are
printed.

Quantifications of the form {\tt
Q}~{\verb"["}$v_1${\verb";"}$\cdots${\verb";"}$v_n${\verb"] "}$P$ are
converted into iterated quantifications {\tt Q}~$v_1$~{\verb"("}{\tt
Q}~$v_2$~{\verb"("}~$\cdots$~{\verb"("}{\tt Q}~%
$v_n~P${\verb")"}~$\cdots$~{\verb")"}{\verb")"}.

\item $
\verb"sig (SCHEMA ["x_1\verb":"S_1\verb";"\ldots\verb";"x_n\verb":"
  S_n\verb"] ["\cdots\verb"])"
$
is expanded to the type membership statement:
\begin{alltt}
     \(x\sb{1}\) IN \(S\sb{1}\) \verb"/\" \(x\sb{2}\) IN \(S\sb{2}\) \verb"/\" \(\ldots\) \verb"/\" \(x\sb{m}\) IN \(S\sb{m}\) 
\end{alltt}

\item $
\verb"theta(SCHEMA ["x_1\verb":"S_1\verb";"\ldots\verb";"x_n\verb":"
  S_n\verb"] ["\cdots\verb"])"
$
is expanded to $n$-tuples of pairs of the form:
\begin{alltt}
     ((`\(x\sb{\sigma\sb{1}}\)`, \(x\sb{\sigma\sb{1}}\)), \(\ldots\) , (`\(x\sb{\sigma\sb{n}}\)`, \(x\sb{\sigma\sb{n}}\)))
\end{alltt}
which represent {\it bindings} in \Z. The sequence $x_{\sigma_1}\ldots x_{\sigma_n}$ is a canonical reordering
of $x_1\ldots x_n$,
which ensures that equivalent bindings (i.e. ones that are equal up to reordering of components)
are translated to the same \HOL{} term.

\item {\verb+DELTA+}$~{\cal S}$ is translated to ${\cal S}{\verb+ AND +}{\cal S}{\verb+'+}$. 
This implements the \Z{} definition:
\[
   \Delta {\cal S} ~\defs~ {\cal S} \land {\cal S}'
\]


\item {\verb+XI+}$~{\cal S}$ is translated to 
{\verb+SCHEMA[DELTA +}${\cal S}${\verb+][theta+}${\cal S}{\verb+'+}${\verb+ = theta+}${\cal S}${\verb+]+}.
This implements the \Z{} definition:
\[
   \Xi {\cal S} ~\defs~ [ \Delta {\cal S} | \theta {\cal S}' = \theta {\cal S} ]
\]


\end{enumerate}

When a term is output by \HOL, any schema representations that have
previously been given a name are replaced by the name. In addition,
any representation resulting from of one of the expansions 
in 3 -- 8 above is replaced by the input to the expansion.
For example, if $S_1~{\tt SEQ}~S_2$ expands to $S_3$ (3b above), then
$S_3$ will be output as $S_1~{\tt SEQ}~S_2$. This process is applied
recursively.

The method of fully expanding out schemas into their semantic
representations works well for small examples like the birthday
book. The interactions shown in the boxed sections mostly happen
instantaneously (though the proofs of {\verb"AbsThm1"} and
{\verb"AbsThm2"} take a few seconds to run). However, the underlying
terms can get large and it is possible that `industrial scale'
specifications might slow down \HOL\ unacceptably. If this were the
case then abbreviatory definitions could be used to prevent terms getting too
large. Such abbreviations could be introduced automatically (e.g.~by
the \ML\ function {\verb"declare"}). Fortunately performance has been
adequate so far and such measures have not been felt necessary.

\subsection{Shallow versus deep embedding}\label{embed}

Shallow embedding can be contrasted with {\it deep embedding\/}
\cite{Embedding,Melham} in which both the syntax and semantics of the
embedded language are formalized inside the host logic. With shallow
embedding the mapping from language constructs to their semantic
representations is part of the metalanguage; with deep embedding it is
part of the object language theory. It is usually more work to support
a language by deep embedding, but it is necessary if one wants to prove
theorems about the language rather than just reason in it.

Since the schema operations are `macro expanded' away, it is not
possible to state general theorems about them. For example, it is
impossible to express the fact that schema conjunction is commutative.
For any particular schema one can prove the instance of the fact, but
such proofs have to be repeated for each separate instance (though they
can be performed automatically with a suitable derived rule).

A weakness of shallow embedding is that the operations that are
computed outside the logic are not subject to the same `quality
control' as operations specified in the logic, because errors in the
definition of operators reside in program code not in logical
formulae. Generally the latter are easier to inspect for correctness
than the former. For example, if the macro expansion of {\tt SEQ}
contained a bug (e.g.~dashed variables were sometimes invalidly
captured by quantifiers) then this might only manifest itself in the
wrong schema expansion being computed. If in addition the output
routines `inverted' the bug the user might be unaware that the wrong
semantic representation was being manipulated. A deep embedding allows
meta-theorems to be proved (e.g.~the associativity of schema
sequencing) that can serve to partially validate the definitions of
the operators.

A deep embedding of \Z\ in \HOL\ is possible. It could, for example,
be based on the metatheory presented in the \Z\ base standard
\cite{Z:Brie92}. The resulting theory would be complex and probably
hard to apply to particular examples like the birthday book. However,
it would be suitable for testing out the meta-theory of \Z\ and
verifying general properties of it (e.g.~see the work by Maharaj
briefly discussed below).

The distinction between ``shallow'' and ``deep'' is not always sharp.
For example, ProofPower provides a much `deeper' embedding than the
one described here (all the \Z\ operators are defined in \HOL) but
there is no single semantic function defined in the the logic that
maps \Z\ syntax into its meaning. ProofPower's embedding is not `deep
enough' to allow facts like the commutativity of schema conjunction to
be proved.

The lightweight shallow embedding illustrated here puts relatively
few obstacles in the way of using all the power of \HOL\ to reason
about particular \Z\ specifications, but it is useless for verifying
properties of \Z\ itself.

\subsection{Z's operators in HOL}\label{zops}

The operators used in the birthday book are included in those shown in
the table below. The {\small\tt ASCII} versions of the
\Z\ operators are based on those used by the
\fuzz\ and ZTC type-checking tools \cite{Z:Spiv92b,Z:ZTC}.

%\begin{table}

\begin{center}
\begin{tabular}{|l|l|l|}
\hline
\Z\ operator & \HOL\ notation & Meaning \\ \hline
             &                & \\[-1ex]
$:$          & {\verb"::"}    & Membership declaration\\
$\dom$       & {\verb"dom"}   & Domain\\
$\mapsto$    & {\verb"|->"}   & Maplet\\
$\power$     & {\verb"P"}     & Power set\\
$\cross$     & {\verb"><"}    & Cartesian product\\
$\rel$       & {\verb"<->"}   & Binary relations\\
$\pfun$      & {\verb"-+>"}   & Partial functions\\
$\fun$       & {\verb"-->"}   & Total functions\\
             & {\verb"^^"}    & Application of \Z\ functions\\
$\ndres$     & {\verb"<+"}    & Domain anti-restriction\\
$\oplus$     & {\verb"(+)"}   & Relational overriding\\
$\nat$       & {\verb"NN"}    & Natural numbers\\
$\nat_1$     & {\verb"NN_1"}  & Strictly positive integers\\
$\upto$      & {\verb".."}    & Number range\\
 \hline
\end{tabular}
\end{center}

%\caption{Z and HOL operators.\label{notation}}

%\end{table}

The operators in this table are defined (in \HOL\ notation)
by:

\begin{verbatim}
   |- (CONJL[] = T) /\ (!b bl. CONJL(CONS b bl) = b /\ CONJL bl)
   |- SCHEMA decs body = CONJL decs /\ CONJL body
   |- x :: s = x IN s
   |- x |-> y = x,y
   |- dom R = {x | ?y. (x |-> y) IN R}
   |- P X = {Y | Y SUBSET X}
   |- X >< Y = {(x,y) | x IN X /\ y IN Y}
   |- X <-> Y = P(X >< Y)
   |- X -+> Y = {f | f IN (X <-> Y) /\ (!x y1 y2.
              (x |-> y1) IN f /\ (x |-> y2) IN f ==> (y1 = y2))}
   |- X --> Y = {f | f IN (X -+> Y) /\ (dom f = X)}
   |- f^^x = @y. (x,y) IN f
   |- S <+ R = {x |-> y | ~x IN S /\ (x |-> y) IN R}
   |- f (+) g = ((dom g) <+ f) UNION g
   |- NN = {n | n >= 0}
   |- NN_1 = {n | n > 0}
   |- m .. n = {i | m <= i /\ i <= n}
\end{verbatim}

\noindent
The \HOL\ function \verb"CONJL" conjoins a list of predicates.
The set application operator {\verb"^^"} is defined using the \HOL\
choice operator {\verb"@"}, which is Hilbert's $\varepsilon$-symbol. The
term {\verb"@"}$x${\verb"."}$P[x]$ denotes some value, $a$ say, such
that $P[a]$ is true. {\verb"@"} is related to the \Z\ $\mu$-operator,
but unlike $\mu$ does not require $P[x]$ to be satisfied by a unique
value. The conventional logical symbol corresponding to $\mu$ in \Z\ is
the unique existence operator $\iota$. If no $a$ exists such that $P[a]$
is true, then {\verb"@"}$x${\verb"."}$P[x]$ denotes an arbitrary value.
It would be possible to choose this arbitrary value in a canonical way,
but its underlying \HOL\ type must be the same as that of $x$ in $P[x]$.

The theory {\tt Z} also contains \HOL\ theorems about the \Z\
operators. The ones used in proving the theorems in
section~\ref{birthdaybook} are listed below:

\begin{verbatim}

   |-  dom(X UNION Y) = (dom X) UNION (dom Y)
   |-  dom{x |-> y} = {x}
   |-  x IN (dom{x |-> y})
   |-  f IN (X -+> Y) /\ x IN (dom f) ==> x IN X
   |-  f IN (X -+> Y) ==> (dom f) IN (P X)
   |-  x IN X /\ y IN Y ==> {x |-> y} IN (X -+> Y)
   |-  f IN (X -+> Y) /\ x IN X /\ y IN Y /\ ~x IN (dom f) ==>
       (f UNION {x |-> y}) IN (X -+> Y)
   |-  f IN (X --> Y) ==> (dom f = X)
   |-  f IN (X --> Y) ==> f IN (X -+> Y)
   |-  ~(x1 = x2) ==> ((X UNION {x1 |-> v}) ^^ x2 = X ^^ x2)
   |-  ~x IN (dom X) ==> ((X UNION {x |-> v}) ^^ x = v)
   |-  {x |-> v} ^^ x = v
   |-  f IN (X -+> Y) /\ x IN (dom f) ==> 
       (!y. (f ^^ x = y) = (x,y) IN f)
   |-  f IN (X -+> Y) ==> (!x. x IN (dom f) = (x,f ^^ x) IN f)
   |-  f IN (X --> Y) /\ g IN (X --> Y) ==> 
       (f (+) g) IN (X --> Y)
   |-  f IN (X -+> Y) /\ g IN (X -+> Y) ==> 
       (f (+) g) IN (X -+> Y)
   |-  f IN (X -+> Y) /\ g IN (X -+> Y) ==>
       (dom(f (+) g) = (dom f) UNION (dom g))
   |-  f IN (X -+> Y) /\ g IN (X -+> Y) /\ 
       x IN ((dom f) DIFF (dom g)) ==> ((f (+) g) ^^ x = f ^^ x)
   |-  f IN (X -+> Y) /\ g IN (X -+> Y) /\ x IN (dom g) ==>
       ((f (+) g) ^^ x = g ^^ x)
   |-  n IN NN
   |-  (n + 1) IN NN_1
   |-  f IN (NN_1 --> X) /\ v IN X ==>
       ((f (+) {(n + 1) |-> v}) ^^ (n + 1) = v)
   |-  1 .. (n + 1) = (1 .. n) UNION ((n + 1) .. (n + 1))
   |-  x IN (n .. n) = (x = n)
   |-  x IN (m .. n) = m <= x /\ x <= n
   |-  f IN (NN_1 -+> X) /\ x IN X ==>
       (f (+) {(n + 1) |-> x}) IN (NN_1 -+> X)
   |-  NN_1 UNION {n + 1} = NN_1
   |-  f IN (NN_1 --> X) /\ x IN X ==>
       (f (+) {(n + 1) |-> x}) IN (NN_1 --> X)
\end{verbatim}


\section{Other related work}\label{other}

ICL's ProofPower \cite{ProofPower} is an `\LCF-like' system that
supports the same version of higher order logic as \HOL, but provides
different theorem proving infrastructure. ICL used the original
\HOL\ for many years and have built on this experience in designing
ProofPower. Although the theorem proving tools are not identical to
\HOL's, they are similar in spirit but aim to be more powerful. Some
of the features provided have been designed with the needs of \Z\
in mind. ProofPower supports \Z\ via a much `deeper' embedding than
the one presented here. The main difference in their approach is
that schemas are treated more like set abstractions (yielding a set
of bindings), and schema operations are then operators over sets of
bindings. Schema references as predicates are treated as abbreviations
for membership statements, e.g.~a reference $S$ abbreviates $\theta
S\in \hat{S}$, where $\hat{S}$ is the representation of schema $S$.
ProofPower has been used for internal applications at ICL and is
currently undergoing evaluation in a small group of companies and
academic institutions. ProofPower proofs in \Z\ are intended to be
conducted with all visible subgoals in \Z\ notation. The language
supported is intended to be compatible with the proposed `ISO standard
\Z' \cite{Z:Brie92} rather than the \Z\ described in ZRM. ProofPower
has a polished interface that understands \Z's special symbols. It
has more \Z-specific proof infrastructure and better coverage of the
\Z\ notation than the implementation described here. More
information is obtainable from the ProofPower server by sending an
email message to: {\verb"ProofPower-server@win.icl.co.uk"}.

A relatively deep embedding of \Z\ in the type theory UTT (Unifying
Theory of dependent Types) has been undertaken by Savi Maharaj
\cite{Maharaj}. A method of representing \Z\ schemas in UTT
(independently of the \Z\ core language) was developed. The LEGO
proof-checker has been used to prove several theorems that are intended
to support reasoning about \Z-like specifications at the schema level.
For example, introduction and elimination rules for schema conjunction
have been verified. Earlier work \cite{Mah90} considered ways of
encoding the core language of \Z\ in type theory.

The \Z/EVES project at Odyssey Research Associates (ORA)
\cite{EVES:Report,EVES:Paper} investigated the feasibility of using
EVES, a theorem prover for ZF set theory, as a proof tool for \Z. A
standard example from the security community (``The Low Water Mark'')
was used as a case study. This was specified in \Z\ and a proof of a
non-interference security property performed. Most of the Mathematical
Toolkit in ZRM was expressed in EVES and the laws proved and installed
as rewrites. EVES is much more automatic than \HOL\ and thus an
embedding of Z into EVES might provide proof support with less user
interaction. However, the feasibility study was not followed by any tool
development.

The Balzac project at Imperial Software Technology (IST) is building
editing, typesetting, type-checking and proof support for \Z\
\cite{Balzac}; it is funded by contracts from CESG (a UK Government
organization). Balzac is a tactic based system in which tactics rather
than rules are primitive; the tactic writing language is a secure form
of Lisp. The user interface is powerful and sophisticated.  The
version of \Z{} supported is non-standard (e.g.~basic types are
assumed non-empty). Balzac has been used to produce specifications
consisting of 500--1000 pages (about two and a half schemas a page)
and has been used to carry out proofs about these which involve a
significant proportion of the schemas.  IST sell a commercial variant
of Balzac called Zola.  \footnote{The example from the report ``A
Simple Demonstration of Balzac'' \cite{Collinson} has been done in
HOL; see {\verb+contrib/Z/TelephoneBook.ml+} distributed with HOL88
Version 2.02.}

Another approach to providing proof support for \Z\ is to encode a
deductive system for it in a generic theorem prover. An example of this
is the encoding of \W, a logic for \Z\ \cite{Z:Wood92}, in the 2OBJ
metalogical theorem prover \cite{Z:Mart93}. This approach differs from
semantic embedding in that the semantics of \Z\ is not represented in
the host logic; instead proof rules are encoded directly. This has the
advantage that complex rules can be immediately implemented as
primitives. With semantic embedding such rules have to be embodied in
procedures (e.g.~\ML\ functions) that perform inferences in an
underlying logic. A single step in a logic designed specially for \Z\
(e.g.~\W) might correspond to many steps in a more primitive logic
(e.g.~higher order logic). For example, the proof of {\verb"AbsThm2"}
above consists of over five thousand primitive \HOL\ inferences.
Currently the encoding of \W\ in 2OBJ is very inefficient and so it is
not yet usable in practice.

A more practical approach, not based on semantic embedding, was adopted
by the \zedB\ tool \cite{Z:Neil91,Z:Neil92}. This was based on the
B-Tool (which is a general-purpose symbolic manipulator not
incorporating any particular logic) and enabled calculation and
verification of properties of Z specifications. Facilities for schema
viewing, expansions, precondition calculation, discharging of
initialization and other syntactic and semantic operations were
included.  Unfortunately only a prototype tool which is not generally
available has been produced.

%%% Comment on level of embedding if you get the Neilson papers in the
%%% post in time. I find it difficult to judge from the papers.
%%% But Z and B are a pretty good match (both from the same
%%% orginator, J-R Abrial).
%%% Not based on semantic embedding [MJCG]

Many \Z\ tools are under development; current information on the
availability of \Z\ tools may be gleaned from the monthly message
issued on the electronic newsgroup \verb"comp.specification.z" and the
associated ZFORUM mailing list on \Z\ \cite{Z:Bowe93}.


\section{Conclusions and future work}

It turned out to be easier than expected to provide basic support
for a significant subset of \Z\ in \HOL. At the time of writing only
a few case studies have been conducted (the birthday book is the
largest), so it is hard to evaluate the success or otherwise of the
approach. Only a fragment of \Z\ is currently supported, but no major
difficulties are anticipated in increasing the coverage to most of
the rest of the Z toolkit. Other more complicated features of \Z\
such as schemas as types, true generic definitions and the complete
facilities for free type definitions may require further thought and/or
compromises. Our plan is to approach this via more case studies.
Examples being considered include the simple checkpointing scheme in ZRM,
the ``Word-For-Word'' example in the textbook {\it An Introduction
to Formal Specification and \Z\/} \cite{Z:Pott90}, an \ML\ pattern
matching refinement case study \cite{Zpatt} and the ``The Low Water
Mark'' \cite{EVES:Report}.

A disadvantage of our approach is that users need to be proficient
with \HOL\ before they can attempt proofs in \Z. Learning \HOL\ is
quite time consuming; at least one week of full-time training is needed
to get started effectively. In particular, \HOL\ tactics must be
mastered. However, extensive training materials for \HOL\ are available
and there is a relatively large international user
community.

In the future it is hoped to provide support for interfacing with the
widely available \LaTeX\ document preparation system for
compatibility with other \Z-processing tools, such as \fuzz\ (whose
\LaTeX\ style option was used to prepare this paper) and the public domain ZTC
\cite{Z:ZTC}. \HOL's parser and pretty printer libraries should make
this relatively straightforward.


\section*{Acknowledgements}

We are grateful to Jim Grundy, Terry Ireland, Roger Jones, Savitri
Maharaj, Tom Melham and Mark Saaltink for reading a draft of this
paper and making numerous suggestions for its improvement. Will Harwood
provided information on Balzac and its use. Mike Spivey
provided the Birthday Book example and the \fuzz\ tool. Jonathan Bowen
is funded by the UK Science and Engineering Research Council (SERC) on
grant no.\ GR/J15186.


% Include all the bibliography if required:
% \nocite{*}

\bibliography{zhol}
\bibliographystyle{wicsbook}

\end{document}


