nominal2: comparison LMCS-Paper/Paper.thy

equal deleted inserted replaced

-:3f32a3eb5618
+:a609eea06119
 Now the last clause ensures that the order of the binders matters (since @{text as}
 and @{text bs} are lists of atoms).
 If we do not want to make any difference between the order of binders \emph{and}
 also allow vacuous binders, that means according to Pitts~\cite{Pitts04}
-\emph{restrict} names, then we keep sets of binders, but drop
+\emph{restrict} atoms, then we keep sets of binders, but drop
 condition {\it (iv)} in Definition~\ref{alphaset}:
 \begin{defi}[Alpha-Equivalence for Set+-Bindings]\label{alphares}\mbox{}\\
 \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl}
 @{term "alpha_res_ex (as, x) R fa (bs, y)"}\hspace{2mm}@{text "\<equiv>"} &
 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
 \[
-@{text "fa(x) \<equiv> {x}"}  \hspace{5mm} @{text "fa(T\<^isub>1 \<rightarrow> T\<^isub>2) \<equiv> fa(T\<^isub>1) \<union> fa(T\<^isub>2)"}
+@{text "fa(x) \<equiv> {x}"}  \hspace{10mm} @{text "fa(T\<^isub>1 \<rightarrow> T\<^isub>2) \<equiv> fa(T\<^isub>1) \<union> fa(T\<^isub>2)"}
 \]\smallskip
 \noindent
 Now recall the examples shown in \eqref{ex1} and
 \eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and
 and @{text "\<pi>\<^isub>2"}, and for the proof obligation use @{text
 "\<pi>\<^isub>1 + \<pi>\<^isub>2"}. Equivariance means @{term "alpha_set_ex (\<pi> \<bullet> as,
 \<pi> \<bullet> x) equal supp (\<pi> \<bullet> bs, \<pi> \<bullet> y)"} holds provided \mbox{@{term
 "alpha_set_ex (as, x) equal supp(bs, y)"}} holds. From the assumption we
 have a permutation @{text "\<pi>'"} and for the proof obligation use @{text "\<pi> \<bullet>
-\<pi>'"}. To show then equivariance, we need to `pull out' the permutations,
+\<pi>'"}. To show equivariance, we need to `pull out' the permutations,
 which is possible since all operators, namely as @{text "#\<^sup>*, -, =, \<bullet>,
 set"} and @{text "supp"}, are equivariant (see
 \cite{HuffmanUrban10}). Finally, we apply the permutation operation on
 booleans.
 \end{proof}
 \begin{equation}\label{halftwo}
 @{thm (concl) Abs_supp_subset1(1)[no_vars]}
 \end{equation}\smallskip
 \noindent
-This is because for every finite sets of atoms, say @{text "bs"}, we have
+This is because for every finite set of atoms, say @{text "bs"}, we have
 @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.
 Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes
 the first equation of Theorem~\ref{suppabs}. The others are similar.
 Recall the definition of support given in \eqref{suppdef}, and note the difference between
 @{text "\<forall>x\<^isub>1\<dots>x\<^isub>l. y = C\<AL>\<^isub>m x\<^isub>1 \<dots> x\<^isub>l \<Rightarrow> P"}\\
 \end{array}}
 \end{equation}\smallskip
 \noindent
-where @{text "y"} is a variable of type @{text "ty"}$_i$ and @{text "P"} is the
+where @{text "y"} is a variable of type @{text "ty\<AL>"}$_i$ and @{text "P"} is the
 property that is established by the case analysis. Similarly, we have a (mutual)
 induction principle for the types @{text "ty\<AL>"}$_{1..n}$, which is of the
 form
 \begin{equation}\label{induct}
 \end{array}}
 \end{tabular}}
 \end{equation}\smallskip
 By working now completely on the alpha-equated level, we
