--- a/Paper/Paper.thy Mon Mar 29 16:44:05 2010 +0200
+++ b/Paper/Paper.thy Mon Mar 29 16:44:26 2010 +0200
@@ -13,7 +13,7 @@
notation (latex output)
swap ("'(_ _')" [1000, 1000] 1000) and
fresh ("_ # _" [51, 51] 50) and
- fresh_star ("_ #* _" [51, 51] 50) and
+ fresh_star ("_ #\<^sup>* _" [51, 51] 50) and
supp ("supp _" [78] 73) and
uminus ("-_" [78] 73) and
If ("if _ then _ else _" 10) and
@@ -47,7 +47,7 @@
successfully in formalisations of an equivalence checking algorithm for LF
\cite{UrbanCheneyBerghofer08}, Typed
Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency
- \cite{BengtsonParrow07,BengtsonParow09} and a strong normalisation result
+ \cite{BengtsonParow09} and a strong normalisation result
for cut-elimination in classical logic \cite{UrbanZhu08}. It has also been
used by Pollack for formalisations in the locally-nameless approach to
binding \cite{SatoPollack10}.
@@ -328,27 +328,24 @@
\noindent
(Note that this means also the term-constructors for variables, applications
and lambda are lifted to the quotient level.) This construction, of course,
- only works if alpha-equivalence is indeed an equivalence relation, and the lifted
- definitions and theorems are respectful w.r.t.~alpha-equivalence. For example, we
- will not be able to lift a bound-variable function, which can be defined for
- raw terms. The reason is that this function does not respect alpha-equivalence.
- To sum up, every lifting of
- theorems to the quotient level needs proofs of some respectfulness
- properties (see \cite{Homeier05}). In the paper we show that we are able to
- automate these
- proofs and therefore can establish a reasoning infrastructure for
- alpha-equated terms.
+ only works if alpha-equivalence is indeed an equivalence relation, and the
+ lifted definitions and theorems are respectful w.r.t.~alpha-equivalence.
+ For example, we will not be able to lift a bound-variable function. Although
+ this function can be defined for raw terms, it does not respect
+ alpha-equivalence and therefore cannot be lifted. To sum up, every lifting
+ of theorems to the quotient level needs proofs of some respectfulness
+ properties (see \cite{Homeier05}). In the paper we show that we are able to
+ automate these proofs and therefore can 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 known as
- Core-Haskell (see Figure~\ref{corehas}). This term language involves patterns
- that include lists of
- type- and term- variables (the arguments of constructors) all of which are
- bound in case expressions. One difficulty is that each of these variables
- come 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
-
+ helpful includes the term language of System @{text "F\<^isub>C"}, also
+ known as Core-Haskell (see Figure~\ref{corehas}). This term language
+ involves patterns that have lists of type- and term-variables (the
+ arguments of constructors) all of which are bound in case expressions. One
+ difficulty is that each of these variables come 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
\noindent
{\bf Contributions:} We provide new definitions for when terms
@@ -369,35 +366,35 @@
\multicolumn{3}{@ {}l}{Coercion Kinds}\\
@{text "\<iota>"} & @{text "::="} & @{text "\<sigma>\<^isub>1 \<sim> \<sigma>\<^isub>2"}\medskip\\
\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> "}\\
- & & ??? Type equality\medskip\\
+ @{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>"}\medskip\\
\multicolumn{3}{@ {}l}{Coercion Types}\\
- @{text "\<gamma>"} & @{text "::="} & @{text "a | C | S\<^isub>n"}$\;\overline{@{text "\<gamma>"}}$@{text "\<^sup>n"}\\
- & & @{text "| \<forall>a:\<iota>. \<gamma>"}\\
- & & ??? Coercion Type equality\\
- & & @{text "| sym \<gamma> | \<gamma>\<^isub>1 \<circ> \<gamma>\<^isub>2 | left \<gamma> | right \<gamma> | \<gamma>\<^isub>1 \<sim> \<gamma>\<^isub>2 "}\\
- & & @{text "| rightc \<gamma> | leftc \<gamma> | \<gamma>\<^isub>1 \<triangleright> \<gamma>\<^isub>2"}\medskip\\
+ @{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 "refl \<sigma> | sym \<gamma> | \<gamma>\<^isub>1 \<circ> \<gamma>\<^isub>2 | \<gamma> @ \<sigma> |"}\\
+ & & @{text "left \<gamma> | right \<gamma> | \<gamma>\<^isub>1 \<sim> \<gamma>\<^isub>2 |"}\\
+ & & @{text "rightc \<gamma> | leftc \<gamma> | \<gamma>\<^isub>1 \<triangleright> \<gamma>\<^isub>2"}\medskip\\
\multicolumn{3}{@ {}l}{Terms}\\
- @{text "e"} & @{text "::="} & @{text "x | K | \<Lambda>a:\<kappa>. e | \<Lambda>a:\<iota>. e | e \<sigma> | e \<gamma> |"}\\
- & & @{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 "\<lambda>x:\<sigma>. e | e\<^isub>1 e\<^isub>2 | \<LET> x:\<sigma> = e\<^isub>1 \<IN> e\<^isub>2 |"}\\
& & @{text "\<CASE> e\<^isub>1 \<OF>"}$\;\overline{@{text "p \<rightarrow> e\<^isub>2"}}$ @{text "| e \<triangleright> \<gamma>"}\medskip\\
\multicolumn{3}{@ {}l}{Patterns}\\
- @{text "p"} & @{text "::="} & @{text "K"}$\;\overline{@{text "a:\<kappa>"}}\;\overline{@{text "a:\<iota>"}}\;\overline{@{text "x:\<sigma>"}}$\medskip\\
+ @{text "p"} & @{text "::="} & @{text "K"}$\;\overline{@{text "a:\<kappa>"}}\;\overline{@{text "c:\<iota>"}}\;\overline{@{text "x:\<sigma>"}}$\medskip\\
\multicolumn{3}{@ {}l}{Constants}\\
- @{text C} & & coercion constant\\
- @{text T} & & value type constructor\\
- @{text "S\<^isub>n"} & & n-ary type function\\
- @{text K} & & data constructor\medskip\\
+ @{text C} & & coercion constants\\
+ @{text T} & & value type constructors\\
+ @{text "S\<^isub>n"} & & n-ary type functions\\
+ @{text K} & & data constructors\medskip\\
\multicolumn{3}{@ {}l}{Variables}\\
- @{text a} & & type variable\\
- @{text x} & & term variable\\
+ @{text a} & & type variables\\
+ @{text c} & & coercion variables\\
+ @{text x} & & term variables\\
\end{tabular}
\end{center}
\end{boxedminipage}
- \caption{The term-language of System @{text "F\<^isub>C"}, also often referred to as Core-Haskell,
- according to \cite{CoreHaskell}. We only made an inessential modification by
- separating the grammars for type kinds and coercion types.\label{corehas}}
+ \caption{The term-language of System @{text "F\<^isub>C"}, also often referred to as \emph{Core-Haskell}
+ \cite{CoreHaskell}. In this version of Core-Haskell we made a modification by
+ separating completely the grammars for type kinds and coercion types.\label{corehas}}
\end{figure}
*}
@@ -406,13 +403,16 @@
text {*
At its core, Nominal Isabelle is an adaption of the nominal logic work by
Pitts \cite{Pitts03}. This adaptation for Isabelle/HOL is described in
- \cite{HuffmanUrban10} (including proofs), which we review here briefly to aid the description
- of what follows. Two central notions in the nominal logic work are sorted
- atoms and sort-respecting permutations of atoms. The sorts can be used to
- represent different kinds of variables, such as the term- and type-variables in
- Core-Haskell, and it is assumed that there is an infinite supply of atoms
- for each sort. However, in order to simplify the description, we shall
- assume in what follows that there is only one sort of atoms.
+ \cite{HuffmanUrban10} (including proofs). We shall briefly review this work
+ to aid the description of what follows.
+
+ Two central notions in the nominal
+ logic work are sorted atoms and sort-respecting permutations of atoms. The
+ sorts can be used to represent different kinds of variables, such as the
+ term- and type-variables in Core-Haskell, and it is assumed that there is an
+ infinite supply of atoms for each sort. However, in order to simplify the
+ description, we shall assume in what follows that there is 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
@@ -422,14 +422,15 @@
\noindent
in which the generic type @{text "\<beta>"} stands for the type of the object
- on which the permutation
+ 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 for products, lists, sets, functions, booleans etc (see \cite{HuffmanUrban10})
+ operation is defined by induction over the type-hierarchy, for example as follows
+ for products, lists, sets, functions and booleans (see \cite{HuffmanUrban10}):
- \begin{center}
- \begin{tabular}{@ {}cc@ {}}
+ \begin{equation}
+ \mbox{\begin{tabular}{@ {}cc@ {}}
\begin{tabular}{@ {}l@ {}}
@{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\[2mm]
@{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\
@@ -437,16 +438,15 @@
\end{tabular} &
\begin{tabular}{@ {}l@ {}}
@{thm permute_set_eq[no_vars, THEN eq_reflection]}\\
- @{text "p \<bullet> (f x) \<equiv> (p \<bullet> f) (p \<bullet> x)"}\\
+ @{text "p \<bullet> f \<equiv> \<lambda>x. p \<bullet> (f (- p \<bullet> x))"}\\
@{thm permute_bool_def[no_vars, THEN eq_reflection]}\\
\end{tabular}
- \end{tabular}
- \end{center}
+ \end{tabular}}
+ \end{equation}
\noindent
- Concrete permutations are build up from
- swappings, written as @{text "(a b)"},
- which are permutations that behave as follows:
+ Concrete permutations are build up from swappings, written as @{text "(a
+ b)"}, which are permutations that behave as follows:
%
@{text[display,indent=5] "(a b) = \<lambda>c. if a = c then b else if b = c then a else c"}
@@ -493,9 +493,8 @@
\noindent
it can sometimes be difficult to establish the support precisely,
- and only give an over approximation (see functions above). This
- over approximation can be formalised with the notions \emph{supports},
- defined as follows.
+ and only give an approximation (see functions above). Such approximations can
+ be formalised with the notion \emph{supports}, defined as follows.
\begin{defn}
A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b}
@@ -503,7 +502,7 @@
\end{defn}
\noindent
- The point of this definitions is that we can show:
+ The point of this definition is that we can show:
\begin{property}
{\it i)} @{thm[mode=IfThen] supp_is_subset[no_vars]}
@@ -512,6 +511,19 @@
\noindent
Another important notion in the nominal logic work is \emph{equivariance}.
+ For a function @{text f}, lets say of type @{text "\<alpha> \<Rightarrow> \<beta>"}, to be equivariant
+ means that every permutation leaves @{text f} unchanged, or equivalently that
+ a permutation applied to an application @{text "f x"} can be moved to its
+ arguments. That is
+
+ \begin{center}
+ @{text "\<forall>p. p \<bullet> f = f"} \hspace{5mm}
+ @{text "\<forall>p. p \<bullet> (f x) = f (p \<bullet> x)"}
+ \end{center}
+
+ \noindent
+ From the first equation we can be easily deduce that an equivariant function has
+ empty support.
%\begin{property}
%@{thm[mode=IfThen] at_set_avoiding[no_vars]}