nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:f5621efe5a20
+:6d9018d62b40
 text {*
 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
 been used successfully in formalisations of an equivalence checking
 algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed
 \begin{array}{l}
 @{text "T ::= x | T \<rightarrow> T"}\hspace{5mm}
 @{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
 binders by iterating single binders, this leads to a rather clumsy
 formalisation of W. The need of iterating single binders is also one reason
 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.
 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
 want to make a distinction about the order of the bound variables. Therefore
 we would like to regard the following two type-schemes as $\alpha$-equivalent
 %
 \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
 %
 \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
 %
 \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
 that can be used to faithfully represent this kind of binding in Nominal
 Isabelle.  The difficulty of finding the right notion for $\alpha$-equivalence
 \eqref{one} as $\alpha$-equivalent with
 %
 \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
 binders has to agree.
 research. For example in @{text "\<LET>"}s containing patterns like
 %
 \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
 we do not want to regard \eqref{two} as $\alpha$-equivalent with
 %
 \end{center}
 %
 \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
 Cheney \cite{Cheney05}: in @{text "\<LET>"}-constructs of the form
 %
 \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
+we care about the
-about the order in which the @{text "x\<^isub>i = t\<^isub>i"} are given,
+information that there are as many bound variables @{text
-but we do care about the information that there are as many @{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
 \mbox{@{text "\<LET> (\<lambda>x . s)  [t\<^isub>1, t\<^isub>2]"}} is a perfectly legal
 instance, but the lengths of the two lists do not agree. To exclude such
 ensure that the two lists are of equal length. This can result in very messy
 reasoning (see for example~\cite{BengtsonParow09}). To avoid this, we will
 allow type specifications for @{text "\<LET>"}s as follows
 %
 \begin{center}
-\begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l}
+\begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}cl}
-@{text trm} & @{text "::="}  & @{text "\<dots>"}\\
+@{text trm} & @{text "::="}  & @{text "\<dots>"}
-& @{text "|"}    & @{text "\<LET>  as::assn  s::trm"}\hspace{4mm}
+& @{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 assn} & @{text "::="} & @{text "\<ANIL>"}
-& @{text "|"}   & @{text "\<ACONS>  name  trm  assn"}
+&  @{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
+inspired by the syntax of the Ott-tool \cite{ott-jfp}.
-has only one binding mode, namely the one where the order of
-binders matters. Consequently, type-schemes with binding sets
+%Though, Ott
-of names cannot be modelled in 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
 at all in a HOL-based environment where every datatype must have a non-empty
 set-theoretic model \cite{Berghofer99}.
 ``$\alpha$-equals-by-$\alpha$-equals'' in a representation based on raw terms
 requires a lot of extra reasoning work.
 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);
 \draw[very thick] (0.7,0.4) circle (4.25mm);
 \draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);
 \draw (-0.95, 0.3) node[above=0mm] {isomorphism};
 \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
 the type of sets of raw terms according to our $\alpha$-equivalence relation,
 and finally define the new type as these $\alpha$-equivalence classes
 (non-emptiness is satisfied whenever the raw terms are definable as datatype
 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
+%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
+%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
+%$\alpha$-equated terms. That is not the case for example for terms using the
-locally nameless representation of binders \cite{McKinnaPollack99}: in this
+%locally nameless representation of binders \cite{McKinnaPollack99}: in this
-representation there are ``junk'' terms that need to be excluded by
+%representation there are ``junk'' terms that need to be excluded by
-reasoning about a well-formedness predicate.
+%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
 underlying subset to the new type. This is usually a tricky and arduous
 task. To ease it, we re-implemented in Isabelle/HOL the quotient package
 allows us to lift definitions and theorems involving raw terms to
 definitions and theorems involving $\alpha$-equated terms. For example if we
 define the free-variable function over raw lambda-terms
 \begin{center}
-@{text "fv(x) = {x}"}\hspace{10mm}
+@{text "fv(x) = {x}"}\hspace{8mm}
-@{text "fv(t\<^isub>1 t\<^isub>2) = fv(t\<^isub>1) \<union> fv(t\<^isub>2)"}\\[1mm]
+@{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}
 \noindent
 then with the help of the quotient package we can obtain a function @{text "fv\<^sup>\<alpha>"}
 operating on quotients, or $\alpha$-equivalence classes of lambda-terms. This
 lifted function is characterised by the equations
 \begin{center}
-@{text "fv\<^sup>\<alpha>(x) = {x}"}\hspace{10mm}
+@{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)"}\\[1mm]
+@{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}
 \noindent
 (Note that this means also the term-constructors for variables, applications
 properties (see \cite{Homeier05}). In the paper we show that we are able to
 automate these proofs and as a result can automatically establish a reasoning
 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
+helpful includes the term language of Core-Haskell. This term language
-known as Core-Haskell (see Figure~\ref{corehas}). This term language
 involves patterns that have lists of type-, coercion- and term-variables,
-all of which are bound in @{text "\<CASE>"}-expressions. One
+all of which are bound in @{text "\<CASE>"}-expressions. In these
-feature is that we do not know in advance how many variables need to
+patterns 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
+be bound. Another example is the specification of SML, which includes
-annotation. Representing such binders with single binders and reasoning
+includes bindings as in type-schemes.\medskip
-about them in a theorem prover would be a major pain.  \medskip
 \noindent
 {\bf Contributions:}  We provide three new definitions for when terms
 involving general binders are $\alpha$-equivalent. These definitions are
 inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic
 terms, including properties about support, freshness and equality
 conditions for $\alpha$-equated terms. We are also able to derive strong
 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,
+that our specifications make sense for reasoning about $\alpha$-equated terms.
-provide precise definitions for $\alpha$-equivalence and for free
+The main improvement over Ott is that we introduce three binding modes
-variables of our terms, and provide automated proofs inside the
+(only one is present in Ott), provide definitions for $\alpha$-equivalence and
-Isabelle theorem prover.
+for free variables of our terms, and also derive a reasoning infrastructure
+about our specifications inside Isabelle/HOL.
-\begin{figure}
-\begin{boxedminipage}{\linewidth}
+%\begin{figure}
-\begin{center}
+%\begin{boxedminipage}{\linewidth}
-\begin{tabular}{r@ {\hspace{1mm}}r@ {\hspace{2mm}}l}
+%%\begin{center}
-\multicolumn{3}{@ {}l}{Type Kinds}\\
+%\begin{tabular}{r@ {\hspace{1mm}}r@ {\hspace{2mm}}l}
-@{text "\<kappa>"} & @{text "::="} & @{text "\<star> | \<kappa>\<^isub>1 \<rightarrow> \<kappa>\<^isub>2"}\smallskip\\
+%\multicolumn{3}{@ {}l}{Type Kinds}\\
-\multicolumn{3}{@ {}l}{Coercion Kinds}\\
+%@{text "\<kappa>"} & @{text "::="} & @{text "\<star> | \<kappa>\<^isub>1 \<rightarrow> \<kappa>\<^isub>2"}\smallskip\\
-@{text "\<iota>"} & @{text "::="} & @{text "\<sigma>\<^isub>1 \<sim> \<sigma>\<^isub>2"}\smallskip\\
+%\multicolumn{3}{@ {}l}{Coercion Kinds}\\
-\multicolumn{3}{@ {}l}{Types}\\
+%@{text "\<iota>"} & @{text "::="} & @{text "\<sigma>\<^isub>1 \<sim> \<sigma>\<^isub>2"}\smallskip\\
-@{text "\<sigma>"} & @{text "::="} & @{text "a | T | \<sigma>\<^isub>1 \<sigma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<sigma>"}}$@{text "\<^sup>n"}
+%\multicolumn{3}{@ {}l}{Types}\\
-@{text "| \<forall>a:\<kappa>. \<sigma> | \<iota> \<Rightarrow> \<sigma>"}\smallskip\\
+%@{text "\<sigma>"} & @{text "::="} & @{text "a | T | \<sigma>\<^isub>1 \<sigma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<sigma>"}}$@{text "\<^sup>n"}
-\multicolumn{3}{@ {}l}{Coercion Types}\\
+%@{text "| \<forall>a:\<kappa>. \<sigma> | \<iota> \<Rightarrow> \<sigma>"}\smallskip\\
-@{text "\<gamma>"} & @{text "::="} & @{text "c | C | \<gamma>\<^isub>1 \<gamma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<gamma>"}}$@{text "\<^sup>n"}
+%\multicolumn{3}{@ {}l}{Coercion Types}\\
-@{text "| \<forall>c:\<iota>. \<gamma> | \<iota> \<Rightarrow> \<gamma> "}\\
+%@{text "\<gamma>"} & @{text "::="} & @{text "c | C | \<gamma>\<^isub>1 \<gamma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<gamma>"}}$@{text "\<^sup>n"}
-& @{text "|"} & @{text "refl \<sigma> | sym \<gamma> | \<gamma>\<^isub>1 \<circ> \<gamma>\<^isub>2 | \<gamma> @ \<sigma> | left \<gamma> | right \<gamma>"}\\
+%@{text "| \<forall>c:\<iota>. \<gamma> | \<iota> \<Rightarrow> \<gamma> "}\\
-& @{text "|"} & @{text "\<gamma>\<^isub>1 \<sim> \<gamma>\<^isub>2 | rightc \<gamma> | leftc \<gamma> | \<gamma>\<^isub>1 \<triangleright> \<gamma>\<^isub>2"}\smallskip\\
+%& @{text "|"} & @{text "refl \<sigma> | sym \<gamma> | \<gamma>\<^isub>1 \<circ> \<gamma>\<^isub>2 | \<gamma> @ \<sigma> | left \<gamma> | right \<gamma>"}\\
-\multicolumn{3}{@ {}l}{Terms}\\
+%& @{text "|"} & @{text "\<gamma>\<^isub>1 \<sim> \<gamma>\<^isub>2 | rightc \<gamma> | leftc \<gamma> | \<gamma>\<^isub>1 \<triangleright> \<gamma>\<^isub>2"}\smallskip\\
-@{text "e"} & @{text "::="} & @{text "x | K | \<Lambda>a:\<kappa>. e | \<Lambda>c:\<iota>. e | e \<sigma> | e \<gamma>"}\\
+%\multicolumn{3}{@ {}l}{Terms}\\
-& @{text "|"} & @{text "\<lambda>x:\<sigma>. e | e\<^isub>1 e\<^isub>2 | \<LET> x:\<sigma> = e\<^isub>1 \<IN> e\<^isub>2"}\\
+%@{text "e"} & @{text "::="} & @{text "x | K | \<Lambda>a:\<kappa>. e | \<Lambda>c:\<iota>. e | e \<sigma> | e \<gamma>"}\\
-& @{text "|"} & @{text "\<CASE> e\<^isub>1 \<OF>"}$\;\overline{@{text "p \<rightarrow> e\<^isub>2"}}$ @{text "| e \<triangleright> \<gamma>"}\smallskip\\
+%& @{text "|"} & @{text "\<lambda>x:\<sigma>. e | e\<^isub>1 e\<^isub>2 | \<LET> x:\<sigma> = e\<^isub>1 \<IN> e\<^isub>2"}\\
-\multicolumn{3}{@ {}l}{Patterns}\\
+%& @{text "|"} & @{text "\<CASE> e\<^isub>1 \<OF>"}$\;\overline{@{text "p \<rightarrow> e\<^isub>2"}}$ @{text "| e \<triangleright> \<gamma>"}\smallskip\\
-@{text "p"} & @{text "::="} & @{text "K"}$\;\overline{@{text "a:\<kappa>"}}\;\overline{@{text "c:\<iota>"}}\;\overline{@{text "x:\<sigma>"}}$\smallskip\\
+%\multicolumn{3}{@ {}l}{Patterns}\\
-\multicolumn{3}{@ {}l}{Constants}\\
+%@{text "p"} & @{text "::="} & @{text "K"}$\;\overline{@{text "a:\<kappa>"}}\;\overline{@{text "c:\<iota>"}}\;\overline{@{text "x:\<sigma>"}}$\smallskip\\
-& @{text C} & coercion constants\\
+%\multicolumn{3}{@ {}l}{Constants}\\
-& @{text T} & value type constructors\\
+%& @{text C} & coercion constants\\
-& @{text "S\<^isub>n"} & n-ary type functions (which need to be fully applied)\\
+%& @{text T} & value type constructors\\
-& @{text K} & data constructors\smallskip\\
+%& @{text "S\<^isub>n"} & n-ary type functions (which need to be fully applied)\\
-\multicolumn{3}{@ {}l}{Variables}\\
+%& @{text K} & data constructors\smallskip\\
-& @{text a} & type variables\\
+%\multicolumn{3}{@ {}l}{Variables}\\
-& @{text c} & coercion variables\\
+%& @{text a} & type variables\\
-& @{text x} & term variables\\
+%& @{text c} & coercion variables\\
-\end{tabular}
+%& @{text x} & term variables\\
-\end{center}
+%\end{tabular}
-\end{boxedminipage}
+%\end{center}
-\caption{The System @{text "F\<^isub>C"}
+%\end{boxedminipage}
-\cite{CoreHaskell}, also often referred to as \emph{Core-Haskell}. In this
+%\caption{The System @{text "F\<^isub>C"}
-version of @{text "F\<^isub>C"} we made a modification by separating the
+%\cite{CoreHaskell}, also often referred to as \emph{Core-Haskell}. In this
-grammars for type kinds and coercion kinds, as well as for types and coercion
+%version of @{text "F\<^isub>C"} we made a modification by separating the
-types. For this paper the interesting term-constructor is @{text "\<CASE>"},
+%grammars for type kinds and coercion kinds, as well as for types and coercion
-which binds multiple type-, coercion- and term-variables.\label{corehas}}
+%types. For this paper the interesting term-constructor is @{text "\<CASE>"},
-\end{figure}
+%which binds multiple type-, coercion- and term-variables.\label{corehas}}
+%\end{figure}
 *}
 section {* A Short Review of the Nominal Logic Work *}
 text {*
 in what follows to only one sort of atoms.
 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"},
 the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}},
 and the inverse permutation of @{term p} as @{text "- p"}. The permutation
 operation is defined by induction over the type-hierarchy \cite{HuffmanUrban10};
 for example permutations acting on products, lists, sets, functions and booleans is
 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]}\\
 @{thm permute_list.simps(2)[no_vars, THEN eq_reflection]}\\
 \end{tabular} &
 \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}
 \noindent
 @{thm supp_def[no_vars, THEN eq_reflection]}
 \end{equation}
 \noindent
 There is also the derived notion for when an atom @{text a} is \emph{fresh}
