Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- % $Id: fitch.sty,v 1.6 2003/06/28 16:53:00 johanw Exp $
- % Macros for Fitch-style formal proofs
- % Johan W. Klüwer, June 10, 2001
- \RequirePackage{mdwtab,latexsym,amsmath,amsfonts,ifthen}
- % Line height in proofs
- \newlength{\fitchlineht}
- \setlength{\fitchlineht}{1.5\baselineskip}
- % Horizontal indent between proof levels
- \newlength{\fitchindent}
- \setlength{\fitchindent}{1em}
- % Indent to comment
- \newlength{\fitchcomind}
- \setlength{\fitchcomind}{2em}
- % Line number width
- \newlength{\fitchnumwd}
- \setlength{\fitchnumwd}{1em}
- % Altered from mdwtab.sty: shorter vline, for start of subproof
- \makeatletter
- \newcommand\fvline[1][\arrayrulewidth]{\vrule\@height.5\fitchlineht\@width#1\relax}
- \makeatother
- % Ordinary vertical line
- \newcommand{\fa}{\vline\hspace*{\fitchindent}}
- % Vertical line, shorter: Use at start of (sub)proof
- \newcommand{\fb}{\fvline\hspace*{\fitchindent}}
- % Hypothesis
- \newcommand{\fh}{\fvline%
- \makebox[0pt][l]{{%
- \raisebox{-1.4ex}[0pt][0pt]{\rule{1.5em}{\arrayrulewidth}}}}%
- \hspace*{\fitchindent}}
- % Hypothesis, with longer vert line: for >1 hypothesis
- \newcommand{\fj}{\vline%
- \makebox[0pt][l]{{%
- \raisebox{-1.4ex}[0pt][0pt]{\rule{1.5em}{\arrayrulewidth}}}}%
- \hspace*{\fitchindent}}
- % Modal subproof: takes argument = operator
- \newcommand{\fitchmodal}[1]{%
- \makebox[0pt][r]{${}^{#1}$\,}\fvline\hspace*{\fitchindent}}
- \newcommand{\fn}{\fitchmodal{\Box}}% Box subproof
- \newcommand{\fp}{\fitchmodal{\Diamond}}% Diamond subproof
- % Modal subproof with hypothesis in first line (as in Fitch)
- \newcommand{\fitchmodalh}[1]{%
- \makebox[0pt][r]{${}^{#1}$\,}%
- \fvline%
- \makebox[0pt][l]{{%
- \raisebox{-1.4ex}[0pt][0pt]{\rule{1.5em}{\arrayrulewidth}}}}%
- \hspace*{\fitchindent}}
- % Rule: formula introduction marker. \fr with line, \fs without line
- \newcommand{\fr}{%
- \makebox[0pt][r]{${\rhd}$\,\,}\vline\hspace*{\fitchindent}}
- \newcommand{\fs}{%
- \makebox[0pt][r]{${\rhd}$\,\,}}
- % Box around argument, like new variable in ql
- \newcommand{\fw}[1]{\fbox{\footnotesize $#1$}}
- %
- \newcounter{fitchcounter}
- \setcounter{fitchcounter}{0}
- %To avoid starting from 1, \setboolean{resetfitchcounter}{false}
- \newboolean{resetfitchcounter}
- \setboolean{resetfitchcounter}{true}
- %To avoid increasing numbers, \setboolean{increasefitchcounter}{false}
- \newboolean{increasefitchcounter}
- \setboolean{increasefitchcounter}{true}
- %\formatfitchcounter can be altered if need be, though only once per proof
- \newcommand{\formatfitchcounter}[1]{\arabic{#1}}
- %Typeset the counter
- \newcommand{\fitchcounter}{%
- \ifthenelse{\boolean{increasefitchcounter}}{\addtocounter{fitchcounter}{1}}{}
- \formatfitchcounter{fitchcounter}}
- %A line with a special number -- a tag, e.g. \ftag{\vdots}{}
- \newcommand{\ftag}[2]{\multicolumn{1}%
- {!{\makebox[\fitchnumwd][r]{#1}\hspace{\fitchindent}}Ml@{\hspace{\fitchcomind}}}%
- {#2}}
- \newenvironment{fitchnum}%
- {\ifthenelse{\boolean{resetfitchcounter}}{\setcounter{fitchcounter}{0}}{}
- \begin{tabular}{!{\makebox[\fitchnumwd][r]{\fitchcounter }\hspace{\fitchindent}}Ml@{\hspace{\fitchcomind}}l}}%
- {\end{tabular}}
- \newenvironment{fitchunum}%
- {\begin{tabular}{!{\makebox[\fitchnumwd][r]{}\hspace{\fitchindent}}Ml@{\hspace{\fitchcomind}}l}}%
- {\end{tabular}}
- \newenvironment{fitch}{\renewcommand{\arraystretch}{1.5}
- \begin{fitchnum}}{\end{fitchnum}}
- \newenvironment{fitch*}{\renewcommand{\arraystretch}{1.5}
- \begin{fitchunum}}{\end{fitchunum}}
- % The following is useful for giving a numbered formula, then the proof.
- \newenvironment{flem}[2]%
- {\begin{eqnarray}
- \label{#2}\\
- &\begin{fitch}}%
- {\end{fitch}\notag\end{eqnarray}}
- %To write comment field for two consecutive lines, with brace
- \newcommand{\ftwocom}[1]{%
- \parbox[t]{3cm}{
- \raisebox{-.6\baselineskip}[\baselineskip][0pt]{%
- $\left.
- \begin{aligned}
- \,\\ \,
- \end{aligned}
- \right\}$\quad #1}
- }}
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement