nominal2: comparison LMCS-Paper/Paper.thy

equal deleted inserted replaced

-:d13ac9f4e773
+:4bad521e3b9e
 \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
+``alpha-equivalent'' to @{text S}. This is because unbinding is a relation, not a function.
+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
+The problem 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
+an existential quantifier). The representation of type-schemes using iterations of 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
+allow us to represent type-schemes so that they can bind multiple variables at once
-a result solve this problem.
+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.
 we would like to regard in \eqref{ex1} below  the first pair of type-schemes as alpha-equivalent,
 but assuming that @{text x}, @{text y} and @{text z} are distinct variables,
 the second pair should \emph{not} be alpha-equivalent:
 \begin{equation}\label{ex1}
-@{text "\<forall>{x, y}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{y, x}. y \<rightarrow> x"}\hspace{10mm}
+@{text "\<forall>{x, y}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{x, y}. y \<rightarrow> x"}\hspace{10mm}
 @{text "\<forall>{x, y}. x \<rightarrow> y  \<notapprox>\<^isub>\<alpha>  \<forall>{z}. z \<rightarrow> z"}
 \end{equation}\smallskip
 \noindent
 Moreover, we like to regard type-schemes as alpha-equivalent, if they differ
 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 automatically-generated
+inspired by earlier work of Pitts \cite{Pitts04}. By means of automati\-cally-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
 @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
 @{thm permute_list.simps(2)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
 \end{tabular} &
 \begin{tabular}{@ {}l@ {}}
 @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", no_vars, THEN eq_reflection]}\\
-@{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+@{thm permute_set_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
 @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f (- \<pi> \<bullet> x))"}\\
 @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}
 \end{tabular}
 \end{tabular}}
 \end{equation}\smallskip
 Another important notion in the nominal logic work is \emph{equivariance}.
 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"}
+@{term "\<forall>\<pi>. \<pi> \<bullet> f = f"}\;.
 \end{equation}\smallskip
 \noindent
 If a function is of type @{text "\<alpha> \<Rightarrow> \<beta>"}, this definition is equivalent to
 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>"}:
+such functions, 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)"}
+@{text "\<forall>x. \<pi> \<bullet> (f x) = f (\<pi> \<bullet> x)"}\;.
 \end{equation}\smallskip
 \noindent
 There is
 also a similar property for relations, which are in HOL functions of type @{text "\<alpha> \<Rightarrow> \<beta> \<Rightarrow> bool"}.
-Suppose a relation @{text R}, then
+Suppose a relation @{text R}, then for all permutations @{text \<pi>}:
-that for all permutations @{text \<pi>}:
 \[
 @{text "\<pi> \<bullet> R = R"} \;\;\;\;\textit{if and only if}\;\;\;\;
-@{text "\<forall>x y."}~~@{text "x R y"} \;\textit{implies}\; @{text "(\<pi> \<bullet> x) R (\<pi> \<bullet> y)"}
+@{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.
+can easily deduce that for a function being equivariant is equivalent to having empty support.
 Using freshness, the nominal logic work provides us with general means for renaming
 binders.
 \noindent
 \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}). If the types are polymorphic, we require the
-type variables are of finitely supported type.
+type variables stand for types that are finitely supported and over which
-The labels annotated on the types are optional. Their
+a permutation operation is defined.
+The labels @{text "label"}$_{1..l}$ 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}:
 \noindent
 Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"}  pick
 out different atoms to become bound, respectively be free, in @{text "p"}.
 (Since the Ott-tool does not derive a reasoning infrastructure for
 alpha-equated terms with deep binders, it can permit such specifications.)
+For convenience we exlude such specifications even if @{text "bn\<^isub>1"} and
+@{text "bn\<^isub>2"} are the same binding functions, which would otherwise be harmless.
 We also need to restrict the form of the binding functions in order to
 ensure the @{text "bn"}-functions can be defined for alpha-equated
 terms. The main restriction is that we cannot return an atom in a binding
 function that is also bound in the corresponding term-constructor.
 Consider again the specification for @{text "trm"} and a contrived

changeset 3128	4bad521e3b9e
parent 3126	d3d5225f4f24
child 3129	8be3155c014f