The oz package^{∗}

edited by Sebastian Rahtz S.Rahtz@elsevier.co.uk

1995/10/03

Contents

1 Introduction 1 1.1 Modification History . . . . . . . . . . . . . . . . . . . . . . . . . . 2

2 Z fonts 4

3 Z symbols 5

4 Utility macros for Z symbols 6

5 Amstex symbol definitions 7

6 Z environments 17 6.1 Margin stack . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 6.2 Utility macros for Z environments . . . . . . . . . . . . . . . . . . 18

6.2.1 Format and control macros . . . . . . . . . . . . . . . . . . 18 6.3 Macros for margins . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 6.4 Macros for drawing boxes . . . . . . . . . . . . . . . . . . . . . . . 19 6.5 Macros for setting up Z environments . . . . . . . . . . . . . . . . 20 6.6 Spacing commands . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 6.7 Environment-breaking commands . . . . . . . . . . . . . . . . . . . 21

7 Utility macros for Object-Z 21

8 Non-box environments 22 8.1 Boxed environments . . . . . . . . . . . . . . . . . . . . . . . . . . 23 8.2 Other environments . . . . . . . . . . . . . . . . . . . . . . . . . . 24

1 Introduction

This file provides macros to type Object Z schemas.

∗This file has version number 2.41, last revised 1995/10/03.

1.1 Modification History

The original zed.sty file was written by Mike Spivey. These macros have been extensively modified to include extra symbols and environments for Object-Z and now have little resemblence to the original macros. Mike Spivey has also extended his macros along different lines for Z — the latest version of macros are called fuzz.sty and come with a syntax checker for Z. They can be purchased for a small

fee from: mike@prg.oxford.ac.uk

87  original zed.sty file — Mike Spivey

88 modified to include extra symbols and environ-

ments — Paul King

88 modified to include macros for UQ editor — Ray

Neucom

May 89 modified to include object-oriented constructs —

PK

Jun 89 modified to automatically change Z symbol size

— PK

27 Jul 89 removed spurious space from \@setsize — PK
3 Aug 89 adjust style of equation number field — PK

24 Aug 89 add optional field to topline and zedline for proofs

— PK

15 Sep 89 added extra qed symbols, updated classcom and

comment — PK

25 Sep 89 renamed z@[bB]ig to z[bB]ig and changed tempo-

ral symbols — PK

30 Sep 89 added \znewpage, \Infrule, removed space

above state box — PK

12 Mar 90 changed \@setsize to work better for double-

spaced text — PK

31 Mar 90 added definition for @ and \bool and redefined

‘;’ — PK

9 May 90 changed \sdef to \varsdef, \sdef & \defs to

Spivey’s latest — PK

27 May 90 added \c{n}{text} — a tab like \t{n} with text

at left — PK

29 May 90 added ‘corners’ to boxes and \zedcornerheight

— PK

11 Jul 90 added \rename*[y/x] and \zseq \zset ...,

changed \zeq \zimp — PK

2 Aug 90 added subseq — PK

9 Nov 90 changed \M to hopefully interact better with spac-

ing — PK

24 Feb 92 changed to work with NFSS — Sebastian Rahtz
29 Dec 92 changed to work with NFSS2 — Sebastian Rahtz
23 Dec 93 checked for \LaTeXe

6 Jan 94 checked again for \LaTeXe with help of David

Carlisle

7 Apr 94 checked again, bundle files added

13 Aug 94 removed hard-wired number of family for math letters removed definition of \c as it prevents cedilla from working

22 Feb 95 updated for AMSLaTeX 2.1 and Lucida compatibility

Please post any updates that you may make to this file to: Paul King – ACSnet: king@batserver.cs.uq.oz.au

1 ⟨∗package⟩

 2 \NeedsTeXFormat{LaTeX2e}[1994/12/01]
 3 \ProvidesPackage{oz}[\filedate\space\fileversion\space Object Z macros]

