nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:fc42d4a06c06
+:abd46dfc0212
 For example, we will not be able to lift a bound-variable function. Although
 this function can be defined for raw terms, it does not respect
 alpha-equivalence and therefore cannot be lifted. To sum up, every lifting
 of theorems to the quotient level needs proofs of some respectfulness
 properties (see \cite{Homeier05}). In the paper we show that we are able to
-automate these proofs and therefore can establish a reasoning infrastructure
+automate these proofs and as a result can automatically establish a reasoning
-for alpha-equated terms.
+infrastructure for alpha-equated terms.
 The examples we have in mind where our reasoning infrastructure will be
 helpful includes the term language of System @{text "F\<^isub>C"}, also
 known as Core-Haskell (see Figure~\ref{corehas}). This term language
 involves patterns that have lists of type-, coercion- and term-variables,
 %
 \begin{center}
 @{text "x R y"} \;\;implies\;\; @{text "(p \<bullet> x) R (p \<bullet> y)"}
 \end{center}
-Finally, the nominal logic work provides us with convenient means to rename
+Finally, the nominal logic work provides us with general means to rename
 binders. While in the older version of Nominal Isabelle, we used extensively
 Property~\ref{swapfreshfresh} for renaming single binders, this property
 proved unwieldy for dealing with multiple binders. For such binders the
 following generalisations turned out to be easier to use.
 as long as it is finitely supported) and also @{text "p"} does not affect anything
 in the support of @{text x} (that is @{term "supp x \<sharp>* p"}). The last
 fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders
 @{text as} in @{text x}, because @{term "p \<bullet> x = x"}.
-Most properties given in this section are described in \cite{HuffmanUrban10}
+Most properties given in this section are described in detail in \cite{HuffmanUrban10}
 and of course all are formalised in Isabelle/HOL. In the next sections we will make
 extensively use of these properties in order to define alpha-equivalence in
 the presence of multiple binders.
 *}
 In order to keep our work with deriving the reasoning infrastructure
 manageable, we will wherever possible state definitions and perform proofs
 on the user-level of Isabelle/HOL, as opposed to write custom ML-code that
 generates them anew for each specification. 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 @{text
+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
 \noindent
 This lemma allows us to use our quotient package and introduce
 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>"}.
+@{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 as x"} \hspace{5mm}
 @{term "Abs_res as x"} \hspace{5mm}
 \end{equation}
 \noindent
 and also
 %
-\begin{equation}
+\begin{equation}\label{absperm}
 @{thm permute_Abs[no_vars]}
 \end{equation}
 \noindent
 The second fact derives from the definition of permutations acting on pairs
 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
-This lemma allows us to show
+This lemma together with \eqref{absperm} allows us to show
 %
 \begin{equation}\label{halfone}
 @{thm abs_supports(1)[no_vars]}
 \end{equation}
 \begin{center}
 @{text "C\<^sup>\<alpha> label\<^isub>1::ty"}$'_1$ @{text "\<dots> label\<^isub>l::ty"}$'_l\;\;$  @{text "binding_clauses"}
 \end{center}
 \noindent
-whereby some of the @{text ty}$'_{1..l}$ (or their components) might be contained
+whereby some of the @{text ty}$'_{1..l}$ (or their components) can be contained
 in the collection of @{text ty}$^\alpha_{1..n}$ declared in
 \eqref{scheme}.
 In this case we will call the corresponding argument a
 \emph{recursive argument} of @{text "C\<^sup>\<alpha>"}.
 %The types of such recursive
 Shallow binders are of the form \isacommand{bind}\; {\it labels}\;
 \isacommand{in}\; {\it labels'} (similar for the other two modes). The
 restriction we impose on shallow binders is that in case of
 \isacommand{bind\_set} and \isacommand{bind\_res} the {\it labels} must
 either refer to atom types or to sets of atom types; in case of
-\isacommand{bind} we allow labels to atom types or lists of atom types. Two
+\isacommand{bind} we allow labels to 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
 set of names is bound:
 \begin{center}
 \end{tabular}
 \end{tabular}
 \end{center}
 \noindent
-Note that in this specification @{text "name"} refers to an atom type, and
+Note that for @{text lam} we have a choice which mode we use. The reason is that
-@{text "fset"} to the type of finite sets. Shallow binders can occur in the
+we bind only a single @{text name}. Having \isacommand{bind\_set} in the second
-binding part of several binding clauses.
+case changes the semantics of the specification.
+Note also that in these specifications @{text "name"} refers to an atom type, and
-A \emph{deep} binder uses an auxiliary binding function that ``picks'' out
+@{text "fset"} to the type of finite sets.
+The restrictions are as follows:
+Shallow binders can occur in the binding part of several binding clauses.
+A \emph{deep} binder, on the other hand, uses an auxiliary binding function that ``picks'' out
 the atoms in one argument of the term-constructor, which can be bound in
 other arguments and also in the same argument (we will
 call such binders \emph{recursive}, see below).
 The corresponding binding functions are expected to return either a set of atoms
 (for \isacommand{bind\_set} and \isacommand{bind\_res}) or a list of atoms
 \end{tabular}}
 \end{equation}
 \noindent
 In this specification the function @{text "bn"} determines which atoms of @{text  p} are
-bound in the argument @{text "t"}. Note that in the second-last clause the function @{text "atom"}
+bound in the argument @{text "t"}. Note that in the second-last @{text bn}-clause the
+function @{text "atom"}
 coerces a name into the generic atom type of Nominal Isabelle \cite{HuffmanUrban10}. This allows
 us to treat binders of different atom type uniformly.
 The most drastic restriction we have to impose on deep binders is that
 we cannot have ``overlapping'' deep binders. Consider for example the

changeset 2128	abd46dfc0212
parent 1961	774d631726ad
child 2134	4648bd6930e4