nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:dff8bd922812
+:8beda0b4e35a
 to a variable bound somewhere else, are not excluded by Ott, but we have
 to).
 Our insistence on reasoning with alpha-equated terms comes from the
 wealth of experience we gained with the older version of Nominal Isabelle:
-for non-trivial properties, reasoning about alpha-equated terms is much
+for non-trivial properties, reasoning with alpha-equated terms is much
 easier than reasoning with raw terms. The fundamental reason for this is
 that the HOL-logic underlying Nominal Isabelle allows us to replace
 ``equals-by-equals''. In contrast, replacing
 ``alpha-equals-by-alpha-equals'' in a representation based on raw terms
 requires a lot of extra reasoning work.
 \end{center}
 \noindent
 We take as the starting point a definition of raw terms (defined as a
 datatype in Isabelle/HOL); identify then the alpha-equivalence classes in
-the type of sets of raw terms according to our alpha-equivalence relation
+the type of sets of raw terms according to our alpha-equivalence relation,
 and finally define the new type as these alpha-equivalence classes
 (non-emptiness is satisfied whenever the raw terms are definable as datatype
 in Isabelle/HOL and the property that our relation for alpha-equivalence is
 indeed an equivalence relation).
 We use for sets of atoms the abbreviation
 @{thm (lhs) fresh_star_def[no_vars]}, defined as
 @{thm (rhs) fresh_star_def[no_vars]}.
 A striking consequence of these definitions is that we can prove
 without knowing anything about the structure of @{term x} that
-swapping two fresh atoms, say @{text a} and @{text b}, leave
+swapping two fresh atoms, say @{text a} and @{text b}, leaves
-@{text x} unchanged.
+@{text x} unchanged:
 \begin{property}\label{swapfreshfresh}
 @{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
 \end{property}
 \end{tabular}
 \end{center}
 \noindent
 Similarly for the other binding modes.
 There are a few restrictions we need to impose: First, a body can only occur in
 \emph{one} binding clause of a term constructor.
 For binders we distinguish between \emph{shallow} and \emph{deep} binders.
 Shallow binders are just labels. The
-restrictions we need to impose on them are that in case of
+restriction we need to impose on them is that in case of
 \isacommand{bind\_set} and \isacommand{bind\_res} the labels must
 either refer to atom types or to sets of atom types; in case of
 \isacommand{bind} the labels must refer to atom types or lists of atom types.
 Two examples for the use of shallow binders are the specification of
 lambda-terms, where a single name is bound, and type-schemes, where a finite
 \end{tabular}
 \end{center}
 \noindent
 Note that for @{text lam} it does not matter which binding mode we use. The reason is that
-we bind only a single @{text name}. However, having \isacommand{bind\_set}, or even
+we bind only a single @{text name}. However, having \isacommand{bind\_set} or
-\isacommand{bind}, in the second
+\isacommand{bind} in the second
 case changes the semantics of the specification.
 Note also that in these specifications @{text "name"} refers to an atom type, and
 @{text "fset"} to the type of finite sets.
 A \emph{deep} binder uses an auxiliary binding function that ``picks'' out
 \hspace{5mm}$\mid$~@{text "bn(PTup p\<^isub>1 p\<^isub>2) = bn(p\<^isub>1) @ bn(p\<^isub>2)"}\\
 \end{tabular}}
 \end{equation}
 \noindent
-In this specification the function @{text "bn"} determines which atoms of @{text  p} are
+In this specification the function @{text "bn"} determines which atoms of
-bound in the argument @{text "t"}. Note that in the second-last @{text bn}-clause the
+@{text p} are bound in the argument @{text "t"}. Note that in the
-function @{text "atom"}
+second-last @{text bn}-clause the function @{text "atom"} coerces a name
-coerces a name into the generic atom type of Nominal Isabelle \cite{HuffmanUrban10}.
+into the generic atom type of Nominal Isabelle \cite{HuffmanUrban10}. This
-This allows
+allows us to treat binders of different atom type uniformly.
-us to treat binders of different atom type uniformly.
+As said above, for deep binders we allow binding clauses such as
-The most drastic restriction we have to impose on deep binders is that
+%
-we cannot have more than one binding function for one binder. Consider for example the
-term-constructors:
 \begin{center}
 \begin{tabular}{ll}
