--- a/Paper/Paper.thy Fri Apr 02 05:09:47 2010 +0200
+++ b/Paper/Paper.thy Fri Apr 02 06:45:50 2010 +0200
@@ -1138,10 +1138,10 @@
raw datatype. We can also easily define permutation operations by
primitive recursion so that for each term constructor @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}
we have that
-
- \begin{center}
+ %
+ \begin{equation}\label{ceqvt}
@{text "p \<bullet> (C x\<^isub>1 \<dots> x\<^isub>n) = C (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"}
- \end{center}
+ \end{equation}
% TODO: we did not define permutation types
%\noindent
@@ -1463,12 +1463,14 @@
section {* Establishing the Reasoning Infrastructure *}
text {*
- Having made all necessary definitions for raw terms, we can start introducing
- the reasoning infrastructure for the types the user specified. For this we first
- have to show that the alpha-equivalence relations defined in the previous
- section are indeed equivalence relations.
+ Having made all necessary definitions for raw terms, we can start
+ introducing the reasoning infrastructure for the alpha-equated types the
+ user specified. We sketch in this section the facts we need for establishing
+ this reasoning infrastructure. We first have to show that the
+ alpha-equivalence relations defined in the previous section are indeed
+ equivalence relations.
- \begin{lemma}
+ \begin{lemma}\label{equiv}
Given the raw types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"} and binding functions
@{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, the relations @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"} and
@{text "\<approx>bn\<^isub>1 \<dots> \<approx>bn\<^isub>m"} are equivalence relations and equivariant.
@@ -1523,7 +1525,7 @@
\noindent
under the assumption that @{text "x\<^isub>i \<approx>ty\<^isub>i y\<^isub>i"} holds for all recursive arguments
and @{text "x\<^isub>i = y\<^isub>i"} for all non-recursive arguments. We can prove this by
- analysing the definition of @{text "\<approx>ty"}. For this to succed we have to establish an
+ analysing the definition of @{text "\<approx>ty"}. For this to succeed we have to establish an
auxiliary fact: given a binding function @{text bn} defined for the type @{text ty}
we have that
@@ -1534,8 +1536,8 @@
\noindent
This can be established by induction on the definition of @{text "\<approx>ty"}.
- Having established respectfullness for every raw term-constructor, the
- quotient package will automaticaly deduce \eqref{distinctalpha} from \eqref{distinctraw}.
+ Having established respectfulness for every raw term-constructor, the
+ quotient package will automatically deduce \eqref{distinctalpha} from \eqref{distinctraw}.
In fact we can lift any fact from the raw level to the alpha-equated level that
apart from variables only contains the raw term-constructors @{text "C\<^isub>i"}. The
induction principles derived by the datatype package of Isabelle/HOL for @{text
@@ -1557,119 +1559,185 @@
\noindent
where the @{text "x\<^isub>i, \<dots>, x\<^isub>j"} are the recursive arguments of @{text "C\<^sup>\<alpha>"}.
-
-
-To lift
- the raw definitions to the quotient type, we need to prove that they
- \emph{respect} the relation. We follow the definition of respectfullness given
- by Homeier~\cite{Homeier05}. The intuition behind a respectfullness condition
- is that when a function (or constructor) is given arguments that are
- alpha-equivalent the results are also alpha equivalent. For arguments that are
- not of any of the relations taken into account, equivalence is replaced by
- equality. In particular the respectfullness condition for a @{text "bn"}
- function means that for alpha equivalent raw terms it returns the same bound
- names. Thanks to the restrictions on the binding functions introduced in
- Section~\ref{sec:alpha} we can show that are respectful.
+ Next we lift the permutation operations defined in \eqref{ceqvt} for
+ the raw term-constructors @{text "C"}. These facts contain, in addition
+ to the term-constructors, also permutations operations. Therefore
+ we have to know that permutation operations are respectful
+ w.r.t.~alpha-equivalence, which amounts to knowing that the
+ alpha-equivalence relations are equivariant, which we established
+ in Lemma~\ref{equiv}. As a result we can add the equations
+
+ \begin{equation}\label{ceqvt}
+ @{text "p \<bullet> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n) = C\<^sup>\<alpha> (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"}
+ \end{equation}
- \begin{lemma} The functions @{text "bn\<^isub>1 \<dots> bn\<^isub>m"}, @{text "fv_ty\<^isub>1 \<dots> fv_ty\<^isub>n"},
- the raw constructors, the raw permutations and @{text "\<approx>bn\<^isub>1 \<dots> \<approx>bn\<^isub>m"} are
- respectful w.r.t. the relations @{text "\<approx>\<^isub>1 \<dots> \<approx>\<^isub>n"}.
- \end{lemma}
- \begin{proof} Respectfullness of permutations is a direct consequence of
- equivariance. All other properties by induction on the alpha-equivalence
- relation. For @{text "bn"} the thesis follows by simple calculations thanks
- to the restrictions on the binding functions. For @{text "fv"} functions it
- follows using respectfullness of @{text "bn"}. For type constructors it is a
- simple calculation thanks to the way alpha-equivalence was defined. For @{text
- "alpha_bn"} after a second induction on the second relation by simple
- calculations. \end{proof}
+ \noindent
+ to our infrastructure. In a similar fashion we can lift the equations
+ characterising our free-variable functions and the binding functions.
+ The necessary respectfulness lemmas are
+ %
+ \begin{equation}\label{fnresp}
+ \mbox{%
+ \begin{tabular}{l}
+ @{text "x \<approx>ty y"} implies @{text "fv_ty x = fv_ty y"}\\
+ @{text "x \<approx>ty y"} implies @{text "bn x = bn y"}
+ \end{tabular}}
+ \end{equation}
- With these respectfullness properties we can use the quotient package
- to define the above constants on the quotient level. We can then automatically
- lift the theorems that talk about the raw constants to theorems on the quotient
- level. The following lifted properties are proved:
+ \noindent
+ which can be established by induction on @{text "\<approx>ty"}. While the first
+ kind of lemma is always ensured by way of how we defined the free variable
+ functions, the second does not hold in general. It only if the @{text bn}-functions
+ do not return any atom that is also bound. Hence our restriction imposed
+ on the binding functions that excludes this possibility.
+
+ Having the facts \eqref{fnresp} at our disposal, we can finally lift the
+ definitions that characterise when two terms of the form
\begin{center}
- \begin{tabular}{cp{7cm}}
-%skipped permute_zero and permute_add, since we do not have a permutation
-%definition
- $\bullet$ & permutation defining equations \\
- $\bullet$ & @{term "bn"} defining equations \\
- $\bullet$ & @{term "fv_ty"} and @{term "fv_bn"} defining equations \\
- $\bullet$ & induction. The induction principle that we obtain by lifting
- is the weak induction principle, just on the term structure \\
- $\bullet$ & quasi-injectivity. This means the equations that specify
- when two constructors are equal and comes from lifting the alpha
- equivalence defining relations\\
- $\bullet$ & distinctness\\
-%may be skipped
- $\bullet$ & equivariance of @{term "fv"} and @{term "bn"} functions\\
+ @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"}
+ \end{center}
+
+ \noindent
+ are alpha-equivalent. This gives us conditions when the corresponding
+ alpha-equated terms are equal, namely
+
+ \begin{center}
+ @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n = C\<^sup>\<alpha> y\<^isub>1 \<dots> y\<^isub>n"}
+ \end{center}
+
+ \noindent
+ We call these conditions as \emph{quasi-injectivity}. Except for one definition we have
+ to lift in the next section, this completes
+ the lifting part of establishing the reasoning infrastructure. From
+ now on we can ``forget'' about the raw types @{text "ty\<^bsub>1..n\<^esub>"} and only
+ reason with @{text "ty\<AL>\<^bsub>1..n\<^esub>"}
+
+ We can first show that the free-variable function and binding functions
+ are equivariant, namely
+
+ \begin{center}
+ \begin{tabular}{rcl}
+ @{text "p \<bullet> (fv_ty\<^sup>\<alpha> x)"} & $=$ & @{text "fv_ty\<^sup>\<alpha> (p \<bullet> x)"}\\
+ @{text "p \<bullet> (bn\<^sup>\<alpha> x)"} & $=$ & @{text "bn\<^sup>\<alpha> (p \<bullet> x)"}
\end{tabular}
\end{center}
- Until now we have not said anything about the support of the
- defined type. This is because we could not use the general definition of
- support in lifted theorems, since it does not preserve the relation.
- Indeed, take the term @{text "\<lambda>x. x"}. The support of the term is empty @{term "{}"},
- since the @{term "x"} is bound. On the raw level, before the binding is
- introduced the term has the support equal to @{text "{x}"}.
+ \noindent
+ These facts can be established by structural induction over the @{text x}.
+
+ Until now we have not yet derived any fact about the support of the
+ alpha-equated terms. Using the equivariance properties in \eqref{ceqvt} we can
+ show for every term-constructor @{text "C\<^sup>\<alpha>"} that
+
+ \begin{center}
+ @{text "supp x\<^isub>1 \<union> \<dots> supp x\<^isub>n supports (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"}
+ \end{center}
+
+ \noindent
+ holds. This together with Property~\ref{supportsprobs} allows us to show
+
- To show the support equations for the lifted types we want to use the
- Theorem \ref{suppabs}, so we start with showing that they have a finite
- support.
+ \begin{center}
+ @{text "finite (supp x\<^isub>i)"}
+ \end{center}
- \begin{lemma} The types @{text "ty\<^isup>\<alpha>\<^isub>1 \<dots> ty\<^isup>\<alpha>\<^isub>n"} have finite support.
+ \noindent
+ by mutual structural induction over @{text "x\<^isub>1, \<dots>, x\<^isub>n"} (whereby @{text "x\<^isub>i"} ranges over the types
+ @{text "ty\<AL>\<^isub>1 \<dots> ty\<AL>\<^isub>n"}). Lastly, we can show that the support of elements in
+ @{text "ty\<AL>\<^bsub>1..n\<^esub>"} coincides with @{text "fv_ty\<AL>\<^bsub>1..n\<^esub>"}.
+
+ \begin{lemma} For every @{text "x\<^isub>i"} of type @{text "ty\<AL>\<^bsub>1..n\<^esub>"}, we have that
+ @{text "supp x\<^isub>i = fv_ty\<AL>\<^isub>i x\<^isub>i"} holds.
\end{lemma}
+
\begin{proof}
- By induction on the lifted types. For each constructor its support is
- supported by the union of the supports of all arguments. By induction
- hypothesis we know that each of the recursive arguments has finite
- support. We also know that atoms and finite atom sets and lists that
- occur in the constructors have finite support. A union of finite
- sets is finite thus the support of the constructor is finite.
+ The proof proceeds by structural induction over the @{text "x\<^isub>i"}. In each case
+ we unfold the definition of @{text "supp"}, move the swapping inside the
+ term-constructors and the use the quasi-injectivity lemmas in order to complete the
+ proof.
\end{proof}
-% Very vague...
- \begin{lemma} For each lifted type @{text "ty\<^isup>\<alpha>\<^isub>i"}, for every @{text "x"}
- of this type:
- \begin{equation}
- @{term "supp x = fv_ty\<^isup>\<alpha>\<^isub>i x"}.
- \end{equation}
- \end{lemma}
- \begin{proof}
- We will show this by induction together with equations that characterize
- @{term "fv_bn\<^isup>\<alpha>\<^isub>"} in terms of @{term "alpha_bn\<^isup>\<alpha>"}. For each of @{text "fv_bn\<^isup>\<alpha>"}
- functions this equation is:
- \begin{center}
- @{term "{a. infinite {b. \<not> alpha_bn\<^isup>\<alpha> ((a \<rightleftharpoons> b) \<bullet> x) x}} = fv_bn\<^isup>\<alpha> x"}
- \end{center}
+ \noindent
+ To sum up this section, we established a reasoning infrastructure
+ for the types @{text "ty\<AL>\<^isub>1 \<dots> ty\<AL>\<^isub>n"}
+ by first lifting definitions from the raw level to the quotient level and
+ then establish facts about these lifted definitions. All necessary proofs
+ are generated automatically by custom ML-code. This code can deal with
+ specifications as shown in Figure~\ref{nominalcorehas} for Core-Haskell.
- In the induction we need to show these equations together with the goal
- for the appropriate constructors. We first transform the right hand sides.
- The free variable functions are applied to theirs respective constructors
- so we can apply the lifted free variable defining equations to obtain
- free variable functions applied to subterms minus binders. Using the
- induction hypothesis we can replace free variable functions applied to
- subterms by support. Using Theorem \ref{suppabs} we replace the differences
- by supports of appropriate abstractions.
-
- Unfolding the definition of supports on both sides of the equations we
- obtain by simple calculations the equalities.
- \end{proof}
+ \begin{figure}[t!]
+ \begin{boxedminipage}{\linewidth}
+ \small
+ \begin{tabular}{l}
+ \isacommand{atom\_decl}~@{text "var"}\\
+ \isacommand{atom\_decl}~@{text "cvar"}\\
+ \isacommand{atom\_decl}~@{text "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{bind}~@{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{bind}~@{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{bind}~@{text "tv"}~\isacommand{in}~@{text t}\\
+ $|$~@{text "LAM_cty cv::cvar ckind t::trm"} \isacommand{bind}~@{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{bind}~@{text "v"}~\isacommand{in}~@{text t}\\
+ $|$~@{text "Let x::var ty trm t::trm"} \isacommand{bind}~@{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{bind}~@{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. At 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}
+*}
- With the above equations we can substitute free variables for support in
- the lifted free variable equations, which gives us the support equations
- for the term constructors. With this we can show that for each binding in
- a constructors the bindings can be renamed. To rename a shallow binder
- or a deep recursive binder a permutation is sufficient. This is not the
- case for a deep non-recursive bindings. Take the term
- @{text "Let (ACons x (Vr x) ANil) (Vr x)"}, representing the language construct
- @{text "let x = x in x"}. To rename the binder the permutation cannot
- be applied to the whole assignment since it would rename the free @{term "x"}
- as well. To avoid this we introduce a new construction operation
- that applies a permutation under a binding function.
-
-*}
section {* Strong Induction Principles *}
@@ -1808,83 +1876,8 @@
}
\end{equation}
-
-
*}
-text {*
-
- \begin{figure}[t!]
- \begin{boxedminipage}{\linewidth}
- \small
- \begin{tabular}{l}
- \isacommand{atom\_decl}~@{text "var"}\\
- \isacommand{atom\_decl}~@{text "cvar"}\\
- \isacommand{atom\_decl}~@{text "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{bind}~@{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{bind}~@{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{bind}~@{text "tv"}~\isacommand{in}~@{text t}\\
- $|$~@{text "LAM_cty cv::cvar ckind t::trm"} \isacommand{bind}~@{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{bind}~@{text "v"}~\isacommand{in}~@{text t}\\
- $|$~@{text "Let x::var ty trm t::trm"} \isacommand{bind}~@{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{bind}~@{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. At 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 {* Related Work *}