%
% logic.sty by Carlos H. C. Duarte
%
% To be used in texts dealing with logics. Some ideas used here were
% inspired by the VDM style created by M.Wolczko. Some others were 
% based on a style written by Leslie Lamport
%
\typeout{Document Style Option 'logic' -- Released 17 May 1995.}

\input{math.sty}
\input{interp.sty}
\edef\restoreenv{\noexpand\catcode\lq\noexpand\@=\the\catcode\lq\@}
\catcode\lq\@=11 
\def\@beginHorizontal{\@restoreLineSeparator
  \@restoreMargins\@raggedRight\noindent$\strut\relax}
\def\@endHorizontal{\relax\strut$}
\def\@restoreLineSeparator{\let\\=\newline}
\def\@restoreMargins{\advance\hsize by-\leftskip
  \advance\hsize by-\rightskip
\def\@raggedRight{\rightskip=0pt plus 1fil
  \hyphenpenalty=-100 \linepenalty=200
  \binoppenalty=10000 \relpenalty=10000 \pretolerance=-1}
  \leftskip=0pt \rightskip=0pt}
\def\@endIndentedPara#1{\strut#1\egroup\hss\egroup}
\def\@beginMathIndentedPara#1#2{\@beginIndentedPara{#1}{#2}%
	{\@beginHorizontal}}
\def\@endMathIndentedPara{\@endIndentedPara{\@endHorizontal}}
\def\@belowAndIndent#1#2{#1\hfil\break
	\@beginMathIndentedPara{\hsize}{\qquad}#2\@endMathIndentedPara}
\def\@mathIndentedPara#1#2#3{\@beginMathIndentedPara{#1}{#2}#3%
	\@endMathIndentedPara}
\def\@beginIndentedPara#1#2#3{\hbox to #1\bgroup \setbox0=\kw{#2}%
        \copy0 \strut \vtop\bgroup \advance\hsize by -\wd0 #3}
\def\@endIndentedPara#1{\strut#1\egroup\hss\egroup}
\ifx\fmtname\@fmtname
        \def\keywordFontBeginSequence{\small\sf}%
\else\ifx\fmtname\@psfmtname
        \def\keywordFontBeginSequence{\sf}%
\else
        \def\keywordFontBeginSequence{\bf}%
\fi\fi
\def\kw#1{\hbox{\keywordFontBeginSequence #1\/}}
\def\generic{\,\rule{0.05ex}{0.6ex}\rule{0.7em}{0.05ex}\rule{0.05ex}{0.6ex}\,}
\let\Iff=\Leftrightarrow
\let\iff=\Iff
\let\Implies=\Rightarrow
\let\implies=\Implies
\let\Or=\vee
\let\And=\land
\let\and=\And
\def\Not{\neg\,}
\mathchardef\Exists="0239
\mathchardef\Forall="0238
\mathchardef\suchthat="2201
\def\exists{\@ifstar{\@splitExists}{\@normalExists}}
\def\@nexists{\hbox to 0pt{\raise0.15ex\hbox{/}\hss}\Exists}
\def\nexists{\@ifstar{\@splitNExists}{\@normalNExists}}
\def\EXISTS{\@ifstar{\@splitEXISTS}{\@normalEXISTS}}
\def\forall{\@ifstar{\@splitForall}{\@normalForall}}
\def\FORALL{\@ifstar{\@splitFORALL}{\@normalFORALL}}
\def\unique{\@ifstar{\@splitUnique}{\@normalUnique}}
\def\uniqueval{\@ifstar{\@splitUniqueval}{\@normalUniqueval}}
\def\abstraction{\@ifstar{\@splitAbstraction}{\@normalAbstraction}}
\def\@normalExists#1#2{{\Exists#1}\suchthat #2}
\def\@normalNExists#1#2{{\@nexists#1}\suchthat #2}
\def\@normalEXISTS#1#2#3{{\Exists_{#1}\,#2}\suchthat #3}
\def\@normalForall#1#2{{\Forall#1}\suchthat #2}
\def\@normalFORALL#1#2#3{{\Forall_{#1}\,#2}\suchthat #3}
\def\@normalUnique#1#2{{\Exists!\,#1}\suchthat #2}
\def\@normalUniqueval#1#2{{\iota\,#1}\suchthat #2}
\def\@normalAbstraction#1#2{{\lambda\,#1}\suchthat #2}
\def\@splitExists#1{\@belowAndIndent{\Exists#1\suchthat}}
\def\@splitNExists#1{\@belowAndIndent{\@nexists#1\suchthat}}
\def\@splitEXISTS#1#2{\@belowAndIndent{\Exists_{#1}\,#2\suchthat}}
\def\@splitForall#1{\@belowAndIndent{\Forall#1\suchthat}}
\def\@splitFORALL#1#2{\@belowAndIndent{\Forall_{#1}\,#2\suchthat}}
\def\@splitUnique#1{\@belowAndIndent{\Exists!\,#1\suchthat}}
\def\@splitUniqueval#1{\@belowAndIndent{\iota\,#1\suchthat}}
\def\@splitAbstraction#1{\@belowAndIndent{\lambda\,#1\suchthat}}

