Advertisement
Guest User

Untitled

a guest
Nov 12th, 2018
114
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
Latex 3.89 KB | None | 0 0
  1. % $Id: fitch.sty,v 1.6 2003/06/28 16:53:00 johanw Exp $
  2.  
  3. % Macros for Fitch-style formal proofs
  4. % Johan W. Klüwer, June 10, 2001
  5.  
  6.  
  7. \RequirePackage{mdwtab,latexsym,amsmath,amsfonts,ifthen}
  8.  
  9.  
  10. % Line height in proofs
  11. \newlength{\fitchlineht}
  12. \setlength{\fitchlineht}{1.5\baselineskip}
  13. % Horizontal indent between proof levels
  14. \newlength{\fitchindent}
  15. \setlength{\fitchindent}{1em}
  16. % Indent to comment
  17. \newlength{\fitchcomind}
  18. \setlength{\fitchcomind}{2em}
  19. % Line number width
  20. \newlength{\fitchnumwd}
  21. \setlength{\fitchnumwd}{1em}
  22.  
  23. % Altered from mdwtab.sty: shorter vline, for start of subproof
  24. \makeatletter
  25. \newcommand\fvline[1][\arrayrulewidth]{\vrule\@height.5\fitchlineht\@width#1\relax}
  26. \makeatother
  27. % Ordinary vertical line
  28. \newcommand{\fa}{\vline\hspace*{\fitchindent}}
  29. % Vertical line, shorter: Use at start of (sub)proof
  30. \newcommand{\fb}{\fvline\hspace*{\fitchindent}}
  31. % Hypothesis
  32. \newcommand{\fh}{\fvline%
  33.   \makebox[0pt][l]{{%
  34.       \raisebox{-1.4ex}[0pt][0pt]{\rule{1.5em}{\arrayrulewidth}}}}%
  35.   \hspace*{\fitchindent}}
  36. % Hypothesis, with longer vert line: for >1 hypothesis
  37. \newcommand{\fj}{\vline%
  38.   \makebox[0pt][l]{{%
  39.       \raisebox{-1.4ex}[0pt][0pt]{\rule{1.5em}{\arrayrulewidth}}}}%
  40.   \hspace*{\fitchindent}}
  41. % Modal subproof: takes argument = operator
  42. \newcommand{\fitchmodal}[1]{%
  43.   \makebox[0pt][r]{${}^{#1}$\,}\fvline\hspace*{\fitchindent}}
  44. \newcommand{\fn}{\fitchmodal{\Box}}% Box subproof
  45. \newcommand{\fp}{\fitchmodal{\Diamond}}% Diamond subproof
  46. % Modal subproof with hypothesis in first line (as in Fitch)
  47. \newcommand{\fitchmodalh}[1]{%
  48.   \makebox[0pt][r]{${}^{#1}$\,}%
  49.   \fvline%
  50.   \makebox[0pt][l]{{%
  51.       \raisebox{-1.4ex}[0pt][0pt]{\rule{1.5em}{\arrayrulewidth}}}}%
  52.   \hspace*{\fitchindent}}
  53. % Rule: formula introduction marker. \fr with line, \fs without line
  54. \newcommand{\fr}{%
  55.   \makebox[0pt][r]{${\rhd}$\,\,}\vline\hspace*{\fitchindent}}
  56. \newcommand{\fs}{%
  57.   \makebox[0pt][r]{${\rhd}$\,\,}}
  58. % Box around argument, like new variable in ql
  59. \newcommand{\fw}[1]{\fbox{\footnotesize $#1$}}
  60.  
  61. %
  62. \newcounter{fitchcounter}
  63. \setcounter{fitchcounter}{0}
  64. %To avoid starting from 1, \setboolean{resetfitchcounter}{false}
  65. \newboolean{resetfitchcounter}
  66. \setboolean{resetfitchcounter}{true}
  67. %To avoid increasing numbers, \setboolean{increasefitchcounter}{false}
  68. \newboolean{increasefitchcounter}
  69. \setboolean{increasefitchcounter}{true}
  70. %\formatfitchcounter can be altered if need be, though only once per proof
  71. \newcommand{\formatfitchcounter}[1]{\arabic{#1}}
  72. %Typeset the counter
  73. \newcommand{\fitchcounter}{%
  74.   \ifthenelse{\boolean{increasefitchcounter}}{\addtocounter{fitchcounter}{1}}{}
  75.  \formatfitchcounter{fitchcounter}}
  76.  
  77. %A line with a special number -- a tag, e.g. \ftag{\vdots}{}
  78. \newcommand{\ftag}[2]{\multicolumn{1}%
  79.   {!{\makebox[\fitchnumwd][r]{#1}\hspace{\fitchindent}}Ml@{\hspace{\fitchcomind}}}%
  80.   {#2}}
  81.  
  82. \newenvironment{fitchnum}%
  83. {\ifthenelse{\boolean{resetfitchcounter}}{\setcounter{fitchcounter}{0}}{}
  84.  \begin{tabular}{!{\makebox[\fitchnumwd][r]{\fitchcounter }\hspace{\fitchindent}}Ml@{\hspace{\fitchcomind}}l}}%
  85. {\end{tabular}}
  86.  
  87. \newenvironment{fitchunum}%
  88. {\begin{tabular}{!{\makebox[\fitchnumwd][r]{}\hspace{\fitchindent}}Ml@{\hspace{\fitchcomind}}l}}%
  89. {\end{tabular}}
  90.  
  91. \newenvironment{fitch}{\renewcommand{\arraystretch}{1.5}
  92.  \begin{fitchnum}}{\end{fitchnum}}
  93. \newenvironment{fitch*}{\renewcommand{\arraystretch}{1.5}
  94.  \begin{fitchunum}}{\end{fitchunum}}
  95.  
  96. % The following is useful for giving a numbered formula, then the proof.
  97. \newenvironment{flem}[2]%
  98. {\begin{eqnarray}
  99.    &#1\label{#2}\\
  100.    &\begin{fitch}}%
  101.     {\end{fitch}\notag\end{eqnarray}}
  102.  
  103. %To write comment field for two consecutive lines, with brace
  104. \newcommand{\ftwocom}[1]{%
  105.   \parbox[t]{3cm}{
  106.    \raisebox{-.6\baselineskip}[\baselineskip][0pt]{%
  107.       $\left.
  108.        \begin{aligned}
  109.          \,\\ \,
  110.        \end{aligned}
  111.      \right\}$\quad #1}
  112.  }}
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement