diff options
Diffstat (limited to '')
| -rw-r--r-- | latex-fitch/source/fitch.sty | 112 |
1 files changed, 112 insertions, 0 deletions
diff --git a/latex-fitch/source/fitch.sty b/latex-fitch/source/fitch.sty new file mode 100644 index 0000000..963010e --- /dev/null +++ b/latex-fitch/source/fitch.sty @@ -0,0 +1,112 @@ +% $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} + }} |