diff -r 47e2e91705f3 -r 774d631726ad Paper/Paper.thy --- a/Paper/Paper.thy Tue Apr 27 19:01:22 2010 +0200 +++ b/Paper/Paper.thy Tue Apr 27 19:51:35 2010 +0200 @@ -921,7 +921,7 @@ ``\isacommand{bind}-part'' will be called \emph{binders}. In contrast to Ott, we allow multiple labels in binders and bodies. For example - we permit binding clauses as follows: + we have binding clauses of the form: \begin{center} \begin{tabular}{ll} @@ -931,18 +931,20 @@ \end{center} \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. A binder, in contrast, may - occur in several binding clauses, but cannot occur as a body. + \emph{one} binding clause of a term constructor. - In addition we distinguish between \emph{shallow} and \emph{deep} - binders. Shallow binders are of the form \isacommand{bind}\; {\it labels}\; + For binders we distinguish between \emph{shallow} and \emph{deep} binders. + Shallow binders are of the form \isacommand{bind}\; {\it labels}\; \isacommand{in}\; {\it labels'} (similar for the other two modes). The - restriction we impose on shallow binders is that the {\it labels} must either - refer to atom types or to finite sets 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: + 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 + 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: \begin{center} \begin{tabular}{@ {}cc@ {}} @@ -965,7 +967,8 @@ \noindent Note that in this specification @{text "name"} refers to an atom type, and - @{text "fset"} to the type of finite sets. + @{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 the atoms in one argument of the term-constructor, which can be bound in @@ -1005,16 +1008,6 @@ coerces a name into the generic atom type of Nominal Isabelle \cite{HuffmanUrban10}. This allows us to treat binders of different atom type uniformly. - As will shortly become clear, we cannot return an atom in a binding function - that is also bound in the corresponding term-constructor. That means in the - example above that the term-constructors @{text PVar} and @{text PTup} may not have a - binding clause. In the version of Nominal Isabelle described here, we also adopted - the restriction from the Ott-tool that binding functions can only return: - the empty set or empty list (as in case @{text PNil}), a singleton set or singleton - list containing an atom (case @{text PVar}), or unions of atom sets or appended atom - lists (case @{text PTup}). This restriction will simplify definitions and - proofs later on. - The most drastic restriction we have to impose on deep binders is that we cannot have ``overlapping'' deep binders. Consider for example the term-constructors: @@ -1047,11 +1040,22 @@ \end{center} \noindent - since there is no overlap of binders. + 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 last example we wrote \isacommand{bind}~@{text - "bn(p)"}~\isacommand{in}~@{text "p.."}. Whenever such a binding clause is - present, we will call the corresponding binder \emph{recursive}. To see the + 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: % @@ -1079,8 +1083,23 @@ 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. - - In order to simplify some definitions, we shall assume specifications + + 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 + bound in the corresponding term-constructor. That means in the example + \eqref{letpat} that the term-constructors @{text PVar} and @{text PTup} may + not have a binding clause (all arguments are used to define @{text "bn"}). + In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons} + may have binding clause involving the argument @{text t} (the only one that + is \emph{not} used in the definition of the binding function). In the version of + Nominal Isabelle described here, we also adopted the restriction from the + Ott-tool that binding functions can only return: the empty set or empty list + (as in case @{text PNil}), a singleton set or singleton list containing an + atom (case @{text PVar}), or unions of atom sets or appended atom lists + (case @{text PTup}). This restriction will simplify some automatic proofs + later on. + + In order to simplify some 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 @@ -1102,7 +1121,7 @@ \noindent The point of completion is that we can make definitions over the binding - clauses and be sure to capture all arguments of a term constructor. + clauses and be sure to have captured all arguments of a term constructor. Having dealt with all syntax matters, the problem now is how we can turn specifications into actual type definitions in Isabelle/HOL and then @@ -1142,7 +1161,7 @@ we have that % \begin{equation}\label{ceqvt} - @{text "p \ (C x\<^isub>1 \ x\<^isub>n) = C (p \ x\<^isub>1) \ (p \ x\<^isub>n)"} + @{text "p \ (C z\<^isub>1 \ z\<^isub>n) = C (p \ z\<^isub>1) \ (p \ z\<^isub>n)"} \end{equation} The first non-trivial step we have to perform is the generation free-variable @@ -1187,28 +1206,32 @@ collect all atoms that are not bound), because of our rather complicated binding mechanisms their definitions are somewhat involved. Given a term-constructor @{text "C"} of type @{text ty} and some associated binding - clauses @{text bcs}, the result of the @{text "fv_ty (C x\<^isub>1 \ x\<^isub>n)"} will be + clauses @{text bcs}, the result of the @{text "fv_ty (C z\<^isub>1 \ z\<^isub>n)"} will be the union of the values, @{text v}, calculated by the rules for empty, shallow and deep binding clauses: % - \begin{equation}\label{deepbinder} + \begin{equation}\label{deepbinderA} \mbox{% \begin{tabular}{c@ {\hspace{2mm}}p{7.4cm}} \multicolumn{2}{@ {}l}{\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\ $\bullet$ & @{term "v = fv_ty y"} provided @{text "y"} is of type @{text "ty"}\smallskip\\ - + % \multicolumn{2}{@ {}l}{\isacommand{bind}~@{text "x\<^isub>1\x\<^isub>n"}~\isacommand{in}~@{text "y\<^isub>1\y\<^isub>m"}:}\\ - $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \ \ \ fv_ty\<^isub>m y\<^isub>m)"}\\ - & \hspace{15mm}@{text "- (fv_aty\<^isub>1 x\<^isub>1 \ \ \ fv_aty\<^isub>n x\<^isub>n)"}\\ + $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \ .. \ fv_ty\<^isub>m y\<^isub>m)"}\\ + & \hspace{15mm}@{text "- (fv_aty\<^isub>1 x\<^isub>1 \ .. \ fv_aty\<^isub>n x\<^isub>n)"}\\ & provided the bodies @{text "y"}$_{1..m}$ are of type @{text "ty"}$_{1..m}$ and the binders @{text "x"}$_{1..n}$ of atomic types @{text "aty"}$_{1..n}$\smallskip\\ - + \end{tabular}} + \end{equation} + \begin{equation}\label{deepbinderB} + \mbox{% + \begin{tabular}{c@ {\hspace{2mm}}p{7.4cm}} \multicolumn{2}{@ {}l}{\isacommand{bind}~@{text "bn x"}~\isacommand{in}~@{text "y\<^isub>1\y\<^isub>m"}:}\\ - $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \ \ \ fv_ty\<^isub>m y\<^isub>m) - set (bn x) \ (fv_bn x)"}\\ - $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \ \ \ fv_ty\<^isub>m y\<^isub>m) - set (bn x)"}\\ + $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \ .. \ fv_ty\<^isub>m y\<^isub>m) - set (bn x) \ (fv_bn x)"}\\ + $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \ .. \ fv_ty\<^isub>m y\<^isub>m) - set (bn x)"}\\ & provided the @{text "y"}$_{1..m}$ are of type @{text "ty"}$_{1..m}$; the first - clause applies for @{text x} being a non-recursive deep binder, the - second for a recursive deep binder + clause applies for @{text x} being a non-recursive deep binder (that is + @{text "x \ y"}$_{1..m}$), the second for a recursive deep binder \end{tabular}} \end{equation} @@ -1217,8 +1240,8 @@ binder, we have to add all atoms that are left unbound by the binding function @{text "bn"}. For this we define the function @{text "fv_bn"}. Assume for the constructor @{text "C"} the binding function is of the form @{text - "bn\<^isub>j (C x\<^isub>1 \ x\<^isub>n) = rhs"}. We again define a value - @{text v} which is exactly as in \eqref{deepbinder} for shallow and deep + "bn (C z\<^isub>1 \ z\<^isub>n) = rhs"}. We again define a value + @{text v} which is exactly as in \eqref{deepbinderA}/\eqref{deepbinderB} for shallow and deep binding clauses, except for empty binding clauses are defined as follows: % \begin{equation}\label{bnemptybinder}