nominal2: comparison LMCS-Paper/Paper.thy

equal deleted inserted replaced

-:e2c4ee6e3ee7
+:01a3861035d4
 \noindent
 Note that the relation is
 dependent on a free-atom function @{text "fa"} and a relation @{text
 "R"}. The reason for this extra generality is that we will use
-$\approx_{\,\textit{set}}$ for both ``raw'' terms and alpha-equated terms. In
+$\approx_{\,\textit{set}}^{\textit{R}, \textit{fa}}$ for both ``raw'' terms and
+alpha-equated terms. In
 the latter case, @{text R} will be replaced by equality @{text "="} and we
 will prove that @{text "fa"} is equal to @{text "supp"}.
 Definition \ref{alphaset} does not make any distinction between the
 order of abstracted atoms. If we want this, then we can define alpha-equivalence
 \end{equation}\smallskip
 \noindent
 Note that in these relation we replaced the free-atom function @{text "fa"}
 with @{term "supp"} and the relation @{text R} with equality. We can show
-the following properties:
+the following two properties:
 \begin{lem}\label{alphaeq}
 The relations $\approx_{\,\textit{set}}^{=, \textit{supp}}$,
 $\approx_{\,\textit{set+}}^{=, \textit{supp}}$
 and $\approx_{\,\textit{list}}^{=, \textit{supp}}$ are
 a permutation @{text "\<pi>"} and for the proof obligation take @{term "-
 \<pi>"}. In case of transitivity, we have two permutations @{text "\<pi>\<^isub>1"}
 and @{text "\<pi>\<^isub>2"}, and for the proof obligation use @{text
 "\<pi>\<^isub>1 + \<pi>\<^isub>2"}. Equivariance means @{term "alpha_set_ex (\<pi> \<bullet> as,
 \<pi> \<bullet> x) equal supp (\<pi> \<bullet> bs, \<pi> \<bullet> y)"} holds provided \mbox{@{term
-"alpha_set_ex (as, x) equal supp(bs, y)"}} holds. To show this, we need to
+"alpha_set_ex (as, x) equal supp(bs, y)"}} holds. From the assumption we
-unfold the definitions and `pull out' the permutations, which is possible
+have a permutation @{text "\<pi>'"} and for the proof obligation use @{text "\<pi> \<bullet>
-since all operators, such as @{text "#\<^sup>*, -, set"} and @{text "supp"},
+\<pi>'"}. To show then equivariance, we need to `pull out' the permutations,
-are equivariant (see \cite{HuffmanUrban10}). Finally we apply the
+which is possible since all operators, namely as @{text "#\<^sup>*, -, =, \<bullet>,
-permutation operation on booleans.
+set"} and @{text "supp"}, are equivariant (see
+\cite{HuffmanUrban10}). Finally, we apply the permutation operation on
+booleans.
 \end{proof}
 \noindent
 Recall the picture shown in \eqref{picture} about new types in HOL.
 The lemma above allows us to use our quotient package for introducing
 @{thm (prem 2) Abs_swap1(1)[where bs="as", no_vars]} then
 @{thm (concl) Abs_swap1(1)[where bs="as", no_vars]}
 \end{lem}
 \begin{proof}
-This lemma is straightforward using \eqref{abseqiff} and observing that
+If @{term "a = b"} the lemma is immediate, since @{term "(a \<rightleftharpoons> b) = 0"}.
-the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}.
+Also in the other case, it is straightforward using \eqref{abseqiff} and
-We therefore can use as permutation the swapping @{term "(a \<rightleftharpoons> b)"}.
+observing that the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) =
+(supp x - as)"}.  We therefore can use as permutation the swapping @{term
+"(a \<rightleftharpoons> b)"}.
 \end{proof}
 \noindent
 Assuming that @{text "x"} has finite support, this lemma together
 with \eqref{absperm} allows us to show
 This is because for every finite sets of atoms, say @{text "bs"}, we have
 @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.
 Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes
 the first equation of Theorem~\ref{suppabs}.
-Recall the definition of support \eqref{suppdef}, and note the difference between
+Recall the definition of support in \eqref{suppdef}, and note the difference between
 the support of a ``raw'' pair and an abstraction
 \[
 @{term "supp (as, x) = supp as \<union> supp x"}\hspace{15mm}
 @{term "supp (Abs_set as x) = supp x - as"}
 \]\smallskip
 \noindent
