# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1315923272 -7200
# Node ID e2c4ee6e3ee7bd4d67e16118c1fe15cbc4f709ce
# Parent  a33e96e62a2b7e8ab482f1868c30697dee0b503e
more on paper

diff -r a33e96e62a2b -r e2c4ee6e3ee7 LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Tue Sep 13 09:30:34 2011 +0200
+++ b/LMCS-Paper/Paper.thy	Tue Sep 13 16:14:32 2011 +0200
@@ -1716,11 +1716,11 @@
   establishing the reasoning infrastructure for the alpha-equated types @{text
   "ty\<AL>"}$_{1..n}$, that is the types the user originally specified. We
   give in this section and the next the proofs we need for establishing this
-  infrastructure. One main point of our work is that we have completely
+  infrastructure. One point of our work is that we have completely
   automated these proofs in Isabelle/HOL.
 
   First we establish that the free-variable functions, the binding functions and the
-  alpha-equivalences are equivariant.
+  alpha-equi\-va\-lences are equivariant.
 
   \begin{lem}\mbox{}\\
   @{text "(i)"} The functions @{text "fa_ty"}$_{1..n}$, @{text "fa_bn"}$_{1..m}$ and
@@ -1730,15 +1730,16 @@
   \end{lem}
 
   \begin{proof}
-  The function package of Isabelle/HOL allows us to prove the first part is by mutual 
-  induction over the definitions of the functions. The second is by a straightforward
-  induction over the rules of @{text "\<approx>ty"}$_{1..n}$ and @{text "\<approx>bn"}$_{1..m}$ using 
-  the first part.
+  The function package of Isabelle/HOL allows us to prove the first part is by
+  mutual induction over the definitions of the functions (we know that they
+  are terminating functions, from which an induction principle can be
+  derived). The second is by a straightforward induction over the rules of
+  @{text "\<approx>ty"}$_{1..n}$ and @{text "\<approx>bn"}$_{1..m}$ using the first part.
   \end{proof}
 
   \noindent
   Next we establish that the alpha-equivalence relations defined in the
-  previous section are equivalence relations.
+  previous section are indeed equivalence relations.
 
   \begin{lem}\label{equiv} 
   The relations @{text "\<approx>ty"}$_{1..n}$ and @{text "\<approx>bn"}$_{1..m}$ are
@@ -1746,7 +1747,7 @@
   \end{lem}
 
   \begin{proof} 
-  The proof is by mutual induction over the definitions. The non-trivial
+  The proof is by induction over the definitions. The non-trivial
   cases involve premises built up by $\approx_{\textit{set}}$, 
   $\approx_{\textit{set+}}$ and $\approx_{\textit{list}}$. They 
   can be dealt with as in Lemma~\ref{alphaeq}. However, the transitivity
@@ -1754,106 +1755,78 @@
   \end{proof}
 
   \noindent 
