\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{Technical University of Munich, Germany}	

\email{urbanc@in.tum.de}

\author{Cezary Kaliszyk}

\address{University of Tsukuba, Japan}

\email{kaliszyk@cs.tsukuba.ac.jp}

\thanks{$^\star$~This is a revised and expanded version of~\cite{UrbanKaliszyk11}}

\keywords{Nominal Isabelle, variable convention, 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: