# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269961234 -7200
# Node ID c6116722b44d57831f4e3e8ea9d1e111ca12eda5
# Parent  a5def8fe07141b875083ef46d3a0c42f7244c3d1
More on section 5.

diff -r a5def8fe0714 -r c6116722b44d Paper/Paper.thy
--- a/Paper/Paper.thy	Tue Mar 30 16:59:23 2010 +0200
+++ b/Paper/Paper.thy	Tue Mar 30 17:00:34 2010 +0200
@@ -1280,8 +1280,10 @@
 section {* The Lifting of Definitions and Properties *}
 
 text {*
-  To define quotient types of the raw types we first show that the defined relations
-  are equivalence relations.
+%%% TODO Fix 'Andrew Pitts' in bibliography
+
+  To define the quotient types we first need to show that the defined
+  relations 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.
@@ -1323,17 +1325,34 @@
 
   \begin{center}
   \begin{tabular}{cp{7cm}}
+%skipped permute_zero and permute_add, since we do not have a permutation
+%definition
   $\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$ & induction. The induction principle that we obtain by lifting
+    is the weak induction principle, just on the term structure \\
+  $\bullet$ & quasi-injectivity. This means the equations that specify
+    when two constructors are equal and comes from lifting the alpha
+    equivalence defining relations\\
   $\bullet$ & distinctness\\
+%may be skipped
   $\bullet$ & equivariance of @{term "fv"} and @{term "bn"} functions\\
   \end{tabular}
   \end{center}
 
+  Notice that until now we have not said anything about the support of the
+  defined type. This is because we could not use the general definition of
+  support in lifted theorems, since it does not preserve the relation.
+  Indeed, take the term @{text "\<lambda>x. x"}. The support of the term is empty @{term "{}"},
+  since the @{term "x"} is bound. On the raw level, before the binding is
+  introduced the term has the support equal to @{text "{x}"}.
+
+  We will now show that the quotient types have a finite support.
+
+
+
+
 *}
 
 text {*