--- a/Paper/Paper.thy Tue Mar 30 15:09:26 2010 +0200
+++ b/Paper/Paper.thy Tue Mar 30 16:59:00 2010 +0200
@@ -222,7 +222,7 @@
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
@@ -844,21 +844,20 @@
\end{equation}
\noindent
- since for finite sets, @{text "S"}, we have
- @{thm (concl) supp_finite_atom_set[no_vars]}).
+ since for finite sets, @{text "S"}, we have @{thm (concl) supp_finite_atom_set[no_vars]}.
- Finally taking \eqref{halfone} and \eqref{halftwo} provides us with a proof
- of Theorem~\ref{suppabs}. The point of these general lemmas about abstractions is that we
- 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 specifications
- of term-calculi.
+ Finally taking \eqref{halfone} and \eqref{halftwo} together provides us with a proof
+ of Theorem~\ref{suppabs}. The point of these properties of abstractions is that we
+ can define and prove them aconveniently on the Isabelle/HOL level,
+ but also use them in what follows next when we deal with binding in
+ specifications 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
@@ -902,8 +901,8 @@
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
- \emph{binding clauses}. These clauses indicate the binders and their scope of
+ the types are optional. Their purpose is to be used in the (possibly empty) list of
+ \emph{binding clauses}, which indicate the binders and their scope
in a term-constructor. They come in three \emph{modes}:
@@ -920,7 +919,7 @@
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
@@ -932,18 +931,18 @@
\begin{center}
\begin{tabular}{@ {}cc@ {}}
\begin{tabular}{@ {}l@ {\hspace{-1mm}}}
- \isacommand{nominal\_datatype} {\it lam} =\\
- \hspace{5mm}\phantom{$\mid$} Var\;{\it name}\\
- \hspace{5mm}$\mid$ App\;{\it lam}\;{\it lam}\\
- \hspace{5mm}$\mid$ Lam\;{\it x::name}\;{\it t::lam}\\
- \hspace{21mm}\isacommand{bind} {\it x} \isacommand{in} {\it t}\\
+ \isacommand{nominal\_datatype} @{text lam} =\\
+ \hspace{5mm}\phantom{$\mid$}~@{text "Var name"}\\
+ \hspace{5mm}$\mid$~@{text "App lam lam"}\\
+ \hspace{5mm}$\mid$~@{text "Lam x::name t::lam"}\\
+ \hspace{21mm}\isacommand{bind} @{text x} \isacommand{in} @{text t}\\
\end{tabular} &
\begin{tabular}{@ {}l@ {}}
- \isacommand{nominal\_datatype} {\it ty} =\\
- \hspace{5mm}\phantom{$\mid$} TVar\;{\it name}\\
- \hspace{5mm}$\mid$ TFun\;{\it ty}\;{\it ty}\\
- \isacommand{and} {\it tsc} = All\;{\it xs::(name fset)}\;{\it T::ty}\\
- \hspace{24mm}\isacommand{bind\_res} {\it xs} \isacommand{in} {\it T}\\
+ \isacommand{nominal\_datatype}~@{text ty} =\\
+ \hspace{5mm}\phantom{$\mid$}~@{text "TVar name"}\\
+ \hspace{5mm}$\mid$~@{text "TFun ty ty"}\\
+ \isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}\\
+ \hspace{24mm}\isacommand{bind\_res} @{text xs} \isacommand{in} @{text T}\\
\end{tabular}
\end{tabular}
\end{center}
@@ -955,9 +954,9 @@
\begin{center}
\begin{tabular}{ll}
- \it {\rm Foo} x::name y::name t::lam & \it
- \isacommand{bind}\;x\;\isacommand{in}\;t,\;
- \isacommand{bind}\;y\;\isacommand{in}\;t
+ @{text "Foo x::name y::name t::lam"} &
+ \isacommand{bind} @{text x} \isacommand{in} @{text t},\;
+ \isacommand{bind} @{text y} \isacommand{in} @{text t}
\end{tabular}
\end{center}
@@ -979,27 +978,27 @@
\begin{center}
\begin{tabular}{l}
- \isacommand{nominal\_datatype} {\it trm} =\\
- \hspace{5mm}\phantom{$\mid$} Var\;{\it name}\\
- \hspace{5mm}$\mid$ App\;{\it trm}\;{\it trm}\\
- \hspace{5mm}$\mid$ Lam\;{\it x::name}\;{\it t::trm}
- \;\;\isacommand{bind} {\it x} \isacommand{in} {\it t}\\
- \hspace{5mm}$\mid$ Let\;{\it p::pat}\;{\it trm}\; {\it t::trm}
- \;\;\isacommand{bind} {\it bn(p)} \isacommand{in} {\it t}\\
- \isacommand{and} {\it pat} =\\
- \hspace{5mm}\phantom{$\mid$} PNil\\
- \hspace{5mm}$\mid$ PVar\;{\it name}\\
- \hspace{5mm}$\mid$ PTup\;{\it pat}\;{\it pat}\\
- \isacommand{with} {\it bn::pat $\Rightarrow$ atom list}\\
- \isacommand{where} $\textit{bn}(\textrm{PNil}) = []$\\
- \hspace{5mm}$\mid$ $\textit{bn}(\textrm{PVar}\;x) = [\textit{atom}\; x]$\\
- \hspace{5mm}$\mid$ $\textit{bn}(\textrm{PTup}\;p_1\;p_2) = \textit{bn}(p_1)\; @\;\textit{bn}(p_2)$\\
+ \isacommand{nominal\_datatype} @{text trm} =\\
+ \hspace{5mm}\phantom{$\mid$}~@{term "Var name"}\\
+ \hspace{5mm}$\mid$~@{term "App trm trm"}\\
+ \hspace{5mm}$\mid$~@{text "Lam x::name t::trm"}
+ \;\;\isacommand{bind} @{text x} \isacommand{in} @{text t}\\
+ \hspace{5mm}$\mid$~@{text "Let p::pat trm t::trm"}
+ \;\;\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t}\\
+ \isacommand{and} @{text pat} =\\
+ \hspace{5mm}\phantom{$\mid$}~@{text PNil}\\
+ \hspace{5mm}$\mid$~@{text "PVar name"}\\
+ \hspace{5mm}$\mid$~@{text "PTup pat pat"}\\
+ \isacommand{with}~@{text "bn::pat \<Rightarrow> atom list"}\\
+ \isacommand{where}~@{text "bn(PNil) = []"}\\
+ \hspace{5mm}$\mid$~@{text "bn(PVar x) = [atom x]"}\\
+ \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.
@@ -1011,16 +1010,19 @@
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,\;
- \isacommand{bind}\;bn(q)\;\isacommand{in}\;t\\
- \it {\rm Foo}$'$x::name p::pat t::trm & \it \it \isacommand{bind}\;x\;\isacommand{in}\;t,\;
- \isacommand{bind}\;bn(p)\;\isacommand{in}\;t
+ @{text "Foo p::pat q::pat t::trm"} &
+ \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t},\;
+ \isacommand{bind} @{text "bn(q)"} \isacommand{in} @{text 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}
@@ -1037,10 +1039,12 @@
\begin{center}
\begin{tabular}{ll}
- \it {\rm Bar} p::pat t::trm s::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;t,\;
- \isacommand{bind}\;bn(p)\;\isacommand{in}\;s\\
- \it {\rm Bar}$'$p::pat t::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;p,\;
- \isacommand{bind}\;bn(p)\;\isacommand{in}\;t\\
+ @{text "Bar p::pat t::trm s::trm"} &
+ \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t},\;
+ \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text s}\\
+ @{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}
@@ -1049,7 +1053,7 @@
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@ {}}
@@ -1083,36 +1087,40 @@
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
- alpha-equivalence relation over them.
+ extract datatype definitions from the specification and then define
+ 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
+ notion defined over alpha-equivalence classes and leave out the superscript
+ for the corresponding notion on the ``raw'' level. So for example:
\begin{center}
- @{text "ty\<^sup>\<alpha> \<mapsto> ty_raw"} \hspace{7mm} @{text "C\<^sup>\<alpha> \<mapsto> C_raw"}
+ @{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
- From this definition we can easily show that the raw datatypes are
- all permutation types (Def ??) by a simple structural induction over
- the @{text "ty_raw"}s.
+ % TODO: we did not define permutation types
+ %\noindent
+ %From this definition we can easily show that the raw datatypes are
+ %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"}
@@ -1136,8 +1144,8 @@
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
- some binding clauses, the function @{text "fv_ty (C_raw x\<^isub>1 \<dots> x\<^isub>n)"} will be
+ 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 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
@@ -1184,7 +1192,7 @@
@{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:
@@ -1219,8 +1227,8 @@
@{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
- 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
+ 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 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:
@@ -1254,8 +1262,8 @@
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 "C_raw x\<^isub>1 \<dots> x\<^isub>n \<approx> C_raw y\<^isub>1 \<dots> y\<^isub>n"} if:
+ @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, two instances of the constructor are equivalent
+ @{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"}\\
--- a/Paper/document/root.bib Tue Mar 30 15:09:26 2010 +0200
+++ b/Paper/document/root.bib Tue Mar 30 16:59:00 2010 +0200
@@ -1,3 +1,14 @@
+@InProceedings{Berghofer99,
+ author = {S.~Berghofer and M.~Wenzel},
+ title = {{I}nductive {D}atatypes in {HOL} - {L}essons {L}earned in
+ {F}ormal-{L}ogic {E}ngineering},
+ booktitle = {Proc.~of the 12th International Conference Theorem Proving in
+ Higher Order Logics (TPHOLs)},
+ pages = {19--36},
+ year = 1999,
+ number = 1690,
+ series = {LNCS}
+}
@InProceedings{CoreHaskell,
author = {M.~Sulzmann and M.~Chakravarty and S.~Peyton Jones and K.~Donnelly},