From 6814d757e06f69d1b3f413c7f9beb948d06fe3ad Mon Sep 17 00:00:00 2001 From: Karl Berry Date: Sun, 1 Nov 2015 22:13:43 +0000 Subject: prftree (1nov15) git-svn-id: svn://tug.org/texlive/trunk@38757 c570f23f-e606-0410-a88d-b1316a301751 --- Master/texmf-dist/tex/latex/prftree/prftree.sty | 184 ++++++++++++++---------- 1 file changed, 106 insertions(+), 78 deletions(-) (limited to 'Master/texmf-dist/tex/latex') 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 % ------------------------------------------------------------------- -- cgit v1.2.3