Initial commit

2 files changed, 228 insertions, 0 deletions

diff --git a/latex/naproche.sty b/latex/naproche.sty
new file mode 100644
index 0000000..9764693
--- /dev/null
+++ b/latex/naproche.sty
@@ -0,0 +1,182 @@
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{naproche}[2021/02/04 Typesetting for Naproche formalizations]
+
+\RequirePackage{amsmath}
+\RequirePackage{amssymb}
+\RequirePackage{amsthm}
+\RequirePackage{etoolbox}
+\RequirePackage{thmtools}
+\RequirePackage{nameref,cleveref}
+
+% command for importing theories, no visible rendering
+\newcommand{\import}[1]{}
+\newcommand{\explanation}[1]{\quad\text{[#1]}}
+
+
+
+
+\newtheoremstyle{formalized}% name of the style to be used
+    {4pt}% measure of space to leave above the theorem. E.g.: 3pt
+    {4pt}% measure of space to leave below the theorem. E.g.: 3pt
+    {\normalfont} % name of font to use in the body of the theorem
+    {0pt}% measure of space to indent
+    {\bfseries}% name of head font
+    {}% punctuation between head and body
+    { }% space after theorem head; " " = normal inter-word space
+    {\thmname{#1}\thmnumber{ #2}. \thmnote{ (#3) }}
+
+\theoremstyle{formalized}
+\newcounter{theoremcount}
+
+\newtheorem{abbreviation}[theoremcount]{Abbreviation}
+\newtheorem{axiom}[theoremcount]{Axiom}
+\newtheorem{corollary}[theoremcount]{Corollary}
+\newtheorem{definition}[theoremcount]{Definition}
+\newtheorem{struct}[theoremcount]{Struct}
+\newtheorem{fact}[theoremcount]{Fact}
+\newtheorem{lemma}[theoremcount]{Lemma}
+\newtheorem{proposition}[theoremcount]{Proposition}
+\newtheorem{remark}[theoremcount]{Remark}
+\newtheorem{signature}[theoremcount]{Signature}
+\newtheorem{theorem}[theoremcount]{Theorem}
+
+% Theorem environments without numbering.
+\newtheorem*{quotedaxiom}{Axiom}
+\newtheorem*{quotedcorollary}{Corollary}
+\newtheorem*{quoteddefinition}{Definition}
+\newtheorem*{quotedstruct}{Struct}
+\newtheorem*{quotedfact}{Fact}
+\newtheorem*{quotedlemma}{Lemma}
+\newtheorem*{quotedproposition}{Proposition}
+\newtheorem*{quotedremark}{Remark}
+\newtheorem*{quotedsignature}{Signature}
+\newtheorem*{quotedtheorem}{Theorem}
+
+\crefname{axiom}{axiom}{axioms}
+\crefname{claim}{claim}{claims}
+\crefname{theorem}{theorem}{theorems}
+\crefname{definition}{definition}{definitions}
+\crefname{abbreviation}{abbreviation}{abbreviations}
+\crefname{proposition}{proposition}{propositions}
+\crefname{lemma}{lemma}{lemmas}
+
+\newcommand{\fun}[1]{\operatorname{\mathsf{#1}}}
+
+
+\newenvironment{byCase}{}{}
+\newcommand{\caseOf}[1]{\par{}Case:\ #1}
+
+\newenvironment{subproof}{\textit{Subproof.\ }}{$\square$}
+
+
+
+
+% Symbols
+% =======
+
+\newcommand{\addNat}{+_{\naturals}}
+\newcommand{\apply}[2]{#1(#2)}
+\newcommand{\bipartitions}[1]{\fun{Bipartitions}#1}
+\newcommand{\bijections}[2]{\fun{Bi}(#1,#2)}
+\newcommand{\cons}[2]{\fun{cons}(#1,#2)}
+\newcommand{\converse}[1]{{#1^{\mathsf{T}}}}
+\newcommand{\dom}[1]{\fun{dom}#1}
+\newcommand{\downward}[2]{#2^{\downarrow #1}}
+\newcommand{\equivalenceClass}[2]{[#2]_{#1}}
+\newcommand{\equivfrompartition}[1]{E_{#1}}
+\newcommand{\fld}[1]{\fun{field}#1}
+\newcommand{\fst}[1]{\fun{fst}#1}
+\newcommand{\funs}[2]{\fun{Fun}(#1,#2)}
+\newcommand{\idempotents}[1]{\fun{Idempotent}(#1)}
+\newcommand{\identity}[1]{\fun{id}_{#1}}
+\newcommand{\img}[2]{#1^{\to}(#2)}
+\newcommand{\inj}[2]{\fun{Inj}(#1,#2)}
+\newcommand{\inter}{\cap}
+\newcommand{\inters}[1]{\bigcap #1}
+\newcommand{\leNat}{\leq_{\naturals}}
+\newcommand{\meets}{\mathrel{\supset\!\!\!\subset}}
+\newcommand{\memrel}[1]{{\in_{#1}}}
+\newcommand{\monusNat}{-_{\naturals}}
+\newcommand{\naturals}{\mathcal{N}}
+\newcommand{\notmeets}{\mathrel{\not\meets}}
+\newcommand{\pow}[1]{\fun{Pow}(#1)}
+\newcommand{\precedes}{<}
+\newcommand{\precedeseq}{\leq}
+\newcommand{\preimg}[2]{#1^{\leftarrow}(#2)}
+\newcommand{\principalfilter}[2]{{\uparrow_{#1}}#2}
+\newcommand{\quotient}[2]{#1/#2}
+\newcommand{\ran}[1]{\fun{ran}#1}
+\newcommand{\reals}{\mathcal{R}}
+\newcommand{\refines}{\leq}
+\newcommand{\reflexiveClosure}[2]{\fun{ReflCl}_{#1}(#2)}
+\newcommand{\reflexiveReduction}[2]{\fun{ReflReduc}_{#1}(#2)}
+\newcommand{\relcomp}{;}
+\newcommand{\rels}[2]{\fun{Rel}(#1,#2)}
+\newcommand{\remove}[2]{#2\setminus\{#1\}}
+\newcommand{\snd}[1]{\fun{snd}#1}
+\newcommand{\subseteqrel}[1]{{\subseteq_{#1}}}
+\newcommand{\suc}[1]{#1^{+}}
+\newcommand{\sucNat}[1]{\suc{#1}}
+\newcommand{\surj}[2]{\fun{Surj}(#1,#2)}
+\newcommand{\symdiff}{\mathbin{\triangle}}
+\newcommand{\symmetricClosure}[1]{\fun{SymCl}(#1)}
+\newcommand{\toorder}[2]{\fun{OrderFromStrictOrder}_{#1}(#2)}
+\newcommand{\tostrictorder}[1]{\fun{StrictOrderFromOrder}(#1)}
+\newcommand{\union}{\cup}
+\newcommand{\unions}[1]{\bigcup #1}
+\newcommand{\Univ}[1]{\fun{Univ}(#1)}
+\newcommand{\upward}[2]{#2^{\uparrow #1}}
+\newcommand{\LeftOrb}[2]{#2\cdot #1}
+
+
+\newcommand\restrl[2]{{% we make the whole thing an ordinary symbol
+  \left.\kern-\nulldelimiterspace % automatically resize the bar with \right
+  #1 % the function
+  \vphantom{\big|} % pretend it's a little taller at normal size
+  \right|_{#2} % this is the delimiter
+  }}
+\let\mathonlyin\in
+\renewcommand{\in}{\texorpdfstring{\ensuremath{\mathonlyin}}{∈}}
+
+\let\mathonlysubseteq\subseteq
+%\renewcommand{\subseteq}{\ensuremath{\mathonlysubseteq}}
+\renewcommand{\subseteq}{\texorpdfstring{\ensuremath{\mathonlysubseteq}}{⊆}}
+
+
+% Structure operations
+
+\newcommand{\carrier}[1][]{#1}
+\newcommand{\mul}[1][]{\textsf{mul}_{#1}}
+\newcommand{\neutral}[1][]{\textsf{e}_{#1}}
+\newcommand{\lt}[1][]{\leq_{#1}}
+\newcommand{\opens}[1][]{\mathcal{O}_{#1}}
+\newcommand{\meet}[1][]{\sqcap_{#1}}
+\newcommand{\join}[1][]{\sqcup_{#1}}
+
+\newcommand{\closeds}[1]{\mathcal{C}_{#1}}
+\newcommand{\interiors}[2]{\fun{Int}_{#2}{#1}}
+\newcommand{\interior}[2]{\fun{int}_{#2}{#1}}
+\newcommand{\closures}[2]{\fun{Cl}_{#2}{#1}}
+\newcommand{\closure}[2]{\fun{cl}_{#2}{#1}}
+\newcommand{\frontier}[2]{\fun{fr}_{#2}{#1}}
+\newcommand{\neighbourhoods}[2]{\textsf{N}_{#2}{#1}}
+\newcommand{\disconnections}[1]{\fun{Disconnections}{#1}}
+
+\newcommand{\teezero}{\ensuremath{T_0}} % Kolmogorov
+\newcommand{\teeone}{\ensuremath{T_1}} % accessible/Frechet
+\newcommand{\teetwo}{\ensuremath{T_2}} % separated/Hausdorff
+\newcommand{\teetwoandahalf}{\ensuremath{T_{2\frac{1}{2}}}} % Urysohn
+\newcommand{\teethree}{\ensuremath{T_3}} % regular Hausdorff
+
+
+% Options
+% =======
+
+\DeclareOption{numberswithinsection}{%
+    \counterwithin{theoremcount}{section}
+}
+\DeclareOption{numberswithinsubsection}{%
+    \counterwithin{theoremcount}{subsection}
+}
+\DeclareOption*{\PackageWarning{naproche}{Unknown ‘\CurrentOption’}}
+\ProcessOptions\relax
diff --git a/latex/stdlib.tex b/latex/stdlib.tex
new file mode 100644
index 0000000..3673801
--- /dev/null
+++ b/latex/stdlib.tex
@@ -0,0 +1,46 @@
+\documentclass{scrartcl}
+
+\usepackage{amsmath}
+\usepackage{hyperref}
+\usepackage{comment}
+\usepackage{cleveref}
+\usepackage{naproche}
+
+\crefdefaultlabelformat{[#2#1#3]}
+%\creflabelformat{theoremcount}{[#2#1#3]}
+
+\begin{document}
+    \tableofcontents
+
+    \input{../library/set.tex}
+    \input{../library/set/cons.tex}
+    \input{../library/set/suc.tex}
+    \input{../library/set/symdiff.tex}
+    \input{../library/set/product.tex}
+    \input{../library/set/powerset.tex}
+    \input{../library/set/bipartition.tex}
+    \input{../library/set/partition.tex}
+    \input{../library/set/cantor.tex}
+    \input{../library/set/filter.tex}
+    \input{../library/set/regularity.tex}
+    \input{../library/set/fixpoint.tex}
+    \input{../library/relation.tex}
+    \input{../library/relation/properties.tex}
+    \input{../library/order/quasiorder.tex}
+    \input{../library/relation/equivalence.tex}
+    \input{../library/relation/closure.tex}
+    \input{../library/relation/uniqueness.tex}
+    \input{../library/function.tex}
+    \input{../library/ordinal.tex}
+    \input{../library/nat.tex}
+    \input{../library/cardinal.tex}
+    \input{../library/algebra/magma.tex}
+    \input{../library/algebra/semigroup.tex}
+    %\input{../library/algebra/quasigroup.tex}
+    %\input{../library/algebra/loop.tex}
+    \input{../library/order/order.tex}
+    \input{../library/order/semilattice.tex}
+    \input{../library/topology/topological-space.tex}
+    \input{../library/topology/basis.tex}
+    \input{../library/topology/disconnection.tex}
+\end{document}