nominal2: comparison LMCS-Paper/Paper.thy

equal deleted inserted replaced

-:860df8e1262f
+:d3d5225f4f24
 \end{equation}\smallskip
 \noindent
 and the @{text "\<forall>"}-quantification binds a finite (possibly empty) set of
 type-variables.  While it is possible to implement this kind of more general
-binders by iterating single binders, this leads to a rather clumsy
+binders by iterating single binders, like @{text "\<forall>x\<^isub>1.\<forall>x\<^isub>2...\<forall>x\<^isub>n.T"}, this leads to a rather clumsy
-formalisation of W.
+formalisation of W. For example, the usual definition when a
+type is an instance of a type-scheme requires the following auxiliary \emph{unbinding relation}
-{\bf add example about W}
+\[
+\infer{@{text T} \hookrightarrow ([], @{text T})}{}\qquad
+\infer{\forall @{text x.S} \hookrightarrow (@{text x}\!::\!@{text xs}, @{text T})}
+{@{text S} \hookrightarrow (@{text xs}, @{text T})}
+\]\smallskip
+\noindent
+which relates a type-scheme with a list of variables and a type. The point of this
+definition is to get access to the bound variables and the type-part of a type-scheme
+@{text S}, though in general
+we will only get access to some variables and some type @{text T} that are
+``alpha-equivalent'' to @{text S}---it is an unbinding \emph{relation}. Still, with this
+definition in place we can formally define when a type is an instance of a type-scheme as
+\[
+@{text "T \<prec> S \<equiv> \<exists>xs T' \<sigma>. S \<hookrightarrow> (xs, T') \<and> dom \<sigma> = set xs \<and> \<sigma>(T') = T"}
+\]\smallskip
+\noindent
+meaning there exists a list of variables @{text xs} and a type @{text T'} to which
+the type-scheme @{text S} unbinds, and there exists a substitution whose domain is
+@{text xs} (seen as set) such that @{text "\<sigma>(T') = T"}.
+The pain with this definition is that we cannot follow the usual proofs
+that are by induction on the type-part of the type-scheme (since it is under
+an existential quantifier). The representation of type-schemes by iterating single binders
+prevents us from directly ``unbinding'' the bound variables and the type-part of
+a type-scheme. The purpose of this paper is to introduce general binders, which
+allow us to represent type-schemes following closely informal practice and as
+a result solve this problem.
 The need of iterating single binders is also one reason
 why Nominal Isabelle and similar theorem provers that only provide
 mechanisms for binding single variables have not fared extremely well with
 the more advanced tasks in the POPLmark challenge \cite{challenge05},
 because also there one would like to bind multiple variables at once.
 which includes multiple binders in type-schemes.\medskip
 \noindent
 {\bf Contributions:} We provide three new definitions for when terms
 involving general binders are alpha-equivalent. These definitions are
-inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic
+inspired by earlier work of Pitts \cite{Pitts04}. By means of automatically-generated
 proofs, we establish a reasoning infrastructure for alpha-equated terms,
 including properties about support, freshness and equality conditions for
 alpha-equated terms. We are also able to automatically derive strong
 induction principles that have the variable convention already built in.
 For this we simplify the earlier automated proofs by using the proving tools
 \noindent
 The main point of @{text supports} is that we can establish the following
 two properties.
 \begin{prop}\label{supportsprop}
-Given a set @{text "as"} of atoms.\\
+Given a set @{text "bs"} of atoms.\\
-{\it (i)} If @{thm (prem 1) supp_is_subset[where S="as", no_vars]}
+{\it (i)} If @{thm (prem 1) supp_is_subset[where S="bs", no_vars]}
-and @{thm (prem 2) supp_is_subset[where S="as", no_vars]} then
+and @{thm (prem 2) supp_is_subset[where S="bs", no_vars]} then
-@{thm (concl) supp_is_subset[where S="as", no_vars]}.\\
+@{thm (concl) supp_is_subset[where S="bs", no_vars]}.\\
 {\it (ii)} @{thm supp_supports[no_vars]}.
 \end{prop}
 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
+For a function @{text f} to be equivariant
 it is required that every permutation leaves @{text f} unchanged, that is
 \begin{equation}\label{equivariancedef}
 @{term "\<forall>\<pi>. \<pi> \<bullet> f = f"}
 \end{equation}\smallskip
-\noindent or equivalently that a permutation applied to the application
+\noindent
-@{text "f x"} can be moved to the argument @{text x}. That means for equivariant
+If a function is of type @{text "\<alpha> \<Rightarrow> \<beta>"}, this definition is equivalent to
-functions @{text f}, we have for all permutations @{text "\<pi>"}:
+the fact that a permutation applied to the application
+@{text "f x"} can be moved to the argument @{text x}. That means for
+functions @{text f} of type @{text "\<alpha> \<Rightarrow> \<beta>"}, we have for all permutations @{text "\<pi>"}:
 \begin{equation}\label{equivariance}
 @{text "\<pi> \<bullet> f = f"} \;\;\;\;\textit{if and only if}\;\;\;\;
 @{text "\<forall>x. \<pi> \<bullet> (f x) = f (\<pi> \<bullet> x)"}
 \end{equation}\smallskip
 \noindent
-From property \eqref{equivariancedef} and the definition of @{text supp}, we
+There is
-can easily deduce that equivariant functions have empty support. There is
+also a similar property for relations, which are in HOL functions of type @{text "\<alpha> \<Rightarrow> \<beta> \<Rightarrow> bool"}.
-also a similar notion for equivariant relations, say @{text R}, namely the property
+Suppose a relation @{text R}, then
-that
+that for all permutations @{text \<pi>}:
 \[
-@{text "x R y"} \;\;\textit{implies}\;\; @{text "(\<pi> \<bullet> x) R (\<pi> \<bullet> y)"}
+@{text "\<pi> \<bullet> R = R"} \;\;\;\;\textit{if and only if}\;\;\;\;
-\]\smallskip
+@{text "\<forall>x y."}~~@{text "x R y"} \;\textit{implies}\; @{text "(\<pi> \<bullet> x) R (\<pi> \<bullet> y)"}
+\]\smallskip
+\noindent
+Note that from property \eqref{equivariancedef} and the definition of @{text supp}, we
+can easily deduce that equivariant functions have empty support.
 Using freshness, the nominal logic work provides us with general means for renaming
 binders.
 \noindent
 While in the older version of Nominal Isabelle, we used extensively
