\documentclass{acmconf}\usepackage{isabelle}\usepackage{isabellesym}\usepackage{amsmath}\usepackage{amssymb}\usepackage{tikz}\usepackage{pgf}\usepackage{pdfsetup}\usepackage{ot1patch}\urlstyle{rm}\isabellestyle{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{\isasymemptyset}{$\varnothing$}\newcommand{\LET}{\;\mathtt{let}\;}\newcommand{\IN}{\;\mathtt{in}\;}\newcommand{\END}{\;\mathtt{end}\;}\newcommand{\AND}{\;\mathtt{and}\;}%----------------- theorem definitions ----------\newtheorem{property}{Property}[section]\newtheorem{Theorem}{Theorem}[section]\newtheorem{Definition}[Theorem]{Definition}\newtheorem{Example}{\it Example}[section]%-------------------- environment definitions -----------------\newenvironment{example}[0]{\begin{Example} \it}{\end{Example}}\newenvironment{proof-of}[1]{{\em Proof of #1:}}{}\begin{document}\title{\LARGE\bf General Binding Structures in Nominal Isabelle,\\ or How to Formalise Core-Haskell}\maketitle\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. In this paper we present an extension of NominalIsabelle for dealing with general binding structures. Such binding structuresare ubiquitous in programming language research and only very poorly supportedby theorem provers providing only single binding as in the lambda-calculus. Wegive in this paper novel definitions for alpha-equivalence and establishautomatically the reasoning structure for alpha-equated terms. For example weprovide a strong induction principle that has the variable convention alreadybuilt in.\end{abstract}\input{session}\bibliographystyle{plain}\bibliography{root}\end{document}%%% Local Variables:%%% mode: latex%%% TeX-master: t%%% End: