nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:a908ea36054f
+:4c5881455923
 easily by iterating single binders. For example in the case of type-schemes we do not
 want to make a distinction about the order of the bound variables. Therefore
 we would like to regard the following two type-schemes as $\alpha$-equivalent
 %
 \begin{equation}\label{ex1}
-@{text "\<forall>{x, y}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{y, x}. y \<rightarrow> x"}
+@{text "\<forall>{x, y}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{y, x}. x \<rightarrow> y"}
 \end{equation}
 \noindent
 but assuming that @{text x}, @{text y} and @{text z} are distinct variables,
 the following two should \emph{not} be $\alpha$-equivalent
 \noindent
 The scope of the binding is indicated by labels given to the types, for
 example @{text "s::trm"}, and a binding clause, in this case
 \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}. This binding
-clause states to bind in @{text s} all the names the function @{text
+clause states that all the names the function @{text
-"bn(as)"} returns.  This style of specifying terms and bindings is heavily
+"bn(as)"} returns should be bound in @{text s}.  This style of specifying terms and bindings is heavily
 inspired by the syntax of the Ott-tool \cite{ott-jfp}.
 However, we will not be able to cope with all specifications that are
 allowed by Ott. One reason is that Ott lets the user specify ``empty''
 types like
 be bound. Another is that each bound variable comes 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
-{\bf Contributions:}  We provide novel definitions for when terms
+{\bf Contributions:}  We provide novel three 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
 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 derive strong
 induction principles that have the variable convention already built in.
 The method behind our specification of general binders is taken
-from the Ott-tool, but we introduce crucial restrictions, and also one extension, so
+from the Ott-tool, but we introduce crucial restrictions, and also extensions, so
 that our specifications make sense for reasoning about $\alpha$-equated terms.
 \begin{figure}
 \begin{boxedminipage}{\linewidth}
 \end{tabular}}
 \end{equation}
 \noindent
 In this specification the function @{text "bn"} determines which atoms of
-@{text p} are bound in the argument @{text "t"}. Note that in the
+the pattern @{text p} are bound in the argument @{text "t"}. Note that in the
 second-last @{text bn}-clause the function @{text "atom"} coerces a name
 into the generic atom type of Nominal Isabelle \cite{HuffmanUrban10}. This
 allows us to treat binders of different atom type uniformly.
 As said above, for deep binders we allow binding clauses such as
 \end{equation}
 \noindent
 The difference is that with @{text Let} we only want to bind the atoms @{text
 "bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms
-inside the assignment. This difference has consequences for the free-variable
+inside the assignment. This difference has consequences for the associated
-function and $\alpha$-equivalence relation.
+notions of free-variables and $\alpha$-equivalence.
 To make sure that variables bound by deep binders cannot be free at the
-same time, we cannot have more than one binding function for one deep binder.
+same time, we cannot have more than one binding function for a deep binder.
 Consequently we exclude specifications such as
 \begin{center}
 \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
 @{text "Baz\<^isub>1 p::pat t::trm"} &
 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"}.
 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. As a result we cannot return an atom in a binding function that is also
+terms. The main restriction is that we cannot return an atom in a binding function that is also
-bound in the corresponding term-constructor. That means in the example
+bound in the corresponding term-constructor. That means in \eqref{letpat}
-\eqref{letpat} that the term-constructors @{text PVar} and @{text PTup} may
+that the term-constructors @{text PVar} and @{text PTup} may
 not have a binding clause (all arguments are used to define @{text "bn"}).
 In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons}
 may have a binding clause involving the argument @{text t} (the only one that
 is \emph{not} used in the definition of the binding function). This restriction
 is sufficient for defining the binding function over $\alpha$-equated terms.
 Pottier and Cheney pointed out \cite{Pottier06,Cheney05}, just
 re-arranging the arguments of
 term-constructors so that binders and their bodies are next to each other will
 result in inadequate representations in cases like @{text "Let x\<^isub>1=t\<^isub>1\<dots>x\<^isub>n=t\<^isub>n in s"}.
 Therefore we will first
-extract datatype definitions from the specification and then define
+extract ``raw'' datatype definitions from the specification and then define
 explicitly an $\alpha$-equivalence relation over them. We subsequently
 quotient the datatypes according to our $\alpha$-equivalence.
-The datatype definition can be obtained by stripping off the
+The ``raw'' datatype definition can be obtained by stripping off the
 binding clauses and the labels from the types. We also have to invent
 new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}
 given by the user. In our implementation we just use the affix ``@{text "_raw"}''.
 But for the purpose of this paper, we use the superscript @{text "_\<^sup>\<alpha>"} to indicate
 that a notion is defined over $\alpha$-equivalence classes and leave it out
 @{text "p \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (p \<bullet> z\<^isub>1) \<dots> (p \<bullet> z\<^isub>n)"}
 \end{equation}
 The first non-trivial step we have to perform is the generation of
 free-variable functions from the specifications. For the
-\emph{raw} types @{text "ty"}$_{1..n}$ extracted from  a specification,
+\emph{raw} types @{text "ty"}$_{1..n}$ we define the free-variable functions
-we define the free-variable functions
 %
 \begin{equation}\label{fvars}
 @{text "fv_ty\<^isub>1, \<dots>, fv_ty\<^isub>n"}
 \end{equation}
 \noindent
-by recursion over the types @{text "ty"}$_{1..n}$.
+by mutual recursion.
 We define these functions together with auxiliary free-variable functions for
 the binding functions. Given raw binding functions @{text "bn"}$_{1..m}$
 we define
 %
 \begin{center}
 that calculates those unbound atoms in a deep binder.
 While the idea behind these free-variable functions is clear (they just
 collect all atoms that are not bound), because of our rather complicated
 binding mechanisms their definitions are somewhat involved.  Given
-the term-constructor @{text "C"} of type @{text ty} and some associated
+a term-constructor @{text "C"} of type @{text ty} and some associated
 binding clauses @{text "bc\<^isub>1\<dots>bc\<^isub>k"}, the result of @{text
 "fv_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be the union @{text
 "fv(bc\<^isub>1) \<union> \<dots> \<union> fv(bc\<^isub>k)"} where we define below what @{text "fv"} of a binding
-clause with mode \isacommand{bin\_set} means (similarly for the other modes).
+clause means. We only show the mode \isacommand{bind\_set} (the other modes are similar).
 Suppose the binding clause @{text bc\<^isub>i} is of the form
 %
 \begin{equation}
 \mbox{\isacommand{bind\_set} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}}
 \end{equation}
 \end{center}
 \noindent
 whereby the functions @{text "fv_ty\<^isub>i"} are the ones we are defining by recursion
 (see \eqref{fvars}) provided the @{text "d\<^isub>i"} refers to one of the raw types
-@{text "ty"}$_{1..n}$ from a specification; otherwise we set @{text "fv_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
+@{text "ty"}$_{1..n}$ from the specification; otherwise we set @{text "fv_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
 In order to define the set @{text B} we use the following auxiliary @{text "bn"}-functions
 for atom types to which shallow binders have to refer
 %
 \begin{center}
 \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}

changeset 2346	4c5881455923
parent 2345	a908ea36054f
child 2347	9807d30c0e54