--- a/Paper/Paper.thy Mon Mar 29 22:26:19 2010 +0200
+++ b/Paper/Paper.thy Tue Mar 30 02:55:18 2010 +0200
@@ -24,10 +24,11 @@
fv ("fv'(_')" [100] 100) and
equal ("=") and
alpha_abs ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
- Abs ("[_]\<^raw:$\!$>\<^bsub>set\<^esub>._") and
+ Abs ("[_]\<^raw:$\!$>\<^bsub>set\<^esub>._" [20, 101] 999) and
Abs_lst ("[_]\<^raw:$\!$>\<^bsub>list\<^esub>._") and
Abs_res ("[_]\<^raw:$\!$>\<^bsub>res\<^esub>._") and
- Cons ("_::_" [78,77] 73)
+ Cons ("_::_" [78,77] 73) and
+ supp_gen ("aux _" [1000] 100)
(*>*)
@@ -169,8 +170,8 @@
\end{center}
\noindent
- where the notation @{text "[_]._"} indicates that the @{text "x\<^isub>i"}
- become bound in @{text s}. In this representation the term
+ where the notation @{text "[_]._"} indicates that the list of @{text "x\<^isub>i"}
+ becomes bound in @{text s}. In this representation the term
\mbox{@{text "\<LET> [x].s [t\<^isub>1, t\<^isub>2]"}} is a perfectly legal
instance, but the lengths of two lists do not agree. To exclude such terms,
additional predicates about well-formed
@@ -236,7 +237,7 @@
\end{center}
\noindent
- are not just alpha-equal, but actually \emph{equal}. As a result, we can
+ are not just alpha-equal, but actually \emph{equal}! As a result, we can
only support specifications that make sense on the level of alpha-equated
terms (offending specifications, which for example bind a variable according
to a variable bound somewhere else, are not excluded by Ott, but we have
@@ -341,8 +342,8 @@
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 have lists of type- and term-variables (the
- arguments of constructors) all of which are bound in case expressions. One
+ involves patterns that have lists of type-, coercion- and term-variables
+ all of which are bound in @{text "\<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
@@ -411,7 +412,7 @@
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
+ term-, coercion- 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.
@@ -420,7 +421,9 @@
the identity everywhere except on a finite number of atoms. There is a
two-place permutation operation written
%
- @{text[display,indent=5] "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
+ \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
@@ -428,10 +431,10 @@
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, for example as follows
- for products, lists, sets, functions and booleans (see \cite{HuffmanUrban10}):
+ operation is defined by induction over the type-hierarchy (see \cite{HuffmanUrban10});
+ for example as follows for products, lists, sets, functions and booleans:
%
- \begin{equation}
+ \begin{equation}\label{permute}
\mbox{\begin{tabular}{@ {}cc@ {}}
\begin{tabular}{@ {}l@ {}}
@{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\[2mm]
@@ -447,30 +450,36 @@
\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 built up from swappings, written as \mbox{@{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"}
-
+ \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
- definition for the notion of ``the set of free variables of an object @{text
+ definition for the notion of the ``set of free variables of an object @{text
"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:
%
- @{thm[display,indent=5] supp_def[no_vars, THEN eq_reflection]}
+ \begin{equation}\label{suppdef}
+ @{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
%
- @{thm[display,indent=5] fresh_def[no_vars]}
+ \begin{center}
+ @{thm fresh_def[no_vars]}
+ \end{center}
\noindent
We also use for sets of atoms the abbreviation
- @{thm (lhs) fresh_star_def[no_vars]} defined as
+ @{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
@@ -482,21 +491,24 @@
\end{property}
\noindent
- While it is often clear what the support for a construction is, for
- example
+ While often the support of an object can be easily described, for
+ example\\[-6mm]
%
\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, xs)"}\\
- @{text "supp (f x)"} & @{text "\<subseteq>"} & @{term "supp (f, x)"}\\
- @{term "supp b"} & = & @{term "{}"}
+ @{text "supp (f x)"} & @{text "\<subseteq>"} & @{term "supp (f, x)"}\label{suppfun}\\
+ @{term "supp b"} & = & @{term "{}"}\\
+ @{term "supp p"} & = & @{term "{a. p \<bullet> a \<noteq> a}"}
\end{eqnarray}
\noindent
- it can sometimes be difficult to establish the support precisely,
- and only give an approximation (see functions above). Such approximations can
- be formalised with the notion \emph{supports}, defined as follows.
+ in some cases it can be difficult to establish the support precisely, and
+ only give an approximation (see the case for function applications
+ above). Such approximations can be made precise 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}
@@ -504,33 +516,31 @@
\end{defn}
\noindent
- The point of this definition is that we can show:
+ The main point of this definition is that we can show the following two properties.
- \begin{property}
- {\it i)} @{thm[mode=IfThen] supp_is_subset[no_vars]}
+ \begin{property}\label{supportsprop}
+ {\it i)} @{thm[mode=IfThen] supp_is_subset[no_vars]}\\
{\it ii)} @{thm supp_supports[no_vars]}.
\end{property}
- \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
+ For a function @{text f}, say of type @{text "\<alpha> \<Rightarrow> \<beta>"}, to be equivariant
+ requires that every permutation leaves @{text f} unchanged, or equivalently that
+ a permutation applied to the application @{text "f x"} can be moved to its
arguments. That is
-
- \begin{center}
- @{text "\<forall>p. p \<bullet> f = f"} \hspace{5mm}
+ %
+ \begin{equation}\label{equivariance}
+ @{text "\<forall>p. p \<bullet> f = f"} \;\;if and only if\;\;
@{text "\<forall>p. p \<bullet> (f x) = f (p \<bullet> x)"}
- \end{center}
+ \end{equation}
\noindent
- From the first equation we can be easily deduce that an equivariant function has
- empty support.
+ From the first equation and the definition of support shown in \eqref{suppdef},
+ we can be easily deduce that an equivariant function has empty support.
- %\begin{property}
- %@{thm[mode=IfThen] at_set_avoiding[no_vars]}
- %\end{property}
-
+ In the next section we use @{text "supp"} and permutations for characterising
+ alpha-equivalence in the presence of multiple binders.
+
*}
@@ -719,7 +729,7 @@
property we need is a characterisation for the support of abstractions, namely
\begin{thm}[Support of Abstractions]\label{suppabs}
- Assuming @{text x} has finite support, then
+ Assuming @{text x} has finite support, then\\[-6mm]
\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]}\\
@@ -730,20 +740,29 @@
\end{thm}
\noindent
- We will only show in the rest of the section the first equation, as the others
+ We will only show the first equation as the others
follow 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 (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
- With this, we can show the following lemma about swapping two atoms (the permutation
- operation for abstractions is the one lifted for pairs).\footnote{metion this in the nominal
- logic section}
+ and also
+ %
+ \begin{equation}
+ @{thm permute_Abs[no_vars]}
+ \end{equation}
+ \noindent
+ The last fact derives from the definition of permutations acting on pairs
+ (see \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.
+
\begin{lemma}
@{thm[mode=IfThen] abs_swap1(1)[no_vars]}
\end{lemma}
@@ -763,28 +782,48 @@
\end{equation}
\noindent
- which with \ref{} gives us one half of Thm~\ref{suppabs}. The other half is
- a bit more involved. We first define an auxiliary function
+ which with Property~\ref{supportsprop} gives us one half of
+ Thm~\ref{suppabs}. The other half is a bit more involved. For this we use a
+ trick from \cite{Pitts04} and first define an auxiliary function
%
\begin{center}
- @{thm supp_res.simps[THEN eq_reflection, no_vars]}
+ @{thm supp_gen.simps[THEN eq_reflection, no_vars]}
\end{center}
-
- \begin{lemma}
- $supp ([as]set. x) = supp x - as$
- \end{lemma}
+ \noindent
+ Using the second equation in \eqref{equivariance}, we can show that
+ @{term "supp_gen"} is equivariant and therefore has empty support. This
+ in turn means
+ %
+ \begin{center}
+ @{thm (prem 1) aux_fresh(1)[where bs="as", no_vars]}
+ \;\;implies\;\;
+ @{thm (concl) aux_fresh(1)[where bs="as", no_vars]}
+ \end{center}
\noindent
- The point of these general lemmas about pairs is that we can define and prove properties
- about them conveniently on the Isabelle level, and in addition can use them in what
- follows next when we have to deal with specific instances of term-specification.
+ using \eqref{suppfun}. Since @{term "supp x"} is by definition equal
+ to @{term "{a. \<not> a \<sharp> x}"} we can establish that
+ %
+ \begin{equation}\label{halftwo}
+ @{thm (concl) supp_abs_subset1(1)[no_vars]}
+ \end{equation}
+
+ \noindent
+ provided @{text x} has finite support (the precondition we need in order to show
+ that for a finite set of atoms, we have @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}).
+
+ Finally taking \eqref{halfone} and \eqref{halftwo} provides us with a proof
+ of Theorem~\ref{suppabs}. The point of these general lemmas about abstractions is that we
+ can define and prove properties about them conveniently on the Isabelle/HOL level,
+ and in addition can use them in what
+ follows next when we have to deal with binding in specifications of term-calculi.
*}
section {* Alpha-Equivalence and Free Variables *}
text {*
- Our specifications for term-calculi are heavily inspired by the existing
+ Our choice of syntax for specifications of term-calculi is influenced by the existing
datatype package of Isabelle/HOL and by the syntax of the Ott-tool
\cite{ott-jfp}. A specification is a collection of (possibly mutual
recursive) type declarations, say @{text "ty"}$^\alpha_1$, \ldots,