--- a/Paper/Paper.thy Mon Oct 04 07:25:37 2010 +0100
+++ b/Paper/Paper.thy Mon Oct 04 12:39:57 2010 +0100
@@ -61,11 +61,11 @@
So far, Nominal Isabelle provided a mechanism for constructing
$\alpha$-equated terms, for example lambda-terms
-
+ %
\begin{center}
@{text "t ::= x | t t | \<lambda>x. t"}
\end{center}
-
+ %
\noindent
where free and bound variables have names. For such $\alpha$-equated terms,
Nominal Isabelle derives automatically a reasoning infrastructure that has
@@ -87,7 +87,7 @@
@{text "S ::= \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. T"}
\end{array}
\end{equation}
-
+ %
\noindent
and the @{text "\<forall>"}-quantification binds a finite (possibly empty) set of
type-variables. While it is possible to implement this kind of more general
@@ -96,7 +96,7 @@
why Nominal Isabelle and similar theorem provers that only provide
mechanisms for binding single variables have not fared extremely well with the
more advanced tasks in the POPLmark challenge \cite{challenge05}, because
- also there one would like to bind multiple variables at once.
+ also there one would like to bind multiple variables at once.
Binding multiple variables has interesting properties that cannot be captured
easily by iterating single binders. For example in the case of type-schemes we do not
@@ -106,7 +106,7 @@
\begin{equation}\label{ex1}
@{text "\<forall>{x, y}. x \<rightarrow> y \<approx>\<^isub>\<alpha> \<forall>{y, x}. x \<rightarrow> y"}
\end{equation}
-
+ %
\noindent
but assuming that @{text x}, @{text y} and @{text z} are distinct variables,
the following two should \emph{not} be $\alpha$-equivalent
@@ -114,7 +114,7 @@
\begin{equation}\label{ex2}
@{text "\<forall>{x, y}. x \<rightarrow> y \<notapprox>\<^isub>\<alpha> \<forall>{z}. z \<rightarrow> z"}
\end{equation}
-
+ %
\noindent
Moreover, we like to regard type-schemes as $\alpha$-equivalent, if they differ
only on \emph{vacuous} binders, such as
@@ -122,7 +122,7 @@
\begin{equation}\label{ex3}
@{text "\<forall>{x}. x \<rightarrow> y \<approx>\<^isub>\<alpha> \<forall>{x, z}. x \<rightarrow> y"}
\end{equation}
-
+ %
\noindent
where @{text z} does not occur freely in the type. In this paper we will
give a general binding mechanism and associated notion of $\alpha$-equivalence
@@ -146,7 +146,7 @@
\begin{center}
@{text "\<LET> x = 3 \<AND> y = 2 \<AND> z = loop \<IN> x - y \<END>"}
\end{center}
-
+ %
\noindent
Therefore we will also provide a separate binding mechanism for cases in
which the order of binders does not matter, but the ``cardinality'' of the
@@ -159,7 +159,7 @@
\begin{equation}\label{two}
@{text "\<LET> (x, y) = (3, 2) \<IN> x - y \<END>"}
\end{equation}
-
+ %
\noindent
we want to bind all variables from the pattern inside the body of the
$\mathtt{let}$, but we also care about the order of these variables, since
@@ -172,7 +172,8 @@
\noindent
As a result, we provide three general binding mechanisms each of which binds
multiple variables at once, and let the user chose which one is intended
- when formalising a term-calculus.
+ in a formalisation.
+ %%when formalising a term-calculus.
By providing these general binding mechanisms, however, we have to work
around a problem that has been pointed out by Pottier \cite{Pottier06} and
@@ -181,18 +182,17 @@
\begin{center}
@{text "\<LET> x\<^isub>1 = t\<^isub>1 \<AND> \<dots> \<AND> x\<^isub>n = t\<^isub>n \<IN> s \<END>"}
\end{center}
-
+ %
\noindent
- which bind all the @{text "x\<^isub>i"} in @{text s}, we might not care
- about the order in which the @{text "x\<^isub>i = t\<^isub>i"} are given,
- but we do care about the information that there are as many @{text
+ we care about the
+ information that there are as many bound variables @{text
"x\<^isub>i"} as there are @{text "t\<^isub>i"}. We lose this information if
we represent the @{text "\<LET>"}-constructor by something like
%
\begin{center}
@{text "\<LET> (\<lambda>x\<^isub>1\<dots>x\<^isub>n . s) [t\<^isub>1,\<dots>,t\<^isub>n]"}
\end{center}
-
+ %
\noindent
where the notation @{text "\<lambda>_ . _"} indicates that the list of @{text
"x\<^isub>i"} becomes bound in @{text s}. In this representation the term
@@ -204,45 +204,47 @@
allow type specifications for @{text "\<LET>"}s as follows
%
\begin{center}
- \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l}
- @{text trm} & @{text "::="} & @{text "\<dots>"}\\
- & @{text "|"} & @{text "\<LET> as::assn s::trm"}\hspace{4mm}
+ \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}cl}
+ @{text trm} & @{text "::="} & @{text "\<dots>"}
+ & @{text "|"} @{text "\<LET> as::assn s::trm"}\hspace{2mm}
\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}\\[1mm]
- @{text assn} & @{text "::="} & @{text "\<ANIL>"}\\
- & @{text "|"} & @{text "\<ACONS> name trm assn"}
+ @{text assn} & @{text "::="} & @{text "\<ANIL>"}
+ & @{text "|"} @{text "\<ACONS> name trm assn"}
\end{tabular}
\end{center}
-
+ %
\noindent
where @{text assn} is an auxiliary type representing a list of assignments
and @{text bn} an auxiliary function identifying the variables to be bound
by the @{text "\<LET>"}. This function can be defined by recursion over @{text
assn} as follows
-
+ %
\begin{center}
@{text "bn(\<ANIL>) ="} @{term "{}"} \hspace{5mm}
@{text "bn(\<ACONS> x t as) = {x} \<union> bn(as)"}
\end{center}
-
+ %
\noindent
The scope of the binding is indicated by labels given to the types, for
example @{text "s::trm"}, and a binding clause, in this case
\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}. This binding
clause states that all the names the function @{text
"bn(as)"} returns should be bound in @{text s}. This style of specifying terms and bindings is heavily
- inspired by the syntax of the Ott-tool \cite{ott-jfp}. Though, Ott
- has only one binding mode, namely the one where the order of
- binders matters. Consequently, type-schemes with binding sets
- of names cannot be modelled in Ott.
+ inspired by the syntax of the Ott-tool \cite{ott-jfp}.
+
+ %Though, Ott
+ %has only one binding mode, namely the one where the order of
+ %binders matters. Consequently, type-schemes with binding sets
+ %of names cannot be modelled in Ott.
However, we will not be able to cope with all specifications that are
allowed by Ott. One reason is that Ott lets the user specify ``empty''
types like
-
+ %
\begin{center}
@{text "t ::= t t | \<lambda>x. t"}
\end{center}
-
+ %
\noindent
where no clause for variables is given. Arguably, such specifications make
some sense in the context of Coq's type theory (which Ott supports), but not
@@ -279,12 +281,12 @@
Although in informal settings a reasoning infrastructure for $\alpha$-equated
terms is nearly always taken for granted, establishing it automatically in
- the Isabelle/HOL theorem prover is a rather non-trivial task. For every
+ the Isabelle/HOL is a rather non-trivial task. For every
specification we will need to construct a type containing as elements the
$\alpha$-equated terms. To do so, we use the standard HOL-technique of defining
a new type by identifying a non-empty subset of an existing type. The
construction we perform in Isabelle/HOL can be illustrated by the following picture:
-
+ %
\begin{center}
\begin{tikzpicture}
%\draw[step=2mm] (-4,-1) grid (4,1);
@@ -308,7 +310,7 @@
\end{tikzpicture}
\end{center}
-
+ %
\noindent
We take as the starting point a definition of raw terms (defined as a
datatype in Isabelle/HOL); then identify the $\alpha$-equivalence classes in
@@ -318,12 +320,12 @@
in Isabelle/HOL and the property that our relation for $\alpha$-equivalence is
indeed an equivalence relation).
- The fact that we obtain an isomorphism between the new type and the
- non-empty subset shows that the new type is a faithful representation of
- $\alpha$-equated terms. That is not the case for example for terms using the
- locally nameless representation of binders \cite{McKinnaPollack99}: in this
- representation there are ``junk'' terms that need to be excluded by
- reasoning about a well-formedness predicate.
+ %The fact that we obtain an isomorphism between the new type and the
+ %non-empty subset shows that the new type is a faithful representation of
+ %$\alpha$-equated terms. That is not the case for example for terms using the
+ %locally nameless representation of binders \cite{McKinnaPollack99}: in this
+ %representation there are ``junk'' terms that need to be excluded by
+ %reasoning about a well-formedness predicate.
The problem with introducing a new type in Isabelle/HOL is that in order to
be useful, a reasoning infrastructure needs to be ``lifted'' from the
@@ -335,8 +337,8 @@
define the free-variable function over raw lambda-terms
\begin{center}
- @{text "fv(x) = {x}"}\hspace{10mm}
- @{text "fv(t\<^isub>1 t\<^isub>2) = fv(t\<^isub>1) \<union> fv(t\<^isub>2)"}\\[1mm]
+ @{text "fv(x) = {x}"}\hspace{8mm}
+ @{text "fv(t\<^isub>1 t\<^isub>2) = fv(t\<^isub>1) \<union> fv(t\<^isub>2)"}\hspace{8mm}
@{text "fv(\<lambda>x.t) = fv(t) - {x}"}
\end{center}
@@ -346,8 +348,8 @@
lifted function is characterised by the equations
\begin{center}
- @{text "fv\<^sup>\<alpha>(x) = {x}"}\hspace{10mm}
- @{text "fv\<^sup>\<alpha>(t\<^isub>1 t\<^isub>2) = fv\<^sup>\<alpha>(t\<^isub>1) \<union> fv\<^sup>\<alpha>(t\<^isub>2)"}\\[1mm]
+ @{text "fv\<^sup>\<alpha>(x) = {x}"}\hspace{8mm}
+ @{text "fv\<^sup>\<alpha>(t\<^isub>1 t\<^isub>2) = fv\<^sup>\<alpha>(t\<^isub>1) \<union> fv\<^sup>\<alpha>(t\<^isub>2)"}\hspace{8mm}
@{text "fv\<^sup>\<alpha>(\<lambda>x.t) = fv\<^sup>\<alpha>(t) - {x}"}
\end{center}
@@ -365,14 +367,12 @@
infrastructure for $\alpha$-equated terms.
The examples we have in mind where our reasoning infrastructure will be
- helpful includes the term language of System @{text "F\<^isub>C"}, also
- known as Core-Haskell (see Figure~\ref{corehas}). This term language
+ helpful includes the term language of Core-Haskell. This term language
involves patterns that have lists of type-, coercion- and term-variables,
- all of which are bound in @{text "\<CASE>"}-expressions. One
- feature is that we do not know in advance how many variables need to
- be bound. Another is that each bound variable comes with a kind or type
- annotation. Representing such binders with single binders and reasoning
- about them in a theorem prover would be a major pain. \medskip
+ all of which are bound in @{text "\<CASE>"}-expressions. In these
+ patterns we do not know in advance how many variables need to
+ be bound. Another example is the specification of SML, which includes
+ includes bindings as in type-schemes.\medskip
\noindent
{\bf Contributions:} We provide three new definitions for when terms
@@ -384,53 +384,54 @@
induction principles that have the variable convention already built in.
The method behind our specification of general binders is taken
from the Ott-tool, but we introduce crucial restrictions, and also extensions, so
- that our specifications make sense for reasoning about $\alpha$-equated terms. The main improvement over Ott is that we introduce three binding modes,
- provide precise definitions for $\alpha$-equivalence and for free
- variables of our terms, and provide automated proofs inside the
- Isabelle theorem prover.
+ that our specifications make sense for reasoning about $\alpha$-equated terms.
+ The main improvement over Ott is that we introduce three binding modes
+ (only one is present in Ott), provide definitions for $\alpha$-equivalence and
+ for free variables of our terms, and also derive a reasoning infrastructure
+ about our specifications inside Isabelle/HOL.
- \begin{figure}
- \begin{boxedminipage}{\linewidth}
- \begin{center}
- \begin{tabular}{r@ {\hspace{1mm}}r@ {\hspace{2mm}}l}
- \multicolumn{3}{@ {}l}{Type Kinds}\\
- @{text "\<kappa>"} & @{text "::="} & @{text "\<star> | \<kappa>\<^isub>1 \<rightarrow> \<kappa>\<^isub>2"}\smallskip\\
- \multicolumn{3}{@ {}l}{Coercion Kinds}\\
- @{text "\<iota>"} & @{text "::="} & @{text "\<sigma>\<^isub>1 \<sim> \<sigma>\<^isub>2"}\smallskip\\
- \multicolumn{3}{@ {}l}{Types}\\
- @{text "\<sigma>"} & @{text "::="} & @{text "a | T | \<sigma>\<^isub>1 \<sigma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<sigma>"}}$@{text "\<^sup>n"}
- @{text "| \<forall>a:\<kappa>. \<sigma> | \<iota> \<Rightarrow> \<sigma>"}\smallskip\\
- \multicolumn{3}{@ {}l}{Coercion Types}\\
- @{text "\<gamma>"} & @{text "::="} & @{text "c | C | \<gamma>\<^isub>1 \<gamma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<gamma>"}}$@{text "\<^sup>n"}
- @{text "| \<forall>c:\<iota>. \<gamma> | \<iota> \<Rightarrow> \<gamma> "}\\
- & @{text "|"} & @{text "refl \<sigma> | sym \<gamma> | \<gamma>\<^isub>1 \<circ> \<gamma>\<^isub>2 | \<gamma> @ \<sigma> | left \<gamma> | right \<gamma>"}\\
- & @{text "|"} & @{text "\<gamma>\<^isub>1 \<sim> \<gamma>\<^isub>2 | rightc \<gamma> | leftc \<gamma> | \<gamma>\<^isub>1 \<triangleright> \<gamma>\<^isub>2"}\smallskip\\
- \multicolumn{3}{@ {}l}{Terms}\\
- @{text "e"} & @{text "::="} & @{text "x | K | \<Lambda>a:\<kappa>. e | \<Lambda>c:\<iota>. e | e \<sigma> | e \<gamma>"}\\
- & @{text "|"} & @{text "\<lambda>x:\<sigma>. e | e\<^isub>1 e\<^isub>2 | \<LET> x:\<sigma> = e\<^isub>1 \<IN> e\<^isub>2"}\\
- & @{text "|"} & @{text "\<CASE> e\<^isub>1 \<OF>"}$\;\overline{@{text "p \<rightarrow> e\<^isub>2"}}$ @{text "| e \<triangleright> \<gamma>"}\smallskip\\
- \multicolumn{3}{@ {}l}{Patterns}\\
- @{text "p"} & @{text "::="} & @{text "K"}$\;\overline{@{text "a:\<kappa>"}}\;\overline{@{text "c:\<iota>"}}\;\overline{@{text "x:\<sigma>"}}$\smallskip\\
- \multicolumn{3}{@ {}l}{Constants}\\
- & @{text C} & coercion constants\\
- & @{text T} & value type constructors\\
- & @{text "S\<^isub>n"} & n-ary type functions (which need to be fully applied)\\
- & @{text K} & data constructors\smallskip\\
- \multicolumn{3}{@ {}l}{Variables}\\
- & @{text a} & type variables\\
- & @{text c} & coercion variables\\
- & @{text x} & term variables\\
- \end{tabular}
- \end{center}
- \end{boxedminipage}
- \caption{The System @{text "F\<^isub>C"}
- \cite{CoreHaskell}, also often referred to as \emph{Core-Haskell}. In this
- version of @{text "F\<^isub>C"} we made a modification by separating the
- grammars for type kinds and coercion kinds, as well as for types and coercion
- types. For this paper the interesting term-constructor is @{text "\<CASE>"},
- which binds multiple type-, coercion- and term-variables.\label{corehas}}
- \end{figure}
+ %\begin{figure}
+ %\begin{boxedminipage}{\linewidth}
+ %%\begin{center}
+ %\begin{tabular}{r@ {\hspace{1mm}}r@ {\hspace{2mm}}l}
+ %\multicolumn{3}{@ {}l}{Type Kinds}\\
+ %@{text "\<kappa>"} & @{text "::="} & @{text "\<star> | \<kappa>\<^isub>1 \<rightarrow> \<kappa>\<^isub>2"}\smallskip\\
+ %\multicolumn{3}{@ {}l}{Coercion Kinds}\\
+ %@{text "\<iota>"} & @{text "::="} & @{text "\<sigma>\<^isub>1 \<sim> \<sigma>\<^isub>2"}\smallskip\\
+ %\multicolumn{3}{@ {}l}{Types}\\
+ %@{text "\<sigma>"} & @{text "::="} & @{text "a | T | \<sigma>\<^isub>1 \<sigma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<sigma>"}}$@{text "\<^sup>n"}
+ %@{text "| \<forall>a:\<kappa>. \<sigma> | \<iota> \<Rightarrow> \<sigma>"}\smallskip\\
+ %\multicolumn{3}{@ {}l}{Coercion Types}\\
+ %@{text "\<gamma>"} & @{text "::="} & @{text "c | C | \<gamma>\<^isub>1 \<gamma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<gamma>"}}$@{text "\<^sup>n"}
+ %@{text "| \<forall>c:\<iota>. \<gamma> | \<iota> \<Rightarrow> \<gamma> "}\\
+ %& @{text "|"} & @{text "refl \<sigma> | sym \<gamma> | \<gamma>\<^isub>1 \<circ> \<gamma>\<^isub>2 | \<gamma> @ \<sigma> | left \<gamma> | right \<gamma>"}\\
+ %& @{text "|"} & @{text "\<gamma>\<^isub>1 \<sim> \<gamma>\<^isub>2 | rightc \<gamma> | leftc \<gamma> | \<gamma>\<^isub>1 \<triangleright> \<gamma>\<^isub>2"}\smallskip\\
+ %\multicolumn{3}{@ {}l}{Terms}\\
+ %@{text "e"} & @{text "::="} & @{text "x | K | \<Lambda>a:\<kappa>. e | \<Lambda>c:\<iota>. e | e \<sigma> | e \<gamma>"}\\
+ %& @{text "|"} & @{text "\<lambda>x:\<sigma>. e | e\<^isub>1 e\<^isub>2 | \<LET> x:\<sigma> = e\<^isub>1 \<IN> e\<^isub>2"}\\
+ %& @{text "|"} & @{text "\<CASE> e\<^isub>1 \<OF>"}$\;\overline{@{text "p \<rightarrow> e\<^isub>2"}}$ @{text "| e \<triangleright> \<gamma>"}\smallskip\\
+ %\multicolumn{3}{@ {}l}{Patterns}\\
+ %@{text "p"} & @{text "::="} & @{text "K"}$\;\overline{@{text "a:\<kappa>"}}\;\overline{@{text "c:\<iota>"}}\;\overline{@{text "x:\<sigma>"}}$\smallskip\\
+ %\multicolumn{3}{@ {}l}{Constants}\\
+ %& @{text C} & coercion constants\\
+ %& @{text T} & value type constructors\\
+ %& @{text "S\<^isub>n"} & n-ary type functions (which need to be fully applied)\\
+ %& @{text K} & data constructors\smallskip\\
+ %\multicolumn{3}{@ {}l}{Variables}\\
+ %& @{text a} & type variables\\
+ %& @{text c} & coercion variables\\
+ %& @{text x} & term variables\\
+ %\end{tabular}
+ %\end{center}
+ %\end{boxedminipage}
+ %\caption{The System @{text "F\<^isub>C"}
+ %\cite{CoreHaskell}, also often referred to as \emph{Core-Haskell}. In this
+ %version of @{text "F\<^isub>C"} we made a modification by separating the
+ %grammars for type kinds and coercion kinds, as well as for types and coercion
+ %types. For this paper the interesting term-constructor is @{text "\<CASE>"},
+ %which binds multiple type-, coercion- and term-variables.\label{corehas}}
+ %\end{figure}
*}
section {* A Short Review of the Nominal Logic Work *}
@@ -454,12 +455,7 @@
Permutations are bijective functions from atoms to atoms that are
the identity everywhere except on a finite number of atoms. There is a
two-place permutation operation written
- %
- \begin{center}
@{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
- \end{center}
-
- \noindent
in which the generic type @{text "\<beta>"} stands for the type of the object
over which the permutation
acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"},
@@ -470,7 +466,7 @@
given by:
%
\begin{equation}\label{permute}
- \mbox{\begin{tabular}{@ {}cc@ {}}
+ \mbox{\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
\begin{tabular}{@ {}l@ {}}
@{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\[2mm]
@{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\
@@ -479,7 +475,7 @@
\begin{tabular}{@ {}l@ {}}
@{thm permute_set_eq[no_vars, THEN eq_reflection]}\\
@{text "p \<bullet> f \<equiv> \<lambda>x. p \<bullet> (f (- p \<bullet> x))"}\\
- @{thm permute_bool_def[no_vars, THEN eq_reflection]}\\
+ @{thm permute_bool_def[no_vars, THEN eq_reflection]}
\end{tabular}
\end{tabular}}
\end{equation}
@@ -507,13 +503,7 @@
\noindent
There is also the derived notion for when an atom @{text a} is \emph{fresh}
- for an @{text x}, defined as
- %
- \begin{center}
- @{thm fresh_def[no_vars]}
- \end{center}
-
- \noindent
+ for an @{text x}, defined as @{thm fresh_def[no_vars]}.
We use for sets of atoms the abbreviation
@{thm (lhs) fresh_star_def[no_vars]}, defined as
@{thm (rhs) fresh_star_def[no_vars]}.
@@ -530,65 +520,74 @@
described, for example for atoms, products, lists, function applications,
booleans and permutations as follows
%
- \begin{eqnarray}
- @{term "supp a"} & = & @{term "{a}"}\\
- @{term "supp (x, y)"} & = & @{term "supp x \<union> supp y"}\\
- @{term "supp []"} & = & @{term "{}"}\\
- @{term "supp (x#xs)"} & = & @{term "supp x \<union> supp xs"}\\
- @{text "supp (f x)"} & @{text "\<subseteq>"} & @{term "supp f \<union> supp x"}\label{suppfun}\\
- @{term "supp b"} & = & @{term "{}"}\\
- @{term "supp p"} & = & @{term "{a. p \<bullet> a \<noteq> a}"}
- \end{eqnarray}
+ \begin{center}
+ \begin{tabular}{c@ {\hspace{10mm}}c}
+ \begin{tabular}{rcl}
+ @{term "supp a"} & $=$ & @{term "{a}"}\\
+ @{term "supp (x, y)"} & $=$ & @{term "supp x \<union> supp y"}\\
+ @{term "supp []"} & $=$ & @{term "{}"}\\
+ @{term "supp (x#xs)"} & $=$ & @{term "supp x \<union> supp xs"}\\
+ \end{tabular}
+ &
+ \begin{tabular}{rcl}
+ @{text "supp (f x)"} & @{text "\<subseteq>"} & @{term "supp f \<union> supp x"}\\
+ @{term "supp b"} & $=$ & @{term "{}"}\\
+ @{term "supp p"} & $=$ & @{term "{a. p \<bullet> a \<noteq> a}"}
+ \end{tabular}
+ \end{tabular}
+ \end{center}
\noindent
in some cases it can be difficult to characterise the support precisely, and
- only an approximation can be established (see \eqref{suppfun} above). Reasoning about
- such approximations can be simplified with the notion \emph{supports}, defined
- as follows:
-
- \begin{definition}
- A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b}
- not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.
- \end{definition}
+ only an approximation can be established (as for functions above).
- \noindent
- The main point of @{text supports} is that we can establish the following
- two properties.
-
- \begin{property}\label{supportsprop}
- Given a set @{text "as"} of atoms.
- {\it (i)} @{thm[mode=IfThen] supp_is_subset[where S="as", no_vars]}
- {\it (ii)} @{thm supp_supports[no_vars]}.
- \end{property}
-
- Another important notion in the nominal logic work is \emph{equivariance}.
- For a function @{text f}, say of type @{text "\<alpha> \<Rightarrow> \<beta>"}, to be equivariant
- it is required that every permutation leaves @{text f} unchanged, that is
+ %Reasoning about
+ %such approximations can be simplified with the notion \emph{supports}, defined
+ %as follows:
+ %
+ %\begin{definition}
+ %A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b}
+ %not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.
+ %\end{definition}
+ %
+ %\noindent
+ %The main point of @{text supports} is that we can establish the following
+ %two properties.
+ %
+ %\begin{property}\label{supportsprop}
+ %Given a set @{text "as"} of atoms.
+ %{\it (i)} @{thm[mode=IfThen] supp_is_subset[where S="as", no_vars]}
+ %{\it (ii)} @{thm supp_supports[no_vars]}.
+ %\end{property}
%
- \begin{equation}\label{equivariancedef}
- @{term "\<forall>p. p \<bullet> f = f"}
- \end{equation}
-
- \noindent or equivalently that a permutation applied to the application
- @{text "f x"} can be moved to the argument @{text x}. That means for equivariant
- functions @{text f}, we have for all permutations @{text p}:
+ %Another important notion in the nominal logic work is \emph{equivariance}.
+ %For a function @{text f}, say of type @{text "\<alpha> \<Rightarrow> \<beta>"}, to be equivariant
+ %it is required that every permutation leaves @{text f} unchanged, that is
+ %%
+ %\begin{equation}\label{equivariancedef}
+ %@{term "\<forall>p. p \<bullet> f = f"}
+ %\end{equation}
%
- \begin{equation}\label{equivariance}
- @{text "p \<bullet> f = f"} \;\;\;\textit{if and only if}\;\;\;
- @{text "p \<bullet> (f x) = f (p \<bullet> x)"}
- \end{equation}
-
- \noindent
- From property \eqref{equivariancedef} and the definition of @{text supp}, we
- can easily deduce that equivariant functions have empty support. There is
- also a similar notion for equivariant relations, say @{text R}, namely the property
- that
- %
- \begin{center}
- @{text "x R y"} \;\;\textit{implies}\;\; @{text "(p \<bullet> x) R (p \<bullet> y)"}
- \end{center}
+ %\noindent or equivalently that a permutation applied to the application
+ %@{text "f x"} can be moved to the argument @{text x}. That means for equivariant
+ %functions @{text f}, we have for all permutations @{text p}:
+ %%
+ %\begin{equation}\label{equivariance}
+ %@{text "p \<bullet> f = f"} \;\;\;\textit{if and only if}\;\;\;
+ %@{text "p \<bullet> (f x) = f (p \<bullet> x)"}
+ %\end{equation}
+ %
+ %\noindent
+ %From property \eqref{equivariancedef} and the definition of @{text supp}, we
+ %can easily deduce that equivariant functions have empty support. There is
+ %also a similar notion for equivariant relations, say @{text R}, namely the property
+ %that
+ %%
+ %\begin{center}
+ %@{text "x R y"} \;\;\textit{implies}\;\; @{text "(p \<bullet> x) R (p \<bullet> y)"}
+ %\end{center}
- Finally, the nominal logic work provides us with general means for renaming
+ Using support and freshness, the nominal logic work provides us with general means for renaming
binders. While in the older version of Nominal Isabelle, we used extensively
Property~\ref{swapfreshfresh} to rename single binders, this property
proved too unwieldy for dealing with multiple binders. For such binders the
@@ -649,15 +648,15 @@
{\it (iii)} ``moves'' their bound names so that we obtain modulo a relation,
say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it (iv)}
@{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
- requirements {\it (i)} to {\it (iv)} can be stated formally as follows:
+ requirements {\it (i)} to {\it (iv)} can be stated formally as the conjunction of:
%
\begin{equation}\label{alphaset}
- \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
- \multicolumn{3}{l}{@{term "(as, x) \<approx>set R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
- & @{term "fa(x) - as = fa(y) - bs"} & \mbox{\it (i)}\\
- @{text "\<and>"} & @{term "(fa(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
- @{text "\<and>"} & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
- @{text "\<and>"} & @{term "(p \<bullet> as) = bs"} & \mbox{\it (iv)}\\
+ \begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l}
+ \multicolumn{4}{l}{@{term "(as, x) \<approx>set R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+ \mbox{\it (i)} & @{term "fa(x) - as = fa(y) - bs"} &
+ \mbox{\it (iii)} & @{text "(p \<bullet> x) R y"} \\
+ \mbox{\it (ii)} & @{term "(fa(x) - as) \<sharp>* p"} &
+ \mbox{\it (iv)} & @{term "(p \<bullet> as) = bs"} \\
\end{array}
\end{equation}
@@ -677,12 +676,12 @@
as follows
%
\begin{equation}\label{alphalist}
- \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
- \multicolumn{2}{l}{@{term "(as, x) \<approx>lst R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
- & @{term "fa(x) - (set as) = fa(y) - (set bs)"} & \mbox{\it (i)}\\
- \wedge & @{term "(fa(x) - set as) \<sharp>* p"} & \mbox{\it (ii)}\\
- \wedge & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
- \wedge & @{term "(p \<bullet> as) = bs"} & \mbox{\it (iv)}\\
+ \begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l}
+ \multicolumn{4}{l}{@{term "(as, x) \<approx>lst R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+ \mbox{\it (i)} & @{term "fa(x) - (set as) = fa(y) - (set bs)"} &
+ \mbox{\it (iii)} & @{text "(p \<bullet> x) R y"}\\
+ \mbox{\it (ii)} & @{term "(fa(x) - set as) \<sharp>* p"} &
+ \mbox{\it (iv)} & @{term "(p \<bullet> as) = bs"}\\
\end{array}
\end{equation}
@@ -696,11 +695,11 @@
condition in \eqref{alphaset}:
%
\begin{equation}\label{alphares}
- \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
+ \begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l}
\multicolumn{2}{l}{@{term "(as, x) \<approx>res R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
- & @{term "fa(x) - as = fa(y) - bs"} & \mbox{\it (i)}\\
- \wedge & @{term "(fa(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
- \wedge & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
+ \mbox{\it (i)} & @{term "fa(x) - as = fa(y) - bs"} &
+ \mbox{\it (iii)} & @{text "(p \<bullet> x) R y"}\\
+ \mbox{\it (ii)} & @{term "(fa(x) - as) \<sharp>* p"}\\
\end{array}
\end{equation}
@@ -780,90 +779,92 @@
abstractions, namely:
\begin{theorem}[Support of Abstractions]\label{suppabs}
- Assuming @{text x} has finite support, then\\[-6mm]
+ Assuming @{text x} has finite support, then
+
\begin{center}
- \begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
- @{thm (lhs) supp_Abs(1)[no_vars]} & $=$ & @{thm (rhs) supp_Abs(1)[no_vars]}\\
- @{thm (lhs) supp_Abs(2)[no_vars]} & $=$ & @{thm (rhs) supp_Abs(2)[no_vars]}\\
- @{thm (lhs) supp_Abs(3)[where bs="as", no_vars]} & $=$ & @{thm (rhs) supp_Abs(3)[where bs="as", no_vars]}
+ \begin{tabular}{l}
+ @{thm (lhs) supp_Abs(1)[no_vars]} $=$
+ @{thm supp_Abs(2)[no_vars]}, and\\
+ @{thm supp_Abs(3)[where bs="as", no_vars]}
\end{tabular}
\end{center}
\end{theorem}
\noindent
- Below we will show the first equation. The others
- follow by similar arguments. By definition of the abstraction type @{text "abs_set"}
- we have
- %
- \begin{equation}\label{abseqiff}
- @{thm (lhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\;
- @{thm (rhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]}
- \end{equation}
-
- \noindent
- and also
- %
- \begin{equation}\label{absperm}
- @{thm permute_Abs[no_vars]}
- \end{equation}
+ This theorem states that the bound names do not appear in the support, as expected.
+ For brevity we omit the proof of this resul and again refer the reader to
+ our formalisation in Isabelle/HOL.
- \noindent
- The second fact derives from the definition of permutations acting on pairs
- \eqref{permute} and $\alpha$-equivalence being equivariant
- (see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show
- the following lemma about swapping two atoms in an abstraction.
-
- \begin{lemma}
- @{thm[mode=IfThen] Abs_swap1(1)[where bs="as", no_vars]}
- \end{lemma}
+ %\noindent
+ %Below we will show the first equation. The others
+ %follow by similar arguments. By definition of the abstraction type @{text "abs_set"}
+ %we have
+ %%
+ %\begin{equation}\label{abseqiff}
+ %@{thm (lhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\;
+ %@{thm (rhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]}
+ %\end{equation}
+ %
+ %\noindent
+ %and also
+ %
+ %\begin{equation}\label{absperm}
+ %%@%{%thm %permute_Abs[no_vars]}%
+ %\end{equation}
- \begin{proof}
- This lemma is straightforward using \eqref{abseqiff} and observing that
- the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}.
- Moreover @{text supp} and set difference are equivariant (see \cite{HuffmanUrban10}).
- \end{proof}
-
- \noindent
- Assuming that @{text "x"} has finite support, this lemma together
- with \eqref{absperm} allows us to show
+ %\noindent
+ %The second fact derives from the definition of permutations acting on pairs
+ %\eqref{permute} and $\alpha$-equivalence being equivariant
+ %(see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show
+ %the following lemma about swapping two atoms in an abstraction.
+ %
+ %\begin{lemma}
+ %@{thm[mode=IfThen] Abs_swap1(1)[where bs="as", no_vars]}
+ %\end{lemma}
+ %
+ %\begin{proof}
+ %This lemma is straightforward using \eqref{abseqiff} and observing that
+ %the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}.
+ %Moreover @{text supp} and set difference are equivariant (see \cite{HuffmanUrban10}).
+ %\end{proof}
%
- \begin{equation}\label{halfone}
- @{thm Abs_supports(1)[no_vars]}
- \end{equation}
-
- \noindent
- which by Property~\ref{supportsprop} gives us ``one half'' of
- Theorem~\ref{suppabs}. The ``other half'' is a bit more involved. To establish
- it, we use a trick from \cite{Pitts04} and first define an auxiliary
- function @{text aux}, taking an abstraction as argument:
+ %\noindent
+ %Assuming that @{text "x"} has finite support, this lemma together
+ %with \eqref{absperm} allows us to show
+ %
+ %\begin{equation}\label{halfone}
+ %@{thm Abs_supports(1)[no_vars]}
+ %\end{equation}
+ %
+ %\noindent
+ %which by Property~\ref{supportsprop} gives us ``one half'' of
+ %Theorem~\ref{suppabs}. The ``other half'' is a bit more involved. To establish
+ %it, we use a trick from \cite{Pitts04} and first define an auxiliary
+ %function @{text aux}, taking an abstraction as argument:
+ %@{thm supp_set.simps[THEN eq_reflection, no_vars]}.
%
- \begin{center}
- @{thm supp_set.simps[THEN eq_reflection, no_vars]}
- \end{center}
-
- \noindent
- Using the second equation in \eqref{equivariance}, we can show that
- @{text "aux"} is equivariant (since @{term "p \<bullet> (supp x - as) =
- (supp (p \<bullet> x)) - (p \<bullet> as)"}) and therefore has empty support.
- This in turn means
+ %Using the second equation in \eqref{equivariance}, we can show that
+ %@{text "aux"} is equivariant (since @{term "p \<bullet> (supp x - as) = (supp (p \<bullet> x)) - (p \<bullet> as)"})
+ %and therefore has empty support.
+ %This in turn means
+ %
+ %\begin{center}
+ %@{term "supp (supp_gen (Abs_set as x)) \<subseteq> supp (Abs_set as x)"}
+ %\end{center}
%
- \begin{center}
- @{term "supp (supp_gen (Abs_set as x)) \<subseteq> supp (Abs_set as x)"}
- \end{center}
-
- \noindent
- using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set,
- we further obtain
+ %\noindent
+ %using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set,
+ %we further obtain
%
- \begin{equation}\label{halftwo}
- @{thm (concl) Abs_supp_subset1(1)[no_vars]}
- \end{equation}
-
- \noindent
- since for finite sets of atoms, @{text "bs"}, we have
- @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.
- Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes
- Theorem~\ref{suppabs}.
+ %\begin{equation}\label{halftwo}
+ %@{thm (concl) Abs_supp_subset1(1)[no_vars]}
+ %\end{equation}
+ %
+ %\noindent
+ %since for finite sets of atoms, @{text "bs"}, we have
+ %@{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.
+ %Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes
+ %Theorem~\ref{suppabs}.
The method of first considering abstractions of the
form @{term "Abs_set as x"} etc is motivated by the fact that
@@ -886,7 +887,7 @@
syntax in Nominal Isabelle for such specifications is roughly as follows:
%
\begin{equation}\label{scheme}
- \mbox{\begin{tabular}{@ {\hspace{-5mm}}p{1.8cm}l}
+ \mbox{\begin{tabular}{@ {}p{2.5cm}l}
type \mbox{declaration part} &
$\begin{cases}
\mbox{\begin{tabular}{l}
@@ -987,8 +988,8 @@
\begin{center}
- \begin{tabular}{@ {}cc@ {}}
- \begin{tabular}{@ {}l@ {\hspace{-2mm}}}
+ \begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
+ \begin{tabular}{@ {}l}
\isacommand{nominal\_datatype} @{text lam} $=$\\
\hspace{5mm}\phantom{$\mid$}~@{text "Var name"}\\
\hspace{5mm}$\mid$~@{text "App lam lam"}\\
@@ -1210,7 +1211,7 @@
\end{equation}
\noindent
- by mutual recursion.
+ by recursion.
We define these functions together with auxiliary free-atom functions for
the binding functions. Given raw binding functions @{text "bn"}$_{1..m}$
we define
@@ -1809,74 +1810,74 @@
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{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. 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}
+ %\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{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. 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}
*}