%LaTeX style
%
% zed.sty 15 feb 88
%
\typeout{Style Option 'zed'. Released 15 February 1988}

%
% Copyright (c) J.M. Spivey 1988
%
% This file contains a collection of macros for typesetting
% Z specifications. There are four sections.
%
% 0. The mathcodes for letters are changed so that they generate text
%    italic instead of math italic. This makes multi-letter identifiers
%    look neater.
%
% 1. Environments for putting the maths in boxes.
%
% 2. Extra symbol fonts are loaded.
%
% 3. Mnemonics for Z symbols are defined. Note that certain plain TeX
%    names are usurped here: \forall is made into a \mathop to give a
%    thin space between it and the following declaration. The same goes
%    for \lambda and \mu, and \exists.
%

%
% Changes since 25 aug 87
%
% 25 aug 87	Renamed \tad as \also and \also as \zbreak. \def'ed \tad
%		to \also for upward compatibility.
%		Inserted message on loading.
%
% 15 sep 87	Revamped special symbol names.
%
% 18 sep 87	Changed \z@d to allow Z text in lists. 
%
% 24 sep 87	Removed assignment to \prevdepth from \endschema
%		--- giving a little more vertical space.
%
%  8 oct 87	Removed a spurious space from \schema --- caused
%		empty paragraph between adjacent schemas.
%		Merged left bar code into \axdef. Removed redef
%		of \_.
%
% 12 oct 87	Removed \@zedwidth -- use \linewidth instead.
%		Removed a spurious space from \z@dpream.
%
% 16 oct 87	Removed def of \par from \z@d.
%
% 10 dec 87	Removed spurious space from \gendef
%
% 15 jan 88	Split into two parts to allow both AMS and OXSY versions.
%
% 15 feb 88	Added gendef* environment

%
% MATHCODES
%
% The mathcodes for the letters A, ..., Z, a, ..., z are changed to
% generate text italic rather than math italic by default. This makes
% multi-letter identifiers look better. The mathcode for character c
% is set to "7000 (variable family) + "400 (text italic) + c.
%
% Also, the mathcode for semicolon is set to "8000, so it behaves as an
% active character in math mode; it is defined to insert a thick space.
% \semicolon is a semicolon as an ordinary symbol.
%

\def\@setmcodes#1#2#3{{\count0=#1 \count1=#3
	\loop \global\mathcode\count0=\count1 \ifnum \count0<#2
	\advance\count0 by1 \advance\count1 by1 \repeat}}

