--- a/Pearl-jv/Paper.thy Tue Oct 12 10:07:48 2010 +0100
+++ b/Pearl-jv/Paper.thy Tue Oct 12 13:06:18 2010 +0100
@@ -3,6 +3,7 @@
imports "../Nominal-General/Nominal2_Base"
"../Nominal-General/Nominal2_Eqvt"
"../Nominal-General/Atoms"
+ "../Nominal/Abs"
"LaTeXsugar"
begin
@@ -60,7 +61,7 @@
al \cite{GabbayPitts02,Pitts03}. The most basic notion in this work is a
sort-respecting permutation operation defined over a countably infinite
collection of sorted atoms. The atoms are used for representing variable names
- that might be free or bound. Multiple sorts are necessary for being able to
+ that might be binding, bound or free. Multiple sorts are necessary for being able to
represent different kinds of variables. For example, in the language Mini-ML
there are bound term variables in lambda abstractions and bound type variables in
type schemes. In order to be able to separate them, each kind of variables needs to be
@@ -68,7 +69,8 @@
In our formalisation of the nominal logic work, we have to make a design decision
about how to represent sorted atoms and sort-respecting permutations. One possibility
- is to have separate types for the different kinds of atoms. With this one can represent
+ is to have separate types for the different kinds of atoms, say @{text "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^isub>n"}.
+ With this design one can represent
permutations as lists of pairs of atoms and the operation of applying
a permutation to an object as the overloaded function
@@ -94,18 +96,12 @@
@{text "b"}. For atoms of different type, the permutation operation
is defined as @{text "\<pi> \<bullet> c \<equiv> c"}.
-
-% Unfortunately, the type system of Isabelle/HOL is not a good fit for the way
-% atoms and sorts are used in the original formulation of the nominal logic work.
-% The reason is that one has to ensure that permutations are sort-respecting.
-% This was done implicitly in the original nominal logic work \cite{Pitts03}.
-
-
With the separate atom types and the list representation of permutations it
- is impossible to state an ``ill-sorted'' permutation, since the type system
- excludes lists containing atoms of different type. However, whenever we
- need to generalise induction hypotheses by quantifying over permutations, we
- have to build cumbersome quantifications like
+ is impossible in systems like Isabelle/HOL to state an ``ill-sorted''
+ permutation, since the type system excludes lists containing atoms of
+ different type. However, a disadvantage is that whenever we need to
+ generalise induction hypotheses by quantifying over permutations, we have to
+ build quantifications like
@{text [display,indent=10] "\<forall>\<pi>\<^isub>1 \<dots> \<forall>\<pi>\<^isub>n. \<dots>"}
@@ -130,21 +126,21 @@
\end{tabular}\hfill\numbered{fssequence}
\end{isabelle}
-
-
-
-
-
-
-
+ \noindent
+ Because of these disadvantages, we will use a single unified atom type to
+ represent atoms of different sorts. As a result, we have to deal with the
+ case that a swapping of two atoms is ill-sorted: we cannot rely anymore on
+ the type systems to exclude them.
- An advantage of the
- list representation is that the basic operations on permutations are already
- defined in the list library: composition of two permutations (written @{text
- "_ @ _"}) is just list append, and inversion of a permutation (written
- @{text "_\<^sup>-\<^sup>1"}) is just list reversal. A disadvantage is that
- permutations do not have unique representations as lists; we had to
- explicitly identify permutations according to the relation
+ We also will not represent permutations as lists of pairs of atoms. An
+ advantage of this representation is that the basic operations on
+ permutations are already defined in Isabelle's list library: composition of
+ two permutations (written @{text "_ @ _"}) is just list append, and
+ inversion of a permutation (written @{text "_\<^sup>-\<^sup>1"}) is just
+ list reversal. Another advantage is that there is a well-understood
+ induction principle for lists. A disadvantage, however, is that permutations
+ do not have unique representations as lists; we have to explicitly identify
+ them according to the relation
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -153,10 +149,13 @@
\end{tabular}\hfill\numbered{permequ}
\end{isabelle}
- When lifting the permutation operation to other types, for example sets,
- functions and so on, we needed to ensure that every definition is
- well-behaved in the sense that it satisfies the following three
- \emph{permutation properties}:
+ \noindent
+ This is a problem when lifting the permutation operation to other types, for
+ example sets, functions and so on, we need to ensure that every definition
+ is well-behaved in the sense that it satisfies some
+ \emph{permutation properties}. In the list representation we need
+ to state these properties as follows:
+
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}
@@ -167,116 +166,25 @@
\end{isabelle}
\noindent
- From these properties we were able to derive most facts about permutations, and
- the type classes of Isabelle/HOL allowed us to reason abstractly about these
- three properties, and then let the type system automatically enforce these
- properties for each type.
-
- The major problem with Isabelle/HOL's type classes, however, is that they
- support operations with only a single type parameter and the permutation
- operations @{text "_ \<bullet> _"} used above in the permutation properties
- contain two! To work around this obstacle, Nominal Isabelle
- required the user to
- declare up-front the collection of \emph{all} atom types, say @{text
- "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^isub>n"}. From this collection it used custom ML-code to
- generate @{text n} type classes corresponding to the permutation properties,
- whereby in these type classes the permutation operation is restricted to
-
- @{text [display,indent=10] "_ \<bullet> _ :: (\<alpha>\<^isub>i \<times> \<alpha>\<^isub>i) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
-
- \noindent
- This operation has only a single type parameter @{text "\<beta>"} (the @{text "\<alpha>\<^isub>i"} are the
- atom types given by the user).
-
- While the representation of permutations-as-lists solved the
- ``sort-respecting'' requirement and the declaration of all atom types
- up-front solved the problem with Isabelle/HOL's type classes, this setup
- caused several problems for formalising the nominal logic work: First,
- Nominal Isabelle had to generate @{text "n\<^sup>2"} definitions for the
- permutation operation over @{text "n"} types of atoms. Second, whenever we
- need to generalise induction hypotheses by quantifying over permutations, we
- have to build cumbersome quantifications like
-
- @{text [display,indent=10] "\<forall>\<pi>\<^isub>1 \<dots> \<forall>\<pi>\<^isub>n. \<dots>"}
-
- \noindent
- where the @{text "\<pi>\<^isub>i"} are of type @{text "(\<alpha>\<^isub>i \<times> \<alpha>\<^isub>i) list"}.
- The reason is that the permutation operation behaves differently for
- every @{text "\<alpha>\<^isub>i"}. Third, although the notion of support
-
- @{text [display,indent=10] "supp _ :: \<beta> \<Rightarrow> \<alpha> set"}
-
- \noindent
- which we will define later, has a generic type @{text "\<alpha> set"}, it cannot be
- used to express the support of an object over \emph{all} atoms. The reason
- is again that support can behave differently for each @{text
- "\<alpha>\<^isub>i"}. This problem is annoying, because if we need to know in
- a statement that an object, say @{text "x"}, is finitely supported we end up
- with having to state premises of the form
-
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- \begin{tabular}{@ {}l}
- @{text "finite ((supp x) :: \<alpha>\<^isub>1 set) , \<dots>, finite ((supp x) :: \<alpha>\<^isub>n set)"}
- \end{tabular}\hfill\numbered{fssequence}
- \end{isabelle}
+ where the last clause explicitly states that the permutation operation has
+ to produce the same result for related permutations. Moreover, permutations
+ as list do not satisfy the usual properties about groups. This means by
+ using this representation we will not be able to reuse the extensive
+ reasoning infrastructure in Isabelle about groups. Therefore, we will use
+ in this paper a unique representation for permutations by representing them
+ as functions from atoms to atoms.
- \noindent
- Sometimes we can avoid such premises completely, if @{text x} is a member of a
- \emph{finitely supported type}. However, keeping track of finitely supported
- types requires another @{text n} type classes, and for technical reasons not
- all types can be shown to be finitely supported.
-
- The real pain of having a separate type for each atom sort arises, however,
- from another permutation property
-
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}
- iv) & @{text "\<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x) = (\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}
- \end{tabular}
- \end{isabelle}
+ Using a single atom type to represent atoms of different sorts and
+ representing permutations as functions are not new ideas. The main
+ contribution of this paper is to show an example of how to make better
+ theorem proving tools by choosing the right level of abstraction for the
+ underlying theory---our design choices take advantage of Isabelle's type
+ system, type classes and reasoning infrastructure. The novel technical
+ contribution is a mechanism for dealing with ``Church-style'' lambda-terms
+ \cite{Church40} and HOL-based languages \cite{PittsHOL4} where variables and
+ variable binding depend on type annotations.
- \noindent
- where permutation @{text "\<pi>\<^isub>1"} has type @{text "(\<alpha> \<times> \<alpha>) list"},
- @{text "\<pi>\<^isub>2"} type @{text "(\<alpha>' \<times> \<alpha>') list"} and @{text x} type @{text
- "\<beta>"}. This property is needed in order to derive facts about how
- permutations of different types interact, which is not covered by the
- permutation properties @{text "i"}-@{text "iii"} shown in
- \eqref{permprops}. The problem is that this property involves three type
- parameters. In order to use again Isabelle/HOL's type class mechanism with
- only permitting a single type parameter, we have to instantiate the atom
- types. Consequently we end up with an additional @{text "n\<^sup>2"}
- slightly different type classes for this permutation property.
-
- While the problems and pain can be almost completely hidden from the user in
- the existing implementation of Nominal Isabelle, the work is \emph{not}
- pretty. It requires a large amount of custom ML-code and also forces the
- user to declare up-front all atom-types that are ever going to be used in a
- formalisation. In this paper we set out to solve the problems with multiple
- type parameters in the permutation operation, and in this way can dispense
- with the large amounts of custom ML-code for generating multiple variants
- for some basic definitions. The result is that we can implement a pleasingly
- simple formalisation of the nominal logic work.\smallskip
-
- \noindent
- {\bf Contributions of the paper:} Using a single atom type to represent
- atoms of different sorts and representing permutations as functions are not
- new ideas. The main contribution of this paper is to show an example of how
- to make better theorem proving tools by choosing the right level of
- abstraction for the underlying theory---our design choices take advantage of
- Isabelle's type system, type classes, and reasoning infrastructure.
- The novel
- technical contribution is a mechanism for dealing with
- ``Church-style'' lambda-terms \cite{Church40} and HOL-based languages
- \cite{PittsHOL4} where variables and variable binding depend on type
- annotations.
-
- Therefore it was decided in earlier versions of Nominal Isabelle to use a
- separate type for each sort of atoms and let the type system enforce the
- sort-respecting property of permutations. Inspired by the work on nominal
- unification \cite{UrbanPittsGabbay04}, it seemed best at the time to also
- implement permutations concretely as lists of pairs of atoms.
-
-
+ The paper is organised as follows
*}
section {* Sorted Atoms and Sort-Respecting Permutations *}
@@ -286,26 +194,24 @@
represented by \emph{atoms}. As stated above, we need to have different
\emph{sorts} of atoms to be able to bind different kinds of variables. A
basic requirement is that there must be a countably infinite number of atoms
- of each sort. Unlike in our earlier work, where we identified each sort with
- a separate type, we implement here atoms to be
+ of each sort. We implement these atoms as
*}
datatype atom\<iota> = Atom\<iota> string nat
text {*
\noindent
- whereby the string argument specifies the sort of the atom.\footnote{A similar
- design choice was made by Gunter et al \cite{GunterOsbornPopescu09}
- for their variables.} (The use type
- \emph{string} is merely for convenience; any countably infinite type would work
- as well.)
- We have an auxiliary function @{text sort} that is defined as @{thm
- sort_of.simps[no_vars]}, and we clearly have for every finite set @{text X} of
- atoms and every sort @{text s} the property:
-
+ whereby the string argument specifies the sort of the atom.\footnote{A
+ similar design choice was made by Gunter et al \cite{GunterOsbornPopescu09}
+ for their variables.} (The use type \emph{string} is merely for
+ convenience; any countably infinite type would work as well.) We have an
+ auxiliary function @{text sort} that is defined as @{thm
+ sort_of.simps[no_vars]}, and we clearly have for every finite set @{text X}
+ of atoms and every sort @{text s} the property:
+
\begin{proposition}\label{choosefresh}
- @{text "If finite X then there exists an atom a such that
- sort a = s and a \<notin> X"}.
+ @{text "For a finite set of atoms S, there exists an atom a such that
+ sort a = s and a \<notin> S"}.
\end{proposition}
For implementing sort-respecting permutations, we use functions of type @{typ
@@ -341,7 +247,7 @@
\noindent
but since permutations are required to respect sorts, we must carefully
consider what happens if a user states a swapping of atoms with different
- sorts. In earlier versions of Nominal Isabelle, we avoided this problem by
+ sorts. In early versions of Nominal Isabelle, we avoided this problem by
using different types for different sorts; the type system prevented users
from stating ill-sorted swappings. Here, however, definitions such
as\footnote{To increase legibility, we omit here and in what follows the
@@ -946,6 +852,218 @@
*}
+section {* An Abstraction Type *}
+
+text {*
+ To that end, we will consider
+ first pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}. These pairs
+ are intended to represent the abstraction, or binding, of the set of atoms @{text
+ "as"} in the body @{text "x"}.
+
+ The first question we have to answer is when two pairs @{text "(as, x)"} and
+ @{text "(bs, y)"} are $\alpha$-equivalent? (For the moment we are interested in
+ the notion of $\alpha$-equivalence that is \emph{not} preserved by adding
+ vacuous binders.) To answer this question, we identify four conditions: {\it (i)}
+ given a free-atom function @{text "fa"} of type \mbox{@{text "\<beta> \<Rightarrow> atom
+ set"}}, then @{text x} and @{text y} need to have the same set of free
+ atoms; moreover there must be a permutation @{text p} such that {\it
+ (ii)} @{text p} leaves the free atoms of @{text x} and @{text y} unchanged, but
+ {\it (iii)} ``moves'' their bound names so that we obtain modulo a relation,
+ say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it (iv)}
+ @{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
+ requirements {\it (i)} to {\it (iv)} can be stated formally as follows:
+ %
+ \begin{equation}\label{alphaset}
+ \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
+ \multicolumn{3}{l}{@{text "(as, x) \<approx>set R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+ & @{term "fa(x) - as = fa(y) - bs"} & \mbox{\it (i)}\\
+ @{text "\<and>"} & @{term "(fa(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
+ @{text "\<and>"} & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
+ @{text "\<and>"} & @{term "(p \<bullet> as) = bs"} & \mbox{\it (iv)}\\
+ \end{array}
+ \end{equation}
+
+ \noindent
+ Note that this relation depends on the permutation @{text
+ "p"}; $\alpha$-equivalence between two pairs is then the relation where we
+ existentially quantify over this @{text "p"}. Also note that the relation is
+ dependent on a free-atom function @{text "fa"} and a relation @{text
+ "R"}. The reason for this extra generality is that we will use
+ $\approx_{\,\textit{set}}$ for both ``raw'' terms and $\alpha$-equated terms. In
+ the latter case, @{text R} will be replaced by equality @{text "="} and we
+ will prove that @{text "fa"} is equal to @{text "supp"}.
+
+ It might be useful to consider first some examples about how these definitions
+ of $\alpha$-equivalence pan out in practice. For this consider the case of
+ abstracting a set of atoms over types (as in type-schemes). We set
+ @{text R} to be the usual equality @{text "="} and for @{text "fa(T)"} we
+ define
+
+ \begin{center}
+ @{text "fa(x) = {x}"} \hspace{5mm} @{text "fa(T\<^isub>1 \<rightarrow> T\<^isub>2) = fa(T\<^isub>1) \<union> fa(T\<^isub>2)"}
+ \end{center}
+
+ \noindent
+ Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and
+ \eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and
+ @{text "({y, x}, y \<rightarrow> x)"} are $\alpha$-equivalent according to
+ $\approx_{\,\textit{set}}$ and $\approx_{\,\textit{res}}$ by taking @{text p} to
+ be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"}, then @{text
+ "([x, y], x \<rightarrow> y)"} $\not\approx_{\,\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"}
+ since there is no permutation that makes the lists @{text "[x, y]"} and
+ @{text "[y, x]"} equal, and also leaves the type \mbox{@{text "x \<rightarrow> y"}}
+ unchanged. Another example is @{text "({x}, x)"} $\approx_{\,\textit{res}}$
+ @{text "({x, y}, x)"} which holds by taking @{text p} to be the identity
+ permutation. However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"}
+ $\not\approx_{\,\textit{set}}$ @{text "({x, y}, x)"} since there is no
+ permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal
+ (similarly for $\approx_{\,\textit{list}}$). It can also relatively easily be
+ shown that all three notions of $\alpha$-equivalence coincide, if we only
+ abstract a single atom.
+
+ In the rest of this section we are going to introduce three abstraction
+ types. For this we define
+ %
+ \begin{equation}
+ @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_set (as, x) equal supp p (bs, x)"}
+ \end{equation}
+
+ \noindent
+ (similarly for $\approx_{\,\textit{abs\_res}}$
+ and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence
+ relations and equivariant.
+
+ \begin{lemma}\label{alphaeq}
+ The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$
+ and $\approx_{\,\textit{abs\_res}}$ are equivalence relations, and if @{term
+ "abs_set (as, x) (bs, y)"} then also @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet>
+ bs, p \<bullet> y)"} (similarly for the other two relations).
+ \end{lemma}
+
+ \begin{proof}
+ Reflexivity is by taking @{text "p"} to be @{text "0"}. For symmetry we have
+ a permutation @{text p} and for the proof obligation take @{term "-p"}. In case
+ of transitivity, we have two permutations @{text p} and @{text q}, and for the
+ proof obligation use @{text "q + p"}. All conditions are then by simple
+ calculations.
+ \end{proof}
+
+ \noindent
+ This lemma allows us to use our quotient package for introducing
+ new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"}
+ representing $\alpha$-equivalence classes of pairs of type
+ @{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"}
+ (in the third case).
+ The elements in these types will be, respectively, written as:
+
+ \begin{center}
+ @{term "Abs_set as x"} \hspace{5mm}
+ @{term "Abs_res as x"} \hspace{5mm}
+ @{term "Abs_lst as x"}
+ \end{center}
+
+ \noindent
+ indicating that a set (or list) of atoms @{text as} is abstracted in @{text x}. We will
+ call the types \emph{abstraction types} and their elements
+ \emph{abstractions}. The important property we need to derive is the support of
+ abstractions, namely:
+
+ \begin{theorem}[Support of Abstractions]\label{suppabs}
+ Assuming @{text x} has finite support, then\\[-6mm]
+ \begin{center}
+ \begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
+ %@ {thm (lhs) supp_abs(1)[no_vars]} & $=$ & @ {thm (rhs) supp_abs(1)[no_vars]}\\
+ %@ {thm (lhs) supp_abs(2)[no_vars]} & $=$ & @ {thm (rhs) supp_abs(2)[no_vars]}\\
+ %@ {thm (lhs) supp_abs(3)[where bs="as", no_vars]} & $=$ & @ {thm (rhs) supp_abs(3)[where bs="as", no_vars]}
+ \end{tabular}
+ \end{center}
+ \end{theorem}
+
+ \noindent
+ Below we will show the first equation. The others
+ follow by similar arguments. By definition of the abstraction type @{text "abs_set"}
+ we have
+ %
+ \begin{equation}\label{abseqiff}
+ %@ {thm (lhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\;
+ %@ {thm (rhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]}
+ \end{equation}
+
+ \noindent
+ and also
+ %
+ \begin{equation}\label{absperm}
+ @{thm permute_Abs[no_vars]}
+ \end{equation}
+
+ \noindent
+ The second fact derives from the definition of permutations acting on pairs
+ \eqref{permute} and $\alpha$-equivalence being equivariant
+ (see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show
+ the following lemma about swapping two atoms in an abstraction.
+
+ \begin{lemma}
+ %@ {thm[mode=IfThen] abs_swap1(1)[where bs="as", no_vars]}
+ \end{lemma}
+
+ \begin{proof}
+ This lemma is straightforward using \eqref{abseqiff} and observing that
+ the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}.
+ Moreover @{text supp} and set difference are equivariant (see \cite{HuffmanUrban10}).
+ \end{proof}
+
+ \noindent
+ Assuming that @{text "x"} has finite support, this lemma together
+ with \eqref{absperm} allows us to show
+ %
+ \begin{equation}\label{halfone}
+ %@ {thm abs_supports(1)[no_vars]}
+ \end{equation}
+
+ \noindent
+ which by Property~\ref{supportsprop} gives us ``one half'' of
+ Theorem~\ref{suppabs}. The ``other half'' is a bit more involved. To establish
+ it, we use a trick from \cite{Pitts04} and first define an auxiliary
+ function @{text aux}, taking an abstraction as argument:
+ %
+ \begin{center}
+ @{thm supp_set.simps[THEN eq_reflection, no_vars]}
+ \end{center}
+
+ \noindent
+ Using the second equation in \eqref{equivariance}, we can show that
+ @{text "aux"} is equivariant (since @{term "p \<bullet> (supp x - as) =
+ (supp (p \<bullet> x)) - (p \<bullet> as)"}) and therefore has empty support.
+ This in turn means
+ %
+ \begin{center}
+ @{term "supp (supp_gen (Abs_set as x)) \<subseteq> supp (Abs_set as x)"}
+ \end{center}
+
+ \noindent
+ using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set,
+ we further obtain
+ %
+ \begin{equation}\label{halftwo}
+ %@ {thm (concl) supp_abs_subset1(1)[no_vars]}
+ \end{equation}
+
+ \noindent
+ since for finite sets of atoms, @{text "bs"}, we have
+ @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.
+ Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes
+ Theorem~\ref{suppabs}.
+
+ The method of first considering abstractions of the
+ form @{term "Abs_set as x"} etc is motivated by the fact that
+ we can conveniently establish at the Isabelle/HOL level
+ properties about them. It would be
+ laborious to write custom ML-code that derives automatically such properties
+ for every term-constructor that binds some atoms. Also the generality of
+ the definitions for $\alpha$-equivalence will help us in the next section.
+*}
+
+
section {* Concrete Atom Types *}
text {*