# HG changeset patch # User Christian Urban # Date 1273768888 -3600 # Node ID abd46dfc021246b73e0022987f7622f91b0c51b4 # Parent fc42d4a06c06d2a4a2c56f7c977451e1cc805ef2 tuned the paper diff -r fc42d4a06c06 -r abd46dfc0212 Paper/Paper.thy --- a/Paper/Paper.thy Thu May 13 16:09:34 2010 +0100 +++ b/Paper/Paper.thy Thu May 13 17:41:28 2010 +0100 @@ -344,8 +344,8 @@ 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 - for alpha-equated terms. + automate these proofs and as a result can automatically establish a reasoning + 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 @@ -563,7 +563,7 @@ @{text "x R y"} \;\;implies\;\; @{text "(p \ x) R (p \ 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 @@ -590,7 +590,7 @@ fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders @{text as} in @{text x}, because @{term "p \ 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. @@ -610,7 +610,7 @@ 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) \ \"}. 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 @@ -737,7 +737,8 @@ This lemma allows us to use our quotient package and introduce new types @{text "\ abs_set"}, @{text "\ abs_res"} and @{text "\ abs_list"} representing alpha-equivalence classes of pairs of type - @{text "(atom set) \ \"} (in the first two cases) and of type @{text "(atom list) \ \"}. + @{text "(atom set) \ \"} (in the first two cases) and of type @{text "(atom list) \ \"} + (in the third case). The elements in these types will be, respectively, written as: \begin{center} @@ -776,7 +777,7 @@ \noindent and also % - \begin{equation} + \begin{equation}\label{absperm} @{thm permute_Abs[no_vars]} \end{equation} @@ -797,7 +798,7 @@ \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]} @@ -890,7 +891,7 @@ \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 @@ -941,7 +942,7 @@ 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: @@ -966,11 +967,15 @@ \end{center} \noindent - Note that in this specification @{text "name"} refers to an atom type, and - @{text "fset"} to the type of finite sets. Shallow binders can occur in the - binding part of several binding clauses. - - A \emph{deep} binder uses an auxiliary binding function that ``picks'' out + Note that for @{text lam} we have a choice which mode we use. The reason is that + we bind only a single @{text name}. Having \isacommand{bind\_set} 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. + + 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). @@ -1004,7 +1009,8 @@ \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.