summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/tex/latex/prftree
diff options
context:
space:
mode:
authorKarl Berry <karl@freefriends.org>2015-11-01 22:13:43 +0000
committerKarl Berry <karl@freefriends.org>2015-11-01 22:13:43 +0000
commit6814d757e06f69d1b3f413c7f9beb948d06fe3ad (patch)
tree03c0466434dede16efed8b84f44afc3f06213b1d /Master/texmf-dist/tex/latex/prftree
parent11f117cbfd9a90cad1d5813ccb66d0fc4c0616c6 (diff)
prftree (1nov15)
git-svn-id: svn://tug.org/texlive/trunk@38757 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Master/texmf-dist/tex/latex/prftree')
-rw-r--r--Master/texmf-dist/tex/latex/prftree/prftree.sty184
1 files changed, 106 insertions, 78 deletions
diff --git a/Master/texmf-dist/tex/latex/prftree/prftree.sty b/Master/texmf-dist/tex/latex/prftree/prftree.sty
index 8396b7b9cf5..2bec5c8f07a 100644
--- a/Master/texmf-dist/tex/latex/prftree/prftree.sty
+++ b/Master/texmf-dist/tex/latex/prftree/prftree.sty
@@ -1,6 +1,7 @@
%
% prftree.sty
-% by Marco Benini - 30th November 2014
+% by Marco Benini - 31st October 2015
+% v1.2
%
% A package to typeset natural deduction proofs, or sequent proofs, or
% tableau proofs
@@ -9,16 +10,16 @@
%
\NeedsTeXFormat{LaTeX2e}
-\ProvidesPackage{prftree}[2014/11/30 Natural Deduction Proofs]
+\ProvidesPackage{prftree}[2015/10/31 Natural Deduction Proofs]
-% Package options
+% Package options: deactivated by default
\newif\ifprf@NDOption\prf@NDOptionfalse
\newif\ifprf@SEQOption\prf@SEQOptionfalse
\newif\ifprfIMPOption\prfIMPOptionfalse
\DeclareOption{ND}{\prf@NDOptiontrue}
\DeclareOption{SEQ}{\prf@SEQOptiontrue}
-\DeclareOption{IMP}{\prf@IMPOptiontrue}
+\DeclareOption{IMP}{\prfIMPOptiontrue}
\ProcessOptions\relax
%--------------------------------------------------------------------
@@ -272,7 +273,7 @@
\def\prf@@top\prf@cons#1#2\prf@eos{#1}
\def\prf@top{\expandafter\prf@@top\prf@stack}
-%% Pop discard the topmost value in the stack
+%% Pop discards the topmost value in the stack
\def\prf@@pop\prf@cons#1#2\prf@eos{%
\expandafter\edef\expandafter\prf@stack{#2\prf@eos}}
\def\prf@pop{\expandafter\prf@@pop\prf@stack}
@@ -340,10 +341,10 @@
\expandafter\ifx\csname prf@w@ref@#1\endcsname\relax}
% Write a reference
-\def\prfref<#1>{%
- \ifprf@undefref<#1>{??}%
- \PackageWarningNoLine{prooftree}{Undefined reference <#1>}%
- \else\csname prf@ref@@#1\endcsname\relax\fi}
+\protected\def\prfref<#1>{%
+ \ifprf@undefref<#1>\relax\mbox{??}%
+ \PackageWarningNoLine{prftree}{Undefined reference <#1>}\relax%
+ \else\csname prf@ref@@#1\endcsname\relax\fi\relax}
% Create the anchor from what stored in the .aux file
\def\prfauxlabel#1#2{%
@@ -409,9 +410,9 @@
% How a labelled assumption is graphically rendered
\def\prflabelledassumptionbox#1#2{%
\setbox\prf@fancybox\hbox{${#1}$}%
- \prf@tmp\wd\prf@fancybox%
+ % \prf@tmp\wd\prf@fancybox% CHANGED FROM v1.0
\setbox\prf@fancybox\hbox{$\box\prf@fancybox^{#2}$}%
- \wd\prf@fancybox\prf@tmp%
+ % \wd\prf@fancybox\prf@tmp% CHANGED FROM v1.0
\prf@assumption{\box\prf@fancybox}}
% How a discharged fancy labelled assumption is graphically rendered
@@ -526,29 +527,29 @@
\def\prf@@summarystyle{%
\ifnum3=\prfsummarystyle\relax%
\setbox\prf@summarybox\hbox{$\mathcal{D}$}%
- \prf@tmp\wd\prf@summarybox%
+ %\prf@tmp\wd\prf@summarybox%
\setbox\prf@summarybox\hbox{$\mathcal{D}%
\hbox{\box\prf@summary@label}\mathstrut$}%
- \wd\prf@summarybox\prf@tmp%
+ %\wd\prf@summarybox\prf@tmp%
\else\ifnum2=\prfsummarystyle\relax%
\setbox\prf@summarybox\hbox{$\prod$}%
- \prf@tmp\wd\prf@summarybox%
+ %\prf@tmp\wd\prf@summarybox%
\setbox\prf@summarybox\hbox{$\prod\hbox{\box\prf@summary@label}$}%
- \wd\prf@summarybox\prf@tmp%
+ %\wd\prf@summarybox\prf@tmp%
\else\ifnum1=\prfsummarystyle\relax%
\setbox\prf@summarybox\hbox{\hbox{\Huge$\Pi$}}%
- \prf@tmp\wd\prf@summarybox%
+ %\prf@tmp\wd\prf@summarybox%
\setbox\prf@summarybox\hbox{\hbox{\Huge$\Pi$}%
\hbox{\box\prf@summary@label}}%
- \wd\prf@summarybox\prf@tmp%
+ %\wd\prf@summarybox\prf@tmp%
\else\ifnum0=\prfsummarystyle\relax%
\setbox\prf@summarybox\hbox{$\cdot$}%
- \prf@tmp\wd\prf@summarybox%
+ %\prf@tmp\wd\prf@summarybox%
\setbox\prf@summarybox%
\vbox to5.2ex{\cleaders\hbox{$\cdot$}\vfill}%
\setbox\prf@summarybox\hbox{\usebox{\prf@summarybox}%
\hbox{\ \box\prf@summary@label}}%
- \wd\prf@summarybox\prf@tmp%
+ %\wd\prf@summarybox\prf@tmp%
\else\setbox\prf@summarybox\hbox{\prffancysummarybox}\fi\fi\fi\fi%
\prf@tmp.5\ht\prf@summarybox%
\advance\prf@tmp-.5\dp\prf@summarybox%
@@ -935,9 +936,9 @@
\advance\prf@temp.5\dp\prf@fancybox\fi\fi%
\setbox\prf@conclusionbox%
\vbox{\vskip\prf@temp\box\prf@conclusionbox}%
- % And, finally, at the very end, we can prepare the proof box and we
- % can calculate the right value from Rassum. At the very end, we can
- % output the result (!!)
+ % And, finally, we can prepare the proof box and we can calculate
+ % the right value from Rassum. At the very end, we can output the
+ % result (!!)
\setbox\prf@rulenamebox%
\vbox{\box\prf@assumptionsbox\nointerlineskip%
\box\prf@linebox\nointerlineskip%
@@ -960,51 +961,68 @@
% Package option [ND]
% -------------------------------------------------------------------
-\newbox\prf@charbox
-\def\prfscript#1{\setbox\prf@charbox%
- \hbox{$\scriptstyle\mathrm{#1}$}\copy\prf@charbox}
\ifprf@NDOption%
\def\NDA{\prfassumption}
\def\NDD{\prfboundedassumption}
\def\NDAL#1{\prfassumption<#1>}
\def\NDDL#1{\prfboundedassumption<#1>}
\def\NDP{\prftree}
- \def\NDANDI{\prftree[by]{$\scriptstyle\wedge\prfscript{I}$}}
- \def\NDANDER{\prftree[by]{%
- $\scriptstyle\wedge\prfscript{E}_{\prfscript{R}}$}}
- \def\NDANDEL{\prftree[by]{%
- $\scriptstyle\wedge\prfscript{E}_{\prfscript{L}}$}}
- \def\NDANDE{\prftree[by]{$\scriptstyle\wedge\prfscript{E}$}}
+ \def\NDANDI{\prftree[by]{$\scriptstyle\mathord{\wedge}%
+ \noexpand\textup{I}$}}
+ \def\NDANDEL{\prftree[by]{$\scriptstyle\mathord{\wedge}%
+ \noexpand\textup{E}_1$}}
+ \def\NDANDER{\prftree[by]{$\scriptstyle\mathord{\wedge}%
+ \noexpand\textup{E}_2$}}
+ \def\NDANDE{\prftree[by]{$\scriptstyle\mathord{\wedge}%
+ \noexpand\textup{E}$}}
+ \def\NDORIL{\prftree[by]{$\scriptstyle\mathord{\vee}%
+ \noexpand\textup{I}_1$}}
+ \def\NDORIR{\prftree[by]{$\scriptstyle\mathord{\vee}%
+ \noexpand\textup{I}_2$}}
+ \def\NDORI{\prftree[by]{$\scriptstyle\mathord{\vee}%
+ \noexpand\textup{I}$}}
+ \def\NDORE{\prftree[by]{$\scriptstyle\mathord{\vee}%
+ \noexpand\textup{E}$}}
+ \def\NDOREL#1{\prftree[by]{$\scriptstyle{\vee}%
+ {\noexpand\textup{E}}^{\noexpand\prfref<#1>}$}}
\ifprfIMPOption
- \def\NDIMPI{\prftree[by]{$\scriptstyle\supset\prfscript{I}$}}
- \def\NDIMPE{\prftree[by]{$\scriptstyle\supset\prfscript{E}$}}
- \def\NDIMPIL#1{\prftree[by]{$\scriptstyle\supset%
- \prfscript{I}_{\prfref<#1>}$}}
+ \def\NDIMPI{\prftree[by]{$\scriptstyle\mathord{\supset}%
+ \noexpand\textup{I}$}}
+ \def\NDIMPE{\prftree[by]{$\scriptstyle\mathord{\supset}%
+ \noexpand\textup{E}$}}
+ \def\NDIMPIL#1{\prftree[by]{$\scriptstyle\mathord{\supset}%
+ \noexpand\textup{I}^{\noexpand\prfref<#1>}$}}
\else
- \def\NDIMPI{\prftree[by]{$\scriptstyle\rightarrow%
- \prfscript{I}$}}
- \def\NDIMPE{\prftree[by]{$\scriptstyle\rightarrow%
- \prfscript{E}$}}
+ \def\NDIMPI{\prftree[by]{$\scriptstyle\mathord{\rightarrow}%
+ \noexpand\textup{I}$}}
+ \def\NDIMPE{\prftree[by]{$\scriptstyle\mathord{\rightarrow}%
+ \noexpand\textup{E}$}}
\def\NDIMPIL#1{%
- \prftree[by]{$\scriptstyle\rightarrow%
- \prfscript{I}_{\prfref<#1>}$}}\fi
- \def\NDORIR{\prftree[by]{$\scriptstyle\vee%
- \prfscript{I}_{\prfscript{R}}$}}
- \def\NDORIL{\prftree[by]{$\scriptstyle\vee%
- \prfscript{I}_{\prfscript{L}}$}}
- \def\NDORI{\prftree[by]{$\scriptstyle\vee\prfscript{I}$}}
- \def\NDORE{\prftree[by]{$\scriptstyle\vee\prfscript{E}$}}
- \def\NDOREL#1{\prftree[by]{$\scriptstyle\vee%
- \prfscript{I}_{\prfref<#1>}$}}
- \def\NDALLI{\prftree[by]{$\scriptstyle\forall\prfscript{I}$}}
- \def\NDALLE{\prftree[by]{$\scriptstyle\forall\prfscript{E}$}}
- \def\NDEXI{\prftree[by]{$\scriptstyle\exists\prfscript{I}$}}
- \def\NDEXE{\prftree[by]{$\scriptstyle\exists\prfscript{E}$}}
+ \prftree[by]{$\scriptstyle\mathord{\rightarrow}%
+ \noexpand\textup{I}^{\noexpand\prfref<#1>}$}}\fi
+ \def\NDNOTI{\prftree[by]{$\scriptstyle\mathord{\neg}%
+ \noexpand\textup{I}$}}
+ \def\NDNOTIL#1{\prftree[by]{$\scriptstyle{\neg}%
+ \noexpand\textup{I}^{\noexpand\prfref<#1>}$}}
+ \def\NDNOTE{\prftree[by]{$\scriptstyle\mathord{\neg}%
+ \noexpand\textup{E}$}}
+ \def\NDALLI{\prftree[by]{$\scriptstyle\mathord{\forall}%
+ \noexpand\textup{I}$}}
+ \def\NDALLE{\prftree[by]{$\scriptstyle\mathord{\forall}%
+ \noexpand\textup{E}$}}
+ \def\NDEXI{\prftree[by]{$\scriptstyle\mathord{\exists}%
+ \noexpand\textup{I}$}}
+ \def\NDEXE{\prftree[by]{$\scriptstyle\mathord{\exists}%
+ \noexpand\textup{E}$}}
\def\NDEXEL#1{%
- \prftree[by]{$\scriptstyle\exists\prfscript{E}_{\prfref<#1>}$}}
- \def\NDTI{\prftree[by]{$\scriptstyle\top\prfscript{I}$}}
- \def\NDFE{\prftree[by]{$\scriptstyle\bot\prfscript{E}$}}
- \def\NDLEM{\prftree[by]{$\scriptstyle\prfscript{lem}$}}
+ \prftree[by]{$\scriptstyle\mathord{\exists}%
+ \noexpand\textup{E}^{\noexpand\prfref<#1>}$}}
+ \def\NDTI{\prftree[by]{$\scriptstyle\mathord{\top}%
+ \noexpand\textup{I}$}}
+ \def\NDFE{\prftree[by]{$\scriptstyle\mathord{\bot}%
+ \noexpand\textup{E}$}}
+ \def\NDLEM{\prftree[by]{$\scriptstyle\noexpand\textup{lem}$}}
+ \def\NDAX{\prftree[by]{$\scriptstyle\noexpand\textup{ax}$}}
\fi
% -------------------------------------------------------------------
@@ -1017,30 +1035,40 @@
\def\SEQA{\prfassumption}
\def\SEQD{\prfboundedassumption}
\def\SEQP{\prftree}
- \def\SEQAX{\prftree[by]{$\scriptstyle\prfscript{Ax}$}}
- \def\SEQLF{\prftree[by]{$\scriptstyle\prfscript{L}\bot$}}
- \def\SEQLW{\prftree[by]{$\scriptstyle\prfscript{LW}$}}
- \def\SEQRW{\prftree[by]{$\scriptstyle\prfscript{RW}$}}
- \def\SEQLC{\prftree[by]{$\scriptstyle\prfscript{LC}$}}
- \def\SEQRC{\prftree[by]{$\scriptstyle\prfscript{RC}$}}
- \def\SEQLAND{\prftree[by]{$\scriptstyle\prfscript{L}\wedge$}}
- \def\SEQRAND{\prftree[by]{$\scriptstyle\prfscript{R}\wedge$}}
- \def\SEQLOR{\prftree[by]{$\scriptstyle\prfscript{L}\vee$}}
- \def\SEQROR{\prftree[by]{$\scriptstyle\prfscript{R}\vee$}}
+ \def\SEQAX{\prftree[by]{$\scriptstyle\noexpand\textup{Ax}$}}
+ \def\SEQLF{\prftree[by]{$\scriptstyle\noexpand\textup{L}\bot$}}
+ \def\SEQLW{\prftree[by]{$\scriptstyle\noexpand\textup{LW}$}}
+ \def\SEQRW{\prftree[by]{$\scriptstyle\noexpand\textup{RW}$}}
+ \def\SEQLC{\prftree[by]{$\scriptstyle\noexpand\textup{LC}$}}
+ \def\SEQRC{\prftree[by]{$\scriptstyle\noexpand\textup{RC}$}}
+ \def\SEQLAND{\prftree[by]{$\scriptstyle\noexpand\textup{L}%
+ \mathord{\wedge}$}}
+ \def\SEQRAND{\prftree[by]{$\scriptstyle\noexpand\textup{R}%
+ \mathord{\wedge}$}}
+ \def\SEQLOR{\prftree[by]{$\scriptstyle\noexpand\textup{L}%
+ \mathord{\vee}$}}
+ \def\SEQROR{\prftree[by]{$\scriptstyle\noexpand\textup{R}%
+ \mathord{\vee}$}}
\ifprfIMPOption
- \def\SEQLIMP{\prftree[by]{$\scriptstyle\prfscript{L}\supset$}}
- \def\SEQRIMP{\prftree[by]{$\scriptstyle\prfscript{R}\supset$}}
+ \def\SEQLIMP{\prftree[by]{$\scriptstyle\noexpand\textup{L}%
+ \mathord{\supset}$}}
+ \def\SEQRIMP{\prftree[by]{$\scriptstyle\noexpand\textup{R}%
+ \mathord{\supset}$}}
\else
- \def\SEQLIMP{\prftree[by]{$\scriptstyle\prfscript{L}%
- \rightarrow$}}
- \def\SEQRIMP{\prftree[by]{$\scriptstyle\prfscript{R}%
- \rightarrow$}}
+ \def\SEQLIMP{\prftree[by]{$\scriptstyle\noexpand\textup{L}%
+ \mathord{\rightarrow}$}}
+ \def\SEQRIMP{\prftree[by]{$\scriptstyle\noexpand\textup{R}%
+ \mathord{\rightarrow}$}}
\fi
- \def\SEQLALL{\prftree[by]{$\scriptstyle\prfscript{L}\forall$}}
- \def\SEQRALL{\prftree[by]{$\scriptstyle\prfscript{R}\forall$}}
- \def\SEQLEX{\prftree[by]{$\scriptstyle\prfscript{L}\exists$}}
- \def\SEQREX{\prftree[by]{$\scriptstyle\prfscript{R}\exists$}}
- \def\SEQCUT{\prftree[by]{$\scriptstyle\prfscript{Cut}$}}
+ \def\SEQLALL{\prftree[by]{$\scriptstyle\noexpand\textup{L}%
+ \mathord{\forall}$}}
+ \def\SEQRALL{\prftree[by]{$\scriptstyle\noexpand\textup{R}%
+ \mathord{\forall}$}}
+ \def\SEQLEX{\prftree[by]{$\scriptstyle\noexpand\textup{L}%
+ \mathord{\exists}$}}
+ \def\SEQREX{\prftree[by]{$\scriptstyle\noexpand\textup{R}%
+ \mathord{\exists}$}}
+ \def\SEQCUT{\prftree[by]{$\scriptstyle\noexpand\textup{Cut}$}}
\fi
% -------------------------------------------------------------------