48 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem |
48 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem |
49 prover. It provides a proving infrastructure for convenient reasoning about |
49 prover. It provides a proving infrastructure for convenient reasoning about |
50 programming language calculi involving bound variables that have names (as |
50 programming language calculi involving bound variables that have names (as |
51 opposed to de-Bruijn indices). In this paper we present an extension of |
51 opposed to de-Bruijn indices). In this paper we present an extension of |
52 Nominal Isabelle for dealing with general bindings, that means |
52 Nominal Isabelle for dealing with general bindings, that means |
53 term-constructors where multiple variables are bound at once. Such |
53 term-constructors where multiple variables are bound at once. Such binding |
54 binding structures are ubiquitous in programming language research and only |
54 structures are ubiquitous in programming language research and only very |
55 very poorly supported with single binders, such as the lambdas in the |
55 poorly supported with single binders, such as lambda-abstractions. Our |
56 lambda-calculus. Our extension includes novel definitions of |
56 extension includes novel definitions of alpha-equivalence and establishes |
57 alpha-equivalence and establishes automatically the reasoning infrastructure for |
57 automatically the reasoning infrastructure for alpha-equated terms. We |
58 alpha-equated terms. We can also provide strong induction principles that have |
58 also provide strong induction principles that have the usual variable |
59 the usual variable convention already built in. |
59 convention already built in. |
60 \end{abstract} |
60 \end{abstract} |
61 |
61 |
62 |
62 |
63 \input{session} |
63 \input{session} |
64 |
64 |