-for an @{text x}, defined as
+for an @{text x}, defined as @{thm fresh_def[no_vars]}.
-%
-\begin{center}
-@{thm fresh_def[no_vars]}
-\end{center}
-\noindent
 We use for sets of atoms the abbreviation
 @{thm (lhs) fresh_star_def[no_vars]}, defined as
 @{thm (rhs) fresh_star_def[no_vars]}.
 A striking consequence of these definitions is that we can prove
 without knowing anything about the structure of @{term x} that
 While often the support of an object can be relatively easily
 described, for example for atoms, products, lists, function applications,
 booleans and permutations as follows
 %
-\begin{eqnarray}
+\begin{center}
-@{term "supp a"} & = & @{term "{a}"}\\
+\begin{tabular}{c@ {\hspace{10mm}}c}
-@{term "supp (x, y)"} & = & @{term "supp x \<union> supp y"}\\
+\begin{tabular}{rcl}
-@{term "supp []"} & = & @{term "{}"}\\
+@{term "supp a"} & $=$ & @{term "{a}"}\\
-@{term "supp (x#xs)"} & = & @{term "supp x \<union> supp xs"}\\
+@{term "supp (x, y)"} & $=$ & @{term "supp x \<union> supp y"}\\
-@{text "supp (f x)"} & @{text "\<subseteq>"} & @{term "supp f \<union> supp x"}\label{suppfun}\\
+@{term "supp []"} & $=$ & @{term "{}"}\\
-@{term "supp b"} & = & @{term "{}"}\\
+@{term "supp (x#xs)"} & $=$ & @{term "supp x \<union> supp xs"}\\
-@{term "supp p"} & = & @{term "{a. p \<bullet> a \<noteq> a}"}
+\end{tabular}
-\end{eqnarray}
+&
+\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
+only an approximation can be established (as for functions above).
-such approximations can be simplified with the notion \emph{supports}, defined
-as follows:
+%Reasoning about
+%such approximations can be simplified with the notion \emph{supports}, defined
-\begin{definition}
+%as follows:
-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"}.
+%\begin{definition}
-\end{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"}.
-\noindent
+%\end{definition}
-The main point of @{text supports} is that we can establish the following
+%
-two properties.
+%\noindent
+%The main point of @{text supports} is that we can establish the following
-\begin{property}\label{supportsprop}
+%two properties.
-Given a set @{text "as"} of atoms.
+%
-{\it (i)} @{thm[mode=IfThen] supp_is_subset[where S="as", no_vars]}
+%\begin{property}\label{supportsprop}
-{\it (ii)} @{thm supp_supports[no_vars]}.
+%Given a set @{text "as"} of atoms.
-\end{property}
+%{\it (i)} @{thm[mode=IfThen] supp_is_subset[where S="as", no_vars]}
+%{\it (ii)} @{thm supp_supports[no_vars]}.
-Another important notion in the nominal logic work is \emph{equivariance}.
+%\end{property}
-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
+%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
-\begin{equation}\label{equivariancedef}
+%it is required that every permutation leaves @{text f} unchanged, that is
-@{term "\<forall>p. p \<bullet> f = f"}
+%%
-\end{equation}
+%\begin{equation}\label{equivariancedef}
+%@{term "\<forall>p. p \<bullet> f = f"}
-\noindent or equivalently that a permutation applied to the application
+%\end{equation}
-@{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}:
+%\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
-\begin{equation}\label{equivariance}
+%functions @{text f}, we have for all permutations @{text p}:
-@{text "p \<bullet> f = f"} \;\;\;\textit{if and only if}\;\;\;
+%%
-@{text "p \<bullet> (f x) = f (p \<bullet> x)"}
+%\begin{equation}\label{equivariance}
-\end{equation}
+%@{text "p \<bullet> f = f"} \;\;\;\textit{if and only if}\;\;\;
+%@{text "p \<bullet> (f x) = f (p \<bullet> x)"}
-\noindent
+%\end{equation}
-From property \eqref{equivariancedef} and the definition of @{text supp}, we
+%
-can easily deduce that equivariant functions have empty support. There is
+%\noindent
-also a similar notion for equivariant relations, say @{text R}, namely the property
+%From property \eqref{equivariancedef} and the definition of @{text supp}, we
-that
+%can easily deduce that equivariant functions have empty support. There is
-%
+%also a similar notion for equivariant relations, say @{text R}, namely the property
-\begin{center}
+%that
-@{text "x R y"} \;\;\textit{implies}\;\; @{text "(p \<bullet> x) R (p \<bullet> y)"}
+%%
-\end{center}
+%\begin{center}
+%@{text "x R y"} \;\;\textit{implies}\;\; @{text "(p \<bullet> x) R (p \<bullet> y)"}
-Finally, the nominal logic work provides us with general means for renaming
+%\end{center}
+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
 following generalisations turned out to be easier to use.
 atoms; moreover there must be a permutation @{text p} such that {\it
 (ii)} @{text p} leaves the free atoms of @{text x} and @{text y} unchanged, but
 {\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}
+\begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l}
-\multicolumn{3}{l}{@{term "(as, x) \<approx>set R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+\multicolumn{4}{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)}\\
+\mbox{\it (i)}   & @{term "fa(x) - as = fa(y) - bs"} &
-@{text "\<and>"} & @{term "(fa(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
+\mbox{\it (iii)} &  @{text "(p \<bullet> x) R y"} \\
-@{text "\<and>"} & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
+\mbox{\it (ii)}  & @{term "(fa(x) - as) \<sharp>* p"} &
-@{text "\<and>"} & @{term "(p \<bullet> as) = bs"} & \mbox{\it (iv)}\\
+\mbox{\it (iv)}  & @{term "(p \<bullet> as) = bs"} \\
 \end{array}
 \end{equation}
 \noindent
 Note that this relation depends on the permutation @{text
 order of abstracted atoms. If we want this, then we can define $\alpha$-equivalence
 for pairs of the form \mbox{@{text "(as, x)"}} with type @{text "(atom list) \<times> \<beta>"}
 as follows
 %
 \begin{equation}\label{alphalist}
-\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>lst R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+\multicolumn{4}{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)}\\
+\mbox{\it (i)}   & @{term "fa(x) - (set as) = fa(y) - (set bs)"} &
-\wedge     & @{term "(fa(x) - set as) \<sharp>* p"} & \mbox{\it (ii)}\\
+\mbox{\it (iii)} & @{text "(p \<bullet> x) R y"}\\
-\wedge     & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
+\mbox{\it (ii)}  & @{term "(fa(x) - set as) \<sharp>* p"} &
-\wedge     & @{term "(p \<bullet> as) = bs"} & \mbox{\it (iv)}\\
+\mbox{\it (iv)}  & @{term "(p \<bullet> as) = bs"}\\
 \end{array}
 \end{equation}
 \noindent
 where @{term set} is the function that coerces a list of atoms into a set of atoms.
 If we do not want to make any difference between the order of binders \emph{and}
 also allow vacuous binders, then we keep sets of binders, but drop the fourth
 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)}\\
+\mbox{\it (i)}   & @{term "fa(x) - as = fa(y) - bs"} &
-\wedge     & @{term "(fa(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
+\mbox{\it (iii)} & @{text "(p \<bullet> x) R y"}\\
-\wedge     & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
+\mbox{\it (ii)}  & @{term "(fa(x) - as) \<sharp>* p"}\\
 \end{array}
 \end{equation}
 It might be useful to consider first some examples about how these definitions
 of $\alpha$-equivalence pan out in practice.  For this consider the case of
 call the types \emph{abstraction types} and their elements
 \emph{abstractions}. The important property we need to derive is the support of
 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}
+\begin{center}
-@{thm (lhs) supp_Abs(1)[no_vars]} & $=$ & @{thm (rhs) supp_Abs(1)[no_vars]}\\
+\begin{tabular}{l}
-@{thm (lhs) supp_Abs(2)[no_vars]} & $=$ & @{thm (rhs) supp_Abs(2)[no_vars]}\\
+@{thm (lhs) supp_Abs(1)[no_vars]} $=$
-@{thm (lhs) supp_Abs(3)[where bs="as", no_vars]} & $=$ & @{thm (rhs) supp_Abs(3)[where bs="as", 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
+This theorem states that the bound names do not appear in the support, as expected.
-follow by similar arguments. By definition of the abstraction type @{text "abs_set"}
+For brevity we omit the proof of this resul and again refer the reader to
-we have
+our formalisation in Isabelle/HOL.
-%
-\begin{equation}\label{abseqiff}
+%\noindent
-@{thm (lhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\;
+%Below we will show the first equation. The others
-@{thm (rhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]}
+%follow by similar arguments. By definition of the abstraction type @{text "abs_set"}
-\end{equation}
+%we have
+%%
-\noindent
+%\begin{equation}\label{abseqiff}
-and also
+%@{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]}
-\begin{equation}\label{absperm}
+%\end{equation}
-@{thm permute_Abs[no_vars]}
+%
-\end{equation}
+%\noindent
+%and also
-\noindent
+%
-The second fact derives from the definition of permutations acting on pairs
+%\begin{equation}\label{absperm}
-\eqref{permute} and $\alpha$-equivalence being equivariant
+%%@%{%thm %permute_Abs[no_vars]}%
-(see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show
+%\end{equation}
-the following lemma about swapping two atoms in an abstraction.
+%\noindent
-\begin{lemma}
+%The second fact derives from the definition of permutations acting on pairs
-@{thm[mode=IfThen] Abs_swap1(1)[where bs="as", no_vars]}
+%\eqref{permute} and $\alpha$-equivalence being equivariant
-\end{lemma}
+%(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{proof}
+%
-This lemma is straightforward using \eqref{abseqiff} and observing that
+%\begin{lemma}
-the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}.
+%@{thm[mode=IfThen] Abs_swap1(1)[where bs="as", no_vars]}
-Moreover @{text supp} and set difference are equivariant (see \cite{HuffmanUrban10}).
+%\end{lemma}
-\end{proof}
+%
+%\begin{proof}
-\noindent
+%This lemma is straightforward using \eqref{abseqiff} and observing that
-Assuming that @{text "x"} has finite support, this lemma together
+%the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}.
-with \eqref{absperm} allows us to show
+%Moreover @{text supp} and set difference are equivariant (see \cite{HuffmanUrban10}).
-%
+%\end{proof}
-\begin{equation}\label{halfone}
+%
-@{thm Abs_supports(1)[no_vars]}
+%\noindent
-\end{equation}
+%Assuming that @{text "x"} has finite support, this lemma together
+%with \eqref{absperm} allows us to show
-\noindent
+%
-which by Property~\ref{supportsprop} gives us ``one half'' of
+%\begin{equation}\label{halfone}
-Theorem~\ref{suppabs}. The ``other half'' is a bit more involved. To establish
+%@{thm Abs_supports(1)[no_vars]}
-it, we use a trick from \cite{Pitts04} and first define an auxiliary
+%\end{equation}
-function @{text aux}, taking an abstraction as argument:
+%
-%
+%\noindent
-\begin{center}
+%which by Property~\ref{supportsprop} gives us ``one half'' of
-@{thm supp_set.simps[THEN eq_reflection, no_vars]}
+%Theorem~\ref{suppabs}. The ``other half'' is a bit more involved. To establish
-\end{center}
+%it, we use a trick from \cite{Pitts04} and first define an auxiliary
+%function @{text aux}, taking an abstraction as argument:
-\noindent
+%@{thm supp_set.simps[THEN eq_reflection, no_vars]}.
-Using the second equation in \eqref{equivariance}, we can show that
+%
-@{text "aux"} is equivariant (since @{term "p \<bullet> (supp x - as) =
+%Using the second equation in \eqref{equivariance}, we can show that
-(supp (p \<bullet> x)) - (p \<bullet> as)"}) and therefore has empty support.
+%@{text "aux"} is equivariant (since @{term "p \<bullet> (supp x - as) = (supp (p \<bullet> x)) - (p \<bullet> as)"})
-This in turn means
+%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)"}
+%\begin{center}
-\end{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,
+%\noindent
-we further obtain
+%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]}
+%\begin{equation}\label{halftwo}
-\end{equation}
+%@{thm (concl) Abs_supp_subset1(1)[no_vars]}
+%\end{equation}
-\noindent
+%
-since for finite sets of atoms, @{text "bs"}, we have
+%\noindent
-@{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.
+%since for finite sets of atoms, @{text "bs"}, we have
-Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes
+%@{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.
-Theorem~\ref{suppabs}.
+%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
 we can conveniently establish  at the Isabelle/HOL level
 properties about them.  It would be
 "ty\<AL>\<^isub>1, \<dots>, ty\<AL>\<^isub>n"}, and an associated collection of
 binding functions, say @{text "bn\<AL>\<^isub>1, \<dots>, bn\<AL>\<^isub>m"}. The
 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}
 \isacommand{nominal\_datatype} @{text "ty\<AL>\<^isub>1 = \<dots>"}\\
 \isacommand{and} @{text "ty\<AL>\<^isub>2 = \<dots>"}\\
 single name is bound, and type-schemes, where a finite set of names is
 bound:
 \begin{center}
-\begin{tabular}{@ {}cc@ {}}
+\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
-\begin{tabular}{@ {}l@ {\hspace{-2mm}}}
+\begin{tabular}{@ {}l}
 \isacommand{nominal\_datatype} @{text lam} $=$\\
 \hspace{5mm}\phantom{$\mid$}~@{text "Var name"}\\
 \hspace{5mm}$\mid$~@{text "App lam lam"}\\
 \hspace{5mm}$\mid$~@{text "Lam x::name t::lam"}\\
 \hspace{21mm}\isacommand{bind} @{text x} \isacommand{in} @{text t}\\
 \begin{equation}\label{fvars}
 @{text "fa_ty\<^isub>1, \<dots>, fa_ty\<^isub>n"}
 \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
 %
 \begin{center}
 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{figure}[t!]
-\begin{boxedminipage}{\linewidth}
+%\begin{boxedminipage}{\linewidth}
-\small
+%\small
-\begin{tabular}{l}
+%\begin{tabular}{l}
-\isacommand{atom\_decl}~@{text "var cvar tvar"}\\[1mm]
+%\isacommand{atom\_decl}~@{text "var cvar tvar"}\\[1mm]
-\isacommand{nominal\_datatype}~@{text "tkind ="}\\
+%\isacommand{nominal\_datatype}~@{text "tkind ="}\\
-\phantom{$|$}~@{text "KStar"}~$|$~@{text "KFun tkind tkind"}\\
+%\phantom{$|$}~@{text "KStar"}~$|$~@{text "KFun tkind tkind"}\\
-\isacommand{and}~@{text "ckind ="}\\
+%\isacommand{and}~@{text "ckind ="}\\
-\phantom{$|$}~@{text "CKSim ty ty"}\\
+%\phantom{$|$}~@{text "CKSim ty ty"}\\
-\isacommand{and}~@{text "ty ="}\\
+%\isacommand{and}~@{text "ty ="}\\
-\phantom{$|$}~@{text "TVar tvar"}~$|$~@{text "T string"}~$|$~@{text "TApp ty ty"}\\
+%\phantom{$|$}~@{text "TVar tvar"}~$|$~@{text "T string"}~$|$~@{text "TApp ty ty"}\\
-$|$~@{text "TFun string ty_list"}~%
+%$|$~@{text "TFun string ty_list"}~%
-$|$~@{text "TAll tv::tvar tkind ty::ty"}  \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text ty}\\
+%$|$~@{text "TAll tv::tvar tkind ty::ty"}  \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text ty}\\
-$|$~@{text "TArr ckind ty"}\\
+%$|$~@{text "TArr ckind ty"}\\
-\isacommand{and}~@{text "ty_lst ="}\\
+%\isacommand{and}~@{text "ty_lst ="}\\
-\phantom{$|$}~@{text "TNil"}~$|$~@{text "TCons ty ty_lst"}\\
+%\phantom{$|$}~@{text "TNil"}~$|$~@{text "TCons ty ty_lst"}\\
-\isacommand{and}~@{text "cty ="}\\
+%\isacommand{and}~@{text "cty ="}\\
-\phantom{$|$}~@{text "CVar cvar"}~%
+%\phantom{$|$}~@{text "CVar cvar"}~%
-$|$~@{text "C string"}~$|$~@{text "CApp cty cty"}~$|$~@{text "CFun string co_lst"}\\
+%$|$~@{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 "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 "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 "CAt cty ty"}~$|$~@{text "CLeft cty"}~$|$~@{text "CRight cty"}~$|$~@{text "CSim cty cty"}\\
-$|$~@{text "CRightc cty"}~$|$~@{text "CLeftc cty"}~$|$~@{text "Coerce cty cty"}\\
+%$|$~@{text "CRightc cty"}~$|$~@{text "CLeftc cty"}~$|$~@{text "Coerce cty cty"}\\
-\isacommand{and}~@{text "co_lst ="}\\
+%\isacommand{and}~@{text "co_lst ="}\\
-\phantom{$|$}@{text "CNil"}~$|$~@{text "CCons cty co_lst"}\\
+%\phantom{$|$}@{text "CNil"}~$|$~@{text "CCons cty co_lst"}\\
-\isacommand{and}~@{text "trm ="}\\
+%\isacommand{and}~@{text "trm ="}\\
-\phantom{$|$}~@{text "Var var"}~$|$~@{text "K string"}\\
+%\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_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 "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 "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 "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 "Let x::var ty trm t::trm"}  \isacommand{bind}~@{text x}~\isacommand{in}~@{text t}\\
-$|$~@{text "Case trm assoc_lst"}~$|$~@{text "Cast trm co"}\\
+%$|$~@{text "Case trm assoc_lst"}~$|$~@{text "Cast trm co"}\\
-\isacommand{and}~@{text "assoc_lst ="}\\
+%\isacommand{and}~@{text "assoc_lst ="}\\
-\phantom{$|$}~@{text ANil}~%
+%\phantom{$|$}~@{text ANil}~%
-$|$~@{text "ACons p::pat t::trm assoc_lst"}  \isacommand{bind}~@{text "bv p"}~\isacommand{in}~@{text t}\\
+%$|$~@{text "ACons p::pat t::trm assoc_lst"}  \isacommand{bind}~@{text "bv p"}~\isacommand{in}~@{text t}\\
-\isacommand{and}~@{text "pat ="}\\
+%\isacommand{and}~@{text "pat ="}\\
-\phantom{$|$}~@{text "Kpat string tvtk_lst tvck_lst vt_lst"}\\
+%\phantom{$|$}~@{text "Kpat string tvtk_lst tvck_lst vt_lst"}\\
-\isacommand{and}~@{text "vt_lst ="}\\
+%\isacommand{and}~@{text "vt_lst ="}\\
-\phantom{$|$}~@{text VTNil}~$|$~@{text "VTCons var ty vt_lst"}\\
+%\phantom{$|$}~@{text VTNil}~$|$~@{text "VTCons var ty vt_lst"}\\
-\isacommand{and}~@{text "tvtk_lst ="}\\
+%\isacommand{and}~@{text "tvtk_lst ="}\\
-\phantom{$|$}~@{text TVTKNil}~$|$~@{text "TVTKCons tvar tkind tvtk_lst"}\\
+%\phantom{$|$}~@{text TVTKNil}~$|$~@{text "TVTKCons tvar tkind tvtk_lst"}\\
-\isacommand{and}~@{text "tvck_lst ="}\\
+%\isacommand{and}~@{text "tvck_lst ="}\\
-\phantom{$|$}~@{text TVCKNil}~$|$ @{text "TVCKCons cvar ckind tvck_lst"}\\
+%\phantom{$|$}~@{text TVCKNil}~$|$ @{text "TVCKCons cvar ckind tvck_lst"}\\
-\isacommand{binder}\\
+%\isacommand{binder}\\
-@{text "bv :: pat \<Rightarrow> atom list"}~\isacommand{and}~%
+%@{text "bv :: pat \<Rightarrow> atom list"}~\isacommand{and}~%
-@{text "bv1 :: vt_lst \<Rightarrow> atom list"}~\isacommand{and}\\
+%@{text "bv1 :: vt_lst \<Rightarrow> atom list"}~\isacommand{and}\\
-@{text "bv2 :: tvtk_lst \<Rightarrow> atom list"}~\isacommand{and}~%
+%@{text "bv2 :: tvtk_lst \<Rightarrow> atom list"}~\isacommand{and}~%
-@{text "bv3 :: tvck_lst \<Rightarrow> atom list"}\\
+%@{text "bv3 :: tvck_lst \<Rightarrow> atom list"}\\
-\isacommand{where}\\
+%\isacommand{where}\\
-\phantom{$|$}~@{text "bv (K s tvts tvcs vs) = (bv3 tvts) @ (bv2 tvcs) @ (bv1 vs)"}\\
+%\phantom{$|$}~@{text "bv (K s tvts tvcs vs) = (bv3 tvts) @ (bv2 tvcs) @ (bv1 vs)"}\\
-$|$~@{text "bv1 VTNil = []"}\\
+%$|$~@{text "bv1 VTNil = []"}\\
-$|$~@{text "bv1 (VTCons x ty tl) = (atom x)::(bv1 tl)"}\\
+%$|$~@{text "bv1 (VTCons x ty tl) = (atom x)::(bv1 tl)"}\\
-$|$~@{text "bv2 TVTKNil = []"}\\
+%$|$~@{text "bv2 TVTKNil = []"}\\
-$|$~@{text "bv2 (TVTKCons a ty tl) = (atom a)::(bv2 tl)"}\\
+%$|$~@{text "bv2 (TVTKCons a ty tl) = (atom a)::(bv2 tl)"}\\
-$|$~@{text "bv3 TVCKNil = []"}\\
+%$|$~@{text "bv3 TVCKNil = []"}\\
-$|$~@{text "bv3 (TVCKCons c cty tl) = (atom c)::(bv3 tl)"}\\
+%$|$~@{text "bv3 (TVCKCons c cty tl) = (atom c)::(bv3 tl)"}\\
-\end{tabular}
+%\end{tabular}
-\end{boxedminipage}
+%\end{boxedminipage}
-\caption{The nominal datatype declaration for Core-Haskell. For the moment we
+%\caption{The nominal datatype declaration for Core-Haskell. For the moment we
-do not support nested types; therefore we explicitly have to unfold the
+%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
+%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
+%in a future version of Nominal Isabelle. Apart from that, the
-declaration follows closely the original in Figure~\ref{corehas}. 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,
+%point of our work is that having made such a declaration in Nominal Isabelle,
-one obtains automatically a reasoning infrastructure for Core-Haskell.
+%one obtains automatically a reasoning infrastructure for Core-Haskell.
-\label{nominalcorehas}}
+%\label{nominalcorehas}}
-\end{figure}
+%\end{figure}
 *}
 section {* Strong Induction Principles *}

changeset 2508	6d9018d62b40
parent 2507	f5621efe5a20
child 2509	679cef364022