nominal2: comparison LMCS-Paper/Paper.thy

equal deleted inserted replaced

-:af6eda1fb91f
+:3941fa3f179a
 each type @{text "ty"}$^\alpha_{1..n}$) that decrease in every induction
 step and the other is that we have covered all cases in the induction
 principle. Once these two proof obligations are discharged, the reasoning
 infrastructure of the function package will automatically derive the
 stronger induction principle. This way of establishing the stronger induction
-principle is considerably simpler than the earlier work presented \cite{Urban08}.
+principle is considerably simpler than the earlier work presented in \cite{Urban08}.
 As measures we can use the size functions @{text "size_ty"}$^\alpha_{1..n}$,
 which we lifted in the previous section and which are all well-founded. It
 is straightforward to establish that the sizes decrease in every
 induction step. What is left to show is that we covered all cases.
 \]\smallskip
 \noindent
 They are stronger in the sense that they allow us to assume in the @{text
 "Lam\<^sup>\<alpha>"} and @{text "Let_pat\<^sup>\<alpha>"} cases that the bound atoms
-avoid a context @{text "c"} (which is assumed to be finitely supported).
+avoid, or being fresh for, a context @{text "c"} (which is assumed to be finitely supported).
 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
 \noindent
 which we must use in order to infer @{text "P\<^bsub>trm\<^esub>"}. Clearly, we cannot
 use this implication directly, because we have no information whether or not @{text
 "x\<^isub>1"} is fresh for @{text "c"}.  However, we can use Properties
-\ref{supppermeq} and \ref{avoiding} to rename @{text "x\<^isub>1"}: we know
+\ref{supppermeq} and \ref{avoiding} to rename @{text "x\<^isub>1"}. We know
 by Theorem~\ref{suppfa} that @{text "{atom x\<^isub>1} #\<^sup>* Lam\<^sup>\<alpha>
 x\<^isub>1 x\<^isub>2"} (since its support is @{text "supp x\<^isub>2 -
 {atom x\<^isub>1}"}). Property \ref{avoiding} provides us then with a
 permutation @{text "\<pi>"}, such that @{text "{atom (\<pi> \<bullet> x\<^isub>1)} #\<^sup>*
 c"} and \mbox{@{text "supp (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2) #\<^sup>* \<pi>"}} hold.
 \eqref{letrecs}.  In such cases @{text "(\<pi> \<bullet> x\<^isub>1)
 \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} does not hold in general. The idea however is
 that @{text "\<pi>"} only renames atoms that become bound. In this way @{text "\<pi>"}
 does not affect @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"} (which only tracks alpha-equivalence of terms that are not
 under the binder). However, the problem is that the
-permutation operation @{text "\<pi> \<bullet> x\<^isub>1"} applies to all attoms in @{text "x\<^isub>1"}. To avoid this
+permutation operation @{text "\<pi> \<bullet> x\<^isub>1"} applies to all atoms in @{text "x\<^isub>1"}. To avoid this
 we introduce an auxiliary permutation operations, written @{text "_
 \<bullet>\<^bsub>bn\<^esub> _"}, for deep binders that only permutes bound atoms (or
 more precisely the atoms specified by the @{text "bn"}-functions) and leaves
 the other atoms unchanged. Like the functions @{text "fa_bn"}$_{1..m}$, we
 can define these permutation operations over raw terms analysing how the functions @{text
 \]\smallskip
 \noindent
 Using again the quotient package  we can lift the auxiliary permutation operations
 @{text "_ \<bullet>\<^bsub>bn\<^esub> _"}
-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\\
 \noindent
 The first property states that a permutation applied to a binding function
 is equivalent to first permuting the binders and then calculating the bound
 atoms. The second states that @{text "_ \<bullet>\<AL>\<^bsub>bn\<^esub> _"} preserves
 @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"}.  The main point of the auxiliary
-permutation functions is that they allow us to rename just the binders in a
+permutation functions is that they allow us to rename just the bound atoms in a
 term, without changing anything else.
 Having the auxiliary permutation function in place, we can now solve all remaining cases.
 For the @{text "Let\<^sup>\<alpha>"} term-constructor, for example, we can by Property \ref{avoiding}
 obtain a @{text "\<pi>"} such that
 We have also not yet played with other binding modes. For example we can
 imagine that there is need for a binding mode where instead of usual lists,
 we abstract lists of distinct elements (the corresponding type @{text
 "dlist"} already exists in the library of Isabelle/HOL). We expect the
-presented work can be easily extended to accommodate such binding modes.\medskip
+presented work can be extended to accommodate such binding modes.\medskip
 \noindent
 {\bf Acknowledgements:} We are very grateful to Andrew Pitts for many
 discussions about Nominal Isabelle. We thank Peter Sewell for making the
 informal notes \cite{SewellBestiary} available to us and also for patiently

changeset 3039	3941fa3f179a
parent 3038	af6eda1fb91f
child 3041	119b9f7e34c0