% macros.tex
% A Constructive Analysis of Realizability Semantics for Constructive Logic
% Kurtz, Mitchell, & O'Donnell
%
% Copyright 1989 Stuart Kurtz, John Mitchell, Michael O'Donnell
% All Rights Reserved
%
% $Log: macros.tex,v $
% Revision 1.5  1994/05/10  05:31:19  odonnell
% *** empty log message ***
%
% Revision 1.4  1994/05/07  01:01:22  odonnell
% *** empty log message ***
%
% Revision 1.3  1994/05/06  04:31:07  odonnell
% Version to send to Jim Lipton.
%
% Revision 1.2  1994/05/05  18:13:25  odonnell
% *** empty log message ***
%
% Revision 1.1  1994/05/05  18:11:33  odonnell
% Initial revision
%
% Revision 1.10  1993/12/20  03:32:27  odonnell
% *** empty log message ***
%
% Revision 1.9  1993/12/18  23:42:26  odonnell
% *** empty log message ***
%
% Revision 1.8  1993/12/18  06:51:03  odonnell
% *** empty log message ***
%
% Revision 1.7  1993/12/18  01:11:26  odonnell
% *** empty log message ***
%
% Revision 1.6  1993/09/23  17:53:50  odonnell
% *** empty log message ***
%
% Revision 1.1  1993/08/20  15:25:23  odonnell
% Initial revision
%
% Revision 1.1  1993/04/16  16:01:28  odonnell
% Initial revision
%
% Revision 1.1  91/10/08  13:22:35  odonnell
% Initial revision
% 
% Revision 1.1  89/07/12  13:33:03  stuart
% Initial revision
% 

% Permit a tiny bit of sloppiness in the formatting:

\hfuzz=2pt

% TeX is too willing to break inline formulae, esp. at \proves ...

\relpenalty=10000
\binoppenalty=10000

% Theorem-like environments

\newtheorem{theorem}{Theorem}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{definition}{Definition}
\newtheorem{indefinition}[theorem]{Informal Definition}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{remark}[theorem]{Remark}

% Set theorem-like entities in italic.

\let\thmfont=\it

% special symbols

\renewcommand{\iff}{\Leftrightarrow}

