nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:a3ef7fba983f
+:0c3c66f5c0e7
 \noindent
 where no clause for variables is given. Arguably, such specifications make
 some sense in the context of Coq's type theory (which Ott supports), but not
 at all in a HOL-based environment where every datatype must have a non-empty
-set-theoretic model.
+set-theoretic model \cite{Berghofer99}.
 Another reason is that we establish the reasoning infrastructure
 for alpha-\emph{equated} terms. In contrast, Ott produces  a reasoning
 infrastructure in Isabelle/HOL for
 \emph{non}-alpha-equated, or ``raw'', terms. While our alpha-equated terms
 \begin{equation}\label{halftwo}
 @{thm (concl) supp_abs_subset1(1)[no_vars]}
 \end{equation}
 \noindent
-since for finite sets, @{text "S"}, we have
+since for finite sets, @{text "S"}, we have @{thm (concl) supp_finite_atom_set[no_vars]}.
-@{thm (concl) supp_finite_atom_set[no_vars]}).
+Finally taking \eqref{halfone} and \eqref{halftwo} together provides us with a proof
-Finally taking \eqref{halfone} and \eqref{halftwo} provides us with a proof
+of Theorem~\ref{suppabs}. The point of these properties of abstractions is that we
-of Theorem~\ref{suppabs}. The point of these general lemmas about abstractions is that we
+can define and prove them aconveniently on the Isabelle/HOL level,
-can define and prove properties about them conveniently on the Isabelle/HOL level,
+but also use them in what follows next when we deal with binding in
-but also use them in what follows next when we deal with binding in specifications
+specifications of term-calculi.
-of term-calculi.
 *}
 section {* Alpha-Equivalence and Free Variables\label{sec:alpha} *}
 text {*
 Our choice of syntax for specifications of term-calculi is influenced by the existing
-datatype package of Isabelle/HOL and by the syntax of the Ott-tool
+datatype package of Isabelle/HOL \cite{Berghofer99} and by the syntax of the Ott-tool
 \cite{ott-jfp}. A specification is a collection of (possibly mutual
 recursive) type declarations, say @{text "ty"}$^\alpha_1$, \ldots,
 @{text ty}$^\alpha_n$, and an associated collection
 of binding functions, say @{text bn}$^\alpha_1$, \ldots, @{text
 bn}$^\alpha_m$. The syntax in Nominal Isabelle for such specifications is
 \noindent
 whereby some of the @{text ty}$'_{1..l}$ (or their components) are contained in the collection
 of @{text ty}$^\alpha_{1..n}$ declared in \eqref{scheme}. In this case we will call the
 corresponding argument a \emph{recursive argument}.  The labels annotated on
-the types are optional and can be used in the (possibly empty) list of
+the types are optional. Their purpose is to be used in the (possibly empty) list of
-\emph{binding clauses}.  These clauses indicate the binders and their scope of
+\emph{binding clauses}, which indicate the binders and their scope
 in a term-constructor.  They come in three \emph{modes}:
 \begin{center}
 \begin{tabular}{l}
 \noindent
 The first mode is for binding lists of atoms (the order of binders matters); the second is for sets
 of binders (the order does not matter, but the cardinality does) and the last is for
 sets of binders (with vacuous binders preserving alpha-equivalence).
-In addition we distinguish between \emph{shallow} binders and \emph{deep}
+In addition we distinguish between \emph{shallow} and \emph{deep}
 binders.  Shallow binders are of the form \isacommand{bind}\; {\it label}\;
 \isacommand{in}\; {\it label'} (similar for the other two modes). The
 restriction we impose on shallow binders is that the {\it label} must either
 refer to a type that is an atom type or to a type that is a finite set or
 list of an atom type. Two examples for the use of shallow binders are the
 type-schemes, where a finite set of names is bound:
 \begin{center}
 \begin{tabular}{@ {}cc@ {}}
 \begin{tabular}{@ {}l@ {\hspace{-1mm}}}
-\isacommand{nominal\_datatype} {\it lam} =\\
+\isacommand{nominal\_datatype} @{text lam} =\\
-\hspace{5mm}\phantom{$\mid$} Var\;{\it name}\\
+\hspace{5mm}\phantom{$\mid$}~@{text "Var name"}\\
-\hspace{5mm}$\mid$ App\;{\it lam}\;{\it lam}\\
+\hspace{5mm}$\mid$~@{text "App lam lam"}\\
-\hspace{5mm}$\mid$ Lam\;{\it x::name}\;{\it t::lam}\\
+\hspace{5mm}$\mid$~@{text "Lam x::name t::lam"}\\
-\hspace{21mm}\isacommand{bind} {\it x} \isacommand{in} {\it t}\\
+\hspace{21mm}\isacommand{bind} @{text x} \isacommand{in} @{text t}\\
 \end{tabular} &
 \begin{tabular}{@ {}l@ {}}
-\isacommand{nominal\_datatype} {\it ty} =\\
+\isacommand{nominal\_datatype}~@{text ty} =\\
-\hspace{5mm}\phantom{$\mid$} TVar\;{\it name}\\
+\hspace{5mm}\phantom{$\mid$}~@{text "TVar name"}\\
-\hspace{5mm}$\mid$ TFun\;{\it ty}\;{\it ty}\\
+\hspace{5mm}$\mid$~@{text "TFun ty ty"}\\
-\isacommand{and} {\it tsc} = All\;{\it xs::(name fset)}\;{\it T::ty}\\
+\isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}\\
-\hspace{24mm}\isacommand{bind\_res} {\it xs} \isacommand{in} {\it T}\\
+\hspace{24mm}\isacommand{bind\_res} @{text xs} \isacommand{in} @{text T}\\
 \end{tabular}
 \end{tabular}
 \end{center}
 \noindent
 If we have shallow binders that ``share'' a body, for instance $t$ in
 the following term-constructor
 \begin{center}
 \begin{tabular}{ll}
-\it {\rm Foo} x::name y::name t::lam & \it
+@{text "Foo x::name y::name t::lam"} &
-\isacommand{bind}\;x\;\isacommand{in}\;t,\;
+\isacommand{bind} @{text x} \isacommand{in} @{text t},\;
-\isacommand{bind}\;y\;\isacommand{in}\;t
+\isacommand{bind} @{text y} \isacommand{in} @{text t}
 \end{tabular}
 \end{center}
 \noindent
 then we have to make sure the modes of the binders agree. We cannot
 the scheme shown in \eqref{scheme}. For example for a calculus containing lets
 with tuple patterns, you might specify
 \begin{center}
 \begin{tabular}{l}
-\isacommand{nominal\_datatype} {\it trm} =\\
+\isacommand{nominal\_datatype} @{text trm} =\\
-\hspace{5mm}\phantom{$\mid$} Var\;{\it name}\\
+\hspace{5mm}\phantom{$\mid$}~@{term "Var name"}\\
-\hspace{5mm}$\mid$ App\;{\it trm}\;{\it trm}\\
+\hspace{5mm}$\mid$~@{term "App trm trm"}\\
-\hspace{5mm}$\mid$ Lam\;{\it x::name}\;{\it t::trm}
+\hspace{5mm}$\mid$~@{text "Lam x::name t::trm"}
-\;\;\isacommand{bind} {\it x} \isacommand{in} {\it t}\\
+\;\;\isacommand{bind} @{text x} \isacommand{in} @{text t}\\
-\hspace{5mm}$\mid$ Let\;{\it p::pat}\;{\it trm}\; {\it t::trm}
+\hspace{5mm}$\mid$~@{text "Let p::pat trm t::trm"}
-\;\;\isacommand{bind} {\it bn(p)} \isacommand{in} {\it t}\\
+\;\;\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t}\\
-\isacommand{and} {\it pat} =\\
+\isacommand{and} @{text pat} =\\
-\hspace{5mm}\phantom{$\mid$} PNil\\
+\hspace{5mm}\phantom{$\mid$}~@{text PNil}\\
-\hspace{5mm}$\mid$ PVar\;{\it name}\\
+\hspace{5mm}$\mid$~@{text "PVar name"}\\
-\hspace{5mm}$\mid$ PTup\;{\it pat}\;{\it pat}\\
+\hspace{5mm}$\mid$~@{text "PTup pat pat"}\\
-\isacommand{with} {\it bn::pat $\Rightarrow$ atom list}\\
+\isacommand{with}~@{text "bn::pat \<Rightarrow> atom list"}\\
-\isacommand{where} $\textit{bn}(\textrm{PNil}) = []$\\
+\isacommand{where}~@{text "bn(PNil) = []"}\\
-\hspace{5mm}$\mid$ $\textit{bn}(\textrm{PVar}\;x) = [\textit{atom}\; x]$\\
+\hspace{5mm}$\mid$~@{text "bn(PVar x) = [atom x]"}\\
-\hspace{5mm}$\mid$ $\textit{bn}(\textrm{PTup}\;p_1\;p_2) = \textit{bn}(p_1)\; @\;\textit{bn}(p_2)$\\
+\hspace{5mm}$\mid$~@{text "bn(PTup p\<^isub>1 p\<^isub>2) = bn(p\<^isub>1) @ bn(p\<^isub>2)"}\\
 \end{tabular}
 \end{center}
 \noindent
 In this specification the function @{text "bn"} determines which atoms of @{text  p} are
