Putting FSet in bot typeclass.
\documentclass{llncs}+ −
\usepackage{times}+ −
\usepackage{isabelle}+ −
\usepackage{isabellesym}+ −
\usepackage{amsmath}+ −
\usepackage{amssymb}+ −
+ −
+ −
\usepackage{pdfsetup}+ −
\urlstyle{rm}+ −
\isabellestyle{it}+ −
\renewcommand{\isastyle}{\isastyleminor}+ −
\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}+ −
\renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}}+ −
\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}+ −
\renewcommand{\isasymequiv}{$\dn$}+ −
\renewcommand{\isasymiota}{}+ −
\renewcommand{\isasymrightleftharpoons}{}+ −
\renewcommand{\isasymemptyset}{$\varnothing$}+ −
+ −
\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}+ −
+ −
+ −
\begin{document}+ −
+ −
\title{Proof Pearl: A New Foundation for Nominal Isabelle}+ −
\author{Brian Huffman\inst{1} and Christian Urban\inst{2}}+ −
\institute{Portland State University \and Technical University of Munich}+ −
\maketitle+ −
+ −
\begin{abstract}+ −
Pitts et al introduced a beautiful theory about names and binding based on the+ −
notions of permutation and support. The engineering challenge is to smoothly+ −
adapt this theory to a theorem prover environment, in our case Isabelle/HOL.+ −
We present a formalisation of this work that differs from our earlier approach+ −
in two important respects: First, instead of representing permutations as+ −
lists of pairs of atoms, we now use a more abstract representation based on+ −
functions. Second, whereas the earlier work modeled different sorts of atoms+ −
using different types, we now introduce a unified atom type that includes all+ −
sorts of atoms. Interestingly, we allow swappings, that is permutations build from+ −
two atoms, to be ill-sorted. As a result of these design changes, we can iron+ −
out inconveniences for the user, considerably simplify proofs and also+ −
drastically reduce the amount of custom ML-code. Furthermore we can extend the+ −
capabilities of Nominal Isabelle to deal with variables that carry additional+ −
information. We end up with a pleasing and formalised theory of permutations+ −
and support, on which we can build an improved and more powerful version of+ −
Nominal Isabelle.+ −
\end{abstract}+ −
+ −
% generated text of all theories+ −
\input{session}+ −
+ −
% optional bibliography+ −
\bibliographystyle{abbrv}+ −
\bibliography{root}+ −
+ −
\end{document}+ −
+ −
%%% Local Variables:+ −
%%% mode: latex+ −
%%% TeX-master: t+ −
%%% End:+ −