nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:9d8ebeded16f
+:9832641ed955
 third \emph{only} holds because of our restriction
 imposed on the form of the binding functions---namely \emph{not} returning
 any bound atoms. In Ott, in contrast, the user may
 define @{text "bn"}$_{1..m}$ so that they return bound
 atoms and in this case the third implication is \emph{not} true. A
-result is that the lifing of the corresponding binding functions to $\alpha$-equated
+result is that the lifing of the corresponding binding functions in Ott to $\alpha$-equated
 terms is impossible.
 Having established respectfulness for the raw term-constructors, the
 quotient package is able to automatically deduce \eqref{distinctalpha} from
 \eqref{distinctraw}. Having the facts \eqref{fnresp} at our disposal, we can
 \noindent
 to our infrastructure. In a similar fashion we can lift the defining equations
 of the free-atom functions @{text "fn_ty\<AL>"}$_{1..n}$ and
 @{text "fa_bn\<AL>"}$_{1..m}$ as well as of the binding functions @{text
-"bn\<AL>"}$_{1..m}$ and of the size functions @{text "size_ty\<AL>"}$_{1..n}$.
+"bn\<AL>"}$_{1..m}$ and the size functions @{text "size_ty\<AL>"}$_{1..n}$.
 The latter are defined automatically for the raw types @{text "ty"}$_{1..n}$
 by the datatype package of Isabelle/HOL.
 Finally we can add to our infrastructure a structural induction principle
 for the types @{text "ty\<AL>"}$_{i..n}$ whose
 in \eqref{weakinduct}.
 Having these equivariant properties established, we can
 show for every term-constructor @{text "C\<^sup>\<alpha>"} that
 \begin{center}
-@{text "(supp x\<^isub>1 \<union> \<dots> supp x\<^isub>r) supports (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r)"}
+@{text "(supp x\<^isub>1 \<union> \<dots> \<union> supp x\<^isub>r) supports (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r)"}
 \end{center}
 \noindent
-holds. This together with Property~\ref{supportsprop} allows us to show
+holds. This together with Property~\ref{supportsprop} allows us to prove
-for every @{text x} of type @{text "ty\<AL>"}$_{1..n}$ is finitely supported,
+that every @{text x} of type @{text "ty\<AL>"}$_{1..n}$ is finitely supported,
 namely @{text "finite (supp x)"}. This can be again shown by induction
 over @{text "ty\<AL>"}$_{1..n}$. Lastly, we can show that the support of
 elements in  @{text "ty\<AL>"}$_{1..n}$ is the same as @{text "fa_ty\<AL>"}$_{1..n}$.
-This important fact provides evidence that our notions of free-atoms and
+This fact is important in a nominal setting, but also provides evidence
-$\alpha$-equivalence are correct.
+that our notions of free-atoms and $\alpha$-equivalence are correct.
 \begin{lemma}
 For every @{text "x"} of type @{text "ty\<AL>"}$_{1..n}$, we have
 @{text "supp x = fa_ty\<AL>\<^isub>i x"}.
 \end{lemma}
 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, we can established automatically a reasoning infrastructure
+To sum up this section, we can established 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. This code can deal with
-specifications like the one shown in Figure~\ref{nominalcorehas} for Core-Haskell.
+specifications such as the one shown in Figure~\ref{nominalcorehas} for Core-Haskell.
 \begin{figure}[t!]
 \begin{boxedminipage}{\linewidth}
 \small
 \begin{tabular}{l}
 section {* Strong Induction Principles *}
 text {*
 In the previous section we were able to provide induction principles that
 allow us to perform structural inductions over $\alpha$-equated terms.
-We call such induction principles \emph{weak}, because in case of a term-constructor @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r"},
+We call such induction principles \emph{weak}, because in case of the
+term-constructor @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r"},
 the induction hypothesis requires us to establish the implications \eqref{weakprem}.
-The problem with these implications is that in general they are not easy to establish.
+The problem with these implications is that in general they are difficult to establish.
 The reason is that we cannot make any assumption about the binders that might be in @{text "C\<^sup>\<alpha>"}
 (for example we cannot assume the variable convention for them).
 In \cite{UrbanTasson05} we introduced a method for automatically
 strengthening weak induction principles for terms containing single
 the general binders presented here. We will indeed be able to so, but for this we need an
 additional notion for permuting deep binders.
 Given a binding function @{text "bn"} we define an auxiliary permutation
 operation @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} which permutes only bound arguments in a deep binder.