-bound in the argument @{text "t"}. Note that the second last clause the function @{text "atom"}
+bound in the argument @{text "t"}. Note that in the second last clause the function @{text "atom"}
 coerces a name into the generic atom type of Nominal Isabelle. 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
 binding clause.  In the present version of Nominal Isabelle, we also adopted
 the restriction from the Ott-tool that binding functions can only return:
 the empty set or empty list (as in case PNil), a singleton set or singleton
 list containing an atom (case PVar), or unions of atom sets or appended atom
 lists (case PTup). This restriction will simplify proofs later on.
-The the most drastic restriction we have to impose on deep binders is that
+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:
 \begin{center}
 \begin{tabular}{ll}
-\it {\rm Foo} p::pat q::pat t::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;t,\;
+@{text "Foo p::pat q::pat t::trm"} &
-\isacommand{bind}\;bn(q)\;\isacommand{in}\;t\\
+\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t},\;
-\it {\rm Foo}$'$x::name p::pat t::trm & \it \it \isacommand{bind}\;x\;\isacommand{in}\;t,\;
+\isacommand{bind} @{text "bn(q)"} \isacommand{in} @{text t}\\
-\isacommand{bind}\;bn(p)\;\isacommand{in}\;t
+@{text "Foo' x::name p::pat t::trm"} &
+\isacommand{bind} @{text x} \isacommand{in} @{text t},\;
+\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t}
 \end{tabular}
 \end{center}
 \noindent
 the general binders described in Section \ref{sec:binders}. However
 the following two term-constructors are allowed
 \begin{center}
 \begin{tabular}{ll}
