nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:6c131c089ce2
+:6b3e8602edcf
 %``$\alpha$-equals-by-$\alpha$-equals'' in a representation based on raw terms
 %requires a lot of extra reasoning work.
 Although in informal settings a reasoning infrastructure for $\alpha$-equated
 terms is nearly always taken for granted, establishing it automatically in
-the Isabelle/HOL is a rather non-trivial task. For every
+Isabelle/HOL is a rather non-trivial task. For every
 specification we will need to construct type(s) containing as elements the
 $\alpha$-equated terms. To do so, we use the standard HOL-technique of defining
 a new type by identifying a non-empty subset of an existing type.  The
 construction we perform in Isabelle/HOL can be illustrated by the following picture:
 %
 Two central notions in the nominal logic work are sorted atoms and
 sort-respecting permutations of atoms. We will use the letters @{text "a,
 b, c, \<dots>"} to stand for atoms and @{text "p, q, \<dots>"} to stand for
 permutations. The purpose of atoms is to represent variables, be they bound or free.
 The sorts of atoms can be used to represent different kinds of
-variables.
+variables, such as the term-, coercion- and type-variables in Core-Haskell.
-%%, such as the term-, coercion- and type-variables in Core-Haskell.
 It is assumed that there is an infinite supply of atoms for each
-sort. However, in the interest of brevity, we shall restrict ourselves
+sort. In the interest of brevity, we shall restrict 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
 over which the permutation
 acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"},
 the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}},
 and the inverse permutation of @{term p} as @{text "- p"}. The permutation
 operation is defined over the type-hierarchy \cite{HuffmanUrban10};
-for example permutations acting on products, lists, sets, functions and booleans is
+for example permutations acting on products, lists, sets, functions and booleans are
 given by:
 %
 %\begin{equation}\label{permute}
 %\mbox{\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
 %\begin{tabular}{@ {}l@ {}}
 %\end{center}
 %
 %\noindent
 for the binding functions @{text "bn"}$_{1..m}$,
 To simplify our definitions we will use the following abbreviations for
-\emph{compound equivalence relations} and \emph{compound free-atom functions} acting on tuples
+\emph{compound equivalence relations} and \emph{compound free-atom functions} acting on tuples.
 %
 \begin{center}
 \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
 @{text "(x\<^isub>1,\<dots>, x\<^isub>n) (R\<^isub>1,\<dots>, R\<^isub>n) (x\<PRIME>\<^isub>1,\<dots>, x\<PRIME>\<^isub>n)"} & @{text "\<equiv>"} &
 @{text "x\<^isub>1 R\<^isub>1 x\<PRIME>\<^isub>1 \<and> \<dots> \<and> x\<^isub>n R\<^isub>n x\<PRIME>\<^isub>n"}\\
 \noindent
 Note the difference between  $\approx_{\textit{assn}}$ and
 $\approx_{\textit{bn}}$: the latter only ``tracks'' $\alpha$-equivalence of
 the components in an assignment that are \emph{not} bound. This is needed in the
-in the clause for @{text "Let"} (which is has
+clause for @{text "Let"} (which has
 a non-recursive binder).
 %The underlying reason is that the terms inside an assignment are not meant
 %to be ``under'' the binder. Such a premise is \emph{not} needed in @{text "Let_rec"},
 %because there all components of an assignment are ``under'' the binder.
 *}
 term-constructors and then use the quasi-injectivity lemmas in order to complete the
 proof. For the abstraction cases we use the facts derived in Theorem~\ref{suppabs}.
 \end{proof}
 \noindent
-To sum up this section, we can established automatically a reasoning infrastructure
+To sum up this section, we can establish automatically a reasoning infrastructure
 for the types @{text "ty\<AL>"}$_{1..n}$
 by first lifting definitions from the raw level to the quotient level and
 then by establishing facts about these lifted definitions. All necessary proofs
 are generated automatically by custom ML-code.
 \end{center}
 In \cite{UrbanTasson05} we showed how the weaker induction principles imply
 the stronger ones. This was done by some quite complicated, nevertheless automated,
 induction proofs. In this paper we simplify this work by leveraging the automated proof
-methods from the function package of Isabelle/HOL generates.
+methods from the function package of Isabelle/HOL.
 The reasoning principle these methods employ is well-founded induction.
 To use them in our setting, we have to discharge
 two proof obligations: one is that we have
 well-founded measures (for each type @{text "ty"}$^\alpha_{1..n}$) that decrease in
 every induction step and the other is that we have covered all cases.
 %\end{center}
 %
 \noindent
 Now Properties \ref{supppermeq} and \ref{avoiding} give us a permutation @{text q} such that
 @{text "(set (bn (q \<bullet>\<^bsub>bn\<^esub> p)) \<FRESH>\<^sup>* c"} holds and such that @{text "[q \<bullet>\<^bsub>bn\<^esub> p]\<^bsub>list\<^esub>.(q \<bullet> t)"}
-is equal to @{text "[p]\<^bsub>list\<^esub>. t"}. We can also show that @{text "(q \<bullet>\<^bsub>bn\<^esub> p) \<approx>\<^bsub>bn\<^esub> p"}. T
+is equal to @{text "[p]\<^bsub>list\<^esub>. t"}. We can also show that @{text "(q \<bullet>\<^bsub>bn\<^esub> p) \<approx>\<^bsub>bn\<^esub> p"}.
-hese facts establish that @{text "Let (q \<bullet>\<^bsub>bn\<^esub> p) (p \<bullet> t) = Let p t"}, as we need. This
+These facts establish that @{text "Let (q \<bullet>\<^bsub>bn\<^esub> p) (p \<bullet> t) = Let p t"}, as we need. This
 completes the non-trivial cases in \eqref{letpat} for strengthening the corresponding induction
 principle.
 de-Bruijn indices representation. Since type-schemes in W contain only a single
 place where variables are bound, different indices do not refer to different binders (as in the usual
 de-Bruijn representation), but to different bound variables. A similar idea
 has been recently explored for general binders in the locally nameless
 approach to binding \cite{chargueraud09}.  There, de-Bruijn indices consist
-of two numbers, one referring to the place where a variable is bound and the
+of two numbers, one referring to the place where a variable is bound, and the
 other to which variable is bound. The reasoning infrastructure for both
 representations of bindings comes for free in theorem provers like Isabelle/HOL or
 Coq, since the corresponding term-calculi can be implemented as ``normal''
 datatypes.  However, in both approaches it seems difficult to achieve our
 fine-grained control over the ``semantics'' of bindings (i.e.~whether the
 terms, and in Coq also a locally nameless representation. The developers of
 this tool have also put forward (on paper) a definition for
 $\alpha$-equivalence of terms that can be specified in Ott.  This definition is
 rather different from ours, not using any nominal techniques.  To our
 knowledge there is also no concrete mathematical result concerning this
-notion of $\alpha$-equivalence.  A definition for the notion of free variables
+notion of $\alpha$-equivalence.  Also the definition for the
-is in Ott work in progress.
+notion of free variables
+is work in progress.
 Although we were heavily inspired by the syntax of Ott,
 its definition of $\alpha$-equivalence 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

changeset 2580	6b3e8602edcf
parent 2555	8cf5c3e58889
child 2604	431cf4e6a7e2