\@setmcodes{`A}{`Z}{"7441}
\@setmcodes{`a}{`z}{"7461}

\mathcode`\;="8000 % Makes ; active in math mode
{\catcode`\;=\active \gdef;{\semicolon\;}}
\mathchardef\semicolon="003B

%
% SCHEMAS, Etc.
%
% Here are environments for the various sorts of
% displays which occur in Z documents. All displays are set
% flush left, indented by \zedindent, by default \leftmargini.
% schemas, etc, are made just wide enough to give equal margins
% left and right.
%
% Some environments (schema, etc.) must only be split at `\zbreak',
% and others (argue) may be split arbitrarily. All generate alignment
% displays, and penalties are used to control page breaks.
%
\newdimen\zedindent	\zedindent=\leftmargini
\newdimen\zedleftsep	\zedleftsep=1em
\newdimen\zedtab	\zedtab=2em
\newdimen\zedbar	\zedbar=6em
\newcount\interzedlinepenalty \interzedlinepenalty=10000
\newcount\preboxpenalty \preboxpenalty=0
\newif\ifzt@p		\zt@pfalse

\def\n@rrow{\advance\linewidth by-\zedindent}
\def\t@pline#1{\omit \hbox to\linewidth{\strut
	\leftt@p#1\thinspace\hrulefill}\cr}
\def\z@dline{\omit \hbox to\linewidth{\hrulefill}\cr}
\def\z@dpream{\halign to\linewidth\bgroup
        \strut\z@dleft$\@lign##$\hfil \tabskip=0pt plus1fil%
	&\hbox to0pt{\hss$\@lign##$}\tabskip=0pt\cr}
\let\z@dleft=\relax

\def\zbreak{\crcr \noalign{\penalty\interdisplaylinepenalty} \also}
\def\also{\crcr \noalign{\vskip\jot}}
\def\tad{\also}

\def\@zed{\ifvmode\@zleavevmode\fi
	$$\global\zt@ptrue \lineskip=0pt
	\advance\linewidth by-\zedindent
	\advance\displayindent by\zedindent
	\def\\{\crcr}% Must have \def and not \let for nested alignments.
	\everycr={\noalign{\ifzt@p \global\zt@pfalse
		\else \penalty\interzedlinepenalty \fi}}
        \tabskip=0pt}
\def\end@zed{$$\global\@ignoretrue}

\def\zed{\@zed\z@dpream}
\def\endzed{\crcr\egroup\end@zed}

\let\[=\zed
\def\]{\crcr\egroup$$\ignorespaces}

\def\axdef{\let\zbreak=\zbre@k \let\also=\@lso \let\z@dleft=\@zedleft
	\predisplaypenalty=\preboxpenalty \zed}
\let\endaxdef=\endzed
\def\zbre@k{\also \noalign{\penalty\interdisplaylinepenalty \vskip-\jot} \also}
\def\@lso{\crcr \@but \omit\vrule height\jot \cr \@but}
\def\@zedleft{\vrule\hskip\zedleftsep}
\def\@but{\noalign{\nointerlineskip}}

\def\schema#1{\n@rrow\axdef \t@pline{$#1$}}
\def\endschema{\also \z@dline \endzed}

\def\where{\also \omit \hbox to\zedbar{\hrulefill}\cr \also}

\@namedef{schema*}{\n@rrow\axdef
	\noalign{\kern-\ht\strutbox} \z@dline \also}
\expandafter\let\csname endschema*\endcsname=\endschema

\def\gendef#1{\let\leftt@p=\@leftt@p
        \setbox0=\hbox{$[#1]$}\setbox1=\null \wd1=\wd0
        \n@rrow\axdef \t@pline{\box0}%
        \noalign{\kern-\baselineskip\kern-\doublerulesep \nobreak}%
	\t@pline{\box1} \noalign{\kern\doublerulesep \nobreak}}
\let\endgendef=\endschema

\@namedef{gendef*}{\n@rrow\axdef
	\noalign{\kern-\ht\strutbox} \z@dline
	\noalign{\kern-\baselineskip\kern-\doublerulesep \nobreak}
	\z@dline \noalign{\kern\doublerulesep \nobreak} \also}
\expandafter\let\csname endgendef*\endcsname=\endschema

% `infrule' environment: used for inference rules. The horizontal line is
% generated by \derive: an optional argument contains the side-conditions
% of the rule.
\def\infrule{\@zed \halign\bgroup
	\strut\quad$\@lign##$\quad\hfil&\quad\@lign##\hfil\cr}
\let\endinfrule=\endzed

\def\derive{\crcr\also\@but\omit\hrulefill\@ifnextchar[{\@xderive}{\@yderive}}
\def\@xderive[#1]{&$\smash{\lower 0.5ex\hbox{$[\;#1\;]$}}$\cr\also\@but}
\def\@yderive{\cr\also\@but}

% `argue' environment: used for algebraic proofs expressed as extended
% equations. Generates an alignment display, which may be split across
% pages.
\def\argue{\@zed \interzedlinepenalty=\interdisplaylinepenalty
	\openup 1\jot \z@dpream \noalign{\vskip-\jot}}
\let\endargue=\endzed

% `syntax' environment: used for syntax rules - even (once!) for VDM.
\def\syntax{\@zed \halign\bgroup
	\strut$\@lign##$\hfil &\hfil$\@lign{}##{}$\hfil
	&$\@lign##$\hfil &\quad\@lign-- ##\hfil\cr}
\let\endsyntax=\endzed

\def\@leftt@p{\vrule height0.4pt\hbox to\zedleftsep{\hrulefill\thinspace}}
\let\leftt@p=\@leftt@p
\def\leftschemas{\let\leftt@p=\relax}

\def\t#1{\hskip #1\zedtab}
\def\flushr#1{\crcr&#1\quad\cr}

% \@zleavevmode -- Enter horizontal mode, taking account of possible
% interaction with lists and section heads:
%	1	After a \item, use \indent to get the label (this
%		fails to run in even short labels).
%	2	After a run-in heading, use \indent.
%	3	After an ordinary heading, throw away the \everypar
%		tokens, reset \@nobreak, and use \noindent with \parskip
%		zero.
%	4	Otherwise, use \noindent with \parskip zero
\def\@zleavevmode{\if@inlabel\indent\else\if@noskipsec\indent\else
	\if@nobreak\global\@nobreakfalse\everypar={}\fi
	{\parskip=0pt\noindent}\fi\fi}

%
% FONTS
%
% The AMS extra symbol fonts are loaded.
%

\def\@fontname{\ifcase\@ptsize m10 scaled \@m%
\or m10 scaled \magstephalf%
\or m10 scaled \magstep1%
\else m\@ptsize\fi}
\font\msx=msx\@fontname % Note: sometimes called euxm10
\font\msy=msy\@fontname % Note: sometimes called euym10

\newfam\msxfam \textfont\msxfam=\msx
\newfam\msyfam \textfont\msyfam=\msy

\def\@famletter#1{\ifcase #1 0\or 1\or 2\or 3\or 4\or 5\or 6\or 7\or
	8\or 9\or A\or B\or C\or D\or E\or F\fi}

\edef\@fx{\@famletter\msxfam}
\edef\@fy{\@famletter\msyfam}

\def\bbold{\fam\msyfam \msy}

%
% Z SYMBOLS
%

\def\token#1{\hbox{`$#1$'}} % makes a quoted expression in mathematical text

\def\report#1{\hbox{`{\tt #1}'}} % used for error messages in Z specs

% \@myop makes an operator, with a strut to defeat TeX's vertical adjustment.
\def\@myop#1{\mathop{\mathstrut{#1}}\nolimits}

% This underscore doesn't have the little kern --- you get an italic
% correction anyway in math mode.
\def\_{\leavevmode \vbox{\hrule width0.5em}}

% Save \q as \xq for quantifiers q.
\let\xforall=\forall
\let\xexists=\exists
\let\xlambda=\lambda
\let\xmu=\mu

% \p and \f make arrows with 1 and 2 crossings resp.
\def\p#1{\mathrel{\ooalign{\hfil$\mapstochar\mkern 5mu$\hfil\cr$#1$}}}
\def\f#1{\mathrel{\ooalign{\hfil
	$\mapstochar\mkern 3mu\mapstochar\mkern 5mu$\hfil\cr$#1$}}}

\let\@mc=\mathchardef

% In the same order as the Z reference manual ...

% Chapter 1
\def \lblot	{\langle\!\left|}
\def \rblot	{\right|\!\rangle}

% Chapter 2
\def \defs	{\mathrel{\widehat=}}
\def \power	{\@myop{\bbold P}}
\let \cross	\times
\def \lambda	{\@myop{\xlambda}}
\def \mu	{\@myop{\xmu}}
\def \lbag	{[\![}
\def \rbag	{]\!]}
\def \lnot	{\neg\;}
\def \land	{\mathrel{\wedge}}
\def \lor	{\mathrel{\vee}}
\let \implies	\Rightarrow
\let \iff	\Leftrightarrow
\def \forall	{\@myop{\xforall}}
\def \exists	{\@myop{\xexists}}
\def \spot	{\mathrel{\bullet}}
\def \hide	{\mathrel{\backslash}}
\@mc \project	"3\@fx16
\def \pre	{\@myop{\rm pre}}
\def \semi	{\mathrel{\comp}}
\def \ldata	{\langle\!\langle}
\def \rdata	{\rangle\!\rangle}
\def \shows	{\;\vdash\;}

% Chapter 3
\@mc \empty	"0\@fy3F
\let \rel	\leftrightarrow
\def \dom	{\@myop{\rm dom}}
\def \ran	{\@myop{\rm ran}}
\def \id	{\@myop{\rm id}}
\def \comp	{\mathbin{\raise 0.6ex\hbox{\oalign{\hfil$\scriptscriptstyle
		 \rm o$\hfil\cr\hfil$\scriptscriptstyle\rm 9$\hfil}}}}
\@mc \dres	"2\@fx43
\@mc \rres	"2\@fx42
\def \ndres	{\mathbin{\rlap{$-$}{\dres}}}
\def \nrres	{\mathbin{\rlap{$-$}{\rres}}}
\def \limg	{(\!\left|}
\def \rimg	{\right|\!)}
\def \pfun	{\p\fun}
\let \fun	\rightarrow
\def \pinj	{\p\inj}
\@mc \inj	"3\@fx1A
\def \psurj	{\p\surj}
\def \surj	{\mathrel{\ooalign{$\fun$\hfil\cr$\mkern4mu\fun$}}}
\def \bij	{\mathrel{\ooalign{$\inj$\hfil\cr$\mkern5mu\fun$}}}
\def \nat	{{\bbold N}}
\def \num	{{\bbold Z}}
\def \div	{\mathbin{\rm div}}
\def \mod	{\mathbin{\rm mod}}
\def \upto	{\mathbin{\ldotp\ldotp}}
\def \finset	{\@myop{\bbold F}}
\def \ffun	{\f\fun}
\def \finj	{\f\inj}
\def \seq	{\@myop{\rm seq}}
\def \cat	{\mathbin{\raise 0.8ex\hbox{$\mathchar"2\@fx61$}}}
\@mc \filter	"2\@fx16
\def \dcat	{\@myop{\cat/}}
\def \disjoint  {{\rm disjoint}\;}
\def \partition {\mathrel{\rm partition}}
\def \bag	{\@myop{\rm bag}}
\def \inbag     {\mathrel{\rm in}}