-\it {\rm Bar} p::pat t::trm s::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;t,\;
+@{text "Bar p::pat t::trm s::trm"} &
-\isacommand{bind}\;bn(p)\;\isacommand{in}\;s\\
+\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t},\;
-\it {\rm Bar}$'$p::pat t::trm &  \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;p,\;
+\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text s}\\
-\isacommand{bind}\;bn(p)\;\isacommand{in}\;t\\
+@{text "Bar' 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}
 \noindent
 since there is no overlap of binders.
 Note that in the last example we wrote {\it\isacommand{bind}\;bn(p)\;\isacommand{in}\;p}.
 Whenever such a binding clause is present, we will call the binder \emph{recursive}.
-To see the purpose for this, consider ``plain'' Lets and Let\_recs:
+To see the purpose for this, compare ``plain'' Lets and Let\_recs:
 \begin{center}
 \begin{tabular}{@ {}l@ {}}
 \isacommand{nominal\_datatype} {\it trm} =\\
 \hspace{5mm}\phantom{$\mid$}\ldots\\
 establish a reasoning infrastructure for them. Because of the problem
 Pottier and Cheney pointed out, we cannot in general re-arrange arguments of
 term-constructors so that binders and their bodies are next to each other, and
 then use the type constructors @{text "abs_set"}, @{text "abs_res"} and
 @{text "abs_list"} from Section \ref{sec:binders}. Therefore we will first
-extract datatype definitions from the specification and then define an
+extract datatype definitions from the specification and then define
-alpha-equivalence relation over them.
+independently an alpha-equivalence relation over them.
 The datatype definition can be obtained by just stripping off the
 binding clauses and the labels on the types. We also have to invent
 new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}
-given by user. In our implementation we just use an affix like
+given by user. In our implementation we just use an affix @{text "_raw"}.
+For the purpose of the paper we just use superscripts to indicate a
-\begin{center}
+notion defined over alpha-equivalence classes and leave out the superscript
-@{text "ty\<^sup>\<alpha> \<mapsto> ty_raw"} \hspace{7mm} @{text "C\<^sup>\<alpha> \<mapsto> C_raw"}
+for the corresponding notion on the ``raw'' level. So for example:
+\begin{center}
+@{text "ty\<^sup>\<alpha> \<mapsto> ty"} \hspace{7mm} @{text "C\<^sup>\<alpha> \<mapsto> C"}
 \end{center}
 \noindent
 The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are
 non-empty and the types in the constructors only occur in positive