-Assuming a clause of @{text bn} is defined as @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, then
+Assuming a clause of @{text bn} is given as
-we define @{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>n) \<equiv> C y\<^isub>1 \<dots> y\<^isub>n"} with @{text "y\<^isub>i"} determined as follows:
+%
+\begin{center}
+@{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"},
+\end{center}
+\noindent
+then we define
+%
+\begin{center}
+@{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"}
+\end{center}
+\noindent
+with @{text "y\<^isub>i"} determined as follows:
 %
 \begin{center}
 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
 $\bullet$ & @{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\
 $\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\
 Using again the quotient package  we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to
 $\alpha$-equated terms. We can then prove the following two facts
 \begin{lemma}\label{permutebn}
 Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text p}
-{\it i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<^bsub>bn\<^esub>\<^sup>\<alpha> x)"} and {\it ii)}
+{\it (i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"} and {\it (ii)}
-@{text "fa_bn\<^isup>\<alpha> x = fa_bn\<^isup>\<alpha> (p \<bullet>\<^bsub>bn\<^esub>\<^sup>\<alpha> x)"}.
+@{text "fa_bn\<^isup>\<alpha> x = fa_bn\<^isup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"}.
 \end{lemma}
 \begin{proof}
 By induction on @{text x}. The equations follow by simple unfolding
 of the definitions.
 effect on the free-atom function. The main point of this permutation
 function, however, is that if we have a permutation that is fresh
 for the support of an object @{text x}, then we can use this permutation
 to rename the binders in @{text x}, without ``changing'' @{text x}. In case of the
 @{text "Let"} term-constructor from the example shown
-\eqref{letpat} this means for a permutation @{text "r"}:
+in \eqref{letpat} this means for a permutation @{text "r"}
 %
 \begin{equation}\label{renaming}
 \begin{array}{l}
 \mbox{if @{term "supp (Abs_lst (bn p) t\<^isub>2)  \<sharp>* r"}}\\
-\qquad\mbox{then @{text "Let p t\<^isub>1 t\<^isub>2 = Let (r \<bullet>\<^bsub>bnpat\<^esub> p) t\<^isub>1 (r \<bullet> t\<^isub>2)"}}
+\qquad\mbox{then @{text "Let p t\<^isub>1 t\<^isub>2 = Let (r \<bullet>\<AL>\<^bsub>bn_pat\<^esub> p) t\<^isub>1 (r \<bullet> t\<^isub>2)"}}
 \end{array}
 \end{equation}
 \noindent
-This fact will be crucial when establishing the strong induction principles.
+This fact will be crucial when establishing the strong induction principles below.
-In our running example about @{text "Let"}, they state that instead
+In our running example about @{text "Let"}, the strong induction
+principle means that instead
 of establishing the implication
 %
 \begin{center}
 @{text "\<forall>p t\<^isub>1 t\<^isub>2. P\<^bsub>pat\<^esub> p \<and> P\<^bsub>trm\<^esub> t\<^isub>1 \<and> P\<^bsub>trm\<^esub> t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Let p t\<^isub>1 t\<^isub>2)"}
 \end{center}
 \end{equation}
 \noindent
 While this implication contains an additional argument, namely @{text c}, and
 also additional universal quantifications, it is usually easier to establish.
-The reason is that we can make the freshness
+The reason is that we have the freshness
 assumption @{text "set (bn\<^sup>\<alpha> p) #\<^sup>* c"}, whereby @{text c} can be arbitrarily
 chosen by the user as long as it has finite support.
 Let us now show how we derive the strong induction principles from the
 weak ones. In case of the @{text "Let"}-example we derive by the weak
 induction the following two properties
 %
 \begin{equation}\label{hyps}
 @{text "\<forall>q c. P\<^bsub>trm\<^esub> c (q \<bullet> t)"} \hspace{4mm}
-@{text "\<forall>q\<^isub>1 q\<^isub>2 c. P\<^bsub>pat\<^esub> (q\<^isub>1 \<bullet>\<^bsub>bn\<^esub> (q\<^isub>2 \<bullet> p))"}
+@{text "\<forall>q\<^isub>1 q\<^isub>2 c. P\<^bsub>pat\<^esub> (q\<^isub>1 \<bullet>\<AL>\<^bsub>bn\<^esub> (q\<^isub>2 \<bullet> p))"}
 \end{equation}
 \noindent
 For the @{text Let} term-constructor  we therefore have to establish @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}
 assuming \eqref{hyps} as induction hypotheses (the first for @{text t\<^isub>1} and @{text t\<^isub>2}).
 hold. The latter fact and \eqref{renaming} give us
 %
 \begin{center}
 \begin{tabular}{l}
 @{text "Let (q \<bullet> p) (q \<bullet> t\<^isub>1) (q \<bullet> t\<^isub>2) ="} \\
-\hspace{15mm}@{text "Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2))"}
+\hspace{15mm}@{text "Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2))"}
 \end{tabular}
 \end{center}
 \noindent
 So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}, we can equally
-establish @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2)))"}.
+establish @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2)))"}.
 To do so, we will use the implication \eqref{strong} of the strong induction
 principle, which requires us to discharge
 the following four proof obligations:
 %
 \begin{center}
 \begin{tabular}{rl}
