2989
|
1 |
\documentclass{lmcs}
|
|
2 |
%%\usepackage{times}
|
2985
|
3 |
\usepackage{isabelle}
|
|
4 |
\usepackage{isabellesym}
|
|
5 |
\usepackage{amsmath}
|
|
6 |
\usepackage{amssymb}
|
|
7 |
%%\usepackage{amsthm}
|
|
8 |
\usepackage{tikz}
|
|
9 |
\usepackage{pgf}
|
|
10 |
\usepackage{ot1patch}
|
|
11 |
\usepackage{times}
|
|
12 |
\usepackage{boxedminipage}
|
|
13 |
\usepackage{proof}
|
|
14 |
\usepackage{setspace}
|
3023
|
15 |
\usepackage{afterpage}
|
3028
|
16 |
\usepackage{pdfsetup}
|
2985
|
17 |
|
|
18 |
\allowdisplaybreaks
|
|
19 |
\urlstyle{rm}
|
|
20 |
\isabellestyle{it}
|
|
21 |
\renewcommand{\isastyleminor}{\it}%
|
|
22 |
\renewcommand{\isastyle}{\normalsize\it}%
|
|
23 |
|
|
24 |
\DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}}
|
|
25 |
\DeclareRobustCommand{\frqq}{\mbox{\guillemotright}}
|
|
26 |
\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
|
|
27 |
\renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\hspace{-0.5mm}\cdot\hspace{-0.5mm}}$}}}
|
|
28 |
\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
|
|
29 |
\renewcommand{\isasymequiv}{$\dn$}
|
|
30 |
%%\renewcommand{\isasymiota}{}
|
|
31 |
\renewcommand{\isasymxi}{$..$}
|
|
32 |
\renewcommand{\isasymemptyset}{$\varnothing$}
|
|
33 |
\newcommand{\isasymnotapprox}{$\not\approx$}
|
|
34 |
\newcommand{\isasymLET}{$\mathtt{let}$}
|
|
35 |
\newcommand{\isasymAND}{$\mathtt{and}$}
|
|
36 |
\newcommand{\isasymIN}{$\mathtt{in}$}
|
|
37 |
\newcommand{\isasymEND}{$\mathtt{end}$}
|
|
38 |
\newcommand{\isasymBIND}{$\mathtt{bind}$}
|
|
39 |
\newcommand{\isasymANIL}{$\mathtt{anil}$}
|
|
40 |
\newcommand{\isasymACONS}{$\mathtt{acons}$}
|
|
41 |
\newcommand{\isasymCASE}{$\mathtt{case}$}
|
|
42 |
\newcommand{\isasymOF}{$\mathtt{of}$}
|
|
43 |
\newcommand{\isasymAL}{\makebox[0mm][l]{$^\alpha$}}
|
|
44 |
\newcommand{\isasymPRIME}{\makebox[0mm][l]{$'$}}
|
|
45 |
\newcommand{\isasymFRESH}{\#}
|
|
46 |
\newcommand{\LET}{\;\mathtt{let}\;}
|
|
47 |
\newcommand{\IN}{\;\mathtt{in}\;}
|
|
48 |
\newcommand{\END}{\;\mathtt{end}\;}
|
|
49 |
\newcommand{\AND}{\;\mathtt{and}\;}
|
|
50 |
\newcommand{\fv}{\mathit{fv}}
|
|
51 |
|
|
52 |
\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}
|
|
53 |
%----------------- theorem definitions ----------
|
|
54 |
%%\theoremstyle{plain}
|
|
55 |
%%\spnewtheorem{thm}[section]{Theorem}
|
|
56 |
%%\newtheorem{property}[thm]{Property}
|
|
57 |
%%\newtheorem{lemma}[thm]{Lemma}
|
|
58 |
%%\spnewtheorem{defn}[theorem]{Definition}
|
|
59 |
%%\spnewtheorem{exmple}[theorem]{Example}
|
2989
|
60 |
%%\spnewtheorem{myproperty}{Property}{\bfseries}{\rmfamily}
|
2985
|
61 |
%-------------------- environment definitions -----------------
|
|
62 |
\newenvironment{proof-of}[1]{{\em Proof of #1:}}{}
|
|
63 |
|
|
64 |
%\addtolength{\textwidth}{2mm}
|
|
65 |
\addtolength{\parskip}{-0.33mm}
|
|
66 |
\begin{document}
|
|
67 |
|
2993
|
68 |
\title[Genral Bindings]{General Bindings and Alpha-Equivalence in Nominal
|
|
69 |
Isabelle$^\star$}
|
2989
|
70 |
\author{Christian Urban}
|
3106
|
71 |
\address{King's College London, United Kingdom}
|
|
72 |
\email{christian.urban@kcl.ac.uk}
|
2989
|
73 |
|
|
74 |
\author{Cezary Kaliszyk}
|
|
75 |
\address{University of Tsukuba, Japan}
|
3014
|
76 |
\email{kaliszyk@cs.tsukuba.ac.jp}
|
2993
|
77 |
\thanks{$^\star$~This is a revised and expanded version of~\cite{UrbanKaliszyk11}}
|
2989
|
78 |
|
3043
|
79 |
\keywords{Nominal Isabelle, variable convention, theorem provers, formal reasoning, lambda-calculus}
|
2991
|
80 |
\subjclass{F.3.1}
|
2985
|
81 |
|
|
82 |
\begin{abstract}
|
|
83 |
Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem
|
|
84 |
prover. It provides a proving infrastructure for reasoning about
|
|
85 |
programming language calculi involving named bound variables (as
|
|
86 |
opposed to de-Bruijn indices). In this paper we present an extension of
|
|
87 |
Nominal Isabelle for dealing with general bindings, that means
|
3106
|
88 |
term constructors where multiple variables are bound at once. Such general
|
2985
|
89 |
bindings are ubiquitous in programming language research and only very
|
|
90 |
poorly supported with single binders, such as lambda-abstractions. Our
|
2989
|
91 |
extension includes new definitions of alpha-equivalence and establishes
|
|
92 |
automatically the reasoning infrastructure for alpha-equated terms. We
|
2985
|
93 |
also prove strong induction principles that have the usual variable
|
|
94 |
convention already built in.
|
|
95 |
\end{abstract}
|
|
96 |
|
2989
|
97 |
\maketitle
|
2985
|
98 |
\input{session}
|
|
99 |
|
2989
|
100 |
\bibliographystyle{plain}
|
|
101 |
\bibliography{root}
|
|
102 |
|
2985
|
103 |
|
|
104 |
%\pagebreak
|
|
105 |
%\input{Appendix}
|
|
106 |
|
|
107 |
\end{document}
|
|
108 |
|
|
109 |
%%% Local Variables:
|
|
110 |
%%% mode: latex
|
|
111 |
%%% TeX-master: t
|
|
112 |
%%% End:
|