21 \renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}} |
21 \renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}} |
22 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
22 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
23 \renewcommand{\isasymequiv}{$\dn$} |
23 \renewcommand{\isasymequiv}{$\dn$} |
24 \renewcommand{\isasymiota}{} |
24 \renewcommand{\isasymiota}{} |
25 \renewcommand{\isasymemptyset}{$\varnothing$} |
25 \renewcommand{\isasymemptyset}{$\varnothing$} |
|
26 \newcommand{\isasymnotapprox}{$\not\approx$} |
|
27 \newcommand{\isasymLET}{$\mathtt{let}$} |
|
28 \newcommand{\isasymAND}{$\mathtt{and}$} |
|
29 \newcommand{\isasymIN}{$\mathtt{in}$} |
|
30 \newcommand{\isasymEND}{$\mathtt{end}$} |
|
31 \newcommand{\isasymBIND}{$\mathtt{bind}$} |
|
32 \newcommand{\isasymANIL}{$\mathtt{anil}$} |
|
33 \newcommand{\isasymACONS}{$\mathtt{acons}$} |
26 \newcommand{\LET}{\;\mathtt{let}\;} |
34 \newcommand{\LET}{\;\mathtt{let}\;} |
27 \newcommand{\IN}{\;\mathtt{in}\;} |
35 \newcommand{\IN}{\;\mathtt{in}\;} |
28 \newcommand{\END}{\;\mathtt{end}\;} |
36 \newcommand{\END}{\;\mathtt{end}\;} |
29 \newcommand{\AND}{\;\mathtt{and}\;} |
37 \newcommand{\AND}{\;\mathtt{and}\;} |
30 \newcommand{\fv}{\mathit{fv}} |
38 \newcommand{\fv}{\mathit{fv}} |
54 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem |
62 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem |
55 prover. It provides a proving infrastructure for convenient reasoning about |
63 prover. It provides a proving infrastructure for convenient reasoning about |
56 programming language calculi involving named bound variables (as |
64 programming language calculi involving named bound variables (as |
57 opposed to de-Bruijn indices). In this paper we present an extension of |
65 opposed to de-Bruijn indices). In this paper we present an extension of |
58 Nominal Isabelle for dealing with general bindings, that means |
66 Nominal Isabelle for dealing with general bindings, that means |
59 term-constructors where multiple variables are bound at once. Such binding |
67 term-constructors where multiple variables are bound at once. Such general |
60 structures are ubiquitous in programming language research and only very |
68 bindings are ubiquitous in programming language research and only very |
61 poorly supported with single binders, such as lambda-abstractions. Our |
69 poorly supported with single binders, such as lambda-abstractions. Our |
62 extension includes novel definitions of alpha-equivalence and establishes |
70 extension includes novel definitions of alpha-equivalence and establishes |
63 automatically the reasoning infrastructure for alpha-equated terms. We |
71 automatically the reasoning infrastructure for alpha-equated terms. We |
64 also provide strong induction principles that have the usual variable |
72 also provide strong induction principles that have the usual variable |
65 convention already built in. |
73 convention already built in. |