nominal2: comparison LMCS-Paper/Paper.thy

equal deleted inserted replaced

-:5d145fe77ec1
+:8146b0ad8212
 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
 can be appreciated in this case by considering that the definition given by
-Leroy in \cite[Page ???]{Leroy92} is incorrect (it omits a side-condition).
+Leroy in \cite[Page 18--19]{Leroy92} is incorrect (it omits a side-condition).
 However, the notion of alpha-equivalence that is preserved by vacuous
 binders is not always wanted. For example in terms like
 \begin{equation}\label{one}
 task. To ease it, we re-implemented in Isabelle/HOL \cite{KaliszykUrban11}
 the quotient package described by Homeier \cite{Homeier05} for the HOL4
 system. This 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
+as follows
 \[
 \mbox{\begin{tabular}{l@ {\hspace{1mm}}r@ {\hspace{1mm}}l}
 @{text "fv(x)"}     & @{text "\<equiv>"} & @{text "{x}"}\\
 @{text "fv(t\<^isub>1 t\<^isub>2)"} & @{text "\<equiv>"} & @{text "fv(t\<^isub>1) \<union> fv(t\<^isub>2)"}\\
 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.\smallskip
 The examples we have in mind where our reasoning infrastructure will be
-helpful includes the term language of Core-Haskell. This term language
+helpful includes the term language of Core-Haskell (see
-involves patterns that have lists of type-, coercion- and term-variables,
+Figure~\ref{corehas}). This term language involves patterns that have lists
-all of which are bound in @{text "\<CASE>"}-expressions. In these
+of type-, coercion- and term-variables, all of which are bound in @{text
-patterns we do not know in advance how many variables need to
+"\<CASE>"}-expressions. In these patterns we do not know in advance how many
-be bound. Another example is the specification of SML, which includes
+variables need to be bound. Another example is the specification of SML,
-includes bindings as in type-schemes.\medskip
+which includes includes bindings as in type-schemes.\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
 (only one is present in Ott), provide formalised definitions for alpha-equivalence and
 for free variables of our terms, and also derive a reasoning infrastructure
 for our specifications from ``first principles''.
-%\begin{figure}
+\begin{figure}
-%\begin{boxedminipage}{\linewidth}
+\begin{boxedminipage}{\linewidth}
-%%\begin{center}
+\begin{center}
-%\begin{tabular}{r@ {\hspace{1mm}}r@ {\hspace{2mm}}l}
+\begin{tabular}{@ {\hspace{8mm}}r@ {\hspace{2mm}}r@ {\hspace{2mm}}l}
-%\multicolumn{3}{@ {}l}{Type Kinds}\\
+\multicolumn{3}{@ {}l}{Type Kinds}\\
-%@{text "\<kappa>"} & @{text "::="} & @{text "\<star> | \<kappa>\<^isub>1 \<rightarrow> \<kappa>\<^isub>2"}\smallskip\\
+@{text "\<kappa>"} & @{text "::="} & @{text "\<star> | \<kappa>\<^isub>1 \<rightarrow> \<kappa>\<^isub>2"}\smallskip\\
-%\multicolumn{3}{@ {}l}{Coercion Kinds}\\
+\multicolumn{3}{@ {}l}{Coercion Kinds}\\
-%@{text "\<iota>"} & @{text "::="} & @{text "\<sigma>\<^isub>1 \<sim> \<sigma>\<^isub>2"}\smallskip\\
+@{text "\<iota>"} & @{text "::="} & @{text "\<sigma>\<^isub>1 \<sim> \<sigma>\<^isub>2"}\smallskip\\
-%\multicolumn{3}{@ {}l}{Types}\\
+\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 "\<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\\
+@{text "| \<forall>a:\<kappa>. \<sigma> | \<iota> \<Rightarrow> \<sigma>"}\smallskip\\
-%\multicolumn{3}{@ {}l}{Coercion Types}\\
+\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 "\<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 "| \<forall>c:\<iota>. \<gamma> | \<iota> \<Rightarrow> \<gamma> | refl \<sigma> | sym \<gamma> | \<gamma>\<^isub>1 \<circ> \<gamma>\<^isub>2"}\\
-%& @{text "|"} & @{text "refl \<sigma> | sym \<gamma> | \<gamma>\<^isub>1 \<circ> \<gamma>\<^isub>2 | \<gamma> @ \<sigma> | left \<gamma> | right \<gamma>"}\\
+& @{text "|"} & @{text "\<gamma> @ \<sigma> | left \<gamma> | right \<gamma> | \<gamma>\<^isub>1 \<sim> \<gamma>\<^isub>2 | rightc \<gamma> | leftc \<gamma> | \<gamma>\<^isub>1 \<triangleright> \<gamma>\<^isub>2"}\smallskip\\
-%& @{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}\\
-%\multicolumn{3}{@ {}l}{Terms}\\
+@{text "e"} & @{text "::="} & @{text "x | K | \<Lambda>a:\<kappa>. e | \<Lambda>c:\<iota>. e | e \<sigma> | e \<gamma> | \<lambda>x:\<sigma>. e | e\<^isub>1 e\<^isub>2"}\\
-%@{text "e"} & @{text "::="} & @{text "x | K | \<Lambda>a:\<kappa>. e | \<Lambda>c:\<iota>. e | e \<sigma> | e \<gamma>"}\\
+& @{text "|"} & @{text "\<LET> x:\<sigma> = e\<^isub>1 \<IN> e\<^isub>2 | \<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 {*
 \noindent
 Concrete permutations in Nominal Isabelle are built up from swappings,
 written as \mbox{@{text "(a b)"}}, which are permutations that behave
 as follows:
-%
 \begin{center}
 @{text "(a b) = \<lambda>c. if a = c then b else if b = c then a else c"}
 \end{center}
 The most original aspect of the nominal logic work of Pitts is a general
 "x"}''.  This notion, written @{term "supp x"}, is general in the sense that
 it applies not only to lambda-terms (alpha-equated or not), but also to lists,
 products, sets and even functions. The definition depends only on the
 permutation operation and on the notion of equality defined for the type of
 @{text x}, namely:
-%
 \begin{equation}\label{suppdef}
 @{thm supp_def[no_vars, THEN eq_reflection]}
 \end{equation}
 \noindent

changeset 2991	8146b0ad8212
parent 2990	5d145fe77ec1
child 3000	3c8d3aaf292c