# HG changeset patch # User Christian Urban # Date 1316622444 -7200 # Node ID 3941fa3f179aef026bb39d2c68c6892bde164bf4 # Parent af6eda1fb91fefc067228a637e74280e2ac6ab86 more polishing diff -r af6eda1fb91f -r 3941fa3f179a LMCS-Paper/Paper.thy --- a/LMCS-Paper/Paper.thy Wed Sep 21 15:18:32 2011 +0200 +++ b/LMCS-Paper/Paper.thy Wed Sep 21 18:27:24 2011 +0200 @@ -2177,7 +2177,7 @@ 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 @@ -2207,7 +2207,7 @@ \noindent They are stronger in the sense that they allow us to assume in the @{text "Lam\<^sup>\"} and @{text "Let_pat\<^sup>\"} 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 @@ -2234,7 +2234,7 @@ 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>\ 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 @@ -2310,7 +2310,7 @@ that @{text "\"} only renames atoms that become bound. In this way @{text "\"} does not affect @{text "\\\<^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 "\ \ x\<^isub>1"} applies to all attoms in @{text "x\<^isub>1"}. To avoid this + permutation operation @{text "\ \ x\<^isub>1"} applies to all atoms in @{text "x\<^isub>1"}. To avoid this we introduce an auxiliary permutation operations, written @{text "_ \\<^bsub>bn\<^esub> _"}, for deep binders that only permutes bound atoms (or more precisely the atoms specified by the @{text "bn"}-functions) and leaves @@ -2336,7 +2336,7 @@ \noindent Using again the quotient package we can lift the auxiliary permutation operations @{text "_ \\<^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>\"} and auxiliary equivalence @{text "\\\<^bsub>bn\<^esub>"} @@ -2355,7 +2355,7 @@ is equivalent to first permuting the binders and then calculating the bound atoms. The second states that @{text "_ \\\<^bsub>bn\<^esub> _"} preserves @{text "\\\<^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. @@ -2654,7 +2654,7 @@ 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 diff -r af6eda1fb91f -r 3941fa3f179a LMCS-Paper/document/root.bib --- a/LMCS-Paper/document/root.bib Wed Sep 21 15:18:32 2011 +0200 +++ b/LMCS-Paper/document/root.bib Wed Sep 21 18:27:24 2011 +0200 @@ -1,8 +1,8 @@ @inproceedings{pfenningsystem, - author = "Frank Pfenning and Carsten Sch{\"u}rmann", - title = "System Description: Twelf---{A} Meta-Logical - Framework for Deductive Systems", - booktitle = "Automated Deduction", + author = "F.~Pfenning and C.~Sch{\"u}rmann", + title = "{S}ystem {D}escription: {T}welf - {A} {M}eta-{L}ogical + {F}ramework for {D}eductive {S}ystems", + booktitle = "Proc.~of the 16th International Conference on Automated Deduction (CADE)", series = "LNAI", volume = 1632, pages = "202--206", @@ -38,8 +38,8 @@ @InProceedings{UrbanKaliszyk11, author = {C.~Urban and C.~Kaliszyk}, - title = {General Bindings and Alpha-Equivalence in Nominal Isabelle}, - booktitle = {Proceedings of the 20th European Symposium on Programming (ESOP)}, + title = {{G}eneral {B}indings and {A}lpha-{E}quivalence in {N}ominal {I}sabelle}, + booktitle = {Proc.~of the 20th European Symposium on Programming (ESOP)}, pages = {480-500}, year = {2011}, volume = {6602}, @@ -50,14 +50,14 @@ @inproceedings{KaliszykUrban11, author = {C.~Kaliszyk and C.~Urban}, title = {{Q}uotients {R}evisited for {I}sabelle/{HOL}}, - booktitle = {Proc.~of the 26th ACM Symposium On Applied Computing (SAC)}, + booktitle = {Proc.~of the 26th ACM Symposium on Applied Computing (SAC)}, year = {2011}, pages = {1639--1644} } @InProceedings{cheney05a, author = {J.~Cheney}, - title = {{S}crap your {N}ameplate ({F}unctional {P}earl)}, + title = {{S}crap {Y}our {N}ameplate ({F}unctional {P}earl)}, booktitle = {Proc.~of the 10th International Conference on Functional Programming (ICFP)}, pages = {180--191}, year = {2005} @@ -137,7 +137,7 @@ @inproceedings{cheney05, author = {J.~Cheney}, - title = {{T}oward a {G}eneral {T}heory of {N}ames: {B}inding and {S}cope}, + title = {{T}owards a {G}eneral {T}heory of {N}ames: {B}inding and {S}cope}, booktitle = {Proc.~of the 3rd ACM Workshop on Mechanized Reasoning about Languages with Variable Binding and Names (MERLIN)}, year = {2005}, @@ -191,7 +191,7 @@ author = {F.~Pottier}, title = {{A}n {O}verview of {C$\alpha$ml}}, year = {2006}, - booktitle = {ACM Workshop on ML}, + booktitle = {Proc.~of the ACM Workshop on ML}, pages = {27--52}, volume = {148}, number = {2},