-{\it i)} &   @{text "set (bn (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p))) #\<^sup>* c"}\\
+{\it (i)} &   @{text "set (bn (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))) #\<^sup>* c"}\\
-{\it ii)} &  @{text "\<forall>d. P\<^bsub>pat\<^esub> d (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p))"}\\
+{\it (ii)} &  @{text "\<forall>d. P\<^bsub>pat\<^esub> d (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))"}\\
-{\it iii)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (q \<bullet> t\<^isub>1)"}\\
+{\it (iii)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (q \<bullet> t\<^isub>1)"}\\
-{\it iv)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (r \<bullet> (q \<bullet> t\<^isub>2))"}\\
+{\it (iv)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (r \<bullet> (q \<bullet> t\<^isub>2))"}\\
 \end{tabular}
 \end{center}
 \noindent
-The first follows from \eqref{rprops} and Lemma~\ref{permutebn}.{\it i)}; the
+The first follows from \eqref{rprops} and Lemma~\ref{permutebn}.{\it (i)}; the
 others from the induction hypotheses in \eqref{hyps} (in the fourth case
 we have to use the fact that @{term "(r \<bullet> (q \<bullet> t\<^isub>2)) = (r + q) \<bullet> t\<^isub>2"}).
 Taking now the identity permutation @{text 0} for the permutations in \eqref{hyps},
 we can establish our original goals, namely @{text "P\<^bsub>trm\<^esub> c t"} and \mbox{@{text "P\<^bsub>pat\<^esub> c p"}}.
-This completes the proof showing that the strong induction principle derives from
+This completes the proof showing that the weak induction principles imply
-the weak induction principle. For the moment we can derive the difficult cases of
+the strong induction principles.
-the strong induction principles only by hand, but they are very schematic
-so that with little effort we can even derive them for
-Core-Haskell given in Figure~\ref{nominalcorehas}.
 *}
 section {* Related Work *}
 versions of Nominal Isabelle (one about Psi-calculi and one about algorithm W
 \cite{BengtsonParow09, UrbanNipkow09}).  Both
 use the approach based on iterated single binders. Our experience with
 the latter formalisation has been disappointing. The major pain arose from
 the need to ``unbind'' variables. This can be done in one step with our
