nominal2: comparison LMCS-Paper/Paper.thy

equal deleted inserted replaced

-:4bad521e3b9e
+:8be3155c014f
 \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, like @{text "\<forall>x\<^isub>1.\<forall>x\<^isub>2...\<forall>x\<^isub>n.T"}, this leads to a rather clumsy
 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}
+type is an instance of a type-scheme requires in the iterated version
+the following auxiliary \emph{unbinding relation}
 \[
 \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
+which relates a type-scheme with a list of type-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
+definition is: given a type-scheme @{text S}, how to get access to the bound type-variables
-@{text S}, though in general
+and the type-part of this type-scheme? The unbinding relation gives an answer, though in general
-we will only get access to some variables and some type @{text T} that are
+we will only get access to some type-variables and some type that are
-``alpha-equivalent'' to @{text S}. This is because unbinding is a relation, not a function.
+``alpha-equivalent'' to @{text S}. This is because unbinding is a relation; it cannot be a function
+for alpha-equated type-schemes.
 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
+meaning there exists a list of type-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 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 using iterations of single binders
+an existential quantifier and only an alpha-variant). The representation of
-prevents us from directly ``unbinding'' the bound variables and the type-part of
+type-schemes using iterations of single binders
-a type-scheme. The purpose of this paper is to introduce general binders, which
+prevents us from directly ``unbinding'' the bound thye-variables and the type-part.
+The purpose of this paper is to introduce general binders, which
 allow us to represent type-schemes so that they can bind multiple variables at once
 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
+mechanisms for binding single variables have so far not fared very well with
 the more advanced tasks in the POPLmark challenge \cite{challenge05},
 because also there one would like to bind multiple variables at once.
 Binding multiple variables has interesting properties that cannot be captured
 easily by iterating single binders. For example in the case of type-schemes we do not
 ourselves in what follows to 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 "_ \<bullet> _  ::  perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
+@{text "_ \<bullet> _ "} and having the type @{text "perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
 where the generic type @{text "\<beta>"} is 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 "\<pi>\<^isub>1"} and @{term "\<pi>\<^isub>2"} as \mbox{@{term "\<pi>\<^isub>1 + \<pi>\<^isub>2"}},
 and the inverse permutation of @{term "\<pi>"} as @{text "- \<pi>"}. The permutation
 \begin{equation}\label{equivariancedef}
 @{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
+If a function is of type @{text "\<alpha> \<Rightarrow> \<beta>"}, say, 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
 such functions, we have for all permutations @{text "\<pi>"}:
 \begin{equation}\label{equivariance}
 @{thm (lhs) Abs_eq_iff(1)[where bs="as" and bs'="bs", no_vars]} \;\;\;\text{if and only if}\;\;\;
 @{term "alpha_set_ex (as, x) equal supp (bs, y)"}
 \end{equation}\smallskip
 \noindent
-and also
+and also set
 \begin{equation}\label{absperm}
-@{thm permute_Abs(1)[where p="\<pi>", no_vars]}
+@{thm permute_Abs(1)[where p="\<pi>", no_vars, THEN eq_reflection]}
 \end{equation}\smallskip
 \noindent
-The second fact derives from the definition of permutations acting on pairs
+With this at our disposal, we can show
-\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 in an abstraction.
 \begin{lem}
 If @{thm (prem 1) Abs_swap1(1)[where bs="as", no_vars]} and
 @{thm (prem 2) Abs_swap1(1)[where bs="as", no_vars]} then
 @{thm (concl) Abs_supp_subset1(1)[no_vars]}
 \end{equation}\smallskip
 \noindent
 This is because for every finite set of atoms, say @{text "bs"}, we have
-@{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.
+@{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.\footnote{Note that this is not
+the case for infinite sets.}
 Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes
 the first equation of Theorem~\ref{suppabs}. The others are similar.
 Recall the definition of support given in \eqref{suppdef}, and note the difference between
 the support of a raw pair and an abstraction
 \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 stand for types that are finitely supported and over which
+type variables to stand for types that are finitely supported and over which
 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}:
 specification:
 \begin{equation}\label{letrecs}
 \mbox{%
 \begin{tabular}{@ {}l@ {}l}
-\isacommand{nominal\_datatype}~@{text "trm ="}~\ldots\\
+\isacommand{nominal\_datatype}~@{text "trm ="}\\
+\hspace{5mm}\phantom{$\mid$}~\ldots\\
 \hspace{5mm}$\mid$~@{text "Let as::assn t::trm"}
 & \hspace{-19mm}\isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text t}\\
 \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"}
 & \hspace{-19mm}\isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text "as t"}\\
 \isacommand{and} @{text "assn"} $=$\\
 \end{tabular}}
 \]\smallskip
 \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"}.
+out different atoms to become bound, respectively be free,
-(Since the Ott-tool does not derive a reasoning infrastructure for
+in @{text "p"}.\footnote{Although harmless, in our implementation
-alpha-equated terms with deep binders, it can permit such specifications.)
+we exlude such specifications even
-For convenience we exlude such specifications even if @{text "bn\<^isub>1"} and
+if @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"} are the same binding
-@{text "bn\<^isub>2"} are the same binding functions, which would otherwise be harmless.
+functions.}$^,$\footnote{Since the Ott-tool does not derive a reasoning
+infrastructure for
+alpha-equated terms with deep binders, it can permit such specifications.}
 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.
 As measures we can use the size functions @{text "size_ty"}$^\alpha_{1..n}$,
 which we lifted in the previous section and which are all well-founded. It
 is straightforward to establish that the sizes decrease in every
 induction step. What is left to show is that we covered all cases.
 To do so, we have to derive stronger cases lemmas, which look in our
-running example are as follows:
+running example as follows:
 \[\mbox{
 \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}
 \infer{@{text "P\<^bsub>trm\<^esub>"}}
 {\begin{array}{@ {}l@ {}}

changeset 3129	8be3155c014f
parent 3128	4bad521e3b9e
child 3130	8fc6b801985b