nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:62b87efcef29
+:55cb244b020c
 \end{center}
 \noindent
 As a result, we provide three general binding mechanisms each of which binds
 multiple variables at once, and let the user chose which one is intended
-when formalising a programming language calculus.
+when formalising a term-calculus.
 By providing these general binding mechanisms, however, we have to work
 around a problem that has been pointed out by Pottier \cite{Pottier06} and
 Cheney \cite{Cheney05}: in @{text "\<LET>"}-constructs of the form
 %
 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-, coercion- and term-variables
+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
 \end{center}
 \end{boxedminipage}
 \caption{The term-language of System @{text "F\<^isub>C"}
 \cite{CoreHaskell}, also often referred to as \emph{Core-Haskell}. In this
 version of the term-language we made a modification by separating the
-grammars for type and coercion kinds, as well as for types and coercion
+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}
 *}
 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). We shall briefly review this work
 to aid the description of what follows.
-Two central notions in the nominal
+Two central notions in the nominal logic work are sorted atoms and
-logic work are sorted atoms and sort-respecting permutations of atoms. The
+sort-respecting permutations of atoms. We will use the variables @{text "a,
-sorts can be used to represent different kinds of variables, such as the
+b, c, \<dots>"} to stand for atoms and @{text "p, q, \<dots>"} to stand for
-term-, coercion- and type-variables in Core-Haskell, and it is assumed that there is an
+permutations.  The sorts of atoms can be used to represent different kinds of
-infinite supply of atoms for each sort. However, in order to simplify the
+variables, such as the term-, coercion- and type-variables in Core-Haskell,
-description, we shall assume in what follows that there is only one sort of
+and it is assumed that there is an infinite supply of atoms for each
-atoms.
+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
 %
 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}
+\begin{property}\label{swapfreshfresh}
 @{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
 \end{property}
-\noindent
+While often the support of an object can be relatively easily
-While often the support of an object can be easily described, for
+described, for example\\[-6mm]
-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)"}\\
+@{term "supp (x#xs)"} & = & @{term "supp x \<union> supp xs"}\\
 @{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
 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
+above). Such approximations can be calculated 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"}.
 {\it ii)} @{thm supp_supports[no_vars]}.
 \end{property}
 Another important notion in the nominal logic work is \emph{equivariance}.
 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
+requires that every permutation leaves @{text f} unchanged, that is
-a permutation applied to the application @{text "f x"} can be moved to its
+%
-arguments. That is
+\begin{equation}\label{equivariancedef}
+@{term "\<forall>p. p \<bullet> f = f"}
+\end{equation}
+\noindent or equivalently that a permutation applied to the application
+@{text "f x"} can be moved to the argument @{text x}. That means we have for
+all permutations @{text p}
 %
 \begin{equation}\label{equivariance}
-@{text "\<forall>p. p \<bullet> f = f"} \;\;if and only if\;\;
+@{text "p \<bullet> f = f"} \;\;\;\textit{if and only if}\;\;\;
-@{text "\<forall>p. p \<bullet> (f x) = f (p \<bullet> x)"}
+@{text "p \<bullet> (f x) = f (p \<bullet> x)"}
 \end{equation}
 \noindent
-From the first equation and the definition of support shown in \eqref{suppdef},
+From equation \eqref{equivariancedef} and the definition of support shown in
-we can be easily deduce that an equivariant function has empty support.
+\eqref{suppdef}, we can be easily deduce that an equivariant function has
+empty support.
-In the next section we use @{text "supp"} and permutations for characterising
-alpha-equivalence in the presence of multiple binders.
+Finally, the nominal logic work provides us with elegant means to rename
+binders. While in the older version of Nominal Isabelle, we used extensively
+Property~\ref{swapfreshfresh} for renaming single binders, this property
+proved unwieldy for dealing with multiple binders. For this the following
+generalisations turned out to be easier to use.
+\begin{property}\label{supppermeq}
+@{thm[mode=IfThen] supp_perm_eq[no_vars]}
+\end{property}
+\begin{property}
+For a finite set @{text xs} and a finitely supported @{text x} with
+@{term "xs \<sharp>* x"} and also a finitely supported @{text c}, there
+exists a permutation @{text p} such that @{term "(p \<bullet> xs) \<sharp>* c"} and
+@{term "supp x \<sharp>* p"}.
+\end{property}
+\noindent
+The idea behind the second property is that given a finite set @{text xs}
+of binders (being bound in @{text x} which is ensured by the
+assumption @{term "xs \<sharp>* x"}), then there exists a permutation @{text p} such that
+the renamed binders @{term "p \<bullet> xs"} avoid the @{text c} (which can be arbitrarily chosen
+as long as it is finitely supported) and also does not affect anything
+in the support of @{text x} (that is @{term "supp x \<sharp>* p"}). The last
+fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders
+in @{text x}, because @{term "p \<bullet> x = x"}.
+All properties given in this section are formalised in Isabelle/HOL and also
+most of them are described with proofs in \cite{HuffmanUrban10}. In the next section
+we make extensively use of the properties of @{text "supp"} and permutations
+for characterising alpha-equivalence in the presence of multiple binders.
 *}
 section {* General Binders\label{sec:binders} *}

changeset 1711	55cb244b020c
parent 1708	62b87efcef29
child 1712	40f13b52b107