\documentclass[10pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{amssymb}
\usepackage[left=2.25cm,right=2.25cm,top=2.25cm,bottom=2.75cm]{geometry}
\usepackage{graphicx}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage[only,bigsqcap]{stmaryrd}
\usepackage{pdfsetup}

\urlstyle{tt}
\isabellestyle{it}

% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}

\renewcommand{\isacharunderscore}{\_}

\begin{document}

\title{Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals}
\author{Jasmin Christian Blanchette, Mathias Fleury, and Dmitriy Traytel}

\maketitle

\begin{abstract}
\noindent
This Isabelle/HOL formalization introduces a nested multiset datatype and
defines Dershowitz and Manna's nested multiset order. The order is proved well
founded and linear. By removing one constructor, we transform the nested
multisets into hereditary multisets. These are isomorphic to the syntactic
ordinals---the ordinals can be recursively expressed in Cantor normal form.
Addition, subtraction, multiplication, and linear orders are provided on this
type.
\end{abstract}

\tableofcontents

% sane default for proof documents
\parindent 0pt
\parskip 0.5ex

\section{Introduction}

This Isabelle/HOL formalization introduces a nested multiset datatype and
defines Dershowitz and Manna's nested multiset order. The order is proved well
founded and linear. By removing one constructor, we transform the nested
multisets into hereditary multisets. These are isomorphic to the syntactic
ordinals---the ordinals can be recursively expressed in Cantor normal form.
Addition, subtraction, multiplication, and linear orders are provided on this
type.

In addition, signed (or hybrid) multisets are provided (i.e., multisets with
possibly negative multiplicities), as well as signed hereditary multisets
and signed ordinals (e.g., $\omega^2 - 2\omega + 1$).

We refer to the following conference paper for details:

\begin{quote}
Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel: \\
Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL. \\
FSCD 2017: 11:1-11:18 \\
\url{https://hal.inria.fr/hal-01599176/document}
\end{quote}

% generated text of all theories
\input{session}

% optional bibliography
%\bibliographystyle{abbrv}
%\bibliography{root}

%\bibliographystyle{abbrv}
%\bibliography{bib}

\end{document}
