From 442d732696ad431b84f6e5c72b6ee785be4fd968 Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Sat, 10 Feb 2024 02:22:14 +0100
Subject: Initial commit

---
 latex/naproche.sty | 182 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 182 insertions(+)
 create mode 100644 latex/naproche.sty

(limited to 'latex/naproche.sty')

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
-- 
cgit v1.2.3