-position (see \cite{} for an indepth explanation of the datatype package
+position (see \cite{Berghofer99} for an indepth explanation of the datatype package
 in Isabelle/HOL). We then define the user-specified binding
 functions by primitive recursion over the raw datatypes. We can also
 easily define a permutation operation by primitive recursion so that for each
-term constructor @{text "C_raw ty\<^isub>1 \<dots> ty\<^isub>n"} we have that
+term constructor @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"} we have that
 \begin{center}
-@{text "p \<bullet> (C_raw x\<^isub>1 \<dots> x\<^isub>n) \<equiv> C_raw (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"}
+@{text "p \<bullet> (C x\<^isub>1 \<dots> x\<^isub>n) \<equiv> C (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"}
 \end{center}
-\noindent
+% TODO: we did not define permutation types
-From this definition we can easily show that the raw datatypes are
+%\noindent
-all permutation types (Def ??) by a simple structural induction over
+%From this definition we can easily show that the raw datatypes are
-the @{text "ty_raw"}s.
+%all permutation types (Def ??) by a simple structural induction over
+%the @{text "ty"}s.
 The first non-trivial step we have to perform is the generation free-variable
 functions from the specifications. Given types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}
 we need to define the free-variable functions
 \noindent
 The basic idea behind these free-variable functions is to collect all atoms
 that are not bound in a term constructor, but because of the rather
 complicated binding mechanisms the details are somewhat involved.
-Given a term-constructor @{text "C_raw ty\<^isub>1 \<dots> ty\<^isub>n"}, of type @{text ty} together with
+Given a term-constructor @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}, of type @{text ty} together with
-some  binding clauses, the function @{text "fv_ty (C_raw x\<^isub>1 \<dots> x\<^isub>n)"} will be
+some  binding clauses, the function @{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be
 the union of the values defined below for each argument, say @{text "x\<^isub>i"} with type @{text "ty\<^isub>i"}.
 From the binding clause of this term constructor, we can determine whether the
 argument @{text "x\<^isub>i"} is a shallow or deep binder, and in the latter case also
 whether it is a recursive or non-recursive of a binder. In these cases the value is:
 function is to compute all the free atoms under this binding
 function. So given that @{text "bn"} is a binding function for type
 @{text "ty\<^isub>i"} it will be the same as @{text "fv_ty\<^isub>i"} with the
 omission of the arguments present in @{text "bn"}.
-For a binding function clause @{text "bn (C_raw x\<^isub>1 \<dots> x\<^isub>n) = rhs"},
+For a binding function clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"},
 we define @{text "fv_bn"} to be the union of the values calculated
 for @{text "x\<^isub>j"} as follows:
 \begin{center}
 \begin{tabular}{cp{7cm}}
 functions for types @{text "bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> \<dots> \<dots> bn\<^isub>m :: ty\<^isub>i\<^isub>m \<Rightarrow> \<dots>"} we need to define
 \begin{center}
 @{text "\<approx>bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> ty\<^isub>i\<^isub>1 \<Rightarrow> bool \<dots> \<approx>bn\<^isub>n :: ty\<^isub>i\<^isub>m \<Rightarrow> ty\<^isub>i\<^isub>m \<Rightarrow> bool"}
 \end{center}
-Given a term-constructor @{text "C_raw ty\<^isub>1 \<dots> ty\<^isub>n"}, of a type @{text ty}, two instances
+Given a term-constructor @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}, of a type @{text ty}, two instances
-of this constructor are alpha-equivalent @{text "C_raw x\<^isub>1 \<dots> x\<^isub>n \<approx> C_raw y\<^isub>1 \<dots> y\<^isub>n"} if there
+of this constructor are alpha-equivalent @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx> C y\<^isub>1 \<dots> y\<^isub>n"} if there
 exist permutations @{text "\<pi>\<^isub>1 \<dots> \<pi>\<^isub>p"} (one for each bound argument) such that
 the conjunction of equivalences defined below for each argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} holds.
 For an argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} this holds if:
 \begin{center}
 The alpha-equivalence relations for binding functions are similar to the alpha-equivalences
 for their respective types, the difference is that they ommit checking the arguments that
 are bound. We assumed that there are no bindings in the type on which the binding function
 is defined so, there are no permutations involved. For a binding function clause
-@{text "bn (C_raw x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, two instances of the constructor are equivalent
+@{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, two instances of the constructor are equivalent
-@{text "C_raw x\<^isub>1 \<dots> x\<^isub>n \<approx> C_raw y\<^isub>1 \<dots> y\<^isub>n"} if:
+@{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx> C y\<^isub>1 \<dots> y\<^isub>n"} if:
 \begin{center}
 \begin{tabular}{cp{7cm}}
 $\bullet$ & @{text "x\<^isub>j"} is not of a type being defined and occurs in @{text "rhs"}\\
 $\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} provided @{text "x\<^isub>j"} is not of a type being defined
 and does not occur in @{text "rhs"}\\

changeset 1719	0c3c66f5c0e7
parent 1717	a3ef7fba983f
child 1720	a5def8fe0714