1 \documentclass{lmcs} |
|
2 %%\usepackage{times} |
|
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} |
|
15 \usepackage{afterpage} |
|
16 \usepackage{pdfsetup} |
|
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} |
|
60 %%\spnewtheorem{myproperty}{Property}{\bfseries}{\rmfamily} |
|
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 |
|
68 \title[Genral Bindings]{General Bindings and Alpha-Equivalence in Nominal |
|
69 Isabelle$^\star$} |
|
70 \author{Christian Urban} |
|
71 \address{Technical University of Munich, Germany} |
|
72 \email{urbanc@in.tum.de} |
|
73 |
|
74 \author{Cezary Kaliszyk} |
|
75 \address{University of Tsukuba, Japan} |
|
76 \email{kaliszyk@cs.tsukuba.ac.jp} |
|
77 \thanks{$^\star$~This is a revised and expanded version of~\cite{UrbanKaliszyk11}} |
|
78 |
|
79 \keywords{Nominal Isabelle, variable convention, theorem provers, formal reasoning, lambda-calculus} |
|
80 \subjclass{F.3.1} |
|
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 |
|
88 term-constructors where multiple variables are bound at once. Such general |
|
89 bindings are ubiquitous in programming language research and only very |
|
90 poorly supported with single binders, such as lambda-abstractions. Our |
|
91 extension includes new definitions of alpha-equivalence and establishes |
|
92 automatically the reasoning infrastructure for alpha-equated terms. We |
|
93 also prove strong induction principles that have the usual variable |
|
94 convention already built in. |
|
95 \end{abstract} |
|
96 |
|
97 \maketitle |
|
98 \input{session} |
|
99 |
|
100 \bibliographystyle{plain} |
|
101 \bibliography{root} |
|
102 |
|
103 |
|
104 %\pagebreak |
|
105 %\input{Appendix} |
|
106 |
|
107 \end{document} |
|
108 |
|
109 %%% Local Variables: |
|
110 %%% mode: latex |
|
111 %%% TeX-master: t |
|
112 %%% End: |
|