%%
%% This is file `czt.sty',
%% generated with the docstrip utility.
%%
%% The original source files were:
%%
%% czt.dtx (with options: `package')
%%
%% This is a generated file
%%
%% Copyright (C) 2008 Leo Freitas.
%% University of York All rights reserved.
%%
%% This is a generated file for Standard Z within the
%% Community Z Tools (CZT). It is based on the Object Z
%% package distribution. Permission is granted to to
%% customize the declarations in this file to serve the
%% needs of your installation. However, no permission
%% is granted to distribute a modified version of this
%% file under its original name.
%%
\def\fileversion{v.1.0}
\def\filedate{2008/10/01}
\def\filedesc{Standard Z style file by the Community Z Tools}
\NeedsTeXFormat{LaTeX2e}[1999/12/01]
\ProvidesPackage{czt}
[\filedate\space\fileversion\space \filedesc]
\message{`\filedesc'\space \fileversion\space <\filedate>}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Design guidelines:
% 1) keep it minimal + simple + consistent
% 2) for machine readable Standard Z only
% 3) identify code sources (when different)
% 4) normalise definitions for consistency
% 5) complete missing cases (use common sense)
% 6) keep it well documented, but not verbose
% 7) follow order of definitions from Z Standard document
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Package options - zed.sty (old version of zed-csp.sty) %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% create conditionals for each option available, init=false
\newif\if@lucida@ \@lucida@false
\newif\if@color@ \@color@false
\newif\if@mathit@ \@mathit@false
\newif\if@mathrm@ \@mathrm@false
\newif\if@tkkeyword@ \@tkkeyword@false
\newif\if@cntglobally@ \@cntglobally@false
\newif\if@cntbychapter@ \@cntbychapter@false
\newif\if@cntbysection@ \@cntbysection@false
% declare what each option actually do - colour=synonym(color)
\DeclareOption{lucida}{\PackageInfo{czt}{'lucidda' option chosen} \@lucida@true}
\DeclareOption{color}{\PackageInfo{czt}{'color' option chosen} \@color@true}
\DeclareOption{colour}{\PackageInfo{czt}{'color' option chosen} \@color@true}
\DeclareOption{mathit}{\PackageInfo{czt}{'mathit' option chosen} \@mathit@true \@mathrm@false}
\DeclareOption{mathrm}{\PackageInfo{czt}{'mathrm' option chosen} \@mathit@false \@mathrm@true}
\DeclareOption{tkkeyword}{\PackageInfo{czt}{'tkkeyword' option chosen} \@tkkeyword@true}
% way to handle paragraph counting
\DeclareOption{cntglobally}{\PackageInfo{czt}{'cntglobally' option chosen} \@cntglobally@true \@cntbychapter@false \@cntbysection@false}
\DeclareOption{cntbychapter}{\PackageInfo{czt}{'cntbychapter' option chosen} \@cntglobally@false \@cntbychapter@true \@cntbysection@false}
\DeclareOption{cntbysection}{\PackageInfo{czt}{'cntbysection' option chosen} \@cntglobally@false \@cntbychapter@false \@cntbysection@true}
% default option as using math italics for mathcode names.
\ExecuteOptions{mathit,cntglobally}
\ProcessOptions\relax
% if Lucida Bright is chosen, then load the package with necessary dependencies
\if@lucida@
\@ifpackageloaded{lucidabr}{%
\PackageInfo{czt}{Lucida Bright already loaded}
}{%
\PackageInfo{czt}{Loading Lucida Bright with `expert' and `altbullet' options.\MessageBreak %
We also require the `texnansi' package}
\RequirePackage{texnansi}
\RequirePackage[expert,altbullet]{lucidabr}
}
\else
\PackageInfo{czt}{AMS fonts selected with default options}
\fi
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Treating colours %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% If colouring is available
\if@color@
\PackageInfo{czt}{Rendering Z math mode with colours}
% check whether to load color package or not
\@ifpackageloaded{color}{%
\relax
}{%
\PackageInfo{czt}{Package `color' loaded with `dvipsnames' \MessageBreak and `usenames' options}
\RequirePackage[dvipsnames,usenames]{color}
}
% define some nice colours to use within Z declarations
%
%\definecolor{ZedBoxColor}{cmyk}{0.99,0,0.52,0}
\definecolor{ZedBoxColor}{cmyk}{1,1,0,0}
\definecolor{AnnotationColor}{cmyk}{0.98,0.13,0,0.43}
\definecolor{ZedColor}{cmyk}{0.50,1,0,0}
% add more color here if needed
\PackageInfo{czt}{Z colours defined as:\MessageBreak%
\space\space ZedBoxColor\space\space\space\space\space = cmyk( 1, 1,0, 0) \MessageBreak%
\space\space AnnotationColor = cmyk(0.98,0.13,0,0.43) \MessageBreak%
\space\space ZedColor\space\space\space\space\space\space\space\space = cmyk(0.50, 1,0, 0) \MessageBreak%
}
\else
\PackageInfo{czt}{Rendering Z math mode in monochrome.}
% if color is loaded do nothing, otherwise redefine \color as empty
\@ifpackageloaded{color}{\relax}{\def\color#1{\relax}}%
\fi
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Some needed markers used in some symbols - font independant %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% horizontal raised bar: used for negated \dres\rres
\def\zmark@hbar#1{\rlap{\raise.0001ex\hbox{$-$}}{#1}}
% vertical raised bar: used for partial and finite markings. #1=symbol
\def\zmark@pvbar#1{\ooalign{\hfil$\mapstochar\mkern 5mu$\hfil\cr$#1$}}
\def\zmark@fvbar#1{\ooalign{\hfil$\mapstochar\mkern 3mu\mapstochar\mkern 5mu$\hfil\cr$#1$}}
% doubled arrow function symbols. symbol = #1/#3; space delta = #2
% surjection (#1=\fun, #2=4mu, #3=\fun); bijection (#1=\inj, #2=5mu, #3=\fun)
\def\zmark@darrow#1#2#3{\ooalign{$#1$\hfil\cr$\mkern#3mu#2$}}
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Loading mathematical symbols from AMS/Lucuida fonts %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% declares the math version for fonts as czt
\DeclareMathVersion{czt}
\PackageInfo{czt}{Creating `czt' math version}
% Selects St. Mary's Road symbol package font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
% Specify aliases for mathematical operator categories
\DeclareSymbolFontAlphabet{\mathrm}{operators}
\DeclareSymbolFontAlphabet{\mathit}{letters}
\DeclareSymbolFontAlphabet{\mathcal}{symbols}
% Some math alphabet defaults regardless of the chosen font
\SetMathAlphabet{\mathrm}{czt}{\encodingdefault}{\rmdefault}{m}{n}%
\SetMathAlphabet{\mathbf}{czt}{\encodingdefault}{\rmdefault}{bx}{n}%
\SetMathAlphabet{\mathsf}{czt}{\encodingdefault}{\sfdefault}{m}{n}%
% set symbol font italics for both Lucida and AMS fonts
% this changes the behaviour of \symitalics
\DeclareSymbolFont{italics}{\encodingdefault}{\rmdefault}{m}{it}%
\DeclareSymbolFontAlphabet{\zit}{italics}
% Saved symbols with other names
\let\mathemptyset=\emptyset % save old \emptyset set version
\let\mathdiv=\div % save the math division symbol
\let\mathstar=\star % save old \star version
% Loading symbols conditionally to Lucida Bright / AMS .
%
% To allow independent conditional loading of fonts, we
% follow the name convention: \zsym@XXX for all needed
% symbols. Equal symbols in both fonts appear at the end.
%
\@ifpackageloaded{lucidabr}{%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Lucida Bright font setup %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
\PackageInfo{czt}{Loading Lucida Bright font symbols for Z}
% Encodings from lucidabr.sty
%
\DeclareSymbolFont{arrows}{LMR}{hlcm}{m}{n} %arrows =LMR/hlcm/m/n
\DeclareSymbolFont{letters}{OML}{hlcm}{m}{n} %letters =OML/hlcm/m/n ; % mathupright= in lucida@expert mode
\DeclareSymbolFont{symbols}{OMS}{hlcy}{m}{n} %symbols =OMS/hlcy/m/n
%operators=\operator@encoding/\rmdefault/m/n
% =OT1-T1-LY1 / ?? / m /n
%largesymbols=OMX/hlcv/m/n
% Mathematical alphabet in lucidabr - \mathbb = math. blackboard bold
\DeclareSymbolFontAlphabet{\mathbb}{arrows}
% Math symbols declaration within Lucida Bright
%%%%%%%%%%%%%%%%% A.2.4.1 - Greek alphabet treated as operators %
% Or should this be largesymbols / mathupright (see lucidabr.sty)?
\DeclareMathSymbol{\zsym@Delta}{\mathord}{letters}{"01}%
\DeclareMathSymbol{\zsym@Xi}{\mathord}{letters}{"04}%
\DeclareMathSymbol{\zsym@theta}{\mathord}{letters}{"12}%
\DeclareMathSymbol{\zsym@lambda}{\mathord}{letters}{"15}%
\DeclareMathSymbol{\zsym@mu}{\mathord}{letters}{"16}%
%%%%%%%%%%%%%%%%% A.2.4.2 - Other letter characters %
% Other special letters
\DeclareMathSymbol{\zsym@arithmos}{\mathord}{arrows}{"41}%
\DeclareMathSymbol{\zsym@nat}{\mathord}{arrows}{"4E}%
\DeclareMathSymbol{\zsym@power}{\mathord}{arrows}{"50}%
\def \zsym@arithmos {\mathbb A}
\def \zsym@nat {\mathbb N}
\def \zsym@power {\mathbb P}
% Other Greek letters
% Or should this be largesymbols / mathupright (see lucidabr.sty)?
\DeclareMathSymbol{\zsym@alpha}{\mathord}{letters}{"0B}%
\DeclareMathSymbol{\zsym@beta}{\mathord}{letters}{"0C}%
\DeclareMathSymbol{\zsym@gamma}{\mathord}{letters}{"0D}%
\DeclareMathSymbol{\zsym@delta}{\mathord}{letters}{"0E}%
\DeclareMathSymbol{\zsym@epsilon}{\mathord}{letters}{"0F}%
\DeclareMathSymbol{\zsym@zeta}{\mathord}{letters}{"10}%
\DeclareMathSymbol{\zsym@eta}{\mathord}{letters}{"11}%
\DeclareMathSymbol{\zsym@iota}{\mathord}{letters}{"13}%
\DeclareMathSymbol{\zsym@kappa}{\mathord}{letters}{"14}%
\DeclareMathSymbol{\zsym@nu}{\mathord}{letters}{"17}%
\DeclareMathSymbol{\zsym@xi}{\mathord}{letters}{"18}%
\DeclareMathSymbol{\zsym@pi}{\mathord}{letters}{"19}%
\DeclareMathSymbol{\zsym@rho}{\mathord}{letters}{"1A}%
\DeclareMathSymbol{\zsym@sigma}{\mathord}{letters}{"1B}%
\DeclareMathSymbol{\zsym@tau}{\mathord}{letters}{"1C}%
\DeclareMathSymbol{\zsym@upsilon}{\mathord}{letters}{"1D}%
\DeclareMathSymbol{\zsym@phi}{\mathord}{letters}{"1E}%
\DeclareMathSymbol{\zsym@chi}{\mathord}{letters}{"1F}%
\DeclareMathSymbol{\zsym@psi}{\mathord}{letters}{"20}%
\DeclareMathSymbol{\zsym@omega}{\mathord}{letters}{"21}%
\DeclareMathSymbol{\zsym@Gamma}{\mathord}{letters}{"00}%
\DeclareMathSymbol{\zsym@Theta}{\mathord}{letters}{"02}%
\DeclareMathSymbol{\zsym@Lambda}{\mathord}{letters}{"03}%
\DeclareMathSymbol{\zsym@Pi}{\mathord}{letters}{"05}%
\DeclareMathSymbol{\zsym@Sigma}{\mathord}{letters}{"06}%
\DeclareMathSymbol{\zsym@Upsilon}{\mathord}{letters}{"07}%
\DeclareMathSymbol{\zsym@Phi}{\mathord}{letters}{"08}%
\DeclareMathSymbol{\zsym@Psi}{\mathord}{letters}{"09}%
\DeclareMathSymbol{\zsym@Omega}{\mathord}{letters}{"0A}%
%%%%%%%%%%%%%%%%% A.2.4.3 - Special characters %
%\def \zsym@langle no need to redefine?
%\def \zsym@rangle no need to redefine?
\def \zsym@lblot {{\langle}\mkern -5mu{|}}
\def \zsym@rblot {{|}\mkern -5mu{\rangle}}
\def \zsym@ldata {\langle\!\langle}
\def \zsym@rdata {\rangle\!\rangle}
\DeclareMathSymbol{\zsym@spot}{\mathrel}{symbols}{"0F}%
\DeclareMathSymbol{\zsym@in}{\mathrel}{symbols}{"32}%
%%%%%%%%%%%%%%%%% A.2.4.4 - symbol characters predicate logic %
% Generic Z operators
\DeclareMathSymbol{\zsym@vdash}{\mathord}{symbols}{"60}%
\DeclareMathSymbol{\zsym@cross}{\mathbin}{symbols}{"02}%
% Schema operators defined as slightly bigger with \z@Bigbinop
\DeclareMathSymbol{\zsym@solidus}{\mathbin}{symbols}{"6E}% %{letters}{"D8}%
\DeclareMathSymbol{\zsym@pipe}{\mathrel}{symbols}{"1D}%
%\def \zsym@comp {\raise 0.66ex\hbox{\oalign{\hfil$\scriptscriptstyle%
% \mathrm{o}$\hfil\cr\hfil$\scriptscriptstyle\mathrm{9}$\hfil}}}
\def \zsym@typecolon {\raise 0.66ex\hbox{\oalign{\hfil$\scriptscriptstyle%
\mathrm{o}$\hfil\cr\hfil$\scriptscriptstyle\mathrm{o}$\hfil}}}%
\DeclareMathSymbol{\zsym@comp}{\mathbin}{stmry}{"23}%
% Predicate and propositional Logic operators - \mathrel please.
% Both oz.sty and zed.sty \implies and \iff were not \mathstrut.
% Adjust the original quantifiers as prefix ops with \mathstrut.
%
%\def \zsym@not {\neg\;}
\DeclareMathSymbol{\zsym@not}{\mathop}{symbols}{"3A}%
\DeclareMathSymbol{\zsym@and}{\mathrel}{symbols}{"5E}%
\DeclareMathSymbol{\zsym@or}{\mathrel}{symbols}{"5F}%
\DeclareMathSymbol{\zsym@implies}{\mathrel}{symbols}{"29}%
\DeclareMathSymbol{\zsym@iff}{\mathrel}{symbols}{"2C}%
\DeclareMathSymbol{\zsym@forall}{\mathrel}{symbols}{"38}%
\DeclareMathSymbol{\zsym@exists}{\mathrel}{symbols}{"39}%
%%%%%%%%%%%%%%%%% A.2.4.5 - core words (keywords) %
%
% no need to change
\DeclareMathSymbol{\zseqcat}{\mathbin}{letters}{"5F}% why "operators"?
\DeclareMathSymbol{\zupharpoonright}{\mathbin}{arrows}{"75}%
\DeclareMathSymbol{\zupharpoonleft}{\mathbin}{arrows}{"76}%
\DeclareMathSymbol{\zdres}{\mathbin}{letters}{"2F}%
\DeclareMathSymbol{\zrres}{\mathbin}{letters}{"2E}%
\DeclareMathSymbol{\zemptyset}{\mathord}{symbols}{"3B}%
\DeclareMathSymbol{\zinj}{\mathbin}{arrows}{"29}%
\let \zsym@upharpoonright \zupharpoonright
% slightly raised concatenation operator given as a \mathcar
\def \zmark@cat {\raise 0.8ex\hbox{$\mathchar\zseqcat$}}
%%%%%%%%%%%%%%%%% A.2.5.1 - set toolkit symbols %
\DeclareMathSymbol{\zsym@rel}{\mathbin}{arrows}{"21}% or {symbols}{"24}
\DeclareMathSymbol{\zsym@fun}{\mathbin}{symbols}{"21}%
\def \zsym@notin {\not\in}
%\DeclareMathSymbol{\zsym@notin}{\mathbin}{arrows}{"1D}%
\DeclareMathSymbol{\zsym@neq}{\mathrel}{arrows}{"94}%
\def \zsym@emptyset {\zemptyset}
\DeclareMathSymbol{\zsym@subseteq}{\mathrel}{symbols}{"12}%
\DeclareMathSymbol{\zsym@subset}{\mathrel}{symbols}{"13}%
\DeclareMathSymbol{\zsym@cup}{\mathbin}{symbols}{"5B}%
\DeclareMathSymbol{\zsym@cap}{\mathbin}{symbols}{"5C}%
\DeclareMathSymbol{\zsym@setminus}{\mathbin}{symbols}{"6E}%
\DeclareMathSymbol{\zsym@symdiff}{\mathbin}{symbols}{"0E}%
\DeclareMathSymbol{\zsym@bigcup}{\mathop}{symbols}{"5B}%
\DeclareMathSymbol{\zsym@bigcap}{\mathop}{symbols}{"5C}%
\def \zsym@finset {\mathbb F}
%%%%%%%%%%%%%%%%% A.2.5.2 - relation toolkit symbols %
\DeclareMathSymbol{\zsym@mapsto}{\mathbin}{arrows}{"2C}%
\def \zsym@dom {dom}
\def \zsym@ran {ran}
\def \zsym@id {id}
\DeclareMathSymbol{\zsym@circ}{\mathbin}{arrows}{"0E}%
\let \zsym@dres \zdres
\let \zsym@rres \zrres
\def \zsym@ndres {\zmark@hbar{\zsym@dres}}
\def \zsym@nrres {\zmark@hbar{\zsym@rres}}
\DeclareMathSymbol{\zsym@inv}{\mathord}{symbols}{"18}%
%\def \zsym@limg {(\mskip-3.5mu|}
%\def \zsym@rimg {|\mskip-5mu)}
\DeclareMathSymbol{\zsym@limg}{\mathopen}{stmry}{"4C}% \llparenthesis in stmaryrd.sty
\DeclareMathSymbol{\zsym@rimg}{\mathopen}{stmry}{"4D}% \rrparenthesis
\DeclareMathSymbol{\zsym@oplus}{\mathbin}{arrows}{"2C}%
\DeclareMathSymbol{\zsym@plus}{\mathbin}{arrows}{"2C}%
\DeclareMathSymbol{\zsym@star}{\mathbin}{arrows}{"2C}%
%%%%%%%%%%%%%%%%% A.2.5.3 - function toolkit symbols %
% The same as in for AMS
\def \zsym@pfun {\zmark@pvbar{\zsym@fun}}
\def \zsym@inj {\zinj}
\def \zsym@pinj {\zmark@pvbar{\zsym@inj}}
\def \zsym@surj {\zmark@darrow{\zsym@fun}{\zsym@fun}{4}}
\def \zsym@bij {\zmark@darrow{\zsym@inj}{\zsym@fun}{5}}
\def \zsym@psurj {\zmark@pvbar{\zsym@surj}}
\def \zsym@ffun {\zmark@fvbar{\zsym@fun}}
\def \zsym@finj {\zmark@fvbar{\zsym@inj}}
\def \zsym@disjoint {disjoint}
\def \zsym@partition {partition}
%%%%%%%%%%%%%%%%% A.2.5.4 - number toolkit symbols %
\def \zsym@num {\mathbb Z}
\DeclareMathSymbol{\zsym@negate}{\mathop}{arrows}{"2D}%
\DeclareMathSymbol{\zsym@leq}{\mathrel}{symbols}{"14}%
\DeclareMathSymbol{\zsym@geq}{\mathrel}{symbols}{"15}%
\def \zsym@div {div}
\def \zsym@mod {mod}
\DeclareMathSymbol{\zsym@miuns}{\mathbin}{symbols}{"00}%
\DeclareMathSymbol{\zsym@sum}{\mathbin}{symbols}{"82}%
\DeclareMathSymbol{\zsym@mult}{\mathbin}{symbols}{"03}%
\DeclareMathSymbol{\zsym@lessthan}{\mathrel}{letters}{"3C}%
\DeclareMathSymbol{\zsym@greaterthan}{\mathrel}{letters}{"3E}%
%%%%%%%%%%%%%%%%% A.2.5.5 - sequence toolkit symbols %
\def \zsym@upto {\ldotp\ldotp}
\DeclareMathSymbol{\zsym@hash}{\mathop}{arrows}{"17}%
\def \zsym@seq {seq}
\def \zsym@iseq {iseq}
%\langle
%\rangle
\def \zsym@cat {\zmark@cat}
\def \zsym@extract {\zupharpoonleft}
\def \zsym@filter {\zupharpoonright}
\def \zsym@prefix {prefix}
\def \zsym@suffix {suffix}
\def \zsym@infix {infix}
\def \zsym@dcat {{\zsym@cat}/}
% mathematical delimiters that can be used for box drawings
% (see LaTeX2e Font Selection guide @ fntguide.pdf).
\DeclareMathDelimiter{\zboxulcorner}{\mathopen}{arrows}{"5B}{arrows}{"5B}
\DeclareMathDelimiter{\zboxurcorner}{\mathclose}{arrows}{"71}{arrows}{"5C}
\DeclareMathDelimiter{\zboxllcorner}{\mathopen}{arrows}{"5D}{arrows}{"5D}
\DeclareMathDelimiter{\zboxlrcorner}{\mathclose}{arrows}{"5E}{arrows}{"5E}
}{%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% AMS font setup %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
\PackageInfo{czt}{Loading AMS font symbols for Z}
% Load msama10 msamb10 font (AMS font dependencies): AMSa, AMSb
\DeclareSymbolFont{AMSa}{U}{msa}{m}{n}
\DeclareSymbolFont{AMSb}{U}{msb}{m}{n}
% Mathematical alphabet in AMSb - \mathbb = math. blackboard bold
\DeclareSymbolFontAlphabet{\mathbb}{AMSb}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Symbols selected from the AMS font %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\DeclareMathSymbol{\zseqcat}{\mathbin}{AMSa}{"61} % \frown
\DeclareMathSymbol{\zupharpoonright}{\mathbin}{AMSa}{"16} % \upharpoonright
\DeclareMathSymbol{\zupharpoonleft}{\mathbin}{AMSa}{"18} % \upharpoonleft
\DeclareMathSymbol{\zdres}{\mathbin}{AMSa}{"43} % \lhd
\DeclareMathSymbol{\zrres}{\mathbin}{AMSa}{"42} % \rhd
\DeclareMathSymbol{\zemptyset}{\mathord}{AMSb}{"3F} % \varnothing; similar to original \emptyset
\DeclareMathSymbol{\zinj}{\mathrel}{AMSa}{"1A} % \rightarrowtail
% Font dependant marker: slightly raised concatenation operator given as a \mathcar
\def \zmark@cat {\raise 0.8ex\hbox{$\mathchar\zseqcat$}}
% oz.sty option seems to use \mathchar, which nicely selects
% and AMS font Unicode character (see LaTeX for \mathcar)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Standard Z symbols and mathematical toolkit %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% NOTE: Some of these symbols resemble those coming
% from the fonts OML/cmm/n/it or OMS/cmsy/m/n
% (similar rendering names aside each symbol)
% - see tex/latex/base/fontmath.ltx
% The synonyms may be useful if AMS is not present?
%
%%%%%%%%%%%%%%%%% A.2.4.1 - Greek alphabet treated as operators %
\let \zsym@Delta \Delta
\let \zsym@Xi \Xi
\let \zsym@theta \theta
\let \zsym@lambda \lambda
\let \zsym@mu \mu
%%%%%%%%%%%%%%%%% A.2.4.2 - Other letter characters %
% Other special letters
\def \zsym@arithmos {\mathbb A}
\def \zsym@nat {\mathbb N}
\def \zsym@power {\mathbb P}
% Other Greek letters
\let \zsym@alpha \alpha
\let \zsym@beta \beta
\let \zsym@gamma \gamma
\let \zsym@delta \delta
\let \zsym@epsilon \epsilon
\let \zsym@zeta \zeta
\let \zsym@eta \eta
\let \zsym@iota \iota
\let \zsym@kappa \kappa
\let \zsym@nu \nu
\let \zsym@xi \xi
\let \zsym@pi \pi
\let \zsym@rho \rho
\let \zsym@sigma \sigma
\let \zsym@tau \tau
\let \zsym@upsilon \upsilon
\let \zsym@phi \phi
\let \zsym@chi \chi
\let \zsym@psi \psi
\let \zsym@omega \omega
\let \zsym@Gamma \Gamma
\let \zsym@Theta \Theta
\let \zsym@Lambda \Lambda
\let \zsym@Pi \Pi
\let \zsym@Sigma \Sigma
\let \zsym@Upsilon \Upsilon
\let \zsym@Phi \Phi
\let \zsym@Psi \Psi
\let \zsym@Omega \Omega
%%%%%%%%%%%%%%%%% A.2.4.3 - Special characters %
%\def \zsym@langle no need to redefine?
%\def \zsym@rangle no need to redefine?
\def \zsym@lblot {{\langle}\mkern -3.5mu{|}}
\def \zsym@rblot {{|}\mkern -3.5mu{\rangle}}
\def \zsym@ldata {\langle\!\langle}
\def \zsym@rdata {\rangle\!\rangle}
\let \zsym@spot \bullet
\let \zsym@in \in
%%%%%%%%%%%%%%%%% A.2.4.4 - symbol characters predicate logic %
% Generic Z operators
\let \zsym@vdash \vdash
\let \zsym@cross \times
% Schema operators defined as slightly bigger with \z@Bigbinop
\let \zsym@solidus \backslash
\let \zsym@upharpoonright \zupharpoonright
\def \zsym@pipe {\mathord>\!\!\mathord>}
% oz.sty has a nicer (without \small) fcn composition symbol.
% It is defined as an `o' sitting on the top of a `9'.
% zed-csp.sty differentiate the heights whenever in Lucida Bright.
% To allow room for greater flexibility, do not surround it with any \zXXXop.
%\def \zsym@comp {\raise 0.6ex\hbox{\oalign{\hfil$\scriptscriptstyle%
% \mathrm{o}$\hfil\cr\hfil$\scriptscriptstyle\mathrm{9}$\hfil}}}
\def \zsym@typecolon {\raise 0.6ex\hbox{\oalign{\hfil$\scriptscriptstyle%
\mathrm{o}$\hfil\cr\hfil$\scriptscriptstyle\mathrm{o}$\hfil}}}%
\DeclareMathSymbol{\zsym@comp}{\mathbin}{stmry}{"23}%
% Predicate logic
\def \zsym@not {\neg\;}
\let \zsym@and \wedge
\let \zsym@or \vee
\let \zsym@implies \Rightarrow
\let \zsym@iff \Leftrightarrow
\let \zsym@forall \forall
\let \zsym@exists \exists
%%%%%%%%%%%%%%%%% A.2.5.1 - set toolkit symbols %
\let \zsym@rel \leftrightarrow
\let \zsym@fun \rightarrow
\def \zsym@notin {\not\in}
\let \zsym@neq \neq
\def \zsym@emptyset {\zemptyset}
\let \zsym@subseteq \subseteq
\let \zsym@subset \subset
\let \zsym@cup \cup
\let \zsym@cap \cap
\let \zsym@setminus \setminus
\let \zsym@symdiff \ominus
\let \zsym@bigcup \bigcup
\let \zsym@bigcap \bigcap
\def \zsym@finset {\mathbb F}
%%%%%%%%%%%%%%%%% A.2.5.2 - relation toolkit symbols %
\let \zsym@mapsto \mapsto
\def \zsym@dom {dom}
\def \zsym@ran {ran}
\def \zsym@id {id}
\let \zsym@circ \circ
\let \zsym@dres \zdres
\let \zsym@rres \zrres
\def \zsym@ndres {\zmark@hbar{\zsym@dres}}
\def \zsym@nrres {\zmark@hbar{\zsym@rres}}
\let \zsym@inv \sim
%\def \zsym@limg {(\mskip-3.5mu|}
%\def \zsym@rimg {|\mskip-5mu)}
\DeclareMathSymbol{\zsym@limg}{\mathopen}{stmry}{"4C}% \llparenthesis in stmaryrd.sty
\DeclareMathSymbol{\zsym@rimg}{\mathopen}{stmry}{"4D}% \rrparenthesis
\let \zsym@oplus \oplus
\let \zsym@plus +
\let \zsym@star *
%%%%%%%%%%%%%%%%% A.2.5.3 - function toolkit symbols %
\def \zsym@pfun {\zmark@pvbar{\zsym@fun}}
\let \zsym@inj \zinj
\def \zsym@pinj {\zmark@pvbar{\zsym@inj}}
\def \zsym@surj {\zmark@darrow{\zsym@fun}{\zsym@fun}{4}} % lucida has 3 here
\def \zsym@bij {\zmark@darrow{\zsym@inj}{\zsym@fun}{5}} % lucida has 4 here
\def \zsym@psurj {\zmark@pvbar{\zsym@surj}}
\def \zsym@ffun {\zmark@fvbar{\zsym@fun}}
\def \zsym@finj {\zmark@fvbar{\zsym@inj}}
\def \zsym@disjoint {disjoint}
\def \zsym@partition {partition}
%%%%%%%%%%%%%%%%% A.2.5.4 - number toolkit symbols %
\def \zsym@num {\mathbb Z}
\def \zsym@negate {\mbox{-}}
\let \zsym@leq \leq
\let \zsym@geq \geq
\def \zsym@div {div}
\def \zsym@mod {mod}
% \def \zsym@miuns {-}
% \def \zsym@sum {+}
% \def \zsym@mult {*}
% \def \zsym@lessthan {<}
% \def \zsym@greaterthan {>}
%%%%%%%%%%%%%%%%% A.2.5.5 - sequence toolkit symbols %
\def \zsym@upto {\ldotp\ldotp}
\let \zsym@hash \#
\def \zsym@seq {seq}
\def \zsym@iseq {iseq}
%\langle
%\rangle
\def \zsym@cat {\zmark@cat}
\let \zsym@extract \zupharpoonleft
\let \zsym@filter \zupharpoonright
\def \zsym@prefix {prefix}
\def \zsym@suffix {suffix}
\def \zsym@infix {infix}
\def \zsym@dcat {{\zsym@cat}/}
% mathematical delimiters that can be used for box drawings
% (see LaTeX2e Font Selection guide @ fntguide.pdf).
\DeclareMathDelimiter{\zboxulcorner}{\mathopen}{AMSa}{"70}{AMSa}{"70}
\DeclareMathDelimiter{\zboxurcorner}{\mathclose}{AMSa}{"71}{AMSa}{"71}
\DeclareMathDelimiter{\zboxllcorner}{\mathopen}{AMSa}{"78}{AMSa}{"78}
\DeclareMathDelimiter{\zboxlrcorner}{\mathclose}{AMSa}{"79}{AMSa}{"79}
}
% sets the math version
\mathversion{czt}%
\PackageInfo{czt}{Current math version set to `czt'}
% changes the rendering of A-Z and a-z in specialised italics when in math mode.
%
% Quite elaborated loop that changes the rendering
% (\mathcode) of #1 to that of #3 until 1# >= #2.
%
% setmcodes(#1 % original mathcode
% #2 % upto threshold
% #3 % mathcode to substitute)
% begin
% var c0, c1 : Register;
% c0 =  c1 =  % fetch value of #1/#3 in c0/c1
% change_mcode(c0, c1); % make math code for c0 the value of c1
% while (c0 < ) do % while c0 has not reached value of #2
% begin
% c0++; c1++; % increment the values of source/target
% changeg_mcode(c0, c1); % make math code for c0 the value of c1
% end
% % all chars from #1..#2 changed to #3
% % incremented one by one.
% end
%
% called as: setmcodes{ }{ }{italics} % makes A-Z and a-z italic in math mode
%
% fuzz.sty has same code but calls with: \@setmcodes{`A}{`Z}{"7441}
% blend from: zed-csp.sty, soz.sty, oz.sty, fuzz.sty
%
% OBS: This is used in all Z styles. It seems to be originally from struktxf.sty
%
\def\@setmcodes#1#2#3{%
{\count0=#1 \count1=#3%
\loop \global\mathcode\count0=\count1%
\ifnum \count0<#2%
\advance\count0 by1 \advance\count1 by1%
\repeat}}
\def\z@mathit%
{%
\@setmcodes{`A}{`Z}{"7\hexnumber@\symitalics41}%
\@setmcodes{`a}{`z}{"7\hexnumber@\symitalics61}%
}
\def\z@mathrm%
{%
\@setmcodes{`A}{`Z}{"7141}
\@setmcodes{`a}{`z}{"7161}
}
% Depending on package options, load the right encoding.
% Or else, raise a warning and use math italics as default.
\if@mathrm@
\PackageInfo{czt}{Setting math code for letters as Roman}
\z@mathrm
\else
\if@mathit@
\PackageInfo{czt}{Setting math code for letters as Italics}
\z@mathit
\else
\PackageWarning{czt}{%
Could not resolve math code for letters.\MessageBreak%
Default could not be found. Using Italics}
\z@mathit
\fi
\fi
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Z definition counters %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% Flag used to switch command counting on/off, default=on
\newif\ifCountDefs
\CountDefstrue
\PackageInfo{czt}{Counting Z declarations? \ifCountDefs YES \else NO \fi}
% Low-level TeX register used to define what to count
% 0 = unboxed para
% 1 = axdef
% 2 = gendef
% 3 = schemas
% 4 = gen schemas
% 99= nothing
\newcount\@zcountingwhat
\@zcountingwhat=99
% Few counters used to calculate number of definitions used.
% Reset is controlled by flag/option, default is "cntglobally".
% Stared versions of environments, which are not parsed, are not counted.
% We do not care about parsing rules here (i.e., incorrect specs
% are going to be counted incorrectly).
%
% We have local and global counters. Global counters accumulate decls
% from the whole documents.
%
% Z paragraphs | Keywords used for counting
% unboxed items | \begin{zed}, \begin{theorem}
% axiomatic def. | \begin{axdef}
% gen. axdef | \begin{gendef}
% schemas | \begin{schema}{NAME}
% gen. schemas | \begin{schema}[X]{NAME}
%
% Counters:
% a) number of unboxed items: given set, freetype, abbreviation, conjectures, op. templates.
% b) number of axiomatic definitions
% c) number of generic axiomatic definitions
% d) number of schemas
% e) number of generic schemas
% f) total number of Z declarations
\newcounter{cntZunboxed} %a) local
\newcounter{cntZaxdef} %b) local
\newcounter{cntZgendef} %c) local
\newcounter{cntZschema} %d) local
\newcounter{cntZgenschema} %e) local
\newcounter{cntZdecl} %f) local
\newcounter{cntZtotunboxed} %a) global
\newcounter{cntZtotaxdef} %b) global
\newcounter{cntZtotgendef} %c) global
\newcounter{cntZtotschema} %d) global
\newcounter{cntZtotgenschema} %e) global
\newcounter{cntZtotdecl} %f) global
% update the reseting rationale based on package options.
% maybe put this code at the \DeclareOption part (?)
\if@cntbychapter@
\@addtoreset{cntZunboxed}{chapter}
\@addtoreset{cntZaxdef}{chapter}
\@addtoreset{cntZgendef}{chapter}
\@addtoreset{cntZschema}{chapter}
\@addtoreset{cntZgenschema}{chapter}
\@addtoreset{cntZdecl}{chapter}
\renewcommand{\thecntZunboxed}{\arabic{cntZunboxed} unboxed \ifnum \arabic{cntZaxdef} = 1 item \else items \fi in Chapter~\thechapter}
\renewcommand{\thecntZaxdef}{\arabic{cntZaxdef} axiomatic \ifnum \arabic{cntZaxdef} = 1 definition \else definitions \fi in Chapter~\thechapter}
\renewcommand{\thecntZgendef}{\arabic{cntZgendef} generic axiomatic \ifnum \arabic{cntZaxdef} = 1 definition \else definitions \fi in Chapter~\thechapter}
\renewcommand{\thecntZschema}{\arabic{cntZschema} \ifnum \arabic{cntZaxdef} = 1 schema \else schemas \fi in Chapter~\thechapter}
\renewcommand{\thecntZgenschema}{\arabic{cntZgenschema} generic \ifnum \arabic{cntZaxdef} = 1 schema \else schemas \fi in Chapter~\thechapter}
\renewcommand{\thecntZdecl}{\arabic{cntZdecl} in Chapter~\thechapter}
\else
\if@cntbysection@
\@addtoreset{cntZunboxed}{section}
\@addtoreset{cntZaxdef}{section}
\@addtoreset{cntZgendef}{section}
\@addtoreset{cntZschema}{section}
\@addtoreset{cntZgenschema}{section}
\@addtoreset{cntZdecl}{section}
\renewcommand{\thecntZunboxed}{\arabic{cntZunboxed} unboxed \ifnum \arabic{cntZaxdef} = 1 item \else items \fi in Section~\thesection}
\renewcommand{\thecntZaxdef}{\arabic{cntZaxdef} axiomatic \ifnum \arabic{cntZaxdef} = 1 definition \else definitions \fi in Section~\thesection}
\renewcommand{\thecntZgendef}{\arabic{cntZgendef} generic axiomatic \ifnum \arabic{cntZaxdef} = 1 definition \else definitions \fi in Section~\thesection}
\renewcommand{\thecntZschema}{\arabic{cntZschema} \ifnum \arabic{cntZaxdef} = 1 schema \else schemas \fi in Section~\thesection}
\renewcommand{\thecntZgenschema}{\arabic{cntZgenschema} generic \ifnum \arabic{cntZaxdef} = 1 schema \else schemas \fi in Section~\thesection}
\renewcommand{\thecntZdecl}{\arabic{cntZdecl} in Section~\thesection}
\fi
%\else \if@cntglobally@ \relax \fi
\fi
% counts the appropriate Z paragraph with correct
% dependant counter reseting according to the rule
% chosen by the package option given.
\def\@countZGlobal{\stepcounter{cntZdecl}\stepcounter{cntZtotdecl}}
\def\@countZPara{%
\ifCountDefs
\ifnum \@zcountingwhat = 0
%unboxed para code...
\stepcounter{cntZunboxed}
\stepcounter{cntZtotunboxed}
\@countZGlobal
\else
\ifnum \@zcountingwhat = 1
%axdef code...
\stepcounter{cntZaxdef}
\stepcounter{cntZtotaxdef}
\@countZGlobal
\else
\ifnum \@zcountingwhat = 2
%gendef code...
\stepcounter{cntZgendef}
\stepcounter{cntZtotgendef}
\@countZGlobal
\else
\ifnum \@zcountingwhat = 3
%schemas code...
\stepcounter{cntZschema}
\stepcounter{cntZtotschema}
\@countZGlobal
\else
\ifnum \@zcountingwhat = 4
%gen schemas code...
\stepcounter{cntZgenschema}
\stepcounter{cntZtotgenschema}
\@countZGlobal
\else
%don't count at all
\relax
\fi
\fi
\fi
\fi
\fi
\else
\relax
\fi
}
\def \ZDeclSummary {%
\ifCountDefs
\begin{table}[ht]
\begin{center}
\if@cntglobally@
\begin{tabular}{|l|r|}
\hline
\textbf{Declarations} & \textbf{Total} \\
\hline
Unboxed items & \arabic{cntZtotunboxed} \\
\hline
Axiomatic definitions & \arabic{cntZtotaxdef} \\
\hline
Generic axiomatic defs. & \arabic{cntZtotgendef} \\
\hline
Schemas & \arabic{cntZtotschema} \\
\hline
Generic schemas & \arabic{cntZtotgenschema} \\
\hline
\textbf{Total} & \textbf{\arabic{cntZtotdecl}} \\
\hline
\end{tabular}
\else
\def \@zcntpart {%
\if@cntbychapter@ Chapter \else \if@cntbysection@ Section \else ??? \fi \fi}
\begin{tabular}{|l|c|c|}
\hline
\textbf{Declarations} & \textbf{This \@zcntpart} & \textbf{Globally} \\
\hline
Unboxed items & \arabic{cntZunboxed} & \arabic{cntZtotunboxed} \\
\hline
Axiomatic definitions & \arabic{cntZaxdef} & \arabic{cntZtotaxdef} \\
\hline
Generic axiomatic defs. & \arabic{cntZgendef} & \arabic{cntZtotgendef} \\
\hline
Schemas & \arabic{cntZschema} & \arabic{cntZtotschema} \\
\hline
Generic schemas & \arabic{cntZgenschema} & \arabic{cntZtotgenschema} \\
\hline
\textbf{Total} & \textbf{\arabic{cntZdecl}} & \textbf{\arabic{cntZtotdecl}} \\
\hline
\end{tabular}
\fi
\end{center}
\if@cntglobally@
\caption{Summary of all Z declarations.}\label{tbl:zdecl:global}
\else
\if@cntbychapter@
\caption{Summary of Z declarations for Chapter~\thechapter.}\label{tbl:zdecl:\thechapter}
\else
\if@cntbysection@
\caption{Summary of Z declarations for Section~\thesection.}\label{tbl:zdecl:\thesection}
\fi
\fi
\fi
\end{table}
\else
\relax
\fi
}
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Z registers: skip, dimen, tab, etc %
% blend: oz.sty, soz.sty, ltcadiz.sty, zed-csp.sty, fuzz.sty %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
%%%%%%%%%% new registers %
% dimen used to:
\newdimen\big@size % 1) calculate the increase on \z@XXXop modifiers
\newdimen\zedtab % 2) define the tab stop (\tn) increment
\newdimen\zedindent % 3) controls how to indent new lines within z para mode
\newdimen\zedleftsep % 4) determinsed how far within a topline letters should appear(?)
\newdimen\zedbar % 5) length horizontal bar in z box drawings
%\newdimen\zedlinethickness % 6) thinkness of z box drawins lines - oz.sty only? TODO: add behaviour if needed
%\newdimen\zedcornerheight % 7) height of corners in z box drawings - oz.sty only?
% counter used to:
\newcount\interzedlinepenalty
\newcount\preboxpenalty
\newcount\forcepagepenalty
% skip used to:
\newskip\zedskip % 1) amount of vertical space inserted by \also
% LaTeX conditional used to:
\newif\ifzt@p % 1) determines whether LaTeX is in z paragraph mode
%%%%%%%%%% registers initialisation %
% initialisation of dimens
\zedtab=2em%
\zedindent=\leftmargini
\zedleftsep=1em
\zedbar=6em % oz.sty = 8em
%\zedlinethickness=0.4pt
%\zedcornerheight=0pt
% initialisation of counters
\interzedlinepenalty=10000 %never break
\preboxpenalty=0 %break easily
\forcepagepenalty=-10000 %always break
\interdisplaylinepenalty=100 %break sometimes
% initialisation of skips
\zedskip=0.5\baselineskip%
plus0.333333\baselineskip%
minus0.333333\baselineskip%
% \zedskip=\medskipamount from fuzz.sty
% initialisation of if-flags (LaTeX conditionals)
\zt@pfalse
\PackageInfo{czt}{%
Initialising Z registers with default values.\MessageBreak
\space\space\space\protect\zedtab=\the\zedtab \MessageBreak%
\space\space\space\protect\zedindent=\the\zedindent=\protect\leftmargini \MessageBreak%
\space\space\space\protect\zedleftsep=\the\zedleftsep \MessageBreak%
\space\space\space\protect\zedbar=\the\zedbar \MessageBreak %
\MessageBreak
\space\space\space\protect\interzedlinepenalty=\the\interzedlinepenalty \MessageBreak%never break
\space\space\space\protect\preboxpenalty=\the\preboxpenalty \MessageBreak%break easily
\space\space\space\protect\forcepagepenalty=\the\forcepagepenalty\MessageBreak%always break
\space\space\space\protect\interdisplaylinepenalty=\the\interdisplaylinepenalty \MessageBreak%break sometimes
\MessageBreak
\space\space\space\protect\zedskip=\the\zedskip \MessageBreak%
\space\space\space\protect\zt@p=\ifzt@p true \else false \fi\MessageBreak%
\space\space\space\protect\CountDefstrue=\ifCountDefs true \else false \fi%
}
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Z spaces, skips, tabs, etc (using the Z registers) %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% Tab stops from \t1 to \t9 - relative to \zedtab
\def\t#1{\hskip #1\zedtab}
% Small vertical space within z paragraph mode - relative to \zedskip
\def\@also{\crcr \noalign{\penalty\interdisplaylinepenalty\vskip\zedskip}}
\def\also{\ifnum \@zcountingwhat = 0 \@countZPara \fi \@also}
% varied spacing based in \also - from oz.sty
\def\@Also{\@also\@also}
\def\@ALSO{\@Also\@Also}
\def\Also{\@countZPara\@Also}
\def\ALSO{\@countZPara\@Also\@Also}
% forces a page break within z paragraph mode
\def\znewpage{\@also\noalign{\penalty\forcepagepenalty}\@also}
% forces a formula break within z paragraph mode.
% varied relative spacing added before/after it.
\def\zbreak{\@also\noalign{\penalty\interdisplaylinepenalty\vskip-\zedskip}\@also}
\def\zBreak{\@also\noalign{\penalty\interdisplaylinepenalty}\@also}
\def\ZBREAK{\@Also\noalign{\penalty\interdisplaylinepenalty}\@Also}
\PackageInfo{czt}{Setting up Standard Z skipping and breaking}
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Basic definitions for Z box drawings - mostly from zed-csp.sty%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
%%%%%%%%%% indent, sizes, skips, padding, new line behaviour %
% various indentation levels depending on the vertical placement
% to be called whenever within vertical mode (\ifvmode = true)
\def\@zleavevmode{%
\if@inlabel
\indent
\else
\if@noskipsec
\indent
\else
\if@nobreak
\global\@nobreakfalse \everypar={}\abovedisplayskip=0pt
\fi
{\parskip=0pt\noindent}
\fi
\fi}
%\def\@zleavevmode{\if@inlabel \indent
% \else\if@noskipsec \indent
% \else\if@nobreak \global\@nobreakfalse
% \everypar={}\abovedisplayskip=0pt\fi
% {\parskip=0pt\noindent}\fi\fi}
% nested (dynamic) command definition to change skip sizes.
% it first saves the display skips; changes it; then restores
% the skips back. This is done incrementally.
\def\z@size{}%
\def\@setzsize{%
\let\next=\@nomath%
\def\@nomath##1{}%
\skip0=\abovedisplayskip\skip1=\belowdisplayskip
\z@size
\let\@nomath=\next
\abovedisplayskip=\skip0\belowdisplayskip=\skip1}
% code that affects the size of Z symbols within formulas without
% actually affecting the surrounding text. e.g., \zedsize{\large}
% (see ozguide.pdf, p. 7).
\def\zedsize#1{\def\z@size{#1}}
% changes the behaviour of new line so that appropriate
% skip and side bar is added. if within z paragraph mode \zt@p = false
\def\@znoskip{\offinterlineskip
\everycr={\noalign{%
\ifzt@p
\global\zt@pfalse
\ifdim\prevdepth>-1000pt
\skip0=\normalbaselineskip
\advance\skip0by-\prevdepth
\advance\skip0by-\ht\strutbox
\ifdim\skip0<\normallineskiplimit
\vskip\normallineskip
\else
\vskip\skip0
\fi
\fi
\else
\penalty\interzedlinepenalty
\fi}}}
% a relative bit of \zedskip
\def\@jot{0.5\zedskip}
% fill a line with appropriate width
\def\@zrulefill{\leaders\hrule height\arrayrulewidth\hfill}
% creates a particular skip after new lines? - (old) zed.sty
\def\@zskip#1{\crcr \omit \hbox{\color{ZedBoxColor}\vrule height#1%
width\arrayrulewidth} \cr}
%\def\@zskip#1{\crcr \omit \vrule height#1 width\arrayrulewidth \cr} zed-csp.sty
% add a tabskip for each new line (?)
\def\@zlign{\tabskip\z@skip\everycr{}}
%%%%%%%%%% individual line drawing %
% creates a top line for schema and other boxes with specific width.
% then creates an \hbox relative to \zedleftsep filled with appropriate spacing.
% #1 = possible name or generic parameters to be added
\def\@topline#1{\hbox to\linewidth{%
\color{ZedBoxColor}%
\vrule height\arrayrulewidth width\arrayrulewidth
\vrule height0pt depth\@jot width0pt
\hbox to\zedleftsep{\@zrulefill\thinspace}%
{\color{ZedColor}#1}\thinspace\@zrulefill}}
% creates a line of sorts. - used (old) zed.sty
\def\@zedline{\omit\hbox to 0pt{\color{ZedBoxColor}\vrule
height\arrayrulewidth width\linewidth\hss} \cr}
%\def\@zedline{\omit \vrule height\arrayrulewidth width\linewidth \cr} zed-csp.sty
% creates a narrow line with \zedindent width
\def\@narrow{\advance\linewidth by-\zedindent}
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Z boxes drawings + paragraph markers + box rendering %
% - mostly from zed-csp.sty (few things from oz.sty) %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
%%%%%%%%%% basic ZEDCHAR definition %
% 1) adds appropriate spacing if in vertical mode
% 2) enters "zed" paragraph mode - \zt@p flag = true
% 3) change skip sizes
% 4) thickens line by negative \zedindent (?)
% 5) increased display indent (?)
% 6) fix new lines and tab stopping
\def\@@zed{\ifvmode\@zleavevmode\fi
$$\global\zt@ptrue
\@setzsize
\advance\linewidth by-\zedindent
\advance\displayindent by\zedindent
% Count this declaration
\@countZPara
% Must have \def and not \let for nested alignments.
% Also, count extra definitions at each "\\", whenever within
% a unboxed paragraph. Changed "\also" accordingly.
\def\\{\crcr \ifnum \@zcountingwhat = 0 \@countZPara \fi}
\let\par=\relax
\tabskip=0pt}
\def\@zed{%
\@@zed\@znoskip\halign to\linewidth\bgroup
{\strut$\color{ZedColor}\@zlign##$}\hfil \tabskip=0pt plus1fil\cr}
%%%%%%%%%% \begin{zed}\end{zed} definition %
% corresponds to "ZEDCHAR" markup in LaTeX for horizontal para
%
% 1) enters z paragraph mode, which sets \zt@p = true
% 2) changes \cr behaviour to pad next line with spaces, which flips \zt@p = false
% 3) changes the tabskip (\zling) for each tabskip (?)
% 4) restores tabskip after the new line (\cr) (?)
\def\zed{%
\@zcountingwhat=0 % sets the kind of counter to addto, 0=unboxed para
\@zed}
% corresponds to "ENDCHAR" markup in LaTeX
%
% 1) restores paragraph and group balancing (i.e., leaves z mode)
% 2) \@ignoretrue makes sure there are no trailing spaces after \end{zed}
\def\endzed{\crcr\egroup$$\global\@ignoretrue}
% stared version which is ignored by the parser.
% - don't count it, set \@zcountingwhat=99
\@namedef{zed*}{\@zcountingwhat=99 \@zed}
\expandafter\let\csname endzed*\endcsname=\endzed
% change displaymath environment to behave just like \begin{zed}\end{zed}
\def\[{\begingroup \@zcountingwhat=99 \@zed}
\def\]{\crcr\egroup$$\endgroup\ignorespaces}
% corresponds to "ZEDCHAR" markup in LaTeX for section headers
% zsection environment
\let\zsection=\zed
\let\endzsection=\endzed
% z named conjecture or theorem environment
%
% 1) if theorem is followed by "[" - std z has no ability or label
%\def\theorem#1{\@ifnextchar[{\@theorem{#1}}{\@@theorem{#1}}} % ]
%\def\@theorem#1[#2]{\@@theorem{#1 $[#2]$}}
%
% 2) just puts the theorem in a bold name
\def\theorem#1{\@@theorem{#1}}
\def\@@theorem#1{%
\@zcountingwhat=0 % sets the kind of counter to addto, 0=unboxed para
\@@zed\@znoskip\halign to\linewidth\bgroup%
{\strut$\color{ZedColor}\@zlign\hskip\zedleftsep##$}\hfil \tabskip=0pt plus1fil\crcr
\hskip -\zedleftsep\hbox{\bf theorem \rm {\color{ZedColor}#1}}\crcr}
%\def\@ability{\relax} % don't follow why z-eves needed this command here. = no need.
% synonym for \endzed - could not add colour to the theorem's body :-(
%\def\endtheorem{\color{ZedColor}\endzed}
\let\endtheorem=\endzed
%%%%%%%%%% \begin{axdef}\end{axdef} definition %
% TODO: create a general command for entering zed paragraph mode
% corresponds to "AXCHAR" markup in LaTeX
%
% 1) enters z paragraph mode with \@@zed
% 2) changes the behaviour of padding and new lines, just
% like in \zed but with a side line displayed
% 3) ???
\def\@axdef{%
\def\also{\@zskip\zedskip}%
\predisplaypenalty=\preboxpenalty
\@@zed\@znoskip \halign to\linewidth\bgroup
\strut{\color{ZedBoxColor}\vrule width\arrayrulewidth} \hskip\zedleftsep
{$\color{ZedColor}\@zlign##$}\hfil \tabskip=0pt plus1fil\cr}
\def\axdef{%
\@zcountingwhat=1 % sets the kind of counter to addto, 1=axdef para
\@axdef}
% synonym for \endzed
\let\endaxdef=\endzed
% stared version which is ignored by the parser.
\@namedef{axdef*}{\@zcountingwhat=99 \@axdef}
\expandafter\let\csname endaxdef*\endcsname=\endaxdef
%%%%%%%%%% \begin{schema}{NAME}[X]\end{schema} definition %
% corresponds to "SCHCHAR" markup in LaTeX
%
% 1) check to see if \begin{schema}?#1 is followed by "["
% 2) if it is, we have a generic schema, in which case
% \@@nschema{#1[#2]} is called, where #1=name, #2=formals
% 3) otherwise, \@@nschema{#1} is called, where #1=name
% 4) \@@nschema draws a narrow \axdef with the name #1 in the middle
\def\schema#1{\@ifnextchar[{\@zcountingwhat=4 \@@schema{#1}} {\@zcountingwhat=3 \@@nschema{#1}}}
\def\@schema#1{\@zcountingwhat=99 \@ifnextchar[{\@@schema{#1}}{\@@nschema{#1}}}
\def\@@schema#1[#2]{\@@nschema{#1[#2]}}
\def\@@nschema#1{\@narrow\@axdef \omit\@topline{$\strut#1$}\cr}
% just like \endzed but with a final underline to close
% the schema box, right after restoring the skip mode.
\def\endschema{\@zskip\@jot \@zedline \endzed}
% for schemas without name, use \begin{plainschema}
% it is ignored by the parser
\def\plainschema{\@narrow \@zcountingwhat=3 \@axdef \@zedline \@zskip\@jot}
\let\endplainschema=\endschema
% similarly, one could use the stared version of the
% schema environment, which accepts name and/or generic
% formals, but is ignored by the parser.
\@namedef{schema*}{\@schema} % don't count those
\expandafter\let\csname endschema*\endcsname=\endschema
%%%%%%%%%% \begin{gendef}[X]\end{gendef} definition %
% corresponds to "AXCHAR GENCHAR" markup in LaTeX
%
% 1) check to see if \begin{gendef}?#1 is followed by "["
% 2) if it is, we have a generic axdef with generic formals,
% in which case \@@ngendef is called to draw double lines
% 3) otherwise, \@@gendef is called to draw double lines but
% with the generic formals given
% 4) lines are draw similarly to \axdef but doubled
\def\gendef{\@zcountingwhat=2 \@ifnextchar[{\@@gendef}{\@@ngendef}}
\def\@gendef{\@zcountingwhat=99 \@ifnextchar[{\@@gendef}{\@@ngendef}}
\def\@@gendef[#1]{\@narrow \@axdef \omit \setbox0=\hbox{$\strut[#1]$}%
\rlap{\raise\doublerulesep\@topline{\hskip\wd0}}\@topline{\box0}\cr}
\def\@@ngendef{\@narrow \@axdef \@zedline \omit \hbox to\linewidth{\vrule
height\doublerulesep width\arrayrulewidth \@zrulefill}\cr
\@zskip\@jot
}
% synonym for \endschema
\let\endgendef=\endschema
% stared version which is ignored by the parser.
\@namedef{gendef*}{\@gendef} % don't count it
\expandafter\let\csname endgendef*\endcsname=\endgendef
%%%%%%%%%% \where separator definition %
% draws the |- line separating declarations from predicates (zed.sty)
\def\where{\@zskip\@jot
\omit\hbox{\color{ZedBoxColor}\vrule height\arrayrulewidth width\zedbar} \cr
\@zskip\@jot}
%\def\where{\@zskip\@jot zed-csp.sty
% \omit \vrule height\arrayrulewidth width\zedbar \cr
% \@zskip\@jot}
\PackageInfo{czt}{Setting up Standard Z LaTeX environments}
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Basic definitions for Z symbols. %
% Mathematical operators classes - Add \mathstrut for boxing %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% The spacing chosen for the math operators should reflect
% their precedences, as defined using the Markup directives.
% That is, function, generic, and schema operators bind
% tighter than relation and predicate logic operators.
% The former are to be \mathbin, whereas the latter are to
% be \mathrel (thanks to Ian Toyn's clarification on the
% CZT mail thread of 24/09/2008).
%
% SUMMARY: Function, generic, schema op = \mathbin
% Relation, predicate logic op = \mathrel
%
% Core symbols and keywords have fixed precedences, and we
% wrap them accordingly. Markup directives have their fixture
% hinting which spacing should they have. For the list of
% core symbols precedence see ISOZ Table 31 p.37.
%
% \z@op = general operator given with \nolimits
% \z@preop = prefix operator spacing - Zprechar / Zpreword
% \z@postop = postfix operator spacing - Zpostchar / Zpostword
% \z@relop = infix operator spacing - Zinchar / Zinword (\;)
% \z@binop = infix operator spacing - Zinchar / Zinword (\:)
% \z@ordop = ordinary char spacing - Zchar / Zword
%
% IMPORTANT:
%
% User defined \LaTeX{} commands used as markup directives
% should take these spacing rules into account, hence wrap
% it with the proper \zXXop.
%
% For that, we provide equivalent macro names without @ so
% that users specifying new commands for markup directives
% can add the appropriate spacing rule.
% (see LaTeX Companion 2nd Ed Table 8.7, p.525)
%
% We need the original commands with the \z@ prefix as this is
% used for slightly increasing/decreasing their size.
%
% LATEX DETAILS:
%
% The use of \nolimits is important for mathematical symbols used
% as keywords as it finely control typesetting and raise errors.
% For the user command form of \z@op, one should refer to \keyword
% (see LaTeX Companion 2nd Ed p.492, 903)
%
% The use of \mathstrut is important only when the symbol may
% appear within other symbols (e.g., \sqrt{y} vs. \sqrt{\mathstrut y}).
% For the Z operators, we tried to compromise between consistency
% and simplicity.
%
% That is, some operators were already relation/binary and we avoided
% redefining them just to add the \mathstrut. For these cases where
% we did not add \mathstrut, a note is added.
% TODO: this is experimental check if need to add everywhere.
%
\def\z@op#1{\mathstrut{#1}}
\def\z@preop#1{\mathop{\z@op{#1}}\nolimits}
\def\z@postop#1{\mathop{\z@op{#1}}\nolimits}
\def\z@relop#1{\mathrel{\mathstrut{#1}}}
\def\z@binop#1{\mathbin{\mathstrut{#1}}}
\def\z@ordop#1{\mathord{#1}}
\def\z@openop#1{\mathopen{#1}}
\def\z@closeop#1{\mathclose{#1}}
\let\zpreop=\z@preop
\let\zpostop=\z@postop
\let\zbinop=\z@binop
\let\zrelop=\z@relop
\let\zordop=\z@ordop
\let\zopenop=\z@openop
\let\zcloseop=\z@closeop
% these operators are reused with increased/reduced size.
% for that we provide increasing/reducing macros for them.
% they come from oz.sty
%
% the (weird) algorithm that calculates the increment based on \big@size
\def\bBigg@#1#2{%
\mbox{\ifcase#1\or\large\or\Large\or\LARGE\or\small\or\footnotesize\fi
$#2$}\nulldelimiterspace\z@ \m@th}
\addto@hook\every@math@size{\setbox\z@\vbox{\hbox{$($}\kern\z@}%
\big@size 1.2\ht\z@}
%
% each relative increment
\def\zBIG{\bBigg@{3}}
\def\zBig{\bBigg@{2}}
\def\zbig{\bBigg@{1}}
\def\zsmall{\bBigg@{4}}
\def\zSmall{\bBigg@{5}}
%
% and their version with varied sizes
\def\z@bigpreop#1{\z@preop{\zbig{#1}}}
\def\z@bigpostop#1{\z@postp{\zbig{#1}}}
\def\z@bigbinop#1{\z@binop{\zbig{#1}}}
\def\z@bigrelop#1{\z@relop{\zbig{#1}}}
%
\def\z@Bigpreop#1{\z@preop{\zBig{#1}}}
\def\z@Bigpostop#1{\z@postp{\zBig{#1}}}
\def\z@Bigbinop#1{\z@binop{\zBig{#1}}}
\def\z@Bigrelop#1{\z@relop{\zBig{#1}}}
%
\def\z@smallpreop#1{\z@preop{\zsmall{#1}}}
\def\z@smallpostop#1{\z@postp{\zsmall{#1}}}
\def\z@smallbinop#1{\z@binop{\zsmall{#1}}}
\def\z@smallrelop#1{\z@relop{\zsmall{#1}}}
\PackageInfo{czt}{Setting up Standard Z basic symbols}
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Z core characters and words (ISOZ A.2.4) %
% adjustment to spacing and boxing + added consistently %
% normalised names to \zsym@XXX to simplify diff. font loading %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
%%%%%%%%%%%%%%%%% A.2.4.1 - Greek alphabet treated as operators %
% Save the original symbols - use before adjusting \mathstrut
\def \Delta {\zordop{\zsym@Delta}}
\def \Xi {\zordop{\zsym@Xi}}
\def \theta {\zpreop{\zsym@theta}}
\def \lambda {\zpreop{\zsym@lambda}}
\def \mu {\zpreop{\zsym@mu}}
%%%%%%%%%%%%%%%%% A.2.4.2 - Other letter characters %
% blackboard bold letters + power set is a primitive prefix operator
\def \arithmos {\zordop{\zsym@arithmos}}
\def \nat {\zordop{\zsym@nat}}
\def \power {\zpreop{\zsym@power}}
% Being Zchar, these Greek letters should be surrounded
% by \zordop. As they are already \mathord, the only
% difference is because of a missing \mathstrut.
% Yet, for when conditionally loading symbols from different
% fonts, it is useful to have meta symbols like all others.
%
\def \alpha {\zordop{\zsym@alpha}}
\def \beta {\zordop{\zsym@beta}}
\def \gamma {\zordop{\zsym@gamma}}
\def \delta {\zordop{\zsym@delta}}
\def \epsilon {\zordop{\zsym@epsilon}}
\def \zeta {\zordop{\zsym@zeta}}
\def \eta {\zordop{\zsym@eta}}
\def \iota {\zordop{\zsym@iota}}
\def \kappa {\zordop{\zsym@kappa}}
\def \nu {\zordop{\zsym@nu}}
\def \xi {\zordop{\zsym@xi}}
\def \pi {\zordop{\zsym@pi}}
\def \rho {\zordop{\zsym@rho}}
\def \sigma {\zordop{\zsym@sigma}}
\def \tau {\zordop{\zsym@tau}}
\def \upsilon {\zordop{\zsym@upsilon}}
\def \phi {\zordop{\zsym@phi}}
\def \chi {\zordop{\zsym@chi}}
\def \psi {\zordop{\zsym@psi}}
\def \omega {\zordop{\zsym@omega}}
\def \Gamma {\zordop{\zsym@Gamma}}
\def \Theta {\zordop{\zsym@Theta}}
\def \Lambda {\zordop{\zsym@Lambda}}
\def \Pi {\zordop{\zsym@Pi}}
\def \Sigma {\zordop{\zsym@Sigma}}
\def \Upsilon {\zordop{\zsym@Upsilon}}
\def \Phi {\zordop{\zsym@Phi}}
\def \Psi {\zordop{\zsym@Psi}}
\def \Omega {\zordop{\zsym@Omega}}
\PackageInfo{czt}{Setting up Standard Z Greek and other letters}
%%%%%%%%%%%%%%%%% A.2.4.3 - Special characters %
% Underscore redefined - used oz.sty width + zed-csp \ifmmode
%\def\_{\leavevmode \vbox{\hrule width0.4em}}
\def\_{\leavevmode \ifmmode\else\kern0.06em\fi \vbox{\hrule width0.5em}}
% Make free type ampersand spacing nicely
\let\zamp=\&
\def\&{\ifmmode \;\zbinop{\zamp} \else ~\zamp~ \fi}
% Hard space redefined - used zed-csp.sty
% in math mode ~=\, ; outside, it is "\@M\ "
% TODO: find out what \@M means!
\def~{\ifmmode\,\else\penalty\@M\ \fi}
% additional Z brackets: bindings + free type constructors
% they are not \zordop because \langle is \mathopen/close
\def \lblot {\zsym@lblot}
\def \rblot {\zsym@rblot}
\def \ldata {\zsym@ldata}
\def \rdata {\zsym@rdata}
%\langle
%\rangle
% Fat spot: used for separating predicates and expressions
\def \spot {\zrelop{\zsym@spot}}
% Set membership with added \mathstrut
\def\in {\zrelop{\zsym@in}}
% Treat ``@'' treated as \spot and ``|'' as \mid
% That is, make then space as function operators
%
\mathcode`\|=\mid
\mathchardef\semicolon="603B
\mathcode`\;="8000 % makes ; active in math mode
{\catcode`\;=\active \gdef;{\semicolon\;}}
\mathcode`\@="8000 % makes @ active in math mode
{\catcode`\@=\active \gdef@{\spot}}
% zed-csp.sty had this for quotes, needed?
\def\@kwote#1"{\hbox{\mathit{#1}}}
\mathcode`\"="8000 % makes " active in math mode
{\catcode`\"=\active \global\let"=\@kwote}
\PackageInfo{czt}{Setting up Standard Z bracket symbols}
\PackageInfo{czt}{Marking \protect\mid, \protect\semicolon,
and \protect\spot \MessageBreak %
as \MessageBreak active in math mode}
%%%%%%%%%%%%%%%%% A.2.4.4 - symbol characters predicate logic %
%
% Redefine logical ops as relational rather than binary ops.
% That is because function, schema and generic operators bind
% tighter than relation and predicate logic operators. Thus,
% the former needs to be \mathbin, whereas the latter are \mathrel.
% Generic Z operators
\def \vdash {\zpreop{\zsym@vdash}}
\def \cross {\zbinop{\zsym@cross}}
% Schema operators defined as slightly bigger with \z@Bigbinop
\def \hide {\zrelop{\z@Bigbinop{\zsym@solidus}}}
\def \project {\zrelop{\z@Bigbinop{\zsym@upharpoonright}}}
\def \semi {\zrelop{\z@Bigbinop{\zsym@comp}}}
\def \pipe {\zrelop{\z@bigbinop{\zsym@pipe}}}
\def \typecolon {\zrelop{\z@bigbinop{\zsym@typecolon}}}
% Z schema renaming or predicate substitution as an operator
% rather than a core symbol. \rename is not in the standard,
% (came from oz.sty). The advantage here is that one could
% have better rendering of complex expression because of the
% use of \left[ instead of just `['.
%
% TODO: discuss if it is worth making it a markup directive?
%
%\def\zfor {/} % solidus char
%\def\z@rename*[#1/#2]{\left[#1 \over #2\right]}
%\def\z@@rename[#1/#2]{\left[#1 \zfor #2\right]}
%\def\rename{\@ifnextchar*{\z@rename}{\z@@rename}}
% Predicate and propositional Logic operators - \mathrel please.
%
\def \lnot {\zordop{\zsym@not}}
\def \land {\zrelop{\zsym@and}}
\def \lor {\zrelop{\zsym@or}}
\def \implies {\zrelop{\zsym@implies}}
\def \iff {\zrelop{\zsym@iff}}
\def \forall {\zpreop{\zsym@forall}}
\def \exists {\zpreop{\zsym@exists}}
\PackageInfo{czt}{Setting up Standard Z predicate logic symbols}
%%%%%%%%%%%%%%%%% A.2.4.5 - core words (keywords) %
%
% A \z@word is a function-like operator (see \z@op) with \nolimits.
% A \z@boldword is a boldface \z@word.
% A \zword is a roman string (within a \mbox) \z@word.
% A \zkeyword is a boldface roman string (within a \mbox) \z@word.
%
% \zword is for defining toolkit symbols, as in \dom, \seq, etc.
% \zkeyword is for language keywords. For Z they are the Z Std keywords.
% \ztoolkit is either \zword or \zkeyword depending on the \@tkkeyword@ option
%
% Toolkit builders are encouraged to use \ztoolkit for their markup directives.
% Language extension style files should use \zkeyword for new keywords.
% For infix or prefix keywords, just insert the appropriate \zXXXop
%
\def\z@word#1{\z@op{#1}}
\def\z@boldword#1{\z@word{\textbf{#1}}}
\def\zword#1{\z@word{\mbox{\textrm{#1}}}}
\def\zkeyword#1{\z@word{\mbox{\textrm{\textbf{#1}}}}}
\def\ztoolkit#1{\if@tkkeyword@ \zkeyword{#1} \else \zword{#1} \fi}
% Z keywords - scattered in the ZStd. They are collected
% in full at "net.sourceforge.czt.parser.z.ZKeyword.java"
%
% sections
\def \SECTION {\zpreop{\zkeyword{section}}}
\def \parents {\zpreop{\zkeyword{parents}}}
%
% if-then-else
\def \IF {\zpreop{\zkeyword{if}}}
\def \THEN {\zbinop{\zkeyword{then}}}
\def \ELSE {\zbinop{\zkeyword{else}}}
%
% let
\def \LET {\zpreop{\zkeyword{let}}}
%
% boolean values - used in ZStd in the Z logic only
% can be used by users that want to define \bool as
% the free type "\bool ::= \false | \true".
\def \true {\zordop{\zkeyword{true}}}
\def \false {\zordop{\zkeyword{false}}}
%
% operator template keywords
\def \function {\zpreop{\zkeyword{function}}}
\def \relation {\zpreop{\zkeyword{relation}}}
\def \generic {\zpreop{\zkeyword{generic}}}
\def \leftassoc {\zbinop{\zkeyword{leftassoc}}}
\def \rightassoc{\zbinop{\zkeyword{rightassoc}}}
%
% schema precondition
\def \pre {\zpreop{\zkeyword{pre}}}
%
% being a Zinword expression, \listarg is \zbinop
% \varg is a synonym for \_ in operator templates
\def \listarg {\zbinop{\zkeyword{,,}}}
\def \varg {\zbinop{\zkeyword{\_}}}
\PackageInfo{czt}{Setting up Standard Z keywords}
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Z mathematical toolkit characters and words (ISOZ A.2.5) %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
\PackageInfo{czt}{\space\space Loading prelude\space\space\space\space\space\space\space\space\space\space symbols}
% NOTE: adjustment to spacing (\mathrel/bin) and boxing (\mathstrut)
%
% Spacing of operator templates and toolkit characters:
%
% \zbinop = Function (F) or Generic (G)
% \zrelop = Relation (R)
%
% \zordop = Zchar or Zword (D) (unless these are used)
% \zpreop = Zprechar or Zpreword (O) (for operator templates)
%
% TODO: Discuss... [wait to see how it renders]
% Shall I really rename all these already relational
% operators just to add \mathstrut to then?
%%%%%%%%%%%%%%%%% A.2.5.1 - set toolkit symbols %
\def \rel {\zbinop{\zsym@rel}} % G
\def \fun {\zbinop{\zsym@fun}} % G
\def \notin {\zbinop{\zsym@notin}} % R
\def \neq {\zrelop{\zsym@neq}} % R
\def \emptyset {\zordop{\zsym@emptyset}} % D
\def \subseteq {\zrelop{\zsym@subseteq}} % R
\def \subset {\zrelop{\zsym@subset}} % R
\def \cup {\zbinop{\zsym@cup}} % F
\def \cap {\zbinop{\zsym@cap}} % F
\def \setminus {\zbinop{\zsym@setminus}} % F
\def \symdiff {\zbinop{\zsym@symdiff}} % F
\def \bigcup {\zpreop{\zsym@bigcup}} % O
\def \bigcap {\zpreop{\zsym@bigcap}} % O
\def \finset {\zpreop{\zsym@finset}} % O
\PackageInfo{czt}{\space\space Loading set\space\space\space\space\space\space toolkit symbols}
%%%%%%%%%%%%%%%%% A.2.5.2 - relation toolkit symbols %
% superscript maths is aligned/spaced differently
% hence no change (see LaTeX Companion 8.7.5 p.505)
%
% NOTE: ISOZ A.2.5.2 does not add wordglue to \inv! TODO: check std bug?
\def \mapsto {\zbinop{\zsym@mapsto}} % F
\def \dom {\zpreop{\ztoolkit{\zsym@dom}}} % O
\def \ran {\zpreop{\ztoolkit{\zsym@ran}}} % O
\def \id {\zpreop{\ztoolkit{\zsym@id}}} % G
\def \comp {\zbinop{\zsym@comp}} % F
\def \circ {\zbinop{\zsym@circ}} % F
\def \dres {\zbinop{\zsym@dres}} % F
\def \rres {\zbinop{\zsym@rres}} % F
\def \ndres {\zbinop{\zsym@ndres}} % F
\def \nrres {\zbinop{\zsym@nrres}} % F
\def \inv {\zpostop{^\zsym@inv}} % F - ZStd alternative should be {^\zsym@inv}
\def \limg {\zbinop{\zsym@limg}} % F
\def \rimg {\zpostop{\zsym@rimg}} % F - it's a Zposchar!
\def \oplus {\zbinop{\zsym@oplus}} % F
\def \plus {\zpostop{^\zsym@plus}} % F - superscripts spaces differently
\def \star {\zpostop{^\zsym@star}} % F
\PackageInfo{czt}{\space\space Loading relation toolkit symbols}
%%%%%%%%%%%%%%%%% A.2.5.3 - function toolkit symbols %
\def \pfun {\zbinop{\zsym@pfun}} % G
\def \inj {\zbinop{\zsym@inj}} % G
\def \pinj {\zbinop{\zsym@pinj}} % G
\def \surj {\zbinop{\zsym@surj}} % G
\def \bij {\zbinop{\zsym@bij}} % G
\def \psurj {\zbinop{\zsym@surj}} % G
\def \ffun {\zbinop{\zsym@ffun}} % G
\def \finj {\zbinop{\zsym@finj}} % G
\def \disjoint {\zpreop{\ztoolkit{\zsym@disjoint}}} % G
\def \partition {\zbinop{\ztoolkit{\zsym@partition}}} % G
\PackageInfo{czt}{\space\space Loading function toolkit symbols}
%%%%%%%%%%%%%%%%% A.2.5.4 - number toolkit symbols %
\def\num {\zordop{\zsym@num}} % D
\def\negate {\zpreop{\zsym@negate}} % F
\def\leq {\zrelop{\zsym@leq}} % R
\def\geq {\zrelop{\zsym@geq}} % R
\def\div {\zbinop{\ztoolkit{\zsym@div}}} % F
\def\mod {\zbinop{\ztoolkit{\zsym@mod}}} % F
%\def-{\zbinop{\zsym@miuns}} % F
%\def+{\zbinop{\zsym@sum}} % F
%\def*{\zbinop{\zsym@mult}} % F
%\def<{\zrelop{\zsym@lessthan}} % R
%\def>{\zrelop{\zsym@greaterthan}} % R
\PackageInfo{czt}{\space\space Loading number\space\space\space toolkit symbols}
%%%%%%%%%%%%%%%%% A.2.5.5 - sequence toolkit symbols %
% NOTE: As with \{ and \}, I am not redefining \langle and \rangle
% Also, \# is not being given as a \zpreop - # is low level
% and I don't know how to "influence" its spacing in \#
%
% MINOR: R~^{~n~} : hard spaces are mandatory for parsing
%
% Relational iteration, as in R~^{~n~}, have superscripts and
% a prefix operator. R alone will be treated as \mathord (rather
% than \mathop), and I do not know how to accommodate that :-(
\def \upto {\zbinop{\zsym@upto}} % F
\def \seq {\zpreop{\ztoolkit{seq}}} % G
\def \iseq {\zpreop{\ztoolkit{iseq}}} % G
\def \cat {\zbinop{\zsym@cat}} % F
\def \extract {\zbinop{\zsym@extract}} % F
\def \filter {\zbinop{\zsym@filter}} % F
\def \prefix {\zbinop{\ztoolkit{\zsym@prefix}}} % R
\def \suffix {\zbinop{\ztoolkit{\zsym@suffix}}} % R
\def \infix {\zbinop{\ztoolkit{\zsym@infix}}} % R
\def \dcat {\zpreop{\zsym@dcat}} % D
%\langle % F
%\rangle % F
\def\#{\zpreop{\zsym@hash}} % F
\PackageInfo{czt}{\space\space Loading sequence toolkit symbols}
%%%%%%%%%%%%%%%%% B.9 - standard toolkit %
\PackageInfo{czt}{\space\space Loading standard toolkit symbols completed}
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Few extra helpful commands %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% users referring to this file in their \LaTeX
\def\cztstylefile {\texttt{czt.sty}}
% macro for block alignment of paragraphs - from (old) zed.sty
\def\zedblock{\@ifnextchar[{\@zedblock}{\@zedblock[t]}}
\def\@zedblock[#1]{\array[#1]{@{}l@{}}}
\let\endzedblock=\endarray
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\endinput
%%
%% End of file `czt.sty'.