# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1286548514 -3600
# Node ID e1093e680bcf933a243d3ad646363c467254bcf0
# Parent  c86b98642013d351317ef7c55bff47600a2c38d9
minor

diff -r c86b98642013 -r e1093e680bcf Paper/Paper.thy
--- a/Paper/Paper.thy	Fri Oct 08 13:41:54 2010 +0100
+++ b/Paper/Paper.thy	Fri Oct 08 15:35:14 2010 +0100
@@ -1934,7 +1934,7 @@
   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
@@ -1942,7 +1942,7 @@
   \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}
 
@@ -1950,30 +1950,30 @@
   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 we employ here is well-founded induction. For this we have to discharge
+  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. 
-  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} 
-  is of the form
+  a cases lemma derived for each type. For the terms in \eqref{letpat} 
+  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.
-  The idea behind them is that we can conclude with a property @{text "P\<^bsub>trm\<^esub>"},
+  where we have a premise for each term-constructor.
+  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. 
   
@@ -1982,29 +1982,31 @@
   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 
-  free. To solve this problem we have to introduce a permutation functions that only
+  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 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}
@@ -2030,10 +2032,10 @@
   \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
-  these 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
-  principles.
+  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
+  hese 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.
   
 
 
@@ -2220,8 +2222,7 @@
   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
-  example 
+  binding constructs where the number of bound variables is not fixed. %For 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
@@ -2250,7 +2251,7 @@
   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
@@ -2337,8 +2338,9 @@
   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 
-  and a dozen of other calculi from programming language research. The code
+  We have tried out the extension with calculi such as Core-Haskell, type-schemes 
+  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}