diff --git a/examples/technical_report/TR_my_commented_isabelle/document/build b/examples/technical_report/TR_my_commented_isabelle/document/build new file mode 100755 index 00000000..893af0ef --- /dev/null +++ b/examples/technical_report/TR_my_commented_isabelle/document/build @@ -0,0 +1,60 @@ +#!/usr/bin/env bash +# Copyright (c) 2018 The University of Sheffield. All rights reserved. +# 2018 The University of Paris-Sud. All rights reserved. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions +# are met: +# 1. Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# 2. Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in +# the documentation and/or other materials provided with the +# distribution. +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS +# FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE +# COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, +# INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, +# BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; +# LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER +# CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT +# LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN +# ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE +# POSSIBILITY OF SUCH DAMAGE. +# +# SPDX-License-Identifier: BSD-2-Clause + +OUTFORMAT=${1:-pdf} +NAME=${2:-root} + +set -e + +ROOT_NAME="root_$NAME" +[ ! -f "$DIR/$ROOT_NAME.tex" ] && ROOT_NAME="root" + +if [ ! -f $ISABELLE_HOME_USER/DOF/latex/DOF-core.sty ]; then + echo "" + echo "Warning: Isabelle DOF not installed" + echo "========" + echo "This is a Isabelle_DOF project. The document preparation requires" + echo "the Isabelle_DOF framework. Please obtain the framework by cloning" + echo "the Isabelle_DOF git repository, i.e.: " + echo " git clone https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF" + echo "You can install the framework as follows:" + echo " cd Isabelle_DOF/document-generator" + echo " ./install" + echo "" + exit 1 +fi + +cp $ISABELLE_HOME_USER/DOF/latex/*.sty . + +$ISABELLE_TOOL latex -o sty "$ROOT_NAME.tex" && \ +$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \ +{ [ ! -f "$ROOT_NAME.bib" ] || $ISABELLE_TOOL latex -o bbl "$ROOT_NAME.tex"; } && \ +{ [ ! -f "$ROOT_NAME.idx" ] || $ISABELLE_TOOL latex -o idx "$ROOT_NAME.tex"; } && \ +$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \ +$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" + diff --git a/examples/technical_report/TR_my_commented_isabelle/document/figures/isabelle-architecture.pdf b/examples/technical_report/TR_my_commented_isabelle/document/figures/isabelle-architecture.pdf new file mode 100644 index 00000000..60823337 Binary files /dev/null and b/examples/technical_report/TR_my_commented_isabelle/document/figures/isabelle-architecture.pdf differ diff --git a/examples/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-I.pdf b/examples/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-I.pdf new file mode 100644 index 00000000..bced6d4f Binary files /dev/null and b/examples/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-I.pdf differ diff --git a/examples/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-II.pdf b/examples/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-II.pdf new file mode 100644 index 00000000..14f6b917 Binary files /dev/null and b/examples/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-II.pdf differ diff --git a/examples/technical_report/TR_my_commented_isabelle/document/ontologies.tex b/examples/technical_report/TR_my_commented_isabelle/document/ontologies.tex new file mode 100644 index 00000000..47fcfd6c --- /dev/null +++ b/examples/technical_report/TR_my_commented_isabelle/document/ontologies.tex @@ -0,0 +1,16 @@ +%% Copyright (C) 2018 The University of Sheffield +%% 2018 The University of Paris-Sud +%% +%% License: +%% This program can be redistributed and/or modified under the terms +%% of the LaTeX Project Public License Distributed from CTAN +%% archives in directory macros/latex/base/lppl.txt; either +%% version 1 of the License, or any later version. +%% OR +%% The 2-clause BSD-style license. +%% +%% SPDX-License-Identifier: LPPL-1.0+ OR BSD-2-Clause + +%% This file is used for including the LaTeX ontology mappings. +\usepackage{DOF-core} +\usepackage{DOF-technical_report} diff --git a/examples/technical_report/TR_my_commented_isabelle/document/preamble.tex b/examples/technical_report/TR_my_commented_isabelle/document/preamble.tex new file mode 100644 index 00000000..8fede196 --- /dev/null +++ b/examples/technical_report/TR_my_commented_isabelle/document/preamble.tex @@ -0,0 +1,15 @@ +%% Copyright (C) 2018 The University of Sheffield +%% 2018 The University of Paris-Sud +%% +%% License: +%% This program can be redistributed and/or modified under the terms +%% of the LaTeX Project Public License Distributed from CTAN +%% archives in directory macros/latex/base/lppl.txt; either +%% version 1 of the License, or any later version. +%% OR +%% The 2-clause BSD-style license. +%% +%% SPDX-License-Identifier: LPPL-1.0+ OR BSD-2-Clause + +%% This is a placeholder for user-specific configuration and packages. +\usepackage{prooftree} diff --git a/examples/technical_report/TR_my_commented_isabelle/document/prooftree.sty b/examples/technical_report/TR_my_commented_isabelle/document/prooftree.sty new file mode 100644 index 00000000..abb7d448 --- /dev/null +++ b/examples/technical_report/TR_my_commented_isabelle/document/prooftree.sty @@ -0,0 +1,347 @@ +\message{} +%% Build proof tree for Natural Deduction, Sequent Calculus, etc. +%% WITH SHORTENING OF PROOF RULES! +%% Paul Taylor, begun 10 Oct 1989 +%% *** THIS IS ONLY A PRELIMINARY VERSION AND THINGS MAY CHANGE! *** +%% +%% 2 Aug 1996: fixed \mscount and \proofdotnumber +%% +%% \prooftree +%% hyp1 produces: +%% hyp2 +%% hyp3 hyp1 hyp2 hyp3 +%% \justifies -------------------- rulename +%% concl concl +%% \thickness=0.08em +%% \shiftright 2em +%% \using +%% rulename +%% \endprooftree +%% +%% where the hypotheses may be similar structures or just formulae. +%% +%% To get a vertical string of dots instead of the proof rule, do +%% +%% \prooftree which produces: +%% [hyp] +%% \using [hyp] +%% name . +%% \proofdotseparation=1.2ex .name +%% \proofdotnumber=4 . +%% \leadsto . +%% concl concl +%% \endprooftree +%% +%% Within a prooftree, \[ and \] may be used instead of \prooftree and +%% \endprooftree; this is not permitted at the outer level because it +%% conflicts with LaTeX. Also, +%% \Justifies +%% produces a double line. In LaTeX you can use \begin{prooftree} and +%% \end{prootree} at the outer level (however this will not work for the inner +%% levels, but in any case why would you want to be so verbose?). +%% +%% All of of the keywords except \prooftree and \endprooftree are optional +%% and may appear in any order. They may also be combined in \newcommand's +%% eg "\def\Cut{\using\sf cut\thickness.08em\justifies}" with the abbreviation +%% "\prooftree hyp1 hyp2 \Cut \concl \endprooftree". This is recommended and +%% some standard abbreviations will be found at the end of this file. +%% +%% \thickness specifies the breadth of the rule in any units, although +%% font-relative units such as "ex" or "em" are preferable. +%% It may optionally be followed by "=". +%% \proofrulebreadth=.08em or \setlength\proofrulebreadth{.08em} may also be +%% used either in place of \thickness or globally; the default is 0.04em. +%% \proofdotseparation and \proofdotnumber control the size of the +%% string of dots +%% +%% If proof trees and formulae are mixed, some explicit spacing is needed, +%% but don't put anything to the left of the left-most (or the right of +%% the right-most) hypothesis, or put it in braces, because this will cause +%% the indentation to be lost. +%% +%% By default the conclusion is centered wrt the left-most and right-most +%% immediate hypotheses (not their proofs); \shiftright or \shiftleft moves +%% it relative to this position. (Not sure about this specification or how +%% it should affect spreading of proof tree.) +% +% global assignments to dimensions seem to have the effect of stretching +% diagrams horizontally. +% +%%========================================================================== + +\def\introrule{{\cal I}}\def\elimrule{{\cal E}}%% +\def\andintro{\using{\land}\introrule\justifies}%% +\def\impelim{\using{\Rightarrow}\elimrule\justifies}%% +\def\allintro{\using{\forall}\introrule\justifies}%% +\def\allelim{\using{\forall}\elimrule\justifies}%% +\def\falseelim{\using{\bot}\elimrule\justifies}%% +\def\existsintro{\using{\exists}\introrule\justifies}%% + +%% #1 is meant to be 1 or 2 for the first or second formula +\def\andelim#1{\using{\land}#1\elimrule\justifies}%% +\def\orintro#1{\using{\lor}#1\introrule\justifies}%% + +%% #1 is meant to be a label corresponding to the discharged hypothesis/es +\def\impintro#1{\using{\Rightarrow}\introrule_{#1}\justifies}%% +\def\orelim#1{\using{\lor}\elimrule_{#1}\justifies}%% +\def\existselim#1{\using{\exists}\elimrule_{#1}\justifies} + +%%========================================================================== + +\newdimen\proofrulebreadth \proofrulebreadth=.05em +\newdimen\proofdotseparation \proofdotseparation=1.25ex +\newdimen\proofrulebaseline \proofrulebaseline=2ex +\newcount\proofdotnumber \proofdotnumber=3 +\let\then\relax +\def\hfi{\hskip0pt plus.0001fil} +\mathchardef\squigto="3A3B +% +% flag where we are +\newif\ifinsideprooftree\insideprooftreefalse +\newif\ifonleftofproofrule\onleftofproofrulefalse +\newif\ifproofdots\proofdotsfalse +\newif\ifdoubleproof\doubleprooffalse +\let\wereinproofbit\relax +% +% dimensions and boxes of bits +\newdimen\shortenproofleft +\newdimen\shortenproofright +\newdimen\proofbelowshift +\newbox\proofabove +\newbox\proofbelow +\newbox\proofrulename +% +% miscellaneous commands for setting values +\def\shiftproofbelow{\let\next\relax\afterassignment\setshiftproofbelow\dimen0 } +\def\shiftproofbelowneg{\def\next{\multiply\dimen0 by-1 }% +\afterassignment\setshiftproofbelow\dimen0 } +\def\setshiftproofbelow{\next\proofbelowshift=\dimen0 } +\def\setproofrulebreadth{\proofrulebreadth} + +%============================================================================= +\def\prooftree{% NESTED ZERO (\ifonleftofproofrule) +% +% first find out whether we're at the left-hand end of a proof rule +\ifnum \lastpenalty=1 +\then \unpenalty +\else \onleftofproofrulefalse +\fi +% +% some space on left (except if we're on left, and no infinity for outermost) +\ifonleftofproofrule +\else \ifinsideprooftree + \then \hskip.5em plus1fil + \fi +\fi +% +% begin our proof tree environment +\bgroup% NESTED ONE (\proofbelow, \proofrulename, \proofabove, +% \shortenproofleft, \shortenproofright, \proofrulebreadth) +\setbox\proofbelow=\hbox{}\setbox\proofrulename=\hbox{}% +\let\justifies\proofover\let\leadsto\proofoverdots\let\Justifies\proofoverdbl +\let\using\proofusing\let\[\prooftree +\ifinsideprooftree\let\]\endprooftree\fi +\proofdotsfalse\doubleprooffalse +\let\thickness\setproofrulebreadth +\let\shiftright\shiftproofbelow \let\shift\shiftproofbelow +\let\shiftleft\shiftproofbelowneg +\let\ifwasinsideprooftree\ifinsideprooftree +\insideprooftreetrue +% +% now begin to set the top of the rule (definitions local to it) +\setbox\proofabove=\hbox\bgroup$\displaystyle % NESTED TWO +\let\wereinproofbit\prooftree +% +% these local variables will be copied out: +\shortenproofleft=0pt \shortenproofright=0pt \proofbelowshift=0pt +% +% flags to enable inner proof tree to detect if on left: +\onleftofproofruletrue\penalty1 +} + +%============================================================================= +% end whatever box and copy crucial values out of it +\def\eproofbit{% NESTED TWO +% +% various hacks applicable to hypothesis list +\ifx \wereinproofbit\prooftree +\then \ifcase \lastpenalty + \then \shortenproofright=0pt % 0: some other object, no indentation + \or \unpenalty\hfil % 1: empty hypotheses, just glue + \or \unpenalty\unskip % 2: just had a tree, remove glue + \else \shortenproofright=0pt % eh? + \fi +\fi +% +% pass out crucial values from scope +\global\dimen0=\shortenproofleft +\global\dimen1=\shortenproofright +\global\dimen2=\proofrulebreadth +\global\dimen3=\proofbelowshift +\global\dimen4=\proofdotseparation +\global\count255=\proofdotnumber +% +% end the box +$\egroup % NESTED ONE +% +% restore the values +\shortenproofleft=\dimen0 +\shortenproofright=\dimen1 +\proofrulebreadth=\dimen2 +\proofbelowshift=\dimen3 +\proofdotseparation=\dimen4 +\proofdotnumber=\count255 +} + +%============================================================================= +\def\proofover{% NESTED TWO +\eproofbit % NESTED ONE +\setbox\proofbelow=\hbox\bgroup % NESTED TWO +\let\wereinproofbit\proofover +$\displaystyle +}% +% +%============================================================================= +\def\proofoverdbl{% NESTED TWO +\eproofbit % NESTED ONE +\doubleprooftrue +\setbox\proofbelow=\hbox\bgroup % NESTED TWO +\let\wereinproofbit\proofoverdbl +$\displaystyle +}% +% +%============================================================================= +\def\proofoverdots{% NESTED TWO +\eproofbit % NESTED ONE +\proofdotstrue +\setbox\proofbelow=\hbox\bgroup % NESTED TWO +\let\wereinproofbit\proofoverdots +$\displaystyle +}% +% +%============================================================================= +\def\proofusing{% NESTED TWO +\eproofbit % NESTED ONE +\setbox\proofrulename=\hbox\bgroup % NESTED TWO +\let\wereinproofbit\proofusing +\kern0.3em$ +} + +%============================================================================= +\def\endprooftree{% NESTED TWO +\eproofbit % NESTED ONE +% \dimen0 = length of proof rule +% \dimen1 = indentation of conclusion wrt rule +% \dimen2 = new \shortenproofleft, ie indentation of conclusion +% \dimen3 = new \shortenproofright, ie +% space on right of conclusion to end of tree +% \dimen4 = space on right of conclusion below rule + \dimen5 =0pt% spread of hypotheses +% \dimen6, \dimen7 = height & depth of rule +% +% length of rule needed by proof above +\dimen0=\wd\proofabove \advance\dimen0-\shortenproofleft +\advance\dimen0-\shortenproofright +% +% amount of spare space below +\dimen1=.5\dimen0 \advance\dimen1-.5\wd\proofbelow +\dimen4=\dimen1 +\advance\dimen1\proofbelowshift \advance\dimen4-\proofbelowshift +% +% conclusion sticks out to left of immediate hypotheses +\ifdim \dimen1<0pt +\then \advance\shortenproofleft\dimen1 + \advance\dimen0-\dimen1 + \dimen1=0pt +% now it sticks out to left of tree! + \ifdim \shortenproofleft<0pt + \then \setbox\proofabove=\hbox{% + \kern-\shortenproofleft\unhbox\proofabove}% + \shortenproofleft=0pt + \fi +\fi +% +% and to the right +\ifdim \dimen4<0pt +\then \advance\shortenproofright\dimen4 + \advance\dimen0-\dimen4 + \dimen4=0pt +\fi +% +% make sure enough space for label +\ifdim \shortenproofright<\wd\proofrulename +\then \shortenproofright=\wd\proofrulename +\fi +% +% calculate new indentations +\dimen2=\shortenproofleft \advance\dimen2 by\dimen1 +\dimen3=\shortenproofright\advance\dimen3 by\dimen4 +% +% make the rule or dots, with name attached +\ifproofdots +\then + \dimen6=\shortenproofleft \advance\dimen6 .5\dimen0 + \setbox1=\vbox to\proofdotseparation{\vss\hbox{$\cdot$}\vss}% + \setbox0=\hbox{% + \advance\dimen6-.5\wd1 + \kern\dimen6 + $\vcenter to\proofdotnumber\proofdotseparation + {\leaders\box1\vfill}$% + \unhbox\proofrulename}% +\else \dimen6=\fontdimen22\the\textfont2 % height of maths axis + \dimen7=\dimen6 + \advance\dimen6by.5\proofrulebreadth + \advance\dimen7by-.5\proofrulebreadth + \setbox0=\hbox{% + \kern\shortenproofleft + \ifdoubleproof + \then \hbox to\dimen0{% + $\mathsurround0pt\mathord=\mkern-6mu% + \cleaders\hbox{$\mkern-2mu=\mkern-2mu$}\hfill + \mkern-6mu\mathord=$}% + \else \vrule height\dimen6 depth-\dimen7 width\dimen0 + \fi + \unhbox\proofrulename}% + \ht0=\dimen6 \dp0=-\dimen7 +\fi +% +% set up to centre outermost tree only +\let\doll\relax +\ifwasinsideprooftree +\then \let\VBOX\vbox +\else \ifmmode\else$\let\doll=$\fi + \let\VBOX\vcenter +\fi +% this \vbox or \vcenter is the actual output: +\VBOX {\baselineskip\proofrulebaseline \lineskip.2ex + \expandafter\lineskiplimit\ifproofdots0ex\else-0.6ex\fi + \hbox spread\dimen5 {\hfi\unhbox\proofabove\hfi}% + \hbox{\box0}% + \hbox {\kern\dimen2 \box\proofbelow}}\doll% +% +% pass new indentations out of scope +\global\dimen2=\dimen2 +\global\dimen3=\dimen3 +\egroup % NESTED ZERO +\ifonleftofproofrule +\then \shortenproofleft=\dimen2 +\fi +\shortenproofright=\dimen3 +% +% some space on right and flag we've just made a tree +\onleftofproofrulefalse +\ifinsideprooftree +\then \hskip.5em plus 1fil \penalty2 +\fi +} + +%========================================================================== +% IDEAS +% 1. Specification of \shiftright and how to spread trees. +% 2. Spacing command \m which causes 1em+1fil spacing, over-riding +% exisiting space on sides of trees and not affecting the +% detection of being on the left or right. +% 3. Hack using \@currenvir to detect LaTeX environment; have to +% use \aftergroup to pass \shortenproofleft/right out. +% 4. (Pie in the sky) detect how much trees can be "tucked in" +% 5. Discharged hypotheses (diagonal lines). diff --git a/examples/technical_report/TR_my_commented_isabelle/document/root.tex b/examples/technical_report/TR_my_commented_isabelle/document/root.tex new file mode 100644 index 00000000..815c5a49 --- /dev/null +++ b/examples/technical_report/TR_my_commented_isabelle/document/root.tex @@ -0,0 +1,79 @@ +%% Copyright (C) 2018 The University of Sheffield +%% 2018 The University of Paris-Sud +%% +%% License: +%% This program can be redistributed and/or modified under the terms +%% of the LaTeX Project Public License Distributed from CTAN +%% archives in directory macros/latex/base/lppl.txt; either +%% version 1 of the License, or any later version. +%% OR +%% The 2-clause BSD-style license. +%% +%% SPDX-License-Identifier: LPPL-1 + +%% Warning: Do Not Edit! +%% ===================== +%% This is the root file for the Isabelle/DOF. +%% All customization and/or additional packages should be added to the file +%% preamble.tex. + + +\RequirePackage{ifvtex} +\documentclass[fontsize=10pt,DIV12,paper=a4,open=right,twoside,abstract=true]{scrreprt} +\usepackage[T1]{fontenc} +\usepackage[utf8]{inputenc} +\usepackage{textcomp} +\usepackage[english]{babel} +\usepackage{isabelle} +\input{ontologies} +\usepackage{isabellesym} +\usepackage{amsmath} +\usepackage{amssymb} +\usepackage[numbers, sort&compress, sectionbib]{natbib} +\input{ontologies} +\IfFileExists{preamble.tex}{\input{preamble.tex}}{}% +\usepackage{xspace} +\newcommand{\isadof}{Isabelle/DOF\xspace} +\usepackage{graphicx} +\usepackage{hyperref} +\setcounter{tocdepth}{3} +\hypersetup{% + bookmarksdepth=3 + ,pdfpagelabels + ,pageanchor=true + ,bookmarksnumbered + ,plainpages=false +} % more detailed digital TOC (aka bookmarks) +\sloppy +\allowdisplaybreaks[4] +\urlstyle{rm} +\isabellestyle{it} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%% Overrides the (rightfully issued) warning by Koma Script that \rm +%%% etc. should not be used (they are deprecated since more than a +%%% decade) + \DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm} + \DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf} + \DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt} + \DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf} + \DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + +\title{.} +\author{By bu} +\begin{document} +\maketitle +\tableofcontents +\input{session} +% optional bibliography +\IfFileExists{root.bib}{% + \bibliographystyle{abbrvnat} + \bibliography{root} +}{} +\end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: