
diff -r 9a894c42e80e -r a2d5f9ea17ad Paper/Paper.thy
--- 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 *}
 




