nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:c86b98642013
+:e1093e680bcf
 %These additional assumptions amount to a formal
 %version of the informal variable convention for binders.
 To sketch how this strengthening extends to the case of multiple binders, we use as
 running example the term-constructors @{text "Lam"} and @{text "Let"}
 from example \eqref{letpat}. Instead of establishing @{text " P\<^bsub>trm\<^esub> t \<and> P\<^bsub>pat\<^esub> p"},
-the stronger induction principles establish properties @{text " P\<^bsub>trm\<^esub> c t \<and> P\<^bsub>pat\<^esub> c p"}
+the stronger induction principle for \eqref{letpat} establishes properties @{text " P\<^bsub>trm\<^esub> c t \<and> P\<^bsub>pat\<^esub> c p"}
 where the additional parameter @{text c} controls
 which freshness assumptions the binders should satisfy. For the two term constructors
 this means that the user has to establish in inductions the implications
 %
 \begin{center}
 \begin{tabular}{l}
 @{text "\<forall>a t c. {atom a} \<FRESH>\<^sup>* c \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t) \<Rightarrow> P\<^bsub>trm\<^esub> c (Lam a t)"}\\
-@{text "\<forall>p t c. (set (bn p)) \<FRESH>\<^sup>* c \<and> (\<forall>d. P\<^bsub>pat\<^esub> d p) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t) \<and> \<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t)"}
+@{text "\<forall>p t c. (set (bn p)) \<FRESH>\<^sup>* c \<and> (\<forall>d. P\<^bsub>pat\<^esub> d p) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t) \<and> \<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t)"}\\%[-0mm]
 \end{tabular}
 \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.
+The reasoning principle these methods employ is well-founded induction.
-The reasoning principle we employ here is well-founded induction. For this we have to discharge
+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.
-As measures we use are the size functions
+As measures we 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 these measures decrease
 in every induction step.
 What is left to show is that we covered all cases. To do so, we use