The L^{A}TEX 2ε parbox code is much more complicated, so we get back a simpler world from L^{A}TEX209.

 4 \def\oz@parbox{\@ifnextchar [{\oz@iparbox}{\oz@iparbox[c]}}
 5 \long\def\oz@iparbox[#1]#2#3{\leavevmode \@pboxswfalse
 6 \if #1b\vbox
 7  \else \if #1t\vtop
 8  \else \vbox
 9  %\ifmmode \vcenter \else \@pboxswtrue $\vcenter \fi
10  \fi
11  \fi
12 {\hsize #2\@parboxrestore #3}
13  %\if@pboxsw \m@th$\fi

14 }

2 Z fonts

The AMS extra symbol fonts are loaded if we are not using Lucida New Math. Note: msam and msbm sometimes called euxm and euym respectively NOTE: the new AMSFONTS 2.0 call these fonts msam and msbm repectively (the fonts below need to be renamed if you want to use the new fonts)

15 \@ifpackageloaded{lucbr}{}{%
16 \DeclareMathVersion{oz}
17 \SetMathAlphabet{\mathrm}{oz}{\encodingdefault}{\rmdefault}{m}{n}%
18 \SetMathAlphabet{\mathbf}{oz}{\encodingdefault}{\rmdefault}{bx}{n}%
19 \SetMathAlphabet{\mathsf}{oz}{\encodingdefault}{\sfdefault}{m}{n}%
20 \DeclareSymbolFont{italics}{\encodingdefault}{\rmdefault}{m}{it}%
21 \DeclareSymbolFontAlphabet{\mathrm}{operators}
22 \DeclareSymbolFontAlphabet{\mathit}{letters}
23 \DeclareSymbolFontAlphabet{\mathcal}{symbols}
24 \DeclareSymbolFontAlphabet{\ozit}{italics}
25 \DeclareSymbolFont{lasy}{U}{lasy}{m}{n}
26 \DeclareSymbolFont{AMSa}{U}{msa}{m}{n}
27 \DeclareSymbolFont{AMSb}{U}{msb}{m}{n}
28 \let\mho\undefined
29 \let\Join\undefined
30 \let\Box\undefined
31 \let\Diamond\undefined
32 \let\leadsto\undefined
33 \let\sqsubset\undefined
34 \let\sqsupset\undefined
35 \let\lhd\undefined
36 \let\unlhd\undefined
37 \let\rhd\undefined
38 \let\unrhd\undefined
39 \DeclareMathSymbol{\mho}{\mathord}{lasy}{"30}
40 \DeclareMathSymbol{\Join}{\mathrel}{lasy}{"31}
41 \DeclareMathSymbol{\Box}{\mathord}{lasy}{"32}
42 \DeclareMathSymbol{\Diamond}{\mathord}{lasy}{"33}
43 \DeclareMathSymbol{\leadsto}{\mathrel}{lasy}{"3B}
44 \DeclareMathSymbol{\sqsubset}{\mathrel}{lasy}{"3C}

45 \DeclareMathSymbol{\sqsupset}{\mathrel}{lasy}{"3D}
46 \DeclareMathSymbol{\lhd}{\mathrel}{lasy}{"01}
47 \DeclareMathSymbol{\unlhd}{\mathrel}{lasy}{"02}
48 \DeclareMathSymbol{\rhd}{\mathrel}{lasy}{"03}
49 \DeclareMathSymbol{\unrhd}{\mathrel}{lasy}{"04}
50 \DeclareSymbolFontAlphabet{\mathbb}{AMSb}
51 \mathversion{oz}

52 }

Allow change of size within schemas. This is a sod to get right; my principle (eventually!) was to go out of math temporarily, change size, go into an inner math, do the business, then get out of math and back to outer math.

53 \newbox\strutbox@
54 \def\strut@{\copy\strutbox@}
55 \addto@hook\every@math@size{%
56  \setbox\strutbox@\hbox{\lower.5\normallineskiplimit
57 \vbox{\kern-\normallineskiplimit\copy\strutbox}}}
58 \def\bBigg@#1#2{%
59 \mbox{\ifcase#1\or\large\or\Large\or\LARGE\or\small\or\footnotesize\fi
60 $#2$}\nulldelimiterspace\z@ \m@th}
61 \addto@hook\every@math@size{\setbox\z@\vbox{\hbox{$($}\kern\z@}%
62 \big@size 1.2\ht\z@}
63 \newdimen\big@size
64 \def\zBIG{\bBigg@{3}}
65 \def\zBig{\bBigg@{2}}
66 \def\zbig{\bBigg@{1}}
67 \def\zsmall{\bBigg@{4}}
68 \def\zSmall{\bBigg@{5}}

WORD STYLES these need handling a bit differently in NFSS from the original.

69 \def\String#1{\hbox{`\texttt{#1}'}}
70 \def\STRING#1{\hbox{``\texttt{#1}''}}
71 \def\infix#1{\z@rel{{\underline{#1}}}}
72 \def\word#1{\z@op{#1}}
73 \def\keyword#1{\z@op{\mbox{\textrm{#1}}}}
74 \def\boldword#1{\z@op{\mbox{\textbf{#1}}}}
75 \def\underword#1{\z@op{{\underline{#1}}}}
76 \def\underkeyword#1{\z@op{{\underline{\mbox{\textrm{#1}}}}}}
77 \def\underboldword#1{\z@op{{\underline{\mbox{\textbf{#1}}}}}}

3 Z symbols

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.

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

Use \hexnumber@\symitalics in case other families are loaded before. (from D. Roegel, July 13, 1994)

81 \@setmcodes{`A}{`Z}{"7\hexnumber@\symitalics41}
82 \@setmcodes{`a}{`z}{"7\hexnumber@\symitalics61}

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.

83 \let\@mc=\mathchardef
84 \mathcode`\;="8000 % Makes ; active in math mode
85 {\catcode`\;=\active \gdef;{\semicolon\;}}
86 \@mc\semicolon="603B

4 Utility macros for Z symbols

\z@op makes a large math operator
\z@rel makes a math relation
\z@bin makes a binary operator

Each use a mathstrut to defeat TeX’s vertical adjustment. \z@bigXXX is a big version of symbol

87 \def\z@op#1{\mathop{\mathstrut{#1}}\nolimits}
88 \def\z@bin#1{\mathbin{\mathstrut{#1}}}
89 \def\z@rel#1{\mathrel{\mathstrut{#1}}}

90 %

91 \def\z@bigop#1{\z@op{\zbig{#1}}}
92 \def\z@bigbin#1{\z@bin{\zbig{#1}}}
93 \def\z@bigrel#1{\z@rel{\zbig{#1}}}

94 %

95 \def\z@Bigop#1{\z@op{\zBig{#1}}}
96 \def\z@Bigbin#1{\z@bin{\zBig{#1}}}
97 \def\z@Bigrel#1{\z@rel{\zBig{#1}}}

98 %

99 \def\z@smallop#1{\z@op{\zsmall{#1}}}
100 \def\z@smallbin#1{\z@bin{\zsmall{#1}}}
101 \def\z@smallrel#1{\z@rel{\zsmall{#1}}}

This underscore doesn’t have the little kern — you get an italic correction anyway in math mode.

102 \def\_{\leavevmode \vbox{\hrule width0.4em}}

Save \q as \xq for quantifiers q.

103 \let\xforall=\forall
104 \let\xexists=\exists
105 \let\xlambda=\lambda
106 \let\xmu=\mu

Save other symbols

107 \let\xsucc\succ
108 \let\xprec\prec
109 \let\dotaccent=\dot
110 \let\sectionsymbol=\S
111 \let\integral=\int
112 \let\product\prod

\p and \f make arrows with 1 and 2 crossings resp.

113 \def\p#1{\mathrel{\ooalign{\hfil$\mapstochar\mkern 5mu$\hfil\cr$#1$}}}

114 \def\f#1{\mathrel{\ooalign{\hfil
115  $\mapstochar\mkern 3mu\mapstochar\mkern 5mu$\hfil\cr$#1$}}}
116 \@ifpackageloaded{lucbr}{%
117 \DeclareMathSymbol{\doublebarwedge}{\mathbin}{symbols}{"D4}
118 \DeclareMathSymbol{\lll}{\mathrel}{letters}{"DE}
119 \DeclareMathSymbol{\ggg}{\mathrel}{letters}{"DF}
120 \DeclareMathSymbol{\eth}{\mathrel}{operators}{"F0}
121 }{%

5 Amstex symbol definitions

Do these before Z symbols so that we can use them in our special symbols. AMSa font:

122 \let\rightleftharpoons\undefined
123 \let\angle\undefined
124 \DeclareMathSymbol\boxdot{\mathbin}{AMSa}{"00}
125 \DeclareMathSymbol\boxplus{\mathbin}{AMSa}{"01}
126 \DeclareMathSymbol\boxtimes{\mathbin}{AMSa}{"02}
127 \DeclareMathSymbol\square{\mathord}{AMSa}{"03}
128 \DeclareMathSymbol\blacksquare{\mathord}{AMSa}{"04}
129 \DeclareMathSymbol\centerdot{\mathbin}{AMSa}{"05}
130 \DeclareMathSymbol\lozenge{\mathord}{AMSa}{"06}
131 \DeclareMathSymbol\blacklozenge{\mathord}{AMSa}{"07}
132 \DeclareMathSymbol\circlearrowright{\mathrel}{AMSa}{"08}
133 \DeclareMathSymbol\circlearrowleft{\mathrel}{AMSa}{"09}
134 \DeclareMathSymbol\rightleftharpoons{\mathrel}{AMSa}{"0A}
135 \DeclareMathSymbol\leftrightharpoons{\mathrel}{AMSa}{"0B}
136 \DeclareMathSymbol\boxminus{\mathbin}{AMSa}{"0C}
137 \DeclareMathSymbol\Vdash{\mathrel}{AMSa}{"0D}
138 \DeclareMathSymbol\Vvdash{\mathrel}{AMSa}{"0E}
139 \DeclareMathSymbol\vDash{\mathrel}{AMSa}{"0F}
140 \DeclareMathSymbol\twoheadrightarrow{\mathrel}{AMSa}{"10}
141 \DeclareMathSymbol\twoheadleftarrow{\mathrel}{AMSa}{"11}
142 \DeclareMathSymbol\leftleftarrows{\mathrel}{AMSa}{"12}
143 \DeclareMathSymbol\rightrightarrows{\mathrel}{AMSa}{"13}
144 \DeclareMathSymbol\upuparrows{\mathrel}{AMSa}{"14}
145 \DeclareMathSymbol\downdownarrows{\mathrel}{AMSa}{"15}
146 \DeclareMathSymbol\upharpoonright{\mathrel}{AMSa}{"16}
147 \DeclareMathSymbol\downharpoonright{\mathrel}{AMSa}{"17}
148 \DeclareMathSymbol\upharpoonleft{\mathrel}{AMSa}{"18}
149 \DeclareMathSymbol\downharpoonleft{\mathrel}{AMSa}{"19}
150 \DeclareMathSymbol\rightarrowtail{\mathrel}{AMSa}{"1A}
151 \DeclareMathSymbol\leftarrowtail{\mathrel}{AMSa}{"1B}
152 \DeclareMathSymbol\leftrightarrows{\mathrel}{AMSa}{"1C}
153 \DeclareMathSymbol\rightleftarrows{\mathrel}{AMSa}{"1D}
154 \DeclareMathSymbol\Lsh{\mathrel}{AMSa}{"1E}
155 \DeclareMathSymbol\Rsh{\mathrel}{AMSa}{"1F}
156 \DeclareMathSymbol\rightsquigarrow{\mathrel}{AMSa}{"20}
157 \DeclareMathSymbol\leftrightsquigarrow{\mathrel}{AMSa}{"21}
158 \DeclareMathSymbol\looparrowleft{\mathrel}{AMSa}{"22}
159 \DeclareMathSymbol\looparrowright{\mathrel}{AMSa}{"23}
160 \DeclareMathSymbol\circeq{\mathrel}{AMSa}{"24}
161 \DeclareMathSymbol\succsim{\mathrel}{AMSa}{"25}

162 \DeclareMathSymbol\gtrsim{\mathrel}{AMSa}{"26}
163 \DeclareMathSymbol\gtrapprox{\mathrel}{AMSa}{"27}
164 \DeclareMathSymbol\multimap{\mathrel}{AMSa}{"28}
165 \DeclareMathSymbol\therefore{\mathrel}{AMSa}{"29}
166 \DeclareMathSymbol\because{\mathrel}{AMSa}{"2A}
167 \DeclareMathSymbol\doteqdot{\mathrel}{AMSa}{"2B}
168 \DeclareMathSymbol\triangleq{\mathrel}{AMSa}{"2C}
169 \DeclareMathSymbol\precsim{\mathrel}{AMSa}{"2D}
170 \DeclareMathSymbol\lesssim{\mathrel}{AMSa}{"2E}
171 \DeclareMathSymbol\lessapprox{\mathrel}{AMSa}{"2F}
172 \DeclareMathSymbol\eqslantless{\mathrel}{AMSa}{"30}
173 \DeclareMathSymbol\eqslantgtr{\mathrel}{AMSa}{"31}
174 \DeclareMathSymbol\curlyeqprec{\mathrel}{AMSa}{"32}
175 \DeclareMathSymbol\curlyeqsucc{\mathrel}{AMSa}{"33}
176 \DeclareMathSymbol\preccurlyeq{\mathrel}{AMSa}{"34}
177 \DeclareMathSymbol\leqq{\mathrel}{AMSa}{"35}
178 \DeclareMathSymbol\leqslant{\mathrel}{AMSa}{"36}
179 \DeclareMathSymbol\lessgtr{\mathrel}{AMSa}{"37}
180 \DeclareMathSymbol\backprime{\mathord}{AMSa}{"38}
181 \DeclareMathSymbol\risingdotseq{\mathrel}{AMSa}{"3A}
182 \DeclareMathSymbol\fallingdotseq{\mathrel}{AMSa}{"3B}
183 \DeclareMathSymbol\succcurlyeq{\mathrel}{AMSa}{"3C}
184 \DeclareMathSymbol\geqq{\mathrel}{AMSa}{"3D}
185 \DeclareMathSymbol\geqslant{\mathrel}{AMSa}{"3E}
186 \DeclareMathSymbol\gtrless{\mathrel}{AMSa}{"3F}
187 \DeclareMathSymbol\sqsubset{\mathrel}{AMSa}{"40}
188 \DeclareMathSymbol\sqsupset{\mathrel}{AMSa}{"41}
189 \DeclareMathSymbol\vartriangleright{\mathrel}{AMSa}{"42}
190 \DeclareMathSymbol\vartriangleleft{\mathrel}{AMSa}{"43}
191 \DeclareMathSymbol\trianglerighteq{\mathrel}{AMSa}{"44}
192 \DeclareMathSymbol\trianglelefteq{\mathrel}{AMSa}{"45}
193 \DeclareMathSymbol\bigstar{\mathord}{AMSa}{"46}
194 \DeclareMathSymbol\between{\mathrel}{AMSa}{"47}
195 \DeclareMathSymbol\blacktriangledown{\mathord}{AMSa}{"48}
196 \DeclareMathSymbol\blacktriangleright{\mathrel}{AMSa}{"49}
197 \DeclareMathSymbol\blacktriangleleft{\mathrel}{AMSa}{"4A}
198 \DeclareMathSymbol\vartriangle{\mathord}{AMSa}{"4D}
199 \DeclareMathSymbol\blacktriangle{\mathord}{AMSa}{"4E}
200 \DeclareMathSymbol\triangledown{\mathord}{AMSa}{"4F}
201 \DeclareMathSymbol\eqcirc{\mathrel}{AMSa}{"50}
202 \DeclareMathSymbol\lesseqgtr{\mathrel}{AMSa}{"51}
203 \DeclareMathSymbol\gtreqless{\mathrel}{AMSa}{"52}
204 \DeclareMathSymbol\lesseqqgtr{\mathrel}{AMSa}{"53}
205 \DeclareMathSymbol\gtreqqless{\mathrel}{AMSa}{"54}
206 \DeclareMathSymbol\Rrightarrow{\mathrel}{AMSa}{"56}
207 \DeclareMathSymbol\Lleftarrow{\mathrel}{AMSa}{"57}
208 \DeclareMathSymbol\veebar{\mathbin}{AMSa}{"59}
209 \DeclareMathSymbol\barwedge{\mathbin}{AMSa}{"5A}
210 \DeclareMathSymbol\doublebarwedge{\mathbin}{AMSa}{"5B}
211 \DeclareMathSymbol\angle{\mathord}{AMSa}{"5C}
212 \DeclareMathSymbol\measuredangle{\mathord}{AMSa}{"5D}
213 \DeclareMathSymbol\sphericalangle{\mathord}{AMSa}{"5E}
214 \DeclareMathSymbol\varpropto{\mathrel}{AMSa}{"5F}
215 \DeclareMathSymbol\smallsmile{\mathrel}{AMSa}{"60}

216 \DeclareMathSymbol\smallfrown{\mathrel}{AMSa}{"61}
217 \DeclareMathSymbol\Subset{\mathrel}{AMSa}{"62}
218 \DeclareMathSymbol\Supset{\mathrel}{AMSa}{"63}
219 \DeclareMathSymbol\Cup{\mathbin}{AMSa}{"64}
220 \DeclareMathSymbol\Cap{\mathbin}{AMSa}{"65}
221 \DeclareMathSymbol\curlywedge{\mathbin}{AMSa}{"66}
222 \DeclareMathSymbol\curlyvee{\mathbin}{AMSa}{"67}
223 \DeclareMathSymbol\leftthreetimes{\mathbin}{AMSa}{"68}
224 \DeclareMathSymbol\rightthreetimes{\mathbin}{AMSa}{"69}
225 \DeclareMathSymbol\subseteqq{\mathrel}{AMSa}{"6A}
226 \DeclareMathSymbol\supseteqq{\mathrel}{AMSa}{"6B}
227 \DeclareMathSymbol\bumpeq{\mathrel}{AMSa}{"6C}
228 \DeclareMathSymbol\Bumpeq{\mathrel}{AMSa}{"6D}
229 \DeclareMathSymbol\lll{\mathrel}{AMSa}{"6E}
230 \DeclareMathSymbol\ggg{\mathrel}{AMSa}{"6F}
231 \DeclareMathDelimiter\ulcorner{4}{AMSa}{"70}{AMSa}{"70}
232 \DeclareMathDelimiter\urcorner{5}{AMSa}{"71}{AMSa}{"71}
233 \DeclareMathDelimiter\llcorner{4}{AMSa}{"78}{AMSa}{"78}
234 \DeclareMathDelimiter\lrcorner{5}{AMSa}{"79}{AMSa}{"79}
235 \xdef\yen  {\noexpand\mathhexbox\hexnumber@\symAMSa 55 }
236 \xdef\checkmark{\noexpand\mathhexbox\hexnumber@\symAMSa 58 }
237 \xdef\circledR {\noexpand\mathhexbox\hexnumber@\symAMSa 72 }
238 \xdef\maltese  {\noexpand\mathhexbox\hexnumber@\symAMSa 7A }
239 \DeclareMathSymbol\circledS{\mathord}{AMSa}{"73}
240 \DeclareMathSymbol\pitchfork{\mathrel}{AMSa}{"74}
241 \DeclareMathSymbol\dotplus{\mathbin}{AMSa}{"75}
242 \DeclareMathSymbol\backsim{\mathrel}{AMSa}{"76}
243 \DeclareMathSymbol\backsimeq{\mathrel}{AMSa}{"77}
244 \DeclareMathSymbol\complement{\mathord}{AMSa}{"7B}
245 \DeclareMathSymbol\intercal{\mathbin}{AMSa}{"7C}
246 \DeclareMathSymbol\circledcirc{\mathbin}{AMSa}{"7D}
247 \DeclareMathSymbol\circledast{\mathbin}{AMSa}{"7E}
248 \DeclareMathSymbol\circleddash{\mathbin}{AMSa}{"7F}

AMSb font:

249 \DeclareMathSymbol\lvertneqq{\mathrel}{AMSb}{"00}
250 \DeclareMathSymbol\gvertneqq{\mathrel}{AMSb}{"01}
251 \DeclareMathSymbol\nleq{\mathrel}{AMSb}{"02}
252 \DeclareMathSymbol\ngeq{\mathrel}{AMSb}{"03}
253 \DeclareMathSymbol\nless{\mathrel}{AMSb}{"04}
254 \DeclareMathSymbol\ngtr{\mathrel}{AMSb}{"05}
255 \DeclareMathSymbol\nprec{\mathrel}{AMSb}{"06}
256 \DeclareMathSymbol\nsucc{\mathrel}{AMSb}{"07}
257 \DeclareMathSymbol\lneqq{\mathrel}{AMSb}{"08}
258 \DeclareMathSymbol\gneqq{\mathrel}{AMSb}{"09}
259 \DeclareMathSymbol\nleqslant{\mathrel}{AMSb}{"0A}
260 \DeclareMathSymbol\ngeqslant{\mathrel}{AMSb}{"0B}
261 \DeclareMathSymbol\lneq{\mathrel}{AMSb}{"0C}
262 \DeclareMathSymbol\gneq{\mathrel}{AMSb}{"0D}
263 \DeclareMathSymbol\npreceq{\mathrel}{AMSb}{"0E}
264 \DeclareMathSymbol\nsucceq{\mathrel}{AMSb}{"0F}
265 \DeclareMathSymbol\precnsim{\mathrel}{AMSb}{"10}
266 \DeclareMathSymbol\succnsim{\mathrel}{AMSb}{"11}
267 \DeclareMathSymbol\lnsim{\mathrel}{AMSb}{"12}

268 \DeclareMathSymbol\gnsim{\mathrel}{AMSb}{"13}
269 \DeclareMathSymbol\nleqq{\mathrel}{AMSb}{"14}
270 \DeclareMathSymbol\ngeqq{\mathrel}{AMSb}{"15}
271 \DeclareMathSymbol\precneqq{\mathrel}{AMSb}{"16}
272 \DeclareMathSymbol\succneqq{\mathrel}{AMSb}{"17}
273 \DeclareMathSymbol\precnapprox{\mathrel}{AMSb}{"18}
274 \DeclareMathSymbol\succnapprox{\mathrel}{AMSb}{"19}
275 \DeclareMathSymbol\lnapprox{\mathrel}{AMSb}{"1A}
276 \DeclareMathSymbol\gnapprox{\mathrel}{AMSb}{"1B}
277 \DeclareMathSymbol\nsim{\mathrel}{AMSb}{"1C}
278 \DeclareMathSymbol\ncong{\mathrel}{AMSb}{"1D}
279 %\DeclareMathSymbol\varsubsetneq{\mathrel}{AMSb}{"20}
280 %\DeclareMathSymbol\varsupsetneq{\mathrel}{AMSb}{"21}
281 \DeclareMathSymbol\nsubseteqq{\mathrel}{AMSb}{"22}
282 \DeclareMathSymbol\nsupseteqq{\mathrel}{AMSb}{"23}
283 \DeclareMathSymbol\subsetneqq{\mathrel}{AMSb}{"24}
284 \DeclareMathSymbol\supsetneqq{\mathrel}{AMSb}{"25}
285 %\DeclareMathSymbol\varsubsetneqq{\mathrel}{AMSb}{"26}
286 %\DeclareMathSymbol\varsupsetneqq{\mathrel}{AMSb}{"27}
287 \DeclareMathSymbol\subsetneq{\mathrel}{AMSb}{"28}
288 \DeclareMathSymbol\supsetneq{\mathrel}{AMSb}{"29}
289 \DeclareMathSymbol\nsubseteq{\mathrel}{AMSb}{"2A}
290 \DeclareMathSymbol\nsupseteq{\mathrel}{AMSb}{"2B}
291 \DeclareMathSymbol\nparallel{\mathrel}{AMSb}{"2C}
292 \DeclareMathSymbol\nmid{\mathrel}{AMSb}{"2D}
293 \DeclareMathSymbol\nshortmid{\mathrel}{AMSb}{"2E}
294 \DeclareMathSymbol\nshortparallel{\mathrel}{AMSb}{"2F}
295 \DeclareMathSymbol\nvdash{\mathrel}{AMSb}{"30}
296 \DeclareMathSymbol\nVdash{\mathrel}{AMSb}{"31}
297 \DeclareMathSymbol\nvDash{\mathrel}{AMSb}{"32}
298 \DeclareMathSymbol\nVDash{\mathrel}{AMSb}{"33}
299 \DeclareMathSymbol\ntrianglerighteq{\mathrel}{AMSb}{"34}
300 \DeclareMathSymbol\ntrianglelefteq{\mathrel}{AMSb}{"35}
301 \DeclareMathSymbol\ntriangleleft{\mathrel}{AMSb}{"36}
302 \DeclareMathSymbol\ntriangleright{\mathrel}{AMSb}{"37}
303 \DeclareMathSymbol\nleftarrow{\mathrel}{AMSb}{"38}
304 \DeclareMathSymbol\nrightarrow{\mathrel}{AMSb}{"39}
305 \DeclareMathSymbol\nLeftarrow{\mathrel}{AMSb}{"3A}
306 \DeclareMathSymbol\nRightarrow{\mathrel}{AMSb}{"3B}
307 \DeclareMathSymbol\nLeftrightarrow{\mathrel}{AMSb}{"3C}
308 \DeclareMathSymbol\nleftrightarrow{\mathrel}{AMSb}{"3D}
309 \DeclareMathSymbol\divideontimes{\mathbin}{AMSb}{"3E}
310 \DeclareMathSymbol\varnothing{\mathord}{AMSb}{"3F}
311 \DeclareMathSymbol\mho{\mathord}{AMSb}{"66}
312 \DeclareMathSymbol\eth{\mathord}{AMSb}{"67}
313 \DeclareMathSymbol\eqsim{\mathrel}{AMSb}{"68}
314 \DeclareMathSymbol\beth{\mathord}{AMSb}{"69}
315 \DeclareMathSymbol\gimel{\mathord}{AMSb}{"6A}
316 \DeclareMathSymbol\daleth{\mathord}{AMSb}{"6B}
317 \DeclareMathSymbol\lessdot{\mathrel}{AMSb}{"6C}
318 \DeclareMathSymbol\gtrdot{\mathrel}{AMSb}{"6D}
319 \DeclareMathSymbol\ltimes{\mathbin}{AMSb}{"6E}
320 \DeclareMathSymbol\rtimes{\mathbin}{AMSb}{"6F}
321 \DeclareMathSymbol\shortmid{\mathrel}{AMSb}{"70}

322 \DeclareMathSymbol\shortparallel{\mathrel}{AMSb}{"71}
323 \DeclareMathSymbol\smallsetminus{\mathbin}{AMSb}{"72}
324 \DeclareMathSymbol\thicksim{\mathrel}{AMSb}{"73}
325 \DeclareMathSymbol\thickapprox{\mathrel}{AMSb}{"74}
326 \DeclareMathSymbol\approxeq{\mathrel}{AMSb}{"75}
327 \DeclareMathSymbol\succapprox{\mathrel}{AMSb}{"76}
328 \DeclareMathSymbol\precapprox{\mathrel}{AMSb}{"77}
329 \DeclareMathSymbol\curvearrowleft{\mathrel}{AMSb}{"78}
330 \DeclareMathSymbol\curvearrowright{\mathrel}{AMSb}{"79}
331 \DeclareMathSymbol\digamma{\mathord}{AMSb}{"7A}
332 \DeclareMathSymbol\varkappa{\mathord}{AMSb}{"7B}
333 \DeclareMathSymbol\hslash{\mathord}{AMSb}{"7D}
334 \DeclareMathSymbol\hbar{\mathord}{AMSb}{"7E}
335 \DeclareMathSymbol\backepsilon{\mathrel}{AMSb}{"7F}

336 }

337 \def\interleave{{\parallel\!\!\vert}}
338 \def\shortinterleave{\z@rel{\mathord\shortmid\mathord\shortparallel}}
339 \def\napprox{\not\approx}
340 \let\restriction\upharpoonright
341 \let\Doteq\doteqdot
342 \let\doublecup\Cup
343 \let\llless\lll
344 \let\gggtr\ggg
345 \let\doublecap\Cap

Numbers

346 \def \nat   {{\mathbb N}}
347 \def \integer   {{\mathbb Z}}
348 \def \natone    {{\mathbb N}_1}
349 \def \real  {{\mathbb R}}
350 \def \bool  {{\mathbb B}}
351 \let \divides   \div
352 \def \div   {\z@bin{\mathrm{div}}}
353 \def \mod   {\z@bin{\mathrm{mod}}}
354 \def \succ  {\word{succ}}
355 \def \expon {^}

aliases

356 \let \num   \integer
357 \let \nplus \natone

Logic

358 \def \lnot  {\neg\;}
359 \def \land  {\z@rel{\wedge}}
360 \def \lor   {\z@rel{\vee}}
361 \let \imp   \Rightarrow
362 \let\iff    \Leftrightarrow
363 \def \all   {\z@op{\xforall}}
364 \def \exi   {\z@op{\xexists}}
365 \def \exione    {\exists_1}
366 \@ifpackageloaded{lucbr}{%
367 \DeclareMathSymbol{\nexi}{0}{arrows}{"20}
368 }{%
369 \DeclareMathSymbol{\nexi}{\mathord}{AMSb}{"40}

370 }

371 \def \dot   {\z@rel{\bullet}}
372 \def \true  {\keyword{true}}
373 \def \false {\keyword{false}}
374 \let \cond  \rightarrow

aliases

375 \let \spot  \dot
376 \mathcode`\@="8000% make @ active in mathmode
377 {\catcode`\@=\active \gdef@{\dot}}
378 \let \implies   \imp
379 \let \forall    \all
380 \let \exists    \exi
381 \let \nexists   \nexi

SETS

382 \let \emptyset  \varnothing
383 \def \varemptyset  {\{\,\}}
384 \def \pset  {\z@op{\mathbb P}}
385 \def \psetone   {\pset_1}
386 \def \fset  {\z@op{\mathbb F}}
387 \def \fsetone   {\fset_1}
388 \def \sset  {\z@op{\mathbb S}}
389 \let \mem   \in
390 \def \nem   {\not\mem}
391 \def \uni   {\z@bin\cup}
392 \def \int   {\z@bin\cap}
393 \let \prod  \times
394 \def \min   {\word{min}}
395 \def \max   {\word{max}}
396 \def \duni  {\z@Bigop{\lower0.25ex\hbox{$\uni$}}}
397 \def \dint  {\z@Bigop{\lower0.25ex\hbox{$\int$}}}
398 \def \upto  {\z@bin{\ldotp\ldotp}}
399 \let \psubs \subset
400 \let \subs  \subseteq
401 \let \psups \supset
402 \let \sups  \supseteq
403 \def \diff  {\z@bin{\backslash}}

aliases

404 \let \cross \prod
405 \let \notin \nem
406 \let \nmem  \nem
407 \let \union \uni
408 \let \inter \int
409 \let \power \pset
410 \let \finset    \fset
411 \let \dunion    \duni
412 \let \dinter    \dint

413 %

RELATIONS & FUNCTIONS

414 \def \lambda    {\z@op{\xlambda}}
415 \def \mu    {\z@op{\xmu}}
416 \def \dom   {\keyword{dom}}
417 \def \ran   {\keyword{ran}}

418 \def \id    {\keyword{id}}
419 \@ifpackageloaded{lucbr}{%
420 \DeclareMathSymbol{\dres}{\mathbin}{letters}{"2F}
421 \DeclareMathSymbol{\rres}{\mathbin}{letters}{"2E}
422 }{%
423 \DeclareMathSymbol{\dres}{\mathbin}{AMSa}{"43}
424 \DeclareMathSymbol{\rres}{\mathbin}{AMSa}{"42}

425 }

426 \def \dsub  {\mathbin{\rlap{\raise.05ex\hbox{$-$}}{\dres}}}
427 \def \rsub  {\mathbin{\rlap{\raise.05ex\hbox{$-$}}{\rres}}}
428 \let \fovr  \oplus
429 \let \cmp   \circ
430 \def \fcmp  {\mathbin{\raise 0.6ex\hbox{\oalign{\hfil$\scriptscriptstyle
431  \mathrm{o}$\hfil\cr\hfil$\scriptscriptstyle\mathrm{9}$\hfil}}}}
432 \def \inv   {^{-1}}
433 \def \limg  {(\!|}
434 \def \rimg  {|\!)}
435 \let \map   \mapsto
436 \let \rel   \leftrightarrow
437 \let \tfun  \rightarrow
438 \let \tinj  \rightarrowtail
439 \def \tsur  {\mathrel{\ooalign{$\tfun$\hfil\cr$\mkern4mu\tfun$}}}
440 \def \pfun  {\p\tfun}
441 \def \pinj  {\p\tinj}
442 \def \psur  {\p\tsur}
443 \def \ffun  {\f\tfun}
444 \def \finj  {\f\tinj}
445 \def \bij   {\mathrel{\ooalign{$\tinj$\hfil\cr$\mkern5mu\tfun$}}}
446 \def \tcl   {^+}
447 \def \rtcl  {^*}
448 \def \iter  {^}

aliases

449 \let \comp  \fcmp
450 \let \ndres \dsub
451 \let \nrres \rsub
452 \let \fun   \tfun
453 \let \inj   \tinj
454 \let \surj  \tsur
455 \let \psurj \psur
456 \let \llless    \lll
457 \let \gggtr \ggg
458 \def \interleave    {{\parallel\!\!\vert}}
459 \def \shortinterleave   {\z@rel{\mathord\shortmid\mathord\shortparallel}}
460 \let \restriction   \upharpoonright
461 \def \napprox   {\not\approx}

SEQUENCES

462 \def \seq   {\keyword{seq}}
463 \def \seqone    {\seq_1}
464 \def \emptyseq  {\lseq\,\rseq}
465 \let \lseq  \langle
466 \let \rseq  \rangle
467 \def \head  {\word{head}}
468 \def \tail  {\word{tail}}

469 \def \front {\word{front}}
470 \def \last  {\word{last}}
471 \def \rev   {\word{rev}}
472 \def \squash    {\word{squash}}
473 \def \next  {\keyword{next}}
474 \def \inseq {\keyword{in}}
475 \@ifpackageloaded{lucbr}{%
476 \DeclareMathSymbol{\sres}{2}{arrows}{"75}
477 \DeclareMathSymbol{\ires}{2}{arrows}{"76}
478 \DeclareMathSymbol{\@@cat}{\mathbin}{operators}{"5F}
479 }{%
480 \DeclareMathSymbol{\@@cat}{\mathbin}{AMSa}{"61}
481 \DeclareMathSymbol{\sres}{\mathbin}{AMSa}{"16}
482 \DeclareMathSymbol{\ires}{\mathbin}{AMSa}{"18}

483 }

484 \def \cat   {\mathbin{\raise 0.8ex\hbox{$\mathchar\@@cat$}}}
485 \def \ssub  {\z@bin{\rlap{$-$}{\sres}}}
486 \def \isub  {\z@bin{\rlap{$-$}{\ires}}}
487 \def \dcat  {\z@op{\cat/}}
488 \def \dovr  {\z@op{\fovr/}}
489 \def \dcmp  {\z@op{\fcmp/}}
490 \let \prefix    \subseteq
491 \def \suffix    {\keyword{suffix}}
492 \def \seqi  {\keyword{seq_\infty}}
493 \def \partitions    {\keyword{partitions}}
494 \def \disjoint  {\keyword{disjoint}}
495 \def \subseq    {\keyword{subseq}}

aliases

496 \let \filter    \sres

Schemas:

497 \def \lsch  {\z@bigop{[}}
498 \def \rsch  {\z@bigop{]}}
499 \def \dparallel {\z@bigop{\parallel}\limits}
500 \def \zand  {\z@bigbin\land}
501 \def \zor   {\z@bigbin\lor}
502 \def \zcmp  {\z@bigbin\fcmp}
503 \def \zexi  {\z@bigop\exists}
504 \def \zall  {\z@bigop\forall}
505 \def \znot  {\z@bigop\neg}
506 \def \zbar  {\z@bigbin\cbar}
507 \def \zfor  {/}
508 \def \zhide {\z@bigbin\backslash}
509 \def \zimp  {\z@bigrel\imp}
510 \def \zeq   {\z@bigrel\iff}
511 \def \zovr  {\z@bigrel\oplus}
512 \def \zpipe {\z@bigbin{\mathord>\!\!\mathord>}}
513 \def \pre   {\keyword{pre}}
514 \def \pred  {\keyword{pred}}
515 \def \post  {\keyword{post}}
516 \def \zproject  {\z@bigbin\sres}
517 \def\rename{\@ifnextchar*{\z@rename}{\z@@rename}}
518 \def\z@rename*[#1/#2]{\left[#1 \over #2\right]}
519 \def\z@@rename[#1/#2]{\left[#1 \zfor #2\right]}

aliases

520 \let \project   \zproject
521 \let \import    \sres
522 \let \semi  \zcmp
523 \let \hide  \zhide

BAGS

524 \let\buni\uplus
525 \def \emptybag  {\lbag\:\rbag}
526 \def \lbag  {[\![}
527 \def \rbag  {]\!]}
528 \def \bag   {\keyword{bag}}
529 \def \items {\word{items}}
530 \let \inbag \inseq
531 \def \bagcount  {\word{count}}

Definitions & declarations

532 \def \ddef  {\z@rel{\;::=\;}}
533 \def \bbar  {\z@bigrel{|}}
534 \let \cbar  \mid
535 \def \lang  {\langle\!\langle}
536 \def \rang  {\rangle\!\rangle}
537 \def \sdef  {\z@rel{\widehat=}}
538 \def \defs  {\z@smallrel{==}}
539 \def \varsdef   {\z@rel\triangleq}

aliases

540 \let \sdefs \sdef
541 \mathcode`\|=\mid
542 \let \ldata \lang
543 \let \rdata \rang

MISCELLANEOUS

544 \def \lblot {\langle\!|}
545 \def \rblot {|\!\rangle}
546 \def \IMP   {\boldword{Import}}
547 \let \env   \Rrightarrow
548 \def \zlet  {\boldword{let}}
549 \def \zin   {\boldword{in}}
550 \def \zwhere    {\boldword{where}}

QZED SUPPORT

551 \def\HOLE{\z@op{\hbox{$\lll\star\star\star\ggg$}}}
552 \def\landd{} % to support qzed editor
553 \def\semid{} % to support qzed editor
554 \def\qzed{\ifz@inclass\else\zed\fi}
555 \def\endqzed{\ifz@inclass\else\endzed\fi}

CLASSES

556 \def\qua{\mbox{::}}
557 \def\redef{\mbox{\textbf{~redef}}}
558 \def\Init{I\!\mbox{\footnotesize\emph{NIT}}}
559 \def\Exit{E\!\mbox{\footnotesize\emph{XIT}}}
560 \def\Internal{I\!\mbox{\footnotesize\emph{NTERNAL}}}
561 \def\Aux{A\!\mbox{\footnotesize\emph{UX}}}
562 \def\intern{\mbox{\textsf{i}}}

PROOFS

563 \def\thrm{\z@rel\vdash}
564 \def\qed{\zsmall\Box}
565 \let\Qed\Box
566 \let\QED\square
567 \def\BLACKQED{\zsmall\blacksquare}
568 \let\ETH\qed
569 \def\TH{\boldword{Theorem}}
570 \def\LE{\boldword{Lemma}}
571 \def\PR{\boldword{Proof}}
572 \def\refines{\z@rel\sqsupseteq}
573 \def\defines{\z@rel\sqsubseteq}
574 \def\weakrefine{\z@rel{\raise0.2ex\rlap{\hbox{$\sqsupset$}}\lower1ex\hbox{$\sim$}}}
575 \def\weakdefine{\z@rel{\raise0.2ex\rlap{\hbox{$\sqsubset$}}\lower1ex\hbox{$\sim$}}}

aliases

576 \let\shows\thrm

OBJECT THEORY

577 \def\childof{\z@rel\xsucc}
578 \def\parentof{\z@rel\xprec}
579 \let\weaksubclass\succsim
580 \let\weaksupclass\precsim
581 \def\hasa{\z@rel{\mathord\xsucc\!\!\!\mathord\xsucc}}
582 \def\instancein{\z@rel{\mathord\xprec\!\!\!\mathord\xprec}}
583 \def\subtype{\z@rel\sqsubset}
584 \def\subtypeeq{\z@rel\sqsubseteq}
585 \def\suptype{\z@rel\sqsupset}
586 \def\suptypeeq{\z@rel\sqsupseteq}

aliases

587 \let\inherits\childof
588 \let\subclass\childof
589 \let\isa\childof
590 \let\supclass\parentof
591 \let\instantiates\hasa
592 \let\islikea\weaksubclass

TEMPORAL LOGIC

593 \def\atnext{\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\zSmall\bigcirc$}\kern0.01em\zSmall\bigcirc}
594 \def\atlast{\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\kern0.01em\mathord-$}\zSmall\bigcirc}
595 \def\always{\lower0.37ex\hbox{$\zbig\Box$}}
596 \def\uptilnow{\rlap{$\kern0.02em\mathord-$}\lower0.37ex\hbox{$\zbig\Box$}}
597 \def\eventually{\lower0.37ex\hbox{$\zbig\Diamond$}}
598 \def\previously{\rlap{$\kern0.04em\mathord-$}\lower0.37ex\hbox{$\zbig\Diamond$}}

aliases

599 \let\henceforth\always

ORDERS

600 \def \mono  {\keyword{monotonic}}
601 \def \porder    {\keyword{partial\_order}}
602 \def \torder    {\keyword{total\_order}}
603 \newbox\z@combox\newdimen\z@wdcalc
604 \def\comment{\@ifnextchar*{\z@leftcomment}{\z@comment}}

605 \def\z@comment#1{$\z@stopfield\z@addfield\z@startfield$%
606 \global\setbox\z@combox\hbox{\quad[{\sf #1}]}\z@wdcalc=\wd\z@combox%
607 \advance\z@wdcalc by \wd\z@curline\advance\z@wdcalc by \z@curindent%
608 \advance\z@wdcalc by \zedleftsep\advance\z@wdcalc by \zedlinethickness%
609 \advance\z@wdcalc by 2\zedindent\ifdim\z@wdcalc>\displaywidth\\%
610 \fi&\box\z@combox\ignorespaces}
611 \def\z@leftcomment*#1{\hbox{[{\sf #1}]}}

6 Z environments

6.1 Margin stack

Define a stack of dimensions (50 elements) This can probably be made smaller when qzed filters its TEX output better

612 \newcount\z@stackmin
613 \newcount\z@stackmax
614 \newcount\z@stacktop
615 \newdimen\@gtempa \z@stackmin=\allocationnumber
616 \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
617 \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
618 \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
619 \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
620 \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
621 \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
622 \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
623 \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
624 \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
625 \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
626 \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
627 \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
628 \newdimen\@gtempa
629 \z@stackmax=\allocationnumber
630 \dimen\z@stackmin=0pt

Define a box to contain the current line & a variable to contain it’s indentation

631 \newbox\z@curline
632 \newdimen\z@curindent
633 \dimen\z@curindent=0pt

Space between operands of a function application

634 \def\z@space{{}\;{}}

Define a box to contain the current field

635 \newbox\z@curfield

Define a mini-tabbing environment for use inside ‘zed’

636 \def\z@startline{\setbox\z@curline\hbox{}%
637  \global\z@curindent\dimen\z@stacktop
638  \z@startfield\ignorespaces}
639 \def\z@stopline{\z@stopfield
640  \z@addfield
641  \hbox{\hskip\z@curindent \box\z@curline}}

642

643 \def\z@startfield{\global\setbox\z@curfield\hbox\bgroup}

644 \def\z@stopfield{\egroup}
645 \def\z@addfield{\global\setbox\z@curline\hbox{\unhbox
646  \z@curline\unhbox\z@curfield}}

647

648 \def\z@pushmargin{\hbox{\kern0pt}$%
649 \z@stopfield
650 \z@addfield
651 \ifnum \z@stacktop < \z@stackmax
652  \global\advance\z@stacktop \@ne
653 \else
654  \@latexerr{Z margin stack overflow (too many \string\M's)}
655  \@ehd
656 \fi
657 \global\dimen\z@stacktop\z@curindent
658 \global\advance\dimen\z@stacktop \wd\z@curline
659 \z@startfield\ignorespaces
660 $\relax}
661 \def\z@popmargin{\ifnum \z@stacktop > \z@stackmin
662  \global\advance\z@stacktop \m@ne \ignorespaces
663 \else
664  \@latexerr{Z Margin stack underflow (too many \string\O's)}
665  \@ehd
666 \fi}
667 \def\M{\z@pushmargin} \def\O{\z@popmargin} \def\S{\z@space}
668 \z@stacktop\z@stackmin

6.2 Utility macros for Z environments

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 (e.g. argue) may be split arbitrarily. All generate alignment displays, and penalties are used to control page breaks.

6.2.1 Format and control macros

669 \newdimen\zedindent \zedindent=\leftmargini
670 \newdimen\zedleftsep    \zedleftsep=1em
671 \newdimen\zedtab    \zedtab=2em
672 \newdimen\zedbar    \zedbar=8em
673 \newdimen\zedlinethickness  \zedlinethickness=0.4pt
674 \newdimen\zedcornerheight   \zedcornerheight=0pt
675 \newcount\z@cols
676 \newif\ifz@firstline    \z@firstlinefalse
677 \newif\ifz@inclass  \z@inclassfalse
678 \newif\ifz@inenv    \z@inenvfalse
679 \newif\ifz@leftmargin   \z@leftmargintrue
680 \newif\ifz@incols   \z@incolsfalse
681 \newif\ifleftnames  \leftnamesfalse
682 \def\leftschemas{\leftnamestrue}
683 \newif\ifz@inbox    \z@inboxfalse
684 \newskip\zedbaselineskip    \zedbaselineskip\baselineskip

685 \newbox\zstrutbox   \setbox\zstrutbox=\copy\strutbox
686 \def\zstrut{\relax\ifmmode\copy\zstrutbox\else\unhcopy\zstrutbox\fi}
687 \def\zedbaselinestretch{1}

Penalties

688 \newcount\interzedlinepenalty   \interzedlinepenalty=10000  %never break
689 \newcount\preboxpenalty \preboxpenalty=0    %break easily
690 \newcount\forcepagepenalty  \forcepagepenalty=-10000    %always break
691 \interdisplaylinepenalty=100    %break sometimes

Macros for changing the size of schema text

692 \def\zedsize#1{\def\z@size{#1}}
693 \def\z@size{}
694 \newskip\z@adskip\newskip\z@bdskip\newskip\z@adsskip\newskip\z@bdsskip
695 \def\z@changesize{%
696 \z@adskip\abovedisplayskip\z@bdskip\belowdisplayskip% save skips
697 \z@adsskip\abovedisplayshortskip\z@bdsskip\belowdisplayshortskip
698 \z@size % change size
699 \abovedisplayskip\z@adskip\belowdisplayskip\z@bdskip% restore skips
700 \abovedisplayshortskip\z@adsskip\belowdisplayshortskip\z@bdsskip}

701 % 702 %

703 \def\z@zeroskips{\abovedisplayskip\z@\belowdisplayskip\z@
704  \abovedisplayshortskip\z@\belowdisplayshortskip\z@}

6.3 Macros for margins

\z@narrow, \z@wide — make the margins narrower, wider

705 \def\z@narrow{\advance\linewidth by -\zedindent}
706 \def\z@wide{\advance\linewidth by \zedindent}

6.4 Macros for drawing boxes

\z@hrulefill — line with correct thickness

707 \def\z@hrulefill{\leaders\hrule height\zedlinethickness\hfill}

\z@topline draws the top horizontal line of boxed environments \z@dbltopline draws a double ruled top line \z@botline draws the bottom horizontal line of boxed environments \zedline[comment] draws a long horizontal line ending in comment \where draws a short horizontal line

708 \def\z@topline#1{\omit\@ifnextchar[{\z@@topline{#1}}{\z@@topline{#1}[]}}
709 \def\z@@topline#1[#2]{\hbox to\linewidth{\zstrut\ifleftnames\else
710  \vrule height\zedlinethickness width\zedlinethickness
711  \hbox to\zedleftsep{\z@hrulefill}\fi#1\z@hrulefill
712  \smash{\vrule height\zedlinethickness width\zedlinethickness
713  depth\zedcornerheight}\hbox{\sf #2}}\cr}
714 \def\z@dbltopline#1{\omit\@ifnextchar[{\z@@dbltopline{#1}}{\z@@dbltopline{#1}[]}}
715 \def\z@@dbltopline#1[#2]{\z@@topline{#1}[#2]%
716 \noalign{\kern-\baselineskip
717  \kern-\zedlinethickness
718  \kern-\doublerulesep \nobreak}%
719 \omit\z@@topline{\hphantom{#1}}[\hphantom{#2}]%
720 \noalign{\kern\doublerulesep

721  \kern\zedlinethickness \nobreak}}
722 \def\z@botline{\also\omit\hbox to\linewidth{\z@hrulefill
723 \smash{\vrule height\zedcornerheight width\zedlinethickness
724  depth 0pt}}\cr}
725 \def\z@@botline[#1]{\hbox to\linewidth{\vrule\z@hrulefill\hbox{\sf\smash{#1}}}\also}
726 \def\zedline{\also\omit\@ifnextchar[{\z@@botline}{\z@@botline[]}}
727 \def\where{\also \omit \hbox to\zedbar{\z@hrulefill}\cr\also}
728 \let \ST    \where

\z@left is placed at the left of each z line: in non-box environments it will do nothing. in boxed environments it will do a vertical line with the same height as the maximum height of the line.

729 \def\z@left{\ifz@inbox\vrule width\zedlinethickness\hskip\zedleftsep\fi}

6.5 Macros for setting up Z environments

730 \def\z@env{\global\z@firstlinetrue\z@changesize

731 $$

732  \z@inenvtrue
733  \baselineskip\zedbaselineskip
734  \parskip=0pt\lineskip=0pt\z@narrow
735  \advance\displayindent by \zedindent
736  \def\\{\crcr}% Must have \def and not \let for nested alignments.
737  \everycr={\noalign{\ifz@firstline \global\z@firstlinefalse
738  \else \penalty\interzedlinepenalty \fi}}
739  \tabskip=0pt}
740 \def\endz@env{$$
741 \global\@ignoretrue

742 }

Z lines are formated in two (overlapping) columns; the first flush left having the same width as the environment, and, the second flush right ending at the right end of the environment.

743 \def\z@format{\halign to\linewidth\bgroup%
744  \zstrut\z@left\z@startline\ignorespaces$\@lign##$\z@stopline\hfil%
745  \tabskip=0pt plus1fil%
746  &\hbox to 0pt{\hss\@lign##}\tabskip=0pt\cr}
747 \def\z@boxenv{\z@narrow\let\also=\als@ \let\Also=\Als@ \let\ALSO=\ALS@
748  \z@inboxtrue \predisplaypenalty=\preboxpenalty \z@env\z@format}
749 \def\z@outnonbox{\z@outclasscheck\z@leavevmode\z@env}
750 \def\z@inoutbox{\z@leavevmode\z@makeouter\z@inclassfalse\z@boxenv}

6.6 Spacing commands

no vertical glue between abutted lines

751 \def\@but{\noalign{\nointerlineskip}}

no \par extra vertical spacing after Z environments

    \def\z@nopar{\ifz@inclass\else\vskip-\parskip\fi}\def\z@nopar{\global\parskip0pt\global\everypar{\parskip30mm\everypar{}}}
752 \def\z@nopar{\global\@endpetrue}

\z@leavevmode – 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

Use when entering displayed environments to get correct spacing

753 \def\z@leavevmode{\ifvmode\if@inlabel\indent\else\if@noskipsec\indent\else
754  \if@nobreak\global\@nobreakfalse\everypar={}\fi
755  {\parskip=0pt\noindent}\fi\fi\fi}

extra vertical space in non-box environments

756 \def\also{\crcr\noalign{\vskip\jot}}
757 \def\Also{\crcr\noalign{\vskip2\jot}}
758 \def\ALSO{\Also\Also}

extra vertical space in boxed environments

759 \def\als@{\crcr\@but\omit\vrule height\jot width\zedlinethickness \cr \@but}
760 \def\Als@{\crcr\@but\omit\vrule height2\jot width\zedlinethickness \cr \@but}
761 \def\ALS@{\crcr\@but\omit\vrule height4\jot width\zedlinethickness \cr \@but}

6.7 Environment-breaking commands

762 \def\znewpage{\also\noalign{\penalty\forcepagepenalty}\also}
763 \def\zbreak{\also\noalign{\penalty\interdisplaylinepenalty\vskip-\jot}\also}
764 \def\Zbreak{\also\noalign{\penalty\interdisplaylinepenalty}\also}
765 \def\ZBREAK{\Also\noalign{\penalty\interdisplaylinepenalty}\Also}
766 \def\t#1{\hskip #1\zedtab}
767 %\def\c#1#2{\hbox to #1\zedtab{$#2$\hfil}}
768 \def\flushr#1{\crcr&#1\quad\cr}

7 Utility macros for Object-Z

769 \def\z@inclasscheck{\ifz@inclass\else
770  \@latexerr{This Z environment is only allowed within a class}
771 {Perhaps you forgot to include a \string\begin\string{class\string}
772 somewhere^^Jor you are trying to print a file that needs updating.^^J\@ehc} \fi}
773 \def\z@outclasscheck{\ifz@inclass
774  \@latexerr{This Z environment is not allowed inside a class}
775 {This environment doesn't really make sense within a class.^^J%
776 If you really want it then I'll try my best to fit in in.^^J\@ehc}\else
777 \ifz@inenv \@latexerr{New Z environment declared before previous
778 one is completed}
779 {I suspect that you've forgotten to finish the last environment.^^J%
780 You are trying to nest environments and this can only be done inside classes^^J%
781 besides, the environment you have started isn't valid within classes any way.^^JI suggest that you type \space X <return> \space to quit and then correct your document.}
782 \fi\fi}

783 %

784 \def\z@makeouter{%

785 \ifz@inenv
786 \ifz@inclass\z@inenvfalse
787  \hskip-\zedleftsep \advance\linewidth by -\zedlinethickness
788  \zedindent=\zedleftsep \zedleftsep=0.8\zedleftsep
789  \zedbar=0.8\zedbar \zedtab=0.8\zedtab
790  \oz@parbox{\linewidth}\bgroup
791  \z@zeroskips
792 \else
793 \@latexerr{Incorrect place for Z environment; nesting is
794 allowed only inside classes}
795 {You've either forgotten to finish the last environment,^^J%
796 you've forgotten to include a
797 \string\begin\string{class\string} somewhere^^J%
798 or you are trying to print a file that needs updating.^^J%
799 (Then again, you might just be trying to do something^^J%
800  that the author of these macros didn't intend you to do)^^J\@ehc}
801 \fi
802 \else
803 \bgroup
804 \fi

805 } 806 %

807 \def \z@makeinner{\egroup
808 \global\z@curindent\z@

809 } 810 %

811 \def \classbreak{\also\egroup$$\vskip -\ht\zstrutbox
812  \vskip -\abovedisplayskip\vskip -\belowdisplayskip\z@wide\z@boxenv\also}

8 Non-box environments

ZED for non-box multiline formulas

813 \def\zed{\z@outnonbox\z@inboxfalse\z@format}
814 \def\endzed{\crcr\egroup\endz@env}
815 \let\[=\zed
816 \def\]{\crcr\egroup$$\ignorespaces}

ARGUE for algebraic arguments

used for algebraic proofs expressed as extended equations. like zed but with extra spacing between lines Generates an alignment display, which may be split across pages.

817 \def\argue{\z@outnonbox\interzedlinepenalty=\interdisplaylinepenalty
818  \openup 1\jot \z@format
819  \noalign{\vskip-\jot}}% equal vspace above and below argue display
820 \let\endargue=\endzed

INFRULE for inference rules

used for inference rules. The horizontal line is generated by \derive: an optional argument contains the side-conditions of the rule.

821 \def\infrule{\z@outnonbox\halign\bgroup
822  \zstrut\quad$\@lign##$\quad\hfil&\quad\@lign##\hfil\cr}
823 \let\endinfrule=\endzed

824 \def\derive{\crcr\also\@but\omit\z@hrulefill%
825  \@ifnextchar[{\z@sidecondition}{\cr\also\@but}}
826 \def\Derive{\crcr\also\@but\omit\z@hrulefill\cr\@but
827  \noalign{\kern-\dp\zstrutbox
828  \kern\doublerulesep \nobreak}%
829 \omit\derive}
830 \def\z@sidecondition[#1]{&$\smash{\lower 0.2ex\hbox{$[\;#1\;]$}}$\cr\also\@but}

SYNTAX for syntax rules

‘syntax’ environment: used for syntax rules — even (once!) for VDM.

831 \def\syntax{\z@outnonbox\halign\bgroup
832  \zstrut$\@lign##$\hfil &\hfil$\@lign{}##{}$\hfil
833  &$\@lign##$\hfil &\qquad\@lign-- ##\hfil\cr}
834 \let\endsyntax=\endzed

8.1 Boxed environments

SCHEMA schema definitions

835 \def\schema#1{\z@inoutbox\z@topline{$\,#1\,$}}
836 \def\endschema{\z@botline \endzed \z@makeinner \z@nopar}

SCHEMA* schema with no name

837 \@namedef{schema*}{\leftnamesfalse\z@inoutbox\z@topline{}}
838 \expandafter\let\csname endschema*\endcsname=\endschema

GENSCHEMA generic schema definitions

839 \def\genschema#1#2{\z@inoutbox\z@topline{$\,#1\:[#2]\,$}}
840 \let\endgenschema=\endschema

AXDEF ‘liberal’ axiomatic definitions

841 \def\axdef{\z@inoutbox}
842 \def\endaxdef{\endzed\z@makeinner}

UNIQDEF ‘unique’ axiomatic definitions

843 \def\uniqdef{\leftnamesfalse\z@inoutbox\z@dbltopline{}}
844 \let\enduniqdef=\endschema

GENDEF ’generic’ axiomatic definitions

845 \def\gendef#1{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,[#1]\,$}}
846 \let\endgendef=\endschema

CLASS

847 \def\class#1{\z@leavevmode\z@makeouter\z@inclasstrue
848  \z@boxenv\z@topline{$\,#1\,$}}
849 \let\endclass\endschema

OP

850 \def\op{\z@inclasscheck\schema}
851 \let\endop\endschema

STATE

852 \def\state{\z@inclasscheck\vbox\bgroup\vskip-\ht\zstrutbox\vbox\bgroup\hbox\bgroup\@nameuse{schema*}}
853 \def\endstate{\endschema\egroup\egroup\egroup}

INIT

854 \def\init{\z@inclasscheck\schema{\Init}}
855 \let\endinit\endschema

8.2 Other environments

SIDEBYSIDE

This should support an arbitary number of columns \zedindent’s proportion of \linewidth gives a practical limit

856 \def\sidebyside{\@ifnextchar[{\z@columns}{\z@columns[2]}}
857 \def\z@columns[#1]{\z@leavevmode\z@cols#1 \z@makeouter\z@narrow%
858  $$\lineskip=0pt\z@incolstrue
859  \predisplaysize\maxdimen
860  \ifz@leftmargin\hskip-\zedindent\z@leftmarginfalse\fi
861  \setbox0=\hbox to \linewidth\bgroup\z@zeroskips%
862  \divide\zedbar by \z@cols \divide\zedleftsep by \z@cols
863  \divide\zedtab by \z@cols \divide\linewidth by \z@cols
864 \oz@parbox[t]{\linewidth}\bgroup\z@wide}

865 %

866 \def\nextside{\egroup\hss\oz@parbox[t]{\linewidth}\bgroup\z@wide}

867 %

868 \newdimen\z@temp
869 \def\endsidebyside{\egroup\egroup
870  \z@temp\ht0 \advance\z@temp by \dp0\advance\z@temp by-\dp\zstrutbox
871  \hbox{\raise\z@temp\box0}\endz@env\z@makeinner\z@nopar}

ZPAR

872 \def\zpar{\z@leavevmode
873  \ifz@inenv\z@inclasstrue\fi% fudge to let zpar in all boxes
874  \z@makeouter\z@changesize
875  \advance\linewidth by -\z@curindent
876  \advance\linewidth by -\wd\z@curline
877  \hskip-\wd\z@curline\advance\linewidth by -\zedindent$$
878  \ifz@leftmargin\hskip-\zedindent\fi% adjustment for first column
879  \advance\displayindent by \zedindent
880  \advance\displaywidth by -\zedindent
881  \advance\displayindent by \z@curindent
882  \advance\displayindent by \wd\z@curline
883  \advance\displaywidth by -\z@curindent
884  \advance\displaywidth by -\wd\z@curline
885  \global\setbox\z@curline\hbox{}
886  \z@narrow\oz@parbox[b]{\linewidth}\bgroup\hfil\break}
887 \def\endzpar{\egroup$$\z@makeinner\z@nopar}

CLASSCOM

888 \def \classcom{\zpar\sf}
889 \let \endclasscom=\endzpar

PROOF

890 \def\proof{\zpar$\PR$\zpar}
891 \def\endproof{\endzpar\endzpar}

Additional auxiliary macros

892 \def\zseq#1{\lseq #1 \rseq}
893 \def\zset#1{\{ #1 \}}
894 \def\zimg#1{\limg #1 \rimg}
895 \def\zsch#1{\lsch #1 \rsch}
896 \def\zimgset#1{\zimg\zset{#1}}

897 % 898 ⟨/package⟩

25