-@{text "Foo\<^isub>1 p::pat t::trm"} &
+@{text "Bar p::pat t::trm"} &
-\isacommand{bind} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\
-@{text "Foo\<^isub>2 x::name p::pat t::trm"} &
-\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t}, ***\\
-\end{tabular}
-\end{center}
-\noindent
-In the first case the intention is to bind all atoms from the pattern @{text p} in @{text t}
-and also all atoms from @{text q} in @{text t}. Unfortunately, we have no way
-to determine whether the binder came from the binding function @{text
-"bn(p)"} or @{text "bn(q)"}. Similarly in the second case. The reason why
-we must exclude such specifications is that they cannot be represented by
-the general binders described in Section \ref{sec:binders}. However
-the following two term-constructors are allowed
-\begin{center}
-\begin{tabular}{ll}
-@{text "Bar\<^isub>1 p::pat t::trm s::trm"} &
-\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "t s"}\\
-@{text "Bar\<^isub>2 p::pat t::trm"} &
 \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p t"}\\
 \end{tabular}
 \end{center}
 \noindent
-since there is no overlap of binders. Unlike shallow binders, we restrict deep
+where the argument of the deep binder is also in the body. We call such
-binders to occur in only one binding clause. Therefore @{text "Bar\<^isub>2"} cannot
+binders \emph{recursive}.  To see the purpose of such recursive binders,
-be reformulated as
+compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s in the following
+specification:
-\begin{center}
-\begin{tabular}{ll}
-@{text "Bar\<^isub>3 p::pat t::trm"} &
-\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p"},
-\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "t"}\\
-\end{tabular}
-\end{center}
-Note that in the @{text "Bar\<^isub>2"}, we wrote \isacommand{bind}~@{text
-"bn(p)"}~\isacommand{in}~@{text "p.."}.  Whenever such a binding clause
-is present, where the argument in the binder also occurs in the body, we will
-call the corresponding binder \emph{recursive}.  To see the
-purpose of such recursive binders, compare ``plain'' @{text "Let"}s and
-@{text "Let_rec"}s in the following specification:
 %
 \begin{equation}\label{letrecs}
 \mbox{%
 \begin{tabular}{@ {}l@ {}}
 \isacommand{nominal\_datatype}~@{text "trm ="}\\
 The difference is that with @{text Let} we only want to bind the atoms @{text
 "bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms
 inside the assignment. This difference has consequences for the free-variable
 function and alpha-equivalence relation, which we are going to describe in the
 rest of this section.
+The restriction we have to impose on deep binders is that we cannot have
+more than one binding function for one binder. So we exclude:
+\begin{center}
+\begin{tabular}{ll}
+@{text "Baz p::pat t::trm"} &
+\isacommand{bind} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\
+\end{tabular}
+\end{center}
+\noindent
+The reason why we must exclude such specifications is that they cannot be
+represented by the general binders described in Section
+\ref{sec:binders}. Unlike shallow binders, we restrict deep binders to occur
+in only one binding clause.
 We also need to restrict the form of the binding functions. As will shortly
 become clear, we cannot return an atom in a binding function that is also
 bound in the corresponding term-constructor. That means in the example
 \eqref{letpat} that the term-constructors @{text PVar} and @{text PTup} may
 (as in case @{text PNil}), a singleton set or singleton list containing an
 atom (case @{text PVar}), or unions of atom sets or appended atom lists
 (case @{text PTup}). This restriction will simplify some automatic proofs
 later on.
-In order to simplify some later definitions, we shall assume specifications
+In order to simplify later definitions, we shall assume specifications
 of term-calculi are \emph{completed}. By this we mean that
 for every argument of a term-constructor that is \emph{not}
 already part of a binding clause, we add implicitly a special \emph{empty} binding
 clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "label"}. In case
 of the lambda-calculus, the completion produces

changeset 2140	8beda0b4e35a
parent 2139	dff8bd922812
child 2141	b9292bbcffb6