-can first show using \eqref{calphaeqvt} that the support of each term
+can first show using \eqref{calphaeqvt} and Property~\ref{swapfreshfresh} that the support of each term
 constructor is included in the support of its arguments,
 namely
 \[
 @{text "(supp x\<^isub>1 \<union> \<dots> \<union> supp x\<^isub>r) supports (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r)"}
 hypothesis requires us to establish (under some assumptions) a property
 @{text "P (C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r)"} for \emph{all} @{text
 "x"}$_{1..r}$. The problem with this is that in the presence of binders we cannot make
 any assumptions about the atoms that are bound---for example assuming the variable convention.
 One obvious way around this
-problem is to rename them. Unfortunately, this leads to very clunky proofs
+problem is to rename bound atoms. Unfortunately, this leads to very clunky proofs
 and makes formalisations grievous experiences (especially in the context of
 multiple bound atoms).
 For the older versions of Nominal Isabelle we described in \cite{Urban08} a
 method for automatically strengthening weak induction principles. These
 for @{text "c"} (third line); for @{text "Let_pat\<^sup>\<alpha>"} we can assume
 all bound atoms from an assignment are fresh for @{text "c"} (fourth
 line). In order to see how an instantiation for @{text "c"} in the
 conclusion `controls' the premises, one has to take into account that
 Isabelle/HOL is a typed logic. That means if @{text "c"} is instantiated
-with a pair, for example, then this type-constraint will be propagated to
+with, for example, a pair, then this type-constraint will be propagated to
 the premises. The main point is that if @{text "c"} is instantiated
 appropriately, then the user can mimic the usual `pencil-and-paper'
 reasoning employing the variable convention about bound and free variables
 being distinct \cite{Urban08}.
 These stronger cases lemmas can be derived from the `weak' cases lemmas
 given in \eqref{inductex}. This is trivial in case of patterns (the one on
 the right-hand side) since the weak and strong cases lemma coincide (there
 is no binding in patterns).  Interesting are only the cases for @{text
 "Lam\<^sup>\<alpha>"} and @{text "Let_pat\<^sup>\<alpha>"}, where we have some binders and
-therefore have an addition assumption about avoiding @{text "c"}.  Let us
+therefore have an additional assumption about avoiding @{text "c"}.  Let us
 first establish the case for @{text "Lam\<^sup>\<alpha>"}. By the weak cases lemma
 \eqref{inductex} we can assume that
 \begin{equation}\label{assm}
 @{text "y = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2"}
 we define @{text "\<pi> \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"} with @{text "y\<^isub>i"} determined as follows:
 \[\mbox{
 \begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}}
 $\bullet$ & @{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\
-$\bullet$ & @{text "y\<^isub>i \<equiv> \<pi> \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\
+$\bullet$ & @{text "y\<^isub>i \<equiv> \<pi> \<bullet>\<^bsub>bn\<^esub> x\<^isub>i"} provided @{text "bn x\<^isub>i"} is in @{text "rhs"}\\
 $\bullet$ & @{text "y\<^isub>i \<equiv> \<pi> \<bullet> x\<^isub>i"} otherwise
 \end{tabular}}
 \]\smallskip
 \noindent
 Using again the quotient package  we can lift the auxiliary permutation operations
 @{text "_ \<bullet>\<^bsub>bn\<^esub> _"}
-to alpha-equated terms. Moreover we can prove the following two properties
+to alpha-equated terms. Moreover we can prove the following two properties:
 \begin{lem}\label{permutebn}
 Given a binding function @{text "bn\<^sup>\<alpha>"} and auxiliary equivalence @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"}
 then for all @{text "\<pi>"}\smallskip\\
 {\it (i)} @{text "\<pi> \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x)"} and\\
 holds. This allows us to use the implication from the strong cases
 lemma, and we are done.
 Consequently,  we can discharge all proof-obligations about having covered all
 cases. This completes the proof establishing that the weak induction principles imply
-the strong induction principles. These strong induction principles have proved
+the strong induction principles. These strong induction principles have already proved
-already to be very useful in practice, particularly for proving properties about
+being very useful in practice, particularly for proving properties about
-capture-avoiding substitution.
+capture-avoiding substitution \cite{Urban08}.
 *}
 section {* Related Work\label{related} *}
 any nominal techniques.  To our knowledge there is no concrete mathematical
 result concerning this notion of alpha-equivalence and free variables. We
 have proved that our definitions lead to alpha-equated terms, whose support
 is as expected (that means bound atoms are removed from the support). We
 also showed that our specifications lift from `raw' types to types of
-alpha-equivalence classes. For this we had to establish (automatically) that every
+alpha-equivalence classes. For this we have established (automatically) that every
 term-constructor and function defined for `raw' types
 is respectful w.r.t.~alpha-equivalence.
 Although we were heavily inspired by the syntax of Ott, its definition of
 alpha-equi\-valence is unsuitable for our extension of Nominal
 it in others so that the definitions make sense in the context of alpha-equated
 terms. We also introduced two binding modes (set and set+) that do not exist
 in Ott. We have tried out the extension with calculi such as Core-Haskell,
 type-schemes and approximately a dozen of other typical examples from
 programming language research~\cite{SewellBestiary}. The code will
-eventually become part of the next Isabelle distribution.\footnote{It
+eventually become part of the Isabelle distribution.\footnote{It
 can be downloaded already from \href{http://isabelle.in.tum.de/nominal/download}
 {http://isabelle.in.tum.de/nominal/download}.}
 We have left out a discussion about how functions can be defined over
 alpha-equated terms involving general binders. In earlier versions of

changeset 3044	a609eea06119
parent 3042	9b9723930a02
child 3098	3d9562921451