\documentclass{llncs}\usepackage{times}\usepackage{isabelle}\usepackage{isabellesym}\usepackage{amsmath}\usepackage{amssymb}%%\usepackage{amsthm}\usepackage{tikz}\usepackage{pgf}\usepackage{pdfsetup}\usepackage{ot1patch}\usepackage{times}\usepackage{boxedminipage}\usepackage{proof}\usepackage{setspace}\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{General Bindings and Alpha-Equivalence\\ in Nominal Isabelle}\author{Christian Urban and Cezary Kaliszyk}\institute{TU Munich, Germany}%%%{\{urbanc, kaliszyk\}@in.tum.de}\maketitle\begin{abstract} Nominal Isabelle is a definitional extension of the Isabelle/HOL theoremprover. It provides a proving infrastructure for reasoning aboutprogramming language calculi involving named bound variables (asopposed to de-Bruijn indices). In this paper we present an extension ofNominal Isabelle for dealing with general bindings, that meansterm-constructors where multiple variables are bound at once. Such generalbindings are ubiquitous in programming language research and only verypoorly supported with single binders, such as lambda-abstractions. Ourextension includes new definitions of $\alpha$-equivalence and establishesautomatically the reasoning infrastructure for $\alpha$-equated terms. Wealso prove strong induction principles that have the usual variableconvention already built in.\end{abstract}%\category{F.4.1}{subcategory}{third-level}%\terms%formal reasoning, programming language calculi%\keywords%nominal logic work, variable convention\input{session}\begin{spacing}{0.9} \bibliographystyle{plain} \bibliography{root}\end{spacing}%\pagebreak%\input{Appendix} \end{document}%%% Local Variables:%%% mode: latex%%% TeX-master: t%%% End: