\documentclass{lmcs}+
−
%%\usepackage{times}+
−
\usepackage{isabelle}+
−
\usepackage{isabellesym}+
−
\usepackage{amsmath}+
−
\usepackage{amssymb}+
−
%%\usepackage{amsthm}+
−
\usepackage{tikz}+
−
\usepackage{pgf}+
−
\usepackage{ot1patch}+
−
\usepackage{times}+
−
\usepackage{boxedminipage}+
−
\usepackage{proof}+
−
\usepackage{setspace}+
−
\usepackage{afterpage}+
−
\usepackage{pdfsetup}+
−
+
−
\allowdisplaybreaks+
−
\urlstyle{rm}+
−
\isabellestyle{it}+
−
\renewcommand{\isastyleminor}{\it}%+
−
\renewcommand{\isastyle}{\normalsize\it}%+
−
+
−
\DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}}+
−
\DeclareRobustCommand{\frqq}{\mbox{\guillemotright}}+
−
\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}+
−
\renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\hspace{-0.5mm}\cdot\hspace{-0.5mm}}$}}}+
−
\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}+
−
\renewcommand{\isasymequiv}{$\dn$}+
−
%%\renewcommand{\isasymiota}{}+
−
\renewcommand{\isasymxi}{$..$}+
−
\renewcommand{\isasymemptyset}{$\varnothing$}+
−
\newcommand{\isasymnotapprox}{$\not\approx$}+
−
\newcommand{\isasymLET}{$\mathtt{let}$}+
−
\newcommand{\isasymAND}{$\mathtt{and}$}+
−
\newcommand{\isasymIN}{$\mathtt{in}$}+
−
\newcommand{\isasymEND}{$\mathtt{end}$}+
−
\newcommand{\isasymBIND}{$\mathtt{bind}$}+
−
\newcommand{\isasymANIL}{$\mathtt{anil}$}+
−
\newcommand{\isasymACONS}{$\mathtt{acons}$}+
−
\newcommand{\isasymCASE}{$\mathtt{case}$}+
−
\newcommand{\isasymOF}{$\mathtt{of}$}+
−
\newcommand{\isasymAL}{\makebox[0mm][l]{$^\alpha$}}+
−
\newcommand{\isasymPRIME}{\makebox[0mm][l]{$'$}}+
−
\newcommand{\isasymFRESH}{\#}+
−
\newcommand{\LET}{\;\mathtt{let}\;}+
−
\newcommand{\IN}{\;\mathtt{in}\;}+
−
\newcommand{\END}{\;\mathtt{end}\;}+
−
\newcommand{\AND}{\;\mathtt{and}\;}+
−
\newcommand{\fv}{\mathit{fv}}+
−
+
−
\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}+
−
%----------------- theorem definitions ----------+
−
%%\theoremstyle{plain}+
−
%%\spnewtheorem{thm}[section]{Theorem}+
−
%%\newtheorem{property}[thm]{Property}+
−
%%\newtheorem{lemma}[thm]{Lemma}+
−
%%\spnewtheorem{defn}[theorem]{Definition}+
−
%%\spnewtheorem{exmple}[theorem]{Example}+
−
%%\spnewtheorem{myproperty}{Property}{\bfseries}{\rmfamily}+
−
%-------------------- environment definitions -----------------+
−
\newenvironment{proof-of}[1]{{\em Proof of #1:}}{}+
−
+
−
%\addtolength{\textwidth}{2mm}+
−
\addtolength{\parskip}{-0.33mm}+
−
\begin{document}+
−
+
−
\title[Genral Bindings]{General Bindings and Alpha-Equivalence in Nominal+
−
Isabelle$^\star$}+
−
\author{Christian Urban} +
−
\address{King's College London, United Kingdom}	+
−
\email{christian.urban@kcl.ac.uk}+
−
+
−
\author{Cezary Kaliszyk}+
−
\address{University of Innsbruck, Austria}+
−
\email{cezary.kaliszyk@uibk.ac.at}+
−
\thanks{$^\star$~This is a revised and expanded version of~\cite{UrbanKaliszyk11}}+
−
+
−
\keywords{Nominal Isabelle, variable convention, alpha-equivalence, theorem provers, formal reasoning, lambda-calculus}+
−
\subjclass{F.3.1}+
−
+
−
\begin{abstract} +
−
Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem+
−
prover. It provides a proving infrastructure for reasoning about+
−
programming language calculi involving named bound variables (as+
−
opposed to de-Bruijn indices). In this paper we present an extension of+
−
Nominal Isabelle for dealing with general bindings, that means+
−
term constructors where multiple variables are bound at once. Such general+
−
bindings are ubiquitous in programming language research and only very+
−
poorly supported with single binders, such as lambda-abstractions. Our+
−
extension includes new definitions of alpha-equivalence and establishes+
−
automatically the reasoning infrastructure for alpha-equated terms. We+
−
also prove strong induction principles that have the usual variable+
−
convention already built in.+
−
\end{abstract}+
−
+
−
\maketitle+
−
\input{session}+
−
+
−
\bibliographystyle{plain}+
−
\bibliography{root}+
−
+
−
+
−
%\pagebreak+
−
%\input{Appendix} +
−
+
−
\end{document}+
−
+
−
%%% Local Variables:+
−
%%% mode: latex+
−
%%% TeX-master: t+
−
%%% End:+
−