-general binders, but needs a cumbersome
+general binders described in this paper, but needs a cumbersome
 iteration with single binders. The resulting formal reasoning turned out to
 be rather unpleasant. The hope is that the extension presented in this paper
 is a substantial improvement.
 The most closely related work to the one presented here is the Ott-tool
 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
 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 HOL-based theorem prover. We also had to generalise slightly their
+meaning in a HOL-based theorem prover. We also had to generalise slightly Ott's
 binding clauses. In Ott you specify 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{bind\_set} and
-\isacommand{bind\_res}. For example
+\isacommand{bind\_res}. Consider the examples
 \begin{center}
 \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
 @{text "Foo\<^isub>1 xs::name fset t::trm s::trm"} &
 \isacommand{bind\_set} @{text "xs"} \isacommand{in} @{text "t s"}\\
 \isacommand{bind\_set} @{text "xs"} \isacommand{in} @{text "s"}\\
 \end{tabular}
 \end{center}
 \noindent
-in the first term-constructor we have a single
+In the first term-constructor we have a single
 body that happens to be ``spread'' over two arguments; in the second term-constructor we have
 two independent bodies in which the same variables are bound. As a result we
 have
 \begin{center}
 reasoning infrastructure is well beyond the purposes of his language.
 In a slightly different domain (programming with dependent types), the
 paper \cite{Altenkirch10} presents a calculus with a notion of
 $\alpha$-equivalence related to our binding mode \isacommand{bind\_res}.
-The corresponding definition is similar to the one by Pottier, except that it
+The definition in \cite{Altenkirch10} is similar to the one by Pottier, except that it
 has a more operational flavour and calculates a partial (renaming) map.
-In this way Altenkirch et al can deal with vacuous binders. However, to our
+In this way, the definition can deal with vacuous binders. However, to our
-best knowledge, no concrete mathematical result concerning their notion
+best knowledge, no concrete mathematical result concerning this
-of equality has been proved.
+definition of $\alpha$-equivalence has been proved.
 *}
 section {* Conclusion *}
 text {*
 We have presented an extension of Nominal Isabelle for dealing with
 general binders, that is term-constructors having multiple bound
 variables. For this extension we introduced novel definitions of
 $\alpha$-equivalence and automated all necessary proofs in Isabelle/HOL.
-We have tried out the extension with terms from Core-Haskell and our code
+To specify general binders we used the syntax from Ott, but modified
-will become part of the Isabelle distribution.\footnote{For the moment
+it so that it makes sense in our context of $\alpha$-equated terms.
+We have tried out the extension with terms from Core-Haskell, type-schemes
+and the lambda-calculus, and our code
+will eventually become part of the next Isabelle distribution.\footnote{For the moment
 it can be downloaded from the Mercurial repository linked at
 \href{http://isabelle.in.tum.de/nominal/download}
 {http://isabelle.in.tum.de/nominal/download}.}
 We have left out a discussion about how functions can be defined over
 hope to do better this time by using the function package that has recently
 been implemented in Isabelle/HOL and also by restricting function
 definitions to equivariant functions (for such functions it is possible to
 provide more automation).
-There are some restrictions we imposed in this paper, that we would like to lift in
+There are some restrictions we imposed in this paper that we would like to lift in
 future work. One is the exclusion of nested datatype definitions. Nested
 datatype definitions allow one to specify, for instance, the function kinds
 in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded
 version @{text "TFun string ty_list"} (see Figure~\ref{nominalcorehas}). To
 achieve this, we need a slightly more clever implementation than we have at the moment.
 A more interesting line of investigation is whether we can go beyond the
-simple-minded form for binding functions that we adopted from Ott. At the moment, binding
+simple-minded form of binding functions that we adopted from Ott. At the moment, binding
 functions can only return the empty set, a singleton atom set or unions
 of atom sets (similarly for lists). It remains to be seen whether
 properties like
 %
 \begin{center}

changeset 2363	9832641ed955
parent 2362	9d8ebeded16f
child 2364	2bf351f09317