\documentclass{acmconf}\usepackage{isabelle}\usepackage{isabellesym}\usepackage{amsmath}\usepackage{amssymb}\usepackage{amsthm}\usepackage{tikz}\usepackage{pgf}\usepackage{pdfsetup}\usepackage{ot1patch}\usepackage{times}\usepackage{boxedminipage}\usepackage{proof}\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{\cdot}$}}}\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{\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}\newtheorem{thm}{Theorem}[section]\newtheorem{property}[thm]{Property}\newtheorem{lemma}[thm]{Lemma}\newtheorem{defn}[thm]{Definition}\newtheorem{exmple}[thm]{Example}%-------------------- environment definitions -----------------\newenvironment{proof-of}[1]{{\em Proof of #1:}}{}\begin{document}\title{\LARGE\bf General Bindings in Nominal Isabelle,\\ or How to Formalise Core-Haskell}\author{Christian Urban, Cezary Kaliszyk}\affiliation{TU Munich, Germany}\maketitle\begin{abstract} Nominal Isabelle is a definitional extension of the Isabelle/HOL theoremprover. It provides a proving infrastructure for convenient 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 novel 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}\input{session}\bibliographystyle{plain}\bibliography{root}\end{document}%%% Local Variables:%%% mode: latex%%% TeX-master: t%%% End: