# HG changeset patch # User Christian Urban # Date 1273957566 -3600 # Node ID 8beda0b4e35a4a5cd38af285f8f0e3453b5a73ef # Parent dff8bd92281281c6b4ce57f4dcc017089f98b758 tuned paper diff -r dff8bd922812 -r 8beda0b4e35a Paper/Paper.thy --- a/Paper/Paper.thy Fri May 14 21:18:34 2010 +0100 +++ b/Paper/Paper.thy Sat May 15 22:06:06 2010 +0100 @@ -253,7 +253,7 @@ Our insistence on reasoning with alpha-equated terms comes from the wealth of experience we gained with the older version of Nominal Isabelle: - for non-trivial properties, reasoning about alpha-equated terms is much + for non-trivial properties, reasoning with alpha-equated terms is much easier than reasoning with raw terms. The fundamental reason for this is that the HOL-logic underlying Nominal Isabelle allows us to replace ``equals-by-equals''. In contrast, replacing @@ -295,7 +295,7 @@ \noindent We take as the starting point a definition of raw terms (defined as a datatype in Isabelle/HOL); identify then the alpha-equivalence classes in - the type of sets of raw terms according to our alpha-equivalence relation + the type of sets of raw terms according to our alpha-equivalence relation, and finally define the new type as these alpha-equivalence classes (non-emptiness is satisfied whenever the raw terms are definable as datatype in Isabelle/HOL and the property that our relation for alpha-equivalence is @@ -495,8 +495,8 @@ @{thm (rhs) fresh_star_def[no_vars]}. A striking consequence of these definitions is that we can prove without knowing anything about the structure of @{term x} that - swapping two fresh atoms, say @{text a} and @{text b}, leave - @{text x} unchanged. + swapping two fresh atoms, say @{text a} and @{text b}, leaves + @{text x} unchanged: \begin{property}\label{swapfreshfresh} @{thm[mode=IfThen] swap_fresh_fresh[no_vars]} @@ -933,12 +933,13 @@ \noindent Similarly for the other binding modes. + + There are a few restrictions we need to impose: First, a body can only occur in \emph{one} binding clause of a term constructor. - For binders we distinguish between \emph{shallow} and \emph{deep} binders. Shallow binders are just labels. The - restrictions we need to impose on them are that in case of + restriction we need to impose on them is that in case of \isacommand{bind\_set} and \isacommand{bind\_res} the labels must either refer to atom types or to sets of atom types; in case of \isacommand{bind} the labels must refer to atom types or lists of atom types. @@ -967,8 +968,8 @@ \noindent Note that for @{text lam} it does not matter which binding mode we use. The reason is that - we bind only a single @{text name}. However, having \isacommand{bind\_set}, or even - \isacommand{bind}, in the second + we bind only a single @{text name}. However, having \isacommand{bind\_set} or + \isacommand{bind} 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. @@ -1006,63 +1007,26 @@ \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 @{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. + 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 @{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 more than one binding function for one binder. Consider for example the - term-constructors: - + As said above, for deep binders we allow binding clauses such as + % \begin{center} \begin{tabular}{ll} - @{text "Foo\<^isub>1 p::pat t::trm"} & - \isacommand{bind} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\ - @{text "Foo\<^isub>2 x::name p::pat t::trm"} & - \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t}, ***\\ - \end{tabular} - \end{center} - - \noindent - In the first case the intention is to bind all atoms from the pattern @{text p} in @{text t} - and also all atoms from @{text q} in @{text t}. Unfortunately, we have no way - to determine whether the binder came from the binding function @{text - "bn(p)"} or @{text "bn(q)"}. Similarly in the second case. The reason why - we must exclude such specifications is that they cannot be represented by - the general binders described in Section \ref{sec:binders}. However - the following two term-constructors are allowed - - \begin{center} - \begin{tabular}{ll} - @{text "Bar\<^isub>1 p::pat t::trm s::trm"} & - \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "t s"}\\ - @{text "Bar\<^isub>2 p::pat t::trm"} & + @{text "Bar p::pat t::trm"} & \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p t"}\\ \end{tabular} \end{center} \noindent - since there is no overlap of binders. Unlike shallow binders, we restrict deep - binders to occur in only one binding clause. Therefore @{text "Bar\<^isub>2"} cannot - be reformulated as - - \begin{center} - \begin{tabular}{ll} - @{text "Bar\<^isub>3 p::pat t::trm"} & - \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p"}, - \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "t"}\\ - \end{tabular} - \end{center} - - Note that in the @{text "Bar\<^isub>2"}, we wrote \isacommand{bind}~@{text - "bn(p)"}~\isacommand{in}~@{text "p.."}. Whenever such a binding clause - is present, where the argument in the binder also occurs in the body, we will - call the corresponding binder \emph{recursive}. To see the - purpose of such recursive binders, compare ``plain'' @{text "Let"}s and - @{text "Let_rec"}s in the following specification: + where the argument of the deep binder is also in the body. We call such + binders \emph{recursive}. To see the purpose of such recursive binders, + compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s in the following + specification: % \begin{equation}\label{letrecs} \mbox{% @@ -1088,6 +1052,22 @@ inside the assignment. This difference has consequences for the free-variable function and alpha-equivalence relation, which we are going to describe in the rest of this section. + + The restriction we have to impose on deep binders is that we cannot have + more than one binding function for one binder. So we exclude: + + \begin{center} + \begin{tabular}{ll} + @{text "Baz p::pat t::trm"} & + \isacommand{bind} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\ + \end{tabular} + \end{center} + + \noindent + The reason why we must exclude such specifications is that they cannot be + represented by the general binders described in Section + \ref{sec:binders}. Unlike shallow binders, we restrict deep binders to occur + in only one binding clause. We also need to restrict the form of the binding functions. As will shortly become clear, we cannot return an atom in a binding function that is also @@ -1104,7 +1084,7 @@ (case @{text PTup}). This restriction will simplify some automatic proofs later on. - In order to simplify some later definitions, we shall assume specifications + In order to simplify later definitions, we shall assume specifications of term-calculi are \emph{completed}. By this we mean that for every argument of a term-constructor that is \emph{not} already part of a binding clause, we add implicitly a special \emph{empty} binding