Newer
Older
\NeedsTeXFormat{LaTeX2e}[1999/12/01]
\ProvidesPackage{pftools}
}{%
\RequirePackage{\basedir locallabel}
}%
\RequirePackage{Tabbing} % Avoid the standard tabbing environment. Its \< conflicts with the semantic package.
\RequirePackage{xparse}
\RequirePackage{xcolor}
%% Biimplication inference rules
% \biimp above below
% The double lines obtained by the simpler
% "\mprset{fraction={===}}" overlap the conclusion (e.g., the
% mask E_M in an atomic triple).
\newcommand*{\biimp}[2]{%
\hbox{%
\ooalign{%
$\genfrac{}{}{1.6pt}1{#1}{#2}$\cr%
$\color{white}\genfrac{}{}{0.8pt}1{\phantom{#1}}{\phantom{#2}}$%
}%
}%
}
\newcommand{\BIIMP}{\mprset{myfraction=\biimp}}
%% inferH is infer with hyperlinked names.
% \savelabel lab text: Arrange for \ref{lab} to print text and to link to the current spot.
\newcommand*{\savelabel}[2]{%
% Think @currentlabel : text ref.
\edef\@currentlabel{#2}% Save text
\phantomsection% Correct hyper reference link
\label{#1}% Print text and store name↦text.
}
% \textlabel label text: Print and label text.
\newcommand*{\textlabel}[2]{{#2}\savelabel{#1}{\detokenize{#2}}} % added \detokenize to make "Löb" title work
% \rulenamestyle visible
\newcommand*{\rulenamestyle}[1]{{\TirNameStyle{#1}}} % From mathpartir.sty.
% \ruleref [discharged] lab
\def\optionaldischarge#1{%
\if\relax\detokenize{#1}\relax\else\ensuremath{^{#1}}\fi}
\newcommand*{\ruleref}[2][]{\textmd{\rulenamestyle{\ref{#2}}}\optionaldischarge{#1}}
\newcommand*{\fakeruleref}[2][]{\rulenamestyle{#2}\optionaldischarge{#1}}
% \rulename label
\newcommand*{\rulename}[1]{\rulenamestyle{\textlabel{#1}{#1}}}
% \inferhref name lab premise conclusion
\newcommand*{\inferhref}[4]{%
\inferrule*[lab=\textlabel{#2}{#1}]{#3}{#4}%
}
% \infernH name premise conclusion, if name a valid label.
\newcommand*{\inferH}[3]{\inferhref{#1}{#1}{#2}{#3}}
\newcommand*{\axiom}[1]{\infer{}{#1}}
\newcommand*{\axiomhref}[3]{\inferhref{#1}{#2}{}{#3}}
\newcommand*{\axiomH}[2]{\inferH{#1}{}{#2}}
\newcommand*{\inferhrefB}[4]{{\BIIMP\inferhref{#1}{#2}{#3}{#4}}}
\newcommand*{\inferB}[3][]{{\BIIMP\infer[#1]{#2}{#3}}}
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
\newcommand*{\inferHB}[3]{{\BIIMP\inferH{#1}{#2}{#3}}}
\newcommand*{\taghref}[2]{\label{#2}\tag{\rulenamestyle{#1}}}
\newcommand*{\tagH}[1]{\taghref{#1}{#1}}
% The sanity checks in \lbind and \llabel
% don't work properly in amsmath environments
% which perhaps lay out their contents more
% than once. Use \lbind in such cases.
% Sigh.
\newcommand*{\tagL}[1]{\lbind{#1}\tag*{\llabel{#1}}}
\newcommand*\ind[1][\quad]{#1\TAB=\TAB+}
\newcommand*\unind{\TAB-}
\newcommand\IND[1][\quad]{\\*\ind[#1]}
\newcommand\UNIND{\unind \\}
% Attribution: http://tex.stackexchange.com/questions/119473/tabbing-and-line-wrapping
\newlength\pf@width
\newcommand*{\CMT}[1]{%
\setlength\pf@width{\linewidth}%
\addtolength\pf@width{\@totalleftmargin}%
\addtolength\pf@width{-\dimen\@curtab}%
\parbox[t]{\pf@width}{\nobelowdisplayskip{#1}\ifhmode\strut\fi}}
\colorlet{rescolor}{rgb:red,0;green,30;blue,55}
\colorlet{ctxcolor}{black}
\colorlet{codecolor}{rgb:red,76;green,177;blue,36}
\newcommand*\res[1]{{\color{rescolor}\ensuremath{#1}}}
%When \left\{ … \right\} looks ugly, remember Dave says you want \bracket.
\NewDocumentCommand{\RES}{s m O{}}{%
$\displaystyle{{\left\{\res{%
\IfBooleanTF{#1}{\begin{inbox}[l]#2\end{inbox}}{#2}%
}\right\}}_{#3}}$}
\NewDocumentCommand{\ARES}{m O{}}{%
${\displaystyle{\bracket\langle\rangle{\color{rescolor}{#1}}}_{#2}}$}
\newcommand*{\CODE}[1]{%
${\displaystyle{\color{codecolor}#1}}$}
\newcommand*{\VARS}[1]{%
Vars: ${\color{ctxcolor}\displaystyle{#1}}$}
\newcommand*{\CTX}[1]{%
Context: ${\color{ctxcolor}\displaystyle{#1}}$}
\newcommand*{\GOAL}[1]{%
Goal: ${\displaystyle{#1}}$}
\newcommand*{\SUFF}[1]{%
Suff: ${\displaystyle{#1}}$}
\newcommand*{\PFHAVE}[1]{%
Have: ${\displaystyle{#1}}$}
\let\pf@origqedhere\qedhere
\def\pf@setup{%
% A version of \qedhere that accounts for tabbing.
\def\qedhere{\TAB`\pf@origqedhere}%
}
\newcommand*{\TAGL}[1]{\TAB`\llabel{#1}}
% The starred version lacks leading and trailing vertical space.
\newenvironment{proofoutline*}
{\partopsep=\z@skip \topsep=\z@skip% avoid initial space
\parskip\z@skip% avoid trailing space
\pf@setup\par\begingroup\Tabbing\ignorespaces}
{\endTabbing\endgroup\unskip\ignorespacesafterend}
\newenvironment{proofoutline}
{\pf@setup\par\begingroup\Tabbing\ignorespaces}
{\endTabbing\endgroup\ignorespacesafterend}
\endinput