\newcommand{\union}{\cup}
\newcommand{\inter}{\cap}
\newcommand{\product}[2]{\prod_{#1}{#2}}
\newcommand{\summ}[2]{\sum_{#1}{#2}}
\newcommand{\proves}{\vdash}
\newcommand{\false}{\bot}
\newcommand{\true}{\top}
\newcommand{\defeq}{\stackrel{\rm def}{=}}
\newcommand{\order}{\hbox{\rm order}}
\newcommand{\invar}{\mathord{\Downarrow}}
\newcommand{\inhab}{\Uparrow}
\newcommand{\init}[1]{#1^\bot}
\newcommand{\now}[1]{#1^{\mathord{+}}}
\newcommand{\term}[1]{#1^\top}
\newcommand{\modal}[2]{#1^{#2}}
\newcommand{\lessmod}{\unlhd}
\newcommand{\delnow}[1]{#1^{\mathord{-}}}
\newcommand{\switch}{\mathord{\mbox{\it switch}}}
\newcommand{\Cov}{\mathord{\mbox{\it Cov}}}

\newcommand{\STUB}[1]{
   \begin{center}
     {\bf **STUB** **STUB** **STUB** **STUB** **STUB** }\\
     #1 \typeout{STUB: #1}\\
     {\bf **STUB** **STUB** **STUB** **STUB** **STUB** }
   \end{center}
}

\newcounter{temp}

% commands for manipulating sequents and tableaux:

\newcommand{\labelf}[2]{(#1):\;#2}
\newcommand{\limplies}{\Rightarrow}
\newcommand{\derive}[2]{\begin{array}{c}#1\\
  \hline\noalign{\vskip 1pt}#2\end{array}}
\newcommand{\psep}{\mkern 20mu}
\newcommand{\rmbox}[1]{\hbox{\rm #1}}

% sets.

\newcommand{\paren}[1]{\left(#1\right)}
\newcommand{\intersect}{\cap}
\newcommand{\appu}[1]{\mathord{\mbox{\fractur A}}_{#1}}
\newcommand{\appel}[2]{\mathord{\mbox{\fractur A}}^{#1}_{#2}}

% semantics.

\newcommand{\sval}[1]{[\![#1]\!]}

\newcommand{\tuple}[1]{\langle #1\rangle}
\newcommand{\sepdot}{\mkern 4mu . \mkern 4mu}

\newcommand{\lambdamodels}{\models_{\lambda}}
\newcommand{\ljoin}[1]{\mathord{\oplus_{#1}}}
\newcommand{\dljoin}[1]{\mathord{\dot{\oplus}_{#1}}}

\newcommand{\bethproves}{\proves_{\rm I}}

\newcommand{\stab}[2]{{\rm stab}_{#2}({#1})}
\newcommand{\realize}[3]{{\rm real}^{#3}_{#2}({#1})}
\newcommand{\theory}{{\rm Theory}}

% We need a nonprinting proof symbol for the euclidean style proofs of
% section 2.

\newcommand{\fprove}{\phantom{\proves\hbox{}}}

% We never use : in mathmode for a relation, only for punctuation

\mathcode`\:="603A

% objects of various types

\newfont{\fractur}{eufb10 scaled \magstephalf}

% models and semantics

\newcommand{\model}[1]{\mathord{\mbox{\fractur #1}}}
\newcommand{\world}[1]{\mathord{\mbox{\fractur #1}}}
\newcommand{\nmodels}{\models_{n}}
\newcommand{\kmodels}{\models_{\cal K}}
\newcommand{\kclmodels}
   {\models_{\mathord{\mbox{{\scriptsize\em Cl\/}}},\cal K}}
\newcommand{\kcomodels}
   {\models_{\mathord{\mbox{{\scriptsize\em Co\/}}},\cal K}}
\newcommand{\kvmodels}{\models_{\mathord{\mbox{{\scriptsize\em C?\/}}},\cal K}}

%From Kurtz.old ----------------------------------------------------------

\newcounter{caseno}

\newcommand{\newcases}{\setcounter{caseno}{0}}

\newenvironment{case}{
  \refstepcounter{caseno}
  \begin{trivlist}
   \item[]{\sc Case~\arabic{caseno}:}\hspace{.5 em}\it
}{\end{trivlist}}

\newcommand{\eop}[1]{
  \begin{flushright}
    {\bf #1\hspace{1em}}$\Box$
  \end{flushright}
}

\newcommand{\forward}{$(\Longrightarrow)$}
\newcommand{\backward}{$(\Longleftarrow)$}

\newcommand{\Proof}{\paragraph{Proof:}}

% logical symbols

\newcommand{\lequiv}{\Leftrightarrow}
\newcommand{\limplied}{\Leftarrow}

\newcommand{\rmodels}{\models_{\rm R}}
\newcommand{\lmodels}{\models_{\cal L}}
\newcommand{\lclmodels}
   {\models_{\mathord{\mbox{{\scriptsize\em Cl\/}}},\cal L}}
\newcommand{\lcomodels}
   {\models_{\mathord{\mbox{{\scriptsize\em Co\/}}},\cal L}}
\newcommand{\lvmodels}{\models_{\mathord{\mbox{{\scriptsize\em C?\/}}},\cal L}}
\newcommand{\cmodels}{\models_{\rm C}}

\newcommand{\sstab}[2]{\mbox{\bf set-stab}_{#2}(#1)}
\newcommand{\seqs}{\mathord{\mbox{\bf seq}}}
\newcommand{\seqleft}{\mathord{\mbox{\it left}}}
\newcommand{\seqright}{\mathord{\mbox{\it right}}}

% HACK!

\def\joinrel{\mathrel{\mkern-4mu}}      % replace latex's joinrel

% set theoretic operators

\newcommand{\Union}{\bigcup}
\newcommand{\Intersect}{\bigcap}
\newcommand{\set}[1]{\{#1\}}
\newcommand{\setof}[2]{\{#1\sep#2\}}
\newcommand{\sep}{\,|\;}
\newcommand{\choice}{\mathord{\mbox{\bf choose}}}

% objects in special fonts.

\newcommand{\labels}{\cal L}
\newcommand{\assignment}[1]{#1}
\newcommand{\assumptions}[1]{{\cal #1}}
\newcommand{\class}[1]{{\bf #1}}
\newcommand{\collection}[1]{\hbox{$\cal #1$}}
\newcommand{\contradiction}[1]{\proofnotation{\omega}_{\formula{#1}}}
\newcommand{\evidence}[1]{{#1}}
\newcommand{\realizers}[1]{{{#1}^{~}}}
\newcommand{\noise}[1]{{\cal #1}}
\newcommand{\fassumptions}[2]{\assumptions{#1}_{\formula{#2}}}
\newcommand{\formulae}[1]{#1}
\newcommand{\formula}[1]{#1}
\newcommand{\fproof}[1]{#1}
\newcommand{\group}[1]{#1}
\newcommand{\lmap}[1]{#1}
\newcommand{\lpermutation}[2]{\permutation{#1}_{\scriptscriptstyle #2}}
\newcommand{\sname}[1]{#1}
\newcommand{\permutation}[1]{#1}
\newcommand{\prooffunc}[1]{{\cal #1}}
\newcommand{\proofobj}[2]{{\prooffunc{#1}}_{\valuation{#2}}}
\newcommand{\proofnotation}[1]{#1}
\newcommand{\relation}[1]{{\mathrel{{[}#1{]}}}}
\newcommand{\rstruct}[1]{{\bf #1}}      % realizability structure
\newcommand{\universe}[1]{{\cal #1}}
\newcommand{\valuation}[1]{{\it #1}}
\newcommand{\pseudoproof}[1]{{\sf #1}}
\newcommand{\assign}[3]{[#1\mathbin{\hbox{:=}}#2]\valuation{#3}}
\newcommand{\flip}{{\sf flip}}
\newcommand{\identityp}{\varepsilon}
\newcommand{\subst}[3]{#3[#1/#2]}

\newcommand{\AS}{\mathord{\mbox{\sf AS}}} % assumptions used in natural proof
\newcommand{\AT}{\mathord{\mbox{\sf AT}}} % atomic terms
\newcommand{\Var}{\mathord{\mbox{\sf V}}} % variables
\newcommand{\Pred}[1]{\mathord{\mbox{\sf P}^{#1}}} % #1-ary predicate symbols
\newcommand{\PF}{\mathord{\mbox{\sf PF}}_1} % positive predicate formulae
\newcommand{\PPF}{\mathord{\mbox{\sf PF}}_0} % positive propositional formulae
\newcommand{\EF}{\mathord{\mbox{\sf EF}}} % extended formulae
\newcommand{\TH}{\mathord{\mbox{\sf TH}}} % theory
\newcommand{\kTH}{\TH_{\cal K}}         % kripke theory
\newcommand{\lambdaTH}{\TH_\lambda}
\newcommand{\lTH}{\TH_{\cal L}}
\newcommand{\MO}{\hbox{\sf MO}}         % a collection of models
\newcommand{\lambdaMO}{\MO_\lambda}
\newcommand{\kMO}{\MO_{\cal K}}         % kripke models of a theory
\newcommand{\lMO}{\MO_{\cal L}}
\newcommand{\PR}{\hbox{\sf PR}}         % provability
\newcommand{\LK}{\hbox{\sf LK}}
\newcommand{\LKs}{\hbox{${\sf LK_s}$}}
\newcommand{\Ind}{I} % class of individuals
\newcommand{\witfunc}{\varsigma_0}
\newcommand{\lambor}{\sqcup}

% HACK

\newcommand{\Bbb}[1]{{\bf #1}}