-  We can feed this lemma into our quotient package and obtain new types @{text
-  "ty"}$^\alpha_{1..n}$ representing alpha-equated terms of types @{text "ty"}$_{1..n}$. 
-  
-  We also obtain definitions for the term-constructors @{text
-  "C"}$^\alpha_{1..k}$ from the raw term-constructors @{text "C"}$_{1..k}$,
-  and similar definitions for the free-atom functions @{text
+  We can feed the last lemma into our quotient package and obtain new types
+  @{text "ty"}$^\alpha_{1..n}$ representing alpha-equated terms of types
+  @{text "ty"}$_{1..n}$. We also obtain definitions for the term-constructors
+  @{text "C"}$^\alpha_{1..k}$ from the raw term-constructors @{text
+  "C"}$_{1..k}$, and similar definitions for the free-atom functions @{text
   "fa_ty"}$^\alpha_{1..n}$ and @{text "fa_bn"}$^\alpha_{1..m}$ as well as the
-  binding functions @{text "bn"}$^\alpha_{1..m}$. For this we have to show
-  by induction over the definitions of alpha-equivalences that the ``raw'' 
-  functions are respectful. This means we need to establish that
-
-  \[\mbox{
-  \begin{tabular}{lll}
-  @{text "x \<approx>ty\<^isub>i x'"} & implies & @{text "fa_ty\<^isub>i x = fa_ty\<^isub>i x'"}\\
-  @{text "x \<approx>ty\<^isub>l x'"} & implies & @{text "fa_bn\<^isub>j x = fa_bn\<^isub>j x'"}\\
-  @{text "x \<approx>ty\<^isub>l x'"} & implies & @{text "bn\<^isub>j x = bn\<^isub>j x'"}\\
-  \end{tabular}
-  }\]\smallskip
-  
-  \noindent
-  holds whereby @{text "ty\<^isub>l"} is the type over which @{text "bn\<^isub>j"} is defined. A 
-  similar property is needed for the constructors @{text "C"}$_{1..k}$. In order 
-  to establish it we need to prove that
-
-  \[\mbox{
-  \begin{tabular}{lll}
-  @{text "x \<approx>ty\<^isub>l x'"} & implies & @{text "x \<approx>bn\<^isub>j x'"}\\
-  \end{tabular}
-  }\]\smallskip
-
-  \noindent
-  The respectfulness properties are crucial, ... ???
-  However, these definitions are not really useful to the 
-  user, since they are given in terms of the isomorphisms we obtained by 
-  creating new types in Isabelle/HOL (recall the picture shown in the 
-  Introduction).
+  binding functions @{text "bn"}$^\alpha_{1..m}$. However, these definitions
+  are not really useful to the user, since they are given in terms of the
+  isomorphisms we obtained by creating new types in Isabelle/HOL (recall the
+  picture shown in the Introduction).
 
   The first useful property for the user is the fact that distinct 
-  term-constructors are not 
-  equal, that is
+  term-constructors are not equal, that is the property
   
-  \[\label{distinctalpha}
+  \begin{equation}\label{distinctalpha}
   \mbox{@{text "C"}$^\alpha$~@{text "x\<^isub>1 \<dots> x\<^isub>r"}~@{text "\<noteq>"}~% 
   @{text "D"}$^\alpha$~@{text "y\<^isub>1 \<dots> y\<^isub>s"}} 
-  \]\smallskip
+  \end{equation}\smallskip
   
   \noindent
   whenever @{text "C"}$^\alpha$~@{text "\<noteq>"}~@{text "D"}$^\alpha$.
-  In order to derive this fact, we use the definition of alpha-equivalence
+  In order to derive this property, we use the definition of alpha-equivalence
   and establish that
   
-  \[\label{distinctraw}
+  \begin{equation}\label{distinctraw}
   \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>r"}\;$\not\approx$@{text ty}\;@{text "D y\<^isub>1 \<dots> y\<^isub>s"}}
-  \]\smallskip
+  \end{equation}\smallskip
 
   \noindent
   holds for the corresponding raw term-constructors.
   In order to deduce \eqref{distinctalpha} from \eqref{distinctraw}, our quotient
   package needs to know that the raw term-constructors @{text "C"} and @{text "D"} 
   are \emph{respectful} w.r.t.~the alpha-equivalence relations (see \cite{Homeier05}).
-  Assuming, for example, @{text "C"} is of type @{text "ty"} with argument types
+  Given, for example, @{text "C"} is of type @{text "ty"} with argument types
   @{text "ty"}$_{1..r}$, respectfulness amounts to showing that
   
-  \begin{center}
+  \[\mbox{
   @{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}
-  \end{center}  
+  }\]\smallskip
 
   \noindent
-  holds under the assumptions that we have \mbox{@{text
+  holds under the assumptions \mbox{@{text
   "x\<^isub>i \<approx>ty\<^isub>i x\<PRIME>\<^isub>i"}} whenever @{text "x\<^isub>i"}
   and @{text "x\<PRIME>\<^isub>i"} are recursive arguments of @{text C} and
-  @{text "x\<^isub>i = x\<PRIME>\<^isub>i"} whenever they are non-recursive arguments. We can prove this
-  implication by applying the corresponding rule in our alpha-equivalence
-  definition and by establishing the following auxiliary implications %facts 
-  %
-  \begin{equation}\label{fnresp}
-  \mbox{%
-  \begin{tabular}{ll@ {\hspace{7mm}}ll}
-  \mbox{\it (i)} & @{text "x \<approx>ty\<^isub>i x\<PRIME>"}~~@{text "\<Rightarrow>"}~~@{text "fa_ty\<^isub>i x = fa_ty\<^isub>i x\<PRIME>"} &
-  \mbox{\it (iii)} & @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~@{text "\<Rightarrow>"}~~@{text "bn\<^isub>j x = bn\<^isub>j x\<PRIME>"}\\
+  @{text "x\<^isub>i = x\<PRIME>\<^isub>i"} whenever they are non-recursive arguments 
+  (similarly for @{text "D"}). For this we have to show
+  by induction over the definitions of alpha-equivalences the following 
+  auxiliary implications
 
-  \mbox{\it (ii)} & @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~@{text "\<Rightarrow>"}~~@{text "fa_bn\<^isub>j x = fa_bn\<^isub>j x\<PRIME>"} &
-  \mbox{\it (iv)} & @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~@{text "\<Rightarrow>"}~~@{text "x \<approx>bn\<^isub>j x\<PRIME>"}\\
-  \end{tabular}}
-  \end{equation}
-
+  \begin{equation}\label{fnresp}\mbox{
+  \begin{tabular}{lll}
+  @{text "x \<approx>ty\<^isub>i x'"} & implies & @{text "fa_ty\<^isub>i x = fa_ty\<^isub>i x'"}\\
+  @{text "x \<approx>ty\<^isub>l x'"} & implies & @{text "fa_bn\<^isub>j x = fa_bn\<^isub>j x'"}\\
+  @{text "x \<approx>ty\<^isub>l x'"} & implies & @{text "bn\<^isub>j x = bn\<^isub>j x'"}\\
+  @{text "x \<approx>ty\<^isub>l x'"} & implies & @{text "x \<approx>bn\<^isub>j x'"}\\
+  \end{tabular}
+  }\end{equation}\smallskip
+  
   \noindent
-  They can be established by induction on @{text "\<approx>ty"}$_{1..n}$. Whereas the first,
-  second and last implication are true by how we stated our definitions, the 
-  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 lifting of the corresponding binding functions in Ott to alpha-equated
-  terms is impossible.
+  whereby @{text "ty\<^isub>l"} is the type over which @{text "bn\<^isub>j"}
+  is defined. These implications can be established by induction on @{text
+  "\<approx>ty"}$_{1..n}$. Whereas the first, second and last implication are true by
+  how we stated our definitions, the 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 lifting 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 
+  \eqref{distinctraw}. Having the facts \eqref{fnresp} at our disposal, we can 
   also lift properties that characterise when two raw terms of the form
   
   \[
@@ -1870,16 +1843,14 @@
   
   \noindent
   We call these conditions as \emph{quasi-injectivity}. They correspond to
-  the premises in our alpha-equivalence relations.
+  the premises in our alpha-equiva\-lence relations.
 
-  Next we can lift the permutation 
-  operations defined in \eqref{ceqvt}. In order to make this 
-  lifting to go through, we have to show that the permutation operations are respectful. 
-  This amounts to showing that the 
-  alpha-equivalence relations are equivariant \cite{HuffmanUrban10}.
-  , which we already established 
-  in Lemma~\ref{equiv}. 
-  As a result we can add the equations
+  Next we can lift the permutation operations defined in \eqref{ceqvt}. In
+  order to make this lifting to go through, we have to show that the
+  permutation operations are respectful. This amounts to showing that the
+  alpha-equivalence relations are equivariant, which
+  we already established in Lemma~\ref{equiv}. As a result we can add the
+  equations
   
   \begin{equation}\label{calphaeqvt}
   @{text "\<pi> \<bullet> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r) = C\<^sup>\<alpha> (\<pi> \<bullet> x\<^isub>1) \<dots> (\<pi> \<bullet> x\<^isub>r)"}
@@ -1893,19 +1864,43 @@
   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 cases lemma (explained in the next section)
-  and a structural induction principle 
-  for the types @{text "ty\<AL>"}$_{1..n}$. The conclusion of the induction principle is
-  of the form
-  
-  \begin{equation}\label{weakinduct}
-  \mbox{@{text "P\<^isub>1 x\<^isub>1 \<and> \<dots> \<and> P\<^isub>n x\<^isub>n "}}
-  \end{equation} \smallskip
-  
+  Finally we can add to our infrastructure cases lemmas and a structural
+  induction principle for the types @{text "ty\<AL>"}$_{1..n}$. The cases
+  lemmas allow the user to deduce a property @{text "P"} by exhaustively 
+  analysing all cases how the elements in a type @{text "ty\<AL>"}$_i$ can
+  be constructed (that means one case for each of term-constructors @{text "C\<AL>"}$_{1..m}$
+  of type @{text "ty\<AL>"}$_i\,$). These are lifted versions of the cases
+  lemma over the raw type  @{text "ty"}$_i$ and schematically look as
+  follows
+
+  \[
+  \infer{P}
+  {\begin{array}{l}
+  @{text "\<forall>x\<^isub>1\<dots>x\<^isub>k. y = C\<AL>\<^isub>1 x\<^isub>1 \<dots> x\<^isub>k \<Rightarrow> P"}\\
+  \hspace{5mm}\ldots\\
+  @{text "\<forall>x\<^isub>1\<dots>x\<^isub>l. y = C\<AL>\<^isub>m x\<^isub>1 \<dots> x\<^isub>l \<Rightarrow> P"}\\
+  \end{array}}
+  \]\smallskip
+
   \noindent
-  whereby the @{text P}$_{1..n}$ are predicates and the @{text x}$_{1..n}$ 
-  have types @{text "ty\<AL>"}$_{1..n}$. This induction principle has for each
-  term constructor @{text "C"}$^\alpha$ a premise of the form
+  where @{text "y"} is a variable of type @{text "ty"}$_i$ and @{text "P"} is the 
+  property that is established by the case analysis. Similarly, we have an induction
+  principle for the types @{text "ty\<AL>"}$_{1..n}$, which is
+
+   \[
+  \infer{@{text "P\<^isub>1 y\<^isub>1 \<and> \<dots> \<and> P\<^isub>n y\<^isub>n "}}
+  {\begin{array}{l}
+  @{text "\<forall>x\<^isub>1\<dots>x\<^isub>k. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<AL>\<^isub>1 x\<^isub>1 \<dots> x\<^isub>k)"}\\
+  \hspace{5mm}\ldots\\
+  @{text "\<forall>x\<^isub>1\<dots>x\<^isub>l. P\<^isub>r x\<^isub>r \<and> \<dots> \<and> P\<^isub>s x\<^isub>s \<Rightarrow> P (C\<AL>\<^isub>m x\<^isub>1 \<dots> x\<^isub>l)"}\\
+  \end{array}}
+  \]\smallskip
+
+  \noindent
+  whereby the @{text P}$_{1..n}$ are the properties established by induction 
+  and the @{text y}$_{1..n}$ are of type @{text "ty\<AL>"}$_{1..n}$. 
+  This induction principle has for all term constructors @{text "C"}$^\alpha$ 
+  a premise of the form
   
   \begin{equation}\label{weakprem}
   \mbox{@{text "\<forall>x\<^isub>1\<dots>x\<^isub>r. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r)"}} 
@@ -1913,7 +1908,26 @@
 
   \noindent 
   in which the @{text "x"}$_{i..j}$ @{text "\<subseteq>"} @{text "x"}$_{1..r}$ are 
-  the recursive arguments of @{text "C\<AL>"}. 
+  the recursive arguments of the term constructor. In case of the lambda-calculus,
+  the cases lemma and the induction principle boil down to the following:
+
+  \[\mbox{
+  \begin{tabular}{c@ {\hspace{10mm}}c}
+  \infer{@{text "P"}}
+  {\begin{array}{l}
+   @{text "\<forall>x. y = Var\<^sup>\<alpha> x \<Rightarrow> P"}\\
+   @{text "\<forall>x\<^isub>1 x\<^isub>2. y = App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P"}\\
+   @{text "\<forall>x\<^isub>1 x\<^isub>2. y = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P"}
+   \end{array}} &
+
+  \infer{@{text "P y"}}
+  {\begin{array}{l}
+   @{text "\<forall>x. P (Var\<^sup>\<alpha> x)"}\\
+   @{text "\<forall>x\<^isub>1 x\<^isub>2. P x\<^isub>1 \<and> P x\<^isub>2 \<Rightarrow> P (App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
+   @{text "\<forall>x\<^isub>1 x\<^isub>2. P x\<^isub>2 \<Rightarrow> P (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}
+   \end{array}}
+  \end{tabular}}
+  \]\smallskip
 
   By working now completely on the alpha-equated level, we
   can first show that the free-atom functions and binding functions are
@@ -1925,12 +1939,12 @@
   @{text "\<pi> \<bullet> (fa_bn\<AL>\<^isub>j  x)"} & $=$ & @{text "fa_bn\<AL>\<^isub>j (\<pi> \<bullet> x)"}\\
   @{text "\<pi> \<bullet> (bn\<AL>\<^isub>j  x)"}    & $=$ & @{text "bn\<AL>\<^isub>j (\<pi> \<bullet> x)"}\\
   \end{tabular}}
-  \]
+  \]\smallskip
 
   
   \noindent
   These properties can be established using the induction principle for the
-  types @{text "ty\<AL>"}$_{1..n}$.  in \eqref{weakinduct}.  Having these
+  types @{text "ty\<AL>"}$_{1..n}$.  Having these
   equivariant properties established, we can show that the support of
   term-constructors @{text "C\<^sup>\<alpha>"} is included in the support of its
   arguments, that means
@@ -1940,14 +1954,13 @@
   \]\smallskip
  
   \noindent
-  holds. This allows us to prove by induction that
-  every @{text x} of type @{text "ty\<AL>"}$_{1..n}$ is finitely supported. 
-  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 fact is important in a nominal setting, but also provides evidence 
-  that our notions of free-atoms and alpha-equivalence are correct.
+  holds. This allows us to prove by induction that every @{text x} of type
+  @{text "ty\<AL>"}$_{1..n}$ is finitely supported. 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 fact is important in the nominal setting, but
+  also provides evidence that our notions of free-atoms and alpha-equivalence
+  are sensible.
 
   \begin{thm} 
   For @{text "x"}$_{1..n}$ with type @{text "ty\<AL>"}$_{1..n}$, we have