From 9c0b575a4064ef065936c234111aa1e7a6f77c38 Mon Sep 17 00:00:00 2001 From: Karl Berry Date: Wed, 11 Jan 2006 23:53:22 +0000 Subject: trunk/Master/texmf-dist/source/latex/flagderiv git-svn-id: svn://tug.org/texlive/trunk@286 c570f23f-e606-0410-a88d-b1316a301751 --- .../source/latex/flagderiv/flagderiv.dtx | 1261 ++++++++++++++++++++ .../source/latex/flagderiv/flagderiv.ins | 63 + 2 files changed, 1324 insertions(+) create mode 100644 Master/texmf-dist/source/latex/flagderiv/flagderiv.dtx create mode 100644 Master/texmf-dist/source/latex/flagderiv/flagderiv.ins (limited to 'Master/texmf-dist/source') diff --git a/Master/texmf-dist/source/latex/flagderiv/flagderiv.dtx b/Master/texmf-dist/source/latex/flagderiv/flagderiv.dtx new file mode 100644 index 00000000000..c9025c73e2e --- /dev/null +++ b/Master/texmf-dist/source/latex/flagderiv/flagderiv.dtx @@ -0,0 +1,1261 @@ +% \iffalse meta-comment +% +% Copyright (C) 2005 by Paul van Tilburg +% ------------------------------------------------------ +% +% This package is free software; you can redistribute it and/or modify +% it under the terms of the GNU General Public License as published by +% the Free Software Foundation; either version 2 of the License, or +% (at your option) any later version. +% +% This package is distributed in the hope that it will be useful, +% but WITHOUT ANY WARRANTY; without even the implied warranty of +% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +% GNU General Public License for more details. +% +% You should have received a copy of the GNU General Public License +% along with this package; if not, write to the Free Software +% Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.% +% +% \fi +% +% \iffalse +%<*driver> +\ProvidesFile{flagderiv.dtx} +% +%\NeedsTeXFormat{LaTeX2e}[1999/12/01] +%\ProvidesPackage{flagderiv} +%<*flagderiv> + [2005/08/26 v0.10 Flag style derivation package] +% +% +%<*driver> +\documentclass{ltxdoc} + +\usepackage{amsmath, amssymb} +\usepackage{calc} +\usepackage{flagderiv} +\usepackage{fvrb-ex} +\usepackage{theorem} +\usepackage{url} + +\setlength{\parindent}{0pt} +\setlength{\parskip}{\medskipamount} +\setcounter{tocdepth}{2} + +\theoremstyle{plain} +\newtheorem{lemma}{Lemma} +\newcommand{\false}{\textit{False}} +\newcommand{\flags}{\texttt{flagderiv}} +\newcommand{\IHbase}{\underline{\textit{Base}}:~} +\newcommand{\IHhyp}{\underline{\textit{Induction-hypothesis}}:~} +\newcommand{\IHstep}{\underline{\textit{Step}}:~} +\newcommand{\Nat}{\ensuremath{\mathbb{N}}} +\newcommand{\All}{\ensuremath{\mathbb{Z}}} +\newcommand{\Powerset}{\ensuremath{\mathcal{P}}} + +\renewcommand{\implies}{\Rightarrow} +\newcommand{\biimplies}{\Leftrightarrow} +\newcommand{\OHA}{\rightarrow} +\newcommand{\THA}{\twoheadrightarrow} +\newcommand{\NHA}[1]{\stackrel{#1}{\rightarrow}} +\newcommand{\CRtext}{\ensuremath{\mathit{CR}}} +\newcommand{\CR}{\ensuremath{(\forall a, b, c\in A: a\THA b\land a\THA c:% + (\exists d\in A:: b\THA d\land c\THA d))}} +\newcommand{\MCtext}{\ensuremath{\mathit{mixed~confluent}}} +\newcommand{\MC}{\ensuremath{(\forall a, b, c\in A: a\OHA b\land a\THA c:% + (\exists d\in A:: b\THA d\land c\THA d))}} + +\EnableCrossrefs +\CodelineIndex +\RecordChanges + +\begin{document} + \DocInput{flagderiv.dtx} +\end{document} +% +% \fi +% +% \CheckSum{0} +% +% \CharacterTable +% {Upper-case \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z +% Lower-case \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z +% Digits \0\1\2\3\4\5\6\7\8\9 +% Exclamation \! Double quote \" Hash (number) \# +% Dollar \$ Percent \% Ampersand \& +% Acute accent \' Left paren \( Right paren \) +% Asterisk \* Plus \+ Comma \, +% Minus \- Point \. Solidus \/ +% Colon \: Semicolon \; Less than \< +% Equals \= Greater than \> Question mark \? +% Commercial at \@ Left bracket \[ Backslash \\ +% Right bracket \] Circumflex \^ Underscore \_ +% Grave accent \` Left brace \{ Vertical bar \| +% Right brace \} Tilde \~} +% +% +% \changes{v0.9f}{2005/02/04}{Initial version.} +% \changes{v0.9g}{2005/05/16}{Added example and usage documentation.} +% \changes{v0.9h}{2005/06/06}{Added the flagderiv* environment.} +% \changes{v0.9i}{2005/06/10}{Fixed minor issues in the documentation +% and resolved a ref-format bug.} +% \changes{v0.10}{2005/08/26}{Drop dependancy on farray, include fix.} +% +% \GetFileInfo{flagderiv.dtx} +% +% \DoNotIndex{\newcommand,\newenvironment} +% +% \title{The \textsf{flagderiv} package\thanks{This document +% corresponds to \textsf{flagderiv}~\fileversion, dated \filedate.}} +% \author{Paul van Tilburg \\ \url{paul@luon.net}} +% +% \maketitle +% +% \tableofcontents +% +% \section{Introduction} +% +% This document describes how to use \flags~to make flag-style proofs in +% \LaTeX. +% +% It can handle taking steps, making assumptions, introducing variables and +% conclusions. The package allows the style to be configured. For +% example, the variable introduction symbol can be redefined. Other +% features include multiple page flag-style proofs. +% +% The documentation and all examples are based upon version \fileversion\ +% of \flags. +% +% \begin{center} +% \scriptsize +% \renewcommand{\introsymb}{\text{Let}} +% \begin{flagderiv} +% \assume{i:assume:no-package}{\text{There is no nice package to do flag-style proofs}}{} +% \introduce{i:intro:feature}{x\text{, such that } x\text{ is a flag-style feature}}{} +% \skipsteps{5}{\vdots}{} +% \step{i:feature-met}{\flags~\text{can do it}}{} +% \conclude{i:conclusion}{\flags~\text{fulfils my every flag-style proof need}} +% {$\forall$-introduction on \ref{i:intro:feature} and \ref{i:feature-met}} +% \step{i:false}{\false}{\false-introduction on \ref{i:assume:no-package} and \ref{i:conclusion}} +% \conclude{i:conclude:not-no-package}{\lnot (\text{There is no nice package to do flag-style proofs})} +% {$\lnot$-introduction on \ref{i:assume:no-package} and \ref{i:false}} +% \step{i:step:nice-package}{\text{So, there exists a nice package to do flag-style proofs}} +% {$\lnot\lnot$-elimination on \ref{i:conclude:not-no-package}} +% \end{flagderiv} +% \end{center} +% +% \section{Acknowledgements} +% +% I want to thank Jan Zwanenburg and Erik Poll for the first versions of +% this package, professor R.P.\ Nederpelt for his ever-persisting package +% reviews, feedback and suggestions and last but not least Mark van Eijk, +% who has written parts of section~\ref{sec:usage} and all examples in +% section~\ref{sec:ex}. +% +% \section{Usage\label{sec:usage}} +% +% This section explains how the \flags\ package works by means of examples +% and how the commands should be used. I try to cover all possibilities and +% features of this package. For bigger examples, please refer to +% section~\ref{sec:ex}; for more detailed documentation on the commands +% and inner workings, refer to the \flags\ package itself. +% +% \subsection{Basic derivations} +% \DescribeEnv{flagderiv} +% Basic derivations are written using an intuitive command sequence +% placed in the |flagderiv| environment\index{usage}. The example below +% uses auto-numbering of the lines. Variable introductions, assumptions, +% steps and conclusions can be done using the following commands +% respectively: +% +% \begin{itemize} +% \item \DescribeMacro{\introduce}\index{usage} +% |\introduce|\marg{label}\marg{formula}\marg{comment}, +% \item \DescribeMacro{\assume}\index{usage} +% |\assume|\marg{label}\marg{formula}\marg{comment}, +% \item \DescribeMacro{\step}\index{usage} +% |\step|\marg{label}\marg{formula}\marg{comment}, and +% \item \DescribeMacro{\conclude}\index{usage} +% |\conclude|\oarg{number}\marg{label}\marg{formula}\marg{comment}. +% \end{itemize} +% +% Lines can be referred to using the {\em label} that is provided as the +% first argument to each of the commands. {\em Formulas} are placed in +% the second argument and a {\em comment} in the third. +% See subsection~\ref{sec:usage:multi} for the explanation of the optional +% argument {\em number} of |\conclude|. +% +% \begin{Example}[gobble=7,frame=single,label=Auto-numbering] +% \begin{flagderiv} +% \introduce{in-x}{x: \Nat}{Introduction of $x$} +% \assume{as-x}{x > 5}{Assumption} +% \step{big-x}{x > 1}{Arithmetic on \ref{in-x} and \ref{as-x}} +% \conclude{conc}{x > 5 \implies x > 1} +% {$\implies$-intro on \ref{as-x} and \ref{big-x}} +% \conclude{}{\forall x \in \Nat: x > 5 \implies x > 1} +% {$\forall$-intro on \ref{in-x} and \ref{conc}} +% \end{flagderiv} +% \end{Example} +% +% The following example uses manual numbering. This is done by using the +% \DescribeMacro{\introduce*} +% starred versions of the previous given commands (|\introduce*|, +% \DescribeMacro{\assume*} +% \DescribeMacro{\step*} +% \DescribeMacro{\conclude*} +% |\assume*|, |\step*| and |\conclude*|) and using a +% {\em custom number} instead of a {\ em label} as the first argument. +% Note that because of this, derivation line references are not possible +% and should be done manually as well. +% +% \begin{Example}[gobble=7,frame=single,label=Manual numbering] +% \begin{flagderiv} +% \introduce*{$(1)$}{x: \Nat}{Introduction of $x$} +% \assume*{$(2)$}{P(x)}{Assumption} +% \skipsteps*{\dots}{} +% \step*{$(n - 2)$}{Q(x)}{} +% \conclude*{$(n - 1)$}{P(x) \implies Q(x)} +% {$\implies$-intro on $(2)$ and $(n - 2)$} +% \conclude*{$(n)$}{\forall x \in \Nat: P(x) \implies Q(x)} +% {$\forall$-intro on $(1)$ and $(n - 1)$} +% \end{flagderiv} +% \end{Example} +% +% Note that the |\skipsteps*| used in the previous example is +% explained in section~\ref{sec:usage:skipsteps}. +% +% \subsection{Concluding multiple assumptions/introductions\label{sec:usage:multi}} +% Sometimes it is useful to make a conclusion from multiple open +% assumptions and/or introductions at once. This can be done by supplying +% an optional {\em number} to the |\conclude| command. Usage is +% illustrated in the example below. +% +% \begin{Example}[gobble=7,frame=single,label=Multiple conclusion] +% \begin{flagderiv} +% \introduce{}{x: \Nat}{} +% \assume{}{P(x)}{} +% \step{}{Q(x)}{} +% \conclude[2]{}{\forall x \in \Nat: (P(x) \implies Q(x))}{} +% \end{flagderiv} +% \end{Example} +% +% \subsection{Skipping steps\label{sec:usage:skipsteps}} +% When writing example derivations or abbreviating those where +% obvious/trivial steps may be skipped, one can use the +% \DescribeMacro{\skipsteps} +% |\skipsteps|\marg{number}\marg{formula}\marg{comment} command for +% auto-numbered derivations. This commands takes the {\em number} of +% steps to skip as the first argument, a {\em formula} as the second and +% a {\em comment} as the third, like a normal step. +% \vspace{3em} +% +% \begin{Example}[gobble=7,frame=single,label=Skipping 5 steps] +% \begin{flagderiv} +% \assume{as}{P \implies Q}{} +% \step{lem-p}{P \lor \neg P}{LEM} +% \skipsteps{5}{\dots} +% {Prove $\neg P \lor Q$ for $P$ and $\neg P$} +% \step{or-elm}{\neg P \lor Q}{$\lor$-elim on \ref{lem-p}} +% \end{flagderiv} +% \end{Example} +% +% For skipping an unknown number of steps in a manual numbered +% \DescribeMacro{\skipsteps*} +% derivation, the command |\skipsteps*|\marg{formula}\marg{comment} can +% be used. Here the number of steps to skip must be omitted, since there +% is no counting involved. See for example the $\implies$-intro rule: +% +% \begin{Example}[gobble=7,frame=single,label=Skipping steps] +% \begin{flagderiv} +% \assume*{$(1)$}{P}{Assumption} +% \skipsteps*{\dots}{Derive $Q$} +% \step*{$(n - 1)$}{Q}{} +% \conclude*{$(n)$}{P \implies Q} +% {$\implies$-intro on $(1)$ to $(n - 1)$} +% \end{flagderiv} +% \end{Example} +% +% \subsection{Closing assumptions/introductions} +% Assumptions and introductions (contexts) are not always closed by a +% conclusion, it is sometimes useful to keep proven propositions within +% \DescribeMacro{\done} +% its context. The |\done| command (|\done|\oarg{number}) can be used to +% close a assumption and/or introduction without mentioning why. It takes +% an optional argument {\em number} to close multiple open assumptions +% and/or introductions. An example from the WTT (Weak Type Theory): +% +% \begin{Example}[gobble=7,frame=single,label=Closing assumptions/introductions] +% \begin{flagderiv} +% \introduce{}{n: \Nat}{} +% \introduce{}{d: \Nat}{} +% \step{}{\text{$d$ is a divisor of $n$} := +% \exists_{k: \Nat} (n = d \cdot k)}{} +% \done +% \introduce{}{m: \Nat}{} +% \step{}{\text{$m$ is a multiple of $n$} := +% \exists_{k: \Nat} (m = k \cdot n)}{} +% \done[2] +% \end{flagderiv} +% \end{Example} +% +% \vspace{-1em} +% The last |\done[2]| can be omitted since closing the \flags\ environment +% implicitly closes all open introductions and assumptions. +% +% +% \subsection{Spacing between lines} +% The spacing between derivation lines defaults to {\tt 8pt} but can be +% changed +% \DescribeMacro{derivskip}\index{setting} +% by adjusting the length (using |\setlength| on {\tt derivskip}) +% before starting or during a \flags\ environment. See for example the +% more condensed proof: +% +% \begin{Example}[gobble=7,frame=single,label=Condensing a derivation] +% \setlength{\derivskip}{4pt} +% \begin{flagderiv} +% \assume{}{P}{} +% \assume{}{Q}{} +% \step{}{P}{} +% \conclude{}{Q \implies P}{} +% \conclude{}{P \implies Q \implies P}{} +% \end{flagderiv} +% \end{Example} +% +% Note that flag derivations will automatically be split across pages if +% it is too long and the |flagderiv| environment is used. See also the +% {\tt longtable} package. This does not happen for |flagderiv*|, which +% is a normal |tabular|. +% +% \subsection{The introduction symbol} +% \DescribeMacro{\introsymb}\index{changing} +% The way an introduction flag differs from an assumption flag is that it +% is prefixed with an {\em introduction symbol}. This symbol is by +% default set to $\mathbf{var}$ (|\mathbf{var}|) but can be changed +% to a different symbol, for example to $\leadsto$ (|\leadsto|) or +% just `Let'. This can be changed by redefining the |\introsymb| +% command before opening the \flags\ environment. +% +% \begin{Example}[gobble=7,frame=single,label=Changing the introduction symbol] +% \renewcommand{\introsymb}{\textbf{Let}} +% \begin{flagderiv} +% \introduce{intro-x}{x: \Nat}{Introduction} +% \introduce{intro-y}{y: \Nat}{Introduction} +% \skipsteps*{\ddots}{} +% \end{flagderiv} +% \end{Example} +% +% \subsection{Numbering and format} +% When the derivation lines are automatically numbered the numbers are +% formatted as ``({\em number})'' and so are the references. This format +% \DescribeMacro{fd@stepcount} +% \DescribeMacro{\thestepcount}\index{changing} +% can be changed by overriding the |\thestepcount| command using the +% {\tt fd@stepcount} counter before opening the \flags\ environment. +% +% \begin{Example}[gobble=7,frame=single,label=Changing the numbering format] +% \renewcommand{\thestepcount}{[\Roman{fd@stepcount}]} +% \begin{flagderiv} +% \step{ass}{P \implies Q}{} +% \step{lem}{P \lor \neg P}{LEM} +% \assume{ass-nP}{\neg P}{Assumption} +% \step{s0}{\neg P \lor \neg Q}{$\lor$-intro on \ref{ass-nP}} +% \done +% \assume{ass-nnP}{P}{Assumption} +% \step{s1}{Q}{$\implies$-elim on \ref{ass-nnP} and \ref{ass}} +% \step{s2}{\neg P \lor \neg Q}{$\lor$-intro on \ref{s1}} +% \done +% \step{or-el}{\neg P \lor Q} +% {$\lor$-elim on \ref{lem}, \ref{s0} and \ref{s2}} +% \end{flagderiv} +% \end{Example} +% +% \DescribeMacro{\thesteplabel}\index{changing} +% Since the manual numbered derivations use no counter, the format can be +% changed by overriding the |\thesteplabel| command which will take +% one argument, the {\em custom number}. +% +% \begin{Example}[gobble=7,frame=single,label=Changing the numbering format] +% \renewcommand{\thesteplabel}[1]{#1.} +% \begin{flagderiv} +% \assume*{1}{P}{Assumption} +% \skipsteps*{\dots}{Derive $Q$} +% \step*{n - 1}{Q}{} +% \conclude*{n}{P \implies Q}{$\implies$-intro on 1 to n - 1} +% \end{flagderiv} +% \end{Example} +% +% Note that since references are also manually done, the same format +% should be used there by the writer him/herself. +% +% \subsection{Inline comments} +% In general there are two ways to place the comments with respect to +% the formulas in derivations. The first is behind the formula (the +% default). The second way is to place them inline, that is, on a separate +% line before the formula. +% +% All \flags\ environments can be set globally to display the comments +% inline by passing the global option {\tt inlcmnts} to the \flags\ +% package (e.g.\\|\usepackage[inlcmnts]{flagsderiv}|). +% +% \DescribeMacro{\inlcmnts}\index{usage} +% Giving the |\inlcmnts| command makes the environments after this +% command explicitly switch into inline-comment-mode (the default or +% \DescribeMacro{\noinlcmnts}\index{usage} +% global option is forgotten) after which giving |\noinlcmnts| will set +% it back to normal mode. +% +% \begin{Example}[gobble=7,frame=single,label=Inline comments] +% \inlcmnts +% \begin{flagderiv} +% \assume{as-P}{P}{Assume:} +% \assume{as-Q}{Q}{Assume:} +% \step{re-P}{P}{Rei \ref{as-P}:} +% \conclude{imp1}{Q \implies P} +% {$\implies$-intro on \ref{as-Q} and \ref{re-P}:} +% \conclude{imp2}{P \implies Q \implies P} +% {$\implies$-intro on \ref{as-P} and \ref{imp1}:} +% \end{flagderiv} +% \end{Example} +% +% When the comments are inserted inline, a certain format is used, namely +% to enclose the comment with braces. This is the default, but can be +% \DescribeMacro{\theinlcmnt} +% overridden by redefining the |\theinlcmnt| command.\index{override} +% \vspace{1em} +% +% \begin{Example}[gobble=7,frame=single,label=Changing inline comments format] +% \inlcmnts +% \renewcommand{\theinlcmnt}[1]{--#1--} +% \begin{flagderiv} +% \assume{ass-P}{P}{Assumption} +% \assume{ass-Q}{Q}{Assumption} +% \step{rei-P}{P}{Rei \ref{ass-P}} +% \end{flagderiv} +% \end{Example} +% +% \subsection{Namespaces for labels} +% In a document with a lot of auto-numbered derivations it is easy to lose +% overview of labels already used or it may be hard to keep thinking of +% new ones. To solve this a \flags\ environment can take a {\em namespace} +% as optional argument\index{namespacing}. This makes the lines referable +% as normal within the same derivation but also globally when the namespace +% and a colon is added outside the derivation. For example a derivation for +% Modus Tollens (MT): +% +% \begin{Example}[gobble=7,frame=single,label=Derivation label namespace] +% \begin{flagderiv}[mt] +% \step{s0}{P \implies Q}{} +% \assume{as-nQ}{\neg Q}{Assumption} +% \assume{as-P}{P}{Assumption} +% \step{s1}{Q}{$\implies$-elim on \ref{s0} and \ref{as-P}} +% \step{s2}{\bot}{$\bot$-intro on \ref{as-nQ} and \ref{s1}} +% \conclude{nP}{\neg P}{$\neg$-intro on \ref{as-P} and \ref{s2}} +% \conclude{nQ-nP}{\neg Q \implies \neg P} +% {$\implies$-intro on \ref{as-nQ} and \ref{nP}} +% \end{flagderiv} +% +% Note that step~\ref{mt:as-P} is not an intuitive step but necessary +% to get $\neg P$ under the assumption $\neg Q$. +% \end{Example} +% +% \subsection{Other options} +% \DescribeMacro{\caption}\index{usage} +% \DescribeMacro{\tablehead}\DescribeMacro{\tablefirsthead} +% A \flags\ environment actually wraps a {\tt longtable}. This means +% that at the start of an environment all {\tt longtable} options are +% available. This means the use of |\caption|, and setting heads +% (|\tablehead| and |\tablefirsthead|) and feet (|\endfoot| +% \DescribeMacro{\endfoot}\DescribeMacro{\endlastfoot} +% and |\endlastfoot|) but also changing the lengths, etc. +% +% \DescribeEnv{flagderiv*} +% Note that this does not hold for the slightly different |flagderiv*| +% environment, which acts exactly the same but is wrapped in a normal +% {\tt tabular} and thus can not be split across pages. +% +% \begin{Example}[gobble=7,frame=single,label=Captioned] +% \inlcmnts +% \begin{flagderiv}[reflex] +% \caption{The reflexivity of $\equiv_n$} \\ +% \introduce*{(1)}{x \in \All}{Assume:} +% \skipsteps*{\dots \\ \dots}{} +% \step*{(n - 1)}{x \equiv_n x}{} +% \conclude*{(n)}{\forall x \in \All: x \equiv_n x} +% {$\forall$-intro on (1) and (n - 1):} +% \end{flagderiv} +% \end{Example} +% +% \DescribeMacro{\\} +% Additional it is possible to add custom newlines (|\\|) in all +% step formulas\footnote{This is not possible in introductions or +% assumptions, but they can often be split into multiple introductions or +% assumptions.} when the formula gets too long as demonstrated in the +% above example. +% +% +% \section{Examples\label{sec:ex}} +% The following are just a few real-life examples of flag-style proofs, +% where \flags\ provides an elegant means to include these proofs in +% \LaTeX-documents. +% +% \subsection{Examples from \flags} +% \subsection*{A derivation with auto-numbering and labels/references} +% \begin{flagderiv} +% \introduce{intro-xy}{x,y \in \mathbb{N}}{Introduction} +% \assume{assum:1}{x > 0}{Assumption} +% \assume{assum:2}{x < y}{Assumption} +% \step{y-pos}{y > 0}{Transitivity on \ref{assum:1} and \ref{assum:2}} +% \step{y3-pos}{y^3 > 0}{Arithmetic on \ref{y-pos}} +% \conclude{imp:1}{x < y \implies y^3 > 0} +% {$\implies$-intro on \ref{assum:2} and \ref{y3-pos}} +% \conclude{imp:2}{x > 0 \implies x < y \implies y^3 > 0} +% {$\implies$-intro on \ref{assum:1} and \ref{imp:1}} +% \conclude{}{\forall x, y \in \Nat: x > 0 \land x < y \implies y^3 > 0} +% {$\forall$-intro on \ref{intro-xy} and \ref{imp:2}} +% \end{flagderiv} +% +% \subsection*{A derivation with manual numbering} +% \begin{flagderiv} +% \assume*{(m)}{\neg P}{} +% \skipsteps{1}{\dots}{} +% \step*{(n - 2)}{False}{} +% \conclude*{(n - 1)}{\neg\neg P} +% {$\implies$-intro on (m) and (n - 2), and Negation} +% \step*{(n)}{P}{Double negation on (n - 1)} +% \end{flagderiv} +% +% +% \subsection{Predicate Calculus} +% \subsubsection*{Idempotence} +% \begin{flagderiv}[pc-idempotence] +% \assume{intro:PP}{P \land P}{} +% \step{and-elim:P}{P}{$\land$-elim on \ref{intro:PP}} +% \conclude{impl-intro:PP-P}{P \land P \implies P} +% {$\implies$-intro on \ref{intro:PP} +% and \ref{and-elim:P}} +% \assume{intro:P}{P}{} +% \step{and-intro:P}{P \land P}{$\land$-intro on \ref{intro:P} +% and \ref{intro:P}} +% \conclude{impl-intro:P-PP}{P \implies P \land P} +% {$\implies$-intro on \ref{intro:P} +% and \ref{and-intro:P}} +% \step{and-intro:result}{(P \land P \implies P) \land +% (P \implies P \land P)} +% {$\land$-intro on \ref{impl-intro:PP-P} +% and \ref{impl-intro:P-PP}} +% \step{idempotence}{P \land P \equiv P} +% {$\equiv$-intro on \ref{and-intro:result}} +% \end{flagderiv} +% +% \subsubsection*{De Morgan} +% \begin{flagderiv}[pc-demorgan] +% \assume{intro:NPQ}{\lnot (P \land Q)}{} +% \assume{intro:NNP}{\lnot\lnot P}{} +% \assume{intro:Q}{Q}{} +% \step{notnot-elim:P}{P}{$\lnot\lnot$-elim on \ref{intro:NNP}} +% \step{and-intro:PQ}{P \land Q}{$\land$-intro on \ref{intro:Q} +% and \ref{notnot-elim:P}} +% \step{false-intro:2}{\false} +% {$\false$-intro on \ref{and-intro:PQ} +% and \ref{intro:NPQ}} +% \conclude{not-intro:Q}{\lnot Q}{$\lnot$-intro on \ref{intro:Q} +% and \ref{false-intro:2}} +% \conclude{impl-intro:NNP-NQ}{\lnot\lnot P \implies \lnot Q} +% {$\implies$-intro on \ref{intro:NNP} +% and \ref{not-intro:Q}} +% \step{or-intro:NP-NQ}{\lnot P \lor \lnot Q} +% {$\lor$-intro on \ref{impl-intro:NNP-NQ}} +% \conclude{impl-intro:NPQ-NPNQ}{\lnot (P \land Q) \implies +% \lnot P \lor \lnot Q} +% {$\implies$-intro on \ref{intro:NPQ} +% and \ref{or-intro:NP-NQ}} +% \assume{intro:NPNQ}{\lnot P \land \lnot Q}{} +% \assume{intro:PQ}{P \lor Q}{} +% \step{or-elim:NP-Q}{\lnot P \implies Q} +% {$\lor$-elim on \ref{intro:PQ}} +% \step{and-elim:NP}{\lnot P}{$\land$-elim on \ref{intro:NPNQ}} +% \step{impl-elim:Q}{Q}{$\implies$-elim on \ref{or-elim:NP-Q} +% and \ref{and-elim:NP}} +% \step{and-elim:NQ}{\lnot Q}{$\land$-elim on \ref{intro:NPNQ}} +% \step{false-intro:1}{\false}{$\false$-intro on \ref{impl-elim:Q} +% and \ref{and-elim:NQ}} +% \conclude{impl-intro:PQ}{P \lor Q \implies \false} +% {$\implies$-intro on \ref{intro:PQ} +% and \ref{false-intro:1}} +% \step{not-intro:PQ}{\lnot (P \lor Q)} +% {$\lnot$-intro on \ref{impl-intro:PQ}} +% \conclude{impl-intro:NPNQ-NPQ}{\lnot P \land \lnot Q \implies +% \lnot (P \lor Q)} +% {$\implies$-intro on \ref{intro:NPNQ} +% and \ref{not-intro:PQ}} +% \step{and-intro:result}{(\lnot (P \land Q) \implies +% \lnot P \lor \lnot Q) +% \land\\ +% (\lnot P \land \lnot Q \implies +% \lnot (P \lor Q))} +% {$\land$-intro on \ref{impl-intro:NPQ-NPNQ} +% and \ref{impl-intro:NPNQ-NPQ}} +% \step{demorgan}{\lnot (P \land Q) \equiv \lnot P \lor \lnot Q} +% {$\equiv$-intro on \ref{and-intro:result}} +% \end{flagderiv} +% +% \subsubsection*{Transitivity} +% \begin{flagderiv}[pc-transitivity] +% \introduce{intro:PQR}{P, Q, R}{} +% \assume{intro:PQQR}{(P \implies Q) \land (Q \implies R)}{} +% \assume{intro:P}{P}{} +% \step{and-elim:PQ}{P \implies Q} +% {$\land$-elim on \ref{intro:PQQR}} +% \step{impl-elim:Q}{Q}{$\implies$-elim on \ref{and-elim:PQ} +% and \ref{intro:P}} +% \step{and-elim:QR}{Q \implies R} +% {$\land$-elim on \ref{intro:PQQR}} +% \step{impl-elim:R}{R}{$\implies$-elim on \ref{and-elim:QR} +% and \ref{impl-elim:Q}} +% \conclude{impl-intro:PR}{P \implies R} +% {$\implies$-intro on \ref{intro:P} +% and \ref{impl-elim:R}} +% \conclude{impl-intro:PQQR-PR}{(P \implies Q) \land (Q \implies R) +% \implies (P \implies R)} +% {$\implies$-intro on \ref{intro:PQQR} +% and \ref{impl-intro:PR}} +% \conclude{transitivity}{(\forall P, Q, R:: +% (P \implies Q) \land (Q \implies R) +% \implies (P \implies R) +% )} +% {$\forall$-intro on \ref{intro:PQR} +% and \ref{impl-intro:PQQR-PR}} +% \end{flagderiv} +% +% \subsection{Rewrite Systems} +% \subsubsection*{Mixed confluent $\biimplies$ Church-Rosser} +% { +% \renewcommand{\introsymb}{\text{Let}} +% \begin{flagderiv} +% \assume*{1}{\CRtext}{hyp} +% \introduce*{2}{a, b, c\in A, \text{such that}~a\OHA b\land a\THA c}{} +% \step*{3}{a\OHA b\land a\THA c}{rei (2)} +% \step*{4}{a\THA b\land a\THA c}{$\forall$-elimination on lemma~\ref{transclosure} and (3)} +% \step*{5}{(\exists d\in A:: b\THA d\land c\THA d)}{$\forall$-elimination on (1) and (4)} +% \conclude*{6}{\MCtext}{$\forall$-introduction on (2) and (5)} +% \conclude*{7}{\CRtext\implies\MCtext}{$\implies$-introduction on (1) and (6)} +% \assume*{8}{\MCtext}{} +% \assume*{9}{\text{Induction on the length of}~a\THA b}{} +% \skipsteps*{\IHbase}{} +% \introduce*{11}{a, b, c\in A, \text{such that}~a\NHA{0} b\land a\THA c}{} +% \step*{12}{a=b}{def $\NHA{0}$, (11)} +% \step*{13}{a\THA c}{$\land$-elimination on (11)} +% \step*{14}{b\THA c}{(12) applied on (13)} +% \step*{15}{c\THA c \land b\THA c}{} +% \step*{16}{(\exists d\in A:: b\THA d\land c\THA d)}{} +% \renewcommand{\thesteplabel}[1]{#1} +% \conclude*{}{\IHhyp}{} +% \step*{18}{\ensuremath{(\forall a, b, c\in A: a\NHA{n} b\land a\THA c:\\ \quad +% (\exists d\in A:: b\THA d\land c\THA d))}}{} +% \skipsteps*{\IHstep}{} +% \introduce*{20}{a, b, c\in A, \text{such that}~a\NHA{n+1} b\land a\THA c}{} +% \step*{21}{a\NHA{n+1} b}{$\land$-elimination on (20)} +% \step*{22}{a\NHA{n} b'\OHA b}{} +% \step*{23}{a\THA c}{$\land$-elimination on (20)} +% \step*{24}{a\NHA{n} b' \land a\THA c}{$\land$-introduction on (22) and (23)} +% \step*{25}{(\exists d'\in A:: b'\THA d'\land c\THA d')}{$\forall$-elimination on (18) and (24)} +% \step*{26}{d', \text{such that}~b'\THA d'\land c\THA d'}{$\exists$-elimination on (25)} +% \step*{27}{b'\OHA b \land b'\THA d'}{} +% \step*{28}{(\exists d\in A:: b\THA d\land d'\THA d)}{$\forall$-elimination on (8) and (27)} +% \step*{29}{d, \text{such that}~b\THA d\land d'\THA d}{$\exists$-elimination on (28)} +% \step*{30}{a\NHA{n} b'\OHA b\THA d \land a\THA c\THA d'\THA d}{} +% \step*{31}{b\THA d \land c\THA d}{} +% \step*{32}{(\exists d\in A:: b\THA d\land c\THA d)}{} +% \conclude*[2]{33}{\CRtext}{} +% \conclude*{34}{\MCtext\implies\CRtext}{$\implies$-introduction on (8) and (33)} +% \step*{35}{\MCtext\biimplies\CRtext}{$\biimplies$-introduction on (7) and (34)} +% \end{flagderiv} +% } +% +% \begin{lemma} +% \label{transclosure} +% \mbox{\ensuremath{(\forall a, b\in A: a\OHA b: a\THA b)}} +% \end{lemma} +% +% \StopEventually{} +% +% \newpage +% \section{Implementation} +% +% First some initial code is needed for processing of the options. +% Note that {\tt ifthen} is used throughout the package. +% \begin{macrocode} +\RequirePackage{ifthen} +\newboolean{@inlcmnts} +% \end{macrocode} +% +% Processing of the option ({\tt inlcmnts}) for enabling inline comments. +% \begin{macrocode} +\DeclareOption{inlcmnts}{\setboolean{@inlcmnts}{true}} +\ProcessOptions +% \end{macrocode} +% +% Loading of the required packages. +% Note that \flags\ needs to require a fix/override for the array package, +% until the fixed version is available in most distributions. +% \begin{macrocode} +\RequirePackage{array} +\RequirePackage{longtable} +\long\@namedef{NC@rewrite@*}#1#2{% + \count@#1\relax + \loop + \ifnum\count@>\z@ + \advance\count@\m@ne + \@temptokena\expandafter{\the\@temptokena#2}% + \repeat + \NC@find} +% \end{macrocode} +% +% \subsection{Generic settings, counters and commands} +% +% \begin{macro}{fd@flagcount} +% \begin{macro}{fd@stepcount} +% The counters keeping the number of opened/nested flags and the number of +% derivation steps. +% \begin{macrocode} +\newcounter{fd@flagcount} +\newcounter{fd@stepcount} +% \end{macrocode} +% \end{macro} +% \end{macro} +% +% \begin{macro}{\derivskip} +% The default space ({\tt 8pt}) between lines in a derivation. This is +% overridable to define a different default length. +% \begin{macrocode} +\newlength{\derivskip} +\setlength{\derivskip}{8pt} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\introsymb} +% The symbol used as variable introduction prefix. Overridable with +% |\renewcommand| to insert a different symbol, defaults to: +% |\textbf{var}|. +% +% Ex. |\renewcommand{\introsymb}{\textbf{Let}}| +% \begin{macrocode} +\newcommand{\introsymb}{\textbf{var}} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\thestepcount} +% This is the command used to generate a step number label (used by +% auto-numbering). |\thestepcount| can be overridden to display labels +% differently, defaults to: ({\it number}). This exposes the internal +% |\thefd@stepcount| command. +% +% Ex. |\renewcommand{\thestepcount}{[\arabic{stepcount}]}| +% \begin{macrocode} +\newcommand{\thestepcount}{(\arabic{fd@stepcount})} +\renewcommand{\thefd@stepcount}{\thestepcount} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\thesteplabel} +% Command used to generate a customized step label (used by manual numbering). +% |\thesteplabel| can be overridden to display manual numbers differently, +% this command has one argument: \marg{label}. +% The command does nothing by default (i.e\@. just returns the argument). +% +% Ex. |\renewcommand{\thesteplabel}[1]{[##1]}| +% \begin{macrocode} +\newcommand{\thesteplabel}[1]{#1} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\theinlcmnt} +% The command used to format inline comments (if enabled). |\theinlcmnt| +% can be overridden to display it differently and has one argument: +% \marg{comment}. Defaults to: \{ {\em comment text} \}. +% +% Ex. |\renewcommand{\theinlcmnt}[1]{--#1--}| +% \begin{macrocode} +\newcommand{\theinlcmnt}[1]{\{ #1 \}} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\inlcmnts} +% Command to switch inline comments explicitly on (and by that, overriding +% and forgetting the default determined by the absence or presence of the +% {\tt inlcmnts} package option). +% +% \begin{macrocode} +\newcommand{\inlcmnts}{\setboolean{@inlcmnts}{true}} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\noinlcmnts} +% Command to switch inline comments explicitly off (and by that, overriding +% and forgetting the default determined by the absence or presence of the +% {\tt inlcmnts} package option). +% +% \begin{macrocode} +\newcommand{\noinlcmnts}{\setboolean{@inlcmnts}{false}} +% \end{macrocode} +% \end{macro} +% +% \subsection{The derivation environment} +% +% The following three sections describe the internal commands and constructs +% of the {\tt flagderiv} environment, after which the last section will +% explain how the environment works and how it is put together using the +% internal constructs. +% +% Note that for almost all commands there exists two versions, one used +% for manual numbered derivations and one for automatic numbered/labelled +% derivations (both forms can be mixed within the environment). +% +% \subsubsection{Labels} +% +% Derivation lines are labelled and can be referred to. This can be done +% with automatically numbered lines where the first argument is a normal +% \LaTeX\ label. However, to avoid clashing, the labels can be automatically +% prefixed with a namespace. The following two commands handle this prefixing. +% +% \begin{macro}{\@labelprefix} +% Command that specifies the label namespace prefix. +% +% \begin{macrocode} +\newcommand{\@labelprefix}{\relax} +% \end{macrocode} +% \end{macro} +% \begin{macro}{\@derlabel} +% Internal command to define a label using the prefix (if a label +% is defined, otherwise do nothing). +% +% \begin{macrocode} +\newcommand{\@derlabel}[1]{% + \ifthenelse{\equal{#1}{}}{}{\label{\@labelprefix#1}}% +} +% \end{macrocode} +% \end{macro} +% +% \subsubsection{Steps} +% +% A line of a derivation can be one of five types: +% \begin{enumerate} +% \item A simple and bare line, only internally accessible, +% \item a comment line, +% \item a derivation step (both automatically and manual numbered), +% \item a line to indicate skipping of steps, +% \item a flag (handled in the next section). +% \end{enumerate} +% +% This section deals with the first four types. +% +% \begin{macro}{\@derline} +% A simple derivation line that uses {\tt fd@flagcount} to remember +% the number of open flags. This command is used as: +% |\@derline|\marg{label}\marg{formula}\marg{comment}, with: +% \begin{description} +% \item[\marg{label}] a label which can be left empty, to refer back to in +% comments of other derivation lines, +% \item[\marg{formula}] the formula, and +% \item[\marg{comment}] a comment. +% \end{description} +% +% \begin{macrocode} +\newcommand{\@derline}[3]{% + \mbox{#1} & + \setlength{\extrarowheight}{\derivskip}% +% \end{macrocode} +% If the flag counter is still zero\dots +% \begin{macrocode} + \ifthenelse{\value{fd@flagcount}=0}% +% \end{macrocode} +% then this line is outside any flag, +% \begin{macrocode} + {\begin{array}[t]{@{}l}}% +% \end{macrocode} +% otherwise this is inside one or more flag contexts and the amount of +% open flagpoles equal to the number of open contexts should be inserted. +% +% \begin{macrocode} + {\begin{array}[t]{*{\value{fd@flagcount}}{|@{\hspace{2\arraycolsep}}}l}} + \ensuremath{#2} + \end{array} & + \mbox{#3} \\ +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@CMNTderline} +% Command to fold the comment on a separate line before the +% actual derivation line if the {\tt inlcmnts} option is set for this +% package, see also |\@derline| for the argument handling. +% +% \begin{macrocode} +\newcommand{\@CMNTderline}[3]{% + \ifthenelse{\boolean{@inlcmnts}}{% +% \end{macrocode} +% If the inline comments option is enabled, fold the comment before the +% actual line. +% \begin{macrocode} + \ifthenelse{\equal{#3}{}}{}{% +% \end{macrocode} +% There is comment, insert it inline. +% \begin{macrocode} + \@derline{}{\mbox{\theinlcmnt{#3}}}{}% + } + \@derline{#1}{#2}{}% + }{% +% \end{macrocode} +% If inline comments are not enabled, pass everything to |\@derline| directly. +% \begin{macrocode} + \@derline{#1}{#2}{#3}% + }% +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@MANstep} +% \begin{macro}{\@AUTOstep} +% Command for the manual ({\tt MAN}) and automatically ({\tt AUTO}) +% numbered version of a derivation step. See also |\@derline|. +% +% \begin{macrocode} +\newcommand{\@MANstep}[3]{\@CMNTderline{\thesteplabel{#1}}{#2}{#3}} +% \end{macrocode} +% +% \begin{macrocode} +\newcommand{\@AUTOstep}[3]{% + \refstepcounter{fd@stepcount}% + \@derlabel{#1}\@CMNTderline{\thestepcount}{#2}{#3}% +} +% \end{macrocode} +% \end{macro} +% \end{macro} +% +% \begin{macro}{\@MANskipsteps} +% \begin{macro}{\@AUTOskipsteps} +% Command for the manual ({\tt MAN}) and automatically ({\tt AUTO}) +% numbered version of skipping derivation steps. See also |\@derline|. +% +% \begin{macrocode} +\newcommand{\@MANskipsteps}[2]{\@CMNTderline{}{#1}{#2}} +% \end{macrocode} +% +% \begin{macrocode} +\newcommand{\@AUTOskipsteps}[3]{% + \addtocounter{fd@stepcount}{#1}% + \@CMNTderline{}{#2}{#3}% +} +% \end{macrocode} +% \end{macro} +% \end{macro} +% +% \subsubsection{Flags} +% +% Flags are actually simple derivation lines with two extras: the formula +% is put into a flag box and the flag counter {\tt fd@flagcount} is incremented +% when one is opened. Next to flag commands there are also commands to +% to close (and by that decrementing the counter) flags. +% +% There exist three types of flags: +% \begin{enumerate} +% \item the simple and bare flag, +% \item the assumption flag (both manual and automatically numbered), +% \item the variable introduction flag (also manual and automatically numbered). +% \end{enumerate} +% +% \begin{macro}{\@flagbox} +% Creates a flag for (a box around) the given text/formula, takes +% \marg{formula} as an argument. +% \begin{macrocode} +\newcommand{\@flagbox}[1]{% + \setlength{\fboxsep}{0.75ex}% + \fbox{#1}% +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@startflag} +% Starts a flag context by opening a flag and incrementing the counter. +% The command is used as: +% |\@startflag|\marg{label}\marg{formula}\marg{comment}, +% see also |\@derline| for the meaning of these arguments. +% +% \begin{macrocode} +\newcommand{\@startflag}[3]{% + \@CMNTderline{#1}{\@flagbox{\ensuremath{#2}}}{#3}% + \addtocounter{fd@flagcount}{1}% +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@endflag} +% Ends a flag by closing it and decrementing the counter. Takes the +% number of flags to close \marg{number} as an argument. +% +% \begin{macrocode} +\newcommand{\@endflag}[1]{\addtocounter{fd@flagcount}{-#1}} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@flagclose} +% Wrapper command for closing a number of flags simultaneously taking \oarg{number} +% as an optional argument, defaulting to 1. See also |\@endflag|. +% +% \begin{macrocode} +\newcommand{\@flagclose}[1][1]{\@endflag{#1}} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@MANassume} +% \begin{macro}{\@AUTOassume} +% Command for the manual ({\tt MAN}) and automatic ({\tt AUTO}) +% numbered version of an assumption flag, see also |\@startflag|. +% +% \begin{macrocode} +\newcommand{\@MANassume}[3]{\@startflag{\thesteplabel{#1}}{#2}{#3}} +% \end{macrocode} +% +% \begin{macrocode} +\newcommand{\@AUTOassume}[3]{ + \refstepcounter{fd@stepcount}% + \@derlabel{#1}\@startflag{\thestepcount}{#2}{#3}% +} +% \end{macrocode} +% \end{macro} +% \end{macro} +% +% \begin{macro}{\@MANintroduction} +% \begin{macro}{\@AUTOintroduction} +% Command for the manual ({\tt MAN}) and automatically ({\tt AUTO}) +% numbered version of an introduction flag, see also |\@startflag|. +% +% \begin{macrocode} +\newcommand{\@MANintroduction}[3]{% + \@startflag{\thesteplabel{#1}}{\introsymb~#2}{#3}% +} +% \end{macrocode} +% +% \begin{macrocode} +\newcommand{\@AUTOintroduction}[3]{ + \refstepcounter{fd@stepcount}% + \@derlabel{#1}\@startflag{\thestepcount}{\introsymb~#2}{#3}% +} +% \end{macrocode} +% \end{macro} +% \end{macro} +% +% \begin{macro}{\@MANconclude} +% \begin{macro}{\@AUTOconclude} +% Command to conclude from one or more open flags in the manual ({\tt MAN}) +% and automatically ({\tt AUTO}) numbered version, see also |\@endflag|. +% The command is used as: +% |\@MANconclude|\oarg{number}\marg{label}\marg{formula}\marg{comment}, +% where the \oarg{number} indicates the number of flags to close, +% defaulting to 1. +% +% \begin{macrocode} +\newcommand{\@MANconclude}[4][1]{\@endflag{#1}\step*{#2}{#3}{#4}} +% \end{macrocode} +% +% \begin{macrocode} +\newcommand{\@AUTOconclude}[4][1]{\@endflag{#1}\step{#2}{#3}{#4}} +% \end{macrocode} +% \end{macro} +% \end{macro} +% +% \subsubsection{The environment itself} +% +% \begin{environment}{flagderiv} +% This section explains the main environment for flag style +% derivations/proofs: {\tt flagderiv}. The command has an optional +% argument \oarg{prefix}, used as label prefix so that labels can be +% ``scoped'' with a namespace local to the derivation but still +% accessible from the outside. +% +% Examples:\\ +% |\begin{flagderiv} ... \end{flagderiv}|\\ +% |\begin{flagderiv}[abs] ... \end{flagderiv}| +% +% \begin{macrocode} +\newenvironment{flagderiv}[1][]{% +% \end{macrocode} +% +% First, set the optional label prefix (if given) and reset the counters. +% +% \begin{macrocode} + \ifthenelse{\equal{#1}{}}{% + \renewcommand{\@labelprefix}{}% + }{% + \renewcommand{\@labelprefix}{#1:}% + }% + \setcounter{fd@flagcount}{0}% + \setcounter{fd@stepcount}{0}% +% \end{macrocode} +% +% Note: {\em All} of the following five commands have a star version which +% allows manual numbering, instead of having auto-numbering, \LaTeX\ labels +% and references. +% +% \begin{macro}{\assume} +% \begin{macro}{\assume*} +% Opens an assumption flag; command usage:\\[1em] +% |\assume|\marg{label}\marg{formula}\marg{comment}\\ +% |\assume*|\marg{custom-number}\marg{formula}\marg{comment} +% +% Examples: \\ +% |\assume{assum:1}{x > 0}{Assumption}|\\ +% |\assume*{l}{\neg P}{}| +% +% \begin{macrocode} + \newcommand{\assume}{\@ifstar{\@MANassume}{\@AUTOassume}} +% \end{macrocode} +% \end{macro} +% \end{macro} +% +% \begin{macro}{\introduce} +% \begin{macro}{\introduce*} +% Opens an introduction flag. Command usage: \\[1em] +% |\introduce|\marg{label}\marg{formula}\marg{comment} \\ +% |\introduce*|\marg{custom-number}\marg{formula}\marg{comment} +% +% Examples:\\ +% |\introduce{intro-x}{x \in \mathbb{N}}{Introduction}| \\ +% |\introduce*{l - 1}{P \in s_P}{}| +% +% \begin{macrocode} + \newcommand{\introduce}{\@ifstar{\@MANintroduction}{\@AUTOintroduction}} +% \end{macrocode} +% \end{macro} +% \end{macro} +% +% \begin{macro}{\conclude} +% \begin{macro}{\conclude*} +% Performs a conclusion/multiple conclusion from one or more +% introductions and/or assumptions. The command usage:\\[1em] +% |\conclude|\oarg{number}\marg{label}\marg{formula}\marg{comment}\\ +% |\conclude*|\oarg{number}\marg{custon-number}\marg{formula}\marg{comment} +% +% The optional argument \oarg{number} indicates how much flags should be +% closed with this conclusion, this defaults to 1. +% +% Examples;\\ +% |\conclude[2]{concl:2}{x > 0 \implies ...}{$\implies$-intro on ...}|\\ +% |\conclude*{n - 1}{\neg\neg P}{$\implies$-intro on (l) ...}| +% +% \begin{macrocode} + \newcommand{\conclude}{\@ifstar{\@MANconclude}{\@AUTOconclude}} +% \end{macrocode} +% \end{macro} +% \end{macro} +% +% \begin{macro}{\step} +% \begin{macro}{\step*} +% Performs a derivation step, command usage:\\[1em] +% |\step|\marg{label}\marg{formula}\marg{comment}\\ +% |\step*|\marg{custom-number}\marg{formula}\marg{comment} +% +% Examples:\\ +% |\step{x-elim}{x > 0}{$\forall$-elem on \ref{assum:1}}|\\ +% |\step*{n - 1}{x > 0}{$\forall$-elem on (n - 3)}| +% +% Note: |\\| (line breaks) may be inserted for splitting +% large formulas. +% +% \begin{macrocode} + \newcommand{\step}{\@ifstar{\@MANstep}{\@AUTOstep}} +% \end{macrocode} +% \end{macro} +% \end{macro} +% +% \begin{macro}{\skipsteps} +% \begin{macro}{\skipsteps*} +% Skips a number of steps (for usage in examples), usage:\\[1em] +% |\skipsteps|\marg{number}\marg{formula}\marg{comments}\\ +% |\skipsteps*|\marg{formula}\marg{comments}. +% +% Examples:\\ +% |\skipsteps{3}{\vdots}{Etcetera, etcetera}|\\ +% |\skipsteps*{\vdots}{Etcetera, etcetera}| +% +% \begin{macrocode} + \newcommand{\skipsteps}{\@ifstar{\@MANskipsteps}{\@AUTOskipsteps}} +% \end{macrocode} +% \end{macro} +% \end{macro} +% +% \begin{macro}{\done} +% Closes a number of flags because contexts have been opened and +% should be closed without conclusions. Command usage: \\[1em] +% |\done|\oarg{number} +% +% This command takes a number of introductions/assumptions, \oarg{number}, +% to close as an optional argument, which defaults to 1. +% +% Examples:\\ +% |\done|\\ +% |\done[3]| +% +% \begin{macrocode} + \newcommand{\done}{\@flagclose} +% \end{macrocode} +% \end{macro} +% +% Silently override |\ref| to work with the defined namespace. +% \begin{macrocode} + \let\origref\ref% + \renewcommand{\ref}[1]{\origref{\@labelprefix##1}}% +% \end{macrocode} +% +% The actual flagderiv environment is just a longtable (called +% ``derivation''). +% +% \begin{macrocode} + \renewcommand{\tablename}{Derivation}% + \begin{longtable}[l]{rll} +}{% + \end{longtable} +} +% \end{macrocode} +% \end{environment} +% +% \begin{environment}{flagderiv*} +% The |flagderiv*| environment is almost the same as |flagderiv| +% with the only difference that the resulting derivation will and +% can not be split across pages. +% +% Example:\\ +% |\begin{flagderiv*} ... \end{flagderiv*}|\\ +% +% \begin{macrocode} +\newenvironment{flagderiv*}[1][]{% + \ifthenelse{\equal{#1}{}}{% + \renewcommand{\@labelprefix}{}% + }{% + \renewcommand{\@labelprefix}{#1:}% + }% + \setcounter{fd@flagcount}{0}% + \setcounter{fd@stepcount}{0}% + \newcommand{\assume}{\@ifstar{\@MANassume}{\@AUTOassume}} + \newcommand{\introduce}{\@ifstar{\@MANintroduction}{\@AUTOintroduction}} + \newcommand{\conclude}{\@ifstar{\@MANconclude}{\@AUTOconclude}} + \newcommand{\step}{\@ifstar{\@MANstep}{\@AUTOstep}} + \newcommand{\skipsteps}{\@ifstar{\@MANskipsteps}{\@AUTOskipsteps}} + \newcommand{\done}{\@flagclose} + \let\origref\ref% + \renewcommand{\ref}[1]{\origref{\@labelprefix##1}}% + \renewcommand{\tablename}{Derivation} + \begin{tabular}{rll} +}{% + \end{tabular} +} +% \end{macrocode} +% \end{environment} +% +% \PrintIndex +% \PrintChanges +% +% \Finale +\endinput diff --git a/Master/texmf-dist/source/latex/flagderiv/flagderiv.ins b/Master/texmf-dist/source/latex/flagderiv/flagderiv.ins new file mode 100644 index 00000000000..2dfc581c97d --- /dev/null +++ b/Master/texmf-dist/source/latex/flagderiv/flagderiv.ins @@ -0,0 +1,63 @@ +%% +%% Copyright (C) 2005 by Paul van Tilburg +%% +%% This package is free software; you can redistribute it and/or modify +%% it under the terms of the GNU General Public License as published by +%% the Free Software Foundation; either version 2 of the License, or +%% (at your option) any later version. +%% +%% This package is distributed in the hope that it will be useful, +%% but WITHOUT ANY WARRANTY; without even the implied warranty of +%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +%% GNU General Public License for more details. +%% +%% You should have received a copy of the GNU General Public License +%% along with this package; if not, write to the Free Software +%% Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + +\input docstrip.tex +\keepsilent + +\usedir{tex/latex/flagderiv} + +\preamble + +This is a generated file. + +Copyright (C) 2005 by Paul van Tilburg + +This package is free software; you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation; either version 2 of the License, or +(at your option) any later version. + +This package is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this package; if not, write to the Free Software +Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + +\endpreamble + +\generate{\file{flagderiv.sty}{\from{flagderiv.dtx}{flagderiv}}} +%\generate{\file{farray.sty}{\from{farray.dtx}{farry}}} + +\obeyspaces +\Msg{*************************************************************} +\Msg{* *} +\Msg{* To finish the installation you have to move the following *} +\Msg{* file into a directory searched by TeX: *} +\Msg{* *} +\Msg{* flagderiv.sty *} +\Msg{* *} +\Msg{* To produce the documentation run the file flagderiv.dtx *} +\Msg{* through LaTeX. *} +\Msg{* *} +\Msg{* Happy TeXing! *} +\Msg{* *} +\Msg{*************************************************************} + +\endbatchfile -- cgit v1.2.3