-While the permutation operations behave in both cases the same (the permutation
+While the permutation operations behave in both cases the same (a permutation
 is just moved to the arguments), the notion of equality is different for pairs and
 abstractions. Therefore we have different supports.
 The method of first considering abstractions of the form @{term "Abs_set as
 x"} etc is motivated by the fact that we can conveniently establish at the
 \begin{equation}\label{ceqvt}
 @{text "\<pi> \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (\<pi> \<bullet> z\<^isub>1) \<dots> (\<pi> \<bullet> z\<^isub>n)"}
 \end{equation}\smallskip
+\noindent
+We need this operation later when we define the notion of alpha-equivalence.
 The first non-trivial step we have to perform is the generation of
 \emph{free-atom functions} from the specifications.\footnote{Admittedly, the
 details of our definitions will be somewhat involved. However they are still
 conceptually simple in comparison with the ``positional'' approach taken in
 Ott \cite[Pages 88--95]{ott-jfp}, which uses the notions of \emph{occurences} and
 @{text "fa_bn"}\mbox{$_{1..m}$}.
 \]\smallskip
 \noindent
 The reason for this setup is that in a deep binder not all atoms have to be
-bound, as we saw in the example with ``plain'' @{text Let}s. We need therefore a function
+bound, as we saw in the example with ``plain'' @{text Let}s. We need
-that calculates those free atoms in a deep binder.
+therefore functions that calculate those free atoms in deep binders.
-While the idea behind these free-atom functions is clear (they just
+While the idea behind these free-atom functions is simple (they just
 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
+a ``raw'' term-constructor @{text "C"} of type @{text ty} and some associated
 binding clauses @{text "bc\<^isub>1\<dots>bc\<^isub>k"}, the result of @{text
 "fa_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be the union @{text
 "fa(bc\<^isub>1) \<union> \<dots> \<union> fa(bc\<^isub>k)"} where we will define below what @{text "fa"} for a binding
 clause means. We only show the details for the mode \isacommand{binds (set)} (the other modes are similar).
 Suppose the binding clause @{text bc\<^isub>i} is of the form
 \end{equation}\smallskip
 \noindent
 where we use the auxiliary binding functions from \eqref{bnaux} for shallow
 binders (that means when @{text "ty"}$_i$ is of type @{text "atom"}, @{text "atom set"} or
-@{text "atom list"}). The set @{text "B'"} in \eqref{fadef} collects all free atoms in
+@{text "atom list"}).
+The set @{text "B'"} in \eqref{fadef} collects all free atoms in
 non-recursive deep binders. Let us assume these binders in the binding
 clause @{text "bc\<^isub>i"} are
 \[
 \mbox{@{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}}
 $\approx_{\,\textit{list}}^{\textit{R}, \textit{fa}}$ for the other
 binding modes). This premise defines alpha-equivalence of two abstractions
 involving multiple binders. As above, we first build the tuples @{text "D"} and
 @{text "D'"} for the bodies @{text "d"}$_{1..q}$, and the corresponding
 compound alpha-relation @{text "R"} (shown in \eqref{rempty}).
-For $\approx_{\,\textit{set}}^{R, fa}$  we also need
+For $\approx_{\,\textit{set}}^{\textit{R}, \textit{fa}}$  we also need
 a compound free-atom function for the bodies defined as
 \[
 \mbox{@{text "fa \<equiv> (fa_ty\<^isub>1,\<dots>, fa_ty\<^isub>q)"}}
 \]\smallskip
 non-empty ones (we just have to unfold the definition of
 $\approx_{\,\textit{set}}^{\textit{R}, \textit{fa}}$ and take @{text "0"}
 for the existentially quantified permutation).
 Again let us take a look at a concrete example for these definitions. For
-teh specification given in \eqref{letrecs}
+the specification given in \eqref{letrecs}
 we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
 $\approx_{\textit{bn}}$ with the following clauses:
 \[\mbox{
 \begin{tabular}{@ {}c @ {}}
 clause for @{text "Let"} (which has
 a non-recursive binder).
 The underlying reason is that the terms inside an assignment are not meant
 to be ``under'' the binder. Such a premise is \emph{not} needed in @{text "Let_rec"},
 because there all components of an assignment are ``under'' the binder.
-Note also that in case of more than one body (e.g.~@{text "Let_rec"}-case)
+Note also that in case of more than one body (e.g.~in the @{text "Let_rec"}-case)
-we need to parametrise the relation $\approx_{\textit{list}}$ with compound
+we need to parametrise the relation $\approx_{\textit{list}}$ with a compound
-equivalence relations and compund free-atom functions.
+equivalence relation and a compound free-atom function. This is because the
+corresponding binding cluase specifies a binder with two bodies.
 *}
 section {* Establishing the Reasoning Infrastructure *}
 text {*
 @{text "(ii)"} The relations @{text "\<approx>ty"}$_{1..n}$ and
 @{text "\<approx>bn"}$_{1..m}$ are equivariant.
 \end{lem}
 \begin{proof}
-The function package of Isabelle/HOL allows us to prove the first part is by
+The function package of Isabelle/HOL \cite{Krauss09} allows us to prove the
-mutual induction over the definitions of the functions (we know that they
+first part is by mutual induction over the definitions of the functions.\footnote{We
-are terminating functions, from which an induction principle can be
+know that they are terminating functions. From this an induction principle
-derived). The second is by a straightforward induction over the rules of
+is derived by the function package.} The second is by a straightforward
-@{text "\<approx>ty"}$_{1..n}$ and @{text "\<approx>bn"}$_{1..m}$ using the first part.
+induction over the rules of @{text "\<approx>ty"}$_{1..n}$ and @{text "\<approx>bn"}$_{1..m}$ using
+the first part.
 \end{proof}
 \noindent
 Next we establish that the alpha-equivalence relations defined in the
 previous section are indeed equivalence relations.
 \noindent
 We can feed the last lemma into our quotient package and obtain new types
 @{text "ty"}$^\alpha_{1..n}$ representing alpha-equated terms of types
 @{text "ty"}$_{1..n}$. We also obtain definitions for the term-constructors
-@{text "C"}$^\alpha_{1..k}$ from the raw term-constructors @{text
+@{text "C"}$^\alpha_{1..k}$ from the ``raw'' term-constructors @{text
 "C"}$_{1..k}$, and similar definitions for the free-atom functions @{text
 "fa_ty"}$^\alpha_{1..n}$ and @{text "fa_bn"}$^\alpha_{1..m}$ as well as the
 binding functions @{text "bn"}$^\alpha_{1..m}$. However, these definitions
 are not really useful to the user, since they are given in terms of the
 isomorphisms we obtained by creating new types in Isabelle/HOL (recall the
 \begin{equation}\label{distinctraw}
 \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>r"}\;$\not\approx$@{text ty}\;@{text "D y\<^isub>1 \<dots> y\<^isub>s"}}
 \end{equation}\smallskip
 \noindent
-holds for the corresponding raw term-constructors.
+holds for the corresponding ``raw'' term-constructors.
 In order to deduce \eqref{distinctalpha} from \eqref{distinctraw}, our quotient
-package needs to know that the raw term-constructors @{text "C"} and @{text "D"}
+package needs to know that the ``raw'' term-constructors @{text "C"} and @{text "D"}
 are \emph{respectful} w.r.t.~the alpha-equivalence relations (see \cite{Homeier05}).
 Given, for example, @{text "C"} is of type @{text "ty"} with argument types
 @{text "ty"}$_{1..r}$, respectfulness amounts to showing that
 \[\mbox{
 }\]\smallskip
 \noindent
 holds under the assumptions \mbox{@{text
 "x\<^isub>i \<approx>ty\<^isub>i x\<PRIME>\<^isub>i"}} whenever @{text "x\<^isub>i"}
-and @{text "x\<PRIME>\<^isub>i"} are recursive arguments of @{text C} and
+and @{text "x\<PRIME>\<^isub>i"} are recursive arguments of @{text C}, and
 @{text "x\<^isub>i = x\<PRIME>\<^isub>i"} whenever they are non-recursive arguments
 (similarly for @{text "D"}). For this we have to show
 by induction over the definitions of alpha-equivalences the following
 auxiliary implications
 \end{tabular}
 }\end{equation}\smallskip
 \noindent
 whereby @{text "ty\<^isub>l"} is the type over which @{text "bn\<^isub>j"}
-is defined. These implications can be established by induction on @{text
+is defined. Whereas the first, second and last implication are true by
-"\<approx>ty"}$_{1..n}$. Whereas the first, second and last implication are true by
 how we stated our definitions, the third \emph{only} holds because of our
 restriction imposed on the form of the binding functions---namely \emph{not}
-returning any bound atoms. In Ott, in contrast, the user may define @{text
+to return any bound atoms. In Ott, in contrast, the user may define @{text
 "bn"}$_{1..m}$ so that they return bound atoms and in this case the third
-implication is \emph{not} true. A result is that the lifting of the
+implication is \emph{not} true. A result is that in general the lifting of the
 corresponding binding functions in Ott to alpha-equated terms is impossible.
-Having established respectfulness for the raw term-constructors, the
+Having established respectfulness for the ``raw'' term-constructors, the
 quotient package is able to automatically deduce \eqref{distinctalpha} from
 \eqref{distinctraw}. Having the facts \eqref{fnresp} at our disposal, we can
-also lift properties that characterise when two raw terms of the form
+also lift properties that characterise when two ``raw'' terms of the form
 \[
 \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}}
 \]\smallskip
 @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r = C\<^sup>\<alpha> x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}.
 \]\smallskip
 \noindent
 We call these conditions as \emph{quasi-injectivity}. They correspond to
-the premises in our alpha-equiva\-lence relations.
+the premises in our alpha-equiva\-lence relations, with the exception that
+in case of binders the relations $\approx_{\textit{set}}^{\textit{R}, \textit{fa}}$
+are replaced by $\approx_{\textit{set}}^{=, \textit{fa}}$.
 Next we can lift the permutation operations defined in \eqref{ceqvt}. In
 order to make this lifting to go through, we have to show that the
 permutation operations are respectful. This amounts to showing that the
 alpha-equivalence relations are equivariant, which
 @{text "fa_bn\<AL>"}$_{1..m}$ as well as of the binding functions @{text
 "bn\<AL>"}$_{1..m}$ and the size functions @{text "size_ty\<AL>"}$_{1..n}$.
 The latter are defined automatically for the raw types @{text "ty"}$_{1..n}$
 by the datatype package of Isabelle/HOL.
-Finally we can add to our infrastructure cases lemmas and a structural
+Finally we can add to our infrastructure cases lemmas and a (mutual)
 induction principle for the types @{text "ty\<AL>"}$_{1..n}$. The cases
 lemmas allow the user to deduce a property @{text "P"} by exhaustively
-analysing all cases how the elements in a type @{text "ty\<AL>"}$_i$ can
+analysing all cases how an element in a type @{text "ty\<AL>"}$_i$ can
-be constructed (that means one case for each of term-constructors @{text "C\<AL>"}$_{1..m}$
+be constructed (that means one case for each of term-constructors
-of type @{text "ty\<AL>"}$_i\,$). These are lifted versions of the cases
+of type @{text "ty\<AL>"}$_i\,$). The lifted cases
-lemma over the raw type  @{text "ty"}$_i$ and schematically look as
+lemma for the type @{text "ty\<AL>"}$_i\,$ looks as
 follows
 \[
 \infer{P}
 {\begin{array}{l}
 \end{array}}
 \]\smallskip
 \noindent
 where @{text "y"} is a variable of type @{text "ty"}$_i$ and @{text "P"} is the
-property that is established by the case analysis. Similarly, we have an induction
+property that is established by the case analysis. Similarly, we have a (mutual)
-principle for the types @{text "ty\<AL>"}$_{1..n}$, which is
+induction principle for the types @{text "ty\<AL>"}$_{1..n}$, which is of the
+form
 \[
 \infer{@{text "P\<^isub>1 y\<^isub>1 \<and> \<dots> \<and> P\<^isub>n y\<^isub>n "}}
 {\begin{array}{l}
 @{text "\<forall>x\<^isub>1\<dots>x\<^isub>k. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<AL>\<^isub>1 x\<^isub>1 \<dots> x\<^isub>k)"}\\
 \]\smallskip
 \noindent
 whereby the @{text P}$_{1..n}$ are the properties established by induction
 and the @{text y}$_{1..n}$ are of type @{text "ty\<AL>"}$_{1..n}$.
-This induction principle has for all term constructors @{text "C"}$^\alpha$
+This induction principle has for the term constructors @{text "C"}$^\alpha_1$
 a premise of the form
 \begin{equation}\label{weakprem}
-\mbox{@{text "\<forall>x\<^isub>1\<dots>x\<^isub>r. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r)"}}
+\mbox{@{text "\<forall>x\<^isub>1\<dots>x\<^isub>k. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<AL>\<^sub>1 x\<^isub>1 \<dots> x\<^isub>k)"}}
 \end{equation}\smallskip
 \noindent
-in which the @{text "x"}$_{i..j}$ @{text "\<subseteq>"} @{text "x"}$_{1..r}$ are
+in which the @{text "x"}$_{i..j}$ @{text "\<subseteq>"} @{text "x"}$_{1..k}$ are
-the recursive arguments of the term constructor. In case of the lambda-calculus,
+the recursive arguments of this term constructor (similarly for the other
-the cases lemma and the induction principle boil down to the following:
+term-constructors). In case of the lambda-calculus (with constructors
+@{text "Var\<^sup>\<alpha>"},  @{text "App\<^sup>\<alpha>"} and  @{text "Lam\<^sup>\<alpha>"}),
+the cases lemmas and the induction principle boil down to the following
+two inference rules:
 \[\mbox{
 \begin{tabular}{c@ {\hspace{10mm}}c}
 \infer{@{text "P"}}
 {\begin{array}{l}
 @{text "\<forall>x\<^isub>1 x\<^isub>2. P x\<^isub>2 \<Rightarrow> P (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}
 \end{array}}
 \end{tabular}}
 \]\smallskip
+\noindent
+We will show in the next section that these inference rules are not very
+convenient for the user to establish properties about lambda-terms, but
+they are crucial for completing our reasoning infrastructure for the
+types @{text "ty\<AL>"}$_{1..n}$.
 By working now completely on the alpha-equated level, we
 can first show that the free-atom functions and binding functions are
 equivariant, namely
 \[\mbox{
 \noindent
 These properties can be established using the induction principle for the
 types @{text "ty\<AL>"}$_{1..n}$.  Having these
-equivariant properties established, we can show that the support of
+equivariant properties at our disposal, we can show that the support of
 term-constructors @{text "C\<^sup>\<alpha>"} is included in the support of its
 arguments, that means
 \[
 @{text "supp (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r) \<subseteq> (supp x\<^isub>1 \<union> \<dots> \<union> supp x\<^isub>r)"}
 \]\smallskip
 \noindent
 holds. This allows us to prove by induction that every @{text x} of type
 @{text "ty\<AL>"}$_{1..n}$ is finitely supported. This can be again shown by
-induction over @{text "ty\<AL>"}$_{1..n}$. Lastly, we can show that the
+the induction principle for  @{text "ty\<AL>"}$_{1..n}$. Lastly, we can show that the
 support of elements in @{text "ty\<AL>"}$_{1..n}$ is the same as @{text
-"fa_ty\<AL>"}$_{1..n}$.  This fact is important in the nominal setting, but
+"fa_ty\<AL>"}$_{1..n}$.  This fact is important in the nominal setting
+where the general theory is formulated in terms of @{text "supp"} and @{text "#"}, but
 also provides evidence that our notions of free-atoms and alpha-equivalence
 are sensible.
 \begin{thm}
 For @{text "x"}$_{1..n}$ with type @{text "ty\<AL>"}$_{1..n}$, we have
 \end{proof}
 \noindent
 To sum up this section, we can establish automatically a reasoning infrastructure
 for the types @{text "ty\<AL>"}$_{1..n}$
-by first lifting definitions from the raw level to the quotient level and
+by first lifting definitions from the ``raw'' level to the quotient level and
 then by establishing facts about these lifted definitions. All necessary proofs
 are generated automatically by custom ML-code.
-%This code can deal with
-%specifications such as the one shown in Figure~\ref{nominalcorehas} for Core-Haskell.
-%\begin{figure}[t!]
-%\begin{boxedminipage}{\linewidth}
-%\small
-%\begin{tabular}{l}
-%\isacommand{atom\_decl}~@{text "var cvar tvar"}\\[1mm]
-%\isacommand{nominal\_datatype}~@{text "tkind ="}\\
-%\phantom{$|$}~@{text "KStar"}~$|$~@{text "KFun tkind tkind"}\\
-%\isacommand{and}~@{text "ckind ="}\\
-%\phantom{$|$}~@{text "CKSim ty ty"}\\
-%\isacommand{and}~@{text "ty ="}\\
-%\phantom{$|$}~@{text "TVar tvar"}~$|$~@{text "T string"}~$|$~@{text "TApp ty ty"}\\
-%$|$~@{text "TFun string ty_list"}~%
-%$|$~@{text "TAll tv::tvar tkind ty::ty"}  \isacommand{binds}~@{text "tv"}~\isacommand{in}~@{text ty}\\
-%$|$~@{text "TArr ckind ty"}\\
-%\isacommand{and}~@{text "ty_lst ="}\\
-%\phantom{$|$}~@{text "TNil"}~$|$~@{text "TCons ty ty_lst"}\\
-%\isacommand{and}~@{text "cty ="}\\
-%\phantom{$|$}~@{text "CVar cvar"}~%
-%$|$~@{text "C string"}~$|$~@{text "CApp cty cty"}~$|$~@{text "CFun string co_lst"}\\
-%$|$~@{text "CAll cv::cvar ckind cty::cty"}  \isacommand{binds}~@{text "cv"}~\isacommand{in}~@{text cty}\\
-%$|$~@{text "CArr ckind cty"}~$|$~@{text "CRefl ty"}~$|$~@{text "CSym cty"}~$|$~@{text "CCirc cty cty"}\\
-%$|$~@{text "CAt cty ty"}~$|$~@{text "CLeft cty"}~$|$~@{text "CRight cty"}~$|$~@{text "CSim cty cty"}\\
-%$|$~@{text "CRightc cty"}~$|$~@{text "CLeftc cty"}~$|$~@{text "Coerce cty cty"}\\
-%\isacommand{and}~@{text "co_lst ="}\\
-%\phantom{$|$}@{text "CNil"}~$|$~@{text "CCons cty co_lst"}\\
-%\isacommand{and}~@{text "trm ="}\\
-%\phantom{$|$}~@{text "Var var"}~$|$~@{text "K string"}\\
-%$|$~@{text "LAM_ty tv::tvar tkind t::trm"}  \isacommand{binds}~@{text "tv"}~\isacommand{in}~@{text t}\\
-%$|$~@{text "LAM_cty cv::cvar ckind t::trm"}   \isacommand{binds}~@{text "cv"}~\isacommand{in}~@{text t}\\
-%$|$~@{text "App_ty trm ty"}~$|$~@{text "App_cty trm cty"}~$|$~@{text "App trm trm"}\\
-%$|$~@{text "Lam v::var ty t::trm"}  \isacommand{binds}~@{text "v"}~\isacommand{in}~@{text t}\\
-%$|$~@{text "Let x::var ty trm t::trm"}  \isacommand{binds}~@{text x}~\isacommand{in}~@{text t}\\
-%$|$~@{text "Case trm assoc_lst"}~$|$~@{text "Cast trm co"}\\
-%\isacommand{and}~@{text "assoc_lst ="}\\
-%\phantom{$|$}~@{text ANil}~%
-%$|$~@{text "ACons p::pat t::trm assoc_lst"}  \isacommand{binds}~@{text "bv p"}~\isacommand{in}~@{text t}\\
-%\isacommand{and}~@{text "pat ="}\\
-%\phantom{$|$}~@{text "Kpat string tvtk_lst tvck_lst vt_lst"}\\
-%\isacommand{and}~@{text "vt_lst ="}\\
-%\phantom{$|$}~@{text VTNil}~$|$~@{text "VTCons var ty vt_lst"}\\
-%\isacommand{and}~@{text "tvtk_lst ="}\\
-%\phantom{$|$}~@{text TVTKNil}~$|$~@{text "TVTKCons tvar tkind tvtk_lst"}\\
-%\isacommand{and}~@{text "tvck_lst ="}\\
-%\phantom{$|$}~@{text TVCKNil}~$|$ @{text "TVCKCons cvar ckind tvck_lst"}\\
-%\isacommand{binder}\\
-%@{text "bv :: pat \<Rightarrow> atom list"}~\isacommand{and}~%
-%@{text "bv1 :: vt_lst \<Rightarrow> atom list"}~\isacommand{and}\\
-%@{text "bv2 :: tvtk_lst \<Rightarrow> atom list"}~\isacommand{and}~%
-%@{text "bv3 :: tvck_lst \<Rightarrow> atom list"}\\
-%\isacommand{where}\\
-%\phantom{$|$}~@{text "bv (K s tvts tvcs vs) = (bv3 tvts) @ (bv2 tvcs) @ (bv1 vs)"}\\
-%$|$~@{text "bv1 VTNil = []"}\\
-%$|$~@{text "bv1 (VTCons x ty tl) = (atom x)::(bv1 tl)"}\\
-%$|$~@{text "bv2 TVTKNil = []"}\\
-%$|$~@{text "bv2 (TVTKCons a ty tl) = (atom a)::(bv2 tl)"}\\
-%$|$~@{text "bv3 TVCKNil = []"}\\
-%$|$~@{text "bv3 (TVCKCons c cty tl) = (atom c)::(bv3 tl)"}\\
-%\end{tabular}
-%\end{boxedminipage}
-%\caption{The nominal datatype declaration for Core-Haskell. For the moment we
-%do not support nested types; therefore we explicitly have to unfold the
-%lists @{text "co_lst"}, @{text "assoc_lst"} and so on. This will be improved
-%in a future version of Nominal Isabelle. Apart from that, the
-%declaration follows closely the original in Figure~\ref{corehas}. The
-%point of our work is that having made such a declaration in Nominal Isabelle,
-%one obtains automatically a reasoning infrastructure for Core-Haskell.
-%\label{nominalcorehas}}
-%\end{figure}
 *}
 section {* Strong Induction Principles *}
 approach to
 binding \cite{chargueraud09}.  There, de-Bruijn indices consist of two
 numbers, one referring to the place where a variable is bound, and the other
 to which variable is bound. The reasoning infrastructure for both
 representations of bindings comes for free in theorem provers like
-Isabelle/HOL or Coq, since the corresponding term-calculi can be implemented
+Isabelle/HOL and Coq, since the corresponding term-calculi can be implemented
 as ``normal'' datatypes.  However, in both approaches it seems difficult to
 achieve our fine-grained control over the ``semantics'' of bindings
 (i.e.~whether the order of binders should matter, or vacuous binders should
 be taken into account). To do so, one would require additional predicates
 that filter out unwanted terms. Our guess is that such predicates result in
-rather intricate formal reasoning. We are not aware of any non-trivial
+rather intricate formal reasoning. We are not aware of any formalisation of
-formalisation that uses Chargu\'eraud's idea.
+a non-trivial language that uses Chargu\'eraud's idea.
 Another technique for representing binding is higher-order abstract syntax
 (HOAS), which for example is implemented in the Twelf system. This
 representation technique supports very elegantly many aspects of
 \emph{single} binding, and impressive work by Lee et al has been done that
 The most closely related work to the one presented here is the Ott-tool by
 Sewell et al \cite{ott-jfp} and the C$\alpha$ml language by Pottier
 \cite{Pottier06}. Ott is a nifty front-end for creating \LaTeX{} documents
 from specifications of term-calculi involving general binders. For a subset
-of the specifications Ott can also generate theorem prover code using a raw
+of the specifications Ott can also generate theorem prover code using a ``raw''
 representation of terms, and in Coq also a locally nameless
 representation. The developers of this tool have also put forward (on paper)
 a definition for alpha-equivalence and free variables for terms that can be
 specified in Ott.  This definition is rather different from ours, not using
 any nominal techniques.  To our knowledge there is no concrete mathematical
 result concerning this notion of alpha-equivalence and free variables. We
 have proved that our definitions lead to alpha-equated terms, whose support
 is as expected (that means bound names are removed from the support). We
-also showed that our specifications lift from a raw type to a type of
+also showed that our specifications lift from ``raw'' types to types of
 alpha-equivalence classes. For this we had to establish (automatically) that every
 term-constructor and function is repectful w.r.t.~alpha-equivalence.
 Although we were heavily inspired by the syntax of Ott, its definition of
 alpha-equi\-valence is unsuitable for our extension of Nominal
 and therefore need the extra generality to be able to distinguish between
 both specifications.  Because of how we set up our definitions, we also had
 to impose some restrictions (like a single binding function for a deep
 binder) that are not present in Ott. Our expectation is that we can still
 cover many interesting term-calculi from programming language research, for
-example Core-Haskell. ???
+example Core-Haskell (see Figure~\ref{nominalcorehas}).
+\begin{figure}[p!]
+\begin{boxedminipage}{\linewidth}
+\small
+\begin{tabular}{l}
+\isacommand{atom\_decl}~@{text "var cvar tvar"}\\[1mm]
+\isacommand{nominal\_datatype}~@{text "tkind ="}~@{text "KStar"}~$|$~@{text "KFun tkind tkind"}\\
+\isacommand{and}~@{text "ckind ="}~@{text "CKSim ty ty"}\\
+\isacommand{and}~@{text "ty ="}~@{text "TVar tvar"}~$|$~@{text "T string"}~$|$~@{text "TApp ty ty"}\\
+$|$~@{text "TFun string ty_list"}~%
+$|$~@{text "TAll tv::tvar tkind ty::ty"}\hspace{3mm}\isacommand{binds}~@{text "tv"}~\isacommand{in}~@{text ty}\\
+$|$~@{text "TArr ckind ty"}\\
+\isacommand{and}~@{text "ty_lst ="}~@{text "TNil"}~$|$~@{text "TCons ty ty_lst"}\\
+\isacommand{and}~@{text "cty ="}~@{text "CVar cvar"}~%
+$|$~@{text "C string"}~$|$~@{text "CApp cty cty"}~$|$~@{text "CFun string co_lst"}\\
+$|$~@{text "CAll cv::cvar ckind cty::cty"}\hspace{3mm}\isacommand{binds}~@{text "cv"}~\isacommand{in}~@{text cty}\\
+$|$~@{text "CArr ckind cty"}~$|$~@{text "CRefl ty"}~$|$~@{text "CSym cty"}~$|$~@{text "CCirc cty cty"}\\
+$|$~@{text "CAt cty ty"}~$|$~@{text "CLeft cty"}~$|$~@{text "CRight cty"}~$|$~@{text "CSim cty cty"}\\
+$|$~@{text "CRightc cty"}~$|$~@{text "CLeftc cty"}~$|$~@{text "Coerce cty cty"}\\
+\isacommand{and}~@{text "co_lst ="}~@{text "CNil"}~$|$~@{text "CCons cty co_lst"}\\
+\isacommand{and}~@{text "trm ="}~@{text "Var var"}~$|$~@{text "K string"}\\
+$|$~@{text "LAM_ty tv::tvar tkind t::trm"}\hspace{3mm}\isacommand{binds}~@{text "tv"}~\isacommand{in}~@{text t}\\
+$|$~@{text "LAM_cty cv::cvar ckind t::trm"}\hspace{3mm}\isacommand{binds}~@{text "cv"}~\isacommand{in}~@{text t}\\
+$|$~@{text "App_ty trm ty"}~$|$~@{text "App_cty trm cty"}~$|$~@{text "App trm trm"}\\
+$|$~@{text "Lam v::var ty t::trm"}\hspace{3mm}\isacommand{binds}~@{text "v"}~\isacommand{in}~@{text t}\\
+$|$~@{text "Let x::var ty trm t::trm"}\hspace{3mm}\isacommand{binds}~@{text x}~\isacommand{in}~@{text t}\\
+$|$~@{text "Case trm assoc_lst"}~$|$~@{text "Cast trm co"}\\
+\isacommand{and}~@{text "assoc_lst ="}~@{text ANil}~%
+$|$~@{text "ACons p::pat t::trm assoc_lst"}\hspace{3mm}\isacommand{binds}~@{text "bv p"}~\isacommand{in}~@{text t}\\
+\isacommand{and}~@{text "pat ="}~@{text "Kpat string tvtk_lst tvck_lst vt_lst"}\\
+\isacommand{and}~@{text "vt_lst ="}~@{text VTNil}~$|$~@{text "VTCons var ty vt_lst"}\\
+\isacommand{and}~@{text "tvtk_lst ="}~@{text TVTKNil}~$|$~@{text "TVTKCons tvar tkind tvtk_lst"}\\
+\isacommand{and}~@{text "tvck_lst ="}~@{text TVCKNil}~$|$ @{text "TVCKCons cvar ckind tvck_lst"}\\
+\isacommand{binder}\\
+@{text "bv :: pat \<Rightarrow> atom list"}~\isacommand{and}\\
+@{text "bv\<^isub>1 :: vt_lst \<Rightarrow> atom list"}~\isacommand{and}\\
+@{text "bv\<^isub>2 :: tvtk_lst \<Rightarrow> atom list"}~\isacommand{and}\\
+@{text "bv\<^isub>3 :: tvck_lst \<Rightarrow> atom list"}\\
+\isacommand{where}\\
+\phantom{$|$}~@{text "bv (K s tvts tvcs vs) = (bv\<^isub>3 tvts) @ (bv\<^isub>2 tvcs) @ (bv\<^isub>1 vs)"}\\
+$|$~@{text "bv\<^isub>1 VTNil = []"}\\
+$|$~@{text "bv\<^isub>1 (VTCons x ty tl) = (atom x)::(bv\<^isub>1 tl)"}\\
+$|$~@{text "bv\<^isub>2 TVTKNil = []"}\\
+$|$~@{text "bv\<^isub>2 (TVTKCons a ty tl) = (atom a)::(bv\<^isub>2 tl)"}\\
+$|$~@{text "bv\<^isub>3 TVCKNil = []"}\\
+$|$~@{text "bv\<^isub>3 (TVCKCons c cty tl) = (atom c)::(bv\<^isub>3 tl)"}\\
+\end{tabular}
+\end{boxedminipage}
+\caption{The nominal datatype declaration for Core-Haskell. For the moment we
+do not support nested types; therefore we explicitly have to unfold the
+lists @{text "co_lst"}, @{text "assoc_lst"} and so on. Apart from that, the
+declaration follows closely the original in Figure~\ref{corehas}. The
+point of our work is that having made such a declaration in Nominal Isabelle,
+one obtains automatically a reasoning infrastructure for Core-Haskell.
+\label{nominalcorehas}}
+\end{figure}
 Pottier presents a programming language, called C$\alpha$ml, for
 representing terms with general binders inside OCaml \cite{Pottier06}. This
 language is implemented as a front-end that can be translated to OCaml with
 the help of a library. He presents a type-system in which the scope of
 eventually become part of the next Isabelle distribution.\footnote{It
 can be downloaded from \href{http://isabelle.in.tum.de/nominal/download}
 {http://isabelle.in.tum.de/nominal/download}.}
 We have left out a discussion about how functions can be defined over
-alpha-equated terms involving general binders. In earlier versions of Nominal
+alpha-equated terms involving general binders. In earlier versions of
-Isabelle this turned out to be a thorny issue.  We
+Nominal Isabelle this turned out to be a thorny issue.  We hope to do better
-hope to do better this time by using the function package that has recently
+this time by using the function package \cite{Krauss09} that has recently
 been implemented in Isabelle/HOL and also by restricting function
-definitions to equivariant functions (for them we can
+definitions to equivariant functions (for them we can provide more
-provide more automation).
+automation).
 There are some restrictions we imposed in this paper that we would like to lift in
 future work. One is the exclusion of nested datatype definitions. Nested
 datatype definitions allow one to specify, for instance, the function kinds
 in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded

changeset 3013	01a3861035d4
parent 3012	e2c4ee6e3ee7
child 3014	e57c175d9214