# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1269961163 -7200
# Node ID a5def8fe07141b875083ef46d3a0c42f7244c3d1
# Parent  0c3c66f5c0e7e7e4f725c7b607ed82a95b38907c# Parent  0d057e57e9a892e1adc105e43f942393201feaf6
merged

diff -r 0c3c66f5c0e7 -r a5def8fe0714 Paper/Paper.thy
--- a/Paper/Paper.thy	Tue Mar 30 16:59:00 2010 +0200
+++ b/Paper/Paper.thy	Tue Mar 30 16:59:23 2010 +0200
@@ -1280,35 +1280,59 @@
 section {* The Lifting of Definitions and Properties *}
 
 text {*
-  To define quotient types of the raw types we first show that the defined relation
-  in an equivalence relation.
+  To define quotient types of the raw types we first show that the defined relations
+  are equivalence relations.
 
-  \begin{lemma} The relations $\approx_1,\ldots,\approx_n,\approx_{bn1},\ldots,\approx_{bnm}$
-  defined as above are equivalence relations.
+  \begin{lemma} The relations @{text "\<approx>\<^isub>1 \<dots> \<approx>\<^isub>1"} and @{text "\<approx>bn\<^isub>1 \<dots> \<approx>bn\<^isub>m"}
+  defined as above are equivalence relations and are equivariant.
   \end{lemma}
-  \begin{proof}
-  Reflexivity by induction on the raw datatype, symmetry and transitivity by
-  induction on the alpha equivalence relation. Using lemma \ref{alphaeq}, the
-  conditions follow by simple calculations.
-  \end{proof}
+  \begin{proof} Reflexivity by induction on the raw datatype. Symmetry,
+  transitivity and equivariance by induction on the alpha equivalence
+  relation. Using lemma \ref{alphaeq}, the conditions follow by simple
+  calculations.  \end{proof}
+
+  \noindent We then define the quotient types @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}.  To lift
+  the raw definitions to the quotient type, we need to prove that they
+  \emph{respect} the relation. We follow the definition of respectfullness given
+  by Homeier~\cite{Homeier05}. The intuition behind a respectfullness condition
+  is that when a function (or constructor) is given arguments that are
+  alpha-equivalent the results are also alpha equivalent. For arguments that are
+  not of any of the relations taken into account, equivalence is replaced by
+  equality. In particular the respectfullness condition for a @{text "bn"}
+  function means that for alpha equivalent raw terms it returns the same bound
+  names. Thanks to the restrictions on the binding functions introduced in
+  Section~\ref{sec:alpha} we can show that are respectful.
 
-  \noindent We then define the quotient types @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}. To lift the raw
-  definitions to the quotient type, we need to prove that they \emph{respect} the
-  relation. We follow the definition of respectfullness given by
-  Homeier~\cite{Homeier05}. The intuition behind a respectfullness condition is that
-  when a function (or constructor) is given arguments that are alpha-equivalent the
-  results are also alpha equivalent. For arguments that are not of any of the relations
-  taken into account, equvalence is replaced by equality.
+  \begin{lemma} The functions @{text "bn\<^isub>1 \<dots> bn\<^isub>m"}, @{text "fv_ty\<^isub>1 \<dots> fv_ty\<^isub>n"},
+  the raw constructors, the raw permutations and @{text "\<approx>bn\<^isub>1 \<dots> \<approx>bn\<^isub>m"} are
+  respectful w.r.t. the relations @{text "\<approx>\<^isub>1 \<dots> \<approx>\<^isub>n"}.
+  \end{lemma}
+  \begin{proof} Respectfullness of permutations is a direct consequence of
+  equivariance.  All other properties by induction on the alpha-equivalence
+  relation.  For @{text "bn"} the thesis follows by simple calculations thanks
+  to the restrictions on the binding functions. For @{text "fv"} functions it
+  follows using respectfullness of @{text "bn"}. For type constructors it is a
+  simple calculation thanks to the way alpha-equivalence was defined. For @{text
+  "alpha_bn"} after a second induction on the second relation by simple
+  calculations.  \end{proof}
 
-% Could be written as a \{lemma}
-  In particular the respectfullness condition for a @{text "bn"} function means that for
-  alpha equivalent raw terms it returns the same bound names. Thanks to the
-  restrictions on the binding functions introduced in Section~\ref{sec:alpha}, we can
-  show that are respectful. With this we can show the respectfullness of @{text "fv_ty"}
-  functions by induction. Respectfullness of permutations is a direct consequence
-  of equivariance. Respectfullness of type constructors and of @{text "alpha_bn"} follows
-  by induction from type definitions.
+  With these respectfullness properties we can use the quotient package
+  to define the above constants on the quotient level. We can then automatically
+  lift the theorems that talk about the raw constants to theorems on the quotient
+  level. The following lifted properties are proved:
 
+  \begin{center}
+  \begin{tabular}{cp{7cm}}
+  $\bullet$ & permutation defining equations \\
+  $\bullet$ & @{term "bn"} defining equations \\
+  $\bullet$ & @{term "fv_ty"} and @{term "fv_bn"} defining equations \\
+  $\bullet$ & induction (weak induction, just on the term structure) \\
+  $\bullet$ & quasi-injectivity, the equations that specify when two
+     constructors are equal\\
+  $\bullet$ & distinctness\\
+  $\bullet$ & equivariance of @{term "fv"} and @{term "bn"} functions\\
+  \end{tabular}
+  \end{center}
 
 *}