-Property~\ref{swapfreshfresh} to rename single binders, this property
+Proposition~\ref{swapfreshfresh} to rename single binders, this property
 proved too unwieldy for dealing with multiple binders. For such binders the
 following generalisations turned out to be easier to use.
 \begin{prop}\label{supppermeq}
 @{thm[mode=IfThen] supp_perm_eq[where p="\<pi>", no_vars]}
 The first question we have to answer is when two pairs @{text "(as, x)"} and
 @{text "(bs, y)"} are alpha-equivalent? (For the moment we are interested in
 the notion of alpha-equivalence that is \emph{not} preserved by adding
 vacuous binders.) To answer this question, we identify four conditions: {\it (i)}
 given a free-atom function @{text "fa"} of type \mbox{@{text "\<beta> \<Rightarrow> atom
-set"}}, then @{text x} and @{text y} need to have the same set of free
+set"}}, then @{text "(as, x)"} and @{text "(bs, y)"} need to have the same set of free
 atoms; moreover there must be a permutation @{text \<pi>} such that {\it
-(ii)} @{text \<pi>} leaves the free atoms of @{text x} and @{text y} unchanged, but
+(ii)} @{text \<pi>} leaves the free atoms of @{text "(as, x)"} and @{text "(bs, y)"} unchanged, but
 {\it (iii)} `moves' their bound names so that we obtain modulo a relation,
 say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it (iv)}
 @{text \<pi>} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
 requirements {\it (i)} to {\it (iv)} can be stated formally as:
 \]\smallskip
 \noindent
 Now recall the examples shown in \eqref{ex1} and
 \eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and
-@{text "({y, x}, y \<rightarrow> x)"} are alpha-equivalent according to
+@{text "({x, y}, y \<rightarrow> x)"} are alpha-equivalent according to
 $\approx_{\,\textit{set}}$ and $\approx_{\,\textit{set+}}$ by taking @{text "\<pi>"} to
 be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"}, then @{text
 "([x, y], x \<rightarrow> y)"} $\not\approx_{\,\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"}
 since there is no permutation that makes the lists @{text "[x, y]"} and
 @{text "[y, x]"} equal, and also leaves the type \mbox{@{text "x \<rightarrow> y"}}
 (supp x - as)"}.  We therefore can use the swapping @{term "(a \<rightleftharpoons> b)"} as
 the permutation for the proof obligation.
 \end{proof}
 \noindent
-Assuming that @{text "x"} has finite support, this lemma together
+This lemma together
 with \eqref{absperm} allows us to show
 \begin{equation}\label{halfone}
 @{thm Abs_supports(1)[no_vars]}
 \end{equation}\smallskip
 \noindent
 which by Property~\ref{supportsprop} gives us `one half' of
-Theorem~\ref{suppabs}. The `other half' is a bit more involved. To establish
+Theorem~\ref{suppabs}. To establish the `other half', we
-it, we use a trick from \cite{Pitts04} and first define an auxiliary
+use a trick from \cite{Pitts04} and first define an auxiliary
 function @{text aux}, taking an abstraction as argument
 \[
 @{thm supp_set.simps[THEN eq_reflection, no_vars]}
 \]\smallskip
 contained in the collection of @{text ty}$^\alpha_{1..n}$ declared in
 \eqref{scheme}. In this case we will call the corresponding argument a
 \emph{recursive argument} of @{text "C\<^sup>\<alpha>"}. The types of such
 recursive arguments need to satisfy a `positivity' restriction, which
 ensures that the type has a set-theoretic semantics (see
-\cite{Berghofer99}).  The labels annotated on the types are optional. Their
+\cite{Berghofer99}). If the types are polymorphic, we require the
+type variables are of finitely supported type.
+The labels annotated on the types are optional. Their
 purpose is to be used in the (possibly empty) list of \emph{binding
 clauses}, which indicate the binders and their scope in a term-constructor.
 They come in three \emph{modes}:
 Although we were heavily inspired by the syntax of Ott, its definition of
 alpha-equi\-valence is unsuitable for our extension of Nominal
 Isabelle. First, it is far too complicated to be a basis for automated
 proofs implemented on the ML-level of Isabelle/HOL. Second, it covers cases
 of binders depending on other binders, which just do not make sense for our
-alpha-equated terms. Third, it allows empty types that have no meaning in a
+alpha-equated terms (the corresponding @{text "fa"}-functions would not lift).
+Third, it allows empty types that have no meaning in a
 HOL-based theorem prover. We also had to generalise slightly Ott's binding
 clauses. In Ott one specifies binding clauses with a single body; we allow
 more than one. We have to do this, because this makes a difference for our
 notion of alpha-equivalence in case of \isacommand{binds (set)} and
 \isacommand{binds (set+)}. Consider the examples

changeset 3126	d3d5225f4f24
parent 3107	e26e933efba0
child 3128	4bad521e3b9e