--- a/LMCS-Paper/Paper.thy Wed Aug 17 09:43:37 2011 +0200
+++ b/LMCS-Paper/Paper.thy Wed Aug 17 21:08:48 2011 +0200
@@ -124,7 +124,7 @@
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
@@ -319,6 +319,7 @@
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}
@@ -356,12 +357,12 @@
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
- involves patterns that have lists of type-, coercion- and term-variables,
- 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
+ helpful includes the term language of 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. 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
@@ -380,47 +381,45 @@
for our specifications from ``first principles''.
- %\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}{@ {\hspace{8mm}}r@ {\hspace{2mm}}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> | refl \<sigma> | sym \<gamma> | \<gamma>\<^isub>1 \<circ> \<gamma>\<^isub>2"}\\
+ & @{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\\
+ \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 "|"} & @{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\\
+ \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 *}
@@ -490,7 +489,7 @@
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}
@@ -502,7 +501,7 @@
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}