-a cases lemma derived for each type, which for the terms in \eqref{letpat}
+a cases lemma derived for each type. For the terms in \eqref{letpat}
-is of the form
+this lemma is of the form
 %
 \begin{equation}\label{weakcases}
 \infer{@{text "P\<^bsub>trm\<^esub>"}}
 {\begin{array}{l@ {\hspace{9mm}}l}
 @{text "\<forall>x. t = Var x \<Rightarrow> P\<^bsub>trm\<^esub>"} & @{text "\<forall>a t'. t = Lam a t' \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
 @{text "\<forall>t\<^isub>1 t\<^isub>2. t = App t\<^isub>1 t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"} & @{text "\<forall>p t'. t = Let p t' \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
-\end{array}}
+\end{array}}\\[-1mm]
 \end{equation}
 %
-These cases lemmas have a premise for each term-constructor.
+where we have a premise for each term-constructor.
-The idea behind them is that we can conclude with a property @{text "P\<^bsub>trm\<^esub>"},
+The idea behind such cases lemmas is that we can conclude with a property @{text "P\<^bsub>trm\<^esub>"},
 provided we can show that this property holds if we substitute for @{text "t"} all
 possible term-constructors.
 The only remaining difficulty is that in order to derive the stronger induction
 principles conveniently, the cases lemma in \eqref{weakcases} is too weak. For this note that
 in order to apply this lemma, we have to establish @{text "P\<^bsub>trm\<^esub>"} for \emph{all} @{text Lam}- and
 \emph{all} @{text Let}-terms.
 What we need instead is a cases rule where we only have to consider terms that have
-binders being fresh w.r.t.~a context @{text "c"}, namely
+binders that are fresh w.r.t.~a context @{text "c"}. This gives the implications
 %
 \begin{center}
 \begin{tabular}{l}
 @{text "\<forall>a t'. t = Lam a t' \<and> {atom a} \<FRESH>\<^sup>* c \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
-@{text "\<forall>p t'. t = Let p t' \<and> (set (bn p)) \<FRESH>\<^sup>* c \<Rightarrow> P\<^bsub>trm\<^esub>"}
+@{text "\<forall>p t'. t = Let p t' \<and> (set (bn p)) \<FRESH>\<^sup>* c \<Rightarrow> P\<^bsub>trm\<^esub>"}\\%[-2mm]
 \end{tabular}
 \end{center}
 %
-However, this can be relatively easily be derived from the implications in \eqref{weakcases}
+\noindent
+which however can be relatively easily be derived from the implications in \eqref{weakcases}
 by a renaming using Properties \ref{supppermeq} and \ref{avoiding}. In the first case we know
 that @{text "{atom a} \<FRESH>\<^sup>* Lam a t"}. Property \eqref{avoiding} provides us therefore with
 a permutation @{text q}, such that @{text "{atom (q \<bullet> a)} \<FRESH>\<^sup>* c"} and
 @{text "supp (Lam a t) \<FRESH>\<^sup>* q"} hold.
-By using Property \ref{supppermeq}, we can infer that @{text "Lam (q \<bullet> a) (q \<bullet> t) = Lam a t"}
+By using Property \ref{supppermeq}, we can infer from the latter
+that @{text "Lam (q \<bullet> a) (q \<bullet> t) = Lam a t"}
 and we are done with this case.
 The @{text Let}-case involving a (non-recursive) deep binder is a bit more complicated.
 The reason is that the we cannot apply Property \ref{avoiding} to the whole term @{text "Let p t"},
-because @{text p} might contain names that are bound (by @{text bn}) and that are
+because @{text p} might contain names that are bound (by @{text bn}) and so are
-free. To solve this problem we have to introduce a permutation functions that only
+free. To solve this problem we have to introduce a permutation function that only
 permutes names bound by @{text bn} and leaves the other names unchanged. We do this again
-by lifting. Assuming a
+by lifting. For a
 clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, 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"} \;\; with
 $\begin{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"}. But
+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
-these facts establish that @{text "Let (q \<bullet>\<^bsub>bn\<^esub> p) (p \<bullet> t) = Let p t"}, as we need. This
+hese facts establish that @{text "Let (q \<bullet>\<^bsub>bn\<^esub> p) (p \<bullet> t) = Let p t"}, as we need. This
-completes the interesting cases in \eqref{letpat} for strengthening the induction
+completes the non-trivial cases in \eqref{letpat} for strengthening the corresponding induction
-principles.
+principle.
 %A natural question is
 %whether we can also strengthen the weak induction principles involving
 technique supports very elegantly many aspects of \emph{single} binding, and
 impressive work has been done that uses HOAS for mechanising the metatheory
 of SML~\cite{LeeCraryHarper07}. We are, however, not aware how multiple
 binders of SML are represented in this work. Judging from the submitted
 Twelf-solution for the POPLmark challenge, HOAS cannot easily deal with
-binding constructs where the number of bound variables is not fixed. %For
+binding constructs where the number of bound variables is not fixed. %For example
-example
 In the second part of this challenge, @{text "Let"}s involve
 patterns that bind multiple variables at once. In such situations, HOAS
 seems to have to resort to the iterated-single-binders-approach with
 all the unwanted consequences when reasoning about the resulting terms.
 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
-is work in progress in Ott.
+is in Ott 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
 To specify general binders we used the specifications from Ott, but extended them
 in some places and restricted
 them in others so that they make sense in the context of $\alpha$-equated terms.
 We also introduced two binding modes (set and res) that do not
 exist in Ott.
-We have tried out the extension with terms from Core-Haskell, type-schemes
+We have tried out the extension with calculi such as Core-Haskell, type-schemes
-and a dozen of other calculi from programming language research. The code
+and approximately a  dozen of other typical examples from programming
+language research \cite{SewellBestiary}. The 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}.}

changeset 2517	e1093e680bcf
parent 2516	c86b98642013
child 2518	7044f796d8d1