nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:ea84c1a0a23c
+:ac2d0d4ea497
 alpha_res ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{res}}$}}>\<^bsup>_,_,_\<^esup> _") and
 abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
 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)
 (*>*)
 section {* Introduction *}
 \begin{center}
 @{text "\<LET> [x\<^isub>1,\<dots>,x\<^isub>n].s [t\<^isub>1,\<dots>,t\<^isub>n]"}
 \end{center}
 \noindent
-where the notation @{text "[_]._"} indicates that the @{text "x\<^isub>i"}
+where the notation @{text "[_]._"} indicates that the list of @{text "x\<^isub>i"}
-become bound in @{text s}. In this representation the term
+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
 terms are needed in order to ensure that the two lists are of equal
 length. This can result into very messy reasoning (see for
 \begin{center}
 @{text "\<forall>{x}. x \<rightarrow> y  = \<forall>{x, z}. x \<rightarrow> y"}
 \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
 to).
 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 have lists of type- and term-variables (the
+involves patterns that have lists of type-, coercion- and term-variables
-arguments of constructors) all of which are bound in case expressions. One
+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
 \noindent
 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
+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.
 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
 %
-@{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
 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, for example as follows
+operation is defined by induction over the type-hierarchy (see \cite{HuffmanUrban10});
-for products, lists, sets, functions and booleans (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]
 @{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\
 @{thm permute_list.simps(2)[no_vars, THEN eq_reflection]}\\
 \end{tabular}
 \end{tabular}}
 \end{equation}
 \noindent
-Concrete permutations are build up from swappings, written as @{text "(a
+Concrete permutations are built up from swappings, written as \mbox{@{text "(a
-b)"}, which are permutations that behave as follows:
+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
 swapping two fresh atoms, say @{text a} and @{text b}, leave
 @{text x} unchanged.
 \begin{property}
 @{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
 \end{property}
 \noindent
-While it is often clear what the support for a construction is, for
+While often the support of an object can be easily described, for
-example
+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)"}\\
+@{text "supp (f x)"} & @{text "\<subseteq>"} & @{term "supp (f, x)"}\label{suppfun}\\
-@{term "supp b"} & = & @{term "{}"}
+@{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,
+in some cases it can be difficult to establish the support precisely, and
-and only give an approximation (see functions above). Such approximations can
+only give an approximation (see the case for function applications
-be formalised with the notion \emph{supports}, defined as follows.
+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}
 not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.
 \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}
+\begin{property}\label{supportsprop}
-{\it i)} @{thm[mode=IfThen] supp_is_subset[no_vars]}
+{\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
+For a function @{text f}, say of type @{text "\<alpha> \<Rightarrow> \<beta>"}, to be equivariant
-means that every permutation leaves @{text f} unchanged, or equivalently that
+requires that every permutation leaves @{text f} unchanged, or equivalently that
-a permutation applied to an application @{text "f x"} can be moved to its
+a permutation applied to the application @{text "f x"} can be moved to its
 arguments. That is
+%
-\begin{center}
+\begin{equation}\label{equivariance}
-@{text "\<forall>p. p \<bullet> f = f"} \hspace{5mm}
+@{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
+From the first equation and the definition of support shown in \eqref{suppdef},
-empty support.
+we can be easily deduce that an equivariant function has empty support.
-%\begin{property}
+In the next section we use @{text "supp"} and permutations for characterising
-%@{thm[mode=IfThen] at_set_avoiding[no_vars]}
+alpha-equivalence in the presence of multiple binders.
-%\end{property}
 *}
 section {* General Binders\label{sec:binders} *}
 indicating that a set or list is abstracted in @{text x}. We will call the types
 \emph{abstraction types} and their elements \emph{abstractions}. The important
 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]}\\
 @{thm (lhs) supp_abs(2)[no_vars]} & $=$ & @{thm (rhs) supp_abs(2)[no_vars]}\\
 @{thm (lhs) supp_abs(3)[no_vars]} & $=$ & @{thm (rhs) supp_abs(3)[no_vars]}
 \end{tabular}
 \end{center}
 \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
+and also
-operation for abstractions is the one lifted for pairs).\footnote{metion this in the nominal
+%
-logic section}
+\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}
 \begin{proof}
 \begin{equation}\label{halfone}
 @{thm abs_supports(1)[no_vars]}
 \end{equation}
 \noindent
-which with \ref{} gives us one half of Thm~\ref{suppabs}. The other half is
+which with Property~\ref{supportsprop} gives us one half of
-a bit more involved. We first define an auxiliary function
+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]}
+\begin{center}
-\end{center}
+@{thm supp_gen.simps[THEN eq_reflection, no_vars]}
+\end{center}
-\begin{lemma}
+\noindent
-$supp ([as]set. x) = supp x - as$
+Using the second equation in \eqref{equivariance}, we can show that
-\end{lemma}
+@{term "supp_gen"} is equivariant and therefore has empty support. This
+in turn means
-\noindent
+%
-The point of these general lemmas about pairs is that we can define and prove properties
+\begin{center}
-about them conveniently on the Isabelle level, and in addition can use them in what
+@{thm (prem 1) aux_fresh(1)[where bs="as", no_vars]}
-follows next when we have to deal with specific instances of term-specification.
+\;\;implies\;\;
+@{thm (concl) aux_fresh(1)[where bs="as", no_vars]}
+\end{center}
+\noindent
+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,
 @{text ty}$^\alpha_n$, and an associated collection
 of binding functions, say @{text bn}$^\alpha_1$, \ldots, @{text

changeset 1703	ac2d0d4ea497
parent 1702	ea84c1a0a23c
child 1704	cbd6a709a664