\let\Tstlp=\vdash
\def\sequent{\@ifstar{\@splitSequent}{\@normalSequent}}
\def\@normalSequent#1#2{{#1}\:\Tstlp\: #2}
\def\@splitSequent#1{\@belowAndIndent{#1\;\Tstlp}}
\def\lsequent{\@ifstar{\@splitLsequent}{\@normalLsequent}}
\def\@normalLsequent#1#2#3{{#1}\:\Tstlp_{#2}\: #3}
\def\@splitLsequent#1#2{\@belowAndIndent{#1\;\Tstlp_{#2}}}
\def\lvee#1#2#3{\bigvee_{#1}^{#2}#3}
\def\lwedge#1#2#3{\bigwedge_{#1}^{#2}#3}
\def\ldiamond#1{\Diamond#1}
\def\lsubst{\@ifstar{\@splitLsubst}{\@normalLsubst}}
\def\@normalLsubst#1#2#3{#1[#2/#3]}
\def\@splitLsubst#1{\@belowAndIndent{#1}}
\def\lbox#1{\Box#1}

\def\lang#1{{\cal L}(#1)}
\def\sort#1{{\sf{#1}}}
\def\const#1{\mbox{\scaledown{\uppercase{{\rm #1}}}}}
\def\false{\hbox{\const{false}\/}}
\def\true{\hbox{\const{true}\/}}
\def\action#1{{\sl #1}}
\def\Next{{\bf X}}
\def\next#1{\Next #1}
\def\Prev{{\bf Y}}
\def\prev#1{\Prev #1}
\def\Hasbeen{{\bf H}}
\def\hasbeen#1{\Hasbeen #1}
\def\Past{{\bf P}}
\def\past#1{\Past #1}
\def\Always{{\bf G}}
\def\always#1{\Always #1}
\def\Until{{\bf U}}
\def\until#1#2{#1 \Until #2}
\def\While{{\bf W}}
\def\while#1#2{#1 \While #2}
\def\Future{{\bf F}}
\def\future#1{\Future #1}
\def\Since{{\bf S}}
\def\since#1#2{#1 \Since #2}
\def\Kampu{{\bf V}}
\def\kampu#1#2{#1 \Kampu #2}
\def\Kamps{{\bf Z}}
\def\kamps#1#2{#1 \Kamps #2}
\def\Some{{\bf E}}
\def\some#1{\Some #1}
\def\Any{{\bf A}}
\def\any#1{\Any #1}
\def\after#1#2{\left[#1\relax\right]\hspace*{-1ex}\begin{array}[t]{l}#2\relax\end{array}\hspace*{-1ex}}
\def\per#1{{\tt Per}\left(#1\right)}
\def\obl#1{{\tt Obl}(#1)}
\def\lolly{-\!\circ}
\def\Vdash{\mathbin{\hbox{$\rule{0.05ex}{1.6ex}\!\vdash$}}}
\def\Vvdash{\mathbin{\hbox{$\rule{0.05ex}{1.6ex}\rule{0.1ex}{1.6ex}\!\vdash$}}}
\def\Alpha{{\cal A}}
\def\df{\raisebox{0.7ex}{\(\scriptstyle\underline{\triangle}\)}}
\def\beg{{\bf beg}}
\def\hoare#1#2#3{\set{#1}#2\set{#3}}
\newsavebox{\bigquantbox}
\newsavebox{\bigquantsbox}
\newlength{\bigquantlength}
\newlength{\bigquantslength}
\def\@@bigquant[#1]#2#3{\@bigquant{#1}{#2}{#3}}
\def\bigquant{\@ifnextchar [{\@@bigquant}{\@bigquant{t}}}
\def\@bigquant#1#2#3{\renewcommand{\arraystretch}{0.7}
                  \savebox{\bigquantbox}{${\textstyle #2\;\;\:}$}
                  \settowidth{\bigquantlength}{\usebox{\bigquantbox}}
                  \savebox{\bigquantsbox}{
                  $\begin{array}[#1]{@{}l@{}} \usebox{\bigquantbox} \\ #3
                  \end{array}$}
                  \settowidth{\bigquantslength}{\usebox{\bigquantsbox}}
                  \usebox{\bigquantsbox}
                  \hspace*{-\bigquantslength}\hspace*{\bigquantlength}}
\def\subs#1{{\scriptstyle #1}\\}
\def\sep{\ |\ }

% Available type sizes:
% \tiny \scriptsize \footnotesize \small \normalsize 
% \large \Large \LARGE \huge \Huge
\newlength{\cfsize}
\newlength{\tmpsize}
\def\scaledown#1{\settoheight{\cfsize}{1ex}%
\settoheight{\tmpsize}{{\normalsize 1ex}}%
\ifdim\cfsize=\tmpsize{\small#1}%
\else%
\settoheight{\tmpsize}{{\small 1ex}}%
\ifdim\cfsize=\tmpsize{\footnotesize#1}%
\else%
\settoheight{\tmpsize}{{\footnotesize 1ex}}%
\ifdim\cfsize=\tmpsize{\scriptsize#1}%
\else%
\settoheight{\tmpsize}{{\scriptsize 1ex}}%
\ifdim\cfsize=\tmpsize{\tiny#1}%
\else%
\settoheight{\tmpsize}{{\Huge 1ex}}%
\ifdim\cfsize=\tmpsize{\huge#1}%
\else%
\settoheight{\tmpsize}{{\huge 1ex}}%
\ifdim\cfsize=\tmpsize{\LARGE#1}%
\else%
\settoheight{\tmpsize}{{\LARGE 1ex}}%
\ifdim\cfsize=\tmpsize{\Large#1}%
\else%
\settoheight{\tmpsize}{{\Large 1ex}}%
\ifdim\cfsize=\tmpsize{\large#1}%
\else%
\settoheight{\tmpsize}{{\large 1ex}}%
\ifdim\cfsize=\tmpsize{\normalsize#1}%
\else%
{\bf undefined}%
\fi\fi\fi\fi\fi\fi\fi\fi\fi}

% The following definitions, through \begin{derivation} \assert \justify
% \continue \comment and \end{derivation} allow us to present Hilbert style 
% derivations or proofs. 
% The optional argument of assert is to define a label for the 
% assertion, which can be referred to afterwards.
% The optional argument of both derivation and proof are to define the
% last step number in a previous use of the environment, presumably 
% containing the previous part of the same real derivation which is 
% to be continuated.
\def\Proof{{\sf Proof:\ }}
\def\Proofsketch{{\sf Proof (sketch):\ }}
\newcounter{asser}
\newif\if@firststep
\newdimen\myparskip
\newdimen\mytopsep
\def\@derivation[#1]{\myparskip=\parskip\parskip=0pt
                       \mytopsep=\topsep\topsep=0pt
                       \setcounter{asser}{#1}\stepcounter{asser}\@firststeptrue
                       \begin{tabbing}}
\def\derivation{\@ifnextchar [{\@derivation}{\@derivation[0]}}
\def\@proof[#1]{\myparskip=\parskip\parskip=0pt
                \mytopsep=\topsep\topsep=0pt
                \setcounter{asser}{#1}\stepcounter{asser}\@firststeptrue
                \begin{tabbing}\Proof\\}
\def\proof{\@ifnextchar [{\@proof}{\@proof[0]}}
\@namedef{derivation*}{\let\labelinit\labelinits\myparskip=\parskip\parskip=0pt
                       \mytopsep=\topsep\topsep=0pt
                       \@firststeptrue\begin{tabbing}}
\@namedef{endderivation*}{\end{tabbing}
                          \parskip=\myparskip
                          \topsep=\mytopsep}
\def\endderivation{\end{tabbing}
                   \parskip=\myparskip
                   \topsep=\mytopsep}
\let\endproof=\endderivation
\def\comment#1{\if@firststep\ \ \ \ \=\else\>\fi #1\@firststepfalse \\}
\def\justify#1{\` \scaledown{#1}\stepcounter{asser}\@firststepfalse \\}
\def\labelinit{\theasser.\if@firststep\ \ \=\else\>\fi}
\def\labelinits{\if@firststep\=\else\>\fi}
\def\begass{\let\@currentlabel\theasser}
\def\endass{}
\def\@@assert[#1]#2{\begass\label{#1}\@assert{#2}\endass}
\def\@assert#1{\labelinit $#1$}
\def\assert{\@ifnextchar [{\@@assert}{\@assert}}
\def\@@continue[#1]#2{\> $#2$ \` \scaledown{#1} \\}
\def\@continue#1{\> $#1$ \\}
\def\continue{\@ifnextchar [{\@@continue}{\@continue}}
% \def\continue#1{\> $#1$ \\}
\def\hstretch{\hspace*{\stretch{1}}}
\def\Qed{\rule{1.5ex}{0.75em}}
\def\qed{\hstretch\Qed}
\def\qedbox#1{\hstretch\mbox{\Qed\ {#1}}}
\def\Defend{\fbox{\rule{0ex}{0.15em}\rule{0.3ex}{0em}}}
\def\defend{\hstretch\Defend}
\restoreenv
\endinput